Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec / src / lustreSpec.ml @ b38ffff3

History | View | Annotate | Download (5.4 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 clock_dec =
36
    {ck_dec_desc: clock_dec_desc;
37
     ck_dec_loc: Location.t}
38

    
39
and clock_dec_desc =
40
  | Ckdec_any
41
  | Ckdec_bool of (ident * ident) list 
42
  | Ckdec_pclock of int * rat
43

    
44
type var_decl = 
45
    {var_id: ident;
46
     var_dec_type: type_dec;
47
     var_dec_clock: clock_dec;
48
     var_dec_const: bool;
49
     mutable var_type: Types.type_expr;
50
     mutable var_clock: Clocks.clock_expr;
51
     var_loc: Location.t}
52

    
53
(** The core language and its ast. Every element of the ast contains its
54
    location in the program text. The type and clock of an ast element
55
    is mutable (and initialized to dummy values). This avoids to have to
56
    duplicate ast structures (e.g. ast, typed_ast, clocked_ast). *)
57

    
58

    
59
type constant =
60
  | Const_int of int
61
  | Const_real of string
62
  | Const_float of float
63
  | Const_array of constant list
64
  | Const_tag of label
65
  | Const_string of string (* used only for annotations *)
66
  | Const_struct of (label * constant) list
67

    
68
type quantifier_type = Exists | Forall
69

    
70

    
71

    
72
(* The tag of an expression is a unique identifier used to distinguish
73
   different instances of the same node *)
74
type expr =
75
    {expr_tag: tag;
76
     expr_desc: expr_desc;
77
     mutable expr_type: Types.type_expr;
78
     mutable expr_clock: Clocks.clock_expr;
79
     mutable expr_delay: Delay.delay_expr;
80
     mutable expr_annot: expr_annot option;
81
     expr_loc: Location.t}
82

    
83
and expr_desc =
84
  | Expr_const of constant
85
  | Expr_ident of ident
86
  | Expr_tuple of expr list
87
  | Expr_ite   of expr * expr * expr
88
  | Expr_arrow of expr * expr
89
  | Expr_fby of expr * expr
90
  | Expr_array of expr list
91
  | Expr_access of expr * Dimension.dim_expr
92
  | Expr_power of expr * Dimension.dim_expr
93
  | Expr_pre of expr
94
  | Expr_when of expr * ident * label
95
  | Expr_merge of ident * (label * expr) list
96
  | Expr_appl of call_t
97
 and call_t = ident * expr * (ident * label) option 
98
     (* The third part denotes the reseting clock label and value *)
99
and 
100
  (* The tag of an expression is a unique identifier used to distinguish
101
     different instances of the same node *)
102
  eexpr =
103
    {eexpr_tag: tag;
104
     eexpr_qfexpr: expr;
105
     eexpr_quantifiers: (quantifier_type * var_decl list) list;
106
     mutable eexpr_type: Types.type_expr;
107
     mutable eexpr_clock: Clocks.clock_expr;
108
     mutable eexpr_normalized: (var_decl * eq list * var_decl list) option;
109
     eexpr_loc: Location.t}
110

    
111
and expr_annot = {
112
  annots: (string list * eexpr) list;
113
  annot_loc: Location.t
114
}
115
and 
116
 eq =
117
    {eq_lhs: ident list;
118
     eq_rhs: expr;
119
     eq_loc: Location.t}
120

    
121

    
122
type node_annot = {
123
  requires: eexpr list;
124
  ensures: eexpr list;
125
  behaviors: (string * eexpr list * eexpr list * Location.t) list;
126
  spec_loc: Location.t;
127
}
128
type assert_t = 
129
    {
130
      assert_expr: expr;
131
      assert_loc: Location.t;
132
    } 
133

    
134
type node_desc =
135
    {node_id: ident;
136
     mutable node_type: Types.type_expr;
137
     mutable node_clock: Clocks.clock_expr;
138
     node_inputs: var_decl list;
139
     node_outputs: var_decl list;
140
     node_locals: var_decl list;
141
     mutable node_gencalls: expr list;
142
     mutable node_checks: Dimension.dim_expr list;
143
     node_asserts: assert_t list; 
144
     node_eqs: eq list;
145
     mutable node_dec_stateless: bool;
146
     mutable node_stateless: bool option;
147
     node_spec: node_annot option;
148
     node_annot: expr_annot list;
149
    }
150

    
151
type imported_node_desc =
152
    {nodei_id: ident;
153
     mutable nodei_type: Types.type_expr;
154
     mutable nodei_clock: Clocks.clock_expr;
155
     nodei_inputs: var_decl list;
156
     nodei_outputs: var_decl list;
157
     nodei_stateless: bool;
158
     nodei_spec: node_annot option;
159
     nodei_prototype: string option;
160
     nodei_in_lib: string option;
161
    }
162

    
163
type const_desc = 
164
    {const_id: ident; 
165
     const_loc: Location.t; 
166
     const_value: constant;      
167
     mutable const_type: Types.type_expr;
168
    }
169

    
170
type top_decl_desc =
171
| Node of node_desc
172
| Consts of const_desc list
173
| ImportedNode of imported_node_desc
174
| Open of bool * string (* the boolean set to true denotes a local 
175
			   lusi vs a lusi installed at system level *)
176

    
177
type top_decl =
178
    {top_decl_desc: top_decl_desc;
179
     top_decl_loc: Location.t}
180

    
181
type program = top_decl list
182

    
183
type error =
184
    Main_not_found
185
  | Main_wrong_kind
186
  | No_main_specified
187
  | Unbound_symbol of ident
188
  | Already_bound_symbol of ident
189

    
190

    
191
(* Local Variables: *)
192
(* compile-command:"make -C .." *)
193
(* End: *)