From 0096fda961fe992a0582a15b75ce0aaa46cba195 Mon Sep 17 00:00:00 2001
From: Erwan Jahier <jahier@imag.fr>
Date: Mon, 9 Jun 2008 10:57:10 +0200
Subject: [PATCH] When evaluating the type of a node call, check that the
arguments and the parameters input types are compatible with Unify.f.
Apply (if necessary) the resulting substitution to the output parameters.
Also, when checking array concat, try to unify the types of both
arrays instead of just checking their equality.
This of course triggers some errors in the non-reg tests. One of
this error is due to a bug in the parser, where the list of parameter
was inversed twice. I've also fixed that in this change.
---
src/TODO | 1 -
src/evalType.ml | 46 ++++++----
src/parser.mly | 4 +-
src/test/should_work/NONREG/Watch.lus | 1 -
src/test/should_work/call/call06.lus | 5 +-
src/test/test.res.exp | 125 ++++++++++++++------------
6 files changed, 97 insertions(+), 85 deletions(-)
diff --git a/src/TODO b/src/TODO
index 87a788df..0479905e 100644
--- a/src/TODO
+++ b/src/TODO
@@ -92,7 +92,6 @@ les operateurs aritmetiques, bof.
***********************************************************************************
*** questions pour bibi
-*parser ligne 532 : ne pas re-inverser la liste des parametres
* Faire qque chose pour les 2 verrues dans predefSemantics
pas facile...
diff --git a/src/evalType.ml b/src/evalType.ml
index c1e4c90a..05738353 100644
--- a/src/evalType.ml
+++ b/src/evalType.ml
@@ -1,4 +1,4 @@
-(** Time-stamp: <modified the 09/06/2008 (at 10:17) by Erwan Jahier> *)
+(** Time-stamp: <modified the 09/06/2008 (at 10:50) by Erwan Jahier> *)
open Predef
@@ -33,8 +33,21 @@ and (eval_by_pos_type :
PredefEvalType.f op lxm sargs (List.map (f id_solver) args)
| CALL_eff node_exp_eff ->
+ let lti = List.map (fun v -> v.var_type_eff) node_exp_eff.it.inlist_eff in
let lto = List.map (fun v -> v.var_type_eff) node_exp_eff.it.outlist_eff in
- lto
+ let t_args = List.flatten (List.map (f id_solver) args) in
+ let llti = List.length lti and lt_args = List.length t_args in
+ if llti <> lt_args then
+ raise (EvalType_error(
+ sprintf
+ "\n*** arity error: %d argument(s) are expected, whereas %d is/are provided"
+ llti lt_args))
+ else
+ (match Unify.f lti t_args with
+ | Unify.Equal -> lto
+ | Unify.Unif subst -> List.map (Unify.subst_type subst) lto
+ | Unify.Ko msg -> raise (Compile_error(lxm, msg))
+ )
| IDENT_eff id -> (
(* [id] migth be a constant, but also a variable *)
@@ -60,33 +73,28 @@ and (eval_by_pos_type :
| CONCAT_eff -> (
match List.map (f id_solver) args with
- | [[Array_type_eff (teff0, size0)]; [Array_type_eff (teff1, size1)]] -> (
- if teff0 = teff1 then
- [Array_type_eff (teff0, size0+size1)]
- else
- raise(EvalType_error(
- sprintf "type combination error, can't concat %s with %s"
- (CompiledDataDump.string_of_type_eff teff0)
- (CompiledDataDump.string_of_type_eff teff1)))
- )
- | [_;_] ->
- raise(EvalType_error("type combination error, array type expected"))
+ | [[Array_type_eff (teff0, size0)]; [Array_type_eff (teff1, size1)]] ->
+ let teff =
+ match Unify.f [teff0] [teff1] with
+ | Unify.Equal -> teff1
+ | Unify.Unif subst -> Unify.subst_type subst teff1
+ | Unify.Ko msg -> raise (Compile_error(lxm, msg))
+ in
+ [Array_type_eff (teff, size0+size1)]
| _ ->
raise(EvalType_error(sprintf "arity error: 2 expected instead of %d"
(List.length args)))
)
-
| STRUCT_ACCESS_eff fid -> (
let type_args_eff = List.flatten (List.map (f id_solver) args) in
match type_args_eff with
| [Struct_type_eff (name, fl)] -> (
- try
- [fst (List.assoc fid fl)]
+ try [fst (List.assoc fid fl)]
with Not_found ->
raise (EvalType_error
- (Printf.sprintf "%s is not a field of struct %s"
- (Ident.to_string fid)
- (CompiledDataDump.string_of_type_eff(List.hd type_args_eff))))
+ (Printf.sprintf "%s is not a field of struct %s"
+ (Ident.to_string fid)
+ (CompiledDataDump.string_of_type_eff(List.hd type_args_eff))))
)
| [x] -> type_error [x] "struct type"
| x -> arity_error x "1"
diff --git a/src/parser.mly b/src/parser.mly
index 4823570d..50aeaa0e 100644
--- a/src/parser.mly
+++ b/src/parser.mly
@@ -530,10 +530,10 @@ sxType:
sxExtNodeDecl:
TK_EXTERN TK_FUNCTION sxIdent sxParams TK_RETURNS sxParams sxOptSemicol
- { treat_external_node false $3 (List.rev $4) (List.rev $6) }
+ { treat_external_node false $3 $4 $6 }
| TK_EXTERN TK_NODE sxIdent sxParams TK_RETURNS sxParams sxOptSemicol
/* WARNING ! il faut remettre les listes à l'endroit */
- { treat_external_node true $3 (List.rev $4) (List.rev $6) }
+ { treat_external_node true $3 $4 $6 }
;
diff --git a/src/test/should_work/NONREG/Watch.lus b/src/test/should_work/NONREG/Watch.lus
index 25f6ab56..554dc7b2 100644
--- a/src/test/should_work/NONREG/Watch.lus
+++ b/src/test/should_work/NONREG/Watch.lus
@@ -138,7 +138,6 @@ extern function ALARM_TIME_TO_MAIN_DISPLAY
(time: ALARM_TIME_TYPE) returns (display: MAIN_DISPLAY_TYPE);
-- translation of "time" to the main display format
-
extern function MAKE_DISPLAY
(main: MAIN_DISPLAY_TYPE;
mini: MINI_DISPLAY_TYPE;
diff --git a/src/test/should_work/call/call06.lus b/src/test/should_work/call/call06.lus
index 7e11e92f..b7d9e8b3 100644
--- a/src/test/should_work/call/call06.lus
+++ b/src/test/should_work/call/call06.lus
@@ -4,7 +4,6 @@ extern function bip(x,y : bool) returns (z,t : bool);
node call06(x,y : bool) returns (z,t : bool);
let
assert (x=>z);
--- (z,t) = bip(x,y);
- z = true;
- (z,t) = bip(1,y); -- i should detect this one during type checking
+ (z,t) = bip(x,y);
+
tel
diff --git a/src/test/test.res.exp b/src/test/test.res.exp
index d09a795f..7e159c98 100644
--- a/src/test/test.res.exp
+++ b/src/test/test.res.exp
@@ -412,12 +412,12 @@ tel
-- end of node Watch__DIVIDE
extern function Watch__MAKE_DISPLAY(
- labels:Watch__LABELS_TYPE;
- enhanced:Watch__DISPLAY_POSITION;
- status:Watch__STATUS_TYPE;
- alpha:Watch__string;
+ main:Watch__MAIN_DISPLAY_TYPE;
mini:Watch__MINI_DISPLAY_TYPE;
- main:Watch__MAIN_DISPLAY_TYPE)
+ alpha:Watch__string;
+ status:Watch__STATUS_TYPE;
+ enhanced:Watch__DISPLAY_POSITION;
+ labels:Watch__LABELS_TYPE)
returns (
display:Watch__DISPLAY_TYPE);
@@ -481,11 +481,11 @@ let
Watch__WATCH_TIME_TO_MINI_DISPLAY(watch_time), stringAL)));
tel
-- end of node Watch__DISPLAY
-extern function Watch__SOMME(i3:int; i2:int; i1:int) returns (somme:int);
+extern function Watch__SOMME(i1:int; i2:int; i3:int) returns (somme:int);
extern function Watch__COMPARE_WATCH_ALARM_TIME(
- alarm_time:Watch__ALARM_TIME_TYPE;
- watch_time:Watch__WATCH_TIME_TYPE)
+ watch_time:Watch__WATCH_TIME_TYPE;
+ alarm_time:Watch__ALARM_TIME_TYPE)
returns (
result:bool);
node Watch__EDGE(b:bool) returns (edge:bool);
@@ -500,8 +500,8 @@ returns (
newtime:Watch__ALARM_TIME_TYPE);
extern function Watch__SET_ALARM_TIME(
- position:Watch__ALARM_TIME_POSITION;
- time:Watch__ALARM_TIME_TYPE)
+ time:Watch__ALARM_TIME_TYPE;
+ position:Watch__ALARM_TIME_POSITION)
returns (
new_time:Watch__ALARM_TIME_TYPE);
@@ -597,14 +597,14 @@ returns (
new_time:Watch__WATCH_TIME_TYPE);
extern function Watch__INCREMENT_WATCH_TIME_IN_SET_MODE(
- position:Watch__WATCH_TIME_POSITION;
- time:Watch__WATCH_TIME_TYPE)
+ time:Watch__WATCH_TIME_TYPE;
+ position:Watch__WATCH_TIME_POSITION)
returns (
new_time:Watch__WATCH_TIME_TYPE);
extern function Watch__SET_WATCH_TIME(
- position:Watch__WATCH_TIME_POSITION;
- time:Watch__WATCH_TIME_TYPE)
+ time:Watch__WATCH_TIME_TYPE;
+ position:Watch__WATCH_TIME_POSITION)
returns (
new_time:Watch__WATCH_TIME_TYPE);
@@ -1773,22 +1773,22 @@ End of Syntax table dump.
Exported types:
Exported constants:
Exported nodes:
-extern node clock__outOnIn(b:bool; a:bool) returns (c:bool when b);
-extern node clock__inOnIn(b:bool when a; a:bool) returns (c:bool);
+extern node clock__outOnIn(a:bool; b:bool) returns (c:bool when b);
+extern node clock__inOnIn(a:bool; b:bool when a) returns (c:bool);
extern node clock__outOnOut(
- b:bool;
- a:bool)
+ a:bool;
+ b:bool)
returns (
- d:bool when c;
- c:bool);
+ c:bool;
+ d:bool when c);
extern node clock__all(
- b:bool when a;
- a:bool)
+ a:bool;
+ b:bool when a)
returns (
- d:bool when c when b when a;
- c:bool when b when a);
+ c:bool when b when a;
+ d:bool when c when b when a);
node clock__clock(in:bool) returns (ok:bool);
var
v1:bool;
@@ -4535,7 +4535,7 @@ let
tel
-- end of node simple__simple
extern function simple__f1(x:int) returns (y:int);
-extern function simple__f2(u:int; v:int) returns (t:bool; s:int);
+extern function simple__f2(u:int; v:int) returns (s:int; t:bool);
----------------------------------------------------------------------
====> ../lus2lic -vl 3 --compile-all-items should_work/NONREG/stopwatch.lus
@@ -6462,8 +6462,7 @@ extern function call06__bip(x:bool; y:bool) returns (z:bool; t:bool);
node call06__call06(x:bool; y:bool) returns (z:bool; t:bool);
let
assert((x => z));
- z = true;
- (z, t) = call06__bip(1, y);
+ (z, t) = call06__bip(x, y);
tel
-- end of node call06__call06
@@ -7155,15 +7154,15 @@ End of Syntax table dump.
Exported types:
Exported constants:
Exported nodes:
-extern node clock__clock2(v:bool when u; u:bool) returns (y:bool);
-extern node clock__clock3(u:bool) returns (y:bool when x; x:bool);
+extern node clock__clock2(u:bool; v:bool when u) returns (y:bool);
+extern node clock__clock3(u:bool) returns (x:bool; y:bool when x);
extern node clock__clock4(
- v:bool when u;
- u:bool)
+ u:bool;
+ v:bool when u)
returns (
- y:bool when x;
- x:bool);
+ x:bool;
+ y:bool when x);
node clock__clock(a:bool; b:bool) returns (c:bool; d:bool when c);
var
z:bool;
@@ -7302,10 +7301,10 @@ returns (
d1:bool^2);
extern node decl__n2(
- d1:bool;
a1:decl__t1^8;
b1:decl__t1^8;
- c1:decl__t1^8)
+ c1:decl__t1^8;
+ d1:bool)
returns (
e1:decl__t1^8^5);
@@ -7396,10 +7395,10 @@ returns (
d1:bool);
extern node declaration__n2(
- d1:bool;
a1:declaration__t1^8;
b1:declaration__t1^8;
- c1:declaration__t1^8)
+ c1:declaration__t1^8;
+ d1:bool)
returns (
e1:declaration__t1^8^5);
node declaration__n4(a1:bool) returns (b1:bool);
@@ -11424,6 +11423,9 @@ type deSimone__tabType = bool^10;
type deSimone__cell_accu = deSimone::cell_accu {token : bool; grant : bool};
Exported constants:
Exported nodes:
+*** Error in file "should_work/lionel/deSimone.lus", line 51, col 23 to 30, token 'deSimone': type error:
+*** arity error: 2 argument(s) are expected, whereas 1 is/are provided
+
node deSimone__oneCell(
accu_in:deSimone::cell_accu {token : bool;
@@ -11463,17 +11465,6 @@ let
10>>(cell_accu{token=new_token;grant=true}, request);
tel
-- end of node deSimone__deSimone
-node deSimone__prop1(request:bool^10) returns (ok:bool);
-var
- acknowledge:bool^10;
- nb_acknowledge:int;
-let
- acknowledge = deSimone__deSimone(request);
- nb_acknowledge = red<<node deSimone__prop1_iter, const 10>>(0,
- acknowledge);
- ok = (nb_acknowledge <= 1);
-tel
--- end of node deSimone__prop1
----------------------------------------------------------------------
====> ../lus2lic -vl 3 --compile-all-items should_work/lionel/iterFibo.lus
@@ -13792,6 +13783,7 @@ let
ok = init -> pre(in);
tel
-- end of node Pbool__n
+const main__pi = 3.141590;
node main__main(
i:int;
@@ -14165,15 +14157,15 @@ End of Syntax table dump.
Exported types:
Exported constants:
Exported nodes:
-extern node clock__clock2(v:bool when u; u:bool) returns (y:bool);
-extern node clock__clock3(u:bool) returns (y:bool when x; x:bool);
+extern node clock__clock2(u:bool; v:bool when u) returns (y:bool);
+extern node clock__clock3(u:bool) returns (x:bool; y:bool when x);
extern node clock__clock4(
- v:bool when u;
- u:bool)
+ u:bool;
+ v:bool when u)
returns (
- y:bool when x;
- x:bool);
+ x:bool;
+ y:bool when x);
node clock__clock(a:bool; b:bool) returns (c:bool; d:bool when c);
var
z:bool;
@@ -14212,6 +14204,7 @@ End of Syntax table dump.
*** Error in file "should_fail/clock/inonout.lus", line 3, col 46 to 46, token 'c':
*** 'c': Unknown variable.
*** Current variables are:
+ a:bool
----------------------------------------------------------------------
@@ -14360,16 +14353,30 @@ End of Syntax table dump.
Exported types:
Exported constants:
Exported nodes:
-*** Error in file "should_fail/semantics/bad_call03.lus", line 7, col 5 to 5, token '=': type mismatch:
-*** 'real^3' (left-hand-side)
-*** is not compatible with
-*** 'o^3' (right-hand-side)
-
function bad_call03__toto(i1:o^3; i2:o^3) returns (o:o^3);
let
o = Lustre__map<<node Lustre__+, const 3>>(i1, i2);
tel
-- end of node bad_call03__toto
+node bad_call03__titi(c:real^3; d:real^3) returns (y:real^3);
+let
+ y = bad_call03__toto(c, d);
+tel
+-- end of node bad_call03__titi
+
+node bad_call03__bad_call03(
+ a:int^3;
+ b:int^3;
+ c:real^3;
+ d:real^3)
+returns (
+ x:int^3;
+ y:real^3);
+let
+ x = bad_call03__toto(a, b);
+ y = bad_call03__titi(c, d);
+tel
+-- end of node bad_call03__bad_call03
----------------------------------------------------------------------
====> ../lus2lic -vl 3 --compile-all-items should_fail/semantics/bug.lus
--
GitLab