From a22f7216f20cf1d0aa124025e4143c7518395f9f Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Le=CC=81onard=20Ge=CC=81rard?= Date: Mon, 1 Nov 2010 01:04:35 +0100 Subject: [PATCH] Added when and merge to heptagon. Need tests ! Clocking is still done in minils since it is way simpler. --- compiler/global/clocks.ml | 2 +- compiler/global/global_mapfold.ml | 2 +- compiler/global/global_printer.ml | 15 +++++ compiler/global/idents.mli | 3 - compiler/heptagon/analysis/causality.ml | 7 ++ compiler/heptagon/analysis/initialization.ml | 13 +++- compiler/heptagon/analysis/typing.ml | 67 ++++++++++++++++--- compiler/heptagon/hept_mapfold.ml | 10 +++ compiler/heptagon/hept_printer.ml | 20 ++++-- compiler/heptagon/heptagon.ml | 16 +++-- compiler/heptagon/main/hept_compiler.ml | 2 +- compiler/heptagon/parsing/hept_scoping.ml | 1 + compiler/heptagon/transformations/reset.ml | 6 +- compiler/main/hept2mls.ml | 5 ++ compiler/main/mls2obc.ml | 2 - compiler/minils/analysis/clocking.ml | 12 ++-- .../minils/transformations/singletonvars.ml | 1 + compiler/minils/transformations/tomato.ml | 1 + 18 files changed, 150 insertions(+), 35 deletions(-) diff --git a/compiler/global/clocks.ml b/compiler/global/clocks.ml index cde5c5b..91f11b7 100644 --- a/compiler/global/clocks.ml +++ b/compiler/global/clocks.ml @@ -33,7 +33,7 @@ let index = ref 0 let gen_index () = (incr index; !index) (** returns a new clock variable *) -let new_var () = Cvar { contents = Cindex (gen_index ()); } +let fresh_clock () = Cvar { contents = Cindex (gen_index ()); } (** returns the canonic (short) representant of a [ck] and update it to this value. *) diff --git a/compiler/global/global_mapfold.ml b/compiler/global/global_mapfold.ml index 6d69ba2..f90d634 100644 --- a/compiler/global/global_mapfold.ml +++ b/compiler/global/global_mapfold.ml @@ -50,6 +50,7 @@ and static_exp_desc funs acc sd = match sd with let f_se_l, acc = mapfold aux acc f_se_l in Srecord f_se_l, acc + and ty_it funs acc t = try funs.ty funs acc t with Fallback -> ty funs acc t and ty funs acc t = match t with | Tid _ -> t, acc @@ -58,7 +59,6 @@ and ty funs acc t = match t with let t, acc = ty_it funs acc t in let se, acc = static_exp_it funs acc se in Tarray (t, se), acc - (* and ct_it funs acc c = try funs.ct funs acc c with Fallback -> ct funs acc t and ct funs acc c = match c with diff --git a/compiler/global/global_printer.ml b/compiler/global/global_printer.ml index 759d470..0a4be9e 100644 --- a/compiler/global/global_printer.ml +++ b/compiler/global/global_printer.ml @@ -1,4 +1,5 @@ open Names +open Idents open Signature open Types open Clocks @@ -107,3 +108,17 @@ let print_interface ff = (fun key sigtype -> print_interface_value ff key sigtype) m.m_values; Format.fprintf ff "@." +let print_ident ff id = Format.fprintf ff "%s" (name id) + + let rec print_ck ff = function + | Cbase -> fprintf ff "base" + | Con (ck, c, n) -> + fprintf ff "%a on %a(%a)" print_ck ck print_qualname c print_ident n + | Cvar { contents = Cindex _ } -> fprintf ff "base" + | Cvar { contents = Clink ck } -> print_ck ff ck + +let rec print_clock ff = function + | Ck ck -> print_ck ff ck + | Cprod ct_list -> + fprintf ff "@[<2>(%a)@]" (print_list_r print_clock """ *""") ct_list + diff --git a/compiler/global/idents.mli b/compiler/global/idents.mli index 82bc420..fb6e88b 100644 --- a/compiler/global/idents.mli +++ b/compiler/global/idents.mli @@ -46,6 +46,3 @@ sig include (Set.S with type elt = ident) val fprint_t : Format.formatter -> t -> unit end - - -val print_ident : Format.formatter -> ident -> unit diff --git a/compiler/heptagon/analysis/causality.ml b/compiler/heptagon/analysis/causality.ml index eec9a92..5e07a51 100644 --- a/compiler/heptagon/analysis/causality.ml +++ b/compiler/heptagon/analysis/causality.ml @@ -108,6 +108,13 @@ let rec typing e = candlist l | Eiterator (_, _, _, e_list, _) -> ctuplelist (List.map typing e_list) + | Ewhen (e, c, n) -> + let t = typing e in + cseq (read n) t + | Emerge (n, c_e_list) -> + let tl = List.map (fun (_,e) -> typing e) c_e_list in + cseq (read n) (candlist tl) + (** Typing an application *) and apply op e_list = diff --git a/compiler/heptagon/analysis/initialization.ml b/compiler/heptagon/analysis/initialization.ml index 90068d5..374f01a 100644 --- a/compiler/heptagon/analysis/initialization.ml +++ b/compiler/heptagon/analysis/initialization.ml @@ -169,6 +169,7 @@ let rec less left_ty right_ty = module Printer = struct open Format open Pp_tools + open Global_printer let rec print_init ff i = match !i with | Izero -> fprintf ff "initialized" @@ -223,7 +224,7 @@ let less_exp e actual_ty expected_ty = (** Main typing function *) let rec typing h e = match e.e_desc with - | Econst c -> skeleton izero e.e_ty + | Econst _ -> skeleton izero e.e_ty | Evar(x) -> IEnv.find_var_typ x h | Elast(x) -> IEnv.find_last_typ x h | Epre(None, e1) -> @@ -248,6 +249,16 @@ let rec typing h e = | Eiterator (_, _, _, e_list, _) -> List.iter (fun e -> initialized_exp h e) e_list; skeleton izero e.e_ty + | Ewhen (e, _, n) -> + let i = imax (itype (IEnv.find_var_typ n h)) (itype (typing h e)) in + skeleton i e.e_ty + | Emerge (n, c_e_list) -> + let i = + List.fold_left + (fun acc (_, e) -> imax acc (itype (typing h e))) izero c_e_list in + let i = imax (itype (IEnv.find_var_typ n h)) i in + skeleton i e.e_ty + (** Typing an application *) and apply h app e_list = diff --git a/compiler/heptagon/analysis/typing.ml b/compiler/heptagon/analysis/typing.ml index 1eaaed9..5c7ba7a 100644 --- a/compiler/heptagon/analysis/typing.ml +++ b/compiler/heptagon/analysis/typing.ml @@ -20,6 +20,7 @@ open Types open Global_printer open Heptagon open Hept_mapfold +open Pp_tools type value = { ty: ty; mutable last: bool } @@ -46,6 +47,9 @@ type error = | Eempty_record | Eempty_array | Efoldi_bad_args of ty + | Emerge_missing_constrs of qualname list + | Emerge_not_enum of name * ty + | Emerge_unexpected_constr of qualname exception Unify exception TypingError of error @@ -91,6 +95,21 @@ let message loc kind = Format.eprintf "%aThe name %s is already defined.@." print_location loc s + | Emerge_missing_constrs cl -> + Format.eprintf "%aSome constructors are missing in this merge :@\n\ + @[%a@]@." + print_location loc + (print_list_r print_qualname """,""") cl + | Emerge_not_enum (n,t) -> + Format.eprintf + "%aThe merge variable %a should be of an enum type (found %a)@." + print_location loc + print_name n + print_type t + | Emerge_unexpected_constr c -> + Format.eprintf "%aThe constructor %a is unexpected.@." + print_location loc + print_qualname c | Enon_exaustive -> Format.eprintf "%aSome constructors are missing in this \ pattern/matching.@." @@ -166,9 +185,9 @@ let find_with_error find_fun f = try find_fun f with Not_found -> error (Eundefined(fullname f)) -let find_value = find_with_error find_value -let find_constrs = find_with_error find_constrs -let find_field = find_with_error find_field +let find_value v = find_with_error find_value v +let find_constrs c = Tid (find_with_error find_constrs c) +let find_field f = find_with_error find_field f (** Constraints related functions *) let (curr_size_constr : size_constraint list ref) = ref [] @@ -393,7 +412,7 @@ and typing_static_exp const_env se = Svar ln, cd.Signature.c_type with Not_found -> (* or a static parameter *) Svar ln, QualEnv.find ln const_env) - | Sconstructor c -> Sconstructor c, Tid (find_constrs c) + | Sconstructor c -> Sconstructor c, find_constrs c | Sfield c -> Sfield c, Tid (find_field c) | Sop (op, se_list) -> let ty_desc = find_value op in @@ -423,10 +442,9 @@ and typing_static_exp const_env se = | [] -> error (Eempty_record) | (f,_)::_ -> struct_info_from_field f ) in - + check_static_field_unicity f_se_list; if List.length f_se_list <> List.length fields then message se.se_loc Esome_fields_are_missing; - check_static_field_unicity f_se_list; let f_se_list = List.map (typing_static_field const_env fields (Tid q)) f_se_list in @@ -539,6 +557,40 @@ let rec typing const_env h e = , typed_n, typed_e_list, reset), ty | Eiterator _ -> assert false + + | Ewhen (e, c, n) -> + let typed_e, t = typing const_env h e in + let tn_expected = find_constrs c in + let tn_actual = typ_of_name h n in + unify tn_actual tn_expected; + Ewhen (typed_e, c, n), t + + | Emerge (n, (c1,e1)::c_e_list) -> + let tn_actual = typ_of_name h n in + unify tn_actual (find_constrs c1); + let typed_e1, t = typing const_env h e1 in + let expected_c_list = (* constructors from the type of n *) + (match tn_actual with + | Tid tc -> + (match find_type tc with + | Tenum cl -> cl + | _ -> message e.e_loc (Emerge_not_enum (name n,tn_actual))) + | _ -> message e.e_loc (Emerge_not_enum (name n,tn_actual))) in + let expected_c_set = + List.fold_left + (fun acc c -> QualSet.add c acc) QualSet.empty expected_c_list in + let typed_c_e_list, left_c_set = + let check_c_e expected_c_set (c,e) = + if not (QualSet.mem c expected_c_set) + then message e.e_loc (Emerge_unexpected_constr c); + (c, expect const_env h t e), QualSet.remove c expected_c_set in + mapfold check_c_e expected_c_set c_e_list in + if not (QualSet.is_empty left_c_set) + then message e.e_loc + (Emerge_missing_constrs (QualSet.elements left_c_set)); + Emerge (n, (c1,typed_e1)::typed_c_e_list), t + | Emerge (_, []) -> assert false + in { e with e_desc = typed_desc; e_ty = ty; }, ty with @@ -1017,8 +1069,7 @@ let typing_const_dec cd = { cd with c_value = se; c_type = ty } let program - ({ p_opened = opened; p_types = p_type_list; - p_nodes = p_node_list; p_consts = p_consts_list } as p) = + ({ p_nodes = p_node_list; p_consts = p_consts_list } as p) = let typed_cd_list = List.map typing_const_dec p_consts_list in let typed_node_list = List.map node p_node_list in { p with p_nodes = typed_node_list; p_consts = typed_cd_list } diff --git a/compiler/heptagon/hept_mapfold.ml b/compiler/heptagon/hept_mapfold.ml index 1ca14d7..22a9722 100644 --- a/compiler/heptagon/hept_mapfold.ml +++ b/compiler/heptagon/hept_mapfold.ml @@ -135,6 +135,16 @@ and edesc funs acc ed = match ed with let args, acc = mapfold (exp_it funs) acc args in let reset, acc = optional_wacc (exp_it funs) acc reset in Eiterator (i, app, param, args, reset), acc + | Ewhen (e, c, n) -> + let e, acc = exp_it funs acc e in + Ewhen (e, c, n), acc + | Emerge (n, c_e_list) -> + let aux acc (c,e) = + let e, acc = exp_it funs acc e in + (c,e), acc in + let c_e_list, acc = mapfold aux acc c_e_list in + Emerge (n, c_e_list), acc + and app_it funs acc a = funs.app funs acc a diff --git a/compiler/heptagon/hept_printer.ml b/compiler/heptagon/hept_printer.ml index c7e1cdf..89f2760 100644 --- a/compiler/heptagon/hept_printer.ml +++ b/compiler/heptagon/hept_printer.ml @@ -96,14 +96,14 @@ and print_exp_desc ff = function | Econst c -> print_static_exp ff c | Epre(None, e) -> fprintf ff "pre %a" print_exp e | Epre(Some c, e) -> - fprintf ff "@[<2>%a fby@ %a@]" print_static_exp c print_exp e + fprintf ff "@[<2>%a fby@ %a@]" print_static_exp c print_exp e | Efby(e1, e2) -> - fprintf ff "@[<2>%a fby@ %a@]" print_exp e1 print_exp e2 + fprintf ff "@[<2>%a fby@ %a@]" print_exp e1 print_exp e2 | Eapp(app, args, reset) -> - fprintf ff "@[<2>%a@,%a@]" + fprintf ff "@[<2>%a@,%a@]" print_app (app, args) print_every reset | Estruct(f_e_list) -> - print_record (print_couple print_qualname print_exp """ = """) ff f_e_list + print_record (print_couple print_qualname print_exp """ = """) ff f_e_list | Eiterator (it, f, param, args, reset) -> fprintf ff "@[<2>(%s (%a)<<%a>>)@,%a@]%a" (iterator_to_string it) @@ -111,6 +111,18 @@ and print_exp_desc ff = function print_static_exp param print_exp_tuple args print_every reset + | Ewhen (e, c, n) -> + fprintf ff "@[<2>(%a@ when %a(%a))@]" + print_exp e print_qualname c print_ident n + | Emerge (x, tag_e_list) -> + fprintf ff "@[<2>merge %a@ %a@]" + print_ident x print_tag_e_list tag_e_list + +and print_handler ff c = + fprintf ff "@[<2>%a@]" (print_couple print_qualname print_exp "("" -> "")") c + +and print_tag_e_list ff tag_e_list = + fprintf ff "@[%a@]" (print_list print_handler """""") tag_e_list and print_every ff reset = print_opt (fun ff id -> fprintf ff " every %a" print_exp id) ff reset diff --git a/compiler/heptagon/heptagon.ml b/compiler/heptagon/heptagon.ml index 0521e19..2bafe0c 100644 --- a/compiler/heptagon/heptagon.ml +++ b/compiler/heptagon/heptagon.ml @@ -14,6 +14,7 @@ open Idents open Static open Signature open Types +open Clocks open Initial type state_name = name @@ -36,6 +37,10 @@ and desc = | Epre of static_exp option * exp | Efby of exp * exp | Estruct of (field_name * exp) list + | Ewhen of exp * constructor_name * var_ident + (** exp when Constructor(ident) *) + | Emerge of var_ident * (constructor_name * exp) list + (** merge ident (Constructor -> exp)+ *) | Eapp of app * exp list * exp option | Eiterator of iterator_type * app * static_exp * exp list * exp option @@ -106,6 +111,7 @@ and present_handler = { and var_dec = { v_ident : var_ident; v_type : ty; + v_clock : ck; v_last : last; v_loc : location } @@ -187,16 +193,18 @@ let mk_type_dec name desc = let mk_equation ?(statefull = true) desc = { eq_desc = desc; eq_statefull = statefull; eq_loc = no_location; } -let mk_var_dec ?(last = Var) name ty = - { v_ident = name; v_type = ty; +let mk_var_dec ?(last = Var) ?(ck = fresh_clock()) name ty = + { v_ident = name; v_type = ty; v_clock = ck; v_last = last; v_loc = no_location } let mk_block ?(statefull = true) ?(defnames = Env.empty) eqs = { b_local = []; b_equs = eqs; b_defnames = defnames; b_statefull = statefull; b_loc = no_location } -let dfalse = mk_exp (Econst (mk_static_bool false)) (Tid Initial.pbool) -let dtrue = mk_exp (Econst (mk_static_bool true)) (Tid Initial.pbool) +let dfalse = + mk_exp (Econst (mk_static_bool false)) (Tid Initial.pbool) +let dtrue = + mk_exp (Econst (mk_static_bool true)) (Tid Initial.pbool) let mk_ifthenelse e1 e2 e3 = { e3 with e_desc = mk_op_app Eifthenelse [e1; e2; e3] } diff --git a/compiler/heptagon/main/hept_compiler.ml b/compiler/heptagon/main/hept_compiler.ml index 0a358a2..11b28cc 100644 --- a/compiler/heptagon/main/hept_compiler.ml +++ b/compiler/heptagon/main/hept_compiler.ml @@ -36,8 +36,8 @@ let parse_interface lexbuf = let compile_impl pp p = (* Typing *) - let p = pass "Typing" true Typing.program p pp in let p = silent_pass "Statefullness check" true Statefull.program p in + let p = pass "Typing" true Typing.program p pp in if !print_types then print_interface Format.std_formatter; diff --git a/compiler/heptagon/parsing/hept_scoping.ml b/compiler/heptagon/parsing/hept_scoping.ml index 2e271a1..7e99da4 100644 --- a/compiler/heptagon/parsing/hept_scoping.ml +++ b/compiler/heptagon/parsing/hept_scoping.ml @@ -368,6 +368,7 @@ and translate_var_dec local_const env vd = { Heptagon.v_ident = Rename.var vd.v_loc env vd.v_name; Heptagon.v_type = translate_type vd.v_loc local_const vd.v_type; Heptagon.v_last = translate_last local_const vd.v_last; + Heptagon.v_clock = Clocks.fresh_clock(); (* TODO add clock annotations *) Heptagon.v_loc = vd.v_loc } and translate_vd_list local_const env = diff --git a/compiler/heptagon/transformations/reset.ml b/compiler/heptagon/transformations/reset.ml index 8b5507e..67fa7ca 100644 --- a/compiler/heptagon/transformations/reset.ml +++ b/compiler/heptagon/transformations/reset.ml @@ -45,10 +45,8 @@ open Initial e1 -> e2 is translated into if (true fby false) then e1 else e2 *) -let mk_bool_var n = - mk_exp (Evar n) (Tid Initial.pbool) -let mk_bool_param n = - mk_var_dec n (Tid Initial.pbool) +let mk_bool_var n = mk_exp (Evar n) (Tid Initial.pbool) +let mk_bool_param n = mk_var_dec n (Tid Initial.pbool) let or_op_call e_list = mk_op_app (Efun Initial.por) e_list diff --git a/compiler/main/hept2mls.ml b/compiler/main/hept2mls.ml index a44d186..e1c7ff0 100644 --- a/compiler/main/hept2mls.ml +++ b/compiler/main/hept2mls.ml @@ -247,6 +247,11 @@ let rec translate env | Heptagon.Efby _ | Heptagon.Elast _ -> Error.message loc Error.Eunsupported_language_construct + | Heptagon.Ewhen (e, c, n) -> + mk_exp ~loc:loc ~ty:ty (Ewhen (translate env e, c, n)) + | Heptagon.Emerge (n, c_e_list) -> + mk_exp ~loc:loc ~ty:ty + (Emerge (n, List.map (fun (c,e) -> c, translate env e) c_e_list)) let rec translate_pat = function | Heptagon.Evarpat(n) -> Evarpat n diff --git a/compiler/main/mls2obc.ml b/compiler/main/mls2obc.ml index 4cbd9c7..631e31d 100644 --- a/compiler/main/mls2obc.ml +++ b/compiler/main/mls2obc.ml @@ -422,8 +422,6 @@ let translate_contract map mem_vars = { Minils.c_eq = eq_list; Minils.c_local = d_list; - Minils.c_assume = e_a; - Minils.c_enforce = e_c } -> let (v, si, j, s_list) = translate_eq_list map empty_call_context eq_list in diff --git a/compiler/minils/analysis/clocking.ml b/compiler/minils/analysis/clocking.ml index c039007..ffac52d 100644 --- a/compiler/minils/analysis/clocking.ml +++ b/compiler/minils/analysis/clocking.ml @@ -35,17 +35,17 @@ let typ_of_name h x = Env.find x h let rec typing h e = let ct = match e.e_desc with - | Econst se -> skeleton (new_var ()) se.se_ty + | Econst se -> skeleton (fresh_clock ()) se.se_ty | Evar x -> Ck (typ_of_name h x) | Efby (_, e) -> typing h e | Eapp({a_op = op}, args, r) -> let ck = match r with - | None -> new_var () + | None -> fresh_clock () | Some(reset) -> typ_of_name h reset in typing_op op args h e ck | Eiterator (_, _, _, args, r) -> (* Typed exactly as a fun or a node... *) let ck = match r with - | None -> new_var() + | None -> fresh_clock() | Some(reset) -> typ_of_name h reset in (List.iter (expect h (Ck ck)) args; skeleton ck e.e_ty) | Ewhen (e, c, n) -> @@ -55,14 +55,14 @@ let rec typing h e = let ck_c = typ_of_name h n in (typing_c_e_list h ck_c n c_e_list; skeleton ck_c e.e_ty) | Estruct l -> - let ck = new_var () in + let ck = fresh_clock () in (List.iter (fun (_, e) -> let ct = skeleton ck e.e_ty in expect h ct e) l; Ck ck) in (e.e_ck <- ckofct ct; ct) and typing_op op e_list h e ck = match op with - | (Eequal | Efun _ | Enode _) -> + | (Eequal | Efun _ | Enode _) -> (*LA*) List.iter (fun e -> expect h (skeleton ck e.e_ty) e) e_list; skeleton ck e.e_ty | Etuple -> @@ -128,7 +128,7 @@ let typing_eqs h eq_list = (*TODO FIXME*) in List.iter typing_eq eq_list let build h dec = - List.fold_left (fun h { v_ident = n } -> Env.add n (new_var ()) h) h dec + List.fold_left (fun h { v_ident = n } -> Env.add n (fresh_clock ()) h) h dec let sbuild h dec base = List.fold_left (fun h { v_ident = n } -> Env.add n base h) h dec diff --git a/compiler/minils/transformations/singletonvars.ml b/compiler/minils/transformations/singletonvars.ml index 7e21ef3..fb547e5 100644 --- a/compiler/minils/transformations/singletonvars.ml +++ b/compiler/minils/transformations/singletonvars.ml @@ -14,6 +14,7 @@ open Signature open Minils open Mls_utils open Mls_printer +open Global_printer open Types open Clocks open Pp_tools diff --git a/compiler/minils/transformations/tomato.ml b/compiler/minils/transformations/tomato.ml index fc456c4..5d38ac2 100644 --- a/compiler/minils/transformations/tomato.ml +++ b/compiler/minils/transformations/tomato.ml @@ -14,6 +14,7 @@ open Signature open Minils open Mls_utils open Mls_printer +open Global_printer open Types open Clocks open Pp_tools