c182c92 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Allow simple function types to be reflected

commitc182c9259878fc1c34a44d3d15dfd504ba1dda2d authorEdwin Brady <ecb10@st-andrews.ac.uk> dateSun 11 Aug 2013, 17:03 (13 years ago) parent6d7dc4e

3 files changed+10

unifiedsplit

src/Core/CaseTree.hs+4

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

255255 return (PV n)

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

257257 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':[])

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

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

260264 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

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

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

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

348352 chooseAlt _ _ _ alts amap

349353 | Just v <- findDefault alts

350354 = if (any fnCase alts)

src/Idris/AbsSyntaxTree.hs+2

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

11151115 se p (PElabError s) = show s

11161116 se p (PCoerced t) = se p t

11171117 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

11181120-- se p x = "Not implemented"

11191121

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