Also use idents for Ewhen in Heptagon
This commit is contained in:
parent
aae38a7844
commit
59c8106e46
8 changed files with 16 additions and 19 deletions
|
@ -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
|
||||
|
|
|
@ -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 =
|
||||
|
|
|
@ -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,
|
||||
|
|
|
@ -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
|
||||
|
|
|
@ -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)+ *)
|
||||
|
|
|
@ -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 =
|
||||
|
|
|
@ -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;
|
||||
|
|
|
@ -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
|
||||
|
|
Loading…
Reference in a new issue