(*  Title:      ~~/test/../Testcode/test-code.sml

    Author:     Walther Neuper 200222

Code used ONLY for ~~/test/*

*)

signature TEST_CODE =

sig

  type NEW (* TODO: refactor "fun me" with calcstate and remove *)

  val f2str : Test_Out.mout -> TermC.as_string

  val TESTg_form : Calc.T -> Test_Out.mout

  val CalcTreeTEST : Formalise.T list -> Pos.pos' * NEW * Test_Out.mout * Tactic.input * Celem.safe * Ctree.ctree

  val me : Tactic.input -> Pos.pos' -> NEW -> Ctree.ctree ->

    Pos.pos' * NEW * Test_Out.mout * Tactic.input * Celem.safe * Ctree.ctree

  val trace_ist_ctxt: Calc.T -> Tactic.input -> unit

  val me_trace: Calc.T -> Tactic.input -> (Calc.T -> Tactic.input -> unit) ->

    Calc.T * Tactic.input * Test_Out.mout

  val tac2tac_ : Ctree.ctree -> Pos.pos' -> Tactic.input -> Tactic.T

end

(**)

structure Test_Code(**): TEST_CODE(**) =

struct

(**)

open Tactic

open Ctree

(** test Step.by_tactic + Step.do_next **)

type NEW = int list; (*TODO remove*)

(* 15.8.03 for me with loc_specify/solve, nxt_specify/solve

   delete as soon as TESTg_form -> _mout_ dropped           *)

fun TESTg_form ptp =

  let

    val (form, _, _) = Chead.pt_extract ptp

  in

    case form of

      Ctree.Form t => Test_Out.FormKF (UnparseC.term t)

    | Ctree.ModSpec (_, p_, _, gfr, pre, _) =>

      Test_Out.PpcKF (

        (case p_ of Pos.Pbl => Test_Out.Problem []

          | Pos.Met => Test_Out.Method []

          | _ => raise ERROR "TESTg_form: uncovered case",

 			P_Model.itms2itemppc (ThyC.get_theory"Isac_Knowledge") gfr pre))

   end

(* for quick test-print-out, until 'type inout' is removed *)

fun f2str (Test_Out.FormKF cterm') = cterm'

  | f2str _ = raise ERROR "f2str: uncovered case in fun.def.";                           

(* create a calc-tree; for use within sml: thus "^^^" NOT decoded to "^" etc;

   compare "fun CalcTree" which DOES decode                        *)

fun CalcTreeTEST [(fmz, sp)] = 

  let

    val ((pt, p), tacis) = Step_Specify.nxt_specify_init_calc (fmz, sp)

	  val tac = case tacis of [] => Tactic.Empty_Tac | _ => (#1 o hd) tacis

	  val f = TESTg_form (pt,p)

  in (p, []:NEW, f, tac, Celem.Sundef, pt) end

| CalcTreeTEST _ = raise ERROR "CalcTreeTEST: uncovered case"

fun me (*(Empty_Tac) p _ _ = raise ERROR ("me:  Empty_Tac at " ^ pos'2str p)

  | me*) tac p _(*NEW remove*) pt =

    let 

      val (pt, p) = 

  	    (*Step.by_tactic is here for testing by me; do_next would suffice in me*)

  	    case Step.by_tactic tac (pt, p) of

  		    ("ok", (_, _, ptp)) => ptp

  	    | ("unsafe-ok", (_, _, ptp)) => ptp

  	    | ("not-applicable",_) => (pt, p)

  	    | ("end-of-calculation", (_, _, ptp)) => ptp

  	    | ("failure", _) => raise ERROR "sys-raise ERROR"

  	    | _ => raise ERROR "me: uncovered case Step.by_tactic"

  	  val (_, ts) =

        (*step's correct ctree is not tested in me, but in autocalc or Step.by_term*)

  	    (case Step.do_next p ((pt, Pos.e_pos'), []) of

  		    ("ok", (ts as (_, _, _) :: _, _, _)) => ("", ts)

  	    | ("helpless", _) => ("helpless: cannot propose tac", [])

  	    | ("dummy", (ts as (_, _, _) :: _, _, _)) => ("", ts) (*intermed.from specify*)

  	    | ("end-of-calculation", (ts, _, _)) => ("", ts)

  	    | _ => raise ERROR  "me: uncovered case do_next")

  	  val tac = 

        case ts of 

          tacis as (_::_) => let val (tac, _, _) = last_elem tacis in tac end 

  		  | _ => if p = ([], Pos.Res) then Tactic.End_Proof' else Tactic.Empty_Tac;

    in

      (p, [] : NEW, TESTg_form (pt, p) (* form output comes from Step.by_tactic *), 

  	    tac, Celem.Sundef, pt)

    end

(** traces for me_trace **)

fun (*quiet (Model_Problem) = true

  |*) quiet (Add_Given _) = true

  | quiet (Add_Find _) = true

  | quiet (Add_Relation _) = true

  | quiet (Specify_Method _) = true

  | quiet (Specify_Problem _) = true

  | quiet (Specify_Theory _) = true

  | quiet _ = false

fun mk_string (ist, ctxt) =

  ("(" ^ Istate.string_of' ist ^ ",\n" 

  ^ "... ctxt:    " ^ (ctxt |> ContextC.get_assumptions |> UnparseC.terms) ^ ")")

fun trace_ist_ctxt (EmptyPtree , ([], Pos.Und)) _ = ()

  | trace_ist_ctxt (pt, (p, _)) tac =

  if quiet tac

  then ()

  else

    case get_obj g_loc pt p of

      (NONE, NONE) =>

        writeln   "Frm, Res: (NONE, NONE)"

    | (SOME ist_ctxt, NONE) =>

        (writeln ("Frm ..... (SOME " ^ mk_string ist_ctxt ^ " ,");

         writeln ("Res .....  NONE)"))

    | (NONE, SOME ist_ctxt) =>

        (writeln ("Frm .....  (NONE,");

         writeln ("Res .....  SOME " ^ mk_string ist_ctxt ^ " )"))

    | (SOME ic_frm, SOME ic_res) =>

        (writeln ("Frm ..... (SOME " ^ mk_string ic_frm ^ " ,");

         writeln ("Res .....  SOME " ^ mk_string ic_res ^ " )"))

(** test Step.by_tactic + Step.do_next with tracing **)

fun me_trace (*(Empty_Tac) p _ _ = raise ERROR ("me:  Empty_Tac at " ^ pos'2str p)

  | me*) (pt, p) tac trace =

    let

      val _ = if quiet tac then () else

        writeln ("========= " ^ Pos.pos'2str p ^ "========= Step.by_tactic: " ^ Tactic.input_to_string tac ^ " ==================================");

      val (pt', p') = 

  	    (*Step.by_tactic is here for testing by me; do_next would suffice for doing steps*)

  	    case Step.by_tactic tac (pt, p) of

  		    ("ok", (_, _, ptp)) => ptp

  	    | ("unsafe-ok", (_, _, ptp)) => ptp

  	    | ("not-applicable",_) => (pt, p)

  	    | ("end-of-calculation", (_, _, ptp)) => ptp

  	    | ("failure", _) => raise ERROR "sys-raise ERROR"

  	    | _ => raise ERROR "me: uncovered case Step.by_tactic"

      val _ = trace (pt', p') tac

  	  val (_, ts, (pt'', p'')) =

        (*step's correct ctree is not tested in me, but in autocalc or Step.by_term*)

  	    (case Step.do_next p' ((pt', Pos.e_pos'), []) of

  		    ("ok", (ts as [(_, _, _)(*, _, _, ...*)], _, (pt'', p''))) => ("", ts, (pt'', p''))

  	    | ("helpless", _) => ("helpless: cannot propose tac", [], Ctree.e_state)

  	    | ("dummy", (ts as (_, _, _) :: _, _, _)) => ("", ts, Ctree.e_state) (*intermed.from specify*)

  	    | ("end-of-calculation", (ts, _, _)) => ("", ts, Ctree.e_state)

  	    | _ => raise ERROR  "me: uncovered case do_next")

  	  val tac'' = 

        case ts of 

          tacis as (_::_) => let val (tac, _, _) = last_elem tacis in tac end 

  		  | _ => if p' = ([], Pos.Res) then Tactic.End_Proof' else Tactic.Empty_Tac;

      val _ = if quiet tac then () else

        writeln ("--------- " ^ Pos.pos'2str p' ^ "--------- Step.do_next \<rightarrow> " ^ Tactic.input_to_string tac'' ^ "----------------------------------");

      val _ = trace (pt'', p'') tac

    in

      ((pt', p'), tac'', TESTg_form (pt', p') (* form output comes from Step.by_tactic *))

    end

fun tac2tac_ pt p m = 

  case Step.check m (pt, p) of

	  Applicable.Yes m' => m' 

  | Applicable.No _ => raise ERROR ("tac2mstp': fails with" ^ Tactic.input_to_string m);

(**)end(**)