Revision 04396cc7
Added by Christophe Garion over 4 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
parser-json: add variables in parsing