{-|
Module      : Idris.Core.WHNF
Description : Reduction to Weak Head Normal Form

License     : BSD3
Maintainer  : The Idris Community.
-}

{-# LANGUAGE FlexibleContexts, PatternGuards #-}
{-# OPTIONS_GHC -fwarn-incomplete-patterns #-}
module Idris.Core.WHNF(whnf, whnfArgs, WEnv) where

import Idris.Core.CaseTree
import Idris.Core.Evaluate hiding (quote)
import Idris.Core.TT

-- | A stack entry consists of a term and the environment it is to be
-- evaluated in (i.e. it's a thunk)
type StackEntry = (Term, WEnv)

data WEnv = WEnv Int -- number of free variables
                 [(Term, WEnv)]
  deriving Int -> WEnv -> ShowS
[WEnv] -> ShowS
WEnv -> String
(Int -> WEnv -> ShowS)
-> (WEnv -> String) -> ([WEnv] -> ShowS) -> Show WEnv
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> WEnv -> ShowS
showsPrec :: Int -> WEnv -> ShowS
$cshow :: WEnv -> String
show :: WEnv -> String
$cshowList :: [WEnv] -> ShowS
showList :: [WEnv] -> ShowS
Show

type Stack = [StackEntry]

-- | A WHNF is a top level term evaluated in the empty environment. It is
-- always headed by either an irreducible expression, i.e. a constructor,
-- a lambda, a constant, or a postulate
--
-- Every 'Term' or 'Type' in this structure is associated with the
-- environment it was encountered in, so that when we quote back to a term
-- we get the substitutions right.

data WHNF = WDCon Int Int Bool Name (Term, WEnv) -- ^ data constructor
          | WTCon Int Int Name (Type, WEnv) -- ^ type constructor
          | WPRef Name (Term, WEnv) -- ^irreducible global (e.g. a postulate)
          | WV Int
          | WBind Name (Binder (Term, WEnv)) (Term, WEnv)
          | WApp WHNF (Term, WEnv)
          | WConstant Const
          | WProj WHNF Int
          | WType UExp
          | WUType Universe
          | WErased
          | WImpossible

-- NOTE: These aren't yet ready to be used in practice - there's still a
-- bug or two in the handling of de Bruijn indices.

-- | Reduce a term to weak head normal form.
whnf :: Context -> Env -> Term -> Term
-- whnf ctxt env tm = let res = whnf' ctxt env tm in
--                        trace (show tm ++ "\n==>\n" ++ show res ++ "\n") res
whnf :: Context -> Env -> Term -> Term
whnf Context
ctxt Env
env Term
tm =
   Context -> Env -> Term -> Term
inlineSmall Context
ctxt Env
env (Term -> Term) -> Term -> Term
forall a b. (a -> b) -> a -> b
$ -- reduce small things in body. This is primarily
                          -- to get rid of any noisy "assert_smaller/assert_total"
                          -- and evaluate any simple operators, which makes things
                          -- easier to read.
     Context -> Env -> Term -> Term
whnf' Context
ctxt Env
env Term
tm
whnf' :: Context -> Env -> Term -> Term
whnf' Context
ctxt Env
env Term
tm =
     WHNF -> Term
quote (Context -> Env -> Term -> WHNF
do_whnf Context
ctxt (((Name, RigCount, Binder Term) -> (Name, RigCount, Binder Term))
-> Env -> Env
forall a b. (a -> b) -> [a] -> [b]
map (Name, RigCount, Binder Term) -> (Name, RigCount, Binder Term)
finalEntry Env
env) (Term -> Term
forall n. Eq n => TT n -> TT n
finalise Term
tm))

-- | Reduce a type so that all arguments are expanded
whnfArgs :: Context -> Env -> Term -> Term
whnfArgs :: Context -> Env -> Term -> Term
whnfArgs Context
ctxt Env
env Term
tm = Context -> Env -> Term -> Term
inlineSmall Context
ctxt Env
env (Term -> Term) -> Term -> Term
forall a b. (a -> b) -> a -> b
$ Term -> Term
forall n. Eq n => TT n -> TT n
finalise (Context -> Env -> Term -> Term
whnfArgs' Context
ctxt Env
env Term
tm)
whnfArgs' :: Context -> Env -> Term -> Term
whnfArgs' Context
ctxt Env
env Term
tm
    = case Context -> Env -> Term -> Term
whnf' Context
ctxt Env
env Term
tm of
           -- The assumption is that de Bruijn indices refer to local things
           -- (so not in the external environment) so we need to instantiate
           -- the name
           Bind Name
n b :: Binder Term
b@(Pi RigCount
rig Maybe ImplicitInfo
_ Term
ty Term
_) Term
sc ->
                    Name -> Binder Term -> Term -> Term
forall n. n -> Binder (TT n) -> TT n -> TT n
Bind Name
n Binder Term
b (Context -> Env -> Term -> Term
whnfArgs' Context
ctxt ((Name
n, RigCount
rig, Binder Term
b)(Name, RigCount, Binder Term) -> Env -> Env
forall a. a -> [a] -> [a]
:Env
env)
                             (Name -> Term -> Term -> Term
forall n. Eq n => n -> TT n -> TT n -> TT n
subst Name
n (NameType -> Name -> Term -> Term
forall n. NameType -> n -> TT n -> TT n
P NameType
Bound Name
n Term
ty) Term
sc))
           Term
res -> Term
tm

finalEntry :: (Name, RigCount, Binder (TT Name)) -> (Name, RigCount, Binder (TT Name))
finalEntry :: (Name, RigCount, Binder Term) -> (Name, RigCount, Binder Term)
finalEntry (Name
n, RigCount
r, Binder Term
b) = (Name
n, RigCount
r, (Term -> Term) -> Binder Term -> Binder Term
forall a b. (a -> b) -> Binder a -> Binder b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Term -> Term
forall n. Eq n => TT n -> TT n
finalise Binder Term
b)

do_whnf :: Context -> Env -> Term -> WHNF
do_whnf :: Context -> Env -> Term -> WHNF
do_whnf Context
ctxt Env
genv Term
tm = WEnv -> [(Term, WEnv)] -> Term -> WHNF
eval (Int -> [(Term, WEnv)] -> WEnv
WEnv Int
0 []) [] Term
tm
  where
    eval :: WEnv -> Stack -> Term -> WHNF
    eval :: WEnv -> [(Term, WEnv)] -> Term -> WHNF
eval wenv :: WEnv
wenv@(WEnv Int
d [(Term, WEnv)]
env) [(Term, WEnv)]
stk (V Int
i)
         | Int
i Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< [(Term, WEnv)] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [(Term, WEnv)]
env = let (Term
tm, WEnv
env') = [(Term, WEnv)]
env [(Term, WEnv)] -> Int -> (Term, WEnv)
forall a. HasCallStack => [a] -> Int -> a
!! Int
i in
                                WEnv -> [(Term, WEnv)] -> Term -> WHNF
eval WEnv
env' [(Term, WEnv)]
stk Term
tm
         | Bool
otherwise = Int -> WHNF
WV Int
i
    eval wenv :: WEnv
wenv@(WEnv Int
d [(Term, WEnv)]
env) [(Term, WEnv)]
stk (Bind Name
n (Let RigCount
c Term
t Term
v) Term
sc)
         = WEnv -> [(Term, WEnv)] -> Term -> WHNF
eval (Int -> [(Term, WEnv)] -> WEnv
WEnv Int
d ((Term
v, WEnv
wenv) (Term, WEnv) -> [(Term, WEnv)] -> [(Term, WEnv)]
forall a. a -> [a] -> [a]
: [(Term, WEnv)]
env)) [(Term, WEnv)]
stk Term
sc
    eval (WEnv Int
d [(Term, WEnv)]
env) ((Term
tm, WEnv
tenv) : [(Term, WEnv)]
stk) (Bind Name
n b :: Binder Term
b@(Lam RigCount
_ Term
_) Term
sc)
         = WEnv -> [(Term, WEnv)] -> Term -> WHNF
eval (Int -> [(Term, WEnv)] -> WEnv
WEnv Int
d ((Term
tm, WEnv
tenv) (Term, WEnv) -> [(Term, WEnv)] -> [(Term, WEnv)]
forall a. a -> [a] -> [a]
: [(Term, WEnv)]
env)) [(Term, WEnv)]
stk Term
sc
    eval wenv :: WEnv
wenv@(WEnv Int
d [(Term, WEnv)]
env) [(Term, WEnv)]
stk (Bind Name
n Binder Term
b Term
sc) -- stk must be empty if well typed
         =let n' :: Name
n' = Name -> [Name] -> Name
uniqueName Name
n (((Name, RigCount, Binder Term) -> Name) -> Env -> [Name]
forall a b. (a -> b) -> [a] -> [b]
map (Name, RigCount, Binder Term) -> Name
forall {a} {b} {c}. (a, b, c) -> a
fstEnv Env
genv) in
              Name -> Binder (Term, WEnv) -> (Term, WEnv) -> WHNF
WBind Name
n' ((Term -> (Term, WEnv)) -> Binder Term -> Binder (Term, WEnv)
forall a b. (a -> b) -> Binder a -> Binder b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (\Term
t -> (Term
t, WEnv
wenv)) Binder Term
b) (Term
sc, Int -> [(Term, WEnv)] -> WEnv
WEnv (Int
d Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1) [(Term, WEnv)]
env)

    eval WEnv
env [(Term, WEnv)]
stk (P NameType
nt Name
n Term
ty)
         | Just (Let RigCount
c Term
t Term
v) <- Name -> Env -> Maybe (Binder Term)
forall n. Eq n => n -> EnvTT n -> Maybe (Binder (TT n))
lookupBinder Name
n Env
genv = WEnv -> [(Term, WEnv)] -> Term -> WHNF
eval WEnv
env [(Term, WEnv)]
stk Term
v
    eval WEnv
env [(Term, WEnv)]
stk (P NameType
nt Name
n Term
ty) = WEnv -> NameType -> Name -> Term -> [(Term, WEnv)] -> WHNF
apply WEnv
env NameType
nt Name
n Term
ty [(Term, WEnv)]
stk
    eval WEnv
env [(Term, WEnv)]
stk (App AppStatus Name
_ Term
f Term
a) = WEnv -> [(Term, WEnv)] -> Term -> WHNF
eval WEnv
env ((Term
a, WEnv
env) (Term, WEnv) -> [(Term, WEnv)] -> [(Term, WEnv)]
forall a. a -> [a] -> [a]
: [(Term, WEnv)]
stk) Term
f
    eval WEnv
env [(Term, WEnv)]
stk (Constant Const
c) = WHNF -> [(Term, WEnv)] -> WHNF
unload (Const -> WHNF
WConstant Const
c) [(Term, WEnv)]
stk

    -- Should never happen in compile time code (for now...)
    eval WEnv
env [(Term, WEnv)]
stk (Proj Term
tm Int
i) = WHNF -> [(Term, WEnv)] -> WHNF
unload (WHNF -> Int -> WHNF
WProj (WEnv -> [(Term, WEnv)] -> Term -> WHNF
eval WEnv
env [] Term
tm) Int
i) [(Term, WEnv)]
stk

    eval WEnv
env [(Term, WEnv)]
stk Term
Erased = WHNF -> [(Term, WEnv)] -> WHNF
unload WHNF
WErased [(Term, WEnv)]
stk
    eval WEnv
env [(Term, WEnv)]
stk Term
Impossible = WHNF -> [(Term, WEnv)] -> WHNF
unload WHNF
WImpossible [(Term, WEnv)]
stk
    eval WEnv
env [(Term, WEnv)]
stk (Inferred Term
tm) = WEnv -> [(Term, WEnv)] -> Term -> WHNF
eval WEnv
env [(Term, WEnv)]
stk Term
tm
    eval WEnv
env [(Term, WEnv)]
stk (TType UExp
u) = WHNF -> [(Term, WEnv)] -> WHNF
unload (UExp -> WHNF
WType UExp
u) [(Term, WEnv)]
stk
    eval WEnv
env [(Term, WEnv)]
stk (UType Universe
u) = WHNF -> [(Term, WEnv)] -> WHNF
unload (Universe -> WHNF
WUType Universe
u) [(Term, WEnv)]
stk

    apply :: WEnv -> NameType -> Name -> Type -> Stack -> WHNF
    apply :: WEnv -> NameType -> Name -> Term -> [(Term, WEnv)] -> WHNF
apply WEnv
env NameType
nt Name
n Term
ty [(Term, WEnv)]
stk
          = let wp :: WHNF
wp = case NameType
nt of
                          DCon Int
t Int
a Bool
u -> Int -> Int -> Bool -> Name -> (Term, WEnv) -> WHNF
WDCon Int
t Int
a Bool
u Name
n (Term
ty, WEnv
env)
                          TCon Int
t Int
a -> Int -> Int -> Name -> (Term, WEnv) -> WHNF
WTCon Int
t Int
a Name
n (Term
ty, WEnv
env)
                          NameType
Ref -> Name -> (Term, WEnv) -> WHNF
WPRef Name
n (Term
ty, WEnv
env)
                          NameType
_ -> Name -> (Term, WEnv) -> WHNF
WPRef Name
n (Term
ty, WEnv
env)
                        in
            if Bool -> Bool
not (Name -> Context -> Bool
tcReducible Name
n Context
ctxt)
               then WHNF -> [(Term, WEnv)] -> WHNF
unload WHNF
wp [(Term, WEnv)]
stk
               else case Name -> Bool -> Context -> Maybe (Def, Accessibility)
lookupDefAccExact Name
n Bool
False Context
ctxt of
                         Just (CaseOp CaseInfo
ci Term
_ [(Term, Bool)]
_ [Either Term (Term, Term)]
_ [([Name], Term, Term)]
_ CaseDefs
cd, Accessibility
acc)
                             | Accessibility
acc Accessibility -> Accessibility -> Bool
forall a. Eq a => a -> a -> Bool
== Accessibility
Public Bool -> Bool -> Bool
|| Accessibility
acc Accessibility -> Accessibility -> Bool
forall a. Eq a => a -> a -> Bool
== Accessibility
Hidden ->
                          let ([Name]
ns, SC
tree) = CaseDefs -> ([Name], SC)
cases_compiletime CaseDefs
cd in
                              case WEnv -> [Name] -> SC -> [(Term, WEnv)] -> Maybe WHNF
evalCase WEnv
env [Name]
ns SC
tree [(Term, WEnv)]
stk of
                                   Just WHNF
w -> WHNF
w
                                   Maybe WHNF
Nothing -> WHNF -> [(Term, WEnv)] -> WHNF
unload WHNF
wp [(Term, WEnv)]
stk
                         Just (Operator Term
_ Int
i [Value] -> Maybe Value
op, Accessibility
acc) ->
                          if Int
i Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
<= [(Term, WEnv)] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [(Term, WEnv)]
stk
                             then case WEnv
-> ([Value] -> Maybe Value)
-> [(Term, WEnv)]
-> [(Term, WEnv)]
-> Maybe WHNF
runOp WEnv
env [Value] -> Maybe Value
op (Int -> [(Term, WEnv)] -> [(Term, WEnv)]
forall a. Int -> [a] -> [a]
take Int
i [(Term, WEnv)]
stk) (Int -> [(Term, WEnv)] -> [(Term, WEnv)]
forall a. Int -> [a] -> [a]
drop Int
i [(Term, WEnv)]
stk) of
                                  Just WHNF
v -> WHNF
v
                                  Maybe WHNF
Nothing -> WHNF -> [(Term, WEnv)] -> WHNF
unload WHNF
wp [(Term, WEnv)]
stk
                             else WHNF -> [(Term, WEnv)] -> WHNF
unload WHNF
wp [(Term, WEnv)]
stk
                         Maybe (Def, Accessibility)
_ -> WHNF -> [(Term, WEnv)] -> WHNF
unload WHNF
wp [(Term, WEnv)]
stk

    unload :: WHNF -> Stack -> WHNF
    unload :: WHNF -> [(Term, WEnv)] -> WHNF
unload WHNF
f [] = WHNF
f
    unload WHNF
f ((Term, WEnv)
a : [(Term, WEnv)]
as) = WHNF -> [(Term, WEnv)] -> WHNF
unload (WHNF -> (Term, WEnv) -> WHNF
WApp WHNF
f (Term, WEnv)
a) [(Term, WEnv)]
as

    runOp :: WEnv -> ([Value] -> Maybe Value) -> Stack -> Stack -> Maybe WHNF
    runOp :: WEnv
-> ([Value] -> Maybe Value)
-> [(Term, WEnv)]
-> [(Term, WEnv)]
-> Maybe WHNF
runOp WEnv
env [Value] -> Maybe Value
op [(Term, WEnv)]
stk [(Term, WEnv)]
rest
        = do [Value]
vals <- ((Term, WEnv) -> Maybe Value) -> [(Term, WEnv)] -> Maybe [Value]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM (Term, WEnv) -> Maybe Value
tmtoValue [(Term, WEnv)]
stk
             case [Value] -> Maybe Value
op [Value]
vals of
                  Just (VConstant Const
c) -> WHNF -> Maybe WHNF
forall a. a -> Maybe a
Just (WHNF -> Maybe WHNF) -> WHNF -> Maybe WHNF
forall a b. (a -> b) -> a -> b
$ WHNF -> [(Term, WEnv)] -> WHNF
unload (Const -> WHNF
WConstant Const
c) [(Term, WEnv)]
rest
                  -- Operators run on values, so we have to convert back
                  -- and forth. This is pretty ugly, but operators that
                  -- aren't run on constants are themselves pretty ugly
                  -- (it's prim__believe_me and prim__syntacticEq, for
                  -- example) so let's not worry too much...
                  -- We will need to deal with believe_me before dropping this
                  -- into the type checker, though.
                  Just Value
val -> WHNF -> Maybe WHNF
forall a. a -> Maybe a
Just (WHNF -> Maybe WHNF) -> WHNF -> Maybe WHNF
forall a b. (a -> b) -> a -> b
$ WEnv -> [(Term, WEnv)] -> Term -> WHNF
eval WEnv
env [(Term, WEnv)]
rest (Value -> Term
quoteTerm Value
val)
                  Maybe Value
_ -> Maybe WHNF
forall a. Maybe a
Nothing

    tmtoValue :: (Term, WEnv) -> Maybe Value
    tmtoValue :: (Term, WEnv) -> Maybe Value
tmtoValue (Term
tm, WEnv
tenv)
        = case WEnv -> [(Term, WEnv)] -> Term -> WHNF
eval WEnv
tenv [] Term
tm of
               WConstant Const
c -> Value -> Maybe Value
forall a. a -> Maybe a
Just (Const -> Value
VConstant Const
c)
               WHNF
_ -> let tm' :: Term
tm' = WEnv -> Term -> Term
quoteEnv WEnv
tenv Term
tm in
                        Value -> Maybe Value
forall a. a -> Maybe a
Just (Context -> Env -> Term -> Value
toValue Context
ctxt [] Term
tm')

    evalCase :: WEnv -> [Name] -> SC -> Stack -> Maybe WHNF
    evalCase :: WEnv -> [Name] -> SC -> [(Term, WEnv)] -> Maybe WHNF
evalCase wenv :: WEnv
wenv@(WEnv Int
d [(Term, WEnv)]
env) [Name]
ns SC
tree [(Term, WEnv)]
args
        | [Name] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Name]
ns Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> [(Term, WEnv)] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [(Term, WEnv)]
args = Maybe WHNF
forall a. Maybe a
Nothing
        | Bool
otherwise = let args' :: [(Term, WEnv)]
args' = Int -> [(Term, WEnv)] -> [(Term, WEnv)]
forall a. Int -> [a] -> [a]
take ([Name] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Name]
ns) [(Term, WEnv)]
args
                          rest :: [(Term, WEnv)]
rest = Int -> [(Term, WEnv)] -> [(Term, WEnv)]
forall a. Int -> [a] -> [a]
drop ([Name] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Name]
ns) [(Term, WEnv)]
args in
                          do (Term
tm, [(Name, (Term, WEnv))]
amap) <- WEnv
-> [(Name, (Term, WEnv))]
-> SC
-> Maybe (Term, [(Name, (Term, WEnv))])
evalTree WEnv
wenv ([Name] -> [(Term, WEnv)] -> [(Name, (Term, WEnv))]
forall a b. [a] -> [b] -> [(a, b)]
zip [Name]
ns [(Term, WEnv)]
args') SC
tree
                             let wtm :: Term
wtm = [Name] -> Term -> Term
forall n. Eq n => [n] -> TT n -> TT n
pToVs (((Name, (Term, WEnv)) -> Name) -> [(Name, (Term, WEnv))] -> [Name]
forall a b. (a -> b) -> [a] -> [b]
map (Name, (Term, WEnv)) -> Name
forall a b. (a, b) -> a
fst [(Name, (Term, WEnv))]
amap) Term
tm
                             WHNF -> Maybe WHNF
forall a. a -> Maybe a
Just (WHNF -> Maybe WHNF) -> WHNF -> Maybe WHNF
forall a b. (a -> b) -> a -> b
$ WEnv -> [(Term, WEnv)] -> Term -> WHNF
eval (Int -> [(Term, WEnv)] -> WEnv
WEnv Int
d (((Name, (Term, WEnv)) -> (Term, WEnv))
-> [(Name, (Term, WEnv))] -> [(Term, WEnv)]
forall a b. (a -> b) -> [a] -> [b]
map (Name, (Term, WEnv)) -> (Term, WEnv)
forall a b. (a, b) -> b
snd [(Name, (Term, WEnv))]
amap)) [(Term, WEnv)]
rest Term
wtm

    evalTree :: WEnv -> [(Name, (Term, WEnv))] -> SC ->
                Maybe (Term, [(Name, (Term, WEnv))])
    evalTree :: WEnv
-> [(Name, (Term, WEnv))]
-> SC
-> Maybe (Term, [(Name, (Term, WEnv))])
evalTree WEnv
env [(Name, (Term, WEnv))]
amap (STerm Term
tm) = (Term, [(Name, (Term, WEnv))])
-> Maybe (Term, [(Name, (Term, WEnv))])
forall a. a -> Maybe a
Just (Term
tm, [(Name, (Term, WEnv))]
amap)
    evalTree WEnv
env [(Name, (Term, WEnv))]
amap (Case CaseType
_ Name
n [CaseAlt' Term]
alts)
        = case Name -> [(Name, (Term, WEnv))] -> Maybe (Term, WEnv)
forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup Name
n [(Name, (Term, WEnv))]
amap of
            Just (Term
tm, WEnv
tenv) -> WEnv
-> [(Name, (Term, WEnv))]
-> (WHNF, [(Term, WEnv)])
-> [CaseAlt' Term]
-> Maybe (Term, [(Name, (Term, WEnv))])
findAlt WEnv
env [(Name, (Term, WEnv))]
amap
                                   (WHNF -> [(Term, WEnv)] -> (WHNF, [(Term, WEnv)])
deconstruct (WEnv -> [(Term, WEnv)] -> Term -> WHNF
eval WEnv
tenv [] Term
tm) []) [CaseAlt' Term]
alts
            Maybe (Term, WEnv)
_ -> Maybe (Term, [(Name, (Term, WEnv))])
forall a. Maybe a
Nothing
    evalTree WEnv
_ [(Name, (Term, WEnv))]
_ SC
_ = Maybe (Term, [(Name, (Term, WEnv))])
forall a. Maybe a
Nothing

    deconstruct :: WHNF -> Stack -> (WHNF, Stack)
    deconstruct :: WHNF -> [(Term, WEnv)] -> (WHNF, [(Term, WEnv)])
deconstruct (WApp WHNF
f (Term, WEnv)
arg) [(Term, WEnv)]
stk = WHNF -> [(Term, WEnv)] -> (WHNF, [(Term, WEnv)])
deconstruct WHNF
f ((Term, WEnv)
arg (Term, WEnv) -> [(Term, WEnv)] -> [(Term, WEnv)]
forall a. a -> [a] -> [a]
: [(Term, WEnv)]
stk)
    deconstruct WHNF
t [(Term, WEnv)]
stk = (WHNF
t, [(Term, WEnv)]
stk)

    findAlt :: WEnv -> [(Name, (Term, WEnv))] -> (WHNF, Stack) ->
               [CaseAlt] ->
               Maybe (Term, [(Name, (Term, WEnv))])
    findAlt :: WEnv
-> [(Name, (Term, WEnv))]
-> (WHNF, [(Term, WEnv)])
-> [CaseAlt' Term]
-> Maybe (Term, [(Name, (Term, WEnv))])
findAlt WEnv
env [(Name, (Term, WEnv))]
amap (WDCon Int
tag Int
_ Bool
_ Name
_ (Term, WEnv)
_, [(Term, WEnv)]
args) [CaseAlt' Term]
alts
        | Just ([Name]
ns, SC
sc) <- Int -> [CaseAlt' Term] -> Maybe ([Name], SC)
findTag Int
tag [CaseAlt' Term]
alts
              = let amap' :: [(Name, (Term, WEnv))]
amap' = [(Name, (Term, WEnv))]
-> [(Name, (Term, WEnv))] -> [(Name, (Term, WEnv))]
forall {a} {b}. Eq a => [(a, b)] -> [(a, b)] -> [(a, b)]
updateAmap ([Name] -> [(Term, WEnv)] -> [(Name, (Term, WEnv))]
forall a b. [a] -> [b] -> [(a, b)]
zip [Name]
ns [(Term, WEnv)]
args) [(Name, (Term, WEnv))]
amap in
                    WEnv
-> [(Name, (Term, WEnv))]
-> SC
-> Maybe (Term, [(Name, (Term, WEnv))])
evalTree WEnv
env [(Name, (Term, WEnv))]
amap' SC
sc
        | Just SC
sc <- [CaseAlt' Term] -> Maybe SC
findDefault [CaseAlt' Term]
alts
              = WEnv
-> [(Name, (Term, WEnv))]
-> SC
-> Maybe (Term, [(Name, (Term, WEnv))])
evalTree WEnv
env [(Name, (Term, WEnv))]
amap SC
sc
    findAlt WEnv
env [(Name, (Term, WEnv))]
amap (WConstant Const
c, []) [CaseAlt' Term]
alts
        | Just SC
sc <- Const -> [CaseAlt' Term] -> Maybe SC
forall {t}. Const -> [CaseAlt' t] -> Maybe (SC' t)
findConst Const
c [CaseAlt' Term]
alts
              = WEnv
-> [(Name, (Term, WEnv))]
-> SC
-> Maybe (Term, [(Name, (Term, WEnv))])
evalTree WEnv
env [(Name, (Term, WEnv))]
amap SC
sc
        | Just SC
sc <- [CaseAlt' Term] -> Maybe SC
findDefault [CaseAlt' Term]
alts
              = WEnv
-> [(Name, (Term, WEnv))]
-> SC
-> Maybe (Term, [(Name, (Term, WEnv))])
evalTree WEnv
env [(Name, (Term, WEnv))]
amap SC
sc
    findAlt WEnv
_ [(Name, (Term, WEnv))]
_ (WHNF, [(Term, WEnv)])
_ [CaseAlt' Term]
_ = Maybe (Term, [(Name, (Term, WEnv))])
forall a. Maybe a
Nothing

    findTag :: Int -> [CaseAlt] -> Maybe ([Name], SC)
    findTag :: Int -> [CaseAlt' Term] -> Maybe ([Name], SC)
findTag Int
i [] = Maybe ([Name], SC)
forall a. Maybe a
Nothing
    findTag Int
i (ConCase Name
n Int
j [Name]
ns SC
sc : [CaseAlt' Term]
xs) | Int
i Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
j = ([Name], SC) -> Maybe ([Name], SC)
forall a. a -> Maybe a
Just ([Name]
ns, SC
sc)
    findTag Int
i (CaseAlt' Term
_ : [CaseAlt' Term]
xs) = Int -> [CaseAlt' Term] -> Maybe ([Name], SC)
findTag Int
i [CaseAlt' Term]
xs

    findDefault :: [CaseAlt] -> Maybe SC
    findDefault :: [CaseAlt' Term] -> Maybe SC
findDefault [] = Maybe SC
forall a. Maybe a
Nothing
    findDefault (DefaultCase SC
sc : [CaseAlt' Term]
xs) = SC -> Maybe SC
forall a. a -> Maybe a
Just SC
sc
    findDefault (CaseAlt' Term
_ : [CaseAlt' Term]
xs) = [CaseAlt' Term] -> Maybe SC
findDefault [CaseAlt' Term]
xs

    findConst :: Const -> [CaseAlt' t] -> Maybe (SC' t)
findConst Const
c [] = Maybe (SC' t)
forall a. Maybe a
Nothing
    findConst Const
c (ConstCase Const
c' SC' t
v : [CaseAlt' t]
xs) | Const
c Const -> Const -> Bool
forall a. Eq a => a -> a -> Bool
== Const
c' = SC' t -> Maybe (SC' t)
forall a. a -> Maybe a
Just SC' t
v
    findConst (AType (ATInt IntTy
ITNative)) (ConCase Name
n Int
1 [] SC' t
v : [CaseAlt' t]
xs) = SC' t -> Maybe (SC' t)
forall a. a -> Maybe a
Just SC' t
v
    findConst (AType ArithTy
ATFloat) (ConCase Name
n Int
2 [] SC' t
v : [CaseAlt' t]
xs) = SC' t -> Maybe (SC' t)
forall a. a -> Maybe a
Just SC' t
v
    findConst (AType (ATInt IntTy
ITChar))  (ConCase Name
n Int
3 [] SC' t
v : [CaseAlt' t]
xs) = SC' t -> Maybe (SC' t)
forall a. a -> Maybe a
Just SC' t
v
    findConst Const
StrType (ConCase Name
n Int
4 [] SC' t
v : [CaseAlt' t]
xs) = SC' t -> Maybe (SC' t)
forall a. a -> Maybe a
Just SC' t
v
    findConst (AType (ATInt IntTy
ITBig)) (ConCase Name
n Int
6 [] SC' t
v : [CaseAlt' t]
xs) = SC' t -> Maybe (SC' t)
forall a. a -> Maybe a
Just SC' t
v
    findConst (AType (ATInt (ITFixed NativeTy
ity))) (ConCase Name
n Int
tag [] SC' t
v : [CaseAlt' t]
xs)
        | Int
tag Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
7 Int -> Int -> Int
forall a. Num a => a -> a -> a
+ NativeTy -> Int
forall a. Enum a => a -> Int
fromEnum NativeTy
ity = SC' t -> Maybe (SC' t)
forall a. a -> Maybe a
Just SC' t
v
    findConst Const
c (CaseAlt' t
_ : [CaseAlt' t]
xs) = Const -> [CaseAlt' t] -> Maybe (SC' t)
findConst Const
c [CaseAlt' t]
xs

    updateAmap :: [(a, b)] -> [(a, b)] -> [(a, b)]
updateAmap [(a, b)]
newm [(a, b)]
amap
       = [(a, b)]
newm [(a, b)] -> [(a, b)] -> [(a, b)]
forall a. [a] -> [a] -> [a]
++ ((a, b) -> Bool) -> [(a, b)] -> [(a, b)]
forall a. (a -> Bool) -> [a] -> [a]
filter (\ (a
x, b
_) -> Bool -> Bool
not (a -> [a] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
elem a
x (((a, b) -> a) -> [(a, b)] -> [a]
forall a b. (a -> b) -> [a] -> [b]
map (a, b) -> a
forall a b. (a, b) -> a
fst [(a, b)]
newm))) [(a, b)]
amap

quote :: WHNF -> Term
quote :: WHNF -> Term
quote (WDCon Int
t Int
a Bool
u Name
n (Term
ty, WEnv
env)) = NameType -> Name -> Term -> Term
forall n. NameType -> n -> TT n -> TT n
P (Int -> Int -> Bool -> NameType
DCon Int
t Int
a Bool
u) Name
n (WEnv -> Term -> Term
quoteEnv WEnv
env Term
ty)
quote (WTCon Int
t Int
a Name
n (Term
ty, WEnv
env)) = NameType -> Name -> Term -> Term
forall n. NameType -> n -> TT n -> TT n
P (Int -> Int -> NameType
TCon Int
t Int
a) Name
n (WEnv -> Term -> Term
quoteEnv WEnv
env Term
ty)
quote (WPRef Name
n (Term
ty, WEnv
env)) = NameType -> Name -> Term -> Term
forall n. NameType -> n -> TT n -> TT n
P NameType
Ref Name
n (WEnv -> Term -> Term
quoteEnv WEnv
env Term
ty)
quote (WV Int
i) = Int -> Term
forall n. Int -> TT n
V Int
i
quote (WBind Name
n Binder (Term, WEnv)
b (Term
sc, WEnv
env)) = Name -> Binder Term -> Term -> Term
forall n. n -> Binder (TT n) -> TT n -> TT n
Bind Name
n (((Term, WEnv) -> Term) -> Binder (Term, WEnv) -> Binder Term
forall a b. (a -> b) -> Binder a -> Binder b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (\ (Term
t, WEnv
env) -> WEnv -> Term -> Term
quoteEnv WEnv
env Term
t) Binder (Term, WEnv)
b)
                                     (WEnv -> Term -> Term
quoteEnv WEnv
env Term
sc)
quote (WApp WHNF
f (Term
a, WEnv
env)) = AppStatus Name -> Term -> Term -> Term
forall n. AppStatus n -> TT n -> TT n -> TT n
App AppStatus Name
forall n. AppStatus n
Complete (WHNF -> Term
quote WHNF
f) (WEnv -> Term -> Term
quoteEnv WEnv
env Term
a)
quote (WConstant Const
c) = Const -> Term
forall n. Const -> TT n
Constant Const
c
quote (WProj WHNF
t Int
i) = Term -> Int -> Term
forall n. TT n -> Int -> TT n
Proj (WHNF -> Term
quote WHNF
t) Int
i
quote (WType UExp
u) = UExp -> Term
forall n. UExp -> TT n
TType UExp
u
quote (WUType Universe
u) = Universe -> Term
forall n. Universe -> TT n
UType Universe
u
quote WHNF
WErased = Term
forall n. TT n
Erased
quote WHNF
WImpossible = Term
forall n. TT n
Impossible

quoteEnv :: WEnv -> Term -> Term
quoteEnv :: WEnv -> Term -> Term
quoteEnv (WEnv Int
d [(Term, WEnv)]
ws) Term
tm = Int -> [(Term, WEnv)] -> Term -> Term
qe' Int
d [(Term, WEnv)]
ws Term
tm
  where
    -- d is number of free variables in the external environment
    -- (all bound in the scope of 'ws')
    qe' :: Int -> [(Term, WEnv)] -> Term -> Term
qe' Int
d [(Term, WEnv)]
ts (V Int
i)
        | (Int
i Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
d) Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< [(Term, WEnv)] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [(Term, WEnv)]
ts Bool -> Bool -> Bool
&& (Int
i Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
d) Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= Int
0
              = let (Term
tm, WEnv
env) = [(Term, WEnv)]
ts [(Term, WEnv)] -> Int -> (Term, WEnv)
forall a. HasCallStack => [a] -> Int -> a
!! (Int
i Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
d) in
                    WEnv -> Term -> Term
quoteEnv WEnv
env Term
tm
        | Bool
otherwise = Int -> Term
forall n. Int -> TT n
V Int
i
    qe' Int
d [(Term, WEnv)]
ts (Bind Name
n Binder Term
b Term
sc)
        = Name -> Binder Term -> Term -> Term
forall n. n -> Binder (TT n) -> TT n -> TT n
Bind Name
n ((Term -> Term) -> Binder Term -> Binder Term
forall a b. (a -> b) -> Binder a -> Binder b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Int -> [(Term, WEnv)] -> Term -> Term
qe' Int
d [(Term, WEnv)]
ts) Binder Term
b) (Int -> [(Term, WEnv)] -> Term -> Term
qe' (Int
d Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1) [(Term, WEnv)]
ts Term
sc)
    qe' Int
d [(Term, WEnv)]
ts (App AppStatus Name
c Term
f Term
a)
        = AppStatus Name -> Term -> Term -> Term
forall n. AppStatus n -> TT n -> TT n -> TT n
App AppStatus Name
c (Int -> [(Term, WEnv)] -> Term -> Term
qe' Int
d [(Term, WEnv)]
ts Term
f) (Int -> [(Term, WEnv)] -> Term -> Term
qe' Int
d [(Term, WEnv)]
ts Term
a)
    qe' Int
d [(Term, WEnv)]
ts (P NameType
nt Name
n Term
ty) = NameType -> Name -> Term -> Term
forall n. NameType -> n -> TT n -> TT n
P NameType
nt Name
n (Int -> [(Term, WEnv)] -> Term -> Term
qe' Int
d [(Term, WEnv)]
ts Term
ty)
    qe' Int
d [(Term, WEnv)]
ts (Proj Term
tm Int
i) = Term -> Int -> Term
forall n. TT n -> Int -> TT n
Proj (Int -> [(Term, WEnv)] -> Term -> Term
qe' Int
d [(Term, WEnv)]
ts Term
tm) Int
i
    qe' Int
d [(Term, WEnv)]
ts Term
tm = Term
tm