# HG changeset patch # User haftmann # Date 1283354082 -7200 # Node ID 3f70c03e828247fb8924791e0d37eb2bd21b1001 # Parent ac7774a35bcfde91f323af1d9ada8a4e395c7021 simultaneous modification of statements diff -r ac7774a35bcf -r 3f70c03e8282 src/Tools/Code/code_namespace.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; diff -r ac7774a35bcf -r 3f70c03e8282 src/Tools/Code/code_scala.ML --- 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