# 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