proper namespace administration for hierarchical modules
authorhaftmann
Fri Aug 27 13:32:05 2010 +0200 (2010-08-27)
changeset 388097dc73a208722
parent 38796 c421cfe2eada
child 38810 361119ea62ee
proper namespace administration for hierarchical modules
src/Tools/Code/code_scala.ML
     1.1 --- a/src/Tools/Code/code_scala.ML	Fri Aug 27 10:57:32 2010 +0200
     1.2 +++ b/src/Tools/Code/code_scala.ML	Fri Aug 27 13:32:05 2010 +0200
     1.3 @@ -27,7 +27,6 @@
     1.4  fun print_scala_stmt labelled_name syntax_tyco syntax_const reserved
     1.5      args_num is_singleton_constr (deresolve, deresolve_full) =
     1.6    let
     1.7 -    val deresolve_base = Long_Name.base_name o deresolve;
     1.8      fun lookup_tyvar tyvars = lookup_var tyvars o first_upper;
     1.9      fun intro_tyvars vs = intro_vars (map (first_upper o fst) vs);
    1.10      fun print_tyco_expr tyvars fxy (tyco, tys) = applify "[" "]"
    1.11 @@ -135,7 +134,7 @@
    1.12      fun print_context tyvars vs name = applify "[" "]"
    1.13        (fn (v, sort) => (Pretty.block o map str)
    1.14          (lookup_tyvar tyvars v :: maps (fn sort => [": ", deresolve sort]) sort))
    1.15 -          NOBR ((str o deresolve_base) name) vs;
    1.16 +          NOBR ((str o deresolve) name) vs;
    1.17      fun print_defhead tyvars vars name vs params tys ty =
    1.18        Pretty.block [str "def ", constraint (applify "(" ")" (fn (param, ty) =>
    1.19          constraint ((str o lookup_var vars) param) (print_typ tyvars NOBR ty))
    1.20 @@ -202,22 +201,22 @@
    1.21            let
    1.22              val tyvars = intro_tyvars vs reserved;
    1.23              fun print_co ((co, _), []) =
    1.24 -                  concat [str "final", str "case", str "object", (str o deresolve_base) co,
    1.25 -                    str "extends", applify "[" "]" I NOBR ((str o deresolve_base) name)
    1.26 +                  concat [str "final", str "case", str "object", (str o deresolve) co,
    1.27 +                    str "extends", applify "[" "]" I NOBR ((str o deresolve) name)
    1.28                        (replicate (length vs) (str "Nothing"))]
    1.29                | print_co ((co, vs_args), tys) =
    1.30                    concat [applify "(" ")"
    1.31                      (fn (v, arg) => constraint (str v) (print_typ tyvars NOBR arg)) NOBR
    1.32                      (applify "[" "]" (str o lookup_tyvar tyvars) NOBR ((concat o map str)
    1.33 -                      ["final", "case", "class", deresolve_base co]) vs_args)
    1.34 +                      ["final", "case", "class", deresolve co]) vs_args)
    1.35                      (Name.names (snd reserved) "a" tys),
    1.36                      str "extends",
    1.37                      applify "[" "]" (str o lookup_tyvar tyvars o fst) NOBR
    1.38 -                      ((str o deresolve_base) name) vs
    1.39 +                      ((str o deresolve) name) vs
    1.40                    ];
    1.41            in
    1.42              Pretty.chunks (applify "[" "]" (str o prefix "+" o lookup_tyvar tyvars o fst)
    1.43 -              NOBR ((concat o map str) ["abstract", "sealed", "class", deresolve_base name]) vs
    1.44 +              NOBR ((concat o map str) ["abstract", "sealed", "class", deresolve name]) vs
    1.45                  :: map print_co cos)
    1.46            end
    1.47        | print_stmt (name, Code_Thingol.Class (_, (v, (super_classes, classparams)))) =
    1.48 @@ -241,7 +240,7 @@
    1.49                in
    1.50                  concat [str "def", constraint (Pretty.block [applify "(" ")"
    1.51                    (fn (aux, ty) => constraint ((str o lookup_var vars) aux)
    1.52 -                  (print_typ tyvars NOBR ty)) NOBR (add_typarg (deresolve_base classparam))
    1.53 +                  (print_typ tyvars NOBR ty)) NOBR (add_typarg (deresolve classparam))
    1.54                    (auxs ~~ tys), str "(implicit ", str implicit_name, str ": ",
    1.55                    add_typarg (deresolve name), str ")"]) (print_typ tyvars NOBR ty), str "=",
    1.56                    applify "(" ")" (str o lookup_var vars) NOBR
    1.57 @@ -250,7 +249,7 @@
    1.58            in
    1.59              Pretty.chunks (
    1.60                (Pretty.block_enclose
    1.61 -                (concat ([str "trait", (add_typarg o deresolve_base) name]
    1.62 +                (concat ([str "trait", (add_typarg o deresolve) name]
    1.63                    @ the_list (print_super_classes super_classes) @ [str "{"]), str "}")
    1.64                  (map print_classparam_val classparams))
    1.65                :: map print_classparam_def classparams
    1.66 @@ -289,7 +288,7 @@
    1.67  datatype node =
    1.68      Dummy
    1.69    | Stmt of Code_Thingol.stmt
    1.70 -  | Module of ((Name.context * Name.context) * Name.context) * (string list * (string * node) Graph.T);
    1.71 +  | Module of (string list * (string * node) Graph.T);
    1.72  
    1.73  in
    1.74  
    1.75 @@ -307,29 +306,53 @@
    1.76      val dest_name = Code_Printer.dest_name #>> (the o Symtab.lookup fragments_tab);
    1.77  
    1.78      (* building empty module hierarchy *)
    1.79 -    val empty_module = (((reserved, reserved), reserved), ([], Graph.empty));
    1.80 +    val empty_module = ([], Graph.empty);
    1.81      fun map_module f (Module content) = Module (f content);
    1.82 -    fun declare_module name_fragement ((nsp_class, nsp_object), nsp_common) =
    1.83 -      let
    1.84 -        val declare = Name.declare name_fragement;
    1.85 -      in ((declare nsp_class, declare nsp_object), declare nsp_common) end;
    1.86 -    fun ensure_module name_fragement (nsps, (implicits, nodes)) =
    1.87 -      if can (Graph.get_node nodes) name_fragement then (nsps, (implicits, nodes))
    1.88 -      else
    1.89 -        (nsps |> declare_module name_fragement, (implicits,
    1.90 -          nodes |> Graph.new_node (name_fragement, (name_fragement, Module empty_module))));
    1.91 +    fun change_module [] = I
    1.92 +      | change_module (name_fragment :: name_fragments) =
    1.93 +          apsnd o Graph.map_node name_fragment o apsnd o map_module
    1.94 +            o change_module name_fragments;
    1.95 +    fun ensure_module name_fragment (implicits, nodes) =
    1.96 +      if can (Graph.get_node nodes) name_fragment then (implicits, nodes)
    1.97 +      else (implicits,
    1.98 +        nodes |> Graph.new_node (name_fragment, (name_fragment, Module empty_module)));
    1.99      fun allocate_module [] = I
   1.100        | allocate_module (name_fragment :: name_fragments) =
   1.101            ensure_module name_fragment
   1.102 -          #> (apsnd o apsnd o Graph.map_node name_fragment o apsnd o map_module o allocate_module) name_fragments;
   1.103 +          #> (apsnd o Graph.map_node name_fragment o apsnd o map_module o allocate_module) name_fragments;
   1.104      val empty_program = Symtab.fold (fn (_, fragments) => allocate_module fragments)
   1.105        fragments_tab empty_module;
   1.106 -    fun change_module [] = I
   1.107 -      | change_module (name_fragment :: name_fragments) =
   1.108 -          apsnd o apsnd o Graph.map_node name_fragment o apsnd o map_module
   1.109 -            o change_module name_fragments;
   1.110  
   1.111 -    (* statement declaration *)
   1.112 +    (* distribute statements over hierarchy *)
   1.113 +    fun add_stmt name stmt =
   1.114 +      let
   1.115 +        val (name_fragments, base) = dest_name name;
   1.116 +        fun is_classinst stmt = case stmt
   1.117 +         of Code_Thingol.Classinst _ => true
   1.118 +          | _ => false;
   1.119 +        val implicit_deps = filter (is_classinst o Graph.get_node program)
   1.120 +          (Graph.imm_succs program name);
   1.121 +      in
   1.122 +        change_module name_fragments (fn (implicits, nodes) =>
   1.123 +          (union (op =) implicit_deps implicits, Graph.new_node (name, (base, Stmt stmt)) nodes))
   1.124 +      end;
   1.125 +    fun add_dependency name name' =
   1.126 +      let
   1.127 +        val (name_fragments, base) = dest_name name;
   1.128 +        val (name_fragments', base') = dest_name name';
   1.129 +        val (name_fragments_common, (diff, diff')) =
   1.130 +          chop_prefix (op =) (name_fragments, name_fragments');
   1.131 +        val dep = if null diff then (name, name') else (hd diff, hd diff')
   1.132 +      in (change_module name_fragments_common o apsnd) (Graph.add_edge dep) end;
   1.133 +    val proto_program = empty_program
   1.134 +      |> Graph.fold (fn (name, (stmt, _)) => add_stmt name stmt) program
   1.135 +      |> Graph.fold (fn (name, (_, (_, names))) => fold (add_dependency name) names) program;
   1.136 +
   1.137 +    (* name declarations *)
   1.138 +    fun namify_module name_fragment ((nsp_class, nsp_object), nsp_common) =
   1.139 +      let
   1.140 +        val declare = Name.declare name_fragment;
   1.141 +      in (name_fragment, ((declare nsp_class, declare nsp_object), declare nsp_common)) end;
   1.142      fun namify_class base ((nsp_class, nsp_object), nsp_common) =
   1.143        let
   1.144          val (base', nsp_class') = yield_singleton Name.variants base nsp_class
   1.145 @@ -346,70 +369,58 @@
   1.146          (base',
   1.147            ((Name.declare base' nsp_class, Name.declare base' nsp_object), nsp_common'))
   1.148        end;
   1.149 -    fun declare_stmt name stmt =
   1.150 +    fun namify_stmt (Code_Thingol.Fun _) = namify_object
   1.151 +      | namify_stmt (Code_Thingol.Datatype _) = namify_class
   1.152 +      | namify_stmt (Code_Thingol.Datatypecons _) = namify_common true
   1.153 +      | namify_stmt (Code_Thingol.Class _) = namify_class
   1.154 +      | namify_stmt (Code_Thingol.Classrel _) = namify_object
   1.155 +      | namify_stmt (Code_Thingol.Classparam _) = namify_object
   1.156 +      | namify_stmt (Code_Thingol.Classinst _) = namify_common false;
   1.157 +    fun make_declarations nsps (implicits, nodes) =
   1.158        let
   1.159 -        val (name_fragments, base) = dest_name name;
   1.160 -        val namify = case stmt
   1.161 -         of Code_Thingol.Fun _ => namify_object
   1.162 -          | Code_Thingol.Datatype _ => namify_class
   1.163 -          | Code_Thingol.Datatypecons _ => namify_common true
   1.164 -          | Code_Thingol.Class _ => namify_class
   1.165 -          | Code_Thingol.Classrel _ => namify_object
   1.166 -          | Code_Thingol.Classparam _ => namify_object
   1.167 -          | Code_Thingol.Classinst _ => namify_common false;
   1.168 -        val stmt' = case stmt
   1.169 -         of Code_Thingol.Datatypecons _ => Dummy
   1.170 -          | Code_Thingol.Classrel _ => Dummy
   1.171 -          | Code_Thingol.Classparam _ => Dummy
   1.172 -          | _ => Stmt stmt;
   1.173 -        fun is_classinst stmt = case stmt
   1.174 -         of Code_Thingol.Classinst _ => true
   1.175 -          | _ => false;
   1.176 -        val implicit_deps = filter (is_classinst o Graph.get_node program)
   1.177 -          (Graph.imm_succs program name);
   1.178 -        fun declaration (nsps, (implicits, nodes)) =
   1.179 +        val (module_fragments, stmt_names) = List.partition
   1.180 +          (fn name_fragment => case Graph.get_node nodes name_fragment
   1.181 +            of (_, Module _) => true | _ => false) (Graph.keys nodes);
   1.182 +        fun modify_stmt (Stmt (Code_Thingol.Datatypecons _)) = Dummy
   1.183 +          | modify_stmt (Stmt (Code_Thingol.Classrel _)) = Dummy
   1.184 +          | modify_stmt (Stmt (Code_Thingol.Classparam _)) = Dummy
   1.185 +          | modify_stmt stmt = stmt;
   1.186 +        fun declare namify modify name (nsps, nodes) =
   1.187            let
   1.188 -            val (base', nsps') = namify base nsps;
   1.189 -            val implicits' = union (op =) implicit_deps implicits;
   1.190 -            val nodes' = Graph.new_node (name, (base', stmt')) nodes;
   1.191 -          in (nsps', (implicits', nodes')) end;
   1.192 -      in change_module name_fragments declaration end;
   1.193 -
   1.194 -    (* dependencies *)
   1.195 -    fun add_dependency name name' =
   1.196 -      let
   1.197 -        val (name_fragments, base) = dest_name name;
   1.198 -        val (name_fragments', base') = dest_name name';
   1.199 -        val (name_fragments_common, (diff, diff')) =
   1.200 -          chop_prefix (op =) (name_fragments, name_fragments');
   1.201 -        val dep = if null diff then (name, name') else (hd diff, hd diff')
   1.202 -      in (change_module name_fragments_common o apsnd o apsnd) (Graph.add_edge dep) end;
   1.203 -
   1.204 -    (* producing program *)
   1.205 -    val (_, (_, sca_program)) = empty_program
   1.206 -      |> Graph.fold (fn (name, (stmt, _)) => declare_stmt name stmt) program
   1.207 -      |> Graph.fold (fn (name, (_, (_, names))) => fold (add_dependency name) names) program;
   1.208 +            val (base, node) = Graph.get_node nodes name;
   1.209 +            val (base', nsps') = namify node base nsps;
   1.210 +            val nodes' = Graph.map_node name (K (base', modify node)) nodes;
   1.211 +          in (nsps', nodes') end;
   1.212 +        val (nsps', nodes') = (nsps, nodes)
   1.213 +          |> fold (declare (K namify_module) I) module_fragments
   1.214 +          |> fold (declare (namify_stmt o (fn Stmt stmt => stmt)) modify_stmt) stmt_names;
   1.215 +        val nodes'' = nodes'
   1.216 +          |> fold (fn name_fragment => (Graph.map_node name_fragment
   1.217 +              o apsnd o map_module) (make_declarations nsps')) module_fragments;
   1.218 +      in (implicits, nodes'') end;
   1.219 +    val (_, sca_program) = make_declarations ((reserved, reserved), reserved) proto_program;
   1.220  
   1.221      (* deresolving *)
   1.222 -    fun deresolve name =
   1.223 +    fun deresolver prefix_fragments name =
   1.224        let
   1.225          val (name_fragments, _) = dest_name name;
   1.226 -        val nodes = fold (fn name_fragement => fn nodes => case Graph.get_node nodes name_fragement
   1.227 -         of (_, Module (_, (_, nodes))) => nodes) name_fragments sca_program;
   1.228 +        val (_, (_, remainder)) = chop_prefix (op =) (prefix_fragments, name_fragments);
   1.229 +        val nodes = fold (fn name_fragment => fn nodes => case Graph.get_node nodes name_fragment
   1.230 +         of (_, Module (_, nodes)) => nodes) name_fragments sca_program;
   1.231          val (base', _) = Graph.get_node nodes name;
   1.232 -      in Long_Name.implode (name_fragments @ [base']) end
   1.233 +      in Long_Name.implode (remainder @ [base']) end
   1.234          handle Graph.UNDEF _ => error ("Unknown statement name: " ^ labelled_name name);
   1.235  
   1.236 -  in (deresolve, sca_program) end;
   1.237 +  in (deresolver, sca_program) end;
   1.238  
   1.239  fun serialize_scala labelled_name raw_reserved includes module_alias
   1.240      _ syntax_tyco syntax_const (code_of_pretty, code_writeln)
   1.241      program (stmt_names, presentation_stmt_names) destination =
   1.242    let
   1.243  
   1.244 -    (* preprocess program *)
   1.245 +    (* build program *)
   1.246      val reserved = fold (insert (op =) o fst) includes raw_reserved;
   1.247 -    val (deresolve, sca_program) = scala_program_of_program labelled_name
   1.248 +    val (deresolver, sca_program) = scala_program_of_program labelled_name
   1.249        (Name.make_context reserved) module_alias program;
   1.250  
   1.251      (* print statements *)
   1.252 @@ -430,41 +441,44 @@
   1.253       of Code_Thingol.Datatypecons (_, tyco) => null (lookup_constr tyco c)
   1.254        | _ => false;
   1.255      val print_stmt = print_scala_stmt labelled_name syntax_tyco syntax_const
   1.256 -      (make_vars reserved) args_num is_singleton_constr
   1.257 -      (deresolve, Long_Name.implode o fst o split_last o Long_Name.explode (*FIXME full*));
   1.258 +      (make_vars reserved) args_num is_singleton_constr;
   1.259  
   1.260      (* print nodes *)
   1.261 -    fun print_implicit implicit =
   1.262 +    fun print_implicit prefix_fragments implicit =
   1.263        let
   1.264 -        val s = deresolve implicit;
   1.265 +        val s = deresolver prefix_fragments implicit;
   1.266        in if length (Long_Name.explode s) = 1 then NONE else SOME (str s) end;
   1.267 -    fun print_implicits implicits = case map_filter print_implicit implicits
   1.268 -     of [] => NONE
   1.269 -      | ps => (SOME o Pretty.block)
   1.270 -          (str "import /*implicits*/" :: Pretty.brk 1 :: commas ps);
   1.271 -    fun print_module base implicits p = Pretty.chunks2
   1.272 -      ([str ("object " ^ base ^ " {")] @ the_list (print_implicits implicits)
   1.273 +    fun print_implicits prefix_fragments implicits =
   1.274 +      case map_filter (print_implicit prefix_fragments) implicits
   1.275 +       of [] => NONE
   1.276 +        | ps => (SOME o Pretty.block)
   1.277 +            (str "import /*implicits*/" :: Pretty.brk 1 :: commas ps);
   1.278 +    fun print_module prefix_fragments base implicits p = Pretty.chunks2
   1.279 +      ([str ("object " ^ base ^ " {")] @ the_list (print_implicits prefix_fragments implicits)
   1.280          @ [p, str ("} /* object " ^ base ^ " */")]);
   1.281 -    fun print_node (_, Dummy) = NONE
   1.282 -      | print_node (name, Stmt stmt) = if null presentation_stmt_names
   1.283 +    fun print_node _ (_, Dummy) = NONE
   1.284 +      | print_node prefix_fragments (name, Stmt stmt) =
   1.285 +          if null presentation_stmt_names
   1.286            orelse member (op =) presentation_stmt_names name
   1.287 -          then SOME (print_stmt (name, stmt))
   1.288 +          then SOME (print_stmt (deresolver prefix_fragments, deresolver []) (name, stmt))
   1.289            else NONE
   1.290 -      | print_node (name, Module (_, (implicits, nodes))) = if null presentation_stmt_names
   1.291 -          then case print_nodes nodes
   1.292 +      | print_node prefix_fragments (name_fragment, Module (implicits, nodes)) =
   1.293 +          if null presentation_stmt_names
   1.294 +          then case print_nodes (prefix_fragments @ [name_fragment]) nodes
   1.295             of NONE => NONE
   1.296 -            | SOME p => SOME (print_module (Long_Name.base_name name) implicits p)
   1.297 -          else print_nodes nodes
   1.298 -    and print_nodes nodes = let
   1.299 -        val ps = map_filter (fn name => print_node (name,
   1.300 +            | SOME p => SOME (print_module prefix_fragments
   1.301 +                (Long_Name.base_name name_fragment) implicits p)
   1.302 +          else print_nodes [] nodes
   1.303 +    and print_nodes prefix_fragments nodes = let
   1.304 +        val ps = map_filter (fn name => print_node prefix_fragments (name,
   1.305            snd (Graph.get_node nodes name)))
   1.306              ((rev o flat o Graph.strong_conn) nodes);
   1.307        in if null ps then NONE else SOME (Pretty.chunks2 ps) end;
   1.308  
   1.309      (* serialization *)
   1.310      val p_includes = if null presentation_stmt_names
   1.311 -      then map (fn (base, p) => print_module base [] p) includes else [];
   1.312 -    val p = Pretty.chunks2 (p_includes @ the_list (print_nodes sca_program));
   1.313 +      then map (fn (base, p) => print_module [] base [] p) includes else [];
   1.314 +    val p = Pretty.chunks2 (p_includes @ the_list (print_nodes [] sca_program));
   1.315    in
   1.316      Code_Target.mk_serialization target
   1.317        (fn NONE => code_writeln | SOME file => File.write file o code_of_pretty)