src/HOL/Tools/typedef_package.ML
changeset 16645 a152d6b21c31
parent 16486 1a12cdb6ee6b
child 17057 0934ac31985f
     1.1 --- a/src/HOL/Tools/typedef_package.ML	Fri Jul 01 14:11:06 2005 +0200
     1.2 +++ b/src/HOL/Tools/typedef_package.ML	Fri Jul 01 14:13:40 2005 +0200
     1.3 @@ -272,17 +272,18 @@
     1.4  
     1.5  (** trivial code generator **)
     1.6  
     1.7 -fun typedef_codegen thy gr dep brack t =
     1.8 +fun typedef_codegen thy defs gr dep thyname brack t =
     1.9    let
    1.10 +    fun get_name (Type (tname, _)) = tname
    1.11 +      | get_name _ = "";
    1.12      fun mk_fun s T ts =
    1.13        let
    1.14 -        val (gr', _) = Codegen.invoke_tycodegen thy dep false (gr, T);
    1.15 +        val (gr', _) = Codegen.invoke_tycodegen thy defs dep thyname false (gr, T);
    1.16          val (gr'', ps) =
    1.17 -          foldl_map (Codegen.invoke_codegen thy dep true) (gr', ts);
    1.18 -        val id = Codegen.mk_const_id thy s
    1.19 +          foldl_map (Codegen.invoke_codegen thy defs dep thyname true) (gr', ts);
    1.20 +        val id = Codegen.mk_const_id thy
    1.21 +          thyname (Codegen.thyname_of_type (get_name T) thy) s
    1.22        in SOME (gr'', Codegen.mk_app brack (Pretty.str id) ps) end;
    1.23 -    fun get_name (Type (tname, _)) = tname
    1.24 -      | get_name _ = "";
    1.25      fun lookup f T = getOpt (Option.map f (Symtab.lookup
    1.26        (TypedefData.get thy, get_name T)), "")
    1.27    in
    1.28 @@ -302,23 +303,25 @@
    1.29    | mk_tyexpr [p] s = Pretty.block [p, Pretty.str (" " ^ s)]
    1.30    | mk_tyexpr ps s = Pretty.list "(" (") " ^ s) ps;
    1.31  
    1.32 -fun typedef_tycodegen thy gr dep brack (Type (s, Ts)) =
    1.33 +fun typedef_tycodegen thy defs gr dep thyname brack (Type (s, Ts)) =
    1.34        (case Symtab.lookup (TypedefData.get thy, s) of
    1.35           NONE => NONE
    1.36         | SOME (newT as Type (tname, Us), oldT, Abs_name, Rep_name) =>
    1.37             if isSome (Codegen.get_assoc_type thy tname) then NONE else
    1.38             let
    1.39 -             val Abs_id = Codegen.mk_const_id thy Abs_name;
    1.40 -             val Rep_id = Codegen.mk_const_id thy Rep_name;
    1.41 -             val ty_id = Codegen.mk_type_id thy s;
    1.42 +             val thyname' = Codegen.thyname_of_type tname thy;
    1.43 +             val Abs_id = Codegen.mk_const_id thy thyname' thyname' Abs_name;
    1.44 +             val Rep_id = Codegen.mk_const_id thy thyname' thyname' Rep_name;
    1.45 +             val ty_id = Codegen.mk_type_id thy thyname' thyname' s;
    1.46 +             val ty_call_id = Codegen.mk_type_id thy thyname thyname' s;
    1.47               val (gr', qs) = foldl_map
    1.48 -               (Codegen.invoke_tycodegen thy dep (length Ts = 1)) (gr, Ts);
    1.49 -             val gr'' = Graph.add_edge (Abs_id, dep) gr' handle Graph.UNDEF _ =>
    1.50 +               (Codegen.invoke_tycodegen thy defs dep thyname (length Ts = 1)) (gr, Ts);
    1.51 +             val gr'' = Graph.add_edge (Abs_name, dep) gr' handle Graph.UNDEF _ =>
    1.52                 let
    1.53                   val (gr'', p :: ps) = foldl_map
    1.54 -                   (Codegen.invoke_tycodegen thy Abs_id false)
    1.55 -                   (Graph.add_edge (Abs_id, dep)
    1.56 -                      (Graph.new_node (Abs_id, (NONE, "")) gr'), oldT :: Us);
    1.57 +                   (Codegen.invoke_tycodegen thy defs Abs_name thyname' false)
    1.58 +                   (Graph.add_edge (Abs_name, dep)
    1.59 +                      (Graph.new_node (Abs_name, (NONE, "", "")) gr'), oldT :: Us);
    1.60                   val s =
    1.61                     Pretty.string_of (Pretty.block [Pretty.str "datatype ",
    1.62                       mk_tyexpr ps ty_id,
    1.63 @@ -329,28 +332,28 @@
    1.64                       Pretty.str "x) = x;"]) ^ "\n\n" ^
    1.65                     (if "term_of" mem !Codegen.mode then
    1.66                        Pretty.string_of (Pretty.block [Pretty.str "fun ",
    1.67 -                        Codegen.mk_term_of thy false newT, Pretty.brk 1,
    1.68 +                        Codegen.mk_term_of thy thyname' false newT, Pretty.brk 1,
    1.69                          Pretty.str ("(" ^ Abs_id), Pretty.brk 1,
    1.70                          Pretty.str "x) =", Pretty.brk 1,
    1.71                          Pretty.block [Pretty.str ("Const (\"" ^ Abs_name ^ "\","),
    1.72                            Pretty.brk 1, Codegen.mk_type false (oldT --> newT),
    1.73                            Pretty.str ")"], Pretty.str " $", Pretty.brk 1,
    1.74 -                        Codegen.mk_term_of thy false oldT, Pretty.brk 1,
    1.75 +                        Codegen.mk_term_of thy thyname' false oldT, Pretty.brk 1,
    1.76                          Pretty.str "x;"]) ^ "\n\n"
    1.77                      else "") ^
    1.78                     (if "test" mem !Codegen.mode then
    1.79                        Pretty.string_of (Pretty.block [Pretty.str "fun ",
    1.80 -                        Codegen.mk_gen thy false [] "" newT, Pretty.brk 1,
    1.81 +                        Codegen.mk_gen thy thyname' false [] "" newT, Pretty.brk 1,
    1.82                          Pretty.str "i =", Pretty.brk 1,
    1.83                          Pretty.block [Pretty.str (Abs_id ^ " ("),
    1.84 -                          Codegen.mk_gen thy false [] "" oldT, Pretty.brk 1,
    1.85 +                          Codegen.mk_gen thy thyname' false [] "" oldT, Pretty.brk 1,
    1.86                            Pretty.str "i);"]]) ^ "\n\n"
    1.87                      else "")
    1.88 -               in Graph.map_node Abs_id (K (NONE, s)) gr'' end
    1.89 +               in Graph.map_node Abs_name (K (NONE, thyname', s)) gr'' end
    1.90             in
    1.91 -             SOME (gr'', mk_tyexpr qs ty_id)
    1.92 +             SOME (gr'', mk_tyexpr qs ty_call_id)
    1.93             end)
    1.94 -  | typedef_tycodegen thy gr dep brack _ = NONE;
    1.95 +  | typedef_tycodegen thy defs gr dep thyname brack _ = NONE;
    1.96  
    1.97  val setup =
    1.98    [TypedefData.init,