--- a/src/HOL/Code_Eval.thy Thu Jul 30 23:50:11 2009 +0200
+++ b/src/HOL/Code_Eval.thy Fri Jul 31 09:34:21 2009 +0200
@@ -39,6 +39,17 @@
subsubsection {* @{text term_of} instances *}
+instantiation "fun" :: (typerep, typerep) term_of
+begin
+
+definition
+ "term_of (f \<Colon> 'a \<Rightarrow> 'b) = Const (STR ''dummy_pattern'') (Typerep.Typerep (STR ''fun'')
+ [Typerep.typerep TYPE('a), Typerep.typerep TYPE('b)])"
+
+instance ..
+
+end
+
setup {*
let
fun add_term_of tyco raw_vs thy =
--- a/src/HOL/Tools/hologic.ML Thu Jul 30 23:50:11 2009 +0200
+++ b/src/HOL/Tools/hologic.ML Fri Jul 31 09:34:21 2009 +0200
@@ -67,14 +67,18 @@
val split_const: typ * typ * typ -> term
val mk_split: term -> term
val flatten_tupleT: typ -> typ list
- val mk_tupleT: int list list -> typ list -> typ
- val strip_tupleT: int list list -> typ -> typ list
+ val mk_tupleT: typ list -> typ
+ val strip_tupleT: typ -> typ list
+ val mk_tuple: term list -> term
+ val strip_tuple: term -> term list
+ val mk_ptupleT: int list list -> typ list -> typ
+ val strip_ptupleT: int list list -> typ -> typ list
val flat_tupleT_paths: typ -> int list list
- val mk_tuple: int list list -> typ -> term list -> term
- val dest_tuple: int list list -> term -> term list
+ val mk_ptuple: int list list -> typ -> term list -> term
+ val strip_ptuple: int list list -> term -> term list
val flat_tuple_paths: term -> int list list
- val mk_splits: int list list -> typ -> typ -> term -> term
- val strip_splits: term -> term * typ list * int list list
+ val mk_psplits: int list list -> typ -> typ -> term -> term
+ val strip_psplits: term -> term * typ list * int list list
val natT: typ
val zero: term
val is_zero: term -> bool
@@ -118,6 +122,8 @@
val mk_literal: string -> term
val dest_literal: term -> string
val mk_typerep: typ -> term
+ val termT: typ
+ val term_of_const: typ -> term
val mk_term_of: typ -> term -> term
val reflect_term: term -> term
val mk_valtermify_app: string -> (string * typ) list -> typ -> term
@@ -321,15 +327,33 @@
fun flatten_tupleT (Type ("*", [T1, T2])) = flatten_tupleT T1 @ flatten_tupleT T2
| flatten_tupleT T = [T];
+
+(* tuples with right-fold structure *)
+
+fun mk_tupleT [] = unitT
+ | mk_tupleT Ts = foldr1 mk_prodT Ts;
+
+fun strip_tupleT (Type ("Product_Type.unit", [])) = []
+ | strip_tupleT (Type ("*", [T1, T2])) = T1 :: strip_tupleT T2
+ | strip_tupleT T = [T];
+
+fun mk_tuple [] = unit
+ | mk_tuple ts = foldr1 mk_prod ts;
+
+fun strip_tuple (Const ("Product_Type.Unity", _)) = []
+ | strip_tuple (Const ("Pair", _) $ t1 $ t2) = t1 :: strip_tuple t2
+ | strip_tuple t = [t];
+
+
(* tuples with specific arities
- an "arity" of a tuple is a list of lists of integers
- ("factors"), denoting paths to subterms that are pairs
+ an "arity" of a tuple is a list of lists of integers,
+ denoting paths to subterms that are pairs
*)
-fun prod_err s = raise TERM (s ^ ": inconsistent use of products", []);
+fun ptuple_err s = raise TERM (s ^ ": inconsistent use of nested products", []);
-fun mk_tupleT ps =
+fun mk_ptupleT ps =
let
fun mk p Ts =
if p mem ps then
@@ -340,12 +364,12 @@
else (hd Ts, tl Ts)
in fst o mk [] end;
-fun strip_tupleT ps =
+fun strip_ptupleT ps =
let
fun factors p T = if p mem ps then (case T of
Type ("*", [T1, T2]) =>
factors (1::p) T1 @ factors (2::p) T2
- | _ => prod_err "strip_tupleT") else [T]
+ | _ => ptuple_err "strip_ptupleT") else [T]
in factors [] end;
val flat_tupleT_paths =
@@ -355,7 +379,7 @@
| factors p _ = []
in factors [] end;
-fun mk_tuple ps =
+fun mk_ptuple ps =
let
fun mk p T ts =
if p mem ps then (case T of
@@ -364,16 +388,16 @@
val (t, ts') = mk (1::p) T1 ts;
val (u, ts'') = mk (2::p) T2 ts'
in (pair_const T1 T2 $ t $ u, ts'') end
- | _ => prod_err "mk_tuple")
+ | _ => ptuple_err "mk_ptuple")
else (hd ts, tl ts)
in fst oo mk [] end;
-fun dest_tuple ps =
+fun strip_ptuple ps =
let
fun dest p t = if p mem ps then (case t of
Const ("Pair", _) $ t $ u =>
dest (1::p) t @ dest (2::p) u
- | _ => prod_err "dest_tuple") else [t]
+ | _ => ptuple_err "strip_ptuple") else [t]
in dest [] end;
val flat_tuple_paths =
@@ -383,24 +407,24 @@
| factors p _ = []
in factors [] end;
-(*In mk_splits ps S T u, term u expects separate arguments for the factors of S,
+(*In mk_psplits ps S T u, term u expects separate arguments for the factors of S,
with result type T. The call creates a new term expecting one argument
of type S.*)
-fun mk_splits ps T T3 u =
+fun mk_psplits ps T T3 u =
let
fun ap ((p, T) :: pTs) =
if p mem ps then (case T of
Type ("*", [T1, T2]) =>
split_const (T1, T2, map snd pTs ---> T3) $
ap ((1::p, T1) :: (2::p, T2) :: pTs)
- | _ => prod_err "mk_splits")
+ | _ => ptuple_err "mk_psplits")
else Abs ("x", T, ap pTs)
| ap [] =
let val k = length ps
in list_comb (incr_boundvars (k + 1) u, map Bound (k downto 0)) end
in ap [([], T)] end;
-val strip_splits =
+val strip_psplits =
let
fun strip [] qs Ts t = (t, Ts, qs)
| strip (p :: ps) qs Ts (Const ("split", _) $ t) =
@@ -591,7 +615,9 @@
val termT = Type ("Code_Eval.term", []);
-fun mk_term_of T t = Const ("Code_Eval.term_of_class.term_of", T --> termT) $ t;
+fun term_of_const T = Const ("Code_Eval.term_of_class.term_of", T --> termT);
+
+fun mk_term_of T t = term_of_const T $ t;
fun reflect_term (Const (c, T)) =
Const ("Code_Eval.Const", literalT --> typerepT --> termT)
--- a/src/HOL/Tools/inductive_codegen.ML Thu Jul 30 23:50:11 2009 +0200
+++ b/src/HOL/Tools/inductive_codegen.ML Fri Jul 31 09:34:21 2009 +0200
@@ -645,7 +645,7 @@
fun inductive_codegen thy defs dep module brack t gr = (case strip_comb t of
(Const ("Collect", _), [u]) =>
- let val (r, Ts, fs) = HOLogic.strip_splits u
+ let val (r, Ts, fs) = HOLogic.strip_psplits u
in case strip_comb r of
(Const (s, T), ts) =>
(case (get_clauses thy s, get_assoc_code thy (s, T)) of
--- a/src/HOL/Tools/inductive_set.ML Thu Jul 30 23:50:11 2009 +0200
+++ b/src/HOL/Tools/inductive_set.ML Fri Jul 31 09:34:21 2009 +0200
@@ -33,10 +33,10 @@
val collect_mem_simproc =
Simplifier.simproc (theory "Set") "Collect_mem" ["Collect t"] (fn thy => fn ss =>
fn S as Const ("Collect", Type ("fun", [_, T])) $ t =>
- let val (u, Ts, ps) = HOLogic.strip_splits t
+ let val (u, Ts, ps) = HOLogic.strip_psplits t
in case u of
(c as Const ("op :", _)) $ q $ S' =>
- (case try (HOLogic.dest_tuple ps) q of
+ (case try (HOLogic.strip_ptuple ps) q of
NONE => NONE
| SOME ts =>
if not (loose_bvar (S', 0)) andalso
@@ -79,7 +79,7 @@
fun mk_collect p T t =
let val U = HOLogic.dest_setT T
in HOLogic.Collect_const U $
- HOLogic.mk_splits (HOLogic.flat_tuple_paths p) U HOLogic.boolT t
+ HOLogic.mk_psplits (HOLogic.flat_tuple_paths p) U HOLogic.boolT t
end;
fun decomp (Const (s, _) $ ((m as Const ("op :",
Type (_, [_, Type (_, [T, _])]))) $ p $ S) $ u) =
@@ -223,11 +223,11 @@
map (fn (x, ps) =>
let
val U = HOLogic.dest_setT (fastype_of x);
- val x' = map_type (K (HOLogic.strip_tupleT ps U ---> HOLogic.boolT)) x
+ val x' = map_type (K (HOLogic.strip_ptupleT ps U ---> HOLogic.boolT)) x
in
(cterm_of thy x,
cterm_of thy (HOLogic.Collect_const U $
- HOLogic.mk_splits ps U HOLogic.boolT x'))
+ HOLogic.mk_psplits ps U HOLogic.boolT x'))
end) fs;
fun mk_to_pred_eq p fs optfs' T thm =
@@ -240,7 +240,7 @@
| SOME fs' =>
let
val (_, U) = split_last (binder_types T);
- val Ts = HOLogic.strip_tupleT fs' U;
+ val Ts = HOLogic.strip_ptupleT fs' U;
(* FIXME: should cterm_instantiate increment indexes? *)
val arg_cong' = Thm.incr_indexes (Thm.maxidx_of thm + 1) arg_cong;
val (arg_cong_f, _) = arg_cong' |> cprop_of |> Drule.strip_imp_concl |>
@@ -248,7 +248,7 @@
in
thm' RS (Drule.cterm_instantiate [(arg_cong_f,
cterm_of thy (Abs ("P", Ts ---> HOLogic.boolT,
- HOLogic.Collect_const U $ HOLogic.mk_splits fs' U
+ HOLogic.Collect_const U $ HOLogic.mk_psplits fs' U
HOLogic.boolT (Bound 0))))] arg_cong' RS sym)
end)
in
@@ -361,12 +361,12 @@
val insts = map (fn (x, ps) =>
let
val Ts = binder_types (fastype_of x);
- val T = HOLogic.mk_tupleT ps Ts;
+ val T = HOLogic.mk_ptupleT ps Ts;
val x' = map_type (K (HOLogic.mk_setT T)) x
in
(cterm_of thy x,
cterm_of thy (list_abs (map (pair "x") Ts, HOLogic.mk_mem
- (HOLogic.mk_tuple ps T (map Bound (length ps downto 0)), x'))))
+ (HOLogic.mk_ptuple ps T (map Bound (length ps downto 0)), x'))))
end) fs
in
thm |>
@@ -422,14 +422,14 @@
SOME fs =>
let
val T = HOLogic.dest_setT (fastype_of x);
- val Ts = HOLogic.strip_tupleT fs T;
+ val Ts = HOLogic.strip_ptupleT fs T;
val x' = map_type (K (Ts ---> HOLogic.boolT)) x
in
(x, (x',
(HOLogic.Collect_const T $
- HOLogic.mk_splits fs T HOLogic.boolT x',
+ HOLogic.mk_psplits fs T HOLogic.boolT x',
list_abs (map (pair "x") Ts, HOLogic.mk_mem
- (HOLogic.mk_tuple fs T (map Bound (length fs downto 0)),
+ (HOLogic.mk_ptuple fs T (map Bound (length fs downto 0)),
x)))))
end
| NONE => (x, (x, (x, x))))) params;
@@ -448,13 +448,13 @@
Pretty.str ("of " ^ s ^ " do not agree with types"),
Pretty.block (Pretty.commas (map (Syntax.pretty_typ ctxt) paramTs)),
Pretty.str "of declared parameters"]));
- val Ts = HOLogic.strip_tupleT fs U;
+ val Ts = HOLogic.strip_ptupleT fs U;
val c' = Free (s ^ "p",
map fastype_of params1 @ Ts ---> HOLogic.boolT)
in
((c', (fs, U, Ts)),
(list_comb (c, params2),
- HOLogic.Collect_const U $ HOLogic.mk_splits fs U HOLogic.boolT
+ HOLogic.Collect_const U $ HOLogic.mk_psplits fs U HOLogic.boolT
(list_comb (c', params1))))
end) |> split_list |>> split_list;
val eqns' = eqns @
@@ -484,7 +484,7 @@
val (defs, ctxt2) = fold_map (LocalTheory.define Thm.internalK)
(map (fn ((c_syn, (fs, U, _)), p) => (c_syn, (Attrib.empty_binding,
fold_rev lambda params (HOLogic.Collect_const U $
- HOLogic.mk_splits fs U HOLogic.boolT (list_comb (p, params3))))))
+ HOLogic.mk_psplits fs U HOLogic.boolT (list_comb (p, params3))))))
(cnames_syn ~~ cs_info ~~ preds)) ctxt1;
(* prove theorems for converting predicate to set notation *)
@@ -495,7 +495,7 @@
(HOLogic.mk_Trueprop (HOLogic.mk_eq
(list_comb (p, params3),
list_abs (map (pair "x") Ts, HOLogic.mk_mem
- (HOLogic.mk_tuple fs U (map Bound (length fs downto 0)),
+ (HOLogic.mk_ptuple fs U (map Bound (length fs downto 0)),
list_comb (c, params))))))
(K (REPEAT (rtac ext 1) THEN simp_tac (HOL_basic_ss addsimps
[def, mem_Collect_eq, split_conv]) 1))
--- a/src/HOL/Tools/quickcheck_generators.ML Thu Jul 30 23:50:11 2009 +0200
+++ b/src/HOL/Tools/quickcheck_generators.ML Fri Jul 31 09:34:21 2009 +0200
@@ -40,9 +40,10 @@
let
val fun_upd = Const (@{const_name fun_upd},
(T1 --> T2) --> T1 --> T2 --> T1 --> T2);
- val (seed', seed'') = random_split seed;
+ val ((y, t2), seed') = random seed;
+ val (seed'', seed''') = random_split seed';
- val state = ref (seed', [], fn () => Const (@{const_name undefined}, T1 --> T2));
+ val state = ref (seed'', [], fn () => Abs ("x", T1, t2 ()));
fun random_fun' x =
let
val (seed, fun_map, f_t) = ! state;
@@ -57,7 +58,7 @@
in y end
end;
fun term_fun' () = #3 (! state) ();
- in ((random_fun', term_fun'), seed'') end;
+ in ((random_fun', term_fun'), seed''') end;
(** type copies **)
--- a/src/HOL/Tools/recfun_codegen.ML Thu Jul 30 23:50:11 2009 +0200
+++ b/src/HOL/Tools/recfun_codegen.ML Fri Jul 31 09:34:21 2009 +0200
@@ -47,7 +47,7 @@
val thms = Code.these_eqns thy c'
|> map_filter (fn (thm, linear) => if linear then SOME thm else NONE)
|> expand_eta thy
- |> Code.norm_varnames thy
+ |> Code.desymbolize_all_vars thy
|> map (rpair opt_name)
in if null thms then NONE else SOME thms end;
--- a/src/HOL/Tools/split_rule.ML Thu Jul 30 23:50:11 2009 +0200
+++ b/src/HOL/Tools/split_rule.ML Fri Jul 31 09:34:21 2009 +0200
@@ -81,7 +81,7 @@
let
val Ts = HOLogic.flatten_tupleT T;
val ys = Name.variant_list xs (replicate (length Ts) a);
- in (xs @ ys, (cterm v, cterm (HOLogic.mk_tuple (HOLogic.flat_tupleT_paths T) T
+ in (xs @ ys, (cterm v, cterm (HOLogic.mk_ptuple (HOLogic.flat_tupleT_paths T) T
(map (Var o apfst (rpair 0)) (ys ~~ Ts))))::insts)
end
| mk_tuple _ x = x;
--- a/src/HOL/ex/Predicate_Compile.thy Thu Jul 30 23:50:11 2009 +0200
+++ b/src/HOL/ex/Predicate_Compile.thy Fri Jul 31 09:34:21 2009 +0200
@@ -1,61 +1,8 @@
theory Predicate_Compile
-imports Complex_Main Lattice_Syntax Code_Eval
+imports Complex_Main
uses "predicate_compile.ML"
begin
-text {* Package setup *}
-
setup {* Predicate_Compile.setup *}
-text {* Experimental code *}
-
-ML {*
-structure Predicate_Compile =
-struct
-
-open Predicate_Compile;
-
-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) Predicate.map thy t' []) end;
-
-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 values_cmd modes k raw_t state =
- let
- 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;
-*}
-
end
\ No newline at end of file
--- a/src/HOL/ex/Predicate_Compile_ex.thy Thu Jul 30 23:50:11 2009 +0200
+++ b/src/HOL/ex/Predicate_Compile_ex.thy Fri Jul 31 09:34:21 2009 +0200
@@ -17,17 +17,11 @@
values 10 "{n. even n}"
values 10 "{n. odd n}"
-
inductive append :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list \<Rightarrow> bool" where
- append_Nil: "append [] xs xs"
- | append_Cons: "append xs ys zs \<Longrightarrow> append (x # xs) ys (x # zs)"
+ "append [] xs xs"
+ | "append xs ys zs \<Longrightarrow> append (x # xs) ys (x # zs)"
-inductive rev
-where
-"rev [] []"
-| "rev xs xs' ==> append xs' [x] ys ==> rev (x#xs) ys"
-
-code_pred rev .
+code_pred append .
thm append.equation
@@ -35,6 +29,16 @@
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 rev where
+ "rev [] []"
+ | "rev xs xs' ==> append xs' [x] ys ==> rev (x#xs) ys"
+
+code_pred rev .
+
+thm rev.equation
+
+values "{xs. rev [0, 1, 2, 3::nat] xs}"
+values "Collect (rev [0, 1, 2, 3::nat])"
inductive partition :: "('a \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> 'a list \<Rightarrow> 'a list \<Rightarrow> bool"
for f where
@@ -57,9 +61,9 @@
lemma [code_pred_intros]:
-"r a b ==> tranclp r a b"
-"r a b ==> tranclp r b c ==> tranclp r a c"
-by auto
+ "r a b \<Longrightarrow> tranclp r a b"
+ "r a b \<Longrightarrow> tranclp r b c \<Longrightarrow> tranclp r a c"
+ by auto
(* Setup requires quick and dirty proof *)
(*
@@ -71,6 +75,7 @@
thm tranclp.equation
*)
+
inductive succ :: "nat \<Rightarrow> nat \<Rightarrow> bool" where
"succ 0 1"
| "succ m n \<Longrightarrow> succ (Suc m) (Suc n)"
@@ -78,6 +83,11 @@
code_pred succ .
thm succ.equation
+
+values 10 "{(m, n). succ n m}"
+values "{m. succ 0 m}"
+values "{m. succ m 0}"
+
(* FIXME: why does this not terminate? *)
(*
values 20 "{n. tranclp succ 10 n}"
--- a/src/HOL/ex/predicate_compile.ML Thu Jul 30 23:50:11 2009 +0200
+++ b/src/HOL/ex/predicate_compile.ML Fri Jul 31 09:34:21 2009 +0200
@@ -68,23 +68,9 @@
HOLogic.mk_eq (Free (a, fastype_of b), b) :: mk_eqs a cs
in mk_eqs x xs end;
-fun mk_tupleT [] = HOLogic.unitT
- | mk_tupleT Ts = foldr1 HOLogic.mk_prodT Ts;
-
-fun dest_tupleT (Type (@{type_name Product_Type.unit}, [])) = []
- | dest_tupleT (Type (@{type_name "*"}, [T1, T2])) = T1 :: (dest_tupleT T2)
- | dest_tupleT t = [t]
+fun mk_pred_enumT T = Type (@{type_name Predicate.pred}, [T])
-fun mk_tuple [] = HOLogic.unit
- | mk_tuple ts = foldr1 HOLogic.mk_prod ts;
-
-fun dest_tuple (Const (@{const_name Product_Type.Unity}, _)) = []
- | dest_tuple (Const (@{const_name Pair}, _) $ t1 $ t2) = t1 :: (dest_tuple t2)
- | dest_tuple t = [t]
-
-fun mk_pred_enumT T = Type (@{type_name "Predicate.pred"}, [T])
-
-fun dest_pred_enumT (Type (@{type_name "Predicate.pred"}, [T])) = T
+fun dest_pred_enumT (Type (@{type_name Predicate.pred}, [T])) = T
| dest_pred_enumT T = raise TYPE ("dest_pred_enumT", [T], []);
fun mk_Enum f =
@@ -119,6 +105,10 @@
fun mk_not_pred t = let val T = mk_pred_enumT HOLogic.unitT
in Const (@{const_name Predicate.not_pred}, T --> T) $ t end
+fun mk_pred_map T1 T2 tf tp = Const (@{const_name Predicate.map},
+ (T1 --> T2) --> mk_pred_enumT T1 --> mk_pred_enumT T2) $ tf $ tp;
+
+
(* destruction of intro rules *)
(* FIXME: look for other place where this functionality was used before *)
@@ -383,7 +373,7 @@
fun get_args is ts = let
fun get_args' _ _ [] = ([], [])
- | get_args' is i (t::ts) = (if i mem is then apfst else apsnd) (cons t)
+ | get_args' is i (t::ts) = (if member (op =) is i then apfst else apsnd) (cons t)
(get_args' is (i+1) ts)
in get_args' is 1 ts end
@@ -553,7 +543,7 @@
| funT_of T (SOME mode) = let
val Ts = binder_types T;
val (Us1, Us2) = get_args mode Ts
- in Us1 ---> (mk_pred_enumT (mk_tupleT Us2)) end;
+ in Us1 ---> (mk_pred_enumT (HOLogic.mk_tupleT Us2)) end;
fun funT'_of (iss, is) T = let
val Ts = binder_types T
@@ -561,7 +551,7 @@
val paramTs' = map2 (fn SOME is => funT'_of ([], is) | NONE => I) iss paramTs
val (inargTs, outargTs) = get_args is argTs
in
- (paramTs' @ inargTs) ---> (mk_pred_enumT (mk_tupleT outargTs))
+ (paramTs' @ inargTs) ---> (mk_pred_enumT (HOLogic.mk_tupleT outargTs))
end;
@@ -589,7 +579,7 @@
val names = fold Term.add_free_names (success_t :: eqs'' @ out_ts) [];
val name = Name.variant names "x";
val name' = Name.variant (name :: names) "y";
- val T = mk_tupleT (map fastype_of out_ts);
+ val T = HOLogic.mk_tupleT (map fastype_of out_ts);
val U = fastype_of success_t;
val U' = dest_pred_enumT U;
val v = Free (name, T);
@@ -597,7 +587,7 @@
in
lambda v (fst (Datatype.make_case
(ProofContext.init thy) false [] v
- [(mk_tuple out_ts,
+ [(HOLogic.mk_tuple out_ts,
if null eqs'' then success_t
else Const (@{const_name HOL.If}, HOLogic.boolT --> U --> U --> U) $
foldr1 HOLogic.mk_conj eqs'' $ success_t $
@@ -605,19 +595,6 @@
(v', mk_empty U')]))
end;
-(*FIXME function can be removed*)
-fun mk_funcomp f t =
- let
- val names = Term.add_free_names t [];
- val Ts = binder_types (fastype_of t);
- val vs = map Free
- (Name.variant_list names (replicate (length Ts) "x") ~~ Ts)
- in
- fold_rev lambda vs (f (list_comb (t, vs)))
- end;
-
-
-
fun compile_param_ext thy modes (NONE, t) = t
| compile_param_ext thy modes (m as SOME (Mode ((iss, is'), is, ms)), t) =
let
@@ -639,11 +616,11 @@
Const (predfun_name_of thy name (iss, is'), funT'_of (iss, is') T)
else error "compile param: Not an inductive predicate with correct mode"
| Free (name, T) => Free (name, funT_of T (SOME is'))
- val outTs = dest_tupleT (dest_pred_enumT (body_type (fastype_of f')))
+ val outTs = HOLogic.strip_tupleT (dest_pred_enumT (body_type (fastype_of f')))
val out_vs = map Free (out_names ~~ outTs)
val params' = map (compile_param thy modes) (ms ~~ params)
val f_app = list_comb (f', params' @ inargs)
- val single_t = (mk_single (mk_tuple (map (fn i => nth out_vs (i - 1)) outp_perm)))
+ val single_t = (mk_single (HOLogic.mk_tuple (map (fn i => nth out_vs (i - 1)) outp_perm)))
val match_t = compile_match thy [] [] out_vs single_t
in list_abs (ivs,
mk_bind (f_app, match_t))
@@ -678,7 +655,7 @@
(curry Library.drop (length ms) (fst (strip_type T)))
val params' = map (compile_param thy modes) (ms ~~ params)
in list_comb (Const (predfun_name_of thy name mode, ((map fastype_of params') @ Ts) --->
- mk_pred_enumT (mk_tupleT Us)), params')
+ mk_pred_enumT (HOLogic.mk_tupleT Us)), params')
end
else error "not a valid inductive expression"
| (Free (name, T), args) =>
@@ -713,7 +690,7 @@
out_ts'' (names', map (rpair []) vs);
in
compile_match thy constr_vs (eqs @ eqs') out_ts'''
- (mk_single (mk_tuple out_ts))
+ (mk_single (HOLogic.mk_tuple out_ts))
end
| compile_prems out_ts vs names ps =
let
@@ -768,12 +745,12 @@
val xs = map2 (fn s => fn T => Free (s, T)) xnames Us1;
val cl_ts =
map (fn cl => compile_clause thy
- all_vs param_vs modes mode cl (mk_tuple xs)) cls;
+ all_vs param_vs modes mode cl (HOLogic.mk_tuple xs)) cls;
val mode_id = predfun_name_of thy s mode
in
HOLogic.mk_Trueprop (HOLogic.mk_eq
(list_comb (Const (mode_id, (Ts1' @ Us1) --->
- mk_pred_enumT (mk_tupleT Us2)),
+ mk_pred_enumT (HOLogic.mk_tupleT Us2)),
map2 (fn s => fn T => Free (s, T)) param_vs Ts1' @ xs),
foldr1 mk_sup cl_ts))
end;
@@ -804,7 +781,7 @@
(map (fn i => "x" ^ string_of_int i) (1 upto (length Ts)));
val args = map Free (argnames ~~ Ts)
val (inargs, outargs) = get_args mode args
- val r = mk_Eval (list_comb (x, inargs), mk_tuple outargs)
+ val r = mk_Eval (list_comb (x, inargs), HOLogic.mk_tuple outargs)
val t = fold_rev lambda args r
in
(t, argnames @ names)
@@ -830,9 +807,9 @@
val param_eqs = map (HOLogic.mk_Trueprop o HOLogic.mk_eq) (param_vs ~~ params')
val funargs = params @ inargs
val funpropE = HOLogic.mk_Trueprop (mk_Eval (list_comb (funtrm, funargs),
- if null outargs then Free("y", HOLogic.unitT) else mk_tuple outargs))
+ if null outargs then Free("y", HOLogic.unitT) else HOLogic.mk_tuple outargs))
val funpropI = HOLogic.mk_Trueprop (mk_Eval (list_comb (funtrm, funargs),
- mk_tuple outargs))
+ HOLogic.mk_tuple outargs))
val introtrm = Logic.list_implies (predpropI :: param_eqs, funpropI)
val _ = Output.tracing (Syntax.string_of_term_global thy introtrm)
val simprules = [defthm, @{thm eval_pred},
@@ -875,7 +852,7 @@
| mk_split_lambda' (x::xs) t = HOLogic.mk_split (lambda x (mk_split_lambda' xs t))
in mk_split_lambda' xs t end;
val predterm = mk_Enum (mk_split_lambda xouts (list_comb (Const (name, T), xparams' @ xargs)))
- val funT = (Ts1' @ Us1) ---> (mk_pred_enumT (mk_tupleT Us2))
+ val funT = (Ts1' @ Us1) ---> (mk_pred_enumT (HOLogic.mk_tupleT Us2))
val mode_id = Sign.full_bname thy (Long_Name.base_name mode_id)
val lhs = list_comb (Const (mode_id, funT), xparams @ xins)
val def = Logic.mk_equals (lhs, predterm)
@@ -1137,7 +1114,7 @@
end
else all_tac
in
- split_term_tac (mk_tuple out_ts)
+ split_term_tac (HOLogic.mk_tuple out_ts)
THEN (DETERM (TRY ((Splitter.split_asm_tac [@{thm "split_if_asm"}] 1) THEN (etac @{thm botE} 2))))
end
@@ -1527,18 +1504,17 @@
val eval_ref = ref (NONE : (unit -> term Predicate.pred) option);
+(*FIXME turn this into an LCF-guarded preprocessor for comprehensions*)
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_splits 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 (nparams_of thy name) all_args
+ val (body, Ts, fp) = HOLogic.strip_psplits split;
+ val (pred as Const (name, T), all_args) = strip_comb body;
+ val (params, args) = chop (nparams_of 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;
+ else SOME (i+1) | _ => SOME (i+1)) args); (*FIXME dangling bounds should not occur*)
val modes = filter (fn Mode (_, is, _) => is = user_mode)
(modes_of_term (all_modes_of thy) (list_comb (pred, params)));
val m = case modes
@@ -1547,9 +1523,63 @@
| [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_of thy) (SOME m, list_comb (pred, params)),
- inargs)
+ val (inargs, outargs) = get_args user_mode args;
+ val t_pred = list_comb (compile_expr thy (all_modes_of thy) (SOME m, list_comb (pred, params)),
+ inargs);
+ val t_eval = if null outargs then t_pred else let
+ val outargs_bounds = map (fn Bound i => i) outargs;
+ val outargsTs = map (nth Ts) outargs_bounds;
+ val T_pred = HOLogic.mk_tupleT outargsTs;
+ val T_compr = HOLogic.mk_ptupleT fp Ts;
+ val arrange_bounds = map_index I outargs_bounds
+ |> sort (prod_ord (K EQUAL) int_ord)
+ |> map fst;
+ val arrange = funpow (length outargs_bounds - 1) HOLogic.mk_split
+ (Term.list_abs (map (pair "") outargsTs,
+ HOLogic.mk_ptuple fp T_compr (map Bound arrange_bounds)))
+ in mk_pred_map T_pred T_compr arrange t_pred end
in t_eval end;
+fun eval thy t_compr =
+ let
+ val t = analyze_compr thy t_compr;
+ val T = dest_pred_enumT (fastype_of t);
+ val t' = mk_pred_map T HOLogic.termT (HOLogic.term_of_const T) t;
+ in (T, Code_ML.eval NONE ("Predicate_Compile.eval_ref", eval_ref) Predicate.map thy t' []) end;
+
+fun values ctxt k t_compr =
+ let
+ val thy = ProofContext.theory_of ctxt;
+ val (T, t) = eval thy t_compr;
+ val setT = HOLogic.mk_setT T;
+ val (ts, _) = Predicate.yieldn k t;
+ val elemsT = HOLogic.mk_set T ts;
+ in if k = ~1 orelse length ts < k then elemsT
+ else Const (@{const_name Set.union}, setT --> setT --> setT) $ elemsT $ t_compr
+ end;
+
+fun values_cmd modes k raw_t state =
+ let
+ 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;
+
+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
+ (values_cmd modes k t)));
+
end;
+end;
+
--- a/src/Pure/Isar/code.ML Thu Jul 30 23:50:11 2009 +0200
+++ b/src/Pure/Isar/code.ML Fri Jul 31 09:34:21 2009 +0200
@@ -34,8 +34,7 @@
val const_typ_eqn: theory -> thm -> string * typ
val typscheme_eqn: theory -> thm -> (string * sort) list * typ
val expand_eta: theory -> int -> thm -> thm
- val norm_args: theory -> thm list -> thm list
- val norm_varnames: theory -> thm list -> thm list
+ val desymbolize_all_vars: theory -> thm list -> thm list
(*executable code*)
val add_datatype: (string * typ) list -> theory -> theory
@@ -135,104 +134,41 @@
val l = if k = ~1
then (length o fst o strip_abs) rhs
else Int.max (0, k - length args);
- val used = Name.make_context (map (fst o fst) (Term.add_vars lhs []));
- fun get_name _ 0 = pair []
- | get_name (Abs (v, ty, t)) k =
- Name.variants [v]
- ##>> get_name t (k - 1)
- #>> (fn ([v'], vs') => (v', ty) :: vs')
- | get_name t k =
- let
- val (tys, _) = (strip_type o fastype_of) t
- in case tys
- of [] => raise TERM ("expand_eta", [t])
- | ty :: _ =>
- Name.variants [""]
- #-> (fn [v] => get_name (t $ Var ((v, 0), ty)) (k - 1)
- #>> (fn vs' => (v, ty) :: vs'))
- end;
- val (vs, _) = get_name rhs l used;
+ val (raw_vars, _) = Term.strip_abs_eta l rhs;
+ val vars = burrow_fst (Name.variant_list (map (fst o fst) (Term.add_vars lhs [])))
+ raw_vars;
fun expand (v, ty) thm = Drule.fun_cong_rule thm
(Thm.cterm_of thy (Var ((v, 0), ty)));
in
thm
- |> fold expand vs
+ |> fold expand vars
|> Conv.fconv_rule Drule.beta_eta_conversion
end;
-fun norm_args thy thms =
- let
- val num_args_of = length o snd o strip_comb o fst o Logic.dest_equals;
- val k = fold (curry Int.max o num_args_of o Thm.prop_of) thms 0;
- in
- thms
- |> map (expand_eta thy k)
- |> map (Conv.fconv_rule Drule.beta_eta_conversion)
- end;
-
-fun canonical_tvars thy thm =
- let
- val ctyp = Thm.ctyp_of thy;
- val purify_tvar = unprefix "'" #> Name.desymbolize false #> prefix "'";
- fun tvars_subst_for thm = (fold_types o fold_atyps)
- (fn TVar (v_i as (v, _), sort) => let
- val v' = purify_tvar v
- in if v = v' then I
- else insert (op =) (v_i, (v', sort)) end
- | _ => I) (prop_of thm) [];
- fun mk_inst (v_i, (v', sort)) (maxidx, acc) =
- let
- val ty = TVar (v_i, sort)
- in
- (maxidx + 1, (ctyp ty, ctyp (TVar ((v', maxidx), sort))) :: acc)
- end;
- val maxidx = Thm.maxidx_of thm + 1;
- val (_, inst) = fold mk_inst (tvars_subst_for thm) (maxidx + 1, []);
- in Thm.instantiate (inst, []) thm end;
-
-fun canonical_vars thy thm =
+fun mk_desymbolization pre post cert vs =
let
- val cterm = Thm.cterm_of thy;
- val purify_var = Name.desymbolize false;
- fun vars_subst_for thm = fold_aterms
- (fn Var (v_i as (v, _), ty) => let
- val v' = purify_var v
- in if v = v' then I
- else insert (op =) (v_i, (v', ty)) end
- | _ => I) (prop_of thm) [];
- fun mk_inst (v_i as (v, i), (v', ty)) (maxidx, acc) =
- let
- val t = Var (v_i, ty)
- in
- (maxidx + 1, (cterm t, cterm (Var ((v', maxidx), ty))) :: acc)
- end;
- val maxidx = Thm.maxidx_of thm + 1;
- val (_, inst) = fold mk_inst (vars_subst_for thm) (maxidx + 1, []);
- in Thm.instantiate ([], inst) thm end;
+ val names = map (pre o fst o fst) vs
+ |> map (Name.desymbolize false)
+ |> Name.variant_list []
+ |> map post;
+ val subst_map = map_filter (fn (((v, i), x), v') =>
+ if v = v' andalso i = 0 then NONE
+ else SOME (((v, i), x), ((v', 0), x))) (vs ~~ names);
+ in (map o pairself) cert subst_map end;
-fun canonical_absvars thm =
+fun desymbolize_tvars thy thms =
let
- val t = Thm.plain_prop_of thm;
- val purify_var = Name.desymbolize false;
- val t' = Term.map_abs_vars purify_var t;
- in Thm.rename_boundvars t t' thm end;
+ val tvs = fold (Term.add_tvars o Thm.prop_of) thms [];
+ val tvar_subst = mk_desymbolization (unprefix "'") (prefix "'") (Thm.ctyp_of thy o TVar) tvs;
+ in map (Thm.instantiate (tvar_subst, [])) thms end;
-fun norm_varnames thy thms =
+fun desymbolize_vars thy thm =
let
- fun burrow_thms f [] = []
- | burrow_thms f thms =
- thms
- |> Conjunction.intr_balanced
- |> f
- |> Conjunction.elim_balanced (length thms)
- in
- thms
- |> map (canonical_vars thy)
- |> map canonical_absvars
- |> map Drule.zero_var_indexes
- |> burrow_thms (canonical_tvars thy)
- |> Drule.zero_var_indexes_list
- end;
+ val vs = Term.add_vars (Thm.prop_of thm) [];
+ val var_subst = mk_desymbolization I I (Thm.cterm_of thy o Var) vs;
+ in Thm.instantiate ([], var_subst) thm end;
+
+fun desymbolize_all_vars thy = desymbolize_tvars thy #> map (desymbolize_vars thy);
(** data store **)
--- a/src/Pure/Isar/overloading.ML Thu Jul 30 23:50:11 2009 +0200
+++ b/src/Pure/Isar/overloading.ML Fri Jul 31 09:34:21 2009 +0200
@@ -132,36 +132,42 @@
|> get_first (fn ((c, _), (v, checked)) =>
if Binding.name_of b = v then SOME (c, checked) else NONE);
-fun confirm b = map_overloading (filter_out (fn (_, (c', _)) => c' = Binding.name_of b));
+
+(* target *)
+fun synchronize_syntax ctxt =
+ let
+ val overloading = OverloadingData.get ctxt;
+ fun subst (c, ty) = case AList.lookup (op =) overloading (c, ty)
+ of SOME (v, _) => SOME (ty, Free (v, ty))
+ | NONE => NONE;
+ val unchecks =
+ map (fn (c_ty as (_, ty), (v, _)) => (Free (v, ty), Const c_ty)) overloading;
+ in
+ ctxt
+ |> map_improvable_syntax (K ((([], []), (((K NONE, subst), false), unchecks)), false))
+ end
-(* overloaded declarations and definitions *)
+fun init raw_overloading thy =
+ let
+ val _ = if null raw_overloading then error "At least one parameter must be given" else ();
+ val overloading = map (fn (v, c_ty, checked) => (c_ty, (v, checked))) raw_overloading;
+ in
+ thy
+ |> ProofContext.init
+ |> OverloadingData.put overloading
+ |> fold (fn ((_, ty), (v, _)) => Variable.declare_names (Free (v, ty))) overloading
+ |> add_improvable_syntax
+ |> synchronize_syntax
+ end;
fun declare c_ty = pair (Const c_ty);
fun define checked b (c, t) = Thm.add_def (not checked) true
(b, Logic.mk_equals (Const (c, Term.fastype_of t), t));
-
-(* target *)
-
-fun init raw_overloading thy =
- let
- val _ = if null raw_overloading then error "At least one parameter must be given" else ();
- val overloading = map (fn (v, c_ty, checked) => (c_ty, (v, checked))) raw_overloading;
- fun subst (c, ty) = case AList.lookup (op =) overloading (c, ty)
- of SOME (v, _) => SOME (ty, Free (v, ty))
- | NONE => NONE;
- val unchecks =
- map (fn (c_ty as (_, ty), (v, _)) => (Free (v, ty), Const c_ty)) overloading;
- in
- thy
- |> ProofContext.init
- |> OverloadingData.put overloading
- |> fold (fn ((_, ty), (v, _)) => Variable.declare_names (Free (v, ty))) overloading
- |> map_improvable_syntax (K ((([], []), (((K NONE, subst), false), unchecks)), false))
- |> add_improvable_syntax
- end;
+fun confirm b = map_overloading (filter_out (fn (_, (c', _)) => c' = Binding.name_of b))
+ #> LocalTheory.target synchronize_syntax
fun conclude lthy =
let
--- a/src/Tools/Code/code_preproc.ML Thu Jul 30 23:50:11 2009 +0200
+++ b/src/Tools/Code/code_preproc.ML Fri Jul 31 09:34:21 2009 +0200
@@ -129,6 +129,12 @@
#> Logic.dest_equals
#> snd;
+fun same_arity thy thms =
+ let
+ val num_args_of = length o snd o strip_comb o fst o Logic.dest_equals;
+ val k = fold (curry Int.max o num_args_of o Thm.prop_of) thms 0;
+ in map (Code.expand_eta thy k) thms end;
+
fun preprocess thy c eqns =
let
val pre = (Simplifier.theory_context thy o #pre o the_thmproc) thy;
@@ -140,8 +146,8 @@
|> (map o apfst) (rewrite_eqn pre)
|> (map o apfst) (AxClass.unoverload thy)
|> map (Code.assert_eqn thy)
- |> burrow_fst (Code.norm_args thy)
- |> burrow_fst (Code.norm_varnames thy)
+ |> burrow_fst (same_arity thy)
+ |> burrow_fst (Code.desymbolize_all_vars thy)
end;
fun preprocess_conv thy ct =