Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec / src / lustreSpec.ml @ 6aeb3388

History | View | Annotate | Download (5.49 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 type_def =
36
  {
37
    ty_def_id: ident;
38
    ty_def_desc: type_dec_desc}
39

    
40
type clock_dec =
41
    {ck_dec_desc: clock_dec_desc;
42
     ck_dec_loc: Location.t}
43

    
44
and clock_dec_desc =
45
  | Ckdec_any
46
  | Ckdec_bool of (ident * ident) list 
47
  | Ckdec_pclock of int * rat
48

    
49
type var_decl = 
50
    {var_id: ident;
51
     var_dec_type: type_dec;
52
     var_dec_clock: clock_dec;
53
     var_dec_const: bool;
54
     mutable var_type: Types.type_expr;
55
     mutable var_clock: Clocks.clock_expr;
56
     var_loc: Location.t}
57

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

    
63

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

    
73
type quantifier_type = Exists | Forall
74

    
75

    
76

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

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

    
116
and expr_annot = {
117
  annots: (string list * eexpr) list;
118
  annot_loc: Location.t
119
}
120
and 
121
 eq =
122
    {eq_lhs: ident list;
123
     eq_rhs: expr;
124
     eq_loc: Location.t}
125

    
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 node_desc =
140
    {node_id: ident;
141
     mutable node_type: Types.type_expr;
142
     mutable node_clock: Clocks.clock_expr;
143
     node_inputs: var_decl list;
144
     node_outputs: var_decl list;
145
     node_locals: var_decl list;
146
     mutable node_gencalls: expr list;
147
     mutable node_checks: Dimension.dim_expr list;
148
     node_asserts: assert_t list; 
149
     node_eqs: eq list;
150
     mutable node_dec_stateless: bool;
151
     mutable node_stateless: bool option;
152
     node_spec: node_annot option;
153
     node_annot: expr_annot list;
154
    }
155

    
156
type imported_node_desc =
157
    {nodei_id: ident;
158
     mutable nodei_type: Types.type_expr;
159
     mutable nodei_clock: Clocks.clock_expr;
160
     nodei_inputs: var_decl list;
161
     nodei_outputs: var_decl list;
162
     nodei_stateless: bool;
163
     nodei_spec: node_annot option;
164
     nodei_prototype: string option;
165
     nodei_in_lib: string option;
166
    }
167

    
168
type const_desc = 
169
    {const_id: ident; 
170
     const_loc: Location.t; 
171
     const_value: constant;      
172
     mutable const_type: Types.type_expr;
173
    }
174

    
175
type top_decl_desc =
176
| Node of node_desc
177
| Consts of const_desc list
178
| ImportedNode of imported_node_desc
179
| Open of bool * string (* the boolean set to true denotes a local 
180
			   lusi vs a lusi installed at system level *)
181
| Type of type_def
182

    
183
type top_decl =
184
    {top_decl_desc: top_decl_desc;
185
     top_decl_loc: Location.t}
186

    
187
type program = top_decl list
188

    
189
type error =
190
    Main_not_found
191
  | Main_wrong_kind
192
  | No_main_specified
193
  | Unbound_symbol of ident
194
  | Already_bound_symbol of ident
195

    
196

    
197
(* Local Variables: *)
198
(* compile-command:"make -C .." *)
199
(* End: *)