--- a/src/HOL/Library/Code_Natural.thy Thu Aug 26 13:44:50 2010 +0200
+++ b/src/HOL/Library/Code_Natural.thy Thu Aug 26 13:56:35 2010 +0200
@@ -9,9 +9,7 @@
section {* Alternative representation of @{typ code_numeral} for @{text Haskell} and @{text Scala} *}
code_include Haskell "Natural"
-{*import Data.Array.ST;
-
-newtype Natural = Natural Integer deriving (Eq, Show, Read);
+{*newtype Natural = Natural Integer deriving (Eq, Show, Read);
instance Num Natural where {
fromInteger k = Natural (if k >= 0 then k else 0);
--- a/src/Tools/Code/code_haskell.ML Thu Aug 26 13:44:50 2010 +0200
+++ b/src/Tools/Code/code_haskell.ML Thu Aug 26 13:56:35 2010 +0200
@@ -261,9 +261,8 @@
end;
in print_stmt end;
-fun haskell_program_of_program labelled_name module_name module_prefix reserved raw_module_alias program =
+fun haskell_program_of_program labelled_name module_prefix reserved module_alias program =
let
- val module_alias = if is_some module_name then K module_name else raw_module_alias;
val reserved = Name.make_context reserved;
val mk_name_module = mk_name_module reserved module_prefix module_alias program;
fun add_stmt (name, (stmt, deps)) =
@@ -314,15 +313,14 @@
handle Option => error ("Unknown statement name: " ^ labelled_name name);
in (deresolver, hs_program) end;
-fun serialize_haskell module_prefix raw_module_name string_classes labelled_name
- raw_reserved includes raw_module_alias
- syntax_class syntax_tyco syntax_const (code_of_pretty, code_writeln) program stmt_names destination =
+fun serialize_haskell module_prefix module_name string_classes labelled_name
+ raw_reserved includes module_alias
+ syntax_class syntax_tyco syntax_const (code_of_pretty, code_writeln) program
+ (stmt_names, presentation_stmt_names) destination =
let
- val presentation_stmt_names = Code_Target.stmt_names_of_destination destination;
- val module_name = if null presentation_stmt_names then raw_module_name else SOME "Code";
val reserved = fold (insert (op =) o fst) includes raw_reserved;
val (deresolver, hs_program) = haskell_program_of_program labelled_name
- module_name module_prefix reserved raw_module_alias program;
+ module_prefix reserved module_alias program;
val contr_classparam_typs = Code_Thingol.contr_classparam_typs program;
fun deriving_show tyco =
let
--- a/src/Tools/Code/code_ml.ML Thu Aug 26 13:44:50 2010 +0200
+++ b/src/Tools/Code/code_ml.ML Thu Aug 26 13:56:35 2010 +0200
@@ -489,7 +489,7 @@
|> intro_vars ((fold o Code_Thingol.fold_varnames)
(insert (op =)) ts []);
in concat [
- (Pretty.block o Pretty.commas)
+ (Pretty.block o commas)
(map (print_term is_pseudo_fun some_thm vars NOBR) ts),
str "->",
print_term is_pseudo_fun some_thm vars NOBR t
@@ -535,7 +535,7 @@
:: Pretty.brk 1
:: str "match"
:: Pretty.brk 1
- :: (Pretty.block o Pretty.commas) dummy_parms
+ :: (Pretty.block o commas) dummy_parms
:: Pretty.brk 1
:: str "with"
:: Pretty.brk 1
@@ -722,9 +722,8 @@
in
-fun ml_node_of_program labelled_name module_name reserved raw_module_alias program =
+fun ml_node_of_program labelled_name module_name reserved module_alias program =
let
- val module_alias = if is_some module_name then K module_name else raw_module_alias;
val reserved = Name.make_context reserved;
val empty_module = ((reserved, reserved), Graph.empty);
fun map_node [] f = f
@@ -813,7 +812,7 @@
) stmts
#>> (split_list #> apsnd (map_filter I
#> (fn [] => error ("Datatype block without data statement: "
- ^ (commas o map (labelled_name o fst)) stmts)
+ ^ (Library.commas o map (labelled_name o fst)) stmts)
| stmts => ML_Datas stmts)));
fun add_class stmts =
fold_map
@@ -828,7 +827,7 @@
) stmts
#>> (split_list #> apsnd (map_filter I
#> (fn [] => error ("Class block without class statement: "
- ^ (commas o map (labelled_name o fst)) stmts)
+ ^ (Library.commas o map (labelled_name o fst)) stmts)
| [stmt] => ML_Class stmt)));
fun add_stmts ([stmt as (name, Code_Thingol.Fun _)]) =
add_fun stmt
@@ -849,7 +848,7 @@
| add_stmts ((stmts as (_, Code_Thingol.Classinst _)::_)) =
add_funs stmts
| add_stmts stmts = error ("Illegal mutual dependencies: " ^
- (commas o map (labelled_name o fst)) stmts);
+ (Library.commas o map (labelled_name o fst)) stmts);
fun add_stmts' stmts nsp_nodes =
let
val names as (name :: names') = map fst stmts;
@@ -858,9 +857,9 @@
val module_name = (the_single o distinct (op =) o map mk_name_module) module_names
handle Empty =>
error ("Different namespace prefixes for mutual dependencies:\n"
- ^ commas (map labelled_name names)
+ ^ Library.commas (map labelled_name names)
^ "\n"
- ^ commas module_names);
+ ^ Library.commas module_names);
val module_name_path = Long_Name.explode module_name;
fun add_dep name name' =
let
@@ -907,15 +906,14 @@
error ("Unknown statement name: " ^ labelled_name name);
in (deresolver, nodes) end;
-fun serialize_ml target print_module print_stmt raw_module_name with_signatures labelled_name
- reserved includes raw_module_alias _ syntax_tyco syntax_const (code_of_pretty, code_writeln) program stmt_names destination =
+fun serialize_ml target print_module print_stmt module_name with_signatures labelled_name
+ reserved includes module_alias _ syntax_tyco syntax_const (code_of_pretty, code_writeln) program
+ (stmt_names, presentation_stmt_names) =
let
val is_cons = Code_Thingol.is_cons program;
- val presentation_stmt_names = Code_Target.stmt_names_of_destination destination;
val is_presentation = not (null presentation_stmt_names);
- val module_name = if is_presentation then SOME "Code" else raw_module_name;
val (deresolver, nodes) = ml_node_of_program labelled_name module_name
- reserved raw_module_alias program;
+ reserved module_alias program;
val reserved = make_vars reserved;
fun print_node prefix (Dummy _) =
NONE
@@ -939,7 +937,7 @@
in
Code_Target.mk_serialization target
(fn NONE => code_writeln | SOME file => File.write file o code_of_pretty)
- (rpair stmt_names' o code_of_pretty) p destination
+ (rpair stmt_names' o code_of_pretty) p
end;
end; (*local*)
--- a/src/Tools/Code/code_printer.ML Thu Aug 26 13:44:50 2010 +0200
+++ b/src/Tools/Code/code_printer.ML Thu Aug 26 13:56:35 2010 +0200
@@ -19,6 +19,7 @@
val concat: Pretty.T list -> Pretty.T
val brackets: Pretty.T list -> Pretty.T
val enclose: string -> string -> Pretty.T list -> Pretty.T
+ val commas: Pretty.T list -> Pretty.T list
val enum: string -> string -> string -> Pretty.T list -> Pretty.T
val enum_default: string -> string -> string -> string -> Pretty.T list -> Pretty.T
val semicolon: Pretty.T list -> Pretty.T
@@ -112,6 +113,7 @@
fun xs @| y = xs @ [y];
val str = Print_Mode.setmp [] Pretty.str;
val concat = Pretty.block o Pretty.breaks;
+val commas = Print_Mode.setmp [] Pretty.commas;
fun enclose l r = Print_Mode.setmp [] (Pretty.enclose l r);
val brackets = enclose "(" ")" o Pretty.breaks;
fun enum sep l r = Print_Mode.setmp [] (Pretty.enum sep l r);
--- a/src/Tools/Code/code_scala.ML Thu Aug 26 13:44:50 2010 +0200
+++ b/src/Tools/Code/code_scala.ML Thu Aug 26 13:56:35 2010 +0200
@@ -25,7 +25,7 @@
(** Scala serializer **)
fun print_scala_stmt labelled_name syntax_tyco syntax_const reserved
- args_num is_singleton_constr deresolve =
+ args_num is_singleton_constr (deresolve, deresolve_full) =
let
val deresolve_base = Long_Name.base_name o deresolve;
fun lookup_tyvar tyvars = lookup_var tyvars o first_upper;
@@ -195,7 +195,7 @@
(map print_clause eqs)
end;
val print_method = str o Library.enclose "`" "`" o space_implode "+"
- o fst o split_last o Long_Name.explode;
+ o Long_Name.explode o deresolve_full;
fun print_stmt (name, Code_Thingol.Fun (_, (((vs, ty), raw_eqs), _))) =
print_def name (vs, ty) (filter (snd o snd) raw_eqs)
| print_stmt (name, Code_Thingol.Datatype (_, (vs, cos))) =
@@ -293,11 +293,10 @@
in
-fun scala_program_of_program labelled_name module_name reserved raw_module_alias program =
+fun scala_program_of_program labelled_name reserved module_alias program =
let
(* building module name hierarchy *)
- val module_alias = if is_some module_name then K module_name else raw_module_alias;
fun alias_fragments name = case module_alias name
of SOME name' => Long_Name.explode name'
| NONE => map (fn name => fst (yield_singleton Name.variants name reserved))
@@ -403,20 +402,15 @@
in (deresolve, sca_program) end;
-fun serialize_scala raw_module_name labelled_name
- raw_reserved includes raw_module_alias
+fun serialize_scala labelled_name raw_reserved includes module_alias
_ syntax_tyco syntax_const (code_of_pretty, code_writeln)
- program stmt_names destination =
+ program (stmt_names, presentation_stmt_names) destination =
let
- (* generic nonsense *)
- val presentation_stmt_names = Code_Target.stmt_names_of_destination destination;
- val module_name = if null presentation_stmt_names then raw_module_name else SOME "Code";
-
(* preprocess program *)
val reserved = fold (insert (op =) o fst) includes raw_reserved;
val (deresolve, sca_program) = scala_program_of_program labelled_name
- module_name (Name.make_context reserved) raw_module_alias program;
+ (Name.make_context reserved) module_alias program;
(* print statements *)
fun lookup_constr tyco constr = case Graph.get_node program tyco
@@ -436,12 +430,13 @@
of Code_Thingol.Datatypecons (_, tyco) => null (lookup_constr tyco c)
| _ => false;
val print_stmt = print_scala_stmt labelled_name syntax_tyco syntax_const
- (make_vars reserved) args_num is_singleton_constr deresolve;
+ (make_vars reserved) args_num is_singleton_constr
+ (deresolve, Long_Name.implode o fst o split_last o Long_Name.explode (*FIXME full*));
(* print nodes *)
fun print_implicits [] = NONE
| print_implicits implicits = (SOME o Pretty.block)
- (str "import /*implicits*/" :: Pretty.brk 1 :: Pretty.commas (map (str o deresolve) implicits));
+ (str "import /*implicits*/" :: Pretty.brk 1 :: commas (map (str o deresolve) implicits));
fun print_module base implicits p = Pretty.chunks2
([str ("object " ^ base ^ " {")] @ the_list (print_implicits implicits)
@ [p, str ("} /* object " ^ base ^ " */")]);
@@ -498,9 +493,9 @@
(** Isar setup **)
-fun isar_serializer module_name =
+fun isar_serializer _ =
Code_Target.parse_args (Scan.succeed ())
- #> (fn () => serialize_scala module_name);
+ #> (fn () => serialize_scala);
val setup =
Code_Target.add_target
--- a/src/Tools/Code/code_target.ML Thu Aug 26 13:44:50 2010 +0200
+++ b/src/Tools/Code/code_target.ML Thu Aug 26 13:56:35 2010 +0200
@@ -111,7 +111,7 @@
-> (string -> Code_Printer.activated_const_syntax option)
-> ((Pretty.T -> string) * (Pretty.T -> unit))
-> Code_Thingol.program
- -> string list (*selected statements*)
+ -> (string list * string list) (*selected statements*)
-> serialization;
datatype description = Fundamental of { serializer: serializer, literals: Code_Printer.literals,
@@ -254,7 +254,7 @@
|>> map_filter I;
fun invoke_serializer thy abortable serializer literals reserved abs_includes
- module_alias class instance tyco const module width args naming program2 names1 =
+ module_alias class instance tyco const module_name width args naming program2 (names1, presentation_names) =
let
val (names_class, class') =
activate_syntax (Code_Thingol.lookup_class naming) class;
@@ -275,14 +275,14 @@
val _ = if null empty_funs then () else error ("No code equations for "
^ commas (map (Sign.extern_const thy) empty_funs));
in
- serializer module args (Code_Thingol.labelled_name thy program2) reserved includes
- (Symtab.lookup module_alias) (Symtab.lookup class')
- (Symtab.lookup tyco') (Symtab.lookup const')
+ serializer module_name args (Code_Thingol.labelled_name thy program2) reserved includes
+ (if is_some module_name then K module_name else Symtab.lookup module_alias)
+ (Symtab.lookup class') (Symtab.lookup tyco') (Symtab.lookup const')
(Code_Printer.string_of_pretty width, Code_Printer.writeln_pretty width)
- program4 names1
+ program4 (names1, presentation_names)
end;
-fun mount_serializer thy alt_serializer target some_width module args naming program names =
+fun mount_serializer thy alt_serializer target some_width raw_module_name args naming program names destination =
let
val ((targets, abortable), default_width) = Targets.get thy;
fun collapse_hierarchy target =
@@ -299,6 +299,9 @@
val (modify, data) = collapse_hierarchy target;
val serializer = the_default (case the_description data
of Fundamental seri => #serializer seri) alt_serializer;
+ val presentation_names = stmt_names_of_destination destination;
+ val module_name = if null presentation_names
+ then raw_module_name else SOME "Code";
val reserved = the_reserved data;
fun select_include names_all (name, (content, cs)) =
if null cs then SOME (name, content)
@@ -308,13 +311,14 @@
then SOME (name, content) else NONE;
fun includes names_all = map_filter (select_include names_all)
((Symtab.dest o the_includes) data);
- val module_alias = the_module_alias data;
+ val module_alias = the_module_alias data
val { class, instance, tyco, const } = the_name_syntax data;
val literals = the_literals thy target;
val width = the_default default_width some_width;
in
invoke_serializer thy abortable serializer literals reserved
- includes module_alias class instance tyco const module width args naming (modify program) names
+ includes module_alias class instance tyco const module_name width args
+ naming (modify program) (names, presentation_names) destination
end;
in