src/Tools/Code/code_namespace.ML
changeset 55679 59244fc1a7ca
parent 55605 b1b363e81c87
child 55680 bc5edc5dbf18
     1.1 --- a/src/Tools/Code/code_namespace.ML	Sun Feb 23 10:33:43 2014 +0100
     1.2 +++ b/src/Tools/Code/code_namespace.ML	Sun Feb 23 10:33:43 2014 +0100
     1.3 @@ -18,7 +18,7 @@
     1.4  
     1.5    datatype ('a, 'b) node =
     1.6        Dummy
     1.7 -    | Stmt of 'a
     1.8 +    | Stmt of bool * 'a
     1.9      | Module of ('b * (string * ('a, 'b) node) Code_Symbol.Graph.T)
    1.10    type ('a, 'b) hierarchical_program
    1.11    val hierarchical_program: Proof.context
    1.12 @@ -32,7 +32,7 @@
    1.13        -> { deresolver: string list -> Code_Symbol.T -> string,
    1.14             hierarchical_program: ('a, 'b) hierarchical_program }
    1.15    val print_hierarchical: { print_module: string list -> string -> 'b -> 'c list -> 'c,
    1.16 -    print_stmt: string list -> Code_Symbol.T * 'a -> 'c,
    1.17 +    print_stmt: string list -> Code_Symbol.T * (bool * 'a) -> 'c,
    1.18      lift_markup: (Pretty.T -> Pretty.T) -> 'c -> 'c }
    1.19        -> ('a, 'b) hierarchical_program -> 'c list
    1.20  end;
    1.21 @@ -82,7 +82,7 @@
    1.22  
    1.23  (** flat program structure **)
    1.24  
    1.25 -type flat_program = ((string * Code_Thingol.stmt option) Code_Symbol.Graph.T * (string * Code_Symbol.T list) list) Graph.T;
    1.26 +type flat_program = ((string * (bool * Code_Thingol.stmt) option) Code_Symbol.Graph.T * (string * Code_Symbol.T list) list) Graph.T;
    1.27  
    1.28  fun flat_program ctxt { module_prefix, module_name, reserved,
    1.29      identifiers, empty_nsp, namify_stmt, modify_stmt } program =
    1.30 @@ -102,7 +102,7 @@
    1.31          val (module_name, base) = prep_sym sym;
    1.32        in
    1.33          Graph.default_node (module_name, (Code_Symbol.Graph.empty, []))
    1.34 -        #> (Graph.map_node module_name o apfst) (Code_Symbol.Graph.new_node (sym, (base, stmt)))
    1.35 +        #> (Graph.map_node module_name o apfst) (Code_Symbol.Graph.new_node (sym, (base, (true, stmt))))
    1.36        end;
    1.37      fun add_dep sym sym' =
    1.38        let
    1.39 @@ -116,7 +116,7 @@
    1.40        { empty = Graph.empty, add_stmt = add_stmt, add_dep = add_dep } program;
    1.41  
    1.42      (* name declarations and statement modifications *)
    1.43 -    fun declare sym (base, stmt) (gr, nsp) = 
    1.44 +    fun declare sym (base, (_, stmt)) (gr, nsp) = 
    1.45        let
    1.46          val (base', nsp') = namify_stmt stmt base nsp;
    1.47          val gr' = (Code_Symbol.Graph.map_node sym o apfst) (K base') gr;
    1.48 @@ -125,7 +125,8 @@
    1.49        |> fold (fn sym => declare sym (Code_Symbol.Graph.get_node gr sym))
    1.50            (prioritize sym_priority (Code_Symbol.Graph.keys gr))
    1.51        |> fst
    1.52 -      |> (Code_Symbol.Graph.map o K o apsnd) modify_stmt;
    1.53 +      |> (Code_Symbol.Graph.map o K o apsnd)
    1.54 +        (fn (export, stmt) => Option.map (pair export) (modify_stmt stmt));
    1.55      val flat_program = proto_program
    1.56        |> (Graph.map o K o apfst) declarations;
    1.57  
    1.58 @@ -162,11 +163,13 @@
    1.59  
    1.60  datatype ('a, 'b) node =
    1.61      Dummy
    1.62 -  | Stmt of 'a
    1.63 +  | Stmt of bool * 'a
    1.64    | Module of ('b * (string * ('a, 'b) node) Code_Symbol.Graph.T);
    1.65  
    1.66  type ('a, 'b) hierarchical_program = (string * ('a, 'b) node) Code_Symbol.Graph.T;
    1.67  
    1.68 +fun the_stmt (Stmt (export, stmt)) = (export, stmt);
    1.69 +
    1.70  fun map_module_content f (Module content) = Module (f content);
    1.71  
    1.72  fun map_module [] = I
    1.73 @@ -206,7 +209,7 @@
    1.74        let
    1.75          val (name_fragments, base) = prep_sym sym;
    1.76        in
    1.77 -        (map_module name_fragments o apsnd) (Code_Symbol.Graph.new_node (sym, (base, Stmt stmt)))
    1.78 +        (map_module name_fragments o apsnd) (Code_Symbol.Graph.new_node (sym, (base, Stmt (true, stmt))))
    1.79        end;
    1.80      fun add_dep sym sym' =
    1.81        let
    1.82 @@ -244,18 +247,18 @@
    1.83            in (nsps', nodes') end;
    1.84          val (nsps', nodes') = (nsps, nodes)
    1.85            |> fold (declare (K namify_module)) module_fragments
    1.86 -          |> fold (declare (namify_stmt o (fn Stmt stmt => stmt))) stmt_syms;
    1.87 +          |> fold (declare (namify_stmt o snd o the_stmt)) stmt_syms;
    1.88          fun select_syms syms = case filter (member (op =) stmt_syms) syms
    1.89           of [] => NONE
    1.90            | syms => SOME syms;
    1.91 -        fun select_stmt (sym, SOME stmt) = SOME (sym, stmt)
    1.92 +        fun select_stmt (sym, (export, SOME stmt)) = SOME (sym, (export, stmt))
    1.93            | select_stmt _ = NONE;
    1.94          fun modify_stmts' syms =
    1.95            let
    1.96 -            val stmts = map ((fn Stmt stmt => stmt) o snd o Code_Symbol.Graph.get_node nodes) syms;
    1.97 +            val (exports, stmts) = map_split (the_stmt o snd o Code_Symbol.Graph.get_node nodes) syms;
    1.98              val stmts' = modify_stmts (syms ~~ stmts);
    1.99              val stmts'' = stmts' @ replicate (length syms - length stmts') NONE;
   1.100 -          in map_filter select_stmt (syms ~~ stmts'') end;
   1.101 +          in map_filter select_stmt (syms ~~ (exports ~~ stmts'')) end;
   1.102          val stmtss' = (maps modify_stmts' o map_filter select_syms o Code_Symbol.Graph.strong_conn) nodes;
   1.103          val nodes'' = Code_Symbol.Graph.map (fn sym => apsnd (fn Module content => Module (make_declarations nsps' content)
   1.104              | _ => case AList.lookup (op =) stmtss' sym of SOME stmt => Stmt stmt | _ => Dummy)) nodes';