diff --git a/src/ast2lic.ml b/src/ast2lic.ml index df6c1c0cf8220fa5a93b1f7a13d2b6448712e53d..faec80a76f8979fdce0637422c07fddf27761837 100644 --- a/src/ast2lic.ml +++ b/src/ast2lic.ml @@ -1,4 +1,4 @@ -(* Time-stamp: <modified the 13/12/2012 (at 11:32) by Erwan Jahier> *) +(* Time-stamp: <modified the 20/12/2012 (at 14:15) by Erwan Jahier> *) open Lxm @@ -329,6 +329,7 @@ and (translate_left_part : id_solver -> AstCore.left_part -> Lic.left) = let teff = Lic.type_of_left lp_eff in let lxm = vef.src in match teff with + | Abstract_type_eff(_,Array_type_eff(teff_elt, size)) | Array_type_eff(teff_elt, size) -> let index = EvalConst.eval_array_index id_solver vef.it lxm in LeftArrayLic(lp_eff, index, teff_elt) @@ -339,6 +340,7 @@ and (translate_left_part : id_solver -> AstCore.left_part -> Lic.left) = let lp_eff = translate_left_part id_solver lp in let teff = Lic.type_of_left lp_eff in match teff with + | Abstract_type_eff(_,Array_type_eff(teff_elt, size)) | Array_type_eff(teff_elt, size) -> let sieff = translate_slice_info id_solver sif.it sif.src in let size_slice = sieff.se_width in diff --git a/src/astCore.ml b/src/astCore.ml index b4e4d8b105b7df407a3fe691128cc0925108453f..dae421999edc586a0f1490c6b3da419f4b52052b 100644 --- a/src/astCore.ml +++ b/src/astCore.ml @@ -1,4 +1,4 @@ -(* Time-stamp: <modified the 13/12/2012 (at 11:31) by Erwan Jahier> *) +(* Time-stamp: <modified the 20/12/2012 (at 16:29) by Erwan Jahier> *) (** (Raw) Abstract syntax tree of source Lustre Core programs. *) @@ -202,3 +202,7 @@ let rec string_of_type_exp x = | Array_type_exp (te, sz) -> (string_of_type_exp te) ^ "^ ..." +let string_of_var_nature = function + | VarInput -> "input" + | VarOutput -> "output" + | VarLocal -> "local" diff --git a/src/compile.ml b/src/compile.ml index 98bc64af400a11e901dc4f4c36f05fa50dee6c37..a7ac7a9132c928292437f9d9d5c6ff53fafbec12 100644 --- a/src/compile.ml +++ b/src/compile.ml @@ -1,4 +1,4 @@ -(* Time-stamp: <modified the 19/12/2012 (at 17:23) by Erwan Jahier> *) +(* Time-stamp: <modified the 20/12/2012 (at 15:25) by Erwan Jahier> *) open Lxm @@ -40,20 +40,31 @@ let (doit : AstV6.pack_or_model list -> Ident.idref option -> LicPrg.t) = LicTab.compile_node lic_tab main_node in let zelic = LicTab.to_lic_prg lic_tab in - (* élimination polymorphisme surcharge *) + (* élimination polymorphisme surcharge *) let zelic = L2lRmPoly.doit zelic in - (* alias des types array *) + (* alias des types array *) let zelic = L2lAliasType.doit zelic in let zelic = if not !Global.inline_iterator then zelic else (* Array and struct expansion: to do after polymorphism elimination *) L2lExpandMetaOp.doit zelic in - let zelic = if not !Global.one_op_per_equation then zelic else + let zelic = + if + not !Global.one_op_per_equation + && not !Global.expand_nodes (* expand performs not fixpoint, so it will work + only if we have one op per equation...*) + then + zelic + else (* Split des equations (1 eq = 1 op) *) L2lSplit.doit zelic in + let zelic = if not !Global.expand_nodes then zelic else + L2lExpandNodes.doit zelic + in let zelic = if not !Global.expand_structs then zelic else (* Array and struct expansion: to do after polymorphism elimination *) L2lExpandArrays.doit zelic in + L2lCheckOutputs.doit zelic; zelic diff --git a/src/l2lCheckOutputs.ml b/src/l2lCheckOutputs.ml index 3753f09769b519f8589e410375b788b86a977fd3..773bbd8a956445a27aaadb2d7376e5161fb2e6b2 100644 --- a/src/l2lCheckOutputs.ml +++ b/src/l2lCheckOutputs.ml @@ -1,4 +1,4 @@ -(* Time-stamp: <modified the 13/12/2012 (at 09:55) by Erwan Jahier> *) +(* Time-stamp: <modified the 20/12/2012 (at 17:14) by Erwan Jahier> *) open Lxm open Errors @@ -17,35 +17,34 @@ and filter = | Faccess of Ident.t * Lic.type_ | Aaccess of int * Lic.type_ - -let rec (left_eff_to_filtered_left: Lic.left -> filtered_left) = +let rec (left_eff_to_filtered_left: Lic.left srcflagged -> filtered_left) = fun le -> - let rec (aux : Lic.type_ -> filter list -> Lic.left -> filtered_left) = + let rec (aux : Lic.type_ -> filter list -> Lic.left -> filtered_left) = fun te_top acc le -> match le with - | LeftVarLic (v,lxm) -> v, lxm, acc - | LeftFieldLic(le,id,te) -> aux te (Faccess(id,te)::acc) le - | LeftArrayLic(le,i,te) -> aux te (Aaccess(i,te)::acc) le - | LeftSliceLic(le,si,te) -> - aux te (Slice(si.se_first,si.se_last,si.se_step,te)::acc) le + | LeftVarLic (v,lxm) -> v, lxm, acc + | LeftFieldLic(le,id,te) -> aux te (Faccess(id,te)::acc) le + | LeftArrayLic(le,i,te) -> aux te (Aaccess(i,te)::acc) le + | LeftSliceLic(le,si,te) -> + aux te (Slice(si.se_first,si.se_last,si.se_step,te)::acc) le in - let te_top = (Lic.var_info_of_left le).var_type_eff in - let (v,lxm,f) = aux te_top [] le in + let te_top = (Lic.var_info_of_left le.it).var_type_eff in + let (v,lxm,f) = aux te_top [] le.it in let (_,f) = (* we don't want to associate to each accessors the type of the - « accessed elements », but its own type. E.g., if "t" is an - array of bool, we want to associate 't[0]' and an array of - bool, and not to a bool. *) + « accessed elements », but its own type. E.g., if "t" is an + array of bool, we want to associate 't[0]' and an array of + bool, and not to a bool. *) List.fold_left - (fun (te_top,acc) el -> - match el with - | Slice(i,j,k,te) -> te, (Slice(i,j,k,te_top))::acc - | Faccess(id,te) -> te, (Faccess(id,te_top))::acc - | Aaccess(i,te) -> te, (Aaccess(i,te_top))::acc - ) - (te_top,[]) - f + (fun (te_top,acc) el -> + match el with + | Slice(i,j,k,te) -> te, (Slice(i,j,k,te_top))::acc + | Faccess(id,te) -> te, (Faccess(id,te_top))::acc + | Aaccess(i,te) -> te, (Aaccess(i,te_top))::acc + ) + (te_top,[]) + f in - (v,lxm, List.rev f) + (v,lxm, List.rev f) @@ -67,12 +66,12 @@ let (vds_to_undefined_vars : string -> var_def_state -> string list) = | VDS_def -> acc | VDS_undef -> v::acc | VDS_struct(fl) -> - List.fold_left (fun acc (id,vds) -> aux vds (v^"."^(id2str id)) acc) acc fl + List.fold_left (fun acc (id,vds) -> aux vds (v^"."^(id2str id)) acc) acc fl | VDS_array(a) -> fst - (Array.fold_left - (fun (acc,i) vds -> aux vds (v^"["^(int2str i) ^"]") acc, i+1) (acc,0) a) + (Array.fold_left + (fun (acc,i) vds -> aux vds (v^"["^(int2str i) ^"]") acc, i+1) (acc,0) a) in - aux vds v [] + aux vds v [] (* Returns the list of defined variables *) let (vds_to_defined_vars : string -> var_def_state -> string list) = @@ -81,12 +80,12 @@ let (vds_to_defined_vars : string -> var_def_state -> string list) = | VDS_def -> v::acc | VDS_undef -> acc | VDS_struct(fl) -> - List.fold_left (fun acc (id,vds) -> aux vds (v^"."^(id2str id)) acc) acc fl + List.fold_left (fun acc (id,vds) -> aux vds (v^"."^(id2str id)) acc) acc fl | VDS_array(a) -> fst - (Array.fold_left - (fun (acc,i) vds -> aux vds (v^"["^(int2str i) ^"]") acc, i+1) (acc,0) a) + (Array.fold_left + (fun (acc,i) vds -> aux vds (v^"["^(int2str i) ^"]") acc, i+1) (acc,0) a) in - aux vds v [] + aux vds v [] (*********************************************************************************) (** This is main function: it computes a new [var_def_state] from an @@ -95,147 +94,181 @@ 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 -> - if vds = VDS_def then - let msg = "\n*** Variable " ^ v ^ " is already defined." in - raise (Compile_error(lxm, msg)) - else - match filters with - | [] -> - let already_def_vars = vds_to_defined_vars v vds in - if already_def_vars <> [] then - let msg = - "\n*** Variable " ^ v ^ " is already partly defined (" ^ - (String.concat "," (already_def_vars)) ^ ")." - in - raise (Compile_error(lxm, msg)) - else - VDS_def - | Slice(i,j,k,te)::tail -> update_slice v i j k tail - (match vds with - | VDS_array(a) -> a - | VDS_undef -> undef_array_of_type te - | _ -> assert false (* by type checking *) - ) - | Aaccess(i,te)::tail -> update_array_access v i tail - (match vds with - | VDS_array(a) -> a - | VDS_undef -> undef_array_of_type te - | _ -> assert false (* by type checking *) - ) - | Faccess(id,te)::tail -> update_field_access v id tail - (match vds with - | VDS_struct(fl) -> fl - | VDS_undef -> undef_struct_of_type te - | _ -> assert false (* by type checking *) - ) + if vds = VDS_def then + let msg = "\n*** Variable " ^ v ^ " is already defined." in + raise (Compile_error(lxm, msg)) + else + match filters with + | [] -> + let already_def_vars = vds_to_defined_vars v vds in + if already_def_vars <> [] then + let msg = + "\n*** Variable " ^ v ^ " is already partly defined (" ^ + (String.concat "," (already_def_vars)) ^ ")." + in + raise (Compile_error(lxm, msg)) + else + VDS_def + | Slice(i,j,k,te)::tail -> update_slice v i j k tail + (match vds with + | VDS_array(a) -> a + | VDS_undef -> undef_array_of_type te + | _ -> assert false (* by type checking *) + ) + | Aaccess(i,te)::tail -> update_array_access v i tail + (match vds with + | VDS_array(a) -> a + | VDS_undef -> undef_array_of_type te + | _ -> assert false (* by type checking *) + ) + | Faccess(id,te)::tail -> update_field_access v id tail + (match vds with + | VDS_struct(fl) -> fl + | VDS_undef -> undef_struct_of_type te + | _ -> assert false (* by type checking *) + ) and undef_array_of_type = function + | Abstract_type_eff(_, Array_type_eff(_,size)) | Array_type_eff(_,size) -> Array.make size VDS_undef - | _ -> assert false - + | t -> + prerr_string ((Lic.string_of_type t) ^ " outh to be an array\n"); + flush stderr; + assert false + and undef_struct_of_type = function | Struct_type_eff(_,fl) -> List.map (fun (id,_) -> id, VDS_undef) fl | _ -> assert false - + and array_for_all pred a = Array.fold_left (fun acc x -> acc && (pred x)) true a and update_slice v i j k filters a = let v = v^"["^(int2str i)^ ".."^(int2str j)^ - (if k=1 then "]" else " step "^(int2str k)^"]") + (if k=1 then "]" else " step "^(int2str k)^"]") in let sub_size = ((j-i)/k+1) in let sub_a = Array.make sub_size VDS_undef in let vds = - for l=0 to sub_size-1 do sub_a.(l) <- a.(i+l*k) done; - update_vds v (VDS_array sub_a) filters + for l=0 to sub_size-1 do sub_a.(l) <- a.(i+l*k) done; + update_vds v (VDS_array sub_a) filters in - (match vds with - | VDS_undef - | VDS_struct(_) -> assert false - | VDS_def -> for l=0 to sub_size-1 do a.(i+l*k) <- VDS_def done - | VDS_array sa -> for l=0 to sub_size-1 do a.(i+l*k) <- sub_a.(l) done - ); - if array_for_all (fun elt -> elt = VDS_def) a then VDS_def else VDS_array(a) + (match vds with + | VDS_undef + | VDS_struct(_) -> assert false + | VDS_def -> for l=0 to sub_size-1 do a.(i+l*k) <- VDS_def done + | VDS_array sa -> for l=0 to sub_size-1 do a.(i+l*k) <- sub_a.(l) done + ); + if array_for_all (fun elt -> elt = VDS_def) a then VDS_def else VDS_array(a) and update_array_access v i filters a = let v = v ^ "[" ^ (int2str i) ^ "]" in let vds_i = update_vds v a.(i) filters in - a.(i) <- vds_i; - if array_for_all (fun elt -> elt = VDS_def) a then VDS_def else VDS_array(a) + a.(i) <- vds_i; + if array_for_all (fun elt -> elt = VDS_def) a then VDS_def else VDS_array(a) and update_field_access v id filters fl = let vds_id = List.assoc id fl in let v = v ^ "." ^ (id2str id) in let vds = update_vds v vds_id filters in let fl = replace_field id vds fl in - if List.for_all (fun (_,vds) -> vds = VDS_def) fl - then VDS_def - else VDS_struct(fl) + if List.for_all (fun (_,vds) -> vds = VDS_def) fl + then VDS_def + else VDS_struct(fl) and replace_field fn new_fv l = match l with - | (id,fv)::tail -> - if id = fn then (id,new_fv)::tail - else (id,fv)::(replace_field fn new_fv tail) - | [] -> assert false (* fn is necessarily in l *) + | (id,fv)::tail -> + if id = fn then (id,new_fv)::tail + else (id,fv)::(replace_field fn new_fv tail) + | [] -> assert false (* fn is necessarily in l *) in let res = update_vds (id2str v.var_name_eff) vds filters in - res + res (*********************************************************************************) (** Sort out the Lic.left according to the variable they define. *) -module VarMap = Map.Make(struct type t = Lic.var_info let compare = compare end) -let (partition_var : Lic.left list -> (Lic.left list) VarMap.t) = + +module VarMap = Map.Make( + struct + type t = Lic.var_info + let compare = Lic.compare_var_info +(* array and array alias migth *) + end) + +let (partition_var : Lic.left srcflagged list -> (Lic.left srcflagged list) VarMap.t) = fun l -> let f tab le = - let v = Lic.var_info_of_left le in - try VarMap.add v (le::(VarMap.find v tab)) tab - with Not_found -> VarMap.add v [le] tab + let v = Lic.var_info_of_left le.it in + try VarMap.add v (le::(VarMap.find v tab)) tab + with Not_found -> VarMap.add v [le] tab in - List.fold_left f VarMap.empty l + List.fold_left f VarMap.empty l (*********************************************************************************) (* exported *) -let (check : Lic.node_exp -> Lxm.t -> unit) = - fun node lxm -> +let (check_node : Lic.node_exp -> unit) = + fun node -> 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 -> Lic.var_info -> Lic.left list -> unit) = - fun lxm v lel -> - let ell = List.map left_eff_to_filtered_left lel in - match List.fold_left update_var_def_state VDS_undef (List.rev ell) with - | VDS_def -> () - | vds -> - let msg = "\n*** Undefined variable(s): " ^ - (String.concat ", " (vds_to_undefined_vars (id2str v.var_name_eff) vds)) - in - raise (Compile_error(lxm, msg)) + let (check_one_var : Lic.var_info -> Lic.left srcflagged list -> unit) = + fun v lel -> + let ell = List.map left_eff_to_filtered_left lel in + match List.fold_left update_var_def_state VDS_undef (List.rev ell) with + | VDS_def -> () + | vds -> + let msg = "\n*** Undefined variable(s): " ^ + (String.concat ", " (vds_to_undefined_vars (id2str v.var_name_eff) vds)) + in + let lxm = (List.hd lel).src in + raise (Compile_error(lxm, msg)) in - match node.def_eff with - | ExternLic - | MetaOpLic _ - | AbstractLic _ -> () - | BodyLic{ eqs_eff = eql } -> - let lel = List.flatten (List.map (fun {it=(left,_)} -> left) eql) in - let lel_map = partition_var lel in - (* Check that one does not define an input *) - VarMap.iter - (fun v _ -> - if v.var_nature_eff = AstCore.VarInput then - let msg = "\n*** Error; " ^(id2str v.var_name_eff) ^ - " is an input, and thus cannot be defined." - in - raise (Compile_error(lxm, msg)) - ) - lel_map; - List.iter - (fun v -> - try check_one_var lxm v (VarMap.find v lel_map) - with Not_found -> - let msg = "\n*** Undefined variable: " ^ (id2str v.var_name_eff) - in - raise (Compile_error(lxm, msg)) - ) - vars_to_check + match node.def_eff with + | ExternLic + | MetaOpLic _ + | AbstractLic _ -> () + | BodyLic{ eqs_eff = eql } -> + let lel = + List.flatten + (List.map + (fun {it=(left,_);src=lxm} -> + List.map (fun l -> Lxm.flagit l lxm) left) + eql) + in + let lel_map = partition_var lel in + (* Check that one does not define an input *) + VarMap.iter + (fun v lel -> + if v.var_nature_eff = AstCore.VarInput then + let msg = "\n*** Error; " ^(id2str v.var_name_eff) ^ + " is an input, and thus cannot be defined." + in + let lxm = (List.hd lel).src in + raise (Compile_error(lxm, msg)) + ) + lel_map; + List.iter + (fun v -> + try check_one_var v (VarMap.find v lel_map) + with Not_found -> + let msg = "\n*** " ^ + (id2str v.var_name_eff) ^ + " is not defined. Defined variables are: "^ + (String.concat ", " + (List.map (fun (v,_v) -> id2str v.var_name_eff) + (VarMap.bindings lel_map))) + in + raise (Compile_error(node.lxm, msg)) + ) + vars_to_check + +(* exported *) +let (doit : LicPrg.t -> unit) = + fun inprg -> + let rec (do_node : Lic.node_key -> Lic.node_exp -> unit) = + fun _nk ne -> + check_node ne + in + LicPrg.iter_nodes do_node inprg + diff --git a/src/l2lCheckOutputs.mli b/src/l2lCheckOutputs.mli index 4cb419a9b9215437fa833013024d0a90b44930c1..1059a5fb7f9138b7a19c2a19deae692bdff5fcc3 100644 --- a/src/l2lCheckOutputs.mli +++ b/src/l2lCheckOutputs.mli @@ -1,6 +1,7 @@ -(* Time-stamp: <modified the 12/12/2012 (at 17:40) by Erwan Jahier> *) +(* Time-stamp: <modified the 20/12/2012 (at 10:57) 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 to define an input. *) -val check : Lic.node_exp -> Lxm.t -> unit +val check_node : Lic.node_exp -> unit +val doit : LicPrg.t -> unit diff --git a/src/l2lExpandArrays.ml b/src/l2lExpandArrays.ml index 00b1a9849f1fa027bb82c55b323b5b888c91118a..0cbbed70ef1193fbc5c8cadb7a3473e9de0f6401 100644 --- a/src/l2lExpandArrays.ml +++ b/src/l2lExpandArrays.ml @@ -1,4 +1,4 @@ -(** Time-stamp: <modified the 18/12/2012 (at 15:54) by Erwan Jahier> *) +(** Time-stamp: <modified the 20/12/2012 (at 16:03) 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... @@ -625,7 +625,7 @@ let rec (doit : LicPrg.t -> LicPrg.t) = let lctx = { idgen = LicPrg.fresh_var_id_generator inprg ne; node = ne; - prg = outprg; + prg = inprg; } in let ne = node lctx ne in diff --git a/src/l2lExpandMetaOp.ml b/src/l2lExpandMetaOp.ml index 0f9c15347b69a226d3ff0c9b5d77602eff5d0235..02fd8159ba00ce096efb7ebc67f11b661b6f0579 100644 --- a/src/l2lExpandMetaOp.ml +++ b/src/l2lExpandMetaOp.ml @@ -1,4 +1,4 @@ -(** Time-stamp: <modified the 20/12/2012 (at 09:49) by Erwan Jahier> *) +(** Time-stamp: <modified the 20/12/2012 (at 16:03) by Erwan Jahier> *) open Lxm open Lic @@ -369,7 +369,7 @@ let rec (node : local_ctx -> Lic.node_exp -> Lic.node_exp) = | BodyLic b -> n (* exported *) -and (doit : LicPrg.t -> LicPrg.t) = +let (doit : LicPrg.t -> LicPrg.t) = fun inprg -> let outprg = LicPrg.empty in (** types and constants do not change *) @@ -381,7 +381,7 @@ and (doit : LicPrg.t -> LicPrg.t) = let lctx = { idgen = LicPrg.fresh_var_id_generator inprg ne; node = ne; - prg = outprg; + prg = inprg; } in let ne = node lctx ne in diff --git a/src/l2lExpandNodes.ml b/src/l2lExpandNodes.ml index 9eeb0172e317b7ee66a5076b32ba036132decf8b..967743c325ff905e1424ac1663432938ce1d95cc 100644 --- a/src/l2lExpandNodes.ml +++ b/src/l2lExpandNodes.ml @@ -1,16 +1,25 @@ -(* Time-stamp: <modified the 13/12/2012 (at 11:32) by Erwan Jahier> *) +(* Time-stamp: <modified the 20/12/2012 (at 16:02) by Erwan Jahier> *) open Lxm open Lic open AstPredef +let dbg=Some (Verbose.get_flag "en") + +(* pack useful info into a single struct *) +type local_ctx = { + idgen : LicPrg.id_generator; + node : Lic.node_exp; + prg : LicPrg.t; +} + (********************************************************************************) (* stuff to create fresh var names. XXX code dupl. with Split.new_var *) -let new_var str ze_env type_eff clock_eff = +let new_var str lctx type_eff clock_eff = let id = Ident.of_string (LicName.new_local_var str) in (* let id = Ident.of_string (LicName.new_local_var "h") in *) let var = @@ -23,7 +32,6 @@ let new_var str ze_env type_eff clock_eff = var_clock_eff = clock_eff; } in - Hashtbl.add ze_env.local.lenv_vars id var; var (********************************************************************************) @@ -32,14 +40,14 @@ let get_locals node = | None -> [] | Some l -> l -let rec (get_node_body : Lic.node_env -> Lic.node_exp -> Lic.node_body option) = - fun ze_env node -> +let rec (get_node_body : local_ctx -> Lic.node_exp -> Lic.node_body option) = + fun lctx node -> match node.def_eff with | ExternLic | AbstractLic None -> None | AbstractLic (Some node) -> assert false | BodyLic node_body -> Some node_body - | MetaOpLic _ -> assert false + | MetaOpLic _ -> None (********************************************************************************) type subst = (var_info * var_info) list @@ -48,7 +56,7 @@ let rec (substitute : fun s { it = (lhs,ve) ; src = lxm } -> let lhs = List.map (subst_in_left s) lhs in let newve = subst_in_val_exp s ve in - { it = (lhs,newve) ; src = lxm } + { it = (lhs,newve) ; src = lxm } and subst_in_left s left = match left with @@ -62,42 +70,42 @@ and (subst_in_val_exp : subst -> val_exp -> val_exp) = let newve = { ve with ve_core = match ve.ve_core with - | CallByPosLic (by_pos_op, OperLic vel) -> - let lxm = by_pos_op.src in - let by_pos_op = by_pos_op.it in - let vel = List.map (subst_in_val_exp s) vel in - let by_pos_op = match by_pos_op with - | CONST_REF idl -> CONST_REF idl - | VAR_REF id -> - let id' = - try - let var = snd(List.find (fun (v,_) -> v.var_name_eff = id) s) in - var.var_name_eff - with Not_found -> id - in - VAR_REF id' - - | WITH(ve) -> WITH(subst_in_val_exp s ve) - | HAT(i,ve) -> HAT(i, subst_in_val_exp s ve) - | ARRAY(vel) -> ARRAY(List.map (subst_in_val_exp s) vel) - | WHEN(AstCore.Base) -> WHEN(AstCore.Base) - | WHEN(AstCore.NamedClock {src=lxm;it=(cc,cv)}) -> - let var = snd(List.find (fun (v,_) -> v.var_name_eff = cv) s) in - let cv = var.var_name_eff in - WHEN(AstCore.NamedClock {src=lxm;it=(cc,cv)}) - | PREDEF_CALL _| CALL _ | PRE | ARROW | FBY | CURRENT | TUPLE - | CONCAT | STRUCT_ACCESS _ | ARRAY_ACCES _ | ARRAY_SLICE _ | MERGE _ - (* | CONST _ *) - -> by_pos_op - in - CallByPosLic(Lxm.flagit by_pos_op lxm, OperLic vel) - - | CallByNameLic(by_name_op, fl) -> - let fl = List.map (fun (id,ve) -> (id, subst_in_val_exp s ve)) fl in - CallByNameLic(by_name_op, fl) + | CallByPosLic (by_pos_op, OperLic vel) -> + let lxm = by_pos_op.src in + let by_pos_op = by_pos_op.it in + let vel = List.map (subst_in_val_exp s) vel in + let by_pos_op = match by_pos_op with + | CONST_REF idl -> CONST_REF idl + | VAR_REF id -> + let id' = + try + let var = snd(List.find (fun (v,_) -> v.var_name_eff = id) s) in + var.var_name_eff + with Not_found -> id + in + VAR_REF id' + + | WITH(ve) -> WITH(subst_in_val_exp s ve) + | HAT(i,ve) -> HAT(i, subst_in_val_exp s ve) + | ARRAY(vel) -> ARRAY(List.map (subst_in_val_exp s) vel) + | WHEN(AstCore.Base) -> WHEN(AstCore.Base) + | WHEN(AstCore.NamedClock {src=lxm;it=(cc,cv)}) -> + let var = snd(List.find (fun (v,_) -> v.var_name_eff = cv) s) in + let cv = var.var_name_eff in + WHEN(AstCore.NamedClock {src=lxm;it=(cc,cv)}) + | PREDEF_CALL _| CALL _ | PRE | ARROW | FBY | CURRENT | TUPLE + | CONCAT | STRUCT_ACCESS _ | ARRAY_ACCES _ | ARRAY_SLICE _ | MERGE _ + (* | CONST _ *) + -> by_pos_op + in + CallByPosLic(Lxm.flagit by_pos_op lxm, OperLic vel) + + | CallByNameLic(by_name_op, fl) -> + let fl = List.map (fun (id,ve) -> (id, subst_in_val_exp s ve)) fl in + CallByNameLic(by_name_op, fl) } in - newve + newve let mk_loc_subst = List.combine @@ -113,18 +121,18 @@ type acc = * (Lic.eq_info srcflagged) list (* equations *) * Lic.var_info list (* new local vars *) -let (mk_fresh_loc : Lic.node_env -> var_info -> var_info) = - fun ze_env v -> - new_var (Ident.to_string v.var_name_eff) ze_env v.var_type_eff v.var_clock_eff +let (mk_fresh_loc : local_ctx -> var_info -> var_info) = + fun lctx v -> + new_var (Ident.to_string v.var_name_eff) lctx v.var_type_eff v.var_clock_eff -let (mk_input_subst: Lic.node_env -> Lxm.t -> var_info list -> +let (mk_input_subst: local_ctx -> Lxm.t -> var_info list -> Lic.val_exp list -> acc -> subst * acc) = - fun ze_env lxm vl vel acc -> + fun lctx lxm vl vel acc -> List.fold_left2 (fun (s,(a_acc,e_acc,v_acc)) v ve -> (* we create a new var for each node argument, which is a little bit « bourrin » if ever ve is a simple ident... *) - let nv = mk_fresh_loc ze_env v in + let nv = mk_fresh_loc lctx v in let neq = [LeftVarLic(nv,lxm)],ve in let neq = flagit neq lxm in (v,nv)::s,(a_acc, neq::e_acc, nv::v_acc) @@ -134,15 +142,15 @@ let (mk_input_subst: Lic.node_env -> Lxm.t -> var_info list -> vel (* create fresh vars if necessary *) -let (mk_output_subst : Lic.node_env -> Lxm.t -> var_info list -> Lic.left list -> +let (mk_output_subst : local_ctx -> Lxm.t -> var_info list -> Lic.left list -> acc -> subst * acc) = - fun ze_env lxm vl leftl acc -> + fun lctx lxm vl leftl acc -> List.fold_left2 (fun (s,acc) v left -> match left with | LeftVarLic(v2,lxm) -> (v,v2)::s, acc | _ -> - let nv = mk_fresh_loc ze_env v in + let nv = mk_fresh_loc lctx v in let nv_id = nv.var_name_eff in let nve = { ve_core = CallByPosLic({it=VAR_REF nv_id;src = lxm },OperLic []); @@ -166,61 +174,74 @@ let (mk_output_subst : Lic.node_env -> Lxm.t -> var_info list -> Lic.left list - vl leftl -let rec (expand_eq : Lic.node_env -> acc -> Lic.eq_info Lxm.srcflagged -> acc) = - fun ze_env (asserts, eqs, locs) { src = lxm_eq ; it = eq } -> - match expand_eq_aux ze_env eq with +let rec (expand_eq : local_ctx -> acc -> Lic.eq_info Lxm.srcflagged -> acc) = + fun lctx (asserts, eqs, locs) { src = lxm_eq ; it = eq } -> + match expand_eq_aux lctx eq with | None -> asserts, { src = lxm_eq ; it = eq }::eqs, locs | Some(nasserts, neqs, nlocs) -> - List.rev_append nasserts asserts, - List.rev_append neqs eqs, - List.rev_append nlocs locs + List.rev_append nasserts asserts, + List.rev_append neqs eqs, + List.rev_append nlocs locs -and (expand_eq_aux: Lic.node_env -> Lic.eq_info -> acc option)= - fun ze_env (lhs,ve) -> +and (expand_eq_aux: local_ctx -> Lic.eq_info -> acc option)= + fun lctx (lhs,ve) -> match ve.ve_core with | CallByPosLic( { it = Lic.CALL node_key ; src = lxm }, OperLic vel) -> - let node = UglyStuff.node_exp_of_node_key ze_env.global node_key.it lxm in - let node = flagit node lxm in - let node = match node.it.def_eff with - | AbstractLic (Some n) -> { it = n ; src = lxm } - | _ -> node - in - if - let nname = Ident.string_of_long2 (fst node.it.node_key_eff) in - (List.mem nname !Global.dont_expand_nodes) - then - None - else - (match get_node_body ze_env node.it with - | None -> None - | Some node_body -> - let node_eqs = node_body.eqs_eff - and asserts = node_body.asserts_eff in - let node = node.it in - let node_locs = get_locals node in - let fresh_locs = List.map (mk_fresh_loc ze_env) node_locs in - let acc = [],[],fresh_locs in - let is,acc = mk_input_subst ze_env lxm node.inlist_eff vel acc in - let os,acc = mk_output_subst ze_env lxm node.outlist_eff lhs acc in - let ls = mk_loc_subst node_locs fresh_locs in - let s = List.rev_append is (List.rev_append os ls) in - let node_eqs = List.map (substitute s) node_eqs in - let subst_assert x = Lxm.flagit (subst_in_val_exp s x.it) x.src in - let asserts = List.map subst_assert asserts in - let acc = List.fold_left (expand_eq ze_env) acc node_eqs in - let acc = List.fold_left (expand_assert ze_env) acc asserts in - Some acc - ) + let node = + match LicPrg.find_node lctx.prg node_key.it with + | Some n -> n + | None -> + prerr_string ( + "*** "^ (Lic.string_of_node_key node_key.it) ^" not defined.\n" ^ + "*** Defined nodes are:"^ + (String.concat "," + (List.map (fun (nk,_) -> "\""^Lic.string_of_node_key nk^"\"") + (LicPrg.list_nodes lctx.prg))) + ); + flush stderr; + assert false + in + let node = flagit node lxm in + let node = match node.it.def_eff with + | AbstractLic (Some n) -> { it = n ; src = lxm } + | _ -> node + in + if + let nname = Ident.string_of_long2 (fst node.it.node_key_eff) in + (List.mem nname !Global.dont_expand_nodes) + then + None + else + (match get_node_body lctx node.it with + | None -> None + | Some node_body -> + let node_eqs = node_body.eqs_eff + and asserts = node_body.asserts_eff in + let node = node.it in + let node_locs = get_locals node in + let fresh_locs = List.map (mk_fresh_loc lctx) node_locs in + let acc = [],[],fresh_locs in + let is,acc = mk_input_subst lctx lxm node.inlist_eff vel acc in + let os,acc = mk_output_subst lctx lxm node.outlist_eff lhs acc in + let ls = mk_loc_subst node_locs fresh_locs in + let s = List.rev_append is (List.rev_append os ls) in + let node_eqs = List.map (substitute s) node_eqs in + let subst_assert x = Lxm.flagit (subst_in_val_exp s x.it) x.src in + let asserts = List.map subst_assert asserts in + let acc = List.fold_left (expand_eq lctx) acc node_eqs in + let acc = List.fold_left (expand_assert lctx) acc asserts in + Some acc + ) | CallByPosLic (_, _) | CallByNameLic (_, _) -> None -and (expand_assert : Lic.node_env -> acc -> val_exp srcflagged -> acc) = - fun n_env (a_acc,e_acc,v_acc) ve -> +and (expand_assert : local_ctx -> acc -> val_exp srcflagged -> acc) = + fun lctx (a_acc,e_acc,v_acc) ve -> let lxm = ve.src in let ve = ve.it in let clk = Ident.of_string "dummy_expand_assert", BaseLic in - let assert_var = new_var "assert" n_env Bool_type_eff clk in + let assert_var = new_var "assert" lctx Bool_type_eff clk in let assert_eq = Lxm.flagit ([LeftVarLic(assert_var,lxm)], ve) lxm in let assert_op = Lic.VAR_REF(assert_var.var_name_eff) in let nve = { @@ -229,19 +250,19 @@ and (expand_assert : Lic.node_env -> acc -> val_exp srcflagged -> acc) = ve_clk = [BaseLic] } in - expand_eq n_env ((Lxm.flagit nve lxm)::a_acc, e_acc, assert_var::v_acc) assert_eq + expand_eq lctx ((Lxm.flagit nve lxm)::a_acc, e_acc, assert_var::v_acc) assert_eq -(* exported *) -let (f : Lic.node_env -> Lic.node_exp -> Lic.node_exp) = - fun n_env n -> + +let (node : local_ctx -> Lic.node_exp -> Lic.node_exp) = + fun lctx n -> match n.def_eff with | ExternLic | AbstractLic _ -> n | BodyLic b -> let locs = get_locals n in - let acc = List.fold_left (expand_eq n_env) ([],[],locs) b.eqs_eff in - let acc = List.fold_left (expand_assert n_env) acc b.asserts_eff in + let acc = List.fold_left (expand_eq lctx) ([],[],locs) b.eqs_eff in + let acc = List.fold_left (expand_assert lctx) acc b.asserts_eff in let (asserts,neqs, nv) = acc in let nb = { eqs_eff = neqs ; @@ -255,4 +276,26 @@ let (f : Lic.node_env -> Lic.node_exp -> Lic.node_exp) = } in res - | MetaOpLic _-> assert false + | MetaOpLic _ -> n + +(* exported *) +let (doit : LicPrg.t -> LicPrg.t) = + fun inprg -> + let outprg = LicPrg.empty in + (** types and constants do not change *) + let outprg = LicPrg.fold_types LicPrg.add_type inprg outprg in + let outprg = LicPrg.fold_consts LicPrg.add_const inprg outprg in + (** transform nodes *) + let rec (do_node : Lic.node_key -> Lic.node_exp -> LicPrg.t -> LicPrg.t) = + fun nk ne outprg -> + let lctx = { + idgen = LicPrg.fresh_var_id_generator inprg ne; + node = ne; + prg = inprg; + } + in + let ne = node lctx ne in + LicPrg.add_node nk ne outprg + in + let outprg = LicPrg.fold_nodes do_node inprg outprg in + outprg diff --git a/src/l2lExpandNodes.mli b/src/l2lExpandNodes.mli index 304d7990dc00ce70b7c13b64f4f2adf9ac9b5965..8b0558db6ebe0eccada41665c13fb11170ed7837 100644 --- a/src/l2lExpandNodes.mli +++ b/src/l2lExpandNodes.mli @@ -1,7 +1,9 @@ -(* Time-stamp: <modified the 13/12/2012 (at 11:09) by Erwan Jahier> *) +(* Time-stamp: <modified the 20/12/2012 (at 15:28) by Erwan Jahier> *) (** Expand user nodes + + Expand nodes: ------------ @@ -67,4 +69,10 @@ *) -val f : Lic.node_env -> Lic.node_exp -> Lic.node_exp +(** nb : it performs not fixpoint, so nested calls won't be expanded + entirely unless L2lSplit.doit has been call before. + + I could remove that restriction by adding a fixpoint somewhere, + but is it worth bothering ? +*) +val doit : LicPrg.t -> LicPrg.t diff --git a/src/l2lRmPoly.ml b/src/l2lRmPoly.ml index 72ed37854928a8ccabf8e4b322d571f2835bc329..d2b215482feb6c64e066644d7ab436b283ef0b96 100644 --- a/src/l2lRmPoly.ml +++ b/src/l2lRmPoly.ml @@ -1,4 +1,4 @@ -(* Time-stamp: <modified the 18/12/2012 (at 15:57) by Erwan Jahier> *) +(* Time-stamp: <modified the 20/12/2012 (at 11:01) by Erwan Jahier> *) (* Source 2 source transformation : @@ -140,10 +140,7 @@ let rec doit (inprg : LicPrg.t) : LicPrg.t = soit un noeud poly, soit un profil attendu, fabrique s'il n'existe pas déjà , un noeud non poly adéquat ... *) - and solve_poly - (tmatches: Lic.type_matches) - (nk: Lic.node_key) - (ne: Lic.node_exp) + and solve_poly (tmatches: Lic.type_matches) (nk: Lic.node_key) (ne: Lic.node_exp) : Lic.node_key = Verbose.printf ~flag:dbg "#DBG: L2lRmPoly.solve_poly nk='%s'\n# prof=%s'\n# matches='%s'\n" @@ -177,6 +174,7 @@ let rec doit (inprg : LicPrg.t) : LicPrg.t = def_eff = def'; has_mem_eff = ne.has_mem_eff; is_safe_eff = ne.is_safe_eff; + lxm = ne.lxm; } in res := LicPrg.add_node nk' ne' !res; nk' diff --git a/src/lic.ml b/src/lic.ml index c22fac7734b1ce13b8e22fae8816208159cb3da3..74d3bd02ae37b477266123ee080843ce685f00a1 100644 --- a/src/lic.ml +++ b/src/lic.ml @@ -1,4 +1,4 @@ -(* Time-stamp: <modified the 19/12/2012 (at 10:18) by Erwan Jahier> *) +(* Time-stamp: <modified the 20/12/2012 (at 17:13) by Erwan Jahier> *) (** Define the Data Structure representing Compiled programs. *) @@ -314,6 +314,7 @@ and node_exp = { def_eff : node_def; has_mem_eff : bool; is_safe_eff : bool; + lxm : Lxm.t; (* is_polym_eff : bool *) } @@ -342,6 +343,26 @@ and static_arg = and sarg_node_eff = node_key * var_info list * var_info list +(****************************************************************************) + +let rec unalias_type = function + | Abstract_type_eff( _, t) -> unalias_type t + | t -> t + +(* Because of clocks and types, we cannot rely on compare; hence this + dedicated function *) +let (compare_var_info : var_info -> var_info -> int) = + fun v1 v2 -> + if + (v1.var_name_eff = v2.var_name_eff) + && (v1.var_nature_eff = v2.var_nature_eff) + && (v1.var_number_eff = v2.var_number_eff) + && (unalias_type v1.var_type_eff = unalias_type v2.var_type_eff) + && (snd v1.var_clock_eff = snd v2.var_clock_eff) + then + 0 + else compare v1 v2 + (****************************************************************************) (** Type check_flag @@ -427,7 +448,6 @@ let lookup_node (lxm: Lxm.t) (* : sarg_node_eff = *) : node_key = - Hashtbl.find env.lenv_nodes (Ident.name_of_idref id) let (lookup_const: local_env -> Ident.idref -> Lxm.t -> const) = @@ -678,7 +698,11 @@ and string_of_const = function (String.concat ", " (List.map string_of_const cl)) and string_of_var_info x = - (Ident.to_string x.var_name_eff) ^ ":"^(string_of_type x.var_type_eff)^(string_of_clock (snd x.var_clock_eff)) + (AstCore.string_of_var_nature x.var_nature_eff) ^ " " ^ + (Ident.to_string x.var_name_eff) ^ ":"^(string_of_type x.var_type_eff)^ + (string_of_clock (snd x.var_clock_eff)^"("^ (Ident.to_string (fst x.var_clock_eff)) ^","^ + (string_of_int x.var_number_eff)^")") + and string_of_var_list vl = String.concat " ; " (List.map string_of_var_info vl) and string_of_node_key = function @@ -691,7 +715,7 @@ and string_of_node_key = function and string_of_static_arg = function | ConstStaticArgLic(id, ceff) -> Printf.sprintf "const %s = %s" id (string_of_const ceff) | TypeStaticArgLic (id, teff) -> Printf.sprintf "type %s = %s" id (string_of_type teff) -(* | NodeStaticArgLic (id, ((long,sargs), _, _), _) -> *) + (* | NodeStaticArgLic (id, ((long,sargs), _, _), _) -> *) | NodeStaticArgLic (id, nk) -> Printf.sprintf "node %s = %s" id (string_of_node_key nk) diff --git a/src/licEvalType.ml b/src/licEvalType.ml index 7ce57be4cc6ba72f631dd80656233b7bd69de5ff..962277f954be14207750e4fe126dc30544391278 100644 --- a/src/licEvalType.ml +++ b/src/licEvalType.ml @@ -1,4 +1,4 @@ -(* Time-stamp: <modified the 13/12/2012 (at 11:32) by Erwan Jahier> *) +(* Time-stamp: <modified the 20/12/2012 (at 10:59) by Erwan Jahier> *) open AstPredef open Lxm @@ -262,11 +262,6 @@ let op2profile (lxm: Lxm.t) (sargs: Lic.static_arg list) : Lic.node_profile = - let id_solver () = - match id_solver_opt with - | Some s -> s - | None -> assert false - in let res = match op with | TRUE_n | FALSE_n -> b_profile @@ -338,6 +333,7 @@ let make_node_exp_eff def_eff = ExternLic; has_mem_eff = (match has_mem with Some b -> b | None -> true); is_safe_eff = true; + lxm = lxm; (* is_polym_eff = *) (* List.exists (fun vi -> Lic.is_polymorphic vi.var_type_eff) inlist_eff || *) (* List.exists (fun vi -> Lic.is_polymorphic vi.var_type_eff) outlist_eff *) @@ -384,6 +380,7 @@ let make_simple_node_exp_eff def_eff = ExternLic; has_mem_eff = (match has_mem with Some b -> b | None -> true); is_safe_eff = true; + lxm = lxm; (* is_polym_eff = *) (* List.exists (fun vi -> Lic.is_polymorphic vi.var_type_eff) inlist_eff || *) (* List.exists (fun vi -> Lic.is_polymorphic vi.var_type_eff) outlist_eff *) diff --git a/src/licMetaOp.ml b/src/licMetaOp.ml index c0ad405d0fcb4a6836ed5e573300682bb49ac128..d6de3123f6754446887dad973213ac2c846cc45a 100644 --- a/src/licMetaOp.ml +++ b/src/licMetaOp.ml @@ -1,4 +1,4 @@ -(* Time-stamp: <modified the 13/12/2012 (at 10:32) by Erwan Jahier> *) +(* Time-stamp: <modified the 20/12/2012 (at 11:00) by Erwan Jahier> *) (* *) @@ -81,6 +81,7 @@ and do_map nk2nd nk lxm = def_eff = MetaOpLic nk; has_mem_eff = nd.has_mem_eff; is_safe_eff = nd.is_safe_eff; + lxm = lxm; } (*-------------------------------------------------------------------- FILLRED @@ -118,6 +119,7 @@ and do_fillred nk2nd nk lxm = def_eff = MetaOpLic nk; has_mem_eff = nd.has_mem_eff; is_safe_eff = nd.is_safe_eff; + lxm = lxm; } (*-------------------------------------------------------------------- CONDACT @@ -162,6 +164,7 @@ try def_eff = MetaOpLic nk; has_mem_eff = ne.has_mem_eff; is_safe_eff = ne.is_safe_eff; + lxm = lxm; } with | EvalType_error msg -> raise (Compile_error(lxm, "type error: "^msg)) @@ -198,5 +201,6 @@ and do_boolred nk2nd nk lxm = (* ???? *) has_mem_eff = true; is_safe_eff = true; + lxm = lxm; } diff --git a/src/licPrg.ml b/src/licPrg.ml index ee70de4cee783aada1e5da9dbfef808f669b9a80..306b9c52cae46bfb77a80f2a8feb45312ae26b79 100644 --- a/src/licPrg.ml +++ b/src/licPrg.ml @@ -82,6 +82,8 @@ let fold_types (f: Lic.item_key -> Lic.type_ -> 'a -> 'a) (this:t) (accin:'a) : let fold_nodes (f: Lic.node_key -> Lic.node_exp -> 'a -> 'a) (this:t) (accin:'a) : 'a = NodeKeyMap.fold f this.nodes accin +let list_nodes t = fold_nodes (fun k e acc -> (k,e)::acc) t [] + let iter_consts (f: Lic.item_key -> Lic.const -> unit) (this:t) : unit = ItemKeyMap.iter f this.consts let iter_types (f: Lic.item_key -> Lic.type_ -> unit) (this:t) : unit = diff --git a/src/licPrg.mli b/src/licPrg.mli index 297e6c60682baf6a5f335c196f55e63939c06565..bab9a3f68f6968b8a7af0c158c4982a7af410e9e 100644 --- a/src/licPrg.mli +++ b/src/licPrg.mli @@ -1,4 +1,4 @@ -(* Time-stamp: <modified the 18/12/2012 (at 15:51) by Erwan Jahier> *) +(* Time-stamp: <modified the 20/12/2012 (at 15:41) by Erwan Jahier> *) (** The data structure resulting from the compilation process *) @@ -37,6 +37,8 @@ val fold_consts : (Lic.item_key -> Lic.const -> 'a -> 'a) -> t -> 'a -> 'a val fold_types : (Lic.item_key -> Lic.type_ -> 'a -> 'a) -> t -> 'a -> 'a val fold_nodes : (Lic.node_key -> Lic.node_exp -> 'a -> 'a) -> t -> 'a -> 'a +val list_nodes : t -> (Lic.node_key * Lic.node_exp) list + val iter_consts : (Lic.item_key -> Lic.const -> unit) -> t -> unit val iter_types : (Lic.item_key -> Lic.type_ -> unit) -> t -> unit val iter_nodes : (Lic.node_key -> Lic.node_exp -> unit) -> t -> unit diff --git a/src/licTab.ml b/src/licTab.ml index a456b53774ef0e21b9ad2a27f84474f47a1a5d35..5265833c0711e1781c70ac75a2681b43eb357447 100644 --- a/src/licTab.ml +++ b/src/licTab.ml @@ -1,4 +1,4 @@ -(* Time-stamp: <modified the 13/12/2012 (at 16:21) by Erwan Jahier> *) +(* Time-stamp: <modified the 20/12/2012 (at 17:21) by Erwan Jahier> *) open Lxm @@ -444,7 +444,7 @@ and (const_check_interface_do: t -> Ident.long -> Lxm.t -> AstTabSymbol.t -> Lic.Abstract_const_eff (body_id, body_teff, body_v, body_is_exported) -> assert false - (* indeed, how can a body constant be extern and have a value? *) + (* indeed, how can a body constant be extern and have a value? *) | Lic.Abstract_const_eff (id, teff, v, is_exported), Lic.Extern_const_eff (body_id, body_teff) @@ -568,7 +568,7 @@ and (type_check_do: t -> Ident.long -> Lxm.t -> AstTabSymbol.t -> bool -> if (not provide_flag) && (not (!Global.expand_structs & is_struct_or_array)) - (* && not !Global.ec (* ec does not need type decl at all *) *) + (* && not !Global.ec (* ec does not need type decl at all *) *) then (); type_eff @@ -605,12 +605,12 @@ and (const_check_do : t -> Ident.long -> Lxm.t -> AstTabSymbol.t -> bool -> if provide_flag then match val_opt with | None -> - (* we put a fake value here as we don't know yet the - concrete value. this will be filled in - const_check_interface_do. I could have put an option - type, but that would make quite a lot of noise in the - remaining... - *) + (* we put a fake value here as we don't know yet the + concrete value. this will be filled in + const_check_interface_do. I could have put an option + type, but that would make quite a lot of noise in the + remaining... + *) Abstract_const_eff(lid, teff, Int_const_eff (-666), false) | Some c -> let ceff = match EvalConst.f id_solver c with @@ -623,7 +623,7 @@ and (const_check_do : t -> Ident.long -> Lxm.t -> AstTabSymbol.t -> bool -> (match val_opt with | None -> Extern_const_eff(lid, teff) | Some c -> assert false - (* indeed, how can a body constant be extern and have a value? *) + (* indeed, how can a body constant be extern and have a value? *) ) | EnumConst (id, texp) -> Enum_const_eff ((Ident.make_long currpack id), Ast2lic.of_type id_solver texp) @@ -731,7 +731,7 @@ and (node_check_interface_do: t -> Lic.node_key -> Lxm.t -> else if (List.exists2 type_is_not_comp prov_node_exp_eff.outlist_eff body_node_exp_eff.outlist_eff) - (* ougth to be checked above: well, it eats no bread to keep that check *) + (* ougth to be checked above: well, it eats no bread to keep that check *) then let msg = msg_prefix ^ "bad output profile. \n*** " ^ (String.concat "*" (List.map str_of_var prov_node_exp_eff.outlist_eff)) ^ @@ -760,11 +760,11 @@ and (node_check_interface_do: t -> Lic.node_key -> Lxm.t -> | _,_ -> prov_node_exp_eff -(* - LE GROS DU BOULOT - - suivant "provide_flag" : check d'interface (provide) ou le check de la définition - (n.b. provide_flag influence la résolution des idents dans l'env local de check) -*) + (* + LE GROS DU BOULOT + - suivant "provide_flag" : check d'interface (provide) ou le check de la définition + (n.b. provide_flag influence la résolution des idents dans l'env local de check) + *) and node_check_do (this: t) (nk: Lic.node_key) @@ -774,7 +774,7 @@ and (node_check_interface_do: t -> Lic.node_key -> Lxm.t -> (pack_name: Ident.pack_name) (node_def: AstCore.node_info srcflagged) : Lic.node_exp = -(* START node_check_do *) + (* START node_check_do *) ( Verbose.printf ~flag:dbg "#DBG: ENTERING node_check_do '%s'\n (%s)\n" @@ -782,9 +782,9 @@ and (node_check_interface_do: t -> Lic.node_key -> Lxm.t -> (Lxm.details lxm) ; let lxm = node_def.src in - (* Creates a local_env with just the global bindings, - local bindinds will be added later (side effect) - *) + (* Creates a local_env with just the global bindings, + local bindinds will be added later (side effect) + *) let local_env = make_local_env nk in let _ = Verbose.exe ~flag:dbg @@ -796,9 +796,9 @@ and (node_check_interface_do: t -> Lic.node_key -> Lxm.t -> ) in let node_id_solver = { - (* a [node_id_solver] is a [id_solver] where we begin to look - into the local environement before looking at the global - one. *) + (* a [node_id_solver] is a [id_solver] where we begin to look + into the local environement before looking at the global + one. *) id2var = (* var can only be local to the node *) (fun id lxm -> try lookup_var local_env (Ident.of_idref id) lxm @@ -832,7 +832,7 @@ and (node_check_interface_do: t -> Lic.node_key -> Lxm.t -> let (node_id,sargs) = Lic.lookup_node local_env id sargs lxm in let node_id = Ident.idref_of_long node_id in solve_node_idref this symbols provide_flag pack_name node_id sargs lxm - (* node_check this (node_id,[]) lxm *) + (* node_check this (node_id,[]) lxm *) with Not_found -> @@ -840,22 +840,22 @@ and (node_check_interface_do: t -> Lic.node_key -> Lxm.t -> | _ -> assert false) ); - (* ATTENTION EN SE SERVANT DE CA ! - ne tient pas compte des params statiques du noeud ! *) + (* ATTENTION EN SE SERVANT DE CA ! + ne tient pas compte des params statiques du noeud ! *) global_symbols = symbols; } in let make_node_eff id node_def_eff = ( - (* building not aliased nodes *) + (* building not aliased nodes *) Verbose.exe ~level:3 ( fun () -> Printf.printf "*** local_env while entering (make_node_eff %s):\n" (Ident.to_string id); Lic.dump_local_env stderr local_env ); - (********************************************************) - (* LOCAL CONSTANTS are evaluated and added to local_env *) - (********************************************************) - (* init intermediate table *) + (********************************************************) + (* LOCAL CONSTANTS are evaluated and added to local_env *) + (********************************************************) + (* init intermediate table *) let sz = List.length node_def.it.loc_consts in let temp_const_eff_tab : (Ident.long, Lic.const Lic.check_flag) Hashtbl.t = Hashtbl.create sz @@ -878,7 +878,7 @@ and (node_check_interface_do: t -> Lic.node_key -> Lxm.t -> ) ) in List.iter init_local_const node_def.it.loc_consts ; - (* differs from node_id_solver only on id2const *) + (* differs from node_id_solver only on id2const *) let rec local_id_solver = { id2var = node_id_solver.id2var; id2const = local_id2const; @@ -897,9 +897,9 @@ and (node_check_interface_do: t -> Lic.node_key -> Lxm.t -> ) with Not_found -> ( let (lxmdef, toptdef, vedef) = Hashtbl.find temp_const_def_tab id in Verbose.printf ~level:3 " * const %s not yet treated ...\n" id ; - (* yes, not yet checked *) + (* yes, not yet checked *) Hashtbl.add temp_const_eff_tab id_key Checking ; - (* computes the value with EvalConst.f id_solver ve ... *) + (* computes the value with EvalConst.f id_solver ve ... *) let ce = match (EvalConst.f local_id_solver vedef) with | [ceff] -> ( match toptdef with @@ -925,9 +925,9 @@ and (node_check_interface_do: t -> Lic.node_key -> Lxm.t -> ) ) and local_id2const idrf lxm = ( - (* is id a local const ? *) + (* is id a local const ? *) try ( - (* certainly NOT if id has a pack *) + (* certainly NOT if id has a pack *) let id = if (Ident.pack_of_idref idrf = None) then Ident.name_of_idref idrf else raise Not_found @@ -935,16 +935,16 @@ and (node_check_interface_do: t -> Lic.node_key -> Lxm.t -> let ce = treat_local_const id in ce ) with Not_found -> ( - (* not a local constant -> search in global env *) + (* not a local constant -> search in global env *) Verbose.printf ~level:3 " * %s not a local const, should be global ?" (Ident.string_of_idref idrf); let ce = node_id_solver.id2const idrf lxm in Verbose.printf ~level:3 " YES -> %s\n" (LicDump.string_of_const_eff ce); ce ) ) in - (* iters local_id2const n eeach declared constant *) + (* iters local_id2const n eeach declared constant *) Hashtbl.iter (fun id _ -> let _ = treat_local_const id in ()) temp_const_def_tab ; - (* Finally, adds each local const to ICI *) + (* Finally, adds each local const to ICI *) let add_local_const idref ceck = ( Verbose.printf ~level:3 " * add_local_const %s = %s\n" (snd idref) @@ -959,18 +959,18 @@ and (node_check_interface_do: t -> Lic.node_key -> Lxm.t -> ) in Hashtbl.iter add_local_const temp_const_eff_tab ; - (********************************************************) - (* LOCAL FLOWS are added to local_env *) - (********************************************************) - (* (i.e. ins,outs,locs) *) + (********************************************************) + (* LOCAL FLOWS are added to local_env *) + (********************************************************) + (* (i.e. ins,outs,locs) *) match node_def.it.vars with | None -> assert false (* a node with a body should have a profile *) | Some vars -> - (* let is_polymorphic = ref false in *) + (* let is_polymorphic = ref false in *) let type_args id = let vi = find_var_info lxm vars id in let t_eff = Ast2lic.of_type node_id_solver vi.it.var_type in - (* let _ = if Lic.is_polymorphic t_eff then is_polymorphic := true in *) + (* let _ = if Lic.is_polymorphic t_eff then is_polymorphic := true in *) let c_eff = Ast2lic.of_clock node_id_solver vi.it in let vi_eff = { var_name_eff = vi.it.var_name; @@ -986,8 +986,8 @@ and (node_check_interface_do: t -> Lic.node_key -> Lxm.t -> in let (sort_vars : Ident.t list -> Ident.t list) = fun l -> - (* I cannot use List.sort as I only have a partial order on vars - -> hence I perform a topological sort *) + (* I cannot use List.sort as I only have a partial order on vars + -> hence I perform a topological sort *) let rec depends_on v1 v2 = match (find_var_info lxm vars v1).it.var_clock with | Base -> false @@ -1019,7 +1019,7 @@ and (node_check_interface_do: t -> Lic.node_key -> Lxm.t -> else let l1,l2 = List.partition (fun v -> v=v2) l in if l1 = [] then - (* v depends on a clock not in l *) + (* v depends on a clock not in l *) aux (v::acc) tail else aux acc (v2::l2) @@ -1053,10 +1053,11 @@ and (node_check_interface_do: t -> Lic.node_key -> Lxm.t -> def_eff = node_def_eff (); has_mem_eff = node_def.it.has_mem; is_safe_eff = node_def.it.is_safe; - (* is_polym_eff = !is_polymorphic *) + lxm = node_def.src; + (* is_polym_eff = !is_polymorphic *) } ) in - (* let's go *) + (* let's go *) let res = match node_def.it.def with | Abstract -> make_node_eff node_def.it.name (fun () -> AbstractLic None) @@ -1079,9 +1080,9 @@ and (node_check_interface_do: t -> Lic.node_key -> Lxm.t -> | Alias({it= alias;src=lxm}) -> ( let aliased_node = match alias with - (* 12/07 SOLUTION INTERMEDIAIRE - - les macros predefs sont traitées comme des call - *) + (* 12/07 SOLUTION INTERMEDIAIRE + - les macros predefs sont traitées comme des call + *) | Predef_n(op, []) -> let predef_op = op.it in let _ = match predef_op with @@ -1095,9 +1096,9 @@ and (node_check_interface_do: t -> Lic.node_key -> Lxm.t -> in predef_op_eff | Predef_n(op, sargs) -> - (* on re-construit une AstCore.node_exp srcflagged - parce que c'est ca qu'attend of_node ... - *) + (* on re-construit une AstCore.node_exp srcflagged + parce que c'est ca qu'attend of_node ... + *) let node_alias = flagit (AstPredef.op_to_idref op.it, sargs) op.src in Ast2lic.of_node node_id_solver node_alias | CALL_n(node_alias) -> @@ -1107,13 +1108,13 @@ and (node_check_interface_do: t -> Lic.node_key -> Lxm.t -> |CURRENT_n|FBY_n|ARROW_n|PRE_n) -> raise (Compile_error (lxm, "can not alias this operator, sorry")) - (* does it make sense to alias when, pre, etc? *) + (* does it make sense to alias when, pre, etc? *) in let (vil, vol) = match node_def.it.vars with | None -> aliased_node.inlist_eff, aliased_node.outlist_eff | Some (vars) -> - (* a type profile is declared; let's check there are compatible *) + (* a type profile is declared; let's check there are compatible *) let (il,ol) = profile_of_node_exp aliased_node in let (il_decl, ol_decl) = let vi_il, vi_ol = @@ -1129,15 +1130,15 @@ and (node_check_interface_do: t -> Lic.node_key -> Lxm.t -> | UnifyType.Ko msg -> raise(Compile_error(lxm, msg)) | UnifyType.Equal -> () | UnifyType.Unif t -> () - (* Ast2lic.dump_polymorphic_nodes t *) + (* Ast2lic.dump_polymorphic_nodes t *) ); (match o_unif_res with | UnifyType.Ko msg -> raise(Compile_error (lxm, msg)) | UnifyType.Equal -> () | UnifyType.Unif t -> () - (* Ast2lic.dump_polymorphic_nodes t *) + (* Ast2lic.dump_polymorphic_nodes t *) ); - (* ok, there are compatible. We use the declared profile. *) + (* ok, there are compatible. We use the declared profile. *) (il_decl, ol_decl) in let instanciate_var_info vi t = { vi with var_type_eff = t } in @@ -1152,37 +1153,32 @@ and (node_check_interface_do: t -> Lic.node_key -> Lxm.t -> in alias_node ) - (* End Alias *) - in - let current_env = { - local = local_env; - global = node_id_solver; - } + (* End Alias *) in - let _ = L2lCheckOutputs.check res node_def.src in - (* gen_code provide_flag current_env res; *) + L2lCheckOutputs.check_node res; + (* gen_code provide_flag current_env res; *) Verbose.printf ~flag:dbg "#DBG: EXITING node_check_do '%s'\n" (Lic.string_of_node_key nk) ; res ) -(*END node_check_do *) - -(* - [make_alias_node aliased_node alias_nk node_id_solver_vars_opt lxm] - builds a node that calls the aliased node. It looks like: - node alias_node(ins) returns (outs); - let - outs = aliased_node(ins); - tel - - When instanciating models with polymorphic operators, it - may happen that some exported user nodes become - polymorphic (via node alias precisely). But in that case, - a non-polymorphic profile is given in the package provided - part. In such a case, we can use the types of the provided - part (itl and otl) instead of the polymorphic ones. *) + (*END node_check_do *) + + (* + [make_alias_node aliased_node alias_nk node_id_solver_vars_opt lxm] + builds a node that calls the aliased node. It looks like: + node alias_node(ins) returns (outs); + let + outs = aliased_node(ins); + tel + + When instanciating models with polymorphic operators, it + may happen that some exported user nodes become + polymorphic (via node alias precisely). But in that case, + a non-polymorphic profile is given in the package provided + part. In such a case, we can use the types of the provided + part (itl and otl) instead of the polymorphic ones. *) and make_alias_node (aliased_node: node_exp) @@ -1230,10 +1226,10 @@ and (node_check_interface_do: t -> Lic.node_key -> Lxm.t -> { asserts_eff = []; eqs_eff = [Lxm.flagit (outs, aliased_node_call) lxm] }); - (* is_polym_eff = List.exists is_polymorphic (List.map (fun vi -> vi.var_type_eff) (vil@vol)); *) + (* is_polym_eff = List.exists is_polymorphic (List.map (fun vi -> vi.var_type_eff) (vil@vol)); *) } in - (* update the local_env table *) + (* update the local_env table *) let _ = let update_local_env_table vi = Hashtbl.add local_env.lenv_vars vi.var_name_eff vi @@ -1245,7 +1241,7 @@ and (node_check_interface_do: t -> Lic.node_key -> Lxm.t -> in alias_node -(** builds a [node_key] and calls [node_check] *) + (** builds a [node_key] and calls [node_check] *) and solve_node_idref (this: t) (symbols: AstTabSymbol.t) @@ -1259,8 +1255,8 @@ and (node_check_interface_do: t -> Lic.node_key -> Lxm.t -> solve_x_idref node_check_interface node_check AstTabSymbol.find_node "node" (fun p id -> - (* builds a [node_key] from a [pack_name] and a [node] id, - and a Lic.static_arg list *) + (* builds a [node_key] from a [pack_name] and a [node] id, + and a Lic.static_arg list *) let long = Ident.make_long p id in let node_key = long, sargs in node_key @@ -1386,27 +1382,27 @@ let compile_all (this:t) : t = | Some tab -> tab | None -> AstTab.pack_body_env this.src_tab pack_name in - Verbose.print_string ~level:3 "\tExported types:\n"; - AstTabSymbol.iter_types prov_symbols (compile_all_types pack_name this); - flush stdout; - Verbose.print_string ~level:3 "\tExported constants:\n"; - AstTabSymbol.iter_consts prov_symbols (compile_all_constants pack_name this); - flush stdout; - Verbose.print_string ~level:3 "\tExported nodes:\n"; - AstTabSymbol.iter_nodes prov_symbols (compile_all_nodes pack_name this); - flush stdout + Verbose.print_string ~level:3 "\tExported types:\n"; + AstTabSymbol.iter_types prov_symbols (compile_all_types pack_name this); + flush stdout; + Verbose.print_string ~level:3 "\tExported constants:\n"; + AstTabSymbol.iter_consts prov_symbols (compile_all_constants pack_name this); + flush stdout; + Verbose.print_string ~level:3 "\tExported nodes:\n"; + AstTabSymbol.iter_nodes prov_symbols (compile_all_nodes pack_name this); + flush stdout ) in let plist = AstTab.pack_list this.src_tab in - Verbose.print_string ~level:3 "*** Dump the exported items of the packages.\n"; - try - List.iter testpack plist; - this - with - Recursion_error (n, stack) -> - let msg = "Recursion loop detected in node " ^ (Ident.string_of_long n) in - let msg = msg ^ "\n*****" ^ (String.concat "\n*****" stack) in - raise (Compile_error (Lxm.dummy "", msg)) + Verbose.print_string ~level:3 "*** Dump the exported items of the packages.\n"; + try + List.iter testpack plist; + this + with + Recursion_error (n, stack) -> + let msg = "Recursion loop detected in node " ^ (Ident.string_of_long n) in + let msg = msg ^ "\n*****" ^ (String.concat "\n*****" stack) in + raise (Compile_error (Lxm.dummy "", msg)) let compile_node (this:t) (main_node:Ident.idref) : t = (* la clée "absolue" du main node (pas d'args statiques) *) diff --git a/src/mainArgs.ml b/src/mainArgs.ml index b1eecee2195a74ab4029338f51ba756e144b5060..eab1f16bb3ad2e61f852641822787237ff834a9f 100644 --- a/src/mainArgs.ml +++ b/src/mainArgs.ml @@ -29,7 +29,6 @@ let (make_opt : unit -> t) = _margin = 12; } - (* all unrecognized options are accumulated *) let (add_other : t -> string -> unit) = fun opt s -> @@ -197,7 +196,11 @@ let mkoptab (opt:t) : unit = ( (Arg.Int(function i -> Verbose.set i)) ["Set the verbose level"] ; - + mkopt opt + ["-h";"-help";"--help"] + (Arg.Unit (help opt)) + ["Display this message."] + ; (* to show Hidden opt *) mkopt opt ["-more"] diff --git a/todo.org b/todo.org index ffbbb645e08c3e8a2e394fe7152876db2f1dde75..6bf17d440bd074e2d0998f5f507b6c4d223bfa5a 100644 --- a/todo.org +++ b/todo.org @@ -4,24 +4,8 @@ * Urgent -** TODO rebrancher le nodeExpand.ml et structArrayExpand.ml - SCHEDULED: <2012-12-14 Fri> - - State "TODO" from "" [2012-12-10 Mon 16:55] - -file:src/l2lExpandNodes.mli -file:src/l2lExpandArrays.mli - -que Pascal les a débranché lors de son ménage d'été. - -** TODO Pascal a shunté mon LicName dans split. Avait-il (une bonne) raison ? - SCHEDULED: <2012-12-17 Mon> - - State "TODO" from "" [2012-12-17 Mon 16:37] - -par ex, file:~/lus2lic/src/l2lExpandArrays.ml::50 -dois-je faire comme lui ou comme avant ? - ** TODO Refaire marcher les tests de non-reg qui sont cassés - SCHEDULED: <2012-12-14 Fri> + SCHEDULED: <2012-12-20 Thu> suites aux modifs de Pascal de l'été 2012 - State "TODO" from "" [2012-10-26 Fri 14:59]