{-|
  Copyright   :  (C) 2013-2016, University of Twente,
                     2016-2017, Myrtle Software Ltd,
                     2017-2022, Google Inc.,
                     2017-2026, QBayLogic B.V.
  License     :  BSD2 (see the file LICENSE)
  Maintainer  :  QBayLogic B.V. <devops@qbaylogic.com>
-}

{-# LANGUAGE RecordWildCards #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE TemplateHaskell #-}

module Clash.GHC.Evaluator.Primitives.GHC.TypeNats
  ( primitives
  ) where

import qualified Data.Either         as Either
import           Data.Text           (Text)

import           Clash.Core.Evaluator.Types
import           Clash.Core.Literal  (Literal (..))
import Clash.Core.Term (Term (..), mkApps)
import Clash.Core.Type (Type (..), LitTy (..), TypeView (..), splitFunForallTy, tyView)
import Clash.Core.TyCon (tyConDataCons)
import qualified Clash.Data.UniqMap as UniqMap
import Clash.Util (textNameLit)

import qualified GHC.TypeNats

import Clash.GHC.Evaluator.Primitive.Util

primitives :: [(Text, PrimStep)]
primitives :: [(Text, PrimStep)]
primitives =
  [ Text -> (PrimStepContext -> Maybe Machine) -> (Text, PrimStep)
primStepEntry $(textNameLit 'GHC.TypeNats.natVal) ((PrimStepContext -> Maybe Machine) -> (Text, PrimStep))
-> (PrimStepContext -> Maybe Machine) -> (Text, PrimStep)
forall a b. (a -> b) -> a -> b
$ \case
      PrimStepContext{Bool
[Type]
[Value]
Type
TyConMap
Machine
PrimInfo
Term -> Maybe Machine
Term -> Term
Type
-> Integer -> Integer -> (Natural -> Natural -> Natural) -> Term
Type -> Integer -> (Natural -> Natural) -> Term
Type -> [Integer] -> ([Natural] -> Term) -> Term
Machine -> Term -> Maybe Machine
tcm :: TyConMap
isSubj :: Bool
pInfo :: PrimInfo
tys :: [Type]
args :: [Value]
mach :: Machine
ty :: Type
checkNaturalRange1 :: Type -> Integer -> (Natural -> Natural) -> Term
checkNaturalRange2 :: Type
-> Integer -> Integer -> (Natural -> Natural -> Natural) -> Term
checkNaturalRange :: Type -> [Integer] -> ([Natural] -> Term) -> Term
reduce :: Term -> Maybe Machine
reduceWith :: Machine -> Term -> Maybe Machine
reduceWHNF :: Term -> Maybe Machine
reduceWHNF' :: Machine -> Term -> Maybe Machine
catchDivByZero :: Term -> Term
catchErrorCall :: Term -> Term
tcm :: PrimStepContext -> TyConMap
isSubj :: PrimStepContext -> Bool
pInfo :: PrimStepContext -> PrimInfo
tys :: PrimStepContext -> [Type]
args :: PrimStepContext -> [Value]
mach :: PrimStepContext -> Machine
ty :: PrimStepContext -> Type
checkNaturalRange1 :: PrimStepContext -> Type -> Integer -> (Natural -> Natural) -> Term
checkNaturalRange2 :: PrimStepContext
-> Type
-> Integer
-> Integer
-> (Natural -> Natural -> Natural)
-> Term
checkNaturalRange :: PrimStepContext -> Type -> [Integer] -> ([Natural] -> Term) -> Term
reduce :: PrimStepContext -> Term -> Maybe Machine
reduceWith :: PrimStepContext -> Machine -> Term -> Maybe Machine
reduceWHNF :: PrimStepContext -> Term -> Maybe Machine
reduceWHNF' :: PrimStepContext -> Machine -> Term -> Maybe Machine
catchDivByZero :: PrimStepContext -> Term -> Term
catchErrorCall :: PrimStepContext -> Term -> Term
..}
        | [Lit (NaturalLiteral Integer
n), Value
_] <- [Value]
args
        -> Term -> Maybe Machine
reduce (Literal -> Term
Literal (Integer -> Literal
NaturalLiteral Integer
n))
      PrimStepContext
_ -> Maybe Machine
forall a. Maybe a
Nothing

  , Text -> (PrimStepContext -> Maybe Machine) -> (Text, PrimStep)
primStepEntry $(textNameLit 'GHC.TypeNats.someNatVal) ((PrimStepContext -> Maybe Machine) -> (Text, PrimStep))
-> (PrimStepContext -> Maybe Machine) -> (Text, PrimStep)
forall a b. (a -> b) -> a -> b
$ \case
      PrimStepContext{Bool
[Type]
[Value]
Type
TyConMap
Machine
PrimInfo
Term -> Maybe Machine
Term -> Term
Type
-> Integer -> Integer -> (Natural -> Natural -> Natural) -> Term
Type -> Integer -> (Natural -> Natural) -> Term
Type -> [Integer] -> ([Natural] -> Term) -> Term
Machine -> Term -> Maybe Machine
tcm :: PrimStepContext -> TyConMap
isSubj :: PrimStepContext -> Bool
pInfo :: PrimStepContext -> PrimInfo
tys :: PrimStepContext -> [Type]
args :: PrimStepContext -> [Value]
mach :: PrimStepContext -> Machine
ty :: PrimStepContext -> Type
checkNaturalRange1 :: PrimStepContext -> Type -> Integer -> (Natural -> Natural) -> Term
checkNaturalRange2 :: PrimStepContext
-> Type
-> Integer
-> Integer
-> (Natural -> Natural -> Natural)
-> Term
checkNaturalRange :: PrimStepContext -> Type -> [Integer] -> ([Natural] -> Term) -> Term
reduce :: PrimStepContext -> Term -> Maybe Machine
reduceWith :: PrimStepContext -> Machine -> Term -> Maybe Machine
reduceWHNF :: PrimStepContext -> Term -> Maybe Machine
reduceWHNF' :: PrimStepContext -> Machine -> Term -> Maybe Machine
catchDivByZero :: PrimStepContext -> Term -> Term
catchErrorCall :: PrimStepContext -> Term -> Term
tcm :: TyConMap
isSubj :: Bool
pInfo :: PrimInfo
tys :: [Type]
args :: [Value]
mach :: Machine
ty :: Type
checkNaturalRange1 :: Type -> Integer -> (Natural -> Natural) -> Term
checkNaturalRange2 :: Type
-> Integer -> Integer -> (Natural -> Natural -> Natural) -> Term
checkNaturalRange :: Type -> [Integer] -> ([Natural] -> Term) -> Term
reduce :: Term -> Maybe Machine
reduceWith :: Machine -> Term -> Maybe Machine
reduceWHNF :: Term -> Maybe Machine
reduceWHNF' :: Machine -> Term -> Maybe Machine
catchDivByZero :: Term -> Term
catchErrorCall :: Term -> Term
..}
        | [Lit (NaturalLiteral Integer
n)] <- [Value]
args
        -> let resTy :: Type
resTy = TyConMap -> Type -> [Type] -> Type
getResultTy TyConMap
tcm Type
ty [Type]
tys
            in Term -> Maybe Machine
reduce (TyConMap -> Integer -> Type -> Term
mkSomeNat TyConMap
tcm Integer
n Type
resTy)
      PrimStepContext
_ -> Maybe Machine
forall a. Maybe a
Nothing

  , Text -> (PrimStepContext -> Maybe Machine) -> (Text, PrimStep)
primStepEntry $(textNameLit 'GHC.TypeNats.withSomeSNat) ((PrimStepContext -> Maybe Machine) -> (Text, PrimStep))
-> (PrimStepContext -> Maybe Machine) -> (Text, PrimStep)
forall a b. (a -> b) -> a -> b
$ \case
      PrimStepContext{Bool
[Type]
[Value]
Type
TyConMap
Machine
PrimInfo
Term -> Maybe Machine
Term -> Term
Type
-> Integer -> Integer -> (Natural -> Natural -> Natural) -> Term
Type -> Integer -> (Natural -> Natural) -> Term
Type -> [Integer] -> ([Natural] -> Term) -> Term
Machine -> Term -> Maybe Machine
tcm :: PrimStepContext -> TyConMap
isSubj :: PrimStepContext -> Bool
pInfo :: PrimStepContext -> PrimInfo
tys :: PrimStepContext -> [Type]
args :: PrimStepContext -> [Value]
mach :: PrimStepContext -> Machine
ty :: PrimStepContext -> Type
checkNaturalRange1 :: PrimStepContext -> Type -> Integer -> (Natural -> Natural) -> Term
checkNaturalRange2 :: PrimStepContext
-> Type
-> Integer
-> Integer
-> (Natural -> Natural -> Natural)
-> Term
checkNaturalRange :: PrimStepContext -> Type -> [Integer] -> ([Natural] -> Term) -> Term
reduce :: PrimStepContext -> Term -> Maybe Machine
reduceWith :: PrimStepContext -> Machine -> Term -> Maybe Machine
reduceWHNF :: PrimStepContext -> Term -> Maybe Machine
reduceWHNF' :: PrimStepContext -> Machine -> Term -> Maybe Machine
catchDivByZero :: PrimStepContext -> Term -> Term
catchErrorCall :: PrimStepContext -> Term -> Term
tcm :: TyConMap
isSubj :: Bool
pInfo :: PrimInfo
tys :: [Type]
args :: [Value]
mach :: Machine
ty :: Type
checkNaturalRange1 :: Type -> Integer -> (Natural -> Natural) -> Term
checkNaturalRange2 :: Type
-> Integer -> Integer -> (Natural -> Natural -> Natural) -> Term
checkNaturalRange :: Type -> [Integer] -> ([Natural] -> Term) -> Term
reduce :: Term -> Maybe Machine
reduceWith :: Machine -> Term -> Maybe Machine
reduceWHNF :: Term -> Maybe Machine
reduceWHNF' :: Machine -> Term -> Maybe Machine
catchDivByZero :: Term -> Term
catchErrorCall :: Term -> Term
..}
        | Lit (NaturalLiteral Integer
n) : Value
fun : [Value]
_ <- [Value]
args
        , Type
_ : Type
funTy : [Type]
_ <- [Either TyVar Type] -> [Type]
forall a b. [Either a b] -> [b]
Either.rights (([Either TyVar Type], Type) -> [Either TyVar Type]
forall a b. (a, b) -> a
fst (Type -> ([Either TyVar Type], Type)
splitFunForallTy Type
ty))
        , (Type -> TypeView
tyView -> TyConApp TyConName
snatTcNm [Type]
_) : [Type]
_ <- [Either TyVar Type] -> [Type]
forall a b. [Either a b] -> [b]
Either.rights (([Either TyVar Type], Type) -> [Either TyVar Type]
forall a b. (a, b) -> a
fst (Type -> ([Either TyVar Type], Type)
splitFunForallTy Type
funTy))
        , Just TyCon
snatTc <- TyConName -> TyConMap -> Maybe TyCon
forall a b. Uniquable a => a -> UniqMap b -> Maybe b
UniqMap.lookup TyConName
snatTcNm TyConMap
tcm
        , [DataCon
snatDc] <- TyCon -> [DataCon]
tyConDataCons TyCon
snatTc
        -> let nTy :: Type
nTy = LitTy -> Type
LitTy (Integer -> LitTy
NumTy Integer
n)
               snat :: Term
snat = Term -> [Either Term Type] -> Term
mkApps (DataCon -> Term
Data DataCon
snatDc) [Type -> Either Term Type
forall a b. b -> Either a b
Right Type
nTy, Term -> Either Term Type
forall a b. a -> Either a b
Left (Literal -> Term
Literal (Integer -> Literal
NaturalLiteral Integer
n))]
               ret :: Term
ret = Term -> [Either Term Type] -> Term
mkApps (Value -> Term
valToTerm Value
fun) [Type -> Either Term Type
forall a b. b -> Either a b
Right Type
nTy, Term -> Either Term Type
forall a b. a -> Either a b
Left Term
snat]
            in Term -> Maybe Machine
reduce Term
ret
      PrimStepContext
_ -> Maybe Machine
forall a. Maybe a
Nothing

  ]