module Morte.Core (
Var(..),
Const(..),
Expr(..),
Context,
typeWith,
typeOf,
normalize,
used,
prettyExpr,
prettyTypeError,
TypeError(..),
TypeMessage(..),
buildConst,
buildVar,
buildExpr,
buildTypeMessage,
buildTypeError,
) where
import Control.Applicative ((<$>), (<*>))
import Control.DeepSeq
import Control.Exception (Exception)
import Control.Monad.Trans.State (State, evalState)
import qualified Control.Monad.Trans.State as State
import Data.Binary (Binary(get, put), Get, Put)
import Data.Binary.Get (getWord64le)
import Data.Binary.Put (putWord64le)
import Data.Monoid (mempty, (<>))
import Data.String (IsString(fromString))
import Data.Text ()
import Data.Text.Lazy (Text, unpack)
import qualified Data.Text.Encoding as Text
import qualified Data.Text.Lazy as Text
import Data.Text.Lazy.Builder (Builder, toLazyText, fromLazyText)
import Data.Text.Lazy.Builder.Int (decimal)
import Data.Typeable (Typeable)
import Data.Word (Word8)
data Var = V Text Int deriving (Eq, Show)
putUtf8 :: Text -> Put
putUtf8 txt = put (Text.encodeUtf8 (Text.toStrict txt))
getUtf8 :: Get Text
getUtf8 = do
bs <- get
case Text.decodeUtf8' bs of
Left e -> fail (show e)
Right txt -> return (Text.fromStrict txt)
instance Binary Var where
put (V x n) = do
putUtf8 x
putWord64le (fromIntegral n)
get = V <$> getUtf8 <*> fmap fromIntegral getWord64le
instance IsString Var
where
fromString str = V (Text.pack str) 0
instance NFData Var where
rnf (V n p) = rnf n `seq` rnf p
data Const = Star | Box deriving (Eq, Show, Bounded, Enum)
instance Binary Const where
put c = case c of
Star -> put (0 :: Word8)
Box -> put (1 :: Word8)
get = do
n <- get :: Get Word8
case n of
0 -> return Star
1 -> return Box
_ -> fail "get Const: Invalid tag byte"
instance NFData Const
axiom :: Const -> Either TypeError Const
axiom Star = return Box
axiom Box = Left (TypeError [] (Const Box) (Untyped Box))
rule :: Const -> Const -> Either TypeError Const
rule Star Box = return Box
rule Star Star = return Star
rule Box Box = return Box
rule Box Star = return Star
data Expr
= Const Const
| Var Var
| Lam Text Expr Expr
| Pi Text Expr Expr
| App Expr Expr
deriving (Show)
lookupN :: Eq a => a -> [(a, b)] -> Int -> Maybe b
lookupN a ((a', b'):abs') n | a /= a' = lookupN a abs' n
| n > 0 = lookupN a abs' $! n 1
| n == 0 = Just b'
| otherwise = Nothing
lookupN _ [] _ = Nothing
lookupCtx :: Var -> Context -> Maybe Expr
lookupCtx (V x n) ctx = lookupN x ctx n
instance Eq Expr where
eL0 == eR0 = evalState (go (normalize eL0) (normalize eR0)) []
where
go :: Expr -> Expr -> State [(Text, Text)] Bool
go (Const cL) (Const cR) = return (cL == cR)
go (Var (V xL nL)) (Var (V xR nR)) = do
ctx <- State.get
return (nL == nR && case lookupN xL ctx nL of
Nothing -> xL == xR
Just xR' -> xR' == xR )
go (Lam xL tL bL) (Lam xR tR bR) = do
ctx <- State.get
State.put ((xL, xR):ctx)
eq1 <- go tL tR
eq2 <- go bL bR
State.put ctx
return (eq1 && eq2)
go (Pi xL tL bL) (Pi xR tR bR) = do
ctx <- State.get
State.put ((xL, xR):ctx)
eq1 <- go tL tR
eq2 <- go bL bR
State.put ctx
return (eq1 && eq2)
go (App fL aL) (App fR aR) = do
b1 <- go fL fR
b2 <- go aL aR
return (b1 && b2)
go _ _ = return False
instance Binary Expr where
put e = case e of
Const c -> do
put (0 :: Word8)
put c
Var x -> do
put (1 :: Word8)
put x
Lam x _A b -> do
put (2 :: Word8)
putUtf8 x
put _A
put b
Pi x _A _B -> do
put (3 :: Word8)
putUtf8 x
put _A
put _B
App f a -> do
put (4 :: Word8)
put f
put a
get = do
n <- get :: Get Word8
case n of
0 -> Const <$> get
1 -> Var <$> get
2 -> Lam <$> getUtf8 <*> get <*> get
3 -> Pi <$> getUtf8 <*> get <*> get
4 -> App <$> get <*> get
_ -> fail "get Expr: Invalid tag byte"
instance IsString Expr
where
fromString str = Var (fromString str)
instance NFData Expr where
rnf e = case e of
Const c -> rnf c
Var v -> rnf v
Lam x _A b -> rnf x `seq` rnf _A `seq` rnf b
Pi x _A _B -> rnf x `seq` rnf _A `seq` rnf _B
App f a -> rnf f `seq` rnf a
type Context = [(Text, Expr)]
data TypeMessage
= UnboundVariable
| InvalidInputType Expr
| InvalidOutputType Expr
| NotAFunction
| TypeMismatch Expr Expr
| Untyped Const
deriving (Show)
instance NFData TypeMessage where
rnf tm = case tm of
UnboundVariable -> ()
InvalidInputType e -> rnf e
InvalidOutputType e -> rnf e
NotAFunction -> ()
TypeMismatch e1 e2 -> rnf e1 `seq` rnf e2
Untyped c -> rnf c
data TypeError = TypeError
{ context :: Context
, current :: Expr
, typeMessage :: TypeMessage
} deriving (Typeable)
instance Show TypeError where
show = unpack . prettyTypeError
instance Exception TypeError
instance NFData TypeError where
rnf (TypeError ctx crr tym) = rnf ctx `seq` rnf crr `seq` rnf tym
buildConst :: Const -> Builder
buildConst c = case c of
Star -> "*"
Box -> "□"
buildVar :: Var -> Builder
buildVar (V txt n) =
fromLazyText txt <> if n == 0 then mempty else "@" <> decimal n
buildExpr :: Expr -> Builder
buildExpr = go False False
where
go :: Bool -> Bool -> Expr -> Builder
go parenBind parenApp e = case e of
Const c -> buildConst c
Var x -> buildVar x
Lam x _A b ->
(if parenBind then "(" else "")
<> "λ("
<> fromLazyText x
<> " : "
<> go False False _A
<> ") → "
<> go False False b
<> (if parenBind then ")" else "")
Pi x _A b ->
(if parenBind then "(" else "")
<> (if used x b
then
"∀(" <> fromLazyText x <> " : " <> go False False _A <> ")"
else go True False _A )
<> " → "
<> go False False b
<> (if parenBind then ")" else "")
App f a ->
(if parenApp then "(" else "")
<> go True False f <> " " <> go True True a
<> (if parenApp then ")" else "")
used :: Text -> Expr -> Bool
used x e0 = go e0 0
where
go e n = case e of
Var (V x' n') | x == x' && n' >= n -> True
| otherwise -> False
Lam x' _A b -> go _A n || (go b $! n')
where
n' = if x == x' then n + 1 else n
Pi x' _A _B -> go _A n || (go _B $! n')
where
n' = if x == x' then n + 1 else n
App f a -> go f n || go a n
Const _ -> False
buildTypeMessage :: TypeMessage -> Builder
buildTypeMessage msg = case msg of
UnboundVariable ->
"Error: Unbound variable\n"
InvalidInputType expr ->
"Error: Invalid input type\n"
<> "\n"
<> "Type: " <> buildExpr expr <> "\n"
InvalidOutputType expr ->
"Error: Invalid output type\n"
<> "\n"
<> "Type: " <> buildExpr expr <> "\n"
NotAFunction ->
"Error: Only functions may be applied to values\n"
TypeMismatch expr1 expr2 ->
"Error: Function applied to argument of the wrong type\n"
<> "\n"
<> "Expected type: " <> buildExpr expr1 <> "\n"
<> "Argument type: " <> buildExpr expr2 <> "\n"
Untyped c ->
"Error: " <> buildConst c <> " has no type\n"
buildTypeError :: TypeError -> Builder
buildTypeError (TypeError ctx expr msg)
= ( if Text.null (toLazyText buildContext )
then mempty
else "Context:\n" <> buildContext <> "\n"
)
<> "Expression: " <> buildExpr expr <> "\n"
<> "\n"
<> buildTypeMessage msg
where
buildKV (key, val) = fromLazyText key <> " : " <> buildExpr val
buildContext =
(fromLazyText . Text.unlines . map (toLazyText . buildKV) . reverse) ctx
subst :: Text -> Int -> Expr -> Expr -> Expr
subst x n e' e = case e of
Lam x' _A b -> Lam x' (subst x n e' _A) b'
where
n' = if x == x' then n + 1 else n
b' = n' `seq` subst x n' (shift 1 x' 0 e') b
Pi x' _A _B -> Pi x' (subst x n e' _A) _B'
where
n' = if x == x' then n + 1 else n
_B' = n' `seq` subst x n' (shift 1 x' 0 e') _B
App f a -> App (subst x n e' f) (subst x n e' a)
Var (V x' n') -> if x == x' && n == n' then e' else e
Const k -> Const k
shift :: Int -> Text -> Int -> Expr -> Expr
shift d x0 c0 e0 = go e0 c0
where
go e c = case e of
Lam x _A b -> Lam x (go _A c) (go b $! c')
where
c' = if x == x0 then c + 1 else c
Pi x _A _B -> Pi x (go _A c) (go _B $! c')
where
c' = if x == x0 then c + 1 else c
App f a -> App (go f c) (go a c)
Var (V x n) -> n' `seq` Var (V x n')
where
n' = if x == x0 && n >= c then n + d else n
Const k -> Const k
typeWith :: Context -> Expr -> Either TypeError Expr
typeWith ctx e = case e of
Const c -> fmap Const (axiom c)
Var x -> case lookupCtx x ctx of
Nothing -> Left (TypeError ctx e UnboundVariable)
Just a -> return a
Lam x _A b -> do
let ctx' = [ (x', shift 1 x 0 _A') | (x', _A') <- (x, _A):ctx ]
_B <- typeWith ctx' b
let p = Pi x _A _B
_t <- typeWith ctx p
return p
Pi x _A _B -> do
eS <- fmap whnf (typeWith ctx _A)
s <- case eS of
Const s -> return s
_ -> Left (TypeError ctx e (InvalidInputType _A))
let ctx' = [ (x', shift 1 x 0 _A') | (x', _A') <- (x, _A):ctx ]
eT <- fmap whnf (typeWith ctx' _B)
t <- case eT of
Const t -> return t
_ -> Left (TypeError ctx' e (InvalidOutputType _B))
fmap Const (rule s t)
App f a -> do
e' <- fmap whnf (typeWith ctx f)
(x, _A, _B) <- case e' of
Pi x _A _B -> return (x, _A, _B)
_ -> Left (TypeError ctx e NotAFunction)
_A' <- typeWith ctx a
if _A == _A'
then do
let a' = shift 1 x 0 a
_B' = subst x 0 a' _B
return (shift (1) x 0 _B')
else do
let nf_A = normalize _A
nf_A' = normalize _A'
Left (TypeError ctx e (TypeMismatch nf_A nf_A'))
typeOf :: Expr -> Either TypeError Expr
typeOf = typeWith []
whnf :: Expr -> Expr
whnf e = case e of
App f a -> case whnf f of
Lam x _A b -> whnf (shift (1) x 0 b')
where
a' = shift 1 x 0 a
b' = subst x 0 a' b
_ -> e
_ -> e
freeIn :: Var -> Expr -> Bool
freeIn v@(V x n) = go
where
go e = case e of
Lam x' _A b ->
n' `seq` (go _A || if x == x' then freeIn (V x n') b else go b)
where
n' = n + 1
Pi x' _A _B ->
n' `seq` (go _A || if x == x' then freeIn (V x n') _B else go _B)
where
n' = n + 1
Var v' -> v == v'
App f a -> go f || go a
Const _ -> False
normalize :: Expr -> Expr
normalize e = case e of
Lam x _A b -> case b' of
App f a -> case a of
Var v' | v == v' && not (v `freeIn` f) ->
shift (1) x 0 f
| otherwise ->
e'
where
v = V x 0
_ -> e'
_ -> e'
where
b' = normalize b
e' = Lam x (normalize _A) b'
Pi x _A _B -> Pi x (normalize _A) (normalize _B)
App f a -> case normalize f of
Lam x _A b -> normalize (shift (1) x 0 b')
where
a' = shift 1 x 0 a
b' = subst x 0 a' b
f' -> App f' (normalize a)
Var _ -> e
Const _ -> e
prettyExpr :: Expr -> Text
prettyExpr = toLazyText . buildExpr
prettyTypeError :: TypeError -> Text
prettyTypeError = toLazyText . buildTypeError