summaryrefslogtreecommitdiff
path: root/contrib/interface/debug_tac.ml4
diff options
context:
space:
mode:
Diffstat (limited to 'contrib/interface/debug_tac.ml4')
-rw-r--r--contrib/interface/debug_tac.ml4148
1 files changed, 18 insertions, 130 deletions
diff --git a/contrib/interface/debug_tac.ml4 b/contrib/interface/debug_tac.ml4
index bf596b28..56abfb82 100644
--- a/contrib/interface/debug_tac.ml4
+++ b/contrib/interface/debug_tac.ml4
@@ -1,7 +1,5 @@
(*i camlp4deps: "parsing/grammar.cma" i*)
-open Ast;;
-open Coqast;;
open Tacmach;;
open Tacticals;;
open Proof_trees;;
@@ -12,6 +10,8 @@ open Proof_type;;
open Tacexpr;;
open Genarg;;
+let pr_glob_tactic = Pptactic.pr_glob_tactic (Global.env())
+
(* Compacting and uncompacting proof commands *)
type report_tree =
@@ -72,11 +72,6 @@ let check_subgoals_count2
Recursive_fail (List.hd !new_report_holder)));
result;;
-(*
-let traceable = function
- Node(_, "TACTICLIST", a::b::tl) -> true
- | _ -> false;;
-*)
let traceable = function
| TacThen _ | TacThens _ -> true
| _ -> false;;
@@ -116,25 +111,6 @@ let count_subgoals2
result;;
let rec local_interp : glob_tactic_expr -> report_holder -> tactic = function
-(*
- Node(_, "TACTICLIST", [a;Node(_, "TACLIST", l)]) ->
- (fun report_holder -> checked_thens report_holder a l)
- | Node(_, "TACTICLIST", a::((Node(_, "TACLIST", l))as b)::c::tl) ->
- local_interp(ope ("TACTICLIST", (ope("TACTICLIST", [a;b]))::c::tl))
- | Node(_, "TACTICLIST", [a;b]) ->
- (fun report_holder -> checked_then report_holder a b)
- | Node(_, "TACTICLIST", a::b::c::tl) ->
- local_interp(ope ("TACTICLIST", (ope("TACTICLIST", [a;b]))::c::tl))
- | ast ->
- (fun report_holder g ->
- try
- let (gls, _) as result = Tacinterp.interp ast g in
- report_holder := (Report_node(true, List.length (sig_it gls), []))
- ::!report_holder;
- result
- with e -> (report_holder := (Failed 1)::!report_holder;
- tclIDTAC g))
-*)
TacThens (a,l) ->
(fun report_holder -> checked_thens report_holder a l)
| TacThen (a,b) ->
@@ -263,9 +239,14 @@ and checked_then: report_holder -> glob_tactic_expr -> glob_tactic_expr -> tacti
by the list of integers given as extra arguments.
*)
+let rawwit_main_tactic = rawwit_tactic Pcoq.Tactic.tactic_main_level
+let globwit_main_tactic = globwit_tactic Pcoq.Tactic.tactic_main_level
+let wit_main_tactic = wit_tactic Pcoq.Tactic.tactic_main_level
+
+
let on_then = function [t1;t2;l] ->
- let t1 = out_gen wit_tactic t1 in
- let t2 = out_gen wit_tactic t2 in
+ let t1 = out_gen wit_main_tactic t1 in
+ let t2 = out_gen wit_main_tactic t2 in
let l = out_gen (wit_list0 wit_int) l in
tclTHEN_i (Tacinterp.eval_tactic t1)
(fun i ->
@@ -276,78 +257,18 @@ let on_then = function [t1;t2;l] ->
| _ -> anomaly "bad arguments for on_then";;
let mkOnThen t1 t2 selected_indices =
- let a = in_gen rawwit_tactic t1 in
- let b = in_gen rawwit_tactic t2 in
+ let a = in_gen rawwit_main_tactic t1 in
+ let b = in_gen rawwit_main_tactic t2 in
let l = in_gen (wit_list0 rawwit_int) selected_indices in
TacAtom (dummy_loc, TacExtend (dummy_loc, "OnThen", [a;b;l]));;
(* Analyzing error reports *)
-(*
-let rec select_success n = function
- [] -> []
- | Report_node(true,_,_)::tl -> (Num((0,0),n))::select_success (n+1) tl
- | _::tl -> select_success (n+1) tl;;
-*)
let rec select_success n = function
[] -> []
| Report_node(true,_,_)::tl -> n::select_success (n+1) tl
| _::tl -> select_success (n+1) tl;;
-(*
-let rec expand_tactic = function
- Node(loc1, "TACTICLIST", [a;Node(loc2,"TACLIST", l)]) ->
- Node(loc1, "TACTICLIST",
- [expand_tactic a;
- Node(loc2, "TACLIST", List.map expand_tactic l)])
- | Node(loc1, "TACTICLIST", a::((Node(loc2, "TACLIST", l))as b)::c::tl) ->
- expand_tactic (Node(loc1, "TACTICLIST",
- (Node(loc1, "TACTICLIST", [a;b]))::c::tl))
- | Node(loc1, "TACTICLIST", [a;b]) ->
- Node(loc1, "TACTICLIST",[expand_tactic a;expand_tactic b])
- | Node(loc1, "TACTICLIST", a::b::c::tl) ->
- expand_tactic (Node(loc1, "TACTICLIST",
- (Node(loc1, "TACTICLIST", [a;b]))::c::tl))
- | any -> any;;
-*)
-(* Useless: already in binary form...
-let rec expand_tactic = function
- TacThens (a,l) -> TacThens (expand_tactic a, List.map expand_tactic l)
- | TacThen (a,b) -> TacThen (expand_tactic a, expand_tactic b)
- | any -> any;;
-*)
-
-(*
-let rec reconstruct_success_tac ast =
- match ast with
- Node(_, "TACTICLIST", [a;Node(_,"TACLIST",l)]) ->
- (function
- Report_node(true, n, l) -> ast
- | Report_node(false, n, rl) ->
- ope("TACTICLIST",[a;ope("TACLIST",
- List.map2 reconstruct_success_tac l rl)])
- | Failed n -> ope("Idtac",[])
- | Tree_fail r -> reconstruct_success_tac a r
- | Mismatch (n,p) -> a)
- | Node(_, "TACTICLIST", [a;b]) ->
- (function
- Report_node(true, n, l) -> ast
- | Report_node(false, n, rl) ->
- let selected_indices = select_success 1 rl in
- ope("OnThen", a::b::selected_indices)
- | Failed n -> ope("Idtac",[])
- | Tree_fail r -> reconstruct_success_tac a r
- | _ -> error "this error case should not happen in a THEN tactic")
- | _ ->
- (function
- Report_node(true, n, l) -> ast
- | Failed n -> ope("Idtac",[])
- | _ ->
- errorlabstrm
- "this error case should not happen on an unknown tactic"
- (str "error in reconstruction with " ++ fnl () ++
- (gentacpr ast)));;
-*)
let rec reconstruct_success_tac (tac:glob_tactic_expr) =
match tac with
TacThens (a,l) ->
@@ -355,7 +276,7 @@ let rec reconstruct_success_tac (tac:glob_tactic_expr) =
Report_node(true, n, l) -> tac
| Report_node(false, n, rl) ->
TacThens (a,List.map2 reconstruct_success_tac l rl)
- | Failed n -> TacId ""
+ | Failed n -> TacId []
| Tree_fail r -> reconstruct_success_tac a r
| Mismatch (n,p) -> a)
| TacThen (a,b) ->
@@ -364,16 +285,16 @@ let rec reconstruct_success_tac (tac:glob_tactic_expr) =
| Report_node(false, n, rl) ->
let selected_indices = select_success 1 rl in
TacAtom (dummy_loc,TacExtend (dummy_loc,"OnThen",
- [in_gen globwit_tactic a;
- in_gen globwit_tactic b;
+ [in_gen globwit_main_tactic a;
+ in_gen globwit_main_tactic b;
in_gen (wit_list0 globwit_int) selected_indices]))
- | Failed n -> TacId ""
+ | Failed n -> TacId []
| Tree_fail r -> reconstruct_success_tac a r
| _ -> error "this error case should not happen in a THEN tactic")
| _ ->
(function
Report_node(true, n, l) -> tac
- | Failed n -> TacId ""
+ | Failed n -> TacId []
| _ ->
errorlabstrm
"this error case should not happen on an unknown tactic"
@@ -391,21 +312,6 @@ let rec path_to_first_error = function
p::(path_to_first_error t)
| _ -> [];;
-(*
-let rec flatten_then_list tail = function
- | Node(_, "TACTICLIST", [a;b]) ->
- flatten_then_list ((flatten_then b)::tail) a
- | ast -> ast::tail
-and flatten_then = function
- Node(_, "TACTICLIST", [a;b]) ->
- ope("TACTICLIST", flatten_then_list [flatten_then b] a)
- | Node(_, "TACLIST", l) ->
- ope("TACLIST", List.map flatten_then l)
- | Node(_, "OnThen", t1::t2::l) ->
- ope("OnThen", (flatten_then t1)::(flatten_then t2)::l)
- | ast -> ast;;
-*)
-
let debug_tac = function
[(Tacexp ast)] ->
(fun g ->
@@ -430,26 +336,8 @@ let debug_tac = function
add_tactic "DebugTac" debug_tac;;
*)
-(*
-hide_tactic "OnThen" on_then;;
-*)
Refiner.add_tactic "OnThen" on_then;;
-(*
-let rec clean_path p ast l =
- match ast, l with
- Node(_, "TACTICLIST", ([_;_] as tacs)), fst::tl ->
- fst::(clean_path 0 (List.nth tacs (fst - 1)) tl)
- | Node(_, "TACTICLIST", tacs), 2::tl ->
- let rank = (List.length tacs) - p in
- rank::(clean_path 0 (List.nth tacs (rank - 1)) tl)
- | Node(_, "TACTICLIST", tacs), 1::tl ->
- clean_path (p+1) ast tl
- | Node(_, "TACLIST", tacs), fst::tl ->
- fst::(clean_path 0 (List.nth tacs (fst - 1)) tl)
- | _, [] -> []
- | _, _ -> failwith "this case should not happen in clean_path";;
-*)
let rec clean_path tac l =
match tac, l with
| TacThen (a,b), fst::tl ->
@@ -554,8 +442,8 @@ let descr_first_error tac =
(msgnl (str "Execution of this tactic raised message " ++ fnl () ++
fnl () ++ Cerrors.explain_exn e ++ fnl () ++
fnl () ++ str "on goal" ++ fnl () ++
- pr_goal (sig_it (strip_some !the_goal)) ++ fnl () ++
- str "faulty tactic is" ++ fnl () ++ fnl () ++
+ Printer.pr_goal (sig_it (strip_some !the_goal)) ++
+ fnl () ++ str "faulty tactic is" ++ fnl () ++ fnl () ++
pr_glob_tactic ((*flatten_then*) !the_ast) ++ fnl ());
tclIDTAC g))
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-18 16:03:48 +0000