fun purge _ _ = CodegenThingol.empty_code;

   fun purge _ NONE _ = CodegenThingol.empty_code

     | purge NONE _ _ = CodegenThingol.empty_code

     | purge (SOME thy) (SOME cs) code =

         let

           val cs_exisiting =

             map_filter (CodegenNames.const_rev thy) (Graph.keys code);

         in

           Graph.del_nodes

             ((Graph.all_succs code

               o map (CodegenNames.const thy)

               o filter (member CodegenConsts.eq_const cs_exisiting)

               ) cs)

             code

         end;

   type T = appgens;

   type T = appgens * abstypes;

   val empty = Symtab.empty;

   val empty = (Symtab.empty, (Symtab.empty, Consttab.empty));

   fun merge _ = merge_appgens;

   fun merge _ ((appgens1, abstypes1), (appgens2, abstypes2)) =

     (merge_appgens (appgens1, appgens2), merge_abstypes (abstypes1, abstypes2));

 fun check_strict has_seri x (false, _) =

 fun check_strict (false, _) has_seri x =

   | check_strict has_seri x (_, SOME targets) =

   | check_strict (_, SOME targets) has_seri x =

   | check_strict has_seri x (true, _) =

   | check_strict (true, _) has_seri x =

     val strict = check_strict (CodegenSerializer.tyco_has_serialization thy) tyco' strct;

     val strict = check_strict strct (CodegenSerializer.tyco_has_serialization thy) tyco';

       trns

       case get_abstype thy (tyco, tys)

       |> ensure_def_tyco thy algbr funcgr strct tyco

        of SOME ty =>

       ||>> fold_map (exprgen_type thy algbr funcgr strct) tys

             trns

       |-> (fn (tyco, tys) => pair (tyco `%% tys));

             |> exprgen_type thy algbr funcgr strct ty

         | NONE =>

             trns

             |> ensure_def_tyco thy algbr funcgr strct tyco

             ||>> fold_map (exprgen_type thy algbr funcgr strct) tys

             |-> (fn (tyco, tys) => pair (tyco `%% tys));

       case CodegenFuncgr.get_funcs funcgr (c, tys)

       case CodegenFuncgr.get_funcs funcgr

         (perhaps (Consttab.lookup ((snd o snd o CodegenPackageData.get) thy)) (c, tys))

     val strict = check_strict (CodegenSerializer.const_has_serialization thy) c' strct;

     val strict = check_strict strct (CodegenSerializer.const_has_serialization thy) c';

   case Symtab.lookup (CodegenPackageData.get thy) c

   case Symtab.lookup (fst (CodegenPackageData.get thy)) c

     val i = (length o fst o strip_type o Sign.the_const_type thy) c

     val i = (length o fst o strip_type o Sign.the_const_type thy) c;

   in CodegenPackageData.map (Symtab.update (c, (i, (appgen, stamp ())))) thy end;

     val _ = Code.change thy (K CodegenThingol.empty_code);

   in

     (CodegenPackageData.map o apfst)

       (Symtab.update (c, (i, (appgen, stamp ())))) thy

   end;

 (** abstype and constsubst interface **)

 fun gen_abstyp prep_const prep_typ (raw_abstyp, raw_substtyp) raw_absconsts thy =

   let

     val abstyp = Type.no_tvars (prep_typ thy raw_abstyp);

     val substtyp = Type.no_tvars (prep_typ thy raw_substtyp);

     val absconsts = (map o pairself) (prep_const thy) raw_absconsts;

     val Type (abstyco, tys) = abstyp handle BIND => error ("bad type: " ^ Sign.string_of_typ thy abstyp);

     val typarms = map (fst o dest_TFree) tys handle MATCH => error ("bad type: " ^ Sign.string_of_typ thy abstyp);

     fun mk_index v = 

       let

         val k = find_index (fn w => v = w) typarms;

       in if k = ~1

         then error ("free type variable: " ^ quote v)

         else TFree (string_of_int k, [])

       end;

     val typpat = map_atyps (fn TFree (v, _) => mk_index v) substtyp;

     fun apply_typpat (Type (tyco, tys)) =

           let

             val tys' = map apply_typpat tys;

           in if tyco = abstyco then

             (map_atyps (fn TFree (n, _) => nth tys' (the (Int.fromString n)))) typpat

           else

             Type (tyco, tys')

           end

       | apply_typpat ty = ty;

     val string_of_typ = setmp show_sorts true (Sign.string_of_typ thy);

     fun add_consts (c1, c2) =

       let

         val _ = if CodegenNames.has_nsp CodegenNames.nsp_fun (CodegenNames.const thy c2)

           then ()

           else error ("not a function: " ^ CodegenConsts.string_of_const thy c2);

         val funcgr = CodegenFuncgr.mk_funcgr thy [c1, c2] [];

         val ty_map = CodegenFuncgr.get_func_typs funcgr;

         val ty1 = (apply_typpat o the o AList.lookup CodegenConsts.eq_const ty_map) c1;

         val ty2 = (the o AList.lookup CodegenConsts.eq_const ty_map) c2;

         val _ = if Sign.typ_equiv thy (ty1, ty2) then () else

           error ("Incompatiable type signatures of " ^ CodegenConsts.string_of_const thy c1

             ^ " and " ^ CodegenConsts.string_of_const thy c2 ^ ":\n"

             ^ string_of_typ ty1 ^ "\n" ^ string_of_typ ty2);

       in Consttab.update (c1, c2) end;

     val _ = Code.change thy (K CodegenThingol.empty_code);

   in

     thy

     |> (CodegenPackageData.map o apsnd) (fn (abstypes, abscs) =>

           (abstypes

           |> Symtab.update (abstyco, typpat),

           abscs

           |> fold add_consts absconsts)

        )

   end;

 fun gen_constsubst prep_const raw_constsubsts thy =

   let

     val constsubsts = (map o pairself) (prep_const thy) raw_constsubsts;

     val string_of_typ = setmp show_sorts true (Sign.string_of_typ thy);

     fun add_consts (c1, c2) =

       let

         val _ = if CodegenNames.has_nsp CodegenNames.nsp_fun (CodegenNames.const thy c2)

           then ()

           else error ("not a function: " ^ CodegenConsts.string_of_const thy c2);

         val funcgr = CodegenFuncgr.mk_funcgr thy [c1, c2] [];

         val ty_map = CodegenFuncgr.get_func_typs funcgr;

         val ty1 = (the o AList.lookup CodegenConsts.eq_const ty_map) c1;

         val ty2 = (the o AList.lookup CodegenConsts.eq_const ty_map) c2;

         val _ = if Sign.typ_equiv thy (ty1, ty2) then () else

           error ("Incompatiable type signatures of " ^ CodegenConsts.string_of_const thy c1

             ^ " and " ^ CodegenConsts.string_of_const thy c2 ^ ":\n"

             ^ string_of_typ ty1 ^ "\n" ^ string_of_typ ty2);

       in Consttab.update (c1, c2) end;

     val _ = Code.change thy (K CodegenThingol.empty_code);

   in

     thy

     |> (CodegenPackageData.map o apsnd o apsnd) (fold add_consts constsubsts)

   end;

 val abstyp = gen_abstyp CodegenConsts.norm Sign.certify_typ;

 val abstyp_e = gen_abstyp CodegenConsts.read_const (fn thy => Sign.read_typ (thy, K NONE));

 val constsubst = gen_constsubst CodegenConsts.norm;

 val constsubst_e = gen_constsubst CodegenConsts.read_const;

     val funcgr = CodegenFuncgr.mk_funcgr thy cs rhss;

     val raw_funcgr = CodegenFuncgr.mk_funcgr thy cs rhss;

     val qnaming = NameSpace.qualified_names NameSpace.default_naming

     val cs' = map_filter (Consttab.lookup ((snd o snd o CodegenPackageData.get) thy))

       (CodegenFuncgr.Constgraph.keys raw_funcgr);

     val funcgr = CodegenFuncgr.mk_funcgr thy cs' [];

     val qnaming = NameSpace.qualified_names NameSpace.default_naming;

            (CodegenFuncgr.get_func_typs funcgr)

            (CodegenFuncgr.get_func_typs funcgr);

 fun reader_tyco thy rhss target dep =

 val (codeK, code_abstypeK, code_constsubstK) =

   generate thy rhss (SOME [target]) (SOME dep) (fold_map oooo exprgen_type);

   ("code_gen", "code_abstype", "code_constsubst");

 fun reader_const thy rhss target dep =

   generate thy rhss (SOME [target]) (SOME dep) (fold_map oooo exprgen_term');

 fun zip_list (x::xs) f g =

   f x #-> (fn y => fold_map (fn x => g |-- f x >> pair x) xs

     #-> (fn xys => pair ((x, y) :: xys)));

 fun parse_multi_syntax parse_thing parse_syntax =

   P.and_list1 parse_thing

   #-> (fn things => Scan.repeat1 (P.$$$ "(" |-- P.name :--

       (fn target => zip_list things (parse_syntax target)

         (P.$$$ "and")) --| P.$$$ ")"))

 val syntax_classP =

 val code_abstypeP =

   OuterSyntax.command syntax_classK "define code syntax for class" K.thy_decl (

   OuterSyntax.command code_abstypeK "axiomatic abstypes for code generation" K.thy_decl (

     parse_multi_syntax P.xname

     (P.typ -- P.typ -- Scan.optional (P.$$$ "where" |-- Scan.repeat1

       (fn _ => fn _ => P.string -- Scan.optional (P.$$$ "where" |-- Scan.repeat1

         (P.term --| (P.$$$ "\\<equiv>" || P.$$$ "==") -- P.term)) [])

         (P.term --| (P.$$$ "\\<equiv>" || P.$$$ "==") -- P.string)) [])

     >> (Toplevel.theory o uncurry abstyp_e)

     >> (Toplevel.theory oo fold) (fn (target, syns) =>

           fold (fn (raw_class, syn) => CodegenSerializer.add_syntax_class target raw_class syn) syns)

 val syntax_instP =

 val code_constsubstP =

   OuterSyntax.command syntax_instK "define code syntax for instance" K.thy_decl (

   OuterSyntax.command code_constsubstK "axiomatic constant substitutions for code generation" K.thy_decl (

     parse_multi_syntax (P.xname --| P.$$$ "::" -- P.xname)

     Scan.repeat1 (P.term --| (P.$$$ "\\<equiv>" || P.$$$ "==") -- P.term)

       (fn _ => fn _ => P.name #->

     >> (Toplevel.theory o constsubst_e)

         (fn "-" => Scan.succeed () | _ => Scan.fail_with (fn _ => "\"-\" expected") ()))

     >> (Toplevel.theory oo fold) (fn (target, syns) =>

           fold (fn (raw_inst, ()) => CodegenSerializer.add_syntax_inst target raw_inst) syns)

 val syntax_tycoP =

 val _ = OuterSyntax.add_parsers [codeP, code_abstypeP, code_constsubstP];

   OuterSyntax.command syntax_tycoK "define code syntax for type constructor" K.thy_decl (

     Scan.repeat1 (

       parse_multi_syntax P.xname (CodegenSerializer.parse_syntax_tyco reader_tyco)

     )

     >> (Toplevel.theory o (fold o fold) (fold snd o snd))

   );

 val syntax_constP =

   OuterSyntax.command syntax_constK "define code syntax for constant" K.thy_decl (

     Scan.repeat1 (

       parse_multi_syntax P.term (CodegenSerializer.parse_syntax_const reader_const)

     )

     >> (Toplevel.theory o (fold o fold) (fold snd o snd))

   );

 val _ = OuterSyntax.add_parsers [codeP,

   syntax_classP, syntax_instP, syntax_tycoP, syntax_constP];