merged

--- a/src/Pure/Isar/theory_target.ML	Wed Aug 11 13:30:24 2010 +0800
+++ b/src/Pure/Isar/theory_target.ML	Wed Aug 11 08:50:20 2010 +0200
@@ -107,20 +107,54 @@
   Local_Theory.target (Class_Target.refresh_syntax target);
 
 
-(* mixfix notation *)
+(* define *)
+
+fun syntax_error c = error ("Illegal mixfix syntax for overloaded constant " ^ quote c);
+
+fun theory_foundation (((b, U), mx), (b_def, rhs)) (type_params, term_params) lthy =
+  let
+    val (const, lthy2) = lthy |> Local_Theory.theory_result
+      (Sign.declare_const ((b, U), mx));
+    val lhs = list_comb (const, type_params @ term_params);
+    val ((_, def), lthy3) = lthy2 |> Local_Theory.theory_result
+      (Thm.add_def false false (b_def, Logic.mk_equals (lhs, rhs)));
+  in ((lhs, def), lthy3) end;
+
+fun locale_foundation ta (((b, U), mx), (b_def, rhs)) (type_params, term_params) =
+  theory_foundation (((b, U), NoSyn), (b_def, rhs)) (type_params, term_params)
+  #-> (fn (lhs, def) => locale_const_declaration ta Syntax.mode_default ((b, mx), lhs)
+    #> pair (lhs, def))
+
+fun class_foundation (ta as Target {target, ...})
+    (((b, U), mx), (b_def, rhs)) (type_params, term_params) =
+  theory_foundation (((b, U), NoSyn), (b_def, rhs)) (type_params, term_params)
+  #-> (fn (lhs, def) => locale_const_declaration ta Syntax.mode_default ((b, NoSyn), lhs)
+    #> class_target ta (Class_Target.declare target ((b, mx), (type_params, lhs)))
+    #> pair (lhs, def))
+
+fun instantiation_foundation (((b, U), mx), (b_def, rhs)) (type_params, term_params) lthy =
+  case Class_Target.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))
+          ||> Class_Target.confirm_declaration b
+    | NONE => lthy |>
+        theory_foundation (((b, U), mx), (b_def, rhs)) (type_params, term_params);
+
+fun overloading_foundation (((b, U), mx), (b_def, rhs)) (type_params, term_params) lthy =
+  case Overloading.operation lthy b
+   of SOME (c, checked) => if mx <> NoSyn then syntax_error c
+        else lthy |> Local_Theory.theory_result (Overloading.declare (c, U)
+            ##>> Overloading.define checked b_def (c, rhs))
+          ||> Overloading.confirm b
+    | NONE => lthy |>
+        theory_foundation (((b, U), mx), (b_def, rhs)) (type_params, term_params);
 
 fun fork_mixfix (Target {is_locale, is_class, ...}) mx =
   if not is_locale then (NoSyn, NoSyn, mx)
   else if not is_class then (NoSyn, mx, NoSyn)
   else (mx, NoSyn, NoSyn);
 
-
-(* define *)
-
-local
-
-fun syntax_error c = error ("Illegal mixfix syntax for overloaded constant " ^ quote c);
-
 fun foundation (ta as Target {target, is_locale, is_class, ...})
     (((b, U), mx), (b_def, rhs)) (type_params, term_params) lthy =
   let
@@ -155,12 +189,6 @@
           (Class_Target.declare target ((b, mx1), (type_params, lhs)))
   end;
 
-in
-
-fun define ta = Generic_Target.define (foundation ta);
-
-end;
-
 
 (* notes *)
 
@@ -185,9 +213,9 @@
     |> Local_Theory.target (Locale.add_thmss locale kind local_facts')
   end
 
-fun notes (Target {target, is_locale, ...}) =
-  Generic_Target.notes (if is_locale then locale_notes target
-    else fn kind => fn global_facts => fn _ => theory_notes kind global_facts);
+fun target_notes (ta as Target {target, is_locale, ...}) =
+  if is_locale then locale_notes target
+    else fn kind => fn global_facts => fn _ => theory_notes kind global_facts;
 
 
 (* abbrev *)
@@ -203,17 +231,12 @@
 
 fun target_abbrev (ta as Target {target, is_locale, is_class, ...})
     prmode (b, mx) (global_rhs, t') xs lthy =
-  let
-    val (mx1, mx2, mx3) = fork_mixfix ta mx;
-  in if is_locale
+  if is_locale
     then lthy
-      |> locale_abbrev ta prmode ((b, mx2), global_rhs) xs
-      |> is_class ? class_target ta (Class_Target.abbrev target prmode ((b, mx1), t'))
+      |> locale_abbrev ta prmode ((b, if is_class then NoSyn else mx), global_rhs) xs
+      |> is_class ? class_target ta (Class_Target.abbrev target prmode ((b, mx), t'))
     else lthy
-      |> theory_abbrev prmode ((b, mx3), global_rhs)
-  end;
-
-fun abbrev ta = Generic_Target.abbrev (target_abbrev ta);
+      |> theory_abbrev prmode ((b, mx), global_rhs);
 
 
 (* pretty *)
@@ -262,9 +285,9 @@
   |> init_data ta
   |> Data.put ta
   |> Local_Theory.init NONE (Long_Name.base_name target)
-     {define = define ta,
-      notes = notes ta,
-      abbrev = abbrev ta,
+     {define = Generic_Target.define (foundation ta),
+      notes = Generic_Target.notes (target_notes ta),
+      abbrev = Generic_Target.abbrev (target_abbrev ta),
       declaration = fn pervasive => target_declaration ta
         { syntax = false, pervasive = pervasive },
       syntax_declaration = fn pervasive => target_declaration ta
@@ -287,7 +310,22 @@
     val ctxt = ProofContext.init_global thy;
     val ops = raw_ops |> map (fn (name, const, checked) =>
       (name, Term.dest_Const (prep_const ctxt const), checked));
-  in thy |> init_target (make_target "" false false ([], [], []) ops) end;
+  in
+    thy
+    |> Overloading.init ops
+    |> Local_Theory.init NONE ""
+       {define = Generic_Target.define overloading_foundation,
+        notes = Generic_Target.notes
+          (fn kind => fn global_facts => fn _ => theory_notes kind global_facts),
+        abbrev = Generic_Target.abbrev
+          (fn prmode => fn (b, mx) => fn (t, _) => fn _ =>
+            theory_abbrev prmode ((b, mx), t)),
+        declaration = fn pervasive => theory_declaration,
+        syntax_declaration = fn pervasive => theory_declaration,
+        pretty = single o Overloading.pretty,
+        reinit = gen_overloading prep_const raw_ops o ProofContext.theory_of,
+        exit = Local_Theory.target_of o Overloading.conclude}
+  end;
 
 in
 
@@ -296,7 +334,21 @@
 fun context_cmd "-" thy = init NONE thy
   | context_cmd target thy = init (SOME (Locale.intern thy target)) thy;
 
-fun instantiation arities = init_target (make_target "" false false arities []);
+fun instantiation arities thy =
+  thy
+  |> Class_Target.init_instantiation arities
+  |> Local_Theory.init NONE ""
+     {define = Generic_Target.define instantiation_foundation,
+      notes = Generic_Target.notes
+        (fn kind => fn global_facts => fn _ => theory_notes kind global_facts),
+      abbrev = Generic_Target.abbrev
+        (fn prmode => fn (b, mx) => fn (t, _) => fn _ => theory_abbrev prmode ((b, mx), t)),
+      declaration = fn pervasive => theory_declaration,
+      syntax_declaration = fn pervasive => theory_declaration,
+      pretty = single o Class_Target.pretty_instantiation,
+      reinit = instantiation arities o ProofContext.theory_of,
+      exit = Local_Theory.target_of o Class_Target.conclude_instantiation};
+
 fun instantiation_cmd arities thy =
   instantiation (Class_Target.read_multi_arity thy arities) thy;