Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec / src / lustreSpec.ml @ 45f0f48d

History | View | Annotate | Download (7.11 KB)

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 Format
13

    
14
type ident = Utils.ident
15
type rat = Utils.rat
16
type tag = Utils.tag
17
type label = Utils.ident
18

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

    
23
and type_dec_desc =
24
  | Tydec_any
25
  | Tydec_int
26
  | Tydec_real
27
  (* | Tydec_float *)
28
  | Tydec_bool
29
  | Tydec_clock of type_dec_desc
30
  | Tydec_const of ident
31
  | Tydec_enum of ident list
32
  | Tydec_struct of (ident * type_dec_desc) list
33
  | Tydec_array of Dimension.dim_expr * type_dec_desc
34

    
35
type typedec_desc =
36
    {tydec_id: ident}
37

    
38
type typedef_desc =
39
    {tydef_id: ident;
40
     tydef_desc: type_dec_desc}
41

    
42
type clock_dec =
43
    {ck_dec_desc: clock_dec_desc;
44
     ck_dec_loc: Location.t}
45

    
46
and clock_dec_desc =
47
  | Ckdec_any
48
  | Ckdec_bool of (ident * ident) list 
49

    
50

    
51
type constant =
52
  | Const_int of int
53
  | Const_real of Num.num * int * string (* (a, b, c) means a * 10^-b. c is the original string *)
54
  | Const_array of constant list
55
  | Const_tag of label
56
  | Const_string of string (* used only for annotations *)
57
  | Const_struct of (label * constant) list
58

    
59
type quantifier_type = Exists | Forall
60

    
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_type: Types.type_expr;
69
     mutable var_clock: Clocks.clock_expr;
70
     var_loc: Location.t}
71

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

    
77

    
78

    
79
(* The tag of an expression is a unique identifier used to distinguish
80
   different instances of the same node *)
81
and expr =
82
    {expr_tag: tag;
83
     expr_desc: expr_desc;
84
     mutable expr_type: Types.type_expr;
85
     mutable expr_clock: Clocks.clock_expr;
86
     mutable expr_delay: Delay.delay_expr;
87
     mutable expr_annot: expr_annot option;
88
     expr_loc: Location.t}
89

    
90
and expr_desc =
91
  | Expr_const of constant
92
  | Expr_ident of ident
93
  | Expr_tuple of expr list
94
  | Expr_ite   of expr * expr * expr
95
  | Expr_arrow of expr * expr
96
  | Expr_fby of expr * expr
97
  | Expr_array of expr list
98
  | Expr_access of expr * Dimension.dim_expr
99
  | Expr_power of expr * Dimension.dim_expr
100
  | Expr_pre of expr
101
  | Expr_when of expr * ident * label
102
  | Expr_merge of ident * (label * expr) list
103
  | Expr_appl of call_t
104

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

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

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

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

    
128
type node_annot = {
129
  requires: eexpr list;
130
  ensures: eexpr list;
131
  behaviors: (string * eexpr list * eexpr list * Location.t) list;
132
  spec_loc: Location.t;
133
}
134

    
135
type offset =
136
| Index of Dimension.dim_expr
137
| Field of label
138

    
139
type assert_t = 
140
    {
141
      assert_expr: expr;
142
      assert_loc: Location.t;
143
    }
144

    
145
type statement =
146
| Eq of eq
147
| Aut of automata_desc
148

    
149
and automata_desc =
150
  {aut_id : ident;
151
   aut_handlers: handler_desc list;
152
   aut_loc: Location.t}
153

    
154
and handler_desc =
155
  {hand_state: ident;
156
   hand_unless: (Location.t * expr * bool * ident) list;
157
   hand_until: (Location.t * expr * bool * ident) list;
158
   hand_locals: var_decl list;
159
   hand_stmts: statement list;
160
   hand_asserts: assert_t list;
161
   hand_annots: expr_annot list;
162
   hand_loc: Location.t}
163

    
164
type node_desc =
165
    {node_id: ident;
166
     mutable node_type: Types.type_expr;
167
     mutable node_clock: Clocks.clock_expr;
168
     node_inputs: var_decl list;
169
     node_outputs: var_decl list;
170
     node_locals: var_decl list;
171
     mutable node_gencalls: expr list;
172
     mutable node_checks: Dimension.dim_expr list;
173
     node_asserts: assert_t list; 
174
     node_stmts: statement list;
175
     mutable node_dec_stateless: bool;
176
     mutable node_stateless: bool option;
177
     node_spec: node_annot option;
178
     node_annot: expr_annot list;
179
    }
180

    
181
type imported_node_desc =
182
    {nodei_id: ident;
183
     mutable nodei_type: Types.type_expr;
184
     mutable nodei_clock: Clocks.clock_expr;
185
     nodei_inputs: var_decl list;
186
     nodei_outputs: var_decl list;
187
     nodei_stateless: bool;
188
     nodei_spec: node_annot option;
189
     nodei_prototype: string option;
190
     nodei_in_lib: string list;
191
    }
192

    
193
type const_desc = 
194
    {const_id: ident; 
195
     const_loc: Location.t; 
196
     const_value: constant;      
197
     mutable const_type: Types.type_expr;
198
    }
199

    
200
type top_decl_desc =
201
| Node of node_desc
202
| Const of const_desc
203
| ImportedNode of imported_node_desc
204
| Open of bool * string (* the boolean set to true denotes a local 
205
			   lusi vs a lusi installed at system level *)
206
| TypeDef of typedef_desc
207

    
208
type top_decl =
209
    {top_decl_desc: top_decl_desc;      (* description of the symbol *)
210
     top_decl_owner: Location.filename; (* the module where it is defined *)
211
     top_decl_itf: bool;                (* header or source file ? *)
212
     top_decl_loc: Location.t}          (* the location where it is defined *)
213

    
214
type program = top_decl list
215

    
216
type dep_t = Dep of 
217
    bool 
218
  * ident
219
  * (top_decl list) 
220
  * bool (* is stateful *)
221

    
222

    
223
(************ Machine code types *************)
224

    
225
type value_t = 
226
  {
227
    value_desc: value_t_desc;
228
    value_type: Types.type_expr;
229
    value_annot: expr_annot option
230
  }
231
and value_t_desc =
232
  | Cst of constant
233
  | LocalVar of var_decl
234
  | StateVar of var_decl
235
  | Fun of ident * value_t list 
236
  | Array of value_t list
237
  | Access of value_t * value_t
238
  | Power of value_t * value_t
239

    
240
type instr_t =
241
  | MLocalAssign of var_decl * value_t
242
  | MStateAssign of var_decl * value_t
243
  | MReset of ident
244
  | MNoReset of ident
245
  | MStep of var_decl list * ident * value_t list
246
  | MBranch of value_t * (label * instr_t list) list
247
  | MComment of string
248

    
249

    
250
type error =
251
    Main_not_found
252
  | Main_wrong_kind
253
  | No_main_specified
254
  | Unbound_symbol of ident
255
  | Already_bound_symbol of ident
256
  | Unknown_library of ident
257
  | Wrong_number of ident
258

    
259
(* Local Variables: *)
260
(* compile-command:"make -C .." *)
261
(* End: *)