-- 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 (..)
  , Contract (..)
  , toMichelsonContract
  , Lambda
  ) where

import Data.Default (def)
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, typeCheckingWith)
import Michelson.Typed
  (Instr(..), IsoValue(..), Operation, RemFail(..), ToT, ToTs, Value, rfAnyInstr, rfMapAnyInstr,
  rfMerge)
import qualified Michelson.Typed as M (Contract(..))
import qualified Michelson.Untyped as U
import Michelson.Printer.Util (RenderDoc (..), buildRenderDocExtended)
import Morley.Micheline (ToExpression(..))

-- | 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

-- | 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 annots (LorentzInstr i) = case i of
  RfNormal instr -> LorentzInstr $ RfNormal $
    InstrWithVarNotes (NE.fromList $ map U.UnsafeAnnotation annots) instr
  RfAlwaysFails instr -> LorentzInstr $ RfAlwaysFails $
    InstrWithVarNotes (NE.fromList $ map U.UnsafeAnnotation annots) instr

-- 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)]
type ContractCode cp st = '[(cp, st)] :-> ContractOut st

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

-- | Compiled Lorentz contract.
data Contract cp st =
  (NiceParameterFull cp, NiceStorage st) =>
  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 'ContractDoc' but Lorentz code because the latter is
    -- easier to modify.
  , cDocumentedCode :: ~(ContractCode cp st)
  }

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

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

-- | Demote Lorentz 'Contract' to Michelson typed 'M.Contract'.
toMichelsonContract :: Contract cp st -> 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 '(:#)' 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 #

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

-- | 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
  => Text
  -> Either ParseLorentzError v
parseLorentzValue =
  fmap fromVal . (toTyped <=< first ParseLorentzParseError . parseExpandValue)
  where
    toTyped :: U.Value -> Either ParseLorentzError (Value (ToT v))
    toTyped =
      first ParseLorentzTypecheckError .
      typeCheckingWith def .
      runTypeCheckIsolated .
      usingReaderT (def @InstrCallStack) .
      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