# HG changeset patch # User krauss # Date 1278972937 -7200 # Node ID 93f6dcf9ec02b239362a7792fa64f910e360b71f # Parent 261c61fabc9815bc266863d50b81076f30718878 generic ad-hoc overloading via check/uncheck diff -r 261c61fabc98 -r 93f6dcf9ec02 src/HOL/IsaMakefile --- a/src/HOL/IsaMakefile Tue Jul 13 11:38:04 2010 +0200 +++ b/src/HOL/IsaMakefile Tue Jul 13 00:15:37 2010 +0200 @@ -397,7 +397,7 @@ $(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/AssocList.thy \ + Library/Abstract_Rat.thy Library/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 \ @@ -434,8 +434,8 @@ 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/positivstellensatz.ML Library/reflection.ML \ - Library/reify_data.ML \ + Library/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 261c61fabc98 -r 93f6dcf9ec02 src/HOL/Library/Adhoc_Overloading.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Library/Adhoc_Overloading.thy Tue Jul 13 00:15:37 2010 +0200 @@ -0,0 +1,14 @@ +(* 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 261c61fabc98 -r 93f6dcf9ec02 src/HOL/Library/Library.thy --- a/src/HOL/Library/Library.thy Tue Jul 13 11:38:04 2010 +0200 +++ b/src/HOL/Library/Library.thy Tue Jul 13 00:15:37 2010 +0200 @@ -2,6 +2,7 @@ theory Library imports Abstract_Rat + Adhoc_Overloading AssocList BigO Binomial diff -r 261c61fabc98 -r 93f6dcf9ec02 src/HOL/Library/adhoc_overloading.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Library/adhoc_overloading.ML Tue Jul 13 00:15:37 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