Project

General

Profile

Download (5.26 KB) Statistics
| Branch: | Tag: | Revision:
1 ca7ff3f7 Lélio Brun
open Basetypes
2
3 2de7fa82 ploc
(* open ActiveEnv *)
4 ca7ff3f7 Lélio Brun
open CPS_transformer
5
6 2de7fa82 ploc
(* open Datatype *)
7
(* open Simulink *)
8
9 ca7ff3f7 Lélio Brun
(* Theta functions interfaces including memoization when using modular calls
10 2de7fa82 ploc
11 ca7ff3f7 Lélio Brun
   parametrized by the transformer specifying the type of the continuation.
12
   Evaluation of actions is also continuation dependent. *)
13 2de7fa82 ploc
14 ca7ff3f7 Lélio Brun
module KenvTheta (T : TransformerType) = struct
15 2de7fa82 ploc
  type kenv_t = {
16 ca7ff3f7 Lélio Brun
    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 2de7fa82 ploc
  }
27
28
  let init_env src =
29 ca7ff3f7 Lélio Brun
    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 2de7fa82 ploc
    val kenv : kenv_t
40
  end
41
42 ca7ff3f7 Lélio Brun
  module type MemoThetaTablesType = sig
43 2de7fa82 ploc
    val tables : 'c call_t -> ('c, T.t) Memo.t
44
  end
45
46 ca7ff3f7 Lélio Brun
  module type MemoThetaType = sig
47 2de7fa82 ploc
    include ThetaType with type t = T.t
48 ca7ff3f7 Lélio Brun
49 2de7fa82 ploc
    val components : 'c call_t -> ('c * t) list
50
  end
51
52 ca7ff3f7 Lélio Brun
  module type ModularType = sig
53 2de7fa82 ploc
    val modular : (path_t, 'b, bool) tag_t -> path_t -> 'b
54
  end
55
56 ca7ff3f7 Lélio Brun
  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 2de7fa82 ploc
    type t = Theta.t
83
84
    let components call =
85 ca7ff3f7 Lélio Brun
      Memo.fold (Tables.tables call) (fun k v res -> (k, v) :: res) []
86 2de7fa82 ploc
87
    let theta : type a b. (a, b, t) theta_t =
88 ca7ff3f7 Lélio Brun
     fun tag ->
89 2de7fa82 ploc
      match tag with
90 ca7ff3f7 Lélio Brun
      | 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 2de7fa82 ploc
  end
99 ca7ff3f7 Lélio Brun
100
  module Modularize (Mod : ModularType) (Theta : MemoThetaType) :
101
    MemoThetaType = struct
102 2de7fa82 ploc
    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 ca7ff3f7 Lélio Brun
     fun call ->
108 2de7fa82 ploc
      match call with
109 ca7ff3f7 Lélio Brun
      | 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 2de7fa82 ploc
120
    let theta : type a b. (a, b, t) theta_t =
121 ca7ff3f7 Lélio Brun
     fun tag ->
122 2de7fa82 ploc
      match tag with
123 ca7ff3f7 Lélio Brun
      | 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 2de7fa82 ploc
  end
142
143
  module type ThetaifyType = functor (Kenv : KenvType) -> MemoThetaType
144
145 ca7ff3f7 Lélio Brun
  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 2de7fa82 ploc
end