ctl/wrapper_ctl.mli

   1 (*
   2  * Copyright 2010, INRIA, University of Copenhagen
   3  * Julia Lawall, Rene Rydhof Hansen, Gilles Muller, Nicolas Palix
   4  * Copyright 2005-2009, Ecole des Mines de Nantes, University of Copenhagen
   5  * Yoann Padioleau, Julia Lawall, Rene Rydhof Hansen, Henrik Stuart, Gilles Muller, Nicolas Palix
   6  * This file is part of Coccinelle.
   7  *
   8  * Coccinelle is free software: you can redistribute it and/or modify
   9  * it under the terms of the GNU General Public License as published by
  10  * the Free Software Foundation, according to version 2 of the License.
  11  *
  12  * Coccinelle is distributed in the hope that it will be useful,
  13  * but WITHOUT ANY WARRANTY; without even the implied warranty of
  14  * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
  15  * GNU General Public License for more details.
  16  *
  17  * You should have received a copy of the GNU General Public License
  18  * along with Coccinelle.  If not, see <http://www.gnu.org/licenses/>.
  19  *
  20  * The authors reserve the right to distribute this or future versions of
  21  * Coccinelle under other licenses.
  22  *)
  23
  24
  25 (*
  26  * Copyright 2010, INRIA, University of Copenhagen
  27  * Julia Lawall, Rene Rydhof Hansen, Gilles Muller, Nicolas Palix
  28  * Copyright 2005-2009, Ecole des Mines de Nantes, University of Copenhagen
  29  * Yoann Padioleau, Julia Lawall, Rene Rydhof Hansen, Henrik Stuart, Gilles Muller, Nicolas Palix
  30  * This file is part of Coccinelle.
  31  *
  32  * Coccinelle is free software: you can redistribute it and/or modify
  33  * it under the terms of the GNU General Public License as published by
  34  * the Free Software Foundation, according to version 2 of the License.
  35  *
  36  * Coccinelle is distributed in the hope that it will be useful,
  37  * but WITHOUT ANY WARRANTY; without even the implied warranty of
  38  * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
  39  * GNU General Public License for more details.
  40  *
  41  * You should have received a copy of the GNU General Public License
  42  * along with Coccinelle.  If not, see <http://www.gnu.org/licenses/>.
  43  *
  44  * The authors reserve the right to distribute this or future versions of
  45  * Coccinelle under other licenses.
  46  *)
  47
  48
  49 type info = int
  50
  51 type ('pred, 'mvar) wrapped_ctl =
  52     ('pred * 'mvar Ast_ctl.modif,  'mvar, info) Ast_ctl.generic_ctl
  53
  54 type ('a, 'b) wrapped_binding =
  55     ClassicVal of 'a
  56   | PredVal of 'b Ast_ctl.modif
  57
  58 type ('pred,'state,'mvar,'value) labelfunc =
  59     'pred ->
  60       ('state * ('pred * ('mvar, 'value) Ast_ctl.generic_substitution))  list
  61
  62 module CTL_ENGINE_BIS :
  63   functor (SUB : Ctl_engine.SUBST) ->
  64     functor (G : Ctl_engine.GRAPH) ->
  65       functor(P : Ctl_engine.PREDICATE) ->
  66   sig
  67
  68     type predicate = P.t
  69     module WRAPPER_ENV :
  70         sig
  71           type mvar = SUB.mvar
  72           type value = (SUB.value, predicate) wrapped_binding
  73         end
  74     module WRAPPER_PRED :
  75         sig
  76           type t = P.t * SUB.mvar Ast_ctl.modif
  77         end
  78     module WRAPPER_ENGINE :
  79         sig
  80           type substitution =
  81               (WRAPPER_ENV.mvar, WRAPPER_ENV.value) Ast_ctl.generic_subst list
  82           type ('a, 'b) witness =
  83               (G.node, substitution,
  84                ('a, WRAPPER_ENV.mvar, 'b) Ast_ctl.generic_ctl list)
  85                 Ast_ctl.generic_witnesstree
  86           type ('a, 'b) triples =
  87               (G.node * substitution * ('a, 'b) witness list) list
  88         end
  89
  90
  91     val satbis_noclean :
  92         G.cfg *
  93         (predicate, G.node, WRAPPER_ENV.mvar, SUB.value) labelfunc *
  94         G.node list ->
  95           ((WRAPPER_PRED.t, WRAPPER_ENV.mvar, int) Ast_ctl.generic_ctl *
  96              (WRAPPER_PRED.t list list)) ->
  97                (WRAPPER_PRED.t, 'a) WRAPPER_ENGINE.triples
  98
  99     val satbis :
 100         G.cfg *
 101          (predicate,G.node,SUB.mvar,SUB.value) labelfunc *
 102          G.node list ->
 103            ((predicate,SUB.mvar) wrapped_ctl *
 104               (WRAPPER_PRED.t list list)) ->
 105                 (WRAPPER_ENV.mvar list * (SUB.mvar * SUB.value) list) ->
 106                   ((WRAPPER_PRED.t, 'a) WRAPPER_ENGINE.triples *
 107                      ((G.node * (SUB.mvar * SUB.value) list * predicate)
 108                         list list *
 109                         bool *
 110                         (WRAPPER_ENV.mvar * SUB.value) list list))
 111
 112     val print_bench : unit -> unit
 113 end