src/HOL/Tools/typedef_package.ML
changeset 16645 a152d6b21c31
parent 16486 1a12cdb6ee6b
child 17057 0934ac31985f
--- a/src/HOL/Tools/typedef_package.ML	Fri Jul 01 14:11:06 2005 +0200
+++ b/src/HOL/Tools/typedef_package.ML	Fri Jul 01 14:13:40 2005 +0200
@@ -272,17 +272,18 @@
 
 (** trivial code generator **)
 
-fun typedef_codegen thy gr dep brack t =
+fun typedef_codegen thy defs gr dep thyname brack t =
   let
+    fun get_name (Type (tname, _)) = tname
+      | get_name _ = "";
     fun mk_fun s T ts =
       let
-        val (gr', _) = Codegen.invoke_tycodegen thy dep false (gr, T);
+        val (gr', _) = Codegen.invoke_tycodegen thy defs dep thyname false (gr, T);
         val (gr'', ps) =
-          foldl_map (Codegen.invoke_codegen thy dep true) (gr', ts);
-        val id = Codegen.mk_const_id thy s
+          foldl_map (Codegen.invoke_codegen thy defs dep thyname true) (gr', ts);
+        val id = Codegen.mk_const_id thy
+          thyname (Codegen.thyname_of_type (get_name T) thy) s
       in SOME (gr'', Codegen.mk_app brack (Pretty.str id) ps) end;
-    fun get_name (Type (tname, _)) = tname
-      | get_name _ = "";
     fun lookup f T = getOpt (Option.map f (Symtab.lookup
       (TypedefData.get thy, get_name T)), "")
   in
@@ -302,23 +303,25 @@
   | mk_tyexpr [p] s = Pretty.block [p, Pretty.str (" " ^ s)]
   | mk_tyexpr ps s = Pretty.list "(" (") " ^ s) ps;
 
-fun typedef_tycodegen thy gr dep brack (Type (s, Ts)) =
+fun typedef_tycodegen thy defs gr dep thyname brack (Type (s, Ts)) =
       (case Symtab.lookup (TypedefData.get thy, s) of
          NONE => NONE
        | SOME (newT as Type (tname, Us), oldT, Abs_name, Rep_name) =>
            if isSome (Codegen.get_assoc_type thy tname) then NONE else
            let
-             val Abs_id = Codegen.mk_const_id thy Abs_name;
-             val Rep_id = Codegen.mk_const_id thy Rep_name;
-             val ty_id = Codegen.mk_type_id thy s;
+             val thyname' = Codegen.thyname_of_type tname thy;
+             val Abs_id = Codegen.mk_const_id thy thyname' thyname' Abs_name;
+             val Rep_id = Codegen.mk_const_id thy thyname' thyname' Rep_name;
+             val ty_id = Codegen.mk_type_id thy thyname' thyname' s;
+             val ty_call_id = Codegen.mk_type_id thy thyname thyname' s;
              val (gr', qs) = foldl_map
-               (Codegen.invoke_tycodegen thy dep (length Ts = 1)) (gr, Ts);
-             val gr'' = Graph.add_edge (Abs_id, dep) gr' handle Graph.UNDEF _ =>
+               (Codegen.invoke_tycodegen thy defs dep thyname (length Ts = 1)) (gr, Ts);
+             val gr'' = Graph.add_edge (Abs_name, dep) gr' handle Graph.UNDEF _ =>
                let
                  val (gr'', p :: ps) = foldl_map
-                   (Codegen.invoke_tycodegen thy Abs_id false)
-                   (Graph.add_edge (Abs_id, dep)
-                      (Graph.new_node (Abs_id, (NONE, "")) gr'), oldT :: Us);
+                   (Codegen.invoke_tycodegen thy defs Abs_name thyname' false)
+                   (Graph.add_edge (Abs_name, dep)
+                      (Graph.new_node (Abs_name, (NONE, "", "")) gr'), oldT :: Us);
                  val s =
                    Pretty.string_of (Pretty.block [Pretty.str "datatype ",
                      mk_tyexpr ps ty_id,
@@ -329,28 +332,28 @@
                      Pretty.str "x) = x;"]) ^ "\n\n" ^
                    (if "term_of" mem !Codegen.mode then
                       Pretty.string_of (Pretty.block [Pretty.str "fun ",
-                        Codegen.mk_term_of thy false newT, Pretty.brk 1,
+                        Codegen.mk_term_of thy thyname' false newT, Pretty.brk 1,
                         Pretty.str ("(" ^ Abs_id), Pretty.brk 1,
                         Pretty.str "x) =", Pretty.brk 1,
                         Pretty.block [Pretty.str ("Const (\"" ^ Abs_name ^ "\","),
                           Pretty.brk 1, Codegen.mk_type false (oldT --> newT),
                           Pretty.str ")"], Pretty.str " $", Pretty.brk 1,
-                        Codegen.mk_term_of thy false oldT, Pretty.brk 1,
+                        Codegen.mk_term_of thy thyname' false oldT, Pretty.brk 1,
                         Pretty.str "x;"]) ^ "\n\n"
                     else "") ^
                    (if "test" mem !Codegen.mode then
                       Pretty.string_of (Pretty.block [Pretty.str "fun ",
-                        Codegen.mk_gen thy false [] "" newT, Pretty.brk 1,
+                        Codegen.mk_gen thy thyname' false [] "" newT, Pretty.brk 1,
                         Pretty.str "i =", Pretty.brk 1,
                         Pretty.block [Pretty.str (Abs_id ^ " ("),
-                          Codegen.mk_gen thy false [] "" oldT, Pretty.brk 1,
+                          Codegen.mk_gen thy thyname' false [] "" oldT, Pretty.brk 1,
                           Pretty.str "i);"]]) ^ "\n\n"
                     else "")
-               in Graph.map_node Abs_id (K (NONE, s)) gr'' end
+               in Graph.map_node Abs_name (K (NONE, thyname', s)) gr'' end
            in
-             SOME (gr'', mk_tyexpr qs ty_id)
+             SOME (gr'', mk_tyexpr qs ty_call_id)
            end)
-  | typedef_tycodegen thy gr dep brack _ = NONE;
+  | typedef_tycodegen thy defs gr dep thyname brack _ = NONE;
 
 val setup =
   [TypedefData.init,