@@ -20,6 +20,7 @@ import Debug.Trace
2020-- | A stack entry consists of a term and the environment it is to be
2121-- evaluated in (i.e. it's a thunk)
2222type StackEntry = (Term, WEnv)
23+
2324data WEnv = WEnv Int -- number of free variables
2425 [(Term, WEnv)]
2526 deriving Show
@@ -47,6 +48,9 @@ data WHNF = WDCon Int Int Bool Name (Term, WEnv) -- ^ data constructor
4748 | WErased
4849 | WImpossible
4950
51+-- NOTE: These aren't yet ready to be used in practice - there's still a
52+-- bug or two in the handling of de Bruijn indices.
53+
5054-- | Reduce a term to weak head normal form.
5155whnf :: Context -> Env -> Term -> Term
5256whnf ctxt env tm =
@@ -54,7 +58,7 @@ whnf ctxt env tm =
5458 -- to get rid of any noisy "assert_smaller/assert_total"
5559 -- and evaluate any simple operators, which makes things
5660 -- easier to read.
57− quote (do_whnf ctxt (map finalEntry env) tm)
61+ quote (do_whnf ctxt (map finalEntry env) (finalise tm))
5862
5963-- | Reduce a type so that all arguments are expanded, and all argument types
6064-- are in weak head normal form
@@ -227,10 +231,13 @@ quote WImpossible = Impossible
227231quoteEnv :: WEnv -> Term -> Term
228232quoteEnv (WEnv d ws) tm = qe' d ws tm
229233 where
234+ -- d is number of free variables in the external environment
235+ -- (all bound in the scope of 'ws')
230236 qe' d ts (V i)
231− | i < d = V i
232− | otherwise = let (tm, env) = ts !! (i - d) in
233− quoteEnv env tm
237+ | (i - d) < length ts && (i - d) >= 0
238+ = let (tm, env) = ts !! (i - d) in
239+ quoteEnv env tm
240+ | otherwise = V i
234241 qe' d ts (Bind n b sc)
235242 = Bind n (fmap (qe' d ts) b) (qe' (d + 1) ts sc)
236243 qe' d ts (App c f a)