c182c92 · Idris-dev · git.iko.soy

src/Core/CaseTree.hs+4

@@ -255,6 +255,10 @@ toPat reflect tc tms = evalState (mapM (\x -> toPat' x []) tms) []

255 return (PV n)

256 toPat' (App f a) args = toPat' f (a : args)

257 toPat' (Constant x) [] = return $ PConst x

258+ toPat' (Bind n (Pi t) sc) [] | reflect && noOccurrence n sc

259+ = do t' <- toPat' t []

260+ sc' <- toPat' sc []

261+ return $ PReflected (UN "->") (t':sc':[])

258 toPat' (P _ n _) args | reflect

262 toPat' (P _ n _) args | reflect

259 = do args' <- mapM (\x -> toPat' x []) args

263 = do args' <- mapM (\x -> toPat' x []) args

260 return $ PReflected n args'

264 return $ PReflected n args'

src/Core/Evaluate.hs+4

@@ -345,6 +345,10 @@ eval traceon ctxt ntimes genv tm opts = ev ntimes [] True [] tm where

345 | Just v <- findDefault alts = return $ Just (amap, v)

346 chooseAlt env _ (VP _ n _, args) alts amap

347 | Just (ns, sc) <- findFn n alts = return $ Just (updateAmap (zip ns args) amap, sc)

348+ chooseAlt env _ (VBind _ _ (Pi s) t, []) alts amap

349+ | Just (ns, sc) <- findFn (UN "->") alts

350+ = do t' <- t (VV 0) -- we know it's not in scope or it's not a pattern

351+ return $ Just (updateAmap (zip ns [s, t']) amap, sc)

348 chooseAlt _ _ _ alts amap

352 chooseAlt _ _ _ alts amap

349 | Just v <- findDefault alts

353 | Just v <- findDefault alts

350 = if (any fnCase alts)

354 = if (any fnCase alts)

src/Idris/AbsSyntaxTree.hs+2

@@ -1115,6 +1115,8 @@ showImp impl tm = se 10 tm where

1115 se p (PElabError s) = show s

1116 se p (PCoerced t) = se p t

1117 se p (PUnifyLog t) = "%unifyLog " ++ se p t

1118+ se p (PGoal f t n sc) = "quoteGoal " ++ show n ++ " by " ++ se 10 t ++

1119+ " in " ++ se 10 sc

1118-- se p x = "Not implemented"

1120-- se p x = "Not implemented"

1119

1121

1120 slist' p (PApp _ (PRef _ nil) _)

1122 slist' p (PApp _ (PRef _ nil) _)