# HG changeset patch # User haftmann # Date 1391978247 -3600 # Node ID 3662c44d018cb3c998eba06d348545ee294052d0 # Parent cb0c6cb10681fe42a81f538567510c316beea264 dropped legacy finally diff -r cb0c6cb10681 -r 3662c44d018c src/Doc/Codegen/Further.thy --- a/src/Doc/Codegen/Further.thy Sun Feb 09 19:10:12 2014 +0000 +++ b/src/Doc/Codegen/Further.thy Sun Feb 09 21:37:27 2014 +0100 @@ -33,7 +33,7 @@ rather than function definitions are always curried. The second aspect affects user-defined adaptations with @{command - code_const}. For regular terms, the @{text Scala} serializer prints + code_printing}. For regular terms, the @{text Scala} serializer prints all type arguments explicitly. For user-defined term adaptations this is only possible for adaptations which take no arguments: here the type arguments are just appended. Otherwise they are ignored; diff -r cb0c6cb10681 -r 3662c44d018c src/Doc/IsarRef/HOL_Specific.thy --- a/src/Doc/IsarRef/HOL_Specific.thy Sun Feb 09 19:10:12 2014 +0000 +++ b/src/Doc/IsarRef/HOL_Specific.thy Sun Feb 09 21:37:27 2014 +0100 @@ -2386,13 +2386,7 @@ @{command_def (HOL) "code_deps"}@{text "\<^sup>*"} & : & @{text "context \"} \\ @{command_def (HOL) "code_reserved"} & : & @{text "theory \ theory"} \\ @{command_def (HOL) "code_printing"} & : & @{text "theory \ theory"} \\ - @{command_def (HOL) "code_const"} & : & @{text "theory \ theory"} \\ - @{command_def (HOL) "code_type"} & : & @{text "theory \ theory"} \\ - @{command_def (HOL) "code_class"} & : & @{text "theory \ theory"} \\ - @{command_def (HOL) "code_instance"} & : & @{text "theory \ theory"} \\ - @{command_def (HOL) "code_include"} & : & @{text "theory \ theory"} \\ @{command_def (HOL) "code_identifier"} & : & @{text "theory \ theory"} \\ - @{command_def (HOL) "code_modulename"} & : & @{text "theory \ theory"} \\ @{command_def (HOL) "code_monad"} & : & @{text "theory \ theory"} \\ @{command_def (HOL) "code_reflect"} & : & @{text "theory \ theory"} \\ @{command_def (HOL) "code_pred"} & : & @{text "theory \ proof(prove)"} @@ -2494,34 +2488,12 @@ | printing_module ) + '|' ) ; - @@{command (HOL) code_const} (const + @'and') \ - ( ( '(' target ( syntax ? + @'and' ) ')' ) + ) - ; - - @@{command (HOL) code_type} (typeconstructor + @'and') \ - ( ( '(' target ( syntax ? + @'and' ) ')' ) + ) - ; - - @@{command (HOL) code_class} (class + @'and') \ - ( ( '(' target \ ( @{syntax string} ? + @'and' ) ')' ) + ) - ; - - @@{command (HOL) code_instance} (( typeconstructor '::' class ) + @'and') \ - ( ( '(' target ( '-' ? + @'and' ) ')' ) + ) - ; - - @@{command (HOL) code_include} target ( @{syntax string} ( @{syntax string} | '-') ) - ; - @@{command (HOL) code_identifier} ( ( symbol_const | symbol_typeconstructor | symbol_class | symbol_class_relation | symbol_class_instance | symbol_module ) ( '\' | '=>' ) \ ( '(' target ')' @{syntax string} ? + @'and' ) + '|' ) ; - @@{command (HOL) code_modulename} target ( ( @{syntax string} @{syntax string} ) + ) - ; - @@{command (HOL) code_monad} const const target ; @@ -2629,10 +2601,7 @@ \item @{command (HOL) "code_printing"} associates a series of symbols (constants, type constructors, classes, class relations, instances, module names) with target-specific serializations; omitting a serialization - deletes an existing serialization. Legacy variants of this are - @{command (HOL) "code_const"}, @{command (HOL) "code_type"}, - @{command (HOL) "code_class"}, @{command (HOL) "code_instance"}, - @{command (HOL) "code_include"}. + deletes an existing serialization. \item @{command (HOL) "code_monad"} provides an auxiliary mechanism to generate monadic code for Haskell. @@ -2642,8 +2611,6 @@ module names) with target-specific hints how these symbols shall be named. These hints gain precedence over names for symbols with no hints at all. Conflicting hints are subject to name disambiguation. - @{command (HOL) "code_modulename"} is a legacy variant for - @{command (HOL) "code_identifier"} on module names. \emph{Warning:} It is at the discretion of the user to ensure that name prefixes of identifiers in compound statements like type classes or datatypes are still the same. diff -r cb0c6cb10681 -r 3662c44d018c src/HOL/Imperative_HOL/Heap_Monad.thy --- a/src/HOL/Imperative_HOL/Heap_Monad.thy Sun Feb 09 19:10:12 2014 +0000 +++ b/src/HOL/Imperative_HOL/Heap_Monad.thy Sun Feb 09 21:37:27 2014 +0100 @@ -575,7 +575,7 @@ text {* Adaption layer *} -code_include Haskell "Heap" +code_printing code_module "Heap" \ (Haskell) {*import qualified Control.Monad; import qualified Control.Monad.ST; import qualified Data.STRef; @@ -620,7 +620,7 @@ subsubsection {* Scala *} -code_include Scala "Heap" +code_printing code_module "Heap" \ (Scala) {*object Heap { def bind[A, B](f: Unit => A, g: A => Unit => B): Unit => B = (_: Unit) => g (f ()) () } diff -r cb0c6cb10681 -r 3662c44d018c src/Tools/Code/code_target.ML --- a/src/Tools/Code/code_target.ML Sun Feb 09 19:10:12 2014 +0000 +++ b/src/Tools/Code/code_target.ML Sun Feb 09 21:37:27 2014 +0100 @@ -53,16 +53,9 @@ type identifier_data val set_identifiers: (string, string, string, string, string, string) symbol_attr_decl -> theory -> theory - type raw_const_syntax = Code_Printer.raw_const_syntax - type tyco_syntax = Code_Printer.tyco_syntax - val set_printings: (raw_const_syntax, tyco_syntax, string, unit, unit, (string * string list)) symbol_attr_decl + val set_printings: (Code_Printer.raw_const_syntax, Code_Printer.tyco_syntax, string, unit, unit, (string * string list)) symbol_attr_decl -> theory -> theory - val add_const_syntax: string -> string -> raw_const_syntax option -> theory -> theory - val add_tyco_syntax: string -> string -> tyco_syntax option -> theory -> theory - val add_class_syntax: string -> class -> string option -> theory -> theory - val add_instance_syntax: string -> class * string -> unit option -> theory -> theory val add_reserved: string -> string -> theory -> theory - val add_include: string -> string * (string * string list) option -> theory -> theory val codegen_tool: string (*theory name*) -> string (*export_code expr*) -> unit @@ -584,15 +577,6 @@ val set_identifiers = gen_set_identifiers cert_name_decls; val set_identifiers_cmd = gen_set_identifiers read_name_decls; -fun add_module_alias_cmd target aliasses thy = - let - val _ = legacy_feature "prefer \"code_identifier\" over \"code_modulename\""; - in - fold (fn (sym, name) => set_identifier - (target, Code_Symbol.Module (sym, if name = "" then NONE else SOME (check_name true name)))) - aliasses thy - end; - (* custom printings *) @@ -620,62 +604,9 @@ val set_printings = gen_set_printings cert_printings; val set_printings_cmd = gen_set_printings read_printings; -fun gen_add_syntax Symbol prep_x prep_syn target raw_x some_raw_syn thy = - let - val _ = legacy_feature "prefer \"code_printing\" for custom serialisations" - val x = prep_x thy raw_x; - in set_printing (target, Symbol (x, Option.map (prep_syn thy target x) some_raw_syn)) thy end; - -fun gen_add_const_syntax prep_const = - gen_add_syntax Constant prep_const check_const_syntax; - -fun gen_add_tyco_syntax prep_tyco = - gen_add_syntax Type_Constructor prep_tyco check_tyco_syntax; - -fun gen_add_class_syntax prep_class = - gen_add_syntax Type_Class prep_class ((K o K o K) I); - -fun gen_add_instance_syntax prep_inst = - gen_add_syntax Class_Instance prep_inst ((K o K o K) I); - -fun gen_add_include prep_const target (name, some_content) thy = - gen_add_syntax Module (K I) - (fn thy => fn _ => fn _ => fn (raw_content, raw_cs) => (Code_Printer.str raw_content, map (prep_const thy) raw_cs)) - target name some_content thy; - (* concrete syntax *) -local - -fun zip_list (x :: xs) f g = - f - :|-- (fn y => - fold_map (fn x => g |-- f >> pair x) xs - :|-- (fn xys => pair ((x, y) :: xys))); - -fun process_multi_syntax parse_thing parse_syntax change = - (Parse.and_list1 parse_thing - :|-- (fn things => Scan.repeat1 (@{keyword "("} |-- Parse.name -- - (zip_list things (Scan.option parse_syntax) @{keyword "and"}) --| @{keyword ")"}))) - >> (Toplevel.theory oo fold) - (fn (target, syns) => fold (fn (raw_x, syn) => change target raw_x syn) syns); - -in - -val add_reserved = add_reserved; -val add_const_syntax = gen_add_const_syntax (K I); -val add_tyco_syntax = gen_add_tyco_syntax cert_tyco; -val add_class_syntax = gen_add_class_syntax cert_class; -val add_instance_syntax = gen_add_instance_syntax cert_inst; -val add_include = gen_add_include (K I); - -val add_const_syntax_cmd = gen_add_const_syntax Code.read_const; -val add_tyco_syntax_cmd = gen_add_tyco_syntax read_tyco; -val add_class_syntax_cmd = gen_add_class_syntax read_class; -val add_instance_syntax_cmd = gen_add_instance_syntax read_inst; -val add_include_cmd = gen_add_include Code.read_const; - fun parse_args f args = case Scan.read Token.stopper f args of SOME x => x @@ -736,11 +667,6 @@ >> (Toplevel.theory o fold set_identifiers_cmd)); val _ = - Outer_Syntax.command @{command_spec "code_modulename"} "alias module to other name" - (Parse.name -- Scan.repeat1 (Parse.name -- Parse.name) - >> (fn (target, modlnames) => (Toplevel.theory o add_module_alias_cmd target) modlnames)); - -val _ = Outer_Syntax.command @{command_spec "code_printing"} "declare dedicated printing for code symbols" (parse_symbol_pragmas (Code_Printer.parse_const_syntax) (Code_Printer.parse_tyco_syntax) Parse.string (Parse.minus >> K ()) (Parse.minus >> K ()) @@ -748,40 +674,9 @@ >> (Toplevel.theory o fold set_printings_cmd)); val _ = - Outer_Syntax.command @{command_spec "code_const"} "define code syntax for constant" - (process_multi_syntax Parse.term Code_Printer.parse_const_syntax - add_const_syntax_cmd); - -val _ = - Outer_Syntax.command @{command_spec "code_type"} "define code syntax for type constructor" - (process_multi_syntax Parse.type_const Code_Printer.parse_tyco_syntax - add_tyco_syntax_cmd); - -val _ = - Outer_Syntax.command @{command_spec "code_class"} "define code syntax for class" - (process_multi_syntax Parse.class Parse.string - add_class_syntax_cmd); - -val _ = - Outer_Syntax.command @{command_spec "code_instance"} "define code syntax for instance" - (process_multi_syntax parse_inst_ident (Parse.minus >> K ()) - add_instance_syntax_cmd); - -val _ = - Outer_Syntax.command @{command_spec "code_include"} - "declare piece of code to be included in generated code" - (Parse.name -- Parse.name -- (Parse.text :|-- - (fn "-" => Scan.succeed NONE - | s => Scan.optional (@{keyword "attach"} |-- Scan.repeat1 Parse.term) [] >> pair s >> SOME)) - >> (fn ((target, name), content_consts) => - (Toplevel.theory o add_include_cmd target) (name, content_consts))); - -val _ = Outer_Syntax.command @{command_spec "export_code"} "generate executable code for constants" (Parse.!!! code_exprP >> (fn f => Toplevel.keep (f o Toplevel.theory_of))); -end; (*local*) - (** external entrance point -- for codegen tool **) diff -r cb0c6cb10681 -r 3662c44d018c src/Tools/Code_Generator.thy --- a/src/Tools/Code_Generator.thy Sun Feb 09 19:10:12 2014 +0000 +++ b/src/Tools/Code_Generator.thy Sun Feb 09 21:37:27 2014 +0100 @@ -8,8 +8,7 @@ imports Pure keywords "value" "print_codeproc" "code_thms" "code_deps" :: diag and - "export_code" "code_identifier" "code_printing" "code_class" "code_instance" "code_type" - "code_const" "code_reserved" "code_include" "code_modulename" + "export_code" "code_identifier" "code_printing" "code_reserved" "code_monad" "code_reflect" :: thy_decl and "datatypes" "functions" "module_name" "file" "checking" "constant" "type_constructor" "type_class" "class_relation" "class_instance" "code_module"