(* Title:  Test_Code/test-tool.sml

   Author: Walther Neuper 110226

   (c) due to copyright terms

*)

signature TEST_TOOL =

sig

  val show_ptyps : unit -> unit

  val show_mets : unit -> unit

  val show_pblguhs : unit -> unit

  val sort_pblguhs : unit -> unit

  val show_metguhs : unit -> unit

  val sort_metguhs : unit -> unit

  val show_pt : Ctree.ctree -> unit

  val show_pt_tac : Ctree.ctree -> unit

  val write_rules: Proof.context -> int -> Rule.rule list -> unit

\<^isac_test>\<open>

  val posterms2str: Proof.context -> (Pos.pos' * term * 'a) list -> string

  val postermtacs2str: Proof.context -> (Pos.pos' * term * Tactic.input option) list -> string

\<close>

end

(**)

structure Test_Tool(**) : TEST_TOOL(**) =

struct

(**)

fun format_pblID strl = enclose " [" "]" (commas_quote strl);

fun format_pblIDl strll = enclose "[\n" "\n]\n" (space_implode ",\n" (map format_pblID strll));

fun show_ptyps () = (writeln o format_pblIDl o (Store.scan [])) (get_pbls ()); (* for tests *)

fun show_mets () = (writeln o format_pblIDl o (Store.scan [])) (get_pbls ()); (* for tests *)

fun show_pblguhs () =

  (tracing o strs2str o (map linefeed))

    (Check_Unique.collect (#guh : Probl_Def.T -> Check_Unique.id) (get_pbls ()))

fun sort_pblguhs () =

  (tracing o strs2str o (map linefeed))

    (((sort string_ord) o (Check_Unique.collect (#guh : Probl_Def.T -> Check_Unique.id)))

      (get_pbls ()))

fun show_metguhs () =

  (tracing o strs2str o (map linefeed))

    (Check_Unique.collect (#guh : Meth_Def.T -> Check_Unique.id) (get_mets ()))

fun sort_metguhs () =

  (tracing o strs2str o (map linefeed))

    (((sort string_ord) o (Check_Unique.collect (#guh : Meth_Def.T -> Check_Unique.id)))

      (get_mets ()))

(** show a whole Calc.T **)

fun posterm2str ctxt (pos, t, _) = "(" ^ Pos.pos'2str pos ^ ", " ^ UnparseC.term_in_ctxt ctxt t ^ ")"

fun posterms2str ctxt pfs = (strs2str' o (map (curry op ^ "\n")) o (map (posterm2str ctxt))) pfs

fun postermtac2str ctxt (pos, t, SOME tac) =

      Pos.pos'2str pos ^ ", " ^ UnparseC.term_in_ctxt ctxt t ^ "\n" ^

        indent 10 ^ Tactic.input_to_string ctxt tac

  | postermtac2str ctxt (pos, t, NONE) =

      Pos.pos'2str pos ^ ", " ^ UnparseC.term_in_ctxt ctxt t

fun postermtacs2str ctxt pfts =

  (strs2str' o (map (curry op ^ "\n")) o (map (postermtac2str ctxt))) pfts

(* WN050225 shows a WRONG last step, if pt is incomplete *)

fun show_pt pt =

  let 

    val ctxt = Ctree.get_ctxt pt ([], Pos.Pbl) (*for coarse approximation*)

  in

    tracing (posterms2str ctxt (ME_Misc.get_interval ctxt ([], Pos.Frm) ([], Pos.Res) 99999 pt))

  end

fun show_pt_tac pt =

  let 

    val ctxt = Ctree.get_ctxt pt ([], Pos.Pbl) (*for coarse approximation*)

  in

    tracing (postermtacs2str ctxt (ME_Misc.get_interval ctxt ([], Pos.Frm) ([], Pos.Res) 99999 pt))

  end

(** for finding a culprit in a (usually lengthy) list of Rule.T **)

fun write_rules _ _ [] = writeln ""

  | write_rules ctxt i (r :: rs) =

    let val _ = 

      case r of

        Rule.Thm (thmid, thm) =>

          writeln (string_of_int i ^ " Thm (" ^ thmid ^ ", " ^ ThmC.string_of_thm ctxt thm ^ ")")

      | Rule.Eval (op_, _) =>

          writeln (string_of_int i ^ " Eval (" ^ op_ ^ ", _)")

      | Rule.Cal1 (op_, _) => 

          writeln (string_of_int i ^ " Cal1 (" ^ op_ ^ ", _)")

      | Rule.Rls_ rls => 

          writeln (string_of_int i ^ " Rls_ {id = " ^ (Rule_Set.rep rls |> #id) ^ ", ...}")

    in

      write_rules ctxt (i + 1) rs

    end

(**)end(*sruct*)