-- 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.
--
-- The complexity of this operation is linear in the number of instructions. If
-- possible, avoid nested uses as that would imply multiple traversals. Worst
-- case, complexity can become quadratic.
framed
  :: forall s i o.
      (KnownList i, KnownList o)
  => (i :-> o) -> ((i ++ s) :-> (o ++ s))
framed :: forall (s :: [*]) (i :: [*]) (o :: [*]).
(KnownList i, KnownList o) =>
(i :-> o) -> (i ++ s) :-> (o ++ s)
framed ((i :-> o) -> Instr (ToTs i) (ToTs o)
forall (inp :: [*]) (out :: [*]).
HasCallStack =>
(inp :-> out) -> Instr (ToTs inp) (ToTs out)
iNonFailingCode -> Instr (ToTs i) (ToTs o)
i) =
  Instr (ToTs (i ++ s)) (ToTs (o ++ s)) -> (i ++ s) :-> (o ++ s)
forall (inp :: [*]) (out :: [*]).
Instr (ToTs inp) (ToTs out) -> inp :-> out
I (Instr (ToTs (i ++ s)) (ToTs (o ++ s)) -> (i ++ s) :-> (o ++ s))
-> Instr (ToTs (i ++ s)) (ToTs (o ++ s)) -> (i ++ s) :-> (o ++ s)
forall a b. (a -> b) -> a -> b
$ forall (s :: [T]) (a :: [T]) (b :: [T]).
Instr a b -> Instr (a ++ s) (b ++ s)
frameInstr @(ToTs s) Instr (ToTs i) (ToTs o)
i
    (KnownList (ToTs i) => Instr (ToTs (i ++ s)) (ToTs (o ++ s)))
-> (KnownList i :- KnownList (ToTs i))
-> Instr (ToTs (i ++ s)) (ToTs (o ++ s))
forall (c :: Constraint) e r. HasDict c e => (c => r) -> e -> r
\\ forall (s :: [*]). KnownList s :- KnownList (ToTs s)
totsKnownLemma @i
    ((ToTs (i ++ s) ~ (ToTs i ++ ToTs s)) =>
 Instr (ToTs (i ++ s)) (ToTs (o ++ s)))
-> Dict (ToTs (i ++ s) ~ (ToTs i ++ ToTs s))
-> Instr (ToTs (i ++ s)) (ToTs (o ++ s))
forall (c :: Constraint) e r. HasDict c e => (c => r) -> e -> r
\\ forall (a :: [*]) (b :: [*]).
KnownList a =>
Dict (ToTs (a ++ b) ~ (ToTs a ++ ToTs b))
totsAppendLemma @i @s
    ((ToTs (o ++ s) ~ (ToTs o ++ ToTs s)) =>
 Instr (ToTs (i ++ s)) (ToTs (o ++ s)))
-> Dict (ToTs (o ++ s) ~ (ToTs o ++ ToTs s))
-> Instr (ToTs (i ++ s)) (ToTs (o ++ s))
forall (c :: Constraint) e r. HasDict c e => (c => r) -> e -> r
\\ forall (a :: [*]) (b :: [*]).
KnownList a =>
Dict (ToTs (a ++ b) ~ (ToTs a ++ ToTs b))
totsAppendLemma @o @s