{-# LANGUAGE OverloadedStrings, BangPatterns, ScopedTypeVariables #-}

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           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]
--------------------------------------------------------------------------------
elsa :: forall a. Elsa a -> [Result a]
elsa = (Id -> Bool) -> Elsa a -> [Result a]
forall a. (Id -> Bool) -> Elsa a -> [Result a]
elsaOn (Bool -> Id -> Bool
forall a b. a -> b -> a
const Bool
True)

--------------------------------------------------------------------------------
elsaOn :: (Id -> Bool) -> Elsa a -> [Result a]
--------------------------------------------------------------------------------
elsaOn :: forall a. (Id -> Bool) -> Elsa a -> [Result a]
elsaOn Id -> Bool
cond Elsa a
p =
  case [Defn a] -> CheckM a (Env a)
forall a. [Defn a] -> CheckM a (Env a)
mkEnv (Elsa a -> [Defn a]
forall a. Elsa a -> [Defn a]
defns Elsa a
p) of
    Left Result a
err -> [Result a
err]
    Right Env a
g  -> case [Eval a] -> CheckM a (HashSet Id)
forall a. [Eval a] -> CheckM a (HashSet Id)
checkDupEval (Elsa a -> [Eval a]
forall a. Elsa a -> [Eval a]
evals Elsa a
p) of
      Left Result a
err -> [Result a
err]
      Right HashSet Id
_  -> [Env a -> Eval a -> Result a
forall a. Env a -> Eval a -> Result a
result Env a
g Eval a
e | Eval a
e <- Elsa a -> [Eval a]
forall a. Elsa a -> [Eval a]
evals Elsa a
p, Eval a -> Bool
forall {a}. Eval a -> Bool
check Eval a
e ]
  where
    check :: Eval a -> Bool
check = Id -> Bool
cond (Id -> Bool) -> (Eval a -> Id) -> Eval a -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Bind a -> Id
forall a. Bind a -> Id
bindId (Bind a -> Id) -> (Eval a -> Bind a) -> Eval a -> Id
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Eval a -> Bind a
forall a. Eval a -> Bind a
evName

checkDupEval :: [Eval a] -> CheckM a (S.HashSet Id)
checkDupEval :: forall a. [Eval a] -> CheckM a (HashSet Id)
checkDupEval = (HashSet Id -> Eval a -> Either (Result a) (HashSet Id))
-> HashSet Id -> [Eval a] -> Either (Result a) (HashSet Id)
forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldM HashSet Id -> Eval a -> Either (Result a) (HashSet Id)
forall a. HashSet Id -> Eval a -> CheckM a (HashSet Id)
addEvalId HashSet Id
forall a. HashSet a
S.empty

addEvalId :: S.HashSet Id -> Eval a -> CheckM a (S.HashSet Id)
addEvalId :: forall a. HashSet Id -> Eval a -> CheckM a (HashSet Id)
addEvalId HashSet Id
s Eval a
e =
  if Id -> HashSet Id -> Bool
forall a. (Eq a, Hashable a) => a -> HashSet a -> Bool
S.member (Bind a -> Id
forall a. Bind a -> Id
bindId Bind a
b) HashSet Id
s
    then Result a -> Either (Result a) (HashSet Id)
forall a b. a -> Either a b
Left  (Bind a -> Result a
forall a. Bind a -> Result a
errDupEval Bind a
b)
    else HashSet Id -> Either (Result a) (HashSet Id)
forall a b. b -> Either a b
Right (Id -> HashSet Id -> HashSet Id
forall a. (Eq a, Hashable a) => a -> HashSet a -> HashSet a
S.insert (Bind a -> Id
forall a. Bind a -> Id
bindId Bind a
b) HashSet Id
s)
  where
    b :: Bind a
b = Eval a -> Bind a
forall a. Eval a -> Bind a
evName Eval a
e

result :: Env a -> Eval a -> Result a
result :: forall a. Env a -> Eval a -> Result a
result Env a
g Eval a
e = Either (Result a) (Result a) -> Result a
forall a. Either a a -> a
fromEither (Env a -> Eval a -> Either (Result a) (Result a)
forall a. Env a -> Eval a -> CheckM a (Result a)
eval Env a
g Eval a
e)

mkEnv :: [Defn a] -> CheckM a (Env a)
mkEnv :: forall a. [Defn a] -> CheckM a (Env a)
mkEnv = (Env a -> Defn a -> Either (Result a) (Env a))
-> Env a -> [Defn a] -> Either (Result a) (Env a)
forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldM Env a -> Defn a -> Either (Result a) (Env a)
forall a. Env a -> Defn a -> CheckM a (Env a)
expand Env a
forall k v. HashMap k v
M.empty

expand :: Env a -> Defn a -> CheckM a (Env a)
expand :: forall a. Env a -> Defn a -> CheckM a (Env a)
expand Env a
g (Defn Bind a
b Expr a
e) =
  if Bool
dupId
    then Result a -> CheckM a (Env a)
forall a b. a -> Either a b
Left (Bind a -> Result a
forall a. Bind a -> Result a
errDupDefn Bind a
b)
    else case [(Id, a)]
zs of
      (Id
x,a
l) : [(Id, a)]
_ -> Result a -> CheckM a (Env a)
forall a b. a -> Either a b
Left  (Bind a -> Id -> a -> Result a
forall a. Bind a -> Id -> a -> Result a
Unbound Bind a
b Id
x a
l)
      []        -> Env a -> CheckM a (Env a)
forall a b. b -> Either a b
Right (Id -> Expr a -> Env a -> Env a
forall k v.
(Eq k, Hashable k) =>
k -> v -> HashMap k v -> HashMap k v
M.insert (Bind a -> Id
forall a. Bind a -> Id
bindId Bind a
b) Expr a
e' Env a
g)
  where
    dupId :: Bool
dupId           = Id -> Env a -> Bool
forall k a. (Eq k, Hashable k) => k -> HashMap k a -> Bool
M.member (Bind a -> Id
forall a. Bind a -> Id
bindId Bind a
b) Env a
g
    e' :: Expr a
e'              = Expr a -> Env a -> Expr a
forall a. Expr a -> Env a -> Expr a
subst Expr a
e Env a
g
    zs :: [(Id, a)]
zs              = HashMap Id a -> [(Id, a)]
forall k v. HashMap k v -> [(k, v)]
M.toList (Expr a -> HashMap Id a
forall a. Expr a -> HashMap Id a
freeVars' Expr a
e')

--------------------------------------------------------------------------------
type CheckM a b = Either (Result a) b
type Env a      = M.HashMap Id (Expr a)
--------------------------------------------------------------------------------

--------------------------------------------------------------------------------
eval :: Env a -> Eval a -> CheckM a (Result a)
--------------------------------------------------------------------------------
eval :: forall a. Env a -> Eval a -> CheckM a (Result a)
eval Env a
g (Eval EvalKind
kind Bind a
n Expr a
e [Step a]
steps) = Expr a -> [Step a] -> Either (Result a) (Result a)
go Expr a
e [Step a]
steps
  where
    go :: Expr a -> [Step a] -> Either (Result a) (Result a)
go Expr a
e []
      | EvalKind -> Bool
noCheck EvalKind
kind Bool -> Bool -> Bool
|| Env a -> Expr a -> Bool
forall a. Env a -> Expr a -> Bool
isNormal Env a
g Expr a
e = Result a -> Either (Result a) (Result a)
forall a. a -> Either (Result a) a
forall (m :: * -> *) a. Monad m => a -> m a
return (Bind a -> Result a
forall a. Bind a -> Result a
OK Bind a
n)
      | Bool
otherwise                    = Result a -> Either (Result a) (Result a)
forall a b. a -> Either a b
Left (Bind a -> Expr a -> Result a
forall a. Bind a -> Expr a -> Result a
errPartial Bind a
n Expr a
e)
    go Expr a
e (Step a
s:[Step a]
steps)                   = Env a -> Bind a -> Expr a -> Step a -> CheckM a (Expr a)
forall a. Env a -> Bind a -> Expr a -> Step a -> CheckM a (Expr a)
step Env a
g Bind a
n Expr a
e Step a
s CheckM a (Expr a)
-> (Expr a -> Either (Result a) (Result a))
-> Either (Result a) (Result a)
forall a b.
Either (Result a) a
-> (a -> Either (Result a) b) -> Either (Result a) b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= (Expr a -> [Step a] -> Either (Result a) (Result a)
`go` [Step a]
steps)
    -- Regular is just "eval", then there is always a strong normal form check
    -- at the end
    noCheck :: EvalKind -> Bool
noCheck EvalKind
Regular = Bool
False
    -- Similar to "Regular" but without a strong normal form check at the end
    noCheck EvalKind
Conf    = Bool
True

step :: Env a -> Bind a -> Expr a -> Step a -> CheckM a (Expr a)
step :: forall a. Env a -> Bind a -> Expr a -> Step a -> CheckM a (Expr a)
step Env a
g Bind a
n Expr a
e (Step Eqn a
k Expr a
e')
  | Eqn a -> Env a -> Expr a -> Expr a -> Bool
forall a. Eqn a -> Env a -> Expr a -> Expr a -> Bool
isEq Eqn a
k Env a
g Expr a
e Expr a
e' = Expr a -> Either (Result a) (Expr a)
forall a. a -> Either (Result a) a
forall (m :: * -> *) a. Monad m => a -> m a
return Expr a
e'
  | Bool
otherwise     = Result a -> Either (Result a) (Expr a)
forall a b. a -> Either a b
Left (Bind a -> Expr a -> Eqn a -> Expr a -> Result a
forall a. Bind a -> Expr a -> Eqn a -> Expr a -> Result a
errInvalid Bind a
n Expr a
e Eqn a
k Expr a
e')

isEq :: Eqn a -> Env a -> Expr a -> Expr a -> Bool
isEq :: forall a. Eqn a -> Env a -> Expr a -> Expr a -> Bool
isEq (Eqn EqnOp
op Maybe NormCheck
chk a
_) =
  case EqnOp
op of
    EqnOp
EqAlpha          -> Maybe NormCheck -> Env a -> Expr a -> Expr a -> Bool
forall a. Maybe NormCheck -> Env a -> Expr a -> Expr a -> Bool
isAlphEq Maybe NormCheck
chk
    EqnOp
EqBeta           -> Maybe NormCheck -> Env a -> Expr a -> Expr a -> Bool
forall a. Maybe NormCheck -> Env a -> Expr a -> Expr a -> Bool
isBetaEq Maybe NormCheck
chk
    EqnOp
EqEta            -> Maybe NormCheck -> Env a -> Expr a -> Expr a -> Bool
forall a. Maybe NormCheck -> Env a -> Expr a -> Expr a -> Bool
isEtaaEq Maybe NormCheck
chk
    EqnOp
EqDefn           -> Maybe NormCheck -> Env a -> Expr a -> Expr a -> Bool
forall a. Maybe NormCheck -> Env a -> Expr a -> Expr a -> Bool
isDefnEq Maybe NormCheck
chk
    EqnOp
EqNormOrd        -> Maybe NormCheck -> Env a -> Expr a -> Expr a -> Bool
forall a. Maybe NormCheck -> Env a -> Expr a -> Expr a -> Bool
isNBetaEq Maybe NormCheck
chk
    EqnOp
EqAppOrd         -> Maybe NormCheck -> Env a -> Expr a -> Expr a -> Bool
forall a. Maybe NormCheck -> Env a -> Expr a -> Expr a -> Bool
isABetaEq Maybe NormCheck
chk
    EqnOp
EqTrans          -> Maybe NormCheck -> Env a -> Expr a -> Expr a -> Bool
forall a. Maybe NormCheck -> Env a -> Expr a -> Expr a -> Bool
isTrnsEq Maybe NormCheck
chk
    EqnOp
EqNormTrans      -> Env a -> Expr a -> Expr a -> Bool
forall a. Env a -> Expr a -> Expr a -> Bool
toNormEq --chk unnecessary
    EqnOp
EqNormOrdTrans   -> Maybe NormCheck -> Env a -> Expr a -> Expr a -> Bool
forall a. Maybe NormCheck -> Env a -> Expr a -> Expr a -> Bool
isNTrnsEq Maybe NormCheck
chk
    EqnOp
EqAppOrdTrans    -> Maybe NormCheck -> Env a -> Expr a -> Expr a -> Bool
forall a. Maybe NormCheck -> Env a -> Expr a -> Expr a -> Bool
isATrnsEq Maybe NormCheck
chk
    EqnOp
EqUnBeta         -> Env a -> Expr a -> Expr a -> Bool
forall a. Env a -> Expr a -> Expr a -> Bool
isUnBeta
    EqnOp
EqUnEta          -> Env a -> Expr a -> Expr a -> Bool
forall a. Env a -> Expr a -> Expr a -> Bool
isUnEtaa
    EqnOp
EqUnNormOrd      -> Env a -> Expr a -> Expr a -> Bool
forall a. Env a -> Expr a -> Expr a -> Bool
isUnNBeta
    EqnOp
EqUnAppOrd       -> Env a -> Expr a -> Expr a -> Bool
forall a. Env a -> Expr a -> Expr a -> Bool
isUnABeta
    EqnOp
EqUnTrans        -> Env a -> Expr a -> Expr a -> Bool
forall a. Env a -> Expr a -> Expr a -> Bool
isUnTrEq
    EqnOp
EqUnNormOrdTrans -> Env a -> Expr a -> Expr a -> Bool
forall a. Env a -> Expr a -> Expr a -> Bool
isUnNTrEq
    EqnOp
EqUnAppOrdTrans  -> Env a -> Expr a -> Expr a -> Bool
forall a. Env a -> Expr a -> Expr a -> Bool
isUnATrEq

--------------------------------------------------------------------------------
-- | Transitive Reachability
--------------------------------------------------------------------------------
isTrnsEq :: Maybe NormCheck -> Env a -> Expr a -> Expr a -> Bool
isTrnsEq :: forall a. Maybe NormCheck -> Env a -> Expr a -> Expr a -> Bool
isTrnsEq Maybe NormCheck
Nothing Env a
g Expr a
e1 Expr a
e2 = Maybe (Expr a) -> Bool
forall a. Maybe a -> Bool
Mb.isJust ((Expr a -> Bool) -> Expr a -> Maybe (Expr a)
forall a. (Expr a -> Bool) -> Expr a -> Maybe (Expr a)
findTrans (Env a -> Expr a -> Expr a -> Bool
forall a. Env a -> Expr a -> Expr a -> Bool
isEquiv Env a
g Expr a
e2) (Env a -> Expr a -> Expr a
forall a. Env a -> Expr a -> Expr a
canon Env a
g Expr a
e1))
isTrnsEq (Just NormCheck
Strong) Env a
g Expr a
e1 Expr a
e2 = (Env a -> Expr a -> Expr a -> Bool)
-> Env a -> Expr a -> Expr a -> Bool
forall a.
(Env a -> Expr a -> Expr a -> Bool)
-> Env a -> Expr a -> Expr a -> Bool
isTnsSEq Env a -> Expr a -> Expr a -> Bool
forall a. Env a -> Expr a -> Expr a -> Bool
isNormEq Env a
g Expr a
e1 Expr a
e2
isTrnsEq (Just NormCheck
Weak) Env a
g Expr a
e1 Expr a
e2 = (Env a -> Expr a -> Expr a -> Bool)
-> Env a -> Expr a -> Expr a -> Bool
forall a.
(Env a -> Expr a -> Expr a -> Bool)
-> Env a -> Expr a -> Expr a -> Bool
isTnsSEq Env a -> Expr a -> Expr a -> Bool
forall a. Env a -> Expr a -> Expr a -> Bool
isWnfEq Env a
g Expr a
e1 Expr a
e2
isTrnsEq (Just NormCheck
Head) Env a
g Expr a
e1 Expr a
e2 = (Env a -> Expr a -> Expr a -> Bool)
-> Env a -> Expr a -> Expr a -> Bool
forall a.
(Env a -> Expr a -> Expr a -> Bool)
-> Env a -> Expr a -> Expr a -> Bool
isTnsSEq Env a -> Expr a -> Expr a -> Bool
forall a. Env a -> Expr a -> Expr a -> Bool
isHnfEq Env a
g Expr a
e1 Expr a
e2

isUnTrEq :: Env a -> Expr a -> Expr a -> Bool
isUnTrEq :: forall a. Env a -> Expr a -> Expr a -> Bool
isUnTrEq Env a
g Expr a
e1 Expr a
e2 = Maybe NormCheck -> Env a -> Expr a -> Expr a -> Bool
forall a. Maybe NormCheck -> Env a -> Expr a -> Expr a -> Bool
isTrnsEq Maybe NormCheck
forall a. Maybe a
Nothing Env a
g Expr a
e2 Expr a
e1

findTrans :: (Expr a -> Bool) -> Expr a -> Maybe (Expr a)
findTrans :: forall a. (Expr a -> Bool) -> Expr a -> Maybe (Expr a)
findTrans Expr a -> Bool
p Expr a
e = HashSet (Expr a) -> Queue (Expr a) -> Maybe (Expr a)
go HashSet (Expr a)
forall a. HashSet a
S.empty (Expr a -> Queue (Expr a)
forall a. a -> Queue a
qInit Expr a
e)
  where
    go :: HashSet (Expr a) -> Queue (Expr a) -> Maybe (Expr a)
go HashSet (Expr a)
seen Queue (Expr a)
q = do
      (Expr a
e, Queue (Expr a)
q') <- Queue (Expr a) -> Maybe (Expr a, Queue (Expr a))
forall a. Queue a -> Maybe (a, Queue a)
qPop Queue (Expr a)
q
      if Expr a -> HashSet (Expr a) -> Bool
forall a. (Eq a, Hashable a) => a -> HashSet a -> Bool
S.member Expr a
e HashSet (Expr a)
seen
        then HashSet (Expr a) -> Queue (Expr a) -> Maybe (Expr a)
go HashSet (Expr a)
seen Queue (Expr a)
q'
        else if Expr a -> Bool
p Expr a
e
             then Expr a -> Maybe (Expr a)
forall a. a -> Maybe a
forall (m :: * -> *) a. Monad m => a -> m a
return Expr a
e
             else HashSet (Expr a) -> Queue (Expr a) -> Maybe (Expr a)
go (Expr a -> HashSet (Expr a) -> HashSet (Expr a)
forall a. (Eq a, Hashable a) => a -> HashSet a -> HashSet a
S.insert Expr a
e HashSet (Expr a)
seen) (Queue (Expr a) -> [Expr a] -> Queue (Expr a)
forall a. Queue a -> [a] -> Queue a
qPushes Queue (Expr a)
q (Expr a -> [Expr a]
forall a. Expr a -> [Expr a]
betas Expr a
e))

-- findTrans with selected normal form check
isTnsSEq :: (Env a -> Expr a -> Expr a -> Bool) -> Env a -> Expr a -> Expr a -> Bool
isTnsSEq :: forall a.
(Env a -> Expr a -> Expr a -> Bool)
-> Env a -> Expr a -> Expr a -> Bool
isTnsSEq Env a -> Expr a -> Expr a -> Bool
isNfEq Env a
g Expr a
e1 Expr a
e2 = Bool -> (Expr a -> Bool) -> Maybe (Expr a) -> Bool
forall b a. b -> (a -> b) -> Maybe a -> b
maybe Bool
False ((Expr a -> Expr a -> Bool) -> Expr a -> Expr a -> Bool
forall a b c. (a -> b -> c) -> b -> a -> c
flip (Env a -> Expr a -> Expr a -> Bool
isNfEq Env a
g) Expr a
e2) ((Expr a -> Bool) -> Expr a -> Maybe (Expr a)
forall a. (Expr a -> Bool) -> Expr a -> Maybe (Expr a)
findTrans (Env a -> Expr a -> Expr a -> Bool
forall a. Env a -> Expr a -> Expr a -> Bool
isEquiv Env a
g Expr a
e2) (Env a -> Expr a -> Expr a
forall a. Env a -> Expr a -> Expr a
canon Env a
g Expr a
e1))

-- Multiple normal order beta, alpha reductions and/or definitions
isNTrnsEq :: Maybe NormCheck -> Env a -> Expr a -> Expr a -> Bool
isNTrnsEq :: forall a. Maybe NormCheck -> Env a -> Expr a -> Expr a -> Bool
isNTrnsEq Maybe NormCheck
Nothing = (Expr a -> Maybe (Expr a)) -> Env a -> Expr a -> Expr a -> Bool
forall a.
(Expr a -> Maybe (Expr a)) -> Env a -> Expr a -> Expr a -> Bool
isSTrnsEq Expr a -> Maybe (Expr a)
forall a. Expr a -> Maybe (Expr a)
norStep
isNTrnsEq (Just NormCheck
Strong) = (Expr a -> Maybe (Expr a))
-> (Env a -> Expr a -> Expr a -> Bool)
-> Env a
-> Expr a
-> Expr a
-> Bool
forall a.
(Expr a -> Maybe (Expr a))
-> (Env a -> Expr a -> Expr a -> Bool)
-> Env a
-> Expr a
-> Expr a
-> Bool
isSTrnsSEq Expr a -> Maybe (Expr a)
forall a. Expr a -> Maybe (Expr a)
norStep Env a -> Expr a -> Expr a -> Bool
forall a. Env a -> Expr a -> Expr a -> Bool
isNormEq
isNTrnsEq (Just NormCheck
Weak) = (Expr a -> Maybe (Expr a))
-> (Env a -> Expr a -> Expr a -> Bool)
-> Env a
-> Expr a
-> Expr a
-> Bool
forall a.
(Expr a -> Maybe (Expr a))
-> (Env a -> Expr a -> Expr a -> Bool)
-> Env a
-> Expr a
-> Expr a
-> Bool
isSTrnsSEq Expr a -> Maybe (Expr a)
forall a. Expr a -> Maybe (Expr a)
norStep Env a -> Expr a -> Expr a -> Bool
forall a. Env a -> Expr a -> Expr a -> Bool
isWnfEq
isNTrnsEq (Just NormCheck
Head) = (Expr a -> Maybe (Expr a))
-> (Env a -> Expr a -> Expr a -> Bool)
-> Env a
-> Expr a
-> Expr a
-> Bool
forall a.
(Expr a -> Maybe (Expr a))
-> (Env a -> Expr a -> Expr a -> Bool)
-> Env a
-> Expr a
-> Expr a
-> Bool
isSTrnsSEq Expr a -> Maybe (Expr a)
forall a. Expr a -> Maybe (Expr a)
norStep Env a -> Expr a -> Expr a -> Bool
forall a. Env a -> Expr a -> Expr a -> Bool
isHnfEq

isUnNTrEq :: Env a -> Expr a -> Expr a -> Bool
isUnNTrEq :: forall a. Env a -> Expr a -> Expr a -> Bool
isUnNTrEq Env a
g Expr a
e1 Expr a
e2 = Maybe NormCheck -> Env a -> Expr a -> Expr a -> Bool
forall a. Maybe NormCheck -> Env a -> Expr a -> Expr a -> Bool
isNTrnsEq Maybe NormCheck
forall a. Maybe a
Nothing Env a
g Expr a
e2 Expr a
e1

-- Multiple applicative order beta, alpha reductions and/or definitions
isATrnsEq :: Maybe NormCheck -> Env a -> Expr a -> Expr a -> Bool
isATrnsEq :: forall a. Maybe NormCheck -> Env a -> Expr a -> Expr a -> Bool
isATrnsEq Maybe NormCheck
Nothing = (Expr a -> Maybe (Expr a)) -> Env a -> Expr a -> Expr a -> Bool
forall a.
(Expr a -> Maybe (Expr a)) -> Env a -> Expr a -> Expr a -> Bool
isSTrnsEq Expr a -> Maybe (Expr a)
forall a. Expr a -> Maybe (Expr a)
appStep
isATrnsEq (Just NormCheck
Strong) = (Expr a -> Maybe (Expr a))
-> (Env a -> Expr a -> Expr a -> Bool)
-> Env a
-> Expr a
-> Expr a
-> Bool
forall a.
(Expr a -> Maybe (Expr a))
-> (Env a -> Expr a -> Expr a -> Bool)
-> Env a
-> Expr a
-> Expr a
-> Bool
isSTrnsSEq Expr a -> Maybe (Expr a)
forall a. Expr a -> Maybe (Expr a)
appStep Env a -> Expr a -> Expr a -> Bool
forall a. Env a -> Expr a -> Expr a -> Bool
isNormEq
isATrnsEq (Just NormCheck
Weak) = (Expr a -> Maybe (Expr a))
-> (Env a -> Expr a -> Expr a -> Bool)
-> Env a
-> Expr a
-> Expr a
-> Bool
forall a.
(Expr a -> Maybe (Expr a))
-> (Env a -> Expr a -> Expr a -> Bool)
-> Env a
-> Expr a
-> Expr a
-> Bool
isSTrnsSEq Expr a -> Maybe (Expr a)
forall a. Expr a -> Maybe (Expr a)
appStep Env a -> Expr a -> Expr a -> Bool
forall a. Env a -> Expr a -> Expr a -> Bool
isWnfEq
isATrnsEq (Just NormCheck
Head) = (Expr a -> Maybe (Expr a))
-> (Env a -> Expr a -> Expr a -> Bool)
-> Env a
-> Expr a
-> Expr a
-> Bool
forall a.
(Expr a -> Maybe (Expr a))
-> (Env a -> Expr a -> Expr a -> Bool)
-> Env a
-> Expr a
-> Expr a
-> Bool
isSTrnsSEq Expr a -> Maybe (Expr a)
forall a. Expr a -> Maybe (Expr a)
appStep Env a -> Expr a -> Expr a -> Bool
forall a. Env a -> Expr a -> Expr a -> Bool
isHnfEq

isUnATrEq :: Env a -> Expr a -> Expr a -> Bool
isUnATrEq :: forall a. Env a -> Expr a -> Expr a -> Bool
isUnATrEq Env a
g Expr a
e1 Expr a
e2 = Maybe NormCheck -> Env a -> Expr a -> Expr a -> Bool
forall a. Maybe NormCheck -> Env a -> Expr a -> Expr a -> Bool
isATrnsEq Maybe NormCheck
forall a. Maybe a
Nothing Env a
g Expr a
e2 Expr a
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 :: forall a.
(Expr a -> Maybe (Expr a)) -> Env a -> Expr a -> Expr a -> Bool
isSTrnsEq Expr a -> Maybe (Expr a)
step Env a
g Expr a
e1 Expr a
e2 = Maybe (Expr a) -> Bool
forall a. Maybe a -> Bool
Mb.isJust ((Expr a -> Maybe (Expr a))
-> (Expr a -> Bool) -> Expr a -> Maybe (Expr a)
forall a.
(Expr a -> Maybe (Expr a))
-> (Expr a -> Bool) -> Expr a -> Maybe (Expr a)
findSTrans Expr a -> Maybe (Expr a)
step (Env a -> Expr a -> Expr a -> Bool
forall a. Env a -> Expr a -> Expr a -> Bool
isEquiv Env a
g Expr a
e2) (Env a -> Expr a -> Expr a
forall a. Env a -> Expr a -> Expr a
canon Env a
g Expr a
e1))

findSTrans :: (Expr a -> Maybe (Expr a)) -> (Expr a -> Bool) -> Expr a -> Maybe (Expr a)
findSTrans :: forall a.
(Expr a -> Maybe (Expr a))
-> (Expr a -> Bool) -> Expr a -> Maybe (Expr a)
findSTrans Expr a -> Maybe (Expr a)
step Expr a -> Bool
f Expr a
e = do
  if Expr a -> Bool
f Expr a
e then -- Maybe no reductions are needed
    Expr a -> Maybe (Expr a)
forall a. a -> Maybe a
forall (m :: * -> *) a. Monad m => a -> m a
return Expr a
e
  else do -- One or more reductions are needed
    Expr a
e' <- Expr a -> Maybe (Expr a)
step Expr a
e
    if Expr a -> Bool
f Expr a
e' then
      Expr a -> Maybe (Expr a)
forall a. a -> Maybe a
forall (m :: * -> *) a. Monad m => a -> m a
return Expr a
e'
    else
      (Expr a -> Maybe (Expr a))
-> (Expr a -> Bool) -> Expr a -> Maybe (Expr a)
forall a.
(Expr a -> Maybe (Expr a))
-> (Expr a -> Bool) -> Expr a -> Maybe (Expr a)
findSTrans Expr a -> Maybe (Expr a)
step Expr a -> Bool
f Expr a
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 :: forall a.
(Expr a -> Maybe (Expr a))
-> (Env a -> Expr a -> Expr a -> Bool)
-> Env a
-> Expr a
-> Expr a
-> Bool
isSTrnsSEq Expr a -> Maybe (Expr a)
step Env a -> Expr a -> Expr a -> Bool
isNfEq Env a
g Expr a
e1 Expr a
e2 =
  case (Expr a -> Maybe (Expr a))
-> (Expr a -> Bool) -> Expr a -> Maybe (Expr a)
forall a.
(Expr a -> Maybe (Expr a))
-> (Expr a -> Bool) -> Expr a -> Maybe (Expr a)
findSTrans Expr a -> Maybe (Expr a)
step (Env a -> Expr a -> Expr a -> Bool
forall a. Env a -> Expr a -> Expr a -> Bool
isEquiv Env a
g Expr a
e2) (Env a -> Expr a -> Expr a
forall a. Env a -> Expr a -> Expr a
canon Env a
g Expr a
e1) of
    Maybe (Expr a)
Nothing -> Bool
False
    Just Expr a
e1' -> Env a -> Expr a -> Expr a -> Bool
isNfEq Env a
g Expr a
e1' Expr a
e2

--------------------------------------------------------------------------------
-- | Definition Equivalence
--------------------------------------------------------------------------------
isDefnEq :: Maybe NormCheck -> Env a -> Expr a -> Expr a -> Bool
isDefnEq :: forall a. Maybe NormCheck -> Env a -> Expr a -> Expr a -> Bool
isDefnEq Maybe NormCheck
Nothing Env a
g Expr a
e1 Expr a
e2 = Expr a -> Env a -> Expr a
forall a. Expr a -> Env a -> Expr a
subst Expr a
e1 Env a
g Expr a -> Expr a -> Bool
forall a. Eq a => a -> a -> Bool
== Expr a -> Env a -> Expr a
forall a. Expr a -> Env a -> Expr a
subst Expr a
e2 Env a
g
isDefnEq (Just NormCheck
Strong) Env a
g Expr a
e1 Expr a
e2 = Env a -> Expr a -> Expr a -> Bool
forall a. Env a -> Expr a -> Expr a -> Bool
isNormEq Env a
g Expr a
e1 Expr a
e2
isDefnEq (Just NormCheck
Weak) Env a
g Expr a
e1 Expr a
e2 = Env a -> Expr a -> Expr a -> Bool
forall a. Env a -> Expr a -> Expr a -> Bool
isWnfEq Env a
g Expr a
e1 Expr a
e2
isDefnEq (Just NormCheck
Head) Env a
g Expr a
e1 Expr a
e2 = Env a -> Expr a -> Expr a -> Bool
forall a. Env a -> Expr a -> Expr a -> Bool
isHnfEq Env a
g Expr a
e1 Expr a
e2

--------------------------------------------------------------------------------
-- | Alpha Equivalence
--------------------------------------------------------------------------------
isAlphEq :: Maybe NormCheck -> Env a -> Expr a -> Expr a -> Bool
isAlphEq :: forall a. Maybe NormCheck -> Env a -> Expr a -> Expr a -> Bool
isAlphEq Maybe NormCheck
Nothing Env a
_ Expr a
e1 Expr a
e2 = Expr a -> Expr a
forall a. Expr a -> Expr a
alphaNormal Expr a
e1 Expr a -> Expr a -> Bool
forall a. Eq a => a -> a -> Bool
== Expr a -> Expr a
forall a. Expr a -> Expr a
alphaNormal Expr a
e2
isAlphEq (Just NormCheck
Strong) Env a
g Expr a
e1 Expr a
e2 = (Env a -> Expr a -> Expr a -> Bool)
-> Env a -> Expr a -> Expr a -> Bool
forall a.
(Env a -> Expr a -> Expr a -> Bool)
-> Env a -> Expr a -> Expr a -> Bool
isAlphPEq Env a -> Expr a -> Expr a -> Bool
forall a. Env a -> Expr a -> Expr a -> Bool
isNormEq Env a
g Expr a
e1 Expr a
e2
isAlphEq (Just NormCheck
Weak) Env a
g Expr a
e1 Expr a
e2 = (Env a -> Expr a -> Expr a -> Bool)
-> Env a -> Expr a -> Expr a -> Bool
forall a.
(Env a -> Expr a -> Expr a -> Bool)
-> Env a -> Expr a -> Expr a -> Bool
isAlphPEq Env a -> Expr a -> Expr a -> Bool
forall a. Env a -> Expr a -> Expr a -> Bool
isWnfEq Env a
g Expr a
e1 Expr a
e2
isAlphEq (Just NormCheck
Head) Env a
g Expr a
e1 Expr a
e2 = (Env a -> Expr a -> Expr a -> Bool)
-> Env a -> Expr a -> Expr a -> Bool
forall a.
(Env a -> Expr a -> Expr a -> Bool)
-> Env a -> Expr a -> Expr a -> Bool
isAlphPEq Env a -> Expr a -> Expr a -> Bool
forall a. Env a -> Expr a -> Expr a -> Bool
isHnfEq Env a
g Expr a
e1 Expr a
e2

-- Alpha Equivalence with provided normal form check
isAlphPEq :: (Env a -> Expr a -> Expr a -> Bool) -> Env a -> Expr a -> Expr a -> Bool
isAlphPEq :: forall a.
(Env a -> Expr a -> Expr a -> Bool)
-> Env a -> Expr a -> Expr a -> Bool
isAlphPEq Env a -> Expr a -> Expr a -> Bool
isNfEq Env a
g Expr a
e1 Expr a
e2 = (Expr a -> Expr a
forall a. Expr a -> Expr a
alphaNormal Expr a
e1 Expr a -> Expr a -> Bool
forall a. Eq a => a -> a -> Bool
== Expr a -> Expr a
forall a. Expr a -> Expr a
alphaNormal Expr a
e2) Bool -> Bool -> Bool
&& Env a -> Expr a -> Expr a -> Bool
isNfEq Env a
g Expr a
e1 Expr a
e2

alphaNormal :: Expr a -> Expr a
alphaNormal :: forall a. Expr a -> Expr a
alphaNormal = Int -> Expr a -> Expr a
forall a. Int -> Expr a -> Expr a
alphaShift Int
0

alphaShift :: Int -> Expr a -> Expr a
alphaShift :: forall a. Int -> Expr a -> Expr a
alphaShift Int
n Expr a
e = State Int (Expr a) -> Int -> Expr a
forall s a. State s a -> s -> a
evalState (HashMap Id Id -> Expr a -> State Int (Expr a)
forall a. HashMap Id Id -> Expr a -> AlphaM (Expr a)
normalize HashMap Id Id
forall k v. HashMap k v
M.empty Expr a
e) Int
n

type AlphaM a = State Int a

normalize :: M.HashMap Id Id -> Expr a -> AlphaM (Expr a)
normalize :: forall a. HashMap Id Id -> Expr a -> AlphaM (Expr a)
normalize HashMap Id Id
g (EVar Id
x a
z) =
  Expr a -> StateT Int Identity (Expr a)
forall a. a -> StateT Int Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return (Id -> a -> Expr a
forall a. Id -> a -> Expr a
EVar (HashMap Id Id -> Id -> Id
rename HashMap Id Id
g Id
x) a
z)

normalize HashMap Id Id
g (EApp Expr a
e1 Expr a
e2 a
z) = do
  Expr a
e1' <- HashMap Id Id -> Expr a -> StateT Int Identity (Expr a)
forall a. HashMap Id Id -> Expr a -> AlphaM (Expr a)
normalize HashMap Id Id
g Expr a
e1
  Expr a
e2' <- HashMap Id Id -> Expr a -> StateT Int Identity (Expr a)
forall a. HashMap Id Id -> Expr a -> AlphaM (Expr a)
normalize HashMap Id Id
g Expr a
e2
  Expr a -> StateT Int Identity (Expr a)
forall a. a -> StateT Int Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return (Expr a -> Expr a -> a -> Expr a
forall a. Expr a -> Expr a -> a -> Expr a
EApp Expr a
e1' Expr a
e2' a
z)

normalize HashMap Id Id
g (ELam (Bind Id
x a
z1) Expr a
e a
z2) = do
  Id
y     <- AlphaM Id
fresh
  let g' :: HashMap Id Id
g' = Id -> Id -> HashMap Id Id -> HashMap Id Id
forall k v.
(Eq k, Hashable k) =>
k -> v -> HashMap k v -> HashMap k v
M.insert Id
x Id
y HashMap Id Id
g
  Expr a
e'    <- HashMap Id Id -> Expr a -> StateT Int Identity (Expr a)
forall a. HashMap Id Id -> Expr a -> AlphaM (Expr a)
normalize HashMap Id Id
g' Expr a
e
  Expr a -> StateT Int Identity (Expr a)
forall a. a -> StateT Int Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return (Bind a -> Expr a -> a -> Expr a
forall a. Bind a -> Expr a -> a -> Expr a
ELam (Id -> a -> Bind a
forall a. Id -> a -> Bind a
Bind Id
y a
z1) Expr a
e' a
z2)

rename :: M.HashMap Id Id -> Id -> Id
rename :: HashMap Id Id -> Id -> Id
rename HashMap Id Id
g Id
x = Id -> Id -> HashMap Id Id -> Id
forall k v. (Eq k, Hashable k) => v -> k -> HashMap k v -> v
M.lookupDefault Id
x Id
x HashMap Id Id
g

fresh :: AlphaM Id
fresh :: AlphaM Id
fresh = do
  Int
n <- StateT Int Identity Int
forall s (m :: * -> *). MonadState s m => m s
get
  Int -> StateT Int Identity ()
forall s (m :: * -> *). MonadState s m => s -> m ()
put (Int
n Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1)
  Id -> AlphaM Id
forall a. a -> StateT Int Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return (Int -> Id
newAId Int
n)

newAId :: Int -> Id
newAId :: Int -> Id
newAId Int
n = Id
aId Id -> Id -> Id
forall a. [a] -> [a] -> [a]
++ Int -> Id
forall a. Show a => a -> Id
show Int
n

_isAId :: Id -> Maybe Int
_isAId :: Id -> Maybe Int
_isAId Id
x
  | Id -> Id -> Bool
forall a. Eq a => [a] -> [a] -> Bool
L.isPrefixOf Id
aId Id
x = Int -> Maybe Int
forall a. a -> Maybe a
Just (Int -> Maybe Int) -> (Id -> Int) -> Id -> Maybe Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Id -> Int
forall a. Read a => Id -> a
read (Id -> Int) -> (Id -> Id) -> Id -> Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> Id -> Id
forall a. Int -> [a] -> [a]
drop Int
2 (Id -> Maybe Int) -> Id -> Maybe Int
forall a b. (a -> b) -> a -> b
$ Id
x
  | Bool
otherwise          = Maybe Int
forall a. Maybe a
Nothing

aId :: String
aId :: Id
aId = Id
"$x"

--------------------------------------------------------------------------------
-- | Beta Reduction
--------------------------------------------------------------------------------
-- Beta reduction, without any normal form check
isBetaEq :: Maybe NormCheck -> Env a -> Expr a -> Expr a -> Bool
isBetaEq :: forall a. Maybe NormCheck -> Env a -> Expr a -> Expr a -> Bool
isBetaEq Maybe NormCheck
Nothing Env a
_ Expr a
e1 Expr a
e2 = [Bool] -> Bool
forall (t :: * -> *). Foldable t => t Bool -> Bool
or [ Expr a
e1' Expr a -> Expr a -> Bool
forall a. Eq a => a -> a -> Bool
== Expr a
e2  | Expr a
e1' <- Expr a -> [Expr a]
forall a. Expr a -> [Expr a]
betas Expr a
e1 ]
isBetaEq (Just NormCheck
Strong) Env a
g Expr a
e1 Expr a
e2 = (Env a -> Expr a -> Expr a -> Bool)
-> Env a -> Expr a -> Expr a -> Bool
forall a.
(Env a -> Expr a -> Expr a -> Bool)
-> Env a -> Expr a -> Expr a -> Bool
isBetaPEq Env a -> Expr a -> Expr a -> Bool
forall a. Env a -> Expr a -> Expr a -> Bool
isNormEq Env a
g Expr a
e1 Expr a
e2
isBetaEq (Just NormCheck
Weak) Env a
g Expr a
e1 Expr a
e2 = (Env a -> Expr a -> Expr a -> Bool)
-> Env a -> Expr a -> Expr a -> Bool
forall a.
(Env a -> Expr a -> Expr a -> Bool)
-> Env a -> Expr a -> Expr a -> Bool
isBetaPEq Env a -> Expr a -> Expr a -> Bool
forall a. Env a -> Expr a -> Expr a -> Bool
isWnfEq Env a
g Expr a
e1 Expr a
e2
isBetaEq (Just NormCheck
Head) Env a
g Expr a
e1 Expr a
e2 = (Env a -> Expr a -> Expr a -> Bool)
-> Env a -> Expr a -> Expr a -> Bool
forall a.
(Env a -> Expr a -> Expr a -> Bool)
-> Env a -> Expr a -> Expr a -> Bool
isBetaPEq Env a -> Expr a -> Expr a -> Bool
forall a. Env a -> Expr a -> Expr a -> Bool
isHnfEq Env a
g Expr a
e1 Expr a
e2

isUnBeta :: Env a -> Expr a -> Expr a -> Bool
isUnBeta :: forall a. Env a -> Expr a -> Expr a -> Bool
isUnBeta Env a
g Expr a
e1 Expr a
e2 = Maybe NormCheck -> Env a -> Expr a -> Expr a -> Bool
forall a. Maybe NormCheck -> Env a -> Expr a -> Expr a -> Bool
isBetaEq Maybe NormCheck
forall a. Maybe a
Nothing Env a
g Expr a
e2 Expr a
e1

-- Beta reduction, with provided normal form check
isBetaPEq :: (Env a -> Expr a -> Expr a -> Bool) -> Env a -> Expr a -> Expr a -> Bool
isBetaPEq :: forall a.
(Env a -> Expr a -> Expr a -> Bool)
-> Env a -> Expr a -> Expr a -> Bool
isBetaPEq Env a -> Expr a -> Expr a -> Bool
isNfEq Env a
g Expr a
e1 Expr a
e2 = [Bool] -> Bool
forall (t :: * -> *). Foldable t => t Bool -> Bool
or [ Env a -> Expr a -> Expr a -> Bool
isNfEq Env a
g Expr a
e1' Expr a
e2  | Expr a
e1' <- Expr a -> [Expr a]
forall a. Expr a -> [Expr a]
betas Expr a
e1 ]

-- Use normal order evaluation strategy
isNBetaEq :: Maybe NormCheck -> Env a -> Expr a -> Expr a -> Bool
isNBetaEq :: forall a. Maybe NormCheck -> Env a -> Expr a -> Expr a -> Bool
isNBetaEq = (Expr a -> Maybe (Expr a))
-> Maybe NormCheck -> Env a -> Expr a -> Expr a -> Bool
forall a.
(Expr a -> Maybe (Expr a))
-> Maybe NormCheck -> Env a -> Expr a -> Expr a -> Bool
isSBetaEq Expr a -> Maybe (Expr a)
forall a. Expr a -> Maybe (Expr a)
norStep

isUnNBeta :: Env a -> Expr a -> Expr a -> Bool
isUnNBeta :: forall a. Env a -> Expr a -> Expr a -> Bool
isUnNBeta Env a
g Expr a
e1 Expr a
e2 = Maybe NormCheck -> Env a -> Expr a -> Expr a -> Bool
forall a. Maybe NormCheck -> Env a -> Expr a -> Expr a -> Bool
isNBetaEq Maybe NormCheck
forall a. Maybe a
Nothing Env a
g Expr a
e2 Expr a
e1

-- Use applicative order evaluation strategy
isABetaEq :: Maybe NormCheck -> Env a -> Expr a -> Expr a -> Bool
isABetaEq :: forall a. Maybe NormCheck -> Env a -> Expr a -> Expr a -> Bool
isABetaEq = (Expr a -> Maybe (Expr a))
-> Maybe NormCheck -> Env a -> Expr a -> Expr a -> Bool
forall a.
(Expr a -> Maybe (Expr a))
-> Maybe NormCheck -> Env a -> Expr a -> Expr a -> Bool
isSBetaEq Expr a -> Maybe (Expr a)
forall a. Expr a -> Maybe (Expr a)
appStep

isUnABeta :: Env a -> Expr a -> Expr a -> Bool
isUnABeta :: forall a. Env a -> Expr a -> Expr a -> Bool
isUnABeta Env a
g Expr a
e1 Expr a
e2 = Maybe NormCheck -> Env a -> Expr a -> Expr a -> Bool
forall a. Maybe NormCheck -> Env a -> Expr a -> Expr a -> Bool
isABetaEq Maybe NormCheck
forall a. Maybe a
Nothing Env a
g Expr a
e2 Expr a
e1

-- Use selected order evaluation strategy
isSBetaEq :: (Expr a -> Maybe (Expr a)) -> Maybe NormCheck -> Env a -> Expr a -> Expr a -> Bool
isSBetaEq :: forall a.
(Expr a -> Maybe (Expr a))
-> Maybe NormCheck -> Env a -> Expr a -> Expr a -> Bool
isSBetaEq Expr a -> Maybe (Expr a)
step Maybe NormCheck
Nothing Env a
g Expr a
e1 Expr a
e2 = Expr a -> Maybe (Expr a)
step (Expr a -> Env a -> Expr a
forall a. Expr a -> Env a -> Expr a
subst Expr a
e1 Env a
g) Maybe (Expr a) -> Maybe (Expr a) -> Bool
forall a. Eq a => a -> a -> Bool
== Expr a -> Maybe (Expr a)
forall a. a -> Maybe a
Just (Expr a -> Env a -> Expr a
forall a. Expr a -> Env a -> Expr a
subst Expr a
e2 Env a
g)
isSBetaEq Expr a -> Maybe (Expr a)
step (Just NormCheck
Strong) Env a
g Expr a
e1 Expr a
e2 = case Expr a -> Maybe (Expr a)
step (Expr a -> Env a -> Expr a
forall a. Expr a -> Env a -> Expr a
subst Expr a
e1 Env a
g) of
  Maybe (Expr a)
Nothing -> Bool
False
  Just Expr a
e1' -> Env a -> Expr a -> Expr a -> Bool
forall a. Env a -> Expr a -> Expr a -> Bool
isNormEq Env a
g Expr a
e1' Expr a
e2
isSBetaEq Expr a -> Maybe (Expr a)
step (Just NormCheck
Weak) Env a
g Expr a
e1 Expr a
e2 = case Expr a -> Maybe (Expr a)
step (Expr a -> Env a -> Expr a
forall a. Expr a -> Env a -> Expr a
subst Expr a
e1 Env a
g) of
  Maybe (Expr a)
Nothing -> Bool
False
  Just Expr a
e1' -> Env a -> Expr a -> Expr a -> Bool
forall a. Env a -> Expr a -> Expr a -> Bool
isWnfEq Env a
g Expr a
e1' Expr a
e2
isSBetaEq Expr a -> Maybe (Expr a)
step (Just NormCheck
Head) Env a
g Expr a
e1 Expr a
e2 = case Expr a -> Maybe (Expr a)
step (Expr a -> Env a -> Expr a
forall a. Expr a -> Env a -> Expr a
subst Expr a
e1 Env a
g) of
  Maybe (Expr a)
Nothing -> Bool
False
  Just Expr a
e1' -> Env a -> Expr a -> Expr a -> Bool
forall a. Env a -> Expr a -> Expr a -> Bool
isHnfEq Env a
g Expr a
e1' Expr a
e2

-- norStep is a single normal order reduction
norStep :: Expr a -> Maybe (Expr a)
norStep :: forall a. Expr a -> Maybe (Expr a)
norStep (EVar {}) = Maybe (Expr a)
forall a. Maybe a
Nothing
norStep (ELam Bind a
b Expr a
e a
l) = do
  Expr a
e' <- Expr a -> Maybe (Expr a)
forall a. Expr a -> Maybe (Expr a)
norStep Expr a
e
  Expr a -> Maybe (Expr a)
forall a. a -> Maybe a
forall (m :: * -> *) a. Monad m => a -> m a
return (Expr a -> Maybe (Expr a)) -> Expr a -> Maybe (Expr a)
forall a b. (a -> b) -> a -> b
$ Bind a -> Expr a -> a -> Expr a
forall a. Bind a -> Expr a -> a -> Expr a
ELam Bind a
b Expr a
e' a
l
norStep (EApp e1 :: Expr a
e1@(ELam {}) Expr a
e2 a
_) = Expr a -> Expr a -> Maybe (Expr a)
forall a. Expr a -> Expr a -> Maybe (Expr a)
beta Expr a
e1 Expr a
e2
norStep (EApp Expr a
e1 Expr a
e2 a
l) = case Expr a -> Maybe (Expr a)
forall a. Expr a -> Maybe (Expr a)
norStep Expr a
e1 of
  Just Expr a
e1' -> Expr a -> Maybe (Expr a)
forall a. a -> Maybe a
forall (m :: * -> *) a. Monad m => a -> m a
return (Expr a -> Maybe (Expr a)) -> Expr a -> Maybe (Expr a)
forall a b. (a -> b) -> a -> b
$ Expr a -> Expr a -> a -> Expr a
forall a. Expr a -> Expr a -> a -> Expr a
EApp Expr a
e1' Expr a
e2 a
l
  Maybe (Expr a)
Nothing -> case Expr a -> Maybe (Expr a)
forall a. Expr a -> Maybe (Expr a)
norStep Expr a
e2 of
    Just Expr a
e2' -> Expr a -> Maybe (Expr a)
forall a. a -> Maybe a
forall (m :: * -> *) a. Monad m => a -> m a
return (Expr a -> Maybe (Expr a)) -> Expr a -> Maybe (Expr a)
forall a b. (a -> b) -> a -> b
$ Expr a -> Expr a -> a -> Expr a
forall a. Expr a -> Expr a -> a -> Expr a
EApp Expr a
e1 Expr a
e2' a
l
    Maybe (Expr a)
Nothing -> Maybe (Expr a)
forall a. Maybe a
Nothing

-- appStep is a single applicative order reduction
appStep :: Expr a -> Maybe (Expr a)
appStep :: forall a. Expr a -> Maybe (Expr a)
appStep (EVar {}) = Maybe (Expr a)
forall a. Maybe a
Nothing
appStep (ELam Bind a
b Expr a
e a
l) = do
  Expr a
e' <- Expr a -> Maybe (Expr a)
forall a. Expr a -> Maybe (Expr a)
appStep Expr a
e
  Expr a -> Maybe (Expr a)
forall a. a -> Maybe a
forall (m :: * -> *) a. Monad m => a -> m a
return (Expr a -> Maybe (Expr a)) -> Expr a -> Maybe (Expr a)
forall a b. (a -> b) -> a -> b
$ Bind a -> Expr a -> a -> Expr a
forall a. Bind a -> Expr a -> a -> Expr a
ELam Bind a
b Expr a
e' a
l
appStep (EApp e1 :: Expr a
e1@(ELam {}) Expr a
e2 a
l) = case Expr a -> Maybe (Expr a)
forall a. Expr a -> Maybe (Expr a)
appStep Expr a
e1 of
  Just Expr a
e1' -> Expr a -> Maybe (Expr a)
forall a. a -> Maybe a
Just (Expr a -> Maybe (Expr a)) -> Expr a -> Maybe (Expr a)
forall a b. (a -> b) -> a -> b
$ Expr a -> Expr a -> a -> Expr a
forall a. Expr a -> Expr a -> a -> Expr a
EApp Expr a
e1' Expr a
e2 a
l
  Maybe (Expr a)
Nothing -> case Expr a -> Maybe (Expr a)
forall a. Expr a -> Maybe (Expr a)
appStep Expr a
e2 of
    Just Expr a
e2' -> Expr a -> Maybe (Expr a)
forall a. a -> Maybe a
Just (Expr a -> Maybe (Expr a)) -> Expr a -> Maybe (Expr a)
forall a b. (a -> b) -> a -> b
$ Expr a -> Expr a -> a -> Expr a
forall a. Expr a -> Expr a -> a -> Expr a
EApp Expr a
e1 Expr a
e2' a
l
    Maybe (Expr a)
Nothing -> Expr a -> Expr a -> Maybe (Expr a)
forall a. Expr a -> Expr a -> Maybe (Expr a)
beta Expr a
e1 Expr a
e2
appStep (EApp Expr a
e1 Expr a
e2 a
l) = case Expr a -> Maybe (Expr a)
forall a. Expr a -> Maybe (Expr a)
appStep Expr a
e1 of
  Just Expr a
e1' -> Expr a -> Maybe (Expr a)
forall a. a -> Maybe a
forall (m :: * -> *) a. Monad m => a -> m a
return (Expr a -> Maybe (Expr a)) -> Expr a -> Maybe (Expr a)
forall a b. (a -> b) -> a -> b
$ Expr a -> Expr a -> a -> Expr a
forall a. Expr a -> Expr a -> a -> Expr a
EApp Expr a
e1' Expr a
e2 a
l
  Maybe (Expr a)
Nothing -> case Expr a -> Maybe (Expr a)
forall a. Expr a -> Maybe (Expr a)
appStep Expr a
e2 of
    Just Expr a
e2' -> Expr a -> Maybe (Expr a)
forall a. a -> Maybe a
forall (m :: * -> *) a. Monad m => a -> m a
return (Expr a -> Maybe (Expr a)) -> Expr a -> Maybe (Expr a)
forall a b. (a -> b) -> a -> b
$ Expr a -> Expr a -> a -> Expr a
forall a. Expr a -> Expr a -> a -> Expr a
EApp Expr a
e1 Expr a
e2' a
l
    Maybe (Expr a)
Nothing -> Maybe (Expr a)
forall a. Maybe a
Nothing

isNormal :: Env a -> Expr a -> Bool
isNormal :: forall a. Env a -> Expr a -> Bool
isNormal Env a
g = [Expr a] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null ([Expr a] -> Bool) -> (Expr a -> [Expr a]) -> Expr a -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Expr a -> [Expr a]
forall a. Expr a -> [Expr a]
betas (Expr a -> [Expr a]) -> (Expr a -> Expr a) -> Expr a -> [Expr a]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Expr a -> Env a -> Expr a
forall a. Expr a -> Env a -> Expr a
`subst` Env a
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 :: forall a. Expr a -> [Expr a]
betas (EVar Id
_ a
_)     = []
betas (ELam Bind a
b Expr a
e a
z)   = [ Bind a -> Expr a -> a -> Expr a
forall a. Bind a -> Expr a -> a -> Expr a
ELam Bind a
b Expr a
e' a
z | Expr a
e' <- Expr a -> [Expr a]
forall a. Expr a -> [Expr a]
betas Expr a
e ]
betas (EApp Expr a
e1 Expr a
e2 a
z) = [ Expr a -> Expr a -> a -> Expr a
forall a. Expr a -> Expr a -> a -> Expr a
EApp Expr a
e1' Expr a
e2 a
z | Expr a
e1' <- Expr a -> [Expr a]
forall a. Expr a -> [Expr a]
betas Expr a
e1 ]
                    [Expr a] -> [Expr a] -> [Expr a]
forall a. [a] -> [a] -> [a]
++ [ Expr a -> Expr a -> a -> Expr a
forall a. Expr a -> Expr a -> a -> Expr a
EApp Expr a
e1 Expr a
e2' a
z | Expr a
e2' <- Expr a -> [Expr a]
forall a. Expr a -> [Expr a]
betas Expr a
e2 ]
                    [Expr a] -> [Expr a] -> [Expr a]
forall a. [a] -> [a] -> [a]
++ Maybe (Expr a) -> [Expr a]
forall a. Maybe a -> [a]
Mb.maybeToList (Expr a -> Expr a -> Maybe (Expr a)
forall a. Expr a -> Expr a -> Maybe (Expr a)
beta Expr a
e1 Expr a
e2)

beta :: Expr a -> Expr a -> Maybe (Expr a)
beta :: forall a. Expr a -> Expr a -> Maybe (Expr a)
beta (ELam (Bind Id
x a
_) Expr a
e a
_) Expr a
e' = Expr a -> Id -> Expr a -> Maybe (Expr a)
forall a. Expr a -> Id -> Expr a -> Maybe (Expr a)
substCA Expr a
e Id
x Expr a
e'
beta Expr a
_                    Expr a
_   = Maybe (Expr a)
forall a. Maybe a
Nothing

substCA :: Expr a -> Id -> Expr a -> Maybe (Expr a)
substCA :: forall a. Expr a -> Id -> Expr a -> Maybe (Expr a)
substCA Expr a
e Id
x Expr a
e'           = [Bind a] -> Expr a -> Maybe (Expr a)
go [] Expr a
e
  where
    zs :: HashSet Id
zs                   = Expr a -> HashSet Id
forall a. Expr a -> HashSet Id
freeVars Expr a
e'
    bnd :: [Bind a] -> HashSet Id -> Bool
bnd  [Bind a]
bs HashSet Id
zs           = [Bool] -> Bool
forall (t :: * -> *). Foldable t => t Bool -> Bool
or [ Bind a
b Bind a -> HashSet Id -> Bool
forall a. Bind a -> HashSet Id -> Bool
`isIn` HashSet Id
zs | Bind a
b <- [Bind a]
bs ]
    go :: [Bind a] -> Expr a -> Maybe (Expr a)
go [Bind a]
bs e :: Expr a
e@(EVar Id
y a
_)
      | Id
y Id -> Id -> Bool
forall a. Eq a => a -> a -> Bool
/= Id
x           = Expr a -> Maybe (Expr a)
forall a. a -> Maybe a
Just Expr a
e            -- different var, no subst
      | [Bind a] -> HashSet Id -> Bool
forall {a}. [Bind a] -> HashSet Id -> Bool
bnd  [Bind a]
bs HashSet Id
zs       = Maybe (Expr a)
forall a. Maybe a
Nothing           -- same var, but free-var-captured
      | Bool
otherwise        = Expr a -> Maybe (Expr a)
forall a. a -> Maybe a
Just Expr a
e'           -- same var, but no capture
    go [Bind a]
bs (EApp Expr a
e1 Expr a
e2 a
l) = do Expr a
e1' <- [Bind a] -> Expr a -> Maybe (Expr a)
go [Bind a]
bs Expr a
e1
                              Expr a
e2' <- [Bind a] -> Expr a -> Maybe (Expr a)
go [Bind a]
bs Expr a
e2
                              Expr a -> Maybe (Expr a)
forall a. a -> Maybe a
Just (Expr a -> Expr a -> a -> Expr a
forall a. Expr a -> Expr a -> a -> Expr a
EApp Expr a
e1' Expr a
e2' a
l)
    go [Bind a]
bs e :: Expr a
e@(ELam Bind a
b Expr a
e1  a
l)
      | Id
x Id -> Id -> Bool
forall a. Eq a => a -> a -> Bool
== Bind a -> Id
forall a. Bind a -> Id
bindId Bind a
b    = Expr a -> Maybe (Expr a)
forall a. a -> Maybe a
Just Expr a
e            -- subst-var has been rebound
      | Bool
otherwise        = do Expr a
e1' <- [Bind a] -> Expr a -> Maybe (Expr a)
go (Bind a
bBind a -> [Bind a] -> [Bind a]
forall a. a -> [a] -> [a]
:[Bind a]
bs) Expr a
e1
                              Expr a -> Maybe (Expr a)
forall a. a -> Maybe a
Just (Bind a -> Expr a -> a -> Expr a
forall a. Bind a -> Expr a -> a -> Expr a
ELam Bind a
b Expr a
e1' a
l)

isIn :: Bind a -> S.HashSet Id -> Bool
isIn :: forall a. Bind a -> HashSet Id -> Bool
isIn = Id -> HashSet Id -> Bool
forall a. (Eq a, Hashable a) => a -> HashSet a -> Bool
S.member (Id -> HashSet Id -> Bool)
-> (Bind a -> Id) -> Bind a -> HashSet Id -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Bind a -> Id
forall a. Bind a -> Id
bindId

--------------------------------------------------------------------------------
-- | Eta Reduction
--------------------------------------------------------------------------------
-- Eta reduction, without any normal form check
isEtaaEq :: Maybe NormCheck -> Env a -> Expr a -> Expr a -> Bool
isEtaaEq :: forall a. Maybe NormCheck -> Env a -> Expr a -> Expr a -> Bool
isEtaaEq Maybe NormCheck
Nothing Env a
g Expr a
e1 Expr a
e2 = Expr a -> Expr a -> Bool
go Expr a
e1 (Expr a -> Env a -> Expr a
forall a. Expr a -> Env a -> Expr a
subst Expr a
e2 Env a
g)
  where
    go :: Expr a -> Expr a -> Bool
go Expr a
e1 Expr a
e2' = [Bool] -> Bool
forall (t :: * -> *). Foldable t => t Bool -> Bool
or [Expr a
e1' Expr a -> Expr a -> Bool
forall a. Eq a => a -> a -> Bool
== Expr a
e2' | Expr a
e1' <- Env a -> Expr a -> [Expr a]
forall a. Env a -> Expr a -> [Expr a]
etas Env a
g Expr a
e1]
isEtaaEq (Just NormCheck
Strong) Env a
g Expr a
e1 Expr a
e2 = (Env a -> Expr a -> Expr a -> Bool)
-> Env a -> Expr a -> Expr a -> Bool
forall a.
(Env a -> Expr a -> Expr a -> Bool)
-> Env a -> Expr a -> Expr a -> Bool
isEtaPEq Env a -> Expr a -> Expr a -> Bool
forall a. Env a -> Expr a -> Expr a -> Bool
isNormEq Env a
g Expr a
e1 Expr a
e2
isEtaaEq (Just NormCheck
Weak) Env a
g Expr a
e1 Expr a
e2 = (Env a -> Expr a -> Expr a -> Bool)
-> Env a -> Expr a -> Expr a -> Bool
forall a.
(Env a -> Expr a -> Expr a -> Bool)
-> Env a -> Expr a -> Expr a -> Bool
isEtaPEq Env a -> Expr a -> Expr a -> Bool
forall a. Env a -> Expr a -> Expr a -> Bool
isWnfEq Env a
g Expr a
e1 Expr a
e2
isEtaaEq (Just NormCheck
Head) Env a
g Expr a
e1 Expr a
e2 = (Env a -> Expr a -> Expr a -> Bool)
-> Env a -> Expr a -> Expr a -> Bool
forall a.
(Env a -> Expr a -> Expr a -> Bool)
-> Env a -> Expr a -> Expr a -> Bool
isEtaPEq Env a -> Expr a -> Expr a -> Bool
forall a. Env a -> Expr a -> Expr a -> Bool
isHnfEq Env a
g Expr a
e1 Expr a
e2

isUnEtaa :: Env a -> Expr a -> Expr a -> Bool
isUnEtaa :: forall a. Env a -> Expr a -> Expr a -> Bool
isUnEtaa Env a
g Expr a
e1 Expr a
e2 = Maybe NormCheck -> Env a -> Expr a -> Expr a -> Bool
forall a. Maybe NormCheck -> Env a -> Expr a -> Expr a -> Bool
isEtaaEq Maybe NormCheck
forall a. Maybe a
Nothing Env a
g Expr a
e2 Expr a
e1

-- Eta reduction, with provided normal form check
isEtaPEq :: (Env a -> Expr a -> Expr a -> Bool) -> Env a -> Expr a -> Expr a -> Bool
isEtaPEq :: forall a.
(Env a -> Expr a -> Expr a -> Bool)
-> Env a -> Expr a -> Expr a -> Bool
isEtaPEq Env a -> Expr a -> Expr a -> Bool
isNfEq Env a
g Expr a
e1 Expr a
e2 = [Bool] -> Bool
forall (t :: * -> *). Foldable t => t Bool -> Bool
or [Env a -> Expr a -> Expr a -> Bool
isNfEq Env a
g Expr a
e1' Expr a
e2 | Expr a
e1' <- Env a -> Expr a -> [Expr a]
forall a. Env a -> Expr a -> [Expr a]
etas Env a
g Expr a
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 :: forall a. Expr a -> Maybe (Expr a)
eta (ELam Bind a
x (EApp Expr a
e (EVar Id
x' a
_) a
_) a
_) =
  let zs :: HashSet Id
zs = Expr a -> HashSet Id
forall a. Expr a -> HashSet Id
freeVars Expr a
e in
  if (Bind a -> Id
forall a. Bind a -> Id
bindId Bind a
x Id -> Id -> Bool
forall a. Eq a => a -> a -> Bool
== Id
x') Bool -> Bool -> Bool
&& Bool -> Bool
not (Bind a -> HashSet Id -> Bool
forall a. Bind a -> HashSet Id -> Bool
isIn Bind a
x HashSet Id
zs)
    then
      Expr a -> Maybe (Expr a)
forall a. a -> Maybe a
Just Expr a
e
    else Maybe (Expr a)
forall a. Maybe a
Nothing
eta Expr a
_ = Maybe (Expr a)
forall a. Maybe a
Nothing

etas :: Env a -> Expr a -> [Expr a]
etas :: forall a. Env a -> Expr a -> [Expr a]
etas Env a
g Expr a
e = Expr a -> [Expr a]
forall a. Expr a -> [Expr a]
go (Expr a -> Env a -> Expr a
forall a. Expr a -> Env a -> Expr a
subst Expr a
e Env a
g)
  where
    go :: Expr a -> [Expr a]
go (EVar {})        = []
    -- Pattern where reduction might be possible
    go e' :: Expr a
e'@(ELam Bind a
b Expr a
e1 a
z) = Maybe (Expr a) -> [Expr a]
forall a. Maybe a -> [a]
Mb.maybeToList (Expr a -> Maybe (Expr a)
forall a. Expr a -> Maybe (Expr a)
eta Expr a
e')
                       [Expr a] -> [Expr a] -> [Expr a]
forall a. [a] -> [a] -> [a]
++ [Bind a -> Expr a -> a -> Expr a
forall a. Bind a -> Expr a -> a -> Expr a
ELam Bind a
b Expr a
e1' a
z | Expr a
e1' <- Expr a -> [Expr a]
go Expr a
e1]
    go (EApp Expr a
e1 Expr a
e2 a
z)   = [Expr a -> Expr a -> a -> Expr a
forall a. Expr a -> Expr a -> a -> Expr a
EApp Expr a
e1' Expr a
e2 a
z | Expr a
e1' <- Expr a -> [Expr a]
go Expr a
e1]
                       [Expr a] -> [Expr a] -> [Expr a]
forall a. [a] -> [a] -> [a]
++ [Expr a -> Expr a -> a -> Expr a
forall a. Expr a -> Expr a -> a -> Expr a
EApp Expr a
e1 Expr a
e2' a
z | Expr a
e2' <- Expr a -> [Expr a]
go Expr a
e2]

--------------------------------------------------------------------------------
-- | Evaluation to Normal Form
--------------------------------------------------------------------------------
-- Check if e1 is strong normal form
isNormEq :: Env a -> Expr a -> Expr a -> Bool
isNormEq :: forall a. Env a -> Expr a -> Expr a -> Bool
isNormEq Env a
g Expr a
e1 Expr a
e2 = (Expr a
e1' Expr a -> Expr a -> Bool
forall a. Eq a => a -> a -> Bool
== Expr a
e2') Bool -> Bool -> Bool
&& Expr a -> Value -> Bool
forall a. Expr a -> Value -> Bool
nEqVal Expr a
e2' (Expr a -> Value
forall {a}. Expr a -> Value
nf Expr a
e2')
  where
    e1' :: Expr a
e1' = Expr a -> Expr a
forall a. Expr a -> Expr a
alphaNormal (Expr a -> Expr a) -> Expr a -> Expr a
forall a b. (a -> b) -> a -> b
$ Expr a -> Env a -> Expr a
forall a. Expr a -> Env a -> Expr a
subst Expr a
e1 Env a
g
    e2' :: Expr a
e2' = Expr a -> Expr a
forall a. Expr a -> Expr a
alphaNormal (Expr a -> Expr a) -> Expr a -> Expr a
forall a b. (a -> b) -> a -> b
$ Expr a -> Env a -> Expr a
forall a. Expr a -> Env a -> Expr a
subst Expr a
e2 Env a
g
    nf :: Expr a -> Value
nf = HashMap Id Value -> Expr a -> Value
forall a. HashMap Id Value -> Expr a -> Value
evalNbE HashMap Id Value
forall k v. HashMap k v
ML.empty

toNormEq :: Env a -> Expr a -> Expr a -> Bool
toNormEq :: forall a. Env a -> Expr a -> Expr a -> Bool
toNormEq Env a
g Expr a
e1 Expr a
e2 = Expr a -> Value -> Bool
forall a. Expr a -> Value -> Bool
nEqVal (Expr a -> Env a -> Expr a
forall a. Expr a -> Env a -> Expr a
subst Expr a
e2 Env a
g) (Value -> Bool) -> Value -> Bool
forall a b. (a -> b) -> a -> b
$ HashMap Id Value -> Expr a -> Value
forall a. HashMap Id Value -> Expr a -> Value
evalNbE HashMap Id Value
forall k v. HashMap k v
ML.empty (Expr a -> Env a -> Expr a
forall a. Expr a -> Env a -> Expr a
subst Expr a
e1 Env a
g)

evalNbE :: ML.HashMap Id Value -> Expr a -> Value
evalNbE :: forall a. HashMap Id Value -> Expr a -> Value
evalNbE !HashMap Id Value
env Expr a
e = case Expr a
e of
  EVar Id
x a
_            -> Value -> Maybe Value -> Value
forall a. a -> Maybe a -> a
Mb.fromMaybe (Id -> [Value] -> Value
Neutral Id
x []) (Maybe Value -> Value) -> Maybe Value -> Value
forall a b. (a -> b) -> a -> b
$ Id -> HashMap Id Value -> Maybe Value
forall k v. (Eq k, Hashable k) => k -> HashMap k v -> Maybe v
ML.lookup Id
x HashMap Id Value
env
  ELam (Bind Id
x a
_) Expr a
b a
_ -> (Value -> Value) -> Value
Fun ((Value -> Value) -> Value) -> (Value -> Value) -> Value
forall a b. (a -> b) -> a -> b
$ \Value
val -> HashMap Id Value -> Expr a -> Value
forall a. HashMap Id Value -> Expr a -> Value
evalNbE (Id -> Value -> HashMap Id Value -> HashMap Id Value
forall k v.
(Eq k, Hashable k) =>
k -> v -> HashMap k v -> HashMap k v
ML.insert Id
x Value
val HashMap Id Value
env) Expr a
b
  EApp Expr a
f Expr a
arg a
_        -> case HashMap Id Value -> Expr a -> Value
forall a. HashMap Id Value -> Expr a -> Value
evalNbE HashMap Id Value
env Expr a
f of
    Fun Value -> Value
f' -> Value -> Value
f' (HashMap Id Value -> Expr a -> Value
forall a. HashMap Id Value -> Expr a -> Value
evalNbE HashMap Id Value
env Expr a
arg)
    Neutral Id
x [Value]
args -> Id -> [Value] -> Value
Neutral Id
x (HashMap Id Value -> Expr a -> Value
forall a. HashMap Id Value -> Expr a -> Value
evalNbE HashMap Id Value
env Expr a
argValue -> [Value] -> [Value]
forall a. a -> [a] -> [a]
:[Value]
args)

nEqVal :: Expr a -> Value -> Bool
nEqVal :: forall a. Expr a -> Value -> Bool
nEqVal (EVar Id
x a
_) (Neutral Id
x' [])
  = Id
x Id -> Id -> Bool
forall a. Eq a => a -> a -> Bool
== Id
x'
nEqVal (ELam (Bind Id
x a
_) Expr a
b a
_) (Fun Value -> Value
f)
  = Expr a -> Value -> Bool
forall a. Expr a -> Value -> Bool
nEqVal Expr a
b (Value -> Value
f (Id -> [Value] -> Value
Neutral Id
x []))
nEqVal (EApp Expr a
f Expr a
a a
_) (Neutral Id
x (Value
a':[Value]
args))
  = Expr a -> Value -> Bool
forall a. Expr a -> Value -> Bool
nEqVal Expr a
a Value
a' Bool -> Bool -> Bool
&& Expr a -> Value -> Bool
forall a. Expr a -> Value -> Bool
nEqVal Expr a
f (Id -> [Value] -> Value
Neutral Id
x [Value]
args)
nEqVal Expr a
_ Value
_ = Bool
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 :: forall a. Env a -> Expr a -> Expr a -> Bool
isWnfEq Env a
g Expr a
e1 Expr a
e2 = (Expr a
e1' Expr a -> Expr a -> Bool
forall a. Eq a => a -> a -> Bool
== Expr a
e2') Bool -> Bool -> Bool
&& (Expr a
e2' Expr a -> Expr a -> Bool
forall a. Eq a => a -> a -> Bool
== Expr a -> Expr a
forall a. Expr a -> Expr a
wnf Expr a
e2')
  where
    e1' :: Expr a
e1' = Expr a -> Expr a
forall a. Expr a -> Expr a
alphaNormal (Expr a -> Expr a) -> Expr a -> Expr a
forall a b. (a -> b) -> a -> b
$ Expr a -> Env a -> Expr a
forall a. Expr a -> Env a -> Expr a
subst Expr a
e1 Env a
g
    e2' :: Expr a
e2' = Expr a -> Expr a
forall a. Expr a -> Expr a
alphaNormal (Expr a -> Expr a) -> Expr a -> Expr a
forall a b. (a -> b) -> a -> b
$ Expr a -> Env a -> Expr a
forall a. Expr a -> Env a -> Expr a
subst Expr a
e2 Env a
g
    wnf :: Expr a -> Expr a
    wnf :: forall a. Expr a -> Expr a
wnf e :: Expr a
e@(EVar {}) = Expr a
e
    wnf e :: Expr a
e@(ELam {}) = Expr a
e
    wnf (EApp Expr a
f Expr a
arg a
l) = case Expr a -> Expr a
forall a. Expr a -> Expr a
wnf Expr a
f of
      f' :: Expr a
f'@ELam {} -> Expr a -> (Expr a -> Expr a) -> Maybe (Expr a) -> Expr a
forall b a. b -> (a -> b) -> Maybe a -> b
maybe (Expr a -> Expr a -> a -> Expr a
forall a. Expr a -> Expr a -> a -> Expr a
EApp Expr a
f' (Expr a -> Expr a
forall a. Expr a -> Expr a
wnf Expr a
arg) a
l) Expr a -> Expr a
forall a. Expr a -> Expr a
wnf (Expr a -> Expr a -> Maybe (Expr a)
forall a. Expr a -> Expr a -> Maybe (Expr a)
beta Expr a
f (Expr a -> Maybe (Expr a)) -> Expr a -> Maybe (Expr a)
forall a b. (a -> b) -> a -> b
$ Expr a -> Expr a
forall a. Expr a -> Expr a
wnf Expr a
arg)
      Expr a
f' -> Expr a -> Expr a -> a -> Expr a
forall a. Expr a -> Expr a -> a -> Expr a
EApp Expr a
f' (Expr a -> Expr a
forall a. Expr a -> Expr a
wnf Expr a
arg) a
l

--------------------------------------------------------------------------------
-- | Evaluation to Head Normal Form
--------------------------------------------------------------------------------
isHnfEq :: Env a -> Expr a -> Expr a -> Bool
isHnfEq :: forall a. Env a -> Expr a -> Expr a -> Bool
isHnfEq Env a
g Expr a
e1 Expr a
e2 = (Expr a
e1' Expr a -> Expr a -> Bool
forall a. Eq a => a -> a -> Bool
== Expr a
e2') Bool -> Bool -> Bool
&& (Expr a
e2' Expr a -> Expr a -> Bool
forall a. Eq a => a -> a -> Bool
== Expr a -> Expr a
forall a. Expr a -> Expr a
hnf Expr a
e2')
  where
    e1' :: Expr a
e1' = Expr a -> Expr a
forall a. Expr a -> Expr a
alphaNormal (Expr a -> Expr a) -> Expr a -> Expr a
forall a b. (a -> b) -> a -> b
$ Expr a -> Env a -> Expr a
forall a. Expr a -> Env a -> Expr a
subst Expr a
e1 Env a
g
    e2' :: Expr a
e2' = Expr a -> Expr a
forall a. Expr a -> Expr a
alphaNormal (Expr a -> Expr a) -> Expr a -> Expr a
forall a b. (a -> b) -> a -> b
$ Expr a -> Env a -> Expr a
forall a. Expr a -> Env a -> Expr a
subst Expr a
e2 Env a
g
    hnf :: Expr a -> Expr a
    hnf :: forall a. Expr a -> Expr a
hnf e :: Expr a
e@(EVar {}) = Expr a
e
    hnf (ELam Bind a
bi Expr a
b a
a) = Bind a -> Expr a -> a -> Expr a
forall a. Bind a -> Expr a -> a -> Expr a
ELam Bind a
bi (Expr a -> Expr a
forall a. Expr a -> Expr a
hnf Expr a
b) a
a
    hnf (EApp Expr a
f Expr a
arg a
l) = case Expr a -> Expr a
forall a. Expr a -> Expr a
hnf Expr a
f of
      f' :: Expr a
f'@ELam {} -> Expr a -> (Expr a -> Expr a) -> Maybe (Expr a) -> Expr a
forall b a. b -> (a -> b) -> Maybe a -> b
maybe (Expr a -> Expr a -> a -> Expr a
forall a. Expr a -> Expr a -> a -> Expr a
EApp Expr a
f' (Expr a -> Expr a
forall a. Expr a -> Expr a
hnf Expr a
arg) a
l) Expr a -> Expr a
forall a. Expr a -> Expr a
hnf (Expr a -> Expr a -> Maybe (Expr a)
forall a. Expr a -> Expr a -> Maybe (Expr a)
beta Expr a
f' Expr a
arg)
      Expr a
f' -> Expr a -> Expr a -> a -> Expr a
forall a. Expr a -> Expr a -> a -> Expr a
EApp Expr a
f' Expr a
arg a
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
freeVars :: forall a. Expr a -> HashSet Id
freeVars = [Id] -> HashSet Id
forall a. (Eq a, Hashable a) => [a] -> HashSet a
S.fromList ([Id] -> HashSet Id) -> (Expr a -> [Id]) -> Expr a -> HashSet Id
forall b c a. (b -> c) -> (a -> b) -> a -> c
. HashMap Id a -> [Id]
forall k v. HashMap k v -> [k]
M.keys (HashMap Id a -> [Id])
-> (Expr a -> HashMap Id a) -> Expr a -> [Id]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Expr a -> HashMap Id a
forall a. Expr a -> HashMap Id a
freeVars'

freeVars' :: Expr a -> M.HashMap Id a
freeVars' :: forall a. Expr a -> HashMap Id a
freeVars' (EVar Id
x a
l)    = Id -> a -> HashMap Id a
forall k v. Hashable k => k -> v -> HashMap k v
M.singleton Id
x a
l
freeVars' (ELam Bind a
b Expr a
e a
_)  = Id -> HashMap Id a -> HashMap Id a
forall k v. (Eq k, Hashable k) => k -> HashMap k v -> HashMap k v
M.delete (Bind a -> Id
forall a. Bind a -> Id
bindId Bind a
b)    (Expr a -> HashMap Id a
forall a. Expr a -> HashMap Id a
freeVars' Expr a
e)
freeVars' (EApp Expr a
e Expr a
e' a
_) = HashMap Id a -> HashMap Id a -> HashMap Id a
forall k v. Eq k => HashMap k v -> HashMap k v -> HashMap k v
M.union  (Expr a -> HashMap Id a
forall a. Expr a -> HashMap Id a
freeVars' Expr a
e) (Expr a -> HashMap Id a
forall a. Expr a -> HashMap Id a
freeVars' Expr a
e')

subst :: Expr a -> Env a -> Expr a
subst :: forall a. Expr a -> Env a -> Expr a
subst e :: Expr a
e@(EVar Id
v a
_)   Env a
su = Expr a -> Id -> Env a -> Expr a
forall k v. (Eq k, Hashable k) => v -> k -> HashMap k v -> v
M.lookupDefault Expr a
e Id
v Env a
su
subst (EApp Expr a
e1 Expr a
e2 a
z) Env a
su = Expr a -> Expr a -> a -> Expr a
forall a. Expr a -> Expr a -> a -> Expr a
EApp (Expr a -> Env a -> Expr a
forall a. Expr a -> Env a -> Expr a
subst Expr a
e1 Env a
su) (Expr a -> Env a -> Expr a
forall a. Expr a -> Env a -> Expr a
subst Expr a
e2 Env a
su) a
z
subst (ELam Bind a
b Expr a
e a
z)   Env a
su = Bind a -> Expr a -> a -> Expr a
forall a. Bind a -> Expr a -> a -> Expr a
ELam Bind a
b (Expr a -> Env a -> Expr a
forall a. Expr a -> Env a -> Expr a
subst Expr a
e Env a
su') a
z
  where
    su' :: Env a
su'                 = Id -> Env a -> Env a
forall k v. (Eq k, Hashable k) => k -> HashMap k v -> HashMap k v
M.delete (Bind a -> Id
forall a. Bind a -> Id
bindId Bind a
b) Env a
su

canon :: Env a -> Expr a -> Expr  a
canon :: forall a. Env a -> Expr a -> Expr a
canon Env a
g = Expr a -> Expr a
forall a. Expr a -> Expr a
alphaNormal (Expr a -> Expr a) -> (Expr a -> Expr a) -> Expr a -> Expr a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Expr a -> Env a -> Expr a
forall a. Expr a -> Env a -> Expr a
`subst` Env a
g)

isEquiv :: Env a -> Expr a -> Expr a -> Bool
isEquiv :: forall a. Env a -> Expr a -> Expr a -> Bool
isEquiv Env a
g Expr a
e1 Expr a
e2 = Maybe NormCheck -> Env a -> Expr a -> Expr a -> Bool
forall a. Maybe NormCheck -> Env a -> Expr a -> Expr a -> Bool
isAlphEq Maybe NormCheck
forall a. Maybe a
Nothing Env a
g (Expr a -> Env a -> Expr a
forall a. Expr a -> Env a -> Expr a
subst Expr a
e1 Env a
g) (Expr a -> Env a -> Expr a
forall a. Expr a -> Env a -> Expr a
subst Expr a
e2 Env a
g)
--------------------------------------------------------------------------------
-- | Error Cases
--------------------------------------------------------------------------------

errInvalid :: Bind a -> Expr a -> Eqn a -> Expr a -> Result a
errInvalid :: forall a. Bind a -> Expr a -> Eqn a -> Expr a -> Result a
errInvalid Bind a
b Expr a
_ Eqn a
eqn Expr a
_ = Bind a -> a -> Result a
forall a. Bind a -> a -> Result a
Invalid Bind a
b (Eqn a -> a
forall a. Eqn a -> a
forall (t :: * -> *) a. Tagged t => t a -> a
tag Eqn a
eqn)

errPartial :: Bind a -> Expr a -> Result a
errPartial :: forall a. Bind a -> Expr a -> Result a
errPartial Bind a
b Expr a
e = Bind a -> a -> Result a
forall a. Bind a -> a -> Result a
Partial Bind a
b (Expr a -> a
forall a. Expr a -> a
forall (t :: * -> *) a. Tagged t => t a -> a
tag Expr a
e)

errDupDefn :: Bind a -> Result a
errDupDefn :: forall a. Bind a -> Result a
errDupDefn Bind a
b = Bind a -> a -> Result a
forall a. Bind a -> a -> Result a
DupDefn Bind a
b (Bind a -> a
forall a. Bind a -> a
forall (t :: * -> *) a. Tagged t => t a -> a
tag Bind a
b)

errDupEval :: Bind a -> Result a
errDupEval :: forall a. Bind a -> Result a
errDupEval Bind a
b = Bind a -> a -> Result a
forall a. Bind a -> a -> Result a
DupEval Bind a
b (Bind a -> a
forall a. Bind a -> a
forall (t :: * -> *) a. Tagged t => t a -> a
tag Bind a
b)