packages feed

elsa (empty) → 0.1.0.0

raw patch · 12 files changed

+1156/−0 lines, 12 filesdep +arraydep +basedep +containerssetup-changed

Dependencies added: array, base, containers, directory, elsa, filepath, json, megaparsec, mtl, tasty, tasty-hunit

Files

+ LICENSE view
@@ -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.
+ README.md view
@@ -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 <id> = <term>]+++-- reductions+[<reduction>]*+```++where the basic elements are lambda-calulus `term`s++```haskell+<term> ::=  <id>+          \ <id>+ -> <term>+            (<term> <term>)+```++and `id` are lower-case identifiers            ++```+<id>   ::= x, y, z, ...+```++A `<reduction>` is a sequence of `term`s chained together+with a `<step>`++```haskell+<reduction> ::= eval <id> : <term> (<step> <term>)*++<step>      ::= =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**.
+ Setup.hs view
@@ -0,0 +1,2 @@+import Distribution.Simple+main = defaultMain
+ elsa.cabal view
@@ -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
+ src/Language/Elsa/Eval.hs view
@@ -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)
+ src/Language/Elsa/Parser.hs view
@@ -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)
+ src/Language/Elsa/Runner.hs view
@@ -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"
+ src/Language/Elsa/Types.hs view
@@ -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
+ src/Language/Elsa/UX.hs view
@@ -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
+ src/Language/Elsa/Utils.hs view
@@ -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
+ src/Main.hs view
@@ -0,0 +1,5 @@++import Language.Elsa.Runner (topMain)++main :: IO ()+main = topMain
+ tests/Test.hs view
@@ -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 ()