aboutsummaryrefslogtreecommitdiff
path: root/pretyping
diff options
context:
space:
mode:
Diffstat (limited to 'pretyping')
-rw-r--r--pretyping/classops.ml39
-rw-r--r--pretyping/classops.mli2
-rw-r--r--pretyping/evarconv.ml17
-rw-r--r--pretyping/geninterp.ml7
-rw-r--r--pretyping/geninterp.mli7
-rw-r--r--pretyping/globEnv.ml6
-rw-r--r--pretyping/globEnv.mli4
-rw-r--r--pretyping/pretyping.ml64
-rw-r--r--pretyping/pretyping.mli1
-rw-r--r--pretyping/recordops.ml51
-rw-r--r--pretyping/recordops.mli4
11 files changed, 129 insertions, 73 deletions
diff --git a/pretyping/classops.ml b/pretyping/classops.ml
index ef918a614e..5560e5e5f5 100644
--- a/pretyping/classops.ml
+++ b/pretyping/classops.ml
@@ -305,9 +305,16 @@ let install_path_printer f = path_printer := f
let print_path x = !path_printer x
-let message_ambig l =
- str"Ambiguous paths:" ++ spc () ++
- prlist_with_sep fnl print_path l
+let path_comparator : (inheritance_path -> inheritance_path -> bool) ref =
+ ref (fun _ _ -> false)
+
+let install_path_comparator f = path_comparator := f
+
+let compare_path p q = !path_comparator p q
+
+let warn_ambiguous_path =
+ CWarnings.create ~name:"ambiguous-paths" ~category:"typechecker"
+ (fun l -> strbrk"Ambiguous paths: " ++ prlist_with_sep fnl print_path l)
(* add_coercion_in_graph : coe_index * cl_index * cl_index -> unit
coercion,source,target *)
@@ -326,21 +333,15 @@ let add_coercion_in_graph (ic,source,target) =
let ambig_paths =
(ref [] : ((cl_index * cl_index) * inheritance_path) list ref) in
let try_add_new_path (i,j as ij) p =
- try
- if Bijint.Index.equal i j then begin
- if different_class_params i then begin
- let _ = lookup_path_between_class ij in
- ambig_paths := (ij,p)::!ambig_paths
- end
- end else begin
- let _ = lookup_path_between_class ij in
- ambig_paths := (ij,p)::!ambig_paths
- end;
+ if not (Bijint.Index.equal i j) || different_class_params i then
+ match lookup_path_between_class ij with
+ | q ->
+ if not (compare_path p q) then
+ ambig_paths := (ij,p)::!ambig_paths;
+ false
+ | exception Not_found -> (add_new_path ij p; true)
+ else
false
- with Not_found -> begin
- add_new_path ij p;
- true
- end
in
let try_add_new_path1 ij p =
let _ = try_add_new_path ij p in ()
@@ -361,9 +362,7 @@ let add_coercion_in_graph (ic,source,target) =
end)
old_inheritance_graph
end;
- let is_ambig = match !ambig_paths with [] -> false | _ -> true in
- if is_ambig && not !Flags.quiet then
- Feedback.msg_info (message_ambig !ambig_paths)
+ match !ambig_paths with [] -> () | _ -> warn_ambiguous_path !ambig_paths
type coercion = {
coercion_type : coe_typ;
diff --git a/pretyping/classops.mli b/pretyping/classops.mli
index ed2c5478f0..bd468e62ad 100644
--- a/pretyping/classops.mli
+++ b/pretyping/classops.mli
@@ -100,6 +100,8 @@ val lookup_pattern_path_between :
(* Crade *)
val install_path_printer :
((cl_index * cl_index) * inheritance_path -> Pp.t) -> unit
+val install_path_comparator :
+ (inheritance_path -> inheritance_path -> bool) -> unit
(**/**)
(** {6 This is for printing purpose } *)
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index 28a97bb91a..0ccc4fd9f9 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -503,14 +503,23 @@ let rec evar_conv_x flags env evd pbty term1 term2 =
| Evar ev, _ when Evd.is_undefined evd (fst ev) && not (is_frozen flags ev) ->
(match solve_simple_eqn (conv_fun evar_conv_x) flags env evd
(position_problem true pbty,ev,term2) with
- | UnifFailure (_,OccurCheck _) ->
- (* Eta-expansion might apply *) default ()
+ | UnifFailure (_,(OccurCheck _ | NotClean _)) ->
+ (* Eta-expansion might apply *)
+ (* OccurCheck: eta-expansion could solve
+ ?X = {| foo := ?X.(foo) |}
+ NotClean: pruning in solve_simple_eqn is incomplete wrt
+ Miller patterns *)
+ default ()
| x -> x)
| _, Evar ev when Evd.is_undefined evd (fst ev) && not (is_frozen flags ev) ->
(match solve_simple_eqn (conv_fun evar_conv_x) flags env evd
(position_problem false pbty,ev,term1) with
- | UnifFailure (_, OccurCheck _) ->
- (* Eta-expansion might apply *) default ()
+ | UnifFailure (_, (OccurCheck _ | NotClean _)) ->
+ (* OccurCheck: eta-expansion could solve
+ ?X = {| foo := ?X.(foo) |}
+ NotClean: pruning in solve_simple_eqn is incomplete wrt
+ Miller patterns *)
+ default ()
| x -> x)
| _ -> default ()
end
diff --git a/pretyping/geninterp.ml b/pretyping/geninterp.ml
index 1f8b926365..32152ad0e4 100644
--- a/pretyping/geninterp.ml
+++ b/pretyping/geninterp.ml
@@ -82,9 +82,10 @@ let register_val0 wit tag =
(** Interpretation functions *)
-type interp_sign = {
- lfun : Val.t Id.Map.t;
- extra : TacStore.t }
+type interp_sign =
+ { lfun : Val.t Id.Map.t
+ ; poly : bool
+ ; extra : TacStore.t }
type ('glb, 'top) interp_fun = interp_sign -> 'glb -> 'top Ftactic.t
diff --git a/pretyping/geninterp.mli b/pretyping/geninterp.mli
index 606a6ebead..49d874289d 100644
--- a/pretyping/geninterp.mli
+++ b/pretyping/geninterp.mli
@@ -62,9 +62,10 @@ val register_val0 : ('raw, 'glb, 'top) genarg_type -> 'top Val.tag option -> uni
module TacStore : Store.S
-type interp_sign = {
- lfun : Val.t Id.Map.t;
- extra : TacStore.t }
+type interp_sign =
+ { lfun : Val.t Id.Map.t
+ ; poly : bool
+ ; extra : TacStore.t }
type ('glb, 'top) interp_fun = interp_sign -> 'glb -> 'top Ftactic.t
diff --git a/pretyping/globEnv.ml b/pretyping/globEnv.ml
index cd82b1993b..e76eb2a7de 100644
--- a/pretyping/globEnv.ml
+++ b/pretyping/globEnv.ml
@@ -183,7 +183,7 @@ let interp_ltac_id env id = ltac_interp_id env.lvar id
module ConstrInterpObj =
struct
type ('r, 'g, 't) obj =
- unbound_ltac_var_map -> env -> Evd.evar_map -> types -> 'g -> constr * Evd.evar_map
+ unbound_ltac_var_map -> bool -> env -> Evd.evar_map -> types -> 'g -> constr * Evd.evar_map
let name = "constr_interp"
let default _ = None
end
@@ -192,8 +192,8 @@ module ConstrInterp = Genarg.Register(ConstrInterpObj)
let register_constr_interp0 = ConstrInterp.register0
-let interp_glob_genarg env sigma ty arg =
+let interp_glob_genarg env poly sigma ty arg =
let open Genarg in
let GenArg (Glbwit tag, arg) = arg in
let interp = ConstrInterp.obj tag in
- interp env.lvar.ltac_genargs env.renamed_env sigma ty arg
+ interp env.lvar.ltac_genargs poly env.renamed_env sigma ty arg
diff --git a/pretyping/globEnv.mli b/pretyping/globEnv.mli
index 65ae495135..cdd36bbba6 100644
--- a/pretyping/globEnv.mli
+++ b/pretyping/globEnv.mli
@@ -19,7 +19,7 @@ open Evarutil
val register_constr_interp0 :
('r, 'g, 't) Genarg.genarg_type ->
- (unbound_ltac_var_map -> env -> evar_map -> types -> 'g -> constr * evar_map) -> unit
+ (unbound_ltac_var_map -> bool -> env -> evar_map -> types -> 'g -> constr * evar_map) -> unit
(** {6 Pretyping name management} *)
@@ -85,5 +85,5 @@ val interp_ltac_id : t -> Id.t -> Id.t
(** Interpreting a generic argument, typically a "ltac:(...)", taking
into account the possible renaming *)
-val interp_glob_genarg : t -> evar_map -> constr ->
+val interp_glob_genarg : t -> bool -> evar_map -> constr ->
Genarg.glob_generic_argument -> constr * evar_map
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index fa64c21d1e..a6e3cfe085 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -198,6 +198,7 @@ type inference_flags = {
fail_evar : bool;
expand_evars : bool;
program_mode : bool;
+ polymorphic : bool;
}
(* Compute the set of still-undefined initial evars up to restriction
@@ -474,10 +475,10 @@ let mark_obligation_evar sigma k evc =
(* in environment [env], with existential variables [sigma] and *)
(* the type constraint tycon *)
-let rec pretype ~program_mode k0 resolve_tc (tycon : type_constraint) (env : GlobEnv.t) (sigma : evar_map) t =
+let rec pretype ~program_mode ~poly k0 resolve_tc (tycon : type_constraint) (env : GlobEnv.t) (sigma : evar_map) t =
let inh_conv_coerce_to_tycon ?loc = inh_conv_coerce_to_tycon ?loc ~program_mode resolve_tc in
- let pretype_type = pretype_type ~program_mode k0 resolve_tc in
- let pretype = pretype ~program_mode k0 resolve_tc in
+ let pretype_type = pretype_type ~program_mode ~poly k0 resolve_tc in
+ let pretype = pretype ~program_mode ~poly k0 resolve_tc in
let open Context.Rel.Declaration in
let loc = t.CAst.loc in
match DAst.get t with
@@ -497,7 +498,7 @@ let rec pretype ~program_mode k0 resolve_tc (tycon : type_constraint) (env : Glo
try Evd.evar_key id sigma
with Not_found -> error_evar_not_found ?loc !!env sigma id in
let hyps = evar_filtered_context (Evd.find sigma evk) in
- let sigma, args = pretype_instance ~program_mode k0 resolve_tc env sigma loc hyps evk inst in
+ let sigma, args = pretype_instance ~program_mode ~poly k0 resolve_tc env sigma loc hyps evk inst in
let c = mkEvar (evk, args) in
let j = Retyping.get_judgment_of !!env sigma c in
inh_conv_coerce_to_tycon ?loc env sigma j tycon
@@ -530,7 +531,7 @@ let rec pretype ~program_mode k0 resolve_tc (tycon : type_constraint) (env : Glo
match tycon with
| Some ty -> sigma, ty
| None -> new_type_evar env sigma loc in
- let c, sigma = GlobEnv.interp_glob_genarg env sigma ty arg in
+ let c, sigma = GlobEnv.interp_glob_genarg env poly sigma ty arg in
sigma, { uj_val = c; uj_type = ty }
| GRec (fixkind,names,bl,lar,vdef) ->
@@ -983,7 +984,7 @@ let rec pretype ~program_mode k0 resolve_tc (tycon : type_constraint) (env : Glo
in
inh_conv_coerce_to_tycon ?loc env sigma resj tycon
-and pretype_instance ~program_mode k0 resolve_tc env sigma loc hyps evk update =
+and pretype_instance ~program_mode ~poly k0 resolve_tc env sigma loc hyps evk update =
let f decl (subst,update,sigma) =
let id = NamedDecl.get_id decl in
let b = Option.map (replace_vars subst) (NamedDecl.get_value decl) in
@@ -1015,7 +1016,7 @@ and pretype_instance ~program_mode k0 resolve_tc env sigma loc hyps evk update =
let sigma, c, update =
try
let c = List.assoc id update in
- let sigma, c = pretype ~program_mode k0 resolve_tc (mk_tycon t) env sigma c in
+ let sigma, c = pretype ~program_mode ~poly k0 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
with Not_found ->
@@ -1040,7 +1041,7 @@ and pretype_instance ~program_mode k0 resolve_tc env sigma loc hyps evk update =
sigma, Array.map_of_list snd subst
(* [pretype_type valcon env sigma c] coerces [c] into a type *)
-and pretype_type ~program_mode k0 resolve_tc valcon (env : GlobEnv.t) sigma c = match DAst.get c with
+and pretype_type ~program_mode ~poly k0 resolve_tc valcon (env : GlobEnv.t) sigma c = match DAst.get c with
| GHole (knd, naming, None) ->
let loc = loc_of_glob_constr c in
(match valcon with
@@ -1067,7 +1068,7 @@ and pretype_type ~program_mode k0 resolve_tc valcon (env : GlobEnv.t) sigma c =
let sigma = if program_mode then mark_obligation_evar sigma knd utj_val else sigma in
sigma, { utj_val; utj_type = s})
| _ ->
- let sigma, j = pretype ~program_mode k0 resolve_tc empty_tycon env sigma c in
+ let sigma, j = pretype ~program_mode ~poly k0 resolve_tc empty_tycon env sigma c in
let loc = loc_of_glob_constr c in
let sigma, tj = Coercion.inh_coerce_to_sort ?loc !!env sigma j in
match valcon with
@@ -1082,6 +1083,7 @@ and pretype_type ~program_mode k0 resolve_tc valcon (env : GlobEnv.t) sigma c =
let ise_pretype_gen flags env sigma lvar kind c =
let program_mode = flags.program_mode in
+ let poly = flags.polymorphic in
let hypnaming =
if program_mode then ProgramNaming else KeepUserNameAndRenameExistingButSectionNames
in
@@ -1089,13 +1091,13 @@ let ise_pretype_gen flags env sigma lvar kind c =
let k0 = Context.Rel.length (rel_context !!env) in
let sigma', c', c'_ty = match kind with
| WithoutTypeConstraint ->
- let sigma, j = pretype ~program_mode k0 flags.use_typeclasses empty_tycon env sigma c in
+ let sigma, j = pretype ~program_mode ~poly k0 flags.use_typeclasses empty_tycon env sigma c in
sigma, j.uj_val, j.uj_type
| OfType exptyp ->
- let sigma, j = pretype ~program_mode k0 flags.use_typeclasses (mk_tycon exptyp) env sigma c in
+ let sigma, j = pretype ~program_mode ~poly k0 flags.use_typeclasses (mk_tycon exptyp) env sigma c in
sigma, j.uj_val, j.uj_type
| IsType ->
- let sigma, tj = pretype_type ~program_mode k0 flags.use_typeclasses empty_valcon env sigma c in
+ let sigma, tj = pretype_type ~program_mode ~poly k0 flags.use_typeclasses empty_valcon env sigma c in
sigma, tj.utj_val, mkSort tj.utj_type
in
process_inference_flags flags !!env sigma (sigma',c',c'_ty)
@@ -1106,6 +1108,7 @@ let default_inference_flags fail = {
fail_evar = fail;
expand_evars = true;
program_mode = false;
+ polymorphic = false;
}
let no_classes_no_fail_inference_flags = {
@@ -1114,6 +1117,7 @@ let no_classes_no_fail_inference_flags = {
fail_evar = false;
expand_evars = true;
program_mode = false;
+ polymorphic = false;
}
let all_and_fail_flags = default_inference_flags true
@@ -1141,3 +1145,39 @@ let understand_tcc ?flags env sigma ?expected_type c =
let understand_ltac flags env sigma lvar kind c =
let (sigma, c, _) = ise_pretype_gen flags env sigma lvar kind c in
(sigma, c)
+
+let path_convertible p q =
+ let open Classops in
+ let mkGRef ref = DAst.make @@ Glob_term.GRef(ref,None) in
+ let mkGVar id = DAst.make @@ Glob_term.GVar(id) in
+ let mkGApp(rt,rtl) = DAst.make @@ Glob_term.GApp(rt,rtl) in
+ let mkGLambda(n,t,b) = DAst.make @@ Glob_term.GLambda(n,Decl_kinds.Explicit,t,b) in
+ let mkGHole () = DAst.make @@ Glob_term.GHole(Evar_kinds.BinderType Anonymous,Namegen.IntroAnonymous,None) in
+ let path_to_gterm p =
+ match p with
+ | ic :: p' ->
+ let names =
+ List.map (fun n -> Id.of_string ("x" ^ string_of_int n))
+ (List.interval 0 ic.coe_param)
+ in
+ List.fold_right
+ (fun id t -> mkGLambda (Name id, mkGHole (), t)) names @@
+ List.fold_left
+ (fun t ic ->
+ mkGApp (mkGRef ic.coe_value,
+ List.make ic.coe_param (mkGHole ()) @ [t]))
+ (mkGApp (mkGRef ic.coe_value, List.map (fun i -> mkGVar i) names))
+ p'
+ | [] -> anomaly (str "A coercion path shouldn't be empty.")
+ in
+ try
+ let e = Global.env () in
+ let sigma,tp = understand_tcc e (Evd.from_env e) (path_to_gterm p) in
+ let sigma,tq = understand_tcc e sigma (path_to_gterm q) in
+ if Evd.has_undefined sigma then
+ false
+ else
+ let _ = Evarconv.unify_delay e sigma tp tq in true
+ with Evarconv.UnableToUnify _ | PretypeError _ -> false
+
+let _ = Classops.install_path_comparator path_convertible
diff --git a/pretyping/pretyping.mli b/pretyping/pretyping.mli
index 3c875e69d2..1037cf6cc5 100644
--- a/pretyping/pretyping.mli
+++ b/pretyping/pretyping.mli
@@ -38,6 +38,7 @@ type inference_flags = {
fail_evar : bool;
expand_evars : bool;
program_mode : bool;
+ polymorphic : bool;
}
val default_inference_flags : bool -> inference_flags
diff --git a/pretyping/recordops.ml b/pretyping/recordops.ml
index 6d9e3230a4..ef56458f99 100644
--- a/pretyping/recordops.ml
+++ b/pretyping/recordops.ml
@@ -45,14 +45,14 @@ let structure_table =
let projection_table =
Summary.ref (Cmap.empty : struc_typ Cmap.t) ~name:"record-projs"
-(* TODO: could be unify struc_typ and struc_tuple ? in particular,
- is the inductive always (fst constructor) ? It seems so... *)
+(* TODO: could be unify struc_typ and struc_tuple ? *)
type struc_tuple =
- inductive * constructor * (Name.t * bool) list * Constant.t option list
+ constructor * (Name.t * bool) list * Constant.t option list
-let load_structure i (_,(ind,id,kl,projs)) =
+let load_structure i (_, (id,kl,projs)) =
let open Declarations in
+ let ind = fst id in
let mib, mip = Global.lookup_inductive ind in
let n = mib.mind_nparams in
let struc =
@@ -65,8 +65,7 @@ let load_structure i (_,(ind,id,kl,projs)) =
let cache_structure o =
load_structure 1 o
-let subst_structure (subst,((kn,i),id,kl,projs as obj)) =
- let kn' = subst_mind subst kn in
+let subst_structure (subst, (id, kl, projs as obj)) =
let projs' =
(* invariant: struc.s_PROJ is an evaluable reference. Thus we can take *)
(* the first component of subst_con. *)
@@ -75,10 +74,10 @@ let subst_structure (subst,((kn,i),id,kl,projs as obj)) =
projs
in
let id' = subst_constructor subst id in
- if projs' == projs && kn' == kn && id' == id then obj else
- ((kn',i),id',kl,projs')
+ if projs' == projs && id' == id then obj else
+ (id',kl,projs')
-let discharge_structure (_,x) = Some x
+let discharge_structure (_, x) = Some x
let inStruc : struc_tuple -> obj =
declare_object {(default_object "STRUCTURE") with
@@ -88,8 +87,8 @@ let inStruc : struc_tuple -> obj =
classify_function = (fun x -> Substitute x);
discharge_function = discharge_structure }
-let declare_structure (s,c,kl,pl) =
- Lib.add_anonymous_leaf (inStruc (s,c,kl,pl))
+let declare_structure o =
+ Lib.add_anonymous_leaf (inStruc o)
let lookup_structure indsp = Indmap.find indsp !structure_table
@@ -103,6 +102,8 @@ let find_projection = function
| ConstRef cst -> Cmap.find cst !projection_table
| _ -> raise Not_found
+let is_projection cst = Cmap.mem cst !projection_table
+
let prim_table =
Summary.ref (Cmap_env.empty : Projection.Repr.t Cmap_env.t) ~name:"record-prim-projs"
@@ -277,21 +278,21 @@ let add_canonical_structure warn o =
(* 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) ->
+ compute_canonical_projections env warn o |>
+ 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)
- with Not_found -> None
- in match ocs with
- | None -> object_table := GlobRef.Map.add proj ((pat,s)::l) !object_table;
- | Some (c, cs) ->
- 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
- let prj = (Nametab.pr_global_env Id.Set.empty proj)
- and hd_val = (pr_cs_pattern cs_pat) in
- if warn then warn_redundant_canonical_projection (hd_val,prj,new_can_s,old_can_s))
- lo
+ match assoc_pat cs_pat l with
+ | exception Not_found ->
+ object_table := GlobRef.Map.add proj ((pat, s) :: l) !object_table
+ | _, cs ->
+ if warn
+ then
+ let old_can_s = Termops.Internal.print_constr_env env sigma (EConstr.of_constr cs.o_DEF) in
+ let new_can_s = Termops.Internal.print_constr_env env sigma (EConstr.of_constr s.o_DEF) in
+ let prj = Nametab.pr_global_env Id.Set.empty proj in
+ let hd_val = pr_cs_pattern cs_pat in
+ warn_redundant_canonical_projection (hd_val, prj, new_can_s, old_can_s)
+ )
let open_canonical_structure i (_, o) =
if Int.equal i 1 then add_canonical_structure false o
diff --git a/pretyping/recordops.mli b/pretyping/recordops.mli
index 3e43372b65..53a33f6bab 100644
--- a/pretyping/recordops.mli
+++ b/pretyping/recordops.mli
@@ -24,7 +24,7 @@ type struc_typ = {
s_PROJ : Constant.t option list }
type struc_tuple =
- inductive * constructor * (Name.t * bool) list * Constant.t option list
+ constructor * (Name.t * bool) list * Constant.t option list
val declare_structure : struc_tuple -> unit
@@ -44,6 +44,8 @@ val find_projection_nparams : GlobRef.t -> int
(** raise [Not_found] if not a projection *)
val find_projection : GlobRef.t -> struc_typ
+val is_projection : Constant.t -> bool
+
(** Sets up the mapping from constants to primitive projections *)
val declare_primitive_projection : Projection.Repr.t -> Constant.t -> unit
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-02 21:31:06 +0000