module Data.Logic.Types.Harrison.FOL
( TermType(..)
, FOL(..)
, Function(..)
) where
import Data.Generics (Data, Typeable)
import Data.List (intersperse)
import Data.Logic.Classes.Arity
import Data.Logic.Classes.Apply (Apply(..), Predicate)
import Data.Logic.Classes.Constants (Constants(fromBool), asBool)
import Data.Logic.Classes.Pretty (Pretty(pretty), HasFixity(..), Fixity(..), FixityDirection(..))
import Data.Logic.Classes.Skolem (Skolem(..))
import Data.Logic.Classes.Term (Term(vt, foldTerm, fApp))
import qualified Data.Logic.Classes.Term as C
import qualified Data.Logic.Types.Common ()
import Prelude hiding (pred)
import Text.PrettyPrint (text, cat)
data TermType
= Var String
| Fn Function [TermType]
deriving (Eq, Ord)
data FOL = R String [TermType] deriving (Eq, Ord, Show)
instance Show TermType where
show (Var v) = "vt " ++ show v
show (Fn f ts) = "fApp " ++ show f ++ " " ++ show ts
instance Pretty TermType where
pretty (Var v) = pretty v
pretty (Fn f ts) = cat ([pretty f, text "("] ++ intersperse (text ", ") (map pretty ts) ++ [text ")"])
instance Apply FOL String TermType where
foldApply f tf (R p ts) = maybe (f p ts) tf (asBool p)
apply' = R
instance Constants String where
fromBool True = "true"
fromBool False = "false"
asBool x
| x == fromBool True = Just True
| x == fromBool False = Just False
| True = Nothing
instance Constants FOL where
fromBool x = R (fromBool x) []
asBool (R p _) = asBool p
instance Predicate String
instance Pretty FOL where
pretty (R p ts) = cat ([pretty p, text "("] ++ intersperse (text ", ") (map pretty ts) ++ [text ")"])
instance Arity String where
arity _ = Nothing
data Function
= FName String
| Skolem String
deriving (Eq, Ord, Data, Typeable, Show)
instance Pretty Function where
pretty (FName s) = text s
pretty (Skolem v) = text ("sK" ++ v)
instance C.Function Function String
instance Skolem Function String where
toSkolem = Skolem
isSkolem (Skolem _) = True
isSkolem _ = False
instance Term TermType String Function where
vt = Var
fApp = Fn
foldTerm vfn _ (Var x) = vfn x
foldTerm _ ffn (Fn f ts) = ffn f ts
zipTerms = undefined
instance HasFixity FOL where
fixity = const (Fixity 10 InfixN)