diff --git a/test-suite/output/Fixpoint.out b/test-suite/output/Fixpoint.out index 676a805bf1f7..998872105209 100644 --- a/test-suite/output/Fixpoint.out +++ b/test-suite/output/Fixpoint.out @@ -35,3 +35,62 @@ File "./output/Fixpoint.v", line 75, characters 0-48: Warning: Not a fully mutually defined cofixpoint (a2 and a1 are not mutually dependent). [non-full-mutual,fixpoints,default] +File "./output/Fixpoint.v", line 91, characters 2-15: +The command has indeed failed with message: +Recursive definition of foo and bar is ill-formed. +As a mutual fixpoint: +Not enough abstractions in the definition. +The 1st recursive definition is: "?Goal". +The 2nd recursive definition is: "?Goal0". +The condition holds up to here. +File "./output/Fixpoint.v", line 96, characters 6-19: +The command has indeed failed with message: +Recursive definition of foo and bar is ill-formed. +As a mutual fixpoint decreasing on the 1st argument of foo and +1st argument of bar: +Recursive call to bar has principal argument equal to +"0" instead of +a subterm of "n". +As a mutual fixpoint decreasing on the 1st argument of foo and +2nd argument of bar: +Recursive call to bar has principal argument equal to +"0" instead of +a subterm of "n". +As a mutual fixpoint decreasing on the 2nd argument of foo and +1st argument of bar: +Recursive call to bar has principal argument equal to +"0" instead of +a subterm of "m". +As a mutual fixpoint decreasing on the 2nd argument of foo and +2nd argument of bar: +Recursive call to bar has principal argument equal to +"0" instead of a subterm of "m". +The 1st recursive definition is: +"fun n m : nat => + match n with + | 0 => bar 0 0 + | S n0 => (fun n1 : nat => ?Goal0@{n:=n1}) n0 + end". +The 2nd recursive definition is: "fun n m : nat => ?Goal". +The condition holds up to here. +The condition holds up to here. +The condition holds up to here. +The condition holds up to here. +File "./output/Fixpoint.v", line 123, characters 6-19: +The command has indeed failed with message: +Recursive definition of foo' and bar' is ill-formed. +As a mutual fixpoint decreasing on the 1st argument of foo' and +1st argument of bar': +Fixpoints on proof irrelevant inductive types should produce proof irrelevant +values. +As a mutual fixpoint decreasing on the 1st argument of foo' and +2nd argument of bar': +Recursive call to bar' has principal argument equal to +"0" instead of a subterm of "n". +The 1st recursive definition is: +"fun (n : nat) (m : Prop) => + match n with + | 0 => bar' SI 0 + | S n0 => (fun n1 : nat => ?Goal0@{n:=n1}) n0 + end". +The 2nd recursive definition is: "fun (n : STrue) (m : nat) => ?Goal". diff --git a/test-suite/output/Fixpoint.v b/test-suite/output/Fixpoint.v index 26c276b68bca..eb29edbf04d0 100644 --- a/test-suite/output/Fixpoint.v +++ b/test-suite/output/Fixpoint.v @@ -80,3 +80,47 @@ with b2 := b1. *) End Recursivity. + +Module Guard. + +Open Scope nat_scope. + +Lemma foo : nat -> nat -> bool +with bar : nat -> nat -> bool. +Proof. + Fail Guarded. (* not enough abstractions in the definition *) + all:intros n m. + Guarded. + - destruct n as [|n]. + + exact (bar 0 0). + Fail Guarded. (* failure is correct here *) +Abort. + +Lemma foo : nat -> nat -> bool +with bar : nat -> nat -> bool. +Proof. + all:intros n m. + - destruct n as [|n]. + + exact true. + + Guarded. + exact (bar m n). + - Guarded. + destruct m as [|m]. + + exact false. + + exact (foo m n). + Guarded. +Defined. + +Inductive STrue : SProp := SI. + +Lemma foo' : nat -> Prop -> bool +with bar' : STrue -> nat -> bool. +Proof. + all:intros n m. + - destruct n as [|n]. + Guarded. + + exact (bar' SI 0). + Fail Guarded. +Abort. + +End Guard. diff --git a/vernac/comFixpoint.ml b/vernac/comFixpoint.ml index fbc8a8410f51..2068d95993e0 100644 --- a/vernac/comFixpoint.ml +++ b/vernac/comFixpoint.ml @@ -564,20 +564,21 @@ let do_mutually_recursive ?pm ~program_mode ?(use_inference_hook=false) ?scope ? let pm, _ = Declare.Obls.add_definition ~pm ~cinfo ~info ~opaque:false ~body ~uctx ?using obls in Some pm, None | _ -> + let possible_guard = (possible_guard, fixrs) in Some (Declare.Obls.add_mutual_definitions ~pm ~cinfo ~info ~opaque:false ~uctx ~bodies ~possible_guard ?using obls), None) | None -> try let bodies = List.map Option.get bodies in let uctx = Evd.evar_universe_context sigma in (* All bodies are defined *) + let possible_guard = (possible_guard, fixrs) in let _ : GlobRef.t list = - Declare.declare_mutual_definitions ~cinfo ~info ~opaque:false ~uctx - ~possible_guard ~bodies:(bodies,fixrs) ?using () + Declare.declare_mutual_definitions ~cinfo ~info ~opaque:false ~uctx ~possible_guard ~bodies ?using () in None, None with Option.IsNone -> (* At least one undefined body *) Evd.check_univ_decl_early ~poly ~with_obls:false sigma udecl (Option.List.flatten bodies @ fixtypes); - let lemma = Declare.Proof.start_mutual_definitions ~info ~cinfo - ~bodies ~possible_guard ?using sigma in + let possible_guard = (possible_guard, fixrs) in + let lemma = Declare.Proof.start_mutual_definitions ~info ~cinfo ~bodies ~possible_guard ?using sigma in None, Some lemma diff --git a/vernac/declare.ml b/vernac/declare.ml index a5a677b86a5b..bc5462ea405c 100644 --- a/vernac/declare.ml +++ b/vernac/declare.ml @@ -781,60 +781,54 @@ let interp_proof_using_cinfo env evd cinfo using = let f { CInfo.name; typ; _ } = name, [EConstr.of_constr typ] in interp_proof_using_gen f env evd cinfo using -let make_recursive_body env possible_guard rec_declaration = - let indexes = Pretyping.search_guard env possible_guard rec_declaration in - let body = match indexes with - | Some indexes -> Constr.mkFix ((indexes,0), rec_declaration) - | None -> Constr.mkCoFix (0, rec_declaration) in - body, indexes - let gather_mutual_using_data = - List.fold_left2 (fun acc CInfo.{ name; typ; _ } body -> + List.fold_left2 (fun acc CInfo.{ name; typ; _ } (body, _) -> let typ, body = EConstr.(of_constr typ, of_constr body) in (name, [typ; body]) :: acc) [] -let select_body i t = - let open Constr in - match Constr.kind t with - | Fix ((nv,0),decls) -> mkFix ((nv,i),decls) - | CoFix (0,decls) -> mkCoFix (i,decls) - | _ -> assert false - -let make_mutual_bodies env ~typing_flags ~rec_declaration ~possible_guard = +let make_recursive_bodies env ~typing_flags ~possible_guard ~rec_declaration = let env = Environ.update_typing_flags ?typing_flags env in - let body, indexes = make_recursive_body env possible_guard rec_declaration in - let vars = Vars.universes_of_constr body in - let nfix = Array.length (pi1 rec_declaration) in - let fixdecls = List.init nfix (fun i -> select_body i body) in - vars, fixdecls, indexes - -let prepare_recursive_declaration fixitems (fixdefs,fixrs) = - let fixnames = List.map (fun CInfo.{name} -> name) fixitems in - let names = List.map2 (fun CInfo.{name} r -> Context.make_annot (Name name) r) fixitems fixrs in - let fixtypes = List.map (fun CInfo.{typ} -> typ) fixitems in + let indexes = Pretyping.search_guard env possible_guard rec_declaration in + let mkbody i = match indexes with + | Some indexes -> Constr.mkFix ((indexes,i), rec_declaration) + | None -> Constr.mkCoFix (i, rec_declaration) in + List.map_i (fun i typ -> (mkbody i, typ)) 0 (Array.to_list (pi2 rec_declaration)), indexes + +let prepare_recursive_declaration cinfo fixtypes fixrs fixdefs = + let fixnames = List.map (fun CInfo.{name} -> name) cinfo in + let names = List.map2 (fun name r -> Context.make_annot (Name name) r) fixnames fixrs in let defs = List.map (Vars.subst_vars (List.rev fixnames)) fixdefs in (Array.of_list names, Array.of_list fixtypes, Array.of_list defs) +let prepare_recursive_edeclaration sigma cinfo fixtypes fixrs fixdefs = + let fixnames = List.map (fun CInfo.{name} -> name) cinfo in + let names = List.map2 (fun name r -> Context.make_annot (Name name) (EConstr.ERelevance.make r)) fixnames fixrs in + let defs = List.map (EConstr.Vars.subst_vars sigma (List.rev fixnames)) fixdefs in + (Array.of_list names, Array.of_list fixtypes, Array.of_list defs) + let declare_mutual_definitions ~info ~cinfo ~opaque ~uctx ~bodies ~possible_guard ?using () = let { Info.poly; udecl; scope; clearbody; kind; typing_flags; user_warns; ntns; _ } = info in let env = Global.env() in - let rec_declaration = prepare_recursive_declaration cinfo bodies in - let vars, fixdecls, indexes = make_mutual_bodies env ~typing_flags ~rec_declaration ~possible_guard in + let possible_guard, fixrelevances = possible_guard in + let fixtypes = List.map (fun CInfo.{typ} -> typ) cinfo in + let rec_declaration = prepare_recursive_declaration cinfo fixtypes fixrelevances bodies in + let bodies_types, indexes = make_recursive_bodies env ~typing_flags ~rec_declaration ~possible_guard in + let vars = Vars.universes_of_constr (fst (List.hd bodies_types)) in (* All bodies have same vars *) let uctx = UState.restrict uctx vars in let univs = UState.check_univ_decl ~poly uctx udecl in let evd = Evd.from_env env in let using = Option.map (fun using -> - let cinfos = gather_mutual_using_data cinfo fixdecls in + let cinfos = gather_mutual_using_data cinfo bodies_types in let f x = x in interp_proof_using_gen f env evd cinfos using) using in let csts = CList.map2 - (fun CInfo.{ name; typ; impargs } body -> + (fun CInfo.{ name; typ; impargs } (body, _) -> let entry = definition_entry ~opaque ~types:typ ~univs ?using body in declare_entry ~name ~scope ~clearbody ~kind ~impargs ~uctx ~typing_flags ~user_warns entry) - cinfo fixdecls + cinfo bodies_types in let isfix = Option.has_some indexes in let fixnames = List.map (fun { CInfo.name } -> name) cinfo in @@ -976,7 +970,7 @@ module ProgramDecl = struct ; prg_uctx : UState.t ; prg_obligations : obligations ; prg_deps : Id.t list - ; prg_possible_guard : Pretyping.possible_guard option (* None = not recursive *) + ; prg_possible_guard : (Pretyping.possible_guard * Sorts.relevance list) option (* None = not recursive *) ; prg_reduce : constr -> constr } @@ -1356,27 +1350,24 @@ let declare_mutual_definitions ~pm l = let defobl x = let oblsubst = obligation_substitution true x in let subs, typ = subst_prog oblsubst x in - let env = Global.env () in let sigma = Evd.from_ctx x.prg_uctx in - let r = Retyping.relevance_of_type env sigma (EConstr.of_constr typ) in let term = EConstr.of_constr subs in let typ = EConstr.of_constr typ in let term = EConstr.to_constr sigma term in let typ = EConstr.to_constr sigma typ in - let r = EConstr.ERelevance.kind sigma r in - let def = (x.prg_reduce term, r, x.prg_reduce typ, x.prg_cinfo.CInfo.impargs) in + let def = (x.prg_reduce term, x.prg_reduce typ, x.prg_cinfo.CInfo.impargs) in let oblsubst = List.map (fun (id, (_, c)) -> (id, c)) oblsubst in (def, oblsubst) in let defs, obls = List.split (List.map defobl l) in let obls = List.flatten obls in - let fixitems = List.map2 (fun (d, relevance, typ, impargs) name -> CInfo.make ~name ~typ ~impargs ()) defs first.prg_deps in - let fixdefs, fixrs, fixtypes, _ = List.split4 defs in + let fixitems = List.map2 (fun (d, typ, impargs) name -> CInfo.make ~name ~typ ~impargs ()) defs first.prg_deps in + let fixdefs, fixtypes, _ = List.split3 defs in let possible_guard = Option.get first.prg_possible_guard in (* Declare the recursive definitions *) let kns = declare_mutual_definitions ~info:first.prg_info - ~uctx:first.prg_uctx ~bodies:(fixdefs, fixrs) ~possible_guard ~opaque:first.prg_opaque + ~uctx:first.prg_uctx ~bodies:fixdefs ~possible_guard ~opaque:first.prg_opaque ~cinfo:fixitems ?using:first.prg_using () in (* Only for the first constant *) @@ -1548,12 +1539,12 @@ module Proof = struct module Proof_info = struct type t = - { cinfo : Constr.t CInfo.t list + { cinfo : unit CInfo.t list (** cinfo contains each individual constant info in a mutual decl *) ; info : Info.t ; proof_ending : Proof_ending.t CEphemeron.key (* This could be improved and the CEphemeron removed *) - ; possible_guard : Pretyping.possible_guard option (* None = not recursive *) + ; possible_guard : (Pretyping.possible_guard * Sorts.relevance list) option (* None = not recursive *) (** thms and compute guard are specific only to start_definition + regular terminator, so we could make this per-proof kind *) @@ -1616,13 +1607,15 @@ let initialize_named_context_for_proof () = let d = if Decls.variable_opacity id then NamedDecl.drop_body d else d in Environ.push_named_context_val d signv) sign Environ.empty_named_context_val -let start_proof_core ~name ~typ ~pinfo ?(sign=initialize_named_context_for_proof ()) ?using sigma = +let start_proof_core ~name ~pinfo ?using sigma goals = (* In ?sign, we remove the bodies of variables in the named context marked "opaque", this is a hack tho, see #10446, and build_constant_by_tactic uses a different method that would break program_inference_hook *) let { Proof_info.info = { Info.poly; typing_flags; _ }; _ } = pinfo in - let goals = [Global.env_of_context sign, typ] in + let goals = List.map (fun (sign, typ) -> + let sign = match sign with None -> initialize_named_context_for_proof () | Some sign -> sign in + (Global.env_of_context sign, typ)) goals in let proof = Proof.start ~name ~poly ?typing_flags sigma goals in let initial_euctx = Evd.evar_universe_context Proof.((data proof).sigma) in { proof @@ -1638,9 +1631,9 @@ let start_proof_core ~name ~typ ~pinfo ?(sign=initialize_named_context_for_proof let start_core ~info ~cinfo ?proof_ending ?using sigma = let { CInfo.name; typ; _ } = cinfo in check_exists name; - let cinfo = [{ cinfo with CInfo.typ = EConstr.Unsafe.to_constr cinfo.CInfo.typ }] in + let cinfo = [{ cinfo with CInfo.typ = () }] in let pinfo = Proof_info.make ~cinfo ~info ?proof_ending () in - start_proof_core ~name ~typ ~pinfo ?sign:None ?using sigma + start_proof_core ~name ~pinfo ?using sigma [None,typ] let start = start_core ?proof_ending:None @@ -1665,56 +1658,43 @@ let start_equations ~name ~info ~hook ~types sigma goals = let proof_ending = Proof_ending.End_equations {hook; i=name; types; sigma} in start_dependent ~name ~info ~proof_ending goals -let rec_tac_initializer Pretyping.{possibly_cofix; possible_fix_indices} thms = - if possibly_cofix then - match List.map (fun { CInfo.name; typ } -> name, (EConstr.of_constr typ)) thms with - | (id,_)::l -> Tactics.mutual_cofix id l 0 - | _ -> assert false - else - (* nl is set to its maximal possible value for the purpose of mutual_fix; it will then be recomputed at Qed-time *) - let nl = List.map succ (List.map List.last possible_fix_indices) - in match List.map2 (fun { CInfo.name; typ } n -> (name, n, (EConstr.of_constr typ))) thms nl with - | (id,n,_)::l -> Tactics.mutual_fix id n l 0 - | _ -> assert false - let start_definition ~info ~cinfo ?using sigma = let { CInfo.name; typ; args } = cinfo in let init_tac = Tactics.auto_intros_tac args in - let pinfo = Proof_info.make ~cinfo:[cinfo] ~info () in + let pinfo = Proof_info.make ~cinfo:[{cinfo with typ = ()}] ~info () in let env = Global.env () in let using = Option.map (interp_proof_using_cinfo env sigma [cinfo]) using in - let lemma = start_proof_core ~name ~typ:(EConstr.of_constr typ) ~pinfo ?sign:None ?using sigma in + let lemma = start_proof_core ~name ~pinfo ?using sigma [None, EConstr.of_constr typ] in map lemma ~f:(fun p -> pi1 @@ Proof.run_tactic Global.(env ()) init_tac p) -let start_mutual_definitions ~info ~cinfo ?bodies ~possible_guard ?using sigma = +let start_mutual_definitions ~info ~cinfo ~bodies ~possible_guard ?using sigma = let intro_tac { CInfo.args; _ } = Tactics.auto_intros_tac args in + let fixrs = snd possible_guard in let init_tac = - let rec_tac = rec_tac_initializer possible_guard cinfo in - let term_tac = - match bodies with - | None -> - List.map intro_tac cinfo - | Some bodies -> - (* This is the case for hybrid proof mode / definition - fixpoint, where terms for some constants are given with := *) - let tacl = List.map (Option.cata (EConstr.of_constr %> Tactics.exact_no_check) Tacticals.tclIDTAC) bodies in - List.map2 (fun tac thm -> Tacticals.tclTHEN tac (intro_tac thm)) tacl cinfo - in - Tacticals.tclTHENS rec_tac term_tac + (* This is the case for hybrid proof mode / definition + fixpoint, where terms for some constants are given with := *) + let tacl = List.map (Option.cata (EConstr.of_constr %> Tactics.exact_no_check) Tacticals.tclIDTAC) bodies in + List.map2 (fun tac thm -> Tacticals.tclTHEN tac (intro_tac thm)) tacl cinfo in match cinfo with | [] -> CErrors.anomaly (Pp.str "No proof to start.") - | { CInfo.name; typ; _} :: thms -> - let pinfo = Proof_info.make ~cinfo ~info ~possible_guard () in + | { CInfo.name; _} :: _ as thms -> + let pinfo = Proof_info.make ~cinfo:(List.map (fun cinfo -> {cinfo with CInfo.typ = ()}) cinfo) ~info ~possible_guard () in (* start_lemma has the responsibility to add (name, impargs, typ) to thms, once Info.t is more refined this won't be necessary *) - let typ = EConstr.of_constr typ in let env = Global.env () in + let sign = + List.fold_left2 (fun sign CInfo.{name;typ} r -> + let typ = EConstr.of_constr typ in + let r = EConstr.ERelevance.make r in + let decl = Context.Named.Declaration.LocalAssum (Context.make_annot name r, typ) in + EConstr.push_named_context_val decl sign) (initialize_named_context_for_proof ()) cinfo fixrs in let using = Option.map (interp_proof_using_cinfo env sigma cinfo) using in - let lemma = start_proof_core ~name ~typ ~pinfo ?using sigma in + let goals = List.map (function CInfo.{typ} -> (Some sign, EConstr.of_constr typ)) thms in + let lemma = start_proof_core ~name ~pinfo ?using sigma goals in let lemma = map lemma ~f:(fun p -> - pi1 @@ Proof.run_tactic Global.(env ()) init_tac p) in + pi1 @@ Proof.run_tactic Global.(env ()) (Proofview.tclFOCUS 1 (List.length thms) (Proofview.tclDISPATCH init_tac)) p) in let () = (* Temporary declaration of notations for the time of the proofs *) let ntn_env = @@ -1831,7 +1811,7 @@ let () = CErrors.register_handler begin function end (* XXX: This is still separate from close_proof below due to drop_pt in the STM *) -let prepare_proof ?(warn_incomplete=true) { proof } = +let prepare_proof ?(warn_incomplete=true) { proof; pinfo } = let Proof.{name=pid;entry;poly;sigma=evd} = Proof.data proof in let initial_goals = Proofview.initial_goals entry in let () = if not @@ Proof.is_done proof then raise (OpenProof (pid, OpenGoals)) in @@ -1843,8 +1823,7 @@ let prepare_proof ?(warn_incomplete=true) { proof } = let evd = Evd.minimize_universes evd in let to_constr c = match EConstr.to_constr_opt evd c with - | Some p -> - Vars.universes_of_constr p, p + | Some p -> p | None -> let has_given_up = let exception Found in @@ -1871,7 +1850,17 @@ let prepare_proof ?(warn_incomplete=true) { proof } = equations and so far there is no code in the CI that will actually call those and do a side-effect, TTBOMK *) (* EJGA: likely the right solution is to attach side effects to the first constant only? *) - let proofs = List.map (fun (_, body, typ) -> (to_constr body, eff), to_constr typ) initial_goals in + let proofs = List.map (fun (_, body, typ) -> (to_constr body, to_constr typ)) initial_goals in + let proofs = match pinfo.possible_guard with + | None -> proofs + | Some (possible_guard, fixrelevances) -> + let env = Safe_typing.push_private_constants (Global.env()) eff.Evd.seff_private in + let fixbodies, fixtypes = List.split proofs in + let rec_declaration = prepare_recursive_declaration pinfo.cinfo fixtypes fixrelevances fixbodies in + let typing_flags = pinfo.info.typing_flags in + fst (make_recursive_bodies env ~typing_flags ~possible_guard ~rec_declaration) in + let add_univ c = (Vars.universes_of_constr c, c) in + let proofs = List.map (fun (body, typ) -> ((add_univ body, eff), add_univ typ)) proofs in let () = if warn_incomplete then begin if Evd.has_shelved evd then warn_remaining_shelved_goals () @@ -1881,6 +1870,53 @@ let prepare_proof ?(warn_incomplete=true) { proof } = in proofs, Evd.evar_universe_context evd +exception NotGuarded of + Environ.env * Evd.evar_map * + (Environ.env * int * EConstr.t Type_errors.pcofix_guard_error) option * + (Environ.env * int * int list * EConstr.t Type_errors.pfix_guard_error) list * + EConstr.rec_declaration + +let () = CErrors.register_handler (function + | NotGuarded (env, sigma, cofix_err, fix_errs, rec_declaration) -> + Some (Himsg.explain_not_guarded env sigma cofix_err fix_errs rec_declaration) + | _ -> None) + +let control_only_guard { proof; pinfo } = + let { Proof.entry; Proof.sigma; } = Proof.data proof in + let initial_goals = Proofview.initial_goals entry in + let proofs = List.map (fun (_, body, typ) -> Evarutil.(nf_evar sigma body, nf_evar sigma typ)) initial_goals in + let eff = Evd.eval_side_effects sigma in + let env = Safe_typing.push_private_constants (Global.env()) eff.Evd.seff_private in + let open Proof_info in + match pinfo.possible_guard with + | None -> + List.iter (fun (body, _) -> Inductiveops.control_only_guard env sigma body) proofs + | Some (possible_guard, fixrelevances) -> + let fixbodies, fixtypes = List.split proofs in + let rec_declaration = prepare_recursive_edeclaration sigma pinfo.cinfo fixtypes fixrelevances fixbodies in + try + let cofix_error = + if possible_guard.possibly_cofix then + try + Inductiveops.control_only_guard env sigma (EConstr.mkCoFix (0,rec_declaration)); + raise Exit + with Pretype_errors.PretypeError (env, sigma, TypingError (IllFormedRecBody (CoFixGuardError why,lna,i,fixenv,vdefj))) -> + Some (env,i,why) + else None + in + let combinations = List.combinations possible_guard.possible_fix_indices in + let fix_errors = + List.map (fun lv -> + try + Inductiveops.control_only_guard env sigma (EConstr.mkFix ((Array.of_list lv,0),rec_declaration)); + raise Exit + with Pretype_errors.PretypeError (env, sigma, TypingError (IllFormedRecBody (FixGuardError why,lna,i,fixenv,vdefj))) -> + (env,i,lv,why)) + combinations + in + raise (NotGuarded (env, sigma, cofix_error, fix_errors, rec_declaration)) + with Exit -> () + let make_univs_deferred ~poly ~initial_euctx ~uctx ~udecl (used_univs_typ, typ) (used_univs_body, body) eff = let used_univs = Univ.Level.Set.union used_univs_body used_univs_typ in @@ -2008,11 +2044,10 @@ let next = let n = ref 0 in fun () -> incr n; !n let by tac = map_fold ~f:(Proof.solve (Goal_select.SelectNth 1) None tac) let build_constant_by_tactic ~name ?warn_incomplete ~sigma ~sign ~poly (typ : EConstr.t) tac = - let typ_ = EConstr.Unsafe.to_constr typ in - let cinfo = [CInfo.make ~name ~typ:typ_ ()] in + let cinfo = [CInfo.make ~name ~typ:() ()] in let info = Info.make ~poly () in let pinfo = Proof_info.make ~cinfo ~info () in - let pf = start_proof_core ~name ~typ ~pinfo ~sign sigma in + let pf = start_proof_core ~name ~pinfo sigma [Some sign, typ] in let pf, status = by tac pf in let { entries; uctx } = close_proof ?warn_incomplete ~opaque:Vernacexpr.Transparent ~keep_body_ucst_separate:false pf in let { Proof.sigma } = Proof.data pf.proof in @@ -2107,39 +2142,12 @@ module MutualEntry : sig (* Common to all recthms *) : pinfo:Proof_info.t -> uctx:UState.t - -> entry:proof_entry + -> proof_entry list -> Names.GlobRef.t list end = struct - (* XXX: Refactor this with the code in [Declare.declare_possibly_mutual_definitions] *) - let guess_decreasing env possible_guard (body, eff) = - let open Constr in - match Constr.kind body with - | Fix (_,(_,_,fixdefs as fixdecls)) | CoFix (_,(_,_,fixdefs as fixdecls)) -> - let env = Safe_typing.push_private_constants env eff.Evd.seff_private in - let body, _ = make_recursive_body env possible_guard fixdecls in - (body, eff) - | _ -> assert false - - let update_mutual_entry i entry uctx typ = - { entry with - proof_entry_body = ProofEntry.map_entry_body ~f:(fun (body, eff) -> (select_body i body, eff)) entry.proof_entry_body; - proof_entry_type = Some (UState.nf_universes uctx typ) } - - let declare_possibly_mutual_definitions ~pinfo ~uctx ~entry = - let entries = match pinfo.Proof_info.possible_guard with - | None -> - (* Not a recursive statement *) - [entry] - | Some possible_guard -> - (* Try all combinations... not optimal *) - let env = Global.env() in - let typing_flags = pinfo.Proof_info.info.Info.typing_flags in - let env = Environ.update_typing_flags ?typing_flags env in - let entry = ProofEntry.map_proof_entry entry ~f:(guess_decreasing env possible_guard) in - List.map_i (fun i CInfo.{typ} -> update_mutual_entry i entry uctx typ) 0 pinfo.Proof_info.cinfo - in + let declare_possibly_mutual_definitions ~pinfo ~uctx entries = let { Proof_info.info = { Info.hook; scope; clearbody; kind; typing_flags; user_warns; _ } } = pinfo in let refs = List.map2 (fun CInfo.{name; impargs} -> declare_entry ~name ~scope ~clearbody ~kind ?hook ~impargs ~typing_flags ~user_warns ~uctx) pinfo.Proof_info.cinfo entries in @@ -2185,7 +2193,7 @@ let { Goptions.get = get_keep_admitted_vars } = ~value:true () -let compute_proof_using_for_admitted proof typs iproof = +let compute_proof_using_for_admitted pinfo proof typs iproof = if not (get_keep_admitted_vars ()) || not (Lib.sections_are_opened()) then None else match get_used_variables proof with | Some _ as x -> x @@ -2198,6 +2206,12 @@ let compute_proof_using_for_admitted proof typs iproof = (* [pproof] is evar-normalized by [partial_proof]. We don't count variables appearing only in the type of evars. *) let vars = Id.Set.union ids_def ids_typ in + let vars = match pinfo.Proof_info.possible_guard with + | Some _ -> + let recvars = Id.Set.of_list (List.map (fun CInfo.{name} -> name) pinfo.cinfo) in + Id.Set.diff vars recvars + | None -> vars + in Some (Environ.really_needed env vars) let check_type_evars_solved env sigma typ = @@ -2212,7 +2226,7 @@ let finish_admitted ~pm ~pinfo ~uctx ~sec_vars typs = | Proof_ending.End_obligation oinfo -> let declare_fun ~uctx ~mono_uctx_extra typ = List.hd (MutualEntry.declare_possibly_mutual_parameters ~pinfo ~uctx ~sec_vars ~mono_uctx_extra [typ]) in - let typ = Evarutil.nf_evars_universes (Evd.from_ctx uctx) (List.hd pinfo.Proof_info.cinfo).CInfo.typ in + let typ = match typs with [typ] -> typ | _ -> assert false in Obls_.obligation_admitted_terminator ~pm typ oinfo declare_fun sec_vars uctx | _ -> let (_ : 'a list) = MutualEntry.declare_possibly_mutual_parameters ~pinfo ~uctx ~sec_vars typs in @@ -2223,14 +2237,15 @@ let save_admitted ~pm ~proof = let typs = List.map pi3 (Proofview.initial_goals entry) in let iproof = get proof in List.iter (check_type_evars_solved (Global.env()) sigma) typs; - let sec_vars = compute_proof_using_for_admitted proof typs iproof in + let sec_vars = compute_proof_using_for_admitted proof.pinfo proof typs iproof in (* We have the choice of taking CInfo.typ and initial_euctx or or the typs and uctx from the type. By uniformity we would like to do the same as in save_lemma_admitted_delayed, but we would need for that that fixpoints are represented with multi-statements; so we take the initial types *) - let typs = List.map (fun CInfo.{typ} -> typ) proof.pinfo.cinfo in - let uctx = proof.initial_euctx in + let sigma = Evd.minimize_universes sigma in + let typs = List.map (EConstr.to_constr sigma) typs in + let uctx = Evd.evar_universe_context sigma in finish_admitted ~pm ~pinfo:proof.pinfo ~uctx ~sec_vars typs (************************************************************************) @@ -2306,8 +2321,8 @@ let finish_proof ~pm proof_obj proof_info = let open Proof_ending in match CEphemeron.default proof_info.Proof_info.proof_ending Regular with | Regular -> - let entry, uctx = check_single_entry proof_obj "Proof.save" in - pm, MutualEntry.declare_possibly_mutual_definitions ~entry ~uctx ~pinfo:proof_info + let {entries; uctx} = proof_obj in + pm, MutualEntry.declare_possibly_mutual_definitions ~uctx ~pinfo:proof_info entries | End_obligation oinfo -> let entry, uctx = check_single_entry proof_obj "Obligation.save" in Obls_.obligation_terminator ~pm ~entry ~uctx ~oinfo diff --git a/vernac/declare.mli b/vernac/declare.mli index a21de6949df9..a43b1c2cc852 100644 --- a/vernac/declare.mli +++ b/vernac/declare.mli @@ -136,8 +136,8 @@ val declare_mutual_definitions -> cinfo: Constr.t CInfo.t list -> opaque:bool -> uctx:UState.t - -> bodies:(Constr.t list * Sorts.relevance list) - -> possible_guard:Pretyping.possible_guard + -> bodies:Constr.t list + -> possible_guard:Pretyping.possible_guard * Sorts.relevance list -> ?using:Vernacexpr.section_subset_expr -> unit -> Names.GlobRef.t list @@ -216,8 +216,8 @@ module Proof : sig val start_mutual_definitions : info:Info.t -> cinfo:Constr.t CInfo.t list - -> ?bodies:Constr.t option list - -> possible_guard:Pretyping.possible_guard + -> bodies:Constr.t option list + -> possible_guard:(Pretyping.possible_guard * Sorts.relevance list) -> ?using:Vernacexpr.section_subset_expr -> Evd.evar_map -> t @@ -327,6 +327,14 @@ module Proof : sig -> idopt:Names.lident option -> OblState.t + exception NotGuarded of + Environ.env * Evd.evar_map * + (Environ.env * int * EConstr.t Type_errors.pcofix_guard_error) option * + (Environ.env * int * int list * EConstr.t Type_errors.pfix_guard_error) list * + EConstr.rec_declaration + + val control_only_guard : t -> unit + end (** {2 low-level, internal API, avoid using unless you have special needs } *) @@ -559,7 +567,7 @@ val add_mutual_definitions : -> opaque:bool -> uctx:UState.t -> bodies:Constr.t list - -> possible_guard:Pretyping.possible_guard + -> possible_guard:(Pretyping.possible_guard * Sorts.relevance list) -> ?tactic:unit Proofview.tactic -> ?reduce:(Constr.t -> Constr.t) -> ?using:Vernacexpr.section_subset_expr diff --git a/vernac/himsg.ml b/vernac/himsg.ml index 9e115941ee09..35ecb5f0e155 100644 --- a/vernac/himsg.ml +++ b/vernac/himsg.ml @@ -586,6 +586,51 @@ let explain_ill_formed_rec_body env sigma err names i fixenv vdefj = str"Recursive definition is:" ++ spc () ++ pvd ++ str "." with e when CErrors.noncritical e -> mt ()) +let explain_not_guarded env sigma cofix_err fix_errs (names, typs, defs as recdef) = + let nfix = Array.length names in + let lnames = Array.map_to_list binder_name names in + let prt_names = + hov 0 (str "Recursive definition of " ++ pr_enum Name.print lnames) + in + let st = + (match cofix_err with + | None -> mt () + | Some (env, i, err) -> + (if nfix > 1 then str "As a mutual co-fixpoint:" else str "As a co-fixpoint:") + ++ fnl() ++ explain_ill_formed_cofix_body env sigma err) + in + let stl = + if List.exists (fun (env, i, nv, err) -> match err with RecursionOnIllegalTerm _ -> true | _ -> false) fix_errs then + List.map (fun (env, i, nv, err) -> + hov 0 ((if nfix > 1 then str "As a mutual fixpoint" else str "As a fixpoint") + ++ str " decreasing on the " ++ pr_enum (fun (n,na) -> pr_nth (n+1) ++ str " argument of " ++ Name.print na) (List.combine nv lnames) ++ str ":") ++ + fnl() ++ explain_ill_formed_fix_body env sigma names i err ++ str "." ++ fnl ()) + fix_errs + else + match fix_errs with + | [] -> [] + | (env, i, nv, err) :: _ -> + [hov 0 ((if nfix > 1 then str "As a mutual fixpoint" else str "As a fixpoint") ++ str ":") ++ + fnl() ++ explain_ill_formed_fix_body env sigma names i err ++ str "." ++ fnl ()] + + (* A common error independently on the decreasing argument *) + in + let fixenv = EConstr.push_rec_types recdef env in + let st = prlist (fun x -> x) (st::stl) in + prt_names ++ str " is ill-formed." ++ fnl () ++ + pr_ne_context_of (str "In environment") env sigma ++ + st ++ + prvecti_with_sep fnl (fun i v -> + try (* May fail with unresolved globals. *) + let fixenv = make_all_name_different fixenv sigma in + let pvd = pr_leconstr_env fixenv sigma v in + if nfix = 1 then + str "Recursive definition is:" ++ spc () ++ pvd ++ str "." + else + str "The " ++ pr_nth (i+1) ++ str " recursive definition is:" ++ spc () ++ pvd ++ str "." + with e when CErrors.noncritical e -> mt ()) + defs + let explain_ill_typed_rec_body env sigma i names vdefj vargs = let env = make_all_name_different env sigma in let pvd = pr_leconstr_env env sigma vdefj.(i).uj_val in diff --git a/vernac/himsg.mli b/vernac/himsg.mli index f0aa50f22764..555e3334f91d 100644 --- a/vernac/himsg.mli +++ b/vernac/himsg.mli @@ -16,3 +16,8 @@ val explain_type_error : Environ.env -> Evd.evar_map -> Pretype_errors.type_erro val explain_pretype_error : Environ.env -> Evd.evar_map -> Pretype_errors.pretype_error -> Pp.t val explain_refiner_error : Environ.env -> Evd.evar_map -> Logic.refiner_error -> Pp.t + +val explain_not_guarded : Environ.env -> Evd.evar_map -> + (Environ.env * int * EConstr.t Type_errors.pcofix_guard_error) option -> + (Environ.env * int * int list * EConstr.t Type_errors.pfix_guard_error) list -> + EConstr.rec_declaration -> Pp.t diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml index 8f6659abeccf..a55c58e85008 100644 --- a/vernac/vernacentries.ml +++ b/vernac/vernacentries.ml @@ -2210,12 +2210,7 @@ let vernac_show ~pstate = end let vernac_check_guard ~pstate = - let pts = Declare.Proof.get pstate in - let pfterm = List.hd (Proof.partial_proof pts) in - let { Proof.entry; Proof.sigma } = Proof.data pts in - let hyps, _, _ = List.hd (Proofview.initial_goals entry) in - let env = Environ.reset_with_named_context hyps (Global.env ()) in - Inductiveops.control_only_guard env sigma pfterm; + Declare.Proof.control_only_guard pstate; str "The condition holds up to here." let vernac_validate_proof ~pstate =