# HG changeset patch
# User haftmann
# Date 1195848570 -3600
# Node ID ba8f5e4fa33642dd2f94a4f6e15d5374e1dac060
# Parent  ba2bcae7aafdf59d1758e72a713e6276595f6051
separated typedecl module, providing typedecl command with interpretation

diff -r ba2bcae7aafd -r ba8f5e4fa336 src/HOL/Tools/datatype_package.ML
--- a/src/HOL/Tools/datatype_package.ML	Fri Nov 23 17:37:56 2007 +0100
+++ b/src/HOL/Tools/datatype_package.ML	Fri Nov 23 21:09:30 2007 +0100
@@ -557,7 +557,7 @@
     val thy2' = thy
 
       (** new types **)
-      |> fold2 (fn (name, mx) => fn tvs => TypedefPackage.add_typedecls [(name, tvs, mx)])
+      |> fold2 (fn (name, mx) => fn tvs => Typedecl.add (name, tvs, mx) #> snd)
            types_syntax tyvars
       |> add_path flat_names (space_implode "_" new_type_names)
 
diff -r ba2bcae7aafd -r ba8f5e4fa336 src/HOL/Tools/typedef_package.ML
--- a/src/HOL/Tools/typedef_package.ML	Fri Nov 23 17:37:56 2007 +0100
+++ b/src/HOL/Tools/typedef_package.ML	Fri Nov 23 21:09:30 2007 +0100
@@ -9,7 +9,6 @@
 signature TYPEDEF_PACKAGE =
 sig
   val quiet_mode: bool ref
-  val add_typedecls: (bstring * string list * mixfix) list -> theory -> theory
   type info =
    {rep_type: typ, abs_type: typ, Rep_name: string, Abs_name: string,
     type_definition: thm, set_def: thm option, Rep: thm, Rep_inverse: thm,
@@ -45,20 +44,6 @@
 
 
 
-(** type declarations **)
-
-fun HOL_arity (raw_name, args, mx) thy =
-  thy |> AxClass.axiomatize_arity
-    (Sign.full_name thy (Syntax.type_name raw_name mx),
-      replicate (length args) HOLogic.typeS, HOLogic.typeS);
-
-fun add_typedecls decls thy =
-  if can (Theory.assert_super HOL.thy) thy then
-    thy |> Sign.add_typedecls decls |> fold HOL_arity decls
-  else thy |> Sign.add_typedecls decls;
-
-
-
 (** type definitions **)
 
 (* messages *)
@@ -150,7 +135,8 @@
       else (NONE, thy);
 
     fun typedef_result nonempty =
-      add_typedecls [(t, vs, mx)]
+      Typedecl.add (t, vs, mx)
+      #> snd
       #> Sign.add_consts_i
        ((if def then [(name, setT', NoSyn)] else []) @
         [(Rep_name, newT --> oldT, NoSyn),
@@ -275,12 +261,6 @@
 
 val _ = OuterSyntax.keywords ["morphisms"];
 
-val _ =
-  OuterSyntax.command "typedecl" "type declaration (HOL)" K.thy_decl
-    (P.type_args -- P.name -- P.opt_infix >> (fn ((vs, t), mx) =>
-      Toplevel.theory (add_typedecls [(t, vs, mx)])));
-
-
 val typedef_decl =
   Scan.optional (P.$$$ "(" |--
       ((P.$$$ "open" >> K false) -- Scan.option P.name || P.name >> (fn s => (true, SOME s)))
diff -r ba2bcae7aafd -r ba8f5e4fa336 src/Pure/IsaMakefile
--- a/src/Pure/IsaMakefile	Fri Nov 23 17:37:56 2007 +0100
+++ b/src/Pure/IsaMakefile	Fri Nov 23 21:09:30 2007 +0100
@@ -73,7 +73,7 @@
   morphism.ML name.ML net.ML old_goals.ML pattern.ML primitive_defs.ML		\
   proofterm.ML pure_setup.ML pure_thy.ML search.ML sign.ML simplifier.ML	\
   sorts.ML subgoal.ML tactic.ML tctical.ML term.ML term_subst.ML theory.ML	\
-  thm.ML type.ML type_infer.ML unify.ML variable.ML
+  thm.ML type.ML typedecl.ML type_infer.ML unify.ML variable.ML
 	@./mk
 
 
diff -r ba2bcae7aafd -r ba8f5e4fa336 src/Pure/ROOT.ML
--- a/src/Pure/ROOT.ML	Fri Nov 23 17:37:56 2007 +0100
+++ b/src/Pure/ROOT.ML	Fri Nov 23 21:09:30 2007 +0100
@@ -74,6 +74,7 @@
 use "conjunction.ML";
 use "assumption.ML";
 use "goal.ML";
+use "typedecl.ML";
 use "axclass.ML";
 
 (*proof term operations*)
diff -r ba2bcae7aafd -r ba8f5e4fa336 src/Pure/sign.ML
--- a/src/Pure/sign.ML	Fri Nov 23 17:37:56 2007 +0100
+++ b/src/Pure/sign.ML	Fri Nov 23 21:09:30 2007 +0100
@@ -11,7 +11,6 @@
   val add_defsort: string -> theory -> theory
   val add_defsort_i: sort -> theory -> theory
   val add_types: (bstring * int * mixfix) list -> theory -> theory
-  val add_typedecls: (bstring * string list * mixfix) list -> theory -> theory
   val add_nonterminals: bstring list -> theory -> theory
   val add_tyabbrs: (bstring * string list * string * mixfix) list -> theory -> theory
   val add_tyabbrs_i: (bstring * string list * typ * mixfix) list -> theory -> theory
@@ -591,13 +590,6 @@
     val tsig' = Type.add_types naming decls tsig;
   in (naming, syn', tsig', consts) end);
 
-fun add_typedecls decls thy =
-  let
-    fun type_of (a, vs: string list, mx) =
-      if not (has_duplicates (op =) vs) then (a, length vs, mx)
-      else error ("Duplicate parameters in type declaration: " ^ quote a);
-  in add_types (map type_of decls) thy end;
-
 
 (* add nonterminals *)
 
diff -r ba2bcae7aafd -r ba8f5e4fa336 src/Pure/typedecl.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/typedecl.ML	Fri Nov 23 21:09:30 2007 +0100
@@ -0,0 +1,35 @@
+(*  Title:      Pure/typedecl.ML
+    ID:         $Id$
+    Author:     Florian Haftmann, TU Muenchen
+
+Primitive type declarations.
+*)
+
+signature TYPEDECL =
+sig
+  val add: bstring * string list * mixfix -> theory -> typ * theory
+  val interpretation: (string -> theory -> theory) -> theory -> theory
+end
+
+structure Typedecl: TYPEDECL =
+struct
+
+structure TypedeclInterpretation = InterpretationFun(type T = string val eq = op =);
+val interpretation = TypedeclInterpretation.interpretation;
+
+val _ = Context.add_setup TypedeclInterpretation.init;
+
+fun add (a, vs : string list, mx) thy =
+  let
+    val no_typargs = if not (has_duplicates (op =) vs) then length vs
+      else error ("Duplicate parameters in type declaration: " ^ quote a);
+    val a' = Sign.full_name thy a;
+    val T = Type (a', map (fn v => TFree (v, [])) vs);
+  in
+    thy
+    |> Sign.add_types [(a, no_typargs, mx)]
+    |> TypedeclInterpretation.data a'
+    |> pair T
+  end;
+
+end;