6d7dc4e · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Simplify evaluator

6d7dc4eEdwin Brady13 years ago

lib/Builtins.idr−1

compare with master

unifiedsplit

@@ -188,7 +188,6 @@ class Eq a => Ord a where

188 min x y = if (x < y) then x else y

189

190

191−

192instance Ord Int where

191instance Ord Int where

193 compare x y = if (x == y) then EQ else

192 compare x y = if (x == y) then EQ else

194 if (boolOp prim__sltInt x y) then LT else

193 if (boolOp prim__sltInt x y) then LT else

src/Core/Evaluate.hs+76−86

@@ -27,8 +27,7 @@ type Eval a = State EvalState a

28data EvalOpt = Spec

29 | HNF

30− | Simplify Bool -- simplifying - if True, we're doing it to help

30+ | Simplify

31− -- totality checking so reduce dictionaries too

32 | AtREPL

31 | AtREPL

33 deriving (Show, Eq)

32 deriving (Show, Eq)

@@ -42,8 +41,7 @@ data Value = VP NameType Name Value

42 | VBind Bool Name (Binder Value) (Value -> Eval Value)

41 | VBind Bool Name (Binder Value) (Value -> Eval Value)

43 -- For frozen let bindings when simplifying

42 -- For frozen let bindings when simplifying

44 | VBLet Int Name Value Value Value

43 | VBLet Int Name Value Value Value

45− | VApp Value (Value, -- inarg

44+ | VApp Value Value

46− Value) -- not inarg

47 | VType UExp

45 | VType UExp

48 | VErased

46 | VErased

49 | VConstant Const

47 | VConstant Const

@@ -91,15 +89,18 @@ specialise ctxt env limits t

92-- | Like normalise, but we only reduce functions that are marked as okay to

90-- | Like normalise, but we only reduce functions that are marked as okay to

93-- inline (and probably shouldn't reduce lets?)

91-- inline (and probably shouldn't reduce lets?)

92+-- 20130908: now only used to reduce for totality checking. Inlining should

93+-- be done elsewhere.

94+

94−simplify :: Context -> Bool -> Env -> TT Name -> TT Name

95+simplify :: Context -> Env -> TT Name -> TT Name

95−simplify ctxt alldicts env t

96+simplify ctxt env t

96 = evalState (do val <- eval False ctxt [(UN "lazy", 0),

97 = evalState (do val <- eval False ctxt [(UN "lazy", 0),

97 (UN "assert_smaller", 0),

98 (UN "assert_smaller", 0),

98 (UN "par", 0),

99 (UN "par", 0),

99 (UN "prim__syntactic_eq", 0),

100 (UN "prim__syntactic_eq", 0),

100 (UN "fork", 0)]

101 (UN "fork", 0)]

101 (map finalEntry env) (finalise t)

102 (map finalEntry env) (finalise t)

102− [Simplify alldicts]

103+ [Simplify]

103 quote 0 val) initEval

104 quote 0 val) initEval

104

105

105-- | Reduce a term to head normal form

106-- | Reduce a term to head normal form

@@ -125,22 +126,21 @@ unbindEnv :: EnvTT n -> TT n -> TT n

125unbindEnv [] tm = tm

126unbindEnv [] tm = tm

126unbindEnv (_:bs) (Bind n b sc) = unbindEnv bs sc

127unbindEnv (_:bs) (Bind n b sc) = unbindEnv bs sc

127

128

129+usable :: Bool -- specialising

128−usable :: Bool -> Bool -> Name -> [(Name, Int)] -> Eval (Bool, [(Name, Int)])

130+ -> Name -> [(Name, Int)] -> Eval (Bool, [(Name, Int)])

129−usable _ _ _ ns@((MN 0 "STOP", _) : _) = return (False, ns)

131+-- usable _ _ ns@((MN 0 "STOP", _) : _) = return (False, ns)

130−usable True _ (UN "io_bind") ns = return (False, ns)

131−usable simpl False n [] = return (True, [])

132+usable False n [] = return (True, [])

132−usable simpl True n ns

133+usable True n ns

133 = do ES ls num <- get

134 = do ES ls num <- get

134 case lookup n ls of

135 case lookup n ls of

135 Just 0 -> return (False, ns)

136 Just 0 -> return (False, ns)

136 Just i -> return (True, ns)

137 Just i -> return (True, ns)

137 _ -> return (False, ns)

138 _ -> return (False, ns)

138−usable simpl False n ns

139+usable False n ns

139 = case lookup n ns of

140 = case lookup n ns of

140 Just 0 -> return (False, ns)

141 Just 0 -> return (False, ns)

141 Just i -> return $ (True, (n, abs (i-1)) : filter (\ (n', _) -> n/=n') ns)

142 Just i -> return $ (True, (n, abs (i-1)) : filter (\ (n', _) -> n/=n') ns)

142− _ -> if simpl then return $ (True, (n, 0) : filter (\ (n', _) -> n/=n') ns)

143− else return $ (True, (n, 100) : filter (\ (n', _) -> n/=n') ns)

143+ _ -> return $ (True, (n, 100) : filter (\ (n', _) -> n/=n') ns)

144

145

146deduct :: Name -> Eval ()

@@ -161,25 +161,24 @@ eval :: Bool -> Context -> [(Name, Int)] -> Env -> TT Name ->

161 [EvalOpt] -> Eval Value

162eval traceon ctxt ntimes genv tm opts = ev ntimes [] True [] tm where

163 spec = Spec `elem` opts

164− simpl = Simplify True `elem` opts

164+ simpl = Simplify `elem` opts

165 atRepl = AtREPL `elem` opts

166 hnf = HNF `elem` opts

167

168 -- returns 'True' if the function should block

169 -- normal evaluation should return false

170− blockSimplify (CaseInfo inl dict) inarg n stk

170+ blockSimplify (CaseInfo inl dict) n stk

171+ | Simplify `elem` opts

171− = (Simplify False `elem` opts && (not (inl || dict) || elem n stk))

172+ = (not (inl || dict) || elem n stk)

172− || (Simplify True `elem` opts &&

173+ || (n == UN "prim__syntactic_eq")

173− (not (inl || (dict && False)) || elem n stk))

174−

175− ev = ev' False

174+ | otherwise = False

176

175

177− ev' inarg ntimes stk top env (P _ n ty)

176+ ev ntimes stk top env (P _ n ty)

178 | Just (Let t v) <- lookup n genv = ev ntimes stk top env v

177 | Just (Let t v) <- lookup n genv = ev ntimes stk top env v

179− ev' inarg ntimes_in stk top env (P Ref n ty)

178+ ev ntimes_in stk top env (P Ref n ty)

180 | not top && hnf = liftM (VP Ref n) (ev ntimes stk top env ty)

179 | not top && hnf = liftM (VP Ref n) (ev ntimes stk top env ty)

181 | otherwise

180 | otherwise

182− = do (u, ntimes) <- usable simpl spec n ntimes_in

181+ = do (u, ntimes) <- usable spec n ntimes_in

183 if u then

182 if u then

184 do let val = lookupDefAcc n atRepl ctxt

183 do let val = lookupDefAcc n atRepl ctxt

185 case val of

184 case val of

@@ -188,8 +187,8 @@ eval traceon ctxt ntimes genv tm opts = ev ntimes [] True [] tm where

188 [(TyDecl nt ty, _)] -> do vty <- ev ntimes stk True env ty

187 [(TyDecl nt ty, _)] -> do vty <- ev ntimes stk True env ty

189 return $ VP nt n vty

188 return $ VP nt n vty

190 [(CaseOp ci _ _ _ [] tree _ _, acc)]

189 [(CaseOp ci _ _ _ [] tree _ _, acc)]

191− | acc == Public || simpl -> -- unoptimised version

190+ | acc == Public -> -- unoptimised version

192− if blockSimplify ci inarg n stk

191+ if blockSimplify ci n stk

193 then liftM (VP Ref n) (ev ntimes stk top env ty)

192 then liftM (VP Ref n) (ev ntimes stk top env ty)

194 else do c <- evCase ntimes n (n:stk) top env [] [] tree

193 else do c <- evCase ntimes n (n:stk) top env [] [] tree

195 case c of

194 case c of

@@ -197,81 +196,79 @@ eval traceon ctxt ntimes genv tm opts = ev ntimes [] True [] tm where

197 (Just v, _) -> return v

196 (Just v, _) -> return v

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

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

199 else liftM (VP Ref n) (ev ntimes stk top env ty)

198 else liftM (VP Ref n) (ev ntimes stk top env ty)

200− ev' inarg ntimes stk top env (P nt n ty)

199+ ev ntimes stk top env (P nt n ty)

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

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

202− ev' inarg ntimes stk top env (V i)

201+ ev ntimes stk top env (V i)

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

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

204 | otherwise = return $ VV i

203 | otherwise = return $ VV i

205− ev' inarg ntimes stk top env (Bind n (Let t v) sc)

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

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

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

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

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

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

209 wknV (-1) sc'

207 wknV (-1) sc'

210− | otherwise

208+-- | otherwise

211− = do t' <- ev ntimes stk top env t

209+-- = do t' <- ev ntimes stk top env t

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

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

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

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

214− -- again when evaluation finished

212+-- -- again when evaluation finished

215− hs <- get

213+-- hs <- get

216− let vd = nexthole hs

214+-- let vd = nexthole hs

217− put (hs { nexthole = vd + 1 })

215+-- put (hs { nexthole = vd + 1 })

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

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

219− return $ VBLet vd n t' v' sc'

217+-- return $ VBLet vd n t' v' sc'

220− ev' inarg ntimes stk top env (Bind n (NLet t v) sc)

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

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

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

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

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

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

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

224 return $ VBind True n (Let t' v') (\x -> return sc')

222 return $ VBind True n (Let t' v') (\x -> return sc')

225− ev' inarg ntimes stk top env (Bind n b sc)

223+ ev ntimes stk top env (Bind n b sc)

226 = do b' <- vbind env b

224 = do b' <- vbind env b

227− return $ VBind (not simpl || vinstances 0 sc < 2)

225+ return $ VBind True -- (vinstances 0 sc < 2)

228 n b' (\x -> ev ntimes stk False (x:env) sc)

226 n b' (\x -> ev ntimes stk False (x:env) sc)

229 where vbind env t

227 where vbind env t

230− | simpl

228+-- | simpl

231− = fmapMB (\tm -> ev ((MN 0 "STOP", 0) : ntimes)

229+-- = fmapMB (\tm -> ev ((MN 0 "STOP", 0) : ntimes)

232− stk top env (finalise tm)) t

230+-- stk top env (finalise tm)) t

233− | otherwise

231+-- | otherwise

234 = fmapMB (\tm -> ev ntimes stk top env (finalise tm)) t

232 = fmapMB (\tm -> ev ntimes stk top env (finalise tm)) t

235− ev' inarg ntimes stk top env (App f a)

233+ ev ntimes stk top env (App f a)

236 = do f' <- ev ntimes stk False env f

234 = do f' <- ev ntimes stk False env f

237− a' <- ev' False ntimes stk False env a

238− aArg' <- ev' True ntimes stk False env a

235+ a' <- ev ntimes stk False env a

239− evApply inarg ntimes stk top env [(aArg', a')] f'

236+ evApply ntimes stk top env [a'] f'

240− ev' inarg ntimes stk top env (Constant c) = return $ VConstant c

237+ ev ntimes stk top env (Constant c) = return $ VConstant c

241− ev' inarg ntimes stk top env Erased = return VErased

238+ ev ntimes stk top env Erased = return VErased

242− ev' inarg ntimes stk top env (TType i) = return $ VType i

239+ ev ntimes stk top env (TType i) = return $ VType i

243

240

244− evApply inarg ntimes stk top env args (VApp f a)

241+ evApply ntimes stk top env args (VApp f a)

245− = evApply inarg ntimes stk top env (a:args) f

242+ = evApply ntimes stk top env (a:args) f

246− evApply inarg ntimes stk top env args f

243+ evApply ntimes stk top env args f

247− = apply inarg ntimes stk top env f args

244+ = apply ntimes stk top env f args

248

245

249− apply inarg ntimes stk top env (VBind True n (Lam t) sc) ((_,a):as)

246+ apply ntimes stk top env (VBind True n (Lam t) sc) (a:as)

250 = do a' <- sc a

247 = do a' <- sc a

251− app <- apply inarg ntimes stk top env a' as

248+ app <- apply ntimes stk top env a' as

252 wknV (-1) app

249 wknV (-1) app

253− apply inarg ntimes_in stk top env f@(VP Ref n ty) args

250+ apply ntimes_in stk top env f@(VP Ref n ty) args

254 | not top && hnf = case args of

251 | not top && hnf = case args of

255 [] -> return f

252 [] -> return f

256 _ -> return $ unload env f args

253 _ -> return $ unload env f args

257 | otherwise

254 | otherwise

258− = do (u, ntimes) <- usable simpl spec n ntimes_in

255+ = do (u, ntimes) <- usable spec n ntimes_in

259 if u then

256 if u then

260 do let val = lookupDefAcc n atRepl ctxt

257 do let val = lookupDefAcc n atRepl ctxt

261 case val of

258 case val of

262 [(CaseOp ci _ _ _ ns tree _ _, acc)]

259 [(CaseOp ci _ _ _ ns tree _ _, acc)]

263 | acc == Public -> -- unoptimised version

260 | acc == Public -> -- unoptimised version

264− if blockSimplify ci inarg n stk

261+ if blockSimplify ci n stk

265 then return $ unload env (VP Ref n ty) args

262 then return $ unload env (VP Ref n ty) args

266 else do c <- evCase ntimes n (n:stk) top env ns args tree

263 else do c <- evCase ntimes n (n:stk) top env ns args tree

267 case c of

264 case c of

268 (Nothing, _) -> return $ unload env (VP Ref n ty) args

265 (Nothing, _) -> return $ unload env (VP Ref n ty) args

269− (Just v, rest) -> evApply inarg ntimes stk top env rest v

266+ (Just v, rest) -> evApply ntimes stk top env rest v

270 [(Operator _ i op, _)] ->

267 [(Operator _ i op, _)] ->

271 if (i <= length args)

268 if (i <= length args)

272− then case op (map snd (take i args)) of

269+ then case op (take i args) of

273 Nothing -> return $ unload env (VP Ref n ty) args

270 Nothing -> return $ unload env (VP Ref n ty) args

274− Just v -> evApply inarg ntimes stk top env (drop i args) v

271+ Just v -> evApply ntimes stk top env (drop i args) v

275 else return $ unload env (VP Ref n ty) args

272 else return $ unload env (VP Ref n ty) args

276 _ -> case args of

273 _ -> case args of

277 [] -> return f

274 [] -> return f

@@ -279,8 +276,8 @@ eval traceon ctxt ntimes genv tm opts = ev ntimes [] True [] tm where

279 else case args of

276 else case args of

280 (a : as) -> return $ unload env f (a:as)

277 (a : as) -> return $ unload env f (a:as)

281 [] -> return f

278 [] -> return f

282− apply inarg ntimes stk top env f (a:as) = return $ unload env f (a:as)

279+ apply ntimes stk top env f (a:as) = return $ unload env f (a:as)

283− apply inarg ntimes stk top env f [] = return f

280+ apply ntimes stk top env f [] = return f

284

281

285-- specApply stk env f@(VP Ref n ty) args

282-- specApply stk env f@(VP Ref n ty) args

286-- = case lookupCtxt n statics of

283-- = case lookupCtxt n statics of

@@ -291,7 +288,7 @@ eval traceon ctxt ntimes genv tm opts = ev ntimes [] True [] tm where

291-- _ -> return $ unload env f args

288-- _ -> return $ unload env f args

292-- specApply stk env f args = return $ unload env f args

289-- specApply stk env f args = return $ unload env f args

293

290

294− unload :: [Value] -> Value -> [(Value, Value)] -> Value

291+ unload :: [Value] -> Value -> [Value] -> Value

295 unload env f [] = f

292 unload env f [] = f

296 unload env f (a:as) = unload env (VApp f a) as

293 unload env f (a:as) = unload env (VApp f a) as

297

294

@@ -300,10 +297,8 @@ eval traceon ctxt ntimes genv tm opts = ev ntimes [] True [] tm where

300 = do let args' = take (length ns) args

297 = do let args' = take (length ns) args

301 let rest = drop (length ns) args

298 let rest = drop (length ns) args

302 when spec $ deduct n -- successful, so deduct usages

299 when spec $ deduct n -- successful, so deduct usages

303− tInArg <- evTree ntimes stk top env

300+ t <- evTree ntimes stk top env (zip ns args') tree

304− (zipWith (\n (t, _) -> (n, t)) ns args') tree

305− t<- evTree ntimes stk top env

306− (zipWith (\n (_, t) -> (n, t)) ns args') tree

301+-- (zipWith (\n , t) -> (n, t)) ns args') tree

307 return (t, rest)

302 return (t, rest)

308 | otherwise = return (Nothing, args)

303 | otherwise = return (Nothing, args)

309

304

@@ -317,7 +312,7 @@ eval traceon ctxt ntimes genv tm opts = ev ntimes [] True [] tm where

317 return $ Just etm'

312 return $ Just etm'

318 evTree ntimes stk top env amap (Case n alts)

313 evTree ntimes stk top env amap (Case n alts)

319 = case lookup n amap of

314 = case lookup n amap of

320− Just v -> do c <- chooseAlt env v (getValInArgs v) alts amap

315+ Just v -> do c <- chooseAlt env v (getValArgs v) alts amap

321 case c of

316 case c of

322 Just (altmap, sc) -> evTree ntimes stk top env altmap sc

317 Just (altmap, sc) -> evTree ntimes stk top env altmap sc

323 _ -> do c' <- chooseAlt' ntimes stk env v (getValArgs v) alts amap

318 _ -> do c' <- chooseAlt' ntimes stk env v (getValArgs v) alts amap

@@ -332,8 +327,8 @@ eval traceon ctxt ntimes genv tm opts = ev ntimes [] True [] tm where

332 conHeaded t = False

327 conHeaded t = False

333

328

334 chooseAlt' ntimes stk env _ (f, args) alts amap

329 chooseAlt' ntimes stk env _ (f, args) alts amap

335− = do f' <- apply False ntimes stk True env f args

330+ = do f' <- apply ntimes stk True env f args

336− chooseAlt env f' (getValInArgs f')

331+ chooseAlt env f' (getValArgs f')

337 alts amap

332 alts amap

338

333

339 chooseAlt :: [Value] -> Value -> (Value, [Value]) -> [CaseAlt] ->

334 chooseAlt :: [Value] -> Value -> (Value, [Value]) -> [CaseAlt] ->

@@ -391,9 +386,6 @@ eval traceon ctxt ntimes genv tm opts = ev ntimes [] True [] tm where

391 | tag == (fromEnum ity + 1) * 1000 + count = Just v

386 | tag == (fromEnum ity + 1) * 1000 + count = Just v

392 findConst c (_ : xs) = findConst c xs

387 findConst c (_ : xs) = findConst c xs

393

388

394− getValInArgs tm = case getValArgs tm of

395− (f, as) -> (f, map snd as)

396−

397 getValArgs tm = getValArgs' tm []

389 getValArgs tm = getValArgs' tm []

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

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

399 getValArgs' f as = (f, as)

391 getValArgs' f as = (f, as)

@@ -427,7 +419,7 @@ instance Quote Value where

427 v' <- quote i v

419 v' <- quote i v

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

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

429 return (Bind n (Let t' v') sc'')

421 return (Bind n (Let t' v') sc'')

430− quote i (VApp f (_,a)) = liftM2 App (quote i f) (quote i a)

422+ quote i (VApp f a) = liftM2 App (quote i f) (quote i a)

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

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

432 quote i VErased = return $ Erased

424 quote i VErased = return $ Erased

433 quote i (VConstant c) = return $ Constant c

425 quote i (VConstant c) = return $ Constant c

@@ -438,10 +430,7 @@ wknV i (VV x) = return $ VV (x + i)

438wknV i (VBind red n b sc) = do b' <- fmapMB (wknV i) b

430wknV i (VBind red n b sc) = do b' <- fmapMB (wknV i) b

439 return $ VBind red n b' (\x -> do x' <- sc x

431 return $ VBind red n b' (\x -> do x' <- sc x

440 wknV i x')

432 wknV i x')

441−wknV i (VApp f (a,b)) = do a' <- wknV i a

433+wknV i (VApp f a) = liftM2 VApp (wknV i f) (wknV i a)

442− b' <- wknV i b

443− f' <- wknV i f

444− return $ VApp f' (a',b')

445wknV i t = return t

434wknV i t = return t

446

435

447convEq' ctxt x y = evalStateT (convEq ctxt x y) (0, [])

436convEq' ctxt x y = evalStateT (convEq ctxt x y) (0, [])

@@ -693,6 +682,7 @@ simplifyCasedef n uctxt

693 addDef n (CaseOp ci

682 addDef n (CaseOp ci

694 ty ps_in' ps args sc args' sc',

683 ty ps_in' ps args sc args' sc',

695 acc, tot) ctxt

684 acc, tot) ctxt

685+ Error err -> error (show err)

696 _ -> ctxt in

686 _ -> ctxt in

697 uctxt { definitions = ctxt' }

687 uctxt { definitions = ctxt' }

698 where

688 where

@@ -704,7 +694,7 @@ simplifyCasedef n uctxt

704 (vs, x', y')

694 (vs, x', y')

705 debind (Left x) = let (vs, x') = depat [] x in

695 debind (Left x) = let (vs, x') = depat [] x in

706 (vs, x', Impossible)

696 (vs, x', Impossible)

707− simpl (Right (x, y)) = Right (x, simplify uctxt False [] y)

697+ simpl (Right (x, y)) = Right (x, simplify uctxt [] y)

708 simpl t = t

698 simpl t = t

709

699

710addOperator :: Name -> Type -> Int -> ([Value] -> Maybe Value) ->

700addOperator :: Name -> Type -> Int -> ([Value] -> Maybe Value) ->

src/Core/ProofState.hs+2−1

@@ -269,7 +269,8 @@ tactic h f = do ps <- get

269computeLet :: Context -> Name -> Term -> Term

270computeLet ctxt n tm = cl [] tm where

271 cl env (Bind n' (Let t v) sc)

272+ | n' == n = let v' = normalise ctxt env v in

272− | n' == n = Bind n' (Let t (normalise ctxt env v)) sc

273+ Bind n' (Let t v') sc

273 cl env (Bind n' b sc) = Bind n' (fmap (cl env) b) (cl ((n, b):env) sc)

274 cl env (Bind n' b sc) = Bind n' (fmap (cl env) b) (cl ((n, b):env) sc)

274 cl env (App f a) = App (cl env f) (cl env a)

275 cl env (App f a) = App (cl env f) (cl env a)

275 cl env t = t

276 cl env t = t

src/Core/Typecheck.hs+1−1

@@ -79,7 +79,7 @@ check' holes ctxt env top = chk env top where

79 do convertsC ctxt env aty s

80 -- let apty = normalise initContext env

81 -- (Bind x (Let aty av) t)

82− let apty = simplify initContext False env

82+ let apty = simplify initContext env

83 (Bind x (Let aty av) t)

84 return (App fv av, apty)

85 t -> lift $ tfail $ NonFunctionType fv fty -- "Can't apply a non-function type"

src/Idris/ElabDecls.hs+4−6

@@ -253,13 +253,11 @@ elabPrims = do mapM_ (elabDecl EAll toplevel)

253 }

254

255 p_synEq [t,_,x,y]

256− | x == y = Just (vApp (vApp vnJust VErased)

256+ | x == y = Just (VApp (VApp vnJust VErased)

257− (vApp (vApp vnRefl t) x))

257+ (VApp (VApp vnRefl t) x))

258− | otherwise = Just (vApp vnNothing VErased)

258+ | otherwise = Just (VApp vnNothing VErased)

259 p_synEq args = Nothing

260

261− vApp f a = VApp f (a, a)

262−

263 nMaybe = P (TCon 0 2) (NS (UN "Maybe") ["Maybe", "Prelude"]) Erased

261 nMaybe = P (TCon 0 2) (NS (UN "Maybe") ["Maybe", "Prelude"]) Erased

264 vnJust = VP (DCon 1 2) (NS (UN "Just") ["Maybe", "Prelude"]) VErased

262 vnJust = VP (DCon 1 2) (NS (UN "Just") ["Maybe", "Prelude"]) VErased

265 vnNothing = VP (DCon 0 1) (NS (UN "Nothing") ["Maybe", "Prelude"]) VErased

263 vnNothing = VP (DCon 0 1) (NS (UN "Nothing") ["Maybe", "Prelude"]) VErased

@@ -684,7 +682,7 @@ elabClauses info fc opts n_in cs = let n = liftname info n_in in

684 getLHS (_, l, _) = l

682 getLHS (_, l, _) = l

685

683

686 simpl ctxt (Right (x, y)) = Right (normalise ctxt [] x, y)

684 simpl ctxt (Right (x, y)) = Right (normalise ctxt [] x, y)

687−-- Core.Evaluate.simplify ctxt True [] y)

685+-- Core.Evaluate.simplify ctxt False [] y)

688 simpl ctxt t = t

686 simpl ctxt t = t

689

687

690 specNames [] = Nothing

688 specNames [] = Nothing

src/Idris/ElabTerm.hs+1−1

@@ -302,8 +302,8 @@ elab ist info pattern tcgen fn tm

302 letbind n (Var tyn) (Var valn)

303 focus valn

304 elabE (True, a) (PApp fc r [pexp (delab ist rty)])

305− computeLet n

306 env <- get_env

305 env <- get_env

306+ computeLet n

307 elabE (True, a) sc

308 solve

309-- elab' ina (PLet n Placeholder

src/Idris/REPL.hs+1−1

@@ -398,7 +398,7 @@ process fn (Search t) = iFail "Not implemented"

398process fn (Spec t) = do (tm, ty) <- elabVal toplevel False t

399 ctxt <- getContext

400 ist <- getIState

401− let tm' = simplify ctxt True [] {- (idris_statics ist) -} tm

401+ let tm' = simplify ctxt [] {- (idris_statics ist) -} tm

402 iResult (show (delab ist tm'))

403

404process fn (RmProof n')