Added simple code generator.
authorberghofe
Tue Oct 26 16:30:32 2004 +0200 (2004-10-26)
changeset 152596aa593317905
parent 15258 b93efa469f92
child 15260 a12e999a0113
Added simple code generator.
src/HOL/Tools/typedef_package.ML
     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