1

open Basetypes

2

open Datatype

3


4

(* open ActiveEnv *)

5

open CPS_transformer

6


7

(* open Simulink *)

8

open Theta

9


10

module Interpreter (Transformer : TransformerType) = struct

11

module KT = KenvTheta (Transformer)

12

open KT

13


14

let ( >? ) cond tr = if cond then tr else Transformer.null

15


16

module type DenotationType = sig

17

module Theta : MemoThetaType

18


19

val eval_dest :

20

destination_t >

21

Transformer.t wrapper_t >

22

Transformer.t success_t >

23

Transformer.t fail_t >

24

Transformer.t

25


26

val eval_tau :

27

trans_t >

28

Transformer.t wrapper_t >

29

Transformer.t success_t >

30

Transformer.t fail_t >

31

Transformer.t

32


33

val eval_T :

34

transitions_t >

35

Transformer.t wrapper_t >

36

Transformer.t success_t >

37

Transformer.t fail_t >

38

Transformer.t

39


40

val eval_C :

41

(path_t, 'b, Transformer.t) tag_t >

42

path_t >

43

composition_t >

44

Transformer.t

45


46

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

47


48

val eval_S :

49

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

50

end

51


52

module type AbsDenotationType = sig

53

val eval_dest :

54

kenv_t >

55

destination_t >

56

Transformer.t wrapper_t >

57

Transformer.t success_t >

58

Transformer.t fail_t >

59

Transformer.t

60


61

val eval_tau :

62

kenv_t >

63

trans_t >

64

Transformer.t wrapper_t >

65

Transformer.t success_t >

66

Transformer.t fail_t >

67

Transformer.t

68


69

val eval_T :

70

kenv_t >

71

transitions_t >

72

Transformer.t wrapper_t >

73

Transformer.t success_t >

74

Transformer.t fail_t >

75

Transformer.t

76


77

val eval_C :

78

kenv_t >

79

(path_t, 'b, Transformer.t) tag_t >

80

path_t >

81

composition_t >

82

Transformer.t

83


84

val eval_open_path :

85

kenv_t > mode_t > path_t > path_t > Transformer.t wrapper_t

86


87

val eval_S :

88

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

89

end

90


91

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

92

AbsDenotationType = struct

93

let eval_dest kenv =

94

let module Kenv = struct

95

let kenv = kenv

96

end in

97

let module D = Denot (Kenv) in

98

D.eval_dest

99


100

let eval_tau kenv =

101

let module Kenv = struct

102

let kenv = kenv

103

end in

104

let module D = Denot (Kenv) in

105

D.eval_tau

106


107

let eval_T kenv =

108

let module Kenv = struct

109

let kenv = kenv

110

end in

111

let module D = Denot (Kenv) in

112

D.eval_T

113


114

let eval_C kenv =

115

let module Kenv = struct

116

let kenv = kenv

117

end in

118

let module D = Denot (Kenv) in

119

D.eval_C

120


121

let eval_open_path kenv =

122

let module Kenv = struct

123

let kenv = kenv

124

end in

125

let module D = Denot (Kenv) in

126

D.eval_open_path

127


128

let eval_S kenv =

129

let module Kenv = struct

130

let kenv = kenv

131

end in

132

let module D = Denot (Kenv) in

133

D.eval_S

134

end

135


136

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

137

DenotationType =

138

functor

139

(Thetaify : ThetaifyType)

140

(Kenv : KenvType)

141

>

142

struct

143

module Theta = Thetaify (Kenv)

144


145

let eval_dest dest wrapper success fail =

146

Log.report ~level:sf_level (fun fmt >

147

Format.fprintf fmt "@[<v 2>D[[%a]]@ " SF.pp_dest dest);

148

match dest with

149

 DPath p >

150

wrapper p (success p)

151

 DJunction j >

152

Theta.theta J j wrapper success fail

153


154

let eval_tau trans wrapper success fail =

155

Log.report ~level:sf_level (fun fmt >

156

Format.fprintf fmt "@[<v 2>tau[[%a]]@ " SF.pp_trans trans);

157

let success' p =

158

Transformer.(

159

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

160

in

161

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

162

Transformer.(

163

eval_cond cond

164

(eval_act (module Theta) trans.condition_act

165

>> eval_dest trans.dest wrapper success' fail)

166

fail.local)

167


168

let rec eval_T tl wrapper success fail =

169

Log.report ~level:sf_level (fun fmt >

170

Format.fprintf fmt "@[<v 2>T[[%a]]@ " SF.pp_transitions tl);

171

match tl with

172

 [] >

173

fail.global

174

 [ t ] >

175

eval_tau t wrapper success fail

176

 t :: tl >

177

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

178

eval_tau t wrapper success fail'

179


180

let frontier path = match path with [] > [], []  t :: q > [ t ], q

181


182

let rec eval_open_path mode p p1 p2 success_p2 =

183

Log.report ~level:sf_level (fun fmt >

184

Format.fprintf fmt

185

"@[<v 2>open_path_rec[[mode %a, prefix %a, src %a, dst %a]]@ "

186

pp_mode mode pp_path p pp_path p1 pp_path p2);

187

match frontier p1, frontier p2 with

188

 ([ x ], ps), ([ y ], pd) when x = y >

189

eval_open_path mode (p @ [ x ]) ps pd success_p2

190

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

191

match mode with

192

 Outer >

193

Transformer.(

194

Theta.theta X (p @ x) Loose

195

>> success_p2

196

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

197

 Inner >

198

assert (x = []);

199

Transformer.(

200

Theta.theta X (p @ x) Strict

201

>> success_p2

202

>> Theta.theta E (p @ y) pd Strict)

203

 Enter >

204

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

205

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

206


207

let rec eval_C :

208

type a b.

209

(a, b, Transformer.t) tag_t >

210

path_t >

211

composition_t >

212

Transformer.t =

213

fun tag prefix comp >

214

match tag with

215

 E > (

216

Transformer.(

217

Log.report ~level:sf_level (fun fmt >

218

Format.fprintf fmt "@[<v 2>C_%a[[%a, %a]]@ " pp_tag tag pp_path

219

prefix SF.pp_comp comp);

220

match comp with

221

 Or (_T, []) >

222

null

223

 Or ([], [ s0 ]) >

224

eval_open_path Enter prefix [] [ s0 ] null

225

 Or (_T, _S) >

226

let wrapper = eval_open_path Enter [] prefix in

227

let success _p_d = null in

228

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

229

 And _S >

230

List.fold_right

231

(fun p > ( >> ) (Theta.theta E (prefix @ [ p ]) [] Loose))

232

_S null))

233

 D > (

234

Transformer.(

235

match comp with

236

 Or (_T, []) >

237

null

238

 Or (_T, p :: _S) >

239

eval_cond

240

(active (prefix @ [ p ]))

241

(Theta.theta D (prefix @ [ p ]))

242

(eval_C D prefix (Or (_T, _S)))

243

 And _S >

244

List.fold_right

245

(fun p > ( >> ) (Theta.theta D (prefix @ [ p ])))

246

_S null))

247

 X > (

248

Transformer.(

249

match comp with

250

 Or (_T, []) >

251

null

252

 Or (_T, p :: _S) >

253

eval_cond

254

(active (prefix @ [ p ]))

255

(Theta.theta X (prefix @ [ p ]) Loose)

256

(eval_C X prefix (Or (_T, _S)))

257

 And _S >

258

List.fold_right

259

(fun p > ( >> ) (Theta.theta X (prefix @ [ p ]) Loose))

260

_S null))

261

 J >

262

assert false

263


264

let eval_S :

265

type b. (path_t, b, Transformer.t) tag_t > path_t > state_def_t > b

266

=

267

fun tag p p_def >

268

match tag with

269

 E > (

270

fun path frontier >

271

Transformer.(

272

Log.report ~level:sf_level (fun fmt >

273

Format.fprintf fmt

274

"@[<v 2>S_%a[[node %a, dest %a, frontier %a]]@ " pp_tag tag

275

pp_path p pp_path path pp_frontier frontier);

276

frontier = Loose

277

>? (eval_act (module Theta) p_def.state_actions.entry_act

278

>> eval_act (module Theta) (open_path p))

279

>>

280

match path with

281

 [] >

282

eval_C E p p_def.internal_composition

283

 s :: path_tl >

284

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

285

 D >

286

Transformer.(

287

Log.report ~level:sf_level (fun fmt >

288

Format.fprintf fmt "@[<v 2>S_%a[[node %a]]@ " pp_tag tag pp_path

289

p);

290

let wrapper_i = eval_open_path Inner [] p in

291

let wrapper_o = eval_open_path Outer [] p in

292

let success _p_d = null in

293

let fail_o =

294

let fail_i =

295

let same_fail_C = eval_C D p p_def.internal_composition in

296

{ local = same_fail_C; global = same_fail_C }

297

in

298

let same_fail_i =

299

eval_act (module Theta) p_def.state_actions.during_act

300

>> eval_T p_def.inner_trans wrapper_i success fail_i

301

in

302

{ local = same_fail_i; global = same_fail_i }

303

in

304

eval_T p_def.outer_trans wrapper_o success fail_o)

305

 X >

306

fun frontier >

307

Transformer.(

308

Log.report ~level:sf_level (fun fmt >

309

Format.fprintf fmt "@[<v 2>S_%a[[node %a, frontier %a]]@ "

310

pp_tag tag pp_path p pp_frontier frontier);

311

eval_C X p p_def.internal_composition

312

>> (frontier = Loose

313

>? (eval_act (module Theta) p_def.state_actions.exit_act

314

>> eval_act (module Theta) (close_path p))))

315

end

316


317

module type ProgType = sig

318

val init : state_name_t

319


320

val defs : prog_t src_components_t list

321

end

322


323

module type EvaluationType = sig

324

module Theta : ThetaType with type t = Transformer.t

325


326

val eval_prog : Transformer.t

327


328

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

329

end

330


331

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

332

EvaluationType = struct

333

module Denotation = Denotation (Thetaify)

334

module AbsDenotation = AbstractKenv (Denotation)

335

include AbsDenotation

336


337

module Kenv : KenvType = struct

338

let kenv =

339

List.fold_left

340

(fun accu d >

341

match d with

342

 State (p, defp) >

343

{

344

accu with

345

cont_node =

346

( p,

347

( (fun kenv > eval_S kenv E p defp),

348

(fun kenv > eval_S kenv D p defp),

349

fun kenv > eval_S kenv X p defp ) )

350

:: accu.cont_node;

351

}

352

 Junction (j, defj) >

353

{

354

accu with

355

cont_junc = (j, fun kenv > eval_T kenv defj) :: accu.cont_junc;

356

}

357

 SFFunction _ >

358

accu)

359

{ cont_node = []; cont_junc = [] }

360

Prog.defs

361

end

362


363

module AppDenotation = Denotation (Kenv)

364

module Theta = AppDenotation.Theta

365


366

let eval_components = Theta.components

367


368

let eval_prog =

369

Transformer.(

370

eval_cond

371

(active [ Prog.init ])

372

(Theta.theta D [ Prog.init ])

373

(Theta.theta E [ Prog.init ] [] Loose))

374

end

375

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

376

include Denotation (Theta)

377


378

let theta = let kenv = List.fold_left ( fun accu d > match d with  State

379

(p, defp) > { accu with cont_node = (p, (eval_S E p defp, eval_S D p defp,

380

eval_S X p defp))::accu.cont_node }  Junction (j, defj) > { accu with

381

cont_junc = (j, (eval_T defj))::accu.cont_junc } ) {cont_node = [];

382

cont_junc = []} Prog.defs in Obj.magic (fun tag > theta_ify kenv tag) end

383

module Rec (Prog : ProgType) = struct module rec Theta : ThetaType =

384

ThetaFix (Prog) (Theta) end

385


386

module Eval (Prog : ProgType) : EvaluationType = struct module RecTheta =

387

Rec (Prog) module Theta = RecTheta.Theta

388


389

let eval_prog = Transformer.(eval_cond (active [Prog.init]) (Theta.theta D

390

[Prog.init]) (Theta.theta E [Prog.init] [])) end

391


392

module Eval (Prog : ProgType) = struct module ThetaFunctor (Evaluation :

393

EvaluationType) : ThetaType = struct let theta tag = (theta_ify

394

Evaluation.kenv) tag end module EvaluationFunctor (Theta : ThetaType) :

395

EvaluationType = struct include Denotation (Theta)

396


397

let kenv = List.fold_left ( fun accu d > match d with  State (p, defp) >

398

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

399

eval_S X p defp))::accu.cont_node }  Junction (j, defj) > { accu with

400

cont_junc = (j, (eval_T defj))::accu.cont_junc } ) {cont_node = [];

401

cont_junc = []} Prog.defs

402


403

let eval_prog = Transformer.(eval_cond (active [Prog.init]) (Theta.theta D

404

[Prog.init]) (Theta.theta E [Prog.init] [])) end module rec Theta :

405

ThetaType = ThetaFunctor (Evaluation) and Evaluation : EvaluationType =

406

EvaluationFunctor (Theta) end *)

407

end
