Project

General

Profile

« Previous | Next » 

Revision ca7ff3f7

Added by LĂ©lio Brun 7 months ago

reformatting

View differences:

src/lustre_types.ml
9 9
(*                                                                  *)
10 10
(********************************************************************)
11 11

  
12

  
13 12
type ident = Utils.ident
13

  
14 14
type rat = Utils.rat
15

  
15 16
type tag = Utils.tag
17

  
16 18
type label = Utils.ident
17 19

  
18
type type_dec =
19
    {ty_dec_desc: type_dec_desc;
20
     ty_dec_loc: Location.t}
20
type type_dec = { ty_dec_desc : type_dec_desc; ty_dec_loc : Location.t }
21 21

  
22 22
and type_dec_desc =
23 23
  | Tydec_any
......
31 31
  | Tydec_struct of (ident * type_dec_desc) list
32 32
  | Tydec_array of Dimension.dim_expr * type_dec_desc
33 33

  
34
type typedec_desc =
35
    {tydec_id: ident}
36

  
37
type typedef_desc =
38
    {tydef_id: ident;
39
     tydef_desc: type_dec_desc}
34
type typedec_desc = { tydec_id : ident }
40 35

  
41
type clock_dec =
42
    {ck_dec_desc: clock_dec_desc;
43
     ck_dec_loc: Location.t}
36
type typedef_desc = { tydef_id : ident; tydef_desc : type_dec_desc }
44 37

  
45
and clock_dec_desc =
46
  | Ckdec_any
47
  | Ckdec_bool of (ident * ident) list
38
type clock_dec = { ck_dec_desc : clock_dec_desc; ck_dec_loc : Location.t }
48 39

  
40
and clock_dec_desc = Ckdec_any | Ckdec_bool of (ident * ident) list
49 41

  
50 42
type constant =
51 43
  | Const_int of int
52 44
  | Const_real of Real.t
53 45
  | Const_array of constant list
54 46
  | Const_tag of label
55
  | Const_string of string (* used only for annotations *)
56
  | Const_modeid of string (* used only for annotations *)
47
  | Const_string of string
48
  (* used only for annotations *)
49
  | Const_modeid of string
50
  (* used only for annotations *)
57 51
  | Const_struct of (label * constant) list
58 52

  
59 53
type quantifier_type = Exists | Forall
60 54

  
61
type var_decl =
62
    {var_id: ident;
63
     var_orig:bool;
64
     var_dec_type: type_dec;
65
     var_dec_clock: clock_dec;
66
     var_dec_const: bool;
67
     var_dec_value: expr option;
68
     mutable var_parent_nodeid: ident option;
69
     mutable var_type: Types.type_expr;
70
     mutable var_clock: Clocks.clock_expr;
71
     var_loc: Location.t}
55
type var_decl = {
56
  var_id : ident;
57
  var_orig : bool;
58
  var_dec_type : type_dec;
59
  var_dec_clock : clock_dec;
60
  var_dec_const : bool;
61
  var_dec_value : expr option;
62
  mutable var_parent_nodeid : ident option;
63
  mutable var_type : Types.type_expr;
64
  mutable var_clock : Clocks.clock_expr;
65
  var_loc : Location.t;
66
}
67
(* The tag of an expression is a unique identifier used to distinguish different
68
   instances of the same node *)
72 69

  
73 70
(** The core language and its ast. Every element of the ast contains its
74
    location in the program text. The type and clock of an ast element
75
    is mutable (and initialized to dummy values). This avoids to have to
76
    duplicate ast structures (e.g. ast, typed_ast, clocked_ast). *)
77

  
78

  
79

  
80
(* The tag of an expression is a unique identifier used to distinguish
81
   different instances of the same node *)
82
and expr =
83
    {expr_tag: tag;
84
     expr_desc: expr_desc;
85
     mutable expr_type: Types.type_expr;
86
     mutable expr_clock: Clocks.clock_expr;
87
     mutable expr_delay: Delay.delay_expr;
88
     mutable expr_annot: expr_annot option;
89
     expr_loc: Location.t}
71
    location in the program text. The type and clock of an ast element is
72
    mutable (and initialized to dummy values). This avoids to have to duplicate
73
    ast structures (e.g. ast, typed_ast, clocked_ast). *)
74

  
75
and expr = {
76
  expr_tag : tag;
77
  expr_desc : expr_desc;
78
  mutable expr_type : Types.type_expr;
79
  mutable expr_clock : Clocks.clock_expr;
80
  mutable expr_delay : Delay.delay_expr;
81
  mutable expr_annot : expr_annot option;
82
  expr_loc : Location.t;
83
}
90 84

  
91 85
and expr_desc =
92 86
  | Expr_const of constant
93 87
  | Expr_ident of ident
94 88
  | Expr_tuple of expr list
95
  | Expr_ite   of expr * expr * expr
89
  | Expr_ite of expr * expr * expr
96 90
  | Expr_arrow of expr * expr
97 91
  | Expr_fby of expr * expr
98 92
  | Expr_array of expr list
......
104 98
  | Expr_appl of call_t
105 99

  
106 100
and call_t = ident * expr * expr option
107
     (* The third part denotes the boolean condition for resetting *)
108

  
109
and eq =
110
    {eq_lhs: ident list;
111
     eq_rhs: expr;
112
     eq_loc: Location.t}
113

  
114
  (* The tag of an expression is a unique identifier used to distinguish
115
     different instances of the same node *)
116
and  eexpr =
117
    {eexpr_tag: tag;
118
     eexpr_qfexpr: expr;
119
     eexpr_quantifiers: (quantifier_type * var_decl list) list;
120
     eexpr_name: string option;
121
     mutable eexpr_type: Types.type_expr;
122
     mutable eexpr_clock: Clocks.clock_expr;
123
     (* mutable eexpr_normalized: (var_decl * eq list * var_decl list) option; *)
124
     eexpr_loc: Location.t}
125

  
126
and expr_annot =
127
 {annots: (string list * eexpr) list;
128
  annot_loc: Location.t}
129

  
130
type contract_mode =
131
  {
132
    mode_id: ident;
133
    require: eexpr list;
134
    ensure: eexpr list;
135
    mode_loc: Location.t
136
  }
137

  
138
type contract_import =
139
  { import_nodeid: ident;
140
    inputs: expr;
141
    outputs: expr;
142
    import_loc: Location.t }
143
    
144

  
145

  
146
type offset =
147
| Index of Dimension.dim_expr
148
| Field of label
149

  
150
type assert_t =
151
    {
152
      assert_expr: expr;
153
      assert_loc: Location.t;
154
    }
155

  
156
type statement =
157
| Eq of eq
158
| Aut of automata_desc
159

  
160
and automata_desc =
161
  {aut_id : ident;
162
   aut_handlers: handler_desc list;
163
   aut_loc: Location.t}
164

  
165
and handler_desc =
166
  {hand_state: ident;
167
   hand_unless: (Location.t * expr * bool * ident) list;
168
   hand_until: (Location.t * expr * bool * ident) list;
169
   hand_locals: var_decl list;
170
   hand_stmts: statement list;
171
   hand_asserts: assert_t list;
172
   hand_annots: expr_annot list;
173
   hand_loc: Location.t}
174

  
175
type contract_desc = 
176
  {
177
    consts: var_decl list;
178
    locals: var_decl list;
179
    stmts: statement list;
180
    assume: eexpr list;
181
    guarantees: eexpr list;
182
    modes: contract_mode list;
183
    imports: contract_import list; 
184
    spec_loc: Location.t;
185
  }
186

  
187
type node_spec_t = Contract of contract_desc
188
                 | NodeSpec of ident
189

  
190
type node_desc =
191
    {node_id: ident;
192
     mutable node_type: Types.type_expr;
193
     mutable node_clock: Clocks.clock_expr;
194
     node_inputs: var_decl list;
195
     node_outputs: var_decl list;
196
     node_locals: var_decl list;
197
     mutable node_gencalls: expr list;
198
     mutable node_checks: Dimension.dim_expr list;
199
     node_asserts: assert_t list;
200
     node_stmts: statement list;
201
     mutable node_dec_stateless: bool;
202
     mutable node_stateless: bool option;
203
     node_spec: node_spec_t option;
204
     node_annot: expr_annot list;
205
     node_iscontract: bool;
206
    }
207

  
208
type imported_node_desc =
209
    {nodei_id: ident;
210
     mutable nodei_type: Types.type_expr;
211
     mutable nodei_clock: Clocks.clock_expr;
212
     nodei_inputs: var_decl list;
213
     nodei_outputs: var_decl list;
214
     nodei_stateless: bool;
215
     nodei_spec: node_spec_t option;
216
     (* nodei_annot: expr_annot list; *)
217
     nodei_prototype: string option;
218
     nodei_in_lib: string list;
219
    }
220

  
221
type const_desc =
222
    {const_id: ident;
223
     const_loc: Location.t;
224
     const_value: constant;
225
     mutable const_type: Types.type_expr;
226
    }
227

  
228
  
101
(* The third part denotes the boolean condition for resetting *)
102

  
103
and eq = { eq_lhs : ident list; eq_rhs : expr; eq_loc : Location.t }
104

  
105
(* The tag of an expression is a unique identifier used to distinguish different
106
   instances of the same node *)
107
and eexpr = {
108
  eexpr_tag : tag;
109
  eexpr_qfexpr : expr;
110
  eexpr_quantifiers : (quantifier_type * var_decl list) list;
111
  eexpr_name : string option;
112
  mutable eexpr_type : Types.type_expr;
113
  mutable eexpr_clock : Clocks.clock_expr;
114
  (* mutable eexpr_normalized: (var_decl * eq list * var_decl list) option; *)
115
  eexpr_loc : Location.t;
116
}
117

  
118
and expr_annot = { annots : (string list * eexpr) list; annot_loc : Location.t }
119

  
120
type contract_mode = {
121
  mode_id : ident;
122
  require : eexpr list;
123
  ensure : eexpr list;
124
  mode_loc : Location.t;
125
}
126

  
127
type contract_import = {
128
  import_nodeid : ident;
129
  inputs : expr;
130
  outputs : expr;
131
  import_loc : Location.t;
132
}
133

  
134
type offset = Index of Dimension.dim_expr | Field of label
135

  
136
type assert_t = { assert_expr : expr; assert_loc : Location.t }
137

  
138
type statement = Eq of eq | Aut of automata_desc
139

  
140
and automata_desc = {
141
  aut_id : ident;
142
  aut_handlers : handler_desc list;
143
  aut_loc : Location.t;
144
}
145

  
146
and handler_desc = {
147
  hand_state : ident;
148
  hand_unless : (Location.t * expr * bool * ident) list;
149
  hand_until : (Location.t * expr * bool * ident) list;
150
  hand_locals : var_decl list;
151
  hand_stmts : statement list;
152
  hand_asserts : assert_t list;
153
  hand_annots : expr_annot list;
154
  hand_loc : Location.t;
155
}
156

  
157
type contract_desc = {
158
  consts : var_decl list;
159
  locals : var_decl list;
160
  stmts : statement list;
161
  assume : eexpr list;
162
  guarantees : eexpr list;
163
  modes : contract_mode list;
164
  imports : contract_import list;
165
  spec_loc : Location.t;
166
}
167

  
168
type node_spec_t = Contract of contract_desc | NodeSpec of ident
169

  
170
type node_desc = {
171
  node_id : ident;
172
  mutable node_type : Types.type_expr;
173
  mutable node_clock : Clocks.clock_expr;
174
  node_inputs : var_decl list;
175
  node_outputs : var_decl list;
176
  node_locals : var_decl list;
177
  mutable node_gencalls : expr list;
178
  mutable node_checks : Dimension.dim_expr list;
179
  node_asserts : assert_t list;
180
  node_stmts : statement list;
181
  mutable node_dec_stateless : bool;
182
  mutable node_stateless : bool option;
183
  node_spec : node_spec_t option;
184
  node_annot : expr_annot list;
185
  node_iscontract : bool;
186
}
187

  
188
type imported_node_desc = {
189
  nodei_id : ident;
190
  mutable nodei_type : Types.type_expr;
191
  mutable nodei_clock : Clocks.clock_expr;
192
  nodei_inputs : var_decl list;
193
  nodei_outputs : var_decl list;
194
  nodei_stateless : bool;
195
  nodei_spec : node_spec_t option;
196
  (* nodei_annot: expr_annot list; *)
197
  nodei_prototype : string option;
198
  nodei_in_lib : string list;
199
}
200

  
201
type const_desc = {
202
  const_id : ident;
203
  const_loc : Location.t;
204
  const_value : constant;
205
  mutable const_type : Types.type_expr;
206
}
207

  
229 208
type top_decl_desc =
230 209
  | Node of node_desc
231 210
  | Const of const_desc
232 211
  | ImportedNode of imported_node_desc
233
  | Open of bool * string (* the boolean set to true denotes a local
234
			   lusi vs a lusi installed at system level *)
235
  | Include of string (* the boolean set to true denotes a local
236
			   lus vs a lus installed at system level *)
212
  | Open of bool * string
213
  (* the boolean set to true denotes a local lusi vs a lusi installed at system
214
     level *)
215
  | Include of string
216
  (* the boolean set to true denotes a local lus vs a lus installed at system
217
     level *)
237 218
  | TypeDef of typedef_desc
238
    
239
type top_decl =
240
    {top_decl_desc: top_decl_desc;      (* description of the symbol *)
241
     top_decl_owner: Location.filename; (* the module where it is defined *)
242
     top_decl_itf: bool;                (* header or source file ? *)
243
     top_decl_loc: Location.t}          (* the location where it is defined *)
219

  
220
type top_decl = {
221
  top_decl_desc : top_decl_desc;
222
  (* description of the symbol *)
223
  top_decl_owner : Location.filename;
224
  (* the module where it is defined *)
225
  top_decl_itf : bool;
226
  (* header or source file ? *)
227
  top_decl_loc : Location.t;
228
}
229
(* the location where it is defined *)
244 230

  
245 231
type program_t = top_decl list
246 232

  
247 233
type dep_t = {
248
    local: bool;
249
    name: ident;
250
    content: program_t;
251
    is_stateful: bool
252
  }
234
  local : bool;
235
  name : ident;
236
  content : program_t;
237
  is_stateful : bool;
238
}
253 239

  
254 240
type spec_types =
255 241
  | LocalContract of contract_desc
256 242
  | TopContract of top_decl list
257 243

  
258 244
let tag_true = "true"
259
let tag_false = "false"
260 245

  
246
let tag_false = "false"
261 247

  
262 248
(* Local Variables: *)
263 249
(* compile-command:"make -C .." *)

Also available in: Unified diff