src/HOL/Tools/typedef_codegen.ML
author wenzelm
Sun, 01 Mar 2009 23:36:12 +0100
changeset 30190 479806475f3c
parent 28537 1e84256d1a8a
child 31597 9a59cf39ee78
permissions -rw-r--r--
use long names for old-style fold combinators;
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
2041d472fc17 seperated typedef codegen from main code
haftmann
parents:
diff changeset
     2
    ID:         $Id$
2041d472fc17 seperated typedef codegen from main code
haftmann
parents:
diff changeset
     3
    Author:     Stefan Berghofer and Florian Haftmann, TU Muenchen
2041d472fc17 seperated typedef codegen from main code
haftmann
parents:
diff changeset
     4
2041d472fc17 seperated typedef codegen from main code
haftmann
parents:
diff changeset
     5
Code generators for trivial typedefs.
2041d472fc17 seperated typedef codegen from main code
haftmann
parents:
diff changeset
     6
*)
2041d472fc17 seperated typedef codegen from main code
haftmann
parents:
diff changeset
     7
2041d472fc17 seperated typedef codegen from main code
haftmann
parents:
diff changeset
     8
signature TYPEDEF_CODEGEN =
2041d472fc17 seperated typedef codegen from main code
haftmann
parents:
diff changeset
     9
sig
20428
67fa1c6ba89e refinements
haftmann
parents: 20354
diff changeset
    10
  val setup: theory -> theory
19459
2041d472fc17 seperated typedef codegen from main code
haftmann
parents:
diff changeset
    11
end;
2041d472fc17 seperated typedef codegen from main code
haftmann
parents:
diff changeset
    12
2041d472fc17 seperated typedef codegen from main code
haftmann
parents:
diff changeset
    13
structure TypedefCodegen: TYPEDEF_CODEGEN =
2041d472fc17 seperated typedef codegen from main code
haftmann
parents:
diff changeset
    14
struct
2041d472fc17 seperated typedef codegen from main code
haftmann
parents:
diff changeset
    15
28537
1e84256d1a8a established canonical argument order in SML code generators
haftmann
parents: 27398
diff changeset
    16
fun typedef_codegen thy defs dep module brack t gr =
19459
2041d472fc17 seperated typedef codegen from main code
haftmann
parents:
diff changeset
    17
  let
2041d472fc17 seperated typedef codegen from main code
haftmann
parents:
diff changeset
    18
    fun get_name (Type (tname, _)) = tname
2041d472fc17 seperated typedef codegen from main code
haftmann
parents:
diff changeset
    19
      | get_name _ = "";
2041d472fc17 seperated typedef codegen from main code
haftmann
parents:
diff changeset
    20
    fun mk_fun s T ts =
2041d472fc17 seperated typedef codegen from main code
haftmann
parents:
diff changeset
    21
      let
28537
1e84256d1a8a established canonical argument order in SML code generators
haftmann
parents: 27398
diff changeset
    22
        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
    23
        val (ps, gr'') =
1e84256d1a8a established canonical argument order in SML code generators
haftmann
parents: 27398
diff changeset
    24
          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
    25
        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
    26
      in SOME (Codegen.mk_app brack (Codegen.str id) ps, gr'') end;
19459
2041d472fc17 seperated typedef codegen from main code
haftmann
parents:
diff changeset
    27
    fun lookup f T =
19704
9b2612b807ab simplified TypedefPackage.get_info;
wenzelm
parents: 19459
diff changeset
    28
      (case TypedefPackage.get_info thy (get_name T) of
19459
2041d472fc17 seperated typedef codegen from main code
haftmann
parents:
diff changeset
    29
        NONE => ""
19704
9b2612b807ab simplified TypedefPackage.get_info;
wenzelm
parents: 19459
diff changeset
    30
      | SOME info => f info);
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) =>
19704
9b2612b807ab simplified TypedefPackage.get_info;
wenzelm
parents: 19459
diff changeset
    34
         if lookup #Rep_name 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
19704
9b2612b807ab simplified TypedefPackage.get_info;
wenzelm
parents: 19459
diff changeset
    37
         else if lookup #Abs_name 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 =
19704
9b2612b807ab simplified TypedefPackage.get_info;
wenzelm
parents: 19459
diff changeset
    49
      (case TypedefPackage.get_info thy s of
19459
2041d472fc17 seperated typedef codegen from main code
haftmann
parents:
diff changeset
    50
         NONE => NONE
19704
9b2612b807ab simplified TypedefPackage.get_info;
wenzelm
parents: 19459
diff changeset
    51
       | SOME {abs_type as newT as Type (tname, Us), rep_type = oldT, Abs_name, Rep_name, ...} =>
19459
2041d472fc17 seperated typedef codegen from main code
haftmann
parents:
diff changeset
    52
           if is_some (Codegen.get_assoc_type thy tname) then NONE else
2041d472fc17 seperated typedef codegen from main code
haftmann
parents:
diff changeset
    53
           let
2041d472fc17 seperated typedef codegen from main code
haftmann
parents:
diff changeset
    54
             val module' = Codegen.if_library
27398
768da1da59d6 simplified retrieval of theory names of consts and types
haftmann
parents: 26975
diff changeset
    55
               (Codegen.thyname_of_type thy tname) module;
19459
2041d472fc17 seperated typedef codegen from main code
haftmann
parents:
diff changeset
    56
             val node_id = tname ^ " (type)";
28537
1e84256d1a8a established canonical argument order in SML code generators
haftmann
parents: 27398
diff changeset
    57
             val ((((qs, (_, Abs_id)), (_, Rep_id)), ty_id), gr') = gr |> fold_map
19459
2041d472fc17 seperated typedef codegen from main code
haftmann
parents:
diff changeset
    58
                 (Codegen.invoke_tycodegen thy defs dep module (length Ts = 1))
28537
1e84256d1a8a established canonical argument order in SML code generators
haftmann
parents: 27398
diff changeset
    59
                   Ts ||>>
1e84256d1a8a established canonical argument order in SML code generators
haftmann
parents: 27398
diff changeset
    60
               Codegen.mk_const_id module' Abs_name ||>>
1e84256d1a8a established canonical argument order in SML code generators
haftmann
parents: 27398
diff changeset
    61
               Codegen.mk_const_id module' Rep_name ||>>
19459
2041d472fc17 seperated typedef codegen from main code
haftmann
parents:
diff changeset
    62
               Codegen.mk_type_id module' s;
2041d472fc17 seperated typedef codegen from main code
haftmann
parents:
diff changeset
    63
             val tyexpr = mk_tyexpr qs (Codegen.mk_qual_id module ty_id)
28537
1e84256d1a8a established canonical argument order in SML code generators
haftmann
parents: 27398
diff changeset
    64
           in SOME (tyexpr, case try (Codegen.get_node gr') node_id of
19459
2041d472fc17 seperated typedef codegen from main code
haftmann
parents:
diff changeset
    65
               NONE =>
2041d472fc17 seperated typedef codegen from main code
haftmann
parents:
diff changeset
    66
               let
28537
1e84256d1a8a established canonical argument order in SML code generators
haftmann
parents: 27398
diff changeset
    67
                 val (p :: ps, gr'') = fold_map
19459
2041d472fc17 seperated typedef codegen from main code
haftmann
parents:
diff changeset
    68
                   (Codegen.invoke_tycodegen thy defs node_id module' false)
28537
1e84256d1a8a established canonical argument order in SML code generators
haftmann
parents: 27398
diff changeset
    69
                   (oldT :: Us) (Codegen.add_edge (node_id, dep)
1e84256d1a8a established canonical argument order in SML code generators
haftmann
parents: 27398
diff changeset
    70
                      (Codegen.new_node (node_id, (NONE, "", "")) gr'));
19459
2041d472fc17 seperated typedef codegen from main code
haftmann
parents:
diff changeset
    71
                 val s =
26975
103dca19ef2e Replaced Pretty.str and Pretty.string_of by specific functions (from Codegen) that
berghofe
parents: 20597
diff changeset
    72
                   Codegen.string_of (Pretty.block [Codegen.str "datatype ",
19459
2041d472fc17 seperated typedef codegen from main code
haftmann
parents:
diff changeset
    73
                     mk_tyexpr ps (snd ty_id),
26975
103dca19ef2e Replaced Pretty.str and Pretty.string_of by specific functions (from Codegen) that
berghofe
parents: 20597
diff changeset
    74
                     Codegen.str " =", Pretty.brk 1, Codegen.str (Abs_id ^ " of"),
103dca19ef2e Replaced Pretty.str and Pretty.string_of by specific functions (from Codegen) that
berghofe
parents: 20597
diff changeset
    75
                     Pretty.brk 1, p, Codegen.str ";"]) ^ "\n\n" ^
103dca19ef2e Replaced Pretty.str and Pretty.string_of by specific functions (from Codegen) that
berghofe
parents: 20597
diff changeset
    76
                   Codegen.string_of (Pretty.block [Codegen.str ("fun " ^ Rep_id),
103dca19ef2e Replaced Pretty.str and Pretty.string_of by specific functions (from Codegen) that
berghofe
parents: 20597
diff changeset
    77
                     Pretty.brk 1, Codegen.str ("(" ^ Abs_id), Pretty.brk 1,
103dca19ef2e Replaced Pretty.str and Pretty.string_of by specific functions (from Codegen) that
berghofe
parents: 20597
diff changeset
    78
                     Codegen.str "x) = x;"]) ^ "\n\n" ^
19459
2041d472fc17 seperated typedef codegen from main code
haftmann
parents:
diff changeset
    79
                   (if "term_of" mem !Codegen.mode then
26975
103dca19ef2e Replaced Pretty.str and Pretty.string_of by specific functions (from Codegen) that
berghofe
parents: 20597
diff changeset
    80
                      Codegen.string_of (Pretty.block [Codegen.str "fun ",
19459
2041d472fc17 seperated typedef codegen from main code
haftmann
parents:
diff changeset
    81
                        Codegen.mk_term_of gr'' module' false newT, Pretty.brk 1,
26975
103dca19ef2e Replaced Pretty.str and Pretty.string_of by specific functions (from Codegen) that
berghofe
parents: 20597
diff changeset
    82
                        Codegen.str ("(" ^ Abs_id), Pretty.brk 1,
103dca19ef2e Replaced Pretty.str and Pretty.string_of by specific functions (from Codegen) that
berghofe
parents: 20597
diff changeset
    83
                        Codegen.str "x) =", Pretty.brk 1,
103dca19ef2e Replaced Pretty.str and Pretty.string_of by specific functions (from Codegen) that
berghofe
parents: 20597
diff changeset
    84
                        Pretty.block [Codegen.str ("Const (\"" ^ Abs_name ^ "\","),
19459
2041d472fc17 seperated typedef codegen from main code
haftmann
parents:
diff changeset
    85
                          Pretty.brk 1, Codegen.mk_type false (oldT --> newT),
26975
103dca19ef2e Replaced Pretty.str and Pretty.string_of by specific functions (from Codegen) that
berghofe
parents: 20597
diff changeset
    86
                          Codegen.str ")"], Codegen.str " $", Pretty.brk 1,
19459
2041d472fc17 seperated typedef codegen from main code
haftmann
parents:
diff changeset
    87
                        Codegen.mk_term_of gr'' module' false oldT, Pretty.brk 1,
26975
103dca19ef2e Replaced Pretty.str and Pretty.string_of by specific functions (from Codegen) that
berghofe
parents: 20597
diff changeset
    88
                        Codegen.str "x;"]) ^ "\n\n"
19459
2041d472fc17 seperated typedef codegen from main code
haftmann
parents:
diff changeset
    89
                    else "") ^
2041d472fc17 seperated typedef codegen from main code
haftmann
parents:
diff changeset
    90
                   (if "test" mem !Codegen.mode then
26975
103dca19ef2e Replaced Pretty.str and Pretty.string_of by specific functions (from Codegen) that
berghofe
parents: 20597
diff changeset
    91
                      Codegen.string_of (Pretty.block [Codegen.str "fun ",
19459
2041d472fc17 seperated typedef codegen from main code
haftmann
parents:
diff changeset
    92
                        Codegen.mk_gen gr'' module' false [] "" newT, Pretty.brk 1,
26975
103dca19ef2e Replaced Pretty.str and Pretty.string_of by specific functions (from Codegen) that
berghofe
parents: 20597
diff changeset
    93
                        Codegen.str "i =", Pretty.brk 1,
103dca19ef2e Replaced Pretty.str and Pretty.string_of by specific functions (from Codegen) that
berghofe
parents: 20597
diff changeset
    94
                        Pretty.block [Codegen.str (Abs_id ^ " ("),
19459
2041d472fc17 seperated typedef codegen from main code
haftmann
parents:
diff changeset
    95
                          Codegen.mk_gen gr'' module' false [] "" oldT, Pretty.brk 1,
26975
103dca19ef2e Replaced Pretty.str and Pretty.string_of by specific functions (from Codegen) that
berghofe
parents: 20597
diff changeset
    96
                          Codegen.str "i);"]]) ^ "\n\n"
19459
2041d472fc17 seperated typedef codegen from main code
haftmann
parents:
diff changeset
    97
                    else "")
2041d472fc17 seperated typedef codegen from main code
haftmann
parents:
diff changeset
    98
               in Codegen.map_node node_id (K (NONE, module', s)) gr'' end
28537
1e84256d1a8a established canonical argument order in SML code generators
haftmann
parents: 27398
diff changeset
    99
             | SOME _ => Codegen.add_edge (node_id, dep) gr')
19459
2041d472fc17 seperated typedef codegen from main code
haftmann
parents:
diff changeset
   100
           end)
28537
1e84256d1a8a established canonical argument order in SML code generators
haftmann
parents: 27398
diff changeset
   101
  | typedef_tycodegen thy defs dep module brack _ gr = NONE;
19459
2041d472fc17 seperated typedef codegen from main code
haftmann
parents:
diff changeset
   102
2041d472fc17 seperated typedef codegen from main code
haftmann
parents:
diff changeset
   103
val setup =
2041d472fc17 seperated typedef codegen from main code
haftmann
parents:
diff changeset
   104
  Codegen.add_codegen "typedef" typedef_codegen
2041d472fc17 seperated typedef codegen from main code
haftmann
parents:
diff changeset
   105
  #> Codegen.add_tycodegen "typedef" typedef_tycodegen
2041d472fc17 seperated typedef codegen from main code
haftmann
parents:
diff changeset
   106
2041d472fc17 seperated typedef codegen from main code
haftmann
parents:
diff changeset
   107
end;