Advertisement
Not a member of Pastebin yet?
Sign Up,
it unlocks many cool features!
- do
- done <- isEOF
- if done
- then return (good, lastChecked, fstTerm)
- else do inp <- getLine
- let e = parseExpr inp
- let (isAx, axNum) = isAxiom e
- let (canBeMP, impl, leftImpl) = canBeMPonused e (Map.lookup e exprsFromRightParts) good
- if term /= e
- then if e `Map.member` good
- then getCorrectStatements term hyps good exprsFromRightParts (num + 1) e fstTerm
- else if isAx
- then getCorrectStatements term hyps (Map.insert e (Axiom num axNum) good)
- (let (Binary Impl a b) = e in (insertToMap b e num exprsFromRightParts)) (num + 1) e fstTerm
- else if e `Map.member` hyps
- then if isImpl e
- then getCorrectStatements term hyps (Map.insert e (Hyp num (hyps Map.! e)) good)
- (let (Binary Impl a b) = e in (insertToMap b e num exprsFromRightParts)) (num + 1) e fstTerm
- else getCorrectStatements term hyps (Map.insert e (Hyp num (hyps Map.! e)) good) exprsFromRightParts (num + 1) e fstTerm
- else if canBeMP
- then if isImpl e
- then let (Binary Impl a b) = e in getCorrectStatements term hyps (Map.insert e (Mp num impl leftImpl) good)
- (insertToMap b e num exprsFromRightParts) (num + 1) e fstTerm
- else getCorrectStatements term hyps (Map.insert e (Mp num impl leftImpl) good) exprsFromRightParts (num + 1) e fstTerm
- else return (Map.empty, e, 0)
- else if e `Map.member` good
- then getCorrectStatements term hyps good exprsFromRightParts (num + 1) e fstTerm
- else if isAx
- then getCorrectStatements term hyps (Map.insert e (Axiom num axNum) good)
- (let (Binary Impl a b) = e in (insertToMap b e num exprsFromRightParts)) (num + 1) e num
- else if e `Map.member` hyps
- then if isImpl e
- then getCorrectStatements term hyps (Map.insert e (Hyp num (hyps Map.! e)) good)
- (let (Binary Impl a b) = e in (insertToMap b e num exprsFromRightParts)) (num + 1) e num
- else getCorrectStatements term hyps (Map.insert e (Hyp num (hyps Map.! e)) good) exprsFromRightParts (num + 1) e num
- else if canBeMP
- then if isImpl e
- then let (Binary Impl a b) = e in getCorrectStatements term hyps (Map.insert e (Mp num impl leftImpl) good)
- (insertToMap b e num exprsFromRightParts) (num + 1) e num
- else getCorrectStatements term hyps (Map.insert e (Mp num impl leftImpl) good) exprsFromRightParts (num + 1) e num
- else return (Map.empty, e, 0)
Advertisement
Add Comment
Please, Sign In to add comment
Advertisement