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