Folly 0.1.4.1 → 0.1.4.2
raw patch · 4 files changed
+303/−3 lines, 4 files
Files
- Folly.cabal +2/−3
- src/Folly/Lexer.hs +116/−0
- src/Folly/Parser.hs +156/−0
- src/Folly/Theorem.hs +29/−0
Folly.cabal view
@@ -2,7 +2,7 @@ -- see http://haskell.org/cabal/users-guide/ name: Folly-version: 0.1.4.1+version: 0.1.4.2 synopsis: A first order logic library in Haskell description: An implementation of first order logic in Haskell that includes a library of modules for incorporating first@@ -20,8 +20,7 @@ cabal-version: >=1.8 library- exposed-modules: Folly.Formula, Folly.Unification, Folly.Resolution, Folly.Utils- -- other-modules: + exposed-modules: Folly.Formula, Folly.Unification, Folly.Resolution, Folly.Utils, Folly.Theorem, Folly.Lexer, Folly.Parser build-depends: base < 6, containers hs-source-dirs: src
+ src/Folly/Lexer.hs view
@@ -0,0 +1,116 @@+module Folly.Lexer(+ Token, name, isVar, isPred, pos,+ testOp, testVar, testQuant,+ testPred, testSep,+ lexer) where++import Text.Parsec.Pos+import Text.ParserCombinators.Parsec+import Folly.Utils++data Token = + Var String SourcePos |+ Pred String SourcePos |+ Sep String SourcePos |+ Op String SourcePos |+ Quant String SourcePos |+ Res String SourcePos++instance Show Token where+ show = showTok+ +instance Eq Token where+ (==) = tokEqual+ +isVar (Var _ _) = True+isVar _ = False++isPred (Pred _ _) = True+isPred _ = False++name (Var n _) = n+name (Pred n _) = n+name (Sep n _) = n+name (Op n _) = n+name (Res n _) = n+name (Quant n _) = n++pos (Var _ p) = p+pos (Pred _ p) = p+pos (Sep _ p) = p+pos (Op _ p) = p+pos (Res _ p) = p+pos (Quant _ p) = p++testVar s = Var s (newPos "DUMMY" 0 0)+testPred s = Pred s (newPos "DUMMY" 0 0)+testSep s = Sep s (newPos "DUMMY" 0 0)+testOp s = Sep s (newPos "DUMMY" 0 0)+testRes s = Res s (newPos "DUMMY" 0 0)+testQuant s = Quant s (newPos "DUMMY" 0 0)++showTok :: Token -> String+showTok t = name t++tokEqual :: Token -> Token -> Bool+tokEqual t1 t2 = name t1 == name t2++lexer :: String -> Error [Token]+lexer str = case parse parseToks "LEXER" str of+ Left err -> Failed $ show err+ Right toks -> Succeeded $ toks++parseToks = endBy parseTok spaces++parseTok = try atomicLit+ <|> try reservedWord+ <|> try predicate+ <|> try separator+ <|> try quantifier+ <|> operator++predicate = do+ pos <- getPosition+ firstChar <- upper <|> specialChar+ case firstChar of+ 'E' -> eOrQPred 'E' pos+ 'Q' -> eOrQPred 'Q' pos+ _ -> nonEQPred firstChar pos++eOrQPred firstChar pos = do+ rest <- many1 bodyChar+ return $ Pred (firstChar:rest) pos++nonEQPred firstChar pos = do+ rest <- many bodyChar+ return $ Pred (firstChar:rest) pos+ +atomicLit = do+ pos <- getPosition+ firstChar <- lower+ rest <- many bodyChar+ return $ Var (firstChar:rest) pos+ +reservedWord = do+ pos <- getPosition+ name <- try (string "HYPOTHESIS:") <|> (string "CONCLUSION:")+ return $ Res name pos++separator = do+ pos <- getPosition+ name <- choice $ map string ["(", ")", "]", "[", ",", "."]+ return $ Sep name pos++operator = do+ pos <- getPosition+ name <- choice $ map string ["~", "|", "&", "<->", "->"]+ return $ Op name pos++quantifier = do+ pos <- getPosition+ name <- choice $ map string ["E", "Q"]+ return $ Quant name pos++bodyChar = alphaNum <|> specialChar++specialChar = oneOf "!@#$%*<>?+=-_"
+ src/Folly/Parser.hs view
@@ -0,0 +1,156 @@+module Folly.Parser(+ parseFormula,+ parseTheorem) where++import Text.Parsec.Combinator+import Text.Parsec.Expr+import Text.Parsec.Pos+import Text.Parsec.Prim++import Folly.Formula+import Folly.Lexer as Lex+import Folly.Theorem+import Folly.Utils++parseTheorem :: [Token] -> Error Theorem+parseTheorem toks = case parse parseTheoremToks "PARSER" toks of+ Left err -> Failed $ show err+ Right thm -> Succeeded thm++parseTheoremToks = do+ axioms <- parseHypothesis+ hypothesis <- parseConclusion+ return $ theorem axioms hypothesis+ +parseConclusion = do+ propTok "CONCLUSION:"+ axioms <- parseForm+ return axioms+ +parseHypothesis = do+ propTok "HYPOTHESIS:"+ hypothesis <- many parseForm+ return hypothesis++parseFormula :: [Token] -> Error (Formula)+parseFormula toks = case parse parseForm "PARSER" toks of+ Left err -> Failed $ show err+ Right formula -> Succeeded formula++parseForm = buildExpressionParser table parseFactor++parseFactor = try (parseParens parseForm)+ <|> try parsePredicate+ <|> parseQuantification++table =+ [[negation],+ [conjunction],+ [disjunction],+ [implication],+ [bicondition]]++negation = Prefix parseNeg+conjunction = Infix parseCon AssocRight+disjunction = Infix parseDis AssocRight+implication = Infix parseImp AssocRight+bicondition = Infix parseBic AssocRight+--quantification = Prefix parseQuant++parseParens e = do+ propTok "("+ expr <- e+ propTok ")"+ return expr++parseQuantification = do+ quantType <- propTok "V" <|> propTok "E"+ varName <- varTok+ propTok "."+ form <- parseForm+ case (name quantType) of+ "V" -> return $ fa (var (name varName)) form+ "E" -> return $ te (var (name varName)) form+ _ -> error $ show quantType ++ " is not a quantifier"++parseNeg :: (Monad m) => ParsecT [Token] u m (Formula -> Formula)+parseNeg = do+ propTok "~"+ return $ neg+ +parseCon = do+ propTok "&"+ return $ con+ +parseDis = do+ propTok "|"+ return $ dis+ +parseImp = do+ propTok "->"+ return $ imp+ +parseBic = do+ propTok "<->"+ return $ bic++parsePredicate :: (Monad m) => ParsecT [Token] u m (Formula)+parsePredicate = do+ nameTok <- predicateTok+ propTok "["+ terms <- sepBy parseTerm (propTok ",")+ propTok "]"+ return $ pr (name nameTok) terms++parseTerm :: (Monad m) => ParsecT [Token] u m Term+parseTerm = try parseConstant <|> try parseFunc <|> parseVar++parseConstant :: (Monad m) => ParsecT [Token] u m Term+parseConstant = do+ nameTok <- predicateTok+ return $ constant (name nameTok)++parseVar :: (Monad m) => ParsecT [Token] u m Term+parseVar = do+ nameTok <- varTok+ return $ var (name nameTok)++parseFunc :: (Monad m) => ParsecT [Token] u m Term+parseFunc = do+ nameTok <- varTok+ propTok "("+ args <- sepBy parseTerm (propTok ",")+ propTok ")"+ return $ func (name nameTok) args++propTok :: (Monad m) => String -> ParsecT [Token] u m Token+propTok str = tokenPrim show updatePos hasNameStr+ where+ hasNameStr t = if (name t) == str then Just t else Nothing++predicateTok :: (Monad m) => ParsecT [Token] u m Token+predicateTok = tokenPrim show updatePos isPred+ where+ isPred t = if (Lex.isPred t) then Just t else Nothing++varTok :: (Monad m) => ParsecT [Token] u m Token+varTok = tokenPrim show updatePos isPred+ where+ isPred t = if (Lex.isVar t) then Just t else Nothing++literalTok :: (Monad m) => ParsecT [Token] u m Token+literalTok = tokenPrim show updatePos isLit+ where+ isLit t = if (Lex.isVar t) then Just t else Nothing++axiomsTok c = tokenPrim show updatePos isAxiom+ where+ isAxiom t = if (name t) == "AXIOMS:" then Just t else Nothing++hypothesisTok c = tokenPrim show updatePos isAxiom+ where+ isAxiom t = if (name t) == "HYPOTHESIS:" then Just t else Nothing++updatePos :: SourcePos -> Token -> [Token] -> SourcePos+updatePos _ _ (pt:_) = pos pt+updatePos position _ [] = position
+ src/Folly/Theorem.hs view
@@ -0,0 +1,29 @@+module Folly.Theorem(+ Theorem,+ theorem,+ hypothesis,+ conclusion) where++import Data.List as L++import Folly.Formula++data Theorem = Theorem [Formula] (Formula)+ deriving (Eq, Ord)++instance Show Theorem where+ show = showThm++showThm :: Theorem -> String+showThm (Theorem h c) = "Hypothesis:\n" ++ hypStr ++ "\n\n|=\n\n" ++ conclStr+ where+ hypStr = (L.concat $ L.intersperse "\n" $ L.map show h)+ conclStr = "Conclusion:\n" ++ show c++theorem = Theorem++hypothesis :: Theorem -> [Formula]+hypothesis (Theorem hp _) = hp++conclusion :: Theorem -> Formula+conclusion (Theorem _ c) = c