From 48d6f83c36f55471ba66281e6d9b272fb4b336f2 Mon Sep 17 00:00:00 2001 From: tomsmeding Date: Sun, 10 Mar 2019 18:26:30 +0100 Subject: Enough to prove functoriality of Parser --- src/Haskell/AST.hs | 79 ++++++++++++++++++++++++++++------ src/Haskell/Env.hs | 31 +++++++++++--- src/Haskell/Parser.hs | 6 +-- src/Haskell/Rewrite.hs | 100 ++++++++++++++++++++++++++++++++++++++++++++ src/Haskell/SimpleParser.hs | 27 ++++++++---- 5 files changed, 215 insertions(+), 28 deletions(-) create mode 100644 src/Haskell/Rewrite.hs (limited to 'src/Haskell') 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"] -- cgit v1.2.3-54-g00ecf