1 files changed, 91 insertions, 12 deletions
diff --git a/Object.hs b/Object.hs
index 5d0e71e..0fa1736 100644
--- a/Object.hs
+++ b/Object.hs
@@ -1,5 +1,14 @@
 module Object (
 	Object(..),
+    objNum,
+    objName,
+    objList,
+    objTyOp,
+    objType,
+    objConst,
+    objVar,
+    objTerm,
+    objThm,
 
 	List,
 
@@ -8,6 +17,7 @@ module Object (
 
 
 
+import Data.Maybe
 import Data.List
 import TypeVar
 import Term
@@ -15,15 +25,15 @@ 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, Ord)
+data Object = ObjNum Number
+            | ObjName Name
+            | ObjList List
+            | ObjTyOp TypeOp
+            | ObjType Type
+            | ObjConst Const
+            | ObjVar Var
+            | ObjTerm Term
+            | ObjThm Theorem deriving (Eq, Ord)
 
 type List = [Object]
 
@@ -42,8 +52,77 @@ instance Show Object where
 
 
 
-makeSubst :: [Object] -> Substitution
+makeSubst :: [Object] -> Maybe Substitution
 makeSubst l =
-    let list = (map (map objList)) . (map objList) $ l
+    let list = (map (mapMaybe objList)) . (mapMaybe objList) $ l
         f = (\g h x -> (g . head $ x, h . last $ x))
-    in f (map (f objName objType)) (map (f objVar objTerm)) list
+        check = f (map (f objName objType)) (map (f objVar objTerm)) list
+        g = all (\x -> (isJust . fst $ x) && (isJust . snd $ x))
+        h = (\x -> (fromJust . fst $ x, fromJust . snd $ x))
+    in if ((g . fst $ check) && (g . snd $ check))
+       then Just (map h (fst check), map h (snd check))
+       else Nothing
+
+
+objNum :: Object -> Maybe Number
+objNum obj =
+    case (obj) of
+        (ObjNum n) -> Just n
+        (_) -> Nothing
+
+
+objName :: Object -> Maybe Name
+objName obj =
+    case (obj) of
+        (ObjName n) -> Just n
+        (_) -> Nothing
+
+
+objList :: Object -> Maybe List
+objList obj =
+    case (obj) of
+        (ObjList l) -> Just l
+        (_) -> Nothing
+
+
+objTyOp :: Object -> Maybe TypeOp
+objTyOp obj =
+    case (obj) of
+        (ObjTyOp tyop) -> Just tyop
+        (_) -> Nothing
+
+
+objType :: Object -> Maybe Type
+objType obj =
+    case (obj) of
+        (ObjType ty) -> Just ty
+        (_) -> Nothing
+
+
+objConst :: Object -> Maybe Const
+objConst obj =
+    case (obj) of
+        (ObjConst c) -> Just c
+        (_) -> Nothing
+
+
+objVar :: Object -> Maybe Var
+objVar obj =
+    case (obj) of
+        (ObjVar var) -> Just var
+        (_) -> Nothing
+
+
+objTerm :: Object -> Maybe Term
+objTerm obj =
+    case (obj) of
+        (ObjTerm term) -> Just term
+        (_) -> Nothing
+
+
+objThm :: Object -> Maybe Theorem
+objThm obj =
+    case (obj) of
+        (ObjThm thm) -> Just thm
+        (_) -> Nothing
+