{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE DeriveGeneric     #-}
{-# LANGUAGE DeriveFunctor     #-}
{-# LANGUAGE InstanceSigs #-}

module Language.Elsa.Types where

import           GHC.Generics
import           Text.Printf (printf)
import           Language.Elsa.UX
import           Data.Maybe (mapMaybe)
import           Data.Hashable

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
--------------------------------------------------------------------------------

data Result a
  = OK      (Bind a)
  | Partial (Bind a)    a
  | Invalid (Bind a)    a
  | Unbound (Bind a) Id a
  | DupDefn (Bind a)    a
  | DupEval (Bind a)    a
  deriving (Result a -> Result a -> Bool
(Result a -> Result a -> Bool)
-> (Result a -> Result a -> Bool) -> Eq (Result a)
forall a. Eq a => Result a -> Result a -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: forall a. Eq a => Result a -> Result a -> Bool
== :: Result a -> Result a -> Bool
$c/= :: forall a. Eq a => Result a -> Result a -> Bool
/= :: Result a -> Result a -> Bool
Eq, Int -> Result a -> ShowS
[Result a] -> ShowS
Result a -> Id
(Int -> Result a -> ShowS)
-> (Result a -> Id) -> ([Result a] -> ShowS) -> Show (Result a)
forall a. Show a => Int -> Result a -> ShowS
forall a. Show a => [Result a] -> ShowS
forall a. Show a => Result a -> Id
forall a.
(Int -> a -> ShowS) -> (a -> Id) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: forall a. Show a => Int -> Result a -> ShowS
showsPrec :: Int -> Result a -> ShowS
$cshow :: forall a. Show a => Result a -> Id
show :: Result a -> Id
$cshowList :: forall a. Show a => [Result a] -> ShowS
showList :: [Result a] -> ShowS
Show, (forall a b. (a -> b) -> Result a -> Result b)
-> (forall a b. a -> Result b -> Result a) -> Functor Result
forall a b. a -> Result b -> Result a
forall a b. (a -> b) -> Result a -> Result b
forall (f :: * -> *).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
$cfmap :: forall a b. (a -> b) -> Result a -> Result b
fmap :: forall a b. (a -> b) -> Result a -> Result b
$c<$ :: forall a b. a -> Result b -> Result a
<$ :: forall a b. a -> Result b -> Result a
Functor)

failures :: [Result a] -> [Id]
failures :: forall a. [Result a] -> [Id]
failures = (Result a -> Maybe Id) -> [Result a] -> [Id]
forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe Result a -> Maybe Id
forall {a}. Result a -> Maybe Id
go
  where
    go :: Result a -> Maybe Id
go (Partial Bind a
b a
_)   = Id -> Maybe Id
forall a. a -> Maybe a
Just (Bind a -> Id
forall a. Bind a -> Id
bindId Bind a
b)
    go (Invalid Bind a
b a
_)   = Id -> Maybe Id
forall a. a -> Maybe a
Just (Bind a -> Id
forall a. Bind a -> Id
bindId Bind a
b)
    go (Unbound Bind a
b Id
_ a
_) = Id -> Maybe Id
forall a. a -> Maybe a
Just (Bind a -> Id
forall a. Bind a -> Id
bindId Bind a
b)
    go (DupDefn Bind a
b a
_)   = Id -> Maybe Id
forall a. a -> Maybe a
Just (Bind a -> Id
forall a. Bind a -> Id
bindId Bind a
b)
    go (DupEval Bind a
b a
_)   = Id -> Maybe Id
forall a. a -> Maybe a
Just (Bind a -> Id
forall a. Bind a -> Id
bindId Bind a
b)
    go Result a
_               = Maybe Id
forall a. Maybe a
Nothing

successes :: [Result a] -> [Id]
successes :: forall a. [Result a] -> [Id]
successes = (Result a -> Maybe Id) -> [Result a] -> [Id]
forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe Result a -> Maybe Id
forall {a}. Result a -> Maybe Id
go
  where
    go :: Result a -> Maybe Id
go (OK Bind a
b) = Id -> Maybe Id
forall a. a -> Maybe a
Just (Bind a -> Id
forall a. Bind a -> Id
bindId Bind a
b)
    go Result a
_      = Maybe Id
forall a. Maybe a
Nothing

resultError :: (Located a) => Result a -> Maybe UserError
resultError :: forall a. Located a => Result a -> Maybe UserError
resultError (Partial Bind a
b a
l)   = a -> Id -> Maybe UserError
forall a. Located a => a -> Id -> Maybe UserError
mkErr a
l (Bind a -> Id
forall a. Bind a -> Id
bindId Bind a
b Id -> ShowS
forall a. [a] -> [a] -> [a]
++ Id
" can be further reduced!")
resultError (Invalid Bind a
b a
l)   = a -> Id -> Maybe UserError
forall a. Located a => a -> Id -> Maybe UserError
mkErr a
l (Bind a -> Id
forall a. Bind a -> Id
bindId Bind a
b Id -> ShowS
forall a. [a] -> [a] -> [a]
++ Id
" has an invalid reduction!")
resultError (Unbound Bind a
b Id
x a
l) = a -> Id -> Maybe UserError
forall a. Located a => a -> Id -> Maybe UserError
mkErr a
l (Bind a -> Id
forall a. Bind a -> Id
bindId Bind a
b Id -> ShowS
forall a. [a] -> [a] -> [a]
++ Id
" has an unbound variable " Id -> ShowS
forall a. [a] -> [a] -> [a]
++ Id
x )
resultError (DupDefn Bind a
b a
l)   = a -> Id -> Maybe UserError
forall a. Located a => a -> Id -> Maybe UserError
mkErr a
l (Id
"Definition " Id -> ShowS
forall a. [a] -> [a] -> [a]
++ (Bind a -> Id
forall a. Bind a -> Id
bindId Bind a
b) Id -> ShowS
forall a. [a] -> [a] -> [a]
++ Id
" has already been declared")
resultError (DupEval Bind a
b a
l)   = a -> Id -> Maybe UserError
forall a. Located a => a -> Id -> Maybe UserError
mkErr a
l (Id
"Evaluation " Id -> ShowS
forall a. [a] -> [a] -> [a]
++ (Bind a -> Id
forall a. Bind a -> Id
bindId Bind a
b) Id -> ShowS
forall a. [a] -> [a] -> [a]
++ Id
" has already been declared")
resultError Result a
_               = Maybe UserError
forall a. Maybe a
Nothing

mkErr :: (Located a) => a -> Text -> Maybe UserError
mkErr :: forall a. Located a => a -> Id -> Maybe UserError
mkErr a
l Id
msg = UserError -> Maybe UserError
forall a. a -> Maybe a
Just (Id -> SourceSpan -> UserError
mkError Id
msg (a -> SourceSpan
forall a. Located a => a -> SourceSpan
sourceSpan a
l))

--------------------------------------------------------------------------------
-- | Programs
--------------------------------------------------------------------------------
data ElsaItem a = DefnItem (Defn a) | EvalItem (Eval a)

data Elsa a = Elsa
  { forall a. Elsa a -> [Defn a]
defns :: [Defn a]
  , forall a. Elsa a -> [Eval a]
evals :: [Eval a]
  }
  deriving (Elsa a -> Elsa a -> Bool
(Elsa a -> Elsa a -> Bool)
-> (Elsa a -> Elsa a -> Bool) -> Eq (Elsa a)
forall a. Eq a => Elsa a -> Elsa a -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: forall a. Eq a => Elsa a -> Elsa a -> Bool
== :: Elsa a -> Elsa a -> Bool
$c/= :: forall a. Eq a => Elsa a -> Elsa a -> Bool
/= :: Elsa a -> Elsa a -> Bool
Eq, Int -> Elsa a -> ShowS
[Elsa a] -> ShowS
Elsa a -> Id
(Int -> Elsa a -> ShowS)
-> (Elsa a -> Id) -> ([Elsa a] -> ShowS) -> Show (Elsa a)
forall a. Show a => Int -> Elsa a -> ShowS
forall a. Show a => [Elsa a] -> ShowS
forall a. Show a => Elsa a -> Id
forall a.
(Int -> a -> ShowS) -> (a -> Id) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: forall a. Show a => Int -> Elsa a -> ShowS
showsPrec :: Int -> Elsa a -> ShowS
$cshow :: forall a. Show a => Elsa a -> Id
show :: Elsa a -> Id
$cshowList :: forall a. Show a => [Elsa a] -> ShowS
showList :: [Elsa a] -> ShowS
Show)

data Defn a
  = Defn !(Bind a) !(Expr a)
  deriving (Defn a -> Defn a -> Bool
(Defn a -> Defn a -> Bool)
-> (Defn a -> Defn a -> Bool) -> Eq (Defn a)
forall a. Defn a -> Defn a -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: forall a. Defn a -> Defn a -> Bool
== :: Defn a -> Defn a -> Bool
$c/= :: forall a. Defn a -> Defn a -> Bool
/= :: Defn a -> Defn a -> Bool
Eq, Int -> Defn a -> ShowS
[Defn a] -> ShowS
Defn a -> Id
(Int -> Defn a -> ShowS)
-> (Defn a -> Id) -> ([Defn a] -> ShowS) -> Show (Defn a)
forall a. Show a => Int -> Defn a -> ShowS
forall a. Show a => [Defn a] -> ShowS
forall a. Show a => Defn a -> Id
forall a.
(Int -> a -> ShowS) -> (a -> Id) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: forall a. Show a => Int -> Defn a -> ShowS
showsPrec :: Int -> Defn a -> ShowS
$cshow :: forall a. Show a => Defn a -> Id
show :: Defn a -> Id
$cshowList :: forall a. Show a => [Defn a] -> ShowS
showList :: [Defn a] -> ShowS
Show)

data EvalKind = Regular | Conf deriving (EvalKind -> EvalKind -> Bool
(EvalKind -> EvalKind -> Bool)
-> (EvalKind -> EvalKind -> Bool) -> Eq EvalKind
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: EvalKind -> EvalKind -> Bool
== :: EvalKind -> EvalKind -> Bool
$c/= :: EvalKind -> EvalKind -> Bool
/= :: EvalKind -> EvalKind -> Bool
Eq, Int -> EvalKind -> ShowS
[EvalKind] -> ShowS
EvalKind -> Id
(Int -> EvalKind -> ShowS)
-> (EvalKind -> Id) -> ([EvalKind] -> ShowS) -> Show EvalKind
forall a.
(Int -> a -> ShowS) -> (a -> Id) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> EvalKind -> ShowS
showsPrec :: Int -> EvalKind -> ShowS
$cshow :: EvalKind -> Id
show :: EvalKind -> Id
$cshowList :: [EvalKind] -> ShowS
showList :: [EvalKind] -> ShowS
Show)

data Eval a = Eval
  { forall a. Eval a -> EvalKind
evKind  :: EvalKind
  , forall a. Eval a -> Bind a
evName  :: !(Bind a)
  , forall a. Eval a -> Expr a
evRoot  :: !(Expr a)
  , forall a. Eval a -> [Step a]
evSteps :: [Step a]
  } deriving (Eval a -> Eval a -> Bool
(Eval a -> Eval a -> Bool)
-> (Eval a -> Eval a -> Bool) -> Eq (Eval a)
forall a. Eq a => Eval a -> Eval a -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: forall a. Eq a => Eval a -> Eval a -> Bool
== :: Eval a -> Eval a -> Bool
$c/= :: forall a. Eq a => Eval a -> Eval a -> Bool
/= :: Eval a -> Eval a -> Bool
Eq, Int -> Eval a -> ShowS
[Eval a] -> ShowS
Eval a -> Id
(Int -> Eval a -> ShowS)
-> (Eval a -> Id) -> ([Eval a] -> ShowS) -> Show (Eval a)
forall a. Show a => Int -> Eval a -> ShowS
forall a. Show a => [Eval a] -> ShowS
forall a. Show a => Eval a -> Id
forall a.
(Int -> a -> ShowS) -> (a -> Id) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: forall a. Show a => Int -> Eval a -> ShowS
showsPrec :: Int -> Eval a -> ShowS
$cshow :: forall a. Show a => Eval a -> Id
show :: Eval a -> Id
$cshowList :: forall a. Show a => [Eval a] -> ShowS
showList :: [Eval a] -> ShowS
Show)

data Step a
  = Step !(Eqn a) !(Expr a)
  deriving (Step a -> Step a -> Bool
(Step a -> Step a -> Bool)
-> (Step a -> Step a -> Bool) -> Eq (Step a)
forall a. Eq a => Step a -> Step a -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: forall a. Eq a => Step a -> Step a -> Bool
== :: Step a -> Step a -> Bool
$c/= :: forall a. Eq a => Step a -> Step a -> Bool
/= :: Step a -> Step a -> Bool
Eq, Int -> Step a -> ShowS
[Step a] -> ShowS
Step a -> Id
(Int -> Step a -> ShowS)
-> (Step a -> Id) -> ([Step a] -> ShowS) -> Show (Step a)
forall a. Show a => Int -> Step a -> ShowS
forall a. Show a => [Step a] -> ShowS
forall a. Show a => Step a -> Id
forall a.
(Int -> a -> ShowS) -> (a -> Id) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: forall a. Show a => Int -> Step a -> ShowS
showsPrec :: Int -> Step a -> ShowS
$cshow :: forall a. Show a => Step a -> Id
show :: Step a -> Id
$cshowList :: forall a. Show a => [Step a] -> ShowS
showList :: [Step a] -> ShowS
Show)

{-
  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 (EqnOp -> EqnOp -> Bool
(EqnOp -> EqnOp -> Bool) -> (EqnOp -> EqnOp -> Bool) -> Eq EqnOp
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: EqnOp -> EqnOp -> Bool
== :: EqnOp -> EqnOp -> Bool
$c/= :: EqnOp -> EqnOp -> Bool
/= :: EqnOp -> EqnOp -> Bool
Eq, Int -> EqnOp -> ShowS
[EqnOp] -> ShowS
EqnOp -> Id
(Int -> EqnOp -> ShowS)
-> (EqnOp -> Id) -> ([EqnOp] -> ShowS) -> Show EqnOp
forall a.
(Int -> a -> ShowS) -> (a -> Id) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> EqnOp -> ShowS
showsPrec :: Int -> EqnOp -> ShowS
$cshow :: EqnOp -> Id
show :: EqnOp -> Id
$cshowList :: [EqnOp] -> ShowS
showList :: [EqnOp] -> ShowS
Show)

-- Strong, weak, or head normal form check
data NormCheck = Strong | Weak | Head deriving (NormCheck -> NormCheck -> Bool
(NormCheck -> NormCheck -> Bool)
-> (NormCheck -> NormCheck -> Bool) -> Eq NormCheck
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: NormCheck -> NormCheck -> Bool
== :: NormCheck -> NormCheck -> Bool
$c/= :: NormCheck -> NormCheck -> Bool
/= :: NormCheck -> NormCheck -> Bool
Eq, Int -> NormCheck -> ShowS
[NormCheck] -> ShowS
NormCheck -> Id
(Int -> NormCheck -> ShowS)
-> (NormCheck -> Id) -> ([NormCheck] -> ShowS) -> Show NormCheck
forall a.
(Int -> a -> ShowS) -> (a -> Id) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> NormCheck -> ShowS
showsPrec :: Int -> NormCheck -> ShowS
$cshow :: NormCheck -> Id
show :: NormCheck -> Id
$cshowList :: [NormCheck] -> ShowS
showList :: [NormCheck] -> ShowS
Show)

data Eqn a = Eqn EqnOp (Maybe NormCheck) a deriving (Eqn a -> Eqn a -> Bool
(Eqn a -> Eqn a -> Bool) -> (Eqn a -> Eqn a -> Bool) -> Eq (Eqn a)
forall a. Eq a => Eqn a -> Eqn a -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: forall a. Eq a => Eqn a -> Eqn a -> Bool
== :: Eqn a -> Eqn a -> Bool
$c/= :: forall a. Eq a => Eqn a -> Eqn a -> Bool
/= :: Eqn a -> Eqn a -> Bool
Eq, Int -> Eqn a -> ShowS
[Eqn a] -> ShowS
Eqn a -> Id
(Int -> Eqn a -> ShowS)
-> (Eqn a -> Id) -> ([Eqn a] -> ShowS) -> Show (Eqn a)
forall a. Show a => Int -> Eqn a -> ShowS
forall a. Show a => [Eqn a] -> ShowS
forall a. Show a => Eqn a -> Id
forall a.
(Int -> a -> ShowS) -> (a -> Id) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: forall a. Show a => Int -> Eqn a -> ShowS
showsPrec :: Int -> Eqn a -> ShowS
$cshow :: forall a. Show a => Eqn a -> Id
show :: Eqn a -> Id
$cshowList :: forall a. Show a => [Eqn a] -> ShowS
showList :: [Eqn a] -> ShowS
Show)

data Bind a
  = Bind Id a
  deriving (Int -> Bind a -> ShowS
[Bind a] -> ShowS
Bind a -> Id
(Int -> Bind a -> ShowS)
-> (Bind a -> Id) -> ([Bind a] -> ShowS) -> Show (Bind a)
forall a. Show a => Int -> Bind a -> ShowS
forall a. Show a => [Bind a] -> ShowS
forall a. Show a => Bind a -> Id
forall a.
(Int -> a -> ShowS) -> (a -> Id) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: forall a. Show a => Int -> Bind a -> ShowS
showsPrec :: Int -> Bind a -> ShowS
$cshow :: forall a. Show a => Bind a -> Id
show :: Bind a -> Id
$cshowList :: forall a. Show a => [Bind a] -> ShowS
showList :: [Bind a] -> ShowS
Show, (forall a b. (a -> b) -> Bind a -> Bind b)
-> (forall a b. a -> Bind b -> Bind a) -> Functor Bind
forall a b. a -> Bind b -> Bind a
forall a b. (a -> b) -> Bind a -> Bind b
forall (f :: * -> *).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
$cfmap :: forall a b. (a -> b) -> Bind a -> Bind b
fmap :: forall a b. (a -> b) -> Bind a -> Bind b
$c<$ :: forall a b. a -> Bind b -> Bind a
<$ :: forall a b. a -> Bind b -> Bind a
Functor)

data Expr a
  = EVar Id                  a
  | ELam !(Bind a) !(Expr a) a
  | EApp !(Expr a) !(Expr a) a
--  deriving (Show)

instance Show (Expr a) where
  show :: Expr a -> Id
show = Expr a -> Id
forall a. PPrint a => a -> Id
pprint

instance Eq (Bind a) where
  Bind a
b1 == :: Bind a -> Bind a -> Bool
== Bind a
b2 = Bind a -> Id
forall a. Bind a -> Id
bindId Bind a
b1 Id -> Id -> Bool
forall a. Eq a => a -> a -> Bool
== Bind a -> Id
forall a. Bind a -> Id
bindId Bind a
b2

-- instance Eq (Expr a) where
  -- (EVar x _)      == (EVar y _)      = x == y
  -- (ELam b1 e1 _)  == (ELam b2 e2 _ ) = b1 == b2 && e1  == e2
  -- (EApp e1 e1' _) == (EApp e2 e2' _) = e1 == e2 && e1' == e2'
  -- _               == _               = False

data RExpr
  = RVar Id
  | RLam Id    RExpr
  | RApp RExpr RExpr
  deriving (RExpr -> RExpr -> Bool
(RExpr -> RExpr -> Bool) -> (RExpr -> RExpr -> Bool) -> Eq RExpr
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: RExpr -> RExpr -> Bool
== :: RExpr -> RExpr -> Bool
$c/= :: RExpr -> RExpr -> Bool
/= :: RExpr -> RExpr -> Bool
Eq, (forall x. RExpr -> Rep RExpr x)
-> (forall x. Rep RExpr x -> RExpr) -> Generic RExpr
forall x. Rep RExpr x -> RExpr
forall x. RExpr -> Rep RExpr x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. RExpr -> Rep RExpr x
from :: forall x. RExpr -> Rep RExpr x
$cto :: forall x. Rep RExpr x -> RExpr
to :: forall x. Rep RExpr x -> RExpr
Generic)

rExpr :: Expr a -> RExpr
rExpr :: forall a. Expr a -> RExpr
rExpr (EVar Id
x a
_)    = Id -> RExpr
RVar Id
x
rExpr (ELam Bind a
b Expr a
e  a
_) = Id -> RExpr -> RExpr
RLam (Bind a -> Id
forall a. Bind a -> Id
bindId Bind a
b) (Expr a -> RExpr
forall a. Expr a -> RExpr
rExpr Expr a
e )
rExpr (EApp Expr a
e Expr a
e' a
_) = RExpr -> RExpr -> RExpr
RApp (Expr a -> RExpr
forall a. Expr a -> RExpr
rExpr  Expr a
e) (Expr a -> RExpr
forall a. Expr a -> RExpr
rExpr Expr a
e')

instance Eq (Expr a) where
  Expr a
e1 == :: Expr a -> Expr a -> Bool
== Expr a
e2 = Expr a -> RExpr
forall a. Expr a -> RExpr
rExpr Expr a
e1 RExpr -> RExpr -> Bool
forall a. Eq a => a -> a -> Bool
== Expr a -> RExpr
forall a. Expr a -> RExpr
rExpr Expr a
e2

instance Hashable RExpr

instance Hashable (Expr a) where
  hashWithSalt :: Int -> Expr a -> Int
hashWithSalt Int
i = Int -> RExpr -> Int
forall a. Hashable a => Int -> a -> Int
hashWithSalt Int
i (RExpr -> Int) -> (Expr a -> RExpr) -> Expr a -> Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Expr a -> RExpr
forall a. Expr a -> RExpr
rExpr

-------------------------------------------------------------------------------------
-- | Pretty Printing
-------------------------------------------------------------------------------------
instance PPrint (Bind a) where
  pprint :: Bind a -> Id
pprint (Bind Id
x a
_) = Id
x

instance PPrint [Bind a] where
  pprint :: [Bind a] -> Id
pprint = [Id] -> Id
unwords ([Id] -> Id) -> ([Bind a] -> [Id]) -> [Bind a] -> Id
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Bind a -> Id) -> [Bind a] -> [Id]
forall a b. (a -> b) -> [a] -> [b]
map Bind a -> Id
forall a. PPrint a => a -> Id
pprint

instance PPrint (Expr a) where
  pprint :: Expr a -> Id
pprint (EVar Id
x a
_)     = Id
x
  pprint (EApp Expr a
e1 Expr a
e2 a
_) = Id -> Id -> ShowS
forall r. PrintfType r => Id -> r
printf Id
"(%s %s)" (Expr a -> Id
forall a. PPrint a => a -> Id
pprint Expr a
e1) (Expr a -> Id
forall a. PPrint a => a -> Id
pprint Expr a
e2)
  pprint e :: Expr a
e@(ELam {})    = Id -> Id -> ShowS
forall r. PrintfType r => Id -> r
printf Id
"(\\%s -> %s)" ([Bind a] -> Id
forall a. PPrint a => a -> Id
pprint [Bind a]
xs) (Expr a -> Id
forall a. PPrint a => a -> Id
pprint Expr a
body)
    where
      ([Bind a]
xs, Expr a
body)        = Expr a -> ([Bind a], Expr a)
forall a. Expr a -> ([Bind a], Expr a)
bkLam Expr a
e

bkLam :: Expr a -> ([Bind a], Expr a)
bkLam :: forall a. Expr a -> ([Bind a], Expr a)
bkLam (ELam Bind a
x Expr a
e a
_) = (Bind a
xBind a -> [Bind a] -> [Bind a]
forall a. a -> [a] -> [a]
:[Bind a]
xs, Expr a
body)
  where
    ([Bind a]
xs, Expr a
body)     = Expr a -> ([Bind a], Expr a)
forall a. Expr a -> ([Bind a], Expr a)
bkLam Expr a
e
bkLam Expr a
e            = ([], Expr a
e)

mkLam :: (Monoid a) => [Bind a] -> Expr a -> Expr a
mkLam :: forall a. Monoid a => [Bind a] -> Expr a -> Expr a
mkLam []       Expr a
e = Expr a
e
mkLam (Bind a
x:[Bind a]
xs) Expr a
e = Bind a -> Expr a -> a -> Expr a
forall a. Bind a -> Expr a -> a -> Expr a
ELam Bind a
x ([Bind a] -> Expr a -> Expr a
forall a. Monoid a => [Bind a] -> Expr a -> Expr a
mkLam [Bind a]
xs Expr a
e) (Bind a -> a
forall a. Bind a -> a
forall (t :: * -> *) a. Tagged t => t a -> a
tag Bind a
x a -> a -> a
forall a. Semigroup a => a -> a -> a
<> Expr a -> a
forall a. Expr a -> a
forall (t :: * -> *) a. Tagged t => t a -> a
tag Expr a
e)

bindId :: Bind a -> Id
bindId :: forall a. Bind a -> Id
bindId (Bind Id
x a
_) = Id
x

-------------------------------------------------------------------------------------
-- | Tag Extraction
-------------------------------------------------------------------------------------
class Tagged t where
  tag :: t a -> a

instance Tagged Eqn where
  tag :: forall a. Eqn a -> a
tag (Eqn EqnOp
_ Maybe NormCheck
_ a
x) = a
x

instance Tagged Bind where
  tag :: forall a. Bind a -> a
tag (Bind Id
_   a
x) = a
x

instance Tagged Expr where
  tag :: forall a. Expr a -> a
tag (EVar Id
_   a
x) = a
x
  tag (ELam Bind a
_ Expr a
_ a
x) = a
x
  tag (EApp Expr a
_ Expr a
_ a
x) = a
x