{-# LANGUAGE UndecidableInstances #-}
{-# OPTIONS_GHC -Wno-orphans #-}

module Plutarch.Extra.RationalData (
  PRationalData,
  prationalFromData,
) where

import Data.Bifunctor (first)

import Plutarch.Builtin (pasConstr)
import Plutarch.DataRepr (DerivePConstantViaData (DerivePConstantViaData), PDataFields)
import Plutarch.Extra.TermCont (pguardC, pletC, pletFieldsC)
import Plutarch.Lift (PConstantDecl, PUnsafeLiftDecl (PLifted))
import Plutarch.Positive (PPositive)
import Plutarch.Prelude
import Plutarch.TryFrom (PTryFrom (PTryFromExcess, ptryFrom'))
import qualified Plutarch.Unsafe as PUNSAFE
import qualified PlutusTx.Ratio as Plutus

-- | A Rational type that corresponds to the data encoding used by 'Plutus.Rational'.
newtype PRationalData s
  = PRationalData
      ( Term
          s
          ( PDataRecord
              '[ "numerator" ':= PInteger
               , "denominator" ':= PPositive
               ]
          )
      )
  deriving stock (forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall (s :: S) x. Rep (PRationalData s) x -> PRationalData s
forall (s :: S) x. PRationalData s -> Rep (PRationalData s) x
$cto :: forall (s :: S) x. Rep (PRationalData s) x -> PRationalData s
$cfrom :: forall (s :: S) x. PRationalData s -> Rep (PRationalData s) x
Generic)
  deriving anyclass (forall (s :: S). PRationalData s -> Term s (PInner PRationalData)
forall (s :: S) (b :: PType).
Term s (PInner PRationalData)
-> (PRationalData s -> Term s b) -> Term s b
forall (a :: PType).
(forall (s :: S). a s -> Term s (PInner a))
-> (forall (s :: S) (b :: PType).
    Term s (PInner a) -> (a s -> Term s b) -> Term s b)
-> PlutusType a
pmatch' :: forall (s :: S) (b :: PType).
Term s (PInner PRationalData)
-> (PRationalData s -> Term s b) -> Term s b
$cpmatch' :: forall (s :: S) (b :: PType).
Term s (PInner PRationalData)
-> (PRationalData s -> Term s b) -> Term s b
pcon' :: forall (s :: S). PRationalData s -> Term s (PInner PRationalData)
$cpcon' :: forall (s :: S). PRationalData s -> Term s (PInner PRationalData)
PlutusType, forall (s :: S).
Term s (PAsData PRationalData) -> Term s PRationalData
forall (s :: S). Term s PRationalData -> Term s PData
forall (a :: PType).
(forall (s :: S). Term s (PAsData a) -> Term s a)
-> (forall (s :: S). Term s a -> Term s PData) -> PIsData a
pdataImpl :: forall (s :: S). Term s PRationalData -> Term s PData
$cpdataImpl :: forall (s :: S). Term s PRationalData -> Term s PData
pfromDataImpl :: forall (s :: S).
Term s (PAsData PRationalData) -> Term s PRationalData
$cpfromDataImpl :: forall (s :: S).
Term s (PAsData PRationalData) -> Term s PRationalData
PIsData, forall (s :: S).
Term s PRationalData
-> Term s (PDataRecord (PFields PRationalData))
forall (a :: PType).
(forall (s :: S). Term s a -> Term s (PDataRecord (PFields a)))
-> PDataFields a
ptoFields :: forall (s :: S).
Term s PRationalData
-> Term s (PDataRecord (PFields PRationalData))
$cptoFields :: forall (s :: S).
Term s PRationalData
-> Term s (PDataRecord (PFields PRationalData))
PDataFields, forall (s :: S).
Term s PRationalData -> Term s PRationalData -> Term s PBool
forall (t :: PType).
(forall (s :: S). Term s t -> Term s t -> Term s PBool) -> PEq t
#== :: forall (s :: S).
Term s PRationalData -> Term s PRationalData -> Term s PBool
$c#== :: forall (s :: S).
Term s PRationalData -> Term s PRationalData -> Term s PBool
PEq, PEq PRationalData
forall (s :: S).
Term s PRationalData -> Term s PRationalData -> Term s PBool
forall (t :: PType).
PEq t
-> (forall (s :: S). Term s t -> Term s t -> Term s PBool)
-> (forall (s :: S). Term s t -> Term s t -> Term s PBool)
-> PPartialOrd t
#< :: forall (s :: S).
Term s PRationalData -> Term s PRationalData -> Term s PBool
$c#< :: forall (s :: S).
Term s PRationalData -> Term s PRationalData -> Term s PBool
#<= :: forall (s :: S).
Term s PRationalData -> Term s PRationalData -> Term s PBool
$c#<= :: forall (s :: S).
Term s PRationalData -> Term s PRationalData -> Term s PBool
PPartialOrd, PPartialOrd PRationalData
forall (t :: PType). PPartialOrd t -> POrd t
POrd)

instance DerivePlutusType PRationalData where type DPTStrat _ = PlutusTypeData

instance PUnsafeLiftDecl PRationalData where type PLifted PRationalData = Plutus.Rational
deriving via (DerivePConstantViaData Plutus.Rational PRationalData) instance PConstantDecl Plutus.Rational

instance PTryFrom PData PRationalData where
  type PTryFromExcess PData PRationalData = Flip Term PPositive
  ptryFrom' :: forall (s :: S) (r :: PType).
Term s PData
-> ((Term s PRationalData,
     Reduce (PTryFromExcess PData PRationalData s))
    -> Term s r)
-> Term s r
ptryFrom' Term s PData
opq (Term s PRationalData,
 Reduce (PTryFromExcess PData PRationalData s))
-> Term s r
cont = forall (b :: PType) (a :: PType) (s :: S) (r :: PType).
PTryFrom a b =>
Term s a
-> ((Term s b, Reduce (PTryFromExcess a b s)) -> Term s r)
-> Term s r
ptryFrom @(PAsData PRationalData) Term s PData
opq ((Term s PRationalData,
 Reduce (PTryFromExcess PData PRationalData s))
-> Term s r
cont forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (p :: Type -> Type -> Type) a b c.
Bifunctor p =>
(a -> b) -> p a c -> p b c
first forall (s :: S) (a :: PType) (b :: PType). Term s a -> Term s b
PUNSAFE.punsafeCoerce)

-- | NOTE: This instance produces a verified positive denominator as the excess output.
instance PTryFrom PData (PAsData PRationalData) where
  type PTryFromExcess PData (PAsData PRationalData) = Flip Term PPositive
  ptryFrom' :: forall (s :: S) (r :: PType).
Term s PData
-> ((Term s (PAsData PRationalData),
     Reduce (PTryFromExcess PData (PAsData PRationalData) s))
    -> Term s r)
-> Term s r
ptryFrom' Term s PData
opq = forall (r :: PType) (s :: S) a.
TermCont @r s a -> (a -> Term s r) -> Term s r
runTermCont forall a b. (a -> b) -> a -> b
$ do
    Term s (PBuiltinPair PInteger (PBuiltinList PData))
opq' <- forall {r :: PType} (s :: S) (a :: PType).
Term s a -> TermCont @r s (Term s a)
pletC forall a b. (a -> b) -> a -> b
$ forall (s :: S).
Term s (PData :--> PBuiltinPair PInteger (PBuiltinList PData))
pasConstr forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s PData
opq
    forall {r :: PType} (s :: S).
Term s PString -> Term s PBool -> TermCont @r s ()
pguardC Term s PString
"ptryFrom(PRationalData): invalid constructor id" forall a b. (a -> b) -> a -> b
$ forall (s :: S) (a :: PType) (b :: PType).
Term s (PBuiltinPair a b :--> a)
pfstBuiltin forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PBuiltinPair PInteger (PBuiltinList PData))
opq' forall (t :: PType) (s :: S).
PEq t =>
Term s t -> Term s t -> Term s PBool
#== Term s PInteger
0
    Term s (PBuiltinList PData)
flds <- forall {r :: PType} (s :: S) (a :: PType).
Term s a -> TermCont @r s (Term s a)
pletC forall a b. (a -> b) -> a -> b
$ forall (s :: S) (a :: PType) (b :: PType).
Term s (PBuiltinPair a b :--> b)
psndBuiltin forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PBuiltinPair PInteger (PBuiltinList PData))
opq'
    Term s PInteger
_numr <- forall {r :: PType} (s :: S) (a :: PType).
Term s a -> TermCont @r s (Term s a)
pletC forall a b. (a -> b) -> a -> b
$ forall (b :: PType) (a :: PType) (s :: S) (r :: PType).
PTryFrom a b =>
Term s a
-> ((Term s b, Reduce (PTryFromExcess a b s)) -> Term s r)
-> Term s r
ptryFrom @(PAsData PInteger) (forall (list :: PType -> PType) (a :: PType) (s :: S).
(PListLike list, PElemConstraint list a) =>
Term s (list a :--> a)
phead forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PBuiltinList PData)
flds) forall a b. (a, b) -> b
snd
    Term s (PBuiltinList PData)
ratTail <- forall {r :: PType} (s :: S) (a :: PType).
Term s a -> TermCont @r s (Term s a)
pletC forall a b. (a -> b) -> a -> b
$ forall (list :: PType -> PType) (a :: PType) (s :: S).
(PListLike list, PElemConstraint list a) =>
Term s (list a :--> list a)
ptail forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PBuiltinList PData)
flds
    Term s PPositive
denm <- forall {r :: PType} (s :: S) (a :: PType).
Term s a -> TermCont @r s (Term s a)
pletC forall a b. (a -> b) -> a -> b
$ forall (b :: PType) (a :: PType) (s :: S) (r :: PType).
PTryFrom a b =>
Term s a
-> ((Term s b, Reduce (PTryFromExcess a b s)) -> Term s r)
-> Term s r
ptryFrom @(PAsData PPositive) (forall (list :: PType -> PType) (a :: PType) (s :: S).
(PListLike list, PElemConstraint list a) =>
Term s (list a :--> a)
phead forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PBuiltinList PData)
ratTail) forall a b. (a, b) -> b
snd
    forall {r :: PType} (s :: S).
Term s PString -> Term s PBool -> TermCont @r s ()
pguardC Term s PString
"ptryFrom(PRationalData): constructor fields len > 2" forall a b. (a -> b) -> a -> b
$ forall (list :: PType -> PType) (a :: PType) (s :: S).
(PListLike list, PElemConstraint list a) =>
Term s (list a :--> list a)
ptail forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PBuiltinList PData)
ratTail forall (t :: PType) (s :: S).
PEq t =>
Term s t -> Term s t -> Term s PBool
#== forall (list :: PType -> PType) (a :: PType) (s :: S).
(PListLike list, PElemConstraint list a) =>
Term s (list a)
pnil
    forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (forall (s :: S) (a :: PType) (b :: PType). Term s a -> Term s b
PUNSAFE.punsafeCoerce Term s PData
opq, Term s PPositive
denm)

newtype Flip f a b = Flip (f b a) deriving stock (forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall k k (f :: k -> k -> Type) (a :: k) (b :: k) x.
Rep (Flip @k @k f a b) x -> Flip @k @k f a b
forall k k (f :: k -> k -> Type) (a :: k) (b :: k) x.
Flip @k @k f a b -> Rep (Flip @k @k f a b) x
$cto :: forall k k (f :: k -> k -> Type) (a :: k) (b :: k) x.
Rep (Flip @k @k f a b) x -> Flip @k @k f a b
$cfrom :: forall k k (f :: k -> k -> Type) (a :: k) (b :: k) x.
Flip @k @k f a b -> Rep (Flip @k @k f a b) x
Generic)

prationalFromData :: ClosedTerm (PRationalData :--> PRational)
prationalFromData :: ClosedTerm (PRationalData :--> PRational)
prationalFromData = forall (a :: PType) (s :: S).
HasCallStack =>
ClosedTerm a -> Term s a
phoistAcyclic forall a b. (a -> b) -> a -> b
$
  forall a (b :: PType) (s :: S) (c :: PType).
(PLamN a b s, HasCallStack) =>
(Term s c -> a) -> Term s (c :--> b)
plam forall a b. (a -> b) -> a -> b
$ \Term s PRationalData
x -> forall (a :: PType) (s :: S). TermCont @a s (Term s a) -> Term s a
unTermCont forall a b. (a -> b) -> a -> b
$ do
    HRec
  ((':)
     @(Symbol, Type)
     '("numerator", Term s (PAsData PInteger))
     ((':)
        @(Symbol, Type)
        '("denominator", Term s (PAsData PPositive))
        ('[] @(Symbol, Type))))
l <- forall (fs :: [Symbol]) (a :: PType) (s :: S) (b :: PType)
       (ps :: [PLabeledType]) (bs :: [ToBind]).
(PDataFields a,
 (ps :: [PLabeledType]) ~ (PFields a :: [PLabeledType]),
 (bs :: [ToBind]) ~ (Bindings ps fs :: [ToBind]),
 BindFields ps bs) =>
Term s a -> TermCont @b s (HRec (BoundTerms ps bs s))
pletFieldsC @'["numerator", "denominator"] Term s PRationalData
x
    forall (f :: Type -> Type) a. Applicative f => a -> f a
pure forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (a :: PType) (s :: S). PlutusType a => a s -> Term s a
pcon forall a b. (a -> b) -> a -> b
$ forall (s :: S). Term s PInteger -> Term s PPositive -> PRational s
PRational (forall {k} (x :: k) r a. HasField @k x r a => r -> a
getField @"numerator" HRec
  ((':)
     @(Symbol, Type)
     '("numerator", Term s (PAsData PInteger))
     ((':)
        @(Symbol, Type)
        '("denominator", Term s (PAsData PPositive))
        ('[] @(Symbol, Type))))
l) (forall {k} (x :: k) r a. HasField @k x r a => r -> a
getField @"denominator" HRec
  ((':)
     @(Symbol, Type)
     '("numerator", Term s (PAsData PInteger))
     ((':)
        @(Symbol, Type)
        '("denominator", Term s (PAsData PPositive))
        ('[] @(Symbol, Type))))
l)