# HG changeset patch
# User wenzelm
# Date 1442954302 -7200
# Node ID 15865e0c55985ddef2fc885bcdca2d7c0d9a7571
# Parent  4918c6e52a02247d820b617f14955b0494bee97f
eliminated separate type Theory.dep: use typeargs uniformly for consts/types;
Object_Logic.add_judgment more like Theory.specify_const;

diff -r 4918c6e52a02 -r 15865e0c5598 src/Doc/Implementation/Logic.thy
--- a/src/Doc/Implementation/Logic.thy	Tue Sep 22 20:29:20 2015 +0200
+++ b/src/Doc/Implementation/Logic.thy	Tue Sep 22 22:38:22 2015 +0200
@@ -667,7 +667,7 @@
   \end{mldecls}
   \begin{mldecls}
   @{index_ML Theory.add_deps: "Proof.context -> string ->
-  Theory.dep -> Theory.dep list -> theory -> theory"} \\
+  Defs.entry -> Defs.entry list -> theory -> theory"} \\
   \end{mldecls}
 
   \begin{description}
@@ -766,7 +766,7 @@
   \item @{ML Theory.add_deps}~@{text "ctxt name c\<^sub>\<tau> \<^vec>d\<^sub>\<sigma>"}
   declares dependencies of a named specification for constant @{text
   "c\<^sub>\<tau>"}, relative to existing specifications for constants @{text
-  "\<^vec>d\<^sub>\<sigma>"}.
+  "\<^vec>d\<^sub>\<sigma>"}.  This also works for type constructors.
 
   \end{description}
 \<close>
diff -r 4918c6e52a02 -r 15865e0c5598 src/HOL/Tools/typedef.ML
--- a/src/HOL/Tools/typedef.ML	Tue Sep 22 20:29:20 2015 +0200
+++ b/src/HOL/Tools/typedef.ML	Tue Sep 22 22:38:22 2015 +0200
@@ -132,20 +132,21 @@
       |> Local_Theory.background_theory_result
         (Sign.declare_const lthy ((Rep_name, newT --> oldT), NoSyn) ##>>
           Sign.declare_const lthy ((Abs_name, oldT --> newT), NoSyn));
+    val const_dep = Theory.const_dep (Proof_Context.theory_of consts_lthy);
 
-    val A_consts = fold_aterms (fn Const c => insert (op =) (Theory.DConst c) | _ => I) A [];
+    val A_consts = fold_aterms (fn Const c => insert (op =) (const_dep c) | _ => I) A [];
     val A_types =
-      (fold_types o fold_subtypes) (fn Type t => insert (op =) (Theory.DType t) | _ => I) A [];
+      (fold_types o fold_subtypes) (fn Type t => insert (op =) (Theory.type_dep t) | _ => I) A [];
     val typedef_deps = A_consts @ A_types;
 
-    val newT_dep = Theory.DType (dest_Type newT);
+    val newT_dep = Theory.type_dep (dest_Type newT);
 
     val ((axiom_name, axiom), axiom_lthy) = consts_lthy
       |> Local_Theory.background_theory_result
         (Thm.add_axiom consts_lthy (type_definition_name, mk_typedef newT oldT RepC AbsC A) ##>
           Theory.add_deps consts_lthy "" newT_dep typedef_deps ##>
-          Theory.add_deps consts_lthy "" (Theory.DConst (dest_Const RepC)) [newT_dep] ##>
-          Theory.add_deps consts_lthy "" (Theory.DConst (dest_Const AbsC)) [newT_dep]);
+          Theory.add_deps consts_lthy "" (const_dep (dest_Const RepC)) [newT_dep] ##>
+          Theory.add_deps consts_lthy "" (const_dep (dest_Const AbsC)) [newT_dep]);
 
   in ((RepC, AbsC, axiom_name, axiom), axiom_lthy) end;
 
diff -r 4918c6e52a02 -r 15865e0c5598 src/Pure/Isar/object_logic.ML
--- a/src/Pure/Isar/object_logic.ML	Tue Sep 22 20:29:20 2015 +0200
+++ b/src/Pure/Isar/object_logic.ML	Tue Sep 22 22:38:22 2015 +0200
@@ -87,10 +87,13 @@
 local
 
 fun gen_add_judgment add_consts (b, T, mx) thy =
-  let val c = Sign.full_name thy b in
-    thy
-    |> add_consts [(b, T, mx)]
-    |> (fn thy' => Theory.add_deps_global c (Theory.DConst (c, Sign.the_const_type thy' c)) [] thy')
+  let
+    val c = Sign.full_name thy b;
+    val thy' = thy |> add_consts [(b, T, mx)];
+    val T' = Logic.unvarifyT_global (Sign.the_const_type thy' c);
+  in
+    thy'
+    |> Theory.add_deps_global "" (Theory.const_dep thy' (c, T')) []
     |> (Context.theory_map o 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))
diff -r 4918c6e52a02 -r 15865e0c5598 src/Pure/Isar/typedecl.ML
--- a/src/Pure/Isar/typedecl.ML	Tue Sep 22 20:29:20 2015 +0200
+++ b/src/Pure/Isar/typedecl.ML	Tue Sep 22 22:38:22 2015 +0200
@@ -58,7 +58,9 @@
   let
     val c = Local_Theory.full_name lthy b;
     val args = map (fn a => TFree (a, [])) (Name.invent Name.context Name.aT n);
-  in Local_Theory.background_theory (Theory.add_deps lthy "" (Theory.DType (c, args)) []) lthy end;
+  in
+    Local_Theory.background_theory (Theory.add_deps lthy "" (Theory.type_dep (c, args)) []) lthy
+  end;
 
 fun basic_typedecl final (b, n, mx) lthy =
   lthy
diff -r 4918c6e52a02 -r 15865e0c5598 src/Pure/axclass.ML
--- a/src/Pure/axclass.ML	Tue Sep 22 20:29:20 2015 +0200
+++ b/src/Pure/axclass.ML	Tue Sep 22 22:38:22 2015 +0200
@@ -596,6 +596,9 @@
 fun class_const c =
   (Logic.const_of_class c, Term.itselfT (Term.aT []) --> propT);
 
+fun class_const_dep c =
+  ((Defs.Constant, Logic.const_of_class c), [Term.aT []]);
+
 in
 
 val classrel_axiomatization =
@@ -614,8 +617,7 @@
     thy
     |> Sign.primitive_class (bclass, super)
     |> classrel_axiomatization (map (fn c => (class, c)) super)
-    |> Theory.add_deps_global "" (Theory.DConst (class_const class))
-      (map (Theory.DConst o class_const) super)
+    |> Theory.add_deps_global "" (class_const_dep class) (map class_const_dep super)
   end;
 
 end;
diff -r 4918c6e52a02 -r 15865e0c5598 src/Pure/pure_thy.ML
--- a/src/Pure/pure_thy.ML	Tue Sep 22 20:29:20 2015 +0200
+++ b/src/Pure/pure_thy.ML	Tue Sep 22 22:38:22 2015 +0200
@@ -66,10 +66,10 @@
     (Binding.make ("prop", @{here}), 0, NoSyn),
     (Binding.make ("itself", @{here}), 1, NoSyn),
     (Binding.make ("dummy", @{here}), 0, NoSyn)]
-  #> Theory.add_deps_global "fun" (Theory.DType ("fun", [typ "'a", typ "'b"])) []
-  #> Theory.add_deps_global "prop" (Theory.DType ("prop", [])) []
-  #> Theory.add_deps_global "itself" (Theory.DType ("itself", [typ "'a"])) []
-  #> Theory.add_deps_global "dummy" (Theory.DType ("dummy", [])) []
+  #> Theory.add_deps_global "fun" ((Defs.Type, "fun"), [typ "'a", typ "'b"]) []
+  #> Theory.add_deps_global "prop" ((Defs.Type, "prop"), []) []
+  #> Theory.add_deps_global "itself" ((Defs.Type, "itself"), [typ "'a"]) []
+  #> Theory.add_deps_global "dummy" ((Defs.Type, "dummy"), []) []
   #> Sign.add_nonterminals_global
     (map (fn name => Binding.make (name, @{here}))
       (Lexicon.terminals @ ["logic", "type", "types", "sort", "classes",
@@ -198,11 +198,11 @@
     (qualify (Binding.make ("prop", @{here})), typ "prop => prop", NoSyn),
     (qualify (Binding.make ("type", @{here})), typ "'a itself", NoSyn),
     (qualify (Binding.make ("dummy_pattern", @{here})), typ "'a", Delimfix "'_")]
-  #> Theory.add_deps_global "Pure.eq" (Theory.DConst ("Pure.eq", typ "'a => 'a => prop")) []
-  #> Theory.add_deps_global "Pure.imp" (Theory.DConst ("Pure.imp", typ "prop => prop => prop")) []
-  #> Theory.add_deps_global "Pure.all" (Theory.DConst ("Pure.all", typ "('a => prop) => prop")) []
-  #> Theory.add_deps_global "Pure.type" (Theory.DConst ("Pure.type", typ "'a itself")) []
-  #> Theory.add_deps_global "Pure.dummy_pattern" (Theory.DConst ("Pure.dummy_pattern", typ "'a")) []
+  #> Theory.add_deps_global "Pure.eq" ((Defs.Constant, "Pure.eq"), [typ "'a"]) []
+  #> Theory.add_deps_global "Pure.imp" ((Defs.Constant, "Pure.imp"), []) []
+  #> Theory.add_deps_global "Pure.all" ((Defs.Constant, "Pure.all"), [typ "'a"]) []
+  #> Theory.add_deps_global "Pure.type" ((Defs.Constant, "Pure.type"), [typ "'a"]) []
+  #> Theory.add_deps_global "Pure.dummy_pattern" ((Defs.Constant, "Pure.dummy_pattern"), [typ "'a"]) []
   #> Sign.parse_ast_translation Syntax_Trans.pure_parse_ast_translation
   #> Sign.parse_translation Syntax_Trans.pure_parse_translation
   #> Sign.print_ast_translation Syntax_Trans.pure_print_ast_translation
diff -r 4918c6e52a02 -r 15865e0c5598 src/Pure/theory.ML
--- a/src/Pure/theory.ML	Tue Sep 22 20:29:20 2015 +0200
+++ b/src/Pure/theory.ML	Tue Sep 22 22:38:22 2015 +0200
@@ -23,9 +23,10 @@
   val begin_theory: string * Position.T -> theory list -> theory
   val end_theory: theory -> theory
   val add_axiom: Proof.context -> binding * term -> theory -> theory
-  datatype dep = DConst of string * typ | DType of string * typ list
-  val add_deps: Proof.context -> string -> dep -> dep list -> theory -> theory
-  val add_deps_global: string -> dep -> dep list -> theory -> theory
+  val const_dep: theory -> string * typ -> Defs.entry
+  val type_dep: string * typ list -> Defs.entry
+  val add_deps: Proof.context -> string -> Defs.entry -> Defs.entry list -> theory -> theory
+  val add_deps_global: string -> Defs.entry -> Defs.entry list -> theory -> theory
   val add_def: Proof.context -> bool -> bool -> binding * term -> theory -> theory
   val specify_const: (binding * typ) * mixfix -> theory -> term * theory
   val check_overloading: Proof.context -> bool -> string * typ -> unit
@@ -212,29 +213,23 @@
 
 (* dependencies *)
 
-datatype dep = DConst of string * typ | DType of string * typ list
-
-fun name_of_dep (DConst (s, _)) = s
-  | name_of_dep (DType (s, _)) = s
+fun const_dep thy (c, T) = ((Defs.Constant, c), Sign.const_typargs thy (c, T));
+fun type_dep (c, args) = ((Defs.Type, c), args);
 
 fun dependencies ctxt unchecked def description lhs rhs =
   let
     val thy = Proof_Context.theory_of ctxt;
     val consts = Sign.consts_of thy;
 
-    fun prep (DConst const) =
-        let val Const (c, T) = Sign.no_vars ctxt (Const const)
-        in ((Defs.Constant, c), Consts.typargs consts (c, Logic.varifyT_global T)) end
-    | prep (DType typ) =
-        let val Type (c, Ts) = Type.no_tvars (Type typ)
-        in ((Defs.Type, c), map Logic.varifyT_global Ts) end;
+    fun prep (item, args) =
+      (case fold Term.add_tvarsT args [] of
+        [] => (item, map Logic.varifyT_global args)
+      | vs => raise TYPE ("Illegal schematic type variable(s)", map TVar vs, []));
 
-    fun fold_dep_tfree f (DConst (_, T)) = fold_atyps (fn TFree v => f v | _ => I) T
-      | fold_dep_tfree f (DType (_, Ts)) = fold (fold_atyps (fn TFree v => f v | _ => I)) Ts;
-
-    val lhs_vars = fold_dep_tfree (insert (op =)) lhs [];
-    val rhs_extras = fold (fold_dep_tfree
-      (fn v => if member (op =) lhs_vars v then I else insert (op =) v)) rhs [];
+    val lhs_vars = fold Term.add_tfreesT (snd lhs) [];
+    val rhs_extras =
+      fold (fn (_, args) => args |> (fold o Term.fold_atyps) (fn TFree v =>
+        if member (op =) lhs_vars v then I else insert (op =) v)) rhs [];
     val _ =
       if null rhs_extras then ()
       else error ("Specification depends on extra type variables: " ^
@@ -242,19 +237,24 @@
         "\nThe error(s) above occurred in " ^ quote description);
   in Defs.define ctxt unchecked def description (prep lhs) (map prep rhs) end;
 
+fun cert_entry thy ((Defs.Constant, c), args) =
+      Sign.cert_term thy (Const (c, Sign.const_instance thy (c, args)))
+      |> dest_Const |> const_dep thy
+  | cert_entry thy ((Defs.Type, c), args) =
+      Sign.certify_typ thy (Type (c, args)) |> dest_Type |> type_dep;
+
 fun add_deps ctxt a raw_lhs raw_rhs thy =
   let
-    fun cert_dep (DConst const) = const |> Const |> Sign.cert_term thy |> dest_Const |> DConst
-      | cert_dep (DType typ) = typ |> Type |> Sign.certify_typ thy |> dest_Type |> DType;
-    val lhs :: rhs = map cert_dep (raw_lhs :: raw_rhs);
-    val description = if a = "" then name_of_dep lhs ^ " axiom" else a;
+    val (lhs as ((_, lhs_name), _)) :: rhs = map (cert_entry thy) (raw_lhs :: raw_rhs);
+    val description = if a = "" then lhs_name ^ " axiom" else a;
   in thy |> map_defs (dependencies ctxt false NONE description lhs rhs) end;
 
-fun add_deps_global a x y thy = add_deps (Syntax.init_pretty_global thy) a x y thy;
+fun add_deps_global a x y thy =
+  add_deps (Syntax.init_pretty_global thy) a x y thy;
 
 fun specify_const decl thy =
-  let val (t as Const const, thy') = Sign.declare_const_global decl thy;
-  in (t, add_deps_global "" (DConst const) [] thy') end;
+  let val (t, thy') = Sign.declare_const_global decl thy;
+  in (t, add_deps_global "" (const_dep thy' (dest_Const t)) [] thy') end;
 
 
 (* overloading *)
@@ -293,13 +293,14 @@
       handle TERM (msg, _) => error msg;
     val lhs_const = Term.dest_Const (Term.head_of lhs);
 
-    val rhs_consts = fold_aterms (fn Const c => insert (op =) (DConst c) | _ => I) rhs [];
+    val rhs_consts =
+      fold_aterms (fn Const const => insert (op =) (const_dep thy const) | _ => I) rhs [];
     val rhs_types =
-      (fold_types o fold_subtypes) (fn Type t => insert (op =) (DType t) | _ => I) rhs [];
+      (fold_types o fold_subtypes) (fn Type t => insert (op =) (type_dep t) | _ => I) rhs [];
     val rhs_deps = rhs_consts @ rhs_types;
 
     val _ = check_overloading ctxt overloaded lhs_const;
-  in defs |> dependencies ctxt unchecked (SOME name) name (DConst lhs_const) rhs_deps end
+  in defs |> dependencies ctxt unchecked (SOME name) name (const_dep thy lhs_const) rhs_deps end
   handle ERROR msg => cat_error msg (Pretty.string_of (Pretty.block
    [Pretty.str ("The error(s) above occurred in definition " ^ Binding.print b ^ ":"),
     Pretty.fbrk, Pretty.quote (Syntax.pretty_term ctxt tm)]));