head	1.5;
access;
symbols;
locks; strict;
comment	@# @;


1.5
date	97.01.13.12.58.41;	author ids;	state Exp;
branches;
next	1.4;

1.4
date	97.01.13.12.48.51;	author ids;	state Exp;
branches;
next	1.3;

1.3
date	93.06.20.13.20.58;	author ids;	state Exp;
branches;
next	1.2;

1.2
date	93.01.24.22.12.29;	author ids;	state Exp;
branches;
next	1.1;

1.1
date	92.06.18.17.42.03;	author ids;	state Exp;
branches;
next	;


desc
@@


1.5
log
@"if" -> "iff" in library stuff, now that "if" is a reserved word in Miranda.
@
text
@%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
@


1.4
log
@further change to library pathname.
@
text
@d20 1
a20 1
    = if (successful getatomresult)
d23 1
a23 1
      (if (~(successful getleftbracketresult))
d26 1
a26 1
       (if (successful getnotresult)
d28 1
a28 1
        (if (successful getwffafternotresult)
d30 1
a30 1
         (if (successful getrightbracketafternegatedwffresult)
d40 1
a40 1
        (if (successful getfirstwffofbinaryresult)
d42 1
a42 1
         (if (successful getbinaryconnectiveresult)
d44 1
a44 1
          (if (successful getsecondwffofbinaryresult)
d46 1
a46 1
           (if (successful getrightbracketafterbinaryresult)
d89 1
a89 1
  get_atom (h:t) = if (is_atom h)
@


1.3
log
@changed pathname of my library to be more in the spirit of David Turner's
 choice of "real" library pathname.
@
text
@d1 1
a1 1
%include "~ids/.lib/miralib/stdenv.def"
@


1.2
log
@used new, better library directory pathname.
@
text
@d1 1
a1 1
%include "~ids/.miranda/lib/stdenv.def"
@


1.1
log
@Initial revision
@
text
@d1 1
a1 1
%include ".miralib/stdenv.def"
@