aboutsummaryrefslogtreecommitdiff
path: root/pretyping
diff options
context:
space:
mode:
Diffstat (limited to 'pretyping')
-rw-r--r--pretyping/detyping.ml17
-rw-r--r--pretyping/evarconv.ml42
-rw-r--r--pretyping/evardefine.ml24
-rw-r--r--pretyping/evardefine.mli8
-rw-r--r--pretyping/glob_ops.ml4
-rw-r--r--pretyping/glob_term.ml2
-rw-r--r--pretyping/pretype_errors.ml2
-rw-r--r--pretyping/pretype_errors.mli4
-rw-r--r--pretyping/pretyping.ml53
-rw-r--r--pretyping/pretyping.mli2
-rw-r--r--pretyping/reductionops.ml14
-rw-r--r--pretyping/typeclasses.ml6
-rw-r--r--pretyping/typeclasses.mli6
-rw-r--r--pretyping/typing.ml25
-rw-r--r--pretyping/unification.ml4
-rw-r--r--pretyping/vnorm.ml3
16 files changed, 116 insertions, 100 deletions
diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml
index 7fcb0795bd..a12a832f76 100644
--- a/pretyping/detyping.ml
+++ b/pretyping/detyping.ml
@@ -715,9 +715,9 @@ and detype_r d flags avoid env sigma t =
(* Meta in constr are not user-parsable and are mapped to Evar *)
if n = Constr_matching.special_meta then
(* Using a dash to be unparsable *)
- GEvar (Id.of_string_soft "CONTEXT-HOLE", [])
+ GEvar (CAst.make @@ Id.of_string_soft "CONTEXT-HOLE", [])
else
- GEvar (Id.of_string_soft ("M" ^ string_of_int n), [])
+ GEvar (CAst.make @@ 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 (GlobRef.VarRef id, None)
@@ -788,12 +788,12 @@ and detype_r d flags avoid env sigma t =
let l = Evd.evar_instance_array bound_to_itself_or_letin (Evd.find sigma evk) cl in
let fvs,rels = List.fold_left (fun (fvs,rels) (_,c) -> match EConstr.kind sigma c with Rel n -> (fvs,Int.Set.add n rels) | Var id -> (Id.Set.add id fvs,rels) | _ -> (fvs,rels)) (Id.Set.empty,Int.Set.empty) l in
let l = Evd.evar_instance_array (fun d c -> not !print_evar_arguments && (bound_to_itself_or_letin d c && not (isRel sigma c && Int.Set.mem (destRel sigma c) rels || isVar sigma c && (Id.Set.mem (destVar sigma c) fvs)))) (Evd.find sigma evk) cl in
- id,l
+ id,List.map (fun (id,c) -> (CAst.make id,c)) l
with Not_found ->
Id.of_string ("X" ^ string_of_int (Evar.repr evk)),
- (List.map (fun c -> (Id.of_string "__",c)) cl)
+ (List.map (fun c -> (CAst.make @@ Id.of_string "__",c)) cl)
in
- GEvar (id,
+ GEvar (CAst.make id,
List.map (on_snd (detype d flags avoid env sigma)) l)
| Ind (ind_sp,u) ->
GRef (GlobRef.IndRef ind_sp, detype_instance sigma u)
@@ -883,7 +883,12 @@ and detype_binder d flags bk avoid env sigma decl c =
| BLetIn ->
let c = detype d { flags with flg_isgoal = false } avoid env sigma (Option.get body) in
(* Heuristic: we display the type if in Prop *)
- let s = try Retyping.get_sort_family_of (snd env) sigma ty with _ when !Flags.in_debugger || !Flags.in_toplevel -> InType (* Can fail because of sigma missing in debugger *) in
+ let s =
+ (* It can fail if ty is an evar, or if run inside ocamldebug or the
+ OCaml toplevel since their printers don't have access to the proper sigma/env *)
+ try Retyping.get_sort_family_of (snd env) sigma ty
+ with Retyping.RetypeError _ -> InType
+ in
let t = if s != InProp && not !Flags.raw_print then None else Some (detype d { flags with flg_isgoal = false } avoid env sigma ty) in
GLetIn (na', c, t, r)
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index 61453ff214..a5311e162d 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -1213,12 +1213,22 @@ let default_occurrences_selection ?(allowed_evars=AllowedEvars.all) ts n =
(default_occurrence_test ~allowed_evars ts,
List.init n (fun _ -> default_occurrence_selection))
-let apply_on_subterm env evd fixedref f test c t =
+let occur_evars sigma evs c =
+ if Evar.Set.is_empty evs then false
+ else
+ let rec occur_rec c = match EConstr.kind sigma c with
+ | Evar (sp,_) when Evar.Set.mem sp evs -> raise Occur
+ | _ -> EConstr.iter sigma occur_rec c
+ in
+ try occur_rec c; false with Occur -> true
+
+let apply_on_subterm env evd fixed f test c t =
let test = test env evd c in
let prc env evd = Termops.Internal.print_constr_env env evd in
let evdref = ref evd in
+ let fixedref = ref fixed in
let rec applyrec (env,(k,c) as acc) t =
- if Evar.Set.exists (fun fixed -> occur_evar !evdref fixed t) !fixedref then
+ if occur_evars !evdref !fixedref t then
match EConstr.kind !evdref t with
| Evar (ev, args) when Evar.Set.mem ev !fixedref -> t
| _ -> map_constr_with_binders_left_to_right !evdref
@@ -1231,7 +1241,8 @@ let apply_on_subterm env evd fixedref f test c t =
try test env !evdref k c t
with e when CErrors.noncritical e -> assert false in
if b then (if debug_ho_unification () then Feedback.msg_debug (Pp.str "succeeded");
- let evd', t' = f !evdref k t in
+ let evd', fixed, t' = f !evdref !fixedref k t in
+ fixedref := fixed;
evdref := evd'; t')
else (
if debug_ho_unification () then Feedback.msg_debug (Pp.str "failed");
@@ -1240,7 +1251,7 @@ let apply_on_subterm env evd fixedref f test c t =
applyrec acc t))
in
let t' = applyrec (env,(0,c)) t in
- !evdref, t'
+ !evdref, !fixedref, t'
let filter_possible_projections evd c ty ctxt args =
(* Since args in the types will be replaced by holes, we count the
@@ -1377,8 +1388,7 @@ let second_order_matching flags env_rhs evd (evk,args) (test,argoccs) rhs =
| _, _, [] -> []
| _ -> anomaly (Pp.str "Signature or instance are shorter than the occurrences list.")
in
- let fixed = ref Evar.Set.empty in
- let rec set_holes env_rhs evd rhs = function
+ let rec set_holes env_rhs evd fixed rhs = function
| (id,idty,c,cty,evsref,filter,occs)::subst ->
let c = nf_evar evd c in
if debug_ho_unification () then
@@ -1387,7 +1397,7 @@ let second_order_matching flags env_rhs evd (evk,args) (test,argoccs) rhs =
prc env_rhs evd c ++ str" in " ++
prc env_rhs evd rhs);
let occ = ref 1 in
- let set_var evd k inst =
+ let set_var evd fixed k inst =
let oc = !occ in
if debug_ho_unification () then
(Feedback.msg_debug Pp.(str"Found one occurrence");
@@ -1395,10 +1405,10 @@ let second_order_matching flags env_rhs evd (evk,args) (test,argoccs) rhs =
incr occ;
match occs with
| AtOccurrences occs ->
- if Locusops.is_selected oc occs then evd, mkVar id.binder_name
- else evd, inst
+ if Locusops.is_selected oc occs then evd, fixed, mkVar id.binder_name
+ else evd, fixed, inst
| Unspecified prefer_abstraction ->
- let evd, evty = set_holes env_rhs evd cty subst in
+ let evd, fixed, evty = set_holes env_rhs evd fixed cty subst in
let evty = nf_evar evd evty in
if debug_ho_unification () then
Feedback.msg_debug Pp.(str"abstracting one occurrence " ++ prc env_rhs evd inst ++
@@ -1414,21 +1424,21 @@ let second_order_matching flags env_rhs evd (evk,args) (test,argoccs) rhs =
env_evar_unf evd evty
else evd, evty in
let (evd, evk) = new_pure_evar sign evd evty ~filter in
+ let fixed = Evar.Set.add evk fixed in
evsref := (evk,evty,inst,prefer_abstraction)::!evsref;
- fixed := Evar.Set.add evk !fixed;
- evd, mkEvar (evk, instance)
+ evd, fixed, mkEvar (evk, instance)
in
- let evd, rhs' = apply_on_subterm env_rhs evd fixed set_var test c rhs in
+ let evd, fixed, rhs' = apply_on_subterm env_rhs evd fixed set_var test c rhs in
if debug_ho_unification () then
Feedback.msg_debug Pp.(str"abstracted: " ++ prc env_rhs evd rhs');
let () = check_selected_occs env_rhs evd c !occ occs in
let env_rhs' = push_named (NamedDecl.LocalAssum (id,idty)) env_rhs in
- set_holes env_rhs' evd rhs' subst
- | [] -> evd, rhs in
+ set_holes env_rhs' evd fixed rhs' subst
+ | [] -> evd, fixed, rhs in
let subst = make_subst (ctxt,args,argoccs) in
- let evd, rhs' = set_holes env_rhs evd rhs subst in
+ let evd, _, rhs' = set_holes env_rhs evd Evar.Set.empty rhs subst in
let rhs' = nf_evar evd rhs' in
(* Thin evars making the term typable in env_evar *)
let evd, rhs' = thin_evars env_evar evd ctxt rhs' in
diff --git a/pretyping/evardefine.ml b/pretyping/evardefine.ml
index f33030d6a4..eaf8c65811 100644
--- a/pretyping/evardefine.ml
+++ b/pretyping/evardefine.ml
@@ -175,10 +175,7 @@ let define_evar_as_sort env evd (ev,args) =
let evd' = Evd.define ev (mkSort s) evd in
Evd.set_leq_sort env evd' (Sorts.super s) (ESorts.kind evd' 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. *)
+(* Unify with unknown array *)
let rec presplit env sigma c =
let c = Reductionops.whd_all env sigma c in
@@ -189,25 +186,6 @@ let rec presplit env sigma c =
presplit env sigma (mkApp (lam, args))
| _ -> sigma, c
-let split_tycon ?loc env evd tycon =
- match tycon with
- | None -> evd,(make_annot Anonymous Relevant,None,None)
- | Some c ->
- let evd, c = presplit env evd c in
- let evd, na, dom, rng = match EConstr.kind evd c with
- | Prod (na,dom,rng) -> evd, na, dom, rng
- | Evar ev ->
- let (evd,prod) = define_evar_as_product env evd ev in
- let (na,dom,rng) = destProd evd prod in
- let anon = {na with binder_name = Anonymous} in
- evd, anon, dom, rng
- | _ ->
- (* XXX no error to allow later coercion? Not sure if possible with funclass *)
- error_not_product ?loc env evd c
- in
- evd, (na, mk_tycon dom, mk_tycon rng)
-
-
let define_pure_evar_as_array env sigma evk =
let evi = Evd.find_undefined sigma evk in
let evenv = evar_env env evi in
diff --git a/pretyping/evardefine.mli b/pretyping/evardefine.mli
index e5c3f8baa1..5702e169c8 100644
--- a/pretyping/evardefine.mli
+++ b/pretyping/evardefine.mli
@@ -8,7 +8,6 @@
(* * (see LICENSE file for the text of the license) *)
(************************************************************************)
-open Names
open EConstr
open Evd
open Environ
@@ -31,10 +30,6 @@ val mk_valcon : constr -> val_constraint
val evar_absorb_arguments : env -> evar_map -> existential -> constr list ->
evar_map * existential
-val split_tycon :
- ?loc:Loc.t -> env -> evar_map -> type_constraint ->
- evar_map * (Name.t Context.binder_annot * type_constraint * type_constraint)
-
val split_as_array : env -> evar_map -> type_constraint ->
evar_map * type_constraint
(** If the constraint can be made to look like [array A] return [A],
@@ -51,3 +46,6 @@ val define_evar_as_sort : env -> evar_map -> existential -> evar_map * Sorts.t
val pr_tycon : env -> evar_map -> type_constraint -> Pp.t
+(** Used for bidi heuristic when typing lambdas. Transforms an applied
+ evar to an evar with bigger context (ie ?X e to ?X'@{y=e}). *)
+val presplit : env -> evar_map -> EConstr.t -> evar_map * EConstr.t
diff --git a/pretyping/glob_ops.ml b/pretyping/glob_ops.ml
index 5bd26be823..dc5fd80f9e 100644
--- a/pretyping/glob_ops.ml
+++ b/pretyping/glob_ops.ml
@@ -128,7 +128,7 @@ let fix_kind_eq k1 k2 = match k1, k2 with
| (GFix _ | GCoFix _), _ -> false
let instance_eq f (x1,c1) (x2,c2) =
- Id.equal x1 x2 && f c1 c2
+ Id.equal x1.CAst.v x2.CAst.v && f c1 c2
let mk_glob_constr_eq f c1 c2 = match DAst.get c1, DAst.get c2 with
| GRef (gr1, u1), GRef (gr2, u2) ->
@@ -136,7 +136,7 @@ let mk_glob_constr_eq f c1 c2 = match DAst.get c1, DAst.get c2 with
Option.equal (List.equal glob_level_eq) u1 u2
| GVar id1, GVar id2 -> Id.equal id1 id2
| GEvar (id1, arg1), GEvar (id2, arg2) ->
- Id.equal id1 id2 && List.equal (instance_eq f) arg1 arg2
+ Id.equal id1.CAst.v id2.CAst.v && List.equal (instance_eq f) arg1 arg2
| GPatVar k1, GPatVar k2 -> matching_var_kind_eq k1 k2
| GApp (f1, arg1), GApp (f2, arg2) ->
f f1 f2 && List.equal f arg1 arg2
diff --git a/pretyping/glob_term.ml b/pretyping/glob_term.ml
index 526eac6f1e..a49c8abe26 100644
--- a/pretyping/glob_term.ml
+++ b/pretyping/glob_term.ml
@@ -75,7 +75,7 @@ type 'a glob_constr_r =
| GVar of Id.t
(** An identifier that cannot be regarded as "GRef".
Bound variables are typically represented this way. *)
- | GEvar of existential_name * (Id.t * 'a glob_constr_g) list
+ | GEvar of existential_name CAst.t * (lident * 'a glob_constr_g) list
| GPatVar of Evar_kinds.matching_var_kind (** Used for patterns only *)
| GApp of 'a glob_constr_g * 'a glob_constr_g list
| GLambda of Name.t * binding_kind * 'a glob_constr_g * 'a glob_constr_g
diff --git a/pretyping/pretype_errors.ml b/pretyping/pretype_errors.ml
index 1e8441dd8a..1dddc5622d 100644
--- a/pretyping/pretype_errors.ml
+++ b/pretyping/pretype_errors.ml
@@ -48,7 +48,7 @@ type pretype_error =
| CannotUnifyBindingType of constr * constr
| CannotGeneralize of constr
| NoOccurrenceFound of constr * Id.t option
- | CannotFindWellTypedAbstraction of constr * constr list * (env * type_error) option
+ | CannotFindWellTypedAbstraction of constr * constr list * (env * pretype_error) option
| WrongAbstractionType of Name.t * constr * types * types
| AbstractionOverMeta of Name.t * Name.t
| NonLinearUnification of Name.t * constr
diff --git a/pretyping/pretype_errors.mli b/pretyping/pretype_errors.mli
index 45997e9a66..714d68165e 100644
--- a/pretyping/pretype_errors.mli
+++ b/pretyping/pretype_errors.mli
@@ -54,7 +54,7 @@ type pretype_error =
| CannotUnifyBindingType of constr * constr
| CannotGeneralize of constr
| NoOccurrenceFound of constr * Id.t option
- | CannotFindWellTypedAbstraction of constr * constr list * (env * type_error) option
+ | CannotFindWellTypedAbstraction of constr * constr list * (env * pretype_error) option
| WrongAbstractionType of Name.t * constr * types * types
| AbstractionOverMeta of Name.t * Name.t
| NonLinearUnification of Name.t * constr
@@ -132,7 +132,7 @@ val error_cannot_unify : ?loc:Loc.t -> env -> Evd.evar_map ->
val error_cannot_unify_local : env -> Evd.evar_map -> constr * constr * constr -> 'b
val error_cannot_find_well_typed_abstraction : env -> Evd.evar_map ->
- constr -> constr list -> (env * type_error) option -> 'b
+ constr -> constr list -> (env * pretype_error) option -> 'b
val error_wrong_abstraction_type : env -> Evd.evar_map ->
Name.t -> constr -> types -> types -> 'b
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index b9825b6a92..268ad2ae56 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -365,9 +365,9 @@ let inh_conv_coerce_to_tycon ?loc ~program_mode resolve_tc env sigma j = functio
| Some t ->
Coercion.inh_conv_coerce_to ?loc ~program_mode resolve_tc !!env sigma j t
-let check_instance loc subst = function
+let check_instance subst = function
| [] -> ()
- | (id,_) :: _ ->
+ | (CAst.{loc;v=id},_) :: _ ->
if List.mem_assoc id subst then
user_err ?loc (Id.print id ++ str "appears more than once.")
else
@@ -493,7 +493,7 @@ type 'a pretype_fun = ?loc:Loc.t -> program_mode:bool -> poly:bool -> bool -> ty
type pretyper = {
pretype_ref : pretyper -> GlobRef.t * glob_level list option -> unsafe_judgment pretype_fun;
pretype_var : pretyper -> Id.t -> unsafe_judgment pretype_fun;
- pretype_evar : pretyper -> existential_name * (Id.t * glob_constr) list -> unsafe_judgment pretype_fun;
+ pretype_evar : pretyper -> existential_name CAst.t * (lident * glob_constr) list -> unsafe_judgment pretype_fun;
pretype_patvar : pretyper -> Evar_kinds.matching_var_kind -> unsafe_judgment pretype_fun;
pretype_app : pretyper -> glob_constr * glob_constr list -> unsafe_judgment pretype_fun;
pretype_lambda : pretyper -> Name.t * binding_kind * glob_constr * glob_constr -> unsafe_judgment pretype_fun;
@@ -587,10 +587,10 @@ let pretype_instance self ~program_mode ~poly resolve_tc env sigma loc hyps evk
strbrk " is not well-typed.") in
let sigma, c, update =
try
- let c = List.assoc id update in
+ let c = snd (List.find (fun (CAst.{v=id'},c) -> Id.equal id id') update) in
let sigma, c = eval_pretyper self ~program_mode ~poly resolve_tc (mk_tycon t) env sigma c in
check_body sigma id (Some c.uj_val);
- sigma, c.uj_val, List.remove_assoc id update
+ sigma, c.uj_val, List.remove_first (fun (CAst.{v=id'},_) -> Id.equal id id') update
with Not_found ->
try
let (n,b',t') = lookup_rel_id id (rel_context !!env) in
@@ -609,7 +609,7 @@ let pretype_instance self ~program_mode ~poly resolve_tc env sigma loc hyps evk
str " in current context: no binding for " ++ Id.print id ++ str ".") in
((id,c)::subst, update, sigma) in
let subst,inst,sigma = List.fold_right f hyps ([],update,sigma) in
- check_instance loc subst inst;
+ check_instance subst inst;
sigma, List.map snd subst
module Default =
@@ -628,13 +628,13 @@ struct
let sigma, t_id = pretype_id (fun e r t -> pretype tycon e r t) loc env sigma id in
discard_trace @@ inh_conv_coerce_to_tycon ?loc ~program_mode resolve_tc env sigma t_id tycon
- let pretype_evar self (id, inst) ?loc ~program_mode ~poly resolve_tc tycon env sigma =
+ let pretype_evar self (CAst.{v=id;loc=locid}, inst) ?loc ~program_mode ~poly resolve_tc tycon env sigma =
(* Ne faudrait-il pas s'assurer que hyps est bien un
sous-contexte du contexte courant, et qu'il n'y a pas de Rel "caché" *)
let id = interp_ltac_id env id in
let evk =
try Evd.evar_key id sigma
- with Not_found -> error_evar_not_found ?loc !!env sigma id in
+ with Not_found -> error_evar_not_found ?loc:locid !!env sigma id in
let hyps = evar_filtered_context (Evd.find sigma evk) in
let sigma, args = pretype_instance self ~program_mode ~poly resolve_tc env sigma loc hyps evk inst in
let c = mkEvar (evk, args) in
@@ -857,7 +857,7 @@ struct
typing the argument, so we replace it by an existential
variable *)
let sigma, c_hole = new_evar env sigma ~src:(loc,Evar_kinds.InternalHole) c1 in
- (sigma, make_judge c_hole c1), (c_hole, c, trace) :: bidiargs
+ (sigma, make_judge c_hole c1), (c_hole, c1, c, trace) :: bidiargs
else
let tycon = Some c1 in
pretype tycon env sigma c, bidiargs
@@ -886,12 +886,10 @@ struct
let sigma, resj, resj_before_bidi, bidiargs = apply_rec env sigma 0 fj fj candargs [] args in
let sigma, resj = refresh_template env sigma resj in
let sigma, resj, otrace = inh_conv_coerce_to_tycon ?loc ~program_mode resolve_tc env sigma resj tycon in
- let refine_arg n (sigma,t) (newarg,origarg,trace) =
+ let refine_arg n (sigma,t) (newarg,ty,origarg,trace) =
(* Refine an argument (originally `origarg`) represented by an evar
(`newarg`) to use typing information from the context *)
- (* Recover the expected type of the argument *)
- let ty = Retyping.get_type_of !!env sigma newarg in
- (* Type the argument using this expected type *)
+ (* Type the argument using the expected type *)
let sigma, j = pretype (Some ty) env sigma origarg in
(* Unify the (possibly refined) existential variable with the
(typechecked) original value *)
@@ -925,7 +923,32 @@ struct
let sigma, ty' = Coercion.inh_coerce_to_prod ?loc ~program_mode !!env sigma ty in
sigma, Some ty'
in
- let sigma, (name',dom,rng) = split_tycon ?loc !!env sigma tycon' in
+ let sigma,name',dom,rng =
+ match tycon' with
+ | None -> sigma,Anonymous, None, None
+ | Some ty ->
+ let sigma, ty = Evardefine.presplit !!env sigma ty in
+ match EConstr.kind sigma ty with
+ | Prod (na,dom,rng) ->
+ sigma, na.binder_name, Some dom, Some rng
+ | Evar ev ->
+ (* define_evar_as_product works badly when impredicativity
+ is possible but not known (#12623). OTOH if we know we
+ are impredicative (typically Prop) we want to keep the
+ information when typing the body. *)
+ let s = Retyping.get_sort_of !!env sigma ty in
+ if Environ.is_impredicative_sort !!env s
+ || Evd.check_leq sigma (Univ.Universe.type1) (Sorts.univ_of_sort s)
+ then
+ let sigma, prod = define_evar_as_product !!env sigma ev in
+ let na,dom,rng = destProd sigma prod in
+ sigma, na.binder_name, Some dom, Some rng
+ else
+ sigma, Anonymous, None, None
+ | _ ->
+ (* XXX no error to allow later coercion? Not sure if possible with funclass *)
+ error_not_product ?loc !!env sigma ty
+ in
let dom_valcon = valcon_of_tycon dom in
let sigma, j = eval_type_pretyper self ~program_mode ~poly resolve_tc dom_valcon env sigma c1 in
let name = {binder_name=name; binder_relevance=Sorts.relevance_of_sort j.utj_type} in
@@ -934,7 +957,7 @@ struct
let var',env' = push_rel ~hypnaming sigma var env in
let sigma, j' = eval_pretyper self ~program_mode ~poly resolve_tc rng env' sigma c2 in
let name = get_name var' in
- let resj = judge_of_abstraction !!env (orelse_name name name'.binder_name) j j' in
+ let resj = judge_of_abstraction !!env (orelse_name name name') j j' in
discard_trace @@ inh_conv_coerce_to_tycon ?loc ~program_mode resolve_tc env sigma resj tycon
let pretype_prod self (name, bk, c1, c2) =
diff --git a/pretyping/pretyping.mli b/pretyping/pretyping.mli
index c03374c59f..7bb4a6e273 100644
--- a/pretyping/pretyping.mli
+++ b/pretyping/pretyping.mli
@@ -148,7 +148,7 @@ type 'a pretype_fun = ?loc:Loc.t -> program_mode:bool -> poly:bool -> bool -> Ev
type pretyper = {
pretype_ref : pretyper -> GlobRef.t * glob_level list option -> unsafe_judgment pretype_fun;
pretype_var : pretyper -> Id.t -> unsafe_judgment pretype_fun;
- pretype_evar : pretyper -> existential_name * (Id.t * glob_constr) list -> unsafe_judgment pretype_fun;
+ pretype_evar : pretyper -> existential_name CAst.t * (lident * glob_constr) list -> unsafe_judgment pretype_fun;
pretype_patvar : pretyper -> Evar_kinds.matching_var_kind -> unsafe_judgment pretype_fun;
pretype_app : pretyper -> glob_constr * glob_constr list -> unsafe_judgment pretype_fun;
pretype_lambda : pretyper -> Name.t * binding_kind * glob_constr * glob_constr -> unsafe_judgment pretype_fun;
diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml
index aeb18ec322..3352bfce38 100644
--- a/pretyping/reductionops.ml
+++ b/pretyping/reductionops.ml
@@ -445,7 +445,7 @@ type state_reduction_function =
let pr_state env sigma (tm,sk) =
let open Pp in
let pr c = Termops.Internal.print_constr_env env sigma c in
- h 0 (pr tm ++ str "|" ++ cut () ++ Stack.pr pr sk)
+ h (pr tm ++ str "|" ++ cut () ++ Stack.pr pr sk)
(*************************************)
(*** Reduction Functions Operators ***)
@@ -705,7 +705,7 @@ let rec whd_state_gen flags env sigma =
let open Pp in
let pr c = Termops.Internal.print_constr_env env sigma c in
Feedback.msg_debug
- (h 0 (str "<<" ++ pr x ++
+ (h (str "<<" ++ pr x ++
str "|" ++ cut () ++ Stack.pr pr stack ++
str ">>"))
in
@@ -1094,7 +1094,8 @@ let f_conv_leq ?l2r ?reds env ?evars x y =
let test_trans_conversion (f: constr Reduction.extended_conversion_function) reds env sigma x y =
try
let evars ev = safe_evar_value sigma ev in
- let _ = f ~reds env ~evars:(evars, Evd.universes sigma) x y in
+ let env = Environ.set_universes (Evd.universes sigma) env in
+ let _ = f ~reds env ~evars x y in
true
with Reduction.NotConvertible -> false
| e ->
@@ -1112,7 +1113,8 @@ let check_conv ?(pb=Reduction.CUMUL) ?(ts=TransparentState.full) env sigma x y =
| Reduction.CONV -> f_conv
| Reduction.CUMUL -> f_conv_leq
in
- try f ~reds:ts env ~evars:(safe_evar_value sigma, Evd.universes sigma) x y; true
+ let env = Environ.set_universes (Evd.universes sigma) env in
+ try f ~reds:ts env ~evars:(safe_evar_value sigma) x y; true
with Reduction.NotConvertible -> false
| Univ.UniverseInconsistency _ -> false
| e ->
@@ -1138,8 +1140,7 @@ let sigma_check_inductive_instances cv_pb variance u1 u2 sigma =
let sigma_univ_state =
let open Reduction in
- { compare_graph = Evd.universes;
- compare_sorts = sigma_compare_sorts;
+ { compare_sorts = sigma_compare_sorts;
compare_instances = sigma_compare_instances;
compare_cumul_instances = sigma_check_inductive_instances; }
@@ -1164,6 +1165,7 @@ let infer_conv_gen conv_fun ?(catch_incon=true) ?(pb=Reduction.CUMUL)
| None ->
let x = EConstr.Unsafe.to_constr x in
let y = EConstr.Unsafe.to_constr y in
+ let env = Environ.set_universes (Evd.universes sigma) env in
let sigma' =
conv_fun pb ~l2r:false sigma ts
env (sigma, sigma_univ_state) x y in
diff --git a/pretyping/typeclasses.ml b/pretyping/typeclasses.ml
index fc71254a46..51b228a640 100644
--- a/pretyping/typeclasses.ml
+++ b/pretyping/typeclasses.ml
@@ -56,7 +56,7 @@ type typeclass = {
cl_impl : GlobRef.t;
(* Context in which the definitions are typed. Includes both typeclass parameters and superclasses. *)
- cl_context : GlobRef.t option list * Constr.rel_context;
+ cl_context : Constr.rel_context;
(* Context of definitions and properties on defs, will not be shared *)
cl_props : Constr.rel_context;
@@ -97,7 +97,7 @@ let instances : instances ref = Summary.ref GlobRef.Map.empty ~name:"instances"
let typeclass_univ_instance (cl, u) =
assert (Univ.AUContext.size cl.cl_univs == Univ.Instance.length u);
let subst_ctx c = Context.Rel.map (subst_instance_constr u) c in
- { cl with cl_context = on_snd subst_ctx cl.cl_context;
+ { cl with cl_context = subst_ctx cl.cl_context;
cl_props = subst_ctx cl.cl_props}
let class_info env sigma c =
@@ -178,7 +178,7 @@ let remove_instance inst =
let instance_constructor (cl,u) args =
- let lenpars = List.count is_local_assum (snd cl.cl_context) in
+ let lenpars = List.count is_local_assum cl.cl_context in
let open EConstr in
let pars = fst (List.chop lenpars args) in
match cl.cl_impl with
diff --git a/pretyping/typeclasses.mli b/pretyping/typeclasses.mli
index 3f84d08a7e..b749b978c3 100644
--- a/pretyping/typeclasses.mli
+++ b/pretyping/typeclasses.mli
@@ -36,9 +36,9 @@ type typeclass = {
(** The class implementation: a record parameterized by the context with defs in it or a definition if
the class is a singleton. This acts as the class' global identifier. *)
- cl_context : GlobRef.t option list * Constr.rel_context;
- (** Context in which the definitions are typed. Includes both typeclass parameters and superclasses.
- The global reference gives a direct link to the class itself. *)
+ cl_context : Constr.rel_context;
+ (** Context in which the definitions are typed.
+ Includes both typeclass parameters and superclasses. *)
cl_props : Constr.rel_context;
(** Context of definitions and properties on defs, will not be shared *)
diff --git a/pretyping/typing.ml b/pretyping/typing.ml
index 756ccd3438..aeb3873de7 100644
--- a/pretyping/typing.ml
+++ b/pretyping/typing.ml
@@ -220,14 +220,15 @@ let check_allowed_sort env sigma ind c p =
else
Sorts.relevance_of_sort_family ksort
+let check_actual_type env sigma cj t =
+ try Evarconv.unify_leq_delay env sigma cj.uj_type t
+ with Evarconv.UnableToUnify (sigma,e) -> error_actual_type env sigma cj t e
+
let judge_of_cast env sigma cj k tj =
let expected_type = tj.utj_val in
- match Evarconv.unify_leq_delay env sigma cj.uj_type expected_type with
- | exception Evarconv.UnableToUnify _ ->
- error_actual_type_core env sigma cj expected_type;
- | sigma ->
- sigma, { uj_val = mkCast (cj.uj_val, k, expected_type);
- uj_type = expected_type }
+ let sigma = check_actual_type env sigma cj expected_type in
+ sigma, { uj_val = mkCast (cj.uj_val, k, expected_type);
+ uj_type = expected_type }
let check_fix env sigma pfix =
let inj c = EConstr.to_constr ~abort_on_undefined_evars:false sigma c in
@@ -296,7 +297,8 @@ let judge_of_letin env name defj typj j =
uj_type = subst1 defj.uj_val j.uj_type }
let check_hyps_inclusion env sigma x hyps =
- let evars = Evarutil.safe_evar_value sigma, Evd.universes sigma in
+ let env = Environ.set_universes (Evd.universes sigma) env in
+ let evars = Evarutil.safe_evar_value sigma in
Typeops.check_hyps_inclusion env ~evars x hyps
let type_of_constant env sigma (c,u) =
@@ -340,7 +342,7 @@ let judge_of_array env sigma u tj defj tyj =
let sigma = Evd.set_leq_sort env sigma tyj.utj_type
(Sorts.sort_of_univ (Univ.Universe.make ulev))
in
- let check_one sigma j = Evarconv.unify_leq_delay env sigma j.uj_type tyj.utj_val in
+ let check_one sigma j = check_actual_type env sigma j tyj.utj_val in
let sigma = check_one sigma defj in
let sigma = Array.fold_left check_one sigma tj in
let arr = EConstr.of_constr @@ type_of_array env u in
@@ -391,7 +393,7 @@ let rec execute env sigma cstr =
let t = mkApp (mkIndU (ci.ci_ind,univs), args) in
let sigma, tj = execute env sigma t in
let sigma, tj = type_judgment env sigma tj in
- let sigma = Evarconv.unify_leq_delay env sigma cj.uj_type tj.utj_val in
+ let sigma = check_actual_type env sigma cj tj.utj_val in
sigma
in
judge_of_case env sigma ci pj iv cj lfj
@@ -492,10 +494,7 @@ and execute_array env = Array.fold_left_map (execute env)
let check env sigma c t =
let sigma, j = execute env sigma c in
- match Evarconv.unify_leq_delay env sigma j.uj_type t with
- | exception Evarconv.UnableToUnify _ ->
- error_actual_type_core env sigma j t
- | sigma -> sigma
+ check_actual_type env sigma j t
(* Type of a constr *)
diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index 207a03d80f..ccfb508964 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -134,8 +134,8 @@ let abstract_list_all env evd typ c l =
| Type_errors.TypeError (env',x) ->
(* FIXME: plug back the typing information *)
error_cannot_find_well_typed_abstraction env evd p l None
- | Pretype_errors.PretypeError (env',evd,TypingError x) ->
- error_cannot_find_well_typed_abstraction env evd p l (Some (env',x)) in
+ | Pretype_errors.PretypeError (env',evd,e) ->
+ error_cannot_find_well_typed_abstraction env evd p l (Some (env',e)) in
evd,(p,typp)
let set_occurrences_of_last_arg n =
diff --git a/pretyping/vnorm.ml b/pretyping/vnorm.ml
index 900ba0edb9..1420401875 100644
--- a/pretyping/vnorm.ml
+++ b/pretyping/vnorm.ml
@@ -218,7 +218,8 @@ and nf_evar env sigma evk stk =
let t = List.fold_left fold concl hyps in
let t, args = nf_args env sigma args t in
let inst, args = Array.chop (List.length hyps) args in
- let inst = Array.to_list inst in
+ (* Evar instances are reversed w.r.t. argument order *)
+ let inst = Array.rev_to_list inst in
let c = mkApp (mkEvar (evk, inst), args) in
nf_stk env sigma c t stk
| _ ->
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-03 12:34:56 +0000