1 (* Title: MathEngine/detail-step.sml
2 Author: Walther Neuper 2020
3 (c) due to copyright terms
5 Within one step go into detailed steps on request by the user
8 signature DETAIL_STEP =
10 val go : Ctree.ctree -> Pos.pos' -> string * Ctree.ctree * Pos.pos'
11 val detailrls : Ctree.ctree -> Pos.pos' -> string * Ctree.ctree * Pos.pos'
15 structure Detail_Step(**): DETAIL_STEP(**) =
21 (* aux.fun for detailrls with Rrls, reverse rewriting *)
22 fun rul_terms_2nds _ nds _ [] = nds
23 | rul_terms_2nds thy nds t ((rule, res as (t', _)) :: rts) =
24 (append_atomic [] (NONE(*guessed*), (Istate.empty, ContextC.empty)) t (Tactic.rule2tac thy [] rule) res Complete EmptyPtree) ::
25 (rul_terms_2nds thy nds t' rts);
27 (* detail steps done internally by Rewrite_Set* into Ctree
28 by use of a program *)
29 fun detailrls pt (pos as (p, _)) =
31 val t = get_obj g_form pt p
32 val tac = get_obj g_tac pt p
33 val ctxt = get_ctxt pt pos
34 val rls = tac |> Tactic.rls_of |> get_rls ctxt
37 Rule_Set.Rrls {scr = Rule.Rfuns {init_state, ...}, ...} =>
39 val (_, _, _, rul_terms) = init_state t
40 val newnds = rul_terms_2nds ctxt [] t rul_terms
41 val pt''' = ins_chn newnds pt p
42 in ("detailrls", pt''', (p @ [length newnds], Res)) end
45 val is = Istate.init_detail tac t
46 val tac_ = Tactic.Apply_Method' (MethodC.id_empty(*WN0402: see generate1 !?!*), SOME t, is, ctxt)
47 val pos' = ((lev_on o lev_dn) p, Frm)
48 val (_, _, _, pt') = Step.add tac_ (is, ctxt) (pt, pos') (* implicit Take *)
49 val (_,_, (pt'', _)) = Solve.complete_solve Solve.CompleteSubpbl [] (pt', pos')
50 val newnds = children (get_nd pt'' p)
51 val pt''' = ins_chn newnds pt p (*complete_solve cuts branches after*)
52 in ("detailrls", pt''', (p @ [length newnds], Res)) end
55 fun go pt (pos as (p, _)) =
57 val nd = Ctree.get_nd pt p
58 val cn = Ctree.children nd
62 if (Tactic.is_rewset o (Ctree.get_obj Ctree.g_tac nd)) [(*root of nd*)]
64 else ("no-Rewrite_Set...", Ctree.EmptyPtree, Pos.e_pos')
65 else ("donesteps", pt, (p @ [length (Ctree.children (Ctree.get_nd pt p))], Pos.Res))