1
|
open Basetypes
|
2
|
|
3
|
(* open ActiveEnv *)
|
4
|
open CPS_transformer
|
5
|
|
6
|
(* open Datatype *)
|
7
|
(* open Simulink *)
|
8
|
|
9
|
(* Theta functions interfaces including memoization when using modular calls
|
10
|
|
11
|
parametrized by the transformer specifying the type of the continuation.
|
12
|
Evaluation of actions is also continuation dependent. *)
|
13
|
|
14
|
module KenvTheta (T : TransformerType) = struct
|
15
|
type kenv_t = {
|
16
|
cont_node :
|
17
|
(path_t
|
18
|
* ((kenv_t -> path_t -> frontier_t -> T.t)
|
19
|
* (kenv_t -> T.t)
|
20
|
* (kenv_t -> frontier_t -> T.t)))
|
21
|
list;
|
22
|
cont_junc :
|
23
|
(junction_name_t
|
24
|
* (kenv_t -> T.t wrapper_t -> T.t success_t -> T.t fail_t -> T.t))
|
25
|
list;
|
26
|
}
|
27
|
|
28
|
let init_env src =
|
29
|
List.fold_left
|
30
|
(fun accu d ->
|
31
|
match d with
|
32
|
| Datatype.State (p, _) ->
|
33
|
ActiveStates.Env.add p false accu
|
34
|
| _ ->
|
35
|
accu)
|
36
|
ActiveStates.Env.empty src
|
37
|
|
38
|
module type KenvType = sig
|
39
|
val kenv : kenv_t
|
40
|
end
|
41
|
|
42
|
module type MemoThetaTablesType = sig
|
43
|
val tables : 'c call_t -> ('c, T.t) Memo.t
|
44
|
end
|
45
|
|
46
|
module type MemoThetaType = sig
|
47
|
include ThetaType with type t = T.t
|
48
|
|
49
|
val components : 'c call_t -> ('c * t) list
|
50
|
end
|
51
|
|
52
|
module type ModularType = sig
|
53
|
val modular : (path_t, 'b, bool) tag_t -> path_t -> 'b
|
54
|
end
|
55
|
|
56
|
module MemoThetaTables : functor () -> MemoThetaTablesType =
|
57
|
functor
|
58
|
()
|
59
|
->
|
60
|
struct
|
61
|
let table_theta_e =
|
62
|
(Memo.create () : (path_t * path_t * frontier_t, T.t) Memo.t)
|
63
|
|
64
|
let table_theta_d = (Memo.create () : (path_t, T.t) Memo.t)
|
65
|
|
66
|
let table_theta_x = (Memo.create () : (path_t * frontier_t, T.t) Memo.t)
|
67
|
|
68
|
let tables : type c. c call_t -> (c, T.t) Memo.t =
|
69
|
fun call ->
|
70
|
match call with
|
71
|
| Ecall ->
|
72
|
table_theta_e
|
73
|
| Dcall ->
|
74
|
table_theta_d
|
75
|
| Xcall ->
|
76
|
table_theta_x
|
77
|
end
|
78
|
|
79
|
module Memoize
|
80
|
(Tables : MemoThetaTablesType)
|
81
|
(Theta : ThetaType with type t = T.t) : MemoThetaType = struct
|
82
|
type t = Theta.t
|
83
|
|
84
|
let components call =
|
85
|
Memo.fold (Tables.tables call) (fun k v res -> (k, v) :: res) []
|
86
|
|
87
|
let theta : type a b. (a, b, t) theta_t =
|
88
|
fun tag ->
|
89
|
match tag with
|
90
|
| J ->
|
91
|
Theta.theta J
|
92
|
| E ->
|
93
|
Memo.apply3 (Tables.tables Ecall) (Theta.theta E)
|
94
|
| D ->
|
95
|
Memo.apply (Tables.tables Dcall) (Theta.theta D)
|
96
|
| X ->
|
97
|
Memo.apply2 (Tables.tables Xcall) (Theta.theta X)
|
98
|
end
|
99
|
|
100
|
module Modularize (Mod : ModularType) (Theta : MemoThetaType) :
|
101
|
MemoThetaType = struct
|
102
|
type t = Theta.t
|
103
|
|
104
|
let mod_theta = (module Theta : ThetaType with type t = T.t)
|
105
|
|
106
|
let components : type c. c call_t -> (c * t) list =
|
107
|
fun call ->
|
108
|
match call with
|
109
|
| Ecall ->
|
110
|
List.filter
|
111
|
(fun ((p, p', f), _) -> Mod.modular E p p' f)
|
112
|
(Theta.components Ecall)
|
113
|
| Dcall ->
|
114
|
List.filter (fun (p, _) -> Mod.modular D p) (Theta.components Dcall)
|
115
|
| Xcall ->
|
116
|
List.filter
|
117
|
(fun ((p, f), _) -> Mod.modular X p f)
|
118
|
(Theta.components Xcall)
|
119
|
|
120
|
let theta : type a b. (a, b, t) theta_t =
|
121
|
fun tag ->
|
122
|
match tag with
|
123
|
| J ->
|
124
|
Theta.theta tag
|
125
|
| E ->
|
126
|
fun p p' f ->
|
127
|
let theta_e = Theta.theta tag p p' f in
|
128
|
if Mod.modular E p p' f then
|
129
|
T.(eval_act mod_theta (call Ecall (p, p', f)))
|
130
|
else theta_e
|
131
|
| D ->
|
132
|
fun p ->
|
133
|
let theta_d = Theta.theta tag p in
|
134
|
if Mod.modular D p then T.(eval_act mod_theta (call Dcall p))
|
135
|
else theta_d
|
136
|
| X ->
|
137
|
fun p f ->
|
138
|
let theta_x = Theta.theta tag p f in
|
139
|
if Mod.modular X p f then T.(eval_act mod_theta (call Xcall (p, f)))
|
140
|
else theta_x
|
141
|
end
|
142
|
|
143
|
module type ThetaifyType = functor (Kenv : KenvType) -> MemoThetaType
|
144
|
|
145
|
module BasicThetaify : ThetaifyType =
|
146
|
functor
|
147
|
(Kenv : KenvType)
|
148
|
->
|
149
|
struct
|
150
|
type t = T.t
|
151
|
|
152
|
let theta_ify : type a b. kenv_t -> (a, b, T.t) theta_t =
|
153
|
fun kenv tag ->
|
154
|
match tag with
|
155
|
| J -> (
|
156
|
fun j ->
|
157
|
try List.assoc j kenv.cont_junc kenv
|
158
|
with Not_found ->
|
159
|
Format.eprintf "Lost junction %a@ " pp_junction_name j;
|
160
|
assert false)
|
161
|
| E -> (
|
162
|
fun p ->
|
163
|
try
|
164
|
let e, _, _ = List.assoc p kenv.cont_node in
|
165
|
e kenv
|
166
|
with Not_found ->
|
167
|
Format.eprintf "Entering lost path [%a]@." pp_path p;
|
168
|
assert false)
|
169
|
| D -> (
|
170
|
fun p ->
|
171
|
try
|
172
|
let _, d, _ = List.assoc p kenv.cont_node in
|
173
|
d kenv
|
174
|
with Not_found ->
|
175
|
Format.eprintf "During lost path [%a]@." pp_path p;
|
176
|
assert false)
|
177
|
| X -> (
|
178
|
fun p ->
|
179
|
try
|
180
|
let _, _, x = List.assoc p kenv.cont_node in
|
181
|
x kenv
|
182
|
with Not_found ->
|
183
|
Format.eprintf "Exiting lost path [%a]@." pp_path p;
|
184
|
assert false)
|
185
|
|
186
|
let theta tag = theta_ify Kenv.kenv tag
|
187
|
|
188
|
let components _call = []
|
189
|
end
|
190
|
|
191
|
module ModularThetaify : functor
|
192
|
(Tables : MemoThetaTablesType)
|
193
|
(Mod : ModularType)
|
194
|
-> ThetaifyType =
|
195
|
functor
|
196
|
(Tables : MemoThetaTablesType)
|
197
|
(Mod : ModularType)
|
198
|
(Kenv : KenvType)
|
199
|
->
|
200
|
Modularize (Mod) (Memoize (Tables) (BasicThetaify (Kenv)))
|
201
|
end
|