Revision 01c7d5e1 src/lustreSpec.ml
src/lustreSpec.ml | ||
---|---|---|
1 | 1 |
open Format |
2 | 2 |
|
3 |
|
|
4 |
let merge_expr_annot ann1 ann2 = |
|
5 |
match ann1, ann2 with |
|
6 |
| None, None -> assert false |
|
7 |
| Some _, None -> ann1 |
|
8 |
| None, Some _ -> ann2 |
|
9 |
| Some ann1, Some ann2 -> Some (ann1@ann2) |
|
10 |
|
|
11 |
|
|
12 | 3 |
type ident = Utils.ident |
4 |
type label = Utils.ident |
|
13 | 5 |
type rat = Utils.rat |
14 | 6 |
type tag = Utils.tag |
15 | 7 |
|
16 |
type constant = |
|
17 |
| EConst_int of int |
|
18 |
| EConst_real of string |
|
19 |
| EConst_float of float |
|
20 |
| EConst_bool of bool |
|
21 |
| EConst_string of string |
|
22 |
|
|
23 | 8 |
type type_dec = |
24 | 9 |
{ty_dec_desc: type_dec_desc; |
25 | 10 |
ty_dec_loc: Location.t} |
... | ... | |
54 | 39 |
mutable var_clock: Clocks.clock_expr; |
55 | 40 |
var_loc: Location.t} |
56 | 41 |
|
42 |
(** The core language and its ast. Every element of the ast contains its |
|
43 |
location in the program text. The type and clock of an ast element |
|
44 |
is mutable (and initialized to dummy values). This avoids to have to |
|
45 |
duplicate ast structures (e.g. ast, typed_ast, clocked_ast). *) |
|
46 |
|
|
47 |
|
|
48 |
type constant = |
|
49 |
| Const_int of int |
|
50 |
| Const_real of string |
|
51 |
| Const_float of float |
|
52 |
| Const_array of constant list |
|
53 |
| Const_tag of label |
|
54 |
| Const_string of string (* used only for annotations *) |
|
55 |
| Const_struct of (label * constant) list |
|
56 |
|
|
57 |
type quantifier_type = Exists | Forall |
|
58 |
|
|
59 |
|
|
60 |
|
|
57 | 61 |
(* The tag of an expression is a unique identifier used to distinguish |
58 | 62 |
different instances of the same node *) |
59 |
type eexpr = |
|
63 |
type expr = |
|
64 |
{expr_tag: tag; |
|
65 |
expr_desc: expr_desc; |
|
66 |
mutable expr_type: Types.type_expr; |
|
67 |
mutable expr_clock: Clocks.clock_expr; |
|
68 |
mutable expr_delay: Delay.delay_expr; |
|
69 |
mutable expr_annot: expr_annot option; |
|
70 |
expr_loc: Location.t} |
|
71 |
|
|
72 |
and expr_desc = |
|
73 |
| Expr_const of constant |
|
74 |
| Expr_ident of ident |
|
75 |
| Expr_tuple of expr list |
|
76 |
| Expr_ite of expr * expr * expr |
|
77 |
| Expr_arrow of expr * expr |
|
78 |
| Expr_fby of expr * expr |
|
79 |
| Expr_array of expr list |
|
80 |
| Expr_access of expr * Dimension.dim_expr |
|
81 |
| Expr_power of expr * Dimension.dim_expr |
|
82 |
| Expr_pre of expr |
|
83 |
| Expr_when of expr * ident * label |
|
84 |
| Expr_merge of ident * (label * expr) list |
|
85 |
| Expr_appl of call_t |
|
86 |
and call_t = ident * expr * (ident * label) option |
|
87 |
(* The third part denotes the reseting clock label and value *) |
|
88 |
and |
|
89 |
(* The tag of an expression is a unique identifier used to distinguish |
|
90 |
different instances of the same node *) |
|
91 |
eexpr = |
|
60 | 92 |
{eexpr_tag: tag; |
61 |
eexpr_desc: eexpr_desc; |
|
93 |
eexpr_qfexpr: expr; |
|
94 |
eexpr_quantifiers: (quantifier_type * var_decl list) list; |
|
62 | 95 |
mutable eexpr_type: Types.type_expr; |
63 | 96 |
mutable eexpr_clock: Clocks.clock_expr; |
97 |
mutable eexpr_normalized: (var_decl * eq list * var_decl list) option; |
|
64 | 98 |
eexpr_loc: Location.t} |
65 | 99 |
|
66 |
and eexpr_desc = |
|
67 |
| EExpr_const of constant |
|
68 |
| EExpr_ident of ident |
|
69 |
| EExpr_tuple of eexpr list |
|
70 |
| EExpr_arrow of eexpr * eexpr |
|
71 |
| EExpr_fby of eexpr * eexpr |
|
72 |
(* | EExpr_concat of eexpr * eexpr *) |
|
73 |
(* | EExpr_tail of eexpr *) |
|
74 |
| EExpr_pre of eexpr |
|
75 |
| EExpr_when of eexpr * ident |
|
76 |
(* | EExpr_whennot of eexpr * ident *) |
|
77 |
| EExpr_merge of ident * eexpr * eexpr |
|
78 |
| EExpr_appl of ident * eexpr * ident option |
|
79 |
(* | EExpr_uclock of eexpr * int *) |
|
80 |
(* | EExpr_dclock of eexpr * int *) |
|
81 |
(* | EExpr_phclock of eexpr * rat *) |
|
82 |
| EExpr_exists of var_decl list * eexpr |
|
83 |
| EExpr_forall of var_decl list * eexpr |
|
84 |
|
|
85 |
type ensures_t = EnsuresExpr of eexpr | SpecObserverNode of (string * eexpr list) |
|
100 |
and expr_annot = { |
|
101 |
annots: (string list * eexpr) list; |
|
102 |
annot_loc: Location.t |
|
103 |
} |
|
104 |
and |
|
105 |
eq = |
|
106 |
{eq_lhs: ident list; |
|
107 |
eq_rhs: expr; |
|
108 |
eq_loc: Location.t} |
|
109 |
|
|
86 | 110 |
|
87 | 111 |
type node_annot = { |
88 | 112 |
requires: eexpr list; |
89 |
ensures: ensures_t list; |
|
90 |
behaviors: (string * eexpr list * ensures_t list) list |
|
113 |
ensures: eexpr list; |
|
114 |
behaviors: (string * eexpr list * eexpr list * Location.t) list; |
|
115 |
spec_loc: Location.t; |
|
91 | 116 |
} |
117 |
type assert_t = |
|
118 |
{ |
|
119 |
assert_expr: expr; |
|
120 |
assert_loc: Location.t |
|
121 |
} |
|
122 |
|
|
123 |
type node_desc = |
|
124 |
{node_id: ident; |
|
125 |
mutable node_type: Types.type_expr; |
|
126 |
mutable node_clock: Clocks.clock_expr; |
|
127 |
node_inputs: var_decl list; |
|
128 |
node_outputs: var_decl list; |
|
129 |
node_locals: var_decl list; |
|
130 |
mutable node_gencalls: expr list; |
|
131 |
mutable node_checks: Dimension.dim_expr list; |
|
132 |
node_asserts: assert_t list; |
|
133 |
node_eqs: eq list; |
|
134 |
mutable node_dec_stateless: bool; |
|
135 |
mutable node_stateless: bool option; |
|
136 |
node_spec: node_annot option; |
|
137 |
node_annot: expr_annot list; |
|
138 |
} |
|
139 |
|
|
140 |
type imported_node_desc = |
|
141 |
{nodei_id: ident; |
|
142 |
mutable nodei_type: Types.type_expr; |
|
143 |
mutable nodei_clock: Clocks.clock_expr; |
|
144 |
nodei_inputs: var_decl list; |
|
145 |
nodei_outputs: var_decl list; |
|
146 |
nodei_stateless: bool; |
|
147 |
nodei_spec: node_annot option; |
|
148 |
nodei_prototype: string option; |
|
149 |
nodei_in_lib: string option; |
|
150 |
} |
|
151 |
|
|
152 |
type const_desc = |
|
153 |
{const_id: ident; |
|
154 |
const_loc: Location.t; |
|
155 |
const_value: constant; |
|
156 |
mutable const_type: Types.type_expr; |
|
157 |
} |
|
158 |
|
|
159 |
type top_decl_desc = |
|
160 |
| Node of node_desc |
|
161 |
| Consts of const_desc list |
|
162 |
| ImportedNode of imported_node_desc |
|
163 |
| Open of bool * string (* the boolean set to true denotes a local |
|
164 |
lusi vs a lusi installed at system level *) |
|
165 |
|
|
166 |
type top_decl = |
|
167 |
{top_decl_desc: top_decl_desc; |
|
168 |
top_decl_loc: Location.t} |
|
169 |
|
|
170 |
type program = top_decl list |
|
171 |
|
|
172 |
type error = |
|
173 |
Main_not_found |
|
174 |
| Main_wrong_kind |
|
175 |
| No_main_specified |
|
176 |
| Unbound_symbol of ident |
|
177 |
| Already_bound_symbol of ident |
|
92 | 178 |
|
93 | 179 |
|
94 |
type expr_annot = (string list * eexpr) list |
|
95 |
|
|
96 |
let merge_node_annot ann1 ann2 = |
|
97 |
{ requires = ann1.requires @ ann2.requires; |
|
98 |
ensures = ann1.ensures @ ann2.ensures; |
|
99 |
behaviors = ann1.behaviors @ ann2.behaviors; |
|
100 |
} |
|
101 |
|
|
102 |
let mkeexpr loc d = |
|
103 |
{ eexpr_tag = Utils.new_tag (); |
|
104 |
eexpr_desc = d; |
|
105 |
eexpr_type = Types.new_var (); |
|
106 |
eexpr_clock = Clocks.new_var true; |
|
107 |
eexpr_loc = loc } |
|
108 |
|
|
109 |
let mkepredef_call loc funname args = |
|
110 |
mkeexpr loc (EExpr_appl (funname, mkeexpr loc (EExpr_tuple args), None)) |
|
111 |
|
|
112 |
let mkepredef_unary_call loc funname arg = |
|
113 |
mkeexpr loc (EExpr_appl (funname, arg, None)) |
|
114 | 180 |
|
115 | 181 |
(* Local Variables: *) |
116 | 182 |
(* compile-command:"make -C .." *) |
Also available in: Unified diff