1
|
(********************************************************************)
|
2
|
(* *)
|
3
|
(* The LustreC compiler toolset / The LustreC Development Team *)
|
4
|
(* Copyright 2012 - -- ONERA - CNRS - INPT *)
|
5
|
(* *)
|
6
|
(* LustreC is free software, distributed WITHOUT ANY WARRANTY *)
|
7
|
(* under the terms of the GNU Lesser General Public License *)
|
8
|
(* version 2.1. *)
|
9
|
(* *)
|
10
|
(********************************************************************)
|
11
|
|
12
|
open Utils
|
13
|
open LustreSpec
|
14
|
open Corelang
|
15
|
open Format
|
16
|
|
17
|
|
18
|
let expr_true loc ck =
|
19
|
{ expr_tag = Utils.new_tag ();
|
20
|
expr_desc = Expr_const (Const_tag tag_true);
|
21
|
expr_type = Type_predef.type_bool;
|
22
|
expr_clock = ck;
|
23
|
expr_delay = Delay.new_var ();
|
24
|
expr_annot = None;
|
25
|
expr_loc = loc }
|
26
|
|
27
|
let expr_false loc ck =
|
28
|
{ expr_tag = Utils.new_tag ();
|
29
|
expr_desc = Expr_const (Const_tag tag_false);
|
30
|
expr_type = Type_predef.type_bool;
|
31
|
expr_clock = ck;
|
32
|
expr_delay = Delay.new_var ();
|
33
|
expr_annot = None;
|
34
|
expr_loc = loc }
|
35
|
|
36
|
let expr_once loc ck =
|
37
|
{ expr_tag = Utils.new_tag ();
|
38
|
expr_desc = Expr_arrow (expr_true loc ck, expr_false loc ck);
|
39
|
expr_type = Type_predef.type_bool;
|
40
|
expr_clock = ck;
|
41
|
expr_delay = Delay.new_var ();
|
42
|
expr_annot = None;
|
43
|
expr_loc = loc }
|
44
|
|
45
|
let is_expr_once =
|
46
|
let dummy_expr_once = expr_once Location.dummy_loc (Clocks.new_var true) in
|
47
|
fun expr -> Corelang.is_eq_expr expr dummy_expr_once
|
48
|
|
49
|
let unfold_arrow expr =
|
50
|
match expr.expr_desc with
|
51
|
| Expr_arrow (e1, e2) ->
|
52
|
let loc = expr.expr_loc in
|
53
|
let ck = List.hd (Clocks.clock_list_of_clock expr.expr_clock) in
|
54
|
{ expr with expr_desc = Expr_ite (expr_once loc ck, e1, e2) }
|
55
|
| _ -> assert false
|
56
|
|
57
|
let unfold_arrow_active = ref true
|
58
|
let cpt_fresh = ref 0
|
59
|
|
60
|
(* Generate a new local [node] variable *)
|
61
|
let mk_fresh_var node loc ty ck =
|
62
|
let vars = get_node_vars node in
|
63
|
let rec aux () =
|
64
|
incr cpt_fresh;
|
65
|
let s = Printf.sprintf "__%s_%d" node.node_id !cpt_fresh in
|
66
|
if List.exists (fun v -> v.var_id = s) vars then aux () else
|
67
|
{
|
68
|
var_id = s;
|
69
|
var_orig = false;
|
70
|
var_dec_type = dummy_type_dec;
|
71
|
var_dec_clock = dummy_clock_dec;
|
72
|
var_dec_const = false;
|
73
|
var_dec_value = None;
|
74
|
var_type = ty;
|
75
|
var_clock = ck;
|
76
|
var_loc = loc
|
77
|
}
|
78
|
in aux ()
|
79
|
|
80
|
(* Get the equation in [defs] with [expr] as rhs, if any *)
|
81
|
let get_expr_alias defs expr =
|
82
|
try Some (List.find (fun eq -> is_eq_expr eq.eq_rhs expr) defs)
|
83
|
with
|
84
|
| Not_found -> None
|
85
|
|
86
|
(* Replace [expr] with (tuple of) [locals] *)
|
87
|
let replace_expr locals expr =
|
88
|
match locals with
|
89
|
| [] -> assert false
|
90
|
| [v] -> { expr with
|
91
|
expr_tag = Utils.new_tag ();
|
92
|
expr_desc = Expr_ident v.var_id }
|
93
|
| _ -> { expr with
|
94
|
expr_tag = Utils.new_tag ();
|
95
|
expr_desc = Expr_tuple (List.map expr_of_vdecl locals) }
|
96
|
|
97
|
let unfold_offsets e offsets =
|
98
|
let add_offset e d =
|
99
|
(*Format.eprintf "add_offset %a(%a) %a @." Printers.pp_expr e Types.print_ty e.expr_type Dimension.pp_dimension d;
|
100
|
let res = *)
|
101
|
{ e with
|
102
|
expr_tag = Utils.new_tag ();
|
103
|
expr_loc = d.Dimension.dim_loc;
|
104
|
expr_type = Types.array_element_type e.expr_type;
|
105
|
expr_desc = Expr_access (e, d) }
|
106
|
(*in (Format.eprintf "= %a @." Printers.pp_expr res; res) *)
|
107
|
in
|
108
|
List.fold_left add_offset e offsets
|
109
|
|
110
|
(* Create an alias for [expr], if none exists yet *)
|
111
|
let mk_expr_alias node (defs, vars) expr =
|
112
|
(*Format.eprintf "mk_expr_alias %a %a %a@." Printers.pp_expr expr Types.print_ty expr.expr_type Clocks.print_ck expr.expr_clock;*)
|
113
|
match get_expr_alias defs expr with
|
114
|
| Some eq ->
|
115
|
let aliases = List.map (fun id -> List.find (fun v -> v.var_id = id) vars) eq.eq_lhs in
|
116
|
(defs, vars), replace_expr aliases expr
|
117
|
| None ->
|
118
|
let new_aliases =
|
119
|
List.map2
|
120
|
(mk_fresh_var node expr.expr_loc)
|
121
|
(Types.type_list_of_type expr.expr_type)
|
122
|
(Clocks.clock_list_of_clock expr.expr_clock) in
|
123
|
let new_def =
|
124
|
mkeq expr.expr_loc (List.map (fun v -> v.var_id) new_aliases, expr)
|
125
|
in
|
126
|
(* Format.eprintf "Checking def of alias: %a -> %a@." (fprintf_list ~sep:", " (fun fmt v -> Format.pp_print_string fmt v.var_id)) new_aliases Printers.pp_expr expr; *)
|
127
|
(new_def::defs, new_aliases@vars), replace_expr new_aliases expr
|
128
|
|
129
|
(* Create an alias for [expr], if [expr] is not already an alias (i.e. an ident)
|
130
|
and [opt] is true *)
|
131
|
let mk_expr_alias_opt opt node (defs, vars) expr =
|
132
|
(*Format.eprintf "mk_expr_alias_opt %B %a %a %a@." opt Printers.pp_expr expr Types.print_ty expr.expr_type Clocks.print_ck expr.expr_clock;*)
|
133
|
match expr.expr_desc with
|
134
|
| Expr_ident alias ->
|
135
|
(defs, vars), expr
|
136
|
| _ ->
|
137
|
match get_expr_alias defs expr with
|
138
|
| Some eq ->
|
139
|
let aliases = List.map (fun id -> List.find (fun v -> v.var_id = id) vars) eq.eq_lhs in
|
140
|
(defs, vars), replace_expr aliases expr
|
141
|
| None ->
|
142
|
if opt
|
143
|
then
|
144
|
let new_aliases =
|
145
|
List.map2
|
146
|
(mk_fresh_var node expr.expr_loc)
|
147
|
(Types.type_list_of_type expr.expr_type)
|
148
|
(Clocks.clock_list_of_clock expr.expr_clock) in
|
149
|
let new_def =
|
150
|
mkeq expr.expr_loc (List.map (fun v -> v.var_id) new_aliases, expr)
|
151
|
in (new_def::defs, new_aliases@vars), replace_expr new_aliases expr
|
152
|
else
|
153
|
(defs, vars), expr
|