814ebda · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Make sure patterns are in dependency order

814ebdaEdwin Brady15 years ago

src/Core/TT.hs+25

compare with master

unifiedsplit

@@ -6,6 +6,7 @@ import Control.Monad.State

6import Debug.Trace

7import qualified Data.Map as Map

8import Data.Char

9+import Data.List

10{- The language has:

11{- The language has:

11 * Full dependent types

12 * Full dependent types

@@ -405,4 +406,28 @@ weakenEnv env = wk (length env - 1) env

405weakenTmEnv :: Int -> EnvTT n -> EnvTT n

406weakenTmEnv :: Int -> EnvTT n -> EnvTT n

406weakenTmEnv i = map (\ (n, b) -> (n, fmap (weakenTm i) b))

407weakenTmEnv i = map (\ (n, b) -> (n, fmap (weakenTm i) b))

407

408

409+orderPats :: Term -> Term

410+orderPats tm = op [] tm

411+ where

412+ op ps (Bind n (PVar t) sc) = op ((n, t) : ps) sc

413+ op ps sc = bindAll (map (\ (n, t) -> (n, PVar t)) (sortP ps)) sc

414+

415+ sortP ps = pick [] (reverse ps)

416+

417+ namesIn (P _ n _) = [n]

418+ namesIn (Bind n b t) = nub $ nb b ++ (namesIn t \\ [n])

419+ where nb (Let t v) = nub (namesIn t) ++ nub (namesIn v)

420+ nb (Guess t v) = nub (namesIn t) ++ nub (namesIn v)

421+ nb t = namesIn (binderTy t)

422+ namesIn (App f a) = nub (namesIn f ++ namesIn a)

423+ namesIn _ = []

424+

425+ pick acc [] = reverse acc

426+ pick acc ((n, t) : ps) = pick (insert n t acc) ps

427+

428+ insert n t [] = [(n, t)]

429+ insert n t ((n',t') : ps)

430+ | n `elem` (namesIn t' ++ concatMap namesIn (map snd ps))

431+ = (n', t') : insert n t ps

432+ | otherwise = (n,t):(n',t'):ps

408

433

src/Idris/ElabDecls.hs+2−2

@@ -128,7 +128,7 @@ elabClause info fc (PClause fname lhs_in withs rhs_in whereblock)

128 logLvl 5 ("LHS: " ++ showImp True lhs)

129 ((lhs', dlhs), _) <- tclift $ elaborate ctxt (MN 0 "patLHS") infP

130 (erun fc (build i info True (infTerm lhs)))

131− let lhs_tm = getInferTerm lhs'

131+ let lhs_tm = orderPats (getInferTerm lhs')

132 let lhs_ty = getInferType lhs'

133 logLvl 3 (show lhs_tm)

134 (clhs, clhsty) <- tclift $ recheck ctxt [] lhs_tm

@@ -187,7 +187,7 @@ elabClause info fc (PWith fname lhs_in withs wval_in withblock)

187 logLvl 5 ("LHS: " ++ showImp True lhs)

188 ((lhs', dlhs), _) <- tclift $ elaborate ctxt (MN 0 "patLHS") infP

189 (erun fc (build i info True (infTerm lhs)))

190− let lhs_tm = getInferTerm lhs'

190+ let lhs_tm = orderPats (getInferTerm lhs')

191 let lhs_ty = getInferType lhs'

192 let ret_ty = getRetTy lhs_ty

193 logLvl 3 (show lhs_tm)