removed serializer interface redundancies
authorhaftmann
Tue Aug 31 13:55:54 2010 +0200 (2010-08-31)
changeset 38924fcd1d0457e27
parent 38923 79d7f2b4cf71
child 38925 ced825abdc1d
removed serializer interface redundancies
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	Tue Aug 31 13:29:38 2010 +0200
     1.2 +++ b/src/Tools/Code/code_haskell.ML	Tue Aug 31 13:55:54 2010 +0200
     1.3 @@ -313,8 +313,8 @@
     1.4        handle Option => error ("Unknown statement name: " ^ labelled_name name);
     1.5    in (deresolver, hs_program) end;
     1.6  
     1.7 -fun serialize_haskell module_prefix module_name string_classes labelled_name
     1.8 -    raw_reserved includes module_alias
     1.9 +fun serialize_haskell module_prefix string_classes labelled_name
    1.10 +    raw_reserved includes single_module module_alias
    1.11      class_syntax tyco_syntax const_syntax program
    1.12      (stmt_names, presentation_stmt_names) =
    1.13    let
    1.14 @@ -350,7 +350,7 @@
    1.15      fun serialize_module1 (module_name', (deps, (stmts, _))) =
    1.16        let
    1.17          val stmt_names = map fst stmts;
    1.18 -        val qualified = is_none module_name;
    1.19 +        val qualified = not single_module;
    1.20          val imports = subtract (op =) stmt_names deps
    1.21            |> distinct (op =)
    1.22            |> map_filter (try deresolver)
    1.23 @@ -465,11 +465,11 @@
    1.24  
    1.25  (** Isar setup **)
    1.26  
    1.27 -fun isar_serializer module_name =
    1.28 +val isar_serializer =
    1.29    Code_Target.parse_args (Scan.option (Args.$$$ "root" -- Args.colon |-- Args.name)
    1.30      -- Scan.optional (Args.$$$ "string_classes" >> K true) false
    1.31      >> (fn (module_prefix, string_classes) =>
    1.32 -      serialize_haskell module_prefix module_name string_classes));
    1.33 +      serialize_haskell module_prefix string_classes));
    1.34  
    1.35  val _ =
    1.36    Outer_Syntax.command "code_monad" "define code syntax for monads" Keyword.thy_decl (
     2.1 --- a/src/Tools/Code/code_ml.ML	Tue Aug 31 13:29:38 2010 +0200
     2.2 +++ b/src/Tools/Code/code_ml.ML	Tue Aug 31 13:55:54 2010 +0200
     2.3 @@ -718,7 +718,7 @@
     2.4  
     2.5  in
     2.6  
     2.7 -fun ml_node_of_program labelled_name module_name reserved module_alias program =
     2.8 +fun ml_node_of_program labelled_name reserved module_alias program =
     2.9    let
    2.10      val reserved = Name.make_context reserved;
    2.11      val empty_module = ((reserved, reserved), Graph.empty);
    2.12 @@ -902,13 +902,13 @@
    2.13          error ("Unknown statement name: " ^ labelled_name name);
    2.14    in (deresolver, nodes) end;
    2.15  
    2.16 -fun serialize_ml target print_module print_stmt module_name with_signatures labelled_name
    2.17 -  reserved includes module_alias _ tyco_syntax const_syntax program
    2.18 +fun serialize_ml target print_module print_stmt with_signatures labelled_name
    2.19 +  reserved includes single_module module_alias _ tyco_syntax const_syntax program
    2.20    (stmt_names, presentation_stmt_names) =
    2.21    let
    2.22      val is_cons = Code_Thingol.is_cons program;
    2.23      val is_presentation = not (null presentation_stmt_names);
    2.24 -    val (deresolver, nodes) = ml_node_of_program labelled_name module_name
    2.25 +    val (deresolver, nodes) = ml_node_of_program labelled_name
    2.26        reserved module_alias program;
    2.27      val reserved = make_vars reserved;
    2.28      fun print_node prefix (Dummy _) =
    2.29 @@ -927,8 +927,8 @@
    2.30          o rev o flat o Graph.strong_conn) nodes
    2.31        |> split_list
    2.32        |> (fn (decls, body) => (flat decls, body))
    2.33 -    val stmt_names' = (map o try)
    2.34 -      (deresolver (if is_some module_name then the_list module_name else [])) stmt_names;
    2.35 +    val stmt_names' = map (try (deresolver [])) stmt_names
    2.36 +      |> single_module ? (map o Option.map) Long_Name.base_name;
    2.37      val p = Pretty.chunks2 (map snd includes @ snd (print_nodes [] nodes));
    2.38      fun write width NONE = writeln_pretty width
    2.39        | write width (SOME p) = File.write p o string_of_pretty width;
    2.40 @@ -941,15 +941,15 @@
    2.41  
    2.42  (** Isar setup **)
    2.43  
    2.44 -fun isar_serializer_sml module_name =
    2.45 +val isar_serializer_sml =
    2.46    Code_Target.parse_args (Scan.optional (Args.$$$ "no_signatures" >> K false) true
    2.47    >> (fn with_signatures => serialize_ml target_SML
    2.48 -      print_sml_module print_sml_stmt module_name with_signatures));
    2.49 +      print_sml_module print_sml_stmt with_signatures));
    2.50  
    2.51 -fun isar_serializer_ocaml module_name =
    2.52 +val isar_serializer_ocaml =
    2.53    Code_Target.parse_args (Scan.optional (Args.$$$ "no_signatures" >> K false) true
    2.54    >> (fn with_signatures => serialize_ml target_OCaml
    2.55 -      print_ocaml_module print_ocaml_stmt module_name with_signatures));
    2.56 +      print_ocaml_module print_ocaml_stmt with_signatures));
    2.57  
    2.58  val setup =
    2.59    Code_Target.add_target
     3.1 --- a/src/Tools/Code/code_scala.ML	Tue Aug 31 13:29:38 2010 +0200
     3.2 +++ b/src/Tools/Code/code_scala.ML	Tue Aug 31 13:55:54 2010 +0200
     3.3 @@ -413,7 +413,7 @@
     3.4  
     3.5    in (deresolver, sca_program) end;
     3.6  
     3.7 -fun serialize_scala labelled_name raw_reserved includes module_alias
     3.8 +fun serialize_scala labelled_name raw_reserved includes _ module_alias
     3.9      _ tyco_syntax const_syntax
    3.10      program (stmt_names, presentation_stmt_names) =
    3.11    let
    3.12 @@ -513,9 +513,8 @@
    3.13  
    3.14  (** Isar setup **)
    3.15  
    3.16 -fun isar_serializer _ =
    3.17 -  Code_Target.parse_args (Scan.succeed ())
    3.18 -  #> (fn () => serialize_scala);
    3.19 +val isar_serializer =
    3.20 +  Code_Target.parse_args (Scan.succeed ()) #> K serialize_scala;
    3.21  
    3.22  val setup =
    3.23    Code_Target.add_target
     4.1 --- a/src/Tools/Code/code_target.ML	Tue Aug 31 13:29:38 2010 +0200
     4.2 +++ b/src/Tools/Code/code_target.ML	Tue Aug 31 13:55:54 2010 +0200
     4.3 @@ -101,12 +101,11 @@
     4.4         Symtab.join (K snd) (const1, const2))
     4.5    );
     4.6  
     4.7 -type serializer =
     4.8 -  string option                         (*module name*)
     4.9 -  -> Token.T list                       (*arguments*)
    4.10 +type serializer = Token.T list          (*arguments*)
    4.11    -> (string -> string)                 (*labelled_name*)
    4.12    -> string list                        (*reserved symbols*)
    4.13    -> (string * Pretty.T) list           (*includes*)
    4.14 +  -> bool                               (*singleton module*)
    4.15    -> (string -> string option)          (*module aliasses*)
    4.16    -> (string -> string option)          (*class syntax*)
    4.17    -> (string -> Code_Printer.tyco_syntax option)
    4.18 @@ -279,8 +278,8 @@
    4.19      val _ = if null empty_funs then () else error ("No code equations for "
    4.20        ^ commas (map (Sign.extern_const thy) empty_funs));
    4.21    in
    4.22 -    serializer module_name args (Code_Thingol.labelled_name thy program2) reserved includes
    4.23 -      (if is_some module_name then K module_name else Symtab.lookup module_alias)
    4.24 +    serializer args (Code_Thingol.labelled_name thy program2) reserved includes
    4.25 +      (is_some module_name) (if is_some module_name then K module_name else Symtab.lookup module_alias)
    4.26        (Symtab.lookup class') (Symtab.lookup tyco') (Symtab.lookup const')
    4.27        program4 (names1, presentation_names) width
    4.28    end;