HSTypes

module Ledger.Prelude.Foreign.HSTypes where

open import Data.Rational
open import Class.Convertible
open import Tactic.Derive.Convertible
open import Foreign.Haskell
open import Class.HasHsType public
open import Tactic.Derive.HsType
open import stdlib.Foreign.Haskell.Empty
-- open import Class.HasHsType.Foreign
open import Class.Convertible.Foreign

open import Ledger.Prelude
open import Ledger.Prelude.Numeric.UnitInterval
open import Ledger.Prelude.Foreign.Util
open import Ledger.Prelude.Numeric.PositiveNat

{-# FOREIGN GHC
  {-# LANGUAGE DeriveGeneric #-}
  {-# LANGUAGE DeriveFunctor #-}
#-}

{-# FOREIGN GHC
  import GHC.Generics (Generic)
  import Prelude hiding (Rational)
  import GHC.Real (Ratio(..))
#-}

-- * Haskell types

instance
  iConvTop    = Convertible-Refl {⊤}
  iConvNat    = Convertible-Refl {ℕ}
  iConvString = Convertible-Refl {String}
  iConvBool   = Convertible-Refl {Bool}

  HsTy-⊥ = mkHsType ⊥ Empty
  Conv-⊥ = autoConvert ⊥

  HsTy-⊤ = mkHsType ⊤ ⊤

-- * Rational

data Rational : Type where
  _,_ : ℤ → ℕ → Rational
{-# COMPILE GHC Rational = data Rational ((:%)) #-}

-- We'll generate code with qualified references to Rational in this
-- module, so make sure to define it.
{-# FOREIGN GHC type Rational = Ratio Integer #-}

instance
  HsTy-Rational = mkHsType ℚ Rational
  Conv-Rational : HsConvertible ℚ
  Conv-Rational = λ where
    .to (mkℚ n d _)       → n , suc d
    .from (n , zero)    → 0ℚ -- TODO is there a safer way to do this?
    .from (n , (suc d)) → n Data.Rational./ suc d

-- * Maps and Sets

record HSMap K V : Type where
  constructor MkHSMap
  field assocList : List (Pair K V)

record HSSet A : Type where
  constructor MkHSSet
  field elems : List A

{-# FOREIGN GHC
  newtype HSMap k v = MkHSMap [(k, v)]
    deriving (Generic, Show, Eq, Ord)
  newtype HSSet a = MkHSSet [a]
    deriving (Generic, Show, Eq, Ord)
#-}
{-# COMPILE GHC HSMap = data HSMap (MkHSMap) #-}
{-# COMPILE GHC HSSet = data HSSet (MkHSSet) #-}

instance
  HsTy-HSSet : ∀ {A} → ⦃ HasHsType A ⦄ → HasHsType (ℙ A)
  HsTy-HSSet {A} = mkHsType _ (HSSet (HsType A))

  Conv-HSSet : ∀ {A} ⦃ _ : HasHsType A ⦄
             → ⦃ HsConvertible A ⦄
             → HsConvertible (ℙ A)
  Conv-HSSet = λ where
    .to → MkHSSet ∘ to ∘ setToList
    .from → fromList ∘ from ∘ HSSet.elems

  HsTy-Map : ∀ {A B} → ⦃ HasHsType A ⦄ → ⦃ HasHsType B ⦄ → HasHsType (A ⇀ B)
  HsTy-Map {A} {B} = mkHsType _ (HSMap (HsType A) (HsType B))

  Conv-HSMap : ∀ {A B} ⦃ _ : HasHsType A ⦄ ⦃ _ : HasHsType B ⦄
    → ⦃ DecEq A ⦄
    → ⦃ HsConvertible A ⦄
    → ⦃ HsConvertible B ⦄
    → HsConvertible (A ⇀ B)
  Conv-HSMap = λ where
    .to → MkHSMap ∘ to ∘ setToList ∘ proj₁
    .from → fromListᵐ ∘ map from ∘ HSMap.assocList

-- * ComputationResult

data HSComputationResult E A : Type where
  Success : A → HSComputationResult E A
  Failure : E → HSComputationResult E A

{-# FOREIGN GHC
  data ComputationResult e a = Success a | Failure e
    deriving (Functor, Eq, Show, Generic)

  instance Applicative (ComputationResult e) where
    pure = Success
    (Success f) <*> x = f <$> x
    (Failure e) <*> _ = Failure e

  instance Monad (ComputationResult e) where
    return = pure
    (Success a) >>= m = m a
    (Failure e) >>= _ = Failure e
#-}
{-# COMPILE GHC HSComputationResult = data ComputationResult (Success | Failure) #-}

instance
  HsTy-ComputationResult : ∀ {l} {Err} {A : Type l}
                           → ⦃ HasHsType Err ⦄ → ⦃ HasHsType A ⦄
                           → HasHsType (ComputationResult Err A)
  HsTy-ComputationResult {Err = Err} {A} = mkHsType _ (HSComputationResult (HsType Err) (HsType A))

  Conv-ComputationResult : ConvertibleType HSComputationResult ComputationResult
  Conv-ComputationResult = autoConvertible

  Conv-HSComputationResult : ConvertibleType ComputationResult HSComputationResult
  Conv-HSComputationResult = autoConvertible

-- * Numeric types

instance
  HsTy-UnitInterval : HasHsType UnitInterval
  HsTy-UnitInterval .HasHsType.HsType = Rational
    -- I would like to use ℚ here, but Rational converts better.

  Conv-UnitInterval : Convertible UnitInterval Rational
  Conv-UnitInterval .to x = to (fromUnitInterval x)
  Conv-UnitInterval .from x =
    case toUnitInterval (from x) of λ where
      (just x) → x
      nothing → error "Formal Spec: rational outside of unit interval"

instance
  HsTy-PosNat : HasHsType PosNat
  HsTy-PosNat .HasHsType.HsType = ℕ

  Conv-PosNat : Convertible PosNat ℕ
  Conv-PosNat .to x = to (fromPosNat x)
  Conv-PosNat .from x =
    case toPosNat (from x) of λ where
      (just x) → x
      nothing → error "Formal Spec: natural number is zero (not nonZero)"

unquoteDecl = do
  hsTypeAlias Coin