Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec / src / lustreSpec.ml @ 36454535

History | View | Annotate | Download (4.7 KB)

1
open Format
2

    
3
type ident = Utils.ident
4
type rat = Utils.rat
5
type tag = Utils.tag
6
type label = Utils.ident
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
  | Tydec_struct of (ident * type_dec_desc) list
22
  | 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
(** 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
(* The tag of an expression is a unique identifier used to distinguish
62
   different instances of the same node *)
63
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
    {eexpr_tag: tag;
93
     eexpr_qfexpr: expr;
94
     eexpr_quantifiers: (quantifier_type * var_decl list) list;
95
     mutable eexpr_type: Types.type_expr;
96
     mutable eexpr_clock: Clocks.clock_expr;
97
     mutable eexpr_normalized: (var_decl * eq list * var_decl list) option;
98
     eexpr_loc: Location.t}
99

    
100
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

    
111
type node_annot = {
112
  requires: eexpr list;
113
  ensures: eexpr list;
114
  behaviors: (string * eexpr list * eexpr list * Location.t) list;
115
  spec_loc: Location.t;
116
}
117
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

    
179

    
180
(* Local Variables: *)
181
(* compile-command:"make -C .." *)
182
(* End: *)