Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec / src / lustreSpec.ml @ ef8a361a

History | View | Annotate | Download (7.35 KB)

1 a2d97a3e ploc
(********************************************************************)
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 22fe1c93 ploc
type ident = Utils.ident
13
type rat = Utils.rat
14
type tag = Utils.tag
15 af5af1e8 ploc
type label = Utils.ident
16 22fe1c93 ploc
17
type type_dec =
18
    {ty_dec_desc: type_dec_desc;
19
     ty_dec_loc: Location.t}
20
21
and type_dec_desc =
22
  | Tydec_any
23
  | Tydec_int
24
  | Tydec_real
25 04a63d25 xthirioux
  (* | Tydec_float *)
26 22fe1c93 ploc
  | Tydec_bool
27
  | Tydec_clock of type_dec_desc
28
  | Tydec_const of ident
29
  | Tydec_enum of ident list
30 6a6abd76 xthirioux
  | Tydec_struct of (ident * type_dec_desc) list
31 22fe1c93 ploc
  | Tydec_array of Dimension.dim_expr * type_dec_desc
32
33 ef34b4ae xthirioux
type typedec_desc =
34
    {tydec_id: ident}
35
36
type typedef_desc =
37
    {tydef_id: ident;
38
     tydef_desc: type_dec_desc}
39 b1655a21 xthirioux
40 22fe1c93 ploc
type clock_dec =
41
    {ck_dec_desc: clock_dec_desc;
42
     ck_dec_loc: Location.t}
43
44
and clock_dec_desc =
45
  | Ckdec_any
46
  | Ckdec_bool of (ident * ident) list 
47 45f0f48d xthirioux
48 22fe1c93 ploc
49 ec433d69 xthirioux
type constant =
50
  | Const_int of int
51 04a63d25 xthirioux
  | Const_real of Num.num * int * string (* (a, b, c) means a * 10^-b. c is the original string *)
52 ec433d69 xthirioux
  | 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 22fe1c93 ploc
type var_decl = 
60
    {var_id: ident;
61 54d032f5 xthirioux
     var_orig:bool;
62 22fe1c93 ploc
     var_dec_type: type_dec;
63
     var_dec_clock: clock_dec;
64
     var_dec_const: bool;
65 ec433d69 xthirioux
     var_dec_value: expr option;
66 22fe1c93 ploc
     mutable var_type: Types.type_expr;
67
     mutable var_clock: Clocks.clock_expr;
68
     var_loc: Location.t}
69
70 01c7d5e1 ploc
(** The core language and its ast. Every element of the ast contains its
71
    location in the program text. The type and clock of an ast element
72
    is mutable (and initialized to dummy values). This avoids to have to
73
    duplicate ast structures (e.g. ast, typed_ast, clocked_ast). *)
74
75
76
77 22fe1c93 ploc
(* The tag of an expression is a unique identifier used to distinguish
78
   different instances of the same node *)
79 ec433d69 xthirioux
and expr =
80 01c7d5e1 ploc
    {expr_tag: tag;
81
     expr_desc: expr_desc;
82
     mutable expr_type: Types.type_expr;
83
     mutable expr_clock: Clocks.clock_expr;
84
     mutable expr_delay: Delay.delay_expr;
85
     mutable expr_annot: expr_annot option;
86
     expr_loc: Location.t}
87
88
and expr_desc =
89
  | Expr_const of constant
90
  | Expr_ident of ident
91
  | Expr_tuple of expr list
92
  | Expr_ite   of expr * expr * expr
93
  | Expr_arrow of expr * expr
94
  | Expr_fby of expr * expr
95
  | Expr_array of expr list
96
  | Expr_access of expr * Dimension.dim_expr
97
  | Expr_power of expr * Dimension.dim_expr
98
  | Expr_pre of expr
99
  | Expr_when of expr * ident * label
100
  | Expr_merge of ident * (label * expr) list
101
  | Expr_appl of call_t
102 ef34b4ae xthirioux
103 54d032f5 xthirioux
and call_t = ident * expr * expr option 
104
     (* The third part denotes the boolean condition for resetting *)
105 ef34b4ae xthirioux
106
and eq =
107
    {eq_lhs: ident list;
108
     eq_rhs: expr;
109
     eq_loc: Location.t}
110
111 01c7d5e1 ploc
  (* The tag of an expression is a unique identifier used to distinguish
112
     different instances of the same node *)
113 ef34b4ae xthirioux
and  eexpr =
114 22fe1c93 ploc
    {eexpr_tag: tag;
115 01c7d5e1 ploc
     eexpr_qfexpr: expr;
116
     eexpr_quantifiers: (quantifier_type * var_decl list) list;
117 22fe1c93 ploc
     mutable eexpr_type: Types.type_expr;
118
     mutable eexpr_clock: Clocks.clock_expr;
119 01c7d5e1 ploc
     mutable eexpr_normalized: (var_decl * eq list * var_decl list) option;
120 22fe1c93 ploc
     eexpr_loc: Location.t}
121
122 ef34b4ae xthirioux
and expr_annot =
123
 {annots: (string list * eexpr) list;
124
  annot_loc: Location.t}
125 22fe1c93 ploc
126
type node_annot = {
127
  requires: eexpr list;
128 01c7d5e1 ploc
  ensures: eexpr list;
129
  behaviors: (string * eexpr list * eexpr list * Location.t) list;
130
  spec_loc: Location.t;
131 22fe1c93 ploc
}
132 2d179f5b xthirioux
133
type offset =
134
| Index of Dimension.dim_expr
135
| Field of label
136
137 01c7d5e1 ploc
type assert_t = 
138
    {
139
      assert_expr: expr;
140 af5af1e8 ploc
      assert_loc: Location.t;
141 b08ffca7 xthirioux
    }
142
143
type statement =
144
| Eq of eq
145
| Aut of automata_desc
146 01c7d5e1 ploc
147 b08ffca7 xthirioux
and automata_desc =
148 ef34b4ae xthirioux
  {aut_id : ident;
149
   aut_handlers: handler_desc list;
150
   aut_loc: Location.t}
151
152
and handler_desc =
153
  {hand_state: ident;
154 2822cf55 xthirioux
   hand_unless: (Location.t * expr * bool * ident) list;
155
   hand_until: (Location.t * expr * bool * ident) list;
156 ef34b4ae xthirioux
   hand_locals: var_decl list;
157 b08ffca7 xthirioux
   hand_stmts: statement list;
158 2822cf55 xthirioux
   hand_asserts: assert_t list;
159
   hand_annots: expr_annot list;
160 ef34b4ae xthirioux
   hand_loc: Location.t}
161
162 01c7d5e1 ploc
type node_desc =
163
    {node_id: ident;
164
     mutable node_type: Types.type_expr;
165
     mutable node_clock: Clocks.clock_expr;
166
     node_inputs: var_decl list;
167
     node_outputs: var_decl list;
168
     node_locals: var_decl list;
169
     mutable node_gencalls: expr list;
170
     mutable node_checks: Dimension.dim_expr list;
171
     node_asserts: assert_t list; 
172 b08ffca7 xthirioux
     node_stmts: statement list;
173 01c7d5e1 ploc
     mutable node_dec_stateless: bool;
174
     mutable node_stateless: bool option;
175
     node_spec: node_annot option;
176
     node_annot: expr_annot list;
177
    }
178
179
type imported_node_desc =
180
    {nodei_id: ident;
181
     mutable nodei_type: Types.type_expr;
182
     mutable nodei_clock: Clocks.clock_expr;
183
     nodei_inputs: var_decl list;
184
     nodei_outputs: var_decl list;
185
     nodei_stateless: bool;
186
     nodei_spec: node_annot option;
187
     nodei_prototype: string option;
188 04a63d25 xthirioux
     nodei_in_lib: string list;
189 01c7d5e1 ploc
    }
190
191
type const_desc = 
192
    {const_id: ident; 
193
     const_loc: Location.t; 
194
     const_value: constant;      
195
     mutable const_type: Types.type_expr;
196
    }
197
198
type top_decl_desc =
199
| Node of node_desc
200 ef34b4ae xthirioux
| Const of const_desc
201 01c7d5e1 ploc
| ImportedNode of imported_node_desc
202
| Open of bool * string (* the boolean set to true denotes a local 
203
			   lusi vs a lusi installed at system level *)
204 ef34b4ae xthirioux
| TypeDef of typedef_desc
205 01c7d5e1 ploc
206
type top_decl =
207 ef34b4ae xthirioux
    {top_decl_desc: top_decl_desc;      (* description of the symbol *)
208
     top_decl_owner: Location.filename; (* the module where it is defined *)
209
     top_decl_itf: bool;                (* header or source file ? *)
210
     top_decl_loc: Location.t}          (* the location where it is defined *)
211 01c7d5e1 ploc
212
type program = top_decl list
213
214 58a463e7 ploc
type dep_t = Dep of 
215
    bool 
216
  * ident
217
  * (top_decl list) 
218
  * bool (* is stateful *)
219
220 04a63d25 xthirioux
221
(************ Machine code types *************)
222
223
type value_t = 
224
  {
225
    value_desc: value_t_desc;
226
    value_type: Types.type_expr;
227
    value_annot: expr_annot option
228
  }
229
and value_t_desc =
230
  | Cst of constant
231
  | LocalVar of var_decl
232
  | StateVar of var_decl
233
  | Fun of ident * value_t list 
234
  | Array of value_t list
235
  | Access of value_t * value_t
236
  | Power of value_t * value_t
237
238
type instr_t =
239 3ca27bc7 ploc
  {
240 1bff14ac ploc
    instr_desc: instr_t_desc; (* main data: the content *)
241
    (* lustre_expr: expr option; (* possible representation as a lustre expression *) *)
242
    lustre_eq: eq option;     (* possible representation as a lustre flow equation *)
243 3ca27bc7 ploc
  }
244
and instr_t_desc =
245 04a63d25 xthirioux
  | MLocalAssign of var_decl * value_t
246
  | MStateAssign of var_decl * value_t
247
  | MReset of ident
248 45f0f48d xthirioux
  | MNoReset of ident
249 04a63d25 xthirioux
  | MStep of var_decl list * ident * value_t list
250
  | MBranch of value_t * (label * instr_t list) list
251
  | MComment of string
252
253
254 01c7d5e1 ploc
type error =
255
    Main_not_found
256
  | Main_wrong_kind
257
  | No_main_specified
258
  | Unbound_symbol of ident
259
  | Already_bound_symbol of ident
260 ef34b4ae xthirioux
  | Unknown_library of ident
261 ec433d69 xthirioux
  | Wrong_number of ident
262 22fe1c93 ploc
263
(* Local Variables: *)
264
(* compile-command:"make -C .." *)
265
(* End: *)