aboutsummaryrefslogtreecommitdiff
path: root/vernac
diff options
context:
space:
mode:
Diffstat (limited to 'vernac')
-rw-r--r--vernac/comFixpoint.ml2
-rw-r--r--vernac/comInductive.ml29
-rw-r--r--vernac/declare.ml38
-rw-r--r--vernac/himsg.ml41
4 files changed, 53 insertions, 57 deletions
diff --git a/vernac/comFixpoint.ml b/vernac/comFixpoint.ml
index 564d24c1ea..78572c6aa6 100644
--- a/vernac/comFixpoint.ml
+++ b/vernac/comFixpoint.ml
@@ -110,7 +110,7 @@ let interp_fix_context ~program_mode ~cofix env sigma fix =
else [], fix.Vernacexpr.binders in
let sigma, (impl_env, ((env', ctx), imps)) = interp_context_evars ~program_mode env sigma before in
let sigma, (impl_env', ((env'', ctx'), imps')) =
- interp_context_evars ~program_mode ~impl_env ~shift:(Context.Rel.nhyps ctx) env' sigma after
+ interp_context_evars ~program_mode ~impl_env env' sigma after
in
let annot = Option.map (fun _ -> List.length (Termops.assums_of_rel_context ctx)) fix.Vernacexpr.rec_order in
sigma, ((env'', ctx' @ ctx), (impl_env',imps @ imps'), annot)
diff --git a/vernac/comInductive.ml b/vernac/comInductive.ml
index 452de69b1d..bb26ce652e 100644
--- a/vernac/comInductive.ml
+++ b/vernac/comInductive.ml
@@ -16,7 +16,6 @@ open Context
open Environ
open Names
open Libnames
-open Nameops
open Constrexpr
open Constrexpr_ops
open Constrintern
@@ -139,7 +138,7 @@ let model_conclusion env sigma ind_rel params n arity_indices =
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 t = EConstr.Vars.substl subst (EConstr.Vars.liftn n (List.length subst + 1) t) in
let sigma, c = Evarutil.new_evar env sigma t in
sigma, c::subst)
arity_indices (sigma, []) in
@@ -443,9 +442,8 @@ let interp_params env udecl uparamsl paramsl =
interp_context_evars ~program_mode:false ~impl_env:uimpls env_uparams sigma paramsl
in
(* Names of parameters as arguments of the inductive type (defs removed) *)
- let assums = List.filter is_local_assum ctx_params in
sigma, env_params, (ctx_params, env_uparams, ctx_uparams,
- List.map (RelDecl.get_name %> Name.get_id) assums, userimpls, useruimpls, impls, udecl)
+ userimpls, useruimpls, impls, udecl)
(* When a hole remains for a param, pretend the param is uniform and
do the unification.
@@ -482,11 +480,12 @@ let interp_mutual_inductive_gen env0 ~template udecl (uparamsl,paramsl,indl) not
then user_err (str "Inductives with uniform parameters may not have attached notations.");
let indnames = List.map (fun ind -> ind.ind_name) indl in
+ let ninds = List.length indl in
(* In case of template polymorphism, we need to compute more constraints *)
let env0 = if poly then env0 else Environ.set_universes_lbound env0 UGraph.Bound.Prop in
- let sigma, env_params, (ctx_params, env_uparams, ctx_uparams, params, userimpls, useruimpls, impls, udecl) =
+ let sigma, env_params, (ctx_params, env_uparams, ctx_uparams, userimpls, useruimpls, impls, udecl) =
interp_params env0 udecl uparamsl paramsl
in
@@ -496,16 +495,17 @@ let interp_mutual_inductive_gen env0 ~template udecl (uparamsl,paramsl,indl) not
let sigma, arities = List.fold_left_map (pretype_ind_arity env_params) sigma arities in
let arities, relevances, arityconcl, indimpls = List.split4 arities in
- let lift1_ctx ctx =
+ let lift_ctx n ctx =
let t = EConstr.it_mkProd_or_LetIn EConstr.mkProp ctx in
- let t = EConstr.Vars.lift 1 t in
+ let t = EConstr.Vars.lift n t in
let ctx, _ = EConstr.decompose_prod_assum sigma t in
ctx
in
- let ctx_params_lifted, fullarities = CList.fold_left_map
- (fun ctx_params c -> lift1_ctx ctx_params, EConstr.it_mkProd_or_LetIn c ctx_params)
- ctx_params
- arities
+ let ctx_params_lifted, fullarities =
+ lift_ctx ninds ctx_params,
+ CList.map_i
+ (fun i c -> EConstr.Vars.lift i (EConstr.it_mkProd_or_LetIn c ctx_params))
+ 0 arities
in
let env_ar = push_types env_uparams indnames relevances fullarities in
let env_ar_params = EConstr.push_rel_context ctx_params_lifted env_ar in
@@ -515,14 +515,15 @@ let interp_mutual_inductive_gen env0 ~template udecl (uparamsl,paramsl,indl) not
let impls = compute_internalization_env env_uparams sigma ~impls Inductive indnames fullarities indimpls in
let ntn_impls = compute_internalization_env env_uparams sigma Inductive indnames fullarities indimpls in
- 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_left2_map
- (fun (sigma, ind_rel) -> interp_cstrs env_ar_params (sigma, ind_rel) impls ctx_params)
+ (fun (sigma, ind_rel) ind arity ->
+ interp_cstrs env_ar_params (sigma, ind_rel) impls ctx_params_lifted
+ ind (EConstr.Vars.liftn ninds (Rel.length ctx_params + 1) arity))
(sigma, ninds) indl arities)
()
in
@@ -540,7 +541,7 @@ let interp_mutual_inductive_gen env0 ~template udecl (uparamsl,paramsl,indl) not
let nuparams = Context.Rel.length ctx_uparams in
let uargs = Context.Rel.to_extended_vect EConstr.mkRel 0 ctx_uparams in
let uparam_subst =
- List.init (List.length indl) EConstr.(fun i -> mkApp (mkRel (i + 1 + nuparams), uargs))
+ List.init ninds EConstr.(fun i -> mkApp (mkRel (i + 1 + nuparams), uargs))
@ List.init nuparams EConstr.(fun i -> mkRel (i + 1)) in
let generalize_constructor c = EConstr.Unsafe.to_constr (EConstr.Vars.substnl uparam_subst nparams c) in
let cimpls = List.map pi3 constructors in
diff --git a/vernac/declare.ml b/vernac/declare.ml
index 099a63cf8f..ae7878b615 100644
--- a/vernac/declare.ml
+++ b/vernac/declare.ml
@@ -725,7 +725,6 @@ module Obligation = struct
; obl_tac : unit Proofview.tactic option }
let set_type ~typ obl = {obl with obl_type = typ}
- let set_body ~body obl = {obl with obl_body = Some body}
end
type obligations = {obls : Obligation.t array; remaining : int}
@@ -2464,32 +2463,25 @@ let add_mutual_definitions l ~pm ~info ?obl_hook ~uctx
in
pm
-let admit_prog ~pm prg =
- let {obls; remaining} = Internal.get_obligations prg in
- let obls = Array.copy obls in
- Array.iteri
- (fun i x ->
- match x.obl_body with
- | None ->
- let x = subst_deps_obl obls x in
- let uctx = Internal.get_uctx prg in
- let univs = UState.univ_entry ~poly:false uctx in
- let kn = declare_constant ~name:x.obl_name ~local:Locality.ImportNeedQualified
- (ParameterEntry (None, (x.obl_type, univs), None)) ~kind:Decls.(IsAssumption Conjectural)
- in
- assumption_message x.obl_name;
- obls.(i) <- Obligation.set_body ~body:(DefinedObl (kn, Univ.Instance.empty)) x
- | Some _ -> ())
- obls;
- Obls_.update_obls ~pm prg obls 0
-
-(* get_any_prog *)
+let rec admit_prog ~pm prg =
+ let {obls} = Internal.get_obligations prg in
+ let is_open _ x = Option.is_empty x.obl_body && List.is_empty (deps_remaining obls x.obl_deps) in
+ let i = match Array.findi is_open obls with
+ | Some i -> i
+ | None -> CErrors.anomaly (Pp.str "Could not find a solvable obligation.")
+ in
+ let proof = solve_obligation prg i None in
+ let pm = Proof.save_admitted ~pm ~proof in
+ match ProgMap.find_opt (Internal.get_name prg) pm with
+ | Some prg -> admit_prog ~pm (CEphemeron.get prg)
+ | None -> pm
+
let rec admit_all_obligations ~pm =
let prg = State.first_pending pm in
match prg with
| None -> pm
| Some prg ->
- let pm, _prog = admit_prog ~pm prg in
+ let pm = admit_prog ~pm prg in
admit_all_obligations ~pm
let admit_obligations ~pm n =
@@ -2497,7 +2489,7 @@ let admit_obligations ~pm n =
| None -> admit_all_obligations ~pm
| Some _ ->
let prg = get_unique_prog ~pm n in
- let pm, _ = admit_prog ~pm prg in
+ let pm = admit_prog ~pm prg in
pm
let next_obligation ~pm n tac =
diff --git a/vernac/himsg.ml b/vernac/himsg.ml
index 762c95fffe..c16eaac516 100644
--- a/vernac/himsg.ml
+++ b/vernac/himsg.ml
@@ -71,6 +71,9 @@ let rec contract3' env sigma a b c = function
| ConversionFailed (env',t1,t2) ->
let (env',t1,t2) = contract2 env' sigma t1 t2 in
contract3 env sigma a b c, ConversionFailed (env',t1,t2)
+ | IncompatibleInstances (env',ev,t1,t2) ->
+ let (env',ev,t1,t2) = contract3 env' sigma (EConstr.mkEvar ev) t1 t2 in
+ contract3 env sigma a b c, IncompatibleInstances (env',EConstr.destEvar sigma ev,t1,t2)
| NotSameArgSize | NotSameHead | NoCanonicalStructure
| MetaOccurInBody _ | InstanceNotSameType _ | ProblemBeyondCapabilities
| UnifUnivInconsistency _ as x -> contract3 env sigma a b c, x
@@ -313,6 +316,13 @@ let explain_unification_error env sigma p1 p2 = function
let t1, t2 = pr_explicit env sigma t1 t2 in
[str "cannot unify " ++ t1 ++ strbrk " and " ++ t2]
else []
+ | IncompatibleInstances (env,ev,t1,t2) ->
+ let env = make_all_name_different env sigma in
+ let ev = pr_leconstr_env env sigma (EConstr.mkEvar ev) in
+ let t1 = Reductionops.nf_betaiota env sigma t1 in
+ let t2 = Reductionops.nf_betaiota env sigma t2 in
+ let t1, t2 = pr_explicit env sigma t1 t2 in
+ [ev ++ strbrk " has otherwise to unify with " ++ t1 ++ str " which is incompatible with " ++ t2]
| MetaOccurInBody evk ->
[str "instance for " ++ quote (pr_existential_key sigma evk) ++
strbrk " refers to a metavariable - please report your example" ++
@@ -689,34 +699,29 @@ let explain_cannot_unify_binding_type env sigma m n =
str "which should be unifiable with" ++ brk(1,1) ++ pn ++ str "."
let explain_cannot_find_well_typed_abstraction env sigma p l e =
- let p = EConstr.to_constr sigma p in
str "Abstracting over the " ++
str (String.plural (List.length l) "term") ++ spc () ++
- hov 0 (pr_enum (fun c -> pr_lconstr_env env sigma (EConstr.to_constr sigma c)) l) ++ spc () ++
- str "leads to a term" ++ spc () ++ pr_ltype_env ~goal_concl_style:true env sigma p ++
+ hov 0 (pr_enum (fun c -> pr_leconstr_env env sigma c) l) ++ spc () ++
+ str "leads to a term" ++ spc () ++ pr_letype_env ~goal_concl_style:true env sigma p ++
spc () ++ str "which is ill-typed." ++
(match e with None -> mt () | Some e -> fnl () ++ str "Reason is: " ++ e)
let explain_wrong_abstraction_type env sigma na abs expected result =
- let abs = EConstr.to_constr sigma abs in
- let expected = EConstr.to_constr sigma expected in
- let result = EConstr.to_constr sigma result in
let ppname = match na with Name id -> Id.print id ++ spc () | _ -> mt () in
str "Cannot instantiate metavariable " ++ ppname ++ strbrk "of type " ++
- pr_lconstr_env env sigma expected ++ strbrk " with abstraction " ++
- pr_lconstr_env env sigma abs ++ strbrk " of incompatible type " ++
- pr_lconstr_env env sigma result ++ str "."
+ pr_leconstr_env env sigma expected ++ strbrk " with abstraction " ++
+ pr_leconstr_env env sigma abs ++ strbrk " of incompatible type " ++
+ pr_leconstr_env env sigma result ++ str "."
let explain_abstraction_over_meta _ m n =
strbrk "Too complex unification problem: cannot find a solution for both " ++
Name.print m ++ spc () ++ str "and " ++ Name.print n ++ str "."
let explain_non_linear_unification env sigma m t =
- let t = EConstr.to_constr sigma t in
strbrk "Cannot unambiguously instantiate " ++
Name.print m ++ str ":" ++
strbrk " which would require to abstract twice on " ++
- pr_lconstr_env env sigma t ++ str "."
+ pr_leconstr_env env sigma t ++ str "."
let explain_unsatisfied_constraints env sigma cst =
strbrk "Unsatisfied constraints: " ++
@@ -803,10 +808,10 @@ let explain_cannot_unify_occurrences env sigma nested ((cl2,pos2),t2) ((cl1,pos1
explain_unification_error env sigma c1 c2 (Some e)
in
str "Found incompatible occurrences of the pattern" ++ str ":" ++
- spc () ++ str "Matched term " ++ pr_lconstr_env env sigma (EConstr.to_constr sigma t2) ++
+ spc () ++ str "Matched term " ++ pr_leconstr_env env sigma t2 ++
strbrk " at position " ++ pr_position (cl2,pos2) ++
strbrk " is not compatible with matched term " ++
- pr_lconstr_env env sigma (EConstr.to_constr sigma t1) ++ strbrk " at position " ++
+ pr_leconstr_env env sigma t1 ++ strbrk " at position " ++
pr_position (cl1,pos1) ++ ppreason ++ str "."
let pr_constraints printenv env sigma evars cstrs =
@@ -1287,9 +1292,8 @@ let explain_recursion_scheme_error env = function
(* Pattern-matching errors *)
let explain_bad_pattern env sigma cstr ty =
- let ty = EConstr.to_constr sigma ty in
let env = make_all_name_different env sigma in
- let pt = pr_lconstr_env env sigma ty in
+ let pt = pr_leconstr_env env sigma ty in
let pc = pr_constructor env cstr in
str "Found the constructor " ++ pc ++ brk(1,1) ++
str "while matching a term of type " ++ pt ++ brk(1,1) ++
@@ -1326,12 +1330,11 @@ let explain_non_exhaustive env pats =
spc () ++ hov 0 (prlist_with_sep pr_comma pr_cases_pattern pats)
let explain_cannot_infer_predicate env sigma typs =
- let inj c = EConstr.to_constr sigma c in
- let typs = Array.map_to_list (fun (c1, c2) -> (inj c1, inj c2)) typs in
+ let typs = Array.to_list typs in
let env = make_all_name_different env sigma in
let pr_branch (cstr,typ) =
- let cstr,_ = decompose_app cstr in
- str "For " ++ pr_lconstr_env env sigma cstr ++ str ": " ++ pr_lconstr_env env sigma typ
+ let cstr,_ = EConstr.decompose_app sigma cstr in
+ str "For " ++ pr_leconstr_env env sigma cstr ++ str ": " ++ pr_leconstr_env env sigma typ
in
str "Unable to unify the types found in the branches:" ++
spc () ++ hov 0 (prlist_with_sep fnl pr_branch typs)
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-04 12:52:27 +0000