{- 
   Abstract syntax for first order logic
   Pedro Vasconcelos, 2009--2010
   pbv@dcc.fc.up.pt
 -}
module FOL where
import Data.List
import Data.Map (Map)
import qualified Data.Map as Map
import Data.Tree
import Zipper hiding (delete)

-- type synonyms for names of variables, 
-- functional and relational symbols
type Var    = String
type Funsym = String
type Relsym = String

-- first order logic formulas 
data Formula = TT
             | FF
             | Rel Relsym [Term]
             | Not Formula 
             | And Formula Formula
             | Or Formula Formula 
             | Implies Formula Formula
             | Exist Var Formula
             | Forall Var Formula
               deriving (Eq,Show,Read)

-- instance Show Formula where
--    showsPrec p f = showsFormula p f

-- first order logic terms 
data Term = Var Var
          | Fun Funsym [Term]
            deriving (Eq, Show, Read)

-- substitutions: mappings from variables to terms
type Subst = Map Var Term

-- a general class for data types with free variables
class FV a where
    fv :: a -> [Var]
    subst :: Subst -> a -> a

-- instance for terms
instance FV Term where
    fv (Var x) = [x]
    fv (Fun f ts) = concatMap fv ts
    subst s (Var v)    = Map.findWithDefault (Var v) v s
    subst s (Fun f ts) = Fun f $ map (subst s) ts

-- instance for formulas
instance FV Formula where
    fv TT = []
    fv FF = []
    fv (Rel r ts) = concatMap fv ts
    fv (Not f) = fv f
    fv (And f1 f2) = fv f1 ++ fv f2
    fv (Or f1 f2) = fv f1 ++ fv f2
    fv (Implies f1 f2) = fv f1 ++ fv f2
    fv (Exist x f) = delete x (nub (fv f))
    fv (Forall x f) = delete x (nub (fv f))
    --
    subst s TT = TT
    subst s FF = FF
    subst s (Rel r ts) = Rel r $ map (subst s) ts
    subst s (Not f) = Not (subst s f)
    subst s (And f1 f2) = And (subst s f1) (subst s f2)
    subst s (Or f1 f2) = Or (subst s f1) (subst s f2)
    subst s (Implies f1 f2) = Implies (subst s f1) (subst s f2)
    subst s (Exist x f) = Exist x (subst s' f)
        where s' = Map.delete x s
    subst s (Forall x f) = Forall x (subst s' f)
        where s' = Map.delete x s


-- derived instances for parametric types
instance FV a => FV [a] where
    fv ts = concatMap fv ts
    subst s ts = map (subst s) ts

instance (FV a, FV b) => FV (a,b) where
    fv (u,v) = fv u ++ fv v
    subst s (u,v) = (subst s u, subst s v)

instance (FV a, FV b, FV c) => FV (a,b,c) where
    fv (u,v,w) = fv u ++ fv v ++ fv w
    subst s (u,v,w) = (subst s u, subst s v, subst s w)

instance FV a => FV (Maybe a) where
    fv Nothing  = []
    fv (Just x) = fv x
    subst s Nothing = Nothing
    subst s (Just x)= Just (subst s x)

instance FV a => FV (Tree a) where
    fv (Node n ts) = fv n ++ concatMap fv ts
    subst s (Node n ts) = Node (subst s n) (map (subst s) ts)

instance FV a => FV (TreeLoc a) where
    fv (Loc t l r ps) = fv t ++ fv l ++ fv r ++ fv ps
    subst s (Loc t l r ps) = Loc (subst s t) (subst s l) (subst s r) (subst s ps)