--- a/NEWS Fri Jul 23 21:29:29 2010 +0200
+++ b/NEWS Sun Jul 25 15:43:53 2010 +0200
@@ -14,6 +14,11 @@
consistent view on symbols, while raw explode (or String.explode)
merely give a byte-oriented representation.
+* Special treatment of ML file names has been discontinued.
+Historically, optional extensions .ML or .sml were added on demand --
+at the cost of clarity of file dependencies. Recall that Isabelle/ML
+files exclusively use the .ML extension. Minor INCOMPATIBILTY.
+
*** HOL ***
--- a/lib/html/isabelle.css Fri Jul 23 21:29:29 2010 +0200
+++ b/lib/html/isabelle.css Sun Jul 25 15:43:53 2010 +0200
@@ -5,8 +5,8 @@
.head { background-color: #FFFFFF; }
.source { background-color: #F0F0F0; padding: 10px; }
-.mlsource { background-color: #F0F0F0; padding: 10px; }
-.mlfooter { background-color: #FFFFFF; }
+.external_source { background-color: #F0F0F0; padding: 10px; }
+.external_footer { background-color: #FFFFFF; }
.theories { background-color: #F0F0F0; padding: 10px; }
.sessions { background-color: #F0F0F0; padding: 10px; }
@@ -14,9 +14,6 @@
.name { font-style: italic; }
.filename { font-family: fixed; }
-/* hide hr for this style */
-hr { height: 0px; border: 0px; }
-
/* basic syntax markup */
--- a/src/HOL/Boogie/Tools/boogie_commands.ML Fri Jul 23 21:29:29 2010 +0200
+++ b/src/HOL/Boogie/Tools/boogie_commands.ML Sun Jul 25 15:43:53 2010 +0200
@@ -268,7 +268,7 @@
val _ =
Outer_Syntax.command "boogie_open"
- "Open a new Boogie environment and load a Boogie-generated .b2i file."
+ "open a new Boogie environment and load a Boogie-generated .b2i file"
Keyword.thy_decl
(scan_opt "quiet" -- Parse.name -- vc_offsets >>
(Toplevel.theory o boogie_open))
@@ -296,7 +296,7 @@
val _ =
Outer_Syntax.command "boogie_vc"
- "Enter into proof mode for a specific verification condition."
+ "enter into proof mode for a specific verification condition"
Keyword.thy_goal
(vc_name -- vc_opts >> (fn args =>
(Toplevel.print o Toplevel.theory_to_proof (boogie_vc args))))
@@ -329,7 +329,7 @@
val _ =
Outer_Syntax.improper_command "boogie_status"
- "Show the name and state of all loaded verification conditions."
+ "show the name and state of all loaded verification conditions"
Keyword.diag
(status_test >> status_cmd ||
status_vc >> status_cmd ||
@@ -338,7 +338,7 @@
val _ =
Outer_Syntax.command "boogie_end"
- "Close the current Boogie environment."
+ "close the current Boogie environment"
Keyword.thy_decl
(Scan.succeed (Toplevel.theory boogie_end))
--- a/src/HOL/Code_Numeral.thy Fri Jul 23 21:29:29 2010 +0200
+++ b/src/HOL/Code_Numeral.thy Sun Jul 25 15:43:53 2010 +0200
@@ -123,7 +123,7 @@
by (rule HOL.eq_refl)
-subsection {* Indices as datatype of ints *}
+subsection {* Code numerals as datatype of ints *}
instantiation code_numeral :: number
begin
@@ -293,67 +293,74 @@
subsection {* Code generator setup *}
-text {* Implementation of indices by bounded integers *}
+text {* Implementation of code numerals by bounded integers *}
code_type code_numeral
(SML "int")
(OCaml "Big'_int.big'_int")
(Haskell "Integer")
- (Scala "Int")
+ (Scala "BigInt")
code_instance code_numeral :: eq
(Haskell -)
setup {*
- fold (Numeral.add_code @{const_name number_code_numeral_inst.number_of_code_numeral}
- false Code_Printer.literal_naive_numeral) ["SML", "Scala"]
+ Numeral.add_code @{const_name number_code_numeral_inst.number_of_code_numeral}
+ false Code_Printer.literal_naive_numeral "SML"
#> fold (Numeral.add_code @{const_name number_code_numeral_inst.number_of_code_numeral}
- false Code_Printer.literal_numeral) ["OCaml", "Haskell"]
+ false Code_Printer.literal_numeral) ["OCaml", "Haskell", "Scala"]
*}
code_reserved SML Int int
-code_reserved Scala Int
+code_reserved Eval Integer
code_const "op + \<Colon> code_numeral \<Rightarrow> code_numeral \<Rightarrow> code_numeral"
(SML "Int.+/ ((_),/ (_))")
(OCaml "Big'_int.add'_big'_int")
(Haskell infixl 6 "+")
(Scala infixl 7 "+")
+ (Eval infixl 8 "+")
code_const "subtract_code_numeral \<Colon> code_numeral \<Rightarrow> code_numeral \<Rightarrow> code_numeral"
(SML "Int.max/ (_/ -/ _,/ 0 : int)")
(OCaml "Big'_int.max'_big'_int/ (Big'_int.sub'_big'_int/ _/ _)/ Big'_int.zero'_big'_int")
(Haskell "max/ (_/ -/ _)/ (0 :: Integer)")
(Scala "!(_/ -/ _).max(0)")
+ (Eval "Integer.max/ (_/ -/ _)/ 0")
code_const "op * \<Colon> code_numeral \<Rightarrow> code_numeral \<Rightarrow> code_numeral"
(SML "Int.*/ ((_),/ (_))")
(OCaml "Big'_int.mult'_big'_int")
(Haskell infixl 7 "*")
(Scala infixl 8 "*")
+ (Eval infixl 8 "*")
code_const div_mod_code_numeral
- (SML "!(fn n => fn m =>/ if m = 0/ then (0, n) else/ (n div m, n mod m))")
+ (SML "!(fn n => fn m =>/ if m = 0/ then (0, n) else/ (Int.div (n, m), Int.mod (n, m)))")
(OCaml "Big'_int.quomod'_big'_int/ (Big'_int.abs'_big'_int _)/ (Big'_int.abs'_big'_int _)")
(Haskell "divMod")
- (Scala "!((n: Int) => (m: Int) =>/ if (m == 0)/ (0, n) else/ (n '/ m, n % m))")
+ (Scala "!((k: BigInt) => (l: BigInt) =>/ if (l == 0)/ (BigInt(0), k) else/ (k.abs '/% l.abs))")
+ (Eval "!(fn n => fn m =>/ if m = 0/ then (0, n) else/ (n div m, n mod m))")
code_const "eq_class.eq \<Colon> code_numeral \<Rightarrow> code_numeral \<Rightarrow> bool"
(SML "!((_ : Int.int) = _)")
(OCaml "Big'_int.eq'_big'_int")
(Haskell infixl 4 "==")
(Scala infixl 5 "==")
+ (Eval "!((_ : int) = _)")
code_const "op \<le> \<Colon> code_numeral \<Rightarrow> code_numeral \<Rightarrow> bool"
(SML "Int.<=/ ((_),/ (_))")
(OCaml "Big'_int.le'_big'_int")
(Haskell infix 4 "<=")
(Scala infixl 4 "<=")
+ (Eval infixl 6 "<=")
code_const "op < \<Colon> code_numeral \<Rightarrow> code_numeral \<Rightarrow> bool"
(SML "Int.</ ((_),/ (_))")
(OCaml "Big'_int.lt'_big'_int")
(Haskell infix 4 "<")
(Scala infixl 4 "<")
+ (Eval infixl 6 "<")
end
--- a/src/HOL/Imperative_HOL/Imperative_HOL_ex.thy Fri Jul 23 21:29:29 2010 +0200
+++ b/src/HOL/Imperative_HOL/Imperative_HOL_ex.thy Sun Jul 25 15:43:53 2010 +0200
@@ -14,6 +14,6 @@
Array.upd, Array.map_entry, Array.swap, Array.freeze,
ref, Ref.lookup, Ref.update, Ref.change)"
-export_code everything checking SML SML_imp OCaml? OCaml_imp? Haskell? Scala?
+export_code everything checking SML SML_imp OCaml? OCaml_imp? Haskell? (*Scala?*)
end
--- a/src/HOL/Imperative_HOL/ex/Imperative_Quicksort.thy Fri Jul 23 21:29:29 2010 +0200
+++ b/src/HOL/Imperative_HOL/ex/Imperative_Quicksort.thy Sun Jul 25 15:43:53 2010 +0200
@@ -655,6 +655,6 @@
ML {* @{code qsort} (Array.fromList [42, 2, 3, 5, 0, 1705, 8, 3, 15]) () *}
-export_code qsort checking SML SML_imp OCaml? OCaml_imp? Haskell? Scala?
+export_code qsort checking SML SML_imp OCaml? OCaml_imp? Haskell? (*Scala?*)
end
--- a/src/HOL/Imperative_HOL/ex/Imperative_Reverse.thy Fri Jul 23 21:29:29 2010 +0200
+++ b/src/HOL/Imperative_HOL/ex/Imperative_Reverse.thy Sun Jul 25 15:43:53 2010 +0200
@@ -110,6 +110,6 @@
subarray_def sublist'_all rev.simps[where j=0] elim!: crel_elims)
(drule sym[of "List.length (Array.get h a)"], simp)
-export_code rev checking SML SML_imp OCaml? OCaml_imp? Haskell? Scala?
+export_code rev checking SML SML_imp OCaml? OCaml_imp? Haskell? (*Scala?*)
end
--- a/src/HOL/Imperative_HOL/ex/Linked_Lists.thy Fri Jul 23 21:29:29 2010 +0200
+++ b/src/HOL/Imperative_HOL/ex/Linked_Lists.thy Sun Jul 25 15:43:53 2010 +0200
@@ -1014,6 +1014,6 @@
ML {* @{code test_2} () *}
ML {* @{code test_3} () *}
-export_code test_1 test_2 test_3 checking SML SML_imp OCaml? OCaml_imp? Haskell? Scala?
+export_code test_1 test_2 test_3 checking SML SML_imp OCaml? OCaml_imp? Haskell? (*Scala?*)
end
--- a/src/HOL/Library/Code_Integer.thy Fri Jul 23 21:29:29 2010 +0200
+++ b/src/HOL/Library/Code_Integer.thy Sun Jul 25 15:43:53 2010 +0200
@@ -14,6 +14,142 @@
operations for abstract integer operations.
*}
+text {*
+ Preliminary: alternative representation of @{typ code_numeral}
+ for @{text Haskell} and @{text Scala}.
+*}
+
+code_include Haskell "Natural" {*
+newtype Natural = Natural Integer deriving (Eq, Show, Read);
+
+instance Num Natural where {
+ fromInteger k = Natural (if k >= 0 then k else 0);
+ Natural n + Natural m = Natural (n + m);
+ Natural n - Natural m = fromInteger (n - m);
+ Natural n * Natural m = Natural (n * m);
+ abs n = n;
+ signum _ = 1;
+ negate n = error "negate Natural";
+};
+
+instance Ord Natural where {
+ Natural n <= Natural m = n <= m;
+ Natural n < Natural m = n < m;
+};
+
+instance Real Natural where {
+ toRational (Natural n) = toRational n;
+};
+
+instance Enum Natural where {
+ toEnum k = fromInteger (toEnum k);
+ fromEnum (Natural n) = fromEnum n;
+};
+
+instance Integral Natural where {
+ toInteger (Natural n) = n;
+ divMod n m = quotRem n m;
+ quotRem (Natural n) (Natural m)
+ | (m == 0) = (0, Natural n)
+ | otherwise = (Natural k, Natural l) where (k, l) = quotRem n m;
+};
+*}
+
+code_reserved Haskell Natural
+
+code_include Scala "Natural" {*
+import scala.Math
+
+object Natural {
+
+ 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 Natural private(private val value: BigInt) {
+
+ override def hashCode(): Int = this.value.hashCode()
+
+ override def equals(that: Any): Boolean = that match {
+ case that: Natural => this equals that
+ case _ => false
+ }
+
+ override def toString(): String = this.value.toString
+
+ 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 this.value.intValue
+
+ 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: Natural): (Natural, Natural) = if (that.value == 0) (new Natural(0), this)
+ else {
+ val (k, l) = this.value /% that.value
+ (new Natural(k), new Natural(l))
+ }
+
+ def <=(that: Natural): Boolean = this.value <= that.value
+
+ def <(that: Natural): Boolean = this.value < that.value
+
+}
+*}
+
+code_reserved Scala Natural
+
+code_type code_numeral
+ (Haskell "Natural.Natural")
+ (Scala "Natural")
+
+setup {*
+ fold (Numeral.add_code @{const_name number_code_numeral_inst.number_of_code_numeral}
+ false Code_Printer.literal_alternative_numeral) ["Haskell", "Scala"]
+*}
+
+code_instance code_numeral :: eq
+ (Haskell -)
+
+code_const "op + \<Colon> code_numeral \<Rightarrow> code_numeral \<Rightarrow> code_numeral"
+ (Haskell infixl 6 "+")
+ (Scala infixl 7 "+")
+
+code_const "op - \<Colon> code_numeral \<Rightarrow> code_numeral \<Rightarrow> code_numeral"
+ (Haskell infixl 6 "-")
+ (Scala infixl 7 "-")
+
+code_const "op * \<Colon> code_numeral \<Rightarrow> code_numeral \<Rightarrow> code_numeral"
+ (Haskell infixl 7 "*")
+ (Scala infixl 8 "*")
+
+code_const div_mod_code_numeral
+ (Haskell "divMod")
+ (Scala infixl 8 "/%")
+
+code_const "eq_class.eq \<Colon> code_numeral \<Rightarrow> code_numeral \<Rightarrow> bool"
+ (Haskell infixl 4 "==")
+ (Scala infixl 5 "==")
+
+code_const "op \<le> \<Colon> code_numeral \<Rightarrow> code_numeral \<Rightarrow> bool"
+ (Haskell infix 4 "<=")
+ (Scala infixl 4 "<=")
+
+code_const "op < \<Colon> code_numeral \<Rightarrow> code_numeral \<Rightarrow> bool"
+ (Haskell infix 4 "<")
+ (Scala infixl 4 "<")
+
+text {*
+ Setup for @{typ int} proper.
+*}
+
+
code_type int
(SML "IntInf.int")
(OCaml "Big'_int.big'_int")
@@ -26,8 +162,6 @@
setup {*
fold (Numeral.add_code @{const_name number_int_inst.number_of_int}
true Code_Printer.literal_numeral) ["SML", "OCaml", "Haskell", "Scala"]
- #> Numeral.add_code @{const_name number_int_inst.number_of_int}
- true Code_Printer.literal_numeral "Scala"
*}
code_const "Int.Pls" and "Int.Min" and "Int.Bit0" and "Int.Bit1"
@@ -48,72 +182,82 @@
and "!error(\"Bit0\")"
and "!error(\"Bit1\")")
-
code_const Int.pred
(SML "IntInf.- ((_), 1)")
(OCaml "Big'_int.pred'_big'_int")
(Haskell "!(_/ -/ 1)")
(Scala "!(_/ -/ 1)")
+ (Eval "!(_/ -/ 1)")
code_const Int.succ
(SML "IntInf.+ ((_), 1)")
(OCaml "Big'_int.succ'_big'_int")
(Haskell "!(_/ +/ 1)")
(Scala "!(_/ +/ 1)")
+ (Eval "!(_/ +/ 1)")
code_const "op + \<Colon> int \<Rightarrow> int \<Rightarrow> int"
(SML "IntInf.+ ((_), (_))")
(OCaml "Big'_int.add'_big'_int")
(Haskell infixl 6 "+")
(Scala infixl 7 "+")
+ (Eval infixl 8 "+")
code_const "uminus \<Colon> int \<Rightarrow> int"
(SML "IntInf.~")
(OCaml "Big'_int.minus'_big'_int")
(Haskell "negate")
(Scala "!(- _)")
+ (Eval "~/ _")
code_const "op - \<Colon> int \<Rightarrow> int \<Rightarrow> int"
(SML "IntInf.- ((_), (_))")
(OCaml "Big'_int.sub'_big'_int")
(Haskell infixl 6 "-")
(Scala infixl 7 "-")
+ (Eval infixl 8 "-")
code_const "op * \<Colon> int \<Rightarrow> int \<Rightarrow> int"
(SML "IntInf.* ((_), (_))")
(OCaml "Big'_int.mult'_big'_int")
(Haskell infixl 7 "*")
(Scala infixl 8 "*")
+ (Eval infixl 9 "*")
code_const pdivmod
(SML "IntInf.divMod/ (IntInf.abs _,/ IntInf.abs _)")
(OCaml "Big'_int.quomod'_big'_int/ (Big'_int.abs'_big'_int _)/ (Big'_int.abs'_big'_int _)")
(Haskell "divMod/ (abs _)/ (abs _)")
- (Scala "!(_.abs '/% _.abs)")
+ (Scala "!((k: BigInt) => (l: BigInt) =>/ if (l == 0)/ (BigInt(0), k) else/ (k.abs '/% l.abs))")
+ (Eval "Integer.div'_mod/ (abs _)/ (abs _)")
code_const "eq_class.eq \<Colon> int \<Rightarrow> int \<Rightarrow> bool"
(SML "!((_ : IntInf.int) = _)")
(OCaml "Big'_int.eq'_big'_int")
(Haskell infixl 4 "==")
(Scala infixl 5 "==")
+ (Eval infixl 6 "=")
code_const "op \<le> \<Colon> int \<Rightarrow> int \<Rightarrow> bool"
(SML "IntInf.<= ((_), (_))")
(OCaml "Big'_int.le'_big'_int")
(Haskell infix 4 "<=")
(Scala infixl 4 "<=")
+ (Eval infixl 6 "<=")
code_const "op < \<Colon> int \<Rightarrow> int \<Rightarrow> bool"
(SML "IntInf.< ((_), (_))")
(OCaml "Big'_int.lt'_big'_int")
(Haskell infix 4 "<")
- (Scala infixl 4 "<=")
+ (Scala infixl 4 "<")
+ (Eval infixl 6 "<")
code_const Code_Numeral.int_of
(SML "IntInf.fromInt")
(OCaml "_")
- (Haskell "_")
- (Scala "!BigInt((_))")
+ (Haskell "toInteger")
+ (Scala "!_.as'_BigInt")
+ (Eval "_")
text {* Evaluation *}
--- a/src/HOL/Library/Efficient_Nat.thy Fri Jul 23 21:29:29 2010 +0200
+++ b/src/HOL/Library/Efficient_Nat.thy Sun Jul 25 15:43:53 2010 +0200
@@ -50,19 +50,9 @@
"n * m = nat (of_nat n * of_nat m)"
unfolding of_nat_mult [symmetric] by simp
-text {* Specialized @{term "op div \<Colon> nat \<Rightarrow> nat \<Rightarrow> nat"}
- and @{term "op mod \<Colon> nat \<Rightarrow> nat \<Rightarrow> nat"} operations. *}
-
-definition divmod_aux :: "nat \<Rightarrow> nat \<Rightarrow> nat \<times> nat" where
- [code del]: "divmod_aux = divmod_nat"
-
-lemma [code]:
- "divmod_nat n m = (if m = 0 then (0, n) else divmod_aux n m)"
- unfolding divmod_aux_def divmod_nat_div_mod by simp
-
-lemma divmod_aux_code [code]:
- "divmod_aux n m = (nat (of_nat n div of_nat m), nat (of_nat n mod of_nat m))"
- unfolding divmod_aux_def divmod_nat_div_mod zdiv_int [symmetric] zmod_int [symmetric] by simp
+lemma divmod_nat_code [code]:
+ "divmod_nat n m = prod_fun nat nat (pdivmod (of_nat n) (of_nat m))"
+ by (simp add: prod_fun_def split_def pdivmod_def nat_div_distrib nat_mod_distrib divmod_nat_div_mod)
lemma eq_nat_code [code]:
"eq_class.eq n m \<longleftrightarrow> eq_class.eq (of_nat n \<Colon> int) (of_nat m)"
@@ -233,6 +223,7 @@
code_type nat
(SML "IntInf.int")
(OCaml "Big'_int.big'_int")
+ (Eval "int")
types_code
nat ("int")
@@ -281,7 +272,9 @@
instance Integral Nat where {
toInteger (Nat n) = n;
divMod n m = quotRem n m;
- quotRem (Nat n) (Nat m) = (Nat k, Nat l) where (k, l) = quotRem n m;
+ quotRem (Nat n) (Nat m)
+ | (m == 0) = (0, Nat n)
+ | otherwise = (Nat k, Nat l) where (k, l) = quotRem n m;
};
*}
@@ -353,9 +346,7 @@
setup {*
fold (Numeral.add_code @{const_name number_nat_inst.number_of_nat}
- false Code_Printer.literal_positive_numeral) ["SML", "OCaml", "Haskell"]
- #> Numeral.add_code @{const_name number_nat_inst.number_of_nat}
- false Code_Printer.literal_positive_numeral "Scala"
+ false Code_Printer.literal_positive_numeral) ["SML", "OCaml", "Haskell", "Scala"]
*}
text {*
@@ -400,6 +391,7 @@
code_const nat
(SML "IntInf.max/ (/0,/ _)")
(OCaml "Big'_int.max'_big'_int/ Big'_int.zero'_big'_int")
+ (Eval "Integer.max/ _/ 0")
text {* For Haskell and Scala, things are slightly different again. *}
@@ -407,19 +399,21 @@
(Haskell "toInteger" and "fromInteger")
(Scala "!_.as'_BigInt" and "Nat")
-text {* Conversion from and to indices. *}
+text {* Conversion from and to code numerals. *}
code_const Code_Numeral.of_nat
(SML "IntInf.toInt")
(OCaml "_")
- (Haskell "toInteger")
- (Scala "!_.as'_Int")
+ (Haskell "!(fromInteger/ ./ toInteger)")
+ (Scala "!Natural(_.as'_BigInt)")
+ (Eval "_")
code_const Code_Numeral.nat_of
(SML "IntInf.fromInt")
(OCaml "_")
- (Haskell "fromInteger")
- (Scala "Nat")
+ (Haskell "!(fromInteger/ ./ toInteger)")
+ (Scala "!Nat(_.as'_BigInt)")
+ (Eval "_")
text {* Using target language arithmetic operations whenever appropriate *}
@@ -428,6 +422,7 @@
(OCaml "Big'_int.add'_big'_int")
(Haskell infixl 6 "+")
(Scala infixl 7 "+")
+ (Eval infixl 8 "+")
code_const "op - \<Colon> nat \<Rightarrow> nat \<Rightarrow> nat"
(Haskell infixl 6 "-")
@@ -438,34 +433,35 @@
(OCaml "Big'_int.mult'_big'_int")
(Haskell infixl 7 "*")
(Scala infixl 8 "*")
+ (Eval infixl 9 "*")
-code_const divmod_aux
+code_const divmod_nat
(SML "IntInf.divMod/ ((_),/ (_))")
(OCaml "Big'_int.quomod'_big'_int")
(Haskell "divMod")
(Scala infixl 8 "/%")
-
-code_const divmod_nat
- (Haskell "divMod")
- (Scala infixl 8 "/%")
+ (Eval "Integer.div'_mod")
code_const "eq_class.eq \<Colon> nat \<Rightarrow> nat \<Rightarrow> bool"
(SML "!((_ : IntInf.int) = _)")
(OCaml "Big'_int.eq'_big'_int")
(Haskell infixl 4 "==")
(Scala infixl 5 "==")
+ (Eval infixl 6 "=")
code_const "op \<le> \<Colon> nat \<Rightarrow> nat \<Rightarrow> bool"
(SML "IntInf.<= ((_), (_))")
(OCaml "Big'_int.le'_big'_int")
(Haskell infix 4 "<=")
(Scala infixl 4 "<=")
+ (Eval infixl 6 "<=")
code_const "op < \<Colon> nat \<Rightarrow> nat \<Rightarrow> bool"
(SML "IntInf.< ((_), (_))")
(OCaml "Big'_int.lt'_big'_int")
(Haskell infix 4 "<")
(Scala infixl 4 "<")
+ (Eval infixl 6 "<")
consts_code
"0::nat" ("0")
--- a/src/HOL/Tools/Quotient/quotient_info.ML Fri Jul 23 21:29:29 2010 +0200
+++ b/src/HOL/Tools/Quotient/quotient_info.ML Sun Jul 25 15:43:53 2010 +0200
@@ -282,9 +282,9 @@
Keyword.diag (Scan.succeed (Toplevel.keep (pp_fn o Toplevel.context_of)))
val _ = map improper_command
- [(print_mapsinfo, "print_quotmaps", "prints out all map functions"),
- (print_quotinfo, "print_quotients", "prints out all quotients"),
- (print_qconstinfo, "print_quotconsts", "prints out all quotient constants")]
+ [(print_mapsinfo, "print_quotmaps", "print out all map functions"),
+ (print_quotinfo, "print_quotients", "print out all quotients"),
+ (print_qconstinfo, "print_quotconsts", "print out all quotient constants")]
end; (* structure *)
--- a/src/Pure/Isar/toplevel.ML Fri Jul 23 21:29:29 2010 +0200
+++ b/src/Pure/Isar/toplevel.ML Sun Jul 25 15:43:53 2010 +0200
@@ -632,7 +632,7 @@
fun run_command thy_name tr st =
(case
(case init_of tr of
- SOME name => Exn.capture (fn () => Thy_Load.check_name thy_name name) ()
+ SOME name => Exn.capture (fn () => Thy_Load.consistent_name thy_name name) ()
| NONE => Exn.Result ()) of
Exn.Result () =>
let val int = is_some (init_of tr) in
--- a/src/Pure/ProofGeneral/pgip_isabelle.ML Fri Jul 23 21:29:29 2010 +0200
+++ b/src/Pure/ProofGeneral/pgip_isabelle.ML Sun Jul 25 15:43:53 2010 +0200
@@ -80,7 +80,7 @@
NONE => (NONE, NONE)
| SOME fname =>
let val path = Path.explode fname in
- case Thy_Load.check_file Path.current path of
+ case Thy_Load.test_file Path.current path of
SOME _ => (SOME (PgipTypes.pgipurl_of_path path), NONE)
| NONE => (NONE, SOME fname)
end);
--- a/src/Pure/Thy/html.ML Fri Jul 23 21:29:29 2010 +0200
+++ b/src/Pure/Thy/html.ML Sun Jul 25 15:43:53 2010 +0200
@@ -30,7 +30,7 @@
val theory_source: text -> text
val begin_theory: Url.T * string -> string -> (Url.T option * string) list ->
(Url.T * Url.T * bool) list -> text -> text
- val ml_file: Url.T -> string -> text
+ val external_file: Url.T -> string -> text
end;
structure HTML: HTML =
@@ -309,7 +309,7 @@
begin_document ("Index of " ^ session) ^ up_link up ^
para ("View " ^ href_path graph "theory dependencies" ^
implode (map (fn (p, name) => "<br/>\nView " ^ href_path p name) docs)) ^
- "\n</div>\n<hr/>\n<div class=\"theories\">\n<h2>Theories</h2>\n<ul>\n";
+ "\n</div>\n<div class=\"theories\">\n<h2>Theories</h2>\n<ul>\n";
fun choice chs s = space_implode " " (map (fn (s', lnk) =>
enclose "[" "]" (if s = s' then keyword s' else href_name lnk s')) chs);
@@ -329,12 +329,12 @@
(name, begin_document ("Theory dependencies of " ^ session) ^
back_link back ^
para browser_size ^
- "\n</div>\n<hr/>\n<div class=\"graphbrowser\">\n\
+ "\n</div>\n<div class=\"graphbrowser\">\n\
\<applet code=\"GraphBrowser/GraphBrowser.class\" \
\archive=\"GraphBrowser.jar\" \
\width=" ^ quote width ^ " height=" ^ quote height ^ ">\n\
\<param name=\"graphfile\" value=\"" ^ "session.graph" ^ "\"/>\n\
- \</applet>\n<hr/>" ^ end_document)
+ \</applet>" ^ end_document)
end;
in map applet_page sizes end;
@@ -345,15 +345,15 @@
fun session_entries [] = "</ul>"
| session_entries es =
- "</ul>\n</div>\n<hr/>\n<div class=\"sessions\">\n\
+ "</ul>\n</div>\n<div class=\"sessions\">\n\
\<h2>Sessions</h2>\n<ul>\n" ^ implode (map entry es) ^ "</ul>";
(* theory *)
val theory_source = enclose
- "\n</div>\n<hr/>\n<div class=\"source\">\n<pre>"
- "</pre>\n<hr/>\n";
+ "\n</div>\n<div class=\"source\">\n<pre>"
+ "</pre>\n";
local
@@ -379,13 +379,13 @@
end;
-(* ML file *)
+(* external file *)
-fun ml_file path str =
+fun external_file path str =
begin_document ("File " ^ Url.implode path) ^
- "\n</div>\n<hr/><div class=\"mlsource\">\n" ^
+ "\n</div><div class=\"external_source\">\n" ^
verbatim str ^
- "\n</div>\n<hr/>\n<div class=\"mlfooter\">" ^
+ "\n</div>\n<div class=\"external_footer\">" ^
end_document;
end;
--- a/src/Pure/Thy/present.ML Fri Jul 23 21:29:29 2010 +0200
+++ b/src/Pure/Thy/present.ML Sun Jul 25 15:43:53 2010 +0200
@@ -460,18 +460,14 @@
val parents = Theory.parents_of thy;
val parent_specs = map (parent_link remote_path path) parents;
- fun prep_file (raw_path, loadit) =
- (case Thy_Load.check_ml dir raw_path of
- SOME (path, _) =>
- let
- val base = Path.base path;
- val base_html = html_ext base;
- val _ = add_file (Path.append html_prefix base_html,
- HTML.ml_file (Url.File base) (File.read path));
- in (Url.File base_html, Url.File raw_path, loadit) end
- | NONE => error ("Browser info: expected to find ML file " ^ quote (Path.implode raw_path)));
-
- val files_html = map prep_file files;
+ val files_html = files |> map (fn (raw_path, loadit) =>
+ let
+ val path = #1 (Thy_Load.check_file dir raw_path);
+ val base = Path.base path;
+ val base_html = html_ext base;
+ val _ = add_file (Path.append html_prefix base_html,
+ HTML.external_file (Url.File base) (File.read path));
+ in (Url.File base_html, Url.File raw_path, loadit) end);
fun prep_html_source (tex_source, html_source, html) =
let
--- a/src/Pure/Thy/thy_info.ML Fri Jul 23 21:29:29 2010 +0200
+++ b/src/Pure/Thy/thy_info.ML Sun Jul 25 15:43:53 2010 +0200
@@ -8,7 +8,6 @@
signature THY_INFO =
sig
datatype action = Update | Outdate | Remove
- val str_of_action: action -> string
val add_hook: (action -> string -> unit) -> unit
val get_names: unit -> string list
val known_thy: string -> bool
@@ -19,7 +18,6 @@
val is_finished: string -> bool
val master_directory: string -> Path.T
val loaded_files: string -> Path.T list
- val get_parents: string -> string list
val touch_thy: string -> unit
val touch_child_thys: string -> unit
val thy_ord: theory * theory -> order
@@ -44,7 +42,6 @@
(** theory loader actions and hooks **)
datatype action = Update | Outdate | Remove;
-val str_of_action = fn Update => "Update" | Outdate => "Outdate" | Remove => "Remove";
local
val hooks = Unsynchronized.ref ([]: (action -> string -> unit) list);
@@ -296,11 +293,7 @@
let
val dir = master_directory name;
val _ = check_unfinished error name;
- in
- (case Thy_Load.check_file dir path of
- SOME path_info => change_deps name (provide path name path_info)
- | NONE => error ("Could not find file " ^ quote (Path.implode path)))
- end;
+ in change_deps name (provide path name (Thy_Load.check_file dir path)) end;
fun load_file path =
if ! Output.timing then
@@ -417,12 +410,12 @@
local
-fun check_ml master (src_path, info) =
+fun check_file master (src_path, info) =
let val info' =
(case info of
NONE => NONE
| SOME (_, id) =>
- (case Thy_Load.check_ml (master_dir master) src_path of
+ (case Thy_Load.test_file (master_dir master) src_path of
NONE => NONE
| SOME (path', id') => if id <> id' then NONE else SOME (path', id')))
in (src_path, info') end;
@@ -444,7 +437,7 @@
in (false, init_deps master' text' parents' files', parents') end
else
let
- val files' = map (check_ml master') files;
+ val files' = map (check_file master') files;
val current = update_time >= 0 andalso can get_theory name
andalso forall (is_some o snd) files';
val update_time' = if current then update_time else ~1;
--- a/src/Pure/Thy/thy_load.ML Fri Jul 23 21:29:29 2010 +0200
+++ b/src/Pure/Thy/thy_load.ML Sun Jul 25 15:43:53 2010 +0200
@@ -1,7 +1,8 @@
(* Title: Pure/Thy/thy_load.ML
Author: Markus Wenzel, TU Muenchen
-Theory loader primitives, including load path.
+Loading files that contribute to a theory, including global load path
+management.
*)
signature BASIC_THY_LOAD =
@@ -10,22 +11,19 @@
val add_path: string -> unit
val path_add: string -> unit
val del_path: string -> unit
- val with_path: string -> ('a -> 'b) -> 'a -> 'b
- val with_paths: string list -> ('a -> 'b) -> 'a -> 'b
val reset_path: unit -> unit
end;
signature THY_LOAD =
sig
include BASIC_THY_LOAD
- val ml_exts: string list
val ml_path: string -> Path.T
val thy_path: string -> Path.T
val split_thy_path: Path.T -> Path.T * string
- val check_file: Path.T -> Path.T -> (Path.T * File.ident) option
- val check_ml: Path.T -> Path.T -> (Path.T * File.ident) option
+ val consistent_name: string -> string -> unit
+ val test_file: Path.T -> Path.T -> (Path.T * File.ident) option
+ val check_file: Path.T -> Path.T -> Path.T * File.ident
val check_thy: Path.T -> string -> Path.T * File.ident
- val check_name: string -> string -> unit
val deps_thy: Path.T -> string ->
{master: Path.T * File.ident, text: string, imports: string list, uses: Path.T list}
val load_ml: Path.T -> Path.T -> Path.T * File.ident
@@ -50,13 +48,7 @@
CRITICAL (fn () =>
(del_path s; Unsynchronized.change load_path (fn path => path @ [Path.explode s])));
-fun reset_path () = load_path := [Path.current];
-
-fun with_paths ss f x =
- CRITICAL (fn () =>
- setmp_CRITICAL load_path (! load_path @ map Path.explode ss) f x);
-
-fun with_path s f x = with_paths [s] f x;
+fun reset_path () = CRITICAL (fn () => load_path := [Path.current]);
fun search_path dir path =
distinct (op =) (dir :: (if Path.is_basic path then (! load_path) else [Path.current]));
@@ -66,7 +58,6 @@
(* file formats *)
-val ml_exts = ["ML", "sml"];
val ml_path = Path.ext "ML" o Path.basic;
val thy_path = Path.ext "thy" o Path.basic;
@@ -75,38 +66,46 @@
(path', "thy") => (Path.dir path', Path.implode (Path.base path'))
| _ => error ("Bad theory file specification " ^ Path.implode path));
+fun consistent_name name name' =
+ if name = name' then ()
+ else error ("Filename " ^ quote (Path.implode (thy_path name)) ^
+ " does not agree with theory name " ^ quote name');
+
(* check files *)
-fun check_ext exts paths src_path =
+local
+
+exception NOT_FOUND of Path.T list * Path.T;
+
+fun try_file dir src_path =
let
+ val prfxs = search_path dir src_path;
val path = Path.expand src_path;
val _ = Path.is_current path andalso error "Bad file specification";
-
- fun try_ext rel_path ext =
- let val ext_path = Path.expand (Path.ext ext rel_path)
- in Option.map (fn id => (File.full_path ext_path, id)) (File.ident ext_path) end;
- fun try_prfx prfx = get_first (try_ext (Path.append prfx path)) ("" :: exts);
- in get_first try_prfx paths end;
-
-fun check_file dir path = check_ext [] (search_path dir path) path;
-fun check_ml dir path = check_ext ml_exts (search_path dir path) path;
-
-fun check_thy dir name =
- let
- val thy_file = thy_path name;
- val paths = search_path dir thy_file;
+ val result =
+ prfxs |> get_first (fn prfx =>
+ let val full_path = File.full_path (Path.append prfx path)
+ in Option.map (pair full_path) (File.ident full_path) end);
in
- (case check_ext [] paths thy_file of
- NONE => error ("Could not find theory file " ^ quote (Path.implode thy_file) ^
- " in " ^ commas_quote (map Path.implode paths))
- | SOME thy_id => thy_id)
+ (case result of
+ SOME res => res
+ | NONE => raise NOT_FOUND (prfxs, path))
end;
-fun check_name name name' =
- if name = name' then ()
- else error ("Filename " ^ quote (Path.implode (thy_path name)) ^
- " does not agree with theory name " ^ quote name');
+in
+
+fun test_file dir file =
+ SOME (try_file dir file) handle NOT_FOUND _ => NONE;
+
+fun check_file dir file =
+ try_file dir file handle NOT_FOUND (prfxs, path) =>
+ error ("Could not find file " ^ quote (Path.implode path) ^
+ "\nin " ^ commas_quote (map Path.implode prfxs));
+
+fun check_thy dir name = check_file dir (thy_path name);
+
+end;
(* theory deps *)
@@ -117,17 +116,18 @@
val text = File.read path;
val (name', imports, uses) =
Thy_Header.read (Path.position path) (Source.of_string_limited 8000 text);
- val _ = check_name name name';
+ val _ = consistent_name name name';
val uses = map (Path.explode o #1) uses;
in {master = master, text = text, imports = imports, uses = uses} end;
-(* load files *)
+(* ML files *)
fun load_ml dir raw_path =
- (case check_ml dir raw_path of
- NONE => error ("Could not find ML file " ^ quote (Path.implode raw_path))
- | SOME (path, id) => (ML_Context.eval_file path; (path, id)));
+ let
+ val (path, id) = check_file dir raw_path;
+ val _ = ML_Context.eval_file path;
+ in (path, id) end;
end;
--- a/src/Pure/codegen.ML Fri Jul 23 21:29:29 2010 +0200
+++ b/src/Pure/codegen.ML Sun Jul 25 15:43:53 2010 +0200
@@ -1019,12 +1019,12 @@
val _ =
Outer_Syntax.command "code_library"
- "generates code for terms (one structure for each theory)" Keyword.thy_decl
+ "generate code for terms (one structure for each theory)" Keyword.thy_decl
(parse_code true);
val _ =
Outer_Syntax.command "code_module"
- "generates code for terms (single structure, incremental)" Keyword.thy_decl
+ "generate code for terms (single structure, incremental)" Keyword.thy_decl
(parse_code false);
end;
--- a/src/Tools/Code/code_haskell.ML Fri Jul 23 21:29:29 2010 +0200
+++ b/src/Tools/Code/code_haskell.ML Sun Jul 25 15:43:53 2010 +0200
@@ -415,6 +415,7 @@
literal_string = quote o translate_string char_haskell,
literal_numeral = numeral_haskell,
literal_positive_numeral = numeral_haskell,
+ literal_alternative_numeral = numeral_haskell,
literal_naive_numeral = numeral_haskell,
literal_list = enum "," "[" "]",
infix_cons = (5, ":")
--- a/src/Tools/Code/code_ml.ML Fri Jul 23 21:29:29 2010 +0200
+++ b/src/Tools/Code/code_ml.ML Sun Jul 25 15:43:53 2010 +0200
@@ -360,6 +360,7 @@
literal_string = quote o translate_string ML_Syntax.print_char,
literal_numeral = fn k => "(" ^ string_of_int k ^ " : IntInf.int)",
literal_positive_numeral = fn k => "(" ^ string_of_int k ^ " : IntInf.int)",
+ literal_alternative_numeral = fn k => "(" ^ string_of_int k ^ " : IntInf.int)",
literal_naive_numeral = string_of_int,
literal_list = enum "," "[" "]",
infix_cons = (7, "::")
@@ -702,6 +703,7 @@
literal_string = quote o translate_string char_ocaml,
literal_numeral = numeral_ocaml,
literal_positive_numeral = numeral_ocaml,
+ literal_alternative_numeral = numeral_ocaml,
literal_naive_numeral = numeral_ocaml,
literal_list = enum ";" "[" "]",
infix_cons = (6, "::")
--- a/src/Tools/Code/code_printer.ML Fri Jul 23 21:29:29 2010 +0200
+++ b/src/Tools/Code/code_printer.ML Sun Jul 25 15:43:53 2010 +0200
@@ -39,7 +39,9 @@
type literals
val Literals: { literal_char: string -> string, literal_string: string -> string,
- literal_numeral: int -> string, literal_positive_numeral: int -> string,
+ literal_numeral: int -> string,
+ literal_positive_numeral: int -> string,
+ literal_alternative_numeral: int -> string,
literal_naive_numeral: int -> string,
literal_list: Pretty.T list -> Pretty.T, infix_cons: int * string }
-> literals
@@ -47,6 +49,7 @@
val literal_string: literals -> string -> string
val literal_numeral: literals -> int -> string
val literal_positive_numeral: literals -> int -> string
+ val literal_alternative_numeral: literals -> int -> string
val literal_naive_numeral: literals -> int -> string
val literal_list: literals -> Pretty.T list -> Pretty.T
val infix_cons: literals -> int * string
@@ -171,6 +174,7 @@
literal_string: string -> string,
literal_numeral: int -> string,
literal_positive_numeral: int -> string,
+ literal_alternative_numeral: int -> string,
literal_naive_numeral: int -> string,
literal_list: Pretty.T list -> Pretty.T,
infix_cons: int * string
@@ -182,6 +186,7 @@
val literal_string = #literal_string o dest_Literals;
val literal_numeral = #literal_numeral o dest_Literals;
val literal_positive_numeral = #literal_positive_numeral o dest_Literals;
+val literal_alternative_numeral = #literal_alternative_numeral o dest_Literals;
val literal_naive_numeral = #literal_naive_numeral o dest_Literals;
val literal_list = #literal_list o dest_Literals;
val infix_cons = #infix_cons o dest_Literals;
--- a/src/Tools/Code/code_scala.ML Fri Jul 23 21:29:29 2010 +0200
+++ b/src/Tools/Code/code_scala.ML Sun Jul 25 15:43:53 2010 +0200
@@ -402,7 +402,7 @@
else let val k = ord c
in if k < 32 orelse k > 126 then "\\" ^ radixstring (8, "0", k) else c end
fun numeral_scala k = if k < 0
- then if k <= 2147483647 then "- " ^ string_of_int (~ k)
+ then if k > ~ 2147483647 then "- " ^ string_of_int (~ k)
else quote ("- " ^ string_of_int (~ k))
else if k <= 2147483647 then string_of_int k
else quote (string_of_int k)
@@ -411,8 +411,8 @@
literal_string = quote o translate_string char_scala,
literal_numeral = fn k => "BigInt(" ^ numeral_scala k ^ ")",
literal_positive_numeral = fn k => "Nat(" ^ numeral_scala k ^ ")",
- literal_naive_numeral = fn k => if k >= 0
- then string_of_int k else "(- " ^ string_of_int (~ 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, "::")
} end;