e6d48b6 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

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

e6d48b6Edwin Brady13 years ago

src/Core/Evaluate.hs+27−16

compare with master

unifiedsplit

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

19import Core.TT

20import Core.CaseTree

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

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

23+ nexthole :: Int }

24type Eval a = State EvalState a

25type Eval a = State EvalState a

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

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

27 deriving (Show, Eq)

28 deriving (Show, Eq)

29−initEval = ES []

30+initEval = ES [] 0

31-- VALUES (as HOAS) ---------------------------------------------------------

32-- VALUES (as HOAS) ---------------------------------------------------------

32-- | A HOAS representation of values

33-- | A HOAS representation of values

33data Value = VP NameType Name Value

34data Value = VP NameType Name Value

34 | VV Int

35 | VV Int

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

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

37+ | VBLet Int Name Value Value Value

36 | VApp Value Value

38 | VApp Value Value

37 | VType UExp

39 | VType UExp

38 | VErased

40 | VErased

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

166 (Just v, _) -> return v

168 (Just v, _) -> return v

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

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

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

170 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

170 | otherwise = return $ VV i

173 | otherwise = return $ VV i

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

174 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

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

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

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

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

175 wknV (-1) sc'

178 wknV (-1) sc'

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

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

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

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

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

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

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

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

180 -- again when evaluation finished

183 -- again when evaluation finished

184+ hs <- get

185+ let vd = nexthole hs

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

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

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

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

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

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

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

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

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

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

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

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

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

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

332 getValArgs' f as = (f, as)

338 getValArgs' f as = (f, as)

333

339

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

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

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

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

336−

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

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

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

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

339− tmpToV (i + 1) x'

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

340− return (VBind n b' sc')

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

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

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

342−tmpToV i x = return x

347+-- tmpToV i vd x = return x

343

348

344class Quote a where

349class Quote a where

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

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

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

351 b' <- quoteB b

356 b' <- quoteB b

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

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

353 where quoteB t = fmapMB (quote i) t

358 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'')

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

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

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

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

356 quote i VErased = return $ Erased

367 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)

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

570pToV' n i t = t

571

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+

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

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

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

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

574pToVs ns tm = pToVs' ns tm 0 where

585pToVs ns tm = pToVs' ns tm 0 where

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

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

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

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

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

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

800 ++ 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) ++

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

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

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

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

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

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

src/IRTS/Compiler.hs+1−1

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

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

232-- = return $ LConst (BI 0)

233 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))

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

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

237 = do let n' = uniqueName n env

src/Idris/REPL.hs+1−1

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

362 let di = lookupCtxt n (idris_datatypes i)

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

364 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))

366 let cg = lookupCtxtName n (idris_callgraph i)

367 findUnusedArgs (map fst cg)

368 i <- getIState

test/test008/test008.idr−1

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

26 case lookup x testlist of

27 Just v => putStrLn (show v)

28 Nothing => putStrLn "Not there!"

29−