summaryrefslogtreecommitdiff
path: root/frontend/ast.ml
blob: d55626d048ac5bee9c80f54d2d892047c8ad2d3f (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
102
103
104
105
106
107
108
109
110
111
open Lexing
open Util


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
    | AST_idconst     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)
    | AST_cast        of (expr ext) * typ
    (* 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
    | AST_tuple       of expr ext list

type var_def = bool * id * typ

type automaton = id * state ext list * id list
and  state = {
    initial   : bool;
    st_name   : id;
    st_locals : var_def list;
    body      : eqn ext list;
    until     : transition list;
}
and transition = (expr ext) * (id ext) * bool   (* bool : does it reset ? *)

and activate_block = {
    act_id     : id;
    act_locals : var_def list;
    body       : eqn ext list;
}
and activate_if =
    | AST_activate_body of activate_block
    | AST_activate_if of expr ext * activate_if * activate_if
and activate = activate_if * id list

and eqn =
    | AST_assign     of (id ext list) * (expr ext)
    | AST_assume     of (id ext) * (expr ext)
    | AST_guarantee  of (id ext) * (expr ext)
    | AST_automaton  of automaton
    | AST_activate   of activate

type node_decl = {
    n_name : id;
    args   : var_def list;
    ret    : var_def list;
    var    : var_def list;
    body   : eqn ext list;
}

type const_decl = {
    c_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