lustrec / src / lustreSpec.ml @ fa090c4e
History | View | Annotate | Download (2.93 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_struct of (ident * type_dec_desc) list *) |
37 |
| Tydec_array of Dimension.dim_expr * type_dec_desc |
38 |
|
39 |
type clock_dec = |
40 |
{ck_dec_desc: clock_dec_desc; |
41 |
ck_dec_loc: Location.t} |
42 |
|
43 |
and clock_dec_desc = |
44 |
| Ckdec_any |
45 |
| Ckdec_bool of (ident * ident) list |
46 |
| Ckdec_pclock of int * rat |
47 |
|
48 |
type var_decl = |
49 |
{var_id: ident; |
50 |
var_dec_type: type_dec; |
51 |
var_dec_clock: clock_dec; |
52 |
var_dec_const: bool; |
53 |
mutable var_type: Types.type_expr; |
54 |
mutable var_clock: Clocks.clock_expr; |
55 |
var_loc: Location.t} |
56 |
|
57 |
(* The tag of an expression is a unique identifier used to distinguish |
58 |
different instances of the same node *) |
59 |
type eexpr = |
60 |
{eexpr_tag: tag; |
61 |
eexpr_desc: eexpr_desc; |
62 |
mutable eexpr_type: Types.type_expr; |
63 |
mutable eexpr_clock: Clocks.clock_expr; |
64 |
eexpr_loc: Location.t} |
65 |
|
66 |
and eexpr_desc = |
67 |
| EExpr_const of constant |
68 |
| EExpr_ident of ident |
69 |
| EExpr_tuple of eexpr list |
70 |
| EExpr_arrow of eexpr * eexpr |
71 |
| EExpr_fby of eexpr * eexpr |
72 |
(* | EExpr_concat of eexpr * eexpr *) |
73 |
(* | EExpr_tail of eexpr *) |
74 |
| EExpr_pre of eexpr |
75 |
| EExpr_when of eexpr * ident |
76 |
(* | EExpr_whennot of eexpr * ident *) |
77 |
| EExpr_merge of ident * eexpr * eexpr |
78 |
| EExpr_appl of ident * eexpr * ident option |
79 |
(* | EExpr_uclock of eexpr * int *) |
80 |
(* | EExpr_dclock of eexpr * int *) |
81 |
(* | EExpr_phclock of eexpr * rat *) |
82 |
| EExpr_exists of var_decl list * eexpr |
83 |
| EExpr_forall of var_decl list * eexpr |
84 |
|
85 |
type ensures_t = EnsuresExpr of eexpr | SpecObserverNode of (string * eexpr list) |
86 |
|
87 |
type node_annot = { |
88 |
requires: eexpr list; |
89 |
ensures: ensures_t list; |
90 |
behaviors: (string * eexpr list * ensures_t list) list |
91 |
} |
92 |
|
93 |
|
94 |
type expr_annot = (string list * eexpr) list |
95 |
|
96 |
let merge_node_annot ann1 ann2 = |
97 |
{ requires = ann1.requires @ ann2.requires; |
98 |
ensures = ann1.ensures @ ann2.ensures; |
99 |
behaviors = ann1.behaviors @ ann2.behaviors; |
100 |
} |
101 |
|
102 |
let mkeexpr loc d = |
103 |
{ eexpr_tag = Utils.new_tag (); |
104 |
eexpr_desc = d; |
105 |
eexpr_type = Types.new_var (); |
106 |
eexpr_clock = Clocks.new_var true; |
107 |
eexpr_loc = loc } |
108 |
|
109 |
let mkepredef_call loc funname args = |
110 |
mkeexpr loc (EExpr_appl (funname, mkeexpr loc (EExpr_tuple args), None)) |
111 |
|
112 |
let mkepredef_unary_call loc funname arg = |
113 |
mkeexpr loc (EExpr_appl (funname, arg, None)) |
114 |
|
115 |
(* Local Variables: *) |
116 |
(* compile-command:"make -C .." *) |
117 |
(* End: *) |