--- a/Admin/makedist Mon Aug 10 13:53:42 2009 +0200
+++ b/Admin/makedist Tue Aug 11 20:40:02 2009 +0200
@@ -165,8 +165,8 @@
perl -pi -e "s,val changelog = \"\",val changelog = \"$REPOS/log/$IDENT\",g" src/Pure/ROOT.ML
perl -pi -e "s,ISABELLE_IDENTIFIER=\"\",ISABELLE_IDENTIFIER=\"$DISTNAME\",g" lib/scripts/getsettings
perl -pi -e "s,{ISABELLE},$DISTNAME,g" lib/html/library_index_header.template
-perl -pi -e "s,Isabelle repository version,$DISTVERSION,g" src/Pure/ROOT.ML lib/Tools/version
-perl -pi -e "s,the internal repository version of Isabelle,$DISTVERSION,g" README
+perl -pi -e "s,unidentified repository version,$DISTVERSION,g" src/Pure/ROOT.ML lib/Tools/version
+perl -pi -e "s,some unidentified repository version of Isabelle,$DISTVERSION,g" README
# create archives
--- a/README Mon Aug 10 13:53:42 2009 +0200
+++ b/README Tue Aug 11 20:40:02 2009 +0200
@@ -2,7 +2,7 @@
Version information
- This is the internal repository version of Isabelle.
+ This is some unidentified repository version of Isabelle.
See the NEWS file in the distribution for details on user-relevant
changes.
--- a/README_REPOSITORY Mon Aug 10 13:53:42 2009 +0200
+++ b/README_REPOSITORY Tue Aug 11 20:40:02 2009 +0200
@@ -208,8 +208,8 @@
two-dimensional presentation too much.
-Building Isabelle from the repository version
----------------------------------------------
+Building a repository version of Isabelle
+-----------------------------------------
Compared to a proper distribution or development snapshot, a
repository version of Isabelle lacks textual version identifiers in
--- a/doc-src/Codegen/Thy/document/Introduction.tex Mon Aug 10 13:53:42 2009 +0200
+++ b/doc-src/Codegen/Thy/document/Introduction.tex Tue Aug 11 20:40:02 2009 +0200
@@ -229,14 +229,14 @@
\hspace*{0pt}module Example where {\char123}\\
\hspace*{0pt}\\
\hspace*{0pt}\\
-\hspace*{0pt}foldla ::~forall a{\char95}1 b{\char95}1.~(a{\char95}1 -> b{\char95}1 -> a{\char95}1) -> a{\char95}1 -> [b{\char95}1] -> a{\char95}1;\\
+\hspace*{0pt}foldla ::~forall a b.~(a -> b -> a) -> a -> [b] -> a;\\
\hspace*{0pt}foldla f a [] = a;\\
\hspace*{0pt}foldla f a (x :~xs) = foldla f (f a x) xs;\\
\hspace*{0pt}\\
\hspace*{0pt}rev ::~forall a.~[a] -> [a];\\
\hspace*{0pt}rev xs = foldla ({\char92}~xsa x -> x :~xsa) [] xs;\\
\hspace*{0pt}\\
-\hspace*{0pt}list{\char95}case ::~forall t a.~t -> (a -> [a] -> t) -> [a] -> t;\\
+\hspace*{0pt}list{\char95}case ::~forall a b.~a -> (b -> [b] -> a) -> [b] -> a;\\
\hspace*{0pt}list{\char95}case f1 f2 (a :~list) = f2 a list;\\
\hspace*{0pt}list{\char95}case f1 f2 [] = f1;\\
\hspace*{0pt}\\
--- a/doc-src/Codegen/Thy/examples/Example.hs Mon Aug 10 13:53:42 2009 +0200
+++ b/doc-src/Codegen/Thy/examples/Example.hs Tue Aug 11 20:40:02 2009 +0200
@@ -3,14 +3,14 @@
module Example where {
-foldla :: forall a_1 b_1. (a_1 -> b_1 -> a_1) -> a_1 -> [b_1] -> a_1;
+foldla :: forall a b. (a -> b -> a) -> a -> [b] -> a;
foldla f a [] = a;
foldla f a (x : xs) = foldla f (f a x) xs;
rev :: forall a. [a] -> [a];
rev xs = foldla (\ xsa x -> x : xsa) [] xs;
-list_case :: forall t a. t -> (a -> [a] -> t) -> [a] -> t;
+list_case :: forall a b. a -> (b -> [b] -> a) -> [b] -> a;
list_case f1 f2 (a : list) = f2 a list;
list_case f1 f2 [] = f1;
--- a/lib/Tools/version Mon Aug 10 13:53:42 2009 +0200
+++ b/lib/Tools/version Tue Aug 11 20:40:02 2009 +0200
@@ -4,5 +4,4 @@
#
# DESCRIPTION: display Isabelle version
-
-echo 'Isabelle repository version' # filled in automatically!
+echo 'unidentified repository version' # filled in automatically!
--- a/src/HOL/Code_Eval.thy Mon Aug 10 13:53:42 2009 +0200
+++ b/src/HOL/Code_Eval.thy Tue Aug 11 20:40:02 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/Fun.thy Mon Aug 10 13:53:42 2009 +0200
+++ b/src/HOL/Fun.thy Tue Aug 11 20:40:02 2009 +0200
@@ -250,6 +250,9 @@
lemma bij_betw_imp_inj_on: "bij_betw f A B \<Longrightarrow> inj_on f A"
by (simp add: bij_betw_def)
+lemma bij_comp: "bij f \<Longrightarrow> bij g \<Longrightarrow> bij (g o f)"
+by(fastsimp intro: comp_inj_on comp_surj simp: bij_def surj_range)
+
lemma bij_betw_trans:
"bij_betw f A B \<Longrightarrow> bij_betw g B C \<Longrightarrow> bij_betw (g o f) A C"
by(auto simp add:bij_betw_def comp_inj_on)
--- a/src/HOL/Library/Efficient_Nat.thy Mon Aug 10 13:53:42 2009 +0200
+++ b/src/HOL/Library/Efficient_Nat.thy Tue Aug 11 20:40:02 2009 +0200
@@ -167,7 +167,7 @@
val contains_suc = exists_Const (fn (c, _) => c = @{const_name Suc});
in
if forall (can dest) thms andalso exists (contains_suc o dest) thms
- then perhaps_loop (remove_suc thy) thms
+ then thms |> perhaps_loop (remove_suc thy) |> (Option.map o map) Drule.zero_var_indexes
else NONE
end;
--- a/src/HOL/Library/Nat_Int_Bij.thy Mon Aug 10 13:53:42 2009 +0200
+++ b/src/HOL/Library/Nat_Int_Bij.thy Tue Aug 11 20:40:02 2009 +0200
@@ -165,5 +165,11 @@
lemma inj_int_to_nat_bij: "inj int_to_nat_bij"
by(simp add:inv_nat_to_int_bij[symmetric] surj_nat_to_int_bij surj_imp_inj_inv)
+lemma bij_nat_to_int_bij: "bij nat_to_int_bij"
+by(simp add:bij_def inj_nat_to_int_bij surj_nat_to_int_bij)
+
+lemma bij_int_to_nat_bij: "bij int_to_nat_bij"
+by(simp add:bij_def inj_int_to_nat_bij surj_int_to_nat_bij)
+
end
--- a/src/HOL/MicroJava/J/JListExample.thy Mon Aug 10 13:53:42 2009 +0200
+++ b/src/HOL/MicroJava/J/JListExample.thy Tue Aug 11 20:40:02 2009 +0200
@@ -1,12 +1,11 @@
(* Title: HOL/MicroJava/J/JListExample.thy
- ID: $Id$
Author: Stefan Berghofer
*)
header {* \isaheader{Example for generating executable code from Java semantics} *}
theory JListExample
-imports Eval SystemClasses
+imports Eval
begin
ML {* Syntax.ambiguity_level := 100000 *}
--- a/src/HOL/MicroJava/J/State.thy Mon Aug 10 13:53:42 2009 +0200
+++ b/src/HOL/MicroJava/J/State.thy Tue Aug 11 20:40:02 2009 +0200
@@ -1,12 +1,13 @@
(* Title: HOL/MicroJava/J/State.thy
- ID: $Id$
Author: David von Oheimb
Copyright 1999 Technische Universitaet Muenchen
*)
header {* \isaheader{Program State} *}
-theory State imports TypeRel Value begin
+theory State
+imports TypeRel Value
+begin
types
fields' = "(vname \<times> cname \<rightharpoonup> val)" -- "field name, defining class, value"
@@ -19,7 +20,6 @@
init_vars :: "('a \<times> ty) list => ('a \<rightharpoonup> val)"
"init_vars == map_of o map (\<lambda>(n,T). (n,default_val T))"
-
types aheap = "loc \<rightharpoonup> obj" -- {* "@{text heap}" used in a translation below *}
locals = "vname \<rightharpoonup> val" -- "simple state, i.e. variable contents"
--- a/src/HOL/MicroJava/JVM/JVMListExample.thy Mon Aug 10 13:53:42 2009 +0200
+++ b/src/HOL/MicroJava/JVM/JVMListExample.thy Tue Aug 11 20:40:02 2009 +0200
@@ -1,11 +1,12 @@
(* Title: HOL/MicroJava/JVM/JVMListExample.thy
- ID: $Id$
Author: Stefan Berghofer
*)
header {* \isaheader{Example for generating executable code from JVM semantics}\label{sec:JVMListExample} *}
-theory JVMListExample imports "../J/SystemClasses" JVMExec begin
+theory JVMListExample
+imports "../J/SystemClasses" JVMExec
+begin
consts
list_nam :: cnam
--- a/src/HOL/Tools/hologic.ML Mon Aug 10 13:53:42 2009 +0200
+++ b/src/HOL/Tools/hologic.ML Tue Aug 11 20:40:02 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 Mon Aug 10 13:53:42 2009 +0200
+++ b/src/HOL/Tools/inductive_codegen.ML Tue Aug 11 20:40:02 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 Mon Aug 10 13:53:42 2009 +0200
+++ b/src/HOL/Tools/inductive_set.ML Tue Aug 11 20:40:02 2009 +0200
@@ -34,10 +34,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
@@ -80,7 +80,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) =
@@ -224,11 +224,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 =
@@ -241,7 +241,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 |>
@@ -249,7 +249,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
@@ -362,12 +362,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 |>
@@ -423,14 +423,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;
@@ -449,13 +449,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 @
@@ -485,7 +485,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 *)
@@ -496,7 +496,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 Mon Aug 10 13:53:42 2009 +0200
+++ b/src/HOL/Tools/quickcheck_generators.ML Tue Aug 11 20:40:02 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 Mon Aug 10 13:53:42 2009 +0200
+++ b/src/HOL/Tools/recfun_codegen.ML Tue Aug 11 20:40:02 2009 +0200
@@ -14,6 +14,8 @@
open Codegen;
+val const_of = dest_Const o head_of o fst o Logic.dest_equals;
+
structure ModuleData = TheoryDataFun
(
type T = string Symtab.table;
@@ -31,43 +33,32 @@
|> ModuleData.map (Symtab.update (fst (Code.const_typ_eqn thy thm'), module_name))
end;
-fun expand_eta thy [] = []
- | expand_eta thy (thms as thm :: _) =
- let
- val (_, ty) = Code.const_typ_eqn thy thm;
- in if null (Term.add_tvarsT ty []) orelse (null o fst o strip_type) ty
- then thms
- else map (Code.expand_eta thy 1) thms
- end;
+fun avoid_value thy [thm] =
+ let val (_, T) = Code.const_typ_eqn thy thm
+ in if null (Term.add_tvarsT T []) orelse (null o fst o strip_type) T
+ then [thm]
+ else [Code_Thingol.expand_eta thy 1 thm]
+ end
+ | avoid_value thy thms = thms;
-fun retrieve_equations thy (c, T) = if c = @{const_name "op ="} then NONE else
+fun get_equations thy defs (raw_c, T) = if raw_c = @{const_name "op ="} then ([], "") else
let
- val c' = AxClass.unoverload_const thy (c, T);
- val opt_name = Symtab.lookup (ModuleData.get thy) c';
- val thms = Code.these_eqns thy c'
+ val c = AxClass.unoverload_const thy (raw_c, T);
+ val raw_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
- |> map (rpair opt_name)
- in if null thms then NONE else SOME thms end;
-
-val dest_eqn = Logic.dest_equals;
-val const_of = dest_Const o head_of o fst o dest_eqn;
-
-fun get_equations thy defs (s, T) =
- (case retrieve_equations thy (s, T) of
- NONE => ([], "")
- | SOME thms =>
- let val thms' = filter (fn (thm, _) => is_instance T
- (snd (const_of (prop_of thm)))) thms
- in if null thms' then ([], "")
- else (preprocess thy (map fst thms'),
- case snd (snd (split_last thms')) of
- NONE => (case get_defn thy defs s T of
- NONE => Codegen.thyname_of_const thy s
- | SOME ((_, (thyname, _)), _) => thyname)
- | SOME thyname => thyname)
- end);
+ |> filter (is_instance T o snd o const_of o prop_of);
+ val module_name = case Symtab.lookup (ModuleData.get thy) c
+ of SOME module_name => module_name
+ | NONE => case get_defn thy defs c T
+ of SOME ((_, (thyname, _)), _) => thyname
+ | NONE => Codegen.thyname_of_const thy c;
+ in if null raw_thms then ([], "") else
+ raw_thms
+ |> preprocess thy
+ |> avoid_value thy
+ |> Code_Thingol.clean_thms thy
+ |> rpair module_name
+ end;
fun mk_suffix thy defs (s, T) = (case get_defn thy defs s T of
SOME (_, SOME i) => " def" ^ string_of_int i | _ => "");
@@ -81,7 +72,7 @@
fun add_rec_funs thy defs dep module eqs gr =
let
fun dest_eq t = (fst (const_of t) ^ mk_suffix thy defs (const_of t),
- dest_eqn (rename_term t));
+ Logic.dest_equals (rename_term t));
val eqs' = map dest_eq eqs;
val (dname, _) :: _ = eqs';
val (s, T) = const_of (hd eqs);
--- a/src/HOL/Tools/split_rule.ML Mon Aug 10 13:53:42 2009 +0200
+++ b/src/HOL/Tools/split_rule.ML Tue Aug 11 20:40:02 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 Mon Aug 10 13:53:42 2009 +0200
+++ b/src/HOL/ex/Predicate_Compile.thy Tue Aug 11 20:40:02 2009 +0200
@@ -1,61 +1,8 @@
theory Predicate_Compile
-imports Main Lattice_Syntax Code_Eval RPred
+imports Complex_Main RPred
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 Mon Aug 10 13:53:42 2009 +0200
+++ b/src/HOL/ex/Predicate_Compile_ex.thy Tue Aug 11 20:40:02 2009 +0200
@@ -18,15 +18,10 @@
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
@@ -34,6 +29,15 @@
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}"
inductive partition :: "('a \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> 'a list \<Rightarrow> 'a list \<Rightarrow> bool"
for f where
@@ -51,17 +55,15 @@
code_pred is_even .
-(* TODO: requires to handle abstractions in parameter positions correctly *)
values 10 "{(ys, zs). partition is_even
[0, Suc 0, 2, 3, 4, 5, 6, 7] ys zs}"
-
values 10 "{zs. partition is_even zs [0, 2] [3, 5]}"
values 10 "{zs. partition is_even zs [0, 7] [3, 5]}"
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
code_pred tranclp
proof -
@@ -76,6 +78,7 @@
thm tranclp.rpred_equation
*)
+
inductive succ :: "nat \<Rightarrow> nat \<Rightarrow> bool" where
"succ 0 1"
| "succ m n \<Longrightarrow> succ (Suc m) (Suc n)"
@@ -83,7 +86,13 @@
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? -- value chooses mode [] --> [1] and then starts enumerating all successors *)
+
(*
values 20 "{n. tranclp succ 10 n}"
values "{n. tranclp succ n 10}"
--- a/src/HOL/ex/predicate_compile.ML Mon Aug 10 13:53:42 2009 +0200
+++ b/src/HOL/ex/predicate_compile.ML Tue Aug 11 20:40:02 2009 +0200
@@ -54,6 +54,7 @@
mk_sup : term * term -> term,
mk_if : term -> term,
mk_not : term -> term,
+ mk_map : typ -> typ -> term -> term -> term,
lift_pred : term -> term
};
datatype tmode = Mode of mode * int list * tmode option list;
@@ -608,6 +609,7 @@
mk_not : term -> term,
(* funT_of : mode -> typ -> typ, *)
(* mk_fun_of : theory -> (string * typ) -> mode -> term, *)
+ mk_map : typ -> typ -> term -> term -> term,
lift_pred : term -> term
};
@@ -621,6 +623,7 @@
fun mk_not (CompilationFuns funs) = #mk_not funs
(*fun funT_of (CompilationFuns funs) = #funT_of funs*)
(*fun mk_fun_of (CompilationFuns funs) = #mk_fun_of funs*)
+fun mk_map (CompilationFuns funs) = #mk_map funs
fun lift_pred (CompilationFuns funs) = #lift_pred funs
fun funT_of compfuns (iss, is) T =
@@ -691,12 +694,15 @@
in
Const (@{const_name Predicate.eval}, mk_predT T --> T --> HOLogic.boolT) $ f $ x
end;
-
+
+fun mk_map T1 T2 tf tp = Const (@{const_name Predicate.map},
+ (T1 --> T2) --> mk_predT T1 --> mk_predT T2) $ tf $ tp;
+
val lift_pred = I
val compfuns = CompilationFuns {mk_predT = mk_predT, dest_predT = dest_predT, mk_bot = mk_bot,
mk_single = mk_single, mk_bind = mk_bind, mk_sup = mk_sup, mk_if = mk_if, mk_not = mk_not,
- lift_pred = lift_pred}
+ mk_map = mk_map, lift_pred = lift_pred};
end;
@@ -748,7 +754,9 @@
HOLogic.boolT --> mk_rpredT HOLogic.unitT) $ cond;
fun mk_not t = error "Negation is not defined for RPred"
-
+
+fun mk_map t = error "FIXME" (*FIXME*)
+
fun lift_pred t =
let
val T = PredicateCompFuns.dest_predT (fastype_of t)
@@ -759,7 +767,7 @@
val compfuns = CompilationFuns {mk_predT = mk_rpredT, dest_predT = dest_rpredT, mk_bot = mk_bot,
mk_single = mk_single, mk_bind = mk_bind, mk_sup = mk_sup, mk_if = mk_if, mk_not = mk_not,
- lift_pred = lift_pred}
+ mk_map = mk_map, lift_pred = lift_pred};
end;
(* for external use with interactive mode *)
@@ -2094,18 +2102,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, _) = split_smode 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
@@ -2114,10 +2121,62 @@
| [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 NONE thy
- (m, list_comb (pred, params)),
- inargs)
+ val (inargs, outargs) = split_smode user_mode args;
+ val t_pred = list_comb (compile_expr NONE thy (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_map PredicateCompFuns.compfuns 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_predT PredicateCompFuns.compfuns (fastype_of t);
+ val t' = mk_map PredicateCompFuns.compfuns 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 Mon Aug 10 13:53:42 2009 +0200
+++ b/src/Pure/Isar/code.ML Tue Aug 11 20:40:02 2009 +0200
@@ -33,9 +33,6 @@
-> (thm * bool) list -> (thm * bool) list
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
(*executable code*)
val add_datatype: (string * typ) list -> theory -> theory
@@ -126,115 +123,6 @@
in (map dest_TFree (Sign.const_typargs thy (c, ty')), Type.strip_sorts ty') end;
-(* code equation transformations *)
-
-fun expand_eta thy k thm =
- let
- val (lhs, rhs) = (Logic.dest_equals o Thm.plain_prop_of) thm;
- val (head, args) = strip_comb lhs;
- 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;
- fun expand (v, ty) thm = Drule.fun_cong_rule thm
- (Thm.cterm_of thy (Var ((v, 0), ty)));
- in
- thm
- |> fold expand vs
- |> 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 =
- 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;
-
-fun canonical_absvars thm =
- 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;
-
-fun norm_varnames thy thms =
- 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;
-
-
(** data store **)
(* code equations *)
@@ -662,32 +550,21 @@
^ string_of_const thy c ^ "\n" ^ Display.string_of_thm_global thy thm)
in map (cert o assert_eqn thy) eqns end;
-fun common_typ_eqns thy [] = []
- | common_typ_eqns thy [thm] = [thm]
- | common_typ_eqns thy (thms as thm :: _) = (*FIXME is too general*)
- let
- fun incr_thm thm max =
- let
- val thm' = incr_indexes max thm;
- val max' = Thm.maxidx_of thm' + 1;
- in (thm', max') end;
- val (thms', maxidx) = fold_map incr_thm thms 0;
- val ty1 :: tys = map (snd o const_typ_eqn thy) thms';
- fun unify ty env = Sign.typ_unify thy (ty1, ty) env
- handle Type.TUNIFY =>
- error ("Type unificaton failed, while unifying code equations\n"
- ^ (cat_lines o map (Display.string_of_thm_global thy)) thms
- ^ "\nwith types\n"
- ^ (cat_lines o map (string_of_typ thy)) (ty1 :: tys));
- val (env, _) = fold unify tys (Vartab.empty, maxidx)
- val instT = Vartab.fold (fn (x_i, (sort, ty)) =>
- cons (Thm.ctyp_of thy (TVar (x_i, sort)), Thm.ctyp_of thy ty)) env [];
- in map (Thm.instantiate (instT, [])) thms' end;
+fun same_typscheme thy thms =
+ let
+ fun tvars_of t = rev (Term.add_tvars t []);
+ val vss = map (tvars_of o Thm.prop_of) thms;
+ fun inter_sorts vs =
+ fold (curry (Sorts.inter_sort (Sign.classes_of thy)) o snd) vs [];
+ val sorts = map_transpose inter_sorts vss;
+ val vts = Name.names Name.context Name.aT sorts
+ |> map (fn (v, sort) => TVar ((v, 0), sort));
+ in map2 (fn vs => Thm.certify_instantiate (vs ~~ vts, [])) vss thms end;
fun these_eqns thy c =
get_eqns thy c
|> (map o apfst) (Thm.transfer thy)
- |> burrow_fst (common_typ_eqns thy);
+ |> burrow_fst (same_typscheme thy);
fun all_eqns thy =
Symtab.dest ((the_eqns o the_exec) thy)
--- a/src/Pure/Isar/overloading.ML Mon Aug 10 13:53:42 2009 +0200
+++ b/src/Pure/Isar/overloading.ML Tue Aug 11 20:40:02 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/Pure/ROOT.ML Mon Aug 10 13:53:42 2009 +0200
+++ b/src/Pure/ROOT.ML Tue Aug 11 20:40:02 2009 +0200
@@ -2,7 +2,7 @@
structure Distribution = (*filled-in by makedist*)
struct
- val version = "Isabelle repository version";
+ val version = "unidentified repository version";
val is_official = false;
val changelog = "";
end;
--- a/src/Pure/library.ML Mon Aug 10 13:53:42 2009 +0200
+++ b/src/Pure/library.ML Tue Aug 11 20:40:02 2009 +0200
@@ -109,6 +109,7 @@
val split_list: ('a * 'b) list -> 'a list * 'b list
val map_product: ('a -> 'b -> 'c) -> 'a list -> 'b list -> 'c list
val fold_product: ('a -> 'b -> 'c -> 'c) -> 'a list -> 'b list -> 'c -> 'c
+ val map_transpose: ('a list -> 'b) -> 'a list list -> 'b list
val separate: 'a -> 'a list -> 'a list
val surround: 'a -> 'a list -> 'a list
val replicate: int -> 'a -> 'a list
@@ -929,6 +930,17 @@
in dups end;
+(* matrices *)
+
+fun map_transpose f xss =
+ let
+ val n = case distinct (op =) (map length xss)
+ of [] => 0
+ | [n] => n
+ | _ => raise UnequalLengths;
+ in map (fn m => f (map (fn xs => nth xs m) xss)) (0 upto n - 1) end;
+
+
(** lists as multisets **)
--- a/src/Tools/Code/code_preproc.ML Mon Aug 10 13:53:42 2009 +0200
+++ b/src/Tools/Code/code_preproc.ML Tue Aug 11 20:40:02 2009 +0200
@@ -109,7 +109,10 @@
| apply_functrans thy c [] eqns = eqns
| apply_functrans thy c functrans eqns = eqns
|> perhaps (perhaps_loop (perhaps_apply functrans))
- |> Code.assert_eqns_const thy c;
+ |> Code.assert_eqns_const thy c
+ (*FIXME in future, the check here should be more accurate wrt. type schemes
+ -- perhaps by means of upcoming code certificates with a corresponding
+ preprocessor protocol*);
fun rhs_conv conv thm = Thm.transitive thm ((conv o Thm.rhs_of) thm);
@@ -140,8 +143,6 @@
|> (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)
end;
fun preprocess_conv thy ct =
--- a/src/Tools/Code/code_thingol.ML Mon Aug 10 13:53:42 2009 +0200
+++ b/src/Tools/Code/code_thingol.ML Tue Aug 11 20:40:02 2009 +0200
@@ -79,6 +79,8 @@
val is_cons: program -> string -> bool
val contr_classparam_typs: program -> string -> itype option list
+ val expand_eta: theory -> int -> thm -> thm
+ val clean_thms: theory -> thm list -> thm list
val read_const_exprs: theory -> string list -> string list * string list
val consts_program: theory -> string list -> string list * (naming * program)
val cached_program: theory -> naming * program
@@ -376,6 +378,60 @@
end; (* local *)
+(** technical transformations of code equations **)
+
+fun expand_eta thy k thm =
+ let
+ val (lhs, rhs) = (Logic.dest_equals o Thm.plain_prop_of) thm;
+ val (head, args) = strip_comb lhs;
+ val l = if k = ~1
+ then (length o fst o strip_abs) rhs
+ else Int.max (0, k - length args);
+ 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 vars
+ |> Conv.fconv_rule Drule.beta_eta_conversion
+ end;
+
+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 (expand_eta thy k) thms end;
+
+fun mk_desymbolization pre post mk vs =
+ let
+ val names = map (pre o fst o fst) vs
+ |> map (Name.desymbolize false)
+ |> Name.variant_list []
+ |> map post;
+ in map_filter (fn (((v, i), x), v') =>
+ if v = v' andalso i = 0 then NONE
+ else SOME (((v, i), x), mk ((v', 0), x))) (vs ~~ names)
+ end;
+
+fun desymbolize_tvars thy thms =
+ let
+ val tvs = fold (Term.add_tvars o Thm.prop_of) thms [];
+ val tvar_subst = mk_desymbolization (unprefix "'") (prefix "'") TVar tvs;
+ in map (Thm.certify_instantiate (tvar_subst, [])) thms end;
+
+fun desymbolize_vars thy thm =
+ let
+ val vs = Term.add_vars (Thm.prop_of thm) [];
+ val var_subst = mk_desymbolization I I Var vs;
+ in Thm.certify_instantiate ([], var_subst) thm end;
+
+fun desymbolize_all_vars thy = desymbolize_tvars thy #> map (desymbolize_vars thy);
+
+fun clean_thms thy = same_arity thy #> desymbolize_all_vars thy;
+
+
(** statements, abstract programs **)
type typscheme = (vname * sort) list * itype;
@@ -498,17 +554,11 @@
fun stmt_classparam class =
ensure_class thy algbr funcgr class
#>> (fn class => Classparam (c, class));
- fun stmt_fun ((vs, ty), raw_thms) =
- let
- val thms = if null (Term.add_tfreesT ty []) orelse (null o fst o strip_type) ty
- then raw_thms
- else (map o apfst) (Code.expand_eta thy 1) raw_thms;
- in
- fold_map (translate_tyvar_sort thy algbr funcgr) vs
- ##>> translate_typ thy algbr funcgr ty
- ##>> fold_map (translate_eq thy algbr funcgr) thms
- #>> (fn info => Fun (c, info))
- end;
+ fun stmt_fun ((vs, ty), eqns) =
+ fold_map (translate_tyvar_sort thy algbr funcgr) vs
+ ##>> translate_typ thy algbr funcgr ty
+ ##>> fold_map (translate_eqn thy algbr funcgr) (burrow_fst (clean_thms thy) eqns)
+ #>> (fn info => Fun (c, info));
val stmt_const = case Code.get_datatype_of_constr thy c
of SOME tyco => stmt_datatypecons tyco
| NONE => (case AxClass.class_of_param thy c
@@ -597,7 +647,7 @@
translate_term thy algbr funcgr thm t'
##>> fold_map (translate_term thy algbr funcgr thm) ts
#>> (fn (t, ts) => t `$$ ts)
-and translate_eq thy algbr funcgr (thm, proper) =
+and translate_eqn thy algbr funcgr (thm, proper) =
let
val (args, rhs) = (apfst (snd o strip_comb) o Logic.dest_equals
o Logic.unvarify o prop_of) thm;