aboutsummaryrefslogtreecommitdiffhomepage
path: root/pretyping
diff options
context:
space:
mode:
Diffstat (limited to 'pretyping')
-rw-r--r--pretyping/cases.ml1
-rw-r--r--pretyping/coercion.ml6
-rw-r--r--pretyping/evarconv.ml1
-rw-r--r--pretyping/evardefine.ml209
-rw-r--r--pretyping/evardefine.mli46
-rw-r--r--pretyping/evarutil.ml899
-rw-r--r--pretyping/evarutil.mli253
-rw-r--r--pretyping/pretyping.ml18
-rw-r--r--pretyping/pretyping.mli4
-rw-r--r--pretyping/pretyping.mllib4
-rw-r--r--pretyping/reductionops.ml30
-rw-r--r--pretyping/typeclasses.ml2
-rw-r--r--pretyping/typing.ml4
-rw-r--r--pretyping/unification.ml1
14 files changed, 291 insertions, 1187 deletions
diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index 8a55a7aaa..c3968f896 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -25,6 +25,7 @@ open Glob_ops
open Retyping
open Pretype_errors
open Evarutil
+open Evardefine
open Evarsolve
open Evarconv
open Evd
diff --git a/pretyping/coercion.ml b/pretyping/coercion.ml
index 57b273d0d..9d0f391e4 100644
--- a/pretyping/coercion.ml
+++ b/pretyping/coercion.ml
@@ -245,7 +245,7 @@ and coerce loc env evdref (x : Term.constr) (y : Term.constr)
| Lambda (n, t, t') -> c, t'
(*| Prod (n, t, t') -> t'*)
| Evar (k, args) ->
- let (evs, t) = Evarutil.define_evar_as_lambda env !evdref (k,args) in
+ let (evs, t) = Evardefine.define_evar_as_lambda env !evdref (k,args) in
evdref := evs;
let (n, dom, rng) = destLambda t in
let dom = whd_evar !evdref dom in
@@ -375,7 +375,7 @@ let inh_app_fun_core env evd j =
match kind_of_term t with
| Prod (_,_,_) -> (evd,j)
| Evar ev ->
- let (evd',t) = define_evar_as_product evd ev in
+ let (evd',t) = Evardefine.define_evar_as_product evd ev in
(evd',{ uj_val = j.uj_val; uj_type = t })
| _ ->
try let t,p =
@@ -416,7 +416,7 @@ let inh_coerce_to_sort loc env evd j =
match kind_of_term typ with
| Sort s -> (evd,{ utj_val = j.uj_val; utj_type = s })
| Evar ev when not (is_defined evd (fst ev)) ->
- let (evd',s) = define_evar_as_sort env evd ev in
+ let (evd',s) = Evardefine.define_evar_as_sort env evd ev in
(evd',{ utj_val = j.uj_val; utj_type = s })
| _ ->
inh_tosort_force loc env evd j
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index 489a8a729..08973a05c 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -18,6 +18,7 @@ open Termops
open Environ
open Recordops
open Evarutil
+open Evardefine
open Evarsolve
open Globnames
open Evd
diff --git a/pretyping/evardefine.ml b/pretyping/evardefine.ml
new file mode 100644
index 000000000..ef3a3f525
--- /dev/null
+++ b/pretyping/evardefine.ml
@@ -0,0 +1,209 @@
+(************************************************************************)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
+(* \VV/ **************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(************************************************************************)
+
+open Errors
+open Util
+open Pp
+open Names
+open Term
+open Vars
+open Termops
+open Namegen
+open Pre_env
+open Environ
+open Evd
+open Evarutil
+open Pretype_errors
+open Sigma.Notations
+
+let new_evar_unsafe env evd ?src ?filter ?candidates ?store ?naming ?principal typ =
+ let evd = Sigma.Unsafe.of_evar_map evd in
+ let Sigma (evk, evd, _) = new_evar env evd ?src ?filter ?candidates ?store ?naming ?principal typ in
+ (Sigma.to_evar_map evd, evk)
+
+let env_nf_evar sigma env =
+ let open Context.Rel.Declaration in
+ process_rel_context
+ (fun d e -> push_rel (map_constr (nf_evar sigma) d) e) env
+
+let env_nf_betaiotaevar sigma env =
+ let open Context.Rel.Declaration in
+ process_rel_context
+ (fun d e ->
+ push_rel (map_constr (Reductionops.nf_betaiota sigma) d) e) env
+
+(****************************************)
+(* Operations on value/type constraints *)
+(****************************************)
+
+type type_constraint = types option
+
+type val_constraint = constr option
+
+(* Old comment...
+ * Basically, we have the following kind of constraints (in increasing
+ * strength order):
+ * (false,(None,None)) -> no constraint at all
+ * (true,(None,None)) -> we must build a judgement which _TYPE is a kind
+ * (_,(None,Some ty)) -> we must build a judgement which _TYPE is ty
+ * (_,(Some v,_)) -> we must build a judgement which _VAL is v
+ * Maybe a concrete datatype would be easier to understand.
+ * We differentiate (true,(None,None)) from (_,(None,Some Type))
+ * because otherwise Case(s) would be misled, as in
+ * (n:nat) Case n of bool [_]nat end would infer the predicate Type instead
+ * of Set.
+ *)
+
+(* The empty type constraint *)
+let empty_tycon = None
+
+(* Builds a type constraint *)
+let mk_tycon ty = Some ty
+
+(* Constrains the value of a type *)
+let empty_valcon = None
+
+(* Builds a value constraint *)
+let mk_valcon c = Some c
+
+let idx = Namegen.default_dependent_ident
+
+(* Refining an evar to a product *)
+
+let define_pure_evar_as_product evd evk =
+ let open Context.Named.Declaration in
+ let evi = Evd.find_undefined evd evk in
+ let evenv = evar_env evi in
+ let id = next_ident_away idx (ids_of_named_context (evar_context evi)) in
+ let concl = Reductionops.whd_betadeltaiota evenv evd evi.evar_concl in
+ let s = destSort concl in
+ let evd1,(dom,u1) =
+ let evd = Sigma.Unsafe.of_evar_map evd in
+ let Sigma (e, evd1, _) = new_type_evar evenv evd univ_flexible_alg ~filter:(evar_filter evi) in
+ (Sigma.to_evar_map evd1, e)
+ in
+ let evd2,rng =
+ let newenv = push_named (LocalAssum (id, dom)) evenv in
+ let src = evar_source evk evd1 in
+ let filter = Filter.extend 1 (evar_filter evi) in
+ if is_prop_sort s then
+ (* Impredicative product, conclusion must fall in [Prop]. *)
+ new_evar_unsafe newenv evd1 concl ~src ~filter
+ else
+ let status = univ_flexible_alg in
+ let evd3, (rng, srng) =
+ let evd1 = Sigma.Unsafe.of_evar_map evd1 in
+ let Sigma (e, evd3, _) = new_type_evar newenv evd1 status ~src ~filter in
+ (Sigma.to_evar_map evd3, e)
+ in
+ let prods = Univ.sup (univ_of_sort u1) (univ_of_sort srng) in
+ let evd3 = Evd.set_leq_sort evenv evd3 (Type prods) s in
+ evd3, rng
+ in
+ let prod = mkProd (Name id, dom, subst_var id rng) in
+ let evd3 = Evd.define evk prod evd2 in
+ evd3,prod
+
+(* Refine an applied evar to a product and returns its instantiation *)
+
+let define_evar_as_product evd (evk,args) =
+ let evd,prod = define_pure_evar_as_product evd evk in
+ (* Quick way to compute the instantiation of evk with args *)
+ let na,dom,rng = destProd prod in
+ let evdom = mkEvar (fst (destEvar dom), args) in
+ let evrngargs = Array.cons (mkRel 1) (Array.map (lift 1) args) in
+ let evrng = mkEvar (fst (destEvar rng), evrngargs) in
+ evd,mkProd (na, evdom, evrng)
+
+(* Refine an evar with an abstraction
+
+ I.e., solve x1..xq |- ?e:T(x1..xq) with e:=λy:A.?e'[x1..xq,y] where:
+ - either T(x1..xq) = πy:A(x1..xq).B(x1..xq,y)
+ or T(x1..xq) = ?d[x1..xq] and we define ?d := πy:?A.?B
+ with x1..xq |- ?A:Type and x1..xq,y |- ?B:Type
+ - x1..xq,y:A |- ?e':B
+*)
+
+let define_pure_evar_as_lambda env evd evk =
+ let open Context.Named.Declaration in
+ let evi = Evd.find_undefined evd evk in
+ let evenv = evar_env evi in
+ let typ = Reductionops.whd_betadeltaiota evenv evd (evar_concl evi) in
+ let evd1,(na,dom,rng) = match kind_of_term typ with
+ | Prod (na,dom,rng) -> (evd,(na,dom,rng))
+ | Evar ev' -> let evd,typ = define_evar_as_product evd ev' in evd,destProd typ
+ | _ -> error_not_product_loc Loc.ghost env evd typ in
+ let avoid = ids_of_named_context (evar_context evi) in
+ let id =
+ next_name_away_with_default_using_types "x" na avoid (Reductionops.whd_evar evd dom) in
+ let newenv = push_named (LocalAssum (id, dom)) evenv in
+ let filter = Filter.extend 1 (evar_filter evi) in
+ let src = evar_source evk evd1 in
+ let evd2,body = new_evar_unsafe newenv evd1 ~src (subst1 (mkVar id) rng) ~filter in
+ let lam = mkLambda (Name id, dom, subst_var id body) in
+ Evd.define evk lam evd2, lam
+
+let define_evar_as_lambda env evd (evk,args) =
+ let evd,lam = define_pure_evar_as_lambda env evd evk in
+ (* Quick way to compute the instantiation of evk with args *)
+ let na,dom,body = destLambda lam in
+ let evbodyargs = Array.cons (mkRel 1) (Array.map (lift 1) args) in
+ let evbody = mkEvar (fst (destEvar body), evbodyargs) in
+ evd,mkLambda (na, dom, evbody)
+
+let rec evar_absorb_arguments env evd (evk,args as ev) = function
+ | [] -> evd,ev
+ | a::l ->
+ (* TODO: optimize and avoid introducing intermediate evars *)
+ let evd,lam = define_pure_evar_as_lambda env evd evk in
+ let _,_,body = destLambda lam in
+ let evk = fst (destEvar body) in
+ evar_absorb_arguments env evd (evk, Array.cons a args) l
+
+(* Refining an evar to a sort *)
+
+let define_evar_as_sort env evd (ev,args) =
+ let evd, u = new_univ_variable univ_rigid evd in
+ let evi = Evd.find_undefined evd ev in
+ let s = Type u in
+ let concl = Reductionops.whd_betadeltaiota (evar_env evi) evd evi.evar_concl in
+ let sort = destSort concl in
+ let evd' = Evd.define ev (mkSort s) evd in
+ Evd.set_leq_sort env evd' (Type (Univ.super u)) sort, s
+
+(* Propagation of constraints through application and abstraction:
+ Given a type constraint on a functional term, returns the type
+ constraint on its domain and codomain. If the input constraint is
+ an evar instantiate it with the product of 2 new evars. *)
+
+let split_tycon loc env evd tycon =
+ let rec real_split evd c =
+ let t = Reductionops.whd_betadeltaiota env evd c in
+ match kind_of_term t with
+ | Prod (na,dom,rng) -> evd, (na, dom, rng)
+ | Evar ev (* ev is undefined because of whd_betadeltaiota *) ->
+ let (evd',prod) = define_evar_as_product evd ev in
+ let (_,dom,rng) = destProd prod in
+ evd',(Anonymous, dom, rng)
+ | App (c,args) when isEvar c ->
+ let (evd',lam) = define_evar_as_lambda env evd (destEvar c) in
+ real_split evd' (mkApp (lam,args))
+ | _ -> error_not_product_loc loc env evd c
+ in
+ match tycon with
+ | None -> evd,(Anonymous,None,None)
+ | Some c ->
+ let evd', (n, dom, rng) = real_split evd c in
+ evd', (n, mk_tycon dom, mk_tycon rng)
+
+let valcon_of_tycon x = x
+let lift_tycon n = Option.map (lift n)
+
+let pr_tycon env = function
+ None -> str "None"
+ | Some t -> Termops.print_constr_env env t
diff --git a/pretyping/evardefine.mli b/pretyping/evardefine.mli
new file mode 100644
index 000000000..07b0e69d9
--- /dev/null
+++ b/pretyping/evardefine.mli
@@ -0,0 +1,46 @@
+(************************************************************************)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
+(* \VV/ **************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(************************************************************************)
+
+open Names
+open Term
+open Evd
+open Environ
+
+val env_nf_evar : evar_map -> env -> env
+val env_nf_betaiotaevar : evar_map -> env -> env
+
+type type_constraint = types option
+type val_constraint = constr option
+
+val empty_tycon : type_constraint
+val mk_tycon : constr -> type_constraint
+val empty_valcon : val_constraint
+val mk_valcon : constr -> val_constraint
+
+(** Instantiate an evar by as many lambda's as needed so that its arguments
+ are moved to the evar substitution (i.e. turn [?x[vars1:=args1] args] into
+ [?y[vars1:=args1,vars:=args]] with
+ [vars1 |- ?x:=\vars.?y[vars1:=vars1,vars:=vars]] *)
+val evar_absorb_arguments : env -> evar_map -> existential -> constr list ->
+ evar_map * existential
+
+val split_tycon :
+ Loc.t -> env -> evar_map -> type_constraint ->
+ evar_map * (Name.t * type_constraint * type_constraint)
+
+val valcon_of_tycon : type_constraint -> val_constraint
+val lift_tycon : int -> type_constraint -> type_constraint
+
+val define_evar_as_product : evar_map -> existential -> evar_map * types
+val define_evar_as_lambda : env -> evar_map -> existential -> evar_map * types
+val define_evar_as_sort : env -> evar_map -> existential -> evar_map * sorts
+
+(** {6 debug pretty-printer:} *)
+
+val pr_tycon : env -> type_constraint -> Pp.std_ppcmds
+
diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml
deleted file mode 100644
index ab70de057..000000000
--- a/pretyping/evarutil.ml
+++ /dev/null
@@ -1,899 +0,0 @@
-(************************************************************************)
-(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
-(* \VV/ **************************************************************)
-(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
-(************************************************************************)
-
-open Errors
-open Util
-open Pp
-open Names
-open Term
-open Vars
-open Termops
-open Namegen
-open Pre_env
-open Environ
-open Evd
-open Reductionops
-open Pretype_errors
-open Sigma.Notations
-
-(** Combinators *)
-
-let evd_comb0 f evdref =
- let (evd',x) = f !evdref in
- evdref := evd';
- x
-
-let evd_comb1 f evdref x =
- let (evd',y) = f !evdref x in
- evdref := evd';
- y
-
-let evd_comb2 f evdref x y =
- let (evd',z) = f !evdref x y in
- evdref := evd';
- z
-
-let e_new_global evdref x =
- evd_comb1 (Evd.fresh_global (Global.env())) evdref x
-
-let new_global evd x =
- Sigma.fresh_global (Global.env()) evd x
-
-(****************************************************)
-(* Expanding/testing/exposing existential variables *)
-(****************************************************)
-
-(* flush_and_check_evars fails if an existential is undefined *)
-
-exception Uninstantiated_evar of existential_key
-
-let rec flush_and_check_evars sigma c =
- match kind_of_term c with
- | Evar (evk,_ as ev) ->
- (match existential_opt_value sigma ev with
- | None -> raise (Uninstantiated_evar evk)
- | Some c -> flush_and_check_evars sigma c)
- | _ -> map_constr (flush_and_check_evars sigma) c
-
-(* let nf_evar_key = Profile.declare_profile "nf_evar" *)
-(* let nf_evar = Profile.profile2 nf_evar_key Reductionops.nf_evar *)
-let nf_evar = Reductionops.nf_evar
-let j_nf_evar sigma j =
- { uj_val = nf_evar sigma j.uj_val;
- uj_type = nf_evar sigma j.uj_type }
-let j_nf_betaiotaevar sigma j =
- { uj_val = nf_evar sigma j.uj_val;
- uj_type = Reductionops.nf_betaiota sigma j.uj_type }
-let jl_nf_evar sigma jl = List.map (j_nf_evar sigma) jl
-let jv_nf_betaiotaevar sigma jl =
- Array.map (j_nf_betaiotaevar sigma) jl
-let jv_nf_evar sigma = Array.map (j_nf_evar sigma)
-let tj_nf_evar sigma {utj_val=v;utj_type=t} =
- {utj_val=nf_evar sigma v;utj_type=t}
-
-let env_nf_evar sigma env =
- let open Context.Rel.Declaration in
- process_rel_context
- (fun d e -> push_rel (map_constr (nf_evar sigma) d) e) env
-
-let env_nf_betaiotaevar sigma env =
- let open Context.Rel.Declaration in
- process_rel_context
- (fun d e ->
- push_rel (map_constr (Reductionops.nf_betaiota sigma) d) e) env
-
-let nf_evars_universes evm =
- Universes.nf_evars_and_universes_opt_subst (Reductionops.safe_evar_value evm)
- (Evd.universe_subst evm)
-
-let nf_evars_and_universes evm =
- let evm = Evd.nf_constraints evm in
- evm, nf_evars_universes evm
-
-let e_nf_evars_and_universes evdref =
- evdref := Evd.nf_constraints !evdref;
- nf_evars_universes !evdref, Evd.universe_subst !evdref
-
-let nf_evar_map_universes evm =
- let evm = Evd.nf_constraints evm in
- let subst = Evd.universe_subst evm in
- if Univ.LMap.is_empty subst then evm, nf_evar evm
- else
- let f = nf_evars_universes evm in
- Evd.raw_map (fun _ -> map_evar_info f) evm, f
-
-let nf_named_context_evar sigma ctx =
- Context.Named.map (nf_evar sigma) ctx
-
-let nf_rel_context_evar sigma ctx =
- Context.Rel.map (nf_evar sigma) ctx
-
-let nf_env_evar sigma env =
- let nc' = nf_named_context_evar sigma (Environ.named_context env) in
- let rel' = nf_rel_context_evar sigma (Environ.rel_context env) in
- push_rel_context rel' (reset_with_named_context (val_of_named_context nc') env)
-
-let nf_evar_info evc info = map_evar_info (nf_evar evc) info
-
-let nf_evar_map evm =
- Evd.raw_map (fun _ evi -> nf_evar_info evm evi) evm
-
-let nf_evar_map_undefined evm =
- Evd.raw_map_undefined (fun _ evi -> nf_evar_info evm evi) 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
- try let _ = has_ev t in false
- with (Not_found | NotInstantiatedEvar) -> true
-
-let is_ground_term evd t =
- not (has_undefined_evars evd t)
-
-let is_ground_env evd env =
- let open Context.Rel.Declaration in
- let is_ground_rel_decl = function
- | LocalDef (_,b,_) -> is_ground_term evd b
- | _ -> true in
- let open Context.Named.Declaration in
- let is_ground_named_decl = function
- | LocalDef (_,b,_) -> is_ground_term evd b
- | _ -> true in
- List.for_all is_ground_rel_decl (rel_context env) &&
- List.for_all is_ground_named_decl (named_context env)
-
-(* Memoization is safe since evar_map and environ are applicative
- structures *)
-let memo f =
- let m = ref None in
- fun x y -> match !m with
- | Some (x', y', r) when x == x' && y == y' -> r
- | _ -> let r = f x y in m := Some (x, y, r); r
-
-let is_ground_env = memo is_ground_env
-
-(* Return the head evar if any *)
-
-exception NoHeadEvar
-
-let head_evar =
- let rec hrec c = match kind_of_term c with
- | Evar (evk,_) -> evk
- | Case (_,_,c,_) -> hrec c
- | App (c,_) -> hrec c
- | Cast (c,_,_) -> hrec c
- | _ -> raise NoHeadEvar
- in
- hrec
-
-(* Expand head evar if any (currently consider only applications but I
- 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
- | Cast (c,_,_) -> whrec (c, l)
- | App (f,args) -> whrec (f, args :: l)
- | _ -> s
- in
- whrec (c, [])
-
-let whd_head_evar sigma c =
- 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)
-
-(**********************)
-(* Creating new metas *)
-(**********************)
-
-let meta_counter_summary_name = "meta counter"
-
-(* Generator of metavariables *)
-let new_meta =
- let meta_ctr = Summary.ref 0 ~name:meta_counter_summary_name in
- fun () -> incr meta_ctr; !meta_ctr
-
-let mk_new_meta () = mkMeta(new_meta())
-
-(* The list of non-instantiated existential declarations (order is important) *)
-
-let non_instantiated sigma =
- let listev = Evd.undefined_map sigma in
- Evar.Map.smartmap (fun evi -> nf_evar_info sigma evi) listev
-
-(************************)
-(* Manipulating filters *)
-(************************)
-
-let make_pure_subst evi args =
- let open Context.Named.Declaration in
- snd (List.fold_right
- (fun decl (args,l) ->
- match args with
- | a::rest -> (rest, (get_id decl, a)::l)
- | _ -> anomaly (Pp.str "Instance does not match its signature"))
- (evar_filtered_context evi) (Array.rev_to_list args,[]))
-
-(*------------------------------------*
- * functional operations on evar sets *
- *------------------------------------*)
-
-(* [push_rel_context_to_named_context] builds the defining context and the
- * initial instance of an evar. If the evar is to be used in context
- *
- * Gamma = a1 ... an xp ... x1
- * \- named part -/ \- de Bruijn part -/
- *
- * then the x1...xp are turned into variables so that the evar is declared in
- * context
- *
- * a1 ... an xp ... x1
- * \----------- named part ------------/
- *
- * but used applied to the initial instance "a1 ... an Rel(p) ... Rel(1)"
- * so that ev[a1:=a1 ... an:=an xp:=Rel(p) ... x1:=Rel(1)] is correctly typed
- * in context Gamma.
- *
- * Remark 1: The instance is reverted in practice (i.e. Rel(1) comes first)
- * Remark 2: If some of the ai or xj are definitions, we keep them in the
- * instance. This is necessary so that no unfolding of local definitions
- * happens when inferring implicit arguments (consider e.g. the problem
- * "x:nat; x':=x; f:forall y, y=y -> Prop |- f _ (refl_equal x')" which
- * produces the equation "?y[x,x']=?y[x,x']" =? "x'=x'": we want
- * the hole to be instantiated by x', not by x (which would have been
- * the case in [invert_definition] if x' had disappeared from the instance).
- * Note that at any time, if, in some context env, the instance of
- * declaration x:A is t and the instance of definition x':=phi(x) is u, then
- * we have the property that u and phi(t) are convertible in env.
- *)
-
-let subst2 subst vsubst c =
- substl subst (replace_vars vsubst c)
-
-let push_rel_context_to_named_context env typ =
- (* compute the instances relative to the named context and rel_context *)
- let open Context.Named.Declaration in
- let ids = List.map get_id (named_context env) in
- let inst_vars = List.map mkVar ids in
- let inst_rels = List.rev (rel_list 0 (nb_rel env)) in
- let replace_var_named_declaration id0 id decl =
- let id' = get_id decl in
- let id' = if Id.equal id0 id' then id else id' in
- let vsubst = [id0 , mkVar id] in
- decl |> set_id id' |> map_constr (replace_vars vsubst)
- in
- let replace_var_named_context id0 id env =
- let nc = Environ.named_context env in
- let nc' = List.map (replace_var_named_declaration id0 id) nc in
- Environ.reset_with_named_context (val_of_named_context nc') env
- in
- let extract_if_neq id = function
- | Anonymous -> None
- | Name id' when id_ord id id' = 0 -> None
- | Name id' -> Some id'
- in
- (* move the rel context to a named context and extend the named instance *)
- (* with vars of the rel context *)
- (* We do keep the instances corresponding to local definition (see above) *)
- let (subst, vsubst, _, env) =
- Context.Rel.fold_outside
- (fun decl (subst, vsubst, avoid, env) ->
- let open Context.Rel.Declaration in
- let na = get_name decl in
- let c = get_value decl in
- let t = get_type decl in
- let open Context.Named.Declaration in
- let id =
- (* ppedrot: we want to infer nicer names for the refine tactic, but
- keeping at the same time backward compatibility in other code
- using this function. For now, we only attempt to preserve the
- old behaviour of Program, but ultimately, one should do something
- about this whole name generation problem. *)
- if Flags.is_program_mode () then next_name_away na avoid
- else next_ident_away (id_of_name_using_hdchar env t na) avoid
- in
- match extract_if_neq id na with
- | Some id0 when not (is_section_variable id0) ->
- (* spiwack: if [id<>id0], rather than introducing a new
- binding named [id], we will keep [id0] (the name given
- by the user) and rename [id0] into [id] in the named
- context. Unless [id] is a section variable. *)
- let subst = List.map (replace_vars [id0,mkVar id]) subst in
- let vsubst = (id0,mkVar id)::vsubst in
- let d = match c with
- | None -> LocalAssum (id0, subst2 subst vsubst t)
- | Some c -> LocalDef (id0, subst2 subst vsubst c, subst2 subst vsubst t)
- in
- let env = replace_var_named_context id0 id env in
- (mkVar id0 :: subst, vsubst, id::avoid, push_named d env)
- | _ ->
- (* spiwack: if [id0] is a section variable renaming it is
- incorrect. We revert to a less robust behaviour where
- the new binder has name [id]. Which amounts to the same
- behaviour than when [id=id0]. *)
- let d = match c with
- | None -> LocalAssum (id, subst2 subst vsubst t)
- | Some c -> LocalDef (id, subst2 subst vsubst c, subst2 subst vsubst t)
- in
- (mkVar id :: subst, vsubst, id::avoid, push_named d env)
- )
- (rel_context env) ~init:([], [], ids, env) in
- (named_context_val env, subst2 subst vsubst typ, inst_rels@inst_vars, subst, vsubst)
-
-(*------------------------------------*
- * Entry points to define new evars *
- *------------------------------------*)
-
-let default_source = (Loc.ghost,Evar_kinds.InternalHole)
-
-let restrict_evar evd evk filter candidates =
- let evd = Sigma.to_evar_map evd in
- let evd, evk' = Evd.restrict evk filter ?candidates evd in
- Sigma.Unsafe.of_pair (evk', Evd.declare_future_goal evk' evd)
-
-let new_pure_evar_full evd evi =
- let evd = Sigma.to_evar_map evd in
- let (evd, evk) = Evd.new_evar evd evi in
- let evd = Evd.declare_future_goal evk evd in
- Sigma.Unsafe.of_pair (evk, evd)
-
-let new_pure_evar sign evd ?(src=default_source) ?(filter = Filter.identity) ?candidates ?(store = Store.empty) ?naming ?(principal=false) typ =
- let evd = Sigma.to_evar_map evd in
- let default_naming = Misctypes.IntroAnonymous in
- let naming = Option.default default_naming naming in
- let evi = {
- evar_hyps = sign;
- evar_concl = typ;
- evar_body = Evar_empty;
- evar_filter = filter;
- evar_source = src;
- evar_candidates = candidates;
- evar_extra = store; }
- in
- let (evd, newevk) = Evd.new_evar evd ~naming evi in
- let evd =
- if principal then Evd.declare_principal_goal newevk evd
- else Evd.declare_future_goal newevk evd
- in
- Sigma.Unsafe.of_pair (newevk, evd)
-
-let new_evar_instance sign evd typ ?src ?filter ?candidates ?store ?naming ?principal instance =
- assert (not !Flags.debug ||
- List.distinct (ids_of_named_context (named_context_of_val sign)));
- let Sigma (newevk, evd, p) = new_pure_evar sign evd ?src ?filter ?candidates ?store ?naming ?principal typ in
- Sigma (mkEvar (newevk,Array.of_list instance), evd, p)
-
-(* [new_evar] declares a new existential in an env env with type typ *)
-(* Converting the env into the sign of the evar to define *)
-let new_evar env evd ?src ?filter ?candidates ?store ?naming ?principal typ =
- let sign,typ',instance,subst,vsubst = push_rel_context_to_named_context env typ in
- let candidates = Option.map (List.map (subst2 subst vsubst)) candidates in
- let instance =
- match filter with
- | None -> instance
- | Some filter -> Filter.filter_list filter instance in
- new_evar_instance sign evd typ' ?src ?filter ?candidates ?store ?naming ?principal instance
-
-let new_evar_unsafe env evd ?src ?filter ?candidates ?store ?naming ?principal typ =
- let evd = Sigma.Unsafe.of_evar_map evd in
- let Sigma (evk, evd, _) = new_evar env evd ?src ?filter ?candidates ?store ?naming ?principal typ in
- (Sigma.to_evar_map evd, evk)
-
-let new_type_evar env evd ?src ?filter ?naming ?principal rigid =
- let Sigma (s, evd', p) = Sigma.new_sort_variable rigid evd in
- let Sigma (e, evd', q) = new_evar env evd' ?src ?filter ?naming ?principal (mkSort s) in
- Sigma ((e, s), evd', p +> q)
-
-let e_new_type_evar env evdref ?src ?filter ?naming ?principal rigid =
- let sigma = Sigma.Unsafe.of_evar_map !evdref in
- let Sigma (c, sigma, _) = new_type_evar env sigma ?src ?filter ?naming ?principal rigid in
- let sigma = Sigma.to_evar_map sigma in
- evdref := sigma;
- c
-
-let new_Type ?(rigid=Evd.univ_flexible) env evd =
- let Sigma (s, sigma, p) = Sigma.new_sort_variable rigid evd in
- Sigma (mkSort s, sigma, p)
-
-let e_new_Type ?(rigid=Evd.univ_flexible) env evdref =
- let evd', s = new_sort_variable rigid !evdref in
- evdref := evd'; mkSort s
-
- (* The same using side-effect *)
-let e_new_evar env evdref ?(src=default_source) ?filter ?candidates ?store ?naming ?principal ty =
- let (evd',ev) = new_evar_unsafe env !evdref ~src:src ?filter ?candidates ?store ?naming ?principal ty in
- evdref := evd';
- ev
-
-(* This assumes an evar with identity instance and generalizes it over only
- the De Bruijn part of the context *)
-let generalize_evar_over_rels sigma (ev,args) =
- let evi = Evd.find sigma ev in
- let sign = named_context_of_val evi.evar_hyps in
- List.fold_left2
- (fun (c,inst as x) a d ->
- if isRel a then (mkNamedProd_or_LetIn d c,a::inst) else x)
- (evi.evar_concl,[]) (Array.to_list args) sign
-
-(************************************)
-(* Removing a dependency in an evar *)
-(************************************)
-
-type clear_dependency_error =
-| OccurHypInSimpleClause of Id.t option
-| EvarTypingBreak of existential
-
-exception ClearDependencyError of Id.t * clear_dependency_error
-
-let cleared = Store.field ()
-
-exception Depends of Id.t
-
-let rec check_and_clear_in_constr env evdref err ids c =
- (* returns a new constr where all the evars have been 'cleaned'
- (ie the hypotheses ids have been removed from the contexts of
- evars) *)
- let check id' =
- if Id.Set.mem id' ids then
- raise (ClearDependencyError (id',err))
- in
- match kind_of_term c with
- | Var id' ->
- check id'; c
-
- | ( Const _ | Ind _ | Construct _ ) ->
- let vars = Environ.vars_of_global env c in
- Id.Set.iter check vars; c
-
- | Evar (evk,l as ev) ->
- if Evd.is_defined !evdref evk then
- (* If evk is already defined we replace it by its definition *)
- let nc = whd_evar !evdref c in
- (check_and_clear_in_constr env evdref err ids nc)
- else
- (* We check for dependencies to elements of ids in the
- evar_info corresponding to e and in the instance of
- arguments. Concurrently, we build a new evar
- corresponding to e where hypotheses of ids have been
- removed *)
- let evi = Evd.find_undefined !evdref evk in
- let ctxt = Evd.evar_filtered_context evi in
- let (rids,filter) =
- List.fold_right2
- (fun h a (ri,filter) ->
- try
- (* Check if some id to clear occurs in the instance
- a of rid in ev and remember the dependency *)
- let check id = if Id.Set.mem id ids then raise (Depends id) in
- let () = Id.Set.iter check (collect_vars a) in
- (* Check if some rid to clear in the context of ev
- has dependencies in another hyp of the context of ev
- and transitively remember the dependency *)
- let check id _ =
- if occur_var_in_decl (Global.env ()) id h
- then raise (Depends id)
- in
- let () = Id.Map.iter check ri in
- (* No dependency at all, we can keep this ev's context hyp *)
- (ri, true::filter)
- with Depends id -> let open Context.Named.Declaration in
- (Id.Map.add (get_id h) id ri, false::filter))
- ctxt (Array.to_list l) (Id.Map.empty,[]) in
- (* Check if some rid to clear in the context of ev has dependencies
- in the type of ev and adjust the source of the dependency *)
- let _nconcl =
- try
- let nids = Id.Map.domain rids in
- check_and_clear_in_constr env evdref (EvarTypingBreak ev) nids (evar_concl evi)
- with ClearDependencyError (rid,err) ->
- raise (ClearDependencyError (Id.Map.find rid rids,err)) in
-
- if Id.Map.is_empty rids then c
- else
- let origfilter = Evd.evar_filter evi in
- let filter = Evd.Filter.apply_subfilter origfilter filter in
- let evd = Sigma.Unsafe.of_evar_map !evdref in
- let Sigma (_, evd, _) = restrict_evar evd evk filter None in
- let evd = Sigma.to_evar_map evd in
- evdref := evd;
- (* spiwack: hacking session to mark the old [evk] as having been "cleared" *)
- let evi = Evd.find !evdref evk in
- let extra = evi.evar_extra in
- let extra' = Store.set extra cleared true in
- let evi' = { evi with evar_extra = extra' } in
- evdref := Evd.add !evdref evk evi' ;
- (* spiwack: /hacking session *)
- whd_evar !evdref c
-
- | _ -> map_constr (check_and_clear_in_constr env evdref err ids) c
-
-let clear_hyps_in_evi_main env evdref hyps terms ids =
- (* clear_hyps_in_evi erases hypotheses ids in hyps, checking if some
- hypothesis does not depend on a element of ids, and erases ids in
- the contexts of the evars occurring in evi *)
- let terms =
- List.map (check_and_clear_in_constr env evdref (OccurHypInSimpleClause None) ids) terms in
- let nhyps =
- let open Context.Named.Declaration in
- let check_context decl =
- let err = OccurHypInSimpleClause (Some (get_id decl)) in
- map_constr (check_and_clear_in_constr env evdref err ids) decl
- in
- let check_value vk = match force_lazy_val vk with
- | None -> vk
- | Some (_, d) ->
- if (Id.Set.for_all (fun e -> not (Id.Set.mem e d)) ids) then
- (* v does depend on any of ids, it's ok *)
- vk
- else
- (* v depends on one of the cleared hyps:
- we forget the computed value *)
- dummy_lazy_val ()
- in
- remove_hyps ids check_context check_value hyps
- in
- (nhyps,terms)
-
-let clear_hyps_in_evi env evdref hyps concl ids =
- match clear_hyps_in_evi_main env evdref hyps [concl] ids with
- | (nhyps,[nconcl]) -> (nhyps,nconcl)
- | _ -> assert false
-
-let clear_hyps2_in_evi env evdref hyps t concl ids =
- match clear_hyps_in_evi_main env evdref hyps [t;concl] ids with
- | (nhyps,[t;nconcl]) -> (nhyps,t,nconcl)
- | _ -> assert false
-
-(* spiwack: a few functions to gather evars on which goals depend. *)
-let queue_set q is_dependent set =
- Evar.Set.iter (fun a -> Queue.push (is_dependent,a) q) set
-let queue_term q is_dependent c =
- queue_set q is_dependent (evars_of_term c)
-
-let process_dependent_evar q acc evm is_dependent e =
- let evi = Evd.find evm e in
- (* Queues evars appearing in the types of the goal (conclusion, then
- hypotheses), they are all dependent. *)
- queue_term q true evi.evar_concl;
- List.iter begin fun decl ->
- let open Context.Named.Declaration in
- queue_term q true (get_type decl);
- match decl with
- | LocalAssum _ -> ()
- | LocalDef (_,b,_) -> queue_term q true b
- end (Environ.named_context_of_val evi.evar_hyps);
- match evi.evar_body with
- | Evar_empty ->
- if is_dependent then Evar.Map.add e None acc else acc
- | Evar_defined b ->
- let subevars = evars_of_term b in
- (* evars appearing in the definition of an evar [e] are marked
- as dependent when [e] is dependent itself: if [e] is a
- non-dependent goal, then, unless they are reach from another
- path, these evars are just other non-dependent goals. *)
- queue_set q is_dependent subevars;
- if is_dependent then Evar.Map.add e (Some subevars) acc else acc
-
-let gather_dependent_evars q evm =
- let acc = ref Evar.Map.empty in
- while not (Queue.is_empty q) do
- let (is_dependent,e) = Queue.pop q in
- (* checks if [e] has already been added to [!acc] *)
- begin if not (Evar.Map.mem e !acc) then
- acc := process_dependent_evar q !acc evm is_dependent e
- end
- done;
- !acc
-
-let gather_dependent_evars evm l =
- let q = Queue.create () in
- List.iter (fun a -> Queue.add (false,a) q) l;
- gather_dependent_evars q evm
-
-(* /spiwack *)
-
-(** The following functions return the set of undefined evars
- contained in the object, the defined evars being traversed.
- This is roughly a combination of the previous functions and
- [nf_evar]. *)
-
-let undefined_evars_of_term evd t =
- let rec evrec acc c =
- match kind_of_term c with
- | Evar (n, l) ->
- let acc = Array.fold_left evrec acc l in
- (try match (Evd.find evd n).evar_body with
- | Evar_empty -> Evar.Set.add n acc
- | Evar_defined c -> evrec acc c
- with Not_found -> anomaly ~label:"undefined_evars_of_term" (Pp.str "evar not found"))
- | _ -> fold_constr evrec acc c
- in
- evrec Evar.Set.empty t
-
-let undefined_evars_of_named_context evd nc =
- let open Context.Named.Declaration in
- Context.Named.fold_outside
- (fold (fun c s -> Evar.Set.union s (undefined_evars_of_term evd c)))
- nc
- ~init:Evar.Set.empty
-
-let undefined_evars_of_evar_info evd evi =
- Evar.Set.union (undefined_evars_of_term evd evi.evar_concl)
- (Evar.Set.union
- (match evi.evar_body with
- | Evar_empty -> Evar.Set.empty
- | Evar_defined b -> undefined_evars_of_term evd b)
- (undefined_evars_of_named_context evd
- (named_context_of_val evi.evar_hyps)))
-
-(* [check_evars] fails if some unresolved evar remains *)
-
-let check_evars env initial_sigma sigma c =
- let rec proc_rec c =
- match kind_of_term c with
- | Evar (evk,_ as ev) ->
- (match existential_opt_value sigma ev with
- | Some c -> proc_rec c
- | None ->
- if not (Evd.mem initial_sigma evk) then
- let (loc,k) = evar_source evk sigma in
- match k with
- | Evar_kinds.ImplicitArg (gr, (i, id), false) -> ()
- | _ -> error_unsolvable_implicit loc env sigma evk None)
- | _ -> iter_constr proc_rec c
- in proc_rec c
-
-(* spiwack: this is a more complete version of
- {!Termops.occur_evar}. The latter does not look recursively into an
- [evar_map]. If unification only need to check superficially, tactics
- do not have this luxury, and need the more complete version. *)
-let occur_evar_upto sigma n c =
- let rec occur_rec c = match kind_of_term c with
- | Evar (sp,_) when Evar.equal sp n -> raise Occur
- | Evar e -> Option.iter occur_rec (existential_opt_value sigma e)
- | _ -> iter_constr occur_rec c
- in
- try occur_rec c; false with Occur -> true
-
-
-(****************************************)
-(* Operations on value/type constraints *)
-(****************************************)
-
-type type_constraint = types option
-
-type val_constraint = constr option
-
-(* Old comment...
- * Basically, we have the following kind of constraints (in increasing
- * strength order):
- * (false,(None,None)) -> no constraint at all
- * (true,(None,None)) -> we must build a judgement which _TYPE is a kind
- * (_,(None,Some ty)) -> we must build a judgement which _TYPE is ty
- * (_,(Some v,_)) -> we must build a judgement which _VAL is v
- * Maybe a concrete datatype would be easier to understand.
- * We differentiate (true,(None,None)) from (_,(None,Some Type))
- * because otherwise Case(s) would be misled, as in
- * (n:nat) Case n of bool [_]nat end would infer the predicate Type instead
- * of Set.
- *)
-
-(* The empty type constraint *)
-let empty_tycon = None
-
-(* Builds a type constraint *)
-let mk_tycon ty = Some ty
-
-(* Constrains the value of a type *)
-let empty_valcon = None
-
-(* Builds a value constraint *)
-let mk_valcon c = Some c
-
-let idx = Namegen.default_dependent_ident
-
-(* Refining an evar to a product *)
-
-let define_pure_evar_as_product evd evk =
- let open Context.Named.Declaration in
- let evi = Evd.find_undefined evd evk in
- let evenv = evar_env evi in
- let id = next_ident_away idx (ids_of_named_context (evar_context evi)) in
- let concl = whd_betadeltaiota evenv evd evi.evar_concl in
- let s = destSort concl in
- let evd1,(dom,u1) =
- let evd = Sigma.Unsafe.of_evar_map evd in
- let Sigma (e, evd1, _) = new_type_evar evenv evd univ_flexible_alg ~filter:(evar_filter evi) in
- (Sigma.to_evar_map evd1, e)
- in
- let evd2,rng =
- let newenv = push_named (LocalAssum (id, dom)) evenv in
- let src = evar_source evk evd1 in
- let filter = Filter.extend 1 (evar_filter evi) in
- if is_prop_sort s then
- (* Impredicative product, conclusion must fall in [Prop]. *)
- new_evar_unsafe newenv evd1 concl ~src ~filter
- else
- let status = univ_flexible_alg in
- let evd3, (rng, srng) =
- let evd1 = Sigma.Unsafe.of_evar_map evd1 in
- let Sigma (e, evd3, _) = new_type_evar newenv evd1 status ~src ~filter in
- (Sigma.to_evar_map evd3, e)
- in
- let prods = Univ.sup (univ_of_sort u1) (univ_of_sort srng) in
- let evd3 = Evd.set_leq_sort evenv evd3 (Type prods) s in
- evd3, rng
- in
- let prod = mkProd (Name id, dom, subst_var id rng) in
- let evd3 = Evd.define evk prod evd2 in
- evd3,prod
-
-(* Refine an applied evar to a product and returns its instantiation *)
-
-let define_evar_as_product evd (evk,args) =
- let evd,prod = define_pure_evar_as_product evd evk in
- (* Quick way to compute the instantiation of evk with args *)
- let na,dom,rng = destProd prod in
- let evdom = mkEvar (fst (destEvar dom), args) in
- let evrngargs = Array.cons (mkRel 1) (Array.map (lift 1) args) in
- let evrng = mkEvar (fst (destEvar rng), evrngargs) in
- evd,mkProd (na, evdom, evrng)
-
-(* Refine an evar with an abstraction
-
- I.e., solve x1..xq |- ?e:T(x1..xq) with e:=λy:A.?e'[x1..xq,y] where:
- - either T(x1..xq) = πy:A(x1..xq).B(x1..xq,y)
- or T(x1..xq) = ?d[x1..xq] and we define ?d := πy:?A.?B
- with x1..xq |- ?A:Type and x1..xq,y |- ?B:Type
- - x1..xq,y:A |- ?e':B
-*)
-
-let define_pure_evar_as_lambda env evd evk =
- let open Context.Named.Declaration in
- let evi = Evd.find_undefined evd evk in
- let evenv = evar_env evi in
- let typ = whd_betadeltaiota evenv evd (evar_concl evi) in
- let evd1,(na,dom,rng) = match kind_of_term typ with
- | Prod (na,dom,rng) -> (evd,(na,dom,rng))
- | Evar ev' -> let evd,typ = define_evar_as_product evd ev' in evd,destProd typ
- | _ -> error_not_product_loc Loc.ghost env evd typ in
- let avoid = ids_of_named_context (evar_context evi) in
- let id =
- next_name_away_with_default_using_types "x" na avoid (whd_evar evd dom) in
- let newenv = push_named (LocalAssum (id, dom)) evenv in
- let filter = Filter.extend 1 (evar_filter evi) in
- let src = evar_source evk evd1 in
- let evd2,body = new_evar_unsafe newenv evd1 ~src (subst1 (mkVar id) rng) ~filter in
- let lam = mkLambda (Name id, dom, subst_var id body) in
- Evd.define evk lam evd2, lam
-
-let define_evar_as_lambda env evd (evk,args) =
- let evd,lam = define_pure_evar_as_lambda env evd evk in
- (* Quick way to compute the instantiation of evk with args *)
- let na,dom,body = destLambda lam in
- let evbodyargs = Array.cons (mkRel 1) (Array.map (lift 1) args) in
- let evbody = mkEvar (fst (destEvar body), evbodyargs) in
- evd,mkLambda (na, dom, evbody)
-
-let rec evar_absorb_arguments env evd (evk,args as ev) = function
- | [] -> evd,ev
- | a::l ->
- (* TODO: optimize and avoid introducing intermediate evars *)
- let evd,lam = define_pure_evar_as_lambda env evd evk in
- let _,_,body = destLambda lam in
- let evk = fst (destEvar body) in
- evar_absorb_arguments env evd (evk, Array.cons a args) l
-
-(* Refining an evar to a sort *)
-
-let define_evar_as_sort env evd (ev,args) =
- let evd, u = new_univ_variable univ_rigid evd in
- let evi = Evd.find_undefined evd ev in
- let s = Type u in
- let concl = whd_betadeltaiota (evar_env evi) evd evi.evar_concl in
- let sort = destSort concl in
- let evd' = Evd.define ev (mkSort s) evd in
- Evd.set_leq_sort env evd' (Type (Univ.super u)) sort, s
-
-(* We don't try to guess in which sort the type should be defined, since
- any type has type Type. May cause some trouble, but not so far... *)
-
-let judge_of_new_Type evd =
- let Sigma (s, evd', p) = Sigma.new_univ_variable univ_rigid evd in
- Sigma ({ uj_val = mkSort (Type s); uj_type = mkSort (Type (Univ.super s)) }, evd', p)
-
-(* Propagation of constraints through application and abstraction:
- Given a type constraint on a functional term, returns the type
- constraint on its domain and codomain. If the input constraint is
- an evar instantiate it with the product of 2 new evars. *)
-
-let split_tycon loc env evd tycon =
- let rec real_split evd c =
- let t = whd_betadeltaiota env evd c in
- match kind_of_term t with
- | Prod (na,dom,rng) -> evd, (na, dom, rng)
- | Evar ev (* ev is undefined because of whd_betadeltaiota *) ->
- let (evd',prod) = define_evar_as_product evd ev in
- let (_,dom,rng) = destProd prod in
- evd',(Anonymous, dom, rng)
- | App (c,args) when isEvar c ->
- let (evd',lam) = define_evar_as_lambda env evd (destEvar c) in
- real_split evd' (mkApp (lam,args))
- | _ -> error_not_product_loc loc env evd c
- in
- match tycon with
- | None -> evd,(Anonymous,None,None)
- | Some c ->
- let evd', (n, dom, rng) = real_split evd c in
- evd', (n, mk_tycon dom, mk_tycon rng)
-
-let valcon_of_tycon x = x
-let lift_tycon n = Option.map (lift n)
-
-let pr_tycon env = function
- None -> str "None"
- | Some t -> Termops.print_constr_env env t
-
-let subterm_source evk (loc,k) =
- let evk = match k with
- | Evar_kinds.SubEvar (evk) -> evk
- | _ -> evk in
- (loc,Evar_kinds.SubEvar evk)
-
-
-(** Term exploration up to instantiation. *)
-let kind_of_term_upto sigma t =
- Constr.kind (Reductionops.whd_evar sigma t)
-
-(** [eq_constr_univs_test sigma1 sigma2 t u] tests equality of [t] and
- [u] up to existential variable instantiation and equalisable
- universes. The term [t] is interpreted in [sigma1] while [u] is
- interpreted in [sigma2]. The universe constraints in [sigma2] are
- assumed to be an extention of those in [sigma1]. *)
-let eq_constr_univs_test sigma1 sigma2 t u =
- (* spiwack: mild code duplication with {!Evd.eq_constr_univs}. *)
- let open Evd in
- let fold cstr sigma =
- try Some (add_universe_constraints sigma cstr)
- with Univ.UniverseInconsistency _ | UniversesDiffer -> None
- in
- let ans =
- Universes.eq_constr_univs_infer_with
- (fun t -> kind_of_term_upto sigma1 t)
- (fun u -> kind_of_term_upto sigma2 u)
- (universes sigma2) fold t u sigma2
- in
- match ans with None -> false | Some _ -> true
diff --git a/pretyping/evarutil.mli b/pretyping/evarutil.mli
deleted file mode 100644
index bc4c37a91..000000000
--- a/pretyping/evarutil.mli
+++ /dev/null
@@ -1,253 +0,0 @@
-(************************************************************************)
-(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
-(* \VV/ **************************************************************)
-(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
-(************************************************************************)
-
-open Names
-open Term
-open Evd
-open Environ
-
-(** {5 This modules provides useful functions for unification modulo evars } *)
-
-(** {6 Metas} *)
-
-(** [new_meta] is a generator of unique meta variables *)
-val new_meta : unit -> metavariable
-val mk_new_meta : unit -> constr
-
-(** {6 Creating a fresh evar given their type and context} *)
-val new_evar :
- env -> 'r Sigma.t -> ?src:Loc.t * Evar_kinds.t -> ?filter:Filter.t ->
- ?candidates:constr list -> ?store:Store.t ->
- ?naming:Misctypes.intro_pattern_naming_expr ->
- ?principal:bool -> types -> (constr, 'r) Sigma.sigma
-
-val new_pure_evar :
- named_context_val -> 'r Sigma.t -> ?src:Loc.t * Evar_kinds.t -> ?filter:Filter.t ->
- ?candidates:constr list -> ?store:Store.t ->
- ?naming:Misctypes.intro_pattern_naming_expr ->
- ?principal:bool -> types -> (evar, 'r) Sigma.sigma
-
-val new_pure_evar_full : 'r Sigma.t -> evar_info -> (evar, 'r) Sigma.sigma
-
-(** the same with side-effects *)
-val e_new_evar :
- env -> evar_map ref -> ?src:Loc.t * Evar_kinds.t -> ?filter:Filter.t ->
- ?candidates:constr list -> ?store:Store.t ->
- ?naming:Misctypes.intro_pattern_naming_expr ->
- ?principal:bool -> types -> constr
-
-(** Create a new Type existential variable, as we keep track of
- them during type-checking and unification. *)
-val new_type_evar :
- env -> 'r Sigma.t -> ?src:Loc.t * Evar_kinds.t -> ?filter:Filter.t ->
- ?naming:Misctypes.intro_pattern_naming_expr -> ?principal:bool -> rigid ->
- (constr * sorts, 'r) Sigma.sigma
-
-val e_new_type_evar : env -> evar_map ref ->
- ?src:Loc.t * Evar_kinds.t -> ?filter:Filter.t ->
- ?naming:Misctypes.intro_pattern_naming_expr -> ?principal:bool -> rigid -> constr * sorts
-
-val new_Type : ?rigid:rigid -> env -> 'r Sigma.t -> (constr, 'r) Sigma.sigma
-val e_new_Type : ?rigid:rigid -> env -> evar_map ref -> constr
-
-val restrict_evar : 'r Sigma.t -> existential_key -> Filter.t ->
- constr list option -> (existential_key, 'r) Sigma.sigma
-
-(** Polymorphic constants *)
-
-val new_global : 'r Sigma.t -> Globnames.global_reference -> (constr, 'r) Sigma.sigma
-val e_new_global : evar_map ref -> Globnames.global_reference -> constr
-
-(** Create a fresh evar in a context different from its definition context:
- [new_evar_instance sign evd ty inst] creates a new evar of context
- [sign] and type [ty], [inst] is a mapping of the evar context to
- the context where the evar should occur. This means that the terms
- of [inst] are typed in the occurrence context and their type (seen
- as a telescope) is [sign] *)
-val new_evar_instance :
- named_context_val -> 'r Sigma.t -> types ->
- ?src:Loc.t * Evar_kinds.t -> ?filter:Filter.t -> ?candidates:constr list ->
- ?store:Store.t -> ?naming:Misctypes.intro_pattern_naming_expr ->
- ?principal:bool ->
- constr list -> (constr, 'r) Sigma.sigma
-
-val make_pure_subst : evar_info -> constr array -> (Id.t * constr) list
-
-(** {6 Evars/Metas switching...} *)
-
-val non_instantiated : evar_map -> evar_info Evar.Map.t
-
-(** {6 Unification utils} *)
-
-(** [head_evar c] returns the head evar of [c] if any *)
-exception NoHeadEvar
-val head_evar : constr -> existential_key (** may raise NoHeadEvar *)
-
-(* Expand head evar if any *)
-val whd_head_evar : evar_map -> constr -> constr
-
-(* An over-approximation of [has_undefined (nf_evars evd c)] *)
-val has_undefined_evars : evar_map -> constr -> bool
-
-val is_ground_term : evar_map -> constr -> bool
-val is_ground_env : evar_map -> env -> bool
-(** [check_evars env initial_sigma extended_sigma c] fails if some
- new unresolved evar remains in [c] *)
-val check_evars : env -> evar_map -> evar_map -> constr -> unit
-
-val define_evar_as_product : evar_map -> existential -> evar_map * types
-val define_evar_as_lambda : env -> evar_map -> existential -> evar_map * types
-val define_evar_as_sort : env -> evar_map -> existential -> evar_map * sorts
-
-(** Instantiate an evar by as many lambda's as needed so that its arguments
- are moved to the evar substitution (i.e. turn [?x[vars1:=args1] args] into
- [?y[vars1:=args1,vars:=args]] with
- [vars1 |- ?x:=\vars.?y[vars1:=vars1,vars:=vars]] *)
-val evar_absorb_arguments : env -> evar_map -> existential -> constr list ->
- evar_map * existential
-
-(** [gather_dependent_evars evm seeds] classifies the evars in [evm]
- as dependent_evars and goals (these may overlap). A goal is an
- evar in [seeds] or an evar appearing in the (partial) definition
- of a goal. A dependent evar is an evar appearing in the type
- (hypotheses and conclusion) of a goal, or in the type or (partial)
- definition of a dependent evar. The value return is a map
- associating to each dependent evar [None] if it has no (partial)
- definition or [Some s] if [s] is the list of evars appearing in
- its (partial) definition. *)
-val gather_dependent_evars : evar_map -> evar list -> (Evar.Set.t option) Evar.Map.t
-
-(** The following functions return the set of undefined evars
- contained in the object, the defined evars being traversed.
- This is roughly a combination of the previous functions and
- [nf_evar]. *)
-
-val undefined_evars_of_term : evar_map -> constr -> Evar.Set.t
-val undefined_evars_of_named_context : evar_map -> Context.Named.t -> Evar.Set.t
-val undefined_evars_of_evar_info : evar_map -> evar_info -> Evar.Set.t
-
-(** [occur_evar_upto sigma k c] returns [true] if [k] appears in
- [c]. It looks up recursively in [sigma] for the value of existential
- variables. *)
-val occur_evar_upto : evar_map -> Evar.t -> Constr.t -> bool
-
-(** {6 Value/Type constraints} *)
-
-val judge_of_new_Type : 'r Sigma.t -> (unsafe_judgment, 'r) Sigma.sigma
-
-type type_constraint = types option
-type val_constraint = constr option
-
-val empty_tycon : type_constraint
-val mk_tycon : constr -> type_constraint
-val empty_valcon : val_constraint
-val mk_valcon : constr -> val_constraint
-
-val split_tycon :
- Loc.t -> env -> evar_map -> type_constraint ->
- evar_map * (Name.t * type_constraint * type_constraint)
-
-val valcon_of_tycon : type_constraint -> val_constraint
-val lift_tycon : int -> type_constraint -> type_constraint
-
-(***********************************************************)
-
-(** [flush_and_check_evars] raise [Uninstantiated_evar] if an evar remains
- uninstantiated; [nf_evar] leaves uninstantiated evars as is *)
-
-val nf_evar : evar_map -> constr -> constr
-val j_nf_evar : evar_map -> unsafe_judgment -> unsafe_judgment
-val jl_nf_evar :
- evar_map -> unsafe_judgment list -> unsafe_judgment list
-val jv_nf_evar :
- evar_map -> unsafe_judgment array -> unsafe_judgment array
-val tj_nf_evar :
- evar_map -> unsafe_type_judgment -> unsafe_type_judgment
-
-val nf_named_context_evar : evar_map -> Context.Named.t -> Context.Named.t
-val nf_rel_context_evar : evar_map -> Context.Rel.t -> Context.Rel.t
-val nf_env_evar : evar_map -> env -> env
-
-val nf_evar_info : evar_map -> evar_info -> evar_info
-val nf_evar_map : evar_map -> evar_map
-val nf_evar_map_undefined : evar_map -> evar_map
-
-val env_nf_evar : evar_map -> env -> env
-val env_nf_betaiotaevar : evar_map -> env -> env
-
-val j_nf_betaiotaevar : evar_map -> unsafe_judgment -> unsafe_judgment
-val jv_nf_betaiotaevar :
- evar_map -> unsafe_judgment array -> unsafe_judgment array
-(** Presenting terms without solved evars *)
-
-val nf_evars_universes : evar_map -> constr -> constr
-
-val nf_evars_and_universes : evar_map -> evar_map * (constr -> constr)
-val e_nf_evars_and_universes : evar_map ref -> (constr -> constr) * Universes.universe_opt_subst
-
-(** Normalize the evar map w.r.t. universes, after simplification of constraints.
- Return the substitution function for constrs as well. *)
-val nf_evar_map_universes : evar_map -> evar_map * (constr -> constr)
-
-(** Replacing all evars, possibly raising [Uninstantiated_evar] *)
-exception Uninstantiated_evar of existential_key
-val flush_and_check_evars : evar_map -> constr -> constr
-
-(** {6 Term manipulation up to instantiation} *)
-
-(** Like {!Constr.kind} except that [kind_of_term sigma t] exposes [t]
- as an evar [e] only if [e] is uninstantiated in [sigma]. Otherwise the
- value of [e] in [sigma] is (recursively) used. *)
-val kind_of_term_upto : evar_map -> constr -> (constr,types) kind_of_term
-
-(** [eq_constr_univs_test sigma1 sigma2 t u] tests equality of [t] and
- [u] up to existential variable instantiation and equalisable
- universes. The term [t] is interpreted in [sigma1] while [u] is
- interpreted in [sigma2]. The universe constraints in [sigma2] are
- assumed to be an extention of those in [sigma1]. *)
-val eq_constr_univs_test : evar_map -> evar_map -> constr -> constr -> bool
-
-(** {6 debug pretty-printer:} *)
-
-val pr_tycon : env -> type_constraint -> Pp.std_ppcmds
-
-
-(** {6 Removing hyps in evars'context}
-raise OccurHypInSimpleClause if the removal breaks dependencies *)
-
-type clear_dependency_error =
-| OccurHypInSimpleClause of Id.t option
-| EvarTypingBreak of existential
-
-exception ClearDependencyError of Id.t * clear_dependency_error
-
-(* spiwack: marks an evar that has been "defined" by clear.
- used by [Goal] and (indirectly) [Proofview] to handle the clear tactic gracefully*)
-val cleared : bool Store.field
-
-val clear_hyps_in_evi : env -> evar_map ref -> named_context_val -> types ->
- Id.Set.t -> named_context_val * types
-
-val clear_hyps2_in_evi : env -> evar_map ref -> named_context_val -> types -> types ->
- Id.Set.t -> named_context_val * types * types
-
-val push_rel_context_to_named_context : Environ.env -> types ->
- named_context_val * types * constr list * constr list * (identifier*constr) list
-
-val generalize_evar_over_rels : evar_map -> existential -> types * constr list
-
-(** Evar combinators *)
-
-val evd_comb0 : (evar_map -> evar_map * 'a) -> evar_map ref -> 'a
-val evd_comb1 : (evar_map -> 'b -> evar_map * 'a) -> evar_map ref -> 'b -> 'a
-val evd_comb2 : (evar_map -> 'b -> 'c -> evar_map * 'a) -> evar_map ref -> 'b -> 'c -> 'a
-
-val subterm_source : existential_key -> Evar_kinds.t Loc.located ->
- Evar_kinds.t Loc.located
-
-val meta_counter_summary_name : string
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index 8329de2ee..a765d3091 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -36,6 +36,7 @@ open Typeops
open Globnames
open Nameops
open Evarutil
+open Evardefine
open Pretype_errors
open Glob_term
open Glob_ops
@@ -234,6 +235,23 @@ let check_extra_evars_are_solved env current_sigma pending =
| _ ->
error_unsolvable_implicit loc env current_sigma evk None) pending
+(* [check_evars] fails if some unresolved evar remains *)
+
+let check_evars env initial_sigma sigma c =
+ let rec proc_rec c =
+ match kind_of_term c with
+ | Evar (evk,_ as ev) ->
+ (match existential_opt_value sigma ev with
+ | Some c -> proc_rec c
+ | None ->
+ if not (Evd.mem initial_sigma evk) then
+ let (loc,k) = evar_source evk sigma in
+ match k with
+ | Evar_kinds.ImplicitArg (gr, (i, id), false) -> ()
+ | _ -> Pretype_errors.error_unsolvable_implicit loc env sigma evk None)
+ | _ -> Constr.iter proc_rec c
+ in proc_rec c
+
let check_evars_are_solved env current_sigma frozen pending =
check_typeclasses_instances_are_solved env current_sigma frozen;
check_problems_are_solved env current_sigma;
diff --git a/pretyping/pretyping.mli b/pretyping/pretyping.mli
index 40745ed09..4c4c535d8 100644
--- a/pretyping/pretyping.mli
+++ b/pretyping/pretyping.mli
@@ -130,6 +130,10 @@ val solve_remaining_evars : inference_flags ->
val check_evars_are_solved :
env -> (* current map: *) evar_map -> (* map to check: *) pending -> unit
+(** [check_evars env initial_sigma extended_sigma c] fails if some
+ new unresolved evar remains in [c] *)
+val check_evars : env -> evar_map -> evar_map -> constr -> unit
+
(**/**)
(** Internal of Pretyping... *)
val pretype :
diff --git a/pretyping/pretyping.mllib b/pretyping/pretyping.mllib
index b59589bda..c8b3307d7 100644
--- a/pretyping/pretyping.mllib
+++ b/pretyping/pretyping.mllib
@@ -1,4 +1,5 @@
Locusops
+Pretype_errors
Reductionops
Inductiveops
Vnorm
@@ -6,9 +7,8 @@ Arguments_renaming
Nativenorm
Retyping
Cbv
-Pretype_errors
Find_subterm
-Evarutil
+Evardefine
Evarsolve
Recordops
Evarconv
diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml
index 935e18d8d..7f4249c5b 100644
--- a/pretyping/reductionops.ml
+++ b/pretyping/reductionops.ml
@@ -594,9 +594,7 @@ let pr_state (tm,sk) =
(*** Reduction Functions Operators ***)
(*************************************)
-let safe_evar_value sigma ev =
- try Some (Evd.existential_value sigma ev)
- with NotInstantiatedEvar | Not_found -> None
+let safe_evar_value = Evarutil.safe_evar_value
let safe_meta_value sigma ev =
try Some (Evd.meta_value sigma ev)
@@ -1183,30 +1181,8 @@ let whd_zeta c = Stack.zip (local_whd_state_gen zeta Evd.empty (c,Stack.empty))
(****************************************************************************)
(* Replacing defined evars for error messages *)
-let rec whd_evar sigma c =
- match kind_of_term c with
- | Evar ev ->
- let (evk, args) = ev in
- let args = Array.map (fun c -> whd_evar sigma c) args in
- (match safe_evar_value sigma (evk, args) with
- Some c -> whd_evar sigma c
- | None -> c)
- | Sort (Type u) ->
- let u' = Evd.normalize_universe sigma u in
- if u' == u then c else mkSort (Sorts.sort_of_univ u')
- | Const (c', u) when not (Univ.Instance.is_empty u) ->
- let u' = Evd.normalize_universe_instance sigma u in
- if u' == u then c else mkConstU (c', u')
- | Ind (i, u) when not (Univ.Instance.is_empty u) ->
- let u' = Evd.normalize_universe_instance sigma u in
- if u' == u then c else mkIndU (i, u')
- | Construct (co, u) when not (Univ.Instance.is_empty u) ->
- let u' = Evd.normalize_universe_instance sigma u in
- if u' == u then c else mkConstructU (co, u')
- | _ -> c
-
-let nf_evar =
- local_strong whd_evar
+let whd_evar = Evarutil.whd_evar
+let nf_evar = Evarutil.nf_evar
(* lazy reduction functions. The infos must be created for each term *)
(* Note by HH [oct 08] : why would it be the job of clos_norm_flags to add
diff --git a/pretyping/typeclasses.ml b/pretyping/typeclasses.ml
index 0faa35c87..3a5796fe1 100644
--- a/pretyping/typeclasses.ml
+++ b/pretyping/typeclasses.ml
@@ -490,7 +490,7 @@ let is_instance = function
Nota: we will only check the resolvability status of undefined evars.
*)
-let resolvable = Store.field ()
+let resolvable = Proofview.Unsafe.typeclass_resolvable
let set_resolvable s b =
if b then Store.remove s resolvable
diff --git a/pretyping/typing.ml b/pretyping/typing.ml
index 5347d965b..52afa7f83 100644
--- a/pretyping/typing.ml
+++ b/pretyping/typing.ml
@@ -39,7 +39,7 @@ let e_type_judgment env evdref j =
match kind_of_term (whd_betadeltaiota env !evdref j.uj_type) with
| Sort s -> {utj_val = j.uj_val; utj_type = s }
| Evar ev ->
- let (evd,s) = Evarutil.define_evar_as_sort env !evdref ev in
+ let (evd,s) = Evardefine.define_evar_as_sort env !evdref ev in
evdref := evd; { utj_val = j.uj_val; utj_type = s }
| _ -> error_not_type env j
@@ -61,7 +61,7 @@ let e_judge_of_apply env evdref funj argjv =
else
error_cant_apply_bad_type env (n,c1, hj.uj_type) funj argjv
| Evar ev ->
- let (evd',t) = Evarutil.define_evar_as_product !evdref ev in
+ let (evd',t) = Evardefine.define_evar_as_product !evdref ev in
evdref := evd';
let (_,_,c2) = destProd t in
apply_rec (n+1) (subst1 hj.uj_val c2) restjl
diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index a7b415552..a4a386530 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -19,6 +19,7 @@ open Evd
open Reduction
open Reductionops
open Evarutil
+open Evardefine
open Evarsolve
open Pretype_errors
open Retyping
generated by cgit v1.2.3 (git 2.39.1) at 2024-08-20 08:08:16 +0000