Re: [isabelle] Custom Isar Commands



On Tue, 18 Oct 2011, Matthew wrote:

In the first step of building an automatic tool, I am trying to set up
an Isar-level command

File test.ml
----------------------------------------

signature TEST =
sig
end

structure Test : TEST =
struct

fun test_function a =
 writeln( "test function called" )
 |> K(K(Toplevel.empty),a)

fun test_params_function a =
 writeln( "test params function called" )
 |> K(K(Toplevel.empty),a)

val _ = Outer_Syntax.improper_command "test"
           "test the Outer_Syntax.improper_command function"
           Keyword.diag test_function
val _ = Outer_Syntax.command "test_params"
           "test the Outer_Syntax.command function"
           Keyword.thy_decl test_params_function

end

------------------------------------
End file test.ml

Here are some general hints:

  * Isabelle/ML files should always have an .ML extension, not .ml or .sml

  * Small ML things are more easily develepd directly in ML {* ... *}
    chunks within a theory.

  * Proof General requires commands declared statically in a keyword
    file.  It was already pointed out that the cookbook by Christian Urban
    provides some hints on that.

  * The Isabelle/jEdit Prover IDE, which is particulaly nice for ML
    development (as of Isabelle2011-1), requires some trickery though
    to make it accept newly created Isar commands dynamically at runtime.

  * K(K(Toplevel.empty),a) is an odd way to make an outer parser that
    produces an Isar toplevel transition.  Where did you see the example?

Here is my version of your test. It imitates some of the basic print commands in ~~/src/Pure/Isar/isar_syn.ML (the file where the main Isabelle/Pure commands are defined):

ML {*

val _ =
  Outer_Syntax.improper_command "test" "test command" Keyword.diag
    (Scan.succeed
      (Toplevel.no_timing o Toplevel.imperative (fn () => writeln "test")));

*}

Above I have inlined the parser expression and the construction of the toplevel transaction into the command definition. This is more robust wrt. type inference issues than a bottom-up sequence of auxiliary building blocks like test_function above. (That form was preferred in a time where Poly/ML produced very bad type error messages for combinator expressions.)


	Makarius





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.