foh

--ghc 7.10

data Term = Var String | Const String | Func String [Term] deriving Eq

data Formula = Tr | Fa | Rel String [Term] |
               And Formula Formula | Or Formula Formula |
               To Formula Formula | Not Formula |
               Forall String Formula | Exists String Formula

data Expr = Term Term | Formula Formula deriving Show

instance Show Term where
    show (Var s) = s
    show (Const c) = c
    show (Func f ts) = f ++ (show ts)

instance Show Formula where
    show Tr = "T"
    show Fa = "_|_"
    show (Rel r ts) = r ++ (show ts)
    show (And f1 f2) = "(" ++ (show f1) ++ "^" ++ (show f2) ++ ")"
    show (Or f1 f2) = "(" ++ (show f1) ++ "v" ++ (show f2) ++ ")"
    show (To f1 f2) = "(" ++ (show f1) ++ "->" ++ (show f2) ++ ")"
    show (Not f) = "-" ++ (show f)
    show (Forall v f) = "(" ++ "П" ++ v ++ ": " ++ (show f) ++ ")"
    show (Exists v f) = "(" ++ "E" ++ v ++ ": " ++ (show f) ++ ")"


unterm (Term t) = t

unformula (Formula f) = f

subformulas (And f1 f2) = [f1,f2] ++ (subformulas f1) ++ (subformulas f2)
subformulas (Or f1 f2) = subformulas (And f1 f2)
subformulas (To f1 f2) = subformulas (And f1 f2)
subformulas (Not f1) = [f1] ++ (subformulas f1)
subformulas (Forall _ f1) = subformulas (Not f1)
subformulas (Exists _ f1) = subformulas (Not f1)
subformulas _ = []

termSubstitute x t tt@(Var _) = if tt == x then t else tt
termSubstitute _ _ tt@(Const _) = tt
termSubstitute x t tt@(Func f ts) = Func f $ map (\z -> termSubstitute x t z) ts

formSubstitute x t (Rel r ts) = Rel r $ map (\z -> termSubstitute x t z) ts
formSubstitute x t (And f1 f2) = And (formSubstitute x t f1) (formSubstitute x t f2)
formSubstitute x t (Or f1 f2) = Or (formSubstitute x t f1) (formSubstitute x t f2)
formSubstitute x t (To f1 f2) = To (formSubstitute x t f1) (formSubstitute x t f2)
formSubstitute x t (Not f1) = Not (formSubstitute x t f1)
formSubstitute x t ff@(Forall v f) = if (Var v) `elem` (freeVars $ Term t)
                                     then undefined
                                     else if (Var v) == x
                                     then ff else Forall v $ formSubstitute x t f
formSubstitute x t ff@(Exists v f) = if (Var v) `elem` (freeVars $ Term t)
                                     then undefined
                                     else if (Var v) == x
                                     then ff else Exists v $ formSubstitute x t f
formSubstitute _ _ whatever = whatever

-- duplicates are allowed!
freeVars (Term (Var s)) = [Var s]
freeVars (Term (Func _ ts)) = concat $ map (\x -> freeVars (Term x)) ts
freeVars (Formula (Rel _ ts)) = freeVars $ Term $ Func "" ts
freeVars (Formula (And f1 f2)) = freeVars (Formula f1) ++ (freeVars $ Formula f2)
freeVars (Formula (Or f1 f2)) = freeVars (Formula f1) ++ (freeVars $ Formula f2)
freeVars (Formula (To f1 f2)) = freeVars (Formula f1) ++ (freeVars $ Formula f2)
freeVars (Formula (Not f1)) = freeVars (Formula f1)
freeVars (Formula (Forall v f)) = remove (Var v) $ freeVars $ Formula f
freeVars (Formula (Exists v f)) = remove (Var v) $ freeVars $ Formula f

remove _ [] = []
remove y (x:xs) = if x == y then remove y xs else x : (remove y xs)

main = do
       print f
       print $ formSubstitute (Var "x") (Var "z") f
       where f = And (Rel "R2" [Var "x"]) (Not $ Forall "x" $ Or (Rel "R1" [Var "x"]) (Rel "R1" [Var "y"]))