[declare] Merge remaining obligations bits into Declare

This allows us to remove a large chunk of the internal API, and is the
pre-requisite to get rid of [Proof_ending], and even more refactoring
on the declare path.

1 files changed, 410 insertions, 4 deletions

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