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
