src/HOL/Tools/datatype_codegen.ML
author berghofe
Wed, 13 Nov 2002 15:28:41 +0100
changeset 13708 a3a410782c95
parent 12890 75b254b1c8ba
child 13754 021cf00435a9
permissions -rw-r--r--
prove_goal' -> Goal.simple_prove_goal_cterm
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
12446
86887b40aeb1 Tuned header.
berghofe
parents: 12445
diff changeset
     1
(*  Title:      HOL/datatype_codegen.ML
12445
f17eb90bfd16 Code generator for datatypes.
berghofe
parents:
diff changeset
     2
    ID:         $Id$
f17eb90bfd16 Code generator for datatypes.
berghofe
parents:
diff changeset
     3
    Author:     Stefan Berghofer, TU Muenchen
f17eb90bfd16 Code generator for datatypes.
berghofe
parents:
diff changeset
     4
    License:    GPL (GNU GENERAL PUBLIC LICENSE)
f17eb90bfd16 Code generator for datatypes.
berghofe
parents:
diff changeset
     5
f17eb90bfd16 Code generator for datatypes.
berghofe
parents:
diff changeset
     6
Code generator for inductive datatypes.
f17eb90bfd16 Code generator for datatypes.
berghofe
parents:
diff changeset
     7
*)
f17eb90bfd16 Code generator for datatypes.
berghofe
parents:
diff changeset
     8
f17eb90bfd16 Code generator for datatypes.
berghofe
parents:
diff changeset
     9
signature DATATYPE_CODEGEN =
f17eb90bfd16 Code generator for datatypes.
berghofe
parents:
diff changeset
    10
sig
f17eb90bfd16 Code generator for datatypes.
berghofe
parents:
diff changeset
    11
  val setup: (theory -> theory) list
f17eb90bfd16 Code generator for datatypes.
berghofe
parents:
diff changeset
    12
end;
f17eb90bfd16 Code generator for datatypes.
berghofe
parents:
diff changeset
    13
f17eb90bfd16 Code generator for datatypes.
berghofe
parents:
diff changeset
    14
structure DatatypeCodegen : DATATYPE_CODEGEN =
f17eb90bfd16 Code generator for datatypes.
berghofe
parents:
diff changeset
    15
struct
f17eb90bfd16 Code generator for datatypes.
berghofe
parents:
diff changeset
    16
f17eb90bfd16 Code generator for datatypes.
berghofe
parents:
diff changeset
    17
open Codegen;
f17eb90bfd16 Code generator for datatypes.
berghofe
parents:
diff changeset
    18
f17eb90bfd16 Code generator for datatypes.
berghofe
parents:
diff changeset
    19
fun mk_tuple [p] = p
f17eb90bfd16 Code generator for datatypes.
berghofe
parents:
diff changeset
    20
  | mk_tuple ps = Pretty.block (Pretty.str "(" ::
f17eb90bfd16 Code generator for datatypes.
berghofe
parents:
diff changeset
    21
      flat (separate [Pretty.str ",", Pretty.brk 1] (map single ps)) @
f17eb90bfd16 Code generator for datatypes.
berghofe
parents:
diff changeset
    22
        [Pretty.str ")"]);
f17eb90bfd16 Code generator for datatypes.
berghofe
parents:
diff changeset
    23
f17eb90bfd16 Code generator for datatypes.
berghofe
parents:
diff changeset
    24
f17eb90bfd16 Code generator for datatypes.
berghofe
parents:
diff changeset
    25
(**** datatype definition ****)
f17eb90bfd16 Code generator for datatypes.
berghofe
parents:
diff changeset
    26
12890
75b254b1c8ba made MLWorks happy;
wenzelm
parents: 12822
diff changeset
    27
fun add_dt_defs thy dep gr (descr: DatatypeAux.descr) =
12445
f17eb90bfd16 Code generator for datatypes.
berghofe
parents:
diff changeset
    28
  let
f17eb90bfd16 Code generator for datatypes.
berghofe
parents:
diff changeset
    29
    val sg = sign_of thy;
f17eb90bfd16 Code generator for datatypes.
berghofe
parents:
diff changeset
    30
    val tab = DatatypePackage.get_datatypes thy;
f17eb90bfd16 Code generator for datatypes.
berghofe
parents:
diff changeset
    31
f17eb90bfd16 Code generator for datatypes.
berghofe
parents:
diff changeset
    32
    val descr' = filter (can (map DatatypeAux.dest_DtTFree o #2 o snd)) descr;
f17eb90bfd16 Code generator for datatypes.
berghofe
parents:
diff changeset
    33
f17eb90bfd16 Code generator for datatypes.
berghofe
parents:
diff changeset
    34
    val (_, (_, _, (cname, _) :: _)) :: _ = descr';
f17eb90bfd16 Code generator for datatypes.
berghofe
parents:
diff changeset
    35
    val dname = mk_const_id sg cname;
f17eb90bfd16 Code generator for datatypes.
berghofe
parents:
diff changeset
    36
f17eb90bfd16 Code generator for datatypes.
berghofe
parents:
diff changeset
    37
    fun mk_dtdef gr prfx [] = (gr, [])
f17eb90bfd16 Code generator for datatypes.
berghofe
parents:
diff changeset
    38
      | mk_dtdef gr prfx ((_, (tname, dts, cs))::xs) =
f17eb90bfd16 Code generator for datatypes.
berghofe
parents:
diff changeset
    39
          let
f17eb90bfd16 Code generator for datatypes.
berghofe
parents:
diff changeset
    40
            val tvs = map DatatypeAux.dest_DtTFree dts;
f17eb90bfd16 Code generator for datatypes.
berghofe
parents:
diff changeset
    41
            val sorts = map (rpair []) tvs;
f17eb90bfd16 Code generator for datatypes.
berghofe
parents:
diff changeset
    42
            val cs' = map (apsnd (map (DatatypeAux.typ_of_dtyp descr sorts))) cs;
f17eb90bfd16 Code generator for datatypes.
berghofe
parents:
diff changeset
    43
            val (gr', ps) = foldl_map (fn (gr, (cname, cargs)) =>
f17eb90bfd16 Code generator for datatypes.
berghofe
parents:
diff changeset
    44
              apsnd (pair cname) (foldl_map
f17eb90bfd16 Code generator for datatypes.
berghofe
parents:
diff changeset
    45
                (invoke_tycodegen thy dname false) (gr, cargs))) (gr, cs');
f17eb90bfd16 Code generator for datatypes.
berghofe
parents:
diff changeset
    46
            val (gr'', rest) = mk_dtdef gr' "and " xs
f17eb90bfd16 Code generator for datatypes.
berghofe
parents:
diff changeset
    47
          in
f17eb90bfd16 Code generator for datatypes.
berghofe
parents:
diff changeset
    48
            (gr'',
f17eb90bfd16 Code generator for datatypes.
berghofe
parents:
diff changeset
    49
             Pretty.block (Pretty.str prfx ::
f17eb90bfd16 Code generator for datatypes.
berghofe
parents:
diff changeset
    50
               (if null tvs then [] else
f17eb90bfd16 Code generator for datatypes.
berghofe
parents:
diff changeset
    51
                  [mk_tuple (map Pretty.str tvs), Pretty.str " "]) @
f17eb90bfd16 Code generator for datatypes.
berghofe
parents:
diff changeset
    52
               [Pretty.str (mk_type_id sg tname ^ " ="), Pretty.brk 1] @
f17eb90bfd16 Code generator for datatypes.
berghofe
parents:
diff changeset
    53
               flat (separate [Pretty.brk 1, Pretty.str "| "]
f17eb90bfd16 Code generator for datatypes.
berghofe
parents:
diff changeset
    54
                 (map (fn (cname, ps') => [Pretty.block
f17eb90bfd16 Code generator for datatypes.
berghofe
parents:
diff changeset
    55
                   (Pretty.str (mk_const_id sg cname) ::
f17eb90bfd16 Code generator for datatypes.
berghofe
parents:
diff changeset
    56
                    (if null ps' then [] else
f17eb90bfd16 Code generator for datatypes.
berghofe
parents:
diff changeset
    57
                     flat ([Pretty.str " of", Pretty.brk 1] ::
f17eb90bfd16 Code generator for datatypes.
berghofe
parents:
diff changeset
    58
                       separate [Pretty.str " *", Pretty.brk 1]
f17eb90bfd16 Code generator for datatypes.
berghofe
parents:
diff changeset
    59
                         (map single ps'))))]) ps))) :: rest)
f17eb90bfd16 Code generator for datatypes.
berghofe
parents:
diff changeset
    60
          end
f17eb90bfd16 Code generator for datatypes.
berghofe
parents:
diff changeset
    61
  in
f17eb90bfd16 Code generator for datatypes.
berghofe
parents:
diff changeset
    62
    ((Graph.add_edge_acyclic (dname, dep) gr
f17eb90bfd16 Code generator for datatypes.
berghofe
parents:
diff changeset
    63
        handle Graph.CYCLES _ => gr) handle Graph.UNDEF _ =>
f17eb90bfd16 Code generator for datatypes.
berghofe
parents:
diff changeset
    64
         let
f17eb90bfd16 Code generator for datatypes.
berghofe
parents:
diff changeset
    65
           val gr1 = Graph.add_edge (dname, dep)
f17eb90bfd16 Code generator for datatypes.
berghofe
parents:
diff changeset
    66
             (Graph.new_node (dname, (None, "")) gr);
f17eb90bfd16 Code generator for datatypes.
berghofe
parents:
diff changeset
    67
           val (gr2, dtdef) = mk_dtdef gr1 "datatype " descr';
f17eb90bfd16 Code generator for datatypes.
berghofe
parents:
diff changeset
    68
         in
f17eb90bfd16 Code generator for datatypes.
berghofe
parents:
diff changeset
    69
           Graph.map_node dname (K (None,
f17eb90bfd16 Code generator for datatypes.
berghofe
parents:
diff changeset
    70
             Pretty.string_of (Pretty.blk (0, separate Pretty.fbrk dtdef @
f17eb90bfd16 Code generator for datatypes.
berghofe
parents:
diff changeset
    71
               [Pretty.str ";"])) ^ "\n\n")) gr2
f17eb90bfd16 Code generator for datatypes.
berghofe
parents:
diff changeset
    72
         end)
f17eb90bfd16 Code generator for datatypes.
berghofe
parents:
diff changeset
    73
  end;
f17eb90bfd16 Code generator for datatypes.
berghofe
parents:
diff changeset
    74
f17eb90bfd16 Code generator for datatypes.
berghofe
parents:
diff changeset
    75
f17eb90bfd16 Code generator for datatypes.
berghofe
parents:
diff changeset
    76
(**** case expressions ****)
f17eb90bfd16 Code generator for datatypes.
berghofe
parents:
diff changeset
    77
f17eb90bfd16 Code generator for datatypes.
berghofe
parents:
diff changeset
    78
fun pretty_case thy gr dep brack constrs (c as Const (_, T)) ts =
f17eb90bfd16 Code generator for datatypes.
berghofe
parents:
diff changeset
    79
  let val i = length constrs
f17eb90bfd16 Code generator for datatypes.
berghofe
parents:
diff changeset
    80
  in if length ts <= i then
f17eb90bfd16 Code generator for datatypes.
berghofe
parents:
diff changeset
    81
       invoke_codegen thy dep brack (gr, eta_expand c ts (i+1))
f17eb90bfd16 Code generator for datatypes.
berghofe
parents:
diff changeset
    82
    else
f17eb90bfd16 Code generator for datatypes.
berghofe
parents:
diff changeset
    83
      let
f17eb90bfd16 Code generator for datatypes.
berghofe
parents:
diff changeset
    84
        val ts1 = take (i, ts);
f17eb90bfd16 Code generator for datatypes.
berghofe
parents:
diff changeset
    85
        val t :: ts2 = drop (i, ts);
f17eb90bfd16 Code generator for datatypes.
berghofe
parents:
diff changeset
    86
        val names = foldr add_term_names (ts1,
f17eb90bfd16 Code generator for datatypes.
berghofe
parents:
diff changeset
    87
          map (fst o fst o dest_Var) (foldr add_term_vars (ts1, [])));
f17eb90bfd16 Code generator for datatypes.
berghofe
parents:
diff changeset
    88
        val (Ts, dT) = split_last (take (i+1, fst (strip_type T)));
f17eb90bfd16 Code generator for datatypes.
berghofe
parents:
diff changeset
    89
f17eb90bfd16 Code generator for datatypes.
berghofe
parents:
diff changeset
    90
        fun pcase gr [] [] [] = ([], gr)
f17eb90bfd16 Code generator for datatypes.
berghofe
parents:
diff changeset
    91
          | pcase gr ((cname, cargs)::cs) (t::ts) (U::Us) =
f17eb90bfd16 Code generator for datatypes.
berghofe
parents:
diff changeset
    92
              let
f17eb90bfd16 Code generator for datatypes.
berghofe
parents:
diff changeset
    93
                val j = length cargs;
f17eb90bfd16 Code generator for datatypes.
berghofe
parents:
diff changeset
    94
                val xs = variantlist (replicate j "x", names);
f17eb90bfd16 Code generator for datatypes.
berghofe
parents:
diff changeset
    95
                val Us' = take (j, fst (strip_type U));
f17eb90bfd16 Code generator for datatypes.
berghofe
parents:
diff changeset
    96
                val frees = map Free (xs ~~ Us');
f17eb90bfd16 Code generator for datatypes.
berghofe
parents:
diff changeset
    97
                val (gr0, cp) = invoke_codegen thy dep false
f17eb90bfd16 Code generator for datatypes.
berghofe
parents:
diff changeset
    98
                  (gr, list_comb (Const (cname, Us' ---> dT), frees));
f17eb90bfd16 Code generator for datatypes.
berghofe
parents:
diff changeset
    99
                val t' = Envir.beta_norm (list_comb (t, frees));
f17eb90bfd16 Code generator for datatypes.
berghofe
parents:
diff changeset
   100
                val (gr1, p) = invoke_codegen thy dep false (gr0, t');
f17eb90bfd16 Code generator for datatypes.
berghofe
parents:
diff changeset
   101
                val (ps, gr2) = pcase gr1 cs ts Us;
f17eb90bfd16 Code generator for datatypes.
berghofe
parents:
diff changeset
   102
              in
f17eb90bfd16 Code generator for datatypes.
berghofe
parents:
diff changeset
   103
                ([Pretty.block [cp, Pretty.str " =>", Pretty.brk 1, p]] :: ps, gr2)
f17eb90bfd16 Code generator for datatypes.
berghofe
parents:
diff changeset
   104
              end;
f17eb90bfd16 Code generator for datatypes.
berghofe
parents:
diff changeset
   105
f17eb90bfd16 Code generator for datatypes.
berghofe
parents:
diff changeset
   106
        val (ps1, gr1) = pcase gr constrs ts1 Ts;
f17eb90bfd16 Code generator for datatypes.
berghofe
parents:
diff changeset
   107
        val ps = flat (separate [Pretty.brk 1, Pretty.str "| "] ps1);
f17eb90bfd16 Code generator for datatypes.
berghofe
parents:
diff changeset
   108
        val (gr2, p) = invoke_codegen thy dep false (gr1, t);
f17eb90bfd16 Code generator for datatypes.
berghofe
parents:
diff changeset
   109
        val (gr3, ps2) = foldl_map (invoke_codegen thy dep true) (gr2, ts2)
f17eb90bfd16 Code generator for datatypes.
berghofe
parents:
diff changeset
   110
      in (gr3, (if not (null ts2) andalso brack then parens else I)
f17eb90bfd16 Code generator for datatypes.
berghofe
parents:
diff changeset
   111
        (Pretty.block (separate (Pretty.brk 1)
f17eb90bfd16 Code generator for datatypes.
berghofe
parents:
diff changeset
   112
          (Pretty.block ([Pretty.str "(case ", p, Pretty.str " of",
f17eb90bfd16 Code generator for datatypes.
berghofe
parents:
diff changeset
   113
             Pretty.brk 1] @ ps @ [Pretty.str ")"]) :: ps2))))
f17eb90bfd16 Code generator for datatypes.
berghofe
parents:
diff changeset
   114
      end
f17eb90bfd16 Code generator for datatypes.
berghofe
parents:
diff changeset
   115
  end;
f17eb90bfd16 Code generator for datatypes.
berghofe
parents:
diff changeset
   116
f17eb90bfd16 Code generator for datatypes.
berghofe
parents:
diff changeset
   117
f17eb90bfd16 Code generator for datatypes.
berghofe
parents:
diff changeset
   118
(**** constructors ****)
f17eb90bfd16 Code generator for datatypes.
berghofe
parents:
diff changeset
   119
f17eb90bfd16 Code generator for datatypes.
berghofe
parents:
diff changeset
   120
fun pretty_constr thy gr dep brack args (c as Const (s, _)) ts =
f17eb90bfd16 Code generator for datatypes.
berghofe
parents:
diff changeset
   121
  let val i = length args
f17eb90bfd16 Code generator for datatypes.
berghofe
parents:
diff changeset
   122
  in if i > 1 andalso length ts < i then
f17eb90bfd16 Code generator for datatypes.
berghofe
parents:
diff changeset
   123
      invoke_codegen thy dep brack (gr, eta_expand c ts i)
f17eb90bfd16 Code generator for datatypes.
berghofe
parents:
diff changeset
   124
     else
f17eb90bfd16 Code generator for datatypes.
berghofe
parents:
diff changeset
   125
       let
f17eb90bfd16 Code generator for datatypes.
berghofe
parents:
diff changeset
   126
         val id = mk_const_id (sign_of thy) s;
f17eb90bfd16 Code generator for datatypes.
berghofe
parents:
diff changeset
   127
         val (gr', ps) = foldl_map (invoke_codegen thy dep (i = 1)) (gr, ts);
f17eb90bfd16 Code generator for datatypes.
berghofe
parents:
diff changeset
   128
       in (case args of
f17eb90bfd16 Code generator for datatypes.
berghofe
parents:
diff changeset
   129
          _ :: _ :: _ => (gr', (if brack then parens else I)
f17eb90bfd16 Code generator for datatypes.
berghofe
parents:
diff changeset
   130
            (Pretty.block [Pretty.str id, Pretty.brk 1, mk_tuple ps]))
f17eb90bfd16 Code generator for datatypes.
berghofe
parents:
diff changeset
   131
        | _ => (gr', mk_app brack (Pretty.str id) ps))
f17eb90bfd16 Code generator for datatypes.
berghofe
parents:
diff changeset
   132
       end
f17eb90bfd16 Code generator for datatypes.
berghofe
parents:
diff changeset
   133
  end;
f17eb90bfd16 Code generator for datatypes.
berghofe
parents:
diff changeset
   134
f17eb90bfd16 Code generator for datatypes.
berghofe
parents:
diff changeset
   135
f17eb90bfd16 Code generator for datatypes.
berghofe
parents:
diff changeset
   136
(**** code generators for terms and types ****)
f17eb90bfd16 Code generator for datatypes.
berghofe
parents:
diff changeset
   137
f17eb90bfd16 Code generator for datatypes.
berghofe
parents:
diff changeset
   138
fun datatype_codegen thy gr dep brack t = (case strip_comb t of
f17eb90bfd16 Code generator for datatypes.
berghofe
parents:
diff changeset
   139
   (c as Const (s, T), ts) =>
f17eb90bfd16 Code generator for datatypes.
berghofe
parents:
diff changeset
   140
       (case find_first (fn (_, {index, descr, case_name, ...}) =>
f17eb90bfd16 Code generator for datatypes.
berghofe
parents:
diff changeset
   141
         s = case_name orelse
f17eb90bfd16 Code generator for datatypes.
berghofe
parents:
diff changeset
   142
           is_some (assoc (#3 (the (assoc (descr, index))), s)))
f17eb90bfd16 Code generator for datatypes.
berghofe
parents:
diff changeset
   143
             (Symtab.dest (DatatypePackage.get_datatypes thy)) of
f17eb90bfd16 Code generator for datatypes.
berghofe
parents:
diff changeset
   144
          None => None
f17eb90bfd16 Code generator for datatypes.
berghofe
parents:
diff changeset
   145
        | Some (tname, {index, descr, ...}) =>
f17eb90bfd16 Code generator for datatypes.
berghofe
parents:
diff changeset
   146
           if is_some (get_assoc_code thy s T) then None else
f17eb90bfd16 Code generator for datatypes.
berghofe
parents:
diff changeset
   147
           let val Some (_, _, constrs) = assoc (descr, index)
12822
073116d65bb9 datatype_codegen now checks type of constructor.
berghofe
parents: 12446
diff changeset
   148
           in (case (assoc (constrs, s), strip_type T) of
073116d65bb9 datatype_codegen now checks type of constructor.
berghofe
parents: 12446
diff changeset
   149
               (None, _) => Some (pretty_case thy gr dep brack
12445
f17eb90bfd16 Code generator for datatypes.
berghofe
parents:
diff changeset
   150
                 (#3 (the (assoc (descr, index)))) c ts)
12822
073116d65bb9 datatype_codegen now checks type of constructor.
berghofe
parents: 12446
diff changeset
   151
             | (Some args, (_, Type _)) => Some (pretty_constr thy
12445
f17eb90bfd16 Code generator for datatypes.
berghofe
parents:
diff changeset
   152
                 (fst (invoke_tycodegen thy dep false (gr, snd (strip_type T))))
12822
073116d65bb9 datatype_codegen now checks type of constructor.
berghofe
parents: 12446
diff changeset
   153
                 dep brack args c ts)
073116d65bb9 datatype_codegen now checks type of constructor.
berghofe
parents: 12446
diff changeset
   154
             | _ => None)
12445
f17eb90bfd16 Code generator for datatypes.
berghofe
parents:
diff changeset
   155
           end)
f17eb90bfd16 Code generator for datatypes.
berghofe
parents:
diff changeset
   156
 |  _ => None);
f17eb90bfd16 Code generator for datatypes.
berghofe
parents:
diff changeset
   157
f17eb90bfd16 Code generator for datatypes.
berghofe
parents:
diff changeset
   158
fun datatype_tycodegen thy gr dep brack (Type (s, Ts)) =
f17eb90bfd16 Code generator for datatypes.
berghofe
parents:
diff changeset
   159
      (case Symtab.lookup (DatatypePackage.get_datatypes thy, s) of
f17eb90bfd16 Code generator for datatypes.
berghofe
parents:
diff changeset
   160
         None => None
f17eb90bfd16 Code generator for datatypes.
berghofe
parents:
diff changeset
   161
       | Some {descr, ...} =>
f17eb90bfd16 Code generator for datatypes.
berghofe
parents:
diff changeset
   162
           if is_some (get_assoc_type thy s) then None else
f17eb90bfd16 Code generator for datatypes.
berghofe
parents:
diff changeset
   163
           let val (gr', ps) = foldl_map
f17eb90bfd16 Code generator for datatypes.
berghofe
parents:
diff changeset
   164
             (invoke_tycodegen thy dep false) (gr, Ts)
f17eb90bfd16 Code generator for datatypes.
berghofe
parents:
diff changeset
   165
           in Some (add_dt_defs thy dep gr' descr,
f17eb90bfd16 Code generator for datatypes.
berghofe
parents:
diff changeset
   166
             Pretty.block ((if null Ts then [] else
f17eb90bfd16 Code generator for datatypes.
berghofe
parents:
diff changeset
   167
               [mk_tuple ps, Pretty.str " "]) @
f17eb90bfd16 Code generator for datatypes.
berghofe
parents:
diff changeset
   168
               [Pretty.str (mk_type_id (sign_of thy) s)]))
f17eb90bfd16 Code generator for datatypes.
berghofe
parents:
diff changeset
   169
           end)
f17eb90bfd16 Code generator for datatypes.
berghofe
parents:
diff changeset
   170
  | datatype_tycodegen _ _ _ _ _ = None;
f17eb90bfd16 Code generator for datatypes.
berghofe
parents:
diff changeset
   171
f17eb90bfd16 Code generator for datatypes.
berghofe
parents:
diff changeset
   172
f17eb90bfd16 Code generator for datatypes.
berghofe
parents:
diff changeset
   173
val setup =
f17eb90bfd16 Code generator for datatypes.
berghofe
parents:
diff changeset
   174
  [add_codegen "datatype" datatype_codegen,
f17eb90bfd16 Code generator for datatypes.
berghofe
parents:
diff changeset
   175
   add_tycodegen "datatype" datatype_tycodegen];
f17eb90bfd16 Code generator for datatypes.
berghofe
parents:
diff changeset
   176
f17eb90bfd16 Code generator for datatypes.
berghofe
parents:
diff changeset
   177
end;