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

lib/checkall.idr+1

compare with master

unifiedsplit

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

20import prelude.vect

21import prelude.strings

22import prelude.char

23+import prelude.heap

23

24

24import network.cgi

25import network.cgi

25

26

lib/prelude/heap.idr+1−1

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

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

96 where

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

99

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

101fromList = foldr insert empty

src/Idris/ElabTerm.hs+11−1

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

321 False -> return failed

322 elabArgs ina failed r ns args

323

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+

324pruneAlt :: [PTerm] -> [PTerm]

327pruneAlt :: [PTerm] -> [PTerm]

325pruneAlt xs = map prune xs

328pruneAlt xs = map prune xs

326 where

329 where

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

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

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

329 prune t = t

332 prune t = t

330

333

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)

332 choose f t = t

341 choose f t = t

333

342

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

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

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

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

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

336

346

337trivial :: IState -> ElabD ()

347trivial :: IState -> ElabD ()

src/Idris/IBC.hs+1−1

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

177

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

179pFixes f = do i <- getIState

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

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

181

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

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

src/Idris/Parser.hs+2−1

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

459 istate <- getState

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

461 setState (istate {

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

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

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

464 fc <- pfc

465 return (PFix fc (f prec) ops)

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

687modifyConst syn fc (PConstant (I x))

688 | not (inPattern syn)

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

690+ | otherwise = PConstant (I x)

690modifyConst syn fc x = x

691modifyConst syn fc x = x

691

692

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

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