{-|
  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 #-}

{-# OPTIONS_GHC -Wno-incomplete-uni-patterns #-}

module Clash.GHC.Evaluator.Primitives.Clash.Promoted.Nat
  ( primitives
  ) where

import           Control.Monad.Trans.Except (runExcept)
import           Data.Bits
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 Clash.Core.Util (tyNatSize)
import qualified Clash.Data.UniqMap as UniqMap
import Clash.Util (clogBase, flogBase, textNameLit)

import qualified Clash.Promoted.Nat

import Clash.GHC.Evaluator.Primitive.Util

primitives :: [(Text, PrimStep)]
primitives :: [(Text, PrimStep)]
primitives =
  [ Text -> (PrimStepContext -> Maybe Machine) -> (Text, PrimStep)
primStepEntry $(textNameLit 'Clash.Promoted.Nat.powSNat) ((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
..}
        | [Right Integer
a, Right Integer
b] <- (Type -> Either [Char] Integer)
-> [Type] -> [Either [Char] Integer]
forall a b. (a -> b) -> [a] -> [b]
map (Except [Char] Integer -> Either [Char] Integer
forall e a. Except e a -> Either e a
runExcept (Except [Char] Integer -> Either [Char] Integer)
-> (Type -> Except [Char] Integer) -> Type -> Either [Char] Integer
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TyConMap -> Type -> Except [Char] Integer
tyNatSize TyConMap
tcm) [Type]
tys
        -> let c :: Integer
c = case Integer
a of
                     Integer
2 -> Integer
1 Integer -> Int -> Integer
forall a. Bits a => a -> Int -> a
`shiftL` (Integer -> Int
forall a. Num a => Integer -> a
fromInteger Integer
b)
                     Integer
_ -> Integer
a Integer -> Integer -> Integer
forall a b. (Num a, Integral b) => a -> b -> a
^ Integer
b
               ([Either TyVar Type]
_,Type -> TypeView
tyView -> TyConApp TyConName
snatTcNm [Type]
_) = Type -> ([Either TyVar Type], Type)
splitFunForallTy Type
ty
               (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
           in  Term -> Maybe Machine
reduce (Term -> Maybe Machine) -> Term -> Maybe Machine
forall a b. (a -> b) -> a -> b
$
               Term -> [Either Term Type] -> Term
mkApps (DataCon -> Term
Data DataCon
snatDc) [ Type -> Either Term Type
forall a b. b -> Either a b
Right (LitTy -> Type
LitTy (Integer -> LitTy
NumTy Integer
c))
                                    , Term -> Either Term Type
forall a b. a -> Either a b
Left (Literal -> Term
Literal (Integer -> Literal
NaturalLiteral Integer
c))]
      PrimStepContext
_ -> Maybe Machine
forall a. Maybe a
Nothing

  , Text -> (PrimStepContext -> Maybe Machine) -> (Text, PrimStep)
primStepEntry $(textNameLit 'Clash.Promoted.Nat.flogBaseSNat) ((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
..}
        | [Right Integer
a, Right Integer
b] <- (Type -> Either [Char] Integer)
-> [Type] -> [Either [Char] Integer]
forall a b. (a -> b) -> [a] -> [b]
map (Except [Char] Integer -> Either [Char] Integer
forall e a. Except e a -> Either e a
runExcept (Except [Char] Integer -> Either [Char] Integer)
-> (Type -> Except [Char] Integer) -> Type -> Either [Char] Integer
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TyConMap -> Type -> Except [Char] Integer
tyNatSize TyConMap
tcm) [Type]
tys
        , Just Int
c <- Integer -> Integer -> Maybe Int
flogBase Integer
a Integer
b
        , let c' :: Integer
c' = Int -> Integer
forall a. Integral a => a -> Integer
toInteger Int
c
        -> let ([Either TyVar Type]
_,Type -> TypeView
tyView -> TyConApp TyConName
snatTcNm [Type]
_) = Type -> ([Either TyVar Type], Type)
splitFunForallTy Type
ty
               (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
           in  Term -> Maybe Machine
reduce (Term -> Maybe Machine) -> Term -> Maybe Machine
forall a b. (a -> b) -> a -> b
$
               Term -> [Either Term Type] -> Term
mkApps (DataCon -> Term
Data DataCon
snatDc) [ Type -> Either Term Type
forall a b. b -> Either a b
Right (LitTy -> Type
LitTy (Integer -> LitTy
NumTy Integer
c'))
                                    , Term -> Either Term Type
forall a b. a -> Either a b
Left (Literal -> Term
Literal (Integer -> Literal
NaturalLiteral Integer
c'))]
      PrimStepContext
_ -> Maybe Machine
forall a. Maybe a
Nothing

  , Text -> (PrimStepContext -> Maybe Machine) -> (Text, PrimStep)
primStepEntry $(textNameLit 'Clash.Promoted.Nat.clogBaseSNat) ((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
..}
        | [Right Integer
a, Right Integer
b] <- (Type -> Either [Char] Integer)
-> [Type] -> [Either [Char] Integer]
forall a b. (a -> b) -> [a] -> [b]
map (Except [Char] Integer -> Either [Char] Integer
forall e a. Except e a -> Either e a
runExcept (Except [Char] Integer -> Either [Char] Integer)
-> (Type -> Except [Char] Integer) -> Type -> Either [Char] Integer
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TyConMap -> Type -> Except [Char] Integer
tyNatSize TyConMap
tcm) [Type]
tys
        , Just Int
c <- Integer -> Integer -> Maybe Int
clogBase Integer
a Integer
b
        , let c' :: Integer
c' = Int -> Integer
forall a. Integral a => a -> Integer
toInteger Int
c
        -> let ([Either TyVar Type]
_,Type -> TypeView
tyView -> TyConApp TyConName
snatTcNm [Type]
_) = Type -> ([Either TyVar Type], Type)
splitFunForallTy Type
ty
               (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
           in  Term -> Maybe Machine
reduce (Term -> Maybe Machine) -> Term -> Maybe Machine
forall a b. (a -> b) -> a -> b
$
               Term -> [Either Term Type] -> Term
mkApps (DataCon -> Term
Data DataCon
snatDc) [ Type -> Either Term Type
forall a b. b -> Either a b
Right (LitTy -> Type
LitTy (Integer -> LitTy
NumTy Integer
c'))
                                    , Term -> Either Term Type
forall a b. a -> Either a b
Left (Literal -> Term
Literal (Integer -> Literal
NaturalLiteral Integer
c'))]
        | Bool
otherwise
        -> [Char] -> Maybe Machine
forall a. HasCallStack => [Char] -> a
error ([Char]
"clogBaseSNat: args = " [Char] -> [Char] -> [Char]
forall a. Semigroup a => a -> a -> a
<> [Value] -> [Char]
forall a. Show a => a -> [Char]
show [Value]
args [Char] -> [Char] -> [Char]
forall a. Semigroup a => a -> a -> a
<> [Char]
", tys = " [Char] -> [Char] -> [Char]
forall a. Semigroup a => a -> a -> a
<> [Type] -> [Char]
forall a. Show a => a -> [Char]
show [Type]
tys)

  , Text -> (PrimStepContext -> Maybe Machine) -> (Text, PrimStep)
primStepEntry $(textNameLit 'Clash.Promoted.Nat.logBaseSNat) ((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
..}
        | [Right Integer
a, Right Integer
b] <- (Type -> Either [Char] Integer)
-> [Type] -> [Either [Char] Integer]
forall a b. (a -> b) -> [a] -> [b]
map (Except [Char] Integer -> Either [Char] Integer
forall e a. Except e a -> Either e a
runExcept (Except [Char] Integer -> Either [Char] Integer)
-> (Type -> Except [Char] Integer) -> Type -> Either [Char] Integer
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TyConMap -> Type -> Except [Char] Integer
tyNatSize TyConMap
tcm) [Type]
tys
        , Just Int
c <- Integer -> Integer -> Maybe Int
flogBase Integer
a Integer
b
        , let c' :: Integer
c' = Int -> Integer
forall a. Integral a => a -> Integer
toInteger Int
c
        -> let ([Either TyVar Type]
_,Type -> TypeView
tyView -> TyConApp TyConName
snatTcNm [Type]
_) = Type -> ([Either TyVar Type], Type)
splitFunForallTy Type
ty
               (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
           in  Term -> Maybe Machine
reduce (Term -> Maybe Machine) -> Term -> Maybe Machine
forall a b. (a -> b) -> a -> b
$
               Term -> [Either Term Type] -> Term
mkApps (DataCon -> Term
Data DataCon
snatDc) [ Type -> Either Term Type
forall a b. b -> Either a b
Right (LitTy -> Type
LitTy (Integer -> LitTy
NumTy Integer
c'))
                                    , Term -> Either Term Type
forall a b. a -> Either a b
Left (Literal -> Term
Literal (Integer -> Literal
NaturalLiteral Integer
c'))]
      PrimStepContext
_ -> Maybe Machine
forall a. Maybe a
Nothing

  ]