diff --git a/src/Makefile b/src/Makefile
index 123d42f8ce42276d3fb695e7a5edf60224cd891b..76206e39745509ee68c1e3efd34b80a3515e3532 100644
--- a/src/Makefile
+++ b/src/Makefile
@@ -38,8 +38,12 @@ SOURCES = \
./unify.ml \
./syntaxTab.mli \
./syntaxTab.ml \
- ./predefSemantics.mli \
- ./predefSemantics.ml \
+ ./predefEvalClock.mli \
+ ./predefEvalType.mli \
+ ./predefEvalType.ml \
+ ./predefEvalClock.ml \
+ ./predefEvalConst.mli \
+ ./predefEvalConst.ml \
./evalConst.mli \
./evalConst.ml \
./evalType.mli \
diff --git a/src/TODO b/src/TODO
index f095bf871b00efab9f46fb5a382ff56d32680593..56629a88a3ee5a3e4bad6a265572327568c95960 100644
--- a/src/TODO
+++ b/src/TODO
@@ -58,8 +58,21 @@ les operateurs aritmetiques, bof.
pour bien peu...).
* maintenant que je peux definir des trucs du genre
- x = map<<+;3>>
+ x = map<<+;3>>
ai-je encore besoin de Lustre::plus et consort ???
+ bien que
+ Not = not;
+ ne fonctionne pas (bien que ca doit pouvoir)
+
+ D'autant que je peux fournir le fichier src/lustre.lus aux gens...
+ si vraiment ils veulent une version prefixe de ces operateurs...
+
+ En effet, ca reduit l'espace de nommage (j'avais d'ailleurs dans
+ mes tests de non-reg une variable qui s'appelait "plus", que j'ai
+ du renommer en "Plus"...). Il faudrait d'ailleurs, si je garde ce
+ module Lustre prédefini, que je verifie que l'utilisateur n'essaie
+ pas d'en créer un avec ce nom...
+
* au sujet des pragma:
ex : %ASSUME:assumeSelectElementOfRank_inArray_%
@@ -75,7 +88,8 @@ les operateurs aritmetiques, bof.
***********************************************************************************
*** questions pour bibi
-* essayer de faire qque chose pour les 2 verrues dans predefSemantics
+* Faire qque chose pour les 2 verrues dans predefSemantics
+ pas facile...
* splitter predefsemantics en predefTyping et PredefEval?
les function type_error des predefSemantics devraient être
@@ -105,6 +119,10 @@ n'est pas le cas pour l'instant...
* traiter les types int, real, bool dans Predef ?
+
+* un noeud sans memoire pourra etre déclaré comme "node" ou comme
+"function" que si l'option -v4-compat est donnée ?
+
***********************************************************************************
***********************************************************************************
***********************************************************************************
@@ -113,8 +131,15 @@ n'est pas le cas pour l'instant...
*** facile
+* mettre les operateurs temporels dans Predef ???
+
* Verifier que les fonctions sont des fonctions etc.
+* verifier qu'il n'est pas nécessaire de verifier que le gens ne
+ nomme pas leur package Lustre...
+
+* splitter presefSemantics en predefType, predefClock, et predefEval
+
* Encapsuler le module Global.
*** moins facile
@@ -229,9 +254,6 @@ L'id
- memoryfull (i.e., ils utilisent de la mémoire)
-on pourra rajouter l'alias
- function == extern memoryless node
-pour la compatibilité ascendente
bon, non en fait, il n'y a pas besoin de rajouter tous ces mots clefs.
o memoryless -> function, qui existe deja
@@ -253,8 +275,4 @@ nb2 : rejeter les noeuds sans memoire (ce faisant sans indiquer
alors rajouter l'option --infer-memoryless-annotation). Ou alors, on
se contente d'emmettre des warning.
-nb3 : function = memoryless node
-
-
-
\ No newline at end of file
diff --git a/src/evalConst.ml b/src/evalConst.ml
index e0f034c34a74a69c3a039ddf3fd7de2b3bc003fe..b9b77e4320b654f9a131b96f4e5d0cb20b90b9a0 100644
--- a/src/evalConst.ml
+++ b/src/evalConst.ml
@@ -1,4 +1,4 @@
-(** Time-stamp: <modified the 29/05/2008 (at 11:10) by Erwan Jahier> *)
+(** Time-stamp: <modified the 05/06/2008 (at 10:43) by Erwan Jahier> *)
open Printf
@@ -8,7 +8,8 @@ open SyntaxTree
open SyntaxTreeCore
open CompiledData
open Predef
-open PredefSemantics
+open PredefEvalConst
+open PredefEvalType
(*----------------------------------------------------
EvalArray_error :
@@ -319,7 +320,7 @@ let rec f
->
if sargs = [] then
let effargs = (List.map rec_eval_const args) in
- PredefSemantics.const_eval op lxm [] effargs
+ PredefEvalConst.f op lxm [] effargs
else
(* Well, it migth be possible after all... TODO *)
not_evaluable_construct (op2string op)
diff --git a/src/evalType.ml b/src/evalType.ml
index 969630561dc404038cb550069e82f839bb43a489..410092c35aa3c520bb41e6c186fb5921009d020c 100644
--- a/src/evalType.ml
+++ b/src/evalType.ml
@@ -2,7 +2,8 @@
open Predef
-open PredefSemantics
+open PredefEvalType
+open PredefEvalConst
open SyntaxTree
open SyntaxTreeCore
open CompiledData
@@ -29,7 +30,7 @@ and (eval_by_pos_type :
fun id_solver posop lxm args ->
match posop with
| Predef_eff (op,sargs) ->
- PredefSemantics.type_eval op lxm sargs (List.map (f id_solver) args)
+ PredefEvalType.f op lxm sargs (List.map (f id_solver) args)
| CALL_eff node_exp_eff ->
let lto = snd (List.split node_exp_eff.it.outlist_eff) in
diff --git a/src/getEff.ml b/src/getEff.ml
index a6fce3dcc4cb40c58df287600fcea27a29d0836a..ffadee5cab245ebc137e19dd50eb2fd07a088c6a 100644
--- a/src/getEff.ml
+++ b/src/getEff.ml
@@ -1,4 +1,4 @@
-(** Time-stamp: <modified the 02/06/2008 (at 14:16) by Erwan Jahier> *)
+(** Time-stamp: <modified the 05/06/2008 (at 10:45) by Erwan Jahier> *)
open Lxm
@@ -102,7 +102,7 @@ and (check_static_arg : CompiledData.id_solver ->
let sargs_eff =
translate_predef_static_args node_id_solver sargs sa.src
in
- let opeff = PredefSemantics.make_node_exp_eff op sa.src sargs_eff in
+ let opeff = PredefEvalType.make_node_exp_eff op sa.src sargs_eff in
NodeStaticArgEff (id, opeff)
| StaticArgNode(
@@ -253,7 +253,7 @@ and get_node id_solver node_or_node_ident lxm =
| StaticArgNode(CALL_n ne) -> node id_solver ne
| StaticArgNode(Predef (op,sargs)) ->
let sargs_eff = translate_predef_static_args id_solver sargs lxm in
- PredefSemantics.make_node_exp_eff op lxm sargs_eff
+ PredefEvalType.make_node_exp_eff op lxm sargs_eff
| StaticArgNode(_) -> assert false
| StaticArgType _
diff --git a/src/lazyCompiler.ml b/src/lazyCompiler.ml
index e9d7c54bd5f224b66437dc6ed282962d1a8104e1..dc4e95f25d3e08ff478ab7fe2894b2f38012390d 100644
--- a/src/lazyCompiler.ml
+++ b/src/lazyCompiler.ml
@@ -1,4 +1,4 @@
-(** Time-stamp: <modified the 03/06/2008 (at 15:03) by Erwan Jahier> *)
+(** Time-stamp: <modified the 05/06/2008 (at 10:45) by Erwan Jahier> *)
open Lxm
@@ -684,7 +684,7 @@ and (node_check_do: t -> CompiledData.node_key -> Lxm.t -> SymbolTab.t ->
let sargs_eff =
GetEff.translate_predef_static_args node_id_solver sargs lxm
in
- PredefSemantics.make_node_exp_eff predef_op lxm sargs_eff
+ PredefEvalType.make_node_exp_eff predef_op lxm sargs_eff
| CALL_n(node_alias) ->
GetEff.node node_id_solver node_alias
diff --git a/src/lustre.lus b/src/lustre.lus
index 69449fce6b0643a3cb3d004eee7e06d2d38ab32c..7ba864038f67b5245e8d7e9dda0770a233615c79 100644
--- a/src/lustre.lus
+++ b/src/lustre.lus
@@ -1,63 +1,53 @@
--- This package is very useful to get prefix version of predefined infix operators
--- e.g., in order to use those in array iterators.
+-- This package provides prefix version of predefined infix operators
--
--- for prefix operators, it is still useful in order to be able to use them
--- as node aliases.
--
--- nb : note we did not define polymorphic operators here, as we have no
--- polymorphic node in lustre.
+-- nb : note we did not define polymorphic operators here (e.g., '>'),
+-- as we cannot define polymorphic nodes in lustre.
package Lustre
provides
- node Not(x: bool) returns (z: bool);
- node And(x, y: bool) returns (z: bool);
- node Or(x, y: bool) returns (z: bool);
- node Xor(x, y: bool) returns (z: bool);
- node Impl(x, y: bool) returns (z: bool);
-
- node Div(x, y: int) returns (z: int);
- node Mod(x, y: int) returns (z: int);
- node Iplus(x, y: int) returns (z: int);
- node Iminus(x, y: int) returns (z: int);
- node Itimes(x, y: int) returns (z: int);
- node Islash(x, y: int) returns (z: int);
- node Iuminus(x: int) returns (z: int);
-
- node Rplus(x, y: real) returns (z: real);
- node Rminus(x, y: real) returns (z: real);
- node Rtimes(x, y: real) returns (z: real);
- node Rslash(x, y: real) returns (z: real);
- node Ruminus(x: real) returns (z: real);
-
- node Real2int(x: real) returns (z: int);
- node Int2real(x: int) returns (z: real);
-
+ function And(x, y: bool) returns (z: bool);
+ function Or(x, y: bool) returns (z: bool);
+ function Xor(x, y: bool) returns (z: bool);
+ function Impl(x, y: bool) returns (z: bool);
+
+ function Div(x, y: int) returns (z: int);
+ function Mod(x, y: int) returns (z: int);
+ function Iplus(x, y: int) returns (z: int);
+ function Iminus(x, y: int) returns (z: int);
+ function Itimes(x, y: int) returns (z: int);
+ function Islash(x, y: int) returns (z: int);
+ function Iuminus(x: int) returns (z: int);
+
+ function Rplus(x, y: real) returns (z: real);
+ function Rminus(x, y: real) returns (z: real);
+ function Rtimes(x, y: real) returns (z: real);
+ function Rslash(x, y: real) returns (z: real);
+ function Ruminus(x: real) returns (z: real);
body
- node Not(x: bool) returns (z: bool); let z = not x; tel
- node And(x, y: bool) returns (z: bool); let z = x and y; tel
- node Or(x, y: bool) returns (z: bool); let z = x or y; tel
- node Xor(x, y: bool) returns (z: bool); let z = x xor y; tel
- node Impl(x, y: bool) returns (z: bool); let z = x => y; tel
+
+ function And = Lustre::and;
+ function Or(x, y: bool) returns (z: bool); let z = x or y; tel
+ function Xor(x, y: bool) returns (z: bool); let z = x xor y; tel
+ function Impl(x, y: bool) returns (z: bool); let z = x => y; tel
- node Div(x, y: int) returns (z: int); let z = x div y; tel
- node Mod(x, y: int) returns (z: int); let z = x mod y; tel
- node Iplus(x, y: int) returns (z: int); let z = x + y; tel
- node Iminus(x, y: int) returns (z: int); let z = x - y; tel
- node Itimes(x, y: int) returns (z: int); let z = x * y; tel
- node Islash(x, y: int) returns (z: int); let z = x / y; tel
- node Iuminus(x: int) returns (z: int); let z = -x; tel
+ function Div(x, y: int) returns (z: int); let z = x div y; tel
+ function Mod(x, y: int) returns (z: int); let z = x mod y; tel
+ function Iplus(x, y: int) returns (z: int); let z = x + y; tel
+ function Iminus(x, y: int) returns (z: int); let z = x - y; tel
+ function Itimes(x, y: int) returns (z: int); let z = x * y; tel
+ function Islash(x, y: int) returns (z: int); let z = x / y; tel
+ function Iuminus(x: int) returns (z: int); let z = -x; tel
- node Rplus(x, y: real) returns (z: real); let z = x + y; tel
- node Rminus(x, y: real) returns (z: real); let z = x - y; tel
- node Rtimes(x, y: real) returns (z: real); let z = x * y; tel
- node Rslash(x, y: real) returns (z: real); let z = x / y; tel
- node Ruminus(x: real) returns (z: real); let z = -x; tel
+ function Rplus(x, y: real) returns (z: real); let z = x + y; tel
+ function Rminus(x, y: real) returns (z: real); let z = x - y; tel
+ function Rtimes(x, y: real) returns (z: real); let z = x * y; tel
+ function Rslash(x, y: real) returns (z: real); let z = x / y; tel
+ function Ruminus(x: real) returns (z: real); let z = -x; tel
- node Real2int(x: real) returns (z: int); let z = real2int(x); tel
- node Int2real(x: int) returns (z: real); let z = int2real(x); tel
end
diff --git a/src/predef.ml b/src/predef.ml
index 6da2196920a1a6e590b9ca3abefe751f96954cf6..ab5f564f2c4cef38f2b1d3faa7efd426de432ac9 100644
--- a/src/predef.ml
+++ b/src/predef.ml
@@ -169,6 +169,11 @@ let (string_to_op : string -> op) =
| _ -> raise Not_found
+(** An evaluator returns a list because Lustre calls returns tuples.
+
+ SE: migth raise some check error!
+*)
+type 'a evaluator = 'a list list -> 'a list
(*********************************************************************************)
(* Automatically generate the latex documentation associated to predefined
diff --git a/src/predefEvalClock.ml b/src/predefEvalClock.ml
new file mode 100644
index 0000000000000000000000000000000000000000..78270764bb00370e75bb21e81f17a2e1b1b8eb01
--- /dev/null
+++ b/src/predefEvalClock.ml
@@ -0,0 +1,28 @@
+(** Time-stamp: <modified the 26/05/2008 (at 14:57) by Erwan Jahier> *)
+
+open Predef
+open CompiledData
+
+let finish_me msg = print_string ("\n\tXXX predefSemantics.ml:"^msg^" -> finish me!\n")
+
+type clocker = CompiledData.clock_eff Predef.evaluator
+
+let (aa_clocker: clocker) =
+ function
+ | [clk1] -> clk1
+ | _ -> finish_me "a good error msg"; assert false
+
+let (aaa_clocker: clocker) =
+ function
+ | [clk1; clk2] ->
+ if clk1 = clk2 then clk1 else (finish_me "a good error msg"; assert false)
+ | _ ->
+ finish_me "a good error msg"; assert false
+
+
+
+(* This table contains the clock profile of predefined operators *)
+let (clocking_tab: op -> clocker) =
+ fun op ->
+ assert false
+
diff --git a/src/predefEvalClock.mli b/src/predefEvalClock.mli
new file mode 100644
index 0000000000000000000000000000000000000000..947d39c55b187bdd53ee57dae82e1acb53108b68
--- /dev/null
+++ b/src/predefEvalClock.mli
@@ -0,0 +1,3 @@
+(** Time-stamp: <modified the 26/05/2008 (at 14:57) by Erwan Jahier> *)
+
+type clocker = CompiledData.clock_eff Predef.evaluator
diff --git a/src/predefEvalConst.ml b/src/predefEvalConst.ml
new file mode 100644
index 0000000000000000000000000000000000000000..8ccfe3122fdb82a48212422f3235e7065b5f2b85
--- /dev/null
+++ b/src/predefEvalConst.ml
@@ -0,0 +1,242 @@
+(** Time-stamp: <modified the 26/05/2008 (at 14:57) by Erwan Jahier> *)
+
+open Predef
+open SyntaxTreeCore
+open CompiledData
+(* open Lxm *)
+(* open Errors *)
+
+type const_evaluator = const_eff evaluator
+
+exception EvalConst_error of string
+
+(* exported *)
+let (type_error_const : const_eff list -> string -> 'a) =
+ fun v expect ->
+ raise (EvalConst_error(
+ "type mismatch "^(if expect = "" then "" else (expect^" expected"))))
+
+
+let (arity_error_const : const_eff list -> string -> 'a) =
+ fun v expect ->
+ raise (EvalConst_error(
+ Printf.sprintf "\n*** arity error: %d argument%s, whereas %s were expected"
+ (List.length v) (if List.length v>1 then "s" else "") expect))
+
+
+let (bbb_evaluator:(bool -> bool -> bool) -> const_evaluator) =
+ fun op -> fun ll -> match List.flatten ll with
+ | [Bool_const_eff v0; Bool_const_eff v1] -> [Bool_const_eff (op v0 v1)]
+ | _ -> assert false (* should not occur because eval_type is called before *)
+
+let (ooo_evaluator:(int -> int -> int) -> (float -> float -> float) ->
+ const_evaluator) =
+ fun opi opr -> fun ll -> match List.flatten ll with
+ | [Int_const_eff v0; Int_const_eff v1] -> [Int_const_eff (opi v0 v1)]
+ | [Real_const_eff v0; Real_const_eff v1] -> [Real_const_eff (opr v0 v1)]
+ (* XXX should we evaluate reals ??? *)
+ | _ -> assert false (* should not occur because eval_type is called before *)
+
+let (iii_evaluator:(int -> int -> int) -> const_evaluator) =
+ fun op -> fun ll -> match List.flatten ll with
+ | [Int_const_eff v0; Int_const_eff v1] -> [Int_const_eff (op v0 v1)]
+ | _ -> assert false (* should not occur because eval_type is called before *)
+
+let (aab_evaluator:('a -> 'a -> bool) -> const_evaluator) =
+ fun op -> fun ll -> match List.flatten ll with
+ | [v0; v1] -> [Bool_const_eff (op v0 v1)]
+ | _ -> assert false (* should not occur because eval_type is called before *)
+
+let (fff_evaluator:(float -> float -> float) -> const_evaluator) =
+ fun op -> fun ll -> match List.flatten ll with
+ | [Real_const_eff v0; Real_const_eff v1] -> [Real_const_eff (op v0 v1)]
+ | _ -> assert false (* should not occur because eval_type is called before *)
+
+let (bb_evaluator:(bool -> bool) -> const_evaluator) =
+ fun op -> fun ll -> match List.flatten ll with
+ | [Bool_const_eff v0] -> [Bool_const_eff (op v0)]
+ | _ -> assert false (* should not occur because eval_type is called before *)
+
+let (ii_evaluator:(int -> int) -> const_evaluator) =
+ fun op -> fun ll -> match List.flatten ll with
+ | [Int_const_eff v0] -> [Int_const_eff (op v0)]
+ | _ -> assert false (* should not occur because eval_type is called before *)
+
+let (ff_evaluator:(float -> float) -> const_evaluator) =
+ fun op -> fun ll -> match List.flatten ll with
+ | [Real_const_eff v0] -> [Real_const_eff (op v0)]
+ | _ -> assert false (* should not occur because eval_type is called before *)
+
+let (oo_evaluator:(int -> int) -> (float -> float) -> const_evaluator) =
+ fun opi opr -> fun ll -> match List.flatten ll with
+ | [Int_const_eff v0] -> [Int_const_eff (opi v0)]
+ | [Real_const_eff v0] -> [Real_const_eff (opr v0)]
+ (* XXX should we evaluate reals ??? *)
+ | _ -> assert false (* should not occur because eval_type is called before *)
+
+let (sf_evaluator: Ident.t -> const_evaluator) =
+ fun id ceff_ll ->
+ try let v = float_of_string (Ident.to_string id) in
+ [Real_const_eff v]
+ with Failure "float_of_string" ->
+ raise (EvalConst_error(
+ Printf.sprintf "\n*** fail to convert the string \"%s\" into a float"
+ (Ident.to_string id)))
+
+let (si_evaluator: Ident.t -> const_evaluator) =
+ fun id ceff_ll ->
+ try let v = int_of_string (Ident.to_string id) in
+ [Int_const_eff v]
+ with Failure "int_of_string" ->
+ raise (EvalConst_error(
+ Printf.sprintf "\n*** fail to convert the string \"%s\" into an int"
+ (Ident.to_string id)))
+
+let (sb_evaluator: bool -> const_evaluator) =
+ fun v ceff_ll ->
+ [Bool_const_eff v]
+
+let (fi_evaluator:(float -> int) -> const_evaluator) =
+ fun op -> fun ll -> match List.flatten ll with
+ | [Real_const_eff v0] -> [Int_const_eff (op v0)]
+ | _ -> assert false (* should not occur because [eval_type] is called before *)
+
+let (if_evaluator: (int -> float) -> const_evaluator) =
+ fun op -> fun ll -> match List.flatten ll with
+ | [Int_const_eff v0] -> [Real_const_eff (op v0)]
+ | _ -> assert false (* should not occur because [eval_type] is called before *)
+
+let (ite_evaluator : const_evaluator) =
+ function
+ | [[Bool_const_eff c]; t; e] -> if c then t else e
+ | _ -> assert false (* should not occur because [eval_type] is called before *)
+
+let (boolred_evaluator : int -> const_evaluator) =
+ fun max ceff_ll ->
+ let nb = List.fold_left
+ (fun acc -> function
+ | (Bool_const_eff b) -> if b then acc+1 else acc | _ -> assert false)
+ 0
+ (List.flatten ceff_ll)
+ in
+ [Bool_const_eff (nb <= max)]
+
+
+(* exported *)
+let (f: op -> Lxm.t -> static_arg_eff list -> const_evaluator) =
+ fun op lxm sargs ll ->
+ (* we first check the type so that we do not need to check it during the const
+ evaluation *)
+ ignore (PredefEvalType.f op lxm sargs (List.map (List.map type_of_const_eff) ll));
+ match op with
+ | TRUE_n -> sb_evaluator true ll
+ | FALSE_n -> sb_evaluator false ll
+ | ICONST_n id -> si_evaluator id ll
+ | RCONST_n id -> sf_evaluator id ll
+ | NOT_n -> bb_evaluator (not) ll
+ | REAL2INT_n -> fi_evaluator int_of_float ll
+ | INT2REAL_n -> if_evaluator float_of_int ll
+ | AND_n -> bbb_evaluator (&&) ll
+ | OR_n -> bbb_evaluator (||) ll
+ | XOR_n -> bbb_evaluator (<>) ll
+ | IMPL_n -> bbb_evaluator (fun a b -> (not a) || b) ll
+ | EQ_n -> aab_evaluator (=) ll
+ | NEQ_n -> aab_evaluator (<>) ll
+ | LT_n -> aab_evaluator (<) ll
+ | LTE_n -> aab_evaluator (<=) ll
+ | GT_n -> aab_evaluator (>) ll
+ | GTE_n -> aab_evaluator (>=) ll
+ | DIV_n -> iii_evaluator (/) ll
+ | MOD_n -> iii_evaluator (mod) ll
+ | IF_n -> ite_evaluator ll
+ | UMINUS_n -> oo_evaluator (fun x -> -x) (fun x -> -.x) ll
+ | MINUS_n -> ooo_evaluator (-) (-.) ll
+ | PLUS_n -> ooo_evaluator (+) (+.) ll
+ | SLASH_n -> ooo_evaluator (/) (/.) ll
+ | TIMES_n -> ooo_evaluator ( * ) ( *.) ll
+ | IUMINUS_n -> ii_evaluator (fun x -> -x) ll
+ | IMINUS_n -> iii_evaluator (-) ll
+ | IPLUS_n -> iii_evaluator (+) ll
+ | ISLASH_n -> iii_evaluator (/) ll
+ | ITIMES_n -> iii_evaluator ( * ) ll
+ | RUMINUS_n -> ff_evaluator (fun x -> -.x) ll
+ | RMINUS_n -> fff_evaluator (-.) ll
+ | RPLUS_n -> fff_evaluator (+.) ll
+ | RSLASH_n -> fff_evaluator (/.) ll
+ | RTIMES_n -> fff_evaluator ( *.) ll
+ | NOR_n -> boolred_evaluator 0 ll
+ | DIESE_n -> boolred_evaluator 1 ll
+ | Map -> assert false
+ | Fill -> assert false
+ | Red -> assert false
+ | FillRed -> assert false
+ | BoolRed -> boolred_evaluator 1 ll
+
+(*********************************************************************************)
+(*********************************************************************************)
+(*
+pour evaluer l'égalité, Pascal faisait comme ca (j'ai été plus (trop ?) brutal) :
+ (*----------------------------
+ Calcul de l'égalité
+ N.B. Sur les constantes abstraites
+ on est très méfiant
+ N.B. Sur les types structure,
+ on fait des appels récursifs
+ ----------------------------*)
+ let rec compute_eq
+ (args : const_eff list)
+ = (
+ let rec fields_eq f0 f1 = (
+ match (f0, f1) with
+ | ([], []) ->
+ [Bool_const_eff true]
+
+ | ((f0,h0)::t0, (f1,h1)::t1) -> (
+ assert (f0 = f1);
+ match (compute_eq [h0;h1]) with
+ [Bool_const_eff false] -> [Bool_const_eff false]
+ | [Bool_const_eff true] -> (fields_eq t0 t1)
+ | _ -> assert false
+ )
+ | _ -> assert false
+ )
+ in
+ match args with
+ [Bool_const_eff v0; Bool_const_eff v1] -> [Bool_const_eff (v0 = v1)]
+ | [Int_const_eff v0; Int_const_eff v1] -> [Bool_const_eff (v0 = v1)]
+ | [Real_const_eff v0; Real_const_eff v1] -> (
+ let res = (v0 = v1) in
+ warning src
+ (sprintf "float in static exp: %f=%f evaluated as %b" v0 v1 res);
+ [Bool_const_eff res]
+ )
+ (*
+ 2007-07 obsolete
+
+ | [Extern_const_eff (v0, t0); Extern_const_eff (v1, t1)] -> (
+ if (t0 <> t1) then (
+ type_error args "t*t for some type t"
+ ) else if (v0 <> v1) then (
+ uneval_error args (
+ sprintf "%s=%s (external constants)"
+ (string_of_fullid v0)
+ (string_of_fullid v1)
+ )
+ ) else (
+ [Bool_const_eff true]
+ )
+ )
+ *)
+ | [Enum_const_eff (v0, t0); Enum_const_eff (v1, t1)] -> (
+ if (t0 = t1) then [Bool_const_eff (v0 = v1)]
+ else type_error args "t*t for some type t"
+ )
+ | [Struct_const_eff (f0, t0); Struct_const_eff (f1, t1)] -> (
+ if (t0 = t1) then (fields_eq f0 f1)
+ else type_error args "t*t for some type t"
+ )
+ | [x;y] -> type_error args "t*t for some type t"
+ | x -> arity_error args "2"
+ )
+ in
+ *)
diff --git a/src/predefEvalConst.mli b/src/predefEvalConst.mli
new file mode 100644
index 0000000000000000000000000000000000000000..8ed8ea8e065f71027bd8c4b58d61e5b6bc970b58
--- /dev/null
+++ b/src/predefEvalConst.mli
@@ -0,0 +1,16 @@
+(** Time-stamp: <modified the 26/05/2008 (at 14:57) by Erwan Jahier> *)
+open Predef
+open SyntaxTreeCore
+open CompiledData
+
+exception EvalConst_error of string
+
+val type_error_const : const_eff list -> string -> 'a
+val arity_error_const : const_eff list -> string -> 'a
+
+type const_evaluator = const_eff evaluator
+
+(* That function says how to statically evaluate constants *)
+val f:
+ Predef.op -> Lxm.t -> CompiledData.static_arg_eff list -> const_evaluator
+
diff --git a/src/predefEvalType.ml b/src/predefEvalType.ml
new file mode 100644
index 0000000000000000000000000000000000000000..f155c33e07b1af921e590dcc9fa7dc6a114c6983
--- /dev/null
+++ b/src/predefEvalType.ml
@@ -0,0 +1,279 @@
+(** Time-stamp: <modified the 05/06/2008 (at 10:42) by Erwan Jahier> *)
+
+open Predef
+open SyntaxTreeCore
+open CompiledData
+open Lxm
+open Errors
+open Unify
+
+
+(* exported *)
+type typer = type_eff Predef.evaluator
+
+exception EvalType_error of string
+
+
+let (type_error : type_eff list -> string -> 'a) =
+ fun tel expect ->
+ let str_l = List.map CompiledDataDump.string_of_type_eff tel in
+ let str_provided = String.concat "*" str_l in
+ raise (EvalType_error(
+ ("\n*** type '" ^ str_provided ^ "' was provided" ^
+ (if expect = "" then ""
+ else (" whereas\n*** type '" ^expect^"' was expected")))))
+
+let (type_error2 : string -> string -> string -> 'a) =
+ fun provided expect msg ->
+ raise (EvalType_error(
+ ("\n*** type '" ^ provided ^ "' was provided" ^
+ (if expect = "" then ""
+ else (" whereas\n*** type '" ^expect^"' was expected")) ^
+ (if msg = "" then "" else ("\n*** " ^ msg)))))
+
+let (arity_error : 'a list -> string -> 'b) =
+ fun v expect ->
+ raise (EvalType_error(
+ Printf.sprintf "\n*** arity error: %d argument%s, whereas %s were expected"
+ (List.length v) (if List.length v>1 then "s" else "") expect))
+
+(*********************************************************************************)
+(* a few local alias to make the node profile below more readable. *)
+let i = Int_type_eff_ext
+let r = Real_type_eff_ext
+let b = Bool_type_eff_ext
+let id str = Ident.of_string str
+
+(** A few useful type profiles for simple operators *)
+let bb_profile = [(id "i", b)], [(id "o", b)] (* bool -> bool *)
+let bbb_profile = [(id "i1", b);(id "i2", b)], [(id "o", b)] (* bool*bool -> bool *)
+let ii_profile = [(id "i", i)], [(id "o", i)] (* int -> int *)
+let iii_profile = [(id "i1", i);(id "i2", i)], [(id "o", i)] (* int*int -> int *)
+let rr_profile = [(id "i", r)], [(id "o", r)] (* real -> real *)
+let rrr_profile = [(id "i1", r);(id "i2", r)], [(id "o", r)] (* real*real -> real *)
+let ri_profile = [id "i", r], [id "o", i] (* real -> int *)
+let ir_profile = [id "i", i], [id "o", r] (* int -> real *)
+
+(** Constant profiles *)
+let b_profile = [],[id "o", b]
+let i_profile = [],[id "o", i]
+let r_profile = [],[id "o", r]
+
+(** polymorphic operator profiles *)
+let aab_profile = [(id "i1",Any);(id "i2",Any)], [(id "o", b)] (* 'a -> 'a -> bool*)
+let baaa_profile = [(id "c", b);(id "b1",Any);(id "b2",Any)], [(id "o",Any)]
+ (* for if-then-else *)
+
+(** overloaded operator profiles *)
+let oo_profile = [(id "i",Overload)], [(id "o",Overload)]
+let ooo_profile = [(id "i1",Overload);(id "i2",Overload)], [(id "o",Overload)]
+
+(** iterators profiles *)
+(* [type_to_array_type [x1;...;xn] c] returns the array type [x1^c;...;xn^c] *)
+let (type_to_array_type:
+ (Ident.t * type_eff_ext) list -> int -> (Ident.t * type_eff_ext) list) =
+ fun l c ->
+ List.map (fun (id, teff) -> id, Array_type_eff_ext(teff,c)) l
+
+(* Extract the node and the constant from a list of static args *)
+let (get_node_and_constant:static_arg_eff list -> node_exp_eff * int)=
+ fun sargs ->
+ match sargs with
+ | [NodeStaticArgEff(_,n);ConstStaticArgEff(_,Int_const_eff c)] -> n,c
+ | _ -> assert false
+
+
+let map_profile =
+ (* Given
+ - a node n of type: tau_1 * ... * tau_n -> teta_1 * ... * teta_l
+ - a constant c (nb : sargs = [n,c])
+
+ The profile of map is: tau_1^c * ... * tau_n^c -> teta_1^c * ... * teta_l^c
+ *)
+ fun lxm sargs ->
+ let (n,c) = get_node_and_constant sargs in
+ let lti = type_to_array_type n.inlist_eff c in
+ let lto = type_to_array_type n.outlist_eff c in
+ (lti, lto)
+
+
+let fillred_profile =
+ (* Given
+ - a node n of type tau * tau_1 * ... * tau_n -> tau * teta_1 * ... * teta_l
+ - a constant c (nb : sargs = [n,c])
+
+ returns the profile:
+ tau * tau_1^c * ... * tau_n^c -> tau * teta_1^c * ... * teta_l^c
+ *)
+ fun lxm sargs ->
+ let (n,c) = get_node_and_constant sargs in
+ let _ = assert(n.inlist_eff <> [] && n.outlist_eff <> []) in
+ let lti = (List.hd n.inlist_eff)::type_to_array_type (List.tl n.inlist_eff) c in
+ let lto = (List.hd n.outlist_eff)::type_to_array_type (List.tl n.outlist_eff) c in
+ let (id1, t1) = List.hd lti and (id2, t2) = List.hd lto in
+ if t1 = t2 then (lti,lto) else
+ (* if they are not equal, they migth be unifiable *)
+ match Unify.f [t1] [t2] with
+ | Equal -> (lti,lto)
+ | Unif t -> (List.map (fun (id,tid) -> id, subst_type_ext t tid) lti,
+ List.map (fun (id,tid) -> id, subst_type_ext t tid) lto)
+ | Ko(msg) -> raise (Compile_error(lxm, msg))
+
+
+(* let fill_profile = fillred_profile *)
+ (* Given
+ - a node N of type tau -> tau * teta_1 * ... * teta_l
+ - a constant c (nb : sargs = [N,c])
+ returns the profile: [tau -> tau * teta_1^c * ... * teta_l^c]
+ *)
+
+(* let red_profile = fillpred_profile *)
+ (* Given
+ - a node N of type tau * tau_1 * ... * tau_n -> tau
+ - a constant c (nb : sargs = [N,c])
+ returns the profile tau * tau_1^c * ... * tau_n^c -> tau
+ *)
+
+
+(* Given
+ - 3 integer constant i, j, k
+
+ returns the profile bool^k -> bool
+*)
+let boolred_profile =
+ fun lxm sargs ->
+ let (get_three_constants: Lxm.t -> static_arg_eff list -> int * int * int) =
+ fun lxm sargs ->
+ match sargs with
+ | [ConstStaticArgEff(_,Int_const_eff i);
+ ConstStaticArgEff(_,Int_const_eff j);
+ ConstStaticArgEff(_,Int_const_eff k)] -> i,j,k
+ | _ -> raise (Compile_error(lxm, "\n*** type error: 3 int were expected"))
+ in
+ let (_i,_j,k) = get_three_constants lxm sargs in
+ [id "i", (Array_type_eff_ext(Bool_type_eff_ext,k))], [id "o", b]
+
+
+type node_profile = (Ident.t * type_eff_ext) list * (Ident.t * type_eff_ext) list
+
+let (op2profile : Predef.op -> Lxm.t -> static_arg_eff list -> node_profile) =
+ fun op lxm sargs -> match op with
+ | TRUE_n | FALSE_n -> b_profile
+ | ICONST_n id -> i_profile
+ | RCONST_n id -> r_profile
+ | NOT_n -> bb_profile
+ | REAL2INT_n -> ri_profile
+ | INT2REAL_n -> ir_profile
+ | IF_n -> baaa_profile
+ | UMINUS_n -> oo_profile
+ | IUMINUS_n -> ii_profile
+ | RUMINUS_n -> rr_profile
+ | IMPL_n | AND_n | OR_n | XOR_n -> bbb_profile
+ | NEQ_n | EQ_n | LT_n | LTE_n | GT_n | GTE_n -> aab_profile
+ | MINUS_n | PLUS_n | TIMES_n | SLASH_n -> ooo_profile
+ | RMINUS_n | RPLUS_n | RTIMES_n | RSLASH_n -> rrr_profile
+ | DIV_n | MOD_n | IMINUS_n | IPLUS_n | ISLASH_n | ITIMES_n -> iii_profile
+ | Red | Fill | FillRed -> fillred_profile lxm sargs
+ | Map -> map_profile lxm sargs
+ | BoolRed -> boolred_profile lxm sargs
+
+ | NOR_n | DIESE_n -> assert false
+ (* XXX The current representation of node_profile prevent us
+ from being able to represent "bool list" (i.e., operator
+ of variable arity). I could extend the type node_profile,
+ but is it worth the complication just to be able to define
+ alias nodes on "nor" and "#"? Actually, even if I extend
+ this data type, I don'ty know how I could generate an
+ alias node for them anyway...
+ *)
+
+(* exported *)
+let (make_node_exp_eff : op -> Lxm.t -> static_arg_eff list -> node_exp_eff) =
+ fun op lxm sargs ->
+ let id = Ident.make_long
+ (Ident.pack_name_of_string "Lustre") (Ident.of_string (Predef.op2string op))
+ in
+ let (lti,lto) = op2profile op lxm sargs in
+ {
+ node_key_eff = id,sargs ;
+ inlist_eff = lti;
+ outlist_eff = lto;
+ loclist_eff = None;
+ clock_inlist_eff = [];
+ clock_outlist_eff = [];
+ def_eff = ExternEff;
+ has_mem_eff = false;
+ is_safe_eff = true;
+ }
+
+(* exported *)
+let (f : op -> Lxm.t -> CompiledData.static_arg_eff list -> typer) =
+ fun op lxm sargs ll ->
+ match op with
+ | IF_n -> (
+ (* VERRUE 1 *)
+ (* j'arrive pas a traiter le if de facon generique (pour l'instant...)
+ a cause du fait que le if peut renvoyer un tuple.
+ *)
+ match ll with
+ | [[Bool_type_eff]; t; e] ->
+ if t = e then t else
+ (type_error (List.flatten [[Bool_type_eff]; t; e]) "bool*any*any")
+ | x -> (arity_error x "3")
+ )
+ | (NOR_n | DIESE_n) ->
+ (* VERRUE 2 : cf XXX above: therefore i define an ad-hoc
+ check for them. *)
+ let check_nary_iter acc ceff =
+ match ceff with (Bool_type_eff) -> acc | _ -> (type_error [ceff] "bool")
+ in
+ List.fold_left check_nary_iter () (List.flatten ll);
+ [Bool_type_eff]
+ | _ ->
+ (* general case *)
+ let node_eff = make_node_exp_eff op lxm sargs in
+ let lti = List.map (fun (id,t) -> t) node_eff.inlist_eff
+ and lto = List.map (fun (id,t) -> t) node_eff.outlist_eff in
+ let rec (subst_type : type_eff -> type_eff_ext -> type_eff) =
+ fun t teff_ext -> match teff_ext with
+ (* substitutes [t] in [teff_ext] *)
+ | Bool_type_eff_ext -> Bool_type_eff
+ | Int_type_eff_ext -> Int_type_eff
+ | Real_type_eff_ext -> Real_type_eff
+ | External_type_eff_ext l -> External_type_eff l
+ | Enum_type_eff_ext(l,el) -> Enum_type_eff(l,el)
+ | Array_type_eff_ext(teff_ext,i) ->
+ Array_type_eff(subst_type t teff_ext, i)
+ | Struct_type_eff_ext(l, fl) ->
+ Struct_type_eff(
+ l,
+ List.map
+ (fun (id,(teff,copt)) -> (id,(subst_type t teff,copt)))
+ fl)
+ | Any
+ | Overload -> t
+ in
+ let l = List.map type_eff_to_type_eff_ext (List.flatten ll) in
+ if (List.length l <> List.length lti) then
+ arity_error [l] (string_of_int (List.length lti))
+ else
+ match Unify.f lti l with
+ | Equal -> List.map type_eff_ext_to_type_eff lto
+ | Unif Any ->
+ type_error2
+ (CompiledDataDump.type_eff_ext_list_to_string l)
+ (CompiledDataDump.type_eff_ext_list_to_string lti)
+ "could not instanciate polymorphic type"
+ | Unif Overload ->
+ type_error2
+ (CompiledDataDump.type_eff_ext_list_to_string l)
+ (CompiledDataDump.type_eff_ext_list_to_string lti)
+ "could not instanciate overloaded type"
+
+ | Unif t ->
+ List.map (subst_type (type_eff_ext_to_type_eff t)) lto
+
+ | Ko(str) ->
+ type_error2 (CompiledDataDump.type_eff_ext_list_to_string l)
+ (CompiledDataDump.type_eff_ext_list_to_string lti) str
+
diff --git a/src/predefEvalType.mli b/src/predefEvalType.mli
new file mode 100644
index 0000000000000000000000000000000000000000..5aa96a26f76c54cae1ecea3fb5c5129ebde13da5
--- /dev/null
+++ b/src/predefEvalType.mli
@@ -0,0 +1,22 @@
+(** Time-stamp: <modified the 05/06/2008 (at 10:42) by Erwan Jahier> *)
+
+open CompiledData
+
+type typer = type_eff Predef.evaluator
+
+exception EvalType_error of string
+val type_error : type_eff list -> string -> 'a
+val arity_error : 'a list -> string -> 'b
+
+
+(* Provides the type profile of predef operators. More precisely, given an operator
+ and a list of types, This function checks that the provided types are ok, and
+ returns the list of the operator output types.
+*)
+val f : Predef.op -> Lxm.t -> CompiledData.static_arg_eff list -> typer
+
+
+
+val make_node_exp_eff : Predef.op -> Lxm.t -> static_arg_eff list -> node_exp_eff
+
+
diff --git a/src/predefSemantics.ml b/src/predefSemantics.ml
index cac4473e26a53d9a2ff71bbb4ab8714f527ddc4f..e07887a175e87347fa38531849fd2651be76cc62 100644
--- a/src/predefSemantics.ml
+++ b/src/predefSemantics.ml
@@ -9,10 +9,9 @@ open Errors
open Unify
(* exported *)
-type 'a evaluator = 'a list list -> 'a list
-type typer = type_eff evaluator
-type const_evaluator = const_eff evaluator
-type clocker = clock_eff evaluator
+type typer = type_eff Predef.evaluator
+type const_evaluator = Predef.const_eff evaluator
+type clocker = Predef.clock_eff evaluator
(*********************************************************************************)
@@ -76,8 +75,8 @@ let ii_profile = [(id "i", i)], [(id "o", i)] (* int -> int *)
let iii_profile = [(id "i1", i);(id "i2", i)], [(id "o", i)] (* int*int -> int *)
let rr_profile = [(id "i", r)], [(id "o", r)] (* real -> real *)
let rrr_profile = [(id "i1", r);(id "i2", r)], [(id "o", r)] (* real*real -> real *)
-let ri_profile = [id "i", i], [id "o", r] (* real -> int *)
-let ir_profile = [id "i", r], [id "o", i] (* int -> real *)
+let ri_profile = [id "i", r], [id "o", i] (* real -> int *)
+let ir_profile = [id "i", i], [id "o", r] (* int -> real *)
(** Constant profiles *)
let b_profile = [],[id "o", b]
@@ -477,71 +476,3 @@ let (clocking_tab: op -> clocker) =
assert false
-(*********************************************************************************)
-(*********************************************************************************)
-(*
-pour evaluer l'égalité, Pascal faisait comme ca (j'ai été plus (trop ?) brutal) :
- (*----------------------------
- Calcul de l'égalité
- N.B. Sur les constantes abstraites
- on est très méfiant
- N.B. Sur les types structure,
- on fait des appels récursifs
- ----------------------------*)
- let rec compute_eq
- (args : const_eff list)
- = (
- let rec fields_eq f0 f1 = (
- match (f0, f1) with
- | ([], []) ->
- [Bool_const_eff true]
-
- | ((f0,h0)::t0, (f1,h1)::t1) -> (
- assert (f0 = f1);
- match (compute_eq [h0;h1]) with
- [Bool_const_eff false] -> [Bool_const_eff false]
- | [Bool_const_eff true] -> (fields_eq t0 t1)
- | _ -> assert false
- )
- | _ -> assert false
- )
- in
- match args with
- [Bool_const_eff v0; Bool_const_eff v1] -> [Bool_const_eff (v0 = v1)]
- | [Int_const_eff v0; Int_const_eff v1] -> [Bool_const_eff (v0 = v1)]
- | [Real_const_eff v0; Real_const_eff v1] -> (
- let res = (v0 = v1) in
- warning src
- (sprintf "float in static exp: %f=%f evaluated as %b" v0 v1 res);
- [Bool_const_eff res]
- )
- (*
- 2007-07 obsolete
-
- | [Extern_const_eff (v0, t0); Extern_const_eff (v1, t1)] -> (
- if (t0 <> t1) then (
- type_error args "t*t for some type t"
- ) else if (v0 <> v1) then (
- uneval_error args (
- sprintf "%s=%s (external constants)"
- (string_of_fullid v0)
- (string_of_fullid v1)
- )
- ) else (
- [Bool_const_eff true]
- )
- )
- *)
- | [Enum_const_eff (v0, t0); Enum_const_eff (v1, t1)] -> (
- if (t0 = t1) then [Bool_const_eff (v0 = v1)]
- else type_error args "t*t for some type t"
- )
- | [Struct_const_eff (f0, t0); Struct_const_eff (f1, t1)] -> (
- if (t0 = t1) then (fields_eq f0 f1)
- else type_error args "t*t for some type t"
- )
- | [x;y] -> type_error args "t*t for some type t"
- | x -> arity_error args "2"
- )
- in
- *)
diff --git a/src/predefSemantics.mli b/src/predefSemantics.mli
index 756a394b2fb034d3f3a8164cf044097d09f11bdf..01b456d888a6c30eaf9b1c28ee842120b976c6db 100644
--- a/src/predefSemantics.mli
+++ b/src/predefSemantics.mli
@@ -24,8 +24,6 @@ type 'a evaluator = 'a list list -> 'a list
open CompiledData
-(* it is a list of list in order to deal with Lustre tuples *)
-
type typer = type_eff evaluator
type const_evaluator = const_eff evaluator
type clocker = clock_eff evaluator
diff --git a/src/test/Makefile b/src/test/Makefile
index d2163ce30d8594fe8c4bcfb855fb1b54bfb8c9c0..b8d609fd32746d03686632dcb60aa163f3a9a831 100644
--- a/src/test/Makefile
+++ b/src/test/Makefile
@@ -3,7 +3,7 @@ LC=../lus2lic -vl 3 --compile-all-items
LC2=../lus2lic --compile-all-items
NL="----------------------------------------------------------------------\\n"
-
+filter_line=grep -v Opening\ file
OK_LUS=$(shell find should_work -name "*.lus" -print | sort -n)
@@ -38,16 +38,19 @@ xxx:
unit:
$(LC0) -unit -h
+toto:
+ $(LC2) toto.lus -o toto.lic | $(filter_line)
+
test: unit
echo "Non-regression tests" > test_ok.res
echo "Those tests are supposed to generate errors" > test_ko.res
for d in ${OK_LUS}; do \
echo -e "\n$(NL)====> $(LC) $$d" >> test_ok.res; \
- $(LC) $$d >> test_ok.res 2>&1 ;\
+ $(LC) $$d >> test_ok.res 2>&1 ;\
done; \
for d in ${KO_LUS}; do \
- echo -e "\n$(NL)====> $(LC) $$d" >> test_ko.res; \
- $(LC) $$d >> test_ko.res 2>&1 ;\
+ echo -e "\n$(NL)====> $(LC) $$d" >> test_ko.res; \
+ $(LC) $$d >> test_ko.res 2>&1 ;\
done; \
rm -f test.res ; cat test_ok.res test_ko.res > test.res ;\
diff -u test.res.exp test.res > test.diff || \