Directory 'contrib' renamed into 'plugins', to end confusion with archive of user contribs

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11996 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 458 insertions, 0 deletions

diff --git a/plugins/interface/debug_tac.ml4 b/plugins/interface/debug_tac.ml4
new file mode 100644
index 0000000000..aad3a765de
--- /dev/null
+++ b/plugins/interface/debug_tac.ml4
@@ -0,0 +1,458 @@
+(*i camlp4deps: "parsing/grammar.cma" i*)
+
+open Tacmach;;
+open Tacticals;;
+open Proof_trees;;
+open Pp;;
+open Pptactic;;
+open Util;;
+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 =
+    Report_node of bool *int * report_tree list
+  | Mismatch of int * int
+  | Tree_fail of report_tree
+  | Failed of int;;
+
+type report_card =
+    Ngoals of int
+  | Goals_mismatch of int
+  | Recursive_fail of report_tree
+  | Fail;;
+
+type card_holder = report_card ref;;
+type report_holder = report_tree list ref;;
+
+(* This tactical receives an integer and a tactic and checks that the
+   tactic produces that number of goals.  It never fails but signals failure
+   by updating the boolean reference given as third argument to false.
+   It is especially suited for use in checked_thens below. *)
+
+let check_subgoals_count : card_holder -> int -> bool ref -> tactic -> tactic =
+  fun card_holder count flag t g ->
+    try
+      let (gls, v) as result = t g in
+      let len = List.length (sig_it gls) in
+      card_holder :=
+      (if len = count then
+	  (flag := true;
+	  Ngoals count)
+       else
+          (flag := false;
+          Goals_mismatch len));
+      result
+    with
+      e -> card_holder := Fail;
+           flag := false;
+           tclIDTAC g;;
+
+let no_failure = function
+    [Report_node(true,_,_)] -> true
+  | _ -> false;;
+
+let check_subgoals_count2 
+    : card_holder -> int -> bool ref -> (report_holder -> tactic) -> tactic =
+  fun card_holder count flag t g ->
+    let new_report_holder = ref ([] : report_tree list) in
+    let (gls, v) as result = t new_report_holder g in
+    let succeeded = no_failure !new_report_holder in
+    let len = List.length (sig_it gls) in
+    card_holder :=
+      (if (len = count) & succeeded then
+	(flag := true;
+	 Ngoals count)
+      else
+	(flag := false;
+	 Recursive_fail (List.hd !new_report_holder)));
+    result;;
+
+let traceable = function
+  | TacThen _ | TacThens _ -> true
+  | _ -> false;;
+
+let rec collect_status = function
+    Report_node(true,_,_)::tl -> collect_status tl
+  | [] -> true
+  | _ -> false;;
+
+(* This tactical receives a tactic and executes it, reporting information
+   about success in the report holder and a boolean reference. *)
+
+let count_subgoals : card_holder -> bool ref -> tactic -> tactic =
+  fun card_holder flag t g ->
+    try
+      let (gls, _) as result = t g in
+      card_holder := (Ngoals(List.length (sig_it gls)));
+      flag := true;
+      result
+    with
+      e -> card_holder := Fail;
+           flag := false;
+           tclIDTAC g;;
+   
+let count_subgoals2
+    : card_holder -> bool ref -> (report_holder -> tactic) -> tactic =
+  fun card_holder flag t g ->
+    let new_report_holder = ref([] : report_tree list) in
+    let (gls, v) as result = t new_report_holder g in
+    let succeeded = no_failure !new_report_holder in
+    if succeeded then
+      (flag := true;
+       card_holder := Ngoals (List.length (sig_it gls)))
+    else
+      (flag := false;
+       card_holder := Recursive_fail(List.hd !new_report_holder));
+    result;;
+
+let rec local_interp : glob_tactic_expr -> report_holder -> tactic = function
+    TacThens (a,l) ->
+      (fun report_holder -> checked_thens report_holder a l)
+  | TacThen (a,[||],b,[||]) ->
+      (fun report_holder -> checked_then report_holder a b)
+  | t ->
+      (fun report_holder g ->
+	try
+	  let (gls, _) as result = Tacinterp.eval_tactic t 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))
+
+
+(* This tactical receives a tactic and a list of tactics as argument.
+   It applies the first tactic and then maps the list of tactics to
+   various produced sub-goals.  This tactic will never fail, but reports
+   are added in the report_holder in the following way:
+   - In case of partial success, a new report_tree is added to the report_holder
+   - In case of failure of the first tactic, with no more indications
+     then Failed 0 is added to the report_holder,
+   - In case of partial failure of the first tactic then (Failed n) is added to
+     the report holder.
+   - In case of success of the first tactic, but count mismatch, then
+     Mismatch n is added to the report holder. *)
+
+and checked_thens: report_holder -> glob_tactic_expr -> glob_tactic_expr list -> tactic = 
+  (fun report_holder t1 l g ->
+    let flag = ref true in
+    let traceable_t1 = traceable t1 in
+    let card_holder = ref Fail in
+    let new_holder = ref ([]:report_tree list) in
+    let tac_t1 = 
+      if traceable_t1 then
+	(check_subgoals_count2 card_holder (List.length l)
+           flag (local_interp t1))
+      else
+	(check_subgoals_count card_holder (List.length l)
+           flag (Tacinterp.eval_tactic t1)) in
+    let (gls, _) as result = 
+      tclTHEN_i tac_t1
+	(fun i ->
+	  if !flag then
+	    (fun g -> 
+              let tac_i = (List.nth l i) in
+	      if traceable tac_i then
+                 local_interp tac_i new_holder g
+              else
+		 try
+		   let (gls,_) as result = Tacinterp.eval_tactic tac_i g in
+		   let len = List.length (sig_it gls) in
+				   new_holder :=
+		     (Report_node(true, len, []))::!new_holder;
+		   result
+		 with
+			       e -> (new_holder := (Failed 1)::!new_holder;
+			 tclIDTAC g))
+	  else
+	    tclIDTAC) g in
+      let new_goal_list = sig_it gls in
+      (if !flag then
+	report_holder := 
+	  (Report_node(collect_status !new_holder,
+		    (List.length new_goal_list),
+		    List.rev !new_holder))::!report_holder
+      else
+	report_holder :=
+	  (match !card_holder with
+	    Goals_mismatch(n) -> Mismatch(n, List.length l)
+	  | Recursive_fail tr -> Tree_fail tr
+	  | Fail -> Failed 1
+	  | _ -> errorlabstrm "check_thens"
+                  (str "this case should not happen in check_thens"))::
+	  !report_holder);
+      result)
+
+(* This tactical receives two tactics as argument, it executes the
+   first tactic and applies the second one to all the produced goals,
+   reporting information about the success of all tactics in the report
+   holder. It never fails. *)
+
+and checked_then: report_holder -> glob_tactic_expr -> glob_tactic_expr -> tactic =
+  (fun report_holder t1 t2 g ->
+    let flag = ref true in
+    let card_holder = ref Fail in
+    let tac_t1 =
+      if traceable t1 then
+	(count_subgoals2 card_holder flag (local_interp t1))
+      else
+	(count_subgoals card_holder flag (Tacinterp.eval_tactic t1)) in
+    let new_tree_holder = ref ([] : report_tree list) in
+    let (gls, _) as result =
+      tclTHEN tac_t1
+	(fun (g:goal sigma) -> 
+	  if !flag then
+	    if traceable t2 then
+	      local_interp t2 new_tree_holder g
+	    else
+	      try
+		let (gls, _) as result = Tacinterp.eval_tactic t2 g in
+	      	new_tree_holder :=
+		  (Report_node(true, List.length (sig_it gls),[]))::
+		  !new_tree_holder;
+		result
+	      with
+		e ->
+		  (new_tree_holder := ((Failed 1)::!new_tree_holder);
+		   tclIDTAC g)
+	  else
+	    tclIDTAC g) g in
+    (if !flag then
+      report_holder :=
+	(Report_node(collect_status !new_tree_holder,
+		     List.length (sig_it gls),
+		     List.rev !new_tree_holder))::!report_holder
+    else
+      report_holder :=
+	(match !card_holder with
+	  Recursive_fail tr -> Tree_fail tr
+	| Fail -> Failed 1
+	| _ -> error "this case should not happen in check_then")::!report_holder);
+    result);;
+
+(* This tactic applies the given tactic only to those subgoals designated
+   by the list of integers given as extra arguments.
+ *)
+
+let rawwit_main_tactic = Pcoq.rawwit_tactic Pcoq.tactic_main_level
+let globwit_main_tactic = Pcoq.globwit_tactic Pcoq.tactic_main_level
+let wit_main_tactic = Pcoq.wit_tactic Pcoq.tactic_main_level
+
+
+let on_then = function [t1;t2;l] ->
+  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 ->
+      if List.mem (i + 1) l then
+      	(Tacinterp.eval_tactic t2)
+      else
+	tclIDTAC)
+  | _ -> anomaly "bad arguments for on_then";;
+
+let mkOnThen t1 t2 selected_indices =
+  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 -> n::select_success (n+1) tl
+  | _::tl -> select_success (n+1) tl;;
+
+let rec reconstruct_success_tac (tac:glob_tactic_expr) =
+  match tac with
+    TacThens (a,l) ->
+      (function 
+	  Report_node(true, n, l) -> tac
+      	| Report_node(false, n, rl) ->
+	    TacThens (a,List.map2 reconstruct_success_tac l rl)
+      	| Failed n -> TacId []
+      	| Tree_fail r -> reconstruct_success_tac a r
+      	| Mismatch (n,p) -> a)
+  | TacThen (a,[||],b,[||]) ->
+      (function
+	  Report_node(true, n, l) -> tac
+	| Report_node(false, n, rl) ->
+	    let selected_indices = select_success 1 rl in
+	    TacAtom (dummy_loc,TacExtend (dummy_loc,"OnThen",
+	      [in_gen globwit_main_tactic a;
+	       in_gen globwit_main_tactic b;
+	       in_gen (wit_list0 globwit_int) selected_indices]))
+	| 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 []
+	| _ ->
+	    errorlabstrm
+	      "this error case should not happen on an unknown tactic"
+              (str "error in reconstruction with " ++ fnl () ++
+	       (pr_glob_tactic tac)));;
+	  
+
+let rec path_to_first_error = function
+| Report_node(true, _, l) ->
+  let rec find_first_error n = function
+  | (Report_node(true, _, _))::tl -> find_first_error (n + 1) tl
+  | it::tl -> n, it
+  | [] -> error "no error detected" in
+  let p, t = find_first_error 1 l in
+    p::(path_to_first_error t)
+| _ -> [];;
+
+let debug_tac = function
+    [(Tacexp ast)] ->
+      (fun g -> 
+      	let report = ref ([] : report_tree list) in
+      	let result = local_interp ast report g in
+      	let clean_ast = (* expand_tactic *) ast in
+      	let report_tree =
+          try List.hd !report with
+	    Failure "hd" -> (msgnl (str "report is empty"); Failed 1) in
+      	let success_tac = 
+	  reconstruct_success_tac clean_ast report_tree in
+        let compact_success_tac = (* flatten_then *) success_tac in
+      	msgnl (fnl () ++
+	       str "=========    Successful tactic    =============" ++
+               fnl () ++
+	       pr_glob_tactic compact_success_tac ++ fnl () ++
+	       str "========= End of successful tactic ============");
+      	result)
+  | _ -> error "wrong arguments for debug_tac";;
+
+(* TODO ... used ?
+add_tactic "DebugTac" debug_tac;;
+*)
+
+Tacinterp.add_tactic "OnThen" on_then;;
+
+let rec clean_path tac l = 
+  match tac, l with
+  | TacThen (a,[||],b,[||]), fst::tl ->
+      fst::(clean_path (if fst = 1 then a else b) tl)
+  | TacThens (a,l), 1::tl ->
+      1::(clean_path a tl)
+  | TacThens (a,tacs), 2::fst::tl ->
+      2::fst::(clean_path (List.nth tacs (fst - 1)) tl)
+  | _, [] -> []
+  | _, _ -> failwith "this case should not happen in clean_path";;
+
+let rec report_error
+    : glob_tactic_expr -> goal sigma option ref -> glob_tactic_expr ref -> int list ref -> 
+      int list -> tactic =
+  fun tac the_goal the_ast returned_path path -> 
+    match tac with
+      TacThens (a,l) ->
+      let the_card_holder = ref Fail in
+      let the_flag = ref false in
+      let the_exn = ref (Failure "") in
+      tclTHENS
+	(fun g ->
+	  let result =
+	    check_subgoals_count 
+	      the_card_holder
+	      (List.length l) 
+	      the_flag
+	      (fun g2 -> 
+		try 
+		  (report_error a the_goal the_ast returned_path (1::path) g2)
+	  	with
+		  e -> (the_exn := e; raise e))
+	      g in
+	  if !the_flag then
+	    result
+	  else
+	    (match !the_card_holder with
+			Fail -> 
+			  the_ast := TacThens (!the_ast, l);
+			  raise !the_exn
+	    | Goals_mismatch p -> 
+		the_ast := tac;
+		returned_path := path;
+		error ("Wrong number of tactics: expected " ^
+		       (string_of_int (List.length l)) ^ " received " ^
+		       (string_of_int p))
+	    | _ -> error "this should not happen"))
+        (let rec fold_num n = function
+	    [] -> []
+	  | t::tl -> (report_error t the_goal the_ast returned_path (n::2::path))::
+	      (fold_num (n + 1) tl) in
+	fold_num 1 l)
+    | TacThen (a,[||],b,[||]) ->
+	let the_count = ref 1 in
+	tclTHEN
+	  (fun g ->
+	    try
+	      report_error a the_goal the_ast returned_path (1::path) g
+	    with
+	      e ->
+		(the_ast := TacThen (!the_ast,[||], b,[||]);
+		 raise e))
+	  (fun g ->
+	    try
+	      let result = 
+		report_error b the_goal the_ast returned_path (2::path) g in
+	      the_count := !the_count + 1;
+	      result
+	    with
+	      e ->
+		if !the_count > 1 then
+		  msgnl
+		    (str "in branch no " ++ int !the_count ++
+		     str " after tactic " ++ pr_glob_tactic a);
+		raise e)
+    | tac ->
+	(fun g ->
+	  try
+	   Tacinterp.eval_tactic tac g
+	  with
+	    e ->
+	      (the_ast := tac;
+	       the_goal := Some g;
+	       returned_path := path;
+	       raise e));;
+
+let strip_some = function
+    Some n -> n
+  | None -> failwith "No optional value";;
+
+let descr_first_error tac =
+      (fun g ->
+	let the_goal = ref (None : goal sigma option) in
+	let the_ast = ref tac in
+	let the_path = ref ([] : int list) in
+	try
+	  let result = report_error tac the_goal the_ast the_path [] g in
+	  msgnl (str "no Error here");
+	  result
+	with
+	  e ->
+	    (msgnl (str "Execution of this tactic raised message " ++ fnl () ++
+		    fnl () ++ Cerrors.explain_exn e ++ fnl () ++
+		    fnl () ++ str "on goal"  ++ 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))
+
+(* TODO ... used ??
+add_tactic "DebugTac2" descr_first_error;;
+*)
+
+(*
+TACTIC EXTEND DebugTac2
+  [ ??? ] -> [ descr_first_error tac ]
+END
+*)