View difference between Paste ID: tZVCYuDm and pCfDn7d1

 --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 _ = []
--- where possible
+
 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 ff@(Forall v f) = if ((Var v) `elem` (freeVars $ Term t)) || ((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)) || ((Var v) == x) then ff else Exists v $ formSubstitute x t f
+
 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)
-       print $ formSubstitute (Var "x") (Func "f" [Var "z",Var "y"]) f
+
-       where f = Exists "y" $ And (Rel "R2" [Var "x"]) (Not $ Forall "x" $ Or (Rel "R1" [Var "x"]) (Rel "R1" [Var "y"]))
+
 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"]))