From 7cfc4e5146be5666419451bdd516f1f3f264d24a Mon Sep 17 00:00:00 2001
From: Enrico Tassi <gareuselesinge@debian.org>
Date: Sun, 25 Jan 2015 14:42:51 +0100
Subject: Imported Upstream version 8.5~beta1+dfsg

---
 plugins/cc/ccalgo.mli | 132 +++++++++++++++++++++++++++++++-------------------
 1 file changed, 83 insertions(+), 49 deletions(-)

(limited to 'plugins/cc/ccalgo.mli')

diff --git a/plugins/cc/ccalgo.mli b/plugins/cc/ccalgo.mli
index e4713728..c72843d5 100644
--- a/plugins/cc/ccalgo.mli
+++ b/plugins/cc/ccalgo.mli
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
@@ -10,40 +10,39 @@ open Util
 open Term
 open Names
 
+type pa_constructor =
+    { cnode : int;
+      arity : int;
+      args  : int list}
+
+type pa_fun=
+    {fsym:int;
+     fnargs:int}
+
+
+module PafMap : Map.S with type key = pa_fun
+module PacMap : Map.S with type key = pa_constructor
+
 type cinfo =
-    {ci_constr: constructor; (* inductive type *)
+    {ci_constr: pconstructor; (* inductive type *)
      ci_arity: int;     (* # args *)
      ci_nhyps: int}     (* # projectable args *)
 
 type term =
     Symb of constr
   | Product of sorts_family * sorts_family
-  | Eps of identifier
+  | Eps of Id.t
   | Appli of term*term
   | Constructor of cinfo (* constructor arity + nhyps *)
 
-val term_equal : term -> term -> bool
+module Constrhash : Hashtbl.S with type key = constr
+module Termhash : Hashtbl.S with type key = term
 
-type patt_kind =
-    Normal
-  | Trivial of types
-  | Creates_variables
 
 type ccpattern =
     PApp of term * ccpattern list
   | PVar of int
 
-type pa_constructor =
-    { cnode : int;
-      arity : int;
-      args  : int list}
-
-module PacMap : Map.S with type key = pa_constructor
-
-type forest
-
-type state
-
 type rule=
     Congruence
   | Axiom of constr * bool
@@ -61,17 +60,67 @@ type equality = rule eq
 
 type disequality = from eq
 
+type patt_kind =
+    Normal
+  | Trivial of types
+  | Creates_variables
+
+type quant_eq=
+    {qe_hyp_id: Id.t;
+     qe_pol: bool;
+     qe_nvars:int;
+     qe_lhs: ccpattern;
+     qe_lhs_valid:patt_kind;
+     qe_rhs: ccpattern;
+     qe_rhs_valid:patt_kind}
+
+type inductive_status =
+    Unknown
+  | Partial of pa_constructor
+  | Partial_applied
+  | Total of (int * pa_constructor)
+
+type representative=
+    {mutable weight:int;
+     mutable lfathers:Int.Set.t;
+     mutable fathers:Int.Set.t;
+     mutable inductive_status: inductive_status;
+     class_type : Term.types;
+     mutable functions: Int.Set.t PafMap.t} (*pac -> term = app(constr,t) *)
+
+type cl = Rep of representative| Eqto of int*equality
+
+type vertex = Leaf| Node of (int*int)
+
+type node =
+    {mutable clas:cl;
+     mutable cpath: int;
+     mutable constructors: int PacMap.t;
+     vertex:vertex;
+     term:term}
+
+type forest=
+    {mutable max_size:int;
+     mutable size:int;
+     mutable map: node array;
+     axioms: (term*term) Constrhash.t;
+     mutable epsilons: pa_constructor list;
+     syms: int Termhash.t}
+
+type state
+
 type explanation =
     Discrimination of (int*pa_constructor*int*pa_constructor)
   | Contradiction of disequality
   | Incomplete
 
-module Constrhash : Hashtbl.S with type key = constr
-module Termhash : Hashtbl.S with type key = term
+type matching_problem
+
+val term_equal : term -> term -> bool
 
 val constr_of_term : term -> constr
 
-val debug : (Pp.std_ppcmds -> unit) -> Pp.std_ppcmds -> unit
+val debug : Pp.std_ppcmds -> unit
 
 val forest : state -> forest
 
@@ -87,7 +136,7 @@ val add_equality : state -> constr -> term -> term -> unit
 
 val add_disequality : state -> from -> term -> term -> unit
 
-val add_quant : state -> identifier -> bool ->
+val add_quant : state -> Id.t -> bool ->
   int * patt_kind * ccpattern * patt_kind * ccpattern -> unit
 
 val tail_pac : pa_constructor -> pa_constructor
@@ -96,6 +145,8 @@ val find : forest -> int -> int
 
 val find_pac : forest -> int -> pa_constructor -> int
 
+val find_oldest_pac : forest -> int -> pa_constructor -> int
+
 val term : forest -> int -> term
 
 val get_constructor_info : forest -> int -> cinfo
@@ -105,25 +156,7 @@ val subterms : forest -> int -> int * int
 val join_path : forest -> int -> int ->
   ((int * int) * equality) list * ((int * int) * equality) list
 
-type quant_eq=
-    {qe_hyp_id: identifier;
-     qe_pol: bool;
-     qe_nvars:int;
-     qe_lhs: ccpattern;
-     qe_lhs_valid:patt_kind;
-     qe_rhs: ccpattern;
-     qe_rhs_valid:patt_kind}
-
-
-type pa_fun=
-    {fsym:int;
-     fnargs:int}
-
-type matching_problem
-
-module PafMap: Map.S with type key = pa_fun
-
-val make_fun_table : state -> Intset.t PafMap.t
+val make_fun_table : state -> Int.Set.t PafMap.t
 
 val do_match :  state ->
     (quant_eq * int array) list ref -> matching_problem Stack.t -> unit
@@ -136,8 +169,9 @@ val find_instances : state -> (quant_eq * int array) list
 
 val execute : bool -> state -> explanation option
 
+val pr_idx_term : forest -> int -> Pp.std_ppcmds
 
-
+val empty_forest: unit -> forest
 
 
 
@@ -161,7 +195,7 @@ type term =
 
 type rule =
     Congruence
-  | Axiom of Names.identifier
+  | Axiom of Names.Id.t
   | Injection of int*int*int*int
 
 type equality =
@@ -207,19 +241,19 @@ val process_rec : UF.t -> equality list -> int list
 val cc : UF.t -> unit
 
 val make_uf :
-  (Names.identifier * (term * term)) list -> UF.t
+  (Names.Id.t * (term * term)) list -> UF.t
 
 val add_one_diseq : UF.t -> (term * term) -> int * int
 
 val add_disaxioms :
-  UF.t -> (Names.identifier * (term * term)) list ->
-  (Names.identifier * (int * int)) list
+  UF.t -> (Names.Id.t * (term * term)) list ->
+  (Names.Id.t * (int * int)) list
 
 val check_equal : UF.t -> int * int -> bool
 
 val find_contradiction : UF.t ->
-  (Names.identifier * (int * int)) list ->
-  (Names.identifier * (int * int))
+  (Names.Id.t * (int * int)) list ->
+  (Names.Id.t * (int * int))
 *)
 
 
-- 
cgit v1.2.3