# HG changeset patch # User berghofe # Date 1098801032 -7200 # Node ID 6aa5933179056fdea08b323316a08d5203e5c37f # Parent b93efa469f92396fbd6e8c65c6bfbcae46e8e588 Added simple code generator. diff -r b93efa469f92 -r 6aa593317905 src/HOL/Tools/typedef_package.ML --- a/src/HOL/Tools/typedef_package.ML Tue Oct 26 16:29:54 2004 +0200 +++ b/src/HOL/Tools/typedef_package.ML Tue Oct 26 16:30:32 2004 +0200 @@ -25,6 +25,7 @@ * (string * string) option -> bool -> theory -> ProofHistory.T val typedef_proof_i: (bool * string) * (bstring * string list * mixfix) * term * (string * string) option -> bool -> theory -> ProofHistory.T + val setup: (theory -> theory) list end; structure TypedefPackage: TYPEDEF_PACKAGE = @@ -47,6 +48,28 @@ +(** theory data **) + +structure TypedefArgs = +struct + val name = "HOL/typedef"; + type T = (typ * typ * string * string) Symtab.table; + val empty = Symtab.empty; + val copy = I; + val prep_ext = I; + val merge = Symtab.merge op =; + fun print sg _ = (); +end; + +structure TypedefData = TheoryDataFun(TypedefArgs); + +fun put_typedef newT oldT Abs_name Rep_name thy = + TypedefData.put (Symtab.update_new + ((fst (dest_Type newT), (newT, oldT, Abs_name, Rep_name)), + TypedefData.get thy)) thy; + + + (** type declarations **) fun add_typedecls decls thy = @@ -143,6 +166,7 @@ fun typedef_result (theory, nonempty) = theory + |> put_typedef newT oldT (full Abs_name) (full Rep_name) |> add_typedecls [(t, vs, mx)] |> Theory.add_consts_i ((if def then [(name, setT, NoSyn)] else []) @ @@ -250,6 +274,96 @@ +(** trivial code generator **) + +fun typedef_codegen thy gr dep brack t = + let + fun mk_fun s T ts = + let + val (gr', _) = Codegen.invoke_tycodegen thy dep false (gr, T); + val (gr'', ps) = + foldl_map (Codegen.invoke_codegen thy dep true) (gr', ts); + val id = Codegen.mk_const_id (sign_of 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 = if_none (apsome f (Symtab.lookup + (TypedefData.get thy, get_name T))) "" + in + (case strip_comb t of + (Const (s, Type ("fun", [T, U])), ts) => + if lookup #4 T = s andalso + is_none (Codegen.get_assoc_type thy (get_name T)) + then mk_fun s T ts + else if lookup #3 U = s andalso + is_none (Codegen.get_assoc_type thy (get_name U)) + then mk_fun s U ts + else None + | _ => None) + end; + +fun mk_tyexpr [] s = Pretty.str s + | 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)) = + (case Symtab.lookup (TypedefData.get thy, s) of + None => None + | Some (newT as Type (tname, Us), oldT, Abs_name, Rep_name) => + if is_some (Codegen.get_assoc_type thy tname) then None else + let + val sg = sign_of thy; + val Abs_id = Codegen.mk_const_id sg Abs_name; + val Rep_id = Codegen.mk_const_id sg Rep_name; + val ty_id = Codegen.mk_type_id sg 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 _ => + 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); + val s = + Pretty.string_of (Pretty.block [Pretty.str "datatype ", + mk_tyexpr ps ty_id, + Pretty.str " =", Pretty.brk 1, Pretty.str (Abs_id ^ " of"), + Pretty.brk 1, p, Pretty.str ";"]) ^ "\n\n" ^ + Pretty.string_of (Pretty.block [Pretty.str ("fun " ^ Rep_id), + Pretty.brk 1, Pretty.str ("(" ^ Abs_id), Pretty.brk 1, + 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 sg 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 sg 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 sg false [] "" newT, Pretty.brk 1, + Pretty.str "i =", Pretty.brk 1, + Pretty.block [Pretty.str (Abs_id ^ " ("), + Codegen.mk_gen sg false [] "" oldT, Pretty.brk 1, + Pretty.str "i);"]]) ^ "\n\n" + else "") + in Graph.map_node Abs_id (K (None, s)) gr'' end + in + Some (gr'', mk_tyexpr qs ty_id) + end) + | typedef_tycodegen thy gr dep brack _ = None; + +val setup = + [TypedefData.init, + Codegen.add_codegen "typedef" typedef_codegen, + Codegen.add_tycodegen "typedef" typedef_tycodegen]; + + + (** outer syntax **) local structure P = OuterParse and K = OuterSyntax.Keyword in