Project

General

Profile

Download (12.8 KB) Statistics
| Branch: | Tag: | Revision:
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
(4-4/9)