From cdb52a14de50068399e7eaf9f48ba731b93556be Mon Sep 17 00:00:00 2001 From: Erwan Jahier <jahier@imag.fr> Date: Tue, 3 Feb 2009 15:42:44 +0100 Subject: [PATCH] The structure and array expanser was buggy in presence of polymorphic nodes (e.g., map<<+,2>>). While fixing that, I put all the functions that deals with polymorphism into a new (Eponymous) dedicated module. The idea to be able to expand polymorphic node is basically the same, as the one for printing polymorphic nodes: we need to wait until the type is instanciated (in GetEff). That delay is implemented by using a stack of nodes. --- release-lv6/Makefile | 2 + src/Makefile | 9 +++-- src/getEff.ml | 20 ++++++++-- src/inline.ml | 15 +++++--- src/lazyCompiler.ml | 38 +++++++------------ src/licDump.ml | 30 ++++----------- src/licDump.mli | 26 +------------ src/polymorphism.ml | 54 ++++++++++++++++++++++++++ src/polymorphism.mli | 44 ++++++++++++++++++++++ src/structArrayExpand.ml | 79 +++++++++++++++++++++++++++++++++------ src/structArrayExpand.mli | 2 +- 11 files changed, 221 insertions(+), 98 deletions(-) create mode 100644 src/polymorphism.ml create mode 100644 src/polymorphism.mli diff --git a/release-lv6/Makefile b/release-lv6/Makefile index b00f7155..aafdeec1 100644 --- a/release-lv6/Makefile +++ b/release-lv6/Makefile @@ -16,9 +16,11 @@ doc: cp ~/slides/lv6/*.pdf $(RELNAME)/doc lus2lic: + cd $(LUS2LICDIR)/src ; make clean ; make nc cp $(LUS2LICDIR)/src/lus2lic $(RELNAME)/bin/ lic2c: + cd $(LIC2CDIR)/src/ ; make clean ; make nc cp $(LIC2CDIR)/src/lic2c $(RELNAME)/bin/ test_files: diff --git a/src/Makefile b/src/Makefile index beea99d5..aa559b43 100644 --- a/src/Makefile +++ b/src/Makefile @@ -33,6 +33,7 @@ SOURCES = \ ./eff.ml \ ./name.mli \ ./name.ml \ + ./polymorphism.ml \ ./licDump.ml \ ./unifyType.mli \ ./unifyType.ml \ @@ -52,18 +53,18 @@ SOURCES = \ ./evalType.ml \ ./evalClock.mli \ ./evalClock.ml \ - ./getEff.mli \ - ./getEff.ml \ + ./structArrayExpand.mli \ + ./structArrayExpand.ml \ ./uniqueOutput.mli \ ./uniqueOutput.ml \ ./split.mli \ ./split.ml \ ./nodesExpand.mli \ ./nodesExpand.ml \ - ./structArrayExpand.mli \ - ./structArrayExpand.ml \ ./inline.mli \ ./inline.ml \ + ./getEff.mli \ + ./getEff.ml \ ./lazyCompiler.ml \ ./lazyCompiler.mli \ ./compile.ml \ diff --git a/src/getEff.ml b/src/getEff.ml index a6604cd7..b7ea4742 100644 --- a/src/getEff.ml +++ b/src/getEff.ml @@ -1,4 +1,4 @@ -(** Time-stamp: <modified the 28/01/2009 (at 10:56) by Erwan Jahier> *) +(** Time-stamp: <modified the 03/02/2009 (at 15:40) by Erwan Jahier> *) open Lxm @@ -371,8 +371,22 @@ and (translate_val_exp : Eff.id_solver -> SyntaxTreeCore.val_exp -> Eff.val_exp) (* the iterated nodes was polymorphic, but we know here that the type varaible was [typ]. *) - LicDump.unstack_polymorphic_nodes typ; - List.map (instanciate_type typ) sargs_eff + + let expand = StructArrayExpand.node in + let nodes = Polymorphism.unstack_polymorphic_nodes expand typ in + List.iter + (fun (id_solver,nenv,node) -> + let node = + if !Global.inline_iterator + then Inline.iterators nenv id_solver node + else node + in + let str = LicDump.node_of_node_exp_eff node in + output_string !Global.oc str + ) + nodes; + Polymorphism.reset_type (); + List.map (instanciate_type typ) sargs_eff | UnifyType.Ko str -> raise (Compile_error(lxm, str)) in mk_by_pos_op (Eff.Predef(iter_op, sargs_eff)) diff --git a/src/inline.ml b/src/inline.ml index f550385f..887d19da 100644 --- a/src/inline.ml +++ b/src/inline.ml @@ -1,4 +1,4 @@ -(** Time-stamp: <modified the 22/01/2009 (at 11:30) by Erwan Jahier> *) +(** Time-stamp: <modified the 03/02/2009 (at 16:04) by Erwan Jahier> *) open Lxm @@ -120,6 +120,7 @@ let rec (inline_eq: Eff.local_env -> (eqs,locs) index_list + | CallByPosEff({src=lxm_ve;it=Eff.Predef(Predef.Fill, sargs)}, OperEff args) | CallByPosEff({src=lxm_ve;it=Eff.Predef(Predef.Red, sargs)}, OperEff args) | CallByPosEff({src=lxm_ve;it=Eff.Predef(Predef.FillRed,sargs)}, OperEff args) @@ -224,8 +225,8 @@ let rec (inline_eq: Eff.local_env -> let arg = CallByPosEff({src=lxm_ve;it=ARRAY args}, OperEff []) in let rhs = CallByPosEff({src=lxm_ve;it=boolred_op}, OperEff [arg]) in let eq = { src = lxm_eq ; it = (lhs, rhs) } in - inline_eq node_env id_solver (eqs, locs) eq + | CallByPosEff({src=lxm_ve;it=Eff.Predef(Predef.NOR_n,_)}, OperEff args) -> (* a nor is a particular kind of boolred too: #(A,...,an) = boolred(0,0,n)([a1,...,an]) @@ -242,7 +243,7 @@ let rec (inline_eq: Eff.local_env -> let eq = { src = lxm_eq ; it = (lhs, rhs) } in inline_eq node_env id_solver (eqs, locs) eq - | CallByPosEff({src=lxm_ve;it=Eff.Predef(Predef.BoolRed,sargs)}, OperEff args) -> + | CallByPosEff({src=lxm_ve;it=Eff.Predef(Predef.BoolRed,sargs)}, OperEff args) -> (* Given - 3 integers i, j, k boolref<<i,j,k>> has the profile: bool^n -> bool @@ -321,6 +322,8 @@ let rec (inline_eq: Eff.local_env -> else (eq::eq_cpt::eqs, cpt::locs) (* All the other operators *) + + | _ -> (eq::eqs, locs) @@ -328,7 +331,7 @@ let rec (inline_eq: Eff.local_env -> (* exported *) -let (iterators : Eff.local_env -> Eff.id_solver -> Eff.node_exp -> Eff.node_exp) = +and (iterators : Eff.local_env -> Eff.id_solver -> Eff.node_exp -> Eff.node_exp) = fun node_env id_solver n -> match n.def_eff with | ExternEff @@ -336,9 +339,9 @@ let (iterators : Eff.local_env -> Eff.id_solver -> Eff.node_exp -> Eff.node_exp) | BodyEff b -> Name.reset_local_var_prefix "acc"; Name.reset_local_var_prefix "cpt"; - let loc = match n.loclist_eff with None -> [] | Some l -> l in + let nv = match n.loclist_eff with None -> [] | Some l -> l in let (neqs, nv) = - List.fold_left (inline_eq node_env id_solver) ([], loc) b.eqs_eff + List.fold_left (inline_eq node_env id_solver) ([], nv) b.eqs_eff in let nb = { b with eqs_eff = List.rev neqs } in let res = diff --git a/src/lazyCompiler.ml b/src/lazyCompiler.ml index 25555aff..d3577507 100644 --- a/src/lazyCompiler.ml +++ b/src/lazyCompiler.ml @@ -1,4 +1,4 @@ -(** Time-stamp: <modified the 29/01/2009 (at 11:04) by Erwan Jahier> *) +(** Time-stamp: <modified the 03/02/2009 (at 16:05) by Erwan Jahier> *) open Lxm @@ -563,7 +563,7 @@ and (node_check_do: t -> Eff.node_key -> Lxm.t -> SymbolTab.t -> (Hashtbl.fold (fun id vi_eff acc -> acc ^ (Format.sprintf - "\n\t%s" (LicDump.string_of_var_info_eff vi_eff)) + "\n\t%s" (LicDump.string_of_var_info_eff4msg vi_eff)) ) local_env.lenv_vars "" @@ -609,9 +609,7 @@ and (node_check_do: t -> Eff.node_key -> Lxm.t -> SymbolTab.t -> let type_args id = let vi = find_var_info lxm vars id in let t_eff = GetEff.typ node_id_solver vi.it.var_type in - let _ = - if Eff.is_polymorphic t_eff then is_polymorphic := true - in + let _ = if Eff.is_polymorphic t_eff then is_polymorphic := true in let c_eff = GetEff.clock node_id_solver vi.it in let vi_eff = { var_name_eff = vi.it.var_name; @@ -754,18 +752,6 @@ and (node_check_do: t -> Eff.node_key -> Lxm.t -> SymbolTab.t -> match alias with | Predef_n((Predef.NOR_n|Predef.DIESE_n), sargs) -> raise (Compile_error (lxm, "Can not alias 'nor' nor '#', sorry")) -(* | 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_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_n(predef_op, sargs) -> let sargs_eff = @@ -787,6 +773,7 @@ and (node_check_do: t -> Eff.node_key -> Lxm.t -> SymbolTab.t -> (* does it make sense to alias when, pre, etc? *) in let (alias_node : Eff.node_exp) = make_alias_node aliased_node in + (* Check that the declared profile (if any) matches with the alias *) match node_def.it.vars with | None -> alias_node @@ -807,6 +794,7 @@ and (node_check_do: t -> Eff.node_key -> Lxm.t -> SymbolTab.t -> | _ -> alias_node ) + (* End Alias *) in let is_main_node = if !Global.main_node = "" then ( @@ -828,10 +816,10 @@ and (node_check_do: t -> Eff.node_key -> Lxm.t -> SymbolTab.t -> else res in let res_struct = - if !Global.expand_structs then - let new_res = StructArrayExpand.node local_env node_id_solver res in - UniqueOutput.check res node_def.src; - UniqueOutput.check new_res node_def.src; (* is it useful to check both?*) + if !Global.expand_structs & not (res.is_polym_eff) then + let new_res = StructArrayExpand.node node_id_solver local_env res in + UniqueOutput.check res node_def.src; + UniqueOutput.check new_res node_def.src; (* is it useful to check both? *) new_res else ( UniqueOutput.check res node_def.src; @@ -841,11 +829,11 @@ and (node_check_do: t -> Eff.node_key -> Lxm.t -> SymbolTab.t -> if not provide_flag then ( if res.is_polym_eff then - LicDump.push_on_polymorphic_node_stack res_struct + Polymorphism.push_on_polymorphic_node_stack (node_id_solver,local_env,res) else - let str = LicDump.node_of_node_exp_eff res_struct in - if not !Global.expand_nodes || is_main_node then - output_string !Global.oc str + let str = LicDump.node_of_node_exp_eff res_struct in + if not !Global.expand_nodes || is_main_node then + output_string !Global.oc str ); (* nb: we print res_struct, but we return res, because the structure and array expansion modify the node profiles. diff --git a/src/licDump.ml b/src/licDump.ml index 281fee33..9eaae95d 100644 --- a/src/licDump.ml +++ b/src/licDump.ml @@ -1,4 +1,4 @@ -(** Time-stamp: <modified the 28/01/2009 (at 10:43) by Erwan Jahier> *) +(** Time-stamp: <modified the 02/02/2009 (at 11:15) by Erwan Jahier> *) open Printf open Lxm @@ -13,9 +13,6 @@ let type_alias_table = Hashtbl.create 0 (******************************************************************************) -(* To deal with polymorphism: raised when a polymorphic expr is generated. *) -exception Polymorphic -let (poly_var : (unit -> Eff.type_) ref) = ref (fun () -> raise Polymorphic) (******************************************************************************) let (get_rank : 'a -> 'a list -> int) = @@ -123,8 +120,8 @@ and string_of_type_eff = function | Enum_type_eff (name, _) -> prefix ^ (long name) | Array_type_eff (ty, sz) -> array_alias ty sz | Struct_type_eff (name, _) -> prefix ^ (long name) - | Any -> string_of_type_eff (!poly_var ()) - | Overload -> string_of_type_eff (!poly_var ()) + | Any -> string_of_type_eff (Polymorphism.get_type ()) + | Overload -> string_of_type_eff (Polymorphism.get_type ()) and string_of_type_eff4msg = function @@ -177,7 +174,7 @@ and dump_type_alias oc = (fun type_eff alias_name -> try p ("\ntype " ^ alias_name ^ " = " ^ (string_def_of_type_eff type_eff)^";") - with Polymorphic -> () + with Polymorphism.Exc -> () ) type_alias_table @@ -219,6 +216,10 @@ and static_arg2string (sa : Eff.static_arg) = | NodeStaticArgEff (id, (long, _, _)) -> sprintf "%s" (Ident.string_of_long long) +and (string_of_var_info_eff4msg: Eff.var_info -> string) = + fun x -> + (Ident.to_string x.var_name_eff) ^ ":"^(string_of_type_eff4msg x.var_type_eff) + 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) @@ -549,21 +550,6 @@ and string_of_clock (ck : Eff.clock) = and op2string = Predef.op2string -(******************************************************************************) -let polymorphic_node_stack : Eff.node_exp Stack.t = Stack.create () - -let (push_on_polymorphic_node_stack : Eff.node_exp -> unit) = - fun n -> - Stack.push n polymorphic_node_stack - -let (unstack_polymorphic_nodes : Eff.type_ -> unit) = - fun t -> - poly_var := (fun () -> t); - while (not (Stack.is_empty polymorphic_node_stack)) do - let str = node_of_node_exp_eff (Stack.pop polymorphic_node_stack) in - output_string !Global.oc str; - done; - poly_var := (fun () -> raise Polymorphic) (*--------------------------------------------------------------------- diff --git a/src/licDump.mli b/src/licDump.mli index 39ccd9ff..0b651e1a 100644 --- a/src/licDump.mli +++ b/src/licDump.mli @@ -16,6 +16,7 @@ val type_decl: Ident.long -> Eff.type_ -> string val const_decl: Ident.long -> Eff.const -> string val string_of_var_info_eff: Eff.var_info -> string +val string_of_var_info_eff4msg: 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 @@ -30,28 +31,3 @@ val string_of_clock2 : Eff.clock -> string val string_of_val_exp_eff : Eff.val_exp -> string -(** To deal with polymorphic nodes. - - The idea is the following. As soon as we try (in LazyCompiler) to - dump a polymorphic node, we push it on a stack - (push_on_polymorphic_node_stack), instead of dumpinf it, as we have decided - that lic does not accept polymorphic nodes. - - This ougth to occur in a unique situation: when an array iterator - is called over a polymorphic operator, e.g., in - - x = map<<+,3>>([1;2;3],[1;2;3]); - - in such a situation, we do generated a polymorphic Eff.node_exp - for the expression "map<<+,3>>" (but we dont' dump it). But once - we get that node_exp (in GetEff.translate_val_exp), by unifying - the node_exp with the dynamic arguments, we know that the type - variable was an integer. - - Hence, we can now print the instanciated node (unstack_polymorphic_nodes). - - Note that it is a stack because array iterators an be nested. - -*) -val push_on_polymorphic_node_stack : Eff.node_exp -> unit -val unstack_polymorphic_nodes : Eff.type_ -> unit diff --git a/src/polymorphism.ml b/src/polymorphism.ml new file mode 100644 index 00000000..b63bf7ec --- /dev/null +++ b/src/polymorphism.ml @@ -0,0 +1,54 @@ + +open Eff + +(* exported *) +exception Exc + +let type_ref = ref None + +(* exported *) +let get_type () = + match !type_ref with + | None -> raise Exc + | Some t -> t + + +let (set_type : Eff.type_ -> unit) = + fun t -> + type_ref := Some t + +(* exported *) +let (reset_type : unit -> unit) = (* To be called in order to avoid silent bugs *) + fun () -> + type_ref := None + + +(******************************************************************************) + +let polymorphic_node_stack : (Eff.id_solver * Eff.local_env * Eff.node_exp) Stack.t = Stack.create () + +(* exported *) +let (push_on_polymorphic_node_stack : Eff.id_solver * Eff.local_env * Eff.node_exp -> unit) = + fun n -> + Stack.push n polymorphic_node_stack + +(* exported *) +let (unstack_polymorphic_nodes : + (Eff.id_solver -> Eff.local_env -> Eff.node_exp -> Eff.node_exp) -> + Eff.type_ -> (Eff.id_solver * Eff.local_env * Eff.node_exp) list) = + fun expand t -> + let rec aux l = + if Stack.is_empty polymorphic_node_stack + then + l + else + let id_solver, nenv, node = Stack.pop polymorphic_node_stack in + let node = + if !Global.expand_structs then expand id_solver nenv node else node + in + (id_solver, nenv,node)::(aux l) + in + let _ = set_type t in + let res = aux [] in + res + diff --git a/src/polymorphism.mli b/src/polymorphism.mli new file mode 100644 index 00000000..5fe070c2 --- /dev/null +++ b/src/polymorphism.mli @@ -0,0 +1,44 @@ +(** Handling polymorphic nodes. + + XXX I'm not particularly happy with the way all this is done... + + Anyway, the idea is the following. As soon as we try (in + LazyCompiler) to dump a polymorphic node, we push it on a stack + (push_on_polymorphic_node_stack), instead of dumping it, as we + have decided that lic does not accept polymorphic nodes. This + ougth to occur in a unique situation: when an array iterator is + called over a polymorphic operator, e.g., in x = + map<<+,3>>([1;2;3],[1;2;3]); + + in such a situation, we do generate a polymorphic Eff.node_exp + for the expression "map<<+,3>>" (but we don't LicDump it). But + once we get that node_exp (in GetEff.translate_val_exp), by + unifying the node_exp with the dynamic arguments, we know that + the type variable was (here, an integer). Hence, we can now + print the instanciated node (unstack_polymorphic_nodes). + + Note that it is a stack because array iterators an be nested. + +*) + + +(* To deal with polymorphism: raised when a polymorphic expr is generated. *) +exception Exc + + +val get_type : unit -> Eff.type_ + +(* Should be unnecessary, but calling it at the appriopriate + place would avoid silent bugs *) +val reset_type : unit -> unit + +val push_on_polymorphic_node_stack : + Eff.id_solver * Eff.local_env * Eff.node_exp -> unit + +(* we add the StructArrayExpand.node function as parameter of this function + to break a module dependency. +*) +val unstack_polymorphic_nodes : + (Eff.id_solver -> Eff.local_env -> Eff.node_exp -> Eff.node_exp) -> + Eff.type_ -> (Eff.id_solver * Eff.local_env * Eff.node_exp) list + diff --git a/src/structArrayExpand.ml b/src/structArrayExpand.ml index b0e7b1f2..22cc2b53 100644 --- a/src/structArrayExpand.ml +++ b/src/structArrayExpand.ml @@ -1,4 +1,4 @@ -(** Time-stamp: <modified the 29/01/2009 (at 16:56) by Erwan Jahier> *) +(** Time-stamp: <modified the 03/02/2009 (at 11:14) by Erwan Jahier> *) (* Replace structures and arrays by as many variables as necessary. Since structures can be recursive, it migth be a lot of new variables... @@ -59,13 +59,18 @@ let new_var str node_env type_eff clock_eff = let clone_var node_env vi str type_eff = let str = (Ident.to_string vi.var_name_eff) ^ str in let id = Ident.of_string (str) in + let clk_id = Ident.of_string str in + let type_eff = match type_eff with + Any | Overload -> Polymorphism.get_type () + | _ -> type_eff + in let var = { var_name_eff = id; var_nature_eff = vi.var_nature_eff; var_number_eff = vi.var_number_eff; (* this field is useless: to be removed. *) var_type_eff = type_eff; - var_clock_eff = vi.var_clock_eff; + var_clock_eff = clk_id, snd vi.var_clock_eff; } in (* Hashtbl.add node_env.lenv_vars id var; *) @@ -75,6 +80,7 @@ let clone_var node_env vi str type_eff = let rec (is_a_basic_type : Eff.type_ -> bool) = function | Array_type_eff _ | Struct_type_eff _ -> false + | Any | Overload -> is_a_basic_type (Polymorphism.get_type ()) | _ -> true let soi = string_of_int @@ -94,12 +100,14 @@ let (expand_var : string -> Eff.type_ -> (string * Eff.type_) list) = fun prefix teff -> let rec aux prefix acc teff = match teff with - | Any | Overload -> assert false (* should not occur *) + | Any | Overload -> + let teff = Polymorphism.get_type () in + (prefix,teff)::acc | Bool_type_eff | Int_type_eff | Real_type_eff | External_type_eff _ - | Enum_type_eff(_) -> (prefix,teff)::acc + | Enum_type_eff(_) -> (prefix,teff)::acc | Array_type_eff(teff_elt,i) -> let rec unfold acc cpt = if cpt = i then acc else @@ -120,7 +128,6 @@ let (expand_var : string -> Eff.type_ -> (string * Eff.type_) list) = let (index_list_of_slice_info : Eff.slice_info -> int list) = fun si -> - let sign = if si.se_step > 0 then 1 else -1 in let rec aux acc cpt = if ((si.se_step > 0 & cpt > si.se_last) || (si.se_step < 0 & cpt < si.se_last)) then acc else aux (cpt::acc) (cpt + si.se_step) @@ -169,9 +176,12 @@ let rec (gen_var_trees : (string -> Eff.type_ -> 'a) -> string -> Eff.type_ -> 'a var_tree) = fun make_leave prefix teff -> match teff with + | Any | Overload -> + let teff = Polymorphism.get_type () in + L (make_leave prefix teff) + | Bool_type_eff | Int_type_eff | Real_type_eff | External_type_eff _ | Enum_type_eff(_) - | Any | Overload (* should not occur *) -> L (make_leave prefix teff) @@ -280,7 +290,22 @@ and (var_trees_of_val_exp : Eff.local_env -> Eff.id_solver -> acc -> Eff.val_exp | _, (S _ | L _) -> assert false ) | IDENT idref -> - let vi = id_solver.id2var idref lxm in + let vi = + try id_solver.id2var idref lxm + with _ -> + raise (Errors.Compile_error( + lxm, + ("\n*** '"^(Ident.string_of_idref idref)^ + "': Unknown variable.\n*** Current variables are: " ^ + (Hashtbl.fold + (fun id vi_eff acc -> + acc ^ (Format.sprintf + "\n\t%s" (LicDump.string_of_var_info_eff4msg vi_eff)) + ) + nenv.lenv_vars + "" + )))) + in acc, gen_var_trees (make_val_exp nenv lxm vi) "" vi.var_type_eff | WITH(_) | HAT(_) | CONCAT | ARRAY(_) @@ -352,7 +377,8 @@ and (expand_val_exp: Eff.local_env -> Eff.id_solver -> acc -> val_exp -> | ARRAY_SLICE (_) | IDENT _ -> let acc, vt = try var_trees_of_val_exp n_env id_solver acc ve - with _ -> assert false (* just a defense against nth and assoc *) + with (Not_found | Failure _) -> + assert false (* just a defense against nth and assoc *) in TUPLE, acc, flatten_var_tree vt in @@ -385,7 +411,9 @@ and (expand_assert: and (expand_var_info: Eff.local_env -> Eff.id_solver -> var_info list * acc -> var_info -> var_info list * acc) = fun nenv id_solver (vil, acc) vi -> - match vi.var_type_eff with + let rec aux teff = + match teff with + | Any | Overload -> aux (Polymorphism.get_type ()) | Struct_type_eff (name, fl) -> List.fold_left (fun (vil,acc) (fn, (ft,_)) -> @@ -414,10 +442,11 @@ and (expand_var_info: Eff.local_env -> Eff.id_solver -> var_info list * acc -> aux 0 (vil,acc) | _ -> vi::vil, acc + in + aux vi.var_type_eff - -let (node : Eff.local_env -> Eff.id_solver -> Eff.node_exp -> Eff.node_exp) = - fun n_env is n -> +let (node : Eff.id_solver -> Eff.local_env -> Eff.node_exp -> Eff.node_exp) = + fun is n_env n -> match n.def_eff with | ExternEff | AbstractEff -> n @@ -426,9 +455,35 @@ let (node : Eff.local_env -> Eff.id_solver -> Eff.node_exp -> Eff.node_exp) = let inlist = n.inlist_eff in let outlist = n.outlist_eff in let acc = ([],[],[]) in +(* let _ = *) +(* print_string *) +(* ("\n*** nenv.lenv_vars (avant) = " ^ *) +(* (Hashtbl.fold *) +(* (fun id vi_eff acc -> *) +(* acc ^ (Format.sprintf *) +(* "\n\t%s" (LicDump.string_of_var_info_eff4msg vi_eff)) *) +(* ) *) +(* n_env.lenv_vars *) +(* "" *) +(* )); *) +(* flush stdout *) +(* in *) let inlist, acc = List.fold_left (expand_var_info n_env is) ([],acc) inlist in let outlist, acc = List.fold_left (expand_var_info n_env is) ([],acc) outlist in let loclist, acc = List.fold_left (expand_var_info n_env is) ([],acc) loclist in + +(* let _ = *) +(* print_string ("\n*** nenv.lenv_vars (avant) = "^ *) +(* (Hashtbl.fold *) +(* (fun id vi_eff acc -> *) +(* acc ^ (Format.sprintf *) +(* "\n\t%s" (LicDump.string_of_var_info_eff4msg vi_eff)) *) +(* ) *) +(* n_env.lenv_vars *) +(* "" *) +(* )); *) +(* flush stdout *) +(* in *) let acc = List.fold_left (expand_eq n_env is) acc b.eqs_eff in let acc = List.fold_left (expand_assert n_env is) acc b.asserts_eff in let (asserts,neqs, nv) = acc in diff --git a/src/structArrayExpand.mli b/src/structArrayExpand.mli index e805f76f..3b6f6e4e 100644 --- a/src/structArrayExpand.mli +++ b/src/structArrayExpand.mli @@ -2,4 +2,4 @@ (** Expand strutures and arrays *) -val node : Eff.local_env -> Eff.id_solver -> Eff.node_exp -> Eff.node_exp +val node : Eff.id_solver -> Eff.local_env -> Eff.node_exp -> Eff.node_exp -- GitLab