lustrec / src / lustreSpec.ml @ 2d179f5b
History | View | Annotate | Download (6.45 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 | open Format |
13 | |||
14 | type ident = Utils.ident |
||
15 | type rat = Utils.rat |
||
16 | type tag = Utils.tag |
||
17 | af5af1e8 | ploc | type label = Utils.ident |
18 | 22fe1c93 | 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 | | Tydec_float |
||
28 | | Tydec_bool |
||
29 | | Tydec_clock of type_dec_desc |
||
30 | | Tydec_const of ident |
||
31 | | Tydec_enum of ident list |
||
32 | 6a6abd76 | xthirioux | | Tydec_struct of (ident * type_dec_desc) list |
33 | 22fe1c93 | ploc | | Tydec_array of Dimension.dim_expr * type_dec_desc |
34 | |||
35 | ef34b4ae | xthirioux | type typedec_desc = |
36 | {tydec_id: ident} |
||
37 | |||
38 | type typedef_desc = |
||
39 | {tydef_id: ident; |
||
40 | tydef_desc: type_dec_desc} |
||
41 | b1655a21 | xthirioux | |
42 | 22fe1c93 | 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 | ec433d69 | xthirioux | type constant = |
52 | | Const_int of int |
||
53 | | Const_real of string |
||
54 | | Const_float of float |
||
55 | | 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 | 22fe1c93 | ploc | type var_decl = |
63 | {var_id: ident; |
||
64 | 54d032f5 | xthirioux | var_orig:bool; |
65 | 22fe1c93 | ploc | var_dec_type: type_dec; |
66 | var_dec_clock: clock_dec; |
||
67 | var_dec_const: bool; |
||
68 | ec433d69 | xthirioux | var_dec_value: expr option; |
69 | 22fe1c93 | ploc | mutable var_type: Types.type_expr; |
70 | mutable var_clock: Clocks.clock_expr; |
||
71 | var_loc: Location.t} |
||
72 | |||
73 | 01c7d5e1 | 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 | |||
79 | |||
80 | 22fe1c93 | ploc | (* The tag of an expression is a unique identifier used to distinguish |
81 | different instances of the same node *) |
||
82 | ec433d69 | xthirioux | and expr = |
83 | 01c7d5e1 | ploc | {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} |
||
90 | |||
91 | and expr_desc = |
||
92 | | Expr_const of constant |
||
93 | | Expr_ident of ident |
||
94 | | Expr_tuple of expr list |
||
95 | | Expr_ite of expr * expr * expr |
||
96 | | Expr_arrow of expr * expr |
||
97 | | Expr_fby of expr * expr |
||
98 | | Expr_array of expr list |
||
99 | | Expr_access of expr * Dimension.dim_expr |
||
100 | | Expr_power of expr * Dimension.dim_expr |
||
101 | | Expr_pre of expr |
||
102 | | Expr_when of expr * ident * label |
||
103 | | Expr_merge of ident * (label * expr) list |
||
104 | | Expr_appl of call_t |
||
105 | ef34b4ae | xthirioux | |
106 | 54d032f5 | xthirioux | and call_t = ident * expr * expr option |
107 | (* The third part denotes the boolean condition for resetting *) |
||
108 | ef34b4ae | xthirioux | |
109 | and eq = |
||
110 | {eq_lhs: ident list; |
||
111 | eq_rhs: expr; |
||
112 | eq_loc: Location.t} |
||
113 | |||
114 | 01c7d5e1 | ploc | (* The tag of an expression is a unique identifier used to distinguish |
115 | different instances of the same node *) |
||
116 | ef34b4ae | xthirioux | and eexpr = |
117 | 22fe1c93 | ploc | {eexpr_tag: tag; |
118 | 01c7d5e1 | ploc | eexpr_qfexpr: expr; |
119 | eexpr_quantifiers: (quantifier_type * var_decl list) list; |
||
120 | 22fe1c93 | ploc | mutable eexpr_type: Types.type_expr; |
121 | mutable eexpr_clock: Clocks.clock_expr; |
||
122 | 01c7d5e1 | ploc | mutable eexpr_normalized: (var_decl * eq list * var_decl list) option; |
123 | 22fe1c93 | ploc | eexpr_loc: Location.t} |
124 | |||
125 | ef34b4ae | xthirioux | and expr_annot = |
126 | {annots: (string list * eexpr) list; |
||
127 | annot_loc: Location.t} |
||
128 | 22fe1c93 | ploc | |
129 | type node_annot = { |
||
130 | requires: eexpr list; |
||
131 | 01c7d5e1 | ploc | ensures: eexpr list; |
132 | behaviors: (string * eexpr list * eexpr list * Location.t) list; |
||
133 | spec_loc: Location.t; |
||
134 | 22fe1c93 | ploc | } |
135 | 2d179f5b | xthirioux | |
136 | type offset = |
||
137 | | Index of Dimension.dim_expr |
||
138 | | Field of label |
||
139 | |||
140 | 01c7d5e1 | ploc | type assert_t = |
141 | { |
||
142 | assert_expr: expr; |
||
143 | af5af1e8 | ploc | assert_loc: Location.t; |
144 | b08ffca7 | xthirioux | } |
145 | |||
146 | type statement = |
||
147 | | Eq of eq |
||
148 | | Aut of automata_desc |
||
149 | 01c7d5e1 | ploc | |
150 | b08ffca7 | xthirioux | and automata_desc = |
151 | ef34b4ae | xthirioux | {aut_id : ident; |
152 | aut_handlers: handler_desc list; |
||
153 | aut_loc: Location.t} |
||
154 | |||
155 | and handler_desc = |
||
156 | {hand_state: ident; |
||
157 | 2822cf55 | xthirioux | hand_unless: (Location.t * expr * bool * ident) list; |
158 | hand_until: (Location.t * expr * bool * ident) list; |
||
159 | ef34b4ae | xthirioux | hand_locals: var_decl list; |
160 | b08ffca7 | xthirioux | hand_stmts: statement list; |
161 | 2822cf55 | xthirioux | hand_asserts: assert_t list; |
162 | hand_annots: expr_annot list; |
||
163 | ef34b4ae | xthirioux | hand_loc: Location.t} |
164 | |||
165 | 01c7d5e1 | ploc | type node_desc = |
166 | {node_id: ident; |
||
167 | mutable node_type: Types.type_expr; |
||
168 | mutable node_clock: Clocks.clock_expr; |
||
169 | node_inputs: var_decl list; |
||
170 | node_outputs: var_decl list; |
||
171 | node_locals: var_decl list; |
||
172 | mutable node_gencalls: expr list; |
||
173 | mutable node_checks: Dimension.dim_expr list; |
||
174 | node_asserts: assert_t list; |
||
175 | b08ffca7 | xthirioux | node_stmts: statement list; |
176 | 01c7d5e1 | ploc | mutable node_dec_stateless: bool; |
177 | mutable node_stateless: bool option; |
||
178 | node_spec: node_annot option; |
||
179 | node_annot: expr_annot list; |
||
180 | } |
||
181 | |||
182 | type imported_node_desc = |
||
183 | {nodei_id: ident; |
||
184 | mutable nodei_type: Types.type_expr; |
||
185 | mutable nodei_clock: Clocks.clock_expr; |
||
186 | nodei_inputs: var_decl list; |
||
187 | nodei_outputs: var_decl list; |
||
188 | nodei_stateless: bool; |
||
189 | nodei_spec: node_annot option; |
||
190 | nodei_prototype: string option; |
||
191 | nodei_in_lib: string option; |
||
192 | } |
||
193 | |||
194 | type const_desc = |
||
195 | {const_id: ident; |
||
196 | const_loc: Location.t; |
||
197 | const_value: constant; |
||
198 | mutable const_type: Types.type_expr; |
||
199 | } |
||
200 | |||
201 | type top_decl_desc = |
||
202 | | Node of node_desc |
||
203 | ef34b4ae | xthirioux | | Const of const_desc |
204 | 01c7d5e1 | ploc | | ImportedNode of imported_node_desc |
205 | | Open of bool * string (* the boolean set to true denotes a local |
||
206 | lusi vs a lusi installed at system level *) |
||
207 | ef34b4ae | xthirioux | | TypeDef of typedef_desc |
208 | 01c7d5e1 | ploc | |
209 | type top_decl = |
||
210 | ef34b4ae | xthirioux | {top_decl_desc: top_decl_desc; (* description of the symbol *) |
211 | top_decl_owner: Location.filename; (* the module where it is defined *) |
||
212 | top_decl_itf: bool; (* header or source file ? *) |
||
213 | top_decl_loc: Location.t} (* the location where it is defined *) |
||
214 | 01c7d5e1 | ploc | |
215 | type program = top_decl list |
||
216 | |||
217 | 58a463e7 | ploc | type dep_t = Dep of |
218 | bool |
||
219 | * ident |
||
220 | * (top_decl list) |
||
221 | * bool (* is stateful *) |
||
222 | |||
223 | 01c7d5e1 | ploc | type error = |
224 | Main_not_found |
||
225 | | Main_wrong_kind |
||
226 | | No_main_specified |
||
227 | | Unbound_symbol of ident |
||
228 | | Already_bound_symbol of ident |
||
229 | ef34b4ae | xthirioux | | Unknown_library of ident |
230 | ec433d69 | xthirioux | | Wrong_number of ident |
231 | 22fe1c93 | ploc | |
232 | (* Local Variables: *) |
||
233 | (* compile-command:"make -C .." *) |
||
234 | (* End: *) |