Plutonomicon / plutarch-plutus

Typed eDSL for writing UPLC /ˈpluː.tɑːk/
MIT License
123 stars 64 forks source link

Inverting and dividing by negative PRational fails #682

Closed Swordlash closed 4 months ago

Swordlash commented 4 months ago

Not sure why nobody has ever noticed it (I've been bitten by it just now) but inverting and dividing by negative PRational fails the script.

ghci> evalScriptHuge $ compileTraced $ (precip # (-1 :: Term _ PRational))
(Left An error has occurred:  User error:
The machine terminated because of an error, either from a built-in function or from an explicit use of 'error'.,ExBudget {exBudgetCPU = ExCPU 9469224, exBudgetMemory = ExMemory 20208},["ptryPositive: building with non positive: -1"])

ghci> evalScriptHuge $ compileTraced $ (-1 :: Term _ PRational) #/ (-1 :: Term _ PRational)
(Left An error has occurred:  User error:
The machine terminated because of an error, either from a built-in function or from an explicit use of 'error'.,ExBudget {exBudgetCPU = ExCPU 9768597, exBudgetMemory = ExMemory 20212},["ptryPositive: building with non positive: -1"])

The issue is with the PFractional PRational instance

instance PFractional PRational where
  precip =
    phoistAcyclic $
      plam $ \x ->
        pmatch x $ \(PRational xn xd) ->
          pcon $ PRational (pto xd) $ ptryPositive # xn -- HERE it fails if xn < 0

  x' #/ y' =
    phoistAcyclic
      ( plam $ \x y -> unTermCont $ do
          PRational xn xd <- tcont $ pmatch x
          PRational yn yd <- tcont $ pmatch y
          denm <- tcont . plet $ ptryPositive #$ pto xd * yn -- HERE it fails if yn < 0
          pure $ preduce #$ pcon $ PRational (xn * pto yd) denm
      )
      # x'
      # y'

We should ensure a positive integer is passed to ptryPositive, and add an appropriate sign later.

SeungheonOh commented 4 months ago

Thank you. We will fix this

L-as commented 4 months ago

Closed by #683