diff --git a/Makefile b/Makefile index a910c20c54d886b5de9052ed8f02a4477696d4c8..d99f20a236631a0a6e5c70e7b2cd9bc90ab15fe1 100644 --- a/Makefile +++ b/Makefile @@ -16,7 +16,7 @@ log: test: - cd src/test ; make test + cd src/test ; make test & make test_lv4 & make test_ec utest: cd src/test ; make utest diff --git a/src/TODO b/src/TODO index 018a9cf7c159e64525b3aa5ea2fbdcf6709d18af..4533407b91e073de3c3974c458aa062e6be3d32b 100644 --- a/src/TODO +++ b/src/TODO @@ -122,8 +122,14 @@ n'est pas le cas pour l'instant... cf [solve_ident] ----------------------------------------------------------------------- A faire -* Attacher le type et l'horloge des expressions aux expressions elle-meme, -plutot que d'utiliser une hashtbl +* Attacher l'horloge des expressions aux expressions elle-meme, +plutot que d'utiliser une hashtbl (comme pour le type). + +* Maintenant que le type est attaché aux val_exp, il ne devrait plus y +avoir de type attaché a certains variants (eg, STRUCT_ACCESS) ; du coup, +ca permettrait de virer les bouts de types checking qui sont fait dans +GetEff.tralnate_val_exp, alors que pour tous les autres cas, cela est +fait dans EvalType. * Ne pas générer de "current", "->", "pre" (i.e., les traduire en termes de "merge" et "fby"). diff --git a/src/eff.ml b/src/eff.ml index bd3367095548df7ffb865313c4c206f73b3571c0..f7d3f5edc36255388908c80e66a41864a57ed00e 100644 --- a/src/eff.ml +++ b/src/eff.ml @@ -1,4 +1,4 @@ -(** Time-stamp: <modified the 26/02/2009 (at 14:11) by Erwan Jahier> *) +(** Time-stamp: <modified the 11/03/2009 (at 14:13) by Erwan Jahier> *) (** @@ -162,6 +162,16 @@ and left = and eq_info = left list * val_exp and val_exp = + { core : val_exp_core ; + typ : type_ list + (* An empty list means that its type has not been computed (EvalType.f) yet. + a cleaner solution would be to define two versions of val_exp: one with + type info, and one without. But it is a big mutually recursive thing, + and doing that would be a little bit heavy... + *) + (* ; clk : clock *) + } +and val_exp_core = | CallByPosEff of (by_pos_op srcflagged * operands) | CallByNameEff of (by_name_op srcflagged * (Ident.t srcflagged * val_exp) list) @@ -189,7 +199,7 @@ and by_pos_op = | CONCAT | HAT of int * val_exp - | ARRAY of val_exp list + | ARRAY of val_exp list | STRUCT_ACCESS of Ident.t * type_ (* those are different from [by_pos_op] *) @@ -197,7 +207,7 @@ and by_pos_op = | 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 @@ -502,12 +512,13 @@ let (true_type_of_const: const -> type_) = let rec (const_to_val_eff: Lxm.t -> bool -> const -> val_exp) = fun lxm expand_const const -> let mk_by_pos_op by_pos_op_eff = - CallByPosEff(flagit by_pos_op_eff lxm, OperEff []) + { core = CallByPosEff(flagit by_pos_op_eff lxm, OperEff []) ; + typ = [type_of_const const] } in let id_of_int i = Ident.of_string (string_of_int i) in match const with | Bool_const_eff b -> - mk_by_pos_op (Predef((if b then Predef.TRUE_n else Predef.FALSE_n), [])) + mk_by_pos_op (Predef((if b then Predef.TRUE_n else Predef.FALSE_n), [])) | Int_const_eff i -> mk_by_pos_op (Predef((Predef.ICONST_n (id_of_int i)),[])) | Real_const_eff r -> @@ -530,13 +541,15 @@ let rec (const_to_val_eff: Lxm.t -> bool -> const -> val_exp) = in let pack = Ident.pack_of_long sname in let name_op_flg = flagit (STRUCT(pack, Ident.idref_of_long sname)) lxm in - (CallByNameEff( + { core = (CallByNameEff( name_op_flg, List.map (fun (id,const) -> flagit id lxm ,const_to_val_eff lxm expand_const const) fl - )) + )); + typ = [stype] + } let (type_of_left: left -> type_) = diff --git a/src/evalClock.ml b/src/evalClock.ml index 870f6685ff0cd056af21c365ca83e4b3ea9706bc..c019b09095c78fdcc6e46ba84d6a27793ba0ef87 100644 --- a/src/evalClock.ml +++ b/src/evalClock.ml @@ -1,4 +1,4 @@ -(** Time-stamp: <modified the 09/03/2009 (at 16:11) by Erwan Jahier> *) +(** Time-stamp: <modified the 09/03/2009 (at 16:46) by Erwan Jahier> *) open Predef @@ -285,7 +285,7 @@ let rec (f : Lxm.t -> Eff.id_solver -> subst -> Eff.val_exp -> Eff.clock list -> and f_aux id_solver s ve = let cel, s = - match ve with + match ve.core with | CallByPosEff ({it=posop; src=lxm}, OperEff args) -> eval_by_pos_clock id_solver posop lxm args s diff --git a/src/evalType.ml b/src/evalType.ml index 877c72dee6e703af593e36f80d933f8d13c10f30..b485b45121c41520f0f96d8fa314d9bed9e8a62a 100644 --- a/src/evalType.ml +++ b/src/evalType.ml @@ -1,4 +1,4 @@ -(** Time-stamp: <modified the 24/02/2009 (at 18:01) by Erwan Jahier> *) +(** Time-stamp: <modified the 11/03/2009 (at 14:17) by Erwan Jahier> *) open Predef @@ -12,87 +12,61 @@ open Lxm open Errors -(******************************************************************************) -(* 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. -*) - -let val_exp_eff_type_tab = Hashtbl.create 0 - - -let (add : Eff.val_exp -> Eff.type_ list -> unit) = - fun ve tl -> -(* print_string ("\n adding " ^ (LicDump.string_of_val_exp_eff ve)); flush stdout; *) - Hashtbl.add val_exp_eff_type_tab ve tl - -let (lookup : Eff.val_exp -> Eff.type_ list) = - fun vef -> - try Hashtbl.find val_exp_eff_type_tab vef - with _ -> - let lxm = - match vef with - | CallByPosEff(op,_) -> op.src - | CallByNameEff(op,_) -> op.src - in - print_string ( - "*** " ^(Lxm.details lxm) ^ " can not find the exp " ^ - (LicDump.string_of_val_exp_eff vef) ^ " in the table \n\t" ^ - (if Verbose.get_level() <= 2 then "" else - (Hashtbl.fold - (fun ve t acc -> (LicDump.string_of_val_exp_eff ve) ^ "\n\t"^acc) - val_exp_eff_type_tab - "\n" - ) - )); - flush stdout; - assert false - -let (copy : Eff.val_exp -> Eff.val_exp -> unit) = - fun ve1 ve2 -> - let tl = try lookup ve2 - with _ -> assert false - in - Hashtbl.add val_exp_eff_type_tab ve1 tl (******************************************************************************) let finish_me msg = print_string ("\n\tXXX evalType.ml:"^msg^" -> finish me!\n") -let rec (f : Eff.id_solver -> Eff.val_exp -> Eff.type_ list) = +let rec (f : Eff.id_solver -> Eff.val_exp -> Eff.val_exp * Eff.type_ list) = fun id_solver ve -> - let res = - match ve with + let ve_core, tl = + match ve.core with | CallByPosEff ({it=posop; src=lxm}, OperEff args) -> ( - try eval_by_pos_type id_solver posop lxm args - with EvalType_error msg -> - raise (Compile_error(lxm, "type error: "^msg)) + let posop_opt, args, tl = + try eval_by_pos_type id_solver posop lxm args + with EvalType_error msg -> + raise (Compile_error(lxm, "type error: "^msg)) + in + let ve = + match posop_opt with + | None -> CallByPosEff ({it=posop; src=lxm}, OperEff args) + | Some posop -> CallByPosEff ({it=posop; src=lxm}, OperEff args) + in + ve, tl ) | CallByNameEff ({it=nmop; src=lxm}, nmargs ) -> - try eval_by_name_type id_solver nmop lxm nmargs - with EvalConst_error msg -> - raise (Compile_error(lxm, "\n*** can't eval constant: "^msg)) + let nmargs, tl = + try eval_by_name_type id_solver nmop lxm nmargs + with EvalConst_error msg -> + raise (Compile_error(lxm, "\n*** can't eval constant: "^msg)) + in + CallByNameEff ({it=nmop; src=lxm}, nmargs ), tl in - add ve res; - res - -and (eval_by_pos_type : - Eff.id_solver -> Eff.by_pos_op -> Lxm.t -> Eff.val_exp list -> Eff.type_ list) = + { core = ve_core; typ = tl}, tl + + +and (eval_by_pos_type : Eff.id_solver -> Eff.by_pos_op -> Lxm.t -> + Eff.val_exp list -> + Eff.by_pos_op option (* For op that hold a val_exp, we return the modified op *) + * Eff.val_exp list (* The args with type info added *) + * Eff.type_ list (* The type of the val_exp "posop(args)" *) + ) = fun id_solver posop lxm args -> match posop with | Eff.Predef (op,sargs) -> ( - let targs = List.map (f id_solver) args in - let res = PredefEvalType.f op lxm sargs targs in - res + let args, targs = List.split (List.map (f id_solver) args) in + let tve = PredefEvalType.f op lxm sargs targs in + None, args, tve ) | 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 + let args, t_argsl = List.split (List.map (f id_solver) args) in + let t_args = List.flatten t_argsl in let llti = List.length lti and lt_args = List.length t_args in + let tve = if llti <> lt_args then - raise (EvalType_error( - sprintf - "\n*** arity error: %d argument(s) are expected, whereas %d is/are provided" + raise (EvalType_error(sprintf + "\n*** arity error: %d argument(s) are expected, whereas %d is/are provided" llti lt_args)) else (match UnifyType.f lti t_args with @@ -100,43 +74,67 @@ and (eval_by_pos_type : | UnifyType.Unif subst -> List.map (subst_type subst) lto | UnifyType.Ko msg -> raise (Compile_error(lxm, msg)) ) + in + None, args, tve | Eff.IDENT id -> ( - (* [id] migth be a constant, but also a variable *) - try [Eff.type_of_const (id_solver.id2const id lxm)] - with _ -> [(id_solver.id2var id lxm).var_type_eff] - ) - | Eff.WITH(ve) -> f id_solver ve - - | Eff.TUPLE -> List.flatten (List.map (f id_solver) args) + let tve = (* [id] migth be a constant, but also a variable *) + try [Eff.type_of_const (id_solver.id2const id lxm)] + with _ -> [(id_solver.id2var id lxm).var_type_eff] + in + None, [], tve + ) + | Eff.WITH(ve) -> + let ve, tve = f id_solver ve in + Some(Eff.WITH(ve)), [], tve + + | Eff.TUPLE -> + let args, targs = List.split (List.map (f id_solver) args) in + None, args, List.flatten targs | Eff.CONCAT -> ( - match List.map (f id_solver) args with - | [[Array_type_eff (teff0, size0)]; [Array_type_eff (teff1, size1)]] -> - let teff = - match UnifyType.f [teff0] [teff1] with - | UnifyType.Equal -> teff1 - | UnifyType.Unif subst -> subst_type subst teff1 - | UnifyType.Ko msg -> raise (Compile_error(lxm, msg)) - in - [Array_type_eff (teff, size0+size1)] - | _ -> - raise(EvalType_error(sprintf "arity error: 2 expected instead of %d" - (List.length args))) + let args, targs = List.split (List.map (f id_solver) args) in + let tve = + match targs with + | [[Array_type_eff (teff0, size0)]; [Array_type_eff (teff1, size1)]] -> + let teff = + match UnifyType.f [teff0] [teff1] with + | UnifyType.Equal -> teff1 + | UnifyType.Unif subst -> subst_type subst teff1 + | UnifyType.Ko msg -> raise (Compile_error(lxm, msg)) + in + [Array_type_eff (teff, size0+size1)] + | _ -> + raise(EvalType_error(sprintf "arity error: 2 expected instead of %d" + (List.length args))) + in + None, args, tve ) - | Eff.STRUCT_ACCESS (fid,teff) -> [teff] - | Eff.ARRAY_ACCES (_, teff) -> [teff] - - | Eff.ARRAY_SLICE (sieff,teff) -> - [Array_type_eff(teff, sieff.se_width)] + | Eff.STRUCT_ACCESS (fid,teff) -> + let args, targs = List.split (List.map (f id_solver) args) in + (* The type check of teff wrt targs has been done in + GetEff.translate_val_exp (XXX which is not the rigth + place to do that IMHO ; here would be a better place) *) + None, args, [teff] + + | Eff.ARRAY_ACCES (_, teff) -> + let args, targs = List.split (List.map (f id_solver) args) in + (* Ditto XXX type check teff wrt targs here *) + None, args, [teff] + + | Eff.ARRAY_SLICE (sieff,teff) -> + let args, targs = List.split (List.map (f id_solver) args) in + (* Ditto XXX type check teff wrt targs here *) + None, args, [Array_type_eff(teff, sieff.se_width)] | Eff.HAT(size,ceff) -> - let teff_list = f id_solver ceff in - List.map (fun teff -> Array_type_eff(teff, size)) teff_list + let ceff, teff_list = f id_solver ceff in + let tl = List.map (fun teff -> Array_type_eff(teff, size)) teff_list in + Some(Eff.HAT(size,ceff)), [], tl | Eff.ARRAY(args) -> (* check that args are of the same type *) - let type_args_eff = (List.map (f id_solver) args) in + let args, targs = List.split (List.map (f id_solver) args) in let teff_elt = List.fold_left (fun acc teff -> @@ -148,45 +146,47 @@ and (eval_by_pos_type : | _ -> assert false ) [] - type_args_eff + targs in + let tve = assert (List.length teff_elt = 1); [Array_type_eff(List.hd teff_elt, List.length args)] - + in + Some(Eff.ARRAY(args)), [], tve | Eff.WHEN clk_exp -> ( - let type_args_eff = List.map (f id_solver) args in - (match clk_exp with - | Base -> () - | NamedClock( { it = (cc,cv) ; src = lxm }) -> - let vi = id_solver.id2var (Ident.to_idref cv) lxm in - (match vi.var_type_eff with - | Eff.Bool_type_eff - | Eff.Enum_type_eff _ -> () - | teff -> - let msg = "the type of a clock cannot be " ^ - (LicDump.string_of_type_eff4msg teff) - in - raise(Compile_error(lxm,msg)) - ) - ); - match type_args_eff with - | [teff] -> teff + let args, targs = List.split (List.map (f id_solver) args) in + let _ = match clk_exp with + | Base -> () + | NamedClock( { it = (cc,cv) ; src = lxm }) -> + let vi = id_solver.id2var (Ident.to_idref cv) lxm in + (match vi.var_type_eff with + | Eff.Bool_type_eff + | Eff.Enum_type_eff _ -> () + | teff -> + let msg = "the type of a clock cannot be " ^ + (LicDump.string_of_type_eff4msg teff) + in + raise(Compile_error(lxm,msg)) + ) + in + match targs with + | [teff] -> None, args, teff | _ -> raise(EvalType_error("arity error (1 arg expected)")) ) | 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 + let args, targs = List.split (List.map (f id_solver) args) in + match targs with + | [init; teff] -> if init = teff then None, args, teff else raise(EvalType_error("type mismatch. ")) | _ -> raise(EvalType_error("arity error (2 args expected)")) ) | Eff.CURRENT | Eff.PRE -> ( - let type_args_eff = List.map (f id_solver) args in - match type_args_eff with - | [teff] -> teff + let args, targs = List.split (List.map (f id_solver) args) in + match targs with + | [teff] -> None, args, teff | _ -> raise(EvalType_error("arity error (1 arg expected)")) ) | Eff.MERGE _ -> finish_me "merge"; assert false @@ -194,7 +194,8 @@ and (eval_by_pos_type : 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) = + (Ident.t Lxm.srcflagged * Eff.val_exp) list -> + (Ident.t Lxm.srcflagged * Eff.val_exp) list * Eff.type_ list) = fun id_solver namop lxm namargs -> match namop with | Eff.STRUCT_anonymous -> @@ -212,30 +213,34 @@ and (eval_by_name_type : Eff.id_solver -> Eff.by_name_op -> Lxm.t -> | Eff.STRUCT (pn,opid) -> let struct_type = id_solver.id2type opid lxm in - let _ = + let namargs = match struct_type with | Struct_type_eff(sn, fl) -> - List.iter - (fun (fn,fv) -> - let fn, lxm = fn.it, fn.src in - let (ft,fopt) = - try List.assoc fn fl with Not_found -> - let msg = "type error: bad field" ^ (Ident.to_string fn) in - raise (Compile_error(lxm, msg)) - in - (* let's check the type of fv *) - let fv_type = f id_solver fv in - match UnifyType.f [ft] fv_type with - | UnifyType.Unif t -> - (* XXX cannot occur as long as we do not have - user-level polymorphism (really?).*) - () - | UnifyType.Equal -> () - | UnifyType.Ko msg -> raise (Compile_error(lxm, msg)) - ) + let namargs = + List.map + (fun (fn,fv) -> + let lxm = fn.src in + let (ft,fopt) = + try List.assoc fn.it fl with Not_found -> + let msg = "type error: bad field"^(Ident.to_string fn.it) in + raise (Compile_error(lxm, msg)) + in + (* let's check the type of fv *) + let fv, fv_type = f id_solver fv in + let fv_type = (* XXX ignored? *) + match UnifyType.f [ft] fv_type with + | UnifyType.Unif t -> t + | UnifyType.Equal -> ft + | UnifyType.Ko msg -> raise (Compile_error(lxm, msg)) + in + (fn,fv) + ) + namargs + in namargs +(* Struct_type_eff(sn, fl) *) | _ -> raise (Compile_error(lxm, "type error: a structure is expected")) in - [struct_type] + namargs, [struct_type] diff --git a/src/evalType.mli b/src/evalType.mli index 0f1819dcdf4dae30fcf877aae48beaeeb9031bfa..271057154dd8a46c7f31209ea7661329172b3460 100644 --- a/src/evalType.mli +++ b/src/evalType.mli @@ -1,18 +1,10 @@ -(** Time-stamp: <modified the 28/01/2009 (at 10:25) by Erwan Jahier> *) +(** Time-stamp: <modified the 11/03/2009 (at 14:16) by Erwan Jahier> *) -(** Evaluates the type of an expression. *) -val f : Eff.id_solver -> Eff.val_exp -> Eff.type_ list +(** Evaluates the type of an expression, and return a val_exp with + its "typ" field updated (and ditto for the type of its sub expr). + +*) +val f : Eff.id_solver -> Eff.val_exp -> 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 lookup : Eff.val_exp -> Eff.type_ list - -val add : Eff.val_exp -> Eff.type_ list -> unit - -(* [copy ve1 ve2] copies the info info of ve2 for ve1 (i.e., declares that ve1 - has the same type than ve2). *) -val copy : Eff.val_exp -> Eff.val_exp -> unit - diff --git a/src/getEff.ml b/src/getEff.ml index ce9a8ef531bbdc3acb4d287a0ae44cf60b6623f5..1b185b1d4259c92e1a82d49ac591a92937835a03 100644 --- a/src/getEff.ml +++ b/src/getEff.ml @@ -1,4 +1,4 @@ -(** Time-stamp: <modified the 05/03/2009 (at 10:11) by Erwan Jahier> *) +(** Time-stamp: <modified the 11/03/2009 (at 11:26) by Erwan Jahier> *) open Lxm @@ -64,7 +64,7 @@ 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 + let ve_eff, right_part = EvalType.f id_solver ve_eff in if (List.length lpl_teff <> List.length right_part) then raise (Compile_error(lxm, "tuple size error: \n*** the tuple size is\n***\t"^ @@ -351,180 +351,187 @@ and (translate_left_part : id_solver -> SyntaxTreeCore.left_part -> Eff.left) = 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) -> - (CallByNameEff( - flagit (translate_by_name_op id_solver by_name_op) by_name_op.src, - List.map (translate_field id_solver) field_list)) - - | CallByPos(by_pos_op, Oper vel) -> - let vel_eff = List.map (translate_val_exp id_solver) vel in - let lxm = by_pos_op.src in - let by_pos_op = by_pos_op.it in - let mk_by_pos_op by_pos_op_eff = - CallByPosEff(flagit by_pos_op_eff lxm, OperEff vel_eff) - in - match by_pos_op with - (* put that in another module ? yes, see above.*) - | Predef_n(Map, sargs) - | Predef_n(Fill, sargs) - | Predef_n(Red, sargs) - | Predef_n(FillRed, sargs) - | Predef_n(BoolRed, sargs) -> - - (* We will make use of [vel_eff] to resolve the polymorphism *) - let type_l : Eff.type_ list = - List.flatten (List.map (EvalType.f id_solver) vel_eff) - in - let sargs_eff = translate_predef_static_args id_solver sargs lxm in - let iter_op = match by_pos_op with - Predef_n(op,_) -> op | _ -> assert false - in - let iter_profile = match by_pos_op with - | Predef_n(Map,_) -> - PredefEvalType.map_profile lxm sargs_eff - | Predef_n(Fill,_) | Predef_n(Red,_) | Predef_n(FillRed,_) -> - PredefEvalType.fillred_profile lxm sargs_eff - | Predef_n(BoolRed,_) -> - PredefEvalType.boolred_profile lxm sargs_eff - | _ -> assert false - in - let type_l_exp = snd (List.split (fst iter_profile)) in - let sargs_eff = - match UnifyType.f type_l type_l_exp with - | UnifyType.Equal -> sargs_eff - | UnifyType.Unif typ -> - (* the iterated nodes was polymorphic, but we know here - that the type variable was [typ]. - *) + let vef_core = + match ve with + | CallByName(by_name_op, field_list) -> + (CallByNameEff( + flagit (translate_by_name_op id_solver by_name_op) by_name_op.src, + List.map (translate_field id_solver) field_list)) + + | CallByPos(by_pos_op, Oper vel) -> + let vel_eff = List.map (translate_val_exp id_solver) vel in + let lxm = by_pos_op.src in + let by_pos_op = by_pos_op.it in + let mk_by_pos_op by_pos_op_eff = + CallByPosEff(flagit by_pos_op_eff lxm, OperEff vel_eff) + in + let vef_core = + match by_pos_op with + (* put that in another module ? yes, see above.*) + | Predef_n(Map, sargs) + | Predef_n(Fill, sargs) + | Predef_n(Red, sargs) + | Predef_n(FillRed, sargs) + | Predef_n(BoolRed, sargs) -> + (* We will make use of [vel_eff] to resolve the polymorphism *) + let vel_eff, type_ll = + List.split (List.map (EvalType.f id_solver) vel_eff) + in + let type_l : Eff.type_ list = List.flatten type_ll in + let sargs_eff = translate_predef_static_args id_solver sargs lxm in + let iter_op = match by_pos_op with + Predef_n(op,_) -> op | _ -> assert false + in + let iter_profile = match by_pos_op with + | Predef_n(Map,_) -> + PredefEvalType.map_profile lxm sargs_eff + | Predef_n(Fill,_) | Predef_n(Red,_) | Predef_n(FillRed,_) -> + PredefEvalType.fillred_profile lxm sargs_eff + | Predef_n(BoolRed,_) -> + PredefEvalType.boolred_profile lxm sargs_eff + | _ -> assert false + in + let type_l_exp = snd (List.split (fst iter_profile)) in + let sargs_eff = + match UnifyType.f type_l type_l_exp with + | UnifyType.Equal -> sargs_eff + | UnifyType.Unif typ -> + (* the iterated nodes was polymorphic, but we know here + that the type variable was [typ]. + *) dump_polymorphic_nodes typ; 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)) - - (* other predef operators *) - | Predef_n(op, args) -> assert (args=[]); mk_by_pos_op(Predef (op,[])) - - | CALL_n node_exp_f -> - mk_by_pos_op(Eff.CALL (flagit (node id_solver node_exp_f) - node_exp_f.src)) - - | IDENT_n idref -> ( - try Eff.const_to_val_eff lxm false (id_solver.id2const idref lxm) - with _ -> (* It migth not be a static constant... *) - match Ident.pack_of_idref idref with - | Some pn -> mk_by_pos_op(Eff.IDENT idref) - (** Constant with a pack name are treated as - Eff.IDENT. *) - | None -> - try - (* try to add its pack name... *) - let id = Ident.of_idref idref in - let pn = - SymbolTab.find_pack_of_const id_solver.symbols id lxm - in - let idref = Ident.make_idref pn id in - mk_by_pos_op(Eff.IDENT (idref)) - with _ -> - mk_by_pos_op(Eff.IDENT idref) - ) - | CURRENT_n -> mk_by_pos_op Eff.CURRENT - | PRE_n -> mk_by_pos_op Eff.PRE - - | ARROW_n -> mk_by_pos_op Eff.ARROW - | FBY_n -> mk_by_pos_op Eff.FBY - | CONCAT_n -> mk_by_pos_op Eff.CONCAT - | TUPLE_n -> mk_by_pos_op Eff.TUPLE - | ARRAY_n -> - let vel_eff = List.map (translate_val_exp id_solver) vel in + + | UnifyType.Ko str -> raise (Compile_error(lxm, str)) + in + mk_by_pos_op (Eff.Predef(iter_op, sargs_eff)) + + (* other predef operators *) + | Predef_n(op, args) -> + assert (args=[]); mk_by_pos_op(Predef (op,[])) + + | CALL_n node_exp_f -> + mk_by_pos_op(Eff.CALL (flagit (node id_solver node_exp_f) + node_exp_f.src)) + | IDENT_n idref -> ( + try + let const = + Eff.const_to_val_eff lxm false (id_solver.id2const idref lxm) + in + const.core + with _ -> (* It migth not be a static constant... *) + match Ident.pack_of_idref idref with + | Some pn -> mk_by_pos_op(Eff.IDENT idref) + (** Constant with a pack name are treated as + Eff.IDENT. *) + | None -> + try + (* try to add its pack name... *) + let id = Ident.of_idref idref in + let pn = + SymbolTab.find_pack_of_const id_solver.symbols id lxm + in + let idref = Ident.make_idref pn id in + mk_by_pos_op(Eff.IDENT (idref)) + with _ -> + mk_by_pos_op(Eff.IDENT idref) + ) + | CURRENT_n -> mk_by_pos_op Eff.CURRENT + | PRE_n -> mk_by_pos_op Eff.PRE + + | ARROW_n -> mk_by_pos_op Eff.ARROW + | FBY_n -> mk_by_pos_op Eff.FBY + | CONCAT_n -> mk_by_pos_op Eff.CONCAT + | TUPLE_n -> mk_by_pos_op Eff.TUPLE + | ARRAY_n -> CallByPosEff(flagit (Eff.ARRAY vel_eff) lxm, OperEff []) - | WITH_n(c,e1,e2) -> - let c_eff = EvalConst.f id_solver c in - if c_eff = [ Bool_const_eff true ] then - mk_by_pos_op (Eff.WITH (translate_val_exp id_solver e1)) - else - mk_by_pos_op (Eff.WITH (translate_val_exp id_solver e2)) - | STRUCT_ACCESS_n fid -> - let teff = - assert (List.length vel = 1); - EvalType.f id_solver (translate_val_exp id_solver (List.hd vel)) - in - let teff_field = - match teff with - | [Struct_type_eff (name, fl)] -> ( - try fst (List.assoc fid fl) - with Not_found -> - raise ( - PredefEvalType.EvalType_error - (Printf.sprintf "%s is not a field of struct %s" - (Ident.to_string fid) - (LicDump.string_of_type_eff4msg (List.hd teff)))) - ) - | [x] -> PredefEvalType.type_error [x] "struct type" - | x -> PredefEvalType.arity_error x "1" - in - mk_by_pos_op (Eff.STRUCT_ACCESS (fid,teff_field)) - - | WHEN_n Base -> mk_by_pos_op (Eff.WHEN Base) - | WHEN_n (NamedClock { it = (cc,cv) ; src = lxm }) -> - let cc = add_pack_name id_solver lxm cc in - mk_by_pos_op - (Eff.WHEN (NamedClock { it = (cc,cv) ; src = lxm })) - - | ARRAY_ACCES_n ve_index -> - let teff = - assert (List.length vel = 1); - EvalType.f id_solver (translate_val_exp id_solver (List.hd vel)) - in - let size, teff_elt = - match teff with - | [Array_type_eff(teff_elt, size)] -> size, teff_elt - | _ -> - raise (Compile_error( - lxm, "\n*** Type error: '" ^ - (LicDump.string_of_type_eff_list teff) ^ - "' was expected to be an array")) - in - mk_by_pos_op ( - Eff.ARRAY_ACCES( - EvalConst.eval_array_index id_solver ve_index size lxm, - teff_elt - )) - - | ARRAY_SLICE_n si -> - let teff = - assert (List.length vel = 1); - EvalType.f id_solver (translate_val_exp id_solver (List.hd vel)) - in - let size, teff_elt = - match teff with - | [Array_type_eff(teff_elt, size)] -> size, teff_elt - | _ -> - raise (Compile_error( - lxm, "\n*** Type error: '" ^ - (LicDump.string_of_type_eff_list teff) ^ - "' was expected to be an array")) - in - mk_by_pos_op - (Eff.ARRAY_SLICE( - EvalConst.eval_array_slice id_solver si size lxm, teff_elt)) - - | HAT_n -> ( - match vel with - | [exp; ve_size] -> - 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] -> - mk_by_pos_op (Eff.HAT(size, exp_eff)) - | _ -> assert false) - | _ -> assert false - ) - - | MERGE_n(id, idl) -> mk_by_pos_op (Eff.MERGE(id, idl)) - + | WITH_n(c,e1,e2) -> + let c_eff = EvalConst.f id_solver c in + if c_eff = [ Bool_const_eff true ] then + mk_by_pos_op (Eff.WITH (translate_val_exp id_solver e1)) + else + mk_by_pos_op (Eff.WITH (translate_val_exp id_solver e2)) + | STRUCT_ACCESS_n fid -> + assert (List.length vel_eff = 1); + let _, teff = EvalType.f id_solver (List.hd vel_eff) in + let teff_field = + match teff with + | [Struct_type_eff (name, fl)] -> ( + try fst (List.assoc fid fl) + with Not_found -> + raise ( + PredefEvalType.EvalType_error + (Printf.sprintf "%s is not a field of struct %s" + (Ident.to_string fid) + (LicDump.string_of_type_eff4msg (List.hd teff)))) + ) + | [x] -> PredefEvalType.type_error [x] "struct type" + | x -> PredefEvalType.arity_error x "1" + in + mk_by_pos_op (Eff.STRUCT_ACCESS (fid,teff_field)) + + | WHEN_n Base -> mk_by_pos_op (Eff.WHEN Base) + | WHEN_n (NamedClock { it = (cc,cv) ; src = lxm }) -> + let cc = add_pack_name id_solver lxm cc in + mk_by_pos_op (Eff.WHEN (NamedClock { it = (cc,cv) ; src = lxm })) + + | ARRAY_ACCES_n ve_index -> + let _, teff = + assert (List.length vel = 1); + EvalType.f id_solver (List.hd vel_eff) + in + let size, teff_elt = + match teff with + | [Array_type_eff(teff_elt, size)] -> size, teff_elt + | _ -> + raise (Compile_error( + lxm, "\n*** Type error: '" ^ + (LicDump.string_of_type_eff_list teff) ^ + "' was expected to be an array")) + in + mk_by_pos_op ( + Eff.ARRAY_ACCES( + EvalConst.eval_array_index id_solver ve_index size lxm, + teff_elt + )) + + | ARRAY_SLICE_n si -> + let _, teff = + assert (List.length vel = 1); + EvalType.f id_solver (List.hd vel_eff) + in + let size, teff_elt = + match teff with + | [Array_type_eff(teff_elt, size)] -> size, teff_elt + | _ -> + raise (Compile_error( + lxm, "\n*** Type error: '" ^ + (LicDump.string_of_type_eff_list teff) ^ + "' was expected to be an array")) + in + mk_by_pos_op + (Eff.ARRAY_SLICE( + EvalConst.eval_array_slice id_solver si size lxm, teff_elt)) + + | HAT_n -> ( + match vel with + | [exp; ve_size] -> + 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] -> + mk_by_pos_op (Eff.HAT(size, exp_eff)) + | _ -> assert false) + | _ -> assert false + ) + + | MERGE_n(id, idl) -> mk_by_pos_op (Eff.MERGE(id, idl)) + in + vef_core + in + let vef, tl = EvalType.f id_solver { core=vef_core;typ=[] } in + vef and translate_by_name_op id_solver op = match op.it with @@ -601,27 +608,27 @@ and (instanciate_type: Eff.type_ -> Eff.static_arg -> Eff.static_arg) = let op = if t = Int_type_eff then "div" else "rdiv" in make_long "Lustre" op - (* polymorphic op. what should be done for type different from - int and real? - *) - -(* Lustre::ilt and co are not compiled yet. *) -(* | { id_pack = Some "Lustre" ; id_id = "lt" } -> *) -(* let op = if t = Int_type_eff then "ilt" *) -(* else if t = Real_type_eff then "rlt" else "lt" in *) -(* make_long "Lustre" op *) -(* | { id_pack = Some "Lustre" ; id_id = "gt" } -> *) -(* let op = if t = Int_type_eff then "igt" *) -(* else if t = Real_type_eff then "rgt" else "gt" in *) -(* make_long "Lustre" op *) -(* | { id_pack = Some "Lustre" ; id_id = "lte" } -> *) -(* let op = if t = Int_type_eff then "ilte" *) -(* else if t = Real_type_eff then "rlte" else "lte" in *) -(* make_long "Lustre" op *) -(* | { id_pack = Some "Lustre" ; id_id = "gte" } -> *) -(* let op = if t = Int_type_eff then "igte" *) -(* else if t = Real_type_eff then "rgte" else "gte" in *) -(* make_long "Lustre" op *) + (* polymorphic op. what should be done for type different from + int and real? + *) + + (* Lustre::ilt and co are not compiled yet. *) + (* | { id_pack = Some "Lustre" ; id_id = "lt" } -> *) + (* let op = if t = Int_type_eff then "ilt" *) + (* else if t = Real_type_eff then "rlt" else "lt" in *) + (* make_long "Lustre" op *) + (* | { id_pack = Some "Lustre" ; id_id = "gt" } -> *) + (* let op = if t = Int_type_eff then "igt" *) + (* else if t = Real_type_eff then "rgt" else "gt" in *) + (* make_long "Lustre" op *) + (* | { id_pack = Some "Lustre" ; id_id = "lte" } -> *) + (* let op = if t = Int_type_eff then "ilte" *) + (* else if t = Real_type_eff then "rlte" else "lte" in *) + (* make_long "Lustre" op *) + (* | { id_pack = Some "Lustre" ; id_id = "gte" } -> *) + (* let op = if t = Int_type_eff then "igte" *) + (* else if t = Real_type_eff then "rgte" else "gte" in *) + (* make_long "Lustre" op *) | { id_pack = Some "Lustre" ; id_id = "equal" } -> let op = if t = Int_type_eff then "iequal" @@ -729,7 +736,7 @@ let (assertion : Eff.id_solver -> SyntaxTreeCore.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. *) - let evaled_exp = EvalType.f id_solver val_exp_eff in + let val_exp_eff, evaled_exp = EvalType.f id_solver val_exp_eff in List.iter (fun ve -> if ve <> Bool_type_eff then diff --git a/src/inline.ml b/src/inline.ml index efedf909993764264b727fbe40eb2326a9ade62a..9bc53095316047c90f138c9e8c0b3edf4f6cc198 100644 --- a/src/inline.ml +++ b/src/inline.ml @@ -1,4 +1,4 @@ -(** Time-stamp: <modified the 06/03/2009 (at 17:51) by Erwan Jahier> *) +(** Time-stamp: <modified the 11/03/2009 (at 11:19) by Erwan Jahier> *) open Lxm @@ -52,7 +52,8 @@ let (check_clock_and_type : Moreover, this fills some tables that may be used by the call to Split.eq below....*) - if (EvalType.f id_solver rhs <> [exp_type]) then assert false; + let rhs, rhs_tl = EvalType.f id_solver rhs in + if (rhs_tl <> [exp_type]) then assert false; try ignore(EvalClock.f lxm id_solver UnifyClock.empty_subst rhs [exp_clock]) with _ -> assert false @@ -67,7 +68,7 @@ let rec (inline_eq: Eff.local_env -> Eff.id_solver -> inline_acc -> Eff.eq_info srcflagged -> inline_acc) = fun node_env id_solver (eqs, locs) eq -> let { src = lxm_eq ; it = (lhs, rhs) } = eq in - match rhs with + match rhs.core with | CallByPosEff( {src=lxm_ve;it=CALL ({it = {node_key_eff = (("Lustre", "map"),sargs)}})}, OperEff args) @@ -105,20 +106,23 @@ let rec (inline_eq: Eff.local_env -> let args = List.map (fun arg -> - let t_elt = elt_type_of_array (EvalType.lookup arg) in + let targ = arg.typ in + let t_elt = elt_type_of_array targ in let op_flg = { src = lxm_ve ; it = ARRAY_ACCES(i,t_elt) } in - let narg = CallByPosEff(op_flg, OperEff [arg]) in - EvalType.add narg [t_elt]; + let narg = { + core = CallByPosEff(op_flg, OperEff [arg]); + typ = [t_elt] + } + in EvalClock.copy narg arg; narg ) args in - let nrhs = - CallByPosEff({ src = lxm_ve ; it = (CALL node)}, OperEff args) + let nrhs = { rhs with core = + CallByPosEff({ src = lxm_ve ; it = (CALL node)}, OperEff args) } in let eq = { src = lxm_eq ; it = (lhs, nrhs) } in - EvalType.copy nrhs rhs; EvalClock.copy nrhs rhs; (eq::eqs,locs) ) @@ -169,7 +173,7 @@ let rec (inline_eq: Eff.local_env -> let acc_in = List.hd args in let args = List.tl args in let type_exp,clock_exp = - List.hd (EvalType.lookup acc_in), + List.hd (acc_in.typ), List.hd (EvalClock.lookup acc_in) in let (acc_vars : var_info list) = @@ -189,8 +193,10 @@ let rec (inline_eq: Eff.local_env -> (fun vi -> let id = Ident.to_idref vi.var_name_eff in let op_flg = { src = lxm_ve ; it = IDENT id } in - let ve = CallByPosEff(op_flg, OperEff []) in - EvalType.add ve [vi.var_type_eff]; + let ve = { + typ = [vi.var_type_eff]; + core = CallByPosEff(op_flg, OperEff []) } + in EvalClock.add ve [vi.var_clock_eff]; ve ) @@ -202,10 +208,11 @@ let rec (inline_eq: Eff.local_env -> let args = List.map (fun arg -> - let t_elt = elt_type_of_array (EvalType.lookup arg) in + let t_elt = elt_type_of_array arg.typ in let op_flg = {src = lxm_ve ; it = ARRAY_ACCES(i,t_elt)} in - let new_arg = CallByPosEff(op_flg, OperEff [arg]) in - EvalType.add new_arg [t_elt]; + let new_arg = + { core = CallByPosEff(op_flg, OperEff [arg]); typ=[t_elt] } + in EvalClock.add new_arg [clock_exp]; new_arg ) @@ -221,12 +228,14 @@ let rec (inline_eq: Eff.local_env -> in let lhs = acc_left::lhs in let tl = List.map Eff.type_of_left lhs in - let cl = List.map (fun l -> (Eff.var_info_of_left l).var_clock_eff) lhs in - let rhs = - CallByPosEff({ src = lxm_ve ; it = (CALL node)}, OperEff args) + let cl = List.map + (fun l -> (Eff.var_info_of_left l).var_clock_eff) lhs + in + let rhs = { + typ = tl; + core = CallByPosEff({src=lxm_ve;it = (CALL node)}, OperEff args) } in let eq = - EvalType.add rhs tl; EvalClock.add rhs cl; { src = lxm_eq ; it = (lhs, rhs) } in @@ -254,12 +263,15 @@ let rec (inline_eq: Eff.local_env -> ] in let boolred_op = Eff.Predef(Predef.BoolRed,sargs) in - 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 - EvalType.add arg [Array_type_eff(Bool_type_eff, List.length args)]; + let arg = { + typ = [Array_type_eff(Bool_type_eff,n) ]; + core = CallByPosEff({src=lxm_ve;it= ARRAY args}, OperEff [])} in + let rhs = { + typ = [Bool_type_eff]; + core = CallByPosEff({src=lxm_ve;it=boolred_op}, OperEff [arg]) } + in + let eq = { src = lxm_eq ; it = (lhs, rhs) } in EvalClock.add arg clk; - EvalType.add rhs [Bool_type_eff]; EvalClock.add rhs clk; inline_eq node_env id_solver (eqs, locs) eq @@ -278,12 +290,16 @@ let rec (inline_eq: Eff.local_env -> ] in let boolred_op = Eff.Predef(Predef.BoolRed,sargs) in - let arg = CallByPosEff({src=lxm_ve;it=ARRAY args}, OperEff []) in - let rhs = CallByPosEff({src=lxm_ve;it=boolred_op}, OperEff [arg]) in + let arg = { + typ = [Array_type_eff(Bool_type_eff,n) ]; + core = CallByPosEff({src=lxm_ve;it=ARRAY args}, OperEff []) } + in + let rhs = { + typ = [Bool_type_eff]; + core = CallByPosEff({src=lxm_ve;it=boolred_op}, OperEff [arg]) } + in let eq = { src = lxm_eq ; it = (lhs, rhs) } in - EvalType.add arg [Array_type_eff(Bool_type_eff, List.length args)]; EvalClock.add arg clk; - EvalType.add rhs [Bool_type_eff]; EvalClock.add rhs clk; inline_eq node_env id_solver (eqs, locs) eq @@ -302,7 +318,6 @@ let rec (inline_eq: Eff.local_env -> res = i <= cpt && cpt <= j; *) let rhs_clk = EvalClock.lookup rhs in - let rhs_type = EvalType.lookup rhs in let (i,j,k) = match sargs with | [ConstStaticArgEff(_,Int_const_eff i); @@ -323,19 +338,21 @@ let rec (inline_eq: Eff.local_env -> and cpt_op = { it = IDENT (Ident.to_idref cpt.var_name_eff);src=lxm_ve } and and_op = { it = Predef(Predef.AND_n,[]) ; src = lxm_ve } and inf_op = { it = Predef(Predef.LTE_n,[]) ; src = lxm_ve } in - let i_eff = CallByPosEff(i_op, OperEff []) - and j_eff = CallByPosEff(j_op, OperEff []) - and cpt_eff = CallByPosEff(cpt_op, OperEff []) in - let i_inf_cpt = CallByPosEff(inf_op,OperEff[i_eff;cpt_eff]) - and cpt_if_j = CallByPosEff(inf_op,OperEff[cpt_eff;j_eff])in - EvalType.add i_inf_cpt [Bool_type_eff]; + let i_eff = { typ = [Int_type_eff]; core = CallByPosEff(i_op, OperEff []) } + and j_eff = { typ = [Int_type_eff]; core = CallByPosEff(j_op, OperEff [])} + and cpt_eff = { typ = [Int_type_eff]; core = CallByPosEff(cpt_op, OperEff []) } + in + let i_inf_cpt = { typ = [Bool_type_eff]; + core = CallByPosEff(inf_op,OperEff[i_eff;cpt_eff]) } + and cpt_if_j = { typ = [Bool_type_eff]; + core = CallByPosEff(inf_op,OperEff[cpt_eff;j_eff]) } + in EvalClock.add i_inf_cpt rhs_clk; - EvalType.add cpt_if_j [Bool_type_eff]; EvalClock.add cpt_if_j rhs_clk; - CallByPosEff(and_op, OperEff [i_inf_cpt; cpt_if_j]) + { typ = [Bool_type_eff]; + core = CallByPosEff(and_op, OperEff [i_inf_cpt; cpt_if_j]) } in let eq = - EvalType.add rhs rhs_type; EvalClock.add rhs rhs_clk; check_clock_and_type id_solver lxm_eq rhs Bool_type_eff res_clock; { src = lxm_eq ; it = (lhs, rhs) } @@ -343,35 +360,42 @@ let rec (inline_eq: Eff.local_env -> let eq_cpt = let lhs = [LeftVarEff(cpt,lxm_ve)] in (* (if A[0] then 1 else 0) + ... + (if A[k-1] then 1 else 0) *) - let zero = CallByPosEff({it=Predef(id_of_int 0,[]);src=lxm_ve},OperEff[]) - and one = CallByPosEff({it=Predef(id_of_int 1,[]);src=lxm_ve},OperEff[]) + let zero = { + typ = [Int_type_eff]; + core = CallByPosEff({it=Predef(id_of_int 0,[]);src=lxm_ve},OperEff[])} + and one = { + typ = [Int_type_eff]; + core = CallByPosEff({it=Predef(id_of_int 1,[]);src=lxm_ve},OperEff[]) } and plus_op = { it = Predef(Predef.IPLUS_n,[]) ; src = lxm_ve } and ite_op = { it = Predef(Predef.IF_n,[]) ; src = lxm_ve } in let array, type_elt = - EvalType.add zero [Int_type_eff]; EvalClock.add zero rhs_clk; - EvalType.add one [Int_type_eff]; EvalClock.add one rhs_clk; match args with - | [arg] -> arg,elt_type_of_array (EvalType.lookup arg) + | [arg] -> arg,elt_type_of_array arg.typ | _ -> assert false in let make_ite i = (* returns '(if A[i] then 1 else 0)' *) let a_op = { it = ARRAY_ACCES(i,type_elt) ; src = lxm_ve } in - let a_i = CallByPosEff(a_op, OperEff [array]) in - let nve = CallByPosEff(ite_op, OperEff [a_i;one;zero]) in - EvalType.add a_i [Bool_type_eff]; + let a_i = { typ = [type_elt]; + core = CallByPosEff(a_op, OperEff [array]) } + in + let nve = { + typ = [Int_type_eff]; + core = CallByPosEff(ite_op, OperEff [a_i;one;zero]) } + in EvalClock.add a_i rhs_clk; - EvalType.add nve [Int_type_eff]; EvalClock.add nve rhs_clk; nve in let rhs = List.fold_left (fun acc i -> - let nve = CallByPosEff(plus_op, OperEff [acc; make_ite i]) in - EvalType.add nve [Int_type_eff]; + let nve = { + typ = [Int_type_eff]; + core = CallByPosEff(plus_op, OperEff [acc; make_ite i]) } + in EvalClock.add nve rhs_clk; nve ) diff --git a/src/lazyCompiler.ml b/src/lazyCompiler.ml index 91ac961fe4b699c3db0b9e5830492abd42c8e909..be4a99dd521e0a119d3e61676c9959241d0497de 100644 --- a/src/lazyCompiler.ml +++ b/src/lazyCompiler.ml @@ -1,4 +1,4 @@ -(** Time-stamp: <modified the 04/03/2009 (at 10:29) by Erwan Jahier> *) +(** Time-stamp: <modified the 10/03/2009 (at 14:41) by Erwan Jahier> *) open Lxm @@ -809,7 +809,7 @@ and (node_check_do: t -> Eff.node_key -> Lxm.t -> SymbolTab.t -> (* builds a node that calls the aliased node. It looks like: node alias_node(ins) returns (outs); let - outs = aliased_node(ins); + outs = aliased_node(ins); tel When instanciating models with polymorphic operators, it @@ -850,26 +850,29 @@ and (node_check_do: t -> Eff.node_key -> Lxm.t -> SymbolTab.t -> let instanciate_var_info vi t = { vi with var_type_eff = t } in let vil = List.map2 instanciate_var_info aliased_node.inlist_eff il_decl and vol = List.map2 instanciate_var_info aliased_node.outlist_eff ol_decl in - let (outs:Eff.left list) = List.map (fun vi -> LeftVarEff (vi, lxm)) vol - and (aliased_node_call : Eff.val_exp) = - CallByPosEff( - (Lxm.flagit (Eff.CALL(Lxm.flagit aliased_node lxm)) lxm, - OperEff - (List.map - (fun vi -> (* build operands*) - let ve = CallByPosEff( - Lxm.flagit (Eff.IDENT - (Ident.to_idref vi.var_name_eff)) lxm, OperEff []) - in - EvalType.add ve [vi.var_type_eff]; - EvalClock.add ve [vi.var_clock_eff]; - ve - ) - vil))) - in + let (outs:Eff.left list) = List.map (fun vi -> LeftVarEff (vi, lxm)) vol in let tl = List.map Eff.type_of_left outs in + let (aliased_node_call : Eff.val_exp) = + { core = + CallByPosEff( + (Lxm.flagit (Eff.CALL(Lxm.flagit aliased_node lxm)) lxm, + OperEff + (List.map + (fun vi -> (* build operands*) + let ve = { + typ = [vi.var_type_eff]; + core = CallByPosEff( + Lxm.flagit (Eff.IDENT( + Ident.to_idref vi.var_name_eff)) lxm, OperEff [])} + in + EvalClock.add ve [vi.var_clock_eff]; + ve + ) + vil))); + typ = tl + } + in let cl = List.map (fun l -> (Eff.var_info_of_left l).var_clock_eff) outs in - EvalType.add aliased_node_call tl; EvalClock.add aliased_node_call cl; { aliased_node with diff --git a/src/licDump.ml b/src/licDump.ml index baf9d40fcff31feb689f9ef581af71159832609c..10789eea5a94a9ae75c944030026b2be09306096 100644 --- a/src/licDump.ml +++ b/src/licDump.ml @@ -1,4 +1,4 @@ -(** Time-stamp: <modified the 06/03/2009 (at 16:26) by Erwan Jahier> *) +(** Time-stamp: <modified the 10/03/2009 (at 10:02) by Erwan Jahier> *) open Printf open Lxm @@ -29,9 +29,9 @@ let _ = assert (get_rank 5 [1;3;5] = 3) (* check it is a non-singleton tuple *) let rec (is_a_tuple : Eff.val_exp -> bool) = - function - | CallByPosEff ({ it = TUPLE }, OperEff [ve]) -> is_a_tuple ve - | CallByPosEff ({ it = TUPLE }, OperEff vel) -> List.length vel > 1 + function + | { core = CallByPosEff ({ it = TUPLE }, OperEff [ve]) } -> is_a_tuple ve + | { core = CallByPosEff ({ it = TUPLE }, OperEff vel) } -> List.length vel > 1 | _ -> false (******************************************************************************) @@ -47,7 +47,7 @@ let rec string_of_const_eff = | Real_const_eff r -> r | Extern_const_eff (s,t) -> (long s) | Abstract_const_eff (s,t,v,_) -> (long s) ^ (string_of_const_eff v) -(* | Abstract_const_eff (s,t,v,false) -> (long s) *) + (* | Abstract_const_eff (s,t,v,false) -> (long s) *) | Enum_const_eff (s,t) -> if !Global.expand_enums then match t with @@ -98,8 +98,8 @@ and string_def_of_type_eff = function | Enum_type_eff (i, sl) -> assert (sl <>[]); if !Global.expand_enums then "int" else - let f sep acc s = acc ^ sep ^ (long s) in - (List.fold_left (f ", ") (f "" "enum {" (List.hd sl)) (List.tl sl)) ^ "}" + let f sep acc s = acc ^ sep ^ (long s) in + (List.fold_left (f ", ") (f "" "enum {" (List.hd sl)) (List.tl sl)) ^ "}" | Array_type_eff (ty, sz) -> sprintf "%s^%d" (string_of_type_eff ty) sz | Struct_type_eff (name, fl) -> assert (fl <>[]); @@ -125,7 +125,7 @@ and string_of_type_eff = function | Real_type_eff -> "real" | External_type_eff (name) -> prefix ^ (long name) | Abstract_type_eff (name, t) -> prefix ^ (long name) -(* string_of_type_eff t *) + (* string_of_type_eff t *) | Enum_type_eff (name, _) -> prefix ^ (long name) | Array_type_eff (ty, sz) -> array_alias ty sz | Struct_type_eff (name, _) -> prefix ^ (long name) @@ -139,7 +139,7 @@ and string_of_type_eff4msg = function | Real_type_eff -> "real" | External_type_eff (name) -> prefix ^ (long name) | Abstract_type_eff (name, t) -> prefix ^ (long name) -(* string_of_type_eff4msg t *) + (* string_of_type_eff4msg t *) | Enum_type_eff (name, _) -> prefix ^ (long name) | Array_type_eff (ty, sz) -> (string_of_type_eff4msg ty) ^ "^" ^(string_of_int sz) | Struct_type_eff (name, _) -> prefix ^ (long name) @@ -152,12 +152,12 @@ and string_of_type_eff4msg = function Indeed instead of printing: - node toto(x: int ^ 4) ... + node toto(x: int ^ 4) ... we want to print something like : - type int4 = int ^ 4; - node toto(x: int4) ... + type int4 = int ^ 4; + node toto(x: int4) ... That may occur only for array actually. @@ -292,93 +292,93 @@ and (string_of_by_pos_op_eff: Eff.by_pos_op srcflagged -> Eff.val_exp list -> st | Predef (Predef.NOT_n,_), [ve1] -> ((op2string Predef.NOT_n) ^ " " ^ (if is_a_tuple ve1 then (tuple_par [ve1]) else sov ve1)) - + | Predef (Predef.DIESE_n,_), [ve1] -> if !Global.lv4 then sov ve1 (* lv4 does no accept to apply # on One var only! *) else ((op2string Predef.DIESE_n) ^ (tuple_par [ve1])) - + | Predef (Predef.IF_n,_), [ve1; ve2; ve3] -> let ve2str = string_of_val_exp_eff ve2 in let ve2str = if is_a_tuple ve2 then "("^ve2str^")" else ve2str in let ve3str = string_of_val_exp_eff ve3 in let ve3str = if is_a_tuple ve3 then "("^ve3str^")" else ve3str in " if " ^ (string_of_val_exp_eff ve1) ^ - " then " ^ ve2str ^ " else " ^ ve3str + " then " ^ ve2str ^ " else " ^ ve3str | Predef(op,sargs), vel -> if Predef.is_infix op then ( match vel with | [ve1; ve2] -> (string_of_val_exp_eff ve1) ^ " " ^ (op2string op) ^ - " " ^ (string_of_val_exp_eff ve2) + " " ^ (string_of_val_exp_eff ve2) | _ -> assert false ) else ((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 - | Predef.FALSE_n | Predef.TRUE_n -> - tuple vel - | _ -> tuple_par vel - else - "<<" ^ - (String.concat ", " (List.map (static_arg2string) sargs)) - ^ ">>" ^ (tuple_par vel))) + (if sargs = [] then + match op with + | Predef.ICONST_n _ | Predef.RCONST_n _ | Predef.NOT_n + | Predef.UMINUS_n | Predef.IUMINUS_n | Predef.RUMINUS_n + | Predef.FALSE_n | Predef.TRUE_n -> + tuple vel + | _ -> tuple_par vel + else + "<<" ^ + (String.concat ", " (List.map (static_arg2string) sargs)) + ^ ">>" ^ (tuple_par vel))) | CALL nee, _ -> ( if nee.it.def_eff = ExternEff then - if !Global.lv4 then - (match nee.it.node_key_eff with - (* predef op that are iterated are translated into node_exp ; - hence, we need to do (again) a particular threatment to have - a node ouput (i.e., "2>a" vs "Lustre::lt(2,a)" *) - | ("Lustre","uminus"), [] -> " -" ^ sov (hd vel) - | ("Lustre","iuminus"), [] -> " -" ^ sov (hd vel) - | ("Lustre","ruminus"), [] -> " -" ^ sov (hd vel) - | ("Lustre","not"), [] -> " not " ^ sov (hd vel) - - | ("Lustre","lt"), [] -> sov (hd vel) ^ " < " ^ sov (hd (tl vel)) - | ("Lustre","lte"), [] -> sov (hd vel) ^ " <= " ^ sov (hd (tl vel)) - | ("Lustre","gt"), [] -> sov (hd vel) ^ " > " ^ sov (hd (tl vel)) - | ("Lustre","gte"), [] -> sov (hd vel) ^ " >= " ^ sov (hd (tl vel)) - | ("Lustre","eq"), [] -> sov (hd vel) ^ " = " ^ sov (hd (tl vel)) - | ("Lustre","neq"), [] -> sov (hd vel) ^ " <> " ^ sov (hd (tl vel)) - | ("Lustre","diff"), [] -> sov (hd vel) ^ " <> " ^ sov (hd (tl vel)) - | ("Lustre","plus"), [] -> sov (hd vel) ^ " + " ^ sov (hd (tl vel)) - | ("Lustre","iplus"), [] -> sov (hd vel) ^ " + " ^ sov (hd (tl vel)) - | ("Lustre","rplus"), [] -> sov (hd vel) ^ " + " ^ sov (hd (tl vel)) - | ("Lustre","minus"), [] -> sov (hd vel) ^ " - " ^ sov (hd (tl vel)) - | ("Lustre","iminus"), [] -> sov (hd vel) ^ " - " ^ sov (hd (tl vel)) - | ("Lustre","rminus"), [] -> sov (hd vel) ^ " - " ^ sov (hd (tl vel)) - | ("Lustre","div"), [] -> sov (hd vel) ^ " / " ^ sov (hd (tl vel)) - | ("Lustre","idiv"), [] -> sov (hd vel) ^ " / " ^ sov (hd (tl vel)) - | ("Lustre","rdiv"), [] -> sov (hd vel) ^ " / " ^ sov (hd (tl vel)) - | ("Lustre","times"), [] -> sov (hd vel) ^ " * " ^ sov (hd (tl vel)) - | ("Lustre","rtimes"), [] -> sov (hd vel) ^ " * " ^ sov (hd (tl vel)) - | ("Lustre","itimes"), [] -> sov (hd vel) ^ " * " ^ sov (hd (tl vel)) - | ("Lustre","slash"), [] -> sov (hd vel) ^ " / " ^ sov (hd (tl vel)) - | ("Lustre","rslash"), [] -> sov (hd vel) ^ " / " ^ sov (hd (tl vel)) - | ("Lustre","islash"), [] -> sov (hd vel) ^ " / " ^ sov (hd (tl vel)) - - | ("Lustre","impl"), [] -> sov (hd vel) ^ " => " ^ sov (hd (tl vel)) - | ("Lustre","mod"), [] -> sov (hd vel) ^ " mod " ^ sov (hd (tl vel)) - - | ("Lustre","and"), [] -> sov (hd vel) ^ " and " ^ sov (hd (tl vel)) - | ("Lustre","or"), [] -> sov (hd vel) ^ " or " ^ sov (hd (tl vel)) - | ("Lustre","xor"), [] -> sov (hd vel) ^ " xor " ^ sov (hd (tl vel)) - - | ("Lustre","if"), [] -> - " if " ^ sov (hd vel) ^ " then " ^ sov (hd (tl vel)) - ^ " else " ^ sov (hd (tl (tl vel))) - - | _ -> - ((string_of_node_key_iter nee.src nee.it.node_key_eff) ^ (tuple_par vel)) - ) - else - ((string_of_node_key_iter nee.src nee.it.node_key_eff) ^ (tuple_par vel)) + if !Global.lv4 then + (match nee.it.node_key_eff with + (* predef op that are iterated are translated into node_exp ; + hence, we need to do (again) a particular threatment to have + a node ouput (i.e., "2>a" vs "Lustre::lt(2,a)" *) + | ("Lustre","uminus"), [] -> " -" ^ sov (hd vel) + | ("Lustre","iuminus"), [] -> " -" ^ sov (hd vel) + | ("Lustre","ruminus"), [] -> " -" ^ sov (hd vel) + | ("Lustre","not"), [] -> " not " ^ sov (hd vel) + + | ("Lustre","lt"), [] -> sov (hd vel) ^ " < " ^ sov (hd (tl vel)) + | ("Lustre","lte"), [] -> sov (hd vel) ^ " <= " ^ sov (hd (tl vel)) + | ("Lustre","gt"), [] -> sov (hd vel) ^ " > " ^ sov (hd (tl vel)) + | ("Lustre","gte"), [] -> sov (hd vel) ^ " >= " ^ sov (hd (tl vel)) + | ("Lustre","eq"), [] -> sov (hd vel) ^ " = " ^ sov (hd (tl vel)) + | ("Lustre","neq"), [] -> sov (hd vel) ^ " <> " ^ sov (hd (tl vel)) + | ("Lustre","diff"), [] -> sov (hd vel) ^ " <> " ^ sov (hd (tl vel)) + | ("Lustre","plus"), [] -> sov (hd vel) ^ " + " ^ sov (hd (tl vel)) + | ("Lustre","iplus"), [] -> sov (hd vel) ^ " + " ^ sov (hd (tl vel)) + | ("Lustre","rplus"), [] -> sov (hd vel) ^ " + " ^ sov (hd (tl vel)) + | ("Lustre","minus"), [] -> sov (hd vel) ^ " - " ^ sov (hd (tl vel)) + | ("Lustre","iminus"), [] -> sov (hd vel) ^ " - " ^ sov (hd (tl vel)) + | ("Lustre","rminus"), [] -> sov (hd vel) ^ " - " ^ sov (hd (tl vel)) + | ("Lustre","div"), [] -> sov (hd vel) ^ " / " ^ sov (hd (tl vel)) + | ("Lustre","idiv"), [] -> sov (hd vel) ^ " / " ^ sov (hd (tl vel)) + | ("Lustre","rdiv"), [] -> sov (hd vel) ^ " / " ^ sov (hd (tl vel)) + | ("Lustre","times"), [] -> sov (hd vel) ^ " * " ^ sov (hd (tl vel)) + | ("Lustre","rtimes"), [] -> sov (hd vel) ^ " * " ^ sov (hd (tl vel)) + | ("Lustre","itimes"), [] -> sov (hd vel) ^ " * " ^ sov (hd (tl vel)) + | ("Lustre","slash"), [] -> sov (hd vel) ^ " / " ^ sov (hd (tl vel)) + | ("Lustre","rslash"), [] -> sov (hd vel) ^ " / " ^ sov (hd (tl vel)) + | ("Lustre","islash"), [] -> sov (hd vel) ^ " / " ^ sov (hd (tl vel)) + + | ("Lustre","impl"), [] -> sov (hd vel) ^ " => " ^ sov (hd (tl vel)) + | ("Lustre","mod"), [] -> sov (hd vel) ^ " mod " ^ sov (hd (tl vel)) + + | ("Lustre","and"), [] -> sov (hd vel) ^ " and " ^ sov (hd (tl vel)) + | ("Lustre","or"), [] -> sov (hd vel) ^ " or " ^ sov (hd (tl vel)) + | ("Lustre","xor"), [] -> sov (hd vel) ^ " xor " ^ sov (hd (tl vel)) + + | ("Lustre","if"), [] -> + " if " ^ sov (hd vel) ^ " then " ^ sov (hd (tl vel)) + ^ " else " ^ sov (hd (tl (tl vel))) + + | _ -> + ((string_of_node_key_iter nee.src nee.it.node_key_eff) ^ (tuple_par vel)) + ) + else + ((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)) @@ -391,13 +391,13 @@ and (string_of_by_pos_op_eff: Eff.by_pos_op srcflagged -> Eff.val_exp list -> st (if is_a_tuple ve1 then tuple_par [ve2] else string_of_val_exp_eff ve2) | FBY, [ve1; ve2] -> if !Global.lv4 then - (if is_a_tuple ve1 then tuple_par [ve1] else string_of_val_exp_eff ve1) + (if is_a_tuple ve1 then tuple_par [ve1] else string_of_val_exp_eff ve1) ^ " -> pre " ^ - (if is_a_tuple ve1 then tuple_par [ve2] else string_of_val_exp_eff ve2) + (if is_a_tuple ve1 then tuple_par [ve2] else string_of_val_exp_eff ve2) else - (if is_a_tuple ve1 then tuple_par [ve1] else string_of_val_exp_eff ve1) + (if is_a_tuple ve1 then tuple_par [ve1] else string_of_val_exp_eff ve1) ^ " fby " ^ - (if is_a_tuple ve1 then tuple_par [ve2] else string_of_val_exp_eff ve2) + (if is_a_tuple ve1 then tuple_par [ve2] else string_of_val_exp_eff ve2) | WHEN clk, vel -> (tuple vel) ^ (string_of_clock_exp clk) | CURRENT,_ -> "current " ^ tuple_par vel @@ -452,29 +452,31 @@ and (string_of_by_pos_op_eff: Eff.by_pos_op srcflagged -> Eff.val_exp list -> st ("(" ^ str ^ ")") -and string_of_val_exp_eff = function - | CallByPosEff (by_pos_op_eff, OperEff vel) -> - (string_of_by_pos_op_eff by_pos_op_eff vel) - - | CallByNameEff(by_name_op_eff, fl) -> - (match by_name_op_eff.it with - | 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 -> "") ^ - "{" ^ (String.concat ";" - (List.map - (fun (id,veff) -> - let str = string_of_val_exp_eff veff in - (Ident.to_string id.it) ^ "=" ^ - (if is_a_tuple veff then ("("^ str^")") else str) - ) - fl)) ^ - "}" +and string_of_val_exp_eff ve = string_of_val_exp_eff_core ve.core +and string_of_val_exp_eff_core ve_core = + match ve_core with + | CallByPosEff (by_pos_op_eff, OperEff vel) -> + (string_of_by_pos_op_eff by_pos_op_eff vel) + + | CallByNameEff(by_name_op_eff, fl) -> + (match by_name_op_eff.it with + | 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 -> "") ^ + "{" ^ (String.concat ";" + (List.map + (fun (id,veff) -> + let str = string_of_val_exp_eff veff in + (Ident.to_string id.it) ^ "=" ^ + (if is_a_tuple veff then ("("^ str^")") else str) + ) + fl)) ^ + "}" and wrap_long_line str = @@ -501,7 +503,7 @@ and string_of_eq_info_eff (leff_list, vee) = let str = string_of_val_exp_eff vee in wrap_long_line ( (string_of_leff_list leff_list) ^ " = " ^ - (if is_a_tuple vee then ("("^ str^")") else str) ^ ";") + (if is_a_tuple vee then ("("^ str^")") else str) ^ ";") and (string_of_assert : Eff.val_exp srcflagged -> string ) = fun eq_eff -> @@ -557,8 +559,8 @@ and (const_decl: Ident.long -> Eff.const -> string) = if !Global.expand_enums then (begin_str ^ " = " ^ end_str) else - (* do not print those const, because there were - introduced by the compiler *) + (* do not print those const, because there were + introduced by the compiler *) "" | Extern_const_eff _ | Abstract_const_eff _ -> @@ -612,20 +614,20 @@ and (string_of_clock_exp : SyntaxTreeCore.clock_exp -> string) = and (string_of_ident_clk : Ident.clk -> string) = fun clk -> - let (cc,v) = clk in - let clk_exp_str = - match Ident.string_of_idref cc with - | "True" -> (Ident.to_string v) - | "False" -> "not " ^ (Ident.to_string v) - | _ -> - if !Global.lv4 then - raise (Errors.Global_error - ("*** Cannot generate V4 style Lustre for programs with enumerated "^ - "clocks (yet), sorry.")) - else - Ident.string_of_clk clk - in - clk_exp_str + let (cc,v) = clk in + let clk_exp_str = + match Ident.string_of_idref cc with + | "True" -> (Ident.to_string v) + | "False" -> "not " ^ (Ident.to_string v) + | _ -> + if !Global.lv4 then + raise (Errors.Global_error + ("*** Cannot generate V4 style Lustre for programs with enumerated "^ + "clocks (yet), sorry.")) + else + Ident.string_of_clk clk + in + clk_exp_str (* exported *) @@ -637,7 +639,7 @@ and string_of_clock2 (ck : Eff.clock) = " on " ^ clk_exp_str ^ (string_of_clock2 ceff) | ClockVar i -> "'a" ^ string_of_int i - + and string_of_clock (ck : Eff.clock) = match ck with | BaseEff -> "" @@ -648,7 +650,7 @@ and string_of_clock (ck : Eff.clock) = "" (* it migth occur that (unused) constant remain with a clock var. But in that case, it is ok to consider then as on the base clock. *) - (* | ClockVar i -> "_clock_var_" ^ (string_of_int i) *) + (* | ClockVar i -> "_clock_var_" ^ (string_of_int i) *) and op2string = Predef.op2string diff --git a/src/licDump.mli b/src/licDump.mli index 93c7b440d76520200a211357fb4ca677c0e39479..3523a393d600f0a2c8f0fe76548d12d5d7a69013 100644 --- a/src/licDump.mli +++ b/src/licDump.mli @@ -1,4 +1,4 @@ -(** Time-stamp: <modified the 03/03/2009 (at 17:20) by Erwan Jahier> *) +(** Time-stamp: <modified the 10/03/2009 (at 10:02) by Erwan Jahier> *) val string_of_node_key_rec : Eff.node_key -> string @@ -31,5 +31,6 @@ val dump_type_alias : out_channel -> unit val string_of_clock_exp : SyntaxTreeCore.clock_exp -> string val string_of_clock2 : Eff.clock -> string val string_of_val_exp_eff : Eff.val_exp -> string +val string_of_val_exp_eff_core : Eff.val_exp_core -> string diff --git a/src/nodesExpand.ml b/src/nodesExpand.ml index 2ab800d41a925ec9d3f04cb8dc7794a397f559c8..05703c6b2db16324367b173e2cefe5294443ea88 100644 --- a/src/nodesExpand.ml +++ b/src/nodesExpand.ml @@ -1,4 +1,4 @@ -(** Time-stamp: <modified the 24/02/2009 (at 14:34) by Erwan Jahier> *) +(** Time-stamp: <modified the 10/03/2009 (at 14:40) by Erwan Jahier> *) (** nb : only user nodes are expanded. @@ -109,11 +109,10 @@ let (get_node_body : Eff.local_env -> Eff.node_exp -> Eff.node_body option) = (********************************************************************************) type subst = (var_info * var_info) list let rec (substitute : subst -> Eff.eq_info Lxm.srcflagged -> - Eff.eq_info Lxm.srcflagged) = + Eff.eq_info Lxm.srcflagged) = 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 - EvalType.copy newve ve; EvalClock.copy newve ve; { it = (lhs,newve) ; src = lxm } @@ -126,41 +125,42 @@ and subst_in_left s left = and (subst_in_val_exp : subst -> val_exp -> val_exp) = fun s ve -> - let newve = - match ve with - | CallByPosEff (by_pos_op, OperEff 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 - - | IDENT idref -> - let idref = - try - let id = Ident.of_idref idref in - let var = snd(List.find (fun (v,_) -> v.var_name_eff = id) s) in - let idref = Ident.to_idref var.var_name_eff in - idref - with Not_found -> idref - in - IDENT idref - - | 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) - - | Predef _| CALL _ | PRE | ARROW | FBY | CURRENT | WHEN _ | TUPLE | CONCAT - | STRUCT_ACCESS _ | ARRAY_ACCES _ | ARRAY_SLICE _ | MERGE _ -(* | CONST _ *) - -> by_pos_op - in - CallByPosEff(Lxm.flagit by_pos_op lxm, OperEff vel) - - | CallByNameEff(by_name_op, fl) -> - let fl = List.map (fun (id,ve) -> (id, subst_in_val_exp s ve)) fl in - CallByNameEff(by_name_op, fl) + let newve = { + ve with core = + match ve.core with + | CallByPosEff (by_pos_op, OperEff 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 + + | IDENT idref -> + let idref = + try + let id = Ident.of_idref idref in + let var = snd(List.find (fun (v,_) -> v.var_name_eff = id) s) in + let idref = Ident.to_idref var.var_name_eff in + idref + with Not_found -> idref + in + IDENT idref + + | 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) + + | Predef _| CALL _ | PRE | ARROW | FBY | CURRENT | WHEN _ | TUPLE + | CONCAT | STRUCT_ACCESS _ | ARRAY_ACCES _ | ARRAY_SLICE _ | MERGE _ + (* | CONST _ *) + -> by_pos_op + in + CallByPosEff(Lxm.flagit by_pos_op lxm, OperEff vel) + + | CallByNameEff(by_name_op, fl) -> + let fl = List.map (fun (id,ve) -> (id, subst_in_val_exp s ve)) fl in + CallByNameEff(by_name_op, fl) + } in - EvalType.copy newve ve; EvalClock.copy newve ve; newve @@ -209,9 +209,12 @@ let (mk_output_subst : Eff.local_env -> Lxm.t -> var_info list -> Eff.left list | _ -> let nv = mk_fresh_loc node_env v in let nv_idref = Ident.to_idref nv.var_name_eff in - let nve = CallByPosEff({it=IDENT nv_idref;src = lxm },OperEff []) in + let nve = { + core = CallByPosEff({it=IDENT nv_idref;src = lxm },OperEff []); + typ = [nv.var_type_eff] + } + in let neq = - EvalType.add nve [nv.var_type_eff]; EvalClock.add nve [nv.var_clock_eff]; [left], nve in @@ -241,7 +244,7 @@ let rec (expand_eq : Eff.local_env -> acc -> Eff.eq_info Lxm.srcflagged -> acc) and (expand_eq_aux: Eff.local_env -> Eff.eq_info -> acc option)= fun node_env (lhs,ve) -> - match ve with + match ve.core with | CallByPosEff( { it = Eff.CALL node ; src = lxm }, OperEff vel) -> (match get_node_body node_env node.it with | None -> None @@ -275,8 +278,11 @@ and (expand_assert : Eff.local_env -> acc -> val_exp srcflagged -> acc) = let assert_var = new_var "assert" n_env Bool_type_eff clk in let assert_eq = Lxm.flagit ([LeftVarEff(assert_var,lxm)], ve) lxm in let assert_op = Eff.IDENT(Ident.to_idref assert_var.var_name_eff) in - let nve = CallByPosEff((Lxm.flagit assert_op lxm, OperEff [])) in - EvalType.copy nve ve; + let nve = { + core = CallByPosEff((Lxm.flagit assert_op lxm, OperEff [])); + typ = [Bool_type_eff] + } + in EvalClock.copy nve ve; expand_eq n_env ((Lxm.flagit nve lxm)::a_acc, e_acc, assert_var::v_acc) assert_eq diff --git a/src/split.ml b/src/split.ml index 632d60d11f67be531c614875caf829351f7a76c9..f3bc63e6ff2295e9c9f2ccb3598033ba27b7396e 100644 --- a/src/split.ml +++ b/src/split.ml @@ -1,4 +1,4 @@ -(** Time-stamp: <modified the 06/03/2009 (at 16:41) by Erwan Jahier> *) +(** Time-stamp: <modified the 10/03/2009 (at 14:40) by Erwan Jahier> *) open Lxm @@ -28,7 +28,7 @@ let new_var node_env type_eff clock_eff = let rec (get_vel_from_tuple : val_exp -> val_exp list) = function - | CallByPosEff({it=Eff.TUPLE }, OperEff vel) -> + | { core = CallByPosEff({it=Eff.TUPLE }, OperEff vel) } -> List.flatten (List.map get_vel_from_tuple vel) | ve -> [ve] @@ -44,19 +44,21 @@ let to_be_broken = function | _ -> false - let (break_it : val_exp -> val_exp list) = fun ve -> let nvel = - match ve with + match ve.core with | CallByPosEff({it=Eff.Predef(Predef.IF_n,[]);src=lxm}, OperEff [c;ve1;ve2]) -> let vel1 = get_vel_from_tuple ve1 and vel2 = get_vel_from_tuple ve2 in List.map2 (fun ve1 ve2 -> - CallByPosEff({it=Eff.Predef(Predef.IF_n,[]);src=lxm}, - OperEff [c;ve1;ve2]) + { core = + CallByPosEff({it=Eff.Predef(Predef.IF_n,[]);src=lxm}, + OperEff [c;ve1;ve2]); + typ = ve1.typ + } ) vel1 vel2 @@ -64,18 +66,24 @@ let (break_it : val_exp -> val_exp list) = | CallByPosEff({it=WHEN clk; src=lxm}, OperEff vel) -> let vel = List.flatten (List.map get_vel_from_tuple vel) in List.map - (fun ve -> CallByPosEff({it=WHEN clk ; src=lxm }, OperEff [ve])) + (fun ve -> + { ve with + core=CallByPosEff({it=WHEN clk ; src=lxm }, OperEff [ve])}) vel | CallByPosEff({it=Eff.TUPLE ; src=lxm }, OperEff vel) -> let vel = List.flatten (List.map get_vel_from_tuple vel) in List.map - (fun ve -> CallByPosEff({it=Eff.TUPLE ; src=lxm }, OperEff [ve])) + (fun ve -> + { ve with + core=CallByPosEff({it=Eff.TUPLE ; src=lxm }, OperEff [ve])}) vel | CallByPosEff({it=op ; src=lxm }, OperEff [ve]) -> let vel = get_vel_from_tuple ve in - List.map (fun ve -> CallByPosEff({it=op ; src=lxm }, OperEff [ve])) vel + List.map + (fun ve -> { ve with core=CallByPosEff({it=op;src=lxm}, OperEff [ve])}) + vel | CallByPosEff({it=op ; src=lxm }, OperEff [ve1;ve2]) -> let vel1 = get_vel_from_tuple ve1 @@ -83,16 +91,18 @@ let (break_it : val_exp -> val_exp list) = in List.map2 (fun ve1 ve2 -> - CallByPosEff({it=op ; src=lxm }, OperEff [ve1;ve2]) + { core = CallByPosEff({it=op ; src=lxm }, OperEff [ve1;ve2]); + typ = ve1.typ } ) vel1 vel2 - | _ -> assert false + | _ -> assert false (* dead code since it is guarded by to_be_broken... *) in - let tl = EvalType.lookup ve + let tl = ve.typ and cl = EvalClock.lookup ve in - List.iter2 (fun t nve -> EvalType.add nve [t]) tl nvel; + let nvel = List.map2 (fun nve t -> { nve with typ = [t] } ) nvel ve.typ in + assert(ve.typ = tl); List.iter2 (fun c nve -> EvalClock.add nve [c]) cl nvel; nvel @@ -100,7 +110,7 @@ let (split_tuples:Eff.eq_info Lxm.srcflagged list -> Eff.eq_info Lxm.srcflagged fun eql -> let split_one_eq eq = let { src = lxm_eq ; it = (lhs, n_rhs) } = eq in - if List.length lhs > 1 && (to_be_broken n_rhs) then + if List.length lhs > 1 && (to_be_broken n_rhs.core) then let vel = break_it n_rhs in let eqs = try List.map2 (fun lhs ve -> [lhs], ve) lhs vel @@ -150,7 +160,7 @@ and (split_val_exp : bool -> bool -> Eff.local_env -> Eff.val_exp -> *) - match ve with + match ve.core with | CallByPosEff({it=Eff.IDENT _}, _) -> ve, ([],[]) | CallByPosEff({src=lxm;it=Eff.Predef(Predef.TRUE_n,_)}, _) @@ -165,12 +175,14 @@ and (split_val_exp : bool -> bool -> Eff.local_env -> Eff.val_exp -> match snd (List.hd clk) with | On(clock,_) -> let clk_exp = SyntaxTreeCore.NamedClock (Lxm.flagit clock lxm) in - CallByPosEff({src=lxm;it=Eff.WHEN clk_exp}, OperEff [ve]), ([],[]) - + { ve with core = + CallByPosEff({src=lxm;it=Eff.WHEN clk_exp},OperEff [ve])}, + ([],[]) + | (ClockVar _) (* should not occur *) | BaseEff -> ve, ([],[]) else - ve, ([],[]) + ve, ([],[]) | CallByNameEff (by_name_op_eff, fl) -> let lxm = by_name_op_eff.src in @@ -183,30 +195,28 @@ and (split_val_exp : bool -> bool -> Eff.local_env -> Eff.val_exp -> ([],[],[]) fl in - let rhs = CallByNameEff (by_name_op_eff, List.rev fl) in - EvalType.copy rhs ve; + let rhs = { ve with core = CallByNameEff (by_name_op_eff, List.rev fl) } in EvalClock.copy rhs ve; if top_level then rhs, (eql, vl) else (* create the var for the current call *) let clk_l = EvalClock.lookup ve in - let typ_l = EvalType.lookup ve in + let typ_l = ve.typ in let nv_l = List.map2 (new_var node_env) typ_l clk_l in let nve = match nv_l with - | [nv] -> CallByPosEff( - Lxm.flagit (Eff.IDENT (Ident.to_idref nv.var_name_eff)) lxm, - OperEff [] - ) + | [nv] -> { ve with core = + CallByPosEff( + Lxm.flagit (Eff.IDENT (Ident.to_idref nv.var_name_eff)) lxm, + OperEff [] + )} | _ -> assert false in let lpl = List.map (fun nv -> LeftVarEff(nv, lxm)) nv_l in let eq = Lxm.flagit (lpl, rhs) lxm in - EvalType.copy nve ve; EvalClock.copy nve ve; nve, (eql@[eq], vl@nv_l) - - + | CallByPosEff(by_pos_op_eff, OperEff vel) -> (* recursively split the arguments *) let lxm = by_pos_op_eff.src in @@ -231,7 +241,7 @@ and (split_val_exp : bool -> bool -> Eff.local_env -> Eff.val_exp -> let by_pos_op_eff = Lxm.flagit (Eff.WHEN(ve)) lxm in let rhs = CallByPosEff(by_pos_op_eff, OperEff vel) in rhs, (eql, vl) - + | Eff.ARRAY vel -> let vel, (eql, vl) = split_val_exp_list false false node_env vel in let by_pos_op_eff = Lxm.flagit (Eff.ARRAY(vel)) lxm in @@ -243,52 +253,59 @@ and (split_val_exp : bool -> bool -> Eff.local_env -> Eff.val_exp -> let rhs = CallByPosEff(by_pos_op_eff, OperEff vel) in rhs, (eql, vl) in - EvalType.copy rhs ve; + let rhs = { ve with core = rhs } in EvalClock.copy rhs ve; if top_level || by_pos_op_eff.it = TUPLE then rhs, (eql, vl) else (* create the var for the current call *) let clk_l = EvalClock.lookup ve in - let typ_l = EvalType.lookup ve in + let typ_l = ve.typ in let nv_l = List.map2 (new_var node_env) typ_l clk_l in - let nve = match nv_l with - | [nv] -> CallByPosEff( - Lxm.flagit (Eff.IDENT (Ident.to_idref nv.var_name_eff)) lxm, - OperEff []) - - | _ -> - CallByPosEff( - Lxm.flagit Eff.TUPLE lxm, - OperEff - (List.map ( - fun nv -> - let nnv = CallByPosEff - (Lxm.flagit - (Eff.IDENT (Ident.to_idref nv.var_name_eff)) lxm, - OperEff [] - ) - in - EvalType.add nnv [nv.var_type_eff]; - EvalClock.add nnv [nv.var_clock_eff]; - nnv - ) - nv_l - ) - ) + let nve = + match nv_l with + | [nv] -> { + typ = [nv.var_type_eff]; + core = CallByPosEff( + Lxm.flagit (Eff.IDENT (Ident.to_idref nv.var_name_eff)) lxm, + OperEff []) + } + | _ -> { + typ = List.map (fun v -> v.var_type_eff) nv_l; + core = CallByPosEff( + Lxm.flagit Eff.TUPLE lxm, + OperEff + (List.map ( + fun nv -> + let nnv = { + core = CallByPosEff + (Lxm.flagit + (Eff.IDENT (Ident.to_idref nv.var_name_eff)) lxm, + OperEff []); + typ = [nv.var_type_eff] + } + in + EvalClock.add nnv [nv.var_clock_eff]; + nnv + ) + nv_l + ) + ) + } in let lpl = List.map (fun nv -> LeftVarEff(nv, lxm)) nv_l in let eq = Lxm.flagit (lpl, rhs) lxm in - EvalType.copy nve ve; EvalClock.copy nve ve; nve, (eql@[eq], vl@nv_l) and (split_val_exp_list : bool -> - bool -> Eff.local_env -> Eff.val_exp list -> Eff.val_exp list * split_acc) = + bool -> Eff.local_env -> Eff.val_exp list -> Eff.val_exp list * split_acc) = fun when_flag top_level node_env vel -> - let vel, accl = List.split (List.map (split_val_exp when_flag top_level node_env) vel) in + let vel, accl = + List.split (List.map (split_val_exp when_flag top_level node_env) vel) + in let eqll,vll = List.split accl in let eql, vl = List.flatten eqll, List.flatten vll in (vel,(eql,vl)) diff --git a/src/structArrayExpand.ml b/src/structArrayExpand.ml index 614465231b8a4f654f44be7353649a6f85085ec0..f2c3da9750e46947fd1ed993a942f75fe7936690 100644 --- a/src/structArrayExpand.ml +++ b/src/structArrayExpand.ml @@ -1,4 +1,4 @@ -(** Time-stamp: <modified the 27/02/2009 (at 11:08) by Erwan Jahier> *) +(** Time-stamp: <modified the 10/03/2009 (at 14:39) 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... @@ -214,7 +214,7 @@ let (expand_left : Eff.local_env -> left -> left list) = let rec (make_new_loc : Eff.local_env -> Eff.id_solver -> Lxm.t -> acc -> Eff.val_exp -> acc * var_info) = fun nenv id_solver lxm acc ve -> - let teff = List.hd (EvalType.lookup ve) in + let teff = List.hd ve.typ in let ceff = List.hd (EvalClock.lookup ve) in let nv = new_var "v" nenv teff ceff in let neq = [LeftVarEff(nv,lxm)], ve in @@ -229,10 +229,11 @@ and (var_trees_of_val_exp : Eff.local_env -> Eff.id_solver -> acc -> Eff.val_exp let make_val_exp nenv lxm vi prefix teff = let prefix = (Ident.to_string vi.var_name_eff) ^ prefix in let idref = Ident.idref_of_string prefix in - CallByPosEff({src=lxm;it=(IDENT idref)}, OperEff []) + { core = CallByPosEff({src=lxm;it=(IDENT idref)}, OperEff []); + typ = [vi.var_type_eff] } in let loop = var_trees_of_val_exp nenv id_solver acc in - match ve with + match ve.core with | CallByPosEff (by_pos_op, OperEff vel) -> let lxm = by_pos_op.src in let by_pos_op = by_pos_op.it in @@ -278,15 +279,13 @@ and (var_trees_of_val_exp : Eff.local_env -> Eff.id_solver -> acc -> Eff.val_exp in raise (Errors.Compile_error(lxm, msg)) in - let tconst = Eff.true_type_of_const const in let ceff = EvalClock.lookup ve in let ve_const = Eff.const_to_val_eff lxm true const in let _ = - EvalType.add ve_const [tconst]; EvalClock.add ve_const ceff; in let ve_const,acc = - match ve_const with + match ve_const.core with | CallByPosEff ({it=IDENT _},_) -> (* in order to avoid a potential infinite loop *) (ve_const, acc) @@ -320,13 +319,12 @@ and (break_tuple : Lxm.t -> left list -> val_exp -> Eff.eq_info srcflagged list) in the rigth part) *) let rec aux ve = (* flatten val exp*) - match ve with - + match ve.core with | CallByPosEff ({it= TUPLE}, OperEff vel) -> List.flatten (List.map aux vel) | CallByPosEff (unop, OperEff [ve1]) -> let ve1l = aux ve1 in List.map - (fun ve1 -> CallByPosEff (unop, OperEff [ve1])) + (fun ve1 -> { ve1 with core = CallByPosEff (unop, OperEff [ve1])} ) ve1l | CallByPosEff (binop, OperEff [ve1;ve2]) -> let ve1l, ve2l = aux ve1, aux ve2 in @@ -334,15 +332,16 @@ and (break_tuple : Lxm.t -> left list -> val_exp -> Eff.eq_info srcflagged list) let vel2str vel = (String.concat ", " (List.map LicDump.string_of_val_exp_eff vel)) in - let msg = "*** error expression " ^ (LicDump.string_of_val_exp_eff ve) ^ + let msg = + "*** error expression " ^ (LicDump.string_of_val_exp_eff ve) ^ "\n cannot be broken \n" ^(vel2str ve1l) ^ " should have the same arity as\n"^(vel2str ve2l) ^ "\n" - in - (* assert false *) + in raise (Errors.Compile_error(lxm, msg)) else List.map2 - (fun ve1 ve2 -> CallByPosEff (binop, OperEff [ve1;ve2])) + (fun ve1 ve2 -> + { ve with core = CallByPosEff (binop, OperEff [ve1;ve2])}) ve1l ve2l @@ -353,15 +352,19 @@ and (break_tuple : Lxm.t -> left list -> val_exp -> Eff.eq_info srcflagged list) let vel2str vel = (String.concat ", " (List.map LicDump.string_of_val_exp_eff vel)) in - let msg = "*** error expression " ^ (LicDump.string_of_val_exp_eff ve) ^ + let msg = + "*** error expression " ^ (LicDump.string_of_val_exp_eff ve) ^ "\n cannot be broken \n" ^(vel2str ve1l) ^ " should have the same arity as\n"^(vel2str ve2l) ^ "\n" - in - (* assert false *) + in raise (Errors.Compile_error(lxm, msg)) else List.map2 - (fun ve1 ve2 -> CallByPosEff ({it= Predef(IF_n,[]); src=lxm}, OperEff [cond;ve1;ve2])) + (fun ve1 ve2 -> + { ve with core = + CallByPosEff ({it= Predef(IF_n,[]); src=lxm}, + OperEff [cond;ve1;ve2])} + ) ve1l ve2l @@ -375,9 +378,8 @@ and (break_tuple : Lxm.t -> left list -> val_exp -> Eff.eq_info srcflagged list) else List.map2 (fun l ve -> - EvalType.add ve [Eff.type_of_left l]; EvalClock.add ve [(Eff.var_info_of_left l).var_clock_eff]; - { src = lxm ; it = ([l], ve) } + { src = lxm ; it = ([l], { ve with typ = [Eff.type_of_left l]}) } ) left_list vel @@ -403,7 +405,7 @@ and expand_val_exp_list n_env id_solver acc vel = and (expand_val_exp: Eff.local_env -> Eff.id_solver -> acc -> val_exp -> val_exp * acc) = fun n_env id_solver acc ve -> - match ve with + match ve.core with | CallByPosEff (by_pos_op, OperEff vel) -> let lxm = by_pos_op.src in let by_pos_op = by_pos_op.it in @@ -441,9 +443,9 @@ and (expand_val_exp: Eff.local_env -> Eff.id_solver -> acc -> val_exp -> in let newve = CallByPosEff(Lxm.flagit by_pos_op lxm, OperEff vel) in + let newve = { ve with core = newve } in if newve <> ve then ( - EvalType.copy newve ve; - EvalClock.copy newve ve + EvalClock.copy newve ve ); newve, acc @@ -451,7 +453,7 @@ and (expand_val_exp: Eff.local_env -> Eff.id_solver -> acc -> val_exp -> (* we want to print fields in the order of the type. Moreover, we have to deal with default value. *) - let teff = EvalType.lookup ve in + let teff = ve.typ in let ceff = EvalClock.lookup ve in match teff with | [Struct_type_eff(_,fl)] -> @@ -468,12 +470,10 @@ and (expand_val_exp: Eff.local_env -> Eff.id_solver -> acc -> val_exp -> | None -> assert false (* ougth to have been checked before *) | Some const -> - let tconst = Eff.true_type_of_const const in let ve_const = Eff.const_to_val_eff lxm true const in let _ = - EvalType.add ve_const [tconst]; EvalClock.add ve_const ceff; in let ve_const,acc= @@ -484,11 +484,12 @@ and (expand_val_exp: Eff.local_env -> Eff.id_solver -> acc -> val_exp -> ([],acc) fl in - let newve = - CallByPosEff({ src=lxm ; it=TUPLE }, OperEff (List.rev vel)) + let newve = { + typ = ve.typ; + core=CallByPosEff({ src=lxm ; it=TUPLE }, OperEff (List.rev vel)) + } in if newve <> ve then ( - EvalType.copy newve ve; EvalClock.copy newve ve ); newve, acc