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