src/Tools/Code/code_namespace.ML
changeset 52138 e21426f244aa
parent 51930 52fd62618631
child 53414 dd64696d267a
     1.1 --- a/src/Tools/Code/code_namespace.ML	Fri May 24 23:57:24 2013 +0200
     1.2 +++ b/src/Tools/Code/code_namespace.ML	Fri May 24 23:57:24 2013 +0200
     1.3 @@ -7,8 +7,9 @@
     1.4  signature CODE_NAMESPACE =
     1.5  sig
     1.6    type flat_program
     1.7 -  val flat_program: (string -> string) -> { module_alias: string -> string option,
     1.8 -    module_prefix: string, reserved: Name.context, empty_nsp: 'a,
     1.9 +  val flat_program: Proof.context -> (string -> Code_Symbol.symbol)
    1.10 +    -> { module_prefix: string, module_name: string,
    1.11 +    reserved: Name.context, identifiers: Code_Target.identifier_data, empty_nsp: 'a,
    1.12      namify_stmt: Code_Thingol.stmt -> string -> 'a -> string * 'a,
    1.13      modify_stmt: Code_Thingol.stmt -> Code_Thingol.stmt option }
    1.14        -> Code_Thingol.program
    1.15 @@ -20,8 +21,10 @@
    1.16      | Stmt of 'a
    1.17      | Module of ('b * (string * ('a, 'b) node) Graph.T)
    1.18    type ('a, 'b) hierarchical_program
    1.19 -  val hierarchical_program: (string -> string) -> { module_alias: string -> string option,
    1.20 -    reserved: Name.context, empty_nsp: 'c, namify_module: string -> 'c -> string * 'c,
    1.21 +  val hierarchical_program: Proof.context -> (string -> Code_Symbol.symbol)
    1.22 +    -> { module_name: string,
    1.23 +    reserved: Name.context, identifiers: Code_Target.identifier_data,
    1.24 +    empty_nsp: 'c, namify_module: string -> 'c -> string * 'c,
    1.25      namify_stmt: Code_Thingol.stmt -> string -> 'c -> string * 'c,
    1.26      cyclic_modules: bool, empty_data: 'b, memorize_data: string -> 'b -> 'b,
    1.27      modify_stmts: (string * Code_Thingol.stmt) list -> 'a option list }
    1.28 @@ -37,17 +40,25 @@
    1.29  structure Code_Namespace : CODE_NAMESPACE =
    1.30  struct
    1.31  
    1.32 -(** building module name hierarchy **)
    1.33 +(** fundamental module name hierarchy **)
    1.34 +
    1.35 +val split_name = apfst Long_Name.implode o split_last o fst o split_last o Long_Name.explode;
    1.36 +
    1.37 +fun lookup_identifier symbol_of identifiers name =
    1.38 +  Code_Symbol.lookup identifiers (symbol_of name)
    1.39 +  |> Option.map (split_last o Long_Name.explode);
    1.40  
    1.41 -val dest_name =
    1.42 -  apfst Long_Name.implode o split_last o fst o split_last o Long_Name.explode;
    1.43 +fun force_identifier symbol_of fragments_tab identifiers name =
    1.44 +  case lookup_identifier symbol_of identifiers name of
    1.45 +      NONE => (apfst (the o Symtab.lookup fragments_tab) o split_name) name
    1.46 +    | SOME name' => name';
    1.47  
    1.48 -fun build_module_namespace { module_alias, module_prefix, reserved } program =
    1.49 +fun build_module_namespace { module_prefix, module_identifiers, reserved } program =
    1.50    let
    1.51 -    fun alias_fragments name = case module_alias name
    1.52 +    fun alias_fragments name = case module_identifiers name
    1.53       of SOME name' => Long_Name.explode name'
    1.54        | NONE => map (fn name => fst (Name.variant name reserved)) (Long_Name.explode name);
    1.55 -    val module_names = Graph.fold (insert (op =) o fst o dest_name o fst) program [];
    1.56 +    val module_names = Graph.fold (insert (op =) o fst o split_name o fst) program [];
    1.57    in
    1.58      fold (fn name => Symtab.update (name, Long_Name.explode module_prefix @ alias_fragments name))
    1.59        module_names Symtab.empty
    1.60 @@ -58,28 +69,31 @@
    1.61  
    1.62  type flat_program = ((string * Code_Thingol.stmt option) Graph.T * (string * string list) list) Graph.T;
    1.63  
    1.64 -fun flat_program labelled_name { module_alias, module_prefix, reserved,
    1.65 -      empty_nsp, namify_stmt, modify_stmt } program =
    1.66 +fun flat_program ctxt symbol_of { module_prefix, module_name, reserved,
    1.67 +    identifiers, empty_nsp, namify_stmt, modify_stmt } program =
    1.68    let
    1.69  
    1.70      (* building module name hierarchy *)
    1.71 -    val fragments_tab = build_module_namespace { module_alias = module_alias,
    1.72 -      module_prefix = module_prefix, reserved = reserved } program;
    1.73 -    val dest_name = dest_name
    1.74 -      #>> (Long_Name.implode o the o Symtab.lookup fragments_tab);
    1.75 +    val module_identifiers = if module_name = ""
    1.76 +      then Code_Symbol.lookup_module_data identifiers
    1.77 +      else K (SOME module_name);
    1.78 +    val fragments_tab = build_module_namespace { module_prefix = module_prefix,
    1.79 +      module_identifiers = module_identifiers, reserved = reserved } program;
    1.80 +    val prep_name = force_identifier symbol_of fragments_tab identifiers
    1.81 +      #>> Long_Name.implode;
    1.82  
    1.83      (* distribute statements over hierarchy *)
    1.84      fun add_stmt name stmt =
    1.85        let
    1.86 -        val (module_name, base) = dest_name name;
    1.87 +        val (module_name, base) = prep_name name;
    1.88        in
    1.89          Graph.default_node (module_name, (Graph.empty, []))
    1.90          #> (Graph.map_node module_name o apfst) (Graph.new_node (name, (base, stmt)))
    1.91        end;
    1.92      fun add_dependency name name' =
    1.93        let
    1.94 -        val (module_name, _) = dest_name name;
    1.95 -        val (module_name', _) = dest_name name';
    1.96 +        val (module_name, _) = prep_name name;
    1.97 +        val (module_name', _) = prep_name name';
    1.98        in if module_name = module_name'
    1.99          then (Graph.map_node module_name o apfst) (Graph.add_edge (name, name'))
   1.100          else (Graph.map_node module_name o apsnd) (AList.map_default (op =) (module_name', []) (insert (op =) name'))
   1.101 @@ -104,7 +118,7 @@
   1.102  
   1.103      (* qualified and unqualified imports, deresolving *)
   1.104      fun base_deresolver name = fst (Graph.get_node
   1.105 -      (fst (Graph.get_node flat_program (fst (dest_name name)))) name);
   1.106 +      (fst (Graph.get_node flat_program (fst (prep_name name)))) name);
   1.107      fun classify_names gr imports =
   1.108        let
   1.109          val import_tab = maps
   1.110 @@ -122,10 +136,11 @@
   1.111        (uncurry classify_names o Graph.get_node flat_program)
   1.112          (Graph.keys flat_program));
   1.113      fun deresolver "" name =
   1.114 -          Long_Name.append (fst (dest_name name)) (base_deresolver name)
   1.115 +          Long_Name.append (fst (prep_name name)) (base_deresolver name)
   1.116        | deresolver module_name name =
   1.117            the (Symtab.lookup (the (Symtab.lookup deresolver_tab module_name)) name)
   1.118 -          handle Option.Option => error ("Unknown statement name: " ^ labelled_name name);
   1.119 +          handle Option.Option => error ("Unknown statement name: "
   1.120 +            ^ (Code_Symbol.quote_symbol ctxt o symbol_of) name);
   1.121  
   1.122    in { deresolver = deresolver, flat_program = flat_program } end;
   1.123  
   1.124 @@ -146,14 +161,17 @@
   1.125        apsnd o Graph.map_node name_fragment o apsnd o map_module_content
   1.126          o map_module name_fragments;
   1.127  
   1.128 -fun hierarchical_program labelled_name { module_alias, reserved, empty_nsp,
   1.129 +fun hierarchical_program ctxt symbol_of { module_name, reserved, identifiers, empty_nsp,
   1.130        namify_module, namify_stmt, cyclic_modules, empty_data, memorize_data, modify_stmts } program =
   1.131    let
   1.132  
   1.133      (* building module name hierarchy *)
   1.134 -    val fragments_tab = build_module_namespace { module_alias = module_alias,
   1.135 -      module_prefix = "", reserved = reserved } program;
   1.136 -    val dest_name = dest_name #>> (the o Symtab.lookup fragments_tab);
   1.137 +    val module_identifiers = if module_name = ""
   1.138 +      then Code_Symbol.lookup_module_data identifiers
   1.139 +      else K (SOME module_name);
   1.140 +    val fragments_tab = build_module_namespace { module_prefix = "",
   1.141 +      module_identifiers = module_identifiers, reserved = reserved } program;
   1.142 +    val prep_name = force_identifier symbol_of fragments_tab identifiers;
   1.143  
   1.144      (* building empty module hierarchy *)
   1.145      val empty_module = (empty_data, Graph.empty);
   1.146 @@ -165,20 +183,23 @@
   1.147        | allocate_module (name_fragment :: name_fragments) =
   1.148            ensure_module name_fragment
   1.149            #> (apsnd o Graph.map_node name_fragment o apsnd o map_module_content o allocate_module) name_fragments;
   1.150 -    val empty_program = Symtab.fold (fn (_, fragments) => allocate_module fragments)
   1.151 -      fragments_tab empty_module;
   1.152 +    val empty_program =
   1.153 +      empty_module
   1.154 +      |> Symtab.fold (fn (_, fragments) => allocate_module fragments) fragments_tab
   1.155 +      |> Graph.fold (allocate_module o these o Option.map fst
   1.156 +          o lookup_identifier symbol_of identifiers o fst) program;
   1.157  
   1.158      (* distribute statements over hierarchy *)
   1.159      fun add_stmt name stmt =
   1.160        let
   1.161 -        val (name_fragments, base) = dest_name name;
   1.162 +        val (name_fragments, base) = prep_name name;
   1.163        in
   1.164          (map_module name_fragments o apsnd) (Graph.new_node (name, (base, Stmt stmt)))
   1.165        end;
   1.166      fun add_dependency name name' =
   1.167        let
   1.168 -        val (name_fragments, _) = dest_name name;
   1.169 -        val (name_fragments', _) = dest_name name';
   1.170 +        val (name_fragments, _) = prep_name name;
   1.171 +        val (name_fragments', _) = prep_name name';
   1.172          val (name_fragments_common, (diff, diff')) =
   1.173            chop_prefix (op =) (name_fragments, name_fragments');
   1.174          val is_module = not (null diff andalso null diff');
   1.175 @@ -186,7 +207,8 @@
   1.176          val add_edge = if is_module andalso not cyclic_modules
   1.177            then (fn node => Graph.add_edge_acyclic dep node
   1.178              handle Graph.CYCLES _ => error ("Dependency "
   1.179 -              ^ quote name ^ " -> " ^ quote name'
   1.180 +              ^ (Code_Symbol.quote_symbol ctxt o symbol_of) name ^ " -> "
   1.181 +              ^ (Code_Symbol.quote_symbol ctxt o symbol_of) name'
   1.182                ^ " would result in module dependency cycle"))
   1.183            else Graph.add_edge dep
   1.184        in (map_module name_fragments_common o apsnd) add_edge end;
   1.185 @@ -228,13 +250,14 @@
   1.186      (* deresolving *)
   1.187      fun deresolver prefix_fragments name =
   1.188        let
   1.189 -        val (name_fragments, _) = dest_name name;
   1.190 +        val (name_fragments, _) = prep_name name;
   1.191          val (_, (_, remainder)) = chop_prefix (op =) (prefix_fragments, name_fragments);
   1.192          val nodes = fold (fn name_fragment => fn nodes => case Graph.get_node nodes name_fragment
   1.193           of (_, Module (_, nodes)) => nodes) name_fragments hierarchical_program;
   1.194          val (base', _) = Graph.get_node nodes name;
   1.195        in Long_Name.implode (remainder @ [base']) end
   1.196 -        handle Graph.UNDEF _ => error ("Unknown statement name: " ^ labelled_name name);
   1.197 +        handle Graph.UNDEF _ => error ("Unknown statement name: "
   1.198 +          ^ (Code_Symbol.quote_symbol ctxt o symbol_of) name);
   1.199  
   1.200    in { deresolver = deresolver, hierarchical_program = hierarchical_program } end;
   1.201