src/Tools/code/code_ml.ML

   | stmt_names_of (MLClassinst (i, _)) = [i];
 
 
 (** SML serailizer **)
 
-fun pr_sml_stmt syntax_tyco syntax_const labelled_name reserved_names deresolve is_cons =
+fun pr_sml_stmt naming labelled_name syntax_tyco syntax_const reserved_names deresolve is_cons =
   let
     val pr_label_classrel = translate_string (fn "." => "__" | c => c)
       o NameSpace.qualifier;
     val pr_label_classparam = NameSpace.base o NameSpace.qualifier;
     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) ^ "_";
+        fun pr_dictvar (v, (_, 1)) = Code_Name.first_upper v ^ "_"
+          | pr_dictvar (v, (i, _)) = Code_Name.first_upper v ^ string_of_int (i+1) ^ "_";
         fun pr_proj [] p =
               p
           | pr_proj [p'] p =
               brackets [p', p]
           | pr_proj (ps as _ :: _) p =

           | SOME (i, pr) => pr pr_typ fxy tys)
       | pr_typ fxy (ITyVar v) = str ("'" ^ v);
     fun pr_term thm pat vars fxy (IConst c) =
           pr_app thm pat vars fxy (c, [])
       | pr_term thm pat vars fxy (IVar v) =
-          str (lookup_var vars v)
+          str (Code_Name.lookup_var vars v)
       | pr_term thm pat vars fxy (t as t1 `$ t2) =
           (case Code_Thingol.unfold_const_app t
            of SOME c_ts => pr_app thm pat vars fxy c_ts
             | NONE =>
                 brackify fxy [pr_term thm pat vars NOBR t1, pr_term thm pat vars BR t2])

       else if k = length ts then
         [(str o deresolve) c, Pretty.enum "," "(" ")" (map (pr_term thm pat vars NOBR) ts)]
       else [pr_term thm pat vars BR (Code_Thingol.eta_expand k app)] end else
         (str o deresolve) c
           :: (map (pr_dicts BR) o filter_out null) iss @ map (pr_term thm pat vars BR) ts
-    and pr_app thm pat vars = gen_pr_app pr_app' pr_term syntax_const is_cons thm pat vars
+    and pr_app thm pat vars = gen_pr_app pr_app' pr_term syntax_const is_cons naming thm pat vars
     and pr_bind' ((NONE, NONE), _) = str "_"
       | pr_bind' ((SOME v, NONE), _) = str v
       | pr_bind' ((NONE, SOME p), _) = p
       | pr_bind' ((SOME v, SOME p), _) = concat [str v, str "as", p]
     and pr_bind thm = gen_pr_bind pr_bind' pr_term thm

                         val consts = map_filter
                           (fn c => if (is_some o syntax_const) c
                             then NONE else (SOME o NameSpace.base o deresolve) c)
                             ((fold o Code_Thingol.fold_constnames) (insert (op =)) (t :: ts) []);
                         val vars = reserved_names
-                          |> intro_vars consts
-                          |> intro_vars ((fold o Code_Thingol.fold_unbound_varnames)
+                          |> Code_Name.intro_vars consts
+                          |> Code_Name.intro_vars ((fold o Code_Thingol.fold_unbound_varnames)
                                (insert (op =)) ts []);
                       in
                         concat (
                           [str definer, (str o deresolve) name]
                           @ (if null ts andalso null vs_dict

             val (ps, p) = split_last
               (pr_data "datatype" data :: map (pr_data "and") datas');
           in Pretty.chunks (ps @ [Pretty.block ([p, str ";"])]) end
      | pr_stmt (MLClass (class, (v, (superclasses, classparams)))) =
           let
-            val w = first_upper v ^ "_";
+            val w = Code_Name.first_upper v ^ "_";
             fun pr_superclass_field (class, classrel) =
               (concat o map str) [
                 pr_label_classrel classrel, ":", "'" ^ v, deresolve class
               ];
             fun pr_classparam_field (classparam, ty) =

 };
 
 
 (** OCaml serializer **)
 
-fun pr_ocaml_stmt syntax_tyco syntax_const labelled_name reserved_names deresolve is_cons =
+fun pr_ocaml_stmt naming labelled_name syntax_tyco syntax_const reserved_names deresolve is_cons =
   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);
+        fun pr_dictvar (v, (_, 1)) = "_" ^ Code_Name.first_upper v
+          | pr_dictvar (v, (i, _)) = "_" ^ Code_Name.first_upper v ^ string_of_int (i+1);
         fun pr_proj ps p =
           fold_rev (fn p2 => fn p1 => Pretty.block [p1, str ".", str p2]) ps p
         fun pr_dict fxy (DictConst (inst, dss)) =
               brackify fxy ((str o deresolve) inst :: map (pr_dicts BR) dss)
           | pr_dict fxy (DictVar (classrels, v)) =

           | SOME (i, pr) => pr pr_typ fxy tys)
       | pr_typ fxy (ITyVar v) = str ("'" ^ v);
     fun pr_term thm pat vars fxy (IConst c) =
           pr_app thm pat vars fxy (c, [])
       | pr_term thm pat vars fxy (IVar v) =
-          str (lookup_var vars v)
+          str (Code_Name.lookup_var vars v)
       | pr_term thm pat vars fxy (t as t1 `$ t2) =
           (case Code_Thingol.unfold_const_app t
            of SOME c_ts => pr_app thm pat vars fxy c_ts
             | NONE =>
                 brackify fxy [pr_term thm pat vars NOBR t1, pr_term thm pat vars BR t2])

           | _ => [(str o deresolve) c, Pretty.enum "," "(" ")"
                     (map (pr_term thm pat vars NOBR) ts)]
         else [pr_term thm pat vars BR (Code_Thingol.eta_expand (length tys) app)]
       else (str o deresolve) c
         :: ((map (pr_dicts BR) o filter_out null) iss @ map (pr_term thm pat vars BR) ts)
-    and pr_app thm pat vars = gen_pr_app pr_app' pr_term syntax_const is_cons thm pat vars
+    and pr_app thm pat vars = gen_pr_app pr_app' pr_term syntax_const is_cons naming thm pat vars
     and pr_bind' ((NONE, NONE), _) = str "_"
       | pr_bind' ((SOME v, NONE), _) = str v
       | pr_bind' ((NONE, SOME p), _) = p
       | pr_bind' ((SOME v, SOME p), _) = brackets [p, str "as", str v]
     and pr_bind thm = gen_pr_bind pr_bind' pr_term thm

           | fillup_param x (i, NONE) = x ^ string_of_int i;
         val fished1 = fold (map2 fish_param) eqs (replicate (length (hd eqs)) NONE);
         val x = Name.variant (map_filter I fished1) "x";
         val fished2 = map_index (fillup_param x) fished1;
         val (fished3, _) = Name.variants fished2 Name.context;
-        val vars' = intro_vars fished3 vars;
-      in map (lookup_var vars') fished3 end;
+        val vars' = Code_Name.intro_vars fished3 vars;
+      in map (Code_Name.lookup_var vars') fished3 end;
     fun pr_stmt (MLFuns (funns as funn :: funns')) =
           let
             fun pr_eq ((ts, t), (thm, _)) =
               let
                 val consts = map_filter
                   (fn c => if (is_some o syntax_const) c
                     then NONE else (SOME o NameSpace.base o deresolve) c)
                     ((fold o Code_Thingol.fold_constnames) (insert (op =)) (t :: ts) []);
                 val vars = reserved_names
-                  |> intro_vars consts
-                  |> intro_vars ((fold o Code_Thingol.fold_unbound_varnames)
+                  |> Code_Name.intro_vars consts
+                  |> Code_Name.intro_vars ((fold o Code_Thingol.fold_unbound_varnames)
                       (insert (op =)) ts []);
               in concat [
                 (Pretty.block o Pretty.commas) (map (pr_term thm true vars NOBR) ts),
                 str "->",
                 pr_term thm false vars NOBR t

                     val consts = map_filter
                       (fn c => if (is_some o syntax_const) c
                         then NONE else (SOME o NameSpace.base o deresolve) c)
                         ((fold o Code_Thingol.fold_constnames) (insert (op =)) (t :: ts) []);
                     val vars = reserved_names
-                      |> intro_vars consts
-                      |> intro_vars ((fold o Code_Thingol.fold_unbound_varnames)
+                      |> Code_Name.intro_vars consts
+                      |> Code_Name.intro_vars ((fold o Code_Thingol.fold_unbound_varnames)
                           (insert (op =)) ts []);
                   in
                     concat (
                       map (pr_term thm true vars BR) ts
                       @ str "="

                       (fn c => if (is_some o syntax_const) c
                         then NONE else (SOME o NameSpace.base o deresolve) c)
                         ((fold o Code_Thingol.fold_constnames)
                           (insert (op =)) (map (snd o fst) eqs) []);
                     val vars = reserved_names
-                      |> intro_vars consts;
+                      |> Code_Name.intro_vars consts;
                     val dummy_parms = (map str o fish_params vars o map (fst o fst)) eqs;
                   in
                     Pretty.block (
                       Pretty.breaks dummy_parms
                       @ Pretty.brk 1

             val (ps, p) = split_last
               (pr_data "type" data :: map (pr_data "and") datas');
           in Pretty.chunks (ps @ [Pretty.block ([p, str ";;"])]) end
      | pr_stmt (MLClass (class, (v, (superclasses, classparams)))) =
           let
-            val w = "_" ^ first_upper v;
+            val w = "_" ^ Code_Name.first_upper v;
             fun pr_superclass_field (class, classrel) =
               (concat o map str) [
                 deresolve classrel, ":", "'" ^ v, deresolve class
               ];
             fun pr_classparam_field (classparam, ty) =

       in (x, (nsp_fun', nsp_typ)) end;
     fun map_nsp_typ_yield f (nsp_fun, nsp_typ) =
       let
         val (x, nsp_typ') = f nsp_typ
       in (x, (nsp_fun, nsp_typ')) end;
-    val mk_name_module = mk_name_module reserved_names NONE module_alias program;
+    val mk_name_module = Code_Name.mk_name_module reserved_names NONE module_alias program;
     fun mk_name_stmt upper name nsp =
       let
-        val (_, base) = dest_name name;
-        val base' = if upper then first_upper base else base;
+        val (_, base) = Code_Name.dest_name name;
+        val base' = if upper then Code_Name.first_upper base else base;
         val ([base''], nsp') = Name.variants [base'] nsp;
       in (base'', nsp') end;
     fun add_funs stmts =
       fold_map
-        (fn (name, Code_Thingol.Fun stmt) =>
+        (fn (name, Code_Thingol.Fun (_, stmt)) =>
               map_nsp_fun_yield (mk_name_stmt false name) #>>
                 rpair (name, stmt |> apsnd (filter (snd o snd)))
           | (name, _) =>
               error ("Function block containing illegal statement: " ^ labelled_name name)
         ) stmts
       #>> (split_list #> apsnd MLFuns);
     fun add_datatypes stmts =
       fold_map
-        (fn (name, Code_Thingol.Datatype stmt) =>
+        (fn (name, Code_Thingol.Datatype (_, stmt)) =>
               map_nsp_typ_yield (mk_name_stmt false name) #>> rpair (SOME (name, stmt))
           | (name, Code_Thingol.Datatypecons _) =>
               map_nsp_fun_yield (mk_name_stmt true name) #>> rpair NONE
           | (name, _) =>
               error ("Datatype block containing illegal statement: " ^ labelled_name name)

         #> (fn [] => error ("Datatype block without data statement: "
                   ^ (commas o map (labelled_name o fst)) stmts)
              | stmts => MLDatas stmts)));
     fun add_class stmts =
       fold_map
-        (fn (name, Code_Thingol.Class info) =>
-              map_nsp_typ_yield (mk_name_stmt false name) #>> rpair (SOME (name, info))
+        (fn (name, Code_Thingol.Class (_, stmt)) =>
+              map_nsp_typ_yield (mk_name_stmt false name) #>> rpair (SOME (name, stmt))
           | (name, Code_Thingol.Classrel _) =>
               map_nsp_fun_yield (mk_name_stmt false name) #>> rpair NONE
           | (name, Code_Thingol.Classparam _) =>
               map_nsp_fun_yield (mk_name_stmt false name) #>> rpair NONE
           | (name, _) =>

         val names as (name :: names') = map fst stmts;
         val deps =
           []
           |> fold (fold (insert (op =)) o Graph.imm_succs program) names
           |> subtract (op =) names;
-        val (module_names, _) = (split_list o map dest_name) names;
+        val (module_names, _) = (split_list o map Code_Name.dest_name) names;
         val module_name = (the_single o distinct (op =) o map mk_name_module) module_names
           handle Empty =>
             error ("Different namespace prefixes for mutual dependencies:\n"
               ^ commas (map labelled_name names)
               ^ "\n"
               ^ commas module_names);
         val module_name_path = NameSpace.explode module_name;
         fun add_dep name name' =
           let
-            val module_name' = (mk_name_module o fst o dest_name) name';
+            val module_name' = (mk_name_module o fst o Code_Name.dest_name) name';
           in if module_name = module_name' then
             map_node module_name_path (Graph.add_edge (name, name'))
           else let
             val (common, (diff1::_, diff2::_)) = chop_prefix (op =)
               (module_name_path, NameSpace.explode module_name');

     val (_, nodes) = empty_module
       |> fold add_stmts' (map (AList.make (Graph.get_node program))
           (rev (Graph.strong_conn program)));
     fun deresolver prefix name = 
       let
-        val module_name = (fst o dest_name) name;
+        val module_name = (fst o Code_Name.dest_name) name;
         val module_name' = (NameSpace.explode o mk_name_module) module_name;
         val (_, (_, remainder)) = chop_prefix (op =) (prefix, module_name');
         val stmt_name =
           nodes
           |> fold (fn name => fn node => case Graph.get_node node name

       end handle Graph.UNDEF _ =>
         error ("Unknown statement name: " ^ labelled_name name);
   in (deresolver, nodes) end;
 
 fun serialize_ml target compile pr_module pr_stmt raw_module_name labelled_name reserved_names includes raw_module_alias
-  _ syntax_tyco syntax_const program cs destination =
+  _ syntax_tyco syntax_const naming program cs destination =
   let
     val is_cons = Code_Thingol.is_cons program;
     val stmt_names = Code_Target.stmt_names_of_destination destination;
     val module_name = if null stmt_names then raw_module_name else SOME "Code";
     val (deresolver, nodes) = ml_node_of_program labelled_name module_name
       reserved_names raw_module_alias program;
-    val reserved_names = make_vars reserved_names;
+    val reserved_names = Code_Name.make_vars reserved_names;
     fun pr_node prefix (Dummy _) =
           NONE
       | pr_node prefix (Stmt (_, stmt)) = if null stmt_names orelse
           (not o null o filter (member (op =) stmt_names) o stmt_names_of) stmt then SOME
-            (pr_stmt syntax_tyco syntax_const labelled_name reserved_names
+            (pr_stmt naming labelled_name syntax_tyco syntax_const reserved_names
               (deresolver prefix) is_cons stmt)
           else NONE
       | pr_node prefix (Module (module_name, (_, nodes))) =
           separate (str "")
             ((map_filter (pr_node (prefix @ [module_name]) o Graph.get_node nodes)
               o rev o flat o Graph.strong_conn) nodes)
           |> (if null stmt_names then pr_module module_name else Pretty.chunks)
           |> SOME;
-    val cs' = map_filter (try (deresolver (if is_some module_name then the_list module_name else [])))
-      cs;
+    val cs' = (map o try)
+      (deresolver (if is_some module_name then the_list module_name else [])) cs;
     val p = Pretty.chunks (separate (str "") (map snd includes @ (map_filter
       (pr_node [] o Graph.get_node nodes) o rev o flat o Graph.strong_conn) nodes));
   in
     Code_Target.mk_serialization target
       (case compile of SOME compile => SOME (compile o Code_Target.code_of_pretty) | NONE => NONE)

 end; (*local*)
 
 
 (** ML (system language) code for evaluation and instrumentalization **)
 
-fun ml_code_of thy = Code_Target.serialize_custom thy
-  (target_SML, (fn _ => fn [] => serialize_ml target_SML (SOME (K ())) (K Pretty.chunks) pr_sml_stmt (SOME ""),
+fun ml_code_of thy = Code_Target.serialize_custom thy (target_SML,
+    (fn _ => fn [] => serialize_ml target_SML (SOME (K ())) (K Pretty.chunks) pr_sml_stmt (SOME ""),
   literals_sml));
 
 
 (* evaluation *)
 

   let
     val ctxt = ProofContext.init thy;
     val _ = if null (term_frees (term_of ct)) then () else error ("Term "
       ^ quote (Syntax.string_of_term_global thy (term_of ct))
       ^ " to be evaluated contains free variables");
-    fun eval' program ((vs, ty), t) deps =
+    fun eval' naming program ((vs, ty), t) deps =
       let
         val _ = if Code_Thingol.contains_dictvar t then
           error "Term to be evaluated constains free dictionaries" else ();
+        val value_name = "Value.VALUE.value"
         val program' = program
-          |> Graph.new_node (Code_Name.value_name,
-              Code_Thingol.Fun (([], ty), [(([], t), (Drule.dummy_thm, true))]))
-          |> fold (curry Graph.add_edge Code_Name.value_name) deps;
-        val (value_code, [value_name']) = ml_code_of thy program' [Code_Name.value_name];
+          |> Graph.new_node (value_name,
+              Code_Thingol.Fun (Term.dummy_patternN, (([], ty), [(([], t), (Drule.dummy_thm, true))])))
+          |> fold (curry Graph.add_edge value_name) deps;
+        val (value_code, [SOME value_name']) = ml_code_of thy naming program' [value_name];
         val sml_code = "let\n" ^ value_code ^ "\nin " ^ value_name'
           ^ space_implode " " (map (enclose "(" ")") args) ^ " end";
       in ML_Context.evaluate ctxt Output.ml_output false reff sml_code end;
   in eval'' thy (fn t => (t, eval')) ct end;
 

 
 val is_first_occ = fst o snd o CodeAntiqData.get;
 
 fun delayed_code thy consts () =
   let
-    val (consts', program) = Code_Thingol.consts_program thy consts;
-    val (ml_code, consts'') = ml_code_of thy program consts';
-    val _ = if length consts <> length consts'' then
-      error ("One of the constants " ^ commas (map (quote o Code_Unit.string_of_const thy) consts)
-        ^ "\nhas a user-defined serialization") else ();
-  in (ml_code, consts ~~ consts'') end;
+    val (consts', (naming, program)) = Code_Thingol.consts_program thy consts;
+    val (ml_code, consts'') = ml_code_of thy naming program consts';
+    val const_tab = map2 (fn const => fn NONE =>
+      error ("Constant " ^ (quote o Code_Unit.string_of_const thy) const
+        ^ "\nhas a user-defined serialization")
+      | SOME const' => (const, const')) consts consts''
+  in (ml_code, const_tab) end;
 
 fun register_const const ctxt =
   let
     val (consts, (_, (struct_name, _))) = CodeAntiqData.get ctxt;
     val consts' = insert (op =) const consts;