(****************************************************************************
******************************** porgi.sml *******************************
****************************************************************************)
(* Porgi Version 1.0 -- September 2007
a Proof Or Refutation Generator for Intuitionistic propositional logic
Alley Stoughton
Alley.Stoughton@gmail.com
http://alleystoughton.us
Porgi is set up to be compiled using MLton - type mlton porgi.sml
to create the executable "porgi"
Before reading the following code, it would be useful to read the
paper, "Porgi: a Proof Or Refutation Generator for Intuitionistic
propositional logic", which can be obtained via WWW URL
http://alleystoughton.us/porgi/ *)
local (* BEGINNING OF LOCAL PART; to find end, search for *)
(* "END OF LOCAL PART" *)
(************************ Miscellaneous Definitions *************************)
val version = "1.0"; (* version number *)
exception CannotHappen (* used to avoid warning messages *)
(* sumIntList : int list -> int *)
fun sumIntList(nil : int list) = 0
| sumIntList(x :: xs) = x + sumIntList xs
(* appOpp : 'a list -> ('a -> 'b) -> unit *)
fun appOpp xs f = app f xs
(* all : ('a -> bool) -> 'a list -> bool *)
fun all p nil = true
| all p (x :: xs) = p x andalso all p xs
(* filter : ('a -> bool) -> 'a list -> 'a list *)
fun filter p nil = nil
| filter p (x :: xs) =
if p x
then x :: filter p xs
else filter p xs
(* copies : int -> string -> string *)
fun copies 0 _ = ""
| copies n s = s ^ copies (n - 1) s
(* numeral : int -> string
convert an integer into a base-10 numeral (beginning with ~, if the
integer is negative) *)
local
fun digit n = str(chr(ord #"0" + n))
fun num n =
if n < 10
then digit n
else num(n div 10) ^ digit(n mod 10)
in
fun numeral n = if n >= 0 then num n else "~" ^ num(~n)
end
(* prStr : string -> unit *)
fun prStr s = TextIO.output(TextIO.stdOut, s)
(* indent : int -> unit *)
fun indent 0 = ()
| indent n = (prStr " "; indent(n - 1))
(* prStrs : string list -> unit *)
fun prStrs nil = ()
| prStrs [x] = prStr x
| prStrs (x :: xs) = (prStr x; prStr ", "; prStrs xs)
(* prInt : int -> unit *)
fun prInt n = prStr(numeral n)
(* prInts : int list -> unit *)
fun prInts nil = ()
| prInts [x] = prInt x
| prInts (x :: xs) = (prInt x; prStr ", "; prInts xs)
(* exit : OS.Process.status -> 'a *)
fun exit x =
(TextIO.flushOut TextIO.stdOut;
TextIO.flushOut TextIO.stdErr; OS.Process.exit x)
(* error : string -> 'a *)
fun error s =
(TextIO.output(TextIO.stdErr, s);
TextIO.output(TextIO.stdErr, "\n"); exit OS.Process.failure)
(************************** Propositional Formulas **************************)
infixr 5 >> (* see form datatype *)
infixr 6 ||
infixr 7 &&
datatype form =
F (* falsity *)
| Var of string (* propositional variable (single uppercase letter) *)
| && of form * form (* conjunction *)
| || of form * form (* disjunction *)
| >> of form * form (* implication *)
(* a form_set is a list of form's with no duplicates
a form_set_set is a list of form_set's with no duplicates,
relative to the equality testing function formSetEq (see below) *)
type form_set = form list
type form_set_set = form_set list
(***************************** Global Variables *****************************)
val program = ref "" (* name of executable; set by entryPoint *)
val sequentStr = ref "" (* single succedent sequent in string form; *)
(* set by processArgs *)
(* sequent-related; set by main *)
val sequent = ref(nil : form list, F) (* sequent; antecedent in list *)
(* form *)
val assumptions = ref(nil : form_set) (* sequent antecedent *)
val conclusion = ref F (* sequent succedent *)
val universe = ref(nil : form_set) (* subformulas of sequent *)
val areFal = ref false (* true iff universe includes falsity *)
val areAnd = ref false (* true iff universe includes conjunctions *)
val areOr = ref false (* true iff universe includes disjunctions *)
val areImp = ref false (* true iff universe includes implications *)
(* options; set by processArgs *)
val minimal = ref false (* use minimal logic (treat falsity like prop var) *)
val check = ref false (* just check deducibility *)
val lambda = ref false (* output lambda term instead of deduction *)
val verbose = ref false (* output verbose results *)
val trace = ref false (* output tracing information *)
(************************* Formula-related Functions ************************)
(* isFal : form -> bool *)
fun isFal F = true
| isFal _ = false
(* isVar : form -> bool *)
fun isVar (Var _) = true
| isVar _ = false
(* isAnd : form -> bool *)
fun isAnd (_ && _) = true
| isAnd _ = false
(* isOr : form -> bool *)
fun isOr (_ || _) = true
| isOr _ = false
(* isImp : form -> bool *)
fun isImp (_ >> _) = true
| isImp _ = false
(* isBiImp : form -> bool *)
fun isBiImp ((a >> b) && (c >> d)) = a = d andalso b = c
| isBiImp _ = false
(* isVarOrFal : form -> bool *)
fun isVarOrFal a = isFal a orelse isVar a
(* formLTE : form -> form -> bool
a linear ordering on form *)
fun formLTE F _ = true
| formLTE (Var _) F = false
| formLTE (Var c) (Var c') = c <= c'
| formLTE (Var _) _ = true
| formLTE (_ >> F) F = false
| formLTE (_ >> F) (Var _) = false
| formLTE (a >> F) (a' >> F) = formLTE a a'
| formLTE (_ >> F) _ = true
| formLTE (_ && _) F = false
| formLTE (_ && _) (Var _) = false
| formLTE (_ && _) (_ >> F) = false
| formLTE (a && b) (a' && b') =
formLTE a a' andalso a <> a' orelse a = a' andalso formLTE b b'
| formLTE (_ && _) _ = true
| formLTE (_ || _) F = false
| formLTE (_ || _) (Var _) = false
| formLTE (_ || _) (_ >> F) = false
| formLTE (_ || _) (_ && _) = false
| formLTE (a || b) (a' || b') =
formLTE a a' andalso a <> a' orelse a = a' andalso formLTE b b'
| formLTE (_ || _) _ = true
| formLTE (_ >> _) F = false
| formLTE (_ >> _) (Var _) = false
| formLTE (_ >> _) (_ >> F) = false
| formLTE (_ >> _) (_ && _) = false
| formLTE (_ >> _) (_ || _) = false
| formLTE (a >> b) (a' >> b') =
formLTE a a' andalso a <> a' orelse a = a' andalso formLTE b b'
(* formSort : form list -> form list
sort a form list in ascending order, according to formLTE
(duplicates are retained) *)
fun formSort nil = nil
| formSort (x :: xs) =
let fun insertX nil = [x]
| insertX (zs as y :: ys) =
if formLTE x y
then x :: zs
else y :: insertX ys
in insertX(formSort xs) end
(* formPosition : form -> form list -> int *)
exception FormPosition (* as used below, will never be raised *)
fun formPosition (x : form) nil = raise FormPosition
| formPosition x (y :: ys) =
if x = y then 0 else 1 + formPosition x ys
(* formMember : form -> form list -> bool *)
fun formMember (x : form) nil = false
| formMember x (y :: ys) = x = y orelse formMember x ys
(* formMakeSet : form list -> form_set *)
fun formMakeSet nil = nil
| formMakeSet (x :: xs) =
if formMember x xs
then formMakeSet xs
else x :: formMakeSet xs
(* formSubset : form_set -> form_set -> bool *)
fun formSubset nil ys = true
| formSubset (x :: xs) ys = formMember x ys andalso formSubset xs ys
(* formSetEq : form_set -> form_set -> bool *)
fun formSetEq xs ys = formSubset xs ys andalso formSubset ys xs
(* formCommon : form_set -> form_set -> bool *)
fun formCommon nil ys = false
| formCommon (x :: xs) ys = formMember x ys orelse formCommon xs ys
(* formUnion : form_set -> form_set -> form_set *)
fun formUnion nil ys = ys
| formUnion (x :: xs) ys =
formUnion xs (if formMember x ys then ys else x :: ys)
(* formUnion1 : form -> form_set -> form_set *)
fun formUnion1 x ys = if formMember x ys then ys else x :: ys
(* formBigUnion : form_set list -> form_set *)
fun formBigUnion nil = nil
| formBigUnion (xs :: xss) = formUnion xs (formBigUnion xss)
(* formMinus : form_set -> form_set -> form_set *)
fun formMinus nil _ = nil
| formMinus (x :: xs) ys =
if formMember x ys
then formMinus xs ys
else x :: formMinus xs ys
(* formMinus1 : form_set -> form -> form_set
formMinus1 xs y = formMinus xs [y]; but more space-efficient *)
fun formMinus1 xs y =
if formMember y xs
then let fun minSing nil = raise CannotHappen
| minSing (x :: xs) = if x = y then xs else x :: minSing xs
in minSing xs end
else xs
(* formSetMember : form_set -> form_set list -> bool *)
fun formSetMember xs nil = false
| formSetMember xs (ys :: yss) = formSetEq xs ys orelse formSetMember xs yss
(* formSetMakeSet : form_set list -> form_set_set *)
fun formSetMakeSet nil = nil
| formSetMakeSet (xs :: xss) =
if formSetMember xs xss
then formSetMakeSet xss
else xs :: formSetMakeSet xss
(* formSetUnion : form_set_set -> form_set_set -> form_set_set *)
fun formSetUnion nil yss = yss
| formSetUnion (xs :: xss) yss =
formSetUnion xss (if formSetMember xs yss then yss else xs :: yss)
(* formSetBigUnion : form_set_set list -> form_set_set *)
fun formSetBigUnion nil = nil
| formSetBigUnion (xss :: xsss) = formSetUnion xss (formSetBigUnion xsss)
(* formSetMinimal : form_set_set -> form_set_set
select the set of minimal elements, with reference to formSubset,
of a form_set_set *)
local
fun add xs yss =
let datatype relat = GTE | LT | Incomp
fun relat nil = Incomp
| relat (ys :: yss) =
if formSubset ys xs
then GTE
else if formSubset xs ys
then LT
else relat yss
fun rmLT nil = nil
| rmLT (ys :: yss) =
if formSubset xs ys
then rmLT yss
else ys :: rmLT yss
val rel = relat yss
in if rel = GTE
then yss
else if rel = LT
then xs :: rmLT yss
else xs :: yss
end
fun mnml nil yss = yss
| mnml (xs :: xss) yss = mnml xss (add xs yss)
in
fun formSetMinimal xss = mnml xss nil
end
(* subForms : form -> form_set
generate the set of all subformulas of a formula *)
fun subForms F = [F]
| subForms (x as Var _) = [x]
| subForms (x as y >> z) =
formUnion1 x (formUnion (subForms y) (subForms z))
| subForms (x as y || z) =
formUnion1 x (formUnion (subForms y) (subForms z))
| subForms (x as y && z) =
formUnion1 x (formUnion (subForms y) (subForms z))
(***************************** Formula Printing *****************************)
(* prForm : form -> unit
print a formula on a single line, minimizing use of parentheses *)
local
fun prForm0 (e as (a >> b) && (c >> d)) =
if a = d andalso b = c
then (prForm1 a; prStr " <-> "; prForm0 b)
else prForm3 e
| prForm0 a = prForm1 a
and prForm1 (b as a >> F) = prForm4 b
| prForm1 (a >> b) = (prForm2 a; prStr " -> "; prForm1 b)
| prForm1 a = prForm2 a
and prForm2 (a || b) = (prForm3 a; prStr " | "; prForm2 b)
| prForm2 a = prForm3 a
and prForm3 (c as a && b) =
if isBiImp c
then prForm4 c
else (prForm4 a; prStr " & "; prForm3 b)
| prForm3 a = prForm4 a
and prForm4 F = prStr "f"
| prForm4 (Var c) = prStr c
| prForm4 (a >> F) = (prStr "~"; prForm4 a)
| prForm4 a = (prStr "("; prForm0 a; prStr ")")
in
val prForm = prForm0
end
(* prForms : form list -> unit
print a list of formulas on one line *)
fun prForms nil = ()
| prForms [x] = prForm x
| prForms (x :: xs) = (prForm x; prStr ", "; prForms xs)
(* prNumVarForms : string -> form list -> unit
print a list of formulas on one line, labeling each formula with
a numbered variable *)
fun prNumVarForms s xs =
let fun prNVFs i nil = ()
| prNVFs i [x] =
(prStr s; prInt i; prStr ": "; prForm x)
| prNVFs i (x :: xs) =
(prStr s; prInt i; prStr ": "; prForm x; prStr ", ";
prNVFs (i + 1) xs)
in prNVFs 0 xs end
(* prIndForms : int -> form list -> unit
print a list of formulas on multiple lines, indenting each line *)
fun prIndForms i nil = ()
| prIndForms i [x] = (indent i; prForm x)
| prIndForms i (x :: xs) = (indent i; prForm x; prStr ",\n"; prIndForms i xs)
(* prIndLabShortFormSet : int -> string -> form_set -> unit
print a set of formulas on a single line, indented and labeled *)
fun prIndLabShortFormSet i s xs =
(indent i; prStr s; prStr ": { "; prForms xs; prStr " }\n")
(* prIndLabLongFormSet : int -> string -> form_set -> unit
print a set of formulas on multiple lines, indented and labeled *)
fun prIndLabLongFormSet i s xs =
(indent i; prStr s; prStr ": { ";
if xs = nil
then ()
else if tl xs = nil
then prForm(hd xs)
else (prForm(hd xs); prStr ",\n";
prIndForms (i + size s + 4) (tl xs));
prStr " }\n")
(* prOutcome : bool -> form list * form -> unit *)
fun prOutcome b =
(if b then prStr "provable" else prStr "unprovable"; prStr ": ";
if !lambda andalso b
then prNumVarForms "x" (#1(!sequent))
else prForms (#1(!sequent));
if (#1(!sequent)) <> nil then prStr " " else ();
prStr "=> "; prForm(!conclusion); prStr "\n")
(***************************** Sequent Parsing ******************************)
(* parseSequent : string -> form list * form *)
exception SyntaxError
local
fun lex nil = nil
| lex (#"=" :: #">" :: cs) = "=>" :: lex cs
| lex (#"-" :: #">" :: cs) = "->" :: lex cs
| lex (#"<" :: #"-" :: #">" :: cs) = "<->" :: lex cs
| lex (c :: cs) =
if c = #"," orelse c = #"f" orelse c = #"~" orelse c = #"&" orelse
c = #"|" orelse c = #"(" orelse c = #")" orelse
c >= #"A" andalso c <= #"Z"
then str c :: lex cs
else if c = #" " orelse c = #"\t" orelse c = #"\n"
then lex cs
else raise SyntaxError
fun parForm0 ts =
let val (a, ts) = parForm1 ts
in case ts of
"<->" :: ts =>
let val (b, ts) = parForm0 ts
in ((a >> b) && (b >> a), ts) end
| ts => (a, ts)
end
and parForm1 ts =
let val (a, ts) = parForm2 ts
in case ts of
"->" :: ts =>
let val (b, ts) = parForm1 ts
in (a >> b, ts) end
| ts => (a, ts)
end
and parForm2 ts =
let val (a, ts) = parForm3 ts
in case ts of
"|" :: ts =>
let val (b, ts) = parForm2 ts
in (a || b, ts) end
| ts => (a, ts)
end
and parForm3 ts =
let val (a, ts) = parForm4 ts
in case ts of
"&" :: ts =>
let val (b, ts) = parForm3 ts
in (a && b, ts) end
| ts => (a, ts)
end
and parForm4 nil = raise SyntaxError
| parForm4 ("f" :: ts) = (F, ts)
| parForm4 ("~" :: ts) =
let val (a, ts) = parForm4 ts
in (a >> F, ts) end
| parForm4 ("(" :: ts) =
let val (a, ts) = parForm0 ts
in case ts of
")" :: ts => (a, ts)
| _ => raise SyntaxError
end
| parForm4 (t :: ts) =
if size t = 1 andalso t >= "A" andalso t <= "Z"
then (Var t, ts)
else raise SyntaxError
val parForm = parForm0
fun parNonZeroForms xs ts =
let val (a, ts) = parForm ts
val xs = xs @ [a]
in case ts of
"," :: ts => parNonZeroForms xs ts
| _ => (xs, ts)
end
fun parForms (ts as "=>" :: _) = (nil, ts)
| parForms ts = parNonZeroForms nil ts
in
fun parseSequent s =
let val (xs, ts) = parForms(lex(explode s))
in case ts of
"=>" :: ts =>
let val (a, ts) = parForm ts
in if ts = nil then (xs, a) else raise SyntaxError end
| _ => raise SyntaxError
end
end
(************************** Deducibility Relation ***************************)
(* deducible : form_set -> form_set -> bool
check whether the second form_set is deducible from the first form_set *)
local
fun deduc xs ys =
let (* non-invertible right rule *)
fun right3 xs y's nil = false
| right3 xs y's ((y as a >> b) :: ys) =
deduc (formUnion1 a xs) [b] orelse right3 xs (y :: y's) ys
| right3 xs y's (y :: ys) = right3 xs (y :: y's) ys
(* semi-invertible left rule *)
fun left2 x's nil ys =
right3 x's nil ys
| left2 x's ((x as (a >> b) >> c) :: xs) ys =
let val x''s = x's @ xs
in deduc (formUnion1 c x''s) ys andalso
(deduc (formUnion1 (b >> c) x''s) [a >> b] orelse
left2 (x :: x's) xs ys)
end
| left2 x's (x :: xs) ys =
left2 (x :: x's) xs ys
(* invertible left rules *)
fun left1 x's nil ys =
left2 nil x's ys
| left1 x's ((a && b) :: xs) ys =
deduc (formUnion1 b (formUnion1 a (x's @ xs))) ys
| left1 x's ((a || b) :: xs) ys =
let val x''s = x's @ xs
in deduc (formUnion1 a x''s) ys andalso
deduc (formUnion1 b x''s) ys
end
| left1 x's ((x as F >> a) :: xs) ys =
if !minimal andalso (formMember F x's orelse formMember F xs)
then deduc (formUnion1 a (x's @ xs)) ys
else left1 (x :: x's) xs ys
| left1 x's ((x as (a as Var _) >> b) :: xs) ys =
if formMember a x's orelse formMember a xs
then deduc (formUnion1 b (x's @ xs)) ys
else left1 (x :: x's) xs ys
| left1 x's ((a && b >> c) :: xs) ys =
deduc (formUnion1 (a >> b >> c) (x's @ xs)) ys
| left1 x's ((a || b >> c) :: xs) ys =
deduc (formUnion1 (b >> c) (formUnion1 (a >> c) (x's @ xs)))
ys
| left1 x's (x :: xs) ys =
left1 (x :: x's) xs ys
(* invertible right rules *)
fun right2 xs y's nil = left1 nil xs y's
| right2 xs y's ((a && b) :: ys) =
let val y''s = y's @ ys
in deduc xs (formUnion1 a y''s) andalso
deduc xs (formUnion1 b y''s)
end
| right2 xs y's ((a || b) :: ys) =
deduc xs (formUnion1 b (formUnion1 a (y's @ ys)))
| right2 xs y's (y :: ys) = right2 xs (y :: y's) ys
(* invertible right rule (in special cases) *)
fun right1 xs [a >> b] = deduc (formUnion1 a xs) [b]
| right1 xs ys = right2 xs nil ys
in not(!minimal) andalso formMember F xs orelse
formCommon xs ys orelse
right1 xs ys
end
in
fun deducible xs ys =
let val _ =
if !trace
then (prStr "[deducible\n";
prIndLabLongFormSet 4 "left" (formSort xs);
prIndLabLongFormSet 4 "right" (formSort ys))
else ()
val b = deduc xs ys
val _ =
if !trace
then (indent 4; if b then prStr "true" else prStr "false";
prStr "\n]\n")
else ()
in b end
end
(******************************** Deductions ********************************)
(* all formulas occurring in a deduction are elements of the formula
universe *)
datatype deduct =
Ass of int (* assumption number; initially ~1 *)
* form (* assumption *)
| AndIn of deduct (* left premiss *)
* deduct (* right premiss *)
| AndEl1 of deduct (* premiss *)
| AndEl2 of deduct (* premiss *)
| OrIn1 of form (* rhs of conclusion *)
* deduct (* premiss *)
| OrIn2 of form (* lhs of conclusion *)
* deduct (* premiss *)
| OrEl of int (* discharged assumption number; initially ~1; used *)
(* for both discharged assumptions *)
* form (* assumption discharged in left minor premiss *)
* form (* assumption discharged in right minor premiss *)
* deduct (* major premiss *)
* deduct (* left minor premiss *)
* deduct (* right minor premiss *)
| ImpIn of int (* discharged assumption number; initially ~1 *)
* form (* assumption dischanged in premiss *)
* deduct (* premiss *)
| ImpEl of deduct (* major premiss *)
* deduct (* minor premiss *)
| FalEl of form (* conclusion *)
* deduct (* premiss *)
(* numberDeduct : deduct -> deduct
number a deduction, replacing the initial dummy assumption numbers (~1) *)
local
fun labelAss (p as Ass(_, a)) c m = if a = c then Ass(m, a) else p
| labelAss (AndIn(p, q)) c m =
AndIn(labelAss p c m, labelAss q c m)
| labelAss (AndEl1 p) c m = AndEl1(labelAss p c m)
| labelAss (AndEl2 p) c m = AndEl2(labelAss p c m)
| labelAss (OrIn1(a, p)) c m = OrIn1(a, labelAss p c m)
| labelAss (OrIn2(a, p)) c m = OrIn2(a, labelAss p c m)
| labelAss (OrEl(n, a, b, p, q, r)) c m =
OrEl(n, a, b,
labelAss p c m,
if a = c then q else labelAss q c m,
if b = c then r else labelAss r c m)
| labelAss (ImpIn(n, a, p)) c m =
ImpIn(n, a, if a = c then p else labelAss p c m)
| labelAss (ImpEl(p, q)) c m =
ImpEl(labelAss p c m, labelAss q c m)
| labelAss (FalEl(a, p)) c m = FalEl(a, labelAss p c m)
fun numDed (Ass(_, a)) m = (Ass(~1, a), m)
| numDed (AndIn(p, q)) m =
let val (p, m) = numDed p m
val (q, m) = numDed q m
in (AndIn(p, q), m) end
| numDed (AndEl1 p) m =
let val (p, m) = numDed p m
in (AndEl1 p, m) end
| numDed (AndEl2 p) m =
let val (p, m) = numDed p m
in (AndEl2 p, m) end
| numDed (OrIn1(a, p)) m =
let val (p, m) = numDed p m
in (OrIn1(a, p), m) end
| numDed (OrIn2(a, p)) m =
let val (p, m) = numDed p m
in (OrIn2(a, p), m) end
| numDed (OrEl(_, a, b, p, q, r)) m =
let val (p, m) = numDed p m
val (q, m) = numDed q m
val (r, m) = numDed r m
val q = labelAss q a m
val r = labelAss r b m
in (OrEl(m, a, b, p, q, r), m + 1) end
| numDed (ImpIn(_, a, p)) m =
let val (p, m) = numDed p m
val p = labelAss p a m
in (ImpIn(m, a, p), m + 1) end
| numDed (ImpEl(p, q)) m =
let val (p, m) = numDed p m
val (q, m) = numDed q m
in (ImpEl(p, q), m) end
| numDed (FalEl(a, p)) m =
let val (p, m) = numDed p m
in (FalEl(a, p), m) end
in
fun numberDeduct p = #1(numDed p 0)
end
(* prDeduct : deduct -> unit
print an already numbered deduction *)
local
fun prDed (Ass(n, a)) i =
(indent i;
if n = ~1
then prStr "Ass: "
else (prStr "("; prInt n; prStr ") ");
prForm a; prStr "\n"; a)
| prDed (AndIn(p, q)) i =
let val a = prDed p (i + 4)
val b = prDed q (i + 4)
val c = a && b
in indent i; prStr "&I: "; prForm c; prStr "\n"; c end
| prDed (AndEl1 p) i =
let val a = prDed p (i + 4)
in case a of
b && _ =>
(indent i; prStr "&E1: "; prForm b; prStr "\n"; b)
| _ => raise CannotHappen
end
| prDed (AndEl2 p) i =
let val a = prDed p (i + 4)
in case a of
_ && b =>
(indent i; prStr "&E2: "; prForm b; prStr "\n"; b)
| _ => raise CannotHappen
end
| prDed (OrIn1(a, p)) i =
let val b = prDed p (i + 4)
val c = b || a
in indent i; prStr "|I1: "; prForm c; prStr "\n"; c end
| prDed (OrIn2(a, p)) i =
let val b = prDed p (i + 4)
val c = a || b
in indent i; prStr "|I2: "; prForm c; prStr "\n"; c end
| prDed (OrEl(n, a, b, p, q, r)) i =
let val _ = prDed p (i + 4)
val c = prDed q (i + 4)
val _ = prDed r (i + 4)
in indent i; prStr "|E ("; prInt n; prStr "): ";
prForm c; prStr "\n"; c
end
| prDed (ImpIn(n, a, p)) i =
let val b = prDed p (i + 4)
val c = a >> b
in indent i; prStr "->I ("; prInt n; prStr "): ";
prForm c; prStr "\n"; c
end
| prDed (ImpEl(p, q)) i =
let val a = prDed p (i + 4)
val b = prDed q (i + 4)
in case a of
_ >> c =>
(indent i; prStr "->E: "; prForm c; prStr "\n"; c)
| _ => raise CannotHappen
end
| prDed (FalEl(a, p)) i =
(prDed p (i + 4); indent i; prStr "fE: "; prForm a; prStr "\n"; a)
in
fun prDeduct p = (prDed (numberDeduct p) 0; ())
end
exception PrDeductLambda (* as used below, will never be raised *)
(* prDeductLambda : deduct -> form list -> unit
print an already numbered deduction as a lambda term; an undischarged
assumption is named xj, where j is the position of the first occurrence
of the assumption in the form list; a discharged assumption is named yj,
where j is the assumption's number *)
local
fun prLam (Ass(n, a)) xs i =
(indent i;
if n = ~1
then (prStr "x";
prInt(formPosition a xs
handle _ => raise PrDeductLambda))
else (prStr "y"; prInt n);
prStr "\n")
| prLam (AndIn(p, q)) xs i =
(indent i; prStr "pair\n"; prLam p xs (i + 4); prLam q xs (i + 4))
| prLam (AndEl1 p) xs i =
(indent i; prStr "out1\n"; prLam p xs (i + 4))
| prLam (AndEl2 p) xs i =
(indent i; prStr "out2\n"; prLam p xs (i + 4))
| prLam (OrIn1(a, p)) xs i =
(indent i; prStr "in1 "; prForm a; prStr "\n"; prLam p xs (i + 4))
| prLam (OrIn2(a, p)) xs i =
(indent i; prStr "in2 "; prForm a; prStr "\n"; prLam p xs (i + 4))
| prLam (OrEl(n, a, b, p, q, r)) xs i =
(indent i; prStr "case "; prStr "y"; prInt n; prStr ": ";
prForm a; prStr ", "; prForm b; prStr "\n";
prLam p xs (i + 4); prLam q xs (i + 4); prLam r xs (i + 4))
| prLam (ImpIn(n, a, p)) xs i =
(indent i; prStr "lambda y"; prInt n; prStr ": "; prForm a;
prStr "\n"; prLam p xs (i + 4))
| prLam (ImpEl(p, q)) xs i =
(indent i; prStr "app\n"; prLam p xs (i + 4); prLam q xs (i + 4))
| prLam (FalEl(a, p)) xs i =
(indent i; prStr "falsity "; prForm a; prStr "\n"; prLam p xs (i + 4))
in
fun prDeductLambda p xs = prLam (numberDeduct p) xs 0
end
(*************************** Annotated Deductions ***************************)
(* all formulas occurring in an annotated deduction are elements of the
formula universe *)
type a_d =
int (* stage *)
* int (* size *)
* bool (* true iff there is a segment ending with the conclusion *)
(* of this rule and beginning with an intro or false elim rule *)
* form_set (* assumptions of deduction *)
* form (* formula proved *)
* deduct (* deduction of formula *)
(* aDStage : a_d -> int *)
fun aDStage((n, _, _, _, _, _) : a_d) = n
(* aDSize : a_d -> int *)
fun aDSize((_, i, _, _, _, _) : a_d) = i
(* aDDeduct : a_d -> deduct *)
fun aDDeduct((_, _, _, _, _, p) : a_d) = p
(* aDLTE : a_d -> a_d -> bool
when the first a_d is as good as the second a_d *)
fun aDLTE ((l, i, f, xs, a, _) : a_d) ((m, j, g, ys, b, _) : a_d) =
(g orelse not f) andalso
i <= j andalso
a = b andalso
formSubset xs ys
(* aDAdd : bool ref -> a_d -> a_d list -> a_d list
add an a_d to a list of a_d's if the list doesn't already contain an
a_d that is as good; old a_d's that are worse than the new one are
discarded; the bool variable is set to true iff the resulting a_d list
is different from the original one *)
fun aDAdd chgd s ts =
let datatype relat = GTE | LT | Incomp
fun relat nil = Incomp
| relat (t :: ts) =
if aDLTE t s
then GTE
else if aDLTE s t
then LT
else relat ts
fun rmLT nil = nil
| rmLT (t :: ts) =
if aDLTE s t
then rmLT ts
else t :: rmLT ts
val rel = relat ts
in if rel = GTE
then ts
else if rel = LT
then let val t's = rmLT ts
in chgd := true;
if !trace
then (indent 4; prStr "aDs improved: ";
prInt(length ts - length t's); prStr "\n")
else ();
s :: t's
end
else (chgd := true; s :: ts)
end
(* solutions : a_d list -> a_d list
select the elements of an a_d list that prove the sequent's conclusion
from its assumptions *)
fun solutions (aDs : a_d list) : a_d list =
filter (fn (_, _, _, ys, b, _) =>
b = !conclusion andalso formSubset ys (!assumptions))
aDs
(* bestSolution : a_d list -> a_d
select a minimally sized solution from a list of solutions; raises
BestSolution if the list of solutions is empty (this will never
happen) *)
exception BestSolution (* as used below, will never be raised *)
fun bestSolution aDs =
let fun bestSoln s nil = s
| bestSoln s (t :: ts) =
if aDSize t < aDSize s
then bestSoln t ts
else bestSoln s ts
in if aDs = nil
then raise BestSolution
else bestSoln (hd aDs) (tl aDs)
end
(* deduction : unit -> deduct
find a minimally sized, normal deduction of the sequent *)
local
fun andIn st add (_, i, _, xs, a, p) (_, j, _, ys, b, q) =
let val c = a && b
in if formMember c (!universe)
then add(st, i + j + 1, true, formUnion xs ys, c, AndIn(p, q))
else ()
end
fun andEl st add (_, i, f, xs, a, p) =
if f
then ()
else case a of
b && c =>
(add(st, i + 1, false, xs, b, AndEl1 p);
add(st, i + 1, false, xs, c, AndEl2 p))
| _ => ()
fun orIn st add (_, i, _, xs, a, p) =
appOpp (!universe) (fn b =>
case b of
c || d =>
(if c = a
then add(st, i + 1, true, xs, b, OrIn1(d, p))
else ();
if d = a
then add(st, i + 1, true, xs, b, OrIn2(c, p))
else ())
| _ => ())
fun orEl st aDs add (l, i, f, xs, a, p) (m, j, g, ys, b, q) =
if a = b
then appOpp aDs (fn (n, k, h, zs, c, r) =>
(if not h andalso
(l = st - 1 orelse m = st - 1 orelse n = st - 1)
then case c of
d || e =>
if formMember d xs andalso formMember e ys
then let val xs' = formMinus1 xs d
val ys' = formMinus1 ys e
val ws = formUnion zs (formUnion xs' ys')
in add(st, i + j + k + 1, f orelse g,
ws, a, OrEl(~1, d, e, r, p, q))
end
else ()
| _ => ()
else ()))
else ()
fun impIn st add (_, i, _, xs, a, p) =
appOpp (!universe) (fn b =>
case b of
c >> d =>
if d = a
then add(st, i + 1, true, formMinus1 xs c, b, ImpIn(~1, c, p))
else ()
| _ => ())
fun impEl st add (_, i, f, xs, a, p) (_, j, _, ys, d, q) =
if f
then ()
else case a of
b >> c =>
if b = d
then add(st, i + j + 1, false, formUnion xs ys, c,
ImpEl(p, q))
else ()
| _ => ()
fun falEl st add (_, i, _, xs, a, p) =
if a = F
then appOpp (!universe) (fn b =>
add(st, i + 1, true, xs, b, FalEl(b, p)))
else ()
fun tracing aDs =
(indent 4; prStr "aDs: "; prInt(length aDs);
if solutions(aDs) <> nil then prStr " (found)" else ();
prStr "\n")
fun iter st aDs =
let val chgd = ref false
val newADs = ref aDs
fun add s = newADs := aDAdd chgd s (!newADs)
in appOpp aDs (fn s =>
(if aDStage s = st - 1
then (if (!areAnd) then andEl st add s else ();
if (!areOr) then orIn st add s else ();
if (!areImp) then impIn st add s else ();
if not(!minimal) andalso (!areFal)
then falEl st add s
else ())
else ();
appOpp aDs (fn t =>
(if aDStage s = st - 1 orelse aDStage t = st - 1
then (if (!areAnd) then andIn st add s t else ();
if (!areImp) then impEl st add s t else ())
else ();
if (!areOr) then orEl st aDs add s t else ()))));
if !trace then tracing(!newADs) else ();
if !chgd then iter (st + 1) (!newADs) else aDs
end
in
fun deduction() =
let val _ = if !trace then prStr "[deduction\n" else ()
val aDs = map (fn a => (0, 1, false, [a], a, Ass(~1, a)))
(!universe)
val _ = if !trace then tracing aDs else ()
val aDs = iter 1 aDs
val p = aDDeduct(bestSolution(solutions(aDs)))
val _ = if !trace then prStr "]\n" else ()
in p end
end
(************************* Countermodel Construction ************************)
(* all of the form_set's produced/consumed by the functions of this
section are subsets of the formula universe *)
(* closure : form_set -> form_set
deductively close a form_set *)
fun closure xs =
xs @ filter (fn a => deducible xs [a]) (formMinus (!universe) xs)
(* unHandledImps : form_set -> form_set
find the implications that are not handled by a deductively closed
form_set, where an implication is handled by a closed form_set iff
either the formula or its lhs is included in the form_set *)
fun unHandledImps xs =
filter (fn a >> _ => not(formMember a xs)
| _ => false)
(formMinus (!universe) xs)
(* tryHandleImps : form_set -> form_set -> form_set
add implications to the first form_set, handling as many
implications as possible, while still failing to deduce the second
form_set *)
fun tryHandleImps xs ys =
let val xs = closure xs
val imps = unHandledImps xs
val _ =
if !trace
then (prStr "[tryHandleImps (1)\n";
prIndLabLongFormSet 4 "closure" (formSort xs);
prIndLabLongFormSet 4 "unhandled" (formSort imps);
prStr "]\n")
else ()
fun consistent zs = not(deducible (formUnion zs xs) ys)
fun tryAddImp zss (a as b >> _) =
let fun tryAdd nil = zss
| tryAdd (zs :: zss) =
let val vs = formUnion1 a zs
val ws = formUnion1 b zs
in if consistent vs
then if consistent ws
then vs :: ws :: tryAdd zss
else vs :: tryAdd zss
else if consistent ws
then ws :: tryAdd zss
else tryAdd zss
end
in tryAdd zss end
| tryAddImp zss _ = raise CannotHappen
fun tryAddImps zss nil = zss
| tryAddImps zss (v :: vs) = tryAddImps (tryAddImp zss v) vs
fun numHandled vs =
sumIntList(map (fn a as b >> _ =>
if formMember a vs orelse formMember b vs
then 1
else 0
| _ => raise CannotHappen)
imps)
fun best zss =
let fun bst n vs nil = vs
| bst n vs (zs :: zss) =
let val m = numHandled zs
in if m > n
then bst m zs zss
else bst n vs zss
end
in bst (numHandled(hd zss)) (hd zss) (tl zss) end
val vss = tryAddImps [nil] imps
val vs = best vss
val zs = formUnion vs xs
val _ =
if !trace
then (prStr "[tryHandleImps (2)\n";
indent 4; prStr "choices: "; prInt(length vss);
prStr "\n";
prIndLabLongFormSet 4 "added" (formSort vs);
prIndLabLongFormSet 4 "result" (formSort zs))
else ()
in zs end
(* a prime_theory is a form_set xs such that
(a) xs doesn't contain falsity (except in the case of minimal logic);
(b) if a nonempty subset ys of the universe is deducible from xs,
then some element of ys is in xs
a prime_theory_set is a form_set_set whose elements are prime_theory's
a countermodel (of the sequent) is a prime_theory_set xss such that
(a) xss (viewed as a poset, ordered by inclusion) has a least element
that contains the assumptions but not the conclusion of the sequent;
(b) if xs is in xss and a >> b is in the universe but is not in xs,
then there is a ys in xss that contains a and everything in xs
but does not contain b;
(c) only xss's least element lacks the conclusion *)
type prime_theory = form_set
type prime_theory_set = form_set_set
type countermodel = prime_theory_set
(* primeTheory : form_set -> form_set -> prime_theory
build a prime_theory from the first form_set, handling as many implications
as possible, while still failing to prove the second form_set *)
fun primeTheory xs ys =
let val _ =
if !trace
then (prStr "[primeTheory (1)\n";
prIndLabLongFormSet 4 "include" (formSort xs);
prIndLabLongFormSet 4 "exclude" (formSort ys);
prStr "]\n")
else ()
fun tryAdd vs nil = vs
| tryAdd vs (z :: zs) =
let val ws = formUnion1 z vs
in tryAdd (if deducible ws ys then vs else ws) zs end
val xs = tryHandleImps xs ys
val possAdds = formMinus (formMinus (!universe) ys) xs
val xs = tryAdd xs possAdds
val _ =
if !trace
then (prStr "[primeTheory (2)\n";
prIndLabLongFormSet 4 "result" (formSort xs);
prIndLabLongFormSet 4 "unhandled"
(formSort(unHandledImps xs));
prStr "]\n")
else ();
in xs end
(* succTheories : prime_theory -> prime_theory_set
given a prime_theory xs, generate a minimal number of prime_theory's
extending xs, such that, for each implication a >> b in the universe that
is not handled by xs, one of these prime_theory's contains a but does not
contain b *)
fun succTheories xs =
let val imps = unHandledImps xs
val _ =
if !trace
then (prStr "[succTheories (1)\n";
prIndLabLongFormSet 4 "include" (formSort xs);
prIndLabLongFormSet 4 "unhandled" (formSort imps))
else ()
fun left nil = nil
| left ((a >> _) :: vs) = formUnion1 a (left vs)
| left _ = raise CannotHappen
fun right nil = nil
| right ((_ >> a) :: vs) = formUnion1 a (right vs)
| right _ = raise CannotHappen
fun consistent vs =
not(deducible (formUnion (left vs) xs) (right vs))
fun succ vs = primeTheory (formUnion (left vs) xs) (right vs)
fun addImpToPartition zss a =
let fun add vss nil = nil
| add vss (zs :: zss) =
if consistent(a :: zs)
then ((a :: zs) :: (vss @ zss)) ::
add (zs :: vss) zss
else add (zs :: vss) zss
in ([a] :: zss) :: add nil zss end
fun addImpToPartitions nil a = nil
| addImpToPartitions (zss :: zsss) a =
addImpToPartition zss a @ addImpToPartitions zsss a
fun addImpsToPartitions zsss nil = zsss
| addImpsToPartitions zsss (v :: vs) =
addImpsToPartitions (addImpToPartitions zsss v) vs
fun best zsss =
let fun bst n vss nil = vss
| bst n vss (zss :: zsss) =
let val m = length zss
in if m < n
then bst m zss zsss
else bst n vss zsss
end
in bst (length(hd zsss)) (hd zsss) (tl zsss) end
fun tracing i nil = ()
| tracing i (vs :: vss) =
(prIndLabLongFormSet 4 (numeral i) (formSort vs);
tracing (i + 1) vss)
val zsss = addImpsToPartitions [nil] imps
val zss = best zsss
val _ =
if !trace
then (prStr "[succTheories (2)\n";
indent 4; prStr "choices: "; prInt(length zsss);
prStr "\n"; indent 4; prStr "partition:\n";
tracing 0 zss; prStr "]\n")
else ()
val vss = map succ zss (* this will be a form_set_set *)
val _ =
if !trace
then (prStr "[succTheories (3)\n";
indent 4; prStr "successors: "; prInt(length vss);
prStr "\n"; tracing 0 vss; prStr "]\n")
else ()
in vss end
(* countermodel : unit -> countermodel
generate a countermodel of the sequent; a one-theory countermodel
will be produced if possible *)
fun countermodel() =
let val least = primeTheory (!assumptions) [!conclusion]
fun pTs vss nil = vss
| pTs vss (zs :: zss) =
if formSetMember zs vss
then pTs vss zss
else pTs (zs :: vss) (succTheories zs @ zss)
in pTs nil [least] end
(* a prime_theory_tree is a mixed-arity tree whose nodes are labeled by
prime_theory's, and where the label of a child is always a strictly
bigger prime_theory than the label of its parent
a tree_model is a prime_theory_tree such that if xs is a node's label
and a >> b is an implication in the universe that isn't in xs, then there
is a descendent of the node whose label contains a but not b
a tree_countermodel (of the sequent) is a tree_model such that the
root node's label contains the assumptions but not the conclusion
of the sequent, and only the root node has a label that lacks the
conclusion *)
datatype prime_theory_tree = Node of prime_theory * prime_theory_tree list
type tree_model = prime_theory_tree
type tree_countermodel = tree_model
(* countermodelToTreeCountermodel : countermodel -> tree_countermodel
convert a countermodel into a tree_countermodel; if the countermodel
has only one element, then the tree_countermodel will have only one
node *)
fun countermodelToTreeCountermodel vss =
let val least =
case formSetMinimal vss of
[us] => us
| _ => raise CannotHappen
fun succs us =
let fun isSucc vs =
formSubset us vs andalso not(formSubset vs us)
in formSetMinimal(filter isSucc vss) end
fun model us = Node(us, map model (succs us))
in model least end
(* prPrimeTheoryTree : prime_theory_tree -> int -> unit
print a prime_theory_tree at a specified level of indentation, numbering
the tree's nodes in the order that they would be reached in a preorder
traversal of the tree *)
fun prPrimeTheoryTree p i =
let fun prNode (Node(us, ps)) i n =
let val m = prNodes ps (i + 4) (n + 1)
val us = formSort us
in if !verbose
then prIndLabLongFormSet i (numeral n) us
else prIndLabShortFormSet i (numeral n)
(filter isVarOrFal us);
m
end
and prNodes nil i n = n
| prNodes (p :: ps) i n = prNodes ps i (prNode p i n)
in prNode p i 0; () end
(* topLevelOK : prime_theory_tree -> bool
is it the case that, for every unhandled implication a >> b of the label
of the root node of a prime_theory_tree, that there is a descendant node
whose label contains a but not b? *)
fun topLevelOK(Node(us, ps)) =
let fun rejectedWithin (a >> b) p =
let fun rejWithin(Node(us, ps)) =
formMember a us andalso not(formMember b us) orelse
List.exists rejWithin ps
in rejWithin p end
| rejectedWithin _ _ = raise CannotHappen
in all (fn a => List.exists (fn p => rejectedWithin a p)
ps)
(unHandledImps us)
end
(* rmRedundantNode : tree_countermodel -> tree_countermodel list
find all of the tree_countermodels that can be formed by removing
a single ("redundant") non-root node from a countermodel (the node's
children would become children of the node's parent) *)
fun rmRedundantNode p =
let fun rmNodeFromChildOfNode(Node(us, qs)) =
filter topLevelOK
(map (fn rs => Node(us, rs)) (rmNodeFromNodes nil qs))
and rmNodeFromNodes ps nil = nil
| rmNodeFromNodes ps ((s as Node(_, qs)) :: rs) =
(ps @ qs @ rs) ::
map (fn q => ps @ (q :: rs)) (rmNodeFromChildOfNode s) @
rmNodeFromNodes (ps @ [s]) rs
in rmNodeFromChildOfNode p end
(* rmRedundantNodes : tree_countermodel -> tree_countermodel
apply rmRedundantNode to a tree_countermodel repeatedly, until a
tree_countermodel is produced with no redundant non-root nodes *)
fun rmRedundantNodes p =
let fun rmNodes p =
case rmRedundantNode p of
nil => p
| p :: _ => rmNodes p
val _ =
if !trace
then (prStr "[rmRedundantNodes\n"; indent 4;
prStr "old model:\n"; prPrimeTheoryTree p 4)
else ()
val q = rmNodes p
val _ = if !trace then prStr "]\n" else ()
in q end
(***************************** Main Processing ******************************)
(* main : unit -> unit *)
fun main() =
let val _ =
(sequent := parseSequent(!sequentStr);
assumptions := formMakeSet(#1(!sequent));
conclusion := #2(!sequent);
universe :=
formSort(formBigUnion(map subForms
(!conclusion :: !assumptions)));
areFal := List.exists isFal (!universe);
areAnd := List.exists isAnd (!universe);
areOr := List.exists isOr (!universe);
areImp := List.exists isImp (!universe);
if !trace
then prIndLabLongFormSet 0 "universe" (!universe)
else ())
val isDeduc = deducible (!assumptions) [!conclusion]
in prOutcome isDeduc;
if not(!check)
then (prStr "\n";
if isDeduc
then let val p = deduction()
in if !lambda
then prDeductLambda p (#1(!sequent))
else prDeduct p
end
else let val uss = countermodel()
val p = countermodelToTreeCountermodel uss
val p = rmRedundantNodes p
in prPrimeTheoryTree p 0 end)
else ()
end
(************************* Support for Entry Point **************************)
(* helpMessage : unit -> string *)
fun helpMessage() =
"Porgi Version " ^ version ^ "\n\n\
\Usage: " ^ !program ^ " [OPTION]... sequent\n\n\
\ -m, --minimal use minimal logic\n\
\ -c, --check just check deducibility\n\
\ -l, --lambda output lambda term instead of deduction\n\
\ -v, --verbose output verbose results\n\
\ -t, --trace output tracing information\n\
\ -h, --help output this information and exit\n\n\
\Note: \"sequent\" must be a single argument, and should have the\
\ form\n\n\
\ form, ..., form => form\n\n\
\where each \"form\" is a propositional formula built up using\
\ parentheses,\n\
\whitespace and the following symbols:\n\n\
\ f (falsity)\n\
\ A-Z (propositional variables)\n\
\ ~ (negation) highest precedence\n\
\ & (conjunction) . right associative\n\
\ | (disjunction) . right associative\n\
\ -> (implication) . right associative\n\
\ <-> (biimplication) lowest precedence right associative"
(* errorHelp : unit -> 'a *)
fun errorHelp() = error(helpMessage())
(* normalHelp : unit -> 'a *)
fun normalHelp() = (prStr(helpMessage()); prStr "\n"; exit OS.Process.success)
(* procLongOpt : string -> unit
process a long command line option *)
fun procLongOpt "minimal" = minimal := true
| procLongOpt "check" = check := true
| procLongOpt "lambda" = lambda := true
| procLongOpt "verbose" = verbose := true
| procLongOpt "trace" = trace := true
| procLongOpt "help" = normalHelp()
| procLongOpt _ = errorHelp()
(* procShortOpt : char -> unit
process a one-character command line option *)
fun procShortOpt #"m" = minimal := true
| procShortOpt #"c" = check := true
| procShortOpt #"l" = lambda := true
| procShortOpt #"v" = verbose := true
| procShortOpt #"t" = trace := true
| procShortOpt #"h" = normalHelp()
| procShortOpt _ = errorHelp()
(* procShortOpts : char list -> unit
process a list of one character command line options *)
fun procShortOpts nil = errorHelp()
| procShortOpts [c] = procShortOpt c
| procShortOpts (c :: cs) = (procShortOpt c; procShortOpts cs)
(* processArgs : string list -> unit
process command line arguments *)
fun processArgs nil = if !sequentStr = "" then errorHelp() else ()
| processArgs (arg :: args) =
(case explode arg of
#"-" :: #"-" :: cs => procLongOpt(implode cs)
| #"-" :: cs => procShortOpts cs
| _ =>
if !sequentStr = "" then sequentStr := arg else errorHelp();
processArgs args)
(* prCPUTime : unit -> unit
print elapsed cpu time *)
fun prCPUTime timer =
let val {nongc, gc} = Timer.checkCPUTimes timer
val nongc = #usr nongc
val gc = #usr gc
val total = Time.+(nongc, gc)
fun prTime time = prStr(Time.toString time)
in prStr "["; prTime total; prStr " sec user cpu time (";
prTime nongc; prStr " sec non-gc, "; prTime gc; prStr " sec gc)]\n"
end
in (* END OF LOCAL PART; to find beginning, search for *)
(* "BEGINNING OF LOCAL PART" *)
(************************ Entry Point of Executable *************************)
(* entryPoint : string * string list -> 'b *)
fun entryPoint(pgm, args) =
(program := pgm;
processArgs args;
let val timer = Timer.startCPUTimer()
in main()
handle SyntaxError =>
error(!program ^ ": syntax error in \"" ^
!sequentStr ^ "\"")
| _ => error(!program ^ ": internal error");
prStr "\n"; prCPUTime timer; exit OS.Process.success
end)
end;
entryPoint(CommandLine.name(), CommandLine.arguments());