aboutsummaryrefslogtreecommitdiff
path: root/pretyping
diff options
context:
space:
mode:
Diffstat (limited to 'pretyping')
-rw-r--r--pretyping/cases.ml7
-rw-r--r--pretyping/cbv.ml68
-rw-r--r--pretyping/classops.ml13
-rw-r--r--pretyping/coercion.ml1
-rw-r--r--pretyping/detyping.ml5
-rw-r--r--pretyping/dune2
-rw-r--r--pretyping/evarconv.ml3
-rw-r--r--pretyping/evarsolve.ml36
-rw-r--r--pretyping/indrec.ml3
-rw-r--r--pretyping/inferCumulativity.ml2
-rw-r--r--pretyping/pretype_errors.ml4
-rw-r--r--pretyping/pretype_errors.mli4
-rw-r--r--pretyping/pretyping.ml17
-rw-r--r--pretyping/recordops.ml3
-rw-r--r--pretyping/reductionops.ml4
-rw-r--r--pretyping/reductionops.mli1
-rw-r--r--pretyping/retyping.ml8
-rw-r--r--pretyping/tacred.ml4
-rw-r--r--pretyping/tacred.mli4
-rw-r--r--pretyping/typeclasses.ml87
-rw-r--r--pretyping/typeclasses.mli12
21 files changed, 145 insertions, 143 deletions
diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index 54e847988b..164f5ab96d 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -296,8 +296,7 @@ let inductive_template env sigma tmloc ind =
let ty = EConstr.of_constr ty in
let ty' = substl subst ty in
let sigma, e =
- Evarutil.new_evar env ~src:(hole_source n)
- sigma ty'
+ Evarutil.new_evar env ~src:(hole_source n) ~typeclass_candidate:false sigma ty'
in
(sigma, e::subst,e::evarl,n+1)
| LocalDef (na,b,ty) ->
@@ -1698,7 +1697,7 @@ let abstract_tycon ?loc env sigma subst tycon extenv t =
(fun i _ ->
try list_assoc_in_triple i subst0 with Not_found -> mkRel i)
1 (rel_context !!env) in
- let sigma, ev' = Evarutil.new_evar ~src !!env sigma ty in
+ let sigma, ev' = Evarutil.new_evar ~src ~typeclass_candidate:false !!env sigma ty in
begin match solve_simple_eqn (evar_conv_x full_transparent_state) !!env sigma (None,ev,substl inst ev') with
| Success evd -> evdref := evd
| UnifFailure _ -> assert false
@@ -1734,7 +1733,7 @@ let abstract_tycon ?loc env sigma subst tycon extenv t =
(named_context !!extenv) in
let filter = Filter.make (rel_filter @ named_filter) in
let candidates = List.rev (u :: List.map mkRel vl) in
- let sigma, ev = Evarutil.new_evar !!extenv ~src ~filter ~candidates sigma ty in
+ let sigma, ev = Evarutil.new_evar !!extenv ~src ~filter ~candidates ~typeclass_candidate:false sigma ty in
let () = evdref := sigma in
lift k ev
in
diff --git a/pretyping/cbv.ml b/pretyping/cbv.ml
index 265909980b..5061aeff88 100644
--- a/pretyping/cbv.ml
+++ b/pretyping/cbv.ml
@@ -134,7 +134,12 @@ let mkSTACK = function
| STACK(0,v0,stk0), stk -> STACK(0,v0,stack_concat stk0 stk)
| v,stk -> STACK(0,v,stk)
-type cbv_infos = { tab : cbv_value infos_tab; infos : cbv_value infos; sigma : Evd.evar_map }
+type cbv_infos = {
+ env : Environ.env;
+ tab : cbv_value KeyTable.t;
+ reds : RedFlags.reds;
+ sigma : Evd.evar_map
+}
(* Change: zeta reduction cannot be avoided in CBV *)
@@ -260,8 +265,8 @@ let rec norm_head info env t stack =
| Proj (p, c) ->
let p' =
- if red_set (info_flags info.infos) (fCONST (Projection.constant p))
- && red_set (info_flags info.infos) fBETA
+ if red_set info.reds (fCONST (Projection.constant p))
+ && red_set info.reds fBETA
then Projection.unfold p
else p
in
@@ -280,16 +285,16 @@ let rec norm_head info env t stack =
| Var id -> norm_head_ref 0 info env stack (VarKey id)
| Const sp ->
- Reductionops.reduction_effect_hook (env_of_infos info.infos) info.sigma
+ Reductionops.reduction_effect_hook info.env info.sigma
(fst sp) (lazy (reify_stack t stack));
norm_head_ref 0 info env stack (ConstKey sp)
| LetIn (_, b, _, c) ->
(* zeta means letin are contracted; delta without zeta means we *)
(* allow bindings but leave let's in place *)
- if red_set (info_flags info.infos) fZETA then
+ if red_set info.reds fZETA then
(* New rule: for Cbv, Delta does not apply to locally bound variables
- or red_set (info_flags info.infos) fDELTA
+ or red_set info.reds fDELTA
*)
let env' = subs_cons ([|cbv_stack_term info TOP env b|],env) in
norm_head info env' c stack
@@ -297,7 +302,7 @@ let rec norm_head info env t stack =
(CBN(t,env), stack) (* Should we consider a commutative cut ? *)
| Evar ev ->
- (match evar_value info.infos.i_cache ev with
+ (match Reductionops.safe_evar_value info.sigma ev with
Some c -> norm_head info env c stack
| None ->
let e, xs = ev in
@@ -317,8 +322,8 @@ let rec norm_head info env t stack =
| Prod _ -> (CBN(t,env), stack)
and norm_head_ref k info env stack normt =
- if red_set_ref (info_flags info.infos) normt then
- match ref_value_cache info.infos info.tab normt with
+ if red_set_ref info.reds normt then
+ match cbv_value_cache info normt with
| Some body ->
if !debug_cbv then Feedback.msg_debug Pp.(str "Unfolding " ++ debug_pr_key normt);
strip_appl (shift_value k body) stack
@@ -343,7 +348,7 @@ and cbv_stack_term info stack env t =
and cbv_stack_value info env = function
(* a lambda meets an application -> BETA *)
| (LAM (nlams,ctxt,b,env), APP (args, stk))
- when red_set (info_flags info.infos) fBETA ->
+ when red_set info.reds fBETA ->
let nargs = Array.length args in
if nargs == nlams then
cbv_stack_term info stk (subs_cons(args,env)) b
@@ -357,31 +362,31 @@ and cbv_stack_value info env = function
(* a Fix applied enough -> IOTA *)
| (FIXP(fix,env,[||]), stk)
- when fixp_reducible (info_flags info.infos) fix stk ->
+ when fixp_reducible info.reds fix stk ->
let (envf,redfix) = contract_fixp env fix in
cbv_stack_term info stk envf redfix
(* constructor guard satisfied or Cofix in a Case -> IOTA *)
| (COFIXP(cofix,env,[||]), stk)
- when cofixp_reducible (info_flags info.infos) cofix stk->
+ when cofixp_reducible info.reds cofix stk->
let (envf,redfix) = contract_cofixp env cofix in
cbv_stack_term info stk envf redfix
(* constructor in a Case -> IOTA *)
| (CONSTR(((sp,n),u),[||]), APP(args,CASE(_,br,ci,env,stk)))
- when red_set (info_flags info.infos) fMATCH ->
+ when red_set info.reds fMATCH ->
let cargs =
Array.sub args ci.ci_npar (Array.length args - ci.ci_npar) in
cbv_stack_term info (stack_app cargs stk) env br.(n-1)
(* constructor of arity 0 in a Case -> IOTA *)
| (CONSTR(((_,n),u),[||]), CASE(_,br,_,env,stk))
- when red_set (info_flags info.infos) fMATCH ->
+ when red_set info.reds fMATCH ->
cbv_stack_term info stk env br.(n-1)
(* constructor in a Projection -> IOTA *)
| (CONSTR(((sp,n),u),[||]), APP(args,PROJ(p,stk)))
- when red_set (info_flags info.infos) fMATCH && Projection.unfolded p ->
+ when red_set info.reds fMATCH && Projection.unfolded p ->
let arg = args.(Projection.npars p + Projection.arg p) in
cbv_stack_value info env (strip_appl arg stk)
@@ -393,6 +398,29 @@ and cbv_stack_value info env = function
(* definitely a value *)
| (head,stk) -> mkSTACK(head, stk)
+and cbv_value_cache info ref = match KeyTable.find info.tab ref with
+| v -> Some v
+| exception Not_found ->
+ try
+ let body = match ref with
+ | RelKey n ->
+ let open Context.Rel.Declaration in
+ begin match Environ.lookup_rel n info.env with
+ | LocalDef (_, c, _) -> lift n c
+ | LocalAssum _ -> raise Not_found
+ end
+ | VarKey id ->
+ let open Context.Named.Declaration in
+ begin match Environ.lookup_named id info.env with
+ | LocalDef (_, c, _) -> c
+ | LocalAssum _ -> raise Not_found
+ end
+ | ConstKey cst -> Environ.constant_value_in info.env cst
+ in
+ let v = cbv_stack_term info TOP (subs_id 0) body in
+ let () = KeyTable.add info.tab ref v in
+ Some v
+ with Not_found | Environ.NotEvaluableConst _ -> None
(* When we are sure t will never produce a redex with its stack, we
* normalize (even under binders) the applied terms and we build the
@@ -453,11 +481,5 @@ let cbv_norm infos constr =
EConstr.of_constr (with_stats (lazy (cbv_norm_term infos (subs_id 0) constr)))
(* constant bodies are normalized at the first expansion *)
-let create_cbv_infos flgs env sigma =
- let infos = create
- ~share:true (** Not used by cbv *)
- ~repr:(fun old_info tab c -> cbv_stack_term { tab; infos = old_info; sigma } TOP (subs_id 0) c)
- flgs
- env
- (Reductionops.safe_evar_value sigma) in
- { tab = CClosure.create_tab (); infos; sigma }
+let create_cbv_infos reds env sigma =
+ { tab = KeyTable.create 91; reds; env; sigma }
diff --git a/pretyping/classops.ml b/pretyping/classops.ml
index b026397abf..2c2a8fe49e 100644
--- a/pretyping/classops.ml
+++ b/pretyping/classops.ml
@@ -15,7 +15,6 @@ open Names
open Constr
open Libnames
open Globnames
-open Nametab
open Libobject
open Mod_subst
@@ -228,14 +227,14 @@ let string_of_class = function
| CL_FUN -> "Funclass"
| CL_SORT -> "Sortclass"
| CL_CONST sp ->
- string_of_qualid (shortest_qualid_of_global Id.Set.empty (ConstRef sp))
+ string_of_qualid (Nametab.shortest_qualid_of_global Id.Set.empty (ConstRef sp))
| CL_PROJ sp ->
let sp = Projection.Repr.constant sp in
- string_of_qualid (shortest_qualid_of_global Id.Set.empty (ConstRef sp))
+ string_of_qualid (Nametab.shortest_qualid_of_global Id.Set.empty (ConstRef sp))
| CL_IND sp ->
- string_of_qualid (shortest_qualid_of_global Id.Set.empty (IndRef sp))
+ string_of_qualid (Nametab.shortest_qualid_of_global Id.Set.empty (IndRef sp))
| CL_SECVAR sp ->
- string_of_qualid (shortest_qualid_of_global Id.Set.empty (VarRef sp))
+ string_of_qualid (Nametab.shortest_qualid_of_global Id.Set.empty (VarRef sp))
let pr_class x = str (string_of_class x)
@@ -380,7 +379,7 @@ type coercion = {
(* Computation of the class arity *)
let reference_arity_length ref =
- let t, _ = Global.type_of_global_in_context (Global.env ()) ref in
+ let t, _ = Typeops.type_of_global_in_context (Global.env ()) ref in
List.length (fst (Reductionops.splay_arity (Global.env()) Evd.empty (EConstr.of_constr t))) (** FIXME *)
let projection_arity_length p =
@@ -520,7 +519,7 @@ module CoercionPrinting =
let compare = GlobRef.Ordered.compare
let encode = coercion_of_reference
let subst = subst_coe_typ
- let printer x = pr_global_env Id.Set.empty x
+ let printer x = Nametab.pr_global_env Id.Set.empty x
let key = ["Printing";"Coercion"]
let title = "Explicitly printed coercions: "
let member_message x b =
diff --git a/pretyping/coercion.ml b/pretyping/coercion.ml
index e15c00f7dc..e21c2fda85 100644
--- a/pretyping/coercion.ml
+++ b/pretyping/coercion.ml
@@ -104,6 +104,7 @@ let make_existential ?loc ?(opaque = not (get_proofs_transparency ())) na env ev
Evar_kinds.qm_name=na;
}) in
let evd, v = Evarutil.new_evar env !evdref ~src c in
+ let evd = Evd.set_obligation_evar evd (fst (destEvar evd v)) in
evdref := evd;
v
diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml
index 592057ab41..072ac9deed 100644
--- a/pretyping/detyping.ml
+++ b/pretyping/detyping.ml
@@ -25,7 +25,6 @@ open Termops
open Namegen
open Libnames
open Globnames
-open Nametab
open Mod_subst
open Decl_kinds
open Context.Named.Declaration
@@ -58,7 +57,7 @@ let add_name_opt na b t (nenv, env) =
(* Tools for printing of Cases *)
let encode_inductive r =
- let indsp = global_inductive r in
+ let indsp = Nametab.global_inductive r in
let constr_lengths = constructors_nrealargs indsp in
(indsp,constr_lengths)
@@ -97,7 +96,7 @@ module PrintingInductiveMake =
let compare = ind_ord
let encode = Test.encode
let subst subst obj = subst_ind subst obj
- let printer ind = pr_global_env Id.Set.empty (IndRef ind)
+ let printer ind = Nametab.pr_global_env Id.Set.empty (IndRef ind)
let key = ["Printing";Test.field]
let title = Test.title
let member_message x = Test.member_message (printer x)
diff --git a/pretyping/dune b/pretyping/dune
index 6609b4e328..14bce92de1 100644
--- a/pretyping/dune
+++ b/pretyping/dune
@@ -3,4 +3,4 @@
(synopsis "Coq's Type Inference Component (Pretyper)")
(public_name coq.pretyping)
(wrapped false)
- (libraries camlp5.gramlib engine))
+ (libraries engine))
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index f0ff1aa93b..6a75be352b 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -711,8 +711,7 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty
in
ise_try evd [f1; f2]
- | Proj (p, c), Proj (p', c')
- when Constant.equal (Projection.constant p) (Projection.constant p') ->
+ | Proj (p, c), Proj (p', c') when Projection.repr_equal p p' ->
let f1 i =
ise_and i
[(fun i -> evar_conv_x ts env i CONV c c');
diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml
index 22f438c00c..96213af9c6 100644
--- a/pretyping/evarsolve.ml
+++ b/pretyping/evarsolve.ml
@@ -83,7 +83,7 @@ let refresh_universes ?(status=univ_rigid) ?(onlyalg=false) ?(refreshset=false)
(** Refresh the types of evars under template polymorphic references *)
let rec refresh_term_evars ~onevars ~top t =
match EConstr.kind !evdref t with
- | App (f, args) when is_template_polymorphic env !evdref f ->
+ | App (f, args) when Termops.is_template_polymorphic_ind env !evdref f ->
let pos = get_polymorphic_positions !evdref f in
refresh_polymorphic_positions args pos; t
| App (f, args) when top && isEvar !evdref f ->
@@ -1238,33 +1238,31 @@ let check_evar_instance evd evk1 body conv_algo =
| Success evd -> evd
| UnifFailure _ -> raise (IllTypedInstance (evenv,ty, evi.evar_concl))
-let update_evar_source ev1 ev2 evd =
- let loc, evs2 = evar_source ev2 evd in
- match evs2 with
- | (Evar_kinds.QuestionMark _ | Evar_kinds.ImplicitArg (_, _, false)) ->
- let evi = Evd.find evd ev1 in
- Evd.add evd ev1 {evi with evar_source = loc, evs2}
- | _ -> evd
-
+let update_evar_info ev1 ev2 evd =
+ (* We update the source of obligation evars during evar-evar unifications. *)
+ let loc, evs1 = evar_source ev1 evd in
+ let evi = Evd.find evd ev2 in
+ Evd.add evd ev2 {evi with evar_source = loc, evs1}
+
let solve_evar_evar_l2r force f g env evd aliases pbty ev1 (evk2,_ as ev2) =
try
let evd,body = project_evar_on_evar force g env evd aliases 0 pbty ev1 ev2 in
- let evd' = Evd.define evk2 body evd in
- let evd' = update_evar_source (fst (destEvar evd body)) evk2 evd' in
- check_evar_instance evd' evk2 body g
+ let evd' = Evd.define_with_evar evk2 body evd in
+ let evd' =
+ if is_obligation_evar evd evk2 then
+ update_evar_info evk2 (fst (destEvar evd' body)) evd'
+ else evd'
+ in
+ check_evar_instance evd' evk2 body g
with EvarSolvedOnTheFly (evd,c) ->
f env evd pbty ev2 c
let opp_problem = function None -> None | Some b -> Some (not b)
let preferred_orientation evd evk1 evk2 =
- let _,src1 = (Evd.find_undefined evd evk1).evar_source in
- let _,src2 = (Evd.find_undefined evd evk2).evar_source in
- (* This is a heuristic useful for program to work *)
- match src1,src2 with
- | (Evar_kinds.QuestionMark _ | Evar_kinds.ImplicitArg (_, _, false)) , _ -> true
- | _, (Evar_kinds.QuestionMark _ | Evar_kinds.ImplicitArg (_, _, false)) -> false
- | _ -> true
+ if is_obligation_evar evd evk1 then true
+ else if is_obligation_evar evd evk2 then false
+ else true
let solve_evar_evar_aux force f g env evd pbty (evk1,args1 as ev1) (evk2,args2 as ev2) =
let aliases = make_alias_map env evd in
diff --git a/pretyping/indrec.ml b/pretyping/indrec.ml
index e49ba75b3f..89f64d328a 100644
--- a/pretyping/indrec.ml
+++ b/pretyping/indrec.ml
@@ -29,7 +29,6 @@ open Inductive
open Inductiveops
open Environ
open Reductionops
-open Nametab
open Context.Rel.Declaration
type dep_flag = bool
@@ -618,6 +617,6 @@ let lookup_eliminator ind_sp s =
user_err ~hdr:"default_elim"
(strbrk "Cannot find the elimination combinator " ++
Id.print id ++ strbrk ", the elimination of the inductive definition " ++
- pr_global_env Id.Set.empty (IndRef ind_sp) ++
+ Nametab.pr_global_env Id.Set.empty (IndRef ind_sp) ++
strbrk " on sort " ++ Termops.pr_sort_family s ++
strbrk " is probably not allowed.")
diff --git a/pretyping/inferCumulativity.ml b/pretyping/inferCumulativity.ml
index a56a8314e6..422a05c19a 100644
--- a/pretyping/inferCumulativity.ml
+++ b/pretyping/inferCumulativity.ml
@@ -196,7 +196,7 @@ let infer_inductive env mie =
Array.fold_left (fun variances u -> LMap.add u Variance.Irrelevant variances)
LMap.empty uarray
in
- let env, _ = Typeops.infer_local_decls env params in
+ let env = Typeops.check_context env params in
let variances = List.fold_left (fun variances entry ->
let variances = infer_arity_constructor true
env variances entry.mind_entry_arity
diff --git a/pretyping/pretype_errors.ml b/pretyping/pretype_errors.ml
index 856894d9a6..01b0d96f98 100644
--- a/pretyping/pretype_errors.ml
+++ b/pretyping/pretype_errors.ml
@@ -164,8 +164,8 @@ let error_not_product ?loc env sigma c =
(*s Error in conversion from AST to glob_constr *)
-let error_var_not_found ?loc s =
- raise_pretype_error ?loc (empty_env, Evd.from_env empty_env, VarNotFound s)
+let error_var_not_found ?loc env sigma s =
+ raise_pretype_error ?loc (env, sigma, VarNotFound s)
(*s Typeclass errors *)
diff --git a/pretyping/pretype_errors.mli b/pretyping/pretype_errors.mli
index 6f14d025c7..054f0c76a9 100644
--- a/pretyping/pretype_errors.mli
+++ b/pretyping/pretype_errors.mli
@@ -150,9 +150,7 @@ val error_unexpected_type :
val error_not_product :
?loc:Loc.t -> env -> Evd.evar_map -> constr -> 'b
-(** {6 Error in conversion from AST to glob_constr } *)
-
-val error_var_not_found : ?loc:Loc.t -> Id.t -> 'b
+val error_var_not_found : ?loc:Loc.t -> env -> Evd.evar_map -> Id.t -> 'b
(** {6 Typeclass errors } *)
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index f2881e4a19..cba1533da5 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -390,7 +390,7 @@ let pretype_id pretype k0 loc env sigma id =
sigma, { uj_val = mkVar id; uj_type = NamedDecl.get_type (lookup_named id !!env) }
with Not_found ->
(* [id] not found, standard error message *)
- error_var_not_found ?loc id
+ error_var_not_found ?loc !!env sigma id
(*************************************************************************)
(* Main pretyping function *)
@@ -436,7 +436,7 @@ let pretype_ref ?loc sigma env ref us =
(* This may happen if env is a goal env and section variables have
been cleared - section variables should be different from goal
variables *)
- Pretype_errors.error_var_not_found ?loc id)
+ Pretype_errors.error_var_not_found ?loc !!env sigma id)
| ref ->
let sigma, c = pretype_global ?loc univ_flexible env sigma ref us in
let ty = unsafe_type_of !!env sigma c in
@@ -457,6 +457,15 @@ let pretype_sort ?loc sigma = function
let new_type_evar env sigma loc =
new_type_evar env sigma ~src:(Loc.tag ?loc Evar_kinds.InternalHole)
+let mark_obligation_evar sigma k evc =
+ if Flags.is_program_mode () then
+ match k with
+ | Evar_kinds.QuestionMark _
+ | Evar_kinds.ImplicitArg (_, _, false) ->
+ Evd.set_obligation_evar sigma (fst (destEvar sigma evc))
+ | _ -> sigma
+ else sigma
+
(* [pretype tycon env sigma lvar lmeta cstr] attempts to type [cstr] *)
(* in environment [env], with existential variables [sigma] and *)
(* the type constraint tycon *)
@@ -510,6 +519,7 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : GlobEnv.t) (sigma
| Some ty -> sigma, ty
| None -> new_type_evar env sigma loc in
let sigma, uj_val = new_evar env sigma ~src:(loc,k) ~naming ty in
+ let sigma = mark_obligation_evar sigma k uj_val in
sigma, { uj_val; uj_type = ty }
| GHole (k, _naming, Some arg) ->
@@ -682,7 +692,7 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : GlobEnv.t) (sigma
let sigma, resj =
match EConstr.kind sigma resj.uj_val with
| App (f,args) ->
- if is_template_polymorphic !!env sigma f then
+ if Termops.is_template_polymorphic_ind !!env sigma f then
(* Special case for inductive type applications that must be
refreshed right away. *)
let c = mkApp (f, args) in
@@ -1030,6 +1040,7 @@ and pretype_type k0 resolve_tc valcon (env : GlobEnv.t) sigma c = match DAst.get
| None ->
let sigma, s = new_sort_variable univ_flexible_alg sigma in
let sigma, utj_val = new_evar env sigma ~src:(loc, knd) ~naming (mkSort s) in
+ let sigma = mark_obligation_evar sigma knd utj_val in
sigma, { utj_val; utj_type = s})
| _ ->
let sigma, j = pretype k0 resolve_tc empty_tycon env sigma c in
diff --git a/pretyping/recordops.ml b/pretyping/recordops.ml
index f8dc5ba4d6..5d74b59b27 100644
--- a/pretyping/recordops.ml
+++ b/pretyping/recordops.ml
@@ -20,7 +20,6 @@ open Util
open Pp
open Names
open Globnames
-open Nametab
open Constr
open Libobject
open Mod_subst
@@ -330,7 +329,7 @@ let add_canonical_structure x = Lib.add_anonymous_leaf (inCanonStruc x)
let error_not_structure ref description =
user_err ~hdr:"object_declare"
(str"Could not declare a canonical structure " ++
- (Id.print (basename_of_global ref) ++ str"." ++ spc() ++
+ (Id.print (Nametab.basename_of_global ref) ++ str"." ++ spc() ++
description))
let check_and_decompose_canonical_structure ref =
diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml
index 5dbe95a471..aced97e910 100644
--- a/pretyping/reductionops.ml
+++ b/pretyping/reductionops.ml
@@ -398,8 +398,7 @@ struct
match x, y with
| Cst_const (c1,u1), Cst_const (c2, u2) ->
Constant.equal c1 c2 && Univ.Instance.equal u1 u2
- | Cst_proj p1, Cst_proj p2 ->
- Constant.equal (Projection.constant p1) (Projection.constant p2)
+ | Cst_proj p1, Cst_proj p2 -> Projection.repr_equal p1 p2
| _, _ -> false
in
let rec equal_rec sk1 sk2 =
@@ -1252,6 +1251,7 @@ let clos_whd_flags flgs env sigma t =
let nf_beta = clos_norm_flags CClosure.beta
let nf_betaiota = clos_norm_flags CClosure.betaiota
let nf_betaiotazeta = clos_norm_flags CClosure.betaiotazeta
+let nf_zeta = clos_norm_flags CClosure.zeta
let nf_all env sigma =
clos_norm_flags CClosure.all env sigma
diff --git a/pretyping/reductionops.mli b/pretyping/reductionops.mli
index c0ff6723f6..41de779414 100644
--- a/pretyping/reductionops.mli
+++ b/pretyping/reductionops.mli
@@ -171,6 +171,7 @@ val clos_whd_flags : CClosure.RedFlags.reds -> reduction_function
val nf_beta : reduction_function
val nf_betaiota : reduction_function
val nf_betaiotazeta : reduction_function
+val nf_zeta : reduction_function
val nf_all : reduction_function
val nf_evar : evar_map -> constr -> constr
diff --git a/pretyping/retyping.ml b/pretyping/retyping.ml
index 7e43c5e41d..62ad296ecb 100644
--- a/pretyping/retyping.ml
+++ b/pretyping/retyping.ml
@@ -130,7 +130,7 @@ let retype ?(polyprop=true) sigma =
subst1 b (type_of (push_rel (LocalDef (name,b,c1)) env) c2)
| Fix ((_,i),(_,tys,_)) -> tys.(i)
| CoFix (i,(_,tys,_)) -> tys.(i)
- | App(f,args) when is_template_polymorphic env sigma f ->
+ | App(f,args) when Termops.is_template_polymorphic_ind env sigma f ->
let t = type_of_global_reference_knowing_parameters env f args in
strip_outer_cast sigma (subst_type env sigma t (Array.to_list args))
| App(f,args) ->
@@ -156,7 +156,7 @@ let retype ?(polyprop=true) sigma =
let dom = sort_of env t in
let rang = sort_of (push_rel (LocalAssum (name,t)) env) c2 in
Typeops.sort_of_product env dom rang
- | App(f,args) when is_template_polymorphic env sigma f ->
+ | App(f,args) when Termops.is_template_polymorphic_ind env sigma f ->
let t = type_of_global_reference_knowing_parameters env f args in
sort_of_atomic_type env sigma t args
| App(f,args) -> sort_of_atomic_type env sigma (type_of env f) args
@@ -190,14 +190,14 @@ let get_sort_family_of ?(truncation_style=false) ?(polyprop=true) env sigma t =
let s2 = sort_family_of (push_rel (LocalAssum (name,t)) env) c2 in
if not (is_impredicative_set env) &&
s2 == InSet && sort_family_of env t == InType then InType else s2
- | App(f,args) when is_template_polymorphic env sigma f ->
+ | App(f,args) when Termops.is_template_polymorphic_ind env sigma f ->
if truncation_style then InType else
let t = type_of_global_reference_knowing_parameters env f args in
Sorts.family (sort_of_atomic_type env sigma t args)
| App(f,args) ->
Sorts.family (sort_of_atomic_type env sigma (type_of env f) args)
| Lambda _ | Fix _ | Construct _ -> retype_error NotAType
- | Ind _ when truncation_style && is_template_polymorphic env sigma t -> InType
+ | Ind _ when truncation_style && Termops.is_template_polymorphic_ind env sigma t -> InType
| _ ->
Sorts.family (decomp_sort env sigma (type_of env t))
in sort_family_of env t
diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml
index 8911a2f343..4ec8569dd8 100644
--- a/pretyping/tacred.ml
+++ b/pretyping/tacred.ml
@@ -1135,8 +1135,8 @@ let fold_commands cl env sigma c =
let cbv_norm_flags flags env sigma t =
cbv_norm (create_cbv_infos flags env sigma) t
-let cbv_beta = cbv_norm_flags beta empty_env
-let cbv_betaiota = cbv_norm_flags betaiota empty_env
+let cbv_beta = cbv_norm_flags beta
+let cbv_betaiota = cbv_norm_flags betaiota
let cbv_betadeltaiota env sigma = cbv_norm_flags all env sigma
let compute = cbv_betadeltaiota
diff --git a/pretyping/tacred.mli b/pretyping/tacred.mli
index bf38c30a1f..0887d0efd3 100644
--- a/pretyping/tacred.mli
+++ b/pretyping/tacred.mli
@@ -69,8 +69,8 @@ val pattern_occs : (occurrences * constr) list -> e_reduction_function
(** Call by value strategy (uses Closures) *)
val cbv_norm_flags : CClosure.RedFlags.reds -> reduction_function
- val cbv_beta : local_reduction_function
- val cbv_betaiota : local_reduction_function
+ val cbv_beta : reduction_function
+ val cbv_betaiota : reduction_function
val cbv_betadeltaiota : reduction_function
val compute : reduction_function (** = [cbv_betadeltaiota] *)
diff --git a/pretyping/typeclasses.ml b/pretyping/typeclasses.ml
index ce12aaeeb0..4aea2c3db9 100644
--- a/pretyping/typeclasses.ml
+++ b/pretyping/typeclasses.ml
@@ -166,6 +166,21 @@ let rec is_class_type evd c =
let is_class_evar evd evi =
is_class_type evd evi.Evd.evar_concl
+let is_class_constr sigma c =
+ try let gr, u = Termops.global_of_constr sigma c in
+ GlobRef.Map.mem gr !classes
+ with Not_found -> false
+
+let rec is_maybe_class_type evd c =
+ let c, _ = Termops.decompose_app_vect evd c in
+ match EConstr.kind evd c with
+ | Prod (_, _, t) -> is_maybe_class_type evd t
+ | Cast (t, _, _) -> is_maybe_class_type evd t
+ | Evar _ -> true
+ | _ -> is_class_constr evd c
+
+let () = Hook.set Evd.is_maybe_typeclass_hook (fun evd c -> is_maybe_class_type evd (EConstr.of_constr c))
+
(*
* classes persistent object
*)
@@ -279,7 +294,7 @@ let build_subclasses ~check env sigma glob { hint_priority = pri } =
(fun () -> incr i;
Nameops.add_suffix _id ("_subinstance_" ^ string_of_int !i))
in
- let ty, ctx = Global.type_of_global_in_context env glob in
+ let ty, ctx = Typeops.type_of_global_in_context env glob in
let inst, ctx = UnivGen.fresh_instance_from ctx None in
let ty = Vars.subst_instance_constr inst ty in
let ty = EConstr.of_constr ty in
@@ -420,7 +435,7 @@ let remove_instance i =
remove_instance_hint i.is_impl
let declare_instance info local glob =
- let ty, _ = Global.type_of_global_in_context (Global.env ()) glob in
+ let ty, _ = Typeops.type_of_global_in_context (Global.env ()) glob in
let info = Option.default {hint_priority = None; hint_pattern = None} info in
match class_of_constr Evd.empty (EConstr.of_constr ty) with
| Some (rels, ((tc,_), args) as _cl) ->
@@ -481,63 +496,29 @@ let instances r =
let is_class gr =
GlobRef.Map.exists (fun _ v -> GlobRef.equal v.cl_impl gr) !classes
-(* To embed a boolean for resolvability status.
- This is essentially a hack to mark which evars correspond to
- goals and do not need to be resolved when we have nested [resolve_all_evars]
- calls (e.g. when doing apply in an External hint in typeclass_instances).
- Would be solved by having real evars-as-goals.
-
- Nota: we will only check the resolvability status of undefined evars.
- *)
-
-let resolvable = Proofview.Unsafe.typeclass_resolvable
-
-let set_resolvable s b =
- if b then Store.remove s resolvable
- else Store.set s resolvable ()
-
-let is_resolvable evi =
- assert (match evi.evar_body with Evar_empty -> true | _ -> false);
- Option.is_empty (Store.get evi.evar_extra resolvable)
-
-let mark_resolvability_undef b evi =
- if is_resolvable evi == (b : bool) then evi
- else
- let t = set_resolvable evi.evar_extra b in
- { evi with evar_extra = t }
-
-let mark_resolvability b evi =
- assert (match evi.evar_body with Evar_empty -> true | _ -> false);
- mark_resolvability_undef b evi
-
-let mark_unresolvable evi = mark_resolvability false evi
-let mark_resolvable evi = mark_resolvability true evi
-
open Evar_kinds
-type evar_filter = Evar.t -> Evar_kinds.t -> bool
+type evar_filter = Evar.t -> Evar_kinds.t Lazy.t -> bool
+
+let make_unresolvables filter evd =
+ let tcs = Evd.get_typeclass_evars evd in
+ Evd.set_typeclass_evars evd (Evar.Set.filter (fun x -> not (filter x)) tcs)
let all_evars _ _ = true
-let all_goals _ = function VarInstance _ | GoalEvar -> true | _ -> false
+let all_goals _ source =
+ match Lazy.force source with
+ | VarInstance _ | GoalEvar -> true
+ | _ -> false
+
let no_goals ev evi = not (all_goals ev evi)
-let no_goals_or_obligations _ = function
+let no_goals_or_obligations _ source =
+ match Lazy.force source with
| VarInstance _ | GoalEvar | QuestionMark _ -> false
| _ -> true
-let mark_resolvability filter b sigma =
- let map ev evi =
- if filter ev (snd evi.evar_source) then mark_resolvability_undef b evi
- else evi
- in
- Evd.raw_map_undefined map sigma
-
-let mark_unresolvables ?(filter=all_evars) sigma = mark_resolvability filter false sigma
-let mark_resolvables ?(filter=all_evars) sigma = mark_resolvability filter true sigma
-
let has_typeclasses filter evd =
- let check ev evi =
- filter ev (snd evi.evar_source) && is_resolvable evi && is_class_evar evd evi
- in
- Evar.Map.exists check (Evd.undefined_map evd)
+ let tcs = get_typeclass_evars evd in
+ let check ev = filter ev (lazy (snd (Evd.find evd ev).evar_source)) in
+ Evar.Set.exists check tcs
let get_solve_all_instances, solve_all_instances_hook = Hook.make ()
@@ -548,7 +529,7 @@ let solve_all_instances env evd filter unique split fail =
(* let solve_classeskey = CProfile.declare_profile "solve_typeclasses" *)
(* let solve_problem = CProfile.profile5 solve_classeskey solve_problem *)
-let resolve_typeclasses ?(fast_path = true) ?(filter=no_goals) ?(unique=get_typeclasses_unique_solutions ())
+let resolve_typeclasses ?(filter=no_goals) ?(unique=get_typeclasses_unique_solutions ())
?(split=true) ?(fail=true) env evd =
- if fast_path && not (has_typeclasses filter evd) then evd
+ if not (has_typeclasses filter evd) then evd
else solve_all_instances env evd filter unique split fail
diff --git a/pretyping/typeclasses.mli b/pretyping/typeclasses.mli
index f0437be4ed..ee9c83dad3 100644
--- a/pretyping/typeclasses.mli
+++ b/pretyping/typeclasses.mli
@@ -93,7 +93,7 @@ val instance_constructor : typeclass EConstr.puniverses -> EConstr.t list ->
EConstr.t option * EConstr.t
(** Filter which evars to consider for resolution. *)
-type evar_filter = Evar.t -> Evar_kinds.t -> bool
+type evar_filter = Evar.t -> Evar_kinds.t Lazy.t -> bool
val all_evars : evar_filter
val all_goals : evar_filter
val no_goals : evar_filter
@@ -107,16 +107,12 @@ val no_goals_or_obligations : evar_filter
An unresolvable evar is an evar the type-class engine will NOT try to solve
*)
-val set_resolvable : Evd.Store.t -> bool -> Evd.Store.t
-val is_resolvable : evar_info -> bool
-val mark_unresolvable : evar_info -> evar_info
-val mark_unresolvables : ?filter:evar_filter -> evar_map -> evar_map
-val mark_resolvables : ?filter:evar_filter -> evar_map -> evar_map
-val mark_resolvable : evar_info -> evar_info
+val make_unresolvables : (Evar.t -> bool) -> evar_map -> evar_map
+
val is_class_evar : evar_map -> evar_info -> bool
val is_class_type : evar_map -> EConstr.types -> bool
-val resolve_typeclasses : ?fast_path:bool -> ?filter:evar_filter -> ?unique:bool ->
+val resolve_typeclasses : ?filter:evar_filter -> ?unique:bool ->
?split:bool -> ?fail:bool -> env -> evar_map -> evar_map
val resolve_one_typeclass : ?unique:bool -> env -> evar_map -> EConstr.types -> evar_map * EConstr.constr
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-29 10:06:09 +0000