3 type ('pred
, 'mvar
) wrapped_ctl
=
4 ('pred
* 'mvar
Ast_ctl.modif
, 'mvar
, info
) Ast_ctl.generic_ctl
6 type ('a
, 'b
) wrapped_binding
=
8 | PredVal
of 'b
Ast_ctl.modif
10 type ('pred
,'state
,'mvar
,'
value) labelfunc
=
12 ('state
* ('pred
* ('mvar
, '
value) Ast_ctl.generic_substitution
)) list
14 module CTL_ENGINE_BIS
:
15 functor (SUB
: Ctl_engine.SUBST
) ->
16 functor (G
: Ctl_engine.GRAPH
) ->
17 functor(P
: Ctl_engine.PREDICATE
) ->
24 type value = (SUB.value, predicate
) wrapped_binding
28 type t
= P.t
* SUB.mvar
Ast_ctl.modif
30 module WRAPPER_ENGINE
:
33 (WRAPPER_ENV.mvar
, WRAPPER_ENV.value) Ast_ctl.generic_subst list
34 type ('a
, 'b
) witness
=
35 (G.node
, substitution
,
36 ('a
, WRAPPER_ENV.mvar
, 'b
) Ast_ctl.generic_ctl list
)
37 Ast_ctl.generic_witnesstree
38 type ('a
, 'b
) triples
=
39 (G.node
* substitution
* ('a
, 'b
) witness list
) list
45 (predicate
, G.node
, WRAPPER_ENV.mvar
, SUB.value) labelfunc
*
47 ((WRAPPER_PRED.t
, WRAPPER_ENV.mvar
, int) Ast_ctl.generic_ctl
*
48 (WRAPPER_PRED.t list list
)) ->
49 (WRAPPER_PRED.t
, 'a
) WRAPPER_ENGINE.triples
53 (predicate
,G.node
,SUB.mvar
,SUB.value) labelfunc
*
55 ((predicate
,SUB.mvar
) wrapped_ctl
*
56 (WRAPPER_PRED.t list list
)) ->
57 (WRAPPER_ENV.mvar list
* (SUB.mvar
* SUB.value) list
) ->
58 ((WRAPPER_PRED.t
, 'a
) WRAPPER_ENGINE.triples
*
59 ((G.node
* (SUB.mvar
* SUB.value) list
* predicate
)
62 (WRAPPER_ENV.mvar
* SUB.value) list list
))
64 val print_bench
: unit -> unit