1.1 --- a/NEWS Fri Aug 27 09:34:06 2010 +0200
1.2 +++ b/NEWS Fri Aug 27 09:43:52 2010 +0200
1.3 @@ -104,6 +104,7 @@
1.4 Trueprop ~> HOL.Trueprop
1.5 True ~> HOL.True
1.6 False ~> HOL.False
1.7 + op --> ~> HOL.implies
1.8 Not ~> HOL.Not
1.9 The ~> HOL.The
1.10 All ~> HOL.All
2.1 --- a/doc-src/Sledgehammer/sledgehammer.tex Fri Aug 27 09:34:06 2010 +0200
2.2 +++ b/doc-src/Sledgehammer/sledgehammer.tex Fri Aug 27 09:43:52 2010 +0200
2.3 @@ -447,33 +447,29 @@
2.4 \label{relevance-filter}
2.5
2.6 \begin{enum}
2.7 -\opdefault{relevance\_threshold}{int}{40}
2.8 -Specifies the threshold above which facts are considered relevant by the
2.9 -relevance filter. The option ranges from 0 to 100, where 0 means that all
2.10 -theorems are relevant.
2.11 +\opdefault{relevance\_thresholds}{int\_pair}{45~95}
2.12 +Specifies the thresholds above which facts are considered relevant by the
2.13 +relevance filter. The first threshold is used for the first iteration of the
2.14 +relevance filter and the second threshold is used for the last iteration (if it
2.15 +is reached). The effective threshold is quadratically interpolated for the other
2.16 +iterations. Each threshold ranges from 0 to 100, where 0 means that all theorems
2.17 +are relevant and 100 only theorems that refer to previously seen constants.
2.18
2.19 -\opdefault{relevance\_convergence}{int}{31}
2.20 -Specifies the convergence factor, expressed as a percentage, used by the
2.21 -relevance filter. This factor is used by the relevance filter to scale down the
2.22 -relevance of facts at each iteration of the filter.
2.23 -
2.24 -\opdefault{max\_relevant\_per\_iter}{int\_or\_smart}{\textit{smart}}
2.25 -Specifies the maximum number of facts that may be added during one iteration of
2.26 -the relevance filter. If the option is set to \textit{smart}, it is set to a
2.27 -value that was empirically found to be appropriate for the ATP. A typical value
2.28 -would be 50.
2.29 +\opdefault{max\_relevant}{int\_or\_smart}{\textit{smart}}
2.30 +Specifies the maximum number of facts that may be returned by the relevance
2.31 +filter. If the option is set to \textit{smart}, it is set to a value that was
2.32 +empirically found to be appropriate for the ATP. A typical value would be 300.
2.33
2.34 \opsmartx{theory\_relevant}{theory\_irrelevant}
2.35 Specifies whether the theory from which a fact comes should be taken into
2.36 consideration by the relevance filter. If the option is set to \textit{smart},
2.37 -it is taken to be \textit{true} for SPASS and \textit{false} for E and Vampire,
2.38 -because empirical results suggest that these are the best settings.
2.39 +it is taken to be \textit{true} for SPASS and \textit{false} for the other ATPs;
2.40 +empirical results suggest that these are the best settings.
2.41
2.42 -\opfalse{defs\_relevant}{defs\_irrelevant}
2.43 -Specifies whether the definition of constants occurring in the formula to prove
2.44 -should be considered particularly relevant. Enabling this option tends to lead
2.45 -to larger problems and typically slows down the ATPs.
2.46 -
2.47 +%\opfalse{defs\_relevant}{defs\_irrelevant}
2.48 +%Specifies whether the definition of constants occurring in the formula to prove
2.49 +%should be considered particularly relevant. Enabling this option tends to lead
2.50 +%to larger problems and typically slows down the ATPs.
2.51 \end{enum}
2.52
2.53 \subsection{Output Format}
3.1 --- a/src/HOL/Boogie/Tools/boogie_loader.ML Fri Aug 27 09:34:06 2010 +0200
3.2 +++ b/src/HOL/Boogie/Tools/boogie_loader.ML Fri Aug 27 09:43:52 2010 +0200
3.3 @@ -504,7 +504,7 @@
3.4 in
3.5 Const (@{const_name If}, [@{typ bool}, T, T] ---> T) $ c $ t1 $ t2
3.6 end) ||
3.7 - binexp "implies" (binop @{term "op -->"}) ||
3.8 + binexp "implies" (binop @{term HOL.implies}) ||
3.9 scan_line "distinct" num :|-- scan_count exp >>
3.10 (fn [] => @{term True}
3.11 | ts as (t :: _) => mk_distinct (Term.fastype_of t) ts) ||
4.1 --- a/src/HOL/Boogie/Tools/boogie_tactics.ML Fri Aug 27 09:34:06 2010 +0200
4.2 +++ b/src/HOL/Boogie/Tools/boogie_tactics.ML Fri Aug 27 09:43:52 2010 +0200
4.3 @@ -53,7 +53,7 @@
4.4 fun explode_conj (@{term "op &"} $ t $ u) = explode_conj t @ explode_conj u
4.5 | explode_conj t = [t]
4.6
4.7 - fun splt (ts, @{term "op -->"} $ t $ u) = splt (ts @ explode_conj t, u)
4.8 + fun splt (ts, @{term HOL.implies} $ t $ u) = splt (ts @ explode_conj t, u)
4.9 | splt (ts, @{term "op &"} $ t $ u) = splt (ts, t) @ splt (ts, u)
4.10 | splt (ts, @{term assert_at} $ _ $ t) = [(ts, t)]
4.11 | splt (_, @{term True}) = []
5.1 --- a/src/HOL/Boogie/Tools/boogie_vcs.ML Fri Aug 27 09:34:06 2010 +0200
5.2 +++ b/src/HOL/Boogie/Tools/boogie_vcs.ML Fri Aug 27 09:43:52 2010 +0200
5.3 @@ -59,8 +59,8 @@
5.4 fun vc_of @{term True} = NONE
5.5 | vc_of (@{term assert_at} $ Free (n, _) $ t) =
5.6 SOME (Assert ((n, t), True))
5.7 - | vc_of (@{term "op -->"} $ @{term True} $ u) = vc_of u
5.8 - | vc_of (@{term "op -->"} $ t $ u) =
5.9 + | vc_of (@{term HOL.implies} $ @{term True} $ u) = vc_of u
5.10 + | vc_of (@{term HOL.implies} $ t $ u) =
5.11 vc_of u |> Option.map (assume t)
5.12 | vc_of (@{term "op &"} $ (@{term assert_at} $ Free (n, _) $ t) $ u) =
5.13 SOME (vc_of u |> the_default True |> assert (n, t))
5.14 @@ -76,7 +76,7 @@
5.15 let
5.16 fun mk_conj t u = @{term "op &"} $ t $ u
5.17
5.18 - fun term_of (Assume (t, v)) = @{term "op -->"} $ t $ term_of v
5.19 + fun term_of (Assume (t, v)) = @{term HOL.implies} $ t $ term_of v
5.20 | term_of (Assert ((n, t), v)) =
5.21 mk_conj (@{term assert_at} $ Free (n, @{typ bool}) $ t) (term_of v)
5.22 | term_of (Ignore v) = term_of v
6.1 --- a/src/HOL/Decision_Procs/Approximation.thy Fri Aug 27 09:34:06 2010 +0200
6.2 +++ b/src/HOL/Decision_Procs/Approximation.thy Fri Aug 27 09:43:52 2010 +0200
6.3 @@ -3422,7 +3422,7 @@
6.4
6.5 ML {*
6.6 fun calculated_subterms (@{const Trueprop} $ t) = calculated_subterms t
6.7 - | calculated_subterms (@{const "op -->"} $ _ $ t) = calculated_subterms t
6.8 + | calculated_subterms (@{const HOL.implies} $ _ $ t) = calculated_subterms t
6.9 | calculated_subterms (@{term "op <= :: real \<Rightarrow> real \<Rightarrow> bool"} $ t1 $ t2) = [t1, t2]
6.10 | calculated_subterms (@{term "op < :: real \<Rightarrow> real \<Rightarrow> bool"} $ t1 $ t2) = [t1, t2]
6.11 | calculated_subterms (@{term "op : :: real \<Rightarrow> real set \<Rightarrow> bool"} $ t1 $
7.1 --- a/src/HOL/Decision_Procs/Cooper.thy Fri Aug 27 09:34:06 2010 +0200
7.2 +++ b/src/HOL/Decision_Procs/Cooper.thy Fri Aug 27 09:43:52 2010 +0200
7.3 @@ -1956,7 +1956,7 @@
7.4 @{code And} (fm_of_term ps vs t1, fm_of_term ps vs t2)
7.5 | fm_of_term ps vs (@{term "op |"} $ t1 $ t2) =
7.6 @{code Or} (fm_of_term ps vs t1, fm_of_term ps vs t2)
7.7 - | fm_of_term ps vs (@{term "op -->"} $ t1 $ t2) =
7.8 + | fm_of_term ps vs (@{term HOL.implies} $ t1 $ t2) =
7.9 @{code Imp} (fm_of_term ps vs t1, fm_of_term ps vs t2)
7.10 | fm_of_term ps vs (@{term "Not"} $ t') =
7.11 @{code NOT} (fm_of_term ps vs t')
7.12 @@ -2016,7 +2016,7 @@
7.13
7.14 fun term_bools acc t =
7.15 let
7.16 - val is_op = member (op =) [@{term "op &"}, @{term "op |"}, @{term "op -->"}, @{term "op = :: bool => _"},
7.17 + val is_op = member (op =) [@{term "op &"}, @{term "op |"}, @{term HOL.implies}, @{term "op = :: bool => _"},
7.18 @{term "op = :: int => _"}, @{term "op < :: int => _"},
7.19 @{term "op <= :: int => _"}, @{term "Not"}, @{term "All :: (int => _) => _"},
7.20 @{term "Ex :: (int => _) => _"}, @{term "True"}, @{term "False"}]
8.1 --- a/src/HOL/Decision_Procs/Ferrack.thy Fri Aug 27 09:34:06 2010 +0200
8.2 +++ b/src/HOL/Decision_Procs/Ferrack.thy Fri Aug 27 09:43:52 2010 +0200
8.3 @@ -1998,7 +1998,7 @@
8.4 @{code Iff} (fm_of_term vs t1, fm_of_term vs t2)
8.5 | fm_of_term vs (@{term "op &"} $ t1 $ t2) = @{code And} (fm_of_term vs t1, fm_of_term vs t2)
8.6 | fm_of_term vs (@{term "op |"} $ t1 $ t2) = @{code Or} (fm_of_term vs t1, fm_of_term vs t2)
8.7 - | fm_of_term vs (@{term "op -->"} $ t1 $ t2) = @{code Imp} (fm_of_term vs t1, fm_of_term vs t2)
8.8 + | fm_of_term vs (@{term HOL.implies} $ t1 $ t2) = @{code Imp} (fm_of_term vs t1, fm_of_term vs t2)
8.9 | fm_of_term vs (@{term "Not"} $ t') = @{code NOT} (fm_of_term vs t')
8.10 | fm_of_term vs (Const (@{const_name Ex}, _) $ Abs (xn, xT, p)) =
8.11 @{code E} (fm_of_term (("", dummyT) :: vs) p)
9.1 --- a/src/HOL/Decision_Procs/MIR.thy Fri Aug 27 09:34:06 2010 +0200
9.2 +++ b/src/HOL/Decision_Procs/MIR.thy Fri Aug 27 09:43:52 2010 +0200
9.3 @@ -5841,7 +5841,7 @@
9.4 @{code And} (fm_of_term vs t1, fm_of_term vs t2)
9.5 | fm_of_term vs (@{term "op |"} $ t1 $ t2) =
9.6 @{code Or} (fm_of_term vs t1, fm_of_term vs t2)
9.7 - | fm_of_term vs (@{term "op -->"} $ t1 $ t2) =
9.8 + | fm_of_term vs (@{term HOL.implies} $ t1 $ t2) =
9.9 @{code Imp} (fm_of_term vs t1, fm_of_term vs t2)
9.10 | fm_of_term vs (@{term "Not"} $ t') =
9.11 @{code NOT} (fm_of_term vs t')
10.1 --- a/src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy Fri Aug 27 09:34:06 2010 +0200
10.2 +++ b/src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy Fri Aug 27 09:43:52 2010 +0200
10.3 @@ -2956,7 +2956,7 @@
10.4 val nott = @{term "Not"};
10.5 val conjt = @{term "op &"};
10.6 val disjt = @{term "op |"};
10.7 -val impt = @{term "op -->"};
10.8 +val impt = @{term HOL.implies};
10.9 val ifft = @{term "op = :: bool => _"}
10.10 fun llt rT = Const(@{const_name Orderings.less},rrT rT);
10.11 fun lle rT = Const(@{const_name Orderings.less},rrT rT);
10.12 @@ -3020,7 +3020,7 @@
10.13 | Const(@{const_name Not},_)$p => @{code NOT} (fm_of_term m m' p)
10.14 | Const(@{const_name "op &"},_)$p$q => @{code And} (fm_of_term m m' p, fm_of_term m m' q)
10.15 | Const(@{const_name "op |"},_)$p$q => @{code Or} (fm_of_term m m' p, fm_of_term m m' q)
10.16 - | Const(@{const_name "op -->"},_)$p$q => @{code Imp} (fm_of_term m m' p, fm_of_term m m' q)
10.17 + | Const(@{const_name HOL.implies},_)$p$q => @{code Imp} (fm_of_term m m' p, fm_of_term m m' q)
10.18 | Const(@{const_name "op ="},ty)$p$q =>
10.19 if domain_type ty = bT then @{code Iff} (fm_of_term m m' p, fm_of_term m m' q)
10.20 else @{code Eq} (@{code Sub} (tm_of_term m m' p, tm_of_term m m' q))
11.1 --- a/src/HOL/Decision_Procs/ferrante_rackoff.ML Fri Aug 27 09:34:06 2010 +0200
11.2 +++ b/src/HOL/Decision_Procs/ferrante_rackoff.ML Fri Aug 27 09:43:52 2010 +0200
11.3 @@ -183,7 +183,7 @@
11.4 | Const (@{const_name Ex}, _) $ _ => find_body bounds (Thm.dest_arg tm)
11.5 | Const (@{const_name "op &"}, _) $ _ $ _ => find_args bounds tm
11.6 | Const (@{const_name "op |"}, _) $ _ $ _ => find_args bounds tm
11.7 - | Const (@{const_name "op -->"}, _) $ _ $ _ => find_args bounds tm
11.8 + | Const (@{const_name HOL.implies}, _) $ _ $ _ => find_args bounds tm
11.9 | Const ("==>", _) $ _ $ _ => find_args bounds tm
11.10 | Const ("==", _) $ _ $ _ => find_args bounds tm
11.11 | Const ("all", _) $ _ => find_body bounds (Thm.dest_arg tm)
12.1 --- a/src/HOL/Decision_Procs/langford.ML Fri Aug 27 09:34:06 2010 +0200
12.2 +++ b/src/HOL/Decision_Procs/langford.ML Fri Aug 27 09:43:52 2010 +0200
12.3 @@ -185,7 +185,7 @@
12.4 | Const (@{const_name Ex}, _) $ _ => find_body bounds (Thm.dest_arg tm)
12.5 | Const (@{const_name "op &"}, _) $ _ $ _ => find_args bounds tm
12.6 | Const (@{const_name "op |"}, _) $ _ $ _ => find_args bounds tm
12.7 - | Const (@{const_name "op -->"}, _) $ _ $ _ => find_args bounds tm
12.8 + | Const (@{const_name HOL.implies}, _) $ _ $ _ => find_args bounds tm
12.9 | Const ("==>", _) $ _ $ _ => find_args bounds tm
12.10 | Const ("==", _) $ _ $ _ => find_args bounds tm
12.11 | Const (@{const_name Trueprop}, _) $ _ => h bounds (Thm.dest_arg tm)
13.1 --- a/src/HOL/HOL.thy Fri Aug 27 09:34:06 2010 +0200
13.2 +++ b/src/HOL/HOL.thy Fri Aug 27 09:43:52 2010 +0200
13.3 @@ -56,13 +56,13 @@
13.4 True :: bool
13.5 False :: bool
13.6 Not :: "bool => bool" ("~ _" [40] 40)
13.7 + implies :: "[bool, bool] => bool" (infixr "-->" 25)
13.8
13.9 setup Sign.root_path
13.10
13.11 consts
13.12 "op &" :: "[bool, bool] => bool" (infixr "&" 35)
13.13 "op |" :: "[bool, bool] => bool" (infixr "|" 30)
13.14 - "op -->" :: "[bool, bool] => bool" (infixr "-->" 25)
13.15
13.16 "op =" :: "['a, 'a] => bool" (infixl "=" 50)
13.17
13.18 @@ -91,7 +91,7 @@
13.19 Not ("\<not> _" [40] 40) and
13.20 "op &" (infixr "\<and>" 35) and
13.21 "op |" (infixr "\<or>" 30) and
13.22 - "op -->" (infixr "\<longrightarrow>" 25) and
13.23 + HOL.implies (infixr "\<longrightarrow>" 25) and
13.24 not_equal (infix "\<noteq>" 50)
13.25
13.26 notation (HTML output)
13.27 @@ -184,7 +184,7 @@
13.28
13.29 finalconsts
13.30 "op ="
13.31 - "op -->"
13.32 + HOL.implies
13.33 The
13.34
13.35 definition If :: "bool \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'a" ("(if (_)/ then (_)/ else (_))" [0, 0, 10] 10) where
13.36 @@ -1924,7 +1924,7 @@
13.37 (Haskell "True" and "False" and "not"
13.38 and infixl 3 "&&" and infixl 2 "||"
13.39 and "!(if (_)/ then (_)/ else (_))")
13.40 - (Scala "true" and "false" and "'!/ _"
13.41 + (Scala "true" and "false" and "'! _"
13.42 and infixl 3 "&&" and infixl 1 "||"
13.43 and "!(if ((_))/ (_)/ else (_))")
13.44
14.1 --- a/src/HOL/Imperative_HOL/Array.thy Fri Aug 27 09:34:06 2010 +0200
14.2 +++ b/src/HOL/Imperative_HOL/Array.thy Fri Aug 27 09:43:52 2010 +0200
14.3 @@ -484,11 +484,11 @@
14.4
14.5 code_type array (Scala "!collection.mutable.ArraySeq[_]")
14.6 code_const Array (Scala "!error(\"bare Array\")")
14.7 -code_const Array.new' (Scala "('_: Unit)/ => / Array.alloc((_))((_))")
14.8 -code_const Array.make' (Scala "('_: Unit)/ =>/ Array.make((_))((_))")
14.9 -code_const Array.len' (Scala "('_: Unit)/ =>/ Array.len((_))")
14.10 -code_const Array.nth' (Scala "('_: Unit)/ =>/ Array.nth((_), (_))")
14.11 -code_const Array.upd' (Scala "('_: Unit)/ =>/ Array.upd((_), (_), (_))")
14.12 -code_const Array.freeze (Scala "('_: Unit)/ =>/ Array.freeze((_))")
14.13 +code_const Array.new' (Scala "('_: Unit)/ => / Heap.Array.alloc((_))((_))")
14.14 +code_const Array.make' (Scala "('_: Unit)/ =>/ Heap.Array.make((_))((_))")
14.15 +code_const Array.len' (Scala "('_: Unit)/ =>/ Heap.Array.len((_))")
14.16 +code_const Array.nth' (Scala "('_: Unit)/ =>/ Heap.Array.nth((_), (_))")
14.17 +code_const Array.upd' (Scala "('_: Unit)/ =>/ Heap.Array.upd((_), (_), (_))")
14.18 +code_const Array.freeze (Scala "('_: Unit)/ =>/ Heap.Array.freeze((_))")
14.19
14.20 end
15.1 --- a/src/HOL/Imperative_HOL/Heap_Monad.thy Fri Aug 27 09:34:06 2010 +0200
15.2 +++ b/src/HOL/Imperative_HOL/Heap_Monad.thy Fri Aug 27 09:43:52 2010 +0200
15.3 @@ -478,7 +478,6 @@
15.4
15.5 code_include Scala "Heap"
15.6 {*import collection.mutable.ArraySeq
15.7 -import Natural._
15.8
15.9 def bind[A, B](f: Unit => A, g: A => Unit => B): Unit => B = (_: Unit) => g (f ()) ()
15.10
15.11 @@ -487,24 +486,33 @@
15.12 }
15.13
15.14 object Ref {
15.15 - def apply[A](x: A): Ref[A] = new Ref[A](x)
15.16 - def lookup[A](r: Ref[A]): A = r.value
15.17 - def update[A](r: Ref[A], x: A): Unit = { r.value = x }
15.18 + def apply[A](x: A): Ref[A] =
15.19 + new Ref[A](x)
15.20 + def lookup[A](r: Ref[A]): A =
15.21 + r.value
15.22 + def update[A](r: Ref[A], x: A): Unit =
15.23 + { r.value = x }
15.24 }
15.25
15.26 object Array {
15.27 - def alloc[A](n: Natural)(x: A): ArraySeq[A] = ArraySeq.fill(n.as_Int)(x)
15.28 - def make[A](n: Natural)(f: Natural => A): ArraySeq[A] = ArraySeq.tabulate(n.as_Int)((k: Int) => f(Natural(k)))
15.29 - def len[A](a: ArraySeq[A]): Natural = Natural(a.length)
15.30 - def nth[A](a: ArraySeq[A], n: Natural): A = a(n.as_Int)
15.31 - def upd[A](a: ArraySeq[A], n: Natural, x: A): Unit = a.update(n.as_Int, x)
15.32 - def freeze[A](a: ArraySeq[A]): List[A] = a.toList
15.33 + def alloc[A](n: Natural.Nat)(x: A): ArraySeq[A] =
15.34 + ArraySeq.fill(n.as_Int)(x)
15.35 + def make[A](n: Natural.Nat)(f: Natural.Nat => A): ArraySeq[A] =
15.36 + ArraySeq.tabulate(n.as_Int)((k: Int) => f(Natural.Nat(k)))
15.37 + def len[A](a: ArraySeq[A]): Natural.Nat =
15.38 + Natural.Nat(a.length)
15.39 + def nth[A](a: ArraySeq[A], n: Natural.Nat): A =
15.40 + a(n.as_Int)
15.41 + def upd[A](a: ArraySeq[A], n: Natural.Nat, x: A): Unit =
15.42 + a.update(n.as_Int, x)
15.43 + def freeze[A](a: ArraySeq[A]): List[A] =
15.44 + a.toList
15.45 }*}
15.46
15.47 code_reserved Scala bind Ref Array
15.48
15.49 code_type Heap (Scala "Unit/ =>/ _")
15.50 -code_const bind (Scala "bind")
15.51 +code_const bind (Scala "Heap.bind")
15.52 code_const return (Scala "('_: Unit)/ =>/ _")
15.53 code_const Heap_Monad.raise' (Scala "!error((_))")
15.54
16.1 --- a/src/HOL/Imperative_HOL/Ref.thy Fri Aug 27 09:34:06 2010 +0200
16.2 +++ b/src/HOL/Imperative_HOL/Ref.thy Fri Aug 27 09:43:52 2010 +0200
16.3 @@ -306,10 +306,10 @@
16.4
16.5 text {* Scala *}
16.6
16.7 -code_type ref (Scala "!Ref[_]")
16.8 +code_type ref (Scala "!Heap.Ref[_]")
16.9 code_const Ref (Scala "!error(\"bare Ref\")")
16.10 -code_const ref' (Scala "('_: Unit)/ =>/ Ref((_))")
16.11 -code_const Ref.lookup (Scala "('_: Unit)/ =>/ Ref.lookup((_))")
16.12 -code_const Ref.update (Scala "('_: Unit)/ =>/ Ref.update((_), (_))")
16.13 +code_const ref' (Scala "('_: Unit)/ =>/ Heap.Ref((_))")
16.14 +code_const Ref.lookup (Scala "('_: Unit)/ =>/ Heap.Ref.lookup((_))")
16.15 +code_const Ref.update (Scala "('_: Unit)/ =>/ Heap.Ref.update((_), (_))")
16.16
16.17 end
17.1 --- a/src/HOL/Import/Generate-HOLLight/GenHOLLight.thy Fri Aug 27 09:34:06 2010 +0200
17.2 +++ b/src/HOL/Import/Generate-HOLLight/GenHOLLight.thy Fri Aug 27 09:43:52 2010 +0200
17.3 @@ -54,7 +54,7 @@
17.4 ONE_ONE > HOL4Setup.ONE_ONE
17.5 ONTO > Fun.surj
17.6 "=" > "op ="
17.7 - "==>" > "op -->"
17.8 + "==>" > HOL.implies
17.9 "/\\" > "op &"
17.10 "\\/" > "op |"
17.11 "!" > All
18.1 --- a/src/HOL/Import/HOLLight/hollight.imp Fri Aug 27 09:34:06 2010 +0200
18.2 +++ b/src/HOL/Import/HOLLight/hollight.imp Fri Aug 27 09:43:52 2010 +0200
18.3 @@ -233,7 +233,7 @@
18.4 "?" > "HOL.Ex"
18.5 ">=" > "HOLLight.hollight.>="
18.6 ">" > "HOLLight.hollight.>"
18.7 - "==>" > "op -->"
18.8 + "==>" > HOL.implies
18.9 "=" > "op ="
18.10 "<=" > "HOLLight.hollight.<="
18.11 "<" > "HOLLight.hollight.<"
19.1 --- a/src/HOL/Import/hol4rews.ML Fri Aug 27 09:34:06 2010 +0200
19.2 +++ b/src/HOL/Import/hol4rews.ML Fri Aug 27 09:43:52 2010 +0200
19.3 @@ -628,7 +628,7 @@
19.4 |> add_hol4_type_mapping "min" "fun" false "fun"
19.5 |> add_hol4_type_mapping "min" "ind" false @{type_name ind}
19.6 |> add_hol4_const_mapping "min" "=" false @{const_name "op ="}
19.7 - |> add_hol4_const_mapping "min" "==>" false @{const_name "op -->"}
19.8 + |> add_hol4_const_mapping "min" "==>" false @{const_name HOL.implies}
19.9 |> add_hol4_const_mapping "min" "@" false @{const_name "Eps"}
19.10 in
19.11 val hol4_setup =
20.1 --- a/src/HOL/Import/proof_kernel.ML Fri Aug 27 09:34:06 2010 +0200
20.2 +++ b/src/HOL/Import/proof_kernel.ML Fri Aug 27 09:43:52 2010 +0200
20.3 @@ -1205,7 +1205,7 @@
20.4 fun non_trivial_term_consts t = fold_aterms
20.5 (fn Const (c, _) =>
20.6 if c = @{const_name Trueprop} orelse c = @{const_name All}
20.7 - orelse c = @{const_name "op -->"} orelse c = @{const_name "op &"} orelse c = @{const_name "op ="}
20.8 + orelse c = @{const_name HOL.implies} orelse c = @{const_name "op &"} orelse c = @{const_name "op ="}
20.9 then I else insert (op =) c
20.10 | _ => I) t [];
20.11
20.12 @@ -1214,7 +1214,7 @@
20.13 fun add_consts (Const (c, _), cs) =
20.14 (case c of
20.15 @{const_name "op ="} => insert (op =) "==" cs
20.16 - | @{const_name "op -->"} => insert (op =) "==>" cs
20.17 + | @{const_name HOL.implies} => insert (op =) "==>" cs
20.18 | @{const_name All} => cs
20.19 | "all" => cs
20.20 | @{const_name "op &"} => cs
20.21 @@ -1860,7 +1860,7 @@
20.22 val _ = if_debug pth hth
20.23 val th1 = implies_elim_all (beta_eta_thm th)
20.24 val a = case concl_of th1 of
20.25 - _ $ (Const(@{const_name "op -->"},_) $ a $ Const(@{const_name False},_)) => a
20.26 + _ $ (Const(@{const_name HOL.implies},_) $ a $ Const(@{const_name False},_)) => a
20.27 | _ => raise ERR "NOT_INTRO" "Conclusion of bad form"
20.28 val ca = cterm_of thy a
20.29 val th2 = Thm.equal_elim (Drule.instantiate' [] [SOME ca] not_intro_thm) th1
21.1 --- a/src/HOL/Library/Code_Integer.thy Fri Aug 27 09:34:06 2010 +0200
21.2 +++ b/src/HOL/Library/Code_Integer.thy Fri Aug 27 09:43:52 2010 +0200
21.3 @@ -51,14 +51,14 @@
21.4 (SML "IntInf.- ((_), 1)")
21.5 (OCaml "Big'_int.pred'_big'_int")
21.6 (Haskell "!(_/ -/ 1)")
21.7 - (Scala "!(_/ -/ 1)")
21.8 + (Scala "!(_ -/ 1)")
21.9 (Eval "!(_/ -/ 1)")
21.10
21.11 code_const Int.succ
21.12 (SML "IntInf.+ ((_), 1)")
21.13 (OCaml "Big'_int.succ'_big'_int")
21.14 (Haskell "!(_/ +/ 1)")
21.15 - (Scala "!(_/ +/ 1)")
21.16 + (Scala "!(_ +/ 1)")
21.17 (Eval "!(_/ +/ 1)")
21.18
21.19 code_const "op + \<Colon> int \<Rightarrow> int \<Rightarrow> int"
22.1 --- a/src/HOL/Library/Code_Natural.thy Fri Aug 27 09:34:06 2010 +0200
22.2 +++ b/src/HOL/Library/Code_Natural.thy Fri Aug 27 09:43:52 2010 +0200
22.3 @@ -9,9 +9,7 @@
22.4 section {* Alternative representation of @{typ code_numeral} for @{text Haskell} and @{text Scala} *}
22.5
22.6 code_include Haskell "Natural"
22.7 -{*import Data.Array.ST;
22.8 -
22.9 -newtype Natural = Natural Integer deriving (Eq, Show, Read);
22.10 +{*newtype Natural = Natural Integer deriving (Eq, Show, Read);
22.11
22.12 instance Num Natural where {
22.13 fromInteger k = Natural (if k >= 0 then k else 0);
22.14 @@ -54,48 +52,48 @@
22.15
22.16 code_reserved Haskell Natural
22.17
22.18 -code_include Scala "Natural" {*
22.19 -import scala.Math
22.20 +code_include Scala "Natural"
22.21 +{*import scala.Math
22.22
22.23 -object Natural {
22.24 +object Nat {
22.25
22.26 - def apply(numeral: BigInt): Natural = new Natural(numeral max 0)
22.27 - def apply(numeral: Int): Natural = Natural(BigInt(numeral))
22.28 - def apply(numeral: String): Natural = Natural(BigInt(numeral))
22.29 + def apply(numeral: BigInt): Nat = new Nat(numeral max 0)
22.30 + def apply(numeral: Int): Nat = Nat(BigInt(numeral))
22.31 + def apply(numeral: String): Nat = Nat(BigInt(numeral))
22.32
22.33 }
22.34
22.35 -class Natural private(private val value: BigInt) {
22.36 +class Nat private(private val value: BigInt) {
22.37
22.38 override def hashCode(): Int = this.value.hashCode()
22.39
22.40 override def equals(that: Any): Boolean = that match {
22.41 - case that: Natural => this equals that
22.42 + case that: Nat => this equals that
22.43 case _ => false
22.44 }
22.45
22.46 override def toString(): String = this.value.toString
22.47
22.48 - def equals(that: Natural): Boolean = this.value == that.value
22.49 + def equals(that: Nat): Boolean = this.value == that.value
22.50
22.51 def as_BigInt: BigInt = this.value
22.52 def as_Int: Int = if (this.value >= Int.MinValue && this.value <= Int.MaxValue)
22.53 this.value.intValue
22.54 else error("Int value out of range: " + this.value.toString)
22.55
22.56 - def +(that: Natural): Natural = new Natural(this.value + that.value)
22.57 - def -(that: Natural): Natural = Natural(this.value - that.value)
22.58 - def *(that: Natural): Natural = new Natural(this.value * that.value)
22.59 + def +(that: Nat): Nat = new Nat(this.value + that.value)
22.60 + def -(that: Nat): Nat = Nat(this.value - that.value)
22.61 + def *(that: Nat): Nat = new Nat(this.value * that.value)
22.62
22.63 - def /%(that: Natural): (Natural, Natural) = if (that.value == 0) (new Natural(0), this)
22.64 + def /%(that: Nat): (Nat, Nat) = if (that.value == 0) (new Nat(0), this)
22.65 else {
22.66 val (k, l) = this.value /% that.value
22.67 - (new Natural(k), new Natural(l))
22.68 + (new Nat(k), new Nat(l))
22.69 }
22.70
22.71 - def <=(that: Natural): Boolean = this.value <= that.value
22.72 + def <=(that: Nat): Boolean = this.value <= that.value
22.73
22.74 - def <(that: Natural): Boolean = this.value < that.value
22.75 + def <(that: Nat): Boolean = this.value < that.value
22.76
22.77 }
22.78 *}
22.79 @@ -104,7 +102,7 @@
22.80
22.81 code_type code_numeral
22.82 (Haskell "Natural.Natural")
22.83 - (Scala "Natural")
22.84 + (Scala "Natural.Nat")
22.85
22.86 setup {*
22.87 fold (Numeral.add_code @{const_name number_code_numeral_inst.number_of_code_numeral}
23.1 --- a/src/HOL/Library/Efficient_Nat.thy Fri Aug 27 09:34:06 2010 +0200
23.2 +++ b/src/HOL/Library/Efficient_Nat.thy Fri Aug 27 09:43:52 2010 +0200
23.3 @@ -242,8 +242,8 @@
23.4 and @{typ int}.
23.5 *}
23.6
23.7 -code_include Haskell "Nat" {*
23.8 -newtype Nat = Nat Integer deriving (Eq, Show, Read);
23.9 +code_include Haskell "Nat"
23.10 +{*newtype Nat = Nat Integer deriving (Eq, Show, Read);
23.11
23.12 instance Num Nat where {
23.13 fromInteger k = Nat (if k >= 0 then k else 0);
23.14 @@ -280,8 +280,8 @@
23.15
23.16 code_reserved Haskell Nat
23.17
23.18 -code_include Scala "Nat" {*
23.19 -import scala.Math
23.20 +code_include Scala "Nat"
23.21 +{*import scala.Math
23.22
23.23 object Nat {
23.24
23.25 @@ -330,7 +330,7 @@
23.26
23.27 code_type nat
23.28 (Haskell "Nat.Nat")
23.29 - (Scala "Nat")
23.30 + (Scala "Nat.Nat")
23.31
23.32 code_instance nat :: eq
23.33 (Haskell -)
23.34 @@ -397,7 +397,7 @@
23.35
23.36 code_const int and nat
23.37 (Haskell "toInteger" and "fromInteger")
23.38 - (Scala "!_.as'_BigInt" and "Nat")
23.39 + (Scala "!_.as'_BigInt" and "Nat.Nat")
23.40
23.41 text {* Conversion from and to code numerals. *}
23.42
23.43 @@ -405,14 +405,14 @@
23.44 (SML "IntInf.toInt")
23.45 (OCaml "_")
23.46 (Haskell "!(fromInteger/ ./ toInteger)")
23.47 - (Scala "!Natural(_.as'_BigInt)")
23.48 + (Scala "!Natural.Nat(_.as'_BigInt)")
23.49 (Eval "_")
23.50
23.51 code_const Code_Numeral.nat_of
23.52 (SML "IntInf.fromInt")
23.53 (OCaml "_")
23.54 (Haskell "!(fromInteger/ ./ toInteger)")
23.55 - (Scala "!Nat(_.as'_BigInt)")
23.56 + (Scala "!Nat.Nat(_.as'_BigInt)")
23.57 (Eval "_")
23.58
23.59 text {* Using target language arithmetic operations whenever appropriate *}
24.1 --- a/src/HOL/Library/Sum_Of_Squares/sum_of_squares.ML Fri Aug 27 09:34:06 2010 +0200
24.2 +++ b/src/HOL/Library/Sum_Of_Squares/sum_of_squares.ML Fri Aug 27 09:43:52 2010 +0200
24.3 @@ -1356,7 +1356,7 @@
24.4
24.5 val known_sos_constants =
24.6 [@{term "op ==>"}, @{term "Trueprop"},
24.7 - @{term "op -->"}, @{term "op &"}, @{term "op |"},
24.8 + @{term HOL.implies}, @{term "op &"}, @{term "op |"},
24.9 @{term "Not"}, @{term "op = :: bool => _"},
24.10 @{term "All :: (real => _) => _"}, @{term "Ex :: (real => _) => _"},
24.11 @{term "op = :: real => _"}, @{term "op < :: real => _"},
25.1 --- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Fri Aug 27 09:34:06 2010 +0200
25.2 +++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Fri Aug 27 09:43:52 2010 +0200
25.3 @@ -290,10 +290,12 @@
25.4 | NONE => get_prover (default_atp_name ()))
25.5 end
25.6
25.7 +type locality = Sledgehammer_Fact_Filter.locality
25.8 +
25.9 local
25.10
25.11 datatype sh_result =
25.12 - SH_OK of int * int * (string * bool) list |
25.13 + SH_OK of int * int * (string * locality) list |
25.14 SH_FAIL of int * int |
25.15 SH_ERROR
25.16
25.17 @@ -355,8 +357,8 @@
25.18 case result of
25.19 SH_OK (time_isa, time_atp, names) =>
25.20 let
25.21 - fun get_thms (name, chained) =
25.22 - ((name, chained), thms_of_name (Proof.context_of st) name)
25.23 + fun get_thms (name, loc) =
25.24 + ((name, loc), thms_of_name (Proof.context_of st) name)
25.25 in
25.26 change_data id inc_sh_success;
25.27 change_data id (inc_sh_lemmas (length names));
25.28 @@ -445,7 +447,7 @@
25.29 then () else
25.30 let
25.31 val named_thms =
25.32 - Unsynchronized.ref (NONE : ((string * bool) * thm list) list option)
25.33 + Unsynchronized.ref (NONE : ((string * locality) * thm list) list option)
25.34 val minimize = AList.defined (op =) args minimizeK
25.35 val metis_ft = AList.defined (op =) args metis_ftK
25.36
26.1 --- a/src/HOL/Orderings.thy Fri Aug 27 09:34:06 2010 +0200
26.2 +++ b/src/HOL/Orderings.thy Fri Aug 27 09:43:52 2010 +0200
26.3 @@ -640,7 +640,7 @@
26.4 let
26.5 val All_binder = Syntax.binder_name @{const_syntax All};
26.6 val Ex_binder = Syntax.binder_name @{const_syntax Ex};
26.7 - val impl = @{const_syntax "op -->"};
26.8 + val impl = @{const_syntax HOL.implies};
26.9 val conj = @{const_syntax "op &"};
26.10 val less = @{const_syntax less};
26.11 val less_eq = @{const_syntax less_eq};
27.1 --- a/src/HOL/Prolog/prolog.ML Fri Aug 27 09:34:06 2010 +0200
27.2 +++ b/src/HOL/Prolog/prolog.ML Fri Aug 27 09:43:52 2010 +0200
27.3 @@ -12,7 +12,7 @@
27.4 fun isD t = case t of
27.5 Const(@{const_name Trueprop},_)$t => isD t
27.6 | Const(@{const_name "op &"} ,_)$l$r => isD l andalso isD r
27.7 - | Const(@{const_name "op -->"},_)$l$r => isG l andalso isD r
27.8 + | Const(@{const_name HOL.implies},_)$l$r => isG l andalso isD r
27.9 | Const( "==>",_)$l$r => isG l andalso isD r
27.10 | Const(@{const_name All},_)$Abs(s,_,t) => isD t
27.11 | Const("all",_)$Abs(s,_,t) => isD t
27.12 @@ -32,7 +32,7 @@
27.13 Const(@{const_name Trueprop},_)$t => isG t
27.14 | Const(@{const_name "op &"} ,_)$l$r => isG l andalso isG r
27.15 | Const(@{const_name "op |"} ,_)$l$r => isG l andalso isG r
27.16 - | Const(@{const_name "op -->"},_)$l$r => isD l andalso isG r
27.17 + | Const(@{const_name HOL.implies},_)$l$r => isD l andalso isG r
27.18 | Const( "==>",_)$l$r => isD l andalso isG r
27.19 | Const(@{const_name All},_)$Abs(_,_,t) => isG t
27.20 | Const("all",_)$Abs(_,_,t) => isG t
27.21 @@ -54,7 +54,7 @@
27.22 _$(Const(@{const_name All} ,_)$Abs(s,_,_))=> at(thm RS
27.23 (read_instantiate ctxt [(("x", 0), "?" ^ (if s="P" then "PP" else s))] spec))
27.24 | _$(Const(@{const_name "op &"},_)$_$_) => at(thm RS conjunct1)@at(thm RS conjunct2)
27.25 - | _$(Const(@{const_name "op -->"},_)$_$_) => at(thm RS mp)
27.26 + | _$(Const(@{const_name HOL.implies},_)$_$_) => at(thm RS mp)
27.27 | _ => [thm]
27.28 in map zero_var_indexes (at thm) end;
27.29
27.30 @@ -72,7 +72,7 @@
27.31 -- is nice, but cannot instantiate unknowns in the assumptions *)
27.32 fun hyp_resolve_tac i st = let
27.33 fun ap (Const(@{const_name All},_)$Abs(_,_,t))=(case ap t of (k,a,t) => (k+1,a ,t))
27.34 - | ap (Const(@{const_name "op -->"},_)$_$t) =(case ap t of (k,_,t) => (k,true ,t))
27.35 + | ap (Const(@{const_name HOL.implies},_)$_$t) =(case ap t of (k,_,t) => (k,true ,t))
27.36 | ap t = (0,false,t);
27.37 (*
27.38 fun rep_goal (Const ("all",_)$Abs (_,_,t)) = rep_goal t
28.1 --- a/src/HOL/Set.thy Fri Aug 27 09:34:06 2010 +0200
28.2 +++ b/src/HOL/Set.thy Fri Aug 27 09:43:52 2010 +0200
28.3 @@ -219,7 +219,7 @@
28.4 val Type (set_type, _) = @{typ "'a set"}; (* FIXME 'a => bool (!?!) *)
28.5 val All_binder = Syntax.binder_name @{const_syntax All};
28.6 val Ex_binder = Syntax.binder_name @{const_syntax Ex};
28.7 - val impl = @{const_syntax "op -->"};
28.8 + val impl = @{const_syntax HOL.implies};
28.9 val conj = @{const_syntax "op &"};
28.10 val sbset = @{const_syntax subset};
28.11 val sbset_eq = @{const_syntax subset_eq};
29.1 --- a/src/HOL/TLA/Intensional.thy Fri Aug 27 09:34:06 2010 +0200
29.2 +++ b/src/HOL/TLA/Intensional.thy Fri Aug 27 09:43:52 2010 +0200
29.3 @@ -279,7 +279,7 @@
29.4
29.5 fun hflatten t =
29.6 case (concl_of t) of
29.7 - Const _ $ (Const (@{const_name "op -->"}, _) $ _ $ _) => hflatten (t RS mp)
29.8 + Const _ $ (Const (@{const_name HOL.implies}, _) $ _ $ _) => hflatten (t RS mp)
29.9 | _ => (hflatten (matchsome conjI t)) handle THM _ => zero_var_indexes t
29.10 in
29.11 hflatten t
30.1 --- a/src/HOL/Tools/ATP/atp_systems.ML Fri Aug 27 09:34:06 2010 +0200
30.2 +++ b/src/HOL/Tools/ATP/atp_systems.ML Fri Aug 27 09:43:52 2010 +0200
30.3 @@ -19,7 +19,7 @@
30.4 has_incomplete_mode: bool,
30.5 proof_delims: (string * string) list,
30.6 known_failures: (failure * string) list,
30.7 - default_max_relevant_per_iter: int,
30.8 + default_max_relevant: int,
30.9 default_theory_relevant: bool,
30.10 explicit_forall: bool,
30.11 use_conjecture_for_hypotheses: bool}
30.12 @@ -52,7 +52,7 @@
30.13 has_incomplete_mode: bool,
30.14 proof_delims: (string * string) list,
30.15 known_failures: (failure * string) list,
30.16 - default_max_relevant_per_iter: int,
30.17 + default_max_relevant: int,
30.18 default_theory_relevant: bool,
30.19 explicit_forall: bool,
30.20 use_conjecture_for_hypotheses: bool}
30.21 @@ -125,10 +125,20 @@
30.22 priority ("Available ATPs: " ^
30.23 commas (sort_strings (Symtab.keys (Data.get thy))) ^ ".")
30.24
30.25 -fun to_generous_secs time = (Time.toMilliseconds time + 999) div 1000
30.26 +fun to_secs bonus time = (Time.toMilliseconds time + bonus + 999) div 1000
30.27
30.28 (* E prover *)
30.29
30.30 +(* Give older versions of E an extra second, because the "eproof" script wrongly
30.31 + subtracted an entire second to account for the overhead of the script
30.32 + itself, which is in fact much lower. *)
30.33 +fun e_bonus () =
30.34 + case getenv "E_VERSION" of
30.35 + "" => 1000
30.36 + | version =>
30.37 + if exists (fn s => String.isPrefix s version) ["0.9", "1.0"] then 1000
30.38 + else 0
30.39 +
30.40 val tstp_proof_delims =
30.41 ("# SZS output start CNFRefutation.", "# SZS output end CNFRefutation")
30.42
30.43 @@ -137,8 +147,7 @@
30.44 required_execs = [],
30.45 arguments = fn _ => fn timeout =>
30.46 "--tstp-in --tstp-out -l5 -xAutoDev -tAutoDev --silent \
30.47 - \--soft-cpu-limit=" ^
30.48 - string_of_int (to_generous_secs timeout),
30.49 + \--cpu-limit=" ^ string_of_int (to_secs (e_bonus ()) timeout),
30.50 has_incomplete_mode = false,
30.51 proof_delims = [tstp_proof_delims],
30.52 known_failures =
30.53 @@ -150,7 +159,7 @@
30.54 "# Cannot determine problem status within resource limit"),
30.55 (OutOfResources, "SZS status: ResourceOut"),
30.56 (OutOfResources, "SZS status ResourceOut")],
30.57 - default_max_relevant_per_iter = 80 (* FUDGE *),
30.58 + default_max_relevant = 500 (* FUDGE *),
30.59 default_theory_relevant = false,
30.60 explicit_forall = false,
30.61 use_conjecture_for_hypotheses = true}
30.62 @@ -165,7 +174,7 @@
30.63 required_execs = [("SPASS_HOME", "SPASS")],
30.64 arguments = fn complete => fn timeout =>
30.65 ("-Auto -PGiven=0 -PProblem=0 -Splits=0 -FullRed=0 -DocProof \
30.66 - \-VarWeight=3 -TimeLimit=" ^ string_of_int (to_generous_secs timeout))
30.67 + \-VarWeight=3 -TimeLimit=" ^ string_of_int (to_secs 0 timeout))
30.68 |> not complete ? prefix "-SOS=1 ",
30.69 has_incomplete_mode = true,
30.70 proof_delims = [("Here is a proof", "Formulae used in the proof")],
30.71 @@ -177,7 +186,7 @@
30.72 (MalformedInput, "Undefined symbol"),
30.73 (MalformedInput, "Free Variable"),
30.74 (SpassTooOld, "tptp2dfg")],
30.75 - default_max_relevant_per_iter = 40 (* FUDGE *),
30.76 + default_max_relevant = 350 (* FUDGE *),
30.77 default_theory_relevant = true,
30.78 explicit_forall = true,
30.79 use_conjecture_for_hypotheses = true}
30.80 @@ -190,10 +199,11 @@
30.81 val vampire_config : prover_config =
30.82 {exec = ("VAMPIRE_HOME", "vampire"),
30.83 required_execs = [],
30.84 - arguments = fn _ => fn timeout =>
30.85 - "--mode casc -t " ^ string_of_int (to_generous_secs timeout) ^
30.86 - " --thanks Andrei --input_file",
30.87 - has_incomplete_mode = false,
30.88 + arguments = fn complete => fn timeout =>
30.89 + ("--mode casc -t " ^ string_of_int (to_secs 0 timeout) ^
30.90 + " --thanks Andrei --input_file")
30.91 + |> not complete ? prefix "--sos on ",
30.92 + has_incomplete_mode = true,
30.93 proof_delims =
30.94 [("=========== Refutation ==========",
30.95 "======= End of refutation ======="),
30.96 @@ -206,7 +216,7 @@
30.97 (Unprovable, "Satisfiability detected"),
30.98 (Unprovable, "Termination reason: Satisfiable"),
30.99 (VampireTooOld, "not a valid option")],
30.100 - default_max_relevant_per_iter = 45 (* FUDGE *),
30.101 + default_max_relevant = 400 (* FUDGE *),
30.102 default_theory_relevant = false,
30.103 explicit_forall = false,
30.104 use_conjecture_for_hypotheses = true}
30.105 @@ -246,38 +256,38 @@
30.106 | SOME sys => sys
30.107
30.108 fun remote_config system_name system_versions proof_delims known_failures
30.109 - default_max_relevant_per_iter default_theory_relevant
30.110 - use_conjecture_for_hypotheses =
30.111 + default_max_relevant default_theory_relevant
30.112 + use_conjecture_for_hypotheses : prover_config =
30.113 {exec = ("ISABELLE_ATP", "scripts/remote_atp"),
30.114 required_execs = [],
30.115 arguments = fn _ => fn timeout =>
30.116 - " -t " ^ string_of_int (to_generous_secs timeout) ^ " -s " ^
30.117 + " -t " ^ string_of_int (to_secs 0 timeout) ^ " -s " ^
30.118 the_system system_name system_versions,
30.119 has_incomplete_mode = false,
30.120 proof_delims = insert (op =) tstp_proof_delims proof_delims,
30.121 known_failures =
30.122 known_failures @ known_perl_failures @
30.123 [(TimedOut, "says Timeout")],
30.124 - default_max_relevant_per_iter = default_max_relevant_per_iter,
30.125 + default_max_relevant = default_max_relevant,
30.126 default_theory_relevant = default_theory_relevant,
30.127 explicit_forall = true,
30.128 use_conjecture_for_hypotheses = use_conjecture_for_hypotheses}
30.129
30.130 fun remotify_config system_name system_versions
30.131 - ({proof_delims, known_failures, default_max_relevant_per_iter,
30.132 + ({proof_delims, known_failures, default_max_relevant,
30.133 default_theory_relevant, use_conjecture_for_hypotheses, ...}
30.134 : prover_config) : prover_config =
30.135 remote_config system_name system_versions proof_delims known_failures
30.136 - default_max_relevant_per_iter default_theory_relevant
30.137 + default_max_relevant default_theory_relevant
30.138 use_conjecture_for_hypotheses
30.139
30.140 val remotify_name = prefix "remote_"
30.141 fun remote_prover name system_name system_versions proof_delims known_failures
30.142 - default_max_relevant_per_iter default_theory_relevant
30.143 + default_max_relevant default_theory_relevant
30.144 use_conjecture_for_hypotheses =
30.145 (remotify_name name,
30.146 remote_config system_name system_versions proof_delims known_failures
30.147 - default_max_relevant_per_iter default_theory_relevant
30.148 + default_max_relevant default_theory_relevant
30.149 use_conjecture_for_hypotheses)
30.150 fun remotify_prover (name, config) system_name system_versions =
30.151 (remotify_name name, remotify_config system_name system_versions config)
30.152 @@ -285,11 +295,11 @@
30.153 val remote_e = remotify_prover e "EP" ["1.0", "1.1", "1.2"]
30.154 val remote_vampire = remotify_prover vampire "Vampire" ["9.9", "0.6", "1.0"]
30.155 val remote_sine_e =
30.156 - remote_prover "sine_e" "SInE" [] []
30.157 - [(Unprovable, "says Unknown")] 150 (* FUDGE *) false true
30.158 + remote_prover "sine_e" "SInE" [] [] [(Unprovable, "says Unknown")]
30.159 + 1000 (* FUDGE *) false true
30.160 val remote_snark =
30.161 remote_prover "snark" "SNARK---" [] [("refutation.", "end_refutation.")] []
30.162 - 50 (* FUDGE *) false true
30.163 + 350 (* FUDGE *) false true
30.164
30.165 (* Setup *)
30.166
31.1 --- a/src/HOL/Tools/Nitpick/minipick.ML Fri Aug 27 09:34:06 2010 +0200
31.2 +++ b/src/HOL/Tools/Nitpick/minipick.ML Fri Aug 27 09:43:52 2010 +0200
31.3 @@ -132,7 +132,7 @@
31.4 Subset (to_R_rep Ts t1, to_R_rep Ts t2)
31.5 | @{const "op &"} $ t1 $ t2 => And (to_F Ts t1, to_F Ts t2)
31.6 | @{const "op |"} $ t1 $ t2 => Or (to_F Ts t1, to_F Ts t2)
31.7 - | @{const "op -->"} $ t1 $ t2 => Implies (to_F Ts t1, to_F Ts t2)
31.8 + | @{const HOL.implies} $ t1 $ t2 => Implies (to_F Ts t1, to_F Ts t2)
31.9 | t1 $ t2 => Subset (to_S_rep Ts t2, to_R_rep Ts t1)
31.10 | Free _ => raise SAME ()
31.11 | Term.Var _ => raise SAME ()
31.12 @@ -177,8 +177,8 @@
31.13 | @{const "op &"} => to_R_rep Ts (eta_expand Ts t 2)
31.14 | @{const "op |"} $ _ => to_R_rep Ts (eta_expand Ts t 1)
31.15 | @{const "op |"} => to_R_rep Ts (eta_expand Ts t 2)
31.16 - | @{const "op -->"} $ _ => to_R_rep Ts (eta_expand Ts t 1)
31.17 - | @{const "op -->"} => to_R_rep Ts (eta_expand Ts t 2)
31.18 + | @{const HOL.implies} $ _ => to_R_rep Ts (eta_expand Ts t 1)
31.19 + | @{const HOL.implies} => to_R_rep Ts (eta_expand Ts t 2)
31.20 | Const (@{const_name bot_class.bot},
31.21 T as Type (@{type_name fun}, [_, @{typ bool}])) =>
31.22 empty_n_ary_rel (arity_of RRep card T)
32.1 --- a/src/HOL/Tools/Nitpick/nitpick_hol.ML Fri Aug 27 09:34:06 2010 +0200
32.2 +++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML Fri Aug 27 09:43:52 2010 +0200
32.3 @@ -411,7 +411,7 @@
32.4 (@{const_name "op ="}, 1),
32.5 (@{const_name "op &"}, 2),
32.6 (@{const_name "op |"}, 2),
32.7 - (@{const_name "op -->"}, 2),
32.8 + (@{const_name HOL.implies}, 2),
32.9 (@{const_name If}, 3),
32.10 (@{const_name Let}, 2),
32.11 (@{const_name Pair}, 2),
32.12 @@ -1454,7 +1454,7 @@
32.13 | @{const Trueprop} $ t1 => lhs_of_equation t1
32.14 | Const (@{const_name All}, _) $ Abs (_, _, t1) => lhs_of_equation t1
32.15 | Const (@{const_name "op ="}, _) $ t1 $ _ => SOME t1
32.16 - | @{const "op -->"} $ _ $ t2 => lhs_of_equation t2
32.17 + | @{const HOL.implies} $ _ $ t2 => lhs_of_equation t2
32.18 | _ => NONE
32.19 fun is_constr_pattern _ (Bound _) = true
32.20 | is_constr_pattern _ (Var _) = true
33.1 --- a/src/HOL/Tools/Nitpick/nitpick_mono.ML Fri Aug 27 09:34:06 2010 +0200
33.2 +++ b/src/HOL/Tools/Nitpick/nitpick_mono.ML Fri Aug 27 09:43:52 2010 +0200
33.3 @@ -774,7 +774,7 @@
33.4 (MAbs (s, T, M, S Minus, m'), accum |>> pop_bound)
33.5 end))
33.6 | (t0 as Const (@{const_name All}, _))
33.7 - $ Abs (s', T', (t10 as @{const "op -->"}) $ (t11 $ Bound 0) $ t12) =>
33.8 + $ Abs (s', T', (t10 as @{const HOL.implies}) $ (t11 $ Bound 0) $ t12) =>
33.9 do_bounded_quantifier t0 s' T' t10 t11 t12 accum
33.10 | (t0 as Const (@{const_name Ex}, _))
33.11 $ Abs (s', T', (t10 as @{const "op &"}) $ (t11 $ Bound 0) $ t12) =>
33.12 @@ -885,10 +885,10 @@
33.13 s0 = @{const_name Pure.conjunction} orelse
33.14 s0 = @{const_name "op &"} orelse
33.15 s0 = @{const_name "op |"} orelse
33.16 - s0 = @{const_name "op -->"} then
33.17 + s0 = @{const_name HOL.implies} then
33.18 let
33.19 val impl = (s0 = @{const_name "==>"} orelse
33.20 - s0 = @{const_name "op -->"})
33.21 + s0 = @{const_name HOL.implies})
33.22 val (m1, accum) = do_formula (sn |> impl ? negate) t1 accum
33.23 val (m2, accum) = do_formula sn t2 accum
33.24 in
33.25 @@ -976,7 +976,7 @@
33.26 | Const (x as (@{const_name "op ="}, _)) $ t1 $ t2 =>
33.27 consider_general_equals mdata true x t1 t2 accum
33.28 | (t0 as @{const "op &"}) $ t1 $ t2 => do_conjunction t0 t1 t2 accum
33.29 - | (t0 as @{const "op -->"}) $ t1 $ t2 => do_implies t0 t1 t2 accum
33.30 + | (t0 as @{const HOL.implies}) $ t1 $ t2 => do_implies t0 t1 t2 accum
33.31 | _ => raise TERM ("Nitpick_Mono.consider_definitional_axiom.\
33.32 \do_formula", [t])
33.33 in do_formula t end
34.1 --- a/src/HOL/Tools/Nitpick/nitpick_nut.ML Fri Aug 27 09:34:06 2010 +0200
34.2 +++ b/src/HOL/Tools/Nitpick/nitpick_nut.ML Fri Aug 27 09:43:52 2010 +0200
34.3 @@ -522,7 +522,7 @@
34.4 Op2 (And, bool_T, Any, sub' t1, sub' t2)
34.5 | (Const (@{const_name "op |"}, _), [t1, t2]) =>
34.6 Op2 (Or, bool_T, Any, sub t1, sub t2)
34.7 - | (Const (@{const_name "op -->"}, _), [t1, t2]) =>
34.8 + | (Const (@{const_name HOL.implies}, _), [t1, t2]) =>
34.9 Op2 (Or, bool_T, Any, Op1 (Not, bool_T, Any, sub t1), sub' t2)
34.10 | (Const (@{const_name If}, T), [t1, t2, t3]) =>
34.11 Op3 (If, nth_range_type 3 T, Any, sub t1, sub t2, sub t3)
35.1 --- a/src/HOL/Tools/Nitpick/nitpick_preproc.ML Fri Aug 27 09:34:06 2010 +0200
35.2 +++ b/src/HOL/Tools/Nitpick/nitpick_preproc.ML Fri Aug 27 09:43:52 2010 +0200
35.3 @@ -43,7 +43,7 @@
35.4 | aux def (@{const "==>"} $ t1 $ t2) = aux false t1 andalso aux def t2
35.5 | aux def (Const (@{const_name "op ="}, _) $ t1 $ t2) =
35.6 aux def t1 andalso aux false t2
35.7 - | aux def (@{const "op -->"} $ t1 $ t2) = aux false t1 andalso aux def t2
35.8 + | aux def (@{const HOL.implies} $ t1 $ t2) = aux false t1 andalso aux def t2
35.9 | aux def (t1 $ t2) = aux def t1 andalso aux def t2
35.10 | aux def (t as Const (s, _)) =
35.11 (not def orelse t <> @{const Suc}) andalso
35.12 @@ -217,8 +217,8 @@
35.13 | @{const "op |"} $ t1 $ t2 =>
35.14 @{const "op |"} $ do_term new_Ts old_Ts polar t1
35.15 $ do_term new_Ts old_Ts polar t2
35.16 - | @{const "op -->"} $ t1 $ t2 =>
35.17 - @{const "op -->"} $ do_term new_Ts old_Ts (flip_polarity polar) t1
35.18 + | @{const HOL.implies} $ t1 $ t2 =>
35.19 + @{const HOL.implies} $ do_term new_Ts old_Ts (flip_polarity polar) t1
35.20 $ do_term new_Ts old_Ts polar t2
35.21 | Const (x as (s, T)) =>
35.22 if is_descr s then
35.23 @@ -334,7 +334,7 @@
35.24 if def then (t, []) else do_eq_or_imp Ts false def t0 t1 t2 seen
35.25 | (t0 as Const (@{const_name "op ="}, _)) $ t1 $ t2 =>
35.26 do_eq_or_imp Ts true def t0 t1 t2 seen
35.27 - | (t0 as @{const "op -->"}) $ t1 $ t2 =>
35.28 + | (t0 as @{const HOL.implies}) $ t1 $ t2 =>
35.29 do_eq_or_imp Ts false def t0 t1 t2 seen
35.30 | Abs (s, T, t') =>
35.31 let val (t', seen) = do_term (T :: Ts) def t' [] seen in
35.32 @@ -401,7 +401,7 @@
35.33 t0 $ aux false t1 $ aux careful t2
35.34 | aux careful ((t0 as Const (@{const_name "op ="}, _)) $ t1 $ t2) =
35.35 aux_eq careful true t0 t1 t2
35.36 - | aux careful ((t0 as @{const "op -->"}) $ t1 $ t2) =
35.37 + | aux careful ((t0 as @{const HOL.implies}) $ t1 $ t2) =
35.38 t0 $ aux false t1 $ aux careful t2
35.39 | aux careful (Abs (s, T, t')) = Abs (s, T, aux careful t')
35.40 | aux careful (t1 $ t2) = aux careful t1 $ aux careful t2
35.41 @@ -608,8 +608,8 @@
35.42 s_conj (pairself (aux ss Ts js skolemizable polar) (t1, t2))
35.43 | @{const "op |"} $ t1 $ t2 =>
35.44 s_disj (pairself (aux ss Ts js skolemizable polar) (t1, t2))
35.45 - | @{const "op -->"} $ t1 $ t2 =>
35.46 - @{const "op -->"} $ aux ss Ts js skolemizable (flip_polarity polar) t1
35.47 + | @{const HOL.implies} $ t1 $ t2 =>
35.48 + @{const HOL.implies} $ aux ss Ts js skolemizable (flip_polarity polar) t1
35.49 $ aux ss Ts js skolemizable polar t2
35.50 | (t0 as Const (@{const_name Let}, _)) $ t1 $ t2 =>
35.51 t0 $ t1 $ aux ss Ts js skolemizable polar t2
35.52 @@ -1121,7 +1121,7 @@
35.53 (t10 as @{const "op |"}) $ t11 $ t12 =>
35.54 t10 $ distribute_quantifiers (t0 $ Abs (s, T1, t11))
35.55 $ distribute_quantifiers (t0 $ Abs (s, T1, t12))
35.56 - | (t10 as @{const "op -->"}) $ t11 $ t12 =>
35.57 + | (t10 as @{const HOL.implies}) $ t11 $ t12 =>
35.58 t10 $ distribute_quantifiers (Const (@{const_name All}, T0)
35.59 $ Abs (s, T1, t11))
35.60 $ distribute_quantifiers (t0 $ Abs (s, T1, t12))
36.1 --- a/src/HOL/Tools/Predicate_Compile/code_prolog.ML Fri Aug 27 09:34:06 2010 +0200
36.2 +++ b/src/HOL/Tools/Predicate_Compile/code_prolog.ML Fri Aug 27 09:43:52 2010 +0200
36.3 @@ -664,10 +664,10 @@
36.4
36.5 (* FIXME: large copy of Predicate_Compile_Quickcheck - refactor out commons *)
36.6
36.7 -fun strip_imp_prems (Const(@{const_name "op -->"}, _) $ A $ B) = A :: strip_imp_prems B
36.8 +fun strip_imp_prems (Const(@{const_name HOL.implies}, _) $ A $ B) = A :: strip_imp_prems B
36.9 | strip_imp_prems _ = [];
36.10
36.11 -fun strip_imp_concl (Const(@{const_name "op -->"}, _) $ A $ B) = strip_imp_concl B
36.12 +fun strip_imp_concl (Const(@{const_name HOL.implies}, _) $ A $ B) = strip_imp_concl B
36.13 | strip_imp_concl A = A : term;
36.14
36.15 fun strip_horn A = (strip_imp_prems A, strip_imp_concl A);
37.1 --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_data.ML Fri Aug 27 09:34:06 2010 +0200
37.2 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_data.ML Fri Aug 27 09:43:52 2010 +0200
37.3 @@ -218,7 +218,7 @@
37.4 @{const_name Trueprop},
37.5 @{const_name Not},
37.6 @{const_name "op ="},
37.7 - @{const_name "op -->"},
37.8 + @{const_name HOL.implies},
37.9 @{const_name All},
37.10 @{const_name Ex},
37.11 @{const_name "op &"},
38.1 --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_quickcheck.ML Fri Aug 27 09:34:06 2010 +0200
38.2 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_quickcheck.ML Fri Aug 27 09:43:52 2010 +0200
38.3 @@ -168,10 +168,10 @@
38.4 mk_split_lambda' xs t
38.5 end;
38.6
38.7 -fun strip_imp_prems (Const(@{const_name "op -->"}, _) $ A $ B) = A :: strip_imp_prems B
38.8 +fun strip_imp_prems (Const(@{const_name HOL.implies}, _) $ A $ B) = A :: strip_imp_prems B
38.9 | strip_imp_prems _ = [];
38.10
38.11 -fun strip_imp_concl (Const(@{const_name "op -->"}, _) $ A $ B) = strip_imp_concl B
38.12 +fun strip_imp_concl (Const(@{const_name HOL.implies}, _) $ A $ B) = strip_imp_concl B
38.13 | strip_imp_concl A = A : term;
38.14
38.15 fun strip_horn A = (strip_imp_prems A, strip_imp_concl A);
39.1 --- a/src/HOL/Tools/Qelim/cooper.ML Fri Aug 27 09:34:06 2010 +0200
39.2 +++ b/src/HOL/Tools/Qelim/cooper.ML Fri Aug 27 09:43:52 2010 +0200
39.3 @@ -28,7 +28,7 @@
39.4 @{term "op * :: int => _"}, @{term "op * :: nat => _"},
39.5 @{term "op div :: int => _"}, @{term "op div :: nat => _"},
39.6 @{term "op mod :: int => _"}, @{term "op mod :: nat => _"},
39.7 - @{term "op &"}, @{term "op |"}, @{term "op -->"},
39.8 + @{term "op &"}, @{term "op |"}, @{term HOL.implies},
39.9 @{term "op = :: int => _"}, @{term "op = :: nat => _"}, @{term "op = :: bool => _"},
39.10 @{term "op < :: int => _"}, @{term "op < :: nat => _"},
39.11 @{term "op <= :: int => _"}, @{term "op <= :: nat => _"},
39.12 @@ -569,7 +569,7 @@
39.13 fun add_bools t =
39.14 let
39.15 val ops = [@{term "op = :: int => _"}, @{term "op < :: int => _"}, @{term "op <= :: int => _"},
39.16 - @{term "op &"}, @{term "op |"}, @{term "op -->"}, @{term "op = :: bool => _"},
39.17 + @{term "op &"}, @{term "op |"}, @{term HOL.implies}, @{term "op = :: bool => _"},
39.18 @{term "Not"}, @{term "All :: (int => _) => _"},
39.19 @{term "Ex :: (int => _) => _"}, @{term "True"}, @{term "False"}];
39.20 val is_op = member (op =) ops;
39.21 @@ -616,7 +616,7 @@
39.22 Proc.And (fm_of_term ps vs t1, fm_of_term ps vs t2)
39.23 | fm_of_term ps vs (Const (@{const_name "op |"}, _) $ t1 $ t2) =
39.24 Proc.Or (fm_of_term ps vs t1, fm_of_term ps vs t2)
39.25 - | fm_of_term ps vs (Const (@{const_name "op -->"}, _) $ t1 $ t2) =
39.26 + | fm_of_term ps vs (Const (@{const_name HOL.implies}, _) $ t1 $ t2) =
39.27 Proc.Imp (fm_of_term ps vs t1, fm_of_term ps vs t2)
39.28 | fm_of_term ps vs (@{term "op = :: bool => _ "} $ t1 $ t2) =
39.29 Proc.Iff (fm_of_term ps vs t1, fm_of_term ps vs t2)
39.30 @@ -687,7 +687,7 @@
39.31
39.32 fun strip_objimp ct =
39.33 (case Thm.term_of ct of
39.34 - Const (@{const_name "op -->"}, _) $ _ $ _ =>
39.35 + Const (@{const_name HOL.implies}, _) $ _ $ _ =>
39.36 let val (A, B) = Thm.dest_binop ct
39.37 in A :: strip_objimp B end
39.38 | _ => [ct]);
39.39 @@ -712,7 +712,7 @@
39.40 val qs = filter P ps
39.41 val q = if P c then c else @{cterm "False"}
39.42 val ng = fold_rev (fn (a,v) => fn t => Thm.capply a (Thm.cabs v t)) qvs
39.43 - (fold_rev (fn p => fn q => Thm.capply (Thm.capply @{cterm "op -->"} p) q) qs q)
39.44 + (fold_rev (fn p => fn q => Thm.capply (Thm.capply @{cterm HOL.implies} p) q) qs q)
39.45 val g = Thm.capply (Thm.capply @{cterm "op ==>"} (Thm.capply @{cterm "Trueprop"} ng)) p'
39.46 val ntac = (case qs of [] => q aconvc @{cterm "False"}
39.47 | _ => false)
40.1 --- a/src/HOL/Tools/Qelim/qelim.ML Fri Aug 27 09:34:06 2010 +0200
40.2 +++ b/src/HOL/Tools/Qelim/qelim.ML Fri Aug 27 09:43:52 2010 +0200
40.3 @@ -26,7 +26,7 @@
40.4 Const(s,T)$_$_ =>
40.5 if domain_type T = HOLogic.boolT
40.6 andalso member (op =) [@{const_name "op &"}, @{const_name "op |"},
40.7 - @{const_name "op -->"}, @{const_name "op ="}] s
40.8 + @{const_name HOL.implies}, @{const_name "op ="}] s
40.9 then binop_conv (conv env) p
40.10 else atcv env p
40.11 | Const(@{const_name Not},_)$_ => arg_conv (conv env) p
41.1 --- a/src/HOL/Tools/SMT/smtlib_interface.ML Fri Aug 27 09:34:06 2010 +0200
41.2 +++ b/src/HOL/Tools/SMT/smtlib_interface.ML Fri Aug 27 09:43:52 2010 +0200
41.3 @@ -161,7 +161,7 @@
41.4 | conn @{const_name Not} = SOME "not"
41.5 | conn @{const_name "op &"} = SOME "and"
41.6 | conn @{const_name "op |"} = SOME "or"
41.7 - | conn @{const_name "op -->"} = SOME "implies"
41.8 + | conn @{const_name HOL.implies} = SOME "implies"
41.9 | conn @{const_name "op ="} = SOME "iff"
41.10 | conn @{const_name If} = SOME "if_then_else"
41.11 | conn _ = NONE
42.1 --- a/src/HOL/Tools/SMT/z3_interface.ML Fri Aug 27 09:34:06 2010 +0200
42.2 +++ b/src/HOL/Tools/SMT/z3_interface.ML Fri Aug 27 09:43:52 2010 +0200
42.3 @@ -170,7 +170,7 @@
42.4 val mk_true = @{cterm "~False"}
42.5 val mk_false = @{cterm False}
42.6 val mk_not = Thm.capply @{cterm Not}
42.7 -val mk_implies = Thm.mk_binop @{cterm "op -->"}
42.8 +val mk_implies = Thm.mk_binop @{cterm HOL.implies}
42.9 val mk_iff = Thm.mk_binop @{cterm "op = :: bool => _"}
42.10
42.11 fun mk_nary _ cu [] = cu
43.1 --- a/src/HOL/Tools/SMT/z3_proof_tools.ML Fri Aug 27 09:34:06 2010 +0200
43.2 +++ b/src/HOL/Tools/SMT/z3_proof_tools.ML Fri Aug 27 09:43:52 2010 +0200
43.3 @@ -198,7 +198,7 @@
43.4 | @{term Not} $ _ => abstr1 cvs ct
43.5 | @{term "op &"} $ _ $ _ => abstr2 cvs ct
43.6 | @{term "op |"} $ _ $ _ => abstr2 cvs ct
43.7 - | @{term "op -->"} $ _ $ _ => abstr2 cvs ct
43.8 + | @{term HOL.implies} $ _ $ _ => abstr2 cvs ct
43.9 | Const (@{const_name "op ="}, _) $ _ $ _ => abstr2 cvs ct
43.10 | Const (@{const_name distinct}, _) $ _ =>
43.11 if ext_logic then abs_arg (abs_list abstr fresh_abstraction) cvs ct
44.1 --- a/src/HOL/Tools/Sledgehammer/metis_clauses.ML Fri Aug 27 09:34:06 2010 +0200
44.2 +++ b/src/HOL/Tools/Sledgehammer/metis_clauses.ML Fri Aug 27 09:43:52 2010 +0200
44.3 @@ -38,11 +38,10 @@
44.4 val const_prefix: string
44.5 val type_const_prefix: string
44.6 val class_prefix: string
44.7 - val union_all: ''a list list -> ''a list
44.8 val invert_const: string -> string
44.9 val ascii_of: string -> string
44.10 - val undo_ascii_of: string -> string
44.11 - val strip_prefix_and_undo_ascii: string -> string -> string option
44.12 + val unascii_of: string -> string
44.13 + val strip_prefix_and_unascii: string -> string -> string option
44.14 val make_bound_var : string -> string
44.15 val make_schematic_var : string * int -> string
44.16 val make_fixed_var : string -> string
44.17 @@ -98,7 +97,7 @@
44.18 (@{const_name "op ="}, "equal"),
44.19 (@{const_name "op &"}, "and"),
44.20 (@{const_name "op |"}, "or"),
44.21 - (@{const_name "op -->"}, "implies"),
44.22 + (@{const_name HOL.implies}, "implies"),
44.23 (@{const_name Set.member}, "member"),
44.24 (@{const_name fequal}, "fequal"),
44.25 (@{const_name COMBI}, "COMBI"),
44.26 @@ -121,7 +120,7 @@
44.27 Alphanumeric characters are left unchanged.
44.28 The character _ goes to __
44.29 Characters in the range ASCII space to / go to _A to _P, respectively.
44.30 - Other printing characters go to _nnn where nnn is the decimal ASCII code.*)
44.31 + Other characters go to _nnn where nnn is the decimal ASCII code.*)
44.32 val A_minus_space = Char.ord #"A" - Char.ord #" ";
44.33
44.34 fun stringN_of_int 0 _ = ""
44.35 @@ -132,9 +131,7 @@
44.36 else if c = #"_" then "__"
44.37 else if #" " <= c andalso c <= #"/"
44.38 then "_" ^ String.str (Char.chr (Char.ord c + A_minus_space))
44.39 - else if Char.isPrint c
44.40 - then ("_" ^ stringN_of_int 3 (Char.ord c)) (*fixed width, in case more digits follow*)
44.41 - else ""
44.42 + else ("_" ^ stringN_of_int 3 (Char.ord c)) (*fixed width, in case more digits follow*)
44.43
44.44 val ascii_of = String.translate ascii_of_c;
44.45
44.46 @@ -142,29 +139,28 @@
44.47
44.48 (*We don't raise error exceptions because this code can run inside the watcher.
44.49 Also, the errors are "impossible" (hah!)*)
44.50 -fun undo_ascii_aux rcs [] = String.implode(rev rcs)
44.51 - | undo_ascii_aux rcs [#"_"] = undo_ascii_aux (#"_"::rcs) [] (*ERROR*)
44.52 +fun unascii_aux rcs [] = String.implode(rev rcs)
44.53 + | unascii_aux rcs [#"_"] = unascii_aux (#"_"::rcs) [] (*ERROR*)
44.54 (*Three types of _ escapes: __, _A to _P, _nnn*)
44.55 - | undo_ascii_aux rcs (#"_" :: #"_" :: cs) = undo_ascii_aux (#"_"::rcs) cs
44.56 - | undo_ascii_aux rcs (#"_" :: c :: cs) =
44.57 + | unascii_aux rcs (#"_" :: #"_" :: cs) = unascii_aux (#"_"::rcs) cs
44.58 + | unascii_aux rcs (#"_" :: c :: cs) =
44.59 if #"A" <= c andalso c<= #"P" (*translation of #" " to #"/"*)
44.60 - then undo_ascii_aux (Char.chr(Char.ord c - A_minus_space) :: rcs) cs
44.61 + then unascii_aux (Char.chr(Char.ord c - A_minus_space) :: rcs) cs
44.62 else
44.63 let val digits = List.take (c::cs, 3) handle Subscript => []
44.64 in
44.65 case Int.fromString (String.implode digits) of
44.66 - NONE => undo_ascii_aux (c:: #"_"::rcs) cs (*ERROR*)
44.67 - | SOME n => undo_ascii_aux (Char.chr n :: rcs) (List.drop (cs, 2))
44.68 + NONE => unascii_aux (c:: #"_"::rcs) cs (*ERROR*)
44.69 + | SOME n => unascii_aux (Char.chr n :: rcs) (List.drop (cs, 2))
44.70 end
44.71 - | undo_ascii_aux rcs (c::cs) = undo_ascii_aux (c::rcs) cs;
44.72 -
44.73 -val undo_ascii_of = undo_ascii_aux [] o String.explode;
44.74 + | unascii_aux rcs (c::cs) = unascii_aux (c::rcs) cs
44.75 +val unascii_of = unascii_aux [] o String.explode
44.76
44.77 (* If string s has the prefix s1, return the result of deleting it,
44.78 un-ASCII'd. *)
44.79 -fun strip_prefix_and_undo_ascii s1 s =
44.80 +fun strip_prefix_and_unascii s1 s =
44.81 if String.isPrefix s1 s then
44.82 - SOME (undo_ascii_of (String.extract (s, size s1, NONE)))
44.83 + SOME (unascii_of (String.extract (s, size s1, NONE)))
44.84 else
44.85 NONE
44.86
44.87 @@ -514,8 +510,8 @@
44.88 (*Type constructors used to instantiate overloaded constants are the only ones needed.*)
44.89 fun add_type_consts_in_term thy =
44.90 let
44.91 - val const_typargs = Sign.const_typargs thy
44.92 - fun aux (Const x) = fold (fold_type_consts set_insert) (const_typargs x)
44.93 + fun aux (Const x) =
44.94 + fold (fold_type_consts set_insert) (Sign.const_typargs thy x)
44.95 | aux (Abs (_, _, u)) = aux u
44.96 | aux (Const (@{const_name skolem_id}, _) $ _) = I
44.97 | aux (t $ u) = aux t #> aux u
45.1 --- a/src/HOL/Tools/Sledgehammer/metis_tactics.ML Fri Aug 27 09:34:06 2010 +0200
45.2 +++ b/src/HOL/Tools/Sledgehammer/metis_tactics.ML Fri Aug 27 09:43:52 2010 +0200
45.3 @@ -228,15 +228,15 @@
45.4 | smart_invert_const s = invert_const s
45.5
45.6 fun hol_type_from_metis_term _ (Metis.Term.Var v) =
45.7 - (case strip_prefix_and_undo_ascii tvar_prefix v of
45.8 + (case strip_prefix_and_unascii tvar_prefix v of
45.9 SOME w => make_tvar w
45.10 | NONE => make_tvar v)
45.11 | hol_type_from_metis_term ctxt (Metis.Term.Fn(x, tys)) =
45.12 - (case strip_prefix_and_undo_ascii type_const_prefix x of
45.13 + (case strip_prefix_and_unascii type_const_prefix x of
45.14 SOME tc => Term.Type (smart_invert_const tc,
45.15 map (hol_type_from_metis_term ctxt) tys)
45.16 | NONE =>
45.17 - case strip_prefix_and_undo_ascii tfree_prefix x of
45.18 + case strip_prefix_and_unascii tfree_prefix x of
45.19 SOME tf => mk_tfree ctxt tf
45.20 | NONE => raise Fail ("hol_type_from_metis_term: " ^ x));
45.21
45.22 @@ -246,10 +246,10 @@
45.23 val _ = trace_msg (fn () => "hol_term_from_metis_PT: " ^
45.24 Metis.Term.toString fol_tm)
45.25 fun tm_to_tt (Metis.Term.Var v) =
45.26 - (case strip_prefix_and_undo_ascii tvar_prefix v of
45.27 + (case strip_prefix_and_unascii tvar_prefix v of
45.28 SOME w => Type (make_tvar w)
45.29 | NONE =>
45.30 - case strip_prefix_and_undo_ascii schematic_var_prefix v of
45.31 + case strip_prefix_and_unascii schematic_var_prefix v of
45.32 SOME w => Term (mk_var (w, HOLogic.typeT))
45.33 | NONE => Term (mk_var (v, HOLogic.typeT)) )
45.34 (*Var from Metis with a name like _nnn; possibly a type variable*)
45.35 @@ -266,7 +266,7 @@
45.36 and applic_to_tt ("=",ts) =
45.37 Term (list_comb(Const (@{const_name "op ="}, HOLogic.typeT), terms_of (map tm_to_tt ts)))
45.38 | applic_to_tt (a,ts) =
45.39 - case strip_prefix_and_undo_ascii const_prefix a of
45.40 + case strip_prefix_and_unascii const_prefix a of
45.41 SOME b =>
45.42 let val c = smart_invert_const b
45.43 val ntypes = num_type_args thy c
45.44 @@ -284,14 +284,14 @@
45.45 cat_lines (map (Syntax.string_of_term ctxt) (terms_of tts)))
45.46 end
45.47 | NONE => (*Not a constant. Is it a type constructor?*)
45.48 - case strip_prefix_and_undo_ascii type_const_prefix a of
45.49 + case strip_prefix_and_unascii type_const_prefix a of
45.50 SOME b =>
45.51 Type (Term.Type (smart_invert_const b, types_of (map tm_to_tt ts)))
45.52 | NONE => (*Maybe a TFree. Should then check that ts=[].*)
45.53 - case strip_prefix_and_undo_ascii tfree_prefix a of
45.54 + case strip_prefix_and_unascii tfree_prefix a of
45.55 SOME b => Type (mk_tfree ctxt b)
45.56 | NONE => (*a fixed variable? They are Skolem functions.*)
45.57 - case strip_prefix_and_undo_ascii fixed_var_prefix a of
45.58 + case strip_prefix_and_unascii fixed_var_prefix a of
45.59 SOME b =>
45.60 let val opr = Term.Free(b, HOLogic.typeT)
45.61 in apply_list opr (length ts) (map tm_to_tt ts) end
45.62 @@ -307,16 +307,16 @@
45.63 let val _ = trace_msg (fn () => "hol_term_from_metis_FT: " ^
45.64 Metis.Term.toString fol_tm)
45.65 fun cvt (Metis.Term.Fn ("ti", [Metis.Term.Var v, _])) =
45.66 - (case strip_prefix_and_undo_ascii schematic_var_prefix v of
45.67 + (case strip_prefix_and_unascii schematic_var_prefix v of
45.68 SOME w => mk_var(w, dummyT)
45.69 | NONE => mk_var(v, dummyT))
45.70 | cvt (Metis.Term.Fn ("ti", [Metis.Term.Fn ("=",[]), _])) =
45.71 Const (@{const_name "op ="}, HOLogic.typeT)
45.72 | cvt (Metis.Term.Fn ("ti", [Metis.Term.Fn (x,[]), ty])) =
45.73 - (case strip_prefix_and_undo_ascii const_prefix x of
45.74 + (case strip_prefix_and_unascii const_prefix x of
45.75 SOME c => Const (smart_invert_const c, dummyT)
45.76 | NONE => (*Not a constant. Is it a fixed variable??*)
45.77 - case strip_prefix_and_undo_ascii fixed_var_prefix x of
45.78 + case strip_prefix_and_unascii fixed_var_prefix x of
45.79 SOME v => Free (v, hol_type_from_metis_term ctxt ty)
45.80 | NONE => raise Fail ("hol_term_from_metis_FT bad constant: " ^ x))
45.81 | cvt (Metis.Term.Fn ("ti", [Metis.Term.Fn (".",[tm1,tm2]), _])) =
45.82 @@ -327,10 +327,10 @@
45.83 | cvt (Metis.Term.Fn ("=", [tm1,tm2])) =
45.84 list_comb(Const (@{const_name "op ="}, HOLogic.typeT), map cvt [tm1,tm2])
45.85 | cvt (t as Metis.Term.Fn (x, [])) =
45.86 - (case strip_prefix_and_undo_ascii const_prefix x of
45.87 + (case strip_prefix_and_unascii const_prefix x of
45.88 SOME c => Const (smart_invert_const c, dummyT)
45.89 | NONE => (*Not a constant. Is it a fixed variable??*)
45.90 - case strip_prefix_and_undo_ascii fixed_var_prefix x of
45.91 + case strip_prefix_and_unascii fixed_var_prefix x of
45.92 SOME v => Free (v, dummyT)
45.93 | NONE => (trace_msg (fn () => "hol_term_from_metis_FT bad const: " ^ x);
45.94 hol_term_from_metis_PT ctxt t))
45.95 @@ -410,11 +410,11 @@
45.96 " in " ^ Display.string_of_thm ctxt i_th);
45.97 NONE)
45.98 fun remove_typeinst (a, t) =
45.99 - case strip_prefix_and_undo_ascii schematic_var_prefix a of
45.100 + case strip_prefix_and_unascii schematic_var_prefix a of
45.101 SOME b => SOME (b, t)
45.102 - | NONE => case strip_prefix_and_undo_ascii tvar_prefix a of
45.103 + | NONE => case strip_prefix_and_unascii tvar_prefix a of
45.104 SOME _ => NONE (*type instantiations are forbidden!*)
45.105 - | NONE => SOME (a,t) (*internal Metis var?*)
45.106 + | NONE => SOME (a,t) (*internal Metis var?*)
45.107 val _ = trace_msg (fn () => " isa th: " ^ Display.string_of_thm ctxt i_th)
45.108 val substs = map_filter remove_typeinst (Metis.Subst.toList fsubst)
45.109 val (vars,rawtms) = ListPair.unzip (map_filter subst_translation substs)
46.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer.ML Fri Aug 27 09:34:06 2010 +0200
46.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer.ML Fri Aug 27 09:43:52 2010 +0200
46.3 @@ -9,6 +9,7 @@
46.4 signature SLEDGEHAMMER =
46.5 sig
46.6 type failure = ATP_Systems.failure
46.7 + type locality = Sledgehammer_Fact_Filter.locality
46.8 type relevance_override = Sledgehammer_Fact_Filter.relevance_override
46.9 type minimize_command = Sledgehammer_Proof_Reconstruct.minimize_command
46.10 type params =
46.11 @@ -18,11 +19,9 @@
46.12 atps: string list,
46.13 full_types: bool,
46.14 explicit_apply: bool,
46.15 - relevance_threshold: real,
46.16 - relevance_convergence: real,
46.17 - max_relevant_per_iter: int option,
46.18 + relevance_thresholds: real * real,
46.19 + max_relevant: int option,
46.20 theory_relevant: bool option,
46.21 - defs_relevant: bool,
46.22 isar_proof: bool,
46.23 isar_shrink_factor: int,
46.24 timeout: Time.time}
46.25 @@ -30,16 +29,16 @@
46.26 {subgoal: int,
46.27 goal: Proof.context * (thm list * thm),
46.28 relevance_override: relevance_override,
46.29 - axioms: ((string * bool) * thm) list option}
46.30 + axioms: ((string * locality) * thm) list option}
46.31 type prover_result =
46.32 {outcome: failure option,
46.33 message: string,
46.34 pool: string Symtab.table,
46.35 - used_thm_names: (string * bool) list,
46.36 + used_thm_names: (string * locality) list,
46.37 atp_run_time_in_msecs: int,
46.38 output: string,
46.39 proof: string,
46.40 - axiom_names: (string * bool) vector,
46.41 + axiom_names: (string * locality) vector,
46.42 conjecture_shape: int list list}
46.43 type prover = params -> minimize_command -> problem -> prover_result
46.44
46.45 @@ -87,11 +86,9 @@
46.46 atps: string list,
46.47 full_types: bool,
46.48 explicit_apply: bool,
46.49 - relevance_threshold: real,
46.50 - relevance_convergence: real,
46.51 - max_relevant_per_iter: int option,
46.52 + relevance_thresholds: real * real,
46.53 + max_relevant: int option,
46.54 theory_relevant: bool option,
46.55 - defs_relevant: bool,
46.56 isar_proof: bool,
46.57 isar_shrink_factor: int,
46.58 timeout: Time.time}
46.59 @@ -100,17 +97,17 @@
46.60 {subgoal: int,
46.61 goal: Proof.context * (thm list * thm),
46.62 relevance_override: relevance_override,
46.63 - axioms: ((string * bool) * thm) list option}
46.64 + axioms: ((string * locality) * thm) list option}
46.65
46.66 type prover_result =
46.67 {outcome: failure option,
46.68 message: string,
46.69 pool: string Symtab.table,
46.70 - used_thm_names: (string * bool) list,
46.71 + used_thm_names: (string * locality) list,
46.72 atp_run_time_in_msecs: int,
46.73 output: string,
46.74 proof: string,
46.75 - axiom_names: (string * bool) vector,
46.76 + axiom_names: (string * locality) vector,
46.77 conjecture_shape: int list list}
46.78
46.79 type prover = params -> minimize_command -> problem -> prover_result
46.80 @@ -174,10 +171,9 @@
46.81 Scan.this_string set_ClauseFormulaRelationN |-- $$ "("
46.82 |-- Scan.repeat parse_clause_formula_pair
46.83 val extract_clause_formula_relation =
46.84 - Substring.full
46.85 - #> Substring.position set_ClauseFormulaRelationN
46.86 - #> snd #> Substring.string #> strip_spaces #> explode
46.87 - #> parse_clause_formula_relation #> fst
46.88 + Substring.full #> Substring.position set_ClauseFormulaRelationN
46.89 + #> snd #> Substring.string #> strip_spaces_except_between_ident_chars
46.90 + #> explode #> parse_clause_formula_relation #> fst
46.91
46.92 fun repair_conjecture_shape_and_theorem_names output conjecture_shape
46.93 axiom_names =
46.94 @@ -190,17 +186,19 @@
46.95 val seq = extract_clause_sequence output
46.96 val name_map = extract_clause_formula_relation output
46.97 fun renumber_conjecture j =
46.98 - conjecture_prefix ^ Int.toString (j - j0)
46.99 + conjecture_prefix ^ string_of_int (j - j0)
46.100 |> AList.find (fn (s, ss) => member (op =) ss s) name_map
46.101 |> map (fn s => find_index (curry (op =) s) seq + 1)
46.102 fun name_for_number j =
46.103 let
46.104 val axioms =
46.105 - j |> AList.lookup (op =) name_map
46.106 - |> these |> map_filter (try (unprefix axiom_prefix))
46.107 - |> map undo_ascii_of
46.108 - val chained = forall (is_true_for axiom_names) axioms
46.109 - in (axioms |> space_implode " ", chained) end
46.110 + j |> AList.lookup (op =) name_map |> these
46.111 + |> map_filter (try (unprefix axiom_prefix)) |> map unascii_of
46.112 + val loc =
46.113 + case axioms of
46.114 + [axiom] => find_first_in_vector axiom_names axiom General
46.115 + | _ => General
46.116 + in (axioms |> space_implode " ", loc) end
46.117 in
46.118 (conjecture_shape |> map (maps renumber_conjecture),
46.119 seq |> map name_for_number |> Vector.fromList)
46.120 @@ -213,12 +211,11 @@
46.121
46.122 fun prover_fun atp_name
46.123 {exec, required_execs, arguments, has_incomplete_mode, proof_delims,
46.124 - known_failures, default_max_relevant_per_iter, default_theory_relevant,
46.125 + known_failures, default_max_relevant, default_theory_relevant,
46.126 explicit_forall, use_conjecture_for_hypotheses}
46.127 ({debug, verbose, overlord, full_types, explicit_apply,
46.128 - relevance_threshold, relevance_convergence,
46.129 - max_relevant_per_iter, theory_relevant,
46.130 - defs_relevant, isar_proof, isar_shrink_factor, timeout, ...} : params)
46.131 + relevance_thresholds, max_relevant, theory_relevant, isar_proof,
46.132 + isar_shrink_factor, timeout, ...} : params)
46.133 minimize_command
46.134 ({subgoal, goal, relevance_override, axioms} : problem) =
46.135 let
46.136 @@ -226,7 +223,7 @@
46.137 val thy = ProofContext.theory_of ctxt
46.138 val (params, hyp_ts, concl_t) = strip_subgoal th subgoal
46.139
46.140 - fun print s = (priority s; if debug then tracing s else ())
46.141 + val print = priority
46.142 fun print_v f = () |> verbose ? print o f
46.143 fun print_d f = () |> debug ? print o f
46.144
46.145 @@ -234,15 +231,13 @@
46.146 case axioms of
46.147 SOME axioms => axioms
46.148 | NONE =>
46.149 - (relevant_facts full_types relevance_threshold relevance_convergence
46.150 - defs_relevant
46.151 - (the_default default_max_relevant_per_iter
46.152 - max_relevant_per_iter)
46.153 + (relevant_facts full_types relevance_thresholds
46.154 + (the_default default_max_relevant max_relevant)
46.155 (the_default default_theory_relevant theory_relevant)
46.156 relevance_override goal hyp_ts concl_t
46.157 |> tap ((fn n => print_v (fn () =>
46.158 - "Selected " ^ string_of_int n ^ " fact" ^ plural_s n ^
46.159 - " for " ^ quote atp_name ^ ".")) o length))
46.160 + "Selected " ^ string_of_int n ^ " fact" ^ plural_s n ^
46.161 + " for " ^ quote atp_name ^ ".")) o length))
46.162
46.163 (* path to unique problem file *)
46.164 val the_dest_dir = if overlord then getenv "ISABELLE_HOME_USER"
46.165 @@ -261,6 +256,7 @@
46.166 else error ("No such directory: " ^ the_dest_dir ^ ".")
46.167 end;
46.168
46.169 + val measure_run_time = verbose orelse Config.get ctxt measure_runtime
46.170 val command = Path.explode (getenv (fst exec) ^ "/" ^ snd exec)
46.171 (* write out problem file and call prover *)
46.172 fun command_line complete timeout probfile =
46.173 @@ -268,10 +264,8 @@
46.174 val core = File.shell_path command ^ " " ^ arguments complete timeout ^
46.175 " " ^ File.shell_path probfile
46.176 in
46.177 - (if Config.get ctxt measure_runtime then
46.178 - "TIMEFORMAT='%3U'; { time " ^ core ^ " ; }"
46.179 - else
46.180 - "exec " ^ core) ^ " 2>&1"
46.181 + (if measure_run_time then "TIMEFORMAT='%3U'; { time " ^ core ^ " ; }"
46.182 + else "exec " ^ core) ^ " 2>&1"
46.183 end
46.184 fun split_time s =
46.185 let
46.186 @@ -300,14 +294,11 @@
46.187 prefix ("% " ^ command ^ "\n% " ^ timestamp () ^ "\n")
46.188 else
46.189 I)
46.190 - |>> (if Config.get ctxt measure_runtime then split_time
46.191 - else rpair 0)
46.192 + |>> (if measure_run_time then split_time else rpair 0)
46.193 val (proof, outcome) =
46.194 extract_proof_and_outcome complete res_code proof_delims
46.195 known_failures output
46.196 in (output, msecs, proof, outcome) end
46.197 - val _ = print_d (fn () => "Preparing problem for " ^
46.198 - quote atp_name ^ "...")
46.199 val readable_names = debug andalso overlord
46.200 val (problem, pool, conjecture_offset, axiom_names) =
46.201 prepare_problem ctxt readable_names explicit_forall full_types
46.202 @@ -358,6 +349,11 @@
46.203 proof_text isar_proof
46.204 (pool, debug, isar_shrink_factor, ctxt, conjecture_shape)
46.205 (full_types, minimize_command, proof, axiom_names, th, subgoal)
46.206 + |>> (fn message =>
46.207 + message ^ (if verbose then
46.208 + "\nATP CPU time: " ^ string_of_int msecs ^ " ms."
46.209 + else
46.210 + ""))
46.211 | SOME failure => (string_for_failure failure, [])
46.212 in
46.213 {outcome = outcome, message = message, pool = pool,
47.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML Fri Aug 27 09:34:06 2010 +0200
47.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML Fri Aug 27 09:43:52 2010 +0200
47.3 @@ -5,19 +5,21 @@
47.4
47.5 signature SLEDGEHAMMER_FACT_FILTER =
47.6 sig
47.7 + datatype locality = General | Theory | Local | Chained
47.8 +
47.9 type relevance_override =
47.10 {add: Facts.ref list,
47.11 del: Facts.ref list,
47.12 only: bool}
47.13
47.14 val trace : bool Unsynchronized.ref
47.15 - val name_thms_pair_from_ref :
47.16 + val name_thm_pairs_from_ref :
47.17 Proof.context -> unit Symtab.table -> thm list -> Facts.ref
47.18 - -> (unit -> string * bool) * thm list
47.19 + -> ((string * locality) * thm) list
47.20 val relevant_facts :
47.21 - bool -> real -> real -> bool -> int -> bool -> relevance_override
47.22 + bool -> real * real -> int -> bool -> relevance_override
47.23 -> Proof.context * (thm list * 'a) -> term list -> term
47.24 - -> ((string * bool) * thm) list
47.25 + -> ((string * locality) * thm) list
47.26 end;
47.27
47.28 structure Sledgehammer_Fact_Filter : SLEDGEHAMMER_FACT_FILTER =
47.29 @@ -30,6 +32,8 @@
47.30
47.31 val respect_no_atp = true
47.32
47.33 +datatype locality = General | Theory | Local | Chained
47.34 +
47.35 type relevance_override =
47.36 {add: Facts.ref list,
47.37 del: Facts.ref list,
47.38 @@ -37,13 +41,22 @@
47.39
47.40 val sledgehammer_prefix = "Sledgehammer" ^ Long_Name.separator
47.41
47.42 -fun name_thms_pair_from_ref ctxt reserved chained_ths xref =
47.43 - let val ths = ProofContext.get_fact ctxt xref in
47.44 - (fn () => let
47.45 - val name = Facts.string_of_ref xref
47.46 - val name = name |> Symtab.defined reserved name ? quote
47.47 - val chained = forall (member Thm.eq_thm chained_ths) ths
47.48 - in (name, chained) end, ths)
47.49 +fun repair_name reserved multi j name =
47.50 + (name |> Symtab.defined reserved name ? quote) ^
47.51 + (if multi then "(" ^ Int.toString j ^ ")" else "")
47.52 +
47.53 +fun name_thm_pairs_from_ref ctxt reserved chained_ths xref =
47.54 + let
47.55 + val ths = ProofContext.get_fact ctxt xref
47.56 + val name = Facts.string_of_ref xref
47.57 + val multi = length ths > 1
47.58 + in
47.59 + (ths, (1, []))
47.60 + |-> fold (fn th => fn (j, rest) =>
47.61 + (j + 1, ((repair_name reserved multi j name,
47.62 + if member Thm.eq_thm chained_ths th then Chained
47.63 + else General), th) :: rest))
47.64 + |> snd
47.65 end
47.66
47.67 (***************************************************************)
47.68 @@ -53,61 +66,81 @@
47.69 (*** constants with types ***)
47.70
47.71 (*An abstraction of Isabelle types*)
47.72 -datatype const_typ = CTVar | CType of string * const_typ list
47.73 +datatype pseudotype = PVar | PType of string * pseudotype list
47.74 +
47.75 +fun string_for_pseudotype PVar = "?"
47.76 + | string_for_pseudotype (PType (s, Ts)) =
47.77 + (case Ts of
47.78 + [] => ""
47.79 + | [T] => string_for_pseudotype T
47.80 + | Ts => string_for_pseudotypes Ts ^ " ") ^ s
47.81 +and string_for_pseudotypes Ts =
47.82 + "(" ^ commas (map string_for_pseudotype Ts) ^ ")"
47.83
47.84 (*Is the second type an instance of the first one?*)
47.85 -fun match_type (CType(con1,args1)) (CType(con2,args2)) =
47.86 - con1=con2 andalso match_types args1 args2
47.87 - | match_type CTVar _ = true
47.88 - | match_type _ CTVar = false
47.89 -and match_types [] [] = true
47.90 - | match_types (a1::as1) (a2::as2) = match_type a1 a2 andalso match_types as1 as2;
47.91 +fun match_pseudotype (PType (a, T), PType (b, U)) =
47.92 + a = b andalso match_pseudotypes (T, U)
47.93 + | match_pseudotype (PVar, _) = true
47.94 + | match_pseudotype (_, PVar) = false
47.95 +and match_pseudotypes ([], []) = true
47.96 + | match_pseudotypes (T :: Ts, U :: Us) =
47.97 + match_pseudotype (T, U) andalso match_pseudotypes (Ts, Us)
47.98
47.99 (*Is there a unifiable constant?*)
47.100 -fun const_mem const_tab (c, c_typ) =
47.101 - exists (match_types c_typ) (these (Symtab.lookup const_tab c))
47.102 +fun pseudoconst_mem f const_tab (c, c_typ) =
47.103 + exists (curry (match_pseudotypes o f) c_typ)
47.104 + (these (Symtab.lookup const_tab c))
47.105
47.106 -(*Maps a "real" type to a const_typ*)
47.107 -fun const_typ_of (Type (c,typs)) = CType (c, map const_typ_of typs)
47.108 - | const_typ_of (TFree _) = CTVar
47.109 - | const_typ_of (TVar _) = CTVar
47.110 +fun pseudotype_for (Type (c,typs)) = PType (c, map pseudotype_for typs)
47.111 + | pseudotype_for (TFree _) = PVar
47.112 + | pseudotype_for (TVar _) = PVar
47.113 +(* Pairs a constant with the list of its type instantiations. *)
47.114 +fun pseudoconst_for thy (c, T) =
47.115 + (c, map pseudotype_for (Sign.const_typargs thy (c, T)))
47.116 + handle TYPE _ => (c, []) (* Variable (locale constant): monomorphic *)
47.117
47.118 -(*Pairs a constant with the list of its type instantiations (using const_typ)*)
47.119 -fun const_with_typ thy (c,typ) =
47.120 - let val tvars = Sign.const_typargs thy (c,typ) in
47.121 - (c, map const_typ_of tvars) end
47.122 - handle TYPE _ => (c, []) (*Variable (locale constant): monomorphic*)
47.123 +fun string_for_pseudoconst (s, []) = s
47.124 + | string_for_pseudoconst (s, Ts) = s ^ string_for_pseudotypes Ts
47.125 +fun string_for_super_pseudoconst (s, [[]]) = s
47.126 + | string_for_super_pseudoconst (s, Tss) =
47.127 + s ^ "{" ^ commas (map string_for_pseudotypes Tss) ^ "}"
47.128
47.129 -(*Add a const/type pair to the table, but a [] entry means a standard connective,
47.130 - which we ignore.*)
47.131 -fun add_const_to_table (c, ctyps) =
47.132 - Symtab.map_default (c, [ctyps])
47.133 - (fn [] => [] | ctypss => insert (op =) ctyps ctypss)
47.134 +val abs_prefix = "Sledgehammer.abs"
47.135 +val skolem_prefix = "Sledgehammer.sko"
47.136 +
47.137 +(* Add a pseudoconstant to the table, but a [] entry means a standard
47.138 + connective, which we ignore.*)
47.139 +fun add_pseudoconst_to_table also_skolem (c, ctyps) =
47.140 + if also_skolem orelse not (String.isPrefix skolem_prefix c) then
47.141 + Symtab.map_default (c, [ctyps])
47.142 + (fn [] => [] | ctypss => insert (op =) ctyps ctypss)
47.143 + else
47.144 + I
47.145
47.146 fun is_formula_type T = (T = HOLogic.boolT orelse T = propT)
47.147
47.148 -val fresh_prefix = "Sledgehammer.FRESH."
47.149 val flip = Option.map not
47.150 (* These are typically simplified away by "Meson.presimplify". *)
47.151 val boring_consts =
47.152 [@{const_name False}, @{const_name True}, @{const_name If}, @{const_name Let}]
47.153
47.154 -fun get_consts thy pos ts =
47.155 +fun get_pseudoconsts thy also_skolems pos ts =
47.156 let
47.157 (* We include free variables, as well as constants, to handle locales. For
47.158 each quantifiers that must necessarily be skolemized by the ATP, we
47.159 introduce a fresh constant to simulate the effect of Skolemization. *)
47.160 fun do_term t =
47.161 case t of
47.162 - Const x => add_const_to_table (const_with_typ thy x)
47.163 - | Free (s, _) => add_const_to_table (s, [])
47.164 + Const x => add_pseudoconst_to_table also_skolems (pseudoconst_for thy x)
47.165 + | Free (s, _) => add_pseudoconst_to_table also_skolems (s, [])
47.166 | t1 $ t2 => fold do_term [t1, t2]
47.167 - | Abs (_, _, t') => do_term t'
47.168 + | Abs (_, _, t') =>
47.169 + do_term t' #> add_pseudoconst_to_table true (abs_prefix, [])
47.170 | _ => I
47.171 fun do_quantifier will_surely_be_skolemized body_t =
47.172 do_formula pos body_t
47.173 - #> (if will_surely_be_skolemized then
47.174 - add_const_to_table (gensym fresh_prefix, [])
47.175 + #> (if also_skolems andalso will_surely_be_skolemized then
47.176 + add_pseudoconst_to_table true (gensym skolem_prefix, [])
47.177 else
47.178 I)
47.179 and do_term_or_formula T =
47.180 @@ -128,7 +161,7 @@
47.181 do_quantifier (pos = SOME true) body_t
47.182 | @{const "op &"} $ t1 $ t2 => fold (do_formula pos) [t1, t2]
47.183 | @{const "op |"} $ t1 $ t2 => fold (do_formula pos) [t1, t2]
47.184 - | @{const "op -->"} $ t1 $ t2 =>
47.185 + | @{const HOL.implies} $ t1 $ t2 =>
47.186 do_formula (flip pos) t1 #> do_formula pos t2
47.187 | Const (@{const_name "op ="}, Type (_, [T, _])) $ t1 $ t2 =>
47.188 fold (do_term_or_formula T) [t1, t2]
47.189 @@ -164,31 +197,25 @@
47.190
47.191 (**** Constant / Type Frequencies ****)
47.192
47.193 -(*A two-dimensional symbol table counts frequencies of constants. It's keyed first by
47.194 - constant name and second by its list of type instantiations. For the latter, we need
47.195 - a linear ordering on type const_typ list.*)
47.196 +(* A two-dimensional symbol table counts frequencies of constants. It's keyed
47.197 + first by constant name and second by its list of type instantiations. For the
47.198 + latter, we need a linear ordering on "pseudotype list". *)
47.199
47.200 -local
47.201 +fun pseudotype_ord p =
47.202 + case p of
47.203 + (PVar, PVar) => EQUAL
47.204 + | (PVar, PType _) => LESS
47.205 + | (PType _, PVar) => GREATER
47.206 + | (PType q1, PType q2) =>
47.207 + prod_ord fast_string_ord (dict_ord pseudotype_ord) (q1, q2)
47.208
47.209 -fun cons_nr CTVar = 0
47.210 - | cons_nr (CType _) = 1;
47.211 -
47.212 -in
47.213 -
47.214 -fun const_typ_ord TU =
47.215 - case TU of
47.216 - (CType (a, Ts), CType (b, Us)) =>
47.217 - (case fast_string_ord(a,b) of EQUAL => dict_ord const_typ_ord (Ts,Us) | ord => ord)
47.218 - | (T, U) => int_ord (cons_nr T, cons_nr U);
47.219 -
47.220 -end;
47.221 -
47.222 -structure CTtab = Table(type key = const_typ list val ord = dict_ord const_typ_ord);
47.223 +structure CTtab =
47.224 + Table(type key = pseudotype list val ord = dict_ord pseudotype_ord)
47.225
47.226 fun count_axiom_consts theory_relevant thy (_, th) =
47.227 let
47.228 fun do_const (a, T) =
47.229 - let val (c, cts) = const_with_typ thy (a, T) in
47.230 + let val (c, cts) = pseudoconst_for thy (a, T) in
47.231 (* Two-dimensional table update. Constant maps to types maps to
47.232 count. *)
47.233 CTtab.map_default (cts, 0) (Integer.add 1)
47.234 @@ -205,8 +232,8 @@
47.235 (**** Actual Filtering Code ****)
47.236
47.237 (*The frequency of a constant is the sum of those of all instances of its type.*)
47.238 -fun const_frequency const_tab (c, cts) =
47.239 - CTtab.fold (fn (cts', m) => match_types cts cts' ? Integer.add m)
47.240 +fun pseudoconst_freq match const_tab (c, cts) =
47.241 + CTtab.fold (fn (cts', m) => match (cts, cts') ? Integer.add m)
47.242 (the (Symtab.lookup const_tab c)) 0
47.243 handle Option.Option => 0
47.244
47.245 @@ -216,183 +243,206 @@
47.246
47.247 (* "log" seems best in practice. A constant function of one ignores the constant
47.248 frequencies. *)
47.249 -fun rel_log (x : real) = 1.0 + 2.0 / Math.ln (x + 1.0)
47.250 -fun irrel_log (x : real) = Math.ln (x + 19.0) / 6.4
47.251 +fun rel_log n = 1.0 + 2.0 / Math.ln (Real.fromInt n + 1.0)
47.252 +(* TODO: experiment
47.253 +fun irrel_log n = 0.5 + 1.0 / Math.ln (Real.fromInt n + 1.0)
47.254 +*)
47.255 +fun irrel_log n = Math.ln (Real.fromInt n + 19.0) / 6.4
47.256 +
47.257 +(* FUDGE *)
47.258 +val skolem_weight = 1.0
47.259 +val abs_weight = 2.0
47.260
47.261 (* Computes a constant's weight, as determined by its frequency. *)
47.262 -val rel_const_weight = rel_log o real oo const_frequency
47.263 -val irrel_const_weight = irrel_log o real oo const_frequency
47.264 -(* fun irrel_const_weight _ _ = 1.0 FIXME: OLD CODE *)
47.265 -
47.266 -fun axiom_weight const_tab relevant_consts axiom_consts =
47.267 - let
47.268 - val (rel, irrel) = List.partition (const_mem relevant_consts) axiom_consts
47.269 - val rel_weight = fold (curry Real.+ o rel_const_weight const_tab) rel 0.0
47.270 - val irrel_weight = fold (curry Real.+ o irrel_const_weight const_tab) irrel 0.0
47.271 - val res = rel_weight / (rel_weight + irrel_weight)
47.272 - in if Real.isFinite res then res else 0.0 end
47.273 -
47.274 -(* OLD CODE:
47.275 -(*Relevant constants are weighted according to frequency,
47.276 - but irrelevant constants are simply counted. Otherwise, Skolem functions,
47.277 - which are rare, would harm a formula's chances of being picked.*)
47.278 -fun axiom_weight const_tab relevant_consts axiom_consts =
47.279 - let
47.280 - val rel = filter (const_mem relevant_consts) axiom_consts
47.281 - val rel_weight = fold (curry Real.+ o rel_const_weight const_tab) rel 0.0
47.282 - val res = rel_weight / (rel_weight + real (length axiom_consts - length rel))
47.283 - in if Real.isFinite res then res else 0.0 end
47.284 +val rel_weight = rel_log oo pseudoconst_freq match_pseudotypes
47.285 +fun irrel_weight const_tab (c as (s, _)) =
47.286 + if String.isPrefix skolem_prefix s then skolem_weight
47.287 + else if String.isPrefix abs_prefix s then abs_weight
47.288 + else irrel_log (pseudoconst_freq (match_pseudotypes o swap) const_tab c)
47.289 +(* TODO: experiment
47.290 +fun irrel_weight _ _ = 1.0
47.291 *)
47.292
47.293 -(*Multiplies out to a list of pairs: 'a * 'b list -> ('a * 'b) list -> ('a * 'b) list*)
47.294 -fun add_expand_pairs (x, ys) xys = List.foldl (fn (y,acc) => (x,y)::acc) xys ys
47.295 +(* FUDGE *)
47.296 +fun locality_multiplier General = 1.0
47.297 + | locality_multiplier Theory = 1.1
47.298 + | locality_multiplier Local = 1.3
47.299 + | locality_multiplier Chained = 2.0
47.300
47.301 -fun consts_of_term thy t =
47.302 - Symtab.fold add_expand_pairs (get_consts thy (SOME true) [t]) []
47.303 +fun axiom_weight loc const_tab relevant_consts axiom_consts =
47.304 + case axiom_consts |> List.partition (pseudoconst_mem I relevant_consts)
47.305 + ||> filter_out (pseudoconst_mem swap relevant_consts) of
47.306 + ([], []) => 0.0
47.307 + | (_, []) => 1.0
47.308 + | (rel, irrel) =>
47.309 + let
47.310 + val rel_weight = fold (curry Real.+ o rel_weight const_tab) rel 0.0
47.311 + |> curry Real.* (locality_multiplier loc)
47.312 + val irrel_weight = fold (curry Real.+ o irrel_weight const_tab) irrel 0.0
47.313 + val res = rel_weight / (rel_weight + irrel_weight)
47.314 + in if Real.isFinite res then res else 0.0 end
47.315
47.316 +(* TODO: experiment
47.317 +fun debug_axiom_weight const_tab relevant_consts axiom_consts =
47.318 + case axiom_consts |> List.partition (pseudoconst_mem I relevant_consts)
47.319 + ||> filter_out (pseudoconst_mem swap relevant_consts) of
47.320 + ([], []) => 0.0
47.321 + | (_, []) => 1.0
47.322 + | (rel, irrel) =>
47.323 + let
47.324 +val _ = tracing (PolyML.makestring ("REL: ", rel))
47.325 +val _ = tracing (PolyML.makestring ("IRREL: ", irrel))
47.326 + val rel_weight = fold (curry Real.+ o rel_weight const_tab) rel 0.0
47.327 + val irrel_weight = fold (curry Real.+ o irrel_weight const_tab) irrel 0.0
47.328 + val res = rel_weight / (rel_weight + irrel_weight)
47.329 + in if Real.isFinite res then res else 0.0 end
47.330 +*)
47.331 +
47.332 +fun pseudoconsts_of_term thy t =
47.333 + Symtab.fold (fn (x, ys) => fold (fn y => cons (x, y)) ys)
47.334 + (get_pseudoconsts thy true (SOME true) [t]) []
47.335 fun pair_consts_axiom theory_relevant thy axiom =
47.336 (axiom, axiom |> snd |> theory_const_prop_of theory_relevant
47.337 - |> consts_of_term thy)
47.338 -
47.339 -exception CONST_OR_FREE of unit
47.340 -
47.341 -fun dest_Const_or_Free (Const x) = x
47.342 - | dest_Const_or_Free (Free x) = x
47.343 - | dest_Const_or_Free _ = raise CONST_OR_FREE ()
47.344 -
47.345 -(*Look for definitions of the form f ?x1 ... ?xn = t, but not reversed.*)
47.346 -fun defines thy thm gctypes =
47.347 - let val tm = prop_of thm
47.348 - fun defs lhs rhs =
47.349 - let val (rator,args) = strip_comb lhs
47.350 - val ct = const_with_typ thy (dest_Const_or_Free rator)
47.351 - in
47.352 - forall is_Var args andalso const_mem gctypes ct andalso
47.353 - subset (op =) (Term.add_vars rhs [], Term.add_vars lhs [])
47.354 - end
47.355 - handle CONST_OR_FREE () => false
47.356 - in
47.357 - case tm of
47.358 - @{const Trueprop} $ (Const (@{const_name "op ="}, _) $ lhs $ rhs) =>
47.359 - defs lhs rhs
47.360 - | _ => false
47.361 - end;
47.362 + |> pseudoconsts_of_term thy)
47.363
47.364 type annotated_thm =
47.365 - ((unit -> string * bool) * thm) * (string * const_typ list) list
47.366 + (((unit -> string) * locality) * thm) * (string * pseudotype list) list
47.367
47.368 -(*For a reverse sort, putting the largest values first.*)
47.369 -fun compare_pairs ((_, w1), (_, w2)) = Real.compare (w2, w1)
47.370 +fun take_most_relevant max_max_imperfect max_relevant remaining_max
47.371 + (candidates : (annotated_thm * real) list) =
47.372 + let
47.373 + val max_imperfect =
47.374 + Real.ceil (Math.pow (max_max_imperfect,
47.375 + Real.fromInt remaining_max
47.376 + / Real.fromInt max_relevant))
47.377 + val (perfect, imperfect) =
47.378 + candidates |> List.partition (fn (_, w) => w > 0.99999)
47.379 + ||> sort (Real.compare o swap o pairself snd)
47.380 + val ((accepts, more_rejects), rejects) =
47.381 + chop max_imperfect imperfect |>> append perfect |>> chop remaining_max
47.382 + in
47.383 + trace_msg (fn () => "Number of candidates: " ^
47.384 + string_of_int (length candidates));
47.385 + trace_msg (fn () => "Effective threshold: " ^
47.386 + Real.toString (#2 (hd accepts)));
47.387 + trace_msg (fn () => "Actually passed (" ^ Int.toString (length accepts) ^
47.388 + "): " ^ (accepts
47.389 + |> map (fn ((((name, _), _), _), weight) =>
47.390 + name () ^ " [" ^ Real.toString weight ^ "]")
47.391 + |> commas));
47.392 + (accepts, more_rejects @ rejects)
47.393 + end
47.394
47.395 -(* Limit the number of new facts, to prevent runaway acceptance. *)
47.396 -fun take_best max_new (new_pairs : (annotated_thm * real) list) =
47.397 - let val nnew = length new_pairs in
47.398 - if nnew <= max_new then
47.399 - (map #1 new_pairs, [])
47.400 - else
47.401 - let
47.402 - val new_pairs = sort compare_pairs new_pairs
47.403 - val accepted = List.take (new_pairs, max_new)
47.404 - in
47.405 - trace_msg (fn () => ("Number of candidates, " ^ Int.toString nnew ^
47.406 - ", exceeds the limit of " ^ Int.toString max_new));
47.407 - trace_msg (fn () => ("Effective pass mark: " ^ Real.toString (#2 (List.last accepted))));
47.408 - trace_msg (fn () => "Actually passed: " ^
47.409 - space_implode ", " (map (fst o (fn f => f ()) o fst o fst o fst) accepted));
47.410 - (map #1 accepted, List.drop (new_pairs, max_new))
47.411 - end
47.412 - end;
47.413 -
47.414 +(* FUDGE *)
47.415 val threshold_divisor = 2.0
47.416 val ridiculous_threshold = 0.1
47.417 +val max_max_imperfect_fudge_factor = 0.66
47.418
47.419 -fun relevance_filter ctxt relevance_threshold relevance_convergence
47.420 - defs_relevant max_new theory_relevant
47.421 +fun relevance_filter ctxt threshold0 decay max_relevant theory_relevant
47.422 ({add, del, ...} : relevance_override) axioms goal_ts =
47.423 - if relevance_threshold > 1.0 then
47.424 - []
47.425 - else if relevance_threshold < 0.0 then
47.426 - axioms
47.427 - else
47.428 - let
47.429 - val thy = ProofContext.theory_of ctxt
47.430 - val const_tab = fold (count_axiom_consts theory_relevant thy) axioms
47.431 - Symtab.empty
47.432 - val goal_const_tab = get_consts thy (SOME false) goal_ts
47.433 - val _ =
47.434 - trace_msg (fn () => "Initial constants: " ^
47.435 - commas (goal_const_tab
47.436 - |> Symtab.dest
47.437 - |> filter (curry (op <>) [] o snd)
47.438 - |> map fst))
47.439 - val add_thms = maps (ProofContext.get_fact ctxt) add
47.440 - val del_thms = maps (ProofContext.get_fact ctxt) del
47.441 - fun iter j threshold rel_const_tab =
47.442 - let
47.443 - fun relevant ([], rejects) [] =
47.444 - (* Nothing was added this iteration. *)
47.445 - if j = 0 andalso threshold >= ridiculous_threshold then
47.446 - (* First iteration? Try again. *)
47.447 - iter 0 (threshold / threshold_divisor) rel_const_tab
47.448 - (map (apsnd SOME) rejects)
47.449 + let
47.450 + val thy = ProofContext.theory_of ctxt
47.451 + val const_tab = fold (count_axiom_consts theory_relevant thy) axioms
47.452 + Symtab.empty
47.453 + val add_thms = maps (ProofContext.get_fact ctxt) add
47.454 + val del_thms = maps (ProofContext.get_fact ctxt) del
47.455 + val max_max_imperfect =
47.456 + Math.sqrt (Real.fromInt max_relevant * max_max_imperfect_fudge_factor)
47.457 + fun iter j remaining_max threshold rel_const_tab hopeless hopeful =
47.458 + let
47.459 + fun game_over rejects =
47.460 + (* Add "add:" facts. *)
47.461 + if null add_thms then
47.462 + []
47.463 + else
47.464 + map_filter (fn ((p as (_, th), _), _) =>
47.465 + if member Thm.eq_thm add_thms th then SOME p
47.466 + else NONE) rejects
47.467 + fun relevant [] rejects hopeless [] =
47.468 + (* Nothing has been added this iteration. *)
47.469 + if j = 0 andalso threshold >= ridiculous_threshold then
47.470 + (* First iteration? Try again. *)
47.471 + iter 0 max_relevant (threshold / threshold_divisor) rel_const_tab
47.472 + hopeless hopeful
47.473 + else
47.474 + game_over (rejects @ hopeless)
47.475 + | relevant candidates rejects hopeless [] =
47.476 + let
47.477 + val (accepts, more_rejects) =
47.478 + take_most_relevant max_max_imperfect max_relevant remaining_max
47.479 + candidates
47.480 + val rel_const_tab' =
47.481 + rel_const_tab
47.482 + |> fold (add_pseudoconst_to_table false)
47.483 + (maps (snd o fst) accepts)
47.484 + fun is_dirty (c, _) =
47.485 + Symtab.lookup rel_const_tab' c <> Symtab.lookup rel_const_tab c
47.486 + val (hopeful_rejects, hopeless_rejects) =
47.487 + (rejects @ hopeless, ([], []))
47.488 + |-> fold (fn (ax as (_, consts), old_weight) =>
47.489 + if exists is_dirty consts then
47.490 + apfst (cons (ax, NONE))
47.491 + else
47.492 + apsnd (cons (ax, old_weight)))
47.493 + |>> append (more_rejects
47.494 + |> map (fn (ax as (_, consts), old_weight) =>
47.495 + (ax, if exists is_dirty consts then NONE
47.496 + else SOME old_weight)))
47.497 + val threshold =
47.498 + threshold + (1.0 - threshold)
47.499 + * Math.pow (decay, Real.fromInt (length accepts))
47.500 + val remaining_max = remaining_max - length accepts
47.501 + in
47.502 + trace_msg (fn () => "New or updated constants: " ^
47.503 + commas (rel_const_tab' |> Symtab.dest
47.504 + |> subtract (op =) (Symtab.dest rel_const_tab)
47.505 + |> map string_for_super_pseudoconst));
47.506 + map (fst o fst) accepts @
47.507 + (if remaining_max = 0 then
47.508 + game_over (hopeful_rejects @ map (apsnd SOME) hopeless_rejects)
47.509 + else
47.510 + iter (j + 1) remaining_max threshold rel_const_tab'
47.511 + hopeless_rejects hopeful_rejects)
47.512 + end
47.513 + | relevant candidates rejects hopeless
47.514 + (((ax as (((_, loc), th), axiom_consts)), cached_weight)
47.515 + :: hopeful) =
47.516 + let
47.517 + val weight =
47.518 + case cached_weight of
47.519 + SOME w => w
47.520 + | NONE => axiom_weight loc const_tab rel_const_tab axiom_consts
47.521 +(* TODO: experiment
47.522 +val name = fst (fst (fst ax)) ()
47.523 +val _ = if String.isPrefix "lift.simps(3" name then
47.524 +tracing ("*** " ^ name ^ PolyML.makestring (debug_axiom_weight const_tab rel_const_tab axiom_consts))
47.525 +else
47.526 +()
47.527 +*)
47.528 + in
47.529 + if weight >= threshold then
47.530 + relevant ((ax, weight) :: candidates) rejects hopeless hopeful
47.531 else
47.532 - (* Add "add:" facts. *)
47.533 - if null add_thms then
47.534 - []
47.535 - else
47.536 - map_filter (fn ((p as (_, th), _), _) =>
47.537 - if member Thm.eq_thm add_thms th then SOME p
47.538 - else NONE) rejects
47.539 - | relevant (new_pairs, rejects) [] =
47.540 - let
47.541 - val (new_rels, more_rejects) = take_best max_new new_pairs
47.542 - val rel_const_tab' =
47.543 - rel_const_tab |> fold add_const_to_table (maps snd new_rels)
47.544 - fun is_dirty c =
47.545 - const_mem rel_const_tab' c andalso
47.546 - not (const_mem rel_const_tab c)
47.547 - val rejects =
47.548 - more_rejects @ rejects
47.549 - |> map (fn (ax as (_, consts), old_weight) =>
47.550 - (ax, if exists is_dirty consts then NONE
47.551 - else SOME old_weight))
47.552 - val threshold =
47.553 - threshold + (1.0 - threshold) * relevance_convergence
47.554 - in
47.555 - trace_msg (fn () => "relevant this iteration: " ^
47.556 - Int.toString (length new_rels));
47.557 - map #1 new_rels @ iter (j + 1) threshold rel_const_tab' rejects
47.558 - end
47.559 - | relevant (new_rels, rejects)
47.560 - (((ax as ((name, th), axiom_consts)), cached_weight)
47.561 - :: rest) =
47.562 - let
47.563 - val weight =
47.564 - case cached_weight of
47.565 - SOME w => w
47.566 - | NONE => axiom_weight const_tab rel_const_tab axiom_consts
47.567 - in
47.568 - if weight >= threshold orelse
47.569 - (defs_relevant andalso defines thy th rel_const_tab) then
47.570 - (trace_msg (fn () =>
47.571 - fst (name ()) ^ " passes: " ^ Real.toString weight
47.572 - ^ " consts: " ^ commas (map fst axiom_consts));
47.573 - relevant ((ax, weight) :: new_rels, rejects) rest)
47.574 - else
47.575 - relevant (new_rels, (ax, weight) :: rejects) rest
47.576 - end
47.577 - in
47.578 - trace_msg (fn () => "relevant_facts, current threshold: " ^
47.579 - Real.toString threshold);
47.580 - relevant ([], [])
47.581 - end
47.582 - in
47.583 - axioms |> filter_out (member Thm.eq_thm del_thms o snd)
47.584 - |> map (rpair NONE o pair_consts_axiom theory_relevant thy)
47.585 - |> iter 0 relevance_threshold goal_const_tab
47.586 - |> tap (fn res => trace_msg (fn () =>
47.587 + relevant candidates ((ax, weight) :: rejects) hopeless hopeful
47.588 + end
47.589 + in
47.590 + trace_msg (fn () =>
47.591 + "ITERATION " ^ string_of_int j ^ ": current threshold: " ^
47.592 + Real.toString threshold ^ ", constants: " ^
47.593 + commas (rel_const_tab |> Symtab.dest
47.594 + |> filter (curry (op <>) [] o snd)
47.595 + |> map string_for_super_pseudoconst));
47.596 + relevant [] [] hopeless hopeful
47.597 + end
47.598 + in
47.599 + axioms |> filter_out (member Thm.eq_thm del_thms o snd)
47.600 + |> map (rpair NONE o pair_consts_axiom theory_relevant thy)
47.601 + |> iter 0 max_relevant threshold0
47.602 + (get_pseudoconsts thy false (SOME false) goal_ts) []
47.603 + |> tap (fn res => trace_msg (fn () =>
47.604 "Total relevant: " ^ Int.toString (length res)))
47.605 - end
47.606 + end
47.607 +
47.608
47.609 (***************************************************************)
47.610 (* Retrieving and filtering lemmas *)
47.611 @@ -491,7 +541,7 @@
47.612 | (_, @{const "==>"} $ t1 $ t2) =>
47.613 do_formula (not pos) t1 andalso
47.614 (t2 = @{prop False} orelse do_formula pos t2)
47.615 - | (_, @{const "op -->"} $ t1 $ t2) =>
47.616 + | (_, @{const HOL.implies} $ t1 $ t2) =>
47.617 do_formula (not pos) t1 andalso
47.618 (t2 = @{const False} orelse do_formula pos t2)
47.619 | (_, @{const Not} $ t1) => do_formula (not pos) t1
47.620 @@ -533,22 +583,24 @@
47.621
47.622 fun all_name_thms_pairs ctxt reserved full_types add_thms chained_ths =
47.623 let
47.624 - val is_chained = member Thm.eq_thm chained_ths
47.625 - val global_facts = PureThy.facts_of (ProofContext.theory_of ctxt)
47.626 + val thy = ProofContext.theory_of ctxt
47.627 + val thy_prefix = Context.theory_name thy ^ Long_Name.separator
47.628 + val global_facts = PureThy.facts_of thy
47.629 val local_facts = ProofContext.facts_of ctxt
47.630 val named_locals = local_facts |> Facts.dest_static []
47.631 + val is_chained = member Thm.eq_thm chained_ths
47.632 (* Unnamed, not chained formulas with schematic variables are omitted,
47.633 because they are rejected by the backticks (`...`) parser for some
47.634 reason. *)
47.635 - fun is_bad_unnamed_local th =
47.636 - exists (fn (_, ths) => member Thm.eq_thm ths th) named_locals orelse
47.637 - (exists_subterm is_Var (prop_of th) andalso not (is_chained th))
47.638 + fun is_good_unnamed_local th =
47.639 + forall (fn (_, ths) => not (member Thm.eq_thm ths th)) named_locals
47.640 + andalso (not (exists_subterm is_Var (prop_of th)) orelse (is_chained th))
47.641 val unnamed_locals =
47.642 - local_facts |> Facts.props |> filter_out is_bad_unnamed_local
47.643 + local_facts |> Facts.props |> filter is_good_unnamed_local
47.644 |> map (pair "" o single)
47.645 val full_space =
47.646 - Name_Space.merge (Facts.space_of global_facts, Facts.space_of local_facts);
47.647 - fun add_valid_facts foldx facts =
47.648 + Name_Space.merge (Facts.space_of global_facts, Facts.space_of local_facts)
47.649 + fun add_facts global foldx facts =
47.650 foldx (fn (name0, ths) =>
47.651 if name0 <> "" andalso
47.652 forall (not o member Thm.eq_thm add_thms) ths andalso
47.653 @@ -559,10 +611,16 @@
47.654 I
47.655 else
47.656 let
47.657 + val base_loc =
47.658 + if not global then Local
47.659 + else if String.isPrefix thy_prefix name0 then Theory
47.660 + else General
47.661 val multi = length ths > 1
47.662 fun backquotify th =
47.663 "`" ^ Print_Mode.setmp [Print_Mode.input]
47.664 (Syntax.string_of_term ctxt) (prop_of th) ^ "`"
47.665 + |> String.translate (fn c => if Char.isPrint c then str c else "")
47.666 + |> simplify_spaces
47.667 fun check_thms a =
47.668 case try (ProofContext.get_thms ctxt) a of
47.669 NONE => false
47.670 @@ -575,54 +633,48 @@
47.671 not (member Thm.eq_thm add_thms th) then
47.672 rest
47.673 else
47.674 - (fn () =>
47.675 - (if name0 = "" then
47.676 - th |> backquotify
47.677 - else
47.678 - let
47.679 - val name1 = Facts.extern facts name0
47.680 - val name2 = Name_Space.extern full_space name0
47.681 - in
47.682 - case find_first check_thms [name1, name2, name0] of
47.683 - SOME name =>
47.684 - let
47.685 - val name =
47.686 - name |> Symtab.defined reserved name ? quote
47.687 - in
47.688 - if multi then name ^ "(" ^ Int.toString j ^ ")"
47.689 - else name
47.690 - end
47.691 - | NONE => ""
47.692 - end, is_chained th), (multi, th)) :: rest)) ths
47.693 + (((fn () =>
47.694 + if name0 = "" then
47.695 + th |> backquotify
47.696 + else
47.697 + let
47.698 + val name1 = Facts.extern facts name0
47.699 + val name2 = Name_Space.extern full_space name0
47.700 + in
47.701 + case find_first check_thms [name1, name2, name0] of
47.702 + SOME name => repair_name reserved multi j name
47.703 + | NONE => ""
47.704 + end), if is_chained th then Chained else base_loc),
47.705 + (multi, th)) :: rest)) ths
47.706 #> snd
47.707 end)
47.708 in
47.709 - [] |> add_valid_facts fold local_facts (unnamed_locals @ named_locals)
47.710 - |> add_valid_facts Facts.fold_static global_facts global_facts
47.711 + [] |> add_facts false fold local_facts (unnamed_locals @ named_locals)
47.712 + |> add_facts true Facts.fold_static global_facts global_facts
47.713 end
47.714
47.715 (* The single-name theorems go after the multiple-name ones, so that single
47.716 names are preferred when both are available. *)
47.717 fun name_thm_pairs ctxt respect_no_atp =
47.718 - List.partition (fst o snd) #> op @
47.719 - #> map (apsnd snd)
47.720 + List.partition (fst o snd) #> op @ #> map (apsnd snd)
47.721 #> respect_no_atp ? filter_out (No_ATPs.member ctxt o snd)
47.722
47.723 (***************************************************************)
47.724 (* ATP invocation methods setup *)
47.725 (***************************************************************)
47.726
47.727 -fun relevant_facts full_types relevance_threshold relevance_convergence
47.728 - defs_relevant max_new theory_relevant
47.729 - (relevance_override as {add, del, only})
47.730 +fun relevant_facts full_types (threshold0, threshold1) max_relevant
47.731 + theory_relevant (relevance_override as {add, del, only})
47.732 (ctxt, (chained_ths, _)) hyp_ts concl_t =
47.733 let
47.734 + val decay = 1.0 - Math.pow ((1.0 - threshold1) / (1.0 - threshold0),
47.735 + 1.0 / Real.fromInt (max_relevant + 1))
47.736 val add_thms = maps (ProofContext.get_fact ctxt) add
47.737 val reserved = reserved_isar_keyword_table ()
47.738 val axioms =
47.739 (if only then
47.740 - maps ((fn (n, ths) => map (pair n o pair false) ths)
47.741 - o name_thms_pair_from_ref ctxt reserved chained_ths) add
47.742 + maps (map (fn ((name, loc), th) => ((K name, loc), (true, th)))
47.743 + o name_thm_pairs_from_ref ctxt reserved chained_ths) add
47.744 else
47.745 all_name_thms_pairs ctxt reserved full_types add_thms chained_ths)
47.746 |> name_thm_pairs ctxt (respect_no_atp andalso not only)
47.747 @@ -630,11 +682,14 @@
47.748 in
47.749 trace_msg (fn () => "Considering " ^ Int.toString (length axioms) ^
47.750 " theorems");
47.751 - relevance_filter ctxt relevance_threshold relevance_convergence
47.752 - defs_relevant max_new theory_relevant relevance_override
47.753 - axioms (concl_t :: hyp_ts)
47.754 - |> map (apfst (fn f => f ()))
47.755 - |> sort_wrt (fst o fst)
47.756 + (if threshold0 > 1.0 orelse threshold0 > threshold1 then
47.757 + []
47.758 + else if threshold0 < 0.0 then
47.759 + axioms
47.760 + else
47.761 + relevance_filter ctxt threshold0 decay max_relevant theory_relevant
47.762 + relevance_override axioms (concl_t :: hyp_ts))
47.763 + |> map (apfst (apfst (fn f => f ()))) |> sort_wrt (fst o fst)
47.764 end
47.765
47.766 end;
48.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact_minimize.ML Fri Aug 27 09:34:06 2010 +0200
48.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact_minimize.ML Fri Aug 27 09:43:52 2010 +0200
48.3 @@ -7,11 +7,12 @@
48.4
48.5 signature SLEDGEHAMMER_FACT_MINIMIZE =
48.6 sig
48.7 + type locality = Sledgehammer_Fact_Filter.locality
48.8 type params = Sledgehammer.params
48.9
48.10 val minimize_theorems :
48.11 - params -> int -> int -> Proof.state -> ((string * bool) * thm list) list
48.12 - -> ((string * bool) * thm list) list option * string
48.13 + params -> int -> int -> Proof.state -> ((string * locality) * thm list) list
48.14 + -> ((string * locality) * thm list) list option * string
48.15 val run_minimize : params -> int -> Facts.ref list -> Proof.state -> unit
48.16 end;
48.17
48.18 @@ -40,24 +41,20 @@
48.19 "")
48.20 end
48.21
48.22 -fun test_theorems ({debug, verbose, overlord, atps, full_types,
48.23 - relevance_threshold, relevance_convergence,
48.24 - defs_relevant, isar_proof, isar_shrink_factor, ...}
48.25 - : params)
48.26 +fun test_theorems ({debug, verbose, overlord, atps, full_types, isar_proof,
48.27 + isar_shrink_factor, ...} : params)
48.28 (prover : prover) explicit_apply timeout subgoal state
48.29 - name_thms_pairs =
48.30 + axioms =
48.31 let
48.32 val _ =
48.33 - priority ("Testing " ^ n_theorems (map fst name_thms_pairs) ^ "...")
48.34 + priority ("Testing " ^ n_theorems (map fst axioms) ^ "...")
48.35 val params =
48.36 {debug = debug, verbose = verbose, overlord = overlord, atps = atps,
48.37 full_types = full_types, explicit_apply = explicit_apply,
48.38 - relevance_threshold = relevance_threshold,
48.39 - relevance_convergence = relevance_convergence,
48.40 - max_relevant_per_iter = NONE, theory_relevant = NONE,
48.41 - defs_relevant = defs_relevant, isar_proof = isar_proof,
48.42 + relevance_thresholds = (1.01, 1.01), max_relevant = NONE,
48.43 + theory_relevant = NONE, isar_proof = isar_proof,
48.44 isar_shrink_factor = isar_shrink_factor, timeout = timeout}
48.45 - val axioms = maps (fn (n, ths) => map (pair n) ths) name_thms_pairs
48.46 + val axioms = maps (fn (n, ths) => map (pair n) ths) axioms
48.47 val {context = ctxt, facts, goal} = Proof.goal state
48.48 val problem =
48.49 {subgoal = subgoal, goal = (ctxt, (facts, goal)),
48.50 @@ -67,7 +64,7 @@
48.51 in
48.52 priority (case outcome of
48.53 NONE =>
48.54 - if length used_thm_names = length name_thms_pairs then
48.55 + if length used_thm_names = length axioms then
48.56 "Found proof."
48.57 else
48.58 "Found proof with " ^ n_theorems used_thm_names ^ "."
48.59 @@ -93,10 +90,9 @@
48.60 val fudge_msecs = 1000
48.61
48.62 fun minimize_theorems {atps = [], ...} _ _ _ _ = error "No ATP is set."
48.63 - | minimize_theorems
48.64 - (params as {debug, atps = atp :: _, full_types, isar_proof,
48.65 - isar_shrink_factor, timeout, ...})
48.66 - i n state name_thms_pairs =
48.67 + | minimize_theorems (params as {debug, atps = atp :: _, full_types,
48.68 + isar_proof, isar_shrink_factor, timeout, ...})
48.69 + i n state axioms =
48.70 let
48.71 val thy = Proof.theory_of state
48.72 val prover = get_prover_fun thy atp
48.73 @@ -106,13 +102,12 @@
48.74 val (_, hyp_ts, concl_t) = strip_subgoal goal i
48.75 val explicit_apply =
48.76 not (forall (Meson.is_fol_term thy)
48.77 - (concl_t :: hyp_ts @
48.78 - maps (map prop_of o snd) name_thms_pairs))
48.79 + (concl_t :: hyp_ts @ maps (map prop_of o snd) axioms))
48.80 fun do_test timeout =
48.81 test_theorems params prover explicit_apply timeout i state
48.82 val timer = Timer.startRealTimer ()
48.83 in
48.84 - (case do_test timeout name_thms_pairs of
48.85 + (case do_test timeout axioms of
48.86 result as {outcome = NONE, pool, used_thm_names,
48.87 conjecture_shape, ...} =>
48.88 let
48.89 @@ -122,11 +117,11 @@
48.90 |> Time.fromMilliseconds
48.91 val (min_thms, {proof, axiom_names, ...}) =
48.92 sublinear_minimize (do_test new_timeout)
48.93 - (filter_used_facts used_thm_names name_thms_pairs) ([], result)
48.94 + (filter_used_facts used_thm_names axioms) ([], result)
48.95 val n = length min_thms
48.96 val _ = priority (cat_lines
48.97 ["Minimized: " ^ string_of_int n ^ " theorem" ^ plural_s n] ^
48.98 - (case length (filter (snd o fst) min_thms) of
48.99 + (case length (filter (curry (op =) Chained o snd o fst) min_thms) of
48.100 0 => ""
48.101 | n => " (including " ^ Int.toString n ^ " chained)") ^ ".")
48.102 in
48.103 @@ -154,15 +149,14 @@
48.104 val ctxt = Proof.context_of state
48.105 val reserved = reserved_isar_keyword_table ()
48.106 val chained_ths = #facts (Proof.goal state)
48.107 - val name_thms_pairs =
48.108 - map (apfst (fn f => f ())
48.109 - o name_thms_pair_from_ref ctxt reserved chained_ths) refs
48.110 + val axioms =
48.111 + maps (map (apsnd single)
48.112 + o name_thm_pairs_from_ref ctxt reserved chained_ths) refs
48.113 in
48.114 case subgoal_count state of
48.115 0 => priority "No subgoal!"
48.116 | n =>
48.117 - (kill_atps ();
48.118 - priority (#2 (minimize_theorems params i n state name_thms_pairs)))
48.119 + (kill_atps (); priority (#2 (minimize_theorems params i n state axioms)))
48.120 end
48.121
48.122 end;
49.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Fri Aug 27 09:34:06 2010 +0200
49.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Fri Aug 27 09:43:52 2010 +0200
49.3 @@ -67,11 +67,9 @@
49.4 ("verbose", "false"),
49.5 ("overlord", "false"),
49.6 ("explicit_apply", "false"),
49.7 - ("relevance_threshold", "40"),
49.8 - ("relevance_convergence", "31"),
49.9 - ("max_relevant_per_iter", "smart"),
49.10 + ("relevance_thresholds", "45 95"),
49.11 + ("max_relevant", "smart"),
49.12 ("theory_relevant", "smart"),
49.13 - ("defs_relevant", "false"),
49.14 ("isar_proof", "false"),
49.15 ("isar_shrink_factor", "1")]
49.16
49.17 @@ -84,7 +82,6 @@
49.18 ("partial_types", "full_types"),
49.19 ("implicit_apply", "explicit_apply"),
49.20 ("theory_irrelevant", "theory_relevant"),
49.21 - ("defs_irrelevant", "defs_relevant"),
49.22 ("no_isar_proof", "isar_proof")]
49.23
49.24 val params_for_minimize =
49.25 @@ -158,6 +155,14 @@
49.26 SOME n => n
49.27 | NONE => error ("Parameter " ^ quote name ^
49.28 " must be assigned an integer value.")
49.29 + fun lookup_int_pair name =
49.30 + case lookup name of
49.31 + NONE => (0, 0)
49.32 + | SOME s => case s |> space_explode " " |> map Int.fromString of
49.33 + [SOME n1, SOME n2] => (n1, n2)
49.34 + | _ => error ("Parameter " ^ quote name ^
49.35 + "must be assigned a pair of integer values \
49.36 + \(e.g., \"60 95\")")
49.37 fun lookup_int_option name =
49.38 case lookup name of
49.39 SOME "smart" => NONE
49.40 @@ -168,25 +173,20 @@
49.41 val atps = lookup_string "atps" |> space_explode " "
49.42 val full_types = lookup_bool "full_types"
49.43 val explicit_apply = lookup_bool "explicit_apply"
49.44 - val relevance_threshold =
49.45 - 0.01 * Real.fromInt (lookup_int "relevance_threshold")
49.46 - val relevance_convergence =
49.47 - 0.01 * Real.fromInt (lookup_int "relevance_convergence")
49.48 - val max_relevant_per_iter = lookup_int_option "max_relevant_per_iter"
49.49 + val relevance_thresholds =
49.50 + lookup_int_pair "relevance_thresholds"
49.51 + |> pairself (fn n => 0.01 * Real.fromInt n)
49.52 + val max_relevant = lookup_int_option "max_relevant"
49.53 val theory_relevant = lookup_bool_option "theory_relevant"
49.54 - val defs_relevant = lookup_bool "defs_relevant"
49.55 val isar_proof = lookup_bool "isar_proof"
49.56 val isar_shrink_factor = Int.max (1, lookup_int "isar_shrink_factor")
49.57 val timeout = lookup_time "timeout"
49.58 in
49.59 {debug = debug, verbose = verbose, overlord = overlord, atps = atps,
49.60 full_types = full_types, explicit_apply = explicit_apply,
49.61 - relevance_threshold = relevance_threshold,
49.62 - relevance_convergence = relevance_convergence,
49.63 - max_relevant_per_iter = max_relevant_per_iter,
49.64 - theory_relevant = theory_relevant, defs_relevant = defs_relevant,
49.65 - isar_proof = isar_proof, isar_shrink_factor = isar_shrink_factor,
49.66 - timeout = timeout}
49.67 + relevance_thresholds = relevance_thresholds, max_relevant = max_relevant,
49.68 + theory_relevant = theory_relevant, isar_proof = isar_proof,
49.69 + isar_shrink_factor = isar_shrink_factor, timeout = timeout}
49.70 end
49.71
49.72 fun get_params thy = extract_params (default_raw_params thy)
50.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML Fri Aug 27 09:34:06 2010 +0200
50.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML Fri Aug 27 09:43:52 2010 +0200
50.3 @@ -8,19 +8,20 @@
50.4
50.5 signature SLEDGEHAMMER_PROOF_RECONSTRUCT =
50.6 sig
50.7 + type locality = Sledgehammer_Fact_Filter.locality
50.8 type minimize_command = string list -> string
50.9
50.10 val metis_proof_text:
50.11 - bool * minimize_command * string * (string * bool) vector * thm * int
50.12 - -> string * (string * bool) list
50.13 + bool * minimize_command * string * (string * locality) vector * thm * int
50.14 + -> string * (string * locality) list
50.15 val isar_proof_text:
50.16 string Symtab.table * bool * int * Proof.context * int list list
50.17 - -> bool * minimize_command * string * (string * bool) vector * thm * int
50.18 - -> string * (string * bool) list
50.19 + -> bool * minimize_command * string * (string * locality) vector * thm * int
50.20 + -> string * (string * locality) list
50.21 val proof_text:
50.22 bool -> string Symtab.table * bool * int * Proof.context * int list list
50.23 - -> bool * minimize_command * string * (string * bool) vector * thm * int
50.24 - -> string * (string * bool) list
50.25 + -> bool * minimize_command * string * (string * locality) vector * thm * int
50.26 + -> string * (string * locality) list
50.27 end;
50.28
50.29 structure Sledgehammer_Proof_Reconstruct : SLEDGEHAMMER_PROOF_RECONSTRUCT =
50.30 @@ -68,7 +69,7 @@
50.31 Const (@{const_name Ex}, T) $ Abs (s, T', negate_term t')
50.32 | negate_term (Const (@{const_name Ex}, T) $ Abs (s, T', t')) =
50.33 Const (@{const_name All}, T) $ Abs (s, T', negate_term t')
50.34 - | negate_term (@{const "op -->"} $ t1 $ t2) =
50.35 + | negate_term (@{const HOL.implies} $ t1 $ t2) =
50.36 @{const "op &"} $ t1 $ negate_term t2
50.37 | negate_term (@{const "op &"} $ t1 $ t2) =
50.38 @{const "op |"} $ negate_term t1 $ negate_term t2
50.39 @@ -234,7 +235,7 @@
50.40 fst o Scan.finite Symbol.stopper
50.41 (Scan.error (!! (fn _ => raise Fail "unrecognized ATP output")
50.42 (parse_lines pool)))
50.43 - o explode o strip_spaces
50.44 + o explode o strip_spaces_except_between_ident_chars
50.45
50.46 (**** INTERPRETATION OF TSTP SYNTAX TREES ****)
50.47
50.48 @@ -246,18 +247,18 @@
50.49 constrained by information from type literals, or by type inference. *)
50.50 fun type_from_fo_term tfrees (u as ATerm (a, us)) =
50.51 let val Ts = map (type_from_fo_term tfrees) us in
50.52 - case strip_prefix_and_undo_ascii type_const_prefix a of
50.53 + case strip_prefix_and_unascii type_const_prefix a of
50.54 SOME b => Type (invert_const b, Ts)
50.55 | NONE =>
50.56 if not (null us) then
50.57 raise FO_TERM [u] (* only "tconst"s have type arguments *)
50.58 - else case strip_prefix_and_undo_ascii tfree_prefix a of
50.59 + else case strip_prefix_and_unascii tfree_prefix a of
50.60 SOME b =>
50.61 let val s = "'" ^ b in
50.62 TFree (s, AList.lookup (op =) tfrees s |> the_default HOLogic.typeS)
50.63 end
50.64 | NONE =>
50.65 - case strip_prefix_and_undo_ascii tvar_prefix a of
50.66 + case strip_prefix_and_unascii tvar_prefix a of
50.67 SOME b => TVar (("'" ^ b, 0), HOLogic.typeS)
50.68 | NONE =>
50.69 (* Variable from the ATP, say "X1" *)
50.70 @@ -267,7 +268,7 @@
50.71 (* Type class literal applied to a type. Returns triple of polarity, class,
50.72 type. *)
50.73 fun type_constraint_from_term pos tfrees (u as ATerm (a, us)) =
50.74 - case (strip_prefix_and_undo_ascii class_prefix a,
50.75 + case (strip_prefix_and_unascii class_prefix a,
50.76 map (type_from_fo_term tfrees) us) of
50.77 (SOME b, [T]) => (pos, b, T)
50.78 | _ => raise FO_TERM [u]
50.79 @@ -309,7 +310,7 @@
50.80 [typ_u, term_u] =>
50.81 aux (SOME (type_from_fo_term tfrees typ_u)) extra_us term_u
50.82 | _ => raise FO_TERM us
50.83 - else case strip_prefix_and_undo_ascii const_prefix a of
50.84 + else case strip_prefix_and_unascii const_prefix a of
50.85 SOME "equal" =>
50.86 list_comb (Const (@{const_name "op ="}, HOLogic.typeT),
50.87 map (aux NONE []) us)
50.88 @@ -341,10 +342,10 @@
50.89 val ts = map (aux NONE []) (us @ extra_us)
50.90 val T = map fastype_of ts ---> HOLogic.typeT
50.91 val t =
50.92 - case strip_prefix_and_undo_ascii fixed_var_prefix a of
50.93 + case strip_prefix_and_unascii fixed_var_prefix a of
50.94 SOME b => Free (b, T)
50.95 | NONE =>
50.96 - case strip_prefix_and_undo_ascii schematic_var_prefix a of
50.97 + case strip_prefix_and_unascii schematic_var_prefix a of
50.98 SOME b => Var ((b, 0), T)
50.99 | NONE =>
50.100 if is_tptp_variable a then
50.101 @@ -575,10 +576,10 @@
50.102 String.tokens (fn c => not (Char.isAlphaNum c) andalso c <> #"_")
50.103 fun do_line (tag :: num :: "axiom" :: (rest as _ :: _)) =
50.104 if tag = "cnf" orelse tag = "fof" then
50.105 - (case strip_prefix_and_undo_ascii axiom_prefix (List.last rest) of
50.106 + (case strip_prefix_and_unascii axiom_prefix (List.last rest) of
50.107 SOME name =>
50.108 if member (op =) rest "file" then
50.109 - SOME (name, is_true_for axiom_names name)
50.110 + SOME (name, find_first_in_vector axiom_names name General)
50.111 else
50.112 axiom_name_at_index num
50.113 | NONE => axiom_name_at_index num)
50.114 @@ -624,8 +625,8 @@
50.115
50.116 fun used_facts axiom_names =
50.117 used_facts_in_atp_proof axiom_names
50.118 - #> List.partition snd
50.119 - #> pairself (sort_distinct (string_ord) o map fst)
50.120 + #> List.partition (curry (op =) Chained o snd)
50.121 + #> pairself (sort_distinct (string_ord o pairself fst))
50.122
50.123 fun metis_proof_text (full_types, minimize_command, atp_proof, axiom_names,
50.124 goal, i) =
50.125 @@ -633,9 +634,9 @@
50.126 val (chained_lemmas, other_lemmas) = used_facts axiom_names atp_proof
50.127 val n = Logic.count_prems (prop_of goal)
50.128 in
50.129 - (metis_line full_types i n other_lemmas ^
50.130 - minimize_line minimize_command (other_lemmas @ chained_lemmas),
50.131 - map (rpair false) other_lemmas @ map (rpair true) chained_lemmas)
50.132 + (metis_line full_types i n (map fst other_lemmas) ^
50.133 + minimize_line minimize_command (map fst (other_lemmas @ chained_lemmas)),
50.134 + other_lemmas @ chained_lemmas)
50.135 end
50.136
50.137 (** Isar proof construction and manipulation **)
51.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_translate.ML Fri Aug 27 09:34:06 2010 +0200
51.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_translate.ML Fri Aug 27 09:43:52 2010 +0200
51.3 @@ -18,8 +18,8 @@
51.4 val tfrees_name : string
51.5 val prepare_problem :
51.6 Proof.context -> bool -> bool -> bool -> bool -> term list -> term
51.7 - -> ((string * bool) * thm) list
51.8 - -> string problem * string Symtab.table * int * (string * bool) vector
51.9 + -> ((string * 'a) * thm) list
51.10 + -> string problem * string Symtab.table * int * (string * 'a) vector
51.11 end;
51.12
51.13 structure Sledgehammer_Translate : SLEDGEHAMMER_TRANSLATE =
51.14 @@ -39,11 +39,11 @@
51.15 (* Freshness almost guaranteed! *)
51.16 val sledgehammer_weak_prefix = "Sledgehammer:"
51.17
51.18 -datatype fol_formula =
51.19 - FOLFormula of {name: string,
51.20 - kind: kind,
51.21 - combformula: (name, combterm) formula,
51.22 - ctypes_sorts: typ list}
51.23 +type fol_formula =
51.24 + {name: string,
51.25 + kind: kind,
51.26 + combformula: (name, combterm) formula,
51.27 + ctypes_sorts: typ list}
51.28
51.29 fun mk_anot phi = AConn (ANot, [phi])
51.30 fun mk_aconn c phi1 phi2 = AConn (c, [phi1, phi2])
51.31 @@ -72,7 +72,7 @@
51.32 do_quant bs AExists s T t'
51.33 | @{const "op &"} $ t1 $ t2 => do_conn bs AAnd t1 t2
51.34 | @{const "op |"} $ t1 $ t2 => do_conn bs AOr t1 t2
51.35 - | @{const "op -->"} $ t1 $ t2 => do_conn bs AImplies t1 t2
51.36 + | @{const HOL.implies} $ t1 $ t2 => do_conn bs AImplies t1 t2
51.37 | Const (@{const_name "op ="}, Type (_, [@{typ bool}, _])) $ t1 $ t2 =>
51.38 do_conn bs AIff t1 t2
51.39 | _ => (fn ts => do_term bs (Envir.eta_contract t)
51.40 @@ -127,7 +127,7 @@
51.41 aux Ts (t0 $ eta_expand Ts t1 1)
51.42 | (t0 as @{const "op &"}) $ t1 $ t2 => t0 $ aux Ts t1 $ aux Ts t2
51.43 | (t0 as @{const "op |"}) $ t1 $ t2 => t0 $ aux Ts t1 $ aux Ts t2
51.44 - | (t0 as @{const "op -->"}) $ t1 $ t2 => t0 $ aux Ts t1 $ aux Ts t2
51.45 + | (t0 as @{const HOL.implies}) $ t1 $ t2 => t0 $ aux Ts t1 $ aux Ts t2
51.46 | (t0 as Const (@{const_name "op ="}, Type (_, [@{typ bool}, _])))
51.47 $ t1 $ t2 =>
51.48 t0 $ aux Ts t1 $ aux Ts t2
51.49 @@ -190,15 +190,14 @@
51.50 |> kind <> Axiom ? freeze_term
51.51 val (combformula, ctypes_sorts) = combformula_for_prop thy t []
51.52 in
51.53 - FOLFormula {name = name, combformula = combformula, kind = kind,
51.54 - ctypes_sorts = ctypes_sorts}
51.55 + {name = name, combformula = combformula, kind = kind,
51.56 + ctypes_sorts = ctypes_sorts}
51.57 end
51.58
51.59 -fun make_axiom ctxt presimp ((name, chained), th) =
51.60 +fun make_axiom ctxt presimp ((name, loc), th) =
51.61 case make_formula ctxt presimp name Axiom (prop_of th) of
51.62 - FOLFormula {combformula = AAtom (CombConst (("c_True", _), _, _)), ...} =>
51.63 - NONE
51.64 - | formula => SOME ((name, chained), formula)
51.65 + {combformula = AAtom (CombConst (("c_True", _), _, _)), ...} => NONE
51.66 + | formula => SOME ((name, loc), formula)
51.67 fun make_conjecture ctxt ts =
51.68 let val last = length ts - 1 in
51.69 map2 (fn j => make_formula ctxt true (Int.toString j)
51.70 @@ -215,7 +214,7 @@
51.71 fun count_combformula (AQuant (_, _, phi)) = count_combformula phi
51.72 | count_combformula (AConn (_, phis)) = fold count_combformula phis
51.73 | count_combformula (AAtom tm) = count_combterm tm
51.74 -fun count_fol_formula (FOLFormula {combformula, ...}) =
51.75 +fun count_fol_formula ({combformula, ...} : fol_formula) =
51.76 count_combformula combformula
51.77
51.78 val optional_helpers =
51.79 @@ -326,13 +325,13 @@
51.80 | aux (AAtom tm) = AAtom (fo_term_for_combterm full_types tm)
51.81 in aux end
51.82
51.83 -fun formula_for_axiom full_types (FOLFormula {combformula, ctypes_sorts, ...}) =
51.84 +fun formula_for_axiom full_types
51.85 + ({combformula, ctypes_sorts, ...} : fol_formula) =
51.86 mk_ahorn (map (formula_for_fo_literal o fo_literal_for_type_literal)
51.87 (type_literals_for_types ctypes_sorts))
51.88 (formula_for_combformula full_types combformula)
51.89
51.90 -fun problem_line_for_fact prefix full_types
51.91 - (formula as FOLFormula {name, kind, ...}) =
51.92 +fun problem_line_for_fact prefix full_types (formula as {name, kind, ...}) =
51.93 Fof (prefix ^ ascii_of name, kind, formula_for_axiom full_types formula)
51.94
51.95 fun problem_line_for_class_rel_clause (ClassRelClause {name, subclass,
51.96 @@ -357,11 +356,11 @@
51.97 (fo_literal_for_arity_literal conclLit)))
51.98
51.99 fun problem_line_for_conjecture full_types
51.100 - (FOLFormula {name, kind, combformula, ...}) =
51.101 + ({name, kind, combformula, ...} : fol_formula) =
51.102 Fof (conjecture_prefix ^ name, kind,
51.103 formula_for_combformula full_types combformula)
51.104
51.105 -fun free_type_literals_for_conjecture (FOLFormula {ctypes_sorts, ...}) =
51.106 +fun free_type_literals_for_conjecture ({ctypes_sorts, ...} : fol_formula) =
51.107 map fo_literal_for_type_literal (type_literals_for_types ctypes_sorts)
51.108
51.109 fun problem_line_for_free_type lit =
51.110 @@ -407,7 +406,7 @@
51.111 16383 (* large number *)
51.112 else if full_types then
51.113 0
51.114 - else case strip_prefix_and_undo_ascii const_prefix s of
51.115 + else case strip_prefix_and_unascii const_prefix s of
51.116 SOME s' => num_type_args thy (invert_const s')
51.117 | NONE => 0)
51.118 | min_arity_of _ _ (SOME the_const_tab) s =
52.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML Fri Aug 27 09:34:06 2010 +0200
52.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML Fri Aug 27 09:43:52 2010 +0200
52.3 @@ -6,10 +6,11 @@
52.4
52.5 signature SLEDGEHAMMER_UTIL =
52.6 sig
52.7 - val is_true_for : (string * bool) vector -> string -> bool
52.8 + val find_first_in_vector : (''a * 'b) vector -> ''a -> 'b -> 'b
52.9 val plural_s : int -> string
52.10 val serial_commas : string -> string list -> string list
52.11 - val strip_spaces : string -> string
52.12 + val simplify_spaces : string -> string
52.13 + val strip_spaces_except_between_ident_chars : string -> string
52.14 val parse_bool_option : bool -> string -> string -> bool option
52.15 val parse_time_option : string -> string -> Time.time option
52.16 val scan_integer : string list -> int * string list
52.17 @@ -28,8 +29,9 @@
52.18 structure Sledgehammer_Util : SLEDGEHAMMER_UTIL =
52.19 struct
52.20
52.21 -fun is_true_for v s =
52.22 - Vector.foldl (fn ((s', b'), b) => if s' = s then b' else b) false v
52.23 +fun find_first_in_vector vec key default =
52.24 + Vector.foldl (fn ((key', value'), value) =>
52.25 + if key' = key then value' else value) default vec
52.26
52.27 fun plural_s n = if n = 1 then "" else "s"
52.28
52.29 @@ -39,24 +41,27 @@
52.30 | serial_commas conj [s1, s2, s3] = [s1 ^ ",", s2 ^ ",", conj, s3]
52.31 | serial_commas conj (s :: ss) = s ^ "," :: serial_commas conj ss
52.32
52.33 -fun is_ident_char c = Char.isAlphaNum c orelse c = #"_"
52.34 -
52.35 -fun strip_spaces_in_list [] = ""
52.36 - | strip_spaces_in_list [c1] = if Char.isSpace c1 then "" else str c1
52.37 - | strip_spaces_in_list [c1, c2] =
52.38 - strip_spaces_in_list [c1] ^ strip_spaces_in_list [c2]
52.39 - | strip_spaces_in_list (c1 :: c2 :: c3 :: cs) =
52.40 +fun strip_spaces_in_list _ [] = ""
52.41 + | strip_spaces_in_list _ [c1] = if Char.isSpace c1 then "" else str c1
52.42 + | strip_spaces_in_list is_evil [c1, c2] =
52.43 + strip_spaces_in_list is_evil [c1] ^ strip_spaces_in_list is_evil [c2]
52.44 + | strip_spaces_in_list is_evil (c1 :: c2 :: c3 :: cs) =
52.45 if Char.isSpace c1 then
52.46 - strip_spaces_in_list (c2 :: c3 :: cs)
52.47 + strip_spaces_in_list is_evil (c2 :: c3 :: cs)
52.48 else if Char.isSpace c2 then
52.49 if Char.isSpace c3 then
52.50 - strip_spaces_in_list (c1 :: c3 :: cs)
52.51 + strip_spaces_in_list is_evil (c1 :: c3 :: cs)
52.52 else
52.53 - str c1 ^ (if forall is_ident_char [c1, c3] then " " else "") ^
52.54 - strip_spaces_in_list (c3 :: cs)
52.55 + str c1 ^ (if forall is_evil [c1, c3] then " " else "") ^
52.56 + strip_spaces_in_list is_evil (c3 :: cs)
52.57 else
52.58 - str c1 ^ strip_spaces_in_list (c2 :: c3 :: cs)
52.59 -val strip_spaces = strip_spaces_in_list o String.explode
52.60 + str c1 ^ strip_spaces_in_list is_evil (c2 :: c3 :: cs)
52.61 +fun strip_spaces is_evil = strip_spaces_in_list is_evil o String.explode
52.62 +
52.63 +val simplify_spaces = strip_spaces (K true)
52.64 +
52.65 +fun is_ident_char c = Char.isAlphaNum c orelse c = #"_"
52.66 +val strip_spaces_except_between_ident_chars = strip_spaces is_ident_char
52.67
52.68 fun parse_bool_option option name s =
52.69 (case s of
53.1 --- a/src/HOL/Tools/TFL/dcterm.ML Fri Aug 27 09:34:06 2010 +0200
53.2 +++ b/src/HOL/Tools/TFL/dcterm.ML Fri Aug 27 09:43:52 2010 +0200
53.3 @@ -128,7 +128,7 @@
53.4 val dest_neg = dest_monop @{const_name Not}
53.5 val dest_pair = dest_binop @{const_name Pair}
53.6 val dest_eq = dest_binop @{const_name "op ="}
53.7 -val dest_imp = dest_binop @{const_name "op -->"}
53.8 +val dest_imp = dest_binop @{const_name HOL.implies}
53.9 val dest_conj = dest_binop @{const_name "op &"}
53.10 val dest_disj = dest_binop @{const_name "op |"}
53.11 val dest_select = dest_binder @{const_name Eps}
54.1 --- a/src/HOL/Tools/TFL/usyntax.ML Fri Aug 27 09:34:06 2010 +0200
54.2 +++ b/src/HOL/Tools/TFL/usyntax.ML Fri Aug 27 09:43:52 2010 +0200
54.3 @@ -159,7 +159,7 @@
54.4
54.5
54.6 fun mk_imp{ant,conseq} =
54.7 - let val c = Const(@{const_name "op -->"},HOLogic.boolT --> HOLogic.boolT --> HOLogic.boolT)
54.8 + let val c = Const(@{const_name HOL.implies},HOLogic.boolT --> HOLogic.boolT --> HOLogic.boolT)
54.9 in list_comb(c,[ant,conseq])
54.10 end;
54.11
54.12 @@ -247,7 +247,7 @@
54.13 fun dest_eq(Const(@{const_name "op ="},_) $ M $ N) = {lhs=M, rhs=N}
54.14 | dest_eq _ = raise USYN_ERR "dest_eq" "not an equality";
54.15
54.16 -fun dest_imp(Const(@{const_name "op -->"},_) $ M $ N) = {ant=M, conseq=N}
54.17 +fun dest_imp(Const(@{const_name HOL.implies},_) $ M $ N) = {ant=M, conseq=N}
54.18 | dest_imp _ = raise USYN_ERR "dest_imp" "not an implication";
54.19
54.20 fun dest_forall(Const(@{const_name All},_) $ (a as Abs _)) = fst (dest_abs [] a)
55.1 --- a/src/HOL/Tools/cnf_funcs.ML Fri Aug 27 09:34:06 2010 +0200
55.2 +++ b/src/HOL/Tools/cnf_funcs.ML Fri Aug 27 09:43:52 2010 +0200
55.3 @@ -97,7 +97,7 @@
55.4 | is_atom (Const (@{const_name True}, _)) = false
55.5 | is_atom (Const (@{const_name "op &"}, _) $ _ $ _) = false
55.6 | is_atom (Const (@{const_name "op |"}, _) $ _ $ _) = false
55.7 - | is_atom (Const (@{const_name "op -->"}, _) $ _ $ _) = false
55.8 + | is_atom (Const (@{const_name HOL.implies}, _) $ _ $ _) = false
55.9 | is_atom (Const (@{const_name "op ="}, Type ("fun", @{typ bool} :: _)) $ _ $ _) = false
55.10 | is_atom (Const (@{const_name Not}, _) $ _) = false
55.11 | is_atom _ = true;
55.12 @@ -198,7 +198,7 @@
55.13 in
55.14 disj_cong OF [thm1, thm2]
55.15 end
55.16 - | make_nnf_thm thy (Const (@{const_name "op -->"}, _) $ x $ y) =
55.17 + | make_nnf_thm thy (Const (@{const_name HOL.implies}, _) $ x $ y) =
55.18 let
55.19 val thm1 = make_nnf_thm thy (HOLogic.Not $ x)
55.20 val thm2 = make_nnf_thm thy y
55.21 @@ -232,7 +232,7 @@
55.22 in
55.23 make_nnf_not_disj OF [thm1, thm2]
55.24 end
55.25 - | make_nnf_thm thy (Const (@{const_name Not}, _) $ (Const (@{const_name "op -->"}, _) $ x $ y)) =
55.26 + | make_nnf_thm thy (Const (@{const_name Not}, _) $ (Const (@{const_name HOL.implies}, _) $ x $ y)) =
55.27 let
55.28 val thm1 = make_nnf_thm thy x
55.29 val thm2 = make_nnf_thm thy (HOLogic.Not $ y)
56.1 --- a/src/HOL/Tools/groebner.ML Fri Aug 27 09:34:06 2010 +0200
56.2 +++ b/src/HOL/Tools/groebner.ML Fri Aug 27 09:43:52 2010 +0200
56.3 @@ -931,7 +931,7 @@
56.4 | Const (@{const_name Ex}, _) $ _ => find_body bounds (dest_arg tm)
56.5 | Const (@{const_name "op &"}, _) $ _ $ _ => find_args bounds tm
56.6 | Const (@{const_name "op |"}, _) $ _ $ _ => find_args bounds tm
56.7 - | Const (@{const_name "op -->"}, _) $ _ $ _ => find_args bounds tm
56.8 + | Const (@{const_name HOL.implies}, _) $ _ $ _ => find_args bounds tm
56.9 | @{term "op ==>"} $_$_ => find_args bounds tm
56.10 | Const("op ==",_)$_$_ => find_args bounds tm
56.11 | @{term Trueprop}$_ => find_term bounds (dest_arg tm)
57.1 --- a/src/HOL/Tools/hologic.ML Fri Aug 27 09:34:06 2010 +0200
57.2 +++ b/src/HOL/Tools/hologic.ML Fri Aug 27 09:43:52 2010 +0200
57.3 @@ -210,8 +210,8 @@
57.4
57.5 val conj = @{term "op &"}
57.6 and disj = @{term "op |"}
57.7 -and imp = @{term "op -->"}
57.8 -and Not = @{term "Not"};
57.9 +and imp = @{term implies}
57.10 +and Not = @{term Not};
57.11
57.12 fun mk_conj (t1, t2) = conj $ t1 $ t2
57.13 and mk_disj (t1, t2) = disj $ t1 $ t2
57.14 @@ -230,7 +230,7 @@
57.15
57.16 fun disjuncts t = disjuncts_aux t [];
57.17
57.18 -fun dest_imp (Const ("op -->", _) $ A $ B) = (A, B)
57.19 +fun dest_imp (Const ("HOL.implies", _) $ A $ B) = (A, B)
57.20 | dest_imp t = raise TERM ("dest_imp", [t]);
57.21
57.22 fun dest_not (Const ("HOL.Not", _) $ t) = t
58.1 --- a/src/HOL/Tools/meson.ML Fri Aug 27 09:34:06 2010 +0200
58.2 +++ b/src/HOL/Tools/meson.ML Fri Aug 27 09:43:52 2010 +0200
58.3 @@ -274,7 +274,7 @@
58.4 | signed_nclauses b (Const(@{const_name "op |"},_) $ t $ u) =
58.5 if b then prod (signed_nclauses b t) (signed_nclauses b u)
58.6 else sum (signed_nclauses b t) (signed_nclauses b u)
58.7 - | signed_nclauses b (Const(@{const_name "op -->"},_) $ t $ u) =
58.8 + | signed_nclauses b (Const(@{const_name HOL.implies},_) $ t $ u) =
58.9 if b then prod (signed_nclauses (not b) t) (signed_nclauses b u)
58.10 else sum (signed_nclauses (not b) t) (signed_nclauses b u)
58.11 | signed_nclauses b (Const(@{const_name "op ="}, Type ("fun", [T, _])) $ t $ u) =
58.12 @@ -401,7 +401,7 @@
58.13 since this code expects to be called on a clause form.*)
58.14 val is_conn = member (op =)
58.15 [@{const_name Trueprop}, @{const_name "op &"}, @{const_name "op |"},
58.16 - @{const_name "op -->"}, @{const_name Not},
58.17 + @{const_name HOL.implies}, @{const_name Not},
58.18 @{const_name All}, @{const_name Ex}, @{const_name Ball}, @{const_name Bex}];
58.19
58.20 (*True if the term contains a function--not a logical connective--where the type
59.1 --- a/src/HOL/Tools/quickcheck_generators.ML Fri Aug 27 09:34:06 2010 +0200
59.2 +++ b/src/HOL/Tools/quickcheck_generators.ML Fri Aug 27 09:43:52 2010 +0200
59.3 @@ -342,7 +342,7 @@
59.4 val bound_max = length Ts - 1;
59.5 val bounds = map_index (fn (i, ty) =>
59.6 (2 * (bound_max - i) + 1, 2 * (bound_max - i), 2 * i, ty)) Ts;
59.7 - fun strip_imp (Const(@{const_name "op -->"},_) $ A $ B) = apfst (cons A) (strip_imp B)
59.8 + fun strip_imp (Const(@{const_name HOL.implies},_) $ A $ B) = apfst (cons A) (strip_imp B)
59.9 | strip_imp A = ([], A)
59.10 val prop' = betapplys (prop, map (fn (i, _, _, _) => Bound i) bounds);
59.11 val terms = HOLogic.mk_list @{typ term} (map (fn (_, i, _, _) => Bound i $ @{term "()"}) bounds)
60.1 --- a/src/HOL/Tools/refute.ML Fri Aug 27 09:34:06 2010 +0200
60.2 +++ b/src/HOL/Tools/refute.ML Fri Aug 27 09:43:52 2010 +0200
60.3 @@ -650,7 +650,7 @@
60.4 | Const (@{const_name "op ="}, _) => t
60.5 | Const (@{const_name "op &"}, _) => t
60.6 | Const (@{const_name "op |"}, _) => t
60.7 - | Const (@{const_name "op -->"}, _) => t
60.8 + | Const (@{const_name HOL.implies}, _) => t
60.9 (* sets *)
60.10 | Const (@{const_name Collect}, _) => t
60.11 | Const (@{const_name Set.member}, _) => t
60.12 @@ -826,7 +826,7 @@
60.13 | Const (@{const_name "op ="}, T) => collect_type_axioms T axs
60.14 | Const (@{const_name "op &"}, _) => axs
60.15 | Const (@{const_name "op |"}, _) => axs
60.16 - | Const (@{const_name "op -->"}, _) => axs
60.17 + | Const (@{const_name HOL.implies}, _) => axs
60.18 (* sets *)
60.19 | Const (@{const_name Collect}, T) => collect_type_axioms T axs
60.20 | Const (@{const_name Set.member}, T) => collect_type_axioms T axs
60.21 @@ -1895,7 +1895,7 @@
60.22 (* this would make "undef" propagate, even for formulae like *)
60.23 (* "True | undef": *)
60.24 (* SOME (Node [Node [TT, TT], Node [TT, FF]], model, args) *)
60.25 - | Const (@{const_name "op -->"}, _) $ t1 $ t2 => (* similar to "==>" (Pure) *)
60.26 + | Const (@{const_name HOL.implies}, _) $ t1 $ t2 => (* similar to "==>" (Pure) *)
60.27 (* 3-valued logic *)
60.28 let
60.29 val (i1, m1, a1) = interpret thy model args t1
60.30 @@ -1905,9 +1905,9 @@
60.31 in
60.32 SOME (Leaf [fmTrue, fmFalse], m2, a2)
60.33 end
60.34 - | Const (@{const_name "op -->"}, _) $ t1 =>
60.35 + | Const (@{const_name HOL.implies}, _) $ t1 =>
60.36 SOME (interpret thy model args (eta_expand t 1))
60.37 - | Const (@{const_name "op -->"}, _) =>
60.38 + | Const (@{const_name HOL.implies}, _) =>
60.39 SOME (interpret thy model args (eta_expand t 2))
60.40 (* this would make "undef" propagate, even for formulae like *)
60.41 (* "False --> undef": *)
61.1 --- a/src/HOL/Tools/simpdata.ML Fri Aug 27 09:34:06 2010 +0200
61.2 +++ b/src/HOL/Tools/simpdata.ML Fri Aug 27 09:43:52 2010 +0200
61.3 @@ -14,7 +14,7 @@
61.4 | dest_eq _ = NONE;
61.5 fun dest_conj ((c as Const(@{const_name "op &"},_)) $ s $ t) = SOME (c, s, t)
61.6 | dest_conj _ = NONE;
61.7 - fun dest_imp ((c as Const(@{const_name "op -->"},_)) $ s $ t) = SOME (c, s, t)
61.8 + fun dest_imp ((c as Const(@{const_name HOL.implies},_)) $ s $ t) = SOME (c, s, t)
61.9 | dest_imp _ = NONE;
61.10 val conj = HOLogic.conj
61.11 val imp = HOLogic.imp
61.12 @@ -159,7 +159,7 @@
61.13 (Scan.succeed "Clasimp.clasimpset_of (ML_Context.the_local_context ())");
61.14
61.15 val mksimps_pairs =
61.16 - [(@{const_name "op -->"}, [@{thm mp}]),
61.17 + [(@{const_name HOL.implies}, [@{thm mp}]),
61.18 (@{const_name "op &"}, [@{thm conjunct1}, @{thm conjunct2}]),
61.19 (@{const_name All}, [@{thm spec}]),
61.20 (@{const_name True}, []),
62.1 --- a/src/HOL/ex/Meson_Test.thy Fri Aug 27 09:34:06 2010 +0200
62.2 +++ b/src/HOL/ex/Meson_Test.thy Fri Aug 27 09:43:52 2010 +0200
62.3 @@ -10,7 +10,7 @@
62.4 below and constants declared in HOL!
62.5 *}
62.6
62.7 -hide_const (open) subset quotient union inter sum
62.8 +hide_const (open) implies union inter subset sum quotient
62.9
62.10 text {*
62.11 Test data for the MESON proof procedure
63.1 --- a/src/HOL/ex/Numeral.thy Fri Aug 27 09:34:06 2010 +0200
63.2 +++ b/src/HOL/ex/Numeral.thy Fri Aug 27 09:43:52 2010 +0200
63.3 @@ -1033,14 +1033,14 @@
63.4 (SML "IntInf.- ((_), 1)")
63.5 (OCaml "Big'_int.pred'_big'_int")
63.6 (Haskell "!(_/ -/ 1)")
63.7 - (Scala "!(_/ -/ 1)")
63.8 + (Scala "!(_ -/ 1)")
63.9 (Eval "!(_/ -/ 1)")
63.10
63.11 code_const Int.succ
63.12 (SML "IntInf.+ ((_), 1)")
63.13 (OCaml "Big'_int.succ'_big'_int")
63.14 (Haskell "!(_/ +/ 1)")
63.15 - (Scala "!(_/ +/ 1)")
63.16 + (Scala "!(_ +/ 1)")
63.17 (Eval "!(_/ +/ 1)")
63.18
63.19 code_const "op + \<Colon> int \<Rightarrow> int \<Rightarrow> int"
64.1 --- a/src/HOL/ex/SVC_Oracle.thy Fri Aug 27 09:34:06 2010 +0200
64.2 +++ b/src/HOL/ex/SVC_Oracle.thy Fri Aug 27 09:43:52 2010 +0200
64.3 @@ -90,7 +90,7 @@
64.4 (*abstraction of a formula*)
64.5 and fm ((c as Const(@{const_name "op &"}, _)) $ p $ q) = c $ (fm p) $ (fm q)
64.6 | fm ((c as Const(@{const_name "op |"}, _)) $ p $ q) = c $ (fm p) $ (fm q)
64.7 - | fm ((c as Const(@{const_name "op -->"}, _)) $ p $ q) = c $ (fm p) $ (fm q)
64.8 + | fm ((c as Const(@{const_name HOL.implies}, _)) $ p $ q) = c $ (fm p) $ (fm q)
64.9 | fm ((c as Const(@{const_name Not}, _)) $ p) = c $ (fm p)
64.10 | fm ((c as Const(@{const_name True}, _))) = c
64.11 | fm ((c as Const(@{const_name False}, _))) = c
65.1 --- a/src/HOL/ex/svc_funcs.ML Fri Aug 27 09:34:06 2010 +0200
65.2 +++ b/src/HOL/ex/svc_funcs.ML Fri Aug 27 09:43:52 2010 +0200
65.3 @@ -91,7 +91,7 @@
65.4 in case c of
65.5 Const(@{const_name "op &"}, _) => apply c (map tag ts)
65.6 | Const(@{const_name "op |"}, _) => apply c (map tag ts)
65.7 - | Const(@{const_name "op -->"}, _) => apply c (map tag ts)
65.8 + | Const(@{const_name HOL.implies}, _) => apply c (map tag ts)
65.9 | Const(@{const_name Not}, _) => apply c (map tag ts)
65.10 | Const(@{const_name True}, _) => (c, false)
65.11 | Const(@{const_name False}, _) => (c, false)
65.12 @@ -187,7 +187,7 @@
65.13 Buildin("AND", [fm pos p, fm pos q])
65.14 | fm pos (Const(@{const_name "op |"}, _) $ p $ q) =
65.15 Buildin("OR", [fm pos p, fm pos q])
65.16 - | fm pos (Const(@{const_name "op -->"}, _) $ p $ q) =
65.17 + | fm pos (Const(@{const_name HOL.implies}, _) $ p $ q) =
65.18 Buildin("=>", [fm (not pos) p, fm pos q])
65.19 | fm pos (Const(@{const_name Not}, _) $ p) =
65.20 Buildin("NOT", [fm (not pos) p])
66.1 --- a/src/Pure/General/markup.ML Fri Aug 27 09:34:06 2010 +0200
66.2 +++ b/src/Pure/General/markup.ML Fri Aug 27 09:43:52 2010 +0200
66.3 @@ -99,6 +99,8 @@
66.4 val command_spanN: string val command_span: string -> T
66.5 val ignored_spanN: string val ignored_span: T
66.6 val malformed_spanN: string val malformed_span: T
66.7 + val subgoalsN: string
66.8 + val proof_stateN: string val proof_state: int -> T
66.9 val stateN: string val state: T
66.10 val subgoalN: string val subgoal: T
66.11 val sendbackN: string val sendback: T
66.12 @@ -156,16 +158,13 @@
66.13 fun markup_int elem prop = (elem, fn i => (elem, [(prop, print_int i)]): T);
66.14
66.15
66.16 -(* name *)
66.17 +(* misc properties *)
66.18
66.19 val nameN = "name";
66.20 fun name a = properties [(nameN, a)];
66.21
66.22 val (bindingN, binding) = markup_string "binding" nameN;
66.23
66.24 -
66.25 -(* kind *)
66.26 -
66.27 val kindN = "kind";
66.28
66.29
66.30 @@ -305,6 +304,9 @@
66.31
66.32 (* toplevel *)
66.33
66.34 +val subgoalsN = "subgoals";
66.35 +val (proof_stateN, proof_state) = markup_int "proof_state" subgoalsN;
66.36 +
66.37 val (stateN, state) = markup_elem "state";
66.38 val (subgoalN, subgoal) = markup_elem "subgoal";
66.39 val (sendbackN, sendback) = markup_elem "sendback";
67.1 --- a/src/Pure/General/markup.scala Fri Aug 27 09:34:06 2010 +0200
67.2 +++ b/src/Pure/General/markup.scala Fri Aug 27 09:43:52 2010 +0200
67.3 @@ -9,7 +9,7 @@
67.4
67.5 object Markup
67.6 {
67.7 - /* integers */
67.8 + /* plain values */
67.9
67.10 object Int {
67.11 def apply(i: scala.Int): String = i.toString
67.12 @@ -26,25 +26,33 @@
67.13 }
67.14
67.15
67.16 - /* property values */
67.17 + /* named properties */
67.18
67.19 - def get_string(name: String, props: List[(String, String)]): Option[String] =
67.20 - props.find(p => p._1 == name).map(_._2)
67.21 -
67.22 - def get_long(name: String, props: List[(String, String)]): Option[scala.Long] =
67.23 + class Property(val name: String)
67.24 {
67.25 - get_string(name, props) match {
67.26 - case None => None
67.27 - case Some(Long(i)) => Some(i)
67.28 - }
67.29 + def apply(value: String): List[(String, String)] = List((name, value))
67.30 + def unapply(props: List[(String, String)]): Option[String] =
67.31 + props.find(_._1 == name).map(_._2)
67.32 }
67.33
67.34 - def get_int(name: String, props: List[(String, String)]): Option[scala.Int] =
67.35 + class Int_Property(name: String)
67.36 {
67.37 - get_string(name, props) match {
67.38 - case None => None
67.39 - case Some(Int(i)) => Some(i)
67.40 - }
67.41 + def apply(value: scala.Int): List[(String, String)] = List((name, Int(value)))
67.42 + def unapply(props: List[(String, String)]): Option[Int] =
67.43 + props.find(_._1 == name) match {
67.44 + case None => None
67.45 + case Some((_, value)) => Int.unapply(value)
67.46 + }
67.47 + }
67.48 +
67.49 + class Long_Property(name: String)
67.50 + {
67.51 + def apply(value: scala.Long): List[(String, String)] = List((name, Long(value)))
67.52 + def unapply(props: List[(String, String)]): Option[Long] =
67.53 + props.find(_._1 == name) match {
67.54 + case None => None
67.55 + case Some((_, value)) => Long.unapply(value)
67.56 + }
67.57 }
67.58
67.59
67.60 @@ -53,7 +61,7 @@
67.61 val Empty = Markup("", Nil)
67.62
67.63
67.64 - /* name */
67.65 + /* misc properties */
67.66
67.67 val NAME = "name"
67.68 val KIND = "kind"
67.69 @@ -86,9 +94,9 @@
67.70
67.71 /* pretty printing */
67.72
67.73 - val INDENT = "indent"
67.74 + val Indent = new Int_Property("indent")
67.75 val BLOCK = "block"
67.76 - val WIDTH = "width"
67.77 + val Width = new Int_Property("width")
67.78 val BREAK = "break"
67.79
67.80
67.81 @@ -188,6 +196,9 @@
67.82
67.83 /* toplevel */
67.84
67.85 + val SUBGOALS = "subgoals"
67.86 + val PROOF_STATE = "proof_state"
67.87 +
67.88 val STATE = "state"
67.89 val SUBGOAL = "subgoal"
67.90 val SENDBACK = "sendback"
68.1 --- a/src/Pure/General/position.scala Fri Aug 27 09:34:06 2010 +0200
68.2 +++ b/src/Pure/General/position.scala Fri Aug 27 09:43:52 2010 +0200
68.3 @@ -11,22 +11,21 @@
68.4 {
68.5 type T = List[(String, String)]
68.6
68.7 - def get_line(pos: T): Option[Int] = Markup.get_int(Markup.LINE, pos)
68.8 - def get_column(pos: T): Option[Int] = Markup.get_int(Markup.COLUMN, pos)
68.9 - def get_offset(pos: T): Option[Int] = Markup.get_int(Markup.OFFSET, pos)
68.10 - def get_end_line(pos: T): Option[Int] = Markup.get_int(Markup.END_LINE, pos)
68.11 - def get_end_column(pos: T): Option[Int] = Markup.get_int(Markup.END_COLUMN, pos)
68.12 - def get_end_offset(pos: T): Option[Int] = Markup.get_int(Markup.END_OFFSET, pos)
68.13 - def get_file(pos: T): Option[String] = Markup.get_string(Markup.FILE, pos)
68.14 - def get_id(pos: T): Option[Long] = Markup.get_long(Markup.ID, pos)
68.15 + val Line = new Markup.Int_Property(Markup.LINE)
68.16 + val End_Line = new Markup.Int_Property(Markup.END_LINE)
68.17 + val Offset = new Markup.Int_Property(Markup.OFFSET)
68.18 + val End_Offset = new Markup.Int_Property(Markup.END_OFFSET)
68.19 + val File = new Markup.Property(Markup.FILE)
68.20 + val Id = new Markup.Long_Property(Markup.ID)
68.21
68.22 - def get_range(pos: T): Option[Text.Range] =
68.23 - (get_offset(pos), get_end_offset(pos)) match {
68.24 - case (Some(start), Some(stop)) if start <= stop => Some(Text.Range(start, stop))
68.25 - case (Some(start), None) => Some(Text.Range(start))
68.26 - case (_, _) => None
68.27 - }
68.28 -
68.29 - object Id { def unapply(pos: T): Option[Long] = get_id(pos) }
68.30 - object Range { def unapply(pos: T): Option[Text.Range] = get_range(pos) }
68.31 + object Range
68.32 + {
68.33 + def apply(range: Text.Range): T = Offset(range.start) ++ Offset(range.stop)
68.34 + def unapply(pos: T): Option[Text.Range] =
68.35 + (Offset.unapply(pos), End_Offset.unapply(pos)) match {
68.36 + case (Some(start), Some(stop)) if start <= stop => Some(Text.Range(start, stop))
68.37 + case (Some(start), None) => Some(Text.Range(start))
68.38 + case _ => None
68.39 + }
68.40 + }
68.41 }
69.1 --- a/src/Pure/General/pretty.scala Fri Aug 27 09:34:06 2010 +0200
69.2 +++ b/src/Pure/General/pretty.scala Fri Aug 27 09:43:52 2010 +0200
69.3 @@ -19,12 +19,11 @@
69.4 object Block
69.5 {
69.6 def apply(i: Int, body: XML.Body): XML.Tree =
69.7 - XML.Elem(Markup(Markup.BLOCK, List((Markup.INDENT, Markup.Int(i)))), body)
69.8 + XML.Elem(Markup(Markup.BLOCK, Markup.Indent(i)), body)
69.9
69.10 def unapply(tree: XML.Tree): Option[(Int, XML.Body)] =
69.11 tree match {
69.12 - case XML.Elem(
69.13 - Markup(Markup.BLOCK, List((Markup.INDENT, Markup.Int(i)))), body) => Some((i, body))
69.14 + case XML.Elem(Markup(Markup.BLOCK, Markup.Indent(i)), body) => Some((i, body))
69.15 case _ => None
69.16 }
69.17 }
69.18 @@ -32,12 +31,11 @@
69.19 object Break
69.20 {
69.21 def apply(w: Int): XML.Tree =
69.22 - XML.Elem(
69.23 - Markup(Markup.BREAK, List((Markup.WIDTH, Markup.Int(w)))), List(XML.Text(Symbol.spaces(w))))
69.24 + XML.Elem(Markup(Markup.BREAK, Markup.Width(w)), List(XML.Text(Symbol.spaces(w))))
69.25
69.26 def unapply(tree: XML.Tree): Option[Int] =
69.27 tree match {
69.28 - case XML.Elem(Markup(Markup.BREAK, List((Markup.WIDTH, Markup.Int(w)))), _) => Some(w)
69.29 + case XML.Elem(Markup(Markup.BREAK, Markup.Width(w)), _) => Some(w)
69.30 case _ => None
69.31 }
69.32 }
70.1 --- a/src/Pure/Isar/locale.ML Fri Aug 27 09:34:06 2010 +0200
70.2 +++ b/src/Pure/Isar/locale.ML Fri Aug 27 09:43:52 2010 +0200
70.3 @@ -483,7 +483,7 @@
70.4 val thy' = (change_locale loc o apsnd) (cons ((name, (morph, export)), serial ())) thy;
70.5 val context' = Context.Theory thy';
70.6 val (_, regs) = fold_rev (roundup thy' cons export)
70.7 - (all_registrations context') (get_idents (context'), []);
70.8 + (registrations_of context' loc) (get_idents (context'), []);
70.9 in
70.10 thy'
70.11 |> fold_rev (fn dep => Context.theory_map (add_registration dep NONE export)) regs
71.1 --- a/src/Pure/Isar/proof.ML Fri Aug 27 09:34:06 2010 +0200
71.2 +++ b/src/Pure/Isar/proof.ML Fri Aug 27 09:43:52 2010 +0200
71.3 @@ -42,6 +42,7 @@
71.4 val raw_goal: state -> {context: context, facts: thm list, goal: thm}
71.5 val goal: state -> {context: context, facts: thm list, goal: thm}
71.6 val simple_goal: state -> {context: context, goal: thm}
71.7 + val status_markup: state -> Markup.T
71.8 val let_bind: (term list * term) list -> state -> state
71.9 val let_bind_cmd: (string list * string) list -> state -> state
71.10 val write: Syntax.mode -> (term * mixfix) list -> state -> state
71.11 @@ -520,6 +521,11 @@
71.12 val (ctxt, (_, goal)) = get_goal (refine_insert facts state);
71.13 in {context = ctxt, goal = goal} end;
71.14
71.15 +fun status_markup state =
71.16 + (case try goal state of
71.17 + SOME {goal, ...} => Markup.proof_state (Thm.nprems_of goal)
71.18 + | NONE => Markup.empty);
71.19 +
71.20
71.21
71.22 (*** structured proof commands ***)
72.1 --- a/src/Pure/Isar/toplevel.ML Fri Aug 27 09:34:06 2010 +0200
72.2 +++ b/src/Pure/Isar/toplevel.ML Fri Aug 27 09:43:52 2010 +0200
72.3 @@ -563,13 +563,6 @@
72.4 fun status tr m =
72.5 setmp_thread_position tr (fn () => Output.status (Markup.markup m "")) ();
72.6
72.7 -fun async_state (tr as Transition {print, ...}) st =
72.8 - if print then
72.9 - ignore
72.10 - (Future.fork (fn () =>
72.11 - setmp_thread_position tr (fn () => Future.status (fn () => print_state false st)) ()))
72.12 - else ();
72.13 -
72.14 fun error_msg tr exn_info =
72.15 setmp_thread_position tr (fn () =>
72.16 Output.error_msg (ML_Compiler.exn_message (EXCURSION_FAIL exn_info))) ();
72.17 @@ -628,6 +621,22 @@
72.18
72.19 (* managed execution *)
72.20
72.21 +local
72.22 +
72.23 +fun async_state (tr as Transition {print, ...}) st =
72.24 + if print then
72.25 + ignore
72.26 + (Future.fork (fn () =>
72.27 + setmp_thread_position tr (fn () => Future.status (fn () => print_state false st)) ()))
72.28 + else ();
72.29 +
72.30 +fun proof_status tr st =
72.31 + (case try proof_of st of
72.32 + SOME prf => status tr (Proof.status_markup prf)
72.33 + | NONE => ());
72.34 +
72.35 +in
72.36 +
72.37 fun run_command thy_name tr st =
72.38 (case
72.39 (case init_of tr of
72.40 @@ -637,13 +646,18 @@
72.41 let val int = is_some (init_of tr) in
72.42 (case transition int tr st of
72.43 SOME (st', NONE) =>
72.44 - (status tr Markup.finished; if int then () else async_state tr st'; SOME st')
72.45 + (status tr Markup.finished;
72.46 + proof_status tr st';
72.47 + if int then () else async_state tr st';
72.48 + SOME st')
72.49 | SOME (_, SOME (exn as Exn.Interrupt, _)) => reraise exn
72.50 | SOME (_, SOME exn_info) => (error_msg tr exn_info; status tr Markup.failed; NONE)
72.51 | NONE => (error_msg tr (TERMINATE, at_command tr); status tr Markup.failed; NONE))
72.52 end
72.53 | Exn.Exn exn => (error_msg tr (exn, at_command tr); status tr Markup.failed; NONE));
72.54
72.55 +end;
72.56 +
72.57
72.58 (* nested commands *)
72.59
73.1 --- a/src/Pure/ML/ml_compiler_polyml-5.3.ML Fri Aug 27 09:34:06 2010 +0200
73.2 +++ b/src/Pure/ML/ml_compiler_polyml-5.3.ML Fri Aug 27 09:43:52 2010 +0200
73.3 @@ -44,13 +44,18 @@
73.4
73.5 fun report_parse_tree depth space =
73.6 let
73.7 + val report_text =
73.8 + (case Context.thread_data () of
73.9 + SOME (Context.Proof ctxt) => Context_Position.report_text ctxt
73.10 + | _ => Position.report_text);
73.11 +
73.12 fun report_decl markup loc decl =
73.13 - Position.report_text Markup.ML_ref (position_of loc)
73.14 + report_text Markup.ML_ref (position_of loc)
73.15 (Markup.markup (Markup.properties (Position.properties_of (position_of decl)) markup) "");
73.16 fun report loc (PolyML.PTtype types) =
73.17 PolyML.NameSpace.displayTypeExpression (types, depth, space)
73.18 |> pretty_ml |> Pretty.from_ML |> Pretty.string_of
73.19 - |> Position.report_text Markup.ML_typing (position_of loc)
73.20 + |> report_text Markup.ML_typing (position_of loc)
73.21 | report loc (PolyML.PTdeclaredAt decl) = report_decl Markup.ML_def loc decl
73.22 | report loc (PolyML.PTopenedAt decl) = report_decl Markup.ML_open loc decl
73.23 | report loc (PolyML.PTstructureAt decl) = report_decl Markup.ML_struct loc decl
74.1 --- a/src/Pure/ML/ml_context.ML Fri Aug 27 09:34:06 2010 +0200
74.2 +++ b/src/Pure/ML/ml_context.ML Fri Aug 27 09:43:52 2010 +0200
74.3 @@ -166,7 +166,9 @@
74.4 fun eval verbose pos ants =
74.5 let
74.6 (*prepare source text*)
74.7 - val ((env, body), env_ctxt) = eval_antiquotes (ants, pos) (Context.thread_data ());
74.8 + val ((env, body), env_ctxt) =
74.9 + eval_antiquotes (ants, pos) (Context.thread_data ())
74.10 + ||> Option.map (Context.mapping I (Context_Position.set_visible false));
74.11 val _ =
74.12 if ! trace then tracing (cat_lines [ML_Lex.flatten env, ML_Lex.flatten body])
74.13 else ();
75.1 --- a/src/Pure/PIDE/command.scala Fri Aug 27 09:34:06 2010 +0200
75.2 +++ b/src/Pure/PIDE/command.scala Fri Aug 27 09:43:52 2010 +0200
75.3 @@ -46,11 +46,11 @@
75.4 case XML.Elem(Markup(Markup.REPORT, _), msgs) =>
75.5 (this /: msgs)((state, msg) =>
75.6 msg match {
75.7 - case XML.Elem(Markup(name, atts), args)
75.8 - if Position.get_id(atts) == Some(command.id) && Position.get_range(atts).isDefined =>
75.9 - val range = command.decode(Position.get_range(atts).get)
75.10 + case XML.Elem(Markup(name, atts @ Position.Range(range)), args)
75.11 + if Position.Id.unapply(atts) == Some(command.id) =>
75.12 val props = atts.filterNot(p => Markup.POSITION_PROPERTIES(p._1))
75.13 - val info = Text.Info[Any](range, XML.Elem(Markup(name, props), args))
75.14 + val info =
75.15 + Text.Info[Any](command.decode(range), XML.Elem(Markup(name, props), args))
75.16 state.add_markup(info)
75.17 case _ => System.err.println("Ignored report message: " + msg); state
75.18 })
76.1 --- a/src/Pure/PIDE/markup_tree.scala Fri Aug 27 09:34:06 2010 +0200
76.2 +++ b/src/Pure/PIDE/markup_tree.scala Fri Aug 27 09:43:52 2010 +0200
76.3 @@ -115,7 +115,10 @@
76.4 if (last < stop) parent.restrict(Text.Range(last, stop)) #:: nexts
76.5 else nexts
76.6
76.7 - case Nil => Stream(Text.Info(Text.Range(last, root_range.stop), default))
76.8 + case Nil =>
76.9 + val stop = root_range.stop
76.10 + if (last < stop) Stream(Text.Info(Text.Range(last, stop), default))
76.11 + else Stream.empty
76.12 }
76.13 }
76.14 stream(root_range.start, List((Text.Info(root_range, default), overlapping(root_range))))
77.1 --- a/src/Pure/PIDE/text.scala Fri Aug 27 09:34:06 2010 +0200
77.2 +++ b/src/Pure/PIDE/text.scala Fri Aug 27 09:43:52 2010 +0200
77.3 @@ -33,7 +33,7 @@
77.4 def +(i: Offset): Range = map(_ + i)
77.5 def -(i: Offset): Range = map(_ - i)
77.6
77.7 - def is_singleton: Boolean = start == stop
77.8 + def is_singularity: Boolean = start == stop
77.9
77.10 def contains(i: Offset): Boolean = start == i || start < i && i < stop
77.11 def contains(that: Range): Boolean = this.contains(that.start) && that.stop <= this.stop
78.1 --- a/src/Pure/System/session.scala Fri Aug 27 09:34:06 2010 +0200
78.2 +++ b/src/Pure/System/session.scala Fri Aug 27 09:43:52 2010 +0200
78.3 @@ -131,15 +131,15 @@
78.4 {
78.5 raw_protocol.event(result)
78.6
78.7 - Position.get_id(result.properties) match {
78.8 - case Some(state_id) =>
78.9 + result.properties match {
78.10 + case Position.Id(state_id) =>
78.11 try {
78.12 val (st, state) = global_state.accumulate(state_id, result.message)
78.13 global_state = state
78.14 indicate_command_change(st.command)
78.15 }
78.16 catch { case _: Document.State.Fail => bad_result(result) }
78.17 - case None =>
78.18 + case _ =>
78.19 if (result.is_status) {
78.20 result.body match {
78.21 case List(Isar_Document.Assign(id, edits)) =>
79.1 --- a/src/Tools/Code/code_haskell.ML Fri Aug 27 09:34:06 2010 +0200
79.2 +++ b/src/Tools/Code/code_haskell.ML Fri Aug 27 09:43:52 2010 +0200
79.3 @@ -261,9 +261,8 @@
79.4 end;
79.5 in print_stmt end;
79.6
79.7 -fun haskell_program_of_program labelled_name module_name module_prefix reserved raw_module_alias program =
79.8 +fun haskell_program_of_program labelled_name module_prefix reserved module_alias program =
79.9 let
79.10 - val module_alias = if is_some module_name then K module_name else raw_module_alias;
79.11 val reserved = Name.make_context reserved;
79.12 val mk_name_module = mk_name_module reserved module_prefix module_alias program;
79.13 fun add_stmt (name, (stmt, deps)) =
79.14 @@ -314,15 +313,14 @@
79.15 handle Option => error ("Unknown statement name: " ^ labelled_name name);
79.16 in (deresolver, hs_program) end;
79.17
79.18 -fun serialize_haskell module_prefix raw_module_name string_classes labelled_name
79.19 - raw_reserved includes raw_module_alias
79.20 - syntax_class syntax_tyco syntax_const (code_of_pretty, code_writeln) program stmt_names destination =
79.21 +fun serialize_haskell module_prefix module_name string_classes labelled_name
79.22 + raw_reserved includes module_alias
79.23 + syntax_class syntax_tyco syntax_const (code_of_pretty, code_writeln) program
79.24 + (stmt_names, presentation_stmt_names) destination =
79.25 let
79.26 - val presentation_stmt_names = Code_Target.stmt_names_of_destination destination;
79.27 - val module_name = if null presentation_stmt_names then raw_module_name else SOME "Code";
79.28 val reserved = fold (insert (op =) o fst) includes raw_reserved;
79.29 val (deresolver, hs_program) = haskell_program_of_program labelled_name
79.30 - module_name module_prefix reserved raw_module_alias program;
79.31 + module_prefix reserved module_alias program;
79.32 val contr_classparam_typs = Code_Thingol.contr_classparam_typs program;
79.33 fun deriving_show tyco =
79.34 let
79.35 @@ -344,11 +342,9 @@
79.36 contr_classparam_typs
79.37 (if string_classes then deriving_show else K false);
79.38 fun print_module name content =
79.39 - (name, Pretty.chunks [
79.40 + (name, Pretty.chunks2 [
79.41 str ("module " ^ name ^ " where {"),
79.42 - str "",
79.43 content,
79.44 - str "",
79.45 str "}"
79.46 ]);
79.47 fun serialize_module1 (module_name', (deps, (stmts, _))) =
80.1 --- a/src/Tools/Code/code_ml.ML Fri Aug 27 09:34:06 2010 +0200
80.2 +++ b/src/Tools/Code/code_ml.ML Fri Aug 27 09:43:52 2010 +0200
80.3 @@ -489,7 +489,7 @@
80.4 |> intro_vars ((fold o Code_Thingol.fold_varnames)
80.5 (insert (op =)) ts []);
80.6 in concat [
80.7 - (Pretty.block o Pretty.commas)
80.8 + (Pretty.block o commas)
80.9 (map (print_term is_pseudo_fun some_thm vars NOBR) ts),
80.10 str "->",
80.11 print_term is_pseudo_fun some_thm vars NOBR t
80.12 @@ -535,7 +535,7 @@
80.13 :: Pretty.brk 1
80.14 :: str "match"
80.15 :: Pretty.brk 1
80.16 - :: (Pretty.block o Pretty.commas) dummy_parms
80.17 + :: (Pretty.block o commas) dummy_parms
80.18 :: Pretty.brk 1
80.19 :: str "with"
80.20 :: Pretty.brk 1
80.21 @@ -722,9 +722,8 @@
80.22
80.23 in
80.24
80.25 -fun ml_node_of_program labelled_name module_name reserved raw_module_alias program =
80.26 +fun ml_node_of_program labelled_name module_name reserved module_alias program =
80.27 let
80.28 - val module_alias = if is_some module_name then K module_name else raw_module_alias;
80.29 val reserved = Name.make_context reserved;
80.30 val empty_module = ((reserved, reserved), Graph.empty);
80.31 fun map_node [] f = f
80.32 @@ -813,7 +812,7 @@
80.33 ) stmts
80.34 #>> (split_list #> apsnd (map_filter I
80.35 #> (fn [] => error ("Datatype block without data statement: "
80.36 - ^ (commas o map (labelled_name o fst)) stmts)
80.37 + ^ (Library.commas o map (labelled_name o fst)) stmts)
80.38 | stmts => ML_Datas stmts)));
80.39 fun add_class stmts =
80.40 fold_map
80.41 @@ -828,7 +827,7 @@
80.42 ) stmts
80.43 #>> (split_list #> apsnd (map_filter I
80.44 #> (fn [] => error ("Class block without class statement: "
80.45 - ^ (commas o map (labelled_name o fst)) stmts)
80.46 + ^ (Library.commas o map (labelled_name o fst)) stmts)
80.47 | [stmt] => ML_Class stmt)));
80.48 fun add_stmts ([stmt as (name, Code_Thingol.Fun _)]) =
80.49 add_fun stmt
80.50 @@ -849,7 +848,7 @@
80.51 | add_stmts ((stmts as (_, Code_Thingol.Classinst _)::_)) =
80.52 add_funs stmts
80.53 | add_stmts stmts = error ("Illegal mutual dependencies: " ^
80.54 - (commas o map (labelled_name o fst)) stmts);
80.55 + (Library.commas o map (labelled_name o fst)) stmts);
80.56 fun add_stmts' stmts nsp_nodes =
80.57 let
80.58 val names as (name :: names') = map fst stmts;
80.59 @@ -858,9 +857,9 @@
80.60 val module_name = (the_single o distinct (op =) o map mk_name_module) module_names
80.61 handle Empty =>
80.62 error ("Different namespace prefixes for mutual dependencies:\n"
80.63 - ^ commas (map labelled_name names)
80.64 + ^ Library.commas (map labelled_name names)
80.65 ^ "\n"
80.66 - ^ commas module_names);
80.67 + ^ Library.commas module_names);
80.68 val module_name_path = Long_Name.explode module_name;
80.69 fun add_dep name name' =
80.70 let
80.71 @@ -907,15 +906,14 @@
80.72 error ("Unknown statement name: " ^ labelled_name name);
80.73 in (deresolver, nodes) end;
80.74
80.75 -fun serialize_ml target print_module print_stmt raw_module_name with_signatures labelled_name
80.76 - reserved includes raw_module_alias _ syntax_tyco syntax_const (code_of_pretty, code_writeln) program stmt_names destination =
80.77 +fun serialize_ml target print_module print_stmt module_name with_signatures labelled_name
80.78 + reserved includes module_alias _ syntax_tyco syntax_const (code_of_pretty, code_writeln) program
80.79 + (stmt_names, presentation_stmt_names) =
80.80 let
80.81 val is_cons = Code_Thingol.is_cons program;
80.82 - val presentation_stmt_names = Code_Target.stmt_names_of_destination destination;
80.83 val is_presentation = not (null presentation_stmt_names);
80.84 - val module_name = if is_presentation then SOME "Code" else raw_module_name;
80.85 val (deresolver, nodes) = ml_node_of_program labelled_name module_name
80.86 - reserved raw_module_alias program;
80.87 + reserved module_alias program;
80.88 val reserved = make_vars reserved;
80.89 fun print_node prefix (Dummy _) =
80.90 NONE
80.91 @@ -939,7 +937,7 @@
80.92 in
80.93 Code_Target.mk_serialization target
80.94 (fn NONE => code_writeln | SOME file => File.write file o code_of_pretty)
80.95 - (rpair stmt_names' o code_of_pretty) p destination
80.96 + (rpair stmt_names' o code_of_pretty) p
80.97 end;
80.98
80.99 end; (*local*)
80.100 @@ -948,8 +946,8 @@
80.101 (** for instrumentalization **)
80.102
80.103 fun evaluation_code_of thy target struct_name =
80.104 - Code_Target.serialize_custom thy (target, fn _ => fn [] =>
80.105 - serialize_ml target print_sml_module print_sml_stmt (SOME struct_name) true);
80.106 + Code_Target.serialize_custom thy (target, fn module_name => fn [] =>
80.107 + serialize_ml target print_sml_module print_sml_stmt module_name true) (SOME struct_name);
80.108
80.109
80.110 (** Isar setup **)
81.1 --- a/src/Tools/Code/code_printer.ML Fri Aug 27 09:34:06 2010 +0200
81.2 +++ b/src/Tools/Code/code_printer.ML Fri Aug 27 09:43:52 2010 +0200
81.3 @@ -19,6 +19,7 @@
81.4 val concat: Pretty.T list -> Pretty.T
81.5 val brackets: Pretty.T list -> Pretty.T
81.6 val enclose: string -> string -> Pretty.T list -> Pretty.T
81.7 + val commas: Pretty.T list -> Pretty.T list
81.8 val enum: string -> string -> string -> Pretty.T list -> Pretty.T
81.9 val enum_default: string -> string -> string -> string -> Pretty.T list -> Pretty.T
81.10 val semicolon: Pretty.T list -> Pretty.T
81.11 @@ -112,6 +113,7 @@
81.12 fun xs @| y = xs @ [y];
81.13 val str = Print_Mode.setmp [] Pretty.str;
81.14 val concat = Pretty.block o Pretty.breaks;
81.15 +val commas = Print_Mode.setmp [] Pretty.commas;
81.16 fun enclose l r = Print_Mode.setmp [] (Pretty.enclose l r);
81.17 val brackets = enclose "(" ")" o Pretty.breaks;
81.18 fun enum sep l r = Print_Mode.setmp [] (Pretty.enum sep l r);
82.1 --- a/src/Tools/Code/code_scala.ML Fri Aug 27 09:34:06 2010 +0200
82.2 +++ b/src/Tools/Code/code_scala.ML Fri Aug 27 09:43:52 2010 +0200
82.3 @@ -25,7 +25,7 @@
82.4 (** Scala serializer **)
82.5
82.6 fun print_scala_stmt labelled_name syntax_tyco syntax_const reserved
82.7 - args_num is_singleton_constr deresolve =
82.8 + args_num is_singleton_constr (deresolve, deresolve_full) =
82.9 let
82.10 val deresolve_base = Long_Name.base_name o deresolve;
82.11 fun lookup_tyvar tyvars = lookup_var tyvars o first_upper;
82.12 @@ -135,7 +135,7 @@
82.13 fun print_context tyvars vs name = applify "[" "]"
82.14 (fn (v, sort) => (Pretty.block o map str)
82.15 (lookup_tyvar tyvars v :: maps (fn sort => [": ", deresolve sort]) sort))
82.16 - NOBR ((str o deresolve) name) vs;
82.17 + NOBR ((str o deresolve_base) name) vs;
82.18 fun print_defhead tyvars vars name vs params tys ty =
82.19 Pretty.block [str "def ", constraint (applify "(" ")" (fn (param, ty) =>
82.20 constraint ((str o lookup_var vars) param) (print_typ tyvars NOBR ty))
82.21 @@ -194,7 +194,8 @@
82.22 str "match", str "{"], str "}")
82.23 (map print_clause eqs)
82.24 end;
82.25 - val print_method = (str o Library.enclose "`" "+`" o deresolve_base);
82.26 + val print_method = str o Library.enclose "`" "`" o space_implode "+"
82.27 + o Long_Name.explode o deresolve_full;
82.28 fun print_stmt (name, Code_Thingol.Fun (_, (((vs, ty), raw_eqs), _))) =
82.29 print_def name (vs, ty) (filter (snd o snd) raw_eqs)
82.30 | print_stmt (name, Code_Thingol.Datatype (_, (vs, cos))) =
82.31 @@ -240,7 +241,7 @@
82.32 in
82.33 concat [str "def", constraint (Pretty.block [applify "(" ")"
82.34 (fn (aux, ty) => constraint ((str o lookup_var vars) aux)
82.35 - (print_typ tyvars NOBR ty)) NOBR (add_typarg (deresolve classparam))
82.36 + (print_typ tyvars NOBR ty)) NOBR (add_typarg (deresolve_base classparam))
82.37 (auxs ~~ tys), str "(implicit ", str implicit_name, str ": ",
82.38 add_typarg (deresolve name), str ")"]) (print_typ tyvars NOBR ty), str "=",
82.39 applify "(" ")" (str o lookup_var vars) NOBR
82.40 @@ -281,67 +282,137 @@
82.41 end;
82.42 in print_stmt end;
82.43
82.44 -fun scala_program_of_program labelled_name module_name reserved raw_module_alias program =
82.45 +local
82.46 +
82.47 +(* hierarchical module name space *)
82.48 +
82.49 +datatype node =
82.50 + Dummy
82.51 + | Stmt of Code_Thingol.stmt
82.52 + | Module of ((Name.context * Name.context) * Name.context) * (string list * (string * node) Graph.T);
82.53 +
82.54 +in
82.55 +
82.56 +fun scala_program_of_program labelled_name reserved module_alias program =
82.57 let
82.58 - val the_module_name = the_default "Program" module_name;
82.59 - val module_alias = K (SOME the_module_name);
82.60 - val reserved = Name.make_context reserved;
82.61 - fun prepare_stmt (name, stmt) (nsps, stmts) =
82.62 +
82.63 + (* building module name hierarchy *)
82.64 + fun alias_fragments name = case module_alias name
82.65 + of SOME name' => Long_Name.explode name'
82.66 + | NONE => map (fn name => fst (yield_singleton Name.variants name reserved))
82.67 + (Long_Name.explode name);
82.68 + val module_names = Graph.fold (insert (op =) o fst o dest_name o fst) program [];
82.69 + val fragments_tab = fold (fn name => Symtab.update
82.70 + (name, alias_fragments name)) module_names Symtab.empty;
82.71 + val dest_name = Code_Printer.dest_name #>> (the o Symtab.lookup fragments_tab);
82.72 +
82.73 + (* building empty module hierarchy *)
82.74 + val empty_module = (((reserved, reserved), reserved), ([], Graph.empty));
82.75 + fun map_module f (Module content) = Module (f content);
82.76 + fun declare_module name_fragement ((nsp_class, nsp_object), nsp_common) =
82.77 let
82.78 - val (_, base) = Code_Printer.dest_name name;
82.79 - val mk_name_stmt = yield_singleton Name.variants;
82.80 - fun add_class ((nsp_class, nsp_object), nsp_common) =
82.81 + val declare = Name.declare name_fragement;
82.82 + in ((declare nsp_class, declare nsp_object), declare nsp_common) end;
82.83 + fun ensure_module name_fragement (nsps, (implicits, nodes)) =
82.84 + if can (Graph.get_node nodes) name_fragement then (nsps, (implicits, nodes))
82.85 + else
82.86 + (nsps |> declare_module name_fragement, (implicits,
82.87 + nodes |> Graph.new_node (name_fragement, (name_fragement, Module empty_module))));
82.88 + fun allocate_module [] = I
82.89 + | allocate_module (name_fragment :: name_fragments) =
82.90 + ensure_module name_fragment
82.91 + #> (apsnd o apsnd o Graph.map_node name_fragment o apsnd o map_module o allocate_module) name_fragments;
82.92 + val empty_program = Symtab.fold (fn (_, fragments) => allocate_module fragments)
82.93 + fragments_tab empty_module;
82.94 + fun change_module [] = I
82.95 + | change_module (name_fragment :: name_fragments) =
82.96 + apsnd o apsnd o Graph.map_node name_fragment o apsnd o map_module
82.97 + o change_module name_fragments;
82.98 +
82.99 + (* statement declaration *)
82.100 + fun namify_class base ((nsp_class, nsp_object), nsp_common) =
82.101 + let
82.102 + val (base', nsp_class') = yield_singleton Name.variants base nsp_class
82.103 + in (base', ((nsp_class', nsp_object), Name.declare base' nsp_common)) end;
82.104 + fun namify_object base ((nsp_class, nsp_object), nsp_common) =
82.105 + let
82.106 + val (base', nsp_object') = yield_singleton Name.variants base nsp_object
82.107 + in (base', ((nsp_class, nsp_object'), Name.declare base' nsp_common)) end;
82.108 + fun namify_common upper base ((nsp_class, nsp_object), nsp_common) =
82.109 + let
82.110 + val (base', nsp_common') =
82.111 + yield_singleton Name.variants (if upper then first_upper base else base) nsp_common
82.112 + in
82.113 + (base',
82.114 + ((Name.declare base' nsp_class, Name.declare base' nsp_object), nsp_common'))
82.115 + end;
82.116 + fun declare_stmt name stmt =
82.117 + let
82.118 + val (name_fragments, base) = dest_name name;
82.119 + val namify = case stmt
82.120 + of Code_Thingol.Fun _ => namify_object
82.121 + | Code_Thingol.Datatype _ => namify_class
82.122 + | Code_Thingol.Datatypecons _ => namify_common true
82.123 + | Code_Thingol.Class _ => namify_class
82.124 + | Code_Thingol.Classrel _ => namify_object
82.125 + | Code_Thingol.Classparam _ => namify_object
82.126 + | Code_Thingol.Classinst _ => namify_common false;
82.127 + val stmt' = case stmt
82.128 + of Code_Thingol.Datatypecons _ => Dummy
82.129 + | Code_Thingol.Classrel _ => Dummy
82.130 + | Code_Thingol.Classparam _ => Dummy
82.131 + | _ => Stmt stmt;
82.132 + fun is_classinst stmt = case stmt
82.133 + of Code_Thingol.Classinst _ => true
82.134 + | _ => false;
82.135 + val implicit_deps = filter (is_classinst o Graph.get_node program)
82.136 + (Graph.imm_succs program name);
82.137 + fun declaration (nsps, (implicits, nodes)) =
82.138 let
82.139 - val (base', nsp_class') = mk_name_stmt base nsp_class
82.140 - in (base', ((nsp_class', nsp_object), Name.declare base' nsp_common)) end;
82.141 - fun add_object ((nsp_class, nsp_object), nsp_common) =
82.142 - let
82.143 - val (base', nsp_object') = mk_name_stmt base nsp_object
82.144 - in (base', ((nsp_class, nsp_object'), Name.declare base' nsp_common)) end;
82.145 - fun add_common upper ((nsp_class, nsp_object), nsp_common) =
82.146 - let
82.147 - val (base', nsp_common') =
82.148 - mk_name_stmt (if upper then first_upper base else base) nsp_common
82.149 - in
82.150 - (base',
82.151 - ((Name.declare base' nsp_class, Name.declare base' nsp_object), nsp_common'))
82.152 - end;
82.153 - val add_name = case stmt
82.154 - of Code_Thingol.Fun _ => add_object
82.155 - | Code_Thingol.Datatype _ => add_class
82.156 - | Code_Thingol.Datatypecons _ => add_common true
82.157 - | Code_Thingol.Class _ => add_class
82.158 - | Code_Thingol.Classrel _ => add_object
82.159 - | Code_Thingol.Classparam _ => add_object
82.160 - | Code_Thingol.Classinst _ => add_common false;
82.161 - fun add_stmt base' = case stmt
82.162 - of Code_Thingol.Datatypecons _ => cons (name, (base', NONE))
82.163 - | Code_Thingol.Classrel _ => cons (name, (base', NONE))
82.164 - | Code_Thingol.Classparam _ => cons (name, (base', NONE))
82.165 - | _ => cons (name, (base', SOME stmt));
82.166 - in
82.167 - nsps
82.168 - |> add_name
82.169 - |-> (fn base' => rpair (add_stmt base' stmts))
82.170 - end;
82.171 - val stmts = AList.make (Graph.get_node program) (Graph.strong_conn program |> flat)
82.172 - |> filter_out (Code_Thingol.is_case o snd);
82.173 - val (_, sca_program) = fold prepare_stmt stmts (((reserved, reserved), reserved), []);
82.174 - fun deresolver name = (fst o the o AList.lookup (op =) sca_program) name
82.175 - handle Option => error ("Unknown statement name: " ^ labelled_name name);
82.176 - in (deresolver, (the_module_name, sca_program)) end;
82.177 + val (base', nsps') = namify base nsps;
82.178 + val implicits' = union (op =) implicit_deps implicits;
82.179 + val nodes' = Graph.new_node (name, (base', stmt')) nodes;
82.180 + in (nsps', (implicits', nodes')) end;
82.181 + in change_module name_fragments declaration end;
82.182
82.183 -fun serialize_scala raw_module_name labelled_name
82.184 - raw_reserved includes raw_module_alias
82.185 + (* dependencies *)
82.186 + fun add_dependency name name' =
82.187 + let
82.188 + val (name_fragments, base) = dest_name name;
82.189 + val (name_fragments', base') = dest_name name';
82.190 + val (name_fragments_common, (diff, diff')) =
82.191 + chop_prefix (op =) (name_fragments, name_fragments');
82.192 + val dep = if null diff then (name, name') else (hd diff, hd diff')
82.193 + in (change_module name_fragments_common o apsnd o apsnd) (Graph.add_edge dep) end;
82.194 +
82.195 + (* producing program *)
82.196 + val (_, (_, sca_program)) = empty_program
82.197 + |> Graph.fold (fn (name, (stmt, _)) => declare_stmt name stmt) program
82.198 + |> Graph.fold (fn (name, (_, (_, names))) => fold (add_dependency name) names) program;
82.199 +
82.200 + (* deresolving *)
82.201 + fun deresolve name =
82.202 + let
82.203 + val (name_fragments, _) = dest_name name;
82.204 + val nodes = fold (fn name_fragement => fn nodes => case Graph.get_node nodes name_fragement
82.205 + of (_, Module (_, (_, nodes))) => nodes) name_fragments sca_program;
82.206 + val (base', _) = Graph.get_node nodes name;
82.207 + in Long_Name.implode (name_fragments @ [base']) end
82.208 + handle Graph.UNDEF _ => error ("Unknown statement name: " ^ labelled_name name);
82.209 +
82.210 + in (deresolve, sca_program) end;
82.211 +
82.212 +fun serialize_scala labelled_name raw_reserved includes module_alias
82.213 _ syntax_tyco syntax_const (code_of_pretty, code_writeln)
82.214 - program stmt_names destination =
82.215 + program (stmt_names, presentation_stmt_names) destination =
82.216 let
82.217 - val presentation_stmt_names = Code_Target.stmt_names_of_destination destination;
82.218 - val module_name = if null presentation_stmt_names then raw_module_name else SOME "Code";
82.219 +
82.220 + (* preprocess program *)
82.221 val reserved = fold (insert (op =) o fst) includes raw_reserved;
82.222 - val (deresolver, (the_module_name, sca_program)) = scala_program_of_program labelled_name
82.223 - module_name reserved raw_module_alias program;
82.224 - val reserved = make_vars reserved;
82.225 + val (deresolve, sca_program) = scala_program_of_program labelled_name
82.226 + (Name.make_context reserved) module_alias program;
82.227 +
82.228 + (* print statements *)
82.229 fun lookup_constr tyco constr = case Graph.get_node program tyco
82.230 of Code_Thingol.Datatype (_, (_, constrs)) =>
82.231 the (AList.lookup (op = o apsnd fst) constrs constr);
82.232 @@ -359,44 +430,49 @@
82.233 of Code_Thingol.Datatypecons (_, tyco) => null (lookup_constr tyco c)
82.234 | _ => false;
82.235 val print_stmt = print_scala_stmt labelled_name syntax_tyco syntax_const
82.236 - reserved args_num is_singleton_constr deresolver;
82.237 - fun print_module name imports content =
82.238 - (name, Pretty.chunks (
82.239 - str ("object " ^ name ^ " {")
82.240 - :: (if null imports then []
82.241 - else str "" :: map (fn name => str ("import " ^ name ^ "._")) imports)
82.242 - @ [str "",
82.243 - content,
82.244 - str "",
82.245 - str "}"]
82.246 - ));
82.247 - fun serialize_module the_module_name sca_program =
82.248 + (make_vars reserved) args_num is_singleton_constr
82.249 + (deresolve, Long_Name.implode o fst o split_last o Long_Name.explode (*FIXME full*));
82.250 +
82.251 + (* print nodes *)
82.252 + fun print_implicit implicit =
82.253 let
82.254 - val content = Pretty.chunks2 (map_filter
82.255 - (fn (name, (_, SOME stmt)) => SOME (print_stmt (name, stmt))
82.256 - | (_, (_, NONE)) => NONE) sca_program);
82.257 - in print_module the_module_name (map fst includes) content end;
82.258 - fun check_destination destination =
82.259 - (File.check destination; destination);
82.260 - fun write_module destination (modlname, content) =
82.261 - let
82.262 - val filename = case modlname
82.263 - of "" => Path.explode "Main.scala"
82.264 - | _ => (Path.ext "scala" o Path.explode o implode o separate "/"
82.265 - o Long_Name.explode) modlname;
82.266 - val pathname = Path.append destination filename;
82.267 - val _ = File.mkdir_leaf (Path.dir pathname);
82.268 - in File.write pathname (code_of_pretty content) end
82.269 + val s = deresolve implicit;
82.270 + in if length (Long_Name.explode s) = 1 then NONE else SOME (str s) end;
82.271 + fun print_implicits implicits = case map_filter print_implicit implicits
82.272 + of [] => NONE
82.273 + | ps => (SOME o Pretty.block)
82.274 + (str "import /*implicits*/" :: Pretty.brk 1 :: commas ps);
82.275 + fun print_module base implicits p = Pretty.chunks2
82.276 + ([str ("object " ^ base ^ " {")] @ the_list (print_implicits implicits)
82.277 + @ [p, str ("} /* object " ^ base ^ " */")]);
82.278 + fun print_node (_, Dummy) = NONE
82.279 + | print_node (name, Stmt stmt) = if null presentation_stmt_names
82.280 + orelse member (op =) presentation_stmt_names name
82.281 + then SOME (print_stmt (name, stmt))
82.282 + else NONE
82.283 + | print_node (name, Module (_, (implicits, nodes))) = if null presentation_stmt_names
82.284 + then case print_nodes nodes
82.285 + of NONE => NONE
82.286 + | SOME p => SOME (print_module (Long_Name.base_name name) implicits p)
82.287 + else print_nodes nodes
82.288 + and print_nodes nodes = let
82.289 + val ps = map_filter (fn name => print_node (name,
82.290 + snd (Graph.get_node nodes name)))
82.291 + ((rev o flat o Graph.strong_conn) nodes);
82.292 + in if null ps then NONE else SOME (Pretty.chunks2 ps) end;
82.293 +
82.294 + (* serialization *)
82.295 + val p_includes = if null presentation_stmt_names
82.296 + then map (fn (base, p) => print_module base [] p) includes else [];
82.297 + val p = Pretty.chunks2 (p_includes @ the_list (print_nodes sca_program));
82.298 in
82.299 Code_Target.mk_serialization target
82.300 - (fn NONE => K () o map (code_writeln o snd) | SOME file => K () o map
82.301 - (write_module (check_destination file)))
82.302 - (rpair [] o cat_lines o map (code_of_pretty o snd))
82.303 - (map (fn (name, content) => print_module name [] content) includes
82.304 - @| serialize_module the_module_name sca_program)
82.305 - destination
82.306 + (fn NONE => code_writeln | SOME file => File.write file o code_of_pretty)
82.307 + (rpair [] o code_of_pretty) p destination
82.308 end;
82.309
82.310 +end; (*local*)
82.311 +
82.312 val literals = let
82.313 fun char_scala c = if c = "'" then "\\'"
82.314 else if c = "\"" then "\\\""
82.315 @@ -412,8 +488,8 @@
82.316 literal_char = Library.enclose "'" "'" o char_scala,
82.317 literal_string = quote o translate_string char_scala,
82.318 literal_numeral = fn k => "BigInt(" ^ numeral_scala k ^ ")",
82.319 - literal_positive_numeral = fn k => "Nat(" ^ numeral_scala k ^ ")",
82.320 - literal_alternative_numeral = fn k => "Natural(" ^ numeral_scala k ^ ")",
82.321 + literal_positive_numeral = fn k => "Nat.Nat(" ^ numeral_scala k ^ ")",
82.322 + literal_alternative_numeral = fn k => "Natural.Nat(" ^ numeral_scala k ^ ")",
82.323 literal_naive_numeral = fn k => "BigInt(" ^ numeral_scala k ^ ")",
82.324 literal_list = fn [] => str "Nil" | ps => Pretty.block [str "List", enum "," "(" ")" ps],
82.325 infix_cons = (6, "::")
82.326 @@ -422,17 +498,17 @@
82.327
82.328 (** Isar setup **)
82.329
82.330 -fun isar_serializer module_name =
82.331 +fun isar_serializer _ =
82.332 Code_Target.parse_args (Scan.succeed ())
82.333 - #> (fn () => serialize_scala module_name);
82.334 + #> (fn () => serialize_scala);
82.335
82.336 val setup =
82.337 Code_Target.add_target
82.338 (target, { serializer = isar_serializer, literals = literals,
82.339 - check = { env_var = "SCALA_HOME", make_destination = I,
82.340 + check = { env_var = "SCALA_HOME", make_destination = fn p => Path.append p (Path.explode "ROOT.scala"),
82.341 make_command = fn scala_home => fn p => fn _ =>
82.342 "export JAVA_OPTS='-Xms128m -Xmx512m -Xss2m' && "
82.343 - ^ Path.implode (Path.append (Path.explode scala_home) (Path.explode "bin/scalac")) ^ " *.scala" } })
82.344 + ^ Path.implode (Path.append (Path.explode scala_home) (Path.explode "bin/scalac")) ^ " " ^ File.shell_path p } })
82.345 #> Code_Target.add_syntax_tyco target "fun"
82.346 (SOME (2, fn print_typ => fn fxy => fn [ty1, ty2] =>
82.347 brackify_infix (1, R) fxy (
83.1 --- a/src/Tools/Code/code_target.ML Fri Aug 27 09:34:06 2010 +0200
83.2 +++ b/src/Tools/Code/code_target.ML Fri Aug 27 09:43:52 2010 +0200
83.3 @@ -28,7 +28,7 @@
83.4 -> 'a -> serialization
83.5 val serialize: theory -> string -> int option -> string option -> Token.T list
83.6 -> Code_Thingol.naming -> Code_Thingol.program -> string list -> serialization
83.7 - val serialize_custom: theory -> string * serializer
83.8 + val serialize_custom: theory -> string * serializer -> string option
83.9 -> Code_Thingol.naming -> Code_Thingol.program -> string list -> string * string option list
83.10 val the_literals: theory -> string -> literals
83.11 val export: serialization -> unit
83.12 @@ -111,7 +111,7 @@
83.13 -> (string -> Code_Printer.activated_const_syntax option)
83.14 -> ((Pretty.T -> string) * (Pretty.T -> unit))
83.15 -> Code_Thingol.program
83.16 - -> string list (*selected statements*)
83.17 + -> (string list * string list) (*selected statements*)
83.18 -> serialization;
83.19
83.20 datatype description = Fundamental of { serializer: serializer, literals: Code_Printer.literals,
83.21 @@ -254,7 +254,7 @@
83.22 |>> map_filter I;
83.23
83.24 fun invoke_serializer thy abortable serializer literals reserved abs_includes
83.25 - module_alias class instance tyco const module width args naming program2 names1 =
83.26 + module_alias class instance tyco const module_name width args naming program2 (names1, presentation_names) =
83.27 let
83.28 val (names_class, class') =
83.29 activate_syntax (Code_Thingol.lookup_class naming) class;
83.30 @@ -275,14 +275,14 @@
83.31 val _ = if null empty_funs then () else error ("No code equations for "
83.32 ^ commas (map (Sign.extern_const thy) empty_funs));
83.33 in
83.34 - serializer module args (Code_Thingol.labelled_name thy program2) reserved includes
83.35 - (Symtab.lookup module_alias) (Symtab.lookup class')
83.36 - (Symtab.lookup tyco') (Symtab.lookup const')
83.37 + serializer module_name args (Code_Thingol.labelled_name thy program2) reserved includes
83.38 + (if is_some module_name then K module_name else Symtab.lookup module_alias)
83.39 + (Symtab.lookup class') (Symtab.lookup tyco') (Symtab.lookup const')
83.40 (Code_Printer.string_of_pretty width, Code_Printer.writeln_pretty width)
83.41 - program4 names1
83.42 + program4 (names1, presentation_names)
83.43 end;
83.44
83.45 -fun mount_serializer thy alt_serializer target some_width module args naming program names =
83.46 +fun mount_serializer thy alt_serializer target some_width raw_module_name args naming program names destination =
83.47 let
83.48 val ((targets, abortable), default_width) = Targets.get thy;
83.49 fun collapse_hierarchy target =
83.50 @@ -299,6 +299,9 @@
83.51 val (modify, data) = collapse_hierarchy target;
83.52 val serializer = the_default (case the_description data
83.53 of Fundamental seri => #serializer seri) alt_serializer;
83.54 + val presentation_names = stmt_names_of_destination destination;
83.55 + val module_name = if null presentation_names
83.56 + then raw_module_name else SOME "Code";
83.57 val reserved = the_reserved data;
83.58 fun select_include names_all (name, (content, cs)) =
83.59 if null cs then SOME (name, content)
83.60 @@ -308,13 +311,14 @@
83.61 then SOME (name, content) else NONE;
83.62 fun includes names_all = map_filter (select_include names_all)
83.63 ((Symtab.dest o the_includes) data);
83.64 - val module_alias = the_module_alias data;
83.65 + val module_alias = the_module_alias data
83.66 val { class, instance, tyco, const } = the_name_syntax data;
83.67 val literals = the_literals thy target;
83.68 val width = the_default default_width some_width;
83.69 in
83.70 invoke_serializer thy abortable serializer literals reserved
83.71 - includes module_alias class instance tyco const module width args naming (modify program) names
83.72 + includes module_alias class instance tyco const module_name width args
83.73 + naming (modify program) (names, presentation_names) destination
83.74 end;
83.75
83.76 in
83.77 @@ -344,8 +348,8 @@
83.78 else Cache_IO.with_tmp_dir "Code_Test" (ext_check env_param)
83.79 end;
83.80
83.81 -fun serialize_custom thy (target_name, seri) naming program names =
83.82 - mount_serializer thy (SOME seri) target_name NONE NONE [] naming program names (String [])
83.83 +fun serialize_custom thy (target_name, seri) module_name naming program names =
83.84 + mount_serializer thy (SOME seri) target_name NONE module_name [] naming program names (String [])
83.85 |> the;
83.86
83.87 end; (* local *)
84.1 --- a/src/Tools/jEdit/src/jedit/isabelle_hyperlinks.scala Fri Aug 27 09:34:06 2010 +0200
84.2 +++ b/src/Tools/jEdit/src/jedit/isabelle_hyperlinks.scala Fri Aug 27 09:43:52 2010 +0200
84.3 @@ -55,11 +55,11 @@
84.4 val Text.Range(begin, end) = snapshot.convert(info_range + command_start)
84.5 val line = buffer.getLineOfOffset(begin)
84.6
84.7 - (Position.get_file(props), Position.get_line(props)) match {
84.8 + (Position.File.unapply(props), Position.Line.unapply(props)) match {
84.9 case (Some(ref_file), Some(ref_line)) =>
84.10 new External_Hyperlink(begin, end, line, ref_file, ref_line)
84.11 case _ =>
84.12 - (Position.get_id(props), Position.get_offset(props)) match {
84.13 + (Position.Id.unapply(props), Position.Offset.unapply(props)) match {
84.14 case (Some(ref_id), Some(ref_offset)) =>
84.15 snapshot.lookup_command(ref_id) match {
84.16 case Some(ref_cmd) =>