{-|
Module      : Language.Contract.Check
Description : Type checker for the contract language.
Copyright   : (c) Xie Ruifeng, 2020
License     : AGPL-3
Maintainer  : krantz.xrf@outlook.com
Stability   : experimental
Portability : portable
-}
module Language.Contract.Check where

import Data.List
import Data.Bifunctor
import Text.Printf

import Control.Monad.Trans.Maybe
import Control.Monad.Reader

import Language.Contract.AST
import Language.Contract.Pretty
import Language.Contract.Proof

-- |Type checker monad.
type MonadTypeCheck m =
  ( MonadReader ([Type], [Term]) m
  , MonadFail m
  , MonadIO m )

-- |Run the type checker monad, get a 'Maybe' result.
runTypeCheck :: MaybeT (ReaderT ([Type], [Term]) IO) a -> IO (Maybe a)
runTypeCheck :: MaybeT (ReaderT ([Type], [Term]) IO) a -> IO (Maybe a)
runTypeCheck m :: MaybeT (ReaderT ([Type], [Term]) IO) a
m = ReaderT ([Type], [Term]) IO (Maybe a)
-> ([Type], [Term]) -> IO (Maybe a)
forall r (m :: * -> *) a. ReaderT r m a -> r -> m a
runReaderT (MaybeT (ReaderT ([Type], [Term]) IO) a
-> ReaderT ([Type], [Term]) IO (Maybe a)
forall (m :: * -> *) a. MaybeT m a -> m (Maybe a)
runMaybeT MaybeT (ReaderT ([Type], [Term]) IO) a
m) ([], [])

-- |Assertion, fail with 'MonadFail'.
-- 'guard' from Prelude uses Alternative, so not suitable here.
assert :: MonadFail m => Bool -> m ()
assert :: Bool -> m ()
assert c :: Bool
c = Bool -> m () -> m ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless Bool
c (String -> m ()
forall (m :: * -> *) a. MonadFail m => String -> m a
fail "")

-- |Prove a term in the type checker monad.
prove :: MonadTypeCheck m => Term -> m ()
prove :: Term -> m ()
prove res :: Term
res = do
  [Type]
bindings <- (([Type], [Term]) -> [Type]) -> m [Type]
forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
asks ([Type], [Term]) -> [Type]
forall a b. (a, b) -> a
fst
  let n :: Natural
n = [Type] -> Natural
forall i a. Num i => [a] -> i
genericLength [Type]
bindings
  [Term]
premise <- (([Type], [Term]) -> [Term]) -> m [Term]
forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
asks ((Term -> Bool) -> [Term] -> [Term]
forall a. (a -> Bool) -> [a] -> [a]
filter (Term -> Term -> Bool
forall a. Eq a => a -> a -> Bool
/= Bool -> Term
Boolean Bool
True) ([Term] -> [Term])
-> (([Type], [Term]) -> [Term]) -> ([Type], [Term]) -> [Term]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Term -> Term) -> [Term] -> [Term]
forall a b. (a -> b) -> [a] -> [b]
map Term -> Term
eval ([Term] -> [Term])
-> (([Type], [Term]) -> [Term]) -> ([Type], [Term]) -> [Term]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ([Type], [Term]) -> [Term]
forall a b. (a, b) -> b
snd)
  let res' :: Term
res' = Term -> Term
eval Term
res
  if Term
res Term -> Term -> Bool
forall a. Eq a => a -> a -> Bool
/= Term
res'
    then IO () -> m ()
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO () -> m ()) -> IO () -> m ()
forall a b. (a -> b) -> a -> b
$ String -> String -> String -> String -> IO ()
forall r. PrintfType r => String -> r
printf "Proving %s => %s [%s] ... "
      (Natural -> [Term] -> String
forall a. PrettyPrint a => Natural -> a -> String
prettyWith Natural
n [Term]
premise) (Natural -> Term -> String
forall a. PrettyPrint a => Natural -> a -> String
prettyWith Natural
n Term
res') (Natural -> Term -> String
forall a. PrettyPrint a => Natural -> a -> String
prettyWith Natural
n Term
res)
    else IO () -> m ()
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO () -> m ()) -> IO () -> m ()
forall a b. (a -> b) -> a -> b
$ String -> String -> String -> IO ()
forall r. PrintfType r => String -> r
printf "Proving %s => %s ... "
      (Natural -> [Term] -> String
forall a. PrettyPrint a => Natural -> a -> String
prettyWith Natural
n [Term]
premise) (Natural -> Term -> String
forall a. PrettyPrint a => Natural -> a -> String
prettyWith Natural
n Term
res')
  [Type] -> [Term] -> Term -> m (Maybe ThmResult)
forall (m :: * -> *).
MonadIO m =>
[Type] -> [Term] -> Term -> m (Maybe ThmResult)
tryProve [Type]
bindings [Term]
premise Term
res' m (Maybe ThmResult) -> (Maybe ThmResult -> m ()) -> m ()
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
    Just r :: ThmResult
r@ThmResult
Proven -> IO () -> m ()
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (ThmResult -> IO ()
forall a. Show a => a -> IO ()
print ThmResult
r)
    Just r :: ThmResult
r@ThmResult
Falsified -> IO () -> m ()
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (ThmResult -> IO ()
forall a. Show a => a -> IO ()
print ThmResult
r) m () -> m () -> m ()
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> String -> m ()
forall (m :: * -> *) a. MonadFail m => String -> m a
fail "Proof failed."
    Just r :: ThmResult
r -> do
      IO () -> m ()
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (ThmResult -> IO ()
forall a. Show a => a -> IO ()
print ThmResult
r)
      IO () -> m ()
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO () -> m ()) -> IO () -> m ()
forall a b. (a -> b) -> a -> b
$ String -> IO ()
putStr "SBV failed, fall back to naive proving ... "
      [Type] -> [Term] -> Term -> m ()
forall (m :: * -> *).
(MonadFail m, MonadIO m) =>
[Type] -> [Term] -> Term -> m ()
naiveTryProve [Type]
bindings [Term]
premise Term
res'
    Nothing -> do
      IO () -> m ()
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO () -> m ()) -> IO () -> m ()
forall a b. (a -> b) -> a -> b
$ String -> IO ()
putStr "SBV not usable, fall back to naive proving ... "
      [Type] -> [Term] -> Term -> m ()
forall (m :: * -> *).
(MonadFail m, MonadIO m) =>
[Type] -> [Term] -> Term -> m ()
naiveTryProve [Type]
bindings [Term]
premise Term
res'

-- |The type of a term, within a specific context.
typeOf :: MonadTypeCheck m => Term -> m Type
typeOf :: Term -> m Type
typeOf Unit = Type -> m Type
forall (f :: * -> *) a. Applicative f => a -> f a
pure Type
TUnit
typeOf (Lambda p :: Term
p t :: Type
t m :: Term
m) = do
  Type
TBoolean <- (([Type], [Term]) -> ([Type], [Term])) -> m Type -> m Type
forall r (m :: * -> *) a. MonadReader r m => (r -> r) -> m a -> m a
local (([Type] -> [Type]) -> ([Type], [Term]) -> ([Type], [Term])
forall (p :: * -> * -> *) a b c.
Bifunctor p =>
(a -> b) -> p a c -> p b c
first (Type
tType -> [Type] -> [Type]
forall a. a -> [a] -> [a]
:)) (Term -> m Type
forall (m :: * -> *). MonadTypeCheck m => Term -> m Type
typeOf Term
p)
  Term -> Type -> Type -> Type
TArrow Term
p Type
t (Type -> Type) -> m Type -> m Type
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (([Type], [Term]) -> ([Type], [Term])) -> m Type -> m Type
forall r (m :: * -> *) a. MonadReader r m => (r -> r) -> m a -> m a
local (([Type] -> [Type])
-> ([Term] -> [Term]) -> ([Type], [Term]) -> ([Type], [Term])
forall (p :: * -> * -> *) a b c d.
Bifunctor p =>
(a -> b) -> (c -> d) -> p a c -> p b d
bimap (Type
tType -> [Type] -> [Type]
forall a. a -> [a] -> [a]
:) ((Term
pTerm -> [Term] -> [Term]
forall a. a -> [a] -> [a]
:) ([Term] -> [Term]) -> ([Term] -> [Term]) -> [Term] -> [Term]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Term -> Term) -> [Term] -> [Term]
forall a b. (a -> b) -> [a] -> [b]
map (Natural -> Natural -> Term -> Term
liftAtom 0 1))) (Term -> m Type
forall (m :: * -> *). MonadTypeCheck m => Term -> m Type
typeOf Term
m)
typeOf (App f :: Term
f x :: Term
x) = do
  TArrow p :: Term
p tx :: Type
tx tr :: Type
tr <- Term -> m Type
forall (m :: * -> *). MonadTypeCheck m => Term -> m Type
typeOf Term
f
  Type
tx' <- Term -> m Type
forall (m :: * -> *). MonadTypeCheck m => Term -> m Type
typeOf Term
x
  Bool -> m ()
forall (m :: * -> *). MonadFail m => Bool -> m ()
assert (Type
tx Type -> Type -> Bool
forall a. Eq a => a -> a -> Bool
== Type
tx')
  Term -> m ()
forall (m :: * -> *). MonadTypeCheck m => Term -> m ()
prove ([Term] -> Term -> Term
evalWith [Term
x] Term
p)
  Type -> m Type
forall (f :: * -> *) a. Applicative f => a -> f a
pure Type
tr
typeOf (Assert p :: Term
p x :: Term
x) = do
  Type
t <- Term -> m Type
forall (m :: * -> *). MonadTypeCheck m => Term -> m Type
typeOf Term
x
  (([Type], [Term]) -> ([Type], [Term])) -> m () -> m ()
forall r (m :: * -> *) a. MonadReader r m => (r -> r) -> m a -> m a
local (([Type] -> [Type]) -> ([Type], [Term]) -> ([Type], [Term])
forall (p :: * -> * -> *) a b c.
Bifunctor p =>
(a -> b) -> p a c -> p b c
first (Type
tType -> [Type] -> [Type]
forall a. a -> [a] -> [a]
:)) (m () -> m ()) -> m () -> m ()
forall a b. (a -> b) -> a -> b
$ do
    Type
TBoolean <- Term -> m Type
forall (m :: * -> *). MonadTypeCheck m => Term -> m Type
typeOf Term
p
    Term -> m ()
forall (m :: * -> *). MonadTypeCheck m => Term -> m ()
prove Term
p
  Type -> m Type
forall (f :: * -> *) a. Applicative f => a -> f a
pure Type
t
typeOf (Atom n :: Natural
n) = do
  [Type]
ts <- (([Type], [Term]) -> [Type]) -> m [Type]
forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
asks ([Type], [Term]) -> [Type]
forall a b. (a, b) -> a
fst
  Bool -> m ()
forall (m :: * -> *). MonadFail m => Bool -> m ()
assert ([Type] -> Natural
forall i a. Num i => [a] -> i
genericLength [Type]
ts Natural -> Natural -> Bool
forall a. Ord a => a -> a -> Bool
> Natural
n)
  Type -> m Type
forall (f :: * -> *) a. Applicative f => a -> f a
pure ([Type]
ts [Type] -> Natural -> Type
forall i a. Integral i => [a] -> i -> a
`genericIndex` Natural
n)
typeOf (If c :: Term
c t :: Term
t f :: Term
f) = do
  Type
TBoolean <- Term -> m Type
forall (m :: * -> *). MonadTypeCheck m => Term -> m Type
typeOf Term
c
  Type
tt <- (([Type], [Term]) -> ([Type], [Term])) -> m Type -> m Type
forall r (m :: * -> *) a. MonadReader r m => (r -> r) -> m a -> m a
local (([Term] -> [Term]) -> ([Type], [Term]) -> ([Type], [Term])
forall (p :: * -> * -> *) b c a.
Bifunctor p =>
(b -> c) -> p a b -> p a c
second (Term
cTerm -> [Term] -> [Term]
forall a. a -> [a] -> [a]
:)) (Term -> m Type
forall (m :: * -> *). MonadTypeCheck m => Term -> m Type
typeOf Term
t)
  Type
tf <- (([Type], [Term]) -> ([Type], [Term])) -> m Type -> m Type
forall r (m :: * -> *) a. MonadReader r m => (r -> r) -> m a -> m a
local (([Term] -> [Term]) -> ([Type], [Term]) -> ([Type], [Term])
forall (p :: * -> * -> *) b c a.
Bifunctor p =>
(b -> c) -> p a b -> p a c
second (Term -> Term
Not Term
cTerm -> [Term] -> [Term]
forall a. a -> [a] -> [a]
:)) (Term -> m Type
forall (m :: * -> *). MonadTypeCheck m => Term -> m Type
typeOf Term
f)
  Bool -> m ()
forall (m :: * -> *). MonadFail m => Bool -> m ()
assert (Type
tt Type -> Type -> Bool
forall a. Eq a => a -> a -> Bool
== Type
tf)
  Type -> m Type
forall (f :: * -> *) a. Applicative f => a -> f a
pure Type
tt
typeOf (Succ n :: Term
n) = do
  Type
TNatural <- Term -> m Type
forall (m :: * -> *). MonadTypeCheck m => Term -> m Type
typeOf Term
n
  Type -> m Type
forall (f :: * -> *) a. Applicative f => a -> f a
pure Type
TNatural
typeOf (Pred n :: Term
n) = do
  Type
TNatural <- Term -> m Type
forall (m :: * -> *). MonadTypeCheck m => Term -> m Type
typeOf Term
n
  Term -> m ()
forall (m :: * -> *). MonadTypeCheck m => Term -> m ()
prove (Term -> Term
Not (Term -> Term) -> Term -> Term
forall a b. (a -> b) -> a -> b
$ Term -> Term
IsZero Term
n)
  Type -> m Type
forall (f :: * -> *) a. Applicative f => a -> f a
pure Type
TNatural
typeOf (IsZero t :: Term
t) = do
  Type
TNatural <- Term -> m Type
forall (m :: * -> *). MonadTypeCheck m => Term -> m Type
typeOf Term
t
  Type -> m Type
forall (f :: * -> *) a. Applicative f => a -> f a
pure Type
TBoolean
typeOf (Boolean _) = Type -> m Type
forall (f :: * -> *) a. Applicative f => a -> f a
pure Type
TBoolean
typeOf (Natural _) = Type -> m Type
forall (f :: * -> *) a. Applicative f => a -> f a
pure Type
TNatural

-- |One-step evaluation of a term.
eval1 :: [Term] -> Term -> Term
eval1 :: [Term] -> Term -> Term
eval1 vs :: [Term]
vs (App (Lambda _ _ m :: Term
m) x :: Term
x@Term
Value) = [Term] -> Term -> Term
eval1 (Term
xTerm -> [Term] -> [Term]
forall a. a -> [a] -> [a]
:[Term]
vs) Term
m
eval1 vs :: [Term]
vs (App f :: Term
f@(Lambda _ _ _) x :: Term
x) = Term -> Term -> Term
App Term
f ([Term] -> Term -> Term
eval1 [Term]
vs Term
x)
eval1 vs :: [Term]
vs (App f :: Term
f x :: Term
x) = Term -> Term -> Term
App ([Term] -> Term -> Term
eval1 [Term]
vs Term
f) Term
x
eval1 vs :: [Term]
vs (Atom n :: Natural
n) =
  if [Term] -> Natural
forall i a. Num i => [a] -> i
genericLength [Term]
vs Natural -> Natural -> Bool
forall a. Ord a => a -> a -> Bool
> Natural
n
  then [Term]
vs [Term] -> Natural -> Term
forall i a. Integral i => [a] -> i -> a
`genericIndex` Natural
n
  else Natural -> Term
Atom Natural
n
eval1 _  (If (Boolean c :: Bool
c) t :: Term
t f :: Term
f) = if Bool
c then Term
t else Term
f
eval1 vs :: [Term]
vs (If c :: Term
c t :: Term
t f :: Term
f) = Term -> Term -> Term -> Term
If ([Term] -> Term -> Term
eval1 [Term]
vs Term
c) Term
t Term
f
eval1 _  (Succ (Natural n :: Natural
n)) = Natural -> Term
Natural (Natural
n Natural -> Natural -> Natural
forall a. Num a => a -> a -> a
+ 1)
eval1 vs :: [Term]
vs (Succ n :: Term
n) = Term -> Term
Succ ([Term] -> Term -> Term
eval1 [Term]
vs Term
n)
eval1 _  (Pred (Natural n :: Natural
n)) = Natural -> Term
Natural (Natural
n Natural -> Natural -> Natural
forall a. Num a => a -> a -> a
- 1)
eval1 vs :: [Term]
vs (Pred n :: Term
n) = Term -> Term
Pred ([Term] -> Term -> Term
eval1 [Term]
vs Term
n)
eval1 _  (IsZero (Natural n :: Natural
n)) = Bool -> Term
Boolean (Natural
n Natural -> Natural -> Bool
forall a. Eq a => a -> a -> Bool
== 0)
eval1 vs :: [Term]
vs (IsZero n :: Term
n) = Term -> Term
IsZero ([Term] -> Term -> Term
eval1 [Term]
vs Term
n)
eval1 _  v :: Term
v = Term
v

-- |Full evaluation of a term.
evalWith :: [Term] -> Term -> Term
evalWith :: [Term] -> Term -> Term
evalWith vs :: [Term]
vs t :: Term
t = let x :: Term
x = [Term] -> Term -> Term
eval1 [Term]
vs Term
t in
  if Term -> Bool
isValue Term
x Bool -> Bool -> Bool
|| Term
t Term -> Term -> Bool
forall a. Eq a => a -> a -> Bool
== Term
x then Term
x else [Term] -> Term -> Term
evalWith [Term]
vs Term
x

-- |Full evaluation of a term.
eval :: Term -> Term
eval :: Term -> Term
eval = [Term] -> Term -> Term
evalWith []