isabelle-cookbook: comparison CookBook/Parsing.thy

equal deleted inserted replaced

-:dd8eebae11ec
+:123401a5c8e9
 @{ML OuterParse.position}
 *}
-ML{*
-OuterParse.position
-*}
 section {* Parsing Inner Syntax *}
-ML{*
+ML{*let
-let
 val input = OuterSyntax.scan Position.none "0"
 in
 OuterParse.prop input
-end
+end*}
-*}
-ML{*
-OuterParse.opt_target
-*}
 text {* (FIXME funny output for a proposition) *}
-ML{*
+section {* Parsing Specifications *}
-OuterParse.opt_target --
-OuterParse.fixes --
+text {*
-OuterParse.for_fixes --
+There are a number of special purpose parsers that help for parsing specifications.
-Scan.optional (OuterParse.$$$ "where" |--
+For example the function @{ML OuterParse.target} reads a target in order to indicate
-OuterParse.!!! (OuterParse.enum1 "|" (SpecParse.opt_thm_name ":" -- OuterParse.prop))) []
+a locale.
-*}
+@{ML_response [display,gray]
+"let
-ML{* OuterSyntax.command *}
+val input = filtered_input \"(in test)\"
+in
+parse OuterParse.target input
+end" "(\"test\",[])"}
+The function @{ML OuterParse.opt_target} makes this parser ``optional''.
+The function @{ML OuterParse.fixes} reads a list of constants
+which can include a type annotation and a syntax translation.
+The list needs to be separated by \isacommand{and}.
+*}
+text {*
+@{ML_response [display,gray]
+"let
+val input = filtered_input
+\"foo::\\\"int \<Rightarrow> bool\\\" (\\\"FOO\\\" [100] 100) and bar::nat and blonk\"
+in
+parse OuterParse.fixes input
+end"
+"([(foo, SOME \<dots>, Mixfix (\"FOO\",[100],100)),
+(bar, SOME \<dots>, NoSyn),
+(blonk, NONE, NoSyn)],[])"}
+The types of the constants is stored in the @{ML SOME}s.
+We need to write @{text "\\\"int \<Rightarrow> bool\\\""} to properly
+escape the type.
+@{ML OuterParse.for_fixes} is an ``optional'' that prefixes
+@{ML OuterParse.fixes} with the comman \isacommand{for}.
+*}
+ML{*let
+val input = filtered_input "test_lemma[intro,foo,elim,dest!,bar]:"
+in
+parse (SpecParse.thm_name ":") input
+|> fst |> snd |> (Attrib.pretty_attribs @{context}) |> (map Pretty.string_of)
+end*}
+text {*
+(FIXME: why is intro, elim and dest treated differently from bar?)
+*}
+text {*
+@{ML_response [display,gray]
+"let
+val input = filtered_input
+(\"even and odd \" ^
+\"where \" ^
+\"  even0[intro]: \\\"even 0\\\" \" ^
+\"| evenS[intro]: \\\"odd n \<Longrightarrow> even (Suc n)\\\" \" ^
+\"| oddS[intro]:  \\\"even n \<Longrightarrow> odd (Suc n)\\\"\")
+val parser =
+OuterParse.opt_target --
+OuterParse.fixes --
+OuterParse.for_fixes --
+Scan.optional
+(OuterParse.$$$ \"where\" |--
+OuterParse.!!!
+(OuterParse.enum1 \"|\"
+(SpecParse.opt_thm_name \":\" -- OuterParse.prop))) []
+in
+parse parser input
+end"
+"((((NONE, [(even, NONE, NoSyn), (odd, NONE, NoSyn)]), []),
+[((even0,\<dots>), \"\\^E\\^Ftoken\\^Eeven 0\\^E\\^F\\^E\"),
+((evenS,\<dots>), \"\\^E\\^Ftoken\\^Eodd n \<Longrightarrow> even (Suc n)\\^E\\^F\\^E\"),
+((oddS,\<dots>), \"\\^E\\^Ftoken\\^Eeven n \<Longrightarrow> odd (Suc n)\\^E\\^F\\^E\")]), [])"}
+*}
+text {*
+The (outer?) parser for the package: returns optionally a locale;
+a list of predicate constants with optional type-annotation and
+optional syntax-annotation; a list of for-fixes (fixed parameters);
+and a list of rules where each rule has optionally a name and an attribute.
+*}
 section {* New Commands and Keyword Files *}
 text {*
 Often new commands, for example for providing new definitional principles,
 The crucial function @{ML OuterSyntax.command} expects a name for the command, a
 short description, a kind indicator (which we will explain later on more thoroughly) and a
 parser producing a top-level transition function (its purpose will also explained
 later).
-While this is everything we have to do on the ML-level, we need a keyword
+While this is everything you have to do on the ML-level, you need a keyword
 file that can be loaded by ProofGeneral. This is to enable ProofGeneral to
 recognise \isacommand{foobar} as a command. Such a keyword file can be
 generated with the command-line:
 @{text [display] "$ isabelle keywords -k foobar some_log_files"}
 The option @{text "-k foobar"} indicates which postfix the name of the keyword file
 will be assigned. In the case above the file will be named @{text
 "isar-keywords-foobar.el"}. This command requires log files to be
 present (in order to extract the keywords from them). To generate these log
-files, we first package the code above into a separate theory file named
+files, you first need to package the code above into a separate theory file named
 @{text "Command.thy"}, say---see Figure~\ref{fig:commandtheory} for the
 complete code.
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 The @{text "Pure-ProofGeneral"} theory needs to be compiled with
 @{text [display] "$ ./build -m \"Pure-ProofGeneral\" \"Pure\""}
-For the theory @{text "Command.thy"}, we first create a ``managed'' subdirectory
+For the theory @{text "Command.thy"}, you first need to create a ``managed'' subdirectory
 with
 @{text [display] "$ isabelle mkdir FoobarCommand"}
 This generates a directory containing the files
 ./FoobarCommand/ROOT.ML
 ./FoobarCommand/document
 ./FoobarCommand/document/root.tex"}
-We need to copy the file @{text "Command.thy"} into the directory @{text "FoobarCommand"}
+You need to copy the file @{text "Command.thy"} into the directory @{text "FoobarCommand"}
 and add the line
 @{text [display] "use_thy \"Command\";"}
-to the file @{text "./FoobarCommand/ROOT.ML"}. We can now compile the theory by just typing
+to the file @{text "./FoobarCommand/ROOT.ML"}. You can now compile the theory by just typing
 @{text [display] "$ isabelle make"}
-We created finally all the necessary log files. They are stored
+If the compilation succeeds, you have finally created all the necessary log files.
-in the directory
+They are stored in the directory
 @{text [display]  "~/.isabelle/heaps/Isabelle2008/polyml-5.2.1_x86-linux/log"}
 or something similar depending on your Isabelle distribution and architecture.
 One quick way to assign a shell variable to this directory is by typing
 "Pure.gz
 HOL.gz
 Pure-ProofGeneral.gz
 HOL-FoobarCommand.gz"}
-From them we create the keyword files. Assuming the name
+From them you can create the keyword files. Assuming the name
 of the directory is in  @{text "$ISABELLE_LOGS"},
 then the Unix command for creating the keyword file is:
 @{text [display]
 "$ isabelle keywords -k foobar
 The result is the file @{text "isar-keywords-foobar.el"}. It should contain
 the string @{text "foobar"} twice.\footnote{To see whether things are fine, check
 that @{text "grep foobar"} on this file returns something
 non-empty.}  This keyword file needs to
 be copied into the directory @{text "~/.isabelle/etc"}. To make Isabelle
-aware of this keyword file, we have to start Isabelle with the option @{text
+aware of this keyword file, you have to start Isabelle with the option @{text
 "-k foobar"}, i.e.
 @{text [display] "$ isabelle -k foobar a_theory_file"}
-If we now build a theory on top of @{text "Command.thy"},
+If you now build a theory on top of @{text "Command.thy"},
-then we can make use of the command \isacommand{foobar}.
+then the command \isacommand{foobar} can be used.
 Similarly with any other new command.
 At the moment \isacommand{foobar} is not very useful. Let us refine it a bit
 next by taking a proposition as argument and printing this proposition inside
 returns the simple toplevel function @{ML "Toplevel.theory I"}. We can
 replace this code by a function that first parses a proposition (using the
 parser @{ML OuterParse.prop}), then prints out the tracing
 information (using a new top-level function @{text trace_top_lvl}) and
 finally does nothing. For this we can write
 *}
 ML{*let
 fun trace_top_lvl str =
 Toplevel.theory (fn thy => (tracing str; thy))
 \end{isabelle}
 Similarly for the other function composition combinators.
-(FIXME What does @{text "Toplevel.theory"} @{text "Toplevel.print"}?)
+(FIXME What do @{ML "Toplevel.theory"}
+@{ML "Toplevel.print"}
+@{ML Toplevel.local_theory}?)
 (FIXME read a name and show how to store theorems)
 (FIXME possibly also read a locale)
 *}

changeset 101	123401a5c8e9
parent 86	fdb9ea86c2a3
child 102	5e309df58557