diff options
| -rw-r--r-- | .gitignore | 2 | ||||
| -rw-r--r-- | LICENSE | 20 | ||||
| -rw-r--r-- | src/Haskell/AST.hs | 52 | ||||
| -rw-r--r-- | src/Haskell/Env.hs | 29 | ||||
| -rw-r--r-- | src/Haskell/Parser.hs | 133 | ||||
| -rw-r--r-- | src/Haskell/Parser/Def.hs | 100 | ||||
| -rw-r--r-- | src/Haskell/SimpleParser.hs | 124 | ||||
| -rw-r--r-- | src/Main.hs | 58 | ||||
| -rw-r--r-- | test.txt | 10 | ||||
| -rw-r--r-- | verify-hs.cabal | 31 |
10 files changed, 559 insertions, 0 deletions
diff --git a/.gitignore b/.gitignore new file mode 100644 index 0000000..69d9df7 --- /dev/null +++ b/.gitignore @@ -0,0 +1,2 @@ +.ghc.environment.* +/dist-newstyle/ @@ -0,0 +1,20 @@ +Copyright (c) 2019 Tom Smeding + +Permission is hereby granted, free of charge, to any person obtaining +a copy of this software and associated documentation files (the +"Software"), to deal in the Software without restriction, including +without limitation the rights to use, copy, modify, merge, publish, +distribute, sublicense, and/or sell copies of the Software, and to +permit persons to whom the Software is furnished to do so, subject to +the following conditions: + +The above copyright notice and this permission notice shall be included +in all copies or substantial portions of the Software. + +THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, +EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF +MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. +IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY +CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, +TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN CONNECTION WITH THE +SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE. diff --git a/src/Haskell/AST.hs b/src/Haskell/AST.hs new file mode 100644 index 0000000..8326440 --- /dev/null +++ b/src/Haskell/AST.hs @@ -0,0 +1,52 @@ +module Haskell.AST where + + +type Name = String +type TyVar = String + +data AST = AST [Toplevel] + deriving (Show) + +data Toplevel = TopDef Def + | TopDecl Decl + | TopData Data + | TopClass Class + | TopInst Inst + deriving (Show) + +data Def = Def Name Expr + deriving (Show) + +data Expr = App Expr [Expr] + | Ref Name + | LitNum Integer + | Tup [Expr] + | Lam [Name] Expr + | Case Name [(Pat, Expr)] + deriving (Show) + +data Pat = PatAny + | PatVar Name + | PatCon Name [Pat] + | PatTup [Pat] + deriving (Show) + +data Decl = Decl Name Type + deriving (Show) + +data Type = TyTup [Type] + | TyInt + | TyFun Type Type + | TyRef Name [Type] + | TyVar Name + | TyVoid + deriving (Show) + +data Data = Data Name [TyVar] [(Name, [Type])] + deriving (Show) + +data Class = Class Name [TyVar] [Decl] + deriving (Show) + +data Inst = Inst Name Type [Def] + deriving (Show) diff --git a/src/Haskell/Env.hs b/src/Haskell/Env.hs new file mode 100644 index 0000000..21b2d4b --- /dev/null +++ b/src/Haskell/Env.hs @@ -0,0 +1,29 @@ +module Haskell.Env where + +import Control.Monad +import qualified Data.Map.Strict as Map +import Haskell.AST + + +data Env = Env { eDefs :: Map.Map Name Expr } + deriving (Show) + +emptyEnv :: Env +emptyEnv = Env Map.empty + +envFromAST :: AST -> Either String Env +envFromAST = addAST emptyEnv + +addAST :: Env -> AST -> Either String Env +addAST env (AST tops) = foldM addTop env tops + +addTop :: Env -> Toplevel -> Either String Env +addTop env (TopDef (Def n ex)) = + Right $ env { eDefs = Map.insert n ex (eDefs env) } +addTop _ _ = Left "Only plain top-level definitions supported for the moment" + +forget :: Name -> Env -> Either String Env +forget name env = + if Map.member name (eDefs env) + then Right $ env { eDefs = Map.delete name (eDefs env) } + else Left $ "Name '" ++ name ++ "' not found in environment" diff --git a/src/Haskell/Parser.hs b/src/Haskell/Parser.hs new file mode 100644 index 0000000..0f55a63 --- /dev/null +++ b/src/Haskell/Parser.hs @@ -0,0 +1,133 @@ +module Haskell.Parser where + +import Control.Monad +import Control.Monad.Identity +import Haskell.AST +import Haskell.Parser.Def +import Text.Parsec +-- import Text.Parsec.IndentParsec.Combinator +import Text.Parsec.IndentParsec.Prim + + +type Parser a = GenIndentParsecT HaskellLike String () Identity a + +parseAST :: String -> String -> Either ParseError AST +parseAST fname source = runIdentity $ runGIPT pAST () fname source + +pAST :: Parser AST +pAST = do + whiteSpace + tops <- pToplevel `sepBy` someNewline + eof + return $ AST tops + +pToplevel :: Parser Toplevel +pToplevel = choice [TopClass <$> pClass + ,TopInst <$> pInst + ,TopData <$> pData + ,TopDecl <$> pDecl + ,TopDef <$> pDef] + +pData :: Parser Data +pData = do + reserved "data" + n <- typeident + vars <- many varident + ty <- choice [do reservedOp "=" + pConstr `sepBy` reservedOp "|" + ,return []] + return $ Data n vars ty + where + pConstr = liftM2 (,) typeident (many pType) + +pClass :: Parser Class +pClass = do + reserved "class" + n <- typeident + vars <- many varident + reserved "where" + decls <- bracesBlock (semiSepOrFoldedLines pDecl) + return $ Class n vars decls + +pInst :: Parser Inst +pInst = do + reserved "instance" + (n, ty) <- pType >>= \case + TyRef n [ty] -> return (n, ty) + _ -> fail "invalid instance head" + reserved "where" + decls <- bracesBlock (semiSepOrFoldedLines pDef) + return $ Inst n ty decls + +pDecl :: Parser Decl +pDecl = do + n <- try (varident <* reservedOp "::") + ty <- pType + return $ Decl n ty + +pDef :: Parser Def +pDef = do + n <- varident + args <- many varident + reservedOp "=" + body <- pExpr + case args of + [] -> return $ Def n body + _ -> return $ Def n (Lam args body) + +pType :: Parser Type +pType = foldr1 TyFun <$> pSimpleType `sepBy` reservedOp "->" + where + pSimpleType :: Parser Type + pSimpleType = choice [do n <- typeident + args <- many pAtomicType + return (TyRef n args) + ,pAtomicType] + + pAtomicType :: Parser Type + pAtomicType = choice [typeident >>= \n -> return (TyRef n []) + ,TyVar <$> varident + ,parens (pType `sepBy` comma) >>= \case + [ty] -> return ty + tys -> return (TyTup tys)] + +pExpr :: Parser Expr +pExpr = pLam <|> pCase <|> pApp + where + pSimpleExpr = choice [LitNum <$> integer + ,Ref <$> (identifier <|> try (parens operator)) + ,parens pExpr] + + pLam = do + reservedOp "\\" + args <- many1 varident + body <- pExpr + return $ Lam args body + + pApp = App <$> pSimpleExpr <*> many pSimpleExpr + + pCase = do + reserved "case" + n <- varident + reserved "of" + arms <- bracesBlock (semiSepOrFoldedLines pCaseArm) + return $ Case n arms + + pCaseArm = do + pat <- pLargePat + reservedOp "->" + ex <- pExpr + return (pat, ex) + +pSimplePat :: Parser Pat +pSimplePat = choice [lexeme (string "_") >> return PatAny + ,PatVar <$> varident + ,typeident >>= \n -> return (PatCon n []) + ,parens pLargePat] + +pLargePat :: Parser Pat +pLargePat = choice [PatCon <$> typeident <*> many pSimplePat + ,pSimplePat] + +someNewline :: Parser () +someNewline = many (oneOf " \t") >> char '\n' >> whiteSpace diff --git a/src/Haskell/Parser/Def.hs b/src/Haskell/Parser/Def.hs new file mode 100644 index 0000000..812140c --- /dev/null +++ b/src/Haskell/Parser/Def.hs @@ -0,0 +1,100 @@ +{-# OPTIONS_GHC -Wno-missing-signatures #-} +module Haskell.Parser.Def where + +import Control.Monad.Identity +import Data.Char +import Text.Parsec +-- import qualified Text.Parsec.Language as L +import qualified Text.Parsec.Token as T +import qualified Text.Parsec.IndentParsec.Token as IT +import qualified Text.Parsec.IndentParsec.Prim as IP + + +-- LanguageDef things shamelessly stolen from Text.Parsec.Language. +-- Reason for stealing is that these have more generic types. +haskellStyle = T.LanguageDef + { T.commentStart = "{-" + , T.commentEnd = "-}" + , T.commentLine = "--" + , T.nestedComments = True + , T.identStart = letter + , T.identLetter = alphaNum <|> oneOf "_'" + , T.opStart = T.opLetter haskellStyle + , T.opLetter = oneOf ":!#$%&*+./<=>?@\\^|-~" + , T.reservedOpNames= [] + , T.reservedNames = [] + , T.caseSensitive = True + } + +haskell :: T.GenTokenParser String () (IP.IndentT IP.HaskellLike Identity) +haskell = T.makeTokenParser haskellDef + +haskellDef = haskell98Def + { T.identLetter = T.identLetter haskell98Def <|> char '#' + , T.reservedNames = T.reservedNames haskell98Def ++ + ["foreign","import","export","primitive" + ,"_ccall_","_casm_" + ,"forall" + ] + } + +haskell98Def = haskellStyle + { T.reservedOpNames= ["::","..","=","\\","|","<-","->","@","~","=>"] + , T.reservedNames = ["let","in","case","of","if","then","else", + "data","type", + "class","default","deriving","do","import", + "infix","infixl","infixr","instance","module", + "newtype","where", + "primitive" + -- "as","qualified","hiding" + ] + } + +-- Bring the right combinators in scope. +mySemiSep = IT.semiSepOrFoldedLines haskell +myBraces = IT.bracesBlock haskell +identifier = IT.identifier haskell +operator = IT.operator haskell +reserved = IT.reserved haskell +reservedOp = IT.reservedOp haskell +charLiteral = IT.charLiteral haskell +stringLiteral = IT.stringLiteral haskell +natural = IT.natural haskell +integer = IT.integer haskell +float = IT.float haskell +naturalOrFloat = IT.naturalOrFloat haskell +decimal = IT.decimal haskell +hexadecimal = IT.hexadecimal haskell +octal = IT.octal haskell +symbol = IT.symbol haskell +lexeme = IT.lexeme haskell +whiteSpace = IT.whiteSpace haskell +semi = IT.semi haskell +comma = IT.comma haskell +colon = IT.colon haskell +dot = IT.dot haskell +parens = IT.parens haskell +parensBlock = IT.parensBlock haskell +braces = IT.braces haskell +bracesBlock = IT.bracesBlock haskell +angles = IT.angles haskell +anglesBlock = IT.anglesBlock haskell +brackets = IT.brackets haskell +bracketsBlock = IT.bracketsBlock haskell +semiSep = IT.semiSep haskell +semiSepOrFoldedLines = IT.semiSepOrFoldedLines haskell +semiSep1 = IT.semiSep1 haskell +semiSepOrFoldedLines1 = IT.semiSepOrFoldedLines1 haskell +commaSep = IT.commaSep haskell +commaSepOrFoldedLines = IT.commaSepOrFoldedLines haskell +commaSep1 = IT.commaSep1 haskell +commaSepOrFoldedLines1 = IT.commaSepOrFoldedLines1 haskell + +-- Some more specific combinators. +identifierGuard pr = try $ do + s <- identifier + guard (not (null s) && pr s) + return s + +typeident = identifierGuard (isUpper . head) +varident = identifierGuard (isLower . head) diff --git a/src/Haskell/SimpleParser.hs b/src/Haskell/SimpleParser.hs new file mode 100644 index 0000000..26308de --- /dev/null +++ b/src/Haskell/SimpleParser.hs @@ -0,0 +1,124 @@ +module Haskell.SimpleParser where + +import Control.Monad +import Data.Char +import Haskell.AST +import Text.Parsec +import Text.Parsec.String + + +parseAST :: String -> String -> Either ParseError AST +parseAST fname source = parse pAST fname source + +pAST :: Parser AST +pAST = do + whitespace + tops <- many pToplevel + eof + return $ AST tops + +pToplevel :: Parser Toplevel +pToplevel = TopDef <$> pDef + +pDef :: Parser Def +pDef = do + n <- pNameV + args <- many pNameV + symbolO "=" + ex <- pExpr + symbolO ";" + case args of + [] -> return $ Def n ex + _ -> return $ Def n (Lam args ex) + +pExpr :: Parser Expr +pExpr = pLam <|> pCase <|> pApp + where + pSimpleExpr = choice [LitNum <$> pNum + ,Ref <$> (pName <|> try (parens pOperator)) + ,parens (pExpr `sepBy` symbolO ",") >>= \case + [ex] -> return ex + exs -> return $ Tup exs] + + pLam = do + symbolO "\\" + args <- many1 pNameV + body <- pExpr + return $ Lam args body + + pApp = many1 pSimpleExpr >>= \case + [] -> undefined + [e] -> return e + (e:es) -> return $ App e es + + pCase = do + symbolW "case" + n <- pNameV + symbolW "of" + arms <- braces (pCaseArm `sepBy` symbolO ";") + return $ Case n arms + + pCaseArm = do + pat <- pLargePat + symbolO "->" + ex <- pExpr + return (pat, ex) + +pSimplePat :: Parser Pat +pSimplePat = choice [symbolW "_" >> return PatAny + ,PatVar <$> pNameV + ,pNameT >>= \n -> return (PatCon n []) + ,parens (pLargePat `sepBy` symbolO ",") >>= \case + [pat] -> return pat + pats -> return $ PatTup pats] + +pLargePat :: Parser Pat +pLargePat = choice [PatCon <$> pNameT <*> many pSimplePat + ,pSimplePat] + +pNum :: Parser Integer +pNum = (char '-' >> (negate <$> pPositive)) <|> pPositive + where pPositive = read <$> many1 digit + +pName :: Parser Name +pName = liftM2 (:) (satisfy isAlpha) pNameRest + +pNameV :: Parser Name +pNameV = liftM2 (:) (satisfy isLower) pNameRest + +pNameT :: Parser Name +pNameT = liftM2 (:) (satisfy isUpper) pNameRest + +pNameRest :: Parser Name +pNameRest = many (satisfy $ \d -> isAlphaNum d || d == '_') <* aheadW + +pOperator :: Parser String +pOperator = many1 (oneOf ":!#$%&*+./<=>?@\\^|-~") <* aheadO + +parens :: Parser a -> Parser a +parens = between (symbolBare "(") (symbolBare ")") + +braces :: Parser a -> Parser a +braces = between (symbolBare "{") (symbolBare "}") + +symbolW :: String -> Parser () +symbolW s = string s >> aheadW + +symbolO :: String -> Parser () +symbolO s = string s >> aheadO + +symbolBare :: String -> Parser () +symbolBare s = string s >> whitespace + +aheadW :: Parser () +aheadW = do + void (lookAhead (space <|> satisfy (\d -> not (isAlphaNum d) && d /= '_'))) <|> eof + whitespace + +aheadO :: Parser () +aheadO = do + void (lookAhead (space <|> alphaNum <|> oneOf ")};")) <|> eof + whitespace + +whitespace :: Parser () +whitespace = void $ many space diff --git a/src/Main.hs b/src/Main.hs new file mode 100644 index 0000000..fa4416f --- /dev/null +++ b/src/Main.hs @@ -0,0 +1,58 @@ +module Main where + +import Control.Monad +import Haskell.Env +import Haskell.SimpleParser +import System.Environment +import System.Exit +import System.IO + + +tryEither :: Either String a -> IO a +tryEither (Left err) = die err +tryEither (Right x) = return x + +tryEither' :: Show e => Either e a -> IO a +tryEither' (Left err) = die (show err) +tryEither' (Right x) = return x + +while :: Monad m => a -> (a -> m (Maybe a)) -> m () +while val f = f val >>= \case + Nothing -> return () + Just val' -> while val' f + +whenM :: Monad m => m Bool -> m a -> m () +whenM b a = b >>= \b' -> if b' then void a else return () + +main :: IO () +main = do + fname <- getArgs >>= \case + [fname] -> return fname + _ -> die "Usage: verify-hs <file.hs>" + + source <- readFile fname + ast <- tryEither' (parseAST fname source) + print ast + env0 <- tryEither (envFromAST ast) + print env0 + + while env0 $ \env -> do + putStrLn "" + putStr "> " >> hFlush stdout + + eof <- isEOF + if eof + then return Nothing + else words <$> getLine >>= \case + [] -> return (Just env) + + ["forget", name] -> + case forget name env of + Left err -> putStrLn err >> return (Just env) + Right env' -> return (Just env') + + ["show"] -> print env >> return (Just env) + + cmd -> do + putStrLn $ "Unrecognised command: " ++ show cmd + return (Just env) diff --git a/test.txt b/test.txt new file mode 100644 index 0000000..88001e4 --- /dev/null +++ b/test.txt @@ -0,0 +1,10 @@ +fmap f p = Parser ((.) (fmapEither (fmap1st f)) (runParser p)); + +fmapEither f e = case e of { + Left x -> Left x; + Right x -> Right (f x) +}; + +fmap1st f p = case p of { + (l, r) -> (f l, r) +}; diff --git a/verify-hs.cabal b/verify-hs.cabal new file mode 100644 index 0000000..0a1aa2c --- /dev/null +++ b/verify-hs.cabal @@ -0,0 +1,31 @@ +name: verify-hs +version: 0.1.0.0 +synopsis: Interactive equational reasoning system for Haskell +license: MIT +license-file: LICENSE +author: Tom Smeding +maintainer: tom.smeding@gmail.com +copyright: (c) Tom Smeding, 2019 +build-type: Simple +cabal-version: >=1.10 + +executable verify-hs + main-is: Main.hs + other-modules: + Haskell.AST + Haskell.Env + Haskell.Parser + Haskell.Parser.Def + Haskell.SimpleParser + build-depends: + base >=4.12 && <4.13, + containers >=0.6.0.1 && <0.7, + indentparser >=0.1 && <0.2, + mtl >=2.2.2 && <2.3, + parsec >=3.1.13.0 && <3.2 + -- threepenny-gui >=0.8.3.0 && <0.9 + hs-source-dirs: src + ghc-options: -Wall -O2 + default-language: Haskell2010 + default-extensions: + LambdaCase |