removed namespace stuff from code_printer
authorhaftmann
Thu Sep 02 13:43:38 2010 +0200 (2010-09-02)
changeset 3905581e0368812ad
parent 39034 ebeb48fd653b
child 39056 fa197571676b
removed namespace stuff from code_printer
src/Tools/Code/code_haskell.ML
src/Tools/Code/code_namespace.ML
src/Tools/Code/code_printer.ML
     1.1 --- a/src/Tools/Code/code_haskell.ML	Thu Sep 02 12:30:22 2010 +0200
     1.2 +++ b/src/Tools/Code/code_haskell.ML	Thu Sep 02 13:43:38 2010 +0200
     1.3 @@ -261,13 +261,31 @@
     1.4            end;
     1.5    in print_stmt end;
     1.6  
     1.7 +fun mk_name_module reserved module_prefix module_alias program =
     1.8 +  let
     1.9 +    fun mk_alias name = case module_alias name
    1.10 +     of SOME name' => name'
    1.11 +      | NONE => name
    1.12 +          |> Long_Name.explode
    1.13 +          |> map (fn name => (the_single o fst) (Name.variants [name] reserved))
    1.14 +          |> Long_Name.implode;
    1.15 +    fun mk_prefix name = case module_prefix
    1.16 +     of SOME module_prefix => Long_Name.append module_prefix name
    1.17 +      | NONE => name;
    1.18 +    val tab =
    1.19 +      Symtab.empty
    1.20 +      |> Graph.fold ((fn name => Symtab.default (name, (mk_alias #> mk_prefix) name))
    1.21 +           o fst o Code_Namespace.dest_name o fst)
    1.22 +             program
    1.23 +  in the o Symtab.lookup tab end;
    1.24 +
    1.25  fun haskell_program_of_program labelled_name module_prefix reserved module_alias program =
    1.26    let
    1.27      val reserved = Name.make_context reserved;
    1.28      val mk_name_module = mk_name_module reserved module_prefix module_alias program;
    1.29      fun add_stmt (name, (stmt, deps)) =
    1.30        let
    1.31 -        val (module_name, base) = dest_name name;
    1.32 +        val (module_name, base) = Code_Namespace.dest_name name;
    1.33          val module_name' = mk_name_module module_name;
    1.34          val mk_name_stmt = yield_singleton Name.variants;
    1.35          fun add_fun upper (nsp_fun, nsp_typ) =
    1.36 @@ -309,7 +327,7 @@
    1.37        (Graph.get_node program name, Graph.imm_succs program name))
    1.38        (Graph.strong_conn program |> flat)) Symtab.empty;
    1.39      fun deresolver name = (fst o the o AList.lookup (op =) ((fst o snd o the
    1.40 -      o Symtab.lookup hs_program) ((mk_name_module o fst o dest_name) name))) name
    1.41 +      o Symtab.lookup hs_program) ((mk_name_module o fst o Code_Namespace.dest_name) name))) name
    1.42        handle Option => error ("Unknown statement name: " ^ labelled_name name);
    1.43    in (deresolver, hs_program) end;
    1.44  
     2.1 --- a/src/Tools/Code/code_namespace.ML	Thu Sep 02 12:30:22 2010 +0200
     2.2 +++ b/src/Tools/Code/code_namespace.ML	Thu Sep 02 13:43:38 2010 +0200
     2.3 @@ -6,6 +6,7 @@
     2.4  
     2.5  signature CODE_NAMESPACE =
     2.6  sig
     2.7 +  val dest_name: string -> string * string
     2.8    datatype ('a, 'b) node =
     2.9        Dummy
    2.10      | Stmt of 'a
    2.11 @@ -23,7 +24,13 @@
    2.12  structure Code_Namespace : CODE_NAMESPACE =
    2.13  struct
    2.14  
    2.15 -(* hierarchical program structure *)
    2.16 +(** splitting names in module and base part **)
    2.17 +
    2.18 +val dest_name =
    2.19 +  apfst Long_Name.implode o split_last o fst o split_last o Long_Name.explode;
    2.20 +
    2.21 +
    2.22 +(** hierarchical program structure **)
    2.23  
    2.24  datatype ('a, 'b) node =
    2.25      Dummy
    2.26 @@ -46,10 +53,10 @@
    2.27       of SOME name' => Long_Name.explode name'
    2.28        | NONE => map (fn name => fst (yield_singleton Name.variants name reserved))
    2.29            (Long_Name.explode name);
    2.30 -    val module_names = Graph.fold (insert (op =) o fst o Code_Printer.dest_name o fst) program [];
    2.31 +    val module_names = Graph.fold (insert (op =) o fst o dest_name o fst) program [];
    2.32      val fragments_tab = fold (fn name => Symtab.update
    2.33        (name, alias_fragments name)) module_names Symtab.empty;
    2.34 -    val dest_name = Code_Printer.dest_name #>> (the o Symtab.lookup fragments_tab);
    2.35 +    val dest_name = dest_name #>> (the o Symtab.lookup fragments_tab);
    2.36  
    2.37      (* building empty module hierarchy *)
    2.38      val empty_module = (empty_data, Graph.empty);
     3.1 --- a/src/Tools/Code/code_printer.ML	Thu Sep 02 12:30:22 2010 +0200
     3.2 +++ b/src/Tools/Code/code_printer.ML	Thu Sep 02 13:43:38 2010 +0200
     3.3 @@ -70,7 +70,6 @@
     3.4    val applify: string -> string -> ('a -> Pretty.T) -> fixity -> Pretty.T -> 'a list -> Pretty.T
     3.5    val tuplify: (fixity -> 'a -> Pretty.T) -> fixity -> 'a list -> Pretty.T option
     3.6  
     3.7 -
     3.8    type tyco_syntax
     3.9    type simple_const_syntax
    3.10    type complex_const_syntax
    3.11 @@ -93,10 +92,6 @@
    3.12    val gen_print_bind: (thm option -> var_ctxt -> fixity -> iterm -> Pretty.T)
    3.13      -> thm option -> fixity
    3.14      -> iterm -> var_ctxt -> Pretty.T * var_ctxt
    3.15 -
    3.16 -  val mk_name_module: Name.context -> string option -> (string -> string option)
    3.17 -    -> 'a Graph.T -> string -> string
    3.18 -  val dest_name: string -> string * string
    3.19  end;
    3.20  
    3.21  structure Code_Printer : CODE_PRINTER =
    3.22 @@ -395,28 +390,4 @@
    3.23  
    3.24  val parse_const_syntax = parse_syntax plain_const_syntax simple_const_syntax fst;
    3.25  
    3.26 -
    3.27 -(** module name spaces **)
    3.28 -
    3.29 -val dest_name =
    3.30 -  apfst Long_Name.implode o split_last o fst o split_last o Long_Name.explode;
    3.31 -
    3.32 -fun mk_name_module reserved module_prefix module_alias program =
    3.33 -  let
    3.34 -    fun mk_alias name = case module_alias name
    3.35 -     of SOME name' => name'
    3.36 -      | NONE => name
    3.37 -          |> Long_Name.explode
    3.38 -          |> map (fn name => (the_single o fst) (Name.variants [name] reserved))
    3.39 -          |> Long_Name.implode;
    3.40 -    fun mk_prefix name = case module_prefix
    3.41 -     of SOME module_prefix => Long_Name.append module_prefix name
    3.42 -      | NONE => name;
    3.43 -    val tab =
    3.44 -      Symtab.empty
    3.45 -      |> Graph.fold ((fn name => Symtab.default (name, (mk_alias #> mk_prefix) name))
    3.46 -           o fst o dest_name o fst)
    3.47 -             program
    3.48 -  in the o Symtab.lookup tab end;
    3.49 -
    3.50  end; (*struct*)