content: {-
      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
  
  
  