3612623 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

More WHNF edits

3612623Edwin Brady10 years ago

src/Idris/Core/WHNF.hs+11−4

compare with master

unifiedsplit

@@ -20,6 +20,7 @@ import Debug.Trace

20-- | A stack entry consists of a term and the environment it is to be

21-- evaluated in (i.e. it's a thunk)

22type StackEntry = (Term, WEnv)

23+

23data WEnv = WEnv Int -- number of free variables

24data WEnv = WEnv Int -- number of free variables

24 [(Term, WEnv)]

25 [(Term, WEnv)]

25 deriving Show

26 deriving Show

@@ -47,6 +48,9 @@ data WHNF = WDCon Int Int Bool Name (Term, WEnv) -- ^ data constructor

47 | WErased

48 | WErased

48 | WImpossible

49 | WImpossible

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+

50-- | Reduce a term to weak head normal form.

54-- | Reduce a term to weak head normal form.

51whnf :: Context -> Env -> Term -> Term

55whnf :: Context -> Env -> Term -> Term

52whnf ctxt env tm =

56whnf ctxt env tm =

@@ -54,7 +58,7 @@ whnf ctxt env tm =

54 -- to get rid of any noisy "assert_smaller/assert_total"

58 -- to get rid of any noisy "assert_smaller/assert_total"

55 -- and evaluate any simple operators, which makes things

59 -- and evaluate any simple operators, which makes things

56 -- easier to read.

60 -- easier to read.

57− quote (do_whnf ctxt (map finalEntry env) tm)

61+ quote (do_whnf ctxt (map finalEntry env) (finalise tm))

59-- | Reduce a type so that all arguments are expanded, and all argument types

63-- | Reduce a type so that all arguments are expanded, and all argument types

60-- are in weak head normal form

64-- are in weak head normal form

@@ -227,10 +231,13 @@ quote WImpossible = Impossible

227quoteEnv :: WEnv -> Term -> Term

231quoteEnv :: WEnv -> Term -> Term

228quoteEnv (WEnv d ws) tm = qe' d ws tm

232quoteEnv (WEnv d ws) tm = qe' d ws tm

229 where

233 where

234+ -- d is number of free variables in the external environment

235+ -- (all bound in the scope of 'ws')

230 qe' d ts (V i)

236 qe' d ts (V i)

231− | i < d = V i

237+ | (i - d) < length ts && (i - d) >= 0

232− | otherwise = let (tm, env) = ts !! (i - d) in

238+ = let (tm, env) = ts !! (i - d) in

233− quoteEnv env tm

239+ quoteEnv env tm

240+ | otherwise = V i

234 qe' d ts (Bind n b sc)

241 qe' d ts (Bind n b sc)

235 = Bind n (fmap (qe' d ts) b) (qe' (d + 1) ts sc)

242 = Bind n (fmap (qe' d ts) b) (qe' (d + 1) ts sc)

236 qe' d ts (App c f a)

243 qe' d ts (App c f a)

src/Idris/Elab/Term.hs+6−4

@@ -18,7 +18,7 @@ import Idris.Core.ProofTerm (getProofTerm)

18import Idris.Core.TT

19import Idris.Core.Typecheck (check, converts, isType, recheck)

20import Idris.Core.Unify

21−import Idris.Core.WHNF (whnf)

21+import Idris.Core.WHNF (whnf,whnfArgs)

22import Idris.Coverage (genClauses, recoverableCoverage, validCoverageCase)

23import Idris.Delaborate

24import Idris.DSL

@@ -498,11 +498,13 @@ elab ist info emode opts fn tm

498 showHd x = getNameFrom (sMN 0 "_") -- We probably should do something better than this here

499

500 doPrune as =

501− do compute

501+ do compute -- to get 'Delayed' if it's there

502 ty <- goal

503− let (tc, _) = unApply (unDelay ty)

503+ ctxt <- get_context

504 env <- get_env

505+ let ty' = unDelay ty

506+ let (tc, _) = unApply ty'

505− return $ pruneByType env tc (unDelay ty) ist as

507+ return $ pruneByType env tc ty' ist as

506

508

507 unDelay t | (P _ (UN l) _, [_, arg]) <- unApply t,

509 unDelay t | (P _ (UN l) _, [_, arg]) <- unApply t,

508 l == txt "Delayed" = unDelay arg

510 l == txt "Delayed" = unDelay arg