load cache_io before code generator; moved adhoc-overloading to generic tools
authorhaftmann
Wed Jul 14 14:16:12 2010 +0200 (2010-07-14)
changeset 37818dd65033fed78
parent 37817 71e5546b1965
child 37819 000049335247
load cache_io before code generator; moved adhoc-overloading to generic tools
src/HOL/IsaMakefile
src/HOL/Library/Adhoc_Overloading.thy
src/HOL/Library/Library.thy
src/HOL/Library/Monad_Syntax.thy
src/HOL/Library/adhoc_overloading.ML
src/HOL/SMT.thy
src/Tools/Adhoc_Overloading.thy
src/Tools/Code_Generator.thy
src/Tools/adhoc_overloading.ML
     1.1 --- a/src/HOL/IsaMakefile	Wed Jul 14 12:27:44 2010 +0200
     1.2 +++ b/src/HOL/IsaMakefile	Wed Jul 14 14:16:12 2010 +0200
     1.3 @@ -106,6 +106,7 @@
     1.4    $(SRC)/Provers/hypsubst.ML \
     1.5    $(SRC)/Provers/quantifier1.ML \
     1.6    $(SRC)/Provers/splitter.ML \
     1.7 +  $(SRC)/Tools/cache_io.ML \
     1.8    $(SRC)/Tools/Code/code_eval.ML \
     1.9    $(SRC)/Tools/Code/code_haskell.ML \
    1.10    $(SRC)/Tools/Code/code_ml.ML \
    1.11 @@ -266,7 +267,6 @@
    1.12    $(SRC)/Provers/Arith/cancel_numerals.ML \
    1.13    $(SRC)/Provers/Arith/combine_numerals.ML \
    1.14    $(SRC)/Provers/Arith/extract_common_term.ML \
    1.15 -  $(SRC)/Tools/cache_io.ML \
    1.16    $(SRC)/Tools/Metis/metis.ML \
    1.17    Tools/ATP_Manager/async_manager.ML \
    1.18    Tools/ATP_Manager/atp_manager.ML \
    1.19 @@ -397,7 +397,8 @@
    1.20  
    1.21  $(OUT)/HOL-Library: $(OUT)/HOL Library/HOL_Library_ROOT.ML		\
    1.22    $(SRC)/HOL/Tools/float_arith.ML $(SRC)/Tools/float.ML			\
    1.23 -  Library/Abstract_Rat.thy Library/Adhoc_Overloading.thy Library/AssocList.thy	\
    1.24 +  Library/Abstract_Rat.thy $(SRC)/Tools/Adhoc_Overloading.thy		\
    1.25 +  Library/AssocList.thy							\
    1.26    Library/BigO.thy Library/Binomial.thy Library/Bit.thy			\
    1.27    Library/Boolean_Algebra.thy Library/Cardinality.thy			\
    1.28    Library/Char_nat.thy Library/Code_Char.thy Library/Code_Char_chr.thy	\
    1.29 @@ -415,7 +416,8 @@
    1.30    Library/Lattice_Syntax.thy Library/Library.thy			\
    1.31    Library/List_Prefix.thy Library/List_lexord.thy Library/Mapping.thy	\
    1.32    Library/Monad_Syntax.thy Library/More_List.thy Library/More_Set.thy	\
    1.33 -  Library/Multiset.thy Library/Nat_Bijection.thy Library/Nat_Infinity.thy	\
    1.34 +  Library/Multiset.thy Library/Nat_Bijection.thy			\
    1.35 +  Library/Nat_Infinity.thy						\
    1.36    Library/Nested_Environment.thy Library/Numeral_Type.thy		\
    1.37    Library/OptionalSugar.thy Library/Order_Relation.thy			\
    1.38    Library/Permutation.thy Library/Permutations.thy			\
    1.39 @@ -434,7 +436,7 @@
    1.40    Library/Sum_Of_Squares/sum_of_squares.ML				\
    1.41    Library/Transitive_Closure_Table.thy Library/Univ_Poly.thy		\
    1.42    Library/While_Combinator.thy Library/Zorn.thy				\
    1.43 -  Library/adhoc_overloading.ML Library/positivstellensatz.ML		\
    1.44 +  $(SRC)/Tools/adhoc_overloading.ML Library/positivstellensatz.ML	\
    1.45    Library/reflection.ML Library/reify_data.ML				\
    1.46    Library/document/root.bib Library/document/root.tex
    1.47  	@cd Library; $(ISABELLE_TOOL) usedir -b -f HOL_Library_ROOT.ML $(OUT)/HOL HOL-Library
     2.1 --- a/src/HOL/Library/Adhoc_Overloading.thy	Wed Jul 14 12:27:44 2010 +0200
     2.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.3 @@ -1,14 +0,0 @@
     2.4 -(* Author: Alexander Krauss, TU Muenchen
     2.5 -   Author: Christian Sternagel, University of Innsbruck
     2.6 -*)
     2.7 -
     2.8 -header {* Ad-hoc overloading of constants based on their types *}
     2.9 -
    2.10 -theory Adhoc_Overloading
    2.11 -imports Main
    2.12 -uses "adhoc_overloading.ML"
    2.13 -begin
    2.14 -
    2.15 -setup Adhoc_Overloading.setup
    2.16 -
    2.17 -end
     3.1 --- a/src/HOL/Library/Library.thy	Wed Jul 14 12:27:44 2010 +0200
     3.2 +++ b/src/HOL/Library/Library.thy	Wed Jul 14 14:16:12 2010 +0200
     3.3 @@ -2,7 +2,6 @@
     3.4  theory Library
     3.5  imports
     3.6    Abstract_Rat
     3.7 -  Adhoc_Overloading
     3.8    AssocList
     3.9    BigO
    3.10    Binomial
     4.1 --- a/src/HOL/Library/Monad_Syntax.thy	Wed Jul 14 12:27:44 2010 +0200
     4.2 +++ b/src/HOL/Library/Monad_Syntax.thy	Wed Jul 14 14:16:12 2010 +0200
     4.3 @@ -5,7 +5,7 @@
     4.4  header {* Monad notation for arbitrary types *}
     4.5  
     4.6  theory Monad_Syntax
     4.7 -imports Adhoc_Overloading
     4.8 +imports "~~/src/Tools/Adhoc_Overloading"
     4.9  begin
    4.10  
    4.11  text {*
     5.1 --- a/src/HOL/Library/adhoc_overloading.ML	Wed Jul 14 12:27:44 2010 +0200
     5.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     5.3 @@ -1,140 +0,0 @@
     5.4 -(* Author: Alexander Krauss, TU Muenchen
     5.5 -   Author: Christian Sternagel, University of Innsbruck
     5.6 -
     5.7 -Ad-hoc overloading of constants based on their types.
     5.8 -*)
     5.9 -
    5.10 -signature ADHOC_OVERLOADING =
    5.11 -sig
    5.12 -
    5.13 -  val add_overloaded: string -> theory -> theory
    5.14 -  val add_variant: string -> string -> theory -> theory
    5.15 -
    5.16 -  val show_variants: bool Unsynchronized.ref
    5.17 -  val setup: theory -> theory
    5.18 -
    5.19 -end
    5.20 -
    5.21 -
    5.22 -structure Adhoc_Overloading: ADHOC_OVERLOADING =
    5.23 -struct
    5.24 -
    5.25 -val show_variants = Unsynchronized.ref false;
    5.26 -
    5.27 -
    5.28 -(* errors *)
    5.29 -
    5.30 -fun duplicate_variant_err int_name ext_name =
    5.31 -  error ("Constant " ^ quote int_name ^ " is already a variant of " ^ quote ext_name);
    5.32 -
    5.33 -fun not_overloaded_err name =
    5.34 -  error ("Constant " ^ quote name ^ " is not declared as overloaded");
    5.35 -
    5.36 -fun already_overloaded_err name =
    5.37 -  error ("Constant " ^ quote name ^ " is already declared as overloaded");
    5.38 -
    5.39 -fun unresolved_err ctxt (c, T) t reason =
    5.40 -  error ("Unresolved overloading of  " ^ quote c ^ " :: " ^
    5.41 -    quote (Syntax.string_of_typ ctxt T) ^ " in " ^
    5.42 -    quote (Syntax.string_of_term ctxt t) ^ " (" ^ reason ^ ")");
    5.43 -
    5.44 -
    5.45 -(* theory data *)
    5.46 -
    5.47 -structure Overload_Data = Theory_Data
    5.48 -(
    5.49 -  type T =
    5.50 -    { internalize : (string * typ) list Symtab.table,
    5.51 -      externalize : string Symtab.table };
    5.52 -  val empty = {internalize=Symtab.empty, externalize=Symtab.empty};
    5.53 -  val extend = I;
    5.54 -
    5.55 -  fun merge_ext int_name (ext_name1, ext_name2) =
    5.56 -    if ext_name1 = ext_name2 then ext_name1
    5.57 -    else duplicate_variant_err int_name ext_name1;
    5.58 -
    5.59 -  fun merge ({internalize=int1, externalize=ext1},
    5.60 -      {internalize=int2, externalize=ext2}) =
    5.61 -    {internalize=Symtab.join (K (Library.merge (op =))) (int1, int2),
    5.62 -     externalize=Symtab.join merge_ext (ext1, ext2)};
    5.63 -);
    5.64 -
    5.65 -fun map_tables f g =
    5.66 -  Overload_Data.map (fn {internalize=int, externalize=ext} =>
    5.67 -    {internalize=f int, externalize=g ext});
    5.68 -
    5.69 -val is_overloaded = Symtab.defined o #internalize o Overload_Data.get;
    5.70 -val get_variants = Symtab.lookup o #internalize o Overload_Data.get;
    5.71 -val get_external = Symtab.lookup o #externalize o Overload_Data.get;
    5.72 -
    5.73 -fun add_overloaded ext_name thy =
    5.74 -  let val _ = not (is_overloaded thy ext_name) orelse already_overloaded_err ext_name;
    5.75 -  in map_tables (Symtab.update (ext_name, [])) I thy end;
    5.76 -
    5.77 -fun add_variant ext_name name thy =
    5.78 -  let
    5.79 -    val _ = is_overloaded thy ext_name orelse not_overloaded_err ext_name;
    5.80 -    val _ = case get_external thy name of
    5.81 -              NONE => ()
    5.82 -            | SOME gen' => duplicate_variant_err name gen';
    5.83 -    val T = Sign.the_const_type thy name;
    5.84 -  in
    5.85 -    map_tables (Symtab.cons_list (ext_name, (name, T)))
    5.86 -      (Symtab.update (name, ext_name)) thy    
    5.87 -  end
    5.88 -
    5.89 -
    5.90 -(* check / uncheck *)
    5.91 -
    5.92 -fun unifiable_with ctxt T1 (c, T2) =
    5.93 -  let
    5.94 -    val thy = ProofContext.theory_of ctxt;
    5.95 -    val maxidx1 = Term.maxidx_of_typ T1;
    5.96 -    val T2' = Logic.incr_tvar (maxidx1 + 1) T2;
    5.97 -    val maxidx2 = Int.max (maxidx1, Term.maxidx_of_typ T2');
    5.98 -  in
    5.99 -    (Sign.typ_unify thy (T1, T2') (Vartab.empty, maxidx2); SOME c)
   5.100 -    handle Type.TUNIFY => NONE
   5.101 -  end;
   5.102 -
   5.103 -fun insert_internal_same ctxt t (Const (c, T)) =
   5.104 -  (case map_filter (unifiable_with ctxt T) 
   5.105 -     (Same.function (get_variants (ProofContext.theory_of ctxt)) c) of
   5.106 -      [] => unresolved_err ctxt (c, T) t "no instances"
   5.107 -    | [c'] => Const (c', dummyT)
   5.108 -    | _ => raise Same.SAME)
   5.109 -  | insert_internal_same _ _ _ = raise Same.SAME;
   5.110 -
   5.111 -fun insert_external_same ctxt _ (Const (c, T)) =
   5.112 -    Const (Same.function (get_external (ProofContext.theory_of ctxt)) c, T)
   5.113 -  | insert_external_same _ _ _ = raise Same.SAME;
   5.114 -
   5.115 -fun gen_check_uncheck replace ts ctxt =
   5.116 -  Same.capture (Same.map (fn t => Term_Subst.map_aterms_same (replace ctxt t) t)) ts
   5.117 -  |> Option.map (rpair ctxt);
   5.118 -
   5.119 -val check = gen_check_uncheck insert_internal_same;
   5.120 -fun uncheck ts ctxt = 
   5.121 -  if !show_variants then NONE
   5.122 -  else gen_check_uncheck insert_external_same ts ctxt;
   5.123 -
   5.124 -fun reject_unresolved ts ctxt =
   5.125 -  let
   5.126 -    val thy = ProofContext.theory_of ctxt;
   5.127 -    fun check_unresolved t =
   5.128 -      case filter (is_overloaded thy o fst) (Term.add_consts t []) of
   5.129 -          [] => ()
   5.130 -        | ((c, T) :: _) => unresolved_err ctxt (c, T) t "multiple instances";
   5.131 -
   5.132 -    val _ = map check_unresolved ts;
   5.133 -  in NONE end;
   5.134 -
   5.135 -
   5.136 -(* setup *)
   5.137 -
   5.138 -val setup = Context.theory_map 
   5.139 -  (Syntax.add_term_check 0 "adhoc_overloading" check
   5.140 -   #> Syntax.add_term_check 1 "adhoc_overloading_unresolved_check" reject_unresolved
   5.141 -   #> Syntax.add_term_uncheck 0 "adhoc_overloading" uncheck);
   5.142 -
   5.143 -end
     6.1 --- a/src/HOL/SMT.thy	Wed Jul 14 12:27:44 2010 +0200
     6.2 +++ b/src/HOL/SMT.thy	Wed Jul 14 14:16:12 2010 +0200
     6.3 @@ -7,7 +7,6 @@
     6.4  theory SMT
     6.5  imports List
     6.6  uses
     6.7 -  "~~/src/Tools/cache_io.ML"
     6.8    ("Tools/SMT/smt_monomorph.ML")
     6.9    ("Tools/SMT/smt_normalize.ML")
    6.10    ("Tools/SMT/smt_translate.ML")
     7.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     7.2 +++ b/src/Tools/Adhoc_Overloading.thy	Wed Jul 14 14:16:12 2010 +0200
     7.3 @@ -0,0 +1,15 @@
     7.4 +(* Author: Alexander Krauss, TU Muenchen
     7.5 +   Author: Christian Sternagel, University of Innsbruck
     7.6 +*)
     7.7 +
     7.8 +header {* Ad-hoc overloading of constants based on their types *}
     7.9 +
    7.10 +theory Adhoc_Overloading
    7.11 +imports Pure
    7.12 +uses "adhoc_overloading.ML"
    7.13 +begin
    7.14 +
    7.15 +setup Adhoc_Overloading.setup
    7.16 +
    7.17 +end
    7.18 +
     8.1 --- a/src/Tools/Code_Generator.thy	Wed Jul 14 12:27:44 2010 +0200
     8.2 +++ b/src/Tools/Code_Generator.thy	Wed Jul 14 14:16:12 2010 +0200
     8.3 @@ -7,6 +7,7 @@
     8.4  theory Code_Generator
     8.5  imports Pure
     8.6  uses
     8.7 +  "~~/src/Tools/cache_io.ML"
     8.8    "~~/src/Tools/auto_solve.ML"
     8.9    "~~/src/Tools/auto_counterexample.ML"
    8.10    "~~/src/Tools/quickcheck.ML"
     9.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     9.2 +++ b/src/Tools/adhoc_overloading.ML	Wed Jul 14 14:16:12 2010 +0200
     9.3 @@ -0,0 +1,140 @@
     9.4 +(* Author: Alexander Krauss, TU Muenchen
     9.5 +   Author: Christian Sternagel, University of Innsbruck
     9.6 +
     9.7 +Ad-hoc overloading of constants based on their types.
     9.8 +*)
     9.9 +
    9.10 +signature ADHOC_OVERLOADING =
    9.11 +sig
    9.12 +
    9.13 +  val add_overloaded: string -> theory -> theory
    9.14 +  val add_variant: string -> string -> theory -> theory
    9.15 +
    9.16 +  val show_variants: bool Unsynchronized.ref
    9.17 +  val setup: theory -> theory
    9.18 +
    9.19 +end
    9.20 +
    9.21 +
    9.22 +structure Adhoc_Overloading: ADHOC_OVERLOADING =
    9.23 +struct
    9.24 +
    9.25 +val show_variants = Unsynchronized.ref false;
    9.26 +
    9.27 +
    9.28 +(* errors *)
    9.29 +
    9.30 +fun duplicate_variant_err int_name ext_name =
    9.31 +  error ("Constant " ^ quote int_name ^ " is already a variant of " ^ quote ext_name);
    9.32 +
    9.33 +fun not_overloaded_err name =
    9.34 +  error ("Constant " ^ quote name ^ " is not declared as overloaded");
    9.35 +
    9.36 +fun already_overloaded_err name =
    9.37 +  error ("Constant " ^ quote name ^ " is already declared as overloaded");
    9.38 +
    9.39 +fun unresolved_err ctxt (c, T) t reason =
    9.40 +  error ("Unresolved overloading of  " ^ quote c ^ " :: " ^
    9.41 +    quote (Syntax.string_of_typ ctxt T) ^ " in " ^
    9.42 +    quote (Syntax.string_of_term ctxt t) ^ " (" ^ reason ^ ")");
    9.43 +
    9.44 +
    9.45 +(* theory data *)
    9.46 +
    9.47 +structure Overload_Data = Theory_Data
    9.48 +(
    9.49 +  type T =
    9.50 +    { internalize : (string * typ) list Symtab.table,
    9.51 +      externalize : string Symtab.table };
    9.52 +  val empty = {internalize=Symtab.empty, externalize=Symtab.empty};
    9.53 +  val extend = I;
    9.54 +
    9.55 +  fun merge_ext int_name (ext_name1, ext_name2) =
    9.56 +    if ext_name1 = ext_name2 then ext_name1
    9.57 +    else duplicate_variant_err int_name ext_name1;
    9.58 +
    9.59 +  fun merge ({internalize=int1, externalize=ext1},
    9.60 +      {internalize=int2, externalize=ext2}) =
    9.61 +    {internalize=Symtab.join (K (Library.merge (op =))) (int1, int2),
    9.62 +     externalize=Symtab.join merge_ext (ext1, ext2)};
    9.63 +);
    9.64 +
    9.65 +fun map_tables f g =
    9.66 +  Overload_Data.map (fn {internalize=int, externalize=ext} =>
    9.67 +    {internalize=f int, externalize=g ext});
    9.68 +
    9.69 +val is_overloaded = Symtab.defined o #internalize o Overload_Data.get;
    9.70 +val get_variants = Symtab.lookup o #internalize o Overload_Data.get;
    9.71 +val get_external = Symtab.lookup o #externalize o Overload_Data.get;
    9.72 +
    9.73 +fun add_overloaded ext_name thy =
    9.74 +  let val _ = not (is_overloaded thy ext_name) orelse already_overloaded_err ext_name;
    9.75 +  in map_tables (Symtab.update (ext_name, [])) I thy end;
    9.76 +
    9.77 +fun add_variant ext_name name thy =
    9.78 +  let
    9.79 +    val _ = is_overloaded thy ext_name orelse not_overloaded_err ext_name;
    9.80 +    val _ = case get_external thy name of
    9.81 +              NONE => ()
    9.82 +            | SOME gen' => duplicate_variant_err name gen';
    9.83 +    val T = Sign.the_const_type thy name;
    9.84 +  in
    9.85 +    map_tables (Symtab.cons_list (ext_name, (name, T)))
    9.86 +      (Symtab.update (name, ext_name)) thy    
    9.87 +  end
    9.88 +
    9.89 +
    9.90 +(* check / uncheck *)
    9.91 +
    9.92 +fun unifiable_with ctxt T1 (c, T2) =
    9.93 +  let
    9.94 +    val thy = ProofContext.theory_of ctxt;
    9.95 +    val maxidx1 = Term.maxidx_of_typ T1;
    9.96 +    val T2' = Logic.incr_tvar (maxidx1 + 1) T2;
    9.97 +    val maxidx2 = Int.max (maxidx1, Term.maxidx_of_typ T2');
    9.98 +  in
    9.99 +    (Sign.typ_unify thy (T1, T2') (Vartab.empty, maxidx2); SOME c)
   9.100 +    handle Type.TUNIFY => NONE
   9.101 +  end;
   9.102 +
   9.103 +fun insert_internal_same ctxt t (Const (c, T)) =
   9.104 +  (case map_filter (unifiable_with ctxt T) 
   9.105 +     (Same.function (get_variants (ProofContext.theory_of ctxt)) c) of
   9.106 +      [] => unresolved_err ctxt (c, T) t "no instances"
   9.107 +    | [c'] => Const (c', dummyT)
   9.108 +    | _ => raise Same.SAME)
   9.109 +  | insert_internal_same _ _ _ = raise Same.SAME;
   9.110 +
   9.111 +fun insert_external_same ctxt _ (Const (c, T)) =
   9.112 +    Const (Same.function (get_external (ProofContext.theory_of ctxt)) c, T)
   9.113 +  | insert_external_same _ _ _ = raise Same.SAME;
   9.114 +
   9.115 +fun gen_check_uncheck replace ts ctxt =
   9.116 +  Same.capture (Same.map (fn t => Term_Subst.map_aterms_same (replace ctxt t) t)) ts
   9.117 +  |> Option.map (rpair ctxt);
   9.118 +
   9.119 +val check = gen_check_uncheck insert_internal_same;
   9.120 +fun uncheck ts ctxt = 
   9.121 +  if !show_variants then NONE
   9.122 +  else gen_check_uncheck insert_external_same ts ctxt;
   9.123 +
   9.124 +fun reject_unresolved ts ctxt =
   9.125 +  let
   9.126 +    val thy = ProofContext.theory_of ctxt;
   9.127 +    fun check_unresolved t =
   9.128 +      case filter (is_overloaded thy o fst) (Term.add_consts t []) of
   9.129 +          [] => ()
   9.130 +        | ((c, T) :: _) => unresolved_err ctxt (c, T) t "multiple instances";
   9.131 +
   9.132 +    val _ = map check_unresolved ts;
   9.133 +  in NONE end;
   9.134 +
   9.135 +
   9.136 +(* setup *)
   9.137 +
   9.138 +val setup = Context.theory_map 
   9.139 +  (Syntax.add_term_check 0 "adhoc_overloading" check
   9.140 +   #> Syntax.add_term_check 1 "adhoc_overloading_unresolved_check" reject_unresolved
   9.141 +   #> Syntax.add_term_uncheck 0 "adhoc_overloading" uncheck);
   9.142 +
   9.143 +end