elsa 0.2.1.2 → 0.2.2.0

raw patch · 7 files changed

+130/−41 lines, 7 filesPVP ok

version bump matches the API change (PVP)

API changes (from Hackage documentation)

Files

• CHANGES.md +7/−0
• README.md +47/−1
• elsa.cabal +2/−2
• src/Language/Elsa/Eval.hs +45/−29
• src/Language/Elsa/Parser.hs +11/−5
• src/Language/Elsa/Types.hs +6/−0
• tests/Test.hs +12/−4

@@ -0,0 +1,7 @@+# Changes++0.2.2.0++- Faster (and correct!) implementation of Normalization by Mark Barbone (@mb64)+- Better parse error messages by Justin Yao Du (@justinyaodo)+- Updated to work with GHC 8.10.7 by Rose Kunkel (@rosekunkel)

@@ -11,7 +11,7 @@  ## Online Demo -You can try `elsa` online at [this link](http://goto.ucsd.edu:8095/index.html)+You can try `elsa` online at [this link](http://goto.ucsd.edu/elsa/index.html)  ## Install @@ -29,7 +29,11 @@ $ cd elsa $ stack install ```+## Editor Plugins +- [VSCode](https://github.com/mistzzt/vscode-elsa-lang)+- [Vim](https://github.com/glapa-grossklag/elsa.vim)+ ## Overview  `elsa` programs look like:@@ -188,6 +192,48 @@ * `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'`.+++(Due to Michael Borkowski)++The difference between `=*>` and `=~>` is as follows.++* `t =*> t'` is _any_ sequence of zero or more steps from `t` to `t'`. +  So if you are working forwards from the start, backwards from the end, +  or a combination of both, you could use `=*>` as a quick check to see +  if you're on the right track. ++* `t =~> t'` says that `t` reduces to `t'` in zero or more steps **and** +   that `t'` is in **normal form** (i.e. `t'` cannot be reduced further). +   This means you can only place it as the *final step*. ++So `elsa` would accept these three++```+eval ex1:+  (\x y -> x y) (\x -> x) b +  =*> b++eval ex2:+  (\x y -> x y) (\x -> x) b +  =~> b++eval ex3:+  (\x y -> x y) (\x -> x) (\z -> z) +  =*> (\x -> x) (\z -> z) +  =b> (\z -> z)+```++but `elsa` would *not* accept ++```+eval ex3:+  (\x y -> x y) (\x -> x) (\z -> z) +  =~> (\x -> x) (\z -> z) +  =b> (\z -> z)+```++because the right hand side of `=~>` can still be reduced further.  [normalform]: http://dl.acm.org/citation.cfm?id=860276 [normalform-pdf]: http://www.cs.cornell.edu/courses/cs6110/2014sp/Handouts/Sestoft.pdf

@@ -1,5 +1,5 @@ name:                elsa-version:             0.2.1.2+version:             0.2.2.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@@ -13,7 +13,7 @@ category:            Language Homepage:            http://github.com/ucsd-progsys/elsa build-type:          Simple-extra-source-files:  README.md+extra-source-files:  README.md, CHANGES.md cabal-version:       >=1.10  Source-Repository head

@@ -1,14 +1,15 @@-{-# LANGUAGE OverloadedStrings #-}+{-# LANGUAGE OverloadedStrings, BangPatterns #-}  module Language.Elsa.Eval (elsa, elsaOn) where  import qualified Data.HashMap.Strict  as M+import qualified Data.HashMap.Lazy    as ML import qualified Data.HashSet         as S import qualified Data.List            as L import           Control.Monad.State import qualified Data.Maybe           as Mb -- (isJust, maybeToList) import           Language.Elsa.Types-import           Language.Elsa.Utils  (traceShow, qPushes, qInit, qPop, fromEither)+import           Language.Elsa.Utils  (qPushes, qInit, qPop, fromEither)  -------------------------------------------------------------------------------- elsa :: Elsa a -> [Result a]@@ -21,11 +22,23 @@ elsaOn cond p =   case mkEnv (defns p) of     Left err -> [err]-    Right g  -> [result g e | e <- evals p, check e ]+    Right g  -> case checkDupEval (evals p) of+      Left err -> [err]+      Right _  -> [result g e | e <- evals p, check e ]   where     check = cond . bindId . evName +checkDupEval :: [Eval a] -> CheckM a (S.HashSet Id)+checkDupEval = foldM addEvalId S.empty +addEvalId :: S.HashSet Id -> Eval a -> CheckM a (S.HashSet Id)+addEvalId s e = +  if S.member (bindId b) s+    then Left  (errDupEval b)+    else Right (S.insert (bindId b) s)+  where+    b = evName e+ result :: Env a -> Eval a -> Result a result g e = fromEither (eval g e) @@ -33,10 +46,14 @@ 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)+expand g (Defn b e) = +  if dupId +    then Left (errDupDefn b)+    else case zs of+      (x,l) : _ -> Left  (Unbound b x l)+      []        -> Right (M.insert (bindId b) e' g)   where+    dupId           = M.member (bindId b) g     e'              = subst e g     zs              = M.toList (freeVars' e') @@ -192,34 +209,27 @@  -------------------------------------------------------------------------------- -- | Evaluation to Normal Form---   http://www.cs.cornell.edu/courses/cs6110/2014sp/Handouts/Sestoft.pdf -------------------------------------------------------------------------------- isNormEq :: Env a -> Expr a -> Expr a -> Bool-isNormEq g e1 e2 = isEquiv g e1' e2+isNormEq g e1 e2 = eqVal (subst e2 g) $ evalNbE ML.empty (subst e1 g)   where-    e1'          = traceShow ("evalNO" ++ show e1) $ evalNO (traceShow "CANON" $ 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+    evalNbE !env e = case e of+      EVar x _            -> Mb.fromMaybe (Neutral x []) $ ML.lookup x env+      ELam (Bind x _) b _ -> Fun $ \val -> evalNbE (ML.insert x val env) b+      EApp f arg _        -> case evalNbE env f of+        Fun f' -> f' (evalNbE env arg)+        Neutral x args -> Neutral x (evalNbE env arg:args) --- | 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+    eqVal (EVar x _) (Neutral x' [])+      = x == x'+    eqVal (ELam (Bind x _) b _) (Fun f)+      = eqVal b (f (Neutral x []))+    eqVal (EApp f a _) (Neutral x (a':args))+      = eqVal a a' && eqVal f (Neutral x args)+    eqVal _ _ = False --- | 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''       = e' -- alphaShift n e'+-- | NbE semantic domain+data Value = Fun !(Value -> Value) | Neutral !Id ![Value]  -------------------------------------------------------------------------------- -- | General Helpers@@ -253,3 +263,9 @@  errPartial :: Bind a -> Expr a -> Result a errPartial b e = Partial b (tag e)++errDupDefn :: Bind a -> Result a+errDupDefn b = DupDefn b (tag b)++errDupEval :: Bind a -> Result a+errDupEval b = DupEval b (tag b)

@@ -25,14 +25,20 @@  parseWith  :: Parser a -> FilePath -> Text -> a parseWith p f s = case runParser (whole p) f s of-                    Left pErrs -> Ex.throw (mkErrors pErrs) -- panic (show err) (posSpan . NE.head . errorPos $ err)+                    Left pErrs -> Ex.throw (mkErrors pErrs f s) -- panic (show err) (posSpan . NE.head . errorPos $ err)                     Right e  -> e +mkErrors :: ParseErrorBundle Text SourcePos -> FilePath -> Text -> [UserError]+mkErrors b f s = [ mkError (parseErrorPretty e) (span e) | e <- NE.toList (bundleErrors b)]+  where+    span e = let (l, c) = lineCol s (errorOffset e) in posSpan (SourcePos f (mkPos l) (mkPos c)) -mkErrors :: ParseErrorBundle Text SourcePos -> [UserError]-mkErrors b = [ mkError (parseErrorPretty e) (sp b) | e <- NE.toList (bundleErrors b)]-  where -    sp     = posSpan . pstateSourcePos . bundlePosState+-- PosState looks relevant for finding line/column, but I (Justin) don't know how to use it++lineCol :: String -> Int -> (Int, Int)+lineCol s i = foldl f (1, 1) (Prelude.take i s)+  where+    f (l, c) char = if char == '\n' then (l + 1, 1) else (l, c + 1)  instance ShowErrorComponent SourcePos where   showErrorComponent = show

@@ -30,6 +30,8 @@   | Partial (Bind a)    a   | Invalid (Bind a)    a   | Unbound (Bind a) Id a+  | DupDefn (Bind a)    a+  | DupEval (Bind a)    a   deriving (Eq, Show, Functor)  failures :: [Result a] -> [Id]@@ -38,6 +40,8 @@     go (Partial b _)   = Just (bindId b)     go (Invalid b _)   = Just (bindId b)     go (Unbound b _ _) = Just (bindId b)+    go (DupDefn b _)   = Just (bindId b)+    go (DupEval b _)   = Just (bindId b)     go _               = Nothing  successes :: [Result a] -> [Id]@@ -50,6 +54,8 @@ 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 (DupDefn b l)   = mkErr l ("Definition " ++ (bindId b) ++ " has already been declared")+resultError (DupEval b l)   = mkErr l ("Evaluation " ++ (bindId b) ++ " has already been declared") resultError _               = Nothing  mkErr :: (Located a) => a -> Text -> Maybe UserError

@@ -22,6 +22,8 @@   [ testGroup "ok"      <$> dirTests "tests/ok"       TestOk   , testGroup "further" <$> dirTests "tests/further"  TestPartial   , testGroup "invalid" <$> dirTests "tests/invalid"  TestInvalid+  , testGroup "dupdefn" <$> dirTests "tests/dupdefn"  TestDupDefn+  , testGroup "dupeval" <$> dirTests "tests/dupeval"  TestDupEval   ]  data Outcome@@ -29,6 +31,8 @@   | TestPartial   | TestInvalid   | TestMixed+  | TestDupDefn+  | TestDupEval   deriving (Eq, Ord, Show)  --------------------------------------------------------------------------------@@ -54,15 +58,19 @@ doTest f =  resultOutcome . elsa <$> parseFile f  resultOutcome :: [Result a] -> Outcome-resultOutcome rs = case (oks, invs, parts) of-                     (True, False, False) -> TestOk-                     (False, True, False) -> TestInvalid-                     (False, False, True) -> TestPartial+resultOutcome rs = case (oks, invs, parts, ddefn, deval) of+                     (True, False, False, False, False) -> TestOk+                     (False, True, False, False, False) -> TestInvalid+                     (False, False, True, False, False) -> TestPartial+                     (False, False, False, True, False) -> TestDupDefn+                     (False, False, False, False, True) -> TestDupEval                      _                    -> TestMixed   where     oks          = notNull [ r | r@(OK {})      <- rs ]     invs         = notNull [ r | r@(Invalid {}) <- rs ]     parts        = notNull [ r | r@(Partial {}) <- rs ]+    ddefn        = notNull [ r | r@(DupDefn {}) <- rs ]+    deval        = notNull [ r | r@(DupEval {}) <- rs ]     notNull      = not . null  ----------------------------------------------------------------------------------------