--- a/src/HOL/ex/Predicate_Compile.thy Wed May 20 22:24:07 2009 +0200
+++ b/src/HOL/ex/Predicate_Compile.thy Wed May 20 22:24:07 2009 +0200
@@ -7,39 +7,53 @@
setup {* Predicate_Compile.setup *}
-
text {* Experimental code *}
-definition pred_map :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a Predicate.pred \<Rightarrow> 'b Predicate.pred" where
- "pred_map f P = Predicate.bind P (Predicate.single o f)"
-
ML {*
-structure Predicate =
+structure Predicate_Compile =
struct
-open Predicate;
-
-val pred_ref = ref (NONE : (unit -> term Predicate.pred) option);
+open Predicate_Compile;
-fun eval_pred thy t =
- Code_ML.eval NONE ("Predicate.pred_ref", pred_ref) @{code pred_map} thy (HOLogic.mk_term_of (fastype_of t) t) [];
+fun eval thy t_compr =
+ let
+ val t = Predicate_Compile.analyze_compr thy t_compr;
+ val Type (@{type_name Predicate.pred}, [T]) = fastype_of t;
+ fun mk_predT T = Type (@{type_name Predicate.pred}, [T]);
+ val T1 = T --> @{typ term};
+ val T2 = T1 --> mk_predT T --> mk_predT @{typ term};
+ val t' = Const (@{const_name Predicate.map}, T2) (*FIXME*)
+ $ Const (@{const_name Code_Eval.term_of}, T1) $ t;
+ in (T, Code_ML.eval NONE ("Predicate_Compile.eval_ref", eval_ref) @{code Predicate.map} thy t' []) end;
-fun eval_pred_elems thy t T length =
- t |> eval_pred thy |> yieldn length |> fst |> HOLogic.mk_list T;
+fun values ctxt k t_compr =
+ let
+ val thy = ProofContext.theory_of ctxt;
+ val (T, t') = eval thy t_compr;
+ in t' |> Predicate.yieldn k |> fst |> HOLogic.mk_list T end;
-fun analyze_compr thy t =
+fun values_cmd modes k raw_t state =
let
- val split = case t of (Const (@{const_name Collect}, _) $ t') => t'
- | _ => error ("Not a set comprehension: " ^ Syntax.string_of_term_global thy t);
- val (body, Ts, fp) = HOLogic.strip_split split;
- val (t_pred, args) = strip_comb body;
- val pred = case t_pred of Const (pred, _) => pred
- | _ => error ("Not a constant: " ^ Syntax.string_of_term_global thy t_pred);
- val mode = map is_Bound args; (*FIXME what about higher-order modes?*)
- val args' = filter_out is_Bound args;
- val T = HOLogic.mk_tupleT fp Ts;
- val mk = HOLogic.mk_tuple' fp T;
- in (((pred, mode), args), (mk, T)) end;
+ val ctxt = Toplevel.context_of state;
+ val t = Syntax.read_term ctxt raw_t;
+ val t' = values ctxt k t;
+ val ty' = Term.type_of t';
+ val ctxt' = Variable.auto_fixes t' ctxt;
+ val p = PrintMode.with_modes 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;
+
+end;
+
+local structure P = OuterParse in
+
+val opt_modes = Scan.optional (P.$$$ "(" |-- P.!!! (Scan.repeat1 P.xname --| P.$$$ ")")) [];
+
+val _ = OuterSyntax.improper_command "values" "enumerate and print comprehensions" OuterKeyword.diag
+ (opt_modes -- Scan.optional P.nat ~1 -- P.term
+ >> (fn ((modes, k), t) => Toplevel.no_timing o Toplevel.keep
+ (Predicate_Compile.values_cmd modes k t)));
end;
*}
--- a/src/HOL/ex/Predicate_Compile_ex.thy Wed May 20 22:24:07 2009 +0200
+++ b/src/HOL/ex/Predicate_Compile_ex.thy Wed May 20 22:24:07 2009 +0200
@@ -12,7 +12,10 @@
thm even.equation
-ML_val {* Predicate.yieldn 10 @{code even_0} *}
+values "{x. even 2}"
+values "{x. odd 2}"
+values 10 "{n. even n}"
+values 10 "{n. odd n}"
inductive append :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list \<Rightarrow> bool" where
@@ -24,7 +27,9 @@
thm append.equation
-ML_val {* Predicate.yieldn 10 (@{code append_3} [1, 2, 3]) *}
+values "{(ys, xs). append xs ys [0, Suc 0, 2]}"
+values "{zs. append [0, Suc 0, 2] [17, 8] zs}"
+values "{ys. append [0, Suc 0, 2] ys [0, Suc 0, 2, 17, 0,5]}"
inductive partition :: "('a \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> 'a list \<Rightarrow> 'a list \<Rightarrow> bool"
@@ -38,10 +43,26 @@
thm partition.equation
+(*FIXME values 10 "{(ys, zs). partition (\<lambda>n. n mod 2 = 0)
+ [0, Suc 0, 2, 3, 4, 5, 6, 7] ys zs}"*)
+
code_pred tranclp
using assms by (rule tranclp.cases)
thm tranclp.equation
+inductive succ :: "nat \<Rightarrow> nat \<Rightarrow> bool" where
+ "succ 0 1"
+ | "succ m n \<Longrightarrow> succ (Suc m) (Suc n)"
+
+code_pred succ
+ using assms by (rule succ.cases)
+
+thm succ.equation
+
+values 20 "{n. tranclp succ 10 n}"
+values "{n. tranclp succ n 10}"
+values 20 "{(n, m). tranclp succ n m}"
+
end
\ No newline at end of file
--- a/src/HOL/ex/predicate_compile.ML Wed May 20 22:24:07 2009 +0200
+++ b/src/HOL/ex/predicate_compile.ML Wed May 20 22:24:07 2009 +0200
@@ -1,4 +1,4 @@
-(* Author: Lukas Bulwahn
+(* Author: Lukas Bulwahn, TU Muenchen
(Prototype of) A compiler from predicates specified by intro/elim rules
to equations.
@@ -13,14 +13,15 @@
val strip_intro_concl: term -> int -> term * (term list * term list)
val modename_of: theory -> string -> mode -> string
val modes_of: theory -> string -> mode list
+ val pred_intros: theory -> string -> thm list
+ val get_nparams: theory -> string -> int
val setup: theory -> theory
val code_pred: string -> Proof.context -> Proof.state
val code_pred_cmd: string -> Proof.context -> Proof.state
val print_alternative_rules: theory -> theory (*FIXME diagnostic command?*)
val do_proofs: bool ref
- val pred_intros : theory -> string -> thm list
- val get_nparams : theory -> string -> int
- val pred_term_of : theory -> term -> term option
+ val analyze_compr: theory -> term -> term
+ val eval_ref: (unit -> term Predicate.pred) option ref
end;
structure Predicate_Compile : PREDICATE_COMPILE =
@@ -1425,29 +1426,37 @@
(*FIXME
- Naming of auxiliary rules necessary?
+- add default code equations P x y z = P_i_i_i x y z
*)
(* transformation for code generation *)
-fun pred_term_of thy t = let
- val (vars, body) = strip_abs t
- val (pred, all_args) = strip_comb body
- val (name, T) = dest_Const pred
- val (params, args) = chop (get_nparams thy name) all_args
- val user_mode = flat (map_index
- (fn (i, t) => case t of Bound j => if j < length vars then [] else [i+1] | _ => [i+1])
- args)
- val (inargs, _) = get_args user_mode args
- val all_modes = Symtab.dest (#modes (IndCodegenData.get thy))
- val modes = filter (fn Mode (_, is, _) => is = user_mode) (modes_of_term all_modes (list_comb (pred, params)))
- fun compile m = list_comb (compile_expr thy all_modes (SOME m, list_comb (pred, params)), inargs)
- in
- case modes of
- [] => (let val _ = error "No mode possible for this term" in NONE end)
- | [m] => SOME (compile m)
- | ms => (let val _ = warning "Multiple modes possible for this term"
- in SOME (compile (hd ms)) end)
- end;
+val eval_ref = ref (NONE : (unit -> term Predicate.pred) option);
+
+fun analyze_compr thy t_compr =
+ let
+ val split = case t_compr of (Const (@{const_name Collect}, _) $ t) => t
+ | _ => error ("Not a set comprehension: " ^ Syntax.string_of_term_global thy t_compr);
+ val (body, Ts, fp) = HOLogic.strip_split split;
+ (*FIXME former order of tuple positions must be restored*)
+ val (pred as Const (name, T), all_args) = strip_comb body
+ val (params, args) = chop (get_nparams thy name) all_args
+ val user_mode = map_filter I (map_index
+ (fn (i, t) => case t of Bound j => if j < length Ts then NONE
+ else SOME (i+1) | _ => SOME (i+1)) args) (*FIXME dangling bounds should not occur*)
+ val (inargs, _) = get_args user_mode args;
+ val all_modes = Symtab.dest (#modes (IndCodegenData.get thy));
+ val modes = filter (fn Mode (_, is, _) => is = user_mode)
+ (modes_of_term all_modes (list_comb (pred, params)));
+ val m = case modes
+ of [] => error ("No mode possible for comprehension "
+ ^ Syntax.string_of_term_global thy t_compr)
+ | [m] => m
+ | m :: _ :: _ => (warning ("Multiple modes possible for comprehension "
+ ^ Syntax.string_of_term_global thy t_compr); m);
+ val t_eval = list_comb (compile_expr thy all_modes (SOME m, list_comb (pred, params)),
+ inargs)
+ in t_eval end;
end;