# HG changeset patch
# User haftmann
# Date 1174639250 -3600
# Node ID 3572bc633d9a212f6ef9767622b1410beaddb6d1
# Parent  c78f1d924bfea2c9ba68cacd3e9776a9cd8bb102
tuned

diff -r c78f1d924bfe -r 3572bc633d9a src/HOL/Extraction/Pigeonhole.thy
--- a/src/HOL/Extraction/Pigeonhole.thy	Fri Mar 23 09:40:49 2007 +0100
+++ b/src/HOL/Extraction/Pigeonhole.thy	Fri Mar 23 09:40:50 2007 +0100
@@ -282,50 +282,55 @@
 we generate ML code from them.
 *}
 
-consts_code
-  arbitrary :: "nat \<times> nat" ("{* (0::nat, 0::nat) *}")
-
-code_module PH
-contains
-  test = "\<lambda>n. pigeonhole n (\<lambda>m. m - 1)"
-  test' = "\<lambda>n. pigeonhole_slow n (\<lambda>m. m - 1)"
-  sel = "op !"
-
-ML "timeit (fn () => PH.test 10)"
-ML "timeit (fn () => PH.test' 10)"
-ML "timeit (fn () => PH.test 20)"
-ML "timeit (fn () => PH.test' 20)"
-ML "timeit (fn () => PH.test 25)"
-ML "timeit (fn () => PH.test' 25)"
-ML "timeit (fn () => PH.test 500)"
-
-ML "PH.pigeonhole 8 (PH.sel [0,1,2,3,4,5,6,3,7,8])"
-
-definition
-  arbitrary_nat :: "nat \<times> nat" where
-  [symmetric, code inline]: "arbitrary_nat = arbitrary"
-definition
-  arbitrary_nat_subst :: "nat \<times> nat" where
-  "arbitrary_nat_subst = (0, 0)"
-
-code_axioms
-  arbitrary_nat \<equiv> arbitrary_nat_subst
-
 definition
   "test n = pigeonhole n (\<lambda>m. m - 1)"
 definition
   "test' n = pigeonhole_slow n (\<lambda>m. m - 1)"
+definition
+  "test'' u = pigeonhole 8 (op ! [0, 1, 2, 3, 4, 5, 6, 3, 7, 8])"
 
-code_gen test test' "op !" (SML #)
+
+consts_code
+  arbitrary :: "nat \<times> nat" ("{* (0::nat, 0::nat) *}")
+
+definition
+  arbitrary_nat_pair :: "nat \<times> nat" where
+  [symmetric, code inline]: "arbitrary_nat_pair = arbitrary"
+
+code_const arbitrary_nat_pair (SML "(~1, ~1)")
+  (* this is justified since for valid inputs this "arbitrary" will be dropped
+     in the next recursion step in pigeonhole_def *)
 
+code_module PH
+contains
+  test = test
+  test' = test'
+  test'' = test''
+
+code_gen test test' test'' (SML #)
+
+ML "timeit (fn () => PH.test 10)"
 ML "timeit (fn () => ROOT.Pigeonhole.test 10)"
+
+ML "timeit (fn () => PH.test' 10)"
 ML "timeit (fn () => ROOT.Pigeonhole.test' 10)"
+
+ML "timeit (fn () => PH.test 20)"
 ML "timeit (fn () => ROOT.Pigeonhole.test 20)"
+
+ML "timeit (fn () => PH.test' 20)"
 ML "timeit (fn () => ROOT.Pigeonhole.test' 20)"
+
+ML "timeit (fn () => PH.test 25)"
 ML "timeit (fn () => ROOT.Pigeonhole.test 25)"
+
+ML "timeit (fn () => PH.test' 25)"
 ML "timeit (fn () => ROOT.Pigeonhole.test' 25)"
+
+ML "timeit (fn () => PH.test 500)"
 ML "timeit (fn () => ROOT.Pigeonhole.test 500)"
 
-ML "ROOT.Pigeonhole.pigeonhole 8 (ROOT.List.nth [0,1,2,3,4,5,6,3,7,8])"
+ML "timeit PH.test''"
+ML "timeit ROOT.Pigeonhole.test''"
 
 end
diff -r c78f1d924bfe -r 3572bc633d9a src/HOL/Library/EfficientNat.thy
--- a/src/HOL/Library/EfficientNat.thy	Fri Mar 23 09:40:49 2007 +0100
+++ b/src/HOL/Library/EfficientNat.thy	Fri Mar 23 09:40:50 2007 +0100
@@ -148,6 +148,8 @@
   @{typ nat} is no longer a datatype but embedded into the integers.
 *}
 
+code_datatype nat_of_int
+
 code_const "0::nat"
   (SML "!(0 : IntInf.int)")
   (OCaml "Big'_int.big'_int'_of'_int/ 0")
@@ -158,10 +160,6 @@
   (OCaml "Big_int.succ'_big'_int")
   (Haskell "!((_) + 1)")
 
-setup {*
-  CodegenData.add_datatype ("nat", ([], []))
-*}
-
 types_code
   nat ("int")
 attach (term_of) {*
diff -r c78f1d924bfe -r 3572bc633d9a src/HOL/ex/Codegenerator_Rat.thy
--- a/src/HOL/ex/Codegenerator_Rat.thy	Fri Mar 23 09:40:49 2007 +0100
+++ b/src/HOL/ex/Codegenerator_Rat.thy	Fri Mar 23 09:40:50 2007 +0100
@@ -6,7 +6,7 @@
 header {* Simple example for executable rational numbers *}
 
 theory Codegenerator_Rat
-imports ExecutableRat EfficientNat
+imports EfficientNat ExecutableRat
 begin
 
 definition
diff -r c78f1d924bfe -r 3572bc633d9a src/Pure/Tools/class_package.ML
--- a/src/Pure/Tools/class_package.ML	Fri Mar 23 09:40:49 2007 +0100
+++ b/src/Pure/Tools/class_package.ML	Fri Mar 23 09:40:50 2007 +0100
@@ -112,13 +112,13 @@
     val (_, t) = read_def thy (raw_name, raw_t);
     val ((c, ty), _) = Sign.cert_def (Sign.pp thy) t;
     val atts = map (prep_att thy) raw_atts;
-    val insts = (Consts.typargs (Sign.consts_of thy) (c, ty))
+    val insts = Consts.typargs (Sign.consts_of thy) (c, ty);
     val name = case raw_name
      of "" => NONE
       | _ => SOME raw_name;
   in (c, (insts, ((name, t), atts))) end;
 
-fun read_def_cmd thy = gen_read_def thy Attrib.intern_src read_axm;
+fun read_def_cmd thy = gen_read_def thy Attrib.intern_src Theory.read_axm;
 fun read_def thy = gen_read_def thy (K I) (K I);
 
 fun gen_instance_arity prep_arity read_def do_proof raw_arities raw_defs theory =
@@ -153,13 +153,13 @@
             val (c, (inst, ((name_opt, t), atts))) = read_def thy_read raw_def;
             val ty = Consts.instance (Sign.consts_of thy_read) (c, inst);
             val ((tyco, class), ty') = case AList.lookup (op =) cs c
-             of NONE => error ("superfluous definition for constant " ^ quote c)
+             of NONE => error ("illegal definition for constant " ^ quote c)
               | SOME class_ty => class_ty;
             val name = case name_opt
              of NONE => Thm.def_name (Logic.name_arity (tyco, [], c))
               | SOME name => name;
             val t' = case mk_typnorm thy_read (ty', ty)
-             of NONE => error ("superfluous definition for constant " ^
+             of NONE => error ("illegal definition for constant " ^
                   quote c ^ "::" ^ Sign.string_of_typ thy_read ty)
               | SOME norm => map_types norm t
           in (((class, tyco), ((name, t'), atts)), AList.delete (op =) c cs) end;
diff -r c78f1d924bfe -r 3572bc633d9a src/Pure/Tools/codegen_data.ML
--- a/src/Pure/Tools/codegen_data.ML	Fri Mar 23 09:40:49 2007 +0100
+++ b/src/Pure/Tools/codegen_data.ML	Fri Mar 23 09:40:50 2007 +0100
@@ -14,20 +14,23 @@
   val add_func: bool -> thm -> theory -> theory
   val del_func: thm -> theory -> theory
   val add_funcl: CodegenConsts.const * thm list Susp.T -> theory -> theory
-  val add_datatype: string * ((string * sort) list * (string * typ list) list)
-    -> theory -> theory
   val add_inline: thm -> theory -> theory
   val del_inline: thm -> theory -> theory
   val add_inline_proc: string * (theory -> cterm list -> thm list) -> theory -> theory
   val del_inline_proc: string -> theory -> theory
   val add_preproc: string * (theory -> thm list -> thm list) -> theory -> theory
   val del_preproc: string -> theory -> theory
+  val add_datatype: string * ((string * sort) list * (string * typ list) list)
+    -> theory -> theory
+  val add_datatype_consts: CodegenConsts.const list -> theory -> theory
+
   val coregular_algebra: theory -> Sorts.algebra
   val operational_algebra: theory -> (sort -> sort) * Sorts.algebra
   val these_funcs: theory -> CodegenConsts.const -> thm list
   val tap_typ: theory -> CodegenConsts.const -> typ option
   val get_datatype: theory -> string -> ((string * sort) list * (string * typ list) list)
   val get_datatype_of_constr: theory -> CodegenConsts.const -> string option
+  val get_constr_typ: theory -> CodegenConsts.const -> typ option
 
   val preprocess_cterm: cterm -> thm
 
@@ -190,38 +193,37 @@
     in (SOME consts, thms) end;
 
 val eq_string = op = : string * string -> bool;
+val eq_co = eq_pair eq_string (eq_list (is_equal o Term.typ_ord));
 fun eq_dtyp ((vs1, cs1), (vs2, cs2)) = 
   gen_eq_set (eq_pair eq_string (gen_eq_set eq_string)) (vs1, vs2)
-    andalso gen_eq_set (eq_pair eq_string (eq_list (is_equal o Term.typ_ord))) (cs1, cs2);
+    andalso gen_eq_set eq_co (cs1, cs2);
 fun merge_dtyps (tabs as (tab1, tab2)) =
   let
     val tycos1 = Symtab.keys tab1;
     val tycos2 = Symtab.keys tab2;
     val tycos' = filter (member eq_string tycos2) tycos1;
-    val touched = not (gen_eq_set (op =) (tycos1, tycos2) andalso
-      gen_eq_set (eq_pair (op =) (eq_dtyp))
+    val new_types = not (gen_eq_set (op =) (tycos1, tycos2));
+    val diff_types = not (gen_eq_set (eq_pair (op =) eq_dtyp)
       (AList.make (the o Symtab.lookup tab1) tycos',
        AList.make (the o Symtab.lookup tab2) tycos'));
-  in (touched, Symtab.merge (K true) tabs) end;
+  in ((new_types, diff_types), Symtab.merge (K true) tabs) end;
 
 datatype spec = Spec of {
   funcs: sdthms Consttab.table,
-  dconstrs: string Consttab.table,
   dtyps: ((string * sort) list * (string * typ list) list) Symtab.table
 };
 
-fun mk_spec ((funcs, dconstrs), dtyps) =
-  Spec { funcs = funcs, dconstrs = dconstrs, dtyps = dtyps };
-fun map_spec f (Spec { funcs = funcs, dconstrs = dconstrs, dtyps = dtyps }) =
-  mk_spec (f ((funcs, dconstrs), dtyps));
-fun merge_spec (Spec { funcs = funcs1, dconstrs = dconstrs1, dtyps = dtyps1 },
-  Spec { funcs = funcs2, dconstrs = dconstrs2, dtyps = dtyps2 }) =
+fun mk_spec (funcs, dtyps) =
+  Spec { funcs = funcs, dtyps = dtyps };
+fun map_spec f (Spec { funcs = funcs, dtyps = dtyps }) =
+  mk_spec (f (funcs, dtyps));
+fun merge_spec (Spec { funcs = funcs1, dtyps = dtyps1 },
+  Spec { funcs = funcs2, dtyps = dtyps2 }) =
   let
     val (touched_cs, funcs) = merge_funcs (funcs1, funcs2);
-    val dconstrs = Consttab.merge (K true) (dconstrs1, dconstrs2);
-    val (touched', dtyps) = merge_dtyps (dtyps1, dtyps2);
-    val touched = if touched' then NONE else touched_cs;
-  in (touched, mk_spec ((funcs, dconstrs), dtyps)) end;
+    val ((new_types, diff_types), dtyps) = merge_dtyps (dtyps1, dtyps2);
+    val touched = if new_types orelse diff_types then NONE else touched_cs;
+  in (touched, mk_spec (funcs, dtyps)) end;
 
 datatype exec = Exec of {
   preproc: preproc,
@@ -240,16 +242,14 @@
     val touched = if touched' then NONE else touched_cs;
   in (touched, mk_exec (preproc, spec)) end;
 val empty_exec = mk_exec (mk_preproc (([], []), []),
-  mk_spec ((Consttab.empty, Consttab.empty), Symtab.empty));
+  mk_spec (Consttab.empty, Symtab.empty));
 
 fun the_preproc (Exec { preproc = Preproc x, ...}) = x;
 fun the_spec (Exec { spec = Spec x, ...}) = x;
 val the_funcs = #funcs o the_spec;
-val the_dcontrs = #dconstrs o the_spec;
 val the_dtyps = #dtyps o the_spec;
 val map_preproc = map_exec o apfst o map_preproc;
-val map_funcs = map_exec o apsnd o map_spec o apfst o apfst;
-val map_dconstrs = map_exec o apsnd o map_spec o apfst o apsnd;
+val map_funcs = map_exec o apsnd o map_spec o apfst;
 val map_dtyps = map_exec o apsnd o map_spec o apsnd;
 
 
@@ -491,7 +491,6 @@
     val ty_inst = Type (tyco, map TFree sort_args);
   in Logic.varifyT (map_type_tfree (K ty_inst) ty) end;
 
-(*FIXME: make distinct step: building algebra from code theorems*)
 fun retrieve_algebra thy operational =
   Sorts.subalgebra (Sign.pp thy) operational
     (weakest_constraints thy)
@@ -611,80 +610,29 @@
 
 local
 
-fun consts_of_cos thy tyco vs cos =
-  let
-    val dty = Type (tyco, map TFree vs);
-    fun mk_co (co, tys) = CodegenConsts.norm_of_typ thy (co, tys ---> dty);
-  in map mk_co cos end;
-
-fun co_of_const thy (c, ty) =
-  let
-    fun err () = error
-     ("Illegal type for datatype constructor: " ^ Sign.string_of_typ thy ty);
-    val (tys, ty') = strip_type ty;
-    val (tyco, vs) = ((apsnd o map) dest_TFree o dest_Type) ty'
-      handle TYPE _ => err ();
-    val sorts = if has_duplicates (eq_fst op =) vs then err ()
-      else map snd vs;
-    val vs_names = Name.invent_list [] "'a" (length vs);
-    val vs_map = map fst vs ~~ vs_names;
-    val vs' = vs_names ~~ sorts;
-    val tys' = (map o map_type_tfree) (fn (v, sort) =>
-      (TFree ((the o AList.lookup (op =) vs_map) v, sort))) tys
-      handle Option => err ();
-  in (tyco, (vs', (c, tys'))) end;
-
 fun del_datatype tyco thy =
   case Symtab.lookup ((the_dtyps o get_exec) thy) tyco
    of SOME (vs, cos) => let
-        val consts = consts_of_cos thy tyco vs cos;
-        val del =
-          map_dtyps (Symtab.delete tyco)
-          #> map_dconstrs (fold Consttab.delete consts)
-      in map_exec_purge (SOME consts) del thy end
+        val consts = CodegenConsts.consts_of_cos thy tyco vs cos;
+      in map_exec_purge (SOME consts) (map_dtyps (Symtab.delete tyco)) thy end
     | NONE => thy;
 
-(*FIXME integrate this auxiliary properly*)
-
 in
 
 fun add_datatype (tyco, (vs_cos as (vs, cos))) thy =
   let
-    val consts = consts_of_cos thy tyco vs cos;
-    val add =
-      map_dtyps (Symtab.update_new (tyco, vs_cos))
-      #> map_dconstrs (fold (fn c => Consttab.update (c, tyco)) consts)
+    val consts = CodegenConsts.consts_of_cos thy tyco vs cos;
   in
     thy
     |> del_datatype tyco
-    |> map_exec_purge (SOME consts) add
+    |> map_exec_purge (SOME consts) (map_dtyps (Symtab.update_new (tyco, vs_cos)))
   end;
 
-fun add_datatype_consts cs thy =
-  let
-    val raw_cos = map (co_of_const thy) cs;
-    val (tyco, (vs_names, sorts_cos)) = if (length o distinct (eq_fst op =)) raw_cos = 1
-      then ((fst o hd) raw_cos, ((map fst o fst o snd o hd) raw_cos,
-        map ((apfst o map) snd o snd) raw_cos))
-      else error ("Term constructors not referring to the same type: "
-        ^ commas (map (CodegenConsts.string_of_const_typ thy) cs));
-    val sorts = foldr1 ((uncurry o map2 o curry o Sorts.inter_sort) (Sign.classes_of thy))
-      (map fst sorts_cos);
-    val cos = map snd sorts_cos;
-    val vs = vs_names ~~ sorts;
-  in
-    thy
-    |> add_datatype (tyco, (vs, cos))
-  end;
+fun add_datatype_consts consts thy =
+  add_datatype (CodegenConsts.cos_of_consts thy consts) thy;
 
 fun add_datatype_consts_cmd raw_cs thy =
-  let
-    val cs = map (apsnd Logic.unvarifyT o CodegenConsts.typ_of_inst thy
-      o CodegenConsts.read_const thy) raw_cs
-  in
-    thy
-    |> add_datatype_consts cs
-  end;
+  add_datatype_consts (map (CodegenConsts.read_const thy) raw_cs) thy
 
 end; (*local*)
 
@@ -712,6 +660,10 @@
 fun del_preproc name =
   (map_exec_purge NONE o map_preproc o apsnd) (delete_force "preprocessor" name);
 
+
+
+(** retrieval **)
+
 local
 
 fun gen_apply_inline_proc prep post thy f x =
@@ -764,25 +716,6 @@
 
 end; (*local*)
 
-fun get_datatype thy tyco =
-  case Symtab.lookup ((the_dtyps o get_exec) thy) tyco
-   of SOME spec => spec
-    | NONE => Sign.arity_number thy tyco
-        |> Name.invents Name.context "'a"
-        |> map (rpair [])
-        |> rpair [];
-
-fun get_datatype_of_constr thy =
-  Consttab.lookup ((the_dcontrs o get_exec) thy);
-
-fun get_datatype_constr thy const =
-  case Consttab.lookup ((the_dcontrs o get_exec) thy) const
-   of SOME tyco => let
-        val (vs, cs) = get_datatype thy tyco;
-        (*FIXME continue here*)
-      in NONE end
-    | NONE => NONE;
-
 local
 
 fun get_funcs thy const =
@@ -821,6 +754,33 @@
 
 end; (*local*)
 
+fun get_datatype thy tyco =
+  case Symtab.lookup ((the_dtyps o get_exec) thy) tyco
+   of SOME spec => spec
+    | NONE => Sign.arity_number thy tyco
+        |> Name.invents Name.context "'a"
+        |> map (rpair [])
+        |> rpair [];
+
+fun get_datatype_of_constr thy const =
+  case CodegenConsts.co_of_const' thy const
+   of SOME (tyco, (_, co)) => if member eq_co
+        (Symtab.lookup (((the_dtyps o get_exec) thy)) tyco
+          |> Option.map snd
+          |> the_default []) co then SOME tyco else NONE
+    | NONE => NONE;
+
+fun get_constr_typ thy const =
+  case get_datatype_of_constr thy const
+   of SOME tyco => let
+        val (vs, cos) = get_datatype thy tyco;
+        val (_, (_, (co, tys))) = CodegenConsts.co_of_const thy const
+      in (tys ---> Type (tyco, map TFree vs))
+        |> map_atyps (fn TFree (v, _) => TFree (v, AList.lookup (op =) vs v |> the))
+        |> Logic.varifyT
+        |> SOME end
+    | NONE => NONE;
+
 
 (** code attributes **)
 
diff -r c78f1d924bfe -r 3572bc633d9a src/Pure/Tools/codegen_funcgr.ML
--- a/src/Pure/Tools/codegen_funcgr.ML	Fri Mar 23 09:40:49 2007 +0100
+++ b/src/Pure/Tools/codegen_funcgr.ML	Fri Mar 23 09:40:50 2007 +0100
@@ -15,6 +15,7 @@
   val deps: T -> CodegenConsts.const list -> CodegenConsts.const list list
   val all: T -> CodegenConsts.const list
   val pretty: theory -> T -> Pretty.T
+  structure Constgraph : GRAPH
 end
 
 signature CODEGEN_FUNCGR_RETRIEVAL =
@@ -257,11 +258,13 @@
               |> Logic.varifyT
           | _ => TVar (("'a", 0), [class]);
       in Term.map_type_tvar (K inst) ty end;
-    fun default_typ (const as (c, tys)) = case CodegenData.tap_typ thy const
-     of SOME ty => ty
-      | NONE => (case AxClass.class_of_param thy c
+    fun default_typ (const as (c, tys)) = case AxClass.class_of_param thy c
          of SOME class => classop_typ const class
-          | NONE => Sign.the_const_type thy c)
+          | NONE => (case CodegenData.tap_typ thy const
+             of SOME ty => ty
+              | NONE => (case CodegenData.get_constr_typ thy const
+                 of SOME ty => ty
+                  | NONE => Sign.the_const_type thy c))
     fun typ_func (const as (c, tys)) thms thm =
       let
         val ty = CodegenFunc.typ_func thm;
diff -r c78f1d924bfe -r 3572bc633d9a src/Pure/Tools/codegen_package.ML
--- a/src/Pure/Tools/codegen_package.ML	Fri Mar 23 09:40:49 2007 +0100
+++ b/src/Pure/Tools/codegen_package.ML	Fri Mar 23 09:40:50 2007 +0100
@@ -74,6 +74,19 @@
 fun print_codethms thy =
   Pretty.writeln o CodegenFuncgr.pretty thy o Funcgr.make thy;
 
+fun code_deps thy consts =
+  let
+    val gr = Funcgr.make thy consts;
+    fun mk_entry (const, (_, (_, parents))) =
+      let
+        val name = CodegenConsts.string_of_const thy const;
+        val nameparents = map (CodegenConsts.string_of_const thy) parents;
+      in { name = name, ID = name, dir = "", unfold = true,
+        path = "", parents = nameparents }
+      end;
+    val prgr = CodegenFuncgr.Constgraph.fold ((fn x => fn xs => xs @ [x]) o mk_entry) gr [];
+  in Present.display_graph prgr end;
+
 structure Code = CodeDataFun
 (struct
   val name = "Pure/codegen_package_code";
@@ -574,8 +587,8 @@
 
 fun raw_eval_term thy (ref_spec, t) args =
   let
-    val _ = (Term.fold_types o Term.fold_atyps) (fn _ =>
-      error ("Term" ^ Sign.string_of_term thy t ^ "is polymorphic"))
+    val _ = (Term.map_types o Term.map_atyps) (fn _ =>
+      error ("Term " ^ Sign.string_of_term thy t ^ " contains polymorphic type"))
       t;
     val t' = codegen_term thy t;
   in
@@ -650,9 +663,11 @@
     (map (serialize' cs code) (map_filter snd seris'); ())
   end;
 
-fun print_codethms_e thy =
+fun print_codethms_cmd thy =
   print_codethms thy o map (CodegenConsts.read_const thy);
 
+fun code_deps_cmd thy =
+  code_deps thy o map (CodegenConsts.read_const thy);
 
 val code_exprP = (
     (Scan.repeat P.term
@@ -662,8 +677,8 @@
     >> (fn (raw_cs, seris) => code raw_cs seris)
   );
 
-val (codeK, code_abstypeK, code_axiomsK, code_thmsK) =
-  ("code_gen", "code_abstype", "code_axioms", "code_thms");
+val (codeK, code_abstypeK, code_axiomsK, code_thmsK, code_depsK) =
+  ("code_gen", "code_abstype", "code_axioms", "code_thms", "code_deps");
 
 in
 
@@ -693,9 +708,15 @@
   OuterSyntax.improper_command code_thmsK "print cached defining equations" OuterKeyword.diag
     (Scan.repeat P.term
       >> (fn cs => Toplevel.no_timing o Toplevel.unknown_theory
-        o Toplevel.keep ((fn thy => print_codethms_e thy cs) o Toplevel.theory_of)));
+        o Toplevel.keep ((fn thy => print_codethms_cmd thy cs) o Toplevel.theory_of)));
 
-val _ = OuterSyntax.add_parsers [codeP, code_abstypeP, code_axiomsP, code_thmsP];
+val code_depsP =
+  OuterSyntax.improper_command code_depsK "visualize dependencies of defining equations" OuterKeyword.diag
+    (Scan.repeat P.term
+      >> (fn cs => Toplevel.no_timing o Toplevel.unknown_theory
+        o Toplevel.keep ((fn thy => code_deps_cmd thy cs) o Toplevel.theory_of)));
+
+val _ = OuterSyntax.add_parsers [codeP, code_abstypeP, code_axiomsP, code_thmsP, code_depsP];
 
 end; (* local *)