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

module Lorentz.CustomArith.Common
  ( -- * Arithmetic operations
    div
    -- * Lorentz casts
  , LorentzRounding (..)

    -- * Additional Arithmetic operations
  , Div

  ) where

import Prelude hiding (div)

import Lorentz.Arith
import Lorentz.Base

-- | Since Michelson doesn't support divide operation, we will use our own to represent
-- divison of Fixed and Rational values
data Div

-- | Operation that represents division of two values with a given result
div
  :: forall r n m s. ArithOpHs Div n m r
  => n : m : s :-> r : s
div :: forall r n m (s :: [*]).
ArithOpHs Div n m r =>
(n : m : s) :-> (r : s)
div = forall aop n m r (s :: [*]).
ArithOpHs aop n m r =>
(n : m : s) :-> (r : s)
evalArithOpHs @Div

-- | Class that enables support of rounding operations for Lorentz non-integer values
class LorentzRounding a b where
  round_ :: a : s :-> b : s
  ceil_ :: a : s :-> b : s
  floor_ :: a : s :-> b : s