# HG changeset patch
# User wenzelm
# Date 1196264664 -3600
# Node ID 1c9b3733f887f84f818cb8fe1bbe19680ca584c0
# Parent  0a779502be5731cc6479da74df26856d54abd260
added base_sort;
added typedecl, dependent on base_sort (cf. intermediate typedecl.ML and former sign.ML, HOL/Tools/typedef_package.ML);
typedecl: recovered proper use of Syntax.type_name;

diff -r 0a779502be57 -r 1c9b3733f887 src/Pure/Isar/object_logic.ML
--- a/src/Pure/Isar/object_logic.ML	Wed Nov 28 16:44:22 2007 +0100
+++ b/src/Pure/Isar/object_logic.ML	Wed Nov 28 16:44:24 2007 +0100
@@ -7,6 +7,9 @@
 
 signature OBJECT_LOGIC =
 sig
+  val get_base_sort: theory -> sort option
+  val add_base_sort: sort -> theory -> theory
+  val typedecl: bstring * string list * mixfix -> theory -> typ * theory
   val add_judgment: bstring * string * mixfix -> theory -> theory
   val add_judgment_i: bstring * typ * mixfix -> theory -> theory
   val judgment_name: theory -> string
@@ -35,42 +38,82 @@
 structure ObjectLogic: OBJECT_LOGIC =
 struct
 
+(** theory data **)
 
-(** theory data **)
+datatype data = Data of
+ {base_sort: sort option,
+  judgment: string option,
+  atomize_rulify: thm list * thm list};
+
+fun make_data (base_sort, judgment, atomize_rulify) =
+  Data {base_sort = base_sort, judgment = judgment, atomize_rulify = atomize_rulify};
 
 structure ObjectLogicData = TheoryDataFun
 (
-  type T = string option * (thm list * thm list);
-  val empty = (NONE, ([], []));
+  type T = data;
+  val empty = make_data (NONE, NONE, ([], []));
   val copy = I;
   val extend = I;
 
-  fun merge_judgment (SOME x, SOME y) =
-        if (x: string) = y then SOME x else error "Attempt to merge different object-logics"
-    | merge_judgment (j1, j2) = if is_some j1 then j1 else j2;
+  fun merge_opt eq (SOME x, SOME y) =
+        if eq (x, y) then SOME x else error "Attempt to merge different object-logics"
+    | merge_opt _ (x, y) = if is_some x then x else y;
 
-  fun merge _ ((judgment1, (atomize1, rulify1)), (judgment2, (atomize2, rulify2))) =
-    (merge_judgment (judgment1, judgment2),
+  fun merge _
+     (Data {base_sort = base_sort1, judgment = judgment1, atomize_rulify = (atomize1, rulify1)},
+      Data {base_sort = base_sort2, judgment = judgment2, atomize_rulify = (atomize2, rulify2)}) =
+    make_data (merge_opt (op =) (base_sort1, base_sort2), merge_opt (op =) (judgment1, judgment2),
       (Thm.merge_thms (atomize1, atomize2), Thm.merge_thms (rulify1, rulify2)));
 );
 
+fun map_data f = ObjectLogicData.map (fn (Data {base_sort, judgment, atomize_rulify}) =>
+  make_data (f (base_sort, judgment, atomize_rulify)));
+
+fun get_data thy = ObjectLogicData.get thy |> (fn Data args => args);
+
 
 
 (** generic treatment of judgments -- with a single argument only **)
 
+(* base_sort *)
+
+val get_base_sort = #base_sort o get_data;
+
+fun add_base_sort S = map_data (fn (base_sort, judgment, atomize_rulify) =>
+  if is_some base_sort then error "Attempt to redeclare object-logic base sort"
+  else (SOME S, judgment, atomize_rulify));
+
+
+(* typedecl *)
+
+fun typedecl (raw_name, vs, mx) thy =
+  let
+    val base_sort = get_base_sort thy;
+    val name = Sign.full_name thy (Syntax.type_name raw_name mx);
+    val _ = has_duplicates (op =) vs andalso
+      error ("Duplicate parameters in type declaration: " ^ quote name);
+    val n = length vs;
+    val T = Type (name, map (fn v => TFree (v, [])) vs);
+  in
+    thy
+    |> Sign.add_types [(raw_name, n, mx)]
+    |> (case base_sort of NONE => I | SOME S => AxClass.axiomatize_arity (name, replicate n S, S))
+    |> pair T
+  end;
+
+
 (* add judgment *)
 
 local
 
-fun new_judgment name (NONE, rules) = (SOME name, rules)
-  | new_judgment _ (SOME _, _) = error "Attempt to redeclare object-logic judgment";
-
 fun gen_add_judgment add_consts (bname, T, mx) thy =
   let val c = Sign.full_name thy (Syntax.const_name bname mx) in
     thy
     |> add_consts [(bname, T, mx)]
     |> (fn thy' => Theory.add_deps c (c, Sign.the_const_type thy' c) [] thy')
-    |> ObjectLogicData.map (new_judgment c)
+    |> map_data (fn (base_sort, judgment, atomize_rulify) =>
+        if is_some judgment then error "Attempt to redeclare object-logic judgment"
+        else (base_sort, SOME c, atomize_rulify))
   end;
 
 in
@@ -84,8 +127,8 @@
 (* judgments *)
 
 fun judgment_name thy =
-  (case ObjectLogicData.get thy of
-    (SOME name, _) => name
+  (case #judgment (get_data thy) of
+    SOME name => name
   | _ => raise TERM ("Unknown object-logic judgment", []));
 
 fun is_judgment thy (Const (c, _) $ _) = c = judgment_name thy
@@ -138,11 +181,14 @@
 
 (* maintain rules *)
 
-val get_atomize = #1 o #2 o ObjectLogicData.get;
-val get_rulify = #2 o #2 o ObjectLogicData.get;
+val get_atomize = #1 o #atomize_rulify o get_data;
+val get_rulify = #2 o #atomize_rulify o get_data;
 
-val add_atomize = ObjectLogicData.map o apsnd o apfst o Thm.add_thm;
-val add_rulify = ObjectLogicData.map o apsnd o apsnd o Thm.add_thm;
+fun add_atomize th = map_data (fn (base_sort, judgment, (atomize, rulify)) =>
+  (base_sort, judgment, (Thm.add_thm th atomize, rulify)));
+
+fun add_rulify th = map_data (fn (base_sort, judgment, (atomize, rulify)) =>
+  (base_sort, judgment, (atomize, Thm.add_thm th rulify)));
 
 val declare_atomize = Thm.declaration_attribute (fn th => Context.mapping (add_atomize th) I);
 val declare_rulify = Thm.declaration_attribute (fn th => Context.mapping (add_rulify th) I);