{-# LANGUAGE OverloadedStrings, BangPatterns #-}

module Language.Elsa.Eval (elsa, elsaOn) where

import qualified Data.HashMap.Strict  as M
import qualified Data.HashMap.Lazy    as ML
import qualified Data.HashSet         as S
import qualified Data.List            as L
import           Control.Monad.State
import qualified Data.Maybe           as Mb -- (isJust, maybeToList)
import           Language.Elsa.Types
import           Language.Elsa.Utils  (qPushes, qInit, qPop, fromEither)

--------------------------------------------------------------------------------
elsa :: Elsa a -> [Result a]
--------------------------------------------------------------------------------
elsa :: forall a. Elsa a -> [Result a]
elsa = forall a. (Id -> Bool) -> Elsa a -> [Result a]
elsaOn (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 forall a. [Defn a] -> CheckM a (Env a)
mkEnv (forall a. Elsa a -> [Defn a]
defns Elsa a
p) of
    Left Result a
err -> [Result a
err]
    Right Env a
g  -> case forall a. [Eval a] -> CheckM a (HashSet Id)
checkDupEval (forall a. Elsa a -> [Eval a]
evals Elsa a
p) of
      Left Result a
err -> [Result a
err]
      Right HashSet Id
_  -> [forall a. Env a -> Eval a -> Result a
result Env a
g Eval a
e | Eval a
e <- forall a. Elsa a -> [Eval a]
evals Elsa a
p, forall {a}. Eval a -> Bool
check Eval a
e ]
  where
    check :: Eval a -> Bool
check = Id -> Bool
cond forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Bind a -> Id
bindId forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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 = forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldM forall a. HashSet Id -> Eval a -> CheckM a (HashSet Id)
addEvalId 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 forall a. (Eq a, Hashable a) => a -> HashSet a -> Bool
S.member (forall a. Bind a -> Id
bindId Bind a
b) HashSet Id
s
    then forall a b. a -> Either a b
Left  (forall a. Bind a -> Result a
errDupEval Bind a
b)
    else forall a b. b -> Either a b
Right (forall a. (Eq a, Hashable a) => a -> HashSet a -> HashSet a
S.insert (forall a. Bind a -> Id
bindId Bind a
b) HashSet Id
s)
  where
    b :: Bind a
b = 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 = forall a. Either a a -> a
fromEither (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 = forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldM forall a. Env a -> Defn a -> CheckM a (Env a)
expand 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 forall a b. a -> Either a b
Left (forall a. Bind a -> Result a
errDupDefn Bind a
b)
    else case [(Id, a)]
zs of
      (Id
x,a
l) : [(Id, a)]
_ -> forall a b. a -> Either a b
Left  (forall a. Bind a -> Id -> a -> Result a
Unbound Bind a
b Id
x a
l)
      []        -> forall a b. b -> Either a b
Right (forall k v.
(Eq k, Hashable k) =>
k -> v -> HashMap k v -> HashMap k v
M.insert (forall a. Bind a -> Id
bindId Bind a
b) Expr a
e' Env a
g)
  where
    dupId :: Bool
dupId           = forall k a. (Eq k, Hashable k) => k -> HashMap k a -> Bool
M.member (forall a. Bind a -> Id
bindId Bind a
b) Env a
g
    e' :: Expr a
e'              = forall a. Expr a -> Env a -> Expr a
subst Expr a
e Env a
g
    zs :: [(Id, a)]
zs              = forall k v. HashMap k v -> [(k, v)]
M.toList (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 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 []
      | forall a. Env a -> Expr a -> Bool
isNormal Env a
g Expr a
e    = forall (m :: * -> *) a. Monad m => a -> m a
return (forall a. Bind a -> Result a
OK Bind a
n)
      | Bool
otherwise       = forall a b. a -> Either a b
Left (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)      = 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 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)

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')
  | forall a. Eqn a -> Env a -> Expr a -> Expr a -> Bool
isEq Eqn a
k Env a
g Expr a
e Expr a
e' = forall (m :: * -> *) a. Monad m => a -> m a
return Expr a
e'
  | Bool
otherwise     = forall a b. a -> Either a b
Left (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 (AlphEq a
_) = forall a. Env a -> Expr a -> Expr a -> Bool
isAlphEq
isEq (BetaEq a
_) = forall a. Env a -> Expr a -> Expr a -> Bool
isBetaEq
isEq (UnBeta a
_) = forall a. Env a -> Expr a -> Expr a -> Bool
isUnBeta
isEq (DefnEq a
_) = forall a. Env a -> Expr a -> Expr a -> Bool
isDefnEq
isEq (TrnsEq a
_) = forall a. Env a -> Expr a -> Expr a -> Bool
isTrnsEq
isEq (UnTrEq a
_) = forall a. Env a -> Expr a -> Expr a -> Bool
isUnTrEq
isEq (NormEq a
_) = forall a. Env a -> Expr a -> Expr a -> Bool
isNormEq


--------------------------------------------------------------------------------
-- | Transitive Reachability
--------------------------------------------------------------------------------
isTrnsEq :: Env a -> Expr a -> Expr a -> Bool
isTrnsEq :: forall a. Env a -> Expr a -> Expr a -> Bool
isTrnsEq Env a
g Expr a
e1 Expr a
e2 = forall a. Maybe a -> Bool
Mb.isJust (forall a. (Expr a -> Bool) -> Expr a -> Maybe (Expr a)
findTrans (forall a. Env a -> Expr a -> Expr a -> Bool
isEquiv Env a
g Expr a
e2) (forall a. Env a -> Expr a -> Expr a
canon Env a
g Expr a
e1))

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 = forall a. Env a -> Expr a -> Expr a -> Bool
isTrnsEq 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 forall a. HashSet a
S.empty (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') <- forall a. Queue a -> Maybe (a, Queue a)
qPop Queue (Expr a)
q
      if 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 forall (m :: * -> *) a. Monad m => a -> m a
return Expr a
e
             else HashSet (Expr a) -> Queue (Expr a) -> Maybe (Expr a)
go (forall a. (Eq a, Hashable a) => a -> HashSet a -> HashSet a
S.insert Expr a
e HashSet (Expr a)
seen) (forall a. Queue a -> [a] -> Queue a
qPushes Queue (Expr a)
q (forall a. Expr a -> [Expr a]
betas Expr a
e))

--------------------------------------------------------------------------------
-- | Definition Equivalence
--------------------------------------------------------------------------------
isDefnEq :: Env a -> Expr a -> Expr a -> Bool
isDefnEq :: forall a. Env a -> Expr a -> Expr a -> Bool
isDefnEq Env a
g Expr a
e1 Expr a
e2 = forall a. Expr a -> Env a -> Expr a
subst Expr a
e1 Env a
g forall a. Eq a => a -> a -> Bool
== forall a. Expr a -> Env a -> Expr a
subst Expr a
e2 Env a
g

--------------------------------------------------------------------------------
-- | Alpha Equivalence
--------------------------------------------------------------------------------
isAlphEq :: Env a -> Expr a -> Expr a -> Bool
isAlphEq :: forall a. Env a -> Expr a -> Expr a -> Bool
isAlphEq Env a
_ Expr a
e1 Expr a
e2 = forall a. Expr a -> Expr a
alphaNormal Expr a
e1 forall a. Eq a => a -> a -> Bool
== forall a. Expr a -> Expr a
alphaNormal Expr a
e2

alphaNormal :: Expr a -> Expr a
alphaNormal :: forall a. Expr a -> Expr a
alphaNormal = 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 = forall s a. State s a -> s -> a
evalState (forall a. HashMap Id Id -> Expr a -> AlphaM (Expr a)
normalize 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) =
  forall (m :: * -> *) a. Monad m => a -> m a
return (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' <- forall a. HashMap Id Id -> Expr a -> AlphaM (Expr a)
normalize HashMap Id Id
g Expr a
e1
  Expr a
e2' <- forall a. HashMap Id Id -> Expr a -> AlphaM (Expr a)
normalize HashMap Id Id
g Expr a
e2
  forall (m :: * -> *) a. Monad m => a -> m a
return (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' = 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'    <- forall a. HashMap Id Id -> Expr a -> AlphaM (Expr a)
normalize HashMap Id Id
g' Expr a
e
  forall (m :: * -> *) a. Monad m => a -> m a
return (forall a. Bind a -> Expr a -> a -> Expr a
ELam (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 = 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 <- forall s (m :: * -> *). MonadState s m => m s
get
  forall s (m :: * -> *). MonadState s m => s -> m ()
put (Int
n forall a. Num a => a -> a -> a
+ Int
1)
  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 forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> Id
show Int
n

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

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

--------------------------------------------------------------------------------
-- | Beta Reduction
--------------------------------------------------------------------------------
isBetaEq :: Env a -> Expr a -> Expr a -> Bool
isBetaEq :: forall a. Env a -> Expr a -> Expr a -> Bool
isBetaEq Env a
_ Expr a
e1 Expr a
e2 = forall (t :: * -> *). Foldable t => t Bool -> Bool
or [ Expr a
e1' forall a. Eq a => a -> a -> Bool
== Expr a
e2  | Expr a
e1' <- forall a. Expr a -> [Expr a]
betas Expr a
e1 ]

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 = forall a. Env a -> Expr a -> Expr a -> Bool
isBetaEq Env a
g Expr a
e2 Expr a
e1

isNormal :: Env a -> Expr a -> Bool
isNormal :: forall a. Env a -> Expr a -> Bool
isNormal Env a
g = forall (t :: * -> *) a. Foldable t => t a -> Bool
null forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Expr a -> [Expr a]
betas forall b c a. (b -> c) -> (a -> b) -> a -> c
. (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)   = [ forall a. Bind a -> Expr a -> a -> Expr a
ELam Bind a
b Expr a
e' a
z | Expr a
e' <- forall a. Expr a -> [Expr a]
betas Expr a
e ]
betas (EApp Expr a
e1 Expr a
e2 a
z) = [ forall a. Expr a -> Expr a -> a -> Expr a
EApp Expr a
e1' Expr a
e2 a
z | Expr a
e1' <- forall a. Expr a -> [Expr a]
betas Expr a
e1 ]
                    forall a. [a] -> [a] -> [a]
++ [ forall a. Expr a -> Expr a -> a -> Expr a
EApp Expr a
e1 Expr a
e2' a
z | Expr a
e2' <- forall a. Expr a -> [Expr a]
betas Expr a
e2 ]
                    forall a. [a] -> [a] -> [a]
++ forall a. Maybe a -> [a]
Mb.maybeToList (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' = forall a. Expr a -> Id -> Expr a -> Maybe (Expr a)
substCA Expr a
e Id
x Expr a
e'
beta Expr a
_                    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                   = forall a. Expr a -> HashSet Id
freeVars Expr a
e'
    bnd :: [Bind a] -> HashSet Id -> Bool
bnd  [Bind a]
bs HashSet Id
zs           = forall (t :: * -> *). Foldable t => t Bool -> Bool
or [ Bind a
b 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 forall a. Eq a => a -> a -> Bool
/= Id
x           = forall a. a -> Maybe a
Just Expr a
e            -- different var, no subst
      | forall {a}. [Bind a] -> HashSet Id -> Bool
bnd  [Bind a]
bs HashSet Id
zs       = forall a. Maybe a
Nothing           -- same var, but free-var-captured
      | Bool
otherwise        = 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
                              forall a. a -> Maybe a
Just (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 forall a. Eq a => a -> a -> Bool
== forall a. Bind a -> Id
bindId Bind a
b    = 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
bforall a. a -> [a] -> [a]
:[Bind a]
bs) Expr a
e1
                              forall a. a -> Maybe a
Just (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 = forall a. (Eq a, Hashable a) => a -> HashSet a -> Bool
S.member forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Bind a -> Id
bindId

--------------------------------------------------------------------------------
-- | Evaluation to 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 = forall {a}. Expr a -> Value -> Bool
eqVal (forall a. Expr a -> Env a -> Expr a
subst Expr a
e2 Env a
g) forall a b. (a -> b) -> a -> b
$ forall {a}. HashMap Id Value -> Expr a -> Value
evalNbE forall k v. HashMap k v
ML.empty (forall a. Expr a -> Env a -> Expr a
subst Expr a
e1 Env a
g)
  where
    evalNbE :: HashMap Id Value -> Expr a -> Value
evalNbE !HashMap Id Value
env Expr a
e = case Expr a
e of
      EVar Id
x a
_            -> forall a. a -> Maybe a -> a
Mb.fromMaybe (Id -> [Value] -> Value
Neutral Id
x []) forall a b. (a -> b) -> a -> b
$ 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 forall a b. (a -> b) -> a -> b
$ \Value
val -> HashMap Id Value -> Expr a -> Value
evalNbE (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
evalNbE HashMap Id Value
env Expr a
f of
        Fun Value -> Value
f' -> Value -> Value
f' (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
evalNbE HashMap Id Value
env Expr a
argforall a. a -> [a] -> [a]
:[Value]
args)

    eqVal :: Expr a -> Value -> Bool
eqVal (EVar Id
x a
_) (Neutral Id
x' [])
      = Id
x forall a. Eq a => a -> a -> Bool
== Id
x'
    eqVal (ELam (Bind Id
x a
_) Expr a
b a
_) (Fun Value -> Value
f)
      = Expr a -> Value -> Bool
eqVal Expr a
b (Value -> Value
f (Id -> [Value] -> Value
Neutral Id
x []))
    eqVal (EApp Expr a
f Expr a
a a
_) (Neutral Id
x (Value
a':[Value]
args))
      = Expr a -> Value -> Bool
eqVal Expr a
a Value
a' Bool -> Bool -> Bool
&& Expr a -> Value -> Bool
eqVal Expr a
f (Id -> [Value] -> Value
Neutral Id
x [Value]
args)
    eqVal Expr a
_ Value
_ = Bool
False

-- | NbE semantic domain
data Value = Fun !(Value -> Value) | Neutral !Id ![Value]

--------------------------------------------------------------------------------
-- | General Helpers
--------------------------------------------------------------------------------
freeVars :: Expr a -> S.HashSet Id
freeVars :: forall a. Expr a -> HashSet Id
freeVars = forall a. (Eq a, Hashable a) => [a] -> HashSet a
S.fromList forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall k v. HashMap k v -> [k]
M.keys forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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)    = 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
_)  = forall k v. (Eq k, Hashable k) => k -> HashMap k v -> HashMap k v
M.delete (forall a. Bind a -> Id
bindId Bind a
b)    (forall a. Expr a -> HashMap Id a
freeVars' Expr a
e)
freeVars' (EApp Expr a
e Expr a
e' a
_) = forall k v.
(Eq k, Hashable k) =>
HashMap k v -> HashMap k v -> HashMap k v
M.union  (forall a. Expr a -> HashMap Id a
freeVars' Expr a
e) (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 = 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 = forall a. Expr a -> Expr a -> a -> Expr a
EApp (forall a. Expr a -> Env a -> Expr a
subst Expr a
e1 Env a
su) (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 = forall a. Bind a -> Expr a -> a -> Expr a
ELam Bind a
b (forall a. Expr a -> Env a -> Expr a
subst Expr a
e Env a
su') a
z
  where
    su' :: Env a
su'                 = forall k v. (Eq k, Hashable k) => k -> HashMap k v -> HashMap k v
M.delete (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 = forall a. Expr a -> Expr a
alphaNormal forall b c a. (b -> c) -> (a -> b) -> a -> c
. (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 = forall a. Env a -> Expr a -> Expr a -> Bool
isAlphEq Env a
g (forall a. Expr a -> Env a -> Expr a
subst Expr a
e1 Env a
g) (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
_ = forall a. Bind a -> a -> Result a
Invalid Bind a
b (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 = forall a. Bind a -> a -> Result a
Partial Bind a
b (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 = forall a. Bind a -> a -> Result a
DupDefn Bind a
b (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 = forall a. Bind a -> a -> Result a
DupEval Bind a
b (forall (t :: * -> *) a. Tagged t => t a -> a
tag Bind a
b)