## lustrec/src/tools/stateflow/semantics/theta.ml @ ca7ff3f7

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
``` |