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