# HG changeset patch # User haftmann # Date 1282823795 -7200 # Node ID 6b356e3687d25e1a8252120107df4556f95fd508 # Parent 95df565aceb724605150e1a8b672cbed2e74469a# Parent 910cedb62327b17d3eb2edad325841e1dad59f4f merged diff -r 95df565aceb7 -r 6b356e3687d2 src/HOL/Library/Code_Natural.thy --- 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); diff -r 95df565aceb7 -r 6b356e3687d2 src/Tools/Code/code_haskell.ML --- 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 diff -r 95df565aceb7 -r 6b356e3687d2 src/Tools/Code/code_ml.ML --- 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*) diff -r 95df565aceb7 -r 6b356e3687d2 src/Tools/Code/code_printer.ML --- 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); diff -r 95df565aceb7 -r 6b356e3687d2 src/Tools/Code/code_scala.ML --- 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 diff -r 95df565aceb7 -r 6b356e3687d2 src/Tools/Code/code_target.ML --- 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