e6d48b6 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Take care with 'let' in specialiser - avoid duplicating a redex

Let now only reduces if the binding appears at most once in scope during specialisation

commite6d48b62eae092116866fdf7d719e13306e18d42 authorEdwin Brady <ecb10@st-andrews.ac.uk> dateWed 5 Jun 2013, 15:41 (13 years ago) parent61c25d1

5 files changed+42−20

compare with master

unifiedsplit

src/Core/Evaluate.hs+27−16 src/Core/TT.hs+13−1 src/IRTS/Compiler.hs+1−1 src/Idris/REPL.hs+1−1 test/test008/test008.idr−1

src/Core/Evaluate.hs+27−16

@@ -19,20 +19,22 @@ import Data.Binary hiding (get, put)

1919import Core.TT

2020import Core.CaseTree

2121

22−data EvalState = ES { limited :: [(Name, Int)] }

22+data EvalState = ES { limited :: [(Name, Int)],

23+ nexthole :: Int }

2324

2425type Eval a = State EvalState a

2526

2627data EvalOpt = Spec | HNF | Simplify Bool | AtREPL

2728 deriving (Show, Eq)

2829

29−initEval = ES []

30+initEval = ES [] 0

3031

3132-- VALUES (as HOAS) ---------------------------------------------------------

3233-- | A HOAS representation of values

3334data Value = VP NameType Name Value

3435 | VV Int

3536 | VBind Name (Binder Value) (Value -> Eval Value)

37+ | VBLet Int Name Value Value Value

3638 | VApp Value Value

3739 | VType UExp

3840 | VErased

@@ -166,20 +168,24 @@ eval traceon ctxt ntimes genv tm opts = ev ntimes [] True [] tm where

166168 (Just v, _) -> return v

167169 _ -> liftM (VP Ref n) (ev ntimes stk top env ty)

168170 ev ntimes stk top env (P nt n ty) = liftM (VP nt n) (ev ntimes stk top env ty)

169− ev ntimes stk top env (V i) | i < length env = return $ env !! i

171+ ev ntimes stk top env (V i)

172+ | i < length env && i >= 0 = return $ env !! i

170173 | otherwise = return $ VV i

171174 ev ntimes stk top env (Bind n (Let t v) sc)

172−-- | not simpl || vinstances 0 sc < 2

175+ | not simpl -- || vinstances 0 sc < 2

173176 = do v' <- ev ntimes stk top env v --(finalise v)

174177 sc' <- ev ntimes stk top (v' : env) sc

175178 wknV (-1) sc'

176−{- | otherwise -- put this back when the Bind works properly

179+ | otherwise -- put this back when the Bind works properly

177180 = do t' <- ev ntimes stk top env t

178181 v' <- ev ntimes stk top env v --(finalise v)

179182 -- use Tmp as a placeholder, then make it a variable reference

180183 -- again when evaluation finished

181− sc' <- ev ntimes stk top (v' : env) sc

182− return $ VBind n (Let t' v') (\x -> return sc') -}

184+ hs <- get

185+ let vd = nexthole hs

186+ put (hs { nexthole = vd + 1 })

187+ sc' <- ev ntimes stk top (VP Bound (MN vd "vlet") VErased : env) sc

188+ return $ VBLet vd n t' v' sc'

183189 ev ntimes stk top env (Bind n (NLet t v) sc)

184190 = do t' <- ev ntimes stk top env (finalise t)

185191 v' <- ev ntimes stk top env (finalise v)

@@ -331,15 +337,14 @@ eval traceon ctxt ntimes genv tm opts = ev ntimes [] True [] tm where

331337 getValArgs' (VApp f a) as = getValArgs' f (a:as)

332338 getValArgs' f as = (f, as)

333339

334−tmpToV i (VTmp 0) = return $ VV i

335−tmpToV i (VP nt n v) = liftM (VP nt n) (tmpToV i v)

336−

337−tmpToV i (VBind n b sc) = do b' <- fmapMB (tmpToV i) b

338− let sc' = \x -> do x' <- sc x

339− tmpToV (i + 1) x'

340− return (VBind n b' sc')

341−tmpToV i (VApp f a) = liftM2 VApp (tmpToV i f) (tmpToV i a)

342−tmpToV i x = return x

340+-- tmpToV i vd (VLetHole j) | vd == j = return $ VV i

341+-- tmpToV i vd (VP nt n v) = liftM (VP nt n) (tmpToV i vd v)

342+-- tmpToV i vd (VBind n b sc) = do b' <- fmapMB (tmpToV i vd) b

343+-- let sc' = \x -> do x' <- sc x

344+-- tmpToV (i + 1) vd x'

345+-- return (VBind n b' sc')

346+-- tmpToV i vd (VApp f a) = liftM2 VApp (tmpToV i vd f) (tmpToV i vd a)

347+-- tmpToV i vd x = return x

343348

344349class Quote a where

345350 quote :: Int -> a -> Eval (TT Name)

@@ -351,6 +356,12 @@ instance Quote Value where

351356 b' <- quoteB b

352357 liftM (Bind n b') (quote (i+1) sc')

353358 where quoteB t = fmapMB (quote i) t

359+ quote i (VBLet vd n t v sc)

360+ = do sc' <- quote i sc

361+ t' <- quote i t

362+ v' <- quote i v

363+ let sc'' = pToV (MN vd "vlet") (addBinder sc')

364+ return (Bind n (Let t' v') sc'')

354365 quote i (VApp f a) = liftM2 App (quote i f) (quote i a)

355366 quote i (VType u) = return $ TType u

356367 quote i VErased = return $ Erased

src/Core/TT.hs+13−1

@@ -569,6 +569,17 @@ pToV' n i (App f a) = App (pToV' n i f) (pToV' n i a)

569569pToV' n i (Proj t idx) = Proj (pToV' n i t) idx

570570pToV' n i t = t

571571

572+-- increase de Bruijn indices, as if a binder has been added

573+addBinder :: TT n -> TT n

574+addBinder t = ab 0 t

575+ where

576+ ab top (V i) | i >= top = V (i + 1)

577+ | otherwise = V i

578+ ab top (Bind x b sc) = Bind x (fmap (ab top) b) (ab (top + 1) sc)

579+ ab top (App f a) = App (ab top f) (ab top a)

580+ ab top (Proj t idx) = Proj (ab top t) idx

581+ ab top t = t

582+

572583-- | Convert several names. First in the list comes out as V 0

573584pToVs :: Eq n => [n] -> TT n -> TT n

574585pToVs ns tm = pToVs' ns tm 0 where

@@ -787,7 +798,8 @@ prettyEnv env t = prettyEnv' env t False

787798showEnv' env t dbg = se 10 env t where

788799 se p env (P nt n t) = show n

789800 ++ if dbg then "{" ++ show nt ++ " : " ++ se 10 env t ++ "}" else ""

790− se p env (V i) | i < length env = (show $ fst $ env!!i) ++

801+ se p env (V i) | i < length env && i >= 0

802+ = (show $ fst $ env!!i) ++

791803 if dbg then "{" ++ show i ++ "}" else ""

792804 | otherwise = "!!V " ++ show i ++ "!!"

793805 se p env (Bind n b@(Pi t) sc)

src/IRTS/Compiler.hs+1−1

@@ -231,7 +231,7 @@ instance ToIR (TT Name) where

231231-- ir' env (P _ (NS (UN "O") ["Nat", "Prelude"]) _)

232232-- = return $ LConst (BI 0)

233233 ir' env (P _ n _) = return $ LV (Glob n)

234− ir' env (V i) | i < length env = return $ LV (Glob (env!!i))

234+ ir' env (V i) | i >= 0 && i < length env = return $ LV (Glob (env!!i))

235235 | otherwise = error $ "IR fail " ++ show i ++ " " ++ show tm

236236 ir' env (Bind n (Lam _) sc)

237237 = do let n' = uniqueName n env

src/Idris/REPL.hs+1−1

@@ -362,7 +362,7 @@ process fn (DebugInfo n)

362362 let di = lookupCtxt n (idris_datatypes i)

363363 when (not (null di)) $ iputStrLn (show di)

364364 let d = lookupDef n (tt_ctxt i)

365− when (not (null d)) $ iputStrLn (show (head d))

365+ when (not (null d)) $ iputStrLn $ "Definition: " ++ (show (head d))

366366 let cg = lookupCtxtName n (idris_callgraph i)

367367 findUnusedArgs (map fst cg)

368368 i <- getIState

test/test008/test008.idr−1

@@ -26,4 +26,3 @@ main = do (a, b) <- ioVals

2626 case lookup x testlist of

2727 Just v => putStrLn (show v)

2828 Nothing => putStrLn "Not there!"

29−