diff --git a/compiler/global/idents.ml b/compiler/global/idents.ml index eca6811..f053693 100644 --- a/compiler/global/idents.ml +++ b/compiler/global/idents.ml @@ -19,8 +19,11 @@ type ident = { num : int; (* a unique index *) source : string; (* the original name in the source *) is_generated : bool; + is_reset : bool; } +let is_reset id = id.is_reset + type var_ident = ident let num = ref 0 @@ -124,18 +127,19 @@ struct Env.find id !env end -let gen_fresh pass_name kind_to_string kind = +let gen_fresh pass_name kind_to_string ?(reset=false) kind = let s = kind_to_string kind in let s = if !Compiler_options.full_name then "__"^pass_name ^ "_" ^ s else s in num := !num + 1; - let id = { num = !num; source = s; is_generated = true } in + let id = { num = !num; source = s; is_generated = true; is_reset = reset } in UniqueNames.assign_name id; id -let gen_var pass_name name = gen_fresh pass_name (fun () -> name) () +let gen_var pass_name ?(reset=false) name = + gen_fresh pass_name (fun () -> name) ~reset:reset () -let ident_of_name s = +let ident_of_name ?(reset=false) s = num := !num + 1; - let id = { num = !num; source = s; is_generated = false } in + let id = { num = !num; source = s; is_generated = false; is_reset = reset } in UniqueNames.assign_name id; id let source_name id = id.source diff --git a/compiler/global/idents.mli b/compiler/global/idents.mli index bc38346..7130fd7 100644 --- a/compiler/global/idents.mli +++ b/compiler/global/idents.mli @@ -24,15 +24,17 @@ val source_name : ident -> string (** [gen_fresh pass_name kind_to_string kind] generate a fresh ident with a sweet [name]. It should be used to define a [fresh] function specific to a pass. *) -val gen_fresh : string -> ('a -> string) -> 'a -> ident +val gen_fresh : string -> ('a -> string) -> ?reset:bool -> 'a -> ident (** [gen_var pass_name name] generates a fresh ident with a sweet [name] *) -val gen_var : string -> string -> ident +val gen_var : string -> ?reset:bool -> string -> ident (** [ident_of_name n] returns an fresh identifier corresponding to a _source_ variable (do not use it for generated variables). *) -val ident_of_name : string -> ident +val ident_of_name : ?reset:bool -> string -> ident + +val is_reset : ident -> bool (** /!\ This function should be called every time we enter a node *) val enter_node : Names.qualname -> unit diff --git a/compiler/heptagon/transformations/every.ml b/compiler/heptagon/transformations/every.ml index 836f9d9..c81ff95 100644 --- a/compiler/heptagon/transformations/every.ml +++ b/compiler/heptagon/transformations/every.ml @@ -16,10 +16,10 @@ let edesc funs (v,acc_eq_list) ed = let ed, (v, acc_eq_list) = Hept_mapfold.edesc funs (v,acc_eq_list) ed in match ed with | Eapp (op, e_list, Some re) when not (is_var re) -> - let re, vre, eqre = Reset.bool_var_from_exp re in + let re, vre, eqre = Reset.reset_var_from_exp re in Eapp(op, e_list, Some re), (vre::v, eqre::acc_eq_list) | Eiterator(it, op, n, pe_list, e_list, Some re) when not (is_var re) -> - let re, vre, eqre = Reset.bool_var_from_exp re in + let re, vre, eqre = Reset.reset_var_from_exp re in Eiterator(it, op, n, pe_list, e_list, Some re), (vre::v, eqre::acc_eq_list) | _ -> ed, (v, acc_eq_list) diff --git a/compiler/heptagon/transformations/reset.ml b/compiler/heptagon/transformations/reset.ml index 36918f8..594e478 100644 --- a/compiler/heptagon/transformations/reset.ml +++ b/compiler/heptagon/transformations/reset.ml @@ -22,10 +22,10 @@ open Initial -let fresh = Idents.gen_fresh "reset" (fun () -> "r") +let fresh = Idents.gen_fresh "reset" ~reset:true (fun () -> "r") (* get e and return r, var_dec_r, r = e *) -let bool_var_from_exp e = +let reset_var_from_exp e = let r = fresh() in { e with e_desc = Evar r }, mk_var_dec r (Tid Initial.pbool), mk_equation (Eeq(Evarpat r, e)) @@ -83,18 +83,6 @@ let edesc funs ((res,stateful) as acc) ed = match ed with let args,_ = mapfold (Hept_mapfold.exp_it funs) acc e_list in let re,_ = optional_wacc (Hept_mapfold.exp_it funs) acc re in Eiterator(it, op, n, pargs, args, None), acc (* funs don't need resets *) - | Emerge(x, c_e_l) -> - let aux acc (c,e) = - let res = match res with - | None -> None - | Some r -> Some (mk_exp (Ewhen (r,c,x)) Initial.tbool) in - let e,_ = Hept_mapfold.exp_it funs (res,stateful) e in - (c,e), acc - in - let c_e_l, acc = mapfold aux acc c_e_l in - Emerge(x, c_e_l), acc - - | _ -> raise Errors.Fallback let eq funs (res,_) eq = @@ -109,7 +97,7 @@ let eqdesc funs (res,stateful) = function | Ereset(b, e) -> if stateful then ( let e, _ = Hept_mapfold.exp_it funs (res,stateful) e in - let e, vd, eq = bool_var_from_exp e in + let e, vd, eq = reset_var_from_exp e in let r = merge_resets res (Some e) in let b, _ = Hept_mapfold.block_it funs (r,stateful) b in let b = { b with b_equs = eq::b.b_equs; b_local = vd::b.b_local; b_stateful = true } in diff --git a/compiler/minils/analysis/clocking.ml b/compiler/minils/analysis/clocking.ml index 59d5717..9907ccb 100644 --- a/compiler/minils/analysis/clocking.ml +++ b/compiler/minils/analysis/clocking.ml @@ -52,7 +52,10 @@ let error_message loc = function raise Errors.Error -let ck_of_name h x = Env.find x h +let ck_of_name h x = + if is_reset x + then fresh_clock() + else Env.find x h let rec typing_extvalue h w = let ck = match w.w_desc with diff --git a/test/good/ttt.ept b/test/bad/clock_annot.ept similarity index 100% rename from test/good/ttt.ept rename to test/bad/clock_annot.ept