summaryrefslogtreecommitdiff
path: root/contrib/subtac/subtac_obligations.ml
diff options
context:
space:
mode:
Diffstat (limited to 'contrib/subtac/subtac_obligations.ml')
-rw-r--r--contrib/subtac/subtac_obligations.ml205
1 files changed, 133 insertions, 72 deletions
diff --git a/contrib/subtac/subtac_obligations.ml b/contrib/subtac/subtac_obligations.ml
index d6c1772f..d182f7cd 100644
--- a/contrib/subtac/subtac_obligations.ml
+++ b/contrib/subtac/subtac_obligations.ml
@@ -1,3 +1,4 @@
+(* -*- default-directory: "~/research/coq/trunk/" -*- *)
open Printf
open Pp
open Subtac_utils
@@ -12,12 +13,22 @@ open Decl_kinds
open Util
open Evd
-type obligation_info = (Names.identifier * Term.types * Intset.t) array
+let pperror cmd = Util.errorlabstrm "Subtac" cmd
+let error s = pperror (str s)
+
+exception NoObligations of identifier option
+
+let explain_no_obligations = function
+ Some ident -> str "No obligations for program " ++ str (string_of_id ident)
+ | None -> str "No obligations remaining"
+
+type obligation_info = (Names.identifier * Term.types * bool * Intset.t) array
type obligation =
{ obl_name : identifier;
obl_type : types;
obl_body : constr option;
+ obl_opaque : bool;
obl_deps : Intset.t;
}
@@ -36,8 +47,9 @@ let assumption_message id =
Options.if_verbose message ((string_of_id id) ^ " is assumed")
let default_tactic : Proof_type.tactic ref = ref Refiner.tclIDTAC
+let default_tactic_expr : Tacexpr.glob_tactic_expr ref = ref (Obj.magic ())
-let set_default_tactic t = default_tactic := t
+let set_default_tactic t = default_tactic_expr := t; default_tactic := Tacinterp.eval_tactic t
let evar_of_obligation o = { evar_hyps = Global.named_context_val () ;
evar_concl = o.obl_type ;
@@ -81,26 +93,35 @@ let map_first m =
let from_prg : program_info ProgMap.t ref = ref ProgMap.empty
+let freeze () = !from_prg, !default_tactic_expr
+let unfreeze (v, t) = from_prg := v; set_default_tactic t
+let init () =
+ from_prg := ProgMap.empty; set_default_tactic (Subtac_utils.utils_call "subtac_simpl" [])
+
let _ =
Summary.declare_summary "program-tcc-table"
- { Summary.freeze_function = (fun () -> !from_prg);
- Summary.unfreeze_function =
- (fun v -> from_prg := v);
- Summary.init_function =
- (fun () -> from_prg := ProgMap.empty);
+ { Summary.freeze_function = freeze;
+ Summary.unfreeze_function = unfreeze;
+ Summary.init_function = init;
Summary.survive_module = false;
Summary.survive_section = false }
-open Evd
+let progmap_union = ProgMap.fold ProgMap.add
-let terms_of_evar ev =
- match ev.evar_body with
- Evar_defined b ->
- let nc = Environ.named_context_of_val ev.evar_hyps in
- let body = Termops.it_mkNamedLambda_or_LetIn b nc in
- let typ = Termops.it_mkNamedProd_or_LetIn ev.evar_concl nc in
- body, typ
- | _ -> assert(false)
+let cache (_, (infos, tac)) =
+ from_prg := infos;
+ default_tactic_expr := tac
+
+let (input,output) =
+ declare_object
+ { (default_object "Program state") with
+ cache_function = cache;
+ load_function = (fun _ -> cache);
+ open_function = (fun _ -> cache);
+ classify_function = (fun _ -> Dispose);
+ export_function = (fun x -> Some x) }
+
+open Evd
let rec intset_to = function
-1 -> Intset.empty
@@ -113,7 +134,8 @@ let subst_body prg =
let declare_definition prg =
let body = subst_body prg in
(try trace (str "Declaring: " ++ Ppconstr.pr_id prg.prg_name ++ spc () ++
- my_print_constr (Global.env()) body);
+ my_print_constr (Global.env()) body ++ str " : " ++
+ my_print_constr (Global.env()) prg.prg_type);
with _ -> ());
let ce =
{ const_entry_body = body;
@@ -163,7 +185,7 @@ let declare_obligation obl body =
let ce =
{ const_entry_body = body;
const_entry_type = Some obl.obl_type;
- const_entry_opaque = false;
+ const_entry_opaque = obl.obl_opaque;
const_entry_boxed = false}
in
let constant = Declare.declare_constant obl.obl_name
@@ -190,42 +212,53 @@ let red = Reductionops.nf_betaiota
let init_prog_info n b t deps nvrec obls =
let obls' =
Array.mapi
- (fun i (n, t, d) ->
+ (fun i (n, t, o, d) ->
debug 2 (str "Adding obligation " ++ int i ++ str " with deps : " ++ str (string_of_intset d));
{ obl_name = n ; obl_body = None;
- obl_type = red t;
+ obl_type = red t; obl_opaque = o;
obl_deps = d })
obls
in
{ prg_name = n ; prg_body = b; prg_type = red t; prg_obligations = (obls', Array.length obls');
prg_deps = deps; prg_nvrec = nvrec; }
-let pperror cmd = Util.errorlabstrm "Subtac" cmd
-let error s = pperror (str s)
-
let get_prog name =
let prg_infos = !from_prg in
match name with
Some n ->
(try ProgMap.find n prg_infos
- with Not_found -> error ("No obligations for program " ^ string_of_id n))
+ with Not_found -> raise (NoObligations (Some n)))
| None ->
(let n = map_cardinal prg_infos in
match n with
- 0 -> error "No obligations remaining"
+ 0 -> raise (NoObligations None)
| 1 -> map_first prg_infos
| _ -> error "More than one program with unsolved obligations")
+let get_prog_err n =
+ try get_prog n with NoObligations id -> pperror (explain_no_obligations id)
+
let obligations_solved prg = (snd prg.prg_obligations) = 0
+let update_state s =
+(* msgnl (str "Updating obligations info"); *)
+ Lib.add_anonymous_leaf (input s)
+
+let obligations_message rem =
+ if rem > 0 then
+ if rem = 1 then
+ Options.if_verbose msgnl (int rem ++ str " obligation remaining")
+ else
+ Options.if_verbose msgnl (int rem ++ str " obligations remaining")
+ else
+ Options.if_verbose msgnl (str "No more obligations remaining")
+
let update_obls prg obls rem =
let prg' = { prg with prg_obligations = (obls, rem) } in
from_prg := map_replace prg.prg_name prg' !from_prg;
- if rem > 0 then (
- Options.if_verbose msgnl (int rem ++ str " obligation(s) remaining");
- )
+ obligations_message rem;
+ if rem > 0 then ()
else (
- Options.if_verbose msgnl (str "No more obligations remaining");
match prg'.prg_deps with
[] ->
declare_definition prg';
@@ -235,7 +268,10 @@ let update_obls prg obls rem =
if List.for_all (fun x -> obligations_solved x) progs then
(declare_mutual_definition progs;
from_prg := List.fold_left
- (fun acc x -> ProgMap.remove x.prg_name acc) !from_prg progs))
+ (fun acc x ->
+ ProgMap.remove x.prg_name acc) !from_prg progs));
+ update_state (!from_prg, !default_tactic_expr);
+ rem
let is_defined obls x = obls.(x).obl_body <> None
@@ -246,7 +282,24 @@ let deps_remaining obls deps =
else x :: acc)
deps []
-let solve_obligation prg num =
+let kind_of_opacity o =
+ if o then Subtac_utils.goal_proof_kind
+ else Subtac_utils.goal_kind
+
+let obligations_of_evars evars =
+ let arr =
+ Array.of_list
+ (List.map
+ (fun (n, t) ->
+ { obl_name = n;
+ obl_type = t;
+ obl_body = None;
+ obl_opaque = false;
+ obl_deps = Intset.empty;
+ }) evars)
+ in arr, Array.length arr
+
+let rec solve_obligation prg num =
let user_num = succ num in
let obls, rem = prg.prg_obligations in
let obl = obls.(num) in
@@ -256,22 +309,23 @@ let solve_obligation prg num =
match deps_remaining obls obl.obl_deps with
[] ->
let obl = subst_deps_obl obls obl in
- Command.start_proof obl.obl_name Subtac_utils.goal_proof_kind obl.obl_type
+ Command.start_proof obl.obl_name (kind_of_opacity obl.obl_opaque) obl.obl_type
(fun strength gr ->
debug 2 (str "Proof of obligation " ++ int user_num ++ str " finished");
let obl = { obl with obl_body = Some (Libnames.constr_of_global gr) } in
let obls = Array.copy obls in
let _ = obls.(num) <- obl in
- update_obls prg obls (pred rem));
+ if update_obls prg obls (pred rem) <> 0 then
+ auto_solve_obligations (Some prg.prg_name));
trace (str "Started obligation " ++ int user_num ++ str " proof: " ++
Subtac_utils.my_print_constr (Global.env ()) obl.obl_type);
Pfedit.by !default_tactic
| l -> pperror (str "Obligation " ++ int user_num ++ str " depends on obligation(s) "
++ str (string_of_list ", " (fun x -> string_of_int (succ x)) l))
-let subtac_obligation (user_num, name, typ) =
+and subtac_obligation (user_num, name, typ) =
let num = pred user_num in
- let prg = get_prog name in
+ let prg = get_prog_err name in
let obls, rem = prg.prg_obligations in
if num < Array.length obls then
let obl = obls.(num) in
@@ -280,20 +334,8 @@ let subtac_obligation (user_num, name, typ) =
| Some r -> error "Obligation already solved"
else error (sprintf "Unknown obligation number %i" (succ num))
-
-let obligations_of_evars evars =
- let arr =
- Array.of_list
- (List.map
- (fun (n, t) ->
- { obl_name = n;
- obl_type = t;
- obl_body = None;
- obl_deps = Intset.empty;
- }) evars)
- in arr, Array.length arr
-
-let solve_obligation_by_tac prg obls i tac =
+
+and solve_obligation_by_tac prg obls i tac =
let obl = obls.(i) in
match obl.obl_body with
Some _ -> false
@@ -302,13 +344,15 @@ let solve_obligation_by_tac prg obls i tac =
if deps_remaining obls obl.obl_deps = [] then
let obl = subst_deps_obl obls obl in
let t = Subtac_utils.solve_by_tac (evar_of_obligation obl) tac in
- obls.(i) <- { obl with obl_body = Some t };
+ if obl.obl_opaque then
+ obls.(i) <- declare_obligation obl t
+ else
+ obls.(i) <- { obl with obl_body = Some t };
true
else false
with _ -> false)
-let solve_obligations n tac =
- let prg = get_prog n in
+and solve_prg_obligations prg tac =
let obls, rem = prg.prg_obligations in
let rem = ref rem in
let obls' = Array.copy obls in
@@ -320,6 +364,27 @@ let solve_obligations n tac =
in
update_obls prg obls' !rem
+and solve_obligations n tac =
+ let prg = get_prog_err n in
+ solve_prg_obligations prg tac
+
+and solve_all_obligations tac =
+ ProgMap.iter (fun k v -> ignore(solve_prg_obligations v tac)) !from_prg
+
+and try_solve_obligation n prg tac =
+ let prg = get_prog prg in
+ let obls, rem = prg.prg_obligations in
+ let obls' = Array.copy obls in
+ if solve_obligation_by_tac prg obls' n tac then
+ ignore(update_obls prg obls' (pred rem));
+
+and try_solve_obligations n tac =
+ try ignore (solve_obligations n tac) with NoObligations _ -> ()
+
+and auto_solve_obligations n : unit =
+ Options.if_verbose msgnl (str "Solving obligations automatically...");
+ try_solve_obligations n !default_tactic
+
let add_definition n b t obls =
Options.if_verbose pp (str (string_of_id n) ++ str " has type-checked");
let prg = init_prog_info n b t [] (Array.make 0 0) obls in
@@ -332,7 +397,7 @@ let add_definition n b t obls =
let len = Array.length obls in
let _ = Options.if_verbose ppnl (str ", generating " ++ int len ++ str " obligation(s)") in
from_prg := ProgMap.add n prg !from_prg;
- solve_obligations (Some n) !default_tactic)
+ auto_solve_obligations (Some n))
let add_mutual_definitions l nvrec =
let deps = List.map (fun (n, b, t, obls) -> n) l in
@@ -343,22 +408,21 @@ let add_mutual_definitions l nvrec =
!from_prg l
in
from_prg := upd;
- List.iter (fun x -> solve_obligations (Some x) !default_tactic) deps
+ List.iter (fun x -> auto_solve_obligations (Some x)) deps
let admit_obligations n =
- let prg = get_prog n in
+ let prg = get_prog_err n in
let obls, rem = prg.prg_obligations in
- let obls' =
- Array.mapi (fun i x ->
+ Array.iteri (fun i x ->
match x.obl_body with
None ->
- let kn = Declare.declare_constant x.obl_name (ParameterEntry x.obl_type, IsAssumption Conjectural) in
- assumption_message x.obl_name;
- { x with obl_body = Some (mkConst kn) }
- | Some _ -> x)
- obls
- in
- update_obls prg obls' 0
+ let x = subst_deps_obl obls x in
+ let kn = Declare.declare_constant x.obl_name (ParameterEntry x.obl_type, IsAssumption Conjectural) in
+ assumption_message x.obl_name;
+ obls.(i) <- { x with obl_body = Some (mkConst kn) }
+ | Some _ -> ())
+ obls;
+ ignore(update_obls prg obls 0)
exception Found of int
@@ -367,21 +431,17 @@ let array_find f arr =
raise Not_found
with Found i -> i
-let rec next_obligation n =
- let prg = get_prog n in
+let next_obligation n =
+ let prg = get_prog_err n in
let obls, rem = prg.prg_obligations in
let i =
array_find (fun x -> x.obl_body = None && deps_remaining obls x.obl_deps = [])
obls
- in
- if solve_obligation_by_tac prg obls i !default_tactic then (
- update_obls prg obls (pred rem);
- next_obligation n
- ) else solve_obligation prg i
+ in solve_obligation prg i
open Pp
let show_obligations n =
- let prg = get_prog n in
+ let prg = get_prog_err n in
let n = prg.prg_name in
let obls, rem = prg.prg_obligations in
msgnl (int rem ++ str " obligation(s) remaining: ");
@@ -392,3 +452,4 @@ let show_obligations n =
| Some _ -> ())
obls
+let default_tactic () = !default_tactic
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-24 21:06:54 +0000