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