(* 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 = Generate.init_istate 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