code generation: explicitly declared identifiers gain predence over implicit ones
authorhaftmann
Mon Feb 03 08:23:21 2014 +0100 (2014-02-03)
changeset 5529342cf5802d36a
parent 55292 1e973b665b98
child 55294 6f77310a0907
code generation: explicitly declared identifiers gain predence over implicit ones
src/Doc/IsarRef/HOL_Specific.thy
src/Tools/Code/code_namespace.ML
     1.1 --- a/src/Doc/IsarRef/HOL_Specific.thy	Mon Feb 03 08:23:20 2014 +0100
     1.2 +++ b/src/Doc/IsarRef/HOL_Specific.thy	Mon Feb 03 08:23:21 2014 +0100
     1.3 @@ -2640,9 +2640,11 @@
     1.4    \item @{command (HOL) "code_identifier"} associates a a series of symbols
     1.5    (constants, type constructors, classes, class relations, instances,
     1.6    module names) with target-specific hints how these symbols shall be named.
     1.7 -  \emph{Warning:} These hints are still subject to name disambiguation.
     1.8 +  These hints gain precedence over names for symbols with no hints at all.
     1.9 +  Conflicting hints are subject to name disambiguation.
    1.10    @{command (HOL) "code_modulename"} is a legacy variant for
    1.11 -  @{command (HOL) "code_identifier"} on module names.  It is at the discretion
    1.12 +  @{command (HOL) "code_identifier"} on module names.
    1.13 +  \emph{Warning:} It is at the discretion
    1.14    of the user to ensure that name prefixes of identifiers in compound
    1.15    statements like type classes or datatypes are still the same.
    1.16  
     2.1 --- a/src/Tools/Code/code_namespace.ML	Mon Feb 03 08:23:20 2014 +0100
     2.2 +++ b/src/Tools/Code/code_namespace.ML	Mon Feb 03 08:23:21 2014 +0100
     2.3 @@ -69,12 +69,16 @@
     2.4      | SOME prefix_name => if null force_module then prefix_name
     2.5          else (force_module, snd prefix_name);
     2.6  
     2.7 +fun has_priority identifiers = is_some o Code_Symbol.lookup identifiers;
     2.8 +
     2.9  fun build_proto_program { empty, add_stmt, add_dep } program =
    2.10    empty
    2.11    |> Code_Symbol.Graph.fold (fn (sym, (stmt, _)) => add_stmt sym stmt) program
    2.12    |> Code_Symbol.Graph.fold (fn (sym, (_, (_, syms))) =>
    2.13        Code_Symbol.Graph.Keys.fold (add_dep sym) syms) program;
    2.14  
    2.15 +fun prioritize has_priority = uncurry append o List.partition has_priority;
    2.16 +
    2.17  
    2.18  (** flat program structure **)
    2.19  
    2.20 @@ -90,6 +94,7 @@
    2.21      val prep_sym = prep_symbol ctxt { module_namespace = module_namespace,
    2.22        force_module = Long_Name.explode module_name, identifiers = identifiers }
    2.23        #>> Long_Name.implode;
    2.24 +    val sym_priority = has_priority identifiers;
    2.25  
    2.26      (* distribute statements over hierarchy *)
    2.27      fun add_stmt sym stmt =
    2.28 @@ -117,7 +122,8 @@
    2.29          val gr' = (Code_Symbol.Graph.map_node sym o apfst) (K base') gr;
    2.30        in (gr', nsp') end;
    2.31      fun declarations gr = (gr, empty_nsp)
    2.32 -      |> fold (fn sym => declare sym (Code_Symbol.Graph.get_node gr sym)) (Code_Symbol.Graph.keys gr) 
    2.33 +      |> fold (fn sym => declare sym (Code_Symbol.Graph.get_node gr sym))
    2.34 +          (prioritize sym_priority (Code_Symbol.Graph.keys gr))
    2.35        |> fst
    2.36        |> (Code_Symbol.Graph.map o K o apsnd) modify_stmt;
    2.37      val flat_program = proto_program
    2.38 @@ -176,7 +182,8 @@
    2.39      val module_namespace = build_module_namespace ctxt { module_prefix = "",
    2.40        module_name = module_name, identifiers = identifiers, reserved = reserved } program;
    2.41      val prep_sym = prep_symbol ctxt { module_namespace = module_namespace,
    2.42 -      force_module = Long_Name.explode module_name, identifiers = identifiers };
    2.43 +      force_module = Long_Name.explode module_name, identifiers = identifiers }
    2.44 +    val sym_priority = has_priority identifiers;
    2.45  
    2.46      (* building empty module hierarchy *)
    2.47      val empty_module = (empty_data, Code_Symbol.Graph.empty);
    2.48 @@ -223,9 +230,12 @@
    2.49      (* name declarations, data and statement modifications *)
    2.50      fun make_declarations nsps (data, nodes) =
    2.51        let
    2.52 -        val (module_fragments, stmt_syms) = List.partition
    2.53 -          (fn sym => case Code_Symbol.Graph.get_node nodes sym
    2.54 -            of (_, Module _) => true | _ => false) (Code_Symbol.Graph.keys nodes);
    2.55 +        val (module_fragments, stmt_syms) =
    2.56 +          Code_Symbol.Graph.keys nodes
    2.57 +          |> List.partition
    2.58 +              (fn sym => case Code_Symbol.Graph.get_node nodes sym
    2.59 +                of (_, Module _) => true | _ => false)
    2.60 +          |> pairself (prioritize sym_priority)
    2.61          fun declare namify sym (nsps, nodes) =
    2.62            let
    2.63              val (base, node) = Code_Symbol.Graph.get_node nodes sym;