Revision 04396cc7
Added by Christophe Garion almost 7 years ago
src/lustreSpec.ml  

43  43  
44  44 
and clock_dec_desc = 
45  45 
 Ckdec_any 
46 
 Ckdec_bool of (ident * ident) list


46 
 Ckdec_bool of (ident * ident) list 

47  47  
48  48  
49  49 
type constant = 
50 
 Const_bool of bool 

50  51 
 Const_int of int 
51  52 
 Const_real of Num.num * int * string (* (a, b, c) means a * 10^b. c is the original string *) 
52  53 
 Const_array of constant list 
...  ...  
56  57  
57  58 
type quantifier_type = Exists  Forall 
58  59  
59 
type var_decl =


60 
type var_decl = 

60  61 
{var_id: ident; 
61  62 
var_orig:bool; 
62  63 
var_dec_type: type_dec; 
...  ...  
100  101 
 Expr_merge of ident * (label * expr) list 
101  102 
 Expr_appl of call_t 
102  103  
103 
and call_t = ident * expr * expr option


104 
and call_t = ident * expr * expr option 

104  105 
(* The third part denotes the boolean condition for resetting *) 
105  106  
106  107 
and eq = 
...  ...  
134  135 
 Index of Dimension.dim_expr 
135  136 
 Field of label 
136  137  
137 
type assert_t =


138 
type assert_t = 

138  139 
{ 
139  140 
assert_expr: expr; 
140  141 
assert_loc: Location.t; 
...  ...  
168  169 
node_locals: var_decl list; 
169  170 
mutable node_gencalls: expr list; 
170  171 
mutable node_checks: Dimension.dim_expr list; 
171 
node_asserts: assert_t list;


172 
node_asserts: assert_t list; 

172  173 
node_stmts: statement list; 
173  174 
mutable node_dec_stateless: bool; 
174  175 
mutable node_stateless: bool option; 
...  ...  
188  189 
nodei_in_lib: string list; 
189  190 
} 
190  191  
191 
type const_desc =


192 
{const_id: ident;


193 
const_loc: Location.t;


194 
const_value: constant;


192 
type const_desc = 

193 
{const_id: ident; 

194 
const_loc: Location.t; 

195 
const_value: constant; 

195  196 
mutable const_type: Types.type_expr; 
196  197 
} 
197  198  
...  ...  
199  200 
 Node of node_desc 
200  201 
 Const of const_desc 
201  202 
 ImportedNode of imported_node_desc 
202 
 Open of bool * string (* the boolean set to true denotes a local


203 
 Open of bool * string (* the boolean set to true denotes a local 

203  204 
lusi vs a lusi installed at system level *) 
204  205 
 TypeDef of typedef_desc 
205  206  
...  ...  
211  212  
212  213 
type program = top_decl list 
213  214  
214 
type dep_t = Dep of


215 
bool


215 
type dep_t = Dep of 

216 
bool 

216  217 
* ident 
217 
* (top_decl list)


218 
* (top_decl list) 

218  219 
* bool (* is stateful *) 
219  220  
220  221  
221  222 
(************ Machine code types *************) 
222  223  
223 
type value_t =


224 
type value_t = 

224  225 
{ 
225  226 
value_desc: value_t_desc; 
226  227 
value_type: Types.type_expr; 
...  ...  
230  231 
 Cst of constant 
231  232 
 LocalVar of var_decl 
232  233 
 StateVar of var_decl 
233 
 Fun of ident * value_t list


234 
 Fun of ident * value_t list 

234  235 
 Array of value_t list 
235  236 
 Access of value_t * value_t 
236  237 
 Power of value_t * value_t 
Also available in: Unified diff
parserjson: add variables in parsing