diff options
| -rw-r--r-- | plugins/ltac/g_obligations.mlg | 8 | ||||
| -rw-r--r-- | vernac/classes.ml | 2 | ||||
| -rw-r--r-- | vernac/comDefinition.ml | 5 | ||||
| -rw-r--r-- | vernac/comProgramFixpoint.ml | 4 | ||||
| -rw-r--r-- | vernac/declare.ml | 414 | ||||
| -rw-r--r-- | vernac/declare.mli | 200 | ||||
| -rw-r--r-- | vernac/obligations.ml | 407 | ||||
| -rw-r--r-- | vernac/obligations.mli | 121 | ||||
| -rw-r--r-- | vernac/vernac.mllib | 1 | ||||
| -rw-r--r-- | vernac/vernacentries.ml | 4 |
10 files changed, 531 insertions, 635 deletions
diff --git a/plugins/ltac/g_obligations.mlg b/plugins/ltac/g_obligations.mlg index 498b33d1a8..81ee6ed5bb 100644 --- a/plugins/ltac/g_obligations.mlg +++ b/plugins/ltac/g_obligations.mlg @@ -28,7 +28,7 @@ let () = let tac = Proofview.tclBIND (Proofview.tclUNIT ()) begin fun () -> snd (get_default_tactic ()) end in - Obligations.default_tactic := tac + Declare.Obls.default_tactic := tac let with_tac f tac = let env = Genintern.empty_glob_sign (Global.env ()) in @@ -78,10 +78,10 @@ GRAMMAR EXTEND Gram { -open Obligations +open Declare.Obls -let obligation obl tac = with_tac (fun t -> Obligations.obligation obl t) tac -let next_obligation obl tac = with_tac (fun t -> Obligations.next_obligation obl t) tac +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 classify_obbl _ = Vernacextend.(VtStartProof (Doesn'tGuaranteeOpacity,[])) diff --git a/vernac/classes.ml b/vernac/classes.ml index 04321ed844..f02474a405 100644 --- a/vernac/classes.ml +++ b/vernac/classes.ml @@ -350,7 +350,7 @@ let declare_instance_program env sigma ~global ~poly name pri impargs udecl term let cinfo = Declare.CInfo.make ~name ~typ ~impargs () in let info = Declare.Info.make ~udecl ~scope ~poly ~kind ~hook () in let _ : Declare.progress = - Obligations.add_definition ~cinfo ~info ~term ~uctx obls + Declare.Obls.add_definition ~cinfo ~info ~term ~uctx obls in () let declare_instance_open sigma ?hook ~tac ~global ~poly id pri impargs udecl ids term termtype = diff --git a/vernac/comDefinition.ml b/vernac/comDefinition.ml index 537f713e82..5860626917 100644 --- a/vernac/comDefinition.ml +++ b/vernac/comDefinition.ml @@ -127,10 +127,9 @@ let do_definition_program ?hook ~name ~scope ~poly ~kind udecl bl red_option c c let (body, types), evd, udecl, impargs = interp_definition ~program_mode udecl bl ~poly red_option c ctypopt in - let term, typ, uctx, obls = Declare.prepare_obligation ~name ~body ~types evd in + let term, typ, uctx, obls = Declare.Obls.prepare_obligation ~name ~body ~types evd in let _ : Declare.progress = let cinfo = Declare.CInfo.make ~name ~typ ~impargs () in let info = Declare.Info.make ~udecl ~scope ~poly ~kind ?hook () in - Obligations.add_definition - ~cinfo ~info ~term ~uctx obls + Declare.Obls.add_definition ~cinfo ~info ~term ~uctx obls in () diff --git a/vernac/comProgramFixpoint.ml b/vernac/comProgramFixpoint.ml index 381b6cb9fa..b04aaa7e6f 100644 --- a/vernac/comProgramFixpoint.ml +++ b/vernac/comProgramFixpoint.ml @@ -262,7 +262,7 @@ 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.progress = Obligations.add_definition ~cinfo ~info ~term:evars_def ~uctx evars in + let _ : Declare.progress = Declare.Obls.add_definition ~cinfo ~info ~term:evars_def ~uctx evars in () let out_def = function @@ -322,7 +322,7 @@ 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 - Obligations.add_mutual_definitions defs ~info ~uctx ~ntns fixkind + Declare.Obls.add_mutual_definitions defs ~info ~uctx ~ntns fixkind let do_fixpoint ~scope ~poly l = let g = List.map (fun { Vernacexpr.rec_order } -> rec_order) l in diff --git a/vernac/declare.ml b/vernac/declare.ml index 0c66341190..514656a414 100644 --- a/vernac/declare.ml +++ b/vernac/declare.ml @@ -691,7 +691,7 @@ type obligation_resolver = type obligation_qed_info = {name : Id.t; num : int; auto : obligation_resolver} -module Obls = struct +module Obls_ = struct open Constr @@ -973,7 +973,6 @@ module State = struct let prg_ref, prg_tag = Summary.ref_tag ProgMap.empty ~name:"program-tcc-table" - let num_pending () = num_pending !prg_ref 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 @@ -1332,6 +1331,8 @@ module Proof_ending = struct end +(* Alias *) +module Proof_ = Proof module Proof = struct module Proof_info = struct @@ -1943,7 +1944,7 @@ let finish_admitted ~pinfo ~uctx pe = (* 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 oinfo uctx (List.hd cst) | _ -> () let save_admitted ~proof = @@ -2035,7 +2036,7 @@ let finalize_proof proof_obj 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 ~entry ~uctx ~oinfo | End_derive { f ; name } -> finish_derived ~f ~name ~entries:proof_obj.entries | End_equations { hook; i; types; sigma } -> @@ -2099,3 +2100,408 @@ let _ = Ind_tables.declare_definition_scheme := declare_definition_scheme let _ = Abstract.declare_abstract := Proof.declare_abstract let build_by_tactic = Proof.build_by_tactic + +(* This module could be merged with Obl, and placed before [Proof], + however there is a single dependency on [Proof.start] for the interactive case *) +module Obls = struct +(* For the records fields, opens should go away one these types are private *) +open Obls_ +open Obls_.Obligation +open Obls_.ProgramDecl + +let reduce c = + let env = Global.env () in + let sigma = Evd.from_env env in + EConstr.Unsafe.to_constr (Reductionops.clos_norm_flags CClosure.betaiota env sigma (EConstr.of_constr c)) + +let explain_no_obligations = function + Some ident -> str "No obligations for program " ++ Id.print ident + | None -> str "No obligations remaining" + +module Error = struct + + let no_obligations n = + CErrors.user_err (explain_no_obligations n) + + let ambiguous_program id ids = + CErrors.user_err + Pp.(str "More than one program with unsolved obligations: " ++ prlist Id.print ids + ++ str "; use the \"of\" clause to specify, as in \"Obligation 1 of " ++ Id.print id ++ str "\"") + + let unknown_obligation num = + CErrors.user_err (Pp.str (Printf.sprintf "Unknown obligation number %i" (succ num))) + + let already_solved num = + CErrors.user_err + ( str "Obligation" ++ spc () ++ int num ++ str "already" ++ spc () + ++ str "solved." ) + + let depends num rem = + CErrors.user_err + ( str "Obligation " ++ int num + ++ str " depends on obligation(s) " + ++ pr_sequence (fun x -> int (succ x)) rem) + +end + +let default_tactic = ref (Proofview.tclUNIT ()) + +let evar_of_obligation o = Evd.make_evar (Global.named_context_val ()) (EConstr.of_constr o.obl_type) + +let subst_deps expand obls deps t = + let osubst = Obls_.obl_substitution expand obls deps in + (Vars.replace_vars (List.map (fun (n, (_, b)) -> n, b) osubst) t) + +let subst_deps_obl obls obl = + let t' = subst_deps true obls obl.obl_deps obl.obl_type in + Obligation.set_type ~typ:t' obl + +open Evd + +let is_defined obls x = not (Option.is_empty obls.(x).obl_body) + +let deps_remaining obls deps = + Int.Set.fold + (fun x acc -> + if is_defined obls x then acc + else x :: acc) + deps [] + +let goal_kind = Decls.(IsDefinition Definition) +let goal_proof_kind = Decls.(IsProof Lemma) + +let kind_of_obligation o = + match o with + | Evar_kinds.Define false + | Evar_kinds.Expand -> goal_kind + | _ -> goal_proof_kind + +(* Solve an obligation using tactics, return the corresponding proof term *) +let warn_solve_errored = + CWarnings.create ~name:"solve_obligation_error" ~category:"tactics" + (fun err -> + Pp.seq + [ str "Solve Obligations tactic returned error: " + ; err + ; fnl () + ; str "This will become an error in the future" ]) + +let solve_by_tac ?loc name evi t ~poly ~uctx = + (* the status is dropped. *) + try + let env = Global.env () in + let body, types, _univs, _, uctx = + build_by_tactic env ~uctx ~poly ~typ:evi.evar_concl t in + Inductiveops.control_only_guard env (Evd.from_ctx uctx) (EConstr.of_constr body); + Some (body, types, uctx) + with + | Refiner.FailError (_, s) as exn -> + let _ = Exninfo.capture exn in + CErrors.user_err ?loc ~hdr:"solve_obligation" (Lazy.force s) + (* If the proof is open we absorb the error and leave the obligation open *) + | Proof_.OpenProof _ -> + None + | e when CErrors.noncritical e -> + let err = CErrors.print e in + warn_solve_errored ?loc err; + None + +let get_unique_prog prg = + match State.get_unique_open_prog prg with + | Ok prg -> prg + | Error [] -> + Error.no_obligations None + | Error ((id :: _) as ids) -> + Error.ambiguous_program id ids + +let rec solve_obligation prg num tac = + let user_num = succ num in + let { obls; remaining=rem } = Internal.get_obligations prg in + let obl = obls.(num) in + let remaining = deps_remaining obls obl.obl_deps in + let () = + if not (Option.is_empty obl.obl_body) + then Error.already_solved user_num; + if not (List.is_empty remaining) + then Error.depends user_num remaining + in + let obl = subst_deps_obl obls obl in + let scope = Locality.Global Locality.ImportNeedQualified in + 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 proof_ending = + let name = Internal.get_name prg in + Proof_ending.End_obligation {name; num; auto} + in + let cinfo = CInfo.make ~name:obl.obl_name ~typ:(EConstr.of_constr obl.obl_type) () in + let poly = Internal.get_poly prg in + let info = Info.make ~scope ~kind ~poly () in + let lemma = Proof.start ~cinfo ~info ~proof_ending evd in + let lemma = fst @@ Proof.by !default_tactic lemma in + let lemma = Option.cata (fun tac -> Proof.set_endline_tactic tac lemma) lemma tac in + lemma + +and obligation (user_num, name, typ) tac = + let num = pred user_num in + let prg = get_unique_prog name in + let { obls; remaining } = Internal.get_obligations prg in + if num >= 0 && num < Array.length obls then + let obl = obls.(num) in + match obl.obl_body with + | None -> solve_obligation prg num tac + | Some r -> Error.already_solved num + else Error.unknown_obligation num + +and solve_obligation_by_tac prg obls i tac = + let obl = obls.(i) in + match obl.obl_body with + | Some _ -> None + | None -> + if List.is_empty (deps_remaining obls obl.obl_deps) then + let obl = subst_deps_obl obls obl in + let tac = + match tac with + | Some t -> t + | None -> + match obl.obl_tac with + | Some t -> t + | None -> !default_tactic + in + let uctx = Internal.get_uctx prg in + let uctx = UState.update_sigma_env uctx (Global.env ()) in + let poly = Internal.get_poly prg in + match solve_by_tac ?loc:(fst obl.obl_location) obl.obl_name (evar_of_obligation obl) tac ~poly ~uctx with + | None -> None + | Some (t, ty, uctx) -> + let prg = ProgramDecl.Internal.set_uctx ~uctx prg in + let def, obl' = declare_obligation prg obl ~body:t ~types:ty ~uctx in + obls.(i) <- obl'; + if def && not poly then ( + (* Declare the term constraints with the first obligation only *) + let uctx_global = UState.from_env (Global.env ()) in + let uctx = UState.merge_subst uctx_global (UState.subst uctx) in + Some (ProgramDecl.Internal.set_uctx ~uctx prg)) + else Some prg + else None + +and solve_prg_obligations prg ?oblset tac = + let { obls; remaining } = Internal.get_obligations prg in + let rem = ref remaining in + let obls' = Array.copy obls in + let set = ref Int.Set.empty in + let p = match oblset with + | None -> (fun _ -> true) + | Some s -> set := s; + (fun i -> Int.Set.mem i !set) + in + let (), prg = + Array.fold_left_i + (fun i ((), prg) x -> + if p i then ( + match solve_obligation_by_tac prg obls' i tac with + | None -> (), prg + | Some prg -> + let deps = dependencies obls i in + set := Int.Set.union !set deps; + decr rem; + (), prg) + else (), prg) + ((), prg) obls' + in + update_obls prg obls' !rem + +and solve_obligations n tac = + let prg = get_unique_prog n in + solve_prg_obligations prg tac + +and solve_all_obligations tac = + State.fold ~init:() ~f:(fun k v () -> + let _ = solve_prg_obligations v tac in ()) + +and try_solve_obligation n prg tac = + let prg = get_unique_prog 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 -> () + +and try_solve_obligations n tac = + let _ = solve_obligations n tac in + () + +and auto_solve_obligations n ?oblset tac : 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 show_single_obligation i n obls x = + let x = subst_deps_obl obls x in + let env = Global.env () in + let sigma = Evd.from_env env in + let msg = + str "Obligation" ++ spc () + ++ int (succ i) + ++ spc () ++ str "of" ++ spc () ++ Id.print n ++ str ":" ++ spc () + ++ hov 1 (Printer.pr_constr_env env sigma x.obl_type + ++ str "." ++ fnl ()) in + Feedback.msg_info msg + +let show_obligations_of_prg ?(msg = true) prg = + let n = Internal.get_name prg in + let {obls; remaining} = Internal.get_obligations prg in + let showed = ref 5 in + if msg then Feedback.msg_info (int remaining ++ str " obligation(s) remaining: "); + Array.iteri + (fun i x -> + match x.obl_body with + | None -> + if !showed > 0 then begin + decr showed; + show_single_obligation i n obls x + end + | Some _ -> ()) + obls + +let show_obligations ?(msg = true) n = + let progs = + match n with + | None -> + State.all () + | Some n -> + (match State.find 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 + ProgramDecl.show prg + +let msg_generating_obl name obls = + let len = Array.length obls in + let info = Id.print name ++ str " has type-checked" in + Feedback.msg_info + (if len = 0 then info ++ str "." + else + info ++ str ", generating " ++ int len ++ + str (String.plural len " obligation")) + +let add_definition ~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 + in + let name = CInfo.get_name cinfo in + 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) + 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 + match res with + | Remain rem -> + Flags.if_verbose (show_obligations ~msg:false) (Some name); + res + | _ -> res + +let add_mutual_definitions l ~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) -> + 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 + 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 + match res with + | Defined _ -> + (* If one definition is turned into a constant, + the whole block is defined. *) + (pm, true) + | _ -> (pm, false)) + (pm, false) deps + in + pm + +let admit_prog prg = + let {obls; remaining} = Internal.get_obligations prg in + let obls = Array.copy obls in + Array.iteri + (fun i x -> + match x.obl_body with + | None -> + let x = subst_deps_obl obls x in + let uctx = Internal.get_uctx prg in + let univs = UState.univ_entry ~poly:false uctx in + let kn = declare_constant ~name:x.obl_name ~local:Locality.ImportNeedQualified + (ParameterEntry (None, (x.obl_type, univs), None)) ~kind:Decls.(IsAssumption Conjectural) + in + assumption_message x.obl_name; + obls.(i) <- Obligation.set_body ~body:(DefinedObl (kn, Univ.Instance.empty)) x + | Some _ -> ()) + obls; + Obls_.update_obls prg obls 0 + +(* get_any_prog *) +let rec admit_all_obligations () = + let prg = State.first_pending () in + match prg with + | None -> () + | Some prg -> + let _prog = admit_prog prg in + admit_all_obligations () + +let admit_obligations n = + match n with + | None -> admit_all_obligations () + | Some _ -> + let prg = get_unique_prog n in + let _ = admit_prog prg in + () + +let next_obligation n tac = + let prg = match n with + | None -> State.first_pending () |> Option.get + | Some _ -> get_unique_prog 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 + let i = match Array.findi is_open obls with + | Some i -> i + | None -> CErrors.anomaly (Pp.str "Could not find a solvable obligation.") + in + solve_obligation prg i tac + +let check_program_libraries () = + Coqlib.check_required_library Coqlib.datatypes_module_name; + Coqlib.check_required_library ["Coq";"Init";"Specif"]; + 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 = + | IsFixpoint of lident option list | IsCoFixpoint + +end diff --git a/vernac/declare.mli b/vernac/declare.mli index 3ae704c561..b6efa333b7 100644 --- a/vernac/declare.mli +++ b/vernac/declare.mli @@ -417,117 +417,137 @@ val build_by_tactic (** {2 Program mode API} *) -(** Prepare API, to be removed once we provide the corresponding 1-step API *) -val prepare_obligation - : name:Id.t - -> types:EConstr.t option - -> body:EConstr.t - -> Evd.evar_map - -> Constr.constr * Constr.types * UState.t * RetrieveObl.obligation_info - -module Obls : sig +(** Coq's Program mode support. This mode extends declarations of + constants and fixpoints with [Program Definition] and [Program + Fixpoint] to support incremental construction of terms using + delayed proofs, called "obligations" + + The mode also provides facilities for managing and auto-solving + sets of obligations. + + The basic code flow of programs/obligations is as follows: + + - [add_definition] / [add_mutual_definitions] are called from the + respective [Program] vernacular command interpretation; at this + point the only extra work we do is to prepare the new definition + [d] using [RetrieveObl], which consists in turning unsolved evars + into obligations. [d] is not sent to the kernel yet, as it is not + complete and cannot be typchecked, but saved in a special + data-structure. Auto-solving of obligations is tried at this stage + (see below) + + - [next_obligation] will retrieve the next obligation + ([RetrieveObl] sorts them by topological order) and will try to + solve it. When all obligations are solved, the original constant + [d] is grounded and sent to the kernel for addition to the global + environment. Auto-solving of obligations is also triggered on + obligation completion. + +{2} Solving of obligations: Solved obligations are stored as regular + global declarations in the global environment, usually with name + [constant_obligation_number] where [constant] is the original + [constant] and [number] is the corresponding (internal) number. + + Solving an obligation can trigger a bit of a complex cascaded + callback path; closing an obligation can indeed allow all other + obligations to be closed, which in turn may trigged the declaration + of the original constant. Care must be taken, as this can modify + [Global.env] in arbitrarily ways. Current code takes some care to + refresh the [env] in the proper boundaries, but the invariants + remain delicate. + +{2} Saving of obligations: as open obligations use the regular proof + mode, a `Qed` will call `Lemmas.save_lemma` first. For this reason + obligations code is split in two: this file, [Obligations], taking + care of the top-level vernac commands, and [Declare], which is + called by `Lemmas` to close an obligation proof and eventually to + declare the top-level [Program]ed constant. -type 'a obligation_body = DefinedObl of 'a | TermObl of Constr.constr - -module Obligation : sig - type t = private - { obl_name : Id.t - ; obl_type : Constr.types - ; obl_location : Evar_kinds.t Loc.located - ; obl_body : Constr.pconstant obligation_body option - ; obl_status : bool * Evar_kinds.obligation_definition_status - ; obl_deps : Int.Set.t - ; obl_tac : unit Proofview.tactic option } + *) - val set_type : typ:Constr.types -> t -> t - val set_body : body:Constr.pconstant obligation_body -> t -> t -end +module Obls : sig -type obligations = {obls : Obligation.t array; remaining : int} type fixpoint_kind = IsFixpoint of lident option list | IsCoFixpoint -(* Information about a single [Program {Definition,Lemma,..}] declaration *) -module ProgramDecl : sig +module State : sig + (* Internal *) type t - - val make : - info:Info.t - -> cinfo:Constr.types CInfo.t - -> opaque:bool - -> ntns:Vernacexpr.decl_notation list - -> reduce:(Constr.constr -> Constr.constr) - -> deps:Names.Id.t list - -> uctx:UState.t - -> body:Constr.constr option - -> fixpoint_kind:fixpoint_kind option - -> RetrieveObl.obligation_info - -> t - - val show : t -> Pp.t - - (* This is internal, only here as obligations get merged into the - regular declaration path *) - module Internal : sig - val get_poly : t -> bool - val get_name : t -> Id.t - val get_uctx : t -> UState.t - val set_uctx : uctx:UState.t -> t -> t - val get_obligations : t -> obligations - end + val prg_tag : t Summary.Dyn.tag end -(** [declare_obligation prg obl ~uctx ~types ~body] Save an obligation - [obl] for program definition [prg] *) -val declare_obligation : - ProgramDecl.t - -> Obligation.t - -> uctx:UState.t - -> types:Constr.types option - -> body:Constr.types - -> bool * Obligation.t - -module State : sig +(** Check obligations are properly solved before closing the + [what_for] section / module *) +val check_solved_obligations : what_for:Pp.t -> unit - val num_pending : unit -> int - val first_pending : unit -> ProgramDecl.t option +val default_tactic : unit Proofview.tactic ref - (** Returns [Error duplicate_list] if not a single program is open *) - val get_unique_open_prog : - Id.t option -> (ProgramDecl.t, Id.t list) result +(** Prepare API, to be removed once we provide the corresponding 1-step API *) +val prepare_obligation + : name:Id.t + -> types:EConstr.t option + -> body:EConstr.t + -> Evd.evar_map + -> Constr.constr * Constr.types * UState.t * RetrieveObl.obligation_info - (** Add a new obligation *) - val add : Id.t -> ProgramDecl.t -> unit +(** Start a [Program Definition c] proof. [uctx] [udecl] [impargs] + [kind] [scope] [poly] etc... come from the interpretation of the + vernacular; `obligation_info` was generated by [RetrieveObl] It + 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 + -> info:Info.t + -> ?term:Constr.t + -> uctx:UState.t + -> ?tactic:unit Proofview.tactic + -> ?reduce:(Constr.t -> Constr.t) + -> ?opaque:bool + -> RetrieveObl.obligation_info + -> progress - val fold : f:(Id.t -> ProgramDecl.t -> 'a -> 'a) -> init:'a -> 'a +(* XXX: unify with MutualEntry *) - val all : unit -> ProgramDecl.t list +(** Start a [Program Fixpoint] declaration, similar to the above, + except it takes a list now. *) +val add_mutual_definitions : + (Constr.t CInfo.t * Constr.t * RetrieveObl.obligation_info) list + -> info:Info.t + -> uctx:UState.t + -> ?tactic:unit Proofview.tactic + -> ?reduce:(Constr.t -> Constr.t) + -> ?opaque:bool + -> ntns:Vernacexpr.decl_notation list + -> fixpoint_kind + -> unit - val find : Id.t -> ProgramDecl.t option +(** Implementation of the [Obligation] command *) +val obligation : + int * Names.Id.t option * Constrexpr.constr_expr option + -> Genarg.glob_generic_argument option + -> Proof.t - (* Internal *) - type t - val prg_tag : t Summary.Dyn.tag -end +(** Implementation of the [Next Obligation] command *) +val next_obligation : + Names.Id.t option -> Genarg.glob_generic_argument option -> Proof.t -val declare_definition : ProgramDecl.t -> Names.GlobRef.t +(** Implementation of the [Solve Obligation] command *) +val solve_obligations : + Names.Id.t option -> unit Proofview.tactic option -> progress -(** [update_obls prg obls n progress] What does this do? *) -val update_obls : - ProgramDecl.t -> Obligation.t array -> int -> progress +val solve_all_obligations : unit Proofview.tactic option -> unit -(** Check obligations are properly solved before closing the - [what_for] section / module *) -val check_solved_obligations : what_for:Pp.t -> unit +(** Number of remaining obligations to be solved for this program *) +val try_solve_obligation : + int -> Names.Id.t option -> unit Proofview.tactic option -> unit -(** { 2 Util } *) +val try_solve_obligations : + Names.Id.t option -> unit Proofview.tactic option -> unit -val obl_substitution : - bool - -> Obligation.t array - -> Int.Set.t - -> (Id.t * (Constr.types * Constr.types)) list +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 dependencies : Obligation.t array -> int -> Int.Set.t +val check_program_libraries : unit -> unit end diff --git a/vernac/obligations.ml b/vernac/obligations.ml deleted file mode 100644 index 6e84d599c5..0000000000 --- a/vernac/obligations.ml +++ /dev/null @@ -1,407 +0,0 @@ -(************************************************************************) -(* * The Coq Proof Assistant / The Coq Development Team *) -(* v * Copyright INRIA, CNRS and contributors *) -(* <O___,, * (see version control and CREDITS file for authors & dates) *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(* * (see LICENSE file for the text of the license) *) -(************************************************************************) - -open Printf -open Names -open Pp -open Util - -(* For the records fields, opens should go away one these types are private *) -open Declare.Obls -open Declare.Obls.Obligation -open Declare.Obls.ProgramDecl - -let reduce c = - let env = Global.env () in - let sigma = Evd.from_env env in - EConstr.Unsafe.to_constr (Reductionops.clos_norm_flags CClosure.betaiota env sigma (EConstr.of_constr c)) - -let explain_no_obligations = function - Some ident -> str "No obligations for program " ++ Id.print ident - | None -> str "No obligations remaining" - -module Error = struct - - let no_obligations n = - CErrors.user_err (explain_no_obligations n) - - let ambiguous_program id ids = - CErrors.user_err - Pp.(str "More than one program with unsolved obligations: " ++ prlist Id.print ids - ++ str "; use the \"of\" clause to specify, as in \"Obligation 1 of " ++ Id.print id ++ str "\"") - - let unknown_obligation num = - CErrors.user_err (Pp.str (sprintf "Unknown obligation number %i" (succ num))) - - let already_solved num = - CErrors.user_err - ( str "Obligation" ++ spc () ++ int num ++ str "already" ++ spc () - ++ str "solved." ) - - let depends num rem = - CErrors.user_err - ( str "Obligation " ++ int num - ++ str " depends on obligation(s) " - ++ pr_sequence (fun x -> int (succ x)) rem) - -end - -let default_tactic = ref (Proofview.tclUNIT ()) - -let evar_of_obligation o = Evd.make_evar (Global.named_context_val ()) (EConstr.of_constr o.obl_type) - -let subst_deps expand obls deps t = - let osubst = Declare.Obls.obl_substitution expand obls deps in - (Vars.replace_vars (List.map (fun (n, (_, b)) -> n, b) osubst) t) - -let subst_deps_obl obls obl = - let t' = subst_deps true obls obl.obl_deps obl.obl_type in - Obligation.set_type ~typ:t' obl - -open Evd - -let is_defined obls x = not (Option.is_empty obls.(x).obl_body) - -let deps_remaining obls deps = - Int.Set.fold - (fun x acc -> - if is_defined obls x then acc - else x :: acc) - deps [] - -let goal_kind = Decls.(IsDefinition Definition) -let goal_proof_kind = Decls.(IsProof Lemma) - -let kind_of_obligation o = - match o with - | Evar_kinds.Define false - | Evar_kinds.Expand -> goal_kind - | _ -> goal_proof_kind - -(* Solve an obligation using tactics, return the corresponding proof term *) -let warn_solve_errored = - CWarnings.create ~name:"solve_obligation_error" ~category:"tactics" - (fun err -> - Pp.seq - [ str "Solve Obligations tactic returned error: " - ; err - ; fnl () - ; str "This will become an error in the future" ]) - -let solve_by_tac ?loc name evi t ~poly ~uctx = - (* the status is dropped. *) - try - let env = Global.env () in - let body, types, _univs, _, uctx = - Declare.build_by_tactic env ~uctx ~poly ~typ:evi.evar_concl t in - Inductiveops.control_only_guard env (Evd.from_ctx uctx) (EConstr.of_constr body); - Some (body, types, uctx) - with - | Refiner.FailError (_, s) as exn -> - let _ = Exninfo.capture exn in - CErrors.user_err ?loc ~hdr:"solve_obligation" (Lazy.force s) - (* If the proof is open we absorb the error and leave the obligation open *) - | Proof.OpenProof _ -> - None - | e when CErrors.noncritical e -> - let err = CErrors.print e in - warn_solve_errored ?loc err; - None - -let get_unique_prog prg = - match State.get_unique_open_prog prg with - | Ok prg -> prg - | Error [] -> - Error.no_obligations None - | Error ((id :: _) as ids) -> - Error.ambiguous_program id ids - -let rec solve_obligation prg num tac = - let user_num = succ num in - let { obls; remaining=rem } = Internal.get_obligations prg in - let obl = obls.(num) in - let remaining = deps_remaining obls obl.obl_deps in - let () = - if not (Option.is_empty obl.obl_body) - then Error.already_solved user_num; - if not (List.is_empty remaining) - then Error.depends user_num remaining - in - let obl = subst_deps_obl obls obl in - let scope = Locality.Global Locality.ImportNeedQualified in - 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 proof_ending = - let name = Internal.get_name prg in - Declare.Proof_ending.End_obligation {Declare.name; num; auto} - in - let cinfo = Declare.CInfo.make ~name:obl.obl_name ~typ:(EConstr.of_constr obl.obl_type) () in - let poly = Internal.get_poly prg in - let info = Declare.Info.make ~scope ~kind ~poly () in - let lemma = Declare.Proof.start ~cinfo ~info ~proof_ending evd in - let lemma = fst @@ Declare.Proof.by !default_tactic lemma in - let lemma = Option.cata (fun tac -> Declare.Proof.set_endline_tactic tac lemma) lemma tac in - lemma - -and obligation (user_num, name, typ) tac = - let num = pred user_num in - let prg = get_unique_prog name in - let { obls; remaining } = Internal.get_obligations prg in - if num >= 0 && num < Array.length obls then - let obl = obls.(num) in - match obl.obl_body with - | None -> solve_obligation prg num tac - | Some r -> Error.already_solved num - else Error.unknown_obligation num - -and solve_obligation_by_tac prg obls i tac = - let obl = obls.(i) in - match obl.obl_body with - | Some _ -> None - | None -> - if List.is_empty (deps_remaining obls obl.obl_deps) then - let obl = subst_deps_obl obls obl in - let tac = - match tac with - | Some t -> t - | None -> - match obl.obl_tac with - | Some t -> t - | None -> !default_tactic - in - let uctx = Internal.get_uctx prg in - let uctx = UState.update_sigma_env uctx (Global.env ()) in - let poly = Internal.get_poly prg in - match solve_by_tac ?loc:(fst obl.obl_location) obl.obl_name (evar_of_obligation obl) tac ~poly ~uctx with - | None -> None - | Some (t, ty, uctx) -> - let prg = ProgramDecl.Internal.set_uctx ~uctx prg in - let def, obl' = declare_obligation prg obl ~body:t ~types:ty ~uctx in - obls.(i) <- obl'; - if def && not poly then ( - (* Declare the term constraints with the first obligation only *) - let uctx_global = UState.from_env (Global.env ()) in - let uctx = UState.merge_subst uctx_global (UState.subst uctx) in - Some (ProgramDecl.Internal.set_uctx ~uctx prg)) - else Some prg - else None - -and solve_prg_obligations prg ?oblset tac = - let { obls; remaining } = Internal.get_obligations prg in - let rem = ref remaining in - let obls' = Array.copy obls in - let set = ref Int.Set.empty in - let p = match oblset with - | None -> (fun _ -> true) - | Some s -> set := s; - (fun i -> Int.Set.mem i !set) - in - let (), prg = - Array.fold_left_i - (fun i ((), prg) x -> - if p i then ( - match solve_obligation_by_tac prg obls' i tac with - | None -> (), prg - | Some prg -> - let deps = dependencies obls i in - set := Int.Set.union !set deps; - decr rem; - (), prg) - else (), prg) - ((), prg) obls' - in - update_obls prg obls' !rem - -and solve_obligations n tac = - let prg = get_unique_prog n in - solve_prg_obligations prg tac - -and solve_all_obligations tac = - State.fold ~init:() ~f:(fun k v () -> - let _ = solve_prg_obligations v tac in ()) - -and try_solve_obligation n prg tac = - let prg = get_unique_prog 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 -> () - -and try_solve_obligations n tac = - let _ = solve_obligations n tac in - () - -and auto_solve_obligations n ?oblset tac : Declare.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 show_single_obligation i n obls x = - let x = subst_deps_obl obls x in - let env = Global.env () in - let sigma = Evd.from_env env in - let msg = - str "Obligation" ++ spc () - ++ int (succ i) - ++ spc () ++ str "of" ++ spc () ++ Id.print n ++ str ":" ++ spc () - ++ hov 1 (Printer.pr_constr_env env sigma x.obl_type - ++ str "." ++ fnl ()) in - Feedback.msg_info msg - -let show_obligations_of_prg ?(msg = true) prg = - let n = Internal.get_name prg in - let {obls; remaining} = Internal.get_obligations prg in - let showed = ref 5 in - if msg then Feedback.msg_info (int remaining ++ str " obligation(s) remaining: "); - Array.iteri - (fun i x -> - match x.obl_body with - | None -> - if !showed > 0 then begin - decr showed; - show_single_obligation i n obls x - end - | Some _ -> ()) - obls - -let show_obligations ?(msg = true) n = - let progs = - match n with - | None -> - State.all () - | Some n -> - (match State.find 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 - ProgramDecl.show prg - -let msg_generating_obl name obls = - let len = Array.length obls in - let info = Id.print name ++ str " has type-checked" in - Feedback.msg_info - (if len = 0 then info ++ str "." - else - info ++ str ", generating " ++ int len ++ - str (String.plural len " obligation")) - -let add_definition ~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 - in - let name = Declare.CInfo.get_name cinfo in - 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 = Declare.Obls.declare_definition prg in - Declare.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 - match res with - | Declare.Remain rem -> - Flags.if_verbose (show_obligations ~msg:false) (Some name); - res - | _ -> res - -let add_mutual_definitions l ~info ~uctx - ?tactic ?(reduce = reduce) ?(opaque = false) ~ntns fixkind = - let deps = List.map (fun (ci,_,_) -> Declare.CInfo.get_name ci) l in - let pm = - List.fold_left - (fun () (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 (Declare.CInfo.get_name cinfo) prg) - () 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 - match res with - | Declare.Defined _ -> - (* If one definition is turned into a constant, - the whole block is defined. *) - (pm, true) - | _ -> (pm, false)) - (pm, false) deps - in - pm - -let admit_prog prg = - let {obls; remaining} = Internal.get_obligations prg in - let obls = Array.copy obls in - Array.iteri - (fun i x -> - match x.obl_body with - | None -> - let x = subst_deps_obl obls x in - let uctx = Internal.get_uctx prg in - let univs = UState.univ_entry ~poly:false uctx in - let kn = Declare.declare_constant ~name:x.obl_name ~local:Locality.ImportNeedQualified - (Declare.ParameterEntry (None, (x.obl_type, univs), None)) ~kind:Decls.(IsAssumption Conjectural) - in - Declare.assumption_message x.obl_name; - obls.(i) <- Obligation.set_body ~body:(DefinedObl (kn, Univ.Instance.empty)) x - | Some _ -> ()) - obls; - Declare.Obls.update_obls prg obls 0 - -(* get_any_prog *) -let rec admit_all_obligations () = - let prg = State.first_pending () in - match prg with - | None -> () - | Some prg -> - let _prog = admit_prog prg in - admit_all_obligations () - -let admit_obligations n = - match n with - | None -> admit_all_obligations () - | Some _ -> - let prg = get_unique_prog n in - let _ = admit_prog prg in - () - -let next_obligation n tac = - let prg = match n with - | None -> State.first_pending () |> Option.get - | Some _ -> get_unique_prog 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 - let i = match Array.findi is_open obls with - | Some i -> i - | None -> CErrors.anomaly (Pp.str "Could not find a solvable obligation.") - in - solve_obligation prg i tac - -let check_program_libraries () = - Coqlib.check_required_library Coqlib.datatypes_module_name; - Coqlib.check_required_library ["Coq";"Init";"Specif"]; - Coqlib.check_required_library ["Coq";"Program";"Tactics"] diff --git a/vernac/obligations.mli b/vernac/obligations.mli deleted file mode 100644 index 422d187373..0000000000 --- a/vernac/obligations.mli +++ /dev/null @@ -1,121 +0,0 @@ -(************************************************************************) -(* * The Coq Proof Assistant / The Coq Development Team *) -(* v * Copyright INRIA, CNRS and contributors *) -(* <O___,, * (see version control and CREDITS file for authors & dates) *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(* * (see LICENSE file for the text of the license) *) -(************************************************************************) - -open Constr - -(** Coq's Program mode support. This mode extends declarations of - constants and fixpoints with [Program Definition] and [Program - Fixpoint] to support incremental construction of terms using - delayed proofs, called "obligations" - - The mode also provides facilities for managing and auto-solving - sets of obligations. - - The basic code flow of programs/obligations is as follows: - - - [add_definition] / [add_mutual_definitions] are called from the - respective [Program] vernacular command interpretation; at this - point the only extra work we do is to prepare the new definition - [d] using [RetrieveObl], which consists in turning unsolved evars - into obligations. [d] is not sent to the kernel yet, as it is not - complete and cannot be typchecked, but saved in a special - data-structure. Auto-solving of obligations is tried at this stage - (see below) - - - [next_obligation] will retrieve the next obligation - ([RetrieveObl] sorts them by topological order) and will try to - solve it. When all obligations are solved, the original constant - [d] is grounded and sent to the kernel for addition to the global - environment. Auto-solving of obligations is also triggered on - obligation completion. - -{2} Solving of obligations: Solved obligations are stored as regular - global declarations in the global environment, usually with name - [constant_obligation_number] where [constant] is the original - [constant] and [number] is the corresponding (internal) number. - - Solving an obligation can trigger a bit of a complex cascaded - callback path; closing an obligation can indeed allow all other - obligations to be closed, which in turn may trigged the declaration - of the original constant. Care must be taken, as this can modify - [Global.env] in arbitrarily ways. Current code takes some care to - refresh the [env] in the proper boundaries, but the invariants - remain delicate. - -{2} Saving of obligations: as open obligations use the regular proof - mode, a `Qed` will call `Lemmas.save_lemma` first. For this reason - obligations code is split in two: this file, [Obligations], taking - care of the top-level vernac commands, and [Declare], which is - called by `Lemmas` to close an obligation proof and eventually to - declare the top-level [Program]ed constant. - - *) - -val default_tactic : unit Proofview.tactic ref - -(** Start a [Program Definition c] proof. [uctx] [udecl] [impargs] - [kind] [scope] [poly] etc... come from the interpretation of the - vernacular; `obligation_info` was generated by [RetrieveObl] It - will return whether all the obligations were solved; if so, it will - also register [c] with the kernel. *) -val add_definition : - cinfo:types Declare.CInfo.t - -> info:Declare.Info.t - -> ?term:constr - -> uctx:UState.t - -> ?tactic:unit Proofview.tactic - -> ?reduce:(constr -> constr) - -> ?opaque:bool - -> RetrieveObl.obligation_info - -> Declare.progress - -(* XXX: unify with MutualEntry *) - -(** Start a [Program Fixpoint] declaration, similar to the above, - except it takes a list now. *) -val add_mutual_definitions : - (Constr.t Declare.CInfo.t * Constr.t * RetrieveObl.obligation_info) list - -> info:Declare.Info.t - -> uctx:UState.t - -> ?tactic:unit Proofview.tactic - -> ?reduce:(constr -> constr) - -> ?opaque:bool - -> ntns:Vernacexpr.decl_notation list - -> Declare.Obls.fixpoint_kind - -> unit - -(** Implementation of the [Obligation] command *) -val obligation : - int * Names.Id.t option * Constrexpr.constr_expr option - -> Genarg.glob_generic_argument option - -> Declare.Proof.t - -(** Implementation of the [Next Obligation] command *) -val next_obligation : - Names.Id.t option -> Genarg.glob_generic_argument option -> Declare.Proof.t - -(** Implementation of the [Solve Obligation] command *) -val solve_obligations : - Names.Id.t option -> unit Proofview.tactic option -> Declare.progress - -val solve_all_obligations : unit Proofview.tactic option -> unit - -(** Number of remaining obligations to be solved for this program *) -val try_solve_obligation : - int -> Names.Id.t option -> unit Proofview.tactic option -> unit - -val try_solve_obligations : - Names.Id.t option -> unit Proofview.tactic option -> unit - -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 check_program_libraries : unit -> unit diff --git a/vernac/vernac.mllib b/vernac/vernac.mllib index 78f9b6098a..23dde0dd29 100644 --- a/vernac/vernac.mllib +++ b/vernac/vernac.mllib @@ -23,7 +23,6 @@ Library ComCoercion Auto_ind_decl Indschemes -Obligations ComDefinition Classes ComPrimitive diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml index c9d56395c2..1a276ecbad 100644 --- a/vernac/vernacentries.ml +++ b/vernac/vernacentries.ml @@ -84,7 +84,7 @@ let with_module_locality ~atts f = let with_def_attributes ~atts f = let atts = DefAttributes.parse atts in - if atts.DefAttributes.program then Obligations.check_program_libraries (); + if atts.DefAttributes.program then Declare.Obls.check_program_libraries (); f ~atts (*******************) @@ -471,7 +471,7 @@ let check_name_freshness locality {CAst.loc;v=id} : unit = user_err ?loc (Id.print id ++ str " already exists.") let program_inference_hook env sigma ev = - let tac = !Obligations.default_tactic in + let tac = !Declare.Obls.default_tactic in let evi = Evd.find sigma ev in let evi = Evarutil.nf_evar_info sigma evi in let env = Evd.evar_filtered_env env evi in |