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

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

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

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

  , ContractOut
  , ContractCode (..)
  , mkContractCode
  , IsNotInView
  , SomeContractCode (..)
  , ViewCode
  , Contract (..)
  , toMichelsonContract
  , Fn
  ) where

import Data.Default (def)
import Fmt (Buildable(..))

import Lorentz.Constraints
import Morley.Micheline (ToExpression(..))
import Morley.Michelson.Optimizer (OptimizerConf, optimizeWithConf)
import Morley.Michelson.Parser (MichelsonSource, ParserException, parseExpandValue)
import Morley.Michelson.Preprocess (transformBytes, transformStrings)
import Morley.Michelson.Printer.Util (RenderDoc(..), buildRenderDocExtended)
import Morley.Michelson.Text (MText)
import Morley.Michelson.TypeCheck (TCError, typeCheckValue, typeCheckingWith)
import Morley.Michelson.Typed
  (Instr(..), IsNotInView, IsoValue(..), Operation, RemFail(..), ToT, ToTs, Value, rfAnyInstr,
  rfMapAnyInstr, rfMerge)
import Morley.Michelson.Typed qualified as M (Contract)
import Morley.Michelson.Typed.Contract (giveNotInView)
import Morley.Michelson.Untyped qualified as U

-- | Alias for instruction which hides inner types representation via @T@.
newtype (inp :: [Type]) :-> (out :: [Type]) = LorentzInstr
  { unLorentzInstr :: RemFail Instr (ToTs inp) (ToTs out)
  } deriving newtype (Show, Eq)
infixr 1 :->

instance Buildable (inp :-> out) where
  build = buildRenderDocExtended

instance RenderDoc (inp :-> out) where
  renderDoc context = renderDoc context . iAnyCode

instance NFData (i :-> o) where
  rnf (LorentzInstr i) = rnf i

instance Semigroup (s :-> s) where
  (<>) = (#)
instance Monoid (s :-> s) where
  mempty = I Nop

pattern I :: Instr (ToTs inp) (ToTs out) -> inp :-> out
pattern I i = LorentzInstr (RfNormal i)

pattern FI :: (forall out'. Instr (ToTs inp) out') -> inp :-> out
pattern 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 merger (LorentzInstr instr1) (LorentzInstr instr2) =
  LorentzInstr (rfMerge merger instr1 instr2)

iAnyCode :: inp :-> out -> Instr (ToTs inp) (ToTs out)
iAnyCode = rfAnyInstr . unLorentzInstr

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

iMapAnyCode
  :: (forall o'. Instr (ToTs i1) o' -> Instr (ToTs i2) o')
  -> (i1 :-> o)
  -> (i2 :-> o)
iMapAnyCode f (LorentzInstr i) = LorentzInstr $ rfMapAnyInstr f i

iForceNotFail :: (i :-> o) -> (i :-> o)
iForceNotFail = I . iAnyCode

-- There is also @instance IsoValue (i :-> o)@ in the "Lorentz.Zip" 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)]

-- | Wrap contract code capturing the constraint that the code is not inside a
-- view.
newtype ContractCode cp st = ContractCode
  { unContractCode :: '[(cp, st)] :-> ContractOut st }
  deriving stock (Show, Eq)
  deriving newtype NFData

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

type ViewCode arg st ret = '[(arg, st)] :-> '[ret]

-- | A helper to construct 'ContractCode' that provides 'IsNotInView' constraint.
mkContractCode :: (IsNotInView => '[(cp, st)] :-> ContractOut st) -> ContractCode cp st
mkContractCode x = ContractCode $ giveNotInView x

-- | Compiled Lorentz contract.
--
-- Note, that the views argument (views descriptor) is added comparing to the
-- Michelson. In Michelson, ability to call a view is fully checked at runtime,
-- but in Lorentz we want to make calls safer at compile-time.
data Contract cp st vd =
  (NiceParameter cp, NiceStorage st, NiceViewsDescriptor vd) =>
  Contract
  { -- | Ready contract code.
    cMichelsonContract :: M.Contract (ToT cp) (ToT st)

    -- | Contract that contains documentation.
    --
    -- We have to keep it separately, since optimizer is free to destroy
    -- documentation blocks.
    -- Also, it is not 'Lorentz.Doc.ContractDoc' but Lorentz code because the latter is
    -- easier to modify.
  , cDocumentedCode :: ~(ContractCode cp st)
  }

deriving stock instance Show (Contract cp st vd)
deriving stock instance Eq (Contract cp st vd)
instance NFData (Contract cp st vd) where
  rnf (Contract c d) = rnf c `seq` rnf d

instance ToExpression (Contract cp st vd) where
  toExpression = toExpression . toMichelsonContract

-- | Demote Lorentz 'Contract' to Michelson typed 'M.Contract'.
toMichelsonContract :: Contract cp st vd -> M.Contract (ToT cp) (ToT st)
toMichelsonContract = cMichelsonContract

-- | An alias for @':@.
--
-- We discourage its use as this hinders reading error messages
-- (the compiler inserts unnecessary parentheses and indentation).
type (&) (a :: Type) (b :: [Type]) = a ': b
infixr 2 &

-- | Function composition for instructions.
--
-- Note that, unlike Morley's 'Morley.Michelson.Typed.Instr.:#' operator, '(#)' is left-associative.
(#) :: (a :-> b) -> (b :-> c) -> a :-> c
I l # I r = I (l `Seq` r)
I l # FI r = FI (l `Seq` r)
FI l # _ = FI l
infixl 8 #

-- | An instruction sequence taking one stack element as input and returning one
-- stack element as output. Essentially behaves as a Michelson lambda without
-- any additional semantical meaning.
--
-- The reason for this distinction is Michelson lambdas allow instructions
-- inside them that might be forbidden in the outer scope. This type doesn't add
-- any such conditions.
type Fn a b = '[a] :-> '[b]

-- | Errors that can happen during parsing into a Lorentz value.
data ParseLorentzError
  = ParseLorentzParseError ParserException
  | ParseLorentzTypecheckError TCError
  deriving stock (Show, Eq)

instance Buildable ParseLorentzError where
  build =
    \case
      ParseLorentzParseError e -> build e
      ParseLorentzTypecheckError e -> build 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
  => MichelsonSource
  -> Text
  -> Either ParseLorentzError v
parseLorentzValue src =
  fmap fromVal . (toTyped <=< first ParseLorentzParseError . parseExpandValue src)
  where
    toTyped :: U.Value -> Either ParseLorentzError (Value (ToT v))
    toTyped =
      first ParseLorentzTypecheckError .
      typeCheckingWith def .
      typeCheckValue

-- | Lorentz version of 'transformStrings'.
transformStringsLorentz ::
  Bool -> (MText -> MText) -> inp :-> out -> inp :-> out
transformStringsLorentz goToValues f =
  iMapAnyCode $ transformStrings goToValues f

-- | Lorentz version of 'transformBytes'.
transformBytesLorentz ::
  Bool -> (ByteString -> ByteString) -> inp :-> out -> inp :-> out
transformBytesLorentz goToValues f =
  iMapAnyCode $ transformBytes goToValues f

optimizeLorentzWithConf
  :: OptimizerConf
  -> inp :-> out
  -> inp :-> out
optimizeLorentzWithConf 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.
  iMapAnyCode (optimizeWithConf conf)

optimizeLorentz
  :: inp :-> out
  -> inp :-> out
optimizeLorentz = optimizeLorentzWithConf 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 f = f