src/Pure/Tools/codegen_serializer.ML

-    (*  Title:      Pure/Tools/codegen_serializer.ML
+(*  Title:      Pure/Tools/codegen_serializer.ML
     ID:         $Id$
     Author:     Florian Haftmann, TU Muenchen
 
 Serializer from intermediate language ("Thin-gol") to
 target languages (like SML or Haskell).
 *)
 
 signature CODEGEN_SERIALIZER =
 sig
   include BASIC_CODEGEN_THINGOL;
+
+  val add_syntax_class: string -> class
+    -> (string * ((string * typ list) * string) list) option -> theory -> theory;
+  val add_syntax_inst: string -> string * class -> bool -> theory -> theory;
+  val add_syntax_tycoP: string -> string -> OuterParse.token list
+    -> (theory -> theory) * OuterParse.token list;
+  val add_syntax_constP: string -> string -> OuterParse.token list
+    -> (theory -> theory) * OuterParse.token list;
 
   val add_pretty_list: string -> string -> string -> (Pretty.T list -> Pretty.T)
    -> ((string -> string) * (string -> string)) option -> int * string
    -> theory -> theory;
   val add_pretty_ml_string: string -> string -> string -> string

   val eval_term: theory -> (theory -> string -> string) -> CodegenThingol.code
     -> (string * 'a option ref) * CodegenThingol.iterm -> 'a;
   val code_width: int ref;
 end;
 
-structure CodegenSerializer: CODEGEN_SERIALIZER =
+structure CodegenSerializer : CODEGEN_SERIALIZER =
 struct
 
 open BasicCodegenThingol;
 val tracing = CodegenThingol.tracing;
 

       thy
       |> (map_syntax_exprs target o apsnd o apsnd)
            (Symtab.delete_safe c')
   end;
 
+fun cert_class thy class =
+  let
+    val _ = AxClass.get_definition thy class;
+  in class end;
+
 fun read_class thy raw_class =
   let
     val class = Sign.intern_class thy raw_class;
     val _ = AxClass.get_definition thy class;
   in class end;
 
-fun read_type thy raw_tyco =
+fun cert_tyco thy tyco =
+  let
+    val _ = if Sign.declared_tyname thy tyco then ()
+      else error ("No such type constructor: " ^ quote tyco);
+  in tyco end;
+
+fun read_tyco thy raw_tyco =
   let
     val tyco = Sign.intern_type thy raw_tyco;
     val _ = if Sign.declared_tyname thy tyco then ()
       else error ("No such type constructor: " ^ quote raw_tyco);
   in tyco end;

           (no_bindings (SOME (parse_infix fst (L, 1) ">>=")))
     |> gen_add_syntax_const (K I) target_Haskell c_kbind'
           (no_bindings (SOME (parse_infix fst (L, 1) ">>")))
   end;
 
-val add_syntax_class = gen_add_syntax_class read_class CodegenConsts.read_const;
-val add_syntax_inst = gen_add_syntax_inst read_class read_type;
-val add_syntax_tyco = gen_add_syntax_tyco read_type;
-val add_syntax_const = gen_add_syntax_const CodegenConsts.read_const;
-
 fun add_reserved target =
   map_reserveds target o insert (op =);
 
 fun add_modl_alias target =
   map_syntax_modls target o apfst o Symtab.update o apsnd CodegenNames.check_modulename;

   ("code_class", "code_instance", "code_type", "code_const", "code_monad",
     "code_reserved", "code_modulename", "code_moduleprolog");
 
 in
 
+val parse_syntax = parse_syntax;
+
+val add_syntax_class = gen_add_syntax_class cert_class (K I);
+val add_syntax_inst = gen_add_syntax_inst cert_class cert_tyco;
+val add_syntax_tyco = gen_add_syntax_tyco cert_tyco;
+val add_syntax_const = gen_add_syntax_const (K I);
+
+val add_syntax_class_cmd = gen_add_syntax_class read_class CodegenConsts.read_const;
+val add_syntax_inst_cmd = gen_add_syntax_inst read_class read_tyco;
+val add_syntax_tyco_cmd = gen_add_syntax_tyco read_tyco;
+val add_syntax_const_cmd = gen_add_syntax_const CodegenConsts.read_const;
+
+fun add_syntax_tycoP target tyco = parse_syntax I >> add_syntax_tyco_cmd target tyco;
+fun add_syntax_constP target c = parse_syntax fst >> (add_syntax_const_cmd target c o no_bindings);
+
 fun add_pretty_list target nill cons mk_list mk_char_string target_cons thy =
   let
     val (_, nil'') = idfs_of_const thy nill;
     val (cons', cons'') = idfs_of_const thy cons;
     val pr = pretty_list nil'' cons'' mk_list mk_char_string target_cons;
   in
     thy
-    |> gen_add_syntax_const (K I) target cons' (SOME pr)
+    |> add_syntax_const target cons' (SOME pr)
   end;
 
 fun add_pretty_ml_string target nill cons str mk_char mk_string target_implode thy =
   let
     val (_, nil'') = idfs_of_const thy nill;
     val (_, cons'') = idfs_of_const thy cons;
     val (str', _) = idfs_of_const thy str;
     val pr = pretty_ml_string nil'' cons'' mk_char mk_string target_implode;
   in
     thy
-    |> gen_add_syntax_const (K I) target str' (SOME pr)
+    |> add_syntax_const target str' (SOME pr)
   end;
 
 fun add_undefined target undef target_undefined thy =
   let
     val (undef', _) = idfs_of_const thy undef;
     fun pr _ _ _ _ = str target_undefined;
   in
     thy
-    |> gen_add_syntax_const (K I) target undef' (SOME (~1, pr))
+    |> add_syntax_const target undef' (SOME (~1, pr))
   end;
 
 fun add_pretty_imperative_monad_bind target bind thy =
   let
     val (bind', _) = idfs_of_const thy bind;
     val pr = pretty_imperative_monad_bind
   in
     thy
-    |> gen_add_syntax_const (K I) target bind' (SOME pr)
+    |> add_syntax_const target bind' (SOME pr)
   end;
 
 val add_haskell_monad = gen_add_haskell_monad CodegenConsts.read_const;
 
 val code_classP =
   OuterSyntax.command code_classK "define code syntax for class" K.thy_decl (
     parse_multi_syntax P.xname
       (Scan.option (P.string -- Scan.optional (P.$$$ "where" |-- Scan.repeat1
         (P.term --| (P.$$$ "\\<equiv>" || P.$$$ "==") -- P.string)) []))
     >> (Toplevel.theory oo fold) (fn (target, syns) =>
-          fold (fn (raw_class, syn) => add_syntax_class target raw_class syn) syns)
+          fold (fn (raw_class, syn) => add_syntax_class_cmd target raw_class syn) syns)
   );
 
 val code_instanceP =
   OuterSyntax.command code_instanceK "define code syntax for instance" K.thy_decl (
     parse_multi_syntax (P.xname --| P.$$$ "::" -- P.xname)
       ((P.minus >> K true) || Scan.succeed false)
     >> (Toplevel.theory oo fold) (fn (target, syns) =>
-          fold (fn (raw_inst, add_del) => add_syntax_inst target raw_inst add_del) syns)
+          fold (fn (raw_inst, add_del) => add_syntax_inst_cmd target raw_inst add_del) syns)
   );
 
 val code_typeP =
   OuterSyntax.command code_typeK "define code syntax for type constructor" K.thy_decl (
     parse_multi_syntax P.xname (parse_syntax I)
     >> (Toplevel.theory oo fold) (fn (target, syns) =>
-          fold (fn (raw_tyco, syn) => add_syntax_tyco target raw_tyco syn) syns)
+          fold (fn (raw_tyco, syn) => add_syntax_tyco_cmd target raw_tyco syn) syns)
   );
 
 val code_constP =
   OuterSyntax.command code_constK "define code syntax for constant" K.thy_decl (
     parse_multi_syntax P.term (parse_syntax fst)
     >> (Toplevel.theory oo fold) (fn (target, syns) =>
-          fold (fn (raw_const, syn) => add_syntax_const target raw_const (no_bindings syn)) syns)
+          fold (fn (raw_const, syn) => add_syntax_const_cmd target raw_const (no_bindings syn)) syns)
   );
 
 val code_monadP =
   OuterSyntax.command code_monadK "define code syntax for Haskell monads" K.thy_decl (
     P.term -- P.term -- P.term

 val _ = OuterSyntax.add_parsers [code_classP, code_instanceP, code_typeP, code_constP,
   code_reservedP, code_modulenameP, code_moduleprologP, code_monadP];
 
 (*including serializer defaults*)
 val _ = Context.add_setup (
-  gen_add_syntax_tyco (K I) "SML" "fun" (SOME (2, fn pr_typ => fn fxy => fn [ty1, ty2] =>
+  add_syntax_tyco "SML" "fun" (SOME (2, fn pr_typ => fn fxy => fn [ty1, ty2] =>
       (gen_brackify (case fxy of NOBR => false | _ => eval_fxy (INFX (1, R)) fxy) o Pretty.breaks) [
         pr_typ (INFX (1, X)) ty1,
         str "->",
         pr_typ (INFX (1, R)) ty2
       ]))
-  #> gen_add_syntax_tyco (K I) "OCaml" "fun" (SOME (2, fn pr_typ => fn fxy => fn [ty1, ty2] =>
+  #> add_syntax_tyco "OCaml" "fun" (SOME (2, fn pr_typ => fn fxy => fn [ty1, ty2] =>
       (gen_brackify (case fxy of NOBR => false | _ => eval_fxy (INFX (1, R)) fxy) o Pretty.breaks) [
         pr_typ (INFX (1, X)) ty1,
         str "->",
         pr_typ (INFX (1, R)) ty2
       ]))
-  #> gen_add_syntax_tyco (K I) "Haskell" "fun" (SOME (2, fn pr_typ => fn fxy => fn [ty1, ty2] =>
+  #> add_syntax_tyco "Haskell" "fun" (SOME (2, fn pr_typ => fn fxy => fn [ty1, ty2] =>
       brackify_infix (1, R) fxy [
         pr_typ (INFX (1, X)) ty1,
         str "->",
         pr_typ (INFX (1, R)) ty2
       ]))