From e0474577f9b83249d69b0f5b5942d6a6bbb1055b Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Mon, 29 Jun 2020 11:31:09 +0200 Subject: [declare] Generalize type of hooks. This is essential to allow hooks to modify state. --- vernac/declare.ml | 8 +++++--- vernac/declare.mli | 5 ++++- 2 files changed, 9 insertions(+), 4 deletions(-) diff --git a/vernac/declare.ml b/vernac/declare.ml index 85359d5b62..a7da245b0f 100644 --- a/vernac/declare.ml +++ b/vernac/declare.ml @@ -33,11 +33,13 @@ module Hook = struct } end - type t = (S.t -> unit) CEphemeron.key + type 'a g = (S.t -> 'a -> 'a) CEphemeron.key + type t = unit g - let make hook = CEphemeron.create hook + let make_g hook = CEphemeron.create hook + let make (hook : S.t -> unit) : t = CEphemeron.create (fun x () -> hook x) - let call ?hook x = Option.iter (fun hook -> CEphemeron.get hook x) hook + let call ?hook x = Option.iter (fun hook -> CEphemeron.get hook x ()) hook end diff --git a/vernac/declare.mli b/vernac/declare.mli index 4891e66803..e13611a828 100644 --- a/vernac/declare.mli +++ b/vernac/declare.mli @@ -40,7 +40,9 @@ open Names care, as imperative effects may become not supported in the future. *) module Hook : sig - type t + type 'a g + + type t = unit g (** Hooks allow users of the API to perform arbitrary actions at proof/definition saving time. For example, to register a constant @@ -61,6 +63,7 @@ module Hook : sig } end + val make_g : (S.t -> 'a -> 'a) -> 'a g val make : (S.t -> unit) -> t val call : ?hook:t -> S.t -> unit end -- cgit v1.2.3 From 54788df72ce79998ee27db362401a56bda4daceb Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Sun, 15 Mar 2020 17:52:16 -0400 Subject: [obligations] Functionalize Program state In our quest to unify all the declaration paths, an important step is to account for the state pertaining to `Program` declarations. Whereas regular proofs keep are kept in a stack-like structure; obligations for constants defined by `Program` are stored in a global map which is manipulated by almost regular open/close proof primitives. We make this manipulation explicit by handling the program state functionally, in a similar way than we already do for lemmas. This requires to extend the proof DSL a bit; but IMO changes are acceptable given the gain. Most of the PR is routine; only remarkable change is that the hook is called explicitly in `finish_admitted` as it had to learn about the different types of proof_endings. Note that we could have gone deeper and use the type system to refine the core proof type; IMO it is still too preliminary so it is better to do this step as an intermediate one towards a deeper unification. --- coqpp/coqpp_main.ml | 3 + .../11836-ejgallego-obligations+functional.sh | 12 + plugins/funind/functional_principles_proofs.ml | 6 +- plugins/funind/gen_principle.ml | 10 +- plugins/funind/recdef.ml | 18 +- plugins/ltac/g_obligations.mlg | 22 +- vernac/classes.ml | 24 +- vernac/classes.mli | 3 +- vernac/comDefinition.ml | 8 +- vernac/comDefinition.mli | 3 +- vernac/comProgramFixpoint.ml | 29 ++- vernac/comProgramFixpoint.mli | 15 +- vernac/declare.ml | 274 ++++++++++----------- vernac/declare.mli | 58 +++-- vernac/vernacentries.ml | 61 ++--- vernac/vernacextend.ml | 5 +- vernac/vernacextend.mli | 5 +- vernac/vernacinterp.ml | 62 +++-- vernac/vernacstate.ml | 23 +- vernac/vernacstate.mli | 4 +- 20 files changed, 344 insertions(+), 301 deletions(-) create mode 100644 dev/ci/user-overlays/11836-ejgallego-obligations+functional.sh diff --git a/coqpp/coqpp_main.ml b/coqpp/coqpp_main.ml index 39ca5413cc..ffde49f2ac 100644 --- a/coqpp/coqpp_main.ml +++ b/coqpp/coqpp_main.ml @@ -339,6 +339,9 @@ let understand_state = function | "proof" -> "VtModifyProof", false | "proof_opt_query" -> "VtReadProofOpt", false | "proof_query" -> "VtReadProof", false + | "read_program" -> "VtReadProgram", false + | "program" -> "VtModifyProgram", false + | "declare_program" -> "VtDeclareProgram", false | s -> fatal ("unsupported state specifier: " ^ s) let print_body_state state fmt r = diff --git a/dev/ci/user-overlays/11836-ejgallego-obligations+functional.sh b/dev/ci/user-overlays/11836-ejgallego-obligations+functional.sh new file mode 100644 index 0000000000..232ca2bf0d --- /dev/null +++ b/dev/ci/user-overlays/11836-ejgallego-obligations+functional.sh @@ -0,0 +1,12 @@ +if [ "$CI_PULL_REQUEST" = "11836" ] || [ "$CI_BRANCH" = "obligations+functional" ]; then + + equations_CI_REF=obligations+functional + equations_CI_GITURL=https://github.com/ejgallego/Coq-Equations + + paramcoq_CI_REF=obligations+functional + paramcoq_CI_GITURL=https://github.com/ejgallego/paramcoq + + mtac2_CI_REF=obligations+functional + mtac2_CI_GITURL=https://github.com/ejgallego/Mtac2 + +fi diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml index 14d0c04212..b743329e7d 100644 --- a/plugins/funind/functional_principles_proofs.ml +++ b/plugins/funind/functional_principles_proofs.ml @@ -863,8 +863,10 @@ let generate_equation_lemma evd fnames f fun_num nb_params nb_args rec_args_num let lemma, _ = Declare.Proof.by (Proofview.V82.tactic prove_replacement) lemma in - let (_ : _ list) = - Declare.Proof.save ~proof:lemma ~opaque:Vernacexpr.Transparent ~idopt:None + let pm = Declare.OblState.empty in + let _pm, _ = + Declare.Proof.save ~pm ~proof:lemma ~opaque:Vernacexpr.Transparent + ~idopt:None in evd diff --git a/plugins/funind/gen_principle.ml b/plugins/funind/gen_principle.ml index ffce2f8c85..730cf42fe8 100644 --- a/plugins/funind/gen_principle.ml +++ b/plugins/funind/gen_principle.ml @@ -1526,8 +1526,9 @@ let derive_correctness (funs : Constr.pconstant list) (graphs : inductive list) let lemma = fst @@ Declare.Proof.by (Proofview.V82.tactic (proving_tac i)) lemma in - let (_ : GlobRef.t list) = - Declare.Proof.save ~proof:lemma ~opaque:Vernacexpr.Transparent + let pm = Declare.OblState.empty in + let _pm, _ = + Declare.Proof.save ~pm ~proof:lemma ~opaque:Vernacexpr.Transparent ~idopt:None in let finfo = @@ -1598,8 +1599,9 @@ let derive_correctness (funs : Constr.pconstant list) (graphs : inductive list) (proving_tac i))) lemma) in - let (_ : _ list) = - Declare.Proof.save ~proof:lemma ~opaque:Vernacexpr.Transparent + let pm = Declare.OblState.empty in + let _pm, _ = + Declare.Proof.save ~pm ~proof:lemma ~opaque:Vernacexpr.Transparent ~idopt:None in let finfo = diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml index 64f62ba1fb..7b00191026 100644 --- a/plugins/funind/recdef.ml +++ b/plugins/funind/recdef.ml @@ -58,8 +58,10 @@ let declare_fun name kind ?univs value = (Declare.declare_constant ~name ~kind (Declare.DefinitionEntry ce)) let defined lemma = - let (_ : _ list) = - Declare.Proof.save ~proof:lemma ~opaque:Vernacexpr.Transparent ~idopt:None + let pm = Declare.OblState.empty in + let _pm, _ = + Declare.Proof.save ~pm ~proof:lemma ~opaque:Vernacexpr.Transparent + ~idopt:None in () @@ -1502,8 +1504,9 @@ let open_new_goal ~lemma build_proof sigma using_lemmas ref_ goal_name [Hints.Hint_db.empty TransparentState.empty false] ])) in let lemma = build_proof env (Evd.from_env env) start_tac end_tac in - let (_ : _ list) = - Declare.Proof.save ~proof:lemma ~opaque:opacity ~idopt:None + let pm = Declare.OblState.empty in + let _pm, _ = + Declare.Proof.save ~pm ~proof:lemma ~opaque:opacity ~idopt:None in () in @@ -1662,7 +1665,12 @@ let com_eqn uctx nb_arg eq_name functional_ref f_ref terminate_ref in let _ = Flags.silently - (fun () -> Declare.Proof.save ~proof:lemma ~opaque:opacity ~idopt:None) + (fun () -> + let pm = Declare.OblState.empty in + let _pm = + Declare.Proof.save ~pm ~proof:lemma ~opaque:opacity ~idopt:None + in + ()) () in () diff --git a/plugins/ltac/g_obligations.mlg b/plugins/ltac/g_obligations.mlg index 81ee6ed5bb..fa176482bf 100644 --- a/plugins/ltac/g_obligations.mlg +++ b/plugins/ltac/g_obligations.mlg @@ -80,14 +80,14 @@ GRAMMAR EXTEND Gram open Declare.Obls -let obligation obl tac = with_tac (fun t -> obligation obl t) tac -let next_obligation obl tac = with_tac (fun t -> next_obligation obl t) tac +let obligation ~pm obl tac = with_tac (fun t -> obligation ~pm obl t) tac +let next_obligation ~pm obl tac = with_tac (fun t -> next_obligation ~pm obl t) tac let classify_obbl _ = Vernacextend.(VtStartProof (Doesn'tGuaranteeOpacity,[])) } -VERNAC COMMAND EXTEND Obligations CLASSIFIED BY { classify_obbl } STATE open_proof +VERNAC COMMAND EXTEND Obligations CLASSIFIED BY { classify_obbl } STATE declare_program | [ "Obligation" integer(num) "of" ident(name) ":" lglob(t) withtac(tac) ] -> { obligation (num, Some name, Some t) tac } | [ "Obligation" integer(num) "of" ident(name) withtac(tac) ] -> @@ -101,14 +101,14 @@ VERNAC COMMAND EXTEND Obligations CLASSIFIED BY { classify_obbl } STATE open_pro | [ "Next" "Obligation" withtac(tac) ] -> { next_obligation None tac } END -VERNAC COMMAND EXTEND Solve_Obligation CLASSIFIED AS SIDEFF +VERNAC COMMAND EXTEND Solve_Obligation CLASSIFIED AS SIDEFF STATE program | [ "Solve" "Obligation" integer(num) "of" ident(name) "with" tactic(t) ] -> { try_solve_obligation num (Some name) (Some (Tacinterp.interp t)) } | [ "Solve" "Obligation" integer(num) "with" tactic(t) ] -> { try_solve_obligation num None (Some (Tacinterp.interp t)) } END -VERNAC COMMAND EXTEND Solve_Obligations CLASSIFIED AS SIDEFF +VERNAC COMMAND EXTEND Solve_Obligations CLASSIFIED AS SIDEFF STATE program | [ "Solve" "Obligations" "of" ident(name) "with" tactic(t) ] -> { try_solve_obligations (Some name) (Some (Tacinterp.interp t)) } | [ "Solve" "Obligations" "with" tactic(t) ] -> @@ -117,14 +117,14 @@ VERNAC COMMAND EXTEND Solve_Obligations CLASSIFIED AS SIDEFF { try_solve_obligations None None } END -VERNAC COMMAND EXTEND Solve_All_Obligations CLASSIFIED AS SIDEFF +VERNAC COMMAND EXTEND Solve_All_Obligations CLASSIFIED AS SIDEFF STATE program | [ "Solve" "All" "Obligations" "with" tactic(t) ] -> { solve_all_obligations (Some (Tacinterp.interp t)) } | [ "Solve" "All" "Obligations" ] -> { solve_all_obligations None } END -VERNAC COMMAND EXTEND Admit_Obligations CLASSIFIED AS SIDEFF +VERNAC COMMAND EXTEND Admit_Obligations CLASSIFIED AS SIDEFF STATE program | [ "Admit" "Obligations" "of" ident(name) ] -> { admit_obligations (Some name) } | [ "Admit" "Obligations" ] -> { admit_obligations None } END @@ -148,14 +148,14 @@ VERNAC COMMAND EXTEND Show_Solver CLASSIFIED AS QUERY Feedback.msg_notice (str"Program obligation tactic is " ++ print_default_tactic ()) } END -VERNAC COMMAND EXTEND Show_Obligations CLASSIFIED AS QUERY +VERNAC COMMAND EXTEND Show_Obligations CLASSIFIED AS QUERY STATE read_program | [ "Obligations" "of" ident(name) ] -> { show_obligations (Some name) } | [ "Obligations" ] -> { show_obligations None } END -VERNAC COMMAND EXTEND Show_Preterm CLASSIFIED AS QUERY -| [ "Preterm" "of" ident(name) ] -> { Feedback.msg_notice (show_term (Some name)) } -| [ "Preterm" ] -> { Feedback.msg_notice (show_term None) } +VERNAC COMMAND EXTEND Show_Preterm CLASSIFIED AS QUERY STATE read_program +| [ "Preterm" "of" ident(name) ] -> { fun ~pm -> Feedback.msg_notice (show_term ~pm (Some name)) } +| [ "Preterm" ] -> { fun ~pm -> Feedback.msg_notice (show_term ~pm None) } END { diff --git a/vernac/classes.ml b/vernac/classes.ml index ba08aa2b94..f454c389dc 100644 --- a/vernac/classes.ml +++ b/vernac/classes.ml @@ -334,7 +334,7 @@ let do_declare_instance sigma ~global ~poly k u ctx ctx' pri udecl impargs subst Impargs.maybe_declare_manual_implicits false cst impargs; instance_hook pri global cst -let declare_instance_program env sigma ~global ~poly name pri impargs udecl term termtype = +let declare_instance_program pm env sigma ~global ~poly name pri impargs udecl term termtype = let hook { Declare.Hook.S.scope; dref; _ } = let cst = match dref with GlobRef.ConstRef kn -> kn | _ -> assert false in let pri = intern_info pri in @@ -349,9 +349,9 @@ let declare_instance_program env sigma ~global ~poly name pri impargs udecl term Decls.IsDefinition Decls.Instance in let cinfo = Declare.CInfo.make ~name ~typ ~impargs () in let info = Declare.Info.make ~udecl ~scope ~poly ~kind ~hook () in - let _ : Declare.Obls.progress = - Declare.Obls.add_definition ~cinfo ~info ~term ~uctx obls - in () + let pm, _ = + Declare.Obls.add_definition ~pm ~cinfo ~info ~term ~uctx obls + in pm let declare_instance_open sigma ?hook ~tac ~global ~poly id pri impargs udecl ids term termtype = (* spiwack: it is hard to reorder the actions to do @@ -493,7 +493,7 @@ let do_instance env env' sigma ?hook ~global ~poly cty k u ctx ctx' pri decl imp Pretyping.check_evars_are_solved ~program_mode:false env sigma; declare_instance_constant pri global imps ?hook id decl poly sigma term termtype -let do_instance_program env env' sigma ?hook ~global ~poly cty k u ctx ctx' pri decl imps subst id opt_props = +let do_instance_program ~pm env env' sigma ?hook ~global ~poly cty k u ctx ctx' pri decl imps subst id opt_props = let term, termtype, sigma = match opt_props with | Some props -> @@ -506,9 +506,10 @@ let do_instance_program env env' sigma ?hook ~global ~poly cty k u ctx ctx' pri term, termtype, sigma in let termtype, sigma = do_instance_resolve_TC termtype sigma env in if not (Evd.has_undefined sigma) && not (Option.is_empty opt_props) then - declare_instance_constant pri global imps ?hook id decl poly sigma term termtype + let () = declare_instance_constant pri global imps ?hook id decl poly sigma term termtype in + pm else - declare_instance_program env sigma ~global ~poly id pri imps decl term termtype + declare_instance_program pm env sigma ~global ~poly id pri imps decl term termtype let interp_instance_context ~program_mode env ctx ~generalize pl tclass = let sigma, decl = Constrexpr_ops.interp_univ_decl_opt env pl in @@ -564,15 +565,16 @@ let new_instance_interactive ?(global=false) id, do_instance_interactive env env' sigma ?hook ~tac ~global ~poly cty k u ctx ctx' pri decl imps subst id opt_props -let new_instance_program ?(global=false) +let new_instance_program ?(global=false) ~pm ~poly instid ctx cl opt_props ?(generalize=true) ?hook pri = let env = Global.env() in let id, env', sigma, k, u, cty, ctx', ctx, imps, subst, decl = new_instance_common ~program_mode:true ~generalize env instid ctx cl in - do_instance_program env env' sigma ?hook ~global ~poly - cty k u ctx ctx' pri decl imps subst id opt_props; - id + let pm = + do_instance_program ~pm env env' sigma ?hook ~global ~poly + cty k u ctx ctx' pri decl imps subst id opt_props in + pm, id let new_instance ?(global=false) ~poly instid ctx cl props diff --git a/vernac/classes.mli b/vernac/classes.mli index 07695b5bef..e1816fb138 100644 --- a/vernac/classes.mli +++ b/vernac/classes.mli @@ -52,6 +52,7 @@ val new_instance val new_instance_program : ?global:bool (** Not global by default. *) + -> pm:Declare.OblState.t -> poly:bool -> name_decl -> local_binder_expr list @@ -60,7 +61,7 @@ val new_instance_program -> ?generalize:bool -> ?hook:(GlobRef.t -> unit) -> Vernacexpr.hint_info_expr - -> Id.t + -> Declare.OblState.t * Id.t val declare_new_instance : ?global:bool (** Not global by default. *) diff --git a/vernac/comDefinition.ml b/vernac/comDefinition.ml index 5ee847a17e..37b7106856 100644 --- a/vernac/comDefinition.ml +++ b/vernac/comDefinition.ml @@ -125,14 +125,14 @@ let do_definition ?hook ~name ~scope ~poly ~kind udecl bl red_option c ctypopt = Declare.declare_definition ~info ~cinfo ~opaque:false ~body evd in () -let do_definition_program ?hook ~name ~scope ~poly ~kind udecl bl red_option c ctypopt = +let do_definition_program ?hook ~pm ~name ~scope ~poly ~kind udecl bl red_option c ctypopt = let program_mode = true in let (body, types), evd, udecl, impargs = interp_definition ~program_mode udecl bl ~poly red_option c ctypopt in let term, typ, uctx, obls = Declare.Obls.prepare_obligation ~name ~body ~types evd in - let _ : Declare.Obls.progress = + let pm, _ = let cinfo = Declare.CInfo.make ~name ~typ ~impargs () in let info = Declare.Info.make ~udecl ~scope ~poly ~kind ?hook () in - Declare.Obls.add_definition ~cinfo ~info ~term ~uctx obls - in () + Declare.Obls.add_definition ~pm ~cinfo ~info ~term ~uctx obls + in pm diff --git a/vernac/comDefinition.mli b/vernac/comDefinition.mli index e3417d0062..d95e64a85f 100644 --- a/vernac/comDefinition.mli +++ b/vernac/comDefinition.mli @@ -29,6 +29,7 @@ val do_definition val do_definition_program : ?hook:Declare.Hook.t + -> pm:Declare.OblState.t -> name:Id.t -> scope:Locality.locality -> poly:bool @@ -38,4 +39,4 @@ val do_definition_program -> red_expr option -> constr_expr -> constr_expr option - -> unit + -> Declare.OblState.t diff --git a/vernac/comProgramFixpoint.ml b/vernac/comProgramFixpoint.ml index 37615fa09c..55901fd604 100644 --- a/vernac/comProgramFixpoint.ml +++ b/vernac/comProgramFixpoint.ml @@ -109,7 +109,7 @@ let telescope env sigma l = let nf_evar_context sigma ctx = List.map (map_constr (fun c -> Evarutil.nf_evar sigma c)) ctx -let build_wellfounded (recname,pl,bl,arityc,body) poly r measure notation = +let build_wellfounded pm (recname,pl,bl,arityc,body) poly r measure notation = let open EConstr in let open Vars in let lift_rel_context n l = Termops.map_rel_context_with_binders (liftn n) l in @@ -262,9 +262,9 @@ let build_wellfounded (recname,pl,bl,arityc,body) poly r measure notation = let uctx = Evd.evar_universe_context sigma in let cinfo = Declare.CInfo.make ~name:recname ~typ:evars_typ () in let info = Declare.Info.make ~udecl ~poly ~hook () in - let _ : Declare.Obls.progress = - Declare.Obls.add_definition ~cinfo ~info ~term:evars_def ~uctx evars in - () + let pm, _ = + Declare.Obls.add_definition ~pm ~cinfo ~info ~term:evars_def ~uctx evars in + pm let out_def = function | Some def -> def @@ -275,7 +275,7 @@ let collect_evars_of_term evd c ty = Evar.Set.fold (fun ev acc -> Evd.add acc ev (Evd.find_undefined evd ev)) evars (Evd.from_ctx (Evd.evar_universe_context evd)) -let do_program_recursive ~scope ~poly fixkind fixl = +let do_program_recursive ~pm ~scope ~poly fixkind fixl = let cofix = fixkind = Declare.Obls.IsCoFixpoint in let (env, rec_sign, udecl, evd), fix, info = interp_recursive ~cofix ~program_mode:true fixl @@ -323,15 +323,15 @@ let do_program_recursive ~scope ~poly fixkind fixl = in let ntns = List.map_append (fun { Vernacexpr.notations } -> notations ) fixl in let info = Declare.Info.make ~poly ~scope ~kind ~udecl () in - Declare.Obls.add_mutual_definitions defs ~info ~uctx ~ntns fixkind + Declare.Obls.add_mutual_definitions ~pm defs ~info ~uctx ~ntns fixkind -let do_fixpoint ~scope ~poly l = +let do_fixpoint ~pm ~scope ~poly l = let g = List.map (fun { Vernacexpr.rec_order } -> rec_order) l in match g, l with | [Some { CAst.v = CWfRec (n,r) }], [ Vernacexpr.{fname={CAst.v=id}; univs; binders; rtype; body_def; notations} ] -> let recarg = mkIdentC n.CAst.v in - build_wellfounded (id, univs, binders, rtype, out_def body_def) poly r recarg notations + build_wellfounded pm (id, univs, binders, rtype, out_def body_def) poly r recarg notations | [Some { CAst.v = CMeasureRec (n, m, r) }], [Vernacexpr.{fname={CAst.v=id}; univs; binders; rtype; body_def; notations }] -> @@ -344,7 +344,7 @@ let do_fixpoint ~scope ~poly l = user_err Pp.(str"Measure takes only two arguments in Program Fixpoint.") | _, _ -> r in - build_wellfounded (id, univs, binders, rtype, out_def body_def) poly + build_wellfounded pm (id, univs, binders, rtype, out_def body_def) poly (Option.default (CAst.make @@ CRef (lt_ref,None)) r) m notations | _, _ when List.for_all (fun ro -> match ro with None | Some { CAst.v = CStructRec _} -> true | _ -> false) g -> @@ -352,12 +352,11 @@ let do_fixpoint ~scope ~poly l = Vernacexpr.(ComFixpoint.adjust_rec_order ~structonly:true fix.binders fix.rec_order)) l in let fixkind = Declare.Obls.IsFixpoint annots in let l = List.map2 (fun fix rec_order -> { fix with Vernacexpr.rec_order }) l annots in - do_program_recursive ~scope ~poly fixkind l - + do_program_recursive ~pm ~scope ~poly fixkind l | _, _ -> - user_err ~hdr:"do_fixpoint" - (str "Well-founded fixpoints not allowed in mutually recursive blocks") + CErrors.user_err ~hdr:"do_fixpoint" + (str "Well-founded fixpoints not allowed in mutually recursive blocks") -let do_cofixpoint ~scope ~poly fixl = +let do_cofixpoint ~pm ~scope ~poly fixl = let fixl = List.map (fun fix -> { fix with Vernacexpr.rec_order = None }) fixl in - do_program_recursive ~scope ~poly Declare.Obls.IsCoFixpoint fixl + do_program_recursive ~pm ~scope ~poly Declare.Obls.IsCoFixpoint fixl diff --git a/vernac/comProgramFixpoint.mli b/vernac/comProgramFixpoint.mli index e39f62c348..7935cf27fb 100644 --- a/vernac/comProgramFixpoint.mli +++ b/vernac/comProgramFixpoint.mli @@ -11,11 +11,16 @@ open Vernacexpr (** Special Fixpoint handling when command is activated. *) - val do_fixpoint : - (* When [false], assume guarded. *) - scope:Locality.locality -> poly:bool -> fixpoint_expr list -> unit + pm:Declare.OblState.t + -> scope:Locality.locality + -> poly:bool + -> fixpoint_expr list + -> Declare.OblState.t val do_cofixpoint : - (* When [false], assume guarded. *) - scope:Locality.locality -> poly:bool -> cofixpoint_expr list -> unit + pm:Declare.OblState.t + -> scope:Locality.locality + -> poly:bool + -> cofixpoint_expr list + -> Declare.OblState.t diff --git a/vernac/declare.ml b/vernac/declare.ml index a7da245b0f..fa1bf361fb 100644 --- a/vernac/declare.ml +++ b/vernac/declare.ml @@ -685,14 +685,6 @@ let prepare_parameter ~poly ~udecl ~types sigma = type progress = Remain of int | Dependent | Defined of GlobRef.t -type obligation_resolver = - Id.t option - -> Int.Set.t - -> unit Proofview.tactic option - -> progress - -type obligation_qed_info = {name : Id.t; num : int; auto : obligation_resolver} - module Obls_ = struct open Constr @@ -925,11 +917,11 @@ let err_not_transp () = module ProgMap = Id.Map -module StateFunctional = struct +module State = struct type t = ProgramDecl.t CEphemeron.key ProgMap.t - let _empty = ProgMap.empty + let empty = ProgMap.empty let pending pm = ProgMap.filter @@ -967,30 +959,12 @@ module StateFunctional = struct let find m t = ProgMap.find_opt t m |> Option.map CEphemeron.get end -module State = struct - - type t = StateFunctional.t - - open StateFunctional - - let prg_ref, prg_tag = - Summary.ref_tag ProgMap.empty ~name:"program-tcc-table" - - let first_pending () = first_pending !prg_ref - let get_unique_open_prog id = get_unique_open_prog !prg_ref id - let add id prg = prg_ref := add !prg_ref id prg - let fold ~f ~init = fold !prg_ref ~f ~init - let all () = all !prg_ref - let find id = find !prg_ref id - -end - (* In all cases, the use of the map is read-only so we don't expose the ref *) let map_keys m = ProgMap.fold (fun k _ l -> k :: l) m [] -let check_solved_obligations ~what_for : unit = - if not (ProgMap.is_empty !State.prg_ref) then - let keys = map_keys !State.prg_ref in +let check_solved_obligations ~pm ~what_for : unit = + if not (ProgMap.is_empty pm) then + let keys = map_keys pm in let have_string = if Int.equal (List.length keys) 1 then " has " else " have " in CErrors.user_err ~hdr:"Program" Pp.( @@ -1086,7 +1060,7 @@ let subst_prog subst prg = ( Vars.replace_vars subst' prg.prg_body , Vars.replace_vars subst' (* Termops.refresh_universes *) prg.prg_cinfo.CInfo.typ ) -let declare_definition prg = +let declare_definition ~pm prg = let varsubst = obligation_substitution true prg in let sigma = Evd.from_ctx prg.prg_uctx in let body, types = subst_prog varsubst prg in @@ -1096,9 +1070,8 @@ let declare_definition prg = let obls = List.map (fun (id, (_, c)) -> (id, c)) varsubst in (* XXX: This is doing normalization twice *) let kn = declare_definition_core ~cinfo ~info ~obls ~body ~opaque sigma in - let pm = progmap_remove !State.prg_ref prg in - State.prg_ref := pm; - kn + let pm = progmap_remove pm prg in + pm, kn let rec lam_index n t acc = match Constr.kind t with @@ -1119,7 +1092,7 @@ let compute_possible_guardness_evidences n fixbody fixtype = let ctx = fst (Term.decompose_prod_n_assum m fixtype) in List.map_i (fun i _ -> i) 0 ctx -let declare_mutual_definition l = +let declare_mutual_definition ~pm l = let len = List.length l in let first = List.hd l in let defobl x = @@ -1185,32 +1158,29 @@ let declare_mutual_definition l = let dref = List.hd kns in Hook.( call ?hook:first.prg_info.Info.hook {S.uctx = first.prg_uctx; obls; scope; dref}); - let pm = List.fold_left progmap_remove !State.prg_ref l in - State.prg_ref := pm; - dref + let pm = List.fold_left progmap_remove pm l in + pm, dref -let update_obls prg obls rem = +let update_obls ~pm prg obls rem = let prg_obligations = {obls; remaining = rem} in let prg' = {prg with prg_obligations} in - let pm = progmap_replace prg' !State.prg_ref in - State.prg_ref := pm; + let pm = progmap_replace prg' pm in obligations_message rem; - if rem > 0 then Remain rem + if rem > 0 then pm, Remain rem else match prg'.prg_deps with | [] -> - let kn = declare_definition prg' in - let pm = progmap_remove !State.prg_ref prg' in - State.prg_ref := pm; - Defined kn + let pm, kn = declare_definition ~pm prg' in + let pm = progmap_remove pm prg' in + pm, Defined kn | l -> let progs = List.map (fun x -> CEphemeron.get (ProgMap.find x pm)) prg'.prg_deps in if List.for_all (fun x -> obligations_solved x) progs then - let kn = declare_mutual_definition progs in - Defined kn - else Dependent + let pm, kn = declare_mutual_definition ~pm progs in + pm, Defined kn + else pm, Dependent let dependencies obls n = let res = ref Int.Set.empty in @@ -1221,23 +1191,32 @@ let dependencies obls n = obls; !res -let update_program_decl_on_defined prg obls num obl ~uctx rem ~auto = +let update_program_decl_on_defined ~pm prg obls num obl ~uctx rem ~auto = let obls = Array.copy obls in let () = obls.(num) <- obl in let prg = {prg with prg_uctx = uctx} in - let _progress = update_obls prg obls (pred rem) in - let () = + let pm, _progress = update_obls ~pm prg obls (pred rem) in + let pm = if pred rem > 0 then let deps = dependencies obls num in if not (Int.Set.is_empty deps) then - let _progress = auto (Some prg.prg_cinfo.CInfo.name) deps None in - () - else () - else () + let pm, _progress = auto ~pm (Some prg.prg_cinfo.CInfo.name) deps None in + pm + else pm + else pm in - () + pm + +type obligation_resolver = + pm:State.t + -> Id.t option + -> Int.Set.t + -> unit Proofview.tactic option + -> State.t * progress -let obligation_terminator ~entry ~uctx ~oinfo:{name; num; auto} = +type obligation_qed_info = {name : Id.t; num : int; auto : obligation_resolver} + +let obligation_terminator ~pm ~entry ~uctx ~oinfo:{name; num; auto} = let env = Global.env () in let ty = entry.proof_entry_type in let body, uctx = inline_private_constants ~uctx env entry in @@ -1245,7 +1224,7 @@ let obligation_terminator ~entry ~uctx ~oinfo:{name; num; auto} = Inductiveops.control_only_guard (Global.env ()) sigma (EConstr.of_constr body); (* Declare the obligation ourselves and drop the hook *) - let prg = Option.get (State.find name) in + let prg = Option.get (State.find pm name) in let {obls; remaining = rem} = prg.prg_obligations in let obl = obls.(num) in let status = @@ -1276,16 +1255,17 @@ let obligation_terminator ~entry ~uctx ~oinfo:{name; num; auto} = UState.from_env (Global.env ()) else uctx in - update_program_decl_on_defined prg obls num obl ~uctx:prg_ctx rem ~auto; - cst + let pm = + update_program_decl_on_defined ~pm prg obls num obl ~uctx:prg_ctx rem ~auto in + pm, cst (* Similar to the terminator but for the admitted path; this assumes the admitted constant was already declared. FIXME: There is duplication of this code with obligation_terminator and Obligations.admit_obligations *) -let obligation_admitted_terminator {name; num; auto} ctx' dref = - let prg = Option.get (State.find name) in +let obligation_admitted_terminator ~pm {name; num; auto} ctx' dref = + let prg = Option.get (State.find pm name) in let {obls; remaining = rem} = prg.prg_obligations in let obl = obls.(num) in let cst = match dref with GlobRef.ConstRef cst -> cst | _ -> assert false in @@ -1310,7 +1290,7 @@ let obligation_admitted_terminator {name; num; auto} ctx' dref = in let obl = {obl with obl_body = Some (DefinedObl (cst, inst))} in let () = if transparent then add_hint true prg cst in - update_program_decl_on_defined prg obls num obl ~uctx:ctx' rem ~auto + update_program_decl_on_defined ~pm prg obls num obl ~uctx:ctx' rem ~auto end @@ -1324,7 +1304,7 @@ module Proof_ending = struct type t = | Regular - | End_obligation of obligation_qed_info + | End_obligation of Obls_.obligation_qed_info | End_derive of { f : Id.t; name : Id.t } | End_equations of { hook : Constant.t list -> Evd.evar_map -> unit @@ -1953,15 +1933,15 @@ let compute_proof_using_for_admitted proof typ pproofs = Some (Environ.really_needed env (Id.Set.union ids_typ ids_def)) | _ -> None -let finish_admitted ~pinfo ~uctx pe = +let finish_admitted ~pm ~pinfo ~uctx pe = let cst = MutualEntry.declare_variable ~pinfo ~uctx pe in (* If the constant was an obligation we need to update the program map *) match CEphemeron.get pinfo.Proof_info.proof_ending with | Proof_ending.End_obligation oinfo -> - Obls_.obligation_admitted_terminator oinfo uctx (List.hd cst) - | _ -> () + Obls_.obligation_admitted_terminator ~pm oinfo uctx (List.hd cst) + | _ -> pm -let save_admitted ~proof = +let save_admitted ~pm ~proof = let udecl = get_universe_decl proof in let Proof.{ poly; entry } = Proof.data (get proof) in let typ = match Proofview.initial_goals entry with @@ -1974,7 +1954,7 @@ let save_admitted ~proof = let sec_vars = compute_proof_using_for_admitted proof typ pproofs in let uctx = get_initial_euctx proof in let univs = UState.check_univ_decl ~poly uctx udecl in - finish_admitted ~pinfo:proof.pinfo ~uctx (sec_vars, (typ, univs), None) + finish_admitted ~pm ~pinfo:proof.pinfo ~uctx (sec_vars, (typ, univs), None) (************************************************************************) (* Saving a lemma-like constant *) @@ -2041,20 +2021,20 @@ let check_single_entry { entries; uctx } label = | _ -> CErrors.anomaly ~label Pp.(str "close_proof returned more than one proof term") -let finalize_proof proof_obj proof_info = +let finalize_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 - MutualEntry.declare_mutdef ~entry ~uctx ~pinfo:proof_info + pm, MutualEntry.declare_mutdef ~entry ~uctx ~pinfo:proof_info | End_obligation oinfo -> let entry, uctx = check_single_entry proof_obj "Obligation.save" in - Obls_.obligation_terminator ~entry ~uctx ~oinfo + Obls_.obligation_terminator ~pm ~entry ~uctx ~oinfo | End_derive { f ; name } -> - finish_derived ~f ~name ~entries:proof_obj.entries + pm, finish_derived ~f ~name ~entries:proof_obj.entries | End_equations { hook; i; types; sigma } -> let kind = proof_info.Proof_info.info.Info.kind in - finish_proved_equations ~kind ~hook i proof_obj types sigma + pm, finish_proved_equations ~kind ~hook i proof_obj types sigma let err_save_forbidden_in_place_of_qed () = CErrors.user_err (Pp.str "Cannot use Save with more than one constant or in this proof mode") @@ -2072,16 +2052,16 @@ let process_idopt_for_save ~idopt info = err_save_forbidden_in_place_of_qed () in { info with Proof_info.cinfo } -let save ~proof ~opaque ~idopt = +let save ~pm ~proof ~opaque ~idopt = (* Env and sigma are just used for error printing in save_remaining_recthms *) let proof_obj = close_proof ~opaque ~keep_body_ucst_separate:false proof in let proof_info = process_idopt_for_save ~idopt proof.pinfo in - finalize_proof proof_obj proof_info + finalize_proof ~pm proof_obj proof_info (***********************************************************************) (* Special case to close a lemma without forcing a proof *) (***********************************************************************) -let save_lemma_admitted_delayed ~proof ~pinfo = +let save_lemma_admitted_delayed ~pm ~proof ~pinfo = let { entries; uctx } = proof in if List.length entries <> 1 then CErrors.user_err Pp.(str "Admitted does not support multiple statements"); @@ -2094,18 +2074,18 @@ let save_lemma_admitted_delayed ~proof ~pinfo = | Some typ -> typ in let ctx = UState.univ_entry ~poly uctx in let sec_vars = if get_keep_admitted_vars () then proof_entry_secctx else None in - finish_admitted ~uctx ~pinfo (sec_vars, (typ, ctx), None) + finish_admitted ~pm ~uctx ~pinfo (sec_vars, (typ, ctx), None) -let save_lemma_proved_delayed ~proof ~pinfo ~idopt = +let save_lemma_proved_delayed ~pm ~proof ~pinfo ~idopt = (* vio2vo calls this but with invalid info, we have to workaround that to add the name to the info structure *) if CList.is_empty pinfo.Proof_info.cinfo then let name = get_po_name proof in let info = Proof_info.add_first_thm ~pinfo ~name ~typ:EConstr.mkSet ~impargs:[] in - finalize_proof proof info + finalize_proof ~pm proof info else let info = process_idopt_for_save ~idopt pinfo in - finalize_proof proof info + finalize_proof ~pm proof info end (* Proof module *) @@ -2219,8 +2199,8 @@ let solve_by_tac ?loc name evi t ~poly ~uctx = warn_solve_errored ?loc err; None -let get_unique_prog prg = - match State.get_unique_open_prog prg with +let get_unique_prog ~pm prg = + match State.get_unique_open_prog pm prg with | Ok prg -> prg | Error [] -> Error.no_obligations None @@ -2243,7 +2223,7 @@ let rec solve_obligation prg num tac = let kind = kind_of_obligation (snd obl.obl_status) in let evd = Evd.from_ctx (Internal.get_uctx prg) in let evd = Evd.update_sigma_env evd (Global.env ()) in - let auto n oblset tac = auto_solve_obligations n ~oblset tac in + let auto ~pm n oblset tac = auto_solve_obligations ~pm n ~oblset tac in let proof_ending = let name = Internal.get_name prg in Proof_ending.End_obligation {name; num; auto} @@ -2256,9 +2236,9 @@ let rec solve_obligation prg num tac = let lemma = Option.cata (fun tac -> Proof.set_endline_tactic tac lemma) lemma tac in lemma -and obligation (user_num, name, typ) tac = +and obligation (user_num, name, typ) ~pm tac = let num = pred user_num in - let prg = get_unique_prog name in + let prg = get_unique_prog ~pm name in let { obls; remaining } = Internal.get_obligations prg in if num >= 0 && num < Array.length obls then let obl = obls.(num) in @@ -2299,7 +2279,7 @@ and solve_obligation_by_tac prg obls i tac = else Some prg else None -and solve_prg_obligations prg ?oblset tac = +and solve_prg_obligations ~pm prg ?oblset tac = let { obls; remaining } = Internal.get_obligations prg in let rem = ref remaining in let obls' = Array.copy obls in @@ -2309,49 +2289,48 @@ and solve_prg_obligations prg ?oblset tac = | Some s -> set := s; (fun i -> Int.Set.mem i !set) in - let (), prg = + let prg = Array.fold_left_i - (fun i ((), prg) x -> + (fun i prg x -> if p i then ( match solve_obligation_by_tac prg obls' i tac with - | None -> (), prg + | None -> prg | Some prg -> let deps = dependencies obls i in set := Int.Set.union !set deps; decr rem; - (), prg) - else (), prg) - ((), prg) obls' + prg) + else prg) + prg obls' in - update_obls prg obls' !rem + update_obls ~pm prg obls' !rem -and solve_obligations n tac = - let prg = get_unique_prog n in - solve_prg_obligations prg tac +and solve_obligations ~pm n tac = + let prg = get_unique_prog ~pm n in + solve_prg_obligations ~pm prg tac -and solve_all_obligations tac = - State.fold ~init:() ~f:(fun k v () -> - let _ = solve_prg_obligations v tac in ()) +and solve_all_obligations ~pm tac = + State.fold pm ~init:pm ~f:(fun k v pm -> + solve_prg_obligations ~pm v tac |> fst) -and try_solve_obligation n prg tac = - let prg = get_unique_prog prg in +and try_solve_obligation ~pm n prg tac = + let prg = get_unique_prog ~pm prg in let {obls; remaining} = Internal.get_obligations prg in let obls' = Array.copy obls in match solve_obligation_by_tac prg obls' n tac with | Some prg' -> - let _r = update_obls prg' obls' (pred remaining) in - () - | None -> () + let pm, _ = update_obls ~pm prg' obls' (pred remaining) in + pm + | None -> pm -and try_solve_obligations n tac = - let _ = solve_obligations n tac in - () +and try_solve_obligations ~pm n tac = + solve_obligations ~pm n tac |> fst -and auto_solve_obligations n ?oblset tac : progress = +and auto_solve_obligations ~pm n ?oblset tac : State.t * progress = Flags.if_verbose Feedback.msg_info (str "Solving obligations automatically..."); - let prg = get_unique_prog n in - solve_prg_obligations prg ?oblset tac + let prg = get_unique_prog ~pm n in + solve_prg_obligations ~pm prg ?oblset tac let show_single_obligation i n obls x = let x = subst_deps_obl obls x in @@ -2381,20 +2360,20 @@ let show_obligations_of_prg ?(msg = true) prg = | Some _ -> ()) obls -let show_obligations ?(msg = true) n = +let show_obligations ~pm ?(msg = true) n = let progs = match n with | None -> - State.all () + State.all pm | Some n -> - (match State.find n with + (match State.find pm n with | Some prg -> [prg] | None -> Error.no_obligations (Some n)) in List.iter (fun x -> show_obligations_of_prg ~msg x) progs -let show_term n = - let prg = get_unique_prog n in +let show_term ~pm n = + let prg = get_unique_prog ~pm n in ProgramDecl.show prg let msg_generating_obl name obls = @@ -2406,7 +2385,7 @@ let msg_generating_obl name obls = info ++ str ", generating " ++ int len ++ str (String.plural len " obligation")) -let add_definition ~cinfo ~info ?term ~uctx +let add_definition ~pm ~cinfo ~info ?term ~uctx ?tactic ?(reduce = reduce) ?(opaque = false) obls = let prg = ProgramDecl.make ~info ~cinfo ~body:term ~opaque ~uctx ~reduce ~ntns:[] ~deps:[] ~fixpoint_kind:None obls @@ -2415,37 +2394,37 @@ let add_definition ~cinfo ~info ?term ~uctx let {obls;_} = Internal.get_obligations prg in if Int.equal (Array.length obls) 0 then ( Flags.if_verbose (msg_generating_obl name) obls; - let cst = Obls_.declare_definition prg in - Defined cst) + let pm, cst = Obls_.declare_definition ~pm prg in + pm, Defined cst) else let () = Flags.if_verbose (msg_generating_obl name) obls in - let () = State.add name prg in - let res = auto_solve_obligations (Some name) tactic in + let pm = State.add pm name prg in + let pm, res = auto_solve_obligations ~pm (Some name) tactic in match res with | Remain rem -> - Flags.if_verbose (show_obligations ~msg:false) (Some name); - res - | _ -> res + Flags.if_verbose (show_obligations ~pm ~msg:false) (Some name); + pm, res + | _ -> pm, res -let add_mutual_definitions l ~info ~uctx +let add_mutual_definitions l ~pm ~info ~uctx ?tactic ?(reduce = reduce) ?(opaque = false) ~ntns fixkind = let deps = List.map (fun (ci,_,_) -> CInfo.get_name ci) l in let pm = List.fold_left - (fun () (cinfo, b, obls) -> + (fun pm (cinfo, b, obls) -> let prg = ProgramDecl.make ~info ~cinfo ~opaque ~body:(Some b) ~uctx ~deps ~fixpoint_kind:(Some fixkind) ~ntns obls ~reduce in - State.add (CInfo.get_name cinfo) prg) - () l + State.add pm (CInfo.get_name cinfo) prg) + pm l in let pm, _defined = List.fold_left (fun (pm, finished) x -> if finished then (pm, finished) else - let res = auto_solve_obligations (Some x) tactic in + let pm, res = auto_solve_obligations ~pm (Some x) tactic in match res with | Defined _ -> (* If one definition is turned into a constant, @@ -2456,7 +2435,7 @@ let add_mutual_definitions l ~info ~uctx in pm -let admit_prog prg = +let admit_prog ~pm prg = let {obls; remaining} = Internal.get_obligations prg in let obls = Array.copy obls in Array.iteri @@ -2473,29 +2452,29 @@ let admit_prog prg = obls.(i) <- Obligation.set_body ~body:(DefinedObl (kn, Univ.Instance.empty)) x | Some _ -> ()) obls; - Obls_.update_obls prg obls 0 + Obls_.update_obls ~pm prg obls 0 (* get_any_prog *) -let rec admit_all_obligations () = - let prg = State.first_pending () in +let rec admit_all_obligations ~pm = + let prg = State.first_pending pm in match prg with - | None -> () + | None -> pm | Some prg -> - let _prog = admit_prog prg in - admit_all_obligations () + let pm, _prog = admit_prog ~pm prg in + admit_all_obligations ~pm -let admit_obligations n = +let admit_obligations ~pm n = match n with - | None -> admit_all_obligations () + | None -> admit_all_obligations ~pm | Some _ -> - let prg = get_unique_prog n in - let _ = admit_prog prg in - () + let prg = get_unique_prog ~pm n in + let pm, _ = admit_prog ~pm prg in + pm -let next_obligation n tac = +let next_obligation ~pm n tac = let prg = match n with - | None -> State.first_pending () |> Option.get - | Some _ -> get_unique_prog n + | None -> State.first_pending pm |> Option.get + | Some _ -> get_unique_prog ~pm n in let {obls; remaining} = 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 @@ -2511,7 +2490,6 @@ let check_program_libraries () = Coqlib.check_required_library ["Coq";"Program";"Tactics"] (* aliases *) -module State = Obls_.State let prepare_obligation = prepare_obligation let check_solved_obligations = Obls_.check_solved_obligations type fixpoint_kind = Obls_.fixpoint_kind = @@ -2520,3 +2498,5 @@ type nonrec progress = progress = | Remain of int | Dependent | Defined of GlobRef.t end + +module OblState = Obls_.State diff --git a/vernac/declare.mli b/vernac/declare.mli index e13611a828..25fad05a08 100644 --- a/vernac/declare.mli +++ b/vernac/declare.mli @@ -150,6 +150,13 @@ val declare_mutually_recursive (** {2 Declaration of interactive constants } *) +(** [save] / [save_admitted] can update obligations state, so we need + to expose the state here *) +module OblState : sig + type t + val empty : t +end + (** [Declare.Proof.t] Construction of constants using interactive proofs. *) module Proof : sig @@ -201,13 +208,14 @@ module Proof : sig (** Qed a proof *) val save - : proof:t + : pm:OblState.t + -> proof:t -> opaque:Vernacexpr.opacity_flag -> idopt:Names.lident option - -> GlobRef.t list + -> OblState.t * GlobRef.t list (** Admit a proof *) - val save_admitted : proof:t -> unit + val save_admitted : pm:OblState.t -> proof:t -> OblState.t (** [by tac] applies tactic [tac] to the 1st subgoal of the current focused proof. @@ -290,15 +298,17 @@ module Proof : sig (** Special cases for delayed proofs, in this case we must provide the proof information so the proof won't be forced. *) val save_lemma_admitted_delayed : - proof:proof_object + pm:OblState.t + -> proof:proof_object -> pinfo:Proof_info.t - -> unit + -> OblState.t val save_lemma_proved_delayed - : proof:proof_object + : pm:OblState.t + -> proof:proof_object -> pinfo:Proof_info.t -> idopt:Names.lident option - -> GlobRef.t list + -> OblState.t * GlobRef.t list (** Used by the STM only to store info, should go away *) val get_po_name : proof_object -> Id.t @@ -449,16 +459,9 @@ module Obls : sig type fixpoint_kind = IsFixpoint of lident option list | IsCoFixpoint -module State : sig - (* Internal *) - type t - val prg_tag : t Summary.Dyn.tag -end - (** Check obligations are properly solved before closing the [what_for] section / module *) -val check_solved_obligations : what_for:Pp.t -> unit - +val check_solved_obligations : pm:OblState.t -> what_for:Pp.t -> unit val default_tactic : unit Proofview.tactic ref (** Resolution status of a program *) @@ -481,7 +484,8 @@ val prepare_obligation will return whether all the obligations were solved; if so, it will also register [c] with the kernel. *) val add_definition : - cinfo:Constr.types CInfo.t + pm:OblState.t + -> cinfo:Constr.types CInfo.t -> info:Info.t -> ?term:Constr.t -> uctx:UState.t @@ -489,7 +493,7 @@ val add_definition : -> ?reduce:(Constr.t -> Constr.t) -> ?opaque:bool -> RetrieveObl.obligation_info - -> progress + -> OblState.t * progress (* XXX: unify with MutualEntry *) @@ -497,6 +501,7 @@ val add_definition : except it takes a list now. *) val add_mutual_definitions : (Constr.t CInfo.t * Constr.t * RetrieveObl.obligation_info) list + -> pm:OblState.t -> info:Info.t -> uctx:UState.t -> ?tactic:unit Proofview.tactic @@ -504,34 +509,35 @@ val add_mutual_definitions : -> ?opaque:bool -> ntns:Vernacexpr.decl_notation list -> fixpoint_kind - -> unit + -> OblState.t (** Implementation of the [Obligation] command *) val obligation : int * Names.Id.t option * Constrexpr.constr_expr option + -> pm:OblState.t -> Genarg.glob_generic_argument option -> Proof.t (** Implementation of the [Next Obligation] command *) val next_obligation : - Names.Id.t option -> Genarg.glob_generic_argument option -> Proof.t + pm:OblState.t -> Names.Id.t option -> Genarg.glob_generic_argument option -> Proof.t (** Implementation of the [Solve Obligation] command *) val solve_obligations : - Names.Id.t option -> unit Proofview.tactic option -> progress + pm:OblState.t -> Names.Id.t option -> unit Proofview.tactic option -> OblState.t * progress -val solve_all_obligations : unit Proofview.tactic option -> unit +val solve_all_obligations : pm:OblState.t -> unit Proofview.tactic option -> OblState.t (** Number of remaining obligations to be solved for this program *) val try_solve_obligation : - int -> Names.Id.t option -> unit Proofview.tactic option -> unit + pm:OblState.t -> int -> Names.Id.t option -> unit Proofview.tactic option -> OblState.t val try_solve_obligations : - Names.Id.t option -> unit Proofview.tactic option -> unit + pm:OblState.t -> Names.Id.t option -> unit Proofview.tactic option -> OblState.t -val show_obligations : ?msg:bool -> Names.Id.t option -> unit -val show_term : Names.Id.t option -> Pp.t -val admit_obligations : Names.Id.t option -> unit +val show_obligations : pm:OblState.t -> ?msg:bool -> Names.Id.t option -> unit +val show_term : pm:OblState.t -> Names.Id.t option -> Pp.t +val admit_obligations : pm:OblState.t -> Names.Id.t option -> OblState.t val check_program_libraries : unit -> unit diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml index 6ed8c59f9f..d540e7f93d 100644 --- a/vernac/vernacentries.ml +++ b/vernac/vernacentries.ml @@ -579,7 +579,7 @@ let vernac_definition_interactive ~atts (discharge, kind) (lid, pl) bl t = let name = vernac_definition_name lid local in start_lemma_com ~program_mode ~poly ~scope:local ~kind:(Decls.IsDefinition kind) ?hook [(name, pl), (bl, t)] -let vernac_definition ~atts (discharge, kind) (lid, pl) bl red_option c typ_opt = +let vernac_definition ~atts ~pm (discharge, kind) (lid, pl) bl red_option c typ_opt = let open DefAttributes in let scope = enforce_locality_exp atts.locality discharge in let hook = vernac_definition_hook ~canonical_instance:atts.canonical_instance ~local:atts.locality ~poly:atts.polymorphic kind in @@ -593,13 +593,13 @@ let vernac_definition ~atts (discharge, kind) (lid, pl) bl red_option c typ_opt Some (snd (Hook.get f_interp_redexp env sigma r)) in if program_mode then let kind = Decls.IsDefinition kind in - ComDefinition.do_definition_program ~name:name.v + ComDefinition.do_definition_program ~pm ~name:name.v ~poly:atts.polymorphic ~scope ~kind pl bl red_option c typ_opt ?hook else let () = ComDefinition.do_definition ~name:name.v ~poly:atts.polymorphic ~scope ~kind pl bl red_option c typ_opt ?hook in - () + pm (* NB: pstate argument to use combinators easily *) let vernac_start_proof ~atts kind l = @@ -609,19 +609,20 @@ let vernac_start_proof ~atts kind l = List.iter (fun ((id, _), _) -> Dumpglob.dump_definition id false "prf") l; start_lemma_com ~program_mode:atts.program ~poly:atts.polymorphic ~scope ~kind:(Decls.IsProof kind) l -let vernac_end_proof ~lemma = let open Vernacexpr in function +let vernac_end_proof ~lemma ~pm = let open Vernacexpr in function | Admitted -> - Declare.Proof.save_admitted ~proof:lemma + Declare.Proof.save_admitted ~pm ~proof:lemma | Proved (opaque,idopt) -> - let _ : Names.GlobRef.t list = Declare.Proof.save ~proof:lemma ~opaque ~idopt - in () + let pm, _ = Declare.Proof.save ~pm ~proof:lemma ~opaque ~idopt + in pm -let vernac_exact_proof ~lemma c = +let vernac_exact_proof ~lemma ~pm c = (* spiwack: for simplicity I do not enforce that "Proof proof_term" is called only at the beginning of a proof. *) let lemma, status = Declare.Proof.by (Tactics.exact_proof c) lemma in - let _ : _ list = Declare.Proof.save ~proof:lemma ~opaque:Opaque ~idopt:None in - if not status then Feedback.feedback Feedback.AddedAxiom + let pm, _ = Declare.Proof.save ~pm ~proof:lemma ~opaque:Opaque ~idopt:None in + if not status then Feedback.feedback Feedback.AddedAxiom; + pm let vernac_assumption ~atts discharge kind l nl = let open DefAttributes in @@ -837,14 +838,15 @@ let vernac_fixpoint_interactive ~atts discharge l = CErrors.user_err Pp.(str"Program Fixpoint requires a body"); ComFixpoint.do_fixpoint_interactive ~scope ~poly:atts.polymorphic l -let vernac_fixpoint ~atts discharge l = +let vernac_fixpoint ~atts ~pm discharge l = let open DefAttributes in let scope = vernac_fixpoint_common ~atts discharge l in if atts.program then (* XXX: Switch to the attribute system and match on ~atts *) - ComProgramFixpoint.do_fixpoint ~scope ~poly:atts.polymorphic l + ComProgramFixpoint.do_fixpoint ~pm ~scope ~poly:atts.polymorphic l else - ComFixpoint.do_fixpoint ~scope ~poly:atts.polymorphic l + let () = ComFixpoint.do_fixpoint ~scope ~poly:atts.polymorphic l in + pm let vernac_cofixpoint_common ~atts discharge l = if Dumpglob.dump () then @@ -858,13 +860,14 @@ let vernac_cofixpoint_interactive ~atts discharge l = CErrors.user_err Pp.(str"Program CoFixpoint requires a body"); ComFixpoint.do_cofixpoint_interactive ~scope ~poly:atts.polymorphic l -let vernac_cofixpoint ~atts discharge l = +let vernac_cofixpoint ~atts ~pm discharge l = let open DefAttributes in let scope = vernac_cofixpoint_common ~atts discharge l in if atts.program then - ComProgramFixpoint.do_cofixpoint ~scope ~poly:atts.polymorphic l + ComProgramFixpoint.do_cofixpoint ~pm ~scope ~poly:atts.polymorphic l else - ComFixpoint.do_cofixpoint ~scope ~poly:atts.polymorphic l + let () = ComFixpoint.do_cofixpoint ~scope ~poly:atts.polymorphic l in + pm let vernac_scheme l = if Dumpglob.dump () then @@ -1085,10 +1088,10 @@ let msg_of_subsection ss id = in Pp.str kind ++ spc () ++ Id.print id -let vernac_end_segment ({v=id} as lid) = +let vernac_end_segment ~pm ({v=id} as lid) = let ss = Lib.find_opening_node id in let what_for = msg_of_subsection ss lid.v in - Declare.Obls.check_solved_obligations ~what_for; + Declare.Obls.check_solved_obligations ~pm ~what_for; match ss with | Lib.OpenedModule (false,export,_,_) -> vernac_end_module export lid | Lib.OpenedModule (true,_,_,_) -> vernac_end_modtype lid @@ -1147,14 +1150,14 @@ let vernac_identity_coercion ~atts id qids qidt = (* Type classes *) -let vernac_instance_program ~atts name bl t props info = +let vernac_instance_program ~atts ~pm name bl t props info = Dumpglob.dump_constraint (fst name) false "inst"; let locality, poly = Attributes.(parse (Notations.(locality ++ polymorphic))) atts in let global = not (make_section_locality locality) in - let _id : Id.t = Classes.new_instance_program ~global ~poly name bl t props info in - () + let pm, _id = Classes.new_instance_program ~pm ~global ~poly name bl t props info in + pm let vernac_instance_interactive ~atts name bl t info props = Dumpglob.dump_constraint (fst name) false "inst"; @@ -1991,9 +1994,9 @@ let translate_vernac ~atts v = let open Vernacextend in match v with (* Gallina *) | VernacDefinition (discharge,lid,DefineBody (bl,red_option,c,typ)) -> - VtDefault (fun () -> + VtModifyProgram (fun ~pm -> with_def_attributes ~atts - vernac_definition discharge lid bl red_option c typ) + vernac_definition ~pm discharge lid bl red_option c typ) | VernacDefinition (discharge,lid,ProveBody(bl,typ)) -> VtOpenProof(fun () -> with_def_attributes ~atts @@ -2028,14 +2031,14 @@ let translate_vernac ~atts v = let open Vernacextend in match v with VtOpenProof (fun () -> with_def_attributes ~atts vernac_fixpoint_interactive discharge l) else - VtDefault (fun () -> - with_def_attributes ~atts vernac_fixpoint discharge l) + VtModifyProgram (fun ~pm -> + with_def_attributes ~atts (vernac_fixpoint ~pm) discharge l) | VernacCoFixpoint (discharge, l) -> let opens = List.exists (fun { body_def } -> Option.is_empty body_def) l in if opens then VtOpenProof(fun () -> with_def_attributes ~atts vernac_cofixpoint_interactive discharge l) else - VtDefault(fun () -> with_def_attributes ~atts vernac_cofixpoint discharge l) + VtModifyProgram(fun ~pm -> with_def_attributes ~atts (vernac_cofixpoint ~pm) discharge l) | VernacScheme l -> VtDefault(fun () -> @@ -2064,9 +2067,9 @@ let translate_vernac ~atts v = let open Vernacextend in match v with VtNoProof(fun () -> vernac_begin_section ~poly:(only_polymorphism atts) lid) | VernacEndSegment lid -> - VtNoProof(fun () -> + VtReadProgram(fun ~pm -> unsupported_attributes atts; - vernac_end_segment lid) + vernac_end_segment ~pm lid) | VernacNameSectionHypSet (lid, set) -> VtDefault(fun () -> unsupported_attributes atts; @@ -2091,7 +2094,7 @@ let translate_vernac ~atts v = let open Vernacextend in match v with | VernacInstance (name, bl, t, props, info) -> let atts, program = Attributes.(parse_with_extra program) atts in if program then - VtDefault (fun () -> vernac_instance_program ~atts name bl t props info) + VtModifyProgram (vernac_instance_program ~atts name bl t props info) else begin match props with | None -> VtOpenProof (fun () -> diff --git a/vernac/vernacextend.ml b/vernac/vernacextend.ml index f8a80e8feb..7317818730 100644 --- a/vernac/vernacextend.ml +++ b/vernac/vernacextend.ml @@ -55,11 +55,14 @@ and proof_block_name = string (** open type of delimiters *) type typed_vernac = | VtDefault of (unit -> unit) | VtNoProof of (unit -> unit) - | VtCloseProof of (lemma:Declare.Proof.t -> unit) + | VtCloseProof of (lemma:Declare.Proof.t -> pm:Declare.OblState.t -> Declare.OblState.t) | VtOpenProof of (unit -> Declare.Proof.t) | VtModifyProof of (pstate:Declare.Proof.t -> Declare.Proof.t) | VtReadProofOpt of (pstate:Declare.Proof.t option -> unit) | VtReadProof of (pstate:Declare.Proof.t -> unit) + | VtReadProgram of (pm:Declare.OblState.t -> unit) + | VtModifyProgram of (pm:Declare.OblState.t -> Declare.OblState.t) + | VtDeclareProgram of (pm:Declare.OblState.t -> Declare.Proof.t) type vernac_command = atts:Attributes.vernac_flags -> typed_vernac diff --git a/vernac/vernacextend.mli b/vernac/vernacextend.mli index 103e24233b..a24bb9b302 100644 --- a/vernac/vernacextend.mli +++ b/vernac/vernacextend.mli @@ -73,11 +73,14 @@ and proof_block_name = string (** open type of delimiters *) type typed_vernac = | VtDefault of (unit -> unit) | VtNoProof of (unit -> unit) - | VtCloseProof of (lemma:Declare.Proof.t -> unit) + | VtCloseProof of (lemma:Declare.Proof.t -> pm:Declare.OblState.t -> Declare.OblState.t) | VtOpenProof of (unit -> Declare.Proof.t) | VtModifyProof of (pstate:Declare.Proof.t -> Declare.Proof.t) | VtReadProofOpt of (pstate:Declare.Proof.t option -> unit) | VtReadProof of (pstate:Declare.Proof.t -> unit) + | VtReadProgram of (pm:Declare.OblState.t -> unit) + | VtModifyProgram of (pm:Declare.OblState.t -> Declare.OblState.t) + | VtDeclareProgram of (pm:Declare.OblState.t -> Declare.Proof.t) type vernac_command = atts:Attributes.vernac_flags -> typed_vernac diff --git a/vernac/vernacinterp.ml b/vernac/vernacinterp.ml index 1b977b8e10..898506fdbc 100644 --- a/vernac/vernacinterp.ml +++ b/vernac/vernacinterp.ml @@ -22,32 +22,38 @@ let vernac_require_open_lemma ~stack f = | None -> CErrors.user_err (Pp.str "Command not supported (No proof-editing in progress)") -let interp_typed_vernac c ~stack = +let interp_typed_vernac c ~pm ~stack = let open Vernacextend in match c with - | VtDefault f -> f (); stack + | VtDefault f -> f (); stack, pm | VtNoProof f -> if Option.has_some stack then CErrors.user_err (Pp.str "Command not supported (Open proofs remain)"); let () = f () in - stack + stack, pm | VtCloseProof f -> vernac_require_open_lemma ~stack (fun stack -> let lemma, stack = Vernacstate.LemmaStack.pop stack in - f ~lemma; - stack) + let pm = f ~lemma ~pm in + stack, pm) | VtOpenProof f -> - Some (Vernacstate.LemmaStack.push stack (f ())) + Some (Vernacstate.LemmaStack.push stack (f ())), pm | VtModifyProof f -> - Option.map (Vernacstate.LemmaStack.map_top ~f:(fun pstate -> f ~pstate)) stack + Option.map (Vernacstate.LemmaStack.map_top ~f:(fun pstate -> f ~pstate)) stack, pm | VtReadProofOpt f -> let pstate = Option.map (Vernacstate.LemmaStack.with_top ~f:(fun x -> x)) stack in f ~pstate; - stack + stack, pm | VtReadProof f -> vernac_require_open_lemma ~stack (Vernacstate.LemmaStack.with_top ~f:(fun pstate -> f ~pstate)); - stack + stack, pm + | VtReadProgram f -> f ~pm; stack, pm + | VtModifyProgram f -> + let pm = f ~pm in stack, pm + | VtDeclareProgram f -> + let lemma = f ~pm in + Some (Vernacstate.LemmaStack.push stack lemma), pm (* Default proof mode, to be set at the beginning of proofs for programs that cannot be statically classified. *) @@ -123,11 +129,11 @@ let mk_time_header = fun vernac -> Lazy.from_fun (fun () -> pr_time_header vernac) let interp_control_flag ~time_header (f : control_flag) ~st - (fn : st:Vernacstate.t -> Vernacstate.LemmaStack.t option) = + (fn : st:Vernacstate.t -> Vernacstate.LemmaStack.t option * Declare.OblState.t) = match f with | ControlFail -> with_fail ~st (fun () -> fn ~st); - st.Vernacstate.lemmas + st.Vernacstate.lemmas, st.Vernacstate.program | ControlTimeout timeout -> vernac_timeout ~timeout (fun () -> fn ~st) () | ControlTime batch -> @@ -142,6 +148,7 @@ let interp_control_flag ~time_header (f : control_flag) ~st * loc is the Loc.t of the vernacular command being interpreted. *) let rec interp_expr ~atts ~st c = let stack = st.Vernacstate.lemmas in + let program = st.Vernacstate.program in vernac_pperr_endline Pp.(fun () -> str "interpreting: " ++ Ppvernac.pr_vernac_expr c); match c with @@ -163,7 +170,7 @@ let rec interp_expr ~atts ~st c = vernac_load ~verbosely fname | v -> let fv = Vernacentries.translate_vernac ~atts v in - interp_typed_vernac ~stack fv + interp_typed_vernac ~pm:program ~stack fv and vernac_load ~verbosely fname = (* Note that no proof should be open here, so the state here is just token for now *) @@ -180,19 +187,19 @@ and vernac_load ~verbosely fname = let parse_sentence proof_mode = Flags.with_option Flags.we_are_parsing (Pcoq.Entry.parse (Pvernac.main_entry proof_mode)) in - let rec load_loop ~stack = + let rec load_loop ~pm ~stack = let proof_mode = Option.map (fun _ -> get_default_proof_mode ()) stack in match parse_sentence proof_mode input with - | None -> stack + | None -> stack, pm | Some stm -> - let stack = v_mod (interp_control ~st:{ st with Vernacstate.lemmas = stack }) stm in - (load_loop [@ocaml.tailcall]) ~stack + let stack, pm = v_mod (interp_control ~st:{ st with Vernacstate.lemmas = stack; program = pm }) stm in + (load_loop [@ocaml.tailcall]) ~stack ~pm in - let stack = load_loop ~stack:st.Vernacstate.lemmas in + let stack, pm = load_loop ~pm:st.Vernacstate.program ~stack:st.Vernacstate.lemmas in (* If Load left a proof open, we fail too. *) if Option.has_some stack then CErrors.user_err Pp.(str "Files processed by Load cannot leave open proofs."); - stack + stack, pm and interp_control ~st ({ CAst.v = cmd } as vernac) = let time_header = mk_time_header vernac in @@ -200,9 +207,9 @@ and interp_control ~st ({ CAst.v = cmd } as vernac) = cmd.control (fun ~st -> let before_univs = Global.universes () in - let pstack = interp_expr ~atts:cmd.attrs ~st cmd.expr in - if before_univs == Global.universes () then pstack - else Option.map (Vernacstate.LemmaStack.map_top ~f:Declare.Proof.update_global_env) pstack) + let pstack, pm = interp_expr ~atts:cmd.attrs ~st cmd.expr in + if before_univs == Global.universes () then pstack, pm + else Option.map (Vernacstate.LemmaStack.map_top ~f:Declare.Proof.update_global_env) pstack, pm) ~st (* XXX: This won't properly set the proof mode, as of today, it is @@ -213,17 +220,18 @@ and interp_control ~st ({ CAst.v = cmd } as vernac) = *) (* Interpreting a possibly delayed proof *) -let interp_qed_delayed ~proof ~pinfo ~st pe : Vernacstate.LemmaStack.t option = +let interp_qed_delayed ~proof ~pinfo ~st pe : Vernacstate.LemmaStack.t option * Declare.OblState.t = let stack = st.Vernacstate.lemmas in + let pm = st.Vernacstate.program in let stack = Option.cata (fun stack -> snd @@ Vernacstate.LemmaStack.pop stack) None stack in - let () = match pe with + let pm = match pe with | Admitted -> - Declare.Proof.save_lemma_admitted_delayed ~proof ~pinfo + Declare.Proof.save_lemma_admitted_delayed ~pm ~proof ~pinfo | Proved (_,idopt) -> - let _ : _ list = Declare.Proof.save_lemma_proved_delayed ~proof ~pinfo ~idopt in - () + let pm, _ = Declare.Proof.save_lemma_proved_delayed ~pm ~proof ~pinfo ~idopt in + pm in - stack + stack, pm let interp_qed_delayed_control ~proof ~pinfo ~st ~control { CAst.loc; v=pe } = let time_header = mk_time_header (CAst.make ?loc { control; attrs = []; expr = VernacEndProof pe }) in diff --git a/vernac/vernacstate.ml b/vernac/vernacstate.ml index 073ef1c2d7..ee06205427 100644 --- a/vernac/vernacstate.ml +++ b/vernac/vernacstate.ml @@ -113,15 +113,18 @@ type t = { parsing : Parser.t; system : System.t; (* summary + libstack *) lemmas : LemmaStack.t option; (* proofs of lemmas currently opened *) + program : Declare.OblState.t; (* obligations table *) shallow : bool (* is the state trimmed down (libstack) *) } let s_cache = ref None let s_lemmas = ref None +let s_program = ref Declare.OblState.empty let invalidate_cache () = s_cache := None; - s_lemmas := None + s_lemmas := None; + s_program := Declare.OblState.empty let update_cache rf v = rf := Some v; v @@ -138,20 +141,24 @@ let do_if_not_cached rf f v = let freeze_interp_state ~marshallable = { system = update_cache s_cache (System.freeze ~marshallable); lemmas = !s_lemmas; + program = !s_program; shallow = false; parsing = Parser.cur_state (); } -let unfreeze_interp_state { system; lemmas; parsing } = +let unfreeze_interp_state { system; lemmas; program; parsing } = do_if_not_cached s_cache System.unfreeze system; s_lemmas := lemmas; + s_program := program; Pcoq.unfreeze parsing (* Compatibility module *) module Declare_ = struct let get () = !s_lemmas - let set x = s_lemmas := x + let set (pstate,pm) = + s_lemmas := pstate; + s_program := pm let get_pstate () = Option.map (LemmaStack.with_top ~f:(fun x -> x)) !s_lemmas @@ -237,18 +244,16 @@ module Stm = struct type nonrec pstate = LemmaStack.t option * int * (* Evarutil.meta_counter_summary_tag *) - int * (* Evd.evar_counter_summary_tag *) - Declare.Obls.State.t + int (* Evd.evar_counter_summary_tag *) (* Parts of the system state that are morally part of the proof state *) let pstate { lemmas; system } = let st = System.Stm.summary system in lemmas, Summary.project_from_summary st Evarutil.meta_counter_summary_tag, - Summary.project_from_summary st Evd.evar_counter_summary_tag, - Summary.project_from_summary st Declare.Obls.State.prg_tag + Summary.project_from_summary st Evd.evar_counter_summary_tag - let set_pstate ({ lemmas; system } as s) (pstate,c1,c2,c3) = + let set_pstate ({ lemmas; system } as s) (pstate,c1,c2) = { s with lemmas = Declare_.copy_terminators ~src:s.lemmas ~tgt:pstate @@ -258,7 +263,6 @@ module Stm = struct let st = System.Stm.summary s.system in let st = Summary.modify_summary st Evarutil.meta_counter_summary_tag c1 in let st = Summary.modify_summary st Evd.evar_counter_summary_tag c2 in - let st = Summary.modify_summary st Declare.Obls.State.prg_tag c3 in st end } @@ -267,7 +271,6 @@ module Stm = struct let st = System.Stm.summary system in let st = Summary.remove_from_summary st Evarutil.meta_counter_summary_tag in let st = Summary.remove_from_summary st Evd.evar_counter_summary_tag in - let st = Summary.remove_from_summary st Declare.Obls.State.prg_tag in st, System.Stm.lib system let same_env { system = s1 } { system = s2 } = diff --git a/vernac/vernacstate.mli b/vernac/vernacstate.mli index 8c23ac0698..16fab3782b 100644 --- a/vernac/vernacstate.mli +++ b/vernac/vernacstate.mli @@ -52,6 +52,8 @@ type t = (** summary + libstack *) ; lemmas : LemmaStack.t option (** proofs of lemmas currently opened *) + ; program : Declare.OblState.t + (** program mode table *) ; shallow : bool (** is the state trimmed down (libstack) *) } @@ -112,7 +114,7 @@ module Declare : sig (* Low-level stuff *) val get : unit -> LemmaStack.t option - val set : LemmaStack.t option -> unit + val set : LemmaStack.t option * Declare.OblState.t -> unit val get_pstate : unit -> Declare.Proof.t option -- cgit v1.2.3 From 301e9cb85c2ac995d71cb7978ceae78621ec3eee Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Mon, 29 Jun 2020 13:39:18 +0200 Subject: [obligations] Remove duplicate progmap_remove. This is already taken of by `declare_definition`, by consistency with the mutual case. --- vernac/declare.ml | 1 - 1 file changed, 1 deletion(-) diff --git a/vernac/declare.ml b/vernac/declare.ml index fa1bf361fb..757f5b21bc 100644 --- a/vernac/declare.ml +++ b/vernac/declare.ml @@ -1171,7 +1171,6 @@ let update_obls ~pm prg obls rem = match prg'.prg_deps with | [] -> let pm, kn = declare_definition ~pm prg' in - let pm = progmap_remove pm prg' in pm, Defined kn | l -> let progs = -- cgit v1.2.3 From 1954fb6cb6f854c59d7905163ae9b84901edd863 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Mon, 29 Jun 2020 13:27:02 +0200 Subject: [obligations] Allow state-modifying hooks This is for use in Equations. At some point we should make all hook aware of state, but this should suffice for now. Note the comments as the role of hooks here, this may need further cleanup indeed. --- vernac/declare.ml | 35 +++++++++++++++++++++++------------ vernac/declare.mli | 2 ++ 2 files changed, 25 insertions(+), 12 deletions(-) diff --git a/vernac/declare.ml b/vernac/declare.ml index 757f5b21bc..37612a9f9b 100644 --- a/vernac/declare.ml +++ b/vernac/declare.ml @@ -39,6 +39,7 @@ module Hook = struct let make_g hook = CEphemeron.create hook let make (hook : S.t -> unit) : t = CEphemeron.create (fun x () -> hook x) + let call_g ?hook x s = Option.cata (fun hook -> CEphemeron.get hook x s) s hook let call ?hook x = Option.iter (fun hook -> CEphemeron.get hook x ()) hook end @@ -655,9 +656,10 @@ let declare_definition_core ~info ~cinfo ~opaque ~obls ~body sigma = let { CInfo.name; impargs; typ; _ } = cinfo in let entry, uctx = prepare_definition ~info ~opaque ~body ~typ sigma in let { Info.scope; kind; hook; _ } = info in - declare_entry_core ~name ~scope ~kind ~impargs ~obls ?hook ~uctx entry + declare_entry_core ~name ~scope ~kind ~impargs ~obls ?hook ~uctx entry, uctx -let declare_definition = declare_definition_core ~obls:[] +let declare_definition ~info ~cinfo ~opaque ~body sigma = + declare_definition_core ~obls:[] ~info ~cinfo ~opaque ~body sigma |> fst let prepare_obligation ~name ~types ~body sigma = let env = Global.env () in @@ -710,10 +712,11 @@ type fixpoint_kind = IsFixpoint of lident option list | IsCoFixpoint module ProgramDecl = struct - type t = + type 'a t = { prg_cinfo : constr CInfo.t ; prg_info : Info.t ; prg_opaque : bool + ; prg_hook : 'a Hook.g option ; prg_body : constr ; prg_uctx : UState.t ; prg_obligations : obligations @@ -725,7 +728,7 @@ module ProgramDecl = struct open Obligation - let make ~info ~cinfo ~opaque ~ntns ~reduce ~deps ~uctx ~body ~fixpoint_kind obls = + let make ~info ~cinfo ~opaque ~ntns ~reduce ~deps ~uctx ~body ~fixpoint_kind ?obl_hook obls = let obls', body = match body with | None -> @@ -755,6 +758,7 @@ module ProgramDecl = struct let prg_uctx = UState.make_flexible_nonalgebraic uctx in { prg_cinfo = { cinfo with CInfo.typ = reduce cinfo.CInfo.typ } ; prg_info = info + ; prg_hook = obl_hook ; prg_opaque = opaque ; prg_body = body ; prg_uctx @@ -919,7 +923,7 @@ module ProgMap = Id.Map module State = struct - type t = ProgramDecl.t CEphemeron.key ProgMap.t + type t = t ProgramDecl.t CEphemeron.key ProgMap.t let empty = ProgMap.empty @@ -1069,7 +1073,11 @@ let declare_definition ~pm prg = let name, info, opaque = prg.prg_cinfo.CInfo.name, prg.prg_info, prg.prg_opaque in let obls = List.map (fun (id, (_, c)) -> (id, c)) varsubst in (* XXX: This is doing normalization twice *) - let kn = declare_definition_core ~cinfo ~info ~obls ~body ~opaque sigma in + let kn, uctx = declare_definition_core ~cinfo ~info ~obls ~body ~opaque sigma in + (* XXX: We call the obligation hook here, by consistency with the + previous imperative behaviour, however I'm not sure this is right *) + let pm = Hook.call_g ?hook:prg.prg_hook + { Hook.S.uctx; obls; scope = prg.prg_info.Info.scope; dref = kn} pm in let pm = progmap_remove pm prg in pm, kn @@ -1156,8 +1164,11 @@ let declare_mutual_definition ~pm l = in (* Only for the first constant *) let dref = List.hd kns in - Hook.( - call ?hook:first.prg_info.Info.hook {S.uctx = first.prg_uctx; obls; scope; dref}); + let s_hook = {Hook.S.uctx = first.prg_uctx; obls; scope; dref} in + Hook.call ?hook:first.prg_info.Info.hook s_hook; + (* XXX: We call the obligation hook here, by consistency with the + previous imperative behaviour, however I'm not sure this is right *) + let pm = Hook.call_g ?hook:first.prg_hook s_hook pm in let pm = List.fold_left progmap_remove pm l in pm, dref @@ -2384,10 +2395,10 @@ let msg_generating_obl name obls = info ++ str ", generating " ++ int len ++ str (String.plural len " obligation")) -let add_definition ~pm ~cinfo ~info ?term ~uctx +let add_definition ~pm ~cinfo ~info ?obl_hook ?term ~uctx ?tactic ?(reduce = reduce) ?(opaque = false) obls = let prg = - ProgramDecl.make ~info ~cinfo ~body:term ~opaque ~uctx ~reduce ~ntns:[] ~deps:[] ~fixpoint_kind:None obls + ProgramDecl.make ~info ~cinfo ~body:term ~opaque ~uctx ~reduce ~ntns:[] ~deps:[] ~fixpoint_kind:None ?obl_hook obls in let name = CInfo.get_name cinfo in let {obls;_} = Internal.get_obligations prg in @@ -2405,7 +2416,7 @@ let add_definition ~pm ~cinfo ~info ?term ~uctx pm, res | _ -> pm, res -let add_mutual_definitions l ~pm ~info ~uctx +let add_mutual_definitions l ~pm ~info ?obl_hook ~uctx ?tactic ?(reduce = reduce) ?(opaque = false) ~ntns fixkind = let deps = List.map (fun (ci,_,_) -> CInfo.get_name ci) l in let pm = @@ -2413,7 +2424,7 @@ let add_mutual_definitions l ~pm ~info ~uctx (fun pm (cinfo, b, obls) -> let prg = ProgramDecl.make ~info ~cinfo ~opaque ~body:(Some b) ~uctx ~deps - ~fixpoint_kind:(Some fixkind) ~ntns obls ~reduce + ~fixpoint_kind:(Some fixkind) ~ntns ~reduce ?obl_hook obls in State.add pm (CInfo.get_name cinfo) prg) pm l diff --git a/vernac/declare.mli b/vernac/declare.mli index 25fad05a08..9d9516d963 100644 --- a/vernac/declare.mli +++ b/vernac/declare.mli @@ -487,6 +487,7 @@ val add_definition : pm:OblState.t -> cinfo:Constr.types CInfo.t -> info:Info.t + -> ?obl_hook: OblState.t Hook.g -> ?term:Constr.t -> uctx:UState.t -> ?tactic:unit Proofview.tactic @@ -503,6 +504,7 @@ val add_mutual_definitions : (Constr.t CInfo.t * Constr.t * RetrieveObl.obligation_info) list -> pm:OblState.t -> info:Info.t + -> ?obl_hook: OblState.t Hook.g -> uctx:UState.t -> ?tactic:unit Proofview.tactic -> ?reduce:(Constr.t -> Constr.t) -- cgit v1.2.3 From a164eaafad33ccbc2b0bdbb75147a54ebe3a9848 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Mon, 29 Jun 2020 15:00:28 +0200 Subject: [obligations] Allow to simultaneously open a proof and add obligations --- coqpp/coqpp_main.ml | 1 + vernac/vernacextend.ml | 1 + vernac/vernacextend.mli | 1 + vernac/vernacinterp.ml | 3 +++ 4 files changed, 6 insertions(+) diff --git a/coqpp/coqpp_main.ml b/coqpp/coqpp_main.ml index ffde49f2ac..2735c5b5eb 100644 --- a/coqpp/coqpp_main.ml +++ b/coqpp/coqpp_main.ml @@ -342,6 +342,7 @@ let understand_state = function | "read_program" -> "VtReadProgram", false | "program" -> "VtModifyProgram", false | "declare_program" -> "VtDeclareProgram", false + | "program_interactive" -> "VtOpenProofProgram", false | s -> fatal ("unsupported state specifier: " ^ s) let print_body_state state fmt r = diff --git a/vernac/vernacextend.ml b/vernac/vernacextend.ml index 7317818730..496b1a43d1 100644 --- a/vernac/vernacextend.ml +++ b/vernac/vernacextend.ml @@ -63,6 +63,7 @@ type typed_vernac = | VtReadProgram of (pm:Declare.OblState.t -> unit) | VtModifyProgram of (pm:Declare.OblState.t -> Declare.OblState.t) | VtDeclareProgram of (pm:Declare.OblState.t -> Declare.Proof.t) + | VtOpenProofProgram of (pm:Declare.OblState.t -> Declare.OblState.t * Declare.Proof.t) type vernac_command = atts:Attributes.vernac_flags -> typed_vernac diff --git a/vernac/vernacextend.mli b/vernac/vernacextend.mli index a24bb9b302..5ef137cfc0 100644 --- a/vernac/vernacextend.mli +++ b/vernac/vernacextend.mli @@ -81,6 +81,7 @@ type typed_vernac = | VtReadProgram of (pm:Declare.OblState.t -> unit) | VtModifyProgram of (pm:Declare.OblState.t -> Declare.OblState.t) | VtDeclareProgram of (pm:Declare.OblState.t -> Declare.Proof.t) + | VtOpenProofProgram of (pm:Declare.OblState.t -> Declare.OblState.t * Declare.Proof.t) type vernac_command = atts:Attributes.vernac_flags -> typed_vernac diff --git a/vernac/vernacinterp.ml b/vernac/vernacinterp.ml index 898506fdbc..6be2fb0d43 100644 --- a/vernac/vernacinterp.ml +++ b/vernac/vernacinterp.ml @@ -54,6 +54,9 @@ let interp_typed_vernac c ~pm ~stack = | VtDeclareProgram f -> let lemma = f ~pm in Some (Vernacstate.LemmaStack.push stack lemma), pm + | VtOpenProofProgram f -> + let pm, lemma = f ~pm in + Some (Vernacstate.LemmaStack.push stack lemma), pm (* Default proof mode, to be set at the beginning of proofs for programs that cannot be statically classified. *) -- cgit v1.2.3 From 4413a1fb74fc2fd33176e5983a9977f9e28218d9 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Mon, 29 Jun 2020 15:26:12 +0200 Subject: [declare] Allow obligations update on equations closing hook. This is also needed in equations. --- vernac/declare.ml | 10 +++++----- vernac/declare.mli | 2 +- 2 files changed, 6 insertions(+), 6 deletions(-) diff --git a/vernac/declare.ml b/vernac/declare.ml index 37612a9f9b..e19eca9a1c 100644 --- a/vernac/declare.ml +++ b/vernac/declare.ml @@ -1317,7 +1317,7 @@ module Proof_ending = struct | End_obligation of Obls_.obligation_qed_info | End_derive of { f : Id.t; name : Id.t } | End_equations of - { hook : Constant.t list -> Evd.evar_map -> unit + { hook : pm:Obls_.State.t -> Constant.t list -> Evd.evar_map -> Obls_.State.t ; i : Id.t ; types : (Environ.env * Evar.t * Evd.evar_info * EConstr.named_context * Evd.econstr) list ; sigma : Evd.evar_map @@ -2005,7 +2005,7 @@ let finish_derived ~f ~name ~entries = let ct = declare_constant ~name ~kind:Decls.(IsProof Proposition) lemma_def in [GlobRef.ConstRef ct] -let finish_proved_equations ~kind ~hook i proof_obj types sigma0 = +let finish_proved_equations ~pm ~kind ~hook i proof_obj types sigma0 = let obls = ref 1 in let sigma, recobls = @@ -2022,8 +2022,8 @@ let finish_proved_equations ~kind ~hook i proof_obj types sigma0 = sigma, cst) sigma0 types proof_obj.entries in - hook recobls sigma; - List.map (fun cst -> GlobRef.ConstRef cst) recobls + let pm = hook ~pm recobls sigma in + pm, List.map (fun cst -> GlobRef.ConstRef cst) recobls let check_single_entry { entries; uctx } label = match entries with @@ -2044,7 +2044,7 @@ let finalize_proof ~pm proof_obj proof_info = pm, finish_derived ~f ~name ~entries:proof_obj.entries | End_equations { hook; i; types; sigma } -> let kind = proof_info.Proof_info.info.Info.kind in - pm, finish_proved_equations ~kind ~hook i proof_obj types sigma + finish_proved_equations ~pm ~kind ~hook i proof_obj types sigma let err_save_forbidden_in_place_of_qed () = CErrors.user_err (Pp.str "Cannot use Save with more than one constant or in this proof mode") diff --git a/vernac/declare.mli b/vernac/declare.mli index 9d9516d963..d302f68153 100644 --- a/vernac/declare.mli +++ b/vernac/declare.mli @@ -182,7 +182,7 @@ module Proof : sig val start_equations : name:Id.t -> info:Info.t - -> hook:(Constant.t list -> Evd.evar_map -> unit) + -> hook:(pm:OblState.t -> Constant.t list -> Evd.evar_map -> OblState.t) -> types:(Environ.env * Evar.t * Evd.evar_info * EConstr.named_context * Evd.econstr) list -> Evd.evar_map -> Proofview.telescope -- cgit v1.2.3 From 22e2ab01dd9fe4d6b6afb6d1bb171cbf11db4a3f Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Mon, 29 Jun 2020 17:03:39 +0200 Subject: [ci] Overlay for metacoq and rewriter --- .../11836-ejgallego-obligations+functional.sh | 14 ++++++++++---- 1 file changed, 10 insertions(+), 4 deletions(-) diff --git a/dev/ci/user-overlays/11836-ejgallego-obligations+functional.sh b/dev/ci/user-overlays/11836-ejgallego-obligations+functional.sh index 232ca2bf0d..72ec55a37c 100644 --- a/dev/ci/user-overlays/11836-ejgallego-obligations+functional.sh +++ b/dev/ci/user-overlays/11836-ejgallego-obligations+functional.sh @@ -1,12 +1,18 @@ if [ "$CI_PULL_REQUEST" = "11836" ] || [ "$CI_BRANCH" = "obligations+functional" ]; then - equations_CI_REF=obligations+functional - equations_CI_GITURL=https://github.com/ejgallego/Coq-Equations + mtac2_CI_REF=obligations+functional + mtac2_CI_GITURL=https://github.com/ejgallego/Mtac2 paramcoq_CI_REF=obligations+functional paramcoq_CI_GITURL=https://github.com/ejgallego/paramcoq - mtac2_CI_REF=obligations+functional - mtac2_CI_GITURL=https://github.com/ejgallego/Mtac2 + equations_CI_REF=obligations+functional + equations_CI_GITURL=https://github.com/ejgallego/Coq-Equations + + metacoq_CI_REF=obligations+functional + metacoq_CI_GITURL=https://github.com/ejgallego/metacoq + + rewriter_CI_REF=obligations+functional + rewriter_CI_GITURL=https://github.com/ejgallego/rewriter fi -- cgit v1.2.3 From 3ef2bd35926a83fbcfd34d03e1fb1db894a39627 Mon Sep 17 00:00:00 2001 From: Gaëtan Gilbert Date: Wed, 8 Jul 2020 14:06:19 +0200 Subject: declare: Add [save_regular] API for obligation-ignoring proofs --- plugins/funind/functional_principles_proofs.ml | 5 ++--- plugins/funind/gen_principle.ml | 14 ++++++-------- plugins/funind/recdef.ml | 15 ++++++--------- vernac/declare.ml | 8 ++++++++ vernac/declare.mli | 7 +++++++ 5 files changed, 29 insertions(+), 20 deletions(-) diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml index b743329e7d..743afe4177 100644 --- a/plugins/funind/functional_principles_proofs.ml +++ b/plugins/funind/functional_principles_proofs.ml @@ -863,9 +863,8 @@ let generate_equation_lemma evd fnames f fun_num nb_params nb_args rec_args_num let lemma, _ = Declare.Proof.by (Proofview.V82.tactic prove_replacement) lemma in - let pm = Declare.OblState.empty in - let _pm, _ = - Declare.Proof.save ~pm ~proof:lemma ~opaque:Vernacexpr.Transparent + let (_ : _ list) = + Declare.Proof.save_regular ~proof:lemma ~opaque:Vernacexpr.Transparent ~idopt:None in evd diff --git a/plugins/funind/gen_principle.ml b/plugins/funind/gen_principle.ml index 730cf42fe8..45b1713441 100644 --- a/plugins/funind/gen_principle.ml +++ b/plugins/funind/gen_principle.ml @@ -1526,10 +1526,9 @@ let derive_correctness (funs : Constr.pconstant list) (graphs : inductive list) let lemma = fst @@ Declare.Proof.by (Proofview.V82.tactic (proving_tac i)) lemma in - let pm = Declare.OblState.empty in - let _pm, _ = - Declare.Proof.save ~pm ~proof:lemma ~opaque:Vernacexpr.Transparent - ~idopt:None + let (_ : _ list) = + Declare.Proof.save_regular ~proof:lemma + ~opaque:Vernacexpr.Transparent ~idopt:None in let finfo = match find_Function_infos (fst f_as_constant) with @@ -1599,10 +1598,9 @@ let derive_correctness (funs : Constr.pconstant list) (graphs : inductive list) (proving_tac i))) lemma) in - let pm = Declare.OblState.empty in - let _pm, _ = - Declare.Proof.save ~pm ~proof:lemma ~opaque:Vernacexpr.Transparent - ~idopt:None + let (_ : _ list) = + Declare.Proof.save_regular ~proof:lemma + ~opaque:Vernacexpr.Transparent ~idopt:None in let finfo = match find_Function_infos (fst f_as_constant) with diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml index 7b00191026..253c95fa67 100644 --- a/plugins/funind/recdef.ml +++ b/plugins/funind/recdef.ml @@ -58,9 +58,8 @@ let declare_fun name kind ?univs value = (Declare.declare_constant ~name ~kind (Declare.DefinitionEntry ce)) let defined lemma = - let pm = Declare.OblState.empty in - let _pm, _ = - Declare.Proof.save ~pm ~proof:lemma ~opaque:Vernacexpr.Transparent + let (_ : _ list) = + Declare.Proof.save_regular ~proof:lemma ~opaque:Vernacexpr.Transparent ~idopt:None in () @@ -1504,9 +1503,8 @@ let open_new_goal ~lemma build_proof sigma using_lemmas ref_ goal_name [Hints.Hint_db.empty TransparentState.empty false] ])) in let lemma = build_proof env (Evd.from_env env) start_tac end_tac in - let pm = Declare.OblState.empty in - let _pm, _ = - Declare.Proof.save ~pm ~proof:lemma ~opaque:opacity ~idopt:None + let (_ : _ list) = + Declare.Proof.save_regular ~proof:lemma ~opaque:opacity ~idopt:None in () in @@ -1666,9 +1664,8 @@ let com_eqn uctx nb_arg eq_name functional_ref f_ref terminate_ref let _ = Flags.silently (fun () -> - let pm = Declare.OblState.empty in - let _pm = - Declare.Proof.save ~pm ~proof:lemma ~opaque:opacity ~idopt:None + let (_ : _ list) = + Declare.Proof.save_regular ~proof:lemma ~opaque:opacity ~idopt:None in ()) () diff --git a/vernac/declare.ml b/vernac/declare.ml index e19eca9a1c..df75e121d8 100644 --- a/vernac/declare.ml +++ b/vernac/declare.ml @@ -2068,6 +2068,14 @@ let save ~pm ~proof ~opaque ~idopt = let proof_info = process_idopt_for_save ~idopt proof.pinfo in finalize_proof ~pm proof_obj proof_info +let save_regular ~proof ~opaque ~idopt = + let open Proof_ending in + match CEphemeron.default proof.pinfo.Proof_info.proof_ending Regular with + | Regular -> + let (_, grs) : Obls_.State.t * _ = save ~pm:Obls_.State.empty ~proof ~opaque ~idopt in + grs + | _ -> CErrors.anomaly Pp.(str "save_regular: unexpected proof ending") + (***********************************************************************) (* Special case to close a lemma without forcing a proof *) (***********************************************************************) diff --git a/vernac/declare.mli b/vernac/declare.mli index d302f68153..adb5bd026f 100644 --- a/vernac/declare.mli +++ b/vernac/declare.mli @@ -214,6 +214,13 @@ module Proof : sig -> idopt:Names.lident option -> OblState.t * GlobRef.t list + (** For proofs known to have [Regular] ending, no need to touch program state. *) + val save_regular + : proof:t + -> opaque:Vernacexpr.opacity_flag + -> idopt:Names.lident option + -> GlobRef.t list + (** Admit a proof *) val save_admitted : pm:OblState.t -> proof:t -> OblState.t -- cgit v1.2.3