blob: 50fa3f4e5ee0efcd818d95677805cc5ee1e96e78 (
plain) (
blame)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
|
open Lexing
type position = Lexing.position
let position_unknown = Lexing.dummy_pos
type extent = position * position
let extent_unknown = (position_unknown, position_unknown)
type 'a ext = 'a * extent
type id = string
type typ =
| AST_TINT
| AST_TBOOL
| AST_TREAL
type unary_op =
| AST_UPLUS
| AST_UMINUS
type binary_op =
(* num * num -> num *)
| AST_PLUS
| AST_MINUS
| AST_MUL
| AST_DIV
| AST_MOD
type binary_rel_op =
(* 'a * 'a -> bool *)
| AST_EQ
| AST_NE
(* num * num -> bool *)
| AST_LT
| AST_LE
| AST_GT
| AST_GE
type bin_bool_op =
(* bool * bool -> bool *)
| AST_AND
| AST_OR
type expr =
| AST_identifier of id ext
(* on numerical values *)
| AST_int_const of string ext
| AST_real_const of string ext
| AST_unary of unary_op * (expr ext)
| AST_binary of binary_op * (expr ext) * (expr ext)
(* on boolean values *)
| AST_bool_const of bool
| AST_binary_rel of binary_rel_op * (expr ext) * (expr ext)
| AST_binary_bool of bin_bool_op * (expr ext) * (expr ext)
| AST_not of expr ext
(* temporal primitives *)
| AST_pre of expr ext * id
| AST_arrow of (expr ext) * (expr ext)
(* other *)
| AST_if of (expr ext) * (expr ext) * (expr ext)
| AST_instance of (id ext) * (expr ext list) * id
type var_def = bool * (id ext) * typ
type automaton = id * state ext list * id list
and state = {
initial : bool;
name : id;
locals : var_def list;
body : eqn ext list;
until : transition list;
}
and transition = (expr ext) * (id ext)
and eqn =
| AST_assign of (id ext list) * (expr ext)
| AST_guarantee of (id ext) * (expr ext)
| AST_assume of (id ext) * (expr ext)
| AST_automaton of automaton
type node_decl = {
name : id;
args : var_def list;
ret : var_def list;
var : var_def list;
body : eqn ext list;
}
type const_decl = {
name : id;
typ : typ;
value : expr ext;
}
type toplevel =
| AST_node_decl of node_decl ext
| AST_const_decl of const_decl ext
type prog = toplevel list
|
