Ticket #3782: newprop.hs

File newprop.hs, 11.3 KB (added by guest, 4 years ago)
Line 
1{-# LANGUAGE PArr, ParallelListComp #-}
2{-# OPTIONS -fvectorise #-}
3
4module Main where
5import Data.Maybe
6import Control.Monad
7import qualified Prelude
8import Data.Array.Parallel.Prelude
9import Data.Array.Parallel.Prelude.Int
10
11
12data Aprop = A Int
13           deriving (Prelude.Eq, Prelude.Show)
14
15aeq :: Aprop -> Aprop -> Bool
16aeq (A a) (A b) = (a == b)
17
18data Prop = Atom Aprop
19          | And Prop Prop
20          | Or Prop Prop
21          | Imp Prop Prop
22          | Top
23          | Bot
24            deriving (Prelude.Eq, Prelude.Show)
25
26propEq :: Prop -> Prop -> Bool
27propEq Top Top = True
28propEq Bot Bot = True
29propEq (Imp a b) (Imp c d) =  (propEq a c) && (propEq b d) 
30propEq (And a b) (And c d) =  (propEq a c) && (propEq b d) 
31propEq (Or a b) (Or c d) =  (propEq a c) && (propEq b d) 
32propEq (Atom a) (Atom b) = aeq a b
33propEq _ _ = False                 
34
35type Ctx = [Prop]
36
37findIn :: Ctx -> Prop -> Bool
38findIn [] x = False
39findIn (a : aa) x =   (propEq x  a) || (findIn aa x)
40
41data Proof = 
42         Assumption  Aprop
43       | AndL1 Prop  Proof
44       | AndL2 Prop  Proof
45       | OrL   Prop  Proof  Proof
46       | ImpL  Prop  Proof 
47       | AndR  Prop  Proof  Proof
48       | OrR1  Prop  Proof
49       | OrR2  Prop  Proof 
50       | ImpR  Prop  Proof
51       | BotL  Prop 
52       | TopR 
53         deriving Prelude.Show
54
55findProof :: Ctx -> Prop -> Int -> Maybe Proof
56findProof _ _ 0 = Nothing
57findProof ctx goal n =  (m1 `mplus` m2)
58    where
59      m1 = (tryRight ctx goal n) 
60      m2 = (tryLeft ctx goal n)
61
62tryRight :: Ctx -> Prop -> Int -> Maybe Proof
63tryRight _ _ 0 = Nothing
64tryRight ctx (Atom a) n = if (findIn ctx (Atom a)) then 
65                              (Just (Assumption a))
66                          else Nothing
67tryRight ctx (And a b) n = maybe where
68    (m1,m2) = ((findProof ctx a (n-1)),(findProof ctx b (n-1)))
69    maybe = case (m1,m2) of
70              (Just p1, Just p2) -> (Just (AndR (And a b) p1 p2))
71              _ -> Nothing
72tryRight ctx (Or a b) n = maybe where
73    m1  = findProof ctx a (n-1)
74    m2 = m1 >>= (\ x -> (Just (OrR1 (Or a b) x)))
75    maybe = m1 `mplus`  ((findProof ctx b (n-1)) >>= 
76                          (\ x -> (Just (OrR2 (Or a b) x))))
77tryRight ctx (Imp a b) n = 
78    (findProof (a : ctx) b (n-1)) >>= (\ x -> (Just (ImpR (Imp a b) x)))
79
80tryRight ctx Top n = (Just TopR)
81tryRight ctx Bot n = Nothing
82
83sMap :: ( a -> Maybe b) -> [a] -> Maybe b
84sMap f [] = Nothing
85sMap f (a : aa) = maybe where
86    m1 = (f a)
87    maybe = case m1 of Nothing -> (sMap  f aa)
88                       _  -> m1
89
90tryLeft :: Ctx -> Prop -> Int -> Maybe Proof
91tryLeft _ _ 0 = Nothing
92tryLeft ctx goal n = sMap (\ x -> (tryLeftHelper ctx x goal n)) ctx
93
94tryLeftHelper :: Ctx -> Prop -> Prop -> Int -> Maybe Proof
95tryLeftHelper ctx (Atom a) (Atom b) n = 
96    if (aeq a b) then (Just (Assumption a))
97    else Nothing
98tryLeftHelper ctx (And a b) g n = maybe where
99    m1 = (findProof (a : ctx) g (n-1)) >>= (\ x -> (Just (AndL1 g x)))
100    maybe = case m1 of Nothing -> (findProof  (b : ctx) g (n-1)) >>= 
101                               (\ x -> (Just (AndL2 g x)))
102                       _ -> m1
103tryLeftHelper ctx (Or a b) g n = maybe where
104    maybe = (findProof (a : ctx) g (n-1)) >>= 
105            (\ x -> (findProof (b : ctx) g (n-1)) >>= 
106                    (\ y -> (Just (OrL g x y))))
107tryLeftHelper ctx (Imp a b) g n = maybe where
108    maybe = if (findIn ctx a) then
109                (findProof (b : ctx) g (n-1)) >>= (\ x -> (Just (ImpL g x)))
110            else Nothing
111tryLeftHelper ctx Bot g n = (Just (BotL g))
112tryLeftHelper ctx Top g n = Nothing
113tryLeftHelper _ _ _ _ = Nothing
114
115test1 :: Maybe Proof
116test1 = try where
117    a1 = (Atom (A 1))
118    a2  = (Atom (A 2))
119    a3 = (Atom (A 3))
120    goal = (And 
121            (And (And 
122            (And
123            (And 
124            (And (And (And a3 a2) (And (And a2 a1) (And a1 a3)))
125            (And (Imp (And a1 a1) (Or a1 a2)) (And (And a2 a1)(Or a2 a1))))
126            (And (And (And a3 a2) (And (And a2 a1) (And a1 a3)))
127            (And (Imp (And a1 a1) (Or a1 a2)) (And (And a2 a1)(Or a2 a1))))) 
128            (And 
129            (And (And (And a3 a2) (And (And a2 a1) (And a1 a3)))
130            (And (Imp (And a1 a1) (Or a1 a2)) (And (And a2 a1)(Or a2 a1))))
131            (And (And (And a3 a2) (And (And a2 a1) (And a1 a3)))
132            (And (Imp (And a1 a1) (Or a1 a2)) (And (And a2 a1)(Or a2 a1))))))
133            (And
134            (And 
135            (And (And (And a3 a2) (And (And a2 a1) (And a1 a3)))
136            (And (Imp (And a1 a1) (Or a1 a2)) (And (And a2 a1)(Or a2 a1))))
137            (And (And (And a3 a2) (And (And a2 a1) (And a1 a3)))
138            (And (Imp (And a1 a1) (Or a1 a2)) (And (And a2 a1)(Or a2 a1))))) 
139            (And 
140            (And (And (And a3 a2) (And (And a2 a1) (And a1 a3)))
141            (And (Imp (And a1 a1) (Or a1 a2)) (And (And a2 a1)(Or a2 a1))))
142            (And (And (And a3 a2) (And (And a2 a1) (And a1 a3)))
143            (And (Imp (And a1 a1) (Or a1 a2)) (And (And a2 a1)(Or a2 a1)))))))
144            (And 
145            (And
146            (And 
147            (And (And (And a3 a2) (And (And a2 a1) (And a1 a3)))
148            (And (Imp (And a1 a1) (Or a1 a2)) (And (And a2 a1)(Or a2 a1))))
149            (And (And (And a3 a2) (And (And a2 a1) (And a1 a3)))
150            (And (Imp (And a1 a1) (Or a1 a2)) (And (And a2 a1)(Or a2 a1))))) 
151            (And 
152            (And (And (And a3 a2) (And (And a2 a1) (And a1 a3)))
153            (And (Imp (And a1 a1) (Or a1 a2)) (And (And a2 a1)(Or a2 a1))))
154            (And (And (And a3 a2) (And (And a2 a1) (And a1 a3)))
155            (And (Imp (And a1 a1) (Or a1 a2)) (And (And a2 a1)(Or a2 a1))))))
156            (And
157            (And 
158            (And (And (And a3 a2) (And (And a2 a1) (And a1 a3)))
159            (And (Imp (And a1 a1) (Or a1 a2)) (And (And a2 a1)(Or a2 a1))))
160            (And (And (And a3 a2) (And (And a2 a1) (And a1 a3)))
161            (And (Imp (And a1 a1) (Or a1 a2)) (And (And a2 a1)(Or a2 a1))))) 
162            (And 
163            (And (And (And a3 a2) (And (And a2 a1) (And a1 a3)))
164            (And (Imp (And a1 a1) (Or a1 a2)) (And (And a2 a1)(Or a2 a1))))
165            (And (And (And a3 a2) (And (And a2 a1) (And a1 a3)))
166            (And (Imp (And a1 a1) (Or a1 a2)) (And (And a2 a1)(Or a2 a1))))))))
167            (And
168            (And 
169            (And
170            (And 
171            (And (And (And a3 a2) (And (And a2 a1) (And a1 a3)))
172            (And (Imp (And a1 a1) (Or a1 a2)) (And (And a2 a1)(Or a2 a1))))
173            (And (And (And a3 a2) (And (And a2 a1) (And a1 a3)))
174            (And (Imp (And a1 a1) (Or a1 a2)) (And (And a2 a1)(Or a2 a1))))) 
175            (And 
176            (And (And (And a3 a2) (And (And a2 a1) (And a1 a3)))
177            (And (Imp (And a1 a1) (Or a1 a2)) (And (And a2 a1)(Or a2 a1))))
178            (And (And (And a3 a2) (And (And a2 a1) (And a1 a3)))
179            (And (Imp (And a1 a1) (Or a1 a2)) (And (And a2 a1)(Or a2 a1))))))
180            (And
181            (And 
182            (And (And (And a3 a2) (And (And a2 a1) (And a1 a3)))
183            (And (Imp (And a1 a1) (Or a1 a2)) (And (And a2 a1)(Or a2 a1))))
184            (And (And (And a3 a2) (And (And a2 a1) (And a1 a3)))
185            (And (Imp (And a1 a1) (Or a1 a2)) (And (And a2 a1)(Or a2 a1))))) 
186            (And 
187            (And (And (And a3 a2) (And (And a2 a1) (And a1 a3)))
188            (And (Imp (And a1 a1) (Or a1 a2)) (And (And a2 a1)(Or a2 a1))))
189            (And (And (And a3 a2) (And (And a2 a1) (And a1 a3)))
190            (And (Imp (And a1 a1) (Or a1 a2)) (And (And a2 a1)(Or a2 a1)))))))
191            (And 
192            (And
193            (And 
194            (And (And (And a3 a2) (And (And a2 a1) (And a1 a3)))
195            (And (Imp (And a1 a1) (Or a1 a2)) (And (And a2 a1)(Or a2 a1))))
196            (And (And (And a3 a2) (And (And a2 a1) (And a1 a3)))
197            (And (Imp (And a1 a1) (Or a1 a2)) (And (And a2 a1)(Or a2 a1))))) 
198            (And 
199            (And (And (And a3 a2) (And (And a2 a1) (And a1 a3)))
200            (And (Imp (And a1 a1) (Or a1 a2)) (And (And a2 a1)(Or a2 a1))))
201            (And (And (And a3 a2) (And (And a2 a1) (And a1 a3)))
202            (And (Imp (And a1 a1) (Or a1 a2)) (And (And a2 a1)(Or a2 a1))))))
203            (And
204            (And 
205            (And (And (And a3 a2) (And (And a2 a1) (And a1 a3)))
206            (And (Imp (And a1 a1) (Or a1 a2)) (And (And a2 a1)(Or a2 a1))))
207            (And (And (And a3 a2) (And (And a2 a1) (And a1 a3)))
208            (And (Imp (And a1 a1) (Or a1 a2)) (And (And a2 a1)(Or a2 a1))))) 
209            (And 
210            (And (And (And a3 a2) (And (And a2 a1) (And a1 a3)))
211            (And (Imp (And a1 a1) (Or a1 a2)) (And (And a2 a1)(Or a2 a1))))
212            (And (And (And a3 a2) (And (And a2 a1) (And a1 a3)))
213            (And (Imp (And a1 a1) (Or a1 a2)) (And (And a2 a1)(Or a2 a1)))))))))
214    ctx = [a1, a2,a3]
215    p =  findProof ctx goal 100
216    try =  p
217          --  case p of Nothing -> Prelude.print "Sad. Try again."
218            --          (Just j) -> Prelude.print j
219
220     -- A test that makes a straightish tree with only atomis in the ctx
221test2 :: Maybe Proof 
222test2 = try where
223    makeTest :: Int -> Prop -> Prop
224    makeTest i c = if i == 0 then c
225                else if (i`mod`2) == 0 then (makeTest (i-1) (And (Atom (A i)) c))
226                else (makeTest (i-1) (Or (Atom (A i)) c))
227    makeCtx :: Int -> Ctx -> Ctx
228    makeCtx 0 g = g
229    makeCtx n g = (makeCtx (n-1) ((Atom (A n)) : g))
230    goal = makeTest 100 (Atom (A 101))
231    ctx = makeCtx 101 []
232    try = findProof ctx goal 200
233
234
235-- A test that makes a total conjunction with atoms in the ctx
236test3 :: Maybe Proof 
237test3 = try where
238    makeTest :: Int -> Prop -> Prop
239    makeTest i c = if i == 0 then c
240                else (makeTest (i-1)  (And (Atom (A i)) c))
241
242    makeCtx :: Int -> Ctx -> Ctx
243    makeCtx 0 g = g
244    makeCtx n g = (makeCtx (n-1) ((Atom (A n)) : g))
245    goal = makeTest 100 (Atom (A 101))
246    ctx = makeCtx 101 [(Atom (A 101))]
247    try = findProof ctx goal 200
248
249
250
251-- A test with goal of full implications and a ctx of atoms
252test4 :: Maybe Proof 
253test4 = try where
254    makeTest :: Int -> Prop -> Prop
255    makeTest i c = if i == 0 then c
256                   else (makeTest (i-1) (Imp (Atom (A i)) c))
257    makeCtx :: Int -> Ctx -> Ctx
258    makeCtx 0 g = g
259    makeCtx n g = (makeCtx (n-1) ( (Atom (A n)) : g))
260    goal = makeTest 100 (Atom (A 101))
261    ctx = makeCtx 101 [ (Atom (A 101))]
262    try = findProof ctx goal 200
263                   
264{-
265testall :: Int
266testall = case (test1,test2,test3,test4,test5,test6,test7,test8,test9,test10,test11,test12,test13,test14,test15,test16,test17,test18,test19,test20) of
267 (Just _, Just _ ,Just _, Just _ ,Just _, Just _ ,Just _, Just _ ,Just _, Just _ ,Just _, Just _ ,Just _, Just _ ,Just _, Just _ ,Just _, Just _ ,Just _, Just _ )-> 1
268 _ -> 0
269-}
270
271
272testall :: Int 
273testall = case (test1,test2,test3,test4) of 
274            (Just _, Just _ , Just _ , Just _) -> 1
275            (Just _, _ ,_,_) -> 2
276            (_, Just _ ,_ ,_) -> 3
277            (_,_,Just _ ,_) -> 4
278            (_,_,_, Just _ ) -> 5
279            _ -> 0
280
281{-
282testall :: Int
283testall = case test4 of
284            (Just _ ) -> 2
285            _ -> 0
286
287-}
288main :: Prelude.IO ()
289main = 
290 case testall of
291   1 -> return () --print "Yay! you wrotee good tests!"
292   2 -> return () --print "First one passed"
293   3 -> return () --print "First failed, second passed"
294   4 -> return () --print "First two failed third passed"
295   5 -> return () --print "First three failed fourth passed"
296   0 -> return () --print "All failed"
297   _ -> return ()
298