Revision 14ebde97
Added by Xavier Thirioux about 9 years ago
src/normalization.ml | ||
---|---|---|
30 | 30 |
(* open Clocks *) |
31 | 31 |
open Format |
32 | 32 |
|
33 |
let expr_true loc ck = |
|
34 |
{ expr_tag = Utils.new_tag (); |
|
35 |
expr_desc = Expr_const (Const_tag tag_true); |
|
36 |
expr_type = Type_predef.type_bool; |
|
37 |
expr_clock = ck; |
|
38 |
expr_delay = Delay.new_var (); |
|
39 |
expr_annot = None; |
|
40 |
expr_loc = loc } |
|
41 |
|
|
42 |
let expr_false loc ck = |
|
43 |
{ expr_tag = Utils.new_tag (); |
|
44 |
expr_desc = Expr_const (Const_tag tag_false); |
|
45 |
expr_type = Type_predef.type_bool; |
|
46 |
expr_clock = ck; |
|
47 |
expr_delay = Delay.new_var (); |
|
48 |
expr_annot = None; |
|
49 |
expr_loc = loc } |
|
50 |
|
|
51 |
let expr_once loc ck = |
|
52 |
{ expr_tag = Utils.new_tag (); |
|
53 |
expr_desc = Expr_arrow (expr_true loc ck, expr_false loc ck); |
|
54 |
expr_type = Type_predef.type_bool; |
|
55 |
expr_clock = ck; |
|
56 |
expr_delay = Delay.new_var (); |
|
57 |
expr_annot = None; |
|
58 |
expr_loc = loc } |
|
59 |
|
|
60 |
let is_expr_once = |
|
61 |
let dummy_expr_once = expr_once Location.dummy_loc (Clocks.new_var true) in |
|
62 |
fun expr -> Corelang.is_eq_expr expr dummy_expr_once |
|
63 |
|
|
64 |
let unfold_arrow expr = |
|
65 |
match expr.expr_desc with |
|
66 |
| Expr_arrow (e1, e2) -> |
|
67 |
let loc = expr.expr_loc in |
|
68 |
let ck = expr.expr_clock in |
|
69 |
{ expr with expr_desc = Expr_ite (expr_once loc ck, e1, e2) } |
|
70 |
| _ -> assert false |
|
71 |
|
|
33 | 72 |
let cpt_fresh = ref 0 |
34 | 73 |
|
35 | 74 |
(* Generate a new local [node] variable *) |
... | ... | |
166 | 205 |
normalize_expr ~alias:alias node offsets defvars norm_expr |
167 | 206 |
else |
168 | 207 |
mk_expr_alias_opt (alias && not (Basic_library.is_internal_fun id)) node defvars norm_expr |
169 |
| Expr_arrow (e1,e2) -> (* Here we differ from Colaco paper: arrows are pushed to the top *) |
|
208 |
| Expr_arrow (e1,e2) when not (is_expr_once expr) -> (* Here we differ from Colaco paper: arrows are pushed to the top *) |
|
209 |
normalize_expr ~alias:alias node offsets defvars (unfold_arrow expr) |
|
210 |
| Expr_arrow (e1,e2) -> |
|
170 | 211 |
let defvars, norm_e1 = normalize_expr node offsets defvars e1 in |
171 | 212 |
let defvars, norm_e2 = normalize_expr node offsets defvars e2 in |
172 | 213 |
let norm_expr = mk_norm_expr offsets expr (Expr_arrow (norm_e1, norm_e2)) in |
Also available in: Unified diff
improved code generation by factorizing out arrows