# HG changeset patch # User haftmann # Date 1388534748 -3600 # Node ID cb892d835803436bf88dd8003260e0339bdbbb51 # Parent 4121d64fde90ef8513712f5c7a548201b8a17589 fundamental treatment of undefined vs. universally partial replaces code_abort diff -r 4121d64fde90 -r cb892d835803 NEWS --- a/NEWS Wed Jan 01 01:05:46 2014 +0100 +++ b/NEWS Wed Jan 01 01:05:48 2014 +0100 @@ -33,6 +33,12 @@ *** HOL *** +* "declare [[code abort: …]]" replaces "code_abort …". +INCOMPATIBILITY. + +* "declare [[code drop: …]]" drops all code equations associated +with the given constants. + * Abolished slightly odd global lattice interpretation for min/max. Fact consolidations: diff -r 4121d64fde90 -r cb892d835803 src/Doc/Codegen/Foundations.thy --- a/src/Doc/Codegen/Foundations.thy Wed Jan 01 01:05:46 2014 +0100 +++ b/src/Doc/Codegen/Foundations.thy Wed Jan 01 01:05:48 2014 +0100 @@ -308,10 +308,11 @@ of as function definitions which always fail, since there is never a successful pattern match on the left hand side. In order to categorise a constant into that category - explicitly, use @{command_def "code_abort"}: + explicitly, use the @{attribute code} attribute with + @{text abort}: *} -code_abort %quote empty_queue +declare %quote [[code abort: empty_queue]] text {* \noindent Then the code generator will just insert an error or @@ -324,9 +325,9 @@ text {* \noindent This feature however is rarely needed in practice. Note - also that the HOL default setup already declares @{const undefined} - as @{command "code_abort"}, which is most likely to be used in such - situations. + also that the HOL default setup already declares @{const undefined}, + which is most likely to be used in such situations, as + @{text "code abort"}. *} diff -r 4121d64fde90 -r cb892d835803 src/Doc/IsarRef/HOL_Specific.thy --- a/src/Doc/IsarRef/HOL_Specific.thy Wed Jan 01 01:05:46 2014 +0100 +++ b/src/Doc/IsarRef/HOL_Specific.thy Wed Jan 01 01:05:48 2014 +0100 @@ -2391,7 +2391,6 @@ \begin{matharray}{rcl} @{command_def (HOL) "export_code"}@{text "\<^sup>*"} & : & @{text "context \"} \\ @{attribute_def (HOL) code} & : & @{text attribute} \\ - @{command_def (HOL) "code_abort"} & : & @{text "theory \ theory"} \\ @{command_def (HOL) "code_datatype"} & : & @{text "theory \ theory"} \\ @{command_def (HOL) "print_codesetup"}@{text "\<^sup>*"} & : & @{text "context \"} \\ @{attribute_def (HOL) code_unfold} & : & @{text attribute} \\ @@ -2435,10 +2434,8 @@ target: 'SML' | 'OCaml' | 'Haskell' | 'Scala' | 'Eval' ; - @@{attribute (HOL) code} ( 'del' | 'equation' | 'abstype' | 'abstract' )? - ; - - @@{command (HOL) code_abort} ( const + ) + @@{attribute (HOL) code} ( 'del' | 'equation' | 'abstype' | 'abstract' + | 'drop:' ( const + ) | 'abort:' ( const + ) )? ; @@{command (HOL) code_datatype} ( const + ) @@ -2600,13 +2597,15 @@ of the underlying equation. Variant @{text "code del"} deselects a code equation for code generation. + Variants @{text "code drop:"} and @{text "code abort:"} take + a list of constant as arguments and drop all code equations declared + for them. In the case of {text abort}, these constants then are + are not required to have a definition by means of code equations; + if needed these are implemented by program abort (exception) instead. + Usually packages introducing code equations provide a reasonable default setup for selection. - \item @{command (HOL) "code_abort"} declares constants which are not - required to have a definition by means of code equations; if needed - these are implemented by program abort instead. - \item @{command (HOL) "code_datatype"} specifies a constructor set for a logical type. diff -r 4121d64fde90 -r cb892d835803 src/HOL/Enum.thy --- a/src/HOL/Enum.thy Wed Jan 01 01:05:46 2014 +0100 +++ b/src/HOL/Enum.thy Wed Jan 01 01:05:48 2014 +0100 @@ -116,7 +116,7 @@ unfolding enum_the_def by (auto split: list.split) qed -code_abort enum_the +declare [[code abort: enum_the]] code_printing constant enum_the \ (Eval) "(fn '_ => raise Match)" diff -r 4121d64fde90 -r cb892d835803 src/HOL/HOL.thy --- a/src/HOL/HOL.thy Wed Jan 01 01:05:46 2014 +0100 +++ b/src/HOL/HOL.thy Wed Jan 01 01:05:48 2014 +0100 @@ -1832,7 +1832,7 @@ #> Code.add_undefined @{const_name undefined} *} -code_abort undefined +declare [[code abort: undefined]] subsubsection {* Generic code generator target languages *} diff -r 4121d64fde90 -r cb892d835803 src/HOL/Library/Product_Vector.thy --- a/src/HOL/Library/Product_Vector.thy Wed Jan 01 01:05:46 2014 +0100 +++ b/src/HOL/Library/Product_Vector.thy Wed Jan 01 01:05:48 2014 +0100 @@ -87,7 +87,7 @@ end -code_abort "open::('a::topological_space*'b::topological_space) set \ bool" +declare [[code abort: "open::('a::topological_space*'b::topological_space) set \ bool"]] lemma open_Times: "open S \ open T \ open (S \ T)" unfolding open_prod_def by auto @@ -346,7 +346,7 @@ end -code_abort "dist::('a::metric_space*'b::metric_space)\('a*'b) \ real" +declare [[code abort: "dist::('a::metric_space*'b::metric_space)\('a*'b) \ real"]] lemma Cauchy_fst: "Cauchy X \ Cauchy (\n. fst (X n))" unfolding Cauchy_def by (fast elim: le_less_trans [OF dist_fst_le]) @@ -426,7 +426,7 @@ end -code_abort "norm::('a::real_normed_vector*'b::real_normed_vector) \ real" +declare [[code abort: "norm::('a::real_normed_vector*'b::real_normed_vector) \ real"]] instance prod :: (banach, banach) banach .. diff -r 4121d64fde90 -r cb892d835803 src/HOL/List.thy --- a/src/HOL/List.thy Wed Jan 01 01:05:46 2014 +0100 +++ b/src/HOL/List.thy Wed Jan 01 01:05:48 2014 +0100 @@ -6133,7 +6133,7 @@ definition "abort_Bleast S P = (LEAST x. x \ S \ P x)" -code_abort abort_Bleast +declare [[code abort: abort_Bleast]] lemma Bleast_code [code]: "Bleast (set xs) P = (case filter P (sort xs) of diff -r 4121d64fde90 -r cb892d835803 src/HOL/Real_Vector_Spaces.thy --- a/src/HOL/Real_Vector_Spaces.thy Wed Jan 01 01:05:46 2014 +0100 +++ b/src/HOL/Real_Vector_Spaces.thy Wed Jan 01 01:05:48 2014 +0100 @@ -968,7 +968,7 @@ end -code_abort "open :: real set \ bool" +declare [[code abort: "open :: real set \ bool"]] instance real :: linorder_topology proof diff -r 4121d64fde90 -r cb892d835803 src/Tools/Code/code_target.ML --- a/src/Tools/Code/code_target.ML Wed Jan 01 01:05:46 2014 +0100 +++ b/src/Tools/Code/code_target.ML Wed Jan 01 01:05:48 2014 +0100 @@ -64,7 +64,6 @@ 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 allow_abort: string -> theory -> theory val codegen_tool: string (*theory name*) -> string (*export_code expr*) -> unit @@ -231,23 +230,20 @@ structure Targets = Theory_Data ( - type T = (target Symtab.table * string list) * int; - val empty = ((Symtab.empty, []), 80); + type T = target Symtab.table * int; + val empty = (Symtab.empty, 80); val extend = I; - fun merge (((target1, exc1), width1), ((target2, exc2), width2)) : T = - ((Symtab.join (merge_target true) (target1, target2), - Library.merge (op =) (exc1, exc2)), Int.max (width1, width2)); + fun merge ((target1, width1), (target2, width2)) : T = + (Symtab.join (merge_target true) (target1, target2), Int.max (width1, width2)); ); -val abort_allowed = snd o fst o Targets.get; - -fun assert_target thy target = if Symtab.defined ((fst o fst) (Targets.get thy)) target +fun assert_target thy target = if Symtab.defined (fst (Targets.get thy)) target then target else error ("Unknown code target language: " ^ quote target); fun put_target (target, seri) thy = let - val lookup_target = Symtab.lookup ((fst o fst) (Targets.get thy)); + val lookup_target = Symtab.lookup (fst (Targets.get thy)); val _ = case seri of Extension (super, _) => if is_some (lookup_target super) then () else error ("Unknown code target language: " ^ quote super) @@ -263,7 +259,7 @@ else (); in thy - |> (Targets.map o apfst o apfst o Symtab.update) + |> (Targets.map o apfst o Symtab.update) (target, make_target ((serial (), seri), ([], (Code_Symbol.empty_data, Code_Symbol.empty_data)))) end; @@ -277,7 +273,7 @@ val _ = assert_target thy target; in thy - |> (Targets.map o apfst o apfst o Symtab.map_entry target o map_target o apsnd) f + |> (Targets.map o apfst o Symtab.map_entry target o map_target o apsnd) f end; fun map_reserved target = @@ -296,7 +292,7 @@ fun the_fundamental thy = let - val ((targets, _), _) = Targets.get thy; + val (targets, _) = Targets.get thy; fun fundamental target = case Symtab.lookup targets target of SOME data => (case the_description data of Fundamental data => data @@ -308,7 +304,7 @@ fun collapse_hierarchy thy = let - val ((targets, _), _) = Targets.get thy; + val (targets, _) = Targets.get thy; fun collapse target = let val data = case Symtab.lookup targets target @@ -326,9 +322,9 @@ fun activate_target thy target = let - val ((_, abortable), default_width) = Targets.get thy; + val (_, default_width) = Targets.get thy; val (modify, data) = collapse_hierarchy thy target; - in (default_width, abortable, data, modify) end; + in (default_width, data, modify) end; fun activate_const_syntax thy literals cs_data naming = (Symtab.empty, naming) @@ -363,14 +359,13 @@ (const_syntax, tyco_syntax, class_syntax)) end; -fun project_program thy abortable names_hidden names1 program2 = +fun project_program thy names_hidden names1 program2 = let val ctxt = Proof_Context.init_global thy; val names2 = subtract (op =) names_hidden names1; val program3 = Graph.restrict (not o member (op =) names_hidden) program2; val names4 = Graph.all_succs program3 names2; - val unimplemented = filter_out (member (op =) abortable) - (Code_Thingol.unimplemented program3); + val unimplemented = Code_Thingol.unimplemented program3; val _ = if null unimplemented then () else error ("No code equations for " ^ @@ -378,12 +373,12 @@ val program4 = Graph.restrict (member (op =) names4) program3; in (names4, program4) end; -fun prepare_serializer thy abortable (serializer : serializer) literals reserved identifiers +fun prepare_serializer thy (serializer : serializer) literals reserved identifiers printings module_name args naming proto_program names = let val (names_hidden, (const_syntax, tyco_syntax, class_syntax)) = activate_symbol_syntax thy literals naming printings; - val (names_all, program) = project_program thy abortable names_hidden names proto_program; + val (names_all, program) = project_program thy names_hidden names proto_program; fun select_include (name, (content, cs)) = if null cs orelse exists (fn c => case Code_Thingol.lookup_const naming c of SOME name => member (op =) names_all name @@ -405,11 +400,11 @@ fun mount_serializer thy target some_width module_name args naming program names = let - val (default_width, abortable, data, modify) = activate_target thy target; + val (default_width, data, modify) = activate_target thy target; val serializer = case the_description data of Fundamental seri => #serializer seri; val (prepared_serializer, prepared_program) = - prepare_serializer thy abortable serializer (the_literals thy target) + prepare_serializer thy serializer (the_literals thy target) (the_reserved data) (the_identifiers data) (the_printings data) module_name args naming (modify naming program) names val width = the_default default_width some_width; @@ -502,7 +497,7 @@ fun implemented_functions thy naming program = let - val cs = subtract (op =) (abort_allowed thy) (Code_Thingol.unimplemented program); + val cs = Code_Thingol.unimplemented program; val names = map_filter (Code_Thingol.lookup_const naming) cs; in subtract (op =) (Graph.all_preds program names) (Graph.keys program) end; @@ -699,14 +694,6 @@ target name some_content thy; -(* abortable constants *) - -fun gen_allow_abort prep_const raw_c thy = - let - val c = prep_const thy raw_c; - in thy |> (Targets.map o apfst o apsnd) (insert (op =) c) end; - - (* concrete syntax *) local @@ -732,14 +719,12 @@ 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 allow_abort = gen_allow_abort (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; -val allow_abort_cmd = gen_allow_abort Code.read_const; fun parse_args f args = case Scan.read Token.stopper f args @@ -842,11 +827,6 @@ (Toplevel.theory o add_include_cmd target) (name, content_consts))); val _ = - Outer_Syntax.command @{command_spec "code_abort"} - "permit constant to be implemented as program abort" - (Scan.repeat1 Parse.term >> (Toplevel.theory o fold allow_abort_cmd)); - -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))); diff -r 4121d64fde90 -r cb892d835803 src/Tools/Code_Generator.thy --- a/src/Tools/Code_Generator.thy Wed Jan 01 01:05:46 2014 +0100 +++ b/src/Tools/Code_Generator.thy Wed Jan 01 01:05:48 2014 +0100 @@ -10,7 +10,7 @@ "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" - "code_abort" "code_monad" "code_reflect" :: thy_decl and + "code_monad" "code_reflect" :: thy_decl and "datatypes" "functions" "module_name" "file" "checking" "constant" "type_constructor" "type_class" "class_relation" "class_instance" "code_module" begin