src/Pure/Tools/codegen_serializer.ML

 val first_lower = implode o nth_map 0 Symbol.to_ascii_lower o explode;
 
 val dest_name =
   apfst NameSpace.implode o split_last o fst o split_last o NameSpace.explode;
 
-fun mk_modl_name_tab empty_names prefix module_alias code =
+fun mk_modl_name_tab init_names prefix module_alias code =
   let
     fun nsp_map f = NameSpace.explode #> map f #> NameSpace.implode;
     fun mk_alias name =
      case module_alias name
       of SOME name' => name'
        | NONE => nsp_map (fn name => (the_single o fst)
-            (Name.variants [name] empty_names)) name;
+            (Name.variants [name] init_names)) name;
     fun mk_prefix name =
       case prefix
        of SOME prefix => NameSpace.append prefix name
         | NONE => name;
     val tab =

   | MLClass of string * ((class * string) list * (vname * (string * itype) list))
   | MLClassinst of string * ((class * (string * (vname * sort) list))
         * ((class * (string * (string * dict list list))) list
       * (string * iterm) list));
 
-fun pr_sml tyco_syntax const_syntax labelled_name keyword_vars deresolv is_cons ml_def =
+fun pr_sml tyco_syntax const_syntax labelled_name init_syms deresolv is_cons ml_def =
   let
     val pr_label_classrel = translate_string (fn "." => "__" | c => c) o NameSpace.qualifier;
     val pr_label_classop = NameSpace.base o NameSpace.qualifier;
     fun pr_dicts fxy ds =
       let

                   let
                     val consts = map_filter
                       (fn c => if (is_some o const_syntax) c
                         then NONE else (SOME o NameSpace.base o deresolv) c)
                         ((fold o CodegenThingol.fold_constnames) (insert (op =)) (t :: ts) []);
-                    val vars = keyword_vars
+                    val vars = init_syms
                       |> CodegenNames.intro_vars consts
                       |> CodegenNames.intro_vars ((fold o CodegenThingol.fold_unbound_varnames)
                            (insert (op =)) ts []);
                   in
                     concat (

               let
                 val consts = map_filter
                   (fn c => if (is_some o const_syntax) c
                     then NONE else (SOME o NameSpace.base o deresolv) c)
                     (CodegenThingol.fold_constnames (insert (op =)) t []);
-                val vars = CodegenNames.intro_vars consts keyword_vars;
+                val vars = CodegenNames.intro_vars consts init_syms;
               in
                 concat [
                   (str o pr_label_classop) classop,
                   str "=",
                   pr_term vars NOBR t

   ] @ content @ [
     str "",
     str ("end; (*struct " ^ name ^ "*)")
   ]);
 
-fun pr_ocaml tyco_syntax const_syntax labelled_name keyword_vars deresolv is_cons ml_def =
+fun pr_ocaml tyco_syntax const_syntax labelled_name init_syms deresolv is_cons ml_def =
   let
     fun pr_dicts fxy ds =
       let
         fun pr_dictvar (v, (_, 1)) = "_" ^ first_upper v
           | pr_dictvar (v, (i, _)) = "_" ^ first_upper v ^ string_of_int (i+1);

               let
                 val consts = map_filter
                   (fn c => if (is_some o const_syntax) c
                     then NONE else (SOME o NameSpace.base o deresolv) c)
                     ((fold o CodegenThingol.fold_constnames) (insert (op =)) (t :: ts) []);
-                val vars = keyword_vars
+                val vars = init_syms
                   |> CodegenNames.intro_vars consts
                   |> CodegenNames.intro_vars ((fold o CodegenThingol.fold_unbound_varnames)
                       (insert (op =)) ts []);
               in concat [
                 (Pretty.block o Pretty.commas) (map (pr_term vars NOBR) ts),

                   let
                     val consts = map_filter
                       (fn c => if (is_some o const_syntax) c
                         then NONE else (SOME o NameSpace.base o deresolv) c)
                         ((fold o CodegenThingol.fold_constnames) (insert (op =)) (t :: ts) []);
-                    val vars = keyword_vars
+                    val vars = init_syms
                       |> CodegenNames.intro_vars consts
                       |> CodegenNames.intro_vars ((fold o CodegenThingol.fold_unbound_varnames)
                           (insert (op =)) ts []);
                   in
                     concat (

                   let
                     val consts = map_filter
                       (fn c => if (is_some o const_syntax) c
                         then NONE else (SOME o NameSpace.base o deresolv) c)
                         ((fold o CodegenThingol.fold_constnames) (insert (op =)) (map snd eqs) []);
-                    val vars = keyword_vars
+                    val vars = init_syms
                       |> CodegenNames.intro_vars consts;
                     val dummy_parms = (map str o fish_parms vars o map fst) eqs;
                   in
                     Pretty.block (
                       Pretty.breaks dummy_parms

               let
                 val consts = map_filter
                   (fn c => if (is_some o const_syntax) c
                     then NONE else (SOME o NameSpace.base o deresolv) c)
                     (CodegenThingol.fold_constnames (insert (op =)) t []);
-                val vars = CodegenNames.intro_vars consts keyword_vars;
+                val vars = CodegenNames.intro_vars consts init_syms;
               in
                 concat [
                   (str o deresolv) classop,
                   str "=",
                   pr_term vars NOBR t

   ]);
 
 val code_width = ref 80;
 fun code_output p = Pretty.setmp_margin (!code_width) Pretty.output p ^ "\n";
 
-fun seri_ml pr_def pr_modl reserved_ml output labelled_name reserved_user module_alias module_prolog
+fun seri_ml pr_def pr_modl output labelled_name reserved_syms module_alias module_prolog
   (_ : string -> class_syntax option) tyco_syntax const_syntax code =
   let
     val is_cons = fn node => case CodegenThingol.get_def code node
      of CodegenThingol.Datatypecons _ => true
       | _ => false;
     datatype node =
         Def of string * ml_def option
       | Module of string * ((Name.context * Name.context) * node Graph.T);
-    val empty_names = reserved_ml |> fold Name.declare reserved_user;
-    val empty_module = ((empty_names, empty_names), Graph.empty);
+    val init_names = Name.make_context reserved_syms;
+    val init_module = ((init_names, init_names), Graph.empty);
     fun map_node [] f = f
       | map_node (m::ms) f =
-          Graph.default_node (m, Module (m, empty_module))
+          Graph.default_node (m, Module (m, init_module))
           #> Graph.map_node m (fn (Module (dmodlname, (nsp, nodes))) => Module (dmodlname, (nsp, map_node ms f nodes)));
     fun map_nsp_yield [] f (nsp, nodes) =
           let
             val (x, nsp') = f nsp
           in (x, (nsp', nodes)) end
       | map_nsp_yield (m::ms) f (nsp, nodes) =
           let
             val (x, nodes') =
               nodes
-              |> Graph.default_node (m, Module (m, empty_module))
+              |> Graph.default_node (m, Module (m, init_module))
               |> Graph.map_node_yield m (fn Module (dmodlname, nsp_nodes) => 
                   let
                     val (x, nsp_nodes') = map_nsp_yield ms f nsp_nodes
                   in (x, Module (dmodlname, nsp_nodes')) end)
           in (x, (nsp, nodes')) end;
-    val init_vars = CodegenNames.make_vars (ML_Syntax.reserved_names @ reserved_user);
-    val name_modl = mk_modl_name_tab empty_names NONE module_alias code;
+    val init_syms = CodegenNames.make_vars reserved_syms;
+    val name_modl = mk_modl_name_tab init_names NONE module_alias code;
     fun name_def upper name nsp =
       let
         val (_, base) = dest_name name;
         val base' = if upper then first_upper base else base;
         val ([base''], nsp') = Name.variants [base'] nsp;

           add_group mk_class defs
       | group_defs ((defs as [(_, CodegenThingol.Classinst _)])) =
           add_group mk_inst defs
       | group_defs defs = error ("Illegal mutual dependencies: " ^ (commas o map (labelled_name o fst)) defs)
     val (_, nodes) =
-      empty_module
+      init_module
       |> fold group_defs (map (AList.make (Graph.get_node code))
           (rev (Graph.strong_conn code)))
     fun deresolver prefix name = 
       let
         val modl = (fst o dest_name) name;

      of NONE => []
       | SOME p => [p, str ""];
     fun pr_node prefix (Def (_, NONE)) =
           NONE
       | pr_node prefix (Def (_, SOME def)) =
-          SOME (pr_def tyco_syntax const_syntax labelled_name init_vars (deresolver prefix) is_cons def)
+          SOME (pr_def tyco_syntax const_syntax labelled_name init_syms (deresolver prefix) is_cons def)
       | pr_node prefix (Module (dmodlname, (_, nodes))) =
           SOME (pr_modl dmodlname (the_prolog (NameSpace.implode (prefix @ [dmodlname]))
             @ separate (str "") ((map_filter (pr_node (prefix @ [dmodlname]) o Graph.get_node nodes)
                 o rev o flat o Graph.strong_conn) nodes)));
     val p = pr_modl "ROOT" (the_prolog "" @ separate (str "") ((map_filter

      of NONE => use_text "generated code" Output.ml_output false o code_output
       | SOME "-" => writeln o code_output
       | SOME file => File.write (Path.explode file) o code_output;
   in
     parse_args (Scan.succeed ())
-    #> (fn () => seri_ml pr_sml pr_sml_modl ML_Syntax.reserved output)
-  end;
-
-val reserved_ocaml = Name.make_context ["and", "as", "assert", "begin", "class",
-  "constraint", "do", "done", "downto", "else", "end", "exception",
-  "external", "false", "for", "fun", "function", "functor", "if",
-  "in", "include", "inherit", "initializer", "lazy", "let", "match", "method",
-  "module", "mutable", "new", "object", "of", "open", "or", "private", "rec",
-  "sig", "struct", "then", "to", "true", "try", "type", "val",
-  "virtual", "when", "while", "with", "mod"];
+    #> (fn () => seri_ml pr_sml pr_sml_modl output)
+  end;
 
 fun isar_seri_ocaml file =
   let
     val output = case file
      of NONE => error "OCaml: no internal compilation"

       | SOME file => File.write (Path.explode file) o code_output;
     fun output_file file = File.write (Path.explode file) o code_output;
     val output_diag = writeln o code_output;
   in
     parse_args (Scan.succeed ())
-    #> (fn () => seri_ml pr_ocaml pr_ocaml_modl reserved_ocaml output)
+    #> (fn () => seri_ml pr_ocaml pr_ocaml_modl output)
   end;
 
 
 (** Haskell serializer **)
 

 
 val pr_bind_haskell = gen_pr_bind pr_bind';
 
 in
 
-fun pr_haskell class_syntax tyco_syntax const_syntax labelled_name keyword_vars deresolv_here deresolv deriving_show def =
+fun pr_haskell class_syntax tyco_syntax const_syntax labelled_name init_syms deresolv_here deresolv deriving_show def =
   let
     fun class_name class = case class_syntax class
      of NONE => deresolv class
       | SOME (class, _) => class;
     fun classop_name class classop = case class_syntax class

       (str o deresolv) c :: map (pr_term vars BR) ts
     and pr_app vars = gen_pr_app pr_app' pr_term const_syntax vars
     and pr_bind fxy = pr_bind_haskell pr_term fxy;
     fun pr_def (name, CodegenThingol.Fun (eqs, (vs, ty))) =
           let
-            val tyvars = CodegenNames.intro_vars (map fst vs) keyword_vars;
+            val tyvars = CodegenNames.intro_vars (map fst vs) init_syms;
             fun pr_eq (ts, t) =
               let
                 val consts = map_filter
                   (fn c => if (is_some o const_syntax) c
                     then NONE else (SOME o NameSpace.base o deresolv) c)
                     ((fold o CodegenThingol.fold_constnames) (insert (op =)) (t :: ts) []);
-                val vars = keyword_vars
+                val vars = init_syms
                   |> CodegenNames.intro_vars consts
                   |> CodegenNames.intro_vars ((fold o CodegenThingol.fold_unbound_varnames)
                        (insert (op =)) ts []);
               in
                 semicolon (

               :: map pr_eq eqs
             )
           end
       | pr_def (name, CodegenThingol.Datatype (vs, [])) =
           let
-            val tyvars = CodegenNames.intro_vars (map fst vs) keyword_vars;
+            val tyvars = CodegenNames.intro_vars (map fst vs) init_syms;
           in
             semicolon [
               str "data",
               pr_typscheme_expr tyvars (vs, (deresolv_here name, map (ITyVar o fst) vs))
             ]
           end
       | pr_def (name, CodegenThingol.Datatype (vs, [(co, [ty])])) =
           let
-            val tyvars = CodegenNames.intro_vars (map fst vs) keyword_vars;
+            val tyvars = CodegenNames.intro_vars (map fst vs) init_syms;
           in
             semicolon (
               str "newtype"
               :: pr_typscheme_expr tyvars (vs, (deresolv_here name, map (ITyVar o fst) vs))
               :: str "="

               :: (if deriving_show name then [str "deriving (Read, Show)"] else [])
             )
           end
       | pr_def (name, CodegenThingol.Datatype (vs, co :: cos)) =
           let
-            val tyvars = CodegenNames.intro_vars (map fst vs) keyword_vars;
+            val tyvars = CodegenNames.intro_vars (map fst vs) init_syms;
             fun pr_co (co, tys) =
               concat (
                 (str o deresolv_here) co
                 :: map (pr_typ tyvars BR) tys
               )

               @ (if deriving_show name then [str "deriving (Read, Show)"] else [])
             )
           end
       | pr_def (name, CodegenThingol.Class (superclasss, (v, classops))) =
           let
-            val tyvars = CodegenNames.intro_vars [v] keyword_vars;
+            val tyvars = CodegenNames.intro_vars [v] init_syms;
             fun pr_classop (classop, ty) =
               semicolon [
                 (str o classop_name name) classop,
                 str "::",
                 pr_typ tyvars NOBR ty

               str "};"
             ) (map pr_classop classops)
           end
       | pr_def (_, CodegenThingol.Classinst ((class, (tyco, vs)), (_, classop_defs))) =
           let
-            val tyvars = CodegenNames.intro_vars (map fst vs) keyword_vars;
+            val tyvars = CodegenNames.intro_vars (map fst vs) init_syms;
             fun pr_instdef (classop, t) =
                 let
                   val consts = map_filter
                     (fn c => if (is_some o const_syntax) c
                       then NONE else (SOME o NameSpace.base o deresolv) c)
                       (CodegenThingol.fold_constnames (insert (op =)) t []);
-                  val vars = keyword_vars
+                  val vars = init_syms
                     |> CodegenNames.intro_vars consts;
                 in
                   semicolon [
                     (str o classop_name class) classop,
                     str "=",

       in (brack o Pretty.block_enclose (str "do {", str "}")) (ps @| pr vars' NOBR t) end;
   in (1, pretty) end;
 
 end; (*local*)
 
-val reserved_haskell = [
-  "hiding", "deriving", "where", "case", "of", "infix", "infixl", "infixr",
-  "import", "default", "forall", "let", "in", "class", "qualified", "data",
-  "newtype", "instance", "if", "then", "else", "type", "as", "do", "module"
-];
-
-fun seri_haskell module_prefix destination string_classes labelled_name reserved_user module_alias module_prolog
+fun seri_haskell module_prefix destination string_classes labelled_name reserved_syms module_alias module_prolog
   class_syntax tyco_syntax const_syntax code =
   let
     val _ = Option.map File.check destination;
-    val empty_names = Name.make_context (reserved_haskell @ reserved_user);
-    val name_modl = mk_modl_name_tab empty_names module_prefix module_alias code;
+    val init_names = Name.make_context reserved_syms;
+    val name_modl = mk_modl_name_tab init_names module_prefix module_alias code;
     fun add_def (name, (def, deps)) =
       let
         val (modl, base) = dest_name name;
         fun name_def base = Name.variants [base] #>> the_single;
         fun add_fun upper (nsp_fun, nsp_typ) =

             | CodegenThingol.Classrel _ => I
             | CodegenThingol.Classop _ =>
                 cons (name, ((NameSpace.append modlname' base', base'), NONE))
             | _ => cons (name, ((NameSpace.append modlname' base', base'), SOME def));
       in
-        Symtab.map_default (modlname', ([], ([], (empty_names, empty_names))))
+        Symtab.map_default (modlname', ([], ([], (init_names, init_names))))
               (apfst (fold (insert (op = : string * string -> bool)) deps))
         #> `(fn code => add_name ((snd o snd o the o Symtab.lookup code) modlname'))
         #-> (fn (base', names) =>
               (Symtab.map_entry modlname' o apsnd) (fn (defs, _) =>
               (add_def base' defs, names)))
       end;
     val code' =
       fold add_def (AList.make (fn name => (Graph.get_node code name, Graph.imm_succs code name))
         (Graph.strong_conn code |> flat)) Symtab.empty;
-    val init_vars = CodegenNames.make_vars (reserved_haskell @ reserved_user);
+    val init_syms = CodegenNames.make_vars reserved_syms;
     fun deresolv name =
       (fst o fst o the o AList.lookup (op =) ((fst o snd o the
         o Symtab.lookup code') ((name_modl o fst o dest_name) name))) name
         handle Option => error ("Unknown definition name: " ^ labelled_name name);
     fun deresolv_here name =

                     (maps snd cs)
         and deriv' tycos (tyco `%% tys) = deriv tycos tyco
               andalso forall (deriv' tycos) tys
           | deriv' _ (ITyVar _) = true
       in deriv [] tyco end;
-    fun seri_def qualified = pr_haskell class_syntax tyco_syntax const_syntax labelled_name init_vars
+    fun seri_def qualified = pr_haskell class_syntax tyco_syntax const_syntax labelled_name init_syms
       deresolv_here (if qualified then deresolv else deresolv_here)
       (if string_classes then deriving_show else K false);
     fun write_module (SOME destination) modlname =
           let
             val filename = case modlname

 
 (** diagnosis serializer **)
 
 fun seri_diagnosis labelled_name _ _ _ _ _ code =
   let
-    val init_vars = CodegenNames.make_vars reserved_haskell;
+    val init_names = CodegenNames.make_vars [];
     fun pr_fun "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
           ])
       | pr_fun _ = NONE
-    val pr = pr_haskell (K NONE) pr_fun (K NONE) labelled_name init_vars I I (K false);
+    val pr = pr_haskell (K NONE) pr_fun (K NONE) labelled_name init_names I I (K false);
   in
     []
     |> Graph.fold (fn (name, (def, _)) => case try pr (name, def) of SOME p => cons p | NONE => I) code
     |> Pretty.chunks2
     |> code_output

   let
     val val_name = "eval.EVAL.EVAL";
     val val_name' = "ROOT.eval.EVAL";
     val val_name'_args = space_implode " " (val_name' :: map (enclose "(" ")") args);
     val data = (the o Symtab.lookup (CodegenSerializerData.get thy)) "SML"
-    val reserved = the_reserved data;
+    val reserved_syms = the_reserved data;
     val { alias, prolog } = the_syntax_modl data;
     val { class, inst, tyco, const } = the_syntax_expr data;
     fun eval p = (
       reff := NONE;
       if !eval_verbose then Pretty.writeln p else ();

     code
     |> CodegenThingol.add_eval_def (val_name, t)
     |> CodegenThingol.project_code
         (Symtab.keys class @ Symtab.keys inst @ Symtab.keys tyco @ Symtab.keys const)
           (SOME [val_name])
-    |> seri_ml pr_sml pr_sml_modl ML_Syntax.reserved I (labelled_name thy) reserved
+    |> seri_ml pr_sml pr_sml_modl I (labelled_name thy) reserved_syms
         (Symtab.lookup alias) (Symtab.lookup prolog)
         (Symtab.lookup class) (Symtab.lookup tyco) (Symtab.lookup const)
     |> eval
   end;
 

     |> gen_add_syntax_const (K I) target_Haskell c_kbind'
           (no_bindings (SOME (parse_infix fst (L, 1) ">>")))
   end;
 
 fun add_reserved target =
-  map_reserveds target o insert (op =);
+  let
+    fun add sym syms = if member (op =) syms sym
+      then error ("Reserved symbol " ^ quote sym ^ " already declared")
+      else insert (op =) sym syms
+  in map_reserveds target o add end;
 
 fun add_modl_alias target =
   map_syntax_modls target o apfst o Symtab.update o apsnd CodegenNames.check_modulename;
 
 fun add_modl_prolog target =

 
 val _ = OuterSyntax.add_keywords [infixK, infixlK, infixrK];
 
 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 (
   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) [

       brackify_infix (1, R) fxy [
         pr_typ (INFX (1, X)) ty1,
         str "->",
         pr_typ (INFX (1, R)) ty2
       ]))
-  (*IntInt resp. Big_int are added later when code extraction for numerals is set up*)
-  #> fold (add_reserved "SML") ["o" (*dictionary projections use it already*),
-      "div", "mod" (*infixes*)]
+  #> fold (add_reserved "SML") ML_Syntax.reserved_names
+  #> fold (add_reserved "SML")
+      ["o" (*dictionary projections use it already*), "div", "mod" (*standard infixes*)]
+  #> fold (add_reserved "OCaml") [
+      "and", "as", "assert", "begin", "class",
+      "constraint", "do", "done", "downto", "else", "end", "exception",
+      "external", "false", "for", "fun", "function", "functor", "if",
+      "in", "include", "inherit", "initializer", "lazy", "let", "match", "method",
+      "module", "mutable", "new", "object", "of", "open", "or", "private", "rec",
+      "sig", "struct", "then", "to", "true", "try", "type", "val",
+      "virtual", "when", "while", "with", "mod"
+    ]
+  #> fold (add_reserved "Haskell") [
+      "hiding", "deriving", "where", "case", "of", "infix", "infixl", "infixr",
+      "import", "default", "forall", "let", "in", "class", "qualified", "data",
+      "newtype", "instance", "if", "then", "else", "type", "as", "do", "module"
+    ]
   #> fold (add_reserved "Haskell") [
       "Prelude", "Main", "Bool", "Maybe", "Either", "Ordering", "Char", "String", "Int",
       "Integer", "Float", "Double", "Rational", "IO", "Eq", "Ord", "Enum", "Bounded",
       "Num", "Real", "Integral", "Fractional", "Floating", "RealFloat", "Monad", "Functor",
       "AlreadyExists", "ArithException", "ArrayException", "AssertionFailed", "AsyncException",
       "BlockedOnDeadMVar", "Deadlock", "Denormal", "DivideByZero", "DotNetException", "DynException",
       "Dynamic", "EOF", "EQ", "EmptyRec", "ErrorCall", "ExitException", "ExitFailure",
       "ExitSuccess", "False", "GT", "HeapOverflow",
-      "IO", "IOError", "IOException", "IllegalOperation",
+      "IOError", "IOException", "IllegalOperation",
       "IndexOutOfBounds", "Just", "Key", "LT", "Left", "LossOfPrecision", "NoMethodError",
       "NoSuchThing", "NonTermination", "Nothing", "Obj", "OtherError", "Overflow",
       "PatternMatchFail", "PermissionDenied", "ProtocolError", "RecConError", "RecSelError",
       "RecUpdError", "ResourceBusy", "ResourceExhausted", "Right", "StackOverflow",
       "ThreadKilled", "True", "TyCon", "TypeRep", "UndefinedElement", "Underflow",