--- a/src/HOL/OrderedGroup.thy Sun Mar 22 19:36:04 2009 +0100
+++ b/src/HOL/OrderedGroup.thy Sun Mar 22 19:43:21 2009 +0100
@@ -316,6 +316,9 @@
lemma eq_iff_diff_eq_0: "a = b \<longleftrightarrow> a - b = 0"
by (simp add: algebra_simps)
+lemma diff_eq_0_iff_eq [simp, noatp]: "a - b = 0 \<longleftrightarrow> a = b"
+by (simp add: algebra_simps)
+
end
subsection {* (Partially) Ordered Groups *}
@@ -1296,7 +1299,7 @@
done
lemma eq_eqI: "(x::'a::ab_group_add) - y = x' - y' \<Longrightarrow> (x = y) = (x' = y')"
-by (simp add: eq_iff_diff_eq_0[of x y] eq_iff_diff_eq_0[of x' y'])
+by (simp only: eq_iff_diff_eq_0[of x y] eq_iff_diff_eq_0[of x' y'])
lemma diff_def: "(x::'a::ab_group_add) - y == x + (-y)"
by (simp add: diff_minus)
@@ -1344,7 +1347,6 @@
text{*Simplification of @{term "x-y < 0"}, etc.*}
lemmas diff_less_0_iff_less [simp, noatp] = less_iff_diff_less_0 [symmetric]
-lemmas diff_eq_0_iff_eq [simp, noatp] = eq_iff_diff_eq_0 [symmetric]
lemmas diff_le_0_iff_le [simp, noatp] = le_iff_diff_le_0 [symmetric]
ML {*
--- a/src/HOL/Ring_and_Field.thy Sun Mar 22 19:36:04 2009 +0100
+++ b/src/HOL/Ring_and_Field.thy Sun Mar 22 19:43:21 2009 +0100
@@ -534,7 +534,156 @@
by (simp add: divide_inverse)
lemma add_divide_distrib: "(a+b) / c = a/c + b/c"
-by (simp add: divide_inverse algebra_simps)
+by (simp add: divide_inverse algebra_simps)
+
+text{*There is no slick version using division by zero.*}
+lemma inverse_add:
+ "[| a \<noteq> 0; b \<noteq> 0 |]
+ ==> inverse a + inverse b = (a + b) * inverse a * inverse b"
+by (simp add: division_ring_inverse_add mult_ac)
+
+lemma nonzero_mult_divide_mult_cancel_left [simp, noatp]:
+assumes [simp]: "b\<noteq>0" and [simp]: "c\<noteq>0" shows "(c*a)/(c*b) = a/b"
+proof -
+ have "(c*a)/(c*b) = c * a * (inverse b * inverse c)"
+ by (simp add: divide_inverse nonzero_inverse_mult_distrib)
+ also have "... = a * inverse b * (inverse c * c)"
+ by (simp only: mult_ac)
+ also have "... = a * inverse b" by simp
+ finally show ?thesis by (simp add: divide_inverse)
+qed
+
+lemma nonzero_mult_divide_mult_cancel_right [simp, noatp]:
+ "\<lbrakk>b \<noteq> 0; c \<noteq> 0\<rbrakk> \<Longrightarrow> (a * c) / (b * c) = a / b"
+by (simp add: mult_commute [of _ c])
+
+lemma divide_1 [simp]: "a / 1 = a"
+by (simp add: divide_inverse)
+
+lemma times_divide_eq_right: "a * (b / c) = (a * b) / c"
+by (simp add: divide_inverse mult_assoc)
+
+lemma times_divide_eq_left: "(b / c) * a = (b * a) / c"
+by (simp add: divide_inverse mult_ac)
+
+text {* These are later declared as simp rules. *}
+lemmas times_divide_eq [noatp] = times_divide_eq_right times_divide_eq_left
+
+lemma add_frac_eq:
+ assumes "y \<noteq> 0" and "z \<noteq> 0"
+ shows "x / y + w / z = (x * z + w * y) / (y * z)"
+proof -
+ have "x / y + w / z = (x * z) / (y * z) + (y * w) / (y * z)"
+ using assms by simp
+ also have "\<dots> = (x * z + y * w) / (y * z)"
+ by (simp only: add_divide_distrib)
+ finally show ?thesis
+ by (simp only: mult_commute)
+qed
+
+text{*Special Cancellation Simprules for Division*}
+
+lemma nonzero_mult_divide_cancel_right [simp, noatp]:
+ "b \<noteq> 0 \<Longrightarrow> a * b / b = a"
+using nonzero_mult_divide_mult_cancel_right [of 1 b a] by simp
+
+lemma nonzero_mult_divide_cancel_left [simp, noatp]:
+ "a \<noteq> 0 \<Longrightarrow> a * b / a = b"
+using nonzero_mult_divide_mult_cancel_left [of 1 a b] by simp
+
+lemma nonzero_divide_mult_cancel_right [simp, noatp]:
+ "\<lbrakk>a \<noteq> 0; b \<noteq> 0\<rbrakk> \<Longrightarrow> b / (a * b) = 1 / a"
+using nonzero_mult_divide_mult_cancel_right [of a b 1] by simp
+
+lemma nonzero_divide_mult_cancel_left [simp, noatp]:
+ "\<lbrakk>a \<noteq> 0; b \<noteq> 0\<rbrakk> \<Longrightarrow> a / (a * b) = 1 / b"
+using nonzero_mult_divide_mult_cancel_left [of b a 1] by simp
+
+lemma nonzero_mult_divide_mult_cancel_left2 [simp, noatp]:
+ "\<lbrakk>b \<noteq> 0; c \<noteq> 0\<rbrakk> \<Longrightarrow> (c * a) / (b * c) = a / b"
+using nonzero_mult_divide_mult_cancel_left [of b c a] by (simp add: mult_ac)
+
+lemma nonzero_mult_divide_mult_cancel_right2 [simp, noatp]:
+ "\<lbrakk>b \<noteq> 0; c \<noteq> 0\<rbrakk> \<Longrightarrow> (a * c) / (c * b) = a / b"
+using nonzero_mult_divide_mult_cancel_right [of b c a] by (simp add: mult_ac)
+
+lemma minus_divide_left: "- (a / b) = (-a) / b"
+by (simp add: divide_inverse)
+
+lemma nonzero_minus_divide_right: "b \<noteq> 0 ==> - (a / b) = a / (- b)"
+by (simp add: divide_inverse nonzero_inverse_minus_eq)
+
+lemma nonzero_minus_divide_divide: "b \<noteq> 0 ==> (-a) / (-b) = a / b"
+by (simp add: divide_inverse nonzero_inverse_minus_eq)
+
+lemma divide_minus_left [simp, noatp]: "(-a) / b = - (a / b)"
+by (simp add: divide_inverse)
+
+lemma diff_divide_distrib: "(a - b) / c = a / c - b / c"
+by (simp add: diff_minus add_divide_distrib)
+
+lemma add_divide_eq_iff:
+ "z \<noteq> 0 \<Longrightarrow> x + y / z = (z * x + y) / z"
+by (simp add: add_divide_distrib)
+
+lemma divide_add_eq_iff:
+ "z \<noteq> 0 \<Longrightarrow> x / z + y = (x + z * y) / z"
+by (simp add: add_divide_distrib)
+
+lemma diff_divide_eq_iff:
+ "z \<noteq> 0 \<Longrightarrow> x - y / z = (z * x - y) / z"
+by (simp add: diff_divide_distrib)
+
+lemma divide_diff_eq_iff:
+ "z \<noteq> 0 \<Longrightarrow> x / z - y = (x - z * y) / z"
+by (simp add: diff_divide_distrib)
+
+lemma nonzero_eq_divide_eq: "c \<noteq> 0 \<Longrightarrow> a = b / c \<longleftrightarrow> a * c = b"
+proof -
+ assume [simp]: "c \<noteq> 0"
+ have "a = b / c \<longleftrightarrow> a * c = (b / c) * c" by simp
+ also have "... \<longleftrightarrow> a * c = b" by (simp add: divide_inverse mult_assoc)
+ finally show ?thesis .
+qed
+
+lemma nonzero_divide_eq_eq: "c \<noteq> 0 \<Longrightarrow> b / c = a \<longleftrightarrow> b = a * c"
+proof -
+ assume [simp]: "c \<noteq> 0"
+ have "b / c = a \<longleftrightarrow> (b / c) * c = a * c" by simp
+ also have "... \<longleftrightarrow> b = a * c" by (simp add: divide_inverse mult_assoc)
+ finally show ?thesis .
+qed
+
+lemma divide_eq_imp: "c \<noteq> 0 \<Longrightarrow> b = a * c \<Longrightarrow> b / c = a"
+by simp
+
+lemma eq_divide_imp: "c \<noteq> 0 \<Longrightarrow> a * c = b \<Longrightarrow> a = b / c"
+by (erule subst, simp)
+
+lemmas field_eq_simps[noatp] = algebra_simps
+ (* pull / out*)
+ add_divide_eq_iff divide_add_eq_iff
+ diff_divide_eq_iff divide_diff_eq_iff
+ (* multiply eqn *)
+ nonzero_eq_divide_eq nonzero_divide_eq_eq
+(* is added later:
+ times_divide_eq_left times_divide_eq_right
+*)
+
+text{*An example:*}
+lemma "\<lbrakk>a\<noteq>b; c\<noteq>d; e\<noteq>f\<rbrakk> \<Longrightarrow> ((a-b)*(c-d)*(e-f))/((c-d)*(e-f)*(a-b)) = 1"
+apply(subgoal_tac "(c-d)*(e-f)*(a-b) \<noteq> 0")
+ apply(simp add:field_eq_simps)
+apply(simp)
+done
+
+lemma diff_frac_eq:
+ "y \<noteq> 0 \<Longrightarrow> z \<noteq> 0 \<Longrightarrow> x / y - w / z = (x * z - w * y) / (y * z)"
+by (simp add: field_eq_simps times_divide_eq)
+
+lemma frac_eq_eq:
+ "y \<noteq> 0 \<Longrightarrow> z \<noteq> 0 \<Longrightarrow> (x / y = w / z) = (x * z = w * y)"
+by (simp add: field_eq_simps times_divide_eq)
end
@@ -1212,12 +1361,6 @@
thus ?thesis by force
qed
-text{*There is no slick version using division by zero.*}
-lemma inverse_add:
- "[|a \<noteq> 0; b \<noteq> 0|]
- ==> inverse a + inverse b = (a+b) * inverse a * inverse (b::'a::field)"
-by (simp add: division_ring_inverse_add mult_ac)
-
lemma inverse_divide [simp]:
"inverse (a/b) = b / (a::'a::{field,division_by_zero})"
by (simp add: divide_inverse mult_commute)
@@ -1229,44 +1372,18 @@
field} but none for class @{text field} and @{text nonzero_divides}
because the latter are covered by a simproc. *}
-lemma nonzero_mult_divide_mult_cancel_left[simp,noatp]:
-assumes [simp]: "b\<noteq>0" and [simp]: "c\<noteq>0" shows "(c*a)/(c*b) = a/(b::'a::field)"
-proof -
- have "(c*a)/(c*b) = c * a * (inverse b * inverse c)"
- by (simp add: divide_inverse nonzero_inverse_mult_distrib)
- also have "... = a * inverse b * (inverse c * c)"
- by (simp only: mult_ac)
- also have "... = a * inverse b" by simp
- finally show ?thesis by (simp add: divide_inverse)
-qed
-
lemma mult_divide_mult_cancel_left:
"c\<noteq>0 ==> (c*a) / (c*b) = a / (b::'a::{field,division_by_zero})"
apply (cases "b = 0")
apply (simp_all add: nonzero_mult_divide_mult_cancel_left)
done
-lemma nonzero_mult_divide_mult_cancel_right [noatp]:
- "[|b\<noteq>0; c\<noteq>0|] ==> (a*c) / (b*c) = a/(b::'a::field)"
-by (simp add: mult_commute [of _ c] nonzero_mult_divide_mult_cancel_left)
-
lemma mult_divide_mult_cancel_right:
"c\<noteq>0 ==> (a*c) / (b*c) = a / (b::'a::{field,division_by_zero})"
apply (cases "b = 0")
apply (simp_all add: nonzero_mult_divide_mult_cancel_right)
done
-lemma divide_1 [simp]: "a/1 = (a::'a::field)"
-by (simp add: divide_inverse)
-
-lemma times_divide_eq_right: "a * (b/c) = (a*b) / (c::'a::field)"
-by (simp add: divide_inverse mult_assoc)
-
-lemma times_divide_eq_left: "(b/c) * a = (b*a) / (c::'a::field)"
-by (simp add: divide_inverse mult_ac)
-
-lemmas times_divide_eq[noatp] = times_divide_eq_right times_divide_eq_left
-
lemma divide_divide_eq_right [simp,noatp]:
"a / (b/c) = (a*c) / (b::'a::{field,division_by_zero})"
by (simp add: divide_inverse mult_ac)
@@ -1275,20 +1392,6 @@
"(a / b) / (c::'a::{field,division_by_zero}) = a / (b*c)"
by (simp add: divide_inverse mult_assoc)
-lemma add_frac_eq: "(y::'a::field) ~= 0 ==> z ~= 0 ==>
- x / y + w / z = (x * z + w * y) / (y * z)"
-apply (subgoal_tac "x / y = (x * z) / (y * z)")
-apply (erule ssubst)
-apply (subgoal_tac "w / z = (w * y) / (y * z)")
-apply (erule ssubst)
-apply (rule add_divide_distrib [THEN sym])
-apply (subst mult_commute)
-apply (erule nonzero_mult_divide_mult_cancel_left [THEN sym])
-apply assumption
-apply (erule nonzero_mult_divide_mult_cancel_right [THEN sym])
-apply assumption
-done
-
subsubsection{*Special Cancellation Simprules for Division*}
@@ -1297,140 +1400,29 @@
shows "(c*a) / (c*b) = (if c=0 then 0 else a/b)"
by (simp add: mult_divide_mult_cancel_left)
-lemma nonzero_mult_divide_cancel_right[simp,noatp]:
- "b \<noteq> 0 \<Longrightarrow> a * b / b = (a::'a::field)"
-using nonzero_mult_divide_mult_cancel_right[of 1 b a] by simp
-
-lemma nonzero_mult_divide_cancel_left[simp,noatp]:
- "a \<noteq> 0 \<Longrightarrow> a * b / a = (b::'a::field)"
-using nonzero_mult_divide_mult_cancel_left[of 1 a b] by simp
-
-
-lemma nonzero_divide_mult_cancel_right[simp,noatp]:
- "\<lbrakk> a\<noteq>0; b\<noteq>0 \<rbrakk> \<Longrightarrow> b / (a * b) = 1/(a::'a::field)"
-using nonzero_mult_divide_mult_cancel_right[of a b 1] by simp
-
-lemma nonzero_divide_mult_cancel_left[simp,noatp]:
- "\<lbrakk> a\<noteq>0; b\<noteq>0 \<rbrakk> \<Longrightarrow> a / (a * b) = 1/(b::'a::field)"
-using nonzero_mult_divide_mult_cancel_left[of b a 1] by simp
-
-
-lemma nonzero_mult_divide_mult_cancel_left2[simp,noatp]:
- "[|b\<noteq>0; c\<noteq>0|] ==> (c*a) / (b*c) = a/(b::'a::field)"
-using nonzero_mult_divide_mult_cancel_left[of b c a] by(simp add:mult_ac)
-
-lemma nonzero_mult_divide_mult_cancel_right2[simp,noatp]:
- "[|b\<noteq>0; c\<noteq>0|] ==> (a*c) / (c*b) = a/(b::'a::field)"
-using nonzero_mult_divide_mult_cancel_right[of b c a] by(simp add:mult_ac)
-
subsection {* Division and Unary Minus *}
-lemma nonzero_minus_divide_left: "b \<noteq> 0 ==> - (a/b) = (-a) / (b::'a::field)"
-by (simp add: divide_inverse)
-
-lemma nonzero_minus_divide_right: "b \<noteq> 0 ==> - (a/b) = a / -(b::'a::field)"
-by (simp add: divide_inverse nonzero_inverse_minus_eq)
-
-lemma nonzero_minus_divide_divide: "b \<noteq> 0 ==> (-a)/(-b) = a / (b::'a::field)"
-by (simp add: divide_inverse nonzero_inverse_minus_eq)
-
-lemma minus_divide_left: "- (a/b) = (-a) / (b::'a::field)"
-by (simp add: divide_inverse)
-
lemma minus_divide_right: "- (a/b) = a / -(b::'a::{field,division_by_zero})"
by (simp add: divide_inverse)
-
-text{*The effect is to extract signs from divisions*}
-lemmas divide_minus_left[noatp] = minus_divide_left [symmetric]
-lemmas divide_minus_right[noatp] = minus_divide_right [symmetric]
-declare divide_minus_left [simp] divide_minus_right [simp]
-
-lemma minus_divide_divide [simp]:
+lemma divide_minus_right [simp, noatp]:
+ "a / -(b::'a::{field,division_by_zero}) = -(a / b)"
+by (simp add: divide_inverse)
+
+lemma minus_divide_divide:
"(-a)/(-b) = a / (b::'a::{field,division_by_zero})"
apply (cases "b=0", simp)
apply (simp add: nonzero_minus_divide_divide)
done
-lemma diff_divide_distrib: "(a-b)/(c::'a::field) = a/c - b/c"
-by (simp add: diff_minus add_divide_distrib)
-
-lemma add_divide_eq_iff:
- "(z::'a::field) \<noteq> 0 \<Longrightarrow> x + y/z = (z*x + y)/z"
-by(simp add:add_divide_distrib nonzero_mult_divide_cancel_left)
-
-lemma divide_add_eq_iff:
- "(z::'a::field) \<noteq> 0 \<Longrightarrow> x/z + y = (x + z*y)/z"
-by(simp add:add_divide_distrib nonzero_mult_divide_cancel_left)
-
-lemma diff_divide_eq_iff:
- "(z::'a::field) \<noteq> 0 \<Longrightarrow> x - y/z = (z*x - y)/z"
-by(simp add:diff_divide_distrib nonzero_mult_divide_cancel_left)
-
-lemma divide_diff_eq_iff:
- "(z::'a::field) \<noteq> 0 \<Longrightarrow> x/z - y = (x - z*y)/z"
-by(simp add:diff_divide_distrib nonzero_mult_divide_cancel_left)
-
-lemma nonzero_eq_divide_eq: "c\<noteq>0 ==> ((a::'a::field) = b/c) = (a*c = b)"
-proof -
- assume [simp]: "c\<noteq>0"
- have "(a = b/c) = (a*c = (b/c)*c)" by simp
- also have "... = (a*c = b)" by (simp add: divide_inverse mult_assoc)
- finally show ?thesis .
-qed
-
-lemma nonzero_divide_eq_eq: "c\<noteq>0 ==> (b/c = (a::'a::field)) = (b = a*c)"
-proof -
- assume [simp]: "c\<noteq>0"
- have "(b/c = a) = ((b/c)*c = a*c)" by simp
- also have "... = (b = a*c)" by (simp add: divide_inverse mult_assoc)
- finally show ?thesis .
-qed
-
lemma eq_divide_eq:
"((a::'a::{field,division_by_zero}) = b/c) = (if c\<noteq>0 then a*c = b else a=0)"
-by (simp add: nonzero_eq_divide_eq)
+by (simp add: nonzero_eq_divide_eq)
lemma divide_eq_eq:
"(b/c = (a::'a::{field,division_by_zero})) = (if c\<noteq>0 then b = a*c else a=0)"
-by (force simp add: nonzero_divide_eq_eq)
-
-lemma divide_eq_imp: "(c::'a::{division_by_zero,field}) ~= 0 ==>
- b = a * c ==> b / c = a"
-by (subst divide_eq_eq, simp)
-
-lemma eq_divide_imp: "(c::'a::{division_by_zero,field}) ~= 0 ==>
- a * c = b ==> a = b / c"
-by (subst eq_divide_eq, simp)
-
-
-lemmas field_eq_simps[noatp] = algebra_simps
- (* pull / out*)
- add_divide_eq_iff divide_add_eq_iff
- diff_divide_eq_iff divide_diff_eq_iff
- (* multiply eqn *)
- nonzero_eq_divide_eq nonzero_divide_eq_eq
-(* is added later:
- times_divide_eq_left times_divide_eq_right
-*)
-
-text{*An example:*}
-lemma fixes a b c d e f :: "'a::field"
-shows "\<lbrakk>a\<noteq>b; c\<noteq>d; e\<noteq>f \<rbrakk> \<Longrightarrow> ((a-b)*(c-d)*(e-f))/((c-d)*(e-f)*(a-b)) = 1"
-apply(subgoal_tac "(c-d)*(e-f)*(a-b) \<noteq> 0")
- apply(simp add:field_eq_simps)
-apply(simp)
-done
-
-
-lemma diff_frac_eq: "(y::'a::field) ~= 0 ==> z ~= 0 ==>
- x / y - w / z = (x * z - w * y) / (y * z)"
-by (simp add:field_eq_simps times_divide_eq)
-
-lemma frac_eq_eq: "(y::'a::field) ~= 0 ==> z ~= 0 ==>
- (x / y = w / z) = (x * z = w * y)"
-by (simp add:field_eq_simps times_divide_eq)
+by (force simp add: nonzero_divide_eq_eq)
subsection {* Ordered Fields *}
--- a/src/Pure/Concurrent/future.ML Sun Mar 22 19:36:04 2009 +0100
+++ b/src/Pure/Concurrent/future.ML Sun Mar 22 19:43:21 2009 +0100
@@ -44,6 +44,7 @@
val join_result: 'a future -> 'a Exn.result
val join: 'a future -> 'a
val map: ('a -> 'b) -> 'a future -> 'b future
+ val interruptible_task: ('a -> 'b) -> 'a -> 'b
val interrupt_task: string -> unit
val cancel_group: group -> unit
val cancel: 'a future -> unit
@@ -350,6 +351,15 @@
(* cancellation *)
+fun interruptible_task f x =
+ if Multithreading.available then
+ Multithreading.with_attributes
+ (if is_some (thread_data ())
+ then Multithreading.restricted_interrupts
+ else Multithreading.regular_interrupts)
+ (fn _ => f) x
+ else interruptible f x;
+
(*interrupt: permissive signal, may get ignored*)
fun interrupt_task id = SYNCHRONIZED "interrupt"
(fn () => Task_Queue.interrupt_external (! queue) id);
--- a/src/Pure/General/pretty.ML Sun Mar 22 19:36:04 2009 +0100
+++ b/src/Pure/General/pretty.ML Sun Mar 22 19:43:21 2009 +0100
@@ -19,9 +19,6 @@
a unit for breaking).
*)
-type pprint_args = (output -> unit) * (int -> unit) * (int -> unit) *
- (unit -> unit) * (unit -> unit);
-
signature PRETTY =
sig
val default_indent: string -> int -> output
@@ -49,6 +46,7 @@
val commas: T list -> T list
val enclose: string -> string -> T list -> T
val enum: string -> string -> string -> T list -> T
+ val position: Position.T -> T
val list: string -> string -> T list -> T
val str_list: string -> string -> string list -> T
val big_list: string -> T list -> T
@@ -57,7 +55,8 @@
val setmargin: int -> unit
val setmp_margin: int -> ('a -> 'b) -> 'a -> 'b
val setdepth: int -> unit
- val pprint: T -> pprint_args -> unit
+ val to_ML: T -> ML_Pretty.pretty
+ val from_ML: ML_Pretty.pretty -> T
val symbolicN: string
val output_buffer: T -> Buffer.T
val output: T -> output
@@ -159,6 +158,9 @@
fun enum sep lpar rpar prts = enclose lpar rpar (separate sep prts);
+val position =
+ enum "," "{" "}" o map (fn (x, y) => str (x ^ "=" ^ y)) o Position.properties_of;
+
val list = enum ",";
fun str_list lpar rpar strs = list lpar rpar (map str strs);
@@ -318,20 +320,16 @@
| fmt (Break (true, _)) = Buffer.add (output_spaces 1);
in fmt (prune prt) Buffer.empty end;
-(*ML toplevel pretty printing*)
-fun pprint prt (put_str0, begin_blk, put_brk, put_fbrk, end_blk) =
- let
- fun put_str "" = ()
- | put_str s = put_str0 s;
- fun pp (Block (m, prts, ind, _)) =
- let val (bg, en) = Markup.output m
- in put_str bg; begin_blk ind; pp_lst prts; end_blk (); put_str en end
- | pp (String (s, _)) = put_str s
- | pp (Break (false, wd)) = put_brk wd
- | pp (Break (true, _)) = put_fbrk ()
- and pp_lst [] = ()
- | pp_lst (prt :: prts) = (pp prt; pp_lst prts);
- in pp (prune prt) end;
+
+(* ML toplevel pretty printing *)
+
+fun to_ML (Block (m, prts, ind, _)) = ML_Pretty.Block (Markup.output m, map to_ML prts, ind)
+ | to_ML (String s) = ML_Pretty.String s
+ | to_ML (Break b) = ML_Pretty.Break b;
+
+fun from_ML (ML_Pretty.Block (_, prts, ind)) = blk (ind, map from_ML prts)
+ | from_ML (ML_Pretty.String s) = String s
+ | from_ML (ML_Pretty.Break b) = Break b;
(* output interfaces *)
--- a/src/Pure/General/secure.ML Sun Mar 22 19:36:04 2009 +0100
+++ b/src/Pure/General/secure.ML Sun Mar 22 19:43:21 2009 +0100
@@ -14,6 +14,7 @@
val use_file: ML_NameSpace.nameSpace ->
(string -> unit) * (string -> 'a) -> bool -> string -> unit
val use: string -> unit
+ val toplevel_pp: string list -> string -> unit
val commit: unit -> unit
val system_out: string -> string * int
val system: string -> int
@@ -41,6 +42,8 @@
fun raw_use_text ns = use_text ML_Parse.fix_ints (Position.str_of oo Position.line_file) ns;
fun raw_use_file ns = use_file ML_Parse.fix_ints (Position.str_of oo Position.line_file) ns;
+fun raw_toplevel_pp x =
+ toplevel_pp ML_Parse.fix_ints (Position.str_of oo Position.line_file) Output.ml_output x;
fun use_text ns pos pr verbose txt =
(secure_mltext (); raw_use_text ns pos pr verbose txt);
@@ -50,6 +53,8 @@
fun use name = use_file ML_NameSpace.global Output.ml_output true name;
+fun toplevel_pp path pp = (secure_mltext (); raw_toplevel_pp path pp);
+
(*commit is dynamically bound!*)
fun commit () = raw_use_text ML_NameSpace.global (0, "") Output.ml_output false "commit();";
@@ -73,5 +78,6 @@
val use_text = Secure.use_text;
val use_file = Secure.use_file;
fun use s = Secure.use s handle ERROR msg => (writeln msg; raise Fail "ML error");
+val toplevel_pp = Secure.toplevel_pp;
val system_out = Secure.system_out;
val system = Secure.system;
--- a/src/Pure/General/table.ML Sun Mar 22 19:36:04 2009 +0100
+++ b/src/Pure/General/table.ML Sun Mar 22 19:43:21 2009 +0100
@@ -383,3 +383,6 @@
structure Inttab = TableFun(type key = int val ord = int_ord);
structure Symtab = TableFun(type key = string val ord = fast_string_ord);
+structure Symreltab = TableFun(type key = string * string
+ val ord = prod_ord fast_string_ord fast_string_ord);
+
--- a/src/Pure/IsaMakefile Sun Mar 22 19:36:04 2009 +0100
+++ b/src/Pure/IsaMakefile Sun Mar 22 19:43:21 2009 +0100
@@ -20,17 +20,17 @@
## Pure
BOOTSTRAP_FILES = ML-Systems/exn.ML ML-Systems/ml_name_space.ML \
- ML-Systems/mosml.ML ML-Systems/multithreading.ML \
- ML-Systems/multithreading_polyml.ML ML-Systems/overloading_smlnj.ML \
- ML-Systems/polyml-4.1.3.ML ML-Systems/polyml-4.1.4.ML \
- ML-Systems/polyml-4.2.0.ML ML-Systems/polyml-5.0.ML \
- ML-Systems/polyml-5.1.ML ML-Systems/polyml-experimental.ML \
- ML-Systems/polyml.ML ML-Systems/polyml_common.ML \
- ML-Systems/polyml_old_compiler4.ML \
- ML-Systems/polyml_old_compiler5.ML ML-Systems/proper_int.ML \
- ML-Systems/smlnj.ML ML-Systems/system_shell.ML \
- ML-Systems/thread_dummy.ML ML-Systems/time_limit.ML \
- ML-Systems/universal.ML
+ ML-Systems/ml_pretty.ML ML-Systems/mosml.ML \
+ ML-Systems/multithreading.ML ML-Systems/multithreading_polyml.ML \
+ ML-Systems/overloading_smlnj.ML ML-Systems/polyml-4.1.3.ML \
+ ML-Systems/polyml-4.1.4.ML ML-Systems/polyml-4.2.0.ML \
+ ML-Systems/polyml-5.0.ML ML-Systems/polyml-5.1.ML \
+ ML-Systems/polyml-experimental.ML ML-Systems/polyml.ML \
+ ML-Systems/polyml_common.ML ML-Systems/polyml_old_compiler4.ML \
+ ML-Systems/polyml_old_compiler5.ML ML-Systems/polyml_pp.ML \
+ ML-Systems/proper_int.ML ML-Systems/smlnj.ML \
+ ML-Systems/system_shell.ML ML-Systems/thread_dummy.ML \
+ ML-Systems/time_limit.ML ML-Systems/universal.ML
RAW: $(OUT)/RAW
@@ -69,7 +69,8 @@
Isar/spec_parse.ML Isar/specification.ML Isar/theory_target.ML \
Isar/toplevel.ML Isar/value_parse.ML ML/ml_antiquote.ML \
ML/ml_context.ML ML/ml_lex.ML ML/ml_parse.ML ML/ml_syntax.ML \
- ML/ml_thms.ML ML-Systems/install_pp_polyml.ML Proof/extraction.ML \
+ ML/ml_thms.ML ML-Systems/install_pp_polyml.ML \
+ ML-Systems/install_pp_polyml-experimental.ML Proof/extraction.ML \
Proof/proof_rewrite_rules.ML Proof/proof_syntax.ML \
Proof/proofchecker.ML Proof/reconstruct.ML ProofGeneral/ROOT.ML \
ProofGeneral/pgip.ML ProofGeneral/pgip_input.ML \
--- a/src/Pure/Isar/proof_context.ML Sun Mar 22 19:36:04 2009 +0100
+++ b/src/Pure/Isar/proof_context.ML Sun Mar 22 19:43:21 2009 +0100
@@ -36,7 +36,6 @@
val theory_result: (theory -> 'a * theory) -> Proof.context -> 'a * Proof.context
val extern_fact: Proof.context -> string -> xstring
val pretty_term_abbrev: Proof.context -> term -> Pretty.T
- val pretty_thm_legacy: thm -> Pretty.T
val pretty_thm: Proof.context -> thm -> Pretty.T
val pretty_thms: Proof.context -> thm list -> Pretty.T
val pretty_fact: Proof.context -> string * thm list -> Pretty.T
@@ -296,10 +295,6 @@
fun pretty_term_abbrev ctxt = Syntax.pretty_term (set_mode mode_abbrev ctxt);
-fun pretty_thm_legacy th =
- let val thy = Thm.theory_of_thm th
- in Display.pretty_thm_aux (Syntax.pp_global thy) true false [] th end;
-
fun pretty_thm ctxt th =
let val asms = map Thm.term_of (Assumption.all_assms_of ctxt)
in Display.pretty_thm_aux (Syntax.pp ctxt) false true asms th end;
--- a/src/Pure/Isar/proof_display.ML Sun Mar 22 19:36:04 2009 +0100
+++ b/src/Pure/Isar/proof_display.ML Sun Mar 22 19:43:21 2009 +0100
@@ -6,12 +6,12 @@
signature PROOF_DISPLAY =
sig
- val pprint_context: Proof.context -> pprint_args -> unit
- val pprint_typ: theory -> typ -> pprint_args -> unit
- val pprint_term: theory -> term -> pprint_args -> unit
- val pprint_ctyp: ctyp -> pprint_args -> unit
- val pprint_cterm: cterm -> pprint_args -> unit
- val pprint_thm: thm -> pprint_args -> unit
+ val pp_context: Proof.context -> Pretty.T
+ val pp_thm: thm -> Pretty.T
+ val pp_typ: theory -> typ -> Pretty.T
+ val pp_term: theory -> term -> Pretty.T
+ val pp_ctyp: ctyp -> Pretty.T
+ val pp_cterm: cterm -> Pretty.T
val print_theorems_diff: theory -> theory -> unit
val print_theorems: theory -> unit
val pretty_full_theory: bool -> theory -> Pretty.T
@@ -26,18 +26,20 @@
(* toplevel pretty printing *)
-fun pprint_context ctxt = Pretty.pprint
+fun pp_context ctxt =
(if ! ProofContext.debug then
Pretty.quote (Pretty.big_list "proof context:" (ProofContext.pretty_context ctxt))
else Pretty.str "<context>");
-fun pprint pretty thy = Pretty.pprint o Pretty.quote o pretty (Syntax.init_pretty_global thy);
+fun pp_thm th =
+ let val thy = Thm.theory_of_thm th
+ in Display.pretty_thm_aux (Syntax.pp_global thy) true false [] th end;
-val pprint_typ = pprint Syntax.pretty_typ;
-val pprint_term = pprint Syntax.pretty_term;
-fun pprint_ctyp cT = pprint_typ (Thm.theory_of_ctyp cT) (Thm.typ_of cT);
-fun pprint_cterm ct = pprint_term (Thm.theory_of_cterm ct) (Thm.term_of ct);
-val pprint_thm = Pretty.pprint o ProofContext.pretty_thm_legacy;
+val pp_typ = Pretty.quote oo Syntax.pretty_typ_global;
+val pp_term = Pretty.quote oo Syntax.pretty_term_global;
+
+fun pp_ctyp cT = pp_typ (Thm.theory_of_ctyp cT) (Thm.typ_of cT);
+fun pp_cterm ct = pp_term (Thm.theory_of_cterm ct) (Thm.term_of ct);
(* theorems and theory *)
--- a/src/Pure/Isar/toplevel.ML Sun Mar 22 19:36:04 2009 +0100
+++ b/src/Pure/Isar/toplevel.ML Sun Mar 22 19:43:21 2009 +0100
@@ -311,7 +311,7 @@
fun controlled_execution f =
f
|> debugging
- |> interruptible;
+ |> Future.interruptible_task;
fun program f =
(f
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/ML-Systems/install_pp_polyml-experimental.ML Sun Mar 22 19:43:21 2009 +0100
@@ -0,0 +1,27 @@
+(* Title: Pure/ML-Systems/install_pp_polyml-experimental.ML
+
+Extra toplevel pretty-printing for Poly/ML; experimental version for
+Poly/ML 5.3.
+*)
+
+local
+
+fun pretty_future depth (pretty: 'a * int -> pretty) (x: 'a future) =
+ (case Future.peek x of
+ NONE => PrettyString "<future>"
+ | SOME (Exn.Exn _) => PrettyString "<failed>"
+ | SOME (Exn.Result y) => pretty (y, depth));
+
+fun pretty_lazy depth (pretty: 'a * int -> pretty) (x: 'a lazy) =
+ (case Lazy.peek x of
+ NONE => PrettyString "<lazy>"
+ | SOME (Exn.Exn _) => PrettyString "<failed>"
+ | SOME (Exn.Result y) => pretty (y, depth));
+
+in
+
+val _ = addPrettyPrinter pretty_future;
+val _ = addPrettyPrinter pretty_lazy;
+
+end;
+
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/ML-Systems/ml_pretty.ML Sun Mar 22 19:43:21 2009 +0100
@@ -0,0 +1,16 @@
+(* Title: Pure/ML-Systems/ml_pretty.ML
+ Author: Makarius
+
+Raw datatype for ML pretty printing.
+*)
+
+structure ML_Pretty =
+struct
+
+datatype pretty =
+ Block of (string * string) * pretty list * int |
+ String of string * int |
+ Break of bool * int;
+
+end;
+
--- a/src/Pure/ML-Systems/mosml.ML Sun Mar 22 19:36:04 2009 +0100
+++ b/src/Pure/ML-Systems/mosml.ML Sun Mar 22 19:43:21 2009 +0100
@@ -45,6 +45,7 @@
use "ML-Systems/multithreading.ML";
use "ML-Systems/time_limit.ML";
use "ML-Systems/ml_name_space.ML";
+use "ML-Systems/ml_pretty.ML";
(*low-level pointer equality*)
@@ -118,10 +119,8 @@
Meta.printLength := n);
end;
-(*interface for toplevel pretty printers, see also Pure/pure_setup.ML*)
-(*the documentation refers to an installPP but I couldn't fine it!*)
-fun make_pp path pprint = ();
-fun install_pp _ = ();
+(*dummy implementation*)
+fun toplevel_pp _ _ _ _ _ = ();
(*dummy implementation*)
fun ml_prompts p1 p2 = ();
--- a/src/Pure/ML-Systems/polyml-4.1.3.ML Sun Mar 22 19:36:04 2009 +0100
+++ b/src/Pure/ML-Systems/polyml-4.1.3.ML Sun Mar 22 19:43:21 2009 +0100
@@ -8,6 +8,7 @@
use "ML-Systems/thread_dummy.ML";
use "ML-Systems/polyml_common.ML";
use "ML-Systems/polyml_old_compiler4.ML";
+use "ML-Systems/polyml_pp.ML";
val pointer_eq = Address.wordEq;
--- a/src/Pure/ML-Systems/polyml-4.1.4.ML Sun Mar 22 19:36:04 2009 +0100
+++ b/src/Pure/ML-Systems/polyml-4.1.4.ML Sun Mar 22 19:43:21 2009 +0100
@@ -8,6 +8,7 @@
use "ML-Systems/thread_dummy.ML";
use "ML-Systems/polyml_common.ML";
use "ML-Systems/polyml_old_compiler4.ML";
+use "ML-Systems/polyml_pp.ML";
val pointer_eq = Address.wordEq;
--- a/src/Pure/ML-Systems/polyml-4.2.0.ML Sun Mar 22 19:36:04 2009 +0100
+++ b/src/Pure/ML-Systems/polyml-4.2.0.ML Sun Mar 22 19:43:21 2009 +0100
@@ -7,6 +7,7 @@
use "ML-Systems/thread_dummy.ML";
use "ML-Systems/polyml_common.ML";
use "ML-Systems/polyml_old_compiler4.ML";
+use "ML-Systems/polyml_pp.ML";
val pointer_eq = Address.wordEq;
--- a/src/Pure/ML-Systems/polyml-5.0.ML Sun Mar 22 19:36:04 2009 +0100
+++ b/src/Pure/ML-Systems/polyml-5.0.ML Sun Mar 22 19:43:21 2009 +0100
@@ -7,6 +7,7 @@
use "ML-Systems/thread_dummy.ML";
use "ML-Systems/polyml_common.ML";
use "ML-Systems/polyml_old_compiler5.ML";
+use "ML-Systems/polyml_pp.ML";
val pointer_eq = PolyML.pointerEq;
--- a/src/Pure/ML-Systems/polyml-5.1.ML Sun Mar 22 19:36:04 2009 +0100
+++ b/src/Pure/ML-Systems/polyml-5.1.ML Sun Mar 22 19:43:21 2009 +0100
@@ -6,6 +6,7 @@
use "ML-Systems/thread_dummy.ML";
use "ML-Systems/polyml_common.ML";
use "ML-Systems/polyml_old_compiler5.ML";
+use "ML-Systems/polyml_pp.ML";
val pointer_eq = PolyML.pointerEq;
--- a/src/Pure/ML-Systems/polyml-experimental.ML Sun Mar 22 19:36:04 2009 +0100
+++ b/src/Pure/ML-Systems/polyml-experimental.ML Sun Mar 22 19:43:21 2009 +0100
@@ -12,13 +12,6 @@
fun share_common_data () = PolyML.shareCommonData PolyML.rootFunction;
-(* toplevel pretty printers *)
-
-(*dummy version*)
-fun make_pp path pprint = ();
-fun install_pp _ = ();
-
-
(* runtime compilation *)
structure ML_NameSpace =
@@ -75,3 +68,16 @@
in use_text tune str_of_pos name_space (1, name) output verbose txt end;
end;
+
+
+(* toplevel pretty printing *)
+
+fun ml_pretty (ML_Pretty.Block (_, prts, ind)) = PrettyBlock (ind, false, [], map ml_pretty prts)
+ | ml_pretty (ML_Pretty.String (s, _)) = PrettyString s
+ | ml_pretty (ML_Pretty.Break (false, wd)) = PrettyBreak (wd, 0)
+ | ml_pretty (ML_Pretty.Break (true, _)) = PrettyBreak (99999, 0);
+
+fun toplevel_pp tune str_of_pos output (_: string list) pp =
+ use_text tune str_of_pos ML_NameSpace.global (1, "pp") output false
+ ("addPrettyPrinter (fn _ => fn _ => ml_pretty o Pretty.to_ML o (" ^ pp ^ "))");
+
--- a/src/Pure/ML-Systems/polyml.ML Sun Mar 22 19:36:04 2009 +0100
+++ b/src/Pure/ML-Systems/polyml.ML Sun Mar 22 19:43:21 2009 +0100
@@ -68,3 +68,6 @@
in use_text tune str_of_pos name_space (1, name) output verbose txt end;
end;
+
+use "ML-Systems/polyml_pp.ML";
+
--- a/src/Pure/ML-Systems/polyml_common.ML Sun Mar 22 19:36:04 2009 +0100
+++ b/src/Pure/ML-Systems/polyml_common.ML Sun Mar 22 19:43:21 2009 +0100
@@ -10,6 +10,7 @@
use "ML-Systems/time_limit.ML";
use "ML-Systems/system_shell.ML";
use "ML-Systems/ml_name_space.ML";
+use "ML-Systems/ml_pretty.ML";
(** ML system and platform related **)
@@ -73,13 +74,8 @@
fun ml_prompts p1 p2 = (PolyML.Compiler.prompt1 := p1; PolyML.Compiler.prompt2 := p2);
-(* toplevel pretty printing (see also Pure/pure_setup.ML) *)
+(* print depth *)
-fun make_pp _ pprint (str, blk, brk, en) _ _ obj =
- pprint obj (str, fn ind => blk (ind, false), fn wd => brk (wd, 0),
- fn () => brk (99999, 0), en);
-
-(*print depth*)
local
val depth = ref 10;
in
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/ML-Systems/polyml_pp.ML Sun Mar 22 19:43:21 2009 +0100
@@ -0,0 +1,20 @@
+(* Title: Pure/ML-Systems/polyml_pp.ML
+
+Toplevel pretty printing for Poly/ML before 5.3.
+*)
+
+fun ml_pprint (print, begin_blk, brk, end_blk) =
+ let
+ fun str "" = ()
+ | str s = print s;
+ fun pprint (ML_Pretty.Block ((bg, en), prts, ind)) =
+ (str bg; begin_blk (ind, false); List.app pprint prts; end_blk (); str en)
+ | pprint (ML_Pretty.String (s, _)) = str s
+ | pprint (ML_Pretty.Break (false, wd)) = brk (wd, 0)
+ | pprint (ML_Pretty.Break (true, _)) = brk (99999, 0);
+ in pprint end;
+
+fun toplevel_pp tune str_of_pos output (_: string list) pp =
+ use_text tune str_of_pos ML_NameSpace.global (1, "pp") output false
+ ("install_pp (fn args => fn _ => fn _ => ml_pprint args o Pretty.to_ML o (" ^ pp ^ "))");
+
--- a/src/Pure/ML-Systems/smlnj.ML Sun Mar 22 19:36:04 2009 +0100
+++ b/src/Pure/ML-Systems/smlnj.ML Sun Mar 22 19:43:21 2009 +0100
@@ -13,6 +13,7 @@
use "ML-Systems/multithreading.ML";
use "ML-Systems/system_shell.ML";
use "ML-Systems/ml_name_space.ML";
+use "ML-Systems/ml_pretty.ML";
(*low-level pointer equality*)
@@ -97,22 +98,6 @@
fun makestring x = "dummy string for SML New Jersey";
-(* toplevel pretty printing (see also Pure/pure_setup.ML) *)
-
-fun make_pp path pprint =
- let
- open PrettyPrint;
-
- fun pp pps obj =
- pprint obj
- (string pps, openHOVBox pps o Rel o dest_int,
- fn wd => break pps {nsp=dest_int wd, offset=0}, fn () => newline pps,
- fn () => closeBox pps);
- in (path, pp) end;
-
-fun install_pp (path, pp) = CompilerPPTable.install_pp path pp;
-
-
(* ML command execution *)
fun use_text (tune: string -> string) _ _ (line: int, name) (print, err) verbose txt =
@@ -144,6 +129,26 @@
("structure " ^ name ^ " = struct end");
+(* toplevel pretty printing *)
+
+fun ml_pprint pps =
+ let
+ fun str "" = ()
+ | str s = PrettyPrint.string pps s;
+ fun pprint (ML_Pretty.Block ((bg, en), prts, ind)) =
+ (str bg; PrettyPrint.openHOVBox pps (PrettyPrint.Rel (dest_int ind));
+ List.app pprint prts; PrettyPrint.closeBox pps; str en)
+ | pprint (ML_Pretty.String (s, _)) = str s
+ | pprint (ML_Pretty.Break (false, wd)) = PrettyPrint.break pps {nsp = dest_int wd, offset = 0}
+ | pprint (ML_Pretty.Break (true, _)) = PrettyPrint.newline pps;
+ in pprint end;
+
+fun toplevel_pp tune str_of_pos output path pp =
+ use_text tune str_of_pos ML_NameSpace.global (1, "pp") output false
+ ("CompilerPPTable.install_pp [" ^ String.concatWith "," (map (fn s => "\"" ^ s ^ "\"") path) ^
+ "] (fn pps => ml_pprint pps o Pretty.to_ML o (" ^ pp ^ "))");
+
+
(** interrupts **)
--- a/src/Pure/Syntax/ast.ML Sun Mar 22 19:36:04 2009 +0100
+++ b/src/Pure/Syntax/ast.ML Sun Mar 22 19:43:21 2009 +0100
@@ -20,7 +20,6 @@
val str_of_ast: ast -> string
val pretty_ast: ast -> Pretty.T
val pretty_rule: ast * ast -> Pretty.T
- val pprint_ast: ast -> pprint_args -> unit
val fold_ast: string -> ast list -> ast
val fold_ast_p: string -> ast list * ast -> ast
val unfold_ast: string -> ast -> ast list
@@ -79,8 +78,6 @@
| pretty_ast (Appl asts) =
Pretty.enclose "(" ")" (Pretty.breaks (map pretty_ast asts));
-val pprint_ast = Pretty.pprint o pretty_ast;
-
fun pretty_rule (lhs, rhs) =
Pretty.block [pretty_ast lhs, Pretty.str " ->", Pretty.brk 2, pretty_ast rhs];
--- a/src/Pure/context.ML Sun Mar 22 19:36:04 2009 +0100
+++ b/src/Pure/context.ML Sun Mar 22 19:43:21 2009 +0100
@@ -27,8 +27,6 @@
val display_names: theory -> string list
val pretty_thy: theory -> Pretty.T
val string_of_thy: theory -> string
- val pprint_thy: theory -> pprint_args -> unit
- val pprint_thy_ref: theory_ref -> pprint_args -> unit
val pretty_abbrev_thy: theory -> Pretty.T
val str_of_thy: theory -> string
val deref: theory_ref -> theory
@@ -228,7 +226,6 @@
val pretty_thy = Pretty.str_list "{" "}" o display_names;
val string_of_thy = Pretty.string_of o pretty_thy;
-val pprint_thy = Pretty.pprint o pretty_thy;
fun pretty_abbrev_thy thy =
let
@@ -256,8 +253,6 @@
else thy_ref
end;
-val pprint_thy_ref = Pretty.pprint o pretty_thy o deref;
-
(* build ids *)
--- a/src/Pure/pure_setup.ML Sun Mar 22 19:36:04 2009 +0100
+++ b/src/Pure/pure_setup.ML Sun Mar 22 19:43:21 2009 +0100
@@ -27,23 +27,25 @@
(* ML toplevel pretty printing *)
-install_pp (make_pp ["Task_Queue", "task"] (Pretty.pprint o Pretty.str o Task_Queue.str_of_task));
-install_pp (make_pp ["Task_Queue", "group"] (Pretty.pprint o Pretty.str o Task_Queue.str_of_group));
-install_pp (make_pp ["Position", "T"] (Pretty.pprint o Pretty.enum "," "{" "}" o
- map (fn (x, y) => Pretty.str (x ^ "=" ^ y)) o Position.properties_of));
-install_pp (make_pp ["Thm", "thm"] ProofDisplay.pprint_thm);
-install_pp (make_pp ["Thm", "cterm"] ProofDisplay.pprint_cterm);
-install_pp (make_pp ["Binding", "binding"] (Pretty.pprint o Pretty.str o quote o Binding.str_of));
-install_pp (make_pp ["Thm", "ctyp"] ProofDisplay.pprint_ctyp);
-install_pp (make_pp ["Context", "theory"] Context.pprint_thy);
-install_pp (make_pp ["Context", "theory_ref"] Context.pprint_thy_ref);
-install_pp (make_pp ["Context", "proof"] ProofDisplay.pprint_context);
-install_pp (make_pp ["Syntax", "ast"] Syntax.pprint_ast);
-install_pp (make_pp ["typ"] (ProofDisplay.pprint_typ Pure.thy));
-install_pp (make_pp ["Path", "T"] (Pretty.pprint o Pretty.str o quote o Path.implode));
-install_pp (make_pp ["File", "ident"] (Pretty.pprint o Pretty.str o quote o File.rep_ident));
+toplevel_pp ["Task_Queue", "task"] "Pretty.str o Task_Queue.str_of_task";
+toplevel_pp ["Task_Queue", "group"] "Pretty.str o Task_Queue.str_of_group";
+toplevel_pp ["Position", "T"] "Pretty.position";
+toplevel_pp ["Binding", "binding"] "Pretty.str o quote o Binding.str_of";
+toplevel_pp ["Thm", "thm"] "ProofDisplay.pp_thm";
+toplevel_pp ["Thm", "cterm"] "ProofDisplay.pp_cterm";
+toplevel_pp ["Thm", "ctyp"] "ProofDisplay.pp_ctyp";
+toplevel_pp ["typ"] "ProofDisplay.pp_typ Pure.thy";
+toplevel_pp ["Context", "theory"] "Context.pretty_thy";
+toplevel_pp ["Context", "theory_ref"] "Context.pretty_thy o Theory.deref";
+toplevel_pp ["Context", "proof"] "ProofDisplay.pp_context";
+toplevel_pp ["Syntax", "ast"] "Syntax.pretty_ast";
+toplevel_pp ["Path", "T"] "Pretty.str o quote o Path.implode";
+toplevel_pp ["File", "ident"] "Pretty.str o quote o File.rep_ident";
-if String.isPrefix "polyml" ml_system then use "ML-Systems/install_pp_polyml.ML"
+if File.exists (Path.explode ("ML-Systems/install_pp_" ^ ml_system ^ ".ML"))
+then use ("ML-Systems/install_pp_" ^ ml_system ^ ".ML")
+else if String.isPrefix "polyml" ml_system
+then use "ML-Systems/install_pp_polyml.ML"
else ();
--- a/src/Tools/code/code_haskell.ML Sun Mar 22 19:36:04 2009 +0100
+++ b/src/Tools/code/code_haskell.ML Sun Mar 22 19:43:21 2009 +0100
@@ -42,18 +42,18 @@
of [] => []
| classbinds => Pretty.enum "," "(" ")" (
map (fn (v, class) =>
- str (class_name class ^ " " ^ Code_Name.lookup_var tyvars v)) classbinds)
+ str (class_name class ^ " " ^ Code_Printer.lookup_var tyvars v)) classbinds)
@@ str " => ";
fun pr_typforall tyvars vs = case map fst vs
of [] => []
| vnames => str "forall " :: Pretty.breaks
- (map (str o Code_Name.lookup_var tyvars) vnames) @ str "." @@ Pretty.brk 1;
+ (map (str o Code_Printer.lookup_var tyvars) vnames) @ str "." @@ Pretty.brk 1;
fun pr_tycoexpr tyvars fxy (tyco, tys) =
brackify fxy (str tyco :: map (pr_typ tyvars BR) tys)
and pr_typ tyvars fxy (tycoexpr as tyco `%% tys) = (case syntax_tyco tyco
of NONE => pr_tycoexpr tyvars fxy (deresolve tyco, tys)
| SOME (i, pr) => pr (pr_typ tyvars) fxy tys)
- | pr_typ tyvars fxy (ITyVar v) = (str o Code_Name.lookup_var tyvars) v;
+ | pr_typ tyvars fxy (ITyVar v) = (str o Code_Printer.lookup_var tyvars) v;
fun pr_typdecl tyvars (vs, tycoexpr) =
Pretty.block (pr_typcontext tyvars vs @| pr_tycoexpr tyvars NOBR tycoexpr);
fun pr_typscheme tyvars (vs, ty) =
@@ -69,7 +69,7 @@
pr_term tyvars thm vars BR t2
])
| pr_term tyvars thm vars fxy (IVar v) =
- (str o Code_Name.lookup_var vars) v
+ (str o Code_Printer.lookup_var vars) v
| pr_term tyvars thm vars fxy (t as _ `|-> _) =
let
val (binds, t') = Code_Thingol.unfold_abs t;
@@ -127,7 +127,7 @@
| pr_case tyvars thm vars fxy ((_, []), _) = str "error \"empty case\"";
fun pr_stmt (name, Code_Thingol.Fun (_, ((vs, ty), []))) =
let
- val tyvars = Code_Name.intro_vars (map fst vs) init_syms;
+ val tyvars = Code_Printer.intro_vars (map fst vs) init_syms;
val n = (length o fst o Code_Thingol.unfold_fun) ty;
in
Pretty.chunks [
@@ -150,7 +150,7 @@
| pr_stmt (name, Code_Thingol.Fun (_, ((vs, ty), raw_eqs))) =
let
val eqs = filter (snd o snd) raw_eqs;
- val tyvars = Code_Name.intro_vars (map fst vs) init_syms;
+ val tyvars = Code_Printer.intro_vars (map fst vs) init_syms;
fun pr_eq ((ts, t), (thm, _)) =
let
val consts = map_filter
@@ -158,8 +158,8 @@
then NONE else (SOME o Long_Name.base_name o deresolve) c)
((fold o Code_Thingol.fold_constnames) (insert (op =)) (t :: ts) []);
val vars = init_syms
- |> Code_Name.intro_vars consts
- |> Code_Name.intro_vars ((fold o Code_Thingol.fold_unbound_varnames)
+ |> Code_Printer.intro_vars consts
+ |> Code_Printer.intro_vars ((fold o Code_Thingol.fold_unbound_varnames)
(insert (op =)) ts []);
in
semicolon (
@@ -182,7 +182,7 @@
end
| pr_stmt (name, Code_Thingol.Datatype (_, (vs, []))) =
let
- val tyvars = Code_Name.intro_vars (map fst vs) init_syms;
+ val tyvars = Code_Printer.intro_vars (map fst vs) init_syms;
in
semicolon [
str "data",
@@ -191,7 +191,7 @@
end
| pr_stmt (name, Code_Thingol.Datatype (_, (vs, [(co, [ty])]))) =
let
- val tyvars = Code_Name.intro_vars (map fst vs) init_syms;
+ val tyvars = Code_Printer.intro_vars (map fst vs) init_syms;
in
semicolon (
str "newtype"
@@ -204,7 +204,7 @@
end
| pr_stmt (name, Code_Thingol.Datatype (_, (vs, co :: cos))) =
let
- val tyvars = Code_Name.intro_vars (map fst vs) init_syms;
+ val tyvars = Code_Printer.intro_vars (map fst vs) init_syms;
fun pr_co (co, tys) =
concat (
(str o deresolve_base) co
@@ -222,7 +222,7 @@
end
| pr_stmt (name, Code_Thingol.Class (_, (v, (superclasses, classparams)))) =
let
- val tyvars = Code_Name.intro_vars [v] init_syms;
+ val tyvars = Code_Printer.intro_vars [v] init_syms;
fun pr_classparam (classparam, ty) =
semicolon [
(str o deresolve_base) classparam,
@@ -234,7 +234,7 @@
Pretty.block [
str "class ",
Pretty.block (pr_typcontext tyvars [(v, map fst superclasses)]),
- str (deresolve_base name ^ " " ^ Code_Name.lookup_var tyvars v),
+ str (deresolve_base name ^ " " ^ Code_Printer.lookup_var tyvars v),
str " where {"
],
str "};"
@@ -244,7 +244,7 @@
let
val split_abs_pure = (fn (v, _) `|-> t => SOME (v, t) | _ => NONE);
val unfold_abs_pure = Code_Thingol.unfoldr split_abs_pure;
- val tyvars = Code_Name.intro_vars (map fst vs) init_syms;
+ val tyvars = Code_Printer.intro_vars (map fst vs) init_syms;
fun pr_instdef ((classparam, c_inst), (thm, _)) = case syntax_const classparam
of NONE => semicolon [
(str o deresolve_base) classparam,
@@ -259,8 +259,8 @@
val proto_rhs = Code_Thingol.eta_expand k (c_inst, []);
val (vs, rhs) = unfold_abs_pure proto_rhs;
val vars = init_syms
- |> Code_Name.intro_vars (the_list const)
- |> Code_Name.intro_vars vs;
+ |> Code_Printer.intro_vars (the_list const)
+ |> Code_Printer.intro_vars vs;
val lhs = IConst (classparam, ([], tys)) `$$ map IVar vs;
(*dictionaries are not relevant at this late stage*)
in
@@ -288,20 +288,20 @@
let
val module_alias = if is_some module_name then K module_name else raw_module_alias;
val reserved_names = Name.make_context reserved_names;
- val mk_name_module = Code_Name.mk_name_module reserved_names module_prefix module_alias program;
+ val mk_name_module = Code_Printer.mk_name_module reserved_names module_prefix module_alias program;
fun add_stmt (name, (stmt, deps)) =
let
- val (module_name, base) = Code_Name.dest_name name;
+ val (module_name, base) = Code_Printer.dest_name name;
val module_name' = mk_name_module module_name;
val mk_name_stmt = yield_singleton Name.variants;
fun add_fun upper (nsp_fun, nsp_typ) =
let
val (base', nsp_fun') =
- mk_name_stmt (if upper then Code_Name.first_upper base else base) nsp_fun
+ mk_name_stmt (if upper then Code_Printer.first_upper base else base) nsp_fun
in (base', (nsp_fun', nsp_typ)) end;
fun add_typ (nsp_fun, nsp_typ) =
let
- val (base', nsp_typ') = mk_name_stmt (Code_Name.first_upper base) nsp_typ
+ val (base', nsp_typ') = mk_name_stmt (Code_Printer.first_upper base) nsp_typ
in (base', (nsp_fun, nsp_typ')) end;
val add_name = case stmt
of Code_Thingol.Fun _ => add_fun false
@@ -330,7 +330,7 @@
(Graph.get_node program name, Graph.imm_succs program name))
(Graph.strong_conn program |> flat)) Symtab.empty;
fun deresolver name = (fst o the o AList.lookup (op =) ((fst o snd o the
- o Symtab.lookup hs_program) ((mk_name_module o fst o Code_Name.dest_name) name))) name
+ o Symtab.lookup hs_program) ((mk_name_module o fst o Code_Printer.dest_name) name))) name
handle Option => error ("Unknown statement name: " ^ labelled_name name);
in (deresolver, hs_program) end;
@@ -357,7 +357,7 @@
andalso forall (deriv' tycos) tys
| deriv' _ (ITyVar _) = true
in deriv [] tyco end;
- val reserved_names = Code_Name.make_vars reserved_names;
+ val reserved_names = Code_Printer.make_vars reserved_names;
fun pr_stmt qualified = pr_haskell_stmt naming labelled_name
syntax_class syntax_tyco syntax_const reserved_names
(if qualified then deresolver else Long_Name.base_name o deresolver)
--- a/src/Tools/code/code_ml.ML Sun Mar 22 19:36:04 2009 +0100
+++ b/src/Tools/code/code_ml.ML Sun Mar 22 19:43:21 2009 +0100
@@ -50,8 +50,8 @@
val pr_label_classparam = Long_Name.base_name o Long_Name.qualifier;
fun pr_dicts fxy ds =
let
- fun pr_dictvar (v, (_, 1)) = Code_Name.first_upper v ^ "_"
- | pr_dictvar (v, (i, _)) = Code_Name.first_upper v ^ string_of_int (i+1) ^ "_";
+ fun pr_dictvar (v, (_, 1)) = Code_Printer.first_upper v ^ "_"
+ | pr_dictvar (v, (i, _)) = Code_Printer.first_upper v ^ string_of_int (i+1) ^ "_";
fun pr_proj [] p =
p
| pr_proj [p'] p =
@@ -87,7 +87,7 @@
fun pr_term is_closure thm vars fxy (IConst c) =
pr_app is_closure thm vars fxy (c, [])
| pr_term is_closure thm vars fxy (IVar v) =
- str (Code_Name.lookup_var vars v)
+ str (Code_Printer.lookup_var vars v)
| pr_term is_closure thm vars fxy (t as t1 `$ t2) =
(case Code_Thingol.unfold_const_app t
of SOME c_ts => pr_app is_closure thm vars fxy c_ts
@@ -182,7 +182,7 @@
then NONE else (SOME o Long_Name.base_name o deresolve) c)
(Code_Thingol.fold_constnames (insert (op =)) t []);
val vars = reserved_names
- |> Code_Name.intro_vars consts;
+ |> Code_Printer.intro_vars consts;
in
concat [
str "val",
@@ -207,8 +207,8 @@
then NONE else (SOME o Long_Name.base_name o deresolve) c)
((fold o Code_Thingol.fold_constnames) (insert (op =)) (t :: ts) []);
val vars = reserved_names
- |> Code_Name.intro_vars consts
- |> Code_Name.intro_vars ((fold o Code_Thingol.fold_unbound_varnames)
+ |> Code_Printer.intro_vars consts
+ |> Code_Printer.intro_vars ((fold o Code_Thingol.fold_unbound_varnames)
(insert (op =)) ts []);
in
concat (
@@ -266,7 +266,7 @@
in Pretty.chunks (ps @| Pretty.block ([p, str ";"])) end
| pr_stmt (MLClass (class, (v, (superclasses, classparams)))) =
let
- val w = Code_Name.first_upper v ^ "_";
+ val w = Code_Printer.first_upper v ^ "_";
fun pr_superclass_field (class, classrel) =
(concat o map str) [
pr_label_classrel classrel, ":", "'" ^ v, deresolve class
@@ -362,8 +362,8 @@
let
fun pr_dicts fxy ds =
let
- fun pr_dictvar (v, (_, 1)) = "_" ^ Code_Name.first_upper v
- | pr_dictvar (v, (i, _)) = "_" ^ Code_Name.first_upper v ^ string_of_int (i+1);
+ fun pr_dictvar (v, (_, 1)) = "_" ^ Code_Printer.first_upper v
+ | pr_dictvar (v, (i, _)) = "_" ^ Code_Printer.first_upper v ^ string_of_int (i+1);
fun pr_proj ps p =
fold_rev (fn p2 => fn p1 => Pretty.block [p1, str ".", str p2]) ps p
fun pr_dict fxy (DictConst (inst, dss)) =
@@ -395,7 +395,7 @@
fun pr_term is_closure thm vars fxy (IConst c) =
pr_app is_closure thm vars fxy (c, [])
| pr_term is_closure thm vars fxy (IVar v) =
- str (Code_Name.lookup_var vars v)
+ str (Code_Printer.lookup_var vars v)
| pr_term is_closure thm vars fxy (t as t1 `$ t2) =
(case Code_Thingol.unfold_const_app t
of SOME c_ts => pr_app is_closure thm vars fxy c_ts
@@ -468,8 +468,8 @@
val x = Name.variant (map_filter I fished1) "x";
val fished2 = map_index (fillup_param x) fished1;
val (fished3, _) = Name.variants fished2 Name.context;
- val vars' = Code_Name.intro_vars fished3 vars;
- in map (Code_Name.lookup_var vars') fished3 end;
+ val vars' = Code_Printer.intro_vars fished3 vars;
+ in map (Code_Printer.lookup_var vars') fished3 end;
fun pr_stmt (MLExc (name, n)) =
let
val exc_str =
@@ -491,7 +491,7 @@
then NONE else (SOME o Long_Name.base_name o deresolve) c)
(Code_Thingol.fold_constnames (insert (op =)) t []);
val vars = reserved_names
- |> Code_Name.intro_vars consts;
+ |> Code_Printer.intro_vars consts;
in
concat [
str "let",
@@ -511,8 +511,8 @@
then NONE else (SOME o Long_Name.base_name o deresolve) c)
((fold o Code_Thingol.fold_constnames) (insert (op =)) (t :: ts) []);
val vars = reserved_names
- |> Code_Name.intro_vars consts
- |> Code_Name.intro_vars ((fold o Code_Thingol.fold_unbound_varnames)
+ |> Code_Printer.intro_vars consts
+ |> Code_Printer.intro_vars ((fold o Code_Thingol.fold_unbound_varnames)
(insert (op =)) ts []);
in concat [
(Pretty.block o Pretty.commas)
@@ -527,8 +527,8 @@
then NONE else (SOME o Long_Name.base_name o deresolve) c)
((fold o Code_Thingol.fold_constnames) (insert (op =)) (t :: ts) []);
val vars = reserved_names
- |> Code_Name.intro_vars consts
- |> Code_Name.intro_vars ((fold o Code_Thingol.fold_unbound_varnames)
+ |> Code_Printer.intro_vars consts
+ |> Code_Printer.intro_vars ((fold o Code_Thingol.fold_unbound_varnames)
(insert (op =)) ts []);
in
concat (
@@ -556,7 +556,7 @@
((fold o Code_Thingol.fold_constnames)
(insert (op =)) (map (snd o fst) eqs) []);
val vars = reserved_names
- |> Code_Name.intro_vars consts;
+ |> Code_Printer.intro_vars consts;
val dummy_parms = (map str o fish_params vars o map (fst o fst)) eqs;
in
Pretty.block (
@@ -623,7 +623,7 @@
in Pretty.chunks (ps @| Pretty.block ([p, str ";;"])) end
| pr_stmt (MLClass (class, (v, (superclasses, classparams)))) =
let
- val w = "_" ^ Code_Name.first_upper v;
+ val w = "_" ^ Code_Printer.first_upper v;
fun pr_superclass_field (class, classrel) =
(concat o map str) [
deresolve classrel, ":", "'" ^ v, deresolve class
@@ -765,11 +765,11 @@
let
val (x, nsp_typ') = f nsp_typ
in (x, (nsp_fun, nsp_typ')) end;
- val mk_name_module = Code_Name.mk_name_module reserved_names NONE module_alias program;
+ val mk_name_module = Code_Printer.mk_name_module reserved_names NONE module_alias program;
fun mk_name_stmt upper name nsp =
let
- val (_, base) = Code_Name.dest_name name;
- val base' = if upper then Code_Name.first_upper base else base;
+ val (_, base) = Code_Printer.dest_name name;
+ val base' = if upper then Code_Printer.first_upper base else base;
val ([base''], nsp') = Name.variants [base'] nsp;
in (base'', nsp') end;
fun rearrange_fun name (tysm as (vs, ty), raw_eqs) =
@@ -853,7 +853,7 @@
[]
|> fold (fold (insert (op =)) o Graph.imm_succs program) names
|> subtract (op =) names;
- val (module_names, _) = (split_list o map Code_Name.dest_name) names;
+ val (module_names, _) = (split_list o map Code_Printer.dest_name) names;
val module_name = (the_single o distinct (op =) o map mk_name_module) module_names
handle Empty =>
error ("Different namespace prefixes for mutual dependencies:\n"
@@ -863,7 +863,7 @@
val module_name_path = Long_Name.explode module_name;
fun add_dep name name' =
let
- val module_name' = (mk_name_module o fst o Code_Name.dest_name) name';
+ val module_name' = (mk_name_module o fst o Code_Printer.dest_name) name';
in if module_name = module_name' then
map_node module_name_path (Graph.add_edge (name, name'))
else let
@@ -891,7 +891,7 @@
(rev (Graph.strong_conn program)));
fun deresolver prefix name =
let
- val module_name = (fst o Code_Name.dest_name) name;
+ val module_name = (fst o Code_Printer.dest_name) name;
val module_name' = (Long_Name.explode o mk_name_module) module_name;
val (_, (_, remainder)) = chop_prefix (op =) (prefix, module_name');
val stmt_name =
@@ -914,7 +914,7 @@
val module_name = if null stmt_names then raw_module_name else SOME "Code";
val (deresolver, nodes) = ml_node_of_program labelled_name module_name
reserved_names raw_module_alias program;
- val reserved_names = Code_Name.make_vars reserved_names;
+ val reserved_names = Code_Printer.make_vars reserved_names;
fun pr_node prefix (Dummy _) =
NONE
| pr_node prefix (Stmt (_, stmt)) = if null stmt_names orelse
--- a/src/Tools/code/code_name.ML Sun Mar 22 19:36:04 2009 +0100
+++ b/src/Tools/code/code_name.ML Sun Mar 22 19:43:21 2009 +0100
@@ -6,45 +6,20 @@
signature CODE_NAME =
sig
- structure StringPairTab: TABLE
- val first_upper: string -> string
- val first_lower: string -> string
- val dest_name: string -> string * string
-
val purify_var: string -> string
val purify_tvar: string -> string
- val purify_sym: string -> string
- val purify_base: bool -> string -> string
+ val purify_base: string -> string
val check_modulename: string -> string
- type var_ctxt
- val make_vars: string list -> var_ctxt
- val intro_vars: string list -> var_ctxt -> var_ctxt
- val lookup_var: var_ctxt -> string -> string
-
val read_const_exprs: theory -> string list -> string list * string list
- val mk_name_module: Name.context -> string option -> (string -> string option)
- -> 'a Graph.T -> string -> string
end;
structure Code_Name: CODE_NAME =
struct
-(** auxiliary **)
-
-structure StringPairTab =
- TableFun(type key = string * string val ord = prod_ord fast_string_ord fast_string_ord);
-
-val first_upper = implode o nth_map 0 Symbol.to_ascii_upper o explode;
-val first_lower = implode o nth_map 0 Symbol.to_ascii_lower o explode;
-
-val dest_name =
- apfst Long_Name.implode o split_last o fst o split_last o Long_Name.explode;
-
-
(** purification **)
-fun purify_name upper lower =
+fun purify_name upper =
let
fun is_valid s = Symbol.is_ascii_letter s orelse Symbol.is_ascii_digit s orelse s = "'";
val is_junk = not o is_valid andf Symbol.is_regular;
@@ -55,9 +30,8 @@
--| junk))
::: Scan.repeat ((Scan.many1 is_valid >> implode) --| junk));
fun upper_lower cs = if upper then nth_map 0 Symbol.to_ascii_upper cs
- else if lower then (if forall Symbol.is_ascii_upper cs
- then map else nth_map 0) Symbol.to_ascii_lower cs
- else cs;
+ else (if forall Symbol.is_ascii_upper cs
+ then map else nth_map 0) Symbol.to_ascii_lower cs;
in
explode
#> scan_valids
@@ -68,7 +42,7 @@
end;
fun purify_var "" = "x"
- | purify_var v = purify_name false true v;
+ | purify_var v = purify_name false v;
fun purify_tvar "" = "'a"
| purify_tvar v =
@@ -81,52 +55,29 @@
(Scan.repeat ($$ "_" |-- $$ "_" >> (fn _ => ".") || Scan.one Symbol.is_regular))
#> implode
#> Long_Name.explode
- #> map (purify_name true false);
+ #> map (purify_name true);
(*FIMXE non-canonical function treating non-canonical names*)
-fun purify_base _ "op &" = "and"
- | purify_base _ "op |" = "or"
- | purify_base _ "op -->" = "implies"
- | purify_base _ "{}" = "empty"
- | purify_base _ "op :" = "member"
- | purify_base _ "op Int" = "intersect"
- | purify_base _ "op Un" = "union"
- | purify_base _ "*" = "product"
- | purify_base _ "+" = "sum"
- | purify_base lower s = if String.isPrefix "op =" s
- then "eq" ^ purify_name false lower s
- else purify_name false lower s;
-
-val purify_sym = purify_base false;
+fun purify_base "op &" = "and"
+ | purify_base "op |" = "or"
+ | purify_base "op -->" = "implies"
+ | purify_base "op :" = "member"
+ | purify_base "*" = "product"
+ | purify_base "+" = "sum"
+ | purify_base s = if String.isPrefix "op =" s
+ then "eq" ^ purify_name false s
+ else purify_name false s;
fun check_modulename mn =
let
val mns = Long_Name.explode mn;
- val mns' = map (purify_name true false) mns;
+ val mns' = map (purify_name true) mns;
in
if mns' = mns then mn else error ("Invalid module name: " ^ quote mn ^ "\n"
^ "perhaps try " ^ quote (Long_Name.implode mns'))
end;
-(** variable name contexts **)
-
-type var_ctxt = string Symtab.table * Name.context;
-
-fun make_vars names = (fold (fn name => Symtab.update_new (name, name)) names Symtab.empty,
- Name.make_context names);
-
-fun intro_vars names (namemap, namectxt) =
- let
- val (names', namectxt') = Name.variants names namectxt;
- val namemap' = fold2 (curry Symtab.update) names names' namemap;
- in (namemap', namectxt') end;
-
-fun lookup_var (namemap, _) name = case Symtab.lookup namemap name
- of SOME name' => name'
- | NONE => error ("Invalid name in context: " ^ quote name);
-
-
(** misc **)
fun read_const_exprs thy =
@@ -150,22 +101,4 @@
else ([Code_Unit.read_const thy s], []);
in pairself flat o split_list o map read_const_expr end;
-fun mk_name_module reserved_names module_prefix module_alias program =
- let
- fun mk_alias name = case module_alias name
- of SOME name' => name'
- | NONE => name
- |> Long_Name.explode
- |> map (fn name => (the_single o fst) (Name.variants [name] reserved_names))
- |> Long_Name.implode;
- fun mk_prefix name = case module_prefix
- of SOME module_prefix => Long_Name.append module_prefix name
- | NONE => name;
- val tab =
- Symtab.empty
- |> Graph.fold ((fn name => Symtab.default (name, (mk_alias #> mk_prefix) name))
- o fst o dest_name o fst)
- program
- in the o Symtab.lookup tab end;
-
end;
--- a/src/Tools/code/code_printer.ML Sun Mar 22 19:36:04 2009 +0100
+++ b/src/Tools/code/code_printer.ML Sun Mar 22 19:43:21 2009 +0100
@@ -16,6 +16,13 @@
val semicolon: Pretty.T list -> Pretty.T
val enum_default: string -> string -> string -> string -> Pretty.T list -> Pretty.T
+ val first_upper: string -> string
+ val first_lower: string -> string
+ type var_ctxt
+ val make_vars: string list -> var_ctxt
+ val intro_vars: string list -> var_ctxt -> var_ctxt
+ val lookup_var: var_ctxt -> string -> string
+
type lrx
val L: lrx
val R: lrx
@@ -42,14 +49,14 @@
-> fixity -> 'a list -> Pretty.T)) option * OuterParse.token list
val simple_const_syntax: (int * ((fixity -> iterm -> Pretty.T)
-> fixity -> (iterm * itype) list -> Pretty.T)) option -> const_syntax option
- val gen_pr_app: (thm -> Code_Name.var_ctxt -> const * iterm list -> Pretty.T list)
- -> (thm -> Code_Name.var_ctxt -> fixity -> iterm -> Pretty.T)
+ val gen_pr_app: (thm -> var_ctxt -> const * iterm list -> Pretty.T list)
+ -> (thm -> var_ctxt -> fixity -> iterm -> Pretty.T)
-> (string -> const_syntax option) -> Code_Thingol.naming
- -> thm -> Code_Name.var_ctxt -> fixity -> const * iterm list -> Pretty.T
+ -> thm -> var_ctxt -> fixity -> const * iterm list -> Pretty.T
val gen_pr_bind: ((string option * Pretty.T option) * itype -> Pretty.T)
- -> (thm -> Code_Name.var_ctxt -> fixity -> iterm -> Pretty.T)
+ -> (thm -> var_ctxt -> fixity -> iterm -> Pretty.T)
-> thm -> fixity
- -> (string option * iterm option) * itype -> Code_Name.var_ctxt -> Pretty.T * Code_Name.var_ctxt
+ -> (string option * iterm option) * itype -> var_ctxt -> Pretty.T * var_ctxt
type literals
val Literals: { literal_char: string -> string, literal_string: string -> string,
@@ -60,6 +67,10 @@
val literal_numeral: literals -> bool -> int -> string
val literal_list: literals -> Pretty.T list -> Pretty.T
val infix_cons: literals -> int * string
+
+ val mk_name_module: Name.context -> string option -> (string -> string option)
+ -> 'a Graph.T -> string -> string
+ val dest_name: string -> string * string
end;
structure Code_Printer : CODE_PRINTER =
@@ -83,6 +94,27 @@
| enum_default default sep opn cls xs = Pretty.enum sep opn cls xs;
+(** names and variable name contexts **)
+
+type var_ctxt = string Symtab.table * Name.context;
+
+fun make_vars names = (fold (fn name => Symtab.update_new (name, name)) names Symtab.empty,
+ Name.make_context names);
+
+fun intro_vars names (namemap, namectxt) =
+ let
+ val (names', namectxt') = Name.variants names namectxt;
+ val namemap' = fold2 (curry Symtab.update) names names' namemap;
+ in (namemap', namectxt') end;
+
+fun lookup_var (namemap, _) name = case Symtab.lookup namemap name
+ of SOME name' => name'
+ | NONE => error ("Invalid name in context: " ^ quote name);
+
+val first_upper = implode o nth_map 0 Symbol.to_ascii_upper o explode;
+val first_lower = implode o nth_map 0 Symbol.to_ascii_lower o explode;
+
+
(** syntax printer **)
(* binding priorities *)
@@ -125,8 +157,8 @@
type tyco_syntax = int * ((fixity -> itype -> Pretty.T)
-> fixity -> itype list -> Pretty.T);
-type const_syntax = int * ((Code_Name.var_ctxt -> fixity -> iterm -> Pretty.T)
- -> Code_Thingol.naming -> thm -> Code_Name.var_ctxt -> fixity -> (iterm * itype) list -> Pretty.T);
+type const_syntax = int * ((var_ctxt -> fixity -> iterm -> Pretty.T)
+ -> Code_Thingol.naming -> thm -> var_ctxt -> fixity -> (iterm * itype) list -> Pretty.T);
fun simple_const_syntax x = (Option.map o apsnd)
(fn pretty => fn pr => fn naming => fn thm => fn vars => pretty (pr vars)) x;
@@ -150,9 +182,9 @@
val vs = case pat
of SOME pat => Code_Thingol.fold_varnames (insert (op =)) pat []
| NONE => [];
- val vars' = Code_Name.intro_vars (the_list v) vars;
- val vars'' = Code_Name.intro_vars vs vars';
- val v' = Option.map (Code_Name.lookup_var vars') v;
+ val vars' = intro_vars (the_list v) vars;
+ val vars'' = intro_vars vs vars';
+ val v' = Option.map (lookup_var vars') v;
val pat' = Option.map (pr_term thm vars'' fxy) pat;
in (pr_bind ((v', pat'), ty), vars'') end;
@@ -239,4 +271,28 @@
val literal_list = #literal_list o dest_Literals;
val infix_cons = #infix_cons o dest_Literals;
+
+(** module name spaces **)
+
+val dest_name =
+ apfst Long_Name.implode o split_last o fst o split_last o Long_Name.explode;
+
+fun mk_name_module reserved_names module_prefix module_alias program =
+ let
+ fun mk_alias name = case module_alias name
+ of SOME name' => name'
+ | NONE => name
+ |> Long_Name.explode
+ |> map (fn name => (the_single o fst) (Name.variants [name] reserved_names))
+ |> Long_Name.implode;
+ fun mk_prefix name = case module_prefix
+ of SOME module_prefix => Long_Name.append module_prefix name
+ | NONE => name;
+ val tab =
+ Symtab.empty
+ |> Graph.fold ((fn name => Symtab.default (name, (mk_alias #> mk_prefix) name))
+ o fst o dest_name o fst)
+ program
+ in the o Symtab.lookup tab end;
+
end; (*struct*)
--- a/src/Tools/code/code_target.ML Sun Mar 22 19:36:04 2009 +0100
+++ b/src/Tools/code/code_target.ML Sun Mar 22 19:43:21 2009 +0100
@@ -82,11 +82,9 @@
(** theory data **)
-structure StringPairTab = Code_Name.StringPairTab;
-
datatype name_syntax_table = NameSyntaxTable of {
class: string Symtab.table,
- instance: unit StringPairTab.table,
+ instance: unit Symreltab.table,
tyco: tyco_syntax Symtab.table,
const: const_syntax Symtab.table
};
@@ -99,7 +97,7 @@
NameSyntaxTable { class = class2, instance = instance2, tyco = tyco2, const = const2 }) =
mk_name_syntax_table (
(Symtab.join (K snd) (class1, class2),
- StringPairTab.join (K snd) (instance1, instance2)),
+ Symreltab.join (K snd) (instance1, instance2)),
(Symtab.join (K snd) (tyco1, tyco2),
Symtab.join (K snd) (const1, const2))
);
@@ -194,7 +192,7 @@
thy
|> (CodeTargetData.map o apfst oo Symtab.map_default)
(target, mk_target ((serial (), seri), (([], Symtab.empty),
- (mk_name_syntax_table ((Symtab.empty, StringPairTab.empty), (Symtab.empty, Symtab.empty)),
+ (mk_name_syntax_table ((Symtab.empty, Symreltab.empty), (Symtab.empty, Symtab.empty)),
Symtab.empty))))
((map_target o apfst o apsnd o K) seri)
end;
@@ -262,11 +260,11 @@
in if add_del then
thy
|> (map_name_syntax target o apfst o apsnd)
- (StringPairTab.update (inst, ()))
+ (Symreltab.update (inst, ()))
else
thy
|> (map_name_syntax target o apfst o apsnd)
- (StringPairTab.delete_safe inst)
+ (Symreltab.delete_safe inst)
end;
fun gen_add_syntax_tyco prep_tyco target raw_tyco raw_syn thy =
@@ -407,7 +405,7 @@
|>> map_filter I;
val (names_class, class') = distill_names Code_Thingol.lookup_class class;
val names_inst = map_filter (Code_Thingol.lookup_instance naming)
- (StringPairTab.keys instance);
+ (Symreltab.keys instance);
val (names_tyco, tyco') = distill_names Code_Thingol.lookup_tyco tyco;
val (names_const, const') = distill_names Code_Thingol.lookup_const const;
val names_hidden = names_class @ names_inst @ names_tyco @ names_const;
--- a/src/Tools/code/code_thingol.ML Sun Mar 22 19:36:04 2009 +0100
+++ b/src/Tools/code/code_thingol.ML Sun Mar 22 19:43:21 2009 +0100
@@ -242,7 +242,7 @@
fun namify thy get_basename get_thyname name =
let
val prefix = get_thyname thy name;
- val base = (Code_Name.purify_base true o get_basename) name;
+ val base = (Code_Name.purify_base o get_basename) name;
in Long_Name.append prefix base end;
in
@@ -261,13 +261,11 @@
(* data *)
-structure StringPairTab = Code_Name.StringPairTab;
-
datatype naming = Naming of {
class: class Symtab.table * Name.context,
- classrel: string StringPairTab.table * Name.context,
+ classrel: string Symreltab.table * Name.context,
tyco: string Symtab.table * Name.context,
- instance: string StringPairTab.table * Name.context,
+ instance: string Symreltab.table * Name.context,
const: string Symtab.table * Name.context
}
@@ -275,9 +273,9 @@
val empty_naming = Naming {
class = (Symtab.empty, Name.context),
- classrel = (StringPairTab.empty, Name.context),
+ classrel = (Symreltab.empty, Name.context),
tyco = (Symtab.empty, Name.context),
- instance = (StringPairTab.empty, Name.context),
+ instance = (Symreltab.empty, Name.context),
const = (Symtab.empty, Name.context)
};
@@ -334,22 +332,22 @@
val lookup_class = add_suffix suffix_class
oo Symtab.lookup o fst o #class o dest_Naming;
val lookup_classrel = add_suffix suffix_classrel
- oo StringPairTab.lookup o fst o #classrel o dest_Naming;
+ oo Symreltab.lookup o fst o #classrel o dest_Naming;
val lookup_tyco = add_suffix suffix_tyco
oo Symtab.lookup o fst o #tyco o dest_Naming;
val lookup_instance = add_suffix suffix_instance
- oo StringPairTab.lookup o fst o #instance o dest_Naming;
+ oo Symreltab.lookup o fst o #instance o dest_Naming;
val lookup_const = add_suffix suffix_const
oo Symtab.lookup o fst o #const o dest_Naming;
fun declare_class thy = declare thy map_class
lookup_class Symtab.update_new namify_class;
fun declare_classrel thy = declare thy map_classrel
- lookup_classrel StringPairTab.update_new namify_classrel;
+ lookup_classrel Symreltab.update_new namify_classrel;
fun declare_tyco thy = declare thy map_tyco
lookup_tyco Symtab.update_new namify_tyco;
fun declare_instance thy = declare thy map_instance
- lookup_instance StringPairTab.update_new namify_instance;
+ lookup_instance Symreltab.update_new namify_instance;
fun declare_const thy = declare thy map_const
lookup_const Symtab.update_new namify_const;