--- a/src/HOL/Tools/Predicate_Compile/predicate_compile.ML Fri Nov 06 08:11:58 2009 +0100
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile.ML Fri Nov 06 08:11:58 2009 +0100
@@ -155,6 +155,8 @@
local structure P = OuterParse
in
+(* Parser for mode annotations *)
+
(*val parse_argmode' = P.nat >> rpair NONE || P.$$$ "(" |-- P.enum1 "," --| P.$$$ ")"*)
datatype raw_argmode = Argmode of string | Argmode_Tuple of string list
@@ -185,16 +187,37 @@
Scan.optional (P.$$$ "(" |-- Args.$$$ "mode" |-- P.$$$ ":" |--
P.enum1 "," (parse_mode || parse_mode') --| P.$$$ ")" >> SOME) NONE
-val scan_params =
+(* Parser for options *)
+
+val scan_options =
let
- val scan_bool_param = foldl1 (op ||) (map Args.$$$ bool_options)
+ val scan_bool_option = foldl1 (op ||) (map Args.$$$ bool_options)
in
- Scan.optional (P.$$$ "[" |-- P.enum1 "," scan_bool_param --| P.$$$ "]") []
+ Scan.optional (P.$$$ "[" |-- P.enum1 "," scan_bool_option --| P.$$$ "]") []
end
+val opt_print_modes = Scan.optional (P.$$$ "(" |-- P.!!! (Scan.repeat1 P.xname --| P.$$$ ")")) [];
+
+val value_options =
+ let
+ val depth_limit = Scan.optional (Args.$$$ "depth_limit" |-- P.$$$ "=" |-- P.nat >> SOME) NONE
+ val random = Scan.optional (Args.$$$ "random" >> K true) false
+ val annotated = Scan.optional (Args.$$$ "annotated" >> K true) false
+ in
+ Scan.optional (P.$$$ "[" |-- depth_limit -- (random -- annotated) --| P.$$$ "]")
+ (NONE, (false, false))
+ end
+
+(* code_pred command and values command *)
+
val _ = OuterSyntax.local_theory_to_proof "code_pred"
"prove equations for predicate specified by intro/elim rules"
- OuterKeyword.thy_goal (opt_modes -- scan_params -- P.term_group >> code_pred_cmd)
+ OuterKeyword.thy_goal (opt_modes -- scan_options -- P.term_group >> code_pred_cmd)
+
+val _ = OuterSyntax.improper_command "values" "enumerate and print comprehensions" OuterKeyword.diag
+ (opt_print_modes -- value_options -- Scan.optional P.nat ~1 -- P.term
+ >> (fn (((modes, options), k), t) => Toplevel.no_timing o Toplevel.keep
+ (Predicate_Compile_Core.values_cmd modes options k t)));
end