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/pretyping.ml45
-rw-r--r--pretyping/pretyping.mli2
-rw-r--r--pretyping/reductionops.ml4
-rw-r--r--pretyping/vnorm.ml3
10 files changed, 84 insertions, 67 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/pretyping.ml b/pretyping/pretyping.ml
index b9825b6a92..8f52018a44 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
@@ -925,7 +925,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 +959,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..08a6db5639 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
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-03-08 05:49:04 +0000