1 files changed, 54 insertions, 68 deletions

diff --git a/plugins/cc/ccalgo.ml b/plugins/cc/ccalgo.ml
index bc53b113..8e53a044 100644
--- a/plugins/cc/ccalgo.ml
+++ b/plugins/cc/ccalgo.ml
@@ -1,24 +1,26 @@
 (************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
+(* <O___,, *       (see CREDITS file for the list of authors)           *)
 (*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
+(*    //   *    This file is distributed under the terms of the         *)
+(*         *     GNU Lesser General Public License Version 2.1          *)
+(*         *     (see LICENSE file for the text of the license)         *)
 (************************************************************************)
 
 (* This file implements the basic congruence-closure algorithm by *)
-(* Downey,Sethi and Tarjan. *)
+(* Downey, Sethi and Tarjan. *)
 (* Plus some e-matching and constructor handling by P. Corbineau *)
 
 open CErrors
-open Util
 open Pp
-open Goptions
 open Names
-open Term
+open Sorts
+open Constr
 open Vars
+open Goptions
 open Tacmach
-open Evd
+open Util
 
 let init_size=5
 
@@ -29,8 +31,7 @@ let debug x =
 
 let _=
   let gdopt=
-    { optsync=true;
-      optdepr=false;
+    { optdepr=false;
       optname="Congruence Verbose";
       optkey=["Congruence";"Verbose"];
       optread=(fun ()-> !cc_verbose);
@@ -62,7 +63,7 @@ module ST=struct
 
   let enter t sign st=
     if IntPairTable.mem st.toterm sign then
-	anomaly ~label:"enter" (Pp.str "signature already entered")
+	anomaly ~label:"enter" (Pp.str "signature already entered.")
     else
 	IntPairTable.replace st.toterm sign t;
 	IntTable.replace st.tosign t sign
@@ -136,7 +137,7 @@ let family_eq f1 f2 = match f1, f2 with
 
 type term=
     Symb of constr
-  | Product of sorts * sorts
+  | Product of Sorts.t * Sorts.t
   | Eps of Id.t
   | Appli of term*term
   | Constructor of cinfo (* constructor arity + nhyps *)
@@ -155,7 +156,7 @@ let rec term_equal t1 t2 =
 open Hashset.Combine
 
 let rec hash_term = function
-  | Symb c -> combine 1 (hash_constr c)
+  | Symb c -> combine 1 (Constr.hash c)
   | Product (s1, s2) -> combine3 2 (Sorts.hash s1) (Sorts.hash s2)
   | Eps i -> combine 3 (Id.hash i)
   | Appli (t1, t2) -> combine3 4 (hash_term t1) (hash_term t2)
@@ -216,7 +217,7 @@ type representative=
      mutable lfathers:Int.Set.t;
      mutable fathers:Int.Set.t;
      mutable inductive_status: inductive_status;
-     class_type : Term.types;
+     class_type : types;
      mutable functions: Int.Set.t PafMap.t} (*pac -> term = app(constr,t) *)
 
 type cl = Rep of representative| Eqto of int*equality
@@ -233,7 +234,7 @@ type node =
 module Constrhash = Hashtbl.Make
   (struct type t = constr
 	  let equal = eq_constr_nounivs
-	  let hash = hash_constr
+	  let hash = Constr.hash
    end)
 module Typehash = Constrhash
 
@@ -270,7 +271,8 @@ type state =
      mutable rew_depth:int;
      mutable changed:bool;
      by_type: Int.Set.t Typehash.t;
-     mutable gls:Proof_type.goal Tacmach.sigma}
+     mutable env:Environ.env;
+     sigma:Evd.evar_map}
 
 let dummy_node =
   {
@@ -305,7 +307,8 @@ let empty depth gls:state =
     rew_depth=depth;
     by_type=Constrhash.create init_size;
     changed=false;
-    gls=gls
+    env=pf_env gls;
+    sigma=project gls
   }
     
 let forest state = state.uf
@@ -322,7 +325,7 @@ let find uf i= find_aux uf [] i
 let get_representative uf i=
   match uf.map.(i).clas with
       Rep r -> r
-    | _ -> anomaly ~label:"get_representative" (Pp.str "not a representative")
+    | _ -> anomaly ~label:"get_representative" (Pp.str "not a representative.")
 
 let get_constructors uf i= uf.map.(i).constructors
 
@@ -340,7 +343,7 @@ let rec find_oldest_pac uf i pac=
 let get_constructor_info uf i=
   match uf.map.(i).term with
       Constructor cinfo->cinfo
-    | _ -> anomaly ~label:"get_constructor" (Pp.str "not a constructor")
+    | _ -> anomaly ~label:"get_constructor" (Pp.str "not a constructor.")
 
 let size uf i=
   (get_representative uf i).weight
@@ -385,7 +388,7 @@ let term uf i=uf.map.(i).term
 let subterms uf i=
   match uf.map.(i).vertex with
       Node(j,k) -> (j,k)
-    | _ -> anomaly ~label:"subterms" (Pp.str "not a node")
+    | _ -> anomaly ~label:"subterms" (Pp.str "not a node.")
 
 let signature uf i=
   let j,k=subterms uf i in (find uf j,find uf k)
@@ -424,7 +427,7 @@ let cc_product s1 s2 =
 	   mkLambda(_B_,mkSort(s2),_body_))
 
 let rec constr_of_term = function
-    Symb s-> applist_projection s []
+    Symb s-> s
   | Product(s1,s2) -> cc_product s1 s2
   | Eps id -> mkVar id
   | Constructor cinfo -> mkConstructU cinfo.ci_constr
@@ -432,37 +435,20 @@ let rec constr_of_term = function
       make_app [(constr_of_term s2)] s1
 and make_app l=function
     Appli (s1,s2)->make_app ((constr_of_term s2)::l) s1
-  | other -> 
-    applist_proj other l
-and applist_proj c l =
-  match c with
-  | Symb s -> applist_projection s l
-  | _ -> applistc (constr_of_term c) l
-and applist_projection c l =
-  match kind_of_term c with
-  | Const c when Environ.is_projection (fst c) (Global.env()) ->
-    let p = Projection.make (fst c) false in
-    (match l with 
-    | [] -> (* Expand the projection *)
-      let ty,_ = Typeops.type_of_constant (Global.env ()) c in
-      let pb = Environ.lookup_projection p (Global.env()) in
-      let ctx,_ = Term.decompose_prod_n_assum (pb.Declarations.proj_npars + 1) ty in
-	it_mkLambda_or_LetIn (mkProj(p,mkRel 1)) ctx
-    | hd :: tl ->
-      applistc (mkProj (p, hd)) tl)
-  | _ -> applistc c l
-
-let rec canonize_name c =
-  let func =  canonize_name in
-    match kind_of_term c with
+  | other -> Term.applist (constr_of_term other,l)
+
+let rec canonize_name sigma c =
+  let c = EConstr.Unsafe.to_constr c in
+  let func c = canonize_name sigma (EConstr.of_constr c) in
+    match Constr.kind c with
       | Const (kn,u) ->
-	  let canon_const = constant_of_kn (canonical_con kn) in 
+	  let canon_const = Constant.make1 (Constant.canonical kn) in 
 	    (mkConstU (canon_const,u))
       | Ind ((kn,i),u) ->
-	  let canon_mind = mind_of_kn (canonical_mind kn) in
+	  let canon_mind = MutInd.make1 (MutInd.canonical kn) in
 	    (mkIndU ((canon_mind,i),u))
       | Construct (((kn,i),j),u) ->
-	  let canon_mind = mind_of_kn (canonical_mind kn) in
+	  let canon_mind = MutInd.make1 (MutInd.canonical kn) in
 	    mkConstructU (((canon_mind,i),j),u)
       | Prod (na,t,ct) ->
 	  mkProd (na,func t, func ct)
@@ -474,7 +460,7 @@ let rec canonize_name c =
 	  mkApp (func ct,Array.smartmap func l)
       | Proj(p,c) ->
 	let p' = Projection.map (fun kn ->
-          constant_of_kn (canonical_con kn)) p in 
+          Constant.make1 (Constant.canonical kn)) p in 
 	  (mkProj (p', func c))
       | _ -> c
 
@@ -485,7 +471,7 @@ let build_subst uf subst =
     (fun i ->
       try term uf i
       with e when CErrors.noncritical e ->
-        anomaly (Pp.str "incomplete matching"))
+        anomaly (Pp.str "incomplete matching."))
     subst
 
 let rec inst_pattern subst = function
@@ -497,10 +483,10 @@ let rec inst_pattern subst = function
 	   args t
 
 let pr_idx_term uf i = str "[" ++ int i ++ str ":=" ++
-  Termops.print_constr (constr_of_term (term uf i)) ++ str "]"
+  Termops.print_constr (EConstr.of_constr (constr_of_term (term uf i))) ++ str "]"
 
 let pr_term t = str "[" ++
-  Termops.print_constr (constr_of_term t) ++ str "]"
+  Termops.print_constr (EConstr.of_constr (constr_of_term t)) ++ str "]"
 
 let rec add_term state t=
   let uf=state.uf in
@@ -508,8 +494,8 @@ let rec add_term state t=
 	Not_found ->
 	  let b=next uf in
           let trm = constr_of_term t in
-	  let typ = pf_unsafe_type_of state.gls trm in
-	  let typ = canonize_name typ in
+          let typ = Typing.unsafe_type_of state.env state.sigma (EConstr.of_constr trm) in
+          let typ = canonize_name state.sigma typ in
 	  let new_node=
 	    match t with
 		Symb _ | Product (_,_) ->
@@ -615,7 +601,7 @@ let add_inst state (inst,int_subst) =
 	      begin
 		debug (fun () ->
 		   (str "Adding new equality, depth="++ int state.rew_depth) ++ fnl () ++
-	          (str "  [" ++ Termops.print_constr prf ++ str " : " ++
+	          (str "  [" ++ Termops.print_constr (EConstr.of_constr prf) ++ str " : " ++
 			   pr_term s ++ str " == " ++ pr_term t ++ str "]"));
 		add_equality state prf s t
 	      end
@@ -623,7 +609,7 @@ let add_inst state (inst,int_subst) =
 	      begin
 		debug (fun () ->
 		   (str "Adding new disequality, depth="++ int state.rew_depth) ++ fnl () ++
-	          (str "  [" ++ Termops.print_constr prf ++ str " : " ++
+	          (str "  [" ++ Termops.print_constr (EConstr.of_constr prf) ++ str " : " ++
 			   pr_term s ++ str " <> " ++ pr_term t ++ str "]"));
 		add_disequality state (Hyp prf) s t
 	      end
@@ -750,7 +736,7 @@ let process_constructor_mark t i rep pac state =
 			state.combine;
 		      f (n-1) q1 q2
 		  | _-> anomaly ~label:"add_pacs"
-		      (Pp.str "weird error in injection subterms merge")
+		      (Pp.str "weird error in injection subterms merge.")
 	    in f cinfo.ci_nhyps opac.args pac.args
       | Partial_applied | Partial _ ->
 (*	  add_pac state.uf.map.(i) pac t; *)
@@ -817,11 +803,10 @@ let one_step state =
 let __eps__ = Id.of_string "_eps_"
 
 let new_state_var typ state =
-  let id = pf_get_new_id __eps__ state.gls in
-  let {it=gl ; sigma=sigma} = state.gls in
-  let gls = Goal.V82.new_goal_with sigma gl [Context.Named.Declaration.LocalAssum (id,typ)] in
-    state.gls<- gls;
-    id
+  let ids = Environ.ids_of_named_context_val (Environ.named_context_val state.env) in
+  let id = Namegen.next_ident_away __eps__ ids in
+  state.env<- EConstr.push_named (Context.Named.Declaration.LocalAssum (id,typ)) state.env;
+  id
 
 let complete_one_class state i=
   match (get_representative state.uf i).inductive_status with
@@ -829,18 +814,19 @@ let complete_one_class state i=
 	let rec app t typ n =
 	  if n<=0 then t else
 	    let _,etyp,rest= destProd typ in
-	    let id = new_state_var etyp state in
+            let id = new_state_var (EConstr.of_constr etyp) state in
 		app (Appli(t,Eps id)) (substl [mkVar id] rest) (n-1) in
-	let _c = pf_unsafe_type_of state.gls
-	  (constr_of_term (term state.uf pac.cnode)) in
+        let _c = Typing.unsafe_type_of state.env state.sigma
+	  (EConstr.of_constr (constr_of_term (term state.uf pac.cnode))) in
+        let _c = EConstr.Unsafe.to_constr _c in
 	let _args =
 	  List.map (fun i -> constr_of_term (term state.uf  i))
 	    pac.args in
-	let typ = prod_applist _c (List.rev _args) in
+        let typ = Term.prod_applist _c (List.rev _args) in
 	let ct = app (term state.uf i) typ pac.arity in
 	  state.uf.epsilons <- pac :: state.uf.epsilons;
 	  ignore (add_term state ct)
-    | _ -> anomaly (Pp.str "wrong incomplete class")
+    | _ -> anomaly (Pp.str "wrong incomplete class.")
 
 let complete state =
   Int.Set.iter (complete_one_class state) state.pa_classes
@@ -980,7 +966,7 @@ let find_instances state =
 	Control.check_for_interrupt ();
 	do_match state res pb_stack
       done;
-      anomaly (Pp.str "get out of here !")
+      anomaly (Pp.str "get out of here!")
     with Stack.Empty -> () in
     !res