src/Pure/Tools/codegen_package.ML
author wenzelm
Thu Jan 19 21:22:08 2006 +0100 (2006-01-19 ago)
changeset 18708 4b3dadb4fe33
parent 18704 2c86ced392a8
child 18756 5eb3df798405
permissions -rw-r--r--
setup: theory -> theory;
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@18282
     9
(*NOTE: for simplifying developement, this package contains
haftmann@18169
    10
some stuff which will finally be moved upwards to HOL*)
haftmann@18169
    11
haftmann@18169
    12
signature CODEGEN_PACKAGE =
haftmann@18169
    13
sig
haftmann@18454
    14
  type auxtab;
haftmann@18702
    15
  type eqextr = theory -> auxtab
haftmann@18702
    16
    -> (string * typ) -> (thm list * typ) option;
haftmann@18217
    17
  type defgen;
haftmann@18702
    18
  type appgen = theory -> auxtab
haftmann@18702
    19
    -> (string * typ) * term list -> CodegenThingol.transact -> CodegenThingol.iexpr * CodegenThingol.transact;
haftmann@18702
    20
haftmann@18516
    21
  val add_appconst: string * ((int * int) * appgen) -> theory -> theory;
haftmann@18517
    22
  val add_appconst_i: xstring * ((int * int) * appgen) -> theory -> theory;
haftmann@18702
    23
  val add_eqextr: string * eqextr -> theory -> theory;
haftmann@18217
    24
  val add_defgen: string * defgen -> theory -> theory;
haftmann@18517
    25
  val add_prim_class: xstring -> string list -> (string * string)
haftmann@18517
    26
    -> theory -> theory;
haftmann@18517
    27
  val add_prim_tyco: xstring -> string list -> (string * string)
haftmann@18517
    28
    -> theory -> theory;
haftmann@18517
    29
  val add_prim_const: xstring * string option -> string list -> (string * string)
haftmann@18517
    30
    -> theory -> theory;
haftmann@18517
    31
  val add_prim_i: string -> string list -> (string * Pretty.T)
haftmann@18517
    32
    -> theory -> theory;
haftmann@18704
    33
  val add_pretty_list: string -> string -> string * (int * string)
haftmann@18704
    34
    -> theory -> theory;
haftmann@18217
    35
  val add_alias: string * string -> theory -> theory;
haftmann@18217
    36
  val set_is_datatype: (theory -> string -> bool) -> theory -> theory;
haftmann@18455
    37
  val set_get_all_datatype_cons : (theory -> (string * string) list)
haftmann@18454
    38
    -> theory -> theory;
haftmann@18702
    39
  val set_int_tyco: string -> theory -> theory;
haftmann@18217
    40
haftmann@18516
    41
  val exprgen_type: theory -> auxtab
haftmann@18217
    42
    -> typ -> CodegenThingol.transact -> CodegenThingol.itype * CodegenThingol.transact;
haftmann@18516
    43
  val exprgen_term: theory -> auxtab
haftmann@18217
    44
    -> term -> CodegenThingol.transact -> CodegenThingol.iexpr * CodegenThingol.transact;
haftmann@18702
    45
  val appgen_default: appgen;
haftmann@18217
    46
haftmann@18335
    47
  val appgen_let: (int -> term -> term list * term)
haftmann@18335
    48
    -> appgen;
haftmann@18335
    49
  val appgen_split: (int -> term -> term list * term)
haftmann@18335
    50
    -> appgen;
haftmann@18702
    51
  val appgen_number_of: (term -> term) -> (term -> IntInf.int) -> string -> string
haftmann@18335
    52
    -> appgen;
haftmann@18702
    53
  val add_case_const: (theory -> string -> (string * int) list option) -> xstring
haftmann@18517
    54
    -> theory -> theory;
haftmann@18702
    55
  val add_case_const_i: (theory -> string -> (string * int) list option) -> string
haftmann@18517
    56
    -> theory -> theory;
haftmann@18380
    57
  val defgen_datatype: (theory -> string -> ((string * sort) list * string list) option)
haftmann@18335
    58
    -> (theory -> string * string -> typ list option)
haftmann@18217
    59
    -> defgen;
haftmann@18217
    60
haftmann@18247
    61
  val print_codegen_generated: theory -> unit;
haftmann@18454
    62
  val rename_inconsistent: theory -> theory;
haftmann@18517
    63
  val ensure_datatype_case_consts: (theory -> string list)
haftmann@18517
    64
    -> (theory -> string -> (string * int) list option)
haftmann@18517
    65
    -> theory -> theory;
haftmann@18515
    66
haftmann@18515
    67
  (*debugging purpose only*)
haftmann@18454
    68
  structure InstNameMangler: NAME_MANGLER;
haftmann@18454
    69
  structure ConstNameMangler: NAME_MANGLER;
haftmann@18454
    70
  structure DatatypeconsNameMangler: NAME_MANGLER;
haftmann@18231
    71
  structure CodegenData: THEORY_DATA;
haftmann@18454
    72
  val mk_tabs: theory -> auxtab;
haftmann@18454
    73
  val alias_get: theory -> string -> string;
haftmann@18515
    74
  val idf_of_name: theory -> string -> string -> string;
haftmann@18515
    75
  val idf_of_const: theory -> auxtab -> string * typ -> string;
haftmann@18169
    76
end;
haftmann@18169
    77
haftmann@18217
    78
structure CodegenPackage : CODEGEN_PACKAGE =
haftmann@18169
    79
struct
haftmann@18169
    80
haftmann@18385
    81
open CodegenThingolOp;
haftmann@18385
    82
infix 8 `%%;
haftmann@18385
    83
infixr 6 `->;
haftmann@18385
    84
infixr 6 `-->;
haftmann@18385
    85
infix 4 `$;
haftmann@18385
    86
infix 4 `$$;
haftmann@18385
    87
infixr 5 `|->;
haftmann@18385
    88
infixr 5 `|-->;
haftmann@18217
    89
haftmann@18217
    90
(* auxiliary *)
haftmann@18217
    91
haftmann@18454
    92
fun devarify_type ty = (fst o Type.freeze_thaw_type) ty;
haftmann@18335
    93
fun devarify_term t = (fst o Type.freeze_thaw) t;
haftmann@18454
    94
haftmann@18454
    95
val is_number = is_some o Int.fromString;
haftmann@18217
    96
haftmann@18702
    97
fun merge_opt _ (x1, NONE) = x1
haftmann@18702
    98
  | merge_opt _ (NONE, x2) = x2
haftmann@18702
    99
  | merge_opt eq (SOME x1, SOME x2) =
haftmann@18702
   100
      if eq (x1, x2) then SOME x1 else error ("incompatible options during merge");
haftmann@18217
   101
haftmann@18217
   102
haftmann@18702
   103
(* shallow name spaces *)
haftmann@18217
   104
haftmann@18217
   105
val nsp_class = "class";
haftmann@18454
   106
val nsp_tyco = "tyco";
haftmann@18217
   107
val nsp_const = "const";
haftmann@18454
   108
val nsp_overl = "overl";
haftmann@18454
   109
val nsp_dtcon = "dtcon";
haftmann@18217
   110
val nsp_mem = "mem";
haftmann@18217
   111
val nsp_inst = "inst";
haftmann@18217
   112
haftmann@18217
   113
haftmann@18702
   114
(* code generator basics *)
haftmann@18454
   115
haftmann@18454
   116
structure InstNameMangler = NameManglerFun (
haftmann@18454
   117
  type ctxt = theory;
haftmann@18454
   118
  type src = string * (class * string);
haftmann@18454
   119
  val ord = prod_ord string_ord (prod_ord string_ord string_ord);
haftmann@18454
   120
  fun mk thy ((thyname, (cls, tyco)), i) =
haftmann@18454
   121
    NameSpace.base cls ^ "_" ^ NameSpace.base tyco ^ implode (replicate i "'")
haftmann@18454
   122
    |> NameSpace.append thyname;
haftmann@18454
   123
  fun is_valid _ _ = true;
haftmann@18454
   124
  fun maybe_unique _ _ = NONE;
haftmann@18454
   125
  fun re_mangle _ dst = error ("no such instance: " ^ quote dst);
haftmann@18454
   126
);
haftmann@18454
   127
haftmann@18454
   128
structure ConstNameMangler = NameManglerFun (
haftmann@18454
   129
  type ctxt = theory;
haftmann@18454
   130
  type src = string * (typ * typ);
haftmann@18454
   131
  val ord = prod_ord string_ord (prod_ord Term.typ_ord Term.typ_ord);
haftmann@18454
   132
  fun mk thy ((c, (ty_decl, ty)), i) =
haftmann@18454
   133
    let
haftmann@18454
   134
      fun mangle (Type (tyco, tys)) =
haftmann@18454
   135
            NameSpace.base tyco :: Library.flat (List.mapPartial mangle tys) |> SOME
haftmann@18454
   136
        | mangle _ =
haftmann@18454
   137
            NONE
haftmann@18454
   138
    in
haftmann@18454
   139
      Vartab.empty
haftmann@18454
   140
      |> Sign.typ_match thy (ty_decl, ty)
haftmann@18454
   141
      |> map (snd o snd) o Vartab.dest
haftmann@18454
   142
      |> List.mapPartial mangle
haftmann@18454
   143
      |> Library.flat
haftmann@18454
   144
      |> null ? K ["x"]
haftmann@18454
   145
      |> cons c
haftmann@18454
   146
      |> space_implode "_"
haftmann@18454
   147
      |> curry (op ^ o swap) ((implode oo replicate) i "'")
haftmann@18454
   148
    end;
haftmann@18454
   149
  fun is_valid _ _ = true;
haftmann@18454
   150
  fun maybe_unique _ _ = NONE;
haftmann@18454
   151
  fun re_mangle _ dst = error ("no such constant: " ^ quote dst);
haftmann@18454
   152
);
haftmann@18454
   153
haftmann@18454
   154
structure DatatypeconsNameMangler = NameManglerFun (
haftmann@18454
   155
  type ctxt = theory;
haftmann@18454
   156
  type src = string * string;
haftmann@18454
   157
  val ord = prod_ord string_ord string_ord;
haftmann@18702
   158
  fun mk thy ((co, dtco), i) =
haftmann@18454
   159
        let
haftmann@18454
   160
          fun basename 0 = NameSpace.base co
haftmann@18455
   161
            | basename 1 = NameSpace.base dtco ^ "_" ^ NameSpace.base co
haftmann@18454
   162
            | basename i = NameSpace.base dtco ^ "_" ^ NameSpace.base co ^ "_" ^ (implode oo replicate) (i-1) "'";
haftmann@18454
   163
          fun strip_dtco name =
haftmann@18454
   164
            case (rev o NameSpace.unpack) name
haftmann@18454
   165
             of x1::x2::xs =>
haftmann@18454
   166
                  if x2 = NameSpace.base dtco
haftmann@18454
   167
                  then NameSpace.pack (x1::xs)
haftmann@18454
   168
                  else name
haftmann@18454
   169
              | _ => name;
haftmann@18454
   170
        in
haftmann@18454
   171
          NameSpace.append (NameSpace.drop_base dtco) (basename i)
haftmann@18454
   172
          |> strip_dtco
haftmann@18454
   173
        end;
haftmann@18454
   174
  fun is_valid _ _ = true;
haftmann@18454
   175
  fun maybe_unique _ _ = NONE;
haftmann@18454
   176
  fun re_mangle _ dst = error ("no such datatype constructor: " ^ quote dst);
haftmann@18454
   177
);
haftmann@18454
   178
haftmann@18702
   179
type auxtab = ((typ * thm) list Symtab.table * string Symtab.table)
haftmann@18454
   180
  * (InstNameMangler.T * ((typ * typ list) Symtab.table * ConstNameMangler.T) * DatatypeconsNameMangler.T);
haftmann@18702
   181
type eqextr = theory -> auxtab
haftmann@18702
   182
  -> (string * typ) -> (thm list * typ) option;
haftmann@18454
   183
type defgen = theory -> auxtab -> gen_defgen;
haftmann@18702
   184
type appgen = theory -> auxtab -> (string * typ) * term list -> transact -> iexpr * transact;
haftmann@18217
   185
haftmann@18702
   186
val serializers = ref (
haftmann@18702
   187
  Symtab.empty
haftmann@18702
   188
  |> Symtab.update (
haftmann@18702
   189
       #ml CodegenSerializer.serializers
haftmann@18702
   190
       |> apsnd (fn seri => seri
haftmann@18702
   191
            (nsp_dtcon, nsp_class, "")
haftmann@18702
   192
            [[nsp_class, nsp_tyco], [nsp_const, nsp_overl, nsp_dtcon, nsp_mem, nsp_inst]]
haftmann@18702
   193
          )
haftmann@18702
   194
     )
haftmann@18702
   195
  |> Symtab.update (
haftmann@18702
   196
       #haskell CodegenSerializer.serializers
haftmann@18702
   197
       |> apsnd (fn seri => seri
haftmann@18702
   198
            nsp_dtcon
haftmann@18702
   199
            [[nsp_class], [nsp_tyco], [nsp_const, nsp_overl, nsp_mem], [nsp_dtcon], [nsp_inst]]
haftmann@18702
   200
          )
haftmann@18702
   201
     )
haftmann@18702
   202
);
haftmann@18217
   203
haftmann@18217
   204
haftmann@18454
   205
(* theory data for code generator *)
haftmann@18217
   206
haftmann@18217
   207
type gens = {
haftmann@18516
   208
  appconst: ((int * int) * (appgen * stamp)) Symtab.table,
haftmann@18702
   209
  eqextrs: (string * (eqextr * stamp)) list,
haftmann@18217
   210
  defgens: (string * (defgen * stamp)) list
haftmann@18217
   211
};
haftmann@18217
   212
haftmann@18702
   213
fun map_gens f { appconst, eqextrs, defgens } =
haftmann@18217
   214
  let
haftmann@18702
   215
    val (appconst, eqextrs, defgens) =
haftmann@18702
   216
      f (appconst, eqextrs, defgens)
haftmann@18702
   217
  in { appconst = appconst, eqextrs = eqextrs, defgens = defgens } : gens end;
haftmann@18217
   218
haftmann@18217
   219
fun merge_gens
haftmann@18702
   220
  ({ appconst = appconst1 , eqextrs = eqextrs1, defgens = defgens1 },
haftmann@18702
   221
   { appconst = appconst2 , eqextrs = eqextrs2, defgens = defgens2 }) =
haftmann@18516
   222
  { appconst = Symtab.merge
haftmann@18516
   223
      (fn ((bounds1, (_, stamp1)), (bounds2, (_, stamp2))) => bounds1 = bounds2 andalso stamp1 = stamp2)
haftmann@18516
   224
      (appconst1, appconst2),
haftmann@18702
   225
    eqextrs = AList.merge (op =) (eq_snd (op =)) (eqextrs1, eqextrs2),
haftmann@18702
   226
    defgens = AList.merge (op =) (eq_snd (op =)) (defgens1, defgens2)
haftmann@18702
   227
  } : gens;
haftmann@18217
   228
haftmann@18217
   229
type logic_data = {
haftmann@18217
   230
  is_datatype: ((theory -> string -> bool) * stamp) option,
haftmann@18455
   231
  get_all_datatype_cons: ((theory -> (string * string) list) * stamp) option,
haftmann@18217
   232
  alias: string Symtab.table * string Symtab.table
haftmann@18217
   233
};
haftmann@18217
   234
haftmann@18454
   235
fun map_logic_data f { is_datatype, get_all_datatype_cons, alias } =
haftmann@18217
   236
  let
haftmann@18454
   237
    val ((is_datatype, get_all_datatype_cons), alias) =
haftmann@18454
   238
      f ((is_datatype, get_all_datatype_cons), alias)
haftmann@18702
   239
  in { is_datatype = is_datatype, get_all_datatype_cons = get_all_datatype_cons,
haftmann@18702
   240
    alias = alias } : logic_data end;
haftmann@18217
   241
haftmann@18217
   242
fun merge_logic_data
haftmann@18702
   243
  ({ is_datatype = is_datatype1, get_all_datatype_cons = get_all_datatype_cons1,
haftmann@18702
   244
       alias = alias1 },
haftmann@18702
   245
   { is_datatype = is_datatype2, get_all_datatype_cons = get_all_datatype_cons2,
haftmann@18702
   246
       alias = alias2 }) =
haftmann@18217
   247
  let
haftmann@18217
   248
  in
haftmann@18217
   249
    { is_datatype = merge_opt (eq_snd (op =)) (is_datatype1, is_datatype2),
haftmann@18454
   250
      get_all_datatype_cons = merge_opt (eq_snd (op =)) (get_all_datatype_cons1, get_all_datatype_cons2),
haftmann@18217
   251
      alias = (Symtab.merge (op =) (fst alias1, fst alias2),
haftmann@18304
   252
               Symtab.merge (op =) (snd alias1, snd alias2)) } : logic_data
haftmann@18217
   253
  end;
haftmann@18217
   254
haftmann@18702
   255
type target_data = {
haftmann@18516
   256
  syntax_tyco: (itype CodegenSerializer.pretty_syntax * stamp) Symtab.table,
haftmann@18516
   257
  syntax_const: (iexpr CodegenSerializer.pretty_syntax * stamp) Symtab.table
haftmann@18217
   258
};
haftmann@18217
   259
haftmann@18702
   260
fun map_target_data f { syntax_tyco, syntax_const } =
haftmann@18217
   261
  let
haftmann@18517
   262
    val (syntax_tyco, syntax_const) =
haftmann@18517
   263
      f (syntax_tyco, syntax_const)
haftmann@18702
   264
  in { syntax_tyco = syntax_tyco, syntax_const = syntax_const } : target_data
haftmann@18454
   265
  end;
haftmann@18217
   266
haftmann@18702
   267
fun merge_target_data
haftmann@18702
   268
  ({ syntax_tyco = syntax_tyco1, syntax_const = syntax_const1 },
haftmann@18702
   269
   { syntax_tyco = syntax_tyco2, syntax_const = syntax_const2 }) =
haftmann@18702
   270
  { syntax_tyco = Symtab.merge (eq_snd (op =)) (syntax_tyco1, syntax_tyco2),
haftmann@18702
   271
    syntax_const = Symtab.merge (eq_snd (op =)) (syntax_const1, syntax_const2) } : target_data;
haftmann@18217
   272
haftmann@18217
   273
structure CodegenData = TheoryDataFun
haftmann@18217
   274
(struct
haftmann@18217
   275
  val name = "Pure/codegen_package";
haftmann@18217
   276
  type T = {
haftmann@18217
   277
    modl: module,
haftmann@18217
   278
    gens: gens,
haftmann@18217
   279
    logic_data: logic_data,
haftmann@18702
   280
    target_data: target_data Symtab.table
haftmann@18217
   281
  };
haftmann@18217
   282
  val empty = {
haftmann@18217
   283
    modl = empty_module,
haftmann@18702
   284
    gens = { appconst = Symtab.empty, eqextrs = [], defgens = [] } : gens,
haftmann@18454
   285
    logic_data = { is_datatype = NONE, get_all_datatype_cons = NONE,
haftmann@18454
   286
      alias = (Symtab.empty, Symtab.empty) } : logic_data,
haftmann@18702
   287
    target_data =
haftmann@18217
   288
      Symtab.empty
haftmann@18702
   289
      |> Symtab.fold (fn (target, _) =>
haftmann@18702
   290
           Symtab.update (target, { syntax_tyco = Symtab.empty, syntax_const = Symtab.empty })
haftmann@18702
   291
         ) (! serializers)
haftmann@18217
   292
  } : T;
haftmann@18217
   293
  val copy = I;
haftmann@18217
   294
  val extend = I;
haftmann@18217
   295
  fun merge _ (
haftmann@18702
   296
    { modl = modl1, gens = gens1,
haftmann@18702
   297
      target_data = target_data1, logic_data = logic_data1 },
haftmann@18702
   298
    { modl = modl2, gens = gens2,
haftmann@18702
   299
      target_data = target_data2, logic_data = logic_data2 }
haftmann@18217
   300
  ) = {
haftmann@18217
   301
    modl = merge_module (modl1, modl2),
haftmann@18217
   302
    gens = merge_gens (gens1, gens2),
haftmann@18217
   303
    logic_data = merge_logic_data (logic_data1, logic_data2),
haftmann@18702
   304
    target_data = Symtab.join (K (merge_target_data #> SOME))
haftmann@18702
   305
      (target_data1, target_data2)
haftmann@18217
   306
  };
wenzelm@18708
   307
  fun print _ _ = ();
haftmann@18217
   308
end);
haftmann@18217
   309
wenzelm@18708
   310
val _ = Context.add_setup CodegenData.init;
wenzelm@18708
   311
haftmann@18217
   312
fun map_codegen_data f thy =
haftmann@18217
   313
  case CodegenData.get thy
haftmann@18702
   314
   of { modl, gens, target_data, logic_data } =>
haftmann@18702
   315
      let val (modl, gens, target_data, logic_data) =
haftmann@18702
   316
        f (modl, gens, target_data, logic_data)
haftmann@18702
   317
      in CodegenData.put { modl = modl, gens = gens,
haftmann@18702
   318
           target_data = target_data, logic_data = logic_data } thy end;
haftmann@18217
   319
haftmann@18517
   320
fun print_codegen_generated thy =
haftmann@18517
   321
  let
haftmann@18517
   322
    val module = (#modl o CodegenData.get) thy;
haftmann@18517
   323
  in
haftmann@18517
   324
    (writeln o Pretty.output o Pretty.chunks) [pretty_module module, pretty_deps module]
haftmann@18517
   325
  end;
haftmann@18217
   326
haftmann@18516
   327
fun gen_add_appconst prep_const (raw_c, (bounds, ag)) thy =
haftmann@18516
   328
  let
haftmann@18516
   329
    val c = prep_const thy raw_c;
haftmann@18516
   330
  in map_codegen_data
haftmann@18702
   331
    (fn (modl, gens, target_data, logic_data) =>
haftmann@18217
   332
       (modl,
haftmann@18217
   333
        gens |> map_gens
haftmann@18702
   334
          (fn (appconst, eqextrs, defgens) =>
haftmann@18516
   335
            (appconst
haftmann@18516
   336
             |> Symtab.update (c, (bounds, (ag, stamp ()))),
haftmann@18702
   337
             eqextrs, defgens)), target_data, logic_data)) thy
haftmann@18516
   338
  end;
haftmann@18217
   339
haftmann@18516
   340
val add_appconst = gen_add_appconst Sign.intern_const;
haftmann@18516
   341
val add_appconst_i = gen_add_appconst (K I);
haftmann@18217
   342
haftmann@18217
   343
fun add_defgen (name, dg) =
haftmann@18217
   344
  map_codegen_data
haftmann@18702
   345
    (fn (modl, gens, target_data, logic_data) =>
haftmann@18217
   346
       (modl,
haftmann@18217
   347
        gens |> map_gens
haftmann@18702
   348
          (fn (appconst, eqextrs, defgens) =>
haftmann@18702
   349
            (appconst, eqextrs, defgens
haftmann@18335
   350
             |> Output.update_warn (op =) ("overwriting existing definition definition generator " ^ name) (name, (dg, stamp ())))),
haftmann@18702
   351
             target_data, logic_data));
haftmann@18217
   352
haftmann@18454
   353
fun get_defgens thy tabs =
haftmann@18454
   354
  (map (apsnd (fn (dg, _) => dg thy tabs)) o #defgens o #gens o CodegenData.get) thy;
haftmann@18217
   355
haftmann@18702
   356
fun add_eqextr (name, eqx) =
haftmann@18217
   357
  map_codegen_data
haftmann@18702
   358
    (fn (modl, gens, target_data, logic_data) =>
haftmann@18702
   359
       (modl,
haftmann@18702
   360
        gens |> map_gens
haftmann@18702
   361
          (fn (appconst, eqextrs, defgens) =>
haftmann@18702
   362
            (appconst, eqextrs
haftmann@18702
   363
             |> Output.update_warn (op =) ("overwriting existing equation extractor " ^ name) (name, (eqx, stamp ())),
haftmann@18702
   364
             defgens)),
haftmann@18702
   365
             target_data, logic_data));
haftmann@18217
   366
haftmann@18702
   367
fun get_eqextrs thy tabs =
haftmann@18702
   368
  (map (fn (_, (eqx, _)) => eqx thy tabs) o #eqextrs o #gens o CodegenData.get) thy;
haftmann@18454
   369
haftmann@18454
   370
fun is_datatype thy =
haftmann@18454
   371
  case (#is_datatype o #logic_data o CodegenData.get) thy
haftmann@18454
   372
   of NONE => K false
haftmann@18454
   373
    | SOME (f, _) => f thy;
haftmann@18454
   374
haftmann@18454
   375
fun get_all_datatype_cons thy =
haftmann@18454
   376
  case (#get_all_datatype_cons o #logic_data o CodegenData.get) thy
haftmann@18454
   377
   of NONE => []
haftmann@18454
   378
    | SOME (f, _) => f thy;
haftmann@18217
   379
haftmann@18217
   380
fun add_alias (src, dst) =
haftmann@18217
   381
  map_codegen_data
haftmann@18702
   382
    (fn (modl, gens, target_data, logic_data) =>
haftmann@18702
   383
       (modl, gens, target_data,
haftmann@18217
   384
        logic_data |> map_logic_data
haftmann@18217
   385
          (apsnd (fn (tab, tab_rev) =>
haftmann@18217
   386
            (tab |> Symtab.update (src, dst),
haftmann@18217
   387
             tab_rev |> Symtab.update (dst, src))))));
haftmann@18217
   388
haftmann@18217
   389
haftmann@18454
   390
(* name handling *)
haftmann@18217
   391
haftmann@18454
   392
val alias_get = perhaps o Symtab.lookup o fst o #alias o #logic_data o CodegenData.get;
haftmann@18454
   393
val alias_rev = perhaps o Symtab.lookup o snd o #alias o #logic_data o CodegenData.get;
haftmann@18217
   394
haftmann@18454
   395
fun add_nsp shallow name =
haftmann@18454
   396
  name
haftmann@18454
   397
  |> NameSpace.unpack
haftmann@18454
   398
  |> split_last
haftmann@18454
   399
  |> apsnd (single #> cons shallow)
haftmann@18454
   400
  |> (op @)
haftmann@18454
   401
  |> NameSpace.pack;
haftmann@18702
   402
haftmann@18454
   403
fun dest_nsp nsp idf =
haftmann@18217
   404
  let
haftmann@18217
   405
    val idf' = NameSpace.unpack idf;
haftmann@18217
   406
    val (idf'', idf_base) = split_last idf';
haftmann@18217
   407
    val (modl, shallow) = split_last idf'';
haftmann@18217
   408
  in
haftmann@18217
   409
    if nsp = shallow
haftmann@18454
   410
    then (SOME o NameSpace.pack) (modl @ [idf_base])
haftmann@18217
   411
    else NONE
haftmann@18217
   412
  end;
haftmann@18217
   413
haftmann@18454
   414
fun idf_of_name thy shallow name =
haftmann@18702
   415
  name
haftmann@18702
   416
  |> alias_get thy
haftmann@18702
   417
  |> add_nsp shallow;
haftmann@18702
   418
haftmann@18454
   419
fun name_of_idf thy shallow idf =
haftmann@18454
   420
  idf
haftmann@18454
   421
  |> dest_nsp shallow
haftmann@18454
   422
  |> Option.map (alias_rev thy);
haftmann@18217
   423
haftmann@18702
   424
fun set_is_datatype f =
haftmann@18702
   425
  map_codegen_data
haftmann@18702
   426
    (fn (modl, gens, target_data, logic_data) =>
haftmann@18702
   427
       (modl, gens, target_data,
haftmann@18702
   428
        logic_data
haftmann@18702
   429
        |> map_logic_data (apfst (fn (is_datatype, get_all_datatype_cons)
haftmann@18702
   430
             => (SOME (f, stamp ()), get_all_datatype_cons)))));
haftmann@18702
   431
haftmann@18702
   432
fun set_get_all_datatype_cons f =
haftmann@18702
   433
  map_codegen_data
haftmann@18702
   434
    (fn (modl, gens, target_data, logic_data) =>
haftmann@18702
   435
       (modl, gens, target_data,
haftmann@18702
   436
        logic_data
haftmann@18702
   437
        |> map_logic_data ((apfst (fn (is_datatype, get_all_datatype_cons)
haftmann@18702
   438
             => (is_datatype, SOME (f, stamp ())))))));
haftmann@18702
   439
haftmann@18702
   440
fun set_int_tyco tyco thy =
haftmann@18702
   441
  (serializers := (
haftmann@18702
   442
    ! serializers
haftmann@18702
   443
    |> Symtab.update (
haftmann@18702
   444
         #ml CodegenSerializer.serializers
haftmann@18702
   445
         |> apsnd (fn seri => seri
haftmann@18702
   446
              (nsp_dtcon, nsp_class, idf_of_name thy nsp_tyco tyco)
haftmann@18702
   447
              [[nsp_class, nsp_tyco], [nsp_const, nsp_overl, nsp_dtcon, nsp_mem, nsp_inst]]
haftmann@18702
   448
            )
haftmann@18702
   449
       )
haftmann@18702
   450
    ); thy);
haftmann@18702
   451
haftmann@18516
   452
haftmann@18454
   453
(* code generator instantiation *)
haftmann@18217
   454
haftmann@18454
   455
fun ensure_def_class thy tabs cls trns =
haftmann@18454
   456
  let
haftmann@18454
   457
    val cls' = idf_of_name thy nsp_class cls;
haftmann@18454
   458
  in
haftmann@18454
   459
    trns
haftmann@18454
   460
    |> debug 4 (fn _ => "generating class " ^ quote cls)
haftmann@18454
   461
    |> gen_ensure_def (get_defgens thy tabs) ("generating class " ^ quote cls) cls'
haftmann@18454
   462
    |> pair cls'
haftmann@18454
   463
  end;
haftmann@18217
   464
haftmann@18454
   465
fun ensure_def_inst thy (tabs as (_, (insttab, _, _))) (cls, tyco) trns =
haftmann@18454
   466
  let
haftmann@18702
   467
    val thyname = (the o AList.lookup (op =) (ClassPackage.the_instances thy cls)) tyco;
haftmann@18454
   468
    val inst = idf_of_name thy nsp_inst (InstNameMangler.get thy insttab (thyname, (cls, tyco)));
haftmann@18454
   469
  in
haftmann@18454
   470
    trns
haftmann@18454
   471
    |> debug 4 (fn _ => "generating instance " ^ quote cls ^ " / " ^ quote tyco)
haftmann@18454
   472
    |> gen_ensure_def (get_defgens thy tabs) ("generating instance " ^ quote cls ^ " / " ^ quote tyco) inst
haftmann@18454
   473
    |> pair inst
haftmann@18454
   474
  end;
haftmann@18335
   475
haftmann@18454
   476
fun ensure_def_tyco thy tabs tyco trns =
haftmann@18454
   477
  let
haftmann@18454
   478
    val tyco' = idf_of_name thy nsp_tyco tyco;
haftmann@18702
   479
  in
haftmann@18702
   480
    trns
haftmann@18702
   481
    |> debug 4 (fn _ => "generating type constructor " ^ quote tyco)
haftmann@18702
   482
    |> gen_ensure_def (get_defgens thy tabs) ("generating type constructor " ^ quote tyco) tyco'
haftmann@18702
   483
    |> pair tyco'
haftmann@18454
   484
  end;
haftmann@18454
   485
haftmann@18454
   486
fun idf_of_const thy (tabs as ((_, clsmemtab), (_, (overltab1, overltab2), dtcontab))) (c, ty) =
haftmann@18454
   487
  let
haftmann@18515
   488
    fun get_overloaded (c, ty) =
haftmann@18515
   489
      case Symtab.lookup overltab1 c
haftmann@18515
   490
       of SOME (ty_decl, tys) =>
haftmann@18515
   491
            (case find_first (curry (Sign.typ_instance thy) ty) tys
haftmann@18515
   492
             of SOME ty' => ConstNameMangler.get thy overltab2
haftmann@18515
   493
                  (idf_of_name thy nsp_overl c, (ty_decl, ty')) |> SOME
haftmann@18515
   494
              | _ => NONE)
haftmann@18515
   495
        | _ => NONE
haftmann@18515
   496
    fun get_datatypecons (c, ty) =
haftmann@18515
   497
      case (snd o strip_type) ty
haftmann@18515
   498
       of Type (tyco, _) =>
haftmann@18515
   499
            try (DatatypeconsNameMangler.get thy dtcontab) (c, tyco)
haftmann@18515
   500
        | _ => NONE;
haftmann@18702
   501
  in case get_datatypecons (c, ty)
haftmann@18702
   502
   of SOME c' => idf_of_name thy nsp_dtcon c'
haftmann@18702
   503
    | NONE => case get_overloaded (c, ty)
haftmann@18515
   504
   of SOME idf => idf
haftmann@18515
   505
    | NONE => case Symtab.lookup clsmemtab c
haftmann@18515
   506
   of SOME _ => idf_of_name thy nsp_mem c
haftmann@18515
   507
    | NONE => idf_of_name thy nsp_const c
haftmann@18515
   508
  end;
haftmann@18217
   509
haftmann@18454
   510
fun recconst_of_idf thy (_, (_, (_, overltab2), _)) idf =
haftmann@18454
   511
  case name_of_idf thy nsp_const idf
haftmann@18702
   512
   of SOME c => SOME (c, Sign.the_const_type thy c)
haftmann@18454
   513
    | NONE => (
haftmann@18454
   514
        case dest_nsp nsp_overl idf
haftmann@18454
   515
         of SOME _ =>
haftmann@18454
   516
              idf
haftmann@18454
   517
              |> ConstNameMangler.rev thy overltab2
haftmann@18454
   518
              |> apfst (the o name_of_idf thy nsp_overl)
haftmann@18454
   519
              |> apsnd snd
haftmann@18454
   520
              |> SOME
haftmann@18454
   521
          | NONE => NONE
haftmann@18454
   522
      );
haftmann@18454
   523
haftmann@18454
   524
fun ensure_def_const thy (tabs as ((_, clsmemtab), (_, overltab, dtcontab))) (c, ty) trns =
haftmann@18454
   525
  let
haftmann@18454
   526
    val c' = idf_of_const thy tabs (c, ty);
haftmann@18702
   527
  in
haftmann@18702
   528
    trns
haftmann@18702
   529
    |> debug 4 (fn _ => "generating constant " ^ quote c)
haftmann@18702
   530
    |> gen_ensure_def (get_defgens thy tabs) ("generating constant " ^ quote c) c'
haftmann@18702
   531
    |> pair c'
haftmann@18454
   532
  end;
haftmann@18217
   533
haftmann@18702
   534
(* fun ensure_def_eq thy tabs (dtco, (eqpred, arity)) trns =
haftmann@18454
   535
  let
haftmann@18454
   536
    val name_dtco = (the ooo name_of_idf) thy nsp_tyco dtco;
haftmann@18454
   537
    val idf_eqinst = idf_of_name thy nsp_eq_inst name_dtco;
haftmann@18454
   538
    val idf_eqpred = idf_of_name thy nsp_eq_pred name_dtco;
haftmann@18515
   539
    val inst_sortlookup = map (fn (v, _) => [ClassPackage.Lookup ([], (v, 0))]) arity;
haftmann@18454
   540
    fun mk_eq_pred _ trns =
haftmann@18454
   541
      trns
haftmann@18702
   542
      |> succeed (eqpred)
haftmann@18454
   543
    fun mk_eq_inst _ trns =
haftmann@18454
   544
      trns
haftmann@18454
   545
      |> gen_ensure_def [("eqpred", mk_eq_pred)] ("generating equality predicate for " ^ quote dtco) idf_eqpred
haftmann@18702
   546
      |> succeed (Classinst ((class_eq, (dtco, arity)), ([], [(fun_eq, (idf_eqpred, inst_sortlookup))])));
haftmann@18454
   547
  in
haftmann@18454
   548
    trns
haftmann@18454
   549
    |> gen_ensure_def [("eqinst", mk_eq_inst)] ("generating equality instance for " ^ quote dtco) idf_eqinst
haftmann@18702
   550
  end; *)
haftmann@18454
   551
haftmann@18516
   552
haftmann@18516
   553
(* expression generators *)
haftmann@18516
   554
haftmann@18702
   555
fun exprgen_tyvar_sort thy tabs (v, sort) trns =
haftmann@18516
   556
  trns
haftmann@18516
   557
  |> fold_map (ensure_def_class thy tabs) (ClassPackage.syntactic_sort_of thy sort)
haftmann@18702
   558
  |-> (fn sort => pair (unprefix "'" v, sort));
haftmann@18516
   559
haftmann@18516
   560
fun exprgen_type thy tabs (TVar _) trns =
haftmann@18516
   561
      error "TVar encountered during code generation"
haftmann@18702
   562
  | exprgen_type thy tabs (TFree v_s) trns =
haftmann@18516
   563
      trns
haftmann@18702
   564
      |> exprgen_tyvar_sort thy tabs v_s
haftmann@18702
   565
      |-> (fn v_s => pair (IVarT v_s))
haftmann@18516
   566
  | exprgen_type thy tabs (Type ("fun", [t1, t2])) trns =
haftmann@18516
   567
      trns
haftmann@18516
   568
      |> exprgen_type thy tabs t1
haftmann@18516
   569
      ||>> exprgen_type thy tabs t2
haftmann@18516
   570
      |-> (fn (t1', t2') => pair (t1' `-> t2'))
haftmann@18516
   571
  | exprgen_type thy tabs (Type (tyco, tys)) trns =
haftmann@18516
   572
      trns
haftmann@18516
   573
      |> ensure_def_tyco thy tabs tyco
haftmann@18516
   574
      ||>> fold_map (exprgen_type thy tabs) tys
haftmann@18516
   575
      |-> (fn (tyco, tys) => pair (tyco `%% tys));
haftmann@18516
   576
haftmann@18517
   577
fun mk_lookup thy tabs (ClassPackage.Instance (inst as (cls, tyco), ls)) trns =
haftmann@18517
   578
      trns
haftmann@18517
   579
      |> ensure_def_class thy tabs cls
haftmann@18517
   580
      ||>> ensure_def_inst thy tabs inst
haftmann@18517
   581
      ||>> (fold_map o fold_map) (mk_lookup thy tabs) ls
haftmann@18517
   582
      |-> (fn ((cls, i), ls) => pair (ClassPackage.Instance ((cls, i), ls)))
haftmann@18517
   583
  | mk_lookup thy tabs (ClassPackage.Lookup (clss, (v, i))) trns =
haftmann@18516
   584
      trns
haftmann@18517
   585
      |> fold_map (ensure_def_class thy tabs) clss
haftmann@18517
   586
      |-> (fn clss => pair (ClassPackage.Lookup (clss, (v |> unprefix "'", i))));
haftmann@18517
   587
haftmann@18702
   588
fun appgen_default thy tabs ((c, ty), ts) trns =
haftmann@18702
   589
  trns
haftmann@18702
   590
  |> ensure_def_const thy tabs (c, ty)
haftmann@18702
   591
  ||>> (fold_map o fold_map) (mk_lookup thy tabs)
haftmann@18702
   592
    (ClassPackage.extract_sortlookup thy (c, ty))
haftmann@18702
   593
  ||>> exprgen_type thy tabs ty
haftmann@18702
   594
  ||>> fold_map (exprgen_term thy tabs) ts
haftmann@18702
   595
  |-> (fn (((c, ls), ty), es) =>
haftmann@18702
   596
         pair (Library.foldl IInst ((IConst (c, ty)), ls) `$$ es))
haftmann@18702
   597
and appgen thy tabs ((f, ty), ts) trns =
haftmann@18517
   598
  case Symtab.lookup ((#appconst o #gens o CodegenData.get) thy) f
haftmann@18517
   599
   of SOME ((imin, imax), (ag, _)) =>
haftmann@18702
   600
        if length ts < imin then
haftmann@18517
   601
          let
haftmann@18517
   602
            val d = imin - length ts;
haftmann@18517
   603
            val vs = Term.invent_names (add_term_names (Const (f, ty), [])) "x" d;
haftmann@18517
   604
            val tys = Library.take (d, ((fst o strip_type) ty));
haftmann@18517
   605
          in
haftmann@18517
   606
            trns
haftmann@18517
   607
            |> debug 10 (fn _ => "eta-expanding")
haftmann@18517
   608
            |> fold_map (exprgen_type thy tabs) tys
haftmann@18702
   609
            ||>> ag thy tabs ((f, ty), ts @ map2 (curry Free) vs tys)
haftmann@18517
   610
            |-> (fn (tys, e) => pair ((vs ~~ tys) `|--> e))
haftmann@18517
   611
          end
haftmann@18517
   612
        else if length ts > imax then
haftmann@18517
   613
          trns
haftmann@18517
   614
          |> debug 10 (fn _ => "splitting arguments (" ^ string_of_int imax ^ ", " ^ string_of_int (length ts) ^ ")")
haftmann@18702
   615
          |> ag thy tabs ((f, ty), Library.take (imax, ts))
haftmann@18517
   616
          ||>> fold_map (exprgen_term thy tabs) (Library.drop (imax, ts))
haftmann@18517
   617
          |-> (fn es => pair (mk_apps es))
haftmann@18517
   618
        else
haftmann@18517
   619
          trns
haftmann@18517
   620
          |> debug 10 (fn _ => "keeping arguments")
haftmann@18702
   621
          |> ag thy tabs ((f, ty), ts)
haftmann@18517
   622
    | NONE =>
haftmann@18517
   623
        trns
haftmann@18702
   624
        |> appgen_default thy tabs ((f, ty), ts)
haftmann@18517
   625
and exprgen_term thy tabs (Const (f, ty)) trns =
haftmann@18517
   626
      trns
haftmann@18517
   627
      |> appgen thy tabs ((f, ty), [])
haftmann@18516
   628
      |-> (fn e => pair e)
haftmann@18516
   629
  | exprgen_term thy tabs (Var ((v, i), ty)) trns =
haftmann@18516
   630
      trns
haftmann@18516
   631
      |> exprgen_type thy tabs ty
haftmann@18516
   632
      |-> (fn ty => pair (IVarE (if i = 0 then v else v ^ "_" ^ string_of_int i, ty)))
haftmann@18516
   633
  | exprgen_term thy tabs (Free (v, ty)) trns =
haftmann@18516
   634
      trns
haftmann@18516
   635
      |> exprgen_type thy tabs ty
haftmann@18516
   636
      |-> (fn ty => pair (IVarE (v, ty)))
haftmann@18516
   637
  | exprgen_term thy tabs (Abs (v, ty, t)) trns =
haftmann@18516
   638
      trns
haftmann@18516
   639
      |> exprgen_type thy tabs ty
haftmann@18516
   640
      ||>> exprgen_term thy tabs (subst_bound (Free (v, ty), t))
haftmann@18516
   641
      |-> (fn (ty, e) => pair ((v, ty) `|-> e))
haftmann@18516
   642
  | exprgen_term thy tabs (t as t1 $ t2) trns =
haftmann@18516
   643
      let
haftmann@18516
   644
        val (t', ts) = strip_comb t
haftmann@18516
   645
      in case t'
haftmann@18516
   646
       of Const (f, ty) =>
haftmann@18516
   647
            trns
haftmann@18517
   648
            |> appgen thy tabs ((f, ty), ts)
haftmann@18516
   649
            |-> (fn e => pair e)
haftmann@18516
   650
        | _ =>
haftmann@18516
   651
            trns
haftmann@18516
   652
            |> exprgen_term thy tabs t'
haftmann@18516
   653
            ||>> fold_map (exprgen_term thy tabs) ts
haftmann@18516
   654
            |-> (fn (e, es) => pair (e `$$ es))
haftmann@18516
   655
      end;
haftmann@18516
   656
haftmann@18454
   657
haftmann@18517
   658
(* application generators *)
haftmann@18517
   659
haftmann@18702
   660
(* fun appgen_eq thy tabs (("op =", Type ("fun", [ty, _])), [t1, t2]) trns =
haftmann@18517
   661
  trns
haftmann@18517
   662
  |> invoke_eq (exprgen_type thy tabs) (ensure_def_eq thy tabs) ty
haftmann@18517
   663
  |-> (fn false => error ("could not derive equality for " ^ Sign.string_of_typ thy ty)
haftmann@18517
   664
        | true => fn trns => trns
haftmann@18517
   665
  |> exprgen_term thy tabs t1
haftmann@18517
   666
  ||>> exprgen_term thy tabs t2
haftmann@18702
   667
  |-> (fn (e1, e2) => pair (Fun_eq `$ e1 `$ e2))); *)
haftmann@18702
   668
haftmann@18702
   669
haftmann@18702
   670
(* function extractors *)
haftmann@18702
   671
haftmann@18702
   672
fun mk_fun thy tabs (c, ty) trns =
haftmann@18702
   673
  case get_first (fn eqx => eqx (c, ty)) (get_eqextrs thy tabs)
haftmann@18702
   674
   of SOME (eq_thms, ty) =>
haftmann@18702
   675
        let
haftmann@18702
   676
          val sortctxt = ClassPackage.extract_sortctxt thy ty;
haftmann@18702
   677
          fun dest_eqthm eq_thm =
haftmann@18702
   678
            eq_thm
haftmann@18702
   679
            |> prop_of
haftmann@18702
   680
            |> Logic.dest_equals
haftmann@18702
   681
            |> apfst (strip_comb #> snd);
haftmann@18702
   682
          fun mk_eq (args, rhs) trns =
haftmann@18702
   683
            trns
haftmann@18702
   684
            |> fold_map (exprgen_term thy tabs o devarify_term) args
haftmann@18702
   685
            ||>> (exprgen_term thy tabs o devarify_term) rhs
haftmann@18702
   686
            |-> (fn (args, rhs) => pair (map ipat_of_iexpr args, rhs))
haftmann@18702
   687
        in
haftmann@18702
   688
          trns
haftmann@18702
   689
          |> fold_map (mk_eq o dest_eqthm) eq_thms
haftmann@18702
   690
          ||>> exprgen_type thy tabs (devarify_type ty)
haftmann@18702
   691
          ||>> fold_map (exprgen_tyvar_sort thy tabs) sortctxt
haftmann@18702
   692
          |-> (fn ((eqs, ty), sortctxt) => (pair o SOME) (eqs, (sortctxt, ty)))
haftmann@18702
   693
        end
haftmann@18702
   694
    | NONE => (NONE, trns);
haftmann@18702
   695
haftmann@18702
   696
fun eqextr_defs thy ((deftab, _), _) (c, ty) =
haftmann@18702
   697
  let
haftmann@18702
   698
    fun eq_typ (ty1, ty2) = 
haftmann@18702
   699
      Sign.typ_instance thy (ty1, ty2)
haftmann@18702
   700
      andalso Sign.typ_instance thy (ty2, ty1)
haftmann@18702
   701
  in
haftmann@18702
   702
    Option.mapPartial (get_first (fn (ty', thm) => if eq_typ (ty, ty')
haftmann@18702
   703
      then SOME ([thm], ty')
haftmann@18702
   704
      else NONE
haftmann@18702
   705
    )) (Symtab.lookup deftab c)
haftmann@18702
   706
  end;
haftmann@18517
   707
haftmann@18517
   708
haftmann@18517
   709
(* definition generators *)
haftmann@18454
   710
haftmann@18702
   711
fun defgen_clsdecl thy (tabs as (_, (insttab, _, _))) cls trns =
haftmann@18217
   712
  case name_of_idf thy nsp_class cls
haftmann@18217
   713
   of SOME cls =>
haftmann@18380
   714
        let
haftmann@18702
   715
          val cs = (snd o ClassPackage.the_consts_sign thy) cls;
haftmann@18702
   716
          val sortctxts = map (ClassPackage.extract_sortctxt thy o snd) cs;
haftmann@18702
   717
          val idfs = map (idf_of_name thy nsp_mem o fst) cs;
haftmann@18380
   718
        in
haftmann@18380
   719
          trns
haftmann@18380
   720
          |> debug 5 (fn _ => "trying defgen class declaration for " ^ quote cls)
haftmann@18702
   721
          |> fold_map (ensure_def_class thy tabs) (ClassPackage.the_superclasses thy cls)
haftmann@18702
   722
          ||>> fold_map (exprgen_type thy tabs o snd) cs
haftmann@18702
   723
          ||>> (fold_map o fold_map) (exprgen_tyvar_sort thy tabs) sortctxts
haftmann@18702
   724
          |-> (fn ((supcls, memtypes), sortctxts) => succeed
haftmann@18702
   725
            (Class ((supcls, ("a", idfs ~~ (sortctxts ~~ memtypes))), [])))
haftmann@18380
   726
        end
haftmann@18217
   727
    | _ =>
haftmann@18217
   728
        trns
haftmann@18217
   729
        |> fail ("no class definition found for " ^ quote cls);
haftmann@18217
   730
haftmann@18702
   731
fun defgen_funs thy tabs c trns =
haftmann@18702
   732
  case recconst_of_idf thy tabs c
haftmann@18702
   733
   of SOME (c, ty) =>
haftmann@18702
   734
        trns
haftmann@18702
   735
        |> mk_fun thy tabs (c, ty)
haftmann@18702
   736
        |-> (fn (SOME funn) => succeed (Fun funn)
haftmann@18702
   737
              | NONE => fail ("no defining equations found for " ^ quote c))
haftmann@18702
   738
    | NONE =>
haftmann@18702
   739
        trns
haftmann@18702
   740
        |> fail ("not a constant: " ^ quote c);
haftmann@18702
   741
haftmann@18702
   742
fun defgen_datatypecons thy (tabs as (_, (_, _, dtcontab))) co trns =
haftmann@18702
   743
  case Option.map (DatatypeconsNameMangler.rev thy dtcontab) (name_of_idf thy nsp_dtcon co)
haftmann@18702
   744
   of SOME (co, dtco) =>
haftmann@18702
   745
        trns
haftmann@18702
   746
        |> debug 5 (fn _ => "trying defgen datatype constructor for " ^ quote co)
haftmann@18702
   747
        |> ensure_def_tyco thy tabs dtco
haftmann@18702
   748
        |-> (fn dtco => succeed Undef)
haftmann@18702
   749
    | _ =>
haftmann@18702
   750
        trns
haftmann@18702
   751
        |> fail ("not a datatype constructor: " ^ quote co);
haftmann@18702
   752
haftmann@18454
   753
fun defgen_clsmem thy tabs m trns =
haftmann@18454
   754
  case name_of_idf thy nsp_mem m
haftmann@18454
   755
   of SOME m =>
haftmann@18360
   756
        trns
haftmann@18454
   757
        |> debug 5 (fn _ => "trying defgen class member for " ^ quote m)
haftmann@18454
   758
        |> ensure_def_class thy tabs ((the o ClassPackage.lookup_const_class thy) m)
haftmann@18702
   759
        |-> (fn cls => succeed Undef)
haftmann@18217
   760
    | _ =>
haftmann@18454
   761
        trns |> fail ("no class member found for " ^ quote m)
haftmann@18217
   762
haftmann@18454
   763
fun defgen_clsinst thy (tabs as (_, (insttab, _, _))) inst trns =
haftmann@18454
   764
  case Option.map (InstNameMangler.rev thy insttab) (name_of_idf thy nsp_inst inst)
haftmann@18454
   765
   of SOME (_, (cls, tyco)) =>
haftmann@18217
   766
        let
haftmann@18702
   767
          val (arity, memdefs) = ClassPackage.the_inst_sign thy (cls, tyco);
haftmann@18702
   768
          fun gen_membr (m, ty) trns =
haftmann@18702
   769
            trns
haftmann@18702
   770
            |> mk_fun thy tabs (m, ty)
haftmann@18702
   771
            |-> (fn SOME funn => pair (m, funn)
haftmann@18702
   772
                  | NONE => error ("could not derive definition for member " ^ quote m));
haftmann@18217
   773
        in
haftmann@18702
   774
          trns
haftmann@18231
   775
          |> debug 5 (fn _ => "trying defgen class instance for (" ^ quote cls ^ ", " ^ quote tyco ^ ")")
haftmann@18702
   776
          |> ensure_def_class thy tabs cls
haftmann@18454
   777
          ||>> ensure_def_tyco thy tabs tyco
haftmann@18702
   778
          ||>> fold_map (exprgen_tyvar_sort thy tabs) arity
haftmann@18702
   779
          ||>> fold_map gen_membr memdefs
haftmann@18702
   780
          |-> (fn (((cls, tyco), arity), memdefs) =>
haftmann@18702
   781
                 succeed (Classinst ((cls, (tyco, arity)), memdefs)))
haftmann@18217
   782
        end
haftmann@18217
   783
    | _ =>
haftmann@18454
   784
        trns |> fail ("no class instance found for " ^ quote inst);
haftmann@18217
   785
haftmann@18217
   786
haftmann@18217
   787
(* parametrized generators, for instantiation in HOL *)
haftmann@18217
   788
haftmann@18702
   789
fun appgen_let strip_abs thy tabs ((c, ty), [t2, t3]) trns =
haftmann@18517
   790
  let
haftmann@18702
   791
    fun dest_let (l as Const (c', _) $ t $ u) =
haftmann@18702
   792
          if c = c' then
haftmann@18702
   793
            case strip_abs 1 u
haftmann@18702
   794
             of ([p], u') => apfst (cons (p, t)) (dest_let u')
haftmann@18702
   795
              | _ => ([], l)
haftmann@18702
   796
          else ([], t)
haftmann@18517
   797
      | dest_let t = ([], t);
haftmann@18517
   798
    fun mk_let (l, r) trns =
haftmann@18335
   799
      trns
haftmann@18517
   800
      |> exprgen_term thy tabs l
haftmann@18517
   801
      ||>> exprgen_term thy tabs r
haftmann@18517
   802
      |-> (fn (l, r) => pair (r, ipat_of_iexpr l));
haftmann@18702
   803
    val (lets, body) = dest_let (Const (c, ty) $ t2 $ t3)
haftmann@18517
   804
  in
haftmann@18517
   805
    trns
haftmann@18517
   806
    |> fold_map mk_let lets
haftmann@18517
   807
    ||>> exprgen_term thy tabs body
haftmann@18517
   808
    |-> (fn (lets, body) =>
haftmann@18702
   809
         pair (Library.foldr (fn ((e, p), body) => ICase (e, [(p, body)])) (lets, body)))
haftmann@18517
   810
  end
haftmann@18217
   811
haftmann@18517
   812
fun appgen_split strip_abs thy tabs (c, [t2]) trns =
haftmann@18517
   813
  let
haftmann@18517
   814
    val ([p], body) = strip_abs 1 (Const c $ t2)
haftmann@18517
   815
  in
haftmann@18517
   816
    trns
haftmann@18517
   817
    |> exprgen_term thy tabs p
haftmann@18517
   818
    ||>> exprgen_term thy tabs body
haftmann@18702
   819
    |-> (fn (IVarE v, body) => pair (IAbs (v, body)))
haftmann@18517
   820
  end;
haftmann@18335
   821
haftmann@18702
   822
fun appgen_number_of mk_int_to_nat bin_to_int tyco_int tyco_nat thy tabs ((_,
haftmann@18702
   823
  Type (_, [_, ty as Type (tyco, [])])), [bin]) trns =
haftmann@18702
   824
    if tyco = tyco_int then
haftmann@18702
   825
      trns
haftmann@18702
   826
      |> exprgen_type thy tabs ty
haftmann@18702
   827
      |-> (fn ty => pair (CodegenThingol.IConst ((IntInf.toString o bin_to_int) bin, ty)))
haftmann@18702
   828
    else if tyco = tyco_nat then
haftmann@18702
   829
      trns
haftmann@18702
   830
      |> exprgen_term thy tabs (mk_int_to_nat bin)
haftmann@18702
   831
    else error ("invalid type constructor for numeral: " ^ quote tyco);
haftmann@18217
   832
haftmann@18517
   833
fun appgen_datatype_case cos thy tabs ((_, ty), ts) trns =
haftmann@18247
   834
  let
haftmann@18517
   835
    val (ts', t) = split_last ts;
haftmann@18517
   836
    val (tys, dty) = (split_last o fst o strip_type) ty;
haftmann@18517
   837
    fun gen_names i =
haftmann@18517
   838
      variantlist (replicate i "x", foldr add_term_names
haftmann@18517
   839
       (map (fst o fst o dest_Var) (foldr add_term_vars [] ts)) ts);
haftmann@18517
   840
    fun cg_case_d (((cname, i), ty), t) trns =
haftmann@18247
   841
      let
haftmann@18247
   842
        val vs = gen_names i;
haftmann@18247
   843
        val tys = Library.take (i, (fst o strip_type) ty);
haftmann@18330
   844
        val frees = map2 (curry Free) vs tys;
haftmann@18247
   845
        val t' = Envir.beta_norm (list_comb (t, frees));
haftmann@18247
   846
      in
haftmann@18247
   847
        trns
haftmann@18516
   848
        |> exprgen_term thy tabs (list_comb (Const (cname, tys ---> dty), frees))
haftmann@18516
   849
        ||>> exprgen_term thy tabs t'
haftmann@18247
   850
        |-> (fn (ep, e) => pair (ipat_of_iexpr ep, e))
haftmann@18247
   851
      end;
haftmann@18517
   852
  in
haftmann@18517
   853
    trns
haftmann@18517
   854
    |> exprgen_term thy tabs t
haftmann@18517
   855
    ||>> fold_map cg_case_d ((cos ~~ tys) ~~ ts')
haftmann@18702
   856
    |-> (fn (t, ds) => pair (ICase (t, ds)))
haftmann@18247
   857
  end;
haftmann@18247
   858
haftmann@18702
   859
fun gen_add_case_const prep_c get_case_const_data raw_c thy =
haftmann@18517
   860
  let
haftmann@18517
   861
    val c = prep_c thy raw_c;
haftmann@18702
   862
    val (tys, dty) = (split_last o fst o strip_type o Sign.the_const_type thy) c;
haftmann@18517
   863
    val cos = (the o get_case_const_data thy) c;
haftmann@18517
   864
    val n_eta = length cos + 1;
haftmann@18517
   865
  in
haftmann@18517
   866
    thy
haftmann@18517
   867
    |> add_appconst_i (c, ((n_eta, n_eta), appgen_datatype_case cos))
haftmann@18517
   868
  end;
haftmann@18517
   869
haftmann@18702
   870
val add_case_const = gen_add_case_const Sign.intern_const;
haftmann@18702
   871
val add_case_const_i = gen_add_case_const (K I);
haftmann@18517
   872
haftmann@18454
   873
fun defgen_datatype get_datatype get_datacons thy (tabs as (_, (_, _, dtcontab))) dtco trns =
haftmann@18454
   874
  case name_of_idf thy nsp_tyco dtco
haftmann@18380
   875
   of SOME dtco =>
haftmann@18380
   876
        (case get_datatype thy dtco
haftmann@18380
   877
         of SOME (vars, cos) =>
haftmann@18380
   878
              let
haftmann@18380
   879
                val cotys = map (the o get_datacons thy o rpair dtco) cos;
haftmann@18454
   880
                val coidfs = map (fn co => (DatatypeconsNameMangler.get thy dtcontab (co, dtco)) |>
haftmann@18454
   881
                  idf_of_name thy nsp_dtcon) cos;
haftmann@18380
   882
              in
haftmann@18380
   883
                trns
haftmann@18380
   884
                |> debug 5 (fn _ => "trying defgen datatype for " ^ quote dtco)
haftmann@18702
   885
                |> fold_map (exprgen_tyvar_sort thy tabs) vars
haftmann@18516
   886
                ||>> (fold_map o fold_map) (exprgen_type thy tabs o devarify_type) cotys
haftmann@18380
   887
                |-> (fn (sorts, tys) => succeed (Datatype
haftmann@18702
   888
                     ((sorts, coidfs ~~ tys), [])))
haftmann@18380
   889
              end
haftmann@18217
   890
          | NONE =>
haftmann@18217
   891
              trns
haftmann@18380
   892
              |> fail ("no datatype found for " ^ quote dtco))
haftmann@18217
   893
    | NONE =>
haftmann@18217
   894
        trns
haftmann@18454
   895
        |> fail ("not a type constructor: " ^ quote dtco)
haftmann@18335
   896
haftmann@18217
   897
haftmann@18516
   898
haftmann@18516
   899
(** theory interface **)
haftmann@18217
   900
haftmann@18454
   901
fun mk_tabs thy =
haftmann@18217
   902
  let
haftmann@18454
   903
    fun extract_defs thy =
haftmann@18217
   904
      let
haftmann@18702
   905
        fun dest tm =
haftmann@18454
   906
          let
haftmann@18702
   907
            val (lhs, rhs) = Logic.dest_equals (prop_of tm);
haftmann@18702
   908
            val (t, args) = strip_comb lhs;
haftmann@18702
   909
            val (c, ty) = dest_Const t
haftmann@18702
   910
          in if forall is_Var args then SOME ((c, ty), tm) else NONE
haftmann@18454
   911
          end handle TERM _ => NONE;
haftmann@18454
   912
        fun prep_def def = (case Codegen.preprocess thy [def] of
haftmann@18702
   913
          [def'] => def' | _ => error "mk_auxtab: bad preprocessor");
haftmann@18702
   914
        fun add_def (name, _) =
haftmann@18702
   915
          case (dest o prep_def o Thm.get_axiom thy) name
haftmann@18702
   916
           of SOME ((c, ty), tm) =>
haftmann@18702
   917
                Symtab.default (c, []) #> Symtab.map_entry c (cons (ty, tm))
haftmann@18702
   918
            | NONE => I
haftmann@18217
   919
      in
haftmann@18454
   920
        Symtab.empty
haftmann@18702
   921
        |> fold (Symtab.fold add_def o snd o #axioms o Theory.rep_theory)
haftmann@18702
   922
             (thy :: Theory.ancestors_of thy)
haftmann@18217
   923
      end;
haftmann@18454
   924
    fun mk_insttab thy =
haftmann@18454
   925
      InstNameMangler.empty
haftmann@18454
   926
      |> Symtab.fold_map
haftmann@18702
   927
          (fn (cls, (clsmems, clsinsts)) => fold_map
haftmann@18454
   928
            (fn (tyco, thyname) => InstNameMangler.declare thy (thyname, (cls, tyco))) clsinsts)
haftmann@18454
   929
                 (ClassPackage.get_classtab thy)
haftmann@18454
   930
      |-> (fn _ => I);
haftmann@18702
   931
    fun mk_overltabs thy deftab =
haftmann@18454
   932
      (Symtab.empty, ConstNameMangler.empty)
haftmann@18454
   933
      |> Symtab.fold
haftmann@18454
   934
          (fn (c, [_]) => I
haftmann@18454
   935
            | (c, tytab) =>
haftmann@18454
   936
                (fn (overltab1, overltab2) => (
haftmann@18454
   937
                  overltab1
haftmann@18454
   938
                  |> Symtab.update_new (c, (Sign.the_const_constraint thy c, map fst tytab)),
haftmann@18454
   939
                  overltab2
haftmann@18454
   940
                  |> fold (fn (ty, _) => ConstNameMangler.declare thy (idf_of_name thy nsp_overl c, (Sign.the_const_constraint thy c, ty)) #> snd) tytab
haftmann@18702
   941
                ))) deftab;
haftmann@18454
   942
    fun mk_dtcontab thy =
haftmann@18454
   943
      DatatypeconsNameMangler.empty
haftmann@18454
   944
      |> fold_map
haftmann@18455
   945
          (fn (_, co_dtco) => DatatypeconsNameMangler.declare_multi thy co_dtco)
haftmann@18455
   946
            (fold (fn (co, dtco) =>
haftmann@18455
   947
              let
haftmann@18455
   948
                val key = ((NameSpace.drop_base o NameSpace.drop_base) co, NameSpace.base co)
haftmann@18455
   949
              in AList.default (op =) (key, []) #> AList.map_entry (op =) key (cons (co, dtco)) end
haftmann@18455
   950
            ) (get_all_datatype_cons thy) [])
haftmann@18454
   951
      |-> (fn _ => I);
haftmann@18454
   952
    fun mk_clsmemtab thy =
haftmann@18454
   953
      Symtab.empty
haftmann@18454
   954
      |> Symtab.fold
haftmann@18454
   955
          (fn (class, (clsmems, _)) => fold
haftmann@18454
   956
            (fn clsmem => Symtab.update (clsmem, class)) clsmems)
haftmann@18454
   957
              (ClassPackage.get_classtab thy);
haftmann@18702
   958
    val deftab = extract_defs thy;
haftmann@18454
   959
    val insttab = mk_insttab thy;
haftmann@18702
   960
    val overltabs = mk_overltabs thy deftab;
haftmann@18454
   961
    val dtcontab = mk_dtcontab thy;
haftmann@18454
   962
    val clsmemtab = mk_clsmemtab thy;
haftmann@18454
   963
  in ((deftab, clsmemtab), (insttab, overltabs, dtcontab)) end;
haftmann@18217
   964
haftmann@18702
   965
fun check_for_target thy target =
haftmann@18702
   966
  if (Symtab.defined o #target_data o CodegenData.get) thy target
haftmann@18702
   967
  then ()
haftmann@18702
   968
  else error ("unknown code target language: " ^ quote target);
haftmann@18335
   969
haftmann@18516
   970
fun map_module f =
haftmann@18702
   971
  map_codegen_data (fn (modl, gens, target_data, logic_data) =>
haftmann@18702
   972
    (f modl, gens, target_data, logic_data));
haftmann@18516
   973
haftmann@18702
   974
fun expand_module gen thy =
haftmann@18516
   975
  (#modl o CodegenData.get) thy
haftmann@18702
   976
  |> start_transact (gen thy (mk_tabs thy))
haftmann@18516
   977
  |-> (fn x:'a => fn modl => (x, map_module (K modl) thy));
haftmann@18516
   978
haftmann@18516
   979
fun rename_inconsistent thy =
haftmann@18217
   980
  let
haftmann@18516
   981
    fun get_inconsistent thyname =
haftmann@18516
   982
      let
haftmann@18516
   983
        val thy = theory thyname;
haftmann@18516
   984
        fun own_tables get =
haftmann@18516
   985
          (get thy)
haftmann@18516
   986
          |> fold (Symtab.fold (Symtab.remove (K true)) o get) (Theory.parents_of thy)
haftmann@18516
   987
          |> Symtab.keys;
haftmann@18516
   988
        val names = own_tables (#2 o #types o Type.rep_tsig o Sign.tsig_of)
haftmann@18516
   989
          @ own_tables (#2 o #declarations o Consts.dest o #consts o Sign.rep_sg);
haftmann@18516
   990
        fun diff names =
haftmann@18516
   991
          fold (fn name =>
haftmann@18516
   992
            if is_prefix (op =) (NameSpace.unpack thyname) (NameSpace.unpack name)
haftmann@18516
   993
            then I
haftmann@18516
   994
            else cons (name, NameSpace.append thyname (NameSpace.base name))) names [];
haftmann@18516
   995
      in diff names end;
haftmann@18516
   996
    val inconsistent = map get_inconsistent (ThyInfo.names ()) |> Library.flat;
haftmann@18516
   997
    fun add (src, dst) thy =
haftmann@18516
   998
      if (is_some oo Symtab.lookup o fst o #alias o #logic_data o CodegenData.get) thy src
haftmann@18516
   999
      then (warning ("code generator alias already defined for " ^ quote src ^ ", will not overwrite"); thy)
haftmann@18516
  1000
      else add_alias (src, dst) thy
haftmann@18516
  1001
  in fold add inconsistent thy end;
haftmann@18516
  1002
haftmann@18517
  1003
fun ensure_datatype_case_consts get_datatype_case_consts get_case_const_data thy =
haftmann@18517
  1004
  let
haftmann@18517
  1005
    fun ensure case_c thy =
haftmann@18517
  1006
      if
haftmann@18517
  1007
        Symtab.defined ((#appconst o #gens o CodegenData.get) thy) case_c
haftmann@18517
  1008
      then
haftmann@18517
  1009
        (warning ("case constant " ^ quote case_c ^ " already present in application table, will not overwrite"); thy)
haftmann@18517
  1010
      else
haftmann@18702
  1011
        add_case_const_i get_case_const_data case_c thy;
haftmann@18517
  1012
  in
haftmann@18517
  1013
    fold ensure (get_datatype_case_consts thy) thy
haftmann@18517
  1014
  end;
haftmann@18517
  1015
haftmann@18516
  1016
haftmann@18516
  1017
haftmann@18516
  1018
(** target languages **)
haftmann@18516
  1019
haftmann@18516
  1020
(* primitive definitions *)
haftmann@18516
  1021
haftmann@18702
  1022
fun read_typ thy =
haftmann@18702
  1023
  Sign.read_typ (thy, K NONE);
haftmann@18702
  1024
haftmann@18517
  1025
fun read_const thy (raw_c, raw_ty) =
haftmann@18517
  1026
  let
haftmann@18517
  1027
    val c = Sign.intern_const thy raw_c;
haftmann@18702
  1028
    val _ = if Sign.declared_const thy c
haftmann@18702
  1029
      then ()
haftmann@18702
  1030
      else error ("no such constant: " ^ quote c);
haftmann@18517
  1031
    val ty = case raw_ty
haftmann@18517
  1032
     of NONE => Sign.the_const_constraint thy c
haftmann@18702
  1033
      | SOME raw_ty => read_typ thy raw_ty;
haftmann@18517
  1034
  in (c, ty) end;
haftmann@18517
  1035
haftmann@18702
  1036
fun read_quote reader gen raw thy =
haftmann@18702
  1037
  expand_module
haftmann@18702
  1038
    (fn thy => fn tabs => gen thy tabs (reader thy raw))
haftmann@18702
  1039
    thy;
haftmann@18702
  1040
haftmann@18517
  1041
fun gen_add_prim prep_name prep_primdef raw_name deps (target, raw_primdef) thy =
haftmann@18516
  1042
  let
haftmann@18702
  1043
    val _ = if Symtab.defined ((#target_data o CodegenData.get) thy) target
haftmann@18516
  1044
      then () else error ("unknown target language: " ^ quote target);
haftmann@18516
  1045
    val tabs = mk_tabs thy;
haftmann@18516
  1046
    val name = prep_name thy tabs raw_name;
haftmann@18516
  1047
    val primdef = prep_primdef raw_primdef;
haftmann@18217
  1048
  in
haftmann@18516
  1049
    thy
haftmann@18517
  1050
    |> map_module (CodegenThingol.add_prim name deps (target, primdef))
haftmann@18217
  1051
  end;
haftmann@18217
  1052
haftmann@18516
  1053
val add_prim_i = gen_add_prim ((K o K) I) I;
haftmann@18516
  1054
val add_prim_class = gen_add_prim
haftmann@18516
  1055
  (fn thy => K (idf_of_name thy nsp_class o Sign.intern_class thy))
haftmann@18702
  1056
  (Pretty.str o CodegenSerializer.parse_targetdef I);
haftmann@18516
  1057
val add_prim_tyco = gen_add_prim
haftmann@18516
  1058
  (fn thy => K (idf_of_name thy nsp_tyco o Sign.intern_type thy))
haftmann@18702
  1059
  (Pretty.str o CodegenSerializer.parse_targetdef I);
haftmann@18516
  1060
val add_prim_const = gen_add_prim
haftmann@18517
  1061
  (fn thy => fn tabs => idf_of_const thy tabs o read_const thy)
haftmann@18702
  1062
  (Pretty.str o CodegenSerializer.parse_targetdef I);
haftmann@18516
  1063
haftmann@18702
  1064
val ensure_prim = (map_module oo CodegenThingol.ensure_prim);
haftmann@18217
  1065
haftmann@18517
  1066
haftmann@18217
  1067
(* syntax *)
haftmann@18217
  1068
haftmann@18702
  1069
val parse_syntax_tyco =
haftmann@18217
  1070
  let
haftmann@18702
  1071
    fun mk reader raw_tyco target thy =
haftmann@18702
  1072
      let
haftmann@18702
  1073
        val _ = check_for_target thy target;
haftmann@18702
  1074
        fun check_tyco tyco =
haftmann@18702
  1075
          if Sign.declared_tyname thy tyco
haftmann@18702
  1076
          then tyco
haftmann@18702
  1077
          else error ("no such type constructor: " ^ quote tyco);
haftmann@18702
  1078
        fun prep_tyco thy tyco =
haftmann@18702
  1079
          tyco
haftmann@18702
  1080
          |> Sign.intern_type thy
haftmann@18702
  1081
          |> check_tyco
haftmann@18702
  1082
          |> idf_of_name thy nsp_tyco;
haftmann@18702
  1083
        val tyco = prep_tyco thy raw_tyco;
haftmann@18702
  1084
      in
haftmann@18702
  1085
        thy
haftmann@18702
  1086
        |> ensure_prim tyco target
haftmann@18702
  1087
        |> reader
haftmann@18702
  1088
        |-> (fn pretty => map_codegen_data
haftmann@18702
  1089
          (fn (modl, gens, target_data, logic_data) =>
haftmann@18702
  1090
             (modl, gens,
haftmann@18702
  1091
              target_data |> Symtab.map_entry target
haftmann@18702
  1092
                (map_target_data
haftmann@18702
  1093
                  (fn (syntax_tyco, syntax_const) =>
haftmann@18704
  1094
                   (syntax_tyco |> Symtab.update
haftmann@18702
  1095
                      (tyco, (pretty, stamp ())),
haftmann@18702
  1096
                    syntax_const))),
haftmann@18702
  1097
              logic_data)))
haftmann@18702
  1098
      end;
haftmann@18217
  1099
  in
haftmann@18702
  1100
    CodegenSerializer.parse_syntax (read_quote read_typ exprgen_type)
haftmann@18702
  1101
    #-> (fn reader => pair (mk reader))
haftmann@18217
  1102
  end;
haftmann@18217
  1103
haftmann@18704
  1104
fun add_pretty_syntax_const c target pretty =
haftmann@18704
  1105
  map_codegen_data
haftmann@18704
  1106
    (fn (modl, gens, target_data, logic_data) =>
haftmann@18704
  1107
       (modl, gens,
haftmann@18704
  1108
        target_data |> Symtab.map_entry target
haftmann@18704
  1109
          (map_target_data
haftmann@18704
  1110
            (fn (syntax_tyco, syntax_const) =>
haftmann@18704
  1111
             (syntax_tyco,
haftmann@18704
  1112
              syntax_const
haftmann@18704
  1113
              |> Symtab.update
haftmann@18704
  1114
                 (c, (pretty, stamp ()))))),
haftmann@18704
  1115
        logic_data));
haftmann@18704
  1116
haftmann@18702
  1117
val parse_syntax_const =
haftmann@18217
  1118
  let
haftmann@18702
  1119
    fun mk reader raw_const target thy =
haftmann@18702
  1120
      let
haftmann@18702
  1121
        val _ = check_for_target thy target;
haftmann@18702
  1122
        val tabs = mk_tabs thy;
haftmann@18702
  1123
        val c = idf_of_const thy tabs (read_const thy raw_const);
haftmann@18702
  1124
      in
haftmann@18702
  1125
        thy
haftmann@18702
  1126
        |> ensure_prim c target
haftmann@18702
  1127
        |> reader
haftmann@18704
  1128
        |-> (fn pretty => add_pretty_syntax_const c target pretty)
haftmann@18702
  1129
      end;
haftmann@18217
  1130
  in
haftmann@18702
  1131
    CodegenSerializer.parse_syntax (read_quote Sign.read_term exprgen_term)
haftmann@18702
  1132
    #-> (fn reader => pair (mk reader))
haftmann@18217
  1133
  end;
haftmann@18217
  1134
haftmann@18704
  1135
fun add_pretty_list raw_nil raw_cons (target, seri) thy =
haftmann@18704
  1136
  let
haftmann@18704
  1137
    val _ = check_for_target thy target;
haftmann@18704
  1138
    val tabs = mk_tabs thy;
haftmann@18704
  1139
    fun mk_const raw_name =
haftmann@18704
  1140
      let
haftmann@18704
  1141
        val name = Sign.intern_const thy raw_name;
haftmann@18704
  1142
      in idf_of_const thy tabs (name, Sign.the_const_type thy name) end;
haftmann@18704
  1143
    val nil' = mk_const raw_nil;
haftmann@18704
  1144
    val cons' = mk_const raw_cons;
haftmann@18704
  1145
    val pr' = CodegenSerializer.pretty_list nil' cons' seri;
haftmann@18704
  1146
  in
haftmann@18704
  1147
    thy
haftmann@18704
  1148
    |> ensure_prim cons' target
haftmann@18704
  1149
    |> add_pretty_syntax_const cons' target pr'
haftmann@18704
  1150
  end;
haftmann@18704
  1151
haftmann@18217
  1152
haftmann@18516
  1153
haftmann@18516
  1154
(** code generation **)
haftmann@18217
  1155
haftmann@18702
  1156
fun generate_code raw_consts thy =
haftmann@18217
  1157
  let
haftmann@18702
  1158
    val consts = map (read_const thy) raw_consts;
haftmann@18702
  1159
    fun generate thy tabs = fold_map (ensure_def_const thy tabs) consts
haftmann@18217
  1160
  in
haftmann@18217
  1161
    thy
haftmann@18702
  1162
    |> expand_module generate
haftmann@18217
  1163
  end;
haftmann@18217
  1164
haftmann@18702
  1165
fun serialize_code target filename raw_consts thy =
haftmann@18217
  1166
  let
haftmann@18702
  1167
    fun get_serializer thy target =
haftmann@18702
  1168
      let
haftmann@18702
  1169
        val _ = check_for_target thy target;
haftmann@18702
  1170
        val target_data =
haftmann@18702
  1171
          thy
haftmann@18702
  1172
          |> CodegenData.get
haftmann@18702
  1173
          |> #target_data
haftmann@18702
  1174
          |> (fn data => (the oo Symtab.lookup) data target);
haftmann@18702
  1175
      in
haftmann@18702
  1176
        (the o Symtab.lookup (! serializers)) target (
haftmann@18702
  1177
          (Option.map fst oo Symtab.lookup o #syntax_tyco) target_data,
haftmann@18702
  1178
          (Option.map fst oo Symtab.lookup o #syntax_const) target_data
haftmann@18702
  1179
        )
haftmann@18702
  1180
      end;
haftmann@18282
  1181
    fun use_code code =
haftmann@18702
  1182
      if target = "ml" andalso filename = "-"
haftmann@18217
  1183
      then use_text Context.ml_output false code
haftmann@18217
  1184
      else File.write (Path.unpack filename) (code ^ "\n");
haftmann@18702
  1185
    fun serialize thy cs =
haftmann@18702
  1186
      let
haftmann@18702
  1187
        val module = (#modl o CodegenData.get) thy;
haftmann@18702
  1188
        val seri = get_serializer thy target "Generated";
haftmann@18702
  1189
      in case cs
haftmann@18702
  1190
       of [] => seri NONE module () |> fst |> Pretty.output |> use_code
haftmann@18702
  1191
        | cs => seri (SOME cs) module () |> fst |> Pretty.output |> use_code
haftmann@18702
  1192
      end;
haftmann@18217
  1193
  in
haftmann@18217
  1194
    thy
haftmann@18702
  1195
    |> (if is_some raw_consts then generate_code (the raw_consts) else pair [])
haftmann@18702
  1196
    |-> (fn cs => `(fn thy => serialize thy cs))
haftmann@18702
  1197
    |-> (fn _ => I)
haftmann@18217
  1198
  end;
haftmann@18217
  1199
haftmann@18217
  1200
haftmann@18454
  1201
haftmann@18516
  1202
(** toplevel interface **)
haftmann@18217
  1203
haftmann@18217
  1204
local
haftmann@18217
  1205
haftmann@18217
  1206
structure P = OuterParse
haftmann@18217
  1207
and K = OuterKeyword
haftmann@18217
  1208
haftmann@18217
  1209
in
haftmann@18217
  1210
haftmann@18517
  1211
val (classK, generateK, serializeK,
haftmann@18517
  1212
     primclassK, primtycoK, primconstK,
haftmann@18517
  1213
     syntax_tycoK, syntax_constK, aliasK) =
haftmann@18517
  1214
  ("code_class", "code_generate", "code_serialize",
haftmann@18517
  1215
   "code_primclass", "code_primtyco", "code_primconst",
haftmann@18517
  1216
   "code_syntax_tyco", "code_syntax_const", "code_alias");
haftmann@18517
  1217
val (constantsK, dependingK) =
haftmann@18517
  1218
  ("constants", "depending_on");
haftmann@18335
  1219
haftmann@18335
  1220
val classP =
haftmann@18335
  1221
  OuterSyntax.command classK "codegen data for classes" K.thy_decl (
haftmann@18335
  1222
    P.xname
haftmann@18335
  1223
    -- ((P.$$$ "\\<Rightarrow>" || P.$$$ "=>") |-- (P.list1 P.name))
haftmann@18335
  1224
    -- (Scan.optional ((P.$$$ "\\<Rightarrow>" || P.$$$ "=>") |-- (P.list1 P.name)) [])
haftmann@18335
  1225
    >> (fn ((name, tycos), consts) => (Toplevel.theory (ClassPackage.add_classentry name consts tycos)))
haftmann@18335
  1226
  )
haftmann@18217
  1227
haftmann@18217
  1228
val generateP =
haftmann@18282
  1229
  OuterSyntax.command generateK "generate executable code for constants" K.thy_decl (
haftmann@18247
  1230
    Scan.repeat1 (P.name -- Scan.option (P.$$$ "::" |-- P.typ))
haftmann@18217
  1231
    >> (fn consts =>
haftmann@18231
  1232
          Toplevel.theory (generate_code consts #> snd))
haftmann@18217
  1233
  );
haftmann@18217
  1234
haftmann@18217
  1235
val serializeP =
haftmann@18282
  1236
  OuterSyntax.command serializeK "serialize executable code for constants" K.thy_decl (
haftmann@18217
  1237
    P.name
haftmann@18217
  1238
    -- P.name
haftmann@18217
  1239
    -- Scan.option (
haftmann@18380
  1240
         P.$$$ constantsK
haftmann@18247
  1241
         |-- Scan.repeat1 (P.name -- Scan.option (P.$$$ "::" |-- P.typ))
haftmann@18217
  1242
       )
haftmann@18702
  1243
    >> (fn ((target, filename), raw_consts) =>
haftmann@18702
  1244
          Toplevel.theory (serialize_code target filename raw_consts))
haftmann@18217
  1245
  );
haftmann@18217
  1246
haftmann@18217
  1247
val aliasP =
haftmann@18282
  1248
  OuterSyntax.command aliasK "declare an alias for a theory identifier" K.thy_decl (
haftmann@18702
  1249
    Scan.repeat1 (P.name -- P.name)
haftmann@18702
  1250
      >> (Toplevel.theory oo fold) add_alias
haftmann@18217
  1251
  );
haftmann@18217
  1252
haftmann@18517
  1253
val primclassP =
haftmann@18517
  1254
  OuterSyntax.command primclassK "define target-lanugage specific class" K.thy_decl (
haftmann@18517
  1255
    P.xname
haftmann@18702
  1256
    -- Scan.optional (P.$$$ dependingK |--
haftmann@18702
  1257
         P.$$$ "(" |-- P.list1 P.name --| P.$$$ ")") []
haftmann@18517
  1258
    -- Scan.repeat1 (P.name -- P.text)
haftmann@18702
  1259
      >> (fn ((raw_class, depends), primdefs) =>
haftmann@18517
  1260
            (Toplevel.theory oo fold) (add_prim_class raw_class depends) primdefs)
haftmann@18517
  1261
  );
haftmann@18517
  1262
haftmann@18517
  1263
val primtycoP =
haftmann@18517
  1264
  OuterSyntax.command primtycoK "define target-lanugage specific type constructor" K.thy_decl (
haftmann@18517
  1265
    P.xname
haftmann@18702
  1266
    -- Scan.optional (P.$$$ dependingK |--
haftmann@18702
  1267
         P.$$$ "(" |-- P.list1 P.name --| P.$$$ ")") []
haftmann@18517
  1268
    -- Scan.repeat1 (P.name -- P.text)
haftmann@18702
  1269
      >> (fn ((raw_tyco, depends), primdefs) =>
haftmann@18517
  1270
            (Toplevel.theory oo fold) (add_prim_tyco raw_tyco depends) primdefs)
haftmann@18517
  1271
  );
haftmann@18517
  1272
haftmann@18517
  1273
val primconstP =
haftmann@18517
  1274
  OuterSyntax.command primconstK "define target-lanugage specific constant" K.thy_decl (
haftmann@18702
  1275
    (P.xname -- Scan.option (P.$$$ "::" |-- P.typ))
haftmann@18702
  1276
    -- Scan.optional (P.$$$ dependingK |--
haftmann@18702
  1277
         P.$$$ "(" |-- P.list1 P.name --| P.$$$ ")") []
haftmann@18517
  1278
    -- Scan.repeat1 (P.name -- P.text)
haftmann@18702
  1279
      >> (fn ((raw_const, depends), primdefs) =>
haftmann@18517
  1280
            (Toplevel.theory oo fold) (add_prim_const raw_const depends) primdefs)
haftmann@18517
  1281
  );
haftmann@18517
  1282
haftmann@18702
  1283
val _ : OuterParse.token list -> (string -> string -> theory -> theory) * OuterParse.token list
haftmann@18702
  1284
 = parse_syntax_tyco;
haftmann@18702
  1285
haftmann@18217
  1286
val syntax_tycoP =
haftmann@18217
  1287
  OuterSyntax.command syntax_tycoK "define code syntax for type constructor" K.thy_decl (
haftmann@18702
  1288
    Scan.repeat1 (
haftmann@18702
  1289
      P.xname
haftmann@18702
  1290
      -- Scan.repeat1 (
haftmann@18702
  1291
           P.name -- parse_syntax_tyco
haftmann@18702
  1292
         )
haftmann@18702
  1293
    )
haftmann@18702
  1294
    >> (Toplevel.theory oo fold) (fn (raw_tyco, syns) =>
haftmann@18702
  1295
          fold (fn (target, modifier) => modifier raw_tyco target) syns)
haftmann@18217
  1296
  );
haftmann@18217
  1297
haftmann@18217
  1298
val syntax_constP =
haftmann@18217
  1299
  OuterSyntax.command syntax_constK "define code syntax for constant" K.thy_decl (
haftmann@18702
  1300
    Scan.repeat1 (
haftmann@18702
  1301
      (P.xname -- Scan.option (P.$$$ "::" |-- P.typ))
haftmann@18702
  1302
      -- Scan.repeat1 (
haftmann@18702
  1303
           P.name -- parse_syntax_const
haftmann@18702
  1304
         )
haftmann@18702
  1305
    )
haftmann@18702
  1306
    >> (Toplevel.theory oo fold) (fn (raw_c, syns) =>
haftmann@18702
  1307
          fold (fn (target, modifier) => modifier raw_c target) syns)
haftmann@18217
  1308
  );
haftmann@18217
  1309
haftmann@18517
  1310
val _ = OuterSyntax.add_parsers [classP, generateP, serializeP, aliasP,
haftmann@18517
  1311
  primclassP, primtycoP, primconstP, syntax_tycoP, syntax_constP];
haftmann@18517
  1312
val _ = OuterSyntax.add_keywords ["\\<Rightarrow>", "=>", constantsK, dependingK];
haftmann@18217
  1313
haftmann@18217
  1314
haftmann@18516
  1315
wenzelm@18708
  1316
(** theory setup **)
haftmann@18516
  1317
wenzelm@18708
  1318
val _ = Context.add_setup
wenzelm@18708
  1319
 (add_eqextr ("defs", eqextr_defs) #>
wenzelm@18708
  1320
  add_defgen ("clsdecl", defgen_clsdecl) #>
wenzelm@18708
  1321
  add_defgen ("funs", defgen_funs) #>
wenzelm@18708
  1322
  add_defgen ("clsmem", defgen_clsmem) #>
wenzelm@18708
  1323
  add_defgen ("datatypecons", defgen_datatypecons));
wenzelm@18708
  1324
wenzelm@18708
  1325
(*   add_appconst_i ("op =", ((2, 2), appgen_eq))  *)
wenzelm@18708
  1326
(*   add_defgen ("clsinst", defgen_clsinst)  *)
haftmann@18217
  1327
haftmann@18217
  1328
end; (* local *)
haftmann@18217
  1329
haftmann@18217
  1330
end; (* struct *)