Initial

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