--- a/NEWS Fri Aug 27 09:34:06 2010 +0200
+++ b/NEWS Fri Aug 27 09:43:52 2010 +0200
@@ -104,6 +104,7 @@
Trueprop ~> HOL.Trueprop
True ~> HOL.True
False ~> HOL.False
+ op --> ~> HOL.implies
Not ~> HOL.Not
The ~> HOL.The
All ~> HOL.All
--- a/doc-src/Sledgehammer/sledgehammer.tex Fri Aug 27 09:34:06 2010 +0200
+++ b/doc-src/Sledgehammer/sledgehammer.tex Fri Aug 27 09:43:52 2010 +0200
@@ -447,33 +447,29 @@
\label{relevance-filter}
\begin{enum}
-\opdefault{relevance\_threshold}{int}{40}
-Specifies the threshold above which facts are considered relevant by the
-relevance filter. The option ranges from 0 to 100, where 0 means that all
-theorems are relevant.
+\opdefault{relevance\_thresholds}{int\_pair}{45~95}
+Specifies the thresholds above which facts are considered relevant by the
+relevance filter. The first threshold is used for the first iteration of the
+relevance filter and the second threshold is used for the last iteration (if it
+is reached). The effective threshold is quadratically interpolated for the other
+iterations. Each threshold ranges from 0 to 100, where 0 means that all theorems
+are relevant and 100 only theorems that refer to previously seen constants.
-\opdefault{relevance\_convergence}{int}{31}
-Specifies the convergence factor, expressed as a percentage, used by the
-relevance filter. This factor is used by the relevance filter to scale down the
-relevance of facts at each iteration of the filter.
-
-\opdefault{max\_relevant\_per\_iter}{int\_or\_smart}{\textit{smart}}
-Specifies the maximum number of facts that may be added during one iteration of
-the relevance filter. If the option is set to \textit{smart}, it is set to a
-value that was empirically found to be appropriate for the ATP. A typical value
-would be 50.
+\opdefault{max\_relevant}{int\_or\_smart}{\textit{smart}}
+Specifies the maximum number of facts that may be returned by the relevance
+filter. If the option is set to \textit{smart}, it is set to a value that was
+empirically found to be appropriate for the ATP. A typical value would be 300.
\opsmartx{theory\_relevant}{theory\_irrelevant}
Specifies whether the theory from which a fact comes should be taken into
consideration by the relevance filter. If the option is set to \textit{smart},
-it is taken to be \textit{true} for SPASS and \textit{false} for E and Vampire,
-because empirical results suggest that these are the best settings.
+it is taken to be \textit{true} for SPASS and \textit{false} for the other ATPs;
+empirical results suggest that these are the best settings.
-\opfalse{defs\_relevant}{defs\_irrelevant}
-Specifies whether the definition of constants occurring in the formula to prove
-should be considered particularly relevant. Enabling this option tends to lead
-to larger problems and typically slows down the ATPs.
-
+%\opfalse{defs\_relevant}{defs\_irrelevant}
+%Specifies whether the definition of constants occurring in the formula to prove
+%should be considered particularly relevant. Enabling this option tends to lead
+%to larger problems and typically slows down the ATPs.
\end{enum}
\subsection{Output Format}
--- a/src/HOL/Boogie/Tools/boogie_loader.ML Fri Aug 27 09:34:06 2010 +0200
+++ b/src/HOL/Boogie/Tools/boogie_loader.ML Fri Aug 27 09:43:52 2010 +0200
@@ -504,7 +504,7 @@
in
Const (@{const_name If}, [@{typ bool}, T, T] ---> T) $ c $ t1 $ t2
end) ||
- binexp "implies" (binop @{term "op -->"}) ||
+ binexp "implies" (binop @{term HOL.implies}) ||
scan_line "distinct" num :|-- scan_count exp >>
(fn [] => @{term True}
| ts as (t :: _) => mk_distinct (Term.fastype_of t) ts) ||
--- a/src/HOL/Boogie/Tools/boogie_tactics.ML Fri Aug 27 09:34:06 2010 +0200
+++ b/src/HOL/Boogie/Tools/boogie_tactics.ML Fri Aug 27 09:43:52 2010 +0200
@@ -53,7 +53,7 @@
fun explode_conj (@{term "op &"} $ t $ u) = explode_conj t @ explode_conj u
| explode_conj t = [t]
- fun splt (ts, @{term "op -->"} $ t $ u) = splt (ts @ explode_conj t, u)
+ fun splt (ts, @{term HOL.implies} $ t $ u) = splt (ts @ explode_conj t, u)
| splt (ts, @{term "op &"} $ t $ u) = splt (ts, t) @ splt (ts, u)
| splt (ts, @{term assert_at} $ _ $ t) = [(ts, t)]
| splt (_, @{term True}) = []
--- a/src/HOL/Boogie/Tools/boogie_vcs.ML Fri Aug 27 09:34:06 2010 +0200
+++ b/src/HOL/Boogie/Tools/boogie_vcs.ML Fri Aug 27 09:43:52 2010 +0200
@@ -59,8 +59,8 @@
fun vc_of @{term True} = NONE
| vc_of (@{term assert_at} $ Free (n, _) $ t) =
SOME (Assert ((n, t), True))
- | vc_of (@{term "op -->"} $ @{term True} $ u) = vc_of u
- | vc_of (@{term "op -->"} $ t $ u) =
+ | vc_of (@{term HOL.implies} $ @{term True} $ u) = vc_of u
+ | vc_of (@{term HOL.implies} $ t $ u) =
vc_of u |> Option.map (assume t)
| vc_of (@{term "op &"} $ (@{term assert_at} $ Free (n, _) $ t) $ u) =
SOME (vc_of u |> the_default True |> assert (n, t))
@@ -76,7 +76,7 @@
let
fun mk_conj t u = @{term "op &"} $ t $ u
- fun term_of (Assume (t, v)) = @{term "op -->"} $ t $ term_of v
+ fun term_of (Assume (t, v)) = @{term HOL.implies} $ t $ term_of v
| term_of (Assert ((n, t), v)) =
mk_conj (@{term assert_at} $ Free (n, @{typ bool}) $ t) (term_of v)
| term_of (Ignore v) = term_of v
--- a/src/HOL/Decision_Procs/Approximation.thy Fri Aug 27 09:34:06 2010 +0200
+++ b/src/HOL/Decision_Procs/Approximation.thy Fri Aug 27 09:43:52 2010 +0200
@@ -3422,7 +3422,7 @@
ML {*
fun calculated_subterms (@{const Trueprop} $ t) = calculated_subterms t
- | calculated_subterms (@{const "op -->"} $ _ $ t) = calculated_subterms t
+ | calculated_subterms (@{const HOL.implies} $ _ $ t) = calculated_subterms t
| calculated_subterms (@{term "op <= :: real \<Rightarrow> real \<Rightarrow> bool"} $ t1 $ t2) = [t1, t2]
| calculated_subterms (@{term "op < :: real \<Rightarrow> real \<Rightarrow> bool"} $ t1 $ t2) = [t1, t2]
| calculated_subterms (@{term "op : :: real \<Rightarrow> real set \<Rightarrow> bool"} $ t1 $
--- a/src/HOL/Decision_Procs/Cooper.thy Fri Aug 27 09:34:06 2010 +0200
+++ b/src/HOL/Decision_Procs/Cooper.thy Fri Aug 27 09:43:52 2010 +0200
@@ -1956,7 +1956,7 @@
@{code And} (fm_of_term ps vs t1, fm_of_term ps vs t2)
| fm_of_term ps vs (@{term "op |"} $ t1 $ t2) =
@{code Or} (fm_of_term ps vs t1, fm_of_term ps vs t2)
- | fm_of_term ps vs (@{term "op -->"} $ t1 $ t2) =
+ | fm_of_term ps vs (@{term HOL.implies} $ t1 $ t2) =
@{code Imp} (fm_of_term ps vs t1, fm_of_term ps vs t2)
| fm_of_term ps vs (@{term "Not"} $ t') =
@{code NOT} (fm_of_term ps vs t')
@@ -2016,7 +2016,7 @@
fun term_bools acc t =
let
- val is_op = member (op =) [@{term "op &"}, @{term "op |"}, @{term "op -->"}, @{term "op = :: bool => _"},
+ val is_op = member (op =) [@{term "op &"}, @{term "op |"}, @{term HOL.implies}, @{term "op = :: bool => _"},
@{term "op = :: int => _"}, @{term "op < :: int => _"},
@{term "op <= :: int => _"}, @{term "Not"}, @{term "All :: (int => _) => _"},
@{term "Ex :: (int => _) => _"}, @{term "True"}, @{term "False"}]
--- a/src/HOL/Decision_Procs/Ferrack.thy Fri Aug 27 09:34:06 2010 +0200
+++ b/src/HOL/Decision_Procs/Ferrack.thy Fri Aug 27 09:43:52 2010 +0200
@@ -1998,7 +1998,7 @@
@{code Iff} (fm_of_term vs t1, fm_of_term vs t2)
| fm_of_term vs (@{term "op &"} $ t1 $ t2) = @{code And} (fm_of_term vs t1, fm_of_term vs t2)
| fm_of_term vs (@{term "op |"} $ t1 $ t2) = @{code Or} (fm_of_term vs t1, fm_of_term vs t2)
- | fm_of_term vs (@{term "op -->"} $ t1 $ t2) = @{code Imp} (fm_of_term vs t1, fm_of_term vs t2)
+ | fm_of_term vs (@{term HOL.implies} $ t1 $ t2) = @{code Imp} (fm_of_term vs t1, fm_of_term vs t2)
| fm_of_term vs (@{term "Not"} $ t') = @{code NOT} (fm_of_term vs t')
| fm_of_term vs (Const (@{const_name Ex}, _) $ Abs (xn, xT, p)) =
@{code E} (fm_of_term (("", dummyT) :: vs) p)
--- a/src/HOL/Decision_Procs/MIR.thy Fri Aug 27 09:34:06 2010 +0200
+++ b/src/HOL/Decision_Procs/MIR.thy Fri Aug 27 09:43:52 2010 +0200
@@ -5841,7 +5841,7 @@
@{code And} (fm_of_term vs t1, fm_of_term vs t2)
| fm_of_term vs (@{term "op |"} $ t1 $ t2) =
@{code Or} (fm_of_term vs t1, fm_of_term vs t2)
- | fm_of_term vs (@{term "op -->"} $ t1 $ t2) =
+ | fm_of_term vs (@{term HOL.implies} $ t1 $ t2) =
@{code Imp} (fm_of_term vs t1, fm_of_term vs t2)
| fm_of_term vs (@{term "Not"} $ t') =
@{code NOT} (fm_of_term vs t')
--- a/src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy Fri Aug 27 09:34:06 2010 +0200
+++ b/src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy Fri Aug 27 09:43:52 2010 +0200
@@ -2956,7 +2956,7 @@
val nott = @{term "Not"};
val conjt = @{term "op &"};
val disjt = @{term "op |"};
-val impt = @{term "op -->"};
+val impt = @{term HOL.implies};
val ifft = @{term "op = :: bool => _"}
fun llt rT = Const(@{const_name Orderings.less},rrT rT);
fun lle rT = Const(@{const_name Orderings.less},rrT rT);
@@ -3020,7 +3020,7 @@
| Const(@{const_name Not},_)$p => @{code NOT} (fm_of_term m m' p)
| Const(@{const_name "op &"},_)$p$q => @{code And} (fm_of_term m m' p, fm_of_term m m' q)
| Const(@{const_name "op |"},_)$p$q => @{code Or} (fm_of_term m m' p, fm_of_term m m' q)
- | Const(@{const_name "op -->"},_)$p$q => @{code Imp} (fm_of_term m m' p, fm_of_term m m' q)
+ | Const(@{const_name HOL.implies},_)$p$q => @{code Imp} (fm_of_term m m' p, fm_of_term m m' q)
| Const(@{const_name "op ="},ty)$p$q =>
if domain_type ty = bT then @{code Iff} (fm_of_term m m' p, fm_of_term m m' q)
else @{code Eq} (@{code Sub} (tm_of_term m m' p, tm_of_term m m' q))
--- a/src/HOL/Decision_Procs/ferrante_rackoff.ML Fri Aug 27 09:34:06 2010 +0200
+++ b/src/HOL/Decision_Procs/ferrante_rackoff.ML Fri Aug 27 09:43:52 2010 +0200
@@ -183,7 +183,7 @@
| Const (@{const_name Ex}, _) $ _ => find_body bounds (Thm.dest_arg tm)
| Const (@{const_name "op &"}, _) $ _ $ _ => find_args bounds tm
| Const (@{const_name "op |"}, _) $ _ $ _ => find_args bounds tm
- | Const (@{const_name "op -->"}, _) $ _ $ _ => find_args bounds tm
+ | Const (@{const_name HOL.implies}, _) $ _ $ _ => find_args bounds tm
| Const ("==>", _) $ _ $ _ => find_args bounds tm
| Const ("==", _) $ _ $ _ => find_args bounds tm
| Const ("all", _) $ _ => find_body bounds (Thm.dest_arg tm)
--- a/src/HOL/Decision_Procs/langford.ML Fri Aug 27 09:34:06 2010 +0200
+++ b/src/HOL/Decision_Procs/langford.ML Fri Aug 27 09:43:52 2010 +0200
@@ -185,7 +185,7 @@
| Const (@{const_name Ex}, _) $ _ => find_body bounds (Thm.dest_arg tm)
| Const (@{const_name "op &"}, _) $ _ $ _ => find_args bounds tm
| Const (@{const_name "op |"}, _) $ _ $ _ => find_args bounds tm
- | Const (@{const_name "op -->"}, _) $ _ $ _ => find_args bounds tm
+ | Const (@{const_name HOL.implies}, _) $ _ $ _ => find_args bounds tm
| Const ("==>", _) $ _ $ _ => find_args bounds tm
| Const ("==", _) $ _ $ _ => find_args bounds tm
| Const (@{const_name Trueprop}, _) $ _ => h bounds (Thm.dest_arg tm)
--- a/src/HOL/HOL.thy Fri Aug 27 09:34:06 2010 +0200
+++ b/src/HOL/HOL.thy Fri Aug 27 09:43:52 2010 +0200
@@ -56,13 +56,13 @@
True :: bool
False :: bool
Not :: "bool => bool" ("~ _" [40] 40)
+ implies :: "[bool, bool] => bool" (infixr "-->" 25)
setup Sign.root_path
consts
"op &" :: "[bool, bool] => bool" (infixr "&" 35)
"op |" :: "[bool, bool] => bool" (infixr "|" 30)
- "op -->" :: "[bool, bool] => bool" (infixr "-->" 25)
"op =" :: "['a, 'a] => bool" (infixl "=" 50)
@@ -91,7 +91,7 @@
Not ("\<not> _" [40] 40) and
"op &" (infixr "\<and>" 35) and
"op |" (infixr "\<or>" 30) and
- "op -->" (infixr "\<longrightarrow>" 25) and
+ HOL.implies (infixr "\<longrightarrow>" 25) and
not_equal (infix "\<noteq>" 50)
notation (HTML output)
@@ -184,7 +184,7 @@
finalconsts
"op ="
- "op -->"
+ HOL.implies
The
definition If :: "bool \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'a" ("(if (_)/ then (_)/ else (_))" [0, 0, 10] 10) where
@@ -1924,7 +1924,7 @@
(Haskell "True" and "False" and "not"
and infixl 3 "&&" and infixl 2 "||"
and "!(if (_)/ then (_)/ else (_))")
- (Scala "true" and "false" and "'!/ _"
+ (Scala "true" and "false" and "'! _"
and infixl 3 "&&" and infixl 1 "||"
and "!(if ((_))/ (_)/ else (_))")
--- a/src/HOL/Imperative_HOL/Array.thy Fri Aug 27 09:34:06 2010 +0200
+++ b/src/HOL/Imperative_HOL/Array.thy Fri Aug 27 09:43:52 2010 +0200
@@ -484,11 +484,11 @@
code_type array (Scala "!collection.mutable.ArraySeq[_]")
code_const Array (Scala "!error(\"bare Array\")")
-code_const Array.new' (Scala "('_: Unit)/ => / Array.alloc((_))((_))")
-code_const Array.make' (Scala "('_: Unit)/ =>/ Array.make((_))((_))")
-code_const Array.len' (Scala "('_: Unit)/ =>/ Array.len((_))")
-code_const Array.nth' (Scala "('_: Unit)/ =>/ Array.nth((_), (_))")
-code_const Array.upd' (Scala "('_: Unit)/ =>/ Array.upd((_), (_), (_))")
-code_const Array.freeze (Scala "('_: Unit)/ =>/ Array.freeze((_))")
+code_const Array.new' (Scala "('_: Unit)/ => / Heap.Array.alloc((_))((_))")
+code_const Array.make' (Scala "('_: Unit)/ =>/ Heap.Array.make((_))((_))")
+code_const Array.len' (Scala "('_: Unit)/ =>/ Heap.Array.len((_))")
+code_const Array.nth' (Scala "('_: Unit)/ =>/ Heap.Array.nth((_), (_))")
+code_const Array.upd' (Scala "('_: Unit)/ =>/ Heap.Array.upd((_), (_), (_))")
+code_const Array.freeze (Scala "('_: Unit)/ =>/ Heap.Array.freeze((_))")
end
--- a/src/HOL/Imperative_HOL/Heap_Monad.thy Fri Aug 27 09:34:06 2010 +0200
+++ b/src/HOL/Imperative_HOL/Heap_Monad.thy Fri Aug 27 09:43:52 2010 +0200
@@ -478,7 +478,6 @@
code_include Scala "Heap"
{*import collection.mutable.ArraySeq
-import Natural._
def bind[A, B](f: Unit => A, g: A => Unit => B): Unit => B = (_: Unit) => g (f ()) ()
@@ -487,24 +486,33 @@
}
object Ref {
- def apply[A](x: A): Ref[A] = new Ref[A](x)
- def lookup[A](r: Ref[A]): A = r.value
- def update[A](r: Ref[A], x: A): Unit = { r.value = x }
+ def apply[A](x: A): Ref[A] =
+ new Ref[A](x)
+ def lookup[A](r: Ref[A]): A =
+ r.value
+ def update[A](r: Ref[A], x: A): Unit =
+ { r.value = x }
}
object Array {
- def alloc[A](n: Natural)(x: A): ArraySeq[A] = ArraySeq.fill(n.as_Int)(x)
- def make[A](n: Natural)(f: Natural => A): ArraySeq[A] = ArraySeq.tabulate(n.as_Int)((k: Int) => f(Natural(k)))
- def len[A](a: ArraySeq[A]): Natural = Natural(a.length)
- def nth[A](a: ArraySeq[A], n: Natural): A = a(n.as_Int)
- def upd[A](a: ArraySeq[A], n: Natural, x: A): Unit = a.update(n.as_Int, x)
- def freeze[A](a: ArraySeq[A]): List[A] = a.toList
+ def alloc[A](n: Natural.Nat)(x: A): ArraySeq[A] =
+ ArraySeq.fill(n.as_Int)(x)
+ def make[A](n: Natural.Nat)(f: Natural.Nat => A): ArraySeq[A] =
+ ArraySeq.tabulate(n.as_Int)((k: Int) => f(Natural.Nat(k)))
+ def len[A](a: ArraySeq[A]): Natural.Nat =
+ Natural.Nat(a.length)
+ def nth[A](a: ArraySeq[A], n: Natural.Nat): A =
+ a(n.as_Int)
+ def upd[A](a: ArraySeq[A], n: Natural.Nat, x: A): Unit =
+ a.update(n.as_Int, x)
+ def freeze[A](a: ArraySeq[A]): List[A] =
+ a.toList
}*}
code_reserved Scala bind Ref Array
code_type Heap (Scala "Unit/ =>/ _")
-code_const bind (Scala "bind")
+code_const bind (Scala "Heap.bind")
code_const return (Scala "('_: Unit)/ =>/ _")
code_const Heap_Monad.raise' (Scala "!error((_))")
--- a/src/HOL/Imperative_HOL/Ref.thy Fri Aug 27 09:34:06 2010 +0200
+++ b/src/HOL/Imperative_HOL/Ref.thy Fri Aug 27 09:43:52 2010 +0200
@@ -306,10 +306,10 @@
text {* Scala *}
-code_type ref (Scala "!Ref[_]")
+code_type ref (Scala "!Heap.Ref[_]")
code_const Ref (Scala "!error(\"bare Ref\")")
-code_const ref' (Scala "('_: Unit)/ =>/ Ref((_))")
-code_const Ref.lookup (Scala "('_: Unit)/ =>/ Ref.lookup((_))")
-code_const Ref.update (Scala "('_: Unit)/ =>/ Ref.update((_), (_))")
+code_const ref' (Scala "('_: Unit)/ =>/ Heap.Ref((_))")
+code_const Ref.lookup (Scala "('_: Unit)/ =>/ Heap.Ref.lookup((_))")
+code_const Ref.update (Scala "('_: Unit)/ =>/ Heap.Ref.update((_), (_))")
end
--- a/src/HOL/Import/Generate-HOLLight/GenHOLLight.thy Fri Aug 27 09:34:06 2010 +0200
+++ b/src/HOL/Import/Generate-HOLLight/GenHOLLight.thy Fri Aug 27 09:43:52 2010 +0200
@@ -54,7 +54,7 @@
ONE_ONE > HOL4Setup.ONE_ONE
ONTO > Fun.surj
"=" > "op ="
- "==>" > "op -->"
+ "==>" > HOL.implies
"/\\" > "op &"
"\\/" > "op |"
"!" > All
--- a/src/HOL/Import/HOLLight/hollight.imp Fri Aug 27 09:34:06 2010 +0200
+++ b/src/HOL/Import/HOLLight/hollight.imp Fri Aug 27 09:43:52 2010 +0200
@@ -233,7 +233,7 @@
"?" > "HOL.Ex"
">=" > "HOLLight.hollight.>="
">" > "HOLLight.hollight.>"
- "==>" > "op -->"
+ "==>" > HOL.implies
"=" > "op ="
"<=" > "HOLLight.hollight.<="
"<" > "HOLLight.hollight.<"
--- a/src/HOL/Import/hol4rews.ML Fri Aug 27 09:34:06 2010 +0200
+++ b/src/HOL/Import/hol4rews.ML Fri Aug 27 09:43:52 2010 +0200
@@ -628,7 +628,7 @@
|> add_hol4_type_mapping "min" "fun" false "fun"
|> add_hol4_type_mapping "min" "ind" false @{type_name ind}
|> add_hol4_const_mapping "min" "=" false @{const_name "op ="}
- |> add_hol4_const_mapping "min" "==>" false @{const_name "op -->"}
+ |> add_hol4_const_mapping "min" "==>" false @{const_name HOL.implies}
|> add_hol4_const_mapping "min" "@" false @{const_name "Eps"}
in
val hol4_setup =
--- a/src/HOL/Import/proof_kernel.ML Fri Aug 27 09:34:06 2010 +0200
+++ b/src/HOL/Import/proof_kernel.ML Fri Aug 27 09:43:52 2010 +0200
@@ -1205,7 +1205,7 @@
fun non_trivial_term_consts t = fold_aterms
(fn Const (c, _) =>
if c = @{const_name Trueprop} orelse c = @{const_name All}
- orelse c = @{const_name "op -->"} orelse c = @{const_name "op &"} orelse c = @{const_name "op ="}
+ orelse c = @{const_name HOL.implies} orelse c = @{const_name "op &"} orelse c = @{const_name "op ="}
then I else insert (op =) c
| _ => I) t [];
@@ -1214,7 +1214,7 @@
fun add_consts (Const (c, _), cs) =
(case c of
@{const_name "op ="} => insert (op =) "==" cs
- | @{const_name "op -->"} => insert (op =) "==>" cs
+ | @{const_name HOL.implies} => insert (op =) "==>" cs
| @{const_name All} => cs
| "all" => cs
| @{const_name "op &"} => cs
@@ -1860,7 +1860,7 @@
val _ = if_debug pth hth
val th1 = implies_elim_all (beta_eta_thm th)
val a = case concl_of th1 of
- _ $ (Const(@{const_name "op -->"},_) $ a $ Const(@{const_name False},_)) => a
+ _ $ (Const(@{const_name HOL.implies},_) $ a $ Const(@{const_name False},_)) => a
| _ => raise ERR "NOT_INTRO" "Conclusion of bad form"
val ca = cterm_of thy a
val th2 = Thm.equal_elim (Drule.instantiate' [] [SOME ca] not_intro_thm) th1
--- a/src/HOL/Library/Code_Integer.thy Fri Aug 27 09:34:06 2010 +0200
+++ b/src/HOL/Library/Code_Integer.thy Fri Aug 27 09:43:52 2010 +0200
@@ -51,14 +51,14 @@
(SML "IntInf.- ((_), 1)")
(OCaml "Big'_int.pred'_big'_int")
(Haskell "!(_/ -/ 1)")
- (Scala "!(_/ -/ 1)")
+ (Scala "!(_ -/ 1)")
(Eval "!(_/ -/ 1)")
code_const Int.succ
(SML "IntInf.+ ((_), 1)")
(OCaml "Big'_int.succ'_big'_int")
(Haskell "!(_/ +/ 1)")
- (Scala "!(_/ +/ 1)")
+ (Scala "!(_ +/ 1)")
(Eval "!(_/ +/ 1)")
code_const "op + \<Colon> int \<Rightarrow> int \<Rightarrow> int"
--- a/src/HOL/Library/Code_Natural.thy Fri Aug 27 09:34:06 2010 +0200
+++ b/src/HOL/Library/Code_Natural.thy Fri Aug 27 09:43:52 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);
@@ -54,48 +52,48 @@
code_reserved Haskell Natural
-code_include Scala "Natural" {*
-import scala.Math
+code_include Scala "Natural"
+{*import scala.Math
-object Natural {
+object Nat {
- def apply(numeral: BigInt): Natural = new Natural(numeral max 0)
- def apply(numeral: Int): Natural = Natural(BigInt(numeral))
- def apply(numeral: String): Natural = Natural(BigInt(numeral))
+ def apply(numeral: BigInt): Nat = new Nat(numeral max 0)
+ def apply(numeral: Int): Nat = Nat(BigInt(numeral))
+ def apply(numeral: String): Nat = Nat(BigInt(numeral))
}
-class Natural private(private val value: BigInt) {
+class Nat private(private val value: BigInt) {
override def hashCode(): Int = this.value.hashCode()
override def equals(that: Any): Boolean = that match {
- case that: Natural => this equals that
+ case that: Nat => this equals that
case _ => false
}
override def toString(): String = this.value.toString
- def equals(that: Natural): Boolean = this.value == that.value
+ def equals(that: Nat): Boolean = this.value == that.value
def as_BigInt: BigInt = this.value
def as_Int: Int = if (this.value >= Int.MinValue && this.value <= Int.MaxValue)
this.value.intValue
else error("Int value out of range: " + this.value.toString)
- def +(that: Natural): Natural = new Natural(this.value + that.value)
- def -(that: Natural): Natural = Natural(this.value - that.value)
- def *(that: Natural): Natural = new Natural(this.value * that.value)
+ def +(that: Nat): Nat = new Nat(this.value + that.value)
+ def -(that: Nat): Nat = Nat(this.value - that.value)
+ def *(that: Nat): Nat = new Nat(this.value * that.value)
- def /%(that: Natural): (Natural, Natural) = if (that.value == 0) (new Natural(0), this)
+ def /%(that: Nat): (Nat, Nat) = if (that.value == 0) (new Nat(0), this)
else {
val (k, l) = this.value /% that.value
- (new Natural(k), new Natural(l))
+ (new Nat(k), new Nat(l))
}
- def <=(that: Natural): Boolean = this.value <= that.value
+ def <=(that: Nat): Boolean = this.value <= that.value
- def <(that: Natural): Boolean = this.value < that.value
+ def <(that: Nat): Boolean = this.value < that.value
}
*}
@@ -104,7 +102,7 @@
code_type code_numeral
(Haskell "Natural.Natural")
- (Scala "Natural")
+ (Scala "Natural.Nat")
setup {*
fold (Numeral.add_code @{const_name number_code_numeral_inst.number_of_code_numeral}
--- a/src/HOL/Library/Efficient_Nat.thy Fri Aug 27 09:34:06 2010 +0200
+++ b/src/HOL/Library/Efficient_Nat.thy Fri Aug 27 09:43:52 2010 +0200
@@ -242,8 +242,8 @@
and @{typ int}.
*}
-code_include Haskell "Nat" {*
-newtype Nat = Nat Integer deriving (Eq, Show, Read);
+code_include Haskell "Nat"
+{*newtype Nat = Nat Integer deriving (Eq, Show, Read);
instance Num Nat where {
fromInteger k = Nat (if k >= 0 then k else 0);
@@ -280,8 +280,8 @@
code_reserved Haskell Nat
-code_include Scala "Nat" {*
-import scala.Math
+code_include Scala "Nat"
+{*import scala.Math
object Nat {
@@ -330,7 +330,7 @@
code_type nat
(Haskell "Nat.Nat")
- (Scala "Nat")
+ (Scala "Nat.Nat")
code_instance nat :: eq
(Haskell -)
@@ -397,7 +397,7 @@
code_const int and nat
(Haskell "toInteger" and "fromInteger")
- (Scala "!_.as'_BigInt" and "Nat")
+ (Scala "!_.as'_BigInt" and "Nat.Nat")
text {* Conversion from and to code numerals. *}
@@ -405,14 +405,14 @@
(SML "IntInf.toInt")
(OCaml "_")
(Haskell "!(fromInteger/ ./ toInteger)")
- (Scala "!Natural(_.as'_BigInt)")
+ (Scala "!Natural.Nat(_.as'_BigInt)")
(Eval "_")
code_const Code_Numeral.nat_of
(SML "IntInf.fromInt")
(OCaml "_")
(Haskell "!(fromInteger/ ./ toInteger)")
- (Scala "!Nat(_.as'_BigInt)")
+ (Scala "!Nat.Nat(_.as'_BigInt)")
(Eval "_")
text {* Using target language arithmetic operations whenever appropriate *}
--- a/src/HOL/Library/Sum_Of_Squares/sum_of_squares.ML Fri Aug 27 09:34:06 2010 +0200
+++ b/src/HOL/Library/Sum_Of_Squares/sum_of_squares.ML Fri Aug 27 09:43:52 2010 +0200
@@ -1356,7 +1356,7 @@
val known_sos_constants =
[@{term "op ==>"}, @{term "Trueprop"},
- @{term "op -->"}, @{term "op &"}, @{term "op |"},
+ @{term HOL.implies}, @{term "op &"}, @{term "op |"},
@{term "Not"}, @{term "op = :: bool => _"},
@{term "All :: (real => _) => _"}, @{term "Ex :: (real => _) => _"},
@{term "op = :: real => _"}, @{term "op < :: real => _"},
--- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Fri Aug 27 09:34:06 2010 +0200
+++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Fri Aug 27 09:43:52 2010 +0200
@@ -290,10 +290,12 @@
| NONE => get_prover (default_atp_name ()))
end
+type locality = Sledgehammer_Fact_Filter.locality
+
local
datatype sh_result =
- SH_OK of int * int * (string * bool) list |
+ SH_OK of int * int * (string * locality) list |
SH_FAIL of int * int |
SH_ERROR
@@ -355,8 +357,8 @@
case result of
SH_OK (time_isa, time_atp, names) =>
let
- fun get_thms (name, chained) =
- ((name, chained), thms_of_name (Proof.context_of st) name)
+ fun get_thms (name, loc) =
+ ((name, loc), thms_of_name (Proof.context_of st) name)
in
change_data id inc_sh_success;
change_data id (inc_sh_lemmas (length names));
@@ -445,7 +447,7 @@
then () else
let
val named_thms =
- Unsynchronized.ref (NONE : ((string * bool) * thm list) list option)
+ Unsynchronized.ref (NONE : ((string * locality) * thm list) list option)
val minimize = AList.defined (op =) args minimizeK
val metis_ft = AList.defined (op =) args metis_ftK
--- a/src/HOL/Orderings.thy Fri Aug 27 09:34:06 2010 +0200
+++ b/src/HOL/Orderings.thy Fri Aug 27 09:43:52 2010 +0200
@@ -640,7 +640,7 @@
let
val All_binder = Syntax.binder_name @{const_syntax All};
val Ex_binder = Syntax.binder_name @{const_syntax Ex};
- val impl = @{const_syntax "op -->"};
+ val impl = @{const_syntax HOL.implies};
val conj = @{const_syntax "op &"};
val less = @{const_syntax less};
val less_eq = @{const_syntax less_eq};
--- a/src/HOL/Prolog/prolog.ML Fri Aug 27 09:34:06 2010 +0200
+++ b/src/HOL/Prolog/prolog.ML Fri Aug 27 09:43:52 2010 +0200
@@ -12,7 +12,7 @@
fun isD t = case t of
Const(@{const_name Trueprop},_)$t => isD t
| Const(@{const_name "op &"} ,_)$l$r => isD l andalso isD r
- | Const(@{const_name "op -->"},_)$l$r => isG l andalso isD r
+ | Const(@{const_name HOL.implies},_)$l$r => isG l andalso isD r
| Const( "==>",_)$l$r => isG l andalso isD r
| Const(@{const_name All},_)$Abs(s,_,t) => isD t
| Const("all",_)$Abs(s,_,t) => isD t
@@ -32,7 +32,7 @@
Const(@{const_name Trueprop},_)$t => isG t
| Const(@{const_name "op &"} ,_)$l$r => isG l andalso isG r
| Const(@{const_name "op |"} ,_)$l$r => isG l andalso isG r
- | Const(@{const_name "op -->"},_)$l$r => isD l andalso isG r
+ | Const(@{const_name HOL.implies},_)$l$r => isD l andalso isG r
| Const( "==>",_)$l$r => isD l andalso isG r
| Const(@{const_name All},_)$Abs(_,_,t) => isG t
| Const("all",_)$Abs(_,_,t) => isG t
@@ -54,7 +54,7 @@
_$(Const(@{const_name All} ,_)$Abs(s,_,_))=> at(thm RS
(read_instantiate ctxt [(("x", 0), "?" ^ (if s="P" then "PP" else s))] spec))
| _$(Const(@{const_name "op &"},_)$_$_) => at(thm RS conjunct1)@at(thm RS conjunct2)
- | _$(Const(@{const_name "op -->"},_)$_$_) => at(thm RS mp)
+ | _$(Const(@{const_name HOL.implies},_)$_$_) => at(thm RS mp)
| _ => [thm]
in map zero_var_indexes (at thm) end;
@@ -72,7 +72,7 @@
-- is nice, but cannot instantiate unknowns in the assumptions *)
fun hyp_resolve_tac i st = let
fun ap (Const(@{const_name All},_)$Abs(_,_,t))=(case ap t of (k,a,t) => (k+1,a ,t))
- | ap (Const(@{const_name "op -->"},_)$_$t) =(case ap t of (k,_,t) => (k,true ,t))
+ | ap (Const(@{const_name HOL.implies},_)$_$t) =(case ap t of (k,_,t) => (k,true ,t))
| ap t = (0,false,t);
(*
fun rep_goal (Const ("all",_)$Abs (_,_,t)) = rep_goal t
--- a/src/HOL/Set.thy Fri Aug 27 09:34:06 2010 +0200
+++ b/src/HOL/Set.thy Fri Aug 27 09:43:52 2010 +0200
@@ -219,7 +219,7 @@
val Type (set_type, _) = @{typ "'a set"}; (* FIXME 'a => bool (!?!) *)
val All_binder = Syntax.binder_name @{const_syntax All};
val Ex_binder = Syntax.binder_name @{const_syntax Ex};
- val impl = @{const_syntax "op -->"};
+ val impl = @{const_syntax HOL.implies};
val conj = @{const_syntax "op &"};
val sbset = @{const_syntax subset};
val sbset_eq = @{const_syntax subset_eq};
--- a/src/HOL/TLA/Intensional.thy Fri Aug 27 09:34:06 2010 +0200
+++ b/src/HOL/TLA/Intensional.thy Fri Aug 27 09:43:52 2010 +0200
@@ -279,7 +279,7 @@
fun hflatten t =
case (concl_of t) of
- Const _ $ (Const (@{const_name "op -->"}, _) $ _ $ _) => hflatten (t RS mp)
+ Const _ $ (Const (@{const_name HOL.implies}, _) $ _ $ _) => hflatten (t RS mp)
| _ => (hflatten (matchsome conjI t)) handle THM _ => zero_var_indexes t
in
hflatten t
--- a/src/HOL/Tools/ATP/atp_systems.ML Fri Aug 27 09:34:06 2010 +0200
+++ b/src/HOL/Tools/ATP/atp_systems.ML Fri Aug 27 09:43:52 2010 +0200
@@ -19,7 +19,7 @@
has_incomplete_mode: bool,
proof_delims: (string * string) list,
known_failures: (failure * string) list,
- default_max_relevant_per_iter: int,
+ default_max_relevant: int,
default_theory_relevant: bool,
explicit_forall: bool,
use_conjecture_for_hypotheses: bool}
@@ -52,7 +52,7 @@
has_incomplete_mode: bool,
proof_delims: (string * string) list,
known_failures: (failure * string) list,
- default_max_relevant_per_iter: int,
+ default_max_relevant: int,
default_theory_relevant: bool,
explicit_forall: bool,
use_conjecture_for_hypotheses: bool}
@@ -125,10 +125,20 @@
priority ("Available ATPs: " ^
commas (sort_strings (Symtab.keys (Data.get thy))) ^ ".")
-fun to_generous_secs time = (Time.toMilliseconds time + 999) div 1000
+fun to_secs bonus time = (Time.toMilliseconds time + bonus + 999) div 1000
(* E prover *)
+(* Give older versions of E an extra second, because the "eproof" script wrongly
+ subtracted an entire second to account for the overhead of the script
+ itself, which is in fact much lower. *)
+fun e_bonus () =
+ case getenv "E_VERSION" of
+ "" => 1000
+ | version =>
+ if exists (fn s => String.isPrefix s version) ["0.9", "1.0"] then 1000
+ else 0
+
val tstp_proof_delims =
("# SZS output start CNFRefutation.", "# SZS output end CNFRefutation")
@@ -137,8 +147,7 @@
required_execs = [],
arguments = fn _ => fn timeout =>
"--tstp-in --tstp-out -l5 -xAutoDev -tAutoDev --silent \
- \--soft-cpu-limit=" ^
- string_of_int (to_generous_secs timeout),
+ \--cpu-limit=" ^ string_of_int (to_secs (e_bonus ()) timeout),
has_incomplete_mode = false,
proof_delims = [tstp_proof_delims],
known_failures =
@@ -150,7 +159,7 @@
"# Cannot determine problem status within resource limit"),
(OutOfResources, "SZS status: ResourceOut"),
(OutOfResources, "SZS status ResourceOut")],
- default_max_relevant_per_iter = 80 (* FUDGE *),
+ default_max_relevant = 500 (* FUDGE *),
default_theory_relevant = false,
explicit_forall = false,
use_conjecture_for_hypotheses = true}
@@ -165,7 +174,7 @@
required_execs = [("SPASS_HOME", "SPASS")],
arguments = fn complete => fn timeout =>
("-Auto -PGiven=0 -PProblem=0 -Splits=0 -FullRed=0 -DocProof \
- \-VarWeight=3 -TimeLimit=" ^ string_of_int (to_generous_secs timeout))
+ \-VarWeight=3 -TimeLimit=" ^ string_of_int (to_secs 0 timeout))
|> not complete ? prefix "-SOS=1 ",
has_incomplete_mode = true,
proof_delims = [("Here is a proof", "Formulae used in the proof")],
@@ -177,7 +186,7 @@
(MalformedInput, "Undefined symbol"),
(MalformedInput, "Free Variable"),
(SpassTooOld, "tptp2dfg")],
- default_max_relevant_per_iter = 40 (* FUDGE *),
+ default_max_relevant = 350 (* FUDGE *),
default_theory_relevant = true,
explicit_forall = true,
use_conjecture_for_hypotheses = true}
@@ -190,10 +199,11 @@
val vampire_config : prover_config =
{exec = ("VAMPIRE_HOME", "vampire"),
required_execs = [],
- arguments = fn _ => fn timeout =>
- "--mode casc -t " ^ string_of_int (to_generous_secs timeout) ^
- " --thanks Andrei --input_file",
- has_incomplete_mode = false,
+ arguments = fn complete => fn timeout =>
+ ("--mode casc -t " ^ string_of_int (to_secs 0 timeout) ^
+ " --thanks Andrei --input_file")
+ |> not complete ? prefix "--sos on ",
+ has_incomplete_mode = true,
proof_delims =
[("=========== Refutation ==========",
"======= End of refutation ======="),
@@ -206,7 +216,7 @@
(Unprovable, "Satisfiability detected"),
(Unprovable, "Termination reason: Satisfiable"),
(VampireTooOld, "not a valid option")],
- default_max_relevant_per_iter = 45 (* FUDGE *),
+ default_max_relevant = 400 (* FUDGE *),
default_theory_relevant = false,
explicit_forall = false,
use_conjecture_for_hypotheses = true}
@@ -246,38 +256,38 @@
| SOME sys => sys
fun remote_config system_name system_versions proof_delims known_failures
- default_max_relevant_per_iter default_theory_relevant
- use_conjecture_for_hypotheses =
+ default_max_relevant default_theory_relevant
+ use_conjecture_for_hypotheses : prover_config =
{exec = ("ISABELLE_ATP", "scripts/remote_atp"),
required_execs = [],
arguments = fn _ => fn timeout =>
- " -t " ^ string_of_int (to_generous_secs timeout) ^ " -s " ^
+ " -t " ^ string_of_int (to_secs 0 timeout) ^ " -s " ^
the_system system_name system_versions,
has_incomplete_mode = false,
proof_delims = insert (op =) tstp_proof_delims proof_delims,
known_failures =
known_failures @ known_perl_failures @
[(TimedOut, "says Timeout")],
- default_max_relevant_per_iter = default_max_relevant_per_iter,
+ default_max_relevant = default_max_relevant,
default_theory_relevant = default_theory_relevant,
explicit_forall = true,
use_conjecture_for_hypotheses = use_conjecture_for_hypotheses}
fun remotify_config system_name system_versions
- ({proof_delims, known_failures, default_max_relevant_per_iter,
+ ({proof_delims, known_failures, default_max_relevant,
default_theory_relevant, use_conjecture_for_hypotheses, ...}
: prover_config) : prover_config =
remote_config system_name system_versions proof_delims known_failures
- default_max_relevant_per_iter default_theory_relevant
+ default_max_relevant default_theory_relevant
use_conjecture_for_hypotheses
val remotify_name = prefix "remote_"
fun remote_prover name system_name system_versions proof_delims known_failures
- default_max_relevant_per_iter default_theory_relevant
+ default_max_relevant default_theory_relevant
use_conjecture_for_hypotheses =
(remotify_name name,
remote_config system_name system_versions proof_delims known_failures
- default_max_relevant_per_iter default_theory_relevant
+ default_max_relevant default_theory_relevant
use_conjecture_for_hypotheses)
fun remotify_prover (name, config) system_name system_versions =
(remotify_name name, remotify_config system_name system_versions config)
@@ -285,11 +295,11 @@
val remote_e = remotify_prover e "EP" ["1.0", "1.1", "1.2"]
val remote_vampire = remotify_prover vampire "Vampire" ["9.9", "0.6", "1.0"]
val remote_sine_e =
- remote_prover "sine_e" "SInE" [] []
- [(Unprovable, "says Unknown")] 150 (* FUDGE *) false true
+ remote_prover "sine_e" "SInE" [] [] [(Unprovable, "says Unknown")]
+ 1000 (* FUDGE *) false true
val remote_snark =
remote_prover "snark" "SNARK---" [] [("refutation.", "end_refutation.")] []
- 50 (* FUDGE *) false true
+ 350 (* FUDGE *) false true
(* Setup *)
--- a/src/HOL/Tools/Nitpick/minipick.ML Fri Aug 27 09:34:06 2010 +0200
+++ b/src/HOL/Tools/Nitpick/minipick.ML Fri Aug 27 09:43:52 2010 +0200
@@ -132,7 +132,7 @@
Subset (to_R_rep Ts t1, to_R_rep Ts t2)
| @{const "op &"} $ t1 $ t2 => And (to_F Ts t1, to_F Ts t2)
| @{const "op |"} $ t1 $ t2 => Or (to_F Ts t1, to_F Ts t2)
- | @{const "op -->"} $ t1 $ t2 => Implies (to_F Ts t1, to_F Ts t2)
+ | @{const HOL.implies} $ t1 $ t2 => Implies (to_F Ts t1, to_F Ts t2)
| t1 $ t2 => Subset (to_S_rep Ts t2, to_R_rep Ts t1)
| Free _ => raise SAME ()
| Term.Var _ => raise SAME ()
@@ -177,8 +177,8 @@
| @{const "op &"} => to_R_rep Ts (eta_expand Ts t 2)
| @{const "op |"} $ _ => to_R_rep Ts (eta_expand Ts t 1)
| @{const "op |"} => to_R_rep Ts (eta_expand Ts t 2)
- | @{const "op -->"} $ _ => to_R_rep Ts (eta_expand Ts t 1)
- | @{const "op -->"} => to_R_rep Ts (eta_expand Ts t 2)
+ | @{const HOL.implies} $ _ => to_R_rep Ts (eta_expand Ts t 1)
+ | @{const HOL.implies} => to_R_rep Ts (eta_expand Ts t 2)
| Const (@{const_name bot_class.bot},
T as Type (@{type_name fun}, [_, @{typ bool}])) =>
empty_n_ary_rel (arity_of RRep card T)
--- a/src/HOL/Tools/Nitpick/nitpick_hol.ML Fri Aug 27 09:34:06 2010 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML Fri Aug 27 09:43:52 2010 +0200
@@ -411,7 +411,7 @@
(@{const_name "op ="}, 1),
(@{const_name "op &"}, 2),
(@{const_name "op |"}, 2),
- (@{const_name "op -->"}, 2),
+ (@{const_name HOL.implies}, 2),
(@{const_name If}, 3),
(@{const_name Let}, 2),
(@{const_name Pair}, 2),
@@ -1454,7 +1454,7 @@
| @{const Trueprop} $ t1 => lhs_of_equation t1
| Const (@{const_name All}, _) $ Abs (_, _, t1) => lhs_of_equation t1
| Const (@{const_name "op ="}, _) $ t1 $ _ => SOME t1
- | @{const "op -->"} $ _ $ t2 => lhs_of_equation t2
+ | @{const HOL.implies} $ _ $ t2 => lhs_of_equation t2
| _ => NONE
fun is_constr_pattern _ (Bound _) = true
| is_constr_pattern _ (Var _) = true
--- a/src/HOL/Tools/Nitpick/nitpick_mono.ML Fri Aug 27 09:34:06 2010 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_mono.ML Fri Aug 27 09:43:52 2010 +0200
@@ -774,7 +774,7 @@
(MAbs (s, T, M, S Minus, m'), accum |>> pop_bound)
end))
| (t0 as Const (@{const_name All}, _))
- $ Abs (s', T', (t10 as @{const "op -->"}) $ (t11 $ Bound 0) $ t12) =>
+ $ Abs (s', T', (t10 as @{const HOL.implies}) $ (t11 $ Bound 0) $ t12) =>
do_bounded_quantifier t0 s' T' t10 t11 t12 accum
| (t0 as Const (@{const_name Ex}, _))
$ Abs (s', T', (t10 as @{const "op &"}) $ (t11 $ Bound 0) $ t12) =>
@@ -885,10 +885,10 @@
s0 = @{const_name Pure.conjunction} orelse
s0 = @{const_name "op &"} orelse
s0 = @{const_name "op |"} orelse
- s0 = @{const_name "op -->"} then
+ s0 = @{const_name HOL.implies} then
let
val impl = (s0 = @{const_name "==>"} orelse
- s0 = @{const_name "op -->"})
+ s0 = @{const_name HOL.implies})
val (m1, accum) = do_formula (sn |> impl ? negate) t1 accum
val (m2, accum) = do_formula sn t2 accum
in
@@ -976,7 +976,7 @@
| Const (x as (@{const_name "op ="}, _)) $ t1 $ t2 =>
consider_general_equals mdata true x t1 t2 accum
| (t0 as @{const "op &"}) $ t1 $ t2 => do_conjunction t0 t1 t2 accum
- | (t0 as @{const "op -->"}) $ t1 $ t2 => do_implies t0 t1 t2 accum
+ | (t0 as @{const HOL.implies}) $ t1 $ t2 => do_implies t0 t1 t2 accum
| _ => raise TERM ("Nitpick_Mono.consider_definitional_axiom.\
\do_formula", [t])
in do_formula t end
--- a/src/HOL/Tools/Nitpick/nitpick_nut.ML Fri Aug 27 09:34:06 2010 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_nut.ML Fri Aug 27 09:43:52 2010 +0200
@@ -522,7 +522,7 @@
Op2 (And, bool_T, Any, sub' t1, sub' t2)
| (Const (@{const_name "op |"}, _), [t1, t2]) =>
Op2 (Or, bool_T, Any, sub t1, sub t2)
- | (Const (@{const_name "op -->"}, _), [t1, t2]) =>
+ | (Const (@{const_name HOL.implies}, _), [t1, t2]) =>
Op2 (Or, bool_T, Any, Op1 (Not, bool_T, Any, sub t1), sub' t2)
| (Const (@{const_name If}, T), [t1, t2, t3]) =>
Op3 (If, nth_range_type 3 T, Any, sub t1, sub t2, sub t3)
--- a/src/HOL/Tools/Nitpick/nitpick_preproc.ML Fri Aug 27 09:34:06 2010 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_preproc.ML Fri Aug 27 09:43:52 2010 +0200
@@ -43,7 +43,7 @@
| aux def (@{const "==>"} $ t1 $ t2) = aux false t1 andalso aux def t2
| aux def (Const (@{const_name "op ="}, _) $ t1 $ t2) =
aux def t1 andalso aux false t2
- | aux def (@{const "op -->"} $ t1 $ t2) = aux false t1 andalso aux def t2
+ | aux def (@{const HOL.implies} $ t1 $ t2) = aux false t1 andalso aux def t2
| aux def (t1 $ t2) = aux def t1 andalso aux def t2
| aux def (t as Const (s, _)) =
(not def orelse t <> @{const Suc}) andalso
@@ -217,8 +217,8 @@
| @{const "op |"} $ t1 $ t2 =>
@{const "op |"} $ do_term new_Ts old_Ts polar t1
$ do_term new_Ts old_Ts polar t2
- | @{const "op -->"} $ t1 $ t2 =>
- @{const "op -->"} $ do_term new_Ts old_Ts (flip_polarity polar) t1
+ | @{const HOL.implies} $ t1 $ t2 =>
+ @{const HOL.implies} $ do_term new_Ts old_Ts (flip_polarity polar) t1
$ do_term new_Ts old_Ts polar t2
| Const (x as (s, T)) =>
if is_descr s then
@@ -334,7 +334,7 @@
if def then (t, []) else do_eq_or_imp Ts false def t0 t1 t2 seen
| (t0 as Const (@{const_name "op ="}, _)) $ t1 $ t2 =>
do_eq_or_imp Ts true def t0 t1 t2 seen
- | (t0 as @{const "op -->"}) $ t1 $ t2 =>
+ | (t0 as @{const HOL.implies}) $ t1 $ t2 =>
do_eq_or_imp Ts false def t0 t1 t2 seen
| Abs (s, T, t') =>
let val (t', seen) = do_term (T :: Ts) def t' [] seen in
@@ -401,7 +401,7 @@
t0 $ aux false t1 $ aux careful t2
| aux careful ((t0 as Const (@{const_name "op ="}, _)) $ t1 $ t2) =
aux_eq careful true t0 t1 t2
- | aux careful ((t0 as @{const "op -->"}) $ t1 $ t2) =
+ | aux careful ((t0 as @{const HOL.implies}) $ t1 $ t2) =
t0 $ aux false t1 $ aux careful t2
| aux careful (Abs (s, T, t')) = Abs (s, T, aux careful t')
| aux careful (t1 $ t2) = aux careful t1 $ aux careful t2
@@ -608,8 +608,8 @@
s_conj (pairself (aux ss Ts js skolemizable polar) (t1, t2))
| @{const "op |"} $ t1 $ t2 =>
s_disj (pairself (aux ss Ts js skolemizable polar) (t1, t2))
- | @{const "op -->"} $ t1 $ t2 =>
- @{const "op -->"} $ aux ss Ts js skolemizable (flip_polarity polar) t1
+ | @{const HOL.implies} $ t1 $ t2 =>
+ @{const HOL.implies} $ aux ss Ts js skolemizable (flip_polarity polar) t1
$ aux ss Ts js skolemizable polar t2
| (t0 as Const (@{const_name Let}, _)) $ t1 $ t2 =>
t0 $ t1 $ aux ss Ts js skolemizable polar t2
@@ -1121,7 +1121,7 @@
(t10 as @{const "op |"}) $ t11 $ t12 =>
t10 $ distribute_quantifiers (t0 $ Abs (s, T1, t11))
$ distribute_quantifiers (t0 $ Abs (s, T1, t12))
- | (t10 as @{const "op -->"}) $ t11 $ t12 =>
+ | (t10 as @{const HOL.implies}) $ t11 $ t12 =>
t10 $ distribute_quantifiers (Const (@{const_name All}, T0)
$ Abs (s, T1, t11))
$ distribute_quantifiers (t0 $ Abs (s, T1, t12))
--- a/src/HOL/Tools/Predicate_Compile/code_prolog.ML Fri Aug 27 09:34:06 2010 +0200
+++ b/src/HOL/Tools/Predicate_Compile/code_prolog.ML Fri Aug 27 09:43:52 2010 +0200
@@ -664,10 +664,10 @@
(* FIXME: large copy of Predicate_Compile_Quickcheck - refactor out commons *)
-fun strip_imp_prems (Const(@{const_name "op -->"}, _) $ A $ B) = A :: strip_imp_prems B
+fun strip_imp_prems (Const(@{const_name HOL.implies}, _) $ A $ B) = A :: strip_imp_prems B
| strip_imp_prems _ = [];
-fun strip_imp_concl (Const(@{const_name "op -->"}, _) $ A $ B) = strip_imp_concl B
+fun strip_imp_concl (Const(@{const_name HOL.implies}, _) $ A $ B) = strip_imp_concl B
| strip_imp_concl A = A : term;
fun strip_horn A = (strip_imp_prems A, strip_imp_concl A);
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_data.ML Fri Aug 27 09:34:06 2010 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_data.ML Fri Aug 27 09:43:52 2010 +0200
@@ -218,7 +218,7 @@
@{const_name Trueprop},
@{const_name Not},
@{const_name "op ="},
- @{const_name "op -->"},
+ @{const_name HOL.implies},
@{const_name All},
@{const_name Ex},
@{const_name "op &"},
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_quickcheck.ML Fri Aug 27 09:34:06 2010 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_quickcheck.ML Fri Aug 27 09:43:52 2010 +0200
@@ -168,10 +168,10 @@
mk_split_lambda' xs t
end;
-fun strip_imp_prems (Const(@{const_name "op -->"}, _) $ A $ B) = A :: strip_imp_prems B
+fun strip_imp_prems (Const(@{const_name HOL.implies}, _) $ A $ B) = A :: strip_imp_prems B
| strip_imp_prems _ = [];
-fun strip_imp_concl (Const(@{const_name "op -->"}, _) $ A $ B) = strip_imp_concl B
+fun strip_imp_concl (Const(@{const_name HOL.implies}, _) $ A $ B) = strip_imp_concl B
| strip_imp_concl A = A : term;
fun strip_horn A = (strip_imp_prems A, strip_imp_concl A);
--- a/src/HOL/Tools/Qelim/cooper.ML Fri Aug 27 09:34:06 2010 +0200
+++ b/src/HOL/Tools/Qelim/cooper.ML Fri Aug 27 09:43:52 2010 +0200
@@ -28,7 +28,7 @@
@{term "op * :: int => _"}, @{term "op * :: nat => _"},
@{term "op div :: int => _"}, @{term "op div :: nat => _"},
@{term "op mod :: int => _"}, @{term "op mod :: nat => _"},
- @{term "op &"}, @{term "op |"}, @{term "op -->"},
+ @{term "op &"}, @{term "op |"}, @{term HOL.implies},
@{term "op = :: int => _"}, @{term "op = :: nat => _"}, @{term "op = :: bool => _"},
@{term "op < :: int => _"}, @{term "op < :: nat => _"},
@{term "op <= :: int => _"}, @{term "op <= :: nat => _"},
@@ -569,7 +569,7 @@
fun add_bools t =
let
val ops = [@{term "op = :: int => _"}, @{term "op < :: int => _"}, @{term "op <= :: int => _"},
- @{term "op &"}, @{term "op |"}, @{term "op -->"}, @{term "op = :: bool => _"},
+ @{term "op &"}, @{term "op |"}, @{term HOL.implies}, @{term "op = :: bool => _"},
@{term "Not"}, @{term "All :: (int => _) => _"},
@{term "Ex :: (int => _) => _"}, @{term "True"}, @{term "False"}];
val is_op = member (op =) ops;
@@ -616,7 +616,7 @@
Proc.And (fm_of_term ps vs t1, fm_of_term ps vs t2)
| fm_of_term ps vs (Const (@{const_name "op |"}, _) $ t1 $ t2) =
Proc.Or (fm_of_term ps vs t1, fm_of_term ps vs t2)
- | fm_of_term ps vs (Const (@{const_name "op -->"}, _) $ t1 $ t2) =
+ | fm_of_term ps vs (Const (@{const_name HOL.implies}, _) $ t1 $ t2) =
Proc.Imp (fm_of_term ps vs t1, fm_of_term ps vs t2)
| fm_of_term ps vs (@{term "op = :: bool => _ "} $ t1 $ t2) =
Proc.Iff (fm_of_term ps vs t1, fm_of_term ps vs t2)
@@ -687,7 +687,7 @@
fun strip_objimp ct =
(case Thm.term_of ct of
- Const (@{const_name "op -->"}, _) $ _ $ _ =>
+ Const (@{const_name HOL.implies}, _) $ _ $ _ =>
let val (A, B) = Thm.dest_binop ct
in A :: strip_objimp B end
| _ => [ct]);
@@ -712,7 +712,7 @@
val qs = filter P ps
val q = if P c then c else @{cterm "False"}
val ng = fold_rev (fn (a,v) => fn t => Thm.capply a (Thm.cabs v t)) qvs
- (fold_rev (fn p => fn q => Thm.capply (Thm.capply @{cterm "op -->"} p) q) qs q)
+ (fold_rev (fn p => fn q => Thm.capply (Thm.capply @{cterm HOL.implies} p) q) qs q)
val g = Thm.capply (Thm.capply @{cterm "op ==>"} (Thm.capply @{cterm "Trueprop"} ng)) p'
val ntac = (case qs of [] => q aconvc @{cterm "False"}
| _ => false)
--- a/src/HOL/Tools/Qelim/qelim.ML Fri Aug 27 09:34:06 2010 +0200
+++ b/src/HOL/Tools/Qelim/qelim.ML Fri Aug 27 09:43:52 2010 +0200
@@ -26,7 +26,7 @@
Const(s,T)$_$_ =>
if domain_type T = HOLogic.boolT
andalso member (op =) [@{const_name "op &"}, @{const_name "op |"},
- @{const_name "op -->"}, @{const_name "op ="}] s
+ @{const_name HOL.implies}, @{const_name "op ="}] s
then binop_conv (conv env) p
else atcv env p
| Const(@{const_name Not},_)$_ => arg_conv (conv env) p
--- a/src/HOL/Tools/SMT/smtlib_interface.ML Fri Aug 27 09:34:06 2010 +0200
+++ b/src/HOL/Tools/SMT/smtlib_interface.ML Fri Aug 27 09:43:52 2010 +0200
@@ -161,7 +161,7 @@
| conn @{const_name Not} = SOME "not"
| conn @{const_name "op &"} = SOME "and"
| conn @{const_name "op |"} = SOME "or"
- | conn @{const_name "op -->"} = SOME "implies"
+ | conn @{const_name HOL.implies} = SOME "implies"
| conn @{const_name "op ="} = SOME "iff"
| conn @{const_name If} = SOME "if_then_else"
| conn _ = NONE
--- a/src/HOL/Tools/SMT/z3_interface.ML Fri Aug 27 09:34:06 2010 +0200
+++ b/src/HOL/Tools/SMT/z3_interface.ML Fri Aug 27 09:43:52 2010 +0200
@@ -170,7 +170,7 @@
val mk_true = @{cterm "~False"}
val mk_false = @{cterm False}
val mk_not = Thm.capply @{cterm Not}
-val mk_implies = Thm.mk_binop @{cterm "op -->"}
+val mk_implies = Thm.mk_binop @{cterm HOL.implies}
val mk_iff = Thm.mk_binop @{cterm "op = :: bool => _"}
fun mk_nary _ cu [] = cu
--- a/src/HOL/Tools/SMT/z3_proof_tools.ML Fri Aug 27 09:34:06 2010 +0200
+++ b/src/HOL/Tools/SMT/z3_proof_tools.ML Fri Aug 27 09:43:52 2010 +0200
@@ -198,7 +198,7 @@
| @{term Not} $ _ => abstr1 cvs ct
| @{term "op &"} $ _ $ _ => abstr2 cvs ct
| @{term "op |"} $ _ $ _ => abstr2 cvs ct
- | @{term "op -->"} $ _ $ _ => abstr2 cvs ct
+ | @{term HOL.implies} $ _ $ _ => abstr2 cvs ct
| Const (@{const_name "op ="}, _) $ _ $ _ => abstr2 cvs ct
| Const (@{const_name distinct}, _) $ _ =>
if ext_logic then abs_arg (abs_list abstr fresh_abstraction) cvs ct
--- a/src/HOL/Tools/Sledgehammer/metis_clauses.ML Fri Aug 27 09:34:06 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/metis_clauses.ML Fri Aug 27 09:43:52 2010 +0200
@@ -38,11 +38,10 @@
val const_prefix: string
val type_const_prefix: string
val class_prefix: string
- val union_all: ''a list list -> ''a list
val invert_const: string -> string
val ascii_of: string -> string
- val undo_ascii_of: string -> string
- val strip_prefix_and_undo_ascii: string -> string -> string option
+ val unascii_of: string -> string
+ val strip_prefix_and_unascii: string -> string -> string option
val make_bound_var : string -> string
val make_schematic_var : string * int -> string
val make_fixed_var : string -> string
@@ -98,7 +97,7 @@
(@{const_name "op ="}, "equal"),
(@{const_name "op &"}, "and"),
(@{const_name "op |"}, "or"),
- (@{const_name "op -->"}, "implies"),
+ (@{const_name HOL.implies}, "implies"),
(@{const_name Set.member}, "member"),
(@{const_name fequal}, "fequal"),
(@{const_name COMBI}, "COMBI"),
@@ -121,7 +120,7 @@
Alphanumeric characters are left unchanged.
The character _ goes to __
Characters in the range ASCII space to / go to _A to _P, respectively.
- Other printing characters go to _nnn where nnn is the decimal ASCII code.*)
+ Other characters go to _nnn where nnn is the decimal ASCII code.*)
val A_minus_space = Char.ord #"A" - Char.ord #" ";
fun stringN_of_int 0 _ = ""
@@ -132,9 +131,7 @@
else if c = #"_" then "__"
else if #" " <= c andalso c <= #"/"
then "_" ^ String.str (Char.chr (Char.ord c + A_minus_space))
- else if Char.isPrint c
- then ("_" ^ stringN_of_int 3 (Char.ord c)) (*fixed width, in case more digits follow*)
- else ""
+ else ("_" ^ stringN_of_int 3 (Char.ord c)) (*fixed width, in case more digits follow*)
val ascii_of = String.translate ascii_of_c;
@@ -142,29 +139,28 @@
(*We don't raise error exceptions because this code can run inside the watcher.
Also, the errors are "impossible" (hah!)*)
-fun undo_ascii_aux rcs [] = String.implode(rev rcs)
- | undo_ascii_aux rcs [#"_"] = undo_ascii_aux (#"_"::rcs) [] (*ERROR*)
+fun unascii_aux rcs [] = String.implode(rev rcs)
+ | unascii_aux rcs [#"_"] = unascii_aux (#"_"::rcs) [] (*ERROR*)
(*Three types of _ escapes: __, _A to _P, _nnn*)
- | undo_ascii_aux rcs (#"_" :: #"_" :: cs) = undo_ascii_aux (#"_"::rcs) cs
- | undo_ascii_aux rcs (#"_" :: c :: cs) =
+ | unascii_aux rcs (#"_" :: #"_" :: cs) = unascii_aux (#"_"::rcs) cs
+ | unascii_aux rcs (#"_" :: c :: cs) =
if #"A" <= c andalso c<= #"P" (*translation of #" " to #"/"*)
- then undo_ascii_aux (Char.chr(Char.ord c - A_minus_space) :: rcs) cs
+ then unascii_aux (Char.chr(Char.ord c - A_minus_space) :: rcs) cs
else
let val digits = List.take (c::cs, 3) handle Subscript => []
in
case Int.fromString (String.implode digits) of
- NONE => undo_ascii_aux (c:: #"_"::rcs) cs (*ERROR*)
- | SOME n => undo_ascii_aux (Char.chr n :: rcs) (List.drop (cs, 2))
+ NONE => unascii_aux (c:: #"_"::rcs) cs (*ERROR*)
+ | SOME n => unascii_aux (Char.chr n :: rcs) (List.drop (cs, 2))
end
- | undo_ascii_aux rcs (c::cs) = undo_ascii_aux (c::rcs) cs;
-
-val undo_ascii_of = undo_ascii_aux [] o String.explode;
+ | unascii_aux rcs (c::cs) = unascii_aux (c::rcs) cs
+val unascii_of = unascii_aux [] o String.explode
(* If string s has the prefix s1, return the result of deleting it,
un-ASCII'd. *)
-fun strip_prefix_and_undo_ascii s1 s =
+fun strip_prefix_and_unascii s1 s =
if String.isPrefix s1 s then
- SOME (undo_ascii_of (String.extract (s, size s1, NONE)))
+ SOME (unascii_of (String.extract (s, size s1, NONE)))
else
NONE
@@ -514,8 +510,8 @@
(*Type constructors used to instantiate overloaded constants are the only ones needed.*)
fun add_type_consts_in_term thy =
let
- val const_typargs = Sign.const_typargs thy
- fun aux (Const x) = fold (fold_type_consts set_insert) (const_typargs x)
+ fun aux (Const x) =
+ fold (fold_type_consts set_insert) (Sign.const_typargs thy x)
| aux (Abs (_, _, u)) = aux u
| aux (Const (@{const_name skolem_id}, _) $ _) = I
| aux (t $ u) = aux t #> aux u
--- a/src/HOL/Tools/Sledgehammer/metis_tactics.ML Fri Aug 27 09:34:06 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/metis_tactics.ML Fri Aug 27 09:43:52 2010 +0200
@@ -228,15 +228,15 @@
| smart_invert_const s = invert_const s
fun hol_type_from_metis_term _ (Metis.Term.Var v) =
- (case strip_prefix_and_undo_ascii tvar_prefix v of
+ (case strip_prefix_and_unascii tvar_prefix v of
SOME w => make_tvar w
| NONE => make_tvar v)
| hol_type_from_metis_term ctxt (Metis.Term.Fn(x, tys)) =
- (case strip_prefix_and_undo_ascii type_const_prefix x of
+ (case strip_prefix_and_unascii type_const_prefix x of
SOME tc => Term.Type (smart_invert_const tc,
map (hol_type_from_metis_term ctxt) tys)
| NONE =>
- case strip_prefix_and_undo_ascii tfree_prefix x of
+ case strip_prefix_and_unascii tfree_prefix x of
SOME tf => mk_tfree ctxt tf
| NONE => raise Fail ("hol_type_from_metis_term: " ^ x));
@@ -246,10 +246,10 @@
val _ = trace_msg (fn () => "hol_term_from_metis_PT: " ^
Metis.Term.toString fol_tm)
fun tm_to_tt (Metis.Term.Var v) =
- (case strip_prefix_and_undo_ascii tvar_prefix v of
+ (case strip_prefix_and_unascii tvar_prefix v of
SOME w => Type (make_tvar w)
| NONE =>
- case strip_prefix_and_undo_ascii schematic_var_prefix v of
+ case strip_prefix_and_unascii schematic_var_prefix v of
SOME w => Term (mk_var (w, HOLogic.typeT))
| NONE => Term (mk_var (v, HOLogic.typeT)) )
(*Var from Metis with a name like _nnn; possibly a type variable*)
@@ -266,7 +266,7 @@
and applic_to_tt ("=",ts) =
Term (list_comb(Const (@{const_name "op ="}, HOLogic.typeT), terms_of (map tm_to_tt ts)))
| applic_to_tt (a,ts) =
- case strip_prefix_and_undo_ascii const_prefix a of
+ case strip_prefix_and_unascii const_prefix a of
SOME b =>
let val c = smart_invert_const b
val ntypes = num_type_args thy c
@@ -284,14 +284,14 @@
cat_lines (map (Syntax.string_of_term ctxt) (terms_of tts)))
end
| NONE => (*Not a constant. Is it a type constructor?*)
- case strip_prefix_and_undo_ascii type_const_prefix a of
+ case strip_prefix_and_unascii type_const_prefix a of
SOME b =>
Type (Term.Type (smart_invert_const b, types_of (map tm_to_tt ts)))
| NONE => (*Maybe a TFree. Should then check that ts=[].*)
- case strip_prefix_and_undo_ascii tfree_prefix a of
+ case strip_prefix_and_unascii tfree_prefix a of
SOME b => Type (mk_tfree ctxt b)
| NONE => (*a fixed variable? They are Skolem functions.*)
- case strip_prefix_and_undo_ascii fixed_var_prefix a of
+ case strip_prefix_and_unascii fixed_var_prefix a of
SOME b =>
let val opr = Term.Free(b, HOLogic.typeT)
in apply_list opr (length ts) (map tm_to_tt ts) end
@@ -307,16 +307,16 @@
let val _ = trace_msg (fn () => "hol_term_from_metis_FT: " ^
Metis.Term.toString fol_tm)
fun cvt (Metis.Term.Fn ("ti", [Metis.Term.Var v, _])) =
- (case strip_prefix_and_undo_ascii schematic_var_prefix v of
+ (case strip_prefix_and_unascii schematic_var_prefix v of
SOME w => mk_var(w, dummyT)
| NONE => mk_var(v, dummyT))
| cvt (Metis.Term.Fn ("ti", [Metis.Term.Fn ("=",[]), _])) =
Const (@{const_name "op ="}, HOLogic.typeT)
| cvt (Metis.Term.Fn ("ti", [Metis.Term.Fn (x,[]), ty])) =
- (case strip_prefix_and_undo_ascii const_prefix x of
+ (case strip_prefix_and_unascii const_prefix x of
SOME c => Const (smart_invert_const c, dummyT)
| NONE => (*Not a constant. Is it a fixed variable??*)
- case strip_prefix_and_undo_ascii fixed_var_prefix x of
+ case strip_prefix_and_unascii fixed_var_prefix x of
SOME v => Free (v, hol_type_from_metis_term ctxt ty)
| NONE => raise Fail ("hol_term_from_metis_FT bad constant: " ^ x))
| cvt (Metis.Term.Fn ("ti", [Metis.Term.Fn (".",[tm1,tm2]), _])) =
@@ -327,10 +327,10 @@
| cvt (Metis.Term.Fn ("=", [tm1,tm2])) =
list_comb(Const (@{const_name "op ="}, HOLogic.typeT), map cvt [tm1,tm2])
| cvt (t as Metis.Term.Fn (x, [])) =
- (case strip_prefix_and_undo_ascii const_prefix x of
+ (case strip_prefix_and_unascii const_prefix x of
SOME c => Const (smart_invert_const c, dummyT)
| NONE => (*Not a constant. Is it a fixed variable??*)
- case strip_prefix_and_undo_ascii fixed_var_prefix x of
+ case strip_prefix_and_unascii fixed_var_prefix x of
SOME v => Free (v, dummyT)
| NONE => (trace_msg (fn () => "hol_term_from_metis_FT bad const: " ^ x);
hol_term_from_metis_PT ctxt t))
@@ -410,11 +410,11 @@
" in " ^ Display.string_of_thm ctxt i_th);
NONE)
fun remove_typeinst (a, t) =
- case strip_prefix_and_undo_ascii schematic_var_prefix a of
+ case strip_prefix_and_unascii schematic_var_prefix a of
SOME b => SOME (b, t)
- | NONE => case strip_prefix_and_undo_ascii tvar_prefix a of
+ | NONE => case strip_prefix_and_unascii tvar_prefix a of
SOME _ => NONE (*type instantiations are forbidden!*)
- | NONE => SOME (a,t) (*internal Metis var?*)
+ | NONE => SOME (a,t) (*internal Metis var?*)
val _ = trace_msg (fn () => " isa th: " ^ Display.string_of_thm ctxt i_th)
val substs = map_filter remove_typeinst (Metis.Subst.toList fsubst)
val (vars,rawtms) = ListPair.unzip (map_filter subst_translation substs)
--- a/src/HOL/Tools/Sledgehammer/sledgehammer.ML Fri Aug 27 09:34:06 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer.ML Fri Aug 27 09:43:52 2010 +0200
@@ -9,6 +9,7 @@
signature SLEDGEHAMMER =
sig
type failure = ATP_Systems.failure
+ type locality = Sledgehammer_Fact_Filter.locality
type relevance_override = Sledgehammer_Fact_Filter.relevance_override
type minimize_command = Sledgehammer_Proof_Reconstruct.minimize_command
type params =
@@ -18,11 +19,9 @@
atps: string list,
full_types: bool,
explicit_apply: bool,
- relevance_threshold: real,
- relevance_convergence: real,
- max_relevant_per_iter: int option,
+ relevance_thresholds: real * real,
+ max_relevant: int option,
theory_relevant: bool option,
- defs_relevant: bool,
isar_proof: bool,
isar_shrink_factor: int,
timeout: Time.time}
@@ -30,16 +29,16 @@
{subgoal: int,
goal: Proof.context * (thm list * thm),
relevance_override: relevance_override,
- axioms: ((string * bool) * thm) list option}
+ axioms: ((string * locality) * thm) list option}
type prover_result =
{outcome: failure option,
message: string,
pool: string Symtab.table,
- used_thm_names: (string * bool) list,
+ used_thm_names: (string * locality) list,
atp_run_time_in_msecs: int,
output: string,
proof: string,
- axiom_names: (string * bool) vector,
+ axiom_names: (string * locality) vector,
conjecture_shape: int list list}
type prover = params -> minimize_command -> problem -> prover_result
@@ -87,11 +86,9 @@
atps: string list,
full_types: bool,
explicit_apply: bool,
- relevance_threshold: real,
- relevance_convergence: real,
- max_relevant_per_iter: int option,
+ relevance_thresholds: real * real,
+ max_relevant: int option,
theory_relevant: bool option,
- defs_relevant: bool,
isar_proof: bool,
isar_shrink_factor: int,
timeout: Time.time}
@@ -100,17 +97,17 @@
{subgoal: int,
goal: Proof.context * (thm list * thm),
relevance_override: relevance_override,
- axioms: ((string * bool) * thm) list option}
+ axioms: ((string * locality) * thm) list option}
type prover_result =
{outcome: failure option,
message: string,
pool: string Symtab.table,
- used_thm_names: (string * bool) list,
+ used_thm_names: (string * locality) list,
atp_run_time_in_msecs: int,
output: string,
proof: string,
- axiom_names: (string * bool) vector,
+ axiom_names: (string * locality) vector,
conjecture_shape: int list list}
type prover = params -> minimize_command -> problem -> prover_result
@@ -174,10 +171,9 @@
Scan.this_string set_ClauseFormulaRelationN |-- $$ "("
|-- Scan.repeat parse_clause_formula_pair
val extract_clause_formula_relation =
- Substring.full
- #> Substring.position set_ClauseFormulaRelationN
- #> snd #> Substring.string #> strip_spaces #> explode
- #> parse_clause_formula_relation #> fst
+ Substring.full #> Substring.position set_ClauseFormulaRelationN
+ #> snd #> Substring.string #> strip_spaces_except_between_ident_chars
+ #> explode #> parse_clause_formula_relation #> fst
fun repair_conjecture_shape_and_theorem_names output conjecture_shape
axiom_names =
@@ -190,17 +186,19 @@
val seq = extract_clause_sequence output
val name_map = extract_clause_formula_relation output
fun renumber_conjecture j =
- conjecture_prefix ^ Int.toString (j - j0)
+ conjecture_prefix ^ string_of_int (j - j0)
|> AList.find (fn (s, ss) => member (op =) ss s) name_map
|> map (fn s => find_index (curry (op =) s) seq + 1)
fun name_for_number j =
let
val axioms =
- j |> AList.lookup (op =) name_map
- |> these |> map_filter (try (unprefix axiom_prefix))
- |> map undo_ascii_of
- val chained = forall (is_true_for axiom_names) axioms
- in (axioms |> space_implode " ", chained) end
+ j |> AList.lookup (op =) name_map |> these
+ |> map_filter (try (unprefix axiom_prefix)) |> map unascii_of
+ val loc =
+ case axioms of
+ [axiom] => find_first_in_vector axiom_names axiom General
+ | _ => General
+ in (axioms |> space_implode " ", loc) end
in
(conjecture_shape |> map (maps renumber_conjecture),
seq |> map name_for_number |> Vector.fromList)
@@ -213,12 +211,11 @@
fun prover_fun atp_name
{exec, required_execs, arguments, has_incomplete_mode, proof_delims,
- known_failures, default_max_relevant_per_iter, default_theory_relevant,
+ known_failures, default_max_relevant, default_theory_relevant,
explicit_forall, use_conjecture_for_hypotheses}
({debug, verbose, overlord, full_types, explicit_apply,
- relevance_threshold, relevance_convergence,
- max_relevant_per_iter, theory_relevant,
- defs_relevant, isar_proof, isar_shrink_factor, timeout, ...} : params)
+ relevance_thresholds, max_relevant, theory_relevant, isar_proof,
+ isar_shrink_factor, timeout, ...} : params)
minimize_command
({subgoal, goal, relevance_override, axioms} : problem) =
let
@@ -226,7 +223,7 @@
val thy = ProofContext.theory_of ctxt
val (params, hyp_ts, concl_t) = strip_subgoal th subgoal
- fun print s = (priority s; if debug then tracing s else ())
+ val print = priority
fun print_v f = () |> verbose ? print o f
fun print_d f = () |> debug ? print o f
@@ -234,15 +231,13 @@
case axioms of
SOME axioms => axioms
| NONE =>
- (relevant_facts full_types relevance_threshold relevance_convergence
- defs_relevant
- (the_default default_max_relevant_per_iter
- max_relevant_per_iter)
+ (relevant_facts full_types relevance_thresholds
+ (the_default default_max_relevant max_relevant)
(the_default default_theory_relevant theory_relevant)
relevance_override goal hyp_ts concl_t
|> tap ((fn n => print_v (fn () =>
- "Selected " ^ string_of_int n ^ " fact" ^ plural_s n ^
- " for " ^ quote atp_name ^ ".")) o length))
+ "Selected " ^ string_of_int n ^ " fact" ^ plural_s n ^
+ " for " ^ quote atp_name ^ ".")) o length))
(* path to unique problem file *)
val the_dest_dir = if overlord then getenv "ISABELLE_HOME_USER"
@@ -261,6 +256,7 @@
else error ("No such directory: " ^ the_dest_dir ^ ".")
end;
+ val measure_run_time = verbose orelse Config.get ctxt measure_runtime
val command = Path.explode (getenv (fst exec) ^ "/" ^ snd exec)
(* write out problem file and call prover *)
fun command_line complete timeout probfile =
@@ -268,10 +264,8 @@
val core = File.shell_path command ^ " " ^ arguments complete timeout ^
" " ^ File.shell_path probfile
in
- (if Config.get ctxt measure_runtime then
- "TIMEFORMAT='%3U'; { time " ^ core ^ " ; }"
- else
- "exec " ^ core) ^ " 2>&1"
+ (if measure_run_time then "TIMEFORMAT='%3U'; { time " ^ core ^ " ; }"
+ else "exec " ^ core) ^ " 2>&1"
end
fun split_time s =
let
@@ -300,14 +294,11 @@
prefix ("% " ^ command ^ "\n% " ^ timestamp () ^ "\n")
else
I)
- |>> (if Config.get ctxt measure_runtime then split_time
- else rpair 0)
+ |>> (if measure_run_time then split_time else rpair 0)
val (proof, outcome) =
extract_proof_and_outcome complete res_code proof_delims
known_failures output
in (output, msecs, proof, outcome) end
- val _ = print_d (fn () => "Preparing problem for " ^
- quote atp_name ^ "...")
val readable_names = debug andalso overlord
val (problem, pool, conjecture_offset, axiom_names) =
prepare_problem ctxt readable_names explicit_forall full_types
@@ -358,6 +349,11 @@
proof_text isar_proof
(pool, debug, isar_shrink_factor, ctxt, conjecture_shape)
(full_types, minimize_command, proof, axiom_names, th, subgoal)
+ |>> (fn message =>
+ message ^ (if verbose then
+ "\nATP CPU time: " ^ string_of_int msecs ^ " ms."
+ else
+ ""))
| SOME failure => (string_for_failure failure, [])
in
{outcome = outcome, message = message, pool = pool,
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML Fri Aug 27 09:34:06 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML Fri Aug 27 09:43:52 2010 +0200
@@ -5,19 +5,21 @@
signature SLEDGEHAMMER_FACT_FILTER =
sig
+ datatype locality = General | Theory | Local | Chained
+
type relevance_override =
{add: Facts.ref list,
del: Facts.ref list,
only: bool}
val trace : bool Unsynchronized.ref
- val name_thms_pair_from_ref :
+ val name_thm_pairs_from_ref :
Proof.context -> unit Symtab.table -> thm list -> Facts.ref
- -> (unit -> string * bool) * thm list
+ -> ((string * locality) * thm) list
val relevant_facts :
- bool -> real -> real -> bool -> int -> bool -> relevance_override
+ bool -> real * real -> int -> bool -> relevance_override
-> Proof.context * (thm list * 'a) -> term list -> term
- -> ((string * bool) * thm) list
+ -> ((string * locality) * thm) list
end;
structure Sledgehammer_Fact_Filter : SLEDGEHAMMER_FACT_FILTER =
@@ -30,6 +32,8 @@
val respect_no_atp = true
+datatype locality = General | Theory | Local | Chained
+
type relevance_override =
{add: Facts.ref list,
del: Facts.ref list,
@@ -37,13 +41,22 @@
val sledgehammer_prefix = "Sledgehammer" ^ Long_Name.separator
-fun name_thms_pair_from_ref ctxt reserved chained_ths xref =
- let val ths = ProofContext.get_fact ctxt xref in
- (fn () => let
- val name = Facts.string_of_ref xref
- val name = name |> Symtab.defined reserved name ? quote
- val chained = forall (member Thm.eq_thm chained_ths) ths
- in (name, chained) end, ths)
+fun repair_name reserved multi j name =
+ (name |> Symtab.defined reserved name ? quote) ^
+ (if multi then "(" ^ Int.toString j ^ ")" else "")
+
+fun name_thm_pairs_from_ref ctxt reserved chained_ths xref =
+ let
+ val ths = ProofContext.get_fact ctxt xref
+ val name = Facts.string_of_ref xref
+ val multi = length ths > 1
+ in
+ (ths, (1, []))
+ |-> fold (fn th => fn (j, rest) =>
+ (j + 1, ((repair_name reserved multi j name,
+ if member Thm.eq_thm chained_ths th then Chained
+ else General), th) :: rest))
+ |> snd
end
(***************************************************************)
@@ -53,61 +66,81 @@
(*** constants with types ***)
(*An abstraction of Isabelle types*)
-datatype const_typ = CTVar | CType of string * const_typ list
+datatype pseudotype = PVar | PType of string * pseudotype list
+
+fun string_for_pseudotype PVar = "?"
+ | string_for_pseudotype (PType (s, Ts)) =
+ (case Ts of
+ [] => ""
+ | [T] => string_for_pseudotype T
+ | Ts => string_for_pseudotypes Ts ^ " ") ^ s
+and string_for_pseudotypes Ts =
+ "(" ^ commas (map string_for_pseudotype Ts) ^ ")"
(*Is the second type an instance of the first one?*)
-fun match_type (CType(con1,args1)) (CType(con2,args2)) =
- con1=con2 andalso match_types args1 args2
- | match_type CTVar _ = true
- | match_type _ CTVar = false
-and match_types [] [] = true
- | match_types (a1::as1) (a2::as2) = match_type a1 a2 andalso match_types as1 as2;
+fun match_pseudotype (PType (a, T), PType (b, U)) =
+ a = b andalso match_pseudotypes (T, U)
+ | match_pseudotype (PVar, _) = true
+ | match_pseudotype (_, PVar) = false
+and match_pseudotypes ([], []) = true
+ | match_pseudotypes (T :: Ts, U :: Us) =
+ match_pseudotype (T, U) andalso match_pseudotypes (Ts, Us)
(*Is there a unifiable constant?*)
-fun const_mem const_tab (c, c_typ) =
- exists (match_types c_typ) (these (Symtab.lookup const_tab c))
+fun pseudoconst_mem f const_tab (c, c_typ) =
+ exists (curry (match_pseudotypes o f) c_typ)
+ (these (Symtab.lookup const_tab c))
-(*Maps a "real" type to a const_typ*)
-fun const_typ_of (Type (c,typs)) = CType (c, map const_typ_of typs)
- | const_typ_of (TFree _) = CTVar
- | const_typ_of (TVar _) = CTVar
+fun pseudotype_for (Type (c,typs)) = PType (c, map pseudotype_for typs)
+ | pseudotype_for (TFree _) = PVar
+ | pseudotype_for (TVar _) = PVar
+(* Pairs a constant with the list of its type instantiations. *)
+fun pseudoconst_for thy (c, T) =
+ (c, map pseudotype_for (Sign.const_typargs thy (c, T)))
+ handle TYPE _ => (c, []) (* Variable (locale constant): monomorphic *)
-(*Pairs a constant with the list of its type instantiations (using const_typ)*)
-fun const_with_typ thy (c,typ) =
- let val tvars = Sign.const_typargs thy (c,typ) in
- (c, map const_typ_of tvars) end
- handle TYPE _ => (c, []) (*Variable (locale constant): monomorphic*)
+fun string_for_pseudoconst (s, []) = s
+ | string_for_pseudoconst (s, Ts) = s ^ string_for_pseudotypes Ts
+fun string_for_super_pseudoconst (s, [[]]) = s
+ | string_for_super_pseudoconst (s, Tss) =
+ s ^ "{" ^ commas (map string_for_pseudotypes Tss) ^ "}"
+
+val abs_prefix = "Sledgehammer.abs"
+val skolem_prefix = "Sledgehammer.sko"
-(*Add a const/type pair to the table, but a [] entry means a standard connective,
- which we ignore.*)
-fun add_const_to_table (c, ctyps) =
- Symtab.map_default (c, [ctyps])
- (fn [] => [] | ctypss => insert (op =) ctyps ctypss)
+(* Add a pseudoconstant to the table, but a [] entry means a standard
+ connective, which we ignore.*)
+fun add_pseudoconst_to_table also_skolem (c, ctyps) =
+ if also_skolem orelse not (String.isPrefix skolem_prefix c) then
+ Symtab.map_default (c, [ctyps])
+ (fn [] => [] | ctypss => insert (op =) ctyps ctypss)
+ else
+ I
fun is_formula_type T = (T = HOLogic.boolT orelse T = propT)
-val fresh_prefix = "Sledgehammer.FRESH."
val flip = Option.map not
(* These are typically simplified away by "Meson.presimplify". *)
val boring_consts =
[@{const_name False}, @{const_name True}, @{const_name If}, @{const_name Let}]
-fun get_consts thy pos ts =
+fun get_pseudoconsts thy also_skolems pos ts =
let
(* We include free variables, as well as constants, to handle locales. For
each quantifiers that must necessarily be skolemized by the ATP, we
introduce a fresh constant to simulate the effect of Skolemization. *)
fun do_term t =
case t of
- Const x => add_const_to_table (const_with_typ thy x)
- | Free (s, _) => add_const_to_table (s, [])
+ Const x => add_pseudoconst_to_table also_skolems (pseudoconst_for thy x)
+ | Free (s, _) => add_pseudoconst_to_table also_skolems (s, [])
| t1 $ t2 => fold do_term [t1, t2]
- | Abs (_, _, t') => do_term t'
+ | Abs (_, _, t') =>
+ do_term t' #> add_pseudoconst_to_table true (abs_prefix, [])
| _ => I
fun do_quantifier will_surely_be_skolemized body_t =
do_formula pos body_t
- #> (if will_surely_be_skolemized then
- add_const_to_table (gensym fresh_prefix, [])
+ #> (if also_skolems andalso will_surely_be_skolemized then
+ add_pseudoconst_to_table true (gensym skolem_prefix, [])
else
I)
and do_term_or_formula T =
@@ -128,7 +161,7 @@
do_quantifier (pos = SOME true) body_t
| @{const "op &"} $ t1 $ t2 => fold (do_formula pos) [t1, t2]
| @{const "op |"} $ t1 $ t2 => fold (do_formula pos) [t1, t2]
- | @{const "op -->"} $ t1 $ t2 =>
+ | @{const HOL.implies} $ t1 $ t2 =>
do_formula (flip pos) t1 #> do_formula pos t2
| Const (@{const_name "op ="}, Type (_, [T, _])) $ t1 $ t2 =>
fold (do_term_or_formula T) [t1, t2]
@@ -164,31 +197,25 @@
(**** Constant / Type Frequencies ****)
-(*A two-dimensional symbol table counts frequencies of constants. It's keyed first by
- constant name and second by its list of type instantiations. For the latter, we need
- a linear ordering on type const_typ list.*)
-
-local
-
-fun cons_nr CTVar = 0
- | cons_nr (CType _) = 1;
+(* A two-dimensional symbol table counts frequencies of constants. It's keyed
+ first by constant name and second by its list of type instantiations. For the
+ latter, we need a linear ordering on "pseudotype list". *)
-in
+fun pseudotype_ord p =
+ case p of
+ (PVar, PVar) => EQUAL
+ | (PVar, PType _) => LESS
+ | (PType _, PVar) => GREATER
+ | (PType q1, PType q2) =>
+ prod_ord fast_string_ord (dict_ord pseudotype_ord) (q1, q2)
-fun const_typ_ord TU =
- case TU of
- (CType (a, Ts), CType (b, Us)) =>
- (case fast_string_ord(a,b) of EQUAL => dict_ord const_typ_ord (Ts,Us) | ord => ord)
- | (T, U) => int_ord (cons_nr T, cons_nr U);
-
-end;
-
-structure CTtab = Table(type key = const_typ list val ord = dict_ord const_typ_ord);
+structure CTtab =
+ Table(type key = pseudotype list val ord = dict_ord pseudotype_ord)
fun count_axiom_consts theory_relevant thy (_, th) =
let
fun do_const (a, T) =
- let val (c, cts) = const_with_typ thy (a, T) in
+ let val (c, cts) = pseudoconst_for thy (a, T) in
(* Two-dimensional table update. Constant maps to types maps to
count. *)
CTtab.map_default (cts, 0) (Integer.add 1)
@@ -205,8 +232,8 @@
(**** Actual Filtering Code ****)
(*The frequency of a constant is the sum of those of all instances of its type.*)
-fun const_frequency const_tab (c, cts) =
- CTtab.fold (fn (cts', m) => match_types cts cts' ? Integer.add m)
+fun pseudoconst_freq match const_tab (c, cts) =
+ CTtab.fold (fn (cts', m) => match (cts, cts') ? Integer.add m)
(the (Symtab.lookup const_tab c)) 0
handle Option.Option => 0
@@ -216,183 +243,206 @@
(* "log" seems best in practice. A constant function of one ignores the constant
frequencies. *)
-fun rel_log (x : real) = 1.0 + 2.0 / Math.ln (x + 1.0)
-fun irrel_log (x : real) = Math.ln (x + 19.0) / 6.4
+fun rel_log n = 1.0 + 2.0 / Math.ln (Real.fromInt n + 1.0)
+(* TODO: experiment
+fun irrel_log n = 0.5 + 1.0 / Math.ln (Real.fromInt n + 1.0)
+*)
+fun irrel_log n = Math.ln (Real.fromInt n + 19.0) / 6.4
+
+(* FUDGE *)
+val skolem_weight = 1.0
+val abs_weight = 2.0
(* Computes a constant's weight, as determined by its frequency. *)
-val rel_const_weight = rel_log o real oo const_frequency
-val irrel_const_weight = irrel_log o real oo const_frequency
-(* fun irrel_const_weight _ _ = 1.0 FIXME: OLD CODE *)
-
-fun axiom_weight const_tab relevant_consts axiom_consts =
- let
- val (rel, irrel) = List.partition (const_mem relevant_consts) axiom_consts
- val rel_weight = fold (curry Real.+ o rel_const_weight const_tab) rel 0.0
- val irrel_weight = fold (curry Real.+ o irrel_const_weight const_tab) irrel 0.0
- val res = rel_weight / (rel_weight + irrel_weight)
- in if Real.isFinite res then res else 0.0 end
-
-(* OLD CODE:
-(*Relevant constants are weighted according to frequency,
- but irrelevant constants are simply counted. Otherwise, Skolem functions,
- which are rare, would harm a formula's chances of being picked.*)
-fun axiom_weight const_tab relevant_consts axiom_consts =
- let
- val rel = filter (const_mem relevant_consts) axiom_consts
- val rel_weight = fold (curry Real.+ o rel_const_weight const_tab) rel 0.0
- val res = rel_weight / (rel_weight + real (length axiom_consts - length rel))
- in if Real.isFinite res then res else 0.0 end
+val rel_weight = rel_log oo pseudoconst_freq match_pseudotypes
+fun irrel_weight const_tab (c as (s, _)) =
+ if String.isPrefix skolem_prefix s then skolem_weight
+ else if String.isPrefix abs_prefix s then abs_weight
+ else irrel_log (pseudoconst_freq (match_pseudotypes o swap) const_tab c)
+(* TODO: experiment
+fun irrel_weight _ _ = 1.0
*)
-(*Multiplies out to a list of pairs: 'a * 'b list -> ('a * 'b) list -> ('a * 'b) list*)
-fun add_expand_pairs (x, ys) xys = List.foldl (fn (y,acc) => (x,y)::acc) xys ys
+(* FUDGE *)
+fun locality_multiplier General = 1.0
+ | locality_multiplier Theory = 1.1
+ | locality_multiplier Local = 1.3
+ | locality_multiplier Chained = 2.0
+
+fun axiom_weight loc const_tab relevant_consts axiom_consts =
+ case axiom_consts |> List.partition (pseudoconst_mem I relevant_consts)
+ ||> filter_out (pseudoconst_mem swap relevant_consts) of
+ ([], []) => 0.0
+ | (_, []) => 1.0
+ | (rel, irrel) =>
+ let
+ val rel_weight = fold (curry Real.+ o rel_weight const_tab) rel 0.0
+ |> curry Real.* (locality_multiplier loc)
+ val irrel_weight = fold (curry Real.+ o irrel_weight const_tab) irrel 0.0
+ val res = rel_weight / (rel_weight + irrel_weight)
+ in if Real.isFinite res then res else 0.0 end
-fun consts_of_term thy t =
- Symtab.fold add_expand_pairs (get_consts thy (SOME true) [t]) []
+(* TODO: experiment
+fun debug_axiom_weight const_tab relevant_consts axiom_consts =
+ case axiom_consts |> List.partition (pseudoconst_mem I relevant_consts)
+ ||> filter_out (pseudoconst_mem swap relevant_consts) of
+ ([], []) => 0.0
+ | (_, []) => 1.0
+ | (rel, irrel) =>
+ let
+val _ = tracing (PolyML.makestring ("REL: ", rel))
+val _ = tracing (PolyML.makestring ("IRREL: ", irrel))
+ val rel_weight = fold (curry Real.+ o rel_weight const_tab) rel 0.0
+ val irrel_weight = fold (curry Real.+ o irrel_weight const_tab) irrel 0.0
+ val res = rel_weight / (rel_weight + irrel_weight)
+ in if Real.isFinite res then res else 0.0 end
+*)
+fun pseudoconsts_of_term thy t =
+ Symtab.fold (fn (x, ys) => fold (fn y => cons (x, y)) ys)
+ (get_pseudoconsts thy true (SOME true) [t]) []
fun pair_consts_axiom theory_relevant thy axiom =
(axiom, axiom |> snd |> theory_const_prop_of theory_relevant
- |> consts_of_term thy)
-
-exception CONST_OR_FREE of unit
-
-fun dest_Const_or_Free (Const x) = x
- | dest_Const_or_Free (Free x) = x
- | dest_Const_or_Free _ = raise CONST_OR_FREE ()
-
-(*Look for definitions of the form f ?x1 ... ?xn = t, but not reversed.*)
-fun defines thy thm gctypes =
- let val tm = prop_of thm
- fun defs lhs rhs =
- let val (rator,args) = strip_comb lhs
- val ct = const_with_typ thy (dest_Const_or_Free rator)
- in
- forall is_Var args andalso const_mem gctypes ct andalso
- subset (op =) (Term.add_vars rhs [], Term.add_vars lhs [])
- end
- handle CONST_OR_FREE () => false
- in
- case tm of
- @{const Trueprop} $ (Const (@{const_name "op ="}, _) $ lhs $ rhs) =>
- defs lhs rhs
- | _ => false
- end;
+ |> pseudoconsts_of_term thy)
type annotated_thm =
- ((unit -> string * bool) * thm) * (string * const_typ list) list
-
-(*For a reverse sort, putting the largest values first.*)
-fun compare_pairs ((_, w1), (_, w2)) = Real.compare (w2, w1)
+ (((unit -> string) * locality) * thm) * (string * pseudotype list) list
-(* Limit the number of new facts, to prevent runaway acceptance. *)
-fun take_best max_new (new_pairs : (annotated_thm * real) list) =
- let val nnew = length new_pairs in
- if nnew <= max_new then
- (map #1 new_pairs, [])
- else
- let
- val new_pairs = sort compare_pairs new_pairs
- val accepted = List.take (new_pairs, max_new)
- in
- trace_msg (fn () => ("Number of candidates, " ^ Int.toString nnew ^
- ", exceeds the limit of " ^ Int.toString max_new));
- trace_msg (fn () => ("Effective pass mark: " ^ Real.toString (#2 (List.last accepted))));
- trace_msg (fn () => "Actually passed: " ^
- space_implode ", " (map (fst o (fn f => f ()) o fst o fst o fst) accepted));
- (map #1 accepted, List.drop (new_pairs, max_new))
- end
- end;
+fun take_most_relevant max_max_imperfect max_relevant remaining_max
+ (candidates : (annotated_thm * real) list) =
+ let
+ val max_imperfect =
+ Real.ceil (Math.pow (max_max_imperfect,
+ Real.fromInt remaining_max
+ / Real.fromInt max_relevant))
+ val (perfect, imperfect) =
+ candidates |> List.partition (fn (_, w) => w > 0.99999)
+ ||> sort (Real.compare o swap o pairself snd)
+ val ((accepts, more_rejects), rejects) =
+ chop max_imperfect imperfect |>> append perfect |>> chop remaining_max
+ in
+ trace_msg (fn () => "Number of candidates: " ^
+ string_of_int (length candidates));
+ trace_msg (fn () => "Effective threshold: " ^
+ Real.toString (#2 (hd accepts)));
+ trace_msg (fn () => "Actually passed (" ^ Int.toString (length accepts) ^
+ "): " ^ (accepts
+ |> map (fn ((((name, _), _), _), weight) =>
+ name () ^ " [" ^ Real.toString weight ^ "]")
+ |> commas));
+ (accepts, more_rejects @ rejects)
+ end
+(* FUDGE *)
val threshold_divisor = 2.0
val ridiculous_threshold = 0.1
+val max_max_imperfect_fudge_factor = 0.66
-fun relevance_filter ctxt relevance_threshold relevance_convergence
- defs_relevant max_new theory_relevant
+fun relevance_filter ctxt threshold0 decay max_relevant theory_relevant
({add, del, ...} : relevance_override) axioms goal_ts =
- if relevance_threshold > 1.0 then
- []
- else if relevance_threshold < 0.0 then
- axioms
- else
- let
- val thy = ProofContext.theory_of ctxt
- val const_tab = fold (count_axiom_consts theory_relevant thy) axioms
- Symtab.empty
- val goal_const_tab = get_consts thy (SOME false) goal_ts
- val _ =
- trace_msg (fn () => "Initial constants: " ^
- commas (goal_const_tab
- |> Symtab.dest
- |> filter (curry (op <>) [] o snd)
- |> map fst))
- val add_thms = maps (ProofContext.get_fact ctxt) add
- val del_thms = maps (ProofContext.get_fact ctxt) del
- fun iter j threshold rel_const_tab =
- let
- fun relevant ([], rejects) [] =
- (* Nothing was added this iteration. *)
- if j = 0 andalso threshold >= ridiculous_threshold then
- (* First iteration? Try again. *)
- iter 0 (threshold / threshold_divisor) rel_const_tab
- (map (apsnd SOME) rejects)
+ let
+ val thy = ProofContext.theory_of ctxt
+ val const_tab = fold (count_axiom_consts theory_relevant thy) axioms
+ Symtab.empty
+ val add_thms = maps (ProofContext.get_fact ctxt) add
+ val del_thms = maps (ProofContext.get_fact ctxt) del
+ val max_max_imperfect =
+ Math.sqrt (Real.fromInt max_relevant * max_max_imperfect_fudge_factor)
+ fun iter j remaining_max threshold rel_const_tab hopeless hopeful =
+ let
+ fun game_over rejects =
+ (* Add "add:" facts. *)
+ if null add_thms then
+ []
+ else
+ map_filter (fn ((p as (_, th), _), _) =>
+ if member Thm.eq_thm add_thms th then SOME p
+ else NONE) rejects
+ fun relevant [] rejects hopeless [] =
+ (* Nothing has been added this iteration. *)
+ if j = 0 andalso threshold >= ridiculous_threshold then
+ (* First iteration? Try again. *)
+ iter 0 max_relevant (threshold / threshold_divisor) rel_const_tab
+ hopeless hopeful
+ else
+ game_over (rejects @ hopeless)
+ | relevant candidates rejects hopeless [] =
+ let
+ val (accepts, more_rejects) =
+ take_most_relevant max_max_imperfect max_relevant remaining_max
+ candidates
+ val rel_const_tab' =
+ rel_const_tab
+ |> fold (add_pseudoconst_to_table false)
+ (maps (snd o fst) accepts)
+ fun is_dirty (c, _) =
+ Symtab.lookup rel_const_tab' c <> Symtab.lookup rel_const_tab c
+ val (hopeful_rejects, hopeless_rejects) =
+ (rejects @ hopeless, ([], []))
+ |-> fold (fn (ax as (_, consts), old_weight) =>
+ if exists is_dirty consts then
+ apfst (cons (ax, NONE))
+ else
+ apsnd (cons (ax, old_weight)))
+ |>> append (more_rejects
+ |> map (fn (ax as (_, consts), old_weight) =>
+ (ax, if exists is_dirty consts then NONE
+ else SOME old_weight)))
+ val threshold =
+ threshold + (1.0 - threshold)
+ * Math.pow (decay, Real.fromInt (length accepts))
+ val remaining_max = remaining_max - length accepts
+ in
+ trace_msg (fn () => "New or updated constants: " ^
+ commas (rel_const_tab' |> Symtab.dest
+ |> subtract (op =) (Symtab.dest rel_const_tab)
+ |> map string_for_super_pseudoconst));
+ map (fst o fst) accepts @
+ (if remaining_max = 0 then
+ game_over (hopeful_rejects @ map (apsnd SOME) hopeless_rejects)
+ else
+ iter (j + 1) remaining_max threshold rel_const_tab'
+ hopeless_rejects hopeful_rejects)
+ end
+ | relevant candidates rejects hopeless
+ (((ax as (((_, loc), th), axiom_consts)), cached_weight)
+ :: hopeful) =
+ let
+ val weight =
+ case cached_weight of
+ SOME w => w
+ | NONE => axiom_weight loc const_tab rel_const_tab axiom_consts
+(* TODO: experiment
+val name = fst (fst (fst ax)) ()
+val _ = if String.isPrefix "lift.simps(3" name then
+tracing ("*** " ^ name ^ PolyML.makestring (debug_axiom_weight const_tab rel_const_tab axiom_consts))
+else
+()
+*)
+ in
+ if weight >= threshold then
+ relevant ((ax, weight) :: candidates) rejects hopeless hopeful
else
- (* Add "add:" facts. *)
- if null add_thms then
- []
- else
- map_filter (fn ((p as (_, th), _), _) =>
- if member Thm.eq_thm add_thms th then SOME p
- else NONE) rejects
- | relevant (new_pairs, rejects) [] =
- let
- val (new_rels, more_rejects) = take_best max_new new_pairs
- val rel_const_tab' =
- rel_const_tab |> fold add_const_to_table (maps snd new_rels)
- fun is_dirty c =
- const_mem rel_const_tab' c andalso
- not (const_mem rel_const_tab c)
- val rejects =
- more_rejects @ rejects
- |> map (fn (ax as (_, consts), old_weight) =>
- (ax, if exists is_dirty consts then NONE
- else SOME old_weight))
- val threshold =
- threshold + (1.0 - threshold) * relevance_convergence
- in
- trace_msg (fn () => "relevant this iteration: " ^
- Int.toString (length new_rels));
- map #1 new_rels @ iter (j + 1) threshold rel_const_tab' rejects
- end
- | relevant (new_rels, rejects)
- (((ax as ((name, th), axiom_consts)), cached_weight)
- :: rest) =
- let
- val weight =
- case cached_weight of
- SOME w => w
- | NONE => axiom_weight const_tab rel_const_tab axiom_consts
- in
- if weight >= threshold orelse
- (defs_relevant andalso defines thy th rel_const_tab) then
- (trace_msg (fn () =>
- fst (name ()) ^ " passes: " ^ Real.toString weight
- ^ " consts: " ^ commas (map fst axiom_consts));
- relevant ((ax, weight) :: new_rels, rejects) rest)
- else
- relevant (new_rels, (ax, weight) :: rejects) rest
- end
- in
- trace_msg (fn () => "relevant_facts, current threshold: " ^
- Real.toString threshold);
- relevant ([], [])
- end
- in
- axioms |> filter_out (member Thm.eq_thm del_thms o snd)
- |> map (rpair NONE o pair_consts_axiom theory_relevant thy)
- |> iter 0 relevance_threshold goal_const_tab
- |> tap (fn res => trace_msg (fn () =>
+ relevant candidates ((ax, weight) :: rejects) hopeless hopeful
+ end
+ in
+ trace_msg (fn () =>
+ "ITERATION " ^ string_of_int j ^ ": current threshold: " ^
+ Real.toString threshold ^ ", constants: " ^
+ commas (rel_const_tab |> Symtab.dest
+ |> filter (curry (op <>) [] o snd)
+ |> map string_for_super_pseudoconst));
+ relevant [] [] hopeless hopeful
+ end
+ in
+ axioms |> filter_out (member Thm.eq_thm del_thms o snd)
+ |> map (rpair NONE o pair_consts_axiom theory_relevant thy)
+ |> iter 0 max_relevant threshold0
+ (get_pseudoconsts thy false (SOME false) goal_ts) []
+ |> tap (fn res => trace_msg (fn () =>
"Total relevant: " ^ Int.toString (length res)))
- end
+ end
+
(***************************************************************)
(* Retrieving and filtering lemmas *)
@@ -491,7 +541,7 @@
| (_, @{const "==>"} $ t1 $ t2) =>
do_formula (not pos) t1 andalso
(t2 = @{prop False} orelse do_formula pos t2)
- | (_, @{const "op -->"} $ t1 $ t2) =>
+ | (_, @{const HOL.implies} $ t1 $ t2) =>
do_formula (not pos) t1 andalso
(t2 = @{const False} orelse do_formula pos t2)
| (_, @{const Not} $ t1) => do_formula (not pos) t1
@@ -533,22 +583,24 @@
fun all_name_thms_pairs ctxt reserved full_types add_thms chained_ths =
let
- val is_chained = member Thm.eq_thm chained_ths
- val global_facts = PureThy.facts_of (ProofContext.theory_of ctxt)
+ val thy = ProofContext.theory_of ctxt
+ val thy_prefix = Context.theory_name thy ^ Long_Name.separator
+ val global_facts = PureThy.facts_of thy
val local_facts = ProofContext.facts_of ctxt
val named_locals = local_facts |> Facts.dest_static []
+ val is_chained = member Thm.eq_thm chained_ths
(* Unnamed, not chained formulas with schematic variables are omitted,
because they are rejected by the backticks (`...`) parser for some
reason. *)
- fun is_bad_unnamed_local th =
- exists (fn (_, ths) => member Thm.eq_thm ths th) named_locals orelse
- (exists_subterm is_Var (prop_of th) andalso not (is_chained th))
+ fun is_good_unnamed_local th =
+ forall (fn (_, ths) => not (member Thm.eq_thm ths th)) named_locals
+ andalso (not (exists_subterm is_Var (prop_of th)) orelse (is_chained th))
val unnamed_locals =
- local_facts |> Facts.props |> filter_out is_bad_unnamed_local
+ local_facts |> Facts.props |> filter is_good_unnamed_local
|> map (pair "" o single)
val full_space =
- Name_Space.merge (Facts.space_of global_facts, Facts.space_of local_facts);
- fun add_valid_facts foldx facts =
+ Name_Space.merge (Facts.space_of global_facts, Facts.space_of local_facts)
+ fun add_facts global foldx facts =
foldx (fn (name0, ths) =>
if name0 <> "" andalso
forall (not o member Thm.eq_thm add_thms) ths andalso
@@ -559,10 +611,16 @@
I
else
let
+ val base_loc =
+ if not global then Local
+ else if String.isPrefix thy_prefix name0 then Theory
+ else General
val multi = length ths > 1
fun backquotify th =
"`" ^ Print_Mode.setmp [Print_Mode.input]
(Syntax.string_of_term ctxt) (prop_of th) ^ "`"
+ |> String.translate (fn c => if Char.isPrint c then str c else "")
+ |> simplify_spaces
fun check_thms a =
case try (ProofContext.get_thms ctxt) a of
NONE => false
@@ -575,54 +633,48 @@
not (member Thm.eq_thm add_thms th) then
rest
else
- (fn () =>
- (if name0 = "" then
- th |> backquotify
- else
- let
- val name1 = Facts.extern facts name0
- val name2 = Name_Space.extern full_space name0
- in
- case find_first check_thms [name1, name2, name0] of
- SOME name =>
- let
- val name =
- name |> Symtab.defined reserved name ? quote
- in
- if multi then name ^ "(" ^ Int.toString j ^ ")"
- else name
- end
- | NONE => ""
- end, is_chained th), (multi, th)) :: rest)) ths
+ (((fn () =>
+ if name0 = "" then
+ th |> backquotify
+ else
+ let
+ val name1 = Facts.extern facts name0
+ val name2 = Name_Space.extern full_space name0
+ in
+ case find_first check_thms [name1, name2, name0] of
+ SOME name => repair_name reserved multi j name
+ | NONE => ""
+ end), if is_chained th then Chained else base_loc),
+ (multi, th)) :: rest)) ths
#> snd
end)
in
- [] |> add_valid_facts fold local_facts (unnamed_locals @ named_locals)
- |> add_valid_facts Facts.fold_static global_facts global_facts
+ [] |> add_facts false fold local_facts (unnamed_locals @ named_locals)
+ |> add_facts true Facts.fold_static global_facts global_facts
end
(* The single-name theorems go after the multiple-name ones, so that single
names are preferred when both are available. *)
fun name_thm_pairs ctxt respect_no_atp =
- List.partition (fst o snd) #> op @
- #> map (apsnd snd)
+ List.partition (fst o snd) #> op @ #> map (apsnd snd)
#> respect_no_atp ? filter_out (No_ATPs.member ctxt o snd)
(***************************************************************)
(* ATP invocation methods setup *)
(***************************************************************)
-fun relevant_facts full_types relevance_threshold relevance_convergence
- defs_relevant max_new theory_relevant
- (relevance_override as {add, del, only})
+fun relevant_facts full_types (threshold0, threshold1) max_relevant
+ theory_relevant (relevance_override as {add, del, only})
(ctxt, (chained_ths, _)) hyp_ts concl_t =
let
+ val decay = 1.0 - Math.pow ((1.0 - threshold1) / (1.0 - threshold0),
+ 1.0 / Real.fromInt (max_relevant + 1))
val add_thms = maps (ProofContext.get_fact ctxt) add
val reserved = reserved_isar_keyword_table ()
val axioms =
(if only then
- maps ((fn (n, ths) => map (pair n o pair false) ths)
- o name_thms_pair_from_ref ctxt reserved chained_ths) add
+ maps (map (fn ((name, loc), th) => ((K name, loc), (true, th)))
+ o name_thm_pairs_from_ref ctxt reserved chained_ths) add
else
all_name_thms_pairs ctxt reserved full_types add_thms chained_ths)
|> name_thm_pairs ctxt (respect_no_atp andalso not only)
@@ -630,11 +682,14 @@
in
trace_msg (fn () => "Considering " ^ Int.toString (length axioms) ^
" theorems");
- relevance_filter ctxt relevance_threshold relevance_convergence
- defs_relevant max_new theory_relevant relevance_override
- axioms (concl_t :: hyp_ts)
- |> map (apfst (fn f => f ()))
- |> sort_wrt (fst o fst)
+ (if threshold0 > 1.0 orelse threshold0 > threshold1 then
+ []
+ else if threshold0 < 0.0 then
+ axioms
+ else
+ relevance_filter ctxt threshold0 decay max_relevant theory_relevant
+ relevance_override axioms (concl_t :: hyp_ts))
+ |> map (apfst (apfst (fn f => f ()))) |> sort_wrt (fst o fst)
end
end;
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact_minimize.ML Fri Aug 27 09:34:06 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact_minimize.ML Fri Aug 27 09:43:52 2010 +0200
@@ -7,11 +7,12 @@
signature SLEDGEHAMMER_FACT_MINIMIZE =
sig
+ type locality = Sledgehammer_Fact_Filter.locality
type params = Sledgehammer.params
val minimize_theorems :
- params -> int -> int -> Proof.state -> ((string * bool) * thm list) list
- -> ((string * bool) * thm list) list option * string
+ params -> int -> int -> Proof.state -> ((string * locality) * thm list) list
+ -> ((string * locality) * thm list) list option * string
val run_minimize : params -> int -> Facts.ref list -> Proof.state -> unit
end;
@@ -40,24 +41,20 @@
"")
end
-fun test_theorems ({debug, verbose, overlord, atps, full_types,
- relevance_threshold, relevance_convergence,
- defs_relevant, isar_proof, isar_shrink_factor, ...}
- : params)
+fun test_theorems ({debug, verbose, overlord, atps, full_types, isar_proof,
+ isar_shrink_factor, ...} : params)
(prover : prover) explicit_apply timeout subgoal state
- name_thms_pairs =
+ axioms =
let
val _ =
- priority ("Testing " ^ n_theorems (map fst name_thms_pairs) ^ "...")
+ priority ("Testing " ^ n_theorems (map fst axioms) ^ "...")
val params =
{debug = debug, verbose = verbose, overlord = overlord, atps = atps,
full_types = full_types, explicit_apply = explicit_apply,
- relevance_threshold = relevance_threshold,
- relevance_convergence = relevance_convergence,
- max_relevant_per_iter = NONE, theory_relevant = NONE,
- defs_relevant = defs_relevant, isar_proof = isar_proof,
+ relevance_thresholds = (1.01, 1.01), max_relevant = NONE,
+ theory_relevant = NONE, isar_proof = isar_proof,
isar_shrink_factor = isar_shrink_factor, timeout = timeout}
- val axioms = maps (fn (n, ths) => map (pair n) ths) name_thms_pairs
+ val axioms = maps (fn (n, ths) => map (pair n) ths) axioms
val {context = ctxt, facts, goal} = Proof.goal state
val problem =
{subgoal = subgoal, goal = (ctxt, (facts, goal)),
@@ -67,7 +64,7 @@
in
priority (case outcome of
NONE =>
- if length used_thm_names = length name_thms_pairs then
+ if length used_thm_names = length axioms then
"Found proof."
else
"Found proof with " ^ n_theorems used_thm_names ^ "."
@@ -93,10 +90,9 @@
val fudge_msecs = 1000
fun minimize_theorems {atps = [], ...} _ _ _ _ = error "No ATP is set."
- | minimize_theorems
- (params as {debug, atps = atp :: _, full_types, isar_proof,
- isar_shrink_factor, timeout, ...})
- i n state name_thms_pairs =
+ | minimize_theorems (params as {debug, atps = atp :: _, full_types,
+ isar_proof, isar_shrink_factor, timeout, ...})
+ i n state axioms =
let
val thy = Proof.theory_of state
val prover = get_prover_fun thy atp
@@ -106,13 +102,12 @@
val (_, hyp_ts, concl_t) = strip_subgoal goal i
val explicit_apply =
not (forall (Meson.is_fol_term thy)
- (concl_t :: hyp_ts @
- maps (map prop_of o snd) name_thms_pairs))
+ (concl_t :: hyp_ts @ maps (map prop_of o snd) axioms))
fun do_test timeout =
test_theorems params prover explicit_apply timeout i state
val timer = Timer.startRealTimer ()
in
- (case do_test timeout name_thms_pairs of
+ (case do_test timeout axioms of
result as {outcome = NONE, pool, used_thm_names,
conjecture_shape, ...} =>
let
@@ -122,11 +117,11 @@
|> Time.fromMilliseconds
val (min_thms, {proof, axiom_names, ...}) =
sublinear_minimize (do_test new_timeout)
- (filter_used_facts used_thm_names name_thms_pairs) ([], result)
+ (filter_used_facts used_thm_names axioms) ([], result)
val n = length min_thms
val _ = priority (cat_lines
["Minimized: " ^ string_of_int n ^ " theorem" ^ plural_s n] ^
- (case length (filter (snd o fst) min_thms) of
+ (case length (filter (curry (op =) Chained o snd o fst) min_thms) of
0 => ""
| n => " (including " ^ Int.toString n ^ " chained)") ^ ".")
in
@@ -154,15 +149,14 @@
val ctxt = Proof.context_of state
val reserved = reserved_isar_keyword_table ()
val chained_ths = #facts (Proof.goal state)
- val name_thms_pairs =
- map (apfst (fn f => f ())
- o name_thms_pair_from_ref ctxt reserved chained_ths) refs
+ val axioms =
+ maps (map (apsnd single)
+ o name_thm_pairs_from_ref ctxt reserved chained_ths) refs
in
case subgoal_count state of
0 => priority "No subgoal!"
| n =>
- (kill_atps ();
- priority (#2 (minimize_theorems params i n state name_thms_pairs)))
+ (kill_atps (); priority (#2 (minimize_theorems params i n state axioms)))
end
end;
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Fri Aug 27 09:34:06 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Fri Aug 27 09:43:52 2010 +0200
@@ -67,11 +67,9 @@
("verbose", "false"),
("overlord", "false"),
("explicit_apply", "false"),
- ("relevance_threshold", "40"),
- ("relevance_convergence", "31"),
- ("max_relevant_per_iter", "smart"),
+ ("relevance_thresholds", "45 95"),
+ ("max_relevant", "smart"),
("theory_relevant", "smart"),
- ("defs_relevant", "false"),
("isar_proof", "false"),
("isar_shrink_factor", "1")]
@@ -84,7 +82,6 @@
("partial_types", "full_types"),
("implicit_apply", "explicit_apply"),
("theory_irrelevant", "theory_relevant"),
- ("defs_irrelevant", "defs_relevant"),
("no_isar_proof", "isar_proof")]
val params_for_minimize =
@@ -158,6 +155,14 @@
SOME n => n
| NONE => error ("Parameter " ^ quote name ^
" must be assigned an integer value.")
+ fun lookup_int_pair name =
+ case lookup name of
+ NONE => (0, 0)
+ | SOME s => case s |> space_explode " " |> map Int.fromString of
+ [SOME n1, SOME n2] => (n1, n2)
+ | _ => error ("Parameter " ^ quote name ^
+ "must be assigned a pair of integer values \
+ \(e.g., \"60 95\")")
fun lookup_int_option name =
case lookup name of
SOME "smart" => NONE
@@ -168,25 +173,20 @@
val atps = lookup_string "atps" |> space_explode " "
val full_types = lookup_bool "full_types"
val explicit_apply = lookup_bool "explicit_apply"
- val relevance_threshold =
- 0.01 * Real.fromInt (lookup_int "relevance_threshold")
- val relevance_convergence =
- 0.01 * Real.fromInt (lookup_int "relevance_convergence")
- val max_relevant_per_iter = lookup_int_option "max_relevant_per_iter"
+ val relevance_thresholds =
+ lookup_int_pair "relevance_thresholds"
+ |> pairself (fn n => 0.01 * Real.fromInt n)
+ val max_relevant = lookup_int_option "max_relevant"
val theory_relevant = lookup_bool_option "theory_relevant"
- val defs_relevant = lookup_bool "defs_relevant"
val isar_proof = lookup_bool "isar_proof"
val isar_shrink_factor = Int.max (1, lookup_int "isar_shrink_factor")
val timeout = lookup_time "timeout"
in
{debug = debug, verbose = verbose, overlord = overlord, atps = atps,
full_types = full_types, explicit_apply = explicit_apply,
- relevance_threshold = relevance_threshold,
- relevance_convergence = relevance_convergence,
- max_relevant_per_iter = max_relevant_per_iter,
- theory_relevant = theory_relevant, defs_relevant = defs_relevant,
- isar_proof = isar_proof, isar_shrink_factor = isar_shrink_factor,
- timeout = timeout}
+ relevance_thresholds = relevance_thresholds, max_relevant = max_relevant,
+ theory_relevant = theory_relevant, isar_proof = isar_proof,
+ isar_shrink_factor = isar_shrink_factor, timeout = timeout}
end
fun get_params thy = extract_params (default_raw_params thy)
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML Fri Aug 27 09:34:06 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML Fri Aug 27 09:43:52 2010 +0200
@@ -8,19 +8,20 @@
signature SLEDGEHAMMER_PROOF_RECONSTRUCT =
sig
+ type locality = Sledgehammer_Fact_Filter.locality
type minimize_command = string list -> string
val metis_proof_text:
- bool * minimize_command * string * (string * bool) vector * thm * int
- -> string * (string * bool) list
+ bool * minimize_command * string * (string * locality) vector * thm * int
+ -> string * (string * locality) list
val isar_proof_text:
string Symtab.table * bool * int * Proof.context * int list list
- -> bool * minimize_command * string * (string * bool) vector * thm * int
- -> string * (string * bool) list
+ -> bool * minimize_command * string * (string * locality) vector * thm * int
+ -> string * (string * locality) list
val proof_text:
bool -> string Symtab.table * bool * int * Proof.context * int list list
- -> bool * minimize_command * string * (string * bool) vector * thm * int
- -> string * (string * bool) list
+ -> bool * minimize_command * string * (string * locality) vector * thm * int
+ -> string * (string * locality) list
end;
structure Sledgehammer_Proof_Reconstruct : SLEDGEHAMMER_PROOF_RECONSTRUCT =
@@ -68,7 +69,7 @@
Const (@{const_name Ex}, T) $ Abs (s, T', negate_term t')
| negate_term (Const (@{const_name Ex}, T) $ Abs (s, T', t')) =
Const (@{const_name All}, T) $ Abs (s, T', negate_term t')
- | negate_term (@{const "op -->"} $ t1 $ t2) =
+ | negate_term (@{const HOL.implies} $ t1 $ t2) =
@{const "op &"} $ t1 $ negate_term t2
| negate_term (@{const "op &"} $ t1 $ t2) =
@{const "op |"} $ negate_term t1 $ negate_term t2
@@ -234,7 +235,7 @@
fst o Scan.finite Symbol.stopper
(Scan.error (!! (fn _ => raise Fail "unrecognized ATP output")
(parse_lines pool)))
- o explode o strip_spaces
+ o explode o strip_spaces_except_between_ident_chars
(**** INTERPRETATION OF TSTP SYNTAX TREES ****)
@@ -246,18 +247,18 @@
constrained by information from type literals, or by type inference. *)
fun type_from_fo_term tfrees (u as ATerm (a, us)) =
let val Ts = map (type_from_fo_term tfrees) us in
- case strip_prefix_and_undo_ascii type_const_prefix a of
+ case strip_prefix_and_unascii type_const_prefix a of
SOME b => Type (invert_const b, Ts)
| NONE =>
if not (null us) then
raise FO_TERM [u] (* only "tconst"s have type arguments *)
- else case strip_prefix_and_undo_ascii tfree_prefix a of
+ else case strip_prefix_and_unascii tfree_prefix a of
SOME b =>
let val s = "'" ^ b in
TFree (s, AList.lookup (op =) tfrees s |> the_default HOLogic.typeS)
end
| NONE =>
- case strip_prefix_and_undo_ascii tvar_prefix a of
+ case strip_prefix_and_unascii tvar_prefix a of
SOME b => TVar (("'" ^ b, 0), HOLogic.typeS)
| NONE =>
(* Variable from the ATP, say "X1" *)
@@ -267,7 +268,7 @@
(* Type class literal applied to a type. Returns triple of polarity, class,
type. *)
fun type_constraint_from_term pos tfrees (u as ATerm (a, us)) =
- case (strip_prefix_and_undo_ascii class_prefix a,
+ case (strip_prefix_and_unascii class_prefix a,
map (type_from_fo_term tfrees) us) of
(SOME b, [T]) => (pos, b, T)
| _ => raise FO_TERM [u]
@@ -309,7 +310,7 @@
[typ_u, term_u] =>
aux (SOME (type_from_fo_term tfrees typ_u)) extra_us term_u
| _ => raise FO_TERM us
- else case strip_prefix_and_undo_ascii const_prefix a of
+ else case strip_prefix_and_unascii const_prefix a of
SOME "equal" =>
list_comb (Const (@{const_name "op ="}, HOLogic.typeT),
map (aux NONE []) us)
@@ -341,10 +342,10 @@
val ts = map (aux NONE []) (us @ extra_us)
val T = map fastype_of ts ---> HOLogic.typeT
val t =
- case strip_prefix_and_undo_ascii fixed_var_prefix a of
+ case strip_prefix_and_unascii fixed_var_prefix a of
SOME b => Free (b, T)
| NONE =>
- case strip_prefix_and_undo_ascii schematic_var_prefix a of
+ case strip_prefix_and_unascii schematic_var_prefix a of
SOME b => Var ((b, 0), T)
| NONE =>
if is_tptp_variable a then
@@ -575,10 +576,10 @@
String.tokens (fn c => not (Char.isAlphaNum c) andalso c <> #"_")
fun do_line (tag :: num :: "axiom" :: (rest as _ :: _)) =
if tag = "cnf" orelse tag = "fof" then
- (case strip_prefix_and_undo_ascii axiom_prefix (List.last rest) of
+ (case strip_prefix_and_unascii axiom_prefix (List.last rest) of
SOME name =>
if member (op =) rest "file" then
- SOME (name, is_true_for axiom_names name)
+ SOME (name, find_first_in_vector axiom_names name General)
else
axiom_name_at_index num
| NONE => axiom_name_at_index num)
@@ -624,8 +625,8 @@
fun used_facts axiom_names =
used_facts_in_atp_proof axiom_names
- #> List.partition snd
- #> pairself (sort_distinct (string_ord) o map fst)
+ #> List.partition (curry (op =) Chained o snd)
+ #> pairself (sort_distinct (string_ord o pairself fst))
fun metis_proof_text (full_types, minimize_command, atp_proof, axiom_names,
goal, i) =
@@ -633,9 +634,9 @@
val (chained_lemmas, other_lemmas) = used_facts axiom_names atp_proof
val n = Logic.count_prems (prop_of goal)
in
- (metis_line full_types i n other_lemmas ^
- minimize_line minimize_command (other_lemmas @ chained_lemmas),
- map (rpair false) other_lemmas @ map (rpair true) chained_lemmas)
+ (metis_line full_types i n (map fst other_lemmas) ^
+ minimize_line minimize_command (map fst (other_lemmas @ chained_lemmas)),
+ other_lemmas @ chained_lemmas)
end
(** Isar proof construction and manipulation **)
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_translate.ML Fri Aug 27 09:34:06 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_translate.ML Fri Aug 27 09:43:52 2010 +0200
@@ -18,8 +18,8 @@
val tfrees_name : string
val prepare_problem :
Proof.context -> bool -> bool -> bool -> bool -> term list -> term
- -> ((string * bool) * thm) list
- -> string problem * string Symtab.table * int * (string * bool) vector
+ -> ((string * 'a) * thm) list
+ -> string problem * string Symtab.table * int * (string * 'a) vector
end;
structure Sledgehammer_Translate : SLEDGEHAMMER_TRANSLATE =
@@ -39,11 +39,11 @@
(* Freshness almost guaranteed! *)
val sledgehammer_weak_prefix = "Sledgehammer:"
-datatype fol_formula =
- FOLFormula of {name: string,
- kind: kind,
- combformula: (name, combterm) formula,
- ctypes_sorts: typ list}
+type fol_formula =
+ {name: string,
+ kind: kind,
+ combformula: (name, combterm) formula,
+ ctypes_sorts: typ list}
fun mk_anot phi = AConn (ANot, [phi])
fun mk_aconn c phi1 phi2 = AConn (c, [phi1, phi2])
@@ -72,7 +72,7 @@
do_quant bs AExists s T t'
| @{const "op &"} $ t1 $ t2 => do_conn bs AAnd t1 t2
| @{const "op |"} $ t1 $ t2 => do_conn bs AOr t1 t2
- | @{const "op -->"} $ t1 $ t2 => do_conn bs AImplies t1 t2
+ | @{const HOL.implies} $ t1 $ t2 => do_conn bs AImplies t1 t2
| Const (@{const_name "op ="}, Type (_, [@{typ bool}, _])) $ t1 $ t2 =>
do_conn bs AIff t1 t2
| _ => (fn ts => do_term bs (Envir.eta_contract t)
@@ -127,7 +127,7 @@
aux Ts (t0 $ eta_expand Ts t1 1)
| (t0 as @{const "op &"}) $ t1 $ t2 => t0 $ aux Ts t1 $ aux Ts t2
| (t0 as @{const "op |"}) $ t1 $ t2 => t0 $ aux Ts t1 $ aux Ts t2
- | (t0 as @{const "op -->"}) $ t1 $ t2 => t0 $ aux Ts t1 $ aux Ts t2
+ | (t0 as @{const HOL.implies}) $ t1 $ t2 => t0 $ aux Ts t1 $ aux Ts t2
| (t0 as Const (@{const_name "op ="}, Type (_, [@{typ bool}, _])))
$ t1 $ t2 =>
t0 $ aux Ts t1 $ aux Ts t2
@@ -190,15 +190,14 @@
|> kind <> Axiom ? freeze_term
val (combformula, ctypes_sorts) = combformula_for_prop thy t []
in
- FOLFormula {name = name, combformula = combformula, kind = kind,
- ctypes_sorts = ctypes_sorts}
+ {name = name, combformula = combformula, kind = kind,
+ ctypes_sorts = ctypes_sorts}
end
-fun make_axiom ctxt presimp ((name, chained), th) =
+fun make_axiom ctxt presimp ((name, loc), th) =
case make_formula ctxt presimp name Axiom (prop_of th) of
- FOLFormula {combformula = AAtom (CombConst (("c_True", _), _, _)), ...} =>
- NONE
- | formula => SOME ((name, chained), formula)
+ {combformula = AAtom (CombConst (("c_True", _), _, _)), ...} => NONE
+ | formula => SOME ((name, loc), formula)
fun make_conjecture ctxt ts =
let val last = length ts - 1 in
map2 (fn j => make_formula ctxt true (Int.toString j)
@@ -215,7 +214,7 @@
fun count_combformula (AQuant (_, _, phi)) = count_combformula phi
| count_combformula (AConn (_, phis)) = fold count_combformula phis
| count_combformula (AAtom tm) = count_combterm tm
-fun count_fol_formula (FOLFormula {combformula, ...}) =
+fun count_fol_formula ({combformula, ...} : fol_formula) =
count_combformula combformula
val optional_helpers =
@@ -326,13 +325,13 @@
| aux (AAtom tm) = AAtom (fo_term_for_combterm full_types tm)
in aux end
-fun formula_for_axiom full_types (FOLFormula {combformula, ctypes_sorts, ...}) =
+fun formula_for_axiom full_types
+ ({combformula, ctypes_sorts, ...} : fol_formula) =
mk_ahorn (map (formula_for_fo_literal o fo_literal_for_type_literal)
(type_literals_for_types ctypes_sorts))
(formula_for_combformula full_types combformula)
-fun problem_line_for_fact prefix full_types
- (formula as FOLFormula {name, kind, ...}) =
+fun problem_line_for_fact prefix full_types (formula as {name, kind, ...}) =
Fof (prefix ^ ascii_of name, kind, formula_for_axiom full_types formula)
fun problem_line_for_class_rel_clause (ClassRelClause {name, subclass,
@@ -357,11 +356,11 @@
(fo_literal_for_arity_literal conclLit)))
fun problem_line_for_conjecture full_types
- (FOLFormula {name, kind, combformula, ...}) =
+ ({name, kind, combformula, ...} : fol_formula) =
Fof (conjecture_prefix ^ name, kind,
formula_for_combformula full_types combformula)
-fun free_type_literals_for_conjecture (FOLFormula {ctypes_sorts, ...}) =
+fun free_type_literals_for_conjecture ({ctypes_sorts, ...} : fol_formula) =
map fo_literal_for_type_literal (type_literals_for_types ctypes_sorts)
fun problem_line_for_free_type lit =
@@ -407,7 +406,7 @@
16383 (* large number *)
else if full_types then
0
- else case strip_prefix_and_undo_ascii const_prefix s of
+ else case strip_prefix_and_unascii const_prefix s of
SOME s' => num_type_args thy (invert_const s')
| NONE => 0)
| min_arity_of _ _ (SOME the_const_tab) s =
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML Fri Aug 27 09:34:06 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML Fri Aug 27 09:43:52 2010 +0200
@@ -6,10 +6,11 @@
signature SLEDGEHAMMER_UTIL =
sig
- val is_true_for : (string * bool) vector -> string -> bool
+ val find_first_in_vector : (''a * 'b) vector -> ''a -> 'b -> 'b
val plural_s : int -> string
val serial_commas : string -> string list -> string list
- val strip_spaces : string -> string
+ val simplify_spaces : string -> string
+ val strip_spaces_except_between_ident_chars : string -> string
val parse_bool_option : bool -> string -> string -> bool option
val parse_time_option : string -> string -> Time.time option
val scan_integer : string list -> int * string list
@@ -28,8 +29,9 @@
structure Sledgehammer_Util : SLEDGEHAMMER_UTIL =
struct
-fun is_true_for v s =
- Vector.foldl (fn ((s', b'), b) => if s' = s then b' else b) false v
+fun find_first_in_vector vec key default =
+ Vector.foldl (fn ((key', value'), value) =>
+ if key' = key then value' else value) default vec
fun plural_s n = if n = 1 then "" else "s"
@@ -39,24 +41,27 @@
| serial_commas conj [s1, s2, s3] = [s1 ^ ",", s2 ^ ",", conj, s3]
| serial_commas conj (s :: ss) = s ^ "," :: serial_commas conj ss
-fun is_ident_char c = Char.isAlphaNum c orelse c = #"_"
-
-fun strip_spaces_in_list [] = ""
- | strip_spaces_in_list [c1] = if Char.isSpace c1 then "" else str c1
- | strip_spaces_in_list [c1, c2] =
- strip_spaces_in_list [c1] ^ strip_spaces_in_list [c2]
- | strip_spaces_in_list (c1 :: c2 :: c3 :: cs) =
+fun strip_spaces_in_list _ [] = ""
+ | strip_spaces_in_list _ [c1] = if Char.isSpace c1 then "" else str c1
+ | strip_spaces_in_list is_evil [c1, c2] =
+ strip_spaces_in_list is_evil [c1] ^ strip_spaces_in_list is_evil [c2]
+ | strip_spaces_in_list is_evil (c1 :: c2 :: c3 :: cs) =
if Char.isSpace c1 then
- strip_spaces_in_list (c2 :: c3 :: cs)
+ strip_spaces_in_list is_evil (c2 :: c3 :: cs)
else if Char.isSpace c2 then
if Char.isSpace c3 then
- strip_spaces_in_list (c1 :: c3 :: cs)
+ strip_spaces_in_list is_evil (c1 :: c3 :: cs)
else
- str c1 ^ (if forall is_ident_char [c1, c3] then " " else "") ^
- strip_spaces_in_list (c3 :: cs)
+ str c1 ^ (if forall is_evil [c1, c3] then " " else "") ^
+ strip_spaces_in_list is_evil (c3 :: cs)
else
- str c1 ^ strip_spaces_in_list (c2 :: c3 :: cs)
-val strip_spaces = strip_spaces_in_list o String.explode
+ str c1 ^ strip_spaces_in_list is_evil (c2 :: c3 :: cs)
+fun strip_spaces is_evil = strip_spaces_in_list is_evil o String.explode
+
+val simplify_spaces = strip_spaces (K true)
+
+fun is_ident_char c = Char.isAlphaNum c orelse c = #"_"
+val strip_spaces_except_between_ident_chars = strip_spaces is_ident_char
fun parse_bool_option option name s =
(case s of
--- a/src/HOL/Tools/TFL/dcterm.ML Fri Aug 27 09:34:06 2010 +0200
+++ b/src/HOL/Tools/TFL/dcterm.ML Fri Aug 27 09:43:52 2010 +0200
@@ -128,7 +128,7 @@
val dest_neg = dest_monop @{const_name Not}
val dest_pair = dest_binop @{const_name Pair}
val dest_eq = dest_binop @{const_name "op ="}
-val dest_imp = dest_binop @{const_name "op -->"}
+val dest_imp = dest_binop @{const_name HOL.implies}
val dest_conj = dest_binop @{const_name "op &"}
val dest_disj = dest_binop @{const_name "op |"}
val dest_select = dest_binder @{const_name Eps}
--- a/src/HOL/Tools/TFL/usyntax.ML Fri Aug 27 09:34:06 2010 +0200
+++ b/src/HOL/Tools/TFL/usyntax.ML Fri Aug 27 09:43:52 2010 +0200
@@ -159,7 +159,7 @@
fun mk_imp{ant,conseq} =
- let val c = Const(@{const_name "op -->"},HOLogic.boolT --> HOLogic.boolT --> HOLogic.boolT)
+ let val c = Const(@{const_name HOL.implies},HOLogic.boolT --> HOLogic.boolT --> HOLogic.boolT)
in list_comb(c,[ant,conseq])
end;
@@ -247,7 +247,7 @@
fun dest_eq(Const(@{const_name "op ="},_) $ M $ N) = {lhs=M, rhs=N}
| dest_eq _ = raise USYN_ERR "dest_eq" "not an equality";
-fun dest_imp(Const(@{const_name "op -->"},_) $ M $ N) = {ant=M, conseq=N}
+fun dest_imp(Const(@{const_name HOL.implies},_) $ M $ N) = {ant=M, conseq=N}
| dest_imp _ = raise USYN_ERR "dest_imp" "not an implication";
fun dest_forall(Const(@{const_name All},_) $ (a as Abs _)) = fst (dest_abs [] a)
--- a/src/HOL/Tools/cnf_funcs.ML Fri Aug 27 09:34:06 2010 +0200
+++ b/src/HOL/Tools/cnf_funcs.ML Fri Aug 27 09:43:52 2010 +0200
@@ -97,7 +97,7 @@
| is_atom (Const (@{const_name True}, _)) = false
| is_atom (Const (@{const_name "op &"}, _) $ _ $ _) = false
| is_atom (Const (@{const_name "op |"}, _) $ _ $ _) = false
- | is_atom (Const (@{const_name "op -->"}, _) $ _ $ _) = false
+ | is_atom (Const (@{const_name HOL.implies}, _) $ _ $ _) = false
| is_atom (Const (@{const_name "op ="}, Type ("fun", @{typ bool} :: _)) $ _ $ _) = false
| is_atom (Const (@{const_name Not}, _) $ _) = false
| is_atom _ = true;
@@ -198,7 +198,7 @@
in
disj_cong OF [thm1, thm2]
end
- | make_nnf_thm thy (Const (@{const_name "op -->"}, _) $ x $ y) =
+ | make_nnf_thm thy (Const (@{const_name HOL.implies}, _) $ x $ y) =
let
val thm1 = make_nnf_thm thy (HOLogic.Not $ x)
val thm2 = make_nnf_thm thy y
@@ -232,7 +232,7 @@
in
make_nnf_not_disj OF [thm1, thm2]
end
- | make_nnf_thm thy (Const (@{const_name Not}, _) $ (Const (@{const_name "op -->"}, _) $ x $ y)) =
+ | make_nnf_thm thy (Const (@{const_name Not}, _) $ (Const (@{const_name HOL.implies}, _) $ x $ y)) =
let
val thm1 = make_nnf_thm thy x
val thm2 = make_nnf_thm thy (HOLogic.Not $ y)
--- a/src/HOL/Tools/groebner.ML Fri Aug 27 09:34:06 2010 +0200
+++ b/src/HOL/Tools/groebner.ML Fri Aug 27 09:43:52 2010 +0200
@@ -931,7 +931,7 @@
| Const (@{const_name Ex}, _) $ _ => find_body bounds (dest_arg tm)
| Const (@{const_name "op &"}, _) $ _ $ _ => find_args bounds tm
| Const (@{const_name "op |"}, _) $ _ $ _ => find_args bounds tm
- | Const (@{const_name "op -->"}, _) $ _ $ _ => find_args bounds tm
+ | Const (@{const_name HOL.implies}, _) $ _ $ _ => find_args bounds tm
| @{term "op ==>"} $_$_ => find_args bounds tm
| Const("op ==",_)$_$_ => find_args bounds tm
| @{term Trueprop}$_ => find_term bounds (dest_arg tm)
--- a/src/HOL/Tools/hologic.ML Fri Aug 27 09:34:06 2010 +0200
+++ b/src/HOL/Tools/hologic.ML Fri Aug 27 09:43:52 2010 +0200
@@ -210,8 +210,8 @@
val conj = @{term "op &"}
and disj = @{term "op |"}
-and imp = @{term "op -->"}
-and Not = @{term "Not"};
+and imp = @{term implies}
+and Not = @{term Not};
fun mk_conj (t1, t2) = conj $ t1 $ t2
and mk_disj (t1, t2) = disj $ t1 $ t2
@@ -230,7 +230,7 @@
fun disjuncts t = disjuncts_aux t [];
-fun dest_imp (Const ("op -->", _) $ A $ B) = (A, B)
+fun dest_imp (Const ("HOL.implies", _) $ A $ B) = (A, B)
| dest_imp t = raise TERM ("dest_imp", [t]);
fun dest_not (Const ("HOL.Not", _) $ t) = t
--- a/src/HOL/Tools/meson.ML Fri Aug 27 09:34:06 2010 +0200
+++ b/src/HOL/Tools/meson.ML Fri Aug 27 09:43:52 2010 +0200
@@ -274,7 +274,7 @@
| signed_nclauses b (Const(@{const_name "op |"},_) $ t $ u) =
if b then prod (signed_nclauses b t) (signed_nclauses b u)
else sum (signed_nclauses b t) (signed_nclauses b u)
- | signed_nclauses b (Const(@{const_name "op -->"},_) $ t $ u) =
+ | signed_nclauses b (Const(@{const_name HOL.implies},_) $ t $ u) =
if b then prod (signed_nclauses (not b) t) (signed_nclauses b u)
else sum (signed_nclauses (not b) t) (signed_nclauses b u)
| signed_nclauses b (Const(@{const_name "op ="}, Type ("fun", [T, _])) $ t $ u) =
@@ -401,7 +401,7 @@
since this code expects to be called on a clause form.*)
val is_conn = member (op =)
[@{const_name Trueprop}, @{const_name "op &"}, @{const_name "op |"},
- @{const_name "op -->"}, @{const_name Not},
+ @{const_name HOL.implies}, @{const_name Not},
@{const_name All}, @{const_name Ex}, @{const_name Ball}, @{const_name Bex}];
(*True if the term contains a function--not a logical connective--where the type
--- a/src/HOL/Tools/quickcheck_generators.ML Fri Aug 27 09:34:06 2010 +0200
+++ b/src/HOL/Tools/quickcheck_generators.ML Fri Aug 27 09:43:52 2010 +0200
@@ -342,7 +342,7 @@
val bound_max = length Ts - 1;
val bounds = map_index (fn (i, ty) =>
(2 * (bound_max - i) + 1, 2 * (bound_max - i), 2 * i, ty)) Ts;
- fun strip_imp (Const(@{const_name "op -->"},_) $ A $ B) = apfst (cons A) (strip_imp B)
+ fun strip_imp (Const(@{const_name HOL.implies},_) $ A $ B) = apfst (cons A) (strip_imp B)
| strip_imp A = ([], A)
val prop' = betapplys (prop, map (fn (i, _, _, _) => Bound i) bounds);
val terms = HOLogic.mk_list @{typ term} (map (fn (_, i, _, _) => Bound i $ @{term "()"}) bounds)
--- a/src/HOL/Tools/refute.ML Fri Aug 27 09:34:06 2010 +0200
+++ b/src/HOL/Tools/refute.ML Fri Aug 27 09:43:52 2010 +0200
@@ -650,7 +650,7 @@
| Const (@{const_name "op ="}, _) => t
| Const (@{const_name "op &"}, _) => t
| Const (@{const_name "op |"}, _) => t
- | Const (@{const_name "op -->"}, _) => t
+ | Const (@{const_name HOL.implies}, _) => t
(* sets *)
| Const (@{const_name Collect}, _) => t
| Const (@{const_name Set.member}, _) => t
@@ -826,7 +826,7 @@
| Const (@{const_name "op ="}, T) => collect_type_axioms T axs
| Const (@{const_name "op &"}, _) => axs
| Const (@{const_name "op |"}, _) => axs
- | Const (@{const_name "op -->"}, _) => axs
+ | Const (@{const_name HOL.implies}, _) => axs
(* sets *)
| Const (@{const_name Collect}, T) => collect_type_axioms T axs
| Const (@{const_name Set.member}, T) => collect_type_axioms T axs
@@ -1895,7 +1895,7 @@
(* this would make "undef" propagate, even for formulae like *)
(* "True | undef": *)
(* SOME (Node [Node [TT, TT], Node [TT, FF]], model, args) *)
- | Const (@{const_name "op -->"}, _) $ t1 $ t2 => (* similar to "==>" (Pure) *)
+ | Const (@{const_name HOL.implies}, _) $ t1 $ t2 => (* similar to "==>" (Pure) *)
(* 3-valued logic *)
let
val (i1, m1, a1) = interpret thy model args t1
@@ -1905,9 +1905,9 @@
in
SOME (Leaf [fmTrue, fmFalse], m2, a2)
end
- | Const (@{const_name "op -->"}, _) $ t1 =>
+ | Const (@{const_name HOL.implies}, _) $ t1 =>
SOME (interpret thy model args (eta_expand t 1))
- | Const (@{const_name "op -->"}, _) =>
+ | Const (@{const_name HOL.implies}, _) =>
SOME (interpret thy model args (eta_expand t 2))
(* this would make "undef" propagate, even for formulae like *)
(* "False --> undef": *)
--- a/src/HOL/Tools/simpdata.ML Fri Aug 27 09:34:06 2010 +0200
+++ b/src/HOL/Tools/simpdata.ML Fri Aug 27 09:43:52 2010 +0200
@@ -14,7 +14,7 @@
| dest_eq _ = NONE;
fun dest_conj ((c as Const(@{const_name "op &"},_)) $ s $ t) = SOME (c, s, t)
| dest_conj _ = NONE;
- fun dest_imp ((c as Const(@{const_name "op -->"},_)) $ s $ t) = SOME (c, s, t)
+ fun dest_imp ((c as Const(@{const_name HOL.implies},_)) $ s $ t) = SOME (c, s, t)
| dest_imp _ = NONE;
val conj = HOLogic.conj
val imp = HOLogic.imp
@@ -159,7 +159,7 @@
(Scan.succeed "Clasimp.clasimpset_of (ML_Context.the_local_context ())");
val mksimps_pairs =
- [(@{const_name "op -->"}, [@{thm mp}]),
+ [(@{const_name HOL.implies}, [@{thm mp}]),
(@{const_name "op &"}, [@{thm conjunct1}, @{thm conjunct2}]),
(@{const_name All}, [@{thm spec}]),
(@{const_name True}, []),
--- a/src/HOL/ex/Meson_Test.thy Fri Aug 27 09:34:06 2010 +0200
+++ b/src/HOL/ex/Meson_Test.thy Fri Aug 27 09:43:52 2010 +0200
@@ -10,7 +10,7 @@
below and constants declared in HOL!
*}
-hide_const (open) subset quotient union inter sum
+hide_const (open) implies union inter subset sum quotient
text {*
Test data for the MESON proof procedure
--- a/src/HOL/ex/Numeral.thy Fri Aug 27 09:34:06 2010 +0200
+++ b/src/HOL/ex/Numeral.thy Fri Aug 27 09:43:52 2010 +0200
@@ -1033,14 +1033,14 @@
(SML "IntInf.- ((_), 1)")
(OCaml "Big'_int.pred'_big'_int")
(Haskell "!(_/ -/ 1)")
- (Scala "!(_/ -/ 1)")
+ (Scala "!(_ -/ 1)")
(Eval "!(_/ -/ 1)")
code_const Int.succ
(SML "IntInf.+ ((_), 1)")
(OCaml "Big'_int.succ'_big'_int")
(Haskell "!(_/ +/ 1)")
- (Scala "!(_/ +/ 1)")
+ (Scala "!(_ +/ 1)")
(Eval "!(_/ +/ 1)")
code_const "op + \<Colon> int \<Rightarrow> int \<Rightarrow> int"
--- a/src/HOL/ex/SVC_Oracle.thy Fri Aug 27 09:34:06 2010 +0200
+++ b/src/HOL/ex/SVC_Oracle.thy Fri Aug 27 09:43:52 2010 +0200
@@ -90,7 +90,7 @@
(*abstraction of a formula*)
and fm ((c as Const(@{const_name "op &"}, _)) $ p $ q) = c $ (fm p) $ (fm q)
| fm ((c as Const(@{const_name "op |"}, _)) $ p $ q) = c $ (fm p) $ (fm q)
- | fm ((c as Const(@{const_name "op -->"}, _)) $ p $ q) = c $ (fm p) $ (fm q)
+ | fm ((c as Const(@{const_name HOL.implies}, _)) $ p $ q) = c $ (fm p) $ (fm q)
| fm ((c as Const(@{const_name Not}, _)) $ p) = c $ (fm p)
| fm ((c as Const(@{const_name True}, _))) = c
| fm ((c as Const(@{const_name False}, _))) = c
--- a/src/HOL/ex/svc_funcs.ML Fri Aug 27 09:34:06 2010 +0200
+++ b/src/HOL/ex/svc_funcs.ML Fri Aug 27 09:43:52 2010 +0200
@@ -91,7 +91,7 @@
in case c of
Const(@{const_name "op &"}, _) => apply c (map tag ts)
| Const(@{const_name "op |"}, _) => apply c (map tag ts)
- | Const(@{const_name "op -->"}, _) => apply c (map tag ts)
+ | Const(@{const_name HOL.implies}, _) => apply c (map tag ts)
| Const(@{const_name Not}, _) => apply c (map tag ts)
| Const(@{const_name True}, _) => (c, false)
| Const(@{const_name False}, _) => (c, false)
@@ -187,7 +187,7 @@
Buildin("AND", [fm pos p, fm pos q])
| fm pos (Const(@{const_name "op |"}, _) $ p $ q) =
Buildin("OR", [fm pos p, fm pos q])
- | fm pos (Const(@{const_name "op -->"}, _) $ p $ q) =
+ | fm pos (Const(@{const_name HOL.implies}, _) $ p $ q) =
Buildin("=>", [fm (not pos) p, fm pos q])
| fm pos (Const(@{const_name Not}, _) $ p) =
Buildin("NOT", [fm (not pos) p])
--- a/src/Pure/General/markup.ML Fri Aug 27 09:34:06 2010 +0200
+++ b/src/Pure/General/markup.ML Fri Aug 27 09:43:52 2010 +0200
@@ -99,6 +99,8 @@
val command_spanN: string val command_span: string -> T
val ignored_spanN: string val ignored_span: T
val malformed_spanN: string val malformed_span: T
+ val subgoalsN: string
+ val proof_stateN: string val proof_state: int -> T
val stateN: string val state: T
val subgoalN: string val subgoal: T
val sendbackN: string val sendback: T
@@ -156,16 +158,13 @@
fun markup_int elem prop = (elem, fn i => (elem, [(prop, print_int i)]): T);
-(* name *)
+(* misc properties *)
val nameN = "name";
fun name a = properties [(nameN, a)];
val (bindingN, binding) = markup_string "binding" nameN;
-
-(* kind *)
-
val kindN = "kind";
@@ -305,6 +304,9 @@
(* toplevel *)
+val subgoalsN = "subgoals";
+val (proof_stateN, proof_state) = markup_int "proof_state" subgoalsN;
+
val (stateN, state) = markup_elem "state";
val (subgoalN, subgoal) = markup_elem "subgoal";
val (sendbackN, sendback) = markup_elem "sendback";
--- a/src/Pure/General/markup.scala Fri Aug 27 09:34:06 2010 +0200
+++ b/src/Pure/General/markup.scala Fri Aug 27 09:43:52 2010 +0200
@@ -9,7 +9,7 @@
object Markup
{
- /* integers */
+ /* plain values */
object Int {
def apply(i: scala.Int): String = i.toString
@@ -26,25 +26,33 @@
}
- /* property values */
-
- def get_string(name: String, props: List[(String, String)]): Option[String] =
- props.find(p => p._1 == name).map(_._2)
+ /* named properties */
- def get_long(name: String, props: List[(String, String)]): Option[scala.Long] =
+ class Property(val name: String)
{
- get_string(name, props) match {
- case None => None
- case Some(Long(i)) => Some(i)
- }
+ def apply(value: String): List[(String, String)] = List((name, value))
+ def unapply(props: List[(String, String)]): Option[String] =
+ props.find(_._1 == name).map(_._2)
}
- def get_int(name: String, props: List[(String, String)]): Option[scala.Int] =
+ class Int_Property(name: String)
{
- get_string(name, props) match {
- case None => None
- case Some(Int(i)) => Some(i)
- }
+ def apply(value: scala.Int): List[(String, String)] = List((name, Int(value)))
+ def unapply(props: List[(String, String)]): Option[Int] =
+ props.find(_._1 == name) match {
+ case None => None
+ case Some((_, value)) => Int.unapply(value)
+ }
+ }
+
+ class Long_Property(name: String)
+ {
+ def apply(value: scala.Long): List[(String, String)] = List((name, Long(value)))
+ def unapply(props: List[(String, String)]): Option[Long] =
+ props.find(_._1 == name) match {
+ case None => None
+ case Some((_, value)) => Long.unapply(value)
+ }
}
@@ -53,7 +61,7 @@
val Empty = Markup("", Nil)
- /* name */
+ /* misc properties */
val NAME = "name"
val KIND = "kind"
@@ -86,9 +94,9 @@
/* pretty printing */
- val INDENT = "indent"
+ val Indent = new Int_Property("indent")
val BLOCK = "block"
- val WIDTH = "width"
+ val Width = new Int_Property("width")
val BREAK = "break"
@@ -188,6 +196,9 @@
/* toplevel */
+ val SUBGOALS = "subgoals"
+ val PROOF_STATE = "proof_state"
+
val STATE = "state"
val SUBGOAL = "subgoal"
val SENDBACK = "sendback"
--- a/src/Pure/General/position.scala Fri Aug 27 09:34:06 2010 +0200
+++ b/src/Pure/General/position.scala Fri Aug 27 09:43:52 2010 +0200
@@ -11,22 +11,21 @@
{
type T = List[(String, String)]
- def get_line(pos: T): Option[Int] = Markup.get_int(Markup.LINE, pos)
- def get_column(pos: T): Option[Int] = Markup.get_int(Markup.COLUMN, pos)
- def get_offset(pos: T): Option[Int] = Markup.get_int(Markup.OFFSET, pos)
- def get_end_line(pos: T): Option[Int] = Markup.get_int(Markup.END_LINE, pos)
- def get_end_column(pos: T): Option[Int] = Markup.get_int(Markup.END_COLUMN, pos)
- def get_end_offset(pos: T): Option[Int] = Markup.get_int(Markup.END_OFFSET, pos)
- def get_file(pos: T): Option[String] = Markup.get_string(Markup.FILE, pos)
- def get_id(pos: T): Option[Long] = Markup.get_long(Markup.ID, pos)
+ val Line = new Markup.Int_Property(Markup.LINE)
+ val End_Line = new Markup.Int_Property(Markup.END_LINE)
+ val Offset = new Markup.Int_Property(Markup.OFFSET)
+ val End_Offset = new Markup.Int_Property(Markup.END_OFFSET)
+ val File = new Markup.Property(Markup.FILE)
+ val Id = new Markup.Long_Property(Markup.ID)
- def get_range(pos: T): Option[Text.Range] =
- (get_offset(pos), get_end_offset(pos)) match {
- case (Some(start), Some(stop)) if start <= stop => Some(Text.Range(start, stop))
- case (Some(start), None) => Some(Text.Range(start))
- case (_, _) => None
- }
-
- object Id { def unapply(pos: T): Option[Long] = get_id(pos) }
- object Range { def unapply(pos: T): Option[Text.Range] = get_range(pos) }
+ object Range
+ {
+ def apply(range: Text.Range): T = Offset(range.start) ++ Offset(range.stop)
+ def unapply(pos: T): Option[Text.Range] =
+ (Offset.unapply(pos), End_Offset.unapply(pos)) match {
+ case (Some(start), Some(stop)) if start <= stop => Some(Text.Range(start, stop))
+ case (Some(start), None) => Some(Text.Range(start))
+ case _ => None
+ }
+ }
}
--- a/src/Pure/General/pretty.scala Fri Aug 27 09:34:06 2010 +0200
+++ b/src/Pure/General/pretty.scala Fri Aug 27 09:43:52 2010 +0200
@@ -19,12 +19,11 @@
object Block
{
def apply(i: Int, body: XML.Body): XML.Tree =
- XML.Elem(Markup(Markup.BLOCK, List((Markup.INDENT, Markup.Int(i)))), body)
+ XML.Elem(Markup(Markup.BLOCK, Markup.Indent(i)), body)
def unapply(tree: XML.Tree): Option[(Int, XML.Body)] =
tree match {
- case XML.Elem(
- Markup(Markup.BLOCK, List((Markup.INDENT, Markup.Int(i)))), body) => Some((i, body))
+ case XML.Elem(Markup(Markup.BLOCK, Markup.Indent(i)), body) => Some((i, body))
case _ => None
}
}
@@ -32,12 +31,11 @@
object Break
{
def apply(w: Int): XML.Tree =
- XML.Elem(
- Markup(Markup.BREAK, List((Markup.WIDTH, Markup.Int(w)))), List(XML.Text(Symbol.spaces(w))))
+ XML.Elem(Markup(Markup.BREAK, Markup.Width(w)), List(XML.Text(Symbol.spaces(w))))
def unapply(tree: XML.Tree): Option[Int] =
tree match {
- case XML.Elem(Markup(Markup.BREAK, List((Markup.WIDTH, Markup.Int(w)))), _) => Some(w)
+ case XML.Elem(Markup(Markup.BREAK, Markup.Width(w)), _) => Some(w)
case _ => None
}
}
--- a/src/Pure/Isar/locale.ML Fri Aug 27 09:34:06 2010 +0200
+++ b/src/Pure/Isar/locale.ML Fri Aug 27 09:43:52 2010 +0200
@@ -483,7 +483,7 @@
val thy' = (change_locale loc o apsnd) (cons ((name, (morph, export)), serial ())) thy;
val context' = Context.Theory thy';
val (_, regs) = fold_rev (roundup thy' cons export)
- (all_registrations context') (get_idents (context'), []);
+ (registrations_of context' loc) (get_idents (context'), []);
in
thy'
|> fold_rev (fn dep => Context.theory_map (add_registration dep NONE export)) regs
--- a/src/Pure/Isar/proof.ML Fri Aug 27 09:34:06 2010 +0200
+++ b/src/Pure/Isar/proof.ML Fri Aug 27 09:43:52 2010 +0200
@@ -42,6 +42,7 @@
val raw_goal: state -> {context: context, facts: thm list, goal: thm}
val goal: state -> {context: context, facts: thm list, goal: thm}
val simple_goal: state -> {context: context, goal: thm}
+ val status_markup: state -> Markup.T
val let_bind: (term list * term) list -> state -> state
val let_bind_cmd: (string list * string) list -> state -> state
val write: Syntax.mode -> (term * mixfix) list -> state -> state
@@ -520,6 +521,11 @@
val (ctxt, (_, goal)) = get_goal (refine_insert facts state);
in {context = ctxt, goal = goal} end;
+fun status_markup state =
+ (case try goal state of
+ SOME {goal, ...} => Markup.proof_state (Thm.nprems_of goal)
+ | NONE => Markup.empty);
+
(*** structured proof commands ***)
--- a/src/Pure/Isar/toplevel.ML Fri Aug 27 09:34:06 2010 +0200
+++ b/src/Pure/Isar/toplevel.ML Fri Aug 27 09:43:52 2010 +0200
@@ -563,13 +563,6 @@
fun status tr m =
setmp_thread_position tr (fn () => Output.status (Markup.markup m "")) ();
-fun async_state (tr as Transition {print, ...}) st =
- if print then
- ignore
- (Future.fork (fn () =>
- setmp_thread_position tr (fn () => Future.status (fn () => print_state false st)) ()))
- else ();
-
fun error_msg tr exn_info =
setmp_thread_position tr (fn () =>
Output.error_msg (ML_Compiler.exn_message (EXCURSION_FAIL exn_info))) ();
@@ -628,6 +621,22 @@
(* managed execution *)
+local
+
+fun async_state (tr as Transition {print, ...}) st =
+ if print then
+ ignore
+ (Future.fork (fn () =>
+ setmp_thread_position tr (fn () => Future.status (fn () => print_state false st)) ()))
+ else ();
+
+fun proof_status tr st =
+ (case try proof_of st of
+ SOME prf => status tr (Proof.status_markup prf)
+ | NONE => ());
+
+in
+
fun run_command thy_name tr st =
(case
(case init_of tr of
@@ -637,13 +646,18 @@
let val int = is_some (init_of tr) in
(case transition int tr st of
SOME (st', NONE) =>
- (status tr Markup.finished; if int then () else async_state tr st'; SOME st')
+ (status tr Markup.finished;
+ proof_status tr st';
+ if int then () else async_state tr st';
+ SOME st')
| SOME (_, SOME (exn as Exn.Interrupt, _)) => reraise exn
| SOME (_, SOME exn_info) => (error_msg tr exn_info; status tr Markup.failed; NONE)
| NONE => (error_msg tr (TERMINATE, at_command tr); status tr Markup.failed; NONE))
end
| Exn.Exn exn => (error_msg tr (exn, at_command tr); status tr Markup.failed; NONE));
+end;
+
(* nested commands *)
--- a/src/Pure/ML/ml_compiler_polyml-5.3.ML Fri Aug 27 09:34:06 2010 +0200
+++ b/src/Pure/ML/ml_compiler_polyml-5.3.ML Fri Aug 27 09:43:52 2010 +0200
@@ -44,13 +44,18 @@
fun report_parse_tree depth space =
let
+ val report_text =
+ (case Context.thread_data () of
+ SOME (Context.Proof ctxt) => Context_Position.report_text ctxt
+ | _ => Position.report_text);
+
fun report_decl markup loc decl =
- Position.report_text Markup.ML_ref (position_of loc)
+ report_text Markup.ML_ref (position_of loc)
(Markup.markup (Markup.properties (Position.properties_of (position_of decl)) markup) "");
fun report loc (PolyML.PTtype types) =
PolyML.NameSpace.displayTypeExpression (types, depth, space)
|> pretty_ml |> Pretty.from_ML |> Pretty.string_of
- |> Position.report_text Markup.ML_typing (position_of loc)
+ |> report_text Markup.ML_typing (position_of loc)
| report loc (PolyML.PTdeclaredAt decl) = report_decl Markup.ML_def loc decl
| report loc (PolyML.PTopenedAt decl) = report_decl Markup.ML_open loc decl
| report loc (PolyML.PTstructureAt decl) = report_decl Markup.ML_struct loc decl
--- a/src/Pure/ML/ml_context.ML Fri Aug 27 09:34:06 2010 +0200
+++ b/src/Pure/ML/ml_context.ML Fri Aug 27 09:43:52 2010 +0200
@@ -166,7 +166,9 @@
fun eval verbose pos ants =
let
(*prepare source text*)
- val ((env, body), env_ctxt) = eval_antiquotes (ants, pos) (Context.thread_data ());
+ val ((env, body), env_ctxt) =
+ eval_antiquotes (ants, pos) (Context.thread_data ())
+ ||> Option.map (Context.mapping I (Context_Position.set_visible false));
val _ =
if ! trace then tracing (cat_lines [ML_Lex.flatten env, ML_Lex.flatten body])
else ();
--- a/src/Pure/PIDE/command.scala Fri Aug 27 09:34:06 2010 +0200
+++ b/src/Pure/PIDE/command.scala Fri Aug 27 09:43:52 2010 +0200
@@ -46,11 +46,11 @@
case XML.Elem(Markup(Markup.REPORT, _), msgs) =>
(this /: msgs)((state, msg) =>
msg match {
- case XML.Elem(Markup(name, atts), args)
- if Position.get_id(atts) == Some(command.id) && Position.get_range(atts).isDefined =>
- val range = command.decode(Position.get_range(atts).get)
+ case XML.Elem(Markup(name, atts @ Position.Range(range)), args)
+ if Position.Id.unapply(atts) == Some(command.id) =>
val props = atts.filterNot(p => Markup.POSITION_PROPERTIES(p._1))
- val info = Text.Info[Any](range, XML.Elem(Markup(name, props), args))
+ val info =
+ Text.Info[Any](command.decode(range), XML.Elem(Markup(name, props), args))
state.add_markup(info)
case _ => System.err.println("Ignored report message: " + msg); state
})
--- a/src/Pure/PIDE/markup_tree.scala Fri Aug 27 09:34:06 2010 +0200
+++ b/src/Pure/PIDE/markup_tree.scala Fri Aug 27 09:43:52 2010 +0200
@@ -115,7 +115,10 @@
if (last < stop) parent.restrict(Text.Range(last, stop)) #:: nexts
else nexts
- case Nil => Stream(Text.Info(Text.Range(last, root_range.stop), default))
+ case Nil =>
+ val stop = root_range.stop
+ if (last < stop) Stream(Text.Info(Text.Range(last, stop), default))
+ else Stream.empty
}
}
stream(root_range.start, List((Text.Info(root_range, default), overlapping(root_range))))
--- a/src/Pure/PIDE/text.scala Fri Aug 27 09:34:06 2010 +0200
+++ b/src/Pure/PIDE/text.scala Fri Aug 27 09:43:52 2010 +0200
@@ -33,7 +33,7 @@
def +(i: Offset): Range = map(_ + i)
def -(i: Offset): Range = map(_ - i)
- def is_singleton: Boolean = start == stop
+ def is_singularity: Boolean = start == stop
def contains(i: Offset): Boolean = start == i || start < i && i < stop
def contains(that: Range): Boolean = this.contains(that.start) && that.stop <= this.stop
--- a/src/Pure/System/session.scala Fri Aug 27 09:34:06 2010 +0200
+++ b/src/Pure/System/session.scala Fri Aug 27 09:43:52 2010 +0200
@@ -131,15 +131,15 @@
{
raw_protocol.event(result)
- Position.get_id(result.properties) match {
- case Some(state_id) =>
+ result.properties match {
+ case Position.Id(state_id) =>
try {
val (st, state) = global_state.accumulate(state_id, result.message)
global_state = state
indicate_command_change(st.command)
}
catch { case _: Document.State.Fail => bad_result(result) }
- case None =>
+ case _ =>
if (result.is_status) {
result.body match {
case List(Isar_Document.Assign(id, edits)) =>
--- a/src/Tools/Code/code_haskell.ML Fri Aug 27 09:34:06 2010 +0200
+++ b/src/Tools/Code/code_haskell.ML Fri Aug 27 09:43:52 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
@@ -344,11 +342,9 @@
contr_classparam_typs
(if string_classes then deriving_show else K false);
fun print_module name content =
- (name, Pretty.chunks [
+ (name, Pretty.chunks2 [
str ("module " ^ name ^ " where {"),
- str "",
content,
- str "",
str "}"
]);
fun serialize_module1 (module_name', (deps, (stmts, _))) =
--- a/src/Tools/Code/code_ml.ML Fri Aug 27 09:34:06 2010 +0200
+++ b/src/Tools/Code/code_ml.ML Fri Aug 27 09:43:52 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*)
@@ -948,8 +946,8 @@
(** for instrumentalization **)
fun evaluation_code_of thy target struct_name =
- Code_Target.serialize_custom thy (target, fn _ => fn [] =>
- serialize_ml target print_sml_module print_sml_stmt (SOME struct_name) true);
+ Code_Target.serialize_custom thy (target, fn module_name => fn [] =>
+ serialize_ml target print_sml_module print_sml_stmt module_name true) (SOME struct_name);
(** Isar setup **)
--- a/src/Tools/Code/code_printer.ML Fri Aug 27 09:34:06 2010 +0200
+++ b/src/Tools/Code/code_printer.ML Fri Aug 27 09:43:52 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);
--- a/src/Tools/Code/code_scala.ML Fri Aug 27 09:34:06 2010 +0200
+++ b/src/Tools/Code/code_scala.ML Fri Aug 27 09:43:52 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;
@@ -135,7 +135,7 @@
fun print_context tyvars vs name = applify "[" "]"
(fn (v, sort) => (Pretty.block o map str)
(lookup_tyvar tyvars v :: maps (fn sort => [": ", deresolve sort]) sort))
- NOBR ((str o deresolve) name) vs;
+ NOBR ((str o deresolve_base) name) vs;
fun print_defhead tyvars vars name vs params tys ty =
Pretty.block [str "def ", constraint (applify "(" ")" (fn (param, ty) =>
constraint ((str o lookup_var vars) param) (print_typ tyvars NOBR ty))
@@ -194,7 +194,8 @@
str "match", str "{"], str "}")
(map print_clause eqs)
end;
- val print_method = (str o Library.enclose "`" "+`" o deresolve_base);
+ val print_method = str o Library.enclose "`" "`" o space_implode "+"
+ 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))) =
@@ -240,7 +241,7 @@
in
concat [str "def", constraint (Pretty.block [applify "(" ")"
(fn (aux, ty) => constraint ((str o lookup_var vars) aux)
- (print_typ tyvars NOBR ty)) NOBR (add_typarg (deresolve classparam))
+ (print_typ tyvars NOBR ty)) NOBR (add_typarg (deresolve_base classparam))
(auxs ~~ tys), str "(implicit ", str implicit_name, str ": ",
add_typarg (deresolve name), str ")"]) (print_typ tyvars NOBR ty), str "=",
applify "(" ")" (str o lookup_var vars) NOBR
@@ -281,67 +282,137 @@
end;
in print_stmt end;
-fun scala_program_of_program labelled_name module_name reserved raw_module_alias program =
+local
+
+(* hierarchical module name space *)
+
+datatype node =
+ Dummy
+ | Stmt of Code_Thingol.stmt
+ | Module of ((Name.context * Name.context) * Name.context) * (string list * (string * node) Graph.T);
+
+in
+
+fun scala_program_of_program labelled_name reserved module_alias program =
let
- val the_module_name = the_default "Program" module_name;
- val module_alias = K (SOME the_module_name);
- val reserved = Name.make_context reserved;
- fun prepare_stmt (name, stmt) (nsps, stmts) =
+
+ (* building module name hierarchy *)
+ 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))
+ (Long_Name.explode name);
+ val module_names = Graph.fold (insert (op =) o fst o dest_name o fst) program [];
+ val fragments_tab = fold (fn name => Symtab.update
+ (name, alias_fragments name)) module_names Symtab.empty;
+ val dest_name = Code_Printer.dest_name #>> (the o Symtab.lookup fragments_tab);
+
+ (* building empty module hierarchy *)
+ val empty_module = (((reserved, reserved), reserved), ([], Graph.empty));
+ fun map_module f (Module content) = Module (f content);
+ fun declare_module name_fragement ((nsp_class, nsp_object), nsp_common) =
let
- val (_, base) = Code_Printer.dest_name name;
- val mk_name_stmt = yield_singleton Name.variants;
- fun add_class ((nsp_class, nsp_object), nsp_common) =
- let
- val (base', nsp_class') = mk_name_stmt base nsp_class
- in (base', ((nsp_class', nsp_object), Name.declare base' nsp_common)) end;
- fun add_object ((nsp_class, nsp_object), nsp_common) =
- let
- val (base', nsp_object') = mk_name_stmt base nsp_object
- in (base', ((nsp_class, nsp_object'), Name.declare base' nsp_common)) end;
- fun add_common upper ((nsp_class, nsp_object), nsp_common) =
+ val declare = Name.declare name_fragement;
+ in ((declare nsp_class, declare nsp_object), declare nsp_common) end;
+ fun ensure_module name_fragement (nsps, (implicits, nodes)) =
+ if can (Graph.get_node nodes) name_fragement then (nsps, (implicits, nodes))
+ else
+ (nsps |> declare_module name_fragement, (implicits,
+ nodes |> Graph.new_node (name_fragement, (name_fragement, Module empty_module))));
+ fun allocate_module [] = I
+ | allocate_module (name_fragment :: name_fragments) =
+ ensure_module name_fragment
+ #> (apsnd o apsnd o Graph.map_node name_fragment o apsnd o map_module o allocate_module) name_fragments;
+ val empty_program = Symtab.fold (fn (_, fragments) => allocate_module fragments)
+ fragments_tab empty_module;
+ fun change_module [] = I
+ | change_module (name_fragment :: name_fragments) =
+ apsnd o apsnd o Graph.map_node name_fragment o apsnd o map_module
+ o change_module name_fragments;
+
+ (* statement declaration *)
+ fun namify_class base ((nsp_class, nsp_object), nsp_common) =
+ let
+ val (base', nsp_class') = yield_singleton Name.variants base nsp_class
+ in (base', ((nsp_class', nsp_object), Name.declare base' nsp_common)) end;
+ fun namify_object base ((nsp_class, nsp_object), nsp_common) =
+ let
+ val (base', nsp_object') = yield_singleton Name.variants base nsp_object
+ in (base', ((nsp_class, nsp_object'), Name.declare base' nsp_common)) end;
+ fun namify_common upper base ((nsp_class, nsp_object), nsp_common) =
+ let
+ val (base', nsp_common') =
+ yield_singleton Name.variants (if upper then first_upper base else base) nsp_common
+ in
+ (base',
+ ((Name.declare base' nsp_class, Name.declare base' nsp_object), nsp_common'))
+ end;
+ fun declare_stmt name stmt =
+ let
+ val (name_fragments, base) = dest_name name;
+ val namify = case stmt
+ of Code_Thingol.Fun _ => namify_object
+ | Code_Thingol.Datatype _ => namify_class
+ | Code_Thingol.Datatypecons _ => namify_common true
+ | Code_Thingol.Class _ => namify_class
+ | Code_Thingol.Classrel _ => namify_object
+ | Code_Thingol.Classparam _ => namify_object
+ | Code_Thingol.Classinst _ => namify_common false;
+ val stmt' = case stmt
+ of Code_Thingol.Datatypecons _ => Dummy
+ | Code_Thingol.Classrel _ => Dummy
+ | Code_Thingol.Classparam _ => Dummy
+ | _ => Stmt stmt;
+ fun is_classinst stmt = case stmt
+ of Code_Thingol.Classinst _ => true
+ | _ => false;
+ val implicit_deps = filter (is_classinst o Graph.get_node program)
+ (Graph.imm_succs program name);
+ fun declaration (nsps, (implicits, nodes)) =
let
- val (base', nsp_common') =
- mk_name_stmt (if upper then first_upper base else base) nsp_common
- in
- (base',
- ((Name.declare base' nsp_class, Name.declare base' nsp_object), nsp_common'))
- end;
- val add_name = case stmt
- of Code_Thingol.Fun _ => add_object
- | Code_Thingol.Datatype _ => add_class
- | Code_Thingol.Datatypecons _ => add_common true
- | Code_Thingol.Class _ => add_class
- | Code_Thingol.Classrel _ => add_object
- | Code_Thingol.Classparam _ => add_object
- | Code_Thingol.Classinst _ => add_common false;
- fun add_stmt base' = case stmt
- of Code_Thingol.Datatypecons _ => cons (name, (base', NONE))
- | Code_Thingol.Classrel _ => cons (name, (base', NONE))
- | Code_Thingol.Classparam _ => cons (name, (base', NONE))
- | _ => cons (name, (base', SOME stmt));
- in
- nsps
- |> add_name
- |-> (fn base' => rpair (add_stmt base' stmts))
- end;
- val stmts = AList.make (Graph.get_node program) (Graph.strong_conn program |> flat)
- |> filter_out (Code_Thingol.is_case o snd);
- val (_, sca_program) = fold prepare_stmt stmts (((reserved, reserved), reserved), []);
- fun deresolver name = (fst o the o AList.lookup (op =) sca_program) name
- handle Option => error ("Unknown statement name: " ^ labelled_name name);
- in (deresolver, (the_module_name, sca_program)) end;
+ val (base', nsps') = namify base nsps;
+ val implicits' = union (op =) implicit_deps implicits;
+ val nodes' = Graph.new_node (name, (base', stmt')) nodes;
+ in (nsps', (implicits', nodes')) end;
+ in change_module name_fragments declaration end;
+
+ (* dependencies *)
+ fun add_dependency name name' =
+ let
+ val (name_fragments, base) = dest_name name;
+ val (name_fragments', base') = dest_name name';
+ val (name_fragments_common, (diff, diff')) =
+ chop_prefix (op =) (name_fragments, name_fragments');
+ val dep = if null diff then (name, name') else (hd diff, hd diff')
+ in (change_module name_fragments_common o apsnd o apsnd) (Graph.add_edge dep) end;
+
+ (* producing program *)
+ val (_, (_, sca_program)) = empty_program
+ |> Graph.fold (fn (name, (stmt, _)) => declare_stmt name stmt) program
+ |> Graph.fold (fn (name, (_, (_, names))) => fold (add_dependency name) names) program;
-fun serialize_scala raw_module_name labelled_name
- raw_reserved includes raw_module_alias
+ (* deresolving *)
+ fun deresolve name =
+ let
+ val (name_fragments, _) = dest_name name;
+ val nodes = fold (fn name_fragement => fn nodes => case Graph.get_node nodes name_fragement
+ of (_, Module (_, (_, nodes))) => nodes) name_fragments sca_program;
+ val (base', _) = Graph.get_node nodes name;
+ in Long_Name.implode (name_fragments @ [base']) end
+ handle Graph.UNDEF _ => error ("Unknown statement name: " ^ labelled_name name);
+
+ in (deresolve, 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 destination =
+ 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";
+
+ (* preprocess program *)
val reserved = fold (insert (op =) o fst) includes raw_reserved;
- val (deresolver, (the_module_name, sca_program)) = scala_program_of_program labelled_name
- module_name reserved raw_module_alias program;
- val reserved = make_vars reserved;
+ val (deresolve, sca_program) = scala_program_of_program labelled_name
+ (Name.make_context reserved) module_alias program;
+
+ (* print statements *)
fun lookup_constr tyco constr = case Graph.get_node program tyco
of Code_Thingol.Datatype (_, (_, constrs)) =>
the (AList.lookup (op = o apsnd fst) constrs constr);
@@ -359,44 +430,49 @@
of Code_Thingol.Datatypecons (_, tyco) => null (lookup_constr tyco c)
| _ => false;
val print_stmt = print_scala_stmt labelled_name syntax_tyco syntax_const
- reserved args_num is_singleton_constr deresolver;
- fun print_module name imports content =
- (name, Pretty.chunks (
- str ("object " ^ name ^ " {")
- :: (if null imports then []
- else str "" :: map (fn name => str ("import " ^ name ^ "._")) imports)
- @ [str "",
- content,
- str "",
- str "}"]
- ));
- fun serialize_module the_module_name sca_program =
+ (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_implicit implicit =
let
- val content = Pretty.chunks2 (map_filter
- (fn (name, (_, SOME stmt)) => SOME (print_stmt (name, stmt))
- | (_, (_, NONE)) => NONE) sca_program);
- in print_module the_module_name (map fst includes) content end;
- fun check_destination destination =
- (File.check destination; destination);
- fun write_module destination (modlname, content) =
- let
- val filename = case modlname
- of "" => Path.explode "Main.scala"
- | _ => (Path.ext "scala" 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 (code_of_pretty content) end
+ val s = deresolve implicit;
+ in if length (Long_Name.explode s) = 1 then NONE else SOME (str s) end;
+ fun print_implicits implicits = case map_filter print_implicit implicits
+ of [] => NONE
+ | ps => (SOME o Pretty.block)
+ (str "import /*implicits*/" :: Pretty.brk 1 :: commas ps);
+ fun print_module base implicits p = Pretty.chunks2
+ ([str ("object " ^ base ^ " {")] @ the_list (print_implicits implicits)
+ @ [p, str ("} /* object " ^ base ^ " */")]);
+ fun print_node (_, Dummy) = NONE
+ | print_node (name, Stmt stmt) = if null presentation_stmt_names
+ orelse member (op =) presentation_stmt_names name
+ then SOME (print_stmt (name, stmt))
+ else NONE
+ | print_node (name, Module (_, (implicits, nodes))) = if null presentation_stmt_names
+ then case print_nodes nodes
+ of NONE => NONE
+ | SOME p => SOME (print_module (Long_Name.base_name name) implicits p)
+ else print_nodes nodes
+ and print_nodes nodes = let
+ val ps = map_filter (fn name => print_node (name,
+ snd (Graph.get_node nodes name)))
+ ((rev o flat o Graph.strong_conn) nodes);
+ in if null ps then NONE else SOME (Pretty.chunks2 ps) end;
+
+ (* serialization *)
+ 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));
in
Code_Target.mk_serialization target
- (fn NONE => K () o map (code_writeln o snd) | SOME file => K () o map
- (write_module (check_destination file)))
- (rpair [] o cat_lines o map (code_of_pretty o snd))
- (map (fn (name, content) => print_module name [] content) includes
- @| serialize_module the_module_name sca_program)
- destination
+ (fn NONE => code_writeln | SOME file => File.write file o code_of_pretty)
+ (rpair [] o code_of_pretty) p destination
end;
+end; (*local*)
+
val literals = let
fun char_scala c = if c = "'" then "\\'"
else if c = "\"" then "\\\""
@@ -412,8 +488,8 @@
literal_char = Library.enclose "'" "'" o char_scala,
literal_string = quote o translate_string char_scala,
literal_numeral = fn k => "BigInt(" ^ numeral_scala k ^ ")",
- literal_positive_numeral = fn k => "Nat(" ^ numeral_scala k ^ ")",
- literal_alternative_numeral = fn k => "Natural(" ^ numeral_scala k ^ ")",
+ literal_positive_numeral = fn k => "Nat.Nat(" ^ numeral_scala k ^ ")",
+ literal_alternative_numeral = fn k => "Natural.Nat(" ^ numeral_scala k ^ ")",
literal_naive_numeral = fn k => "BigInt(" ^ numeral_scala k ^ ")",
literal_list = fn [] => str "Nil" | ps => Pretty.block [str "List", enum "," "(" ")" ps],
infix_cons = (6, "::")
@@ -422,17 +498,17 @@
(** 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
(target, { serializer = isar_serializer, literals = literals,
- check = { env_var = "SCALA_HOME", make_destination = I,
+ check = { env_var = "SCALA_HOME", make_destination = fn p => Path.append p (Path.explode "ROOT.scala"),
make_command = fn scala_home => fn p => fn _ =>
"export JAVA_OPTS='-Xms128m -Xmx512m -Xss2m' && "
- ^ Path.implode (Path.append (Path.explode scala_home) (Path.explode "bin/scalac")) ^ " *.scala" } })
+ ^ Path.implode (Path.append (Path.explode scala_home) (Path.explode "bin/scalac")) ^ " " ^ File.shell_path p } })
#> Code_Target.add_syntax_tyco target "fun"
(SOME (2, fn print_typ => fn fxy => fn [ty1, ty2] =>
brackify_infix (1, R) fxy (
--- a/src/Tools/Code/code_target.ML Fri Aug 27 09:34:06 2010 +0200
+++ b/src/Tools/Code/code_target.ML Fri Aug 27 09:43:52 2010 +0200
@@ -28,7 +28,7 @@
-> 'a -> serialization
val serialize: theory -> string -> int option -> string option -> Token.T list
-> Code_Thingol.naming -> Code_Thingol.program -> string list -> serialization
- val serialize_custom: theory -> string * serializer
+ 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
@@ -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
@@ -344,8 +348,8 @@
else Cache_IO.with_tmp_dir "Code_Test" (ext_check env_param)
end;
-fun serialize_custom thy (target_name, seri) naming program names =
- mount_serializer thy (SOME seri) target_name NONE NONE [] naming program names (String [])
+fun serialize_custom thy (target_name, seri) module_name naming program names =
+ mount_serializer thy (SOME seri) target_name NONE module_name [] naming program names (String [])
|> the;
end; (* local *)
--- a/src/Tools/jEdit/src/jedit/isabelle_hyperlinks.scala Fri Aug 27 09:34:06 2010 +0200
+++ b/src/Tools/jEdit/src/jedit/isabelle_hyperlinks.scala Fri Aug 27 09:43:52 2010 +0200
@@ -55,11 +55,11 @@
val Text.Range(begin, end) = snapshot.convert(info_range + command_start)
val line = buffer.getLineOfOffset(begin)
- (Position.get_file(props), Position.get_line(props)) match {
+ (Position.File.unapply(props), Position.Line.unapply(props)) match {
case (Some(ref_file), Some(ref_line)) =>
new External_Hyperlink(begin, end, line, ref_file, ref_line)
case _ =>
- (Position.get_id(props), Position.get_offset(props)) match {
+ (Position.Id.unapply(props), Position.Offset.unapply(props)) match {
case (Some(ref_id), Some(ref_offset)) =>
snapshot.lookup_command(ref_id) match {
case Some(ref_cmd) =>