Project

General

Profile

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

    
8
(* Theta functions interfaces including memoization when using modular calls 
9
   
10
   parametrized by the transformer specifying the type of the
11
   continuation. Evaluation of actions is also continuation dependent.
12
*)
13

    
14
module KenvTheta (T : TransformerType) =
15
struct
16

    
17
  type kenv_t = {
18
    cont_node : (
19
      path_t * (
20
	(kenv_t -> path_t -> frontier_t -> T.t) *
21
	(kenv_t -> T.t) *
22
	(kenv_t -> frontier_t -> T.t)
23
      )
24
    ) list;
25
    cont_junc : (
26
      junction_name_t * (
27
	kenv_t -> T.t wrapper_t -> T.t success_t -> T.t fail_t -> T.t)
28
    ) list
29
  }
30

    
31
	
32
  let init_env src =
33
    List.fold_left (fun accu d ->
34
      match d with
35
      | Datatype.State (p, _) -> ActiveStates.Env.add p false accu
36
      | _ -> accu)
37
      ActiveStates.Env.empty
38
      src
39

    
40
  module type KenvType =
41
  sig
42
    val kenv : kenv_t
43
  end
44

    
45
  module type MemoThetaTablesType =
46
  sig
47
    val tables : 'c call_t -> ('c, T.t) Memo.t
48
  end
49

    
50
  module type MemoThetaType =
51
  sig
52
    include ThetaType with type t = T.t
53
    val components : 'c call_t -> ('c * t) list
54
  end
55

    
56
  module type ModularType =
57
  sig
58
    val modular : (path_t, 'b, bool) tag_t -> path_t -> 'b
59
  end
60

    
61
  module MemoThetaTables : functor () -> MemoThetaTablesType = functor () ->
62
  struct
63
    let table_theta_e = (Memo.create () : (path_t * path_t * frontier_t, T.t) Memo.t)
64
    let table_theta_d = (Memo.create () : (path_t, T.t) Memo.t)
65
    let table_theta_x = (Memo.create () : (path_t * frontier_t, T.t) Memo.t)
66

    
67
    let tables : type c. c call_t -> (c, T.t) Memo.t =
68
      fun call ->
69
      match call with
70
      | Ecall -> table_theta_e
71
      | Dcall -> table_theta_d
72
      | Xcall -> table_theta_x
73
  end
74

    
75
  module Memoize (Tables : MemoThetaTablesType) (Theta : ThetaType with type t = T.t) : MemoThetaType =
76
  struct
77
    type t = Theta.t
78

    
79
    let components call =
80
      Memo.fold (Tables.tables call) (fun k v res -> (k, v)::res) []
81

    
82
    let theta : type a b. (a, b, t) theta_t =
83
      fun tag ->
84
      match tag with
85
      | J -> Theta.theta J
86
      | E -> Memo.apply3 (Tables.tables Ecall) (Theta.theta E)
87
      | D -> Memo.apply  (Tables.tables Dcall) (Theta.theta D)
88
      | X -> Memo.apply2 (Tables.tables Xcall) (Theta.theta X)
89
  end
90
    
91
  module Modularize (Mod : ModularType) (Theta : MemoThetaType) : MemoThetaType =
92
  struct
93
    type t = Theta.t
94

    
95
    let mod_theta = (module Theta : ThetaType with type t = T.t)
96

    
97
    let components : type c. c call_t -> (c * t) list =
98
      fun call ->
99
      match call with
100
      | Ecall -> List.filter (fun ((p, p', f), _) -> Mod.modular E p p' f) (Theta.components Ecall)
101
      | Dcall -> List.filter (fun (p         , _) -> Mod.modular D p)      (Theta.components Dcall)
102
      | Xcall -> List.filter (fun ((p, f)    , _) -> Mod.modular X p f)    (Theta.components Xcall)
103

    
104
    let theta : type a b. (a, b, t) theta_t =
105
      fun tag ->
106
      match tag with
107
      | J -> Theta.theta tag
108
      | E -> (fun p p' f -> let theta_e = Theta.theta tag p p' f in
109
	if Mod.modular E p p' f
110
	then T.(eval_act mod_theta (call Ecall (p, p', f)))
111
	else theta_e)
112
      | D -> (fun p -> let theta_d = Theta.theta tag p in
113
	if Mod.modular D p
114
	then T.(eval_act mod_theta (call Dcall p))
115
	else theta_d)
116
      | X -> (fun p f -> let theta_x = Theta.theta tag p f in
117
	if Mod.modular X p f
118
	then T.(eval_act mod_theta (call Xcall (p, f)))
119
	else theta_x)
120
  end
121

    
122
  module type ThetaifyType = functor (Kenv : KenvType) -> MemoThetaType
123

    
124
  module BasicThetaify : ThetaifyType = functor (Kenv : KenvType) ->
125
  struct
126
    type t = T.t
127

    
128
    let theta_ify : type a b. kenv_t -> (a, b, T.t) theta_t =
129
      fun kenv tag ->
130
      match tag with
131
      | J -> (fun j ->
132
	try List.assoc j kenv.cont_junc kenv
133
	with Not_found ->
134
	  Format.eprintf "Lost junction %a@ " pp_junction_name j;
135
	  assert false)
136
      | E -> (fun p ->
137
	try
138
	  let (e, _, _) = List.assoc p kenv.cont_node in e kenv
139
	with Not_found -> 
140
	  Format.eprintf "Entering lost path [%a]@." pp_path p; assert false)
141
      | D -> (fun p ->
142
	try
143
	  let (_, d, _) = List.assoc p kenv.cont_node in d kenv
144
	with Not_found -> 
145
	  Format.eprintf "During lost path [%a]@." pp_path p; assert false)
146
      | X -> (fun p ->
147
	try
148
	  let (_, _, x) = List.assoc p kenv.cont_node in x kenv
149
	with Not_found -> 
150
	  Format.eprintf "Exiting lost path [%a]@." pp_path p; assert false)
151

    
152
    let theta tag = theta_ify Kenv.kenv tag
153

    
154
    let components call = []
155
  end
156

    
157
  module ModularThetaify : functor (Tables : MemoThetaTablesType) (Mod : ModularType) -> ThetaifyType =
158
    functor (Tables : MemoThetaTablesType) (Mod : ModularType) (Kenv : KenvType) ->
159
      Modularize (Mod) (Memoize (Tables) (BasicThetaify (Kenv)))
160

    
161
end
(10-10/10)