# HG changeset patch # User haftmann # Date 1279109772 -7200 # Node ID dd65033fed78dbaa892b206b3363532bacabfc62 # Parent 71e5546b19659497ee6f637cbe7ffdb1369cc54c load cache_io before code generator; moved adhoc-overloading to generic tools diff -r 71e5546b1965 -r dd65033fed78 src/HOL/IsaMakefile --- 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 diff -r 71e5546b1965 -r dd65033fed78 src/HOL/Library/Adhoc_Overloading.thy --- 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 diff -r 71e5546b1965 -r dd65033fed78 src/HOL/Library/Library.thy --- 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 diff -r 71e5546b1965 -r dd65033fed78 src/HOL/Library/Monad_Syntax.thy --- 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 {* diff -r 71e5546b1965 -r dd65033fed78 src/HOL/Library/adhoc_overloading.ML --- 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 diff -r 71e5546b1965 -r dd65033fed78 src/HOL/SMT.thy --- 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") diff -r 71e5546b1965 -r dd65033fed78 src/Tools/Adhoc_Overloading.thy --- /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 + diff -r 71e5546b1965 -r dd65033fed78 src/Tools/Code_Generator.thy --- 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" diff -r 71e5546b1965 -r dd65033fed78 src/Tools/adhoc_overloading.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