Project

General

Profile

« Previous | Next » 

Revision ca7ff3f7

Added by LĂ©lio Brun 7 months ago

reformatting

View differences:

src/tools/stateflow/semantics/cPS_interpreter.ml
1 1
open Basetypes
2 2
open Datatype
3

  
3 4
(* open ActiveEnv *)
4 5
open CPS_transformer
6

  
5 7
(* open Simulink *)
6 8
open Theta
7 9

  
8
module Interpreter (Transformer : TransformerType) =
9
struct
10
module Interpreter (Transformer : TransformerType) = struct
10 11
  module KT = KenvTheta (Transformer)
11 12
  open KT
12 13

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

  
16
  module type DenotationType =
17
  sig
16
  module type DenotationType = sig
18 17
    module Theta : MemoThetaType
19 18

  
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
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

  
24 46
    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
47

  
48
    val eval_S :
49
      (path_t, 'b, Transformer.t) tag_t -> path_t -> state_def_t -> 'b
26 50
  end
27 51

  
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
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
36 89
  end
37 90

  
38
  module AbstractKenv (Denot : functor (Kenv : KenvType) -> DenotationType) : AbsDenotationType =
39
  struct
91
  module AbstractKenv (Denot : functor (Kenv : KenvType) -> DenotationType) :
92
    AbsDenotationType = struct
40 93
    let eval_dest kenv =
41
      let module Kenv =
42
	  struct
43
	    let kenv = kenv
44
	  end in
94
      let module Kenv = struct
95
        let kenv = kenv
96
      end in
45 97
      let module D = Denot (Kenv) in
46 98
      D.eval_dest
47 99

  
48 100
    let eval_tau kenv =
49
      let module Kenv =
50
	  struct
51
	    let kenv = kenv
52
	  end in
101
      let module Kenv = struct
102
        let kenv = kenv
103
      end in
53 104
      let module D = Denot (Kenv) in
54 105
      D.eval_tau
55 106

  
56 107
    let eval_T kenv =
57
      let module Kenv =
58
	  struct
59
	    let kenv = kenv
60
	  end in
108
      let module Kenv = struct
109
        let kenv = kenv
110
      end in
61 111
      let module D = Denot (Kenv) in
62 112
      D.eval_T
63 113

  
64 114
    let eval_C kenv =
65
      let module Kenv =
66
	  struct
67
	    let kenv = kenv
68
	  end in
115
      let module Kenv = struct
116
        let kenv = kenv
117
      end in
69 118
      let module D = Denot (Kenv) in
70 119
      D.eval_C
71 120

  
72 121
    let eval_open_path kenv =
73
      let module Kenv =
74
	  struct
75
	    let kenv = kenv
76
	  end in
122
      let module Kenv = struct
123
        let kenv = kenv
124
      end in
77 125
      let module D = Denot (Kenv) in
78 126
      D.eval_open_path
79 127

  
80 128
    let eval_S kenv =
81
      let module Kenv =
82
	  struct
83
	    let kenv = kenv
84
	  end in
129
      let module Kenv = struct
130
        let kenv = kenv
131
      end in
85 132
      let module D = Denot (Kenv) in
86 133
      D.eval_S
87 134
  end
88 135

  
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
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
194 316

  
195
  module type ProgType =
196
  sig
317
  module type ProgType = sig
197 318
    val init : state_name_t
319

  
198 320
    val defs : prog_t src_components_t list
199 321
  end
200 322

  
201
  module type EvaluationType =
202
  sig
323
  module type EvaluationType = sig
203 324
    module Theta : ThetaType with type t = Transformer.t
325

  
204 326
    val eval_prog : Transformer.t
327

  
205 328
    val eval_components : 'c call_t -> ('c * Transformer.t) list
206 329
  end
207 330

  
208
  module Evaluation (Thetaify : ThetaifyType) (Prog : ProgType) : EvaluationType =
209
  struct
331
  module Evaluation (Thetaify : ThetaifyType) (Prog : ProgType) :
332
    EvaluationType = struct
210 333
    module Denotation = Denotation (Thetaify)
211 334
    module AbsDenotation = AbstractKenv (Denotation)
212 335
    include AbsDenotation
213 336

  
214
    module Kenv : KenvType =
215
    struct
337
    module Kenv : KenvType = struct
216 338
      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
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
225 361
    end
226 362

  
227 363
    module AppDenotation = Denotation (Kenv)
......
230 366
    let eval_components = Theta.components
231 367

  
232 368
    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)
369
      Transformer.(
370
        eval_cond
371
          (active [ Prog.init ])
372
          (Theta.theta D [ Prog.init ])
373
          (Theta.theta E [ Prog.init ] [] Loose))
248 374
  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
  *)
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 *)
287 407
end

Also available in: Unified diff