tuned serializer interface
authorhaftmann
Thu Aug 26 13:50:58 2010 +0200 (2010-08-26)
changeset 3877989f654951200
parent 38778 49b885736e8f
child 38780 910cedb62327
tuned serializer interface
src/Tools/Code/code_haskell.ML
src/Tools/Code/code_ml.ML
src/Tools/Code/code_scala.ML
src/Tools/Code/code_target.ML
     1.1 --- a/src/Tools/Code/code_haskell.ML	Thu Aug 26 12:30:43 2010 +0200
     1.2 +++ b/src/Tools/Code/code_haskell.ML	Thu Aug 26 13:50:58 2010 +0200
     1.3 @@ -261,9 +261,8 @@
     1.4            end;
     1.5    in print_stmt end;
     1.6  
     1.7 -fun haskell_program_of_program labelled_name module_name module_prefix reserved raw_module_alias program =
     1.8 +fun haskell_program_of_program labelled_name module_prefix reserved module_alias program =
     1.9    let
    1.10 -    val module_alias = if is_some module_name then K module_name else raw_module_alias;
    1.11      val reserved = Name.make_context reserved;
    1.12      val mk_name_module = mk_name_module reserved module_prefix module_alias program;
    1.13      fun add_stmt (name, (stmt, deps)) =
    1.14 @@ -314,15 +313,14 @@
    1.15        handle Option => error ("Unknown statement name: " ^ labelled_name name);
    1.16    in (deresolver, hs_program) end;
    1.17  
    1.18 -fun serialize_haskell module_prefix raw_module_name string_classes labelled_name
    1.19 -    raw_reserved includes raw_module_alias
    1.20 -    syntax_class syntax_tyco syntax_const (code_of_pretty, code_writeln) program stmt_names destination =
    1.21 +fun serialize_haskell module_prefix module_name string_classes labelled_name
    1.22 +    raw_reserved includes module_alias
    1.23 +    syntax_class syntax_tyco syntax_const (code_of_pretty, code_writeln) program
    1.24 +    (stmt_names, presentation_stmt_names) destination =
    1.25    let
    1.26 -    val presentation_stmt_names = Code_Target.stmt_names_of_destination destination;
    1.27 -    val module_name = if null presentation_stmt_names then raw_module_name else SOME "Code";
    1.28      val reserved = fold (insert (op =) o fst) includes raw_reserved;
    1.29      val (deresolver, hs_program) = haskell_program_of_program labelled_name
    1.30 -      module_name module_prefix reserved raw_module_alias program;
    1.31 +      module_prefix reserved module_alias program;
    1.32      val contr_classparam_typs = Code_Thingol.contr_classparam_typs program;
    1.33      fun deriving_show tyco =
    1.34        let
     2.1 --- a/src/Tools/Code/code_ml.ML	Thu Aug 26 12:30:43 2010 +0200
     2.2 +++ b/src/Tools/Code/code_ml.ML	Thu Aug 26 13:50:58 2010 +0200
     2.3 @@ -722,9 +722,8 @@
     2.4  
     2.5  in
     2.6  
     2.7 -fun ml_node_of_program labelled_name module_name reserved raw_module_alias program =
     2.8 +fun ml_node_of_program labelled_name module_name reserved module_alias program =
     2.9    let
    2.10 -    val module_alias = if is_some module_name then K module_name else raw_module_alias;
    2.11      val reserved = Name.make_context reserved;
    2.12      val empty_module = ((reserved, reserved), Graph.empty);
    2.13      fun map_node [] f = f
    2.14 @@ -907,15 +906,14 @@
    2.15          error ("Unknown statement name: " ^ labelled_name name);
    2.16    in (deresolver, nodes) end;
    2.17  
    2.18 -fun serialize_ml target print_module print_stmt raw_module_name with_signatures labelled_name
    2.19 -  reserved includes raw_module_alias _ syntax_tyco syntax_const (code_of_pretty, code_writeln) program stmt_names destination =
    2.20 +fun serialize_ml target print_module print_stmt module_name with_signatures labelled_name
    2.21 +  reserved includes module_alias _ syntax_tyco syntax_const (code_of_pretty, code_writeln) program
    2.22 +  (stmt_names, presentation_stmt_names) =
    2.23    let
    2.24      val is_cons = Code_Thingol.is_cons program;
    2.25 -    val presentation_stmt_names = Code_Target.stmt_names_of_destination destination;
    2.26      val is_presentation = not (null presentation_stmt_names);
    2.27 -    val module_name = if is_presentation then SOME "Code" else raw_module_name;
    2.28      val (deresolver, nodes) = ml_node_of_program labelled_name module_name
    2.29 -      reserved raw_module_alias program;
    2.30 +      reserved module_alias program;
    2.31      val reserved = make_vars reserved;
    2.32      fun print_node prefix (Dummy _) =
    2.33            NONE
    2.34 @@ -939,7 +937,7 @@
    2.35    in
    2.36      Code_Target.mk_serialization target
    2.37        (fn NONE => code_writeln | SOME file => File.write file o code_of_pretty)
    2.38 -      (rpair stmt_names' o code_of_pretty) p destination
    2.39 +      (rpair stmt_names' o code_of_pretty) p
    2.40    end;
    2.41  
    2.42  end; (*local*)
     3.1 --- a/src/Tools/Code/code_scala.ML	Thu Aug 26 12:30:43 2010 +0200
     3.2 +++ b/src/Tools/Code/code_scala.ML	Thu Aug 26 13:50:58 2010 +0200
     3.3 @@ -293,11 +293,10 @@
     3.4  
     3.5  in
     3.6  
     3.7 -fun scala_program_of_program labelled_name module_name reserved raw_module_alias program =
     3.8 +fun scala_program_of_program labelled_name reserved module_alias program =
     3.9    let
    3.10  
    3.11      (* building module name hierarchy *)
    3.12 -    val module_alias = if is_some module_name then K module_name else raw_module_alias;
    3.13      fun alias_fragments name = case module_alias name
    3.14       of SOME name' => Long_Name.explode name'
    3.15        | NONE => map (fn name => fst (yield_singleton Name.variants name reserved))
    3.16 @@ -403,20 +402,15 @@
    3.17  
    3.18    in (deresolve, sca_program) end;
    3.19  
    3.20 -fun serialize_scala raw_module_name labelled_name
    3.21 -    raw_reserved includes raw_module_alias
    3.22 +fun serialize_scala labelled_name raw_reserved includes module_alias
    3.23      _ syntax_tyco syntax_const (code_of_pretty, code_writeln)
    3.24 -    program stmt_names destination =
    3.25 +    program (stmt_names, presentation_stmt_names) destination =
    3.26    let
    3.27  
    3.28 -    (* generic nonsense *)
    3.29 -    val presentation_stmt_names = Code_Target.stmt_names_of_destination destination;
    3.30 -    val module_name = if null presentation_stmt_names then raw_module_name else SOME "Code";
    3.31 -
    3.32      (* preprocess program *)
    3.33      val reserved = fold (insert (op =) o fst) includes raw_reserved;
    3.34      val (deresolve, sca_program) = scala_program_of_program labelled_name
    3.35 -      module_name (Name.make_context reserved) raw_module_alias program;
    3.36 +      (Name.make_context reserved) module_alias program;
    3.37  
    3.38      (* print statements *)
    3.39      fun lookup_constr tyco constr = case Graph.get_node program tyco
    3.40 @@ -498,9 +492,9 @@
    3.41  
    3.42  (** Isar setup **)
    3.43  
    3.44 -fun isar_serializer module_name =
    3.45 +fun isar_serializer _ =
    3.46    Code_Target.parse_args (Scan.succeed ())
    3.47 -  #> (fn () => serialize_scala module_name);
    3.48 +  #> (fn () => serialize_scala);
    3.49  
    3.50  val setup =
    3.51    Code_Target.add_target
     4.1 --- a/src/Tools/Code/code_target.ML	Thu Aug 26 12:30:43 2010 +0200
     4.2 +++ b/src/Tools/Code/code_target.ML	Thu Aug 26 13:50:58 2010 +0200
     4.3 @@ -111,7 +111,7 @@
     4.4    -> (string -> Code_Printer.activated_const_syntax option)
     4.5    -> ((Pretty.T -> string) * (Pretty.T -> unit))
     4.6    -> Code_Thingol.program
     4.7 -  -> string list                        (*selected statements*)
     4.8 +  -> (string list * string list)        (*selected statements*)
     4.9    -> serialization;
    4.10  
    4.11  datatype description = Fundamental of { serializer: serializer, literals: Code_Printer.literals,
    4.12 @@ -254,7 +254,7 @@
    4.13    |>> map_filter I;
    4.14  
    4.15  fun invoke_serializer thy abortable serializer literals reserved abs_includes 
    4.16 -    module_alias class instance tyco const module width args naming program2 names1 =
    4.17 +    module_alias class instance tyco const module_name width args naming program2 (names1, presentation_names) =
    4.18    let
    4.19      val (names_class, class') =
    4.20        activate_syntax (Code_Thingol.lookup_class naming) class;
    4.21 @@ -275,14 +275,14 @@
    4.22      val _ = if null empty_funs then () else error ("No code equations for "
    4.23        ^ commas (map (Sign.extern_const thy) empty_funs));
    4.24    in
    4.25 -    serializer module args (Code_Thingol.labelled_name thy program2) reserved includes
    4.26 -      (Symtab.lookup module_alias) (Symtab.lookup class')
    4.27 -      (Symtab.lookup tyco') (Symtab.lookup const')
    4.28 +    serializer module_name args (Code_Thingol.labelled_name thy program2) reserved includes
    4.29 +      (if is_some module_name then K module_name else Symtab.lookup module_alias)
    4.30 +      (Symtab.lookup class') (Symtab.lookup tyco') (Symtab.lookup const')
    4.31        (Code_Printer.string_of_pretty width, Code_Printer.writeln_pretty width)
    4.32 -      program4 names1
    4.33 +      program4 (names1, presentation_names)
    4.34    end;
    4.35  
    4.36 -fun mount_serializer thy alt_serializer target some_width module args naming program names =
    4.37 +fun mount_serializer thy alt_serializer target some_width raw_module_name args naming program names destination =
    4.38    let
    4.39      val ((targets, abortable), default_width) = Targets.get thy;
    4.40      fun collapse_hierarchy target =
    4.41 @@ -299,6 +299,9 @@
    4.42      val (modify, data) = collapse_hierarchy target;
    4.43      val serializer = the_default (case the_description data
    4.44       of Fundamental seri => #serializer seri) alt_serializer;
    4.45 +    val presentation_names = stmt_names_of_destination destination;
    4.46 +    val module_name = if null presentation_names
    4.47 +      then raw_module_name else SOME "Code";
    4.48      val reserved = the_reserved data;
    4.49      fun select_include names_all (name, (content, cs)) =
    4.50        if null cs then SOME (name, content)
    4.51 @@ -308,13 +311,14 @@
    4.52        then SOME (name, content) else NONE;
    4.53      fun includes names_all = map_filter (select_include names_all)
    4.54        ((Symtab.dest o the_includes) data);
    4.55 -    val module_alias = the_module_alias data;
    4.56 +    val module_alias = the_module_alias data 
    4.57      val { class, instance, tyco, const } = the_name_syntax data;
    4.58      val literals = the_literals thy target;
    4.59      val width = the_default default_width some_width;
    4.60    in
    4.61      invoke_serializer thy abortable serializer literals reserved
    4.62 -      includes module_alias class instance tyco const module width args naming (modify program) names
    4.63 +      includes module_alias class instance tyco const module_name width args
    4.64 +        naming (modify program) (names, presentation_names) destination
    4.65    end;
    4.66  
    4.67  in