theory Subgoal
imports Term_pat
begin

section {* Monad for goal and subgoal manipulation, useful for debugging tactics  *}

subsection {* Implementation *}

ML {*
  fun goalM raw_goal = m0M' (fn ((i, _), ctxt) =>
  let
     val thy = Proof_Context.theory_of ctxt
     val goal = raw_goal |> cterm_of thy |> Goal.init
     (* val ctxt' = Variable.auto_fixes raw_goal ctxt *)
     val ctxt' = ctxt
  in (s2M ctxt' |-- (s1M (i, goal)) |-- returnM goal) end)

local
  fun pr_goal ctxt goal = Goal_Display.pretty_goals ctxt goal |> 
                           Pretty.markup_chunks Markup.state |> Pretty.writeln
in
  fun tacM tac = m1M' (fn (i, goal) => m2M (fn ctxt =>
        let 
            val goal' = (Seq.hd (tac ctxt goal)) 
            val _ = pr_goal ctxt goal'
        in
            s1M (i, goal') |-- returnM goal'
        end))
end

  fun focusM i = pushM |-- (liftM (m0M (fn ((_, goal), ctxt) => 
                     let val (focus as {context = ctxt', ...}, goal') = Subgoal.focus ctxt i goal
                     in 
                        setM ((i, goal'), ctxt') |-- returnM focus
                     end)))

  fun end_focusM x = (     popM 
                      :|-- (fn ((i, goal'), _) => topM (fn ((old_i, goal), ctxt) =>
                           let val ({context = ctxt', params, asms, ...}, _) = 
                                               Subgoal.focus ctxt i goal
                               val new_goal = Seq.lifts (Subgoal.retrofit ctxt' ctxt params asms i) 
                                                      (Seq.single goal') goal |> Seq.hd
                               in s1M (old_i, new_goal) |-- returnM new_goal end  ))) x
*}

subsection {* Examples *}

lemma init: "A \<Longrightarrow> A"
  by simp

ML {*
  val r as (result, _)= [((0, @{thm "init"}), @{context})] |> 
          @{fterm "(A \<and> B \<Longrightarrow> A)"} 
          :|-- goalM 
           |-- focusM 1 
          :|--(fn {prems, ...} => let
                       val conj = hd prems
                       val r = rtac (conj RS @{thm HOL.conjunct1}) 1
                   in tacM (K r) end )
           |-- end_focusM >> Drule.export_without_context |> normVal
*}


ML {*
  val r = [((0, @{thm "init"}), @{context})] |> 
          @{fterm "(A \<and> B \<Longrightarrow> A)"} 
          :|-- goalM 
          |-- tacM (fn ctxt => Subgoal.FOCUS (fn {prems, ...} => let
                                  val conj = hd prems
                                  val r = rtac (conj RS @{thm HOL.conjunct1}) 1
                                in r end ) ctxt 1) >> Drule.export_without_context
          |> normVal
*}

end