blob: 180608c43d471989550ff895f0a4f5b1c0207314 (
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
|
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
| AST_NOT
| AST_PRE
type binary_op =
| AST_PLUS
| AST_MINUS
| AST_MUL
| AST_DIV
| AST_MOD
| AST_EQ
| AST_NE
| AST_LT
| AST_LE
| AST_GT
| AST_GE
| AST_AND
| AST_OR
| AST_ARROW
type expr =
| AST_unary of unary_op * (expr ext)
| AST_binary of binary_op * (expr ext) * (expr ext)
| AST_identifier of id ext
| AST_int_const of string ext
| AST_bool_const of bool
| AST_real_const of string ext
| AST_if of (expr ext) * (expr ext) * (expr ext)
| AST_instance of (id ext) * (expr ext list)
type lvalue = id
type eqn =
| AST_assign of (lvalue ext) * (expr ext)
| AST_guarantee of (id ext) * (expr ext)
| AST_assume of (id ext) * (expr ext)
(* and more : automaton, activate... *)
type node_decl = {
name : id;
args : (bool * (id ext) * typ) list;
ret : (bool * (id ext) * typ) list;
var : (bool * (id ext) * typ) list;
body : eqn ext list;
}
type const_decl = (id ext) * typ * (expr ext)
type toplevel =
| AST_node_decl of node_decl ext
| AST_const_decl of const_decl ext
type prog = toplevel list
|
