(****************************************************************************
 ********************************  kripke.sml  *******************************
 ****************************************************************************)

(* Kripke: a Countermodel Checker for Intuitionistic Propositional Logic
   (Version -- September 2007)

   Christian Haack
   Department of Computing and Information Sciences
   Kansas State University
   234 Nichols Hall
   Manhattan, KS 66506, USA
   haack@cis.ksu.edu

   Kripke is set up to be compiled using MLton - type mlton kripke.sml
   to create the executable "kripke"

   The use of the command that is created by this program is explained 
   in the paper "Kripke: a Countermodel Checker for Intuitionistic 
   Propositional Logic", which can be obtained via WWW URL
   
                  http://alleystoughton.us/kripke/
   
   Parts of this code are taken from Alley Stoughton's Proof Or Refutation 
   Generator for Intuitionistic propositional logic, Porgi, which can be found
   on http://alleystoughton.us/porgi/ *)

local  (* BEGINNING OF LOCAL PART; to find end, search for *)
       (* "END OF LOCAL PART"                              *)

(********************** Miscellaneous Definitions ***************************)
                                
exception CannotHappen (* used to avoid warning messages *)

(* implies : bool * bool -> bool *)

fun implies(p,q) = (not p) orelse q

(* forall : 'a list -> ('a -> bool) -> bool *)

fun forall  nil      p = true
  | forall (x :: xs) p = p(x) andalso (forall xs p);

(* numeral : int -> string converts 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

(* letter: string -> bool *)

fun letter(x) =        (#"a" <= x andalso x <= #"z") 
                orelse (#"A" <= x andalso x <= #"Z")
                orelse (#"0" <= x andalso x <= #"9");

(* Letter: string -> bool *)

fun Letter(x) =        (#"A" <= x andalso x <= #"Z")
                orelse (#"0" <= x andalso x <= #"9");

(* charMember : string -> string list -> bool *)

fun charMember (x : char) nil       = false
  | charMember x          (y :: ys) = x = y orelse charMember x ys

(* prStr : string -> unit *)

fun prStr s = TextIO.output(TextIO.stdOut, s)

(* indent : int -> unit *)

fun indent 0 = ()
  | indent n = (prStr " "; indent(n - 1))

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

(* prNames: string list -> unit *)

fun prNames nil       = ()
  | prNames [x]       = (prStr "\""; prStr x; prStr "\"")
  | prNames (x :: xs) = (prNames [x]; prStr ", "; prNames xs)

(* copies : int -> string -> string *)

fun copies 0 _ = ""
  | copies n s = s ^ copies (n - 1) s

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

(* get : string -> string *)

fun get(s) =
 let val is = TextIO.openIn(s) 
     fun g(s,is) =
           if TextIO.endOfStream(is)
           then (TextIO.closeIn(is); explode(s))
           else g(s ^ TextIO.inputN(is,1), is)
 in g("",is) 
 end  

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 *)
  | &&  of form * form  (* conjunction *)
  | ||  of form * form  (* disjunction *)
  | >>  of form * form  (* implication *)

(***************************** Global Variables *****************************)

val program    = ref ""  (* name of executable; set by entryPoint *)
val fileStr    = ref ""  (* name of file that contains tree; *)
                         (* set by processArgs *) 
val sequentStr = ref ""  (* single succedent sequent in string form; *)
                         (* set by processArgs *)

(* options; set by processArgs *)

datatype option = Check  (* output whether sequent holds at root or not *)
                | Find   (* output one maximal node at which sequent doesn't *)
                         (* hold *)
                | List   (* list all maximal nodes at which sequent doesn't *)
                         (* hold *)

val a   = ref false  (* output annotated tree *)
val h   = ref false  (* output help information *)
val m   = ref false  (* use minimal logic (treat falsity like prop var) *)
val opt = ref Check  

(************************* Formula-related Functions ************************)

(* isBiImp : form -> bool *)

fun isBiImp ((a >> b) && (c >> d)) = a = d andalso b = c
  | isBiImp _                      = false

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

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

(* formUnion1 : form list -> form -> form list *)

fun formUnion1 xs y = if formMember y xs then xs else y :: xs

(* formUnion : form list -> form list -> form list *)

fun formUnion nil       ys = ys
  | formUnion (x :: xs) ys =
      formUnion xs (if formMember x ys then ys else x :: ys)

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

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

(* prIndLabLongFormSet : int -> string -> form list -> 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")

(***************************** Sequent Parsing ******************************)

(* parseSequent : string -> form list * form *)

exception SyntaxError

local
  fun getname(cs) =
        let fun g(s, nil) = (s, nil)
              | g(s, cs' as c :: cs)
                          = if letter(c) then g(s ^ str c, cs) else (s, cs')   
        in g("",cs) end

  fun lex nil                          = nil
    | lex (#"=" :: #">" :: cs)         = "=>" :: lex cs
    | lex (#"-" :: #">" :: cs)         = "->" :: lex cs
    | lex (#"<" :: #"-" :: #">" :: cs) = "<->" :: lex cs
    | lex (c :: cs)                 =
        if charMember c [#",", #"f", #"~", #"&", #"|", #"(", #")"] 
          then str c :: lex cs
        else if Letter(c)
          then let val (s,cs) = getname(cs)
               in (str c ^ s) :: lex cs
               end
        else if charMember c [#" ", #"\t", #"\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

(************************* Parsing Labeled Trees ***************************) 

exception Lex of int

(* lex_tree : 
     string list -> (int * int * string * string list) list  

   lex_tree takes in the list of characters xs that is contained in the 
   file-argument of the "kripke" Unix-command and returns a list of 4-tuples 
   ts. Each element of ts represents one line of xs in the following way:
       first component :   line number
       second component:   indentation level
       third component :   node name
       fourth component:   list of propositional variables *)

fun lex_tree(xs) =

   (* lex_varlist : string list * int -> string list * form list

      first  argument        : list of remaining input characters
      second argument        : current line number
      output,first component : what remains of the first argument after taking
        off the list of propositional variables that it begins with
      output,second component: list of propositional variables that the first
        argument begins with *)

  let fun lex_varlist (xs, ln) =
            let datatype State = InitState
                               | NameState
                               | CommaState
                               | NextState
                fun lx(InitState, #"}" :: xs, name, varlist)
                     = (xs, varlist)
                  | lx(InitState, x :: xs, name, varlist)
                     = if Letter(x) 
                        then lx(NameState, xs, name ^ str x, varlist)
                       else if  (!m) andalso (x = #"f")
                        then lx(CommaState, xs, name, formUnion1 varlist F) 
                       else if (x = #" ") orelse (x = #"\t")
                        then lx(InitState, xs, name, varlist)
                       else raise Lex(ln)
                  | lx(NameState, #"," :: xs, name, varlist)
                     = lx(NextState, xs, "", formUnion1 varlist (Var(name)))
                  | lx(NameState, #"}" :: xs, name, varlist)
                     = (xs, formUnion1 varlist (Var(name)))
                  | lx(NameState, x :: xs, name, varlist)
                     = if letter(x)
                        then lx(NameState, xs, name ^ str x, varlist)
                       else if (x = #" ") orelse (x = #"\t")              
                        then lx(CommaState, xs, "", 
                                formUnion1 varlist (Var(name)))
                       else raise Lex(ln)
                  | lx(CommaState, #"," :: xs, name, varlist)
                     = lx(NextState, xs, name, varlist)
                  | lx(CommaState, #"}" :: xs, name, varlist)
                     = (xs, varlist)
                  | lx(CommaState, x :: xs, name, varlist)
                     =  if (x = #" ") orelse (x = #"\t")
                         then lx(CommaState, xs, name, varlist)
                        else raise Lex(ln)
                  | lx(NextState, x :: xs, name, varlist)
                     = if Letter(x) 
                        then lx(NameState, xs, name ^ str x, varlist)
                       else if (!m) andalso (x = #"f")
                        then lx(CommaState, xs, name, formUnion1 varlist F)
                       else if (x = #" ") orelse (x = #"\t") 
                        then lx(NextState, xs, name, varlist)
                       else raise Lex(ln)
                  | lx _
                     = raise Lex(ln)
            in lx(InitState, xs, "", nil) end

   (* lex_line :    string list 
                 *  (int * int * string * string list) list
                 *  int
                 -> string list
                 *  (int * int * string * string list) list
                 *  int     

      first component : list of remaining input characters
      second component: list of tokens that represent the lines 
        that have been read so far
      third component : current line number *)

      fun lex_line(xs, ts, ln) =
            let datatype State = InitState
                               | NameState
                               | ColonState
                               | LeftParenState
                               | NewLineState
                fun lx(InitState, #" " :: xs, ts, ln, sn,  name, varlist)     
                     = lx(InitState, xs, ts, ln, sn+1, name, varlist)
                  | lx(InitState, #"\t" :: xs, ts, ln, sn,  name, varlist) 
                     = lx(InitState, xs, ts, ln, ((sn div 8) + 1) * 8, 
                          name, varlist) 
                  | lx(InitState, #"\n" :: xs, ts, ln, sn, name, varlist)     
                     = (xs, ts, ln+1)                    
                  | lx(InitState, x :: xs, ts, ln, sn, name, varlist)         
                     = if letter(x) 
                        then lx(NameState,  xs, ts, ln, sn, name ^ str x, varlist)
                       else raise Lex(ln)
                  | lx(InitState, nil, ts, ln, sn, name, varlist)            
                     = (nil, ts, ln)
                  | lx(NameState, #":" :: xs, ts, ln, sn, name, varlist)      
                     = lx(LeftParenState,  xs, ts, ln, sn, name, varlist)
                  | lx(NameState, x :: xs, ts, ln, sn, name, varlist)        
                     = if letter(x) 
                        then lx(NameState, xs, ts, ln, sn, name ^ str x, varlist)
                       else if (x = #" ") orelse (x = #"\t")
                        then lx(ColonState,  xs, ts, ln, sn, name, varlist) 
                       else raise Lex(ln)
                  | lx(ColonState, #":" :: xs, ts, ln, sn, name, varlist)     
                     = lx(LeftParenState, xs, ts, ln, sn, name, varlist)
                  | lx(ColonState, x :: xs, ts, ln, sn, name, varlist) 
                     = if (x = #" ") orelse (x = #"\t") 
                        then lx(ColonState, xs, ts, ln, sn, name, varlist)
                       else raise Lex(ln)
                  | lx(LeftParenState, #"{" :: xs, ts, ln, sn, name, varlist) 
                     = let val (xs, varlist) = lex_varlist(xs, ln)
                       in lx(NewLineState, xs, ts, ln, sn, name, varlist) end
                  | lx(LeftParenState, x :: xs, ts, ln, sn, name, varlist) 
                     = if (x = #" ") orelse (x = #"\t") 
                        then lx(LeftParenState, xs, ts, ln, sn, name, varlist)
                       else raise Lex(ln) 
                  | lx(NewLineState, #"\n" :: xs, ts, ln, sn, name, varlist)  
                     = (xs, (ln, sn, name, varlist) :: ts, ln+1)
                  | lx(NewLineState, nil, ts, ln, sn, name, varlist)         
                     = (nil, (ln, sn, name, varlist) :: ts, ln)
                  | lx(NewLineState, x :: xs, ts, ln, sn, name, varlist) 
                     = if (x = #" ") orelse (x = #"\t")
                        then lx(NewLineState, xs, ts, ln, sn, name, varlist)
                       else raise Lex(ln)  
                  | lx(_, _, _, ln, _, _, _)  
                     = raise Lex(ln)
      in lx(InitState, xs, ts, ln, 0, "", nil) end   

      fun lx(nil, ts, ln) = ts 
        | lx(xs, ts, ln)  = lx(lex_line(xs,ts, ln))

  in lx(xs, nil, 1) end   

exception Parse of int
exception NoTreeFound

(* A labeled_tree is a triple whose first component is its name, whose second 
   component is a labeling set of propositional formulas, and whose third 
   component is a list of labeled_trees. *)

datatype labeled_tree = Node of string * form list * labeled_tree list

(* parse_tree : string list  -> labeled_tree *)

fun parse_tree(xs) =
  let fun tree(n: int, (_, _, name, varlist) :: (ln, m, name', varlist') :: ts)
           = if (n < m) 
             then 
              let val (ms, ts) = forest(m, (ln, m, name', varlist') :: ts)
              in (Node(name, varlist, ms), ts) end
             else (Node(name, varlist, nil), (ln, m, name', varlist') :: ts)
        | tree(n, (_, _, name, varlist) :: nil)
           = (Node(name, varlist, nil), nil)
        | tree(n, nil)
           = raise CannotHappen

      and forest(n, ts' as (_, m, name, varlist) :: ts)
           = if (m = n)
             then 
              let val(m, ts)  = tree(n, ts')
                  val(ms, ts) = forest(n, ts)
              in (m :: ms, ts) end
             else (nil, ts')
        | forest(n, nil)
           = (nil,nil)
  in case lex_tree(xs) of 
          nil =>  raise NoTreeFound
        | ts as ((_, n, _, _) :: ts')   
              => let val (m, ts) = tree(n, ts)
                 in if (ts = nil) then m else raise Parse(#1(hd ts)) end
  end

(************************* Printing Labeled Trees ****************************)

(* prModel : labeled_tree -> int -> unit 
   
   prModel p i prints labeled_tree p at indentation level i. *)

fun prModel p i =
      let fun prNode (Node(name, us, ps)) i =
                let val us = formSort us
                in prNodes ps (i+4); prIndLabLongFormSet i name us
                end

          and prNodes nil       i = ()
            | prNodes (p :: ps) i = (prNodes ps i; prNode p i) 
      in prNode p i end

(*********************** Annotating Tree with Formulas *********************)

(* saturate : labeled_tree -> labeled_tree 

   Takes a tree that is annotated with propositional variables and
   extends the variable sets so that the variable set at each node
   contains the variable sets of its ancestors.  *) 

fun saturate(Node(name, vs, cs)) =
      let fun f nil vs = nil
            | f ((Node(name, vs, cs)) :: ns) vs' 
                       = let val vs = formUnion vs vs'
                         in (Node(name, vs, f cs vs)) :: (f ns vs') end 
      in Node(name, vs, f cs vs) end

(* ord_subforms : form list -> form list 

   Takes in a list of formulas and returns a list of all subformulas
   that has the property that each formula is preceded by all of its
   subformulas. *)

fun ord_subforms(ps) =
      let fun sf(F)            = F :: nil
            | sf(r as Var(s))  = r :: nil
            | sf(r as (p || q)) = r :: (sf(q) @ sf(p))
            | sf(r as (p && q)) = r :: (sf(q) @ sf(p))
            | sf(r as (p >> q)) = r :: (sf(q) @ sf(p))

          fun sfl(nil)     = nil
            | sfl(p :: ps) = sfl(ps) @ sf(p)

      in rev(formMakeSet(sfl(ps))) end

(* nodeMember : form -> labeled_tree -> bool *) 

fun nodeMember p (Node(name, vs, cs)) = formMember p vs

(* nodeMember : labeled_tree -> form -> bool *)

fun nodeMember' n p = nodeMember p n

(* annotate : form list -> labeled_tree -> labeled_tree 
   
   If t is a tree that is labeled with propositional variables 
   then annotate ps t is the same tree whose nodes are labeled with the 
   sets of all formulas in the universe ps that are forced. *)

fun annotate ps (Node(name, vs, cs)) = 
      let val cs = map (annotate ps) cs
          fun annotate_node (F :: ps, qs)      
               = if formMember F vs 
                 then annotate_node (ps, formUnion1 qs F)
                 else annotate_node (ps, qs)
            | annotate_node (Var(s) :: ps, qs) 
               = if formMember (Var(s)) vs
                 then annotate_node (ps, formUnion1 qs (Var(s)))
                 else annotate_node (ps, qs)
            | annotate_node ((p || q) :: ps, qs)
               = if (formMember p qs) orelse (formMember q qs)
                 then annotate_node (ps, formUnion1 qs (p || q))
                 else annotate_node (ps, qs)
            | annotate_node ((p && q) :: ps, qs)
               = if (formMember p qs) andalso (formMember q qs)
                 then annotate_node (ps, formUnion1 qs (p && q))
                 else annotate_node (ps, qs)
            | annotate_node ((p >> q) :: ps, qs)
               = if implies((formMember p qs),(formMember q qs))
                  andalso forall cs (nodeMember (p >> q))
                 then annotate_node (ps, formUnion1 qs (p >> q))
                 else annotate_node (ps,  qs)
            | annotate_node (nil, qs)
               = Node(name, qs, cs)
      in annotate_node (ps, nil) end

(******************* Checking if Sequent Holds in Model **********************)

(* check: model -> (form list * form) -> unit *)

fun check tree (sequent: form list * form) =
      if not (forall (#1 sequent) (nodeMember' tree))
       then prStr("\nNot all assumptions of the sequent hold in the model.\n")
      else if nodeMember (#2 sequent) tree
       then prStr("\nThe conclusion of the sequent holds in the model.\n")
      else prStr("\nThe assumptions of the sequent hold in the \ 
                   \model but the conclusion does not.\n")

(***************** Finding Maximal Nodes where Sequent Holds ****************)

(* max_countermodels: labeled_tree -> form list * form -> string list *)

fun max_countermodels tree (sequent: form list * form) =
      let fun holds_not_at n = (forall (#1 sequent) (nodeMember' n)) andalso 
                               (not(nodeMember (#2 sequent) n))     
          fun f nil       = nil
            | f (x :: xs) = (g x) @ (f xs)

          and g(n as Node(name, ps, cs)) =
                let val xs = f cs
                in if (xs = nil) andalso (holds_not_at n)
                   then [name] else xs end
      in g tree end

(* find: labeled_tree -> form list * form -> unit *)

fun find tree sequent =
      let val xs = max_countermodels tree sequent
      in if xs = nil
       then prStr "\nNo node forces all assumptions but not the conclusion.\n"
      else 
       prStr("\nNode \"" ^ hd(xs) ^ "\" forces all assumptions but not the\
             \ conclusion.\n") end             

(* find_all: labeled_tree -> form list * form -> unit *)

fun find_all tree sequent =
      let val xs = max_countermodels tree sequent 
      in if xs = nil
         then prStr "\nNo node forces all assumptions but not the\
                     \ conclusion.\n"
         else (prStr("\nNode(s) ");
               prNames xs; 
               prStr(" force(s) all assumptions but not the conclusion.\n"))
      end

(**************************** Main Processing ********************************)

(* main : unit -> unit *)

fun main() =
      let val tree = parse_tree( get( !fileStr))
          val sequent = parseSequent( !sequentStr) 
          val (assumptions, conclusion) = sequent
          val universe = ord_subforms(conclusion :: assumptions)
          val tree = annotate universe (saturate tree)
      in if !a then ( prStr("\n"); prModel tree 1) else ();
         case !opt of 
               Check => check tree sequent
            |  Find  => find tree sequent
            |  List  => find_all tree sequent
      end

(************************* Support for Entry Point **************************)

(* helpMessage : unit -> string *)

fun helpMessage() =
      "Usage: " ^ !program ^ " [OPTION]... filename sequent\n\n\
      \  -m, --minimal   use minimal logic\n\
      \  -c, --check     check whether root forces assumptions but\
      \ not conclusion\n\
      \                  (default)\n\
      \  -a, --annotate  annotate tree with forced subformulas\n\
      \  -f, --find      find a maximal node that forces assumptions but not\n\
      \                  conclusion\n\
      \  -l, --list      list all maximal nodes that force assumptions but\
      \ not\n\
      \                  conclusion\n\
      \  -h, --help      output this information and exit\n\n\
\The file named by the first argument must contain a tree labeled with\n\
\propositional variables. Check the documentation paper \"Kripke: a\n\
\Countermodel Checker for Intuitionistic Propositonal Logic\" for a\n\
\description of how to represent labeled trees and sequents. This paper\n\
\can be obtained via WWW URL http://people.cis.ksu.edu/~stough/kripke/"

(* errorHelp : unit -> 'a *)

fun errorHelp() = error(helpMessage())

(* normalHelp : unit -> 'a *)

fun normalHelp() = (prStr(helpMessage()); prStr "\n"; exit OS.Process.success)

(* procLongOpt : string -> unit *)

fun procLongOpt "annotate" = a := true
  | procLongOpt "check"    = opt := Check
  | procLongOpt "find"     = opt := Find
  | procLongOpt "list"     = opt := List
  | procLongOpt "minimal"  = m := true
  | procLongOpt "help"     = normalHelp()
  | procLongOpt _          = errorHelp()

(* procShortOpt : string -> unit *)

fun procShortOpt #"a" = a := true
  | procShortOpt #"c" = opt := Check
  | procShortOpt #"f" = opt := Find
  | procShortOpt #"l" = opt := List
  | procShortOpt #"m" = m := true
  | procShortOpt #"h" = normalHelp()
  | procShortOpt _    = errorHelp()

(* procShortOpts : string list -> unit *)

fun procShortOpts nil       = errorHelp()
  | procShortOpts [c]       = procShortOpt c
  | procShortOpts (c :: cs) = (procShortOpt c; procShortOpts cs)

(* processArgs : string list -> unit *)

fun processArgs nil           = if !fileStr = "" orelse !sequentStr = ""
                                 then errorHelp() 
                                else ()
  | processArgs (arg :: args) =
      (case explode arg of
            #"-" :: #"-" :: cs => procLongOpt(implode cs)
          | #"-" :: cs         => procShortOpts cs
          | _                  =>
              if !fileStr = "" then fileStr := arg
              else 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 for Executable *************************) 

(* entryPoint: string * string list -> 'b *)

fun entryPoint(pgm, args) =
      (program := pgm;
       processArgs args;
       let val timer = Timer.startCPUTimer()
       in main()
            handle Lex(ln)     =>
                     error(!fileStr^ ": syntax error in line " 
                           ^ numeral ln)
                 | Parse(ln)   =>
                     error(!fileStr ^ ": illegal indentation in line " 
                           ^ numeral ln)
                 | SyntaxError =>
                     error(!program ^ ": syntax error in sequent \"" ^
                           !sequentStr ^ "\"")
                 | NoTreeFound => 
                     error(!fileStr ^ ": file is empty")
                 | IO.Io(x)    =>
                     error("File " ^ !fileStr ^ " does not exist.") 
                 | _           => error(!program ^ ": internal error");
          prStr "\n"; prCPUTime timer; exit OS.Process.success
       end)

end;

entryPoint(CommandLine.name(), CommandLine.arguments());