lustrec / tools / stateflow / src / semantics / CPS / theta.ml @ 2de7fa82
History  View  Annotate  Download (4.63 KB)
1 
open Basetypes 

2 
(* open ActiveEnv *) 
3 
open CPS_transformer 
4 
(* open Datatype *) 
5 
(* open Simulink *) 
6  
7 
(* Theta functions interfaces including memoization when using modular calls 
8 

9 
parametrized by the transformer specifying the type of the 
10 
continuation. Evaluation of actions is also continuation dependent. 
11 
*) 
12  
13 
module KenvTheta (T : TransformerType) = 
14 
struct 
15  
16 
type kenv_t = { 
17 
cont_node : ( 
18 
path_t * ( 
19 
(kenv_t > path_t > frontier_t > T.t) * 
20 
(kenv_t > T.t) * 
21 
(kenv_t > frontier_t > T.t) 
22 
) 
23 
) list; 
24 
cont_junc : ( 
25 
junction_name_t * ( 
26 
kenv_t > T.t wrapper_t > T.t success_t > T.t fail_t > T.t) 
27 
) list 
28 
} 
29  
30 

31 
let init_env src = 
32 
List.fold_left (fun accu d > 
33 
match d with 
34 
 Datatype.State (p, _) > ActiveStates.Env.add p false accu 
35 
 _ > accu) 
36 
ActiveStates.Env.empty 
37 
src 
38  
39 
module type KenvType = 
40 
sig 
41 
val kenv : kenv_t 
42 
end 
43  
44 
module type MemoThetaTablesType = 
45 
sig 
46 
val tables : 'c call_t > ('c, T.t) Memo.t 
47 
end 
48  
49 
module type MemoThetaType = 
50 
sig 
51 
include ThetaType with type t = T.t 
52 
val components : 'c call_t > ('c * t) list 
53 
end 
54  
55 
module type ModularType = 
56 
sig 
57 
val modular : (path_t, 'b, bool) tag_t > path_t > 'b 
58 
end 
59  
60 
module MemoThetaTables : functor () > MemoThetaTablesType = functor () > 
61 
struct 
62 
let table_theta_e = (Memo.create () : (path_t * path_t * frontier_t, T.t) Memo.t) 
63 
let table_theta_d = (Memo.create () : (path_t, T.t) Memo.t) 
64 
let table_theta_x = (Memo.create () : (path_t * frontier_t, T.t) Memo.t) 
65  
66 
let tables : type c. c call_t > (c, T.t) Memo.t = 
67 
fun call > 
68 
match call with 
69 
 Ecall > table_theta_e 
70 
 Dcall > table_theta_d 
71 
 Xcall > table_theta_x 
72 
end 
73  
74 
module Memoize (Tables : MemoThetaTablesType) (Theta : ThetaType with type t = T.t) : MemoThetaType = 
75 
struct 
76 
type t = Theta.t 
77  
78 
let components call = 
79 
Memo.fold (Tables.tables call) (fun k v res > (k, v)::res) [] 
80  
81 
let theta : type a b. (a, b, t) theta_t = 
82 
fun tag > 
83 
match tag with 
84 
 J > Theta.theta J 
85 
 E > Memo.apply3 (Tables.tables Ecall) (Theta.theta E) 
86 
 D > Memo.apply (Tables.tables Dcall) (Theta.theta D) 
87 
 X > Memo.apply2 (Tables.tables Xcall) (Theta.theta X) 
88 
end 
89 

90 
module Modularize (Mod : ModularType) (Theta : MemoThetaType) : MemoThetaType = 
91 
struct 
92 
type t = Theta.t 
93  
94 
let mod_theta = (module Theta : ThetaType with type t = T.t) 
95  
96 
let components : type c. c call_t > (c * t) list = 
97 
fun call > 
98 
match call with 
99 
 Ecall > List.filter (fun ((p, p', f), _) > Mod.modular E p p' f) (Theta.components Ecall) 
100 
 Dcall > List.filter (fun (p , _) > Mod.modular D p) (Theta.components Dcall) 
101 
 Xcall > List.filter (fun ((p, f) , _) > Mod.modular X p f) (Theta.components Xcall) 
102  
103 
let theta : type a b. (a, b, t) theta_t = 
104 
fun tag > 
105 
match tag with 
106 
 J > Theta.theta tag 
107 
 E > (fun p p' f > let theta_e = Theta.theta tag p p' f in 
108 
if Mod.modular E p p' f 
109 
then T.(eval_act mod_theta (call Ecall (p, p', f))) 
110 
else theta_e) 
111 
 D > (fun p > let theta_d = Theta.theta tag p in 
112 
if Mod.modular D p 
113 
then T.(eval_act mod_theta (call Dcall p)) 
114 
else theta_d) 
115 
 X > (fun p f > let theta_x = Theta.theta tag p f in 
116 
if Mod.modular X p f 
117 
then T.(eval_act mod_theta (call Xcall (p, f))) 
118 
else theta_x) 
119 
end 
120  
121 
module type ThetaifyType = functor (Kenv : KenvType) > MemoThetaType 
122  
123 
module BasicThetaify : ThetaifyType = functor (Kenv : KenvType) > 
124 
struct 
125 
type t = T.t 
126  
127 
let theta_ify : type a b. kenv_t > (a, b, T.t) theta_t = 
128 
fun kenv tag > 
129 
match tag with 
130 
 J > (fun j > 
131 
try List.assoc j kenv.cont_junc kenv 
132 
with Not_found > 
133 
Format.eprintf "Lost junction %a@ " pp_junction_name j; 
134 
assert false) 
135 
 E > (fun p > 
136 
try 
137 
let (e, _, _) = List.assoc p kenv.cont_node in e kenv 
138 
with Not_found > 
139 
Format.eprintf "Entering lost path [%a]@." pp_path p; assert false) 
140 
 D > (fun p > 
141 
try 
142 
let (_, d, _) = List.assoc p kenv.cont_node in d kenv 
143 
with Not_found > 
144 
Format.eprintf "During lost path [%a]@." pp_path p; assert false) 
145 
 X > (fun p > 
146 
try 
147 
let (_, _, x) = List.assoc p kenv.cont_node in x kenv 
148 
with Not_found > 
149 
Format.eprintf "Exiting lost path [%a]@." pp_path p; assert false) 
150  
151 
let theta tag = theta_ify Kenv.kenv tag 
152  
153 
let components call = [] 
154 
end 
155  
156 
module ModularThetaify : functor (Tables : MemoThetaTablesType) (Mod : ModularType) > ThetaifyType = 
157 
functor (Tables : MemoThetaTablesType) (Mod : ModularType) (Kenv : KenvType) > 
158 
Modularize (Mod) (Memoize (Tables) (BasicThetaify (Kenv))) 
159  
160 
end 