elsa 0.1.0.0 → 0.1.0.1
raw patch · 8 files changed
+268/−80 lines, 8 filesdep +dequeuedep +hashabledep +unordered-containersdep −containers
Dependencies added: dequeue, hashable, unordered-containers
Dependencies removed: containers
Files
- README.md +24/−11
- elsa.cabal +9/−8
- src/Language/Elsa.hs +8/−0
- src/Language/Elsa/Eval.hs +112/−20
- src/Language/Elsa/Parser.hs +9/−5
- src/Language/Elsa/Runner.hs +26/−10
- src/Language/Elsa/Types.hs +51/−18
- src/Language/Elsa/Utils.hs +29/−8
README.md view
@@ -9,13 +9,13 @@ whether, under a given sequence of definitions, a particular term _reduces to_ to another. -## Online Demo +## Online Demo You can try `elsa` online at [this link](http://goto.ucsd.edu:8095/index.html) -## Install +## Install -You can locally build and run `elsa` by +You can locally build and run `elsa` by 1. Installing [stack](https://www.haskellstack.org) 2. Cloning this repo@@ -23,14 +23,14 @@ That is, to say -```bash +```bash $ curl -sSL https://get.haskellstack.org/ | sh $ git clone https://github.com/ucsd-progsys/elsa.git-$ cd elsa +$ cd elsa $ stack install ``` -## Overview +## Overview `elsa` programs look like: @@ -41,9 +41,14 @@ eval id_zero : id zero- =d> (\x -> x) (\f x -> x)- =b> (\f x -> x)- =d> zero+ =d> (\x -> x) (\f x -> x) -- expand definitions+ =a> (\z -> z) (\f x -> x) -- alpha rename+ =b> (\f x -> x) -- beta reduce+ =d> zero -- expand definitions++eval id_zero_tr :+ id zero + =*> zero -- transitive reductions ``` When you run `elsa` on the above, you should get the following output:@@ -51,7 +56,7 @@ ```bash $ elsa ex1.lc -OK id_zero.+OK id_zero, id_zero_tr. ``` ## Partial Evaluation@@ -97,7 +102,7 @@ =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 + =b> \f x -> f (f x) -- beta-reduce the above =d> two -- optional ``` @@ -163,6 +168,8 @@ <step> ::= =a> -- alpha equivalence =b> -- beta equivalence =d> -- def equivalence+ =*> -- trans equivalence+ =~> -- normalizes to ``` @@ -178,3 +185,9 @@ * `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**.+* `t =*> t'` is valid if `t` and `t'` are in the reflexive, transitive closure+ of the union of the above three relations.+* `t =~> t'` is valid if `t` [normalizes to][normalform] `t'`.++[normalform]: http://dl.acm.org/citation.cfm?id=860276+[normalform-pdf]: http://www.cs.cornell.edu/courses/cs6110/2014sp/Handouts/Sestoft.pdf
elsa.cabal view
@@ -1,7 +1,7 @@ name: elsa-version: 0.1.0.0+version: 0.1.0.1 synopsis: A tiny language for understanding the lambda-calculus-description: elsa is a small proof checker for verifying sequences of +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@@ -11,7 +11,7 @@ author: Ranjit Jhala maintainer: jhala@cs.ucsd.edu category: Language-Homepage: http://github.com/ucsd-progsys/elsa +Homepage: http://github.com/ucsd-progsys/elsa build-type: Simple extra-source-files: README.md cabal-version: >=1.10@@ -21,27 +21,28 @@ Location: https://github.com/ucsd-progsys/elsa/ Library- ghc-options: -W - exposed-modules: Language.Elsa.Types,+ ghc-options: -W+ exposed-modules: Language.Elsa+ 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,+ hashable,+ unordered-containers, directory, filepath,+ dequeue, json hs-source-dirs: src default-language: Haskell2010--- build-tools: alex, happy other-modules: Language.Elsa.UX, Language.Elsa.Utils
+ src/Language/Elsa.hs view
@@ -0,0 +1,8 @@+-- Re-export library++module Language.Elsa ( module X ) where++import Language.Elsa.Types as X+import Language.Elsa.Parser as X+import Language.Elsa.Eval as X+import Language.Elsa.Runner as X
src/Language/Elsa/Eval.hs view
@@ -1,21 +1,32 @@ {-# LANGUAGE OverloadedStrings #-} -module Language.Elsa.Eval where+module Language.Elsa.Eval (elsa, elsaOn) where -import qualified Data.Map as M-import qualified Data.Set as S+import qualified Data.HashMap.Strict as M+import qualified Data.HashSet as S+import qualified Data.List as L import Control.Monad.State-import Data.Maybe (maybeToList)+import Data.Maybe (mapMaybe, isJust, maybeToList) import Language.Elsa.Types-import Language.Elsa.Utils (fromEither)+import Language.Elsa.Utils (qPushes, qInit, qPop, fromEither) + -------------------------------------------------------------------------------- elsa :: Elsa a -> [Result a] ---------------------------------------------------------------------------------elsa p = case mkEnv (defns p) of- Left err -> [err]- Right g -> [result g e | e <- evals p]+elsa = elsaOn (const True) +--------------------------------------------------------------------------------+elsaOn :: (Id -> Bool) -> Elsa a -> [Result a]+--------------------------------------------------------------------------------+elsaOn cond p =+ case mkEnv (defns p) of+ Left err -> [err]+ Right g -> [result g e | e <- evals p, check e ]+ where+ check = cond . bindId . evName++ result :: Env a -> Eval a -> Result a result g e = fromEither (eval g e) @@ -32,7 +43,7 @@ -------------------------------------------------------------------------------- type CheckM a b = Either (Result a) b-type Env a = M.Map Id (Expr a)+type Env a = M.HashMap Id (Expr a) -------------------------------------------------------------------------------- --------------------------------------------------------------------------------@@ -53,9 +64,34 @@ isEq :: Eqn a -> Env a -> Expr a -> Expr a -> Bool isEq (AlphEq _) = isAlphEq isEq (BetaEq _) = isBetaEq+isEq (UnBeta _) = isUnBeta isEq (DefnEq _) = isDefnEq+isEq (TrnsEq _) = isTrnsEq+isEq (UnTrEq _) = isUnTrEq+isEq (NormEq _) = isNormEq + --------------------------------------------------------------------------------+-- | Transitive Reachability+--------------------------------------------------------------------------------+isTrnsEq :: Env a -> Expr a -> Expr a -> Bool+isTrnsEq g e1 e2 = isJust (findTrans (isEquiv g e2) (canon g e1))++isUnTrEq :: Env a -> Expr a -> Expr a -> Bool+isUnTrEq g e1 e2 = isTrnsEq g e2 e1++findTrans :: (Expr a -> Bool) -> Expr a -> Maybe (Expr a)+findTrans p e = go S.empty (qInit e)+ where+ go seen q = do+ (e, q') <- qPop q+ if S.member e seen+ then go seen q'+ else if p e+ then return e+ else go (S.insert e seen) (qPushes q (betas e))++-------------------------------------------------------------------------------- -- | Definition Equivalence -------------------------------------------------------------------------------- isDefnEq :: Env a -> Expr a -> Expr a -> Bool@@ -68,11 +104,14 @@ isAlphEq _ e1 e2 = alphaNormal e1 == alphaNormal e2 alphaNormal :: Expr a -> Expr a-alphaNormal e = evalState (normalize M.empty e) 0+alphaNormal = alphaShift 0 +alphaShift :: Int -> Expr a -> Expr a+alphaShift n e = evalState (normalize M.empty e) n+ type AlphaM a = State Int a -normalize :: M.Map Id Id -> Expr a -> AlphaM (Expr a)+normalize :: M.HashMap Id Id -> Expr a -> AlphaM (Expr a) normalize g (EVar x z) = return (EVar (rename g x) z) @@ -87,21 +126,35 @@ 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+rename :: M.HashMap Id Id -> Id -> Id+rename g x = M.lookupDefault x x g fresh :: AlphaM Id fresh = do n <- get put (n + 1)- return ("$x" ++ show n)+ return (newAId n) +newAId :: Int -> Id+newAId n = aId ++ show n++isAId :: Id -> Maybe Int+isAId x+ | L.isPrefixOf aId x = Just . read . drop 2 $ x+ | otherwise = Nothing++aId :: String+aId = "$x"+ -------------------------------------------------------------------------------- -- | Beta Reduction -------------------------------------------------------------------------------- isBetaEq :: Env a -> Expr a -> Expr a -> Bool-isBetaEq _ e1 e2 = or [ e1' == e2 | e1' <- betas e1]+isBetaEq _ e1 e2 = or [ e1' == e2 | e1' <- betas e1 ] +isUnBeta :: Env a -> Expr a -> Expr a -> Bool+isUnBeta g e1 e2 = isBetaEq g e2 e1+ isNormal :: Env a -> Expr a -> Bool isNormal g = null . betas . (`subst` g) @@ -133,30 +186,69 @@ 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 :: Bind a -> S.HashSet Id -> Bool isIn = S.member . bindId ----------------------------------------------------------------------------------- | Free Variables and Substitution+-- | Evaluation to Normal Form+-- http://www.cs.cornell.edu/courses/cs6110/2014sp/Handouts/Sestoft.pdf ---------------------------------------------------------------------------------freeVars :: Expr a -> S.Set Id+isNormEq :: Env a -> Expr a -> Expr a -> Bool+isNormEq g e1 e2 = isEquiv g e1' e2+ where+ e1' = evalNO (canon g e1)++-- | normal-order reduction+evalNO :: Expr a -> Expr a+evalNO e@(EVar {}) = e+evalNO (ELam b e l) = ELam b (evalNO e) l+evalNO (EApp e1 e2 l) = case evalCBN e1 of+ ELam b e1' _ -> evalNO (bSubst e1' (bindId b) e2)+ e1' -> EApp (evalNO e1') (evalNO e2) l++-- | call-by-name reduction+evalCBN :: Expr a -> Expr a+evalCBN e@(EVar {}) = e+evalCBN e@(ELam {}) = e+evalCBN (EApp e1 e2 l) = case evalCBN e1 of+ ELam b e1' _ -> evalCBN (bSubst e1' (bindId b) e2)+ e1' -> EApp e1' e2 l++-- | Force alpha-renaming to ensure capture avoiding subst+bSubst :: Expr a -> Id -> Expr a -> Expr a+bSubst e x e' = subst e (M.singleton x e'')+ where+ e'' = alphaShift n e'+ n = 1 + maximum (0 : mapMaybe isAId vs)+ vs = S.toList (freeVars e')++--------------------------------------------------------------------------------+-- | General Helpers+--------------------------------------------------------------------------------+freeVars :: Expr a -> S.HashSet Id freeVars = S.fromList . M.keys . freeVars' -freeVars' :: Expr a -> M.Map Id a+freeVars' :: Expr a -> M.HashMap 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 e@(EVar v _) su = M.lookupDefault 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 +canon :: Env a -> Expr a -> Expr a+canon g = alphaNormal . (`subst` g)++isEquiv :: Env a -> Expr a -> Expr a -> Bool+isEquiv g e1 e2 = isAlphEq g (subst e1 g) (subst e2 g) -------------------------------------------------------------------------------- -- | Error Cases --------------------------------------------------------------------------------+ errInvalid :: Bind a -> Expr a -> Eqn a -> Expr a -> Result a errInvalid b _ eqn _ = Invalid b (tag eqn)
src/Language/Elsa/Parser.hs view
@@ -1,4 +1,7 @@-module Language.Elsa.Parser ( parse, parseFile ) where+module Language.Elsa.Parser+ ( parse+ , parseFile+ ) where import Control.Monad (void) import Text.Megaparsec hiding (parse)@@ -137,10 +140,11 @@ 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 []+ <|> try (withSpan' (symbol "<b=" >> return UnBeta))+ <|> try (withSpan' (symbol "=d>" >> return DefnEq))+ <|> try (withSpan' (symbol "=*>" >> return TrnsEq))+ <|> try (withSpan' (symbol "<*=" >> return UnTrEq))+ <|> (withSpan' (symbol "=~>" >> return NormEq)) expr :: Parser SExpr expr = try lamExpr
src/Language/Elsa/Runner.hs view
@@ -1,21 +1,24 @@ {-# LANGUAGE ScopedTypeVariables #-} -module Language.Elsa.Runner where+module Language.Elsa.Runner+ ( topMain+ , runElsa+ , runElsaId+ ) where import Data.List (intercalate) import Data.Maybe (mapMaybe)-import Control.Monad (when)+import Control.Monad (when, void) 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 System.FilePath+import System.Directory+import Language.Elsa.Parser+import Language.Elsa.Types import Language.Elsa.UX-import Language.Elsa.Eval (elsa)-+import Language.Elsa.Eval topMain:: IO () topMain = do@@ -45,8 +48,8 @@ runElsa :: Mode -> FilePath -> Text -> IO () runElsa mode f s = do- let rs = elsa (parse f s)- let es = mapMaybe resultError rs+ let rs = elsa (parse f s)+ let es = mapMaybe resultError rs when (null es && mode == Cmdline) (putStrLn (okMessage rs)) exitErrors mode f es @@ -60,3 +63,16 @@ ["--server", f] -> return (Server, f) [f] -> return (Cmdline, f) _ -> error "Please run with a single file as input"+++--------------------------------------------------------------------------------+runElsaId :: FilePath -> Id -> IO (Maybe (Result ()))+--------------------------------------------------------------------------------+runElsaId f x = ((`runElsa1` x) <$> parseFile f)+ `catch`+ (\(_ :: [UserError]) -> return Nothing)++runElsa1 :: Elsa a -> Id -> Maybe (Result ())+runElsa1 p x = case elsaOn (== x) p of+ [r] -> Just (void r)+ _ -> Nothing
src/Language/Elsa/Types.hs view
@@ -1,33 +1,37 @@ {-# LANGUAGE OverloadedStrings #-} {-# LANGUAGE FlexibleInstances #-}+{-# LANGUAGE DeriveGeneric #-}+{-# LANGUAGE DeriveFunctor #-} module Language.Elsa.Types where +import GHC.Generics 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+import Data.Hashable +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+type SResult = Result SourceSpan -------------------------------------------------------------------------------- -- | Result --------------------------------------------------------------------------------+ data Result a = OK (Bind a) | Partial (Bind a) a | Invalid (Bind a) a | Unbound (Bind a) Id a- deriving (Eq, Show)+ deriving (Eq, Show, Functor) failures :: [Result a] -> [Id] failures = mapMaybe go@@ -55,7 +59,6 @@ -------------------------------------------------------------------------------- -- | Programs --------------------------------------------------------------------------------- data Elsa a = Elsa { defns :: [Defn a] , evals :: [Eval a]@@ -80,28 +83,54 @@ data Eqn a = AlphEq a | BetaEq a+ | UnBeta a | DefnEq a+ | TrnsEq a+ | UnTrEq a+ | NormEq a deriving (Eq, Show) data Bind a = Bind Id a- deriving (Show)+ deriving (Show, Functor) data Expr a = EVar Id a | ELam !(Bind a) !(Expr a) a | EApp !(Expr a) !(Expr a) a- deriving (Show)+-- deriving (Show) +instance Show (Expr a) where+ show = pprint+ 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++data RExpr+ = RVar Id+ | RLam Id RExpr+ | RApp RExpr RExpr+ deriving (Eq, Generic)++rExpr :: Expr a -> RExpr+rExpr (EVar x _) = RVar x+rExpr (ELam b e _) = RLam (bindId b) (rExpr e )+rExpr (EApp e e' _) = RApp (rExpr e) (rExpr e')+ 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+ e1 == e2 = rExpr e1 == rExpr e2 +instance Hashable RExpr++instance Hashable (Expr a) where+ hashWithSalt i = hashWithSalt i . rExpr+ ------------------------------------------------------------------------------------- -- | Pretty Printing -------------------------------------------------------------------------------------@@ -140,7 +169,11 @@ instance Tagged Eqn where tag (AlphEq x) = x tag (BetaEq x) = x+ tag (UnBeta x) = x tag (DefnEq x) = x+ tag (TrnsEq x) = x+ tag (UnTrEq x) = x+ tag (NormEq x) = x instance Tagged Bind where tag (Bind _ x) = x
src/Language/Elsa/Utils.hs view
@@ -1,7 +1,9 @@ module Language.Elsa.Utils where -import qualified Data.Map as M-import qualified Data.List as L+import qualified Data.HashMap.Strict as M+import qualified Data.List as L+import qualified Data.Dequeue as Q+import Data.Hashable import Data.Monoid import Data.Char (isSpace) import Control.Exception@@ -10,13 +12,13 @@ import System.FilePath import Debug.Trace (trace) -groupBy :: (Ord k) => (a -> k) -> [a] -> [(k, [a])]+groupBy :: (Eq k, Hashable 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+inserts :: (Eq k, Hashable k) => k -> v -> M.HashMap k [v] -> M.HashMap k [v]+inserts k v m = M.insert k (v : M.lookupDefault [] k m) m -dupBy :: (Ord k) => (a -> k) -> [a] -> [[a]]+dupBy :: (Eq k, Hashable k) => (a -> k) -> [a] -> [[a]] dupBy f xs = [ xs' | (_, xs') <- groupBy f xs, 2 <= length xs' ] trim :: String -> String@@ -46,7 +48,26 @@ = take (i2 - i1 + 1) . drop (i1 - 1) - fromEither :: Either a a -> a-fromEither (Left x) = x +fromEither (Left x) = x fromEither (Right x) = x++--------------------------------------------------------------------------------+-- | Queue ---------------------------------------------------------------------+--------------------------------------------------------------------------------++newtype Queue a = Q (Q.BankersDequeue a)++qEmpty :: Queue a+qEmpty = Q Q.empty++qInit :: a -> Queue a+qInit x = qPushes qEmpty [x]++qPushes :: Queue a -> [a] -> Queue a+qPushes (Q q) xs = Q (L.foldl' Q.pushFront q xs)++qPop :: Queue a -> Maybe (a, Queue a)+qPop (Q q) = case Q.popBack q of+ Nothing -> Nothing+ Just (x, q') -> Just (x, Q q')