1

open Basetypes

2

open Datatype

3

(* open ActiveEnv *)

4

open CPS_transformer

5

(* open Simulink *)

6

open Theta

7


8

module Interpreter (Transformer : TransformerType) =

9

struct

10

module KT = KenvTheta (Transformer)

11

open KT

12


13

let ( >? ) cond tr =

14

if cond then tr else Transformer.null

15


16

module type DenotationType =

17

sig

18

module Theta : MemoThetaType

19


20

val eval_dest : destination_t > Transformer.t wrapper_t > Transformer.t success_t > Transformer.t fail_t > Transformer.t

21

val eval_tau : trans_t > Transformer.t wrapper_t > Transformer.t success_t > Transformer.t fail_t > Transformer.t

22

val eval_T : transitions_t > Transformer.t wrapper_t > Transformer.t success_t > Transformer.t fail_t > Transformer.t

23

val eval_C : (path_t, 'b, Transformer.t) tag_t > path_t > composition_t > Transformer.t

24

val eval_open_path : mode_t > path_t > path_t > Transformer.t wrapper_t

25

val eval_S : (path_t, 'b, Transformer.t) tag_t > path_t > state_def_t > 'b

26

end

27


28

module type AbsDenotationType =

29

sig

30

val eval_dest : kenv_t > destination_t > Transformer.t wrapper_t > Transformer.t success_t > Transformer.t fail_t > Transformer.t

31

val eval_tau : kenv_t > trans_t > Transformer.t wrapper_t > Transformer.t success_t > Transformer.t fail_t > Transformer.t

32

val eval_T : kenv_t > transitions_t > Transformer.t wrapper_t > Transformer.t success_t > Transformer.t fail_t > Transformer.t

33

val eval_C : kenv_t > (path_t, 'b, Transformer.t) tag_t > path_t > composition_t > Transformer.t

34

val eval_open_path : kenv_t > mode_t > path_t > path_t > Transformer.t wrapper_t

35

val eval_S : kenv_t > (path_t, 'b, Transformer.t) tag_t > path_t > state_def_t > 'b

36

end

37


38

module AbstractKenv (Denot : functor (Kenv : KenvType) > DenotationType) : AbsDenotationType =

39

struct

40

let eval_dest kenv =

41

let module Kenv =

42

struct

43

let kenv = kenv

44

end in

45

let module D = Denot (Kenv) in

46

D.eval_dest

47


48

let eval_tau kenv =

49

let module Kenv =

50

struct

51

let kenv = kenv

52

end in

53

let module D = Denot (Kenv) in

54

D.eval_tau

55


56

let eval_T kenv =

57

let module Kenv =

58

struct

59

let kenv = kenv

60

end in

61

let module D = Denot (Kenv) in

62

D.eval_T

63


64

let eval_C kenv =

65

let module Kenv =

66

struct

67

let kenv = kenv

68

end in

69

let module D = Denot (Kenv) in

70

D.eval_C

71


72

let eval_open_path kenv =

73

let module Kenv =

74

struct

75

let kenv = kenv

76

end in

77

let module D = Denot (Kenv) in

78

D.eval_open_path

79


80

let eval_S kenv =

81

let module Kenv =

82

struct

83

let kenv = kenv

84

end in

85

let module D = Denot (Kenv) in

86

D.eval_S

87

end

88


89

module Denotation : functor (Thetaify : ThetaifyType) (Kenv : KenvType) > DenotationType =

90

functor (Thetaify : ThetaifyType) (Kenv : KenvType) >

91

struct

92

module Theta = Thetaify (Kenv)

93


94

let eval_dest dest wrapper success fail =

95

Log.report ~level:sf_level (fun fmt > Format.fprintf fmt "@[<v 2>D[[%a]]@ " SF.pp_dest dest);

96

match dest with

97

 DPath p > wrapper p (success p)

98

 DJunction j > Theta.theta J j wrapper success fail

99


100

let eval_tau trans wrapper success fail =

101

Log.report ~level:sf_level (fun fmt > Format.fprintf fmt "@[<v 2>tau[[%a]]@ " SF.pp_trans trans);

102

let success' p =

103

Transformer.(success p >> eval_act (module Theta) trans.transition_act)

104

in

105

let cond = Transformer.(event trans.event && trans.condition) in

106

Transformer.(eval_cond cond

107

(eval_act (module Theta) trans.condition_act >> eval_dest trans.dest wrapper success' fail)

108

fail.local)

109


110

let rec eval_T tl wrapper success fail =

111

Log.report ~level:sf_level (fun fmt > Format.fprintf fmt "@[<v 2>T[[%a]]@ " SF.pp_transitions tl);

112

match tl with

113

 [] > fail.global

114

 t::[] > eval_tau t wrapper success fail

115

 t::tl >

116

let fail' = { fail with local = eval_T tl wrapper success fail } in

117

eval_tau t wrapper success fail'

118


119

let frontier path =

120

match path with

121

 [] > [], []

122

 t::q > [t], q

123


124

let rec eval_open_path mode p p1 p2 success_p2 =

125

Log.report ~level:sf_level (fun fmt > Format.fprintf fmt "@[<v 2>open_path_rec[[mode %a, prefix %a, src %a, dst %a]]@ " pp_mode mode pp_path p pp_path p1 pp_path p2);

126

match frontier p1, frontier p2 with

127

 ([x], ps), ([y], pd) when x = y > eval_open_path mode (p@[x]) ps pd success_p2

128

 (x , _ ), (y , pd) >

129

match mode with

130

 Outer > (Transformer.(Theta.theta X (p@x) Loose >> success_p2 >> Theta.theta E (p@y) pd Loose))

131

 Inner > (assert (x = []);

132

Transformer.(Theta.theta X (p@x) Strict >> success_p2 >> Theta.theta E (p@y) pd Strict))

133

 Enter > (assert (x = [] && y <> []);

134

Transformer.( success_p2 >> Theta.theta E (p@y) pd Loose))

135


136

let rec eval_C : type a b. (a, b, Transformer.t) tag_t > path_t > composition_t > Transformer.t =

137

fun tag prefix comp >

138

match tag with

139

 E > Transformer.(

140

Log.report ~level:sf_level (fun fmt > Format.fprintf fmt "@[<v 2>C_%a[[%a, %a]]@ " pp_tag tag pp_path prefix SF.pp_comp comp);

141

match comp with

142

 Or (_T, []) > null

143

 Or ([], [s0]) > eval_open_path Enter prefix [] [s0] null

144

 Or (_T, _S) > let wrapper = eval_open_path Enter [] prefix in

145

let success p_d = null in

146

eval_T _T wrapper success { local = bot; global = bot }

147

 And (_S) > List.fold_right (fun p > (>>) (Theta.theta E (prefix@[p]) [] Loose)) _S null

148

)

149

 D > Transformer.(

150

match comp with

151

 Or (_T, []) > null

152

 Or (_T, p::_S) > eval_cond (active (prefix@[p])) (Theta.theta D (prefix@[p])) (eval_C D prefix (Or (_T, _S)))

153

 And (_S) > List.fold_right (fun p > (>>) (Theta.theta D (prefix@[p]))) _S null

154

)

155

 X > Transformer.(

156

match comp with

157

 Or (_T, []) > null

158

 Or (_T, p::_S) > eval_cond (active (prefix@[p])) (Theta.theta X (prefix@[p]) Loose) (eval_C X prefix (Or (_T, _S)))

159

 And (_S) > List.fold_right (fun p > (>>) (Theta.theta X (prefix@[p]) Loose)) _S null

160

)

161

 J > assert false

162


163

let eval_S : type b. (path_t, b, Transformer.t) tag_t > path_t > state_def_t > b =

164

fun tag p p_def >

165

match tag with

166

 E > fun path frontier > Transformer.(

167

Log.report ~level:sf_level (fun fmt > Format.fprintf fmt "@[<v 2>S_%a[[node %a, dest %a, frontier %a]]@ " pp_tag tag pp_path p pp_path path pp_frontier frontier);

168

((frontier = Loose) >? (eval_act (module Theta) p_def.state_actions.entry_act >> eval_act (module Theta) (open_path p))) >>

169

match path with

170

 [] > eval_C E p p_def.internal_composition

171

 s::path_tl > Theta.theta E (p@[s]) path_tl Loose

172

)

173

 D > Transformer.(

174

Log.report ~level:sf_level (fun fmt > Format.fprintf fmt "@[<v 2>S_%a[[node %a]]@ " pp_tag tag pp_path p);

175

let wrapper_i = eval_open_path Inner [] p in

176

let wrapper_o = eval_open_path Outer [] p in

177

let success p_d = null in

178

let fail_o =

179

let fail_i =

180

let same_fail_C = eval_C D p p_def.internal_composition in

181

{ local = same_fail_C; global = same_fail_C }

182

in

183

let same_fail_i = eval_act (module Theta) p_def.state_actions.during_act >> eval_T p_def.inner_trans wrapper_i success fail_i in

184

{ local = same_fail_i; global = same_fail_i }

185

in

186

eval_T p_def.outer_trans wrapper_o success fail_o

187

)

188

 X > fun frontier > Transformer.(

189

Log.report ~level:sf_level (fun fmt > Format.fprintf fmt "@[<v 2>S_%a[[node %a, frontier %a]]@ " pp_tag tag pp_path p pp_frontier frontier);

190

eval_C X p p_def.internal_composition >>

191

((frontier = Loose) >? (eval_act (module Theta) p_def.state_actions.exit_act >> eval_act (module Theta) (close_path p)))

192

)

193

end

194


195

module type ProgType =

196

sig

197

val init : state_name_t

198

val defs : prog_t src_components_t list

199

end

200


201

module type EvaluationType =

202

sig

203

module Theta : ThetaType with type t = Transformer.t

204

val eval_prog : Transformer.t

205

val eval_components : 'c call_t > ('c * Transformer.t) list

206

end

207


208

module Evaluation (Thetaify : ThetaifyType) (Prog : ProgType) : EvaluationType =

209

struct

210

module Denotation = Denotation (Thetaify)

211

module AbsDenotation = AbstractKenv (Denotation)

212

include AbsDenotation

213


214

module Kenv : KenvType =

215

struct

216

let kenv =

217

List.fold_left (

218

fun accu d > match d with

219

 State (p, defp) > { accu with cont_node = (p, ((fun kenv > eval_S kenv E p defp),

220

(fun kenv > eval_S kenv D p defp),

221

(fun kenv > eval_S kenv X p defp)))::accu.cont_node }

222

 Junction (j, defj) > { accu with cont_junc = (j, (fun kenv > eval_T kenv defj))::accu.cont_junc }

223

 SFFunction _ > accu

224

) {cont_node = []; cont_junc = []} Prog.defs

225

end

226


227

module AppDenotation = Denotation (Kenv)

228

module Theta = AppDenotation.Theta

229


230

let eval_components = Theta.components

231


232

let eval_prog =

233

Transformer.(eval_cond (active [Prog.init]) (Theta.theta D [Prog.init]) (Theta.theta E [Prog.init] [] Loose))

234

end

235

(*

236

module ThetaFix (Prog : ProgType) (Theta : ThetaType) : ThetaType =

237

struct

238

include Denotation (Theta)

239


240

let theta =

241

let kenv =

242

List.fold_left (

243

fun accu d > match d with

244

 State (p, defp) > { accu with cont_node = (p, (eval_S E p defp, eval_S D p defp, eval_S X p defp))::accu.cont_node }

245

 Junction (j, defj) > { accu with cont_junc = (j, (eval_T defj))::accu.cont_junc }

246

) {cont_node = []; cont_junc = []} Prog.defs

247

in Obj.magic (fun tag > theta_ify kenv tag)

248

end

249

module Rec (Prog : ProgType) =

250

struct

251

module rec Theta : ThetaType = ThetaFix (Prog) (Theta)

252

end

253


254

module Eval (Prog : ProgType) : EvaluationType =

255

struct

256

module RecTheta = Rec (Prog)

257

module Theta = RecTheta.Theta

258


259

let eval_prog =

260

Transformer.(eval_cond (active [Prog.init]) (Theta.theta D [Prog.init]) (Theta.theta E [Prog.init] []))

261

end

262


263

module Eval (Prog : ProgType) =

264

struct

265

module ThetaFunctor (Evaluation : EvaluationType) : ThetaType =

266

struct

267

let theta tag = (theta_ify Evaluation.kenv) tag

268

end

269

module EvaluationFunctor (Theta : ThetaType) : EvaluationType =

270

struct

271

include Denotation (Theta)

272


273

let kenv =

274

List.fold_left (

275

fun accu d > match d with

276

 State (p, defp) > { accu with cont_node = (p, (fun kenv > eval_S E p defp, eval_S D p defp, eval_S X p defp))::accu.cont_node }

277

 Junction (j, defj) > { accu with cont_junc = (j, (eval_T defj))::accu.cont_junc }

278

) {cont_node = []; cont_junc = []} Prog.defs

279


280

let eval_prog =

281

Transformer.(eval_cond (active [Prog.init]) (Theta.theta D [Prog.init]) (Theta.theta E [Prog.init] []))

282

end

283

module rec Theta : ThetaType = ThetaFunctor (Evaluation)

284

and Evaluation : EvaluationType = EvaluationFunctor (Theta)

285

end

286

*)

287

end
