449bb27 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Fix allocation of big integers

commit449bb278f1aed8a9a41ac22cf825d3e65f6dc21d authorEdwin Brady <ecb10@st-andrews.ac.uk> dateWed 14 Nov 2012, 16:30 (14 years ago) parentf9678b7

3 files changed+70−39

compare with master

unifiedsplit

rts/idris_gmp.c+26−19 src/Core/CaseTree.hs+18−13 src/IRTS/Compiler.hs+26−7

rts/idris_gmp.c+26−19

@@ -9,10 +9,11 @@ VAL MKBIGI(int val) {

1010VAL MKBIGC(VM* vm, char* val) {

1111 mpz_t* bigint;

12− // FIXME! what if GC happens after cl allocation?

13− VAL cl = allocate(vm, sizeof(ClosureType) + sizeof(void*), 0);

14− bigint = allocate(vm, sizeof(mpz_t), 0);

15−

12+

13+ VAL cl = allocate(vm, sizeof(ClosureType) + sizeof(void*) +

14+ sizeof(mpz_t), 0);

15+ bigint = (mpz_t*)(((char*)cl) + sizeof(ClosureType) + sizeof(void*));

16+

1617 mpz_init(*bigint);

1718 mpz_set_str(*bigint, val, 10);

1819

@@ -24,9 +25,9 @@ VAL MKBIGC(VM* vm, char* val) {

2425

2526VAL MKBIGM(VM* vm, void* big) {

2627 mpz_t* bigint;

27− // FIXME! what if GC happens after cl allocation?

28− VAL cl = allocate(vm, sizeof(ClosureType) + sizeof(void*), 0);

29− bigint = allocate(vm, sizeof(mpz_t), 0);

28+ VAL cl = allocate(vm, sizeof(ClosureType) + sizeof(void*) +

29+ sizeof(mpz_t), 0);

30+ bigint = (mpz_t*)(((char*)cl) + sizeof(ClosureType) + sizeof(void*));

3031

3132 mpz_init(*bigint);

3233 mpz_set(*bigint, *((mpz_t*)big));

@@ -39,8 +40,9 @@ VAL MKBIGM(VM* vm, void* big) {

3940

4041VAL MKBIGMc(VM* vm, void* big) {

4142 mpz_t* bigint;

42− VAL cl = allocate(vm, sizeof(ClosureType) + sizeof(void*), 1);

43− bigint = allocate(vm, sizeof(mpz_t), 1);

43+ VAL cl = allocate(vm, sizeof(ClosureType) + sizeof(void*) +

44+ sizeof(mpz_t), 0);

45+ bigint = (mpz_t*)(((char*)cl) + sizeof(ClosureType) + sizeof(void*));

4446

4547 mpz_init(*bigint);

4648 mpz_set(*bigint, *((mpz_t*)big));

@@ -54,8 +56,9 @@ VAL MKBIGMc(VM* vm, void* big) {

5456VAL GETBIG(VM * vm, VAL x) {

5557 if (ISINT(x)) {

5658 mpz_t* bigint;

57− VAL cl = allocate(vm, sizeof(ClosureType) + sizeof(void*), 0);

58− bigint = allocate(vm, sizeof(mpz_t), 0);

59+ VAL cl = allocate(vm, sizeof(ClosureType) + sizeof(void*) +

60+ sizeof(mpz_t), 0);

61+ bigint = (mpz_t*)(((char*)cl) + sizeof(ClosureType) + sizeof(void*));

5962

6063 mpz_init(*bigint);

6164 mpz_set_si(*bigint, GETINT(x));

@@ -71,8 +74,9 @@ VAL GETBIG(VM * vm, VAL x) {

7174

7275VAL bigAdd(VM* vm, VAL x, VAL y) {

7376 mpz_t* bigint;

74− VAL cl = allocate(vm, sizeof(ClosureType) + sizeof(void*), 0);

75− bigint = allocate(vm, sizeof(mpz_t), 0);

77+ VAL cl = allocate(vm, sizeof(ClosureType) + sizeof(void*) +

78+ sizeof(mpz_t), 0);

79+ bigint = (mpz_t*)(((char*)cl) + sizeof(ClosureType) + sizeof(void*));

7680 mpz_add(*bigint, GETMPZ(x), GETMPZ(y));

7781 SETTY(cl, BIGINT);

7882 cl -> info.ptr = (void*)bigint;

@@ -81,8 +85,9 @@ VAL bigAdd(VM* vm, VAL x, VAL y) {

8185

8286VAL bigSub(VM* vm, VAL x, VAL y) {

8387 mpz_t* bigint;

84− VAL cl = allocate(vm, sizeof(ClosureType) + sizeof(void*), 0);

85− bigint = allocate(vm, sizeof(mpz_t), 0);

88+ VAL cl = allocate(vm, sizeof(ClosureType) + sizeof(void*) +

89+ sizeof(mpz_t), 0);

90+ bigint = (mpz_t*)(((char*)cl) + sizeof(ClosureType) + sizeof(void*));

8691 mpz_sub(*bigint, GETMPZ(x), GETMPZ(y));

8792 SETTY(cl, BIGINT);

8893 cl -> info.ptr = (void*)bigint;

@@ -91,8 +96,9 @@ VAL bigSub(VM* vm, VAL x, VAL y) {

9196

9297VAL bigMul(VM* vm, VAL x, VAL y) {

9398 mpz_t* bigint;

94− VAL cl = allocate(vm, sizeof(ClosureType) + sizeof(void*), 0);

95− bigint = allocate(vm, sizeof(mpz_t), 0);

99+ VAL cl = allocate(vm, sizeof(ClosureType) + sizeof(void*) +

100+ sizeof(mpz_t), 0);

101+ bigint = (mpz_t*)(((char*)cl) + sizeof(ClosureType) + sizeof(void*));

96102 mpz_mul(*bigint, GETMPZ(x), GETMPZ(y));

97103 SETTY(cl, BIGINT);

98104 cl -> info.ptr = (void*)bigint;

@@ -101,8 +107,9 @@ VAL bigMul(VM* vm, VAL x, VAL y) {

101107

102108VAL bigDiv(VM* vm, VAL x, VAL y) {

103109 mpz_t* bigint;

104− VAL cl = allocate(vm, sizeof(ClosureType) + sizeof(void*), 0);

105− bigint = allocate(vm, sizeof(mpz_t), 0);

110+ VAL cl = allocate(vm, sizeof(ClosureType) + sizeof(void*) +

111+ sizeof(mpz_t), 0);

112+ bigint = (mpz_t*)(((char*)cl) + sizeof(ClosureType) + sizeof(void*));

106113 mpz_div(*bigint, GETMPZ(x), GETMPZ(y));

107114 SETTY(cl, BIGINT);

108115 cl -> info.ptr = (void*)bigint;

src/Core/CaseTree.hs+18−13

@@ -1,6 +1,7 @@

1−{-# LANGUAGE PatternGuards #-}

1+{-# LANGUAGE PatternGuards, DeriveFunctor #-}

3−module Core.CaseTree(CaseDef(..), SC(..), CaseAlt(..), Phase(..), CaseTree,

3+module Core.CaseTree(CaseDef(..), SC, SC'(..), CaseAlt, CaseAlt'(..),

4+ Phase(..), CaseTree,

45 simpleCase, small, namesUsed, findCalls, findUsedArgs) where

67import Core.TT

@@ -13,25 +14,29 @@ import Debug.Trace

1314data CaseDef = CaseDef [Name] SC [Term]

1415 deriving Show

1516

16−data SC = Case Name [CaseAlt] -- invariant: lowest tags first

17− | ProjCase Term [CaseAlt] -- special case for projections

18− | STerm Term

19− | UnmatchedCase String -- error message

20− | ImpossibleCase -- already checked to be impossible

21− deriving (Eq, Ord)

17+data SC' t = Case Name [CaseAlt' t] -- invariant: lowest tags first

18+ | ProjCase t [CaseAlt' t] -- special case for projections

19+ | STerm t

20+ | UnmatchedCase String -- error message

21+ | ImpossibleCase -- already checked to be impossible

22+ deriving (Eq, Ord, Functor)

2223{-!

2324deriving instance Binary SC

2425!-}

2526

26−data CaseAlt = ConCase Name Int [Name] SC

27− | ConstCase Const SC

28− | DefaultCase SC

29− deriving (Show, Eq, Ord)

27+type SC = SC' Term

28+

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

30+ | ConstCase Const (SC' t)

31+ | DefaultCase (SC' t)

32+ deriving (Show, Eq, Ord, Functor)

3033{-!

3134deriving instance Binary CaseAlt

3235!-}

3336

34−instance Show SC where

37+type CaseAlt = CaseAlt' Term

38+

39+instance Show t => Show (SC' t) where

3540 show sc = show' 1 sc

3641 where

3742 show' i (Case n alts) = "case " ++ show n ++ " of\n" ++ indent i ++

src/IRTS/Compiler.hs+26−7

@@ -30,7 +30,8 @@ compile :: Target -> FilePath -> Term -> Idris ()

3030compile target f tm

3131 = do checkMVs

3232 let tmnames = namesUsed (STerm tm)

33− used <- mapM (allNames []) tmnames

33+ usedIn <- mapM (allNames []) tmnames

34+ let used = [UN "prim__subBigInt", UN "prim__addBigInt"] : usedIn

3435 defsIn <- mkDecls tm (concat used)

3536 findUnusedArgs (concat used)

3637 maindef <- irMain tm

@@ -166,6 +167,9 @@ instance ToIR (TT Name) where

166167 | (P _ (UN "trace_malloc") _, [_,t]) <- unApply tm

167168 = do t' <- ir' env t

168169 return t' -- TODO

170+-- | (P _ (NS (UN "S") ["Nat", "Prelude"]) _, [k]) <- unApply tm

171+-- = do k' <- ir' env k

172+-- return (LOp LBPlus [k', LConst (BI 1)])

169173 | (P (DCon t a) n _, args) <- unApply tm

170174 = irCon env t a n args

171175 | (P _ n _, args) <- unApply tm

@@ -187,6 +191,8 @@ instance ToIR (TT Name) where

187191 where mkUnused u i [] = []

188192 mkUnused u i (x : xs) | i `elem` u = LNothing : mkUnused u (i + 1) xs

189193 | otherwise = x : mkUnused u (i + 1) xs

194+-- ir' env (P _ (NS (UN "O") ["Nat", "Prelude"]) _)

195+-- = return $ LConst (BI 0)

190196 ir' env (P _ n _) = return $ LV (Glob n)

191197 ir' env (V i) | i < length env = return $ LV (Glob (env!!i))

192198 | otherwise = error $ "IR fail " ++ show i ++ " " ++ show tm

@@ -249,6 +255,9 @@ mkIty "FString" = FString

249255mkIty "FPtr" = FPtr

250256mkIty "FUnit" = FUnit

251257

258+zname = NS (UN "O") ["Nat","Prelude"]

259+sname = NS (UN "S") ["Nat","Prelude"]

260+

252261instance ToIR ([Name], SC) where

253262 ir (args, tree) = do logLvl 3 $ "Compiling " ++ show args ++ "\n" ++ show tree

254263 tree' <- ir tree

@@ -259,26 +268,36 @@ instance ToIR SC where

259268

260269 ir' (STerm t) = ir t

261270 ir' (UnmatchedCase str) = return $ LError str

262− ir' (ProjCase tm alts) = do alts' <- mapM mkIRAlt alts

271+ ir' (ProjCase tm alts) = do alts' <- mapM (mkIRAlt tm) alts

263272 tm' <- ir tm

264273 return $ LCase tm' alts'

265− ir' (Case n alts) = do alts' <- mapM mkIRAlt alts

274+ ir' (Case n alts) = do alts' <- mapM (mkIRAlt (P Bound n Erased)) alts

266275 return $ LCase (LV (Glob n)) alts'

267276 ir' ImpossibleCase = return LNothing

268277

269− mkIRAlt (ConCase n t args rhs)

278+ -- special cases for O and S

279+ -- Needs rethink: projections make this fail

280+-- mkIRAlt n (ConCase z _ [] rhs) | z == zname

281+-- = mkIRAlt n (ConstCase (BI 0) rhs)

282+-- mkIRAlt n (ConCase s _ [arg] rhs) | s == sname

283+-- = do n' <- ir n

284+-- rhs' <- ir rhs

285+-- return $ LDefaultCase

286+-- (LLet arg (LOp LBMinus [n', LConst (BI 1)])

287+-- rhs')

288+ mkIRAlt _ (ConCase n t args rhs)

270289 = do rhs' <- ir rhs

271290 return $ LConCase (-1) n args rhs'

272− mkIRAlt (ConstCase x rhs)

291+ mkIRAlt _ (ConstCase x rhs)

273292 | matchable x

274293 = do rhs' <- ir rhs

275294 return $ LConstCase x rhs'

276295 | matchableTy x

277296 = do rhs' <- ir rhs

278297 return $ LDefaultCase rhs'

279− mkIRAlt (ConstCase c rhs)

298+ mkIRAlt _ (ConstCase c rhs)

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

281− mkIRAlt (DefaultCase rhs)

300+ mkIRAlt _ (DefaultCase rhs)

282301 = do rhs' <- ir rhs

283302 return $ LDefaultCase rhs'

284303