Project

General

Profile

Download (5.26 KB) Statistics
| Branch: | Tag: | Revision:
1
open Basetypes
2

    
3
(* open ActiveEnv *)
4
open CPS_transformer
5

    
6
(* open Datatype *)
7
(* open Simulink *)
8

    
9
(* Theta functions interfaces including memoization when using modular calls
10

    
11
   parametrized by the transformer specifying the type of the continuation.
12
   Evaluation of actions is also continuation dependent. *)
13

    
14
module KenvTheta (T : TransformerType) = struct
15
  type kenv_t = {
16
    cont_node :
17
      (path_t
18
      * ((kenv_t -> path_t -> frontier_t -> T.t)
19
        * (kenv_t -> T.t)
20
        * (kenv_t -> frontier_t -> T.t)))
21
      list;
22
    cont_junc :
23
      (junction_name_t
24
      * (kenv_t -> T.t wrapper_t -> T.t success_t -> T.t fail_t -> T.t))
25
      list;
26
  }
27

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

    
38
  module type KenvType = sig
39
    val kenv : kenv_t
40
  end
41

    
42
  module type MemoThetaTablesType = sig
43
    val tables : 'c call_t -> ('c, T.t) Memo.t
44
  end
45

    
46
  module type MemoThetaType = sig
47
    include ThetaType with type t = T.t
48

    
49
    val components : 'c call_t -> ('c * t) list
50
  end
51

    
52
  module type ModularType = sig
53
    val modular : (path_t, 'b, bool) tag_t -> path_t -> 'b
54
  end
55

    
56
  module MemoThetaTables : functor () -> MemoThetaTablesType =
57
  functor
58
    ()
59
    ->
60
    struct
61
      let table_theta_e =
62
        (Memo.create () : (path_t * path_t * frontier_t, T.t) Memo.t)
63

    
64
      let table_theta_d = (Memo.create () : (path_t, T.t) Memo.t)
65

    
66
      let table_theta_x = (Memo.create () : (path_t * frontier_t, T.t) Memo.t)
67

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

    
79
  module Memoize
80
      (Tables : MemoThetaTablesType)
81
      (Theta : ThetaType with type t = T.t) : MemoThetaType = struct
82
    type t = Theta.t
83

    
84
    let components call =
85
      Memo.fold (Tables.tables call) (fun k v res -> (k, v) :: res) []
86

    
87
    let theta : type a b. (a, b, t) theta_t =
88
     fun tag ->
89
      match tag with
90
      | J ->
91
        Theta.theta J
92
      | E ->
93
        Memo.apply3 (Tables.tables Ecall) (Theta.theta E)
94
      | D ->
95
        Memo.apply (Tables.tables Dcall) (Theta.theta D)
96
      | X ->
97
        Memo.apply2 (Tables.tables Xcall) (Theta.theta X)
98
  end
99

    
100
  module Modularize (Mod : ModularType) (Theta : MemoThetaType) :
101
    MemoThetaType = struct
102
    type t = Theta.t
103

    
104
    let mod_theta = (module Theta : ThetaType with type t = T.t)
105

    
106
    let components : type c. c call_t -> (c * t) list =
107
     fun call ->
108
      match call with
109
      | Ecall ->
110
        List.filter
111
          (fun ((p, p', f), _) -> Mod.modular E p p' f)
112
          (Theta.components Ecall)
113
      | Dcall ->
114
        List.filter (fun (p, _) -> Mod.modular D p) (Theta.components Dcall)
115
      | Xcall ->
116
        List.filter
117
          (fun ((p, f), _) -> Mod.modular X p f)
118
          (Theta.components Xcall)
119

    
120
    let theta : type a b. (a, b, t) theta_t =
121
     fun tag ->
122
      match tag with
123
      | J ->
124
        Theta.theta tag
125
      | E ->
126
        fun p p' f ->
127
          let theta_e = Theta.theta tag p p' f in
128
          if Mod.modular E p p' f then
129
            T.(eval_act mod_theta (call Ecall (p, p', f)))
130
          else theta_e
131
      | D ->
132
        fun p ->
133
          let theta_d = Theta.theta tag p in
134
          if Mod.modular D p then T.(eval_act mod_theta (call Dcall p))
135
          else theta_d
136
      | X ->
137
        fun p f ->
138
          let theta_x = Theta.theta tag p f in
139
          if Mod.modular X p f then T.(eval_act mod_theta (call Xcall (p, f)))
140
          else theta_x
141
  end
142

    
143
  module type ThetaifyType = functor (Kenv : KenvType) -> MemoThetaType
144

    
145
  module BasicThetaify : ThetaifyType =
146
  functor
147
    (Kenv : KenvType)
148
    ->
149
    struct
150
      type t = T.t
151

    
152
      let theta_ify : type a b. kenv_t -> (a, b, T.t) theta_t =
153
       fun kenv tag ->
154
        match tag with
155
        | J -> (
156
          fun j ->
157
            try List.assoc j kenv.cont_junc kenv
158
            with Not_found ->
159
              Format.eprintf "Lost junction %a@ " pp_junction_name j;
160
              assert false)
161
        | E -> (
162
          fun p ->
163
            try
164
              let e, _, _ = List.assoc p kenv.cont_node in
165
              e kenv
166
            with Not_found ->
167
              Format.eprintf "Entering lost path [%a]@." pp_path p;
168
              assert false)
169
        | D -> (
170
          fun p ->
171
            try
172
              let _, d, _ = List.assoc p kenv.cont_node in
173
              d kenv
174
            with Not_found ->
175
              Format.eprintf "During lost path [%a]@." pp_path p;
176
              assert false)
177
        | X -> (
178
          fun p ->
179
            try
180
              let _, _, x = List.assoc p kenv.cont_node in
181
              x kenv
182
            with Not_found ->
183
              Format.eprintf "Exiting lost path [%a]@." pp_path p;
184
              assert false)
185

    
186
      let theta tag = theta_ify Kenv.kenv tag
187

    
188
      let components _call = []
189
    end
190

    
191
  module ModularThetaify : functor
192
    (Tables : MemoThetaTablesType)
193
    (Mod : ModularType)
194
    -> ThetaifyType =
195
  functor
196
    (Tables : MemoThetaTablesType)
197
    (Mod : ModularType)
198
    (Kenv : KenvType)
199
    ->
200
    Modularize (Mod) (Memoize (Tables) (BasicThetaify (Kenv)))
201
end
(9-9/9)