# HG changeset patch # User haftmann # Date 1214826093 -7200 # Node ID 768da1da59d67299b27171af359cd6dd410a104f # Parent 1d8456c5d53d1b4fcf28dda24a10ddac59254d9e simplified retrieval of theory names of consts and types diff -r 1d8456c5d53d -r 768da1da59d6 src/HOL/Tools/datatype_codegen.ML --- a/src/HOL/Tools/datatype_codegen.ML Mon Jun 30 13:41:31 2008 +0200 +++ b/src/HOL/Tools/datatype_codegen.ML Mon Jun 30 13:41:33 2008 +0200 @@ -46,7 +46,7 @@ val (_, (tname, _, _)) :: _ = descr'; val node_id = tname ^ " (type)"; - val module' = if_library (thyname_of_type tname thy) module; + val module' = if_library (thyname_of_type thy tname) module; fun mk_dtdef gr prfx [] = (gr, []) | mk_dtdef gr prfx ((_, (tname, dts, cs))::xs) = diff -r 1d8456c5d53d -r 768da1da59d6 src/HOL/Tools/inductive_codegen.ML --- a/src/HOL/Tools/inductive_codegen.ML Mon Jun 30 13:41:31 2008 +0200 +++ b/src/HOL/Tools/inductive_codegen.ML Mon Jun 30 13:41:33 2008 +0200 @@ -48,7 +48,7 @@ let val {intros, graph, eqns} = CodegenData.get thy; fun thyname_of s = (case optmod of - NONE => thyname_of_const s thy | SOME s => s); + NONE => Codegen.thyname_of_const thy s | SOME s => s); in (case Option.map strip_comb (try HOLogic.dest_Trueprop (concl_of thm)) of SOME (Const ("op =", _), [t, _]) => (case head_of t of Const (s, _) => @@ -85,7 +85,7 @@ NONE => (case try (InductivePackage.the_inductive (ProofContext.init thy)) s of NONE => NONE | SOME ({names, ...}, {intrs, raw_induct, ...}) => - SOME (names, thyname_of_const s thy, + SOME (names, Codegen.thyname_of_const thy s, length (InductivePackage.params_of raw_induct), preprocess thy intrs)) | SOME _ => diff -r 1d8456c5d53d -r 768da1da59d6 src/HOL/Tools/recfun_codegen.ML --- a/src/HOL/Tools/recfun_codegen.ML Mon Jun 30 13:41:31 2008 +0200 +++ b/src/HOL/Tools/recfun_codegen.ML Mon Jun 30 13:41:33 2008 +0200 @@ -73,7 +73,7 @@ else (preprocess thy (map fst thms'), case snd (snd (split_last thms')) of NONE => (case get_defn thy defs s T of - NONE => thyname_of_const s thy + NONE => Codegen.thyname_of_const thy s | SOME ((_, (thyname, _)), _) => thyname) | SOME thyname => thyname) end); diff -r 1d8456c5d53d -r 768da1da59d6 src/HOL/Tools/typedef_codegen.ML --- a/src/HOL/Tools/typedef_codegen.ML Mon Jun 30 13:41:31 2008 +0200 +++ b/src/HOL/Tools/typedef_codegen.ML Mon Jun 30 13:41:33 2008 +0200 @@ -52,7 +52,7 @@ if is_some (Codegen.get_assoc_type thy tname) then NONE else let val module' = Codegen.if_library - (Codegen.thyname_of_type tname thy) module; + (Codegen.thyname_of_type thy tname) module; val node_id = tname ^ " (type)"; val (gr', (((qs, (_, Abs_id)), (_, Rep_id)), ty_id)) = foldl_map (Codegen.invoke_tycodegen thy defs dep module (length Ts = 1)) diff -r 1d8456c5d53d -r 768da1da59d6 src/Pure/codegen.ML --- a/src/Pure/codegen.ML Mon Jun 30 13:41:31 2008 +0200 +++ b/src/Pure/codegen.ML Mon Jun 30 13:41:33 2008 +0200 @@ -57,8 +57,8 @@ val get_const_id: string -> codegr -> string * string val mk_type_id: string -> string -> codegr -> codegr * (string * string) val get_type_id: string -> codegr -> string * string - val thyname_of_type: string -> theory -> string - val thyname_of_const: string -> theory -> string + val thyname_of_type: theory -> string -> string + val thyname_of_const: theory -> string -> string val rename_terms: term list -> term list val rename_term: term -> term val new_names: term -> string list -> string list @@ -496,23 +496,13 @@ fun map_node k f (gr, x) = (Graph.map_node k f gr, x); fun new_node p (gr, x) = (Graph.new_node p gr, x); -fun theory_of_type s thy = - if Sign.declared_tyname thy s - then SOME (the_default thy (get_first (theory_of_type s) (Theory.parents_of thy))) - else NONE; +fun thyname_of thy f x = the (AList.lookup (op =) (f x) Markup.theory_nameN); -fun theory_of_const s thy = - if Sign.declared_const thy s - then SOME (the_default thy (get_first (theory_of_const s) (Theory.parents_of thy))) - else NONE; +fun thyname_of_type thy = + thyname_of thy (Type.the_tags (Sign.tsig_of thy)); -fun thyname_of_type s thy = (case theory_of_type s thy of - NONE => error ("thyname_of_type: no such type: " ^ quote s) - | SOME thy' => Context.theory_name thy'); - -fun thyname_of_const s thy = (case theory_of_const s thy of - NONE => error ("thyname_of_const: no such constant: " ^ quote s) - | SOME thy' => Context.theory_name thy'); +fun thyname_of_const thy = + thyname_of thy (Consts.the_tags (Sign.consts_of thy)); fun rename_terms ts = let @@ -695,7 +685,7 @@ val (gr4, _) = invoke_tycodegen thy defs dep module false (gr3, funpow (length ts) (hd o tl o snd o dest_Type) T); val (module', suffix) = (case get_defn thy defs s T of - NONE => (if_library (thyname_of_const s thy) module, "") + NONE => (if_library (thyname_of_const thy s) module, "") | SOME ((U, (module', _)), NONE) => (if_library module' module, "") | SOME ((U, (module', _)), SOME i) => @@ -780,7 +770,7 @@ val (gr'', qs) = foldl_map (invoke_tycodegen thy defs dep module false) (gr', quotes_of ms); - val module' = if_library (thyname_of_type s thy) module; + val module' = if_library (thyname_of_type thy s) module; val node_id = s ^ " (type)"; fun p module' = Pretty.block (pretty_mixfix module module' ms ps qs) in SOME (case try (get_node gr'') node_id of