# HG changeset patch # User haftmann # Date 1283185960 -7200 # Node ID fd6b9bdb428e81834ba067dcb1a0949f30ddab3d # Parent 245fca4ce86fdea276195d9a645a1eb1fa63a872# Parent 48d62f237944070c39eab8b3ba4fdff96bc60fac merged diff -r 245fca4ce86f -r fd6b9bdb428e doc-src/more_antiquote.ML --- a/doc-src/more_antiquote.ML Mon Aug 30 18:07:58 2010 +0200 +++ b/doc-src/more_antiquote.ML Mon Aug 30 18:32:40 2010 +0200 @@ -130,6 +130,7 @@ Code_Target.code_of thy target NONE "Example" (mk_cs thy) (fn naming => maps (fn f => f thy naming) mk_stmtss) + |> fst |> typewriter end); diff -r 245fca4ce86f -r fd6b9bdb428e src/Tools/Code/code_haskell.ML --- a/src/Tools/Code/code_haskell.ML Mon Aug 30 18:07:58 2010 +0200 +++ b/src/Tools/Code/code_haskell.ML Mon Aug 30 18:32:40 2010 +0200 @@ -315,8 +315,8 @@ 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 = + syntax_class syntax_tyco syntax_const program + (stmt_names, presentation_stmt_names) = let val reserved = fold (insert (op =) o fst) includes raw_reserved; val (deresolver, hs_program) = haskell_program_of_program labelled_name @@ -375,28 +375,26 @@ | (_, (_, NONE)) => NONE) stmts); val serialize_module = if null presentation_stmt_names then serialize_module1 else pair "" o serialize_module2; - fun check_destination destination = - (File.check destination; destination); - fun write_module destination (modlname, content) = - let - val filename = case modlname - of "" => Path.explode "Main.hs" - | _ => (Path.ext "hs" o Path.explode o implode o separate "/" - o Long_Name.explode) modlname; - val pathname = Path.append destination filename; - val _ = File.mkdir_leaf (Path.dir pathname); - in File.write pathname - ("{-# OPTIONS_GHC -fglasgow-exts #-}\n\n" - ^ code_of_pretty content) - end + fun write_module width (SOME destination) (modlname, content) = + let + val _ = File.check destination; + val filename = case modlname + of "" => Path.explode "Main.hs" + | _ => (Path.ext "hs" o Path.explode o implode o separate "/" + o Long_Name.explode) modlname; + val pathname = Path.append destination filename; + val _ = File.mkdir_leaf (Path.dir pathname); + in File.write pathname + ("{-# OPTIONS_GHC -fglasgow-exts #-}\n\n" + ^ string_of_pretty width content) + end + | write_module width NONE (_, content) = writeln_pretty width content; in - Code_Target.mk_serialization target - (fn NONE => K () o map (code_writeln o (fn p => Pretty.block [p, Pretty.fbrk]) o snd) - | SOME file => K () o map (write_module (check_destination file))) - (rpair [] o cat_lines o map (code_of_pretty o snd)) + Code_Target.serialization + (fn width => fn destination => K () o map (write_module width destination)) + (fn width => rpair [] o cat_lines o map (string_of_pretty width o snd)) (map (uncurry print_module) includes @ map serialize_module (Symtab.dest hs_program)) - destination end; val literals = let diff -r 245fca4ce86f -r fd6b9bdb428e src/Tools/Code/code_ml.ML --- a/src/Tools/Code/code_ml.ML Mon Aug 30 18:07:58 2010 +0200 +++ b/src/Tools/Code/code_ml.ML Mon Aug 30 18:32:40 2010 +0200 @@ -907,7 +907,7 @@ in (deresolver, nodes) end; 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 + reserved includes module_alias _ syntax_tyco syntax_const program (stmt_names, presentation_stmt_names) = let val is_cons = Code_Thingol.is_cons program; @@ -934,10 +934,10 @@ val stmt_names' = (map o try) (deresolver (if is_some module_name then the_list module_name else [])) stmt_names; val p = Pretty.chunks2 (map snd includes @ snd (print_nodes [] nodes)); + fun write width NONE = writeln_pretty width + | write width (SOME p) = File.write p o string_of_pretty width; 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 + Code_Target.serialization write (fn width => (rpair stmt_names' o string_of_pretty width)) p end; end; (*local*) diff -r 245fca4ce86f -r fd6b9bdb428e src/Tools/Code/code_printer.ML --- a/src/Tools/Code/code_printer.ML Mon Aug 30 18:07:58 2010 +0200 +++ b/src/Tools/Code/code_printer.ML Mon Aug 30 18:32:40 2010 +0200 @@ -124,7 +124,7 @@ fun indent i = Print_Mode.setmp [] (Pretty.indent i); fun string_of_pretty width p = Print_Mode.setmp [] (Pretty.string_of_margin width) p ^ "\n"; -fun writeln_pretty width p = writeln (Print_Mode.setmp [] (Pretty.string_of_margin width) p); +fun writeln_pretty width p = writeln (string_of_pretty width p); (** names and variable name contexts **) diff -r 245fca4ce86f -r fd6b9bdb428e src/Tools/Code/code_scala.ML --- a/src/Tools/Code/code_scala.ML Mon Aug 30 18:07:58 2010 +0200 +++ b/src/Tools/Code/code_scala.ML Mon Aug 30 18:32:40 2010 +0200 @@ -414,8 +414,8 @@ in (deresolver, sca_program) end; fun serialize_scala labelled_name raw_reserved includes module_alias - _ syntax_tyco syntax_const (code_of_pretty, code_writeln) - program (stmt_names, presentation_stmt_names) destination = + _ syntax_tyco syntax_const + program (stmt_names, presentation_stmt_names) = let (* build program *) @@ -480,10 +480,10 @@ val p_includes = if null presentation_stmt_names then map (fn (base, p) => print_module base [] p) includes else []; val p = Pretty.chunks2 (p_includes @ the_list (print_nodes [] sca_program)); + fun write width NONE = writeln_pretty width + | write width (SOME p) = File.write p o string_of_pretty width; in - Code_Target.mk_serialization target - (fn NONE => code_writeln | SOME file => File.write file o code_of_pretty) - (rpair [] o code_of_pretty) p destination + Code_Target.serialization write (rpair [] oo string_of_pretty) p end; end; (*local*) diff -r 245fca4ce86f -r fd6b9bdb428e src/Tools/Code/code_target.ML --- a/src/Tools/Code/code_target.ML Mon Aug 30 18:07:58 2010 +0200 +++ b/src/Tools/Code/code_target.ML Mon Aug 30 18:32:40 2010 +0200 @@ -1,7 +1,7 @@ (* Title: Tools/Code/code_target.ML Author: Florian Haftmann, TU Muenchen -Serializer from intermediate language ("Thin-gol") to target languages. +Generic infrastructure for target language data. *) signature CODE_TARGET = @@ -9,6 +9,22 @@ val cert_tyco: theory -> string -> string val read_tyco: theory -> string -> string + val export_code_for: theory -> Path.T option -> string -> int option -> string option -> Token.T list + -> Code_Thingol.naming -> Code_Thingol.program -> string list -> unit + val produce_code_for: theory -> string -> int option -> string option -> Token.T list + -> Code_Thingol.naming -> Code_Thingol.program -> string list * string list -> string * string option list + val check_code_for: theory -> string -> bool -> Token.T list + -> Code_Thingol.naming -> Code_Thingol.program -> string list -> unit + + val export_code: theory -> string list + -> (((string * string option) * Path.T option) * Token.T list) list -> unit + val produce_code: theory -> string list -> (Code_Thingol.naming -> string list) + -> string -> int option -> string option -> Token.T list -> string * string option list + val check_code: theory -> string list + -> ((string * bool) * Token.T list) list -> unit + + val shell_command: string (*theory name*) -> string (*export_code expr*) -> unit + type serializer type literals = Code_Printer.literals val add_target: string * { serializer: serializer, literals: literals, @@ -18,26 +34,19 @@ (string * (Code_Thingol.naming -> Code_Thingol.program -> Code_Thingol.program)) -> theory -> theory val assert_target: theory -> string -> string - - type destination + val the_literals: theory -> string -> literals type serialization val parse_args: 'a parser -> Token.T list -> 'a - val stmt_names_of_destination: destination -> string list - val mk_serialization: string -> (Path.T option -> 'a -> unit) - -> ('a -> string * string option list) - -> 'a -> serialization - val serialize: theory -> string -> int option -> string option -> Token.T list - -> Code_Thingol.naming -> Code_Thingol.program -> string list -> serialization + val serialization: (int -> Path.T option -> 'a -> unit) + -> (int -> 'a -> string * string option list) + -> 'a -> int -> serialization + val set_default_code_width: int -> theory -> theory + + (*FIXME drop asap*) + val code_of: theory -> string -> int option -> string + -> string list -> (Code_Thingol.naming -> string list) -> string * string option list val serialize_custom: theory -> string * serializer -> string option -> Code_Thingol.naming -> Code_Thingol.program -> string list -> string * string option list - val the_literals: theory -> string -> literals - val export: serialization -> unit - val file: Path.T -> serialization -> unit - val string: string list -> serialization -> string - val code_of: theory -> string -> int option -> string - -> string list -> (Code_Thingol.naming -> string list) -> string - val set_default_code_width: int -> theory -> theory - val shell_command: string (*theory name*) -> string (*export_code expr*) -> unit val allow_abort: string -> theory -> theory type tyco_syntax = Code_Printer.tyco_syntax @@ -62,19 +71,17 @@ (** basics **) -datatype destination = Export | File of Path.T | String of string list; +datatype destination = File of Path.T option | String of string list; type serialization = destination -> (string * string option list) option; -fun export f = (f Export; ()); -fun file p f = (f (File p); ()); -fun string stmts f = fst (the (f (String stmts))); - -fun stmt_names_of_destination (String stmts) = stmts +fun stmt_names_of_destination (String stmt_names) = stmt_names | stmt_names_of_destination _ = []; -fun mk_serialization target output _ code Export = (output NONE code ; NONE) - | mk_serialization target output _ code (File file) = (output (SOME file) code; NONE) - | mk_serialization target _ string code (String _) = SOME (string code); +fun serialization output _ pretty width (File some_path) = (output width some_path pretty; NONE) + | serialization _ string pretty width (String _) = SOME (string width pretty); + +fun file some_path f = (f (File some_path); ()); +fun string stmt_names f = the (f (String stmt_names)); (** theory data **) @@ -90,7 +97,8 @@ NameSyntaxTable { class = class, instance = instance, tyco = tyco, const = const }; fun map_name_syntax_table f (NameSyntaxTable { class, instance, tyco, const }) = mk_name_syntax_table (f ((class, instance), (tyco, const))); -fun merge_name_syntax_table (NameSyntaxTable { class = class1, instance = instance1, tyco = tyco1, const = const1 }, +fun merge_name_syntax_table + (NameSyntaxTable { class = class1, instance = instance1, tyco = tyco1, const = const1 }, NameSyntaxTable { class = class2, instance = instance2, tyco = tyco2, const = const2 }) = mk_name_syntax_table ( (Symtab.join (K snd) (class1, class2), @@ -109,15 +117,17 @@ -> (string -> string option) (*class syntax*) -> (string -> Code_Printer.tyco_syntax option) -> (string -> Code_Printer.activated_const_syntax option) - -> ((Pretty.T -> string) * (Pretty.T -> unit)) -> Code_Thingol.program -> (string list * string list) (*selected statements*) + -> int -> serialization; -datatype description = Fundamental of { serializer: serializer, literals: Code_Printer.literals, +datatype description = Fundamental of { serializer: serializer, + literals: literals, check: { env_var: string, make_destination: Path.T -> Path.T, make_command: string -> string -> string } } - | Extension of string * (Code_Thingol.naming -> Code_Thingol.program -> Code_Thingol.program); + | Extension of string * + (Code_Thingol.naming -> Code_Thingol.program -> Code_Thingol.program); datatype target = Target of { serial: serial, @@ -190,8 +200,8 @@ thy |> (Targets.map o apfst o apfst o Symtab.update) (target, make_target ((serial (), seri), (([], Symtab.empty), - (mk_name_syntax_table ((Symtab.empty, Symreltab.empty), (Symtab.empty, Symtab.empty)), - Symtab.empty)))) + (mk_name_syntax_table ((Symtab.empty, Symreltab.empty), + (Symtab.empty, Symtab.empty)), Symtab.empty)))) end; fun add_target (target, seri) = put_target (target, Fundamental seri); @@ -254,7 +264,7 @@ |>> map_filter I; fun invoke_serializer thy abortable serializer literals reserved abs_includes - module_alias class instance tyco const module_name width args naming program2 (names1, presentation_names) = + module_alias class instance tyco const module_name args naming program2 (names1, presentation_names) width = let val (names_class, class') = activate_syntax (Code_Thingol.lookup_class naming) class; @@ -278,8 +288,7 @@ 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, presentation_names) + program4 (names1, presentation_names) width end; fun mount_serializer thy alt_serializer target some_width raw_module_name args naming program names destination = @@ -317,15 +326,21 @@ val width = the_default default_width some_width; in invoke_serializer thy abortable serializer literals reserved - includes module_alias class instance tyco const module_name width args - naming (modify program) (names, presentation_names) destination + includes module_alias class instance tyco const module_name args + naming (modify program) (names, presentation_names) width destination end; in fun serialize thy = mount_serializer thy NONE; -fun check thy names_cs naming program target strict args = +fun export_code_for thy some_path target some_width some_module_name args naming program names = + file some_path (serialize thy target some_width some_module_name args naming program names); + +fun produce_code_for thy target some_width some_module_name args naming program (names, selects) = + string selects (serialize thy target some_width some_module_name args naming program names); + +fun check_code_for thy target strict args naming program names_cs = let val module_name = "Code_Test"; val { env_var, make_destination, make_command } = @@ -334,7 +349,7 @@ fun ext_check env_param p = let val destination = make_destination p; - val _ = file destination (serialize thy target (SOME 80) + val _ = file (SOME destination) (serialize thy target (SOME 80) (SOME module_name) args naming program names_cs); val cmd = make_command env_param module_name; in if bash ("cd " ^ File.shell_path p ^ " && " ^ cmd ^ " 2>&1") <> 0 @@ -383,22 +398,30 @@ if member (op =) names3 name then SOME c else NONE) (cs2 ~~ names2); in union (op =) cs3 cs1 end; +fun prep_destination "" = NONE + | prep_destination "-" = NONE + | prep_destination s = SOME (Path.explode s); + fun export_code thy cs seris = let val (names_cs, (naming, program)) = Code_Thingol.consts_program thy false cs; - fun mk_seri_dest dest = if dest = "" orelse dest = "-" then export - else file (Path.explode dest); - val _ = map (fn (((target, module), dest), args) => - (mk_seri_dest dest (serialize thy target NONE module args naming program names_cs))) seris; + val _ = map (fn (((target, module_name), some_path), args) => + export_code_for thy some_path target NONE module_name args naming program names_cs) seris; in () end; -fun export_code_cmd raw_cs seris thy = export_code thy (read_const_exprs thy raw_cs) seris; +fun export_code_cmd raw_cs seris thy = export_code thy (read_const_exprs thy raw_cs) + ((map o apfst o apsnd) prep_destination seris); + +fun produce_code thy cs names_stmt target some_width some_module_name args = + let + val (names_cs, (naming, program)) = Code_Thingol.consts_program thy false cs; + in produce_code_for thy target some_width some_module_name args naming program (names_cs, names_stmt naming) end; fun check_code thy cs seris = let val (names_cs, (naming, program)) = Code_Thingol.consts_program thy false cs; - val _ = map (fn ((target, strict), args) => check thy names_cs naming program - target strict args) seris; + val _ = map (fn ((target, strict), args) => + check_code_for thy target strict args naming program names_cs) seris; in () end; fun check_code_cmd raw_cs seris thy = check_code thy (read_const_exprs thy raw_cs) seris;