simultaneous modification of statements
authorhaftmann
Wed, 01 Sep 2010 17:14:42 +0200
changeset 39023 3f70c03e8282
parent 39022 ac7774a35bcf
child 39024 30d5dd2f30b6
simultaneous modification of statements
src/Tools/Code/code_namespace.ML
src/Tools/Code/code_scala.ML
--- a/src/Tools/Code/code_namespace.ML	Wed Sep 01 16:08:31 2010 +0200
+++ b/src/Tools/Code/code_namespace.ML	Wed Sep 01 17:14:42 2010 +0200
@@ -14,10 +14,10 @@
     reserved: Name.context, empty_nsp: 'c, namify_module: string -> 'c -> string * 'c,
     namify_stmt: Code_Thingol.stmt -> string -> 'c -> string * 'c,
     cyclic_modules: bool, empty_data: 'b, memorize_data: string -> 'b -> 'b,
-    modify_stmt: Code_Thingol.stmt -> Code_Thingol.stmt option }
+    modify_stmts: Code_Thingol.stmt list -> 'a option list }
       -> Code_Thingol.program
       -> { deresolver: string list -> string -> string,
-           hierarchical_program: (string * (Code_Thingol.stmt, 'b) node) Graph.T }
+           hierarchical_program: (string * ('a, 'b) node) Graph.T }
 end;
 
 structure Code_Namespace : CODE_NAMESPACE =
@@ -38,7 +38,7 @@
         o map_module name_fragments;
 
 fun hierarchical_program labelled_name { module_alias, reserved, empty_nsp,
-      namify_module, namify_stmt, cyclic_modules, empty_data, memorize_data, modify_stmt } program =
+      namify_module, namify_stmt, cyclic_modules, empty_data, memorize_data, modify_stmts } program =
   let
 
     (* building module name hierarchy *)
@@ -77,8 +77,8 @@
         val (name_fragments', base') = dest_name name';
         val (name_fragments_common, (diff, diff')) =
           chop_prefix (op =) (name_fragments, name_fragments');
-        val (is_module, dep) = if null diff then (false, (name, name'))
-          else (true, (hd diff, hd diff'))
+        val is_module = not (null diff andalso null diff');
+        val dep = pairself hd (diff @ [name], diff' @ [name']);
         val add_edge = if is_module andalso not cyclic_modules
           then (fn node => Graph.add_edge_acyclic dep node
             handle Graph.CYCLES _ => error ("Dependency "
@@ -105,11 +105,15 @@
         val (nsps', nodes') = (nsps, nodes)
           |> fold (declare (K namify_module)) module_fragments
           |> fold (declare (namify_stmt o (fn Stmt stmt => stmt))) stmt_names;
-        val nodes'' = nodes'
-          |> fold (fn name_fragment => (Graph.map_node name_fragment
-              o apsnd o map_module_content) (make_declarations nsps')) module_fragments
-          |> fold (fn name => (Graph.map_node name o apsnd) (fn Stmt stmt =>
-               case modify_stmt stmt of NONE => Dummy | SOME stmt => Stmt stmt)) stmt_names;
+        val modify_stmts' = filter (member (op =) stmt_names)
+          #> AList.make (snd o Graph.get_node nodes)
+          #> split_list
+          ##> map (fn Stmt stmt => stmt)
+          ##> modify_stmts
+          #> op ~~;
+        val stmtss' = maps modify_stmts' (Graph.strong_conn nodes);
+        val nodes'' = Graph.map (fn name => apsnd (fn Module content => Module (make_declarations nsps' content)
+            | _ => case AList.lookup (op =) stmtss' name of SOME (SOME stmt) => Stmt stmt | _ => Dummy)) nodes';
         val data' = fold memorize_data stmt_names data;
       in (data', nodes'') end;
     val (_, hierarchical_program) = make_declarations empty_nsp proto_program;
--- a/src/Tools/Code/code_scala.ML	Wed Sep 01 16:08:31 2010 +0200
+++ b/src/Tools/Code/code_scala.ML	Wed Sep 01 17:14:42 2010 +0200
@@ -193,8 +193,7 @@
                 str "match", str "{"], str "}")
               (map print_clause eqs)
           end;
-    val print_method = str o Library.enclose "`" "`" o space_implode "+"
-      o Long_Name.explode o deresolve_full;
+    val print_method = str o Library.enclose "`" "`" o deresolve_full;
     fun print_stmt (name, Code_Thingol.Fun (_, (((vs, ty), raw_eqs), _))) =
           print_def name (vs, ty) (filter (snd o snd) raw_eqs)
       | print_stmt (name, Code_Thingol.Datatype (_, (vs, cos))) =
@@ -325,7 +324,7 @@
   in
     Code_Namespace.hierarchical_program labelled_name { module_alias = module_alias, reserved = reserved,
       empty_nsp = ((reserved, reserved), reserved), namify_module = namify_module, namify_stmt = namify_stmt,
-      cyclic_modules = true, empty_data = [], memorize_data = memorize_implicits, modify_stmt = modify_stmt } program
+      cyclic_modules = true, empty_data = [], memorize_data = memorize_implicits, modify_stmts = map modify_stmt } program
   end;
 
 fun serialize_scala { labelled_name, reserved_syms, includes,
@@ -368,7 +367,7 @@
       let
         val s = deresolver prefix_fragments implicit;
       in if length (Long_Name.explode s) = 1 then NONE else SOME (str s) end;
-    fun print_node _ (_, Dummy) = NONE
+    fun print_node _ (_, Code_Namespace.Dummy) = NONE
       | print_node prefix_fragments (name, Code_Namespace.Stmt stmt) =
           if null presentation_names
           orelse member (op =) presentation_names name