# HG changeset patch
# User haftmann
# Date 1281542372 -7200
# Node ID 8b02c5bf1d0e44fb8e9d54c1ab9af43fcf97c836
# Parent  7d1e2a6831ecd88a8feaf76cbe9f73095a2472f5
tuned internal structure

diff -r 7d1e2a6831ec -r 8b02c5bf1d0e src/Pure/Isar/class.ML
--- a/src/Pure/Isar/class.ML	Wed Aug 11 17:19:27 2010 +0200
+++ b/src/Pure/Isar/class.ML	Wed Aug 11 17:59:32 2010 +0200
@@ -441,6 +441,19 @@
             (((primary_constraints, []), (((improve, subst), false), unchecks)), false))
   end;
 
+fun resort_terms pp algebra consts constraints ts =
+  let
+    fun matchings (Const (c_ty as (c, _))) = (case constraints c
+         of NONE => I
+          | SOME sorts => fold2 (curry (Sorts.meet_sort algebra))
+              (Consts.typargs consts c_ty) sorts)
+      | matchings _ = I
+    val tvartab = (fold o fold_aterms) matchings ts Vartab.empty
+      handle Sorts.CLASS_ERROR e => error (Sorts.class_error pp e);
+    val inst = map_type_tvar
+      (fn (vi, sort) => TVar (vi, the_default sort (Vartab.lookup tvartab vi)));
+  in if Vartab.is_empty tvartab then NONE else SOME ((map o map_types) inst ts) end;
+
 
 (* target *)
 
@@ -461,20 +474,39 @@
 
 val type_name = sanitize_name o Long_Name.base_name;
 
-fun resort_terms pp algebra consts constraints ts =
+fun define_overloaded (c, U) v (b_def, rhs) = Local_Theory.theory_result
+    (AxClass.declare_overloaded (c, U) ##>> AxClass.define_overloaded b_def (c, rhs))
+  ##> (map_instantiation o apsnd) (filter_out (fn (_, (v', _)) => v' = v))
+  ##> Local_Theory.target synchronize_inst_syntax;
+
+fun foundation (((b, U), mx), (b_def, rhs)) (type_params, term_params) lthy =
+  case instantiation_param lthy b
+   of SOME c => if mx <> NoSyn then error ("Illegal mixfix syntax for overloaded constant " ^ quote c)
+        else lthy |> define_overloaded (c, U) (Binding.name_of b) (b_def, rhs)
+    | NONE => lthy |>
+        Generic_Target.theory_foundation (((b, U), mx), (b_def, rhs)) (type_params, term_params);
+
+fun pretty lthy =
   let
-    fun matchings (Const (c_ty as (c, _))) = (case constraints c
-         of NONE => I
-          | SOME sorts => fold2 (curry (Sorts.meet_sort algebra))
-              (Consts.typargs consts c_ty) sorts)
-      | matchings _ = I
-    val tvartab = (fold o fold_aterms) matchings ts Vartab.empty
-      handle Sorts.CLASS_ERROR e => error (Sorts.class_error pp e);
-    val inst = map_type_tvar
-      (fn (vi, sort) => TVar (vi, the_default sort (Vartab.lookup tvartab vi)));
-  in if Vartab.is_empty tvartab then NONE else SOME ((map o map_types) inst ts) end;
+    val { arities = (tycos, vs, sort), params } = the_instantiation lthy;
+    val thy = ProofContext.theory_of lthy;
+    fun pr_arity tyco = Syntax.pretty_arity lthy (tyco, map snd vs, sort);
+    fun pr_param ((c, _), (v, ty)) =
+      (Pretty.block o Pretty.breaks) [Pretty.str v, Pretty.str "==",
+        (Pretty.str o Sign.extern_const thy) c, Pretty.str "::", Syntax.pretty_typ_global thy ty];
+  in Pretty.str "instantiation" :: map pr_arity tycos @ map pr_param params end;
 
-fun init_instantiation (tycos, vs, sort) thy =
+fun conclude lthy =
+  let
+    val (tycos, vs, sort) = (#arities o the_instantiation) lthy;
+    val thy = ProofContext.theory_of lthy;
+    val _ = map (fn tyco => if Sign.of_sort thy
+        (Type (tyco, map TFree vs), sort)
+      then () else error ("Missing instance proof for type " ^ quote (Sign.extern_type thy tyco)))
+        tycos;
+  in lthy end;
+
+fun instantiation (tycos, vs, sort) thy =
   let
     val _ = if null tycos then error "At least one arity must be given" else ();
     val class_params = these_params thy (filter (can (AxClass.get_info thy)) sort);
@@ -512,11 +544,20 @@
     |> Overloading.add_improvable_syntax
     |> Context.proof_map (Syntax.add_term_check 0 "resorting" resort_check)
     |> synchronize_inst_syntax
+    |> Local_Theory.init NONE ""
+       {define = Generic_Target.define foundation,
+        notes = Generic_Target.notes
+          (fn kind => fn global_facts => fn _ => Generic_Target.theory_notes kind global_facts),
+        abbrev = Generic_Target.abbrev
+          (fn prmode => fn (b, mx) => fn (t, _) => fn _ => Generic_Target.theory_abbrev prmode ((b, mx), t)),
+        declaration = K Generic_Target.theory_declaration,
+        syntax_declaration = K Generic_Target.theory_declaration,
+        pretty = pretty,
+        exit = Local_Theory.target_of o conclude}
   end;
 
-fun confirm_declaration b = (map_instantiation o apsnd)
-  (filter_out (fn (_, (c', _)) => c' = Binding.name_of b))
-  #> Local_Theory.target synchronize_inst_syntax
+fun instantiation_cmd arities thy =
+  instantiation (read_multi_arity thy arities) thy;
 
 fun gen_instantiation_instance do_proof after_qed lthy =
   let
@@ -551,57 +592,6 @@
     |> pair y
   end;
 
-fun conclude_instantiation lthy =
-  let
-    val (tycos, vs, sort) = (#arities o the_instantiation) lthy;
-    val thy = ProofContext.theory_of lthy;
-    val _ = map (fn tyco => if Sign.of_sort thy
-        (Type (tyco, map TFree vs), sort)
-      then () else error ("Missing instance proof for type " ^ quote (Sign.extern_type thy tyco)))
-        tycos;
-  in lthy end;
-
-fun pretty_instantiation lthy =
-  let
-    val { arities = (tycos, vs, sort), params } = the_instantiation lthy;
-    val thy = ProofContext.theory_of lthy;
-    fun pr_arity tyco = Syntax.pretty_arity lthy (tyco, map snd vs, sort);
-    fun pr_param ((c, _), (v, ty)) =
-      (Pretty.block o Pretty.breaks) [Pretty.str v, Pretty.str "==",
-        (Pretty.str o Sign.extern_const thy) c, Pretty.str "::", Syntax.pretty_typ_global thy ty];
-  in
-    (Pretty.block o Pretty.fbreaks)
-      (Pretty.str "instantiation" :: map pr_arity tycos @ map pr_param params)
-  end;
-
-fun syntax_error c = error ("Illegal mixfix syntax for overloaded constant " ^ quote c);
-
-fun instantiation_foundation (((b, U), mx), (b_def, rhs)) (type_params, term_params) lthy =
-  case instantiation_param lthy b
-   of SOME c => if mx <> NoSyn then syntax_error c
-        else lthy |> Local_Theory.theory_result (AxClass.declare_overloaded (c, U)
-            ##>> AxClass.define_overloaded b_def (c, rhs))
-          ||> confirm_declaration b
-    | NONE => lthy |>
-        Generic_Target.theory_foundation (((b, U), mx), (b_def, rhs)) (type_params, term_params);
-
-fun instantiation arities thy =
-  thy
-  |> init_instantiation arities
-  |> Local_Theory.init NONE ""
-     {define = Generic_Target.define instantiation_foundation,
-      notes = Generic_Target.notes
-        (fn kind => fn global_facts => fn _ => Generic_Target.theory_notes kind global_facts),
-      abbrev = Generic_Target.abbrev
-        (fn prmode => fn (b, mx) => fn (t, _) => fn _ => Generic_Target.theory_abbrev prmode ((b, mx), t)),
-      declaration = K Generic_Target.theory_declaration,
-      syntax_declaration = K Generic_Target.theory_declaration,
-      pretty = single o pretty_instantiation,
-      exit = Local_Theory.target_of o conclude_instantiation};
-
-fun instantiation_cmd arities thy =
-  instantiation (read_multi_arity thy arities) thy;
-
 
 (* simplified instantiation interface with no class parameter *)
 
diff -r 7d1e2a6831ec -r 8b02c5bf1d0e src/Pure/Isar/overloading.ML
--- a/src/Pure/Isar/overloading.ML	Wed Aug 11 17:19:27 2010 +0200
+++ b/src/Pure/Isar/overloading.ML	Wed Aug 11 17:59:32 2010 +0200
@@ -113,27 +113,22 @@
 
 (** overloading target **)
 
-(* bookkeeping *)
-
-structure OverloadingData = Proof_Data
+structure Data = Proof_Data
 (
   type T = ((string * typ) * (string * bool)) list;
   fun init _ = [];
 );
 
-val get_overloading = OverloadingData.get o Local_Theory.target_of;
-val map_overloading = Local_Theory.target o OverloadingData.map;
+val get_overloading = Data.get o Local_Theory.target_of;
+val map_overloading = Local_Theory.target o Data.map;
 
 fun operation lthy b = get_overloading lthy
   |> get_first (fn ((c, _), (v, checked)) =>
-      if Binding.name_of b = v then SOME (c, checked) else NONE);
-
-
-(* target *)
+      if Binding.name_of b = v then SOME (c, (v, checked)) else NONE);
 
 fun synchronize_syntax ctxt =
   let
-    val overloading = OverloadingData.get ctxt;
+    val overloading = Data.get ctxt;
     fun subst (c, ty) = case AList.lookup (op =) overloading (c, ty)
      of SOME (v, _) => SOME (ty, Free (v, ty))
       | NONE => NONE;
@@ -144,38 +139,20 @@
     |> map_improvable_syntax (K ((([], []), (((K NONE, subst), false), unchecks)), false))
   end
 
-fun init raw_overloading thy =
-  let
-    val _ = if null raw_overloading then error "At least one parameter must be given" else ();
-    val overloading = map (fn (v, c_ty, checked) => (c_ty, (v, checked))) raw_overloading;
-  in
-    thy
-    |> Theory.checkpoint
-    |> ProofContext.init_global
-    |> OverloadingData.put overloading
-    |> fold (fn ((_, ty), (v, _)) => Variable.declare_names (Free (v, ty))) overloading
-    |> add_improvable_syntax
-    |> synchronize_syntax
-  end;
-
-fun declare c_ty = pair (Const c_ty);
+fun define_overloaded (c, U) (v, checked) (b_def, rhs) =
+  Local_Theory.theory_result
+    (Thm.add_def (not checked) true (b_def, Logic.mk_equals (Const (c, Term.fastype_of rhs), rhs)))
+  ##> map_overloading (filter_out (fn (_, (v', _)) => v' = v))
+  ##> Local_Theory.target synchronize_syntax
+  #-> (fn (_, def) => pair (Const (c, U), def))
 
-fun define checked b (c, t) =
-  Thm.add_def (not checked) true (b, Logic.mk_equals (Const (c, Term.fastype_of t), t))
-  #>> snd;
-
-fun confirm b = map_overloading (filter_out (fn (_, (c', _)) => c' = Binding.name_of b))
-  #> Local_Theory.target synchronize_syntax
-
-fun conclude lthy =
-  let
-    val overloading = get_overloading lthy;
-    val _ = if null overloading then () else
-      error ("Missing definition(s) for parameter(s) " ^ commas (map (quote
-        o Syntax.string_of_term lthy o Const o fst) overloading));
-  in
-    lthy
-  end;
+fun foundation (((b, U), mx), (b_def, rhs)) (type_params, term_params) lthy =
+  case operation lthy b
+   of SOME (c, (v, checked)) => if mx <> NoSyn
+       then error ("Illegal mixfix syntax for overloaded constant " ^ quote c)
+        else lthy |> define_overloaded (c, U) (v, checked) (b_def, rhs)
+    | NONE => lthy |>
+        Generic_Target.theory_foundation (((b, U), mx), (b_def, rhs)) (type_params, term_params);
 
 fun pretty lthy =
   let
@@ -184,32 +161,32 @@
     fun pr_operation ((c, ty), (v, _)) =
       (Pretty.block o Pretty.breaks) [Pretty.str v, Pretty.str "==",
         Pretty.str (Sign.extern_const thy c), Pretty.str "::", Syntax.pretty_typ lthy ty];
-  in
-    (Pretty.block o Pretty.fbreaks)
-      (Pretty.str "overloading" :: map pr_operation overloading)
-  end;
-
-fun syntax_error c = error ("Illegal mixfix syntax for overloaded constant " ^ quote c);
+  in Pretty.str "overloading" :: map pr_operation overloading end;
 
-fun overloading_foundation (((b, U), mx), (b_def, rhs)) (type_params, term_params) lthy =
-  case operation lthy b
-   of SOME (c, checked) => if mx <> NoSyn then syntax_error c
-        else lthy |> Local_Theory.theory_result (declare (c, U)
-            ##>> define checked b_def (c, rhs))
-          ||> confirm b
-    | NONE => lthy |>
-        Generic_Target.theory_foundation (((b, U), mx), (b_def, rhs)) (type_params, term_params);
+fun conclude lthy =
+  let
+    val overloading = get_overloading lthy;
+    val _ = if null overloading then () else
+      error ("Missing definition(s) for parameter(s) " ^ commas (map (quote
+        o Syntax.string_of_term lthy o Const o fst) overloading));
+  in lthy end;
 
-fun gen_overloading prep_const raw_ops thy =
+fun gen_overloading prep_const raw_overloading thy =
   let
     val ctxt = ProofContext.init_global thy;
-    val ops = raw_ops |> map (fn (name, const, checked) =>
-      (name, Term.dest_Const (prep_const ctxt const), checked));
+    val _ = if null raw_overloading then error "At least one parameter must be given" else ();
+    val overloading = raw_overloading |> map (fn (v, const, checked) =>
+      (Term.dest_Const (prep_const ctxt const), (v, checked)));
   in
     thy
-    |> init ops
+    |> Theory.checkpoint
+    |> ProofContext.init_global
+    |> Data.put overloading
+    |> fold (fn ((_, ty), (v, _)) => Variable.declare_names (Free (v, ty))) overloading
+    |> add_improvable_syntax
+    |> synchronize_syntax
     |> Local_Theory.init NONE ""
-       {define = Generic_Target.define overloading_foundation,
+       {define = Generic_Target.define foundation,
         notes = Generic_Target.notes
           (fn kind => fn global_facts => fn _ => Generic_Target.theory_notes kind global_facts),
         abbrev = Generic_Target.abbrev
@@ -217,7 +194,7 @@
             Generic_Target.theory_abbrev prmode ((b, mx), t)),
         declaration = K Generic_Target.theory_declaration,
         syntax_declaration = K Generic_Target.theory_declaration,
-        pretty = single o pretty,
+        pretty = pretty,
         exit = Local_Theory.target_of o conclude}
   end;