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

import Data.Char
import Data.Bifunctor
import Numeric.Natural

import Control.Monad.Reader
import Control.Monad.Writer

import Language.Contract.AST

type MonadPretty m = (MonadReader (Int, Natural) m, MonadWriter String m)

newVar :: MonadPretty m => (String -> m a) -> m a
newVar :: (String -> m a) -> m a
newVar p :: String -> m a
p = do
  String
x <- ((Int, Natural) -> String) -> m String
forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
asks (Natural -> String
makeVarName (Natural -> String)
-> ((Int, Natural) -> Natural) -> (Int, Natural) -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Int, Natural) -> Natural
forall a b. (a, b) -> b
snd)
  ((Int, Natural) -> (Int, Natural)) -> m a -> m a
forall r (m :: * -> *) a. MonadReader r m => (r -> r) -> m a -> m a
local ((Natural -> Natural) -> (Int, Natural) -> (Int, Natural)
forall (p :: * -> * -> *) b c a.
Bifunctor p =>
(b -> c) -> p a b -> p a c
second (Natural -> Natural -> Natural
forall a. Num a => a -> a -> a
+1)) (String -> m a
p String
x)

-- |Make a variable name from its internal index.
makeVarName :: Natural -> String
makeVarName :: Natural -> String
makeVarName = [Natural] -> String
forall a. Integral a => [a] -> String
toStr ([Natural] -> String)
-> (Natural -> [Natural]) -> Natural -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Natural] -> Natural -> [Natural]
forall t. Integral t => [t] -> t -> [t]
go [] where
  go :: [t] -> t -> [t]
go xs :: [t]
xs 0 = [t]
xs
  go xs :: [t]
xs n :: t
n = let (q :: t
q, r :: t
r) = t -> t -> (t, t)
forall a. Integral a => a -> a -> (a, a)
quotRem t
n 26 in [t] -> t -> [t]
go (t
r t -> [t] -> [t]
forall a. a -> [a] -> [a]
: [t]
xs) t
q
  toStr :: [a] -> String
toStr [] = "a"
  toStr xs :: [a]
xs = (a -> Char) -> [a] -> String
forall a b. (a -> b) -> [a] -> [b]
map (Int -> Char
chr (Int -> Char) -> (a -> Int) -> a -> Char
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Char -> Int
ord 'a') (Int -> Int) -> (a -> Int) -> a -> Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral) [a]
xs

paren :: MonadPretty m => Int -> m a -> m a
paren :: Int -> m a -> m a
paren n :: Int
n = ((Int, Natural) -> (Int, Natural)) -> m a -> m a
forall r (m :: * -> *) a. MonadReader r m => (r -> r) -> m a -> m a
local ((Int -> Int) -> (Int, Natural) -> (Int, Natural)
forall (p :: * -> * -> *) a b c.
Bifunctor p =>
(a -> b) -> p a c -> p b c
first (Int -> Int -> Int
forall a b. a -> b -> a
const Int
n))

tellParen :: MonadPretty m => Int -> m a -> m a
tellParen :: Int -> m a -> m a
tellParen n :: Int
n m :: m a
m = do
  Int
p <- ((Int, Natural) -> Int) -> m Int
forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
asks (Int, Natural) -> Int
forall a b. (a, b) -> a
fst
  Bool -> m () -> m ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Int
n Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< Int
p) (String -> m ()
forall w (m :: * -> *). MonadWriter w m => w -> m ()
tell "(")
  a
res <- Int -> m a -> m a
forall (m :: * -> *) a. MonadPretty m => Int -> m a -> m a
paren Int
n m a
m
  Bool -> m () -> m ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Int
n Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< Int
p) (String -> m ()
forall w (m :: * -> *). MonadWriter w m => w -> m ()
tell ")")
  a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure a
res

prettyType :: MonadPretty m => Type -> m ()
prettyType :: Type -> m ()
prettyType TUnit = String -> m ()
forall w (m :: * -> *). MonadWriter w m => w -> m ()
tell "Unit"
prettyType TNatural = String -> m ()
forall w (m :: * -> *). MonadWriter w m => w -> m ()
tell "Nat"
prettyType TBoolean = String -> m ()
forall w (m :: * -> *). MonadWriter w m => w -> m ()
tell "Bool"
prettyType (TArrow p :: Term
p s :: Type
s t :: Type
t) = ((Int, Natural) -> (Int, Natural)) -> m () -> m ()
forall r (m :: * -> *) a. MonadReader r m => (r -> r) -> m a -> m a
local ((Natural -> Natural) -> (Int, Natural) -> (Int, Natural)
forall (p :: * -> * -> *) b c a.
Bifunctor p =>
(b -> c) -> p a b -> p a c
second (Natural -> Natural -> Natural
forall a. Num a => a -> a -> a
+1)) (m () -> m ()) -> m () -> m ()
forall a b. (a -> b) -> a -> b
$ do
  String -> m ()
forall w (m :: * -> *). MonadWriter w m => w -> m ()
tell "{"
  Term -> m ()
forall (m :: * -> *). MonadPretty m => Term -> m ()
prettyTerm Term
p
  String -> m ()
forall w (m :: * -> *). MonadWriter w m => w -> m ()
tell "} "
  Type -> m ()
forall (m :: * -> *). MonadPretty m => Type -> m ()
prettyType Type
s
  String -> m ()
forall w (m :: * -> *). MonadWriter w m => w -> m ()
tell " -> "
  Type -> m ()
forall (m :: * -> *). MonadPretty m => Type -> m ()
prettyType Type
t

prettyTerm :: MonadPretty m => Term -> m ()
prettyTerm :: Term -> m ()
prettyTerm (Not t :: Term
t) = Int -> m () -> m ()
forall (m :: * -> *) a. MonadPretty m => Int -> m a -> m a
tellParen 5 (m () -> m ()) -> m () -> m ()
forall a b. (a -> b) -> a -> b
$ String -> m ()
forall w (m :: * -> *). MonadWriter w m => w -> m ()
tell "not " m () -> m () -> m ()
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> Int -> m () -> m ()
forall (m :: * -> *) a. MonadPretty m => Int -> m a -> m a
paren 6 (Term -> m ()
forall (m :: * -> *). MonadPretty m => Term -> m ()
prettyTerm Term
t)
prettyTerm (And x :: Term
x y :: Term
y) = Int -> m () -> m ()
forall (m :: * -> *) a. MonadPretty m => Int -> m a -> m a
tellParen 2 (m () -> m ()) -> m () -> m ()
forall a b. (a -> b) -> a -> b
$ do
  Term -> m ()
forall (m :: * -> *). MonadPretty m => Term -> m ()
prettyTerm Term
x
  String -> m ()
forall w (m :: * -> *). MonadWriter w m => w -> m ()
tell " & "
  Term -> m ()
forall (m :: * -> *). MonadPretty m => Term -> m ()
prettyTerm Term
y
prettyTerm (Or x :: Term
x y :: Term
y) = Int -> m () -> m ()
forall (m :: * -> *) a. MonadPretty m => Int -> m a -> m a
tellParen 1 (m () -> m ()) -> m () -> m ()
forall a b. (a -> b) -> a -> b
$ do
  Term -> m ()
forall (m :: * -> *). MonadPretty m => Term -> m ()
prettyTerm Term
x
  String -> m ()
forall w (m :: * -> *). MonadWriter w m => w -> m ()
tell " | "
  Term -> m ()
forall (m :: * -> *). MonadPretty m => Term -> m ()
prettyTerm Term
y
prettyTerm Unit = String -> m ()
forall w (m :: * -> *). MonadWriter w m => w -> m ()
tell "unit"
prettyTerm (Lambda p :: Term
p t :: Type
t tm :: Term
tm) = (String -> m ()) -> m ()
forall (m :: * -> *) a. MonadPretty m => (String -> m a) -> m a
newVar ((String -> m ()) -> m ()) -> (String -> m ()) -> m ()
forall a b. (a -> b) -> a -> b
$ \x :: String
x -> Int -> m () -> m ()
forall (m :: * -> *) a. MonadPretty m => Int -> m a -> m a
tellParen 0 (m () -> m ()) -> m () -> m ()
forall a b. (a -> b) -> a -> b
$ do
  String -> m ()
forall w (m :: * -> *). MonadWriter w m => w -> m ()
tell "\\"
  String -> m ()
forall w (m :: * -> *). MonadWriter w m => w -> m ()
tell String
x
  String -> m ()
forall w (m :: * -> *). MonadWriter w m => w -> m ()
tell " : "
  Type -> m ()
forall (m :: * -> *). MonadPretty m => Type -> m ()
prettyType Type
t
  String -> m ()
forall w (m :: * -> *). MonadWriter w m => w -> m ()
tell " {"
  Term -> m ()
forall (m :: * -> *). MonadPretty m => Term -> m ()
prettyTerm Term
p
  String -> m ()
forall w (m :: * -> *). MonadWriter w m => w -> m ()
tell "} . "
  Term -> m ()
forall (m :: * -> *). MonadPretty m => Term -> m ()
prettyTerm Term
tm
prettyTerm (App f :: Term
f x :: Term
x) = Int -> m () -> m ()
forall (m :: * -> *) a. MonadPretty m => Int -> m a -> m a
tellParen 5 (m () -> m ()) -> m () -> m ()
forall a b. (a -> b) -> a -> b
$ do
  Term -> m ()
forall (m :: * -> *). MonadPretty m => Term -> m ()
prettyTerm Term
f
  String -> m ()
forall w (m :: * -> *). MonadWriter w m => w -> m ()
tell " "
  Int -> m () -> m ()
forall (m :: * -> *) a. MonadPretty m => Int -> m a -> m a
paren 6 (m () -> m ()) -> m () -> m ()
forall a b. (a -> b) -> a -> b
$ Term -> m ()
forall (m :: * -> *). MonadPretty m => Term -> m ()
prettyTerm Term
x
prettyTerm (Assert p :: Term
p x :: Term
x) = Int -> m () -> m ()
forall (m :: * -> *) a. MonadPretty m => Int -> m a -> m a
tellParen 3 (m () -> m ()) -> m () -> m ()
forall a b. (a -> b) -> a -> b
$ do
  String -> m ()
forall w (m :: * -> *). MonadWriter w m => w -> m ()
tell "{"
  Term -> m ()
forall (m :: * -> *). MonadPretty m => Term -> m ()
prettyTerm Term
p
  String -> m ()
forall w (m :: * -> *). MonadWriter w m => w -> m ()
tell "} "
  Int -> m () -> m ()
forall (m :: * -> *) a. MonadPretty m => Int -> m a -> m a
paren 4 (m () -> m ()) -> m () -> m ()
forall a b. (a -> b) -> a -> b
$ Term -> m ()
forall (m :: * -> *). MonadPretty m => Term -> m ()
prettyTerm Term
x
prettyTerm (Atom n :: Natural
n) = do
  Natural
x <- ((Int, Natural) -> Natural) -> m Natural
forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
asks (Int, Natural) -> Natural
forall a b. (a, b) -> b
snd
  String -> m ()
forall w (m :: * -> *). MonadWriter w m => w -> m ()
tell (Natural -> String
makeVarName (Natural -> String) -> Natural -> String
forall a b. (a -> b) -> a -> b
$ Natural
x Natural -> Natural -> Natural
forall a. Num a => a -> a -> a
- Natural
n Natural -> Natural -> Natural
forall a. Num a => a -> a -> a
- 1)
prettyTerm (If c :: Term
c t :: Term
t f :: Term
f) = Int -> m () -> m ()
forall (m :: * -> *) a. MonadPretty m => Int -> m a -> m a
tellParen 0 (m () -> m ()) -> m () -> m ()
forall a b. (a -> b) -> a -> b
$ do
  String -> m ()
forall w (m :: * -> *). MonadWriter w m => w -> m ()
tell "if "
  Term -> m ()
forall (m :: * -> *). MonadPretty m => Term -> m ()
prettyTerm Term
c
  String -> m ()
forall w (m :: * -> *). MonadWriter w m => w -> m ()
tell " then "
  Term -> m ()
forall (m :: * -> *). MonadPretty m => Term -> m ()
prettyTerm Term
t
  String -> m ()
forall w (m :: * -> *). MonadWriter w m => w -> m ()
tell " else "
  Term -> m ()
forall (m :: * -> *). MonadPretty m => Term -> m ()
prettyTerm Term
f
prettyTerm (Succ t :: Term
t) = Int -> m () -> m ()
forall (m :: * -> *) a. MonadPretty m => Int -> m a -> m a
tellParen 5 (m () -> m ()) -> m () -> m ()
forall a b. (a -> b) -> a -> b
$ String -> m ()
forall w (m :: * -> *). MonadWriter w m => w -> m ()
tell "succ " m () -> m () -> m ()
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> Int -> m () -> m ()
forall (m :: * -> *) a. MonadPretty m => Int -> m a -> m a
paren 6 (Term -> m ()
forall (m :: * -> *). MonadPretty m => Term -> m ()
prettyTerm Term
t)
prettyTerm (Pred t :: Term
t) = Int -> m () -> m ()
forall (m :: * -> *) a. MonadPretty m => Int -> m a -> m a
tellParen 5 (m () -> m ()) -> m () -> m ()
forall a b. (a -> b) -> a -> b
$ String -> m ()
forall w (m :: * -> *). MonadWriter w m => w -> m ()
tell "pred " m () -> m () -> m ()
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> Int -> m () -> m ()
forall (m :: * -> *) a. MonadPretty m => Int -> m a -> m a
paren 6 (Term -> m ()
forall (m :: * -> *). MonadPretty m => Term -> m ()
prettyTerm Term
t)
prettyTerm (IsZero t :: Term
t) = Int -> m () -> m ()
forall (m :: * -> *) a. MonadPretty m => Int -> m a -> m a
tellParen 5 (m () -> m ()) -> m () -> m ()
forall a b. (a -> b) -> a -> b
$ String -> m ()
forall w (m :: * -> *). MonadWriter w m => w -> m ()
tell "iszero " m () -> m () -> m ()
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> Int -> m () -> m ()
forall (m :: * -> *) a. MonadPretty m => Int -> m a -> m a
paren 6 (Term -> m ()
forall (m :: * -> *). MonadPretty m => Term -> m ()
prettyTerm Term
t)
prettyTerm (Natural n :: Natural
n) = String -> m ()
forall w (m :: * -> *). MonadWriter w m => w -> m ()
tell (Natural -> String
forall a. Show a => a -> String
show Natural
n)
prettyTerm (Boolean b :: Bool
b) = String -> m ()
forall w (m :: * -> *). MonadWriter w m => w -> m ()
tell (if Bool
b then "true" else "false")

-- |Pretty show for terms and types.
class PrettyPrint a where
  -- |Pretty show provided the number of layers of lambda abstractions.
  prettyWith :: Natural -> a -> String
  -- |Pretty show assuming no outside lambda abstractions.
  pretty :: a -> String

  prettyWith _ = a -> String
forall a. PrettyPrint a => a -> String
pretty
  pretty = Natural -> a -> String
forall a. PrettyPrint a => Natural -> a -> String
prettyWith 0
  {-# MINIMAL prettyWith | pretty #-}

-- |Pretty print, a 'putStrLn' after a 'prettyWith'.
prettyPrintWith :: PrettyPrint a => Natural -> a -> IO ()
prettyPrintWith :: Natural -> a -> IO ()
prettyPrintWith u :: Natural
u = String -> IO ()
putStrLn (String -> IO ()) -> (a -> String) -> a -> IO ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Natural -> a -> String
forall a. PrettyPrint a => Natural -> a -> String
prettyWith Natural
u

-- |Pretty print, a 'putStrLn' after a 'pretty'.
prettyPrint :: PrettyPrint a => a -> IO ()
prettyPrint :: a -> IO ()
prettyPrint = String -> IO ()
putStrLn (String -> IO ()) -> (a -> String) -> a -> IO ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> String
forall a. PrettyPrint a => a -> String
pretty

instance PrettyPrint Type where
  prettyWith :: Natural -> Type -> String
prettyWith m :: Natural
m t :: Type
t = Reader (Int, Natural) String -> (Int, Natural) -> String
forall r a. Reader r a -> r -> a
runReader (WriterT String (ReaderT (Int, Natural) Identity) ()
-> Reader (Int, Natural) String
forall (m :: * -> *) w a. Monad m => WriterT w m a -> m w
execWriterT (Type -> WriterT String (ReaderT (Int, Natural) Identity) ()
forall (m :: * -> *). MonadPretty m => Type -> m ()
prettyType Type
t)) (0, Natural
m)

instance PrettyPrint Term where
  prettyWith :: Natural -> Term -> String
prettyWith m :: Natural
m t :: Term
t = Reader (Int, Natural) String -> (Int, Natural) -> String
forall r a. Reader r a -> r -> a
runReader (WriterT String (ReaderT (Int, Natural) Identity) ()
-> Reader (Int, Natural) String
forall (m :: * -> *) w a. Monad m => WriterT w m a -> m w
execWriterT (Term -> WriterT String (ReaderT (Int, Natural) Identity) ()
forall (m :: * -> *). MonadPretty m => Term -> m ()
prettyTerm Term
t)) (0, Natural
m)

instance PrettyPrint a => PrettyPrint [a] where
  prettyWith :: Natural -> [a] -> String
prettyWith n :: Natural
n ys :: [a]
ys = "[" String -> String -> String
forall a. Semigroup a => a -> a -> a
<> [a] -> String
go [a]
ys String -> String -> String
forall a. Semigroup a => a -> a -> a
<> "]" where
    go :: [a] -> String
go [] = ""
    go [x :: a
x] = Natural -> a -> String
forall a. PrettyPrint a => Natural -> a -> String
prettyWith Natural
n a
x
    go (x :: a
x : xs :: [a]
xs) = Natural -> a -> String
forall a. PrettyPrint a => Natural -> a -> String
prettyWith Natural
n a
x String -> String -> String
forall a. Semigroup a => a -> a -> a
<> ", " String -> String -> String
forall a. Semigroup a => a -> a -> a
<> [a] -> String
go [a]
xs