aboutsummaryrefslogtreecommitdiff
path: root/src
diff options
context:
space:
mode:
authortomsmeding <tom.smeding@gmail.com>2019-03-10 18:26:30 +0100
committertomsmeding <tom.smeding@gmail.com>2019-03-10 18:26:30 +0100
commit48d6f83c36f55471ba66281e6d9b272fb4b336f2 (patch)
tree0d605ad7140861e30af21c7489d5ea4957ef1c50 /src
parent34d9f21c6ab529e415f38a5a886b1b612bcbd3bc (diff)
Enough to prove functoriality of Parser
Diffstat (limited to 'src')
-rw-r--r--src/Haskell/AST.hs79
-rw-r--r--src/Haskell/Env.hs31
-rw-r--r--src/Haskell/Parser.hs6
-rw-r--r--src/Haskell/Rewrite.hs100
-rw-r--r--src/Haskell/SimpleParser.hs27
-rw-r--r--src/Main.hs196
6 files changed, 391 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