diff options
| -rw-r--r-- | src/Haskell/AST.hs | 79 | ||||
| -rw-r--r-- | src/Haskell/Env.hs | 31 | ||||
| -rw-r--r-- | src/Haskell/Parser.hs | 6 | ||||
| -rw-r--r-- | src/Haskell/Rewrite.hs | 100 | ||||
| -rw-r--r-- | src/Haskell/SimpleParser.hs | 27 | ||||
| -rw-r--r-- | src/Main.hs | 196 | ||||
| -rw-r--r-- | test.txt | 11 | ||||
| -rw-r--r-- | verify-hs.cabal | 2 |
8 files changed, 404 insertions, 48 deletions
diff --git a/src/Haskell/AST.hs b/src/Haskell/AST.hs index 8326440..e1fd1e4 100644 --- a/src/Haskell/AST.hs +++ b/src/Haskell/AST.hs @@ -1,38 +1,40 @@ module Haskell.AST where +import Data.List + type Name = String type TyVar = String data AST = AST [Toplevel] - deriving (Show) + deriving (Show, Eq) data Toplevel = TopDef Def | TopDecl Decl | TopData Data | TopClass Class | TopInst Inst - deriving (Show) + deriving (Show, Eq) data Def = Def Name Expr - deriving (Show) + deriving (Show, Eq) data Expr = App Expr [Expr] | Ref Name - | LitNum Integer + | Num Integer | Tup [Expr] | Lam [Name] Expr - | Case Name [(Pat, Expr)] - deriving (Show) + | Case Expr [(Pat, Expr)] + deriving (Show, Eq) data Pat = PatAny | PatVar Name | PatCon Name [Pat] | PatTup [Pat] - deriving (Show) + deriving (Show, Eq) data Decl = Decl Name Type - deriving (Show) + deriving (Show, Eq) data Type = TyTup [Type] | TyInt @@ -40,13 +42,66 @@ data Type = TyTup [Type] | TyRef Name [Type] | TyVar Name | TyVoid - deriving (Show) + deriving (Show, Eq) data Data = Data Name [TyVar] [(Name, [Type])] - deriving (Show) + deriving (Show, Eq) data Class = Class Name [TyVar] [Decl] - deriving (Show) + deriving (Show, Eq) data Inst = Inst Name Type [Def] - deriving (Show) + deriving (Show, Eq) + + +class Pretty a where + pretty :: a -> String + +instance Pretty AST where + pretty (AST tops) = intercalate "\n" (map pretty tops) + +instance Pretty Toplevel where + pretty (TopDef x) = pretty x + pretty (TopDecl x) = pretty x + pretty (TopData x) = pretty x + pretty (TopClass x) = pretty x + pretty (TopInst x) = pretty x + +instance Pretty Def where + pretty (Def n e) = n ++ " = " ++ pretty e + +instance Pretty Expr where + pretty (App e as) = "(" ++ intercalate " " (map pretty (e:as)) ++ ")" + pretty (Ref n) = n + pretty (Num n) = show n + pretty (Tup es) = "(" ++ intercalate ", " (map pretty es) ++ ")" + pretty (Lam as e) = "(\\" ++ intercalate " " as ++ " -> " ++ pretty e ++ ")" + pretty (Case e arms) = "(case " ++ pretty e ++ " of { " ++ intercalate ";" (map go arms) ++ " })" + where go (p, e') = pretty p ++ " -> " ++ pretty e' + +instance Pretty Pat where + pretty PatAny = "_" + pretty (PatVar n) = n + pretty (PatCon n ps) = "(" ++ n ++ " " ++ intercalate " " (map pretty ps) ++ ")" + pretty (PatTup ps) = "(" ++ intercalate ", " (map pretty ps) ++ ")" + +instance Pretty Decl where + pretty (Decl n t) = n ++ " :: " ++ pretty t + +instance Pretty Type where + pretty (TyTup ts) = "(" ++ intercalate ", " (map pretty ts) ++ ")" + pretty TyInt = "Int" + pretty (TyFun t u) = "(" ++ pretty t ++ " -> " ++ pretty u ++ ")" + pretty (TyRef n as) = "(" ++ n ++ " " ++ intercalate " " (map pretty as) ++ ")" + pretty (TyVar n) = n + pretty TyVoid = "#Void" + +instance Pretty Data where + pretty (Data n as cs) = "data " ++ n ++ " " ++ intercalate " " as ++ " = " ++ intercalate " | " (map go cs) + where go (m, ts) = m ++ " " ++ intercalate " " (map pretty ts) + +instance Pretty Class where + pretty (Class n as ds) = "class " ++ n ++ " " ++ intercalate " " as ++ " where { " ++ intercalate " ; " (map pretty ds) ++ "}" + +instance Pretty Inst where + pretty (Inst n t ds) = "instance " ++ n ++ " " ++ pretty t ++ " where { " ++ intercalate " ; " (map pretty ds) ++ " }" diff --git a/src/Haskell/Env.hs b/src/Haskell/Env.hs index 21b2d4b..6b74221 100644 --- a/src/Haskell/Env.hs +++ b/src/Haskell/Env.hs @@ -1,6 +1,7 @@ module Haskell.Env where import Control.Monad +import Data.List import qualified Data.Map.Strict as Map import Haskell.AST @@ -8,6 +9,10 @@ import Haskell.AST data Env = Env { eDefs :: Map.Map Name Expr } deriving (Show) +instance Pretty Env where + pretty (Env defs) = + intercalate "\n" [n ++ " = " ++ pretty e | (n, e) <- Map.assocs defs] + emptyEnv :: Env emptyEnv = Env Map.empty @@ -18,12 +23,28 @@ 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 env (TopDef def) = addDef env def 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) +addDef :: Env -> Def -> Either String Env +addDef env (Def n ex) = + if envContains env n + then Left $ "Name '" ++ n ++ "' already present in environment" + else Right $ env { eDefs = Map.insert n ex (eDefs env) } + +envContains :: Env -> Name -> Bool +envContains env name = Map.member name (eDefs env) + +forget :: Env -> Name -> Either String Env +forget env name = + if envContains env name then Right $ env { eDefs = Map.delete name (eDefs env) } else Left $ "Name '" ++ name ++ "' not found in environment" + +reAdd :: Env -> Def -> Either String Env +reAdd env def@(Def name _) = forget env name >>= flip addDef def + +get :: Env -> Name -> Either String Expr +get env name = case Map.lookup name (eDefs env) of + Nothing -> Left "Name doesn't exist" + Just ex -> Right ex diff --git a/src/Haskell/Parser.hs b/src/Haskell/Parser.hs index 0f55a63..e7b9535 100644 --- a/src/Haskell/Parser.hs +++ b/src/Haskell/Parser.hs @@ -94,7 +94,7 @@ pType = foldr1 TyFun <$> pSimpleType `sepBy` reservedOp "->" pExpr :: Parser Expr pExpr = pLam <|> pCase <|> pApp where - pSimpleExpr = choice [LitNum <$> integer + pSimpleExpr = choice [Num <$> integer ,Ref <$> (identifier <|> try (parens operator)) ,parens pExpr] @@ -108,10 +108,10 @@ pExpr = pLam <|> pCase <|> pApp pCase = do reserved "case" - n <- varident + e <- pExpr reserved "of" arms <- bracesBlock (semiSepOrFoldedLines pCaseArm) - return $ Case n arms + return $ Case e arms pCaseArm = do pat <- pLargePat diff --git a/src/Haskell/Rewrite.hs b/src/Haskell/Rewrite.hs new file mode 100644 index 0000000..d53eb6f --- /dev/null +++ b/src/Haskell/Rewrite.hs @@ -0,0 +1,100 @@ +module Haskell.Rewrite + (rewrite + ,betared, etared, casered + ,etacase, casecase + ,normalise) where + +import Control.Monad +import Data.List +import Data.Maybe +import qualified Data.Map.Strict as Map +import Haskell.AST + + +rewrite :: Name -> Expr -> Expr -> Expr +rewrite name repl = \case + App e as -> App (rewrite name repl e) (map (rewrite name repl) as) + Ref n -> if n == name then repl else Ref n + Num k -> Num k + Tup es -> Tup (map (rewrite name repl) es) + Lam ns e -> if name `elem` ns then Lam ns e else Lam ns (rewrite name repl e) + Case e as -> Case (rewrite name repl e) (map caseArm as) + where + caseArm (p, e') = + if name `elem` boundVars p then (p, e') else (p, rewrite name repl e') + +boundVars :: Pat -> [Name] +boundVars PatAny = [] +boundVars (PatVar n) = [n] +boundVars (PatCon n ps) = nub $ [n] ++ concatMap boundVars ps +boundVars (PatTup ps) = nub $ concatMap boundVars ps + +betared :: Expr -> Expr +betared (App (Lam (n:as) bd) (arg:args)) = + App (Lam as (rewrite n arg bd)) args +betared e = recurse id betared e + +etared :: Expr -> Expr +etared (Lam (n:as) (App e es@(_:_))) + | last es == Ref n = + Lam as (App e (init es)) +etared e = recurse id etared e + +casered :: Bool -> Expr -> Expr +casered ambig orig@(Case subj arms) = + case catMaybes [(,rhs) <$> unify p subj | (p, rhs) <- arms] of + [] -> recurse id (casered ambig) orig + ((mp, rhs):rest) -> + let res = foldl' (\e' (n, rhs') -> rewrite n rhs' e') rhs (Map.assocs mp) + in case (ambig, rest) of + (True, _) -> res + (False, []) -> res + (False, _) -> recurse id (casered ambig) orig +casered ambig e = recurse id (casered ambig) e + +etacase :: Expr -> Expr +etacase (Case subj arms) | all (uncurry eqPE) arms = subj +etacase e = recurse id etacase e + +casecase :: Expr -> Expr +casecase (Case (Case subj arms1) arms2) = + Case subj [(p, Case e arms2) | (p, e) <- arms1] +casecase e = recurse id casecase e + +eqPE :: Pat -> Expr -> Bool +eqPE pat expr = case unify pat expr of + Nothing -> False + Just mp -> all (uncurry isIdmap) (Map.assocs mp) + where + isIdmap n = (== Ref n) + +unify :: Pat -> Expr -> Maybe (Map.Map Name Expr) +unify PatAny _ = Just Map.empty +unify (PatVar n) e = Just (Map.singleton n e) +unify (PatCon n ps) (App n' es) + | n' == Ref n, length ps == length es = + foldM (\m (p, e) -> unify p e >>= reconcile m) Map.empty (zip ps es) +unify (PatTup ps) (Tup es) + | length ps == length es = + foldM (\m (p, e) -> unify p e >>= reconcile m) Map.empty (zip ps es) +unify _ _ = Nothing + +reconcile :: Map.Map Name Expr -> Map.Map Name Expr -> Maybe (Map.Map Name Expr) +reconcile m1 m2 = foldM func m1 (Map.assocs m2) + where func m (k, v) = case Map.lookup k m of + Nothing -> Just (Map.insert k v m) + Just v' | v == v' -> Just m + | otherwise -> Nothing + +normalise :: Expr -> Expr +normalise (App e []) = normalise e +normalise (Lam [] e) = normalise e +normalise e = recurse id normalise e + +recurse :: (Pat -> Pat) -> (Expr -> Expr) -> Expr -> Expr +recurse _ f (App e as) = App (f e) (map f as) +recurse _ _ (Ref n) = Ref n +recurse _ _ (Num k) = Num k +recurse _ f (Tup es) = Tup (map f es) +recurse _ f (Lam ns e) = Lam ns (f e) +recurse fp f (Case e as) = Case (f e) (map (\(p, e') -> (fp p, f e')) as) diff --git a/src/Haskell/SimpleParser.hs b/src/Haskell/SimpleParser.hs index 26308de..841e41c 100644 --- a/src/Haskell/SimpleParser.hs +++ b/src/Haskell/SimpleParser.hs @@ -22,7 +22,7 @@ pToplevel = TopDef <$> pDef pDef :: Parser Def pDef = do - n <- pNameV + n <- pVariable args <- many pNameV symbolO "=" ex <- pExpr @@ -34,8 +34,8 @@ pDef = do pExpr :: Parser Expr pExpr = pLam <|> pCase <|> pApp where - pSimpleExpr = choice [LitNum <$> pNum - ,Ref <$> (pName <|> try (parens pOperator)) + pSimpleExpr = choice [Num <$> pNum + ,Ref <$> pVariable ,parens (pExpr `sepBy` symbolO ",") >>= \case [ex] -> return ex exs -> return $ Tup exs] @@ -53,10 +53,10 @@ pExpr = pLam <|> pCase <|> pApp pCase = do symbolW "case" - n <- pNameV + e <- pExpr symbolW "of" arms <- braces (pCaseArm `sepBy` symbolO ";") - return $ Case n arms + return $ Case e arms pCaseArm = do pat <- pLargePat @@ -80,18 +80,26 @@ pNum :: Parser Integer pNum = (char '-' >> (negate <$> pPositive)) <|> pPositive where pPositive = read <$> many1 digit +pVariable :: Parser Name +pVariable = pName <|> try (parens pOperator) + pName :: Parser Name -pName = liftM2 (:) (satisfy isAlpha) pNameRest +pName = notReserved $ liftM2 (:) (satisfy isAlpha) pNameRest pNameV :: Parser Name -pNameV = liftM2 (:) (satisfy isLower) pNameRest +pNameV = notReserved $ liftM2 (:) (satisfy isLower) pNameRest pNameT :: Parser Name -pNameT = liftM2 (:) (satisfy isUpper) pNameRest +pNameT = notReserved $ liftM2 (:) (satisfy isUpper) pNameRest pNameRest :: Parser Name pNameRest = many (satisfy $ \d -> isAlphaNum d || d == '_') <* aheadW +notReserved :: Parser Name -> Parser Name +notReserved p = + try $ p >>= \n -> + if n `elem` reservedWords then unexpected "reserved word" else return n + pOperator :: Parser String pOperator = many1 (oneOf ":!#$%&*+./<=>?@\\^|-~") <* aheadO @@ -122,3 +130,6 @@ aheadO = do whitespace :: Parser () whitespace = void $ many space + +reservedWords :: [String] +reservedWords = ["case", "of", "class", "instance", "where", "let", "in"] diff --git a/src/Main.hs b/src/Main.hs index fa4416f..3ed39f9 100644 --- a/src/Main.hs +++ b/src/Main.hs @@ -1,7 +1,9 @@ module Main where import Control.Monad +import Haskell.AST import Haskell.Env +import Haskell.Rewrite import Haskell.SimpleParser import System.Environment import System.Exit @@ -24,6 +26,179 @@ while val f = f val >>= \case whenM :: Monad m => m Bool -> m a -> m () whenM b a = b >>= \b' -> if b' then void a else return () +ifM :: Monad m => m Bool -> m a -> m a -> m a +ifM b t e = b >>= \b' -> if b' then t else e + +splitOn :: Eq a => a -> [a] -> [[a]] +splitOn _ [] = [[]] +splitOn spl (x:xs) + | x == spl = [] : splitOn spl xs + | otherwise = let (r : rs) = splitOn spl xs in (x:r) : rs + + +data AppState = AppState { asCtx :: Context, asFocus :: Maybe Name } + deriving (Show) + +data Context = Context { cStack :: [(Action, Env)], cBaseEnv :: Env } + deriving (Show) + +data Action = Action Cmd Name + deriving (Show) + +data Cmd = CForget + | CRewrite Name + | CBeta + | CEta + | CCase + | CCaseForce + | CEtaCase + | CCaseCase + deriving (Show) + +data UserCmd = UCCmd Cmd + | CAction Action + | CExit + | CUndo + | CShowEnv + | CUnFocus + | CFocus Name + | CLog + deriving (Show) + +instance Pretty Action where + pretty (Action cmd target) = "action " ++ target ++ " " ++ pretty cmd + +instance Pretty Cmd where + pretty CForget = "forget" + pretty (CRewrite name) = "rew " ++ name + pretty CBeta = "beta" + pretty CEta = "eta" + pretty CCase = "case" + pretty CCaseForce = "case!" + pretty CEtaCase = "etacase" + pretty CCaseCase = "casecase" + +topEnv :: Context -> Env +topEnv (Context [] env) = env +topEnv (Context ((_, env):_) _) = env + +pushCtx :: (Action, Env) -> Context -> Context +pushCtx pair ctx = ctx { cStack = pair : cStack ctx } + +apply :: Context -> Action -> Either String Context +apply ctx act@(Action cmd target) = case cmd of + CForget -> do + env' <- forget (topEnv ctx) target + return $ pushCtx (act, env') ctx + CRewrite name -> genTransform (\env -> liftM2 (,) (get env name) (get env target)) + (\(repl, expr) -> rewrite name repl expr) + CBeta -> transform betared + CEta -> transform etared + CCase -> transform (casered False) + CCaseForce -> transform (casered True) + CEtaCase -> transform etacase + CCaseCase -> transform casecase + where + transform :: (Expr -> Expr) -> Either String Context + transform = genTransform (\env -> get env target) + + genTransform :: (Env -> Either String a) -> (a -> Expr) -> Either String Context + genTransform getter f = do + expr <- normalise . f <$> getter (topEnv ctx) + env' <- reAdd (topEnv ctx) (Def target expr) + return $ pushCtx (act, env') ctx + +applyUserCmd :: AppState -> UserCmd -> IO (Either String (Maybe AppState)) +applyUserCmd appstate = \case + UCCmd cmd -> + case asFocus appstate of + Nothing -> return (Left "No focus set") + Just focus -> + case apply (asCtx appstate) (Action cmd focus) of + Left err -> return (Left err) + Right ctx -> return (Right (Just appstate { asCtx = ctx })) + CAction act -> case apply (asCtx appstate) act of + Left err -> return (Left err) + Right ctx -> return (Right (Just appstate { asCtx = ctx })) + CExit -> return (Right Nothing) + CUndo -> + let ctx = asCtx appstate + in case cStack ctx of + [] -> return (Left "Empty environment stack") + (_:stk) -> return (Right (Just appstate { asCtx = ctx { cStack = stk } })) + CShowEnv -> putStrLn (pretty (topEnv (asCtx appstate))) >> return (Right (Just appstate)) + CUnFocus -> return (Right (Just appstate { asFocus = Nothing })) + CFocus name -> if envContains (topEnv (asCtx appstate)) name + then return (Right (Just appstate { asFocus = Just name })) + else return (Left "Name doesn't exist") + CLog -> do + mapM_ (putStrLn . pretty) $ map fst (reverse $ cStack (asCtx appstate)) + return (Right (Just appstate)) + +applyUserCmds :: AppState -> [UserCmd] -> IO (Either String (Maybe AppState)) +applyUserCmds appstate [] = return (Right (Just appstate)) +applyUserCmds appstate (ucmd : ucmds) = + applyUserCmd appstate ucmd >>= \case + Left err -> return (Left err) + Right Nothing -> return (Right Nothing) + Right (Just as) -> applyUserCmds as ucmds + +interface :: AppState -> IO (Maybe AppState) +interface appstate = do + putStrLn "" + + let appstate' = case asFocus appstate of + Nothing -> appstate + Just focus -> + if envContains (topEnv (asCtx appstate)) focus + then appstate + else appstate { asFocus = Nothing } + + case asFocus appstate' of + Nothing -> return () + Just n -> + case get (topEnv (asCtx appstate')) n of + Left _ -> return () + Right expr -> putStrLn $ pretty (Def n expr) + + putStr "> " >> hFlush stdout + + ifM isEOF (return Nothing) + (getLine >>= handleInputLine appstate') + +handleInputLine :: AppState -> String -> IO (Maybe AppState) +handleInputLine appstate line = do + let phrases = map words $ splitOn ';' line + + ucmds <- case mapM parseCmd $ filter (not . null) phrases of + Left err -> putStrLn err >> return [] + Right ucmds -> return ucmds + + applyUserCmds appstate ucmds >>= \case + Left err -> putStrLn err >> return (Just appstate) + Right Nothing -> return Nothing + Right (Just as) -> return (Just as) + +parseCmd :: [String] -> Either String UserCmd +parseCmd ("action" : target : rest) = parseCmd rest >>= \case + UCCmd cmd -> Right (CAction (Action cmd target)) + _ -> Left "Invalid command within 'action'" +parseCmd ["exit"] = Right CExit +parseCmd ["undo"] = Right CUndo +parseCmd ["env"] = Right CShowEnv +parseCmd ["focus"] = Right CUnFocus +parseCmd ["focus", name] = Right (CFocus name) +parseCmd ["log"] = Right CLog +parseCmd ["forget"] = Right (UCCmd CForget) +parseCmd ["rew", func] = Right (UCCmd (CRewrite func)) +parseCmd ["beta"] = Right (UCCmd CBeta) +parseCmd ["eta"] = Right (UCCmd CEta) +parseCmd ["case"] = Right (UCCmd CCase) +parseCmd ["case!"] = Right (UCCmd CCaseForce) +parseCmd ["etacase"] = Right (UCCmd CEtaCase) +parseCmd ["casecase"] = Right (UCCmd CCaseCase) +parseCmd cmd = Left $ "Unrecognised command: " ++ show cmd + main :: IO () main = do fname <- getArgs >>= \case @@ -36,23 +211,4 @@ main = do 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) + while (AppState (Context [] env0) Nothing) interface @@ -8,3 +8,14 @@ fmapEither f e = case e of { fmap1st f p = case p of { (l, r) -> (f l, r) }; + +runParser p = case p of { + Parser g -> g +}; + +(.) f g x = f (g x); +id x = x; + +v = fmap id (Parser g); +x = fmap ((.) f g) (Parser g); +y = ((.) (fmap f) (fmap g)) (Parser g); diff --git a/verify-hs.cabal b/verify-hs.cabal index 0a1aa2c..ec92482 100644 --- a/verify-hs.cabal +++ b/verify-hs.cabal @@ -16,6 +16,7 @@ executable verify-hs Haskell.Env Haskell.Parser Haskell.Parser.Def + Haskell.Rewrite Haskell.SimpleParser build-depends: base >=4.12 && <4.13, @@ -29,3 +30,4 @@ executable verify-hs default-language: Haskell2010 default-extensions: LambdaCase + TupleSections |