--- a/src/HOL/IsaMakefile Wed Jul 14 12:27:44 2010 +0200
+++ b/src/HOL/IsaMakefile Wed Jul 14 14:16:12 2010 +0200
@@ -106,6 +106,7 @@
$(SRC)/Provers/hypsubst.ML \
$(SRC)/Provers/quantifier1.ML \
$(SRC)/Provers/splitter.ML \
+ $(SRC)/Tools/cache_io.ML \
$(SRC)/Tools/Code/code_eval.ML \
$(SRC)/Tools/Code/code_haskell.ML \
$(SRC)/Tools/Code/code_ml.ML \
@@ -266,7 +267,6 @@
$(SRC)/Provers/Arith/cancel_numerals.ML \
$(SRC)/Provers/Arith/combine_numerals.ML \
$(SRC)/Provers/Arith/extract_common_term.ML \
- $(SRC)/Tools/cache_io.ML \
$(SRC)/Tools/Metis/metis.ML \
Tools/ATP_Manager/async_manager.ML \
Tools/ATP_Manager/atp_manager.ML \
@@ -397,7 +397,8 @@
$(OUT)/HOL-Library: $(OUT)/HOL Library/HOL_Library_ROOT.ML \
$(SRC)/HOL/Tools/float_arith.ML $(SRC)/Tools/float.ML \
- Library/Abstract_Rat.thy Library/Adhoc_Overloading.thy Library/AssocList.thy \
+ Library/Abstract_Rat.thy $(SRC)/Tools/Adhoc_Overloading.thy \
+ Library/AssocList.thy \
Library/BigO.thy Library/Binomial.thy Library/Bit.thy \
Library/Boolean_Algebra.thy Library/Cardinality.thy \
Library/Char_nat.thy Library/Code_Char.thy Library/Code_Char_chr.thy \
@@ -415,7 +416,8 @@
Library/Lattice_Syntax.thy Library/Library.thy \
Library/List_Prefix.thy Library/List_lexord.thy Library/Mapping.thy \
Library/Monad_Syntax.thy Library/More_List.thy Library/More_Set.thy \
- Library/Multiset.thy Library/Nat_Bijection.thy Library/Nat_Infinity.thy \
+ Library/Multiset.thy Library/Nat_Bijection.thy \
+ Library/Nat_Infinity.thy \
Library/Nested_Environment.thy Library/Numeral_Type.thy \
Library/OptionalSugar.thy Library/Order_Relation.thy \
Library/Permutation.thy Library/Permutations.thy \
@@ -434,7 +436,7 @@
Library/Sum_Of_Squares/sum_of_squares.ML \
Library/Transitive_Closure_Table.thy Library/Univ_Poly.thy \
Library/While_Combinator.thy Library/Zorn.thy \
- Library/adhoc_overloading.ML Library/positivstellensatz.ML \
+ $(SRC)/Tools/adhoc_overloading.ML Library/positivstellensatz.ML \
Library/reflection.ML Library/reify_data.ML \
Library/document/root.bib Library/document/root.tex
@cd Library; $(ISABELLE_TOOL) usedir -b -f HOL_Library_ROOT.ML $(OUT)/HOL HOL-Library
--- a/src/HOL/Library/Adhoc_Overloading.thy Wed Jul 14 12:27:44 2010 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,14 +0,0 @@
-(* Author: Alexander Krauss, TU Muenchen
- Author: Christian Sternagel, University of Innsbruck
-*)
-
-header {* Ad-hoc overloading of constants based on their types *}
-
-theory Adhoc_Overloading
-imports Main
-uses "adhoc_overloading.ML"
-begin
-
-setup Adhoc_Overloading.setup
-
-end
--- a/src/HOL/Library/Library.thy Wed Jul 14 12:27:44 2010 +0200
+++ b/src/HOL/Library/Library.thy Wed Jul 14 14:16:12 2010 +0200
@@ -2,7 +2,6 @@
theory Library
imports
Abstract_Rat
- Adhoc_Overloading
AssocList
BigO
Binomial
--- a/src/HOL/Library/Monad_Syntax.thy Wed Jul 14 12:27:44 2010 +0200
+++ b/src/HOL/Library/Monad_Syntax.thy Wed Jul 14 14:16:12 2010 +0200
@@ -5,7 +5,7 @@
header {* Monad notation for arbitrary types *}
theory Monad_Syntax
-imports Adhoc_Overloading
+imports "~~/src/Tools/Adhoc_Overloading"
begin
text {*
--- a/src/HOL/Library/adhoc_overloading.ML Wed Jul 14 12:27:44 2010 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,140 +0,0 @@
-(* Author: Alexander Krauss, TU Muenchen
- Author: Christian Sternagel, University of Innsbruck
-
-Ad-hoc overloading of constants based on their types.
-*)
-
-signature ADHOC_OVERLOADING =
-sig
-
- val add_overloaded: string -> theory -> theory
- val add_variant: string -> string -> theory -> theory
-
- val show_variants: bool Unsynchronized.ref
- val setup: theory -> theory
-
-end
-
-
-structure Adhoc_Overloading: ADHOC_OVERLOADING =
-struct
-
-val show_variants = Unsynchronized.ref false;
-
-
-(* errors *)
-
-fun duplicate_variant_err int_name ext_name =
- error ("Constant " ^ quote int_name ^ " is already a variant of " ^ quote ext_name);
-
-fun not_overloaded_err name =
- error ("Constant " ^ quote name ^ " is not declared as overloaded");
-
-fun already_overloaded_err name =
- error ("Constant " ^ quote name ^ " is already declared as overloaded");
-
-fun unresolved_err ctxt (c, T) t reason =
- error ("Unresolved overloading of " ^ quote c ^ " :: " ^
- quote (Syntax.string_of_typ ctxt T) ^ " in " ^
- quote (Syntax.string_of_term ctxt t) ^ " (" ^ reason ^ ")");
-
-
-(* theory data *)
-
-structure Overload_Data = Theory_Data
-(
- type T =
- { internalize : (string * typ) list Symtab.table,
- externalize : string Symtab.table };
- val empty = {internalize=Symtab.empty, externalize=Symtab.empty};
- val extend = I;
-
- fun merge_ext int_name (ext_name1, ext_name2) =
- if ext_name1 = ext_name2 then ext_name1
- else duplicate_variant_err int_name ext_name1;
-
- fun merge ({internalize=int1, externalize=ext1},
- {internalize=int2, externalize=ext2}) =
- {internalize=Symtab.join (K (Library.merge (op =))) (int1, int2),
- externalize=Symtab.join merge_ext (ext1, ext2)};
-);
-
-fun map_tables f g =
- Overload_Data.map (fn {internalize=int, externalize=ext} =>
- {internalize=f int, externalize=g ext});
-
-val is_overloaded = Symtab.defined o #internalize o Overload_Data.get;
-val get_variants = Symtab.lookup o #internalize o Overload_Data.get;
-val get_external = Symtab.lookup o #externalize o Overload_Data.get;
-
-fun add_overloaded ext_name thy =
- let val _ = not (is_overloaded thy ext_name) orelse already_overloaded_err ext_name;
- in map_tables (Symtab.update (ext_name, [])) I thy end;
-
-fun add_variant ext_name name thy =
- let
- val _ = is_overloaded thy ext_name orelse not_overloaded_err ext_name;
- val _ = case get_external thy name of
- NONE => ()
- | SOME gen' => duplicate_variant_err name gen';
- val T = Sign.the_const_type thy name;
- in
- map_tables (Symtab.cons_list (ext_name, (name, T)))
- (Symtab.update (name, ext_name)) thy
- end
-
-
-(* check / uncheck *)
-
-fun unifiable_with ctxt T1 (c, T2) =
- let
- val thy = ProofContext.theory_of ctxt;
- val maxidx1 = Term.maxidx_of_typ T1;
- val T2' = Logic.incr_tvar (maxidx1 + 1) T2;
- val maxidx2 = Int.max (maxidx1, Term.maxidx_of_typ T2');
- in
- (Sign.typ_unify thy (T1, T2') (Vartab.empty, maxidx2); SOME c)
- handle Type.TUNIFY => NONE
- end;
-
-fun insert_internal_same ctxt t (Const (c, T)) =
- (case map_filter (unifiable_with ctxt T)
- (Same.function (get_variants (ProofContext.theory_of ctxt)) c) of
- [] => unresolved_err ctxt (c, T) t "no instances"
- | [c'] => Const (c', dummyT)
- | _ => raise Same.SAME)
- | insert_internal_same _ _ _ = raise Same.SAME;
-
-fun insert_external_same ctxt _ (Const (c, T)) =
- Const (Same.function (get_external (ProofContext.theory_of ctxt)) c, T)
- | insert_external_same _ _ _ = raise Same.SAME;
-
-fun gen_check_uncheck replace ts ctxt =
- Same.capture (Same.map (fn t => Term_Subst.map_aterms_same (replace ctxt t) t)) ts
- |> Option.map (rpair ctxt);
-
-val check = gen_check_uncheck insert_internal_same;
-fun uncheck ts ctxt =
- if !show_variants then NONE
- else gen_check_uncheck insert_external_same ts ctxt;
-
-fun reject_unresolved ts ctxt =
- let
- val thy = ProofContext.theory_of ctxt;
- fun check_unresolved t =
- case filter (is_overloaded thy o fst) (Term.add_consts t []) of
- [] => ()
- | ((c, T) :: _) => unresolved_err ctxt (c, T) t "multiple instances";
-
- val _ = map check_unresolved ts;
- in NONE end;
-
-
-(* setup *)
-
-val setup = Context.theory_map
- (Syntax.add_term_check 0 "adhoc_overloading" check
- #> Syntax.add_term_check 1 "adhoc_overloading_unresolved_check" reject_unresolved
- #> Syntax.add_term_uncheck 0 "adhoc_overloading" uncheck);
-
-end
--- a/src/HOL/SMT.thy Wed Jul 14 12:27:44 2010 +0200
+++ b/src/HOL/SMT.thy Wed Jul 14 14:16:12 2010 +0200
@@ -7,7 +7,6 @@
theory SMT
imports List
uses
- "~~/src/Tools/cache_io.ML"
("Tools/SMT/smt_monomorph.ML")
("Tools/SMT/smt_normalize.ML")
("Tools/SMT/smt_translate.ML")
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/Adhoc_Overloading.thy Wed Jul 14 14:16:12 2010 +0200
@@ -0,0 +1,15 @@
+(* Author: Alexander Krauss, TU Muenchen
+ Author: Christian Sternagel, University of Innsbruck
+*)
+
+header {* Ad-hoc overloading of constants based on their types *}
+
+theory Adhoc_Overloading
+imports Pure
+uses "adhoc_overloading.ML"
+begin
+
+setup Adhoc_Overloading.setup
+
+end
+
--- a/src/Tools/Code_Generator.thy Wed Jul 14 12:27:44 2010 +0200
+++ b/src/Tools/Code_Generator.thy Wed Jul 14 14:16:12 2010 +0200
@@ -7,6 +7,7 @@
theory Code_Generator
imports Pure
uses
+ "~~/src/Tools/cache_io.ML"
"~~/src/Tools/auto_solve.ML"
"~~/src/Tools/auto_counterexample.ML"
"~~/src/Tools/quickcheck.ML"
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/adhoc_overloading.ML Wed Jul 14 14:16:12 2010 +0200
@@ -0,0 +1,140 @@
+(* Author: Alexander Krauss, TU Muenchen
+ Author: Christian Sternagel, University of Innsbruck
+
+Ad-hoc overloading of constants based on their types.
+*)
+
+signature ADHOC_OVERLOADING =
+sig
+
+ val add_overloaded: string -> theory -> theory
+ val add_variant: string -> string -> theory -> theory
+
+ val show_variants: bool Unsynchronized.ref
+ val setup: theory -> theory
+
+end
+
+
+structure Adhoc_Overloading: ADHOC_OVERLOADING =
+struct
+
+val show_variants = Unsynchronized.ref false;
+
+
+(* errors *)
+
+fun duplicate_variant_err int_name ext_name =
+ error ("Constant " ^ quote int_name ^ " is already a variant of " ^ quote ext_name);
+
+fun not_overloaded_err name =
+ error ("Constant " ^ quote name ^ " is not declared as overloaded");
+
+fun already_overloaded_err name =
+ error ("Constant " ^ quote name ^ " is already declared as overloaded");
+
+fun unresolved_err ctxt (c, T) t reason =
+ error ("Unresolved overloading of " ^ quote c ^ " :: " ^
+ quote (Syntax.string_of_typ ctxt T) ^ " in " ^
+ quote (Syntax.string_of_term ctxt t) ^ " (" ^ reason ^ ")");
+
+
+(* theory data *)
+
+structure Overload_Data = Theory_Data
+(
+ type T =
+ { internalize : (string * typ) list Symtab.table,
+ externalize : string Symtab.table };
+ val empty = {internalize=Symtab.empty, externalize=Symtab.empty};
+ val extend = I;
+
+ fun merge_ext int_name (ext_name1, ext_name2) =
+ if ext_name1 = ext_name2 then ext_name1
+ else duplicate_variant_err int_name ext_name1;
+
+ fun merge ({internalize=int1, externalize=ext1},
+ {internalize=int2, externalize=ext2}) =
+ {internalize=Symtab.join (K (Library.merge (op =))) (int1, int2),
+ externalize=Symtab.join merge_ext (ext1, ext2)};
+);
+
+fun map_tables f g =
+ Overload_Data.map (fn {internalize=int, externalize=ext} =>
+ {internalize=f int, externalize=g ext});
+
+val is_overloaded = Symtab.defined o #internalize o Overload_Data.get;
+val get_variants = Symtab.lookup o #internalize o Overload_Data.get;
+val get_external = Symtab.lookup o #externalize o Overload_Data.get;
+
+fun add_overloaded ext_name thy =
+ let val _ = not (is_overloaded thy ext_name) orelse already_overloaded_err ext_name;
+ in map_tables (Symtab.update (ext_name, [])) I thy end;
+
+fun add_variant ext_name name thy =
+ let
+ val _ = is_overloaded thy ext_name orelse not_overloaded_err ext_name;
+ val _ = case get_external thy name of
+ NONE => ()
+ | SOME gen' => duplicate_variant_err name gen';
+ val T = Sign.the_const_type thy name;
+ in
+ map_tables (Symtab.cons_list (ext_name, (name, T)))
+ (Symtab.update (name, ext_name)) thy
+ end
+
+
+(* check / uncheck *)
+
+fun unifiable_with ctxt T1 (c, T2) =
+ let
+ val thy = ProofContext.theory_of ctxt;
+ val maxidx1 = Term.maxidx_of_typ T1;
+ val T2' = Logic.incr_tvar (maxidx1 + 1) T2;
+ val maxidx2 = Int.max (maxidx1, Term.maxidx_of_typ T2');
+ in
+ (Sign.typ_unify thy (T1, T2') (Vartab.empty, maxidx2); SOME c)
+ handle Type.TUNIFY => NONE
+ end;
+
+fun insert_internal_same ctxt t (Const (c, T)) =
+ (case map_filter (unifiable_with ctxt T)
+ (Same.function (get_variants (ProofContext.theory_of ctxt)) c) of
+ [] => unresolved_err ctxt (c, T) t "no instances"
+ | [c'] => Const (c', dummyT)
+ | _ => raise Same.SAME)
+ | insert_internal_same _ _ _ = raise Same.SAME;
+
+fun insert_external_same ctxt _ (Const (c, T)) =
+ Const (Same.function (get_external (ProofContext.theory_of ctxt)) c, T)
+ | insert_external_same _ _ _ = raise Same.SAME;
+
+fun gen_check_uncheck replace ts ctxt =
+ Same.capture (Same.map (fn t => Term_Subst.map_aterms_same (replace ctxt t) t)) ts
+ |> Option.map (rpair ctxt);
+
+val check = gen_check_uncheck insert_internal_same;
+fun uncheck ts ctxt =
+ if !show_variants then NONE
+ else gen_check_uncheck insert_external_same ts ctxt;
+
+fun reject_unresolved ts ctxt =
+ let
+ val thy = ProofContext.theory_of ctxt;
+ fun check_unresolved t =
+ case filter (is_overloaded thy o fst) (Term.add_consts t []) of
+ [] => ()
+ | ((c, T) :: _) => unresolved_err ctxt (c, T) t "multiple instances";
+
+ val _ = map check_unresolved ts;
+ in NONE end;
+
+
+(* setup *)
+
+val setup = Context.theory_map
+ (Syntax.add_term_check 0 "adhoc_overloading" check
+ #> Syntax.add_term_check 1 "adhoc_overloading_unresolved_check" reject_unresolved
+ #> Syntax.add_term_uncheck 0 "adhoc_overloading" uncheck);
+
+end