From 09b1e4d6dba949bfef839d34efcbf09112c94b02 Mon Sep 17 00:00:00 2001
From: Erwan Jahier <jahier@imag.fr>
Date: Thu, 12 Jun 2008 11:21:10 +0200
Subject: [PATCH] Begin to implement clock checkinhg of expressions.
It does not work, I have changed my mind to use a more general
clocking algorithm based on unification. I commit that current state
just in case I change my mind again...
---
src/Makefile | 2 +
src/TODO | 3 +
src/compiledData.ml | 28 +-
src/compiledDataDump.ml | 8 +
src/evalClock.ml | 374 ++++++++++++++++++
src/evalClock.mli | 35 ++
src/evalType.ml | 4 +-
src/getEff.ml | 83 ++--
src/getEff.mli | 6 +-
src/lazyCompiler.ml | 3 +-
src/parserUtils.ml | 52 +--
src/predefEvalClock.ml | 57 ++-
src/predefEvalClock.mli | 6 +-
src/predefEvalType.ml | 15 +-
src/predefEvalType.mli | 4 +-
src/syntaxTreeCore.ml | 3 +-
src/test/should_fail/clock/clock.lus | 14 +-
src/test/should_fail/semantics/bad_call03.lus | 2 +-
src/test/test.res.exp | 36 +-
19 files changed, 635 insertions(+), 100 deletions(-)
create mode 100644 src/evalClock.ml
create mode 100644 src/evalClock.mli
diff --git a/src/Makefile b/src/Makefile
index 00354d09..ff93d3dc 100644
--- a/src/Makefile
+++ b/src/Makefile
@@ -46,6 +46,8 @@ SOURCES = \
./evalConst.ml \
./evalType.mli \
./evalType.ml \
+ ./evalClock.mli \
+ ./evalClock.ml \
./getEff.mli \
./getEff.ml \
./lazyCompiler.ml \
diff --git a/src/TODO b/src/TODO
index ce75d692..84c7f2bf 100644
--- a/src/TODO
+++ b/src/TODO
@@ -136,6 +136,9 @@ n'est pas le cas pour l'instant...
*** facile
+* dans evalType, je ne checke pas tous les arguments !
+ecrire les tests idoines puis faire ces checks.
+
* verifier que chacun des exemples du repertoire "should_fail" échoue
avec un bon message d'erreur.
diff --git a/src/compiledData.ml b/src/compiledData.ml
index c7f579a8..15bfdd2a 100644
--- a/src/compiledData.ml
+++ b/src/compiledData.ml
@@ -1,4 +1,4 @@
-(** Time-stamp: <modified the 09/06/2008 (at 10:05) by Erwan Jahier> *)
+(** Time-stamp: <modified the 12/06/2008 (at 11:06) by Erwan Jahier> *)
(**
@@ -239,6 +239,7 @@ and const_eff =
and var_info_eff = {
var_name_eff : Ident.t;
var_nature_eff : var_nature;
+ var_number_eff : int;
var_type_eff : type_eff;
var_clock_eff : clock_eff;
}
@@ -285,7 +286,24 @@ and static_arg_eff =
| NodeStaticArgEff of (Ident.t * node_exp_eff)
-
+let (make_dummy_var: Ident.idref -> var_info_eff) =
+ fun idref ->
+ let id = Ident.of_idref idref in
+ let str = Ident.string_of_idref idref in
+ let teff =
+ try ignore (int_of_string str); Int_type_eff
+ with _ ->
+ try ignore (float_of_string str); Real_type_eff
+ with _ -> Bool_type_eff
+ in
+ {
+ var_name_eff = id;
+ var_nature_eff = VarLocal;
+ var_number_eff = 0;
+ var_type_eff = teff;
+ var_clock_eff = BaseEff;
+ }
+
(****************************************************************************)
(** Type check_flag
@@ -439,6 +457,12 @@ let (type_eff_of_left_eff: left_eff -> type_eff) =
| LeftArrayEff(_, _, t_eff) -> t_eff
| LeftSliceEff(_, _, t_eff) -> t_eff
+let rec (clock_of_left_eff: left_eff -> clock_eff) =
+ function
+ | LeftVarEff (var_info_eff, _) -> var_info_eff.var_clock_eff
+ | LeftFieldEff (left_eff,_,_) -> clock_of_left_eff left_eff
+ | LeftArrayEff (left_eff,_,_) -> clock_of_left_eff left_eff
+ | LeftSliceEff (left_eff,_,_) -> clock_of_left_eff left_eff
(*---------------------------------------------------------------------
diff --git a/src/compiledDataDump.ml b/src/compiledDataDump.ml
index fd2b1a68..55bb79b0 100644
--- a/src/compiledDataDump.ml
+++ b/src/compiledDataDump.ml
@@ -313,6 +313,12 @@ and (node_of_node_exp_eff: node_exp_eff -> string) =
)
+and string_of_clock2 (ck : clock_eff) =
+ match ck with
+ | BaseEff -> " on base "
+ | On veff ->" on " ^ (Ident.to_string veff.var_name_eff) ^
+ (string_of_clock veff.var_clock_eff)
+
and string_of_clock (ck : clock_eff) =
match ck with
| BaseEff -> ""
@@ -320,6 +326,8 @@ and string_of_clock (ck : clock_eff) =
(string_of_clock veff.var_clock_eff)
+and string_of_clock_list cl =
+ "(" ^ (String.concat ", " (List.map string_of_clock cl)) ^ ")"
(*---------------------------------------------------------------------
Formatage standard des erreurs de compil
diff --git a/src/evalClock.ml b/src/evalClock.ml
new file mode 100644
index 00000000..fb1c68b4
--- /dev/null
+++ b/src/evalClock.ml
@@ -0,0 +1,374 @@
+(** Time-stamp: <modified the 12/06/2008 (at 11:10) by Erwan Jahier> *)
+
+
+open Predef
+open PredefEvalConst
+open SyntaxTree
+open SyntaxTreeCore
+open CompiledData
+open CompiledDataDump
+open Printf
+open Lxm
+open Errors
+
+
+(** clock checking of expression.
+
+ nb:
+ In the following, we speak about input/output arguments/parameters of an
+ expression because:
+ - the difficult case wrt clock checking concerns nodes
+ - other kind of expressions can be seen as nodes, as they «take» some input
+ arguments, and return some outputs.
+
+
+ The clock checking consists in verifying that expression arguments clocks
+ are compatible with the expression parameters clocks.
+
+ For instance, for a node of profile:
+
+ node toto(a; b when a) returns (x when a; y when x);
+
+ when it is called, e.g., like that:
+
+ (v1,v2) = toto(v3,v4);
+
+ we need to check that:
+ - the argument clocks are ok, i.e., v4 is on v3 (1)
+ cf the [check_arg] function below
+ - the result clocks are ok, i.e., v2 is on v1 + v1 is on v3 (2)
+ cf the [check_res] function below
+
+ Let's focus first on argument checking:
+*)
+type clock_info_par =
+ | Base_par of var_info_eff
+ | Input_par of var_info_eff * int
+ | Output_par of var_info_eff * int
+
+(** A [clock_info_par] is an abstraction of a [var_info_eff] meant to
+ be able to check the clocks of expressions arguments. A pair of
+ list of [clock_info_par] is therefore represent the expression
+ clock profile.
+
+ In this abstraction, the name binding is replaced by a relative
+ position binding.
+
+ For instance, for a node toto of profile:
+
+ node toto(a; b when a) returns (x when a; y when x);
+
+ we have as input profile: [Base_arg; Input_par 0]
+ and as output profile: [Input_par 0, Output_par 0]
+
+ This information is extracted from the node profile by
+ [get_clock_profile]:
+*)
+
+type clock_profile = clock_info_par list * clock_info_par list
+
+let (get_clock_profile : Lxm.t -> node_exp_eff -> clock_profile) =
+ fun lxm n ->
+ let (il, ol) = (n.inlist_eff, n.outlist_eff) in
+ let rec find_index v l i =
+ match l with
+ | [] -> raise Not_found
+ | v2::tail -> if v=v2 then i else find_index v tail (i+1)
+ in
+ let f v =
+ match v.var_clock_eff with
+ | BaseEff -> Base_par(v)
+ | On clk ->
+ try Input_par(v, find_index clk il 0)
+ with Not_found ->
+ try Output_par(v, find_index clk ol 0)
+ with Not_found ->
+ let msg = "\n*** "^ (Ident.to_string clk.var_name_eff)^
+ ": unknown clock" in
+ raise(Compile_error (lxm, msg))
+ in
+ (List.map f il, List.map f ol)
+
+(** We also introduce a second kind of var_info_eff abstraction, dedicated
+ to the checking of expresion result:
+*)
+type clock_info_res =
+ | Base_res of var_info_eff
+ | OnVar of var_info_eff * var_info_eff
+ | OnRel of var_info_eff * int
+
+let string_of_clock_info_res = function
+ | Base_res v -> (Ident.to_string v.var_name_eff) ^ " on base"
+ | OnVar (v,clk) -> (Ident.to_string v.var_name_eff) ^ " on " ^
+ (Ident.to_string clk.var_name_eff)
+ | OnRel (v,i) -> (Ident.to_string v.var_name_eff) ^ " on #" ^
+ (string_of_int i) ^ "^nth"
+
+(** For example, when checking the equation
+
+ (x,y)=toto(a,b);
+
+ the clock checking of "toto(a,b)" will return
+ [OnVar a, OnRel 0]
+ which makes it easy to compute that:
+ - x is on a,
+ - y is on x
+
+ Hence, [clock_info_res list] is the type that is return by f, the
+ main function of this clock checking module.
+
+
+ ** Checking expression arguments
+ --------------------------------
+
+ ok. So now, let us detail how we clock check expression
+ arguments. e.g., in the equation
+
+ (x,y)=toto(a,b);
+
+ we want to make sure that the clocks of the argument "a" and "b" are compatible
+ with the input clock profile of "toto".
+
+ To do that, we suppose we have already computed:
+
+ - "ci_par_l" the expected input clock profile (via "get_clock_profile" defined
+ above)
+ - "cl" the list of arguments "clock_info_res" (via a rec call to f)
+*)
+let (check_args : Lxm.t -> clock_info_par list -> clock_info_res list -> unit) =
+ fun lxm ci_par_l cl ->
+ let (f : clock_info_par -> clock_info_res -> unit) =
+ fun cip cir -> match (cip,cir) with
+ | Base_par _, Base_res _ -> ()
+ | Input_par(vpar,i), OnRel (v,j) -> if i = j then () else
+ let msg = "\n*** clock error" in
+ raise(Compile_error(lxm,msg))
+
+ | Input_par(vpar,i), OnVar (v,clk) ->
+ (match List.nth cl i with
+ | OnVar (v2,clk2) ->
+ if clk2 = clk then () else
+ let msg = "\n*** clock error: " ^
+ (string_of_clock_info_res (OnVar (v,clk))) ^ " (provided) <> " ^
+ (string_of_clock_info_res (OnVar (v2,clk2))) ^ " (expected)"
+ in
+ raise(Compile_error(lxm, msg))
+ | Base_res(v2) ->
+ let msg = "\n*** clock error: " ^
+ (string_of_clock_info_res (OnVar (v,clk))) ^ " (provided) <> " ^
+ "base (expected)"
+ in
+ raise(Compile_error(lxm,msg))
+ | OnRel (v,i) -> assert false
+ )
+ | Input_par _, Base_res(_)
+ | Base_par _, _ ->
+ raise(Compile_error(lxm,"\n*** clock error: bad arg clocks"))
+ | Output_par _, _ -> assert false (* inputs cannot be clocked on outputs*)
+ in
+ List.iter2 f ci_par_l cl
+
+(** In order to use check_args, we need another intermediary function
+ that merges list of list of [clock_info_res]. Indeed, to be able
+ to check the arguments of an expression like:
+
+ tata(toto(a,b),toto(c,d));
+
+ We sais before that we compute the [clock_info_res list] of the
+ arguments via a recursive call to f. But such a recursive call
+ returns a list of list of [clock_info_res], which contains
+ information relative to variable positions. Therefore we cannot
+ just flatten that list of list; we also need to shift the indexes
+ encoding variable positions.
+
+ For example, for checking the args of tata above, we call
+
+ merge_clock_ll [[OnVar a; OnRel 0]; [OnVar c; OnRel 0]]
+
+ that ougth to return the following flattenned list with shifted index:
+
+ [OnVar a; OnRel 0; OnVar c; OnRel 2]
+
+ and then we can call check_res with that list.
+*)
+
+let (merge_clock_ll: clock_info_res list list -> clock_info_res list) =
+ fun ll ->
+ let f (shift,acc) l =
+ let new_l = List.map
+ (function
+ | Base_res(v) -> Base_res(v)
+ | OnVar(v,clk) -> OnVar(v,clk)
+ | OnRel(v,j) -> OnRel(v,j+shift)
+ )
+ l
+ in
+ (shift + (List.length l), acc @ new_l)
+ in
+ snd (List.fold_left f (0,[]) ll)
+
+
+
+(** Checking expression result
+ --------------------------
+
+ e.g., in the equation:
+
+ (x,y)=toto(a,b);
+
+ we want to check that the clocks of "x" and "y" are compatible with
+ the output clock profile of node "toto".
+
+ To do that, we suppose we have already computed:
+
+ - "cil" the expected output clock profile (via "get_clock_profile" again)
+ - "cel" the list of result "clock_info_res"
+
+*)
+let (check_res2 : Lxm.t -> clock_info_res list -> clock_info_res list -> unit) =
+ fun lxm cil cel ->
+ if cil = cel then () else
+ let msg = "\n*** clock error: " ^
+ (String.concat ", " (List.map string_of_clock_info_res cil)) ^ " <> " ^
+ (String.concat ", " (List.map string_of_clock_info_res cel))
+ in
+ raise(Compile_error(lxm,msg))
+
+let (get_nth_var : clock_info_res list -> int -> var_info_eff) =
+ fun vil i ->
+ match List.nth vil i with
+ | Base_res(v) -> v
+ | OnVar(v,_) -> v
+ | OnRel(v,_) -> v
+
+let (check_res : Lxm.t -> clock_info_res list -> clock_eff list -> unit) =
+ fun lxm rigth left ->
+ let cpt = ref 0 in
+ let (f : clock_info_res -> clock_eff -> unit) =
+ fun cip ce ->
+ incr cpt;
+ match (cip,ce) with
+ | Base_res(_), BaseEff -> ()
+ | OnVar(v1,clk1), On clk2 ->
+ if clk1 = clk2 then () else
+ let msg = "\n*** clock error (ckeck_res), " ^
+ (string_of_int !cpt) ^ "nth element:"^
+ (Ident.to_string clk2.var_name_eff) ^ " <> " ^
+ (Ident.to_string clk1.var_name_eff)
+ in
+ raise(Compile_error(lxm,msg))
+
+ | OnRel(v,i), On clk ->
+ let clk2 = get_nth_var rigth i in
+ if clk2 = clk then () else
+ let msg = "\n*** clock error (ckeck_res), " ^
+ (string_of_int !cpt) ^ "nth element:"^
+ (Ident.to_string clk.var_name_eff) ^ " <> " ^
+ (Ident.to_string clk2.var_name_eff)
+ in
+ raise(Compile_error(lxm,msg))
+
+
+ | Base_res _, On _
+ | _, BaseEff -> raise(Compile_error(lxm,"\n*** clock error"))
+ in
+ if List.length rigth <> List.length left then
+ raise(Compile_error(lxm,"\n*** clock error"))
+ else
+ List.iter2 f rigth left
+
+
+
+
+(** Now we can go on and define [f]. *)
+
+(******************************************************************************)
+
+let rec (f : id_solver -> val_exp_eff -> clock_info_res list) =
+ fun id_solver ve ->
+ match ve with
+ | CallByPosEff ({it=posop; src=lxm}, OperEff args) -> (
+ eval_by_pos_clock id_solver posop lxm args
+ )
+ | CallByNameEff ({it=nmop; src=lxm}, nmargs ) ->
+ try eval_by_name_clock id_solver nmop lxm nmargs
+ with EvalConst_error msg ->
+ raise (Compile_error(lxm, "\n*** can't eval constant: "^msg))
+
+and (eval_by_pos_clock : id_solver -> by_pos_op_eff -> Lxm.t -> val_exp_eff list
+ -> clock_info_res list) =
+ fun id_solver posop lxm args ->
+ match posop with
+ | CALL_eff node_exp_eff ->
+ let (ip,op) = get_clock_profile node_exp_eff.src node_exp_eff.it in
+ let clocks_of_args = merge_clock_ll (List.map (f id_solver) args) in
+ let res =
+ List.map
+ (function
+ | Base_par(v) -> Base_res(v)
+ | Output_par(v, i) -> OnRel(v, i)
+ | Input_par(v, i) ->
+ (* that would occur if one writes
+ toto(tata(x),x)
+ where one output clock of tata depends on one of its input, eg
+
+ node tata(i) returns (o when i)
+
+ arg...
+ *)
+ let msg = "\n*** clock error: this kind of expression can "^
+ "not be clocked with our current algo, sorry..." in
+ raise (Compile_error(lxm,msg))
+ )
+ op
+ in
+ check_args lxm ip clocks_of_args;
+ res
+
+
+ | CURRENT_eff -> assert false (* prendre l'horloge de l'horloge de l'argument *)
+
+ | WHEN_eff ->
+ let clk_exp = List.nth args 1 in
+ (* Non: je doit plutot extraire de clk_exp une var_info_eff,
+ et raler si ca n'est pas possible.
+ *)
+ (f id_solver clk_exp)
+
+
+ | MERGE_eff _ -> f id_solver (List.hd args)
+
+ | Predef_eff (_,_)
+ | WITH_eff
+ | ARROW_eff
+ | FBY_eff
+ | CONCAT_eff
+ | HAT_eff(_,_)
+ | PRE_eff
+ | STRUCT_ACCESS_eff _
+ | ARRAY_ACCES_eff (_, _)
+ | ARRAY_SLICE_eff (_,_)
+ | ARRAY_eff -> (
+ (* check that args are of the same clocks, which also is the
+ returned clock *)
+ match List.flatten (List.map (f id_solver) args) with
+ | clk1::tail ->
+ if List.for_all (fun clk -> clk = clk1) tail then [clk1] else
+ raise (Compile_error(lxm, "clock mismatch"))
+ | [] -> assert false
+ )
+
+ | TUPLE_eff -> List.flatten (List.map (f id_solver) args)
+
+
+ | IDENT_eff idref -> [Base_res(make_dummy_var idref)] (* all constants are on the base clock *)
+
+
+and (eval_by_name_clock : id_solver -> by_name_op_eff -> Lxm.t ->
+ (Ident.t Lxm.srcflagged * val_exp_eff) list -> clock_info_res list) =
+ fun id_solver namop lxm namargs ->
+ match namop with
+ | STRUCT_anonymous_eff -> assert false (* cf EvalClock.f *)
+ | STRUCT_eff opid -> assert false
+(* [id_solver.id2clock opid lxm] *)
+
diff --git a/src/evalClock.mli b/src/evalClock.mli
new file mode 100644
index 00000000..d911f3f3
--- /dev/null
+++ b/src/evalClock.mli
@@ -0,0 +1,35 @@
+(** Time-stamp: <modified the 12/06/2008 (at 09:50) by Erwan Jahier> *)
+
+open CompiledData
+
+
+(** [f ids ve ]checks that [ve] is well-clocked (i.e., for node calls,
+ it checks that the argument and the parameter clocks are correct),
+ and returns a clock profile that contains all the necessary information
+ to be able to check.
+*)
+
+type clock_info_res
+
+val f : id_solver -> val_exp_eff -> clock_info_res list
+
+(** [check_res lxm cel cil] check that the expected output clock
+ profile of an expression "cil" is compatible with the result clocks
+ "cel" of the expression.
+
+ For instance, for clocks checking the equation
+
+ (x,y)=toto(a,b);
+
+ it checks that the clock of "(x,y)" (cel) is compatible with the
+ output clock profile of node toto (cil).
+
+ The type [clock_info_res] is exported to be able to call that
+ function outside this module, which is necessary to clock
+ equations (an equation is not an expression (i.e., not a
+ val_exp_eff).
+
+*)
+
+val check_res : Lxm.t -> clock_info_res list -> clock_eff list -> unit
+val merge_clock_ll: clock_info_res list list -> clock_info_res list
diff --git a/src/evalType.ml b/src/evalType.ml
index 05738353..21613165 100644
--- a/src/evalType.ml
+++ b/src/evalType.ml
@@ -1,4 +1,4 @@
-(** Time-stamp: <modified the 09/06/2008 (at 10:50) by Erwan Jahier> *)
+(** Time-stamp: <modified the 09/06/2008 (at 14:47) by Erwan Jahier> *)
open Predef
@@ -99,7 +99,7 @@ and (eval_by_pos_type :
| [x] -> type_error [x] "struct type"
| x -> arity_error x "1"
)
- | ARRAY_ACCES_eff (_, teff) -> [teff]
+ | ARRAY_ACCES_eff (_, teff) -> [teff] (* XXX check args type! *)
| ARRAY_SLICE_eff (sieff,teff) ->
[Array_type_eff(teff, sieff.se_width)]
diff --git a/src/getEff.ml b/src/getEff.ml
index 4c4e55eb..c12aebf2 100644
--- a/src/getEff.ml
+++ b/src/getEff.ml
@@ -1,4 +1,4 @@
-(** Time-stamp: <modified the 09/06/2008 (at 10:03) by Erwan Jahier> *)
+(** Time-stamp: <modified the 12/06/2008 (at 11:12) by Erwan Jahier> *)
open Lxm
@@ -32,7 +32,6 @@ let rec (typ:CompiledData.id_solver -> SyntaxTreeCore.type_exp ->
with GetEffType_error msg ->
raise (Compile_error(texp.src, "can't eval type: "^msg))
-(******************************************************************************)
(* exported *)
let rec (clock : CompiledData.id_solver -> SyntaxTreeCore.clock_exp ->
CompiledData.clock_eff)=
@@ -42,6 +41,43 @@ let rec (clock : CompiledData.id_solver -> SyntaxTreeCore.clock_exp ->
| NamedClock id -> On (id_solver.id2var (Ident.to_idref id.it) id.src)
+(******************************************************************************)
+(* Checks that the left part has the same type as the right one. *)
+and (type_check_equation: id_solver -> eq_info srcflagged -> left_eff list ->
+ val_exp_eff -> unit) =
+ fun id_solver eq_info lpl_eff ve_eff ->
+ let lpl_teff = List.map type_eff_of_left_eff lpl_eff in
+ let right_part = EvalType.f id_solver ve_eff in
+ if (List.length lpl_teff <> List.length right_part) then
+ raise (Compile_error(eq_info.src,
+ "tuple size error: \n*** the tuple size is\n***\t"^
+ (string_of_int (List.length lpl_teff)) ^
+ " for the left-hand-side, and \n***\t" ^
+ (string_of_int (List.length right_part)) ^
+ " for the right-hand-side"))
+ else
+ List.iter2
+ (fun le re ->
+ if le <> re then
+ let msg = "type mismatch: \n***\t'"
+ ^ (CompiledDataDump.string_of_type_eff le) ^
+ "' (left-hand-side) \n*** is not compatible with \n***\t'"
+ ^ (CompiledDataDump.string_of_type_eff re) ^ "' (right-hand-side)"
+ in
+ raise (Compile_error(eq_info.src, msg))
+ )
+ lpl_teff
+ right_part
+
+(* Checks that the left part has the same clock as the right one. *)
+and (clock_check_equation:id_solver -> eq_info srcflagged -> left_eff list ->
+ val_exp_eff -> unit) =
+ fun id_solver eq_info lpl_eff ve_eff ->
+ let lpl_clk = List.map (clock_of_left_eff) lpl_eff in
+ let right_part = EvalClock.f id_solver ve_eff in
+ EvalClock.check_res eq_info.src right_part lpl_clk
+
+
(******************************************************************************)
let (get_static_params_from_idref : SymbolTab.t -> Lxm.t -> Ident.idref ->
static_param srcflagged list) =
@@ -64,7 +100,7 @@ let rec (node : CompiledData.id_solver -> SyntaxTreeCore.node_exp srcflagged ->
in
id_solver.id2node idref static_args_eff lxm
-
+
(** [check_static_arg this pn id sa (symbols, acc)] compile a static arg
into a static_arg_eff
*)
@@ -82,12 +118,12 @@ and (check_static_arg : CompiledData.id_solver ->
| StaticArgIdent idref, StaticParamType(id) ->
let teff = node_id_solver.id2type idref sa.src in
TypeStaticArgEff (id, teff)
-
+
| StaticArgIdent idref, StaticParamNode(id,_,_,_) ->
let sargs = [] in
- (* We suppose that static arg cannot themselves be
- template calls (eg, f<<g<<3>>>> is forbidden)
- *)
+ (* We suppose that static arg cannot themselves be
+ template calls (eg, f<<g<<3>>>> is forbidden)
+ *)
let neff = node_id_solver.id2node idref sargs sa.src in
NodeStaticArgEff (id, neff)
@@ -122,16 +158,17 @@ and (check_static_arg : CompiledData.id_solver ->
| StaticArgNode _, StaticParamType(id)
| StaticArgNode _, StaticParamConst(id,_)
-
+
| StaticArgConst _, StaticParamNode(id,_,_,_)
| StaticArgConst _, StaticParamType(id)
- ->
+ ->
assert false (* can it occur actually? Let's wait it occurs...*)
in
sa_eff
(******************************************************************************)
+
(* exported *)
and (eq : id_solver -> eq_info srcflagged -> eq_info_eff srcflagged) =
fun id_solver eq_info ->
@@ -139,32 +176,8 @@ and (eq : id_solver -> eq_info srcflagged -> eq_info_eff srcflagged) =
let lpl_eff = List.map (translate_left_part id_solver) lpl
and ve_eff = translate_val_exp id_solver ve
in
- (* Type check here (i.e., check that the left part has the same type as the
- right one).
- *)
- let lpl_teff = List.map type_eff_of_left_eff lpl_eff in
- let right_part = EvalType.f id_solver ve_eff in
- if (List.length lpl_teff <> List.length right_part) then
- raise (Compile_error(eq_info.src,
- "tuple size error: \n*** the tuple size is\n***\t"^
- (string_of_int (List.length lpl_teff)) ^
- " for the left-hand-side, and \n***\t" ^
- (string_of_int (List.length right_part)) ^
- " for the right-hand-side"))
- else
- List.iter2
- (fun le re ->
- if le <> re then
- let msg = "type mismatch: \n***\t'"
- ^ (CompiledDataDump.string_of_type_eff le) ^
- "' (left-hand-side) \n*** is not compatible with \n***\t'"
- ^ (CompiledDataDump.string_of_type_eff re) ^ "' (right-hand-side)"
- in
- raise (Compile_error(eq_info.src, msg))
- )
- lpl_teff
- right_part;
- (* type is ok *)
+ type_check_equation id_solver eq_info lpl_eff ve_eff;
+(* clock_check_equation id_solver eq_info lpl_eff ve_eff; *)
flagit (lpl_eff, ve_eff) eq_info.src
diff --git a/src/getEff.mli b/src/getEff.mli
index ff5df7dc..cc6a5826 100644
--- a/src/getEff.mli
+++ b/src/getEff.mli
@@ -1,4 +1,4 @@
-(** Time-stamp: <modified the 09/06/2008 (at 10:05) by Erwan Jahier> *)
+(** Time-stamp: <modified the 09/06/2008 (at 11:27) by Erwan Jahier> *)
(** This module defines functions that translate SyntaxTreeCore datatypes into
@@ -9,8 +9,8 @@
- calls [EvalConst.f] wherever it is necessary, i.e., for items
that are required to be static, such as arrays sizes, or array
indexes.
-
- - recursively call itself for translating sub-terms
+ - recursively calls itself for translating sub-terms
+ - checks the arguments and the parameters are compatible (i.e., that they unify)
*)
val typ : CompiledData.id_solver -> SyntaxTreeCore.type_exp -> CompiledData.type_eff
diff --git a/src/lazyCompiler.ml b/src/lazyCompiler.ml
index 48f83c5b..3a3d27f0 100644
--- a/src/lazyCompiler.ml
+++ b/src/lazyCompiler.ml
@@ -1,4 +1,4 @@
-(** Time-stamp: <modified the 09/06/2008 (at 10:20) by Erwan Jahier> *)
+(** Time-stamp: <modified the 10/06/2008 (at 10:47) by Erwan Jahier> *)
open Lxm
@@ -565,6 +565,7 @@ and (node_check_do: t -> CompiledData.node_key -> Lxm.t -> SymbolTab.t ->
let vi_eff = {
var_name_eff = vi.it.var_name;
var_nature_eff = vi.it.var_nature;
+ var_number_eff = vi.it.var_number;
var_type_eff = t_eff;
var_clock_eff = c_eff;
}
diff --git a/src/parserUtils.ml b/src/parserUtils.ml
index c2d48e1d..8e230a56 100644
--- a/src/parserUtils.ml
+++ b/src/parserUtils.ml
@@ -1,4 +1,4 @@
-(** Time-stamp: <modified the 06/06/2008 (at 18:01) by Erwan Jahier> *)
+(** Time-stamp: <modified the 10/06/2008 (at 10:20) by Erwan Jahier> *)
@@ -310,15 +310,21 @@ let (clocked_ids_to_var_infos : var_nature ->
(((Lxm.t list) * type_exp) list * SyntaxTreeCore.clock_exp) list ->
var_info srcflagged list) =
fun vnat vdefs ->
+ let i = ref 0 in
let makevar lxm te ce =
- Lxm.flagit
- {
- var_nature = vnat ;
- var_name = (Lxm.id lxm) ;
- var_type = te ;
- var_clock = ce ;
- }
- lxm
+ let res =
+ Lxm.flagit
+ {
+ var_nature = vnat;
+ var_name = (Lxm.id lxm);
+ var_number = !i;
+ var_type = te;
+ var_clock = ce;
+ }
+ lxm
+ in
+ incr i;
+ res
in
flat_twice_flagged_list vdefs makevar
@@ -338,20 +344,22 @@ let (treat_node_decl : bool -> Lxm.t -> static_param srcflagged list ->
let rec (treat_vars : clocked_ids list -> var_nature -> var_info srcflagged list) =
(* Procedure de traitement des in, out ou loc, paramétrée par la [var_nature] *)
fun vdefs nat ->
- match vdefs with
- | [] -> []
- | (tids, ck)::reste ->
- let put_var_in_table (lxm: Lxm.t) (ty: type_exp) =
- let vinfo = {
- var_nature = nat; var_name = (Lxm.id lxm);
- var_type = ty; var_clock = ck
- }
+ let i = ref 0 in
+ match vdefs with
+ | [] -> []
+ | (tids, ck)::reste ->
+ let put_var_in_table (lxm: Lxm.t) (ty: type_exp) =
+ let vinfo = {
+ var_nature = nat; var_name = (Lxm.id lxm);
+ var_type = ty; var_clock = ck; var_number = !i
+ }
+ in
+ incr i;
+ add_info vtable "variable" lxm vinfo;
+ Lxm.flagit vinfo lxm
in
- add_info vtable "variable" lxm vinfo;
- Lxm.flagit vinfo lxm
- in
- (flat_flagged_list tids put_var_in_table)
- @ (treat_vars reste nat)
+ (flat_flagged_list tids put_var_in_table)
+ @ (treat_vars reste nat)
in
let invars = treat_vars indefs VarInput
and outvars = treat_vars outdefs VarOutput
diff --git a/src/predefEvalClock.ml b/src/predefEvalClock.ml
index 511a9be2..de392113 100644
--- a/src/predefEvalClock.ml
+++ b/src/predefEvalClock.ml
@@ -1,30 +1,59 @@
-(** Time-stamp: <modified the 05/06/2008 (at 11:11) by Erwan Jahier> *)
+(** Time-stamp: <modified the 09/06/2008 (at 12:25) by Erwan Jahier> *)
open Predef
open CompiledData
+(* exported *)
type clocker = CompiledData.clock_eff Predef.evaluator
-let (aa_clocker: clocker) =
+(* exported *)
+exception EvalClock_error of string
+
+
+(** A few useful clock profiles *)
+
+let (arity_zero_profile: clocker) = assert false
+let (arity_one_profile: clocker) =
function
| [clk1] -> clk1
- | _ -> print_string "a good error msg"; assert false
+ | _ -> raise (EvalClock_error "a good error msg")
-let (aaa_clocker: clocker) =
+let (arity_two_profile: clocker) =
function
| [clk1; clk2] ->
- if clk1 = clk2 then clk1 else (print_string "a good error msg"; assert false)
+ if clk1 = clk2 then clk1 else raise (EvalClock_error "a good error msg")
| _ ->
- print_string "a good error msg"; assert false
+ raise (EvalClock_error "a good error msg")
-
-(** A few useful clock profiles *)
-(* let bb_profile = [(id "i", b)], [(id "o", b)] *)
-
-
+
+let if_clock_profile c = assert false
+let fillred_clock_profile c = assert false
+let map_clock_profile c = assert false
+let boolred_clock_profile c = assert false
(* This table contains the clock profile of predefined operators *)
-let (f: op -> clocker) =
- fun op ->
- assert false
+let (f: op -> Lxm.t -> CompiledData.static_arg_eff list -> clocker) =
+ fun op lxm sargs -> assert false
+(* match op with *)
+(* | TRUE_n | FALSE_n | ICONST_n _id | RCONST_n _id *)
+(* -> arity_zero_profile *)
+(* *)
+(* | NOT_n | REAL2INT_n | INT2REAL_n | UMINUS_n | IUMINUS_n | RUMINUS_n *)
+(* -> arity_one_profile *)
+(* *)
+(* *)
+(* | IMPL_n | AND_n | OR_n | XOR_n *)
+(* | NEQ_n | EQ_n | LT_n | LTE_n | GT_n | GTE_n *)
+(* | MINUS_n | PLUS_n | TIMES_n | SLASH_n *)
+(* | RMINUS_n | RPLUS_n | RTIMES_n | RSLASH_n *)
+(* | DIV_n | MOD_n | IMINUS_n | IPLUS_n | ISLASH_n | ITIMES_n *)
+(* -> arity_two_profile *)
+(* *)
+(* | IF_n -> if_clock_profile *)
+(* | Red | Fill | FillRed -> fillred_clock_profile lxm sargs *)
+(* | Map -> map_clock__profile lxm sargs *)
+(* | BoolRed -> boolred_clock__profile lxm sargs *)
+(* *)
+(* | NOR_n | DIESE_n -> assert false *)
+
diff --git a/src/predefEvalClock.mli b/src/predefEvalClock.mli
index 8e561823..cd2dabb5 100644
--- a/src/predefEvalClock.mli
+++ b/src/predefEvalClock.mli
@@ -1,4 +1,8 @@
-(** Time-stamp: <modified the 05/06/2008 (at 11:01) by Erwan Jahier> *)
+(** Time-stamp: <modified the 09/06/2008 (at 12:31) by Erwan Jahier> *)
type clocker = CompiledData.clock_eff Predef.evaluator
+exception EvalClock_error of string
+
+
+val f: Predef.op -> Lxm.t -> CompiledData.static_arg_eff list -> clocker
diff --git a/src/predefEvalType.ml b/src/predefEvalType.ml
index b95b27a2..6c9d127d 100644
--- a/src/predefEvalType.ml
+++ b/src/predefEvalType.ml
@@ -1,4 +1,4 @@
-(** Time-stamp: <modified the 09/06/2008 (at 10:09) by Erwan Jahier> *)
+(** Time-stamp: <modified the 10/06/2008 (at 10:48) by Erwan Jahier> *)
open Predef
open SyntaxTreeCore
@@ -198,10 +198,12 @@ let (make_node_exp_eff : op -> Lxm.t -> static_arg_eff list -> node_exp_eff) =
(Ident.pack_name_of_string "Lustre") (Ident.of_string (Predef.op2string op))
in
let (lti,lto) = op2profile op lxm sargs in
+ let i = ref 0 in
let to_var_info_eff nature (id, te) =
{
var_name_eff = id;
var_nature_eff = nature;
+ var_number_eff = !i;
var_type_eff = te;
var_clock_eff = BaseEff;
}
@@ -209,7 +211,7 @@ let (make_node_exp_eff : op -> Lxm.t -> static_arg_eff list -> node_exp_eff) =
{
node_key_eff = id,sargs ;
inlist_eff = List.map (to_var_info_eff VarInput) lti;
- outlist_eff = List.map (to_var_info_eff VarOutput) lto;
+ outlist_eff = (i:=0; List.map (to_var_info_eff VarOutput) lto);
loclist_eff = None;
def_eff = ExternEff;
has_mem_eff = false;
@@ -249,12 +251,11 @@ let (f : op -> Lxm.t -> CompiledData.static_arg_eff list -> typer) =
fun t teff -> match teff with
(* substitutes [t] in [teff] *)
| Bool_type_eff -> Bool_type_eff
- | Int_type_eff -> Int_type_eff
+ | Int_type_eff -> Int_type_eff
| Real_type_eff -> Real_type_eff
- | External_type_eff l -> External_type_eff l
- | Enum_type_eff(l,el) -> Enum_type_eff(l,el)
- | Array_type_eff(teff,i) ->
- Array_type_eff(subst_type t teff, i)
+ | External_type_eff l -> External_type_eff l
+ | Enum_type_eff(l,el) -> Enum_type_eff(l,el)
+ | Array_type_eff(teff,i) -> Array_type_eff(subst_type t teff, i)
| Struct_type_eff(l, fl) ->
Struct_type_eff(
l,
diff --git a/src/predefEvalType.mli b/src/predefEvalType.mli
index 707db070..668759ba 100644
--- a/src/predefEvalType.mli
+++ b/src/predefEvalType.mli
@@ -1,4 +1,4 @@
-(** Time-stamp: <modified the 09/06/2008 (at 10:05) by Erwan Jahier> *)
+(** Time-stamp: <modified the 09/06/2008 (at 12:23) by Erwan Jahier> *)
open CompiledData
@@ -16,7 +16,7 @@ val arity_error : 'a list -> string -> 'b
val f : Predef.op -> Lxm.t -> CompiledData.static_arg_eff list -> typer
-
+(* Does not work for NOR_n and DIESE_n! *)
val make_node_exp_eff : Predef.op -> Lxm.t -> static_arg_eff list -> node_exp_eff
diff --git a/src/syntaxTreeCore.ml b/src/syntaxTreeCore.ml
index bb0e67c1..d5bd7a13 100644
--- a/src/syntaxTreeCore.ml
+++ b/src/syntaxTreeCore.ml
@@ -1,4 +1,4 @@
-(** Time-stamp: <modified the 05/06/2008 (at 16:09) by Erwan Jahier> *)
+(** Time-stamp: <modified the 10/06/2008 (at 10:49) by Erwan Jahier> *)
(** (Raw) Abstract syntax tree of source programs. *)
@@ -48,6 +48,7 @@ and var_info_table = (Ident.t, var_info srcflagged) Hashtbl.t
and var_info = {
var_nature : var_nature;
var_name : Ident.t;
+ var_number : int;
var_type : type_exp;
var_clock : clock_exp
}
diff --git a/src/test/should_fail/clock/clock.lus b/src/test/should_fail/clock/clock.lus
index 86512949..9e9a0645 100644
--- a/src/test/should_fail/clock/clock.lus
+++ b/src/test/should_fail/clock/clock.lus
@@ -1,15 +1,15 @@
--- Entee sur entree
+-- Entree sur entree: ok
extern node clock2(u: bool; v: bool when u) returns (y: bool );
--- Sortie sur sortie
+-- Sortie sur sortie: ok
extern node clock3(u: bool) returns (x: bool; y: bool when x);
--- Entree sur entree et sortie sur sortie
+-- Entree sur entree et sortie sur sortie: ok
extern node clock4(u: bool; v: bool when u) returns (x: bool; y: bool when x);
--- Noeud principale.
+-- Noeud principal.
node clock(a: bool; b: bool) returns (c: bool; d: bool when c);
var
z: bool;
@@ -18,7 +18,7 @@ var
let
-- c = clock2(a, (b or b) when a) or (true->a);
-- d = clock2(a, b when a) when c;
- y = clock2(a, b when a) when x;
- (z, x) = clock3(z);
- (c, d) = clock4(a, b when a);
+ y = clock2(a, b when a) when x; -- ok
+ (z, x) = clock3(z);-- ok
+ (c, d) = clock4(a, b when c); -- a la place de clock4(a, b when c)
tel
diff --git a/src/test/should_fail/semantics/bad_call03.lus b/src/test/should_fail/semantics/bad_call03.lus
index d4b59319..c8a5e8a9 100644
--- a/src/test/should_fail/semantics/bad_call03.lus
+++ b/src/test/should_fail/semantics/bad_call03.lus
@@ -11,5 +11,5 @@ node bad_call03(a,b:int^3; c,d:real^3) returns (x : int^3; y:real^3);
let
x = toto(a,b);
- y = titi(c,d);
+ y = toto(c,d);
tel
diff --git a/src/test/test.res.exp b/src/test/test.res.exp
index dc5fbb46..6ae23879 100644
--- a/src/test/test.res.exp
+++ b/src/test/test.res.exp
@@ -3835,6 +3835,38 @@ let
tel
-- end of node call07__call07
+----------------------------------------------------------------------
+====> ../lus2lic -vl 2 --compile-all-items should_work/clock/clock.lus
+Opening file /home/jahier/lus2lic/src/test/should_work/clock/clock.lus
+extern node clock__clock3(u:bool) returns (toto:bool; y:bool when toto);
+
+extern node clock__clock4(
+ u:bool;
+ v:bool when u)
+returns (
+ x:bool;
+ y:bool when x);
+
+extern node clock__clock5(
+ x:bool;
+ y:bool when x;
+ z:bool when y when x)
+returns (
+ a:bool);
+node clock__clock(a:bool; b:bool) returns (c:bool; d:bool when c);
+var
+ z:bool;
+ x:bool when z;
+ y:bool when x when z;
+ e:bool when b;
+let
+ (z, x) = clock__clock3(z);
+ (c, d) = clock__clock4(a, b when a);
+ z = clock__clock5(a, b when a, e when b when a);
+tel
+-- end of node clock__clock
+extern node clock__clock2(u:bool; v:bool when u) returns (y:bool);
+
----------------------------------------------------------------------
====> ../lus2lic -vl 2 --compile-all-items should_work/demo/Gyroscope2.lus
Opening file /home/jahier/lus2lic/src/test/should_work/demo/Gyroscope2.lus
@@ -9313,7 +9345,7 @@ var
let
y = clock__clock2(a, b when a) when x;
(z, x) = clock__clock3(z);
- (c, d) = clock__clock4(a, b when a);
+ (c, d) = clock__clock4(a, b when c);
tel
-- end of node clock__clock
@@ -9405,7 +9437,7 @@ returns (
y:real^3);
let
x = bad_call03__toto(a, b);
- y = bad_call03__titi(c, d);
+ y = bad_call03__toto(c, d);
tel
-- end of node bad_call03__bad_call03
--
GitLab