Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec / src / lustreSpec.ml @ 01d48bb0

History | View | Annotate | Download (6.39 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
  | Tydec_float
28
  | 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
  | 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 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
79
80 0cbf0839 ploc
(* The tag of an expression is a unique identifier used to distinguish
81
   different instances of the same node *)
82 01d48bb0 xthirioux
and expr =
83 0038002e 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 70e1006b xthirioux
106 6a1a01d2 xthirioux
and call_t = ident * expr * expr option 
107
     (* The third part denotes the boolean condition for resetting *)
108 70e1006b xthirioux
109
and eq =
110
    {eq_lhs: ident list;
111
     eq_rhs: expr;
112
     eq_loc: Location.t}
113
114 0038002e ploc
  (* The tag of an expression is a unique identifier used to distinguish
115
     different instances of the same node *)
116 70e1006b xthirioux
and  eexpr =
117 0cbf0839 ploc
    {eexpr_tag: tag;
118 0038002e ploc
     eexpr_qfexpr: expr;
119
     eexpr_quantifiers: (quantifier_type * var_decl list) list;
120 0cbf0839 ploc
     mutable eexpr_type: Types.type_expr;
121
     mutable eexpr_clock: Clocks.clock_expr;
122 0038002e ploc
     mutable eexpr_normalized: (var_decl * eq list * var_decl list) option;
123 0cbf0839 ploc
     eexpr_loc: Location.t}
124
125 70e1006b xthirioux
and expr_annot =
126
 {annots: (string list * eexpr) list;
127
  annot_loc: Location.t}
128 0cbf0839 ploc
129
type node_annot = {
130
  requires: eexpr list;
131 0038002e ploc
  ensures: eexpr list;
132
  behaviors: (string * eexpr list * eexpr list * Location.t) list;
133
  spec_loc: Location.t;
134 0cbf0839 ploc
}
135 0038002e ploc
type assert_t = 
136
    {
137
      assert_expr: expr;
138 36454535 ploc
      assert_loc: Location.t;
139 1eda3e78 xthirioux
    }
140
141
type statement =
142
| Eq of eq
143
| Aut of automata_desc
144 0038002e ploc
145 1eda3e78 xthirioux
and automata_desc =
146 70e1006b xthirioux
  {aut_id : ident;
147
   aut_handlers: handler_desc list;
148
   aut_loc: Location.t}
149
150
and handler_desc =
151
  {hand_state: ident;
152 29ced7be xthirioux
   hand_unless: (Location.t * expr * bool * ident) list;
153
   hand_until: (Location.t * expr * bool * ident) list;
154 70e1006b xthirioux
   hand_locals: var_decl list;
155 1eda3e78 xthirioux
   hand_stmts: statement list;
156 29ced7be xthirioux
   hand_asserts: assert_t list;
157
   hand_annots: expr_annot list;
158 70e1006b xthirioux
   hand_loc: Location.t}
159
160 0038002e ploc
type node_desc =
161
    {node_id: ident;
162
     mutable node_type: Types.type_expr;
163
     mutable node_clock: Clocks.clock_expr;
164
     node_inputs: var_decl list;
165
     node_outputs: var_decl list;
166
     node_locals: var_decl list;
167
     mutable node_gencalls: expr list;
168
     mutable node_checks: Dimension.dim_expr list;
169
     node_asserts: assert_t list; 
170 1eda3e78 xthirioux
     node_stmts: statement list;
171 0038002e ploc
     mutable node_dec_stateless: bool;
172
     mutable node_stateless: bool option;
173
     node_spec: node_annot option;
174
     node_annot: expr_annot list;
175
    }
176
177
type imported_node_desc =
178
    {nodei_id: ident;
179
     mutable nodei_type: Types.type_expr;
180
     mutable nodei_clock: Clocks.clock_expr;
181
     nodei_inputs: var_decl list;
182
     nodei_outputs: var_decl list;
183
     nodei_stateless: bool;
184
     nodei_spec: node_annot option;
185
     nodei_prototype: string option;
186
     nodei_in_lib: string option;
187
    }
188
189
type const_desc = 
190
    {const_id: ident; 
191
     const_loc: Location.t; 
192
     const_value: constant;      
193
     mutable const_type: Types.type_expr;
194
    }
195
196
type top_decl_desc =
197
| Node of node_desc
198 70e1006b xthirioux
| Const of const_desc
199 0038002e ploc
| ImportedNode of imported_node_desc
200
| Open of bool * string (* the boolean set to true denotes a local 
201
			   lusi vs a lusi installed at system level *)
202 70e1006b xthirioux
| TypeDef of typedef_desc
203 0038002e ploc
204
type top_decl =
205 70e1006b xthirioux
    {top_decl_desc: top_decl_desc;      (* description of the symbol *)
206
     top_decl_owner: Location.filename; (* the module where it is defined *)
207
     top_decl_itf: bool;                (* header or source file ? *)
208
     top_decl_loc: Location.t}          (* the location where it is defined *)
209 0038002e ploc
210
type program = top_decl list
211
212 830de634 ploc
type dep_t = Dep of 
213
    bool 
214
  * ident
215
  * (top_decl list) 
216
  * bool (* is stateful *)
217
218 0038002e ploc
type error =
219
    Main_not_found
220
  | Main_wrong_kind
221
  | No_main_specified
222
  | Unbound_symbol of ident
223
  | Already_bound_symbol of ident
224 70e1006b xthirioux
  | Unknown_library of ident
225 01d48bb0 xthirioux
  | Wrong_number of ident
226 0cbf0839 ploc
227
(* Local Variables: *)
228
(* compile-command:"make -C .." *)
229
(* End: *)