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

git.iko.soy/Idris-dev

Simplify evaluator

It tries to support too much, but since it's part of the kernel it should do as little clever stuff as possible. Now just normalises, simplifies or specialises, the latter two simply meaning that certain names are blocked from being reduced.

commit6d7dc4e33431f434814122f2c03d1244cfc2dfd4 authorEdwin Brady <ecb10@st-andrews.ac.uk> dateFri 9 Aug 2013, 17:46 (13 years ago) parentdd12ac4

7 files changed+85−97

compare with master

unifiedsplit

lib/Builtins.idr−1 src/Core/Evaluate.hs+76−86 src/Core/ProofState.hs+2−1 src/Core/Typecheck.hs+1−1 src/Idris/ElabDecls.hs+4−6 src/Idris/ElabTerm.hs+1−1 src/Idris/REPL.hs+1−1

lib/Builtins.idr−1

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

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

189189

190190

191−

192191instance Ord Int where

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

194193 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

2727

2828data EvalOpt = Spec

2929 | HNF

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

31− -- totality checking so reduce dictionaries too

30+ | Simplify

3231 | AtREPL

3332 deriving (Show, Eq)

3433

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

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

4342 -- For frozen let bindings when simplifying

4443 | VBLet Int Name Value Value Value

45− | VApp Value (Value, -- inarg

46− Value) -- not inarg

44+ | VApp Value Value

4745 | VType UExp

4846 | VErased

4947 | VConstant Const

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

9189

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

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

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

95−simplify ctxt alldicts env t

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

93+-- be done elsewhere.

94+

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

96+simplify ctxt env t

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

9798 (UN "assert_smaller", 0),

9899 (UN "par", 0),

99100 (UN "prim__syntactic_eq", 0),

100101 (UN "fork", 0)]

101102 (map finalEntry env) (finalise t)

102− [Simplify alldicts]

103+ [Simplify]

103104 quote 0 val) initEval

104105

105106-- | Reduce a term to head normal form

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

125126unbindEnv [] tm = tm

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

127128

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

129−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 simpl True n ns

129+usable :: Bool -- specialising

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

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

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

133+usable True n ns

133134 = do ES ls num <- get

134135 case lookup n ls of

135136 Just 0 -> return (False, ns)

136137 Just i -> return (True, ns)

137138 _ -> return (False, ns)

138−usable simpl False n ns

139+usable False n ns

139140 = case lookup n ns of

140141 Just 0 -> return (False, ns)

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

144144

145145

146146deduct :: Name -> Eval ()

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

161161 [EvalOpt] -> Eval Value

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

163163 spec = Spec `elem` opts

164− simpl = Simplify True `elem` opts

164+ simpl = Simplify `elem` opts

165165 atRepl = AtREPL `elem` opts

166166 hnf = HNF `elem` opts

167167

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

169169 -- normal evaluation should return false

170− blockSimplify (CaseInfo inl dict) inarg n stk

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

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

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

174−

175− ev = ev' False

170+ blockSimplify (CaseInfo inl dict) n stk

171+ | Simplify `elem` opts

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

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

174+ | otherwise = False

176175

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

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

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

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

181180 | otherwise

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

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

183182 if u then

184183 do let val = lookupDefAcc n atRepl ctxt

185184 case val of

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

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

189188 return $ VP nt n vty

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

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

192− if blockSimplify ci inarg n stk

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

191+ if blockSimplify ci n stk

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

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

195194 case c of

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

197196 (Just v, _) -> return v

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

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

201200 = 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)

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

204203 | otherwise = return $ VV i

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

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

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

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

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

209207 wknV (-1) sc'

210− | otherwise

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

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

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

214− -- again when evaluation finished

215− hs <- get

216− let vd = nexthole hs

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

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

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

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

208+-- | otherwise

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

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

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

212+-- -- again when evaluation finished

213+-- hs <- get

214+-- let vd = nexthole hs

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

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

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

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

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

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

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

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

226224 = do b' <- vbind env b

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

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

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

229227 where vbind env t

230− | simpl

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

232− stk top env (finalise tm)) t

233− | otherwise

228+-- | simpl

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

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

231+-- | otherwise

234232 = 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)

236234 = 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

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

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

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

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

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

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

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

238+ ev ntimes stk top env Erased = return VErased

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

243240

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

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

246− evApply inarg ntimes stk top env args f

247− = apply inarg ntimes stk top env f args

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

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

243+ evApply ntimes stk top env args f

244+ = apply ntimes stk top env f args

248245

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)

250247 = do a' <- sc a

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

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

252249 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

254251 | not top && hnf = case args of

255252 [] -> return f

256253 _ -> return $ unload env f args

257254 | otherwise

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

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

259256 if u then

260257 do let val = lookupDefAcc n atRepl ctxt

261258 case val of

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

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

264− if blockSimplify ci inarg n stk

261+ if blockSimplify ci n stk

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

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

267264 case c of

268265 (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

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

271268 if (i <= length args)

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

269+ then case op (take i args) of

273270 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

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

276273 _ -> case args of

277274 [] -> return f

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

279276 else case args of

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

281278 [] -> return f

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

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

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

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

284281

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

286283-- = case lookupCtxt n statics of

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

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

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

293290

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

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

295292 unload env f [] = f

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

297294

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

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

301298 let rest = drop (length ns) args

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

303− tInArg <- evTree ntimes stk top env

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

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

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

307302 return (t, rest)

308303 | otherwise = return (Nothing, args)

309304

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

317312 return $ Just etm'

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

319314 = 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

321316 case c of

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

323318 _ -> 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

332327 conHeaded t = False

333328

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

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

336− chooseAlt env f' (getValInArgs f')

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

331+ chooseAlt env f' (getValArgs f')

337332 alts amap

338333

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

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

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

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

393388

394− getValInArgs tm = case getValArgs tm of

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

396−

397389 getValArgs tm = getValArgs' tm []

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

399391 getValArgs' f as = (f, as)

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

427419 v' <- quote i v

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

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

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

432424 quote i VErased = return $ Erased

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

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

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

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

440432 wknV i x')

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

442− b' <- wknV i b

443− f' <- wknV i f

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

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

445434wknV i t = return t

446435

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

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

693682 addDef n (CaseOp ci

694683 ty ps_in' ps args sc args' sc',

695684 acc, tot) ctxt

685+ Error err -> error (show err)

696686 _ -> ctxt in

697687 uctxt { definitions = ctxt' }

698688 where

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

704694 (vs, x', y')

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

706696 (vs, x', Impossible)

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

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

708698 simpl t = t

709699

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

src/Core/ProofState.hs+2−1

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

269269computeLet :: Context -> Name -> Term -> Term

270270computeLet ctxt n tm = cl [] tm where

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

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

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

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

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

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

275276 cl env t = t

src/Core/Typecheck.hs+1−1

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

7979 do convertsC ctxt env aty s

8080 -- let apty = normalise initContext env

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

82− let apty = simplify initContext False env

82+ let apty = simplify initContext env

8383 (Bind x (Let aty av) t)

8484 return (App fv av, apty)

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

253253 }

254254

255255 p_synEq [t,_,x,y]

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

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

258− | otherwise = Just (vApp vnNothing VErased)

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

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

258+ | otherwise = Just (VApp vnNothing VErased)

259259 p_synEq args = Nothing

260260

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

262−

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

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

265263 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

684682 getLHS (_, l, _) = l

685683

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

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

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

688686 simpl ctxt t = t

689687

690688 specNames [] = Nothing

src/Idris/ElabTerm.hs+1−1

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

302302 letbind n (Var tyn) (Var valn)

303303 focus valn

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

305− computeLet n

306305 env <- get_env

306+ computeLet n

307307 elabE (True, a) sc

308308 solve

309309-- elab' ina (PLet n Placeholder

src/Idris/REPL.hs+1−1

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

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

399399 ctxt <- getContext

400400 ist <- getIState

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

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

402402 iResult (show (delab ist tm'))

403403

404404process fn (RmProof n')