diff --git a/LICENSE b/LICENSE new file mode 100644 --- /dev/null +++ b/LICENSE @@ -0,0 +1,20 @@ +Copyright (c) 2016 Ranjit Jhala + +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/README.md b/README.md new file mode 100644 --- /dev/null +++ b/README.md @@ -0,0 +1,180 @@ +# ELSA + +`elsa` is a tiny language designed to build +intuition about how the Lambda Calculus, or +more generally, _computation-by-substitution_ works. +Rather than the usual interpreter that grinds +lambda terms down to values, `elsa` aims to be +a light-weight _proof checker_ that determines +whether, under a given sequence of definitions, +a particular term _reduces to_ to another. + +## Online Demo + +You can try `elsa` online at [this link](http://goto.ucsd.edu:8095/index.html) + +## Install + +You can locally build and run `elsa` by + +1. Installing [stack](https://www.haskellstack.org) +2. Cloning this repo +3. Building `elsa` with `stack`. + +That is, to say + +```bash +$ curl -sSL https://get.haskellstack.org/ | sh +$ git clone https://github.com/ucsd-progsys/elsa.git +$ cd elsa +$ stack install +``` + +## Overview + +`elsa` programs look like: + +```haskell +-- id_0.lc +let id = \x -> x +let zero = \f x -> x + +eval id_zero : + id zero + =d> (\x -> x) (\f x -> x) + =b> (\f x -> x) + =d> zero +``` + +When you run `elsa` on the above, you should get the following output: + +```bash +$ elsa ex1.lc + +OK id_zero. +``` + +## Partial Evaluation + +If instead you write a partial sequence of +reductions, i.e. where the _last_ term can +still be further reduced: + +```haskell +-- succ_1_bad.lc +let one = \f x -> f x +let two = \f x -> f (f x) +let incr = \n f x -> f (n f x) + +eval succ_one : + incr one + =d> (\n f x -> f (n f x)) (\f x -> f x) + =b> \f x -> f ((\f x -> f x) f x) + =b> \f x -> f ((\x -> f x) x) +``` + +Then `elsa` will complain that + +```bash +$ elsa ex2.lc + +ex2.lc:11:7-30: succ_one can be further reduced + + 11 | =b> \f x -> f ((\x -> f x) x) + ^^^^^^^^^^^^^^^^^^^^^^^^^ +``` + +You can _fix_ the error by completing the reduction + +```haskell +-- succ_1.lc +let one = \f x -> f x +let two = \f x -> f (f x) +let incr = \n f x -> f (n f x) + +eval succ_one : + incr one + =d> (\n f x -> f (n f x)) (\f x -> f x) + =b> \f x -> f ((\f x -> f x) f x) + =b> \f x -> f ((\x -> f x) x) + =b> \f x -> f (f x) -- beta-reduce the above + =d> two -- optional +``` + +Similarly, `elsa` rejects the following program, + +```haskell +-- id_0_bad.lc +let id = \x -> x +let zero = \f x -> x + +eval id_zero : + id zero + =b> (\f x -> x) + =d> zero +``` + +with the error + +```bash +$ elsa ex4.lc + +ex4.lc:7:5-20: id_zero has an invalid beta-reduction + + 7 | =b> (\f x -> x) + ^^^^^^^^^^^^^^^ +``` + +You can fix the error by inserting the appropriate +intermediate term as shown in `id_0.lc` above. + +## Syntax of `elsa` Programs + +An `elsa` program has the form + +```haskell +-- definitions +[let = ]+ + +-- reductions +[]* +``` + +where the basic elements are lambda-calulus `term`s + +```haskell + ::= + \ + -> + ( ) +``` + +and `id` are lower-case identifiers + +``` + ::= x, y, z, ... +``` + +A `` is a sequence of `term`s chained together +with a `` + +```haskell + ::= eval : ( )* + + ::= =a> -- alpha equivalence + =b> -- beta equivalence + =d> -- def equivalence +``` + + +## Semantics of `elsa` programs + +A `reduction` of the form `t_1 s_1 t_2 s_2 ... t_n` is **valid** if + +* Each `t_i s_i t_i+1` is **valid**, and +* `t_n` is in normal form (i.e. cannot be further beta-reduced.) + +Furthermore, a `step` of the form + +* `t =a> t'` is valid if `t` and `t'` are equivalent up to **alpha-renaming**, +* `t =b> t'` is valid if `t` **beta-reduces** to `t'` in a single step, +* `t =d> t'` is valid if `t` and `t'` are identical after **let-expansion**. diff --git a/Setup.hs b/Setup.hs new file mode 100644 --- /dev/null +++ b/Setup.hs @@ -0,0 +1,2 @@ +import Distribution.Simple +main = defaultMain diff --git a/elsa.cabal b/elsa.cabal new file mode 100644 --- /dev/null +++ b/elsa.cabal @@ -0,0 +1,68 @@ +name: elsa +version: 0.1.0.0 +synopsis: A tiny language for understanding the lambda-calculus +description: elsa is a small proof checker for verifying sequences of + reductions of lambda-calculus terms. The goal is to help + students build up intuition about lambda-terms, alpha-equivalence, + beta-reduction, and in general, the notion of computation + by substitution. +license: MIT +license-file: LICENSE +author: Ranjit Jhala +maintainer: jhala@cs.ucsd.edu +category: Language +Homepage: http://github.com/ucsd-progsys/elsa +build-type: Simple +extra-source-files: README.md +cabal-version: >=1.10 + +Source-Repository head + Type: git + Location: https://github.com/ucsd-progsys/elsa/ + +Library + ghc-options: -W + exposed-modules: Language.Elsa.Types, + Language.Elsa.Eval, + Language.Elsa.Parser, + Language.Elsa.Runner + + Default-Extensions: OverloadedStrings + + -- other-extensions: + build-depends: base >= 4 && < 5, + array, + mtl, + megaparsec, + containers, + directory, + filepath, + json + + hs-source-dirs: src + default-language: Haskell2010 +-- build-tools: alex, happy + other-modules: Language.Elsa.UX, + Language.Elsa.Utils + +executable elsa + build-depends: base, + mtl, + elsa + default-language: Haskell2010 + main-is: src/Main.hs + Default-Extensions: OverloadedStrings + +test-suite test + default-language: Haskell98 + type: exitcode-stdio-1.0 + hs-source-dirs: tests + ghc-options: -threaded + Default-Extensions: OverloadedStrings + main-is: Test.hs + build-depends: base, + directory, + filepath, + tasty, + tasty-hunit, + elsa diff --git a/src/Language/Elsa/Eval.hs b/src/Language/Elsa/Eval.hs new file mode 100644 --- /dev/null +++ b/src/Language/Elsa/Eval.hs @@ -0,0 +1,164 @@ +{-# LANGUAGE OverloadedStrings #-} + +module Language.Elsa.Eval where + +import qualified Data.Map as M +import qualified Data.Set as S +import Control.Monad.State +import Data.Maybe (maybeToList) +import Language.Elsa.Types +import Language.Elsa.Utils (fromEither) + +-------------------------------------------------------------------------------- +elsa :: Elsa a -> [Result a] +-------------------------------------------------------------------------------- +elsa p = case mkEnv (defns p) of + Left err -> [err] + Right g -> [result g e | e <- evals p] + +result :: Env a -> Eval a -> Result a +result g e = fromEither (eval g e) + +mkEnv :: [Defn a] -> CheckM a (Env a) +mkEnv = foldM expand M.empty + +expand :: Env a -> Defn a -> CheckM a (Env a) +expand g (Defn b e) = case zs of + (x,l) : _ -> Left (Unbound b x l) + [] -> Right (M.insert (bindId b) e' g) + where + e' = subst e g + zs = M.toList (freeVars' e') + +-------------------------------------------------------------------------------- +type CheckM a b = Either (Result a) b +type Env a = M.Map Id (Expr a) +-------------------------------------------------------------------------------- + +-------------------------------------------------------------------------------- +eval :: Env a -> Eval a -> CheckM a (Result a) +-------------------------------------------------------------------------------- +eval g (Eval n e steps) = go e steps + where + go e [] + | isNormal g e = return (OK n) + | otherwise = Left (errPartial n e) + go e (s:steps) = step g n e s >>= (`go` steps) + +step :: Env a -> Bind a -> Expr a -> Step a -> CheckM a (Expr a) +step g n e (Step k e') + | isEq k g e e' = return e' + | otherwise = Left (errInvalid n e k e') + +isEq :: Eqn a -> Env a -> Expr a -> Expr a -> Bool +isEq (AlphEq _) = isAlphEq +isEq (BetaEq _) = isBetaEq +isEq (DefnEq _) = isDefnEq + +-------------------------------------------------------------------------------- +-- | Definition Equivalence +-------------------------------------------------------------------------------- +isDefnEq :: Env a -> Expr a -> Expr a -> Bool +isDefnEq g e1 e2 = subst e1 g == subst e2 g + +-------------------------------------------------------------------------------- +-- | Alpha Equivalence +-------------------------------------------------------------------------------- +isAlphEq :: Env a -> Expr a -> Expr a -> Bool +isAlphEq _ e1 e2 = alphaNormal e1 == alphaNormal e2 + +alphaNormal :: Expr a -> Expr a +alphaNormal e = evalState (normalize M.empty e) 0 + +type AlphaM a = State Int a + +normalize :: M.Map Id Id -> Expr a -> AlphaM (Expr a) +normalize g (EVar x z) = + return (EVar (rename g x) z) + +normalize g (EApp e1 e2 z) = do + e1' <- normalize g e1 + e2' <- normalize g e2 + return (EApp e1' e2' z) + +normalize g (ELam (Bind x z1) e z2) = do + y <- fresh + let g' = M.insert x y g + e' <- normalize g' e + return (ELam (Bind y z1) e' z2) + +rename :: M.Map Id Id -> Id -> Id +rename g x = M.findWithDefault x x g + +fresh :: AlphaM Id +fresh = do + n <- get + put (n + 1) + return ("$x" ++ show n) + +-------------------------------------------------------------------------------- +-- | Beta Reduction +-------------------------------------------------------------------------------- +isBetaEq :: Env a -> Expr a -> Expr a -> Bool +isBetaEq _ e1 e2 = or [ e1' == e2 | e1' <- betas e1] + +isNormal :: Env a -> Expr a -> Bool +isNormal g = null . betas . (`subst` g) + +-- | `betas e` returns the list [e1,...en] of terms obtainable via a single-step +-- beta reduction from `e`. +betas :: Expr a -> [Expr a] +betas (EVar _ _) = [] +betas (ELam b e z) = [ ELam b e' z | e' <- betas e ] +betas (EApp e1 e2 z) = [ EApp e1' e2 z | e1' <- betas e1 ] + ++ [ EApp e1 e2' z | e2' <- betas e2 ] + ++ maybeToList (beta e1 e2) + +beta :: Expr a -> Expr a -> Maybe (Expr a) +beta (ELam (Bind x _) e _) e' = substCA e x e' +beta _ _ = Nothing + +substCA :: Expr a -> Id -> Expr a -> Maybe (Expr a) +substCA e x e' = go [] e + where + zs = freeVars e' + bnd bs zs = or [ b `isIn` zs | b <- bs ] + go bs e@(EVar y _) + | y /= x = Just e -- different var, no subst + | bnd bs zs = Nothing -- same var, but free-var-captured + | otherwise = Just e' -- same var, but no capture + go bs (EApp e1 e2 l) = do e1' <- go bs e1 + e2' <- go bs e2 + Just (EApp e1' e2' l) + go bs (ELam b e1 l) = do e1' <- go (b:bs) e1 + Just (ELam b e1' l) + +isIn :: Bind a -> S.Set Id -> Bool +isIn = S.member . bindId + +-------------------------------------------------------------------------------- +-- | Free Variables and Substitution +-------------------------------------------------------------------------------- +freeVars :: Expr a -> S.Set Id +freeVars = S.fromList . M.keys . freeVars' + +freeVars' :: Expr a -> M.Map Id a +freeVars' (EVar x l) = M.singleton x l +freeVars' (ELam b e _) = M.delete (bindId b) (freeVars' e) +freeVars' (EApp e e' _) = M.union (freeVars' e) (freeVars' e') + +subst :: Expr a -> Env a -> Expr a +subst e@(EVar v _) su = M.findWithDefault e v su +subst (EApp e1 e2 z) su = EApp (subst e1 su) (subst e2 su) z +subst (ELam b e z) su = ELam b (subst e su') z + where + su' = M.delete (bindId b) su + +-------------------------------------------------------------------------------- +-- | Error Cases +-------------------------------------------------------------------------------- +errInvalid :: Bind a -> Expr a -> Eqn a -> Expr a -> Result a +errInvalid b _ eqn _ = Invalid b (tag eqn) + +errPartial :: Bind a -> Expr a -> Result a +errPartial b e = Partial b (tag e) diff --git a/src/Language/Elsa/Parser.hs b/src/Language/Elsa/Parser.hs new file mode 100644 --- /dev/null +++ b/src/Language/Elsa/Parser.hs @@ -0,0 +1,170 @@ +module Language.Elsa.Parser ( parse, parseFile ) where + +import Control.Monad (void) +import Text.Megaparsec hiding (parse) +import Text.Megaparsec.String +import qualified Text.Megaparsec.Lexer as L +import qualified Data.List as L +import Language.Elsa.Types +import Language.Elsa.UX + +-------------------------------------------------------------------------------- +parse :: FilePath -> Text -> SElsa +-------------------------------------------------------------------------------- +parse = parseWith elsa + +parseWith :: Parser a -> FilePath -> Text -> a +parseWith p f s = case runParser (whole p) f s of + Left err -> panic (show err) (posSpan . errorPos $ err) + Right e -> e + +instance Located ParseError where + sourceSpan = posSpan . errorPos + +instance PPrint ParseError where + pprint = show + +-------------------------------------------------------------------------------- +parseFile :: FilePath -> IO SElsa +-------------------------------------------------------------------------------- +parseFile f = parse f <$> readFile f + +-- https://mrkkrp.github.io/megaparsec/tutorials/parsing-simple-imperative-language.html + +-- | Top-level parsers (should consume all input) +whole :: Parser a -> Parser a +whole p = sc *> p <* eof + +-- RJ: rename me "space consumer" +sc :: Parser () +sc = L.space (void spaceChar) lineCmnt blockCmnt + where + lineCmnt = L.skipLineComment "--" + blockCmnt = L.skipBlockComment "{-" "-}" + +-- | `symbol s` parses just the string s (and trailing whitespace) +symbol :: String -> Parser String +symbol = L.symbol sc + +arrow :: Parser String +arrow = symbol "->" + +colon :: Parser String +colon = symbol ":" + +equal :: Parser String +equal = symbol "=" + +lam :: Parser String +lam = symbol "\\" + + +-- | 'parens' parses something between parenthesis. +parens :: Parser a -> Parser a +parens = betweenS "(" ")" + +betweenS :: String -> String -> Parser a -> Parser a +betweenS l r = between (symbol l) (symbol r) + +-- | `lexeme p` consume whitespace after running p +lexeme :: Parser a -> Parser (a, SourceSpan) +lexeme p = L.lexeme sc (withSpan p) + +-- | `rWord` +rWord :: String -> Parser SourceSpan +rWord w = snd <$> (withSpan (string w) <* notFollowedBy alphaNumChar <* sc) + +-- | list of reserved words +keywords :: [Text] +keywords = [ "let" , "eval" ] + +-- | `identifier` parses identifiers: lower-case alphabets followed by alphas or digits +identifier :: Parser (String, SourceSpan) +identifier = lexeme (p >>= check) + where + p = (:) <$> letterChar <*> many identChar -- alphaNumChar + check x = if x `elem` keywords + then fail $ "keyword " ++ show x ++ " cannot be an identifier" + else return x + +identChar :: Parser Char +identChar = alphaNumChar + <|> oneOf "_#'" + +-- | `binder` parses BareBind, used for let-binds and function parameters. +binder :: Parser SBind +binder = uncurry Bind <$> identifier + +withSpan' :: Parser (SourceSpan -> a) -> Parser a +withSpan' p = do + p1 <- getPosition + f <- p + p2 <- getPosition + return (f (SS p1 p2)) + +withSpan :: Parser a -> Parser (a, SourceSpan) +withSpan p = do + p1 <- getPosition + x <- p + p2 <- getPosition + return (x, SS p1 p2) + +-------------------------------------------------------------------------------- +-------------------------------------------------------------------------------- +-------------------------------------------------------------------------------- +elsa :: Parser SElsa +elsa = Elsa <$> many defn <*> many eval + +defn :: Parser SDefn +defn = do + rWord "let" + b <- binder <* equal + e <- expr + return (Defn b e) + +eval :: Parser SEval +eval = do + rWord "eval" + name <- binder + colon + root <- expr + steps <- many step + return $ Eval name root steps + +step :: Parser SStep +step = Step <$> eqn <*> expr + +eqn :: Parser SEqn +eqn = try (withSpan' (symbol "=a>" >> return AlphEq)) + <|> try (withSpan' (symbol "=b>" >> return BetaEq)) + <|> (withSpan' (symbol "=d>" >> return DefnEq)) + +-- expr :: Parser SExpr +-- expr = makeExprParser expr0 [] + +expr :: Parser SExpr +expr = try lamExpr + <|> try appExpr + <|> try idExpr + <|> parenExpr + +parenExpr :: Parser SExpr +parenExpr = parens expr + +idExpr :: Parser SExpr +idExpr = uncurry EVar <$> identifier + +appExpr :: Parser SExpr +appExpr = apps <$> funExpr <*> sepBy1 funExpr sc + where + apps = L.foldl' (\e1 e2 -> EApp e1 e2 (tag e1 `mappend` tag e2)) + +funExpr :: Parser SExpr +funExpr = try idExpr <|> parenExpr + +lamExpr :: Parser SExpr +lamExpr = do + lam + xs <- sepBy binder sc <* arrow + e <- expr + return (mkLam xs e) diff --git a/src/Language/Elsa/Runner.hs b/src/Language/Elsa/Runner.hs new file mode 100644 --- /dev/null +++ b/src/Language/Elsa/Runner.hs @@ -0,0 +1,62 @@ +{-# LANGUAGE ScopedTypeVariables #-} + +module Language.Elsa.Runner where + +import Data.List (intercalate) +import Data.Maybe (mapMaybe) +import Control.Monad (when) +import Control.Exception +import System.IO +import System.Exit +import System.Environment (getArgs) +import System.FilePath -- (takeDirectory, takeFileName) +import System.Directory -- (takeDirectory, takeFileName) +import Language.Elsa.Parser (parse) +import Language.Elsa.Types (successes, resultError) +import Language.Elsa.UX +import Language.Elsa.Eval (elsa) + + +topMain:: IO () +topMain = do + (m, f) <- getSrcFile + s <- readFile f + runElsa m f s `catch` exitErrors m f + +exitErrors :: Mode -> FilePath -> [UserError] -> IO () +exitErrors mode f es = esHandle mode (modeWriter mode f) resultExit es + +resultExit :: [UserError] -> IO a +resultExit [] = exitSuccess +resultExit _ = exitFailure + +esHandle :: Mode -> (Text -> IO ()) -> ([UserError] -> IO a) -> [UserError] -> IO a +esHandle mode writer exitF es = renderErrors mode es >>= writer >> exitF es + +modeWriter :: Mode -> FilePath -> Text -> IO () +modeWriter Cmdline _ s = hPutStrLn stderr s +modeWriter Json _ s = hPutStrLn stderr s +modeWriter Server f s = do createDirectoryIfMissing True jsonDir + writeFile jsonFile s + hPutStrLn stderr s + where + jsonDir = takeDirectory f ".elsa" + jsonFile = jsonDir addExtension (takeFileName f) ".json" + +runElsa :: Mode -> FilePath -> Text -> IO () +runElsa mode f s = do + let rs = elsa (parse f s) + let es = mapMaybe resultError rs + when (null es && mode == Cmdline) (putStrLn (okMessage rs)) + exitErrors mode f es + +okMessage rs = "OK " ++ intercalate ", " (successes rs) ++ "." + +getSrcFile :: IO (Mode, Text) +getSrcFile = do + args <- getArgs + case args of + ["--json" , f] -> return (Json, f) + ["--server", f] -> return (Server, f) + [f] -> return (Cmdline, f) + _ -> error "Please run with a single file as input" diff --git a/src/Language/Elsa/Types.hs b/src/Language/Elsa/Types.hs new file mode 100644 --- /dev/null +++ b/src/Language/Elsa/Types.hs @@ -0,0 +1,151 @@ +{-# LANGUAGE OverloadedStrings #-} +{-# LANGUAGE FlexibleInstances #-} + +module Language.Elsa.Types where + +import Text.Printf (printf) +import Data.Monoid +import Language.Elsa.UX +import Data.Maybe (mapMaybe) + +type Id = String + +type SElsa = Elsa SourceSpan +type SDefn = Defn SourceSpan +type SExpr = Expr SourceSpan +type SEval = Eval SourceSpan +type SStep = Step SourceSpan +type SBind = Bind SourceSpan +type SEqn = Eqn SourceSpan + + +-------------------------------------------------------------------------------- +-- | Result +-------------------------------------------------------------------------------- +data Result a + = OK (Bind a) + | Partial (Bind a) a + | Invalid (Bind a) a + | Unbound (Bind a) Id a + deriving (Eq, Show) + +failures :: [Result a] -> [Id] +failures = mapMaybe go + where + go (Partial b _) = Just (bindId b) + go (Invalid b _) = Just (bindId b) + go (Unbound b _ _) = Just (bindId b) + go _ = Nothing + +successes :: [Result a] -> [Id] +successes = mapMaybe go + where + go (OK b) = Just (bindId b) + go _ = Nothing + +resultError :: (Located a) => Result a -> Maybe UserError +resultError (Partial b l) = mkErr l (bindId b ++ " can be further reduced!") +resultError (Invalid b l) = mkErr l (bindId b ++ " has an invalid reduction!") +resultError (Unbound b x l) = mkErr l (bindId b ++ " has an unbound variable " ++ x ) +resultError _ = Nothing + +mkErr :: (Located a) => a -> Text -> Maybe UserError +mkErr l msg = Just (mkError msg (sourceSpan l)) + +-------------------------------------------------------------------------------- +-- | Programs +-------------------------------------------------------------------------------- + +data Elsa a = Elsa + { defns :: [Defn a] + , evals :: [Eval a] + } + deriving (Eq, Show) + +data Defn a + = Defn !(Bind a) !(Expr a) + deriving (Eq, Show) + +data Eval a = Eval + { evName :: !(Bind a) + , evRoot :: !(Expr a) + , evSteps :: [Step a] + } + deriving (Eq, Show) + +data Step a + = Step !(Eqn a) !(Expr a) + deriving (Eq, Show) + +data Eqn a + = AlphEq a + | BetaEq a + | DefnEq a + deriving (Eq, Show) + +data Bind a + = Bind Id a + deriving (Show) + +data Expr a + = EVar Id a + | ELam !(Bind a) !(Expr a) a + | EApp !(Expr a) !(Expr a) a + deriving (Show) + +instance Eq (Bind a) where + b1 == b2 = bindId b1 == bindId b2 + +instance Eq (Expr a) where + (EVar x _) == (EVar y _) = x == y + (ELam b1 e1 _) == (ELam b2 e2 _ ) = b1 == b2 && e1 == e2 + (EApp e1 e1' _) == (EApp e2 e2' _) = e1 == e2 && e1' == e2' + _ == _ = False + +------------------------------------------------------------------------------------- +-- | Pretty Printing +------------------------------------------------------------------------------------- +instance PPrint (Bind a) where + pprint (Bind x _) = x + +instance PPrint [Bind a] where + pprint = unwords . map pprint + +instance PPrint (Expr a) where + pprint (EVar x _) = x + pprint (EApp e1 e2 _) = printf "(%s %s)" (pprint e1) (pprint e2) + pprint e@(ELam {}) = printf "\\%s -> %s" (pprint xs) (pprint body) + where + (xs, body) = bkLam e + +bkLam :: Expr a -> ([Bind a], Expr a) +bkLam (ELam x e _) = (x:xs, body) + where + (xs, body) = bkLam e +bkLam e = ([], e) + +mkLam :: (Monoid a) => [Bind a] -> Expr a -> Expr a +mkLam [] e = e +mkLam (x:xs) e = ELam x (mkLam xs e) (tag x <> tag e) + +bindId :: Bind a -> Id +bindId (Bind x _) = x + +------------------------------------------------------------------------------------- +-- | Tag Extraction +------------------------------------------------------------------------------------- +class Tagged t where + tag :: t a -> a + +instance Tagged Eqn where + tag (AlphEq x) = x + tag (BetaEq x) = x + tag (DefnEq x) = x + +instance Tagged Bind where + tag (Bind _ x) = x + +instance Tagged Expr where + tag (EVar _ x) = x + tag (ELam _ _ x) = x + tag (EApp _ _ x) = x diff --git a/src/Language/Elsa/UX.hs b/src/Language/Elsa/UX.hs new file mode 100644 --- /dev/null +++ b/src/Language/Elsa/UX.hs @@ -0,0 +1,271 @@ +-- | This module contains the code for all the user (programmer) facing +-- aspects, i.e. error messages, source-positions, overall results. + +{-# LANGUAGE TypeSynonymInstances #-} +{-# LANGUAGE FlexibleInstances #-} + +module Language.Elsa.UX + ( + -- * Representation + SourceSpan (..) + , Located (..) + + -- * Usage Mode + , Mode (..) + + -- * Extraction from Source file + , readFileSpan + + -- * Constructing spans + , posSpan, junkSpan + + -- * Success and Failure + , UserError + , eMsg + , eSpan + -- , Result + + -- * Throwing & Handling Errors + , mkError + , abort + , panic + , renderErrors + + -- * Pretty Printing + , Text + , PPrint (..) + ) where + +import Control.Exception +import Data.Typeable +import Data.Monoid +import qualified Data.List as L +import Text.Printf (printf) +import Text.Megaparsec +import Text.Megaparsec.Pos +-- import Text.JSON.Pretty +import Text.JSON hiding (Error) +import Language.Elsa.Utils + +type Text = String + +class PPrint a where + pprint :: a -> Text + +-------------------------------------------------------------------------------- +-- | Accessing SourceSpan +-------------------------------------------------------------------------------- +class Located a where + sourceSpan :: a -> SourceSpan + +instance Located SourceSpan where + sourceSpan x = x + +-------------------------------------------------------------------------------- +-- | Source Span Representation +-------------------------------------------------------------------------------- +data SourceSpan = SS + { ssBegin :: !SourcePos + , ssEnd :: !SourcePos + } + deriving (Eq, Show) + +instance Monoid SourceSpan where + mempty = junkSpan + mappend = mappendSpan + +mappendSpan :: SourceSpan -> SourceSpan -> SourceSpan +mappendSpan s1 s2 + | s1 == junkSpan = s2 + | s2 == junkSpan = s1 + | otherwise = SS (ssBegin s1) (ssEnd s2) + +instance PPrint SourceSpan where + pprint = ppSourceSpan + +ppSourceSpan :: SourceSpan -> String +ppSourceSpan s + | l1 == l2 = printf "%s:%d:%d-%d" f l1 c1 c2 + | otherwise = printf "%s:(%d:%d)-(%d:%d)" f l1 c1 l2 c2 + where + (f, l1, c1, l2, c2) = spanInfo s + +spanInfo :: SourceSpan -> (FilePath, Int, Int, Int, Int) +spanInfo s = (f s, l1 s, c1 s, l2 s, c2 s) + where + f = spanFile + l1 = sourceLine . ssBegin + c1 = sourceColumn . ssBegin + l2 = sourceLine . ssEnd + c2 = sourceColumn . ssEnd + +-------------------------------------------------------------------------------- +-- | Source Span Extraction +-------------------------------------------------------------------------------- +readFileSpan :: SourceSpan -> IO String +-------------------------------------------------------------------------------- +readFileSpan sp = getSpan sp <$> readFile (spanFile sp) + + +spanFile :: SourceSpan -> FilePath +spanFile = sourceName . ssBegin + +getSpan :: SourceSpan -> String -> String +getSpan sp + | sameLine = getSpanSingle l1 c1 c2 + | sameLineEnd = getSpanSingleEnd l1 c1 + | otherwise = getSpanMulti l1 l2 + where + sameLine = l1 == l2 + sameLineEnd = l1 + 1 == l2 && c2 == 1 + (_, l1, c1, l2, c2) = spanInfo sp + + +getSpanSingleEnd :: Int -> Int -> String -> String +getSpanSingleEnd l c1 + = highlightEnd l c1 + . safeHead "" + . getRange l l + . lines + +getSpanSingle :: Int -> Int -> Int -> String -> String +getSpanSingle l c1 c2 + = highlight l c1 c2 + . safeHead "" + . getRange l l + . lines + +getSpanMulti :: Int -> Int -> String -> String +getSpanMulti l1 l2 + = highlights l1 + . getRange l1 l2 + . lines + +highlight :: Int -> Int -> Int -> String -> String +highlight l c1 c2 s = unlines + [ cursorLine l s + , replicate (12 + c1) ' ' <> replicate (c2 - c1) '^' + ] + +highlightEnd :: Int -> Int -> String -> String +highlightEnd l c1 s = highlight l c1 (1 + length s') s' + where + s' = trimEnd s + +highlights :: Int -> [String] -> String +highlights i ls = unlines $ zipWith cursorLine [i..] ls + +cursorLine :: Int -> String -> String +cursorLine l = printf "%s| %s" (lineString l) + +lineString :: Int -> String +lineString n = replicate (10 - nD) ' ' <> nS + where + nS = show n + nD = length nS + +-------------------------------------------------------------------------------- +-- | Source Span Construction +-------------------------------------------------------------------------------- +posSpan :: SourcePos -> SourceSpan +-------------------------------------------------------------------------------- +posSpan p = SS p p + +junkSpan :: SourceSpan +junkSpan = posSpan (initialPos "unknown") + +-------------------------------------------------------------------------------- +-- | Usage Mode +-------------------------------------------------------------------------------- +data Mode + = Json + | Cmdline + | Server + deriving (Eq, Show) + +-------------------------------------------------------------------------------- +-- | Representing (unrecoverable) failures +-------------------------------------------------------------------------------- +data UserError = Error + { eMsg :: !Text + , eSpan :: !SourceSpan + } + deriving (Show, Typeable) + +instance Located UserError where + sourceSpan = eSpan + +instance Exception [UserError] + +-------------------------------------------------------------------------------- +panic :: String -> SourceSpan -> a +-------------------------------------------------------------------------------- +panic msg sp = throw [Error msg sp] + +-------------------------------------------------------------------------------- +abort :: UserError -> b +-------------------------------------------------------------------------------- +abort e = throw [e] + +-------------------------------------------------------------------------------- +mkError :: Text -> SourceSpan -> UserError +-------------------------------------------------------------------------------- +mkError = Error + +-------------------------------------------------------------------------------- +renderErrors :: Mode -> [UserError] -> IO Text +-------------------------------------------------------------------------------- +renderErrors Json es = return (renderErrorsJson es) +renderErrors Server es = return (renderResultJson es) +renderErrors Cmdline es = renderErrorsText es + +renderErrorsText :: [UserError] -> IO Text +renderErrorsText [] = + return "" +renderErrorsText es = do + errs <- mapM renderError es + return $ L.intercalate "\n" ("Errors found!" : errs) + +renderError :: UserError -> IO Text +renderError e = do + let sp = sourceSpan e + snippet <- readFileSpan sp + return $ printf "%s: %s\n\n%s" (pprint sp) (eMsg e) snippet + +renderErrorsJson :: [UserError] -> Text +renderErrorsJson es = "RESULT\n" ++ showJSValue' (showJSON es) + +showJSValue' :: JSValue -> Text +showJSValue' x = showJSValue x "" + +renderResultJson :: [UserError] -> Text +renderResultJson es = showJSValue' $ jObj + [ ("types" , jObj [] ) + , ("status" , status es) + , ("errors" , showJSON es) + ] + where + status [] = showJSON ("safe" :: String) + status _ = showJSON ("unsafe" :: String) + + +instance JSON UserError where + readJSON = undefined + showJSON err = jObj [ ("start" , showJSON $ start err) + , ("stop" , showJSON $ stop err ) + , ("message", showJSON $ eMsg err ) + ] + where + start = ssBegin . eSpan + stop = ssEnd . eSpan + +jObj = JSObject . toJSObject + +instance JSON SourcePos where + readJSON = undefined + showJSON sp = jObj [ ("line" , showJSON l) + , ("column", showJSON c) + ] + where + l = sourceLine sp + c = sourceColumn sp diff --git a/src/Language/Elsa/Utils.hs b/src/Language/Elsa/Utils.hs new file mode 100644 --- /dev/null +++ b/src/Language/Elsa/Utils.hs @@ -0,0 +1,52 @@ +module Language.Elsa.Utils where + +import qualified Data.Map as M +import qualified Data.List as L +import Data.Monoid +import Data.Char (isSpace) +import Control.Exception +import Text.Printf +import System.Directory +import System.FilePath +import Debug.Trace (trace) + +groupBy :: (Ord k) => (a -> k) -> [a] -> [(k, [a])] +groupBy f = M.toList . L.foldl' (\m x -> inserts (f x) x m) M.empty + +inserts :: (Ord k) => k -> v -> M.Map k [v] -> M.Map k [v] +inserts k v m = M.insert k (v : M.findWithDefault [] k m) m + +dupBy :: (Ord k) => (a -> k) -> [a] -> [[a]] +dupBy f xs = [ xs' | (_, xs') <- groupBy f xs, 2 <= length xs' ] + +trim :: String -> String +trim = f . f where f = reverse . dropWhile isSpace + +trimEnd :: String -> String +trimEnd = reverse . dropWhile isSpace . reverse + +ensurePath :: FilePath -> IO () +ensurePath = createDirectoryIfMissing True . takeDirectory + +safeReadFile :: FilePath -> IO (Either String String) +safeReadFile f = (Right <$> readFile f) `catch` handleIO f + +handleIO :: FilePath -> IOException -> IO (Either String a) +handleIO f e = return . Left $ "Warning: Couldn't open " <> f <> ": " <> show e + +traceShow :: (Show a) => String -> a -> a +traceShow msg x = trace (printf "TRACE: %s = %s" msg (show x)) x + +safeHead :: a -> [a] -> a +safeHead def [] = def +safeHead _ (x:_) = x + +getRange :: Int -> Int -> [a] -> [a] +getRange i1 i2 + = take (i2 - i1 + 1) + . drop (i1 - 1) + + +fromEither :: Either a a -> a +fromEither (Left x) = x +fromEither (Right x) = x diff --git a/src/Main.hs b/src/Main.hs new file mode 100644 --- /dev/null +++ b/src/Main.hs @@ -0,0 +1,5 @@ + +import Language.Elsa.Runner (topMain) + +main :: IO () +main = topMain diff --git a/tests/Test.hs b/tests/Test.hs new file mode 100644 --- /dev/null +++ b/tests/Test.hs @@ -0,0 +1,11 @@ +{-# LANGUAGE OverloadedStrings #-} + +-- import Control.Exception +-- import Test.Tasty +-- import Common +-- import Data.List (isInfixOf) +-- import qualified Language.Elsa.Types as Nano +-- import qualified Language.Nano.Eval as Nano + +main :: IO () +main = return ()