--- a/NEWS Thu Jun 30 19:24:09 2011 +0200
+++ b/NEWS Fri Jul 01 14:17:02 2011 +0200
@@ -126,6 +126,8 @@
* Antiquotation @{rail} layouts railroad syntax diagrams, see also
isar-ref manual.
+* Antiquotation @{value} evaluates the given term and presents its result.
+
* Localized \isabellestyle switch can be used within blocks or groups
like this:
--- a/doc-src/IsarRef/Thy/Document_Preparation.thy Thu Jun 30 19:24:09 2011 +0200
+++ b/doc-src/IsarRef/Thy/Document_Preparation.thy Fri Jul 01 14:17:02 2011 +0200
@@ -188,6 +188,7 @@
@@{antiquotation lemma} options @{syntax prop} @'by' @{syntax method} @{syntax method}? |
@@{antiquotation prop} options styles @{syntax prop} |
@@{antiquotation term} options styles @{syntax term} |
+ @@{antiquotation value} options styles @{syntax term} |
@@{antiquotation term_type} options styles @{syntax term} |
@@{antiquotation typeof} options styles @{syntax term} |
@@{antiquotation const} options @{syntax term} |
@@ -236,6 +237,8 @@
@{text "\<phi>"} by method @{text m} and prints the original @{text "\<phi>"}.
\item @{text "@{term t}"} prints a well-typed term @{text "t"}.
+
+ \item @{text "@{value t}"} evaluates a term @{text "t"} and prints its result.
\item @{text "@{term_type t}"} prints a well-typed term @{text "t"}
annotated with its type.
--- a/doc-src/IsarRef/Thy/document/Document_Preparation.tex Thu Jun 30 19:24:09 2011 +0200
+++ b/doc-src/IsarRef/Thy/document/Document_Preparation.tex Fri Jul 01 14:17:02 2011 +0200
@@ -235,7 +235,7 @@
\rail@nont{\isa{antiquotation}}[]
\rail@term{\isa{{\isaliteral{7D}{\isacharbraceright}}}}[]
\rail@end
-\rail@begin{22}{\indexdef{}{syntax}{antiquotation}\hypertarget{syntax.antiquotation}{\hyperlink{syntax.antiquotation}{\mbox{\isa{antiquotation}}}}}
+\rail@begin{23}{\indexdef{}{syntax}{antiquotation}\hypertarget{syntax.antiquotation}{\hyperlink{syntax.antiquotation}{\mbox{\isa{antiquotation}}}}}
\rail@bar
\rail@term{\hyperlink{antiquotation.theory}{\mbox{\isa{theory}}}}[]
\rail@nont{\isa{options}}[]
@@ -266,66 +266,71 @@
\rail@nont{\isa{styles}}[]
\rail@nont{\hyperlink{syntax.term}{\mbox{\isa{term}}}}[]
\rail@nextbar{6}
-\rail@term{\hyperlink{antiquotation.term-type}{\mbox{\isa{term{\isaliteral{5F}{\isacharunderscore}}type}}}}[]
+\rail@term{\hyperlink{antiquotation.value}{\mbox{\isa{value}}}}[]
\rail@nont{\isa{options}}[]
\rail@nont{\isa{styles}}[]
\rail@nont{\hyperlink{syntax.term}{\mbox{\isa{term}}}}[]
\rail@nextbar{7}
-\rail@term{\hyperlink{antiquotation.typeof}{\mbox{\isa{typeof}}}}[]
+\rail@term{\hyperlink{antiquotation.term-type}{\mbox{\isa{term{\isaliteral{5F}{\isacharunderscore}}type}}}}[]
\rail@nont{\isa{options}}[]
\rail@nont{\isa{styles}}[]
\rail@nont{\hyperlink{syntax.term}{\mbox{\isa{term}}}}[]
\rail@nextbar{8}
+\rail@term{\hyperlink{antiquotation.typeof}{\mbox{\isa{typeof}}}}[]
+\rail@nont{\isa{options}}[]
+\rail@nont{\isa{styles}}[]
+\rail@nont{\hyperlink{syntax.term}{\mbox{\isa{term}}}}[]
+\rail@nextbar{9}
\rail@term{\hyperlink{antiquotation.const}{\mbox{\isa{const}}}}[]
\rail@nont{\isa{options}}[]
\rail@nont{\hyperlink{syntax.term}{\mbox{\isa{term}}}}[]
-\rail@nextbar{9}
+\rail@nextbar{10}
\rail@term{\hyperlink{antiquotation.abbrev}{\mbox{\isa{abbrev}}}}[]
\rail@nont{\isa{options}}[]
\rail@nont{\hyperlink{syntax.term}{\mbox{\isa{term}}}}[]
-\rail@nextbar{10}
+\rail@nextbar{11}
\rail@term{\hyperlink{antiquotation.typ}{\mbox{\isa{typ}}}}[]
\rail@nont{\isa{options}}[]
\rail@nont{\hyperlink{syntax.type}{\mbox{\isa{type}}}}[]
-\rail@nextbar{11}
+\rail@nextbar{12}
\rail@term{\hyperlink{antiquotation.type}{\mbox{\isa{type}}}}[]
\rail@nont{\isa{options}}[]
\rail@nont{\hyperlink{syntax.name}{\mbox{\isa{name}}}}[]
-\rail@nextbar{12}
+\rail@nextbar{13}
\rail@term{\hyperlink{antiquotation.class}{\mbox{\isa{class}}}}[]
\rail@nont{\isa{options}}[]
\rail@nont{\hyperlink{syntax.name}{\mbox{\isa{name}}}}[]
-\rail@nextbar{13}
-\rail@term{\hyperlink{antiquotation.text}{\mbox{\isa{text}}}}[]
-\rail@nont{\isa{options}}[]
-\rail@nont{\hyperlink{syntax.name}{\mbox{\isa{name}}}}[]
\rail@nextbar{14}
+\rail@term{\hyperlink{antiquotation.text}{\mbox{\isa{text}}}}[]
+\rail@nont{\isa{options}}[]
+\rail@nont{\hyperlink{syntax.name}{\mbox{\isa{name}}}}[]
+\rail@nextbar{15}
\rail@term{\hyperlink{antiquotation.goals}{\mbox{\isa{goals}}}}[]
\rail@nont{\isa{options}}[]
-\rail@nextbar{15}
+\rail@nextbar{16}
\rail@term{\hyperlink{antiquotation.subgoals}{\mbox{\isa{subgoals}}}}[]
\rail@nont{\isa{options}}[]
-\rail@nextbar{16}
+\rail@nextbar{17}
\rail@term{\hyperlink{antiquotation.prf}{\mbox{\isa{prf}}}}[]
\rail@nont{\isa{options}}[]
\rail@nont{\hyperlink{syntax.thmrefs}{\mbox{\isa{thmrefs}}}}[]
-\rail@nextbar{17}
+\rail@nextbar{18}
\rail@term{\hyperlink{antiquotation.full-prf}{\mbox{\isa{full{\isaliteral{5F}{\isacharunderscore}}prf}}}}[]
\rail@nont{\isa{options}}[]
\rail@nont{\hyperlink{syntax.thmrefs}{\mbox{\isa{thmrefs}}}}[]
-\rail@nextbar{18}
+\rail@nextbar{19}
\rail@term{\hyperlink{antiquotation.ML}{\mbox{\isa{ML}}}}[]
\rail@nont{\isa{options}}[]
\rail@nont{\hyperlink{syntax.name}{\mbox{\isa{name}}}}[]
-\rail@nextbar{19}
+\rail@nextbar{20}
\rail@term{\hyperlink{antiquotation.ML-type}{\mbox{\isa{ML{\isaliteral{5F}{\isacharunderscore}}type}}}}[]
\rail@nont{\isa{options}}[]
\rail@nont{\hyperlink{syntax.name}{\mbox{\isa{name}}}}[]
-\rail@nextbar{20}
+\rail@nextbar{21}
\rail@term{\hyperlink{antiquotation.ML-struct}{\mbox{\isa{ML{\isaliteral{5F}{\isacharunderscore}}struct}}}}[]
\rail@nont{\isa{options}}[]
\rail@nont{\hyperlink{syntax.name}{\mbox{\isa{name}}}}[]
-\rail@nextbar{21}
+\rail@nextbar{22}
\rail@term{\hyperlink{antiquotation.file}{\mbox{\isa{file}}}}[]
\rail@nont{\isa{options}}[]
\rail@nont{\hyperlink{syntax.name}{\mbox{\isa{name}}}}[]
@@ -390,6 +395,8 @@
\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C7068693E}{\isasymphi}}{\isaliteral{22}{\isachardoublequote}}} by method \isa{m} and prints the original \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C7068693E}{\isasymphi}}{\isaliteral{22}{\isachardoublequote}}}.
\item \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{40}{\isacharat}}{\isaliteral{7B}{\isacharbraceleft}}term\ t{\isaliteral{7D}{\isacharbraceright}}{\isaliteral{22}{\isachardoublequote}}} prints a well-typed term \isa{{\isaliteral{22}{\isachardoublequote}}t{\isaliteral{22}{\isachardoublequote}}}.
+
+ \item \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{40}{\isacharat}}{\isaliteral{7B}{\isacharbraceleft}}value\ t{\isaliteral{7D}{\isacharbraceright}}{\isaliteral{22}{\isachardoublequote}}} evaluates a term \isa{{\isaliteral{22}{\isachardoublequote}}t{\isaliteral{22}{\isachardoublequote}}} and prints its result.
\item \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{40}{\isacharat}}{\isaliteral{7B}{\isacharbraceleft}}term{\isaliteral{5F}{\isacharunderscore}}type\ t{\isaliteral{7D}{\isacharbraceright}}{\isaliteral{22}{\isachardoublequote}}} prints a well-typed term \isa{{\isaliteral{22}{\isachardoublequote}}t{\isaliteral{22}{\isachardoublequote}}}
annotated with its type.
--- a/src/HOL/IsaMakefile Thu Jun 30 19:24:09 2011 +0200
+++ b/src/HOL/IsaMakefile Fri Jul 01 14:17:02 2011 +0200
@@ -150,6 +150,7 @@
$(SRC)/Tools/project_rule.ML \
$(SRC)/Tools/quickcheck.ML \
$(SRC)/Tools/solve_direct.ML \
+ $(SRC)/Tools/subtyping.ML \
$(SRC)/Tools/try.ML \
$(SRC)/Tools/value.ML \
HOL.thy \
@@ -168,7 +169,6 @@
$(SRC)/Provers/trancl.ML \
$(SRC)/Tools/Metis/metis.ML \
$(SRC)/Tools/rat.ML \
- $(SRC)/Tools/subtyping.ML \
Complete_Lattice.thy \
Complete_Partial_Order.thy \
Datatype.thy \
--- a/src/Pure/General/file.ML Thu Jun 30 19:24:09 2011 +0200
+++ b/src/Pure/General/file.ML Fri Jul 01 14:17:02 2011 +0200
@@ -21,7 +21,6 @@
val open_input: (TextIO.instream -> 'a) -> Path.T -> 'a
val open_output: (TextIO.outstream -> 'a) -> Path.T -> 'a
val open_append: (TextIO.outstream -> 'a) -> Path.T -> 'a
- val fold_fields: (char -> bool) -> (string -> 'a -> 'a) -> Path.T -> 'a -> 'a
val fold_lines: (string -> 'a -> 'a) -> Path.T -> 'a -> 'a
val read: Path.T -> string
val write: Path.T -> string -> unit
@@ -111,21 +110,19 @@
(* input *)
(*scalable iterator -- avoid size limit of TextIO.inputAll, and overhead of many TextIO.inputLine*)
-fun fold_fields sep f path a = open_input (fn file =>
+fun fold_lines f path a = open_input (fn file =>
let
fun read buf x =
(case TextIO.input file of
"" => (case Buffer.content buf of "" => x | line => f line x)
| input =>
- (case String.fields sep input of
+ (case String.fields (fn c => c = #"\n") input of
[rest] => read (Buffer.add rest buf) x
- | field :: more => read_fields more (f (Buffer.content (Buffer.add field buf)) x)))
- and read_fields [rest] x = read (Buffer.add rest Buffer.empty) x
- | read_fields (field :: more) x = read_fields more (f field x);
+ | line :: more => read_lines more (f (Buffer.content (Buffer.add line buf)) x)))
+ and read_lines [rest] x = read (Buffer.add rest Buffer.empty) x
+ | read_lines (line :: more) x = read_lines more (f line x);
in read Buffer.empty a end) path;
-fun fold_lines f path a = fold_fields (fn c => c = #"\n") f path a;
-
val read = open_input TextIO.inputAll;
--- a/src/Pure/General/yxml.ML Thu Jun 30 19:24:09 2011 +0200
+++ b/src/Pure/General/yxml.ML Fri Jul 01 14:17:02 2011 +0200
@@ -21,7 +21,6 @@
val string_of: XML.tree -> string
val parse_body: string -> XML.body
val parse: string -> XML.tree
- val parse_file: (XML.tree -> 'a -> 'a) -> Path.T -> 'a -> 'a
end;
structure YXML: YXML =
@@ -107,7 +106,6 @@
fun pop ((("", _), _) :: _) = err_unbalanced ""
| pop ((markup, body) :: pending) = add (XML.Elem (markup, rev body)) pending;
-val stack_init = [(("", []), [])];
(* parsing *)
@@ -121,16 +119,10 @@
| parse_chunk ("" :: name :: atts) = push name (map parse_attrib atts)
| parse_chunk txts = fold (add o XML.Text) txts;
-fun preparse_chunk _ "" x = x
- | preparse_chunk f str (pending, results) =
- (case parse_chunk (String.fields (is_char Y) str) pending of
- [(("", _), [result])] => (stack_init, f result results)
- | x => (x, results));
-
in
fun parse_body source =
- (case fold parse_chunk (split_string source) stack_init of
+ (case fold parse_chunk (split_string source) [(("", []), [])] of
[(("", _), result)] => rev result
| ((name, _), _) :: _ => err_unbalanced name);
@@ -140,13 +132,6 @@
| [] => XML.Text ""
| _ => err "multiple results");
-(*folds a function over each XML.Tree in the file*)
-fun parse_file f path s =
- (case File.fold_fields (is_char X) (preparse_chunk f)
- path (stack_init, s) of
- ([(("", _), [])], result) => result
- | (((name, _), _) :: _, _) => err_unbalanced name);
-
end;
end;
--- a/src/Tools/Code_Generator.thy Thu Jun 30 19:24:09 2011 +0200
+++ b/src/Tools/Code_Generator.thy Fri Jul 01 14:17:02 2011 +0200
@@ -34,6 +34,7 @@
#> Code_Haskell.setup
#> Code_Scala.setup
#> Quickcheck.setup
+ #> Value.setup
*}
code_datatype "TYPE('a\<Colon>{})"
--- a/src/Tools/value.ML Thu Jun 30 19:24:09 2011 +0200
+++ b/src/Tools/value.ML Fri Jul 01 14:17:02 2011 +0200
@@ -10,6 +10,7 @@
val value_select: string -> Proof.context -> term -> term
val value_cmd: string option -> string list -> string -> Toplevel.state -> unit
val add_evaluator: string * (Proof.context -> term -> term) -> theory -> theory
+ val setup : theory -> theory
end;
structure Value : VALUE =
@@ -38,13 +39,16 @@
| NONE => evaluator ctxt t
end end;
+fun value_maybe_select some_name =
+ case some_name
+ of NONE => value
+ | SOME name => value_select name;
+
fun value_cmd some_name modes raw_t state =
let
val ctxt = Toplevel.context_of state;
val t = Syntax.read_term ctxt raw_t;
- val t' = case some_name
- of NONE => value ctxt t
- | SOME name => value_select name ctxt t;
+ val t' = value_maybe_select some_name ctxt t;
val ty' = Term.type_of t';
val ctxt' = Variable.auto_fixes t' ctxt;
val p = Print_Mode.with_modes modes (fn () =>
@@ -55,10 +59,22 @@
val opt_modes =
Scan.optional (Parse.$$$ "(" |-- Parse.!!! (Scan.repeat1 Parse.xname --| Parse.$$$ ")")) [];
+val opt_evaluator =
+ Scan.option (Parse.$$$ "[" |-- Parse.xname --| Parse.$$$ "]")
+
val _ =
Outer_Syntax.improper_command "value" "evaluate and print term" Keyword.diag
- (Scan.option (Parse.$$$ "[" |-- Parse.xname --| Parse.$$$ "]") -- opt_modes -- Parse.term
+ (opt_evaluator -- opt_modes -- Parse.term
>> (fn ((some_name, modes), t) => Toplevel.no_timing o Toplevel.keep
(value_cmd some_name modes t)));
+val antiq_setup =
+ Thy_Output.antiquotation (Binding.name "value")
+ (Scan.lift opt_evaluator -- Term_Style.parse -- Args.term)
+ (fn {source, context, ...} => fn ((some_name, style), t) => Thy_Output.output context
+ (Thy_Output.maybe_pretty_source Thy_Output.pretty_term context source
+ [style (value_maybe_select some_name context t)]));
+
+val setup = antiq_setup;
+
end;