{-# 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
type StackEntry = (Term, WEnv)
data WEnv = WEnv Int
[(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]
data WHNF = WDCon Int Int Bool Name (Term, WEnv)
| WTCon Int Int Name (Type, WEnv)
| WPRef Name (Term, WEnv)
| WV Int
| WBind Name (Binder (Term, WEnv)) (Term, WEnv)
| WApp WHNF (Term, WEnv)
| WConstant Const
| WProj WHNF Int
| WType UExp
| WUType Universe
| WErased
| WImpossible
whnf :: Context -> Env -> Term -> Term
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
$
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))
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
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)
=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
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
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
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