--- a/Admin/isatest/isatest-stats Thu Jun 25 14:59:29 2009 +0200
+++ b/Admin/isatest/isatest-stats Thu Jun 25 15:42:36 2009 +0200
@@ -24,6 +24,7 @@
HOL-MetisExamples \
HOL-MicroJava \
HOL-NSA \
+ HOL-NewNumberTheory \
HOL-Nominal-Examples \
HOL-NumberTheory \
HOL-SET-Protocol \
--- a/bin/isabelle-process Thu Jun 25 14:59:29 2009 +0200
+++ b/bin/isabelle-process Thu Jun 25 15:42:36 2009 +0200
@@ -214,7 +214,7 @@
NICE="nice"
if [ -n "$WRAPPER_OUTPUT" ]; then
[ "$WRAPPER_OUTPUT" = "-" -o -p "$WRAPPER_OUTPUT" ] || fail "Bad named pipe: $WRAPPER_OUTPUT"
- MLTEXT="$MLTEXT; IsabelleProcess.init \"$WRAPPER_OUTPUT\";"
+ MLTEXT="$MLTEXT; Isabelle_Process.init \"$WRAPPER_OUTPUT\";"
elif [ -n "$PGIP" ]; then
MLTEXT="$MLTEXT; ProofGeneralPgip.init_pgip $ISAR;"
elif [ -n "$PROOFGENERAL" ]; then
--- a/src/HOL/Tools/res_hol_clause.ML Thu Jun 25 14:59:29 2009 +0200
+++ b/src/HOL/Tools/res_hol_clause.ML Thu Jun 25 15:42:36 2009 +0200
@@ -12,8 +12,6 @@
val comb_B: thm
val comb_C: thm
val comb_S: thm
- datatype type_level = T_FULL | T_CONST
- val typ_level: type_level
val minimize_applies: bool
type axiom_name = string
type polarity = bool
@@ -59,10 +57,8 @@
val equal_imp_fequal = thm "ATP_Linkup.equal_imp_fequal";
-(*The different translations of types*)
-datatype type_level = T_FULL | T_CONST;
-
-val typ_level = T_CONST;
+(* Parameter t_full below indicates that full type information is to be
+exported *)
(*If true, each function will be directly applied to as many arguments as possible, avoiding
use of the "apply" operator. Use of hBOOL is also minimized.*)
@@ -260,26 +256,26 @@
fun wrap_type_if t_full cnh (head, s, tp) =
if head_needs_hBOOL cnh head then wrap_type t_full (s, tp) else s;
-fun string_of_combterm t_full cma cnh t =
+fun string_of_combterm (params as (t_full, cma, cnh)) t =
let val (head, args) = strip_comb t
in wrap_type_if t_full cnh (head,
- string_of_applic t_full cma (head, map (string_of_combterm t_full cma cnh) args),
+ string_of_applic t_full cma (head, map (string_of_combterm (params)) args),
type_of_combterm t)
end;
(*Boolean-valued terms are here converted to literals.*)
-fun boolify t_full cma cnh t =
- "hBOOL" ^ RC.paren_pack [string_of_combterm t_full cma cnh t];
+fun boolify params t =
+ "hBOOL" ^ RC.paren_pack [string_of_combterm params t];
-fun string_of_predicate t_full cma cnh t =
+fun string_of_predicate (params as (_,_,cnh)) t =
case t of
(CombApp(CombApp(CombConst("equal",_,_), t1), t2)) =>
(*DFG only: new TPTP prefers infix equality*)
- ("equal" ^ RC.paren_pack [string_of_combterm t_full cma cnh t1, string_of_combterm t_full cma cnh t2])
+ ("equal" ^ RC.paren_pack [string_of_combterm params t1, string_of_combterm params t2])
| _ =>
case #1 (strip_comb t) of
- CombConst(c,_,_) => if needs_hBOOL cnh c then boolify t_full cma cnh t else string_of_combterm t_full cma cnh t
- | _ => boolify t_full cma cnh t;
+ CombConst(c,_,_) => if needs_hBOOL cnh c then boolify params t else string_of_combterm params t
+ | _ => boolify params t;
fun string_of_clausename (cls_id,ax_name) =
RC.clause_prefix ^ RC.ascii_of ax_name ^ "_" ^ Int.toString cls_id;
@@ -290,23 +286,23 @@
(*** tptp format ***)
-fun tptp_of_equality t_full cma cnh pol (t1,t2) =
+fun tptp_of_equality params pol (t1,t2) =
let val eqop = if pol then " = " else " != "
- in string_of_combterm t_full cma cnh t1 ^ eqop ^ string_of_combterm t_full cma cnh t2 end;
+ in string_of_combterm params t1 ^ eqop ^ string_of_combterm params t2 end;
-fun tptp_literal t_full cma cnh (Literal(pol, CombApp(CombApp(CombConst("equal",_,_), t1), t2))) =
- tptp_of_equality t_full cma cnh pol (t1,t2)
- | tptp_literal t_full cma cnh (Literal(pol,pred)) =
- RC.tptp_sign pol (string_of_predicate t_full cma cnh pred);
+fun tptp_literal params (Literal(pol, CombApp(CombApp(CombConst("equal",_,_), t1), t2))) =
+ tptp_of_equality params pol (t1,t2)
+ | tptp_literal params (Literal(pol,pred)) =
+ RC.tptp_sign pol (string_of_predicate params pred);
(*Given a clause, returns its literals paired with a list of literals concerning TFrees;
the latter should only occur in conjecture clauses.*)
-fun tptp_type_lits t_full cma cnh pos (Clause{literals, ctypes_sorts, ...}) =
- (map (tptp_literal t_full cma cnh) literals,
+fun tptp_type_lits params pos (Clause{literals, ctypes_sorts, ...}) =
+ (map (tptp_literal params) literals,
map (RC.tptp_of_typeLit pos) (RC.add_typs ctypes_sorts));
-fun clause2tptp (t_full, cma, cnh) (cls as Clause{axiom_name,clause_id,kind,ctypes_sorts,...}) =
- let val (lits,tylits) = tptp_type_lits t_full cma cnh (kind = RC.Conjecture) cls
+fun clause2tptp params (cls as Clause{axiom_name,clause_id,kind,ctypes_sorts,...}) =
+ let val (lits,tylits) = tptp_type_lits params (kind = RC.Conjecture) cls
in
(RC.gen_tptp_cls(clause_id,axiom_name,kind,lits,tylits), tylits)
end;
@@ -314,10 +310,10 @@
(*** dfg format ***)
-fun dfg_literal t_full cma cnh (Literal(pol,pred)) = RC.dfg_sign pol (string_of_predicate t_full cma cnh pred);
+fun dfg_literal params (Literal(pol,pred)) = RC.dfg_sign pol (string_of_predicate params pred);
-fun dfg_type_lits t_full cma cnh pos (Clause{literals, ctypes_sorts, ...}) =
- (map (dfg_literal t_full cma cnh) literals,
+fun dfg_type_lits params pos (Clause{literals, ctypes_sorts, ...}) =
+ (map (dfg_literal params) literals,
map (RC.dfg_of_typeLit pos) (RC.add_typs ctypes_sorts));
fun get_uvars (CombConst _) vars = vars
@@ -328,8 +324,8 @@
fun dfg_vars (Clause {literals,...}) = RC.union_all (map get_uvars_l literals);
-fun clause2dfg (t_full, cma, cnh) (cls as Clause{axiom_name,clause_id,kind,ctypes_sorts,...}) =
- let val (lits,tylits) = dfg_type_lits t_full cma cnh (kind = RC.Conjecture) cls
+fun clause2dfg params (cls as Clause{axiom_name,clause_id,kind,ctypes_sorts,...}) =
+ let val (lits,tylits) = dfg_type_lits params (kind = RC.Conjecture) cls
val vars = dfg_vars cls
val tvars = RC.get_tvar_strs ctypes_sorts
in
@@ -341,7 +337,7 @@
fun addtypes tvars tab = List.foldl RC.add_foltype_funcs tab tvars;
-fun add_decls t_full cma cnh (CombConst(c,tp,tvars), (funcs,preds)) =
+fun add_decls (t_full, cma, cnh) (CombConst(c,tp,tvars), (funcs,preds)) =
if c = "equal" then (addtypes tvars funcs, preds)
else
let val arity = min_arity_of cma c
@@ -351,20 +347,20 @@
if needs_hBOOL cnh c then (addtypes tvars (addit funcs), preds)
else (addtypes tvars funcs, addit preds)
end
- | add_decls _ _ _ (CombVar(_,ctp), (funcs,preds)) =
+ | add_decls _ (CombVar(_,ctp), (funcs,preds)) =
(RC.add_foltype_funcs (ctp,funcs), preds)
- | add_decls t_full cma cnh (CombApp(P,Q),decls) = add_decls t_full cma cnh (P,add_decls t_full cma cnh (Q,decls));
+ | add_decls params (CombApp(P,Q),decls) = add_decls params (P,add_decls params (Q,decls));
-fun add_literal_decls t_full cma cnh (Literal(_,c), decls) = add_decls t_full cma cnh (c,decls);
+fun add_literal_decls params (Literal(_,c), decls) = add_decls params (c,decls);
-fun add_clause_decls t_full cma cnh (Clause {literals, ...}, decls) =
- List.foldl (add_literal_decls t_full cma cnh) decls literals
+fun add_clause_decls params (Clause {literals, ...}, decls) =
+ List.foldl (add_literal_decls params) decls literals
handle Symtab.DUP a => error ("function " ^ a ^ " has multiple arities")
-fun decls_of_clauses (t_full, cma, cnh) clauses arity_clauses =
+fun decls_of_clauses params clauses arity_clauses =
let val init_functab = Symtab.update (type_wrapper,2) (Symtab.update ("hAPP",2) RC.init_functab)
val init_predtab = Symtab.update ("hBOOL",1) Symtab.empty
- val (functab,predtab) = (List.foldl (add_clause_decls t_full cma cnh) (init_functab, init_predtab) clauses)
+ val (functab,predtab) = (List.foldl (add_clause_decls params) (init_functab, init_predtab) clauses)
in
(Symtab.dest (List.foldl RC.add_arityClause_funcs functab arity_clauses),
Symtab.dest predtab)
--- a/src/Pure/Isar/isar.scala Thu Jun 25 14:59:29 2009 +0200
+++ b/src/Pure/Isar/isar.scala Thu Jun 25 15:42:36 2009 +0200
@@ -7,8 +7,9 @@
package isabelle
-class Isar(isabelle_system: IsabelleSystem, results: EventBus[IsabelleProcess.Result], args: String*)
- extends IsabelleProcess(isabelle_system, results, args: _*)
+class Isar(isabelle_system: Isabelle_System,
+ results: EventBus[Isabelle_Process.Result], args: String*)
+ extends Isabelle_Process(isabelle_system, results, args: _*)
{
/* basic editor commands */
--- a/src/Pure/Isar/isar_document.scala Thu Jun 25 14:59:29 2009 +0200
+++ b/src/Pure/Isar/isar_document.scala Thu Jun 25 15:42:36 2009 +0200
@@ -14,7 +14,7 @@
type Document_ID = String
}
-trait IsarDocument extends IsabelleProcess
+trait IsarDocument extends Isabelle_Process
{
import IsarDocument._
--- a/src/Pure/System/isabelle_process.ML Thu Jun 25 14:59:29 2009 +0200
+++ b/src/Pure/System/isabelle_process.ML Thu Jun 25 15:42:36 2009 +0200
@@ -27,7 +27,7 @@
val init: string -> unit
end;
-structure IsabelleProcess: ISABELLE_PROCESS =
+structure Isabelle_Process: ISABELLE_PROCESS =
struct
(* print modes *)
--- a/src/Pure/System/isabelle_process.scala Thu Jun 25 14:59:29 2009 +0200
+++ b/src/Pure/System/isabelle_process.scala Thu Jun 25 15:42:36 2009 +0200
@@ -12,7 +12,7 @@
InputStream, OutputStream, IOException}
-object IsabelleProcess {
+object Isabelle_Process {
/* results */
@@ -96,7 +96,7 @@
def is_system = Kind.is_system(kind)
}
- def parse_message(isabelle_system: IsabelleSystem, result: Result) =
+ def parse_message(isabelle_system: Isabelle_System, result: Result) =
{
XML.Elem(Markup.MESSAGE, (Markup.CLASS, Kind.markup(result.kind)) :: result.props,
YXML.parse_body_failsafe(isabelle_system.symbols.decode(result.result)))
@@ -104,16 +104,16 @@
}
-class IsabelleProcess(isabelle_system: IsabelleSystem,
- results: EventBus[IsabelleProcess.Result], args: String*)
+class Isabelle_Process(isabelle_system: Isabelle_System,
+ results: EventBus[Isabelle_Process.Result], args: String*)
{
- import IsabelleProcess._
+ import Isabelle_Process._
/* demo constructor */
def this(args: String*) =
- this(new IsabelleSystem, new EventBus[IsabelleProcess.Result] + Console.println, args: _*)
+ this(new Isabelle_System, new EventBus[Isabelle_Process.Result] + Console.println, args: _*)
/* process information */
@@ -128,7 +128,7 @@
/* results */
def parse_message(result: Result): XML.Tree =
- IsabelleProcess.parse_message(isabelle_system, result)
+ Isabelle_Process.parse_message(isabelle_system, result)
private val result_queue = new LinkedBlockingQueue[Result]
@@ -230,7 +230,7 @@
private class StdinThread(out_stream: OutputStream) extends Thread("isabelle: stdin") {
override def run() = {
- val writer = new BufferedWriter(new OutputStreamWriter(out_stream, IsabelleSystem.charset))
+ val writer = new BufferedWriter(new OutputStreamWriter(out_stream, Isabelle_System.charset))
var finished = false
while (!finished) {
try {
@@ -260,7 +260,7 @@
private class StdoutThread(in_stream: InputStream) extends Thread("isabelle: stdout") {
override def run() = {
- val reader = new BufferedReader(new InputStreamReader(in_stream, IsabelleSystem.charset))
+ val reader = new BufferedReader(new InputStreamReader(in_stream, Isabelle_System.charset))
var result = new StringBuilder(100)
var finished = false
--- a/src/Pure/System/isabelle_system.scala Thu Jun 25 14:59:29 2009 +0200
+++ b/src/Pure/System/isabelle_system.scala Thu Jun 25 15:42:36 2009 +0200
@@ -1,7 +1,7 @@
/* Title: Pure/System/isabelle_system.scala
Author: Makarius
-Isabelle system support -- basic Cygwin/Posix compatibility.
+Isabelle system support, with basic Cygwin/Posix compatibility.
*/
package isabelle
@@ -13,7 +13,7 @@
import scala.util.matching.Regex
-object IsabelleSystem
+object Isabelle_System
{
val charset = "UTF-8"
@@ -48,20 +48,23 @@
}
-class IsabelleSystem
+class Isabelle_System
{
- /* unique ids */
+ /** unique ids **/
private var id_count: BigInt = 0
def id(): String = synchronized { id_count += 1; "j" + id_count }
- /* Isabelle settings environment */
+
+ /** Isabelle environment **/
+
+ /* platform prefixes */
private val (platform_root, drive_prefix, shell_prefix) =
{
- if (IsabelleSystem.is_cygwin) {
+ if (Isabelle_System.is_cygwin) {
val root = Cygwin.root() getOrElse "C:\\cygwin"
val drive = Cygwin.cygdrive() getOrElse "/cygdrive"
val shell = List(root + "\\bin\\bash", "-l")
@@ -70,6 +73,9 @@
else ("/", "", Nil)
}
+
+ /* bash environment */
+
private val environment: Map[String, String] =
{
import scala.collection.jcl.Conversions._
@@ -88,8 +94,8 @@
val dump = File.createTempFile("isabelle", null)
try {
val cmdline = shell_prefix ::: List(isabelle, "getenv", "-d", dump.toString)
- val proc = IsabelleSystem.raw_execute(env0, true, cmdline: _*)
- val (output, rc) = IsabelleSystem.process_output(proc)
+ val proc = Isabelle_System.raw_execute(env0, true, cmdline: _*)
+ val (output, rc) = Isabelle_System.process_output(proc)
if (rc != 0) error(output)
val entries =
@@ -105,10 +111,11 @@
finally { dump.delete }
}
+
+ /* getenv */
+
def getenv(name: String): String =
- {
environment.getOrElse(if (name == "HOME") "HOME_JVM" else name, "")
- }
def getenv_strict(name: String): String =
{
@@ -119,7 +126,43 @@
override def toString = getenv("ISABELLE_HOME")
- /* file path specifications */
+
+ /** file path specifications **/
+
+ /* Isabelle paths */
+
+ def expand_path(source_path: String): String =
+ {
+ val result_path = new StringBuilder
+ def init(path: String)
+ {
+ if (path.startsWith("/")) {
+ result_path.clear
+ result_path += '/'
+ }
+ }
+ def append(path: String)
+ {
+ init(path)
+ for (p <- path.split("/") if p != "") {
+ val len = result_path.length
+ if (len > 0 && result_path(len - 1) != '/')
+ result_path += '/'
+ result_path ++= p
+ }
+ }
+ init(source_path)
+ for (p <- source_path.split("/")) {
+ if (p.startsWith("$")) append(getenv_strict(p.substring(1)))
+ else if (p == "~") append(getenv_strict("HOME"))
+ else if (p == "~~") append(getenv_strict("ISABELLE_HOME"))
+ else append(p)
+ }
+ result_path.toString
+ }
+
+
+ /* platform paths */
private val Cygdrive = new Regex(
if (drive_prefix == "") "\0"
@@ -128,39 +171,21 @@
def platform_path(source_path: String): String =
{
val result_path = new StringBuilder
-
- def init(path: String): String =
- {
- path match {
+ val rest =
+ expand_path(source_path) match {
case Cygdrive(drive, rest) =>
- result_path.length = 0
- result_path.append(drive)
- result_path.append(":")
- result_path.append(File.separator)
+ result_path ++= (drive + ":" + File.separator)
rest
- case _ if (path.startsWith("/")) =>
- result_path.length = 0
- result_path.append(platform_root)
- path.substring(1)
- case _ => path
+ case path if path.startsWith("/") =>
+ result_path ++= platform_root
+ path
+ case path => path
}
- }
- def append(path: String)
- {
- for (p <- init(path) split "/") {
- if (p != "") {
- val len = result_path.length
- if (len > 0 && result_path(len - 1) != File.separatorChar)
- result_path.append(File.separator)
- result_path.append(p)
- }
- }
- }
- for (p <- init(source_path) split "/") {
- if (p.startsWith("$")) append(getenv_strict(p.substring(1)))
- else if (p == "~") append(getenv_strict("HOME"))
- else if (p == "~~") append(getenv_strict("ISABELLE_HOME"))
- else append(p)
+ for (p <- rest.split("/") if p != "") {
+ val len = result_path.length
+ if (len > 0 && result_path(len - 1) != File.separatorChar)
+ result_path += File.separatorChar
+ result_path ++= p
}
result_path.toString
}
@@ -186,20 +211,22 @@
}
+ /** system tools **/
+
/* external processes */
def execute(redirect: Boolean, args: String*): Process =
{
val cmdline =
- if (IsabelleSystem.is_cygwin) List(platform_path("/bin/env")) ++ args
+ if (Isabelle_System.is_cygwin) List(platform_path("/bin/env")) ++ args
else args
- IsabelleSystem.raw_execute(environment, redirect, cmdline: _*)
+ Isabelle_System.raw_execute(environment, redirect, cmdline: _*)
}
def isabelle_tool(args: String*): (String, Int) =
{
val proc = execute(true, (List(getenv_strict("ISABELLE_TOOL")) ++ args): _*)
- IsabelleSystem.process_output(proc)
+ Isabelle_System.process_output(proc)
}
@@ -222,12 +249,14 @@
{
// blocks until writer is ready
val stream =
- if (IsabelleSystem.is_cygwin) execute(false, "cat", fifo).getInputStream
+ if (Isabelle_System.is_cygwin) execute(false, "cat", fifo).getInputStream
else new FileInputStream(fifo)
- new BufferedReader(new InputStreamReader(stream, IsabelleSystem.charset))
+ new BufferedReader(new InputStreamReader(stream, Isabelle_System.charset))
}
+ /** Isabelle resources **/
+
/* find logics */
def find_logics(): List[String] =