packages feed

cleveland-0.1.0: lorentz-test/Test/Lorentz/Optimizer.hs

-- SPDX-FileCopyrightText: 2020 Tocqueville Group
--
-- SPDX-License-Identifier: LicenseRef-MIT-TQ

-- | Tests for optimization of Lorentz-specific instruction sequences.
module Test.Lorentz.Optimizer
  ( unit_eq0
  , unit_non
  , unit_stGet
  ) where

import Lorentz ((#), (:->))
import qualified Lorentz as L
import Morley.Michelson.Optimizer (optimize)
import Morley.Michelson.Typed.Util (linearizeLeft)
import Test.HUnit (Assertion, (@?=))

-- | Check whether code on left hand side optimizes to the code on
-- the right hand side.
infix 1 ->?=
(->?=) :: i :-> o -> i :-> o -> Assertion
(L.iAnyCode -> pre) ->?= (L.iAnyCode -> post) =
  linearizeLeft (optimize pre) @?= linearizeLeft post

unit_eq0 :: Assertion
unit_eq0 =
  L.push @Integer 0 # L.eq ->?= L.eq0

unit_non :: Assertion
unit_non =
  L.non @Integer 0 ->?= L.nonZero

-- TODO [#300]: this test fails because the optimizer seemingly doesn't revisit the
-- optimized instruction after one rule application, e.g. here the adjacent DIPs
-- rule is applied, but not the 'isSome after if' one.
-- unit_stUpdate :: Assertion
-- unit_stUpdate =
--   L.dip (L.if_ (L.push (Just @Integer 0)) (L.push Nothing)) # L.stUpdate L.this ->?= update'
--     where
--       update' :: (Integer : Bool : Set Integer : s) :-> (Set Integer : s)
--       update' = L.update

unit_stGet :: Assertion
unit_stGet =
  L.stGet L.this # L.isSome ->?= mem'
    where
      mem' :: (Integer : Set Integer : s) :-> (Bool : s)
      mem' = L.mem