diff -r dd8eebae11ec -r 123401a5c8e9 CookBook/Parsing.thy --- a/CookBook/Parsing.thy Thu Feb 05 22:44:11 2009 +0000 +++ b/CookBook/Parsing.thy Fri Feb 06 06:19:52 2009 +0000 @@ -515,38 +515,104 @@ *} -ML{* - OuterParse.position -*} - - section {* Parsing Inner Syntax *} -ML{* -let +ML{*let val input = OuterSyntax.scan Position.none "0" in OuterParse.prop input -end +end*} + +text {* (FIXME funny output for a proposition) *} + +section {* Parsing Specifications *} + +text {* + There are a number of special purpose parsers that help for parsing specifications. + For example the function @{ML OuterParse.target} reads a target in order to indicate + a locale. + +@{ML_response [display,gray] +"let + 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}. *} -ML{* - OuterParse.opt_target +text {* + +@{ML_response [display,gray] +"let + val input = filtered_input + \"foo::\\\"int \ bool\\\" (\\\"FOO\\\" [100] 100) and bar::nat and blonk\" +in + parse OuterParse.fixes input +end" +"([(foo, SOME \, Mixfix (\"FOO\",[100],100)), + (bar, SOME \, NoSyn), + (blonk, NONE, NoSyn)],[])"} + + The types of the constants is stored in the @{ML SOME}s. + We need to write @{text "\\\"int \ 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 {* (FIXME funny output for a proposition) *} +text {* +@{ML_response [display,gray] +"let + val input = filtered_input + (\"even and odd \" ^ + \"where \" ^ + \" even0[intro]: \\\"even 0\\\" \" ^ + \"| evenS[intro]: \\\"odd n \ even (Suc n)\\\" \" ^ + \"| oddS[intro]: \\\"even n \ odd (Suc n)\\\"\") -ML{* - OuterParse.opt_target -- - OuterParse.fixes -- - OuterParse.for_fixes -- - Scan.optional (OuterParse.$$$ "where" |-- - OuterParse.!!! (OuterParse.enum1 "|" (SpecParse.opt_thm_name ":" -- OuterParse.prop))) [] - + 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,\), \"\\^E\\^Ftoken\\^Eeven 0\\^E\\^F\\^E\"), + ((evenS,\), \"\\^E\\^Ftoken\\^Eodd n \ even (Suc n)\\^E\\^F\\^E\"), + ((oddS,\), \"\\^E\\^Ftoken\\^Eeven n \ odd (Suc n)\\^E\\^F\\^E\")]), [])"} *} -ML{* OuterSyntax.command *} +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 *} @@ -575,7 +641,7 @@ 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: @@ -586,7 +652,7 @@ 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. @@ -633,7 +699,7 @@ @{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"} @@ -647,17 +713,17 @@ ./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 - in the directory + If the compilation succeeds, you have finally created all the necessary log files. + They are stored in the directory @{text [display] "~/.isabelle/heaps/Isabelle2008/polyml-5.2.1_x86-linux/log"} @@ -674,7 +740,7 @@ 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: @@ -687,14 +753,14 @@ 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"}, - then we can make use of the command \isacommand{foobar}. + If you now build a theory on top of @{text "Command.thy"}, + then the command \isacommand{foobar} can be used. Similarly with any other new command. @@ -710,7 +776,6 @@ 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 @@ -797,7 +862,11 @@ 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)