# HG changeset patch
# User haftmann
# Date 1162303167 -3600
# Node ID c725181f5117d6645421368de042fc3497366ff3
# Parent  8e621232a865a5b66db9513c5696bc9dc8f31869
new SML serializer

diff -r 8e621232a865 -r c725181f5117 src/Pure/Tools/codegen_serializer.ML
--- a/src/Pure/Tools/codegen_serializer.ML	Tue Oct 31 14:59:26 2006 +0100
+++ b/src/Pure/Tools/codegen_serializer.ML	Tue Oct 31 14:59:27 2006 +0100
@@ -131,12 +131,12 @@
   let
     val sym_any = Scan.one Symbol.not_eof;
     val parse = Scan.optional ($$ "!" >> K true) false -- Scan.repeat (
-         ($$ "_" -- $$ "_" >> K (Arg NOBR))
+         ($$ "(" -- $$ "_" -- $$ ")" >> K (Arg NOBR))
       || ($$ "_" >> K (Arg BR))
       || ($$ "/" |-- Scan.repeat ($$ " ") >> (Pretty o Pretty.brk o length))
       || (Scan.repeat1
            (   $$ "'" |-- sym_any
-            || Scan.unless ($$ "_" || $$ "/")
+            || Scan.unless ($$ "_" || $$ "/" || $$ "(" |-- $$ "_" |-- $$ ")")
                  sym_any) >> (Pretty o str o implode)));
   in case Scan.finite Symbol.stopper parse (Symbol.explode s)
    of ((_, p as [_]), []) => mk_mixfix (NOBR, p)
@@ -601,37 +601,50 @@
         val base' = if upper then first_upper base else base;
         val ([base''], nsp') = Name.variants [base'] nsp;
       in (base'', nsp') end;
-    fun mk_funs defs nsp =
-      (([], MLFuns (map
-        (fn (name, CodegenThingol.Fun info) => (name, info)
-          | (name, def) => error ("Function block containing illegal def: " ^ quote name)
-        ) defs)), nsp);
-    (*fun mk_funs defs =
+    fun map_nsp_fun f (nsp_fun, nsp_typ) =
+      let
+        val (x, nsp_fun') = f nsp_fun
+      in (x, (nsp_fun', nsp_typ)) end;
+    fun map_nsp_typ f (nsp_fun, nsp_typ) =
+      let
+        val (x, nsp_typ') = f nsp_typ
+      in (x, (nsp_fun, nsp_typ')) end;
+    fun mk_funs defs =
       fold_map
         (fn (name, CodegenThingol.Fun info) =>
-              name_def false (NameSpace.base name) >> (fn base => pair (base, (base, info)))
-          | (name, def) => error ("Function block containing illegal def: " ^ quote name)) defs
-      >> (fn xs : 'a => xs)(*split_list (#> apsnd MLFuns*);*)
-    fun mk_datatype defs nsp =
-      case map_filter
-        (fn (name, CodegenThingol.Datatype info) => SOME (name, info)
-          | (name, CodegenThingol.Datatypecons _) => NONE
+              map_nsp_fun (name_def false (NameSpace.base name)) >> (fn base => (base, (name, info)))
+          | (name, def) => error ("Function block containing illegal def: " ^ quote name)
+        ) defs
+      >> (split_list #> apsnd MLFuns);
+    fun mk_datatype defs =
+      fold_map
+        (fn (name, CodegenThingol.Datatype info) =>
+              map_nsp_typ (name_def false (NameSpace.base name)) >> (fn base => (base, SOME (name, info)))
+          | (name, CodegenThingol.Datatypecons _) =>
+              map_nsp_fun (name_def true (NameSpace.base name)) >> (fn base => (base, NONE))
           | (name, def) => error ("Datatype block containing illegal def: " ^ quote name)
         ) defs
-       of datas as _ :: _ => (([], MLDatas datas), nsp)
-        | _ => error ("Datatype block without data: " ^ (commas o map (quote o fst)) defs);
-    fun mk_class defs nsp =
-      case map_filter
-        (fn (name, CodegenThingol.Class info) => SOME (name, info)
-          | (name, CodegenThingol.Classop _) => NONE
+      >> (split_list #> apsnd (map_filter I
+        #> (fn [] => error ("Datatype block without data: " ^ (commas o map (quote o fst)) defs)
+             | infos => MLDatas infos)));
+    fun mk_class defs =
+      fold_map
+        (fn (name, CodegenThingol.Class info) =>
+              map_nsp_typ (name_def false (NameSpace.base name)) >> (fn base => (base, SOME (name, info)))
+          | (name, CodegenThingol.Classop _) =>
+              map_nsp_fun (name_def true (NameSpace.base name)) >> (fn base => (base, NONE))
           | (name, def) => error ("Class block containing illegal def: " ^ quote name)
         ) defs
-       of [class] => (([], MLClass class), nsp)
-        | _ => error ("Class block without class: " ^ (commas o map (quote o fst)) defs);
+      >> (split_list #> apsnd (map_filter I
+        #> (fn [] => error ("Class block without class: " ^ (commas o map (quote o fst)) defs)
+             | [info] => MLClass info)));
+    fun mk_inst [(name, CodegenThingol.Classinst info)] =
+      map_nsp_fun (name_def false (NameSpace.base name))
+      >> (fn base => ([base], MLClassinst (name, info)));
     fun add_group mk defs nsp_nodes =
       let
         val names as (name :: names') = map fst defs;
-        val _ = writeln ("adding " ^ commas names);
+(*         val _ = writeln ("adding " ^ commas names);  *)
         val deps =
           []
           |> fold (fold (insert (op =)) o Graph.imm_succs code) names
@@ -644,7 +657,7 @@
         fun add_dep defname name'' =
           let
             val (modl'', defname'') = (apfst name_modl o dest_name) name'';
-            val _ = writeln (uncurry NameSpace.append defname ^ " -> " ^ name'');
+(*             val _ = writeln (uncurry NameSpace.append defname ^ " -> " ^ name'');  *)
           in if modl' = modl'' then
             map_node modl'
               (Graph.add_edge (NameSpace.pack (modl @ [fst defname, snd defname]), name''))
@@ -677,20 +690,32 @@
           add_group mk_class defs
       | group_defs ((defs as (_, CodegenThingol.Classop _)::_)) =
           add_group mk_class defs
-      | group_defs [(name, CodegenThingol.Classinst info)] =
-          add_group (fn [def] => fn nsp => (([], MLClassinst def), nsp)) [(name, info)]
+      | group_defs ((defs as [(_, CodegenThingol.Classinst _)])) =
+          add_group mk_inst defs
       | group_defs defs = error ("Illegal mutual dependencies: " ^ (commas o map fst) defs)
-    fun dummy_deresolver prefix name = 
+    val (_, nodes) =
+      empty_module
+      |> fold group_defs (map (AList.make (Graph.get_node code))
+          (rev (Graph.strong_conn code)))
+    fun deresolver prefix name = 
       let
-        val name' = (op @ o apfst name_modl o apsnd (single o snd) o dest_name) name;
-      in (NameSpace.pack o snd o snd o chop_prefix (op =)) (prefix, name') end;
+(*         val _ = writeln ("resolving " ^ name)  *)
+        val (modl, _) = apsnd (uncurry NameSpace.append) (dest_name name);
+        val modl' = name_modl modl;
+        val (_, (_, remainder)) = chop_prefix (op =) (prefix, modl');
+        val defname' =
+          nodes
+          |> fold (fn m => fn g => case Graph.get_node g m
+              of Module (_, (_, g)) => g) modl'
+          |> (fn g => case Graph.get_node g name of Def (defname, _) => defname);
+      in NameSpace.pack (remainder @ [defname']) end;
     fun the_prolog modlname = case module_prolog modlname
      of NONE => []
-      | SOME p => [p, str ""]
+      | SOME p => [p, str ""];
     fun pr_node prefix (Def (_, NONE)) =
           NONE
       | pr_node prefix (Def (_, SOME def)) =
-          SOME (pr_sml_def tyco_syntax const_syntax init_vars (dummy_deresolver prefix) def)
+          SOME (pr_sml_def tyco_syntax const_syntax init_vars (deresolver prefix) def)
       | pr_node prefix (Module (dmodlname, (_, nodes))) =
           (SOME o Pretty.chunks) ([
             str ("structure " ^ dmodlname ^ " = "),
@@ -702,10 +727,6 @@
             str "",
             str ("end; (*struct " ^ dmodlname ^ "*)")
           ]);
-    val (_, nodes) =
-      empty_module
-      |> fold group_defs (map (AList.make (Graph.get_node code))
-          (rev (Graph.strong_conn code)))
     val p = Pretty.chunks ([
         str ("structure ROOT = "),
         str "struct",
@@ -1536,8 +1557,8 @@
 
 val _ = Context.add_setup (
   CodegenSerializerData.init
-  #> add_serializer ("SML", ml_from_thingol)
-  #> add_serializer ("sml", isar_seri_sml)
+  #> add_serializer ("SML", isar_seri_sml)
+  #> add_serializer ("sml", ml_from_thingol)
   #> add_serializer ("Haskell", isar_seri_haskell)
   #> add_serializer (target_diag, (fn _ => fn _ => seri_diagnosis))
 );