simplified retrieval of theory names of consts and types
authorhaftmann
Mon Jun 30 13:41:33 2008 +0200 (2008-06-30)
changeset 27398768da1da59d6
parent 27397 1d8456c5d53d
child 27399 1fb3d1219c12
simplified retrieval of theory names of consts and types
src/HOL/Tools/datatype_codegen.ML
src/HOL/Tools/inductive_codegen.ML
src/HOL/Tools/recfun_codegen.ML
src/HOL/Tools/typedef_codegen.ML
src/Pure/codegen.ML
     1.1 --- a/src/HOL/Tools/datatype_codegen.ML	Mon Jun 30 13:41:31 2008 +0200
     1.2 +++ b/src/HOL/Tools/datatype_codegen.ML	Mon Jun 30 13:41:33 2008 +0200
     1.3 @@ -46,7 +46,7 @@
     1.4  
     1.5      val (_, (tname, _, _)) :: _ = descr';
     1.6      val node_id = tname ^ " (type)";
     1.7 -    val module' = if_library (thyname_of_type tname thy) module;
     1.8 +    val module' = if_library (thyname_of_type thy tname) module;
     1.9  
    1.10      fun mk_dtdef gr prfx [] = (gr, [])
    1.11        | mk_dtdef gr prfx ((_, (tname, dts, cs))::xs) =
     2.1 --- a/src/HOL/Tools/inductive_codegen.ML	Mon Jun 30 13:41:31 2008 +0200
     2.2 +++ b/src/HOL/Tools/inductive_codegen.ML	Mon Jun 30 13:41:33 2008 +0200
     2.3 @@ -48,7 +48,7 @@
     2.4    let
     2.5      val {intros, graph, eqns} = CodegenData.get thy;
     2.6      fun thyname_of s = (case optmod of
     2.7 -      NONE => thyname_of_const s thy | SOME s => s);
     2.8 +      NONE => Codegen.thyname_of_const thy s | SOME s => s);
     2.9    in (case Option.map strip_comb (try HOLogic.dest_Trueprop (concl_of thm)) of
    2.10        SOME (Const ("op =", _), [t, _]) => (case head_of t of
    2.11          Const (s, _) =>
    2.12 @@ -85,7 +85,7 @@
    2.13        NONE => (case try (InductivePackage.the_inductive (ProofContext.init thy)) s of
    2.14          NONE => NONE
    2.15        | SOME ({names, ...}, {intrs, raw_induct, ...}) =>
    2.16 -          SOME (names, thyname_of_const s thy,
    2.17 +          SOME (names, Codegen.thyname_of_const thy s,
    2.18              length (InductivePackage.params_of raw_induct),
    2.19              preprocess thy intrs))
    2.20      | SOME _ =>
     3.1 --- a/src/HOL/Tools/recfun_codegen.ML	Mon Jun 30 13:41:31 2008 +0200
     3.2 +++ b/src/HOL/Tools/recfun_codegen.ML	Mon Jun 30 13:41:33 2008 +0200
     3.3 @@ -73,7 +73,7 @@
     3.4           else (preprocess thy (map fst thms'),
     3.5             case snd (snd (split_last thms')) of
     3.6                 NONE => (case get_defn thy defs s T of
     3.7 -                   NONE => thyname_of_const s thy
     3.8 +                   NONE => Codegen.thyname_of_const thy s
     3.9                   | SOME ((_, (thyname, _)), _) => thyname)
    3.10               | SOME thyname => thyname)
    3.11         end);
     4.1 --- a/src/HOL/Tools/typedef_codegen.ML	Mon Jun 30 13:41:31 2008 +0200
     4.2 +++ b/src/HOL/Tools/typedef_codegen.ML	Mon Jun 30 13:41:33 2008 +0200
     4.3 @@ -52,7 +52,7 @@
     4.4             if is_some (Codegen.get_assoc_type thy tname) then NONE else
     4.5             let
     4.6               val module' = Codegen.if_library
     4.7 -               (Codegen.thyname_of_type tname thy) module;
     4.8 +               (Codegen.thyname_of_type thy tname) module;
     4.9               val node_id = tname ^ " (type)";
    4.10               val (gr', (((qs, (_, Abs_id)), (_, Rep_id)), ty_id)) = foldl_map
    4.11                   (Codegen.invoke_tycodegen thy defs dep module (length Ts = 1))
     5.1 --- a/src/Pure/codegen.ML	Mon Jun 30 13:41:31 2008 +0200
     5.2 +++ b/src/Pure/codegen.ML	Mon Jun 30 13:41:33 2008 +0200
     5.3 @@ -57,8 +57,8 @@
     5.4    val get_const_id: string -> codegr -> string * string
     5.5    val mk_type_id: string -> string -> codegr -> codegr * (string * string)
     5.6    val get_type_id: string -> codegr -> string * string
     5.7 -  val thyname_of_type: string -> theory -> string
     5.8 -  val thyname_of_const: string -> theory -> string
     5.9 +  val thyname_of_type: theory -> string -> string
    5.10 +  val thyname_of_const: theory -> string -> string
    5.11    val rename_terms: term list -> term list
    5.12    val rename_term: term -> term
    5.13    val new_names: term -> string list -> string list
    5.14 @@ -496,23 +496,13 @@
    5.15  fun map_node k f (gr, x) = (Graph.map_node k f gr, x);
    5.16  fun new_node p (gr, x) = (Graph.new_node p gr, x);
    5.17  
    5.18 -fun theory_of_type s thy =
    5.19 -  if Sign.declared_tyname thy s
    5.20 -  then SOME (the_default thy (get_first (theory_of_type s) (Theory.parents_of thy)))
    5.21 -  else NONE;
    5.22 +fun thyname_of thy f x = the (AList.lookup (op =) (f x) Markup.theory_nameN);
    5.23  
    5.24 -fun theory_of_const s thy =
    5.25 -  if Sign.declared_const thy s
    5.26 -  then SOME (the_default thy (get_first (theory_of_const s) (Theory.parents_of thy)))
    5.27 -  else NONE;
    5.28 +fun thyname_of_type thy =
    5.29 +  thyname_of thy (Type.the_tags (Sign.tsig_of thy));
    5.30  
    5.31 -fun thyname_of_type s thy = (case theory_of_type s thy of
    5.32 -    NONE => error ("thyname_of_type: no such type: " ^ quote s)
    5.33 -  | SOME thy' => Context.theory_name thy');
    5.34 -
    5.35 -fun thyname_of_const s thy = (case theory_of_const s thy of
    5.36 -    NONE => error ("thyname_of_const: no such constant: " ^ quote s)
    5.37 -  | SOME thy' => Context.theory_name thy');
    5.38 +fun thyname_of_const thy =
    5.39 +  thyname_of thy (Consts.the_tags (Sign.consts_of thy));
    5.40  
    5.41  fun rename_terms ts =
    5.42    let
    5.43 @@ -695,7 +685,7 @@
    5.44                   val (gr4, _) = invoke_tycodegen thy defs dep module false
    5.45                     (gr3, funpow (length ts) (hd o tl o snd o dest_Type) T);
    5.46                   val (module', suffix) = (case get_defn thy defs s T of
    5.47 -                     NONE => (if_library (thyname_of_const s thy) module, "")
    5.48 +                     NONE => (if_library (thyname_of_const thy s) module, "")
    5.49                     | SOME ((U, (module', _)), NONE) =>
    5.50                         (if_library module' module, "")
    5.51                     | SOME ((U, (module', _)), SOME i) =>
    5.52 @@ -780,7 +770,7 @@
    5.53               val (gr'', qs) = foldl_map
    5.54                 (invoke_tycodegen thy defs dep module false)
    5.55                 (gr', quotes_of ms);
    5.56 -             val module' = if_library (thyname_of_type s thy) module;
    5.57 +             val module' = if_library (thyname_of_type thy s) module;
    5.58               val node_id = s ^ " (type)";
    5.59               fun p module' = Pretty.block (pretty_mixfix module module' ms ps qs)
    5.60             in SOME (case try (get_node gr'') node_id of