Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec / src / lustreSpec.ml @ 58a463e7

History | View | Annotate | Download (6.33 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 var_decl = 
52
    {var_id: ident;
53
     var_orig:bool;
54
     var_dec_type: type_dec;
55
     var_dec_clock: clock_dec;
56
     var_dec_const: bool;
57
     mutable var_type: Types.type_expr;
58
     mutable var_clock: Clocks.clock_expr;
59
     var_loc: Location.t}
60

    
61
(** The core language and its ast. Every element of the ast contains its
62
    location in the program text. The type and clock of an ast element
63
    is mutable (and initialized to dummy values). This avoids to have to
64
    duplicate ast structures (e.g. ast, typed_ast, clocked_ast). *)
65

    
66

    
67
type constant =
68
  | Const_int of int
69
  | Const_real of string
70
  | Const_float of float
71
  | Const_array of constant list
72
  | Const_tag of label
73
  | Const_string of string (* used only for annotations *)
74
  | Const_struct of (label * constant) list
75

    
76
type quantifier_type = Exists | Forall
77

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

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

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

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

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

    
127
type node_annot = {
128
  requires: eexpr list;
129
  ensures: eexpr list;
130
  behaviors: (string * eexpr list * eexpr list * Location.t) list;
131
  spec_loc: Location.t;
132
}
133
type assert_t = 
134
    {
135
      assert_expr: expr;
136
      assert_loc: Location.t;
137
    }
138

    
139
type statement =
140
| Eq of eq
141
| Aut of automata_desc
142

    
143
and automata_desc =
144
  {aut_id : ident;
145
   aut_handlers: handler_desc list;
146
   aut_loc: Location.t}
147

    
148
and handler_desc =
149
  {hand_state: ident;
150
   hand_unless: (Location.t * expr * bool * ident) list;
151
   hand_until: (Location.t * expr * bool * ident) list;
152
   hand_locals: var_decl list;
153
   hand_stmts: statement list;
154
   hand_asserts: assert_t list;
155
   hand_annots: expr_annot list;
156
   hand_loc: Location.t}
157

    
158
type node_desc =
159
    {node_id: ident;
160
     mutable node_type: Types.type_expr;
161
     mutable node_clock: Clocks.clock_expr;
162
     node_inputs: var_decl list;
163
     node_outputs: var_decl list;
164
     node_locals: var_decl list;
165
     mutable node_gencalls: expr list;
166
     mutable node_checks: Dimension.dim_expr list;
167
     node_asserts: assert_t list; 
168
     node_stmts: statement list;
169
     mutable node_dec_stateless: bool;
170
     mutable node_stateless: bool option;
171
     node_spec: node_annot option;
172
     node_annot: expr_annot list;
173
    }
174

    
175
type imported_node_desc =
176
    {nodei_id: ident;
177
     mutable nodei_type: Types.type_expr;
178
     mutable nodei_clock: Clocks.clock_expr;
179
     nodei_inputs: var_decl list;
180
     nodei_outputs: var_decl list;
181
     nodei_stateless: bool;
182
     nodei_spec: node_annot option;
183
     nodei_prototype: string option;
184
     nodei_in_lib: string option;
185
    }
186

    
187
type const_desc = 
188
    {const_id: ident; 
189
     const_loc: Location.t; 
190
     const_value: constant;      
191
     mutable const_type: Types.type_expr;
192
    }
193

    
194
type top_decl_desc =
195
| Node of node_desc
196
| Const of const_desc
197
| ImportedNode of imported_node_desc
198
| Open of bool * string (* the boolean set to true denotes a local 
199
			   lusi vs a lusi installed at system level *)
200
| TypeDef of typedef_desc
201

    
202
type top_decl =
203
    {top_decl_desc: top_decl_desc;      (* description of the symbol *)
204
     top_decl_owner: Location.filename; (* the module where it is defined *)
205
     top_decl_itf: bool;                (* header or source file ? *)
206
     top_decl_loc: Location.t}          (* the location where it is defined *)
207

    
208
type program = top_decl list
209

    
210
type dep_t = Dep of 
211
    bool 
212
  * ident
213
  * (top_decl list) 
214
  * bool (* is stateful *)
215

    
216
type error =
217
    Main_not_found
218
  | Main_wrong_kind
219
  | No_main_specified
220
  | Unbound_symbol of ident
221
  | Already_bound_symbol of ident
222
  | Unknown_library of ident
223

    
224
(* Local Variables: *)
225
(* compile-command:"make -C .." *)
226
(* End: *)