aboutsummaryrefslogtreecommitdiff
path: root/pretyping
diff options
context:
space:
mode:
Diffstat (limited to 'pretyping')
-rw-r--r--pretyping/cases.ml12
-rw-r--r--pretyping/detyping.ml1
-rw-r--r--pretyping/evarconv.ml20
-rw-r--r--pretyping/evarconv.mli2
-rw-r--r--pretyping/evarsolve.ml61
-rw-r--r--pretyping/program.ml54
-rw-r--r--pretyping/recordops.ml11
-rw-r--r--pretyping/unification.ml4
8 files changed, 89 insertions, 76 deletions
diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index 9fa8442f8a..54e847988b 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -994,8 +994,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 +1024,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
@@ -2512,7 +2512,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 +2593,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 +2668,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/detyping.ml b/pretyping/detyping.ml
index 0dc5a9bad5..592057ab41 100644
--- a/pretyping/detyping.ml
+++ b/pretyping/detyping.ml
@@ -647,6 +647,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 bae13dbba1..f0ff1aa93b 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -46,20 +46,24 @@ let _ = Goptions.declare_bool_option {
(*******************************************)
(* Functions to deal with impossible cases *)
(*******************************************)
-(* XXX: we would like to search for this with late binding
- "data.id.type" etc... *)
-let impossible_default_case () =
- let c, ctx = UnivGen.fresh_global_instance (Global.env()) (Globnames.ConstRef Coqlib.id) in
+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 env (Coqlib.(lib_ref "core.IDProp.idProp")) in
let (_, u) = Constr.destConst c in
- Some (c, Constr.mkConstU (Coqlib.type_of_id, u), ctx)
+ Some (c, Constr.mkConstU (type_of_id, u), ctx)
let coq_unit_judge =
let open Environ in
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 ->
@@ -1348,7 +1352,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 44bfe4b6cc..62d719034c 100644
--- a/pretyping/evarsolve.ml
+++ b/pretyping/evarsolve.ml
@@ -42,7 +42,6 @@ let get_polymorphic_positions sigma f =
let refresh_universes ?(status=univ_rigid) ?(onlyalg=false) ?(refreshset=false)
pbty env evd t =
let evdref = ref evd in
- let modified = ref false in
(* direction: true for fresh universes lower than the existing ones *)
let refresh_sort status ~direction s =
let s = ESorts.kind !evdref s in
@@ -51,18 +50,18 @@ let refresh_universes ?(status=univ_rigid) ?(onlyalg=false) ?(refreshset=false)
let evd =
if direction then set_leq_sort env !evdref s' s
else set_leq_sort env !evdref s s'
- in
- modified := true; evdref := evd; mkSort s'
+ in evdref := evd; mkSort s'
in
let rec refresh ~onlyalg status ~direction t =
match EConstr.kind !evdref t with
| Sort s ->
begin match ESorts.kind !evdref s with
| Type u ->
- (match Univ.universe_level u with
+ (* TODO: check if max(l,u) is not ok as well *)
+ (match Univ.universe_level u with
| None -> refresh_sort status ~direction s
| Some l ->
- (match Evd.universe_rigidity evd l with
+ (match Evd.universe_rigidity !evdref l with
| UnivRigid ->
if not onlyalg then refresh_sort status ~direction s
else t
@@ -76,34 +75,43 @@ let refresh_universes ?(status=univ_rigid) ?(onlyalg=false) ?(refreshset=false)
refresh_sort status ~direction s
| _ -> t
end
- | Prod (na,u,v) ->
- mkProd (na, u, refresh ~onlyalg status ~direction v)
+ | Prod (na,u,v) ->
+ let v' = refresh ~onlyalg status ~direction v in
+ if v' == v then t else mkProd (na, u, v')
| _ -> t
+ in
(** Refresh the types of evars under template polymorphic references *)
- and refresh_term_evars onevars top t =
+ let rec refresh_term_evars ~onevars ~top t =
match EConstr.kind !evdref t with
| App (f, args) when is_template_polymorphic env !evdref f ->
let pos = get_polymorphic_positions !evdref f in
- refresh_polymorphic_positions args pos
+ refresh_polymorphic_positions args pos; t
| App (f, args) when top && isEvar !evdref f ->
- refresh_term_evars true false f;
- Array.iter (refresh_term_evars onevars false) args
+ let f' = refresh_term_evars ~onevars:true ~top:false f in
+ let args' = Array.map (refresh_term_evars ~onevars ~top:false) args in
+ if f' == f && args' == args then t
+ else mkApp (f', args')
| Evar (ev, a) when onevars ->
let evi = Evd.find !evdref ev in
- let ty' = refresh ~onlyalg univ_flexible ~direction:true evi.evar_concl in
- if !modified then
- evdref := Evd.add !evdref ev {evi with evar_concl = ty'}
- else ()
- | _ -> EConstr.iter !evdref (refresh_term_evars onevars false) t
+ let ty = evi.evar_concl in
+ let ty' = refresh ~onlyalg univ_flexible ~direction:true ty in
+ if ty == ty' then t
+ else (evdref := Evd.downcast ev ty' !evdref; t)
+ | Sort s ->
+ (match ESorts.kind !evdref s with
+ | Type u when not (Univ.Universe.is_levels u) ->
+ refresh_sort Evd.univ_flexible ~direction:false s
+ | _ -> t)
+ | _ -> EConstr.map !evdref (refresh_term_evars ~onevars ~top:false) t
and refresh_polymorphic_positions args pos =
let rec aux i = function
| Some l :: ls ->
if i < Array.length args then
- ignore(refresh_term_evars true false args.(i));
+ ignore(refresh_term_evars ~onevars:true ~top:false args.(i));
aux (succ i) ls
| None :: ls ->
if i < Array.length args then
- ignore(refresh_term_evars false false args.(i));
+ ignore(refresh_term_evars ~onevars:false ~top:false args.(i));
aux (succ i) ls
| [] -> ()
in aux 0 pos
@@ -115,9 +123,8 @@ let refresh_universes ?(status=univ_rigid) ?(onlyalg=false) ?(refreshset=false)
(* No cumulativity needed, but we still need to refresh the algebraics *)
refresh ~onlyalg:true univ_flexible ~direction:false t
| Some direction -> refresh ~onlyalg status ~direction t
- else (refresh_term_evars false true t; t)
- in
- if !modified then !evdref, t' else !evdref, t
+ else refresh_term_evars ~onevars:false ~top:true t
+ in !evdref, t'
let get_type_of_refresh ?(polyprop=true) ?(lax=false) env sigma c =
let ty = Retyping.get_type_of ~polyprop ~lax env sigma c in
@@ -418,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
@@ -450,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 (EConstr.to_constr sigma c)) !acc2
| _ ->
iter_with_full_binders sigma
(fun d (aliases,depth) -> (extend_alias sigma d aliases,depth+1))
@@ -481,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
@@ -513,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 =
@@ -1195,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
diff --git a/pretyping/program.ml b/pretyping/program.ml
index 8cfb7966cb..bbabbefdc3 100644
--- a/pretyping/program.ml
+++ b/pretyping/program.ml
@@ -11,8 +11,6 @@
open CErrors
open Util
-let init_reference dir s () = Coqlib.coq_reference "Program" dir s
-
let papp evdref r args =
let open EConstr in
let gr = delayed_force r in
@@ -20,44 +18,48 @@ let papp evdref r args =
evdref := evd;
mkApp (hd, args)
-let sig_typ = init_reference ["Init"; "Specif"] "sig"
-let sig_intro = init_reference ["Init"; "Specif"] "exist"
-let sig_proj1 = init_reference ["Init"; "Specif"] "proj1_sig"
-
-let sigT_typ = init_reference ["Init"; "Specif"] "sigT"
-let sigT_intro = init_reference ["Init"; "Specif"] "existT"
-let sigT_proj1 = init_reference ["Init"; "Specif"] "projT1"
-let sigT_proj2 = init_reference ["Init"; "Specif"] "projT2"
-
-let prod_typ = init_reference ["Init"; "Datatypes"] "prod"
-let prod_intro = init_reference ["Init"; "Datatypes"] "pair"
-let prod_proj1 = init_reference ["Init"; "Datatypes"] "fst"
-let prod_proj2 = init_reference ["Init"; "Datatypes"] "snd"
+let sig_typ () = Coqlib.lib_ref "core.sig.type"
+let sig_intro () = Coqlib.lib_ref "core.sig.intro"
+let sig_proj1 () = Coqlib.lib_ref "core.sig.proj1"
+(* let sig_proj2 () = Coqlib.lib_ref "core.sig.proj2" *)
-let coq_eq_ind = init_reference ["Init"; "Logic"] "eq"
-let coq_eq_refl = init_reference ["Init"; "Logic"] "eq_refl"
-let coq_eq_refl_ref = init_reference ["Init"; "Logic"] "eq_refl"
-let coq_eq_rect = init_reference ["Init"; "Logic"] "eq_rect"
+let sigT_typ () = Coqlib.lib_ref "core.sigT.type"
+let sigT_intro () = Coqlib.lib_ref "core.sigT.intro"
+let sigT_proj1 () = Coqlib.lib_ref "core.sigT.proj1"
+let sigT_proj2 () = Coqlib.lib_ref "core.sigT.proj2"
-let coq_JMeq_ind = init_reference ["Logic";"JMeq"] "JMeq"
-let coq_JMeq_refl = init_reference ["Logic";"JMeq"] "JMeq_refl"
+let prod_typ () = Coqlib.lib_ref "core.prod.type"
+let prod_intro () = Coqlib.lib_ref "core.prod.intro"
+let prod_proj1 () = Coqlib.lib_ref "core.prod.proj1"
+let prod_proj2 () = Coqlib.lib_ref "core.prod.proj2"
-let coq_not = init_reference ["Init";"Logic"] "not"
-let coq_and = init_reference ["Init";"Logic"] "and"
+let coq_eq_ind () = Coqlib.lib_ref "core.eq.type"
+let coq_eq_refl () = Coqlib.lib_ref "core.eq.refl"
+let coq_eq_refl_ref () = Coqlib.lib_ref "core.eq.refl"
+let coq_eq_rect () = Coqlib.lib_ref "core.eq.rect"
let mk_coq_not sigma x =
- let sigma, notc = Evarutil.new_global sigma (coq_not ()) in
+ let sigma, notc = Evarutil.new_global sigma Coqlib.(lib_ref "core.not.type") in
sigma, EConstr.mkApp (notc, [| x |])
+let coq_JMeq_ind () =
+ try Coqlib.lib_ref "core.JMeq.type"
+ with Not_found ->
+ user_err (Pp.str "cannot find Coq.Logic.JMeq.JMeq; maybe library Coq.Logic.JMeq has to be required first.")
+let coq_JMeq_refl () = Coqlib.lib_ref "core.JMeq.refl"
+
+(* let coq_not () = Universes.constr_of_global @@ Coqlib.lib_ref "core.not.type" *)
+(* let coq_and () = Universes.constr_of_global @@ Coqlib.lib_ref "core.and.type" *)
+
let unsafe_fold_right f = function
hd :: tl -> List.fold_right f tl hd
| [] -> invalid_arg "unsafe_fold_right"
let mk_coq_and sigma l =
- let sigma, and_typ = Evarutil.new_global sigma (coq_and ()) in
+ let sigma, and_typ = Evarutil.new_global sigma Coqlib.(lib_ref "core.and.type") in
sigma, unsafe_fold_right
(fun c conj ->
- EConstr.mkApp (and_typ, [| c ; conj |]))
+ EConstr.(mkApp (and_typ, [| c ; conj |])))
l
(* true = transparent by default, false = opaque if possible *)
diff --git a/pretyping/recordops.ml b/pretyping/recordops.ml
index 3719f9302a..f8dc5ba4d6 100644
--- a/pretyping/recordops.ml
+++ b/pretyping/recordops.ml
@@ -230,8 +230,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 +281,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 +292,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
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-03-10 16:21:26 +0000