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

Fixed clocking annotations. 

1. Transmit annotations to extvaluese in Hept2mls.

2. Handle a pre-existing w_ck when clocking extvalues.
This commit is contained in:
Adrien Guatto 2011-11-10 15:36:54 +01:00
parent 0222d11b2d
commit 1a9dc17618
2 changed files with 9 additions and 2 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

4
compiler/main/hept2mls.ml
View File

@ -90,7 +90,9 @@ let translate_app app =
let rec translate_extvalue e = let rec translate_extvalue e =
let mk_extvalue = let mk_extvalue =
mk_extvalue ~loc:e.Heptagon.e_loc ~linearity:e.Heptagon.e_linearity ~ty:e.Heptagon.e_ty mk_extvalue
~loc:e.Heptagon.e_loc ~linearity:e.Heptagon.e_linearity ~ty:e.Heptagon.e_ty
~clock:(match e.Heptagon.e_ct_annot with None -> fresh_clock () | Some ct -> assert_1 (unprod ct))
in in
match e.Heptagon.e_desc with match e.Heptagon.e_desc with
| Heptagon.Econst c -> mk_extvalue (Wconst c) | Heptagon.Econst c -> mk_extvalue (Wconst c)

7
compiler/minils/analysis/clocking.ml
View File

@ -73,6 +73,11 @@ let rec typing_extvalue h w =
unify_ck t1 t2; unify_ck t1 t2;
t1 t1
in in
(try unify_ck ck w.w_ck
with Unify ->
eprintf "Incoherent clock annotation for extvalue %a.@\n"
Mls_printer.print_extvalue w;
error_message w.w_loc (Etypeclash (Ck ck, Ck w.w_ck)));
w.w_ck <- ck; w.w_ck <- ck;
ck ck
@ -187,7 +192,7 @@ let typing_eq h { eq_lhs = pat; eq_rhs = e; eq_loc = loc } =
e.e_base_ck <- base; e.e_base_ck <- base;
(try unify ct e.e_ct (try unify ct e.e_ct
with Unify -> with Unify ->
eprintf "Incoherent clock annotation for exp %a.@\n" eprintf "Inconsistent clock annotation for exp %a.@\n"
Mls_printer.print_exp e; Mls_printer.print_exp e;
error_message e.e_loc (Etypeclash (ct,e.e_ct))); error_message e.e_loc (Etypeclash (ct,e.e_ct)));
e.e_ct <- ct; e.e_ct <- ct;