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.ml246
1 files changed, 136 insertions, 110 deletions
diff --git a/contrib/subtac/subtac_obligations.ml b/contrib/subtac/subtac_obligations.ml
index a393e2c9..cc1e2dde 100644
--- a/contrib/subtac/subtac_obligations.ml
+++ b/contrib/subtac/subtac_obligations.ml
@@ -1,7 +1,9 @@
+(* -*- compile-command: "make -C ../.. bin/coqtop.byte" -*- *)
open Printf
open Pp
open Subtac_utils
open Command
+open Environ
open Term
open Names
@@ -13,9 +15,11 @@ open Decl_kinds
open Util
open Evd
open Declare
+open Proof_type
type definition_hook = global_reference -> unit
+let ppwarn cmd = Pp.warn (str"Program:" ++ cmd)
let pperror cmd = Util.errorlabstrm "Program" cmd
let error s = pperror (str s)
@@ -25,15 +29,17 @@ 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 * loc * bool * Intset.t) array
-
+type obligation_info = (Names.identifier * Term.types * loc * obligation_definition_status * Intset.t
+ * Tacexpr.raw_tactic_expr option) array
+
type obligation =
{ obl_name : identifier;
obl_type : types;
obl_location : loc;
obl_body : constr option;
- obl_opaque : bool;
+ obl_status : obligation_definition_status;
obl_deps : Intset.t;
+ obl_tac : Tacexpr.raw_tactic_expr option;
}
type obligations = (obligation array * int)
@@ -79,22 +85,29 @@ let _ =
let evar_of_obligation o = make_evar (Global.named_context_val ()) o.obl_type
-let subst_deps obls deps t =
- Intset.fold
- (fun x acc ->
- let xobl = obls.(x) in
- debug 3 (str "Trying to get body of obligation " ++ int x);
- let oblb =
- try Option.get xobl.obl_body
- with _ ->
- debug 3 (str "Couldn't get body of obligation " ++ int x);
- assert(false)
- in
- Term.subst1 oblb (Term.subst_var xobl.obl_name acc))
- deps t
-
+let get_obligation_body expand obl =
+ let c = Option.get obl.obl_body in
+ if expand && obl.obl_status = Expand then
+ match kind_of_term c with
+ | Const c -> constant_value (Global.env ()) c
+ | _ -> c
+ else c
+
+let subst_deps expand obls deps t =
+ let subst =
+ Intset.fold
+ (fun x acc ->
+ let xobl = obls.(x) in
+ let oblb =
+ try get_obligation_body expand xobl
+ with _ -> assert(false)
+ in (xobl.obl_name, oblb) :: acc)
+ deps []
+ in(* Termops.it_mkNamedProd_or_LetIn t subst *)
+ Term.replace_vars subst t
+
let subst_deps_obl obls obl =
- let t' = subst_deps obls obl.obl_deps obl.obl_type in
+ let t' = subst_deps false obls obl.obl_deps obl.obl_type in
{ obl with obl_type = t' }
module ProgMap = Map.Make(struct type t = identifier let compare = compare end)
@@ -150,14 +163,14 @@ let rec intset_to = function
-1 -> Intset.empty
| n -> Intset.add n (intset_to (pred n))
-let subst_body prg =
+let subst_body expand prg =
let obls, _ = prg.prg_obligations in
let ints = intset_to (pred (Array.length obls)) in
- subst_deps obls ints prg.prg_body,
- subst_deps obls ints (Termops.refresh_universes prg.prg_type)
+ subst_deps expand obls ints prg.prg_body,
+ subst_deps expand obls ints (Termops.refresh_universes prg.prg_type)
let declare_definition prg =
- let body, typ = subst_body prg in
+ let body, typ = subst_body false prg in
(try trace (str "Declaring: " ++ Ppconstr.pr_id prg.prg_name ++ spc () ++
my_print_constr (Global.env()) body ++ str " : " ++
my_print_constr (Global.env()) prg.prg_type);
@@ -188,7 +201,7 @@ let declare_definition prg =
in
let gr = ConstRef c in
if Impargs.is_implicit_args () || prg.prg_implicits <> [] then
- Impargs.declare_manual_implicits false gr (Impargs.is_implicit_args ()) prg.prg_implicits;
+ Impargs.declare_manual_implicits false gr prg.prg_implicits;
print_message (Subtac_utils.definition_message prg.prg_name);
prg.prg_hook gr;
gr
@@ -216,14 +229,18 @@ let compute_possible_guardness_evidences (n,_) fixbody fixtype =
let ctx = fst (Sign.decompose_prod_n_assum m fixtype) in
list_map_i (fun i _ -> i) 0 ctx
+let reduce_fix =
+ Reductionops.clos_norm_flags Closure.betaiotazeta (Global.env ()) Evd.empty
+
let declare_mutual_definition l =
let len = List.length l in
let fixdefs, fixtypes, fiximps =
list_split3
(List.map (fun x ->
- let subs, typ = (subst_body x) in
+ let subs, typ = (subst_body false x) in
snd (decompose_lam_n len subs), snd (decompose_prod_n len typ), x.prg_implicits) l)
in
+(* let fixdefs = List.map reduce_fix fixdefs in *)
let fixkind = Option.get (List.hd l).prg_fixkind in
let arrrec, recvec = Array.of_list fixtypes, Array.of_list fixdefs in
let fixdecls = (Array.of_list (List.map (fun x -> Name x.prg_name) l), arrrec, recvec) in
@@ -248,41 +265,33 @@ let declare_mutual_definition l =
(match List.hd kns with ConstRef kn -> kn | _ -> assert false)
let declare_obligation obl body =
- let ce =
- { const_entry_body = body;
- const_entry_type = Some obl.obl_type;
- const_entry_opaque = if get_proofs_transparency () then false else obl.obl_opaque;
- const_entry_boxed = false}
- in
- let constant = Declare.declare_constant obl.obl_name
- (DefinitionEntry ce,IsProof Property)
- in
- print_message (Subtac_utils.definition_message obl.obl_name);
- { obl with obl_body = Some (mkConst constant) }
-
-let try_tactics obls =
- Array.map
- (fun obl ->
- match obl.obl_body with
- None ->
- (try
- let ev = evar_of_obligation obl in
- let c = Subtac_utils.solve_by_tac ev Auto.default_full_auto in
- declare_obligation obl c
- with _ -> obl)
- | _ -> obl)
- obls
-
+ match obl.obl_status with
+ | Expand -> { obl with obl_body = Some body }
+ | Define opaque ->
+ let ce =
+ { const_entry_body = body;
+ const_entry_type = Some obl.obl_type;
+ const_entry_opaque =
+ (if get_proofs_transparency () then false
+ else opaque) ;
+ const_entry_boxed = false}
+ in
+ let constant = Declare.declare_constant obl.obl_name
+ (DefinitionEntry ce,IsProof Property)
+ in
+ print_message (Subtac_utils.definition_message obl.obl_name);
+ { obl with obl_body = Some (mkConst constant) }
+
let red = Reductionops.nf_betaiota
let init_prog_info n b t deps fixkind notations obls impls kind hook =
let obls' =
Array.mapi
- (fun i (n, t, l, o, d) ->
+ (fun i (n, t, l, o, d, tac) ->
debug 2 (str "Adding obligation " ++ int i ++ str " with deps : " ++ str (string_of_intset d));
{ obl_name = n ; obl_body = None;
- obl_location = l; obl_type = red t; obl_opaque = o;
- obl_deps = d })
+ obl_location = l; obl_type = red t; obl_status = o;
+ obl_deps = d; obl_tac = tac })
obls
in
{ prg_name = n ; prg_body = b; prg_type = red t; prg_obligations = (obls', Array.length obls');
@@ -369,22 +378,16 @@ let has_dependencies obls n =
!res
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_location = dummy_loc;
- obl_body = None;
- obl_opaque = false;
- obl_deps = Intset.empty;
- }) evars)
- in arr, Array.length arr
+ match o with
+ | Define false | Expand -> Subtac_utils.goal_kind
+ | _ -> Subtac_utils.goal_proof_kind
+
+let not_transp_msg =
+ str "Obligation should be transparent but was declared opaque." ++ spc () ++
+ str"Use 'Defined' instead."
+
+let warn_not_transp () = ppwarn not_transp_msg
+let error_not_transp () = pperror not_transp_msg
let rec solve_obligation prg num =
let user_num = succ num in
@@ -394,26 +397,37 @@ let rec solve_obligation prg num =
pperror (str "Obligation" ++ spc () ++ int user_num ++ str "already" ++ spc() ++ str "solved.")
else
match deps_remaining obls obl.obl_deps with
- [] ->
- let obl = subst_deps_obl obls obl in
- 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
- match update_obls prg obls (pred rem) with
- | Remain n when n > 0 ->
- if has_dependencies obls num then
- ignore(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;
- Flags.if_verbose (fun () -> msg (Printer.pr_open_subgoals ())) ()
- | 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 obl = subst_deps_obl obls obl in
+ Command.start_proof obl.obl_name (kind_of_opacity obl.obl_status) obl.obl_type
+ (fun strength gr ->
+ let cst = match gr with ConstRef cst -> cst | _ -> assert false in
+ let obl =
+ let transparent = evaluable_constant cst (Global.env ()) in
+ let body =
+ match obl.obl_status with
+ | Expand ->
+ if not transparent then error_not_transp ()
+ else constant_value (Global.env ()) cst
+ | Define opaque ->
+ if not opaque && not transparent then error_not_transp ()
+ else Libnames.constr_of_global gr
+ in { obl with obl_body = Some body }
+ in
+ let obls = Array.copy obls in
+ let _ = obls.(num) <- obl in
+ match update_obls prg obls (pred rem) with
+ | Remain n when n > 0 ->
+ if has_dependencies obls num then
+ ignore(auto_solve_obligations (Some prg.prg_name) None)
+ | _ -> ());
+ trace (str "Started obligation " ++ int user_num ++ str " proof: " ++
+ Subtac_utils.my_print_constr (Global.env ()) obl.obl_type);
+ Pfedit.by !default_tactic;
+ Flags.if_verbose (fun () -> msg (Printer.pr_open_subgoals ())) ()
+ | l -> pperror (str "Obligation " ++ int user_num ++ str " depends on obligation(s) "
+ ++ str (string_of_list ", " (fun x -> string_of_int (succ x)) l))
+
and subtac_obligation (user_num, name, typ) =
let num = pred user_num in
let prg = get_prog_err name in
@@ -434,12 +448,17 @@ and solve_obligation_by_tac prg obls i tac =
(try
if 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 -> Tacinterp.interp t
+ | None -> !default_tactic
+ in
let t = Subtac_utils.solve_by_tac (evar_of_obligation obl) tac in
- if obl.obl_opaque then
- obls.(i) <- declare_obligation obl t
- else
- obls.(i) <- { obl with obl_body = Some t };
- true
+ obls.(i) <- declare_obligation obl t;
+ true
else false
with
| Stdpp.Exc_located(_, Proof_type.LtacLocated (_, Refiner.FailError (_, s)))
@@ -473,34 +492,40 @@ and try_solve_obligation n prg tac =
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 : progress =
+and auto_solve_obligations n tac : progress =
Flags.if_verbose msgnl (str "Solving obligations automatically...");
- try solve_obligations n !default_tactic with NoObligations _ -> Dependent
+ try solve_prg_obligations (get_prog_err n) tac with NoObligations _ -> Dependent
open Pp
let show_obligations ?(msg=true) n =
let prg = get_prog_err n in
let n = prg.prg_name in
let obls, rem = prg.prg_obligations in
+ let showed = ref 5 in
if msg then msgnl (int rem ++ str " obligation(s) remaining: ");
Array.iteri (fun i x ->
match x.obl_body with
- None -> msgnl (str "Obligation" ++ spc() ++ int (succ i) ++ spc () ++ str "of" ++ spc() ++ str (string_of_id n) ++ str ":" ++ spc () ++
- my_print_constr (Global.env ()) x.obl_type ++ str "." ++ fnl ())
- | Some _ -> ())
+ | None ->
+ if !showed > 0 then (
+ decr showed;
+ msgnl (str "Obligation" ++ spc() ++ int (succ i) ++ spc () ++
+ str "of" ++ spc() ++ str (string_of_id n) ++ str ":" ++ spc () ++
+ hov 1 (my_print_constr (Global.env ()) x.obl_type ++ str "." ++ fnl ())))
+ | Some _ -> ())
obls
-
+
let show_term n =
let prg = get_prog_err n in
let n = prg.prg_name in
- msgnl (str (string_of_id n) ++ spc () ++ str":" ++ spc () ++ my_print_constr (Global.env ()) prg.prg_type ++ spc () ++ str ":=" ++ fnl ()
+ msgnl (str (string_of_id n) ++ spc () ++ str":" ++ spc () ++
+ my_print_constr (Global.env ()) prg.prg_type ++ spc () ++ str ":=" ++ fnl ()
++ my_print_constr (Global.env ()) prg.prg_body)
-let add_definition n b t ?(implicits=[]) ?(kind=Global,false,Definition) ?(hook=fun x -> ()) obls =
+let add_definition n b t ?(implicits=[]) ?(kind=Global,false,Definition) ?tactic ?(hook=fun x -> ()) obls =
Flags.if_verbose pp (str (string_of_id n) ++ str " has type-checked");
let prg = init_prog_info n b t [] None [] obls implicits kind hook in
let obls,_ = prg.prg_obligations in
@@ -513,12 +538,12 @@ let add_definition n b t ?(implicits=[]) ?(kind=Global,false,Definition) ?(hook=
let len = Array.length obls in
let _ = Flags.if_verbose ppnl (str ", generating " ++ int len ++ str " obligation(s)") in
from_prg := ProgMap.add n prg !from_prg;
- let res = auto_solve_obligations (Some n) in
+ let res = auto_solve_obligations (Some n) tactic in
match res with
- | Remain rem when rem < 5 -> Flags.if_verbose (fun () -> show_obligations ~msg:false (Some n)) (); res
- | _ -> res)
+ | Remain rem -> Flags.if_verbose (fun () -> show_obligations ~msg:false (Some n)) (); res
+ | _ -> res)
-let add_mutual_definitions l ?(kind=Global,false,Definition) notations fixkind =
+let add_mutual_definitions l ?tactic ?(kind=Global,false,Definition) notations fixkind =
let deps = List.map (fun (n, b, t, imps, obls) -> n) l in
let upd = List.fold_left
(fun acc (n, b, t, imps, obls) ->
@@ -531,8 +556,9 @@ let add_mutual_definitions l ?(kind=Global,false,Definition) notations fixkind =
List.fold_left (fun finished x ->
if finished then finished
else
- match auto_solve_obligations (Some x) with
- Defined _ -> (* If one definition is turned into a constant, the whole block is defined. *) true
+ 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. *) true
| _ -> false)
false deps
in ()
@@ -562,8 +588,8 @@ 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
+ try array_find (fun x -> x.obl_body = None && deps_remaining obls x.obl_deps = []) obls
+ with Not_found -> anomaly "Could not find a solvable obligation."
in solve_obligation prg i
let default_tactic () = !default_tactic
generated by cgit v1.2.3 (git 2.39.1) at 2025-01-12 23:22:06 +0000