printing combinator for hierarchical programs
authorhaftmann
Sat Sep 04 21:13:13 2010 +0200 (2010-09-04)
changeset 391473c284a152bd6
parent 39145 154fd9c06c63
child 39148 b6530978c14d
printing combinator for hierarchical programs
src/Tools/Code/code_ml.ML
src/Tools/Code/code_namespace.ML
src/Tools/Code/code_scala.ML
     1.1 --- a/src/Tools/Code/code_ml.ML	Sat Sep 04 08:32:19 2010 -0700
     1.2 +++ b/src/Tools/Code/code_ml.ML	Sat Sep 04 21:13:13 2010 +0200
     1.3 @@ -785,31 +785,33 @@
     1.4        cyclic_modules = false, empty_data = (), memorize_data = K I, modify_stmts = modify_stmts } program
     1.5    end;
     1.6  
     1.7 -fun serialize_ml target print_module print_stmt with_signatures { labelled_name,
     1.8 +fun serialize_ml target print_ml_module print_ml_stmt with_signatures { labelled_name,
     1.9    reserved_syms, includes, module_alias, class_syntax, tyco_syntax,
    1.10    const_syntax, program, names } =
    1.11    let
    1.12 -    val is_cons = Code_Thingol.is_cons program;
    1.13 +
    1.14 +    (* build program *)
    1.15      val { deresolver, hierarchical_program = ml_program } =
    1.16        ml_program_of_program labelled_name (Name.make_context reserved_syms) module_alias program;
    1.17 -    val print_stmt = print_stmt labelled_name tyco_syntax const_syntax
    1.18 -      (make_vars reserved_syms) is_cons;
    1.19 -    fun print_node _ (_, Code_Namespace.Dummy) =
    1.20 -          NONE
    1.21 -      | print_node prefix_fragments (name, Code_Namespace.Stmt stmt) =
    1.22 -          SOME (apsnd (markup_stmt name) (print_stmt (deresolver prefix_fragments) stmt))
    1.23 -      | print_node prefix_fragments (name_fragment, Code_Namespace.Module (_, nodes)) =
    1.24 -          let
    1.25 -            val (decls, body) = print_nodes (prefix_fragments @ [name_fragment]) nodes;
    1.26 -            val p = print_module name_fragment
    1.27 -                (if with_signatures then SOME decls else NONE) body;
    1.28 -          in SOME ([], p) end
    1.29 -    and print_nodes prefix_fragments nodes = (map_filter
    1.30 -        (fn name => print_node prefix_fragments (name, snd (Graph.get_node nodes name)))
    1.31 -        o rev o flat o Graph.strong_conn) nodes
    1.32 -      |> split_list
    1.33 -      |> (fn (decls, body) => (flat decls, body))
    1.34 -    val p = Pretty.chunks2 (map snd includes @ snd (print_nodes [] ml_program));
    1.35 +
    1.36 +    (* print statements *)
    1.37 +    fun print_stmt prefix_fragments (_, stmt) = print_ml_stmt
    1.38 +      labelled_name tyco_syntax const_syntax (make_vars reserved_syms)
    1.39 +      (Code_Thingol.is_cons program) (deresolver prefix_fragments) stmt
    1.40 +      |> apfst SOME;
    1.41 +
    1.42 +    (* print modules *)
    1.43 +    fun print_module prefix_fragments base _ xs =
    1.44 +      let
    1.45 +        val (raw_decls, body) = split_list xs;
    1.46 +        val decls = if with_signatures then SOME (maps these raw_decls) else NONE 
    1.47 +      in (NONE, print_ml_module base decls body) end;
    1.48 +
    1.49 +    (* serialization *)
    1.50 +    val p = Pretty.chunks2 (map snd includes
    1.51 +      @ map snd (Code_Namespace.print_hierarchical {
    1.52 +        print_module = print_module, print_stmt = print_stmt,
    1.53 +        lift_markup = apsnd } ml_program));
    1.54      fun write width NONE = writeln o format [] width
    1.55        | write width (SOME p) = File.write p o format [] width;
    1.56    in
     2.1 --- a/src/Tools/Code/code_namespace.ML	Sat Sep 04 08:32:19 2010 -0700
     2.2 +++ b/src/Tools/Code/code_namespace.ML	Sat Sep 04 21:13:13 2010 +0200
     2.3 @@ -10,7 +10,8 @@
     2.4    datatype ('a, 'b) node =
     2.5        Dummy
     2.6      | Stmt of 'a
     2.7 -    | Module of ('b * (string * ('a, 'b) node) Graph.T);
     2.8 +    | Module of ('b * (string * ('a, 'b) node) Graph.T)
     2.9 +  type ('a, 'b) hierarchical_program = (string * ('a, 'b) node) Graph.T
    2.10    val hierarchical_program: (string -> string) -> { module_alias: string -> string option,
    2.11      reserved: Name.context, empty_nsp: 'c, namify_module: string -> 'c -> string * 'c,
    2.12      namify_stmt: Code_Thingol.stmt -> string -> 'c -> string * 'c,
    2.13 @@ -18,7 +19,11 @@
    2.14      modify_stmts: (string * Code_Thingol.stmt) list -> 'a option list }
    2.15        -> Code_Thingol.program
    2.16        -> { deresolver: string list -> string -> string,
    2.17 -           hierarchical_program: (string * ('a, 'b) node) Graph.T }
    2.18 +           hierarchical_program: ('a, 'b) hierarchical_program }
    2.19 +  val print_hierarchical: { print_module: string list -> string -> 'b -> 'c list -> 'c,
    2.20 +    print_stmt: string list -> string * 'a -> 'c,
    2.21 +    lift_markup: (Pretty.T -> Pretty.T) -> 'c -> 'c }
    2.22 +      -> ('a, 'b) hierarchical_program -> 'c list
    2.23  end;
    2.24  
    2.25  structure Code_Namespace : CODE_NAMESPACE =
    2.26 @@ -37,6 +42,8 @@
    2.27    | Stmt of 'a
    2.28    | Module of ('b * (string * ('a, 'b) node) Graph.T);
    2.29  
    2.30 +type ('a, 'b) hierarchical_program = (string * ('a, 'b) node) Graph.T;
    2.31 +
    2.32  fun map_module_content f (Module content) = Module (f content);
    2.33  
    2.34  fun map_module [] = I
    2.35 @@ -140,4 +147,25 @@
    2.36  
    2.37    in { deresolver = deresolver, hierarchical_program = hierarchical_program } end;
    2.38  
    2.39 +fun print_hierarchical { print_module, print_stmt, lift_markup } =
    2.40 +  let
    2.41 +    fun print_node _ (_, Dummy) =
    2.42 +          NONE
    2.43 +      | print_node prefix_fragments (name, Stmt stmt) =
    2.44 +          SOME (lift_markup (Code_Printer.markup_stmt name)
    2.45 +            (print_stmt prefix_fragments (name, stmt)))
    2.46 +      | print_node prefix_fragments (name_fragment, Module (data, nodes)) =
    2.47 +          let
    2.48 +            val prefix_fragments' = prefix_fragments @ [name_fragment]
    2.49 +          in
    2.50 +            Option.map (print_module prefix_fragments'
    2.51 +              name_fragment data) (print_nodes prefix_fragments' nodes)
    2.52 +          end
    2.53 +    and print_nodes prefix_fragments nodes =
    2.54 +      let
    2.55 +        val xs = (map_filter (fn name => print_node prefix_fragments
    2.56 +          (name, snd (Graph.get_node nodes name))) o rev o flat o Graph.strong_conn) nodes
    2.57 +      in if null xs then NONE else SOME xs end;
    2.58 +  in these o print_nodes [] end;
    2.59 +
    2.60  end;
    2.61 \ No newline at end of file
     3.1 --- a/src/Tools/Code/code_scala.ML	Sat Sep 04 08:32:19 2010 -0700
     3.2 +++ b/src/Tools/Code/code_scala.ML	Sat Sep 04 21:13:13 2010 +0200
     3.3 @@ -334,7 +334,7 @@
     3.4    let
     3.5  
     3.6      (* build program *)
     3.7 -    val { deresolver, hierarchical_program = sca_program } =
     3.8 +    val { deresolver, hierarchical_program = scala_program } =
     3.9        scala_program_of_program labelled_name (Name.make_context reserved_syms) module_alias program;
    3.10  
    3.11      (* print statements *)
    3.12 @@ -354,38 +354,27 @@
    3.13      fun is_singleton_constr c = case Graph.get_node program c
    3.14       of Code_Thingol.Datatypecons (_, tyco) => null (lookup_constr tyco c)
    3.15        | _ => false;
    3.16 -    val print_stmt = print_scala_stmt labelled_name tyco_syntax const_syntax
    3.17 -      (make_vars reserved_syms) args_num is_singleton_constr;
    3.18 +    fun print_stmt prefix_fragments = print_scala_stmt labelled_name
    3.19 +      tyco_syntax const_syntax (make_vars reserved_syms) args_num
    3.20 +      is_singleton_constr (deresolver prefix_fragments, deresolver []);
    3.21  
    3.22 -    (* print nodes *)
    3.23 -    fun print_module base implicit_ps p = Pretty.chunks2
    3.24 -      ([str ("object " ^ base ^ " {")]
    3.25 -        @ (if null implicit_ps then [] else (single o Pretty.block)
    3.26 -            (str "import /*implicits*/" :: Pretty.brk 1 :: commas implicit_ps))
    3.27 -        @ [p, str ("} /* object " ^ base ^ " */")]);
    3.28 +    (* print modules *)
    3.29      fun print_implicit prefix_fragments implicit =
    3.30        let
    3.31          val s = deresolver prefix_fragments implicit;
    3.32        in if length (Long_Name.explode s) = 1 then NONE else SOME (str s) end;
    3.33 -    fun print_node _ (_, Code_Namespace.Dummy) = NONE
    3.34 -      | print_node prefix_fragments (name, Code_Namespace.Stmt stmt) =
    3.35 -          SOME (markup_stmt name (print_stmt (deresolver prefix_fragments, deresolver []) (name, stmt)))
    3.36 -      | print_node prefix_fragments (name_fragment, Code_Namespace.Module (implicits, nodes)) =
    3.37 -          let
    3.38 -            val prefix_fragments' = prefix_fragments @ [name_fragment];
    3.39 -          in
    3.40 -            Option.map (print_module name_fragment
    3.41 -              (map_filter (print_implicit prefix_fragments') implicits))
    3.42 -                (print_nodes prefix_fragments' nodes)
    3.43 -          end
    3.44 -    and print_nodes prefix_fragments nodes = let
    3.45 -        val ps = map_filter (fn name => print_node prefix_fragments (name,
    3.46 -          snd (Graph.get_node nodes name)))
    3.47 -            ((rev o flat o Graph.strong_conn) nodes);
    3.48 -      in if null ps then NONE else SOME (Pretty.chunks2 ps) end;
    3.49 +    fun print_module prefix_fragments base implicits ps = Pretty.chunks2
    3.50 +      ([str ("object " ^ base ^ " {")]
    3.51 +        @ (case map_filter (print_implicit prefix_fragments) implicits
    3.52 +            of [] => [] | implicit_ps => (single o Pretty.block)
    3.53 +            (str "import /*implicits*/" :: Pretty.brk 1 :: commas implicit_ps))
    3.54 +        @ ps @ [str ("} /* object " ^ base ^ " */")]);
    3.55  
    3.56      (* serialization *)
    3.57 -    val p = Pretty.chunks2 (map snd includes @ the_list (print_nodes [] sca_program));
    3.58 +    val p = Pretty.chunks2 (map snd includes
    3.59 +      @ Code_Namespace.print_hierarchical {
    3.60 +        print_module = print_module, print_stmt = print_stmt,
    3.61 +        lift_markup = I } scala_program);
    3.62      fun write width NONE = writeln o format [] width
    3.63        | write width (SOME p) = File.write p o format [] width;
    3.64    in