Cc API using EConstr.

5 files changed, 86 insertions, 67 deletions

diff --git a/plugins/cc/cctac.ml b/plugins/cc/cctac.ml
index 130f01e97..0d48b65d0 100644
--- a/plugins/cc/cctac.ml
+++ b/plugins/cc/cctac.ml
@@ -13,6 +13,7 @@ open Names
 open Inductiveops
 open Declarations
 open Term
+open EConstr
 open Vars
 open Tacmach
 open Tactics
@@ -27,6 +28,10 @@ open Proofview.Notations
 module RelDecl = Context.Rel.Declaration
 module NamedDecl = Context.Named.Declaration
 
+let local_assum (na, t) =
+  let inj = EConstr.Unsafe.to_constr in
+  RelDecl.LocalAssum (na, inj t)
+
 let reference dir s = lazy (Coqlib.gen_reference "CC" dir s)
 
 let _f_equal = reference ["Init";"Logic"] "f_equal"
@@ -39,27 +44,26 @@ let _False = reference ["Init";"Logic"] "False"
 let _True = reference ["Init";"Logic"] "True"
 let _I = reference ["Init";"Logic"] "I"
 
-let whd env=
-  let infos=CClosure.create_clos_infos CClosure.betaiotazeta env in
-    (fun t -> CClosure.whd_val infos (CClosure.inject t))
+let whd env sigma t =
+  Reductionops.clos_whd_flags CClosure.betaiotazeta env sigma t
 
-let whd_delta env=
-   let infos=CClosure.create_clos_infos CClosure.all env in
-    (fun t -> CClosure.whd_val infos (CClosure.inject t))
+let whd_delta env sigma t =
+  Reductionops.clos_whd_flags CClosure.all env sigma t
 
 (* decompose member of equality in an applicative format *)
 
 (** FIXME: evar leak *)
-let sf_of env sigma c = e_sort_of env (ref sigma) (EConstr.of_constr 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
+    match EConstr.kind sigma (whd env sigma t) with
       App (f,args)->
 	let tf=decompose_term env sigma f in
 	let targs=Array.map (decompose_term env sigma) args in
 	  Array.fold_left (fun s t->Appli (s,t)) tf targs
-    | Prod (_,a,_b) when EConstr.Vars.noccurn sigma 1 (EConstr.of_constr _b) ->
-	let b = Termops.pop (EConstr.of_constr _b) in
+    | Prod (_,a,_b) when noccurn sigma 1 _b ->
+	let b = Termops.pop _b in
+	let b = EConstr.of_constr b in
 	let sort_b = sf_of env sigma b in
 	let sort_a = sf_of env sigma a in
 	Appli(Appli(Product (sort_a,sort_b) ,
@@ -77,28 +81,27 @@ let rec decompose_term env sigma t=
     | Ind c -> 
 	let (mind,i_ind),u = c in 
 	let canon_mind = mind_of_kn (canonical_mind mind) in
-	let canon_ind = canon_mind,i_ind in  (Symb (mkIndU (canon_ind,u)))
+	let canon_ind = canon_mind,i_ind in  (Symb (Constr.mkIndU (canon_ind,u)))
     | Const (c,u) -> 
 	let canon_const = constant_of_kn (canonical_con c) in 
-	  (Symb (mkConstU (canon_const,u)))
+	  (Symb (Constr.mkConstU (canon_const,u)))
     | 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))
+	(Appli (Symb (Constr.mkConst (Projection.constant p')), decompose_term env sigma c))
     | _ ->
-       let t = Termops.strip_outer_cast sigma (EConstr.of_constr t) in
-       let t = EConstr.Unsafe.to_constr t in
-       if closed0 t then Symb t else raise Not_found
+       let t = Termops.strip_outer_cast sigma t in
+       if closed0 sigma t then Symb (EConstr.to_constr sigma t) else raise Not_found
 
 (* decompose equality in members and type *)
-open Globnames
+open Termops
 
 let atom_of_constr env sigma term =
-  let wh =  (whd_delta env term) in
-  let kot = kind_of_term wh in
+  let wh = whd_delta env sigma term in
+  let kot = EConstr.kind sigma wh in
     match kot with
       App (f,args)->
-	if is_global (Lazy.force _eq) f && Int.equal (Array.length args) 3
+	if is_global sigma (Lazy.force _eq) f && Int.equal (Array.length args) 3
 	  then `Eq (args.(0),
 		   decompose_term env sigma args.(1),
 		   decompose_term env sigma args.(2))
@@ -106,15 +109,16 @@ let atom_of_constr env sigma term =
     | _ -> `Other (decompose_term env sigma term)
 
 let rec pattern_of_constr env sigma c =
-  match kind_of_term (whd env c) with
+  match EConstr.kind sigma (whd env sigma c) with
       App (f,args)->
 	let pf = decompose_term env sigma f in
 	let pargs,lrels = List.split
 	  (Array.map_to_list (pattern_of_constr env sigma) args) in
 	  PApp (pf,List.rev pargs),
 	List.fold_left Int.Set.union Int.Set.empty lrels
-    | Prod (_,a,_b) when EConstr.Vars.noccurn sigma 1 (EConstr.of_constr _b) ->
-	let b = Termops.pop (EConstr.of_constr _b) in
+    | Prod (_,a,_b) when noccurn sigma 1 _b ->
+	let b = Termops.pop _b in
+	let b = EConstr.of_constr b in
 	let pa,sa = pattern_of_constr env sigma a in
 	let pb,sb = pattern_of_constr env sigma b in
 	let sort_b = sf_of env sigma b in
@@ -132,19 +136,19 @@ let non_trivial = function
 
 let patterns_of_constr env sigma nrels term=
   let f,args=
-    try destApp (whd_delta env term) with DestKO -> raise Not_found in
-	if is_global (Lazy.force _eq) f && Int.equal (Array.length args) 3
+    try destApp sigma (whd_delta env sigma term) with DestKO -> raise Not_found in
+	if is_global sigma (Lazy.force _eq) f && Int.equal (Array.length args) 3
 	then
 	  let patt1,rels1 = pattern_of_constr env sigma args.(1)
 	  and patt2,rels2 = pattern_of_constr env sigma args.(2) in
 	  let valid1 =
 	    if not (Int.equal (Int.Set.cardinal rels1) nrels) then Creates_variables
 	    else if non_trivial patt1 then Normal
-	    else Trivial args.(0)
+	    else Trivial (EConstr.to_constr sigma args.(0))
 	  and valid2 =
 	    if not (Int.equal (Int.Set.cardinal rels2) nrels) then Creates_variables
 	    else if non_trivial patt2 then Normal
-	    else Trivial args.(0) in
+	    else Trivial (EConstr.to_constr sigma args.(0)) in
 	    if valid1 != Creates_variables
 	      || valid2 != Creates_variables  then
 	      nrels,valid1,patt1,valid2,patt2
@@ -152,28 +156,28 @@ let patterns_of_constr env sigma nrels term=
 	else raise Not_found
 
 let rec quantified_atom_of_constr env sigma nrels term =
-  match kind_of_term (whd_delta env term) with
+  match EConstr.kind sigma (whd_delta env sigma term) with
       Prod (id,atom,ff) -> 
-	if is_global (Lazy.force _False) ff then
+	if is_global sigma (Lazy.force _False) ff then
 	  let patts=patterns_of_constr env sigma nrels atom in
 	      `Nrule patts
 	else 
-	  quantified_atom_of_constr (Environ.push_rel (RelDecl.LocalAssum (id,atom)) env) sigma (succ nrels) ff
+	  quantified_atom_of_constr (Environ.push_rel (local_assum (id,atom)) env) sigma (succ nrels) ff
     | _ ->  
 	let patts=patterns_of_constr env sigma nrels term in
 	    `Rule patts
 
 let litteral_of_constr env sigma term=
-  match kind_of_term (whd_delta env term) with
+  match EConstr.kind sigma (whd_delta env sigma term) with
     | Prod (id,atom,ff) -> 
-	if is_global (Lazy.force _False) ff then
+	if is_global sigma (Lazy.force _False) ff then
 	  match (atom_of_constr env sigma atom) with
 	      `Eq(t,a,b) -> `Neq(t,a,b)
 	    | `Other(p) -> `Nother(p)
 	else
 	  begin
 	    try 
-	      quantified_atom_of_constr (Environ.push_rel (RelDecl.LocalAssum (id,atom)) env) sigma 1 ff
+	      quantified_atom_of_constr (Environ.push_rel (local_assum (id,atom)) env) sigma 1 ff
 	    with Not_found ->
 	      `Other (decompose_term env sigma term)
 	  end
@@ -197,8 +201,8 @@ let make_prb gls depth additionnal_terms =
       (fun decl ->
          let id = NamedDecl.get_id decl in
 	 begin
-	   let cid=mkVar id in
-	   match litteral_of_constr env sigma (NamedDecl.get_type decl) with
+	   let cid=Constr.mkVar id in
+	   match litteral_of_constr env sigma (EConstr.of_constr (NamedDecl.get_type decl)) with
 	       `Eq (t,a,b) -> add_equality state cid a b
 	     | `Neq (t,a,b) -> add_disequality state (Hyp cid) a b
 	     | `Other ph ->
@@ -217,7 +221,7 @@ let make_prb gls depth additionnal_terms =
 	     | `Nrule patts -> add_quant state id false patts
 	 end) (Environ.named_context_of_val (Goal.V82.nf_hyps gls.sigma gls.it));
     begin
-      match atom_of_constr env sigma (Evarutil.nf_evar sigma (pf_concl gls)) with
+      match atom_of_constr env sigma (EConstr.of_constr (pf_concl gls)) with
 	  `Eq (t,a,b) -> add_disequality state Goal a b
 	|	`Other g ->
 		  List.iter
@@ -230,8 +234,7 @@ let make_prb gls depth additionnal_terms =
 
 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 (EConstr.mkRel 1) (EConstr.of_constr intype) (EConstr.of_constr special) default in
-  let body = EConstr.Unsafe.to_constr body 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)
 
@@ -240,10 +243,10 @@ let build_projection intype (cstr:pconstructor) special default gls=
 let _M =mkMeta
 
 let app_global f args k =
-  Tacticals.pf_constr_of_global (Lazy.force f) (fun fc -> k (EConstr.of_constr (mkApp (fc, args))))
+  Tacticals.pf_constr_of_global (Lazy.force f) (fun fc -> k (mkApp (EConstr.of_constr fc, args)))
 
 let new_app_global f args k =
-  Tacticals.New.pf_constr_of_global (Lazy.force f) (fun fc -> k (EConstr.of_constr (mkApp (fc, args))))
+  Tacticals.New.pf_constr_of_global (Lazy.force f) (fun fc -> k (mkApp (EConstr.of_constr fc, args)))
 
 let new_refine c = Proofview.V82.tactic (refine c)
 let refine c = refine c
@@ -259,20 +262,24 @@ let refresh_type env evm ty =
 			      (Some false) env evm ty
 
 let refresh_universes ty k =
-  Proofview.Goal.enter { enter = begin fun gl ->
+  Proofview.Goal.s_enter { s_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 (EConstr.of_constr ty) in
-    Tacticals.New.tclTHEN (Proofview.V82.tactic (Refiner.tclEVARS evm)) (k ty)
+    let evm, ty = refresh_type env evm ty in
+    let ty = EConstr.of_constr ty in
+    Sigma.Unsafe.of_pair (k ty, evm)
   end }
 
+let constr_of_term c = EConstr.of_constr (constr_of_term c)
+
 let rec proof_tac p : unit Proofview.tactic =
   Proofview.Goal.nf_enter { enter = begin fun gl ->
-  let type_of t = Tacmach.New.pf_unsafe_type_of gl (EConstr.of_constr t) in
+  let type_of t = EConstr.of_constr (Tacmach.New.pf_unsafe_type_of gl t) in
   try (* type_of can raise exceptions *)
   match p.p_rule with
       Ax c -> exact_check (EConstr.of_constr c)
     | SymAx c ->
+        let c = EConstr.of_constr c in
 	let l=constr_of_term p.p_lhs and
 	    r=constr_of_term p.p_rhs in
 	refresh_universes (type_of l) (fun typ ->
@@ -321,7 +328,6 @@ let rec proof_tac p : unit Proofview.tactic =
 	 let special=mkRel (1+nargs-argind) in
 	 refresh_universes (type_of ti) (fun intype ->
          refresh_universes (type_of default) (fun outtype ->
-         let default = EConstr.of_constr default in
          let proj =
            Tacmach.New.of_old (build_projection intype cstr special default) gl
          in
@@ -336,12 +342,11 @@ let refute_tac c t1 t2 p =
   let tt1=constr_of_term t1 and tt2=constr_of_term t2 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 false_t = EConstr.of_constr false_t 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]
-  in refresh_universes (Tacmach.New.pf_unsafe_type_of gl (EConstr.of_constr tt1)) k
+  in refresh_universes (EConstr.of_constr (Tacmach.New.pf_unsafe_type_of gl tt1)) k
   end }
 
 let refine_exact_check c gl =
@@ -359,7 +364,7 @@ let convert_to_goal_tac c t1 t2 p =
     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)]
-  in refresh_universes (Tacmach.New.pf_unsafe_type_of gl (EConstr.of_constr tt2)) k
+  in refresh_universes (EConstr.of_constr (Tacmach.New.pf_unsafe_type_of gl tt2)) k
   end }
 
 let convert_to_hyp_tac c1 t1 c2 t2 p =
@@ -367,8 +372,6 @@ let convert_to_hyp_tac c1 t1 c2 t2 p =
   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
-  let false_t = EConstr.of_constr false_t in
-  let tt2 = EConstr.of_constr tt2 in
     Tacticals.New.tclTHENS (assert_before (Name h) tt2)
       [convert_to_goal_tac c1 t1 t2 p;
        simplest_elim false_t]
@@ -381,20 +384,21 @@ let discriminate_tac (cstr,u as cstru) p =
     let concl = Proofview.Goal.concl gl in
     let xid = Tacmach.New.of_old (pf_get_new_id (Id.of_string "X")) gl in
     let identity = Universes.constr_of_global (Lazy.force _I) in
+    let identity = EConstr.of_constr identity in
     let trivial = Universes.constr_of_global (Lazy.force _True) in
+    let trivial = EConstr.of_constr trivial in
     let evm = Tacmach.New.project gl in
-    let evm, intype = refresh_type env evm (EConstr.of_constr (Tacmach.New.pf_unsafe_type_of gl (EConstr.of_constr t1))) in
+    let evm, intype = refresh_type env evm (EConstr.of_constr (Tacmach.New.pf_unsafe_type_of gl t1)) in
+    let intype = EConstr.of_constr intype 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 hid = Tacmach.New.of_old (pf_get_new_id (Id.of_string "Heq")) gl in
     let proj = Tacmach.New.of_old (build_projection intype cstru trivial concl) gl in
-    let concl = EConstr.Unsafe.to_constr concl in
     let injt=app_global _f_equal
 			[|intype;outtype;proj;t1;t2;mkVar hid|] in
     let endt k =
       injt (fun injt ->
-            let injt = EConstr.Unsafe.to_constr injt in
             app_global _eq_rect
 		       [|outtype;trivial;pred;identity;concl;injt|] k) in
     let neweq=new_app_global _eq [|intype;t1;t2|] in
@@ -410,7 +414,7 @@ let build_term_to_complete uf meta pac =
   let real_args = List.map (fun i -> constr_of_term (term uf i)) pac.args in
   let dummy_args = List.rev (List.init pac.arity meta) in
   let all_args = List.rev_append real_args dummy_args in
-    applistc (mkConstructU cinfo.ci_constr) all_args
+    applist (mkConstructU cinfo.ci_constr, all_args)
 
 let cc_tactic depth additionnal_terms =
   Proofview.Goal.nf_enter { enter = begin fun gl ->
@@ -448,7 +452,7 @@ let cc_tactic depth additionnal_terms =
 		   str "\"congruence with (" ++
 		     prlist_with_sep
 		     (fun () -> str ")" ++ spc () ++ str "(")
-		     (Termops.print_constr_env env)
+		     (EConstr.Unsafe.to_constr %> Termops.print_constr_env env)
 		     terms_to_complete ++
 		     str ")\","
 		 end ++
@@ -459,10 +463,13 @@ let cc_tactic depth additionnal_terms =
 	    let ta=term uf dis.lhs and tb=term uf dis.rhs in
 	    match dis.rule with
 	      Goal -> proof_tac p
-	    | Hyp id -> refute_tac id ta tb p
+	    | Hyp id -> refute_tac (EConstr.of_constr id) ta tb p
 	    | HeqG id ->
+                let id = EConstr.of_constr id in
 		convert_to_goal_tac id ta tb p
 	    | HeqnH (ida,idb) ->
+                let ida = EConstr.of_constr ida in
+                let idb = EConstr.of_constr idb in
 		convert_to_hyp_tac ida ta idb tb p
   end }
 
@@ -487,20 +494,23 @@ let congruence_tac depth l =
 
 let mk_eq f c1 c2 k =
   Tacticals.New.pf_constr_of_global (Lazy.force f) (fun fc ->
+  let fc = EConstr.of_constr fc in
   Proofview.Goal.enter { enter = begin fun gl ->
     let open Tacmach.New in
-    let evm, ty = pf_apply type_of gl (EConstr.of_constr c1) in
-    let evm, ty = Evarsolve.refresh_universes (Some false) (pf_env gl) evm (EConstr.of_constr ty) in
+    let evm, ty = pf_apply type_of gl c1 in
+    let ty = EConstr.of_constr ty in
+    let evm, ty = Evarsolve.refresh_universes (Some false) (pf_env gl) evm ty in
+    let ty = EConstr.of_constr ty in
     let term = mkApp (fc, [| ty; c1; c2 |]) in
-    let evm, _ =  type_of (pf_env gl) evm (EConstr.of_constr term) in
+    let evm, _ =  type_of (pf_env gl) evm term in
     Tacticals.New.tclTHEN (Proofview.V82.tactic (Refiner.tclEVARS evm))
-			  (k (EConstr.of_constr term))
+			  (k term)
     end })
 
 let f_equal =
   Proofview.Goal.nf_enter { enter = begin fun gl ->
     let concl = Proofview.Goal.concl gl in
-    let concl = EConstr.Unsafe.to_constr concl in
+    let sigma = Tacmach.New.project gl in
     let cut_eq c1 c2 =
       try (* type_of can raise an exception *)
         Tacticals.New.tclTHENS
@@ -509,9 +519,9 @@ let f_equal =
       with e when Proofview.V82.catchable_exception e -> Proofview.tclZERO e
     in
     Proofview.tclORELSE
-      begin match kind_of_term concl with
-      | App (r,[|_;t;t'|]) when Globnames.is_global (Lazy.force _eq) r ->
-	  begin match kind_of_term t, kind_of_term t' with
+      begin match EConstr.kind sigma concl with
+      | App (r,[|_;t;t'|]) when is_global sigma (Lazy.force _eq) r ->
+	  begin match EConstr.kind sigma t, EConstr.kind sigma t' with
 	  | App (f,v), App (f',v') when Int.equal (Array.length v) (Array.length v') ->
 	      let rec cuts i =
 		if i < 0 then Tacticals.New.tclTRY (congruence_tac 1000 [])
diff --git a/plugins/cc/cctac.mli b/plugins/cc/cctac.mli
index 7c1d9f1c0..de6eb982e 100644
--- a/plugins/cc/cctac.mli
+++ b/plugins/cc/cctac.mli
@@ -7,7 +7,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-open Term
+open EConstr
 open Proof_type
 
 val proof_tac: Ccproof.proof -> unit Proofview.tactic
diff --git a/plugins/cc/g_congruence.ml4 b/plugins/cc/g_congruence.ml4
index 6f6811334..b787e824f 100644
--- a/plugins/cc/g_congruence.ml4
+++ b/plugins/cc/g_congruence.ml4
@@ -18,9 +18,9 @@ DECLARE PLUGIN "cc_plugin"
 TACTIC EXTEND cc
  [ "congruence" ] -> [ congruence_tac 1000 [] ]
  |[ "congruence" integer(n) ] -> [ congruence_tac n [] ]
- |[ "congruence" "with" ne_constr_list(l) ] -> [ congruence_tac 1000 l ]
+ |[ "congruence" "with" ne_constr_list(l) ] -> [ congruence_tac 1000 (List.map EConstr.of_constr l) ]
  |[ "congruence" integer(n) "with" ne_constr_list(l) ] ->
-   [ congruence_tac n l ]
+   [ congruence_tac n (List.map EConstr.of_constr l) ]
 END
 
 TACTIC EXTEND f_equal
diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml
index 45e7abcb7..c796a91ca 100644
--- a/pretyping/reductionops.ml
+++ b/pretyping/reductionops.ml
@@ -1221,6 +1221,14 @@ let clos_norm_flags flgs env sigma t =
       (CClosure.inject (EConstr.Unsafe.to_constr t)))
   with e when is_anomaly e -> error "Tried to normalize ill-typed term"
 
+let clos_whd_flags flgs env sigma t =
+  try
+    let evars ev = safe_evar_value sigma ev in
+    EConstr.of_constr (CClosure.whd_val
+      (CClosure.create_clos_infos ~evars flgs env)
+      (CClosure.inject (EConstr.Unsafe.to_constr t)))
+  with e when is_anomaly e -> error "Tried to normalize ill-typed term"
+
 let nf_beta = clos_norm_flags CClosure.beta (Global.env ())
 let nf_betaiota = clos_norm_flags CClosure.betaiota (Global.env ())
 let nf_betaiotazeta = clos_norm_flags CClosure.betaiotazeta (Global.env ())
diff --git a/pretyping/reductionops.mli b/pretyping/reductionops.mli
index add1d186b..8aaeeb2c2 100644
--- a/pretyping/reductionops.mli
+++ b/pretyping/reductionops.mli
@@ -149,6 +149,7 @@ val iterate_whd_gen : bool -> CClosure.RedFlags.reds ->
 (** {6 Generic Optimized Reduction Function using Closures } *)
 
 val clos_norm_flags : CClosure.RedFlags.reds -> reduction_function
+val clos_whd_flags : CClosure.RedFlags.reds -> reduction_function
 
 (** Same as [(strong whd_beta[delta][iota])], but much faster on big terms *)
 val nf_beta : local_reduction_function