1 (* **********************************************************************
3 * Wrapping for FUNCTORS and MODULES
6 * $Id: wrapper_ctl.ml,v 1.67 2007/11/20 12:57:25 julia Exp $
8 * **********************************************************************)
12 type ('pred
, 'mvar
) wrapped_ctl
=
13 ('pred
* 'mvar
Ast_ctl.modif
, 'mvar
, info
) Ast_ctl.generic_ctl
15 type ('
value, 'pred
) wrapped_binding
=
16 | ClassicVal
of '
value
17 | PredVal
of 'pred
Ast_ctl.modif
19 type ('pred
,'state
,'mvar
,'
value) labelfunc
=
21 ('state
* ('pred
* ('mvar
, '
value) Ast_ctl.generic_substitution
)) list
23 (* pad: what is 'wit ? *)
24 type ('pred
,'state
,'mvar
,'
value,'wit
) wrapped_labelfunc
=
25 ('pred
* 'mvar
Ast_ctl.modif
) ->
27 ('mvar
,('
value,'pred
) wrapped_binding
) Ast_ctl.generic_substitution
*
31 (* ********************************************************************** *)
32 (* Module type: CTL_ENGINE_BIS (wrapper for CTL_ENGINE) *)
33 (* ********************************************************************** *)
35 (* This module must convert the labelling function passed as parameter, by
36 using convert_label. Then create a SUBST2 module handling the
37 wrapped_binding. Then it can instantiates the generic CTL_ENGINE
38 module. Call sat. And then process the witness tree to remove all that
39 is not revelevant for the transformation phase.
42 module CTL_ENGINE_BIS
=
43 functor (SUB
: Ctl_engine.SUBST
) ->
44 functor (G
: Ctl_engine.GRAPH
) ->
45 functor(P
: Ctl_engine.PREDICATE
) ->
48 exception TODO_CTL
of string (* implementation still not quite done so... *)
49 exception NEVER_CTL
of string (* Some things should never happen *)
57 type value = (SUB.value,predicate
) wrapped_binding
58 let eq_mvar = SUB.eq_mvar
61 | (ClassicVal
(v1
),ClassicVal
(v2
)) -> SUB.eq_val v1 v2
62 | (PredVal
(v1
),PredVal
(v2
)) -> v1
= v2
(* FIX ME: ok? *)
64 let merge_val wv1 wv2
=
66 | (ClassicVal
(v1
),ClassicVal
(v2
)) -> ClassicVal
(SUB.merge_val v1 v2
)
67 | _
-> wv1
(* FIX ME: ok? *)
70 let print_mvar x
= SUB.print_mvar x
73 ClassicVal v
-> SUB.print_value v
74 | PredVal
(A.Modif v
) -> P.print_predicate v
75 | PredVal
(A.UnModif v
) -> P.print_predicate v
76 | PredVal
(A.Control
) -> Format.print_string
"no value"
81 type t
= P.t
* SUB.mvar
Ast_ctl.modif
82 let print_predicate (pred
, modif
) =
84 P.print_predicate pred
;
86 Ast_ctl.Modif x
| Ast_ctl.UnModif x
->
87 Format.print_string
" with <modifTODO>"
88 | Ast_ctl.Control
-> ())
92 (* Instantiate a wrapped version of CTL_ENGINE *)
93 module WRAPPER_ENGINE
=
94 Ctl_engine.CTL_ENGINE
(WRAPPER_ENV
) (G
) (WRAPPER_PRED
)
96 (* Wrap a label function *)
97 let (wrap_label
: ('pred
,'state
,'mvar
,'
value) labelfunc
->
98 ('pred
,'state
,'mvar
,'
value,'wit
) wrapped_labelfunc
) =
104 | A.Modif
(x
) -> [A.Subst
(x
,PredVal
(A.Modif
(p'
)))]
105 | A.UnModif
(x
) -> [A.Subst
(x
,PredVal
(A.UnModif
(p'
)))]
110 | A.Subst
(x
,v
) -> A.Subst
(x
,ClassicVal
(v
))
111 | A.NegSubst
(x
,v
) -> A.NegSubst
(x
,ClassicVal
(v
)) in
113 let conv_trip (s
,(p'
,env
)) =
114 (s
,penv p'
@ (List.map
conv_sub env
),[](*pad: ?*))
116 List.map
conv_trip (oldlabelfunc p
)
118 (* ---------------------------------------------------------------- *)
120 (* FIX ME: what about negative witnesses and negative substitutions *)
121 let unwrap_wits modifonly wits
=
124 (function A.Subst
(x
,ClassicVal
(v
)) -> Some
(x
,v
) | _
-> None
)
126 let rec loop neg acc
= function
127 A.Wit
(st
,[A.Subst
(x
,PredVal
(A.Modif
(v
)))],anno
,wit
) ->
130 | _
-> raise
(NEVER_CTL
"predvar tree should have no children"))
131 | A.Wit
(st
,[A.Subst
(x
,PredVal
(A.UnModif
(v
)))],anno
,wit
)
132 when not modifonly
or !Flag.track_iso_usage
->
135 | _
-> raise
(NEVER_CTL
"predvar tree should have no children"))
136 | A.Wit
(st
,th
,anno
,wit
) ->
137 List.concat
(List.map
(loop neg
((mkth th
) @ acc
)) wit
)
138 | A.NegWit
(_
) -> [] (* why not failure? *) in
139 List.concat
(List.map
(function wit
-> loop false [] wit
) wits
)
143 (* a match can return many trees, but within each tree, there has to be
144 at most one value for each variable that is in the used_after list *)
145 let collect_used_after used_after envs
=
146 let print_var var
= SUB.print_mvar var
; Format.print_flush
() in
149 (function used_after_var
->
155 let vl = List.assoc used_after_var env
in
158 | Some old_vl
when SUB.eq_val vl old_vl
-> rest
159 | Some old_vl
-> print_var used_after_var
;
160 Format.print_newline
();
161 SUB.print_value old_vl
;
162 Format.print_newline
();
164 Format.print_newline
();
165 failwith
"incompatible values"
166 with Not_found
-> rest
)
170 | Some
vl -> [(used_after_var
, vl)])
174 (* a match can return many trees, but within each tree, there has to be
175 at most one value for each variable that is in the used_after list *)
176 (* actually, this should always be the case, because these variables
177 should be quantified at the top level. so the more complicated
178 definition above should not be needed. *)
179 let collect_used_after used_after envs
=
182 (function used_after_var
->
188 let vl = List.assoc used_after_var env
in
189 if List.exists
(function x
-> SUB.eq_val x
vl) rest
192 with Not_found
-> rest
)
194 List.map
(function x
-> (used_after_var
, x
)) vl)
197 (* ----------------------------------------------------- *)
199 (* The wrapper for sat from the CTL_ENGINE *)
200 let satbis_noclean (grp
,lab
,states
) (phi
,reqopt
) :
201 ('pred
,'anno
) WRAPPER_ENGINE.triples
=
202 WRAPPER_ENGINE.sat
(grp
,wrap_label lab
,states
) phi reqopt
204 (* Returns the "cleaned up" result from satbis_noclean *)
207 (predicate
,G.node
,SUB.mvar
,SUB.value) labelfunc
*
209 ((predicate
,SUB.mvar
) wrapped_ctl
*
210 (WRAPPER_PRED.t list list
)) ->
211 (WRAPPER_ENV.mvar list
* (SUB.mvar
* SUB.value) list
) ->
212 ((WRAPPER_PRED.t
, 'a
) WRAPPER_ENGINE.triples
*
213 ((G.node
* (SUB.mvar
* SUB.value) list
* predicate
)
216 (WRAPPER_ENV.mvar
* SUB.value) list list
))) =
217 fun m phi
(used_after
, binding
) ->
218 let noclean = satbis_noclean m phi
in
219 let witness_trees = List.map
(fun (_
,_
,w
) -> w
) noclean in
220 let res = List.map
(unwrap_wits true) witness_trees in
223 (function bindings_per_witness_tree
->
224 (List.map
(function (_
,env
,_
) -> env
) bindings_per_witness_tree
))
225 (List.map
(unwrap_wits false) witness_trees) in
227 (res,not
(noclean = []),
228 (* throw in the old binding. By construction it doesn't conflict
229 with any of the new things, and it is useful if there are no new
231 (List.map
(collect_used_after used_after
) new_bindings)))
233 let print_bench _
= WRAPPER_ENGINE.print_bench()
235 (* END OF MODULE: CTL_ENGINE_BIS *)