--- a/NEWS Fri Oct 21 11:27:21 2011 +0200
+++ b/NEWS Fri Oct 21 16:21:12 2011 +0200
@@ -13,6 +13,9 @@
'code_library', 'consts_code', 'types_code' have been discontinued.
Use commands of the generic code generator instead. INCOMPATIBILITY.
+* Redundant attribute 'code_inline' has been discontinued. Use 'code_unfold'
+instead. INCOMPATIBILITY.
+
*** HOL ***
* 'Transitive_Closure.ntrancl': bounded transitive closure on relations.
--- a/doc-src/IsarRef/Thy/HOL_Specific.thy Fri Oct 21 11:27:21 2011 +0200
+++ b/doc-src/IsarRef/Thy/HOL_Specific.thy Fri Oct 21 16:21:12 2011 +0200
@@ -1744,8 +1744,9 @@
@{command_def (HOL) "code_abort"} & : & @{text "theory \<rightarrow> theory"} \\
@{command_def (HOL) "code_datatype"} & : & @{text "theory \<rightarrow> theory"} \\
@{command_def (HOL) "print_codesetup"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\
- @{attribute_def (HOL) code_inline} & : & @{text attribute} \\
+ @{attribute_def (HOL) code_unfold} & : & @{text attribute} \\
@{attribute_def (HOL) code_post} & : & @{text attribute} \\
+ @{attribute_def (HOL) code_unfold_post} & : & @{text attribute} \\
@{command_def (HOL) "print_codeproc"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\
@{command_def (HOL) "code_thms"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\
@{command_def (HOL) "code_deps"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\
@@ -1790,12 +1791,15 @@
@@{command (HOL) code_datatype} ( const + )
;
- @@{attribute (HOL) code_inline} ( 'del' ) ?
+ @@{attribute (HOL) code_unfold} ( 'del' ) ?
;
@@{attribute (HOL) code_post} ( 'del' ) ?
;
+ @@{attribute (HOL) code_unfold_post}
+ ;
+
@@{command (HOL) code_thms} ( constexpr + ) ?
;
@@ -1887,14 +1891,18 @@
\item @{command (HOL) "print_codesetup"} gives an overview on
selected code equations and code generator datatypes.
- \item @{attribute (HOL) code_inline} declares (or with option
- ``@{text "del"}'' removes) inlining theorems which are applied as
+ \item @{attribute (HOL) code_unfold} declares (or with option
+ ``@{text "del"}'' removes) theorems which are applied as
rewrite rules to any code equation during preprocessing.
\item @{attribute (HOL) code_post} declares (or with option ``@{text
"del"}'' removes) theorems which are applied as rewrite rules to any
result of an evaluation.
+ \item @{attribute (HOL) code_unfold_post} declares equations which are
+ applied as rewrite rules to any code equation during preprocessing,
+ and symmetrically to any result of an evaluation.
+
\item @{command (HOL) "print_codeproc"} prints the setup of the code
generator preprocessor.
--- a/doc-src/IsarRef/Thy/document/HOL_Specific.tex Fri Oct 21 11:27:21 2011 +0200
+++ b/doc-src/IsarRef/Thy/document/HOL_Specific.tex Fri Oct 21 16:21:12 2011 +0200
@@ -2543,8 +2543,9 @@
\indexdef{HOL}{command}{code\_abort}\hypertarget{command.HOL.code-abort}{\hyperlink{command.HOL.code-abort}{\mbox{\isa{\isacommand{code{\isaliteral{5F}{\isacharunderscore}}abort}}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}theory\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ theory{\isaliteral{22}{\isachardoublequote}}} \\
\indexdef{HOL}{command}{code\_datatype}\hypertarget{command.HOL.code-datatype}{\hyperlink{command.HOL.code-datatype}{\mbox{\isa{\isacommand{code{\isaliteral{5F}{\isacharunderscore}}datatype}}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}theory\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ theory{\isaliteral{22}{\isachardoublequote}}} \\
\indexdef{HOL}{command}{print\_codesetup}\hypertarget{command.HOL.print-codesetup}{\hyperlink{command.HOL.print-codesetup}{\mbox{\isa{\isacommand{print{\isaliteral{5F}{\isacharunderscore}}codesetup}}}}}\isa{{\isaliteral{22}{\isachardoublequote}}\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isaliteral{2A}{\isacharasterisk}}{\isaliteral{22}{\isachardoublequote}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}context\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}{\isaliteral{22}{\isachardoublequote}}} \\
- \indexdef{HOL}{attribute}{code\_inline}\hypertarget{attribute.HOL.code-inline}{\hyperlink{attribute.HOL.code-inline}{\mbox{\isa{code{\isaliteral{5F}{\isacharunderscore}}inline}}}} & : & \isa{attribute} \\
+ \indexdef{HOL}{attribute}{code\_unfold}\hypertarget{attribute.HOL.code-unfold}{\hyperlink{attribute.HOL.code-unfold}{\mbox{\isa{code{\isaliteral{5F}{\isacharunderscore}}unfold}}}} & : & \isa{attribute} \\
\indexdef{HOL}{attribute}{code\_post}\hypertarget{attribute.HOL.code-post}{\hyperlink{attribute.HOL.code-post}{\mbox{\isa{code{\isaliteral{5F}{\isacharunderscore}}post}}}} & : & \isa{attribute} \\
+ \indexdef{HOL}{attribute}{code\_unfold\_post}\hypertarget{attribute.HOL.code-unfold-post}{\hyperlink{attribute.HOL.code-unfold-post}{\mbox{\isa{code{\isaliteral{5F}{\isacharunderscore}}unfold{\isaliteral{5F}{\isacharunderscore}}post}}}} & : & \isa{attribute} \\
\indexdef{HOL}{command}{print\_codeproc}\hypertarget{command.HOL.print-codeproc}{\hyperlink{command.HOL.print-codeproc}{\mbox{\isa{\isacommand{print{\isaliteral{5F}{\isacharunderscore}}codeproc}}}}}\isa{{\isaliteral{22}{\isachardoublequote}}\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isaliteral{2A}{\isacharasterisk}}{\isaliteral{22}{\isachardoublequote}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}context\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}{\isaliteral{22}{\isachardoublequote}}} \\
\indexdef{HOL}{command}{code\_thms}\hypertarget{command.HOL.code-thms}{\hyperlink{command.HOL.code-thms}{\mbox{\isa{\isacommand{code{\isaliteral{5F}{\isacharunderscore}}thms}}}}}\isa{{\isaliteral{22}{\isachardoublequote}}\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isaliteral{2A}{\isacharasterisk}}{\isaliteral{22}{\isachardoublequote}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}context\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}{\isaliteral{22}{\isachardoublequote}}} \\
\indexdef{HOL}{command}{code\_deps}\hypertarget{command.HOL.code-deps}{\hyperlink{command.HOL.code-deps}{\mbox{\isa{\isacommand{code{\isaliteral{5F}{\isacharunderscore}}deps}}}}}\isa{{\isaliteral{22}{\isachardoublequote}}\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isaliteral{2A}{\isacharasterisk}}{\isaliteral{22}{\isachardoublequote}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}context\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}{\isaliteral{22}{\isachardoublequote}}} \\
@@ -2654,7 +2655,7 @@
\rail@endplus
\rail@end
\rail@begin{2}{}
-\rail@term{\hyperlink{attribute.HOL.code-inline}{\mbox{\isa{code{\isaliteral{5F}{\isacharunderscore}}inline}}}}[]
+\rail@term{\hyperlink{attribute.HOL.code-unfold}{\mbox{\isa{code{\isaliteral{5F}{\isacharunderscore}}unfold}}}}[]
\rail@bar
\rail@nextbar{1}
\rail@term{\isa{del}}[]
@@ -2667,6 +2668,9 @@
\rail@term{\isa{del}}[]
\rail@endbar
\rail@end
+\rail@begin{1}{}
+\rail@term{\hyperlink{attribute.HOL.code-unfold-post}{\mbox{\isa{code{\isaliteral{5F}{\isacharunderscore}}unfold{\isaliteral{5F}{\isacharunderscore}}post}}}}[]
+\rail@end
\rail@begin{3}{}
\rail@term{\hyperlink{command.HOL.code-thms}{\mbox{\isa{\isacommand{code{\isaliteral{5F}{\isacharunderscore}}thms}}}}}[]
\rail@bar
@@ -2919,13 +2923,17 @@
\item \hyperlink{command.HOL.print-codesetup}{\mbox{\isa{\isacommand{print{\isaliteral{5F}{\isacharunderscore}}codesetup}}}} gives an overview on
selected code equations and code generator datatypes.
- \item \hyperlink{attribute.HOL.code-inline}{\mbox{\isa{code{\isaliteral{5F}{\isacharunderscore}}inline}}} declares (or with option
- ``\isa{{\isaliteral{22}{\isachardoublequote}}del{\isaliteral{22}{\isachardoublequote}}}'' removes) inlining theorems which are applied as
+ \item \hyperlink{attribute.HOL.code-unfold}{\mbox{\isa{code{\isaliteral{5F}{\isacharunderscore}}unfold}}} declares (or with option
+ ``\isa{{\isaliteral{22}{\isachardoublequote}}del{\isaliteral{22}{\isachardoublequote}}}'' removes) theorems which are applied as
rewrite rules to any code equation during preprocessing.
\item \hyperlink{attribute.HOL.code-post}{\mbox{\isa{code{\isaliteral{5F}{\isacharunderscore}}post}}} declares (or with option ``\isa{{\isaliteral{22}{\isachardoublequote}}del{\isaliteral{22}{\isachardoublequote}}}'' removes) theorems which are applied as rewrite rules to any
result of an evaluation.
+ \item \hyperlink{attribute.HOL.code-unfold-post}{\mbox{\isa{code{\isaliteral{5F}{\isacharunderscore}}unfold{\isaliteral{5F}{\isacharunderscore}}post}}} declares equations which are
+ applied as rewrite rules to any code equation during preprocessing,
+ and symmetrically to any result of an evaluation.
+
\item \hyperlink{command.HOL.print-codeproc}{\mbox{\isa{\isacommand{print{\isaliteral{5F}{\isacharunderscore}}codeproc}}}} prints the setup of the code
generator preprocessor.
--- a/src/HOL/Divides.thy Fri Oct 21 11:27:21 2011 +0200
+++ b/src/HOL/Divides.thy Fri Oct 21 16:21:12 2011 +0200
@@ -131,7 +131,7 @@
note that ultimately show thesis by blast
qed
-lemma dvd_eq_mod_eq_0 [code, code_unfold, code_inline del]: "a dvd b \<longleftrightarrow> b mod a = 0"
+lemma dvd_eq_mod_eq_0 [code]: "a dvd b \<longleftrightarrow> b mod a = 0"
proof
assume "b mod a = 0"
with mod_div_equality [of b a] have "b div a * a = b" by simp
--- a/src/HOL/HOL.thy Fri Oct 21 11:27:21 2011 +0200
+++ b/src/HOL/HOL.thy Fri Oct 21 16:21:12 2011 +0200
@@ -1729,7 +1729,7 @@
assumes equal_eq: "equal x y \<longleftrightarrow> x = y"
begin
-lemma equal [code_unfold, code_inline del]: "equal = (op =)"
+lemma equal: "equal = (op =)"
by (rule ext equal_eq)+
lemma equal_refl: "equal x x \<longleftrightarrow> True"
--- a/src/HOL/Imperative_HOL/Heap_Monad.thy Fri Oct 21 11:27:21 2011 +0200
+++ b/src/HOL/Imperative_HOL/Heap_Monad.thy Fri Oct 21 16:21:12 2011 +0200
@@ -495,7 +495,7 @@
lemma [code_post]: "raise' (STR s) = raise s"
unfolding raise'_def by (simp add: STR_inverse)
-lemma raise_raise' [code_inline]:
+lemma raise_raise' [code_unfold]:
"raise s = raise' (STR s)"
unfolding raise'_def by (simp add: STR_inverse)
--- a/src/HOL/Library/Executable_Set.thy Fri Oct 21 11:27:21 2011 +0200
+++ b/src/HOL/Library/Executable_Set.thy Fri Oct 21 16:21:12 2011 +0200
@@ -67,7 +67,7 @@
"{} = empty"
by simp
-lemma [code_unfold, code_inline del]:
+lemma
"empty = Set []"
by simp -- {* Otherwise @{text \<eta>}-expansion produces funny things. *}
--- a/src/HOL/Library/Extended_Real.thy Fri Oct 21 11:27:21 2011 +0200
+++ b/src/HOL/Library/Extended_Real.thy Fri Oct 21 16:21:12 2011 +0200
@@ -1362,8 +1362,7 @@
}
moreover
{ assume "?lhs" hence "?rhs"
- by (metis SUP_least assms atLeastatMost_empty atLeastatMost_empty_iff
- inf_sup_ord(4) linorder_le_cases sup_absorb1 xt1(8))
+ by (metis less_SUP_iff order_less_imp_le order_less_le_trans)
} ultimately show ?thesis by auto
qed
@@ -1382,8 +1381,7 @@
}
moreover
{ assume "?lhs" hence "?rhs"
- by (metis INF_greatest assms atLeastatMost_empty atLeastatMost_empty_iff
- inf_sup_ord(4) linorder_le_cases sup_absorb1 xt1(8))
+ by (metis INF_less_iff order_le_less order_less_le_trans)
} ultimately show ?thesis by auto
qed
--- a/src/HOL/Library/List_Prefix.thy Fri Oct 21 11:27:21 2011 +0200
+++ b/src/HOL/Library/List_Prefix.thy Fri Oct 21 16:21:12 2011 +0200
@@ -74,7 +74,7 @@
next
assume "xs = ys @ [y] \<or> xs \<le> ys"
then show "xs \<le> ys @ [y]"
- by (metis order_eq_iff strict_prefixE strict_prefixI' xt1(7))
+ by (metis order_eq_iff order_trans prefixI)
qed
lemma Cons_prefix_Cons [simp]: "(x # xs \<le> y # ys) = (x = y \<and> xs \<le> ys)"
--- a/src/HOL/Library/Mapping.thy Fri Oct 21 11:27:21 2011 +0200
+++ b/src/HOL/Library/Mapping.thy Fri Oct 21 16:21:12 2011 +0200
@@ -90,7 +90,7 @@
subsection {* Properties *}
-lemma keys_is_none_lookup [code_inline]:
+lemma keys_is_none_lookup [code_unfold]:
"k \<in> keys m \<longleftrightarrow> \<not> (Option.is_none (lookup m k))"
by (auto simp add: keys_def is_none_def)
--- a/src/HOL/Library/Predicate_Compile_Alternative_Defs.thy Fri Oct 21 11:27:21 2011 +0200
+++ b/src/HOL/Library/Predicate_Compile_Alternative_Defs.thy Fri Oct 21 16:21:12 2011 +0200
@@ -84,7 +84,7 @@
definition subtract
where
- [code_inline]: "subtract x y = y - x"
+ [code_unfold]: "subtract x y = y - x"
setup {*
let
--- a/src/HOL/Library/Transitive_Closure_Table.thy Fri Oct 21 11:27:21 2011 +0200
+++ b/src/HOL/Library/Transitive_Closure_Table.thy Fri Oct 21 16:21:12 2011 +0200
@@ -185,8 +185,6 @@
by (auto simp add: rtranclp_eq_rtrancl_path)
qed
-declare rtranclp_eq_rtrancl_tab_nil [code_unfold, code_inline del]
-
declare rtranclp_eq_rtrancl_tab_nil[THEN iffD2, code_pred_intro]
code_pred rtranclp using rtranclp_eq_rtrancl_tab_nil [THEN iffD1] by fastforce
--- a/src/HOL/MicroJava/J/JListExample.thy Fri Oct 21 11:27:21 2011 +0200
+++ b/src/HOL/MicroJava/J/JListExample.thy Fri Oct 21 16:21:12 2011 +0200
@@ -118,12 +118,12 @@
definition undefined_cname :: cname
where [code del]: "undefined_cname = undefined"
-declare undefined_cname_def[symmetric, code_inline]
+declare undefined_cname_def[symmetric, code_unfold]
code_datatype Object Xcpt Cname undefined_cname
definition undefined_val :: val
where [code del]: "undefined_val = undefined"
-declare undefined_val_def[symmetric, code_inline]
+declare undefined_val_def[symmetric, code_unfold]
code_datatype Unit Null Bool Intg Addr undefined_val
definition E where
--- a/src/HOL/MicroJava/J/SystemClasses.thy Fri Oct 21 11:27:21 2011 +0200
+++ b/src/HOL/MicroJava/J/SystemClasses.thy Fri Oct 21 16:21:12 2011 +0200
@@ -13,18 +13,18 @@
*}
definition ObjectC :: "'c cdecl" where
- [code_inline]: "ObjectC \<equiv> (Object, (undefined,[],[]))"
+ [code_unfold]: "ObjectC \<equiv> (Object, (undefined,[],[]))"
definition NullPointerC :: "'c cdecl" where
- [code_inline]: "NullPointerC \<equiv> (Xcpt NullPointer, (Object,[],[]))"
+ [code_unfold]: "NullPointerC \<equiv> (Xcpt NullPointer, (Object,[],[]))"
definition ClassCastC :: "'c cdecl" where
- [code_inline]: "ClassCastC \<equiv> (Xcpt ClassCast, (Object,[],[]))"
+ [code_unfold]: "ClassCastC \<equiv> (Xcpt ClassCast, (Object,[],[]))"
definition OutOfMemoryC :: "'c cdecl" where
- [code_inline]: "OutOfMemoryC \<equiv> (Xcpt OutOfMemory, (Object,[],[]))"
+ [code_unfold]: "OutOfMemoryC \<equiv> (Xcpt OutOfMemory, (Object,[],[]))"
definition SystemClasses :: "'c cdecl list" where
- [code_inline]: "SystemClasses \<equiv> [ObjectC, NullPointerC, ClassCastC, OutOfMemoryC]"
+ [code_unfold]: "SystemClasses \<equiv> [ObjectC, NullPointerC, ClassCastC, OutOfMemoryC]"
end
--- a/src/HOL/MicroJava/J/TypeRel.thy Fri Oct 21 11:27:21 2011 +0200
+++ b/src/HOL/MicroJava/J/TypeRel.thy Fri Oct 21 16:21:12 2011 +0200
@@ -97,7 +97,7 @@
[inductify]
subcls'
.
-lemma subcls_conv_subcls' [code_inline]:
+lemma subcls_conv_subcls' [code_unfold]:
"(subcls1 G)^* = (\<lambda>(C, D). subcls' G C D)"
by(simp add: subcls'_def subcls1_def rtrancl_def)(simp add: Collect_def)
--- a/src/HOL/MicroJava/JVM/JVMListExample.thy Fri Oct 21 11:27:21 2011 +0200
+++ b/src/HOL/MicroJava/JVM/JVMListExample.thy Fri Oct 21 16:21:12 2011 +0200
@@ -125,11 +125,11 @@
definition undefined_cname :: cname
where [code del]: "undefined_cname = undefined"
code_datatype Object Xcpt Cname undefined_cname
-declare undefined_cname_def[symmetric, code_inline]
+declare undefined_cname_def[symmetric, code_unfold]
definition undefined_val :: val
where [code del]: "undefined_val = undefined"
-declare undefined_val_def[symmetric, code_inline]
+declare undefined_val_def[symmetric, code_unfold]
code_datatype Unit Null Bool Intg Addr undefined_val
definition
--- a/src/HOL/Nat.thy Fri Oct 21 11:27:21 2011 +0200
+++ b/src/HOL/Nat.thy Fri Oct 21 16:21:12 2011 +0200
@@ -1301,7 +1301,7 @@
end
-declare of_nat_code [code, code_unfold, code_inline del]
+declare of_nat_code [code]
text{*Class for unital semirings with characteristic zero.
Includes non-ordered rings like the complex numbers.*}
--- a/src/HOL/Orderings.thy Fri Oct 21 11:27:21 2011 +0200
+++ b/src/HOL/Orderings.thy Fri Oct 21 16:21:12 2011 +0200
@@ -305,13 +305,13 @@
text {* Explicit dictionaries for code generation *}
-lemma min_ord_min [code, code_unfold, code_inline del]:
+lemma min_ord_min [code]:
"min = ord.min (op \<le>)"
by (rule ext)+ (simp add: min_def ord.min_def)
declare ord.min_def [code]
-lemma max_ord_max [code, code_unfold, code_inline del]:
+lemma max_ord_max [code]:
"max = ord.max (op \<le>)"
by (rule ext)+ (simp add: max_def ord.max_def)
--- a/src/HOL/Power.thy Fri Oct 21 11:27:21 2011 +0200
+++ b/src/HOL/Power.thy Fri Oct 21 16:21:12 2011 +0200
@@ -460,7 +460,7 @@
subsection {* Code generator tweak *}
-lemma power_power_power [code, code_unfold, code_inline del]:
+lemma power_power_power [code]:
"power = power.power (1::'a::{power}) (op *)"
unfolding power_def power.power_def ..
--- a/src/HOL/Tools/ATP/atp_proof.ML Fri Oct 21 11:27:21 2011 +0200
+++ b/src/HOL/Tools/ATP/atp_proof.ML Fri Oct 21 16:21:12 2011 +0200
@@ -247,36 +247,37 @@
|| Scan.repeat ($$ "$") -- Scan.many1 Symbol.is_letdig
>> (fn (ss1, ss2) => implode ss1 ^ implode ss2)
-val dummy_phi = AAtom (ATerm ("", []))
-
-fun skip_formula ss =
+val skip_term =
let
- fun skip _ [] = []
- | skip 0 (ss as "," :: _) = ss
- | skip 0 (ss as ")" :: _) = ss
- | skip 0 (ss as "]" :: _) = ss
- | skip n ("(" :: ss) = skip (n + 1) ss
- | skip n ("[" :: ss) = skip (n + 1) ss
- | skip n ("]" :: ss) = skip (n - 1) ss
- | skip n (")" :: ss) = skip (n - 1) ss
- | skip n (_ :: ss) = skip n ss
- in (dummy_phi, skip 0 ss) end
+ fun skip _ accum [] = (accum, [])
+ | skip 0 accum (ss as "," :: _) = (accum, ss)
+ | skip 0 accum (ss as ")" :: _) = (accum, ss)
+ | skip 0 accum (ss as "]" :: _) = (accum, ss)
+ | skip n accum ((s as "(") :: ss) = skip (n + 1) (s :: accum) ss
+ | skip n accum ((s as "[") :: ss) = skip (n + 1) (s :: accum) ss
+ | skip n accum ((s as "]") :: ss) = skip (n - 1) (s :: accum) ss
+ | skip n accum ((s as ")") :: ss) = skip (n - 1) (s :: accum) ss
+ | skip n accum (s :: ss) = skip n (s :: accum) ss
+ in skip 0 [] #>> (rev #> implode) end
datatype source =
File_Source of string * string option |
Inference_Source of string * string list
-fun parse_dependencies x =
- (scan_general_id ::: Scan.repeat ($$ "," |-- scan_general_id)) x
+val dummy_phi = AAtom (ATerm ("", []))
+val dummy_inference = Inference_Source ("", [])
+
+fun parse_dependencies x = (skip_term ::: Scan.repeat ($$ "," |-- skip_term)) x
fun parse_source x =
(Scan.this_string "file" |-- $$ "(" |-- scan_general_id --
Scan.option ($$ "," |-- scan_general_id) --| $$ ")"
>> File_Source
|| Scan.this_string "inference" |-- $$ "(" |-- scan_general_id
- --| skip_formula --| $$ "," --| skip_formula --| $$ "," --| $$ "["
+ --| skip_term --| $$ "," --| skip_term --| $$ "," --| $$ "["
-- parse_dependencies --| $$ "]" --| $$ ")"
- >> Inference_Source) x
+ >> Inference_Source
+ || skip_term >> K dummy_inference) x
fun list_app (f, args) =
fold (fn arg => fn f => ATerm (tptp_app, [f, arg])) args f
@@ -345,9 +346,8 @@
AQuant (q, map (rpair NONE o ho_term_head) ts, phi))) x
val parse_tstp_extra_arguments =
- Scan.optional ($$ "," |-- parse_source
- --| Scan.option ($$ "," |-- skip_formula))
- (Inference_Source ("", []))
+ Scan.optional ($$ "," |-- parse_source --| Scan.option ($$ "," |-- skip_term))
+ dummy_inference
val waldmeister_conjecture = "conjecture_1"
@@ -399,8 +399,8 @@
((Scan.this_string tptp_cnf || Scan.this_string tptp_fof
|| Scan.this_string tptp_tff || Scan.this_string tptp_thf) -- $$ "(")
|-- scan_general_id --| $$ "," -- Symbol.scan_id --| $$ ","
- -- (parse_formula || skip_formula) -- parse_tstp_extra_arguments --| $$ ")"
- --| $$ "."
+ -- (parse_formula || skip_term >> K dummy_phi) -- parse_tstp_extra_arguments
+ --| $$ ")" --| $$ "."
>> (fn (((num, role), phi), deps) =>
let
val (name, rule, deps) =
--- a/src/HOL/Tools/ATP/atp_systems.ML Fri Oct 21 11:27:21 2011 +0200
+++ b/src/HOL/Tools/ATP/atp_systems.ML Fri Oct 21 16:21:12 2011 +0200
@@ -344,7 +344,8 @@
required_execs = [],
arguments = fn _ => fn _ => fn sos => fn timeout => fn _ =>
"--mode casc -t " ^ string_of_int (to_secs 1 timeout) ^
- " --proof tptp --output_axiom_names on \
+ " --proof tptp --output_axiom_names on\
+ \ --forced_options propositional_to_bdd=off\
\ --thanks \"Andrei and Krystof\" --input_file"
|> sos = sosN ? prefix "--sos on ",
proof_delims =
--- a/src/Tools/Code/code_preproc.ML Fri Oct 21 11:27:21 2011 +0200
+++ b/src/Tools/Code/code_preproc.ML Fri Oct 21 16:21:12 2011 +0200
@@ -518,8 +518,6 @@
in
Attrib.setup @{binding code_unfold} (add_del_attribute_parser add_unfold del_unfold)
"preprocessing equations for code generator"
- #> Attrib.setup @{binding code_inline} (add_del_attribute_parser add_unfold del_unfold)
- "preprocessing equations for code generator"
#> Attrib.setup @{binding code_post} (add_del_attribute_parser add_post del_post)
"postprocessing equations for code generator"
#> Attrib.setup @{binding code_unfold_post} (Scan.succeed (mk_attribute add_unfold_post))