{-|
  Copyright   :  (C) 2017-2022, Google Inc.,
                     2021-2024, QBayLogic B.V.
  License     :  BSD2 (see the file LICENSE)
  Maintainer  :  QBayLogic B.V. <devops@qbaylogic.com>

  Call-by-need evaluator based on the evaluator described in:

  Maximilian Bolingbroke, Simon Peyton Jones, "Supercompilation by evaluation",
  Haskell '10, Baltimore, Maryland, USA.

-}

{-# LANGUAGE CPP #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE MagicHash #-}
{-# LANGUAGE NamedFieldPuns #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE TemplateHaskell #-}

module Clash.GHC.Evaluator where

import           Prelude                                 hiding (lookup)

import           Control.Concurrent.Supply               (Supply, freshId)
import           Data.Either                             (lefts,rights)
import           Data.List                               (mapAccumL)
#if !MIN_VERSION_base(4,20,0)
import           Data.List                               (foldl')
#endif
import qualified Data.Primitive.ByteArray                as BA
import qualified Data.Text as Text
#if MIN_VERSION_base(4,15,0)
import           GHC.Num.Integer                         (Integer (..))
#else
import           GHC.Integer.GMP.Internals
  (Integer (..), BigNat (..))
#endif

import           Clash.Core.DataCon
import           Clash.Core.Evaluator.Types
import           Clash.Core.HasFreeVars
import           Clash.Core.HasType
import           Clash.Core.Literal
import           Clash.Core.Name
import           Clash.Core.Pretty
import           Clash.Core.Subst
import           Clash.Core.Term
import           Clash.Core.TyCon
import           Clash.Core.Type
import           Clash.Core.Util
import           Clash.Core.Var
import           Clash.Core.VarEnv
import           Clash.Debug
import qualified Clash.Normalize.Primitives as NP (removedArg, undefined, undefinedX)
import           Clash.Unique
import           Clash.Util                              (curLoc)

import           Clash.GHC.Evaluator.Primitive

evaluator :: Evaluator
evaluator :: Evaluator
evaluator = Evaluator :: Step -> Unwind -> PrimStep -> PrimUnwind -> Evaluator
Evaluator
  { step :: Step
step = Step
ghcStep
  , unwind :: Unwind
unwind = Unwind
ghcUnwind
  , primStep :: PrimStep
primStep = PrimStep
ghcPrimStep
  , primUnwind :: PrimUnwind
primUnwind = PrimUnwind
ghcPrimUnwind
  }

{- [Note: forcing special primitives]
Clash uses the `whnf` function in two places (for now):

  1. The case-of-known-constructor transformation
  2. The reduceConstant transformation

The first transformation is needed to reach the required normal form. The
second transformation is more of cleanup transformation, so non-essential.

Normally, `whnf` would force the evaluation of all primitives, which is needed
in the `case-of-known-constructor` transformation. However, there are some
primitives which we want to leave unevaluated in the `reduceConstant`
transformation. Such primitives are:

  - Primitives such as `Clash.Sized.Vector.transpose`, `Clash.Sized.Vector.map`,
    etc. that do not reduce to an expression in normal form. Where the
    `reduceConstant` transformation is supposed to be normal-form preserving.
  - Primitives such as `GHC.Int.I8#`, `GHC.Word.W32#`, etc. which seem like
    wrappers around a 64-bit literal, but actually perform truncation to the
    desired bit-size.

This is why the Primitive Evaluator gets a flag telling whether it should
evaluate these special primitives.
-}

stepVar :: Id -> Step
stepVar :: Id -> Step
stepVar Id
i Machine
m TyConMap
_
  | Just Term
e <- IdScope -> Id -> Machine -> Maybe Term
heapLookup IdScope
LocalId Id
i Machine
m
  = IdScope -> Term -> Maybe Machine
go IdScope
LocalId Term
e

  | Just Term
e <- IdScope -> Id -> Machine -> Maybe Term
heapLookup IdScope
GlobalId Id
i Machine
m
  , Id -> Bool
forall a. Var a -> Bool
isGlobalId Id
i
  = IdScope -> Term -> Maybe Machine
go IdScope
GlobalId Term
e

  | Bool
otherwise
  = Maybe Machine
forall a. Maybe a
Nothing
 where
  go :: IdScope -> Term -> Maybe Machine
go IdScope
s Term
e =
    let term :: Term
term = HasCallStack => InScopeSet -> Term -> Term
InScopeSet -> Term -> Term
deShadowTerm (Machine -> InScopeSet
mScopeNames Machine
m) (Term -> Term
tickExpr Term
e)
     in Machine -> Maybe Machine
forall a. a -> Maybe a
Just (Machine -> Maybe Machine)
-> (Machine -> Machine) -> Machine -> Maybe Machine
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Term -> Machine -> Machine
setTerm Term
term (Machine -> Machine) -> (Machine -> Machine) -> Machine -> Machine
forall b c a. (b -> c) -> (a -> b) -> a -> c
. StackFrame -> Machine -> Machine
stackPush (IdScope -> Id -> StackFrame
Update IdScope
s Id
i) (Machine -> Maybe Machine) -> Machine -> Maybe Machine
forall a b. (a -> b) -> a -> b
$ IdScope -> Id -> Machine -> Machine
heapDelete IdScope
s Id
i Machine
m

  -- Removing the heap-bound value on a force ensures we do not get stuck on
  -- expressions such as: "let x = x in x"
  tickExpr :: Term -> Term
tickExpr = TickInfo -> Term -> Term
Tick (NameMod -> Type -> TickInfo
NameMod NameMod
PrefixName (LitTy -> Type
LitTy (LitTy -> Type) -> (String -> LitTy) -> String -> Type
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> LitTy
SymTy (String -> Type) -> String -> Type
forall a b. (a -> b) -> a -> b
$ Id -> String
forall a. Var a -> String
toStr Id
i))
  unQualName :: Text -> Text
unQualName = (Text, Text) -> Text
forall a b. (a, b) -> b
snd ((Text, Text) -> Text) -> (Text -> (Text, Text)) -> Text -> Text
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Text -> Text -> (Text, Text)
Text.breakOnEnd Text
"."
  toStr :: Var a -> String
toStr = Text -> String
Text.unpack (Text -> String) -> (Var a -> Text) -> Var a -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Text -> Text
unQualName (Text -> Text) -> (Var a -> Text) -> Var a -> Text
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Text -> Char -> Text) -> Char -> Text -> Text
forall a b c. (a -> b -> c) -> b -> a -> c
flip Text -> Char -> Text
Text.snoc Char
'_' (Text -> Text) -> (Var a -> Text) -> Var a -> Text
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Name a -> Text
forall a. Name a -> Text
nameOcc (Name a -> Text) -> (Var a -> Name a) -> Var a -> Text
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Var a -> Name a
forall a. Var a -> Name a
varName

stepData :: DataCon -> Step
stepData :: DataCon -> Step
stepData DataCon
dc = Unwind
ghcUnwind (DataCon -> [Either Term Type] -> Value
DC DataCon
dc [])

stepLiteral :: Literal -> Step
stepLiteral :: Literal -> Step
stepLiteral Literal
l = Unwind
ghcUnwind (Literal -> Value
Lit Literal
l)

stepPrim :: PrimInfo -> Step
stepPrim :: PrimInfo -> Step
stepPrim PrimInfo
pInfo Machine
m TyConMap
tcm
  | PrimInfo -> Text
primName PrimInfo
pInfo Text -> Text -> Bool
forall a. Eq a => a -> a -> Bool
== Text
"GHC.Prim.realWorld#" =
      Unwind
ghcUnwind (PrimInfo -> [Type] -> [Value] -> Value
PrimVal PrimInfo
pInfo [] []) Machine
m TyConMap
tcm

  | Bool
otherwise =
      case ([Either TyVar Type], Type) -> [Either TyVar Type]
forall a b. (a, b) -> a
fst (([Either TyVar Type], Type) -> [Either TyVar Type])
-> ([Either TyVar Type], Type) -> [Either TyVar Type]
forall a b. (a -> b) -> a -> b
$ Type -> ([Either TyVar Type], Type)
splitFunForallTy (PrimInfo -> Type
primType PrimInfo
pInfo) of
        []  -> PrimStep
ghcPrimStep TyConMap
tcm (Machine -> Bool
forcePrims Machine
m) PrimInfo
pInfo [] [] Machine
m
        [Either TyVar Type]
tys -> [Either TyVar Type] -> Term -> Step
newBinder [Either TyVar Type]
tys (PrimInfo -> Term
Prim PrimInfo
pInfo) Machine
m TyConMap
tcm

stepLam :: Id -> Term -> Step
stepLam :: Id -> Term -> Step
stepLam Id
x Term
e = Unwind
ghcUnwind (Id -> Term -> Value
Lambda Id
x Term
e)

stepTyLam :: TyVar -> Term -> Step
stepTyLam :: TyVar -> Term -> Step
stepTyLam TyVar
x Term
e = Unwind
ghcUnwind (TyVar -> Term -> Value
TyLambda TyVar
x Term
e)

stepApp :: Term -> Term -> Step
stepApp :: Term -> Term -> Step
stepApp Term
x Term
y Machine
m TyConMap
tcm =
  case Term
term of
    Data DataCon
dc ->
      let tys :: [Either TyVar Type]
tys = ([Either TyVar Type], Type) -> [Either TyVar Type]
forall a b. (a, b) -> a
fst (([Either TyVar Type], Type) -> [Either TyVar Type])
-> ([Either TyVar Type], Type) -> [Either TyVar Type]
forall a b. (a -> b) -> a -> b
$ Type -> ([Either TyVar Type], Type)
splitFunForallTy (DataCon -> Type
dcType DataCon
dc)
       in case Int -> Int -> Ordering
forall a. Ord a => a -> a -> Ordering
compare ([Either Term Type] -> Int
forall (t :: Type -> Type) a. Foldable t => t a -> Int
length [Either Term Type]
args) ([Either TyVar Type] -> Int
forall (t :: Type -> Type) a. Foldable t => t a -> Int
length [Either TyVar Type]
tys) of
            Ordering
EQ -> Unwind
ghcUnwind (DataCon -> [Either Term Type] -> Value
DC DataCon
dc [Either Term Type]
args) Machine
m TyConMap
tcm
            Ordering
LT -> [Either TyVar Type] -> Term -> Step
newBinder [Either TyVar Type]
tys' (Term -> Term -> Term
App Term
x Term
y) Machine
m TyConMap
tcm
            Ordering
GT -> String -> Maybe Machine
forall a. HasCallStack => String -> a
error String
"Overapplied DC"

    Prim PrimInfo
p ->
      let tys :: [Either TyVar Type]
tys = ([Either TyVar Type], Type) -> [Either TyVar Type]
forall a b. (a, b) -> a
fst (([Either TyVar Type], Type) -> [Either TyVar Type])
-> ([Either TyVar Type], Type) -> [Either TyVar Type]
forall a b. (a -> b) -> a -> b
$ Type -> ([Either TyVar Type], Type)
splitFunForallTy (PrimInfo -> Type
primType PrimInfo
p)
       in case Int -> Int -> Ordering
forall a. Ord a => a -> a -> Ordering
compare ([Either Term Type] -> Int
forall (t :: Type -> Type) a. Foldable t => t a -> Int
length [Either Term Type]
args) ([Either TyVar Type] -> Int
forall (t :: Type -> Type) a. Foldable t => t a -> Int
length [Either TyVar Type]
tys) of
            Ordering
EQ -> case [Either Term Type] -> [Term]
forall a b. [Either a b] -> [a]
lefts [Either Term Type]
args of
              -- We make boolean conjunction and disjunction extra lazy by
              -- deferring the evaluation of the arguments during the evaluation
              -- of the primop rule.
              --
              -- This allows us to implement:
              --
              -- x && True  --> x
              -- x && False --> False
              -- x || True  --> True
              -- x || False --> x
              --
              -- even when that 'x' is _|_. This makes the evaluation
              -- rule lazier than the actual Haskel implementations which
              -- are strict in the first argument and lazy in the second.
              [Term
a0, Term
a1] | PrimInfo -> Text
primName PrimInfo
p Text -> [Text] -> Bool
forall (t :: Type -> Type) a.
(Foldable t, Eq a) =>
a -> t a -> Bool
`elem` [Text
"GHC.Classes.&&",Text
"GHC.Classes.||"] ->
                    let (Machine
m0,Id
i) = TyConMap -> Machine -> Term -> (Machine, Id)
newLetBinding TyConMap
tcm Machine
m  Term
a0
                        (Machine
m1,Id
j) = TyConMap -> Machine -> Term -> (Machine, Id)
newLetBinding TyConMap
tcm Machine
m0 Term
a1
                    in  PrimStep
ghcPrimStep TyConMap
tcm (Machine -> Bool
forcePrims Machine
m) PrimInfo
p [] [Term -> Value
Suspend (Id -> Term
Var Id
i), Term -> Value
Suspend (Id -> Term
Var Id
j)] Machine
m1

              (Term
e':[Term]
es)
                | PrimInfo -> Text
primName PrimInfo
p Text -> [Text] -> Bool
forall (t :: Type -> Type) a.
(Foldable t, Eq a) =>
a -> t a -> Bool
`elem` ([Text]
undefinedXPrims [Text] -> [Text] -> [Text]
forall a. [a] -> [a] -> [a]
++ [Text]
undefinedPrims)
                -- The above primitives are (bottoming) values, whose arguments
                -- are never used anywhere in the rest of the compiler. So
                -- instead of pushing a PrimApply frame on the stack to evaluate
                -- those arguments, we instead just unwind the stack with the
                -- primitive value and leave its arguments in an unevaluated
                -- state (Suspend).
                -> Unwind
ghcUnwind (PrimInfo -> [Type] -> [Value] -> Value
PrimVal PrimInfo
p ([Either Term Type] -> [Type]
forall a b. [Either a b] -> [b]
rights [Either Term Type]
args) ((Term -> Value) -> [Term] -> [Value]
forall a b. (a -> b) -> [a] -> [b]
map Term -> Value
Suspend (Term
e'Term -> [Term] -> [Term]
forall a. a -> [a] -> [a]
:[Term]
es))) Machine
m TyConMap
tcm
                | Bool
otherwise
                -> Machine -> Maybe Machine
forall a. a -> Maybe a
Just (Machine -> Maybe Machine)
-> (Machine -> Machine) -> Machine -> Maybe Machine
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Term -> Machine -> Machine
setTerm Term
e' (Machine -> Maybe Machine) -> Machine -> Maybe Machine
forall a b. (a -> b) -> a -> b
$ StackFrame -> Machine -> Machine
stackPush (PrimInfo -> [Type] -> [Value] -> [Term] -> StackFrame
PrimApply PrimInfo
p ([Either Term Type] -> [Type]
forall a b. [Either a b] -> [b]
rights [Either Term Type]
args) [] [Term]
es) Machine
m

              [Term]
_ -> String -> Maybe Machine
forall a. HasCallStack => String -> a
error String
"internal error"

            Ordering
LT -> [Either TyVar Type] -> Term -> Step
newBinder [Either TyVar Type]
tys' (Term -> Term -> Term
App Term
x Term
y) Machine
m TyConMap
tcm

            Ordering
GT -> let (Machine
m0, Id
n) = TyConMap -> Machine -> Term -> (Machine, Id)
newLetBinding TyConMap
tcm Machine
m Term
y
                   in Machine -> Maybe Machine
forall a. a -> Maybe a
Just (Machine -> Maybe Machine)
-> (Machine -> Machine) -> Machine -> Maybe Machine
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Term -> Machine -> Machine
setTerm Term
x (Machine -> Maybe Machine) -> Machine -> Maybe Machine
forall a b. (a -> b) -> a -> b
$ StackFrame -> Machine -> Machine
stackPush (Id -> StackFrame
Apply Id
n) Machine
m0

    Term
_ -> let (Machine
m0, Id
n) = TyConMap -> Machine -> Term -> (Machine, Id)
newLetBinding TyConMap
tcm Machine
m Term
y
          in Machine -> Maybe Machine
forall a. a -> Maybe a
Just (Machine -> Maybe Machine)
-> (Machine -> Machine) -> Machine -> Maybe Machine
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Term -> Machine -> Machine
setTerm Term
x (Machine -> Maybe Machine) -> Machine -> Maybe Machine
forall a b. (a -> b) -> a -> b
$ StackFrame -> Machine -> Machine
stackPush (Id -> StackFrame
Apply Id
n) Machine
m0
 where
  (Term
term, [Either Term Type]
args, [TickInfo]
_) = Term -> (Term, [Either Term Type], [TickInfo])
collectArgsTicks (Term -> Term -> Term
App Term
x Term
y)
  tys' :: [Either TyVar Type]
tys' = ([Either TyVar Type], Type) -> [Either TyVar Type]
forall a b. (a, b) -> a
fst (([Either TyVar Type], Type) -> [Either TyVar Type])
-> (Term -> ([Either TyVar Type], Type))
-> Term
-> [Either TyVar Type]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Type -> ([Either TyVar Type], Type)
splitFunForallTy (Type -> ([Either TyVar Type], Type))
-> (Term -> Type) -> Term -> ([Either TyVar Type], Type)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TyConMap -> Term -> Type
forall a. InferType a => TyConMap -> a -> Type
inferCoreTypeOf TyConMap
tcm (Term -> [Either TyVar Type]) -> Term -> [Either TyVar Type]
forall a b. (a -> b) -> a -> b
$ Term -> Term -> Term
App Term
x Term
y

stepTyApp :: Term -> Type -> Step
stepTyApp :: Term -> Type -> Step
stepTyApp Term
x Type
ty Machine
m TyConMap
tcm =
  case Term
term of
    Data DataCon
dc ->
      let tys :: [Either TyVar Type]
tys = ([Either TyVar Type], Type) -> [Either TyVar Type]
forall a b. (a, b) -> a
fst (([Either TyVar Type], Type) -> [Either TyVar Type])
-> ([Either TyVar Type], Type) -> [Either TyVar Type]
forall a b. (a -> b) -> a -> b
$ Type -> ([Either TyVar Type], Type)
splitFunForallTy (DataCon -> Type
dcType DataCon
dc)
       in case Int -> Int -> Ordering
forall a. Ord a => a -> a -> Ordering
compare ([Either Term Type] -> Int
forall (t :: Type -> Type) a. Foldable t => t a -> Int
length [Either Term Type]
args) ([Either TyVar Type] -> Int
forall (t :: Type -> Type) a. Foldable t => t a -> Int
length [Either TyVar Type]
tys) of
            Ordering
EQ -> Unwind
ghcUnwind (DataCon -> [Either Term Type] -> Value
DC DataCon
dc [Either Term Type]
args) Machine
m TyConMap
tcm
            Ordering
LT -> [Either TyVar Type] -> Term -> Step
newBinder [Either TyVar Type]
tys' (Term -> Type -> Term
TyApp Term
x Type
ty) Machine
m TyConMap
tcm
            Ordering
GT -> String -> Maybe Machine
forall a. HasCallStack => String -> a
error String
"Overapplied DC"

    Prim PrimInfo
p ->
      let tys :: [Either TyVar Type]
tys = ([Either TyVar Type], Type) -> [Either TyVar Type]
forall a b. (a, b) -> a
fst (([Either TyVar Type], Type) -> [Either TyVar Type])
-> ([Either TyVar Type], Type) -> [Either TyVar Type]
forall a b. (a -> b) -> a -> b
$ Type -> ([Either TyVar Type], Type)
splitFunForallTy (PrimInfo -> Type
primType PrimInfo
p)
       in case Int -> Int -> Ordering
forall a. Ord a => a -> a -> Ordering
compare ([Either Term Type] -> Int
forall (t :: Type -> Type) a. Foldable t => t a -> Int
length [Either Term Type]
args) ([Either TyVar Type] -> Int
forall (t :: Type -> Type) a. Foldable t => t a -> Int
length [Either TyVar Type]
tys) of
            Ordering
EQ -> case [Either Term Type] -> [Term]
forall a b. [Either a b] -> [a]
lefts [Either Term Type]
args of
                    [] | PrimInfo -> Text
primName PrimInfo
p Text -> [Text] -> Bool
forall (t :: Type -> Type) a.
(Foldable t, Eq a) =>
a -> t a -> Bool
`elem` (PrimInfo -> Text) -> [PrimInfo] -> [Text]
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
fmap PrimInfo -> Text
primName [ PrimInfo
NP.removedArg
                                                         , PrimInfo
NP.undefined
                                                         , PrimInfo
NP.undefinedX ] ->
                            Unwind
ghcUnwind (PrimInfo -> [Type] -> [Value] -> Value
PrimVal PrimInfo
p ([Either Term Type] -> [Type]
forall a b. [Either a b] -> [b]
rights [Either Term Type]
args) []) Machine
m TyConMap
tcm

                       | Bool
otherwise ->
                            PrimStep
ghcPrimStep TyConMap
tcm (Machine -> Bool
forcePrims Machine
m) PrimInfo
p ([Either Term Type] -> [Type]
forall a b. [Either a b] -> [b]
rights [Either Term Type]
args) [] Machine
m

                    (Term
e':[Term]
es) ->
                      Machine -> Maybe Machine
forall a. a -> Maybe a
Just (Machine -> Maybe Machine)
-> (Machine -> Machine) -> Machine -> Maybe Machine
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Term -> Machine -> Machine
setTerm Term
e' (Machine -> Maybe Machine) -> Machine -> Maybe Machine
forall a b. (a -> b) -> a -> b
$ StackFrame -> Machine -> Machine
stackPush (PrimInfo -> [Type] -> [Value] -> [Term] -> StackFrame
PrimApply PrimInfo
p ([Either Term Type] -> [Type]
forall a b. [Either a b] -> [b]
rights [Either Term Type]
args) [] [Term]
es) Machine
m

            Ordering
LT -> [Either TyVar Type] -> Term -> Step
newBinder [Either TyVar Type]
tys' (Term -> Type -> Term
TyApp Term
x Type
ty) Machine
m TyConMap
tcm
            Ordering
GT -> Machine -> Maybe Machine
forall a. a -> Maybe a
Just (Machine -> Maybe Machine)
-> (Machine -> Machine) -> Machine -> Maybe Machine
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Term -> Machine -> Machine
setTerm Term
x (Machine -> Maybe Machine) -> Machine -> Maybe Machine
forall a b. (a -> b) -> a -> b
$ StackFrame -> Machine -> Machine
stackPush (Type -> StackFrame
Instantiate Type
ty) Machine
m

    Term
_ -> Machine -> Maybe Machine
forall a. a -> Maybe a
Just (Machine -> Maybe Machine)
-> (Machine -> Machine) -> Machine -> Maybe Machine
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Term -> Machine -> Machine
setTerm Term
x (Machine -> Maybe Machine) -> Machine -> Maybe Machine
forall a b. (a -> b) -> a -> b
$ StackFrame -> Machine -> Machine
stackPush (Type -> StackFrame
Instantiate Type
ty) Machine
m
 where
  (Term
term, [Either Term Type]
args, [TickInfo]
_) = Term -> (Term, [Either Term Type], [TickInfo])
collectArgsTicks (Term -> Type -> Term
TyApp Term
x Type
ty)
  tys' :: [Either TyVar Type]
tys' = ([Either TyVar Type], Type) -> [Either TyVar Type]
forall a b. (a, b) -> a
fst (([Either TyVar Type], Type) -> [Either TyVar Type])
-> (Term -> ([Either TyVar Type], Type))
-> Term
-> [Either TyVar Type]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Type -> ([Either TyVar Type], Type)
splitFunForallTy (Type -> ([Either TyVar Type], Type))
-> (Term -> Type) -> Term -> ([Either TyVar Type], Type)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TyConMap -> Term -> Type
forall a. InferType a => TyConMap -> a -> Type
inferCoreTypeOf TyConMap
tcm (Term -> [Either TyVar Type]) -> Term -> [Either TyVar Type]
forall a b. (a -> b) -> a -> b
$ Term -> Type -> Term
TyApp Term
x Type
ty

stepLet :: Bind Term -> Term -> Step
stepLet :: Bind Term -> Term -> Step
stepLet (NonRec Id
i Term
b) Term
x Machine
m TyConMap
_ = Machine -> Maybe Machine
forall a. a -> Maybe a
Just ([LetBinding] -> Term -> Machine -> Machine
allocate [(Id
i,Term
b)] Term
x Machine
m)
stepLet (Rec [LetBinding]
bs) Term
x Machine
m TyConMap
_ = Machine -> Maybe Machine
forall a. a -> Maybe a
Just ([LetBinding] -> Term -> Machine -> Machine
allocate [LetBinding]
bs Term
x Machine
m)

stepCase :: Term -> Type -> [Alt] -> Step
stepCase :: Term -> Type -> [Alt] -> Step
stepCase Term
scrut Type
ty [Alt]
alts Machine
m TyConMap
_ =
  Machine -> Maybe Machine
forall a. a -> Maybe a
Just (Machine -> Maybe Machine)
-> (Machine -> Machine) -> Machine -> Maybe Machine
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Term -> Machine -> Machine
setTerm Term
scrut (Machine -> Maybe Machine) -> Machine -> Maybe Machine
forall a b. (a -> b) -> a -> b
$ StackFrame -> Machine -> Machine
stackPush (Type -> [Alt] -> StackFrame
Scrutinise Type
ty [Alt]
alts) Machine
m

-- TODO Support stepwise evaluation of casts.
--
stepCast :: Term -> Type -> Type -> Step
stepCast :: Term -> Type -> Type -> Step
stepCast Term
_ Type
_ Type
_ Machine
_ TyConMap
_ =
  (String -> Maybe Machine -> Maybe Machine)
-> Maybe Machine -> String -> Maybe Machine
forall a b c. (a -> b -> c) -> b -> a -> c
flip String -> Maybe Machine -> Maybe Machine
forall a. String -> a -> a
trace Maybe Machine
forall a. Maybe a
Nothing (String -> Maybe Machine) -> String -> Maybe Machine
forall a b. (a -> b) -> a -> b
$ [String] -> String
unlines
    [ String
"WARNING: " String -> String -> String
forall a. Semigroup a => a -> a -> a
<> $(String
curLoc) String -> String -> String
forall a. Semigroup a => a -> a -> a
<> String
"Clash can't symbolically evaluate casts"
    , String
"Please file an issue at https://github.com/clash-lang/clash-compiler/issues"
    ]

stepTick :: TickInfo -> Term -> Step
stepTick :: TickInfo -> Term -> Step
stepTick TickInfo
tick Term
x Machine
m TyConMap
_ =
  Machine -> Maybe Machine
forall a. a -> Maybe a
Just (Machine -> Maybe Machine)
-> (Machine -> Machine) -> Machine -> Maybe Machine
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Term -> Machine -> Machine
setTerm Term
x (Machine -> Maybe Machine) -> Machine -> Maybe Machine
forall a b. (a -> b) -> a -> b
$ StackFrame -> Machine -> Machine
stackPush (TickInfo -> StackFrame
Tickish TickInfo
tick) Machine
m

-- | Small-step operational semantics.
--
ghcStep :: Step
ghcStep :: Step
ghcStep Machine
m = case Machine -> Term
mTerm Machine
m of
  Var Id
i -> Id -> Step
stepVar Id
i Machine
m
  Data DataCon
dc -> DataCon -> Step
stepData DataCon
dc Machine
m
  Literal Literal
l -> Literal -> Step
stepLiteral Literal
l Machine
m
  Prim PrimInfo
p -> PrimInfo -> Step
stepPrim PrimInfo
p Machine
m
  Lam Id
v Term
x -> Id -> Term -> Step
stepLam Id
v Term
x Machine
m
  TyLam TyVar
v Term
x -> TyVar -> Term -> Step
stepTyLam TyVar
v Term
x Machine
m
  App Term
x Term
y -> Term -> Term -> Step
stepApp Term
x Term
y Machine
m
  TyApp Term
x Type
ty -> Term -> Type -> Step
stepTyApp Term
x Type
ty Machine
m
  Let Bind Term
bs Term
x -> Bind Term -> Term -> Step
stepLet Bind Term
bs Term
x Machine
m
  Case Term
s Type
ty [Alt]
as -> Term -> Type -> [Alt] -> Step
stepCase Term
s Type
ty [Alt]
as Machine
m
  Cast Term
x Type
a Type
b -> Term -> Type -> Type -> Step
stepCast Term
x Type
a Type
b Machine
m
  Tick TickInfo
t Term
x -> TickInfo -> Term -> Step
stepTick TickInfo
t Term
x Machine
m

-- | Take a list of types or type variables and create a lambda / type lambda
-- for each one around the given term.
--
newBinder :: [Either TyVar Type] -> Term -> Step
newBinder :: [Either TyVar Type] -> Term -> Step
newBinder [Either TyVar Type]
tys Term
e Machine
m TyConMap
tcm =
  let ((Supply
supply1,InScopeSet
_), Term
e1) = (Supply, InScopeSet)
-> [Either TyVar Type] -> ((Supply, InScopeSet), Term)
etaExpand (Machine -> Supply
mSupply Machine
m, Machine -> InScopeSet
mScopeNames Machine
m) [Either TyVar Type]
tys
      m1 :: Machine
m1 = Machine
m { mSupply :: Supply
mSupply = Supply
supply1, mTerm :: Term
mTerm = Term
e1 }
   in Step
ghcStep Machine
m1 TyConMap
tcm
 where
  etaExpand :: (Supply, InScopeSet)
-> [Either TyVar Type] -> ((Supply, InScopeSet), Term)
etaExpand (Supply, InScopeSet)
env [Either TyVar Type]
args =
    let ((Supply, InScopeSet)
env1,[Either Id TyVar]
args1) = ((Supply, InScopeSet)
 -> Either TyVar Type -> ((Supply, InScopeSet), Either Id TyVar))
-> (Supply, InScopeSet)
-> [Either TyVar Type]
-> ((Supply, InScopeSet), [Either Id TyVar])
forall (t :: Type -> Type) a b c.
Traversable t =>
(a -> b -> (a, c)) -> a -> t b -> (a, t c)
mapAccumL (Supply, InScopeSet)
-> Either TyVar Type -> ((Supply, InScopeSet), Either Id TyVar)
forall b.
(Supply, InScopeSet)
-> Either b Type -> ((Supply, InScopeSet), Either Id b)
go (Supply, InScopeSet)
env [Either TyVar Type]
args
     in ((Supply, InScopeSet)
env1,Term -> [Either Id TyVar] -> Term
mkAbstraction ((Term -> Either Id TyVar -> Term)
-> Term -> [Either Id TyVar] -> Term
forall (t :: Type -> Type) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl' Term -> Either Id TyVar -> Term
go2 Term
e [Either Id TyVar]
args1) [Either Id TyVar]
args1)

  go :: (Supply, InScopeSet)
-> Either b Type -> ((Supply, InScopeSet), Either Id b)
go (Supply, InScopeSet)
env (Left b
tv) = ((Supply, InScopeSet)
env, b -> Either Id b
forall a b. b -> Either a b
Right b
tv)
  go (Supply, InScopeSet)
env (Right Type
ty) =
    let ((Supply, InScopeSet)
env1, Id
n) = (Supply, InScopeSet) -> (Text, Type) -> ((Supply, InScopeSet), Id)
mkUniqSystemId (Supply, InScopeSet)
env (Text
"x", Type
ty)
     in ((Supply, InScopeSet)
env1, Id -> Either Id b
forall a b. a -> Either a b
Left Id
n)

  go2 :: Term -> Either Id TyVar -> Term
go2 Term
u (Left Id
i) = Term -> Term -> Term
App Term
u (Id -> Term
Var Id
i)
  go2 Term
u (Right TyVar
tv) = Term -> Type -> Term
TyApp Term
u (TyVar -> Type
VarTy TyVar
tv)

newLetBinding
  :: TyConMap
  -> Machine
  -> Term
  -> (Machine, Id)
newLetBinding :: TyConMap -> Machine -> Term -> (Machine, Id)
newLetBinding TyConMap
tcm Machine
m Term
e
  | Var Id
v <- Term
e
  , IdScope -> Id -> Machine -> Bool
heapContains IdScope
LocalId Id
v Machine
m
  = (Machine
m, Id
v)

  | Bool
otherwise
  = let m' :: Machine
m' = IdScope -> Id -> Term -> Machine -> Machine
heapInsert IdScope
LocalId Id
id_ Term
e Machine
m
     in (Machine
m' { mSupply :: Supply
mSupply = Supply
ids', mScopeNames :: InScopeSet
mScopeNames = InScopeSet
is1 }, Id
id_)
 where
  ty :: Type
ty = TyConMap -> Term -> Type
forall a. InferType a => TyConMap -> a -> Type
inferCoreTypeOf TyConMap
tcm Term
e
  ((Supply
ids', InScopeSet
is1), Id
id_) = (Supply, InScopeSet) -> (Text, Type) -> ((Supply, InScopeSet), Id)
mkUniqSystemId (Machine -> Supply
mSupply Machine
m, Machine -> InScopeSet
mScopeNames Machine
m) (Text
"x", Type
ty)

-- | Unwind the stack by 1
ghcUnwind :: Unwind
ghcUnwind :: Unwind
ghcUnwind Value
v Machine
m TyConMap
tcm = do
  (Machine
m', StackFrame
kf) <- Machine -> Maybe (Machine, StackFrame)
stackPop Machine
m
  StackFrame -> Machine -> Maybe Machine
go StackFrame
kf Machine
m'
 where
  go :: StackFrame -> Machine -> Maybe Machine
go (Update IdScope
s Id
x)             = Machine -> Maybe Machine
forall (m :: Type -> Type) a. Monad m => a -> m a
return (Machine -> Maybe Machine)
-> (Machine -> Machine) -> Machine -> Maybe Machine
forall b c a. (b -> c) -> (a -> b) -> a -> c
. IdScope -> Id -> Value -> Machine -> Machine
update IdScope
s Id
x Value
v
  go (Apply Id
x)                = Machine -> Maybe Machine
forall (m :: Type -> Type) a. Monad m => a -> m a
return (Machine -> Maybe Machine)
-> (Machine -> Machine) -> Machine -> Maybe Machine
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TyConMap -> Value -> Id -> Machine -> Machine
apply TyConMap
tcm Value
v Id
x
  go (Instantiate Type
ty)         = Machine -> Maybe Machine
forall (m :: Type -> Type) a. Monad m => a -> m a
return (Machine -> Maybe Machine)
-> (Machine -> Machine) -> Machine -> Maybe Machine
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TyConMap -> Value -> Type -> Machine -> Machine
instantiate TyConMap
tcm Value
v Type
ty
  go (PrimApply PrimInfo
p [Type]
tys [Value]
vs [Term]
tms) = PrimUnwind
ghcPrimUnwind TyConMap
tcm PrimInfo
p [Type]
tys [Value]
vs Value
v [Term]
tms
  go (Scrutinise Type
altTy [Alt]
as)    = Machine -> Maybe Machine
forall (m :: Type -> Type) a. Monad m => a -> m a
return (Machine -> Maybe Machine)
-> (Machine -> Machine) -> Machine -> Maybe Machine
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Value -> Type -> [Alt] -> Machine -> Machine
scrutinise Value
v Type
altTy [Alt]
as
  go (Tickish TickInfo
_)              = Machine -> Maybe Machine
forall (m :: Type -> Type) a. Monad m => a -> m a
return (Machine -> Maybe Machine)
-> (Machine -> Machine) -> Machine -> Maybe Machine
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Term -> Machine -> Machine
setTerm (Value -> Term
valToTerm Value
v)

-- | Update the Heap with the evaluated term
update :: IdScope -> Id -> Value -> Machine -> Machine
update :: IdScope -> Id -> Value -> Machine -> Machine
update IdScope
s Id
x (Value -> Term
valToTerm -> Term
term) =
  Term -> Machine -> Machine
setTerm Term
term (Machine -> Machine) -> (Machine -> Machine) -> Machine -> Machine
forall b c a. (b -> c) -> (a -> b) -> a -> c
. IdScope -> Id -> Term -> Machine -> Machine
heapInsert IdScope
s Id
x Term
term

-- | Apply a value to a function
apply :: TyConMap -> Value -> Id -> Machine -> Machine
apply :: TyConMap -> Value -> Id -> Machine -> Machine
apply TyConMap
_tcm (Lambda Id
x' Term
e) Id
x Machine
m =
  Term -> Machine -> Machine
setTerm (HasCallStack => Doc () -> Subst -> Term -> Term
Doc () -> Subst -> Term -> Term
substTm Doc ()
"Evaluator.apply" Subst
subst Term
e) Machine
m
 where
  subst :: Subst
subst  = Subst -> Id -> Term -> Subst
extendIdSubst Subst
subst0 Id
x' (Id -> Term
Var Id
x)
  subst0 :: Subst
subst0 = InScopeSet -> Subst
mkSubst (InScopeSet -> Subst) -> InScopeSet -> Subst
forall a b. (a -> b) -> a -> b
$ InScopeSet -> Id -> InScopeSet
forall a. InScopeSet -> Var a -> InScopeSet
extendInScopeSet (Machine -> InScopeSet
mScopeNames Machine
m) Id
x
apply TyConMap
tcm pVal :: Value
pVal@(PrimVal (PrimInfo{Type
primType :: Type
primType :: PrimInfo -> Type
primType}) [Type]
tys [Value]
vs) Id
x Machine
m
  | Value -> Bool
isUndefinedXPrimVal Value
pVal
  = Term -> Machine -> Machine
setTerm (Term -> Type -> Term
TyApp (PrimInfo -> Term
Prim PrimInfo
NP.undefinedX) Type
ty) Machine
m
  | Value -> Bool
isUndefinedPrimVal Value
pVal
  = Term -> Machine -> Machine
setTerm (Term -> Type -> Term
TyApp (PrimInfo -> Term
Prim PrimInfo
NP.undefined) Type
ty) Machine
m
 where
  ty :: Type
ty = HasCallStack => TyConMap -> Type -> [Type] -> Type
TyConMap -> Type -> [Type] -> Type
piResultTys TyConMap
tcm Type
primType ([Type]
tys [Type] -> [Type] -> [Type]
forall a. [a] -> [a] -> [a]
++ (Value -> Type) -> [Value] -> [Type]
forall a b. (a -> b) -> [a] -> [b]
map (TyConMap -> Term -> Type
forall a. InferType a => TyConMap -> a -> Type
inferCoreTypeOf TyConMap
tcm (Term -> Type) -> (Value -> Term) -> Value -> Type
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Value -> Term
valToTerm) [Value]
vs [Type] -> [Type] -> [Type]
forall a. [a] -> [a] -> [a]
++ [Id -> Type
forall a. Var a -> Type
varType Id
x])

apply TyConMap
_ Value
v Id
_ Machine
m = String -> Machine
forall a. HasCallStack => String -> a
error (String -> Machine) -> String -> Machine
forall a b. (a -> b) -> a -> b
$ String
"Evaluator.apply: Not a lambda: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Value -> String
forall a. Show a => a -> String
show Value
v String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"\n" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Machine -> String
forall a. Show a => a -> String
show Machine
m

-- | Instantiate a type-abstraction
instantiate :: TyConMap -> Value -> Type -> Machine -> Machine
instantiate :: TyConMap -> Value -> Type -> Machine -> Machine
instantiate TyConMap
_tcm (TyLambda TyVar
x Term
e) Type
ty Machine
m =
  Term -> Machine -> Machine
setTerm (HasCallStack => Doc () -> Subst -> Term -> Term
Doc () -> Subst -> Term -> Term
substTm Doc ()
"Evaluator.instantiate1" Subst
subst Term
e) Machine
m
 where
  subst :: Subst
subst  = Subst -> TyVar -> Type -> Subst
extendTvSubst Subst
subst0 TyVar
x Type
ty
  subst0 :: Subst
subst0 = InScopeSet -> Subst
mkSubst InScopeSet
iss0
  iss0 :: InScopeSet
iss0   = VarSet -> InScopeSet
mkInScopeSet (Term -> VarSet
forall a. HasFreeVars a => a -> VarSet
freeVarsOf Term
e VarSet -> VarSet -> VarSet
forall a. Semigroup a => a -> a -> a
<> Type -> VarSet
forall a. HasFreeVars a => a -> VarSet
freeVarsOf Type
ty)
-- The evaluator is setup in such a way that under normal conditions anything
-- of type 'forall a . ty' must be a ty-lambda.
--
-- However, sometimes we evaluate to an error /value/. When this happens,
-- instead of doing a regural type substitition we:
--
-- 1. Calculate the 'forall a . ty' type of the error value
-- 2. Substitute the 'a' by the applied type.
-- 3. Create a new error value of the shape: 'undefined @substituted_type'
--    Where this particular 'undefined' has type 'forall a . a'. We destinquish
--    between error values throwing X exceptions and other error values, and
--    create appropriate error values that we return. We make this distinctions
--    in onder to enable conversion of X-exception throwing code to undefined
--    bitvectors.
instantiate TyConMap
tcm pVal :: Value
pVal@(PrimVal (PrimInfo{Type
primType :: Type
primType :: PrimInfo -> Type
primType}) [Type]
tys [Value]
es) Type
ty Machine
m
  | Value -> Bool
isUndefinedXPrimVal Value
pVal
  = Term -> Machine -> Machine
setTerm (Term -> Type -> Term
TyApp (PrimInfo -> Term
Prim PrimInfo
NP.undefinedX) Type
primType1) Machine
m
  | Value -> Bool
isUndefinedPrimVal Value
pVal
  = Term -> Machine -> Machine
setTerm (Term -> Type -> Term
TyApp (PrimInfo -> Term
Prim PrimInfo
NP.undefined) Type
primType1) Machine
m
 where
  esTys :: [Type]
esTys = (Value -> Type) -> [Value] -> [Type]
forall a b. (a -> b) -> [a] -> [b]
map (TyConMap -> Value -> Type
forall a. InferType a => TyConMap -> a -> Type
inferCoreTypeOf TyConMap
tcm) [Value]
es
  -- Calculate the type of: prim @ty0 .. @tyN e0 .. eN @ty
  --
  -- This combines the above-mentioned step 1 and 2
  primType1 :: Type
primType1 = HasCallStack => TyConMap -> Type -> [Type] -> Type
TyConMap -> Type -> [Type] -> Type
piResultTys TyConMap
tcm Type
primType ([Type]
tys [Type] -> [Type] -> [Type]
forall a. [a] -> [a] -> [a]
++ [Type]
esTys [Type] -> [Type] -> [Type]
forall a. [a] -> [a] -> [a]
++ [Type
ty])

instantiate TyConMap
_ Value
p Type
_ Machine
_ = String -> Machine
forall a. HasCallStack => String -> a
error (String -> Machine) -> String -> Machine
forall a b. (a -> b) -> a -> b
$ String
"Evaluator.instantiate: Not a tylambda: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Value -> String
forall a. Show a => a -> String
show Value
p

-- | Evaluate a case-expression
scrutinise :: Value -> Type -> [Alt] -> Machine -> Machine
scrutinise :: Value -> Type -> [Alt] -> Machine -> Machine
scrutinise Value
v Type
_altTy [] Machine
m = Term -> Machine -> Machine
setTerm (Value -> Term
valToTerm Value
v) Machine
m
-- [Note: empty case expressions]
--
-- Clash does not have empty case-expressions; instead, empty case-expressions
-- are used to indicate that the `whnf` function was called the context of a
-- case-expression, which means certain special primitives must be forced.
-- See also [Note: forcing special primitives]
scrutinise (Lit Literal
l) Type
_altTy [Alt]
alts Machine
m = case [Alt]
alts of
  (Pat
DefaultPat, Term
altE):[Alt]
alts1 -> Term -> Machine -> Machine
setTerm (Term -> [Alt] -> Term
go Term
altE [Alt]
alts1) Machine
m
  [Alt]
_ -> let term :: Term
term = Term -> [Alt] -> Term
go (String -> Term
forall a. HasCallStack => String -> a
error (String -> Term) -> String -> Term
forall a b. (a -> b) -> a -> b
$ String
"Evaluator.scrutinise: no match "
                    String -> String -> String
forall a. Semigroup a => a -> a -> a
<> Term -> String
forall p. PrettyPrec p => p -> String
showPpr (Term -> Type -> [Alt] -> Term
Case (Value -> Term
valToTerm (Literal -> Value
Lit Literal
l)) (ConstTy -> Type
ConstTy ConstTy
Arrow) [Alt]
alts)) [Alt]
alts
        in Term -> Machine -> Machine
setTerm Term
term Machine
m
 where
  go :: Term -> [Alt] -> Term
go Term
def [] = Term
def
  go Term
_ ((LitPat Literal
l1,Term
altE):[Alt]
_) | Literal
l1 Literal -> Literal -> Bool
forall a. Eq a => a -> a -> Bool
== Literal
l = Term
altE
  go Term
_ ((DataPat DataCon
dc [] [Id
x],Term
altE):[Alt]
_)
    | IntegerLiteral Integer
l1 <- Literal
l
    , Just Literal
patE <- case DataCon -> Int
dcTag DataCon
dc of
       Int
1 | Integer
l1 Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
>= ((-Integer
2)Integer -> Int -> Integer
forall a b. (Num a, Integral b) => a -> b -> a
^(Int
63::Int)) Bool -> Bool -> Bool
&&  Integer
l1 Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
< Integer
2Integer -> Int -> Integer
forall a b. (Num a, Integral b) => a -> b -> a
^(Int
63::Int) ->
          Literal -> Maybe Literal
forall a. a -> Maybe a
Just (Integer -> Literal
IntLiteral Integer
l1)
       Int
2 | Integer
l1 Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
>= (Integer
2Integer -> Int -> Integer
forall a b. (Num a, Integral b) => a -> b -> a
^(Int
63::Int)) ->
#if MIN_VERSION_base(4,15,0)
          let !(IP ba0) = l1
#else
          let !(Jp# !(BN# ByteArray#
ba0)) = Integer
l1
#endif
              ba1 :: ByteArray
ba1 = ByteArray# -> ByteArray
BA.ByteArray ByteArray#
ba0
          in  Literal -> Maybe Literal
forall a. a -> Maybe a
Just (ByteArray -> Literal
ByteArrayLiteral ByteArray
ba1)
       Int
3 | Integer
l1 Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
< ((-Integer
2)Integer -> Int -> Integer
forall a b. (Num a, Integral b) => a -> b -> a
^(Int
63::Int)) ->
#if MIN_VERSION_base(4,15,0)
          let !(IN ba0) = l1
#else
          let !(Jn# !(BN# ByteArray#
ba0)) = Integer
l1
#endif
              ba1 :: ByteArray
ba1 = ByteArray# -> ByteArray
BA.ByteArray ByteArray#
ba0
          in  Literal -> Maybe Literal
forall a. a -> Maybe a
Just (ByteArray -> Literal
ByteArrayLiteral ByteArray
ba1)
       Int
_ -> Maybe Literal
forall a. Maybe a
Nothing
    = let inScope :: VarSet
inScope = Term -> VarSet
forall a. HasFreeVars a => a -> VarSet
freeVarsOf Term
altE
          subst0 :: Subst
subst0  = InScopeSet -> Subst
mkSubst (VarSet -> InScopeSet
mkInScopeSet VarSet
inScope)
          subst1 :: Subst
subst1  = Subst -> Id -> Term -> Subst
extendIdSubst Subst
subst0 Id
x (Literal -> Term
Literal Literal
patE)
      in  HasCallStack => Doc () -> Subst -> Term -> Term
Doc () -> Subst -> Term -> Term
substTm Doc ()
"Evaluator.scrutinise" Subst
subst1 Term
altE
    | NaturalLiteral Integer
l1  <- Literal
l
    , Just Literal
patE <- case DataCon -> Int
dcTag DataCon
dc of
       Int
1 | Integer
l1 Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
>= Integer
0 Bool -> Bool -> Bool
&&  Integer
l1 Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
< Integer
2Integer -> Int -> Integer
forall a b. (Num a, Integral b) => a -> b -> a
^(Int
64::Int) ->
          Literal -> Maybe Literal
forall a. a -> Maybe a
Just (Integer -> Literal
WordLiteral Integer
l1)
       Int
2 | Integer
l1 Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
>= (Integer
2Integer -> Int -> Integer
forall a b. (Num a, Integral b) => a -> b -> a
^(Int
64::Int)) ->
#if MIN_VERSION_base(4,15,0)
          let !(IP ba0) = l1
#else
          let !(Jp# !(BN# ByteArray#
ba0)) = Integer
l1
#endif
              ba1 :: ByteArray
ba1 = ByteArray# -> ByteArray
BA.ByteArray ByteArray#
ba0
          in  Literal -> Maybe Literal
forall a. a -> Maybe a
Just (ByteArray -> Literal
ByteArrayLiteral ByteArray
ba1)
       Int
_ -> Maybe Literal
forall a. Maybe a
Nothing
    = let inScope :: VarSet
inScope = Term -> VarSet
forall a. HasFreeVars a => a -> VarSet
freeVarsOf Term
altE
          subst0 :: Subst
subst0  = InScopeSet -> Subst
mkSubst (VarSet -> InScopeSet
mkInScopeSet VarSet
inScope)
          subst1 :: Subst
subst1  = Subst -> Id -> Term -> Subst
extendIdSubst Subst
subst0 Id
x (Literal -> Term
Literal Literal
patE)
      in  HasCallStack => Doc () -> Subst -> Term -> Term
Doc () -> Subst -> Term -> Term
substTm Doc ()
"Evaluator.scrutinise" Subst
subst1 Term
altE
  go Term
def (Alt
_:[Alt]
alts1) = Term -> [Alt] -> Term
go Term
def [Alt]
alts1

scrutinise (DC DataCon
dc [Either Term Type]
xs) Type
_altTy [Alt]
alts Machine
m
  | Term
altE:[Term]
_ <- [DataCon -> [TyVar] -> [Id] -> [Either Term Type] -> Term -> Term
substInAlt DataCon
altDc [TyVar]
tvs [Id]
pxs [Either Term Type]
xs Term
altE
              | (DataPat DataCon
altDc [TyVar]
tvs [Id]
pxs,Term
altE) <- [Alt]
alts, DataCon
altDc DataCon -> DataCon -> Bool
forall a. Eq a => a -> a -> Bool
== DataCon
dc ] [Term] -> [Term] -> [Term]
forall a. [a] -> [a] -> [a]
++
              [Term
altE | (Pat
DefaultPat,Term
altE) <- [Alt]
alts ]
  = Term -> Machine -> Machine
setTerm Term
altE Machine
m

scrutinise v :: Value
v@(PrimVal PrimInfo
p [Type]
_ [Value]
vs) Type
altTy [Alt]
alts Machine
m
  | Value -> Bool
isUndefinedXPrimVal Value
v
  = Term -> Machine -> Machine
setTerm (Term -> Type -> Term
TyApp (PrimInfo -> Term
Prim PrimInfo
NP.undefinedX) Type
altTy) Machine
m
  | Value -> Bool
isUndefinedPrimVal Value
v
  = Term -> Machine -> Machine
setTerm (Term -> Type -> Term
TyApp (PrimInfo -> Term
Prim PrimInfo
NP.undefined) Type
altTy) Machine
m

  | (Alt -> Bool) -> [Alt] -> Bool
forall (t :: Type -> Type) a.
Foldable t =>
(a -> Bool) -> t a -> Bool
any (\case {(LitPat {},Term
_) -> Bool
True; Alt
_ -> Bool
False}) [Alt]
alts
  = case [Alt]
alts of
      ((Pat
DefaultPat,Term
altE):[Alt]
alts1) -> Term -> Machine -> Machine
setTerm (Term -> [Alt] -> Term
forall t. t -> [(Pat, t)] -> t
go Term
altE [Alt]
alts1) Machine
m
      [Alt]
_ -> let term :: Term
term = Term -> [Alt] -> Term
forall t. t -> [(Pat, t)] -> t
go (String -> Term
forall a. HasCallStack => String -> a
error (String -> Term) -> String -> Term
forall a b. (a -> b) -> a -> b
$ String
"Evaluator.scrutinise: no match "
                        String -> String -> String
forall a. Semigroup a => a -> a -> a
<> Term -> String
forall p. PrettyPrec p => p -> String
showPpr (Term -> Type -> [Alt] -> Term
Case (Value -> Term
valToTerm Value
v) (ConstTy -> Type
ConstTy ConstTy
Arrow) [Alt]
alts)) [Alt]
alts
            in Term -> Machine -> Machine
setTerm Term
term Machine
m
 where
  go :: t -> [(Pat, t)] -> t
go t
def [] = t
def
  go t
_   ((LitPat Literal
l1,t
altE):[(Pat, t)]
_) | Literal
l1 Literal -> Literal -> Bool
forall a. Eq a => a -> a -> Bool
== Literal
l = t
altE
  go t
def ((Pat, t)
_:[(Pat, t)]
alts1) = t -> [(Pat, t)] -> t
go t
def [(Pat, t)]
alts1

  l :: Literal
l = case PrimInfo -> Text
primName PrimInfo
p of
        Text
"Clash.Sized.Internal.BitVector.fromInteger##"
          | [Lit (WordLiteral Integer
0), Lit Literal
l0] <- [Value]
vs -> Literal
l0
        Text
"Clash.Sized.Internal.BitVector.fromInteger#"
          | [Value
_,Lit (NaturalLiteral Integer
0),Lit Literal
l0] <- [Value]
vs -> Literal
l0
        Text
"Clash.Sized.Internal.Index.fromInteger#"
          | [Value
_,Lit Literal
l0] <- [Value]
vs -> Literal
l0
        Text
"Clash.Sized.Internal.Signed.fromInteger#"
          | [Value
_,Lit Literal
l0] <- [Value]
vs -> Literal
l0
        Text
"Clash.Sized.Internal.Unsigned.fromInteger#"
          | [Value
_,Lit Literal
l0] <- [Value]
vs -> Literal
l0
        Text
_ -> String -> Literal
forall a. HasCallStack => String -> a
error (String
"scrutinise: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Term -> String
forall p. PrettyPrec p => p -> String
showPpr (Term -> Type -> [Alt] -> Term
Case (Value -> Term
valToTerm Value
v) (ConstTy -> Type
ConstTy ConstTy
Arrow) [Alt]
alts))

scrutinise Value
v Type
_altTy [Alt]
alts Machine
_ =
  String -> Machine
forall a. HasCallStack => String -> a
error (String
"scrutinise: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Term -> String
forall p. PrettyPrec p => p -> String
showPpr (Term -> Type -> [Alt] -> Term
Case (Value -> Term
valToTerm Value
v) (ConstTy -> Type
ConstTy ConstTy
Arrow) [Alt]
alts))

substInAlt :: DataCon -> [TyVar] -> [Id] -> [Either Term Type] -> Term -> Term
substInAlt :: DataCon -> [TyVar] -> [Id] -> [Either Term Type] -> Term -> Term
substInAlt DataCon
dc [TyVar]
tvs [Id]
xs [Either Term Type]
args Term
e = HasCallStack => Doc () -> Subst -> Term -> Term
Doc () -> Subst -> Term -> Term
substTm Doc ()
"Evaluator.substInAlt" Subst
subst Term
e
 where
  tys :: [Type]
tys        = [Either Term Type] -> [Type]
forall a b. [Either a b] -> [b]
rights [Either Term Type]
args
  tms :: [Term]
tms        = [Either Term Type] -> [Term]
forall a b. [Either a b] -> [a]
lefts [Either Term Type]
args
  substTyMap :: [(TyVar, Type)]
substTyMap = [TyVar] -> [Type] -> [(TyVar, Type)]
forall a b. [a] -> [b] -> [(a, b)]
zip [TyVar]
tvs (Int -> [Type] -> [Type]
forall a. Int -> [a] -> [a]
drop ([TyVar] -> Int
forall (t :: Type -> Type) a. Foldable t => t a -> Int
length (DataCon -> [TyVar]
dcUnivTyVars DataCon
dc)) [Type]
tys)
  substTmMap :: [LetBinding]
substTmMap = [Id] -> [Term] -> [LetBinding]
forall a b. [a] -> [b] -> [(a, b)]
zip [Id]
xs [Term]
tms
  inScope :: VarSet
inScope    = [Type] -> VarSet
forall a. HasFreeVars a => a -> VarSet
freeVarsOf [Type]
tys VarSet -> VarSet -> VarSet
`unionVarSet` [Term] -> VarSet
forall a. HasFreeVars a => a -> VarSet
freeVarsOf (Term
eTerm -> [Term] -> [Term]
forall a. a -> [a] -> [a]
:[Term]
tms)
  subst :: Subst
subst      = Subst -> [(TyVar, Type)] -> Subst
extendTvSubstList (Subst -> [LetBinding] -> Subst
extendIdSubstList Subst
subst0 [LetBinding]
substTmMap) [(TyVar, Type)]
substTyMap
  subst0 :: Subst
subst0     = InScopeSet -> Subst
mkSubst (VarSet -> InScopeSet
mkInScopeSet VarSet
inScope)

-- | Allocate let-bindings on the heap
allocate :: [LetBinding] -> Term -> Machine -> Machine
allocate :: [LetBinding] -> Term -> Machine -> Machine
allocate [LetBinding]
xes Term
e Machine
m =
  Machine
m { mHeapLocal :: PureHeap
mHeapLocal = PureHeap -> [LetBinding] -> PureHeap
forall a b. VarEnv a -> [(Var b, a)] -> VarEnv a
extendVarEnvList (Machine -> PureHeap
mHeapLocal Machine
m) [LetBinding]
xes'
    , mSupply :: Supply
mSupply = Supply
ids'
    , mScopeNames :: InScopeSet
mScopeNames = InScopeSet
isN
    , mTerm :: Term
mTerm = Term
e'
    }
 where
  xNms :: [Id]
xNms      = (LetBinding -> Id) -> [LetBinding] -> [Id]
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
fmap LetBinding -> Id
forall a b. (a, b) -> a
fst [LetBinding]
xes
  is1 :: InScopeSet
is1       = InScopeSet -> [Id] -> InScopeSet
forall a. InScopeSet -> [Var a] -> InScopeSet
extendInScopeSetList (Machine -> InScopeSet
mScopeNames Machine
m) [Id]
xNms
  (Supply
ids', [(Id, LetBinding)]
s) = (Supply -> Id -> (Supply, (Id, LetBinding)))
-> Supply -> [Id] -> (Supply, [(Id, LetBinding)])
forall (t :: Type -> Type) a b c.
Traversable t =>
(a -> b -> (a, c)) -> a -> t b -> (a, t c)
mapAccumL (PureHeap -> Supply -> Id -> (Supply, (Id, LetBinding))
letSubst (Machine -> PureHeap
mHeapLocal Machine
m)) (Machine -> Supply
mSupply Machine
m) [Id]
xNms
  ([Id]
nms, [LetBinding]
s') = [(Id, LetBinding)] -> ([Id], [LetBinding])
forall a b. [(a, b)] -> ([a], [b])
unzip [(Id, LetBinding)]
s
  isN :: InScopeSet
isN       = InScopeSet -> [Id] -> InScopeSet
forall a. InScopeSet -> [Var a] -> InScopeSet
extendInScopeSetList InScopeSet
is1 [Id]
nms
  subst :: Subst
subst     = Subst -> [LetBinding] -> Subst
extendIdSubstList Subst
subst0 [LetBinding]
s'
  subst0 :: Subst
subst0    = InScopeSet -> Subst
mkSubst ((InScopeSet -> Id -> InScopeSet)
-> InScopeSet -> [Id] -> InScopeSet
forall (t :: Type -> Type) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl' InScopeSet -> Id -> InScopeSet
forall a. InScopeSet -> Var a -> InScopeSet
extendInScopeSet InScopeSet
is1 [Id]
nms)
  xes' :: [LetBinding]
xes'      = [Id] -> [Term] -> [LetBinding]
forall a b. [a] -> [b] -> [(a, b)]
zip [Id]
nms ((LetBinding -> Term) -> [LetBinding] -> [Term]
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
fmap (HasCallStack => Doc () -> Subst -> Term -> Term
Doc () -> Subst -> Term -> Term
substTm Doc ()
"Evaluator.allocate0" Subst
subst (Term -> Term) -> (LetBinding -> Term) -> LetBinding -> Term
forall b c a. (b -> c) -> (a -> b) -> a -> c
. LetBinding -> Term
forall a b. (a, b) -> b
snd) [LetBinding]
xes)
  e' :: Term
e'        = HasCallStack => Doc () -> Subst -> Term -> Term
Doc () -> Subst -> Term -> Term
substTm Doc ()
"Evaluator.allocate1" Subst
subst Term
e

-- | Create a unique name and substitution for a let-binder
letSubst
  :: PureHeap
  -> Supply
  -> Id
  -> (Supply, (Id, (Id, Term)))
letSubst :: PureHeap -> Supply -> Id -> (Supply, (Id, LetBinding))
letSubst PureHeap
h Supply
acc Id
id0 =
  let (Supply
acc',Id
id1) = PureHeap -> Supply -> Id -> (Supply, Id)
mkUniqueHeapId PureHeap
h Supply
acc Id
id0
  in  (Supply
acc',(Id
id1,(Id
id0,Id -> Term
Var Id
id1)))
 where
  mkUniqueHeapId :: PureHeap -> Supply -> Id -> (Supply, Id)
  mkUniqueHeapId :: PureHeap -> Supply -> Id -> (Supply, Id)
mkUniqueHeapId PureHeap
h' Supply
ids Id
x =
    (Supply, Id)
-> (Term -> (Supply, Id)) -> Maybe Term -> (Supply, Id)
forall b a. b -> (a -> b) -> Maybe a -> b
maybe (Supply
ids', Id
x') ((Supply, Id) -> Term -> (Supply, Id)
forall a b. a -> b -> a
const ((Supply, Id) -> Term -> (Supply, Id))
-> (Supply, Id) -> Term -> (Supply, Id)
forall a b. (a -> b) -> a -> b
$ PureHeap -> Supply -> Id -> (Supply, Id)
mkUniqueHeapId PureHeap
h' Supply
ids' Id
x) (Id -> PureHeap -> Maybe Term
forall b a. Var b -> VarEnv a -> Maybe a
lookupVarEnv Id
x' PureHeap
h')
   where
    (Int
i,Supply
ids') = Supply -> (Int, Supply)
freshId Supply
ids
    x' :: Id
x'       = (Name Term -> Name Term) -> Id -> Id
forall a. (Name a -> Name a) -> Var a -> Var a
modifyVarName (Name Term -> Int -> Name Term
forall a. Uniquable a => a -> Int -> a
`setUnique` Int
i) Id
x