lustrec / src / lustreSpec.ml @ e2380d4d
History | View | Annotate | Download (2.88 KB)
1 |
open Format |
---|---|
2 |
|
3 |
|
4 |
let merge_expr_annot ann1 ann2 = |
5 |
match ann1, ann2 with |
6 |
| None, None -> assert false |
7 |
| Some _, None -> ann1 |
8 |
| None, Some _ -> ann2 |
9 |
| Some ann1, Some ann2 -> Some (ann1@ann2) |
10 |
|
11 |
|
12 |
type ident = Utils.ident |
13 |
type rat = Utils.rat |
14 |
type tag = Utils.tag |
15 |
|
16 |
type constant = |
17 |
| EConst_int of int |
18 |
| EConst_real of string |
19 |
| EConst_float of float |
20 |
| EConst_bool of bool |
21 |
| EConst_string of string |
22 |
|
23 |
type type_dec = |
24 |
{ty_dec_desc: type_dec_desc; |
25 |
ty_dec_loc: Location.t} |
26 |
|
27 |
and type_dec_desc = |
28 |
| Tydec_any |
29 |
| Tydec_int |
30 |
| Tydec_real |
31 |
| Tydec_float |
32 |
| Tydec_bool |
33 |
| Tydec_clock of type_dec_desc |
34 |
| Tydec_const of ident |
35 |
| Tydec_enum of ident list |
36 |
| Tydec_array of Dimension.dim_expr * type_dec_desc |
37 |
|
38 |
type clock_dec = |
39 |
{ck_dec_desc: clock_dec_desc; |
40 |
ck_dec_loc: Location.t} |
41 |
|
42 |
and clock_dec_desc = |
43 |
| Ckdec_any |
44 |
| Ckdec_bool of (ident * ident) list |
45 |
| Ckdec_pclock of int * rat |
46 |
|
47 |
type var_decl = |
48 |
{var_id: ident; |
49 |
var_dec_type: type_dec; |
50 |
var_dec_clock: clock_dec; |
51 |
var_dec_const: bool; |
52 |
mutable var_type: Types.type_expr; |
53 |
mutable var_clock: Clocks.clock_expr; |
54 |
var_loc: Location.t} |
55 |
|
56 |
(* The tag of an expression is a unique identifier used to distinguish |
57 |
different instances of the same node *) |
58 |
type eexpr = |
59 |
{eexpr_tag: tag; |
60 |
eexpr_desc: eexpr_desc; |
61 |
mutable eexpr_type: Types.type_expr; |
62 |
mutable eexpr_clock: Clocks.clock_expr; |
63 |
eexpr_loc: Location.t} |
64 |
|
65 |
and eexpr_desc = |
66 |
| EExpr_const of constant |
67 |
| EExpr_ident of ident |
68 |
| EExpr_tuple of eexpr list |
69 |
| EExpr_arrow of eexpr * eexpr |
70 |
| EExpr_fby of eexpr * eexpr |
71 |
(* | EExpr_concat of eexpr * eexpr *) |
72 |
(* | EExpr_tail of eexpr *) |
73 |
| EExpr_pre of eexpr |
74 |
| EExpr_when of eexpr * ident |
75 |
(* | EExpr_whennot of eexpr * ident *) |
76 |
| EExpr_merge of ident * eexpr * eexpr |
77 |
| EExpr_appl of ident * eexpr * ident option |
78 |
(* | EExpr_uclock of eexpr * int *) |
79 |
(* | EExpr_dclock of eexpr * int *) |
80 |
(* | EExpr_phclock of eexpr * rat *) |
81 |
| EExpr_exists of var_decl list * eexpr |
82 |
| EExpr_forall of var_decl list * eexpr |
83 |
|
84 |
type ensures_t = EnsuresExpr of eexpr | SpecObserverNode of (string * eexpr list) |
85 |
|
86 |
type node_annot = { |
87 |
requires: eexpr list; |
88 |
ensures: ensures_t list; |
89 |
behaviors: (string * eexpr list * ensures_t list) list |
90 |
} |
91 |
|
92 |
|
93 |
type expr_annot = (string list * eexpr) list |
94 |
|
95 |
let merge_node_annot ann1 ann2 = |
96 |
{ requires = ann1.requires @ ann2.requires; |
97 |
ensures = ann1.ensures @ ann2.ensures; |
98 |
behaviors = ann1.behaviors @ ann2.behaviors; |
99 |
} |
100 |
|
101 |
let mkeexpr loc d = |
102 |
{ eexpr_tag = Utils.new_tag (); |
103 |
eexpr_desc = d; |
104 |
eexpr_type = Types.new_var (); |
105 |
eexpr_clock = Clocks.new_var true; |
106 |
eexpr_loc = loc } |
107 |
|
108 |
let mkepredef_call loc funname args = |
109 |
mkeexpr loc (EExpr_appl (funname, mkeexpr loc (EExpr_tuple args), None)) |
110 |
|
111 |
let mkepredef_unary_call loc funname arg = |
112 |
mkeexpr loc (EExpr_appl (funname, arg, None)) |
113 |
|
114 |
(* Local Variables: *) |
115 |
(* compile-command:"make -C .." *) |
116 |
(* End: *) |