src/Tools/Code/code_namespace.ML
changeset 39029 cef7b58555aa
parent 39024 30d5dd2f30b6
child 39055 81e0368812ad
equal deleted inserted replaced
39028:0dd6c5a0beef 39029:cef7b58555aa
   103             val nodes' = Graph.map_node name (K (base', node)) nodes;
   103             val nodes' = Graph.map_node name (K (base', node)) nodes;
   104           in (nsps', nodes') end;
   104           in (nsps', nodes') end;
   105         val (nsps', nodes') = (nsps, nodes)
   105         val (nsps', nodes') = (nsps, nodes)
   106           |> fold (declare (K namify_module)) module_fragments
   106           |> fold (declare (K namify_module)) module_fragments
   107           |> fold (declare (namify_stmt o (fn Stmt stmt => stmt))) stmt_names;
   107           |> fold (declare (namify_stmt o (fn Stmt stmt => stmt))) stmt_names;
   108         val modify_stmts' = filter (member (op =) stmt_names)
   108         fun zip_fillup xs ys = xs ~~ ys @ replicate (length xs - length ys) NONE;
   109           #> AList.make (snd o Graph.get_node nodes)
   109         fun select_names names = case filter (member (op =) stmt_names) names
       
   110          of [] => NONE
       
   111           | xs => SOME xs;
       
   112         val modify_stmts' = AList.make (snd o Graph.get_node nodes)
   110           #> split_list
   113           #> split_list
   111           ##> map (fn Stmt stmt => stmt)
   114           ##> map (fn Stmt stmt => stmt)
   112           #> (fn (names, stmts) => names ~~ modify_stmts (names ~~ stmts));
   115           #> (fn (names, stmts) => zip_fillup names (modify_stmts (names ~~ stmts)));
   113         val stmtss' = maps modify_stmts' (Graph.strong_conn nodes);
   116         val stmtss' = (maps modify_stmts' o map_filter select_names o Graph.strong_conn) nodes;
   114         val nodes'' = Graph.map (fn name => apsnd (fn Module content => Module (make_declarations nsps' content)
   117         val nodes'' = Graph.map (fn name => apsnd (fn Module content => Module (make_declarations nsps' content)
   115             | _ => case AList.lookup (op =) stmtss' name of SOME (SOME stmt) => Stmt stmt | _ => Dummy)) nodes';
   118             | _ => case AList.lookup (op =) stmtss' name of SOME (SOME stmt) => Stmt stmt | _ => Dummy)) nodes';
   116         val data' = fold memorize_data stmt_names data;
   119         val data' = fold memorize_data stmt_names data;
   117       in (data', nodes'') end;
   120       in (data', nodes'') end;
   118     val (_, hierarchical_program) = make_declarations empty_nsp proto_program;
   121     val (_, hierarchical_program) = make_declarations empty_nsp proto_program;