-- SPDX-FileCopyrightText: 2021 Oxhead Alpha
-- SPDX-License-Identifier: LicenseRef-MIT-OA

{-# OPTIONS_GHC -Wno-unticked-promoted-constructors #-}
{-# OPTIONS_HADDOCK not-home #-}

-- | This module is introduced to break some cycles in "Lorentz.Lambda"
module Lorentz.Instr.Framed
  ( framed
  ) where

import Prelude hiding
  (EQ, GT, LT, abs, and, compare, concat, drop, get, map, not, or, some, swap, xor)

import Data.Constraint ((\\))

import Lorentz.Base
import Morley.Michelson.Typed hiding (Contract, pattern S)
import Morley.Util.Type

-- | Execute given instruction on truncated stack.
--
-- This instruction requires you to specify the piece of stack to truncate
-- as type argument.
framed
  :: forall s i o.
      (KnownList i, KnownList o)
  => (i :-> o) -> ((i ++ s) :-> (o ++ s))
framed (iNonFailingCode -> i) =
  I $ FrameInstr (Proxy @(ToTs s)) i
    \\ totsKnownLemma @i
    \\ totsAppendLemma @i @s
    \\ totsAppendLemma @o @s