0f957f6 · Idris-dev · git.iko.soy

rts/idris_rts.c+1−1

@@ -80,7 +80,7 @@ void* allocate(VM* vm, size_t size) {

8080 void* ptr = (void*)(vm->heap_next + sizeof(size_t));

8181 *((size_t*)(vm->heap_next)) = size + sizeof(size_t);

8282 vm -> heap_next += size + sizeof(size_t);

83− bzero(ptr, size);

83+ memset(ptr, 0, size);

8484 return ptr;

8585 } else {

8686 gc(vm);

rts/idris_rts.h+1

@@ -129,6 +129,7 @@ VAL MKCON(VM* vm, VAL cl, int tag, int arity, ...);

129129

130130#define SETTAG(x, a) (x)->info.c.tag = (a)

131131#define SETARG(x, i, a) ((VAL*)((x)->info.c.args))[i] = ((VAL)(a))

132+#define GETARG(x, i) ((VAL*)((x)->info.c.args))[i]

132133

133134void PROJECT(VM* vm, VAL r, int loc, int arity);

134135void SLIDE(VM* vm, int args);

src/Core/CaseTree.hs+79−11

@@ -1,5 +1,5 @@

11module Core.CaseTree(CaseDef(..), SC(..), CaseAlt(..), CaseTree,

2− simpleCase, small, namesUsed) where

2+ simpleCase, small, namesUsed, findCalls) where

33

44import Core.TT

55

@@ -12,6 +12,7 @@ data CaseDef = CaseDef [Name] SC [Term]

1212 deriving Show

1313

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

15+ | ProjCase Term [CaseAlt] -- special case for projections

1516 | STerm Term

1617 | UnmatchedCase String -- error message

1718 deriving (Show, Eq, Ord)

@@ -62,10 +63,51 @@ namesUsed sc = nub $ nu' [] sc where

6263 nut ps (Bind n b sc) = nut (n:ps) sc

6364 nut ps _ = []

6465

65−simpleCase :: Bool -> Bool -> FC -> [([Name], Term, Term)] -> TC CaseDef

66−simpleCase tc cover fc []

66+-- Return all called functions, and which arguments are used in each argument position

67+-- for the call, in order to help reduce compilation time, and trace all unused

68+-- arguments

69+

70+findCalls :: SC -> [Name] -> [(Name, [[Name]])]

71+findCalls sc ign = nub $ nu' ign sc where

72+ nu' ps (Case n alts) = nub (concatMap (nua (n : ps)) alts)

73+ nu' ps (STerm t) = nub $ nut ps t

74+ nu' ps _ = []

75+

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

77+ nua ps (ConstCase _ sc) = nu' ps sc

78+ nua ps (DefaultCase sc) = nu' ps sc

79+

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

81+ | otherwise = [(n, [])] -- tmp

82+ nut ps (App f a) = nut ps f ++ nut ps a

83+ nut ps (Bind n (Let t v) sc) = nut ps v ++ nut (n:ps) sc

84+ nut ps (Bind n b sc) = nut (n:ps) sc

85+ nut ps _ = []

86+

87+-- Find directly used arguments (i.e. used but not in function calls)

88+{-

89+findUsedArgs :: SC -> [Name] -> [(Name, [[Name]])]

90+findUsedArgs sc ign = nub $ nu' ign sc where

91+ nu' ps (Case n alts) = nub (concatMap (nua (n : ps)) alts)

92+ nu' ps (STerm t) = nub $ nut ps t

93+ nu' ps _ = []

94+

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

96+ nua ps (ConstCase _ sc) = nu' ps sc

97+ nua ps (DefaultCase sc) = nu' ps sc

98+

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

100+ | otherwise = [(n, [])] -- tmp

101+ nut ps (App f a) = nut ps f ++ nut ps a

102+ nut ps (Bind n (Let t v) sc) = nut ps v ++ nut (n:ps) sc

103+ nut ps (Bind n b sc) = nut (n:ps) sc

104+ nut ps _ = []

105+-}

106+

107+simpleCase :: Bool -> Bool -> Bool -> FC -> [([Name], Term, Term)] -> TC CaseDef

108+simpleCase tc cover proj fc []

67109 = return $ CaseDef [] (UnmatchedCase "No pattern clauses") []

68−simpleCase tc cover fc cs

110+simpleCase tc cover proj fc cs

69111 = let pats = map (\ (avs, l, r) ->

70112 (avs, reverse (toPats tc l), (l, r))) cs

71113 chkPats = mapM chkAccessible pats in

@@ -75,7 +117,7 @@ simpleCase tc cover fc cs

75117 ns = take numargs args

76118 (tree, st) = runState

77119 (match (reverse ns) pats (defaultCase cover)) ([], numargs) in

78− return $ CaseDef ns (prune tree) (fst st)

120+ return $ CaseDef ns (prune proj tree) (fst st)

79121 Error err -> Error (At fc err)

80122 where args = map (\i -> MN i "e") [0..]

81123 defaultCase True = STerm Erased

@@ -250,19 +292,45 @@ varRule (v : vs) alts err =

250292 repVar v (PV p : ps , (lhs, res)) = (ps, (lhs, subst p (P Bound v (V 0)) res))

251293 repVar v (PAny : ps , res) = (ps, res)

252294

253−prune :: SC -> SC

254−prune (Case n alts)

295+prune :: Bool -> -- ^ Convert single brances to projections (only useful at runtime)

296+ SC -> SC

297+prune proj (Case n alts)

255298 = let alts' = map pruneAlt $

256299 filter notErased alts in

257300 case alts' of

258301 [] -> STerm Erased

302+ as@[ConCase cn i args sc] -> if proj then mkProj n 0 args sc

303+ else Case n as

259304 as -> Case n as

260− where pruneAlt (ConCase cn i ns sc) = ConCase cn i ns (prune sc)

261− pruneAlt (ConstCase c sc) = ConstCase c (prune sc)

262− pruneAlt (DefaultCase sc) = DefaultCase (prune sc)

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

306+ pruneAlt (ConstCase c sc) = ConstCase c (prune proj sc)

307+ pruneAlt (DefaultCase sc) = DefaultCase (prune proj sc)

263308

264309 notErased (DefaultCase (STerm Erased)) = False

265310 notErased _ = True

266−prune t = t

311+

312+ mkProj n i [] sc = sc

313+ mkProj n i (x : xs) sc = mkProj n (i + 1) xs (projRep x n i sc)

314+

315+ projRep :: Name -> Name -> Int -> SC -> SC

316+ projRep arg n i (Case x alts)

317+ | x == arg = ProjCase (Proj (P Bound n Erased) i)

318+ (map (projRepAlt arg n i) alts)

319+ | otherwise = Case x (map (projRepAlt arg n i) alts)

320+ projRep arg n i (ProjCase t alts)

321+ = ProjCase (projRepTm arg n i t) (map (projRepAlt arg n i) alts)

322+ projRep arg n i (STerm t) = STerm (projRepTm arg n i t)

323+ projRep arg n i c = c -- unmatched

324+

325+ projRepAlt arg n i (ConCase cn t args rhs)

326+ = ConCase cn t args (projRep arg n i rhs)

327+ projRepAlt arg n i (ConstCase t rhs)

328+ = ConstCase t (projRep arg n i rhs)

329+ projRepAlt arg n i (DefaultCase rhs)

330+ = DefaultCase (projRep arg n i rhs)

331+

332+ projRepTm arg n i t = subst arg (Proj (P Bound n Erased) i) t

333+

334+prune _ t = t

267335

268336

src/Core/Evaluate.hs+3−3

@@ -691,14 +691,14 @@ addCasedef :: Name -> Bool -> Bool -> Bool ->

691691 Type -> Context -> Context

692692addCasedef n alwaysInline tcase covering ps psrt ty uctxt

693693 = let ctxt = definitions uctxt

694− ctxt' = case (simpleCase tcase covering (FC "" 0) ps,

695− simpleCase tcase covering (FC "" 0) psrt) of

694+ ctxt' = case (simpleCase tcase covering False (FC "" 0) ps,

695+ simpleCase tcase covering True (FC "" 0) psrt) of

696696 (OK (CaseDef args sc _), OK (CaseDef args' sc' _)) ->

697697 let inl = alwaysInline || small sc' in

698698 addDef n (CaseOp inl ty ps args sc args' sc',

699699 Public, Unchecked) ctxt in

700700 uctxt { definitions = ctxt' }

701−

701+

702702addOperator :: Name -> Type -> Int -> ([Value] -> Maybe Value) -> Context -> Context

703703addOperator n ty a op uctxt

704704 = let ctxt = definitions uctxt

src/Core/TT.hs+12−1

@@ -162,6 +162,7 @@ traceWhen False _ a = a

162162data Name = UN String

163163 | NS Name [String] -- root, namespaces

164164 | MN Int String

165+ | NErased -- name of somethng which is never used in scope

165166 deriving (Eq, Ord)

166167{-!

167168deriving instance Binary Name

@@ -171,6 +172,7 @@ instance Sized Name where

171172 size (UN n) = 1

172173 size (NS n els) = 1 + length els

173174 size (MN i n) = 1

175+ size NErased = 1

174176

175177instance Pretty Name where

176178 pretty (UN n) = text n

@@ -181,7 +183,7 @@ instance Show Name where

181183 show (UN n) = n

182184 show (NS n s) = showSep "." (reverse s) ++ "." ++ show n

183185 show (MN i s) = "{" ++ s ++ show i ++ "}"

184−

186+ show NErased = "_"

185187

186188-- Contexts allow us to map names to things. A root name maps to a collection

187189-- of things in different namespaces with that name.

@@ -410,6 +412,7 @@ data TT n = P NameType n (TT n) -- embed type

410412 | Bind n (Binder (TT n)) (TT n)

411413 | App (TT n) (TT n) -- function, function type, arg

412414 | Constant Const

415+ | Proj (TT n) Int -- argument projection; runtime only

413416 | Erased

414417 | Set UExp

415418 deriving (Ord, Functor)

@@ -458,6 +461,7 @@ instance Eq n => Eq (TT n) where

458461 (==) (App fx ax) (App fy ay) = fx == fy && ax == ay

459462 (==) (Set _) (Set _) = True -- deal with constraints later

460463 (==) (Constant x) (Constant y) = x == y

464+ (==) (Proj x i) (Proj y j) = x == y && i == j

461465 (==) Erased _ = True

462466 (==) _ Erased = True

463467 (==) _ _ = False

@@ -487,6 +491,7 @@ instantiate e = subst 0 where

487491 subst i (V x) | i == x = e

488492 subst i (Bind x b sc) = Bind x (fmap (subst i) b) (subst (i+1) sc)

489493 subst i (App f a) = App (subst i f) (subst i a)

494+ subst i (Proj x idx) = Proj (subst i x) idx

490495 subst i t = t

491496

492497pToV :: Eq n => n -> TT n -> TT n

@@ -496,6 +501,7 @@ pToV' n i (Bind x b sc)

496501 | n == x = Bind x (fmap (pToV' n i) b) sc

497502 | otherwise = Bind x (fmap (pToV' n i) b) (pToV' n (i+1) sc)

498503pToV' n i (App f a) = App (pToV' n i f) (pToV' n i a)

504+pToV' n i (Proj t idx) = Proj (pToV' n i t) idx

499505pToV' n i t = t

500506

501507-- Convert several names. First in the list comes out as V 0

@@ -537,6 +543,7 @@ noOccurrence n t = no' 0 t

537543 noB' i (Guess t v) = no' i t && no' i v

538544 noB' i b = no' i (binderTy b)

539545 no' i (App f a) = no' i f && no' i a

546+ no' i (Proj x _) = no' i x

540547 no' i _ = True

541548

542549-- Returns all names used free in the term

@@ -547,6 +554,7 @@ freeNames (Bind n (Let t v) sc) = nub $ freeNames v ++ (freeNames sc \\ [n])

547554 ++ freeNames t

548555freeNames (Bind n b sc) = nub $ freeNames (binderTy b) ++ (freeNames sc \\ [n])

549556freeNames (App f a) = nub $ freeNames f ++ freeNames a

557+freeNames (Proj x i) = nub $ freeNames x

550558freeNames _ = []

551559

552560-- Return the arity of a (normalised) type

@@ -669,6 +677,8 @@ prettyEnv env t = prettyEnv' env t False

669677 bracket p 2 $ prettySb env n b debug <> prettySe 10 ((n, b):env) sc debug

670678 prettySe p env (App f a) debug =

671679 bracket p 1 $ prettySe 1 env f debug <+> prettySe 0 env a debug

680+ prettySe p env (Proj x i) debug =

681+ prettySe 1 env x debug <+> text ("!" ++ show i)

672682 prettySe p env (Constant c) debug = pretty c

673683 prettySe p env Erased debug = text "[_]"

674684 prettySe p env (Set i) debug = text "Set" <+> (text . show $ i)

@@ -699,6 +709,7 @@ showEnv' env t dbg = se 10 env t where

699709 | noOccurrence n sc && not dbg = bracket p 2 $ se 1 env t ++ " -> " ++ se 10 ((n,b):env) sc

700710 se p env (Bind n b sc) = bracket p 2 $ sb env n b ++ se 10 ((n,b):env) sc

701711 se p env (App f a) = bracket p 1 $ se 1 env f ++ " " ++ se 0 env a

712+ se p env (Proj x i) = se 1 env x ++ "!" ++ show i

702713 se p env (Constant c) = show c

703714 se p env Erased = "[__]"

704715 se p env (Set i) = "Set " ++ show i

src/IRTS/Bytecode.hs+4

@@ -30,6 +30,7 @@ data BC = ASSIGN Reg Reg

3030 | MKCON Reg Int [Reg]

3131 | CASE Reg [(Int, [BC])] (Maybe [BC])

3232 | PROJECT Reg Int Int -- get all args from reg, put them from Int onwards

33+ | PROJECTINTO Reg Reg Int -- project argument from one reg into another

3334 | CONSTCASE Reg [(Const, [BC])] (Maybe [BC])

3435 | CALL Name

3536 | TAILCALL Name

@@ -43,6 +44,7 @@ data BC = ASSIGN Reg Reg

4344 | BASETOP Int -- set BASE = TOP + n

4445 | STOREOLD -- set OLDBASE = BASE

4546 | OP Reg PrimFn [Reg]

47+ | NULL Reg -- clear reg

4648 | ERROR String

4749 deriving Show

4850

@@ -72,10 +74,12 @@ bc reg (SForeign l t fname args) r

7274bc reg (SLet (Loc i) e sc) r = bc (L i) e False ++ bc reg sc r

7375bc reg (SCon i _ vs) r = MKCON reg i (map getL vs) : clean r

7476 where getL (Loc x) = L x

77+bc reg (SProj (Loc l) i) r = PROJECTINTO reg (L l) i : clean r

7578bc reg (SConst i) r = ASSIGNCONST reg i : clean r

7679bc reg (SOp p vs) r = OP reg p (map getL vs) : clean r

7780 where getL (Loc x) = L x

7881bc reg (SError str) r = [ERROR str]

82+bc reg SNothing r = NULL reg : clean r

7983bc reg (SCase (Loc l) alts) r

8084 | isConst alts = constCase reg (L l) alts r

8185 | otherwise = conCase reg (L l) alts r

src/IRTS/CodegenC.hs+3

@@ -112,6 +112,8 @@ bcc i (MKCON l tag args)

112112

113113bcc i (PROJECT l loc a) = indent i ++ "PROJECT(vm, " ++ creg l ++ ", " ++ show loc ++

114114 ", " ++ show a ++ ");\n"

115+bcc i (PROJECTINTO r t idx)

116+ = indent i ++ creg r ++ " = GETARG(" ++ creg t ++ ", " ++ show idx ++ ");\n"

115117bcc i (CASE r code def)

116118 = indent i ++ "switch(TAG(" ++ creg r ++ ")) {\n" ++

117119 concatMap (showCase i) code ++

@@ -149,6 +151,7 @@ bcc i (FOREIGNCALL l LANG_C rty fn args)

149151 c_irts rty (creg l ++ " = ")

150152 (fn ++ "(" ++ showSep "," (map fcall args) ++ ")") ++ ";\n"

151153 where fcall (t, arg) = irts_c t (creg arg)

154+bcc i (NULL r) = indent i ++ creg r ++ " = NULL;\n" -- clear, so it'll be GCed

152155bcc i (ERROR str) = indent i ++ "fprintf(stderr, " ++ show str ++ "); assert(0); exit(-1);"

153156-- bcc i _ = indent i ++ "// not done yet\n"

154157

src/IRTS/Compiler.hs+13−10

@@ -72,7 +72,7 @@ allNames :: [Name] -> Name -> Idris [Name]

7272allNames ns n | n `elem` ns = return []

7373allNames ns n = do i <- get

7474 case lookupCtxt Nothing n (idris_callgraph i) of

75− [ns'] -> do more <- mapM (allNames (n:ns)) ns'

75+ [ns'] -> do more <- mapM (allNames (n:ns)) (map fst (calls ns'))

7676 return (nub (n : concat more))

7777 _ -> return [n]

7878

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

157157 v' <- ir' env v

158158 return $ LLet n v' sc'

159159 ir' env (Bind _ _ _) = return $ LConst (I 424242)

160+ ir' env (Proj t i) = do t' <- ir' env t

161+ return $ LProj t' i

160162 ir' env (Constant c) = return $ LConst c

161163 ir' env _ = return $ LError "Impossible"

162164

@@ -207,11 +209,16 @@ instance ToIR ([Name], SC) where

207209 return $ LLam args tree'

208210

209211instance ToIR SC where

210− ir (STerm t) = ir t

211− ir (UnmatchedCase str) = return $ LError str

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

213− return $ LCase (LV (Glob n)) alts'

214− where

212+ ir t = ir' t where

213+

214+ ir' (STerm t) = ir t

215+ ir' (UnmatchedCase str) = return $ LError str

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

217+ tm' <- ir tm

218+ return $ LCase tm' alts'

219+ ir' (Case n alts) = do alts' <- mapM mkIRAlt alts

220+ return $ LCase (LV (Glob n)) alts'

221+

215222 mkIRAlt (ConCase n t args rhs)

216223 = do rhs' <- ir rhs

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

@@ -227,7 +234,3 @@ instance ToIR SC where

227234 = do rhs' <- ir rhs

228235 return $ LDefaultCase rhs'

229236

230−

231−

232−

233−

src/IRTS/Defunctionalise.hs+6−3

@@ -11,12 +11,14 @@ import Data.List

1111data DExp = DV LVar

1212 | DApp Bool Name [DExp] -- True = tail call

1313 | DLet Name DExp DExp -- name just for pretty printing

14− | DLam [Name] DExp -- lambda, lifted out before compiling

14+ | DProj DExp Int

1515 | DC Int Name [DExp]

1616 | DCase DExp [DAlt]

1717 | DConst Const

1818 | DForeign FLang FType String [(FType, DExp)]

1919 | DOp PrimFn [DExp]

20+ | DNothing -- erased value, can be compiled to anything since it'll never

21+ -- be inspected

2022 | DError String

2123 deriving Eq

2224

@@ -85,11 +87,13 @@ addApps defs (n, LFun _ args e) = (n, DFun n args (aa args e))

8587 aa env (LForce e) = eEVAL (aa env e)

8688 aa env (LLet n v sc) = DLet n (aa env v) (aa (n : env) sc)

8789 aa env (LCon i n args) = DC i n (map (aa env) args)

90+ aa env (LProj t i) = DProj (eEVAL (aa env t)) i

8891 aa env (LCase e alts) = DCase (eEVAL (aa env e)) (map (aaAlt env) alts)

8992 aa env (LConst c) = DConst c

9093 aa env (LForeign l t n args) = DForeign l t n (map (aaF env) args)

9194 aa env (LOp LFork args) = DOp LFork (map (aa env) args)

9295 aa env (LOp f args) = DOp f (map (eEVAL . (aa env)) args)

96+ aa env LNothing = DNothing

9397 aa env (LError e) = DError e

9498

9599 aaF env (t, e) = (t, eEVAL (aa env e))

@@ -176,9 +180,8 @@ instance Show DExp where

176180 showSep ", " (map (show' env) args) ++")"

177181 show' env (DLet n v e) = "let " ++ show n ++ " = " ++ show' env v ++ " in " ++

178182 show' (env ++ [show n]) e

179− show' env (DLam args e) = "\\ " ++ showSep "," (map show args) ++ " => " ++

180− show' (env ++ (map show args)) e

181183 show' env (DC i n args) = show n ++ ")" ++ showSep ", " (map (show' env) args) ++ ")"

184+ show' env (DProj t i) = show t ++ "!" ++ show i

182185 show' env (DCase e alts) = "case " ++ show' env e ++ " of {\n\t" ++

183186 showSep "\n\t| " (map (showAlt env) alts)

184187 show' env (DConst c) = show c

src/IRTS/Lang.hs+7−1

@@ -15,11 +15,13 @@ data LExp = LV LVar

1515 | LForce LExp -- make sure Exp is evaluted

1616 | LLet Name LExp LExp -- name just for pretty printing

1717 | LLam [Name] LExp -- lambda, lifted out before compiling

18+ | LProj LExp Int -- projection

1819 | LCon Int Name [LExp]

1920 | LCase LExp [LAlt]

2021 | LConst Const

2122 | LForeign FLang FType String [(FType, LExp)]

2223 | LOp PrimFn [LExp]

24+ | LNothing

2325 | LError String

2426 deriving Eq

2527

@@ -118,6 +120,8 @@ lift env (LLam args e) = do e' <- lift (env ++ args) e

118120 fn <- getNextName

119121 addFn fn (LFun fn (usedArgs ++ args) e')

120122 return (LApp False (LV (Glob fn)) (map (LV . Glob) usedArgs))

123+lift env (LProj t i) = do t' <- lift env t

124+ return (LProj t' i)

121125lift env (LCon i n args) = do args' <- mapM (lift env) args

122126 return (LCon i n args')

123127lift env (LCase e alts) = do alts' <- mapM liftA alts

@@ -155,7 +159,8 @@ usedIn env (LForce e) = usedIn env e

155159usedIn env (LLet n v e) = usedIn env v ++ usedIn (env \\ [n]) e

156160usedIn env (LLam ns e) = usedIn (env \\ ns) e

157161usedIn env (LCon i n args) = concatMap (usedIn env) args

158−usedIn env (LCase e alts) = concatMap (usedInA env) alts

162+usedIn env (LProj t i) = usedIn env t

163+usedIn env (LCase e alts) = usedIn env e ++ concatMap (usedInA env) alts

159164 where usedInA env (LConCase i n ns e) = usedIn env e

160165 usedInA env (LConstCase c e) = usedIn env e

161166 usedInA env (LDefaultCase e) = usedIn env e

@@ -175,6 +180,7 @@ instance Show LExp where

175180 show' (env ++ [show n]) e

176181 show' env (LLam args e) = "\\ " ++ showSep "," (map show args) ++ " => " ++

177182 show' (env ++ (map show args)) e

183+ show' env (LProj t i) = show t ++ "!" ++ show i

178184 show' env (LCon i n args) = show n ++ ")" ++ showSep ", " (map (show' env) args) ++ ")"

179185 show' env (LCase e alts) = "case " ++ show' env e ++ " of {\n\t" ++

180186 showSep "\n\t| " (map (showAlt env) alts)

src/IRTS/Simplified.hs+16−2

@@ -5,6 +5,8 @@ import Core.TT

55import Data.Maybe

66import Control.Monad.State

77

8+import Debug.Trace

9+

810-- Simplified expressions, where functions/constructors can only be applied

911-- to variables

1012

@@ -13,9 +15,11 @@ data SExp = SV LVar

1315 | SLet LVar SExp SExp

1416 | SCon Int Name [LVar]

1517 | SCase LVar [SAlt]

18+ | SProj LVar Int

1619 | SConst Const

1720 | SForeign FLang FType String [(FType, LVar)]

1821 | SOp PrimFn [LVar]

22+ | SNothing -- erased value, will never be inspected

1923 | SError String

2024 deriving Show

2125

@@ -54,6 +58,11 @@ simplify tl (DLet n v e) = do v' <- simplify False v

5458 return (SLet (Glob n) v' e')

5559simplify tl (DC i n args) = do args' <- mapM sVar args

5660 mkapp (SCon i n) args'

61+simplify tl (DProj t i) = do v <- sVar t

62+ case v of

63+ (x, Nothing) -> return (SProj x i)

64+ (Glob x, Just e) ->

65+ return (SLet (Glob x) e (SProj (Glob x) i))

5766simplify tl (DCase e alts) = do v <- sVar e

5867 alts' <- mapM (sAlt tl) alts

5968 case v of

@@ -63,6 +72,7 @@ simplify tl (DCase e alts) = do v <- sVar e

6372simplify tl (DConst c) = return (SConst c)

6473simplify tl (DOp p args) = do args' <- mapM sVar args

6574 mkapp (SOp p) args'

75+simplify tl DNothing = return SNothing

6676simplify tl (DError str) = return $ SError str

6777

6878sVar (DV (Glob x))

@@ -111,7 +121,7 @@ lvar v = do i <- get

111121 put (max i v)

112122

113123scopecheck :: DDefs -> [(Name, Int)] -> SExp -> StateT Int TC SExp

114−scopecheck ctxt env tm = sc env tm where

124+scopecheck ctxt envTop tm = sc envTop tm where

115125 sc env (SV (Glob n)) =

116126 case lookup n (reverse env) of -- most recent first

117127 Just i -> do lvar i; return (SV (Loc i))

@@ -146,6 +156,9 @@ scopecheck ctxt env tm = sc env tm where

146156 else fail $ "Codegen error: Constructor " ++ show f ++

147157 " has arity " ++ show ar

148158 _ -> fail $ "Codegen error: No such constructor " ++ show f

159+ sc env (SProj e i)

160+ = do e' <- scVar env e

161+ return (SProj e' i)

149162 sc env (SCase e alts)

150163 = do e' <- scVar env e

151164 alts' <- mapM (scalt env) alts

@@ -168,7 +181,8 @@ scopecheck ctxt env tm = sc env tm where

168181 [DConstructor _ i ar] ->

169182 fail $ "Codegen error : can't pass constructor here"

170183 [_] -> return (Glob n)

171− [] -> fail $ "Codegen error: No such variable " ++ show n

184+ [] -> fail $ "Codegen error: No such variable " ++ show n ++

185+ " in " ++ show tm ++ " " ++ show envTop

172186 scVar _ x = return x

173187

174188 scalt env (SConCase _ i n args e)

src/Idris/AbsSyntax.hs+3−2

@@ -67,9 +67,10 @@ getTotality n

6767 [t] -> return t

6868 _ -> return (Total [])

6969

70−addToCG :: Name -> [Name] -> Idris ()

70+addToCG :: Name -> [(Name, [[Name]])] -> Idris ()

7171addToCG n ns = do i <- get

72− put (i { idris_callgraph = addDef n ns (idris_callgraph i) })

72+ put (i { idris_callgraph = addDef n (CGInfo ns [])

73+ (idris_callgraph i) })

7374

7475addToCalledG :: Name -> [Name] -> Idris ()

7576addToCalledG n ns = return () -- TODO

src/Idris/AbsSyntaxTree.hs+42−35

@@ -43,41 +43,48 @@ defaultOpts = IOption 0 False False True False False True True "" [] []

4343-- This will include all the functions and data declarations, plus fixity declarations

4444-- and syntax macros.

4545

46−data IState = IState { tt_ctxt :: Context,

47− idris_constraints :: [(UConstraint, FC)],

48− idris_infixes :: [FixDecl],

49− idris_implicits :: Ctxt [PArg],

50− idris_statics :: Ctxt [Bool],

51− idris_classes :: Ctxt ClassInfo,

52− idris_dsls :: Ctxt DSL,

53− idris_optimisation :: Ctxt OptInfo,

54− idris_datatypes :: Ctxt TypeInfo,

55− idris_patdefs :: Ctxt [([Name], Term, Term)], -- not exported

56− idris_flags :: Ctxt [FnOpt],

57− idris_callgraph :: Ctxt [Name],

58− idris_calledgraph :: Ctxt [Name],

59− idris_totcheck :: [(FC, Name)],

60− idris_log :: String,

61− idris_options :: IOption,

62− idris_name :: Int,

63− idris_metavars :: [Name],

64− syntax_rules :: [Syntax],

65− syntax_keywords :: [String],

66− imported :: [FilePath],

67− idris_scprims :: [(Name, (Int, PrimFn))],

68− idris_objs :: [FilePath],

69− idris_libs :: [String],

70− idris_hdrs :: [String],

71− proof_list :: [(Name, [String])],

72− errLine :: Maybe Int,

73− lastParse :: Maybe Name,

74− indent_stack :: [Int],

75− brace_stack :: [Maybe Int],

76− hide_list :: [(Name, Maybe Accessibility)],

77− default_access :: Accessibility,

78− ibc_write :: [IBCWrite],

79− compiled_so :: Maybe String

80− }

46+data IState = IState {

47+ tt_ctxt :: Context,

48+ idris_constraints :: [(UConstraint, FC)],

49+ idris_infixes :: [FixDecl],

50+ idris_implicits :: Ctxt [PArg],

51+ idris_statics :: Ctxt [Bool],

52+ idris_classes :: Ctxt ClassInfo,

53+ idris_dsls :: Ctxt DSL,

54+ idris_optimisation :: Ctxt OptInfo,

55+ idris_datatypes :: Ctxt TypeInfo,

56+ idris_patdefs :: Ctxt [([Name], Term, Term)], -- not exported

57+ idris_flags :: Ctxt [FnOpt],

58+ idris_callgraph :: Ctxt CGInfo, -- name, args used in each pos

59+ idris_calledgraph :: Ctxt [Name],

60+ idris_totcheck :: [(FC, Name)],

61+ idris_log :: String,

62+ idris_options :: IOption,

63+ idris_name :: Int,

64+ idris_metavars :: [Name],

65+ syntax_rules :: [Syntax],

66+ syntax_keywords :: [String],

67+ imported :: [FilePath],

68+ idris_scprims :: [(Name, (Int, PrimFn))],

69+ idris_objs :: [FilePath],

70+ idris_libs :: [String],

71+ idris_hdrs :: [String],

72+ proof_list :: [(Name, [String])],

73+ errLine :: Maybe Int,

74+ lastParse :: Maybe Name,

75+ indent_stack :: [Int],

76+ brace_stack :: [Maybe Int],

77+ hide_list :: [(Name, Maybe Accessibility)],

78+ default_access :: Accessibility,

79+ ibc_write :: [IBCWrite],

80+ compiled_so :: Maybe String

81+ }

82+

83+data CGInfo = CGInfo { calls :: [(Name, [[Name]])],

84+ argsused :: [Name] }

85+{-!

86+deriving instance Binary CGInfo

87+!-}

8188

8289primDefs = [UN "unsafePerformIO", UN "mkLazyForeign", UN "mkForeign", UN "FalseElim"]

8390

src/Idris/ElabDecls.hs+6−6

@@ -268,7 +268,7 @@ elabClauses info fc opts n_in cs = let n = liftname info n_in in

268268-- return False

269269 else return False

270270 pdef' <- applyOpts pdef

271− tree@(CaseDef _ sc _) <- tclift $ simpleCase tcase pcover fc pdef

271+ tree@(CaseDef _ sc _) <- tclift $ simpleCase tcase pcover False fc pdef

272272 ist <- get

273273-- let wf = wellFounded ist n sc

274274 let tot = if pcover || AssertTotal `elem` opts

@@ -287,7 +287,7 @@ elabClauses info fc opts n_in cs = let n = liftname info n_in in

287287 iputStrLn $ show fc ++

288288 ":warning - Unreachable case: " ++

289289 show (delab ist x)) xs

290− tree' <- tclift $ simpleCase tcase pcover fc pdef'

290+ tree' <- tclift $ simpleCase tcase pcover True fc pdef'

291291 logLvl 3 (show tree)

292292 logLvl 3 $ "Optimised: " ++ show tree'

293293 ctxt <- getContext

@@ -303,10 +303,10 @@ elabClauses info fc opts n_in cs = let n = liftname info n_in in

303303 i <- get

304304 case lookupDef Nothing n (tt_ctxt i) of

305305 (CaseOp _ _ _ scargs sc _ _ : _) ->

306− do let ns = namesUsed sc \\ scargs

307− logLvl 2 $ "Called names: " ++ show ns

308− addToCG n ns

309− addToCalledG n ns -- plus names in type!

306+ do let calls = findCalls sc scargs

307+ logLvl 2 $ "Called names: " ++ show calls

308+ addToCG n calls

309+ addToCalledG n (nub (map fst calls)) -- plus names in type!

310310 addIBC (IBCCG n)

311311 _ -> return ()

312312-- addIBC (IBCTotal n tot)

src/Idris/IBC.hs+35−14

@@ -21,7 +21,7 @@ import System.Directory

2121import Paths_idris

2222

2323ibcVersion :: Word8

24−ibcVersion = 19

24+ibcVersion = 21

2525

2626data IBCFile = IBCFile { ver :: Word8,

2727 sourcefile :: FilePath,

@@ -42,7 +42,7 @@ data IBCFile = IBCFile { ver :: Word8,

4242 ibc_access :: [(Name, Accessibility)],

4343 ibc_total :: [(Name, Totality)],

4444 ibc_flags :: [(Name, [FnOpt])],

45− ibc_cg :: [(Name, [Name])],

45+ ibc_cg :: [(Name, CGInfo)],

4646 ibc_defs :: [(Name, Def)] }

4747{-!

4848deriving instance Binary IBCFile

@@ -258,12 +258,20 @@ pTotal ds = mapM_ (\ (n, a) ->

258258 putIState (i { tt_ctxt = setTotal n a (tt_ctxt i) }))

259259 ds

260260

261−pCG :: [(Name, [Name])] -> Idris ()

262−pCG ds = mapM_ (\ (n, a) -> addToCG n a) ds

261+pCG :: [(Name, CGInfo)] -> Idris ()

262+pCG ds = mapM_ (\ (n, a) -> addToCG n (calls a)) ds

263263

264264----- Generated by 'derive'

265265

266−

266+instance Binary CGInfo where

267+ put (CGInfo x1 x2)

268+ = do put x1

269+ put x2

270+ get

271+ = do x1 <- get

272+ x2 <- get

273+ return (CGInfo x1 x2)

274+

267275instance Binary FC where

268276 put (FC x1 x2)

269277 = do put x1

@@ -285,6 +293,7 @@ instance Binary Name where

285293 MN x1 x2 -> do putWord8 2

286294 put x1

287295 put x2

296+ NErased -> putWord8 3

288297 get

289298 = do i <- getWord8

290299 case i of

@@ -296,6 +305,7 @@ instance Binary Name where

296305 2 -> do x1 <- get

297306 x2 <- get

298307 return (MN x1 x2)

308+ 3 -> return NErased

299309 _ -> error "Corrupted binary data for Name"

300310

301311

@@ -454,7 +464,7 @@ instance Binary NameType where

454464 return (TCon x1 x2)

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

456466

457−

467+

458468instance (Binary n) => Binary (TT n) where

459469 put x

460470 = case x of

@@ -473,9 +483,12 @@ instance (Binary n) => Binary (TT n) where

473483 put x2

474484 Constant x1 -> do putWord8 4

475485 put x1

476− Set x1 -> do putWord8 5

486+ Proj x1 x2 -> do putWord8 5

487+ put x1

488+ put x2

489+ Erased -> putWord8 6

490+ Set x1 -> do putWord8 7

477491 put x1

478− Erased -> do putWord8 6

479492 get

480493 = do i <- getWord8

481494 case i of

@@ -495,20 +508,25 @@ instance (Binary n) => Binary (TT n) where

495508 4 -> do x1 <- get

496509 return (Constant x1)

497510 5 -> do x1 <- get

498− return (Set x1)

511+ x2 <- get

512+ return (Proj x1 x2)

499513 6 -> return Erased

514+ 7 -> do x1 <- get

515+ return (Set x1)

500516 _ -> error "Corrupted binary data for TT"

501517

502−

503518instance Binary SC where

504519 put x

505520 = case x of

506521 Case x1 x2 -> do putWord8 0

507522 put x1

508523 put x2

509− STerm x1 -> do putWord8 1

524+ ProjCase x1 x2 -> do putWord8 1

525+ put x1

526+ put x2

527+ STerm x1 -> do putWord8 2

510528 put x1

511− UnmatchedCase x1 -> do putWord8 2

529+ UnmatchedCase x1 -> do putWord8 3

512530 put x1

513531 get

514532 = do i <- getWord8

@@ -517,10 +535,13 @@ instance Binary SC where

517535 x2 <- get

518536 return (Case x1 x2)

519537 1 -> do x1 <- get

520− return (STerm x1)

538+ x2 <- get

539+ return (ProjCase x1 x2)

521540 2 -> do x1 <- get

541+ return (STerm x1)

542+ 3 -> do x1 <- get

522543 return (UnmatchedCase x1)

523− _ -> error "Corrupted binary data for SC"

544+ _ -> error "Corrupted binary data for SC"

524545

525546

526547instance Binary CaseAlt where

src/Idris/Prover.hs+1−1

@@ -46,7 +46,7 @@ prove ctxt lit n ty

4646 i <- get

4747 let proofs = proof_list i

4848 put (i { proof_list = (n, prf) : proofs })

49− let tree = simpleCase False True (FC "proof" 0) [([], P Ref n ty, tm)]

49+ let tree = simpleCase False True False (FC "proof" 0) [([], P Ref n ty, tm)]

5050 logLvl 3 (show tree)

5151 (ptm, pty) <- recheckC (FC "proof" 0) [] tm

5252 ptm' <- applyOpts ptm