Types.hs

{-# 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 (Eq, Show, Functor)

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

successes :: [Result a] -> [Id]
successes = mapMaybe go
  where
    go (OK b) = Just (bindId b)
    go _      = Nothing

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

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

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

data Elsa a = Elsa
  { defns :: [Defn a]
  , evals :: [Eval a]
  }
  deriving (Eq, Show)

data Defn a
  = Defn !(Bind a) !(Expr a)
  deriving (Eq, Show)

data EvalKind = Regular | Conf deriving (Eq, Show)

data Eval a = Eval
  { evKind  :: EvalKind
  , evName  :: !(Bind a)
  , evRoot  :: !(Expr a)
  , evSteps :: [Step a]
  } deriving (Eq, Show)

data Step a
  = Step !(Eqn a) !(Expr a)
  deriving (Eq, 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 (Eq, Show)

-- Strong, weak, or head normal form check
data NormCheck = Strong | Weak | Head deriving (Eq, Show)

data Eqn a = Eqn EqnOp (Maybe NormCheck) a deriving (Eq, Show)

data Bind a
  = Bind Id a
  deriving (Show, Functor)

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

instance Eq (Bind a) where
  b1 == b2 = bindId b1 == bindId 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 (Eq, Generic)

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

instance Eq (Expr a) where
  e1 == e2 = rExpr e1 == rExpr e2

instance Hashable RExpr

instance Hashable (Expr a) where
  hashWithSalt i = hashWithSalt i . rExpr

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

instance PPrint [Bind a] where
  pprint = unwords . map pprint

instance PPrint (Expr a) where
  pprint (EVar x _)     = x
  pprint (EApp e1 e2 _) = printf "(%s %s)" (pprint e1) (pprint e2)
  pprint e@(ELam {})    = printf "(\\%s -> %s)" (pprint xs) (pprint body)
    where
      (xs, body)        = bkLam e

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

mkLam :: (Monoid a) => [Bind a] -> Expr a -> Expr a
mkLam []       e = e
mkLam (x:xs) e = ELam x (mkLam xs e) (tag x <> tag e)

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

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

instance Tagged Eqn where
  tag (Eqn _ _ x) = x

instance Tagged Bind where
  tag (Bind _   x) = x

instance Tagged Expr where
  tag (EVar _   x) = x
  tag (ELam _ _ x) = x
  tag (EApp _ _ x) = x