aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rw-r--r--.gitignore2
-rw-r--r--LICENSE20
-rw-r--r--src/Haskell/AST.hs52
-rw-r--r--src/Haskell/Env.hs29
-rw-r--r--src/Haskell/Parser.hs133
-rw-r--r--src/Haskell/Parser/Def.hs100
-rw-r--r--src/Haskell/SimpleParser.hs124
-rw-r--r--src/Main.hs58
-rw-r--r--test.txt10
-rw-r--r--verify-hs.cabal31
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/
diff --git a/LICENSE b/LICENSE
new file mode 100644
index 0000000..9afdd75
--- /dev/null
+++ b/LICENSE
@@ -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