aboutsummaryrefslogtreecommitdiff
path: root/plugins
diff options
context:
space:
mode:
Diffstat (limited to 'plugins')
-rw-r--r--plugins/subtac/g_subtac.ml441
-rw-r--r--plugins/subtac/subtac_obligations.ml85
2 files changed, 69 insertions, 57 deletions
diff --git a/plugins/subtac/g_subtac.ml4 b/plugins/subtac/g_subtac.ml4
index c1e168da17..071ffb2c5a 100644
--- a/plugins/subtac/g_subtac.ml4
+++ b/plugins/subtac/g_subtac.ml4
@@ -101,41 +101,52 @@ VERNAC COMMAND EXTEND Subtac
[ "Program" subtac_gallina_loc(g) ] -> [ Subtac.subtac g ]
END
+let try_catch_exn f e =
+ try f e
+ with exn -> errorlabstrm "Program" (Cerrors.explain_exn exn)
+
+let subtac_obligation e = try_catch_exn Subtac_obligations.subtac_obligation e
+let next_obligation e = try_catch_exn Subtac_obligations.next_obligation e
+let try_solve_obligation e = try_catch_exn Subtac_obligations.try_solve_obligation e
+let try_solve_obligations e = try_catch_exn Subtac_obligations.try_solve_obligations e
+let solve_all_obligations e = try_catch_exn Subtac_obligations.solve_all_obligations e
+let admit_obligations e = try_catch_exn Subtac_obligations.admit_obligations e
+
VERNAC COMMAND EXTEND Subtac_Obligations
-| [ "Obligation" integer(num) "of" ident(name) ":" lconstr(t) ] -> [ Subtac_obligations.subtac_obligation (num, Some name, Some t) ]
-| [ "Obligation" integer(num) "of" ident(name) ] -> [ Subtac_obligations.subtac_obligation (num, Some name, None) ]
-| [ "Obligation" integer(num) ":" lconstr(t) ] -> [ Subtac_obligations.subtac_obligation (num, None, Some t) ]
-| [ "Obligation" integer(num) ] -> [ Subtac_obligations.subtac_obligation (num, None, None) ]
-| [ "Next" "Obligation" "of" ident(name) ] -> [ Subtac_obligations.next_obligation (Some name) ]
-| [ "Next" "Obligation" ] -> [ Subtac_obligations.next_obligation None ]
+| [ "Obligation" integer(num) "of" ident(name) ":" lconstr(t) ] -> [ subtac_obligation (num, Some name, Some t) ]
+| [ "Obligation" integer(num) "of" ident(name) ] -> [ subtac_obligation (num, Some name, None) ]
+| [ "Obligation" integer(num) ":" lconstr(t) ] -> [ subtac_obligation (num, None, Some t) ]
+| [ "Obligation" integer(num) ] -> [ subtac_obligation (num, None, None) ]
+| [ "Next" "Obligation" "of" ident(name) ] -> [ next_obligation (Some name) ]
+| [ "Next" "Obligation" ] -> [ next_obligation None ]
END
VERNAC COMMAND EXTEND Subtac_Solve_Obligation
| [ "Solve" "Obligation" integer(num) "of" ident(name) "using" tactic(t) ] ->
- [ Subtac_obligations.try_solve_obligation num (Some name) (Some (Tacinterp.interp t)) ]
+ [ try_solve_obligation num (Some name) (Some (Tacinterp.interp t)) ]
| [ "Solve" "Obligation" integer(num) "using" tactic(t) ] ->
- [ Subtac_obligations.try_solve_obligation num None (Some (Tacinterp.interp t)) ]
+ [ try_solve_obligation num None (Some (Tacinterp.interp t)) ]
END
VERNAC COMMAND EXTEND Subtac_Solve_Obligations
| [ "Solve" "Obligations" "of" ident(name) "using" tactic(t) ] ->
- [ Subtac_obligations.try_solve_obligations (Some name) (Some (Tacinterp.interp t)) ]
+ [ try_solve_obligations (Some name) (Some (Tacinterp.interp t)) ]
| [ "Solve" "Obligations" "using" tactic(t) ] ->
- [ Subtac_obligations.try_solve_obligations None (Some (Tacinterp.interp t)) ]
+ [ try_solve_obligations None (Some (Tacinterp.interp t)) ]
| [ "Solve" "Obligations" ] ->
- [ Subtac_obligations.try_solve_obligations None None ]
+ [ try_solve_obligations None None ]
END
VERNAC COMMAND EXTEND Subtac_Solve_All_Obligations
| [ "Solve" "All" "Obligations" "using" tactic(t) ] ->
- [ Subtac_obligations.solve_all_obligations (Some (Tacinterp.interp t)) ]
+ [ solve_all_obligations (Some (Tacinterp.interp t)) ]
| [ "Solve" "All" "Obligations" ] ->
- [ Subtac_obligations.solve_all_obligations None ]
+ [ solve_all_obligations None ]
END
VERNAC COMMAND EXTEND Subtac_Admit_Obligations
-| [ "Admit" "Obligations" "of" ident(name) ] -> [ Subtac_obligations.admit_obligations (Some name) ]
-| [ "Admit" "Obligations" ] -> [ Subtac_obligations.admit_obligations None ]
+| [ "Admit" "Obligations" "of" ident(name) ] -> [ admit_obligations (Some name) ]
+| [ "Admit" "Obligations" ] -> [ admit_obligations None ]
END
VERNAC COMMAND EXTEND Subtac_Set_Solver
diff --git a/plugins/subtac/subtac_obligations.ml b/plugins/subtac/subtac_obligations.ml
index 74ac787064..c4efef11b1 100644
--- a/plugins/subtac/subtac_obligations.ml
+++ b/plugins/subtac/subtac_obligations.ml
@@ -1,4 +1,4 @@
-(* -*- compile-command: "make -C ../.. bin/coqtop.byte" -*- *)
+(* -*- compile-command: "make -C ../.. plugins/subtac/subtac_plugin.cma" -*- *)
open Printf
open Pp
open Subtac_utils
@@ -347,23 +347,21 @@ let update_obls prg obls rem =
if rem > 0 then Remain rem
else (
match prg'.prg_deps with
- [] ->
- let kn = declare_definition prg' in
- from_prg := ProgMap.remove prg.prg_name !from_prg;
- Defined kn
- | l ->
- let progs = List.map (fun x -> ProgMap.find x !from_prg) prg'.prg_deps in
- if List.for_all (fun x -> obligations_solved x) progs then
- (let kn = declare_mutual_definition progs in
- from_prg := List.fold_left
- (fun acc x ->
- ProgMap.remove x.prg_name acc) !from_prg progs;
- Defined (ConstRef kn))
- else Dependent);
- in
- update_state (!from_prg, !default_tactic_expr);
- res
-
+ | [] ->
+ let kn = declare_definition prg' in
+ from_prg := ProgMap.remove prg.prg_name !from_prg;
+ Defined kn
+ | l ->
+ let progs = List.map (fun x -> ProgMap.find x !from_prg) prg'.prg_deps in
+ if List.for_all (fun x -> obligations_solved x) progs then
+ (let kn = declare_mutual_definition progs in
+ from_prg := List.fold_left
+ (fun acc x ->
+ ProgMap.remove x.prg_name acc) !from_prg progs;
+ Defined (ConstRef kn))
+ else Dependent);
+ in update_state (!from_prg, !default_tactic_expr); res
+
let is_defined obls x = obls.(x).obl_body <> None
let deps_remaining obls deps =
@@ -421,7 +419,10 @@ let rec solve_obligation prg num =
in
let obls = Array.copy obls in
let _ = obls.(num) <- obl in
- match update_obls prg obls (pred rem) with
+ let res = try update_obls prg obls (pred rem)
+ with e -> pperror (Cerrors.explain_exn e)
+ in
+ match res with
| Remain n when n > 0 ->
if has_dependencies obls num then
ignore(auto_solve_obligations (Some prg.prg_name) None)
@@ -447,30 +448,30 @@ and subtac_obligation (user_num, name, typ) =
and solve_obligation_by_tac prg obls i tac =
let obl = obls.(i) in
- match obl.obl_body with
- Some _ -> false
+ match obl.obl_body with
+ | Some _ -> false
| None ->
- (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
- obls.(i) <- declare_obligation obl t;
- true
- else false
- with
- | Stdpp.Exc_located(_, Proof_type.LtacLocated (_, Refiner.FailError (_, s)))
- | Stdpp.Exc_located(_, Refiner.FailError (_, s))
- | Refiner.FailError (_, s) ->
- user_err_loc (obl.obl_location, "solve_obligation", Lazy.force s)
- | e -> false)
+ 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
+ obls.(i) <- declare_obligation obl t;
+ true
+ else false
+ with
+ | Stdpp.Exc_located(_, Proof_type.LtacLocated (_, Refiner.FailError (_, s)))
+ | Stdpp.Exc_located(_, Refiner.FailError (_, s))
+ | Refiner.FailError (_, s) ->
+ user_err_loc (obl.obl_location, "solve_obligation", Lazy.force s)
+ | e -> false
and solve_prg_obligations prg tac =
let obls, rem = prg.prg_obligations in
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-01 12:32:33 +0000