Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec / src / lustreSpec.ml @ 53206908

History | View | Annotate | Download (7.14 KB)

1 b38ffff3 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 0cbf0839 ploc
open Format
13
14
type ident = Utils.ident
15
type rat = Utils.rat
16
type tag = Utils.tag
17 36454535 ploc
type label = Utils.ident
18 0cbf0839 ploc
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 53206908 xthirioux
  (* | Tydec_float *)
28 0cbf0839 ploc
  | Tydec_bool
29
  | Tydec_clock of type_dec_desc
30
  | Tydec_const of ident
31
  | Tydec_enum of ident list
32 6560bb94 xthirioux
  | Tydec_struct of (ident * type_dec_desc) list
33 0cbf0839 ploc
  | Tydec_array of Dimension.dim_expr * type_dec_desc
34
35 70e1006b xthirioux
type typedec_desc =
36
    {tydec_id: ident}
37
38
type typedef_desc =
39
    {tydef_id: ident;
40
     tydef_desc: type_dec_desc}
41 6aeb3388 xthirioux
42 0cbf0839 ploc
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
  | Ckdec_pclock of int * rat
50
51 01d48bb0 xthirioux
type constant =
52
  | Const_int of int
53 53206908 xthirioux
  | Const_real of Num.num * int * string (* (a,b, c) means a * 10^-b. c is the original string *)
54
  (* | Const_float of float *)
55 01d48bb0 xthirioux
  | Const_array of constant list
56
  | Const_tag of label
57
  | Const_string of string (* used only for annotations *)
58
  | Const_struct of (label * constant) list
59
60
type quantifier_type = Exists | Forall
61
62 0cbf0839 ploc
type var_decl = 
63
    {var_id: ident;
64 6a1a01d2 xthirioux
     var_orig:bool;
65 0cbf0839 ploc
     var_dec_type: type_dec;
66
     var_dec_clock: clock_dec;
67
     var_dec_const: bool;
68 01d48bb0 xthirioux
     var_dec_value: expr option;
69 0cbf0839 ploc
     mutable var_type: Types.type_expr;
70
     mutable var_clock: Clocks.clock_expr;
71
     var_loc: Location.t}
72
73 0038002e ploc
(** 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 0cbf0839 ploc
(* The tag of an expression is a unique identifier used to distinguish
79
   different instances of the same node *)
80 01d48bb0 xthirioux
and expr =
81 0038002e ploc
    {expr_tag: tag;
82
     expr_desc: expr_desc;
83
     mutable expr_type: Types.type_expr;
84
     mutable expr_clock: Clocks.clock_expr;
85
     mutable expr_delay: Delay.delay_expr;
86
     mutable expr_annot: expr_annot option;
87
     expr_loc: Location.t}
88
89
and expr_desc =
90
  | Expr_const of constant
91
  | Expr_ident of ident
92
  | Expr_tuple of expr list
93
  | Expr_ite   of expr * expr * expr
94
  | Expr_arrow of expr * expr
95
  | Expr_fby of expr * expr
96
  | Expr_array of expr list
97
  | Expr_access of expr * Dimension.dim_expr
98
  | Expr_power of expr * Dimension.dim_expr
99
  | Expr_pre of expr
100
  | Expr_when of expr * ident * label
101
  | Expr_merge of ident * (label * expr) list
102
  | Expr_appl of call_t
103 70e1006b xthirioux
104 6a1a01d2 xthirioux
and call_t = ident * expr * expr option 
105
     (* The third part denotes the boolean condition for resetting *)
106 70e1006b xthirioux
107
and eq =
108
    {eq_lhs: ident list;
109
     eq_rhs: expr;
110
     eq_loc: Location.t}
111
112 0038002e ploc
  (* The tag of an expression is a unique identifier used to distinguish
113
     different instances of the same node *)
114 70e1006b xthirioux
and  eexpr =
115 0cbf0839 ploc
    {eexpr_tag: tag;
116 0038002e ploc
     eexpr_qfexpr: expr;
117
     eexpr_quantifiers: (quantifier_type * var_decl list) list;
118 0cbf0839 ploc
     mutable eexpr_type: Types.type_expr;
119
     mutable eexpr_clock: Clocks.clock_expr;
120 0038002e ploc
     mutable eexpr_normalized: (var_decl * eq list * var_decl list) option;
121 0cbf0839 ploc
     eexpr_loc: Location.t}
122
123 70e1006b xthirioux
and expr_annot =
124
 {annots: (string list * eexpr) list;
125
  annot_loc: Location.t}
126 0cbf0839 ploc
127
type node_annot = {
128
  requires: eexpr list;
129 0038002e ploc
  ensures: eexpr list;
130
  behaviors: (string * eexpr list * eexpr list * Location.t) list;
131
  spec_loc: Location.t;
132 0cbf0839 ploc
}
133 79614a15 xthirioux
134
type offset =
135
| Index of Dimension.dim_expr
136
| Field of label
137
138 0038002e ploc
type assert_t = 
139
    {
140
      assert_expr: expr;
141 36454535 ploc
      assert_loc: Location.t;
142 1eda3e78 xthirioux
    }
143
144
type statement =
145
| Eq of eq
146
| Aut of automata_desc
147 0038002e ploc
148 1eda3e78 xthirioux
and automata_desc =
149 70e1006b xthirioux
  {aut_id : ident;
150
   aut_handlers: handler_desc list;
151
   aut_loc: Location.t}
152
153
and handler_desc =
154
  {hand_state: ident;
155 29ced7be xthirioux
   hand_unless: (Location.t * expr * bool * ident) list;
156
   hand_until: (Location.t * expr * bool * ident) list;
157 70e1006b xthirioux
   hand_locals: var_decl list;
158 1eda3e78 xthirioux
   hand_stmts: statement list;
159 29ced7be xthirioux
   hand_asserts: assert_t list;
160
   hand_annots: expr_annot list;
161 70e1006b xthirioux
   hand_loc: Location.t}
162
163 0038002e ploc
type node_desc =
164
    {node_id: ident;
165
     mutable node_type: Types.type_expr;
166
     mutable node_clock: Clocks.clock_expr;
167
     node_inputs: var_decl list;
168
     node_outputs: var_decl list;
169
     node_locals: var_decl list;
170
     mutable node_gencalls: expr list;
171
     mutable node_checks: Dimension.dim_expr list;
172
     node_asserts: assert_t list; 
173 1eda3e78 xthirioux
     node_stmts: statement list;
174 0038002e ploc
     mutable node_dec_stateless: bool;
175
     mutable node_stateless: bool option;
176
     node_spec: node_annot option;
177
     node_annot: expr_annot list;
178
    }
179
180
type imported_node_desc =
181
    {nodei_id: ident;
182
     mutable nodei_type: Types.type_expr;
183
     mutable nodei_clock: Clocks.clock_expr;
184
     nodei_inputs: var_decl list;
185
     nodei_outputs: var_decl list;
186
     nodei_stateless: bool;
187
     nodei_spec: node_annot option;
188
     nodei_prototype: string option;
189 53206908 xthirioux
     nodei_in_lib: string list;
190 0038002e ploc
    }
191
192
type const_desc = 
193
    {const_id: ident; 
194
     const_loc: Location.t; 
195
     const_value: constant;      
196
     mutable const_type: Types.type_expr;
197
    }
198
199
type top_decl_desc =
200
| Node of node_desc
201 70e1006b xthirioux
| Const of const_desc
202 0038002e ploc
| ImportedNode of imported_node_desc
203
| Open of bool * string (* the boolean set to true denotes a local 
204
			   lusi vs a lusi installed at system level *)
205 70e1006b xthirioux
| TypeDef of typedef_desc
206 0038002e ploc
207
type top_decl =
208 70e1006b xthirioux
    {top_decl_desc: top_decl_desc;      (* description of the symbol *)
209
     top_decl_owner: Location.filename; (* the module where it is defined *)
210
     top_decl_itf: bool;                (* header or source file ? *)
211
     top_decl_loc: Location.t}          (* the location where it is defined *)
212 0038002e ploc
213
type program = top_decl list
214
215 830de634 ploc
type dep_t = Dep of 
216
    bool 
217
  * ident
218
  * (top_decl list) 
219
  * bool (* is stateful *)
220
221 53206908 xthirioux
222
(************ Machine code types *************)
223
224
type value_t = 
225
  {
226
    value_desc: value_t_desc;
227
    value_type: Types.type_expr;
228
    value_annot: expr_annot option
229
  }
230
and value_t_desc =
231
  | Cst of constant
232
  | LocalVar of var_decl
233
  | StateVar of var_decl
234
  | Fun of ident * value_t list 
235
  | Array of value_t list
236
  | Access of value_t * value_t
237
  | Power of value_t * value_t
238
239
type instr_t =
240
  | MLocalAssign of var_decl * value_t
241
  | MStateAssign of var_decl * value_t
242
  | MReset of ident
243
  | MStep of var_decl list * ident * value_t list
244
  | MBranch of value_t * (label * instr_t list) list
245
  | MComment of string
246
247
248 0038002e ploc
type error =
249
    Main_not_found
250
  | Main_wrong_kind
251
  | No_main_specified
252
  | Unbound_symbol of ident
253
  | Already_bound_symbol of ident
254 70e1006b xthirioux
  | Unknown_library of ident
255 01d48bb0 xthirioux
  | Wrong_number of ident
256 0cbf0839 ploc
257
(* Local Variables: *)
258
(* compile-command:"make -C .." *)
259
(* End: *)