{-
Haskell version of ...
! The Checker module for the Boyer benchmark
! Started by Tony Kitto on March 30th 1988
! Changes Log
! 07-04-88 ADK Tautp function removed to main body
! 08-04-88 ADK bug fix = Truep returns True for (t)
! Falsep returns True for (f)
Haskell version::
23-06-93 JSM initial version
-}
module Checker (tautologyp) where
import Lisplikefns
tautologyp :: (Lisplist, Lisplist, Lisplist) -> Bool
tautologyp (Nil, _, _) = False
tautologyp (term@(Atom x), truelst, _) = truep (term, truelst)
tautologyp (term@(Cons (x, y)), truelst, falselst) =
if truep (term, truelst) then True
else if falsep (term, falselst) then False
else case x of
Atom "if" -> if truep (car y, truelst) then
tautologyp (cadr y, truelst, falselst)
else if falsep (car y, falselst) then
tautologyp (caddr y, truelst, falselst)
else
(tautologyp (cadr y, Cons (car y, truelst), falselst)) &&
(tautologyp (caddr y, truelst, Cons (car y, falselst)))
_ -> False
truep :: (Lisplist, Lisplist) -> Bool
truep (Nil, _) = False
truep (Cons (Atom "t", Nil), _) = True
truep (term, l) = lispmember (term, l)
falsep :: (Lisplist, Lisplist) -> Bool
falsep (Nil, _) = False
falsep (Cons (Atom "f", Nil), _) = True
falsep (term, l) = lispmember (term, l)
lispmember :: (Lisplist, Lisplist) -> Bool
lispmember (e, Cons (x, xs)) | e == x = True
| otherwise = lispmember (e, xs)
lispmember (_, _) = False
|