aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--doc/changelog/02-specification-language/11579-inductive-params.rst4
-rw-r--r--interp/constrintern.ml150
-rw-r--r--interp/constrintern.mli6
-rw-r--r--test-suite/bugs/closed/bug_11585.v3
-rw-r--r--test-suite/bugs/closed/bug_5233.v3
-rw-r--r--test-suite/output/Inductive.out8
-rw-r--r--test-suite/success/InductiveVsImplicitsVsTC.v10
-rw-r--r--vernac/classes.ml3
-rw-r--r--vernac/comAssumption.ml3
-rw-r--r--vernac/comDefinition.ml3
-rw-r--r--vernac/comFixpoint.ml3
-rw-r--r--vernac/comInductive.ml118
-rw-r--r--vernac/comInductive.mli6
-rw-r--r--vernac/comProgramFixpoint.ml4
-rw-r--r--vernac/record.ml54
-rw-r--r--vernac/vernacentries.ml7
16 files changed, 225 insertions, 160 deletions
diff --git a/doc/changelog/02-specification-language/11579-inductive-params.rst b/doc/changelog/02-specification-language/11579-inductive-params.rst
new file mode 100644
index 0000000000..75358ab4ad
--- /dev/null
+++ b/doc/changelog/02-specification-language/11579-inductive-params.rst
@@ -0,0 +1,4 @@
+- **Changed:**
+ Treatment of implicit inductive parameters in inductive declarations is less adhoc.
+ (`#11579 <https://github.com/coq/coq/pull/11579>`_,
+ by Maxime Dénès, Gaëtan Gilbert and Jasper Hugunin).
diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index a071ba7ec9..9a69af0f64 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -57,9 +57,6 @@ type var_internalization_data =
(* type of the "free" variable, for coqdoc, e.g. while typing the
constructor of JMeq, "JMeq" behaves as a variable of type Inductive *)
var_internalization_type *
- (* impargs to automatically add to the variable, e.g. for "JMeq A a B b"
- in implicit mode, this is [A;B] and this adds (A:=A) and (B:=B) *)
- Id.t list *
(* signature of impargs of the variable *)
Impargs.implicit_status list *
(* subscopes of the args of the variable *)
@@ -180,20 +177,9 @@ let parsing_explicit = ref false
let empty_internalization_env = Id.Map.empty
-let compute_explicitable_implicit imps = function
- | Inductive (params,_) ->
- (* In inductive types, the parameters are fixed implicit arguments *)
- let sub_impl,_ = List.chop (List.length params) imps in
- let sub_impl' = List.filter is_status_implicit sub_impl in
- List.map name_of_implicit sub_impl'
- | Recursive | Method | Variable ->
- (* Unable to know in advance what the implicit arguments will be *)
- []
-
let compute_internalization_data env sigma ty typ impl =
let impl = compute_implicits_with_manual env sigma typ (is_implicit_args()) impl in
- let expls_impl = compute_explicitable_implicit impl ty in
- (ty, expls_impl, impl, compute_arguments_scope sigma typ)
+ (ty, impl, compute_arguments_scope sigma typ)
let compute_internalization_env env sigma ?(impls=empty_internalization_env) ty =
List.fold_left3
@@ -355,7 +341,7 @@ let impls_binder_list =
let impls_type_list n ?(args = []) =
let rec aux acc n c = match DAst.get c with
| GProd (na,bk,_,c) -> aux (build_impls n bk na acc) (n+1) c
- | _ -> (Variable,[],List.rev acc,[])
+ | _ -> (Variable,List.rev acc,[])
in aux args n
let impls_term_list n ?(args = []) =
@@ -365,7 +351,7 @@ let impls_term_list n ?(args = []) =
let nb = match fix_kind with |GFix (_, n) -> n | GCoFix n -> n in
let n,acc' = List.fold_left (fun (n,acc) (na, bk, _, _) -> (n+1,build_impls n bk na acc)) (n,acc) args.(nb) in
aux acc' n bds.(nb)
- |_ -> (Variable,[],List.rev acc,[])
+ |_ -> (Variable,List.rev acc,[])
in aux args n
(* Check if in binder "(x1 x2 .. xn : t)", none of x1 .. xn-1 occurs in t *)
@@ -431,12 +417,12 @@ let locate_if_hole ?loc na c = match DAst.get c with
let reset_hidden_inductive_implicit_test env =
{ env with impls = Id.Map.map (function
- | (Inductive (params,_),b,c,d) -> (Inductive (params,false),b,c,d)
+ | (Inductive (params,_),b,c) -> (Inductive (params,false),b,c)
| x -> x) env.impls }
let check_hidden_implicit_parameters ?loc id impls =
if Id.Map.exists (fun _ -> function
- | (Inductive (indparams,check),_,_,_) when check -> Id.List.mem id indparams
+ | (Inductive (indparams,check),_,_) when check -> Id.List.mem id indparams
| _ -> false) impls
then
user_err ?loc (Id.print id ++ strbrk " is already used as name of " ++
@@ -492,7 +478,7 @@ let intern_generalized_binder intern_type ntnvars
let ty' = intern_type {env with ids = ids; unb = true} ty in
let fvs = Implicit_quantifiers.generalizable_vars_of_glob_constr ~bound:ids ~allowed:ids' ty' in
let env' = List.fold_left
- (fun env {loc;v=x} -> push_name_env ntnvars (Variable,[],[],[])(*?*) env (make ?loc @@ Name x))
+ (fun env {loc;v=x} -> push_name_env ntnvars (Variable,[],[])(*?*) env (make ?loc @@ Name x))
env fvs in
let b' = check_implicit_meaningful ?loc b' env in
let bl = List.map
@@ -559,7 +545,7 @@ let intern_cases_pattern_as_binder ?loc ntnvars env p =
user_err ?loc (str "Unsupported nested \"as\" clause.");
il,disjpat
in
- let env = List.fold_right (fun {loc;v=id} env -> push_name_env ntnvars (Variable,[],[],[]) env (make ?loc @@ Name id)) il env in
+ let env = List.fold_right (fun {loc;v=id} env -> push_name_env ntnvars (Variable,[],[]) env (make ?loc @@ Name id)) il env in
let na = alias_of_pat (List.hd disjpat) in
let ienv = Name.fold_right Id.Set.remove na env.ids in
let id = Namegen.next_name_away_with_default "pat" na ienv in
@@ -615,7 +601,7 @@ let intern_generalization intern env ntnvars loc bk ak c =
GLambda (Name id, bk, DAst.make ?loc:loc' @@ GHole (Evar_kinds.BinderType (Name id), IntroAnonymous, None), acc))
in
List.fold_right (fun ({loc;v=id} as lid) (env, acc) ->
- let env' = push_name_env ntnvars (Variable,[],[],[]) env CAst.(make @@ Name id) in
+ let env' = push_name_env ntnvars (Variable,[],[]) env CAst.(make @@ Name id) in
(env', abs lid acc)) fvs (env,c)
in c'
@@ -706,7 +692,7 @@ let traverse_binder intern_pat ntnvars (terms,_,binders,_ as subst) avoid (renam
if onlyident then
(* Do not try to interpret a variable as a constructor *)
let na = out_patvar pat in
- let env = push_name_env ntnvars (Variable,[],[],[]) env (make ?loc:pat.loc na) in
+ let env = push_name_env ntnvars (Variable,[],[]) env (make ?loc:pat.loc na) in
(renaming,env), None, na
else
(* Interpret as a pattern *)
@@ -1031,27 +1017,25 @@ let intern_var env (ltacvars,ntnvars) namedctx loc id us =
if Id.Map.mem id ntnvars then
begin
if not (Id.Map.mem id env.impls) then set_var_scope ?loc id true (env.tmp_scope,env.scopes) ntnvars;
- gvar (loc,id) us, [], [], []
+ gvar (loc,id) us, [], []
end
else
(* Is [id] registered with implicit arguments *)
try
- let ty,expl_impls,impls,argsc = Id.Map.find id env.impls in
- let expl_impls = List.map
- (fun id -> CAst.make ?loc @@ CRef (qualid_of_ident ?loc id,None), Some (make ?loc @@ ExplByName id)) expl_impls in
+ let ty,impls,argsc = Id.Map.find id env.impls in
let tys = string_of_ty ty in
Dumpglob.dump_reference ?loc "<>" (Id.to_string id) tys;
- gvar (loc,id) us, make_implicits_list impls, argsc, expl_impls
+ gvar (loc,id) us, make_implicits_list impls, argsc
with Not_found ->
(* Is [id] bound in current term or is an ltac var bound to constr *)
if Id.Set.mem id env.ids || Id.Set.mem id ltacvars.ltac_vars
then
- gvar (loc,id) us, [], [], []
+ gvar (loc,id) us, [], []
else if Id.equal id ldots_var
(* Is [id] the special variable for recursive notations? *)
then if Id.Map.is_empty ntnvars
then error_ldots_var ?loc
- else gvar (loc,id) us, [], [], []
+ else gvar (loc,id) us, [], []
else if Id.Set.mem id ltacvars.ltac_bound then
(* Is [id] bound to a free name in ltac (this is an ltac error message) *)
user_err ?loc ~hdr:"intern_var"
@@ -1067,17 +1051,17 @@ let intern_var env (ltacvars,ntnvars) namedctx loc id us =
let scopes = find_arguments_scope ref in
Dumpglob.dump_secvar ?loc id; (* this raises Not_found when not a section variable *)
(* Someday we should stop relying on Dumglob raising exceptions *)
- DAst.make ?loc @@ GRef (ref, us), impls, scopes, []
+ DAst.make ?loc @@ GRef (ref, us), impls, scopes
with e when CErrors.noncritical e ->
(* [id] a goal variable *)
- gvar (loc,id) us, [], [], []
+ gvar (loc,id) us, [], []
let find_appl_head_data c =
match DAst.get c with
| GRef (ref,_) ->
let impls = implicits_of_global ref in
let scopes = find_arguments_scope ref in
- c, impls, scopes, []
+ c, impls, scopes
| GApp (r, l) ->
begin match DAst.get r with
| GRef (ref,_) ->
@@ -1085,10 +1069,10 @@ let find_appl_head_data c =
let impls = implicits_of_global ref in
let scopes = find_arguments_scope ref in
c, (if n = 0 then [] else List.map (drop_first_implicits n) impls),
- List.skipn_at_least n scopes,[]
- | _ -> c,[],[],[]
+ List.skipn_at_least n scopes
+ | _ -> c,[],[]
end
- | _ -> c,[],[],[]
+ | _ -> c,[],[]
let error_not_enough_arguments ?loc =
user_err ?loc (str "Abbreviation is not applied enough.")
@@ -1196,13 +1180,12 @@ let intern_applied_reference ~isproj intern env namedctx (_, ntnvars as lvar) us
try
let r, realref, args2 = intern_qualid ~no_secvar:true qid intern env ntnvars us args in
check_applied_projection isproj realref qid;
- let x, imp, scopes, l = find_appl_head_data r in
- (x,imp,scopes,l), args2
+ find_appl_head_data r, args2
with Not_found ->
(* Extra allowance for non globalizing functions *)
if !interning_grammar || env.unb then
(* check_applied_projection ?? *)
- (gvar (loc,qualid_basename qid) us, [], [], []), args
+ (gvar (loc,qualid_basename qid) us, [], []), args
else Nametab.error_global_not_found qid
else
let r,realref,args2 =
@@ -1210,11 +1193,10 @@ let intern_applied_reference ~isproj intern env namedctx (_, ntnvars as lvar) us
with Not_found -> Nametab.error_global_not_found qid
in
check_applied_projection isproj realref qid;
- let x, imp, scopes, l = find_appl_head_data r in
- (x,imp,scopes,l), args2
+ find_appl_head_data r, args2
let interp_reference vars r =
- let (r,_,_,_),_ =
+ let (r,_,_),_ =
intern_applied_reference ~isproj:None (fun _ -> error_not_enough_arguments ?loc:None)
{ids = Id.Set.empty; unb = false ;
tmp_scope = None; scopes = []; impls = empty_internalization_env;
@@ -1882,18 +1864,6 @@ let intern_ind_pattern genv ntnvars scopes pat =
(**********************************************************************)
(* Utilities for application *)
-let merge_impargs l args =
- let test x = function
- | (_, Some {v=y}) -> explicitation_eq x y
- | _ -> false
- in
- List.fold_right (fun a l ->
- match a with
- | (_, Some {v=ExplByName id as x}) when
- List.exists (test x) args -> l
- | _ -> a::l)
- l args
-
let get_implicit_name n imps =
Some (Impargs.name_of_implicit (List.nth imps (n-1)))
@@ -1954,11 +1924,11 @@ let extract_explicit_arg imps args =
let internalize globalenv env pattern_mode (_, ntnvars as lvar) c =
let rec intern env = CAst.with_loc_val (fun ?loc -> function
| CRef (ref,us) ->
- let (c,imp,subscopes,l),_ =
+ let (c,imp,subscopes),_ =
intern_applied_reference ~isproj:None intern env (Environ.named_context_val globalenv)
lvar us [] ref
in
- apply_impargs c env imp subscopes l loc
+ apply_impargs c env imp subscopes [] loc
| CFix ({ CAst.loc = locid; v = iddef}, dl) ->
let lf = List.map (fun ({CAst.v = id},_,_,_,_) -> id) dl in
@@ -2053,8 +2023,8 @@ let internalize globalenv env pattern_mode (_, ntnvars as lvar) c =
| CNotation (_,(InConstrEntrySomeLevel,"( _ )"),([a],[],[],[])) -> intern env a
| CNotation (_,ntn,args) ->
let c = intern_notation intern env ntnvars loc ntn args in
- let x, impl, scopes, l = find_appl_head_data c in
- apply_impargs x env impl scopes l loc
+ let x, impl, scopes = find_appl_head_data c in
+ apply_impargs x env impl scopes [] loc
| CGeneralization (b,a,c) ->
intern_generalization intern env ntnvars loc b a c
| CPrim p ->
@@ -2063,7 +2033,7 @@ let internalize globalenv env pattern_mode (_, ntnvars as lvar) c =
intern {env with tmp_scope = None;
scopes = find_delimiters_scope ?loc key :: env.scopes} e
| CAppExpl ((isproj,ref,us), args) ->
- let (f,_,args_scopes,_),args =
+ let (f,_,args_scopes),args =
let args = List.map (fun a -> (a,None)) args in
intern_applied_reference ~isproj intern env (Environ.named_context_val globalenv)
lvar us args ref
@@ -2074,25 +2044,24 @@ let internalize globalenv env pattern_mode (_, ntnvars as lvar) c =
smart_gapp f loc (intern_args env args_scopes (List.map fst args))
| CApp ((isproj,f), args) ->
- let isproj,f,args = match f.CAst.v with
- (* Compact notations like "t.(f args') args" *)
- | CApp ((Some _ as isproj',f), args') when not (Option.has_some isproj) ->
- isproj',f,args'@args
- (* Don't compact "(f args') args" to resolve implicits separately *)
- | _ -> isproj,f,args in
- let (c,impargs,args_scopes,l),args =
- match f.CAst.v with
- | CRef (ref,us) ->
- intern_applied_reference ~isproj intern env
- (Environ.named_context_val globalenv) lvar us args ref
- | CNotation (_,ntn,ntnargs) ->
- assert (Option.is_empty isproj);
- let c = intern_notation intern env ntnvars loc ntn ntnargs in
- let x, impl, scopes, l = find_appl_head_data c in
- (x,impl,scopes,l), args
- | _ -> assert (Option.is_empty isproj); (intern_no_implicit env f,[],[],[]), args in
- apply_impargs c env impargs args_scopes
- (merge_impargs l args) loc
+ let isproj,f,args = match f.CAst.v with
+ (* Compact notations like "t.(f args') args" *)
+ | CApp ((Some _ as isproj',f), args') when not (Option.has_some isproj) ->
+ isproj',f,args'@args
+ (* Don't compact "(f args') args" to resolve implicits separately *)
+ | _ -> isproj,f,args in
+ let (c,impargs,args_scopes),args =
+ match f.CAst.v with
+ | CRef (ref,us) ->
+ intern_applied_reference ~isproj intern env
+ (Environ.named_context_val globalenv) lvar us args ref
+ | CNotation (_,ntn,ntnargs) ->
+ assert (Option.is_empty isproj);
+ let c = intern_notation intern env ntnvars loc ntn ntnargs in
+ find_appl_head_data c, args
+ | _ -> assert (Option.is_empty isproj); (intern_no_implicit env f,[],[]), args in
+ apply_impargs c env impargs args_scopes
+ args loc
| CRecord fs ->
let st = Evar_kinds.Define (not (Program.get_proofs_transparency ())) in
@@ -2133,7 +2102,7 @@ let internalize globalenv env pattern_mode (_, ntnvars as lvar) c =
List.rev_append match_td matchs)
tms ([],Id.Set.empty,Id.Map.empty,[]) in
let env' = Id.Set.fold
- (fun var bli -> push_name_env ntnvars (Variable,[],[],[]) bli (CAst.make @@ Name var))
+ (fun var bli -> push_name_env ntnvars (Variable,[],[]) bli (CAst.make @@ Name var))
(Id.Set.union ex_ids as_in_vars)
(reset_hidden_inductive_implicit_test (restart_lambda_binders env)) in
(* PatVars before a real pattern do not need to be matched *)
@@ -2170,17 +2139,17 @@ let internalize globalenv env pattern_mode (_, ntnvars as lvar) c =
(* "in" is None so no match to add *)
let ((b',(na',_)),_,_) = intern_case_item env' Id.Set.empty (b,na,None) in
let p' = Option.map (fun u ->
- let env'' = push_name_env ntnvars (Variable,[],[],[]) (reset_hidden_inductive_implicit_test env')
+ let env'' = push_name_env ntnvars (Variable,[],[]) (reset_hidden_inductive_implicit_test env')
(CAst.make na') in
intern_type (slide_binders env'') u) po in
DAst.make ?loc @@
GLetTuple (List.map (fun { CAst.v } -> v) nal, (na', p'), b',
- intern (List.fold_left (push_name_env ntnvars (Variable,[],[],[])) (reset_hidden_inductive_implicit_test env) nal) c)
+ intern (List.fold_left (push_name_env ntnvars (Variable,[],[])) (reset_hidden_inductive_implicit_test env) nal) c)
| CIf (c, (na,po), b1, b2) ->
let env' = reset_tmp_scope env in
let ((c',(na',_)),_,_) = intern_case_item env' Id.Set.empty (c,na,None) in (* no "in" no match to ad too *)
let p' = Option.map (fun p ->
- let env'' = push_name_env ntnvars (Variable,[],[],[]) (reset_hidden_inductive_implicit_test env)
+ let env'' = push_name_env ntnvars (Variable,[],[]) (reset_hidden_inductive_implicit_test env)
(CAst.make na') in
intern_type (slide_binders env'') p) po in
DAst.make ?loc @@
@@ -2478,22 +2447,23 @@ let interp_open_constr ?(expected_type=WithoutTypeConstraint) env sigma c =
(* Not all evars expected to be resolved and computation of implicit args *)
-let interp_constr_evars_gen_impls ?(program_mode=false) env sigma
+let interp_constr_evars_gen_impls ?(flags=Pretyping.all_no_fail_flags) env sigma
?(impls=empty_internalization_env) expected_type c =
let c = intern_gen expected_type ~impls env sigma c in
let imps = Implicit_quantifiers.implicits_of_glob_constr ~with_products:(expected_type == IsType) c in
- let flags = { Pretyping.all_no_fail_flags with program_mode } in
let sigma, c = understand_tcc ~flags env sigma ~expected_type c in
sigma, (c, imps)
-let interp_constr_evars_impls ?program_mode env sigma ?(impls=empty_internalization_env) c =
- interp_constr_evars_gen_impls ?program_mode env sigma ~impls WithoutTypeConstraint c
+let interp_constr_evars_impls ?(program_mode=false) env sigma ?(impls=empty_internalization_env) c =
+ let flags = { Pretyping.all_no_fail_flags with program_mode } in
+ interp_constr_evars_gen_impls ~flags env sigma ~impls WithoutTypeConstraint c
-let interp_casted_constr_evars_impls ?program_mode env evdref ?(impls=empty_internalization_env) c typ =
- interp_constr_evars_gen_impls ?program_mode env evdref ~impls (OfType typ) c
+let interp_casted_constr_evars_impls ?(program_mode=false) env evdref ?(impls=empty_internalization_env) c typ =
+ let flags = { Pretyping.all_no_fail_flags with program_mode } in
+ interp_constr_evars_gen_impls ~flags env evdref ~impls (OfType typ) c
-let interp_type_evars_impls ?program_mode env sigma ?(impls=empty_internalization_env) c =
- interp_constr_evars_gen_impls ?program_mode env sigma ~impls IsType c
+let interp_type_evars_impls ?(flags=Pretyping.all_no_fail_flags) env sigma ?(impls=empty_internalization_env) c =
+ interp_constr_evars_gen_impls ~flags env sigma ~impls IsType c
(* Not all evars expected to be resolved, with side-effect on evars *)
diff --git a/interp/constrintern.mli b/interp/constrintern.mli
index 9d36bf2151..fb1c6684a1 100644
--- a/interp/constrintern.mli
+++ b/interp/constrintern.mli
@@ -48,10 +48,6 @@ type var_internalization_data =
(* type of the "free" variable, for coqdoc, e.g. while typing the
constructor of JMeq, "JMeq" behaves as a variable of type Inductive *)
- Id.t list *
- (* impargs to automatically add to the variable, e.g. for "JMeq A a B b"
- in implicit mode, this is [A;B] and this adds (A:=A) and (B:=B) *)
-
Impargs.implicit_status list * (* signature of impargs of the variable *)
Notation_term.scope_name option list (* subscopes of the args of the variable *)
@@ -132,7 +128,7 @@ val interp_casted_constr_evars_impls : ?program_mode:bool -> env -> evar_map ->
?impls:internalization_env -> constr_expr -> types ->
evar_map * (constr * Impargs.manual_implicits)
-val interp_type_evars_impls : ?program_mode:bool -> env -> evar_map ->
+val interp_type_evars_impls : ?flags:inference_flags -> env -> evar_map ->
?impls:internalization_env -> constr_expr ->
evar_map * (types * Impargs.manual_implicits)
diff --git a/test-suite/bugs/closed/bug_11585.v b/test-suite/bugs/closed/bug_11585.v
new file mode 100644
index 0000000000..6294668323
--- /dev/null
+++ b/test-suite/bugs/closed/bug_11585.v
@@ -0,0 +1,3 @@
+Fail Inductive type {type : Type} : Type := T : type.
+
+Inductive type {type : Type} : Type := T .
diff --git a/test-suite/bugs/closed/bug_5233.v b/test-suite/bugs/closed/bug_5233.v
index 06286c740d..63e33b63f7 100644
--- a/test-suite/bugs/closed/bug_5233.v
+++ b/test-suite/bugs/closed/bug_5233.v
@@ -1,2 +1,5 @@
(* Implicit arguments on type were missing for recursive records *)
Inductive foo {A : Type} : Type := { Foo : foo }.
+
+(* Implicit arguments can be overidden *)
+Inductive bar {A : Type} : Type := { Bar : @bar (A*A) }.
diff --git a/test-suite/output/Inductive.out b/test-suite/output/Inductive.out
index ff2556c5dc..e6c2806433 100644
--- a/test-suite/output/Inductive.out
+++ b/test-suite/output/Inductive.out
@@ -1,6 +1,10 @@
The command has indeed failed with message:
-Last occurrence of "list'" must have "A" as 1st argument in
- "A -> list' A -> list' (A * A)%type".
+In environment
+list' : Set -> Set
+A : Set
+a : A
+l : list' A
+Unable to unify "list' (A * A)%type" with "list' A".
Inductive foo (A : Type) (x : A) (y : A := x) : Prop := Foo : foo A x
Arguments foo _%type_scope
diff --git a/test-suite/success/InductiveVsImplicitsVsTC.v b/test-suite/success/InductiveVsImplicitsVsTC.v
new file mode 100644
index 0000000000..9b787867fc
--- /dev/null
+++ b/test-suite/success/InductiveVsImplicitsVsTC.v
@@ -0,0 +1,10 @@
+Class C := {}.
+
+Definition useC {c:C} := nat.
+
+Inductive foo {a b : C} := CC : useC -> foo.
+(* If TC search runs before parameter unification it will pick the
+ wrong instance for the first parameter.
+
+ useC makes sure we don't completely skip TC search.
+*)
diff --git a/vernac/classes.ml b/vernac/classes.ml
index 6e929de581..3d38713e09 100644
--- a/vernac/classes.ml
+++ b/vernac/classes.ml
@@ -514,7 +514,8 @@ let interp_instance_context ~program_mode env ctx ~generalize pl tclass =
else tclass
in
let sigma, (impls, ((env', ctx), imps)) = interp_context_evars ~program_mode env sigma ctx in
- let sigma, (c', imps') = interp_type_evars_impls ~program_mode ~impls env' sigma tclass in
+ let flags = Pretyping.{ all_no_fail_flags with program_mode } in
+ let sigma, (c', imps') = interp_type_evars_impls ~flags ~impls env' sigma tclass in
let imps = imps @ imps' in
let ctx', c = decompose_prod_assum sigma c' in
let ctx'' = ctx' @ ctx in
diff --git a/vernac/comAssumption.ml b/vernac/comAssumption.ml
index 47ae03e0a3..1e2e2e53e2 100644
--- a/vernac/comAssumption.ml
+++ b/vernac/comAssumption.ml
@@ -70,7 +70,8 @@ let declare_axiom is_coe ~poly ~local ~kind typ (univs, pl) imps nl {CAst.v=name
(gr,inst)
let interp_assumption ~program_mode sigma env impls c =
- let sigma, (ty, impls) = interp_type_evars_impls ~program_mode env sigma ~impls c in
+ let flags = { Pretyping.all_no_fail_flags with program_mode } in
+ let sigma, (ty, impls) = interp_type_evars_impls ~flags env sigma ~impls c in
sigma, (ty, impls)
(* When monomorphic the universe constraints and universe names are
diff --git a/vernac/comDefinition.ml b/vernac/comDefinition.ml
index 8a91e9e63f..66d5a4f7f5 100644
--- a/vernac/comDefinition.ml
+++ b/vernac/comDefinition.ml
@@ -79,6 +79,7 @@ let protect_pattern_in_binder bl c ctypopt =
(bl, c, ctypopt, fun f env evd c -> f env evd c)
let interp_definition ~program_mode pl bl ~poly red_option c ctypopt =
+ let flags = Pretyping.{ all_no_fail_flags with program_mode } in
let env = Global.env() in
(* Explicitly bound universes and constraints *)
let evd, udecl = Constrexpr_ops.interp_univ_decl_opt env pl in
@@ -87,7 +88,7 @@ let interp_definition ~program_mode pl bl ~poly red_option c ctypopt =
let evd, (impls, ((env_bl, ctx), imps1)) = interp_context_evars ~program_mode env evd bl in
(* Build the type *)
let evd, tyopt = Option.fold_left_map
- (interp_type_evars_impls ~program_mode ~impls env_bl)
+ (interp_type_evars_impls ~flags ~impls env_bl)
evd ctypopt
in
(* Build the body, and merge implicits from parameters and from type/body *)
diff --git a/vernac/comFixpoint.ml b/vernac/comFixpoint.ml
index cbf0affc12..e4fa212a23 100644
--- a/vernac/comFixpoint.ml
+++ b/vernac/comFixpoint.ml
@@ -107,7 +107,8 @@ let interp_fix_context ~program_mode ~cofix env sigma fix =
sigma, ((env'', ctx' @ ctx), (impl_env',imps @ imps'), annot)
let interp_fix_ccl ~program_mode sigma impls (env,_) fix =
- let sigma, (c, impl) = interp_type_evars_impls ~program_mode ~impls env sigma fix.Vernacexpr.rtype in
+ let flags = Pretyping.{ all_no_fail_flags with program_mode } in
+ let sigma, (c, impl) = interp_type_evars_impls ~flags ~impls env sigma fix.Vernacexpr.rtype in
let r = Retyping.relevance_of_type env sigma c in
sigma, (c, r, impl)
diff --git a/vernac/comInductive.ml b/vernac/comInductive.ml
index 1f1700b4d6..895561324b 100644
--- a/vernac/comInductive.ml
+++ b/vernac/comInductive.ml
@@ -20,7 +20,6 @@ open Nameops
open Constrexpr
open Constrexpr_ops
open Constrintern
-open Reductionops
open Type_errors
open Pretyping
open Context.Rel.Declaration
@@ -51,20 +50,6 @@ let should_auto_template =
if b then warn_auto_template id;
b
-let rec complete_conclusion a cs = CAst.map_with_loc (fun ?loc -> function
- | CProdN (bl,c) -> CProdN (bl,complete_conclusion a cs c)
- | CLetIn (na,b,t,c) -> CLetIn (na,b,t,complete_conclusion a cs c)
- | CHole (k, _, _) ->
- let (has_no_args,name,params) = a in
- if not has_no_args then
- user_err ?loc
- (strbrk"Cannot infer the non constant arguments of the conclusion of "
- ++ Id.print cs ++ str ".");
- let args = List.map (fun id -> CAst.(make ?loc @@ CRef(qualid_of_ident ?loc id,None))) params in
- CAppExpl ((None,qualid_of_ident ?loc name,None),List.rev args)
- | c -> c
- )
-
let push_types env idl rl tl =
List.fold_left3 (fun env id r t -> EConstr.push_rel (LocalAssum (make_annot (Name id) r,t)) env)
env idl rl tl
@@ -93,10 +78,6 @@ let check_all_names_different indl =
| [] -> ()
| _ -> raise (InductiveError (SameNamesOverlap l))
-let mk_mltype_data sigma env assums arity indname =
- let is_ml_type = is_sort env sigma arity in
- (is_ml_type,indname,assums)
-
(** Make the arity conclusion flexible to avoid generating an upper bound universe now,
only if the universe does not appear anywhere else.
This is really a hack to stay compatible with the semantics of template polymorphic
@@ -145,16 +126,50 @@ let pretype_ind_arity env sigma (loc, c, impls, pseudo_poly) =
in
sigma, (t, Retyping.relevance_of_sort s, concl, impls)
-let interp_cstrs env sigma impls mldata arity ind =
+(* ind_rel is the Rel for this inductive in the context without params.
+ n is how many arguments there are in the constructor. *)
+let model_conclusion env sigma ind_rel params n arity_indices =
+ let model_head = EConstr.mkRel (n + Context.Rel.length params + ind_rel) in
+ let model_params = Context.Rel.to_extended_vect EConstr.mkRel n params in
+ let sigma,model_indices =
+ List.fold_right
+ (fun (_,t) (sigma, subst) ->
+ let t = EConstr.Vars.substl subst (EConstr.Vars.liftn n (List.length subst + 1) (EConstr.Vars.liftn 1 (List.length params + List.length subst + 1) t)) in
+ let sigma, c = Evarutil.new_evar env sigma t in
+ sigma, c::subst)
+ arity_indices (sigma, []) in
+ sigma, EConstr.mkApp (EConstr.mkApp (model_head, model_params), Array.of_list (List.rev model_indices))
+
+let interp_cstrs env (sigma, ind_rel) impls params ind arity =
let cnames,ctyps = List.split ind.ind_lc in
- (* Complete conclusions of constructor types if given in ML-style syntax *)
- let ctyps' = List.map2 (complete_conclusion mldata) cnames ctyps in
+ let arity_indices, cstr_sort = Reductionops.splay_arity env sigma arity in
(* Interpret the constructor types *)
- let sigma, (ctyps'', cimpls) =
+ let interp_cstr sigma ctyp =
+ let flags =
+ Pretyping.{ all_no_fail_flags with
+ use_typeclasses = false;
+ solve_unification_constraints = false }
+ in
+ let sigma, (ctyp, cimpl) = interp_type_evars_impls ~flags env sigma ~impls ctyp in
+ let ctx, concl = Reductionops.splay_prod_assum env sigma ctyp in
+ let concl_env = EConstr.push_rel_context ctx env in
+ let sigma_with_model_evars, model =
+ model_conclusion concl_env sigma ind_rel params (Context.Rel.length ctx) arity_indices
+ in
+ (* unify the expected with the provided conclusion *)
+ let sigma =
+ try Evarconv.unify concl_env sigma_with_model_evars Reduction.CONV concl model
+ with Evarconv.UnableToUnify (sigma,e) ->
+ user_err (Himsg.explain_pretype_error concl_env sigma
+ (Pretype_errors.CannotUnify (concl, model, (Some e))))
+ in
+ sigma, (ctyp, cimpl)
+ in
+ let sigma, (ctyps, cimpls) =
on_snd List.split @@
- List.fold_left_map (fun sigma l ->
- interp_type_evars_impls ~program_mode:false env sigma ~impls l) sigma ctyps' in
- sigma, (cnames, ctyps'', cimpls)
+ List.fold_left_map interp_cstr sigma ctyps
+ in
+ (sigma, pred ind_rel), (cnames, ctyps, cimpls)
let sign_level env evd sign =
fst (List.fold_right
@@ -427,6 +442,30 @@ let interp_params env udecl uparamsl paramsl =
sigma, env_params, (ctx_params, env_uparams, ctx_uparams,
List.map (RelDecl.get_name %> Name.get_id) assums, userimpls, useruimpls, impls, udecl)
+(* When a hole remains for a param, pretend the param is uniform and
+ do the unification.
+ [env_ar_par] is [uparams; inds; params]
+ *)
+let maybe_unify_params_in env_ar_par sigma ~ninds ~nparams c =
+ let is_ind sigma k c = match EConstr.kind sigma c with
+ | Constr.Rel n ->
+ (* env is [uparams; inds; params; k other things] *)
+ n > k + nparams && n <= k + nparams + ninds
+ | _ -> false
+ in
+ let rec aux (env,k as envk) sigma c = match EConstr.kind sigma c with
+ | Constr.App (h,args) when is_ind sigma k h ->
+ Array.fold_left_i (fun i sigma arg ->
+ if i >= nparams || not (EConstr.isEvar sigma arg) then sigma
+ else Evarconv.unify_delay env sigma arg (EConstr.mkRel (k+nparams-i)))
+ sigma args
+ | _ -> Termops.fold_constr_with_full_binders
+ sigma
+ (fun d (env,k) -> EConstr.push_rel d env, k+1)
+ aux envk sigma c
+ in
+ aux (env_ar_par,0) sigma c
+
let interp_mutual_inductive_gen env0 ~template udecl (uparamsl,paramsl,indl) notations ~cumulative ~poly ~private_ind finite =
check_all_names_different indl;
List.iter check_param paramsl;
@@ -466,18 +505,29 @@ let interp_mutual_inductive_gen env0 ~template udecl (uparamsl,paramsl,indl) not
let indimpls = List.map (fun impls -> userimpls @ impls) indimpls in
let impls = compute_internalization_env env_uparams sigma ~impls (Inductive (params,true)) indnames fullarities indimpls in
let ntn_impls = compute_internalization_env env_uparams sigma (Inductive (params,true)) indnames fullarities indimpls in
- let mldatas = List.map2 (mk_mltype_data sigma env_params params) arities indnames in
- let sigma, constructors =
+ let ninds = List.length indl in
+ let (sigma, _), constructors =
Metasyntax.with_syntax_protection (fun () ->
- (* Temporary declaration of notations and scopes *)
- List.iter (Metasyntax.set_notation_for_interpretation env_params ntn_impls) notations;
- (* Interpret the constructor types *)
- List.fold_left3_map (fun sigma -> interp_cstrs env_ar_params sigma impls) sigma mldatas arities indl)
- () in
+ (* Temporary declaration of notations and scopes *)
+ List.iter (Metasyntax.set_notation_for_interpretation env_params ntn_impls) notations;
+ (* Interpret the constructor types *)
+ List.fold_left2_map
+ (fun (sigma, ind_rel) -> interp_cstrs env_ar_params (sigma, ind_rel) impls ctx_params)
+ (sigma, ninds) indl arities)
+ ()
+ in
- (* generalize over the uniform parameters *)
let nparams = Context.Rel.length ctx_params in
+ let sigma =
+ List.fold_left (fun sigma (_,ctyps,_) ->
+ List.fold_left (fun sigma ctyp ->
+ maybe_unify_params_in env_ar_params sigma ~ninds ~nparams ctyp)
+ sigma ctyps)
+ sigma constructors
+ in
+
+ (* generalize over the uniform parameters *)
let nuparams = Context.Rel.length ctx_uparams in
let uargs = Context.Rel.to_extended_vect EConstr.mkRel 0 ctx_uparams in
let uparam_subst =
diff --git a/vernac/comInductive.mli b/vernac/comInductive.mli
index 2b9da1d4e5..984581152a 100644
--- a/vernac/comInductive.mli
+++ b/vernac/comInductive.mli
@@ -88,3 +88,9 @@ val template_polymorphism_candidate
polymorphic. It should have at least one universe in its
monomorphic universe context that can be made parametric in its
conclusion sort, if one is given. *)
+
+val maybe_unify_params_in : Environ.env -> Evd.evar_map -> ninds:int -> nparams:int
+ -> EConstr.t -> Evd.evar_map
+(** [nparams] is the number of parameters which aren't treated as
+ uniform, ie the length of params (including letins) where the env
+ is [uniform params, inductives, params]. *)
diff --git a/vernac/comProgramFixpoint.ml b/vernac/comProgramFixpoint.ml
index 56780d00a6..80e7e6ab96 100644
--- a/vernac/comProgramFixpoint.ml
+++ b/vernac/comProgramFixpoint.ml
@@ -195,12 +195,12 @@ let build_wellfounded (recname,pl,bl,arityc,body) poly r measure notation =
let lift_lets = lift_rel_context 1 letbinders in
let sigma, intern_body =
let ctx = LocalAssum (make_annot (Name recname) Sorts.Relevant, get_type curry_fun) :: binders_rel in
- let (r, l, impls, scopes) =
+ let (r, impls, scopes) =
Constrintern.compute_internalization_data env sigma
Constrintern.Recursive full_arity impls
in
let newimpls = Id.Map.singleton recname
- (r, l, impls @ [Some (ExplByName (Id.of_string "recproof"), Impargs.Manual, (true, false))],
+ (r, impls @ [Some (ExplByName (Id.of_string "recproof"), Impargs.Manual, (true, false))],
scopes @ [None]) in
interp_casted_constr_evars ~program_mode:true (push_rel_context ctx env) sigma
~impls:newimpls body (lift 1 top_arity)
diff --git a/vernac/record.ml b/vernac/record.ml
index d974ead942..785ed89372 100644
--- a/vernac/record.ml
+++ b/vernac/record.ml
@@ -59,26 +59,37 @@ let () =
optread = (fun () -> !typeclasses_unique);
optwrite = (fun b -> typeclasses_unique := b); }
-let interp_fields_evars env sigma impls_env nots l =
- List.fold_left2
- (fun (env, sigma, uimpls, params, impls) no ({CAst.loc;v=i}, b, t) ->
- let sigma, (t', impl) = interp_type_evars_impls ~program_mode:false env sigma ~impls t in
- let r = Retyping.relevance_of_type env sigma t' in
- let sigma, b' =
- Option.cata (fun x -> on_snd (fun x -> Some (fst x)) @@
- interp_casted_constr_evars_impls ~program_mode:false env sigma ~impls x t') (sigma,None) b in
- let impls =
- match i with
- | Anonymous -> impls
- | Name id -> Id.Map.add id (compute_internalization_data env sigma Constrintern.Method t' impl) impls
- in
- let d = match b' with
- | None -> LocalAssum (make_annot i r,t')
- | Some b' -> LocalDef (make_annot i r,b',t')
+let interp_fields_evars env sigma ~ninds ~nparams impls_env nots l =
+ let _, sigma, impls, newfs, _ =
+ List.fold_left2
+ (fun (env, sigma, uimpls, params, impls) no ({CAst.loc;v=i}, b, t) ->
+ let sigma, (t', impl) = interp_type_evars_impls env sigma ~impls t in
+ let r = Retyping.relevance_of_type env sigma t' in
+ let sigma, b' =
+ Option.cata (fun x -> on_snd (fun x -> Some (fst x)) @@
+ interp_casted_constr_evars_impls ~program_mode:false env sigma ~impls x t') (sigma,None) b in
+ let impls =
+ match i with
+ | Anonymous -> impls
+ | Name id -> Id.Map.add id (compute_internalization_data env sigma Constrintern.Method t' impl) impls
+ in
+ let d = match b' with
+ | None -> LocalAssum (make_annot i r,t')
+ | Some b' -> LocalDef (make_annot i r,b',t')
+ in
+ List.iter (Metasyntax.set_notation_for_interpretation env impls) no;
+ (EConstr.push_rel d env, sigma, impl :: uimpls, d::params, impls))
+ (env, sigma, [], [], impls_env) nots l
+ in
+ let _, sigma = Context.Rel.fold_outside ~init:(env,sigma) (fun f (env,sigma) ->
+ let sigma = RelDecl.fold_constr (fun c sigma ->
+ ComInductive.maybe_unify_params_in env sigma ~ninds ~nparams c)
+ f sigma
in
- List.iter (Metasyntax.set_notation_for_interpretation env impls) no;
- (EConstr.push_rel d env, sigma, impl :: uimpls, d::params, impls))
- (env, sigma, [], [], impls_env) nots l
+ EConstr.push_rel f env, sigma)
+ newfs
+ in
+ sigma, (impls, newfs)
let compute_constructor_level evars env l =
List.fold_right (fun d (env, univ) ->
@@ -165,9 +176,10 @@ let typecheck_params_and_fields finite def poly pl ps records =
let imps = List.map (fun _ -> imps) arities in
compute_internalization_env env0 sigma ~impls:impls_env ty ids arities imps
in
+ let ninds = List.length arities in
+ let nparams = List.length newps in
let fold sigma (_, _, nots, fs) arity =
- let _, sigma, impls, newfs, _ = interp_fields_evars env_ar sigma impls_env nots (binders_of_decls fs) in
- (sigma, (impls, newfs))
+ interp_fields_evars env_ar sigma ~ninds ~nparams impls_env nots (binders_of_decls fs)
in
let (sigma, data) = List.fold_left2_map fold sigma records arities in
let sigma =
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index 4806c6bb9c..2e509921c1 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -486,11 +486,14 @@ let program_inference_hook env sigma ev =
let start_lemma_com ~program_mode ~poly ~scope ~kind ?hook thms =
let env0 = Global.env () in
+ let flags = Pretyping.{ all_no_fail_flags with program_mode } in
let decl = fst (List.hd thms) in
let evd, udecl = Constrexpr_ops.interp_univ_decl_opt env0 (snd decl) in
let evd, thms = List.fold_left_map (fun evd ((id, _), (bl, t)) ->
- let evd, (impls, ((env, ctx), imps)) = Constrintern.interp_context_evars ~program_mode env0 evd bl in
- let evd, (t', imps') = Constrintern.interp_type_evars_impls ~program_mode ~impls env evd t in
+ let evd, (impls, ((env, ctx), imps)) =
+ Constrintern.interp_context_evars ~program_mode env0 evd bl
+ in
+ let evd, (t', imps') = Constrintern.interp_type_evars_impls ~flags ~impls env evd t in
let flags = Pretyping.{ all_and_fail_flags with program_mode } in
let inference_hook = if program_mode then Some program_inference_hook else None in
let evd = Pretyping.solve_remaining_evars ?hook:inference_hook flags env evd in
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 19:40:11 +0000