Source file expr_interpreter.ml
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
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
let value_state_alg_op counter ?(time = Counter.current_time counter) = function
| Operator.CPUTIME -> Nbr.F (Sys.time ())
| Operator.TIME_VAR -> Nbr.F time
| Operator.EVENT_VAR -> Nbr.I (Counter.current_event counter)
| Operator.NULL_EVENT_VAR -> Nbr.I (Counter.nb_null_event counter)
| Operator.EMAX_VAR ->
(match Counter.max_events counter with
| Some n -> Nbr.I n
| None -> Nbr.F infinity)
| Operator.TMAX_VAR ->
(match Counter.max_time counter with
| Some t -> Nbr.F t
| None -> Nbr.F infinity)
type (_, _) stack =
| RETURN : ('a, 'a) stack
| TO_EXEC_ALG :
Operator.bin_alg_op * Primitives.alg_expr * (Nbr.t, 'a) stack
-> (Nbr.t, 'a) stack
| TO_EXEC_COMP :
Operator.compare_op * Primitives.alg_expr * (bool, 'a) stack
-> (Nbr.t, 'a) stack
| TO_EXEC_IF :
Primitives.alg_expr * Primitives.alg_expr * (Nbr.t, 'a) stack
-> (bool, 'a) stack
| TO_EXEC_BOOL :
Operator.bin_bool_op
* (Pattern.id array list, int) Alg_expr.bool
* (bool, 'a) stack
-> (bool, 'a) stack
| TO_COMPUTE_ALG :
Operator.bin_alg_op * Nbr.t * (Nbr.t, 'a) stack
-> (Nbr.t, 'a) stack
| TO_COMPUTE_COMP :
Operator.compare_op * Nbr.t * (bool, 'a) stack
-> (Nbr.t, 'a) stack
| TO_COMPUTE_UN : Operator.un_alg_op * (Nbr.t, 'a) stack -> (Nbr.t, 'a) stack
| TO_COMPUTE_BOOL : Operator.un_bool_op * (bool, 'a) stack -> (bool, 'a) stack
let rec exec_alg :
type a.
Counter.t ->
?time:float ->
get_alg:(int -> Primitives.alg_expr) ->
get_mix:(Pattern.id array list -> Nbr.t) ->
get_tok:(int -> Nbr.t) ->
(Pattern.id array list, int) Alg_expr.e ->
(Nbr.t, a) stack ->
a =
fun counter ?time ~get_alg ~get_mix ~get_tok alg sk ->
match alg with
| Alg_expr.BIN_ALG_OP (op, (a, _), (b, _)) ->
exec_alg counter ?time ~get_alg ~get_mix ~get_tok a
(TO_EXEC_ALG (op, b, sk))
| Alg_expr.UN_ALG_OP (op, (a, _)) ->
exec_alg counter ?time ~get_alg ~get_mix ~get_tok a (TO_COMPUTE_UN (op, sk))
| Alg_expr.STATE_ALG_OP op ->
with_value counter ?time ~get_alg ~get_mix ~get_tok
(value_state_alg_op counter ?time op)
sk
| Alg_expr.ALG_VAR i ->
exec_alg counter ?time ~get_alg ~get_mix ~get_tok (get_alg i) sk
| Alg_expr.KAPPA_INSTANCE ccs ->
with_value counter ?time ~get_alg ~get_mix ~get_tok (get_mix ccs) sk
| Alg_expr.TOKEN_ID i ->
with_value counter ?time ~get_alg ~get_mix ~get_tok (get_tok i) sk
| Alg_expr.CONST n -> with_value counter ?time ~get_alg ~get_mix ~get_tok n sk
| Alg_expr.IF ((cond, _), (yes, _), (no, _)) ->
exec_bool counter ?time ~get_alg ~get_mix ~get_tok cond
(TO_EXEC_IF (yes, no, sk))
| Alg_expr.DIFF_TOKEN _ | Alg_expr.DIFF_KAPPA_INSTANCE _ ->
raise
(ExceptionDefn.Internal_Error
("Cannot evalutate derivatives in expression", Loc.dummy))
and exec_bool :
type a.
Counter.t ->
?time:float ->
get_alg:(int -> Primitives.alg_expr) ->
get_mix:(Pattern.id array list -> Nbr.t) ->
get_tok:(int -> Nbr.t) ->
(Pattern.id array list, int) Alg_expr.bool ->
(bool, a) stack ->
a =
fun counter ?time ~get_alg ~get_mix ~get_tok expr sk ->
match expr with
| Alg_expr.TRUE -> with_value counter ?time ~get_alg ~get_mix ~get_tok true sk
| Alg_expr.FALSE ->
with_value counter ?time ~get_alg ~get_mix ~get_tok false sk
| Alg_expr.UN_BOOL_OP (op, (a, _)) ->
exec_bool counter ?time ~get_alg ~get_mix ~get_tok a
(TO_COMPUTE_BOOL (op, sk))
| Alg_expr.BIN_BOOL_OP (op, (a, _), (b, _)) ->
exec_bool counter ?time ~get_alg ~get_mix ~get_tok a
(TO_EXEC_BOOL (op, b, sk))
| Alg_expr.COMPARE_OP (op, (a, _), (b, _)) ->
exec_alg counter ?time ~get_alg ~get_mix ~get_tok a
(TO_EXEC_COMP (op, b, sk))
and with_value :
type a b.
Counter.t ->
?time:float ->
get_alg:(int -> Primitives.alg_expr) ->
get_mix:(Pattern.id array list -> Nbr.t) ->
get_tok:(int -> Nbr.t) ->
a ->
(a, b) stack ->
b =
fun counter ?time ~get_alg ~get_mix ~get_tok n -> function
| RETURN -> n
| TO_EXEC_ALG (op, alg, sk) ->
exec_alg counter ?time ~get_alg ~get_mix ~get_tok alg
(TO_COMPUTE_ALG (op, n, sk))
| TO_COMPUTE_ALG (op, n1, sk) ->
with_value counter ?time ~get_alg ~get_mix ~get_tok
(Nbr.of_bin_alg_op op n1 n)
sk
| TO_COMPUTE_UN (op, sk) ->
with_value counter ?time ~get_alg ~get_mix ~get_tok (Nbr.of_un_alg_op op n)
sk
| TO_EXEC_COMP (op, alg, sk) ->
exec_alg counter ?time ~get_alg ~get_mix ~get_tok alg
(TO_COMPUTE_COMP (op, n, sk))
| TO_COMPUTE_COMP (op, n1, sk) ->
with_value counter ?time ~get_alg ~get_mix ~get_tok
(Nbr.of_compare_op op n1 n)
sk
| TO_EXEC_IF (yes, no, sk) ->
exec_alg counter ?time ~get_alg ~get_mix ~get_tok
(if n then
yes
else
no)
sk
| TO_EXEC_BOOL (Operator.OR, _, sk) when n ->
with_value counter ?time ~get_alg ~get_mix ~get_tok true sk
| TO_EXEC_BOOL (Operator.AND, _, sk) when not n ->
with_value counter ?time ~get_alg ~get_mix ~get_tok false sk
| TO_EXEC_BOOL ((Operator.OR | Operator.AND), expr, sk) ->
exec_bool counter ?time ~get_alg ~get_mix ~get_tok expr sk
| TO_COMPUTE_BOOL (Operator.NOT, sk) ->
with_value counter ?time ~get_alg ~get_mix ~get_tok (not n) sk
let value_bool counter ?time ~get_alg ~get_mix ~get_tok expr =
exec_bool counter ?time ~get_alg ~get_mix ~get_tok expr RETURN
let value_alg counter ?time ~get_alg ~get_mix ~get_tok alg =
exec_alg counter ?time ~get_alg ~get_mix ~get_tok alg RETURN