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

git.iko.soy/Idris-dev

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

Deals with issue #171

commit6857a2cd7f95c627cc61d81fee6c8f0b34ebe505 authorEdwin Brady <ecb10@st-andrews.ac.uk> dateFri 12 Apr 2013, 17:23 (14 years ago) parent071b834

3 files changed+29−19

compare with master

unifiedsplit

lib/Prelude.idr+2−2 src/Core/ProofState.hs+1−1 src/Idris/IBC.hs+26−16

lib/Prelude.idr+2−2

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

189189

190190---- Ranges

191191

192−%assert_total

192+partial abstract

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

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

195195 else []

196196

197−partial

197+partial abstract

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

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

200200

src/Core/ProofState.hs+1−1

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

162162-- -- " in " ++ show env ++

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

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

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

165+-- ++ show (pterm ps)

166166-- ++ "\n----------") $

167167 case fails of

168168-- [] -> return u

src/Idris/IBC.hs+26−16

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

1818import System.FilePath

1919import System.Directory

2020

21+import Debug.Trace

22+

2123import Paths_idris

2224

2325ibcVersion :: Word8

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

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

4951 ibc_coercions :: [Name]

5052 }

53+ deriving Show

5154{-!

5255deriving instance Binary IBCFile

5356!-}

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

327330

328331instance Binary Name where

329332 put x

330− = case x of

331− UN x1 -> do putWord8 0

332− put x1

333− NS x1 x2 -> do putWord8 1

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

334+ case x of

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

336+ do putWord8 0

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

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

339+ do putWord8 1

334340 put x1

335341 put x2

336− MN x1 x2 -> do putWord8 2

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

343+ do putWord8 2

337344 put x1

338345 put x2

339− NErased -> putWord8 3

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

347+ putWord8 3

340348 get

341349 = do i <- getWord8

342350 case i of

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

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

529537

530538

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

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

532540 put x

533− = case x of

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

542+ case x of

534543 P x1 x2 x3 -> do putWord8 0

535544 put x1

536545 put x2

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

613622

614623instance Binary CaseAlt where

615624 put x

616− = case x of

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

626+ case x of

617627 ConCase x1 x2 x3 x4 -> do putWord8 0

618628 put x1

619629 put x2

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

642652

643653instance Binary Def where

644654 put x

645− = case x of

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

656+ case x of

646657 Function x1 x2 -> do putWord8 0

647658 put x1

648659 put x2

649660 TyDecl x1 x2 -> do putWord8 1

650661 put x1

651662 put x2

652− Operator x1 x2 x3 -> do putWord8 2

653− put x1

654− put x2

655− put x3

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

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

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

657666 do putWord8 3

658667 put x1

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

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

751760

752761instance 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)

754− = do put x1

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" #-}

764+ do put x1

755765 put x2

756766 put x3

757767 put x4