%include "~ids/misc/lib/miralib/stdenv.def"
wff ::= ATOM atom
        | wff $AND wff
        | wff $OR wff
        | NOT wff
        | wff $IMPLIES wff

atom == char || 'A'-'Z', 'a'-'z'
binary_connective ::= ANDSymbol | ORSymbol | IMPLIESSymbol



result * ::= Failure [char] | Success *




get_wff :: [char] -> (result wff, [char])
  get_wff l
    = iff (successful getatomresult)
      then (Success (ATOM (value getatomresult)), getatomrest)
      else
      (iff (~(successful getleftbracketresult))
       then (Failure "wff must be atomic or bracketted", l)
       else
       (iff (successful getnotresult)
        then || we have a not-symbol!
        (iff (successful getwffafternotresult)
         then
         (iff (successful getrightbracketafternegatedwffresult)
          then (Success (NOT (value getwffafternotresult)),
                 getrightbracketafternegatedwffrest)
          else (Failure "missing right bracket",
                 getwffafternotrest)
         )
         else
         (Failure "invalid wff after a negation", getnotrest)
        )
        else || we don't have a not-symbol; see if binary pattern exists...
        (iff (successful getfirstwffofbinaryresult)
         then
         (iff (successful getbinaryconnectiveresult)
          then
          (iff (successful getsecondwffofbinaryresult)
           then
           (iff (successful getrightbracketafterbinaryresult)
            then (Success (build_binary
                           (value getfirstwffofbinaryresult)
                           (value getbinaryconnectiveresult)
                           (value getsecondwffofbinaryresult)
                          ),
                   getrightbracketafterbinaryrest)
            else (Failure "missing right bracket", getsecondwffofbinaryrest)
           )
           else
           (Failure "invalid second component of binary",
             getbinaryconnectiverest)
          )
          else
          (Failure "missing binary connective", getfirstwffofbinaryrest)
         )
         else
         (Failure "invalid first component of binary", getnotrest)
        )
       )
      )
      where
      (getatomresult, getatomrest) = get_atom l
      (getleftbracketresult, getleftbracketrest) = get_left_bracket l
      (getnotresult, getnotrest) = get_not getleftbracketrest
      (getwffafternotresult, getwffafternotrest) = get_wff getnotrest
      (getrightbracketafternegatedwffresult, getrightbracketafternegatedwffrest)
        = get_right_bracket getwffafternotrest
      (getfirstwffofbinaryresult, getfirstwffofbinaryrest)
        = get_wff getleftbracketrest
      (getbinaryconnectiveresult, getbinaryconnectiverest) 
        = get_binary_connective getfirstwffofbinaryrest
      (getsecondwffofbinaryresult, getsecondwffofbinaryrest)
        = get_wff getbinaryconnectiverest
      (getrightbracketafterbinaryresult, getrightbracketafterbinaryrest)
        = get_right_bracket getsecondwffofbinaryrest





get_atom :: [char] -> (result atom, [char])
  get_atom [] = (Failure "no more characters", [])
  get_atom (h:t) = iff (is_atom h)
                   then (Success h, t)
                   else (Failure "invalid atom", h:t)


get_left_bracket :: [char] -> (result (), [char])
  get_left_bracket [] = (Failure "no more characters", [])
  get_left_bracket ('(':t) = (Success (), t)
  get_left_bracket (other:t) = (Failure "left bracket expected", other:t)




get_right_bracket :: [char] -> (result (), [char])
  get_right_bracket [] = (Failure "no more characters", [])
  get_right_bracket (')':t) = (Success (), t)
  get_right_bracket (other:t) = (Failure "right bracket expected", other:t)



get_not :: [char] -> (result (), [char])
  get_not [] = (Failure "no more characters", [])
  get_not ('~':t) = (Success (), t)
  get_not (other:t) = (Failure "not-symbol expected", other:t)



get_binary_connective :: [char] -> (result binary_connective, [char])
  get_binary_connective [] = (Failure "no more characters", [])
  get_binary_connective ('&':t) = (Success ANDSymbol, t)
  get_binary_connective ('|':t) = (Success ORSymbol,  t)
  get_binary_connective ('-':'>':t) = (Success IMPLIESSymbol, t)
  get_binary_connective (other:t)
    = (Failure "binary connective expected", other:t)









is_atom :: char -> bool
  is_atom x = (x >= 'A' & x <= 'Z') \/ (x >= 'a' & x <= 'z')



build_binary :: wff -> binary_connective -> wff -> wff
  build_binary a ANDSymbol b = a $AND b
  build_binary a ORSymbol  b = a $OR  b
  build_binary a IMPLIESSymbol b = a $IMPLIES b


successful :: result * -> bool
  successful (Failure x) = False
  successful (Success x) = True


value :: result * -> *
  value (Failure x) = error "value of failure is meaningless"
  value (Success x) = x
