--- a/src/HOL/Auth/Event.thy Thu Sep 02 00:50:51 2010 +0200
+++ b/src/HOL/Auth/Event.thy Thu Sep 02 08:29:30 2010 +0200
@@ -22,14 +22,6 @@
consts
bad :: "agent set" -- {* compromised agents *}
- knows :: "agent => event list => msg set"
-
-
-text{*The constant "spies" is retained for compatibility's sake*}
-
-abbreviation (input)
- spies :: "event list => msg set" where
- "spies == knows Spy"
text{*Spy has access to his own key for spoof messages, but Server is secure*}
specification (bad)
@@ -37,9 +29,10 @@
Server_not_bad [iff]: "Server \<notin> bad"
by (rule exI [of _ "{Spy}"], simp)
-primrec
+primrec knows :: "agent => event list => msg set"
+where
knows_Nil: "knows A [] = initState A"
- knows_Cons:
+| knows_Cons:
"knows A (ev # evs) =
(if A = Spy then
(case ev of
@@ -62,14 +55,20 @@
therefore the oops case must use Notes
*)
-consts
- (*Set of items that might be visible to somebody:
+text{*The constant "spies" is retained for compatibility's sake*}
+
+abbreviation (input)
+ spies :: "event list => msg set" where
+ "spies == knows Spy"
+
+
+(*Set of items that might be visible to somebody:
complement of the set of fresh items*)
- used :: "event list => msg set"
-primrec
+primrec used :: "event list => msg set"
+where
used_Nil: "used [] = (UN B. parts (initState B))"
- used_Cons: "used (ev # evs) =
+| used_Cons: "used (ev # evs) =
(case ev of
Says A B X => parts {X} \<union> used evs
| Gets A X => used evs
--- a/src/HOL/Auth/NS_Public_Bad.thy Thu Sep 02 00:50:51 2010 +0200
+++ b/src/HOL/Auth/NS_Public_Bad.thy Thu Sep 02 08:29:30 2010 +0200
@@ -203,7 +203,7 @@
apply clarify
apply (frule_tac A' = A in
Says_imp_knows_Spy [THEN parts.Inj, THEN unique_NB], auto)
-apply (rename_tac C B' evs3)
+apply (rename_tac evs3 B' C)
txt{*This is the attack!
@{subgoals[display,indent=0,margin=65]}
*}
--- a/src/HOL/HOL.thy Thu Sep 02 00:50:51 2010 +0200
+++ b/src/HOL/HOL.thy Thu Sep 02 08:29:30 2010 +0200
@@ -1897,9 +1897,10 @@
code_abort undefined
+
subsubsection {* Generic code generator target languages *}
-text {* type bool *}
+text {* type @{typ bool} *}
code_type bool
(SML "bool")
--- a/src/HOL/Imperative_HOL/Array.thy Thu Sep 02 00:50:51 2010 +0200
+++ b/src/HOL/Imperative_HOL/Array.thy Thu Sep 02 08:29:30 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)/ => / 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((_))")
+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((_))")
end
--- a/src/HOL/Imperative_HOL/Heap_Monad.thy Thu Sep 02 00:50:51 2010 +0200
+++ b/src/HOL/Imperative_HOL/Heap_Monad.thy Thu Sep 02 08:29:30 2010 +0200
@@ -477,9 +477,9 @@
subsubsection {* Scala *}
code_include Scala "Heap"
-{*import collection.mutable.ArraySeq
-
-def bind[A, B](f: Unit => A, g: A => Unit => B): Unit => B = (_: Unit) => g (f ()) ()
+{*object Heap {
+ def bind[A, B](f: Unit => A, g: A => Unit => B): Unit => B = (_: Unit) => g (f ()) ()
+}
class Ref[A](x: A) {
var value = x
@@ -495,21 +495,23 @@
}
object Array {
- def alloc[A](n: Natural.Nat)(x: A): ArraySeq[A] =
+ import collection.mutable.ArraySeq
+ def alloc[A](n: Natural)(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 =
+ 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.Nat, x: A): Unit =
+ 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
-}*}
+}
+*}
-code_reserved Scala bind Ref Array
+code_reserved Scala Heap Ref Array
code_type Heap (Scala "Unit/ =>/ _")
code_const bind (Scala "Heap.bind")
--- a/src/HOL/Imperative_HOL/Ref.thy Thu Sep 02 00:50:51 2010 +0200
+++ b/src/HOL/Imperative_HOL/Ref.thy Thu Sep 02 08:29:30 2010 +0200
@@ -306,10 +306,10 @@
text {* Scala *}
-code_type ref (Scala "!Heap.Ref[_]")
+code_type ref (Scala "!Ref[_]")
code_const Ref (Scala "!error(\"bare Ref\")")
-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((_), (_))")
+code_const ref' (Scala "('_: Unit)/ =>/ Ref((_))")
+code_const Ref.lookup (Scala "('_: Unit)/ =>/ Ref.lookup((_))")
+code_const Ref.update (Scala "('_: Unit)/ =>/ Ref.update((_), (_))")
end
--- a/src/HOL/IsaMakefile Thu Sep 02 00:50:51 2010 +0200
+++ b/src/HOL/IsaMakefile Thu Sep 02 08:29:30 2010 +0200
@@ -110,6 +110,7 @@
$(SRC)/Tools/Code/code_eval.ML \
$(SRC)/Tools/Code/code_haskell.ML \
$(SRC)/Tools/Code/code_ml.ML \
+ $(SRC)/Tools/Code/code_namespace.ML \
$(SRC)/Tools/Code/code_preproc.ML \
$(SRC)/Tools/Code/code_printer.ML \
$(SRC)/Tools/Code/code_scala.ML \
@@ -1323,7 +1324,8 @@
Predicate_Compile_Examples/Predicate_Compile_Examples.thy \
Predicate_Compile_Examples/Predicate_Compile_Quickcheck_Examples.thy \
Predicate_Compile_Examples/Code_Prolog_Examples.thy \
- Predicate_Compile_Examples/Hotel_Example.thy
+ Predicate_Compile_Examples/Hotel_Example.thy \
+ Predicate_Compile_Examples/Lambda_Example.thy
@$(ISABELLE_TOOL) usedir $(OUT)/HOL Predicate_Compile_Examples
--- a/src/HOL/Library/Code_Natural.thy Thu Sep 02 00:50:51 2010 +0200
+++ b/src/HOL/Library/Code_Natural.thy Thu Sep 02 08:29:30 2010 +0200
@@ -56,47 +56,45 @@
code_reserved Haskell Natural
code_include Scala "Natural"
-{*import scala.Math
-
-object Nat {
+{*object Natural {
- 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))
+ 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))
}
-class Nat private(private val value: BigInt) {
+class Natural private(private val value: BigInt) {
override def hashCode(): Int = this.value.hashCode()
override def equals(that: Any): Boolean = that match {
- case that: Nat => this equals that
+ case that: Natural => this equals that
case _ => false
}
override def toString(): String = this.value.toString
- def equals(that: Nat): Boolean = this.value == that.value
+ def equals(that: Natural): 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: 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 = 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, Nat) = if (that.value == 0) (new Nat(0), this)
+ def /%(that: Natural): (Natural, Natural) = if (that.value == 0) (new Natural(0), this)
else {
val (k, l) = this.value /% that.value
- (new Nat(k), new Nat(l))
+ (new Natural(k), new Natural(l))
}
- def <=(that: Nat): Boolean = this.value <= that.value
+ def <=(that: Natural): Boolean = this.value <= that.value
- def <(that: Nat): Boolean = this.value < that.value
+ def <(that: Natural): Boolean = this.value < that.value
}
*}
@@ -105,7 +103,7 @@
code_type code_numeral
(Haskell "Natural.Natural")
- (Scala "Natural.Nat")
+ (Scala "Natural")
setup {*
fold (Numeral.add_code @{const_name number_code_numeral_inst.number_of_code_numeral}
--- a/src/HOL/Library/Efficient_Nat.thy Thu Sep 02 00:50:51 2010 +0200
+++ b/src/HOL/Library/Efficient_Nat.thy Thu Sep 02 08:29:30 2010 +0200
@@ -281,9 +281,7 @@
code_reserved Haskell Nat
code_include Scala "Nat"
-{*import scala.Math
-
-object Nat {
+{*object Nat {
def apply(numeral: BigInt): Nat = new Nat(numeral max 0)
def apply(numeral: Int): Nat = Nat(BigInt(numeral))
@@ -330,7 +328,7 @@
code_type nat
(Haskell "Nat.Nat")
- (Scala "Nat.Nat")
+ (Scala "Nat")
code_instance nat :: equal
(Haskell -)
@@ -397,7 +395,7 @@
code_const int and nat
(Haskell "toInteger" and "fromInteger")
- (Scala "!_.as'_BigInt" and "Nat.Nat")
+ (Scala "!_.as'_BigInt" and "Nat")
text {* Conversion from and to code numerals. *}
@@ -405,14 +403,14 @@
(SML "IntInf.toInt")
(OCaml "_")
(Haskell "!(fromInteger/ ./ toInteger)")
- (Scala "!Natural.Nat(_.as'_BigInt)")
+ (Scala "!Natural(_.as'_BigInt)")
(Eval "_")
code_const Code_Numeral.nat_of
(SML "IntInf.fromInt")
(OCaml "_")
(Haskell "!(fromInteger/ ./ toInteger)")
- (Scala "!Nat.Nat(_.as'_BigInt)")
+ (Scala "!Nat(_.as'_BigInt)")
(Eval "_")
text {* Using target language arithmetic operations whenever appropriate *}
--- a/src/HOL/Predicate_Compile_Examples/Code_Prolog_Examples.thy Thu Sep 02 00:50:51 2010 +0200
+++ b/src/HOL/Predicate_Compile_Examples/Code_Prolog_Examples.thy Thu Sep 02 08:29:30 2010 +0200
@@ -10,17 +10,35 @@
"append [] ys ys"
| "append xs ys zs ==> append (x # xs) ys (x # zs)"
-ML {* Code_Prolog.options := { ensure_groundness = false, limited_types = [], prolog_system = Code_Prolog.SWI_PROLOG} *}
+setup {* Code_Prolog.map_code_options (K
+ {ensure_groundness = false,
+ limited_types = [],
+ limited_predicates = [],
+ replacing = [],
+ manual_reorder = [],
+ prolog_system = Code_Prolog.SWI_PROLOG}) *}
values "{(x, y, z). append x y z}"
values 3 "{(x, y, z). append x y z}"
-ML {* Code_Prolog.options := { ensure_groundness = false, limited_types = [], prolog_system = Code_Prolog.YAP} *}
+setup {* Code_Prolog.map_code_options (K
+ {ensure_groundness = false,
+ limited_types = [],
+ limited_predicates = [],
+ replacing = [],
+ manual_reorder = [],
+ prolog_system = Code_Prolog.YAP}) *}
values "{(x, y, z). append x y z}"
-ML {* Code_Prolog.options := { ensure_groundness = false, limited_types = [], prolog_system = Code_Prolog.SWI_PROLOG} *}
+setup {* Code_Prolog.map_code_options (K
+ {ensure_groundness = false,
+ limited_types = [],
+ limited_predicates = [],
+ replacing = [],
+ manual_reorder = [],
+ prolog_system = Code_Prolog.SWI_PROLOG}) *}
section {* Example queens *}
@@ -183,7 +201,13 @@
where
"y \<noteq> B \<Longrightarrow> notB y"
-ML {* Code_Prolog.options := {ensure_groundness = true, limited_types = [], prolog_system = Code_Prolog.SWI_PROLOG} *}
+setup {* Code_Prolog.map_code_options (K
+ {ensure_groundness = true,
+ limited_types = [],
+ limited_predicates = [],
+ replacing = [],
+ manual_reorder = [],
+ prolog_system = Code_Prolog.SWI_PROLOG}) *}
values 2 "{y. notB y}"
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Predicate_Compile_Examples/Context_Free_Grammar_Example.thy Thu Sep 02 08:29:30 2010 +0200
@@ -0,0 +1,169 @@
+theory Context_Free_Grammar_Example
+imports Code_Prolog
+begin
+
+declare mem_def[code_pred_inline]
+
+
+subsection {* Alternative rules for length *}
+
+definition size_list :: "'a list => nat"
+where "size_list = size"
+
+lemma size_list_simps:
+ "size_list [] = 0"
+ "size_list (x # xs) = Suc (size_list xs)"
+by (auto simp add: size_list_def)
+
+declare size_list_simps[code_pred_def]
+declare size_list_def[symmetric, code_pred_inline]
+
+
+setup {* Quickcheck.add_generator ("prolog", Code_Prolog.quickcheck) *}
+
+datatype alphabet = a | b
+
+inductive_set S\<^isub>1 and A\<^isub>1 and B\<^isub>1 where
+ "[] \<in> S\<^isub>1"
+| "w \<in> A\<^isub>1 \<Longrightarrow> b # w \<in> S\<^isub>1"
+| "w \<in> B\<^isub>1 \<Longrightarrow> a # w \<in> S\<^isub>1"
+| "w \<in> S\<^isub>1 \<Longrightarrow> a # w \<in> A\<^isub>1"
+| "w \<in> S\<^isub>1 \<Longrightarrow> b # w \<in> S\<^isub>1"
+| "\<lbrakk>v \<in> B\<^isub>1; v \<in> B\<^isub>1\<rbrakk> \<Longrightarrow> a # v @ w \<in> B\<^isub>1"
+
+lemma
+ "w \<in> S\<^isub>1 \<Longrightarrow> w = []"
+quickcheck[generator = prolog, iterations=1, expect = counterexample]
+oops
+
+definition "filter_a = filter (\<lambda>x. x = a)"
+
+lemma [code_pred_def]: "filter_a [] = []"
+unfolding filter_a_def by simp
+
+lemma [code_pred_def]: "filter_a (x#xs) = (if x = a then x # filter_a xs else filter_a xs)"
+unfolding filter_a_def by simp
+
+declare filter_a_def[symmetric, code_pred_inline]
+
+definition "filter_b = filter (\<lambda>x. x = b)"
+
+lemma [code_pred_def]: "filter_b [] = []"
+unfolding filter_b_def by simp
+
+lemma [code_pred_def]: "filter_b (x#xs) = (if x = b then x # filter_b xs else filter_b xs)"
+unfolding filter_b_def by simp
+
+declare filter_b_def[symmetric, code_pred_inline]
+
+setup {* Code_Prolog.map_code_options (K
+ {ensure_groundness = true,
+ limited_types = [],
+ limited_predicates = [(["s1", "a1", "b1"], 2)],
+ replacing = [(("s1", "limited_s1"), "quickcheck")],
+ manual_reorder = [(("quickcheck", 1), [0,2,1,4,3,5])],
+ prolog_system = Code_Prolog.SWI_PROLOG}) *}
+
+
+theorem S\<^isub>1_sound:
+"w \<in> S\<^isub>1 \<Longrightarrow> length [x \<leftarrow> w. x = a] = length [x \<leftarrow> w. x = b]"
+quickcheck[generator = prolog, iterations=1, expect = counterexample]
+oops
+
+
+inductive_set S\<^isub>2 and A\<^isub>2 and B\<^isub>2 where
+ "[] \<in> S\<^isub>2"
+| "w \<in> A\<^isub>2 \<Longrightarrow> b # w \<in> S\<^isub>2"
+| "w \<in> B\<^isub>2 \<Longrightarrow> a # w \<in> S\<^isub>2"
+| "w \<in> S\<^isub>2 \<Longrightarrow> a # w \<in> A\<^isub>2"
+| "w \<in> S\<^isub>2 \<Longrightarrow> b # w \<in> B\<^isub>2"
+| "\<lbrakk>v \<in> B\<^isub>2; v \<in> B\<^isub>2\<rbrakk> \<Longrightarrow> a # v @ w \<in> B\<^isub>2"
+
+
+setup {* Code_Prolog.map_code_options (K
+ {ensure_groundness = true,
+ limited_types = [],
+ limited_predicates = [(["s2", "a2", "b2"], 3)],
+ replacing = [(("s2", "limited_s2"), "quickcheck")],
+ manual_reorder = [(("quickcheck", 1), [0,2,1,4,3,5])],
+ prolog_system = Code_Prolog.SWI_PROLOG}) *}
+
+
+theorem S\<^isub>2_sound:
+"w \<in> S\<^isub>2 \<longrightarrow> length [x \<leftarrow> w. x = a] = length [x \<leftarrow> w. x = b]"
+quickcheck[generator=prolog, iterations=1, expect = counterexample]
+oops
+
+inductive_set S\<^isub>3 and A\<^isub>3 and B\<^isub>3 where
+ "[] \<in> S\<^isub>3"
+| "w \<in> A\<^isub>3 \<Longrightarrow> b # w \<in> S\<^isub>3"
+| "w \<in> B\<^isub>3 \<Longrightarrow> a # w \<in> S\<^isub>3"
+| "w \<in> S\<^isub>3 \<Longrightarrow> a # w \<in> A\<^isub>3"
+| "w \<in> S\<^isub>3 \<Longrightarrow> b # w \<in> B\<^isub>3"
+| "\<lbrakk>v \<in> B\<^isub>3; w \<in> B\<^isub>3\<rbrakk> \<Longrightarrow> a # v @ w \<in> B\<^isub>3"
+
+
+setup {* Code_Prolog.map_code_options (K
+ {ensure_groundness = true,
+ limited_types = [],
+ limited_predicates = [(["s3", "a3", "b3"], 6)],
+ replacing = [(("s3", "limited_s3"), "quickcheck")],
+ manual_reorder = [(("quickcheck", 1), [0,2,1,4,3,5])],
+ prolog_system = Code_Prolog.SWI_PROLOG}) *}
+
+lemma S\<^isub>3_sound:
+"w \<in> S\<^isub>3 \<longrightarrow> length [x \<leftarrow> w. x = a] = length [x \<leftarrow> w. x = b]"
+quickcheck[generator=prolog, iterations=1, size=1, expect = no_counterexample]
+oops
+
+
+(*
+setup {* Code_Prolog.map_code_options (K
+ {ensure_groundness = true,
+ limited_types = [],
+ limited_predicates = [],
+ replacing = [],
+ manual_reorder = [],
+ prolog_system = Code_Prolog.SWI_PROLOG}) *}
+
+
+theorem S\<^isub>3_complete:
+"length [x \<leftarrow> w. x = a] = length [x \<leftarrow> w. x = b] \<longrightarrow> w \<in> S\<^isub>3"
+quickcheck[generator = prolog, size=1, iterations=1]
+oops
+*)
+
+inductive_set S\<^isub>4 and A\<^isub>4 and B\<^isub>4 where
+ "[] \<in> S\<^isub>4"
+| "w \<in> A\<^isub>4 \<Longrightarrow> b # w \<in> S\<^isub>4"
+| "w \<in> B\<^isub>4 \<Longrightarrow> a # w \<in> S\<^isub>4"
+| "w \<in> S\<^isub>4 \<Longrightarrow> a # w \<in> A\<^isub>4"
+| "\<lbrakk>v \<in> A\<^isub>4; w \<in> A\<^isub>4\<rbrakk> \<Longrightarrow> b # v @ w \<in> A\<^isub>4"
+| "w \<in> S\<^isub>4 \<Longrightarrow> b # w \<in> B\<^isub>4"
+| "\<lbrakk>v \<in> B\<^isub>4; w \<in> B\<^isub>4\<rbrakk> \<Longrightarrow> a # v @ w \<in> B\<^isub>4"
+
+
+setup {* Code_Prolog.map_code_options (K
+ {ensure_groundness = true,
+ limited_types = [],
+ limited_predicates = [(["s4", "a4", "b4"], 6)],
+ replacing = [(("s4", "limited_s4"), "quickcheck")],
+ manual_reorder = [(("quickcheck", 1), [0,2,1,4,3,5])],
+ prolog_system = Code_Prolog.SWI_PROLOG}) *}
+
+
+theorem S\<^isub>4_sound:
+"w \<in> S\<^isub>4 \<longrightarrow> length [x \<leftarrow> w. x = a] = length [x \<leftarrow> w. x = b]"
+quickcheck[generator = prolog, size=1, iterations=1, expect = no_counterexample]
+oops
+
+(*
+theorem S\<^isub>4_complete:
+"length [x \<leftarrow> w. x = a] = length [x \<leftarrow> w. x = b] \<longrightarrow> w \<in> S\<^isub>4"
+oops
+*)
+
+hide_const a b
+
+
+end
\ No newline at end of file
--- a/src/HOL/Predicate_Compile_Examples/Hotel_Example.thy Thu Sep 02 00:50:51 2010 +0200
+++ b/src/HOL/Predicate_Compile_Examples/Hotel_Example.thy Thu Sep 02 08:29:30 2010 +0200
@@ -84,18 +84,46 @@
lemma [code_pred_inline]: "(op -) == (%A B x. A x \<and> \<not> B x)"
by (auto simp add: Diff_iff[unfolded mem_def] expand_fun_eq intro!: eq_reflection)
-ML {* Code_Prolog.options := {ensure_groundness = true} *}
+setup {* Code_Prolog.map_code_options (K
+ {ensure_groundness = true,
+ limited_types = [],
+ limited_predicates = [],
+ replacing = [],
+ manual_reorder = [],
+ prolog_system = Code_Prolog.SWI_PROLOG}) *}
values 40 "{s. hotel s}"
setup {* Quickcheck.add_generator ("prolog", Code_Prolog.quickcheck) *}
-ML {* set Code_Prolog.trace *}
lemma "\<lbrakk> hotel s; g \<in> isin s r \<rbrakk> \<Longrightarrow> owns s r = Some g"
quickcheck[generator = code, iterations = 100000, report]
-quickcheck[generator = prolog, iterations = 1]
+quickcheck[generator = prolog, iterations = 1, expect = counterexample]
oops
+definition no_Check_in :: "event list \<Rightarrow> room \<Rightarrow> bool" where(*>*)
+[code del]: "no_Check_in s r \<equiv> \<not>(\<exists>g c. Check_in g r c \<in> set s)"
+
+
+definition feels_safe :: "event list \<Rightarrow> room \<Rightarrow> bool"
+where
+ "feels_safe s r = (\<exists>s\<^isub>1 s\<^isub>2 s\<^isub>3 g c c'.
+ s = s\<^isub>3 @ [Enter g r c] @ s\<^isub>2 @ [Check_in g r c'] @ s\<^isub>1 \<and>
+ no_Check_in (s\<^isub>3 @ s\<^isub>2) r \<and> isin (s\<^isub>2 @ [Check_in g r c] @ s\<^isub>1) r = {})"
+
+setup {* Code_Prolog.map_code_options (K
+ {ensure_groundness = true,
+ limited_types = [],
+ limited_predicates = [(["hotel"], 5)],
+ replacing = [(("hotel", "limited_hotel"), "quickcheck")],
+ manual_reorder = [],
+ prolog_system = Code_Prolog.SWI_PROLOG}) *}
+
+lemma
+ "hotel s ==> feels_safe s r ==> g \<in> isin s r ==> owns s r = Some g"
+quickcheck[generator = prolog, iterations = 1, expect = counterexample]
+oops
+
end
\ No newline at end of file
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Predicate_Compile_Examples/Lambda_Example.thy Thu Sep 02 08:29:30 2010 +0200
@@ -0,0 +1,126 @@
+theory Lambda_Example
+imports Code_Prolog
+begin
+
+subsection {* Lambda *}
+
+datatype type =
+ Atom nat
+ | Fun type type (infixr "\<Rightarrow>" 200)
+
+datatype dB =
+ Var nat
+ | App dB dB (infixl "\<degree>" 200)
+ | Abs type dB
+
+primrec
+ nth_el :: "'a list \<Rightarrow> nat \<Rightarrow> 'a option" ("_\<langle>_\<rangle>" [90, 0] 91)
+where
+ "[]\<langle>i\<rangle> = None"
+| "(x # xs)\<langle>i\<rangle> = (case i of 0 \<Rightarrow> Some x | Suc j \<Rightarrow> xs \<langle>j\<rangle>)"
+
+inductive nth_el1 :: "'a list \<Rightarrow> nat \<Rightarrow> 'a \<Rightarrow> bool"
+where
+ "nth_el1 (x # xs) 0 x"
+| "nth_el1 xs i y \<Longrightarrow> nth_el1 (x # xs) (Suc i) y"
+
+inductive typing :: "type list \<Rightarrow> dB \<Rightarrow> type \<Rightarrow> bool" ("_ \<turnstile> _ : _" [50, 50, 50] 50)
+ where
+ Var [intro!]: "nth_el1 env x T \<Longrightarrow> env \<turnstile> Var x : T"
+ | Abs [intro!]: "T # env \<turnstile> t : U \<Longrightarrow> env \<turnstile> Abs T t : (T \<Rightarrow> U)"
+ | App [intro!]: "env \<turnstile> s : U \<Rightarrow> T \<Longrightarrow> env \<turnstile> t : T \<Longrightarrow> env \<turnstile> (s \<degree> t) : U"
+
+primrec
+ lift :: "[dB, nat] => dB"
+where
+ "lift (Var i) k = (if i < k then Var i else Var (i + 1))"
+ | "lift (s \<degree> t) k = lift s k \<degree> lift t k"
+ | "lift (Abs T s) k = Abs T (lift s (k + 1))"
+
+primrec pred :: "nat => nat"
+where
+ "pred (Suc i) = i"
+
+primrec
+ subst :: "[dB, dB, nat] => dB" ("_[_'/_]" [300, 0, 0] 300)
+where
+ subst_Var: "(Var i)[s/k] =
+ (if k < i then Var (pred i) else if i = k then s else Var i)"
+ | subst_App: "(t \<degree> u)[s/k] = t[s/k] \<degree> u[s/k]"
+ | subst_Abs: "(Abs T t)[s/k] = Abs T (t[lift s 0 / k+1])"
+
+inductive beta :: "[dB, dB] => bool" (infixl "\<rightarrow>\<^sub>\<beta>" 50)
+ where
+ beta [simp, intro!]: "Abs T s \<degree> t \<rightarrow>\<^sub>\<beta> s[t/0]"
+ | appL [simp, intro!]: "s \<rightarrow>\<^sub>\<beta> t ==> s \<degree> u \<rightarrow>\<^sub>\<beta> t \<degree> u"
+ | appR [simp, intro!]: "s \<rightarrow>\<^sub>\<beta> t ==> u \<degree> s \<rightarrow>\<^sub>\<beta> u \<degree> t"
+ | abs [simp, intro!]: "s \<rightarrow>\<^sub>\<beta> t ==> Abs T s \<rightarrow>\<^sub>\<beta> Abs T t"
+
+subsection {* Inductive definitions for ordering on naturals *}
+
+inductive less_nat
+where
+ "less_nat 0 (Suc y)"
+| "less_nat x y ==> less_nat (Suc x) (Suc y)"
+
+lemma less_nat[code_pred_inline]:
+ "x < y = less_nat x y"
+apply (rule iffI)
+apply (induct x arbitrary: y)
+apply (case_tac y) apply (auto intro: less_nat.intros)
+apply (case_tac y)
+apply (auto intro: less_nat.intros)
+apply (induct rule: less_nat.induct)
+apply auto
+done
+
+lemma [code_pred_inline]: "(x::nat) + 1 = Suc x"
+by simp
+
+section {* Manual setup to find counterexample *}
+
+setup {* Quickcheck.add_generator ("prolog", Code_Prolog.quickcheck) *}
+
+setup {* Code_Prolog.map_code_options (K
+ { ensure_groundness = true,
+ limited_types = [(@{typ nat}, 1), (@{typ "type"}, 1), (@{typ dB}, 1), (@{typ "type list"}, 1)],
+ limited_predicates = [(["typing"], 2), (["nthel1"], 2)],
+ replacing = [(("typing", "limited_typing"), "quickcheck"),
+ (("nthel1", "limited_nthel1"), "lim_typing")],
+ manual_reorder = [],
+ prolog_system = Code_Prolog.SWI_PROLOG}) *}
+
+lemma
+ "\<Gamma> \<turnstile> t : U \<Longrightarrow> t \<rightarrow>\<^sub>\<beta> t' \<Longrightarrow> \<Gamma> \<turnstile> t' : U"
+quickcheck[generator = prolog, iterations = 1, expect = counterexample]
+oops
+
+text {* Verifying that the found counterexample really is one by means of a proof *}
+
+lemma
+assumes
+ "t' = Var 0"
+ "U = Atom 0"
+ "\<Gamma> = [Atom 1]"
+ "t = App (Abs (Atom 0) (Var 1)) (Var 0)"
+shows
+ "\<Gamma> \<turnstile> t : U"
+ "t \<rightarrow>\<^sub>\<beta> t'"
+ "\<not> \<Gamma> \<turnstile> t' : U"
+proof -
+ from assms show "\<Gamma> \<turnstile> t : U"
+ by (auto intro!: typing.intros nth_el1.intros)
+next
+ from assms have "t \<rightarrow>\<^sub>\<beta> (Var 1)[Var 0/0]"
+ by (auto simp only: intro: beta.intros)
+ moreover
+ from assms have "(Var 1)[Var 0/0] = t'" by simp
+ ultimately show "t \<rightarrow>\<^sub>\<beta> t'" by simp
+next
+ from assms show "\<not> \<Gamma> \<turnstile> t' : U"
+ by (auto elim: typing.cases nth_el1.cases)
+qed
+
+
+end
+
--- a/src/HOL/Predicate_Compile_Examples/ROOT.ML Thu Sep 02 00:50:51 2010 +0200
+++ b/src/HOL/Predicate_Compile_Examples/ROOT.ML Thu Sep 02 08:29:30 2010 +0200
@@ -1,2 +1,2 @@
use_thys ["Predicate_Compile_Examples", "Predicate_Compile_Quickcheck_Examples", "Specialisation_Examples"];
-if getenv "PROLOG_HOME" = "" then () else use_thys ["Code_Prolog_Examples", "Hotel_Example"];
+if getenv "PROLOG_HOME" = "" then () else use_thys ["Code_Prolog_Examples", "Hotel_Example", "Lambda_Example"];
--- a/src/HOL/Tools/Datatype/datatype_realizer.ML Thu Sep 02 00:50:51 2010 +0200
+++ b/src/HOL/Tools/Datatype/datatype_realizer.ML Thu Sep 02 08:29:30 2010 +0200
@@ -56,7 +56,7 @@
val recs = filter (is_rec_type o fst o fst) (cargs ~~ tnames ~~ Ts);
val frees = tnames ~~ Ts;
- fun mk_prems vs [] =
+ fun mk_prems vs [] =
let
val rT = nth (rec_result_Ts) i;
val vs' = filter_out is_unit vs;
@@ -67,7 +67,7 @@
in (HOLogic.mk_Trueprop (make_pred i rT T (list_comb (f, vs'))
(list_comb (Const (cname, Ts ---> T), map Free frees))), f')
end
- | mk_prems vs (((dt, s), T) :: ds) =
+ | mk_prems vs (((dt, s), T) :: ds) =
let
val k = body_index dt;
val (Us, U) = strip_type T;
@@ -83,7 +83,7 @@
in (apfst (curry list_all_free frees) (mk_prems (map Free frees) recs), j + 1) end)
constrs) (descr ~~ recTs) 1)));
-
+
fun mk_proj j [] t = t
| mk_proj j (i :: is) t = if null is then t else
if (j: int) = i then HOLogic.mk_fst t
@@ -107,14 +107,16 @@
val inst = map (pairself cert) (map head_of (HOLogic.dest_conj
(HOLogic.dest_Trueprop (concl_of induct))) ~~ ps);
- val thm = OldGoals.simple_prove_goal_cterm (cert (Logic.list_implies (prems, concl)))
+ val thm = Goal.prove_internal (map cert prems) (cert concl)
(fn prems =>
- [rewrite_goals_tac (map mk_meta_eq [@{thm fst_conv}, @{thm snd_conv}]),
+ EVERY [
+ rewrite_goals_tac (map mk_meta_eq [@{thm fst_conv}, @{thm snd_conv}]),
rtac (cterm_instantiate inst induct) 1,
ALLGOALS Object_Logic.atomize_prems_tac,
rewrite_goals_tac (@{thm o_def} :: map mk_meta_eq rec_rewrites),
REPEAT ((resolve_tac prems THEN_ALL_NEW (fn i =>
- REPEAT (etac allE i) THEN atac i)) 1)]);
+ REPEAT (etac allE i) THEN atac i)) 1)])
+ |> Drule.export_without_context;
val ind_name = Thm.derivation_name induct;
val vs = map (fn i => List.nth (pnames, i)) is;
@@ -178,14 +180,15 @@
val y = Var (("y", 0), Logic.varifyT_global T);
val y' = Free ("y", T);
- val thm = OldGoals.prove_goalw_cterm [] (cert (Logic.list_implies (prems,
- HOLogic.mk_Trueprop (Free ("P", rT --> HOLogic.boolT) $
- list_comb (r, rs @ [y'])))))
+ val thm = Goal.prove_internal (map cert prems)
+ (cert (HOLogic.mk_Trueprop (Free ("P", rT --> HOLogic.boolT) $ list_comb (r, rs @ [y']))))
(fn prems =>
- [rtac (cterm_instantiate [(cert y, cert y')] exhaust) 1,
+ EVERY [
+ rtac (cterm_instantiate [(cert y, cert y')] exhaust) 1,
ALLGOALS (EVERY'
[asm_simp_tac (HOL_basic_ss addsimps case_rewrites),
- resolve_tac prems, asm_simp_tac HOL_basic_ss])]);
+ resolve_tac prems, asm_simp_tac HOL_basic_ss])])
+ |> Drule.export_without_context;
val exh_name = Thm.derivation_name exhaust;
val (thm', thy') = thy
@@ -213,15 +216,16 @@
fun add_dt_realizers config names thy =
if ! Proofterm.proofs < 2 then thy
- else let
- val _ = message config "Adding realizers for induction and case analysis ..."
- val infos = map (Datatype.the_info thy) names;
- val info :: _ = infos;
- in
- thy
- |> fold_rev (make_ind (#sorts info) info) (subsets 0 (length (#descr info) - 1))
- |> fold_rev (make_casedists (#sorts info)) infos
- end;
+ else
+ let
+ val _ = message config "Adding realizers for induction and case analysis ..."
+ val infos = map (Datatype.the_info thy) names;
+ val info :: _ = infos;
+ in
+ thy
+ |> fold_rev (make_ind (#sorts info) info) (subsets 0 (length (#descr info) - 1))
+ |> fold_rev (make_casedists (#sorts info)) infos
+ end;
val setup = Datatype.interpretation add_dt_realizers;
--- a/src/HOL/Tools/Predicate_Compile/code_prolog.ML Thu Sep 02 00:50:51 2010 +0200
+++ b/src/HOL/Tools/Predicate_Compile/code_prolog.ML Thu Sep 02 08:29:30 2010 +0200
@@ -8,8 +8,14 @@
sig
datatype prolog_system = SWI_PROLOG | YAP
type code_options =
- {ensure_groundness : bool, limited_types : (typ * int) list, prolog_system : prolog_system}
- val options : code_options ref
+ {ensure_groundness : bool,
+ limited_types : (typ * int) list,
+ limited_predicates : (string list * int) list,
+ replacing : ((string * string) * string) list,
+ manual_reorder : ((string * int) * int list) list,
+ prolog_system : prolog_system}
+ val code_options_of : theory -> code_options
+ val map_code_options : (code_options -> code_options) -> theory -> theory
datatype arith_op = Plus | Minus
datatype prol_term = Var of string | Cons of string | AppF of string * prol_term list
@@ -31,6 +37,8 @@
val quickcheck : Proof.context -> bool -> term -> int -> term list option * (bool list * bool)
val trace : bool Unsynchronized.ref
+
+ val replace : ((string * string) * string) -> logic_program -> logic_program
end;
structure Code_Prolog : CODE_PROLOG =
@@ -47,10 +55,38 @@
datatype prolog_system = SWI_PROLOG | YAP
type code_options =
- {ensure_groundness : bool, limited_types : (typ * int) list, prolog_system : prolog_system}
+ {ensure_groundness : bool,
+ limited_types : (typ * int) list,
+ limited_predicates : (string list * int) list,
+ replacing : ((string * string) * string) list,
+ manual_reorder : ((string * int) * int list) list,
+ prolog_system : prolog_system}
-val options = Unsynchronized.ref {ensure_groundness = false, limited_types = [],
- prolog_system = SWI_PROLOG};
+structure Options = Theory_Data
+(
+ type T = code_options
+ val empty = {ensure_groundness = false,
+ limited_types = [], limited_predicates = [], replacing = [], manual_reorder = [],
+ prolog_system = SWI_PROLOG}
+ val extend = I;
+ fun merge
+ ({ensure_groundness = ensure_groundness1, limited_types = limited_types1,
+ limited_predicates = limited_predicates1, replacing = replacing1,
+ manual_reorder = manual_reorder1, prolog_system = prolog_system1},
+ {ensure_groundness = ensure_groundness2, limited_types = limited_types2,
+ limited_predicates = limited_predicates2, replacing = replacing2,
+ manual_reorder = manual_reorder2, prolog_system = prolog_system2}) =
+ {ensure_groundness = ensure_groundness1 orelse ensure_groundness2,
+ limited_types = AList.merge (op =) (K true) (limited_types1, limited_types2),
+ limited_predicates = AList.merge (op =) (K true) (limited_predicates1, limited_predicates2),
+ manual_reorder = AList.merge (op =) (K true) (manual_reorder1, manual_reorder2),
+ replacing = Library.merge (op =) (replacing1, replacing2),
+ prolog_system = prolog_system1};
+);
+
+val code_options_of = Options.get
+
+val map_code_options = Options.map
(* general string functions *)
@@ -124,16 +160,32 @@
(* translation from introduction rules to internal representation *)
+fun mk_conform f empty avoid name =
+ let
+ fun dest_Char (Symbol.Char c) = c
+ val name' = space_implode "" (map (dest_Char o Symbol.decode)
+ (filter (fn s => Symbol.is_ascii_letter s orelse Symbol.is_ascii_digit s)
+ (Symbol.explode name)))
+ val name'' = f (if name' = "" then empty else name')
+ in (if member (op =) avoid name'' then Name.variant avoid name'' else name'') end
+
(** constant table **)
type constant_table = (string * string) list
(* assuming no clashing *)
-fun mk_constant_table consts =
- AList.make (first_lower o Long_Name.base_name) consts
-
fun declare_consts consts constant_table =
- fold (fn c => AList.update (op =) (c, first_lower (Long_Name.base_name c))) consts constant_table
+ let
+ fun update' c table =
+ if AList.defined (op =) table c then table else
+ let
+ val c' = mk_conform first_lower "pred" (map snd table) (Long_Name.base_name c)
+ in
+ AList.update (op =) (c, c') table
+ end
+ in
+ fold update' consts constant_table
+ end
fun translate_const constant_table c =
case AList.lookup (op =) constant_table c of
@@ -234,7 +286,8 @@
val prems' = Conj (map (translate_prem ensure_groundness ctxt' constant_table') prems)
val clause = (dest_Rel (translate_literal ctxt' constant_table' head), prems')
in clause end
- in (map translate_intro intros', constant_table') end
+ val res = (map translate_intro intros', constant_table')
+ in res end
fun depending_preds_of (key, intros) =
fold Term.add_const_names (map Thm.prop_of intros) []
@@ -263,7 +316,7 @@
val gr = Predicate_Compile_Core.intros_graph_of ctxt
val gr' = add_edges depending_preds_of const gr
val scc = strong_conn_of gr' [const]
- val constant_table = mk_constant_table (flat scc)
+ val constant_table = declare_consts (flat scc) []
in
apfst flat (fold_map (translate_intros ensure_groundness ctxt gr) (flat scc) constant_table)
end
@@ -347,28 +400,88 @@
((flat grs) @ p', constant_table')
end
+(* make depth-limited version of predicate *)
+
+fun mk_lim_rel_name rel_name = "lim_" ^ rel_name
+
+fun mk_depth_limited rel_names ((rel_name, ts), prem) =
+ let
+ fun has_positive_recursive_prems (Conj prems) = exists has_positive_recursive_prems prems
+ | has_positive_recursive_prems (Rel (rel, ts)) = member (op =) rel_names rel
+ | has_positive_recursive_prems _ = false
+ fun mk_lim_prem (Conj prems) = Conj (map mk_lim_prem prems)
+ | mk_lim_prem (p as Rel (rel, ts)) =
+ if member (op =) rel_names rel then Rel (mk_lim_rel_name rel, Var "Lim" :: ts) else p
+ | mk_lim_prem p = p
+ in
+ if has_positive_recursive_prems prem then
+ ((mk_lim_rel_name rel_name, (AppF ("suc", [Var "Lim"])) :: ts), mk_lim_prem prem)
+ else
+ ((mk_lim_rel_name rel_name, (Var "Lim") :: ts), prem)
+ end
+
+fun add_limited_predicates limited_predicates =
+ let
+ fun add (rel_names, limit) (p, constant_table) =
+ let
+ val clauses = filter (fn ((rel, _), _) => member (op =) rel_names rel) p
+ val clauses' = map (mk_depth_limited rel_names) clauses
+ fun nat_term_of n = funpow n (fn t => AppF ("suc", [t])) (Cons "zero")
+ fun mk_entry_clause rel_name =
+ let
+ val nargs = length (snd (fst
+ (the (find_first (fn ((rel, _), _) => rel = rel_name) clauses))))
+ val vars = map (fn i => Var ("x" ^ string_of_int i)) (1 upto nargs)
+ in
+ (("limited_" ^ rel_name, vars), Rel ("lim_" ^ rel_name, nat_term_of limit :: vars))
+ end
+ in (p @ (map mk_entry_clause rel_names) @ clauses', constant_table) end
+ in
+ fold add limited_predicates
+ end
+
+
+(* replace predicates in clauses *)
+
+(* replace (A, B, C) p = replace A by B in clauses of C *)
+fun replace ((from, to), location) p =
+ let
+ fun replace_prem (Conj prems) = Conj (map replace_prem prems)
+ | replace_prem (r as Rel (rel, ts)) =
+ if rel = from then Rel (to, ts) else r
+ | replace_prem r = r
+ in
+ map (fn ((rel, args), prem) => ((rel, args), (if rel = location then replace_prem else I) prem)) p
+ end
+
+(* reorder manually : reorder premises of ith clause of predicate p by a permutation perm *)
+
+fun reorder_manually reorder p =
+ let
+ fun reorder' (clause as ((rel, args), prem)) seen =
+ let
+ val seen' = AList.map_default (op =) (rel, 0) (fn x => x + 1) seen
+ val i = the (AList.lookup (op =) seen' rel)
+ val perm = AList.lookup (op =) reorder (rel, i)
+ val prem' = (case perm of
+ SOME p => (case prem of Conj prems => Conj (map (nth prems) p) | _ => prem)
+ | NONE => prem)
+ in (((rel, args), prem'), seen') end
+ in
+ fst (fold_map reorder' p [])
+ end
(* rename variables to prolog-friendly names *)
fun rename_vars_term renaming = map_vars (fn v => the (AList.lookup (op =) renaming v))
fun rename_vars_prem renaming = map_term_prem (rename_vars_term renaming)
-fun dest_Char (Symbol.Char c) = c
-
fun is_prolog_conform v =
forall (fn s => Symbol.is_ascii_letter s orelse Symbol.is_ascii_digit s) (Symbol.explode v)
-
-fun mk_conform avoid v =
- let
- val v' = space_implode "" (map (dest_Char o Symbol.decode)
- (filter (fn s => Symbol.is_ascii_letter s orelse Symbol.is_ascii_digit s)
- (Symbol.explode v)))
- val v' = if v' = "" then "var" else v'
- in Name.variant avoid (first_upper v') end
fun mk_renaming v renaming =
- (v, mk_conform (map snd renaming) v) :: renaming
+ (v, mk_conform first_upper "Var" (map snd renaming) v) :: renaming
fun rename_vars_clause ((rel, args), prem) =
let
@@ -377,7 +490,7 @@
in ((rel, map (rename_vars_term renaming) args), rename_vars_prem renaming prem) end
val rename_vars_program = map rename_vars_clause
-
+
(* code printer *)
fun write_arith_op Plus = "+"
@@ -460,7 +573,7 @@
let
val cmd =
case system of SWI_PROLOG => "/usr/local/bin/swipl -f " | YAP => "/usr/local/bin/yap -L "
- in bash_output (cmd ^ file_name) end
+ in fst (bash_output (cmd ^ file_name)) end
(* parsing prolog solution *)
@@ -508,24 +621,23 @@
(l :: r :: []) => parse_term (unprefix " " r)
| _ => raise Fail "unexpected equation in prolog output"
fun parse_solution s = map dest_eq (space_explode ";" s)
+ val sols = case space_explode "\n" sol of [] => [] | s => fst (split_last s)
in
- map parse_solution (fst (split_last (space_explode "\n" sol)))
+ map parse_solution sols
end
(* calling external interpreter and getting results *)
fun run system p query_rel vnames nsols =
let
- val cmd = Path.named_root
val p' = rename_vars_program p
val _ = tracing "Renaming variable names..."
val renaming = fold mk_renaming vnames []
val vnames' = map (fn v => the (AList.lookup (op =) renaming v)) vnames
val prog = prelude system ^ query system nsols query_rel vnames' ^ write_program p'
val _ = tracing ("Generated prolog program:\n" ^ prog)
- val prolog_file = File.tmp_path (Path.basic "prolog_file")
- val _ = File.write prolog_file prog
- val (solution, _) = invoke system (File.shell_path prolog_file)
+ val solution = Cache_IO.with_tmp_file "prolog_file" (fn prolog_file =>
+ (File.write prolog_file prog; invoke system (Path.implode prolog_file)))
val _ = tracing ("Prolog returned solution(s):\n" ^ solution)
val tss = parse_solutions solution
in
@@ -577,7 +689,7 @@
fun values ctxt soln t_compr =
let
- val options = !options
+ val options = code_options_of (ProofContext.theory_of ctxt)
val split = case t_compr of (Const (@{const_name Collect}, _) $ t) => t
| _ => error ("Not a set comprehension: " ^ Syntax.string_of_term ctxt t_compr);
val (body, Ts, fp) = HOLogic.strip_psplits split;
@@ -605,6 +717,9 @@
|> (if #ensure_groundness options then
add_ground_predicates ctxt' (#limited_types options)
else I)
+ |> add_limited_predicates (#limited_predicates options)
+ |> apfst (fold replace (#replacing options))
+ |> apfst (reorder_manually (#manual_reorder options))
val _ = tracing "Running prolog program..."
val tss = run (#prolog_system options)
p (translate_const constant_table name) (map first_upper vnames) soln
@@ -675,6 +790,7 @@
fun quickcheck ctxt report t size =
let
+ val options = code_options_of (ProofContext.theory_of ctxt)
val thy = Theory.copy (ProofContext.theory_of ctxt)
val (vs, t') = strip_abs t
val vs' = Variable.variant_frees ctxt [] vs
@@ -696,12 +812,18 @@
val ctxt' = ProofContext.init_global thy3
val _ = tracing "Generating prolog program..."
val (p, constant_table) = generate true ctxt' full_constname
- |> add_ground_predicates ctxt' (#limited_types (!options))
+ |> add_ground_predicates ctxt' (#limited_types options)
+ |> add_limited_predicates (#limited_predicates options)
+ |> apfst (fold replace (#replacing options))
+ |> apfst (reorder_manually (#manual_reorder options))
val _ = tracing "Running prolog program..."
- val [ts] = run (#prolog_system (!options))
+ val tss = run (#prolog_system options)
p (translate_const constant_table full_constname) (map fst vs') (SOME 1)
val _ = tracing "Restoring terms..."
- val res = SOME (map (restore_term ctxt' constant_table) (ts ~~ Ts))
+ val res =
+ case tss of
+ [ts] => SOME (map (restore_term ctxt' constant_table) (ts ~~ Ts))
+ | _ => NONE
val empty_report = ([], false)
in
(res, empty_report)
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML Thu Sep 02 00:50:51 2010 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML Thu Sep 02 08:29:30 2010 +0200
@@ -63,6 +63,19 @@
val add_random_dseq_equations : options -> string list -> theory -> theory
val add_new_random_dseq_equations : options -> string list -> theory -> theory
val mk_tracing : string -> term -> term
+ val prepare_intrs : options -> compilation -> theory -> string list -> thm list ->
+ ((string * typ) list * string list * string list * (string * mode list) list *
+ (string * (Term.term list * Predicate_Compile_Aux.indprem list) list) list)
+ type mode_analysis_options = {use_random : bool, reorder_premises : bool, infer_pos_and_neg_modes : bool}
+ datatype mode_derivation = Mode_App of mode_derivation * mode_derivation | Context of mode
+ | Mode_Pair of mode_derivation * mode_derivation | Term of mode
+ type moded_clause = term list * (Predicate_Compile_Aux.indprem * mode_derivation) list
+ type 'a pred_mode_table = (string * ((bool * mode) * 'a) list) list
+
+ val infer_modes :
+ mode_analysis_options -> options -> compilation -> (string * typ) list -> (string * mode list) list ->
+ string list -> (string * (Term.term list * Predicate_Compile_Aux.indprem list) list) list ->
+ theory -> ((moded_clause list pred_mode_table * string list) * theory)
end;
structure Predicate_Compile_Core : PREDICATE_COMPILE_CORE =
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_fun.ML Thu Sep 02 00:50:51 2010 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_fun.ML Thu Sep 02 08:29:30 2010 +0200
@@ -351,13 +351,17 @@
|> map (fn (resargs, (names', prems')) =>
let
val prem' = HOLogic.mk_Trueprop (mk_lit (list_comb (P, resargs)))
- in (prem'::prems', names') end)
+ in (prems' @ [prem'], names') end)
end
val intro_ts' = folds_map rewrite prems frees
|> maps (fn (prems', frees') =>
rewrite concl frees'
- |> map (fn (concl'::conclprems, _) =>
- Logic.list_implies ((flat prems') @ conclprems, concl')))
+ |> map (fn (conclprems, _) =>
+ let
+ val (conclprems', concl') = split_last conclprems
+ in
+ Logic.list_implies ((flat prems') @ conclprems', concl')
+ end))
(*val _ = tracing ("Rewritten intro to " ^
commas (map (Syntax.string_of_term_global thy) intro_ts'))*)
in
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_pred.ML Thu Sep 02 00:50:51 2010 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_pred.ML Thu Sep 02 08:29:30 2010 +0200
@@ -259,7 +259,8 @@
fun rewrite_intros thy =
Simplifier.full_simplify (HOL_basic_ss addsimps [@{thm all_not_ex}])
- #> Simplifier.full_simplify (HOL_basic_ss addsimps @{thms bool_simps} addsimps @{thms nnf_simps})
+ #> Simplifier.full_simplify
+ (HOL_basic_ss addsimps (tl @{thms bool_simps}) addsimps @{thms nnf_simps})
#> map_term thy (maps_premises (split_conjs thy))
fun print_specs options thy msg ths =
--- a/src/Pure/General/markup.ML Thu Sep 02 00:50:51 2010 +0200
+++ b/src/Pure/General/markup.ML Thu Sep 02 08:29:30 2010 +0200
@@ -14,8 +14,8 @@
val properties: Properties.T -> T -> T
val nameN: string
val name: string -> T -> T
+ val kindN: string
val bindingN: string val binding: string -> T
- val kindN: string
val entityN: string val entity: string -> T
val defN: string
val refN: string
@@ -115,8 +115,10 @@
val assignN: string val assign: int -> T
val editN: string val edit: int -> int -> T
val pidN: string
+ val serialN: string
val promptN: string val prompt: T
val readyN: string val ready: T
+ val reportN: string val report: T
val no_output: output * output
val default_output: T -> output * output
val add_mode: string -> (T -> output * output) -> unit
@@ -163,13 +165,12 @@
val nameN = "name";
fun name a = properties [(nameN, a)];
-val (bindingN, binding) = markup_string "binding" nameN;
-
val kindN = "kind";
(* formal entities *)
+val (bindingN, binding) = markup_string "binding" nameN;
val (entityN, entity) = markup_string "entity" nameN;
val defN = "def";
@@ -337,10 +338,13 @@
(* messages *)
val pidN = "pid";
+val serialN = "serial";
val (promptN, prompt) = markup_elem "prompt";
val (readyN, ready) = markup_elem "ready";
+val (reportN, report) = markup_elem "report";
+
(** print mode operations **)
--- a/src/Pure/General/markup.scala Thu Sep 02 00:50:51 2010 +0200
+++ b/src/Pure/General/markup.scala Thu Sep 02 08:29:30 2010 +0200
@@ -69,6 +69,7 @@
/* formal entities */
+ val BINDING = "binding"
val ENTITY = "entity"
val DEF = "def"
val REF = "ref"
@@ -226,6 +227,7 @@
/* messages */
val PID = "pid"
+ val Serial = new Long_Property("serial")
val MESSAGE = "message"
val CLASS = "class"
--- a/src/Pure/General/position.ML Thu Sep 02 00:50:51 2010 +0200
+++ b/src/Pure/General/position.ML Thu Sep 02 08:29:30 2010 +0200
@@ -27,6 +27,7 @@
val of_properties: Properties.T -> T
val properties_of: T -> Properties.T
val default_properties: T -> Properties.T -> Properties.T
+ val report_markup: T -> Markup.T
val report_text: Markup.T -> T -> string -> unit
val report: Markup.T -> T -> unit
val str_of: T -> string
@@ -125,6 +126,8 @@
if exists (member (op =) Markup.position_properties o #1) props then props
else properties_of default @ props;
+fun report_markup pos = Markup.properties (properties_of pos) Markup.report;
+
fun report_text markup (pos as Pos (count, _)) txt =
if invalid_count count then ()
else Output.report (Markup.markup (Markup.properties (properties_of pos) markup) txt);
--- a/src/Pure/General/position.scala Thu Sep 02 00:50:51 2010 +0200
+++ b/src/Pure/General/position.scala Thu Sep 02 08:29:30 2010 +0200
@@ -28,4 +28,15 @@
case _ => None
}
}
+
+ object Id_Range
+ {
+ def unapply(pos: T): Option[(Long, Text.Range)] =
+ (pos, pos) match {
+ case (Id(id), Range(range)) => Some((id, range))
+ case _ => None
+ }
+ }
+
+ def purge(props: T): T = props.filterNot(p => Markup.POSITION_PROPERTIES(p._1))
}
--- a/src/Pure/General/scan.ML Thu Sep 02 00:50:51 2010 +0200
+++ b/src/Pure/General/scan.ML Thu Sep 02 08:29:30 2010 +0200
@@ -105,7 +105,7 @@
fun catch scan xs = scan xs
handle ABORT msg => raise Fail msg
- | FAIL msg => raise Fail (the_default "Syntax error." msg);
+ | FAIL msg => raise Fail (the_default "Syntax error" msg);
(* scanner combinators *)
--- a/src/Pure/General/symbol.scala Thu Sep 02 00:50:51 2010 +0200
+++ b/src/Pure/General/symbol.scala Thu Sep 02 08:29:30 2010 +0200
@@ -53,6 +53,9 @@
def is_plain(c: Char): Boolean = !(c == '\r' || c == '\\' || '\ud800' <= c && c <= '\udfff')
+ def is_physical_newline(s: CharSequence): Boolean =
+ "\n".contentEquals(s) || "\r".contentEquals(s) || "\r\n".contentEquals(s)
+
def is_wellformed(s: CharSequence): Boolean =
s.length == 1 && is_plain(s.charAt(0)) || !bad_symbol.pattern.matcher(s).matches
--- a/src/Pure/General/xml.scala Thu Sep 02 00:50:51 2010 +0200
+++ b/src/Pure/General/xml.scala Thu Sep 02 08:29:30 2010 +0200
@@ -102,17 +102,19 @@
x
}
+ def trim_bytes(s: String): String = new String(s.toCharArray)
+
def cache_string(x: String): String =
lookup(x) match {
case Some(y) => y
- case None => store(new String(x.toCharArray)) // trim string value
+ case None => store(trim_bytes(x))
}
def cache_props(x: List[(String, String)]): List[(String, String)] =
if (x.isEmpty) x
else
lookup(x) match {
case Some(y) => y
- case None => store(x.map(p => (cache_string(p._1).intern, cache_string(p._2))))
+ case None => store(x.map(p => (trim_bytes(p._1).intern, cache_string(p._2))))
}
def cache_markup(x: Markup): Markup =
lookup(x) match {
--- a/src/Pure/IsaMakefile Thu Sep 02 00:50:51 2010 +0200
+++ b/src/Pure/IsaMakefile Thu Sep 02 08:29:30 2010 +0200
@@ -230,7 +230,6 @@
morphism.ML \
name.ML \
net.ML \
- old_goals.ML \
old_term.ML \
pattern.ML \
primitive_defs.ML \
--- a/src/Pure/Isar/class_declaration.ML Thu Sep 02 00:50:51 2010 +0200
+++ b/src/Pure/Isar/class_declaration.ML Thu Sep 02 08:29:30 2010 +0200
@@ -126,8 +126,8 @@
else error ("Type inference imposes additional sort constraint "
^ Syntax.string_of_sort_global thy inferred_sort
^ " of type parameter " ^ Name.aT ^ " of sort "
- ^ Syntax.string_of_sort_global thy a_sort ^ ".")
- | _ => error "Multiple type variables in class specification.";
+ ^ Syntax.string_of_sort_global thy a_sort)
+ | _ => error "Multiple type variables in class specification";
in (map o map_atyps) (K (TFree (Name.aT, fixate_sort))) Ts end;
val after_infer_fixate = (map o map_atyps)
(fn T as TFree _ => T | T as TVar (vi, sort) =>
--- a/src/Pure/Isar/isar_cmd.ML Thu Sep 02 00:50:51 2010 +0200
+++ b/src/Pure/Isar/isar_cmd.ML Thu Sep 02 08:29:30 2010 +0200
@@ -44,7 +44,6 @@
val pwd: Toplevel.transition -> Toplevel.transition
val display_drafts: Path.T list -> Toplevel.transition -> Toplevel.transition
val print_drafts: Path.T list -> Toplevel.transition -> Toplevel.transition
- val pretty_setmargin: int -> Toplevel.transition -> Toplevel.transition
val print_context: Toplevel.transition -> Toplevel.transition
val print_theory: bool -> Toplevel.transition -> Toplevel.transition
val print_syntax: Toplevel.transition -> Toplevel.transition
@@ -321,11 +320,6 @@
in File.isabelle_tool "print" ("-c " ^ outfile); () end);
-(* pretty_setmargin *)
-
-fun pretty_setmargin n = Toplevel.imperative (fn () => Pretty.margin_default := n);
-
-
(* print parts of theory and proof context *)
val print_context = Toplevel.keep Toplevel.print_state_context;
--- a/src/Pure/Isar/isar_syn.ML Thu Sep 02 00:50:51 2010 +0200
+++ b/src/Pure/Isar/isar_syn.ML Thu Sep 02 08:29:30 2010 +0200
@@ -786,7 +786,8 @@
val _ =
Outer_Syntax.improper_command "pretty_setmargin" "change default margin for pretty printing"
- Keyword.diag (Parse.nat >> (Toplevel.no_timing oo Isar_Cmd.pretty_setmargin));
+ Keyword.diag (Parse.nat >>
+ (fn n => Toplevel.no_timing o Toplevel.imperative (fn () => Pretty.margin_default := n)));
val _ =
Outer_Syntax.improper_command "help" "print outer syntax commands" Keyword.diag
@@ -991,7 +992,7 @@
(Scan.succeed
(Toplevel.no_timing o Toplevel.keep (fn state =>
(Context.set_thread_data (try Toplevel.generic_theory_of state);
- raise Toplevel.TERMINATE))));
+ raise Runtime.TERMINATE))));
end;
--- a/src/Pure/Isar/obtain.ML Thu Sep 02 00:50:51 2010 +0200
+++ b/src/Pure/Isar/obtain.ML Thu Sep 02 08:29:30 2010 +0200
@@ -181,7 +181,7 @@
if Thm.concl_of th aconv thesis andalso
Logic.strip_assums_concl prem aconv thesis then th
else error ("Guessed a different clause:\n" ^ Display.string_of_thm ctxt th)
- | [] => error "Goal solved -- nothing guessed."
+ | [] => error "Goal solved -- nothing guessed"
| _ => error ("Guess split into several cases:\n" ^ Display.string_of_thm ctxt th));
fun result tac facts ctxt =
--- a/src/Pure/Isar/runtime.ML Thu Sep 02 00:50:51 2010 +0200
+++ b/src/Pure/Isar/runtime.ML Thu Sep 02 08:29:30 2010 +0200
@@ -11,6 +11,7 @@
exception EXCURSION_FAIL of exn * string
exception TOPLEVEL_ERROR
val exn_context: Proof.context option -> exn -> exn
+ val exn_messages: (exn -> Position.T) -> exn -> string list
val exn_message: (exn -> Position.T) -> exn -> string
val debugging: ('a -> 'b) -> 'a -> 'b
val controlled_execution: ('a -> 'b) -> 'a -> 'b
@@ -41,7 +42,7 @@
fun if_context NONE _ _ = []
| if_context (SOME ctxt) f xs = map (f ctxt) xs;
-fun exn_message exn_position e =
+fun exn_messages exn_position e =
let
fun raised exn name msgs =
let val pos = Position.str_of (exn_position exn) in
@@ -53,32 +54,36 @@
val detailed = ! Output.debugging;
- fun exn_msg _ (CONTEXT (ctxt, exn)) = exn_msg (SOME ctxt) exn
- | exn_msg _ (Exn.EXCEPTIONS []) = "Exception."
- | exn_msg ctxt (Exn.EXCEPTIONS exns) = cat_lines (map (exn_msg ctxt) exns)
- | exn_msg ctxt (EXCURSION_FAIL (exn, loc)) =
- exn_msg ctxt exn ^ Markup.markup Markup.location ("\n" ^ loc)
- | exn_msg _ TERMINATE = "Exit."
- | exn_msg _ Exn.Interrupt = "Interrupt."
- | exn_msg _ TimeLimit.TimeOut = "Timeout."
- | exn_msg _ TOPLEVEL_ERROR = "Error."
- | exn_msg _ (SYS_ERROR msg) = "## SYSTEM ERROR ##\n" ^ msg
- | exn_msg _ (ERROR msg) = msg
- | exn_msg _ (exn as Fail msg) = raised exn "Fail" [msg]
- | exn_msg _ (exn as THEORY (msg, thys)) =
- raised exn "THEORY" (msg :: (if detailed then map Context.str_of_thy thys else []))
- | exn_msg _ (exn as Syntax.AST (msg, asts)) = raised exn "AST" (msg ::
- (if detailed then map (Pretty.string_of o Syntax.pretty_ast) asts else []))
- | exn_msg ctxt (exn as TYPE (msg, Ts, ts)) = raised exn "TYPE" (msg ::
+ fun exn_msgs _ (CONTEXT (ctxt, exn)) = exn_msgs (SOME ctxt) exn
+ | exn_msgs ctxt (Exn.EXCEPTIONS exns) = maps (exn_msgs ctxt) exns
+ | exn_msgs ctxt (EXCURSION_FAIL (exn, loc)) =
+ map (fn msg => msg ^ Markup.markup Markup.location ("\n" ^ loc)) (exn_msgs ctxt exn)
+ | exn_msgs _ TERMINATE = ["Exit"]
+ | exn_msgs _ Exn.Interrupt = []
+ | exn_msgs _ TimeLimit.TimeOut = ["Timeout"]
+ | exn_msgs _ TOPLEVEL_ERROR = ["Error"]
+ | exn_msgs _ (SYS_ERROR msg) = ["## SYSTEM ERROR ##\n" ^ msg]
+ | exn_msgs _ (ERROR msg) = [msg]
+ | exn_msgs _ (exn as Fail msg) = [raised exn "Fail" [msg]]
+ | exn_msgs _ (exn as THEORY (msg, thys)) =
+ [raised exn "THEORY" (msg :: (if detailed then map Context.str_of_thy thys else []))]
+ | exn_msgs _ (exn as Syntax.AST (msg, asts)) = [raised exn "AST" (msg ::
+ (if detailed then map (Pretty.string_of o Syntax.pretty_ast) asts else []))]
+ | exn_msgs ctxt (exn as TYPE (msg, Ts, ts)) = [raised exn "TYPE" (msg ::
(if detailed then
if_context ctxt Syntax.string_of_typ Ts @ if_context ctxt Syntax.string_of_term ts
- else []))
- | exn_msg ctxt (exn as TERM (msg, ts)) = raised exn "TERM" (msg ::
- (if detailed then if_context ctxt Syntax.string_of_term ts else []))
- | exn_msg ctxt (exn as THM (msg, i, thms)) = raised exn ("THM " ^ string_of_int i) (msg ::
- (if detailed then if_context ctxt Display.string_of_thm thms else []))
- | exn_msg _ exn = raised exn (General.exnMessage exn) [];
- in exn_msg NONE e end;
+ else []))]
+ | exn_msgs ctxt (exn as TERM (msg, ts)) = [raised exn "TERM" (msg ::
+ (if detailed then if_context ctxt Syntax.string_of_term ts else []))]
+ | exn_msgs ctxt (exn as THM (msg, i, thms)) = [raised exn ("THM " ^ string_of_int i) (msg ::
+ (if detailed then if_context ctxt Display.string_of_thm thms else []))]
+ | exn_msgs _ exn = [raised exn (General.exnMessage exn) []];
+ in exn_msgs NONE e end;
+
+fun exn_message exn_position exn =
+ (case exn_messages exn_position exn of
+ [] => "Interrupt"
+ | msgs => cat_lines msgs);
--- a/src/Pure/Isar/toplevel.ML Thu Sep 02 00:50:51 2010 +0200
+++ b/src/Pure/Isar/toplevel.ML Thu Sep 02 08:29:30 2010 +0200
@@ -30,19 +30,20 @@
val timing: bool Unsynchronized.ref
val profiling: int Unsynchronized.ref
val skip_proofs: bool Unsynchronized.ref
- exception TERMINATE
exception TOPLEVEL_ERROR
val program: (unit -> 'a) -> 'a
val thread: bool -> (unit -> unit) -> Thread.thread
type transition
val empty: transition
val init_of: transition -> string option
+ val print_of: transition -> bool
val name_of: transition -> string
val pos_of: transition -> Position.T
val str_of: transition -> string
val name: string -> transition -> transition
val position: Position.T -> transition -> transition
val interactive: bool -> transition -> transition
+ val set_print: bool -> transition -> transition
val print: transition -> transition
val no_timing: transition -> transition
val init_theory: string -> (unit -> theory) -> transition -> transition
@@ -84,10 +85,9 @@
val unknown_context: transition -> transition
val setmp_thread_position: transition -> ('a -> 'b) -> 'a -> 'b
val status: transition -> Markup.T -> unit
- val error_msg: transition -> exn * string -> unit
+ val error_msg: transition -> string -> unit
val add_hook: (transition -> state -> state -> unit) -> unit
val transition: bool -> transition -> state -> (state * (exn * string) option) option
- val run_command: string -> transition -> state -> state option
val command: transition -> state -> state
val excursion: (transition * transition list) list -> (transition * state) list lazy * theory
end;
@@ -222,8 +222,6 @@
val profiling = Unsynchronized.ref 0;
val skip_proofs = Unsynchronized.ref false;
-exception TERMINATE = Runtime.TERMINATE;
-exception EXCURSION_FAIL = Runtime.EXCURSION_FAIL;
exception TOPLEVEL_ERROR = Runtime.TOPLEVEL_ERROR;
fun program body =
@@ -351,12 +349,13 @@
fun init_of (Transition {trans = [Init (name, _)], ...}) = SOME name
| init_of _ = NONE;
+fun print_of (Transition {print, ...}) = print;
fun name_of (Transition {name, ...}) = name;
fun pos_of (Transition {pos, ...}) = pos;
fun str_of tr = quote (name_of tr) ^ Position.str_of (pos_of tr);
fun command_msg msg tr = msg ^ "command " ^ str_of tr;
-fun at_command tr = command_msg "At " tr ^ ".";
+fun at_command tr = command_msg "At " tr;
fun type_error tr state =
ERROR (command_msg "Illegal application of " tr ^ " " ^ str_of_state state);
@@ -563,9 +562,8 @@
fun status tr m =
setmp_thread_position tr (fn () => Output.status (Markup.markup m "")) ();
-fun error_msg tr exn_info =
- setmp_thread_position tr (fn () =>
- Output.error_msg (ML_Compiler.exn_message (EXCURSION_FAIL exn_info))) ();
+fun error_msg tr msg =
+ setmp_thread_position tr (fn () => Output.error_msg msg) ();
(* post-transition hooks *)
@@ -609,8 +607,8 @@
val ctxt = try context_of st;
val res =
(case app int tr st of
- (_, SOME TERMINATE) => NONE
- | (st', SOME (EXCURSION_FAIL exn_info)) => SOME (st', SOME exn_info)
+ (_, SOME Runtime.TERMINATE) => NONE
+ | (st', SOME (Runtime.EXCURSION_FAIL exn_info)) => SOME (st', SOME exn_info)
| (st', SOME exn) => SOME (st', SOME (Runtime.exn_context ctxt exn, at_command tr))
| (st', NONE) => SOME (st', NONE));
val _ = (case res of SOME (st', NONE) => apply_hooks st' | _ => ());
@@ -619,53 +617,13 @@
end;
-(* 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
- SOME name => Exn.capture (fn () => Thy_Header.consistent_name thy_name name) ()
- | NONE => Exn.Result ()) of
- Exn.Result () =>
- let val int = is_some (init_of tr) in
- (case transition int tr st of
- SOME (st', NONE) =>
- (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 *)
fun command tr st =
(case transition (! interact) tr st of
SOME (st', NONE) => st'
- | SOME (_, SOME exn_info) => raise EXCURSION_FAIL exn_info
- | NONE => raise EXCURSION_FAIL (TERMINATE, at_command tr));
+ | SOME (_, SOME exn_info) => raise Runtime.EXCURSION_FAIL exn_info
+ | NONE => raise Runtime.EXCURSION_FAIL (Runtime.TERMINATE, at_command tr));
fun command_result tr st =
let val st' = command tr st
--- a/src/Pure/ML/ml_compiler.ML Thu Sep 02 00:50:51 2010 +0200
+++ b/src/Pure/ML/ml_compiler.ML Thu Sep 02 08:29:30 2010 +0200
@@ -7,6 +7,7 @@
signature ML_COMPILER =
sig
val exn_position: exn -> Position.T
+ val exn_messages: exn -> string list
val exn_message: exn -> string
val eval: bool -> Position.T -> ML_Lex.token list -> unit
end
@@ -15,6 +16,7 @@
struct
fun exn_position _ = Position.none;
+val exn_messages = Runtime.exn_messages exn_position;
val exn_message = Runtime.exn_message exn_position;
fun eval verbose pos toks =
--- a/src/Pure/ML/ml_compiler_polyml-5.3.ML Thu Sep 02 00:50:51 2010 +0200
+++ b/src/Pure/ML/ml_compiler_polyml-5.3.ML Thu Sep 02 08:29:30 2010 +0200
@@ -4,13 +4,6 @@
Advanced runtime compilation for Poly/ML 5.3.0.
*)
-signature ML_COMPILER =
-sig
- val exn_position: exn -> Position.T
- val exn_message: exn -> string
- val eval: bool -> Position.T -> ML_Lex.token list -> unit
-end
-
structure ML_Compiler: ML_COMPILER =
struct
@@ -37,6 +30,7 @@
NONE => Position.none
| SOME loc => position_of loc);
+val exn_messages = Runtime.exn_messages exn_position;
val exn_message = Runtime.exn_message exn_position;
--- a/src/Pure/PIDE/command.scala Thu Sep 02 00:50:51 2010 +0200
+++ b/src/Pure/PIDE/command.scala Thu Sep 02 08:29:30 2010 +0200
@@ -8,23 +8,25 @@
package isabelle
+import scala.collection.immutable.SortedMap
+
+
object Command
{
/** accumulated results from prover **/
case class State(
val command: Command,
- val status: List[Markup],
- val reverse_results: List[XML.Tree],
- val markup: Markup_Tree)
+ val status: List[Markup] = Nil,
+ val results: SortedMap[Long, XML.Tree] = SortedMap.empty,
+ val markup: Markup_Tree = Markup_Tree.empty)
{
/* content */
- lazy val results = reverse_results.reverse
-
def add_status(st: Markup): State = copy(status = st :: status)
def add_markup(info: Text.Info[Any]): State = copy(markup = markup + info)
- def add_result(result: XML.Tree): State = copy(reverse_results = result :: reverse_results)
+ def add_result(serial: Long, result: XML.Tree): State =
+ copy(results = results + (serial -> result))
def root_info: Text.Info[Any] =
new Text.Info(command.range,
@@ -34,7 +36,7 @@
/* message dispatch */
- def accumulate(message: XML.Tree): Command.State =
+ def accumulate(message: XML.Elem): Command.State =
message match {
case XML.Elem(Markup(Markup.STATUS, _), msgs) =>
(this /: msgs)((state, msg) =>
@@ -46,15 +48,22 @@
case XML.Elem(Markup(Markup.REPORT, _), msgs) =>
(this /: msgs)((state, msg) =>
msg match {
- 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))
+ case XML.Elem(Markup(name, atts @ Position.Id_Range(id, range)), args)
+ if id == command.id =>
+ val props = Position.purge(atts)
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
})
- case _ => add_result(message)
+ case XML.Elem(Markup(name, atts), body) =>
+ atts match {
+ case Markup.Serial(i) =>
+ val result = XML.Elem(Markup(name, Position.purge(atts)), body)
+ (add_result(i, result) /: Isar_Document.reported_positions(command.id, message))(
+ (st, range) => st.add_markup(Text.Info(command.decode(range), result)))
+ case _ => System.err.println("Ignored message without serial number: " + message); this
+ }
}
}
@@ -89,6 +98,10 @@
def source(range: Text.Range): String = source.substring(range.start, range.stop)
def length: Int = source.length
+ val newlines =
+ (0 /: Symbol.iterator(source)) {
+ case (n, s) => if (Symbol.is_physical_newline(s)) n + 1 else n }
+
val range: Text.Range = Text.Range(0, length)
lazy val symbol_index = new Symbol.Index(source)
@@ -98,5 +111,5 @@
/* accumulated results */
- val empty_state: Command.State = Command.State(this, Nil, Nil, Markup_Tree.empty)
+ val empty_state: Command.State = Command.State(this)
}
--- a/src/Pure/PIDE/document.ML Thu Sep 02 00:50:51 2010 +0200
+++ b/src/Pure/PIDE/document.ML Thu Sep 02 08:29:30 2010 +0200
@@ -192,6 +192,59 @@
+(* toplevel transactions *)
+
+local
+
+fun proof_status tr st =
+ (case try Toplevel.proof_of st of
+ SOME prf => Toplevel.status tr (Proof.status_markup prf)
+ | NONE => ());
+
+fun async_state tr st =
+ if Toplevel.print_of tr then
+ ignore
+ (Future.fork
+ (fn () =>
+ Toplevel.setmp_thread_position tr
+ (fn () => Future.status (fn () => Toplevel.print_state false st)) ()))
+ else ();
+
+in
+
+fun run_command thy_name tr st =
+ (case
+ (case Toplevel.init_of tr of
+ SOME name => Exn.capture (fn () => Thy_Header.consistent_name thy_name name) ()
+ | NONE => Exn.Result ()) of
+ Exn.Result () =>
+ let
+ val int = is_some (Toplevel.init_of tr);
+ val (errs, result) =
+ (case Toplevel.transition int tr st of
+ SOME (st', NONE) => ([], SOME st')
+ | SOME (_, SOME exn_info) =>
+ (case ML_Compiler.exn_messages (Runtime.EXCURSION_FAIL exn_info) of
+ [] => raise Exn.Interrupt
+ | errs => (errs, NONE))
+ | NONE => ([ML_Compiler.exn_message Runtime.TERMINATE], NONE));
+ val _ = List.app (Toplevel.error_msg tr) errs;
+ val _ =
+ (case result of
+ NONE => Toplevel.status tr Markup.failed
+ | SOME st' =>
+ (Toplevel.status tr Markup.finished;
+ proof_status tr st';
+ if int then () else async_state tr st'));
+ in result end
+ | Exn.Exn exn =>
+ (Toplevel.error_msg tr (ML_Compiler.exn_message exn); Toplevel.status tr Markup.failed; NONE))
+
+end;
+
+
+
+
(** editing **)
(* edit *)
@@ -214,7 +267,7 @@
NONE => NONE
| SOME st =>
let val exec_tr = Toplevel.put_id (print_id exec_id') (Future.join future_tr)
- in Toplevel.run_command name exec_tr st end));
+ in run_command name exec_tr st end));
val state' = define_exec exec_id' exec' state;
in (exec_id', (id, exec_id') :: updates, state') end;
@@ -263,7 +316,8 @@
| force_exec (SOME exec_id) = ignore (Lazy.force (the_exec state exec_id));
val _ = List.app Future.cancel execution;
- fun await_cancellation () = uninterruptible (fn _ => Future.join_results) execution;
+ fun await_cancellation () =
+ uninterruptible (fn _ => fn () => Future.join_results execution) ();
val execution' = (* FIXME proper node deps *)
node_names_of version |> map (fn name =>
--- a/src/Pure/PIDE/document.scala Thu Sep 02 00:50:51 2010 +0200
+++ b/src/Pure/PIDE/document.scala Thu Sep 02 08:29:30 2010 +0200
@@ -44,7 +44,6 @@
{
val empty: Node = new Node(Linear_Set())
- // FIXME not scalable
def command_starts(commands: Iterator[Command], offset: Text.Offset = 0)
: Iterator[(Command, Text.Offset)] =
{
@@ -57,16 +56,36 @@
}
}
+ private val block_size = 1024
+
class Node(val commands: Linear_Set[Command])
{
- def command_starts: Iterator[(Command, Text.Offset)] =
- Node.command_starts(commands.iterator)
+ private lazy val full_index: (Array[(Command, Text.Offset)], Text.Range) =
+ {
+ val blocks = new mutable.ListBuffer[(Command, Text.Offset)]
+ var next_block = 0
+ var last_stop = 0
+ for ((command, start) <- Node.command_starts(commands.iterator)) {
+ last_stop = start + command.length
+ while (last_stop + 1 > next_block) {
+ blocks += (command -> start)
+ next_block += block_size
+ }
+ }
+ (blocks.toArray, Text.Range(0, last_stop))
+ }
- def command_start(cmd: Command): Option[Text.Offset] =
- command_starts.find(_._1 == cmd).map(_._2)
+ def full_range: Text.Range = full_index._2
def command_range(i: Text.Offset = 0): Iterator[(Command, Text.Offset)] =
- command_starts dropWhile { case (cmd, start) => start + cmd.length <= i }
+ {
+ if (!commands.isEmpty && full_range.contains(i)) {
+ val (cmd0, start0) = full_index._1(i / block_size)
+ Node.command_starts(commands.iterator(cmd0), start0) dropWhile {
+ case (cmd, start) => start + cmd.length <= i }
+ }
+ else Iterator.empty
+ }
def command_range(range: Text.Range): Iterator[(Command, Text.Offset)] =
command_range(range.start) takeWhile { case (_, start) => start < range.stop }
@@ -83,6 +102,12 @@
commands.reverse_iterator(command).find(cmd => !cmd.is_ignored)
case None => None
}
+
+ def command_start(cmd: Command): Option[Text.Offset] =
+ command_starts.find(_._1 == cmd).map(_._2)
+
+ def command_starts: Iterator[(Command, Text.Offset)] =
+ Node.command_starts(commands.iterator)
}
@@ -155,19 +180,17 @@
{
class Fail(state: State) extends Exception
- val init = State().define_version(Version.init, Map()).assign(Version.init.id, Nil)
+ val init = State().define_version(Version.init, Map()).assign(Version.init.id, Nil)._2
- class Assignment(former_assignment: Map[Command, Exec_ID])
+ case class Assignment(
+ val assignment: Map[Command, Exec_ID],
+ val is_finished: Boolean = false)
{
- @volatile private var tmp_assignment = former_assignment
- private val promise = Future.promise[Map[Command, Exec_ID]]
- def is_finished: Boolean = promise.is_finished
- def join: Map[Command, Exec_ID] = promise.join
- def get_finished: Map[Command, Exec_ID] = promise.get_finished
- def assign(command_execs: List[(Command, Exec_ID)])
+ def get_finished: Map[Command, Exec_ID] = { require(is_finished); assignment }
+ def assign(command_execs: List[(Command, Exec_ID)]): Assignment =
{
- promise.fulfill(tmp_assignment ++ command_execs)
- tmp_assignment = Map()
+ require(!is_finished)
+ Assignment(assignment ++ command_execs, true)
}
}
}
@@ -187,7 +210,7 @@
val id = version.id
if (versions.isDefinedAt(id) || disposed(id)) fail
copy(versions = versions + (id -> version),
- assignments = assignments + (version -> new State.Assignment(former_assignment)))
+ assignments = assignments + (version -> State.Assignment(former_assignment)))
}
def define_command(command: Command): State =
@@ -204,7 +227,7 @@
def the_exec_state(id: Exec_ID): Command.State = execs.getOrElse(id, fail)._1
def the_assignment(version: Version): State.Assignment = assignments.getOrElse(version, fail)
- def accumulate(id: ID, message: XML.Tree): (Command.State, State) =
+ def accumulate(id: ID, message: XML.Elem): (Command.State, State) =
execs.get(id) match {
case Some((st, occs)) =>
val new_st = st.accumulate(message)
@@ -218,7 +241,7 @@
}
}
- def assign(id: Version_ID, edits: List[(Command_ID, Exec_ID)]): State =
+ def assign(id: Version_ID, edits: List[(Command_ID, Exec_ID)]): (List[Command], State) =
{
val version = the_version(id)
val occs = Set(version) // FIXME unused (!?)
@@ -231,8 +254,10 @@
new_execs += (exec_id -> (st, occs))
(st.command, exec_id)
}
- the_assignment(version).assign(assigned_execs) // FIXME explicit value instead of promise (!?)
- copy(execs = new_execs)
+ val new_assignment = the_assignment(version).assign(assigned_execs)
+ val new_state =
+ copy(assignments = assignments + (version -> new_assignment), execs = new_execs)
+ (assigned_execs.map(_._1), new_state)
}
def is_assigned(version: Version): Boolean =
--- a/src/Pure/PIDE/isar_document.scala Thu Sep 02 00:50:51 2010 +0200
+++ b/src/Pure/PIDE/isar_document.scala Thu Sep 02 08:29:30 2010 +0200
@@ -54,6 +54,22 @@
else if (markup.exists(_.name == Markup.FINISHED)) Finished
else Unprocessed
}
+
+
+ /* reported positions */
+
+ def reported_positions(command_id: Document.Command_ID, message: XML.Elem): Set[Text.Range] =
+ {
+ def reported(set: Set[Text.Range], tree: XML.Tree): Set[Text.Range] =
+ tree match {
+ case XML.Elem(Markup(name, Position.Id_Range(id, range)), body)
+ if (name == Markup.BINDING || name == Markup.ENTITY || name == Markup.REPORT) &&
+ id == command_id => body.foldLeft(set + range)(reported)
+ case XML.Elem(_, body) => body.foldLeft(set)(reported)
+ case XML.Text(_) => set
+ }
+ reported(Set.empty, message) ++ Position.Range.unapply(message.markup.properties)
+ }
}
--- a/src/Pure/ROOT.ML Thu Sep 02 00:50:51 2010 +0200
+++ b/src/Pure/ROOT.ML Thu Sep 02 08:29:30 2010 +0200
@@ -179,9 +179,9 @@
use "ML/ml_syntax.ML";
use "ML/ml_env.ML";
use "Isar/runtime.ML";
+use "ML/ml_compiler.ML";
if ml_system = "polyml-5.2" orelse ml_system = "polyml-5.2.1" orelse
- String.isPrefix "smlnj" ml_system
-then use "ML/ml_compiler.ML"
+ String.isPrefix "smlnj" ml_system then ()
else use "ML/ml_compiler_polyml-5.3.ML";
use "ML/ml_context.ML";
@@ -238,7 +238,6 @@
use "Thy/term_style.ML";
use "Thy/thy_output.ML";
use "Thy/thy_syntax.ML";
-use "old_goals.ML";
use "Isar/outer_syntax.ML";
use "PIDE/document.ML";
use "Thy/thy_info.ML";
--- a/src/Pure/Syntax/parser.ML Thu Sep 02 00:50:51 2010 +0200
+++ b/src/Pure/Syntax/parser.ML Thu Sep 02 08:29:30 2010 +0200
@@ -773,7 +773,7 @@
if not (! warned) andalso
length (new_states @ States) > ! branching_level then
(Context_Position.if_visible ctxt warning
- "Currently parsed expression could be extremely ambiguous.";
+ "Currently parsed expression could be extremely ambiguous";
warned := true)
else ();
in
--- a/src/Pure/System/isabelle_process.ML Thu Sep 02 00:50:51 2010 +0200
+++ b/src/Pure/System/isabelle_process.ML Thu Sep 02 08:29:30 2010 +0200
@@ -63,7 +63,8 @@
in
fun standard_message out_stream ch body =
- message out_stream ch (Position.properties_of (Position.thread_data ())) body;
+ message out_stream ch
+ ((Markup.serialN, serial_string ()) :: Position.properties_of (Position.thread_data ())) body;
fun init_message out_stream =
message out_stream "A" [(Markup.pidN, process_id ())] (Session.welcome ());
--- a/src/Pure/System/isar.ML Thu Sep 02 00:50:51 2010 +0200
+++ b/src/Pure/System/isar.ML Thu Sep 02 08:29:30 2010 +0200
@@ -94,7 +94,10 @@
fun op >> tr =
(case Toplevel.transition true tr (state ()) of
NONE => false
- | SOME (_, SOME err) => (set_exn (SOME err); Toplevel.error_msg tr err; true)
+ | SOME (_, SOME exn_info) =>
+ (set_exn (SOME exn_info);
+ Toplevel.error_msg tr (ML_Compiler.exn_message (Runtime.EXCURSION_FAIL exn_info));
+ true)
| SOME (st', NONE) =>
let
val name = Toplevel.name_of tr;
--- a/src/Pure/System/session.scala Thu Sep 02 00:50:51 2010 +0200
+++ b/src/Pure/System/session.scala Thu Sep 02 08:29:30 2010 +0200
@@ -190,7 +190,8 @@
result.body match {
case List(Isar_Document.Assign(id, edits)) =>
try {
- global_state.change(_.assign(id, edits))
+ val cmds: List[Command] = global_state.change_yield(_.assign(id, edits))
+ for (cmd <- cmds) command_change_buffer ! cmd
assignments.event(Session.Assignment)
}
catch { case _: Document.State.Fail => bad_result(result) }
--- a/src/Pure/Thy/thy_syntax.scala Thu Sep 02 00:50:51 2010 +0200
+++ b/src/Pure/Thy/thy_syntax.scala Thu Sep 02 08:29:30 2010 +0200
@@ -77,9 +77,11 @@
commands.iterator.find(_.is_unparsed) match {
case Some(first_unparsed) =>
val first =
- commands.reverse_iterator(first_unparsed).find(_.is_command) getOrElse commands.head
+ commands.reverse_iterator(first_unparsed).
+ dropWhile(_.newlines == 0).find(_.is_command) getOrElse commands.head
val last =
- commands.iterator(first_unparsed).find(_.is_command) getOrElse commands.last
+ commands.iterator(first_unparsed).
+ dropWhile(_.newlines == 0).find(_.is_command) getOrElse commands.last
val range =
commands.iterator(first).takeWhile(_ != last).toList ::: List(last)
--- a/src/Pure/goal.ML Thu Sep 02 00:50:51 2010 +0200
+++ b/src/Pure/goal.ML Thu Sep 02 08:29:30 2010 +0200
@@ -159,7 +159,7 @@
(case SINGLE (tac (map Assumption.assume casms)) (init cprop) of
SOME th => Drule.implies_intr_list casms
(finish (Syntax.init_pretty_global (Thm.theory_of_thm th)) th)
- | NONE => error "Tactic failed.");
+ | NONE => error "Tactic failed");
(* prove_common etc. *)
@@ -191,7 +191,7 @@
fun result () =
(case SINGLE (tac {prems = prems, context = ctxt'}) (init stmt) of
- NONE => err "Tactic failed."
+ NONE => err "Tactic failed"
| SOME st =>
let val res = finish ctxt' st handle THM (msg, _, _) => err msg in
if Unify.matches_list thy [Thm.term_of stmt] [Thm.prop_of res]
--- a/src/Pure/old_goals.ML Thu Sep 02 00:50:51 2010 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,440 +0,0 @@
-(* Title: Pure/old_goals.ML
- Author: Lawrence C Paulson, Cambridge University Computer Laboratory
- Copyright 1993 University of Cambridge
-
-Old-style goal stack package. The goal stack initially holds a dummy
-proof, and can never become empty. Each goal stack consists of a list
-of levels. The undo list is a list of goal stacks. Finally, there
-may be a stack of pending proofs.
-*)
-
-signature OLD_GOALS =
-sig
- type proof
- val premises: unit -> thm list
- val reset_goals: unit -> unit
- val result_error_fn: (thm -> string -> thm) Unsynchronized.ref
- val print_sign_exn: theory -> exn -> 'a
- val prove_goalw_cterm: thm list->cterm->(thm list->tactic list)->thm
- val prove_goalw_cterm_nocheck: thm list->cterm->(thm list->tactic list)->thm
- val prove_goalw: theory -> thm list -> string -> (thm list -> tactic list) -> thm
- val prove_goal: theory -> string -> (thm list -> tactic list) -> thm
- val topthm: unit -> thm
- val result: unit -> thm
- val uresult: unit -> thm
- val getgoal: int -> term
- val print_exn: exn -> 'a
- val filter_goal: (term*term->bool) -> thm list -> int -> thm list
- val prlev: int -> unit
- val pr: unit -> unit
- val prlim: int -> unit
- val goalw_cterm: thm list -> cterm -> thm list
- val goalw: theory -> thm list -> string -> thm list
- val goal: theory -> string -> thm list
- val Goalw: thm list -> string -> thm list
- val Goal: string -> thm list
- val simple_prove_goal_cterm: cterm->(thm list->tactic list)->thm
- val by: tactic -> unit
- val byev: tactic list -> unit
- val back: unit -> unit
- val choplev: int -> unit
- val chop: unit -> unit
- val undo: unit -> unit
- val save_proof: unit -> proof
- val restore_proof: proof -> thm list
- val push_proof: unit -> unit
- val pop_proof: unit -> thm list
- val rotate_proof: unit -> thm list
- val qed: string -> unit
- val qed_goal: string -> theory -> string -> (thm list -> tactic list) -> unit
- val qed_goalw: string -> theory -> thm list -> string
- -> (thm list -> tactic list) -> unit
- val qed_spec_mp: string -> unit
- val qed_goal_spec_mp: string -> theory -> string -> (thm list -> tactic list) -> unit
- val qed_goalw_spec_mp: string -> theory -> thm list -> string
- -> (thm list -> tactic list) -> unit
-end;
-
-structure OldGoals: OLD_GOALS =
-struct
-
-
-(*** Goal package ***)
-
-(*Each level of goal stack includes a proof state and alternative states,
- the output of the tactic applied to the preceeding level. *)
-type gstack = (thm * thm Seq.seq) list;
-
-datatype proof = Proof of gstack list * thm list * (bool*thm->thm);
-
-
-(*** References ***)
-
-(*Current assumption list -- set by "goal".*)
-val curr_prems = Unsynchronized.ref([] : thm list);
-
-(*Return assumption list -- useful if you didn't save "goal"'s result. *)
-fun premises() = !curr_prems;
-
-(*Current result maker -- set by "goal", used by "result". *)
-fun init_mkresult _ = error "No goal has been supplied in subgoal module";
-val curr_mkresult = Unsynchronized.ref (init_mkresult: bool*thm->thm);
-
-(*List of previous goal stacks, for the undo operation. Set by setstate.
- A list of lists!*)
-val undo_list = Unsynchronized.ref([[(asm_rl, Seq.empty)]] : gstack list);
-
-(* Stack of proof attempts *)
-val proofstack = Unsynchronized.ref([]: proof list);
-
-(*reset all refs*)
-fun reset_goals () =
- (curr_prems := []; curr_mkresult := init_mkresult;
- undo_list := [[(asm_rl, Seq.empty)]]);
-
-
-(*** Setting up goal-directed proof ***)
-
-(*Generates the list of new theories when the proof state's theory changes*)
-fun thy_error (thy,thy') =
- let val names = subtract (op =) (Context.display_names thy) (Context.display_names thy')
- in case names of
- [name] => "\nNew theory: " ^ name
- | _ => "\nNew theories: " ^ space_implode ", " names
- end;
-
-(*Default action is to print an error message; could be suppressed for
- special applications.*)
-fun result_error_default state msg : thm =
- Pretty.str "Bad final proof state:" ::
- Goal_Display.pretty_goals_without_context (!goals_limit) state @
- [Pretty.str msg, Pretty.str "Proof failed!"] |> Pretty.chunks |> Pretty.string_of |> error;
-
-val result_error_fn = Unsynchronized.ref result_error_default;
-
-
-(*Common treatment of "goal" and "prove_goal":
- Return assumptions, initial proof state, and function to make result.
- "atomic" indicates if the goal should be wrapped up in the function
- "Goal::prop=>prop" to avoid assumptions being returned separately.
-*)
-fun prepare_proof atomic rths chorn =
- let
- val thy = Thm.theory_of_cterm chorn;
- val horn = Thm.term_of chorn;
- val _ = Term.no_dummy_patterns horn handle TERM (msg, _) => error msg;
- val (As, B) = Logic.strip_horn horn;
- val atoms = atomic andalso
- forall (fn t => not (can Logic.dest_implies t orelse Logic.is_all t)) As;
- val (As,B) = if atoms then ([],horn) else (As,B);
- val cAs = map (cterm_of thy) As;
- val prems = map (rewrite_rule rths o Thm.forall_elim_vars 0 o Thm.assume) cAs;
- val cB = cterm_of thy B;
- val st0 = let val st = Goal.init cB |> fold Thm.weaken cAs
- in rewrite_goals_rule rths st end
- (*discharges assumptions from state in the order they appear in goal;
- checks (if requested) that resulting theorem is equivalent to goal. *)
- fun mkresult (check,state) =
- let val state = Seq.hd (Thm.flexflex_rule state)
- handle THM _ => state (*smash flexflex pairs*)
- val ngoals = nprems_of state
- val ath = implies_intr_list cAs state
- val th = Goal.conclude ath
- val thy' = Thm.theory_of_thm th
- val {hyps, prop, ...} = Thm.rep_thm th
- val final_th = Drule.export_without_context th
- in if not check then final_th
- else if not (Theory.eq_thy(thy,thy')) then !result_error_fn state
- ("Theory of proof state has changed!" ^
- thy_error (thy,thy'))
- else if ngoals>0 then !result_error_fn state
- (string_of_int ngoals ^ " unsolved goals!")
- else if not (null hyps) then !result_error_fn state
- ("Additional hypotheses:\n" ^
- cat_lines (map (Syntax.string_of_term_global thy) hyps))
- else if Pattern.matches thy
- (Envir.beta_norm (term_of chorn), Envir.beta_norm prop)
- then final_th
- else !result_error_fn state "proved a different theorem"
- end
- in
- if Theory.eq_thy(thy, Thm.theory_of_thm st0)
- then (prems, st0, mkresult)
- else error ("Definitions would change the proof state's theory" ^
- thy_error (thy, Thm.theory_of_thm st0))
- end
- handle THM(s,_,_) => error("prepare_proof: exception THM was raised!\n" ^ s);
-
-(*Prints exceptions readably to users*)
-fun print_sign_exn_unit thy e =
- case e of
- THM (msg,i,thms) =>
- (writeln ("Exception THM " ^ string_of_int i ^ " raised:\n" ^ msg);
- List.app (writeln o Display.string_of_thm_global thy) thms)
- | THEORY (msg,thys) =>
- (writeln ("Exception THEORY raised:\n" ^ msg);
- List.app (writeln o Context.str_of_thy) thys)
- | TERM (msg,ts) =>
- (writeln ("Exception TERM raised:\n" ^ msg);
- List.app (writeln o Syntax.string_of_term_global thy) ts)
- | TYPE (msg,Ts,ts) =>
- (writeln ("Exception TYPE raised:\n" ^ msg);
- List.app (writeln o Syntax.string_of_typ_global thy) Ts;
- List.app (writeln o Syntax.string_of_term_global thy) ts)
- | e => raise e;
-
-(*Prints an exception, then fails*)
-fun print_sign_exn thy e = (print_sign_exn_unit thy e; raise ERROR "");
-
-(** the prove_goal.... commands
- Prove theorem using the listed tactics; check it has the specified form.
- Augment theory with all type assignments of goal.
- Syntax is similar to "goal" command for easy keyboard use. **)
-
-(*Version taking the goal as a cterm*)
-fun prove_goalw_cterm_general check rths chorn tacsf =
- let val (prems, st0, mkresult) = prepare_proof false rths chorn
- val tac = EVERY (tacsf prems)
- fun statef() =
- (case Seq.pull (tac st0) of
- SOME(st,_) => st
- | _ => error ("prove_goal: tactic failed"))
- in mkresult (check, cond_timeit (!Output.timing) "" statef) end;
-
-(*Two variants: one checking the result, one not.
- Neither prints runtime messages: they are for internal packages.*)
-fun prove_goalw_cterm rths chorn =
- setmp_CRITICAL Output.timing false (prove_goalw_cterm_general true rths chorn)
-and prove_goalw_cterm_nocheck rths chorn =
- setmp_CRITICAL Output.timing false (prove_goalw_cterm_general false rths chorn);
-
-
-(*Version taking the goal as a string*)
-fun prove_goalw thy rths agoal tacsf =
- let val chorn = cterm_of thy (Syntax.read_prop_global thy agoal)
- in prove_goalw_cterm_general true rths chorn tacsf end
- handle ERROR msg => cat_error msg (*from read_prop?*)
- ("The error(s) above occurred for " ^ quote agoal);
-
-(*String version with no meta-rewrite-rules*)
-fun prove_goal thy = prove_goalw thy [];
-
-
-
-(*** Commands etc ***)
-
-(*Return the current goal stack, if any, from undo_list*)
-fun getstate() : gstack = case !undo_list of
- [] => error"No current state in subgoal module"
- | x::_ => x;
-
-(*Pops the given goal stack*)
-fun pop [] = error"Cannot go back past the beginning of the proof!"
- | pop (pair::pairs) = (pair,pairs);
-
-
-(* Print a level of the goal stack *)
-
-fun print_top ((th, _), pairs) =
- let
- val n = length pairs;
- val m = (! goals_limit);
- val ngoals = nprems_of th;
- in
- [Pretty.str ("Level " ^ string_of_int n ^
- (if ngoals > 0 then " (" ^ string_of_int ngoals ^ " subgoal" ^
- (if ngoals <> 1 then "s" else "") ^ ")"
- else ""))] @
- Goal_Display.pretty_goals_without_context m th
- end |> Pretty.chunks |> Pretty.writeln;
-
-(*Printing can raise exceptions, so the assignment occurs last.
- Can do setstate[(st,Seq.empty)] to set st as the state. *)
-fun setstate newgoals =
- (print_top (pop newgoals); undo_list := newgoals :: !undo_list);
-
-(*Given a proof state transformation, return a command that updates
- the goal stack*)
-fun make_command com = setstate (com (pop (getstate())));
-
-(*Apply a function on proof states to the current goal stack*)
-fun apply_fun f = f (pop(getstate()));
-
-(*Return the top theorem, representing the proof state*)
-fun topthm () = apply_fun (fn ((th,_), _) => th);
-
-(*Return the final result. *)
-fun result () = !curr_mkresult (true, topthm());
-
-(*Return the result UNCHECKED that it equals the goal -- for synthesis,
- answer extraction, or other instantiation of Vars *)
-fun uresult () = !curr_mkresult (false, topthm());
-
-(*Get subgoal i from goal stack*)
-fun getgoal i = Logic.get_goal (prop_of (topthm())) i;
-
-(*Prints exceptions nicely at top level;
- raises the exception in order to have a polymorphic type!*)
-fun print_exn e = (print_sign_exn_unit (Thm.theory_of_thm (topthm())) e; raise e);
-
-(*Which thms could apply to goal i? (debugs tactics involving filter_thms) *)
-fun filter_goal could ths i = filter_thms could (999, getgoal i, ths);
-
-(*For inspecting earlier levels of the backward proof*)
-fun chop_level n (pair,pairs) =
- let val level = length pairs
- in if n<0 andalso ~n <= level
- then List.drop (pair::pairs, ~n)
- else if 0<=n andalso n<= level
- then List.drop (pair::pairs, level - n)
- else error ("Level number must lie between 0 and " ^
- string_of_int level)
- end;
-
-(*Print the given level of the proof; prlev ~1 prints previous level*)
-fun prlev n = apply_fun (print_top o pop o (chop_level n));
-fun pr () = apply_fun print_top;
-
-(*Set goals_limit and print again*)
-fun prlim n = (goals_limit:=n; pr());
-
-(** the goal.... commands
- Read main goal. Set global variables curr_prems, curr_mkresult.
- Initial subgoal and premises are rewritten using rths. **)
-
-(*Version taking the goal as a cterm; if you have a term t and theory thy, use
- goalw_cterm rths (cterm_of thy t); *)
-fun agoalw_cterm atomic rths chorn =
- let val (prems, st0, mkresult) = prepare_proof atomic rths chorn
- in undo_list := [];
- setstate [ (st0, Seq.empty) ];
- curr_prems := prems;
- curr_mkresult := mkresult;
- prems
- end;
-
-val goalw_cterm = agoalw_cterm false;
-
-(*Version taking the goal as a string*)
-fun agoalw atomic thy rths agoal =
- agoalw_cterm atomic rths (cterm_of thy (Syntax.read_prop_global thy agoal))
- handle ERROR msg => cat_error msg (*from type_assign, etc via prepare_proof*)
- ("The error(s) above occurred for " ^ quote agoal);
-
-val goalw = agoalw false;
-fun goal thy = goalw thy [];
-
-(*now the versions that wrap the goal up in `Goal' to make it atomic*)
-fun Goalw thms s = agoalw true (ML_Context.the_global_context ()) thms s;
-val Goal = Goalw [];
-
-(*simple version with minimal amount of checking and postprocessing*)
-fun simple_prove_goal_cterm G f =
- let
- val As = Drule.strip_imp_prems G;
- val B = Drule.strip_imp_concl G;
- val asms = map Assumption.assume As;
- fun check NONE = error "prove_goal: tactic failed"
- | check (SOME (thm, _)) = (case nprems_of thm of
- 0 => thm
- | i => !result_error_fn thm (string_of_int i ^ " unsolved goals!"))
- in
- Drule.export_without_context (implies_intr_list As
- (check (Seq.pull (EVERY (f asms) (Thm.trivial B)))))
- end;
-
-
-(*Proof step "by" the given tactic -- apply tactic to the proof state*)
-fun by_com tac ((th,ths), pairs) : gstack =
- (case Seq.pull(tac th) of
- NONE => error"by: tactic failed"
- | SOME(th2,ths2) =>
- (if Thm.eq_thm(th,th2)
- then warning "Warning: same as previous level"
- else if Thm.eq_thm_thy(th,th2) then ()
- else warning ("Warning: theory of proof state has changed" ^
- thy_error (Thm.theory_of_thm th, Thm.theory_of_thm th2));
- ((th2,ths2)::(th,ths)::pairs)));
-
-fun by tac = cond_timeit (!Output.timing) ""
- (fn() => make_command (by_com tac));
-
-(* byev[tac1,...,tacn] applies tac1 THEN ... THEN tacn.
- Good for debugging proofs involving prove_goal.*)
-val byev = by o EVERY;
-
-
-(*Backtracking means find an alternative result from a tactic.
- If none at this level, try earlier levels*)
-fun backtrack [] = error"back: no alternatives"
- | backtrack ((th,thstr) :: pairs) =
- (case Seq.pull thstr of
- NONE => (writeln"Going back a level..."; backtrack pairs)
- | SOME(th2,thstr2) =>
- (if Thm.eq_thm(th,th2)
- then warning "Warning: same as previous choice at this level"
- else if Thm.eq_thm_thy(th,th2) then ()
- else warning "Warning: theory of proof state has changed";
- (th2,thstr2)::pairs));
-
-fun back() = setstate (backtrack (getstate()));
-
-(*Chop back to previous level of the proof*)
-fun choplev n = make_command (chop_level n);
-
-(*Chopping back the goal stack*)
-fun chop () = make_command (fn (_,pairs) => pairs);
-
-(*Restore the previous proof state; discard current state. *)
-fun undo() = case !undo_list of
- [] => error"No proof state"
- | [_] => error"Already at initial state"
- | _::newundo => (undo_list := newundo; pr()) ;
-
-
-(*** Managing the proof stack ***)
-
-fun save_proof() = Proof(!undo_list, !curr_prems, !curr_mkresult);
-
-fun restore_proof(Proof(ul,prems,mk)) =
- (undo_list:= ul; curr_prems:= prems; curr_mkresult := mk; prems);
-
-
-fun top_proof() = case !proofstack of
- [] => error("Stack of proof attempts is empty!")
- | p::ps => (p,ps);
-
-(* push a copy of the current proof state on to the stack *)
-fun push_proof() = (proofstack := (save_proof() :: !proofstack));
-
-(* discard the top proof state of the stack *)
-fun pop_proof() =
- let val (p,ps) = top_proof()
- val prems = restore_proof p
- in proofstack := ps; pr(); prems end;
-
-(* rotate the stack so that the top element goes to the bottom *)
-fun rotate_proof() =
- let val (p,ps) = top_proof()
- in proofstack := ps@[save_proof()];
- restore_proof p;
- pr();
- !curr_prems
- end;
-
-
-(** theorem bindings **)
-
-fun qed name = ML_Context.ml_store_thm (name, result ());
-fun qed_goal name thy goal tacsf = ML_Context.ml_store_thm (name, prove_goal thy goal tacsf);
-fun qed_goalw name thy rews goal tacsf =
- ML_Context.ml_store_thm (name, prove_goalw thy rews goal tacsf);
-fun qed_spec_mp name =
- ML_Context.ml_store_thm (name, Object_Logic.rulify_no_asm (result ()));
-fun qed_goal_spec_mp name thy s p =
- bind_thm (name, Object_Logic.rulify_no_asm (prove_goal thy s p));
-fun qed_goalw_spec_mp name thy defs s p =
- bind_thm (name, Object_Logic.rulify_no_asm (prove_goalw thy defs s p));
-
-end;
-
--- a/src/Pure/pure_thy.ML Thu Sep 02 00:50:51 2010 +0200
+++ b/src/Pure/pure_thy.ML Thu Sep 02 08:29:30 2010 +0200
@@ -320,6 +320,7 @@
("_indexvar", typ "index", Delimfix "'\\<index>"),
("_struct", typ "index => logic", Mixfix ("\\<struct>_", [1000], 1000)),
("_update_name", typ "idt", NoSyn),
+ (Syntax.constrainAbsC, typ "'a", NoSyn),
(const "==>", typ "prop => prop => prop", Delimfix "op ==>"),
(const Term.dummy_patternN, typ "aprop", Delimfix "'_"),
("_sort_constraint", typ "type => prop", Delimfix "(1SORT'_CONSTRAINT/(1'(_')))"),
--- a/src/Tools/Code/code_haskell.ML Thu Sep 02 00:50:51 2010 +0200
+++ b/src/Tools/Code/code_haskell.ML Thu Sep 02 08:29:30 2010 +0200
@@ -397,6 +397,12 @@
@ map serialize_module (Symtab.dest hs_program))
end;
+val serializer : Code_Target.serializer =
+ Code_Target.parse_args (Scan.option (Args.$$$ "root" -- Args.colon |-- Args.name)
+ -- Scan.optional (Args.$$$ "string_classes" >> K true) false
+ >> (fn (module_prefix, string_classes) =>
+ serialize_haskell module_prefix string_classes));
+
val literals = let
fun char_haskell c =
let
@@ -465,12 +471,6 @@
(** Isar setup **)
-val isar_serializer =
- Code_Target.parse_args (Scan.option (Args.$$$ "root" -- Args.colon |-- Args.name)
- -- Scan.optional (Args.$$$ "string_classes" >> K true) false
- >> (fn (module_prefix, string_classes) =>
- serialize_haskell module_prefix string_classes));
-
val _ =
Outer_Syntax.command "code_monad" "define code syntax for monads" Keyword.thy_decl (
Parse.term_group -- Parse.name >> (fn (raw_bind, target) =>
@@ -479,7 +479,7 @@
val setup =
Code_Target.add_target
- (target, { serializer = isar_serializer, literals = literals,
+ (target, { serializer = serializer, literals = literals,
check = { env_var = "EXEC_GHC", make_destination = I,
make_command = fn ghc => fn module_name =>
ghc ^ " -fglasgow-exts -odir build -hidir build -stubdir build -e \"\" " ^ module_name ^ ".hs" } })
--- a/src/Tools/Code/code_ml.ML Thu Sep 02 00:50:51 2010 +0200
+++ b/src/Tools/Code/code_ml.ML Thu Sep 02 08:29:30 2010 +0200
@@ -935,26 +935,26 @@
end; (*local*)
-
-(** Isar setup **)
-
-val isar_serializer_sml =
+val serializer_sml : Code_Target.serializer =
Code_Target.parse_args (Scan.optional (Args.$$$ "no_signatures" >> K false) true
>> (fn with_signatures => serialize_ml target_SML
print_sml_module print_sml_stmt with_signatures));
-val isar_serializer_ocaml =
+val serializer_ocaml : Code_Target.serializer =
Code_Target.parse_args (Scan.optional (Args.$$$ "no_signatures" >> K false) true
>> (fn with_signatures => serialize_ml target_OCaml
print_ocaml_module print_ocaml_stmt with_signatures));
+
+(** Isar setup **)
+
val setup =
Code_Target.add_target
- (target_SML, { serializer = isar_serializer_sml, literals = literals_sml,
+ (target_SML, { serializer = serializer_sml, literals = literals_sml,
check = { env_var = "ISABELLE_PROCESS", make_destination = fn p => Path.append p (Path.explode "ROOT.ML"),
make_command = fn isabelle => fn _ => isabelle ^ " -r -q -u Pure" } })
#> Code_Target.add_target
- (target_OCaml, { serializer = isar_serializer_ocaml, literals = literals_ocaml,
+ (target_OCaml, { serializer = serializer_ocaml, literals = literals_ocaml,
check = { env_var = "EXEC_OCAML", make_destination = fn p => Path.append p (Path.explode "ROOT.ocaml"),
make_command = fn ocaml => fn _ => ocaml ^ " -w pu nums.cma ROOT.ocaml" } })
#> Code_Target.add_tyco_syntax target_SML "fun" (SOME (2, fn print_typ => fn fxy => fn [ty1, ty2] =>
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/Code/code_namespace.ML Thu Sep 02 08:29:30 2010 +0200
@@ -0,0 +1,129 @@
+(* Title: Tools/Code/code_namespace.ML
+ Author: Florian Haftmann, TU Muenchen
+
+Mastering target language namespaces.
+*)
+
+signature CODE_NAMESPACE =
+sig
+ datatype 'a node =
+ Dummy
+ | Stmt of Code_Thingol.stmt
+ | Module of ('a * (string * 'a node) Graph.T);
+ val hierarchical_program: (string -> string) -> { module_alias: string -> string option,
+ reserved: Name.context, empty_nsp: 'b, namify_module: string -> 'b -> string * 'b,
+ namify_stmt: Code_Thingol.stmt -> string -> 'b -> string * 'b,
+ cyclic_modules: bool, empty_data: 'a, memorize_data: string -> 'a -> 'a }
+ -> Code_Thingol.program
+ -> { deresolver: string list -> string -> string,
+ hierarchical_program: (string * 'a node) Graph.T }
+end;
+
+structure Code_Namespace : CODE_NAMESPACE =
+struct
+
+(* hierarchical program structure *)
+
+datatype 'a node =
+ Dummy
+ | Stmt of Code_Thingol.stmt
+ | Module of ('a * (string * 'a node) Graph.T);
+
+fun hierarchical_program labelled_name { module_alias, reserved, empty_nsp,
+ namify_module, namify_stmt, cyclic_modules, empty_data, memorize_data } program =
+ let
+
+ (* 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 Code_Printer.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 = (empty_data, Graph.empty);
+ fun map_module f (Module content) = Module (f content);
+ fun change_module [] = I
+ | change_module (name_fragment :: name_fragments) =
+ apsnd o Graph.map_node name_fragment o apsnd o map_module
+ o change_module name_fragments;
+ fun ensure_module name_fragment (data, nodes) =
+ if can (Graph.get_node nodes) name_fragment then (data, nodes)
+ else (data,
+ nodes |> Graph.new_node (name_fragment, (name_fragment, Module empty_module)));
+ fun allocate_module [] = I
+ | allocate_module (name_fragment :: name_fragments) =
+ ensure_module name_fragment
+ #> (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;
+
+ (* distribute statements over hierarchy *)
+ fun add_stmt name stmt =
+ let
+ val (name_fragments, base) = dest_name name;
+ in
+ change_module name_fragments (fn (data, nodes) =>
+ (memorize_data name data, Graph.new_node (name, (base, Stmt stmt)) nodes))
+ end;
+ 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 (is_module, dep) = if null diff then (false, (name, name'))
+ else (true, (hd diff, hd diff'))
+ val add_edge = if is_module andalso not cyclic_modules
+ then (fn node => Graph.add_edge_acyclic dep node
+ handle Graph.CYCLES _ => error ("Dependency "
+ ^ quote name ^ " -> " ^ quote name'
+ ^ " would result in module dependency cycle"))
+ else Graph.add_edge dep
+ in (change_module name_fragments_common o apsnd) add_edge end;
+ val proto_program = empty_program
+ |> Graph.fold (fn (name, (stmt, _)) => add_stmt name stmt) program
+ |> Graph.fold (fn (name, (_, (_, names))) => fold (add_dependency name) names) program;
+
+ (* name declarations *)
+ fun make_declarations nsps (data, nodes) =
+ let
+ val (module_fragments, stmt_names) = List.partition
+ (fn name_fragment => case Graph.get_node nodes name_fragment
+ of (_, Module _) => true | _ => false) (Graph.keys nodes);
+ fun modify_stmt (Stmt (Code_Thingol.Datatypecons _)) = Dummy
+ | modify_stmt (Stmt (Code_Thingol.Classrel _)) = Dummy
+ | modify_stmt (Stmt (Code_Thingol.Classparam _)) = Dummy
+ | modify_stmt stmt = stmt;
+ fun declare namify modify name (nsps, nodes) =
+ let
+ val (base, node) = Graph.get_node nodes name;
+ val (base', nsps') = namify node base nsps;
+ val nodes' = Graph.map_node name (K (base', modify node)) nodes;
+ in (nsps', nodes') end;
+ val (nsps', nodes') = (nsps, nodes)
+ |> fold (declare (K namify_module) I) module_fragments
+ |> fold (declare (namify_stmt o (fn Stmt stmt => stmt)) modify_stmt) stmt_names;
+ val nodes'' = nodes'
+ |> fold (fn name_fragment => (Graph.map_node name_fragment
+ o apsnd o map_module) (make_declarations nsps')) module_fragments;
+ in (data, nodes'') end;
+ val (_, hierarchical_program) = make_declarations empty_nsp proto_program;
+
+ (* deresolving *)
+ fun deresolver prefix_fragments name =
+ let
+ val (name_fragments, _) = dest_name name;
+ val (_, (_, remainder)) = chop_prefix (op =) (prefix_fragments, name_fragments);
+ val nodes = fold (fn name_fragment => fn nodes => case Graph.get_node nodes name_fragment
+ of (_, Module (_, nodes)) => nodes) name_fragments hierarchical_program;
+ val (base', _) = Graph.get_node nodes name;
+ in Long_Name.implode (remainder @ [base']) end
+ handle Graph.UNDEF _ => error ("Unknown statement name: " ^ labelled_name name);
+
+ in { deresolver = deresolver, hierarchical_program = hierarchical_program } end;
+
+end;
\ No newline at end of file
--- a/src/Tools/Code/code_preproc.ML Thu Sep 02 00:50:51 2010 +0200
+++ b/src/Tools/Code/code_preproc.ML Thu Sep 02 08:29:30 2010 +0200
@@ -92,7 +92,7 @@
val thm_sym = Thm.symmetric thm;
in
thy |> map_pre_post (fn (pre, post) =>
- (pre |> MetaSimplifier.add_simp thm, post |> MetaSimplifier.del_simp thm_sym))
+ (pre |> MetaSimplifier.add_simp thm, post |> MetaSimplifier.add_simp thm_sym))
end;
fun add_functrans (name, f) = (map_data o apsnd)
--- a/src/Tools/Code/code_scala.ML Thu Sep 02 00:50:51 2010 +0200
+++ b/src/Tools/Code/code_scala.ML Thu Sep 02 08:29:30 2010 +0200
@@ -281,74 +281,8 @@
end;
in print_stmt end;
-local
-
-(* hierarchical module name space *)
-
-datatype node =
- Dummy
- | Stmt of Code_Thingol.stmt
- | Module of (string list * (string * node) Graph.T);
-
-in
-
fun scala_program_of_program labelled_name reserved module_alias program =
let
-
- (* 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 = ([], Graph.empty);
- fun map_module f (Module content) = Module (f content);
- fun change_module [] = I
- | change_module (name_fragment :: name_fragments) =
- apsnd o Graph.map_node name_fragment o apsnd o map_module
- o change_module name_fragments;
- fun ensure_module name_fragment (implicits, nodes) =
- if can (Graph.get_node nodes) name_fragment then (implicits, nodes)
- else (implicits,
- nodes |> Graph.new_node (name_fragment, (name_fragment, Module empty_module)));
- fun allocate_module [] = I
- | allocate_module (name_fragment :: name_fragments) =
- ensure_module name_fragment
- #> (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;
-
- (* distribute statements over hierarchy *)
- fun add_stmt name stmt =
- let
- val (name_fragments, base) = dest_name name;
- 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);
- in
- change_module name_fragments (fn (implicits, nodes) =>
- (union (op =) implicit_deps implicits, Graph.new_node (name, (base, Stmt stmt)) nodes))
- end;
- 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) (Graph.add_edge dep) end;
- val proto_program = empty_program
- |> Graph.fold (fn (name, (stmt, _)) => add_stmt name stmt) program
- |> Graph.fold (fn (name, (_, (_, names))) => fold (add_dependency name) names) program;
-
- (* name declarations *)
fun namify_module name_fragment ((nsp_class, nsp_object), nsp_common) =
let
val declare = Name.declare name_fragment;
@@ -376,42 +310,19 @@
| namify_stmt (Code_Thingol.Classrel _) = namify_object
| namify_stmt (Code_Thingol.Classparam _) = namify_object
| namify_stmt (Code_Thingol.Classinst _) = namify_common false;
- fun make_declarations nsps (implicits, nodes) =
+ fun memorize_implicits name =
let
- val (module_fragments, stmt_names) = List.partition
- (fn name_fragment => case Graph.get_node nodes name_fragment
- of (_, Module _) => true | _ => false) (Graph.keys nodes);
- fun modify_stmt (Stmt (Code_Thingol.Datatypecons _)) = Dummy
- | modify_stmt (Stmt (Code_Thingol.Classrel _)) = Dummy
- | modify_stmt (Stmt (Code_Thingol.Classparam _)) = Dummy
- | modify_stmt stmt = stmt;
- fun declare namify modify name (nsps, nodes) =
- let
- val (base, node) = Graph.get_node nodes name;
- val (base', nsps') = namify node base nsps;
- val nodes' = Graph.map_node name (K (base', modify node)) nodes;
- in (nsps', nodes') end;
- val (nsps', nodes') = (nsps, nodes)
- |> fold (declare (K namify_module) I) module_fragments
- |> fold (declare (namify_stmt o (fn Stmt stmt => stmt)) modify_stmt) stmt_names;
- val nodes'' = nodes'
- |> fold (fn name_fragment => (Graph.map_node name_fragment
- o apsnd o map_module) (make_declarations nsps')) module_fragments;
- in (implicits, nodes'') end;
- val (_, sca_program) = make_declarations ((reserved, reserved), reserved) proto_program;
-
- (* deresolving *)
- fun deresolver prefix_fragments name =
- let
- val (name_fragments, _) = dest_name name;
- val (_, (_, remainder)) = chop_prefix (op =) (prefix_fragments, name_fragments);
- val nodes = fold (fn name_fragment => fn nodes => case Graph.get_node nodes name_fragment
- of (_, Module (_, nodes)) => nodes) name_fragments sca_program;
- val (base', _) = Graph.get_node nodes name;
- in Long_Name.implode (remainder @ [base']) end
- handle Graph.UNDEF _ => error ("Unknown statement name: " ^ labelled_name name);
-
- in (deresolver, sca_program) end;
+ fun is_classinst stmt = case stmt
+ of Code_Thingol.Classinst _ => true
+ | _ => false;
+ val implicits = filter (is_classinst o Graph.get_node program)
+ (Graph.imm_succs program name);
+ in union (op =) implicits end;
+ in
+ Code_Namespace.hierarchical_program labelled_name { module_alias = module_alias, reserved = reserved,
+ empty_nsp = ((reserved, reserved), reserved), namify_module = namify_module, namify_stmt = namify_stmt,
+ cyclic_modules = true, empty_data = [], memorize_data = memorize_implicits } program
+ end;
fun serialize_scala { labelled_name, reserved_syms, includes,
module_alias, class_syntax, tyco_syntax, const_syntax, program,
@@ -420,8 +331,8 @@
(* build program *)
val reserved = fold (insert (op =) o fst) includes reserved_syms;
- val (deresolver, sca_program) = scala_program_of_program labelled_name
- (Name.make_context reserved) module_alias program;
+ val { deresolver, hierarchical_program = 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
@@ -454,12 +365,12 @@
val s = deresolver prefix_fragments implicit;
in if length (Long_Name.explode s) = 1 then NONE else SOME (str s) end;
fun print_node _ (_, Dummy) = NONE
- | print_node prefix_fragments (name, Stmt stmt) =
+ | print_node prefix_fragments (name, Code_Namespace.Stmt stmt) =
if null presentation_names
orelse member (op =) presentation_names name
then SOME (print_stmt (deresolver prefix_fragments, deresolver []) (name, stmt))
else NONE
- | print_node prefix_fragments (name_fragment, Module (implicits, nodes)) =
+ | print_node prefix_fragments (name_fragment, Code_Namespace.Module (implicits, nodes)) =
if null presentation_names
then
let
@@ -477,8 +388,7 @@
in if null ps then NONE else SOME (Pretty.chunks2 ps) end;
(* serialization *)
- val p_includes = if null presentation_names
- then map (fn (base, p) => print_module base [] p) includes else [];
+ val p_includes = if null presentation_names then map snd includes else [];
val p = Pretty.chunks2 (p_includes @ the_list (print_nodes [] sca_program));
fun write width NONE = writeln_pretty width
| write width (SOME p) = File.write p o string_of_pretty width;
@@ -486,7 +396,8 @@
Code_Target.serialization write (rpair [] oo string_of_pretty) p
end;
-end; (*local*)
+val serializer : Code_Target.serializer =
+ Code_Target.parse_args (Scan.succeed ()) #> K serialize_scala;
val literals = let
fun char_scala c = if c = "'" then "\\'"
@@ -503,8 +414,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.Nat(" ^ numeral_scala k ^ ")",
- literal_alternative_numeral = fn k => "Natural.Nat(" ^ numeral_scala k ^ ")",
+ literal_positive_numeral = fn k => "Nat(" ^ numeral_scala k ^ ")",
+ literal_alternative_numeral = fn k => "Natural(" ^ 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, "::")
@@ -513,12 +424,9 @@
(** Isar setup **)
-val isar_serializer =
- Code_Target.parse_args (Scan.succeed ()) #> K serialize_scala;
-
val setup =
Code_Target.add_target
- (target, { serializer = isar_serializer, literals = literals,
+ (target, { serializer = serializer, literals = literals,
check = { env_var = "SCALA_HOME", make_destination = fn p => Path.append p (Path.explode "ROOT.scala"),
make_command = fn scala_home => fn _ =>
"export JAVA_OPTS='-Xms128m -Xmx512m -Xss2m' && "
--- a/src/Tools/Code/lib/Tools/codegen Thu Sep 02 00:50:51 2010 +0200
+++ b/src/Tools/Code/lib/Tools/codegen Thu Sep 02 08:29:30 2010 +0200
@@ -53,13 +53,13 @@
if [ "$QUICK_AND_DIRTY" -eq 1 ]
then
- QND_CMD="set"
+ QND_FLAG="true"
else
- QND_CMD="reset"
+ QND_FLAG="false"
fi
CTXT_CMD="ML_Context.eval_text_in (SOME (ProofContext.init_global (Thy_Info.get_theory \"HOL\"))) false Position.none \"Code_Target.shell_command thyname cmd\";"
-FULL_CMD="Unsynchronized.$QND_CMD quick_and_dirty; val thyname = \"$THY\"; val cmd = \"$CODE_CMD\"; $CTXT_CMD"
+FULL_CMD="quick_and_dirty := QND_FLAG; val thyname = \"$THY\"; val cmd = \"$CODE_CMD\"; $CTXT_CMD"
"$ISABELLE_PROCESS" -q -e "$FULL_CMD" "$IMAGE" || exit 1
--- a/src/Tools/Code_Generator.thy Thu Sep 02 00:50:51 2010 +0200
+++ b/src/Tools/Code_Generator.thy Thu Sep 02 08:29:30 2010 +0200
@@ -17,10 +17,11 @@
"~~/src/Tools/Code/code_simp.ML"
"~~/src/Tools/Code/code_printer.ML"
"~~/src/Tools/Code/code_target.ML"
+ "~~/src/Tools/Code/code_namespace.ML"
"~~/src/Tools/Code/code_ml.ML"
- "~~/src/Tools/Code/code_eval.ML"
"~~/src/Tools/Code/code_haskell.ML"
"~~/src/Tools/Code/code_scala.ML"
+ "~~/src/Tools/Code/code_eval.ML"
"~~/src/Tools/nbe.ML"
begin
@@ -28,9 +29,9 @@
Code_Preproc.setup
#> Code_Simp.setup
#> Code_ML.setup
- #> Code_Eval.setup
#> Code_Haskell.setup
#> Code_Scala.setup
+ #> Code_Eval.setup
#> Nbe.setup
#> Quickcheck.setup
*}
--- a/src/Tools/jEdit/src/jedit/document_model.scala Thu Sep 02 00:50:51 2010 +0200
+++ b/src/Tools/jEdit/src/jedit/document_model.scala Thu Sep 02 08:29:30 2010 +0200
@@ -190,19 +190,6 @@
class Document_Model(val session: Session, val buffer: Buffer, val thy_name: String)
{
- /* visible line end */
-
- // simplify slightly odd result of TextArea.getLineEndOffset
- // NB: jEdit already normalizes \r\n and \r to \n
- def visible_line_end(start: Text.Offset, end: Text.Offset): Text.Offset =
- {
- val end1 = end - 1
- if (start <= end1 && end1 < buffer.getLength &&
- buffer.getSegment(end1, 1).charAt(0) == '\n') end1
- else end
- }
-
-
/* pending text edits */
object pending_edits // owned by Swing thread
--- a/src/Tools/jEdit/src/jedit/document_view.scala Thu Sep 02 00:50:51 2010 +0200
+++ b/src/Tools/jEdit/src/jedit/document_view.scala Thu Sep 02 08:29:30 2010 +0200
@@ -97,6 +97,24 @@
}
+ /* visible line ranges */
+
+ // simplify slightly odd result of TextArea.getScreenLineEndOffset etc.
+ // NB: jEdit already normalizes \r\n and \r to \n
+ def proper_line_range(start: Text.Offset, end: Text.Offset): Text.Range =
+ {
+ val stop = if (start < end) end - 1 else end min model.buffer.getLength
+ Text.Range(start, stop)
+ }
+
+ def screen_lines_range(): Text.Range =
+ {
+ val start = text_area.getScreenLineStartOffset(0)
+ val raw_end = text_area.getScreenLineEndOffset(text_area.getVisibleLines - 1 max 0)
+ proper_line_range(start, if (raw_end >= 0) raw_end else model.buffer.getLength)
+ }
+
+
/* commands_changed_actor */
private val commands_changed_actor = actor {
@@ -106,23 +124,25 @@
val buffer = model.buffer
Isabelle.swing_buffer_lock(buffer) {
val snapshot = model.snapshot()
- if (changed.exists(snapshot.node.commands.contains)) {
- var visible_change = false
- for ((command, start) <- snapshot.node.command_starts) {
- if (changed(command)) {
- val stop = start + command.length
- val line1 = buffer.getLineOfOffset(snapshot.convert(start))
- val line2 = buffer.getLineOfOffset(snapshot.convert(stop))
- if (line2 >= text_area.getFirstLine &&
- line1 <= text_area.getFirstLine + text_area.getVisibleLines)
- visible_change = true
- text_area.invalidateLineRange(line1, line2)
- }
- }
+
+ if (changed.exists(snapshot.node.commands.contains))
+ overview.repaint()
+
+ val visible_range = screen_lines_range()
+ val visible_cmds = snapshot.node.command_range(snapshot.revert(visible_range)).map(_._1)
+ if (visible_cmds.exists(changed)) {
+ for {
+ line <- 0 until text_area.getVisibleLines
+ val start = text_area.getScreenLineStartOffset(line) if start >= 0
+ val end = text_area.getScreenLineEndOffset(line) if end >= 0
+ val range = proper_line_range(start, end)
+ val line_cmds = snapshot.node.command_range(snapshot.revert(range)).map(_._1)
+ if line_cmds.exists(changed)
+ } text_area.invalidateScreenLineRange(line, line)
+
// FIXME danger of deadlock!?
- if (visible_change) model.buffer.propertiesChanged()
-
- overview.repaint() // FIXME really paint here!?
+ // FIXME potentially slow!?
+ model.buffer.propertiesChanged()
}
}
@@ -138,49 +158,26 @@
{
override def paintScreenLineRange(gfx: Graphics2D,
first_line: Int, last_line: Int, physical_lines: Array[Int],
- start: Array[Int], end: Array[Int], y0: Int, line_height: Int)
+ start: Array[Int], end: Array[Int], y: Int, line_height: Int)
{
Isabelle.swing_buffer_lock(model.buffer) {
val snapshot = model.snapshot()
-
- val command_range: Iterable[(Command, Text.Offset)] =
- {
- val range = snapshot.node.command_range(snapshot.revert(start(0)))
- if (range.hasNext) {
- val (cmd0, start0) = range.next
- new Iterable[(Command, Text.Offset)] {
- def iterator =
- Document.Node.command_starts(snapshot.node.commands.iterator(cmd0), start0)
- }
- }
- else Iterable.empty
- }
-
val saved_color = gfx.getColor
try {
- var y = y0
for (i <- 0 until physical_lines.length) {
if (physical_lines(i) != -1) {
- val line_start = start(i)
- val line_end = model.visible_line_end(line_start, end(i))
-
- val a = snapshot.revert(line_start)
- val b = snapshot.revert(line_end)
- val cmds = command_range.iterator.
- dropWhile { case (cmd, c) => c + cmd.length <= a } .
- takeWhile { case (_, c) => c < b }
-
+ val line_range = proper_line_range(start(i), end(i))
+ val cmds = snapshot.node.command_range(snapshot.revert(line_range))
for ((command, command_start) <- cmds if !command.is_ignored) {
- val p =
- text_area.offsetToXY(line_start max snapshot.convert(command_start))
- val q =
- text_area.offsetToXY(line_end min snapshot.convert(command_start + command.length))
- if (p.y != q.y) System.err.println("Unexpected coordinates: " + p + ", " + q)
- gfx.setColor(Document_View.choose_color(snapshot, command))
- gfx.fillRect(p.x, y, q.x - p.x, line_height)
+ val range = line_range.restrict(snapshot.convert(command.range + command_start))
+ val p = text_area.offsetToXY(range.start)
+ val q = text_area.offsetToXY(range.stop)
+ if (p != null && q != null) {
+ gfx.setColor(Document_View.choose_color(snapshot, command))
+ gfx.fillRect(p.x, y + i * line_height, q.x - p.x, line_height)
+ }
}
}
- y += line_height
}
}
finally { gfx.setColor(saved_color) }
--- a/src/Tools/jEdit/src/jedit/output_dockable.scala Thu Sep 02 00:50:51 2010 +0200
+++ b/src/Tools/jEdit/src/jedit/output_dockable.scala Thu Sep 02 08:29:30 2010 +0200
@@ -67,12 +67,12 @@
case Some(cmd) if !restriction.isDefined || restriction.get.contains(cmd) =>
val snapshot = doc_view.model.snapshot()
val filtered_results =
- snapshot.state(cmd).results filter {
+ snapshot.state(cmd).results.iterator.map(_._2) filter {
case XML.Elem(Markup(Markup.TRACING, _), _) => show_tracing
case XML.Elem(Markup(Markup.DEBUG, _), _) => show_debug
case _ => true
}
- html_panel.render(filtered_results)
+ html_panel.render(filtered_results.toList)
case _ =>
}
case None =>