Reductionops API using EConstr.

5 files changed, 35 insertions, 28 deletions

diff --git a/proofs/clenv.ml b/proofs/clenv.ml
index 34bc83097..d64cd9fff 100644
--- a/proofs/clenv.ml
+++ b/proofs/clenv.ml
@@ -72,7 +72,7 @@ let clenv_get_type_of ce c = Retyping.get_type_of (cl_env ce) (cl_sigma ce) c
 exception NotExtensibleClause
 
 let clenv_push_prod cl =
-  let typ = whd_all (cl_env cl) (cl_sigma cl) (clenv_type cl) in
+  let typ = whd_all (cl_env cl) (cl_sigma cl) (EConstr.of_constr (clenv_type cl)) in
   let rec clrec typ = match kind_of_term typ with
     | Cast (t,_,_) -> clrec t
     | Prod (na,t,u) ->
@@ -264,7 +264,7 @@ let clenv_unify_meta_types ?(flags=default_unify_flags ()) clenv =
 
 let clenv_unique_resolver ?(flags=default_unify_flags ()) clenv gl =
   let concl = Goal.V82.concl clenv.evd (sig_it gl) in
-  if isMeta (fst (decompose_appvect (whd_nored clenv.evd clenv.templtyp.rebus))) then
+  if isMeta (fst (decompose_appvect (whd_nored clenv.evd (EConstr.of_constr clenv.templtyp.rebus)))) then
     clenv_unify CUMUL ~flags (clenv_type clenv) concl
       (clenv_unify_meta_types ~flags clenv)
   else
@@ -482,7 +482,7 @@ let error_already_defined b =
           (str "Position " ++ int n ++ str" already defined.")
 
 let clenv_unify_binding_type clenv c t u =
-  if isMeta (fst (decompose_appvect (whd_nored clenv.evd u))) then
+  if isMeta (fst (decompose_appvect (whd_nored clenv.evd (EConstr.of_constr u)))) then
     (* Not enough information to know if some subtyping is needed *)
     CoerceToType, clenv, c
   else
@@ -498,8 +498,8 @@ let clenv_unify_binding_type clenv c t u =
 	  TypeNotProcessed, clenv, c
 
 let clenv_assign_binding clenv k c =
-  let k_typ = clenv_hnf_constr clenv (clenv_meta_type clenv k) in
-  let c_typ = nf_betaiota clenv.evd (clenv_get_type_of clenv c) in
+  let k_typ = clenv_hnf_constr clenv (EConstr.of_constr (clenv_meta_type clenv k)) in
+  let c_typ = nf_betaiota clenv.evd (EConstr.of_constr (clenv_get_type_of clenv c)) in
   let status,clenv',c = clenv_unify_binding_type clenv c c_typ k_typ in
   { clenv' with evd = meta_assign k (c,(Conv,status)) clenv'.evd }
 
diff --git a/proofs/logic.ml b/proofs/logic.ml
index 29f295682..0fa193065 100644
--- a/proofs/logic.ml
+++ b/proofs/logic.ml
@@ -345,7 +345,7 @@ let rec mk_refgoals sigma goal goalacc conclty trm =
     else
       match kind_of_term trm with
       | Meta _ ->
-	let conclty = nf_betaiota sigma conclty in
+	let conclty = nf_betaiota sigma (EConstr.of_constr conclty) in
 	  if !check && occur_meta sigma (EConstr.of_constr conclty) then
 	    raise (RefinerError (MetaInType conclty));
 	  let (gl,ev,sigma) = mk_goal hyps conclty in
@@ -423,7 +423,7 @@ and mk_hdgoals sigma goal goalacc trm =
   match kind_of_term trm with
     | Cast (c,_, ty) when isMeta c ->
 	check_typability env sigma ty;
-	let (gl,ev,sigma) = mk_goal hyps (nf_betaiota sigma ty) in
+	let (gl,ev,sigma) = mk_goal hyps (nf_betaiota sigma (EConstr.of_constr ty)) in
 	gl::goalacc,ty,sigma,ev
 
     | Cast (t,_, ty) ->
@@ -470,7 +470,7 @@ and mk_hdgoals sigma goal goalacc trm =
 
 and mk_arggoals sigma goal goalacc funty allargs =
   let foldmap (goalacc, funty, sigma) harg =
-    let t = whd_all (Goal.V82.env sigma goal) sigma funty in
+    let t = whd_all (Goal.V82.env sigma goal) sigma (EConstr.of_constr funty) in
     let rec collapse t = match kind_of_term t with
     | LetIn (_, c1, _, b) -> collapse (subst1 c1 b)
     | _ -> t
@@ -491,21 +491,21 @@ and mk_casegoals sigma goal goalacc p c =
   let indspec =
     try Tacred.find_hnf_rectype env sigma ct
     with Not_found -> anomaly (Pp.str "mk_casegoals") in
-  let (lbrty,conclty) = type_case_branches_with_names env indspec p c in
+  let (lbrty,conclty) = type_case_branches_with_names env sigma indspec p c in
   (acc'',lbrty,conclty,sigma,p',c')
 
 
 let convert_hyp check sign sigma d =
   let id = NamedDecl.get_id d in
-  let b = NamedDecl.get_value d in
+  let b = Option.map EConstr.of_constr (NamedDecl.get_value d) in
   let env = Global.env() in
   let reorder = ref [] in
   let sign' =
     apply_to_hyp check sign id
       (fun _ d' _ ->
-        let c = NamedDecl.get_value d' in
+        let c = Option.map EConstr.of_constr (NamedDecl.get_value d') in
         let env = Global.env_of_context sign in
-        if check && not (is_conv env sigma (NamedDecl.get_type d) (NamedDecl.get_type d')) then
+        if check && not (is_conv env sigma (EConstr.of_constr (NamedDecl.get_type d)) (EConstr.of_constr (NamedDecl.get_type d'))) then
 	  user_err ~hdr:"Logic.convert_hyp"
             (str "Incorrect change of the type of " ++ pr_id id ++ str ".");
         if check && not (Option.equal (is_conv env sigma) b c) then
@@ -532,7 +532,7 @@ let prim_refiner r sigma goal =
     (* Logical rules *)
     | Cut (b,replace,id,t) ->
 (*        if !check && not (Retyping.get_sort_of env sigma t) then*)
-        let (sg1,ev1,sigma) = mk_goal sign (nf_betaiota sigma t) in
+        let (sg1,ev1,sigma) = mk_goal sign (nf_betaiota sigma (EConstr.of_constr t)) in
 	let sign,t,cl,sigma =
 	  if replace then
 	    let nexthyp = get_hyp_after id (named_context_of_val sign) in
diff --git a/proofs/redexpr.ml b/proofs/redexpr.ml
index a442a5e63..40a8077a7 100644
--- a/proofs/redexpr.ml
+++ b/proofs/redexpr.ml
@@ -24,10 +24,11 @@ open Misctypes
 
 (* call by value normalisation function using the virtual machine *)
 let cbv_vm env sigma c =
+  let c = EConstr.Unsafe.to_constr c in
   let ctyp = Retyping.get_type_of env sigma c in
   if Termops.occur_meta_or_existential sigma (EConstr.of_constr c) then
     error "vm_compute does not support existential variables.";
-  Vnorm.cbv_vm env c ctyp
+  Vnorm.cbv_vm env sigma c ctyp
 
 let warn_native_compute_disabled =
   CWarnings.create ~name:"native-compute-disabled" ~category:"native-compiler"
@@ -39,13 +40,15 @@ let cbv_native env sigma c =
     (warn_native_compute_disabled ();
      cbv_vm env sigma c)
   else
+    let c = EConstr.Unsafe.to_constr c in
     let ctyp = Retyping.get_type_of env sigma c in
     Nativenorm.native_norm env sigma c ctyp
 
 let whd_cbn flags env sigma t =
   let (state,_) =
     (whd_state_gen true true flags env sigma (t,Reductionops.Stack.empty))
-  in Reductionops.Stack.zip ~refold:true state
+  in
+  EConstr.Unsafe.to_constr (Reductionops.Stack.zip ~refold:true sigma state)
 
 let strong_cbn flags =
   strong (whd_cbn flags)
diff --git a/proofs/tacmach.ml b/proofs/tacmach.ml
index e41fb94cc..09f5246ab 100644
--- a/proofs/tacmach.ml
+++ b/proofs/tacmach.ml
@@ -77,26 +77,27 @@ let pf_global gls id = Constrintern.construct_reference (pf_hyps gls) id
 let pf_reduction_of_red_expr gls re c =
   let (redfun, _) = reduction_of_red_expr (pf_env gls) re in
   let sigma = Sigma.Unsafe.of_evar_map (project gls) in
-  let Sigma (c, sigma, _) = redfun.e_redfun (pf_env gls) sigma c in
+  let Sigma (c, sigma, _) = redfun.e_redfun (pf_env gls) sigma (EConstr.of_constr c) in
   (Sigma.to_evar_map sigma, c)
 
 let pf_apply f gls = f (pf_env gls) (project gls)
 let pf_eapply f gls x = 
   on_sig gls (fun evm -> f (pf_env gls) evm x)
 let pf_reduce = pf_apply
+let pf_reduce' f gl c = pf_apply f gl (EConstr.of_constr c)
 let pf_e_reduce = pf_apply
 
-let pf_whd_all         = pf_reduce whd_all
-let pf_hnf_constr                = pf_reduce hnf_constr
-let pf_nf                        = pf_reduce simpl
-let pf_nf_betaiota               = pf_reduce (fun _ -> nf_betaiota)
-let pf_compute                   = pf_reduce compute
-let pf_unfoldn ubinds            = pf_reduce (unfoldn ubinds)
+let pf_whd_all         = pf_reduce' whd_all
+let pf_hnf_constr                = pf_reduce' hnf_constr
+let pf_nf                        = pf_reduce' simpl
+let pf_nf_betaiota               = pf_reduce' (fun _ -> nf_betaiota)
+let pf_compute                   = pf_reduce' compute
+let pf_unfoldn ubinds            = pf_reduce' (unfoldn ubinds)
 let pf_unsafe_type_of            = pf_reduce unsafe_type_of
 let pf_type_of                   = pf_reduce type_of
 let pf_get_type_of               = pf_reduce Retyping.get_type_of
 
-let pf_conv_x gl                = pf_reduce test_conversion gl Reduction.CONV
+let pf_conv_x gl                = pf_apply test_conversion gl Reduction.CONV
 let pf_conv_x_leq gl            = pf_reduce test_conversion gl Reduction.CUMUL
 let pf_const_value              = pf_reduce (fun env _ -> constant_value_in env)
 
@@ -158,6 +159,9 @@ module New = struct
   let pf_apply f gl =
     f (Proofview.Goal.env gl) (project gl)
 
+  let pf_reduce f gl c =
+    f (Proofview.Goal.env gl) (project gl) (EConstr.of_constr c)
+
   let of_old f gl =
     f { Evd.it = Proofview.Goal.goal gl ; sigma = project gl; }
 
@@ -217,14 +221,14 @@ module New = struct
     let sigma = project gl in
     nf_evar sigma concl
 
-  let pf_whd_all gl t = pf_apply whd_all gl t
+  let pf_whd_all gl t = pf_reduce whd_all gl t
 
   let pf_get_type_of gl t = pf_apply Retyping.get_type_of gl t
 
   let pf_reduce_to_quantified_ind gl t =
     pf_apply reduce_to_quantified_ind gl t
 
-  let pf_hnf_constr gl t = pf_apply hnf_constr gl t
+  let pf_hnf_constr gl t = pf_reduce hnf_constr gl t
   let pf_hnf_type_of gl t =
     pf_whd_all gl (pf_get_type_of gl t)
 
diff --git a/proofs/tacmach.mli b/proofs/tacmach.mli
index 727efcf6d..16f6f88c1 100644
--- a/proofs/tacmach.mli
+++ b/proofs/tacmach.mli
@@ -110,7 +110,7 @@ module New : sig
 
   val pf_unsafe_type_of : ('a, 'r) Proofview.Goal.t -> Term.constr -> Term.types
   val pf_type_of : ('a, 'r) Proofview.Goal.t -> Term.constr -> evar_map * Term.types
-  val pf_conv_x : ('a, 'r) Proofview.Goal.t -> Term.constr -> Term.constr -> bool
+  val pf_conv_x : ('a, 'r) Proofview.Goal.t -> EConstr.t -> EConstr.t -> bool
 
   val pf_get_new_id  : identifier -> ([ `NF ], 'r) Proofview.Goal.t -> identifier
   val pf_ids_of_hyps : ('a, 'r) Proofview.Goal.t -> identifier list
@@ -126,8 +126,8 @@ module New : sig
   val pf_hnf_constr : ('a, 'r) Proofview.Goal.t -> constr -> types
   val pf_hnf_type_of : ('a, 'r) Proofview.Goal.t -> constr -> types
 
-  val pf_whd_all : ('a, 'r) Proofview.Goal.t -> constr -> constr
-  val pf_compute : ('a, 'r) Proofview.Goal.t -> constr -> constr
+  val pf_whd_all : ('a, 'r) Proofview.Goal.t -> EConstr.t -> constr
+  val pf_compute : ('a, 'r) Proofview.Goal.t -> EConstr.t -> constr
 
   val pf_matches : ('a, 'r) Proofview.Goal.t -> constr_pattern -> constr -> patvar_map