src/HOL/Tools/typedef_codegen.ML
author haftmann
Thu, 08 Jul 2010 16:19:24 +0200
changeset 37744 3daaf23b9ab4
parent 36692 54b64d4ad524
permissions -rw-r--r--
tuned titles
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
19459
2041d472fc17 seperated typedef codegen from main code
haftmann
parents:
diff changeset
     1
(*  Title:      HOL/Tools/typedef_codegen.ML
31597
9a59cf39ee78 tuned author list
haftmann
parents: 28537
diff changeset
     2
    Author:     Stefan Berghofer, TU Muenchen
19459
2041d472fc17 seperated typedef codegen from main code
haftmann
parents:
diff changeset
     3
2041d472fc17 seperated typedef codegen from main code
haftmann
parents:
diff changeset
     4
Code generators for trivial typedefs.
2041d472fc17 seperated typedef codegen from main code
haftmann
parents:
diff changeset
     5
*)
2041d472fc17 seperated typedef codegen from main code
haftmann
parents:
diff changeset
     6
2041d472fc17 seperated typedef codegen from main code
haftmann
parents:
diff changeset
     7
signature TYPEDEF_CODEGEN =
2041d472fc17 seperated typedef codegen from main code
haftmann
parents:
diff changeset
     8
sig
20428
67fa1c6ba89e refinements
haftmann
parents: 20354
diff changeset
     9
  val setup: theory -> theory
19459
2041d472fc17 seperated typedef codegen from main code
haftmann
parents:
diff changeset
    10
end;
2041d472fc17 seperated typedef codegen from main code
haftmann
parents:
diff changeset
    11
2041d472fc17 seperated typedef codegen from main code
haftmann
parents:
diff changeset
    12
structure TypedefCodegen: TYPEDEF_CODEGEN =
2041d472fc17 seperated typedef codegen from main code
haftmann
parents:
diff changeset
    13
struct
2041d472fc17 seperated typedef codegen from main code
haftmann
parents:
diff changeset
    14
28537
1e84256d1a8a established canonical argument order in SML code generators
haftmann
parents: 27398
diff changeset
    15
fun typedef_codegen thy defs dep module brack t gr =
19459
2041d472fc17 seperated typedef codegen from main code
haftmann
parents:
diff changeset
    16
  let
2041d472fc17 seperated typedef codegen from main code
haftmann
parents:
diff changeset
    17
    fun get_name (Type (tname, _)) = tname
2041d472fc17 seperated typedef codegen from main code
haftmann
parents:
diff changeset
    18
      | get_name _ = "";
2041d472fc17 seperated typedef codegen from main code
haftmann
parents:
diff changeset
    19
    fun mk_fun s T ts =
2041d472fc17 seperated typedef codegen from main code
haftmann
parents:
diff changeset
    20
      let
28537
1e84256d1a8a established canonical argument order in SML code generators
haftmann
parents: 27398
diff changeset
    21
        val (_, gr') = Codegen.invoke_tycodegen thy defs dep module false T gr;
1e84256d1a8a established canonical argument order in SML code generators
haftmann
parents: 27398
diff changeset
    22
        val (ps, gr'') =
1e84256d1a8a established canonical argument order in SML code generators
haftmann
parents: 27398
diff changeset
    23
          fold_map (Codegen.invoke_codegen thy defs dep module true) ts gr';
1e84256d1a8a established canonical argument order in SML code generators
haftmann
parents: 27398
diff changeset
    24
        val id = Codegen.mk_qual_id module (Codegen.get_const_id gr'' s)
1e84256d1a8a established canonical argument order in SML code generators
haftmann
parents: 27398
diff changeset
    25
      in SOME (Codegen.mk_app brack (Codegen.str id) ps, gr'') end;
19459
2041d472fc17 seperated typedef codegen from main code
haftmann
parents:
diff changeset
    26
    fun lookup f T =
35743
c506c029a082 adapted to localized typedef: handle single global interpretation only;
wenzelm
parents: 31723
diff changeset
    27
      (* FIXME handle multiple typedef interpretations (!??) *)
c506c029a082 adapted to localized typedef: handle single global interpretation only;
wenzelm
parents: 31723
diff changeset
    28
      (case Typedef.get_info_global thy (get_name T) of
c506c029a082 adapted to localized typedef: handle single global interpretation only;
wenzelm
parents: 31723
diff changeset
    29
        [info] => f info
c506c029a082 adapted to localized typedef: handle single global interpretation only;
wenzelm
parents: 31723
diff changeset
    30
      | _ => "");
19459
2041d472fc17 seperated typedef codegen from main code
haftmann
parents:
diff changeset
    31
  in
2041d472fc17 seperated typedef codegen from main code
haftmann
parents:
diff changeset
    32
    (case strip_comb t of
2041d472fc17 seperated typedef codegen from main code
haftmann
parents:
diff changeset
    33
       (Const (s, Type ("fun", [T, U])), ts) =>
35994
9cc3df9a606e Typedef.info: separate global and local part, only the latter is transformed by morphisms;
wenzelm
parents: 35743
diff changeset
    34
         if lookup (#Rep_name o #1) T = s andalso
19459
2041d472fc17 seperated typedef codegen from main code
haftmann
parents:
diff changeset
    35
           is_none (Codegen.get_assoc_type thy (get_name T))
2041d472fc17 seperated typedef codegen from main code
haftmann
parents:
diff changeset
    36
         then mk_fun s T ts
35994
9cc3df9a606e Typedef.info: separate global and local part, only the latter is transformed by morphisms;
wenzelm
parents: 35743
diff changeset
    37
         else if lookup (#Abs_name o #1) U = s andalso
19459
2041d472fc17 seperated typedef codegen from main code
haftmann
parents:
diff changeset
    38
           is_none (Codegen.get_assoc_type thy (get_name U))
2041d472fc17 seperated typedef codegen from main code
haftmann
parents:
diff changeset
    39
         then mk_fun s U ts
2041d472fc17 seperated typedef codegen from main code
haftmann
parents:
diff changeset
    40
         else NONE
2041d472fc17 seperated typedef codegen from main code
haftmann
parents:
diff changeset
    41
     | _ => NONE)
2041d472fc17 seperated typedef codegen from main code
haftmann
parents:
diff changeset
    42
  end;
2041d472fc17 seperated typedef codegen from main code
haftmann
parents:
diff changeset
    43
26975
103dca19ef2e Replaced Pretty.str and Pretty.string_of by specific functions (from Codegen) that
berghofe
parents: 20597
diff changeset
    44
fun mk_tyexpr [] s = Codegen.str s
103dca19ef2e Replaced Pretty.str and Pretty.string_of by specific functions (from Codegen) that
berghofe
parents: 20597
diff changeset
    45
  | mk_tyexpr [p] s = Pretty.block [p, Codegen.str (" " ^ s)]
19459
2041d472fc17 seperated typedef codegen from main code
haftmann
parents:
diff changeset
    46
  | mk_tyexpr ps s = Pretty.list "(" (") " ^ s) ps;
2041d472fc17 seperated typedef codegen from main code
haftmann
parents:
diff changeset
    47
28537
1e84256d1a8a established canonical argument order in SML code generators
haftmann
parents: 27398
diff changeset
    48
fun typedef_tycodegen thy defs dep module brack (Type (s, Ts)) gr =
35743
c506c029a082 adapted to localized typedef: handle single global interpretation only;
wenzelm
parents: 31723
diff changeset
    49
      (case Typedef.get_info_global thy s of
c506c029a082 adapted to localized typedef: handle single global interpretation only;
wenzelm
parents: 31723
diff changeset
    50
        (* FIXME handle multiple typedef interpretations (!??) *)
35994
9cc3df9a606e Typedef.info: separate global and local part, only the latter is transformed by morphisms;
wenzelm
parents: 35743
diff changeset
    51
        [({abs_type as newT as Type (tname, Us), rep_type = oldT, Abs_name, Rep_name, ...}, _)] =>
35743
c506c029a082 adapted to localized typedef: handle single global interpretation only;
wenzelm
parents: 31723
diff changeset
    52
          if is_some (Codegen.get_assoc_type thy tname) then NONE
c506c029a082 adapted to localized typedef: handle single global interpretation only;
wenzelm
parents: 31723
diff changeset
    53
          else
c506c029a082 adapted to localized typedef: handle single global interpretation only;
wenzelm
parents: 31723
diff changeset
    54
            let
c506c029a082 adapted to localized typedef: handle single global interpretation only;
wenzelm
parents: 31723
diff changeset
    55
              val module' = Codegen.if_library
c506c029a082 adapted to localized typedef: handle single global interpretation only;
wenzelm
parents: 31723
diff changeset
    56
                (Codegen.thyname_of_type thy tname) module;
c506c029a082 adapted to localized typedef: handle single global interpretation only;
wenzelm
parents: 31723
diff changeset
    57
              val node_id = tname ^ " (type)";
c506c029a082 adapted to localized typedef: handle single global interpretation only;
wenzelm
parents: 31723
diff changeset
    58
              val ((((qs, (_, Abs_id)), (_, Rep_id)), ty_id), gr') = gr |> fold_map
c506c029a082 adapted to localized typedef: handle single global interpretation only;
wenzelm
parents: 31723
diff changeset
    59
                  (Codegen.invoke_tycodegen thy defs dep module (length Ts = 1))
c506c029a082 adapted to localized typedef: handle single global interpretation only;
wenzelm
parents: 31723
diff changeset
    60
                    Ts ||>>
c506c029a082 adapted to localized typedef: handle single global interpretation only;
wenzelm
parents: 31723
diff changeset
    61
                Codegen.mk_const_id module' Abs_name ||>>
c506c029a082 adapted to localized typedef: handle single global interpretation only;
wenzelm
parents: 31723
diff changeset
    62
                Codegen.mk_const_id module' Rep_name ||>>
c506c029a082 adapted to localized typedef: handle single global interpretation only;
wenzelm
parents: 31723
diff changeset
    63
                Codegen.mk_type_id module' s;
c506c029a082 adapted to localized typedef: handle single global interpretation only;
wenzelm
parents: 31723
diff changeset
    64
              val tyexpr = mk_tyexpr qs (Codegen.mk_qual_id module ty_id)
c506c029a082 adapted to localized typedef: handle single global interpretation only;
wenzelm
parents: 31723
diff changeset
    65
            in
c506c029a082 adapted to localized typedef: handle single global interpretation only;
wenzelm
parents: 31723
diff changeset
    66
              SOME (tyexpr, case try (Codegen.get_node gr') node_id of
c506c029a082 adapted to localized typedef: handle single global interpretation only;
wenzelm
parents: 31723
diff changeset
    67
                NONE =>
c506c029a082 adapted to localized typedef: handle single global interpretation only;
wenzelm
parents: 31723
diff changeset
    68
                  let
c506c029a082 adapted to localized typedef: handle single global interpretation only;
wenzelm
parents: 31723
diff changeset
    69
                    val (p :: ps, gr'') = fold_map
c506c029a082 adapted to localized typedef: handle single global interpretation only;
wenzelm
parents: 31723
diff changeset
    70
                      (Codegen.invoke_tycodegen thy defs node_id module' false)
c506c029a082 adapted to localized typedef: handle single global interpretation only;
wenzelm
parents: 31723
diff changeset
    71
                      (oldT :: Us) (Codegen.add_edge (node_id, dep)
c506c029a082 adapted to localized typedef: handle single global interpretation only;
wenzelm
parents: 31723
diff changeset
    72
                        (Codegen.new_node (node_id, (NONE, "", "")) gr'));
c506c029a082 adapted to localized typedef: handle single global interpretation only;
wenzelm
parents: 31723
diff changeset
    73
                    val s =
c506c029a082 adapted to localized typedef: handle single global interpretation only;
wenzelm
parents: 31723
diff changeset
    74
                      Codegen.string_of (Pretty.block [Codegen.str "datatype ",
c506c029a082 adapted to localized typedef: handle single global interpretation only;
wenzelm
parents: 31723
diff changeset
    75
                        mk_tyexpr ps (snd ty_id),
c506c029a082 adapted to localized typedef: handle single global interpretation only;
wenzelm
parents: 31723
diff changeset
    76
                        Codegen.str " =", Pretty.brk 1, Codegen.str (Abs_id ^ " of"),
c506c029a082 adapted to localized typedef: handle single global interpretation only;
wenzelm
parents: 31723
diff changeset
    77
                        Pretty.brk 1, p, Codegen.str ";"]) ^ "\n\n" ^
c506c029a082 adapted to localized typedef: handle single global interpretation only;
wenzelm
parents: 31723
diff changeset
    78
                      Codegen.string_of (Pretty.block [Codegen.str ("fun " ^ Rep_id),
c506c029a082 adapted to localized typedef: handle single global interpretation only;
wenzelm
parents: 31723
diff changeset
    79
                        Pretty.brk 1, Codegen.str ("(" ^ Abs_id), Pretty.brk 1,
c506c029a082 adapted to localized typedef: handle single global interpretation only;
wenzelm
parents: 31723
diff changeset
    80
                        Codegen.str "x) = x;"]) ^ "\n\n" ^
36692
54b64d4ad524 farewell to old-style mem infixes -- type inference in situations with mem_int and mem_string should provide enough information to resolve the type of (op =)
haftmann
parents: 35994
diff changeset
    81
                      (if member (op =) (!Codegen.mode) "term_of" then
35743
c506c029a082 adapted to localized typedef: handle single global interpretation only;
wenzelm
parents: 31723
diff changeset
    82
                        Codegen.string_of (Pretty.block [Codegen.str "fun ",
c506c029a082 adapted to localized typedef: handle single global interpretation only;
wenzelm
parents: 31723
diff changeset
    83
                          Codegen.mk_term_of gr'' module' false newT, Pretty.brk 1,
c506c029a082 adapted to localized typedef: handle single global interpretation only;
wenzelm
parents: 31723
diff changeset
    84
                          Codegen.str ("(" ^ Abs_id), Pretty.brk 1,
c506c029a082 adapted to localized typedef: handle single global interpretation only;
wenzelm
parents: 31723
diff changeset
    85
                          Codegen.str "x) =", Pretty.brk 1,
c506c029a082 adapted to localized typedef: handle single global interpretation only;
wenzelm
parents: 31723
diff changeset
    86
                          Pretty.block [Codegen.str ("Const (\"" ^ Abs_name ^ "\","),
c506c029a082 adapted to localized typedef: handle single global interpretation only;
wenzelm
parents: 31723
diff changeset
    87
                            Pretty.brk 1, Codegen.mk_type false (oldT --> newT),
c506c029a082 adapted to localized typedef: handle single global interpretation only;
wenzelm
parents: 31723
diff changeset
    88
                            Codegen.str ")"], Codegen.str " $", Pretty.brk 1,
c506c029a082 adapted to localized typedef: handle single global interpretation only;
wenzelm
parents: 31723
diff changeset
    89
                          Codegen.mk_term_of gr'' module' false oldT, Pretty.brk 1,
c506c029a082 adapted to localized typedef: handle single global interpretation only;
wenzelm
parents: 31723
diff changeset
    90
                          Codegen.str "x;"]) ^ "\n\n"
c506c029a082 adapted to localized typedef: handle single global interpretation only;
wenzelm
parents: 31723
diff changeset
    91
                       else "") ^
36692
54b64d4ad524 farewell to old-style mem infixes -- type inference in situations with mem_int and mem_string should provide enough information to resolve the type of (op =)
haftmann
parents: 35994
diff changeset
    92
                      (if member (op =) (!Codegen.mode) "test" then
35743
c506c029a082 adapted to localized typedef: handle single global interpretation only;
wenzelm
parents: 31723
diff changeset
    93
                        Codegen.string_of (Pretty.block [Codegen.str "fun ",
c506c029a082 adapted to localized typedef: handle single global interpretation only;
wenzelm
parents: 31723
diff changeset
    94
                          Codegen.mk_gen gr'' module' false [] "" newT, Pretty.brk 1,
c506c029a082 adapted to localized typedef: handle single global interpretation only;
wenzelm
parents: 31723
diff changeset
    95
                          Codegen.str "i =", Pretty.brk 1,
c506c029a082 adapted to localized typedef: handle single global interpretation only;
wenzelm
parents: 31723
diff changeset
    96
                          Pretty.block [Codegen.str (Abs_id ^ " ("),
c506c029a082 adapted to localized typedef: handle single global interpretation only;
wenzelm
parents: 31723
diff changeset
    97
                            Codegen.mk_gen gr'' module' false [] "" oldT, Pretty.brk 1,
c506c029a082 adapted to localized typedef: handle single global interpretation only;
wenzelm
parents: 31723
diff changeset
    98
                            Codegen.str "i);"]]) ^ "\n\n"
c506c029a082 adapted to localized typedef: handle single global interpretation only;
wenzelm
parents: 31723
diff changeset
    99
                       else "")
c506c029a082 adapted to localized typedef: handle single global interpretation only;
wenzelm
parents: 31723
diff changeset
   100
                  in Codegen.map_node node_id (K (NONE, module', s)) gr'' end
c506c029a082 adapted to localized typedef: handle single global interpretation only;
wenzelm
parents: 31723
diff changeset
   101
              | SOME _ => Codegen.add_edge (node_id, dep) gr')
c506c029a082 adapted to localized typedef: handle single global interpretation only;
wenzelm
parents: 31723
diff changeset
   102
            end
c506c029a082 adapted to localized typedef: handle single global interpretation only;
wenzelm
parents: 31723
diff changeset
   103
      | _ => NONE)
28537
1e84256d1a8a established canonical argument order in SML code generators
haftmann
parents: 27398
diff changeset
   104
  | typedef_tycodegen thy defs dep module brack _ gr = NONE;
19459
2041d472fc17 seperated typedef codegen from main code
haftmann
parents:
diff changeset
   105
2041d472fc17 seperated typedef codegen from main code
haftmann
parents:
diff changeset
   106
val setup =
2041d472fc17 seperated typedef codegen from main code
haftmann
parents:
diff changeset
   107
  Codegen.add_codegen "typedef" typedef_codegen
2041d472fc17 seperated typedef codegen from main code
haftmann
parents:
diff changeset
   108
  #> Codegen.add_tycodegen "typedef" typedef_tycodegen
2041d472fc17 seperated typedef codegen from main code
haftmann
parents:
diff changeset
   109
2041d472fc17 seperated typedef codegen from main code
haftmann
parents:
diff changeset
   110
end;