elsa 0.2.0.1 → 0.2.1.0
raw patch · 6 files changed
+46/−32 lines, 6 files
Files
- elsa.cabal +1/−1
- src/Language/Elsa/Eval.hs +5/−7
- src/Language/Elsa/Parser.hs +31/−13
- src/Language/Elsa/Types.hs +0/−1
- src/Language/Elsa/UX.hs +9/−9
- src/Language/Elsa/Utils.hs +0/−1
elsa.cabal view
@@ -1,5 +1,5 @@ name: elsa-version: 0.2.0.1+version: 0.2.1.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
src/Language/Elsa/Eval.hs view
@@ -6,7 +6,7 @@ import qualified Data.HashSet as S import qualified Data.List as L import Control.Monad.State-import Data.Maybe (mapMaybe, isJust, maybeToList)+import qualified Data.Maybe as Mb -- (isJust, maybeToList) import Language.Elsa.Types import Language.Elsa.Utils (traceShow, qPushes, qInit, qPop, fromEither) @@ -74,7 +74,7 @@ -- | Transitive Reachability -------------------------------------------------------------------------------- isTrnsEq :: Env a -> Expr a -> Expr a -> Bool-isTrnsEq g e1 e2 = isJust (findTrans (isEquiv g e2) (canon g e1))+isTrnsEq g e1 e2 = Mb.isJust (findTrans (isEquiv g e2) (canon g e1)) isUnTrEq :: Env a -> Expr a -> Expr a -> Bool isUnTrEq g e1 e2 = isTrnsEq g e2 e1@@ -137,8 +137,8 @@ newAId :: Int -> Id newAId n = aId ++ show n -isAId :: Id -> Maybe Int-isAId x+_isAId :: Id -> Maybe Int+_isAId x | L.isPrefixOf aId x = Just . read . drop 2 $ x | otherwise = Nothing @@ -164,7 +164,7 @@ 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)+ ++ Mb.maybeToList (beta e1 e2) beta :: Expr a -> Expr a -> Maybe (Expr a) beta (ELam (Bind x _) e _) e' = substCA e x e'@@ -220,8 +220,6 @@ bSubst e x e' = subst e (M.singleton x e'') where e'' = e' -- alphaShift n e'- n = 1 + maximum (0 : mapMaybe isAId vs)- vs = S.toList (freeVars e') -------------------------------------------------------------------------------- -- | General Helpers
src/Language/Elsa/Parser.hs view
@@ -1,16 +1,23 @@+{-# LANGUAGE FlexibleInstances #-}+ module Language.Elsa.Parser ( parse , parseFile ) where -import Control.Monad (void)+import qualified Control.Exception as Ex+import Control.Monad (void) import Text.Megaparsec hiding (parse)-import Text.Megaparsec.String-import qualified Text.Megaparsec.Lexer as L+import qualified Text.Megaparsec.Char.Lexer as L+import Text.Megaparsec.Char+import Text.Megaparsec.Stream () import qualified Data.List as L import Language.Elsa.Types import Language.Elsa.UX+import Data.List.NonEmpty as NE +type Parser = Parsec SourcePos Text+ -------------------------------------------------------------------------------- parse :: FilePath -> Text -> SElsa --------------------------------------------------------------------------------@@ -18,15 +25,26 @@ 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)+ Left pErrs -> Ex.throw (mkErrors pErrs) -- panic (show err) (posSpan . NE.head . errorPos $ err) Right e -> e -instance Located ParseError where- sourceSpan = posSpan . errorPos -instance PPrint ParseError where- pprint = show+mkErrors :: ParseErrorBundle Text SourcePos -> [UserError]+mkErrors b = [ mkError (parseErrorPretty e) (sp b) | e <- NE.toList (bundleErrors b)]+ where + sp = posSpan . pstateSourcePos . bundlePosState +instance ShowErrorComponent SourcePos where+ showErrorComponent = show+ ++-- panic msg sp = throw [Error msg sp]+-- instance Located (ParseError SourcePos Text) where+-- sourceSpan = posSpan . errorPos++-- instance PPrint (ParseError SourcePos Text) where+-- pprint = show+ -------------------------------------------------------------------------------- parseFile :: FilePath -> IO SElsa --------------------------------------------------------------------------------@@ -92,7 +110,7 @@ identChar :: Parser Char identChar = alphaNumChar- <|> oneOf "_#'"+ <|> oneOf ['_', '#', '\''] -- | `binder` parses BareBind, used for let-binds and function parameters. binder :: Parser SBind@@ -100,16 +118,16 @@ withSpan' :: Parser (SourceSpan -> a) -> Parser a withSpan' p = do- p1 <- getPosition+ p1 <- getSourcePos f <- p- p2 <- getPosition+ p2 <- getSourcePos return (f (SS p1 p2)) withSpan :: Parser a -> Parser (a, SourceSpan) withSpan p = do- p1 <- getPosition+ p1 <- getSourcePos x <- p- p2 <- getPosition+ p2 <- getSourcePos return (x, SS p1 p2) --------------------------------------------------------------------------------
src/Language/Elsa/Types.hs view
@@ -7,7 +7,6 @@ import GHC.Generics import Text.Printf (printf)-import Data.Monoid import Language.Elsa.UX import Data.Maybe (mapMaybe) import Data.Hashable
src/Language/Elsa/UX.hs view
@@ -38,12 +38,9 @@ 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 @@ -70,6 +67,9 @@ } deriving (Eq, Show) +instance Semigroup SourceSpan where+ x <> y = mappendSpan x y + instance Monoid SourceSpan where mempty = junkSpan mappend = mappendSpan@@ -94,10 +94,10 @@ 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+ l1 = unPos . sourceLine . ssBegin+ c1 = unPos . sourceColumn . ssBegin+ l2 = unPos . sourceLine . ssEnd+ c2 = unPos . sourceColumn . ssEnd -------------------------------------------------------------------------------- -- | Source Span Extraction@@ -263,8 +263,8 @@ instance JSON SourcePos where readJSON = undefined- showJSON sp = jObj [ ("line" , showJSON l)- , ("column", showJSON c)+ showJSON sp = jObj [ ("line" , showJSON (unPos l))+ , ("column", showJSON (unPos c)) ] where l = sourceLine sp
src/Language/Elsa/Utils.hs view
@@ -4,7 +4,6 @@ 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 import Text.Printf