Project

General

Profile

Download (10.8 KB) Statistics
| Branch: | Tag: | Revision:
1
open Lustrec
2
open Basetypes
3
open Datatype
4
(* open ActiveEnv *)
5
open CPS_transformer
6
(* open Simulink *)
7
open Theta
8

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

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

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

    
21
    val eval_dest : destination_t -> Transformer.t wrapper_t -> Transformer.t success_t -> Transformer.t fail_t -> Transformer.t
22
    val eval_tau : trans_t -> Transformer.t wrapper_t -> Transformer.t success_t -> Transformer.t fail_t -> Transformer.t
23
    val eval_T : transitions_t -> Transformer.t wrapper_t -> Transformer.t success_t -> Transformer.t fail_t -> Transformer.t
24
    val eval_C : (path_t, 'b, Transformer.t) tag_t -> path_t -> composition_t -> Transformer.t
25
    val eval_open_path : mode_t -> path_t -> path_t -> Transformer.t wrapper_t
26
    val eval_S : (path_t, 'b, Transformer.t) tag_t -> path_t -> state_def_t -> 'b
27
  end
28

    
29
  module type AbsDenotationType =
30
  sig
31
    val eval_dest : kenv_t -> destination_t -> Transformer.t wrapper_t -> Transformer.t success_t -> Transformer.t fail_t -> Transformer.t
32
    val eval_tau : kenv_t -> trans_t -> Transformer.t wrapper_t -> Transformer.t success_t -> Transformer.t fail_t -> Transformer.t
33
    val eval_T : kenv_t -> transitions_t -> Transformer.t wrapper_t -> Transformer.t success_t -> Transformer.t fail_t -> Transformer.t
34
    val eval_C : kenv_t -> (path_t, 'b, Transformer.t) tag_t -> path_t -> composition_t -> Transformer.t
35
    val eval_open_path : kenv_t -> mode_t -> path_t -> path_t -> Transformer.t wrapper_t
36
    val eval_S : kenv_t -> (path_t, 'b, Transformer.t) tag_t -> path_t -> state_def_t -> 'b
37
  end
38

    
39
  module AbstractKenv (Denot : functor (Kenv : KenvType) -> DenotationType) : AbsDenotationType =
40
  struct
41
    let eval_dest kenv =
42
      let module Kenv =
43
	  struct
44
	    let kenv = kenv
45
	  end in
46
      let module D = Denot (Kenv) in
47
      D.eval_dest
48

    
49
    let eval_tau kenv =
50
      let module Kenv =
51
	  struct
52
	    let kenv = kenv
53
	  end in
54
      let module D = Denot (Kenv) in
55
      D.eval_tau
56

    
57
    let eval_T kenv =
58
      let module Kenv =
59
	  struct
60
	    let kenv = kenv
61
	  end in
62
      let module D = Denot (Kenv) in
63
      D.eval_T
64

    
65
    let eval_C kenv =
66
      let module Kenv =
67
	  struct
68
	    let kenv = kenv
69
	  end in
70
      let module D = Denot (Kenv) in
71
      D.eval_C
72

    
73
    let eval_open_path kenv =
74
      let module Kenv =
75
	  struct
76
	    let kenv = kenv
77
	  end in
78
      let module D = Denot (Kenv) in
79
      D.eval_open_path
80

    
81
    let eval_S kenv =
82
      let module Kenv =
83
	  struct
84
	    let kenv = kenv
85
	  end in
86
      let module D = Denot (Kenv) in
87
      D.eval_S
88
  end
89

    
90
  module Denotation : functor (Thetaify : ThetaifyType) (Kenv : KenvType) -> DenotationType =
91
  functor (Thetaify : ThetaifyType) (Kenv : KenvType) ->
92
  struct
93
    module Theta = Thetaify (Kenv)
94

    
95
    let eval_dest dest wrapper success fail =
96
      Log.report ~level:sf_level (fun fmt -> Format.fprintf fmt "@[<v 2>D[[%a]]@ " SF.pp_dest dest);
97
      match dest with
98
      | DPath p -> wrapper p (success p)
99
      | DJunction j -> Theta.theta J j wrapper success fail
100

    
101
    let eval_tau trans wrapper success fail =
102
      Log.report ~level:sf_level (fun fmt -> Format.fprintf fmt "@[<v 2>tau[[%a]]@ " SF.pp_trans trans);
103
      let success' p =
104
	Transformer.(success p >> eval_act (module Theta) trans.transition_act)
105
      in
106
      let cond = Transformer.(event trans.event && trans.condition) in
107
      Transformer.(eval_cond cond
108
		     (eval_act (module Theta) trans.condition_act >> eval_dest trans.dest wrapper success' fail)
109
		     fail.local)
110

    
111
    let rec eval_T tl wrapper success fail =
112
      Log.report ~level:sf_level (fun fmt -> Format.fprintf fmt "@[<v 2>T[[%a]]@ " SF.pp_transitions tl);
113
      match tl with
114
      | [] -> fail.global
115
      | t::[] ->  eval_tau t wrapper success fail
116
      | t::tl ->
117
	 let fail' = { fail with local = eval_T tl wrapper success fail } in
118
	 eval_tau t wrapper success fail'
119

    
120
    let frontier path =
121
      match path with
122
      | []   -> [], []
123
      | t::q -> [t], q
124

    
125
    let rec eval_open_path mode p p1 p2 success_p2 =
126
      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);
127
      match frontier p1, frontier p2 with
128
      | ([x], ps), ([y], pd) when x = y -> eval_open_path mode (p@[x]) ps pd success_p2
129
      | (x  , _ ), (y  , pd)            ->
130
	 match mode with
131
	 | Outer -> (Transformer.(Theta.theta X (p@x) Loose  >> success_p2 >> Theta.theta E (p@y) pd Loose))
132
	 | Inner -> (assert (x = []);
133
		     Transformer.(Theta.theta X (p@x) Strict >> success_p2 >> Theta.theta E (p@y) pd Strict))
134
	 | Enter -> (assert (x = [] && y <> []);
135
		     Transformer.(                              success_p2 >> Theta.theta E (p@y) pd Loose))
136

    
137
    let rec eval_C : type a b. (a, b, Transformer.t) tag_t -> path_t -> composition_t -> Transformer.t =
138
      fun tag prefix comp ->
139
	match tag with
140
	| E -> Transformer.(
141
	  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);
142
	  match comp with
143
	  | Or (_T, [])   -> null
144
	  | Or ([], [s0]) -> eval_open_path Enter prefix [] [s0] null
145
	  | Or (_T, _S)   -> let wrapper = eval_open_path Enter [] prefix in
146
			     let success p_d = null in
147
			     eval_T _T wrapper success { local = bot; global = bot }
148
	  | And (_S)    -> List.fold_right (fun p -> (>>) (Theta.theta E (prefix@[p]) [] Loose)) _S null
149
	)
150
	| D -> Transformer.(
151
	  match comp with
152
	  | Or (_T, [])    -> null
153
	  | Or (_T, p::_S) -> eval_cond (active (prefix@[p])) (Theta.theta D (prefix@[p])) (eval_C D prefix (Or (_T, _S)))
154
	  | And (_S)       -> List.fold_right (fun p -> (>>) (Theta.theta D (prefix@[p]))) _S null
155
	)
156
	| X -> Transformer.(
157
	  match comp with
158
	  | Or (_T, [])    -> null
159
	  | Or (_T, p::_S) -> eval_cond (active (prefix@[p])) (Theta.theta X (prefix@[p]) Loose) (eval_C X prefix (Or (_T, _S)))
160
	  | And (_S)       -> List.fold_right (fun p -> (>>) (Theta.theta X (prefix@[p]) Loose)) _S null
161
	)
162
	| J -> assert false
163

    
164
    let eval_S : type b. (path_t, b, Transformer.t) tag_t -> path_t -> state_def_t -> b =
165
      fun tag p p_def ->
166
	match tag with
167
	| E -> fun path frontier -> Transformer.(
168
	  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);
169
	  ((frontier = Loose) >? (eval_act (module Theta) p_def.state_actions.entry_act >> eval_act (module Theta) (open_path p))) >>
170
	  match path with
171
	  | []         -> eval_C E p p_def.internal_composition
172
	  | s::path_tl -> Theta.theta E (p@[s]) path_tl Loose
173
	)
174
	| D -> Transformer.(
175
	  Log.report ~level:sf_level (fun fmt -> Format.fprintf fmt "@[<v 2>S_%a[[node %a]]@ " pp_tag tag pp_path p);
176
	  let wrapper_i = eval_open_path Inner [] p in
177
	  let wrapper_o = eval_open_path Outer [] p in
178
	  let success p_d = null in
179
	  let fail_o =
180
	    let fail_i =
181
	      let same_fail_C = eval_C D p p_def.internal_composition in
182
	      { local = same_fail_C; global = same_fail_C }
183
	    in
184
	    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
185
	    { local = same_fail_i; global = same_fail_i }
186
	  in
187
	  eval_T p_def.outer_trans wrapper_o success fail_o
188
	)
189
	| X -> fun frontier -> Transformer.(
190
	  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);
191
	  eval_C X p p_def.internal_composition >>
192
	  ((frontier = Loose) >? (eval_act (module Theta) p_def.state_actions.exit_act >> eval_act (module Theta) (close_path p)))
193
	)
194
  end
195

    
196
  module type ProgType =
197
  sig
198
    val init : state_name_t
199
    val defs : prog_t src_components_t list
200
  end
201

    
202
  module type EvaluationType =
203
  sig
204
    module Theta : ThetaType with type t = Transformer.t
205
    val eval_prog : Transformer.t
206
    val eval_components : 'c call_t -> ('c * Transformer.t) list
207
  end
208

    
209
  module Evaluation (Thetaify : ThetaifyType) (Prog : ProgType) : EvaluationType =
210
  struct
211
    module Denotation = Denotation (Thetaify)
212
    module AbsDenotation = AbstractKenv (Denotation)
213
    include AbsDenotation
214

    
215
    module Kenv : KenvType =
216
    struct
217
      let kenv =
218
	List.fold_left (
219
	  fun accu d -> match d with
220
          | State (p, defp)    -> { accu with cont_node = (p, ((fun kenv -> eval_S kenv E p defp),
221
                                                               (fun kenv -> eval_S kenv D p defp),
222
                                                               (fun kenv -> eval_S kenv X p defp)))::accu.cont_node }
223
	  | Junction (j, defj) -> { accu with cont_junc = (j, (fun kenv -> eval_T kenv defj))::accu.cont_junc }
224
          | SFFunction _       -> accu
225
        ) {cont_node = []; cont_junc = []} Prog.defs
226
    end
227

    
228
    module AppDenotation = Denotation (Kenv)
229
    module Theta = AppDenotation.Theta
230

    
231
    let eval_components = Theta.components
232

    
233
    let eval_prog =
234
      Transformer.(eval_cond (active [Prog.init]) (Theta.theta D [Prog.init]) (Theta.theta E [Prog.init] [] Loose))
235
  end
236
 (*
237
  module ThetaFix (Prog : ProgType) (Theta : ThetaType) : ThetaType =
238
  struct
239
    include Denotation (Theta)
240

    
241
    let theta =
242
      let kenv =
243
	List.fold_left (
244
	  fun accu d -> match d with
245
	  | 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  }
246
	  | Junction (j, defj) -> { accu with cont_junc = (j, (eval_T defj))::accu.cont_junc  }
247
	) {cont_node = []; cont_junc = []} Prog.defs
248
      in Obj.magic (fun tag -> theta_ify kenv tag)
249
  end
250
  module Rec (Prog : ProgType) =
251
  struct
252
    module rec Theta : ThetaType = ThetaFix (Prog) (Theta)
253
  end
254

    
255
  module Eval (Prog : ProgType) : EvaluationType =
256
  struct
257
    module RecTheta = Rec (Prog)
258
    module Theta = RecTheta.Theta
259

    
260
    let eval_prog =
261
	Transformer.(eval_cond (active [Prog.init]) (Theta.theta D [Prog.init]) (Theta.theta E [Prog.init] []))
262
  end
263

    
264
  module Eval (Prog : ProgType) =
265
  struct
266
    module ThetaFunctor (Evaluation : EvaluationType) : ThetaType =
267
    struct
268
      let theta tag = (theta_ify Evaluation.kenv) tag
269
    end
270
    module EvaluationFunctor (Theta : ThetaType) : EvaluationType =
271
    struct
272
      include Denotation (Theta)
273

    
274
      let kenv =
275
	List.fold_left (
276
	  fun accu d -> match d with
277
	  | 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  }
278
	  | Junction (j, defj) -> { accu with cont_junc = (j, (eval_T defj))::accu.cont_junc  }
279
	) {cont_node = []; cont_junc = []} Prog.defs
280

    
281
      let eval_prog =
282
	Transformer.(eval_cond (active [Prog.init]) (Theta.theta D [Prog.init]) (Theta.theta E [Prog.init] []))
283
    end
284
    module rec Theta : ThetaType = ThetaFunctor (Evaluation)
285
    and Evaluation : EvaluationType = EvaluationFunctor (Theta)
286
end
287
  *)
288
end
(5-5/10)