1.1 --- a/src/HOL/Library/Code_Natural.thy Thu Aug 26 13:44:50 2010 +0200
1.2 +++ b/src/HOL/Library/Code_Natural.thy Thu Aug 26 13:56:35 2010 +0200
1.3 @@ -9,9 +9,7 @@
1.4 section {* Alternative representation of @{typ code_numeral} for @{text Haskell} and @{text Scala} *}
1.5
1.6 code_include Haskell "Natural"
1.7 -{*import Data.Array.ST;
1.8 -
1.9 -newtype Natural = Natural Integer deriving (Eq, Show, Read);
1.10 +{*newtype Natural = Natural Integer deriving (Eq, Show, Read);
1.11
1.12 instance Num Natural where {
1.13 fromInteger k = Natural (if k >= 0 then k else 0);
2.1 --- a/src/Tools/Code/code_haskell.ML Thu Aug 26 13:44:50 2010 +0200
2.2 +++ b/src/Tools/Code/code_haskell.ML Thu Aug 26 13:56:35 2010 +0200
2.3 @@ -261,9 +261,8 @@
2.4 end;
2.5 in print_stmt end;
2.6
2.7 -fun haskell_program_of_program labelled_name module_name module_prefix reserved raw_module_alias program =
2.8 +fun haskell_program_of_program labelled_name module_prefix 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 mk_name_module = mk_name_module reserved module_prefix module_alias program;
2.13 fun add_stmt (name, (stmt, deps)) =
2.14 @@ -314,15 +313,14 @@
2.15 handle Option => error ("Unknown statement name: " ^ labelled_name name);
2.16 in (deresolver, hs_program) end;
2.17
2.18 -fun serialize_haskell module_prefix raw_module_name string_classes labelled_name
2.19 - raw_reserved includes raw_module_alias
2.20 - syntax_class syntax_tyco syntax_const (code_of_pretty, code_writeln) program stmt_names destination =
2.21 +fun serialize_haskell module_prefix module_name string_classes labelled_name
2.22 + raw_reserved includes module_alias
2.23 + syntax_class syntax_tyco syntax_const (code_of_pretty, code_writeln) program
2.24 + (stmt_names, presentation_stmt_names) destination =
2.25 let
2.26 - val presentation_stmt_names = Code_Target.stmt_names_of_destination destination;
2.27 - val module_name = if null presentation_stmt_names then raw_module_name else SOME "Code";
2.28 val reserved = fold (insert (op =) o fst) includes raw_reserved;
2.29 val (deresolver, hs_program) = haskell_program_of_program labelled_name
2.30 - module_name module_prefix reserved raw_module_alias program;
2.31 + module_prefix reserved module_alias program;
2.32 val contr_classparam_typs = Code_Thingol.contr_classparam_typs program;
2.33 fun deriving_show tyco =
2.34 let
3.1 --- a/src/Tools/Code/code_ml.ML Thu Aug 26 13:44:50 2010 +0200
3.2 +++ b/src/Tools/Code/code_ml.ML Thu Aug 26 13:56:35 2010 +0200
3.3 @@ -489,7 +489,7 @@
3.4 |> intro_vars ((fold o Code_Thingol.fold_varnames)
3.5 (insert (op =)) ts []);
3.6 in concat [
3.7 - (Pretty.block o Pretty.commas)
3.8 + (Pretty.block o commas)
3.9 (map (print_term is_pseudo_fun some_thm vars NOBR) ts),
3.10 str "->",
3.11 print_term is_pseudo_fun some_thm vars NOBR t
3.12 @@ -535,7 +535,7 @@
3.13 :: Pretty.brk 1
3.14 :: str "match"
3.15 :: Pretty.brk 1
3.16 - :: (Pretty.block o Pretty.commas) dummy_parms
3.17 + :: (Pretty.block o commas) dummy_parms
3.18 :: Pretty.brk 1
3.19 :: str "with"
3.20 :: Pretty.brk 1
3.21 @@ -722,9 +722,8 @@
3.22
3.23 in
3.24
3.25 -fun ml_node_of_program labelled_name module_name reserved raw_module_alias program =
3.26 +fun ml_node_of_program labelled_name module_name reserved module_alias program =
3.27 let
3.28 - val module_alias = if is_some module_name then K module_name else raw_module_alias;
3.29 val reserved = Name.make_context reserved;
3.30 val empty_module = ((reserved, reserved), Graph.empty);
3.31 fun map_node [] f = f
3.32 @@ -813,7 +812,7 @@
3.33 ) stmts
3.34 #>> (split_list #> apsnd (map_filter I
3.35 #> (fn [] => error ("Datatype block without data statement: "
3.36 - ^ (commas o map (labelled_name o fst)) stmts)
3.37 + ^ (Library.commas o map (labelled_name o fst)) stmts)
3.38 | stmts => ML_Datas stmts)));
3.39 fun add_class stmts =
3.40 fold_map
3.41 @@ -828,7 +827,7 @@
3.42 ) stmts
3.43 #>> (split_list #> apsnd (map_filter I
3.44 #> (fn [] => error ("Class block without class statement: "
3.45 - ^ (commas o map (labelled_name o fst)) stmts)
3.46 + ^ (Library.commas o map (labelled_name o fst)) stmts)
3.47 | [stmt] => ML_Class stmt)));
3.48 fun add_stmts ([stmt as (name, Code_Thingol.Fun _)]) =
3.49 add_fun stmt
3.50 @@ -849,7 +848,7 @@
3.51 | add_stmts ((stmts as (_, Code_Thingol.Classinst _)::_)) =
3.52 add_funs stmts
3.53 | add_stmts stmts = error ("Illegal mutual dependencies: " ^
3.54 - (commas o map (labelled_name o fst)) stmts);
3.55 + (Library.commas o map (labelled_name o fst)) stmts);
3.56 fun add_stmts' stmts nsp_nodes =
3.57 let
3.58 val names as (name :: names') = map fst stmts;
3.59 @@ -858,9 +857,9 @@
3.60 val module_name = (the_single o distinct (op =) o map mk_name_module) module_names
3.61 handle Empty =>
3.62 error ("Different namespace prefixes for mutual dependencies:\n"
3.63 - ^ commas (map labelled_name names)
3.64 + ^ Library.commas (map labelled_name names)
3.65 ^ "\n"
3.66 - ^ commas module_names);
3.67 + ^ Library.commas module_names);
3.68 val module_name_path = Long_Name.explode module_name;
3.69 fun add_dep name name' =
3.70 let
3.71 @@ -907,15 +906,14 @@
3.72 error ("Unknown statement name: " ^ labelled_name name);
3.73 in (deresolver, nodes) end;
3.74
3.75 -fun serialize_ml target print_module print_stmt raw_module_name with_signatures labelled_name
3.76 - reserved includes raw_module_alias _ syntax_tyco syntax_const (code_of_pretty, code_writeln) program stmt_names destination =
3.77 +fun serialize_ml target print_module print_stmt module_name with_signatures labelled_name
3.78 + reserved includes module_alias _ syntax_tyco syntax_const (code_of_pretty, code_writeln) program
3.79 + (stmt_names, presentation_stmt_names) =
3.80 let
3.81 val is_cons = Code_Thingol.is_cons program;
3.82 - val presentation_stmt_names = Code_Target.stmt_names_of_destination destination;
3.83 val is_presentation = not (null presentation_stmt_names);
3.84 - val module_name = if is_presentation then SOME "Code" else raw_module_name;
3.85 val (deresolver, nodes) = ml_node_of_program labelled_name module_name
3.86 - reserved raw_module_alias program;
3.87 + reserved module_alias program;
3.88 val reserved = make_vars reserved;
3.89 fun print_node prefix (Dummy _) =
3.90 NONE
3.91 @@ -939,7 +937,7 @@
3.92 in
3.93 Code_Target.mk_serialization target
3.94 (fn NONE => code_writeln | SOME file => File.write file o code_of_pretty)
3.95 - (rpair stmt_names' o code_of_pretty) p destination
3.96 + (rpair stmt_names' o code_of_pretty) p
3.97 end;
3.98
3.99 end; (*local*)
4.1 --- a/src/Tools/Code/code_printer.ML Thu Aug 26 13:44:50 2010 +0200
4.2 +++ b/src/Tools/Code/code_printer.ML Thu Aug 26 13:56:35 2010 +0200
4.3 @@ -19,6 +19,7 @@
4.4 val concat: Pretty.T list -> Pretty.T
4.5 val brackets: Pretty.T list -> Pretty.T
4.6 val enclose: string -> string -> Pretty.T list -> Pretty.T
4.7 + val commas: Pretty.T list -> Pretty.T list
4.8 val enum: string -> string -> string -> Pretty.T list -> Pretty.T
4.9 val enum_default: string -> string -> string -> string -> Pretty.T list -> Pretty.T
4.10 val semicolon: Pretty.T list -> Pretty.T
4.11 @@ -112,6 +113,7 @@
4.12 fun xs @| y = xs @ [y];
4.13 val str = Print_Mode.setmp [] Pretty.str;
4.14 val concat = Pretty.block o Pretty.breaks;
4.15 +val commas = Print_Mode.setmp [] Pretty.commas;
4.16 fun enclose l r = Print_Mode.setmp [] (Pretty.enclose l r);
4.17 val brackets = enclose "(" ")" o Pretty.breaks;
4.18 fun enum sep l r = Print_Mode.setmp [] (Pretty.enum sep l r);
5.1 --- a/src/Tools/Code/code_scala.ML Thu Aug 26 13:44:50 2010 +0200
5.2 +++ b/src/Tools/Code/code_scala.ML Thu Aug 26 13:56:35 2010 +0200
5.3 @@ -25,7 +25,7 @@
5.4 (** Scala serializer **)
5.5
5.6 fun print_scala_stmt labelled_name syntax_tyco syntax_const reserved
5.7 - args_num is_singleton_constr deresolve =
5.8 + args_num is_singleton_constr (deresolve, deresolve_full) =
5.9 let
5.10 val deresolve_base = Long_Name.base_name o deresolve;
5.11 fun lookup_tyvar tyvars = lookup_var tyvars o first_upper;
5.12 @@ -195,7 +195,7 @@
5.13 (map print_clause eqs)
5.14 end;
5.15 val print_method = str o Library.enclose "`" "`" o space_implode "+"
5.16 - o fst o split_last o Long_Name.explode;
5.17 + o Long_Name.explode o deresolve_full;
5.18 fun print_stmt (name, Code_Thingol.Fun (_, (((vs, ty), raw_eqs), _))) =
5.19 print_def name (vs, ty) (filter (snd o snd) raw_eqs)
5.20 | print_stmt (name, Code_Thingol.Datatype (_, (vs, cos))) =
5.21 @@ -293,11 +293,10 @@
5.22
5.23 in
5.24
5.25 -fun scala_program_of_program labelled_name module_name reserved raw_module_alias program =
5.26 +fun scala_program_of_program labelled_name reserved module_alias program =
5.27 let
5.28
5.29 (* building module name hierarchy *)
5.30 - val module_alias = if is_some module_name then K module_name else raw_module_alias;
5.31 fun alias_fragments name = case module_alias name
5.32 of SOME name' => Long_Name.explode name'
5.33 | NONE => map (fn name => fst (yield_singleton Name.variants name reserved))
5.34 @@ -403,20 +402,15 @@
5.35
5.36 in (deresolve, sca_program) end;
5.37
5.38 -fun serialize_scala raw_module_name labelled_name
5.39 - raw_reserved includes raw_module_alias
5.40 +fun serialize_scala labelled_name raw_reserved includes module_alias
5.41 _ syntax_tyco syntax_const (code_of_pretty, code_writeln)
5.42 - program stmt_names destination =
5.43 + program (stmt_names, presentation_stmt_names) destination =
5.44 let
5.45
5.46 - (* generic nonsense *)
5.47 - val presentation_stmt_names = Code_Target.stmt_names_of_destination destination;
5.48 - val module_name = if null presentation_stmt_names then raw_module_name else SOME "Code";
5.49 -
5.50 (* preprocess program *)
5.51 val reserved = fold (insert (op =) o fst) includes raw_reserved;
5.52 val (deresolve, sca_program) = scala_program_of_program labelled_name
5.53 - module_name (Name.make_context reserved) raw_module_alias program;
5.54 + (Name.make_context reserved) module_alias program;
5.55
5.56 (* print statements *)
5.57 fun lookup_constr tyco constr = case Graph.get_node program tyco
5.58 @@ -436,12 +430,13 @@
5.59 of Code_Thingol.Datatypecons (_, tyco) => null (lookup_constr tyco c)
5.60 | _ => false;
5.61 val print_stmt = print_scala_stmt labelled_name syntax_tyco syntax_const
5.62 - (make_vars reserved) args_num is_singleton_constr deresolve;
5.63 + (make_vars reserved) args_num is_singleton_constr
5.64 + (deresolve, Long_Name.implode o fst o split_last o Long_Name.explode (*FIXME full*));
5.65
5.66 (* print nodes *)
5.67 fun print_implicits [] = NONE
5.68 | print_implicits implicits = (SOME o Pretty.block)
5.69 - (str "import /*implicits*/" :: Pretty.brk 1 :: Pretty.commas (map (str o deresolve) implicits));
5.70 + (str "import /*implicits*/" :: Pretty.brk 1 :: commas (map (str o deresolve) implicits));
5.71 fun print_module base implicits p = Pretty.chunks2
5.72 ([str ("object " ^ base ^ " {")] @ the_list (print_implicits implicits)
5.73 @ [p, str ("} /* object " ^ base ^ " */")]);
5.74 @@ -498,9 +493,9 @@
5.75
5.76 (** Isar setup **)
5.77
5.78 -fun isar_serializer module_name =
5.79 +fun isar_serializer _ =
5.80 Code_Target.parse_args (Scan.succeed ())
5.81 - #> (fn () => serialize_scala module_name);
5.82 + #> (fn () => serialize_scala);
5.83
5.84 val setup =
5.85 Code_Target.add_target
6.1 --- a/src/Tools/Code/code_target.ML Thu Aug 26 13:44:50 2010 +0200
6.2 +++ b/src/Tools/Code/code_target.ML Thu Aug 26 13:56:35 2010 +0200
6.3 @@ -111,7 +111,7 @@
6.4 -> (string -> Code_Printer.activated_const_syntax option)
6.5 -> ((Pretty.T -> string) * (Pretty.T -> unit))
6.6 -> Code_Thingol.program
6.7 - -> string list (*selected statements*)
6.8 + -> (string list * string list) (*selected statements*)
6.9 -> serialization;
6.10
6.11 datatype description = Fundamental of { serializer: serializer, literals: Code_Printer.literals,
6.12 @@ -254,7 +254,7 @@
6.13 |>> map_filter I;
6.14
6.15 fun invoke_serializer thy abortable serializer literals reserved abs_includes
6.16 - module_alias class instance tyco const module width args naming program2 names1 =
6.17 + module_alias class instance tyco const module_name width args naming program2 (names1, presentation_names) =
6.18 let
6.19 val (names_class, class') =
6.20 activate_syntax (Code_Thingol.lookup_class naming) class;
6.21 @@ -275,14 +275,14 @@
6.22 val _ = if null empty_funs then () else error ("No code equations for "
6.23 ^ commas (map (Sign.extern_const thy) empty_funs));
6.24 in
6.25 - serializer module args (Code_Thingol.labelled_name thy program2) reserved includes
6.26 - (Symtab.lookup module_alias) (Symtab.lookup class')
6.27 - (Symtab.lookup tyco') (Symtab.lookup const')
6.28 + serializer module_name args (Code_Thingol.labelled_name thy program2) reserved includes
6.29 + (if is_some module_name then K module_name else Symtab.lookup module_alias)
6.30 + (Symtab.lookup class') (Symtab.lookup tyco') (Symtab.lookup const')
6.31 (Code_Printer.string_of_pretty width, Code_Printer.writeln_pretty width)
6.32 - program4 names1
6.33 + program4 (names1, presentation_names)
6.34 end;
6.35
6.36 -fun mount_serializer thy alt_serializer target some_width module args naming program names =
6.37 +fun mount_serializer thy alt_serializer target some_width raw_module_name args naming program names destination =
6.38 let
6.39 val ((targets, abortable), default_width) = Targets.get thy;
6.40 fun collapse_hierarchy target =
6.41 @@ -299,6 +299,9 @@
6.42 val (modify, data) = collapse_hierarchy target;
6.43 val serializer = the_default (case the_description data
6.44 of Fundamental seri => #serializer seri) alt_serializer;
6.45 + val presentation_names = stmt_names_of_destination destination;
6.46 + val module_name = if null presentation_names
6.47 + then raw_module_name else SOME "Code";
6.48 val reserved = the_reserved data;
6.49 fun select_include names_all (name, (content, cs)) =
6.50 if null cs then SOME (name, content)
6.51 @@ -308,13 +311,14 @@
6.52 then SOME (name, content) else NONE;
6.53 fun includes names_all = map_filter (select_include names_all)
6.54 ((Symtab.dest o the_includes) data);
6.55 - val module_alias = the_module_alias data;
6.56 + val module_alias = the_module_alias data
6.57 val { class, instance, tyco, const } = the_name_syntax data;
6.58 val literals = the_literals thy target;
6.59 val width = the_default default_width some_width;
6.60 in
6.61 invoke_serializer thy abortable serializer literals reserved
6.62 - includes module_alias class instance tyco const module width args naming (modify program) names
6.63 + includes module_alias class instance tyco const module_name width args
6.64 + naming (modify program) (names, presentation_names) destination
6.65 end;
6.66
6.67 in