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

{-# OPTIONS_GHC -Wno-redundant-constraints #-}

-- | Foundation of Lorentz development.
module Lorentz.Base
  ( (:->) (..)
  , type (%>)
  , type (&)
  , (#)
  , (##)
  , pattern I
  , pattern FI
  , iGenericIf
  , iAnyCode
  , iNonFailingCode
  , iMapAnyCode
  , iForceNotFail
  , iWithVarAnnotations

  , parseLorentzValue
  , transformStringsLorentz
  , transformBytesLorentz
  , optimizeLorentz
  , optimizeLorentzWithConf
  , MapLorentzInstr (..)

  , ContractOut
  , ContractCode
  , SomeContractCode (..)
  , Lambda
  ) where

import Data.Default (def)
import qualified Data.Kind as Kind
import qualified Data.List.NonEmpty as NE (fromList)
import Fmt (Buildable(..))

import Lorentz.Constraints
import Michelson.ErrorPos (InstrCallStack)
import Michelson.Optimizer (OptimizerConf, optimizeWithConf)
import Michelson.Parser (ParserException, parseExpandValue)
import Michelson.Preprocess (transformBytes, transformStrings)
import Michelson.Text (MText)
import Michelson.TypeCheck (TCError, runTypeCheckIsolated, typeCheckValue)
import Michelson.Typed
  (Instr(..), IsoValue(..), Operation, RemFail(..), ToT, ToTs, Value, rfAnyInstr, rfMapAnyInstr,
  rfMerge)
import qualified Michelson.Untyped as U

-- | Alias for instruction which hides inner types representation via 'T'.
newtype (inp :: [Kind.Type]) :-> (out :: [Kind.Type]) = LorentzInstr
  { (inp :-> out) -> RemFail Instr (ToTs inp) (ToTs out)
unLorentzInstr :: RemFail Instr (ToTs inp) (ToTs out)
  } deriving newtype (Int -> (inp :-> out) -> ShowS
[inp :-> out] -> ShowS
(inp :-> out) -> String
(Int -> (inp :-> out) -> ShowS)
-> ((inp :-> out) -> String)
-> ([inp :-> out] -> ShowS)
-> Show (inp :-> out)
forall (inp :: [*]) (out :: [*]). Int -> (inp :-> out) -> ShowS
forall (inp :: [*]) (out :: [*]). [inp :-> out] -> ShowS
forall (inp :: [*]) (out :: [*]). (inp :-> out) -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [inp :-> out] -> ShowS
$cshowList :: forall (inp :: [*]) (out :: [*]). [inp :-> out] -> ShowS
show :: (inp :-> out) -> String
$cshow :: forall (inp :: [*]) (out :: [*]). (inp :-> out) -> String
showsPrec :: Int -> (inp :-> out) -> ShowS
$cshowsPrec :: forall (inp :: [*]) (out :: [*]). Int -> (inp :-> out) -> ShowS
Show, (inp :-> out) -> (inp :-> out) -> Bool
((inp :-> out) -> (inp :-> out) -> Bool)
-> ((inp :-> out) -> (inp :-> out) -> Bool) -> Eq (inp :-> out)
forall (inp :: [*]) (out :: [*]).
(inp :-> out) -> (inp :-> out) -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: (inp :-> out) -> (inp :-> out) -> Bool
$c/= :: forall (inp :: [*]) (out :: [*]).
(inp :-> out) -> (inp :-> out) -> Bool
== :: (inp :-> out) -> (inp :-> out) -> Bool
$c== :: forall (inp :: [*]) (out :: [*]).
(inp :-> out) -> (inp :-> out) -> Bool
Eq)
infixr 1 :->

instance Semigroup (s :-> s) where
  <> :: (s :-> s) -> (s :-> s) -> s :-> s
(<>) = (s :-> s) -> (s :-> s) -> s :-> s
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
(#)
instance Monoid (s :-> s) where
  mempty :: s :-> s
mempty = Instr (ToTs s) (ToTs s) -> s :-> s
forall (inp :: [*]) (out :: [*]).
Instr (ToTs inp) (ToTs out) -> inp :-> out
I Instr (ToTs s) (ToTs s)
forall (inp :: [T]). Instr inp inp
Nop

pattern I :: Instr (ToTs inp) (ToTs out) -> inp :-> out
pattern $bI :: Instr (ToTs inp) (ToTs out) -> inp :-> out
$mI :: forall r (inp :: [*]) (out :: [*]).
(inp :-> out)
-> (Instr (ToTs inp) (ToTs out) -> r) -> (Void# -> r) -> r
I i = LorentzInstr (RfNormal i)

pattern FI :: (forall out'. Instr (ToTs inp) out') -> inp :-> out
pattern $bFI :: (forall (out' :: [T]). Instr (ToTs inp) out') -> inp :-> out
$mFI :: forall r (inp :: [*]) (out :: [*]).
(inp :-> out)
-> ((forall (out' :: [T]). Instr (ToTs inp) out') -> r)
-> (Void# -> r)
-> r
FI i = LorentzInstr (RfAlwaysFails i)

{-# COMPLETE I, FI #-}

iGenericIf
  :: (forall s'. Instr (ToTs a) s' -> Instr (ToTs b) s' -> Instr (ToTs c) s')
  -> (a :-> s) -> (b :-> s) -> (c :-> s)
iGenericIf :: (forall (s' :: [T]).
 Instr (ToTs a) s' -> Instr (ToTs b) s' -> Instr (ToTs c) s')
-> (a :-> s) -> (b :-> s) -> c :-> s
iGenericIf merger :: forall (s' :: [T]).
Instr (ToTs a) s' -> Instr (ToTs b) s' -> Instr (ToTs c) s'
merger (LorentzInstr instr1 :: RemFail Instr (ToTs a) (ToTs s)
instr1) (LorentzInstr instr2 :: RemFail Instr (ToTs b) (ToTs s)
instr2) =
  RemFail Instr (ToTs c) (ToTs s) -> c :-> s
forall (inp :: [*]) (out :: [*]).
RemFail Instr (ToTs inp) (ToTs out) -> inp :-> out
LorentzInstr ((forall (s' :: [T]).
 Instr (ToTs a) s' -> Instr (ToTs b) s' -> Instr (ToTs c) s')
-> RemFail Instr (ToTs a) (ToTs s)
-> RemFail Instr (ToTs b) (ToTs s)
-> RemFail Instr (ToTs c) (ToTs s)
forall k (instr :: k -> k -> *) (i1 :: k) (i2 :: k) (i3 :: k)
       (o :: k).
(forall (o' :: k). instr i1 o' -> instr i2 o' -> instr i3 o')
-> RemFail instr i1 o -> RemFail instr i2 o -> RemFail instr i3 o
rfMerge forall (s' :: [T]).
Instr (ToTs a) s' -> Instr (ToTs b) s' -> Instr (ToTs c) s'
merger RemFail Instr (ToTs a) (ToTs s)
instr1 RemFail Instr (ToTs b) (ToTs s)
instr2)

iAnyCode :: inp :-> out -> Instr (ToTs inp) (ToTs out)
iAnyCode :: (inp :-> out) -> Instr (ToTs inp) (ToTs out)
iAnyCode = RemFail Instr (ToTs inp) (ToTs out) -> Instr (ToTs inp) (ToTs out)
forall k (instr :: k -> k -> *) (i :: k) (o :: k).
RemFail instr i o -> instr i o
rfAnyInstr (RemFail Instr (ToTs inp) (ToTs out)
 -> Instr (ToTs inp) (ToTs out))
-> ((inp :-> out) -> RemFail Instr (ToTs inp) (ToTs out))
-> (inp :-> out)
-> Instr (ToTs inp) (ToTs out)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (inp :-> out) -> RemFail Instr (ToTs inp) (ToTs out)
forall (inp :: [*]) (out :: [*]).
(inp :-> out) -> RemFail Instr (ToTs inp) (ToTs out)
unLorentzInstr

iNonFailingCode :: HasCallStack => inp :-> out -> Instr (ToTs inp) (ToTs out)
iNonFailingCode :: (inp :-> out) -> Instr (ToTs inp) (ToTs out)
iNonFailingCode (I i :: Instr (ToTs inp) (ToTs out)
i) = Instr (ToTs inp) (ToTs out)
i
iNonFailingCode (FI _) = Text -> Instr (ToTs inp) (ToTs out)
forall a. HasCallStack => Text -> a
error "Always failing code cannot appear here"

iMapAnyCode
  :: (forall o'. Instr (ToTs i1) o' -> Instr (ToTs i2) o')
  -> (i1 :-> o)
  -> (i2 :-> o)
iMapAnyCode :: (forall (o' :: [T]). Instr (ToTs i1) o' -> Instr (ToTs i2) o')
-> (i1 :-> o) -> i2 :-> o
iMapAnyCode f :: forall (o' :: [T]). Instr (ToTs i1) o' -> Instr (ToTs i2) o'
f (LorentzInstr i :: RemFail Instr (ToTs i1) (ToTs o)
i) = RemFail Instr (ToTs i2) (ToTs o) -> i2 :-> o
forall (inp :: [*]) (out :: [*]).
RemFail Instr (ToTs inp) (ToTs out) -> inp :-> out
LorentzInstr (RemFail Instr (ToTs i2) (ToTs o) -> i2 :-> o)
-> RemFail Instr (ToTs i2) (ToTs o) -> i2 :-> o
forall a b. (a -> b) -> a -> b
$ (forall (o' :: [T]). Instr (ToTs i1) o' -> Instr (ToTs i2) o')
-> RemFail Instr (ToTs i1) (ToTs o)
-> RemFail Instr (ToTs i2) (ToTs o)
forall k (instr :: k -> k -> *) (i1 :: k) (i2 :: k) (o :: k).
(forall (o' :: k). instr i1 o' -> instr i2 o')
-> RemFail instr i1 o -> RemFail instr i2 o
rfMapAnyInstr forall (o' :: [T]). Instr (ToTs i1) o' -> Instr (ToTs i2) o'
f RemFail Instr (ToTs i1) (ToTs o)
i

iForceNotFail :: (i :-> o) -> (i :-> o)
iForceNotFail :: (i :-> o) -> i :-> o
iForceNotFail = Instr (ToTs i) (ToTs o) -> i :-> o
forall (inp :: [*]) (out :: [*]).
Instr (ToTs inp) (ToTs out) -> inp :-> out
I (Instr (ToTs i) (ToTs o) -> i :-> o)
-> ((i :-> o) -> Instr (ToTs i) (ToTs o)) -> (i :-> o) -> i :-> o
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (i :-> o) -> Instr (ToTs i) (ToTs o)
forall (inp :: [*]) (out :: [*]).
(inp :-> out) -> Instr (ToTs inp) (ToTs out)
iAnyCode

-- | Wrap Lorentz instruction with variable annotations, @annots@ list has to be
-- non-empty, otherwise this function raises an error.
iWithVarAnnotations :: HasCallStack => [Text] -> inp :-> out -> inp :-> out
iWithVarAnnotations :: [Text] -> (inp :-> out) -> inp :-> out
iWithVarAnnotations annots :: [Text]
annots (LorentzInstr i :: RemFail Instr (ToTs inp) (ToTs out)
i) = case RemFail Instr (ToTs inp) (ToTs out)
i of
  RfNormal instr :: Instr (ToTs inp) (ToTs out)
instr -> RemFail Instr (ToTs inp) (ToTs out) -> inp :-> out
forall (inp :: [*]) (out :: [*]).
RemFail Instr (ToTs inp) (ToTs out) -> inp :-> out
LorentzInstr (RemFail Instr (ToTs inp) (ToTs out) -> inp :-> out)
-> RemFail Instr (ToTs inp) (ToTs out) -> inp :-> out
forall a b. (a -> b) -> a -> b
$ Instr (ToTs inp) (ToTs out) -> RemFail Instr (ToTs inp) (ToTs out)
forall k (instr :: k -> k -> *) (i :: k) (o :: k).
instr i o -> RemFail instr i o
RfNormal (Instr (ToTs inp) (ToTs out)
 -> RemFail Instr (ToTs inp) (ToTs out))
-> Instr (ToTs inp) (ToTs out)
-> RemFail Instr (ToTs inp) (ToTs out)
forall a b. (a -> b) -> a -> b
$
    NonEmpty VarAnn
-> Instr (ToTs inp) (ToTs out) -> Instr (ToTs inp) (ToTs out)
forall (inp :: [T]) (out :: [T]).
NonEmpty VarAnn -> Instr inp out -> Instr inp out
InstrWithVarNotes ([VarAnn] -> NonEmpty VarAnn
forall a. [a] -> NonEmpty a
NE.fromList ([VarAnn] -> NonEmpty VarAnn) -> [VarAnn] -> NonEmpty VarAnn
forall a b. (a -> b) -> a -> b
$ (Text -> VarAnn) -> [Text] -> [VarAnn]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
map Text -> VarAnn
forall k (tag :: k). Text -> Annotation tag
U.AnnotationUnsafe [Text]
annots) Instr (ToTs inp) (ToTs out)
instr
  RfAlwaysFails instr :: forall (o' :: [T]). Instr (ToTs inp) o'
instr -> RemFail Instr (ToTs inp) (ToTs out) -> inp :-> out
forall (inp :: [*]) (out :: [*]).
RemFail Instr (ToTs inp) (ToTs out) -> inp :-> out
LorentzInstr (RemFail Instr (ToTs inp) (ToTs out) -> inp :-> out)
-> RemFail Instr (ToTs inp) (ToTs out) -> inp :-> out
forall a b. (a -> b) -> a -> b
$ (forall (o' :: [T]). Instr (ToTs inp) o')
-> RemFail Instr (ToTs inp) (ToTs out)
forall k (instr :: k -> k -> *) (i :: k) (o :: k).
(forall (o' :: k). instr i o') -> RemFail instr i o
RfAlwaysFails ((forall (o' :: [T]). Instr (ToTs inp) o')
 -> RemFail Instr (ToTs inp) (ToTs out))
-> (forall (o' :: [T]). Instr (ToTs inp) o')
-> RemFail Instr (ToTs inp) (ToTs out)
forall a b. (a -> b) -> a -> b
$
    NonEmpty VarAnn -> Instr (ToTs inp) o' -> Instr (ToTs inp) o'
forall (inp :: [T]) (out :: [T]).
NonEmpty VarAnn -> Instr inp out -> Instr inp out
InstrWithVarNotes ([VarAnn] -> NonEmpty VarAnn
forall a. [a] -> NonEmpty a
NE.fromList ([VarAnn] -> NonEmpty VarAnn) -> [VarAnn] -> NonEmpty VarAnn
forall a b. (a -> b) -> a -> b
$ (Text -> VarAnn) -> [Text] -> [VarAnn]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
map Text -> VarAnn
forall k (tag :: k). Text -> Annotation tag
U.AnnotationUnsafe [Text]
annots) Instr (ToTs inp) o'
forall (o' :: [T]). Instr (ToTs inp) o'
instr

-- There is also @instance IsoValue (i :-> o)@ in a separate module.

-- | Alias for ':->', seems to make signatures more readable sometimes.
--
-- Let's someday decide which one of these two should remain.
type (%>) = (:->)
infixr 1 %>

type ContractOut st = '[([Operation], st)]
type ContractCode cp st = '[(cp, st)] :-> ContractOut st

data SomeContractCode where
  SomeContractCode
    :: (NiceParameterFull cp, NiceStorage st)
    => ContractCode cp st
    -> SomeContractCode

type (&) (a :: Kind.Type) (b :: [Kind.Type]) = a ': b
infixr 2 &

(#) :: (a :-> b) -> (b :-> c) -> a :-> c
I l :: Instr (ToTs a) (ToTs b)
l # :: (a :-> b) -> (b :-> c) -> a :-> c
# I r :: Instr (ToTs b) (ToTs c)
r = Instr (ToTs a) (ToTs c) -> a :-> c
forall (inp :: [*]) (out :: [*]).
Instr (ToTs inp) (ToTs out) -> inp :-> out
I (Instr (ToTs a) (ToTs b)
l Instr (ToTs a) (ToTs b)
-> Instr (ToTs b) (ToTs c) -> Instr (ToTs a) (ToTs c)
forall (inp :: [T]) (b :: [T]) (out :: [T]).
Instr inp b -> Instr b out -> Instr inp out
`Seq` Instr (ToTs b) (ToTs c)
r)
I l :: Instr (ToTs a) (ToTs b)
l # FI r :: forall (out' :: [T]). Instr (ToTs b) out'
r = (forall (out' :: [T]). Instr (ToTs a) out') -> a :-> c
forall (inp :: [*]) (out :: [*]).
(forall (out' :: [T]). Instr (ToTs inp) out') -> inp :-> out
FI (Instr (ToTs a) (ToTs b)
l Instr (ToTs a) (ToTs b)
-> Instr (ToTs b) out' -> Instr (ToTs a) out'
forall (inp :: [T]) (b :: [T]) (out :: [T]).
Instr inp b -> Instr b out -> Instr inp out
`Seq` Instr (ToTs b) out'
forall (out' :: [T]). Instr (ToTs b) out'
r)
FI l :: forall (out' :: [T]). Instr (ToTs a) out'
l # _ = (forall (out' :: [T]). Instr (ToTs a) out') -> a :-> c
forall (inp :: [*]) (out :: [*]).
(forall (out' :: [T]). Instr (ToTs inp) out') -> inp :-> out
FI forall (out' :: [T]). Instr (ToTs a) out'
l
infixl 8 #

-- | Version of '#' which performs some optimizations immediately.
(##) :: (a :-> b) -> (b :-> c) -> (a :-> c)
l :: a :-> b
l ## :: (a :-> b) -> (b :-> c) -> a :-> c
## r :: b :-> c
r = case (a :-> b
l, b :-> c
r) of
  (I Nop, I x :: Instr (ToTs b) (ToTs c)
x) -> Instr (ToTs a) (ToTs c) -> a :-> c
forall (inp :: [*]) (out :: [*]).
Instr (ToTs inp) (ToTs out) -> inp :-> out
I Instr (ToTs a) (ToTs c)
Instr (ToTs b) (ToTs c)
x
  (I x :: Instr (ToTs a) (ToTs b)
x, I Nop) -> Instr (ToTs a) (ToTs c) -> a :-> c
forall (inp :: [*]) (out :: [*]).
Instr (ToTs inp) (ToTs out) -> inp :-> out
I Instr (ToTs a) (ToTs b)
Instr (ToTs a) (ToTs c)
x
  _ -> a :-> b
l (a :-> b) -> (b :-> c) -> a :-> c
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
# b :-> c
r


type Lambda i o = '[i] :-> '[o]

-- | Errors that can happen during parsing into a Lorentz value.
data ParseLorentzError
  = ParseLorentzParseError ParserException
  | ParseLorentzTypecheckError TCError
  deriving stock (Int -> ParseLorentzError -> ShowS
[ParseLorentzError] -> ShowS
ParseLorentzError -> String
(Int -> ParseLorentzError -> ShowS)
-> (ParseLorentzError -> String)
-> ([ParseLorentzError] -> ShowS)
-> Show ParseLorentzError
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [ParseLorentzError] -> ShowS
$cshowList :: [ParseLorentzError] -> ShowS
show :: ParseLorentzError -> String
$cshow :: ParseLorentzError -> String
showsPrec :: Int -> ParseLorentzError -> ShowS
$cshowsPrec :: Int -> ParseLorentzError -> ShowS
Show, ParseLorentzError -> ParseLorentzError -> Bool
(ParseLorentzError -> ParseLorentzError -> Bool)
-> (ParseLorentzError -> ParseLorentzError -> Bool)
-> Eq ParseLorentzError
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: ParseLorentzError -> ParseLorentzError -> Bool
$c/= :: ParseLorentzError -> ParseLorentzError -> Bool
== :: ParseLorentzError -> ParseLorentzError -> Bool
$c== :: ParseLorentzError -> ParseLorentzError -> Bool
Eq)

instance Buildable ParseLorentzError where
  build :: ParseLorentzError -> Builder
build =
    \case
      ParseLorentzParseError e :: ParserException
e -> ParserException -> Builder
forall p. Buildable p => p -> Builder
build ParserException
e
      ParseLorentzTypecheckError e :: TCError
e -> TCError -> Builder
forall p. Buildable p => p -> Builder
build TCError
e

-- | Parse textual representation of a Michelson value and turn it
-- into corresponding Haskell value.
--
-- Note: it won't work in some complex cases, e. g. if there is a
-- lambda which uses an instruction which depends on current
-- contract's type. Obviously it can not work, because we don't have
-- any information about a contract to which this value belongs (there
-- is no such contract at all).
parseLorentzValue
  :: forall v. KnownValue v
  => Text
  -> Either ParseLorentzError v
parseLorentzValue :: Text -> Either ParseLorentzError v
parseLorentzValue =
  (Value (ToT v) -> v)
-> Either ParseLorentzError (Value (ToT v))
-> Either ParseLorentzError v
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Value (ToT v) -> v
forall a. IsoValue a => Value (ToT a) -> a
fromVal (Either ParseLorentzError (Value (ToT v))
 -> Either ParseLorentzError v)
-> (Text -> Either ParseLorentzError (Value (ToT v)))
-> Text
-> Either ParseLorentzError v
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Value -> Either ParseLorentzError (Value (ToT v))
toTyped (Value -> Either ParseLorentzError (Value (ToT v)))
-> (Text -> Either ParseLorentzError Value)
-> Text
-> Either ParseLorentzError (Value (ToT v))
forall (m :: * -> *) b c a.
Monad m =>
(b -> m c) -> (a -> m b) -> a -> m c
<=< (ParserException -> ParseLorentzError)
-> Either ParserException Value -> Either ParseLorentzError Value
forall (p :: * -> * -> *) a b c.
Bifunctor p =>
(a -> b) -> p a c -> p b c
first ParserException -> ParseLorentzError
ParseLorentzParseError (Either ParserException Value -> Either ParseLorentzError Value)
-> (Text -> Either ParserException Value)
-> Text
-> Either ParseLorentzError Value
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Text -> Either ParserException Value
parseExpandValue)
  where
    toTyped :: U.Value -> Either ParseLorentzError (Value (ToT v))
    toTyped :: Value -> Either ParseLorentzError (Value (ToT v))
toTyped =
      (TCError -> ParseLorentzError)
-> Either TCError (Value (ToT v))
-> Either ParseLorentzError (Value (ToT v))
forall (p :: * -> * -> *) a b c.
Bifunctor p =>
(a -> b) -> p a c -> p b c
first TCError -> ParseLorentzError
ParseLorentzTypecheckError (Either TCError (Value (ToT v))
 -> Either ParseLorentzError (Value (ToT v)))
-> (Value -> Either TCError (Value (ToT v)))
-> Value
-> Either ParseLorentzError (Value (ToT v))
forall b c a. (b -> c) -> (a -> b) -> a -> c
.
      TypeCheck (Value (ToT v)) -> Either TCError (Value (ToT v))
forall a. TypeCheck a -> Either TCError a
runTypeCheckIsolated (TypeCheck (Value (ToT v)) -> Either TCError (Value (ToT v)))
-> (Value -> TypeCheck (Value (ToT v)))
-> Value
-> Either TCError (Value (ToT v))
forall b c a. (b -> c) -> (a -> b) -> a -> c
.
      InstrCallStack
-> ReaderT InstrCallStack TypeCheck (Value (ToT v))
-> TypeCheck (Value (ToT v))
forall r (m :: * -> *) a. r -> ReaderT r m a -> m a
usingReaderT (Default InstrCallStack => InstrCallStack
forall a. Default a => a
def @InstrCallStack) (ReaderT InstrCallStack TypeCheck (Value (ToT v))
 -> TypeCheck (Value (ToT v)))
-> (Value -> ReaderT InstrCallStack TypeCheck (Value (ToT v)))
-> Value
-> TypeCheck (Value (ToT v))
forall b c a. (b -> c) -> (a -> b) -> a -> c
.
      Value -> ReaderT InstrCallStack TypeCheck (Value (ToT v))
forall (t :: T). SingI t => Value -> TypeCheckInstr (Value t)
typeCheckValue

-- | Lorentz version of 'transformStrings'.
transformStringsLorentz ::
  Bool -> (MText -> MText) -> inp :-> out -> inp :-> out
transformStringsLorentz :: Bool -> (MText -> MText) -> (inp :-> out) -> inp :-> out
transformStringsLorentz goToValues :: Bool
goToValues f :: MText -> MText
f =
  (forall (o' :: [T]). Instr (ToTs inp) o' -> Instr (ToTs inp) o')
-> (inp :-> out) -> inp :-> out
forall (i1 :: [*]) (i2 :: [*]) (o :: [*]).
(forall (o' :: [T]). Instr (ToTs i1) o' -> Instr (ToTs i2) o')
-> (i1 :-> o) -> i2 :-> o
iMapAnyCode ((forall (o' :: [T]). Instr (ToTs inp) o' -> Instr (ToTs inp) o')
 -> (inp :-> out) -> inp :-> out)
-> (forall (o' :: [T]). Instr (ToTs inp) o' -> Instr (ToTs inp) o')
-> (inp :-> out)
-> inp :-> out
forall a b. (a -> b) -> a -> b
$ Bool
-> (MText -> MText) -> Instr (ToTs inp) o' -> Instr (ToTs inp) o'
forall (inp :: [T]) (out :: [T]).
Bool -> (MText -> MText) -> Instr inp out -> Instr inp out
transformStrings Bool
goToValues MText -> MText
f

-- | Lorentz version of 'transformBytes'.
transformBytesLorentz ::
  Bool -> (ByteString -> ByteString) -> inp :-> out -> inp :-> out
transformBytesLorentz :: Bool -> (ByteString -> ByteString) -> (inp :-> out) -> inp :-> out
transformBytesLorentz goToValues :: Bool
goToValues f :: ByteString -> ByteString
f =
  (forall (o' :: [T]). Instr (ToTs inp) o' -> Instr (ToTs inp) o')
-> (inp :-> out) -> inp :-> out
forall (i1 :: [*]) (i2 :: [*]) (o :: [*]).
(forall (o' :: [T]). Instr (ToTs i1) o' -> Instr (ToTs i2) o')
-> (i1 :-> o) -> i2 :-> o
iMapAnyCode ((forall (o' :: [T]). Instr (ToTs inp) o' -> Instr (ToTs inp) o')
 -> (inp :-> out) -> inp :-> out)
-> (forall (o' :: [T]). Instr (ToTs inp) o' -> Instr (ToTs inp) o')
-> (inp :-> out)
-> inp :-> out
forall a b. (a -> b) -> a -> b
$ Bool
-> (ByteString -> ByteString)
-> Instr (ToTs inp) o'
-> Instr (ToTs inp) o'
forall (inp :: [T]) (out :: [T]).
Bool
-> (ByteString -> ByteString) -> Instr inp out -> Instr inp out
transformBytes Bool
goToValues ByteString -> ByteString
f

optimizeLorentzWithConf
  :: OptimizerConf
  -> inp :-> out
  -> inp :-> out
optimizeLorentzWithConf :: OptimizerConf -> (inp :-> out) -> inp :-> out
optimizeLorentzWithConf conf :: OptimizerConf
conf =
  -- Optimizer can produce dead code.
  -- Example: @push True # if_ failWith nop # ...@ will fold to @failWith # ...@.
  -- But let's not care about this case for now until need in it fires.
  (forall (o' :: [T]). Instr (ToTs inp) o' -> Instr (ToTs inp) o')
-> (inp :-> out) -> inp :-> out
forall (i1 :: [*]) (i2 :: [*]) (o :: [*]).
(forall (o' :: [T]). Instr (ToTs i1) o' -> Instr (ToTs i2) o')
-> (i1 :-> o) -> i2 :-> o
iMapAnyCode (OptimizerConf -> Instr (ToTs inp) o' -> Instr (ToTs inp) o'
forall (inp :: [T]) (out :: [T]).
OptimizerConf -> Instr inp out -> Instr inp out
optimizeWithConf OptimizerConf
conf)

optimizeLorentz
  :: inp :-> out
  -> inp :-> out
optimizeLorentz :: (inp :-> out) -> inp :-> out
optimizeLorentz = OptimizerConf -> (inp :-> out) -> inp :-> out
forall (inp :: [*]) (out :: [*]).
OptimizerConf -> (inp :-> out) -> inp :-> out
optimizeLorentzWithConf OptimizerConf
forall a. Default a => a
def

-- | Applicable for wrappers over Lorentz code.
class MapLorentzInstr instr where
  -- | Modify all the code under given entity.
  mapLorentzInstr :: (forall i o. (i :-> o) -> (i :-> o)) -> instr -> instr

instance MapLorentzInstr (i :-> o) where
  mapLorentzInstr :: (forall (i :: [*]) (o :: [*]). (i :-> o) -> i :-> o)
-> (i :-> o) -> i :-> o
mapLorentzInstr f :: forall (i :: [*]) (o :: [*]). (i :-> o) -> i :-> o
f = (i :-> o) -> i :-> o
forall (i :: [*]) (o :: [*]). (i :-> o) -> i :-> o
f