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
