added code_abstype and code_constsubst
authorhaftmann
Tue Oct 10 09:17:17 2006 +0200 (2006-10-10)
changeset 2093119d9b78218fd
parent 20930 7ab9fa7d658f
child 20932 e65e1234c9d3
added code_abstype and code_constsubst
etc/isar-keywords-HOL-Nominal.el
etc/isar-keywords-ZF.el
etc/isar-keywords.el
src/Pure/Tools/codegen_package.ML
src/Pure/Tools/codegen_serializer.ML
     1.1 --- a/etc/isar-keywords-HOL-Nominal.el	Mon Oct 09 20:12:45 2006 +0200
     1.2 +++ b/etc/isar-keywords-HOL-Nominal.el	Tue Oct 10 09:17:17 2006 +0200
     1.3 @@ -43,15 +43,16 @@
     1.4      "classes"
     1.5      "classrel"
     1.6      "clear_undos"
     1.7 +    "code_abstype"
     1.8      "code_class"
     1.9      "code_const"
    1.10      "code_constname"
    1.11 +    "code_constsubst"
    1.12      "code_gen"
    1.13      "code_instance"
    1.14      "code_instname"
    1.15      "code_library"
    1.16      "code_module"
    1.17 -    "code_simtype"
    1.18      "code_type"
    1.19      "code_typename"
    1.20      "coinductive"
    1.21 @@ -206,6 +207,7 @@
    1.22      "types_code"
    1.23      "ultimately"
    1.24      "undo"
    1.25 +    "undo_end"
    1.26      "undos_proof"
    1.27      "unfolding"
    1.28      "update_thy"
    1.29 @@ -283,6 +285,7 @@
    1.30      "quit"
    1.31      "redo"
    1.32      "undo"
    1.33 +    "undo_end"
    1.34      "undos_proof"))
    1.35  
    1.36  (defconst isar-keywords-diag
    1.37 @@ -373,9 +376,11 @@
    1.38      "class"
    1.39      "classes"
    1.40      "classrel"
    1.41 +    "code_abstype"
    1.42      "code_class"
    1.43      "code_const"
    1.44      "code_constname"
    1.45 +    "code_constsubst"
    1.46      "code_instance"
    1.47      "code_instname"
    1.48      "code_library"
    1.49 @@ -439,7 +444,6 @@
    1.50  
    1.51  (defconst isar-keywords-theory-goal
    1.52    '("ax_specification"
    1.53 -    "code_simtype"
    1.54      "corollary"
    1.55      "function"
    1.56      "instance"
     2.1 --- a/etc/isar-keywords-ZF.el	Mon Oct 09 20:12:45 2006 +0200
     2.2 +++ b/etc/isar-keywords-ZF.el	Tue Oct 10 09:17:17 2006 +0200
     2.3 @@ -41,15 +41,16 @@
     2.4      "classrel"
     2.5      "clear_undos"
     2.6      "codatatype"
     2.7 +    "code_abstype"
     2.8      "code_class"
     2.9      "code_const"
    2.10      "code_constname"
    2.11 +    "code_constsubst"
    2.12      "code_gen"
    2.13      "code_instance"
    2.14      "code_instname"
    2.15      "code_library"
    2.16      "code_module"
    2.17 -    "code_simtype"
    2.18      "code_type"
    2.19      "code_typename"
    2.20      "coinductive"
    2.21 @@ -193,6 +194,7 @@
    2.22      "types_code"
    2.23      "ultimately"
    2.24      "undo"
    2.25 +    "undo_end"
    2.26      "undos_proof"
    2.27      "unfolding"
    2.28      "update_thy"
    2.29 @@ -269,6 +271,7 @@
    2.30      "quit"
    2.31      "redo"
    2.32      "undo"
    2.33 +    "undo_end"
    2.34      "undos_proof"))
    2.35  
    2.36  (defconst isar-keywords-diag
    2.37 @@ -358,9 +361,11 @@
    2.38      "classes"
    2.39      "classrel"
    2.40      "codatatype"
    2.41 +    "code_abstype"
    2.42      "code_class"
    2.43      "code_const"
    2.44      "code_constname"
    2.45 +    "code_constsubst"
    2.46      "code_instance"
    2.47      "code_instname"
    2.48      "code_library"
    2.49 @@ -417,8 +422,7 @@
    2.50      "inductive_cases"))
    2.51  
    2.52  (defconst isar-keywords-theory-goal
    2.53 -  '("code_simtype"
    2.54 -    "corollary"
    2.55 +  '("corollary"
    2.56      "instance"
    2.57      "interpretation"
    2.58      "lemma"
     3.1 --- a/etc/isar-keywords.el	Mon Oct 09 20:12:45 2006 +0200
     3.2 +++ b/etc/isar-keywords.el	Tue Oct 10 09:17:17 2006 +0200
     3.3 @@ -43,15 +43,16 @@
     3.4      "classes"
     3.5      "classrel"
     3.6      "clear_undos"
     3.7 +    "code_abstype"
     3.8      "code_class"
     3.9      "code_const"
    3.10      "code_constname"
    3.11 +    "code_constsubst"
    3.12      "code_gen"
    3.13      "code_instance"
    3.14      "code_instname"
    3.15      "code_library"
    3.16      "code_module"
    3.17 -    "code_simtype"
    3.18      "code_type"
    3.19      "code_typename"
    3.20      "coinductive"
    3.21 @@ -210,6 +211,7 @@
    3.22      "types_code"
    3.23      "ultimately"
    3.24      "undo"
    3.25 +    "undo_end"
    3.26      "undos_proof"
    3.27      "unfolding"
    3.28      "update_thy"
    3.29 @@ -304,6 +306,7 @@
    3.30      "quit"
    3.31      "redo"
    3.32      "undo"
    3.33 +    "undo_end"
    3.34      "undos_proof"))
    3.35  
    3.36  (defconst isar-keywords-diag
    3.37 @@ -394,9 +397,11 @@
    3.38      "class"
    3.39      "classes"
    3.40      "classrel"
    3.41 +    "code_abstype"
    3.42      "code_class"
    3.43      "code_const"
    3.44      "code_constname"
    3.45 +    "code_constsubst"
    3.46      "code_instance"
    3.47      "code_instname"
    3.48      "code_library"
    3.49 @@ -462,7 +467,6 @@
    3.50  
    3.51  (defconst isar-keywords-theory-goal
    3.52    '("ax_specification"
    3.53 -    "code_simtype"
    3.54      "corollary"
    3.55      "cpodef"
    3.56      "function"
     4.1 --- a/src/Pure/Tools/codegen_package.ML	Mon Oct 09 20:12:45 2006 +0200
     4.2 +++ b/src/Pure/Tools/codegen_package.ML	Tue Oct 10 09:17:17 2006 +0200
     4.3 @@ -35,34 +35,53 @@
     4.4  
     4.5  (* theory data *)
     4.6  
     4.7 +structure Code = CodeDataFun
     4.8 +(struct
     4.9 +  val name = "Pure/code";
    4.10 +  type T = CodegenThingol.code;
    4.11 +  val empty = CodegenThingol.empty_code;
    4.12 +  fun merge _ = CodegenThingol.merge_code;
    4.13 +  fun purge _ NONE _ = CodegenThingol.empty_code
    4.14 +    | purge NONE _ _ = CodegenThingol.empty_code
    4.15 +    | purge (SOME thy) (SOME cs) code =
    4.16 +        let
    4.17 +          val cs_exisiting =
    4.18 +            map_filter (CodegenNames.const_rev thy) (Graph.keys code);
    4.19 +        in
    4.20 +          Graph.del_nodes
    4.21 +            ((Graph.all_succs code
    4.22 +              o map (CodegenNames.const thy)
    4.23 +              o filter (member CodegenConsts.eq_const cs_exisiting)
    4.24 +              ) cs)
    4.25 +            code
    4.26 +        end;
    4.27 +end);
    4.28 +
    4.29  type appgen = theory -> ((sort -> sort) * Sorts.algebra) * Consts.T
    4.30    -> CodegenFuncgr.T
    4.31    -> bool * string list option
    4.32    -> (string * typ) * term list -> CodegenThingol.transact -> iterm * CodegenThingol.transact;
    4.33  
    4.34  type appgens = (int * (appgen * stamp)) Symtab.table;
    4.35 -
    4.36 -fun merge_appgens (x : appgens * appgens) =
    4.37 +val merge_appgens : appgens * appgens -> appgens =
    4.38    Symtab.merge (fn ((bounds1, (_, stamp1)), (bounds2, (_, stamp2))) =>
    4.39 -    bounds1 = bounds2 andalso stamp1 = stamp2) x;
    4.40 +    bounds1 = bounds2 andalso stamp1 = stamp2);
    4.41  
    4.42 -structure Code = CodeDataFun
    4.43 -(struct
    4.44 -  val name = "Pure/code";
    4.45 -  type T = CodegenThingol.code;
    4.46 -  val empty = CodegenThingol.empty_code;
    4.47 -  fun merge _ = CodegenThingol.merge_code;
    4.48 -  fun purge _ _ = CodegenThingol.empty_code;
    4.49 -end);
    4.50 +structure Consttab = CodegenConsts.Consttab;
    4.51 +type abstypes = typ Symtab.table * CodegenConsts.const Consttab.table;
    4.52 +fun merge_abstypes ((typs1, consts1) : abstypes, (typs2, consts2) : abstypes) =
    4.53 +  (Symtab.merge (Type.eq_type Vartab.empty) (typs1, typs2),
    4.54 +    Consttab.merge CodegenConsts.eq_const (consts1, consts2));
    4.55  
    4.56  structure CodegenPackageData = TheoryDataFun
    4.57  (struct
    4.58    val name = "Pure/codegen_package";
    4.59 -  type T = appgens;
    4.60 -  val empty = Symtab.empty;
    4.61 +  type T = appgens * abstypes;
    4.62 +  val empty = (Symtab.empty, (Symtab.empty, Consttab.empty));
    4.63    val copy = I;
    4.64    val extend = I;
    4.65 -  fun merge _ = merge_appgens;
    4.66 +  fun merge _ ((appgens1, abstypes1), (appgens2, abstypes2)) =
    4.67 +    (merge_appgens (appgens1, appgens2), merge_abstypes (abstypes1, abstypes2));
    4.68    fun print _ _ = ();
    4.69  end);
    4.70  
    4.71 @@ -71,13 +90,17 @@
    4.72  
    4.73  (* extraction kernel *)
    4.74  
    4.75 -fun check_strict has_seri x (false, _) =
    4.76 +fun check_strict (false, _) has_seri x =
    4.77        false
    4.78 -  | check_strict has_seri x (_, SOME targets) =
    4.79 +  | check_strict (_, SOME targets) has_seri x =
    4.80        not (has_seri targets x)
    4.81 -  | check_strict has_seri x (true, _) =
    4.82 +  | check_strict (true, _) has_seri x =
    4.83        true;
    4.84  
    4.85 +fun get_abstype thy (tyco, tys) = case Symtab.lookup ((fst o snd o CodegenPackageData.get) thy) tyco
    4.86 + of SOME ty => SOME ((map_atyps (fn TFree (n, _) => nth tys (the (Int.fromString n)))) ty)
    4.87 +  | NONE => NONE;
    4.88 +
    4.89  fun ensure_def_class thy (algbr as ((proj_sort, _), _)) funcgr strct class trns =
    4.90    let
    4.91      val (v, cs) = (ClassPackage.the_consts_sign thy) class;
    4.92 @@ -115,7 +138,7 @@
    4.93              trns
    4.94              |> fail ("No such datatype: " ^ quote tyco)
    4.95      val tyco' = CodegenNames.tyco thy tyco;
    4.96 -    val strict = check_strict (CodegenSerializer.tyco_has_serialization thy) tyco' strct;
    4.97 +    val strict = check_strict strct (CodegenSerializer.tyco_has_serialization thy) tyco';
    4.98    in
    4.99      trns
   4.100      |> tracing (fn _ => "generating type constructor " ^ quote tyco)
   4.101 @@ -139,10 +162,15 @@
   4.102        ||>> exprgen_type thy algbr funcgr strct t2
   4.103        |-> (fn (t1', t2') => pair (t1' `-> t2'))
   4.104    | exprgen_type thy algbr funcgr strct (Type (tyco, tys)) trns =
   4.105 -      trns
   4.106 -      |> ensure_def_tyco thy algbr funcgr strct tyco
   4.107 -      ||>> fold_map (exprgen_type thy algbr funcgr strct) tys
   4.108 -      |-> (fn (tyco, tys) => pair (tyco `%% tys));
   4.109 +      case get_abstype thy (tyco, tys)
   4.110 +       of SOME ty =>
   4.111 +            trns
   4.112 +            |> exprgen_type thy algbr funcgr strct ty
   4.113 +        | NONE =>
   4.114 +            trns
   4.115 +            |> ensure_def_tyco thy algbr funcgr strct tyco
   4.116 +            ||>> fold_map (exprgen_type thy algbr funcgr strct) tys
   4.117 +            |-> (fn (tyco, tys) => pair (tyco `%% tys));
   4.118  
   4.119  exception CONSTRAIN of (string * typ) * typ;
   4.120  
   4.121 @@ -239,7 +267,8 @@
   4.122        |> ensure_def_class thy algbr funcgr strct ((the o AxClass.class_of_param thy) c)
   4.123        |-> (fn _ => succeed CodegenThingol.Bot);
   4.124      fun defgen_fun trns =
   4.125 -      case CodegenFuncgr.get_funcs funcgr (c, tys)
   4.126 +      case CodegenFuncgr.get_funcs funcgr
   4.127 +        (perhaps (Consttab.lookup ((snd o snd o CodegenPackageData.get) thy)) (c, tys))
   4.128         of eq_thms as eq_thm :: _ =>
   4.129              let
   4.130                val msg = cat_lines ("generating code for theorems " :: map string_of_thm eq_thms);
   4.131 @@ -271,7 +300,7 @@
   4.132        else if CodegenNames.has_nsp CodegenNames.nsp_dtco c'
   4.133        then defgen_datatypecons
   4.134        else error ("Illegal shallow name space for constant: " ^ quote c');
   4.135 -    val strict = check_strict (CodegenSerializer.const_has_serialization thy) c' strct;
   4.136 +    val strict = check_strict strct (CodegenSerializer.const_has_serialization thy) c';
   4.137    in
   4.138      trns
   4.139      |> tracing (fn _ => "generating constant "
   4.140 @@ -318,7 +347,7 @@
   4.141    |-> (fn (((c, ty), iss), ts) =>
   4.142           pair (IConst (c, (iss, ty)) `$$ ts))
   4.143  and select_appgen thy algbr funcgr strct ((c, ty), ts) trns =
   4.144 -  case Symtab.lookup (CodegenPackageData.get thy) c
   4.145 +  case Symtab.lookup (fst (CodegenPackageData.get thy)) c
   4.146     of SOME (i, (appgen, _)) =>
   4.147          if length ts < i then
   4.148            let
   4.149 @@ -415,8 +444,96 @@
   4.150  
   4.151  fun add_appconst (c, appgen) thy =
   4.152    let
   4.153 -    val i = (length o fst o strip_type o Sign.the_const_type thy) c
   4.154 -  in CodegenPackageData.map (Symtab.update (c, (i, (appgen, stamp ())))) thy end;
   4.155 +    val i = (length o fst o strip_type o Sign.the_const_type thy) c;
   4.156 +    val _ = Code.change thy (K CodegenThingol.empty_code);
   4.157 +  in
   4.158 +    (CodegenPackageData.map o apfst)
   4.159 +      (Symtab.update (c, (i, (appgen, stamp ())))) thy
   4.160 +  end;
   4.161 +
   4.162 +
   4.163 +
   4.164 +(** abstype and constsubst interface **)
   4.165 +
   4.166 +fun gen_abstyp prep_const prep_typ (raw_abstyp, raw_substtyp) raw_absconsts thy =
   4.167 +  let
   4.168 +    val abstyp = Type.no_tvars (prep_typ thy raw_abstyp);
   4.169 +    val substtyp = Type.no_tvars (prep_typ thy raw_substtyp);
   4.170 +    val absconsts = (map o pairself) (prep_const thy) raw_absconsts;
   4.171 +    val Type (abstyco, tys) = abstyp handle BIND => error ("bad type: " ^ Sign.string_of_typ thy abstyp);
   4.172 +    val typarms = map (fst o dest_TFree) tys handle MATCH => error ("bad type: " ^ Sign.string_of_typ thy abstyp);
   4.173 +    fun mk_index v = 
   4.174 +      let
   4.175 +        val k = find_index (fn w => v = w) typarms;
   4.176 +      in if k = ~1
   4.177 +        then error ("free type variable: " ^ quote v)
   4.178 +        else TFree (string_of_int k, [])
   4.179 +      end;
   4.180 +    val typpat = map_atyps (fn TFree (v, _) => mk_index v) substtyp;
   4.181 +    fun apply_typpat (Type (tyco, tys)) =
   4.182 +          let
   4.183 +            val tys' = map apply_typpat tys;
   4.184 +          in if tyco = abstyco then
   4.185 +            (map_atyps (fn TFree (n, _) => nth tys' (the (Int.fromString n)))) typpat
   4.186 +          else
   4.187 +            Type (tyco, tys')
   4.188 +          end
   4.189 +      | apply_typpat ty = ty;
   4.190 +    val string_of_typ = setmp show_sorts true (Sign.string_of_typ thy);
   4.191 +    fun add_consts (c1, c2) =
   4.192 +      let
   4.193 +        val _ = if CodegenNames.has_nsp CodegenNames.nsp_fun (CodegenNames.const thy c2)
   4.194 +          then ()
   4.195 +          else error ("not a function: " ^ CodegenConsts.string_of_const thy c2);
   4.196 +        val funcgr = CodegenFuncgr.mk_funcgr thy [c1, c2] [];
   4.197 +        val ty_map = CodegenFuncgr.get_func_typs funcgr;
   4.198 +        val ty1 = (apply_typpat o the o AList.lookup CodegenConsts.eq_const ty_map) c1;
   4.199 +        val ty2 = (the o AList.lookup CodegenConsts.eq_const ty_map) c2;
   4.200 +        val _ = if Sign.typ_equiv thy (ty1, ty2) then () else
   4.201 +          error ("Incompatiable type signatures of " ^ CodegenConsts.string_of_const thy c1
   4.202 +            ^ " and " ^ CodegenConsts.string_of_const thy c2 ^ ":\n"
   4.203 +            ^ string_of_typ ty1 ^ "\n" ^ string_of_typ ty2);
   4.204 +      in Consttab.update (c1, c2) end;
   4.205 +    val _ = Code.change thy (K CodegenThingol.empty_code);
   4.206 +  in
   4.207 +    thy
   4.208 +    |> (CodegenPackageData.map o apsnd) (fn (abstypes, abscs) =>
   4.209 +          (abstypes
   4.210 +          |> Symtab.update (abstyco, typpat),
   4.211 +          abscs
   4.212 +          |> fold add_consts absconsts)
   4.213 +       )
   4.214 +  end;
   4.215 +
   4.216 +fun gen_constsubst prep_const raw_constsubsts thy =
   4.217 +  let
   4.218 +    val constsubsts = (map o pairself) (prep_const thy) raw_constsubsts;
   4.219 +    val string_of_typ = setmp show_sorts true (Sign.string_of_typ thy);
   4.220 +    fun add_consts (c1, c2) =
   4.221 +      let
   4.222 +        val _ = if CodegenNames.has_nsp CodegenNames.nsp_fun (CodegenNames.const thy c2)
   4.223 +          then ()
   4.224 +          else error ("not a function: " ^ CodegenConsts.string_of_const thy c2);
   4.225 +        val funcgr = CodegenFuncgr.mk_funcgr thy [c1, c2] [];
   4.226 +        val ty_map = CodegenFuncgr.get_func_typs funcgr;
   4.227 +        val ty1 = (the o AList.lookup CodegenConsts.eq_const ty_map) c1;
   4.228 +        val ty2 = (the o AList.lookup CodegenConsts.eq_const ty_map) c2;
   4.229 +        val _ = if Sign.typ_equiv thy (ty1, ty2) then () else
   4.230 +          error ("Incompatiable type signatures of " ^ CodegenConsts.string_of_const thy c1
   4.231 +            ^ " and " ^ CodegenConsts.string_of_const thy c2 ^ ":\n"
   4.232 +            ^ string_of_typ ty1 ^ "\n" ^ string_of_typ ty2);
   4.233 +      in Consttab.update (c1, c2) end;
   4.234 +    val _ = Code.change thy (K CodegenThingol.empty_code);
   4.235 +  in
   4.236 +    thy
   4.237 +    |> (CodegenPackageData.map o apsnd o apsnd) (fold add_consts constsubsts)
   4.238 +  end;
   4.239 +
   4.240 +val abstyp = gen_abstyp CodegenConsts.norm Sign.certify_typ;
   4.241 +val abstyp_e = gen_abstyp CodegenConsts.read_const (fn thy => Sign.read_typ (thy, K NONE));
   4.242 +
   4.243 +val constsubst = gen_constsubst CodegenConsts.norm;
   4.244 +val constsubst_e = gen_constsubst CodegenConsts.read_const;
   4.245  
   4.246  
   4.247  
   4.248 @@ -424,13 +541,16 @@
   4.249  
   4.250  fun generate thy (cs, rhss) targets init gen it =
   4.251    let
   4.252 -    val funcgr = CodegenFuncgr.mk_funcgr thy cs rhss;
   4.253 -    val qnaming = NameSpace.qualified_names NameSpace.default_naming
   4.254 +    val raw_funcgr = CodegenFuncgr.mk_funcgr thy cs rhss;
   4.255 +    val cs' = map_filter (Consttab.lookup ((snd o snd o CodegenPackageData.get) thy))
   4.256 +      (CodegenFuncgr.Constgraph.keys raw_funcgr);
   4.257 +    val funcgr = CodegenFuncgr.mk_funcgr thy cs' [];
   4.258 +    val qnaming = NameSpace.qualified_names NameSpace.default_naming;
   4.259      val algebr = ClassPackage.operational_algebra thy;
   4.260      val consttab = Consts.empty
   4.261        |> fold (fn (c, ty) => Consts.declare qnaming
   4.262             ((CodegenNames.const thy c, ty), true))
   4.263 -           (CodegenFuncgr.get_func_typs funcgr)
   4.264 +           (CodegenFuncgr.get_func_typs funcgr);
   4.265      val algbr = (algebr, consttab);
   4.266    in   
   4.267      Code.change_yield thy (CodegenThingol.start_transact init (gen thy algbr funcgr
   4.268 @@ -504,30 +624,11 @@
   4.269      (map (serialize' cs code) seris'; ())
   4.270    end;
   4.271  
   4.272 -fun reader_tyco thy rhss target dep =
   4.273 -  generate thy rhss (SOME [target]) (SOME dep) (fold_map oooo exprgen_type);
   4.274 -
   4.275 -fun reader_const thy rhss target dep =
   4.276 -  generate thy rhss (SOME [target]) (SOME dep) (fold_map oooo exprgen_term');
   4.277 -
   4.278 -fun zip_list (x::xs) f g =
   4.279 -  f x #-> (fn y => fold_map (fn x => g |-- f x >> pair x) xs
   4.280 -    #-> (fn xys => pair ((x, y) :: xys)));
   4.281 -
   4.282 -fun parse_multi_syntax parse_thing parse_syntax =
   4.283 -  P.and_list1 parse_thing
   4.284 -  #-> (fn things => Scan.repeat1 (P.$$$ "(" |-- P.name :--
   4.285 -      (fn target => zip_list things (parse_syntax target)
   4.286 -        (P.$$$ "and")) --| P.$$$ ")"))
   4.287 -
   4.288 +val (codeK, code_abstypeK, code_constsubstK) =
   4.289 +  ("code_gen", "code_abstype", "code_constsubst");
   4.290  
   4.291  in
   4.292  
   4.293 -val (codeK,
   4.294 -     syntax_classK, syntax_instK, syntax_tycoK, syntax_constK) =
   4.295 -  ("code_gen",
   4.296 -   "code_class", "code_instance", "code_type", "code_const");
   4.297 -
   4.298  val codeP =
   4.299    OuterSyntax.improper_command codeK "generate and serialize executable code for constants" K.diag (
   4.300      Scan.repeat P.term
   4.301 @@ -537,42 +638,20 @@
   4.302      >> (fn (raw_cs, seris) => Toplevel.keep (code raw_cs seris o Toplevel.theory_of))
   4.303    );
   4.304  
   4.305 -val syntax_classP =
   4.306 -  OuterSyntax.command syntax_classK "define code syntax for class" K.thy_decl (
   4.307 -    parse_multi_syntax P.xname
   4.308 -      (fn _ => fn _ => P.string -- Scan.optional (P.$$$ "where" |-- Scan.repeat1
   4.309 -        (P.term --| (P.$$$ "\\<equiv>" || P.$$$ "==") -- P.string)) [])
   4.310 -    >> (Toplevel.theory oo fold) (fn (target, syns) =>
   4.311 -          fold (fn (raw_class, syn) => CodegenSerializer.add_syntax_class target raw_class syn) syns)
   4.312 -  );
   4.313 -
   4.314 -val syntax_instP =
   4.315 -  OuterSyntax.command syntax_instK "define code syntax for instance" K.thy_decl (
   4.316 -    parse_multi_syntax (P.xname --| P.$$$ "::" -- P.xname)
   4.317 -      (fn _ => fn _ => P.name #->
   4.318 -        (fn "-" => Scan.succeed () | _ => Scan.fail_with (fn _ => "\"-\" expected") ()))
   4.319 -    >> (Toplevel.theory oo fold) (fn (target, syns) =>
   4.320 -          fold (fn (raw_inst, ()) => CodegenSerializer.add_syntax_inst target raw_inst) syns)
   4.321 +val code_abstypeP =
   4.322 +  OuterSyntax.command code_abstypeK "axiomatic abstypes for code generation" K.thy_decl (
   4.323 +    (P.typ -- P.typ -- Scan.optional (P.$$$ "where" |-- Scan.repeat1
   4.324 +        (P.term --| (P.$$$ "\\<equiv>" || P.$$$ "==") -- P.term)) [])
   4.325 +    >> (Toplevel.theory o uncurry abstyp_e)
   4.326    );
   4.327  
   4.328 -val syntax_tycoP =
   4.329 -  OuterSyntax.command syntax_tycoK "define code syntax for type constructor" K.thy_decl (
   4.330 -    Scan.repeat1 (
   4.331 -      parse_multi_syntax P.xname (CodegenSerializer.parse_syntax_tyco reader_tyco)
   4.332 -    )
   4.333 -    >> (Toplevel.theory o (fold o fold) (fold snd o snd))
   4.334 +val code_constsubstP =
   4.335 +  OuterSyntax.command code_constsubstK "axiomatic constant substitutions for code generation" K.thy_decl (
   4.336 +    Scan.repeat1 (P.term --| (P.$$$ "\\<equiv>" || P.$$$ "==") -- P.term)
   4.337 +    >> (Toplevel.theory o constsubst_e)
   4.338    );
   4.339  
   4.340 -val syntax_constP =
   4.341 -  OuterSyntax.command syntax_constK "define code syntax for constant" K.thy_decl (
   4.342 -    Scan.repeat1 (
   4.343 -      parse_multi_syntax P.term (CodegenSerializer.parse_syntax_const reader_const)
   4.344 -    )
   4.345 -    >> (Toplevel.theory o (fold o fold) (fold snd o snd))
   4.346 -  );
   4.347 -
   4.348 -val _ = OuterSyntax.add_parsers [codeP,
   4.349 -  syntax_classP, syntax_instP, syntax_tycoP, syntax_constP];
   4.350 +val _ = OuterSyntax.add_parsers [codeP, code_abstypeP, code_constsubstP];
   4.351  
   4.352  end; (* local *)
   4.353  
     5.1 --- a/src/Pure/Tools/codegen_serializer.ML	Mon Oct 09 20:12:45 2006 +0200
     5.2 +++ b/src/Pure/Tools/codegen_serializer.ML	Tue Oct 10 09:17:17 2006 +0200
     5.3 @@ -9,35 +9,7 @@
     5.4  signature CODEGEN_SERIALIZER =
     5.5  sig
     5.6    include BASIC_CODEGEN_THINGOL;
     5.7 -  val get_serializer: theory -> string * Args.T list
     5.8 -    -> string list option -> CodegenThingol.code -> unit;
     5.9 -  val eval_verbose: bool ref;
    5.10 -  val eval_term: theory ->
    5.11 -    (string * 'a option ref) * CodegenThingol.iterm -> CodegenThingol.code
    5.12 -    -> 'a;
    5.13 -  val const_has_serialization: theory -> string list -> string -> bool;
    5.14 -  val tyco_has_serialization: theory -> string list -> string -> bool;
    5.15 -  val add_syntax_class:
    5.16 -    string -> string -> string * (string * string) list  -> theory -> theory;
    5.17 -  val add_syntax_inst: string -> (string * string) -> theory -> theory;
    5.18 -  val parse_syntax_tyco: (theory
    5.19 -           -> CodegenConsts.const list * (string * typ) list
    5.20 -              -> string
    5.21 -                 -> CodegenNames.tyco
    5.22 -                    -> typ list -> CodegenThingol.itype list)
    5.23 -          -> Symtab.key
    5.24 -             -> xstring
    5.25 -                -> OuterParse.token list
    5.26 -                   -> (theory -> theory) * OuterParse.token list;
    5.27 -  val parse_syntax_const: (theory
    5.28 -           -> CodegenConsts.const list * (string * typ) list
    5.29 -              -> string
    5.30 -                 -> CodegenNames.const
    5.31 -                    -> term list -> CodegenThingol.iterm list)
    5.32 -          -> Symtab.key
    5.33 -             -> string
    5.34 -                -> OuterParse.token list
    5.35 -                   -> (theory -> theory) * OuterParse.token list;
    5.36 +
    5.37    val add_pretty_list: string -> string -> string -> (Pretty.T list -> Pretty.T)
    5.38     -> ((string -> string) * (string -> string)) option -> int * string
    5.39     -> theory -> theory;
    5.40 @@ -45,11 +17,20 @@
    5.41     -> (string -> string) -> (string -> string) -> string -> theory -> theory;
    5.42    val add_undefined: string -> string -> string -> theory -> theory;
    5.43  
    5.44 -  type fixity;
    5.45    type serializer;
    5.46    val add_serializer : string * serializer -> theory -> theory;
    5.47    val ml_from_thingol: serializer;
    5.48    val hs_from_thingol: serializer;
    5.49 +  val get_serializer: theory -> string * Args.T list
    5.50 +    -> string list option -> CodegenThingol.code -> unit;
    5.51 +
    5.52 +  val const_has_serialization: theory -> string list -> string -> bool;
    5.53 +  val tyco_has_serialization: theory -> string list -> string -> bool;
    5.54 +
    5.55 +  val eval_verbose: bool ref;
    5.56 +  val eval_term: theory ->
    5.57 +    (string * 'a option ref) * CodegenThingol.iterm -> CodegenThingol.code
    5.58 +    -> 'a;
    5.59  end;
    5.60  
    5.61  structure CodegenSerializer: CODEGEN_SERIALIZER =
    5.62 @@ -120,8 +101,7 @@
    5.63  
    5.64  datatype 'a mixfix =
    5.65      Arg of fixity
    5.66 -  | Pretty of Pretty.T
    5.67 -  | Quote of 'a;
    5.68 +  | Pretty of Pretty.T;
    5.69  
    5.70  fun fillin_mixfix fxy_this ms fxy_ctxt pr args =
    5.71    let
    5.72 @@ -131,8 +111,6 @@
    5.73            pr fxy a :: fillin ms args
    5.74        | fillin (Pretty p :: ms) args =
    5.75            p :: fillin ms args
    5.76 -      | fillin (Quote q :: ms) args =
    5.77 -          pr BR q :: fillin ms args
    5.78        | fillin [] _ =
    5.79            error ("Inconsistent mixfix: too many arguments")
    5.80        | fillin _ [] =
    5.81 @@ -146,44 +124,40 @@
    5.82      val r = case x of R => fixity
    5.83                      | _ => INFX (i, X);
    5.84    in
    5.85 -    pair [Arg l, (Pretty o Pretty.brk) 1, (Pretty o str) s, (Pretty o Pretty.brk) 1, Arg r]
    5.86 +    [Arg l, (Pretty o Pretty.brk) 1, (Pretty o str) s, (Pretty o Pretty.brk) 1, Arg r]
    5.87    end;
    5.88  
    5.89 -fun parse_mixfix reader s ctxt =
    5.90 +fun parse_mixfix s =
    5.91    let
    5.92 -    fun sym s = Scan.lift ($$ s);
    5.93 -    fun lift_reader ctxt s =
    5.94 -      ctxt
    5.95 -      |> reader s
    5.96 -      |-> (fn x => pair (Quote x));
    5.97 -    val sym_any = Scan.lift (Scan.one Symbol.not_eof);
    5.98 +    val sym_any = Scan.one Symbol.not_eof;
    5.99      val parse = Scan.repeat (
   5.100 -         (sym "_" -- sym "_" >> K (Arg NOBR))
   5.101 -      || (sym "_" >> K (Arg BR))
   5.102 -      || (sym "/" |-- Scan.repeat (sym " ") >> (Pretty o Pretty.brk o length))
   5.103 -      || Scan.depend (fn ctxt => $$ "{" |-- $$ "*" |-- Scan.repeat1
   5.104 -           (   $$ "'" |-- Scan.one Symbol.not_eof
   5.105 -            || Scan.unless ($$ "*" -- $$ "}") (Scan.one Symbol.not_eof)) --|
   5.106 -         $$ "*" --| $$ "}" >> (implode #> lift_reader ctxt #> swap))
   5.107 +         ($$ "_" -- $$ "_" >> K (Arg NOBR))
   5.108 +      || ($$ "_" >> K (Arg BR))
   5.109 +      || ($$ "/" |-- Scan.repeat ($$ " ") >> (Pretty o Pretty.brk o length))
   5.110        || (Scan.repeat1
   5.111 -           (   sym "'" |-- sym_any
   5.112 -            || Scan.unless (sym "_" || sym "?" || sym "/" || sym "{" |-- sym "*")
   5.113 +           (   $$ "'" |-- sym_any
   5.114 +            || Scan.unless ($$ "_" || $$ "/")
   5.115                   sym_any) >> (Pretty o str o implode)));
   5.116 -  in case Scan.finite' Symbol.stopper parse (ctxt, Symbol.explode s)
   5.117 -   of (p, (ctxt, [])) => (p, ctxt)
   5.118 +  in case Scan.finite Symbol.stopper parse (Symbol.explode s)
   5.119 +   of (p, []) => p
   5.120      | _ => error ("Malformed mixfix annotation: " ^ quote s)
   5.121    end;
   5.122  
   5.123 -fun parse_syntax num_args reader =
   5.124 +fun parse_syntax num_args =
   5.125    let
   5.126      fun is_arg (Arg _) = true
   5.127        | is_arg _ = false;
   5.128 -    fun parse_nonatomic s ctxt =
   5.129 -      case parse_mixfix reader s ctxt
   5.130 -       of ([Pretty _], _) =>
   5.131 +    fun parse_nonatomic s =
   5.132 +      case parse_mixfix s
   5.133 +       of [Pretty _] =>
   5.134              error ("Mixfix contains just one pretty element; either declare as "
   5.135                ^ quote atomK ^ " or consider adding a break")
   5.136          | x => x;
   5.137 +    fun mk fixity mfx ctxt =
   5.138 +      let
   5.139 +        val i = (length o List.filter is_arg) mfx;
   5.140 +        val _ = if i > num_args ctxt then error "Too many arguments in code syntax" else ();
   5.141 +      in (i, fillin_mixfix fixity mfx) end;
   5.142      val parse = (
   5.143             OuterParse.$$$ infixK  |-- OuterParse.nat
   5.144              >> (fn i => (parse_infix (INFX (i, X)), INFX (i, X)))
   5.145 @@ -191,19 +165,11 @@
   5.146              >> (fn i => (parse_infix (INFX (i, L)), INFX (i, L)))
   5.147          || OuterParse.$$$ infixrK |-- OuterParse.nat
   5.148              >> (fn i => (parse_infix (INFX (i, R)), INFX (i, R)))
   5.149 -        || OuterParse.$$$ atomK |-- pair (parse_mixfix reader, NOBR)
   5.150 +        || OuterParse.$$$ atomK |-- pair (parse_mixfix, NOBR)
   5.151          || pair (parse_nonatomic, BR)
   5.152        ) -- OuterParse.string >> (fn ((p, fxy), s) => (p s, fxy));
   5.153 -    fun mk fixity mfx ctxt =
   5.154 -      let
   5.155 -        val i = (length o List.filter is_arg) mfx;
   5.156 -        val _ = if i > num_args ctxt then error "Too many arguments in code syntax" else ();
   5.157 -      in ((i, fillin_mixfix fixity mfx), ctxt) end;
   5.158    in
   5.159 -    parse
   5.160 -    #-> (fn (mfx_reader, fixity) =>
   5.161 -      pair (mfx_reader #-> (fn mfx => (mk fixity mfx)))
   5.162 -    )
   5.163 +    parse #-> (fn (mfx, fixity) => pair (mk fixity mfx))
   5.164    end;
   5.165  
   5.166  
   5.167 @@ -858,7 +824,7 @@
   5.168                ) classop_defs)
   5.169              ]
   5.170            end |> SOME
   5.171 -  in pr_def def end;
   5.172 +  in Pretty.setmp_margin 999999 pr_def def end;
   5.173  
   5.174  
   5.175  (** generic abstract serializer **)
   5.176 @@ -1320,138 +1286,6 @@
   5.177    end;
   5.178  
   5.179  
   5.180 -(** LEGACY DIAGNOSIS **)
   5.181 -
   5.182 -local
   5.183 -
   5.184 -open CodegenThingol;
   5.185 -
   5.186 -in
   5.187 -
   5.188 -val pretty_typparms =
   5.189 -  Pretty.list "(" ")" o Pretty.commas o map (fn (v, sort) => (Pretty.block o Pretty.breaks)
   5.190 -    [Pretty.str v, Pretty.str "::", Pretty.enum "&" "" "" (map Pretty.str sort)]);
   5.191 -
   5.192 -fun pretty_itype (tyco `%% tys) =
   5.193 -      Pretty.enum "" "(" ")" (Pretty.str tyco :: map pretty_itype tys)
   5.194 -  | pretty_itype (ty1 `-> ty2) =
   5.195 -      Pretty.enum "" "(" ")" [pretty_itype ty1, Pretty.str "->", pretty_itype ty2]
   5.196 -  | pretty_itype (ITyVar v) =
   5.197 -      Pretty.str v;
   5.198 -
   5.199 -fun pretty_iterm (IConst (c, _)) =
   5.200 -      Pretty.str c
   5.201 -  | pretty_iterm (IVar v) =
   5.202 -      Pretty.str ("?" ^ v)
   5.203 -  | pretty_iterm (t1 `$ t2) =
   5.204 -      (Pretty.enclose "(" ")" o Pretty.breaks)
   5.205 -        [pretty_iterm t1, pretty_iterm t2]
   5.206 -  | pretty_iterm ((v, ty) `|-> t) =
   5.207 -      (Pretty.enclose "(" ")" o Pretty.breaks)
   5.208 -        [Pretty.str v, Pretty.str "::", pretty_itype ty, Pretty.str "|->", pretty_iterm t]
   5.209 -  | pretty_iterm (INum (n, _)) =
   5.210 -      (Pretty.str o IntInf.toString) n
   5.211 -  | pretty_iterm (IChar (h, _)) =
   5.212 -      (Pretty.str o quote) h
   5.213 -  | pretty_iterm (ICase (((t, _), bs), _)) =
   5.214 -      (Pretty.enclose "(" ")" o Pretty.breaks) [
   5.215 -        Pretty.str "case",
   5.216 -        pretty_iterm t,
   5.217 -        Pretty.enclose "(" ")" (map (fn (p, t) =>
   5.218 -          (Pretty.block o Pretty.breaks) [
   5.219 -            pretty_iterm p,
   5.220 -            Pretty.str "=>",
   5.221 -            pretty_iterm t
   5.222 -          ]
   5.223 -        ) bs)
   5.224 -      ];
   5.225 -
   5.226 -fun pretty_def Bot =
   5.227 -      Pretty.str "<Bot>"
   5.228 -  | pretty_def (Fun (eqs, (vs, ty))) =
   5.229 -      Pretty.enum " |" "" "" (
   5.230 -        map (fn (ps, body) =>
   5.231 -          Pretty.block [
   5.232 -            Pretty.enum "," "[" "]" (map pretty_iterm ps),
   5.233 -            Pretty.str " |->",
   5.234 -            Pretty.brk 1,
   5.235 -            pretty_iterm body,
   5.236 -            Pretty.str "::",
   5.237 -            pretty_typparms vs,
   5.238 -            Pretty.str "/",
   5.239 -            pretty_itype ty
   5.240 -          ]) eqs
   5.241 -        )
   5.242 -  | pretty_def (Datatype (vs, cs)) =
   5.243 -      Pretty.block [
   5.244 -        pretty_typparms vs,
   5.245 -        Pretty.str " |=> ",
   5.246 -        Pretty.enum " |" "" ""
   5.247 -          (map (fn (c, tys) => (Pretty.block o Pretty.breaks)
   5.248 -            (Pretty.str c :: map pretty_itype tys)) cs)
   5.249 -      ]
   5.250 -  | pretty_def (Datatypecons dtname) =
   5.251 -      Pretty.str ("cons " ^ dtname)
   5.252 -  | pretty_def (Class (supcls, (v, mems))) =
   5.253 -      Pretty.block [
   5.254 -        Pretty.str ("class var " ^ v ^ " extending "),
   5.255 -        Pretty.enum "," "[" "]" (map Pretty.str supcls),
   5.256 -        Pretty.str " with ",
   5.257 -        Pretty.enum "," "[" "]"
   5.258 -          (map (fn (m, ty) => Pretty.block
   5.259 -            [Pretty.str (m ^ "::"), pretty_itype ty]) mems)
   5.260 -      ]
   5.261 -  | pretty_def (Classmember clsname) =
   5.262 -      Pretty.block [
   5.263 -        Pretty.str "class member belonging to ",
   5.264 -        Pretty.str clsname
   5.265 -      ]
   5.266 -  | pretty_def (Classinst ((clsname, (tyco, arity)), _)) =
   5.267 -      Pretty.block [
   5.268 -        Pretty.str "class instance (",
   5.269 -        Pretty.str clsname,
   5.270 -        Pretty.str ", (",
   5.271 -        Pretty.str tyco,
   5.272 -        Pretty.str ", ",
   5.273 -        Pretty.enum "," "[" "]" (map (Pretty.enum "," "{" "}" o
   5.274 -          map Pretty.str o snd) arity),
   5.275 -        Pretty.str "))"
   5.276 -      ];
   5.277 -
   5.278 -fun pretty_module code =
   5.279 -  Pretty.chunks (map (fn (name, def) => Pretty.block
   5.280 -    [Pretty.str name, Pretty.str " :=", Pretty.brk 1, pretty_def def])
   5.281 -    (AList.make (Graph.get_node code) (Graph.strong_conn code |> flat |> rev)));
   5.282 -
   5.283 -fun pretty_deps code =
   5.284 -  let
   5.285 -    fun one_node key =
   5.286 -      let
   5.287 -        val preds_ = Graph.imm_preds code key;
   5.288 -        val succs_ = Graph.imm_succs code key;
   5.289 -        val mutbs = gen_inter (op =) (preds_, succs_);
   5.290 -        val preds = subtract (op =) mutbs preds_;
   5.291 -        val succs = subtract (op =) mutbs succs_;
   5.292 -      in
   5.293 -        (Pretty.block o Pretty.fbreaks) (
   5.294 -          Pretty.str key
   5.295 -          :: map (fn s => Pretty.str ("<-> " ^ s)) mutbs
   5.296 -          @ map (fn s => Pretty.str ("<-- " ^ s)) preds
   5.297 -          @ map (fn s => Pretty.str ("--> " ^ s)) succs
   5.298 -        )
   5.299 -      end
   5.300 -  in
   5.301 -    code
   5.302 -    |> Graph.strong_conn
   5.303 -    |> flat
   5.304 -    |> rev
   5.305 -    |> map one_node
   5.306 -    |> Pretty.chunks
   5.307 -  end;
   5.308 -
   5.309 -end; (*local*)
   5.310 -
   5.311 -
   5.312  
   5.313  (** theory data **)
   5.314  
   5.315 @@ -1603,7 +1437,7 @@
   5.316  
   5.317  
   5.318  
   5.319 -(** target syntax interfaces **)
   5.320 +(** ML and toplevel interface **)
   5.321  
   5.322  local
   5.323  
   5.324 @@ -1675,26 +1509,26 @@
   5.325      val cs'' = map (CodegenConsts.norm_of_typ thy) cs';
   5.326    in AList.make (CodegenNames.const thy) cs'' end;
   5.327  
   5.328 -fun read_quote reader consts_of target get_init gen raw_it thy =
   5.329 -  let
   5.330 -    val it = reader thy raw_it;
   5.331 -    val cs = consts_of thy it;
   5.332 -  in
   5.333 -    gen thy cs target (get_init thy) [it]
   5.334 -    |> (fn [it'] => (it', thy))
   5.335 -  end;
   5.336 +fun parse_quote num_of consts_of target get_init adder =
   5.337 +  parse_syntax num_of #-> (fn mfx => pair (fn thy => adder target (mfx thy) thy));
   5.338 +
   5.339 +fun zip_list (x::xs) f g =
   5.340 +  f x #-> (fn y => fold_map (fn x => g |-- f x >> pair x) xs
   5.341 +    #-> (fn xys => pair ((x, y) :: xys)));
   5.342  
   5.343 -fun parse_quote num_of reader consts_of target get_init gen adder =
   5.344 -  parse_syntax num_of
   5.345 -    (read_quote reader consts_of target get_init gen)
   5.346 -  #-> (fn modifier => pair (modifier #-> adder target));
   5.347 +structure P = OuterParse
   5.348 +and K = OuterKeyword
   5.349  
   5.350 -in
   5.351 +fun parse_multi_syntax parse_thing parse_syntax =
   5.352 +  P.and_list1 parse_thing
   5.353 +  #-> (fn things => Scan.repeat1 (P.$$$ "(" |-- P.name :--
   5.354 +      (fn target => zip_list things (parse_syntax target)
   5.355 +        (P.$$$ "and")) --| P.$$$ ")"))
   5.356  
   5.357  val add_syntax_class = gen_add_syntax_class ClassPackage.read_class CodegenConsts.read_const;
   5.358  val add_syntax_inst = gen_add_syntax_inst ClassPackage.read_class read_type;
   5.359  
   5.360 -fun parse_syntax_tyco generate target raw_tyco  =
   5.361 +fun parse_syntax_tyco target raw_tyco  =
   5.362    let
   5.363      fun intern thy = read_type thy raw_tyco;
   5.364      fun num_of thy = Sign.arity_number thy (intern thy);
   5.365 @@ -1702,20 +1536,61 @@
   5.366      fun read_typ thy =
   5.367        Sign.read_typ (thy, K NONE);
   5.368    in
   5.369 -    parse_quote num_of read_typ ((K o K) ([], [])) target idf_of generate
   5.370 +    parse_quote num_of ((K o K) ([], [])) target idf_of
   5.371        (gen_add_syntax_tyco read_type raw_tyco)
   5.372    end;
   5.373  
   5.374 -fun parse_syntax_const generate target raw_const =
   5.375 +fun parse_syntax_const target raw_const =
   5.376    let
   5.377      fun intern thy = CodegenConsts.read_const thy raw_const;
   5.378      fun num_of thy = (length o fst o strip_type o Sign.the_const_type thy o fst o intern) thy;
   5.379      fun idf_of thy = (CodegenNames.const thy o intern) thy;
   5.380    in
   5.381 -    parse_quote num_of Sign.read_term CodegenConsts.consts_of target idf_of generate
   5.382 +    parse_quote num_of CodegenConsts.consts_of target idf_of
   5.383        (gen_add_syntax_const CodegenConsts.read_const raw_const)
   5.384    end;
   5.385  
   5.386 +val (code_classK, code_instanceK, code_typeK, code_constK) =
   5.387 +  ("code_class", "code_instance", "code_type", "code_const");
   5.388 +
   5.389 +in
   5.390 +
   5.391 +val code_classP =
   5.392 +  OuterSyntax.command code_classK "define code syntax for class" K.thy_decl (
   5.393 +    parse_multi_syntax P.xname
   5.394 +      (fn _ => fn _ => P.string -- Scan.optional (P.$$$ "where" |-- Scan.repeat1
   5.395 +        (P.term --| (P.$$$ "\\<equiv>" || P.$$$ "==") -- P.string)) [])
   5.396 +    >> (Toplevel.theory oo fold) (fn (target, syns) =>
   5.397 +          fold (fn (raw_class, syn) => add_syntax_class target raw_class syn) syns)
   5.398 +  );
   5.399 +
   5.400 +val code_instanceP =
   5.401 +  OuterSyntax.command code_instanceK "define code syntax for instance" K.thy_decl (
   5.402 +    parse_multi_syntax (P.xname --| P.$$$ "::" -- P.xname)
   5.403 +      (fn _ => fn _ => P.name #->
   5.404 +        (fn "-" => Scan.succeed () | _ => Scan.fail_with (fn _ => "\"-\" expected") ()))
   5.405 +    >> (Toplevel.theory oo fold) (fn (target, syns) =>
   5.406 +          fold (fn (raw_inst, ()) => add_syntax_inst target raw_inst) syns)
   5.407 +  );
   5.408 +
   5.409 +val code_typeP =
   5.410 +  OuterSyntax.command code_typeK "define code syntax for type constructor" K.thy_decl (
   5.411 +    Scan.repeat1 (
   5.412 +      parse_multi_syntax P.xname parse_syntax_tyco
   5.413 +    )
   5.414 +    >> (Toplevel.theory o (fold o fold) (fold snd o snd))
   5.415 +  );
   5.416 +
   5.417 +val code_constP =
   5.418 +  OuterSyntax.command code_constK "define code syntax for constant" K.thy_decl (
   5.419 +    Scan.repeat1 (
   5.420 +      parse_multi_syntax P.term parse_syntax_const
   5.421 +    )
   5.422 +    >> (Toplevel.theory o (fold o fold) (fold snd o snd))
   5.423 +  );
   5.424 +
   5.425 +val _ = OuterSyntax.add_parsers [code_classP, code_instanceP, code_typeP, code_constP];
   5.426 +
   5.427  fun add_pretty_list target nill cons mk_list mk_char_string target_cons thy =
   5.428    let
   5.429      val [(_, nil''), (cons', cons'')] = idfs_of_const_names thy [nill, cons];