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

import Numeric.Natural

-- |Types: Nat, Bool, * -> *
data Type
  = TUnit
  | TNatural
  | TBoolean
  | TArrow Term Type Type
  deriving stock (Int -> Type -> ShowS
[Type] -> ShowS
Type -> String
(Int -> Type -> ShowS)
-> (Type -> String) -> ([Type] -> ShowS) -> Show Type
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Type] -> ShowS
$cshowList :: [Type] -> ShowS
show :: Type -> String
$cshow :: Type -> String
showsPrec :: Int -> Type -> ShowS
$cshowsPrec :: Int -> Type -> ShowS
Show, Type -> Type -> Bool
(Type -> Type -> Bool) -> (Type -> Type -> Bool) -> Eq Type
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Type -> Type -> Bool
$c/= :: Type -> Type -> Bool
== :: Type -> Type -> Bool
$c== :: Type -> Type -> Bool
Eq, Eq Type
Eq Type =>
(Type -> Type -> Ordering)
-> (Type -> Type -> Bool)
-> (Type -> Type -> Bool)
-> (Type -> Type -> Bool)
-> (Type -> Type -> Bool)
-> (Type -> Type -> Type)
-> (Type -> Type -> Type)
-> Ord Type
Type -> Type -> Bool
Type -> Type -> Ordering
Type -> Type -> Type
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
min :: Type -> Type -> Type
$cmin :: Type -> Type -> Type
max :: Type -> Type -> Type
$cmax :: Type -> Type -> Type
>= :: Type -> Type -> Bool
$c>= :: Type -> Type -> Bool
> :: Type -> Type -> Bool
$c> :: Type -> Type -> Bool
<= :: Type -> Type -> Bool
$c<= :: Type -> Type -> Bool
< :: Type -> Type -> Bool
$c< :: Type -> Type -> Bool
compare :: Type -> Type -> Ordering
$ccompare :: Type -> Type -> Ordering
$cp1Ord :: Eq Type
Ord)

-- |Terms of STLC.
data Term
  = Unit
  | Lambda Term Type Term
  | App Term Term
  | Assert Term Term
  | Atom Natural
  | If Term Term Term
  | Succ Term
  | Pred Term
  | IsZero Term
  | Natural Natural
  | Boolean Bool
  deriving stock (Int -> Term -> ShowS
[Term] -> ShowS
Term -> String
(Int -> Term -> ShowS)
-> (Term -> String) -> ([Term] -> ShowS) -> Show Term
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Term] -> ShowS
$cshowList :: [Term] -> ShowS
show :: Term -> String
$cshow :: Term -> String
showsPrec :: Int -> Term -> ShowS
$cshowsPrec :: Int -> Term -> ShowS
Show, Term -> Term -> Bool
(Term -> Term -> Bool) -> (Term -> Term -> Bool) -> Eq Term
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Term -> Term -> Bool
$c/= :: Term -> Term -> Bool
== :: Term -> Term -> Bool
$c== :: Term -> Term -> Bool
Eq, Eq Term
Eq Term =>
(Term -> Term -> Ordering)
-> (Term -> Term -> Bool)
-> (Term -> Term -> Bool)
-> (Term -> Term -> Bool)
-> (Term -> Term -> Bool)
-> (Term -> Term -> Term)
-> (Term -> Term -> Term)
-> Ord Term
Term -> Term -> Bool
Term -> Term -> Ordering
Term -> Term -> Term
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
min :: Term -> Term -> Term
$cmin :: Term -> Term -> Term
max :: Term -> Term -> Term
$cmax :: Term -> Term -> Term
>= :: Term -> Term -> Bool
$c>= :: Term -> Term -> Bool
> :: Term -> Term -> Bool
$c> :: Term -> Term -> Bool
<= :: Term -> Term -> Bool
$c<= :: Term -> Term -> Bool
< :: Term -> Term -> Bool
$c< :: Term -> Term -> Bool
compare :: Term -> Term -> Ordering
$ccompare :: Term -> Term -> Ordering
$cp1Ord :: Eq Term
Ord)

-- |@x & y = if x then y else false@
pattern And :: Term -> Term -> Term
pattern $bAnd :: Term -> Term -> Term
$mAnd :: forall r. Term -> (Term -> Term -> r) -> (Void# -> r) -> r
And x y = If x y (Boolean False)

-- |@x | y = if x then true else y@
pattern Or :: Term -> Term -> Term
pattern $bOr :: Term -> Term -> Term
$mOr :: forall r. Term -> (Term -> Term -> r) -> (Void# -> r) -> r
Or x y = If x (Boolean True) y

-- |@not x = if x then false else true@
pattern Not :: Term -> Term
pattern $bNot :: Term -> Term
$mNot :: forall r. Term -> (Term -> r) -> (Void# -> r) -> r
Not x = If x (Boolean False) (Boolean True)

-- |Is this term a value?
isValue :: Term -> Bool
isValue :: Term -> Bool
isValue Unit = Bool
True
isValue (Lambda _ _ _) = Bool
True
isValue (Natural _) = Bool
True 
isValue (Boolean _) = Bool
True
isValue _ = Bool
False

-- |Bind to a value.
pattern Value :: Term
pattern $mValue :: forall r. Term -> (Void# -> r) -> (Void# -> r) -> r
Value <- (isValue -> True)

-- |The lift operation of de Bruijn notation.
liftAtom :: Natural -> Natural -> Term -> Term
liftAtom :: Natural -> Natural -> Term -> Term
liftAtom c :: Natural
c n :: Natural
n (Lambda p :: Term
p t :: Type
t m :: Term
m)
  = Term -> Type -> Term -> Term
Lambda (Natural -> Natural -> Term -> Term
liftAtom (Natural -> Natural
forall a. Enum a => a -> a
succ Natural
c) Natural
n Term
p) Type
t (Natural -> Natural -> Term -> Term
liftAtom (Natural -> Natural
forall a. Enum a => a -> a
succ Natural
c) Natural
n Term
m)
liftAtom c :: Natural
c n :: Natural
n (App f :: Term
f x :: Term
x) = Term -> Term -> Term
App (Natural -> Natural -> Term -> Term
liftAtom Natural
c Natural
n Term
f) (Natural -> Natural -> Term -> Term
liftAtom Natural
c Natural
n Term
x)
liftAtom c :: Natural
c n :: Natural
n (Assert p :: Term
p x :: Term
x) = Term -> Term -> Term
Assert (Natural -> Natural -> Term -> Term
liftAtom Natural
c Natural
n Term
p) (Natural -> Natural -> Term -> Term
liftAtom Natural
c Natural
n Term
x)
liftAtom c :: Natural
c n :: Natural
n (Atom k :: Natural
k) = if Natural
k Natural -> Natural -> Bool
forall a. Ord a => a -> a -> Bool
>= Natural
c then Natural -> Term
Atom (Natural
k Natural -> Natural -> Natural
forall a. Num a => a -> a -> a
+ Natural
n) else Natural -> Term
Atom Natural
k
liftAtom c :: Natural
c n :: Natural
n (If b :: Term
b t :: Term
t f :: Term
f) = Term -> Term -> Term -> Term
If (Natural -> Natural -> Term -> Term
liftAtom Natural
c Natural
n Term
b) (Natural -> Natural -> Term -> Term
liftAtom Natural
c Natural
n Term
t) (Natural -> Natural -> Term -> Term
liftAtom Natural
c Natural
n Term
f)
liftAtom c :: Natural
c n :: Natural
n (Succ t :: Term
t) = Term -> Term
Succ (Natural -> Natural -> Term -> Term
liftAtom Natural
c Natural
n Term
t)
liftAtom c :: Natural
c n :: Natural
n (Pred t :: Term
t) = Term -> Term
Pred (Natural -> Natural -> Term -> Term
liftAtom Natural
c Natural
n Term
t)
liftAtom c :: Natural
c n :: Natural
n (IsZero t :: Term
t) = Term -> Term
IsZero (Natural -> Natural -> Term -> Term
liftAtom Natural
c Natural
n Term
t)
liftAtom _ _ x :: Term
x = Term
x