6857a2c · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Make 'count' partial/abstract to prevent compile-time reduction

6857a2cEdwin Brady14 years ago

lib/Prelude.idr+2−2

compare with master

unifiedsplit

@@ -189,12 +189,12 @@ ceiling x = prim__floatCeil x

189

190---- Ranges

191

192−%assert_total

192+partial abstract

193count : (Ord a, Num a) => a -> a -> a -> List a

194count a inc b = if a <= b then a :: count (a + inc) inc b

195 else []

196

197−partial

197+partial abstract

198countFrom : (Ord a, Num a) => a -> a -> List a

199countFrom a inc = a :: lazy (countFrom (a + inc) inc)

200

src/Core/ProofState.hs+1−1

@@ -162,7 +162,7 @@ unify' ctxt env topx topy =

162-- -- " in " ++ show env ++

163-- "\n" ++ show u ++ "\n" ++ qshow fails ++ "\nCurrent problems:\n"

164-- ++ qshow (problems ps) ++ "\n" ++ show (holes ps) ++ "\n"

165−-- -- ++ show (pterm ps)

165+-- ++ show (pterm ps)

166-- ++ "\n----------") $

167 case fails of

168-- [] -> return u

src/Idris/IBC.hs+26−16

@@ -18,6 +18,8 @@ import Control.Monad.State hiding (get, put)

18import System.FilePath

19import System.Directory

21+import Debug.Trace

22+

21import Paths_idris

23import Paths_idris

23ibcVersion :: Word8

25ibcVersion :: Word8

@@ -48,6 +50,7 @@ data IBCFile = IBCFile { ver :: Word8,

48 ibc_docstrings :: [(Name, String)],

50 ibc_docstrings :: [(Name, String)],

49 ibc_coercions :: [Name]

51 ibc_coercions :: [Name]

50 }

52 }

53+ deriving Show

51{-!

54{-!

52deriving instance Binary IBCFile

55deriving instance Binary IBCFile

53!-}

56!-}

@@ -327,16 +330,21 @@ instance Binary FC where

327

330

328instance Binary Name where

331instance Binary Name where

329 put x

332 put x

333+ = {-# SCC "putName" #-}

330− = case x of

334+ case x of

335+ UN x1 -> {-# SCC "putUN" #-}

331− UN x1 -> do putWord8 0

336+ do putWord8 0

332− put x1

337+ {-# SCC "putNString" #-} put x1

338+ NS x1 x2 -> {-# SCC "putNS" #-}

333− NS x1 x2 -> do putWord8 1

339+ do putWord8 1

334 put x1

340 put x1

335 put x2

341 put x2

342+ MN x1 x2 -> {-# SCC "putMN" #-}

336− MN x1 x2 -> do putWord8 2

343+ do putWord8 2

337 put x1

344 put x1

338 put x2

345 put x2

346+ NErased -> {-# SCC "putNErased" #-}

339− NErased -> putWord8 3

347+ putWord8 3

340 get

348 get

341 = do i <- getWord8

349 = do i <- getWord8

342 case i of

350 case i of

@@ -528,9 +536,10 @@ instance Binary NameType where

528 _ -> error "Corrupted binary data for NameType"

536 _ -> error "Corrupted binary data for NameType"

529

537

530

538

531−instance (Binary n) => Binary (TT n) where

539+instance {-(Binary n) =>-} Binary (TT Name) where

532 put x

540 put x

541+ = {-# SCC "putTT" #-}

533− = case x of

542+ case x of

534 P x1 x2 x3 -> do putWord8 0

543 P x1 x2 x3 -> do putWord8 0

535 put x1

544 put x1

536 put x2

545 put x2

@@ -613,7 +622,8 @@ instance Binary SC where

613

622

614instance Binary CaseAlt where

623instance Binary CaseAlt where

615 put x

624 put x

625+ = {-# SCC "putCaseAlt" #-}

616− = case x of

626+ case x of

617 ConCase x1 x2 x3 x4 -> do putWord8 0

627 ConCase x1 x2 x3 x4 -> do putWord8 0

618 put x1

628 put x1

619 put x2

629 put x2

@@ -642,17 +652,16 @@ instance Binary CaseAlt where

642

652

643instance Binary Def where

653instance Binary Def where

644 put x

654 put x

655+ = {-# SCC "putDef" #-}

645− = case x of

656+ case x of

646 Function x1 x2 -> do putWord8 0

657 Function x1 x2 -> do putWord8 0

647 put x1

658 put x1

648 put x2

659 put x2

649 TyDecl x1 x2 -> do putWord8 1

660 TyDecl x1 x2 -> do putWord8 1

650 put x1

661 put x1

651 put x2

662 put x2

663+ -- all primitives just get added at the start, don't write

652− Operator x1 x2 x3 -> do putWord8 2

664+ Operator x1 x2 x3 -> do return ()

653− put x1

654− put x2

655− put x3

656 CaseOp x1 x2 x3 x3a x4 x5 x6 x7 x8 ->

665 CaseOp x1 x2 x3 x3a x4 x5 x6 x7 x8 ->

657 do putWord8 3

666 do putWord8 3

658 put x1

667 put x1

@@ -750,8 +759,9 @@ instance Binary Totality where

750 _ -> error "Corrupted binary data for Totality"

759 _ -> error "Corrupted binary data for Totality"

751

760

752instance Binary IBCFile where

761instance Binary IBCFile where

753− put (IBCFile x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 x21 x22 x23 x24)

762+ put x@(IBCFile x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 x21 x22 x23 x24)

763+ = {-# SCC "putIBCFile" #-}

754− = do put x1

764+ do put x1

755 put x2

765 put x2

756 put x3

766 put x3

757 put x4

767 put x4