Project

General

Profile

« Previous | Next » 

Revision ca7ff3f7

Added by LĂ©lio Brun 8 months ago

reformatting

View differences:

src/tools/stateflow/semantics/theta.ml
1
 open Basetypes 
1
open Basetypes
2

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

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

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

  
13
module KenvTheta (T : TransformerType) =
14
struct
11
   parametrized by the transformer specifying the type of the continuation.
12
   Evaluation of actions is also continuation dependent. *)
15 13

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

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

  
39
  module type KenvType =
40
  sig
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
41 39
    val kenv : kenv_t
42 40
  end
43 41

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

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

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

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

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

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

  
74
  module Memoize (Tables : MemoThetaTablesType) (Theta : ThetaType with type t = T.t) : MemoThetaType =
75
  struct
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
76 82
    type t = Theta.t
77 83

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

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

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

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

  
96 106
    let components : type c. c call_t -> (c * t) list =
97
      fun call ->
107
     fun call ->
98 108
      match call with
99
      | Ecall -> List.filter (fun ((p, p', f), _) -> Mod.modular E p p' f) (Theta.components Ecall)
100
      | Dcall -> List.filter (fun (p         , _) -> Mod.modular D p)      (Theta.components Dcall)
101
      | Xcall -> List.filter (fun ((p, f)    , _) -> Mod.modular X p f)    (Theta.components Xcall)
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)
102 119

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

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

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

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

  
151
    let theta tag = theta_ify Kenv.kenv tag
152

  
153
    let components _call = []
154
  end
155

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

  
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)))
160 201
end

Also available in: Unified diff