93992c3 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Compile Nat as Int, (and plus/mult/fromInteger)

Currently done as a special case transformation - we should provide syntax eventually so that any desired optimisation can be done as transformations in patterns/terms.

commit93992c3255242830e4e4bee14c6ce11b776ceb41 authorEdwin Brady <ecb10@st-andrews.ac.uk> dateFri 13 Sep 2013, 18:29 (13 years ago) parent65ee53e

8 files changed+89−18

compare with master

unifiedsplit

lib/Prelude/Nat.idr+15−12 src/Core/CaseTree.hs+32−2 src/Core/Evaluate.hs+9−1 src/IRTS/Compiler.hs+6 src/IRTS/Defunctionalise.hs+2−1 src/IRTS/Java/Mangling.hs+1 src/Idris/DataOpts.hs+17−1 src/Idris/IBC.hs+7−1

lib/Prelude/Nat.idr+15−12

@@ -36,6 +36,19 @@ total mult : Nat -> Nat -> Nat

3636mult Z right = Z

3737mult (S left) right = plus right $ mult left right

3838

39+%assert_total

40+fromIntegerNat : Integer -> Nat

41+fromIntegerNat 0 = Z

42+fromIntegerNat n =

43+ if (n > 0) then

44+ S (fromIntegerNat (n - 1))

45+ else

46+ Z

47+

48+toIntegerNat : Nat -> Integer

49+toIntegerNat Z = 0

50+toIntegerNat (S k) = 1 + toIntegerNat k

51+

3952total minus : Nat -> Nat -> Nat

4053minus Z right = Z

4154minus left Z = left

@@ -108,8 +121,7 @@ instance Eq Nat where

108121 _ == _ = False

109122

110123instance Cast Nat Integer where

111− cast Z = 0

112− cast (S k) = 1 + cast k

124+ cast = toIntegerNat

113125

114126instance Ord Nat where

115127 compare Z Z = EQ

@@ -124,16 +136,7 @@ instance Num Nat where

124136

125137 abs x = x

126138

127− fromInteger x = fromInteger' x

128− where

129− %assert_total

130− fromInteger' : Integer -> Nat

131− fromInteger' 0 = Z

132− fromInteger' n =

133− if (n > 0) then

134− S (fromInteger' (n - 1))

135− else

136− Z

139+ fromInteger = fromIntegerNat

137140

138141instance Cast Integer Nat where

139142 cast = fromInteger

src/Core/CaseTree.hs+32−2

@@ -29,6 +29,7 @@ type SC = SC' Term

2929data CaseAlt' t = ConCase Name Int [Name] (SC' t)

3030 | FnCase Name [Name] (SC' t) -- ^ reflection function

3131 | ConstCase Const (SC' t)

32+ | SucCase Name (SC' t)

3233 | DefaultCase (SC' t)

3334 deriving (Show, Eq, Ord, Functor)

3435{-!

@@ -58,6 +59,8 @@ instance Show t => Show (SC' t) where

5859 ++ show' (i+1) sc

5960 showA i (ConstCase t sc)

6061 = show t ++ " => " ++ show' (i+1) sc

62+ showA i (SucCase n sc)

63+ = show n ++ "+1 => " ++ show' (i+1) sc

6164 showA i (DefaultCase sc)

6265 = "_ => " ++ show' (i+1) sc

6366

@@ -76,6 +79,7 @@ instance TermSize CaseAlt where

7679 termsize n (ConCase _ _ _ s) = termsize n s

7780 termsize n (FnCase _ _ s) = termsize n s

7881 termsize n (ConstCase _ s) = termsize n s

82+ termsize n (SucCase _ s) = termsize n s

7983 termsize n (DefaultCase s) = termsize n s

8084

8185-- simple terms can be inlined trivially - good for primitives in particular

@@ -98,6 +102,7 @@ namesUsed sc = nub $ nu' [] sc where

98102 nua ps (ConCase n i args sc) = nub (nu' (ps ++ args) sc) \\ args

99103 nua ps (FnCase n args sc) = nub (nu' (ps ++ args) sc) \\ args

100104 nua ps (ConstCase _ sc) = nu' ps sc

105+ nua ps (SucCase _ sc) = nu' ps sc

101106 nua ps (DefaultCase sc) = nu' ps sc

102107

103108 nut ps (P _ n _) | n `elem` ps = []

@@ -122,6 +127,7 @@ findCalls sc topargs = nub $ nu' topargs sc where

122127 nua ps (ConCase n i args sc) = nub (nu' (ps ++ args) sc)

123128 nua ps (FnCase n args sc) = nub (nu' (ps ++ args) sc)

124129 nua ps (ConstCase _ sc) = nu' ps sc

130+ nua ps (SucCase _ sc) = nu' ps sc

125131 nua ps (DefaultCase sc) = nu' ps sc

126132

127133 nut ps (P Ref n _) | n `elem` ps = []

@@ -166,6 +172,7 @@ findAllUsedArgs sc topargs = filter (\x -> x `elem` topargs) (nu' sc) where

166172 nua (ConCase n i args sc) = nu' sc

167173 nua (FnCase n args sc) = nu' sc

168174 nua (ConstCase _ sc) = nu' sc

175+ nua (SucCase _ sc) = nu' sc

169176 nua (DefaultCase sc) = nu' sc

170177

171178data Phase = CompileTime | RunTime

@@ -212,11 +219,13 @@ simpleCase tc cover reflect phase fc cs

212219 acc [] n = Error (Inaccessible n)

213220 acc (PV x : xs) n | x == n = OK ()

214221 acc (PCon _ _ ps : xs) n = acc (ps ++ xs) n

222+ acc (PSuc p : xs) n = acc (p : xs) n

215223 acc (_ : xs) n = acc xs n

216224

217225data Pat = PCon Name Int [Pat]

218226 | PConst Const

219227 | PV Name

228+ | PSuc Pat -- special case for n+1 on Integer

220229 | PReflected Name [Pat]

221230 | PAny

222231 deriving Show

@@ -234,6 +243,11 @@ toPat reflect tc tms = evalState (mapM (\x -> toPat' x []) tms) []

234243 where

235244 toPat' (P (DCon t a) n _) args = do args' <- mapM (\x -> toPat' x []) args

236245 return $ PCon n t args'

246+ -- n + 1

247+ toPat' (P _ (UN "prim__addBigInt") _)

248+ [p, Constant (BI 1)]

249+ = do p' <- toPat' p []

250+ return $ PSuc p'

237251 -- Typecase

238252 toPat' (P (TCon t a) n _) args | tc

239253 = do args' <- mapM (\x -> toPat' x []) args

@@ -280,6 +294,7 @@ isVarPat _ = False

280294

281295isConPat (PCon _ _ _ : ps, _) = True

282296isConPat (PReflected _ _ : ps, _) = True

297+isConPat (PSuc _ : ps, _) = True

283298isConPat (PConst _ : ps, _) = True

284299isConPat _ = False

285300

@@ -338,11 +353,13 @@ mixture vs (Vars ms : ps) err = do fallthrough <- mixture vs ps err

338353

339354data ConType = CName Name Int -- named constructor

340355 | CFn Name -- reflected function name

356+ | CSuc -- n+1

341357 | CConst Const -- constant, not implemented yet

342− deriving Eq

358+ deriving (Show, Eq)

343359

344360data Group = ConGroup ConType -- Constructor

345361 [([Pat], Clause)] -- arguments and rest of alternative

362+ deriving Show

346363

347364conRule :: [Name] -> [Clause] -> SC -> State CS SC

348365conRule (v:vs) cs err = do groups <- groupCons cs

@@ -361,6 +378,10 @@ caseGroups (v:vs) gs err = do g <- altGroups gs

361378 = do g <- altFnGroup n args

362379 rest <- altGroups cs

363380 return (g : rest)

381+ altGroups (ConGroup CSuc args : cs)

382+ = do g <- altSucGroup args

383+ rest <- altGroups cs

384+ return (g : rest)

364385 altGroups (ConGroup (CConst c) args : cs)

365386 = do g <- altConstGroup c args

366387 rest <- altGroups cs

@@ -372,6 +393,9 @@ caseGroups (v:vs) gs err = do g <- altGroups gs

372393 altFnGroup n gs = do (newArgs, nextCs) <- argsToAlt gs

373394 matchCs <- match (newArgs ++ vs) nextCs err

374395 return $ FnCase n newArgs matchCs

396+ altSucGroup gs = do ([newArg], nextCs) <- argsToAlt gs

397+ matchCs <- match (newArg:vs) nextCs err

398+ return $ SucCase newArg matchCs

375399 altConstGroup n gs = do (_, nextCs) <- argsToAlt gs

376400 matchCs <- match vs nextCs err

377401 return $ ConstCase n matchCs

@@ -411,6 +435,7 @@ groupCons cs = gc [] cs

411435 addGroup p ps res acc = case p of

412436 PCon con i args -> return $ addg (CName con i) args (ps, res) acc

413437 PConst cval -> return $ addConG cval (ps, res) acc

438+ PSuc n -> return $ addg CSuc [n] (ps, res) acc

414439 PReflected fn args -> return $ addg (CFn fn) args (ps, res) acc

415440 pat -> fail $ show pat ++ " is not a constructor or constant (can't happen)"

416441

@@ -423,7 +448,8 @@ groupCons cs = gc [] cs

423448 addConG con res [] = [ConGroup (CConst con) [([], res)]]

424449 addConG con res (g@(ConGroup (CConst n) cs) : gs)

425450 | con == n = ConGroup (CConst n) (cs ++ [([], res)]) : gs

426− | otherwise = g : addConG con res gs

451+-- | otherwise = g : addConG con res gs

452+ addConG con res (g : gs) = g : addConG con res gs

427453

428454varRule :: [Name] -> [Clause] -> SC -> State CS SC

429455varRule (v : vs) alts err =

@@ -448,6 +474,7 @@ depatt ns tm = dp [] tm

448474 dpa ms x (FnCase n args sc)

449475 = FnCase n args (dp ((x, (n, args)) : ms) sc)

450476 dpa ms x (ConstCase c sc) = ConstCase c (dp ms sc)

477+ dpa ms x (SucCase n sc) = SucCase n (dp ms sc)

451478 dpa ms x (DefaultCase sc) = DefaultCase (dp ms sc)

452479

453480 applyMaps ms f@(App _ _)

@@ -478,6 +505,7 @@ prune proj (Case n alts)

478505 where pruneAlt (ConCase cn i ns sc) = ConCase cn i ns (prune proj sc)

479506 pruneAlt (FnCase cn ns sc) = FnCase cn ns (prune proj sc)

480507 pruneAlt (ConstCase c sc) = ConstCase c (prune proj sc)

508+ pruneAlt (SucCase n sc) = SucCase n (prune proj sc)

481509 pruneAlt (DefaultCase sc) = DefaultCase (prune proj sc)

482510

483511 notErased (DefaultCase (STerm Erased)) = False

@@ -503,6 +531,8 @@ prune proj (Case n alts)

503531 = FnCase cn args (projRep arg n i rhs)

504532 projRepAlt arg n i (ConstCase t rhs)

505533 = ConstCase t (projRep arg n i rhs)

534+ projRepAlt arg n i (SucCase sn rhs)

535+ = SucCase sn (projRep arg n i rhs)

506536 projRepAlt arg n i (DefaultCase rhs)

507537 = DefaultCase (projRep arg n i rhs)

508538

src/Core/Evaluate.hs+9−1

@@ -343,10 +343,13 @@ eval traceon ctxt ntimes genv tm opts = ev ntimes [] True [] tm where

343343 | Just (ns, sc) <- findTag i alts = return $ Just (updateAmap (zip ns args) amap, sc)

344344 | Just v <- findDefault alts = return $ Just (amap, v)

345345 chooseAlt env _ (VP (TCon i a) _ _, args) alts amap

346− | Just (ns, sc) <- findTag i alts = return $ Just (updateAmap (zip ns args) amap, sc)

346+ | Just (ns, sc) <- findTag i alts

347+ = return $ Just (updateAmap (zip ns args) amap, sc)

347348 | Just v <- findDefault alts = return $ Just (amap, v)

348349 chooseAlt env _ (VConstant c, []) alts amap

349350 | Just v <- findConst c alts = return $ Just (amap, v)

351+ | Just (n', sub, sc) <- findSuc c alts

352+ = return $ Just (updateAmap [(n',sub)] amap, sc)

350353 | Just v <- findDefault alts = return $ Just (amap, v)

351354 chooseAlt env _ (VP _ n _, args) alts amap

352355 | Just (ns, sc) <- findFn n alts = return $ Just (updateAmap (zip ns args) amap, sc)

@@ -381,6 +384,11 @@ eval traceon ctxt ntimes genv tm opts = ev ntimes [] True [] tm where

381384 findDefault (DefaultCase sc : xs) = Just sc

382385 findDefault (_ : xs) = findDefault xs

383386

387+ findSuc c [] = Nothing

388+ findSuc (BI val) (SucCase n sc : _)

389+ | val /= 0 = Just (n, VConstant (BI (val - 1)), sc)

390+ findSuc c (_ : xs) = findSuc c xs

391+

384392 findConst c [] = Nothing

385393 findConst c (ConstCase c' v : xs) | c == c' = Just v

386394 findConst (AType (ATInt ITNative)) (ConCase n 1 [] v : xs) = Just v

src/IRTS/Compiler.hs+6

@@ -379,6 +379,12 @@ instance ToIR SC where

379379 | matchableTy x

380380 = do rhs' <- ir rhs

381381 return $ LDefaultCase rhs'

382+ mkIRAlt (P _ orig _) (SucCase n rhs)

383+ = do rhs' <- ir rhs

384+ return $ LDefaultCase (LLet n (LOp (LMinus (ATInt ITBig))

385+ [LV (Glob orig),

386+ LConst (BI 1)]) rhs')

387+-- return $ LSucCase n rhs'

382388 mkIRAlt _ (ConstCase c rhs)

383389 = fail $ "Can't match on (" ++ show c ++ ")"

384390 mkIRAlt _ (DefaultCase rhs)

src/IRTS/Defunctionalise.hs+2−1

@@ -286,13 +286,14 @@ mkBigCase cn max arg branches

286286 tagOrd (DConCase t _ _ _) (DConCase t' _ _ _) = compare t t'

287287 tagOrd (DConstCase c _) (DConstCase c' _) = compare c c'

288288 tagOrd (DDefaultCase _) (DDefaultCase _) = EQ

289+

289290 tagOrd (DConCase _ _ _ _) (DDefaultCase _) = LT

290291 tagOrd (DConCase _ _ _ _) (DConstCase _ _) = LT

291292 tagOrd (DConstCase _ _) (DDefaultCase _) = LT

293+

292294 tagOrd (DDefaultCase _) (DConCase _ _ _ _) = GT

293295 tagOrd (DConstCase _ _) (DConCase _ _ _ _) = GT

294296 tagOrd (DDefaultCase _) (DConstCase _ _) = GT

295−

296297

297298groupsOf :: Int -> [DAlt] -> [[DAlt]]

298299groupsOf x [] = []

src/IRTS/Java/Mangling.hs+1

@@ -18,6 +18,7 @@ import Language.Java.Syntax hiding (Name)

1818import qualified Language.Java.Syntax as J

1919

2020import System.FilePath

21+import Debug.Trace

2122

2223prefixCallNamespaces :: Ident -> SDecl -> SDecl

2324prefixCallNamespaces name (SFun fname args i e) =

src/Idris/DataOpts.hs+17−1

@@ -214,13 +214,23 @@ applyDataOpt oi n args

214214-- Run-time: do everything

215215

216216instance Optimisable (TT Name) where

217+ applyOpts (P _ (NS (UN "plus") ["Nat","Prelude"]) _)

218+ = return (P Ref (UN "prim__addBigInt") Erased)

219+ applyOpts (P _ (NS (UN "mult") ["Nat","Prelude"]) _)

220+ = return (P Ref (UN "prim__mulBigInt") Erased)

221+ applyOpts (App (P _ (NS (UN "fromIntegerNat") ["Nat","Prelude"]) _) x)

222+ = applyOpts x

223+ applyOpts (P _ (NS (UN "fromIntegerNat") ["Nat","Prelude"]) _)

224+ = return (App (P Ref (NS (UN "id") ["Builtins"]) Erased) Erased)

225+ applyOpts (P _ (NS (UN "toIntegerNat") ["Nat","Prelude"]) _)

226+ = return (App (P Ref (NS (UN "id") ["Builtins"]) Erased) Erased)

217227 applyOpts c@(P (DCon t arity) n _)

218228 = do i <- getIState

219229 case lookupCtxt n (idris_optimisation i) of

220230 (oi:_) -> return $ applyDataOptRT oi n t arity []

221231 _ -> return c

222232 applyOpts t@(App f a)

223− | (c@(P (DCon t arity) n _), args) <- unApply t -- MAGIC HERE

233+ | (c@(P (DCon t arity) n _), args) <- unApply t

224234 = do args' <- mapM applyOpts args

225235 i <- getIState

226236 case lookupCtxt n (idris_optimisation i) of

@@ -266,6 +276,12 @@ applyDataOptRT oi n tag arity args

266276 bind [] tm = tm

267277 bind (n:ns) tm = Bind n (Lam Erased) (pToV n (bind ns tm))

268278

279+ -- Nat special cases

280+ -- TODO: Would be nice if this was configurable in idris source!

281+ doOpts (NS (UN "Z") ["Nat", "Prelude"]) [] _ _ = Constant (BI 0)

282+ doOpts (NS (UN "S") ["Nat", "Prelude"]) [k] _ _

283+ = App (App (P Ref (UN "prim__addBigInt") Erased) k) (Constant (BI 1))

284+

269285 doOpts n args True f = Erased

270286 doOpts n args _ forced

271287 = let args' = filter keep (zip (map (\x -> x `elem` forced) [0..])

src/Idris/IBC.hs+7−1

@@ -23,7 +23,7 @@ import Debug.Trace

2323import Paths_idris

2424

2525ibcVersion :: Word8

26−ibcVersion = 38

26+ibcVersion = 39

2727

2828data IBCFile = IBCFile { ver :: Word8,

2929 sourcefile :: FilePath,

@@ -714,6 +714,9 @@ instance Binary CaseAlt where

714714 put x1

715715 put x2

716716 put x3

717+ SucCase x1 x2 -> do putWord8 4

718+ put x1

719+ put x2

717720 get

718721 = do i <- getWord8

719722 case i of

@@ -731,6 +734,9 @@ instance Binary CaseAlt where

731734 x2 <- get

732735 x3 <- get

733736 return (FnCase x1 x2 x3)

737+ 4 -> do x1 <- get

738+ x2 <- get

739+ return (SucCase x1 x2)

734740 _ -> error "Corrupted binary data for CaseAlt"

735741

736742instance Binary CaseDefs where