From b365304d32db443194b7eaadda63c784814f53f1 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Sun, 6 Nov 2016 03:23:13 +0100 Subject: Evarconv API using EConstr. --- engine/evarutil.ml | 37 +++++++++---------------------------- engine/evarutil.mli | 6 +++--- engine/termops.ml | 11 +++++++++++ engine/termops.mli | 1 + engine/universes.ml | 9 --------- engine/universes.mli | 2 -- 6 files changed, 24 insertions(+), 42 deletions(-) (limited to 'engine') 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 -> -- cgit v1.2.3