1.1 --- a/src/HOL/Tools/typedef_package.ML Tue Oct 26 16:29:54 2004 +0200
1.2 +++ b/src/HOL/Tools/typedef_package.ML Tue Oct 26 16:30:32 2004 +0200
1.3 @@ -25,6 +25,7 @@
1.4 * (string * string) option -> bool -> theory -> ProofHistory.T
1.5 val typedef_proof_i: (bool * string) * (bstring * string list * mixfix) * term
1.6 * (string * string) option -> bool -> theory -> ProofHistory.T
1.7 + val setup: (theory -> theory) list
1.8 end;
1.9
1.10 structure TypedefPackage: TYPEDEF_PACKAGE =
1.11 @@ -47,6 +48,28 @@
1.12
1.13
1.14
1.15 +(** theory data **)
1.16 +
1.17 +structure TypedefArgs =
1.18 +struct
1.19 + val name = "HOL/typedef";
1.20 + type T = (typ * typ * string * string) Symtab.table;
1.21 + val empty = Symtab.empty;
1.22 + val copy = I;
1.23 + val prep_ext = I;
1.24 + val merge = Symtab.merge op =;
1.25 + fun print sg _ = ();
1.26 +end;
1.27 +
1.28 +structure TypedefData = TheoryDataFun(TypedefArgs);
1.29 +
1.30 +fun put_typedef newT oldT Abs_name Rep_name thy =
1.31 + TypedefData.put (Symtab.update_new
1.32 + ((fst (dest_Type newT), (newT, oldT, Abs_name, Rep_name)),
1.33 + TypedefData.get thy)) thy;
1.34 +
1.35 +
1.36 +
1.37 (** type declarations **)
1.38
1.39 fun add_typedecls decls thy =
1.40 @@ -143,6 +166,7 @@
1.41
1.42 fun typedef_result (theory, nonempty) =
1.43 theory
1.44 + |> put_typedef newT oldT (full Abs_name) (full Rep_name)
1.45 |> add_typedecls [(t, vs, mx)]
1.46 |> Theory.add_consts_i
1.47 ((if def then [(name, setT, NoSyn)] else []) @
1.48 @@ -250,6 +274,96 @@
1.49
1.50
1.51
1.52 +(** trivial code generator **)
1.53 +
1.54 +fun typedef_codegen thy gr dep brack t =
1.55 + let
1.56 + fun mk_fun s T ts =
1.57 + let
1.58 + val (gr', _) = Codegen.invoke_tycodegen thy dep false (gr, T);
1.59 + val (gr'', ps) =
1.60 + foldl_map (Codegen.invoke_codegen thy dep true) (gr', ts);
1.61 + val id = Codegen.mk_const_id (sign_of thy) s
1.62 + in Some (gr'', Codegen.mk_app brack (Pretty.str id) ps) end;
1.63 + fun get_name (Type (tname, _)) = tname
1.64 + | get_name _ = "";
1.65 + fun lookup f T = if_none (apsome f (Symtab.lookup
1.66 + (TypedefData.get thy, get_name T))) ""
1.67 + in
1.68 + (case strip_comb t of
1.69 + (Const (s, Type ("fun", [T, U])), ts) =>
1.70 + if lookup #4 T = s andalso
1.71 + is_none (Codegen.get_assoc_type thy (get_name T))
1.72 + then mk_fun s T ts
1.73 + else if lookup #3 U = s andalso
1.74 + is_none (Codegen.get_assoc_type thy (get_name U))
1.75 + then mk_fun s U ts
1.76 + else None
1.77 + | _ => None)
1.78 + end;
1.79 +
1.80 +fun mk_tyexpr [] s = Pretty.str s
1.81 + | mk_tyexpr [p] s = Pretty.block [p, Pretty.str (" " ^ s)]
1.82 + | mk_tyexpr ps s = Pretty.list "(" (") " ^ s) ps;
1.83 +
1.84 +fun typedef_tycodegen thy gr dep brack (Type (s, Ts)) =
1.85 + (case Symtab.lookup (TypedefData.get thy, s) of
1.86 + None => None
1.87 + | Some (newT as Type (tname, Us), oldT, Abs_name, Rep_name) =>
1.88 + if is_some (Codegen.get_assoc_type thy tname) then None else
1.89 + let
1.90 + val sg = sign_of thy;
1.91 + val Abs_id = Codegen.mk_const_id sg Abs_name;
1.92 + val Rep_id = Codegen.mk_const_id sg Rep_name;
1.93 + val ty_id = Codegen.mk_type_id sg s;
1.94 + val (gr', qs) = foldl_map
1.95 + (Codegen.invoke_tycodegen thy dep (length Ts = 1)) (gr, Ts);
1.96 + val gr'' = Graph.add_edge (Abs_id, dep) gr' handle Graph.UNDEF _ =>
1.97 + let
1.98 + val (gr'', p :: ps) = foldl_map
1.99 + (Codegen.invoke_tycodegen thy Abs_id false)
1.100 + (Graph.add_edge (Abs_id, dep)
1.101 + (Graph.new_node (Abs_id, (None, "")) gr'), oldT :: Us);
1.102 + val s =
1.103 + Pretty.string_of (Pretty.block [Pretty.str "datatype ",
1.104 + mk_tyexpr ps ty_id,
1.105 + Pretty.str " =", Pretty.brk 1, Pretty.str (Abs_id ^ " of"),
1.106 + Pretty.brk 1, p, Pretty.str ";"]) ^ "\n\n" ^
1.107 + Pretty.string_of (Pretty.block [Pretty.str ("fun " ^ Rep_id),
1.108 + Pretty.brk 1, Pretty.str ("(" ^ Abs_id), Pretty.brk 1,
1.109 + Pretty.str "x) = x;"]) ^ "\n\n" ^
1.110 + (if "term_of" mem !Codegen.mode then
1.111 + Pretty.string_of (Pretty.block [Pretty.str "fun ",
1.112 + Codegen.mk_term_of sg false newT, Pretty.brk 1,
1.113 + Pretty.str ("(" ^ Abs_id), Pretty.brk 1,
1.114 + Pretty.str "x) =", Pretty.brk 1,
1.115 + Pretty.block [Pretty.str ("Const (\"" ^ Abs_name ^ "\","),
1.116 + Pretty.brk 1, Codegen.mk_type false (oldT --> newT),
1.117 + Pretty.str ")"], Pretty.str " $", Pretty.brk 1,
1.118 + Codegen.mk_term_of sg false oldT, Pretty.brk 1,
1.119 + Pretty.str "x;"]) ^ "\n\n"
1.120 + else "") ^
1.121 + (if "test" mem !Codegen.mode then
1.122 + Pretty.string_of (Pretty.block [Pretty.str "fun ",
1.123 + Codegen.mk_gen sg false [] "" newT, Pretty.brk 1,
1.124 + Pretty.str "i =", Pretty.brk 1,
1.125 + Pretty.block [Pretty.str (Abs_id ^ " ("),
1.126 + Codegen.mk_gen sg false [] "" oldT, Pretty.brk 1,
1.127 + Pretty.str "i);"]]) ^ "\n\n"
1.128 + else "")
1.129 + in Graph.map_node Abs_id (K (None, s)) gr'' end
1.130 + in
1.131 + Some (gr'', mk_tyexpr qs ty_id)
1.132 + end)
1.133 + | typedef_tycodegen thy gr dep brack _ = None;
1.134 +
1.135 +val setup =
1.136 + [TypedefData.init,
1.137 + Codegen.add_codegen "typedef" typedef_codegen,
1.138 + Codegen.add_tycodegen "typedef" typedef_tycodegen];
1.139 +
1.140 +
1.141 +
1.142 (** outer syntax **)
1.143
1.144 local structure P = OuterParse and K = OuterSyntax.Keyword in