# HG changeset patch # User bulwahn # Date 1257491518 -3600 # Node ID b70fe083694daa7de7081fcbcd2cc273e91e4b83 # Parent 1272cfc7b910416f3627daeb61a07e92e9c9520a moved values command from core to predicate compile diff -r 1272cfc7b910 -r b70fe083694d src/HOL/Tools/Predicate_Compile/predicate_compile.ML --- 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 diff -r 1272cfc7b910 -r b70fe083694d src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML Fri Nov 06 08:11:58 2009 +0100 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML Fri Nov 06 08:11:58 2009 +0100 @@ -6,9 +6,10 @@ signature PREDICATE_COMPILE_CORE = sig - val setup: theory -> theory - val code_pred: Predicate_Compile_Aux.options -> string -> Proof.context -> Proof.state - val code_pred_cmd: Predicate_Compile_Aux.options -> string -> Proof.context -> Proof.state + val setup : theory -> theory + val code_pred : Predicate_Compile_Aux.options -> string -> Proof.context -> Proof.state + val code_pred_cmd : Predicate_Compile_Aux.options -> string -> Proof.context -> Proof.state + val values_cmd : string list -> int option * (bool * bool) -> int -> string -> Toplevel.state -> unit val register_predicate : (string * thm list * thm * int) -> theory -> theory val register_intros : string * thm list -> theory -> theory val is_registered : theory -> string -> bool @@ -23,13 +24,13 @@ val generator_name_of : theory -> string -> Predicate_Compile_Aux.mode -> string val all_modes_of : theory -> (string * Predicate_Compile_Aux.mode list) list val all_generator_modes_of : theory -> (string * Predicate_Compile_Aux.mode list) list - val intros_of: theory -> string -> thm list - val nparams_of: theory -> string -> int - val add_intro: thm -> theory -> theory - val set_elim: thm -> theory -> theory + val intros_of : theory -> string -> thm list + val nparams_of : theory -> string -> int + val add_intro : thm -> theory -> theory + val set_elim : thm -> theory -> theory val set_nparams : string -> int -> theory -> theory - val print_stored_rules: theory -> unit - val print_all_modes: theory -> unit + val print_stored_rules : theory -> unit + val print_all_modes : theory -> unit val mk_casesrule : Proof.context -> term -> int -> thm list -> term val eval_ref : (unit -> term Predicate.pred) option Unsynchronized.ref val random_eval_ref : (unit -> int * int -> term Predicate.pred * (int * int)) option Unsynchronized.ref @@ -2564,37 +2565,16 @@ in end; *) -fun values_cmd modes options k raw_t state = +fun values_cmd print_modes options k raw_t state = let val ctxt = Toplevel.context_of state; val t = Syntax.read_term ctxt raw_t; val t' = values ctxt options k t; val ty' = Term.type_of t'; val ctxt' = Variable.auto_fixes t' ctxt; - val p = PrintMode.with_modes modes (fn () => + val p = PrintMode.with_modes print_modes (fn () => Pretty.block [Pretty.quote (Syntax.pretty_term ctxt' t'), Pretty.fbrk, Pretty.str "::", Pretty.brk 1, Pretty.quote (Syntax.pretty_typ ctxt' ty')]) (); in Pretty.writeln p end; -local structure P = OuterParse in - -val opt_modes = Scan.optional (P.$$$ "(" |-- P.!!! (Scan.repeat1 P.xname --| P.$$$ ")")) []; - -val 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 - -val _ = OuterSyntax.improper_command "values" "enumerate and print comprehensions" OuterKeyword.diag - (opt_modes -- options -- Scan.optional P.nat ~1 -- P.term - >> (fn (((modes, options), k), t) => Toplevel.no_timing o Toplevel.keep - (values_cmd modes options k t))); - end; - -end;