Moved datatype declarations and associated functions to separate files

5 files changed, 307 insertions, 227 deletions

diff --git a/Object.hs b/Object.hs
new file mode 100644
index 0000000..640cf08
--- /dev/null
+++ b/Object.hs
@@ -0,0 +1,39 @@
+module Object (
+	Object(..),
+
+	List
+	) where
+
+
+
+import Data.List
+import TypeVar
+import Term
+import Theorem
+
+
+
+data Object = ObjNum { objNum :: Number }
+            | ObjName { objName :: Name }
+            | ObjList { objList :: List }
+            | ObjTyOp { objTyOp :: TypeOp }
+            | ObjType { objType :: Type }
+            | ObjConst { objConst :: Const }
+            | ObjVar { objVar :: Var }
+            | ObjTerm { objTerm :: Term }
+            | ObjThm { objThm :: Theorem } deriving (Eq)
+
+type List = [Object]
+
+
+
+instance Show Object where
+    show (ObjNum a)    =   show a
+    show (ObjName a)   =   show a
+    show (ObjList a)   =   show a
+    show (ObjTyOp a)   =   show a
+    show (ObjType a)   =   show a
+    show (ObjConst a)  =   show a
+    show (ObjVar a)    =   show a
+    show (ObjTerm a)   =   show a
+    show (ObjThm a)    =   show a
diff --git a/Semantic.hs b/Semantic.hs
index 7de8dee..d50905c 100644
--- a/Semantic.hs
+++ b/Semantic.hs
@@ -1,89 +1,12 @@
 import Control.Monad( liftM )
 import System( getArgs )
 import Data.List
+import TypeVar
+import Term
+import Theorem
+import Object
 
 
-data Object = ObjNum { objNum :: Number }
-            | ObjName { objName :: Name }
-            | ObjList { objList :: List }
-            | ObjTyOp { objTyOp :: TypeOp }
-            | ObjType { objType :: Type }
-            | ObjConst { objConst :: Const }
-            | ObjVar { objVar :: Var }
-            | ObjTerm { objTerm :: Term }
-            | ObjThm { objThm :: Theorem } deriving (Eq)
-
-type Number = Int
-
-data Name = Name { nameSpace :: [String]
-                 , nameId :: String } deriving (Eq)
-
-type List = [Object]
-
-data TypeOp = TypeOp { tyOp :: Name } deriving (Eq)
-
-data Type = TypeVar { typeVar :: Name }
-          | AType { aType :: [Type]
-                  , aTypeOp :: TypeOp } deriving (Eq)
-
-data Const = Const { constName :: Name } deriving (Eq)
-
-data Var = Var { varName :: Name
-               , varTy :: Type } deriving (Eq)
-
-data Term = TVar { tVar :: Var }
-          | TConst { tConst :: Const
-                   , tConstType :: Type }
-          | TApp { tAppLeft :: Term
-                 , tAppRight :: Term }
-          | TAbs { tAbsVar :: Term
-                 , tAbsTerm :: Term }
-
-data Theorem = Theorem { thmHyp :: [Term]
-                       , thmCon :: Term } deriving (Eq)
-
-
-instance Show Object where
-    show (ObjNum a)    =   show a
-    show (ObjName a)   =   show a
-    show (ObjList a)   =   show a
-    show (ObjTyOp a)   =   show a
-    show (ObjType a)   =   show a
-    show (ObjConst a)  =   show a
-    show (ObjVar a)    =   show a
-    show (ObjTerm a)   =   show a
-    show (ObjThm a)    =   show a
-
-instance Show Name where
-    show a   =   intercalate "." (nameSpace a ++ [nameId a])
-
-instance Show TypeOp where
-    show a   =   "typeOp " ++ (show $ tyOp a)
-
-instance Show Type where
-    show (TypeVar tyVar)   =   "typeVar " ++ (show tyVar)
-    show (AType list typeOp) =   "type " ++ (show $ tyOp typeOp) ++ " " ++ (show list)
-
-instance Show Const where
-    show (Const a)   =   show a
-
-instance Show Var where
-    show (Var a _)   =   show a
-
-instance Show Term where
-    show (TVar a)       =   show a
-    show (TConst a _)   =   show a
-    show (TApp (TApp eq lhs) rhs)
-            | isEq eq   =   "(" ++ (show lhs) ++ " = " ++ (show rhs) ++ ")"
-    show (TApp a b)     =   "(" ++ (show a) ++ " " ++ (show b) ++ ")"
-    show (TAbs a b)     =   "(\\" ++ (show a) ++ " -> " ++ (show b) ++ ")"
-
-instance Show Theorem where
-    show a   =   (show . thmHyp $ a) ++ " |- " ++ (show . thmCon $ a)
-
-instance Eq Term where
-    a == b   =   a `alphaEquiv` b
-
 
 data Stack = Stack { stackList :: [Object] }
 data Dictionary = Dictionary { dictionMap :: [(Int,Object)] }
@@ -104,9 +27,6 @@ instance Show Theorems where
     show a   =   "Theorems:\n" ++ intercalate "\n" (map (show) (theoremList a)) ++ "\n\n"
 
 
-type Substitution = [[[Object]]]
-
-
 data ArticleLine = Comment { commentString :: String }
                  | Command { commandFunc :: ((Stack,Dictionary,Assumptions,Theorems)->(Stack,Dictionary,Assumptions,Theorems)) }
 
@@ -225,7 +145,7 @@ betaConv :: (Stack,Dictionary,Assumptions,Theorems) -> (Stack,Dictionary,Assumpt
 betaConv (s,d,a,t) =
     let stack = stackList s
         op = (\x -> Theorem [] (mkEquals x
-                                         (substitute [[], [[ObjVar . tVar . tAbsVar . tAppLeft $ x, ObjTerm . tAppRight $ x]]]
+                                         (substitute ([], [(tVar . tAbsVar . tAppLeft $ x, tAppRight $ x)])
                                                      (tAbsTerm . tAppLeft $ x))))
         theorem = ObjThm $ op (objTerm $ stack!!0)
         s' = Stack $ theorem : (tail stack)
@@ -380,7 +300,12 @@ subst (s,d,a,t) =
     let stack = stackList s
         op = (\x y -> Theorem (map (substitute y) (thmHyp x))
                               (substitute y (thmCon x)))
-        theorem = ObjThm $ op (objThm $ stack!!0) ((map (map objList)) . (map objList) . objList $ stack!!1)
+        substitution =
+            (\x -> let list = (map (map objList)) . (map objList) . objList $ x
+                       f = (\g h x -> (g . head $ x, h . last $ x))
+                   in f (map (f objName objType)) (map (f objVar objTerm)) list)
+
+        theorem = ObjThm $ op (objThm $ stack!!0) (substitution $ stack!!1)
         s' = Stack $ theorem : (drop 2 stack)
     in (s',d,a,t)
 
@@ -434,147 +359,6 @@ varType (s,d,a,t) =
 
 
 
-
-alphaEquiv :: Term -> Term -> Bool
-alphaEquiv a b =
-    let equiv = \term1 term2 varmap lambdaDepth ->
-            case (term1,term2) of
-                (TConst a1 b1, TConst a2 b2) ->
-                    a1 == a2 && b1 == b2
-
-                (TApp a1 b1, TApp a2 b2) ->
-                    equiv a1 a2 varmap lambdaDepth &&
-                    equiv b1 b2 varmap lambdaDepth
-
-                (TAbs (TVar (Var name1 type1)) b1, TAbs (TVar (Var name2 type2)) b2) ->
-                    type1 == type2 &&
-                    equiv b1 b2 newmap (lambdaDepth + 1)
-                    where newmap = (lambdaDepth + 1, ((Var name1 type1),(Var name2 type2))) : varmap
-
-                (TVar a1, TVar a2) ->
-                    -- the order of the pair is important
-                    (lambdaDepth, (a1,a2)) `elem` varmap ||
-                    not ((lambdaDepth, (a1,a2)) `elem` varmap) && a1 == a2
-
-                (_,_) -> False
-    in equiv a b [] 0
-
-
-alphaConvert :: Term -> Term -> Term
-alphaConvert (TConst a ty) (TConst _ _) = TConst a ty
-alphaConvert (TApp a1 b1) (TApp a2 b2) = TApp (alphaConvert a1 a2) (alphaConvert b1 b2)
-alphaConvert (TVar v) (TVar _) = TVar v
-alphaConvert (TAbs v1 a) (TAbs v2 b) = substitute [[],[[ObjVar $ tVar v1, ObjTerm $ v2]]] (TAbs v1 (alphaConvert a b))
-
-
-alphaConvertList :: [Term] -> [Term] -> [Term]
-alphaConvertList a b = map (\x -> alphaConvert (fst x) (snd x)) (zip a b)
-
-
-substitute :: Substitution -> Term -> Term
-substitute [tymap, vmap] term =
-    let typesub =
-            (\x y ->
-                case y of
-                    (TConst a ty) -> if (ty == (objType . head $ x))
-                                     then TConst a (objType . last $ x)
-                                     else TConst a ty
-                    (TApp a b) -> TApp (typesub x a) (typesub x b)
-                    (TAbs v a) -> TAbs v (typesub x a)
-                    (TVar v) -> TVar v)
-        varsub =
-            (\x y ->
-                case y of
-                    (TConst a ty) -> TConst a ty
-                    (TApp a b) -> TApp (varsub x a) (varsub x b)
-                    (TVar v) -> if (v == (objVar . head $ x))
-                                then objTerm . last $ x
-                                else TVar v
-                    (TAbs v a) -> let safe = rename (TAbs v a) (union [(objVar . head $ x)] (containsVars (objTerm . last $ x)))
-                                  in case safe of
-                                         (TAbs m n) -> TAbs m (varsub x n))
-        tydone = foldl' (\x y -> typesub y x) term tymap
-        vdone = foldl' (\x y -> varsub y x) tydone vmap
-    in vdone
-
-
-containsVars :: Term -> [Var]
-containsVars t =
-    let f = (\term list ->
-            case term of
-                (TConst a b) -> list
-                (TApp a b) -> union list ((f a list) ++ (f b list))
-                (TVar a) -> union list [a]
-                (TAbs a b) -> union list ([tVar a] ++ (f b list)))
-    in f t []
-
-
-rename :: Term -> [Var] -> Term
-rename (TAbs (TVar v) t) varlist =
-    let doRename =
-            (\x y z -> case x of
-                           (TAbs (TVar a) b) -> if (a == y)
-                                         then TAbs (TVar z) (doRename b y z)
-                                         else TAbs (TVar a) (doRename b y z)
-                           (TConst a b) -> TConst a b
-                           (TApp a b) -> TApp (doRename a y z) (doRename b y z)
-                           (TVar a) -> if (a == y)
-                                         then TVar z
-                                         else TVar a)
-        findSafe =
-            (\x y -> if (x `elem` y)
-                     then case x of
-                              (Var a b) ->
-                                  case a of
-                                      (Name c d) -> findSafe (Var (Name c (d ++ "'")) b) y
-                     else x)
-    in if (v `elem` varlist)
-       then doRename (TAbs (TVar v) t) v (findSafe v varlist)
-       else TAbs (TVar v) t
-
-
-
-
-typeOf :: Term -> Type
-typeOf (TConst c ty) = ty
-typeOf (TVar v) = varTy v
-typeOf (TAbs v t) = typeFunc (typeOf v) (typeOf t)
-typeOf (TApp f _) = 
-    -- type of f is of the form [[a,b], "->"]
-    last . aType . typeOf $ f
-
-
-mkEquals :: Term -> Term -> Term
-mkEquals lhs rhs =
-    let eqConst = TConst (Const (Name [] "=")) (mkEqualsType (typeOf lhs))
-    in TApp (TApp eqConst lhs) rhs
-
-
-mkEqualsType :: Type -> Type
-mkEqualsType ty = typeFunc (AType [] (TypeOp (Name [] "bool"))) (typeFunc ty ty)
-
-
-getlhs :: Term -> Term
-getlhs (TApp (TApp eq lhs) _) =
-    if (isEq eq) then lhs else error "Tried to get lhs from a non-eq term"
-
-
-getrhs :: Term -> Term
-getrhs (TApp (TApp eq _) rhs) =
-    if (isEq eq) then rhs else error "Tried to get rhs from a non-eq term"
-
-
-isEq :: Term -> Bool
-isEq (TConst (Const (Name [] "=")) _) = True
-isEq _ = False
-
-
-typeFunc :: Type -> Type -> Type
-typeFunc ty1 ty2 = AType [ty1,ty2] (TypeOp (Name [] "->"))
-
-
-
-
 doSemanticCheck :: [String] -> (Stack,Dictionary,Assumptions,Theorems)
 doSemanticCheck =
     let s = Stack []
diff --git a/Term.hs b/Term.hs
new file mode 100644
index 0000000..626b91c
--- /dev/null
+++ b/Term.hs
@@ -0,0 +1,173 @@
+module Term (
+    Term(..),
+
+    alphaEquiv,
+    alphaConvert,
+    alphaConvertList,
+    substitute,
+    containsVars,
+    rename,
+    typeOf,
+    mkEquals,
+    isEq,
+    getlhs,
+    getrhs
+    ) where
+
+
+
+import Data.List
+import TypeVar
+
+
+
+data Term = TVar { tVar :: Var }
+          | TConst { tConst :: Const
+                   , tConstType :: Type }
+          | TApp { tAppLeft :: Term
+                 , tAppRight :: Term }
+          | TAbs { tAbsVar :: Term
+                 , tAbsTerm :: Term }
+
+type Substitution = ( [(Name,Type)], [(Var,Term)] )
+
+
+instance Show Term where
+    show (TVar a)       =   show a
+    show (TConst a _)   =   show a
+    show (TApp (TApp eq lhs) rhs)
+            | isEq eq   =   "(" ++ (show lhs) ++ " = " ++ (show rhs) ++ ")"
+    show (TApp a b)     =   "(" ++ (show a) ++ " " ++ (show b) ++ ")"
+    show (TAbs a b)     =   "(\\" ++ (show a) ++ " -> " ++ (show b) ++ ")"
+
+instance Eq Term where
+    a == b   =   a `alphaEquiv` b
+
+
+
+alphaEquiv :: Term -> Term -> Bool
+alphaEquiv a b =
+    let equiv = \term1 term2 varmap lambdaDepth ->
+            case (term1,term2) of
+                (TConst a1 b1, TConst a2 b2) ->
+                    a1 == a2 && b1 == b2
+
+                (TApp a1 b1, TApp a2 b2) ->
+                    equiv a1 a2 varmap lambdaDepth &&
+                    equiv b1 b2 varmap lambdaDepth
+
+                (TAbs (TVar (Var name1 type1)) b1, TAbs (TVar (Var name2 type2)) b2) ->
+                    type1 == type2 &&
+                    equiv b1 b2 newmap (lambdaDepth + 1)
+                    where newmap = (lambdaDepth + 1, ((Var name1 type1),(Var name2 type2))) : varmap
+
+                (TVar a1, TVar a2) ->
+                    -- the order of the pair is important
+                    (lambdaDepth, (a1,a2)) `elem` varmap ||
+                    not ((lambdaDepth, (a1,a2)) `elem` varmap) && a1 == a2
+
+                (_,_) -> False
+    in equiv a b [] 0
+
+
+alphaConvert :: Term -> Term -> Term
+alphaConvert (TConst a ty) (TConst _ _) = TConst a ty
+alphaConvert (TApp a1 b1) (TApp a2 b2) = TApp (alphaConvert a1 a2) (alphaConvert b1 b2)
+alphaConvert (TVar v) (TVar _) = TVar v
+alphaConvert (TAbs v1 a) (TAbs v2 b) = substitute ([],[(tVar v1,v2)]) (TAbs v1 (alphaConvert a b))
+
+
+alphaConvertList :: [Term] -> [Term] -> [Term]
+alphaConvertList a b = map (\x -> alphaConvert (fst x) (snd x)) (zip a b)
+
+
+substitute :: Substitution -> Term -> Term
+substitute (tymap,vmap) term =
+    let typesub =
+            (\x y ->
+                case y of
+                    (TConst a ty) -> if (ty == (TypeVar . fst $ x))
+                                     then TConst a (snd x)
+                                     else TConst a ty
+                    (TApp a b) -> TApp (typesub x a) (typesub x b)
+                    (TAbs v a) -> TAbs v (typesub x a)
+                    (TVar v) -> TVar v)
+        varsub =
+            (\x y ->
+                case y of
+                    (TConst a ty) -> TConst a ty
+                    (TApp a b) -> TApp (varsub x a) (varsub x b)
+                    (TVar v) -> if (v == (fst x))
+                                then snd x
+                                else TVar v
+                    (TAbs v a) -> let safe = rename (TAbs v a) (union [fst x] (containsVars . snd $ x))
+                                  in case safe of
+                                         (TAbs m n) -> TAbs m (varsub x n))
+        tydone = foldl' (\x y -> typesub y x) term tymap
+        vdone = foldl' (\x y -> varsub y x) tydone vmap
+    in vdone
+
+
+containsVars :: Term -> [Var]
+containsVars t =
+    let f = (\term list ->
+            case term of
+                (TConst a b) -> list
+                (TApp a b) -> union list ((f a list) ++ (f b list))
+                (TVar a) -> union list [a]
+                (TAbs a b) -> union list ([tVar a] ++ (f b list)))
+    in f t []
+
+
+rename :: Term -> [Var] -> Term
+rename (TAbs (TVar v) t) varlist =
+    let doRename =
+            (\x y z -> case x of
+                           (TAbs (TVar a) b) -> if (a == y)
+                                         then TAbs (TVar z) (doRename b y z)
+                                         else TAbs (TVar a) (doRename b y z)
+                           (TConst a b) -> TConst a b
+                           (TApp a b) -> TApp (doRename a y z) (doRename b y z)
+                           (TVar a) -> if (a == y)
+                                         then TVar z
+                                         else TVar a)
+        findSafe =
+            (\x y -> if (x `elem` y)
+                     then case x of
+                              (Var a b) ->
+                                  case a of
+                                      (Name c d) -> findSafe (Var (Name c (d ++ "'")) b) y
+                     else x)
+    in if (v `elem` varlist)
+       then doRename (TAbs (TVar v) t) v (findSafe v varlist)
+       else TAbs (TVar v) t
+
+
+typeOf :: Term -> Type
+typeOf (TConst c ty) = ty
+typeOf (TVar v) = varTy v
+typeOf (TAbs v t) = typeFunc (typeOf v) (typeOf t)
+typeOf (TApp f _) = 
+    -- type of f is of the form [[a,b], "->"]
+    last . aType . typeOf $ f
+
+
+mkEquals :: Term -> Term -> Term
+mkEquals lhs rhs =
+    let eqConst = TConst (Const (Name [] "=")) (mkEqualsType (typeOf lhs))
+    in TApp (TApp eqConst lhs) rhs
+
+
+getlhs :: Term -> Term
+getlhs (TApp (TApp eq lhs) _)
+    | (isEq eq) = lhs
+
+
+getrhs :: Term -> Term
+getrhs (TApp (TApp eq _) rhs)
+    | (isEq eq) = rhs
+
+
+isEq :: Term -> Bool
+isEq (TConst (Const (Name [] "=")) _) = True
+isEq _ = False
diff --git a/Theorem.hs b/Theorem.hs
new file mode 100644
index 0000000..c4a36c8
--- /dev/null
+++ b/Theorem.hs
@@ -0,0 +1,19 @@
+module Theorem (
+	Theorem(..),
+	) where
+
+
+
+import Data.List
+import TypeVar
+import Term
+
+
+
+data Theorem = Theorem { thmHyp :: [Term]
+                       , thmCon :: Term } deriving (Eq)
+
+
+
+instance Show Theorem where
+    show a   =   (show . thmHyp $ a) ++ " |- " ++ (show . thmCon $ a)
diff --git a/TypeVar.hs b/TypeVar.hs
new file mode 100644
index 0000000..2dae613
--- /dev/null
+++ b/TypeVar.hs
@@ -0,0 +1,65 @@
+module TypeVar (
+	Number,
+
+	Name(..),
+
+	TypeOp(..),
+
+	Type(..),
+
+	Const(..),
+
+	Var(..),
+
+	mkEqualsType,
+	typeFunc
+	) where
+
+
+
+import Data.List
+
+
+
+type Number = Int
+
+data Name = Name { nameSpace :: [String]
+                 , nameId :: String } deriving (Eq)
+
+data TypeOp = TypeOp { tyOp :: Name } deriving (Eq)
+
+data Type = TypeVar { typeVar :: Name }
+          | AType { aType :: [Type]
+                  , aTypeOp :: TypeOp } deriving (Eq)
+
+data Const = Const { constName :: Name } deriving (Eq)
+
+data Var = Var { varName :: Name
+               , varTy :: Type } deriving (Eq)
+
+
+
+instance Show Name where
+    show a   =   intercalate "." (nameSpace a ++ [nameId a])
+
+instance Show TypeOp where
+    show a   =   "typeOp " ++ (show $ tyOp a)
+
+instance Show Type where
+    show (TypeVar tyVar)   =   "typeVar " ++ (show tyVar)
+    show (AType list typeOp) =   "type " ++ (show $ tyOp typeOp) ++ " " ++ (show list)
+
+instance Show Const where
+    show (Const a)   =   show a
+
+instance Show Var where
+    show (Var a _)   =   show a
+
+
+
+mkEqualsType :: Type -> Type
+mkEqualsType ty = typeFunc (AType [] (TypeOp (Name [] "bool"))) (typeFunc ty ty)
+
+
+typeFunc :: Type -> Type -> Type
+typeFunc ty1 ty2 = AType [ty1,ty2] (TypeOp (Name [] "->"))