src/Pure/Tools/codegen_package.ML
author haftmann
Mon, 14 Aug 2006 13:46:21 +0200
changeset 20386 d1cbe5aa6bf2
parent 20353 d73e49780ef2
child 20389 8b6ecb22ef35
permissions -rw-r--r--
module restructuring
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
18169
45def66f86cb added modules for code generator generation two, not operational yet
haftmann
parents:
diff changeset
     1
(*  Title:      Pure/Tools/codegen_package.ML
45def66f86cb added modules for code generator generation two, not operational yet
haftmann
parents:
diff changeset
     2
    ID:         $Id$
45def66f86cb added modules for code generator generation two, not operational yet
haftmann
parents:
diff changeset
     3
    Author:     Florian Haftmann, TU Muenchen
45def66f86cb added modules for code generator generation two, not operational yet
haftmann
parents:
diff changeset
     4
18217
e0b08c9534ff added codegen package
haftmann
parents: 18169
diff changeset
     5
Code generator from Isabelle theories to
18169
45def66f86cb added modules for code generator generation two, not operational yet
haftmann
parents:
diff changeset
     6
intermediate language ("Thin-gol").
45def66f86cb added modules for code generator generation two, not operational yet
haftmann
parents:
diff changeset
     7
*)
45def66f86cb added modules for code generator generation two, not operational yet
haftmann
parents:
diff changeset
     8
45def66f86cb added modules for code generator generation two, not operational yet
haftmann
parents:
diff changeset
     9
signature CODEGEN_PACKAGE =
45def66f86cb added modules for code generator generation two, not operational yet
haftmann
parents:
diff changeset
    10
sig
20105
454f4be984b7 adaptions in codegen
haftmann
parents: 20076
diff changeset
    11
  val codegen_term: term -> theory -> CodegenThingol.iterm * theory;
20213
2b319e945905 added eval_term
haftmann
parents: 20194
diff changeset
    12
  val eval_term: (string (*reference name!*) * 'a ref) * term -> theory -> 'a * theory;
19884
a7be206d8655 improvements in code generator
haftmann
parents: 19816
diff changeset
    13
  val is_dtcon: string -> bool;
a7be206d8655 improvements in code generator
haftmann
parents: 19816
diff changeset
    14
  val consts_of_idfs: theory -> string list -> (string * typ) list;
a7be206d8655 improvements in code generator
haftmann
parents: 19816
diff changeset
    15
  val idfs_of_consts: theory -> (string * typ) list -> string list;
19967
33da452f0abe slight refinements
haftmann
parents: 19956
diff changeset
    16
  val get_root_module: theory -> CodegenThingol.module * theory;
19884
a7be206d8655 improvements in code generator
haftmann
parents: 19816
diff changeset
    17
  val get_ml_fun_datatype: theory -> (string -> string)
a7be206d8655 improvements in code generator
haftmann
parents: 19816
diff changeset
    18
    -> ((string * CodegenThingol.funn) list -> Pretty.T)
a7be206d8655 improvements in code generator
haftmann
parents: 19816
diff changeset
    19
        * ((string * CodegenThingol.datatyp) list -> Pretty.T);
18702
7dc7dcd63224 substantial improvements in code generator
haftmann
parents: 18517
diff changeset
    20
18704
2c86ced392a8 substantial improvement in serialization handling
haftmann
parents: 18702
diff changeset
    21
  val add_pretty_list: string -> string -> string * (int * string)
2c86ced392a8 substantial improvement in serialization handling
haftmann
parents: 18702
diff changeset
    22
    -> theory -> theory;
20175
0a8ca32f6e64 class package and codegen refinements
haftmann
parents: 20105
diff changeset
    23
  val purge_code: theory -> theory;
18217
e0b08c9534ff added codegen package
haftmann
parents: 18169
diff changeset
    24
19884
a7be206d8655 improvements in code generator
haftmann
parents: 19816
diff changeset
    25
  type appgen;
20105
454f4be984b7 adaptions in codegen
haftmann
parents: 20076
diff changeset
    26
  val add_appconst: xstring * appgen -> theory -> theory;
454f4be984b7 adaptions in codegen
haftmann
parents: 20076
diff changeset
    27
  val add_appconst_i: string * appgen -> theory -> theory;
18702
7dc7dcd63224 substantial improvements in code generator
haftmann
parents: 18517
diff changeset
    28
  val appgen_default: appgen;
20353
d73e49780ef2 code generator refinements
haftmann
parents: 20216
diff changeset
    29
  val appgen_rep_bin: (theory -> term -> IntInf.int) -> appgen;
19607
07eeb832f28d introduced characters for code generator; some improved code lemmas for some list functions
haftmann
parents: 19597
diff changeset
    30
  val appgen_char: (term -> int option) -> appgen;
20105
454f4be984b7 adaptions in codegen
haftmann
parents: 20076
diff changeset
    31
  val appgen_case: (theory -> term
454f4be984b7 adaptions in codegen
haftmann
parents: 20076
diff changeset
    32
    -> ((string * typ) list * ((term * typ) * (term * term) list)) option)
454f4be984b7 adaptions in codegen
haftmann
parents: 20076
diff changeset
    33
    -> appgen;
454f4be984b7 adaptions in codegen
haftmann
parents: 20076
diff changeset
    34
  val appgen_let: appgen;
19038
62c5f7591a43 improved handling of iml abstractions
haftmann
parents: 19025
diff changeset
    35
  val appgen_wfrec: appgen;
18217
e0b08c9534ff added codegen package
haftmann
parents: 18169
diff changeset
    36
19008
14c1b2f5dda4 improved code generator devarification
haftmann
parents: 18963
diff changeset
    37
  val print_code: theory -> unit;
18515
1cad5c2b2a0b substantial improvements in code generating
haftmann
parents: 18455
diff changeset
    38
18231
2eea98bbf650 improved failure tracking
haftmann
parents: 18217
diff changeset
    39
  structure CodegenData: THEORY_DATA;
19884
a7be206d8655 improvements in code generator
haftmann
parents: 19816
diff changeset
    40
  type auxtab;
20353
d73e49780ef2 code generator refinements
haftmann
parents: 20216
diff changeset
    41
  val mk_tabs: theory -> string list option -> (string * typ) list -> auxtab;
18169
45def66f86cb added modules for code generator generation two, not operational yet
haftmann
parents:
diff changeset
    42
end;
45def66f86cb added modules for code generator generation two, not operational yet
haftmann
parents:
diff changeset
    43
18217
e0b08c9534ff added codegen package
haftmann
parents: 18169
diff changeset
    44
structure CodegenPackage : CODEGEN_PACKAGE =
18169
45def66f86cb added modules for code generator generation two, not operational yet
haftmann
parents:
diff changeset
    45
struct
45def66f86cb added modules for code generator generation two, not operational yet
haftmann
parents:
diff changeset
    46
18850
92ef83e5eaea various improvements
haftmann
parents: 18756
diff changeset
    47
open CodegenThingol;
18217
e0b08c9534ff added codegen package
haftmann
parents: 18169
diff changeset
    48
18702
7dc7dcd63224 substantial improvements in code generator
haftmann
parents: 18517
diff changeset
    49
(* shallow name spaces *)
18217
e0b08c9534ff added codegen package
haftmann
parents: 18169
diff changeset
    50
20216
f30b73385060 added eval_term
haftmann
parents: 20213
diff changeset
    51
val nsp_module = ""; (*a dummy by convention*)
18217
e0b08c9534ff added codegen package
haftmann
parents: 18169
diff changeset
    52
val nsp_class = "class";
18454
6720b5010a57 slight improvements in name handling
haftmann
parents: 18385
diff changeset
    53
val nsp_tyco = "tyco";
18217
e0b08c9534ff added codegen package
haftmann
parents: 18169
diff changeset
    54
val nsp_const = "const";
18454
6720b5010a57 slight improvements in name handling
haftmann
parents: 18385
diff changeset
    55
val nsp_dtcon = "dtcon";
18217
e0b08c9534ff added codegen package
haftmann
parents: 18169
diff changeset
    56
val nsp_mem = "mem";
e0b08c9534ff added codegen package
haftmann
parents: 18169
diff changeset
    57
val nsp_inst = "inst";
19213
ee83040c3c84 first running version of type classes
haftmann
parents: 19202
diff changeset
    58
val nsp_instmem = "instmem";
20216
f30b73385060 added eval_term
haftmann
parents: 20213
diff changeset
    59
val nsp_eval = "EVAL"; (*only for evaluation*)
18217
e0b08c9534ff added codegen package
haftmann
parents: 18169
diff changeset
    60
19038
62c5f7591a43 improved handling of iml abstractions
haftmann
parents: 19025
diff changeset
    61
fun add_nsp shallow name =
62c5f7591a43 improved handling of iml abstractions
haftmann
parents: 19025
diff changeset
    62
  name
62c5f7591a43 improved handling of iml abstractions
haftmann
parents: 19025
diff changeset
    63
  |> NameSpace.unpack
62c5f7591a43 improved handling of iml abstractions
haftmann
parents: 19025
diff changeset
    64
  |> split_last
62c5f7591a43 improved handling of iml abstractions
haftmann
parents: 19025
diff changeset
    65
  |> apsnd (single #> cons shallow)
62c5f7591a43 improved handling of iml abstractions
haftmann
parents: 19025
diff changeset
    66
  |> (op @)
62c5f7591a43 improved handling of iml abstractions
haftmann
parents: 19025
diff changeset
    67
  |> NameSpace.pack;
62c5f7591a43 improved handling of iml abstractions
haftmann
parents: 19025
diff changeset
    68
62c5f7591a43 improved handling of iml abstractions
haftmann
parents: 19025
diff changeset
    69
fun dest_nsp nsp idf =
62c5f7591a43 improved handling of iml abstractions
haftmann
parents: 19025
diff changeset
    70
  let
62c5f7591a43 improved handling of iml abstractions
haftmann
parents: 19025
diff changeset
    71
    val idf' = NameSpace.unpack idf;
62c5f7591a43 improved handling of iml abstractions
haftmann
parents: 19025
diff changeset
    72
    val (idf'', idf_base) = split_last idf';
62c5f7591a43 improved handling of iml abstractions
haftmann
parents: 19025
diff changeset
    73
    val (modl, shallow) = split_last idf'';
62c5f7591a43 improved handling of iml abstractions
haftmann
parents: 19025
diff changeset
    74
  in
62c5f7591a43 improved handling of iml abstractions
haftmann
parents: 19025
diff changeset
    75
    if nsp = shallow
62c5f7591a43 improved handling of iml abstractions
haftmann
parents: 19025
diff changeset
    76
   then (SOME o NameSpace.pack) (modl @ [idf_base])
62c5f7591a43 improved handling of iml abstractions
haftmann
parents: 19025
diff changeset
    77
    else NONE
62c5f7591a43 improved handling of iml abstractions
haftmann
parents: 19025
diff changeset
    78
  end;
62c5f7591a43 improved handling of iml abstractions
haftmann
parents: 19025
diff changeset
    79
20386
d1cbe5aa6bf2 module restructuring
haftmann
parents: 20353
diff changeset
    80
fun if_nsp nsp f idf =
d1cbe5aa6bf2 module restructuring
haftmann
parents: 20353
diff changeset
    81
  Option.map f (dest_nsp nsp idf);
19956
f992e507020e slight improvements in code generation
haftmann
parents: 19953
diff changeset
    82
f992e507020e slight improvements in code generation
haftmann
parents: 19953
diff changeset
    83
18702
7dc7dcd63224 substantial improvements in code generator
haftmann
parents: 18517
diff changeset
    84
(* code generator basics *)
18454
6720b5010a57 slight improvements in name handling
haftmann
parents: 18385
diff changeset
    85
20386
d1cbe5aa6bf2 module restructuring
haftmann
parents: 20353
diff changeset
    86
type auxtab = (bool * string list option) * CodegenTheorems.thmtab;
18865
31aed965135c minor cleanups
haftmann
parents: 18850
diff changeset
    87
type appgen = theory -> auxtab
20105
454f4be984b7 adaptions in codegen
haftmann
parents: 20076
diff changeset
    88
  -> (string * typ) * term list -> transact -> iterm * transact;
18217
e0b08c9534ff added codegen package
haftmann
parents: 18169
diff changeset
    89
18702
7dc7dcd63224 substantial improvements in code generator
haftmann
parents: 18517
diff changeset
    90
val serializers = ref (
7dc7dcd63224 substantial improvements in code generator
haftmann
parents: 18517
diff changeset
    91
  Symtab.empty
7dc7dcd63224 substantial improvements in code generator
haftmann
parents: 18517
diff changeset
    92
  |> Symtab.update (
7dc7dcd63224 substantial improvements in code generator
haftmann
parents: 18517
diff changeset
    93
       #ml CodegenSerializer.serializers
7dc7dcd63224 substantial improvements in code generator
haftmann
parents: 18517
diff changeset
    94
       |> apsnd (fn seri => seri
20183
fd546b0c8a7c major simplifications for integers
haftmann
parents: 20175
diff changeset
    95
            nsp_dtcon
20386
d1cbe5aa6bf2 module restructuring
haftmann
parents: 20353
diff changeset
    96
            [[nsp_module], [nsp_class, nsp_tyco], [nsp_const, nsp_dtcon, nsp_class, nsp_mem, nsp_inst, nsp_instmem]]
18702
7dc7dcd63224 substantial improvements in code generator
haftmann
parents: 18517
diff changeset
    97
          )
7dc7dcd63224 substantial improvements in code generator
haftmann
parents: 18517
diff changeset
    98
     )
7dc7dcd63224 substantial improvements in code generator
haftmann
parents: 18517
diff changeset
    99
  |> Symtab.update (
7dc7dcd63224 substantial improvements in code generator
haftmann
parents: 18517
diff changeset
   100
       #haskell CodegenSerializer.serializers
7dc7dcd63224 substantial improvements in code generator
haftmann
parents: 18517
diff changeset
   101
       |> apsnd (fn seri => seri
19953
2f54a51f1801 class package refinements, slight code generation refinements
haftmann
parents: 19884
diff changeset
   102
            (nsp_dtcon, [nsp_module, nsp_class, nsp_tyco, nsp_dtcon])
20386
d1cbe5aa6bf2 module restructuring
haftmann
parents: 20353
diff changeset
   103
            [[nsp_module], [nsp_class], [nsp_tyco], [nsp_const,  nsp_mem], [nsp_dtcon], [nsp_inst], [nsp_instmem]]
18702
7dc7dcd63224 substantial improvements in code generator
haftmann
parents: 18517
diff changeset
   104
          )
7dc7dcd63224 substantial improvements in code generator
haftmann
parents: 18517
diff changeset
   105
     )
7dc7dcd63224 substantial improvements in code generator
haftmann
parents: 18517
diff changeset
   106
);
18217
e0b08c9534ff added codegen package
haftmann
parents: 18169
diff changeset
   107
e0b08c9534ff added codegen package
haftmann
parents: 18169
diff changeset
   108
18454
6720b5010a57 slight improvements in name handling
haftmann
parents: 18385
diff changeset
   109
(* theory data for code generator *)
18217
e0b08c9534ff added codegen package
haftmann
parents: 18169
diff changeset
   110
18912
dd168daf172d improvement in devarifications
haftmann
parents: 18885
diff changeset
   111
fun merge_opt _ (x1, NONE) = x1
dd168daf172d improvement in devarifications
haftmann
parents: 18885
diff changeset
   112
  | merge_opt _ (NONE, x2) = x2
dd168daf172d improvement in devarifications
haftmann
parents: 18885
diff changeset
   113
  | merge_opt eq (SOME x1, SOME x2) =
dd168daf172d improvement in devarifications
haftmann
parents: 18885
diff changeset
   114
      if eq (x1, x2) then SOME x1 else error ("incompatible options during merge");
dd168daf172d improvement in devarifications
haftmann
parents: 18885
diff changeset
   115
20105
454f4be984b7 adaptions in codegen
haftmann
parents: 20076
diff changeset
   116
type appgens = (int * (appgen * stamp)) Symtab.table
18217
e0b08c9534ff added codegen package
haftmann
parents: 18169
diff changeset
   117
20386
d1cbe5aa6bf2 module restructuring
haftmann
parents: 20353
diff changeset
   118
fun merge_appgens (x : appgens * appgens) =
20105
454f4be984b7 adaptions in codegen
haftmann
parents: 20076
diff changeset
   119
  Symtab.merge (fn ((bounds1, (_, stamp1)), (bounds2, (_, stamp2))) =>
454f4be984b7 adaptions in codegen
haftmann
parents: 20076
diff changeset
   120
    bounds1 = bounds2 andalso stamp1 = stamp2) x
18217
e0b08c9534ff added codegen package
haftmann
parents: 18169
diff changeset
   121
18702
7dc7dcd63224 substantial improvements in code generator
haftmann
parents: 18517
diff changeset
   122
type target_data = {
18865
31aed965135c minor cleanups
haftmann
parents: 18850
diff changeset
   123
  syntax_class: string Symtab.table,
18516
4424e2bce9af slightly improved serialization
haftmann
parents: 18515
diff changeset
   124
  syntax_tyco: (itype CodegenSerializer.pretty_syntax * stamp) Symtab.table,
20105
454f4be984b7 adaptions in codegen
haftmann
parents: 20076
diff changeset
   125
  syntax_const: (iterm CodegenSerializer.pretty_syntax * stamp) Symtab.table
18217
e0b08c9534ff added codegen package
haftmann
parents: 18169
diff changeset
   126
};
e0b08c9534ff added codegen package
haftmann
parents: 18169
diff changeset
   127
18865
31aed965135c minor cleanups
haftmann
parents: 18850
diff changeset
   128
fun map_target_data f { syntax_class, syntax_tyco, syntax_const } =
18217
e0b08c9534ff added codegen package
haftmann
parents: 18169
diff changeset
   129
  let
18865
31aed965135c minor cleanups
haftmann
parents: 18850
diff changeset
   130
    val (syntax_class, syntax_tyco, syntax_const) =
31aed965135c minor cleanups
haftmann
parents: 18850
diff changeset
   131
      f (syntax_class, syntax_tyco, syntax_const)
31aed965135c minor cleanups
haftmann
parents: 18850
diff changeset
   132
  in {
31aed965135c minor cleanups
haftmann
parents: 18850
diff changeset
   133
    syntax_class = syntax_class,
31aed965135c minor cleanups
haftmann
parents: 18850
diff changeset
   134
    syntax_tyco = syntax_tyco,
31aed965135c minor cleanups
haftmann
parents: 18850
diff changeset
   135
    syntax_const = syntax_const } : target_data
18454
6720b5010a57 slight improvements in name handling
haftmann
parents: 18385
diff changeset
   136
  end;
18217
e0b08c9534ff added codegen package
haftmann
parents: 18169
diff changeset
   137
18702
7dc7dcd63224 substantial improvements in code generator
haftmann
parents: 18517
diff changeset
   138
fun merge_target_data
18865
31aed965135c minor cleanups
haftmann
parents: 18850
diff changeset
   139
  ({ syntax_class = syntax_class1, syntax_tyco = syntax_tyco1, syntax_const = syntax_const1 },
31aed965135c minor cleanups
haftmann
parents: 18850
diff changeset
   140
   { syntax_class = syntax_class2, syntax_tyco = syntax_tyco2, syntax_const = syntax_const2 }) =
31aed965135c minor cleanups
haftmann
parents: 18850
diff changeset
   141
  { syntax_class = Symtab.merge (op =) (syntax_class1, syntax_class2),
31aed965135c minor cleanups
haftmann
parents: 18850
diff changeset
   142
    syntax_tyco = Symtab.merge (eq_snd (op =)) (syntax_tyco1, syntax_tyco2),
18702
7dc7dcd63224 substantial improvements in code generator
haftmann
parents: 18517
diff changeset
   143
    syntax_const = Symtab.merge (eq_snd (op =)) (syntax_const1, syntax_const2) } : target_data;
18217
e0b08c9534ff added codegen package
haftmann
parents: 18169
diff changeset
   144
e0b08c9534ff added codegen package
haftmann
parents: 18169
diff changeset
   145
structure CodegenData = TheoryDataFun
e0b08c9534ff added codegen package
haftmann
parents: 18169
diff changeset
   146
(struct
19953
2f54a51f1801 class package refinements, slight code generation refinements
haftmann
parents: 19884
diff changeset
   147
  val name = "Pure/codegen_package";
18217
e0b08c9534ff added codegen package
haftmann
parents: 18169
diff changeset
   148
  type T = {
e0b08c9534ff added codegen package
haftmann
parents: 18169
diff changeset
   149
    modl: module,
20105
454f4be984b7 adaptions in codegen
haftmann
parents: 20076
diff changeset
   150
    appgens: appgens,
18702
7dc7dcd63224 substantial improvements in code generator
haftmann
parents: 18517
diff changeset
   151
    target_data: target_data Symtab.table
18217
e0b08c9534ff added codegen package
haftmann
parents: 18169
diff changeset
   152
  };
e0b08c9534ff added codegen package
haftmann
parents: 18169
diff changeset
   153
  val empty = {
e0b08c9534ff added codegen package
haftmann
parents: 18169
diff changeset
   154
    modl = empty_module,
20105
454f4be984b7 adaptions in codegen
haftmann
parents: 20076
diff changeset
   155
    appgens = Symtab.empty,
18702
7dc7dcd63224 substantial improvements in code generator
haftmann
parents: 18517
diff changeset
   156
    target_data =
18217
e0b08c9534ff added codegen package
haftmann
parents: 18169
diff changeset
   157
      Symtab.empty
18702
7dc7dcd63224 substantial improvements in code generator
haftmann
parents: 18517
diff changeset
   158
      |> Symtab.fold (fn (target, _) =>
18865
31aed965135c minor cleanups
haftmann
parents: 18850
diff changeset
   159
           Symtab.update (target,
31aed965135c minor cleanups
haftmann
parents: 18850
diff changeset
   160
             { syntax_class = Symtab.empty, syntax_tyco = Symtab.empty, syntax_const = Symtab.empty })
18702
7dc7dcd63224 substantial improvements in code generator
haftmann
parents: 18517
diff changeset
   161
         ) (! serializers)
18217
e0b08c9534ff added codegen package
haftmann
parents: 18169
diff changeset
   162
  } : T;
e0b08c9534ff added codegen package
haftmann
parents: 18169
diff changeset
   163
  val copy = I;
e0b08c9534ff added codegen package
haftmann
parents: 18169
diff changeset
   164
  val extend = I;
e0b08c9534ff added codegen package
haftmann
parents: 18169
diff changeset
   165
  fun merge _ (
20105
454f4be984b7 adaptions in codegen
haftmann
parents: 20076
diff changeset
   166
    { modl = modl1, appgens = appgens1,
20386
d1cbe5aa6bf2 module restructuring
haftmann
parents: 20353
diff changeset
   167
      target_data = target_data1 },
20105
454f4be984b7 adaptions in codegen
haftmann
parents: 20076
diff changeset
   168
    { modl = modl2, appgens = appgens2,
20386
d1cbe5aa6bf2 module restructuring
haftmann
parents: 20353
diff changeset
   169
      target_data = target_data2 }
18217
e0b08c9534ff added codegen package
haftmann
parents: 18169
diff changeset
   170
  ) = {
e0b08c9534ff added codegen package
haftmann
parents: 18169
diff changeset
   171
    modl = merge_module (modl1, modl2),
20105
454f4be984b7 adaptions in codegen
haftmann
parents: 20076
diff changeset
   172
    appgens = merge_appgens (appgens1, appgens2),
19025
596fb1eb7856 simplified TableFun.join;
wenzelm
parents: 19008
diff changeset
   173
    target_data = Symtab.join (K merge_target_data) (target_data1, target_data2)
18217
e0b08c9534ff added codegen package
haftmann
parents: 18169
diff changeset
   174
  };
19341
3414c04fbc39 added definitional code generator module: codegen_theorems.ML
haftmann
parents: 19283
diff changeset
   175
  fun print thy (data : T) =
3414c04fbc39 added definitional code generator module: codegen_theorems.ML
haftmann
parents: 19283
diff changeset
   176
    let
3414c04fbc39 added definitional code generator module: codegen_theorems.ML
haftmann
parents: 19283
diff changeset
   177
      val module = #modl data
3414c04fbc39 added definitional code generator module: codegen_theorems.ML
haftmann
parents: 19283
diff changeset
   178
    in
3414c04fbc39 added definitional code generator module: codegen_theorems.ML
haftmann
parents: 19283
diff changeset
   179
      (Pretty.writeln o Pretty.chunks) [pretty_module module, pretty_deps module]
3414c04fbc39 added definitional code generator module: codegen_theorems.ML
haftmann
parents: 19283
diff changeset
   180
    end;
18217
e0b08c9534ff added codegen package
haftmann
parents: 18169
diff changeset
   181
end);
e0b08c9534ff added codegen package
haftmann
parents: 18169
diff changeset
   182
18708
4b3dadb4fe33 setup: theory -> theory;
wenzelm
parents: 18704
diff changeset
   183
val _ = Context.add_setup CodegenData.init;
4b3dadb4fe33 setup: theory -> theory;
wenzelm
parents: 18704
diff changeset
   184
18217
e0b08c9534ff added codegen package
haftmann
parents: 18169
diff changeset
   185
fun map_codegen_data f thy =
e0b08c9534ff added codegen package
haftmann
parents: 18169
diff changeset
   186
  case CodegenData.get thy
20386
d1cbe5aa6bf2 module restructuring
haftmann
parents: 20353
diff changeset
   187
   of { modl, appgens, target_data } =>
d1cbe5aa6bf2 module restructuring
haftmann
parents: 20353
diff changeset
   188
      let val (modl, appgens, target_data) =
d1cbe5aa6bf2 module restructuring
haftmann
parents: 20353
diff changeset
   189
        f (modl, appgens, target_data)
20105
454f4be984b7 adaptions in codegen
haftmann
parents: 20076
diff changeset
   190
      in CodegenData.put { modl = modl, appgens = appgens,
20386
d1cbe5aa6bf2 module restructuring
haftmann
parents: 20353
diff changeset
   191
           target_data = target_data } thy end;
18217
e0b08c9534ff added codegen package
haftmann
parents: 18169
diff changeset
   192
19341
3414c04fbc39 added definitional code generator module: codegen_theorems.ML
haftmann
parents: 19283
diff changeset
   193
val print_code = CodegenData.print;
18217
e0b08c9534ff added codegen package
haftmann
parents: 18169
diff changeset
   194
20386
d1cbe5aa6bf2 module restructuring
haftmann
parents: 20353
diff changeset
   195
val purge_code = map_codegen_data (fn (_, appgens, target_data) =>
d1cbe5aa6bf2 module restructuring
haftmann
parents: 20353
diff changeset
   196
  (empty_module, appgens, target_data));
18454
6720b5010a57 slight improvements in name handling
haftmann
parents: 18385
diff changeset
   197
18865
31aed965135c minor cleanups
haftmann
parents: 18850
diff changeset
   198
20386
d1cbe5aa6bf2 module restructuring
haftmann
parents: 20353
diff changeset
   199
(* name handling *)
d1cbe5aa6bf2 module restructuring
haftmann
parents: 20353
diff changeset
   200
d1cbe5aa6bf2 module restructuring
haftmann
parents: 20353
diff changeset
   201
fun idf_of_class thy class =
d1cbe5aa6bf2 module restructuring
haftmann
parents: 20353
diff changeset
   202
  CodegenNames.class thy class
d1cbe5aa6bf2 module restructuring
haftmann
parents: 20353
diff changeset
   203
  |> add_nsp nsp_class;
d1cbe5aa6bf2 module restructuring
haftmann
parents: 20353
diff changeset
   204
d1cbe5aa6bf2 module restructuring
haftmann
parents: 20353
diff changeset
   205
fun class_of_idf thy = if_nsp nsp_class (CodegenNames.class_rev thy);
d1cbe5aa6bf2 module restructuring
haftmann
parents: 20353
diff changeset
   206
d1cbe5aa6bf2 module restructuring
haftmann
parents: 20353
diff changeset
   207
fun idf_of_tyco thy tyco =
d1cbe5aa6bf2 module restructuring
haftmann
parents: 20353
diff changeset
   208
  CodegenNames.tyco thy tyco
d1cbe5aa6bf2 module restructuring
haftmann
parents: 20353
diff changeset
   209
  |> add_nsp nsp_tyco;
d1cbe5aa6bf2 module restructuring
haftmann
parents: 20353
diff changeset
   210
d1cbe5aa6bf2 module restructuring
haftmann
parents: 20353
diff changeset
   211
fun tyco_of_idf thy = if_nsp nsp_tyco (CodegenNames.tyco_rev thy);
d1cbe5aa6bf2 module restructuring
haftmann
parents: 20353
diff changeset
   212
d1cbe5aa6bf2 module restructuring
haftmann
parents: 20353
diff changeset
   213
fun idf_of_inst thy inst =
d1cbe5aa6bf2 module restructuring
haftmann
parents: 20353
diff changeset
   214
  CodegenNames.instance thy inst
d1cbe5aa6bf2 module restructuring
haftmann
parents: 20353
diff changeset
   215
  |> add_nsp nsp_inst;
d1cbe5aa6bf2 module restructuring
haftmann
parents: 20353
diff changeset
   216
d1cbe5aa6bf2 module restructuring
haftmann
parents: 20353
diff changeset
   217
fun inst_of_idf thy = if_nsp nsp_inst (CodegenNames.instance_rev thy);
d1cbe5aa6bf2 module restructuring
haftmann
parents: 20353
diff changeset
   218
d1cbe5aa6bf2 module restructuring
haftmann
parents: 20353
diff changeset
   219
fun idf_of_const thy thmtab (c_ty as (c, ty)) =
d1cbe5aa6bf2 module restructuring
haftmann
parents: 20353
diff changeset
   220
  if is_some (CodegenTheorems.get_dtyp_of_cons thmtab c_ty) then
d1cbe5aa6bf2 module restructuring
haftmann
parents: 20353
diff changeset
   221
    CodegenNames.const thy c_ty
d1cbe5aa6bf2 module restructuring
haftmann
parents: 20353
diff changeset
   222
    |> add_nsp nsp_dtcon
d1cbe5aa6bf2 module restructuring
haftmann
parents: 20353
diff changeset
   223
  else if (is_some o CodegenConsts.class_of_classop thy o CodegenConsts.typinst_of_typ thy) c_ty then
d1cbe5aa6bf2 module restructuring
haftmann
parents: 20353
diff changeset
   224
    CodegenNames.const thy c_ty
d1cbe5aa6bf2 module restructuring
haftmann
parents: 20353
diff changeset
   225
    |> add_nsp nsp_mem
d1cbe5aa6bf2 module restructuring
haftmann
parents: 20353
diff changeset
   226
  else
d1cbe5aa6bf2 module restructuring
haftmann
parents: 20353
diff changeset
   227
    CodegenNames.const thy c_ty
d1cbe5aa6bf2 module restructuring
haftmann
parents: 20353
diff changeset
   228
    |> add_nsp nsp_const;
d1cbe5aa6bf2 module restructuring
haftmann
parents: 20353
diff changeset
   229
d1cbe5aa6bf2 module restructuring
haftmann
parents: 20353
diff changeset
   230
fun const_of_idf thy idf =
d1cbe5aa6bf2 module restructuring
haftmann
parents: 20353
diff changeset
   231
  case dest_nsp nsp_const idf
d1cbe5aa6bf2 module restructuring
haftmann
parents: 20353
diff changeset
   232
   of SOME c => CodegenNames.const_rev thy c |> SOME
d1cbe5aa6bf2 module restructuring
haftmann
parents: 20353
diff changeset
   233
    | _ => (case dest_nsp nsp_dtcon idf
d1cbe5aa6bf2 module restructuring
haftmann
parents: 20353
diff changeset
   234
   of SOME c => CodegenNames.const_rev thy c |> SOME
d1cbe5aa6bf2 module restructuring
haftmann
parents: 20353
diff changeset
   235
    | _ => (case dest_nsp nsp_mem idf
d1cbe5aa6bf2 module restructuring
haftmann
parents: 20353
diff changeset
   236
   of SOME c => CodegenNames.const_rev thy c |> SOME
d1cbe5aa6bf2 module restructuring
haftmann
parents: 20353
diff changeset
   237
    | _ => NONE));
d1cbe5aa6bf2 module restructuring
haftmann
parents: 20353
diff changeset
   238
d1cbe5aa6bf2 module restructuring
haftmann
parents: 20353
diff changeset
   239
d1cbe5aa6bf2 module restructuring
haftmann
parents: 20353
diff changeset
   240
(* application generators *)
18865
31aed965135c minor cleanups
haftmann
parents: 18850
diff changeset
   241
20105
454f4be984b7 adaptions in codegen
haftmann
parents: 20076
diff changeset
   242
fun gen_add_appconst prep_const (raw_c, appgen) thy =
18454
6720b5010a57 slight improvements in name handling
haftmann
parents: 18385
diff changeset
   243
  let
18865
31aed965135c minor cleanups
haftmann
parents: 18850
diff changeset
   244
    val c = prep_const thy raw_c;
20105
454f4be984b7 adaptions in codegen
haftmann
parents: 20076
diff changeset
   245
    val i = (length o fst o strip_type o Sign.the_const_type thy) c
18865
31aed965135c minor cleanups
haftmann
parents: 18850
diff changeset
   246
  in map_codegen_data
20386
d1cbe5aa6bf2 module restructuring
haftmann
parents: 20353
diff changeset
   247
    (fn (modl, appgens, target_data) =>
18865
31aed965135c minor cleanups
haftmann
parents: 18850
diff changeset
   248
       (modl,
20105
454f4be984b7 adaptions in codegen
haftmann
parents: 20076
diff changeset
   249
        appgens |> Symtab.update (c, (i, (appgen, stamp ()))),
20386
d1cbe5aa6bf2 module restructuring
haftmann
parents: 20353
diff changeset
   250
        target_data)) thy
18454
6720b5010a57 slight improvements in name handling
haftmann
parents: 18385
diff changeset
   251
  end;
18217
e0b08c9534ff added codegen package
haftmann
parents: 18169
diff changeset
   252
18865
31aed965135c minor cleanups
haftmann
parents: 18850
diff changeset
   253
val add_appconst = gen_add_appconst Sign.intern_const;
31aed965135c minor cleanups
haftmann
parents: 18850
diff changeset
   254
val add_appconst_i = gen_add_appconst (K I);
31aed965135c minor cleanups
haftmann
parents: 18850
diff changeset
   255
31aed965135c minor cleanups
haftmann
parents: 18850
diff changeset
   256
20386
d1cbe5aa6bf2 module restructuring
haftmann
parents: 20353
diff changeset
   257
(* extraction kernel *)
18865
31aed965135c minor cleanups
haftmann
parents: 18850
diff changeset
   258
20386
d1cbe5aa6bf2 module restructuring
haftmann
parents: 20353
diff changeset
   259
fun check_strict thy f x ((false, _), _) =
19884
a7be206d8655 improvements in code generator
haftmann
parents: 19816
diff changeset
   260
      false
20386
d1cbe5aa6bf2 module restructuring
haftmann
parents: 20353
diff changeset
   261
  | check_strict thy f x ((_, SOME targets), _) =
19884
a7be206d8655 improvements in code generator
haftmann
parents: 19816
diff changeset
   262
      exists (
a7be206d8655 improvements in code generator
haftmann
parents: 19816
diff changeset
   263
        is_none o (fn tab => Symtab.lookup tab x) o f o the o (Symtab.lookup ((#target_data o CodegenData.get) thy))
a7be206d8655 improvements in code generator
haftmann
parents: 19816
diff changeset
   264
      ) targets
20386
d1cbe5aa6bf2 module restructuring
haftmann
parents: 20353
diff changeset
   265
  | check_strict thy f x ((true, _), _) =
19884
a7be206d8655 improvements in code generator
haftmann
parents: 19816
diff changeset
   266
      true;
a7be206d8655 improvements in code generator
haftmann
parents: 19816
diff changeset
   267
20386
d1cbe5aa6bf2 module restructuring
haftmann
parents: 20353
diff changeset
   268
fun no_strict ((_, targets), thmtab) = ((false, targets), thmtab);
d1cbe5aa6bf2 module restructuring
haftmann
parents: 20353
diff changeset
   269
d1cbe5aa6bf2 module restructuring
haftmann
parents: 20353
diff changeset
   270
fun sortlookups_const thy thmtab (c, typ_ctxt) =
d1cbe5aa6bf2 module restructuring
haftmann
parents: 20353
diff changeset
   271
  let
d1cbe5aa6bf2 module restructuring
haftmann
parents: 20353
diff changeset
   272
    val typ_decl = case CodegenTheorems.get_fun_thms thmtab (c, typ_ctxt)
d1cbe5aa6bf2 module restructuring
haftmann
parents: 20353
diff changeset
   273
     of thms as thm :: _ => CodegenTheorems.extr_typ thy thm
d1cbe5aa6bf2 module restructuring
haftmann
parents: 20353
diff changeset
   274
      | [] => (case AxClass.class_of_param thy c
d1cbe5aa6bf2 module restructuring
haftmann
parents: 20353
diff changeset
   275
         of SOME class => (case ClassPackage.the_consts_sign thy class of (v, cs) =>
d1cbe5aa6bf2 module restructuring
haftmann
parents: 20353
diff changeset
   276
              (Logic.varifyT o map_type_tfree (fn u as (w, _) =>
d1cbe5aa6bf2 module restructuring
haftmann
parents: 20353
diff changeset
   277
                if w = v then TFree (v, [class]) else TFree u))
d1cbe5aa6bf2 module restructuring
haftmann
parents: 20353
diff changeset
   278
              ((the o AList.lookup (op =) cs) c))
d1cbe5aa6bf2 module restructuring
haftmann
parents: 20353
diff changeset
   279
          | NONE => Sign.the_const_type thy c);
d1cbe5aa6bf2 module restructuring
haftmann
parents: 20353
diff changeset
   280
  in
d1cbe5aa6bf2 module restructuring
haftmann
parents: 20353
diff changeset
   281
    Vartab.empty
d1cbe5aa6bf2 module restructuring
haftmann
parents: 20353
diff changeset
   282
    |> Sign.typ_match thy (typ_decl, typ_ctxt) 
d1cbe5aa6bf2 module restructuring
haftmann
parents: 20353
diff changeset
   283
    |> Vartab.dest
d1cbe5aa6bf2 module restructuring
haftmann
parents: 20353
diff changeset
   284
    |> map_filter (fn (_, ([], _)) => NONE
d1cbe5aa6bf2 module restructuring
haftmann
parents: 20353
diff changeset
   285
                   | (_, (sort, ty)) => SOME (ClassPackage.sortlookup thy (ty, sort)))
d1cbe5aa6bf2 module restructuring
haftmann
parents: 20353
diff changeset
   286
    |> filter_out null
d1cbe5aa6bf2 module restructuring
haftmann
parents: 20353
diff changeset
   287
  end;
19816
a8c8ed1c85e0 removed 'primitive definitions' added (non)strict generation, minor fixes
haftmann
parents: 19806
diff changeset
   288
18865
31aed965135c minor cleanups
haftmann
parents: 18850
diff changeset
   289
fun ensure_def_class thy tabs cls trns =
18454
6720b5010a57 slight improvements in name handling
haftmann
parents: 18385
diff changeset
   290
  let
20386
d1cbe5aa6bf2 module restructuring
haftmann
parents: 20353
diff changeset
   291
    fun defgen_class thy (tabs as (_, thmtab)) cls trns =
d1cbe5aa6bf2 module restructuring
haftmann
parents: 20353
diff changeset
   292
      case class_of_idf thy cls
18865
31aed965135c minor cleanups
haftmann
parents: 18850
diff changeset
   293
       of SOME cls =>
31aed965135c minor cleanups
haftmann
parents: 18850
diff changeset
   294
            let
19283
88172041c084 fixed clsvar bug
haftmann
parents: 19280
diff changeset
   295
              val (v, cs) = (ClassPackage.the_consts_sign thy) cls;
19953
2f54a51f1801 class package refinements, slight code generation refinements
haftmann
parents: 19884
diff changeset
   296
              val sortctxts = map (ClassPackage.sortcontext_of_typ thy o snd) cs;
20386
d1cbe5aa6bf2 module restructuring
haftmann
parents: 20353
diff changeset
   297
              val idfs = map (idf_of_const thy thmtab) cs;
18865
31aed965135c minor cleanups
haftmann
parents: 18850
diff changeset
   298
            in
31aed965135c minor cleanups
haftmann
parents: 18850
diff changeset
   299
              trns
19341
3414c04fbc39 added definitional code generator module: codegen_theorems.ML
haftmann
parents: 19283
diff changeset
   300
              |> debug_msg (fn _ => "trying defgen class declaration for " ^ quote cls)
18865
31aed965135c minor cleanups
haftmann
parents: 18850
diff changeset
   301
              |> fold_map (ensure_def_class thy tabs) (ClassPackage.the_superclasses thy cls)
19816
a8c8ed1c85e0 removed 'primitive definitions' added (non)strict generation, minor fixes
haftmann
parents: 19806
diff changeset
   302
              ||>> (fold_map (exprgen_type thy tabs) o map snd) cs
18865
31aed965135c minor cleanups
haftmann
parents: 18850
diff changeset
   303
              ||>> (fold_map o fold_map) (exprgen_tyvar_sort thy tabs) sortctxts
31aed965135c minor cleanups
haftmann
parents: 18850
diff changeset
   304
              |-> (fn ((supcls, memtypes), sortctxts) => succeed
19283
88172041c084 fixed clsvar bug
haftmann
parents: 19280
diff changeset
   305
                (Class (supcls, (unprefix "'" v, idfs ~~ (sortctxts ~~ memtypes)))))
18865
31aed965135c minor cleanups
haftmann
parents: 18850
diff changeset
   306
            end
31aed965135c minor cleanups
haftmann
parents: 18850
diff changeset
   307
        | _ =>
31aed965135c minor cleanups
haftmann
parents: 18850
diff changeset
   308
            trns
31aed965135c minor cleanups
haftmann
parents: 18850
diff changeset
   309
            |> fail ("no class definition found for " ^ quote cls);
20386
d1cbe5aa6bf2 module restructuring
haftmann
parents: 20353
diff changeset
   310
    val cls' = idf_of_class thy cls;
18454
6720b5010a57 slight improvements in name handling
haftmann
parents: 18385
diff changeset
   311
  in
6720b5010a57 slight improvements in name handling
haftmann
parents: 18385
diff changeset
   312
    trns
19341
3414c04fbc39 added definitional code generator module: codegen_theorems.ML
haftmann
parents: 19283
diff changeset
   313
    |> debug_msg (fn _ => "generating class " ^ quote cls)
19816
a8c8ed1c85e0 removed 'primitive definitions' added (non)strict generation, minor fixes
haftmann
parents: 19806
diff changeset
   314
    |> ensure_def (defgen_class thy tabs) true ("generating class " ^ quote cls) cls'
18865
31aed965135c minor cleanups
haftmann
parents: 18850
diff changeset
   315
    |> pair cls'
31aed965135c minor cleanups
haftmann
parents: 18850
diff changeset
   316
  end
20386
d1cbe5aa6bf2 module restructuring
haftmann
parents: 20353
diff changeset
   317
and ensure_def_tyco thy (tabs as (_, thmtab)) tyco trns =
18865
31aed965135c minor cleanups
haftmann
parents: 18850
diff changeset
   318
  let
20386
d1cbe5aa6bf2 module restructuring
haftmann
parents: 20353
diff changeset
   319
    val tyco' = idf_of_tyco thy tyco;
19816
a8c8ed1c85e0 removed 'primitive definitions' added (non)strict generation, minor fixes
haftmann
parents: 19806
diff changeset
   320
    val strict = check_strict thy #syntax_tyco tyco' tabs;
20386
d1cbe5aa6bf2 module restructuring
haftmann
parents: 20353
diff changeset
   321
    fun defgen_datatype thy (tabs as (_, thmtab)) dtco trns =
d1cbe5aa6bf2 module restructuring
haftmann
parents: 20353
diff changeset
   322
      case tyco_of_idf thy dtco
18963
3adfc9dfb30a slight improvements in code generation
haftmann
parents: 18960
diff changeset
   323
       of SOME dtco =>
20353
d73e49780ef2 code generator refinements
haftmann
parents: 20216
diff changeset
   324
         (case CodegenTheorems.get_dtyp_spec thmtab dtco
d73e49780ef2 code generator refinements
haftmann
parents: 20216
diff changeset
   325
             of SOME (vars, cos) =>
19341
3414c04fbc39 added definitional code generator module: codegen_theorems.ML
haftmann
parents: 19283
diff changeset
   326
                  trns
3414c04fbc39 added definitional code generator module: codegen_theorems.ML
haftmann
parents: 19283
diff changeset
   327
                  |> debug_msg (fn _ => "trying defgen datatype for " ^ quote dtco)
3414c04fbc39 added definitional code generator module: codegen_theorems.ML
haftmann
parents: 19283
diff changeset
   328
                  |> fold_map (exprgen_tyvar_sort thy tabs) vars
19816
a8c8ed1c85e0 removed 'primitive definitions' added (non)strict generation, minor fixes
haftmann
parents: 19806
diff changeset
   329
                  ||>> fold_map (fn (c, tys) =>
a8c8ed1c85e0 removed 'primitive definitions' added (non)strict generation, minor fixes
haftmann
parents: 19806
diff changeset
   330
                    fold_map (exprgen_type thy tabs) tys
20386
d1cbe5aa6bf2 module restructuring
haftmann
parents: 20353
diff changeset
   331
                    #-> (fn tys' => pair (idf_of_const thy thmtab (c, tys ---> Type (dtco, map TFree vars)), tys'))) cos
19341
3414c04fbc39 added definitional code generator module: codegen_theorems.ML
haftmann
parents: 19283
diff changeset
   332
                  |-> (fn (vars, cos) => succeed (Datatype
3414c04fbc39 added definitional code generator module: codegen_theorems.ML
haftmann
parents: 19283
diff changeset
   333
                       (vars, cos)))
18963
3adfc9dfb30a slight improvements in code generation
haftmann
parents: 18960
diff changeset
   334
              | NONE =>
3adfc9dfb30a slight improvements in code generation
haftmann
parents: 18960
diff changeset
   335
                  trns
3adfc9dfb30a slight improvements in code generation
haftmann
parents: 18960
diff changeset
   336
                  |> fail ("no datatype found for " ^ quote dtco))
3adfc9dfb30a slight improvements in code generation
haftmann
parents: 18960
diff changeset
   337
        | NONE =>
3adfc9dfb30a slight improvements in code generation
haftmann
parents: 18960
diff changeset
   338
            trns
3adfc9dfb30a slight improvements in code generation
haftmann
parents: 18960
diff changeset
   339
            |> fail ("not a type constructor: " ^ quote dtco)
18865
31aed965135c minor cleanups
haftmann
parents: 18850
diff changeset
   340
  in
31aed965135c minor cleanups
haftmann
parents: 18850
diff changeset
   341
    trns
19341
3414c04fbc39 added definitional code generator module: codegen_theorems.ML
haftmann
parents: 19283
diff changeset
   342
    |> debug_msg (fn _ => "generating type constructor " ^ quote tyco)
19816
a8c8ed1c85e0 removed 'primitive definitions' added (non)strict generation, minor fixes
haftmann
parents: 19806
diff changeset
   343
    |> ensure_def (defgen_datatype thy tabs) strict ("generating type constructor " ^ quote tyco) tyco'
18865
31aed965135c minor cleanups
haftmann
parents: 18850
diff changeset
   344
    |> pair tyco'
31aed965135c minor cleanups
haftmann
parents: 18850
diff changeset
   345
  end
31aed965135c minor cleanups
haftmann
parents: 18850
diff changeset
   346
and exprgen_tyvar_sort thy tabs (v, sort) trns =
18516
4424e2bce9af slightly improved serialization
haftmann
parents: 18515
diff changeset
   347
  trns
18885
ee8b5c36ba2b substantial cleanup and simplifications
haftmann
parents: 18865
diff changeset
   348
  |> fold_map (ensure_def_class thy tabs) (ClassPackage.operational_sort_of thy sort)
18865
31aed965135c minor cleanups
haftmann
parents: 18850
diff changeset
   349
  |-> (fn sort => pair (unprefix "'" v, sort))
31aed965135c minor cleanups
haftmann
parents: 18850
diff changeset
   350
and exprgen_type thy tabs (TVar _) trns =
18516
4424e2bce9af slightly improved serialization
haftmann
parents: 18515
diff changeset
   351
      error "TVar encountered during code generation"
18702
7dc7dcd63224 substantial improvements in code generator
haftmann
parents: 18517
diff changeset
   352
  | exprgen_type thy tabs (TFree v_s) trns =
18516
4424e2bce9af slightly improved serialization
haftmann
parents: 18515
diff changeset
   353
      trns
18702
7dc7dcd63224 substantial improvements in code generator
haftmann
parents: 18517
diff changeset
   354
      |> exprgen_tyvar_sort thy tabs v_s
19167
f237c0cb3882 refined representation of codegen intermediate language
haftmann
parents: 19150
diff changeset
   355
      |-> (fn (v, sort) => pair (ITyVar v))
18516
4424e2bce9af slightly improved serialization
haftmann
parents: 18515
diff changeset
   356
  | exprgen_type thy tabs (Type ("fun", [t1, t2])) trns =
4424e2bce9af slightly improved serialization
haftmann
parents: 18515
diff changeset
   357
      trns
4424e2bce9af slightly improved serialization
haftmann
parents: 18515
diff changeset
   358
      |> exprgen_type thy tabs t1
4424e2bce9af slightly improved serialization
haftmann
parents: 18515
diff changeset
   359
      ||>> exprgen_type thy tabs t2
4424e2bce9af slightly improved serialization
haftmann
parents: 18515
diff changeset
   360
      |-> (fn (t1', t2') => pair (t1' `-> t2'))
4424e2bce9af slightly improved serialization
haftmann
parents: 18515
diff changeset
   361
  | exprgen_type thy tabs (Type (tyco, tys)) trns =
4424e2bce9af slightly improved serialization
haftmann
parents: 18515
diff changeset
   362
      trns
4424e2bce9af slightly improved serialization
haftmann
parents: 18515
diff changeset
   363
      |> ensure_def_tyco thy tabs tyco
4424e2bce9af slightly improved serialization
haftmann
parents: 18515
diff changeset
   364
      ||>> fold_map (exprgen_type thy tabs) tys
19816
a8c8ed1c85e0 removed 'primitive definitions' added (non)strict generation, minor fixes
haftmann
parents: 19806
diff changeset
   365
      |-> (fn (tyco, tys) => pair (tyco `%% tys));
18516
4424e2bce9af slightly improved serialization
haftmann
parents: 18515
diff changeset
   366
18885
ee8b5c36ba2b substantial cleanup and simplifications
haftmann
parents: 18865
diff changeset
   367
fun exprgen_classlookup thy tabs (ClassPackage.Instance (inst, ls)) trns =
18517
788fa99aba33 slight improvements
haftmann
parents: 18516
diff changeset
   368
      trns
18885
ee8b5c36ba2b substantial cleanup and simplifications
haftmann
parents: 18865
diff changeset
   369
      |> ensure_def_inst thy tabs inst
ee8b5c36ba2b substantial cleanup and simplifications
haftmann
parents: 18865
diff changeset
   370
      ||>> (fold_map o fold_map) (exprgen_classlookup thy tabs) ls
ee8b5c36ba2b substantial cleanup and simplifications
haftmann
parents: 18865
diff changeset
   371
      |-> (fn (inst, ls) => pair (Instance (inst, ls)))
19253
f3ce97b5661a refined representation of instance dictionaries
haftmann
parents: 19213
diff changeset
   372
  | exprgen_classlookup thy tabs (ClassPackage.Lookup (clss, (v, (i, j)))) trns =
18516
4424e2bce9af slightly improved serialization
haftmann
parents: 18515
diff changeset
   373
      trns
18517
788fa99aba33 slight improvements
haftmann
parents: 18516
diff changeset
   374
      |> fold_map (ensure_def_class thy tabs) clss
19253
f3ce97b5661a refined representation of instance dictionaries
haftmann
parents: 19213
diff changeset
   375
      |-> (fn clss => pair (Lookup (clss, (v |> unprefix "'", if j = 1 then ~1 else i))))
20386
d1cbe5aa6bf2 module restructuring
haftmann
parents: 20353
diff changeset
   376
and mk_fun thy (tabs as (_, thmtab)) (c, ty) trns =
d1cbe5aa6bf2 module restructuring
haftmann
parents: 20353
diff changeset
   377
  case CodegenTheorems.get_fun_thms thmtab (c, ty)
19953
2f54a51f1801 class package refinements, slight code generation refinements
haftmann
parents: 19884
diff changeset
   378
   of eq_thms as eq_thm :: _ =>
18865
31aed965135c minor cleanups
haftmann
parents: 18850
diff changeset
   379
        let
19884
a7be206d8655 improvements in code generator
haftmann
parents: 19816
diff changeset
   380
          val msg = cat_lines ("generating code for theorems " :: map string_of_thm eq_thms);
20386
d1cbe5aa6bf2 module restructuring
haftmann
parents: 20353
diff changeset
   381
          val ty = (Logic.unvarifyT o CodegenTheorems.extr_typ thy) eq_thm
19953
2f54a51f1801 class package refinements, slight code generation refinements
haftmann
parents: 19884
diff changeset
   382
          val sortcontext = ClassPackage.sortcontext_of_typ thy ty;
18865
31aed965135c minor cleanups
haftmann
parents: 18850
diff changeset
   383
          fun dest_eqthm eq_thm =
31aed965135c minor cleanups
haftmann
parents: 18850
diff changeset
   384
            let
31aed965135c minor cleanups
haftmann
parents: 18850
diff changeset
   385
              val ((t, args), rhs) =
19953
2f54a51f1801 class package refinements, slight code generation refinements
haftmann
parents: 19884
diff changeset
   386
                (apfst strip_comb o Logic.dest_equals o Logic.legacy_unvarify o prop_of) eq_thm;
18865
31aed965135c minor cleanups
haftmann
parents: 18850
diff changeset
   387
            in case t
31aed965135c minor cleanups
haftmann
parents: 18850
diff changeset
   388
             of Const (c', _) => if c' = c then (args, rhs)
31aed965135c minor cleanups
haftmann
parents: 18850
diff changeset
   389
                 else error ("illegal function equation for " ^ quote c
31aed965135c minor cleanups
haftmann
parents: 18850
diff changeset
   390
                   ^ ", actually defining " ^ quote c')
31aed965135c minor cleanups
haftmann
parents: 18850
diff changeset
   391
              | _ => error ("illegal function equation for " ^ quote c)
31aed965135c minor cleanups
haftmann
parents: 18850
diff changeset
   392
            end;
19816
a8c8ed1c85e0 removed 'primitive definitions' added (non)strict generation, minor fixes
haftmann
parents: 19806
diff changeset
   393
          fun exprgen_eq (args, rhs) trns =
a8c8ed1c85e0 removed 'primitive definitions' added (non)strict generation, minor fixes
haftmann
parents: 19806
diff changeset
   394
            trns
a8c8ed1c85e0 removed 'primitive definitions' added (non)strict generation, minor fixes
haftmann
parents: 19806
diff changeset
   395
            |> fold_map (exprgen_term thy tabs) args
19884
a7be206d8655 improvements in code generator
haftmann
parents: 19816
diff changeset
   396
            ||>> exprgen_term thy tabs rhs;
20105
454f4be984b7 adaptions in codegen
haftmann
parents: 20076
diff changeset
   397
          fun checkvars (args, rhs) =
454f4be984b7 adaptions in codegen
haftmann
parents: 20076
diff changeset
   398
            if CodegenThingol.vars_distinct args then (args, rhs)
454f4be984b7 adaptions in codegen
haftmann
parents: 20076
diff changeset
   399
            else error ("repeated variables on left hand side of function")
18865
31aed965135c minor cleanups
haftmann
parents: 18850
diff changeset
   400
        in
18517
788fa99aba33 slight improvements
haftmann
parents: 18516
diff changeset
   401
          trns
19884
a7be206d8655 improvements in code generator
haftmann
parents: 19816
diff changeset
   402
          |> message msg (fn trns => trns
19816
a8c8ed1c85e0 removed 'primitive definitions' added (non)strict generation, minor fixes
haftmann
parents: 19806
diff changeset
   403
          |> fold_map (exprgen_eq o dest_eqthm) eq_thms
20105
454f4be984b7 adaptions in codegen
haftmann
parents: 20076
diff changeset
   404
          |-> (fn eqs => pair (map checkvars eqs))
19953
2f54a51f1801 class package refinements, slight code generation refinements
haftmann
parents: 19884
diff changeset
   405
          ||>> fold_map (exprgen_tyvar_sort thy tabs) sortcontext
19816
a8c8ed1c85e0 removed 'primitive definitions' added (non)strict generation, minor fixes
haftmann
parents: 19806
diff changeset
   406
          ||>> exprgen_type thy tabs ty
19953
2f54a51f1801 class package refinements, slight code generation refinements
haftmann
parents: 19884
diff changeset
   407
          |-> (fn ((eqs, sortctxt), ty) => (pair o SOME) ((eqs, (sortctxt, ty)), map snd sortcontext)))
18865
31aed965135c minor cleanups
haftmann
parents: 18850
diff changeset
   408
        end
19953
2f54a51f1801 class package refinements, slight code generation refinements
haftmann
parents: 19884
diff changeset
   409
    | [] => (NONE, trns)
20386
d1cbe5aa6bf2 module restructuring
haftmann
parents: 20353
diff changeset
   410
and ensure_def_inst thy tabs (cls, tyco) trns =
18865
31aed965135c minor cleanups
haftmann
parents: 18850
diff changeset
   411
  let
20386
d1cbe5aa6bf2 module restructuring
haftmann
parents: 20353
diff changeset
   412
    fun defgen_inst thy (tabs as (_, thmtab)) inst trns =
d1cbe5aa6bf2 module restructuring
haftmann
parents: 20353
diff changeset
   413
      case inst_of_idf thy inst
19956
f992e507020e slight improvements in code generation
haftmann
parents: 19953
diff changeset
   414
       of SOME (class, tyco) =>
18865
31aed965135c minor cleanups
haftmann
parents: 18850
diff changeset
   415
            let
18885
ee8b5c36ba2b substantial cleanup and simplifications
haftmann
parents: 18865
diff changeset
   416
              val (arity, memdefs) = ClassPackage.the_inst_sign thy (class, tyco);
20386
d1cbe5aa6bf2 module restructuring
haftmann
parents: 20353
diff changeset
   417
              val (_, memnames) = ClassPackage.the_consts_sign thy class;
19953
2f54a51f1801 class package refinements, slight code generation refinements
haftmann
parents: 19884
diff changeset
   418
              val arity_typ = Type (tyco, (map TFree arity));
2f54a51f1801 class package refinements, slight code generation refinements
haftmann
parents: 19884
diff changeset
   419
              val operational_arity = map_filter (fn (v, sort) => case ClassPackage.operational_sort_of thy sort
2f54a51f1801 class package refinements, slight code generation refinements
haftmann
parents: 19884
diff changeset
   420
               of [] => NONE
2f54a51f1801 class package refinements, slight code generation refinements
haftmann
parents: 19884
diff changeset
   421
                | sort => SOME (v, sort)) arity;
20386
d1cbe5aa6bf2 module restructuring
haftmann
parents: 20353
diff changeset
   422
              fun mk_instmemname (m, ty) =
d1cbe5aa6bf2 module restructuring
haftmann
parents: 20353
diff changeset
   423
                NameSpace.append (NameSpace.append ((NameSpace.drop_base o NameSpace.drop_base)
d1cbe5aa6bf2 module restructuring
haftmann
parents: 20353
diff changeset
   424
                  inst) nsp_instmem) (NameSpace.base (idf_of_const thy thmtab (m, ty)));
18865
31aed965135c minor cleanups
haftmann
parents: 18850
diff changeset
   425
              fun gen_suparity supclass trns =
31aed965135c minor cleanups
haftmann
parents: 18850
diff changeset
   426
                trns
19136
00ade10f611d some refinements
haftmann
parents: 19111
diff changeset
   427
                |> ensure_def_class thy tabs supclass
19953
2f54a51f1801 class package refinements, slight code generation refinements
haftmann
parents: 19884
diff changeset
   428
                ||>> fold_map (exprgen_classlookup thy tabs)
20386
d1cbe5aa6bf2 module restructuring
haftmann
parents: 20353
diff changeset
   429
                      (ClassPackage.sortlookup thy (arity_typ, [supclass]));
d1cbe5aa6bf2 module restructuring
haftmann
parents: 20353
diff changeset
   430
              fun gen_membr ((m0, ty0), (m, ty)) trns =
18865
31aed965135c minor cleanups
haftmann
parents: 18850
diff changeset
   431
                trns
19341
3414c04fbc39 added definitional code generator module: codegen_theorems.ML
haftmann
parents: 19283
diff changeset
   432
                |> mk_fun thy tabs (m, ty)
19280
5091dc43817b slight improvement in serializer, stub for code generator theorems added
haftmann
parents: 19253
diff changeset
   433
                |-> (fn NONE => error ("could not derive definition for member "
5091dc43817b slight improvement in serializer, stub for code generator theorems added
haftmann
parents: 19253
diff changeset
   434
                          ^ quote m ^ " :: " ^ Sign.string_of_typ thy ty)
19953
2f54a51f1801 class package refinements, slight code generation refinements
haftmann
parents: 19884
diff changeset
   435
                      | SOME (funn, sorts) => fold_map (fn (sort, sort_ctxt) =>
2f54a51f1801 class package refinements, slight code generation refinements
haftmann
parents: 19884
diff changeset
   436
                          fold_map (exprgen_classlookup thy tabs)
20386
d1cbe5aa6bf2 module restructuring
haftmann
parents: 20353
diff changeset
   437
                            (ClassPackage.sortlookup thy (TFree sort_ctxt, sort)))
20191
b43fd26e1aaa improvements for lazy code generation
haftmann
parents: 20183
diff changeset
   438
                            (sorts ~~ operational_arity)
19253
f3ce97b5661a refined representation of instance dictionaries
haftmann
parents: 19213
diff changeset
   439
                #-> (fn lss =>
20386
d1cbe5aa6bf2 module restructuring
haftmann
parents: 20353
diff changeset
   440
                       pair (idf_of_const thy thmtab (m0, ty0),
d1cbe5aa6bf2 module restructuring
haftmann
parents: 20353
diff changeset
   441
                         ((mk_instmemname (m0, ty0), funn), lss))));
18865
31aed965135c minor cleanups
haftmann
parents: 18850
diff changeset
   442
            in
31aed965135c minor cleanups
haftmann
parents: 18850
diff changeset
   443
              trns
19341
3414c04fbc39 added definitional code generator module: codegen_theorems.ML
haftmann
parents: 19283
diff changeset
   444
              |> debug_msg (fn _ => "trying defgen class instance for (" ^ quote cls
18865
31aed965135c minor cleanups
haftmann
parents: 18850
diff changeset
   445
                   ^ ", " ^ quote tyco ^ ")")
18885
ee8b5c36ba2b substantial cleanup and simplifications
haftmann
parents: 18865
diff changeset
   446
              |> ensure_def_class thy tabs class
18865
31aed965135c minor cleanups
haftmann
parents: 18850
diff changeset
   447
              ||>> ensure_def_tyco thy tabs tyco
31aed965135c minor cleanups
haftmann
parents: 18850
diff changeset
   448
              ||>> fold_map (exprgen_tyvar_sort thy tabs) arity
18885
ee8b5c36ba2b substantial cleanup and simplifications
haftmann
parents: 18865
diff changeset
   449
              ||>> fold_map gen_suparity (ClassPackage.the_superclasses thy class)
20386
d1cbe5aa6bf2 module restructuring
haftmann
parents: 20353
diff changeset
   450
              ||>> fold_map gen_membr (memnames ~~ memdefs)
18885
ee8b5c36ba2b substantial cleanup and simplifications
haftmann
parents: 18865
diff changeset
   451
              |-> (fn ((((class, tyco), arity), suparities), memdefs) =>
ee8b5c36ba2b substantial cleanup and simplifications
haftmann
parents: 18865
diff changeset
   452
                     succeed (Classinst (((class, (tyco, arity)), suparities), memdefs)))
18865
31aed965135c minor cleanups
haftmann
parents: 18850
diff changeset
   453
            end
31aed965135c minor cleanups
haftmann
parents: 18850
diff changeset
   454
        | _ =>
31aed965135c minor cleanups
haftmann
parents: 18850
diff changeset
   455
            trns |> fail ("no class instance found for " ^ quote inst);
20386
d1cbe5aa6bf2 module restructuring
haftmann
parents: 20353
diff changeset
   456
    val inst = idf_of_inst thy (cls, tyco);
18865
31aed965135c minor cleanups
haftmann
parents: 18850
diff changeset
   457
  in
31aed965135c minor cleanups
haftmann
parents: 18850
diff changeset
   458
    trns
19341
3414c04fbc39 added definitional code generator module: codegen_theorems.ML
haftmann
parents: 19283
diff changeset
   459
    |> debug_msg (fn _ => "generating instance " ^ quote cls ^ " / " ^ quote tyco)
19816
a8c8ed1c85e0 removed 'primitive definitions' added (non)strict generation, minor fixes
haftmann
parents: 19806
diff changeset
   460
    |> ensure_def (defgen_inst thy tabs) true
18865
31aed965135c minor cleanups
haftmann
parents: 18850
diff changeset
   461
         ("generating instance " ^ quote cls ^ " / " ^ quote tyco) inst
31aed965135c minor cleanups
haftmann
parents: 18850
diff changeset
   462
    |> pair inst
31aed965135c minor cleanups
haftmann
parents: 18850
diff changeset
   463
  end
20386
d1cbe5aa6bf2 module restructuring
haftmann
parents: 20353
diff changeset
   464
and ensure_def_const thy (tabs as (_, thmtab)) (c, ty) trns =
18865
31aed965135c minor cleanups
haftmann
parents: 18850
diff changeset
   465
  let
20386
d1cbe5aa6bf2 module restructuring
haftmann
parents: 20353
diff changeset
   466
    fun defgen_datatypecons thy (tabs as (_, thmtab)) co trns =
d1cbe5aa6bf2 module restructuring
haftmann
parents: 20353
diff changeset
   467
      case CodegenTheorems.get_dtyp_of_cons thmtab ((the o const_of_idf thy) co)
d1cbe5aa6bf2 module restructuring
haftmann
parents: 20353
diff changeset
   468
       of SOME tyco =>
18865
31aed965135c minor cleanups
haftmann
parents: 18850
diff changeset
   469
            trns
19341
3414c04fbc39 added definitional code generator module: codegen_theorems.ML
haftmann
parents: 19283
diff changeset
   470
            |> debug_msg (fn _ => "trying defgen datatype constructor for " ^ quote co)
20386
d1cbe5aa6bf2 module restructuring
haftmann
parents: 20353
diff changeset
   471
            |> ensure_def_tyco thy tabs tyco
d1cbe5aa6bf2 module restructuring
haftmann
parents: 20353
diff changeset
   472
            |-> (fn _ => succeed Bot)
18865
31aed965135c minor cleanups
haftmann
parents: 18850
diff changeset
   473
        | _ =>
31aed965135c minor cleanups
haftmann
parents: 18850
diff changeset
   474
            trns
31aed965135c minor cleanups
haftmann
parents: 18850
diff changeset
   475
            |> fail ("not a datatype constructor: " ^ quote co);
20386
d1cbe5aa6bf2 module restructuring
haftmann
parents: 20353
diff changeset
   476
    fun defgen_clsmem thy (tabs as (_, thmtab)) m trns =
d1cbe5aa6bf2 module restructuring
haftmann
parents: 20353
diff changeset
   477
      case CodegenConsts.class_of_classop thy
d1cbe5aa6bf2 module restructuring
haftmann
parents: 20353
diff changeset
   478
        ((CodegenConsts.typinst_of_typ thy o the o const_of_idf thy) m)
d1cbe5aa6bf2 module restructuring
haftmann
parents: 20353
diff changeset
   479
       of SOME class =>
d1cbe5aa6bf2 module restructuring
haftmann
parents: 20353
diff changeset
   480
            trns
d1cbe5aa6bf2 module restructuring
haftmann
parents: 20353
diff changeset
   481
            |> debug_msg (fn _ => "trying defgen class member for " ^ quote m)
d1cbe5aa6bf2 module restructuring
haftmann
parents: 20353
diff changeset
   482
            |> ensure_def_class thy tabs class
d1cbe5aa6bf2 module restructuring
haftmann
parents: 20353
diff changeset
   483
            |-> (fn _ => succeed Bot)
d1cbe5aa6bf2 module restructuring
haftmann
parents: 20353
diff changeset
   484
        | _ =>
d1cbe5aa6bf2 module restructuring
haftmann
parents: 20353
diff changeset
   485
            trns |> fail ("no class found for " ^ quote m)
d1cbe5aa6bf2 module restructuring
haftmann
parents: 20353
diff changeset
   486
    fun defgen_funs thy (tabs as (_, thmtab)) c' trns =
d1cbe5aa6bf2 module restructuring
haftmann
parents: 20353
diff changeset
   487
        trns
d1cbe5aa6bf2 module restructuring
haftmann
parents: 20353
diff changeset
   488
        |> mk_fun thy tabs ((the o const_of_idf thy) c')
d1cbe5aa6bf2 module restructuring
haftmann
parents: 20353
diff changeset
   489
        |-> (fn SOME (funn, _) => succeed (Fun funn)
d1cbe5aa6bf2 module restructuring
haftmann
parents: 20353
diff changeset
   490
              | NONE => fail ("no defining equations found for " ^
d1cbe5aa6bf2 module restructuring
haftmann
parents: 20353
diff changeset
   491
                  (quote (c ^ " :: " ^ Sign.string_of_typ thy ty))))
19816
a8c8ed1c85e0 removed 'primitive definitions' added (non)strict generation, minor fixes
haftmann
parents: 19806
diff changeset
   492
    fun get_defgen tabs idf strict =
20386
d1cbe5aa6bf2 module restructuring
haftmann
parents: 20353
diff changeset
   493
      if (is_some oo dest_nsp) nsp_const idf
19816
a8c8ed1c85e0 removed 'primitive definitions' added (non)strict generation, minor fixes
haftmann
parents: 19806
diff changeset
   494
      then defgen_funs thy tabs strict
20386
d1cbe5aa6bf2 module restructuring
haftmann
parents: 20353
diff changeset
   495
      else if (is_some oo dest_nsp) nsp_mem idf
19816
a8c8ed1c85e0 removed 'primitive definitions' added (non)strict generation, minor fixes
haftmann
parents: 19806
diff changeset
   496
      then defgen_clsmem thy tabs strict
20386
d1cbe5aa6bf2 module restructuring
haftmann
parents: 20353
diff changeset
   497
      else if (is_some oo dest_nsp) nsp_dtcon idf
19816
a8c8ed1c85e0 removed 'primitive definitions' added (non)strict generation, minor fixes
haftmann
parents: 19806
diff changeset
   498
      then defgen_datatypecons thy tabs strict
18963
3adfc9dfb30a slight improvements in code generation
haftmann
parents: 18960
diff changeset
   499
      else error ("illegal shallow name space for constant: " ^ quote idf);
20386
d1cbe5aa6bf2 module restructuring
haftmann
parents: 20353
diff changeset
   500
    val idf = idf_of_const thy thmtab (c, ty);
19816
a8c8ed1c85e0 removed 'primitive definitions' added (non)strict generation, minor fixes
haftmann
parents: 19806
diff changeset
   501
    val strict = check_strict thy #syntax_const idf tabs;
18865
31aed965135c minor cleanups
haftmann
parents: 18850
diff changeset
   502
  in
31aed965135c minor cleanups
haftmann
parents: 18850
diff changeset
   503
    trns
20353
d73e49780ef2 code generator refinements
haftmann
parents: 20216
diff changeset
   504
    |> debug_msg (fn _ => "generating constant " ^ (quote (c ^ " :: " ^ Sign.string_of_typ thy ty)))
19816
a8c8ed1c85e0 removed 'primitive definitions' added (non)strict generation, minor fixes
haftmann
parents: 19806
diff changeset
   505
    |> ensure_def (get_defgen tabs idf) strict ("generating constant " ^ quote c) idf
18963
3adfc9dfb30a slight improvements in code generation
haftmann
parents: 18960
diff changeset
   506
    |> pair idf
18865
31aed965135c minor cleanups
haftmann
parents: 18850
diff changeset
   507
  end
18517
788fa99aba33 slight improvements
haftmann
parents: 18516
diff changeset
   508
and exprgen_term thy tabs (Const (f, ty)) trns =
788fa99aba33 slight improvements
haftmann
parents: 18516
diff changeset
   509
      trns
788fa99aba33 slight improvements
haftmann
parents: 18516
diff changeset
   510
      |> appgen thy tabs ((f, ty), [])
18516
4424e2bce9af slightly improved serialization
haftmann
parents: 18515
diff changeset
   511
      |-> (fn e => pair e)
18912
dd168daf172d improvement in devarifications
haftmann
parents: 18885
diff changeset
   512
  | exprgen_term thy tabs (Var _) trns =
dd168daf172d improvement in devarifications
haftmann
parents: 18885
diff changeset
   513
      error "Var encountered during code generation"
18516
4424e2bce9af slightly improved serialization
haftmann
parents: 18515
diff changeset
   514
  | exprgen_term thy tabs (Free (v, ty)) trns =
4424e2bce9af slightly improved serialization
haftmann
parents: 18515
diff changeset
   515
      trns
18912
dd168daf172d improvement in devarifications
haftmann
parents: 18885
diff changeset
   516
      |> exprgen_type thy tabs ty
19167
f237c0cb3882 refined representation of codegen intermediate language
haftmann
parents: 19150
diff changeset
   517
      |-> (fn ty => pair (IVar v))
19967
33da452f0abe slight refinements
haftmann
parents: 19956
diff changeset
   518
  | exprgen_term thy tabs (Abs (raw_v, ty, raw_t)) trns =
19136
00ade10f611d some refinements
haftmann
parents: 19111
diff changeset
   519
      let
20386
d1cbe5aa6bf2 module restructuring
haftmann
parents: 20353
diff changeset
   520
        val (v, t) = Syntax.variant_abs (CodegenNames.purify_var raw_v, ty, raw_t);
19136
00ade10f611d some refinements
haftmann
parents: 19111
diff changeset
   521
      in
00ade10f611d some refinements
haftmann
parents: 19111
diff changeset
   522
        trns
00ade10f611d some refinements
haftmann
parents: 19111
diff changeset
   523
        |> exprgen_type thy tabs ty
00ade10f611d some refinements
haftmann
parents: 19111
diff changeset
   524
        ||>> exprgen_term thy tabs t
19167
f237c0cb3882 refined representation of codegen intermediate language
haftmann
parents: 19150
diff changeset
   525
        |-> (fn (ty, e) => pair ((v, ty) `|-> e))
19136
00ade10f611d some refinements
haftmann
parents: 19111
diff changeset
   526
      end
18516
4424e2bce9af slightly improved serialization
haftmann
parents: 18515
diff changeset
   527
  | exprgen_term thy tabs (t as t1 $ t2) trns =
4424e2bce9af slightly improved serialization
haftmann
parents: 18515
diff changeset
   528
      let
4424e2bce9af slightly improved serialization
haftmann
parents: 18515
diff changeset
   529
        val (t', ts) = strip_comb t
4424e2bce9af slightly improved serialization
haftmann
parents: 18515
diff changeset
   530
      in case t'
4424e2bce9af slightly improved serialization
haftmann
parents: 18515
diff changeset
   531
       of Const (f, ty) =>
4424e2bce9af slightly improved serialization
haftmann
parents: 18515
diff changeset
   532
            trns
18517
788fa99aba33 slight improvements
haftmann
parents: 18516
diff changeset
   533
            |> appgen thy tabs ((f, ty), ts)
18516
4424e2bce9af slightly improved serialization
haftmann
parents: 18515
diff changeset
   534
            |-> (fn e => pair e)
4424e2bce9af slightly improved serialization
haftmann
parents: 18515
diff changeset
   535
        | _ =>
4424e2bce9af slightly improved serialization
haftmann
parents: 18515
diff changeset
   536
            trns
4424e2bce9af slightly improved serialization
haftmann
parents: 18515
diff changeset
   537
            |> exprgen_term thy tabs t'
4424e2bce9af slightly improved serialization
haftmann
parents: 18515
diff changeset
   538
            ||>> fold_map (exprgen_term thy tabs) ts
4424e2bce9af slightly improved serialization
haftmann
parents: 18515
diff changeset
   539
            |-> (fn (e, es) => pair (e `$$ es))
18865
31aed965135c minor cleanups
haftmann
parents: 18850
diff changeset
   540
      end
20386
d1cbe5aa6bf2 module restructuring
haftmann
parents: 20353
diff changeset
   541
and appgen_default thy (tabs as (_, thmtab)) ((c, ty), ts) trns =
18865
31aed965135c minor cleanups
haftmann
parents: 18850
diff changeset
   542
  trns
31aed965135c minor cleanups
haftmann
parents: 18850
diff changeset
   543
  |> ensure_def_const thy tabs (c, ty)
19816
a8c8ed1c85e0 removed 'primitive definitions' added (non)strict generation, minor fixes
haftmann
parents: 19806
diff changeset
   544
  ||>> exprgen_type thy tabs ty
18885
ee8b5c36ba2b substantial cleanup and simplifications
haftmann
parents: 18865
diff changeset
   545
  ||>> (fold_map o fold_map) (exprgen_classlookup thy tabs)
20386
d1cbe5aa6bf2 module restructuring
haftmann
parents: 20353
diff changeset
   546
         (sortlookups_const thy thmtab (c, ty))
18912
dd168daf172d improvement in devarifications
haftmann
parents: 18885
diff changeset
   547
  ||>> fold_map (exprgen_term thy tabs) ts
19816
a8c8ed1c85e0 removed 'primitive definitions' added (non)strict generation, minor fixes
haftmann
parents: 19806
diff changeset
   548
  |-> (fn (((c, ty), ls), es) =>
19202
0b9eb4b0ad98 substantial improvement in codegen iml
haftmann
parents: 19177
diff changeset
   549
         pair (IConst (c, (ls, ty)) `$$ es))
18865
31aed965135c minor cleanups
haftmann
parents: 18850
diff changeset
   550
and appgen thy tabs ((f, ty), ts) trns =
20105
454f4be984b7 adaptions in codegen
haftmann
parents: 20076
diff changeset
   551
  case Symtab.lookup ((#appgens o CodegenData.get) thy) f
454f4be984b7 adaptions in codegen
haftmann
parents: 20076
diff changeset
   552
   of SOME (i, (ag, _)) =>
454f4be984b7 adaptions in codegen
haftmann
parents: 20076
diff changeset
   553
        if length ts < i then
18865
31aed965135c minor cleanups
haftmann
parents: 18850
diff changeset
   554
          let
20105
454f4be984b7 adaptions in codegen
haftmann
parents: 20076
diff changeset
   555
            val tys = Library.take (i - length ts, ((fst o strip_type) ty));
20192
956cd30ef3be renamed Name.give_names to Name.names and moved Name.alphanum to Symbol.alphanum
haftmann
parents: 20191
diff changeset
   556
            val vs = Name.names (Name.declare f Name.context) "a" tys;
18865
31aed965135c minor cleanups
haftmann
parents: 18850
diff changeset
   557
          in
31aed965135c minor cleanups
haftmann
parents: 18850
diff changeset
   558
            trns
18912
dd168daf172d improvement in devarifications
haftmann
parents: 18885
diff changeset
   559
            |> fold_map (exprgen_type thy tabs) tys
20105
454f4be984b7 adaptions in codegen
haftmann
parents: 20076
diff changeset
   560
            ||>> ag thy tabs ((f, ty), ts @ map Free vs)
454f4be984b7 adaptions in codegen
haftmann
parents: 20076
diff changeset
   561
            |-> (fn (tys, e) => pair (map2 (fn (v, _) => pair v) vs tys `|--> e))
18865
31aed965135c minor cleanups
haftmann
parents: 18850
diff changeset
   562
          end
20105
454f4be984b7 adaptions in codegen
haftmann
parents: 20076
diff changeset
   563
        else if length ts > i then
18865
31aed965135c minor cleanups
haftmann
parents: 18850
diff changeset
   564
          trns
20105
454f4be984b7 adaptions in codegen
haftmann
parents: 20076
diff changeset
   565
          |> ag thy tabs ((f, ty), Library.take (i, ts))
454f4be984b7 adaptions in codegen
haftmann
parents: 20076
diff changeset
   566
          ||>> fold_map (exprgen_term thy tabs) (Library.drop (i, ts))
19167
f237c0cb3882 refined representation of codegen intermediate language
haftmann
parents: 19150
diff changeset
   567
          |-> (fn (e, es) => pair (e `$$ es))
18865
31aed965135c minor cleanups
haftmann
parents: 18850
diff changeset
   568
        else
31aed965135c minor cleanups
haftmann
parents: 18850
diff changeset
   569
          trns
31aed965135c minor cleanups
haftmann
parents: 18850
diff changeset
   570
          |> ag thy tabs ((f, ty), ts)
31aed965135c minor cleanups
haftmann
parents: 18850
diff changeset
   571
    | NONE =>
31aed965135c minor cleanups
haftmann
parents: 18850
diff changeset
   572
        trns
31aed965135c minor cleanups
haftmann
parents: 18850
diff changeset
   573
        |> appgen_default thy tabs ((f, ty), ts);
18516
4424e2bce9af slightly improved serialization
haftmann
parents: 18515
diff changeset
   574
18702
7dc7dcd63224 substantial improvements in code generator
haftmann
parents: 18517
diff changeset
   575
18217
e0b08c9534ff added codegen package
haftmann
parents: 18169
diff changeset
   576
(* parametrized generators, for instantiation in HOL *)
e0b08c9534ff added codegen package
haftmann
parents: 18169
diff changeset
   577
20353
d73e49780ef2 code generator refinements
haftmann
parents: 20216
diff changeset
   578
fun appgen_rep_bin int_of_numeral thy tabs (app as (c as (_, ty), [bin])) trns =
d73e49780ef2 code generator refinements
haftmann
parents: 20216
diff changeset
   579
  case try (int_of_numeral thy) bin
d73e49780ef2 code generator refinements
haftmann
parents: 20216
diff changeset
   580
   of SOME i => if i < 0 then (*preprocessor eliminates negative numerals*)
d73e49780ef2 code generator refinements
haftmann
parents: 20216
diff changeset
   581
        trns
d73e49780ef2 code generator refinements
haftmann
parents: 20216
diff changeset
   582
        |> appgen_default thy (no_strict tabs) app
19884
a7be206d8655 improvements in code generator
haftmann
parents: 19816
diff changeset
   583
      else
a7be206d8655 improvements in code generator
haftmann
parents: 19816
diff changeset
   584
        trns
20353
d73e49780ef2 code generator refinements
haftmann
parents: 20216
diff changeset
   585
        |> exprgen_term thy (no_strict tabs) (Const c)
19884
a7be206d8655 improvements in code generator
haftmann
parents: 19816
diff changeset
   586
        ||>> exprgen_term thy (no_strict tabs) bin
20353
d73e49780ef2 code generator refinements
haftmann
parents: 20216
diff changeset
   587
        |-> (fn (e1, e2) => pair (CodegenThingol.INum (i, e1 `$ e2)))
19884
a7be206d8655 improvements in code generator
haftmann
parents: 19816
diff changeset
   588
    | NONE =>
a7be206d8655 improvements in code generator
haftmann
parents: 19816
diff changeset
   589
        trns
a7be206d8655 improvements in code generator
haftmann
parents: 19816
diff changeset
   590
        |> appgen_default thy tabs app;
18217
e0b08c9534ff added codegen package
haftmann
parents: 18169
diff changeset
   591
19607
07eeb832f28d introduced characters for code generator; some improved code lemmas for some list functions
haftmann
parents: 19597
diff changeset
   592
fun appgen_char char_to_index thy tabs (app as ((_, ty), _)) trns =
07eeb832f28d introduced characters for code generator; some improved code lemmas for some list functions
haftmann
parents: 19597
diff changeset
   593
  case (char_to_index o list_comb o apfst Const) app
07eeb832f28d introduced characters for code generator; some improved code lemmas for some list functions
haftmann
parents: 19597
diff changeset
   594
   of SOME i =>
07eeb832f28d introduced characters for code generator; some improved code lemmas for some list functions
haftmann
parents: 19597
diff changeset
   595
        trns
07eeb832f28d introduced characters for code generator; some improved code lemmas for some list functions
haftmann
parents: 19597
diff changeset
   596
        |> exprgen_type thy tabs ty
07eeb832f28d introduced characters for code generator; some improved code lemmas for some list functions
haftmann
parents: 19597
diff changeset
   597
        ||>> appgen_default thy tabs app
07eeb832f28d introduced characters for code generator; some improved code lemmas for some list functions
haftmann
parents: 19597
diff changeset
   598
        |-> (fn (_, e0) => pair (IChar (chr i, e0)))
07eeb832f28d introduced characters for code generator; some improved code lemmas for some list functions
haftmann
parents: 19597
diff changeset
   599
    | NONE =>
07eeb832f28d introduced characters for code generator; some improved code lemmas for some list functions
haftmann
parents: 19597
diff changeset
   600
        trns
07eeb832f28d introduced characters for code generator; some improved code lemmas for some list functions
haftmann
parents: 19597
diff changeset
   601
        |> appgen_default thy tabs app;
07eeb832f28d introduced characters for code generator; some improved code lemmas for some list functions
haftmann
parents: 19597
diff changeset
   602
20105
454f4be984b7 adaptions in codegen
haftmann
parents: 20076
diff changeset
   603
fun appgen_case dest_case_expr thy tabs (app as (c_ty, ts)) trns =
454f4be984b7 adaptions in codegen
haftmann
parents: 20076
diff changeset
   604
  let
454f4be984b7 adaptions in codegen
haftmann
parents: 20076
diff changeset
   605
    val SOME ([], ((st, sty), ds)) = dest_case_expr thy (list_comb (Const c_ty, ts));
454f4be984b7 adaptions in codegen
haftmann
parents: 20076
diff changeset
   606
    fun clausegen (dt, bt) trns =
454f4be984b7 adaptions in codegen
haftmann
parents: 20076
diff changeset
   607
      trns
454f4be984b7 adaptions in codegen
haftmann
parents: 20076
diff changeset
   608
      |> exprgen_term thy tabs dt
454f4be984b7 adaptions in codegen
haftmann
parents: 20076
diff changeset
   609
      ||>> exprgen_term thy tabs bt;
454f4be984b7 adaptions in codegen
haftmann
parents: 20076
diff changeset
   610
  in
454f4be984b7 adaptions in codegen
haftmann
parents: 20076
diff changeset
   611
    trns
454f4be984b7 adaptions in codegen
haftmann
parents: 20076
diff changeset
   612
    |> exprgen_term thy tabs st
454f4be984b7 adaptions in codegen
haftmann
parents: 20076
diff changeset
   613
    ||>> exprgen_type thy tabs sty
454f4be984b7 adaptions in codegen
haftmann
parents: 20076
diff changeset
   614
    ||>> fold_map clausegen ds
454f4be984b7 adaptions in codegen
haftmann
parents: 20076
diff changeset
   615
    ||>> appgen_default thy tabs app
454f4be984b7 adaptions in codegen
haftmann
parents: 20076
diff changeset
   616
    |-> (fn (((se, sty), ds), e0) => pair (ICase (((se, sty), ds), e0)))
454f4be984b7 adaptions in codegen
haftmann
parents: 20076
diff changeset
   617
  end;
454f4be984b7 adaptions in codegen
haftmann
parents: 20076
diff changeset
   618
454f4be984b7 adaptions in codegen
haftmann
parents: 20076
diff changeset
   619
fun appgen_let thy tabs (app as (_, [st, ct])) trns =
454f4be984b7 adaptions in codegen
haftmann
parents: 20076
diff changeset
   620
  trns
454f4be984b7 adaptions in codegen
haftmann
parents: 20076
diff changeset
   621
  |> exprgen_term thy tabs ct
454f4be984b7 adaptions in codegen
haftmann
parents: 20076
diff changeset
   622
  ||>> exprgen_term thy tabs st
454f4be984b7 adaptions in codegen
haftmann
parents: 20076
diff changeset
   623
  ||>> appgen_default thy tabs app
454f4be984b7 adaptions in codegen
haftmann
parents: 20076
diff changeset
   624
  |-> (fn (((v, ty) `|-> be, se), e0) =>
454f4be984b7 adaptions in codegen
haftmann
parents: 20076
diff changeset
   625
            pair (ICase (((se, ty), case be
454f4be984b7 adaptions in codegen
haftmann
parents: 20076
diff changeset
   626
              of ICase (((IVar w, _), ds), _) => if v = w then ds else [(IVar v, be)]
454f4be984b7 adaptions in codegen
haftmann
parents: 20076
diff changeset
   627
               | _ => [(IVar v, be)]
454f4be984b7 adaptions in codegen
haftmann
parents: 20076
diff changeset
   628
            ), e0))
454f4be984b7 adaptions in codegen
haftmann
parents: 20076
diff changeset
   629
        | (_, e0) => pair e0);
454f4be984b7 adaptions in codegen
haftmann
parents: 20076
diff changeset
   630
20386
d1cbe5aa6bf2 module restructuring
haftmann
parents: 20353
diff changeset
   631
fun appgen_wfrec thy (tabs as (_, thmtab)) ((c, ty), [_, tf, tx]) trns =
19038
62c5f7591a43 improved handling of iml abstractions
haftmann
parents: 19025
diff changeset
   632
  let
20386
d1cbe5aa6bf2 module restructuring
haftmann
parents: 20353
diff changeset
   633
    val ty_def = (op ---> o apfst tl o strip_type o Logic.unvarifyT o Sign.the_const_type thy) c;
19038
62c5f7591a43 improved handling of iml abstractions
haftmann
parents: 19025
diff changeset
   634
    val ty' = (op ---> o apfst tl o strip_type) ty;
20386
d1cbe5aa6bf2 module restructuring
haftmann
parents: 20353
diff changeset
   635
    val idf = idf_of_const thy thmtab (c, ty);
19038
62c5f7591a43 improved handling of iml abstractions
haftmann
parents: 19025
diff changeset
   636
  in
62c5f7591a43 improved handling of iml abstractions
haftmann
parents: 19025
diff changeset
   637
    trns
20386
d1cbe5aa6bf2 module restructuring
haftmann
parents: 20353
diff changeset
   638
    |> ensure_def ((K o fail) "no extraction for wfrec") false ("generating wfrec") idf
19136
00ade10f611d some refinements
haftmann
parents: 19111
diff changeset
   639
    |> exprgen_type thy tabs ty'
00ade10f611d some refinements
haftmann
parents: 19111
diff changeset
   640
    ||>> (fold_map o fold_map) (exprgen_classlookup thy tabs)
20386
d1cbe5aa6bf2 module restructuring
haftmann
parents: 20353
diff changeset
   641
           (sortlookups_const thy thmtab (c, ty))
19816
a8c8ed1c85e0 removed 'primitive definitions' added (non)strict generation, minor fixes
haftmann
parents: 19806
diff changeset
   642
    ||>> exprgen_type thy tabs ty_def
19136
00ade10f611d some refinements
haftmann
parents: 19111
diff changeset
   643
    ||>> exprgen_term thy tabs tf
00ade10f611d some refinements
haftmann
parents: 19111
diff changeset
   644
    ||>> exprgen_term thy tabs tx
19816
a8c8ed1c85e0 removed 'primitive definitions' added (non)strict generation, minor fixes
haftmann
parents: 19806
diff changeset
   645
    |-> (fn ((((_, ls), ty), tf), tx) => pair (IConst (idf, (ls, ty)) `$ tf `$ tx))
19038
62c5f7591a43 improved handling of iml abstractions
haftmann
parents: 19025
diff changeset
   646
  end;
62c5f7591a43 improved handling of iml abstractions
haftmann
parents: 19025
diff changeset
   647
18217
e0b08c9534ff added codegen package
haftmann
parents: 18169
diff changeset
   648
18516
4424e2bce9af slightly improved serialization
haftmann
parents: 18515
diff changeset
   649
4424e2bce9af slightly improved serialization
haftmann
parents: 18515
diff changeset
   650
(** theory interface **)
18217
e0b08c9534ff added codegen package
haftmann
parents: 18169
diff changeset
   651
20353
d73e49780ef2 code generator refinements
haftmann
parents: 20216
diff changeset
   652
fun mk_tabs thy targets cs =
20386
d1cbe5aa6bf2 module restructuring
haftmann
parents: 20353
diff changeset
   653
  ((true, targets), CodegenTheorems.mk_thmtab thy cs);
18217
e0b08c9534ff added codegen package
haftmann
parents: 18169
diff changeset
   654
18756
5eb3df798405 more general serializer
haftmann
parents: 18708
diff changeset
   655
fun get_serializer target =
5eb3df798405 more general serializer
haftmann
parents: 18708
diff changeset
   656
  case Symtab.lookup (!serializers) target
5eb3df798405 more general serializer
haftmann
parents: 18708
diff changeset
   657
   of SOME seri => seri
19008
14c1b2f5dda4 improved code generator devarification
haftmann
parents: 18963
diff changeset
   658
    | NONE => Scan.fail_with (fn _ => "unknown code target language: " ^ quote target) ();
18335
99baddf6b0d0 various improvements
haftmann
parents: 18330
diff changeset
   659
18516
4424e2bce9af slightly improved serialization
haftmann
parents: 18515
diff changeset
   660
fun map_module f =
20386
d1cbe5aa6bf2 module restructuring
haftmann
parents: 20353
diff changeset
   661
  map_codegen_data (fn (modl, gens, target_data) =>
d1cbe5aa6bf2 module restructuring
haftmann
parents: 20353
diff changeset
   662
    (f modl, gens, target_data));
18516
4424e2bce9af slightly improved serialization
haftmann
parents: 18515
diff changeset
   663
19884
a7be206d8655 improvements in code generator
haftmann
parents: 19816
diff changeset
   664
fun purge_defs NONE thy =
19341
3414c04fbc39 added definitional code generator module: codegen_theorems.ML
haftmann
parents: 19283
diff changeset
   665
      map_module (K CodegenThingol.empty_module) thy
20191
b43fd26e1aaa improvements for lazy code generation
haftmann
parents: 20183
diff changeset
   666
  | purge_defs (SOME []) thy =
b43fd26e1aaa improvements for lazy code generation
haftmann
parents: 20183
diff changeset
   667
      thy
19884
a7be206d8655 improvements in code generator
haftmann
parents: 19816
diff changeset
   668
  | purge_defs (SOME cs) thy =
20191
b43fd26e1aaa improvements for lazy code generation
haftmann
parents: 20183
diff changeset
   669
      map_module (K CodegenThingol.empty_module) thy;
b43fd26e1aaa improvements for lazy code generation
haftmann
parents: 20183
diff changeset
   670
      (*let
19816
a8c8ed1c85e0 removed 'primitive definitions' added (non)strict generation, minor fixes
haftmann
parents: 19806
diff changeset
   671
        val tabs = mk_tabs thy NONE;
19884
a7be206d8655 improvements in code generator
haftmann
parents: 19816
diff changeset
   672
        val idfs = map (idf_of_const' thy tabs) cs;
a7be206d8655 improvements in code generator
haftmann
parents: 19816
diff changeset
   673
        fun purge idfs modl =
a7be206d8655 improvements in code generator
haftmann
parents: 19816
diff changeset
   674
          CodegenThingol.purge_module (filter (can (get_def modl)) idfs) modl
19341
3414c04fbc39 added definitional code generator module: codegen_theorems.ML
haftmann
parents: 19283
diff changeset
   675
      in
19884
a7be206d8655 improvements in code generator
haftmann
parents: 19816
diff changeset
   676
        map_module (purge idfs) thy
20191
b43fd26e1aaa improvements for lazy code generation
haftmann
parents: 20183
diff changeset
   677
      end;*)
19341
3414c04fbc39 added definitional code generator module: codegen_theorems.ML
haftmann
parents: 19283
diff changeset
   678
20353
d73e49780ef2 code generator refinements
haftmann
parents: 20216
diff changeset
   679
fun expand_module targets cs init gen arg thy =
19597
8ced57ffc090 major refinement of codegen_theorems.ML
haftmann
parents: 19571
diff changeset
   680
  thy
8ced57ffc090 major refinement of codegen_theorems.ML
haftmann
parents: 19571
diff changeset
   681
  |> CodegenTheorems.notify_dirty
8ced57ffc090 major refinement of codegen_theorems.ML
haftmann
parents: 19571
diff changeset
   682
  |> `(#modl o CodegenData.get)
8ced57ffc090 major refinement of codegen_theorems.ML
haftmann
parents: 19571
diff changeset
   683
  |> (fn (modl, thy) =>
20353
d73e49780ef2 code generator refinements
haftmann
parents: 20216
diff changeset
   684
        (start_transact init (gen thy (mk_tabs thy targets cs) arg) modl, thy))
19597
8ced57ffc090 major refinement of codegen_theorems.ML
haftmann
parents: 19571
diff changeset
   685
  |-> (fn (x, modl) => map_module (K modl) #> pair x);
18516
4424e2bce9af slightly improved serialization
haftmann
parents: 18515
diff changeset
   686
20353
d73e49780ef2 code generator refinements
haftmann
parents: 20216
diff changeset
   687
fun consts_of t =
d73e49780ef2 code generator refinements
haftmann
parents: 20216
diff changeset
   688
  fold_aterms (fn Const c => cons c | _ => I) t [];
d73e49780ef2 code generator refinements
haftmann
parents: 20216
diff changeset
   689
20105
454f4be984b7 adaptions in codegen
haftmann
parents: 20076
diff changeset
   690
fun codegen_term t thy =
20353
d73e49780ef2 code generator refinements
haftmann
parents: 20216
diff changeset
   691
  let
d73e49780ef2 code generator refinements
haftmann
parents: 20216
diff changeset
   692
    val _ = Thm.cterm_of thy t;
d73e49780ef2 code generator refinements
haftmann
parents: 20216
diff changeset
   693
(*     val _ = writeln "STARTING GENERATION";  *)
d73e49780ef2 code generator refinements
haftmann
parents: 20216
diff changeset
   694
(*     val _ = (writeln o Sign.string_of_term thy) t;  *)
d73e49780ef2 code generator refinements
haftmann
parents: 20216
diff changeset
   695
  in
d73e49780ef2 code generator refinements
haftmann
parents: 20216
diff changeset
   696
    thy
d73e49780ef2 code generator refinements
haftmann
parents: 20216
diff changeset
   697
    |> expand_module (SOME [] (*(Symtab.keys (#target_data (CodegenData.get thy)))*)) (consts_of t) NONE exprgen_term t
d73e49780ef2 code generator refinements
haftmann
parents: 20216
diff changeset
   698
  end;
19136
00ade10f611d some refinements
haftmann
parents: 19111
diff changeset
   699
00ade10f611d some refinements
haftmann
parents: 19111
diff changeset
   700
val is_dtcon = has_nsp nsp_dtcon;
00ade10f611d some refinements
haftmann
parents: 19111
diff changeset
   701
00ade10f611d some refinements
haftmann
parents: 19111
diff changeset
   702
fun consts_of_idfs thy =
20386
d1cbe5aa6bf2 module restructuring
haftmann
parents: 20353
diff changeset
   703
  map (the o const_of_idf thy);
19150
1457d810b408 class package and codegen refinements
haftmann
parents: 19136
diff changeset
   704
20353
d73e49780ef2 code generator refinements
haftmann
parents: 20216
diff changeset
   705
fun idfs_of_consts thy cs =
20386
d1cbe5aa6bf2 module restructuring
haftmann
parents: 20353
diff changeset
   706
  map (idf_of_const thy (snd (mk_tabs thy NONE cs))) cs;
19150
1457d810b408 class package and codegen refinements
haftmann
parents: 19136
diff changeset
   707
19967
33da452f0abe slight refinements
haftmann
parents: 19956
diff changeset
   708
fun get_root_module thy =
33da452f0abe slight refinements
haftmann
parents: 19956
diff changeset
   709
  thy
33da452f0abe slight refinements
haftmann
parents: 19956
diff changeset
   710
  |> CodegenTheorems.notify_dirty
33da452f0abe slight refinements
haftmann
parents: 19956
diff changeset
   711
  |> `(#modl o CodegenData.get);
19042
630b8dd0b31a exported some interfaces useful for other code generator approaches
haftmann
parents: 19038
diff changeset
   712
20213
2b319e945905 added eval_term
haftmann
parents: 20194
diff changeset
   713
fun eval_term (ref_spec, t) thy =
2b319e945905 added eval_term
haftmann
parents: 20194
diff changeset
   714
  let
2b319e945905 added eval_term
haftmann
parents: 20194
diff changeset
   715
    val target_data =
2b319e945905 added eval_term
haftmann
parents: 20194
diff changeset
   716
      ((fn data => (the o Symtab.lookup data) "ml") o #target_data o CodegenData.get) thy;
20386
d1cbe5aa6bf2 module restructuring
haftmann
parents: 20353
diff changeset
   717
    val eval = CodegenSerializer.eval_term nsp_eval nsp_dtcon [[nsp_module], [nsp_class, nsp_tyco], [nsp_const, nsp_dtcon, nsp_class, nsp_mem, nsp_inst, nsp_instmem], [nsp_eval]]
20213
2b319e945905 added eval_term
haftmann
parents: 20194
diff changeset
   718
      ((Option.map fst oo Symtab.lookup) (#syntax_tyco target_data),
2b319e945905 added eval_term
haftmann
parents: 20194
diff changeset
   719
       (Option.map fst oo Symtab.lookup) (#syntax_const target_data))
2b319e945905 added eval_term
haftmann
parents: 20194
diff changeset
   720
      (Symtab.keys (#syntax_tyco target_data) @ Symtab.keys (#syntax_const target_data))
2b319e945905 added eval_term
haftmann
parents: 20194
diff changeset
   721
  in
2b319e945905 added eval_term
haftmann
parents: 20194
diff changeset
   722
    thy
2b319e945905 added eval_term
haftmann
parents: 20194
diff changeset
   723
    |> codegen_term t
2b319e945905 added eval_term
haftmann
parents: 20194
diff changeset
   724
    ||>> `(#modl o CodegenData.get)
2b319e945905 added eval_term
haftmann
parents: 20194
diff changeset
   725
    |-> (fn (t', modl) => `(fn _ => eval (ref_spec, t') modl))
2b319e945905 added eval_term
haftmann
parents: 20194
diff changeset
   726
  end;
2b319e945905 added eval_term
haftmann
parents: 20194
diff changeset
   727
19042
630b8dd0b31a exported some interfaces useful for other code generator approaches
haftmann
parents: 19038
diff changeset
   728
fun get_ml_fun_datatype thy resolv =
630b8dd0b31a exported some interfaces useful for other code generator approaches
haftmann
parents: 19038
diff changeset
   729
  let
19150
1457d810b408 class package and codegen refinements
haftmann
parents: 19136
diff changeset
   730
    val target_data =
19042
630b8dd0b31a exported some interfaces useful for other code generator approaches
haftmann
parents: 19038
diff changeset
   731
      ((fn data => (the o Symtab.lookup data) "ml") o #target_data o CodegenData.get) thy;
630b8dd0b31a exported some interfaces useful for other code generator approaches
haftmann
parents: 19038
diff changeset
   732
  in
20183
fd546b0c8a7c major simplifications for integers
haftmann
parents: 20175
diff changeset
   733
    CodegenSerializer.ml_fun_datatype nsp_dtcon
19042
630b8dd0b31a exported some interfaces useful for other code generator approaches
haftmann
parents: 19038
diff changeset
   734
      ((Option.map fst oo Symtab.lookup o #syntax_tyco) target_data,
630b8dd0b31a exported some interfaces useful for other code generator approaches
haftmann
parents: 19038
diff changeset
   735
      (Option.map fst oo Symtab.lookup o #syntax_const) target_data)
630b8dd0b31a exported some interfaces useful for other code generator approaches
haftmann
parents: 19038
diff changeset
   736
      resolv
630b8dd0b31a exported some interfaces useful for other code generator approaches
haftmann
parents: 19038
diff changeset
   737
  end;
18516
4424e2bce9af slightly improved serialization
haftmann
parents: 18515
diff changeset
   738
4424e2bce9af slightly improved serialization
haftmann
parents: 18515
diff changeset
   739
4424e2bce9af slightly improved serialization
haftmann
parents: 18515
diff changeset
   740
(** target languages **)
4424e2bce9af slightly improved serialization
haftmann
parents: 18515
diff changeset
   741
19816
a8c8ed1c85e0 removed 'primitive definitions' added (non)strict generation, minor fixes
haftmann
parents: 19806
diff changeset
   742
(* syntax *)
18516
4424e2bce9af slightly improved serialization
haftmann
parents: 18515
diff changeset
   743
18702
7dc7dcd63224 substantial improvements in code generator
haftmann
parents: 18517
diff changeset
   744
fun read_typ thy =
7dc7dcd63224 substantial improvements in code generator
haftmann
parents: 18517
diff changeset
   745
  Sign.read_typ (thy, K NONE);
7dc7dcd63224 substantial improvements in code generator
haftmann
parents: 18517
diff changeset
   746
20353
d73e49780ef2 code generator refinements
haftmann
parents: 20216
diff changeset
   747
fun read_quote get reader consts_of gen raw thy =
d73e49780ef2 code generator refinements
haftmann
parents: 20216
diff changeset
   748
  let
d73e49780ef2 code generator refinements
haftmann
parents: 20216
diff changeset
   749
    val it = reader thy raw;
d73e49780ef2 code generator refinements
haftmann
parents: 20216
diff changeset
   750
    val cs = consts_of it;
d73e49780ef2 code generator refinements
haftmann
parents: 20216
diff changeset
   751
  in
d73e49780ef2 code generator refinements
haftmann
parents: 20216
diff changeset
   752
    thy
d73e49780ef2 code generator refinements
haftmann
parents: 20216
diff changeset
   753
    |> expand_module (SOME (Symtab.keys (#target_data (CodegenData.get thy)))) cs ((SOME o get) thy)
d73e49780ef2 code generator refinements
haftmann
parents: 20216
diff changeset
   754
         (fn thy => fn tabs => gen thy tabs) [it]
d73e49780ef2 code generator refinements
haftmann
parents: 20216
diff changeset
   755
    |-> (fn [x] => pair x)
d73e49780ef2 code generator refinements
haftmann
parents: 20216
diff changeset
   756
  end;
18702
7dc7dcd63224 substantial improvements in code generator
haftmann
parents: 18517
diff changeset
   757
18865
31aed965135c minor cleanups
haftmann
parents: 18850
diff changeset
   758
fun gen_add_syntax_class prep_class class target pretty thy =
31aed965135c minor cleanups
haftmann
parents: 18850
diff changeset
   759
  thy
31aed965135c minor cleanups
haftmann
parents: 18850
diff changeset
   760
  |> map_codegen_data
20386
d1cbe5aa6bf2 module restructuring
haftmann
parents: 20353
diff changeset
   761
    (fn (modl, gens, target_data) =>
18865
31aed965135c minor cleanups
haftmann
parents: 18850
diff changeset
   762
       (modl, gens,
31aed965135c minor cleanups
haftmann
parents: 18850
diff changeset
   763
        target_data |> Symtab.map_entry target
31aed965135c minor cleanups
haftmann
parents: 18850
diff changeset
   764
          (map_target_data
31aed965135c minor cleanups
haftmann
parents: 18850
diff changeset
   765
            (fn (syntax_class, syntax_tyco, syntax_const) =>
31aed965135c minor cleanups
haftmann
parents: 18850
diff changeset
   766
             (syntax_class
20386
d1cbe5aa6bf2 module restructuring
haftmann
parents: 20353
diff changeset
   767
              |> Symtab.update (prep_class thy class, pretty), syntax_tyco, syntax_const)))));
18865
31aed965135c minor cleanups
haftmann
parents: 18850
diff changeset
   768
31aed965135c minor cleanups
haftmann
parents: 18850
diff changeset
   769
val add_syntax_class = gen_add_syntax_class Sign.intern_class;
31aed965135c minor cleanups
haftmann
parents: 18850
diff changeset
   770
18963
3adfc9dfb30a slight improvements in code generation
haftmann
parents: 18960
diff changeset
   771
fun parse_syntax_tyco raw_tyco =
18217
e0b08c9534ff added codegen package
haftmann
parents: 18169
diff changeset
   772
  let
19042
630b8dd0b31a exported some interfaces useful for other code generator approaches
haftmann
parents: 19038
diff changeset
   773
    fun prep_tyco thy raw_tyco =
630b8dd0b31a exported some interfaces useful for other code generator approaches
haftmann
parents: 19038
diff changeset
   774
      raw_tyco
18963
3adfc9dfb30a slight improvements in code generation
haftmann
parents: 18960
diff changeset
   775
      |> Sign.intern_type thy
20386
d1cbe5aa6bf2 module restructuring
haftmann
parents: 20353
diff changeset
   776
      |> idf_of_tyco thy;
19042
630b8dd0b31a exported some interfaces useful for other code generator approaches
haftmann
parents: 19038
diff changeset
   777
    fun no_args_tyco thy raw_tyco =
630b8dd0b31a exported some interfaces useful for other code generator approaches
haftmann
parents: 19038
diff changeset
   778
      AList.lookup (op =) ((NameSpace.dest_table o #types o Type.rep_tsig o Sign.tsig_of) thy)
630b8dd0b31a exported some interfaces useful for other code generator approaches
haftmann
parents: 19038
diff changeset
   779
        (Sign.intern_type thy raw_tyco)
630b8dd0b31a exported some interfaces useful for other code generator approaches
haftmann
parents: 19038
diff changeset
   780
      |> (fn SOME ((Type.LogicalType i), _) => i);
18963
3adfc9dfb30a slight improvements in code generation
haftmann
parents: 18960
diff changeset
   781
    fun mk reader target thy =
18702
7dc7dcd63224 substantial improvements in code generator
haftmann
parents: 18517
diff changeset
   782
      let
18756
5eb3df798405 more general serializer
haftmann
parents: 18708
diff changeset
   783
        val _ = get_serializer target;
18702
7dc7dcd63224 substantial improvements in code generator
haftmann
parents: 18517
diff changeset
   784
        val tyco = prep_tyco thy raw_tyco;
7dc7dcd63224 substantial improvements in code generator
haftmann
parents: 18517
diff changeset
   785
      in
7dc7dcd63224 substantial improvements in code generator
haftmann
parents: 18517
diff changeset
   786
        thy
7dc7dcd63224 substantial improvements in code generator
haftmann
parents: 18517
diff changeset
   787
        |> reader
7dc7dcd63224 substantial improvements in code generator
haftmann
parents: 18517
diff changeset
   788
        |-> (fn pretty => map_codegen_data
20386
d1cbe5aa6bf2 module restructuring
haftmann
parents: 20353
diff changeset
   789
          (fn (modl, gens, target_data) =>
18702
7dc7dcd63224 substantial improvements in code generator
haftmann
parents: 18517
diff changeset
   790
             (modl, gens,
7dc7dcd63224 substantial improvements in code generator
haftmann
parents: 18517
diff changeset
   791
              target_data |> Symtab.map_entry target
7dc7dcd63224 substantial improvements in code generator
haftmann
parents: 18517
diff changeset
   792
                (map_target_data
18865
31aed965135c minor cleanups
haftmann
parents: 18850
diff changeset
   793
                  (fn (syntax_class, syntax_tyco, syntax_const) =>
31aed965135c minor cleanups
haftmann
parents: 18850
diff changeset
   794
                   (syntax_class, syntax_tyco |> Symtab.update
18702
7dc7dcd63224 substantial improvements in code generator
haftmann
parents: 18517
diff changeset
   795
                      (tyco, (pretty, stamp ())),
20386
d1cbe5aa6bf2 module restructuring
haftmann
parents: 20353
diff changeset
   796
                    syntax_const))))))
18702
7dc7dcd63224 substantial improvements in code generator
haftmann
parents: 18517
diff changeset
   797
      end;
18217
e0b08c9534ff added codegen package
haftmann
parents: 18169
diff changeset
   798
  in
19042
630b8dd0b31a exported some interfaces useful for other code generator approaches
haftmann
parents: 19038
diff changeset
   799
    CodegenSerializer.parse_syntax (fn thy => no_args_tyco thy raw_tyco)
20353
d73e49780ef2 code generator refinements
haftmann
parents: 20216
diff changeset
   800
    (read_quote (fn thy => prep_tyco thy raw_tyco) read_typ (K [])
19816
a8c8ed1c85e0 removed 'primitive definitions' added (non)strict generation, minor fixes
haftmann
parents: 19806
diff changeset
   801
      (fn thy => fn tabs => fold_map (exprgen_type thy tabs)))
18702
7dc7dcd63224 substantial improvements in code generator
haftmann
parents: 18517
diff changeset
   802
    #-> (fn reader => pair (mk reader))
18217
e0b08c9534ff added codegen package
haftmann
parents: 18169
diff changeset
   803
  end;
e0b08c9534ff added codegen package
haftmann
parents: 18169
diff changeset
   804
18704
2c86ced392a8 substantial improvement in serialization handling
haftmann
parents: 18702
diff changeset
   805
fun add_pretty_syntax_const c target pretty =
2c86ced392a8 substantial improvement in serialization handling
haftmann
parents: 18702
diff changeset
   806
  map_codegen_data
20386
d1cbe5aa6bf2 module restructuring
haftmann
parents: 20353
diff changeset
   807
    (fn (modl, gens, target_data) =>
18704
2c86ced392a8 substantial improvement in serialization handling
haftmann
parents: 18702
diff changeset
   808
       (modl, gens,
2c86ced392a8 substantial improvement in serialization handling
haftmann
parents: 18702
diff changeset
   809
        target_data |> Symtab.map_entry target
2c86ced392a8 substantial improvement in serialization handling
haftmann
parents: 18702
diff changeset
   810
          (map_target_data
18865
31aed965135c minor cleanups
haftmann
parents: 18850
diff changeset
   811
            (fn (syntax_class, syntax_tyco, syntax_const) =>
31aed965135c minor cleanups
haftmann
parents: 18850
diff changeset
   812
             (syntax_class, syntax_tyco,
18704
2c86ced392a8 substantial improvement in serialization handling
haftmann
parents: 18702
diff changeset
   813
              syntax_const
2c86ced392a8 substantial improvement in serialization handling
haftmann
parents: 18702
diff changeset
   814
              |> Symtab.update
20386
d1cbe5aa6bf2 module restructuring
haftmann
parents: 20353
diff changeset
   815
                 (c, (pretty, stamp ())))))));
18704
2c86ced392a8 substantial improvement in serialization handling
haftmann
parents: 18702
diff changeset
   816
18963
3adfc9dfb30a slight improvements in code generation
haftmann
parents: 18960
diff changeset
   817
fun parse_syntax_const raw_const =
18217
e0b08c9534ff added codegen package
haftmann
parents: 18169
diff changeset
   818
  let
18963
3adfc9dfb30a slight improvements in code generation
haftmann
parents: 18960
diff changeset
   819
    fun prep_const thy raw_const =
20353
d73e49780ef2 code generator refinements
haftmann
parents: 20216
diff changeset
   820
      let
20386
d1cbe5aa6bf2 module restructuring
haftmann
parents: 20353
diff changeset
   821
        val c_ty = CodegenConsts.read_const_typ thy raw_const
d1cbe5aa6bf2 module restructuring
haftmann
parents: 20353
diff changeset
   822
      in idf_of_const thy (snd (mk_tabs thy NONE [c_ty])) c_ty end;
19042
630b8dd0b31a exported some interfaces useful for other code generator approaches
haftmann
parents: 19038
diff changeset
   823
    fun no_args_const thy raw_const =
20386
d1cbe5aa6bf2 module restructuring
haftmann
parents: 20353
diff changeset
   824
      (length o fst o strip_type o snd o CodegenConsts.read_const_typ thy) raw_const;
18963
3adfc9dfb30a slight improvements in code generation
haftmann
parents: 18960
diff changeset
   825
    fun mk reader target thy =
18702
7dc7dcd63224 substantial improvements in code generator
haftmann
parents: 18517
diff changeset
   826
      let
18756
5eb3df798405 more general serializer
haftmann
parents: 18708
diff changeset
   827
        val _ = get_serializer target;
18963
3adfc9dfb30a slight improvements in code generation
haftmann
parents: 18960
diff changeset
   828
        val c = prep_const thy raw_const;
18702
7dc7dcd63224 substantial improvements in code generator
haftmann
parents: 18517
diff changeset
   829
      in
7dc7dcd63224 substantial improvements in code generator
haftmann
parents: 18517
diff changeset
   830
        thy
7dc7dcd63224 substantial improvements in code generator
haftmann
parents: 18517
diff changeset
   831
        |> reader
18704
2c86ced392a8 substantial improvement in serialization handling
haftmann
parents: 18702
diff changeset
   832
        |-> (fn pretty => add_pretty_syntax_const c target pretty)
18702
7dc7dcd63224 substantial improvements in code generator
haftmann
parents: 18517
diff changeset
   833
      end;
18217
e0b08c9534ff added codegen package
haftmann
parents: 18169
diff changeset
   834
  in
19042
630b8dd0b31a exported some interfaces useful for other code generator approaches
haftmann
parents: 19038
diff changeset
   835
    CodegenSerializer.parse_syntax (fn thy => no_args_const thy raw_const)
20353
d73e49780ef2 code generator refinements
haftmann
parents: 20216
diff changeset
   836
      (read_quote (fn thy => prep_const thy raw_const) Sign.read_term consts_of
19816
a8c8ed1c85e0 removed 'primitive definitions' added (non)strict generation, minor fixes
haftmann
parents: 19806
diff changeset
   837
      (fn thy => fn tabs => fold_map (exprgen_term thy tabs)))
18702
7dc7dcd63224 substantial improvements in code generator
haftmann
parents: 18517
diff changeset
   838
    #-> (fn reader => pair (mk reader))
18217
e0b08c9534ff added codegen package
haftmann
parents: 18169
diff changeset
   839
  end;
e0b08c9534ff added codegen package
haftmann
parents: 18169
diff changeset
   840
18704
2c86ced392a8 substantial improvement in serialization handling
haftmann
parents: 18702
diff changeset
   841
fun add_pretty_list raw_nil raw_cons (target, seri) thy =
2c86ced392a8 substantial improvement in serialization handling
haftmann
parents: 18702
diff changeset
   842
  let
18756
5eb3df798405 more general serializer
haftmann
parents: 18708
diff changeset
   843
    val _ = get_serializer target;
20353
d73e49780ef2 code generator refinements
haftmann
parents: 20216
diff changeset
   844
    fun prep_const raw =
18704
2c86ced392a8 substantial improvement in serialization handling
haftmann
parents: 18702
diff changeset
   845
      let
20353
d73e49780ef2 code generator refinements
haftmann
parents: 20216
diff changeset
   846
        val c = Sign.intern_const thy raw
d73e49780ef2 code generator refinements
haftmann
parents: 20216
diff changeset
   847
      in (c, Sign.the_const_type thy c) end;
d73e49780ef2 code generator refinements
haftmann
parents: 20216
diff changeset
   848
    val nil' = prep_const raw_nil;
d73e49780ef2 code generator refinements
haftmann
parents: 20216
diff changeset
   849
    val cons' = prep_const raw_cons;
d73e49780ef2 code generator refinements
haftmann
parents: 20216
diff changeset
   850
    val tabs = mk_tabs thy NONE [nil', cons'];
d73e49780ef2 code generator refinements
haftmann
parents: 20216
diff changeset
   851
    fun mk_const c_ty =
20386
d1cbe5aa6bf2 module restructuring
haftmann
parents: 20353
diff changeset
   852
      idf_of_const thy (snd tabs) c_ty;
20353
d73e49780ef2 code generator refinements
haftmann
parents: 20216
diff changeset
   853
    val nil'' = mk_const nil';
d73e49780ef2 code generator refinements
haftmann
parents: 20216
diff changeset
   854
    val cons'' = mk_const cons';
d73e49780ef2 code generator refinements
haftmann
parents: 20216
diff changeset
   855
    val pr = CodegenSerializer.pretty_list nil'' cons'' seri;
18704
2c86ced392a8 substantial improvement in serialization handling
haftmann
parents: 18702
diff changeset
   856
  in
2c86ced392a8 substantial improvement in serialization handling
haftmann
parents: 18702
diff changeset
   857
    thy
20353
d73e49780ef2 code generator refinements
haftmann
parents: 20216
diff changeset
   858
    |> add_pretty_syntax_const cons'' target pr
18704
2c86ced392a8 substantial improvement in serialization handling
haftmann
parents: 18702
diff changeset
   859
  end;
2c86ced392a8 substantial improvement in serialization handling
haftmann
parents: 18702
diff changeset
   860
18217
e0b08c9534ff added codegen package
haftmann
parents: 18169
diff changeset
   861
18516
4424e2bce9af slightly improved serialization
haftmann
parents: 18515
diff changeset
   862
19884
a7be206d8655 improvements in code generator
haftmann
parents: 19816
diff changeset
   863
(** code basis change notifications **)
a7be206d8655 improvements in code generator
haftmann
parents: 19816
diff changeset
   864
a7be206d8655 improvements in code generator
haftmann
parents: 19816
diff changeset
   865
val _ = Context.add_setup (CodegenTheorems.add_notify purge_defs);
a7be206d8655 improvements in code generator
haftmann
parents: 19816
diff changeset
   866
a7be206d8655 improvements in code generator
haftmann
parents: 19816
diff changeset
   867
a7be206d8655 improvements in code generator
haftmann
parents: 19816
diff changeset
   868
18756
5eb3df798405 more general serializer
haftmann
parents: 18708
diff changeset
   869
(** toplevel interface **)
5eb3df798405 more general serializer
haftmann
parents: 18708
diff changeset
   870
5eb3df798405 more general serializer
haftmann
parents: 18708
diff changeset
   871
local
19150
1457d810b408 class package and codegen refinements
haftmann
parents: 19136
diff changeset
   872
19884
a7be206d8655 improvements in code generator
haftmann
parents: 19816
diff changeset
   873
fun generate_code targets (SOME raw_consts) thy =
19816
a8c8ed1c85e0 removed 'primitive definitions' added (non)strict generation, minor fixes
haftmann
parents: 19806
diff changeset
   874
      let
20386
d1cbe5aa6bf2 module restructuring
haftmann
parents: 20353
diff changeset
   875
        val consts = map (CodegenConsts.read_const_typ thy) raw_consts;
19884
a7be206d8655 improvements in code generator
haftmann
parents: 19816
diff changeset
   876
        val _ = case targets of SOME targets => (map get_serializer targets; ()) | _ => ();
18756
5eb3df798405 more general serializer
haftmann
parents: 18708
diff changeset
   877
      in
5eb3df798405 more general serializer
haftmann
parents: 18708
diff changeset
   878
        thy
20353
d73e49780ef2 code generator refinements
haftmann
parents: 20216
diff changeset
   879
        |> expand_module targets consts NONE (fold_map oo ensure_def_const) consts
18756
5eb3df798405 more general serializer
haftmann
parents: 18708
diff changeset
   880
        |-> (fn cs => pair (SOME cs))
5eb3df798405 more general serializer
haftmann
parents: 18708
diff changeset
   881
      end
19816
a8c8ed1c85e0 removed 'primitive definitions' added (non)strict generation, minor fixes
haftmann
parents: 19806
diff changeset
   882
  | generate_code _ NONE thy =
18756
5eb3df798405 more general serializer
haftmann
parents: 18708
diff changeset
   883
      (NONE, thy);
5eb3df798405 more general serializer
haftmann
parents: 18708
diff changeset
   884
5eb3df798405 more general serializer
haftmann
parents: 18708
diff changeset
   885
fun serialize_code target seri raw_consts thy =
18217
e0b08c9534ff added codegen package
haftmann
parents: 18169
diff changeset
   886
  let
18756
5eb3df798405 more general serializer
haftmann
parents: 18708
diff changeset
   887
    fun serialize cs thy =
18702
7dc7dcd63224 substantial improvements in code generator
haftmann
parents: 18517
diff changeset
   888
      let
18756
5eb3df798405 more general serializer
haftmann
parents: 18708
diff changeset
   889
        val module = (#modl o CodegenData.get) thy;
18702
7dc7dcd63224 substantial improvements in code generator
haftmann
parents: 18517
diff changeset
   890
        val target_data =
7dc7dcd63224 substantial improvements in code generator
haftmann
parents: 18517
diff changeset
   891
          thy
7dc7dcd63224 substantial improvements in code generator
haftmann
parents: 18517
diff changeset
   892
          |> CodegenData.get
7dc7dcd63224 substantial improvements in code generator
haftmann
parents: 18517
diff changeset
   893
          |> #target_data
7dc7dcd63224 substantial improvements in code generator
haftmann
parents: 18517
diff changeset
   894
          |> (fn data => (the oo Symtab.lookup) data target);
20216
f30b73385060 added eval_term
haftmann
parents: 20213
diff changeset
   895
        val s_class = #syntax_class target_data
f30b73385060 added eval_term
haftmann
parents: 20213
diff changeset
   896
        val s_tyco = #syntax_tyco target_data
f30b73385060 added eval_term
haftmann
parents: 20213
diff changeset
   897
        val s_const = #syntax_const target_data
19884
a7be206d8655 improvements in code generator
haftmann
parents: 19816
diff changeset
   898
      in
20216
f30b73385060 added eval_term
haftmann
parents: 20213
diff changeset
   899
        (seri (
f30b73385060 added eval_term
haftmann
parents: 20213
diff changeset
   900
          Symtab.lookup s_class,
f30b73385060 added eval_term
haftmann
parents: 20213
diff changeset
   901
          (Option.map fst oo Symtab.lookup) s_tyco,
f30b73385060 added eval_term
haftmann
parents: 20213
diff changeset
   902
          (Option.map fst oo Symtab.lookup) s_const
f30b73385060 added eval_term
haftmann
parents: 20213
diff changeset
   903
        ) (Symtab.keys s_class @ Symtab.keys s_tyco @ Symtab.keys s_const, cs) module : unit; thy)
19884
a7be206d8655 improvements in code generator
haftmann
parents: 19816
diff changeset
   904
      end;
18217
e0b08c9534ff added codegen package
haftmann
parents: 18169
diff changeset
   905
  in
e0b08c9534ff added codegen package
haftmann
parents: 18169
diff changeset
   906
    thy
19884
a7be206d8655 improvements in code generator
haftmann
parents: 19816
diff changeset
   907
    |> generate_code (SOME [target]) raw_consts
18756
5eb3df798405 more general serializer
haftmann
parents: 18708
diff changeset
   908
    |-> (fn cs => serialize cs)
18217
e0b08c9534ff added codegen package
haftmann
parents: 18169
diff changeset
   909
  end;
e0b08c9534ff added codegen package
haftmann
parents: 18169
diff changeset
   910
19341
3414c04fbc39 added definitional code generator module: codegen_theorems.ML
haftmann
parents: 19283
diff changeset
   911
fun purge_consts raw_ts thy =
3414c04fbc39 added definitional code generator module: codegen_theorems.ML
haftmann
parents: 19283
diff changeset
   912
  let
20386
d1cbe5aa6bf2 module restructuring
haftmann
parents: 20353
diff changeset
   913
    val cs = map (CodegenConsts.read_const_typ thy) raw_ts;
19341
3414c04fbc39 added definitional code generator module: codegen_theorems.ML
haftmann
parents: 19283
diff changeset
   914
  in fold CodegenTheorems.purge_defs cs thy end;
3414c04fbc39 added definitional code generator module: codegen_theorems.ML
haftmann
parents: 19283
diff changeset
   915
18217
e0b08c9534ff added codegen package
haftmann
parents: 18169
diff changeset
   916
structure P = OuterParse
e0b08c9534ff added codegen package
haftmann
parents: 18169
diff changeset
   917
and K = OuterKeyword
e0b08c9534ff added codegen package
haftmann
parents: 18169
diff changeset
   918
e0b08c9534ff added codegen package
haftmann
parents: 18169
diff changeset
   919
in
e0b08c9534ff added codegen package
haftmann
parents: 18169
diff changeset
   920
18850
92ef83e5eaea various improvements
haftmann
parents: 18756
diff changeset
   921
val (generateK, serializeK,
19341
3414c04fbc39 added definitional code generator module: codegen_theorems.ML
haftmann
parents: 19283
diff changeset
   922
     syntax_classK, syntax_tycoK, syntax_constK,
20386
d1cbe5aa6bf2 module restructuring
haftmann
parents: 20353
diff changeset
   923
     purgeK) =
18850
92ef83e5eaea various improvements
haftmann
parents: 18756
diff changeset
   924
  ("code_generate", "code_serialize",
19884
a7be206d8655 improvements in code generator
haftmann
parents: 19816
diff changeset
   925
   "code_classapp", "code_typapp", "code_constapp",
20386
d1cbe5aa6bf2 module restructuring
haftmann
parents: 20353
diff changeset
   926
   "code_purge");
18335
99baddf6b0d0 various improvements
haftmann
parents: 18330
diff changeset
   927
18217
e0b08c9534ff added codegen package
haftmann
parents: 18169
diff changeset
   928
val generateP =
18282
98431741bda3 added haskell serializer
haftmann
parents: 18247
diff changeset
   929
  OuterSyntax.command generateK "generate executable code for constants" K.thy_decl (
19884
a7be206d8655 improvements in code generator
haftmann
parents: 19816
diff changeset
   930
    (Scan.option (P.$$$ "(" |-- P.list1 P.name --| P.$$$ ")")
a7be206d8655 improvements in code generator
haftmann
parents: 19816
diff changeset
   931
    >> (fn SOME ["-"] => SOME [] | ts => ts))
19816
a8c8ed1c85e0 removed 'primitive definitions' added (non)strict generation, minor fixes
haftmann
parents: 19806
diff changeset
   932
    -- Scan.repeat1 P.term
19884
a7be206d8655 improvements in code generator
haftmann
parents: 19816
diff changeset
   933
    >> (fn (targets, raw_consts) =>
a7be206d8655 improvements in code generator
haftmann
parents: 19816
diff changeset
   934
          Toplevel.theory (generate_code targets (SOME raw_consts) #> snd))
18217
e0b08c9534ff added codegen package
haftmann
parents: 18169
diff changeset
   935
  );
e0b08c9534ff added codegen package
haftmann
parents: 18169
diff changeset
   936
e0b08c9534ff added codegen package
haftmann
parents: 18169
diff changeset
   937
val serializeP =
18282
98431741bda3 added haskell serializer
haftmann
parents: 18247
diff changeset
   938
  OuterSyntax.command serializeK "serialize executable code for constants" K.thy_decl (
18217
e0b08c9534ff added codegen package
haftmann
parents: 18169
diff changeset
   939
    P.name
19136
00ade10f611d some refinements
haftmann
parents: 19111
diff changeset
   940
    -- Scan.option (Scan.repeat1 P.term)
18756
5eb3df798405 more general serializer
haftmann
parents: 18708
diff changeset
   941
    #-> (fn (target, raw_consts) =>
18850
92ef83e5eaea various improvements
haftmann
parents: 18756
diff changeset
   942
          P.$$$ "("
92ef83e5eaea various improvements
haftmann
parents: 18756
diff changeset
   943
          |-- get_serializer target
92ef83e5eaea various improvements
haftmann
parents: 18756
diff changeset
   944
          --| P.$$$ ")"
18756
5eb3df798405 more general serializer
haftmann
parents: 18708
diff changeset
   945
          >> (fn seri =>
5eb3df798405 more general serializer
haftmann
parents: 18708
diff changeset
   946
            Toplevel.theory (serialize_code target seri raw_consts)
5eb3df798405 more general serializer
haftmann
parents: 18708
diff changeset
   947
          ))
18217
e0b08c9534ff added codegen package
haftmann
parents: 18169
diff changeset
   948
  );
e0b08c9534ff added codegen package
haftmann
parents: 18169
diff changeset
   949
18865
31aed965135c minor cleanups
haftmann
parents: 18850
diff changeset
   950
val syntax_classP =
19884
a7be206d8655 improvements in code generator
haftmann
parents: 19816
diff changeset
   951
  OuterSyntax.command syntax_classK "define code syntax for class" K.thy_decl (
18865
31aed965135c minor cleanups
haftmann
parents: 18850
diff changeset
   952
    Scan.repeat1 (
31aed965135c minor cleanups
haftmann
parents: 18850
diff changeset
   953
      P.xname
31aed965135c minor cleanups
haftmann
parents: 18850
diff changeset
   954
      -- Scan.repeat1 (
31aed965135c minor cleanups
haftmann
parents: 18850
diff changeset
   955
           P.name -- P.string
31aed965135c minor cleanups
haftmann
parents: 18850
diff changeset
   956
         )
31aed965135c minor cleanups
haftmann
parents: 18850
diff changeset
   957
    )
31aed965135c minor cleanups
haftmann
parents: 18850
diff changeset
   958
    >> (Toplevel.theory oo fold) (fn (raw_class, syns) =>
31aed965135c minor cleanups
haftmann
parents: 18850
diff changeset
   959
          fold (fn (target, p) => add_syntax_class raw_class target p) syns)
31aed965135c minor cleanups
haftmann
parents: 18850
diff changeset
   960
  );
31aed965135c minor cleanups
haftmann
parents: 18850
diff changeset
   961
18217
e0b08c9534ff added codegen package
haftmann
parents: 18169
diff changeset
   962
val syntax_tycoP =
e0b08c9534ff added codegen package
haftmann
parents: 18169
diff changeset
   963
  OuterSyntax.command syntax_tycoK "define code syntax for type constructor" K.thy_decl (
18702
7dc7dcd63224 substantial improvements in code generator
haftmann
parents: 18517
diff changeset
   964
    Scan.repeat1 (
7dc7dcd63224 substantial improvements in code generator
haftmann
parents: 18517
diff changeset
   965
      P.xname
18963
3adfc9dfb30a slight improvements in code generation
haftmann
parents: 18960
diff changeset
   966
      #-> (fn raw_tyco => Scan.repeat1 (
3adfc9dfb30a slight improvements in code generation
haftmann
parents: 18960
diff changeset
   967
             P.name -- parse_syntax_tyco raw_tyco
3adfc9dfb30a slight improvements in code generation
haftmann
parents: 18960
diff changeset
   968
          ))
18702
7dc7dcd63224 substantial improvements in code generator
haftmann
parents: 18517
diff changeset
   969
    )
18963
3adfc9dfb30a slight improvements in code generation
haftmann
parents: 18960
diff changeset
   970
    >> (Toplevel.theory oo fold o fold)
3adfc9dfb30a slight improvements in code generation
haftmann
parents: 18960
diff changeset
   971
          (fn (target, modifier) => modifier target)
18217
e0b08c9534ff added codegen package
haftmann
parents: 18169
diff changeset
   972
  );
e0b08c9534ff added codegen package
haftmann
parents: 18169
diff changeset
   973
e0b08c9534ff added codegen package
haftmann
parents: 18169
diff changeset
   974
val syntax_constP =
e0b08c9534ff added codegen package
haftmann
parents: 18169
diff changeset
   975
  OuterSyntax.command syntax_constK "define code syntax for constant" K.thy_decl (
18702
7dc7dcd63224 substantial improvements in code generator
haftmann
parents: 18517
diff changeset
   976
    Scan.repeat1 (
19136
00ade10f611d some refinements
haftmann
parents: 19111
diff changeset
   977
      P.term
18963
3adfc9dfb30a slight improvements in code generation
haftmann
parents: 18960
diff changeset
   978
      #-> (fn raw_const => Scan.repeat1 (
3adfc9dfb30a slight improvements in code generation
haftmann
parents: 18960
diff changeset
   979
             P.name -- parse_syntax_const raw_const
3adfc9dfb30a slight improvements in code generation
haftmann
parents: 18960
diff changeset
   980
          ))
18702
7dc7dcd63224 substantial improvements in code generator
haftmann
parents: 18517
diff changeset
   981
    )
19008
14c1b2f5dda4 improved code generator devarification
haftmann
parents: 18963
diff changeset
   982
    >> (Toplevel.theory oo fold o fold)
18963
3adfc9dfb30a slight improvements in code generation
haftmann
parents: 18960
diff changeset
   983
          (fn (target, modifier) => modifier target)
18217
e0b08c9534ff added codegen package
haftmann
parents: 18169
diff changeset
   984
  );
e0b08c9534ff added codegen package
haftmann
parents: 18169
diff changeset
   985
19341
3414c04fbc39 added definitional code generator module: codegen_theorems.ML
haftmann
parents: 19283
diff changeset
   986
val purgeP =
20175
0a8ca32f6e64 class package and codegen refinements
haftmann
parents: 20105
diff changeset
   987
  OuterSyntax.command purgeK "purge all incrementally generated code" K.thy_decl
0a8ca32f6e64 class package and codegen refinements
haftmann
parents: 20105
diff changeset
   988
    (Scan.succeed (Toplevel.theory purge_code));
18516
4424e2bce9af slightly improved serialization
haftmann
parents: 18515
diff changeset
   989
19884
a7be206d8655 improvements in code generator
haftmann
parents: 19816
diff changeset
   990
val _ = OuterSyntax.add_parsers [generateP, serializeP,
a7be206d8655 improvements in code generator
haftmann
parents: 19816
diff changeset
   991
  syntax_classP, syntax_tycoP, syntax_constP,
20386
d1cbe5aa6bf2 module restructuring
haftmann
parents: 20353
diff changeset
   992
  purgeP];
18217
e0b08c9534ff added codegen package
haftmann
parents: 18169
diff changeset
   993
e0b08c9534ff added codegen package
haftmann
parents: 18169
diff changeset
   994
end; (* local *)
e0b08c9534ff added codegen package
haftmann
parents: 18169
diff changeset
   995
e0b08c9534ff added codegen package
haftmann
parents: 18169
diff changeset
   996
end; (* struct *)