Enough to prove functoriality of Parser

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