(*  Title:      Tools/isac/Testcode/test-code.sml

    Author:     Walther Neuper 200222

Code used ONLY for $ISABELLE_ISAC_TEST/Tools/isac/*

*)

signature TEST_CODE =

sig

  type NEW (* TODO: refactor "fun me" with Calc.state_pre and remove *)

  val f2str : Test_Out.mout -> TermC.as_string

  val TESTg_form : Proof.context -> Calc.T -> Test_Out.mout

  val init_calc : Proof.context -> 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 init_calc': Proof.context -> Formalise.T list -> Tactic.input * Calc.T

  val me': Tactic.input * Calc.T -> Tactic.input * Calc.T

  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 ctxt ptp =

  let

    val (form, _, _) = ME_Misc.pt_extract ctxt ptp

  in

    case form of

      Ctree.Form t => Test_Out.FormKF (UnparseC.term_in_ctxt ctxt t)

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

      Test_Out.PpcKF (

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

          | Pos.Met => Test_Out.MethodC []

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

 			P_Model.from (Proof_Context.theory_of ctxt) gfr where_))

   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 *)

fun init_calc ctxt [(model, refs as (thy_id, _, _))] =

  let

(*old* )val ctxt = thy_id |> ThyC.get_theory_PIDE ctxt |> Proof_Context.init_global

( *new*)val thy = thy_id |> ThyC.get_theory_PIDE ctxt  (*^^^^^^^^^^^^^^^^^^^^^^^^^ misleading*)

    val ((pt, p), tacis) = Step_Specify.nxt_specify_init_calc_PIDE thy (model, refs)

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

	  val f = TESTg_form ctxt (pt,p)

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

| init_calc _ _ = raise ERROR "Tess_Code.init_calc: uncovered case"

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

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

    let

      val ctxt = Ctree.get_ctxt pt p

      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 by Step.by_tactic"

  	    | _ => 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)

  	    | ("failure", _) => raise ERROR "sys-raise ERROR by Step.do_next"

  	    | _ => raise ERROR  "me: uncovered case Step.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 ctxt (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 ctxt = Ctree.get_ctxt pt p

      val _ = if quiet tac then () else

        writeln ("========= " ^ Pos.pos'2str p ^ "========= Step.by_tactic: " ^

          Tactic.input_to_string ctxt tac ^ " ==================================");

      val (pt', p') = 

  	    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 by Step.by_tactic"

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

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

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

  	    (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)

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

  	    | ("failure", _) => raise ERROR "sys-raise ERROR by Step.do_next"

  	    | _ => raise ERROR  "me: uncovered case Step.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 ctxt tac'' ^ "----------------------------------");

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

    in

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

    end

fun tac2tac_ pt p m = 

  let

    val ctxt = Ctree.get_ctxt pt p

  in

    case Step.check m (pt, p) of

  	  Applicable.Yes m' => m' 

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

  end;

(** me' for |> **)

fun init_calc' ctxt [(model, refs as (thy_id, _, _))] =

  let

    val ctxt = thy_id |> ThyC.get_theory_PIDE ctxt |> Proof_Context.init_global

    val ((pt, p), _) = Step_Specify.nxt_specify_init_calc ctxt (model, refs)

  in

    (Tactic.Model_Problem, (pt, p))                       (* thus <Output> shows Tactic on top *)

  end

| init_calc' _ _ = raise ERROR "Test_Code.init_calc' @{context}: uncovered case"

fun me' (tac, (pt, p)) =                                  (* thus <Output> shows Tactic on top *)

  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 by Step.by_tactic"

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

    val tac' =

      (*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", ((tac', _, _) :: _, _, _)) => tac'

      | ("helpless", _) => Tactic.Empty_Tac

      | ("dummy", ((tac', _, _) :: _, _, _)) => tac'

      | ("end-of-calculation", _) => Tactic.End_Proof'

      | ("failure", _) => raise ERROR "sys-raise ERROR by Step.do_next"

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

  in 

    (tac', (pt', p'))                                     (* thus <Output> shows Tactic on top *)

  (* ^^^^----- is the next step after "(pt', p')", but we prefer ----------------^^^^^^^^^^^^^ *)

  end

(**)end(**)