summaryrefslogtreecommitdiff
path: root/src/Library/Object.hs
blob: dd65ded9c1244619dd85a349df72b75a9d98bd40 (plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
module Library.Object (
	Object(..),
    objNum,
    objName,
    objList,
    objTyOp,
    objType,
    objConst,
    objVar,
    objTerm,
    objThm,

	List,

    makeSubst
	) where



import Data.Maybe
import Data.List
import Library.TypeVar
import Library.Term
import Library.Theorem



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]



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



makeSubst :: [Object] -> Maybe Substitution
makeSubst l =
    let list = (map (mapMaybe objList)) . (mapMaybe objList) $ l
        f g h x = (g . head $ x, h . last $ x)
        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