From 59c8106e46c3f68854d981c2aa74e249b93ced15 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?C=C3=A9dric=20Pasteur?= Date: Fri, 29 Apr 2011 14:46:32 +0200 Subject: [PATCH] Also use idents for Ewhen in Heptagon --- compiler/heptagon/analysis/causality.ml | 4 ++-- compiler/heptagon/analysis/initialization.ml | 4 ++-- compiler/heptagon/analysis/typing.ml | 6 +++--- compiler/heptagon/hept_printer.ml | 4 ++-- compiler/heptagon/heptagon.ml | 2 +- compiler/heptagon/parsing/hept_scoping.ml | 6 +++--- compiler/heptagon/transformations/switch.ml | 2 +- compiler/main/hept2mls.ml | 7 ++----- 8 files changed, 16 insertions(+), 19 deletions(-) diff --git a/compiler/heptagon/analysis/causality.ml b/compiler/heptagon/analysis/causality.ml index b9b3107..cc6bb8b 100644 --- a/compiler/heptagon/analysis/causality.ml +++ b/compiler/heptagon/analysis/causality.ml @@ -108,9 +108,9 @@ let rec typing e = candlist l | Eiterator (_, _, _, pe_list, e_list, _) -> ctuplelist (List.map typing (pe_list@e_list)) - | Ewhen (e, c, ce) -> + | Ewhen (e, c, x) -> let t = typing e in - let tc = typing ce in + let tc = read x in cseq tc t | Emerge (x, c_e_list) -> let t = read x in diff --git a/compiler/heptagon/analysis/initialization.ml b/compiler/heptagon/analysis/initialization.ml index 8b44845..afc9bd8 100644 --- a/compiler/heptagon/analysis/initialization.ml +++ b/compiler/heptagon/analysis/initialization.ml @@ -250,8 +250,8 @@ let rec typing h e = List.iter (fun e -> initialized_exp h e) pe_list; List.iter (fun e -> initialized_exp h e) e_list; skeleton izero e.e_ty - | Ewhen (e, _, ce) -> - let i = imax (itype (typing h ce)) (itype (typing h e)) in + | Ewhen (e, _, x) -> + let i = imax (IEnv.find_var x h) (itype (typing h e)) in skeleton i e.e_ty | Emerge (x, c_e_list) -> let i = diff --git a/compiler/heptagon/analysis/typing.ml b/compiler/heptagon/analysis/typing.ml index b5103af..a1c4da2 100644 --- a/compiler/heptagon/analysis/typing.ml +++ b/compiler/heptagon/analysis/typing.ml @@ -555,12 +555,12 @@ let rec typing const_env h e = , typed_n, typed_pe_list, typed_e_list, reset), ty | Eiterator _ -> assert false - | Ewhen (e, c, ce) -> + | Ewhen (e, c, x) -> let typed_e, t = typing const_env h e in let tn_expected = find_constrs c in - let typed_ce, tn_actual = typing const_env h ce in + let tn_actual = typ_of_name h x in unify tn_actual tn_expected; - Ewhen (typed_e, c, typed_ce), t + Ewhen (typed_e, c, x), t | Emerge (x, (c1,e1)::c_e_list) -> (* verify the constructors : they should be unique, diff --git a/compiler/heptagon/hept_printer.ml b/compiler/heptagon/hept_printer.ml index e9f84dd..61e6be7 100644 --- a/compiler/heptagon/hept_printer.ml +++ b/compiler/heptagon/hept_printer.ml @@ -116,9 +116,9 @@ and print_exp_desc ff = function print_exp_tuple pargs print_exp_tuple args print_every reset - | Ewhen (e, c, ec) -> + | Ewhen (e, c, x) -> fprintf ff "@[<2>(%a@ when %a(%a))@]" - print_exp e print_qualname c print_exp ec + print_exp e print_qualname c print_ident x | Emerge (x, tag_e_list) -> fprintf ff "@[<2>merge %a@ %a@]" print_ident x print_tag_e_list tag_e_list diff --git a/compiler/heptagon/heptagon.ml b/compiler/heptagon/heptagon.ml index 123d635..663ed71 100644 --- a/compiler/heptagon/heptagon.ml +++ b/compiler/heptagon/heptagon.ml @@ -41,7 +41,7 @@ and desc = | Epre of static_exp option * exp | Efby of exp * exp | Estruct of (field_name * exp) list - | Ewhen of exp * constructor_name * exp + | Ewhen of exp * constructor_name * var_ident (** exp when Constructor(ident) *) | Emerge of var_ident * (constructor_name * exp) list (** merge ident (Constructor -> exp)+ *) diff --git a/compiler/heptagon/parsing/hept_scoping.ml b/compiler/heptagon/parsing/hept_scoping.ml index 9a50dac..81cacc6 100644 --- a/compiler/heptagon/parsing/hept_scoping.ml +++ b/compiler/heptagon/parsing/hept_scoping.ml @@ -273,11 +273,11 @@ and translate_desc loc env = function let app = mk_app ~params:params (translate_op op) in Heptagon.Eiterator (translate_iterator_type it, app, n, pe_list, e_list, None) - | Ewhen (e, c, ce) -> + | Ewhen (e, c, x) -> + let x = Rename.var loc env x in let e = translate_exp env e in let c = qualify_constrs c in - let ce = translate_exp env (mk_exp (Evar ce) loc) in - Heptagon.Ewhen (e, c, ce) + Heptagon.Ewhen (e, c, x) | Emerge (x, c_e_list) -> let x = Rename.var loc env x in let c_e_list = diff --git a/compiler/heptagon/transformations/switch.ml b/compiler/heptagon/transformations/switch.ml index 707e7b3..a98480b 100644 --- a/compiler/heptagon/transformations/switch.ml +++ b/compiler/heptagon/transformations/switch.ml @@ -90,7 +90,7 @@ let rec sample_var e env = match env with then e (* the var is declared at this level, nothing to do *) else (*sample to lower level*) {e with e_desc = - Ewhen ((sample_var e env_d), constr, {e with e_desc = Evar ck})} + Ewhen ((sample_var e env_d), constr, ck)} | _ -> (Format.eprintf "'sample_var' called on full exp : %a@." Hept_printer.print_exp e; diff --git a/compiler/main/hept2mls.ml b/compiler/main/hept2mls.ml index ed384a3..984291a 100644 --- a/compiler/main/hept2mls.ml +++ b/compiler/main/hept2mls.ml @@ -94,11 +94,8 @@ let rec translate_extvalue e = match e.Heptagon.e_desc with | Heptagon.Econst c -> mk_extvalue (Wconst c) | Heptagon.Evar x -> mk_extvalue (Wvar x) - | Heptagon.Ewhen (e, c, ce) -> - (match ce.Heptagon.e_desc with - | Heptagon.Evar x -> - mk_extvalue (Wwhen (translate_extvalue e, c, x)) - | _ -> Error.message e.Heptagon.e_loc Error.Enormalization) + | Heptagon.Ewhen (e, c, x) -> + mk_extvalue (Wwhen (translate_extvalue e, c, x)) | Heptagon.Eapp({ Heptagon.a_op = Heptagon.Efield; Heptagon.a_params = params }, e_list, reset) -> let e = assert_1 e_list in