aboutsummaryrefslogtreecommitdiff
path: root/pretyping
diff options
context:
space:
mode:
Diffstat (limited to 'pretyping')
-rw-r--r--pretyping/cases.ml19
-rw-r--r--pretyping/cbv.ml68
-rw-r--r--pretyping/classops.ml13
-rw-r--r--pretyping/detyping.ml6
-rw-r--r--pretyping/evarconv.ml13
-rw-r--r--pretyping/evarconv.mli2
-rw-r--r--pretyping/evarsolve.ml44
-rw-r--r--pretyping/indrec.ml3
-rw-r--r--pretyping/inferCumulativity.ml2
-rw-r--r--pretyping/nativenorm.ml12
-rw-r--r--pretyping/pretyping.ml42
-rw-r--r--pretyping/recordops.ml14
-rw-r--r--pretyping/reductionops.ml3
-rw-r--r--pretyping/typeclasses.ml89
-rw-r--r--pretyping/typeclasses.mli12
-rw-r--r--pretyping/unification.ml4
16 files changed, 169 insertions, 177 deletions
diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index 9fa8442f8a..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) ->
@@ -994,8 +993,8 @@ let expand_arg tms (p,ccl) ((_,t),_,na) =
let k = length_of_tomatch_type_sign na t in
(p+k,liftn_predicate (k-1) (p+1) ccl tms)
-let use_unit_judge evd =
- let j, ctx = coq_unit_judge () in
+let use_unit_judge env evd =
+ let j, ctx = coq_unit_judge !!env in
let evd' = Evd.merge_context_set Evd.univ_flexible_alg evd ctx in
evd', j
@@ -1024,7 +1023,7 @@ let adjust_impossible_cases sigma pb pred tomatch submat =
| Evar (evk,_) when snd (evar_source evk sigma) == Evar_kinds.ImpossibleCase ->
let sigma =
if not (Evd.is_defined sigma evk) then
- let sigma, default = use_unit_judge sigma in
+ let sigma, default = use_unit_judge pb.env sigma in
let sigma = Evd.define evk default.uj_type sigma in
sigma
else sigma
@@ -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
@@ -2512,7 +2511,7 @@ let compile_program_cases ?loc style (typing_function, sigma) tycon env
(predopt, tomatchl, eqns) =
let typing_fun tycon env sigma = function
| Some t -> typing_function tycon env sigma t
- | None -> use_unit_judge sigma in
+ | None -> use_unit_judge env sigma in
(* We build the matrix of patterns and right-hand side *)
let matx = matx_of_eqns env eqns in
@@ -2593,7 +2592,7 @@ let compile_program_cases ?loc style (typing_function, sigma) tycon env
let typing_function tycon env sigma = function
| Some t -> typing_function tycon env sigma t
- | None -> use_unit_judge sigma in
+ | None -> use_unit_judge env sigma in
let pb =
{ env = env;
@@ -2668,7 +2667,7 @@ let compile_cases ?loc style (typing_fun, sigma) tycon env (predopt, tomatchl, e
(* A typing function that provides with a canonical term for absurd cases*)
let typing_fun tycon env sigma = function
| Some t -> typing_fun tycon env sigma t
- | None -> use_unit_judge sigma in
+ | None -> use_unit_judge env sigma in
let pb =
{ env = env;
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/detyping.ml b/pretyping/detyping.ml
index 0dc5a9bad5..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)
@@ -647,6 +646,7 @@ and detype_r d flags avoid env sigma t =
else
GEvar (Id.of_string_soft ("M" ^ string_of_int n), [])
| Var id ->
+ (* Discriminate between section variable and non-section variable *)
(try let _ = Global.lookup_named id in GRef (VarRef id, None)
with Not_found -> GVar id)
| Sort s -> GSort (detype_sort sigma (ESorts.kind sigma s))
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index 72d95f7eb1..6a75be352b 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -46,14 +46,14 @@ let _ = Goptions.declare_bool_option {
(*******************************************)
(* Functions to deal with impossible cases *)
(*******************************************)
-let impossible_default_case () =
+let impossible_default_case env =
let type_of_id =
let open Names.GlobRef in
match Coqlib.lib_ref "core.IDProp.type" with
| ConstRef c -> c
| VarRef _ | IndRef _ | ConstructRef _ -> assert false
in
- let c, ctx = UnivGen.fresh_global_instance (Global.env()) (Coqlib.(lib_ref "core.IDProp.idProp")) in
+ let c, ctx = UnivGen.fresh_global_instance env (Coqlib.(lib_ref "core.IDProp.idProp")) in
let (_, u) = Constr.destConst c in
Some (c, Constr.mkConstU (type_of_id, u), ctx)
@@ -62,8 +62,8 @@ let coq_unit_judge =
let make_judge c t = make_judge (EConstr.of_constr c) (EConstr.of_constr t) in
let na1 = Name (Id.of_string "A") in
let na2 = Name (Id.of_string "H") in
- fun () ->
- match impossible_default_case () with
+ fun env ->
+ match impossible_default_case env with
| Some (id, type_of_id, ctx) ->
make_judge id type_of_id, ctx
| None ->
@@ -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');
@@ -1352,7 +1351,7 @@ let solve_unconstrained_impossible_cases env evd =
Evd.fold_undefined (fun evk ev_info evd' ->
match ev_info.evar_source with
| loc,Evar_kinds.ImpossibleCase ->
- let j, ctx = coq_unit_judge () in
+ let j, ctx = coq_unit_judge env in
let evd' = Evd.merge_context_set Evd.univ_flexible_alg ?loc evd' ctx in
let ty = j_type j in
let conv_algo = evar_conv_x full_transparent_state in
diff --git a/pretyping/evarconv.mli b/pretyping/evarconv.mli
index 20a4f34ec7..350dece28a 100644
--- a/pretyping/evarconv.mli
+++ b/pretyping/evarconv.mli
@@ -80,4 +80,4 @@ val evar_eqappr_x : ?rhs_is_already_stuck:bool -> transparent_state * bool ->
(**/**)
(** {6 Functions to deal with impossible cases } *)
-val coq_unit_judge : unit -> EConstr.unsafe_judgment Univ.in_universe_context_set
+val coq_unit_judge : env -> EConstr.unsafe_judgment Univ.in_universe_context_set
diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml
index 6f5cba3e03..674f6846ae 100644
--- a/pretyping/evarsolve.ml
+++ b/pretyping/evarsolve.ml
@@ -425,7 +425,7 @@ let rec expand_vars_in_term_using sigma aliases t = match EConstr.kind sigma t w
let expand_vars_in_term env sigma = expand_vars_in_term_using sigma (make_alias_map env sigma)
-let free_vars_and_rels_up_alias_expansion sigma aliases c =
+let free_vars_and_rels_up_alias_expansion env sigma aliases c =
let acc1 = ref Int.Set.empty and acc2 = ref Id.Set.empty in
let acc3 = ref Int.Set.empty and acc4 = ref Id.Set.empty in
let cache_rel = ref Int.Set.empty and cache_var = ref Id.Set.empty in
@@ -457,7 +457,7 @@ let free_vars_and_rels_up_alias_expansion sigma aliases c =
| Rel n -> if n >= depth+1 then acc1 := Int.Set.add (n-depth) !acc1
| _ -> frec (aliases,depth) c end
| Const _ | Ind _ | Construct _ ->
- acc2 := Id.Set.union (vars_of_global (Global.env()) (EConstr.to_constr sigma c)) !acc2
+ acc2 := Id.Set.union (vars_of_global env (fst @@ EConstr.destRef sigma c)) !acc2
| _ ->
iter_with_full_binders sigma
(fun d (aliases,depth) -> (extend_alias sigma d aliases,depth+1))
@@ -488,13 +488,13 @@ let alias_distinct l =
in
check (Int.Set.empty, Id.Set.empty) l
-let get_actual_deps evd aliases l t =
+let get_actual_deps env evd aliases l t =
if occur_meta_or_existential evd t then
(* Probably no restrictions on allowed vars in presence of evars *)
l
else
(* Probably strong restrictions coming from t being evar-closed *)
- let (fv_rels,fv_ids,_,_) = free_vars_and_rels_up_alias_expansion evd aliases t in
+ let (fv_rels,fv_ids,_,_) = free_vars_and_rels_up_alias_expansion env evd aliases t in
List.filter (function
| VarAlias id -> Id.Set.mem id fv_ids
| RelAlias n -> Int.Set.mem n fv_rels
@@ -520,7 +520,7 @@ let remove_instance_local_defs evd evk args =
let find_unification_pattern_args env evd l t =
let aliases = make_alias_map env evd in
match expand_and_check_vars evd aliases l with
- | Some l as x when alias_distinct (get_actual_deps evd aliases l t) -> x
+ | Some l as x when alias_distinct (get_actual_deps env evd aliases l t) -> x
| _ -> None
let is_unification_pattern_meta env evd nb m l t =
@@ -1202,7 +1202,7 @@ exception EvarSolvedOnTheFly of evar_map * EConstr.constr
the common domain of definition *)
let project_evar_on_evar force g env evd aliases k2 pbty (evk1,argsv1 as ev1) (evk2,argsv2 as ev2) =
(* Apply filtering on ev1 so that fvs(ev1) are in fvs(ev2). *)
- let fvs2 = free_vars_and_rels_up_alias_expansion evd aliases (mkEvar ev2) in
+ let fvs2 = free_vars_and_rels_up_alias_expansion env evd aliases (mkEvar ev2) in
let filter1 = restrict_upon_filter evd evk1
(has_constrainable_free_vars env evd aliases force k2 evk2 fvs2)
argsv1 in
@@ -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 update_evar_info ev1 ev2 evd =
+ (* We update the source of obligation evars during evar-evar unifications. *)
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 evi = Evd.find evd ev1 in
+ Evd.add evd ev1 {evi with evar_source = loc, evs2}
+
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/nativenorm.ml b/pretyping/nativenorm.ml
index 20185363e6..022c383f60 100644
--- a/pretyping/nativenorm.ml
+++ b/pretyping/nativenorm.ml
@@ -132,15 +132,15 @@ let construct_of_constr_notnative const env tag (mind, _ as ind) u allargs =
(mkApp(mkConstructU((ind,i),u), params), ctyp)
-let construct_of_constr const env tag typ =
+let construct_of_constr const env sigma tag typ =
let t, l = app_type env typ in
- match kind t with
+ match EConstr.kind_upto sigma t with
| Ind (ind,u) ->
construct_of_constr_notnative const env tag ind u l
| _ -> assert false
-let construct_of_constr_const env tag typ =
- fst (construct_of_constr true env tag typ)
+let construct_of_constr_const env sigma tag typ =
+ fst (construct_of_constr true env sigma tag typ)
let construct_of_constr_block = construct_of_constr false
@@ -207,9 +207,9 @@ let rec nf_val env sigma v typ =
let env = push_rel (LocalAssum (name,dom)) env in
let body = nf_val env sigma (f (mk_rel_accu lvl)) codom in
mkLambda(name,dom,body)
- | Vconst n -> construct_of_constr_const env n typ
+ | Vconst n -> construct_of_constr_const env sigma n typ
| Vblock b ->
- let capp,ctyp = construct_of_constr_block env (block_tag b) typ in
+ let capp,ctyp = construct_of_constr_block env sigma (block_tag b) typ in
let args = nf_bargs env sigma b ctyp in
mkApp(capp,args)
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index 495f5c0660..37afcf75e1 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -405,32 +405,25 @@ let interp_glob_level ?loc evd : glob_level -> _ = function
| GSet -> evd, Univ.Level.set
| GType s -> interp_level_info ?loc evd s
-let interp_instance ?loc evd ~len l =
- if len != List.length l then
+let interp_instance ?loc evd l =
+ let evd, l' =
+ List.fold_left
+ (fun (evd, univs) l ->
+ let evd, l = interp_glob_level ?loc evd l in
+ (evd, l :: univs)) (evd, [])
+ l
+ in
+ if List.exists (fun l -> Univ.Level.is_prop l) l' then
user_err ?loc ~hdr:"pretype"
- (str "Universe instance should have length " ++ int len)
- else
- let evd, l' =
- List.fold_left
- (fun (evd, univs) l ->
- let evd, l = interp_glob_level ?loc evd l in
- (evd, l :: univs)) (evd, [])
- l
- in
- if List.exists (fun l -> Univ.Level.is_prop l) l' then
- user_err ?loc ~hdr:"pretype"
- (str "Universe instances cannot contain Prop, polymorphic" ++
- str " universe instances must be greater or equal to Set.");
- evd, Some (Univ.Instance.of_array (Array.of_list (List.rev l')))
+ (str "Universe instances cannot contain Prop, polymorphic" ++
+ str " universe instances must be greater or equal to Set.");
+ evd, Some (Univ.Instance.of_array (Array.of_list (List.rev l')))
let pretype_global ?loc rigid env evd gr us =
let evd, instance =
match us with
| None -> evd, None
- | Some l ->
- let _, ctx = Global.constr_of_global_in_context !!env gr in
- let len = Univ.AUContext.size ctx in
- interp_instance ?loc evd ~len l
+ | Some l -> interp_instance ?loc evd l
in
Evd.fresh_global ?loc ~rigid ?names:instance !!env evd gr
@@ -517,6 +510,15 @@ 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 =
+ if Flags.is_program_mode () then
+ match k with
+ | Evar_kinds.QuestionMark _
+ | Evar_kinds.ImplicitArg (_, _, false) ->
+ Evd.set_obligation_evar sigma (fst (destEvar sigma uj_val))
+ | _ -> sigma
+ else sigma
+ in
sigma, { uj_val; uj_type = ty }
| GHole (k, _naming, Some arg) ->
diff --git a/pretyping/recordops.ml b/pretyping/recordops.ml
index 3719f9302a..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
@@ -230,8 +229,7 @@ let warn_projection_no_head_constant =
++ con_pp ++ str " of " ++ proji_sp_pp ++ strbrk ", ignoring it.")
(* Intended to always succeed *)
-let compute_canonical_projections warn (con,ind) =
- let env = Global.env () in
+let compute_canonical_projections env warn (con,ind) =
let ctx = Environ.constant_context env con in
let u = Univ.make_abstract_instance ctx in
let v = (mkConstU (con,u)) in
@@ -282,7 +280,10 @@ let warn_redundant_canonical_projection =
++ new_can_s ++ strbrk ": redundant with " ++ old_can_s)
let add_canonical_structure warn o =
- let lo = compute_canonical_projections warn o in
+ (* XXX: Undesired global access to env *)
+ let env = Global.env () in
+ let sigma = Evd.from_env env in
+ let lo = compute_canonical_projections env warn o in
List.iter (fun ((proj,(cs_pat,_ as pat)),s) ->
let l = try GlobRef.Map.find proj !object_table with Not_found -> [] in
let ocs = try Some (assoc_pat cs_pat l)
@@ -290,9 +291,6 @@ let add_canonical_structure warn o =
in match ocs with
| None -> object_table := GlobRef.Map.add proj ((pat,s)::l) !object_table;
| Some (c, cs) ->
- (* XXX: Undesired global access to env *)
- let env = Global.env () in
- let sigma = Evd.from_env env in
let old_can_s = (Termops.Internal.print_constr_env env sigma (EConstr.of_constr cs.o_DEF))
and new_can_s = (Termops.Internal.print_constr_env env sigma (EConstr.of_constr s.o_DEF))
in
@@ -331,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..367a48cb5e 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 =
diff --git a/pretyping/typeclasses.ml b/pretyping/typeclasses.ml
index 7e5815acd1..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
@@ -320,7 +335,7 @@ let build_subclasses ~check env sigma glob { hint_priority = pri } =
hints @ (path', info, body) :: rest
in List.fold_left declare_proj [] projs
in
- let term = UnivGen.constr_of_global_univ (glob, inst) in
+ let term = Constr.mkRef (glob, inst) in
(*FIXME subclasses should now get substituted for each particular instance of
the polymorphic superclass *)
aux pri term ty [glob]
@@ -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
diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index 4665486fc0..e3b942b610 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -1417,7 +1417,7 @@ let w_merge env with_types flags (evd,metas,evars : subst0) =
and mimick_undefined_evar evd flags hdc nargs sp =
let ev = Evd.find_undefined evd sp in
- let sp_env = Global.env_of_context (evar_filtered_hyps ev) in
+ let sp_env = reset_with_named_context (evar_filtered_hyps ev) env in
let (evd', c) = applyHead sp_env evd nargs hdc in
let (evd'',mc,ec) =
unify_0 sp_env evd' CUMUL flags
@@ -1633,7 +1633,7 @@ let make_eq_test env evd c =
let make_abstraction_core name (test,out) env sigma c ty occs check_occs concl =
let id =
let t = match ty with Some t -> t | None -> get_type_of env sigma c in
- let x = id_of_name_using_hdchar (Global.env()) sigma t name in
+ let x = id_of_name_using_hdchar env sigma t name in
let ids = Environ.ids_of_named_context_val (named_context_val env) in
if name == Anonymous then next_ident_away_in_goal x ids else
if mem_named_context_val x (named_context_val env) then
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-05 01:37:52 +0000