3ce7d92 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Better pruning of alternatives so that resolving is much faster

commit3ce7d92173204c1e920223fbeaffacb1f4319427 authorEdwin Brady <eb@cs.st-andrews.ac.uk> dateSat 25 Feb 2012, 18:53 (15 years ago) parent58d0a31

5 files changed+16−4

compare with master

unifiedsplit

lib/checkall.idr+1 lib/prelude/heap.idr+1−1 src/Idris/ElabTerm.hs+11−1 src/Idris/IBC.hs+1−1 src/Idris/Parser.hs+2−1

lib/checkall.idr+1

@@ -20,6 +20,7 @@ import prelude.either

2020import prelude.vect

2121import prelude.strings

2222import prelude.char

23+import prelude.heap

2324

2425import network.cgi

2526

lib/prelude/heap.idr+1−1

@@ -95,7 +95,7 @@ toList Empty = []

9595toList (Node s l e r) = toList' (Node s l e r) refl

9696 where

9797 toList' : Ord a => (h : MaxiphobicHeap a) -> (isEmpty h = False) -> List a

98− toList' heap p = findMinimum heap p :: toList $ deleteMinimum heap p

98+ toList' heap p = findMinimum heap p :: (toList $ deleteMinimum heap p)

9999

100100fromList : Ord a => List a -> MaxiphobicHeap a

101101fromList = foldr insert empty

src/Idris/ElabTerm.hs+11−1

@@ -321,6 +321,9 @@ elab ist info pattern tcgen fn tm

321321 False -> return failed

322322 elabArgs ina failed r ns args

323323

324+-- For every alternative, look at the function at the head. Automatically resolve

325+-- any nested alternatives where that function is also at the head

326+

324327pruneAlt :: [PTerm] -> [PTerm]

325328pruneAlt xs = map prune xs

326329 where

@@ -328,10 +331,17 @@ pruneAlt xs = map prune xs

328331 = PApp fc1 (PRef fc2 f) (fmap (fmap (choose f)) as)

329332 prune t = t

330333

331− choose f (PAlternative as) = PAlternative (filter (headIs f) as)

334+ choose f (PAlternative as)

335+ = let as' = fmap (choose f) as

336+ fs = filter (headIs f) as' in

337+ case fs of

338+ [a] -> a

339+ _ -> PAlternative as'

340+ choose f (PApp fc f' as) = PApp fc (choose f f') (fmap (fmap (choose f)) as)

332341 choose f t = t

333342

334343 headIs f (PApp _ (PRef _ f') _) = f == f'

344+ headIs f (PApp _ f' _) = headIs f f'

335345 headIs f _ = True -- keep if it's not an application

336346

337347trivial :: IState -> ElabD ()

src/Idris/IBC.hs+1−1

@@ -177,7 +177,7 @@ pImps imps = mapM_ (\ (n, imp) ->

177177

178178pFixes :: [FixDecl] -> Idris ()

179179pFixes f = do i <- getIState

180− putIState (i { idris_infixes = f ++ idris_infixes i })

180+ putIState (i { idris_infixes = sort $ f ++ idris_infixes i })

181181

182182pStatics :: [(Name, [Bool])] -> Idris ()

183183pStatics ss = mapM_ (\ (n, s) ->

src/Idris/Parser.hs+2−1

@@ -459,7 +459,7 @@ pFixity = do push_indent

459459 istate <- getState

460460 let fs = map (Fix (f prec)) ops

461461 setState (istate {

462− idris_infixes = sort (fs ++ idris_infixes istate),

462+ idris_infixes = nub $ sort (fs ++ idris_infixes istate),

463463 ibc_write = map IBCFix fs ++ ibc_write istate })

464464 fc <- pfc

465465 return (PFix fc (f prec) ops)

@@ -687,6 +687,7 @@ modifyConst :: SyntaxInfo -> FC -> PTerm -> PTerm

687687modifyConst syn fc (PConstant (I x))

688688 | not (inPattern syn)

689689 = PApp fc (PRef fc (UN "fromInteger")) [pexp (PConstant (I x))]

690+ | otherwise = PConstant (I x)

690691modifyConst syn fc x = x

691692

692693pList syn = do lchar '['; fc <- pfc