# HG changeset patch # User blanchet # Date 1280065433 -7200 # Node ID 61887e5b3d1d3630c77ae760b6f5767be21f8c13 # Parent 6fe5fa827f188860af59d1793e8bad7b013082a6# Parent d7dbe01f48d7abf366e0f8cea0f7ebcebf0cbd05 merged diff -r d7dbe01f48d7 -r 61887e5b3d1d NEWS --- 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 *** diff -r d7dbe01f48d7 -r 61887e5b3d1d lib/html/isabelle.css --- 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 */ diff -r d7dbe01f48d7 -r 61887e5b3d1d src/HOL/Boogie/Tools/boogie_commands.ML --- 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)) diff -r d7dbe01f48d7 -r 61887e5b3d1d src/HOL/Code_Numeral.thy --- 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 + \ code_numeral \ code_numeral \ code_numeral" (SML "Int.+/ ((_),/ (_))") (OCaml "Big'_int.add'_big'_int") (Haskell infixl 6 "+") (Scala infixl 7 "+") + (Eval infixl 8 "+") code_const "subtract_code_numeral \ code_numeral \ code_numeral \ 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 * \ code_numeral \ code_numeral \ 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 \ code_numeral \ code_numeral \ bool" (SML "!((_ : Int.int) = _)") (OCaml "Big'_int.eq'_big'_int") (Haskell infixl 4 "==") (Scala infixl 5 "==") + (Eval "!((_ : int) = _)") code_const "op \ \ code_numeral \ code_numeral \ bool" (SML "Int.<=/ ((_),/ (_))") (OCaml "Big'_int.le'_big'_int") (Haskell infix 4 "<=") (Scala infixl 4 "<=") + (Eval infixl 6 "<=") code_const "op < \ code_numeral \ code_numeral \ bool" (SML "Int.= 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 + \ code_numeral \ code_numeral \ code_numeral" + (Haskell infixl 6 "+") + (Scala infixl 7 "+") + +code_const "op - \ code_numeral \ code_numeral \ code_numeral" + (Haskell infixl 6 "-") + (Scala infixl 7 "-") + +code_const "op * \ code_numeral \ code_numeral \ code_numeral" + (Haskell infixl 7 "*") + (Scala infixl 8 "*") + +code_const div_mod_code_numeral + (Haskell "divMod") + (Scala infixl 8 "/%") + +code_const "eq_class.eq \ code_numeral \ code_numeral \ bool" + (Haskell infixl 4 "==") + (Scala infixl 5 "==") + +code_const "op \ \ code_numeral \ code_numeral \ bool" + (Haskell infix 4 "<=") + (Scala infixl 4 "<=") + +code_const "op < \ code_numeral \ code_numeral \ 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 + \ int \ int \ int" (SML "IntInf.+ ((_), (_))") (OCaml "Big'_int.add'_big'_int") (Haskell infixl 6 "+") (Scala infixl 7 "+") + (Eval infixl 8 "+") code_const "uminus \ int \ int" (SML "IntInf.~") (OCaml "Big'_int.minus'_big'_int") (Haskell "negate") (Scala "!(- _)") + (Eval "~/ _") code_const "op - \ int \ int \ int" (SML "IntInf.- ((_), (_))") (OCaml "Big'_int.sub'_big'_int") (Haskell infixl 6 "-") (Scala infixl 7 "-") + (Eval infixl 8 "-") code_const "op * \ int \ int \ 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 \ int \ int \ bool" (SML "!((_ : IntInf.int) = _)") (OCaml "Big'_int.eq'_big'_int") (Haskell infixl 4 "==") (Scala infixl 5 "==") + (Eval infixl 6 "=") code_const "op \ \ int \ int \ bool" (SML "IntInf.<= ((_), (_))") (OCaml "Big'_int.le'_big'_int") (Haskell infix 4 "<=") (Scala infixl 4 "<=") + (Eval infixl 6 "<=") code_const "op < \ int \ int \ 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 *} diff -r d7dbe01f48d7 -r 61887e5b3d1d src/HOL/Library/Efficient_Nat.thy --- 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 \ nat \ nat \ nat"} - and @{term "op mod \ nat \ nat \ nat"} operations. *} - -definition divmod_aux :: "nat \ nat \ nat \ 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 \ eq_class.eq (of_nat n \ 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 - \ nat \ nat \ 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 \ nat \ nat \ bool" (SML "!((_ : IntInf.int) = _)") (OCaml "Big'_int.eq'_big'_int") (Haskell infixl 4 "==") (Scala infixl 5 "==") + (Eval infixl 6 "=") code_const "op \ \ nat \ nat \ bool" (SML "IntInf.<= ((_), (_))") (OCaml "Big'_int.le'_big'_int") (Haskell infix 4 "<=") (Scala infixl 4 "<=") + (Eval infixl 6 "<=") code_const "op < \ nat \ nat \ bool" (SML "IntInf.< ((_), (_))") (OCaml "Big'_int.lt'_big'_int") (Haskell infix 4 "<") (Scala infixl 4 "<") + (Eval infixl 6 "<") consts_code "0::nat" ("0") diff -r d7dbe01f48d7 -r 61887e5b3d1d src/HOL/Tools/Quotient/quotient_info.ML --- 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 *) diff -r d7dbe01f48d7 -r 61887e5b3d1d src/Pure/Isar/toplevel.ML --- 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 diff -r d7dbe01f48d7 -r 61887e5b3d1d src/Pure/ProofGeneral/pgip_isabelle.ML --- 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); diff -r d7dbe01f48d7 -r 61887e5b3d1d src/Pure/Thy/html.ML --- 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) => "
\nView " ^ href_path p name) docs)) ^ - "\n\n
\n
\n

Theories

\n
    \n"; + "\n
\n
\n

Theories

\n
    \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
\n
\n
\n\ + "\n
\n
\n\ \\n\ \\n\ - \\n
" ^ end_document) + \" ^ end_document) end; in map applet_page sizes end; @@ -345,15 +345,15 @@ fun session_entries [] = "" | session_entries es = - "\n
\n
\n
\n\ + "\n
\n
\n\ \

Sessions

\n
    \n" ^ implode (map entry es) ^ "
"; (* theory *) val theory_source = enclose - "\n
\n
\n
\n
"
-  "
\n
\n"; + "\n
\n
\n
"
+  "
\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
\n
\n" ^ + "\n
\n" ^ verbatim str ^ - "\n
\n
\n
" ^ + "\n
\n
" ^ end_document; end; diff -r d7dbe01f48d7 -r 61887e5b3d1d src/Pure/Thy/present.ML --- 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 diff -r d7dbe01f48d7 -r 61887e5b3d1d src/Pure/Thy/thy_info.ML --- 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; diff -r d7dbe01f48d7 -r 61887e5b3d1d src/Pure/Thy/thy_load.ML --- 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; diff -r d7dbe01f48d7 -r 61887e5b3d1d src/Pure/codegen.ML --- 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; diff -r d7dbe01f48d7 -r 61887e5b3d1d src/Tools/Code/code_haskell.ML --- 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, ":") diff -r d7dbe01f48d7 -r 61887e5b3d1d src/Tools/Code/code_ml.ML --- 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, "::") diff -r d7dbe01f48d7 -r 61887e5b3d1d src/Tools/Code/code_printer.ML --- 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; diff -r d7dbe01f48d7 -r 61887e5b3d1d src/Tools/Code/code_scala.ML --- 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;