{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE TypeApplications    #-}
{-# LANGUAGE TypeOperators       #-}
module Evaluation.Builtins.Integer.Common
where

import Prelude hiding (and, not, or)

import PlutusCore qualified as PLC
import PlutusCore.Generators.QuickCheck.Builtin (AsArbitraryBuiltin (..))
import PlutusCore.MkPlc (builtin, mkIterAppNoAnn, mkTyBuiltin, tyInst)

import Evaluation.Builtins.Common

import Test.QuickCheck (Arbitrary, Gen, arbitrary, choose, oneof)

{- We don't want to use the standard QuickCheck generator for Integers in these
   property tests because that only produces values in [-99..99].  Instead we
   mix the better generator for AsArbitraryBuiltin Integer and one which
   produces Integers up to 400 bits.  The name `BigInteger` is maybe slightly
   misleading but it has the merit of being relatively short.
-}
arbitraryBigInteger :: Gen Integer
arbitraryBigInteger :: Gen Integer
arbitraryBigInteger =
  [Gen Integer] -> Gen Integer
forall a. HasCallStack => [Gen a] -> Gen a
oneof [ AsArbitraryBuiltin Integer -> Integer
forall a. AsArbitraryBuiltin a -> a
unAsArbitraryBuiltin (AsArbitraryBuiltin Integer -> Integer)
-> Gen (AsArbitraryBuiltin Integer) -> Gen Integer
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Gen (AsArbitraryBuiltin Integer)
forall a. Arbitrary a => Gen a
arbitrary
        , (Integer, Integer) -> Gen Integer
forall a. Random a => (a, a) -> Gen a
choose (-Integer
b, Integer
b)
        ]
  where b :: Integer
b = (Integer
2::Integer)Integer -> Integer -> Integer
forall a b. (Num a, Integral b) => a -> b -> a
^(Integer
400::Integer)

newtype BigInteger = BigInteger Integer
  deriving newtype (Int -> BigInteger -> ShowS
[BigInteger] -> ShowS
BigInteger -> String
(Int -> BigInteger -> ShowS)
-> (BigInteger -> String)
-> ([BigInteger] -> ShowS)
-> Show BigInteger
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> BigInteger -> ShowS
showsPrec :: Int -> BigInteger -> ShowS
$cshow :: BigInteger -> String
show :: BigInteger -> String
$cshowList :: [BigInteger] -> ShowS
showList :: [BigInteger] -> ShowS
Show, BigInteger -> BigInteger -> Bool
(BigInteger -> BigInteger -> Bool)
-> (BigInteger -> BigInteger -> Bool) -> Eq BigInteger
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: BigInteger -> BigInteger -> Bool
== :: BigInteger -> BigInteger -> Bool
$c/= :: BigInteger -> BigInteger -> Bool
/= :: BigInteger -> BigInteger -> Bool
Eq, Eq BigInteger
Eq BigInteger =>
(BigInteger -> BigInteger -> Ordering)
-> (BigInteger -> BigInteger -> Bool)
-> (BigInteger -> BigInteger -> Bool)
-> (BigInteger -> BigInteger -> Bool)
-> (BigInteger -> BigInteger -> Bool)
-> (BigInteger -> BigInteger -> BigInteger)
-> (BigInteger -> BigInteger -> BigInteger)
-> Ord BigInteger
BigInteger -> BigInteger -> Bool
BigInteger -> BigInteger -> Ordering
BigInteger -> BigInteger -> BigInteger
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
$ccompare :: BigInteger -> BigInteger -> Ordering
compare :: BigInteger -> BigInteger -> Ordering
$c< :: BigInteger -> BigInteger -> Bool
< :: BigInteger -> BigInteger -> Bool
$c<= :: BigInteger -> BigInteger -> Bool
<= :: BigInteger -> BigInteger -> Bool
$c> :: BigInteger -> BigInteger -> Bool
> :: BigInteger -> BigInteger -> Bool
$c>= :: BigInteger -> BigInteger -> Bool
>= :: BigInteger -> BigInteger -> Bool
$cmax :: BigInteger -> BigInteger -> BigInteger
max :: BigInteger -> BigInteger -> BigInteger
$cmin :: BigInteger -> BigInteger -> BigInteger
min :: BigInteger -> BigInteger -> BigInteger
Ord, Integer -> BigInteger
BigInteger -> BigInteger
BigInteger -> BigInteger -> BigInteger
(BigInteger -> BigInteger -> BigInteger)
-> (BigInteger -> BigInteger -> BigInteger)
-> (BigInteger -> BigInteger -> BigInteger)
-> (BigInteger -> BigInteger)
-> (BigInteger -> BigInteger)
-> (BigInteger -> BigInteger)
-> (Integer -> BigInteger)
-> Num BigInteger
forall a.
(a -> a -> a)
-> (a -> a -> a)
-> (a -> a -> a)
-> (a -> a)
-> (a -> a)
-> (a -> a)
-> (Integer -> a)
-> Num a
$c+ :: BigInteger -> BigInteger -> BigInteger
+ :: BigInteger -> BigInteger -> BigInteger
$c- :: BigInteger -> BigInteger -> BigInteger
- :: BigInteger -> BigInteger -> BigInteger
$c* :: BigInteger -> BigInteger -> BigInteger
* :: BigInteger -> BigInteger -> BigInteger
$cnegate :: BigInteger -> BigInteger
negate :: BigInteger -> BigInteger
$cabs :: BigInteger -> BigInteger
abs :: BigInteger -> BigInteger
$csignum :: BigInteger -> BigInteger
signum :: BigInteger -> BigInteger
$cfromInteger :: Integer -> BigInteger
fromInteger :: Integer -> BigInteger
Num)

instance Arbitrary BigInteger where
   arbitrary :: Gen BigInteger
arbitrary = Integer -> BigInteger
BigInteger (Integer -> BigInteger) -> Gen Integer -> Gen BigInteger
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Gen Integer
arbitraryBigInteger

biginteger :: BigInteger -> PlcTerm
biginteger :: BigInteger -> PlcTerm
biginteger (BigInteger Integer
n) = Integer -> PlcTerm
integer Integer
n

-- Functions creating terms that are applications of various builtins, for
-- convenience.

addInteger :: PlcTerm -> PlcTerm -> PlcTerm
addInteger :: PlcTerm -> PlcTerm -> PlcTerm
addInteger PlcTerm
a PlcTerm
b = PlcTerm -> [PlcTerm] -> PlcTerm
forall (term :: * -> *) tyname name (uni :: * -> *) fun.
TermLike term tyname name uni fun =>
term () -> [term ()] -> term ()
mkIterAppNoAnn (() -> DefaultFun -> PlcTerm
forall ann.
ann -> DefaultFun -> Term TyName Name DefaultUni DefaultFun ann
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> fun -> term ann
builtin () DefaultFun
PLC.AddInteger) [PlcTerm
a, PlcTerm
b]

subtractInteger :: PlcTerm -> PlcTerm -> PlcTerm
subtractInteger :: PlcTerm -> PlcTerm -> PlcTerm
subtractInteger PlcTerm
a PlcTerm
b = PlcTerm -> [PlcTerm] -> PlcTerm
forall (term :: * -> *) tyname name (uni :: * -> *) fun.
TermLike term tyname name uni fun =>
term () -> [term ()] -> term ()
mkIterAppNoAnn (() -> DefaultFun -> PlcTerm
forall ann.
ann -> DefaultFun -> Term TyName Name DefaultUni DefaultFun ann
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> fun -> term ann
builtin () DefaultFun
PLC.SubtractInteger) [PlcTerm
a, PlcTerm
b]

divideInteger :: PlcTerm -> PlcTerm -> PlcTerm
divideInteger :: PlcTerm -> PlcTerm -> PlcTerm
divideInteger PlcTerm
a PlcTerm
b = PlcTerm -> [PlcTerm] -> PlcTerm
forall (term :: * -> *) tyname name (uni :: * -> *) fun.
TermLike term tyname name uni fun =>
term () -> [term ()] -> term ()
mkIterAppNoAnn (() -> DefaultFun -> PlcTerm
forall ann.
ann -> DefaultFun -> Term TyName Name DefaultUni DefaultFun ann
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> fun -> term ann
builtin () DefaultFun
PLC.DivideInteger) [PlcTerm
a, PlcTerm
b]

modInteger :: PlcTerm -> PlcTerm -> PlcTerm
modInteger :: PlcTerm -> PlcTerm -> PlcTerm
modInteger PlcTerm
a PlcTerm
b = PlcTerm -> [PlcTerm] -> PlcTerm
forall (term :: * -> *) tyname name (uni :: * -> *) fun.
TermLike term tyname name uni fun =>
term () -> [term ()] -> term ()
mkIterAppNoAnn (() -> DefaultFun -> PlcTerm
forall ann.
ann -> DefaultFun -> Term TyName Name DefaultUni DefaultFun ann
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> fun -> term ann
builtin () DefaultFun
PLC.ModInteger) [PlcTerm
a, PlcTerm
b]

multiplyInteger :: PlcTerm -> PlcTerm -> PlcTerm
multiplyInteger :: PlcTerm -> PlcTerm -> PlcTerm
multiplyInteger PlcTerm
a PlcTerm
b = PlcTerm -> [PlcTerm] -> PlcTerm
forall (term :: * -> *) tyname name (uni :: * -> *) fun.
TermLike term tyname name uni fun =>
term () -> [term ()] -> term ()
mkIterAppNoAnn (() -> DefaultFun -> PlcTerm
forall ann.
ann -> DefaultFun -> Term TyName Name DefaultUni DefaultFun ann
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> fun -> term ann
builtin () DefaultFun
PLC.MultiplyInteger) [PlcTerm
a, PlcTerm
b]

quotientInteger :: PlcTerm -> PlcTerm -> PlcTerm
quotientInteger :: PlcTerm -> PlcTerm -> PlcTerm
quotientInteger PlcTerm
a PlcTerm
b = PlcTerm -> [PlcTerm] -> PlcTerm
forall (term :: * -> *) tyname name (uni :: * -> *) fun.
TermLike term tyname name uni fun =>
term () -> [term ()] -> term ()
mkIterAppNoAnn (() -> DefaultFun -> PlcTerm
forall ann.
ann -> DefaultFun -> Term TyName Name DefaultUni DefaultFun ann
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> fun -> term ann
builtin () DefaultFun
PLC.QuotientInteger) [PlcTerm
a, PlcTerm
b]

remainderInteger :: PlcTerm -> PlcTerm -> PlcTerm
remainderInteger :: PlcTerm -> PlcTerm -> PlcTerm
remainderInteger PlcTerm
a PlcTerm
b = PlcTerm -> [PlcTerm] -> PlcTerm
forall (term :: * -> *) tyname name (uni :: * -> *) fun.
TermLike term tyname name uni fun =>
term () -> [term ()] -> term ()
mkIterAppNoAnn (() -> DefaultFun -> PlcTerm
forall ann.
ann -> DefaultFun -> Term TyName Name DefaultUni DefaultFun ann
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> fun -> term ann
builtin () DefaultFun
PLC.RemainderInteger) [PlcTerm
a, PlcTerm
b]

equalsInteger :: PlcTerm -> PlcTerm -> PlcTerm
equalsInteger :: PlcTerm -> PlcTerm -> PlcTerm
equalsInteger PlcTerm
a PlcTerm
b = PlcTerm -> [PlcTerm] -> PlcTerm
forall (term :: * -> *) tyname name (uni :: * -> *) fun.
TermLike term tyname name uni fun =>
term () -> [term ()] -> term ()
mkIterAppNoAnn (() -> DefaultFun -> PlcTerm
forall ann.
ann -> DefaultFun -> Term TyName Name DefaultUni DefaultFun ann
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> fun -> term ann
builtin () DefaultFun
PLC.EqualsInteger) [PlcTerm
a, PlcTerm
b]

lessThanInteger :: PlcTerm -> PlcTerm -> PlcTerm
lessThanInteger :: PlcTerm -> PlcTerm -> PlcTerm
lessThanInteger PlcTerm
a PlcTerm
b = PlcTerm -> [PlcTerm] -> PlcTerm
forall (term :: * -> *) tyname name (uni :: * -> *) fun.
TermLike term tyname name uni fun =>
term () -> [term ()] -> term ()
mkIterAppNoAnn (() -> DefaultFun -> PlcTerm
forall ann.
ann -> DefaultFun -> Term TyName Name DefaultUni DefaultFun ann
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> fun -> term ann
builtin () DefaultFun
PLC.LessThanInteger) [PlcTerm
a, PlcTerm
b]

lessThanEqualsInteger :: PlcTerm -> PlcTerm -> PlcTerm
lessThanEqualsInteger :: PlcTerm -> PlcTerm -> PlcTerm
lessThanEqualsInteger PlcTerm
a PlcTerm
b = PlcTerm -> [PlcTerm] -> PlcTerm
forall (term :: * -> *) tyname name (uni :: * -> *) fun.
TermLike term tyname name uni fun =>
term () -> [term ()] -> term ()
mkIterAppNoAnn (() -> DefaultFun -> PlcTerm
forall ann.
ann -> DefaultFun -> Term TyName Name DefaultUni DefaultFun ann
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> fun -> term ann
builtin () DefaultFun
PLC.LessThanEqualsInteger) [PlcTerm
a, PlcTerm
b]

le0 :: PlcTerm -> PlcTerm
le0 :: PlcTerm -> PlcTerm
le0 PlcTerm
t = PlcTerm -> PlcTerm -> PlcTerm
lessThanEqualsInteger PlcTerm
t PlcTerm
zero

ge0 :: PlcTerm -> PlcTerm
ge0 :: PlcTerm -> PlcTerm
ge0 PlcTerm
t = PlcTerm -> PlcTerm -> PlcTerm
lessThanEqualsInteger PlcTerm
zero PlcTerm
t

ite
  :: forall a
   . PLC.DefaultUni `PLC.HasTypeLevel` a
  => PlcTerm -> PlcTerm -> PlcTerm -> PlcTerm
ite :: forall a.
HasTypeLevel DefaultUni a =>
PlcTerm -> PlcTerm -> PlcTerm -> PlcTerm
ite PlcTerm
b PlcTerm
t PlcTerm
f =
  let ty :: Type tyname DefaultUni ()
ty = forall a (x :: a) (uni :: * -> *) ann tyname.
HasTypeLevel uni x =>
ann -> Type tyname uni ann
mkTyBuiltin @_ @a ()
      iteInst :: PlcTerm
iteInst = () -> PlcTerm -> Type TyName DefaultUni () -> PlcTerm
forall ann.
ann
-> Term TyName Name DefaultUni DefaultFun ann
-> Type TyName DefaultUni ann
-> Term TyName Name DefaultUni DefaultFun ann
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> term ann -> Type tyname uni ann -> term ann
tyInst () (() -> DefaultFun -> PlcTerm
forall ann.
ann -> DefaultFun -> Term TyName Name DefaultUni DefaultFun ann
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> fun -> term ann
builtin () DefaultFun
PLC.IfThenElse) Type TyName DefaultUni ()
forall {tyname}. Type tyname DefaultUni ()
ty
  in PlcTerm -> [PlcTerm] -> PlcTerm
forall (term :: * -> *) tyname name (uni :: * -> *) fun.
TermLike term tyname name uni fun =>
term () -> [term ()] -> term ()
mkIterAppNoAnn PlcTerm
iteInst [PlcTerm
b, PlcTerm
t, PlcTerm
f]

-- Various logical combinations of boolean terms.

abs :: PlcTerm -> PlcTerm
abs :: PlcTerm -> PlcTerm
abs PlcTerm
t = forall a.
HasTypeLevel DefaultUni a =>
PlcTerm -> PlcTerm -> PlcTerm -> PlcTerm
ite @Integer (PlcTerm -> PlcTerm -> PlcTerm
lessThanEqualsInteger PlcTerm
zero PlcTerm
t) PlcTerm
t (PlcTerm -> PlcTerm -> PlcTerm
subtractInteger PlcTerm
zero PlcTerm
t)

not :: PlcTerm -> PlcTerm
not :: PlcTerm -> PlcTerm
not PlcTerm
t = forall a.
HasTypeLevel DefaultUni a =>
PlcTerm -> PlcTerm -> PlcTerm -> PlcTerm
ite @Bool PlcTerm
t PlcTerm
false PlcTerm
true

and :: PlcTerm -> PlcTerm -> PlcTerm
and :: PlcTerm -> PlcTerm -> PlcTerm
and PlcTerm
t1 PlcTerm
t2 = forall a.
HasTypeLevel DefaultUni a =>
PlcTerm -> PlcTerm -> PlcTerm -> PlcTerm
ite @Bool PlcTerm
t1 (forall a.
HasTypeLevel DefaultUni a =>
PlcTerm -> PlcTerm -> PlcTerm -> PlcTerm
ite @Bool PlcTerm
t2 PlcTerm
true PlcTerm
false) PlcTerm
false

or :: PlcTerm -> PlcTerm -> PlcTerm
or :: PlcTerm -> PlcTerm -> PlcTerm
or PlcTerm
t1 PlcTerm
t2 = forall a.
HasTypeLevel DefaultUni a =>
PlcTerm -> PlcTerm -> PlcTerm -> PlcTerm
ite @Bool PlcTerm
t1 PlcTerm
true (forall a.
HasTypeLevel DefaultUni a =>
PlcTerm -> PlcTerm -> PlcTerm -> PlcTerm
ite @Bool PlcTerm
t2 PlcTerm
true PlcTerm
false)

xor :: PlcTerm -> PlcTerm -> PlcTerm
xor :: PlcTerm -> PlcTerm -> PlcTerm
xor PlcTerm
t1 PlcTerm
t2 = forall a.
HasTypeLevel DefaultUni a =>
PlcTerm -> PlcTerm -> PlcTerm -> PlcTerm
ite @Bool PlcTerm
t1 (forall a.
HasTypeLevel DefaultUni a =>
PlcTerm -> PlcTerm -> PlcTerm -> PlcTerm
ite @Bool PlcTerm
t2 PlcTerm
false PlcTerm
true) PlcTerm
t2

implies :: PlcTerm -> PlcTerm -> PlcTerm
implies :: PlcTerm -> PlcTerm -> PlcTerm
implies PlcTerm
t1 PlcTerm
t2 = (PlcTerm -> PlcTerm
not PlcTerm
t1) PlcTerm -> PlcTerm -> PlcTerm
`or` PlcTerm
t2

iff :: PlcTerm -> PlcTerm -> PlcTerm
iff :: PlcTerm -> PlcTerm -> PlcTerm
iff PlcTerm
t1 PlcTerm
t2 = (PlcTerm
t1 PlcTerm -> PlcTerm -> PlcTerm
`implies` PlcTerm
t2) PlcTerm -> PlcTerm -> PlcTerm
`and` (PlcTerm
t2 PlcTerm -> PlcTerm -> PlcTerm
`implies` PlcTerm
t1)