Evarconv API using EConstr.

6 files changed, 24 insertions, 42 deletions

diff --git a/engine/evarutil.ml b/engine/evarutil.ml
index 05f98a41f..62627a416 100644
--- a/engine/evarutil.ml
+++ b/engine/evarutil.ml
@@ -148,21 +148,11 @@ let nf_evar_map_undefined evm =
 (* Auxiliary functions for the conversion algorithms modulo evars
  *)
 
-(* A probably faster though more approximative variant of
-   [has_undefined (nf_evar c)]: instances are not substituted and
-   maybe an evar occurs in an instance and it would disappear by
-   instantiation *)
-
 let has_undefined_evars evd t =
   let rec has_ev t =
-    match kind_of_term t with
-    | Evar (ev,args) ->
-        (match evar_body (Evd.find evd ev) with
-        | Evar_defined c ->
-            has_ev c; Array.iter has_ev args
-        | Evar_empty ->
-	    raise NotInstantiatedEvar)
-    | _ -> iter_constr has_ev t in
+    match EConstr.kind evd t with
+    | Evar _ -> raise NotInstantiatedEvar
+    | _ -> EConstr.iter evd has_ev t in
   try let _ = has_ev t in false
   with (Not_found | NotInstantiatedEvar) -> true
 
@@ -171,10 +161,10 @@ let is_ground_term evd t =
 
 let is_ground_env evd env =
   let is_ground_rel_decl = function
-    | RelDecl.LocalDef (_,b,_) -> is_ground_term evd b
+    | RelDecl.LocalDef (_,b,_) -> is_ground_term evd (EConstr.of_constr b)
     | _ -> true in
   let is_ground_named_decl = function
-    | NamedDecl.LocalDef (_,b,_) -> is_ground_term evd b
+    | NamedDecl.LocalDef (_,b,_) -> is_ground_term evd (EConstr.of_constr b)
     | _ -> true in
   List.for_all is_ground_rel_decl (rel_context env) &&
   List.for_all is_ground_named_decl (named_context env)
@@ -208,27 +198,18 @@ let head_evar =
    guess it should consider Case too) *)
 
 let whd_head_evar_stack sigma c =
-  let rec whrec (c, l as s) =
-    match kind_of_term c with
-      | Evar (evk,args as ev) ->
-        let v =
-          try Some (existential_value sigma ev)
-          with NotInstantiatedEvar | Not_found  -> None in
-        begin match v with
-        | None -> s
-        | Some c -> whrec (c, l)
-        end
+  let rec whrec (c, l) =
+    match EConstr.kind sigma c with
       | Cast (c,_,_) -> whrec (c, l)
       | App (f,args) -> whrec (f, args :: l)
-      | _ -> s
+      | c -> (EConstr.of_kind c, l)
   in
   whrec (c, [])
 
 let whd_head_evar sigma c =
+  let open EConstr in
   let (f, args) = whd_head_evar_stack sigma c in
-  (** optim: don't reallocate if empty/singleton *)
   match args with
-  | [] -> f
   | [arg] -> mkApp (f, arg)
   | _ -> mkApp (f, Array.concat args)
 
diff --git a/engine/evarutil.mli b/engine/evarutil.mli
index a2e2a07dd..d6e2d4534 100644
--- a/engine/evarutil.mli
+++ b/engine/evarutil.mli
@@ -91,12 +91,12 @@ exception NoHeadEvar
 val head_evar : constr -> existential_key (** may raise NoHeadEvar *)
 
 (* Expand head evar if any *)
-val whd_head_evar :  evar_map -> constr -> constr
+val whd_head_evar :  evar_map -> EConstr.constr -> EConstr.constr
 
 (* An over-approximation of [has_undefined (nf_evars evd c)] *)
-val has_undefined_evars : evar_map -> constr -> bool
+val has_undefined_evars : evar_map -> EConstr.constr -> bool
 
-val is_ground_term :  evar_map -> constr -> bool
+val is_ground_term :  evar_map -> EConstr.constr -> bool
 val is_ground_env  :  evar_map -> env -> bool
 
 (** [gather_dependent_evars evm seeds] classifies the evars in [evm]
diff --git a/engine/termops.ml b/engine/termops.ml
index 356312e2f..26b22be4e 100644
--- a/engine/termops.ml
+++ b/engine/termops.ml
@@ -1068,6 +1068,17 @@ let dependency_closure env sigma sign hyps =
         sign in
     List.rev lh
 
+let global_app_of_constr sigma c =
+  let open Univ in
+  let open Globnames in
+  match EConstr.kind sigma c with
+  | Const (c, u) -> (ConstRef c, u), None
+  | Ind (i, u) -> (IndRef i, u), None
+  | Construct (c, u) -> (ConstructRef c, u), None
+  | Var id -> (VarRef id, Instance.empty), None
+  | Proj (p, c) -> (ConstRef (Projection.constant p), Instance.empty), Some c
+  | _ -> raise Not_found
+
 (* Combinators on judgments *)
 
 let on_judgment f j = { uj_val = f j.uj_val; uj_type = f j.uj_type }
diff --git a/engine/termops.mli b/engine/termops.mli
index b536b0fb8..24c2c82f2 100644
--- a/engine/termops.mli
+++ b/engine/termops.mli
@@ -254,6 +254,7 @@ val clear_named_body : Id.t -> env -> env
 
 val global_vars : env -> Evd.evar_map -> EConstr.t -> Id.t list
 val global_vars_set_of_decl : env -> Evd.evar_map -> Context.Named.Declaration.t -> Id.Set.t
+val global_app_of_constr : Evd.evar_map -> EConstr.constr -> Globnames.global_reference puniverses * EConstr.constr option
 
 (** Gives an ordered list of hypotheses, closed by dependencies,
    containing a given set *)
diff --git a/engine/universes.ml b/engine/universes.ml
index 6720fcef8..51a113219 100644
--- a/engine/universes.ml
+++ b/engine/universes.ml
@@ -446,15 +446,6 @@ let global_of_constr c =
   | Var id -> VarRef id, Instance.empty
   | _ -> raise Not_found
 
-let global_app_of_constr c =
-  match kind_of_term c with
-  | Const (c, u) -> (ConstRef c, u), None
-  | Ind (i, u) -> (IndRef i, u), None
-  | Construct (c, u) -> (ConstructRef c, u), None
-  | Var id -> (VarRef id, Instance.empty), None
-  | Proj (p, c) -> (ConstRef (Projection.constant p), Instance.empty), Some c
-  | _ -> raise Not_found
-
 open Declarations
 
 let type_of_reference env r =
diff --git a/engine/universes.mli b/engine/universes.mli
index 725c21d29..c3e2055f3 100644
--- a/engine/universes.mli
+++ b/engine/universes.mli
@@ -130,8 +130,6 @@ val fresh_universe_context_set_instance : universe_context_set ->
 (** Raises [Not_found] if not a global reference. *)
 val global_of_constr : constr -> Globnames.global_reference puniverses
 
-val global_app_of_constr : constr -> Globnames.global_reference puniverses * constr option
-
 val constr_of_global_univ : Globnames.global_reference puniverses -> constr
 
 val extend_context : 'a in_universe_context_set -> universe_context_set ->