{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE OverloadedStrings #-}
{-# OPTIONS_GHC -Wno-orphans #-}

module Analysis.Spec where

import Analysis.Lib
import PlutusCore.Default (DefaultFun (..), DefaultUni)
import PlutusCore.Name.Unique (Name (..))
import Test.Tasty (TestTree, testGroup)
import Test.Tasty.Extras (embed, runTestNested)
import Test.Tasty.HUnit (testCase, (@=?), (@?=))
import UntypedPlutusCore (Term (Apply, Builtin, Force))
import UntypedPlutusCore.Purity (isPure, termEvaluationOrder, unEvalOrder)

evalOrder :: TestTree
evalOrder :: TestTree
evalOrder =
  [String] -> [TestNested] -> TestTree
runTestNested
    [String
"untyped-plutus-core", String
"test", String
"Analysis", String
"evalOrder"]
    [ String -> Term Name DefaultUni DefaultFun () -> TestNested
goldenEvalOrder String
"letFun" Term Name DefaultUni DefaultFun ()
letFun
    , String -> Term Name DefaultUni DefaultFun () -> TestNested
goldenEvalOrder String
"letImpure" Term Name DefaultUni DefaultFun ()
letImpure
    , String -> Term Name DefaultUni DefaultFun () -> TestNested
goldenEvalOrder String
"ifThenElse" Term Name DefaultUni DefaultFun ()
termIfThenElse
    , TestTree -> TestNested
forall a (m :: * -> *). MonadFree ((,) a) m => a -> m ()
embed TestTree
testEvalOrderIsLazy
    , TestTree -> TestNested
forall a (m :: * -> *). MonadFree ((,) a) m => a -> m ()
embed (TestTree -> TestNested) -> TestTree -> TestNested
forall a b. (a -> b) -> a -> b
$
        String -> [TestTree] -> TestTree
testGroup
          String
"Purity"
          [ TestTree
testSomeTypeSomeTermArgsLeft
          , TestTree
testNoTypeSomeTermArgsLeft
          , TestTree
testNoTypeNoTermArgsLeft
          , TestTree
testForceNoTypeParam
          , TestTree
testApplyNoTermParam
          ]
    ]

testEvalOrderIsLazy :: TestTree
testEvalOrderIsLazy :: TestTree
testEvalOrderIsLazy =
  String -> Assertion -> TestTree
testCase String
"evalOrderLazy" (Assertion -> TestTree) -> Assertion -> TestTree
forall a b. (a -> b) -> a -> b
$
    let order :: EvalOrder Name DefaultUni DefaultFun ()
order = BuiltinSemanticsVariant DefaultFun
-> Term Name DefaultUni DefaultFun ()
-> EvalOrder Name DefaultUni DefaultFun ()
forall name (uni :: * -> *) fun a.
ToBuiltinMeaning uni fun =>
BuiltinSemanticsVariant fun
-> Term name uni fun a -> EvalOrder name uni fun a
termEvaluationOrder BuiltinSemanticsVariant DefaultFun
builtinSemantics Term Name DefaultUni DefaultFun ()
dangerTerm
        subterms :: [EvalTerm Name DefaultUni DefaultFun ()]
subterms = EvalOrder Name DefaultUni DefaultFun ()
-> [EvalTerm Name DefaultUni DefaultFun ()]
forall name (uni :: * -> *) fun a.
EvalOrder name uni fun a -> [EvalTerm name uni fun a]
unEvalOrder EvalOrder Name DefaultUni DefaultFun ()
order
     in Int
4 Int -> Int -> Assertion
forall a. (Eq a, Show a, HasCallStack) => a -> a -> Assertion
@=? [EvalTerm Name DefaultUni DefaultFun ()] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [EvalTerm Name DefaultUni DefaultFun ()]
subterms

{-

  Builtin functions can in theory have their type- and term- arguments
  interleaved arbitrarily, but in the default set of builtins ('DefaultFun')
  we have the following patterns:

  - Builtin functions with 0 type arguments followed by N>0 term arguments:
      - EncodeUtf8 : [ string ] -> bytestring
      - AddInteger : [ integer, integer ] -> integer
      - WriteBits  : [ bytestring, list(integer), bool ] -> bytestring

  - Builtin functions with 1 type argument followed by N>0 term arguments:
      - HeadList   : [ forall a, list(a) ] -> a
      - Trace      : [ forall a, string, a ] -> a
      - IfThenElse : [ forall a, bool, a, a ] -> a

  - Builtin functions with 2 type arguments followed by N>0 term arguments:
      - FstPair    : [ forall a, forall b, pair(a, b) ] -> a
      - ChooseList : [ forall a, forall b, list(a), b, b ] -> b
      - CaseList   : [ forall a, forall b
                      , b
                      , (fun a (fun [ (con list) a ] b))
                      , list(a)
                      ] -> b

  When it comes to purity of builtin terms,
  we want to test the following cases:
  +---------------+---------------+
  | Type args     | Term args     |
  | left to apply | left to apply |
  +---------------+---------------+
  |     some      |     some      |
  |     none      |     some      |
  |     none      |     none      |
  +---------------+---------------+
-}

testSomeTypeSomeTermArgsLeft :: TestTree
testSomeTypeSomeTermArgsLeft :: TestTree
testSomeTypeSomeTermArgsLeft =
  String -> Assertion -> TestTree
testCase String
"some type args and some term args are unapplied" (Assertion -> TestTree) -> Assertion -> TestTree
forall a b. (a -> b) -> a -> b
$
    (Term Name DefaultUni DefaultFun () -> Bool)
-> [Term Name DefaultUni DefaultFun ()] -> [Bool]
forall a b. (a -> b) -> [a] -> [b]
map (BuiltinSemanticsVariant DefaultFun
-> Term Name DefaultUni DefaultFun () -> Bool
forall (uni :: * -> *) fun name a.
ToBuiltinMeaning uni fun =>
BuiltinSemanticsVariant fun -> Term name uni fun a -> Bool
isPure BuiltinSemanticsVariant DefaultFun
builtinSemantics) [Term Name DefaultUni DefaultFun ()]
terms [Bool] -> [Bool] -> Assertion
forall a. (Eq a, Show a, HasCallStack) => a -> a -> Assertion
@?= [Bool
True, Bool
True]
 where
  [Term Name DefaultUni DefaultFun ()]
terms :: [Term Name DefaultUni DefaultFun ()] =
    [ () -> DefaultFun -> Term Name DefaultUni DefaultFun ()
forall name (uni :: * -> *) fun ann.
ann -> fun -> Term name uni fun ann
Builtin () DefaultFun
Trace -- 1 type arg and 2 term args are unapplied
    , ()
-> Term Name DefaultUni DefaultFun ()
-> Term Name DefaultUni DefaultFun ()
forall name (uni :: * -> *) fun ann.
ann -> Term name uni fun ann -> Term name uni fun ann
Force () (() -> DefaultFun -> Term Name DefaultUni DefaultFun ()
forall name (uni :: * -> *) fun ann.
ann -> fun -> Term name uni fun ann
Builtin () DefaultFun
FstPair) -- 2 type args, 1 applied and 1 left
    ]

testNoTypeSomeTermArgsLeft :: TestTree
testNoTypeSomeTermArgsLeft :: TestTree
testNoTypeSomeTermArgsLeft =
  String -> Assertion -> TestTree
testCase String
"no type args and some term args are unapplied" (Assertion -> TestTree) -> Assertion -> TestTree
forall a b. (a -> b) -> a -> b
$
    (Term Name DefaultUni DefaultFun () -> Bool)
-> [Term Name DefaultUni DefaultFun ()] -> [Bool]
forall a b. (a -> b) -> [a] -> [b]
map (BuiltinSemanticsVariant DefaultFun
-> Term Name DefaultUni DefaultFun () -> Bool
forall (uni :: * -> *) fun name a.
ToBuiltinMeaning uni fun =>
BuiltinSemanticsVariant fun -> Term name uni fun a -> Bool
isPure BuiltinSemanticsVariant DefaultFun
builtinSemantics) [Term Name DefaultUni DefaultFun ()]
terms [Bool] -> [Bool] -> Assertion
forall a. (Eq a, Show a, HasCallStack) => a -> a -> Assertion
@?= [Bool
True, Bool
True]
 where
  [Term Name DefaultUni DefaultFun ()]
terms :: [Term Name DefaultUni DefaultFun ()] =
    [ () -> DefaultFun -> Term Name DefaultUni DefaultFun ()
forall name (uni :: * -> *) fun ann.
ann -> fun -> Term name uni fun ann
Builtin () DefaultFun
EncodeUtf8 -- no type args, 1 term arg left to apply
    , ()
-> Term Name DefaultUni DefaultFun ()
-> Term Name DefaultUni DefaultFun ()
forall name (uni :: * -> *) fun ann.
ann -> Term name uni fun ann -> Term name uni fun ann
Force () (() -> DefaultFun -> Term Name DefaultUni DefaultFun ()
forall name (uni :: * -> *) fun ann.
ann -> fun -> Term name uni fun ann
Builtin () DefaultFun
Trace) -- 1 type arg applied, 2 term args left
    ]

testNoTypeNoTermArgsLeft :: TestTree
testNoTypeNoTermArgsLeft :: TestTree
testNoTypeNoTermArgsLeft =
  String -> [TestTree] -> TestTree
testGroup
    String
"no type args and no term args are unapplied"
    [ TestTree
testAddInteger
    , TestTree
testIfThenElse
    ]
 where
  TestTree
testAddInteger :: TestTree =
    String -> Assertion -> TestTree
testCase String
"AddInteger" (Assertion -> TestTree) -> Assertion -> TestTree
forall a b. (a -> b) -> a -> b
$ BuiltinSemanticsVariant DefaultFun
-> Term Name DefaultUni DefaultFun () -> Bool
forall (uni :: * -> *) fun name a.
ToBuiltinMeaning uni fun =>
BuiltinSemanticsVariant fun -> Term name uni fun a -> Bool
isPure BuiltinSemanticsVariant DefaultFun
builtinSemantics Term Name DefaultUni DefaultFun ()
term Bool -> Bool -> Assertion
forall a. (Eq a, Show a, HasCallStack) => a -> a -> Assertion
@?= Bool
False
   where
    Term Name DefaultUni DefaultFun ()
term :: Term Name DefaultUni DefaultFun () =
      ()
-> Term Name DefaultUni DefaultFun ()
-> Term Name DefaultUni DefaultFun ()
-> Term Name DefaultUni DefaultFun ()
forall name (uni :: * -> *) fun ann.
ann
-> Term name uni fun ann
-> Term name uni fun ann
-> Term name uni fun ann
Apply () (()
-> Term Name DefaultUni DefaultFun ()
-> Term Name DefaultUni DefaultFun ()
-> Term Name DefaultUni DefaultFun ()
forall name (uni :: * -> *) fun ann.
ann
-> Term name uni fun ann
-> Term name uni fun ann
-> Term name uni fun ann
Apply () (() -> DefaultFun -> Term Name DefaultUni DefaultFun ()
forall name (uni :: * -> *) fun ann.
ann -> fun -> Term name uni fun ann
Builtin () DefaultFun
AddInteger) (Natural -> Term Name DefaultUni DefaultFun ()
termVar Natural
1)) (Natural -> Term Name DefaultUni DefaultFun ()
termVar Natural
2)

  TestTree
testIfThenElse :: TestTree =
    String -> Assertion -> TestTree
testCase String
"IfThenElseApplied" (Assertion -> TestTree) -> Assertion -> TestTree
forall a b. (a -> b) -> a -> b
$
      BuiltinSemanticsVariant DefaultFun
-> Term Name DefaultUni DefaultFun () -> Bool
forall (uni :: * -> *) fun name a.
ToBuiltinMeaning uni fun =>
BuiltinSemanticsVariant fun -> Term name uni fun a -> Bool
isPure BuiltinSemanticsVariant DefaultFun
builtinSemantics Term Name DefaultUni DefaultFun ()
termIfThenElse Bool -> Bool -> Assertion
forall a. (Eq a, Show a, HasCallStack) => a -> a -> Assertion
@?= Bool
False

testForceNoTypeParam :: TestTree
testForceNoTypeParam :: TestTree
testForceNoTypeParam =
  String -> Assertion -> TestTree
testCase String
"forcing a non-existing type param is impure" (Assertion -> TestTree) -> Assertion -> TestTree
forall a b. (a -> b) -> a -> b
$
    BuiltinSemanticsVariant DefaultFun
-> Term Any DefaultUni DefaultFun () -> Bool
forall (uni :: * -> *) fun name a.
ToBuiltinMeaning uni fun =>
BuiltinSemanticsVariant fun -> Term name uni fun a -> Bool
isPure BuiltinSemanticsVariant DefaultFun
builtinSemantics (()
-> Term Any DefaultUni DefaultFun ()
-> Term Any DefaultUni DefaultFun ()
forall name (uni :: * -> *) fun ann.
ann -> Term name uni fun ann -> Term name uni fun ann
Force () (() -> DefaultFun -> Term Any DefaultUni DefaultFun ()
forall name (uni :: * -> *) fun ann.
ann -> fun -> Term name uni fun ann
Builtin () DefaultFun
EncodeUtf8)) Bool -> Bool -> Assertion
forall a. (Eq a, Show a, HasCallStack) => a -> a -> Assertion
@?= Bool
False

testApplyNoTermParam :: TestTree
testApplyNoTermParam :: TestTree
testApplyNoTermParam =
  String -> [TestTree] -> TestTree
testGroup
    String
"invalid application of a term param is impure"
    [ String -> Assertion -> TestTree
testCase String
"when a type param is expected" (Assertion -> TestTree) -> Assertion -> TestTree
forall a b. (a -> b) -> a -> b
$
        BuiltinSemanticsVariant DefaultFun
-> Term Name DefaultUni DefaultFun () -> Bool
forall (uni :: * -> *) fun name a.
ToBuiltinMeaning uni fun =>
BuiltinSemanticsVariant fun -> Term name uni fun a -> Bool
isPure BuiltinSemanticsVariant DefaultFun
builtinSemantics Term Name DefaultUni DefaultFun ()
termExpectingType Bool -> Bool -> Assertion
forall a. (Eq a, Show a, HasCallStack) => a -> a -> Assertion
@?= Bool
False
    , String -> Assertion -> TestTree
testCase String
"when a builtin is saturated" (Assertion -> TestTree) -> Assertion -> TestTree
forall a b. (a -> b) -> a -> b
$
        BuiltinSemanticsVariant DefaultFun
-> Term Name DefaultUni DefaultFun () -> Bool
forall (uni :: * -> *) fun name a.
ToBuiltinMeaning uni fun =>
BuiltinSemanticsVariant fun -> Term name uni fun a -> Bool
isPure BuiltinSemanticsVariant DefaultFun
builtinSemantics Term Name DefaultUni DefaultFun ()
termSaturated Bool -> Bool -> Assertion
forall a. (Eq a, Show a, HasCallStack) => a -> a -> Assertion
@?= Bool
False
    ]
 where
  Term Name DefaultUni DefaultFun ()
termExpectingType :: Term Name DefaultUni DefaultFun () =
    ()
-> Term Name DefaultUni DefaultFun ()
-> Term Name DefaultUni DefaultFun ()
-> Term Name DefaultUni DefaultFun ()
forall name (uni :: * -> *) fun ann.
ann
-> Term name uni fun ann
-> Term name uni fun ann
-> Term name uni fun ann
Apply () (() -> DefaultFun -> Term Name DefaultUni DefaultFun ()
forall name (uni :: * -> *) fun ann.
ann -> fun -> Term name uni fun ann
Builtin () DefaultFun
Trace) (Natural -> Term Name DefaultUni DefaultFun ()
termVar Natural
1)
  Term Name DefaultUni DefaultFun ()
termSaturated :: Term Name DefaultUni DefaultFun () =
    ()
-> Term Name DefaultUni DefaultFun ()
-> Term Name DefaultUni DefaultFun ()
-> Term Name DefaultUni DefaultFun ()
forall name (uni :: * -> *) fun ann.
ann
-> Term name uni fun ann
-> Term name uni fun ann
-> Term name uni fun ann
Apply () (() -> DefaultFun -> Term Name DefaultUni DefaultFun ()
forall name (uni :: * -> *) fun ann.
ann -> fun -> Term name uni fun ann
Builtin () DefaultFun
EncodeUtf8) (Natural -> Term Name DefaultUni DefaultFun ()
termVar Natural
1)