Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec / src / lustreSpec.ml @ 01c7d5e1

History | View | Annotate | Download (4.7 KB)

1 22fe1c93 ploc
open Format
2
3
type ident = Utils.ident
4 01c7d5e1 ploc
type label = Utils.ident
5 22fe1c93 ploc
type rat = Utils.rat
6
type tag = Utils.tag
7
8
type type_dec =
9
    {ty_dec_desc: type_dec_desc;
10
     ty_dec_loc: Location.t}
11
12
and type_dec_desc =
13
  | Tydec_any
14
  | Tydec_int
15
  | Tydec_real
16
  | Tydec_float
17
  | Tydec_bool
18
  | Tydec_clock of type_dec_desc
19
  | Tydec_const of ident
20
  | Tydec_enum of ident list
21 6a6abd76 xthirioux
  | Tydec_struct of (ident * type_dec_desc) list
22 22fe1c93 ploc
  | Tydec_array of Dimension.dim_expr * type_dec_desc
23
24
type clock_dec =
25
    {ck_dec_desc: clock_dec_desc;
26
     ck_dec_loc: Location.t}
27
28
and clock_dec_desc =
29
  | Ckdec_any
30
  | Ckdec_bool of (ident * ident) list 
31
  | Ckdec_pclock of int * rat
32
33
type var_decl = 
34
    {var_id: ident;
35
     var_dec_type: type_dec;
36
     var_dec_clock: clock_dec;
37
     var_dec_const: bool;
38
     mutable var_type: Types.type_expr;
39
     mutable var_clock: Clocks.clock_expr;
40
     var_loc: Location.t}
41
42 01c7d5e1 ploc
(** The core language and its ast. Every element of the ast contains its
43
    location in the program text. The type and clock of an ast element
44
    is mutable (and initialized to dummy values). This avoids to have to
45
    duplicate ast structures (e.g. ast, typed_ast, clocked_ast). *)
46
47
48
type constant =
49
  | Const_int of int
50
  | Const_real of string
51
  | Const_float of float
52
  | Const_array of constant list
53
  | Const_tag of label
54
  | Const_string of string (* used only for annotations *)
55
  | Const_struct of (label * constant) list
56
57
type quantifier_type = Exists | Forall
58
59
60
61 22fe1c93 ploc
(* The tag of an expression is a unique identifier used to distinguish
62
   different instances of the same node *)
63 01c7d5e1 ploc
type expr =
64
    {expr_tag: tag;
65
     expr_desc: expr_desc;
66
     mutable expr_type: Types.type_expr;
67
     mutable expr_clock: Clocks.clock_expr;
68
     mutable expr_delay: Delay.delay_expr;
69
     mutable expr_annot: expr_annot option;
70
     expr_loc: Location.t}
71
72
and expr_desc =
73
  | Expr_const of constant
74
  | Expr_ident of ident
75
  | Expr_tuple of expr list
76
  | Expr_ite   of expr * expr * expr
77
  | Expr_arrow of expr * expr
78
  | Expr_fby of expr * expr
79
  | Expr_array of expr list
80
  | Expr_access of expr * Dimension.dim_expr
81
  | Expr_power of expr * Dimension.dim_expr
82
  | Expr_pre of expr
83
  | Expr_when of expr * ident * label
84
  | Expr_merge of ident * (label * expr) list
85
  | Expr_appl of call_t
86
 and call_t = ident * expr * (ident * label) option 
87
     (* The third part denotes the reseting clock label and value *)
88
and 
89
  (* The tag of an expression is a unique identifier used to distinguish
90
     different instances of the same node *)
91
  eexpr =
92 22fe1c93 ploc
    {eexpr_tag: tag;
93 01c7d5e1 ploc
     eexpr_qfexpr: expr;
94
     eexpr_quantifiers: (quantifier_type * var_decl list) list;
95 22fe1c93 ploc
     mutable eexpr_type: Types.type_expr;
96
     mutable eexpr_clock: Clocks.clock_expr;
97 01c7d5e1 ploc
     mutable eexpr_normalized: (var_decl * eq list * var_decl list) option;
98 22fe1c93 ploc
     eexpr_loc: Location.t}
99
100 01c7d5e1 ploc
and expr_annot = {
101
  annots: (string list * eexpr) list;
102
  annot_loc: Location.t
103
}
104
and 
105
 eq =
106
    {eq_lhs: ident list;
107
     eq_rhs: expr;
108
     eq_loc: Location.t}
109
110 22fe1c93 ploc
111
type node_annot = {
112
  requires: eexpr list;
113 01c7d5e1 ploc
  ensures: eexpr list;
114
  behaviors: (string * eexpr list * eexpr list * Location.t) list;
115
  spec_loc: Location.t;
116 22fe1c93 ploc
}
117 01c7d5e1 ploc
type assert_t = 
118
    {
119
      assert_expr: expr;
120
      assert_loc: Location.t
121
    } 
122
123
type node_desc =
124
    {node_id: ident;
125
     mutable node_type: Types.type_expr;
126
     mutable node_clock: Clocks.clock_expr;
127
     node_inputs: var_decl list;
128
     node_outputs: var_decl list;
129
     node_locals: var_decl list;
130
     mutable node_gencalls: expr list;
131
     mutable node_checks: Dimension.dim_expr list;
132
     node_asserts: assert_t list; 
133
     node_eqs: eq list;
134
     mutable node_dec_stateless: bool;
135
     mutable node_stateless: bool option;
136
     node_spec: node_annot option;
137
     node_annot: expr_annot list;
138
    }
139
140
type imported_node_desc =
141
    {nodei_id: ident;
142
     mutable nodei_type: Types.type_expr;
143
     mutable nodei_clock: Clocks.clock_expr;
144
     nodei_inputs: var_decl list;
145
     nodei_outputs: var_decl list;
146
     nodei_stateless: bool;
147
     nodei_spec: node_annot option;
148
     nodei_prototype: string option;
149
     nodei_in_lib: string option;
150
    }
151
152
type const_desc = 
153
    {const_id: ident; 
154
     const_loc: Location.t; 
155
     const_value: constant;      
156
     mutable const_type: Types.type_expr;
157
    }
158
159
type top_decl_desc =
160
| Node of node_desc
161
| Consts of const_desc list
162
| ImportedNode of imported_node_desc
163
| Open of bool * string (* the boolean set to true denotes a local 
164
			   lusi vs a lusi installed at system level *)
165
166
type top_decl =
167
    {top_decl_desc: top_decl_desc;
168
     top_decl_loc: Location.t}
169
170
type program = top_decl list
171
172
type error =
173
    Main_not_found
174
  | Main_wrong_kind
175
  | No_main_specified
176
  | Unbound_symbol of ident
177
  | Already_bound_symbol of ident
178 22fe1c93 ploc
179
180
181
(* Local Variables: *)
182
(* compile-command:"make -C .." *)
183
(* End: *)