(*
 * a2.sml
 *
 * CSE3322 Programming Languages and Implementation, 2006
 * Assignment 2 sample solution
 *
 * Cameron McCormack cam OF mcc.id.au
 *
 * August 25, 2006
 *)

use "parser.sml";  (* include the WFF datatype and parser *)

(* Q2 *)
fun trav f g h t =
      let
        fun trav' (varid p)               = f p
          | trav' (unexp  (oper, rt))     = g oper (trav' rt)
          | trav' (binexp (lt, oper, rt)) = h (trav' lt) oper (trav' rt);
      in
        trav' t
      end;

(* Q3 *)
fun show t =
      let
        fun f p        = p;
        fun g knot p   = "(not " ^ p ^ ")";
        fun h p oper q = "(" ^ p ^ (case oper of
                                           imp  => " => "
                                         | disj => " or "
                                         | conj => " and ") ^ q ^ ")";
      in
        trav f g h t
      end;

(* Q4 *)
fun eval ps t =
      let
        fun f p        = member p ps;  (* member is defined in parser.sml *)
        fun g knot p   = not p;
        fun h p imp  q = not p orelse q
          | h p disj q = p orelse q
          | h p conj q = p andalso q;
      in
        trav f g h t
      end;

(* Q5 *)
fun parse s = parseExpression (lexical (explode s));

(* Q6 *)
datatype proof = SATISFIABLE | TAUTOLOGY | CONTRADICTION;

fun prove t =
    let
      (* gather traverses a WFF option and returns a list of all of
         the propositions present in the tree.  It doesn't attempt to
         eliminate duplicates. *)
      fun gather NONE     = []  (* no WFF, so no propositions *)
        | gather (SOME t) =     (* there is a WFF... *)
              let
                fun gather' (varid p)            = [p]  (* found one *)
                  | gather' (unexp (_, rt))      = gather' rt  (* found a unary operator, so search its subtree *)
                  | gather' (binexp (lt, _, rt)) = (gather' lt) @ (gather' rt);  (* found a binary operator, so search its two subtrees *)
              in
                gather' t
              end;
      
      (* overlap takes two string lists and determines whether any proposition
         in the first list occurs in the second list. *)
      fun overlap []      _  = false
        | overlap (x::xs) L  = member x L orelse overlap xs L;

      (* Helper functions to AND optional WFFs together. *)
      fun And'  p        (SOME q) = SOME (binexp (p, conj, q))  (* WFF -> WFF option -> WFF option *)
        | And'  p        NONE     = SOME p;
      fun And'' (SOME p) (SOME q) = SOME (binexp (p, conj, q))  (* WFF option -> WFF option -> WFF option *)
        | And'' (SOME p) NONE     = SOME p
        | And'' NONE     (SOME q) = SOME q
        | And'' NONE     NONE     = NONE;

      (* Helper functions to OR optional WFFs together. *)
      fun Or   p        q        = SOME (binexp (p, disj, q));  (* WFF -> WFF -> WFF option *)
      fun Or'  p        (SOME q) = SOME (binexp (p, disj, q))   (* WFF -> WFF option -> WFF option *)
        | Or'  p        NONE     = SOME p;
      fun Or'' (SOME p) (SOME q) = SOME (binexp (p, disj, q))   (* WFF option -> WFF option -> WFF option *)
        | Or'' (SOME p) NONE     = SOME p
        | Or'' NONE     (SOME q) = SOME q
        | Or'' NONE     NONE     = NONE;

      (* Helper function to NOT a WFF. *)
      fun Not p = unexp (knot, p);  (* WFF -> WFF *)

      (* findOpr will search a WFF option for a unary operator or a binary
         operator that is not 'opr'.  It will return a
         (WFF * WFF option) option, where the first WFF is the subtree rooted
         at that found operator, and the second WFF is the 'rest' of the tree
         that has been accumulated as it searched down the tree (which might
         be NONE, if the "bad" operator was found at the top of the tree).  If
         no applicable operator was found, the function returns NONE. *)
      fun findOpr opr NONE     = NONE
        | findOpr opr (SOME t) =
            let
              (* makeTree takes a list of WFFs and joins them all together
                 with binary operator 'opr'. *)
              fun makeTree [] = NONE
                | makeTree L  =
                    let
                      fun makeTree' [x]     = x
                        | makeTree' (x::xs) = binexp (x, opr, (makeTree' xs));
                    in
                      SOME (makeTree' L)
                    end;

              (* findOpr' does all the real work. *)
              fun findOpr' (varid _)               rest = NONE  (* End of a branch, so no bad operator found. *)
                | findOpr' (T as unexp (knot, _))  rest = SOME (T, makeTree rest) (* Unary operators are always bad. *)
                | findOpr' (T as binexp (l, b, r)) rest =
                    if b <> opr then SOME (T, makeTree rest)  (* A bad binary operator. *)
                                else let  (* A good binary operator, so recursively search the left subtree... *)
                                       val ret = findOpr' l (r::rest);
                                     in   (* and if there was one on the left, return it, otherwise recursively
                                             search the right subtree. *)
                                       if isSome ret then ret else findOpr' r (l::rest)
                                     end;
            in
              findOpr' t []
            end;

      (* This is the main follows function, that applies the rules 1--7 as
         described at http://www.csse.monash.edu.au/~lloyd/tildeAlgDS/Wff/.
         The function takes three arguments: the depth string that will be used
         in the trace print, and two WFF options that are both sides of the
         'follows'.

         The function first calls "findOpr" on the left tree, looking for
         non-AND operators.  If it found one, it uses pattern matching to
         handle rules 1--3.  If it didn't find one, it will call "findOpr"
         on the right tree, looking for non-OR operators.  If it found one
         of those, it uses pattern matching to handle rules 4--6.  If "findOpr"
         didn't find one on the RHS either, it uses the 'overlap' and
         'gather' functions defined above to implement rule 7.

         For each pattern, a trace line will be printed out (with the
         "trace" function, or "traceLast" in rule 7) and then "follows'" is
         called recursively with an updated depth string (the "(deeper1 d)" or
         "(deeper2 d)") and the two new WFF options to test.
       *)
      fun follows' d L R =
            let
              fun show' NONE       = ""
                | show' (SOME t)   = show t;
              fun traceMessage n   = "[" ^ (Int.toString n) ^ "] " ^ d ^ ": " ^ (show' L) ^ " ==> " ^ (show' R);
              fun trace        n   = print ((traceMessage n) ^ "\n");
              fun traceLast    res = print ((traceMessage 7) ^ (if res then ", succeed\n" else ", fail\n"));
              fun deeper1 d        = d ^ ".1";
              fun deeper2 d        = d ^ ".2";
            in
              case findOpr conj L of
                  SOME (binexp (p, disj, q), rest) => (* rule 1 *)
                        (trace 1;
                         follows' (deeper1 d) (And' p rest) R
                           andalso follows' (deeper2 d) (And' q rest) R)

                | SOME (binexp (p, imp, q), rest) => (* rule 2 *)
                        (trace 2;
                         follows' (deeper1 d) (And'' (Or (Not p) q) rest) R)

                | SOME (unexp (knot, p), rest) => (* rule 3 *)
                        (trace 3;
                         follows' (deeper1 d) rest (Or' p R))

                | _ => 

              case findOpr disj R of
                  SOME (binexp (p, conj, q), rest) => (* rule 4 *)
                        (trace 4;
                         follows' (deeper1 d) L (Or' p rest)
                           andalso follows' (deeper2 d) L (Or' q rest))

                | SOME (binexp (p, imp, q), rest) => (* rule 5 *)
                        (trace 5;
                         follows' (deeper1 d) L (Or'' (Or (Not p) q) rest))

                | SOME (unexp (knot, p), rest) => (* rule 6 *)
                        (trace 6;
                         follows' (deeper1 d) (And' p L) rest)

                | _ => (* rule 7 *)
                        let
                          val res = overlap (gather L) (gather R);
                        in
                          (traceLast res; res)
                        end
            end;

      val follows = follows' "1";
    in
      if      follows NONE (SOME t) then TAUTOLOGY
      else if follows (SOME t) NONE then CONTRADICTION
      else                               SATISFIABLE
    end;

val p = varid "p";
val q = varid "q";
val r = varid "r";
val piq = binexp (p, imp, r);