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

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

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

successes :: [Result a] -> [Id]
successes :: forall a. [Result a] -> [Id]
successes = forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe forall {a}. Result a -> Maybe Id
go
  where
    go :: Result a -> Maybe Id
go (OK Bind a
b) = forall a. a -> Maybe a
Just (forall a. Bind a -> Id
bindId Bind a
b)
    go Result a
_      = 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)   = forall a. Located a => a -> Id -> Maybe UserError
mkErr a
l (forall a. Bind a -> Id
bindId Bind a
b forall a. [a] -> [a] -> [a]
++ Id
" can be further reduced!")
resultError (Invalid Bind a
b a
l)   = forall a. Located a => a -> Id -> Maybe UserError
mkErr a
l (forall a. Bind a -> Id
bindId Bind a
b forall a. [a] -> [a] -> [a]
++ Id
" has an invalid reduction!")
resultError (Unbound Bind a
b Id
x a
l) = forall a. Located a => a -> Id -> Maybe UserError
mkErr a
l (forall a. Bind a -> Id
bindId Bind a
b forall a. [a] -> [a] -> [a]
++ Id
" has an unbound variable " forall a. [a] -> [a] -> [a]
++ Id
x )
resultError (DupDefn Bind a
b a
l)   = forall a. Located a => a -> Id -> Maybe UserError
mkErr a
l (Id
"Definition " forall a. [a] -> [a] -> [a]
++ (forall a. Bind a -> Id
bindId Bind a
b) forall a. [a] -> [a] -> [a]
++ Id
" has already been declared")
resultError (DupEval Bind a
b a
l)   = forall a. Located a => a -> Id -> Maybe UserError
mkErr a
l (Id
"Evaluation " forall a. [a] -> [a] -> [a]
++ (forall a. Bind a -> Id
bindId Bind a
b) forall a. [a] -> [a] -> [a]
++ Id
" has already been declared")
resultError Result a
_               = 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 = forall a. a -> Maybe a
Just (Id -> SourceSpan -> UserError
mkError Id
msg (forall a. Located a => a -> SourceSpan
sourceSpan a
l))

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

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

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

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

data Eqn a
  = AlphEq a
  | BetaEq a
  | UnBeta a
  | DefnEq a
  | TrnsEq a
  | UnTrEq a
  | NormEq a
  deriving (Eqn a -> Eqn a -> Bool
forall a. Eq a => Eqn a -> Eqn a -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Eqn a -> Eqn a -> Bool
$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
Eq, Int -> Eqn a -> ShowS
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
showList :: [Eqn a] -> ShowS
$cshowList :: forall a. Show a => [Eqn a] -> ShowS
show :: Eqn a -> Id
$cshow :: forall a. Show a => Eqn a -> Id
showsPrec :: Int -> Eqn a -> ShowS
$cshowsPrec :: forall a. Show a => Int -> Eqn a -> ShowS
Show)

data Bind a
  = Bind Id a
  deriving (Int -> Bind a -> ShowS
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
showList :: [Bind a] -> ShowS
$cshowList :: forall a. Show a => [Bind a] -> ShowS
show :: Bind a -> Id
$cshow :: forall a. Show a => Bind a -> Id
showsPrec :: Int -> Bind a -> ShowS
$cshowsPrec :: forall a. Show a => Int -> Bind a -> ShowS
Show, 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
<$ :: forall a b. a -> Bind b -> Bind a
$c<$ :: forall a b. a -> Bind b -> Bind a
fmap :: forall a b. (a -> b) -> Bind a -> Bind b
$cfmap :: forall a b. (a -> b) -> Bind a -> Bind b
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 = forall a. PPrint a => a -> Id
pprint

instance Eq (Bind a) where
  Bind a
b1 == :: Bind a -> Bind a -> Bool
== Bind a
b2 = forall a. Bind a -> Id
bindId Bind a
b1 forall a. Eq a => a -> a -> Bool
== 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
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: RExpr -> RExpr -> Bool
$c/= :: RExpr -> RExpr -> Bool
== :: RExpr -> RExpr -> Bool
$c== :: RExpr -> RExpr -> Bool
Eq, 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
$cto :: forall x. Rep RExpr x -> RExpr
$cfrom :: forall x. RExpr -> Rep RExpr x
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 (forall a. Bind a -> Id
bindId Bind a
b) (forall a. Expr a -> RExpr
rExpr Expr a
e )
rExpr (EApp Expr a
e Expr a
e' a
_) = RExpr -> RExpr -> RExpr
RApp (forall a. Expr a -> RExpr
rExpr  Expr a
e) (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 = forall a. Expr a -> RExpr
rExpr Expr a
e1 forall a. Eq a => a -> a -> Bool
== 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 = forall a. Hashable a => Int -> a -> Int
hashWithSalt Int
i forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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 forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a -> b) -> [a] -> [b]
map 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
_) = forall r. PrintfType r => Id -> r
printf Id
"(%s %s)" (forall a. PPrint a => a -> Id
pprint Expr a
e1) (forall a. PPrint a => a -> Id
pprint Expr a
e2)
  pprint e :: Expr a
e@(ELam {})    = forall r. PrintfType r => Id -> r
printf Id
"(\\%s -> %s)" (forall a. PPrint a => a -> Id
pprint [Bind a]
xs) (forall a. PPrint a => a -> Id
pprint Expr a
body)
    where
      ([Bind a]
xs, Expr a
body)        = 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
xforall a. a -> [a] -> [a]
:[Bind a]
xs, Expr a
body)
  where
    ([Bind a]
xs, Expr a
body)     = 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 = forall a. Bind a -> Expr a -> a -> Expr a
ELam Bind a
x (forall a. Monoid a => [Bind a] -> Expr a -> Expr a
mkLam [Bind a]
xs Expr a
e) (forall (t :: * -> *) a. Tagged t => t a -> a
tag Bind a
x forall a. Semigroup a => a -> 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 (AlphEq a
x) = a
x
  tag (BetaEq a
x) = a
x
  tag (UnBeta a
x) = a
x
  tag (DefnEq a
x) = a
x
  tag (TrnsEq a
x) = a
x
  tag (UnTrEq a
x) = a
x
  tag (NormEq 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