jeltz/heptagon
1
0
Fork 0
Code Issues Pull requests Releases Activity

Use idents for Emerge in Heptagon

Browse source
This commit is contained in:
Cédric Pasteur 2011-04-29 14:26:07 +02:00 committed by Cédric Pasteur
parent 670d8962df
commit aae38a7844
9 changed files with 18 additions and 26 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
compiler/heptagon/analysis/causality.ml
View file

@ -112,8 +112,8 @@ let rec typing e =
let t = typing e in
let tc = typing ce in
cseq tc t
| Emerge (e, c_e_list) ->
let t = typing e in
| Emerge (x, c_e_list) ->
let t = read x in
let tl = List.map (fun (_,e) -> typing e) c_e_list in
cseq t (candlist tl)

4
compiler/heptagon/analysis/initialization.ml
View file

@ -253,11 +253,11 @@ let rec typing h e =
| Ewhen (e, _, ce) ->
let i = imax (itype (typing h ce)) (itype (typing h e)) in
skeleton i e.e_ty
| Emerge (e, c_e_list) ->
| Emerge (x, 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 (typing h e)) i in
let i = imax (IEnv.find_var x h) i in
skeleton i e.e_ty

9
compiler/heptagon/analysis/typing.ml
View file

@ -562,7 +562,7 @@ let rec typing const_env h e =
unify tn_actual tn_expected;
Ewhen (typed_e, c, typed_ce), t
| Emerge (e, (c1,e1)::c_e_list) ->
| Emerge (x, (c1,e1)::c_e_list) ->
(* verify the constructors : they should be unique,
all of the same type and cover all the possibilities *)
let c_type = find_constrs c1 in
@ -586,14 +586,13 @@ let rec typing const_env h e =
let c_set_diff = QualSet.diff expected_c_set c_set in
if not (QualSet.is_empty c_set_diff)
then message e.e_loc (Emerge_missing_constrs c_set_diff);
(* verify [n] is of the right type *)
let typed_e, e_type = typing const_env h e in
unify e_type c_type;
(* verify [x] is of the right type *)
unify (typ_of_name h x) c_type;
(* type *)
let typed_e1, t = typing const_env h e1 in
let typed_c_e_list =
List.map (fun (c, e) -> (c, expect const_env h t e)) c_e_list in
Emerge (typed_e, (c1,typed_e1)::typed_c_e_list), t
Emerge (x, (c1,typed_e1)::typed_c_e_list), t
| Emerge (_, []) -> assert false
in
{ e with e_desc = typed_desc; e_ty = ty; }, ty

4
compiler/heptagon/hept_printer.ml
View file

@ -119,9 +119,9 @@ and print_exp_desc ff = function
| Ewhen (e, c, ec) ->
fprintf ff "@[<2>(%a@ when %a(%a))@]"
print_exp e print_qualname c print_exp ec
| Emerge (e, tag_e_list) ->
| Emerge (x, tag_e_list) ->
fprintf ff "@[<2>merge %a@ %a@]"
print_exp e print_tag_e_list tag_e_list
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

4
compiler/heptagon/heptagon.ml
View file

@ -43,7 +43,7 @@ and desc =
| Estruct of (field_name * exp) list
| Ewhen of exp * constructor_name * exp
(** exp when Constructor(ident) *)
| Emerge of exp * (constructor_name * exp) list
| 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
@ -266,4 +266,4 @@ let vars_pat pat =
let rec vd_mem n = function
| [] -> false
| vd::l -> vd.v_ident = n or (vd_mem n l)
*)
*)

6
compiler/heptagon/parsing/hept_scoping.ml
View file

@ -278,15 +278,15 @@ and translate_desc loc env = function
let c = qualify_constrs c in
let ce = translate_exp env (mk_exp (Evar ce) loc) in
Heptagon.Ewhen (e, c, ce)
| Emerge (e, c_e_list) ->
let e = translate_exp env (mk_exp (Evar e) loc) in
| Emerge (x, c_e_list) ->
let x = Rename.var loc env x in
let c_e_list =
let fun_c_e (c, e) =
let e = translate_exp env e in
let c = qualify_constrs c in
(c, e) in
List.map fun_c_e c_e_list in
Heptagon.Emerge (e, c_e_list)
Heptagon.Emerge (x, c_e_list)
and translate_op = function

1
compiler/heptagon/transformations/normalize.ml
View file

@ -222,7 +222,6 @@ and merge context e x c_e_list =
let t_e_list = List.map2 (fun t e -> (t,e)) c_list e_list in
mk_exp ~loc:e.e_loc (Emerge(x, t_e_list)) ty
in
let context, x = translate ExtValue context x in
let c_e_list, context = mapfold translate_tag context c_e_list in
match c_e_list with
| [] -> assert false

3
compiler/heptagon/transformations/switch.ml
View file

@ -170,7 +170,6 @@ let eqdesc funs (env,h) eqd = match eqd with
(* create a clock var corresponding to the switch condition [e] *)
let ck = fresh_clock_id () in
let e, (env,h) = exp_it funs (env,h) e in
let ck_e = { e with e_desc = Evar ck } in
let locals = [mk_var_dec ck e.e_ty] in
let equs = [mk_equation (Eeq (Evarpat ck, e))] in
@ -200,7 +199,7 @@ let eqdesc funs (env,h) eqd = match eqd with
let c_h_to_c_e (constr,h) =
constr, mk_exp (Evar (Rename.rename n h)) ty in
let c_e_l = List.map c_h_to_c_e c_h_l in
let merge = mk_exp (Emerge (ck_e, c_e_l)) ty in
let merge = mk_exp (Emerge (ck, c_e_l)) ty in
(mk_equation (Eeq (Evarpat n, merge))) :: equs in
let equs =
Idents.Env.fold (fun n _ equs -> new_merge n equs) defnames equs in

9
compiler/main/hept2mls.ml
View file

@ -144,13 +144,8 @@ let translate
| Heptagon.Efby _
| Heptagon.Elast _ ->
Error.message loc Error.Eunsupported_language_construct
| Heptagon.Emerge (e, c_e_list) ->
(match e.Heptagon.e_desc with
| Heptagon.Evar x ->
mk_exp ty
(Emerge (x, List.map (fun (c,e)->c,
translate_extvalue e) c_e_list))
| _ -> Error.message loc Error.Enormalization)
| Heptagon.Emerge (x, c_e_list) ->
mk_exp ty (Emerge (x, List.map (fun (c,e)-> c, translate_extvalue e) c_e_list))
let rec translate_pat = function
| Heptagon.Evarpat(n) -> Evarpat n