-
Notifications
You must be signed in to change notification settings - Fork 2
/
Copy pathLogic.hs
159 lines (141 loc) · 5.58 KB
/
Logic.hs
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
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
-- This file is part of tersmu
-- Copyright (C) 2014 Martin Bays <[email protected]>
--
-- This program is free software: you can redistribute it and/or modify
-- it under the terms of version 3 of the GNU General Public License as
-- published by the Free Software Foundation.
--
-- You should have received a copy of the GNU General Public License
-- along with this program. If not, see http://www.gnu.org/licenses/.
{-# LANGUAGE DeriveDataTypeable #-}
module Logic where
import Control.Monad.State
import Data.Data
-- |Prop: abstract proposition type, allowing for generalised quantifiers,
-- structured relations and terms, modal operators, and non-logical
-- connectives.
data Prop r t c o q
= Not (Prop r t c o q)
| Connected Connective (Prop r t c o q) (Prop r t c o q)
| NonLogConnected c (Prop r t c o q) (Prop r t c o q)
| Quantified q (Maybe (Int -> Prop r t c o q)) (Int -> Prop r t c o q)
| Modal o (Prop r t c o q)
| Rel r [t]
| Eet
deriving (Typeable,Data)
class Dummyful a where dummy :: a
instance Dummyful Int where dummy = -1
instance (Typeable a, Dummyful a, Data p) => Data (a -> p) where
-- XXX: these dummy instances don't cut it when we really want to traverse
-- over a proposition - see gsubstituteIn
gfoldl k z f = z const `k` f dummy
gunfold k z c = k $ z const
toConstr f = mkConstr (dataTypeOf f) "Dummyful -> " [] Prefix
dataTypeOf f = mkDataType "DataIntFun" $ [toConstr f]
data Connective = And | Or | Impl | Equiv
deriving (Eq, Ord,Typeable,Data)
data LojQuantifier = Exists | Forall | Exactly Int
deriving (Eq, Ord,Typeable,Data)
instance Show Connective where
show And = "/\\"
show Or = "\\/"
show Impl = "-->"
show Equiv = "<->"
instance Show LojQuantifier where
show Exists = "EX"
show Forall = "FA"
show (Exactly n) = "EQ(" ++ show n ++ ")"
class Term t where
var :: Int -> t
class Rel r where
relstr :: r -> String
-- terpProp: lift an interpretation of atomic formulae, operators, and
-- quantifiers to an interpretation of arbitrary formula
terpProp ::
(r1 -> [t1] -> Prop r2 t2 c o2 q2)
-> (o1 -> o2)
-> (q1 -> q2)
-> Prop r1 t1 c o1 q1 -> Prop r2 t2 c o2 q2
terpProp terpAtomic terpOp terpQ p = terpProp' p
where terpProp' (Rel r ts) = terpAtomic r ts
terpProp' (Quantified q r p) =
Quantified (terpQ q) (case r of
Nothing -> Nothing
Just r' -> Just (\v -> terpProp' $ r' v))
(\v -> terpProp' $ p v)
terpProp' (Not p) = Not $ terpProp' p
terpProp' (Connected c p1 p2) =
Connected c (terpProp' p1) (terpProp' p2)
terpProp' (NonLogConnected c p1 p2) =
NonLogConnected c (terpProp' p1) (terpProp' p2)
terpProp' Eet = Eet
terpProp' (Modal o p) = Modal (terpOp o) (terpProp' p)
bigAnd :: [Prop r t c o q] -> Prop r t c o q
bigAnd ps = bigAnd' $ filter (\p -> case p of {Not Eet -> False; _ -> True}) ps
where bigAnd' [] = Not Eet
bigAnd' [p] = p
bigAnd' (p:ps) = Connected And p (bigAnd' ps)
-- instance (Rel r, Term t) => Show (Prop r t) where
-- show p = evalState (serialise p False) 1
-- type PropPrintFlags = Bool -- insert newlines and tabs?
-- serialise :: (Rel r, Term t) => (Prop r t) -> PropPrintFlags -> State Int String
-- serialise p f = _serialise p f 0
--
-- _serialise :: (Rel r, Term t) => Prop r t -> PropPrintFlags -> Int -> State Int String
-- _serialise (Not p) f d =
-- do s <- _serialise p f (d+1)
-- return $ "! ( " ++ s ++ " )"
-- _serialise (Connected c p1 p2) f d =
-- do s1 <- _serialise p1 f (d+1); s2 <- _serialise p2 f (d+1);
-- return $ "( " ++ s1 ++ " " ++ show c ++ " " ++
-- (if f then "\n"++(replicate (d+1) '\t') else "") ++ s2 ++ " )"
-- _serialise (Quantified q r p::Prop r t) f d =
-- do n <- get
-- put $ n+1
-- case r of Nothing -> do s <- _serialise (p n) f (d+1)
-- return $ show q ++ " " ++
-- objlogstr (var n::t) ++
-- ". " ++ s
-- Just r' -> do s1 <- _serialise (r' n) f (d+1)
-- s2 <- _serialise (p n) f (d+1)
-- return $ show q ++ " " ++
-- objlogstr (var n::t) ++
-- ":(" ++ s1 ++ ")" ++
-- ". " ++ s2
-- _serialise (Rel r ts) f d =
-- return $ relstr r ++ "(" ++ unwords (map objlogstr ts) ++ ")"
-- _serialise Eet f d = return "_|_"
-- XXX: broken
{-
pnf :: (Prop r t) -> (Prop r t)
pnf (Impl p1 p2) = pnf $ Or (Not p1) p2
pnf (Equiv p1 p2) = pnf $ Or (And (Not p1) p2)
(And p1 (Not p2))
pnf (Or p1 p2) =
pnfOr (pnf p1) (pnf p2)
where pnfOr (Forall f) p2 = pnf $ Forall (\x -> Or (f x) p2)
pnfOr (Exists f) p2 = pnf $ Exists (\x -> Or (f x) p2)
pnfOr p1 (Forall f) = pnf $ Forall (\x -> Or p1 (f x))
pnfOr p1 (Exists f) = pnf $ Exists (\x -> Or p1 (f x))
pnfOr p1 p2 = (Or p1 p2)
pnf (And p1 p2) =
pnfAnd (pnf p1) (pnf p2)
where pnfAnd (Forall f) p2 = pnf $ Forall (\x -> And (f x) p2)
pnfAnd (Exists f) p2 = pnf $ Exists (\x -> And (f x) p2)
pnfAnd p1 (Forall f) = pnf $ Forall (\x -> And p1 (f x))
pnfAnd p1 (Exists f) = pnf $ Exists (\x -> And p1 (f x))
pnfAnd (Or p3 p4) p2 = pnf $ Or (And p3 p2) (And p4 p2)
pnfAnd p1 (Or p3 p4) = pnf $ Or (And p1 p3) (And p1 p4)
pnfAnd p1 p2 = (And p1 p2)
pnf (Not p) =
pnfNot (pnf p)
where pnfNot (Forall f) = pnf $ Exists (\x -> Not (f x))
pnfNot (Exists f) = pnf $ Forall (\x -> Not (f x))
pnfNot (And p1 p2) = pnf $ Or (Not p1) (Not p2)
pnfNot (Or p1 p2) = pnf $ And (Not p1) (Not p2)
pnfNot (Not p) = p
pnfNot p = (Not p)
pnf (Forall f) = Forall (\x -> pnf (f x))
pnf (Exists f) = Exists (\x -> pnf (f x))
pnf p = p
-}