(* Title:  MathEngine/detail-step.sml

   Author: Walther Neuper 2020

   (c) due to copyright terms

Within one step go into detailed steps on request by the user

*)

signature DETAIL_STEP =

sig

  val go : Ctree.ctree -> Pos.pos' -> string * Ctree.ctree * Pos.pos'

  val detailrls : Ctree.ctree -> Pos.pos' -> string * Ctree.ctree * Pos.pos'

end

(**)

structure Detail_Step(**): DETAIL_STEP(**) =

struct

(**)

open Ctree;

open Pos

(* aux.fun for detailrls with Rrls, reverse rewriting *)

fun rul_terms_2nds _ nds _ [] = nds

  | rul_terms_2nds thy nds t ((rule, res as (t', _)) :: rts) =

    (append_atomic [] (NONE(*guessed*), (Istate.empty, ContextC.empty)) t (Tactic.rule2tac thy [] rule) res Complete EmptyPtree) ::

      (rul_terms_2nds thy nds t' rts);

(* detail steps done internally by Rewrite_Set* into Ctree 

  by use of a program *)

fun detailrls pt (pos as (p, _)) = 

  let

    val t = get_obj g_form pt p

	  val tac = get_obj g_tac pt p

	  val rls = (assoc_rls o Tactic.rls_of) tac

    val ctxt = get_ctxt pt pos

  in

    case rls of

	    Rule_Set.Rrls {scr = Rule.Rfuns {init_state, ...}, ...} => 

	    let

        val (_, _, _, rul_terms) = init_state t

	      val newnds = rul_terms_2nds (Proof_Context.theory_of ctxt) [] t rul_terms

	      val pt''' = ins_chn newnds pt p 

	    in ("detailrls", pt''', (p @ [length newnds], Res)) end

	  | _ =>

	    let

        val is = Istate.init_detail tac t

	      val tac_ = Tactic.Apply_Method' (Method.id_empty(*WN0402: see generate1 !?!*), SOME t, is, ctxt)

	      val pos' = ((lev_on o lev_dn) p, Frm)

	      val (_, _, _, pt') = Step.add tac_ (is, ctxt) (pt, pos') (* implicit Take *)

	      val (_,_, (pt'', _)) = Solve.complete_solve Solve.CompleteSubpbl [] (pt', pos')

	      val newnds = children (get_nd pt'' p)

	      val pt''' = ins_chn newnds pt p (*complete_solve cuts branches after*)

	    in ("detailrls", pt''', (p @ [length newnds], Res)) end

  end;

fun go pt (pos as (p, _)) = 

  let 

    val nd = Ctree.get_nd pt p

    val cn = Ctree.children nd

  in 

    if null cn 

    then

      if (Tactic.is_rewset o (Ctree.get_obj Ctree.g_tac nd)) [(*root of nd*)]

      then detailrls pt pos

      else ("no-Rewrite_Set...", Ctree.EmptyPtree, Pos.e_pos')

    else ("donesteps", pt, (p @ [length (Ctree.children (Ctree.get_nd pt p))], Pos.Res)) 

  end;

end