From fbfa6eda1a2da9ef4998cb23c2d7464b80844e0b Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?L=C3=A9onard=20G=C3=A9rard?= Date: Wed, 18 May 2011 09:59:21 +0200 Subject: [PATCH] Add Ewhen to the minils ast, And clocking of iterators. Ewhen is now the only case of possible recursion for minils exps. This add was motivated by equations like : (y,z) = f(x) when c This equation to be correctly normalized in minils before needed : y',z' = f(x) y = y' when c z = z' when c But this new variables where needless since the final translation of when c is the identity. --- compiler/global/clocks.ml | 17 ++++ compiler/global/signature.ml | 11 +-- compiler/main/hept2mls.ml | 4 +- compiler/main/mls2obc.ml | 4 + compiler/minils/analysis/clocking.ml | 130 +++++++++++++++++---------- compiler/minils/minils.ml | 5 +- compiler/minils/mls_mapfold.ml | 3 + compiler/minils/mls_printer.ml | 2 + compiler/minils/mls_utils.ml | 5 +- 9 files changed, 119 insertions(+), 62 deletions(-) diff --git a/compiler/global/clocks.ml b/compiler/global/clocks.ml index 8bb2f4b..2094e3c 100644 --- a/compiler/global/clocks.ml +++ b/compiler/global/clocks.ml @@ -99,6 +99,19 @@ and unify_list t1_list t2_list = try List.iter2 unify t1_list t2_list with _ -> raise Unify +let rec skeleton ck = function + | Tprod ty_list -> + (match ty_list with + | [x] -> Ck ck + | l -> Cprod (List.map (skeleton ck) l)) + | Tarray _ | Tid _ | Tinvalid -> Ck ck + +let unprod ct = + let rec f acc ct = match ct with + | Ck ck -> ck::acc + | Cprod ct_l -> List.fold_left f acc ct_l + in + f [] ct let prod ck_l = match ck_l with | [ck] -> Ck ck @@ -108,6 +121,10 @@ let rec root_ck_of ck = match ck_repr ck with | Cbase | Cvar _ -> ck | Con(ck,_,_) -> root_ck_of ck +let rec last_clock ct = match ct with + | Ck ck -> ck + | Cprod l -> last_clock (Misc.last_element l) + (* let rec tuple ck = function | Tprod ty_list -> diff --git a/compiler/global/signature.ml b/compiler/global/signature.ml index c31c0d5..12eb04d 100644 --- a/compiler/global/signature.ml +++ b/compiler/global/signature.ml @@ -59,11 +59,10 @@ type const_def = { c_type : ty; c_value : static_exp } (** { 3 Signature helper functions } *) type error = - | Eckvar_unbound of name option * name | Eckvar_unbound_input of name option * name | Eckvar_unbound_ouput of name option * name -exception SignatureError of error +exception SignatureError of name option * name let message loc e = begin match e with | Eckvar_unbound_input(var_name,ck_name) -> @@ -76,8 +75,6 @@ let message loc e = begin match e with Format.eprintf "%a%s sampled ouput%s should be returned with its sampling value %s.@." print_location loc a name ck_name - | Eckvar_unbound(var_name,ck_name) -> - Format.eprintf "%aThe variable %s is unbound.@." print_location loc ck_name end; raise Errors.Error @@ -98,7 +95,7 @@ let check_signature s = | Cbase -> () | Con(ck,_,x) -> if not (NamesSet.mem x env) - then raise (SignatureError (Eckvar_unbound (n,x))); + then raise (SignatureError (n,x)); f ck in f arg.a_clock @@ -106,11 +103,11 @@ let check_signature s = (*initial env with only the inputs*) let env = append NamesSet.empty s.node_inputs in (try List.iter (check env) s.node_inputs - with SignatureError (Eckvar_unbound (x,c)) -> + with SignatureError (x,c) -> message s.node_loc (Eckvar_unbound_input (x,c))); let env = append env s.node_outputs in try List.iter (check env) s.node_outputs - with SignatureError (Eckvar_unbound (x,c)) -> + with SignatureError (x,c) -> message s.node_loc (Eckvar_unbound_ouput (x,c)) diff --git a/compiler/main/hept2mls.ml b/compiler/main/hept2mls.ml index c9bc74a..a54402b 100644 --- a/compiler/main/hept2mls.ml +++ b/compiler/main/hept2mls.ml @@ -98,15 +98,15 @@ let rec translate_extvalue e = mk_extvalue (Wfield (translate_extvalue e, fn)) | _ -> Error.message e.Heptagon.e_loc Error.Enormalization -let translate ({ Heptagon.e_desc = desc; Heptagon.e_ty = ty; Heptagon.e_level_ck = b_ck; +let rec translate ({ Heptagon.e_desc = desc; Heptagon.e_ty = ty; Heptagon.e_level_ck = b_ck; Heptagon.e_ct_annot = a_ct; Heptagon.e_loc = loc } as e) = let desc = match desc with | Heptagon.Econst _ | Heptagon.Evar _ - | Heptagon.Ewhen _ | Heptagon.Eapp({ Heptagon.a_op = Heptagon.Efield }, _, _) -> let w = translate_extvalue e in Eextvalue w + | Heptagon.Ewhen (e,c,x) -> Ewhen (translate e, c, x) | Heptagon.Epre(None, e) -> Efby(None, translate_extvalue e) | Heptagon.Epre(Some c, e) -> diff --git a/compiler/main/mls2obc.ml b/compiler/main/mls2obc.ml index 83e09c6..993352d 100644 --- a/compiler/main/mls2obc.ml +++ b/compiler/main/mls2obc.ml @@ -209,6 +209,9 @@ let rec translate map e = let e = translate_extvalue map (assert_1 e_list) in let idx_list = List.map (fun idx -> mk_exp tint (Econst idx)) idx in Epattern (pattern_of_idx_list (pattern_of_exp e) idx_list) + | Minils.Ewhen(e,_,_) -> + let e = translate map e in + e.e_desc (* Already treated cases when translating the [eq] *) | Minils.Eiterator _ | Minils.Emerge _ | Minils.Efby _ | Minils.Eapp ({Minils.a_op=(Minils.Enode _|Minils.Efun _|Minils.Econcat @@ -231,6 +234,7 @@ and translate_act map pat ({ Minils.e_desc = desc } as act) = match pat, desc with (* When Merge *) + | pat, Minils.Ewhen (e,_,_) -> translate_act map pat e | Minils.Evarpat x, Minils.Emerge (y, c_act_list) -> let x = var_from_name map x in let translate_c_extvalue (c, w) = diff --git a/compiler/minils/analysis/clocking.ml b/compiler/minils/analysis/clocking.ml index 5d5c2b2..4b671ce 100644 --- a/compiler/minils/analysis/clocking.ml +++ b/compiler/minils/analysis/clocking.ml @@ -97,7 +97,7 @@ let typing_app h base pat op w_list = match op with in let env_pat = build_env node.node_outputs pat_id_list [] in let env_args = build_env node.node_inputs w_list [] in - (* implement with Cbase as base, replace name dep by ident dep *) +(* implement with Cbase as base, replace name dep by ident dep *) let rec sigck_to_ck sck = match sck with | Signature.Cbase -> base | Signature.Con (sck,c,x) -> @@ -118,55 +118,89 @@ let typing_app h base pat op w_list = match op with Clocks.prod (List.map (fun a -> sigck_to_ck a.a_clock) node.node_outputs) -let typing_eq h { eq_lhs = pat; eq_rhs = e } = - (* typing the expression *) - let ct,base = match e.e_desc with - | Eextvalue w - | Efby (_, w) -> - let ck = typing_extvalue h w in - Ck ck, ck - | Emerge (x, c_e_list) -> - let ck = ck_of_name h x in - List.iter (fun (c,e) -> expect_extvalue h (Con (ck,c,x)) e) c_e_list; - Ck ck, ck - | Estruct l -> - let ck = fresh_clock () in - List.iter (fun (_, e) -> expect_extvalue h ck e) l; - Ck ck, ck - | Eapp({a_op = op}, args, r) -> - let ck_r = match r with - | None -> fresh_clock () - | Some(reset) -> ck_of_name h reset in - let ct = typing_app h ck_r pat op args in - ct, ck_r - | Eiterator (_, _, _, pargs, args, r) -> (*TODO*) - (* Typed exactly as a fun or a node... *) - let ck_r = match r with - | None -> fresh_clock() - | Some(reset) -> ck_of_name h reset - in - List.iter (expect_extvalue h ck_r) pargs; - List.iter (expect_extvalue h ck_r) args; - Ck ck_r, ck_r - in - e.e_base_ck <- base; - begin - try unify ct e.e_ct - with Unify -> - eprintf "Incoherent clock annotation.@\n"; - error_message e.e_loc (Etypeclash (ct,e.e_ct)) - end; - e.e_ct <- ct; - (* typing the full equation *) - let pat_ct = typing_pat h pat in - begin - try unify ct pat_ct - with Unify -> - eprintf "Incoherent clock between right and left side of the equation@\n"; - error_message e.e_loc (Etypeclash (ct, pat_ct)) - end +let typing_eq h { eq_lhs = pat; eq_rhs = e } = + (* typing the expression, returns ct, ck_base *) + let rec typing e = + let ct,base = match e.e_desc with + | Eextvalue w + | Efby (_, w) -> + let ck = typing_extvalue h w in + Ck ck, ck + | Ewhen (e,c,n) -> + let ck_n = ck_of_name h n in + let base = expect (skeleton ck_n e.e_ty) e in + skeleton (Con (ck_n, c, n)) e.e_ty, base + | Emerge (x, c_e_list) -> + let ck = ck_of_name h x in + List.iter (fun (c,e) -> expect_extvalue h (Con (ck,c,x)) e) c_e_list; + Ck ck, ck + | Estruct l -> + let ck = fresh_clock () in + List.iter (fun (_, e) -> expect_extvalue h ck e) l; + Ck ck, ck + | Eapp({a_op = op}, args, r) -> + (* base clock of the node *) + let ck_r = match r with + | None -> fresh_clock () + | Some(reset) -> ck_of_name h reset in + let ct = typing_app h ck_r pat op args in + ct, ck_r + | Eiterator (it, {a_op = op}, _, pargs, args, r) -> + (* base clock of the node *) + let ck_r = match r with + | None -> fresh_clock() + | Some(reset) -> ck_of_name h reset + in + let ct = match it with + | Imap -> (* exactly as if clocking the node *) + typing_app h ck_r pat op args + | Imapi -> (* clocking the node with the extra [i] input on [ck_r] *) + let i (* stubs [i] as 0 *) = + mk_extvalue ~ty:Initial.tint ~clock:ck_r (Wconst (Initial.mk_static_int 0)) + in + typing_app h ck_r pat op (args@[i]) + | Ifold | Imapfold -> + (* clocking node with equality constaint on last input and last output *) + let ct = typing_app h ck_r pat op args in + unify_ck (Clocks.last_clock ct) (Misc.last_element args).w_ck; + ct + | Ifoldi -> (* clocking the node with the extra [i] and last in/out constraints *) + let i (* stubs [i] as 0 *) = + mk_extvalue ~ty:Initial.tint ~clock:ck_r (Wconst (Initial.mk_static_int 0)) + in + let rec insert_i args = match args with + | [] -> [i] + | [l] -> i::[l] + | h::l -> h::(insert_i l) + in + let ct = typing_app h ck_r pat op (insert_i args) in + unify_ck (Clocks.last_clock ct) (Misc.last_element args).w_ck; + ct + in + ct, ck_r + in + e.e_base_ck <- base; + (try unify ct e.e_ct + with Unify -> + eprintf "Incoherent clock annotation.@\n"; + error_message e.e_loc (Etypeclash (ct,e.e_ct))); + e.e_ct <- ct; + ct, base + and expect expected_ct e = + let actual_ct,base = typing e in + (try unify actual_ct expected_ct + with Unify -> error_message e.e_loc (Etypeclash (actual_ct, expected_ct))); + base + in + let ct,base = typing e in + let pat_ct = typing_pat h pat in + (try unify ct pat_ct + with Unify -> + eprintf "Incoherent clock between right and left side of the equation.@\n"; + error_message e.e_loc (Etypeclash (ct, pat_ct))) + let typing_eqs h eq_list = List.iter (typing_eq h) eq_list let append_env h vds = diff --git a/compiler/minils/minils.ml b/compiler/minils/minils.ml index eefcb9a..4aae37d 100644 --- a/compiler/minils/minils.ml +++ b/compiler/minils/minils.ml @@ -53,7 +53,7 @@ and extvalue_desc = and exp = { e_desc : edesc; - e_level_ck : ck; (* when no data dep, execute the exp on this clock (set by [switch] *) + e_level_ck : ck; (*when no data dep, execute the exp on this clock (set by [switch] *) mutable e_base_ck : ck; mutable e_ct : ct; e_ty : ty; @@ -65,13 +65,14 @@ and edesc = (** static_exp fby extvalue *) | Eapp of app * extvalue list * var_ident option (** app ~args=(extvalue,extvalue...) reset ~r=ident *) + | Ewhen of exp * constructor_name * var_ident (** e when C(c) *) | Emerge of var_ident * (constructor_name * extvalue) list (** merge ident (Constructor -> extvalue)+ *) | Estruct of (field_name * extvalue) list (** { field=extvalue; ... } *) | Eiterator of iterator_type * app * static_exp * extvalue list * extvalue list * var_ident option - (** map f <> (extvalue, extvalue...) reset ident *) + (** map f <> <(extvalue)> (extvalue) reset ident *) and app = { a_op: op; a_params: static_exp list; a_unsafe: bool } (** Unsafe applications could have side effects diff --git a/compiler/minils/mls_mapfold.ml b/compiler/minils/mls_mapfold.ml index 0cb5d02..ff66125 100644 --- a/compiler/minils/mls_mapfold.ml +++ b/compiler/minils/mls_mapfold.ml @@ -85,6 +85,9 @@ and edesc funs acc ed = match ed with (c,w), acc in let c_w_list, acc = mapfold aux acc c_w_list in Emerge(x, c_w_list), acc + | Ewhen(e,c,x) -> + let e, acc = exp_it funs acc e in + Ewhen(e,c,x), acc | Estruct n_w_list -> let aux acc (n,w) = let w, acc = extvalue_it funs acc w in diff --git a/compiler/minils/mls_printer.ml b/compiler/minils/mls_printer.ml index 10b00f3..138e3de 100644 --- a/compiler/minils/mls_printer.ml +++ b/compiler/minils/mls_printer.ml @@ -102,6 +102,8 @@ and print_exp_desc ff = function fprintf ff "@[<2>%a@,%a@]" print_app (app, args) print_every reset | Emerge (x, tag_w_list) -> fprintf ff "@[<2>merge %a@ %a@]" print_ident x print_tag_w_list tag_w_list + | Ewhen (e,c,x) -> + fprintf ff "@[<2>(%a@ when %a(%a))@]" print_exp e print_qualname c print_ident x | Estruct f_w_list -> print_record (print_couple print_qualname print_extvalue """ = """) ff f_w_list | Eiterator (it, f, param, pargs, args, reset) -> diff --git a/compiler/minils/mls_utils.ml b/compiler/minils/mls_utils.ml index ed55270..0b62477 100644 --- a/compiler/minils/mls_utils.ml +++ b/compiler/minils/mls_utils.ml @@ -193,10 +193,9 @@ let eq_find id = List.find (fun eq -> List.mem id (Vars.def [] eq)) let ident_list_of_pat pat = let rec f acc pat = match pat with | Evarpat id -> id::acc - | Etuplepat [] -> acc - | Etuplepat (pat::pat_l) -> f (f acc pat) (Etuplepat pat_l) + | Etuplepat pat_l -> List.fold_left f acc pat_l in - f [] pat + List.rev (f [] pat) let args_of_var_decs =