From 4588d9682a0ece4cf5ee2819615ce79a7134ff61 Mon Sep 17 00:00:00 2001 From: Erwan Jahier <jahier@imag.fr> Date: Fri, 29 Aug 2008 10:53:27 +0200 Subject: [PATCH] Rename CompiledData into Eff. --- src/Makefile | 2 +- src/TODO | 22 +- src/compile.ml | 4 +- src/{compiledData.ml => eff.ml} | 268 +++++++++--------- src/errors.ml | 6 +- src/evalClock.ml | 88 +++--- src/evalClock.mli | 13 +- src/evalConst.ml | 54 ++-- src/evalConst.mli | 26 +- src/evalType.ml | 60 ++-- src/evalType.mli | 7 +- src/getEff.ml | 150 +++++----- src/getEff.mli | 24 +- src/iteratorSemantic.ml | 21 -- src/iteratorSemantic.mli | 1 - src/lazyCompiler.ml | 131 +++++---- src/lazyCompiler.mli | 4 +- src/licDump.ml | 322 ++++++++++----------- src/licDump.mli | 35 ++- src/parser.mly | 44 +-- src/parserUtils.ml | 12 +- src/predefEvalClock.ml | 7 +- src/predefEvalClock.mli | 6 +- src/predefEvalConst.ml | 16 +- src/predefEvalConst.mli | 11 +- src/predefEvalType.ml | 32 +-- src/predefEvalType.mli | 23 +- src/predefSemantics.ml | 478 -------------------------------- src/predefSemantics.mli | 53 ---- src/solveIdent.ml | 10 +- src/split.ml | 42 +-- src/split.mli | 4 +- src/syntaxTreeCore.ml | 4 +- src/syntaxTreeDump.ml | 80 +++--- src/test/test.res.exp | 2 +- src/unifyClock.ml | 19 +- src/unifyClock.mli | 19 +- src/unifyType.ml | 17 +- src/unifyType.mli | 6 +- src/uniqueOutput.ml | 41 ++- src/uniqueOutput.mli | 4 +- 41 files changed, 808 insertions(+), 1360 deletions(-) rename src/{compiledData.ml => eff.ml} (64%) delete mode 100644 src/iteratorSemantic.ml delete mode 100644 src/iteratorSemantic.mli delete mode 100644 src/predefSemantics.ml delete mode 100644 src/predefSemantics.mli diff --git a/src/Makefile b/src/Makefile index 8c965644..03967361 100644 --- a/src/Makefile +++ b/src/Makefile @@ -32,7 +32,7 @@ SOURCES = \ ./expandPack.ml \ ./symbolTab.mli \ ./symbolTab.ml \ - ./compiledData.ml \ + ./eff.ml \ ./licDump.ml \ ./unifyType.mli \ ./unifyType.ml \ diff --git a/src/TODO b/src/TODO index f706890a..d8dcbd2d 100644 --- a/src/TODO +++ b/src/TODO @@ -122,7 +122,7 @@ n'est pas le cas pour l'instant... cf [solve_ident] * traiter les types int, real, bool dans Predef ? -* accepter les expressions su style "b when not(a)" ? +* accepter les expressions du style "b when not(a)" ? ou bien rajouter un mot clef "whenot" comme Marc? * un noeud sans memoire pourra etre déclaré comme "node" ou comme @@ -140,6 +140,26 @@ n'est pas le cas pour l'instant... cf [solve_ident] *** facile ---------- +* (a, b, c) = (1, 1, 1) fby (x, x, x); + +est traduit en y + +... + +il faudrait plutot + + (a, b, c) = (_v1 fby _v2); + (_v1, _v2, _v3) = (1, 1, 1); + (_v4, _v5, _v6) = (x, x, x); + + + +??? + a = _v1 -> _v4; + b = _v2 -> _v5; + (sans introduire de var ici) + ... + * Revoir la facon de fournir des noms frais de variables (eg, split.ml) -> renommer les variables du programme en les prefixant par "_". diff --git a/src/compile.ml b/src/compile.ml index 305670bc..e29e3ad3 100644 --- a/src/compile.ml +++ b/src/compile.ml @@ -1,4 +1,4 @@ -(** Time-stamp: <modified the 28/08/2008 (at 10:24) by Erwan Jahier> *) +(** Time-stamp: <modified the 28/08/2008 (at 14:47) by Erwan Jahier> *) open Lxm @@ -36,7 +36,7 @@ let (doit : SyntaxTree.pack_or_model list -> Ident.idref option -> unit) = | Some main_node -> (* la clée "absolue" du main node (pas d'args statiques) *) let main_node_key = - CompiledData.make_simple_node_key (Ident.long_of_idref main_node) + Eff.make_simple_node_key (Ident.long_of_idref main_node) in Verbose.printf "-- MAIN NODE: \"%s\"\n" diff --git a/src/compiledData.ml b/src/eff.ml similarity index 64% rename from src/compiledData.ml rename to src/eff.ml index c160cf4c..20b7ad41 100644 --- a/src/compiledData.ml +++ b/src/eff.ml @@ -1,11 +1,11 @@ -(** Time-stamp: <modified the 28/08/2008 (at 10:26) by Erwan Jahier> *) +(** Time-stamp: <modified the 28/08/2008 (at 17:19) by Erwan Jahier> *) (** *) (*---------------------------------------------------------------------- - module : CompiledData + module : Eff date : ------------------------------------------------------------------------ @@ -21,42 +21,42 @@ D'une manière générale, la compil d'une entité syntaxique "toto" est implémentée par une fonction check_toto, qui prend en entrée (entr'autre) un toto et renvoie un - toto_eff. + toto. TYPES DE DONNEES : - - type_eff : + - type_ : dénotation de type effectif, implémente l'équivalence des types, construit à partir d'une type_exp. - - const_eff : + - const : dénotation de constante effective, construit à partir d'une val_exp => IL S'AGIT DE LA REPRESENTATION INTERNE DES CONSTANTES STATIQUES - - var_info_eff : + - var_info : déclaration de variable, construit à partir de var_info. - - val_eff : - union entre const_eff et var_info_eff. + - val : + union entre const et var_info. - - slice_info_eff : + - slice_info : dénotation de tranche de tableau, construit à partir de slice_info. - - left_eff : + - left : version compilée de left_part - - eq_info_eff : + - eq_info : version compilée de eq_info - - node_exp_eff : + - node_exp : dénotation d'opération, peut être predef ou utilisateur, construit à partir de node_exp. - - static_arg_eff : + - static_arg : déclaration d'un static arg - pack_env : @@ -76,18 +76,18 @@ UTILITAIRES : - - type_of_const_eff : renvoie le type_eff d'une const_eff - - string_of_type_eff : pretty-print d'un type_eff - - string_of_const_eff : pretty-print d'une const_eff + - type_of_const : renvoie le type d'une const + - string_of_type : pretty-print d'un type + - string_of_const : pretty-print d'une const - string_of_node_key : pretty-print d'un node_key - _ string_of_slice_eff : + _ string_of_slice : ----------------------------------------------------------------------*) open Printf open Lxm open SyntaxTree -open SyntaxTreeCore +(* open SyntaxTreeCore *) (*--------------------------------------------------------------------- Type : id_solver @@ -101,38 +101,38 @@ N.B. On fournit les constructeurs des id_solver courants, voir : ----------------------------------------------------------------------*) type id_solver = { (* XXX I should not have [idref] in this module !!! *) - id2const : Ident.idref -> Lxm.t -> const_eff; - id2type : Ident.idref -> Lxm.t -> type_eff; - id2node : Ident.idref -> static_arg_eff list -> Lxm.t -> node_exp_eff; - id2var : Ident.idref -> Lxm.t -> var_info_eff; + id2const : Ident.idref -> Lxm.t -> const; + id2type : Ident.idref -> Lxm.t -> type_; + id2node : Ident.idref -> static_arg list -> Lxm.t -> node_exp; + id2var : Ident.idref -> Lxm.t -> var_info; symbols : SymbolTab.t; } (*--------------------------------------------------------------------- - Type : type_eff + Type : type ----------------------------------------------------------------------- Dénotation de type immédiat : l'équivalence sémantique des types - EST l'équivalence structurelle des type_eff. + EST l'équivalence structurelle des type. Par rapport à une type_exp : - pas d'alias - taille des tableaux résolues ----------------------------------------------------------------------*) -and type_eff = +and type_ = | Bool_type_eff | Int_type_eff | Real_type_eff | External_type_eff of Ident.long | Enum_type_eff of Ident.long * (Ident.long list) - | Array_type_eff of type_eff * int + | Array_type_eff of type_ * int | Struct_type_eff of - Ident.long * (Ident.t * (type_eff * const_eff option)) list + Ident.long * (Ident.t * (type_ * const option)) list | Any | Overload (* [Overload] is like [Any], except that it can only be [int] or [real] *) -and slice_info_eff = { +and slice_info = { (** Dénotation de tranche de tableau correcte : si A est le tableau d'entrée, alors S est le tableau de sortie avec : @@ -144,7 +144,7 @@ and slice_info_eff = { se_width : int; (* -> size? *) } -and left_eff = +and left = (** Version checkée des left_part (les idents, les index et les tranches sont résolus) @@ -152,105 +152,105 @@ and left_eff = bien qu'il soit possible de le retrouver. N.B. On garde aussi l'info source des idents au cas ou.*) - | LeftVarEff of (var_info_eff * Lxm.t) - | LeftFieldEff of (left_eff * Ident.t * type_eff) - | LeftArrayEff of (left_eff * int * type_eff) - | LeftSliceEff of (left_eff * slice_info_eff * type_eff) + | LeftVarEff of (var_info * Lxm.t) + | LeftFieldEff of (left * Ident.t * type_) + | LeftArrayEff of (left * int * type_) + | LeftSliceEff of (left * slice_info * type_) -and eq_info_eff = left_eff list * val_exp_eff +and eq_info = left list * val_exp -and val_exp_eff = - | CallByPosEff of (by_pos_op_eff srcflagged * operands_eff) +and val_exp = + | CallByPosEff of (by_pos_op srcflagged * operands) | CallByNameEff of - (by_name_op_eff srcflagged * (Ident.t srcflagged * val_exp_eff) list) + (by_name_op srcflagged * (Ident.t srcflagged * val_exp) list) -and operands_eff = OperEff of val_exp_eff list +and operands = OperEff of val_exp list -and by_name_op_eff = - | STRUCT_eff of Ident.pack_name * Ident.idref - | STRUCT_anonymous_eff +and by_name_op = + | STRUCT of Ident.pack_name * Ident.idref + | STRUCT_anonymous -and by_pos_op_eff = - | Predef_eff of Predef.op * static_arg_eff list - | CALL_eff of node_exp_eff srcflagged - | IDENT_eff of Ident.idref (* should be an Ident.t or long, really... *) - | CONST_eff of Ident.idref * Ident.pack_name +and by_pos_op = + | Predef of Predef.op * static_arg list + | CALL of node_exp srcflagged + | IDENT of Ident.idref (* should be an Ident.t or long, really... *) + | CONST of Ident.idref * Ident.pack_name - | PRE_eff - | ARROW_eff - | FBY_eff - | CURRENT_eff + | PRE + | ARROW + | FBY + | CURRENT - | WHEN_eff of var_info_eff - | WHENOT_eff of var_info_eff - | TUPLE_eff - | WITH_eff of val_exp_eff + | WHEN of var_info + | WHENOT of var_info + | TUPLE + | WITH of val_exp - | CONCAT_eff - | HAT_eff of int * val_exp_eff - | ARRAY_eff - | STRUCT_ACCESS_eff of Ident.t + | CONCAT + | HAT of int * val_exp + | ARRAY + | STRUCT_ACCESS of Ident.t (* those are different from [by_pos_op] *) - | ARRAY_ACCES_eff of int * type_eff (* index + type of the element *) - | ARRAY_SLICE_eff of slice_info_eff * type_eff - | MERGE_eff of (Ident.t * (Ident.t list)) + | ARRAY_ACCES of int * type_ (* index + type_ of the element *) + | ARRAY_SLICE of slice_info * type_ + | MERGE of (Ident.t * (Ident.t list)) (*--------------------------------------------------------------------- - Type : const_eff + Type : const ----------------------------------------------------------------------- Dénotation de constante immédiate - N.B. les const_eff "portent" leur type : + N.B. les const "portent" leur type : - il est implicite pour bool, int, real, - explicite pour extern, enum et struct - pour array c'est le TYPE DES ELEMENTS QU'ON TRIMBALE - VOIR => type_of_const_eff + VOIR => type_of_const ----------------------------------------------------------------------*) -and const_eff = +and const = (* type predef *) Bool_const_eff of bool | Int_const_eff of int | Real_const_eff of float (* type atomique non predef : on précise le type *) - | Extern_const_eff of (Ident.long * type_eff * const_eff option) - | Enum_const_eff of (Ident.long * type_eff) - (* type structure : liste (champ,valeur) + type structure *) - | Struct_const_eff of ((Ident.t * const_eff) list * type_eff) - (* type tableau : liste des valeurs + type des elts + taille *) - | Array_const_eff of (const_eff array * type_eff) + | Extern_const_eff of (Ident.long * type_ * const option) + | Enum_const_eff of (Ident.long * type_) + (* type_ structure : liste (champ,valeur) + type_ structure *) + | Struct_const_eff of ((Ident.t * const) list * type_) + (* type_ tableau : liste des valeurs + type_ des elts + taille *) + | Array_const_eff of (const array * type_) (*--------------------------------------------------------------------- - Type: val_eff + Type: val ----------------------------------------------------------------------- Une constante ou une variable => item de la table des symboles de valeurs ----------------------------------------------------------------------*) -(* and val_eff = *) -(* ConstEff of const_eff *) -(* | VarEff of var_info_eff *) +(* and val = *) +(* ConstEff of const *) +(* | VarEff of var_info *) (*--------------------------------------------------------------------- - Type: var_info_eff + Type: var_info ----------------------------------------------------------------------- Info associée à un ident de variable ----------------------------------------------------------------------*) (* ICI à completer/modifier sans doute *) -and var_info_eff = { +and var_info = { var_name_eff : Ident.t; - var_nature_eff : var_nature; + var_nature_eff : SyntaxTreeCore.var_nature; var_number_eff : int; - var_type_eff : type_eff; - var_clock_eff : clock_eff; + var_type_eff : type_; + var_clock_eff : clock; } -and clock_eff = +and clock = | BaseEff (* it's not bezef... *) - | On of Ident.t * clock_eff + | On of Ident.t * clock | ClockVar of int (* to deal with polymorphic clocks (i.e., constants) *) (**********************************************************************************) -(** [node_exp_eff] correspond à une instance de template (ou, cas +(** [node_exp] correspond à une instance de template (ou, cas limite, de noeud sans param statique). La clé est un couple ident/liste d'arguments statiques effectifs @@ -259,34 +259,34 @@ and clock_eff = entrée (0..nb entrées-1). Les formal-clocks sont créées au cours du type-checking (et pas du clock-checking) *) -and node_exp_eff = { +and node_exp = { node_key_eff : node_key; - inlist_eff : var_info_eff list; - outlist_eff : var_info_eff list; - loclist_eff : var_info_eff list option; (* None => extern or abstract *) - def_eff : node_def_eff; + inlist_eff : var_info list; + outlist_eff : var_info list; + loclist_eff : var_info list option; (* None => extern or abstract *) + def_eff : node_def; has_mem_eff : bool; is_safe_eff : bool; lxm : Lxm.t; } -and node_def_eff = +and node_def = | ExternEff | AbstractEff - | BodyEff of node_body_eff + | BodyEff of node_body -and node_body_eff = { - asserts_eff : (val_exp_eff srcflagged) list; - eqs_eff : (eq_info_eff srcflagged) list; +and node_body = { + asserts_eff : (val_exp srcflagged) list; + eqs_eff : (eq_info srcflagged) list; } (* key used for type, constant, and clock tables *) and item_key = Ident.long -and node_key = item_key * static_arg_eff list -and static_arg_eff = - | ConstStaticArgEff of (Ident.t * const_eff) - | TypeStaticArgEff of (Ident.t * type_eff) - | NodeStaticArgEff of (Ident.t * node_exp_eff) +and node_key = item_key * static_arg list +and static_arg = + | ConstStaticArgEff of (Ident.t * const) + | TypeStaticArgEff of (Ident.t * type_) + | NodeStaticArgEff of (Ident.t * node_exp) @@ -306,7 +306,7 @@ type 'a check_flag = | Incorrect -let (profile_of_node_exp_eff : node_exp_eff -> type_eff list * type_eff list) = +let (profile_of_node_exp : node_exp -> type_ list * type_ list) = fun ne -> List.map (fun vi -> vi.var_type_eff) ne.inlist_eff, List.map (fun vi -> vi.var_type_eff) ne.outlist_eff @@ -324,10 +324,10 @@ let (profile_of_node_exp_eff : node_exp_eff -> type_eff list * type_eff list) = (* and pack_env = { *) (* penv_world : world_env ; *) (* (* penv_src : SyntaxTree.package ; *) *) -(* penv_type_table : (Ident.t, type_eff check_flag) Hashtbl.t ; *) -(* penv_const_table : (Ident.t, const_eff check_flag) Hashtbl.t ; *) -(* penv_oper_table : (Ident.t, node_half_eff) Hashtbl.t ; *) -(* penv_node_table : (node_key, node_exp_eff check_flag) Hashtbl.t *) +(* penv_type_table : (Ident.t, type check_flag) Hashtbl.t ; *) +(* penv_const_table : (Ident.t, const check_flag) Hashtbl.t ; *) +(* penv_oper_table : (Ident.t, node_half) Hashtbl.t ; *) +(* penv_node_table : (node_key, node_exp check_flag) Hashtbl.t *) (* } *) (* the local tables are indexed by Ident.t, because local idents (var,const, flow) @@ -350,27 +350,27 @@ let (profile_of_node_exp_eff : node_exp_eff -> type_eff list * type_eff list) = type local_env = { lenv_node_key : node_key ; (* lenv_globals : pack_env ; *) - lenv_types : (Ident.t, type_eff) Hashtbl.t ; - lenv_const : (Ident.t, const_eff) Hashtbl.t ; - lenv_nodes : (Ident.t, node_exp_eff) Hashtbl.t ; + lenv_types : (Ident.t, type_) Hashtbl.t ; + lenv_const : (Ident.t, const) Hashtbl.t ; + lenv_nodes : (Ident.t, node_exp) Hashtbl.t ; - lenv_vars : (Ident.t, var_info_eff) Hashtbl.t ; + lenv_vars : (Ident.t, var_info) Hashtbl.t ; } -let (lookup_type: local_env -> Ident.idref -> Lxm.t -> type_eff) = +let (lookup_type: local_env -> Ident.idref -> Lxm.t -> type_) = fun env id lxm -> Hashtbl.find env.lenv_types (Ident.name_of_idref id) -let (lookup_node: local_env -> Ident.idref -> static_arg_eff list -> Lxm.t -> - node_exp_eff) = +let (lookup_node: local_env -> Ident.idref -> static_arg list -> Lxm.t -> + node_exp) = fun env id sargs lmx -> Hashtbl.find env.lenv_nodes (Ident.name_of_idref id) -let (lookup_const: local_env -> Ident.idref -> Lxm.t -> const_eff) = +let (lookup_const: local_env -> Ident.idref -> Lxm.t -> const) = fun env id lmx -> Hashtbl.find env.lenv_const (Ident.name_of_idref id) -let (lookup_var: local_env -> Ident.t -> Lxm.t -> var_info_eff) = +let (lookup_var: local_env -> Ident.t -> Lxm.t -> var_info) = fun env id lmx -> Hashtbl.find env.lenv_vars id @@ -401,28 +401,28 @@ let (make_local_env : node_key -> local_env) = (** [type_are_compatible t1 t2] checks that t1 is compatible with t2, i.e., if t1 = t2 or t1 is abstract and not t2. *) -let (type_eff_are_compatible : type_eff -> type_eff -> bool) = +let (type_are_compatible : type_ -> type_ -> bool) = fun te1 te2 -> match te1, te2 with | External_type_eff id1, External_type_eff id2 -> id1 = id2 | External_type_eff _, _ -> true | t1, t2 -> t1 = t2 -let rec (clock_eff_are_equals : clock_eff -> clock_eff -> bool) = +let rec (clock_are_equals : clock -> clock -> bool) = fun c1 c2 -> match c1, c2 with - | On(_,c1), On(_,c2) -> clock_eff_are_equals c1 c2 + | On(_,c1), On(_,c2) -> clock_are_equals c1 c2 | c1, c2 -> c1 = c2 -let (var_eff_are_compatible : var_info_eff -> var_info_eff -> bool) = +let (var_are_compatible : var_info -> var_info -> bool) = fun v1 v2 -> - (type_eff_are_compatible v1.var_type_eff v2.var_type_eff) && - (clock_eff_are_equals v1.var_clock_eff v2.var_clock_eff) + (type_are_compatible v1.var_type_eff v2.var_type_eff) && + (clock_are_equals v1.var_clock_eff v2.var_clock_eff) (****************************************************************************) (* Utilitaires liés aux node_key *) let (make_simple_node_key : Ident.long -> node_key) = fun nkey -> (nkey, []) -let rec (subst_type : type_eff -> type_eff -> type_eff) = +let rec (subst_type : type_ -> type_ -> type_) = fun t teff_ext -> match teff_ext with (* substitutes [t] in [teff_ext] *) | Bool_type_eff -> Bool_type_eff @@ -439,7 +439,7 @@ let rec (subst_type : type_eff -> type_eff -> type_eff) = | Overload -> t -let (type_of_const_eff: const_eff -> type_eff) = +let (type_of_const: const -> type_) = function | Bool_const_eff v -> Bool_type_eff | Int_const_eff v -> Int_type_eff @@ -450,26 +450,26 @@ let (type_of_const_eff: const_eff -> type_eff) = | Array_const_eff (ct, teff) -> Array_type_eff (teff, Array.length ct) -let (type_eff_of_left_eff: left_eff -> type_eff) = +let (type_of_left: left -> type_) = function - | LeftVarEff (vi_eff,lxm) -> vi_eff.var_type_eff - | LeftFieldEff(_, _, t_eff) -> t_eff - | LeftArrayEff(_, _, t_eff) -> t_eff - | LeftSliceEff(_, _, t_eff) -> t_eff + | LeftVarEff (vi,lxm) -> vi.var_type_eff + | LeftFieldEff(_, _, t) -> t + | LeftArrayEff(_, _, t) -> t + | LeftSliceEff(_, _, t) -> t -let rec (clock_of_left_eff: left_eff -> clock_eff) = +let rec (clock_of_left: left -> clock) = 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 + | LeftVarEff (var_info, _) -> var_info.var_clock_eff + | LeftFieldEff (left,_,_) -> clock_of_left left + | LeftArrayEff (left,_,_) -> clock_of_left left + | LeftSliceEff (left,_,_) -> clock_of_left left -let rec (var_info_of_left_eff: left_eff -> var_info_eff) = +let rec (var_info_of_left: left -> var_info) = function | LeftVarEff (v, _) -> v - | LeftFieldEff (left_eff,_,_) -> var_info_of_left_eff left_eff - | LeftArrayEff (left_eff,_,_) -> var_info_of_left_eff left_eff - | LeftSliceEff (left_eff,_,_) -> var_info_of_left_eff left_eff + | LeftFieldEff (left,_,_) -> var_info_of_left left + | LeftArrayEff (left,_,_) -> var_info_of_left left + | LeftSliceEff (left,_,_) -> var_info_of_left left diff --git a/src/errors.ml b/src/errors.ml index 81a85974..ffa376fa 100644 --- a/src/errors.ml +++ b/src/errors.ml @@ -1,4 +1,4 @@ -(** Time-stamp: <modified the 30/06/2008 (at 11:06) by Erwan Jahier> *) +(** Time-stamp: <modified the 28/08/2008 (at 14:48) by Erwan Jahier> *) (*---------------------------------------------------------------------- module : Errors.ml @@ -28,12 +28,12 @@ une erreur qui n'est pas spécialement liée à un lexeme, (mais peut-être liée à un noeud -> void checkNode) * - - Compile_node_error of CompiledData.node_key * Lxm.t * string : + - Compile_node_error of Eff.node_key * Lxm.t * string : ------------------------------------------------------------------ une erreur de compil liée à un lexeme et à un noeud (en fait une instance de template) particulier * ** *** - - Global_node_error of CompiledData.node_key * string : + - Global_node_error of Eff.node_key * string : ------------------------------------------------------------------ une erreur de compil non liée à un lexeme particulier, mais dependant levée lors de la compilation d'un noeud * ** *** diff --git a/src/evalClock.ml b/src/evalClock.ml index 3b268817..816e8baf 100644 --- a/src/evalClock.ml +++ b/src/evalClock.ml @@ -1,11 +1,11 @@ -(** Time-stamp: <modified the 28/08/2008 (at 11:17) by Erwan Jahier> *) +(** Time-stamp: <modified the 29/08/2008 (at 09:28) by Erwan Jahier> *) open Predef open PredefEvalConst open SyntaxTree open SyntaxTreeCore -open CompiledData +open Eff open LicDump open Printf open Lxm @@ -59,7 +59,7 @@ open UnifyClock *) -let (check_args : Lxm.t -> subst -> clock_eff list -> clock_eff list -> subst) = +let (check_args : Lxm.t -> subst -> Eff.clock list -> Eff.clock list -> subst) = fun lxm s cil_par cil_arg -> assert (List.length cil_par = List.length cil_arg); let s = List.fold_left2 (UnifyClock.f lxm) s cil_par cil_arg in @@ -68,8 +68,8 @@ let (check_args : Lxm.t -> subst -> clock_eff list -> clock_eff list -> subst) = (** Checking expression result -------------------------- - It is the same thing, except that we have left_eff list instead - of clock_eff list. + It is the same thing, except that we have Eff.left list instead + of Eff.clock list. e.g., in the equation: @@ -80,13 +80,13 @@ let (check_args : Lxm.t -> subst -> clock_eff list -> clock_eff list -> subst) = To do that, we suppose we have: - - "left" the list of left_eff + - "left" the list of Eff.left - "rigth" the list of result clock. (via "get_clock_profile" again) and we just need to check that both side are unifiable. *) -let rec (var_info_eff_of_left_eff: left_eff -> var_info_eff) = +let rec (var_info_eff_of_left_eff: Eff.left -> Eff.var_info) = function | LeftVarEff (v, _) -> v | LeftFieldEff (l, id,_) -> @@ -111,7 +111,7 @@ let rec (var_info_eff_of_left_eff: left_eff -> var_info_eff) = let var_info_eff_to_clock_eff v = v.var_clock_eff (* exported *) -let (check_res : Lxm.t -> subst -> left_eff list -> clock_eff list -> unit) = +let (check_res : Lxm.t -> subst -> Eff.left list -> Eff.clock list -> unit) = fun lxm s left rigth -> let left_vi = List.map var_info_eff_of_left_eff left in let left_ci = List.map var_info_eff_to_clock_eff left_vi in @@ -124,7 +124,7 @@ let (check_res : Lxm.t -> subst -> left_eff list -> clock_eff list -> unit) = (** In order to clock check "when" statements, we need to know if a clock [sc] is a sub_clock of another one c (i.e., for all instants i, c(i) => sc(i)) *) -let rec (is_a_sub_clock : Lxm.t -> subst -> clock_eff -> clock_eff -> subst option) = +let rec (is_a_sub_clock : Lxm.t -> subst -> Eff.clock -> Eff.clock -> subst option) = fun lxm s sc c -> (* check if [sc] is a sub-clock of [c] (in the large sens). Returns Some updated substitution if it is the case, @@ -157,9 +157,9 @@ let rec (is_a_sub_clock : Lxm.t -> subst -> clock_eff -> clock_eff -> subst opti Some (s1,(i,sc)::s2) -type clock_profile = clock_eff list * clock_eff list +type clock_profile = Eff.clock list * Eff.clock list -let (get_clock_profile : node_exp_eff -> clock_profile) = +let (get_clock_profile : Eff.node_exp -> clock_profile) = fun n -> (List.map var_info_eff_to_clock_eff n.inlist_eff, List.map var_info_eff_to_clock_eff n.outlist_eff) @@ -178,7 +178,7 @@ let (make_dummy_var: string -> Ident.t) = let concat_subst (s11,s12) (s21,s22) = (s11 @ s21, s12@s22) (******************************************************************************) -(* We tabulate the result of the val_exp_eff clock ckecking. Note, +(* We tabulate the result of the Eff.val_exp clock ckecking. Note, that there is no clash in that table because all var_exp_eff are srcflagged. *) @@ -193,7 +193,8 @@ let tabulate_res vef clock_eff_list = (* flush stdout; *) Hashtbl.add val_exp_eff_clk_tab vef clock_eff_list -let (get_val_exp_eff : val_exp_eff -> clock_eff list) = + +let (get_val_exp_eff : Eff.val_exp -> Eff.clock list) = fun vef -> try let res = Hashtbl.find val_exp_eff_clk_tab vef in @@ -201,6 +202,7 @@ let (get_val_exp_eff : val_exp_eff -> clock_eff list) = (* Some expressions migth be infered to be a variable clock (e.g., constants). In that case, it is ok to consider that such expressions are on the base clock.*) + (* XXX 'm pretty sure this is wrong! *) | ClockVar _ | On(_,ClockVar _) -> BaseEff | x -> x @@ -216,7 +218,7 @@ let (get_val_exp_eff : val_exp_eff -> clock_eff list) = (******************************************************************************) (** Now we can go on and define [f]. *) -let rec (f : id_solver -> subst -> val_exp_eff -> clock_eff list * subst) = +let rec (f : Eff.id_solver -> subst -> Eff.val_exp -> Eff.clock list * subst) = fun id_solver s ve -> cpt_var_name := 0; UnifyClock.reset_var_type (); @@ -249,7 +251,7 @@ and f_aux id_solver s ve = cel, s (* iterate f on a list of expressions *) -and (f_list : id_solver -> subst -> val_exp_eff list -> clock_eff list list * subst) = +and (f_list : Eff.id_solver -> subst -> Eff.val_exp list -> Eff.clock list list * subst) = fun id_solver s args -> let aux (acc,s) arg = let cil, s = f_aux id_solver s arg in @@ -259,19 +261,19 @@ and (f_list : id_solver -> subst -> val_exp_eff list -> clock_eff list list * su let cil = List.rev cil in cil, s -and (eval_by_pos_clock : id_solver -> by_pos_op_eff -> Lxm.t -> val_exp_eff list -> - subst -> clock_eff list * subst) = +and (eval_by_pos_clock : Eff.id_solver -> Eff.by_pos_op -> Lxm.t -> Eff.val_exp list -> + subst -> Eff.clock list * subst) = fun id_solver posop lxm args s -> match posop with - | CURRENT_eff -> ( (* we return the clock of the argument *) + | Eff.CURRENT -> ( (* we return the clock of the argument *) let clocks_of_args, s = f_list id_solver s args in match List.flatten clocks_of_args with | [BaseEff] -> [BaseEff],s | [On(_,clk)] -> [clk],s | _ -> assert false ) - | WHENOT_eff clk_var -> assert false (* use merge when it is implemented *) - | WHEN_eff clk_var -> ( + | Eff.WHENOT clk_var -> assert false (* use merge when it is implemented *) + | Eff.WHEN clk_var -> ( let clk = var_info_eff_to_clock_eff clk_var in (match f_list id_solver s args with | [[c1];_], s -> ( @@ -300,19 +302,19 @@ and (eval_by_pos_clock : id_solver -> by_pos_op_eff -> Lxm.t -> val_exp_eff list | _ -> assert false (* "(x1,x2) when node (x,y)" *) ) ) - | MERGE_eff _ -> assert false + | Eff.MERGE _ -> assert false (* f_aux id_solver (List.hd args) *) - | HAT_eff(i,ve) -> f_aux id_solver s ve + | Eff.HAT(i,ve) -> f_aux id_solver s ve (* nb: the args have been put inside the HAT_eff constructor *) - | CONST_eff (idref,_) -> [get_constant_clock ()],s - | IDENT_eff idref -> ( + | Eff.CONST (idref,_) -> [get_constant_clock ()],s + | Eff.IDENT idref -> ( try ([var_info_eff_to_clock_eff (id_solver.id2var idref lxm)], s) with _ -> (* => it is a constant *) [get_constant_clock ()],s ) - | CALL_eff node_exp_eff -> + | Eff.CALL node_exp_eff -> let (cil_arg, cil_res) = get_clock_profile node_exp_eff.it in (* the value of the base clock of a node is actually relative to the context into which the node is called. @@ -321,7 +323,7 @@ and (eval_by_pos_clock : id_solver -> by_pos_op_eff -> Lxm.t -> val_exp_eff list by the caller. *) let rel_base = ClockVar (UnifyClock.get_var_type ()) in - let rec (replace_base : clock_eff -> clock_eff -> clock_eff) = + let rec (replace_base : Eff.clock -> Eff.clock -> Eff.clock) = fun rel_base ci -> (* [replace_base rel_base ci ] replaces in [ci] any occurences of the base clock by [rel_base] *) @@ -337,14 +339,14 @@ and (eval_by_pos_clock : id_solver -> by_pos_op_eff -> Lxm.t -> val_exp_eff list List.map (apply_subst s) cil_res, s (* One argument. *) - | PRE_eff - | STRUCT_ACCESS_eff _ - | ARRAY_ACCES_eff (_, _) - | ARRAY_SLICE_eff (_,_) -> + | Eff.PRE + | Eff.STRUCT_ACCESS _ + | Eff.ARRAY_ACCES (_, _) + | Eff.ARRAY_SLICE (_,_) -> assert(List.length args = 1); f_aux id_solver s (List.hd args) - | Predef_eff (op,sargs) -> + | Eff.Predef (op,sargs) -> let clk_args, s = f_list id_solver s args in let flat_clk_args = List.flatten clk_args in (* => mono-clock! *) @@ -356,11 +358,11 @@ and (eval_by_pos_clock : id_solver -> by_pos_op_eff -> Lxm.t -> val_exp_eff list PredefEvalClock.f op lxm sargs clk_list, s (* may have tuples as arguments *) - | TUPLE_eff - | ARROW_eff - | FBY_eff - | CONCAT_eff - | ARRAY_eff -> ( + | Eff.TUPLE + | Eff.ARROW + | Eff.FBY + | Eff.CONCAT + | Eff.ARRAY -> ( (* Check that all args are of the same (unifiable) clocks. XXX : we suppose that all those operators are @@ -372,22 +374,22 @@ and (eval_by_pos_clock : id_solver -> by_pos_op_eff -> Lxm.t -> val_exp_eff list let clk,s = UnifyClock.list lxm flat_clk_args s in let clk_list = match posop with - | TUPLE_eff -> List.map (apply_subst s) flat_clk_args + | Eff.TUPLE -> List.map (apply_subst s) flat_clk_args | _ -> List.map (apply_subst s) (List.hd clk_args) in clk_list, s ) - | WITH_eff(ve) -> f_aux id_solver s ve + | Eff.WITH(ve) -> f_aux id_solver s ve -and (eval_by_name_clock : id_solver -> by_name_op_eff -> Lxm.t -> - (Ident.t Lxm.srcflagged * val_exp_eff) list -> subst -> - clock_eff list * subst) = +and (eval_by_name_clock : Eff.id_solver -> Eff.by_name_op -> Lxm.t -> + (Ident.t Lxm.srcflagged * Eff.val_exp) list -> subst -> + Eff.clock list * subst) = fun id_solver namop lxm namargs s -> match namop with - | STRUCT_anonymous_eff -> assert false (* cf EvalType.f *) - | STRUCT_eff _ -> + | Eff.STRUCT_anonymous -> assert false (* cf EvalType.E *) + | Eff.STRUCT _ -> let args = List.map (fun (id,ve) -> ve) namargs in (* XXX The 3 following lines duplicates the code of TUPLE_eff and co *) let clk_args, s = f_list id_solver s args in diff --git a/src/evalClock.mli b/src/evalClock.mli index c604d44d..5b088787 100644 --- a/src/evalClock.mli +++ b/src/evalClock.mli @@ -1,6 +1,5 @@ -(** Time-stamp: <modified the 28/08/2008 (at 10:43) by Erwan Jahier> *) +(** Time-stamp: <modified the 28/08/2008 (at 16:01) by Erwan Jahier> *) -open CompiledData open UnifyClock (** [f ids ve] checks that [ve] is well-clocked (i.e., for node calls, @@ -8,7 +7,7 @@ open UnifyClock and returns a clock profile that contains all the necessary information to be able to check. *) -val f : id_solver -> subst -> val_exp_eff -> clock_eff list * subst +val f : Eff.id_solver -> subst -> Eff.val_exp -> Eff.clock list * subst (** [check_res lxm cel cil] checks that the expected output clock @@ -22,17 +21,17 @@ val f : id_solver -> subst -> val_exp_eff -> clock_eff list * subst it checks that the clock of "(x,y)" (cel) is compatible with the output clock profile of node toto (cil). - The type [clock_eff_res] is exported to be able to call that + The type [Eff.clock_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). + Eff.val_exp). *) -val check_res : Lxm.t -> subst -> left_eff list -> clock_eff list -> unit +val check_res : Lxm.t -> subst -> Eff.left list -> Eff.clock list -> unit (* Returns the clock of an expression. Note that this function uses an internal table, and therefore it should not be called before the clock checking has been done (by the function f above).*) -val get_val_exp_eff : val_exp_eff -> clock_eff list +val get_val_exp_eff : Eff.val_exp -> Eff.clock list diff --git a/src/evalConst.ml b/src/evalConst.ml index ac108ca5..032a3ced 100644 --- a/src/evalConst.ml +++ b/src/evalConst.ml @@ -1,12 +1,12 @@ -(** Time-stamp: <modified the 28/08/2008 (at 10:26) by Erwan Jahier> *) +(** Time-stamp: <modified the 29/08/2008 (at 10:21) by Erwan Jahier> *) open Printf open Lxm open Errors open SyntaxTree +open Eff open SyntaxTreeCore -open CompiledData open Predef open PredefEvalConst open PredefEvalType @@ -40,21 +40,21 @@ venir de eva et donc N.B. Puisque correct, last_ix est inutile, mais bon ... -----------------------------------------------------*) let (make_slice_const : - const_eff array -> type_eff -> slice_info_eff -> const_eff list) = + Eff.const array -> Eff.type_ -> Eff.slice_info -> Eff.const list) = fun ctab ctype slice -> let get_res (ix : int) = Array.get ctab (slice.se_first + ix*slice.se_step) in [Array_const_eff (Array.init slice.se_width get_res, ctype)] (** Utilitaire : fabriquer si possible une constante tableau *) -let (make_array_const : const_eff list array -> const_eff) = +let (make_array_const : Eff.const list array -> Eff.const) = fun ops -> let expected_type = ref None in - let treat_arg (op : const_eff list) = + let treat_arg (op : Eff.const list) = match op with | [x] -> ( (* non tuple *) - let xtyp = type_of_const_eff x in + let xtyp = Eff.type_of_const x in match (!expected_type) with | None -> expected_type := Some xtyp; x | Some t -> ( @@ -81,21 +81,21 @@ let (make_array_const : const_eff list array -> const_eff) = N.B. Par construction on sait que nops n'a pas de doublons *) let make_struct_const - (teff : type_eff) - (arg_tab : (Ident.t, Lxm.t * const_eff) Hashtbl.t) = + (teff : Eff.type_) + (arg_tab : (Ident.t, Lxm.t * Eff.const) Hashtbl.t) = ( (* on verifie qu'on a bien un type struct *) match teff with Struct_type_eff (tnm, flst) -> ( (* on construit la liste dans le BON ordre *) - let make_eff_field ((fn: Ident.t),((ft:type_eff),(fv:const_eff option))) = ( + let make_eff_field ((fn: Ident.t),((ft:Eff.type_),(fv:Eff.const option))) = ( try ( (* on prend en priorité dans arg_tab *) match (Hashtbl.find arg_tab fn) with (lxm, v) -> ( (* effet de bord : on vire la valeur de arg_tab *) Hashtbl.remove arg_tab fn ; - let vt = type_of_const_eff v in + let vt = Eff.type_of_const v in if (vt = ft) then (fn, v) (*ok*) else raise (Compile_error( lxm , @@ -121,7 +121,7 @@ let make_struct_const (* on mappe flst pour avoir la liste dans le bon ordre *) let eff_fields = List.map make_eff_field flst in (* si arg_tab n'est pas vide, erreur sur le premier *) - let raise_error (id : Ident.t) ((lxm : Lxm.t), (veff : const_eff)) + let raise_error (id : Ident.t) ((lxm : Lxm.t), (veff : Eff.const)) = raise(Compile_error( lxm, sprintf @@ -148,15 +148,15 @@ let l2ll l = if l = [] then [] else [l] Evaluation récursive des expressions constantes ------------------------------------------------------ f : - - entrées : id_solver et val_exp - - sortie : const_eff list + - entrées : Eff.id_solver et val_exp + - sortie : Eff.const list - Effet de bord : Compile_error Rôle : -> résoud les références aux idents -> gère les appels récursifs (évaluation des arguments) ----------------------------------------------------*) let rec f - (env : id_solver) + (env : Eff.id_solver) (vexp : val_exp) = ( (*----------------------------------- @@ -164,9 +164,9 @@ let rec f -> capte les nv -> récupère les EvalConst_error -----------------------------------*) - let rec rec_eval_const (vexp : val_exp) = ( + let rec rec_eval_const (vexp : SyntaxTreeCore.val_exp) = ( match vexp with - | CallByPos ({it=posop; src=lxm}, Oper args) -> ( + | SyntaxTreeCore.CallByPos ({it=posop; src=lxm}, Oper args) -> ( try eval_by_pos_const posop lxm args with | EvalType_error msg -> @@ -174,7 +174,7 @@ let rec f | EvalConst_error msg -> raise (Compile_error(lxm, "\n*** can't eval constant: "^msg)) ) - | CallByName ({it=nmop; src=lxm}, nmargs ) -> ( + | SyntaxTreeCore.CallByName ({it=nmop; src=lxm}, nmargs ) -> ( try eval_by_name_const nmop lxm nmargs with EvalConst_error msg -> raise (Compile_error(lxm, "\n*** can't eval constant: "^msg)) @@ -222,7 +222,7 @@ let rec f match rec_eval_const cexp with | [cst] -> let atab = Array.make sz cst in - [ Array_const_eff (atab, type_of_const_eff cst) ] + [ Array_const_eff (atab, Eff.type_of_const cst) ] | x -> raise (EvalConst_error("array of tuple not allowed")) with @@ -309,7 +309,7 @@ let rec f | CURRENT_n -> not_evaluable_construct "current" | PRE_n -> not_evaluable_construct "pre" - | Predef(op,sargs) + | Predef_n(op,sargs) -> if sargs = [] then let effargs = (List.map rec_eval_const args) in @@ -392,7 +392,7 @@ let rec f EvalArray_error "bad array size, type int expected but get <t>" si t pas int EvalArray_error "bad array size <n>" si n <= 0 ----------------------------------------------------------------------*) -and (eval_array_size: id_solver -> val_exp -> int) = +and (eval_array_size: Eff.id_solver -> val_exp -> int) = fun id_solver szexp -> match (f id_solver szexp) with | [Int_const_eff sz] -> @@ -400,7 +400,7 @@ and (eval_array_size: id_solver -> val_exp -> int) = raise(EvalArray_error(sprintf "bad array size %d" sz)) | [x] -> raise(EvalArray_error(sprintf "bad array size, int expected but get %s" - (LicDump.string_of_type_eff(type_of_const_eff x)))) + (LicDump.string_of_type_eff(Eff.type_of_const x)))) | _ -> raise(EvalArray_error(sprintf "bad array size, int expected, not a tuple")) @@ -419,7 +419,7 @@ and (eval_array_size: id_solver -> val_exp -> int) = EvalArray_error msg si pas bon ----------------------------------------------------------------------*) and eval_array_index - (env : id_solver) + (env : Eff.id_solver) (ixexp : val_exp) (sz : int) (lxm : Lxm.t) @@ -435,7 +435,7 @@ and eval_array_index | [Extern_const_eff(_,_, Some x)] | [x] -> raise(EvalArray_error(sprintf "bad array index, int expected but get %s" - (LicDump.string_of_type_eff(type_of_const_eff x))) + (LicDump.string_of_type_eff(Eff.type_of_const x))) ) | _ -> raise(EvalArray_error( sprintf "bad array index, int expected but get a tuple")) @@ -456,9 +456,9 @@ and eval_array_index Rôle : Entrées : - id_solver, slice_info, size du tableau, + Eff.id_solver, slice_info, size du tableau, lxm (source de l'opération slice pour warning) - Sorties : + Eff.Sor : slice_info_eff, i.e. (fisrt,last,step,width) tels que step <> 0 et - si step > 0 alors 0<=first<=last<=sz @@ -467,7 +467,7 @@ and eval_array_index Effets de bord : EvalArray_error msg si pas bon ----------------------------------------------------------------------*) -and eval_array_slice (env : id_solver) (sl : slice_info) (sz : int) (lxm : Lxm.t) = +and eval_array_slice (env : Eff.id_solver) (sl : slice_info) (sz : int) (lxm : Lxm.t) = try let first_ix = eval_array_index env sl.si_first sz lxm in let last_ix = eval_array_index env sl.si_last sz lxm in @@ -478,7 +478,7 @@ and eval_array_slice (env : id_solver) (sl : slice_info) (sz : int) (lxm : Lxm.t | [Int_const_eff s] -> s (* ok *) | [x] -> raise(EvalArray_error( sprintf "bad array step, int expected but get %s" - (LicDump.string_of_type_eff (type_of_const_eff x)))) + (LicDump.string_of_type_eff (Eff.type_of_const x)))) | _ -> raise(EvalArray_error( sprintf "bad array step, int expected but get a tuple")) ) diff --git a/src/evalConst.mli b/src/evalConst.mli index 74d6f609..182b1a53 100644 --- a/src/evalConst.mli +++ b/src/evalConst.mli @@ -1,4 +1,4 @@ -(** Time-stamp: <modified the 27/03/2008 (at 17:09) by Erwan Jahier> *) +(** Time-stamp: <modified the 29/08/2008 (at 10:21) by Erwan Jahier> *) (* @@ -8,10 +8,10 @@ DESCRIPTION : PARAMETRES : Pour avoir qq chose de générique, les fonctions - sont paramétrées par un "id_solver", qui contient deux fonctions : - (voir CompiledData) + sont paramétrées par un "Eff.id_solver", qui contient deux fonctions : + (voir Eff) - type id_solver = { + type Eff.id_solver = { id2const : Ident.idref -> Lxm.t -> const_eff id2type : Ident.idref -> Lxm.t -> const_eff } @@ -21,7 +21,7 @@ FONCTION PRINCIPALE : Elle lève "Compile_error lxm msg" en cas d'erreur. eval_const - (env : id_solver) + (env : Eff.id_solver) (vexp : val_exp) -> const_eff list @@ -33,14 +33,14 @@ FONCTIONS DERIVEES : (permet de pr se qui permet de récupérer l'erreur. eval_array_size - (env : id_solver) + (env : Eff.id_solver) (vexp : val_exp) -> int (N.B. ne renvoie que des taille correctes : > 0) eval_array_index - (env : id_solver) + (env : Eff.id_solver) (vexp : val_exp) (sz : int) -> int @@ -48,7 +48,7 @@ FONCTIONS DERIVEES : (permet de pr (N.B. on doit préciser la taille sz du tableau) eval_array_slice - (env : id_solver) + (env : Eff.id_solver) (sl : slice_info srcflagged) (sz : int) (lxm : Lxm.t) @@ -62,7 +62,7 @@ FONCTIONS DERIVEES : (permet de pr exception EvalArray_error of string -val f : CompiledData.id_solver -> SyntaxTreeCore.val_exp -> CompiledData.const_eff list +val f : Eff.id_solver -> SyntaxTreeCore.val_exp -> Eff.const list (** Rôle : calcule une taille de tableau @@ -76,7 +76,7 @@ val f : CompiledData.id_solver -> SyntaxTreeCore.val_exp -> CompiledData.const_e EvalArray_error "bad array size, type int expected but get <t>" si t pas int EvalArray_error "bad array size <n>" si n <= 0 *) -val eval_array_size : CompiledData.id_solver -> SyntaxTreeCore.val_exp -> int +val eval_array_size : Eff.id_solver -> SyntaxTreeCore.val_exp -> int (** Rôle : @@ -90,7 +90,7 @@ val eval_array_size : CompiledData.id_solver -> SyntaxTreeCore.val_exp -> int Effets de bord : EvalArray_error msg si pas bon *) -val eval_array_index : CompiledData.id_solver -> SyntaxTreeCore.val_exp -> +val eval_array_index : Eff.id_solver -> SyntaxTreeCore.val_exp -> int -> Lxm.t -> int (** @@ -109,5 +109,5 @@ val eval_array_index : CompiledData.id_solver -> SyntaxTreeCore.val_exp -> EvalArray_error msg si pas bon *) val eval_array_slice : - CompiledData.id_solver -> SyntaxTreeCore.slice_info -> int -> Lxm.t -> - CompiledData.slice_info_eff + Eff.id_solver -> SyntaxTreeCore.slice_info -> int -> Lxm.t -> + Eff.slice_info diff --git a/src/evalType.ml b/src/evalType.ml index 5211210e..cd5b3fd9 100644 --- a/src/evalType.ml +++ b/src/evalType.ml @@ -1,4 +1,4 @@ -(** Time-stamp: <modified the 28/08/2008 (at 10:27) by Erwan Jahier> *) +(** Time-stamp: <modified the 29/08/2008 (at 09:23) by Erwan Jahier> *) open Predef @@ -6,14 +6,14 @@ open PredefEvalType open PredefEvalConst open SyntaxTree open SyntaxTreeCore -open CompiledData +open Eff open Printf open Lxm open Errors (******************************************************************************) -(* We tabulate the result of the [val_exp_eff] type ckecking. Note, +(* We tabulate the result of the [Eff.val_exp] type ckecking. Note, that there is no clash in that table because all [var_exp_eff] are srcflagged. *) @@ -22,7 +22,7 @@ let val_exp_eff_type_tab = Hashtbl.create 0 let tabulate_res val_exp_eff type_eff_list = Hashtbl.add val_exp_eff_type_tab val_exp_eff type_eff_list -let (val_exp_eff : val_exp_eff -> type_eff list) = +let (val_exp_eff : Eff.val_exp -> Eff.type_ list) = fun vef -> try Hashtbl.find val_exp_eff_type_tab vef with _ -> assert false @@ -30,7 +30,7 @@ let (val_exp_eff : val_exp_eff -> type_eff list) = (******************************************************************************) let finish_me msg = print_string ("\n\tXXX evalType.ml:"^msg^" -> finish me!\n") -let rec (f : id_solver -> val_exp_eff -> type_eff list) = +let rec (f : Eff.id_solver -> Eff.val_exp -> Eff.type_ list) = fun id_solver ve -> let res = match ve with @@ -48,10 +48,10 @@ let rec (f : id_solver -> val_exp_eff -> type_eff list) = res and (eval_by_pos_type : - id_solver -> by_pos_op_eff -> Lxm.t -> val_exp_eff list -> type_eff list) = + Eff.id_solver -> Eff.by_pos_op -> Lxm.t -> Eff.val_exp list -> Eff.type_ list) = fun id_solver posop lxm args -> match posop with - | Predef_eff (op,sargs) -> ( + | Eff.Predef (op,sargs) -> ( let targs = List.map (f id_solver) args in let res = PredefEvalType.f op lxm sargs targs in (* Handling iterator calls: cf comments in LucDump.mli *) @@ -70,7 +70,7 @@ and (eval_by_pos_type : ); res ) - | CALL_eff node_exp_eff -> + | Eff.CALL 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 let t_args = List.flatten (List.map (f id_solver) args) in @@ -87,17 +87,17 @@ and (eval_by_pos_type : | UnifyType.Ko msg -> raise (Compile_error(lxm, msg)) ) - | CONST_eff (id,_) -> [type_of_const_eff (id_solver.id2const id lxm)] - | IDENT_eff id -> ( + | Eff.CONST (id,_) -> [Eff.type_of_const (id_solver.id2const id lxm)] + | Eff.IDENT id -> ( (* [id] migth be a constant, but also a variable *) - try [type_of_const_eff (id_solver.id2const id lxm)] + try [Eff.type_of_const (id_solver.id2const id lxm)] with _ -> [(id_solver.id2var id lxm).var_type_eff] ) - | WITH_eff(ve) -> f id_solver ve + | Eff.WITH(ve) -> f id_solver ve - | TUPLE_eff -> List.flatten (List.map (f id_solver) args) + | Eff.TUPLE -> List.flatten (List.map (f id_solver) args) - | CONCAT_eff -> ( + | Eff.CONCAT -> ( match List.map (f id_solver) args with | [[Array_type_eff (teff0, size0)]; [Array_type_eff (teff1, size1)]] -> let teff = @@ -111,7 +111,7 @@ and (eval_by_pos_type : raise(EvalType_error(sprintf "arity error: 2 expected instead of %d" (List.length args))) ) - | STRUCT_ACCESS_eff fid -> ( + | Eff.STRUCT_ACCESS fid -> ( let type_args_eff = List.flatten (List.map (f id_solver) args) in match type_args_eff with | [Struct_type_eff (name, fl)] -> ( @@ -125,16 +125,16 @@ and (eval_by_pos_type : | [x] -> type_error [x] "struct type" | x -> arity_error x "1" ) - | ARRAY_ACCES_eff (_, teff) -> [teff] (* XXX check args type! *) + | Eff.ARRAY_ACCES (_, teff) -> [teff] (* XXX check args type! *) - | ARRAY_SLICE_eff (sieff,teff) -> + | Eff.ARRAY_SLICE (sieff,teff) -> [Array_type_eff(teff, sieff.se_width)] - | HAT_eff(size,ceff) -> + | Eff.HAT(size,ceff) -> let teff_list = f id_solver ceff in List.map (fun teff -> Array_type_eff(teff, size)) teff_list - | ARRAY_eff -> + | Eff.ARRAY -> (* check that args are of the same type *) let type_args_eff = (List.map (f id_solver) args) in let teff_elt = @@ -154,8 +154,8 @@ and (eval_by_pos_type : [Array_type_eff(List.hd teff_elt, List.length args)] - | WHENOT_eff _ - | WHEN_eff _ -> ( + | Eff.WHENOT _ + | Eff.WHEN _ -> ( let type_args_eff = List.map (f id_solver) args in match type_args_eff with | [teff; [Bool_type_eff]] @@ -167,30 +167,30 @@ and (eval_by_pos_type : raise(EvalType_error(msg)) | _ -> raise(EvalType_error("arity error (2 args expected)")) ) - | ARROW_eff - | FBY_eff -> ( + | Eff.ARROW + | Eff.FBY -> ( let type_args_eff = List.map (f id_solver) args in match type_args_eff with | [init; teff] -> if init = teff then teff else raise(EvalType_error("type mismatch. ")) | _ -> raise(EvalType_error("arity error (2 args expected)")) ) - | CURRENT_eff - | PRE_eff -> ( + | Eff.CURRENT + | Eff.PRE -> ( let type_args_eff = List.map (f id_solver) args in match type_args_eff with | [teff] -> teff | _ -> raise(EvalType_error("arity error (1 arg expected)")) ) - | MERGE_eff _ -> finish_me "merge"; assert false + | Eff.MERGE _ -> finish_me "merge"; assert false -and (eval_by_name_type : id_solver -> by_name_op_eff -> Lxm.t -> - (Ident.t Lxm.srcflagged * val_exp_eff) list -> type_eff list) = +and (eval_by_name_type : Eff.id_solver -> Eff.by_name_op -> Lxm.t -> + (Ident.t Lxm.srcflagged * Eff.val_exp) list -> Eff.type_ list) = fun id_solver namop lxm namargs -> match namop with - | STRUCT_anonymous_eff -> + | Eff.STRUCT_anonymous -> (* ??? comment faire ici pour recuperer son type ??? il faut que je recherche à l'aide des noms de champs le type structure qui va bien ! @@ -203,5 +203,5 @@ and (eval_by_name_type : id_solver -> by_name_op_eff -> Lxm.t -> assert false (* failwith "Finish me: anonymous struct not yet supported" *) - | STRUCT_eff (pn,opid) -> [id_solver.id2type opid lxm] + | Eff.STRUCT (pn,opid) -> [id_solver.id2type opid lxm] diff --git a/src/evalType.mli b/src/evalType.mli index 61347052..0b46196d 100644 --- a/src/evalType.mli +++ b/src/evalType.mli @@ -1,12 +1,11 @@ -(** Time-stamp: <modified the 18/08/2008 (at 11:21) by Erwan Jahier> *) +(** Time-stamp: <modified the 28/08/2008 (at 15:31) by Erwan Jahier> *) -open CompiledData (** Evaluates the type of an expression. *) -val f : id_solver -> val_exp_eff -> type_eff list +val f : Eff.id_solver -> Eff.val_exp -> Eff.type_ list (* Returns the type of an expression. Note that this function uses an internal table, and therefore it should not be called before the type checking has been done (by the function f above).*) -val val_exp_eff : val_exp_eff -> type_eff list +val val_exp_eff : Eff.val_exp -> Eff.type_ list diff --git a/src/getEff.ml b/src/getEff.ml index 7ea8a6f7..94e4aa81 100644 --- a/src/getEff.ml +++ b/src/getEff.ml @@ -1,11 +1,11 @@ -(** Time-stamp: <modified the 28/08/2008 (at 10:27) by Erwan Jahier> *) +(** Time-stamp: <modified the 29/08/2008 (at 10:40) by Erwan Jahier> *) open Lxm open Predef open SyntaxTree open SyntaxTreeCore -open CompiledData +open Eff open Errors @@ -13,8 +13,7 @@ open Errors exception GetEffType_error of string (* exported *) -let rec (typ:CompiledData.id_solver -> SyntaxTreeCore.type_exp -> - CompiledData.type_eff)= +let rec (typ:Eff.id_solver -> SyntaxTreeCore.type_exp -> Eff.type_) = fun env texp -> try ( match texp.it with @@ -33,7 +32,7 @@ let rec (typ:CompiledData.id_solver -> SyntaxTreeCore.type_exp -> raise (Compile_error(texp.src, "can't eval type: "^msg)) (* exported *) -let rec (clock : CompiledData.id_solver -> var_info -> CompiledData.clock_eff)= +let rec (clock : Eff.id_solver -> SyntaxTreeCore.var_info -> Eff.clock)= fun id_solver v -> match v.var_clock with | Base -> On(v.var_name,BaseEff) @@ -44,13 +43,13 @@ let rec (clock : CompiledData.id_solver -> var_info -> CompiledData.clock_eff)= (******************************************************************************) (* 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 +and (type_check_equation: Eff.id_solver -> Lxm.t -> Eff.left list -> + Eff.val_exp -> unit) = + fun id_solver lxm lpl_eff ve_eff -> + let lpl_teff = List.map Eff.type_of_left 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, + raise (Compile_error(lxm, "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" ^ @@ -65,17 +64,17 @@ and (type_check_equation: id_solver -> eq_info srcflagged -> left_eff list -> "' (left-hand-side) \n*** is not compatible with \n***\t'" ^ (LicDump.string_of_type_eff re) ^ "' (right-hand-side)" in - raise (Compile_error(eq_info.src, msg)) + raise (Compile_error(lxm, 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 -> +and (clock_check_equation:Eff.id_solver -> Lxm.t -> Eff.left list -> + Eff.val_exp -> unit) = + fun id_solver lxm lpl_eff ve_eff -> let right_part,s = EvalClock.f id_solver UnifyClock.empty_subst ve_eff in - EvalClock.check_res eq_info.src s lpl_eff right_part + EvalClock.check_res lxm s lpl_eff right_part (******************************************************************************) @@ -88,8 +87,8 @@ let (get_static_params_from_idref : SymbolTab.t -> Lxm.t -> Ident.idref -> (* exported *) -let rec (node : CompiledData.id_solver -> SyntaxTreeCore.node_exp srcflagged -> - CompiledData.node_exp_eff) = +let rec (node : Eff.id_solver -> SyntaxTreeCore.node_exp srcflagged -> + Eff.node_exp) = fun id_solver { src = lxm; it=(idref, static_args) } -> let static_params = get_static_params_from_idref id_solver.symbols lxm idref in let static_args_eff = @@ -102,12 +101,12 @@ let rec (node : CompiledData.id_solver -> SyntaxTreeCore.node_exp srcflagged -> (** [check_static_arg this pn id sa (symbols, acc)] compile a static arg - into a static_arg_eff + into a static_arg *) -and (check_static_arg : CompiledData.id_solver -> +and (check_static_arg : Eff.id_solver -> SyntaxTreeCore.static_param srcflagged -> SyntaxTreeCore.static_arg srcflagged -> - CompiledData.static_arg_eff) = + Eff.static_arg) = fun node_id_solver sp sa -> let sa_eff = match sa.it, sp.it with @@ -141,7 +140,7 @@ and (check_static_arg : CompiledData.id_solver -> let neff = node node_id_solver ne in NodeStaticArgEff (id, neff) - | StaticArgNode(Predef (op,sargs)), StaticParamNode(id,_,_,_) -> + | StaticArgNode(Predef_n (op,sargs)), StaticParamNode(id,_,_,_) -> let sargs_eff = translate_predef_static_args node_id_solver sargs sa.src in @@ -170,18 +169,18 @@ and (check_static_arg : CompiledData.id_solver -> (* exported *) -and (eq:id_solver -> eq_info srcflagged -> eq_info_eff srcflagged) = +and (eq:Eff.id_solver -> SyntaxTreeCore.eq_info srcflagged -> Eff.eq_info srcflagged) = fun id_solver eq_info -> let (lpl, ve) = eq_info.it in let lpl_eff = List.map (translate_left_part id_solver) lpl and ve_eff = translate_val_exp id_solver ve in - type_check_equation id_solver eq_info lpl_eff ve_eff; - clock_check_equation id_solver eq_info lpl_eff ve_eff; + type_check_equation id_solver eq_info.src lpl_eff ve_eff; + clock_check_equation id_solver eq_info.src lpl_eff ve_eff; flagit (lpl_eff, ve_eff) eq_info.src -and (translate_left_part : id_solver -> left_part -> left_eff) = +and (translate_left_part : id_solver -> SyntaxTreeCore.left_part -> Eff.left) = fun id_solver lp_top -> match lp_top with | LeftVar id -> @@ -192,7 +191,7 @@ and (translate_left_part : id_solver -> left_part -> left_eff) = | LeftField (lp, id) -> ( let lp_eff = translate_left_part id_solver lp in - let teff = CompiledData.type_eff_of_left_eff lp_eff in + let teff = Eff.type_of_left lp_eff in (* check that [lp_eff] is a struct that have a field named [id] *) match teff with | Struct_type_eff(_, fl) -> ( @@ -205,7 +204,7 @@ and (translate_left_part : id_solver -> left_part -> left_eff) = ) | LeftArray (lp, vef) -> ( let lp_eff = translate_left_part id_solver lp in - let teff = CompiledData.type_eff_of_left_eff lp_eff in + let teff = Eff.type_of_left lp_eff in let lxm = vef.src in match teff with | Array_type_eff(teff_elt, size) -> @@ -216,7 +215,7 @@ and (translate_left_part : id_solver -> left_part -> left_eff) = ) | LeftSlice (lp, sif) -> ( let lp_eff = translate_left_part id_solver lp in - let teff = CompiledData.type_eff_of_left_eff lp_eff in + let teff = Eff.type_of_left lp_eff in match teff with | Array_type_eff(teff_elt, size) -> let sieff = translate_slice_info id_solver sif.it size sif.src in @@ -227,7 +226,7 @@ and (translate_left_part : id_solver -> left_part -> left_eff) = ) -and (translate_val_exp : id_solver -> val_exp -> val_exp_eff) = +and (translate_val_exp : Eff.id_solver -> SyntaxTreeCore.val_exp -> Eff.val_exp) = fun id_solver ve -> match ve with | CallByName(by_name_op, field_list) -> @@ -243,15 +242,15 @@ and (translate_val_exp : id_solver -> val_exp -> val_exp_eff) = and translate_by_name_op id_solver op = match op.it with - | STRUCT_anonymous_n -> STRUCT_anonymous_eff + | STRUCT_anonymous_n -> STRUCT_anonymous | STRUCT_n idref -> match Ident.pack_of_idref idref with | None -> (* If no pack name is provided, we lookup it in the symbol table *) let id = Ident.of_idref idref in let pn = SymbolTab.find_pack_of_type id_solver.symbols id op.src in - STRUCT_eff (pn, idref) - | Some pn -> STRUCT_eff (pn, idref) + STRUCT (pn, idref) + | Some pn -> STRUCT (pn, idref) and translate_field id_solver (id, ve) = (id, translate_val_exp id_solver ve) @@ -274,7 +273,7 @@ and get_node id_solver node_or_node_ident lxm = id_solver.id2node id sargs lxm | StaticArgNode(CALL_n ne) -> node id_solver ne - | StaticArgNode(Predef (op,sargs)) -> + | StaticArgNode(Predef_n (op,sargs)) -> let sargs_eff = translate_predef_static_args id_solver sargs lxm in PredefEvalType.make_node_exp_eff None op lxm sargs_eff | StaticArgNode(_) -> assert false @@ -284,8 +283,8 @@ and get_node id_solver node_or_node_ident lxm = (* exported *) -and (translate_predef_static_args: id_solver -> static_arg srcflagged list -> - Lxm.t -> static_arg_eff list) = +and (translate_predef_static_args: Eff.id_solver -> + SyntaxTreeCore.static_arg srcflagged list -> Lxm.t -> Eff.static_arg list) = fun id_solver sargs lxm -> match sargs with | [] -> [] @@ -304,35 +303,36 @@ and (translate_predef_static_args: id_solver -> static_arg srcflagged list -> raise (Compile_error(lxm, "bad arguments number for array iterator")) -and (translate_iteror: id_solver -> by_pos_op -> Lxm.t -> by_pos_op_eff) = +and (translate_iteror: Eff.id_solver -> SyntaxTreeCore.by_pos_op -> Lxm.t -> + Eff.by_pos_op) = fun id_solver op lxm -> match op with - | Predef(iter_op, sargs) -> - Predef_eff(iter_op, translate_predef_static_args id_solver sargs lxm) + | Predef_n(iter_op, sargs) -> + Eff.Predef(iter_op, translate_predef_static_args id_solver sargs lxm) | _ -> assert false -and (translate_by_pos_op : id_solver -> by_pos_op srcflagged -> val_exp list -> - by_pos_op_eff) = +and (translate_by_pos_op : Eff.id_solver -> SyntaxTreeCore.by_pos_op srcflagged -> + SyntaxTreeCore.val_exp list -> Eff.by_pos_op) = fun id_solver {it=by_pos_op;src=lxm} args -> match by_pos_op with (* put that in another module ? yes, see above.*) - | Predef(Map, _) - | Predef(Fill, _) - | Predef(Red, _) - | Predef(FillRed, _) - | Predef(BoolRed, _) -> translate_iteror id_solver by_pos_op lxm + | Predef_n(Map, _) + | Predef_n(Fill, _) + | Predef_n(Red, _) + | Predef_n(FillRed, _) + | Predef_n(BoolRed, _) -> translate_iteror id_solver by_pos_op lxm (* other predef operators *) - | Predef(op, args) -> assert (args=[]); Predef_eff (op,[]) + | Predef_n(op, args) -> assert (args=[]); Predef (op,[]) | CALL_n node_exp_f -> - CALL_eff (flagit (node id_solver node_exp_f) node_exp_f.src) + Eff.CALL (flagit (node id_solver node_exp_f) node_exp_f.src) | IDENT_n idref -> ( try match Ident.pack_of_idref idref with - | Some pn -> IDENT_eff idref + | Some pn -> Eff.IDENT idref (* Constant with a pack name are treated as IDENT_eff. Indeed, I do not see any means to know if an idref denotes a constant or not, since @@ -345,36 +345,36 @@ and (translate_by_pos_op : id_solver -> by_pos_op srcflagged -> val_exp list -> | None -> let id = Ident.of_idref idref in let pn = SymbolTab.find_pack_of_const id_solver.symbols id lxm in - CONST_eff (idref, pn) - with _ -> IDENT_eff idref + Eff.CONST (idref, pn) + with _ -> Eff.IDENT idref ) - | CURRENT_n -> CURRENT_eff - | PRE_n -> PRE_eff - - | ARROW_n -> ARROW_eff - | FBY_n -> FBY_eff - | CONCAT_n -> CONCAT_eff - | TUPLE_n -> TUPLE_eff - | ARRAY_n -> ARRAY_eff + | CURRENT_n -> Eff.CURRENT + | PRE_n -> Eff.PRE + + | ARROW_n -> Eff.ARROW + | FBY_n -> Eff.FBY + | CONCAT_n -> Eff.CONCAT + | TUPLE_n -> Eff.TUPLE + | ARRAY_n -> Eff.ARRAY | WITH_n(c,e1,e2) -> let c_eff = EvalConst.f id_solver c in - if c_eff = [ Bool_const_eff true ] then - WITH_eff (translate_val_exp id_solver e1) + if c_eff = [ Bool_const_eff true ] then + Eff.WITH (translate_val_exp id_solver e1) else - WITH_eff (translate_val_exp id_solver e2) - | STRUCT_ACCESS_n id -> STRUCT_ACCESS_eff id + Eff.WITH (translate_val_exp id_solver e2) + | STRUCT_ACCESS_n id -> Eff.STRUCT_ACCESS id | WHEN_n -> (match List.map (translate_val_exp id_solver) args with - | [_;CallByPosEff({it=IDENT_eff id; src=lxm}, _)] -> + | [_;CallByPosEff({it=Eff.IDENT id; src=lxm}, _)] -> let clk = try (id_solver.id2var id lxm) with _ -> assert false in - WHEN_eff clk + Eff.WHEN clk | [_;CallByPosEff - ({it=Predef_eff(NOT_n,[])}, - OperEff [CallByPosEff({src = lxm; it = IDENT_eff id}, _)])] -> + ({it=Predef(NOT_n,[])}, + OperEff [CallByPosEff({src = lxm; it = Eff.IDENT id}, _)])] -> let clk = try (id_solver.id2var id lxm) with _ -> assert false in - WHENOT_eff clk + Eff.WHENOT clk | _ -> let msg = "syntax error: clock expr expected" in @@ -394,7 +394,7 @@ and (translate_by_pos_op : id_solver -> by_pos_op srcflagged -> val_exp list -> (LicDump.string_of_type_eff_list teff) ^ "' was expected to be an array")) in - ARRAY_ACCES_eff( + Eff.ARRAY_ACCES( EvalConst.eval_array_index id_solver ve_index size lxm, teff_elt ) @@ -413,7 +413,7 @@ and (translate_by_pos_op : id_solver -> by_pos_op srcflagged -> val_exp list -> (LicDump.string_of_type_eff_list teff) ^ "' was expected to be an array")) in - ARRAY_SLICE_eff(EvalConst.eval_array_slice id_solver si size lxm, + Eff.ARRAY_SLICE(EvalConst.eval_array_slice id_solver si size lxm, teff_elt) | HAT_n -> ( @@ -422,24 +422,24 @@ and (translate_by_pos_op : id_solver -> by_pos_op srcflagged -> val_exp list -> let size_const_eff = EvalConst.f id_solver ve_size and exp_eff = translate_val_exp id_solver exp in (match size_const_eff with - | [Int_const_eff size] -> HAT_eff(size, exp_eff) + | [Int_const_eff size] -> Eff.HAT(size, exp_eff) | _ -> assert false) | _ -> assert false ) - | MERGE_n(id, idl) -> MERGE_eff(id, idl) + | MERGE_n(id, idl) -> Eff.MERGE(id, idl) -and (translate_slice_info : id_solver -> slice_info -> int -> Lxm.t -> - slice_info_eff) = +and (translate_slice_info : Eff.id_solver -> SyntaxTreeCore.slice_info -> int -> + Lxm.t -> Eff.slice_info) = fun id_solver si size lxm -> EvalConst.eval_array_slice id_solver si size lxm (**********************************************************************************) (* exported *) -let (assertion : CompiledData.id_solver -> SyntaxTreeCore.val_exp Lxm.srcflagged -> - CompiledData.val_exp_eff Lxm.srcflagged) = +let (assertion : Eff.id_solver -> SyntaxTreeCore.val_exp Lxm.srcflagged -> + Eff.val_exp Lxm.srcflagged) = fun id_solver vef -> let val_exp_eff = translate_val_exp id_solver vef.it in (* Check that the assert is a bool. *) diff --git a/src/getEff.mli b/src/getEff.mli index 05c936cd..6cbbee90 100644 --- a/src/getEff.mli +++ b/src/getEff.mli @@ -1,8 +1,8 @@ -(** Time-stamp: <modified the 19/08/2008 (at 14:35) by Erwan Jahier> *) +(** Time-stamp: <modified the 29/08/2008 (at 09:28) by Erwan Jahier> *) (** This module defines functions that translate SyntaxTreeCore datatypes into - CompiledData one. + Eff ones. Basically, it @@ -13,8 +13,8 @@ - checks the arguments and the parameters are compatible (i.e., that they unify) *) -val typ : CompiledData.id_solver -> SyntaxTreeCore.type_exp -> CompiledData.type_eff -val clock: CompiledData.id_solver -> SyntaxTreeCore.var_info -> CompiledData.clock_eff +val typ : Eff.id_solver -> SyntaxTreeCore.type_exp -> Eff.type_ +val clock: Eff.id_solver -> SyntaxTreeCore.var_info -> Eff.clock (** A [node_exp] is a name plus a list of static arguments. @@ -24,17 +24,17 @@ val clock: CompiledData.id_solver -> SyntaxTreeCore.var_info -> CompiledData.clo - check they are compatible with the node signature check the type of the static arguments ( *) -val node : CompiledData.id_solver -> SyntaxTreeCore.node_exp Lxm.srcflagged -> - CompiledData.node_exp_eff +val node : Eff.id_solver -> SyntaxTreeCore.node_exp Lxm.srcflagged -> + Eff.node_exp -val eq : CompiledData.id_solver -> SyntaxTreeCore.eq_info Lxm.srcflagged -> - CompiledData.eq_info_eff Lxm.srcflagged +val eq : Eff.id_solver -> SyntaxTreeCore.eq_info Lxm.srcflagged -> + Eff.eq_info Lxm.srcflagged -val assertion : CompiledData.id_solver -> SyntaxTreeCore.val_exp Lxm.srcflagged -> - CompiledData.val_exp_eff Lxm.srcflagged +val assertion : Eff.id_solver -> SyntaxTreeCore.val_exp Lxm.srcflagged -> + Eff.val_exp Lxm.srcflagged (** Useful to type check node aliased by array iterators *) val translate_predef_static_args: - CompiledData.id_solver -> SyntaxTreeCore.static_arg Lxm.srcflagged list -> - Lxm.t -> CompiledData.static_arg_eff list + Eff.id_solver -> SyntaxTreeCore.static_arg Lxm.srcflagged list -> + Lxm.t -> Eff.static_arg list diff --git a/src/iteratorSemantic.ml b/src/iteratorSemantic.ml deleted file mode 100644 index 69ad7c1c..00000000 --- a/src/iteratorSemantic.ml +++ /dev/null @@ -1,21 +0,0 @@ - - - - - -(*********************************************************************************) -let (check_iterator_args : CompiledData.id_solver -> Predef.op -> - static_arg srcflagged list -> static_arg_eff list) = - fun id_solver op args -> - match op,args with - | Map,_ -> assert false - | Fill,_ -> assert false - | Red,_ -> assert false - | MapRed, [{src=lxm_n;it=StaticArgNode(n)}; {src=lxm_c;it=StaticArgConst(c)}] -> - let neff = GetEff.node id_solver {src=lxm_n; it=n } in - let ceff = List.hd (EvalConst.f id_solver c) in - [NodeStaticArgEff(Ident.of_string "mapnode", neff); - ConstStaticArgEff(Ident.of_string "mapsize", ceff)] - | MapRed, _ -> failwith "bad arguments for mapred" - | BoolRed,_ ->assert false - diff --git a/src/iteratorSemantic.mli b/src/iteratorSemantic.mli deleted file mode 100644 index ae217094..00000000 --- a/src/iteratorSemantic.mli +++ /dev/null @@ -1 +0,0 @@ -val check_iterator_args : CompiledData.id_solver -> Predef.op diff --git a/src/lazyCompiler.ml b/src/lazyCompiler.ml index df7dcd32..bdad0868 100644 --- a/src/lazyCompiler.ml +++ b/src/lazyCompiler.ml @@ -1,11 +1,11 @@ -(** Time-stamp: <modified the 28/08/2008 (at 11:12) by Erwan Jahier> *) +(** Time-stamp: <modified the 29/08/2008 (at 10:48) by Erwan Jahier> *) open Lxm open Errors open SyntaxTree open SyntaxTreeCore -open CompiledData +open Eff let finish_me msg = print_string ("\n\tXXX LazyCompiler:"^msg^" -> finish me!\n") @@ -34,13 +34,13 @@ let recursion_error (lxm : Lxm.t) (stack : string list) = type t = { src_tab : SyntaxTab.t; (* table des defs *) - types : (item_key, CompiledData.type_eff check_flag) Hashtbl.t; - consts : (item_key, CompiledData.const_eff check_flag) Hashtbl.t; - nodes : (node_key, CompiledData.node_exp_eff check_flag) Hashtbl.t; + types : (Eff.item_key, Eff.type_ Eff.check_flag) Hashtbl.t; + consts : (Eff.item_key, Eff.const Eff.check_flag) Hashtbl.t; + nodes : (Eff.node_key, Eff.node_exp Eff.check_flag) Hashtbl.t; (* table des prov *) - prov_types : (item_key, CompiledData.type_eff check_flag) Hashtbl.t; - prov_consts : (item_key, CompiledData.const_eff check_flag) Hashtbl.t; - prov_nodes : (node_key, CompiledData.node_exp_eff check_flag) Hashtbl.t + prov_types : (Eff.item_key, Eff.type_ Eff.check_flag) Hashtbl.t; + prov_consts : (Eff.item_key, Eff.const Eff.check_flag) Hashtbl.t; + prov_nodes : (Eff.node_key, Eff.node_exp Eff.check_flag) Hashtbl.t } (******************************************************************************) @@ -123,7 +123,7 @@ fun tbl -> - [solve_x_idref] - o takes an idref (plus a «static_arg_eff list» for x=node!) + o takes an idref (plus a «Eff.static_arg list» for x=node!) o perform name resolution o calls [x_check] (loop!) @@ -149,7 +149,7 @@ let x_check tab find_x x_check_do lookup_x_eff pack_of_x_key name_of_x_key this x_key lxm = try lookup_x_eff tab x_key lxm with Not_found -> - Hashtbl.add tab x_key Checking; + Hashtbl.add tab x_key Eff.Checking; let (x_pack,xn) = (pack_of_x_key x_key, name_of_x_key x_key) in let x_pack_symbols = SyntaxTab.pack_body_env this.src_tab x_pack in let x_def = match find_x x_pack_symbols xn lxm with @@ -160,7 +160,7 @@ let x_check assert false (* should not occur *) in let res = x_check_do this x_key lxm x_pack_symbols false x_pack x_def in - Hashtbl.replace tab x_key (Checked res); + Hashtbl.replace tab x_key (Eff.Checked res); res let x_check_interface @@ -168,7 +168,7 @@ let x_check_interface pack_of_x_key name_of_x_key this x_key lxm = try lookup_x_eff tab x_key lxm with Not_found -> - Hashtbl.add tab x_key Checking; + Hashtbl.add tab x_key Eff.Checking; let (xp,xn) = (pack_of_x_key x_key, name_of_x_key x_key) in let xp_prov_symbols_opt = SyntaxTab.pack_prov_env this.src_tab xp lxm in let res = (* [xp] migth have no provided symbol table *) @@ -183,29 +183,29 @@ let x_check_interface in x_check_interface_do this x_key lxm xp_prov_symbols xp x_def in - Hashtbl.replace tab x_key (Checked res); + Hashtbl.replace tab x_key (Eff.Checked res); res (* Returns the tabulated [type] or [const], if it has already been computed; otherwise, raise [Not_found] otherwise. *) let lookup_x_eff x_label id_of_x_key x_tab x_key lxm = match Hashtbl.find x_tab x_key with - | Checked res -> res - | Checking -> + | Eff.Checked res -> res + | Eff.Checking -> raise (Recursion_error (id_of_x_key x_key, [x_label^(Lxm.details lxm)])) - | Incorrect -> raise (BadCheckRef_error) + | Eff.Incorrect -> raise (BadCheckRef_error) -let (lookup_type_eff: (item_key, CompiledData.type_eff check_flag) Hashtbl.t -> - Ident.long -> Lxm.t -> CompiledData.type_eff) = +let (lookup_type_eff: (Eff.item_key, Eff.type_ Eff.check_flag) Hashtbl.t -> + Ident.long -> Lxm.t -> Eff.type_) = lookup_x_eff "type ref " (fun k -> k) -let (lookup_const_eff:(item_key, CompiledData.const_eff check_flag) Hashtbl.t -> - Ident.long -> Lxm.t -> CompiledData.const_eff) = +let (lookup_const_eff:(Eff.item_key, Eff.const Eff.check_flag) Hashtbl.t -> + Ident.long -> Lxm.t -> Eff.const) = lookup_x_eff "const ref " (fun k -> k) let (lookup_node_exp_eff: - (CompiledData.node_key, CompiledData.node_exp_eff check_flag) Hashtbl.t -> - CompiledData.node_key -> Lxm.t -> CompiledData.node_exp_eff) = + (Eff.node_key, Eff.node_exp Eff.check_flag) Hashtbl.t -> + Eff.node_key -> Lxm.t -> Eff.node_exp) = lookup_x_eff "node ref " (fun k -> fst k) @@ -243,26 +243,26 @@ let solve_x_idref (* And now we can start the big mutually recursive definition... *) (** Tabulated version of [type_check_do]. *) -let rec (type_check : t -> Ident.long -> Lxm.t -> CompiledData.type_eff) = +let rec (type_check : t -> Ident.long -> Lxm.t -> Eff.type_) = fun this -> x_check this.types SymbolTab.find_type type_check_do lookup_type_eff Ident.pack_of_long Ident.of_long this (** Tabulated version of [const_check_do]. *) -and (const_check : t -> Ident.long -> Lxm.t -> CompiledData.const_eff) = +and (const_check : t -> Ident.long -> Lxm.t -> Eff.const) = fun this -> x_check this.consts SymbolTab.find_const const_check_do lookup_const_eff Ident.pack_of_long Ident.of_long this (** Tabulated version of [type_check_interface_do]. *) -and (type_check_interface: t -> Ident.long -> Lxm.t -> CompiledData.type_eff) = +and (type_check_interface: t -> Ident.long -> Lxm.t -> Eff.type_) = fun this -> x_check_interface this.prov_types SymbolTab.find_type type_check type_check_interface_do lookup_type_eff Ident.pack_of_long Ident.of_long this (** Tabulated version of [const_check_interface_do]. *) -and (const_check_interface: t -> Ident.long -> Lxm.t -> CompiledData.const_eff) = +and (const_check_interface: t -> Ident.long -> Lxm.t -> Eff.const) = fun this -> x_check_interface this.prov_consts SymbolTab.find_const const_check const_check_interface_do @@ -270,7 +270,7 @@ and (const_check_interface: t -> Ident.long -> Lxm.t -> CompiledData.const_eff) (** solving type and constant references *) and (solve_type_idref : t -> SymbolTab.t -> bool -> Ident.pack_name -> - Ident.idref -> Lxm.t -> CompiledData.type_eff) = + Ident.idref -> Lxm.t -> Eff.type_) = fun this symbols provide_flag currpack idr lxm -> solve_x_idref type_check_interface type_check SymbolTab.find_type "type" @@ -278,7 +278,7 @@ and (solve_type_idref : t -> SymbolTab.t -> bool -> Ident.pack_name -> this symbols provide_flag currpack idr [] lxm and (solve_const_idref : t -> SymbolTab.t -> bool -> Ident.pack_name -> - Ident.idref -> Lxm.t -> CompiledData.const_eff) = + Ident.idref -> Lxm.t -> Eff.const) = fun this symbols provide_flag currpack idr lxm -> solve_x_idref const_check_interface const_check SymbolTab.find_const "const" @@ -289,7 +289,7 @@ and (solve_const_idref : t -> SymbolTab.t -> bool -> Ident.pack_name -> (* now the real work! *) and (type_check_interface_do: t -> Ident.long -> Lxm.t -> SymbolTab.t -> Ident.pack_name -> SyntaxTreeCore.type_info srcflagged -> - CompiledData.type_eff) = + Eff.type_) = fun this type_name lxm prov_symbols pack_name type_def -> (* We type check the interface and the body. For non-abstract types, we also check that both effective types are @@ -298,7 +298,7 @@ and (type_check_interface_do: t -> Ident.long -> Lxm.t -> SymbolTab.t -> let prov_type_eff = type_check_do this type_name lxm prov_symbols true pack_name type_def in - if CompiledData.type_eff_are_compatible prov_type_eff body_type_eff then + if Eff.type_are_compatible prov_type_eff body_type_eff then prov_type_eff else raise(Compile_error ( @@ -311,18 +311,18 @@ and (type_check_interface_do: t -> Ident.long -> Lxm.t -> SymbolTab.t -> and (const_check_interface_do: t -> Ident.long -> Lxm.t -> SymbolTab.t -> Ident.pack_name -> SyntaxTreeCore.const_info srcflagged -> - CompiledData.const_eff) = + Eff.const) = fun this cn lxm prov_symbols p const_def -> let prov_const_eff = const_check_do this cn lxm prov_symbols true p const_def in let body_const_eff = const_check this cn lxm in match prov_const_eff with - | Extern_const_eff (id, teff_prov, v_opt) -> - let teff_body = type_of_const_eff body_const_eff in + | Eff.Extern_const_eff (id, teff_prov, v_opt) -> + let teff_body = Eff.type_of_const body_const_eff in if (id <> cn) then assert false else if v_opt <> None && v_opt <> Some(body_const_eff) then raise(Compile_error (const_def.src, " constant values mismatch")) - else if CompiledData.type_eff_are_compatible teff_prov teff_body then + else if Eff.type_are_compatible teff_prov teff_body then prov_const_eff else raise(Compile_error ( @@ -332,12 +332,12 @@ and (const_check_interface_do: t -> Ident.long -> Lxm.t -> SymbolTab.t -> " is not compatible with its implementation \n***\t" ^ (LicDump.string_of_type_eff teff_body) ^ "") )) - | Enum_const_eff (_, _) - | Bool_const_eff _ - | Int_const_eff _ - | Real_const_eff _ - | Struct_const_eff (_,_) - | Array_const_eff (_,_) + | Eff.Enum_const_eff (_, _) + | Eff.Bool_const_eff _ + | Eff.Int_const_eff _ + | Eff.Real_const_eff _ + | Eff.Struct_const_eff (_,_) + | Eff.Array_const_eff (_,_) -> if prov_const_eff = body_const_eff then body_const_eff @@ -349,7 +349,7 @@ and (const_check_interface_do: t -> Ident.long -> Lxm.t -> SymbolTab.t -> and (type_check_do: t -> Ident.long -> Lxm.t -> SymbolTab.t -> bool -> Ident.pack_name -> SyntaxTreeCore.type_info srcflagged -> - CompiledData.type_eff) = + Eff.type_) = fun this type_name lxm symbols provide_flag pack_name type_def -> try ( (* Solveur d'idref pour les appels à eval_type/eval_const *) @@ -381,7 +381,7 @@ and (type_check_do: t -> Ident.long -> Lxm.t -> SymbolTab.t -> bool -> let veff = EvalConst.f id_solver vexp in match veff with | [v] -> ( - let tv = type_of_const_eff v in + let tv = Eff.type_of_const v in if (tv = teff) then (fname, (teff, Some v)) else raise (Compile_error(field_def.src, Printf.sprintf @@ -413,7 +413,7 @@ and (type_check_do: t -> Ident.long -> Lxm.t -> SymbolTab.t -> bool -> and (const_check_do : t -> Ident.long -> Lxm.t -> SymbolTab.t -> bool -> Ident.pack_name -> SyntaxTreeCore.const_info srcflagged -> - CompiledData.const_eff) = + Eff.const) = fun this cn lxm symbols provide_flag currpack const_def -> (* [cn] and [lxm] are used for recursion errors. [symbols] is the current symbol table. @@ -451,7 +451,7 @@ and (const_check_do : t -> Ident.long -> Lxm.t -> SymbolTab.t -> bool -> | None -> ceff | Some texp -> ( let tdecl = GetEff.typ id_solver texp in - let teff = type_of_const_eff ceff in + let teff = Eff.type_of_const ceff in if (tdecl = teff ) then ceff else raise (Compile_error (const_def.src, Printf.sprintf @@ -477,9 +477,9 @@ and (const_check_do : t -> Ident.long -> Lxm.t -> SymbolTab.t -> bool -> (******************************************************************************) -and (node_check_interface_do: t -> CompiledData.node_key -> Lxm.t -> +and (node_check_interface_do: t -> Eff.node_key -> Lxm.t -> SymbolTab.t -> Ident.pack_name -> SyntaxTreeCore.node_info srcflagged -> - CompiledData.node_exp_eff) = + Eff.node_exp) = fun this nk lxm symbols pn node_def -> let body_node_exp_eff = node_check this nk lxm in let prov_node_exp_eff = node_check_do this nk lxm symbols true pn node_def in @@ -491,7 +491,7 @@ and (node_check_interface_do: t -> CompiledData.node_key -> Lxm.t -> " is not compatible with its implementation: ") in let str_of_var = LicDump.type_string_of_var_info_eff in - let type_is_not_comp v1 v2 = not (CompiledData.var_eff_are_compatible v1 v2) in + let type_is_not_comp v1 v2 = not (Eff.var_are_compatible v1 v2) in if prov_node_exp_eff.node_key_eff <> body_node_exp_eff.node_key_eff then @@ -534,9 +534,9 @@ and (node_check_interface_do: t -> CompiledData.node_key -> Lxm.t -> prov_node_exp_eff -and (node_check_do: t -> CompiledData.node_key -> Lxm.t -> SymbolTab.t -> +and (node_check_do: t -> Eff.node_key -> Lxm.t -> SymbolTab.t -> bool -> Ident.pack_name -> SyntaxTreeCore.node_info srcflagged -> - CompiledData.node_exp_eff) = + Eff.node_exp) = fun this nk lxm symbols provide_flag pack_name node_def -> let lxm = node_def.src in let local_env = make_local_env nk in @@ -677,10 +677,7 @@ and (node_check_do: t -> CompiledData.node_key -> Lxm.t -> SymbolTab.t -> lxm = lxm; } in - let is_a_predef_node n = - Ident.pack_name_to_string (Ident.pack_of_long (fst n.node_key_eff)) = "Lustre" - in - let (make_alias_node : CompiledData.node_exp_eff -> CompiledData.node_exp_eff) = + let (make_alias_node : Eff.node_exp -> Eff.node_exp) = fun aliased_node -> (* builds a node that calls the aliased node. It looks like: node alias_node( ins ) returns ( outs ); @@ -688,16 +685,16 @@ and (node_check_do: t -> CompiledData.node_key -> Lxm.t -> SymbolTab.t -> outs = aliased_node(ins); tel *) - let (outs:left_eff list) = + let (outs:Eff.left list) = List.map (fun vi -> LeftVarEff (vi, lxm)) aliased_node.outlist_eff - and (aliased_node_call : val_exp_eff) = + and (aliased_node_call : Eff.val_exp) = CallByPosEff( - (Lxm.flagit (CALL_eff(Lxm.flagit aliased_node lxm)) lxm, + (Lxm.flagit (Eff.CALL(Lxm.flagit aliased_node lxm)) lxm, OperEff (List.map (fun vi -> (* build operands*) CallByPosEff( - Lxm.flagit (IDENT_eff + Lxm.flagit (Eff.IDENT (Ident.to_idref vi.var_name_eff)) lxm, OperEff []) ) aliased_node.inlist_eff))) @@ -735,22 +732,22 @@ and (node_check_do: t -> CompiledData.node_key -> Lxm.t -> SymbolTab.t -> | Alias({it= alias;src=lxm}) -> ( let aliased_node = match alias with - | Predef((Predef.NOR_n|Predef.DIESE_n), sargs) -> + | Predef_n((Predef.NOR_n|Predef.DIESE_n), sargs) -> raise (Compile_error (lxm, "Can not alias 'nor' nor '#', sorry")) -(* | Predef( *) +(* | Predef_n( *) (* (Predef.NEQ_n | Predef.EQ_n | Predef.LT_n | Predef.LTE_n *) (* | Predef.GT_n | Predef.GTE_n | Predef.IF_n), _sargs *) (* ) -> *) (* raise (Compile_error ( *) (* lxm, "can not alias polymorphic operators, sorry")) *) -(* | Predef( *) +(* | Predef_n( *) (* ( Predef.UMINUS_n | Predef.MINUS_n | Predef.PLUS_n *) (* | Predef.TIMES_n | Predef.SLASH_n), _sargs *) (* ) -> *) (* raise (Compile_error ( *) (* lxm, "can not alias overloaded operators, sorry")) *) - | Predef(predef_op, sargs) -> + | Predef_n(predef_op, sargs) -> let sargs_eff = GetEff.translate_predef_static_args node_id_solver sargs lxm in @@ -777,7 +774,7 @@ and (node_check_do: t -> CompiledData.node_key -> Lxm.t -> SymbolTab.t -> in let aux vi = GetEff.typ node_id_solver vi.it.var_type in - let (il,ol) = CompiledData.profile_of_node_exp_eff alias_node in + let (il,ol) = Eff.profile_of_node_exp alias_node in let (il_exp, ol_exp) = List.map aux vi_il, List.map aux vi_ol in match UnifyType.f il_exp il with | UnifyType.Ko msg -> raise(Compile_error(lxm, msg)) @@ -798,20 +795,20 @@ and (node_check_do: t -> CompiledData.node_key -> Lxm.t -> SymbolTab.t -> (** builds a [node_key] and calls [node_check] *) and (solve_node_idref : t -> SymbolTab.t -> bool -> Ident.pack_name -> Ident.idref -> - static_arg_eff list -> Lxm.t -> CompiledData.node_exp_eff) = + Eff.static_arg list -> Lxm.t -> Eff.node_exp) = fun this symbols provide_flag currpack idr sargs lxm -> solve_x_idref node_check_interface node_check SymbolTab.find_node "node" (fun p id -> (* builds a [node_key] from a [pack_name] and a [node] id, - and a static_arg_eff list *) + and a Eff.static_arg list *) let long = Ident.make_long p id in let node_key = long, sargs in node_key ) this symbols provide_flag currpack idr sargs lxm -and (node_check: t -> CompiledData.node_key -> Lxm.t -> CompiledData.node_exp_eff) = +and (node_check: t -> Eff.node_key -> Lxm.t -> Eff.node_exp) = fun this nk -> x_check this.nodes SymbolTab.find_node node_check_do lookup_node_exp_eff (fun nk -> Ident.pack_of_long (fst nk)) @@ -819,7 +816,7 @@ and (node_check: t -> CompiledData.node_key -> Lxm.t -> CompiledData.node_exp_ef this nk and (node_check_interface: - t -> CompiledData.node_key -> Lxm.t -> CompiledData.node_exp_eff) = + t -> Eff.node_key -> Lxm.t -> Eff.node_exp) = fun this nk -> x_check_interface this.prov_nodes SymbolTab.find_node node_check node_check_interface_do lookup_node_exp_eff @@ -868,7 +865,7 @@ let compile_all_nodes pack_name this id ni_f = else compile_all_item this "node" node_check_interface (LicDump.string_of_node_key_rec) - CompiledData.profile_of_node_exp_eff + Eff.profile_of_node_exp (fun id -> (Ident.make_long pack_name id, [])) id ni_f diff --git a/src/lazyCompiler.mli b/src/lazyCompiler.mli index 70e3f8d1..fe8d1fbf 100644 --- a/src/lazyCompiler.mli +++ b/src/lazyCompiler.mli @@ -1,4 +1,4 @@ -(** Time-stamp: <modified the 12/03/2008 (at 14:15) by Erwan Jahier> *) +(** Time-stamp: <modified the 28/08/2008 (at 17:01) by Erwan Jahier> *) (** nb: compiling = type checking + constant evaluation *) @@ -15,7 +15,7 @@ val create : SyntaxTab.t -> t (** Compiles one node *) -val node_check : t -> CompiledData.node_key -> Lxm.t -> CompiledData.node_exp_eff +val node_check : t -> Eff.node_key -> Lxm.t -> Eff.node_exp (* compile all items *) diff --git a/src/licDump.ml b/src/licDump.ml index 57083413..94a9f6d1 100644 --- a/src/licDump.ml +++ b/src/licDump.ml @@ -1,8 +1,8 @@ -(** Time-stamp: <modified the 28/08/2008 (at 10:22) by Erwan Jahier> *) +(** Time-stamp: <modified the 28/08/2008 (at 17:25) by Erwan Jahier> *) -open CompiledData open Printf open Lxm +open Eff let (long : Ident.long -> string) = Ident.string_of_long (* fun id -> *) @@ -14,8 +14,8 @@ let type_alias_table = Hashtbl.create 0 (******************************************************************************) (* exported *) type tab_elt = - | OpProfile of type_eff list * type_eff list - | Subst of type_eff + | OpProfile of Eff.type_ list * Eff.type_ list + | Subst of Eff.type_ let (polymorph_op_tab: (Lxm.t, tab_elt) Hashtbl.t) = Hashtbl.create 0 @@ -52,8 +52,8 @@ let last_poly_var = ref Int_type_eff (* This table associates to node its definition plus a flag indicating if that node has been generated. *) -type node_profile = CompiledData.type_eff list * CompiledData.type_eff list -let (node_alias_tbl : (string, node_exp_eff * tab_elt option * bool) Hashtbl.t) = +type node_profile = Eff.type_ list * Eff.type_ list +let (node_alias_tbl : (string, Eff.node_exp * tab_elt option * bool) Hashtbl.t) = Hashtbl.create 0 let alias_fresh_var_cpt = ref 0 let create_alias_name long = @@ -76,16 +76,16 @@ let rec string_of_const_eff = ( | Extern_const_eff (s,t,vopt) -> (long s) ^ (string_of_const_eff_opt vopt) | Enum_const_eff (s,t) -> (long s) | Struct_const_eff (fl, t) -> ( - let string_of_field = - function (id, veff) -> - (Ident.to_string id)^" = "^(string_of_const_eff veff) - in - let flst = List.map string_of_field fl in - (string_of_type_eff t)^"{"^(String.concat "; " flst)^"}" + let string_of_field = + function (id, veff) -> + (Ident.to_string id)^" = "^(string_of_const_eff veff) + in + let flst = List.map string_of_field fl in + (string_of_type_eff t)^"{"^(String.concat "; " flst)^"}" ) | Array_const_eff (ctab, t) -> ( - let vl = Array.to_list(Array.map string_of_const_eff ctab) in - "["^(String.concat ", " vl)^"]" + let vl = Array.to_list(Array.map string_of_const_eff ctab) in + "["^(String.concat ", " vl)^"]" ) ) @@ -106,15 +106,15 @@ and string_def_of_type_eff = function | Struct_type_eff (name, fl) -> assert (fl <>[]); let f sep acc (id, (type_eff, const_eff_opt)) = - acc ^ sep ^ (Ident.to_string id) ^ " : " ^ - (string_of_type_eff type_eff) ^ - match const_eff_opt with - None -> "" - | Some ce -> " = " ^ (string_of_const_eff ce) + acc ^ sep ^ (Ident.to_string id) ^ " : " ^ + (string_of_type_eff type_eff) ^ + match const_eff_opt with + None -> "" + | Some ce -> " = " ^ (string_of_const_eff ce) in "struct " ^ - (List.fold_left (f "; ") (f "" " {" (List.hd fl)) (List.tl fl)) ^ "}" - + (List.fold_left (f "; ") (f "" " {" (List.hd fl)) (List.tl fl)) ^ "}" + | Any -> "a" | Overload -> "o" @@ -155,7 +155,7 @@ and string_of_type_eff = function at the top of this file). *) -and (array_alias : type_eff -> int -> string) = +and (array_alias : Eff.type_ -> int -> string) = fun t size -> let array_t = Array_type_eff(t,size) in try @@ -224,7 +224,7 @@ and (dump_node_alias : out_channel -> unit) = (******************************************************************************) (* exported *) -and (type_eff_list_to_string :type_eff list -> string) = +and (type_eff_list_to_string : Eff.type_ list -> string) = fun tel -> let str_l = List.map string_of_type_eff tel in String.concat "*" str_l @@ -241,27 +241,27 @@ and string_of_node_key_rec (nkey: node_key) = match nkey with | (ik, []) -> long ik | (ik, salst) -> - let astrings = List.map static_arg2string_rec salst in - sprintf "%s_%s" (long ik) (String.concat "_" astrings) + let astrings = List.map static_arg2string_rec salst in + sprintf "%s_%s" (long ik) (String.concat "_" astrings) (* for printing iterators *) and string_of_node_key_iter lxm (nkey: node_key) = match nkey with | (ik, []) -> long ik | (ik, salst) -> - let astrings = List.map (static_arg2string (Some lxm)) salst in - sprintf "%s<<%s>>" (long ik) (String.concat ", " astrings) + let astrings = List.map (static_arg2string (Some lxm)) salst in + sprintf "%s<<%s>>" (long ik) (String.concat ", " astrings) (* for printing recursive node *) -and static_arg2string_rec (sa : static_arg_eff) = +and static_arg2string_rec (sa : Eff.static_arg) = match sa with | ConstStaticArgEff (id, ceff) -> sprintf "%s" (string_of_const_eff ceff) | TypeStaticArgEff (id, teff) -> sprintf "%s" (string_of_type_eff teff) | NodeStaticArgEff (id, opeff) -> - sprintf "%s" (string_of_node_key_rec opeff.node_key_eff) + sprintf "%s" (string_of_node_key_rec opeff.node_key_eff) (* for printing iterators *) -and static_arg2string lxm_opt (sa : static_arg_eff) = +and static_arg2string lxm_opt (sa : Eff.static_arg) = match sa with | ConstStaticArgEff (id, ceff) -> sprintf "%s" (string_of_const_eff ceff) | TypeStaticArgEff (id, teff) -> sprintf "%s" (string_of_type_eff teff) @@ -269,7 +269,7 @@ and static_arg2string lxm_opt (sa : static_arg_eff) = if (snd opeff.node_key_eff) = [] then - sprintf "%s" (string_of_node_key_iter opeff.lxm opeff.node_key_eff) + sprintf "%s" (string_of_node_key_iter opeff.lxm opeff.node_key_eff) else let np = match lxm_opt with @@ -280,11 +280,11 @@ and static_arg2string lxm_opt (sa : static_arg_eff) = Hashtbl.add node_alias_tbl alias (opeff, np, false); sprintf "%s" alias -and (string_of_var_info_eff: var_info_eff -> string) = +and (string_of_var_info_eff: Eff.var_info -> string) = fun x -> (Ident.to_string x.var_name_eff) ^ ":"^(string_of_type_eff x.var_type_eff) -and (type_string_of_var_info_eff: var_info_eff -> string) = +and (type_string_of_var_info_eff: Eff.var_info -> string) = fun x -> (string_of_type_eff x.var_type_eff) ^ (string_of_clock2 x.var_clock_eff) @@ -293,7 +293,7 @@ and string_of_decl var_info_eff = (string_of_type_eff var_info_eff.var_type_eff) ^ (string_of_clock var_info_eff.var_clock_eff) -and (string_of_type_decl_list : var_info_eff list -> string -> string) = +and (string_of_type_decl_list : Eff.var_info list -> string -> string) = fun tel sep -> let str = String.concat sep (List.map string_of_decl tel) in str @@ -305,14 +305,14 @@ and string_of_slice_info_eff si_eff = (if si_eff.se_step = 1 then "" else " step " ^ (string_of_int si_eff.se_step)) ^ "]" -and (string_of_leff : left_eff -> string) = +and (string_of_leff : Eff.left -> string) = function | LeftVarEff (vi_eff,_) -> Ident.to_string vi_eff.var_name_eff | LeftFieldEff(leff,id,_) -> (string_of_leff leff) ^ "." ^ (Ident.to_string id) | LeftArrayEff(leff,i,_) -> (string_of_leff leff) ^ "[" ^ (string_of_int i) ^ "]" | LeftSliceEff(leff,si,_) -> (string_of_leff leff) ^ (string_of_slice_info_eff si) -and (string_of_leff_list : left_eff list -> string) = +and (string_of_leff_list : Eff.left list -> string) = fun l -> (if List.length l = 1 then "" else "(") ^ (String.concat ", " (List.map string_of_leff l)) ^ @@ -321,7 +321,7 @@ and (string_of_leff_list : left_eff list -> string) = -and (string_of_by_pos_op_eff: by_pos_op_eff srcflagged -> val_exp_eff list -> string) = +and (string_of_by_pos_op_eff: Eff.by_pos_op srcflagged -> Eff.val_exp list -> string) = fun posop vel -> let tuple vel = (String.concat ", " (List.map string_of_val_exp_eff vel)) in let tuple_par vel = "(" ^ (tuple vel) ^ ")" in @@ -331,22 +331,22 @@ and (string_of_by_pos_op_eff: by_pos_op_eff srcflagged -> val_exp_eff list -> st let lxm = posop.src in let str = match posop.it,vel with - | Predef_eff (Predef.IF_n,_), [ve1; ve2; ve3] -> - " if " ^ (string_of_val_exp_eff ve1) ^ - " then " ^ (string_of_val_exp_eff ve2) ^ - " else " ^ (string_of_val_exp_eff ve3) - - | Predef_eff(op,sargs), vel -> - if Predef.is_infix op then ( - match vel with - | [ve1; ve2] -> - (string_of_val_exp_eff ve1) ^ " " ^ (Predef.op2string op) ^ - " " ^ (string_of_val_exp_eff ve2) - | _ -> assert false - ) - else - ((Predef.op2string op) ^ - (if sargs = [] then + | Predef (Predef.IF_n,_), [ve1; ve2; ve3] -> + " if " ^ (string_of_val_exp_eff ve1) ^ + " then " ^ (string_of_val_exp_eff ve2) ^ + " else " ^ (string_of_val_exp_eff ve3) + + | Predef(op,sargs), vel -> + if Predef.is_infix op then ( + match vel with + | [ve1; ve2] -> + (string_of_val_exp_eff ve1) ^ " " ^ (Predef.op2string op) ^ + " " ^ (string_of_val_exp_eff ve2) + | _ -> assert false + ) + else + ((Predef.op2string op) ^ + (if sargs = [] then match op with | Predef.ICONST_n _ | Predef.RCONST_n _ | Predef.NOT_n | Predef.UMINUS_n | Predef.IUMINUS_n | Predef.RUMINUS_n @@ -355,67 +355,67 @@ and (string_of_by_pos_op_eff: by_pos_op_eff srcflagged -> val_exp_eff list -> st else "<<" ^ (String.concat ", " (List.map (static_arg2string (Some lxm)) sargs)) - ^ ">>" ^ (tuple_par vel))) - - | CALL_eff nee, _ -> ( - if nee.it.def_eff = ExternEff then - ((string_of_node_key_iter nee.src nee.it.node_key_eff) ^ (tuple_par vel)) - else - (* recursive node cannot be extern *) - ((string_of_node_key_rec nee.it.node_key_eff) ^ (tuple_par vel)) - ) - | IDENT_eff idref, _ -> Ident.string_of_idref idref - | CONST_eff (idref,pn), _ -> + ^ ">>" ^ (tuple_par vel))) + + | CALL nee, _ -> ( + if nee.it.def_eff = ExternEff then + ((string_of_node_key_iter nee.src nee.it.node_key_eff) ^ (tuple_par vel)) + else + (* recursive node cannot be extern *) + ((string_of_node_key_rec nee.it.node_key_eff) ^ (tuple_par vel)) + ) + | IDENT idref, _ -> Ident.string_of_idref idref + | CONST (idref,pn), _ -> Ident.string_of_idref ( match Ident.pack_of_idref idref with | Some _ -> idref | None -> Ident.make_idref pn (Ident.of_idref idref) ) - | PRE_eff, _ -> "pre " ^ (tuple vel) - | ARROW_eff, [ve1; ve2] -> - (string_of_val_exp_eff ve1) ^ " -> " ^ (string_of_val_exp_eff ve2) - | FBY_eff, [ve1; ve2] -> - (string_of_val_exp_eff ve1) ^ " fby " ^ (string_of_val_exp_eff ve2) - | WHEN_eff _, [ve1; ve2] -> - (string_of_val_exp_eff ve1) ^ " when " ^ (string_of_val_exp_eff ve2) - | WHENOT_eff _, [ve1; ve2] -> - (string_of_val_exp_eff ve1) ^ " when not " ^ (string_of_val_exp_eff ve2) - | CURRENT_eff,_ -> "current " ^ (tuple vel) - | TUPLE_eff,_ -> (tuple vel) - | WITH_eff(ve),_ -> (string_of_val_exp_eff ve) - | CONCAT_eff, [ve1; ve2] -> - (string_of_val_exp_eff ve1) ^ " | " ^ (string_of_val_exp_eff ve2) - | HAT_eff (i, ve), _ -> (string_of_val_exp_eff ve) ^ "^" ^ (string_of_int i) - | ARRAY_eff, _ -> tuple_square vel - | STRUCT_ACCESS_eff(id), [ve1] -> - (string_of_val_exp_eff ve1) ^ "." ^ (Ident.to_string id) - - | ARRAY_ACCES_eff(i, type_eff), [ve1] -> - (string_of_val_exp_eff ve1) ^ "[" ^ (string_of_int i) ^ "]" - - | ARRAY_SLICE_eff(si_eff, type_eff), [ve1] -> - (string_of_val_exp_eff ve1) ^ (string_of_slice_info_eff si_eff) - - | ARRAY_SLICE_eff(_,_), _ -> assert false (* todo *) - | MERGE_eff _, _ -> assert false (* todo *) - (* | ITERATOR_eff _, _ -> assert false (* todo *) *) + | PRE, _ -> "pre " ^ (tuple vel) + | ARROW, [ve1; ve2] -> + (string_of_val_exp_eff ve1) ^ " -> " ^ (string_of_val_exp_eff ve2) + | FBY, [ve1; ve2] -> + (string_of_val_exp_eff ve1) ^ " fby " ^ (string_of_val_exp_eff ve2) + | WHEN _, [ve1; ve2] -> + (string_of_val_exp_eff ve1) ^ " when " ^ (string_of_val_exp_eff ve2) + | WHENOT _, [ve1; ve2] -> + (string_of_val_exp_eff ve1) ^ " when not " ^ (string_of_val_exp_eff ve2) + | CURRENT,_ -> "current " ^ (tuple vel) + | TUPLE,_ -> (tuple vel) + | WITH(ve),_ -> (string_of_val_exp_eff ve) + | CONCAT, [ve1; ve2] -> + (string_of_val_exp_eff ve1) ^ " | " ^ (string_of_val_exp_eff ve2) + | HAT (i, ve), _ -> (string_of_val_exp_eff ve) ^ "^" ^ (string_of_int i) + | ARRAY, _ -> tuple_square vel + | STRUCT_ACCESS(id), [ve1] -> + (string_of_val_exp_eff ve1) ^ "." ^ (Ident.to_string id) + + | ARRAY_ACCES(i, type_eff), [ve1] -> + (string_of_val_exp_eff ve1) ^ "[" ^ (string_of_int i) ^ "]" + + | ARRAY_SLICE(si_eff, type_eff), [ve1] -> + (string_of_val_exp_eff ve1) ^ (string_of_slice_info_eff si_eff) + + | ARRAY_SLICE(_,_), _ -> assert false (* todo *) + | MERGE _, _ -> assert false (* todo *) + (* | ITERATOR _, _ -> assert false (* todo *) *) (* Cannot happen *) - | ARROW_eff, _ -> assert false - | FBY_eff, _ -> assert false - | CONCAT_eff, _ -> assert false - | STRUCT_ACCESS_eff(_), _ -> assert false - | ARRAY_ACCES_eff(i, type_eff), _ -> assert false + | ARROW, _ -> assert false + | FBY, _ -> assert false + | CONCAT, _ -> assert false + | STRUCT_ACCESS(_), _ -> assert false + | ARRAY_ACCES(i, type_eff), _ -> assert false in let do_not_parenthesize = function - | CONST_eff _,_ - | IDENT_eff _,_ - | Predef_eff((Predef.ICONST_n _), _),_ - | Predef_eff((Predef.RCONST_n _), _),_ - | Predef_eff((Predef.FALSE_n), _),_ - | Predef_eff((Predef.TRUE_n), _),_ - | ARRAY_ACCES_eff _,_ - | STRUCT_ACCESS_eff _,_ -> true + | CONST _,_ + | IDENT _,_ + | Predef((Predef.ICONST_n _), _),_ + | Predef((Predef.RCONST_n _), _),_ + | Predef((Predef.FALSE_n), _),_ + | Predef((Predef.TRUE_n), _),_ + | ARRAY_ACCES _,_ + | STRUCT_ACCESS _,_ -> true | _,_ -> false in if @@ -436,21 +436,21 @@ and string_of_val_exp_eff = function | CallByNameEff(by_name_op_eff, fl) -> (match by_name_op_eff.it with - | STRUCT_eff (pn,idref) -> prefix ^ ( + | STRUCT (pn,idref) -> prefix ^ ( match Ident.pack_of_idref idref with | Some pn -> Ident.string_of_idref idref | None -> let idref = Ident.make_idref pn (Ident.of_idref idref) in Ident.string_of_idref idref ) - | STRUCT_anonymous_eff -> "") ^ - "{" ^ (String.concat ";" - (List.map - (fun (id,veff) -> - (Ident.to_string id.it) ^ "=" ^ (string_of_val_exp_eff veff) - ) - fl)) ^ - "}" + | STRUCT_anonymous -> "") ^ + "{" ^ (String.concat ";" + (List.map + (fun (id,veff) -> + (Ident.to_string id.it) ^ "=" ^ (string_of_val_exp_eff veff) + ) + fl)) ^ + "}" @@ -459,17 +459,17 @@ and wrap_long_line str = let str_list = Str.split (Str.regexp " ") str in let new_str, reste = List.fold_left - (fun (accl, acc_str) str -> - let new_acc_str = acc_str ^ " " ^ str in - if - String.length new_acc_str > 75 - then - (accl ^ acc_str ^ "\n\t" , str) - else - (accl, new_acc_str) - ) - ("","") - str_list + (fun (accl, acc_str) str -> + let new_acc_str = acc_str ^ " " ^ str in + if + String.length new_acc_str > 75 + then + (accl ^ acc_str ^ "\n\t" , str) + else + (accl, new_acc_str) + ) + ("","") + str_list in new_str ^ " " ^ reste @@ -477,12 +477,12 @@ and string_of_eq_info_eff (leff_list, vee) = wrap_long_line ( (string_of_leff_list leff_list) ^ " = " ^ (string_of_val_exp_eff vee) ^ ";") -and (string_of_assert : val_exp_eff srcflagged -> string ) = +and (string_of_assert : Eff.val_exp srcflagged -> string ) = fun eq_eff -> wrap_long_line ( "assert(" ^ string_of_val_exp_eff eq_eff.it ^ ");") -and (string_of_eq : eq_info_eff srcflagged -> string) = +and (string_of_eq : Eff.eq_info srcflagged -> string) = fun eq_eff -> string_of_eq_info_eff eq_eff.it @@ -492,51 +492,51 @@ and wrap_long_profile str = if String.length str < 75 then str else "\n"^( Str.global_replace (Str.regexp "returns") "\nreturns" - (Str.global_replace (Str.regexp "(") "(\n\t" - (Str.global_replace (Str.regexp "; ") ";\n\t" str))) + (Str.global_replace (Str.regexp "(") "(\n\t" + (Str.global_replace (Str.regexp "; ") ";\n\t" str))) -and (profile_of_node_exp_eff: node_exp_eff -> string) = +and (profile_of_node_exp_eff: Eff.node_exp -> string) = fun neff -> ("(" ^ (string_of_type_decl_list neff.inlist_eff "; ") ^ ") returns (" ^ (string_of_type_decl_list neff.outlist_eff "; ") ^ ");\n") -and (string_of_node_def : node_def_eff -> string list) = +and (string_of_node_def : Eff.node_def -> string list) = function | ExternEff | AbstractEff -> [] | BodyEff node_body_eff -> - List.append - (List.map string_of_assert node_body_eff.asserts_eff) - (List.map string_of_eq node_body_eff.eqs_eff) + List.append + (List.map string_of_assert node_body_eff.asserts_eff) + (List.map string_of_eq node_body_eff.eqs_eff) (* exported *) -and (type_decl: Ident.long -> type_eff -> string) = +and (type_decl: Ident.long -> Eff.type_ -> string) = fun tname teff -> "type " ^ prefix ^ (long tname) ^ (match teff with - | External_type_eff _ -> ";\n" - | _ -> " = " ^ (string_def_of_type_eff teff) ^ ";\n" + | External_type_eff _ -> ";\n" + | _ -> " = " ^ (string_def_of_type_eff teff) ^ ";\n" ) (* exported *) -and (const_decl: Ident.long -> const_eff -> string) = +and (const_decl: Ident.long -> Eff.const -> string) = fun tname ceff -> let str = "const " ^ (long tname) in (match ceff with - | Extern_const_eff _ -> - str^":" ^ (string_of_type_eff (type_of_const_eff ceff))^ ";\n" - | Enum_const_eff _ -> "" (* do not print those const *) - | Struct_const_eff _ -> assert false - | Array_const_eff _ - | Bool_const_eff _ - | Int_const_eff _ - | Real_const_eff _ -> str^" = " ^ (string_of_const_eff ceff)^ ";\n" + | Extern_const_eff _ -> + str^":" ^ (string_of_type_eff (Eff.type_of_const ceff))^ ";\n" + | Enum_const_eff _ -> "" (* do not print those const *) + | Struct_const_eff _ -> assert false + | Array_const_eff _ + | Bool_const_eff _ + | Int_const_eff _ + | Real_const_eff _ -> str^" = " ^ (string_of_const_eff ceff)^ ";\n" ) (* exported *) -and (node_of_node_exp_eff: node_exp_eff -> string) = +and (node_of_node_exp_eff: Eff.node_exp -> string) = fun neff -> wrap_long_profile ( (if neff.def_eff = ExternEff then "extern " else "") ^ @@ -544,28 +544,28 @@ and (node_of_node_exp_eff: node_exp_eff -> string) = (string_of_node_key_rec neff.node_key_eff) ^ (profile_of_node_exp_eff neff)) ^ (match neff.def_eff with - | ExternEff -> "" - | AbstractEff -> "" - | BodyEff _ -> - ((match neff.loclist_eff with None -> "" | Some [] -> "" - | Some l -> - "var\n " ^ (string_of_type_decl_list l ";\n ") ^ ";\n") ^ - "let\n " ^ - (String.concat "\n " (string_of_node_def neff.def_eff)) ^ - "\ntel\n-- end of node " ^ - (string_of_node_key_rec neff.node_key_eff) ^ "\n" - ) + | ExternEff -> "" + | AbstractEff -> "" + | BodyEff _ -> + ((match neff.loclist_eff with None -> "" | Some [] -> "" + | Some l -> + "var\n " ^ (string_of_type_decl_list l ";\n ") ^ ";\n") ^ + "let\n " ^ + (String.concat "\n " (string_of_node_def neff.def_eff)) ^ + "\ntel\n-- end of node " ^ + (string_of_node_key_rec neff.node_key_eff) ^ "\n" + ) ) (* exported *) -and string_of_clock2 (ck : clock_eff) = +and string_of_clock2 (ck : Eff.clock) = let rec string_of_clock2_aux ck = (* to avoid printing the first level var name *) match ck with | BaseEff -> " on base" | On(veff,ceff) ->" on " ^ (Ident.to_string veff) ^ - (string_of_clock2_aux ceff) + (string_of_clock2_aux ceff) | ClockVar i -> "'a" ^ string_of_int i in match ck with @@ -573,7 +573,7 @@ and string_of_clock2 (ck : clock_eff) = | On(_,ceff) -> (string_of_clock2_aux ceff) | ClockVar i -> "'a" ^ string_of_int i -and string_of_clock (ck : clock_eff) = +and string_of_clock (ck : Eff.clock) = match ck with | BaseEff -> "" | On(_,BaseEff) -> "" diff --git a/src/licDump.mli b/src/licDump.mli index c93af2e8..2647f854 100644 --- a/src/licDump.mli +++ b/src/licDump.mli @@ -1,23 +1,22 @@ -(** Time-stamp: <modified the 27/08/2008 (at 16:09) by Erwan Jahier> *) +(** Time-stamp: <modified the 29/08/2008 (at 10:15) by Erwan Jahier> *) -open CompiledData -val string_of_node_key_rec : node_key -> string -val node_of_node_exp_eff: node_exp_eff -> string +val string_of_node_key_rec : Eff.node_key -> string +val node_of_node_exp_eff: Eff.node_exp -> string -val string_of_const_eff : const_eff -> string +val string_of_const_eff : Eff.const -> string -val string_of_type_eff : type_eff -> string -val string_of_type_eff_list : type_eff list -> string -val type_eff_list_to_string :type_eff list -> string +val string_of_type_eff : Eff.type_ -> string +val string_of_type_eff_list : Eff.type_ list -> string +val type_eff_list_to_string :Eff.type_ list -> string -val type_decl: Ident.long -> type_eff -> string -val const_decl: Ident.long -> const_eff -> string +val type_decl: Ident.long -> Eff.type_ -> string +val const_decl: Ident.long -> Eff.const -> string -val profile_of_node_exp_eff: node_exp_eff -> string -val string_of_var_info_eff: var_info_eff -> string -val type_string_of_var_info_eff: var_info_eff -> string -val string_of_slice_info_eff : slice_info_eff -> string +val profile_of_node_exp_eff: Eff.node_exp -> string +val string_of_var_info_eff: Eff.var_info -> string +val type_string_of_var_info_eff: Eff.var_info -> string +val string_of_slice_info_eff : Eff.slice_info -> string (* Dump all the aliases that were introduced during the compilation process *) @@ -54,14 +53,14 @@ val dump_node_alias : out_channel -> unit intertwinned... *) type tab_elt = - | OpProfile of type_eff list * type_eff list - | Subst of type_eff + | OpProfile of Eff.type_ list * Eff.type_ list + | Subst of Eff.type_ val tabulate_poly_op : Lxm.t -> tab_elt -> unit val poly_op_mem : Lxm.t -> bool val poly_op_find : Lxm.t -> tab_elt option (* used for error msgs *) -val string_of_clock2 : clock_eff -> string -val string_of_val_exp_eff : val_exp_eff -> string +val string_of_clock2 : Eff.clock -> string +val string_of_val_exp_eff : Eff.val_exp -> string diff --git a/src/parser.mly b/src/parser.mly index 62533452..edc86881 100644 --- a/src/parser.mly +++ b/src/parser.mly @@ -812,29 +812,29 @@ sxExpression: ; sxPredefOp: - | TK_NOT { {src=$1; it=Predef(NOT_n,[])} } + | TK_NOT { {src=$1; it=Predef_n(NOT_n,[])} } | TK_FBY { {src=$1; it=FBY_n} } | TK_PRE { {src=$1; it=PRE_n} } | TK_CURRENT{ {src=$1; it=CURRENT_n} } | TK_ARROW { {src=$1; it=ARROW_n} } | TK_WHEN { {src=$1; it=WHEN_n} } - | TK_AND { {src=$1; it=Predef(AND_n,[]) } } - | TK_OR { {src=$1; it=Predef(OR_n,[]) } } - | TK_XOR { {src=$1; it=Predef(XOR_n,[]) } } - | TK_IMPL { {src=$1; it=Predef(IMPL_n,[]) } } - | TK_EQ { {src=$1; it=Predef(EQ_n,[]) } } - | TK_NEQ { {src=$1; it=Predef(NEQ_n,[]) } } - | TK_LT { {src=$1; it=Predef(LT_n,[]) } } - | TK_LTE { {src=$1; it=Predef(LTE_n,[]) } } - | TK_GT { {src=$1; it=Predef(GT_n,[]) } } - | TK_GTE { {src=$1; it=Predef(GTE_n,[]) } } - | TK_DIV { {src=$1; it=Predef(DIV_n,[]) } } - | TK_MOD { {src=$1; it=Predef(MOD_n,[]) } } - | TK_MINUS { {src=$1; it=Predef(MINUS_n,[]) } } - | TK_PLUS { {src=$1; it=Predef(PLUS_n,[]) } } - | TK_SLASH { {src=$1; it=Predef(SLASH_n,[]) } } - | TK_STAR { {src=$1; it=Predef(TIMES_n,[]) } } - | TK_IF { {src=$1; it=Predef(IF_n,[]) } } + | TK_AND { {src=$1; it=Predef_n(AND_n,[]) } } + | TK_OR { {src=$1; it=Predef_n(OR_n,[]) } } + | TK_XOR { {src=$1; it=Predef_n(XOR_n,[]) } } + | TK_IMPL { {src=$1; it=Predef_n(IMPL_n,[]) } } + | TK_EQ { {src=$1; it=Predef_n(EQ_n,[]) } } + | TK_NEQ { {src=$1; it=Predef_n(NEQ_n,[]) } } + | TK_LT { {src=$1; it=Predef_n(LT_n,[]) } } + | TK_LTE { {src=$1; it=Predef_n(LTE_n,[]) } } + | TK_GT { {src=$1; it=Predef_n(GT_n,[]) } } + | TK_GTE { {src=$1; it=Predef_n(GTE_n,[]) } } + | TK_DIV { {src=$1; it=Predef_n(DIV_n,[]) } } + | TK_MOD { {src=$1; it=Predef_n(MOD_n,[]) } } + | TK_MINUS { {src=$1; it=Predef_n(MINUS_n,[]) } } + | TK_PLUS { {src=$1; it=Predef_n(PLUS_n,[]) } } + | TK_SLASH { {src=$1; it=Predef_n(SLASH_n,[]) } } + | TK_STAR { {src=$1; it=Predef_n(TIMES_n,[]) } } + | TK_IF { {src=$1; it=Predef_n(IF_n,[]) } } ; /* Appel fonctionnel par position (classique) */ /* NB @@ -1006,13 +1006,13 @@ sxExpressionList: sxExpression ; sxConstant: TK_TRUE - { (leafexp $1 (Predef(TRUE_n,[]))) } + { (leafexp $1 (Predef_n(TRUE_n,[]))) } | TK_FALSE - { (leafexp $1 (Predef(FALSE_n,[]))) } + { (leafexp $1 (Predef_n(FALSE_n,[]))) } | TK_ICONST - { (leafexp $1 (Predef((ICONST_n (Lxm.id $1)),[]))) } + { (leafexp $1 (Predef_n((ICONST_n (Lxm.id $1)),[]))) } | TK_RCONST - { (leafexp $1 (Predef((RCONST_n (Lxm.id $1)),[]))) } + { (leafexp $1 (Predef_n((RCONST_n (Lxm.id $1)),[]))) } ; /* WARNING ! : les listes sont crées à l'envers */ diff --git a/src/parserUtils.ml b/src/parserUtils.ml index 3c1600e5..36d4cf73 100644 --- a/src/parserUtils.ml +++ b/src/parserUtils.ml @@ -1,4 +1,4 @@ -(** Time-stamp: <modified the 28/08/2008 (at 10:29) by Erwan Jahier> *) +(** Time-stamp: <modified the 29/08/2008 (at 09:34) by Erwan Jahier> *) @@ -123,18 +123,18 @@ let flat_twice_flagged_list let leafexp lxm op = CallByPos({src = lxm ; it = op }, Oper []) let unexp lxm op e1 = CallByPos( {src = lxm ; it = op }, Oper [e1] ) -let unexp_predef lxm op e1 = CallByPos( {src = lxm ; it = Predef (op,[]) }, Oper [e1] ) +let unexp_predef lxm op e1 = CallByPos( {src = lxm ; it = Predef_n (op,[]) }, Oper [e1] ) let binexp lxm op e1 e2 = CallByPos( {src = lxm ; it = op }, Oper [e1 ; e2] ) -let binexp_predef lxm op e1 e2 = CallByPos( {src = lxm ; it = Predef (op,[]) }, +let binexp_predef lxm op e1 e2 = CallByPos( {src = lxm ; it = Predef_n (op,[]) }, Oper [e1 ; e2] ) let ternexp lxm op e1 e2 e3 = CallByPos( {src = lxm ; it = op }, Oper [e1 ; e2; e3] ) -let ternexp_predef lxm op e1 e2 e3 = CallByPos( {src = lxm ; it = Predef (op,[]) }, +let ternexp_predef lxm op e1 e2 e3 = CallByPos( {src = lxm ; it = Predef_n (op,[]) }, Oper [e1 ; e2; e3] ) let naryexp lxm op elst = CallByPos( {src = lxm ; it = op }, Oper elst ) -let naryexp_predef lxm op elst = CallByPos( {src = lxm ; it = Predef (op,[]) }, +let naryexp_predef lxm op elst = CallByPos( {src = lxm ; it = Predef_n (op,[]) }, Oper elst ) @@ -458,7 +458,7 @@ let (threat_slice_start : Lxm.t -> val_exp -> val_exp option -> slice_info srcfl let int_to_val_exp istr = try ignore (int_of_string istr); - CallByPos(flagit (Predef(ICONST_n (Ident.of_string(istr)),[])) lxm, + CallByPos(flagit (Predef_n(ICONST_n (Ident.of_string(istr)),[])) lxm, Oper []) with _ -> CallByPos(flagit (IDENT_n (Ident.idref_of_string(istr))) lxm, diff --git a/src/predefEvalClock.ml b/src/predefEvalClock.ml index 14921087..ce06ce9b 100644 --- a/src/predefEvalClock.ml +++ b/src/predefEvalClock.ml @@ -1,10 +1,9 @@ -(** Time-stamp: <modified the 28/08/2008 (at 10:29) by Erwan Jahier> *) +(** Time-stamp: <modified the 28/08/2008 (at 15:35) by Erwan Jahier> *) open Predef -open CompiledData (* exported *) -type clocker = CompiledData.clock_eff Predef.evaluator +type clocker = Eff.clock Predef.evaluator (* exported *) exception EvalClock_error of string @@ -46,7 +45,7 @@ let boolred_clock_profile lxm sargs clks = (* This table contains the clock profile of predefined operators *) -let (f: op -> Lxm.t -> CompiledData.static_arg_eff list -> clocker) = +let (f: op -> Lxm.t -> Eff.static_arg list -> clocker) = fun op lxm sargs -> match op with | TRUE_n | FALSE_n | ICONST_n _ | RCONST_n _ -> constant_profile diff --git a/src/predefEvalClock.mli b/src/predefEvalClock.mli index cd2dabb5..403d8671 100644 --- a/src/predefEvalClock.mli +++ b/src/predefEvalClock.mli @@ -1,8 +1,8 @@ -(** Time-stamp: <modified the 09/06/2008 (at 12:31) by Erwan Jahier> *) +(** Time-stamp: <modified the 28/08/2008 (at 16:05) by Erwan Jahier> *) -type clocker = CompiledData.clock_eff Predef.evaluator +type clocker = Eff.clock Predef.evaluator exception EvalClock_error of string -val f: Predef.op -> Lxm.t -> CompiledData.static_arg_eff list -> clocker +val f: Predef.op -> Lxm.t -> Eff.static_arg list -> clocker diff --git a/src/predefEvalConst.ml b/src/predefEvalConst.ml index c0b2a393..b0a7ce8b 100644 --- a/src/predefEvalConst.ml +++ b/src/predefEvalConst.ml @@ -1,23 +1,23 @@ -(** Time-stamp: <modified the 28/08/2008 (at 10:29) by Erwan Jahier> *) +(** Time-stamp: <modified the 28/08/2008 (at 17:30) by Erwan Jahier> *) open Predef -open SyntaxTreeCore -open CompiledData +open Eff + (* open Lxm *) (* open Errors *) -type const_evaluator = const_eff evaluator +type const_evaluator = Eff.const evaluator exception EvalConst_error of string (* exported *) -let (type_error_const : const_eff list -> string -> 'a) = +let (type_error_const : Eff.const 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) = +let (arity_error_const : Eff.const list -> string -> 'a) = fun v expect -> raise (EvalConst_error( Printf.sprintf "\n*** arity error: %d argument%s, whereas %s were expected" @@ -123,11 +123,11 @@ let (boolred_evaluator : int -> const_evaluator) = (* exported *) -let (f: op -> Lxm.t -> static_arg_eff list -> const_evaluator) = +let (f: op -> Lxm.t -> Eff.static_arg 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)); + ignore (PredefEvalType.f op lxm sargs (List.map (List.map Eff.type_of_const) ll)); match op with | TRUE_n -> sb_evaluator true ll | FALSE_n -> sb_evaluator false ll diff --git a/src/predefEvalConst.mli b/src/predefEvalConst.mli index 8ed8ea8e..79d4ad27 100644 --- a/src/predefEvalConst.mli +++ b/src/predefEvalConst.mli @@ -1,16 +1,15 @@ -(** Time-stamp: <modified the 26/05/2008 (at 14:57) by Erwan Jahier> *) +(** Time-stamp: <modified the 28/08/2008 (at 17:01) 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 +val type_error_const : Eff.const list -> string -> 'a +val arity_error_const : Eff.const list -> string -> 'a -type const_evaluator = const_eff evaluator +type const_evaluator = Eff.const evaluator (* That function says how to statically evaluate constants *) val f: - Predef.op -> Lxm.t -> CompiledData.static_arg_eff list -> const_evaluator + Predef.op -> Lxm.t -> Eff.static_arg list -> const_evaluator diff --git a/src/predefEvalType.ml b/src/predefEvalType.ml index ee1b471b..f5153206 100644 --- a/src/predefEvalType.ml +++ b/src/predefEvalType.ml @@ -1,22 +1,20 @@ -(** Time-stamp: <modified the 28/08/2008 (at 10:29) by Erwan Jahier> *) +(** Time-stamp: <modified the 28/08/2008 (at 17:30) by Erwan Jahier> *) open Predef -open SyntaxTreeCore -open CompiledData open Lxm open Errors open UnifyType - +open Eff (* exported *) -type typer = type_eff Predef.evaluator +type typer = Eff.type_ Predef.evaluator (* exported *) exception EvalType_error of string (* exported *) -let (type_error : type_eff list -> string -> 'a) = +let (type_error : Eff.type_ list -> string -> 'a) = fun tel expect -> let str_l = List.map LicDump.string_of_type_eff tel in let str_provided = String.concat "*" str_l in @@ -72,12 +70,12 @@ 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: var_info_eff list -> int -> (Ident.t * type_eff) list) = +let (type_to_array_type: Eff.var_info list -> int -> (Ident.t * Eff.type_) list) = fun l c -> List.map (fun vi -> vi.var_name_eff, Array_type_eff(vi.var_type_eff,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)= +let (get_node_and_constant:Eff.static_arg list -> Eff.node_exp * int)= fun sargs -> match sargs with | [NodeStaticArgEff(_,n);ConstStaticArgEff(_,Int_const_eff c)] -> n,c @@ -104,8 +102,8 @@ let map_profile = let get_id_type vi = vi.var_name_eff, vi.var_type_eff -let (fillred_profile : Lxm.t -> CompiledData.static_arg_eff list -> - (Ident.t * type_eff) list * (Ident.t * type_eff) list) = +let (fillred_profile : Lxm.t -> Eff.static_arg list -> + (Ident.t * Eff.type_) list * (Ident.t * Eff.type_) list) = (* Given - a node n of type tau * tau_1 * ... * tau_n -> tau * teta_1 * ... * teta_l - a constant c (nb : sargs = [n,c]) @@ -162,7 +160,7 @@ let (fillred_profile : Lxm.t -> CompiledData.static_arg_eff list -> *) let boolred_profile = fun lxm sargs -> - let (get_three_constants: Lxm.t -> static_arg_eff list -> int * int * int) = + let (get_three_constants: Lxm.t -> Eff.static_arg list -> int * int * int) = fun lxm sargs -> match sargs with | [ConstStaticArgEff(_,Int_const_eff i); @@ -174,11 +172,11 @@ let boolred_profile = [id "i", (Array_type_eff(Bool_type_eff,k))], [id "o", b] -type node_profile = (Ident.t * type_eff) list * (Ident.t * type_eff) list +type node_profile = (Ident.t * Eff.type_) list * (Ident.t * Eff.type_) list -let (op2profile : Predef.op -> Lxm.t -> static_arg_eff list -> node_profile) = +let (op2profile : Predef.op -> Lxm.t -> Eff.static_arg list -> node_profile) = fun op lxm sargs -> let res = match op with @@ -214,7 +212,7 @@ let (op2profile : Predef.op -> Lxm.t -> static_arg_eff list -> node_profile) = res (* exported *) let (make_node_exp_eff : - bool option -> op -> Lxm.t -> static_arg_eff list -> node_exp_eff) = + bool option -> op -> Lxm.t -> Eff.static_arg list -> Eff.node_exp) = fun has_mem op lxm sargs -> let id = Ident.make_long (Ident.pack_name_of_string "Lustre") (Ident.of_string (Predef.op2string_long op)) @@ -236,8 +234,8 @@ let (make_node_exp_eff : in { node_key_eff = id,sargs ; - inlist_eff = List.map (to_var_info_eff VarInput) lti; - outlist_eff = (i:=0; List.map (to_var_info_eff VarOutput) lto); + inlist_eff = List.map (to_var_info_eff SyntaxTreeCore.VarInput) lti; + outlist_eff = (i:=0; List.map (to_var_info_eff SyntaxTreeCore.VarOutput) lto); loclist_eff = None; def_eff = ExternEff; has_mem_eff = (match has_mem with Some b -> b | None -> true); @@ -246,7 +244,7 @@ let (make_node_exp_eff : } (* exported *) -let (f : op -> Lxm.t -> CompiledData.static_arg_eff list -> typer) = +let (f : op -> Lxm.t -> Eff.static_arg list -> typer) = fun op lxm sargs ll -> match op with | IF_n -> ( diff --git a/src/predefEvalType.mli b/src/predefEvalType.mli index d5e00942..63dae2b8 100644 --- a/src/predefEvalType.mli +++ b/src/predefEvalType.mli @@ -1,11 +1,9 @@ -(** Time-stamp: <modified the 26/08/2008 (at 14:49) by Erwan Jahier> *) +(** Time-stamp: <modified the 29/08/2008 (at 10:21) by Erwan Jahier> *) -open CompiledData - -type typer = type_eff Predef.evaluator +type typer = Eff.type_ Predef.evaluator exception EvalType_error of string -val type_error : type_eff list -> string -> 'a +val type_error : Eff.type_ list -> string -> 'a val arity_error : 'a list -> string -> 'b @@ -13,17 +11,16 @@ val arity_error : 'a list -> string -> 'b 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 f : Predef.op -> Lxm.t -> Eff.static_arg list -> typer (* Does not work for NOR_n and DIESE_n! *) val make_node_exp_eff : - bool option -> Predef.op -> Lxm.t -> static_arg_eff list -> node_exp_eff + bool option -> Predef.op -> Lxm.t -> Eff.static_arg list -> Eff.node_exp + +type node_profile = (Ident.t * Eff.type_) list * (Ident.t * Eff.type_) list -val fillred_profile : Lxm.t -> CompiledData.static_arg_eff list -> - (Ident.t * type_eff) list * (Ident.t * type_eff) list -val map_profile : Lxm.t -> CompiledData.static_arg_eff list -> - (Ident.t * type_eff) list * (Ident.t * type_eff) list -val boolred_profile : Lxm.t -> CompiledData.static_arg_eff list -> - (Ident.t * type_eff) list * (Ident.t * type_eff) list +val fillred_profile : Lxm.t -> Eff.static_arg list -> node_profile +val map_profile : Lxm.t -> Eff.static_arg list -> node_profile +val boolred_profile : Lxm.t -> Eff.static_arg list -> node_profile diff --git a/src/predefSemantics.ml b/src/predefSemantics.ml deleted file mode 100644 index 47932651..00000000 --- a/src/predefSemantics.ml +++ /dev/null @@ -1,478 +0,0 @@ -(** Time-stamp: <modified the 22/07/2008 (at 10:56) by Erwan Jahier> *) - - -open Predef -open SyntaxTreeCore -open CompiledData -open Lxm -open Errors -open UnifyType - -(* exported *) -type typer = type_eff Predef.evaluator -type const_evaluator = Predef.const_eff evaluator -type clocker = Predef.clock_eff evaluator - - -(*********************************************************************************) -exception EvalConst_error of string -exception EvalType_error of string - - -let (type_error : type_eff list -> string -> 'a) = - fun tel expect -> - let str_l = List.map LicDump.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 (v : 'a list) (expect : string) = - 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)) - -(* exported *) -let (type_error_const : const_eff list -> string -> 'a) = - fun v expect -> - raise (EvalConst_error( - "type mismatch "^(if expect = "" then "" else (expect^" expected")))) - -(* exported *) -let arity_error_const (v : const_eff list) (expect : string) = - 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 not_evaluable op l = - raise (EvalConst_error( - Printf.sprintf "The operator %s is not allowed in static expression" - (op2string op))) - -(*********************************************************************************) - -(*********************************************************************************) -(* a few local alias to make the node profile below more readable. *) -let i = Int_type_eff -let r = Real_type_eff -let b = Bool_type_eff -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) list -> int -> (Ident.t * type_eff) list) = - fun l c -> - List.map (fun (id, teff) -> id, Array_type_eff(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 UnifyType.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(Bool_type_eff,k))], [id "o", b] - - -type node_profile = (Ident.t * type_eff) list * (Ident.t * type_eff) 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 (type_eval : 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 -> type_eff) = - fun t teff_ext -> match teff_ext with - (* substitutes [t] in [teff_ext] *) - | Bool_type_eff -> Bool_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_ext,i) -> - Array_type_eff(subst_type t teff_ext, i) - | Struct_type_eff(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 (List.flatten ll) in - if (List.length l <> List.length lti) then - arity_error l (string_of_int (List.length lti)) - else - match UnifyType.f lti l with - | Equal -> List.map type_eff_to_type_eff lto - | Unif Any -> - type_error2 - (LicDump.type_eff_list_to_string l) - (LicDump.type_eff_list_to_string lti) - "could not instanciate polymorphic type" - | Unif Overload -> - type_error2 - (LicDump.type_eff_list_to_string l) - (LicDump.type_eff_list_to_string lti) - "could not instanciate overloaded type" - - | Unif t -> - List.map (subst_type (type_eff_to_type_eff t)) lto - - | Ko(str) -> - type_error2 (LicDump.type_eff_list_to_string l) - (LicDump.type_eff_list_to_string lti) str - - -(*********************************************************************************) - -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 (const_eval: 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 (type_eval 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 - -(*********************************************************************************) - -let finish_me msg = print_string ("\n\tXXX predefSemantics.ml:"^msg^" -> finish me!\n") - -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/predefSemantics.mli b/src/predefSemantics.mli deleted file mode 100644 index 01b456d8..00000000 --- a/src/predefSemantics.mli +++ /dev/null @@ -1,53 +0,0 @@ -(** Time-stamp: <modified the 26/05/2008 (at 14:57) by Erwan Jahier> *) - -(** - As far as predefined operators are concerned, typing, clock checking, and constant - evaluation are very similar tasks. It consists in: - - - checking the arity - - checking (recursively) the arguments - - apply a rule associated to the operator that says, given a list - of checked arguments, what is the "result" of the operator call. - - That's why we gathered those three activities in this module. - - nb: the whole operational semantics of predefined operators is - defined by this module. -*) - - -(** An evaluator returns a list because Lustre calls returns tuples. - - SE: migth raise some check error! -*) -type 'a evaluator = 'a list list -> 'a list - -open CompiledData - -type typer = type_eff evaluator -type const_evaluator = const_eff evaluator -type clocker = clock_eff evaluator - - -exception EvalConst_error of string -exception EvalType_error of string - -(* That function says how to statically evaluate constants *) -val const_eval: - Predef.op -> Lxm.t -> CompiledData.static_arg_eff list -> const_evaluator - -(* 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 type_eval: - Predef.op -> Lxm.t -> CompiledData.static_arg_eff list -> typer - -val type_error_const : const_eff list -> string -> 'a -val type_error : type_eff list -> string -> 'a - -val arity_error_const : const_eff list -> string -> 'a -val arity_error : type_eff list -> string -> 'a - - -val make_node_exp_eff : Predef.op -> Lxm.t -> static_arg_eff list -> node_exp_eff diff --git a/src/solveIdent.ml b/src/solveIdent.ml index a0a062ba..7d516834 100644 --- a/src/solveIdent.ml +++ b/src/solveIdent.ml @@ -1,4 +1,4 @@ -(** Time-stamp: <modified the 25/08/2008 (at 11:28) by Erwan Jahier> *) +(** Time-stamp: <modified the 29/08/2008 (at 09:34) by Erwan Jahier> *) let (get_predef : Ident.idref -> Predef.op option) = @@ -58,23 +58,23 @@ and r_static_arg = function | StaticArgIdent(idref) -> ( match get_predef idref with | None -> StaticArgIdent idref - | Some predef -> StaticArgNode (Predef (predef,[])) + | Some predef -> StaticArgNode (Predef_n (predef,[])) ) | StaticArgConst(ve) -> StaticArgConst(r_val_exp ve) | StaticArgType(te) -> StaticArgType(te) | StaticArgNode(by_pos_op) -> StaticArgNode(r_by_pos_op by_pos_op) and r_by_pos_op = function - | Predef(op,args) -> Predef(op,args) (* assert false *) + | Predef_n(op,args) -> Predef_n(op,args) (* assert false *) | CALL_n { src=lxm;it=(idref,sargs) } -> ( match get_predef idref with | None -> CALL_n { src=lxm;it= r_node_exp (idref,sargs) } - | Some op -> Predef (op, List.map (flag r_static_arg) sargs) + | Some op -> Predef_n (op, List.map (flag r_static_arg) sargs) ) | IDENT_n(idref) -> ( match get_predef idref with | None -> IDENT_n(idref) - | Some op -> Predef (op,[]) + | Some op -> Predef_n (op,[]) ) | ARRAY_ACCES_n(val_exp) -> ARRAY_ACCES_n(r_val_exp val_exp) | ARRAY_SLICE_n(slice_info) -> ARRAY_SLICE_n(r_slice_info slice_info) diff --git a/src/split.ml b/src/split.ml index 3fa17785..28d44ca7 100644 --- a/src/split.ml +++ b/src/split.ml @@ -1,8 +1,8 @@ -(** Time-stamp: <modified the 28/08/2008 (at 10:43) by Erwan Jahier> *) +(** Time-stamp: <modified the 29/08/2008 (at 10:43) by Erwan Jahier> *) open Lxm -open CompiledData +open Eff (********************************************************************************) (* stuff to create fresh var names. *) @@ -27,27 +27,27 @@ let init_var () = (1) the new equations (2) the fresh variables. *) -type split_acc = (eq_info_eff srcflagged) list * var_info_eff list +type split_acc = (Eff.eq_info srcflagged) list * Eff.var_info list -let rec (split_eq : split_acc -> eq_info_eff srcflagged -> split_acc) = +let rec (split_eq : split_acc -> Eff.eq_info srcflagged -> split_acc) = fun (eqs, locs) eq -> let (neqs, nlocs) = split_eq_do eq in (eqs@neqs, locs@nlocs) -and (split_eq_do : eq_info_eff Lxm.srcflagged -> split_acc) = +and (split_eq_do : Eff.eq_info Lxm.srcflagged -> split_acc) = fun { src = lxm ; it = (lhs, rhs) } -> let n_rhs, (neqs, nlocs) = split_val_exp true rhs in { src = lxm ; it = (lhs, n_rhs) }::neqs, nlocs -and (split_val_exp : bool -> val_exp_eff -> val_exp_eff * split_acc) = +and (split_val_exp : bool -> Eff.val_exp -> Eff.val_exp * split_acc) = fun top_level ve -> match ve with - | CallByPosEff({it= IDENT_eff _}, _) - | CallByPosEff({it=CONST_eff _}, _) - | CallByPosEff({it=Predef_eff(Predef.TRUE_n,_)}, _) - | CallByPosEff({it=Predef_eff(Predef.FALSE_n,_)}, _) - | CallByPosEff({it=Predef_eff(Predef.ICONST_n _,_)}, _) - | CallByPosEff({it=Predef_eff(Predef.RCONST_n _,_)}, _) + | CallByPosEff({it=Eff.IDENT _}, _) + | CallByPosEff({it=Eff.CONST _}, _) + | CallByPosEff({it=Eff.Predef(Predef.TRUE_n,_)}, _) + | CallByPosEff({it=Eff.Predef(Predef.FALSE_n,_)}, _) + | CallByPosEff({it=Eff.Predef(Predef.ICONST_n _,_)}, _) + | CallByPosEff({it=Eff.Predef(Predef.RCONST_n _,_)}, _) (* We do not create an intermediary variable for those *) -> ve, ([],[]) @@ -59,15 +59,15 @@ and (split_val_exp : bool -> val_exp_eff -> val_exp_eff * split_acc) = let lxm = by_pos_op_eff.src in let (rhs, vel, (eql,vl)) = match by_pos_op_eff.it with - | WITH_eff(ve) -> + | Eff.WITH(ve) -> let ve, (eql, vl) = split_val_exp false ve in - let by_pos_op_eff = Lxm.flagit (WITH_eff(ve)) lxm in + let by_pos_op_eff = Lxm.flagit (Eff.WITH(ve)) lxm in let rhs = CallByPosEff(by_pos_op_eff, OperEff []) in rhs, [ve], (eql, vl) - | HAT_eff (i,ve) -> + | Eff.HAT (i,ve) -> let ve, (eql, vl) = split_val_exp false ve in - let by_pos_op_eff = Lxm.flagit (HAT_eff(i, ve)) lxm in + let by_pos_op_eff = Lxm.flagit (Eff.HAT(i, ve)) lxm in let rhs = CallByPosEff(by_pos_op_eff, OperEff []) in rhs, [ve], (eql, vl) @@ -86,17 +86,17 @@ and (split_val_exp : bool -> val_exp_eff -> val_exp_eff * split_acc) = let nve = match nv_l with | [nv] -> CallByPosEff( - Lxm.flagit (IDENT_eff (Ident.to_idref nv.var_name_eff)) lxm, + Lxm.flagit (Eff.IDENT (Ident.to_idref nv.var_name_eff)) lxm, OperEff [] ) | _ -> CallByPosEff( - Lxm.flagit TUPLE_eff lxm, + Lxm.flagit Eff.TUPLE lxm, OperEff (List.map ( fun nv -> CallByPosEff (Lxm.flagit - (IDENT_eff (Ident.to_idref nv.var_name_eff)) lxm, + (Eff.IDENT (Ident.to_idref nv.var_name_eff)) lxm, OperEff [] )) nv_l @@ -109,7 +109,7 @@ and (split_val_exp : bool -> val_exp_eff -> val_exp_eff * split_acc) = nve, (eql@[eq], vl@nv_l) -and (split_val_exp_list : bool -> val_exp_eff list -> val_exp_eff list * split_acc) = +and (split_val_exp_list : bool -> Eff.val_exp list -> Eff.val_exp list * split_acc) = fun top_level vel -> let vel, accl = List.split (List.map (split_val_exp top_level) vel) in let eqll,vll = List.split accl in @@ -117,7 +117,7 @@ and (split_val_exp_list : bool -> val_exp_eff list -> val_exp_eff list * split_a (vel,(eql,vl)) (* exported *) -let (node : CompiledData.node_exp_eff -> CompiledData.node_exp_eff) = +let (node : Eff.node_exp -> Eff.node_exp) = fun n -> match n.def_eff with | ExternEff diff --git a/src/split.mli b/src/split.mli index 5815b188..96f96bd3 100644 --- a/src/split.mli +++ b/src/split.mli @@ -1,4 +1,4 @@ -(** Time-stamp: <modified the 22/08/2008 (at 14:54) by Erwan Jahier> *) +(** Time-stamp: <modified the 28/08/2008 (at 15:52) by Erwan Jahier> *) (** Split the equations of a node into several ones, in such a way @@ -6,4 +6,4 @@ doing that is to make the clock checking trivial in the lic code (indeed, nested node call makes it tricky). *) -val node : CompiledData.node_exp_eff -> CompiledData.node_exp_eff +val node : Eff.node_exp -> Eff.node_exp diff --git a/src/syntaxTreeCore.ml b/src/syntaxTreeCore.ml index 062ec7e9..512d36fb 100644 --- a/src/syntaxTreeCore.ml +++ b/src/syntaxTreeCore.ml @@ -1,4 +1,4 @@ -(** Time-stamp: <modified the 09/07/2008 (at 11:29) by Erwan Jahier> *) +(** Time-stamp: <modified the 29/08/2008 (at 09:33) by Erwan Jahier> *) (** (Raw) Abstract syntax tree of source programs. *) @@ -86,7 +86,7 @@ and slice_info = { and by_pos_op = (* zeroaire *) - | Predef of Predef.op * static_arg srcflagged list (* e.g., map<<toto,3>> *) + | Predef_n of Predef.op * static_arg srcflagged list (* e.g., map<<toto,3>> *) | CALL_n of node_exp srcflagged (* e.g., a_node<<xx>> *) | IDENT_n of Ident.idref (* constant or variable *) diff --git a/src/syntaxTreeDump.ml b/src/syntaxTreeDump.ml index 376fba6c..f4015e24 100644 --- a/src/syntaxTreeDump.ml +++ b/src/syntaxTreeDump.ml @@ -1,4 +1,4 @@ -(** Time-stamp: <modified the 01/07/2008 (at 14:02) by Erwan Jahier> *) +(** Time-stamp: <modified the 29/08/2008 (at 09:35) by Erwan Jahier> *) open Lxm @@ -21,7 +21,7 @@ let (op2string : SyntaxTreeCore.by_pos_op -> string) = fun op -> match op with (* unaires *) - | Predef(op,sargs) -> (Predef.op2string op) ^ + | Predef_n(op,sargs) -> (Predef.op2string op) ^ (if sargs = [] then "" else "<<" ^ (String.concat ", " (List.map static_arg_to_string sargs)) ^ ">>") | (PRE_n ) -> "pre" @@ -372,54 +372,54 @@ and dump_val_exp_list (os : formatter) (xl: val_exp list) = ( and dump_by_pos_exp (os: Format.formatter) (oper: by_pos_op) (pars: operands) = ( match (oper, pars) with - (Predef (TRUE_n,_), Oper []) -> dump_leaf_exp os "true" - | (Predef (FALSE_n,_), Oper []) -> dump_leaf_exp os "false" - | (Predef (ICONST_n s, _), Oper []) -> dump_leaf_exp os (Ident.to_string s) - | (Predef (RCONST_n s, _), Oper []) -> dump_leaf_exp os (Ident.to_string s) + (Predef_n (TRUE_n,_), Oper []) -> dump_leaf_exp os "true" + | (Predef_n (FALSE_n,_), Oper []) -> dump_leaf_exp os "false" + | (Predef_n (ICONST_n s, _), Oper []) -> dump_leaf_exp os (Ident.to_string s) + | (Predef_n (RCONST_n s, _), Oper []) -> dump_leaf_exp os (Ident.to_string s) | (IDENT_n id,Oper []) -> dump_leaf_exp os (Ident.string_of_idref id) (* unaires *) - | (Predef (NOT_n,_), Oper [p0]) -> dump_unary_exp os "not" p0 - | (Predef (UMINUS_n,_), Oper [p0]) -> dump_unary_exp os "-" p0 - | (Predef (RUMINUS_n,_), Oper [p0]) -> dump_unary_exp os "-" p0 - | (Predef (IUMINUS_n,_), Oper [p0]) -> dump_unary_exp os "-" p0 + | (Predef_n (NOT_n,_), Oper [p0]) -> dump_unary_exp os "not" p0 + | (Predef_n (UMINUS_n,_), Oper [p0]) -> dump_unary_exp os "-" p0 + | (Predef_n (RUMINUS_n,_), Oper [p0]) -> dump_unary_exp os "-" p0 + | (Predef_n (IUMINUS_n,_), Oper [p0]) -> dump_unary_exp os "-" p0 | (PRE_n, Oper [p0]) -> dump_unary_exp os "pre" p0 | (CURRENT_n, Oper [p0]) -> dump_unary_exp os "current" p0 - | (Predef (REAL2INT_n,_), Oper [p0]) -> dump_unary_exp os "int" p0 - | (Predef (INT2REAL_n,_), Oper [p0]) -> dump_unary_exp os "real" p0 + | (Predef_n (REAL2INT_n,_), Oper [p0]) -> dump_unary_exp os "int" p0 + | (Predef_n (INT2REAL_n,_), Oper [p0]) -> dump_unary_exp os "real" p0 (* binaires *) | (ARROW_n, Oper [p0;p1]) -> dump_binary_exp os "->" p0 p1 | (FBY_n, Oper [p0;p1]) -> dump_binary_exp os "fby" p0 p1 | (WHEN_n, Oper [p0;p1]) -> dump_binary_exp os "when" p0 p1 - | (Predef (AND_n,_), Oper [p0;p1]) -> dump_binary_exp os "and" p0 p1 - | (Predef (OR_n,_), Oper [p0;p1]) -> dump_binary_exp os "or" p0 p1 - | (Predef (XOR_n,_), Oper [p0;p1]) -> dump_binary_exp os "xor" p0 p1 - | (Predef (IMPL_n,_), Oper [p0;p1]) -> dump_binary_exp os "=>" p0 p1 - | (Predef (EQ_n,_), Oper [p0;p1]) -> dump_binary_exp os "=" p0 p1 - | (Predef (NEQ_n,_), Oper [p0;p1]) -> dump_binary_exp os "<>" p0 p1 - | (Predef (LT_n,_), Oper [p0;p1]) -> dump_binary_exp os "<" p0 p1 - | (Predef (LTE_n,_), Oper [p0;p1]) -> dump_binary_exp os "<=" p0 p1 - | (Predef (GT_n,_), Oper [p0;p1]) -> dump_binary_exp os ">" p0 p1 - | (Predef (GTE_n,_), Oper [p0;p1]) -> dump_binary_exp os ">=" p0 p1 - | (Predef (DIV_n,_), Oper [p0;p1]) -> dump_binary_exp os "div" p0 p1 - | (Predef (MOD_n,_), Oper [p0;p1]) -> dump_binary_exp os "mod" p0 p1 - | (Predef (MINUS_n,_), Oper [p0]) -> dump_unary_exp os "-" p0 - | (Predef (RMINUS_n,_), Oper [p0]) -> dump_unary_exp os "-" p0 - | (Predef (IMINUS_n,_), Oper [p0]) -> dump_unary_exp os "-" p0 - | (Predef (PLUS_n,_), Oper [p0;p1]) -> dump_binary_exp os "+" p0 p1 - | (Predef (RPLUS_n,_), Oper [p0;p1]) -> dump_binary_exp os "+" p0 p1 - | (Predef (IPLUS_n,_), Oper [p0;p1]) -> dump_binary_exp os "+" p0 p1 - | (Predef (SLASH_n,_), Oper [p0;p1]) -> dump_binary_exp os "/" p0 p1 - | (Predef (RSLASH_n,_), Oper [p0;p1]) -> dump_binary_exp os "/" p0 p1 - | (Predef (ISLASH_n,_), Oper [p0;p1]) -> dump_binary_exp os "/" p0 p1 - | (Predef (TIMES_n,_), Oper [p0;p1]) -> dump_binary_exp os "*" p0 p1 - | (Predef (RTIMES_n,_), Oper [p0;p1]) -> dump_binary_exp os "*" p0 p1 - | (Predef (ITIMES_n,_), Oper [p0;p1]) -> dump_binary_exp os "*" p0 p1 + | (Predef_n (AND_n,_), Oper [p0;p1]) -> dump_binary_exp os "and" p0 p1 + | (Predef_n (OR_n,_), Oper [p0;p1]) -> dump_binary_exp os "or" p0 p1 + | (Predef_n (XOR_n,_), Oper [p0;p1]) -> dump_binary_exp os "xor" p0 p1 + | (Predef_n (IMPL_n,_), Oper [p0;p1]) -> dump_binary_exp os "=>" p0 p1 + | (Predef_n (EQ_n,_), Oper [p0;p1]) -> dump_binary_exp os "=" p0 p1 + | (Predef_n (NEQ_n,_), Oper [p0;p1]) -> dump_binary_exp os "<>" p0 p1 + | (Predef_n (LT_n,_), Oper [p0;p1]) -> dump_binary_exp os "<" p0 p1 + | (Predef_n (LTE_n,_), Oper [p0;p1]) -> dump_binary_exp os "<=" p0 p1 + | (Predef_n (GT_n,_), Oper [p0;p1]) -> dump_binary_exp os ">" p0 p1 + | (Predef_n (GTE_n,_), Oper [p0;p1]) -> dump_binary_exp os ">=" p0 p1 + | (Predef_n (DIV_n,_), Oper [p0;p1]) -> dump_binary_exp os "div" p0 p1 + | (Predef_n (MOD_n,_), Oper [p0;p1]) -> dump_binary_exp os "mod" p0 p1 + | (Predef_n (MINUS_n,_), Oper [p0]) -> dump_unary_exp os "-" p0 + | (Predef_n (RMINUS_n,_), Oper [p0]) -> dump_unary_exp os "-" p0 + | (Predef_n (IMINUS_n,_), Oper [p0]) -> dump_unary_exp os "-" p0 + | (Predef_n (PLUS_n,_), Oper [p0;p1]) -> dump_binary_exp os "+" p0 p1 + | (Predef_n (RPLUS_n,_), Oper [p0;p1]) -> dump_binary_exp os "+" p0 p1 + | (Predef_n (IPLUS_n,_), Oper [p0;p1]) -> dump_binary_exp os "+" p0 p1 + | (Predef_n (SLASH_n,_), Oper [p0;p1]) -> dump_binary_exp os "/" p0 p1 + | (Predef_n (RSLASH_n,_), Oper [p0;p1]) -> dump_binary_exp os "/" p0 p1 + | (Predef_n (ISLASH_n,_), Oper [p0;p1]) -> dump_binary_exp os "/" p0 p1 + | (Predef_n (TIMES_n,_), Oper [p0;p1]) -> dump_binary_exp os "*" p0 p1 + | (Predef_n (RTIMES_n,_), Oper [p0;p1]) -> dump_binary_exp os "*" p0 p1 + | (Predef_n (ITIMES_n,_), Oper [p0;p1]) -> dump_binary_exp os "*" p0 p1 | (HAT_n, Oper [p0;p1]) -> dump_binary_exp os "^" p0 p1 | (CONCAT_n, Oper [p0;p1]) -> dump_binary_exp os "|" p0 p1 - | (Predef (IF_n,_), Oper [p0;p1;p2]) -> dump_ternary_exp os "if" "then" "else" p0 p1 p2 + | (Predef_n (IF_n,_), Oper [p0;p1;p2]) -> dump_ternary_exp os "if" "then" "else" p0 p1 p2 | (WITH_n(_), Oper [p0;p1;p2]) -> dump_ternary_exp os "with" "then" "else" p0 p1 p2 - | (Predef (NOR_n,_), Oper pl) -> dump_nary_exp os "nor" pl - | (Predef (DIESE_n,_), Oper pl) -> dump_nary_exp os "#" pl + | (Predef_n (NOR_n,_), Oper pl) -> dump_nary_exp os "nor" pl + | (Predef_n (DIESE_n,_), Oper pl) -> dump_nary_exp os "#" pl | (TUPLE_n, Oper pl) -> dump_nary_exp os "" pl | (CALL_n s, Oper pl) -> fprintf os "%a(@,%a@,)" dump_node_exp s.it dump_val_exp_list pl @@ -431,7 +431,7 @@ and dump_by_pos_exp (os: Format.formatter) (oper: by_pos_op) (pars: operands) = | (STRUCT_ACCESS_n fld, Oper [p0]) -> fprintf os "%a.%s" dump_val_exp p0 (Ident.to_string fld) - | (Predef (_,_),_) -> assert false + | (Predef_n (_,_),_) -> assert false (* | (ITERATOR_n _, _) -> assert false *) | (MERGE_n _,_) -> assert false diff --git a/src/test/test.res.exp b/src/test/test.res.exp index 86cac852..219a3eaa 100644 --- a/src/test/test.res.exp +++ b/src/test/test.res.exp @@ -9919,7 +9919,7 @@ returns ( clock4_x:bool; clock4_y:bool when clock4_x); -*** oops: an internal error occurred in file evalClock.ml, line 273, column 31 +*** oops: an internal error occurred in file evalClock.ml, line 275, column 31 *** when compiling lustre program should_work/clock/when_not.lus ---------------------------------------------------------------------- diff --git a/src/unifyClock.ml b/src/unifyClock.ml index de10f687..2ed5aa66 100644 --- a/src/unifyClock.ml +++ b/src/unifyClock.ml @@ -1,19 +1,16 @@ -(** Time-stamp: <modified the 19/08/2008 (at 16:54) by Erwan Jahier> *) +(** Time-stamp: <modified the 28/08/2008 (at 17:29) by Erwan Jahier> *) -open SyntaxTree -open SyntaxTreeCore -open CompiledData open LicDump open Printf open Lxm open Errors - +open Eff let ci2str = LicDump.string_of_clock2 (* exported *) -type subst = (Ident.t * Ident.t) list * (int * clock_eff) list +type subst = (Ident.t * Ident.t) list * (int * Eff.clock) list (* exported *) let (empty_subst:subst) = [],[] @@ -29,7 +26,7 @@ let (get_var_type : unit -> int) = (* exported *) -let (get_constant_clock : unit -> clock_eff) = +let (get_constant_clock : unit -> Eff.clock) = fun () -> ClockVar (get_var_type ()) (******************************************************************************) @@ -42,7 +39,7 @@ let subst_to_string (s1,s2) = (ci2str v2)) s2)) (* exported *) -let rec (apply_subst:subst -> clock_eff -> clock_eff) = +let rec (apply_subst:subst -> Eff.clock -> Eff.clock) = fun (s1,s2) c -> match c with | BaseEff -> BaseEff @@ -54,7 +51,7 @@ let rec (apply_subst:subst -> clock_eff -> clock_eff) = with Not_found -> c (* exported *) -let rec (apply_subst2:subst -> clock_eff -> clock_eff) = +let rec (apply_subst2:subst -> Eff.clock -> Eff.clock) = fun (s1,s2) c -> match c with | BaseEff -> BaseEff @@ -64,7 +61,7 @@ let rec (apply_subst2:subst -> clock_eff -> clock_eff) = with Not_found -> c (* exported *) -let (f : Lxm.t -> subst -> clock_eff -> clock_eff -> subst) = +let (f : Lxm.t -> subst -> Eff.clock -> Eff.clock -> subst) = fun lxm (s1,s2) ci1 ci2 -> let ci1 = apply_subst (s1,s2) ci1 in let ci2 = apply_subst (s1,s2) ci2 in @@ -110,7 +107,7 @@ let (f : Lxm.t -> subst -> clock_eff -> clock_eff -> subst) = raise(Compile_error(lxm, msg)) (* exported *) -let (list : Lxm.t -> clock_eff list -> subst -> clock_eff * subst) = +let (list : Lxm.t -> Eff.clock list -> subst -> Eff.clock * subst) = fun lxm cl s -> List.fold_left (fun (clk,s) clk2 -> diff --git a/src/unifyClock.mli b/src/unifyClock.mli index 330a7b4d..48308082 100644 --- a/src/unifyClock.mli +++ b/src/unifyClock.mli @@ -1,7 +1,4 @@ -(** Time-stamp: <modified the 19/08/2008 (at 16:41) by Erwan Jahier> *) - -open CompiledData - +(** Time-stamp: <modified the 28/08/2008 (at 16:06) by Erwan Jahier> *) (* XXX use Map.t @@ -25,24 +22,24 @@ open CompiledData XXX Make it abstract? *) -type subst = (Ident.t * Ident.t) list * (int * clock_eff) list +type subst = (Ident.t * Ident.t) list * (int * Eff.clock) list val empty_subst : subst -val apply_subst:subst -> clock_eff -> clock_eff +val apply_subst:subst -> Eff.clock -> Eff.clock (* only apply the part of the subst that deals with clock var *) -val apply_subst2:subst -> clock_eff -> clock_eff +val apply_subst2:subst -> Eff.clock -> Eff.clock -(** Raises an error is the 2 clock_eff are not unifiable *) -val f : Lxm.t -> subst -> clock_eff -> clock_eff -> subst -val list : Lxm.t -> clock_eff list -> subst -> clock_eff * subst +(** Raises an error is the 2 Eff.clock are not unifiable *) +val f : Lxm.t -> subst -> Eff.clock -> Eff.clock -> subst +val list : Lxm.t -> Eff.clock list -> subst -> Eff.clock * subst (* Stuff to generated fresh var clocks XXX bad place, bad name *) val reset_var_type : unit -> unit -val get_constant_clock : unit -> clock_eff +val get_constant_clock : unit -> Eff.clock val get_var_type : unit -> int diff --git a/src/unifyType.ml b/src/unifyType.ml index 725e5b79..1c05dd75 100644 --- a/src/unifyType.ml +++ b/src/unifyType.ml @@ -1,24 +1,23 @@ -(** Time-stamp: <modified the 27/08/2008 (at 15:37) by Erwan Jahier> *) - -open CompiledData +(** Time-stamp: <modified the 28/08/2008 (at 17:26) by Erwan Jahier> *) +open Eff (* exported *) type t = | Equal - | Unif of type_eff + | Unif of Eff.type_ | Ko of string (* a msg explaining why the unification failed *) let teff2str = LicDump.string_of_type_eff -let (is_overloadable : type_eff -> bool) = function +let (is_overloadable : Eff.type_ -> bool) = function | Int_type_eff -> true | Real_type_eff -> true | _ -> false (* [contains t1 t2] is true iff t2 appears in t1 *) -let rec (contains : type_eff -> type_eff -> bool) = +let rec (contains : Eff.type_ -> Eff.type_ -> bool) = fun t1 t2 -> if t1 = t2 then true else match t1 with @@ -35,8 +34,8 @@ let rec (contains : type_eff -> type_eff -> bool) = (* exported *) -let (f : type_eff list -> type_eff list -> t) = fun l1 l2 -> - let rec (unify_type_eff : type_eff -> type_eff -> t) = +let (f : Eff.type_ list -> Eff.type_ list -> t) = fun l1 l2 -> + let rec (unify_type_eff : Eff.type_ -> Eff.type_ -> t) = fun t1 t2 -> if t1 = t2 then Equal else match (t1,t2) with @@ -75,7 +74,7 @@ let (f : type_eff list -> type_eff list -> t) = fun l1 l2 -> Ko("\n*** " ^ (teff2str t1) ^ " and " ^ (teff2str t2) ^ " are not unifiable") - and (unify_do_acc: t -> type_eff -> type_eff -> t) = + and (unify_do_acc: t -> Eff.type_ -> Eff.type_ -> t) = fun acc te1 te2 -> match acc, unify_type_eff te1 te2 with | Equal, Equal -> Equal diff --git a/src/unifyType.mli b/src/unifyType.mli index 6b9d7ba9..873167fb 100644 --- a/src/unifyType.mli +++ b/src/unifyType.mli @@ -1,4 +1,4 @@ -(** Time-stamp: <modified the 27/08/2008 (at 15:48) by Erwan Jahier> *) +(** Time-stamp: <modified the 28/08/2008 (at 15:58) by Erwan Jahier> *) (** This unify function is quite specific. It can only unify 2 lists of types with at most one type variable (Any or Overload). @@ -15,10 +15,10 @@ type t = | Equal - | Unif of CompiledData.type_eff + | Unif of Eff.type_ | Ko of string (* a msg explaining why the unification failed *) -val f : CompiledData.type_eff list -> CompiledData.type_eff list -> t +val f : Eff.type_ list -> Eff.type_ list -> t (**/**) diff --git a/src/uniqueOutput.ml b/src/uniqueOutput.ml index a380c202..d8d1af2f 100644 --- a/src/uniqueOutput.ml +++ b/src/uniqueOutput.ml @@ -1,27 +1,26 @@ -(** Time-stamp: <modified the 21/08/2008 (at 18:15) by Erwan Jahier> *) +(** Time-stamp: <modified the 29/08/2008 (at 10:42) by Erwan Jahier> *) -open CompiledData open Lxm open Errors - +open Eff (*********************************************************************************) (** [left_eff] is a kind of list, but which is in a « bad » order for - easy checking; [eff_left] contains just the same information, but + easy checking; [filtered_left] contains just the same information, but the list is made explicit and the infomartion (struct or array accesses) is ordered in the « good » way. *) -type eff_left = var_info_eff * Lxm.t * filter list +type filtered_left = Eff.var_info * Lxm.t * filter list and filter = - | Slice of int * int * int * type_eff - | Faccess of Ident.t * type_eff - | Aaccess of int * type_eff + | Slice of int * int * int * Eff.type_ + | Faccess of Ident.t * Eff.type_ + | Aaccess of int * Eff.type_ -let rec (left_eff_to_eff_left: left_eff -> eff_left) = +let rec (left_eff_to_filtered_left: Eff.left -> filtered_left) = fun le -> - let rec (aux : type_eff -> filter list -> left_eff -> eff_left) = + let rec (aux : Eff.type_ -> filter list -> Eff.left -> filtered_left) = fun te_top acc le -> match le with | LeftVarEff (v,lxm) -> v, lxm, acc | LeftFieldEff(le,id,te) -> aux te (Faccess(id,te)::acc) le @@ -29,7 +28,7 @@ let rec (left_eff_to_eff_left: left_eff -> eff_left) = | LeftSliceEff(le,si,te) -> aux te (Slice(si.se_first,si.se_last,si.se_step,te)::acc) le in - let te_top = (var_info_of_left_eff le).var_type_eff in + let te_top = (Eff.var_info_of_left le).var_type_eff in let (v,lxm,f) = aux te_top [] le in let (_,f) = (* we don't want to associate to each accessors the type of the @@ -60,7 +59,7 @@ let id2str = Ident.to_string let int2str = string_of_int (* Returns the list of undefined variables *) -let (vds_to_string : var_info_eff -> var_def_state -> string list) = +let (vds_to_string : Eff.var_info -> var_def_state -> string list) = fun v vds -> let rec aux vds v acc = match vds with | VDS_def -> acc @@ -75,8 +74,8 @@ let (vds_to_string : var_info_eff -> var_def_state -> string list) = (*********************************************************************************) (** This is main function: it computes a new [var_def_state] from an - [var_def_state] and a [eff_left]. *) -let (update_var_def_state : var_def_state -> eff_left -> var_def_state) = + [var_def_state] and a [filtered_left]. *) +let (update_var_def_state : var_def_state -> filtered_left -> var_def_state) = fun vds (v, lxm, filters) -> let rec (update_vds : string -> var_def_state -> filter list -> var_def_state) = fun v vds filters -> @@ -158,13 +157,13 @@ let (update_var_def_state : var_def_state -> eff_left -> var_def_state) = res (*********************************************************************************) -(** Sort out the left_eff according to the variable they define. *) -module VarMap = Map.Make(struct type t = var_info_eff let compare = compare end) +(** Sort out the Eff.left according to the variable they define. *) +module VarMap = Map.Make(struct type t = Eff.var_info let compare = compare end) -let (partition_var : left_eff list -> (left_eff list) VarMap.t) = +let (partition_var : Eff.left list -> (Eff.left list) VarMap.t) = fun l -> let f tab le = - let v = var_info_of_left_eff le in + let v = Eff.var_info_of_left le in try VarMap.add v (le::(VarMap.find v tab)) tab with Not_found -> VarMap.add v [le] tab in @@ -172,15 +171,15 @@ let (partition_var : left_eff list -> (left_eff list) VarMap.t) = (*********************************************************************************) (* exported *) -let (check : CompiledData.node_exp_eff -> Lxm.t -> unit) = +let (check : Eff.node_exp -> Lxm.t -> unit) = fun node lxm -> let vars_to_check = match node.loclist_eff with | None -> node.outlist_eff | Some l -> node.outlist_eff @ l in - let (check_one_var : Lxm.t -> var_info_eff -> left_eff list -> unit) = + let (check_one_var : Lxm.t -> Eff.var_info -> Eff.left list -> unit) = fun lxm v lel -> - let ell = List.map left_eff_to_eff_left lel in + let ell = List.map left_eff_to_filtered_left lel in match List.fold_left update_var_def_state VDS_undef ell with | VDS_def -> () | vds -> diff --git a/src/uniqueOutput.mli b/src/uniqueOutput.mli index f9a7d674..88786202 100644 --- a/src/uniqueOutput.mli +++ b/src/uniqueOutput.mli @@ -1,6 +1,6 @@ -(** Time-stamp: <modified the 25/06/2008 (at 16:34) by Erwan Jahier> *) +(** Time-stamp: <modified the 28/08/2008 (at 15:52) by Erwan Jahier> *) (** Check that each output and each local variable is defined at most and at least once. Also check that one does not try ti define an input. *) -val check : CompiledData.node_exp_eff -> Lxm.t -> unit +val check : Eff.node_exp -> Lxm.t -> unit -- GitLab