elsa 0.2.2.0 → 0.3.0.0

raw patch · 6 files changed

+587/−124 lines, 6 filesdep ~ansi-terminaldep ~arraydep ~dequeuePVP ok

version bump matches the API change (PVP)

Dependency ranges changed: ansi-terminal, array, dequeue, directory, filepath, hashable, json, megaparsec, mtl, unordered-containers

API changes (from Hackage documentation)

Files

• CHANGES.md +12/−0
• README.md +174/−34
• elsa.cabal +11/−11
• src/Language/Elsa/Eval.hs +279/−41
• src/Language/Elsa/Parser.hs +60/−11
• src/Language/Elsa/Types.hs +51/−27

@@ -1,5 +1,17 @@ # Changes +0.3.0.0 ++- bump to GHC 9.8.4 by @ilanashapiro++- new evaluation steps and strategies by @JRB-Prod-UVA+    - A new operator =e> for the eta reduction has been added.+    - Definitions introduced with let and the evaluation or confirmation statements can now be used interchangeably. So after an evaluation or confirmation block a new let binding can be introduced.+    - Reduction and equivalence checking sequence that do not have to end in a strong normal form are now also supported, by replacing the keyword `eval` with `conf`+    - Different normal form checks on arbitrary reduction and equivalence proof checking results are now supported.+    - Support for two specific reduction strategies: normal order and applicative order were added. For this, we introduced two new operators (`=n>` and `=p>`).++ 0.2.2.0  - Faster (and correct!) implementation of Normalization by Mark Barbone (@mb64)

@@ -11,8 +11,9 @@  ## Online Demo -You can try `elsa` online at [this link](http://goto.ucsd.edu/elsa/index.html)+You can try `elsa` online at [this link](https://elsa.goto.ucsd.edu/index.html) + ## Install  You can locally build and run `elsa` by@@ -31,7 +32,9 @@ ``` ## Editor Plugins -- [VSCode](https://github.com/mistzzt/vscode-elsa-lang)+- [VS Code extension](https://marketplace.visualstudio.com/items?itemName=akainth015.elsa-lang) with syntax highlighting and autocompletion support+  - [Source](https://github.com/akainth015/vscode-elsa-lang)+  - Contributed by [**@akainth015**](https://github.com/akainth015/), based on the [original version](https://github.com/mistzzt/vscode-elsa-lang) by [**@mistzzt**](https://github.com/mistzzt) - [Vim](https://github.com/glapa-grossklag/elsa.vim)  ## Overview@@ -51,7 +54,7 @@   =d> zero                    -- expand definitions  eval id_zero_tr :-  id zero  +  id zero   =*> zero                    -- transitive reductions ``` @@ -63,6 +66,82 @@ OK id_zero, id_zero_tr. ``` +## Operators and Normal Form Checking++Elsa supports several operators with optional normal form checking:++### Basic Operators+- `=a>` - alpha equivalence+- `=b>` - single beta reduction+- `=e>` - single eta reduction+- `=d>` - definition expansion+- `=n>` - normal order beta reduction+- `=p>` - applicative order beta reduction+- `=*>` - transitive closure of reductions++### Normal Form Extensions+All operators can be extended with normal form checks:+- `=op:s>` - check strong normal form after operation+- `=op:w>` - check weak normal form after operation+- `=op:h>` - check head normal form after operation++Examples:+```haskell+-- nf_0.lc+let id = \z -> z++-- Check beta reduction to weak normal form+conf example1:+  (\x y -> x (\w -> w w)) id+  =b:w> (\y -> id (\w -> w w))++-- Check beta reduction to head normal form+conf example2:+  ((\x -> x) Z) (\x y -> x (\w -> w w)) id+  =b:h> Z (\x y -> x (\w -> w w)) id++-- Normal order reduction to strong normal form+conf example3:+  (\x y -> x) id+  =n:s> \y -> id+```++### Strategy-Specific Transitive Reductions+- `=n*>` - normal order transitive reductions+- `=p*>` - applicative order transitive reductions++Example:+```haskell+-- sptr_0.lc++-- The numbers 0, 1, 3, 6 in church encoding+let c0 = \f x -> x+let c1 = \f x -> f x+let c3 = \f x -> f (f (f x))+let c6 = \f x -> f (f (f (f (f (f x)))))++-- Boolean functions+let true = \x y -> x+let false = \x y -> y++-- Number operations+let iszero = \n -> n (\x -> false) true+let pred = \n f x -> n (\g h -> h (g f)) (\u -> x) (\u -> u)+let mult = \m n f x -> m (n f) x++-- Fixed-point combinator and recursive function+let Y = \g -> (\x -> g (x x)) (\x -> g (x x))+let G = \f n -> iszero n c1 (mult n (f (pred n)))+let fact = Y G++eval factorial:+  fact c3+  -- The next line shows that we can show specific intermediate steps and leave out the rest+  =n*> iszero c3 c1 (mult c3 (((\x -> G (x x)) (\x -> G (x x))) (pred c3)))+  =n*> c6 --In this case, using =~> also works++```+ ## Partial Evaluation  If instead you write a partial sequence of@@ -110,6 +189,22 @@   =d> two                             -- optional ``` +Or you can change evaluation method, by changing+`eval` to `conf` (see also next section)++```haskell+-- succ_1_alt.lc+let one  = \f x -> f x+let two  = \f x -> f (f x)+let incr = \n f x -> f (n f x)++conf 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)+```+ Similarly, `elsa` rejects the following program,  ```haskell@@ -137,16 +232,32 @@ You can fix the error by inserting the appropriate intermediate term as shown in `id_0.lc` above. +## Confirmation Statements++The `conf` statement works like `eval` but+doesn't require the final term to be in normal+form. This is useful for infinite reductions+or intermediate proofs.++Example:+```haskell+-- om_0.lc+let omega = (\x -> x x) (\x -> x x)++conf omega_reduces_to_self:+  omega+  =d> (\x -> x x) (\x -> x x)+  =b> (\x -> x x) (\x -> x x)+  =d> omega+```+ ## Syntax of `elsa` Programs  An `elsa` program has the form  ```haskell--- definitions-[let <id> = <term>]+---- reductions-[<reduction>]*+-- definitions and evaluations can be mixed+  ([let <id> = <term>] | [<reduction>])* ```  where the basic elements are lambda-calulus `term`s@@ -156,8 +267,7 @@           \ <id>+ -> <term>             (<term> <term>) ```--and `id` are lower-case identifiers            +and `id` are lower-case identifiers  ``` <id>   ::= x, y, z, ...@@ -167,69 +277,99 @@ with a `<step>`  ```haskell-<reduction> ::= eval <id> : <term> (<step> <term>)*+<reduction> ::= (eval | conf) <id> : <term> (<step> <term>)* -<step>      ::= =a>   -- alpha equivalence-                =b>   -- beta  equivalence-                =d>   -- def   equivalence-                =*>   -- trans equivalence-                =~>   -- normalizes to+<step> ::= =, <equivtype>, [:, <nfcheck>], >++<equivtype> ::= a   -- alpha equivalence+                b   -- beta  equivalence+                e   -- eta   equivalence+                d   -- def   equivalence+                *   -- trans equivalence+                n   -- normal order            beta equivalence+                p   -- applicative order       beta equivalence+                n*  -- normal order      trans beta equivalence+                p*  -- applicative order trans beta equivalence+                ~   -- normalizes to++<nfcheck> ::= s -- strong normal form check+              w -- weak normal form check+              h -- head normal form check ```   ## Semantics of `elsa` programs -A `reduction` of the form `t_1 s_1 t_2 s_2 ... t_n` is **valid** if+An `eval` `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  +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**. * `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'`.+             of the union of the above three relations,+* `t =n> t'` is valid if `t` **beta-reduces** using normal order to `t'` in+             a single step,+* `t =p> t'` is valid if `t` **beta-reduces** using applicative order to `t'`+             in a single step,+* `t =n*> t'` is valid if `t` and `t'` are in the reflexive, transitive closure+             of the union of the `=a>`, `=d>` and `=n>` operator relations,+* `t =p*> t'` is valid if `t` and `t'` are in the reflexive, transitive closure+             of the union of the `=a>`, `=d>` and `=p>` operator relations,+* `t =~> t'` is valid if `t` [normalizes to][normalform] `t'`,+* `t =e> t'` is valid if `t` **eta-reduces** to `t'` in a single step. +A `conf` `reduction` of the form `t_1 s_1 t_2 s_2 ... t_n` is similar to the+`eval` `reduction` of the same form, except that `t_n` *does not* have to be+in normal form. +Each `reduction` supports an optional `nfcheck`, which specifically checks+whether the operator is in the requested normal form, in addition to checking+the functionality of the operator. For example, `t =b:w> t'` not only checks+whether `t` can be reduced to `t'` in a single step, but also whether the+result is in weak normal form.++ (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'` 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*. +* `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 +  (\x y -> x y) (\x -> x) b   =*> b  eval ex2:-  (\x y -> x y) (\x -> x) b +  (\x y -> x y) (\x -> x) b   =~> b  eval ex3:-  (\x y -> x y) (\x -> x) (\z -> z) -  =*> (\x -> x) (\z -> z) +  (\x y -> x y) (\x -> x) (\z -> z)+  =*> (\x -> x) (\z -> z)   =b> (\z -> z) ``` -but `elsa` would *not* accept +but `elsa` would *not* accept  ``` eval ex3:-  (\x y -> x y) (\x -> x) (\z -> z) -  =~> (\x -> x) (\z -> z) +  (\x y -> x y) (\x -> x) (\z -> z)+  =~> (\x -> x) (\z -> z)   =b> (\z -> z) ``` 

@@ -1,5 +1,5 @@ name:                elsa-version:             0.2.2.0+version:             0.3.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@@ -31,16 +31,16 @@   Default-Extensions: OverloadedStrings    build-depends:       base >= 4 && < 5,-                       array,-                       mtl,-                       megaparsec >= 7.0.4,-                       ansi-terminal,-                       hashable,-                       unordered-containers,-                       directory,-                       filepath,-                       dequeue,-                       json+                       array >= 0.5.8 && < 1,+                       mtl >= 2.3.1 && < 3,+                       megaparsec >= 9.7.0 && < 10,+                       ansi-terminal >= 1.1.2 && < 2,+                       hashable >= 1.5.0 && < 2,+                       unordered-containers >= 0.2.20 && < 1,+                       directory >= 1.3.9 && < 2,+                       filepath >= 1.5.4 && < 2,+                       dequeue >= 0.1.12 && < 1,+                       json >= 0.11 && < 1    hs-source-dirs:      src   default-language:    Haskell2010

@@ -1,4 +1,4 @@-{-# LANGUAGE OverloadedStrings, BangPatterns #-}+{-# LANGUAGE OverloadedStrings, BangPatterns, ScopedTypeVariables #-}  module Language.Elsa.Eval (elsa, elsaOn) where @@ -7,9 +7,11 @@ import qualified Data.HashSet         as S import qualified Data.List            as L import           Control.Monad.State+import           Control.Monad        (foldM) import qualified Data.Maybe           as Mb -- (isJust, maybeToList) import           Language.Elsa.Types import           Language.Elsa.Utils  (qPushes, qInit, qPop, fromEither)+import Data.List (group)  -------------------------------------------------------------------------------- elsa :: Elsa a -> [Result a]@@ -32,7 +34,7 @@ checkDupEval = foldM addEvalId S.empty  addEvalId :: S.HashSet Id -> Eval a -> CheckM a (S.HashSet Id)-addEvalId s e = +addEvalId s e =   if S.member (bindId b) s     then Left  (errDupEval b)     else Right (S.insert (bindId b) s)@@ -46,8 +48,8 @@ mkEnv = foldM expand M.empty  expand :: Env a -> Defn a -> CheckM a (Env a)-expand g (Defn b e) = -  if dupId +expand g (Defn b e) =+  if dupId     then Left (errDupDefn b)     else case zs of       (x,l) : _ -> Left  (Unbound b x l)@@ -65,12 +67,17 @@ -------------------------------------------------------------------------------- eval :: Env a -> Eval a -> CheckM a (Result a) ---------------------------------------------------------------------------------eval g (Eval n e steps) = go e steps+eval g (Eval kind 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)+      | noCheck kind || isNormal g e = return (OK n)+      | otherwise                    = Left (errPartial n e)+    go e (s:steps)                   = step g n e s >>= (`go` steps)+    -- Regular is just "eval", then there is always a strong normal form check+    -- at the end+    noCheck Regular = False+    -- Similar to "Regular" but without a strong normal form check at the end+    noCheck Conf    = True  step :: Env a -> Bind a -> Expr a -> Step a -> CheckM a (Expr a) step g n e (Step k e')@@ -78,23 +85,37 @@   | otherwise     = Left (errInvalid n e k e')  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-+isEq (Eqn op chk _) =+  case op of+    EqAlpha          -> isAlphEq chk+    EqBeta           -> isBetaEq chk+    EqEta            -> isEtaaEq chk+    EqDefn           -> isDefnEq chk+    EqNormOrd        -> isNBetaEq chk+    EqAppOrd         -> isABetaEq chk+    EqTrans          -> isTrnsEq chk+    EqNormTrans      -> toNormEq --chk unnecessary+    EqNormOrdTrans   -> isNTrnsEq chk+    EqAppOrdTrans    -> isATrnsEq chk+    EqUnBeta         -> isUnBeta+    EqUnEta          -> isUnEtaa+    EqUnNormOrd      -> isUnNBeta+    EqUnAppOrd       -> isUnABeta+    EqUnTrans        -> isUnTrEq+    EqUnNormOrdTrans -> isUnNTrEq+    EqUnAppOrdTrans  -> isUnATrEq  -------------------------------------------------------------------------------- -- | Transitive Reachability ---------------------------------------------------------------------------------isTrnsEq :: Env a -> Expr a -> Expr a -> Bool-isTrnsEq g e1 e2 = Mb.isJust (findTrans (isEquiv g e2) (canon g e1))+isTrnsEq :: Maybe NormCheck -> Env a -> Expr a -> Expr a -> Bool+isTrnsEq Nothing g e1 e2 = Mb.isJust (findTrans (isEquiv g e2) (canon g e1))+isTrnsEq (Just Strong) g e1 e2 = isTnsSEq isNormEq g e1 e2+isTrnsEq (Just Weak) g e1 e2 = isTnsSEq isWnfEq g e1 e2+isTrnsEq (Just Head) g e1 e2 = isTnsSEq isHnfEq g e1 e2  isUnTrEq :: Env a -> Expr a -> Expr a -> Bool-isUnTrEq g e1 e2 = isTrnsEq g e2 e1+isUnTrEq g e1 e2 = isTrnsEq Nothing g e2 e1  findTrans :: (Expr a -> Bool) -> Expr a -> Maybe (Expr a) findTrans p e = go S.empty (qInit e)@@ -107,18 +128,74 @@              then return e              else go (S.insert e seen) (qPushes q (betas e)) +-- findTrans with selected normal form check+isTnsSEq :: (Env a -> Expr a -> Expr a -> Bool) -> Env a -> Expr a -> Expr a -> Bool+isTnsSEq isNfEq g e1 e2 = maybe False (flip (isNfEq g) e2) (findTrans (isEquiv g e2) (canon g e1))++-- Multiple normal order beta, alpha reductions and/or definitions+isNTrnsEq :: Maybe NormCheck -> Env a -> Expr a -> Expr a -> Bool+isNTrnsEq Nothing = isSTrnsEq norStep+isNTrnsEq (Just Strong) = isSTrnsSEq norStep isNormEq+isNTrnsEq (Just Weak) = isSTrnsSEq norStep isWnfEq+isNTrnsEq (Just Head) = isSTrnsSEq norStep isHnfEq++isUnNTrEq :: Env a -> Expr a -> Expr a -> Bool+isUnNTrEq g e1 e2 = isNTrnsEq Nothing g e2 e1++-- Multiple applicative order beta, alpha reductions and/or definitions+isATrnsEq :: Maybe NormCheck -> Env a -> Expr a -> Expr a -> Bool+isATrnsEq Nothing = isSTrnsEq appStep+isATrnsEq (Just Strong) = isSTrnsSEq appStep isNormEq+isATrnsEq (Just Weak) = isSTrnsSEq appStep isWnfEq+isATrnsEq (Just Head) = isSTrnsSEq appStep isHnfEq++isUnATrEq :: Env a -> Expr a -> Expr a -> Bool+isUnATrEq g e1 e2 = isATrnsEq Nothing g e2 e1++-- Multiple beta, alpha reductions and/or definitions, using selected strategy+isSTrnsEq :: forall a. (Expr a -> Maybe (Expr a)) -> Env a -> Expr a -> Expr a -> Bool+isSTrnsEq step g e1 e2 = Mb.isJust (findSTrans step (isEquiv g e2) (canon g e1))++findSTrans :: (Expr a -> Maybe (Expr a)) -> (Expr a -> Bool) -> Expr a -> Maybe (Expr a)+findSTrans step f e = do+  if f e then -- Maybe no reductions are needed+    return e+  else do -- One or more reductions are needed+    e' <- step e+    if f e' then+      return e'+    else+      findSTrans step f e'++-- isSTrnsEq with selected normal form check+isSTrnsSEq :: (Expr a -> Maybe (Expr a)) -> (Env a -> Expr a -> Expr a -> Bool) -> Env a -> Expr a -> Expr a -> Bool+isSTrnsSEq step isNfEq g e1 e2 =+  case findSTrans step (isEquiv g e2) (canon g e1) of+    Nothing -> False+    Just e1' -> isNfEq g e1' e2+ -------------------------------------------------------------------------------- -- | Definition Equivalence ---------------------------------------------------------------------------------isDefnEq :: Env a -> Expr a -> Expr a -> Bool-isDefnEq g e1 e2 = subst e1 g == subst e2 g+isDefnEq :: Maybe NormCheck -> Env a -> Expr a -> Expr a -> Bool+isDefnEq Nothing g e1 e2 = subst e1 g == subst e2 g+isDefnEq (Just Strong) g e1 e2 = isNormEq g e1 e2+isDefnEq (Just Weak) g e1 e2 = isWnfEq g e1 e2+isDefnEq (Just Head) g e1 e2 = isHnfEq g e1 e2  -------------------------------------------------------------------------------- -- | Alpha Equivalence ---------------------------------------------------------------------------------isAlphEq :: Env a -> Expr a -> Expr a -> Bool-isAlphEq _ e1 e2 = alphaNormal e1 == alphaNormal e2+isAlphEq :: Maybe NormCheck -> Env a -> Expr a -> Expr a -> Bool+isAlphEq Nothing _ e1 e2 = alphaNormal e1 == alphaNormal e2+isAlphEq (Just Strong) g e1 e2 = isAlphPEq isNormEq g e1 e2+isAlphEq (Just Weak) g e1 e2 = isAlphPEq isWnfEq g e1 e2+isAlphEq (Just Head) g e1 e2 = isAlphPEq isHnfEq g e1 e2 +-- Alpha Equivalence with provided normal form check+isAlphPEq :: (Env a -> Expr a -> Expr a -> Bool) -> Env a -> Expr a -> Expr a -> Bool+isAlphPEq isNfEq g e1 e2 = (alphaNormal e1 == alphaNormal e2) && isNfEq g e1 e2+ alphaNormal :: Expr a -> Expr a alphaNormal = alphaShift 0 @@ -165,12 +242,77 @@ -------------------------------------------------------------------------------- -- | Beta Reduction ---------------------------------------------------------------------------------isBetaEq :: Env a -> Expr a -> Expr a -> Bool-isBetaEq _ e1 e2 = or [ e1' == e2  | e1' <- betas e1 ]+-- Beta reduction, without any normal form check+isBetaEq :: Maybe NormCheck -> Env a -> Expr a -> Expr a -> Bool+isBetaEq Nothing _ e1 e2 = or [ e1' == e2  | e1' <- betas e1 ]+isBetaEq (Just Strong) g e1 e2 = isBetaPEq isNormEq g e1 e2+isBetaEq (Just Weak) g e1 e2 = isBetaPEq isWnfEq g e1 e2+isBetaEq (Just Head) g e1 e2 = isBetaPEq isHnfEq g e1 e2  isUnBeta :: Env a -> Expr a -> Expr a -> Bool-isUnBeta g e1 e2 = isBetaEq g e2 e1+isUnBeta g e1 e2 = isBetaEq Nothing g e2 e1 +-- Beta reduction, with provided normal form check+isBetaPEq :: (Env a -> Expr a -> Expr a -> Bool) -> Env a -> Expr a -> Expr a -> Bool+isBetaPEq isNfEq g e1 e2 = or [ isNfEq g e1' e2  | e1' <- betas e1 ]++-- Use normal order evaluation strategy+isNBetaEq :: Maybe NormCheck -> Env a -> Expr a -> Expr a -> Bool+isNBetaEq = isSBetaEq norStep++isUnNBeta :: Env a -> Expr a -> Expr a -> Bool+isUnNBeta g e1 e2 = isNBetaEq Nothing g e2 e1++-- Use applicative order evaluation strategy+isABetaEq :: Maybe NormCheck -> Env a -> Expr a -> Expr a -> Bool+isABetaEq = isSBetaEq appStep++isUnABeta :: Env a -> Expr a -> Expr a -> Bool+isUnABeta g e1 e2 = isABetaEq Nothing g e2 e1++-- Use selected order evaluation strategy+isSBetaEq :: (Expr a -> Maybe (Expr a)) -> Maybe NormCheck -> Env a -> Expr a -> Expr a -> Bool+isSBetaEq step Nothing g e1 e2 = step (subst e1 g) == Just (subst e2 g)+isSBetaEq step (Just Strong) g e1 e2 = case step (subst e1 g) of+  Nothing -> False+  Just e1' -> isNormEq g e1' e2+isSBetaEq step (Just Weak) g e1 e2 = case step (subst e1 g) of+  Nothing -> False+  Just e1' -> isWnfEq g e1' e2+isSBetaEq step (Just Head) g e1 e2 = case step (subst e1 g) of+  Nothing -> False+  Just e1' -> isHnfEq g e1' e2++-- norStep is a single normal order reduction+norStep :: Expr a -> Maybe (Expr a)+norStep (EVar {}) = Nothing+norStep (ELam b e l) = do+  e' <- norStep e+  return $ ELam b e' l+norStep (EApp e1@(ELam {}) e2 _) = beta e1 e2+norStep (EApp e1 e2 l) = case norStep e1 of+  Just e1' -> return $ EApp e1' e2 l+  Nothing -> case norStep e2 of+    Just e2' -> return $ EApp e1 e2' l+    Nothing -> Nothing++-- appStep is a single applicative order reduction+appStep :: Expr a -> Maybe (Expr a)+appStep (EVar {}) = Nothing+appStep (ELam b e l) = do+  e' <- appStep e+  return $ ELam b e' l+appStep (EApp e1@(ELam {}) e2 l) = case appStep e1 of+  Just e1' -> Just $ EApp e1' e2 l+  Nothing -> case appStep e2 of+    Just e2' -> Just $ EApp e1 e2' l+    Nothing -> beta e1 e2+appStep (EApp e1 e2 l) = case appStep e1 of+  Just e1' -> return $ EApp e1' e2 l+  Nothing -> case appStep e2 of+    Just e2' -> return $ EApp e1 e2' l+    Nothing -> Nothing+ isNormal :: Env a -> Expr a -> Bool isNormal g = null . betas . (`subst` g) @@ -208,30 +350,126 @@ isIn = S.member . bindId  --------------------------------------------------------------------------------+-- | Eta Reduction+--------------------------------------------------------------------------------+-- Eta reduction, without any normal form check+isEtaaEq :: Maybe NormCheck -> Env a -> Expr a -> Expr a -> Bool+isEtaaEq Nothing g e1 e2 = go e1 (subst e2 g)+  where+    go e1 e2' = or [e1' == e2' | e1' <- etas g e1]+isEtaaEq (Just Strong) g e1 e2 = isEtaPEq isNormEq g e1 e2+isEtaaEq (Just Weak) g e1 e2 = isEtaPEq isWnfEq g e1 e2+isEtaaEq (Just Head) g e1 e2 = isEtaPEq isHnfEq g e1 e2++isUnEtaa :: Env a -> Expr a -> Expr a -> Bool+isUnEtaa g e1 e2 = isEtaaEq Nothing g e2 e1++-- Eta reduction, with provided normal form check+isEtaPEq :: (Env a -> Expr a -> Expr a -> Bool) -> Env a -> Expr a -> Expr a -> Bool+isEtaPEq isNfEq g e1 e2 = or [isNfEq g e1' e2 | e1' <- etas g e1]++-- Search for an eta reduction.+-- Returns the reduced formula if one can be found,+-- returns Nothing if no reductions are possible+eta :: Expr a -> Maybe (Expr a)+eta (ELam x (EApp e (EVar x' _) _) _) =+  let zs = freeVars e in+  if (bindId x == x') && not (isIn x zs)+    then+      Just e+    else Nothing+eta _ = Nothing++etas :: Env a -> Expr a -> [Expr a]+etas g e = go (subst e g)+  where+    go (EVar {})        = []+    -- Pattern where reduction might be possible+    go e'@(ELam b e1 z) = Mb.maybeToList (eta e')+                       ++ [ELam b e1' z | e1' <- go e1]+    go (EApp e1 e2 z)   = [EApp e1' e2 z | e1' <- go e1]+                       ++ [EApp e1 e2' z | e2' <- go e2]++-------------------------------------------------------------------------------- -- | Evaluation to Normal Form --------------------------------------------------------------------------------+-- Check if e1 is strong normal form isNormEq :: Env a -> Expr a -> Expr a -> Bool-isNormEq g e1 e2 = eqVal (subst e2 g) $ evalNbE ML.empty (subst e1 g)+isNormEq g e1 e2 = (e1' == e2') && nEqVal e2' (nf e2')   where-    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)+    e1' = alphaNormal $ subst e1 g+    e2' = alphaNormal $ subst e2 g+    nf = evalNbE ML.empty -    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+toNormEq :: Env a -> Expr a -> Expr a -> Bool+toNormEq g e1 e2 = nEqVal (subst e2 g) $ evalNbE ML.empty (subst e1 g) +evalNbE :: ML.HashMap Id Value -> Expr a -> Value+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)++nEqVal :: Expr a -> Value -> Bool+nEqVal (EVar x _) (Neutral x' [])+  = x == x'+nEqVal (ELam (Bind x _) b _) (Fun f)+  = nEqVal b (f (Neutral x []))+nEqVal (EApp f a _) (Neutral x (a':args))+  = nEqVal a a' && nEqVal f (Neutral x args)+nEqVal _ _ = False+ -- | NbE semantic domain data Value = Fun !(Value -> Value) | Neutral !Id ![Value]  --------------------------------------------------------------------------------+-- | Evaluation to Weak Normal Form+--------------------------------------------------------------------------------+isWnfEq :: Env a -> Expr a -> Expr a -> Bool+isWnfEq g e1 e2 = (e1' == e2') && (e2' == wnf e2')+  where+    e1' = alphaNormal $ subst e1 g+    e2' = alphaNormal $ subst e2 g+    wnf :: Expr a -> Expr a+    wnf e@(EVar {}) = e+    wnf e@(ELam {}) = e+    wnf (EApp f arg l) = case wnf f of+      f'@ELam {} -> maybe (EApp f' (wnf arg) l) wnf (beta f $ wnf arg)+      f' -> EApp f' (wnf arg) l++--------------------------------------------------------------------------------+-- | Evaluation to Head Normal Form+--------------------------------------------------------------------------------+isHnfEq :: Env a -> Expr a -> Expr a -> Bool+isHnfEq g e1 e2 = (e1' == e2') && (e2' == hnf e2')+  where+    e1' = alphaNormal $ subst e1 g+    e2' = alphaNormal $ subst e2 g+    hnf :: Expr a -> Expr a+    hnf e@(EVar {}) = e+    hnf (ELam bi b a) = ELam bi (hnf b) a+    hnf (EApp f arg l) = case hnf f of+      f'@ELam {} -> maybe (EApp f' (hnf arg) l) hnf (beta f' arg)+      f' -> EApp f' arg l++--------------------------------------------------------------------------------+-- | Evaluation to Weak Head Normal Form+--------------------------------------------------------------------------------+{- isWhnfEq :: Env a -> Expr a -> Expr a -> Bool+isWhnfEq g e1 e2 = (e1' == e2') && (e2' == whnf e2')+  where+    e1' = subst e1 g+    e2' = subst e2 g+    whnf :: Expr a -> Expr a+    whnf e@(EVar {}) = e+    whnf e@(ELam {}) = e+    whnf (EApp f arg l) = case whnf f of+      f'@ELam {} -> maybe (EApp f' arg l) whnf (beta f arg)+      f' -> EApp f' arg l -}++-------------------------------------------------------------------------------- -- | General Helpers -------------------------------------------------------------------------------- freeVars :: Expr a -> S.HashSet Id@@ -253,7 +491,7 @@ 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)+isEquiv g e1 e2 = isAlphEq Nothing g (subst e1 g) (subst e2 g) -------------------------------------------------------------------------------- -- | Error Cases --------------------------------------------------------------------------------

@@ -103,7 +103,7 @@  -- | list of reserved words keywords :: [Text]-keywords = [ "let"  , "eval" ]+keywords = [ "let"  , "eval"  , "conf" ]  -- | `identifier` parses identifiers: lower-case alphabets followed by alphas or digits identifier :: Parser (String, SourceSpan)@@ -140,8 +140,18 @@ -------------------------------------------------------------------------------- -------------------------------------------------------------------------------- elsa :: Parser SElsa-elsa = Elsa <$> many defn <*> many eval+elsa = do+  items <- many elsaItem+  pure $+    Elsa+      { defns = [d | DefnItem d <- items],+        evals = [e | EvalItem e <- items]+      } +elsaItem :: Parser SElsaItem+elsaItem = +  (DefnItem <$> defn) <|> (EvalItem <$> eval)+ defn :: Parser SDefn defn = do   rWord "let"@@ -151,24 +161,63 @@  eval :: Parser SEval eval = do-  rWord "eval"+  kind <- (rWord "eval" >> return Regular) <|> (rWord "conf" >> return Conf)   name  <- binder   colon   root  <- expr   steps <- many step-  return $ Eval name root steps+  return $ Eval kind 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))-   <|> 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))+eqn = withSpan' parseEqn++parseEqn :: Parser (SourceSpan -> Eqn SourceSpan)+parseEqn = try parseUnEqn <|> parseRegEqn++parseUnEqn :: Parser (SourceSpan -> Eqn SourceSpan)+parseUnEqn = do+  void $ char '<'+  op <- choice+    [ try (symbol "n*=") >> return EqUnNormOrdTrans+    , try (symbol "p*=") >> return EqUnAppOrdTrans+    , try (symbol "b=")  >> return EqUnBeta+    , try (symbol "n=") >> return EqUnNormOrd+    , try (symbol "p=") >> return EqUnAppOrd+    , try (symbol "e=")  >> return EqUnEta+    , try (symbol "*=")  >> return EqUnTrans+    ]+  return $ \sp -> Eqn op Nothing sp++parseRegEqn :: Parser (SourceSpan -> Eqn SourceSpan)+parseRegEqn = do+  void $ char '='+  op <- choice+    [ try (string "n*") >> return EqNormOrdTrans+    , try (string "p*") >> return EqAppOrdTrans+    , try (string "n") >> return EqNormOrd+    , try (string "p") >> return EqAppOrd+    , try (string "a")  >> return EqAlpha+    , try (string "b")  >> return EqBeta+    , try (string "e")  >> return EqEta+    , try (string "d")  >> return EqDefn+    , try (string "*")  >> return EqTrans+    , try (string "~")  >> return EqNormTrans+    ]+  mChk <- optional parseNormCheck+  void $ symbol ">"+  return $ \sp -> Eqn op mChk sp++parseNormCheck :: Parser NormCheck+parseNormCheck = do+  void $ char ':'+  choice+    [ char 's' >> return Strong+    , char 'w' >> return Weak+    , char 'h' >> return Head+    ]  expr :: Parser SExpr expr =  try lamExpr

@@ -2,6 +2,7 @@ {-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE DeriveGeneric     #-} {-# LANGUAGE DeriveFunctor     #-}+{-# LANGUAGE InstanceSigs #-}  module Language.Elsa.Types where @@ -11,15 +12,16 @@ import           Data.Maybe (mapMaybe) 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+type Id        = String+type SElsaItem = ElsaItem SourceSpan+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@@ -64,6 +66,8 @@ -------------------------------------------------------------------------------- -- | Programs --------------------------------------------------------------------------------+data ElsaItem a = DefnItem (Defn a) | EvalItem (Eval a)+ data Elsa a = Elsa   { defns :: [Defn a]   , evals :: [Eval a]@@ -74,27 +78,53 @@   = Defn !(Bind a) !(Expr a)   deriving (Eq, Show) +data EvalKind = Regular | Conf deriving (Eq, Show)+ data Eval a = Eval-  { evName  :: !(Bind a)+  { evKind  :: EvalKind+  , evName  :: !(Bind a)   , evRoot  :: !(Expr a)   , evSteps :: [Step a]-  }-  deriving (Eq, Show)+  } deriving (Eq, Show)  data Step a   = Step !(Eqn a) !(Expr a)   deriving (Eq, Show) -data Eqn a-  = AlphEq a-  | BetaEq a-  | UnBeta a-  | DefnEq a-  | TrnsEq a-  | UnTrEq a-  | NormEq a+{-+  EqAlpha         : Alpha equivalence+  EqBeta          : Beta reduction+  EqEta           : Eta reduction+  EqDefn          : Definition unpacking+  EqNormOrd       : Normal order beta reduction+  EqAppOrd        : Applicative order beta reduction+  EqNormOrdTrans  : Normal order beta reduction with alpha equivalence and definition unpacking+  EqAppOrdTrans   : Applicative order beta reduction with alpha equivalence and definition unpacking+  EqTrans         : Zero or more beta reductions with alpha equivalence and definition unpacking+  EqNormTrans     : Acts the same as the "=n*:s>" operator, no matter the normal form check+  EqUnBeta        : Backwards beta reduction+  EqUnEta         : Backwards eta reduction+  EqUnNormOrd     : Backwards normal order beta reduction+  EqUnAppOrd      : Backwards applicative order beta reduction+  EqUnTrans       : Backwards zero or more beta reductions with alpha equivalence and definition unpacking+  EqUnNormOrdTrans: Backwards normal order beta reduction with alpha equivalence and definition unpacking+  EqUnAppOrdTrans : Backwards applicative order beta reduction with alpha equivalence and definition unpacking+-}+data EqnOp+  = EqAlpha | EqBeta | EqEta | EqDefn+  | EqNormOrd | EqAppOrd | EqTrans+  | EqNormOrdTrans | EqAppOrdTrans+  | EqNormTrans+  | EqUnBeta | EqUnEta | EqUnNormOrd+  | EqUnAppOrd | EqUnTrans+  | EqUnNormOrdTrans | EqUnAppOrdTrans   deriving (Eq, Show) +-- Strong, weak, or head normal form check+data NormCheck = Strong | Weak | Head deriving (Eq, Show)++data Eqn a = Eqn EqnOp (Maybe NormCheck) a deriving (Eq, Show)+ data Bind a   = Bind Id a   deriving (Show, Functor)@@ -172,13 +202,7 @@   tag :: t a -> a  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+  tag (Eqn _ _ x) = x  instance Tagged Bind where   tag (Bind _   x) = x