(****************************************************************************
 ********************************  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;

val _ : unit = entryPoint(CommandLine.name(), CommandLine.arguments());