Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec / src / tools / stateflow / semantics / theta.ml @ 93119c3f

History | View | Annotate | Download (4.63 KB)

1
 open Basetypes 
2
(* open ActiveEnv *)
3
open CPS_transformer 
4
(* open Datatype *)
5
(* open Simulink *)
6

    
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
*)
12

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

    
16
  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
28
  }
29

    
30
	
31
  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
41
    val kenv : kenv_t
42
  end
43

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

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

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

    
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
76
    type t = Theta.t
77

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

    
81
    let theta : type a b. (a, b, t) theta_t =
82
      fun tag ->
83
      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)
88
  end
89
    
90
  module Modularize (Mod : ModularType) (Theta : MemoThetaType) : MemoThetaType =
91
  struct
92
    type t = Theta.t
93

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

    
96
    let components : type c. c call_t -> (c * t) list =
97
      fun call ->
98
      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)
102

    
103
    let theta : type a b. (a, b, t) theta_t =
104
      fun tag ->
105
      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)
119
  end
120

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

    
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

    
160
end