# HG changeset patch
# User haftmann
# Date 1283416188 -7200
# Node ID 0dd6c5a0beef31c668a5e269b076a968a68fe4af
# Parent  e4262f9e6a4e171eda01fe87e41cf6de1dfacbad
use code_namespace module for SML and OCaml code

diff -r e4262f9e6a4e -r 0dd6c5a0beef src/Tools/Code/code_ml.ML
--- a/src/Tools/Code/code_ml.ML	Thu Sep 02 10:29:48 2010 +0200
+++ b/src/Tools/Code/code_ml.ML	Thu Sep 02 10:29:48 2010 +0200
@@ -707,6 +707,87 @@
 
 (** SML/OCaml generic part **)
 
+fun ml_program_of_program labelled_name reserved module_alias program =
+  let
+    fun namify_const upper base (nsp_const, nsp_type) =
+      let
+        val (base', nsp_const') = yield_singleton Name.variants
+          (if upper then first_upper base else base) nsp_const
+      in (base', (nsp_const', nsp_type)) end;
+    fun namify_type base (nsp_const, nsp_type) =
+      let
+        val (base', nsp_type') = yield_singleton Name.variants base nsp_type
+      in (base', (nsp_const, nsp_type')) end;
+    fun namify_stmt (Code_Thingol.Fun _) = namify_const false
+      | namify_stmt (Code_Thingol.Datatype _) = namify_type
+      | namify_stmt (Code_Thingol.Datatypecons _) = namify_const true
+      | namify_stmt (Code_Thingol.Class _) = namify_type
+      | namify_stmt (Code_Thingol.Classrel _) = namify_const false
+      | namify_stmt (Code_Thingol.Classparam _) = namify_const false
+      | namify_stmt (Code_Thingol.Classinst _) = namify_const false;
+    fun ml_binding_of_stmt (name, Code_Thingol.Fun (_, ((tysm as (vs, ty), raw_eqs), _))) =
+          let
+            val eqs = filter (snd o snd) raw_eqs;
+            val (eqs', some_value_name) = if null (filter_out (null o snd) vs) then case eqs
+               of [(([], t), some_thm)] => if (not o null o fst o Code_Thingol.unfold_fun) ty
+                  then ([(([IVar (SOME "x")], t `$ IVar (SOME "x")), some_thm)], NONE)
+                  else (eqs, SOME (name, member (op =) (Code_Thingol.add_constnames t []) name))
+                | _ => (eqs, NONE)
+              else (eqs, NONE)
+          in (ML_Function (name, (tysm, eqs')), some_value_name) end
+      | ml_binding_of_stmt (name, Code_Thingol.Classinst (stmt as ((_, (_, vs)), _))) =
+          (ML_Instance (name, stmt), if forall (null o snd) vs then SOME (name, false) else NONE)
+      | ml_binding_of_stmt (name, _) =
+          error ("Binding block containing illegal statement: " ^ labelled_name name)
+    fun modify_fun (name, stmt) =
+      let
+        val (binding, some_value_name) = ml_binding_of_stmt (name, stmt);
+        val ml_stmt = case binding
+         of ML_Function (name, ((vs, ty), [])) =>
+              ML_Exc (name, ((vs, ty),
+                (length o filter_out (null o snd)) vs + (length o fst o Code_Thingol.unfold_fun) ty))
+          | _ => case some_value_name
+             of NONE => ML_Funs ([binding], [])
+              | SOME (name, true) => ML_Funs ([binding], [name])
+              | SOME (name, false) => ML_Val binding
+      in SOME ml_stmt end;
+    fun modify_funs stmts =
+      (SOME (ML_Funs (map_split ml_binding_of_stmt stmts |> (apsnd o map_filter o Option.map) fst))
+        :: replicate (length stmts - 1) NONE)
+    fun modify_datatypes stmts =
+      (SOME (ML_Datas (map_filter
+        (fn (name, Code_Thingol.Datatype (_, stmt)) => SOME (name, stmt) | _ => NONE) stmts))
+        :: replicate (length stmts - 1) NONE)
+    fun modify_class stmts =
+      (SOME (ML_Class (the_single (map_filter
+        (fn (name, Code_Thingol.Class (_, stmt)) => SOME (name, stmt) | _ => NONE) stmts)))
+        :: replicate (length stmts - 1) NONE)
+    fun modify_stmts ([stmt as (name, Code_Thingol.Fun _)]) =
+          [modify_fun stmt]
+      | modify_stmts ((stmts as (_, Code_Thingol.Fun _)::_)) =
+          modify_funs stmts
+      | modify_stmts ((stmts as (_, Code_Thingol.Datatypecons _)::_)) =
+          modify_datatypes stmts
+      | modify_stmts ((stmts as (_, Code_Thingol.Datatype _)::_)) =
+          modify_datatypes stmts
+      | modify_stmts ((stmts as (_, Code_Thingol.Class _)::_)) =
+          modify_class stmts
+      | modify_stmts ((stmts as (_, Code_Thingol.Classrel _)::_)) =
+          modify_class stmts
+      | modify_stmts ((stmts as (_, Code_Thingol.Classparam _)::_)) =
+          modify_class stmts
+      | modify_stmts ([stmt as (_, Code_Thingol.Classinst _)]) =
+          [modify_fun stmt]
+      | modify_stmts ((stmts as (_, Code_Thingol.Classinst _)::_)) =
+          modify_funs stmts
+      | modify_stmts stmts = error ("Illegal mutual dependencies: " ^
+          (Library.commas o map (labelled_name o fst)) stmts);
+  in
+    Code_Namespace.hierarchical_program labelled_name { module_alias = module_alias, reserved = reserved,
+      empty_nsp = (reserved, reserved), namify_module = pair, namify_stmt = namify_stmt,
+      cyclic_modules = false, empty_data = (), memorize_data = K I, modify_stmts = modify_stmts } program
+  end;
+
 local
 
 datatype ml_node =
@@ -906,27 +987,30 @@
   let
     val is_cons = Code_Thingol.is_cons program;
     val is_presentation = not (null presentation_names);
-    val (deresolver, nodes) = ml_node_of_program labelled_name
-      reserved_syms module_alias program;
-    val reserved = make_vars reserved_syms;
-    fun print_node prefix (Dummy _) =
+    val { deresolver, hierarchical_program = ml_program } =
+      ml_program_of_program labelled_name (Name.make_context reserved_syms) module_alias program;
+    fun print_node _ (_, Code_Namespace.Dummy) =
           NONE
-      | print_node prefix (Stmt (_, stmt)) = if is_presentation andalso
-          (null o filter (member (op =) presentation_names) o stmt_names_of) stmt
+      | print_node prefix_fragments (_, Code_Namespace.Stmt stmt) =
+          if is_presentation andalso
+            (null o filter (member (op =) presentation_names) o stmt_names_of) stmt
           then NONE
-          else SOME (print_stmt labelled_name tyco_syntax const_syntax reserved is_cons (deresolver prefix) stmt)
-      | print_node prefix (Module (module_name, (_, nodes))) =
+          else SOME (print_stmt labelled_name tyco_syntax const_syntax (make_vars reserved_syms)
+            is_cons (deresolver prefix_fragments) stmt)
+      | print_node prefix_fragments (name_fragment, Code_Namespace.Module (_, nodes)) =
           let
-            val (decls, body) = print_nodes (prefix @ [module_name]) nodes;
+            val (decls, body) = print_nodes (prefix_fragments @ [name_fragment]) nodes;
             val p = if is_presentation then Pretty.chunks2 body
-              else print_module module_name (if with_signatures then SOME decls else NONE) body;
+              else print_module name_fragment
+                (if with_signatures then SOME decls else NONE) body;
           in SOME ([], p) end
-    and print_nodes prefix nodes = (map_filter (print_node prefix o Graph.get_node nodes)
+    and print_nodes prefix_fragments nodes = (map_filter
+        (fn name => print_node prefix_fragments (name, snd (Graph.get_node nodes name)))
         o rev o flat o Graph.strong_conn) nodes
       |> split_list
       |> (fn (decls, body) => (flat decls, body))
     val names' = map (try (deresolver [])) names;
-    val p = Pretty.chunks2 (map snd includes @ snd (print_nodes [] nodes));
+    val p = Pretty.chunks2 (map snd includes @ snd (print_nodes [] ml_program));
     fun write width NONE = writeln_pretty width
       | write width (SOME p) = File.write p o string_of_pretty width;
   in