Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec / src / lustreSpec.ml @ 2d179f5b

History | View | Annotate | Download (6.45 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
  | Ckdec_pclock of int * rat
50

    
51
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
type var_decl = 
63
    {var_id: ident;
64
     var_orig:bool;
65
     var_dec_type: type_dec;
66
     var_dec_clock: clock_dec;
67
     var_dec_const: bool;
68
     var_dec_value: expr option;
69
     mutable var_type: Types.type_expr;
70
     mutable var_clock: Clocks.clock_expr;
71
     var_loc: Location.t}
72

    
73
(** 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
(* The tag of an expression is a unique identifier used to distinguish
81
   different instances of the same node *)
82
and expr =
83
    {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

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

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

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

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

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

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

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

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

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

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

    
165
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
     node_stmts: statement list;
176
     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
| Const of const_desc
204
| 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
| TypeDef of typedef_desc
208

    
209
type top_decl =
210
    {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

    
215
type program = top_decl list
216

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

    
223
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
  | Unknown_library of ident
230
  | Wrong_number of ident
231

    
232
(* Local Variables: *)
233
(* compile-command:"make -C .." *)
234
(* End: *)