1 files changed, 98 insertions, 108 deletions

diff --git a/plugins/cc/cctac.ml b/plugins/cc/cctac.ml
index 0baa5337..fd46d806 100644
--- a/plugins/cc/cctac.ml
+++ b/plugins/cc/cctac.ml
@@ -20,8 +20,10 @@ open Typing
 open Ccalgo
 open Ccproof
 open Pp
-open Errors
+open CErrors
 open Util
+open Proofview.Notations
+open Context.Rel.Declaration
 
 let reference dir s = lazy (Coqlib.gen_reference "CC" dir s)
 
@@ -36,17 +38,17 @@ let _True = reference ["Init";"Logic"] "True"
 let _I = reference ["Init";"Logic"] "I"
 
 let whd env=
-  let infos=Closure.create_clos_infos Closure.betaiotazeta env in
-    (fun t -> Closure.whd_val infos (Closure.inject t))
+  let infos=CClosure.create_clos_infos CClosure.betaiotazeta env in
+    (fun t -> CClosure.whd_val infos (CClosure.inject t))
 
 let whd_delta env=
-   let infos=Closure.create_clos_infos Closure.betadeltaiota env in
-    (fun t -> Closure.whd_val infos (Closure.inject t))
+   let infos=CClosure.create_clos_infos CClosure.all env in
+    (fun t -> CClosure.whd_val infos (CClosure.inject t))
 
 (* decompose member of equality in an applicative format *)
 
 (** FIXME: evar leak *)
-let sf_of env sigma c = sort_of env (ref sigma) c
+let sf_of env sigma c = e_sort_of env (ref sigma) c
 
 let rec decompose_term env sigma t=
     match kind_of_term (whd env t) with
@@ -80,8 +82,10 @@ let rec decompose_term env sigma t=
     | Proj (p, c) -> 
 	let canon_const kn = constant_of_kn (canonical_con kn) in 
 	let p' = Projection.map canon_const p in
-	  (Appli (Symb (mkConst (Projection.constant p')), decompose_term env sigma c))
-    | _ ->if closed0 t then (Symb t) else raise Not_found
+	(Appli (Symb (mkConst (Projection.constant p')), decompose_term env sigma c))
+    | _ ->
+       let t = strip_outer_cast t in
+       if closed0 t then Symb t else raise Not_found
 
 (* decompose equality in members and type *)
 open Globnames
@@ -151,7 +155,7 @@ let rec quantified_atom_of_constr env sigma nrels term =
 	  let patts=patterns_of_constr env sigma nrels atom in
 	      `Nrule patts
 	else 
-	  quantified_atom_of_constr (Environ.push_rel (id,None,atom) env) sigma (succ nrels) ff
+	  quantified_atom_of_constr (Environ.push_rel (LocalAssum (id,atom)) env) sigma (succ nrels) ff
     | _ ->  
 	let patts=patterns_of_constr env sigma nrels term in
 	    `Rule patts
@@ -166,7 +170,7 @@ let litteral_of_constr env sigma term=
 	else
 	  begin
 	    try 
-	      quantified_atom_of_constr (Environ.push_rel (id,None,atom) env) sigma 1 ff  
+	      quantified_atom_of_constr (Environ.push_rel (LocalAssum (id,atom)) env) sigma 1 ff
 	    with Not_found ->
 	      `Other (decompose_term env sigma term)
 	  end
@@ -187,7 +191,8 @@ let make_prb gls depth additionnal_terms =
 	 let t = decompose_term env sigma c in
 	   ignore (add_term state t)) additionnal_terms;
     List.iter
-      (fun (id,_,e) ->
+      (fun decl ->
+         let (id,_,e) = Context.Named.Declaration.to_tuple decl in
 	 begin
 	   let cid=mkVar id in
 	   match litteral_of_constr env sigma e with
@@ -220,24 +225,9 @@ let make_prb gls depth additionnal_terms =
 
 (* indhyps builds the array of arrays of constructor hyps for (ind largs) *)
 
-let build_projection intype outtype (cstr:pconstructor) special default gls=
-  let env=pf_env gls in
-  let (h,argv) = try destApp intype with DestKO -> (intype,[||]) in
-  let ind,u=destInd h in
-  let types=Inductiveops.arities_of_constructors env (ind,u) in
-  let lp=Array.length types in
-  let ci=pred (snd(fst cstr)) in
-  let branch i=
-    let ti= prod_appvect types.(i) argv in
-    let rc=fst (decompose_prod_assum ti) in
-    let head=
-      if Int.equal i ci then special else default in
-      it_mkLambda_or_LetIn head rc in
-  let branches=Array.init lp branch in
-  let casee=mkRel 1 in
-  let pred=mkLambda(Anonymous,intype,outtype) in
-  let case_info=make_case_info (pf_env gls) ind RegularStyle in
-  let body= mkCase(case_info, pred, casee, branches) in
+let build_projection intype (cstr:pconstructor) special default gls=
+  let ci= (snd(fst cstr)) in
+  let body=Equality.build_selector (pf_env gls) (project gls) ci (mkRel 1) intype special default in
   let id=pf_get_new_id (Id.of_string "t") gls in
     mkLambda(Name id,intype,body)
 
@@ -245,22 +235,34 @@ let build_projection intype outtype (cstr:pconstructor) special default gls=
 
 let _M =mkMeta
 
-let app_global f args k = 
+let app_global f args k =
   Tacticals.pf_constr_of_global (Lazy.force f) (fun fc -> k (mkApp (fc, args)))
 
-let new_app_global f args k = 
+let new_app_global f args k =
   Tacticals.New.pf_constr_of_global (Lazy.force f) (fun fc -> k (mkApp (fc, args)))
 
 let new_refine c = Proofview.V82.tactic (refine c)
 
 let assert_before n c =
-  Proofview.Goal.enter begin fun gl ->
+  Proofview.Goal.enter { enter = begin fun gl ->
     let evm, _ = Tacmach.New.pf_apply type_of gl c in
       Tacticals.New.tclTHEN (Proofview.V82.tactic (Refiner.tclEVARS evm)) (assert_before n c)
-  end
-    
+  end }
+
+let refresh_type env evm ty =
+  Evarsolve.refresh_universes ~status:Evd.univ_flexible ~refreshset:true
+			      (Some false) env evm ty
+
+let refresh_universes ty k =
+  Proofview.Goal.enter { enter = begin fun gl ->
+    let env = Proofview.Goal.env gl in
+    let evm = Tacmach.New.project gl in
+    let evm, ty = refresh_type env evm ty in
+    Tacticals.New.tclTHEN (Proofview.V82.tactic (Refiner.tclEVARS evm)) (k ty)
+  end }
+
 let rec proof_tac p : unit Proofview.tactic =
-  Proofview.Goal.nf_enter begin fun gl ->
+  Proofview.Goal.nf_enter { enter = begin fun gl ->
   let type_of t = Tacmach.New.pf_unsafe_type_of gl t in
   try (* type_of can raise exceptions *)
   match p.p_rule with
@@ -268,35 +270,31 @@ let rec proof_tac p : unit Proofview.tactic =
     | SymAx c ->
 	let l=constr_of_term p.p_lhs and
 	    r=constr_of_term p.p_rhs in
-        let typ = (* Termops.refresh_universes *) type_of l in
-        new_app_global _sym_eq [|typ;r;l;c|] exact_check
+	refresh_universes (type_of l) (fun typ ->
+        new_app_global _sym_eq [|typ;r;l;c|] exact_check)
     | Refl t ->
 	let lr = constr_of_term t in
-	let typ = (* Termops.refresh_universes *) type_of lr in
-        new_app_global _refl_equal [|typ;constr_of_term t|] exact_check
+	refresh_universes (type_of lr) (fun typ ->
+        new_app_global _refl_equal [|typ;constr_of_term t|] exact_check)
     | Trans (p1,p2)->
 	let t1 = constr_of_term p1.p_lhs and
 	    t2 = constr_of_term p1.p_rhs and
 	    t3 = constr_of_term p2.p_rhs in
-	let typ = (* Termops.refresh_universes *) (type_of t2) in
+	refresh_universes (type_of t2) (fun typ ->
 	let prf = new_app_global _trans_eq [|typ;t1;t2;t3;_M 1;_M 2|] in
-          Tacticals.New.tclTHENS (prf new_refine) [(proof_tac p1);(proof_tac p2)]
+          Tacticals.New.tclTHENS (prf new_refine) [(proof_tac p1);(proof_tac p2)])
     | Congr (p1,p2)->
 	let tf1=constr_of_term p1.p_lhs
 	and tx1=constr_of_term p2.p_lhs
 	and tf2=constr_of_term p1.p_rhs
 	and tx2=constr_of_term p2.p_rhs in
-	let typf = (* Termops.refresh_universes  *)(type_of tf1) in
-	let typx = (* Termops.refresh_universes *) (type_of tx1) in
-	let typfx = (* Termops.refresh_universes *) (type_of (mkApp (tf1,[|tx1|]))) in
+	refresh_universes (type_of tf1) (fun typf ->
+	refresh_universes (type_of tx1) (fun typx ->
+	refresh_universes (type_of (mkApp (tf1,[|tx1|]))) (fun typfx ->
         let id = Tacmach.New.of_old (fun gls -> pf_get_new_id (Id.of_string "f") gls) gl in
 	let appx1 = mkLambda(Name id,typf,mkApp(mkRel 1,[|tx1|])) in
-	let lemma1 =
-	  app_global _f_equal
-		[|typf;typfx;appx1;tf1;tf2;_M 1|] in
-	let lemma2=
-	  app_global _f_equal
-		[|typx;typfx;tf2;tx1;tx2;_M 1|] in
+	let lemma1 = app_global _f_equal [|typf;typfx;appx1;tf1;tf2;_M 1|] in
+	let lemma2 = app_global _f_equal [|typx;typfx;tf2;tx1;tx2;_M 1|] in
 	let prf =
 	  app_global _trans_eq
 		[|typfx;
@@ -310,96 +308,89 @@ let rec proof_tac p : unit Proofview.tactic =
 		reflexivity;
                 Tacticals.New.tclZEROMSG
 		    (Pp.str
-		       "I don't know how to handle dependent equality")]]
+		       "I don't know how to handle dependent equality")]])))
   | Inject (prf,cstr,nargs,argind) ->
 	 let ti=constr_of_term prf.p_lhs in
 	 let tj=constr_of_term prf.p_rhs in
 	 let default=constr_of_term p.p_lhs in
-	 let intype = (* Termops.refresh_universes *) (type_of ti) in
-	 let outtype = (* Termops.refresh_universes *) (type_of default) in
 	 let special=mkRel (1+nargs-argind) in
+	 refresh_universes (type_of ti) (fun intype ->
+         refresh_universes (type_of default) (fun outtype ->
          let proj =
-           Tacmach.New.of_old (build_projection intype outtype cstr special default) gl
+           Tacmach.New.of_old (build_projection intype cstr special default) gl
          in
 	 let injt=
            app_global _f_equal [|intype;outtype;proj;ti;tj;_M 1|] in
-	   Tacticals.New.tclTHEN (Proofview.V82.tactic (injt refine)) (proof_tac prf)
+	   Tacticals.New.tclTHEN (Proofview.V82.tactic (injt refine)) (proof_tac prf)))
   with e when Proofview.V82.catchable_exception e -> Proofview.tclZERO e
-  end
+  end }
 
 let refute_tac c t1 t2 p =
-  Proofview.Goal.nf_enter begin fun gl ->
+  Proofview.Goal.nf_enter { enter = begin fun gl ->
   let tt1=constr_of_term t1 and tt2=constr_of_term t2 in
-  let intype =
-    Tacmach.New.of_old (fun gls -> (* Termops.refresh_universes *) (pf_unsafe_type_of gls tt1)) gl
-  in
-  let neweq= new_app_global _eq [|intype;tt1;tt2|] in
   let hid = Tacmach.New.of_old (pf_get_new_id (Id.of_string "Heq")) gl in
   let false_t=mkApp (c,[|mkVar hid|]) in
+  let k intype =
+    let neweq= new_app_global _eq [|intype;tt1;tt2|] in
     Tacticals.New.tclTHENS (neweq (assert_before (Name hid)))
       [proof_tac p; simplest_elim false_t]
-  end
+  in refresh_universes (Tacmach.New.pf_unsafe_type_of gl tt1) k
+  end }
 
 let refine_exact_check c gl =
   let evm, _ = pf_apply type_of gl c in
     Tacticals.tclTHEN (Refiner.tclEVARS evm) (Proofview.V82.of_tactic (exact_check c)) gl
 
 let convert_to_goal_tac c t1 t2 p = 
-  Proofview.Goal.nf_enter begin fun gl ->
+  Proofview.Goal.nf_enter { enter = begin fun gl ->
   let tt1=constr_of_term t1 and tt2=constr_of_term t2 in
-  let sort =
-    Tacmach.New.of_old (fun gls -> (* Termops.refresh_universes *) (pf_unsafe_type_of gls tt2)) gl
-  in
-  let neweq= new_app_global _eq [|sort;tt1;tt2|] in
-  let e = Tacmach.New.of_old (pf_get_new_id (Id.of_string "e")) gl in
-  let x = Tacmach.New.of_old (pf_get_new_id (Id.of_string "X")) gl in
-  let identity=mkLambda (Name x,sort,mkRel 1) in
-  let endt=app_global _eq_rect [|sort;tt1;identity;c;tt2;mkVar e|] in
+  let k sort =
+    let neweq= new_app_global _eq [|sort;tt1;tt2|] in
+    let e = Tacmach.New.of_old (pf_get_new_id (Id.of_string "e")) gl in
+    let x = Tacmach.New.of_old (pf_get_new_id (Id.of_string "X")) gl in
+    let identity=mkLambda (Name x,sort,mkRel 1) in
+    let endt=app_global _eq_rect [|sort;tt1;identity;c;tt2;mkVar e|] in
     Tacticals.New.tclTHENS (neweq (assert_before (Name e)))
-      [proof_tac p; Proofview.V82.tactic (endt refine_exact_check)]
-  end
+			   [proof_tac p; Proofview.V82.tactic (endt refine_exact_check)]
+  in refresh_universes (Tacmach.New.pf_unsafe_type_of gl tt2) k
+  end }
 
 let convert_to_hyp_tac c1 t1 c2 t2 p =
-  Proofview.Goal.nf_enter begin fun gl ->
+  Proofview.Goal.nf_enter { enter = begin fun gl ->
   let tt2=constr_of_term t2 in
   let h = Tacmach.New.of_old (pf_get_new_id (Id.of_string "H")) gl in
   let false_t=mkApp (c2,[|mkVar h|]) in
     Tacticals.New.tclTHENS (assert_before (Name h) tt2)
       [convert_to_goal_tac c1 t1 t2 p;
        simplest_elim false_t]
-  end
+  end }
 
 let discriminate_tac (cstr,u as cstru) p =
-  Proofview.Goal.nf_enter begin fun gl ->
+  Proofview.Goal.nf_enter { enter = begin fun gl ->
     let t1=constr_of_term p.p_lhs and t2=constr_of_term p.p_rhs in
-    let intype =
-      Tacmach.New.of_old (fun gls -> (* Termops.refresh_universes *) (pf_unsafe_type_of gls t1)) gl
-    in
+    let env = Proofview.Goal.env gl in
     let concl = Proofview.Goal.concl gl in
-    (* let evm,outsort = Evd.new_sort_variable Evd.univ_rigid (project gls) in  *)
-    (* let outsort = mkSort outsort in *)
     let xid = Tacmach.New.of_old (pf_get_new_id (Id.of_string "X")) gl in
-    (* let tid = Tacmach.New.of_old (pf_get_new_id (Id.of_string "t")) gl in *)
-    (* let identity=mkLambda(Name xid,outsort,mkLambda(Name tid,mkRel 1,mkRel 1)) in *)
     let identity = Universes.constr_of_global (Lazy.force _I) in
-    (* let trivial=pf_unsafe_type_of gls identity in *)
     let trivial = Universes.constr_of_global (Lazy.force _True) in
-    let evm, outtype = Evd.new_sort_variable Evd.univ_flexible (Proofview.Goal.sigma gl) in 
+    let evm = Tacmach.New.project gl in
+    let evm, intype = refresh_type env evm (Tacmach.New.pf_unsafe_type_of gl t1) in
+    let evm, outtype = Evd.new_sort_variable Evd.univ_flexible evm in
     let outtype = mkSort outtype in
-    let pred=mkLambda(Name xid,outtype,mkRel 1) in
+    let pred = mkLambda(Name xid,outtype,mkRel 1) in
     let hid = Tacmach.New.of_old (pf_get_new_id (Id.of_string "Heq")) gl in
-    let proj = Tacmach.New.of_old (build_projection intype outtype cstru trivial concl) gl in
+    let proj = Tacmach.New.of_old (build_projection intype cstru trivial concl) gl in
     let injt=app_global _f_equal
-                    [|intype;outtype;proj;t1;t2;mkVar hid|] in
+			[|intype;outtype;proj;t1;t2;mkVar hid|] in
     let endt k =
       injt (fun injt ->
-        app_global _eq_rect
-          [|outtype;trivial;pred;identity;concl;injt|] k) in
+            app_global _eq_rect
+		       [|outtype;trivial;pred;identity;concl;injt|] k) in
     let neweq=new_app_global _eq [|intype;t1;t2|] in
     Tacticals.New.tclTHEN (Proofview.Unsafe.tclEVARS evm)
-      (Tacticals.New.tclTHENS (neweq (assert_before (Name hid)))
-        [proof_tac p; Proofview.V82.tactic (endt refine_exact_check)])
-  end
+			  (Tacticals.New.tclTHENS (neweq (assert_before (Name hid)))
+      [proof_tac p; Proofview.V82.tactic (endt refine_exact_check)])
+  end }
 
 (* wrap everything *)
 
@@ -411,18 +402,18 @@ let build_term_to_complete uf meta pac =
     applistc (mkConstructU cinfo.ci_constr) all_args
 
 let cc_tactic depth additionnal_terms =
-  Proofview.Goal.nf_enter begin fun gl ->
+  Proofview.Goal.nf_enter { enter = begin fun gl ->
     Coqlib.check_required_library Coqlib.logic_module_name;
-    let _ = debug (Pp.str "Reading subgoal ...") in
+    let _ = debug (fun () -> Pp.str "Reading subgoal ...") in
     let state = Tacmach.New.of_old (fun gls -> make_prb gls depth additionnal_terms) gl in
-    let _ = debug (Pp.str "Problem built, solving ...") in
+    let _ = debug (fun () -> Pp.str "Problem built, solving ...") in
     let sol = execute true state in
-    let _ = debug (Pp.str "Computation completed.") in
+    let _ = debug (fun () -> Pp.str "Computation completed.") in
     let uf=forest state in
     match sol with
       None -> Tacticals.New.tclFAIL 0 (str "congruence failed")
     | Some reason ->
-	debug (Pp.str "Goal solved, generating proof ...");
+	debug (fun () -> Pp.str "Goal solved, generating proof ...");
 	match reason with
 	  Discrimination (i,ipac,j,jpac) ->
 	    let p=build_proof uf (`Discr (i,ipac,j,jpac)) in
@@ -436,10 +427,10 @@ let cc_tactic depth additionnal_terms =
 	      List.map
 		(build_term_to_complete uf newmeta)
 		(epsilons uf) in
-	    Pp.msg_info
+	    Feedback.msg_info
 	      (Pp.str "Goal is solvable by congruence but \
  some arguments are missing.");
-	    Pp.msg_info
+	    Feedback.msg_info
 	      (Pp.str "  Try " ++
 		 hov 8
 		 begin
@@ -462,7 +453,7 @@ let cc_tactic depth additionnal_terms =
 		convert_to_goal_tac id ta tb p
 	    | HeqnH (ida,idb) ->
 		convert_to_hyp_tac ida ta idb tb p
-  end
+  end }
 
 let cc_fail gls =
   errorlabstrm  "Congruence" (Pp.str "congruence failed.")
@@ -482,11 +473,10 @@ let congruence_tac depth l =
    This isn't particularly related with congruence, apart from
    the fact that congruence is called internally.
 *)
-    
+
 let mk_eq f c1 c2 k =
   Tacticals.New.pf_constr_of_global (Lazy.force f) (fun fc ->
-  Proofview.Goal.enter begin
-    fun gl ->
+  Proofview.Goal.enter { enter = begin fun gl ->
     let open Tacmach.New in
     let evm, ty = pf_apply type_of gl c1 in
     let evm, ty = Evarsolve.refresh_universes (Some false) (pf_env gl) evm ty in
@@ -494,10 +484,10 @@ let mk_eq f c1 c2 k =
     let evm, _ =  type_of (pf_env gl) evm term in
     Tacticals.New.tclTHEN (Proofview.V82.tactic (Refiner.tclEVARS evm))
 			  (k term)
-    end)
-    
+    end })
+
 let f_equal =
-  Proofview.Goal.nf_enter begin fun gl ->
+  Proofview.Goal.nf_enter { enter = begin fun gl ->
     let concl = Proofview.Goal.concl gl in
     let cut_eq c1 c2 =
       try (* type_of can raise an exception *)
@@ -523,4 +513,4 @@ let f_equal =
         | Type_errors.TypeError _ -> Proofview.tclUNIT ()
         | e -> Proofview.tclZERO ~info e
       end
-  end
+  end }