theory MLs
imports Pure
keywords "ML_psf" :: prf_script and
         "ML_goal" :: thy_goal
begin

section {* ML for proof state transformation *}

ML {*
  structure ML_psf = Proof_Data (
    type T = Proof.state -> Proof.state
    fun init _ = undefined
  )
*}


ML {*
 fun ml_psf (txt, pos) state =   
        (((Proof.context_of state) |>
         Context.proof_map (ML_Context.expression Position.none 
                 "val psf : Proof.state -> Proof.state"
                  "Context.map_proof (ML_psf.put psf)"  (ML_Lex.read pos txt)) |>
         ML_psf.get) state):Proof.state
*}

ML {*
val _ =
  Outer_Syntax.command @{command_spec "ML_psf"} "ML state transfer function"
    (Parse.ML_source >> (Toplevel.print oo (Toplevel.proof o ml_psf)))
*}

section {* ML for global goal establishment *}

ML {*
  structure ML_goal = Proof_Data (
    type T = local_theory -> Proof.state
    fun init _ = undefined
  )
*}

ML {*
 fun ml_goal (txt, pos) ctxt =   
        ((ctxt |>
         Context.proof_map (ML_Context.expression Position.none 
                 "val goalf : local_theory -> Proof.state"
                  "Context.map_proof (ML_goal.put goalf)"  (ML_Lex.read pos txt)) |>
         ML_goal.get) ctxt) :Proof.state
*}

ML {*
val _ =
  Outer_Syntax.local_theory_to_proof @{command_spec "ML_goal"} "ML goal function"
    (Parse.ML_source >> ml_goal)
*}

ML {*
  fun start_theorem prop = Proof.theorem NONE (K I) [[(prop, [])]]
*}

end