f03ee7e · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Merge pull request #1065 from ziman/fields

f03ee7eEdwin Brady13 years ago

idris.cabal+1

compare with master

unifiedsplit

@@ -456,6 +456,7 @@ Library

456 , Idris.AbsSyntax

457 , Idris.AbsSyntaxTree

458 , Idris.Apropos

459+ , Idris.ASTUtils

459 , Idris.CaseSplit

460 , Idris.CaseSplit

460 , Idris.Chaser

461 , Idris.Chaser

461 , Idris.Colours

462 , Idris.Colours

src/IRTS/Compiler.hs+11−14

@@ -19,6 +19,7 @@ import IRTS.Inliner

20import Idris.AbsSyntax

21import Idris.AbsSyntaxTree

22+import Idris.ASTUtils

22import Idris.Erasure

23import Idris.Erasure

23import Idris.Error

24import Idris.Error

@@ -28,6 +29,9 @@ import Idris.Core.TT

28import Idris.Core.Evaluate

29import Idris.Core.Evaluate

29import Idris.Core.CaseTree

30import Idris.Core.CaseTree

32+import Control.Category

33+import Prelude hiding (id, (.))

34+

31import Control.Applicative

35import Control.Applicative

32import Control.Monad.State

36import Control.Monad.State

33import Data.Maybe

37import Data.Maybe

@@ -172,10 +176,7 @@ mkLDecl n (CaseOp ci _ _ _ pats cd)

172 (args, sc) = cases_runtime cd

176 (args, sc) = cases_runtime cd

173

177

174mkLDecl n (TyDecl (DCon tag arity) _) =

178mkLDecl n (TyDecl (DCon tag arity) _) =

175− LConstructor n tag . erasedArity . lookup n <$> getIState

179+ LConstructor n tag . length <$> fgetState (cg_usedpos . ist_callgraph n)

176− where

177− lookup n = lookupCtxtExact n . idris_callgraph

178− erasedArity = maybe 0 (length . usedpos)

179

180

180mkLDecl n (TyDecl (TCon t a) _) = return $ LConstructor n (-1) a

181mkLDecl n (TyDecl (TCon t a) _) = return $ LConstructor n (-1) a

181mkLDecl n _ = return $ (declArgs [] True n LNothing) -- postulate, never run

182mkLDecl n _ = return $ (declArgs [] True n LNothing) -- postulate, never run

@@ -262,14 +263,13 @@ irTerm vs env tm@(App f a) = case unApply tm of

262 ])

263 ])

263

264

264 (P (DCon t arity) n _, args) -> do

265 (P (DCon t arity) n _, args) -> do

265− ist <- getIState

266+ detag <- fgetState (opt_detaggable . ist_optimisation n)

266− let detag = maybe False detaggable . lookupCtxtExact n $ idris_optimisation ist

267+ used <- map fst <$> fgetState (cg_usedpos . ist_callgraph n)

267− used = maybe [] (map fst . usedpos) . lookupCtxtExact n $ idris_callgraph ist

268− args' = [a | (i,a) <- zip [0..] args, i `elem` used]

269

268

270 when (length args > arity) $

269 when (length args > arity) $

271 ifail ("oversaturated data ctor: " ++ show tm)

270 ifail ("oversaturated data ctor: " ++ show tm)

272

271

272+ let args' = [a | (i,a) <- zip [0..] args, i `elem` used]

273 if length args' == 1 && detag -- detaggable

274 then irTerm vs env (head args') -- newtype

275 else irCon vs env (length used) n args'

@@ -473,8 +473,8 @@ irSC vs (Case n [ConCase (UN delay) i [_, _, n'] sc])

473irSC vs (Case n [alt]) = do

474 replacement <- case alt of

475 ConCase cn a ns sc -> do

476− detag <- maybe False detaggable . lookupCtxtExact cn . idris_optimisation <$> getIState

476+ detag <- fgetState (opt_detaggable . ist_optimisation cn)

477− used <- maybe [] (map fst . usedpos) . lookupCtxtExact cn . idris_callgraph <$> getIState

477+ used <- map fst <$> fgetState (cg_usedpos . ist_callgraph cn)

478 if detag && length used == 1

479 then return . Just $ substSC (ns !! head used) n sc

480 else return Nothing

@@ -505,13 +505,10 @@ irAlt :: Vars -> LExp -> CaseAlt -> Idris LAlt

505

506-- this leaves out all unused arguments of the constructor

507irAlt vs _ (ConCase n t args sc) = do

508− used <- getUsed . lookup n <$> getIState

508+ used <- map fst <$> fgetState (cg_usedpos . ist_callgraph n)

509 let usedArgs = [a | (i,a) <- zip [0..] args, i `elem` used]

510 LConCase (-1) n usedArgs <$> irSC (methodVars `M.union` vs) sc

511 where

512− lookup n = lookupCtxtExact n . idris_callgraph

513− getUsed = maybe [] (map fst . usedpos)

514−

515 methodVars = case n of

512 methodVars = case n of

516 SN (InstanceCtorN className)

513 SN (InstanceCtorN className)

517 -> M.fromList [(v, VI

514 -> M.fromList [(v, VI

src/Idris/ASTUtils.hsnew file+115

@@ -0,0 +1,115 @@

1+module Idris.ASTUtils where

3+-- This implements just a few basic lens-like concepts to ease state updates.

4+-- Similar to fclabels in approach, just without the extra dependency.

5+--

6+-- We don't include an explicit export list

7+-- because everything here is meant to be exported.

8+--

9+-- Short synopsis:

10+-- ---------------

11+--

12+-- f :: Idris ()

13+-- f = do

14+-- -- these two steps:

15+-- detaggable <- fgetState (opt_detaggable . ist_optimisation typeName)

16+-- fputState (opt_detaggable . ist_optimisation typeName) (not detaggable)

17+--

18+-- -- are equivalent to:

19+-- fmodifyState (opt_detaggable . ist_optimisation typeName) not

20+--

21+-- -- of course, the long accessor can be put in a variable;

22+-- -- everything is first-class

23+-- let detag n = opt_detaggable . ist_optimisation n

24+-- fputState (detag n1) True

25+-- fputState (detag n2) False

26+--

27+-- -- Note that all these operations handle missing items consistently

28+-- -- and transparently, as prescribed by the typeclass InitialValue.

29+

30+import Control.Category

31+import Control.Applicative

32+import Control.Monad.State.Class

33+import Data.Maybe

34+import Prelude hiding (id, (.))

35+

36+import Idris.Core.TT

37+import Idris.AbsSyntaxTree

38+

39+data Field rec fld = Field

40+ { fget :: rec -> fld

41+ , fset :: fld -> rec -> rec

42+ }

43+

44+fmodify :: Field rec fld -> (fld -> fld) -> rec -> rec

45+fmodify field f x = fset field (f $ fget field x) x

46+

47+instance Category Field where

48+ id = Field id const

49+ Field g2 s2 . Field g1 s1 = Field (g2 . g1) (\v2 x1 -> s1 (s2 v2 $ g1 x1) x1)

50+

51+fgetState :: MonadState s m => Field s a -> m a

52+fgetState field = gets $ fget field

53+

54+fputState :: MonadState s m => Field s a -> a -> m ()

55+fputState field x = fmodifyState field (const x)

56+

57+fmodifyState :: MonadState s m => Field s a -> (a -> a) -> m ()

58+fmodifyState field f = modify $ fmodify field f

59+

60+-- Until now, we'd have just ad-hoc empty lists and Falses thrown around

61+-- whenever a new instance of a record was to be created.

62+--

63+-- This class formalises the notion of an initial value for a record.

64+class InitialValue a where

65+ initialValue :: a

66+

67+-- Exact-name context lookup; uses the initial value if needed.

68+ctxt_lookupExact :: InitialValue a => Name -> Field (Ctxt a) a

69+ctxt_lookupExact n = Field

70+ { fget = fromMaybe initialValue . lookupCtxtExact n

71+ , fset = addDef n

72+ }

73+

74+

75+-----------------------------------

76+-- Individual records and fields --

77+-----------------------------------

78+--

79+-- These could probably be generated; let's use lazy addition for now.

80+--

81+

82+

83+-- OptInfo

84+----------

85+

86+instance InitialValue OptInfo where

87+ initialValue = Optimise [] False

88+

89+-- the optimisation record for the given (exact) name

90+ist_optimisation :: Name -> Field IState OptInfo

91+ist_optimisation n = ctxt_lookupExact n

92+ . Field idris_optimisation (\v ist -> ist{ idris_optimisation = v })

93+

94+-- two fields of the optimisation record

95+opt_inaccessible :: Field OptInfo [(Int, Name)]

96+opt_inaccessible = Field inaccessible (\v opt -> opt{ inaccessible = v })

97+

98+opt_detaggable :: Field OptInfo Bool

99+opt_detaggable = Field detaggable (\v opt -> opt{ detaggable = v })

100+

101+

102+-- CGInfo

103+---------

104+

105+instance InitialValue CGInfo where

106+ initialValue = CGInfo [] [] [] [] []

107+

108+-- callgraph record for the given (exact) name

109+ist_callgraph :: Name -> Field IState CGInfo

110+ist_callgraph n = ctxt_lookupExact n

111+ . Field idris_callgraph (\v ist -> ist{ idris_callgraph = v })

112+

113+-- some fields of the CGInfo record

114+cg_usedpos :: Field CGInfo [(Int, [UsageReason])]

115+cg_usedpos = Field usedpos (\v cg -> cg{ usedpos = v })

src/Idris/AbsSyntaxTree.hs+2−1

@@ -177,12 +177,13 @@ deriving instance NFData SizeChange

177!-}

178

179type SCGEntry = (Name, [Maybe (Int, SizeChange)])

180+type UsageReason = (Name, Int) -- fn_name, its_arg_number

180

181

181data CGInfo = CGInfo { argsdef :: [Name],

182data CGInfo = CGInfo { argsdef :: [Name],

182 calls :: [(Name, [[Name]])],

183 calls :: [(Name, [[Name]])],

183 scg :: [SCGEntry],

184 scg :: [SCGEntry],

184 argsused :: [Name],

185 argsused :: [Name],

185− usedpos :: [(Int, [(Name, Int)])] } -- (used_arg#, [(using_fn, its_arg#)])

186+ usedpos :: [(Int, [UsageReason])] }

186 deriving Show

187 deriving Show

187{-!

188{-!

188deriving instance Binary CGInfo

189deriving instance Binary CGInfo

src/Idris/Core/TT.hs+1

@@ -383,6 +383,7 @@ implicitable _ = False

383nsroot (NS n _) = n

384nsroot n = n

385

386+-- this will overwrite already existing definitions

386addDef :: Name -> a -> Ctxt a -> Ctxt a

387addDef :: Name -> a -> Ctxt a -> Ctxt a

387addDef n v ctxt = case Map.lookup (nsroot n) ctxt of

388addDef n v ctxt = case Map.lookup (nsroot n) ctxt of

388 Nothing -> Map.insert (nsroot n)

389 Nothing -> Map.insert (nsroot n)

src/Idris/ElabDecls.hs+14−24

@@ -4,6 +4,7 @@

4module Idris.ElabDecls where

6import Idris.AbsSyntax

7+import Idris.ASTUtils

7import Idris.DSL

8import Idris.DSL

8import Idris.Error

9import Idris.Error

9import Idris.Delaborate

10import Idris.Delaborate

@@ -29,6 +30,10 @@ import Idris.Core.CaseTree

30import Idris.Docstrings

31import Idris.Docstrings

33+import Prelude hiding (id, (.))

34+import Control.Category

35+

36+import Control.Applicative hiding (Const)

32import Control.DeepSeq

37import Control.DeepSeq

33import Control.Monad

38import Control.Monad

34import Control.Monad.State.Strict as State

39import Control.Monad.State.Strict as State

@@ -88,7 +93,7 @@ elabType' norm info syn doc argDocs fc opts n ty' = {- let ty' = piBind (params

88 let ty = addImpl i ty'

93 let ty = addImpl i ty'

89 inacc = inaccessibleArgs 0 ty

94 inacc = inaccessibleArgs 0 ty

90 logLvl 3 $ show n ++ " type " ++ showTmImpls ty

95 logLvl 3 $ show n ++ " type " ++ showTmImpls ty

91− logLvl 5 $ "Inaccessible arguments: " ++ show inacc

96+ logLvl 3 $ show n ++ ": inaccessible arguments: " ++ show inacc

93 ((tyT, defer, is), log) <-

98 ((tyT, defer, is), log) <-

94 tclift $ elaborate ctxt n (TType (UVal 0)) []

99 tclift $ elaborate ctxt n (TType (UVal 0)) []

@@ -134,7 +139,8 @@ elabType' norm info syn doc argDocs fc opts n ty' = {- let ty' = piBind (params

134 addDocStr n doc argDocs

139 addDocStr n doc argDocs

135 addIBC (IBCDoc n)

140 addIBC (IBCDoc n)

136 addIBC (IBCFlags n opts')

141 addIBC (IBCFlags n opts')

137− saveInaccArgs n inacc

142+ fputState (opt_inaccessible . ist_optimisation n) inacc

143+ addIBC (IBCOpt n)

138 when (Implicit `elem` opts') $ do addCoercion n

144 when (Implicit `elem` opts') $ do addCoercion n

139 addIBC (IBCCoercion n)

145 addIBC (IBCCoercion n)

140

146

@@ -178,24 +184,10 @@ elabType' norm info syn doc argDocs fc opts n ty' = {- let ty' = piBind (params

178 , ns4 == map txt ["Errors","Reflection","Language"] = True

184 , ns4 == map txt ["Errors","Reflection","Language"] = True

179 tyIsHandler _ = False

185 tyIsHandler _ = False

180

186

181−-- Store the list of inaccessible arguments in the internal state.

182−saveInaccArgs :: Name -> [(Int,Name)] -> Idris ()

183−saveInaccArgs n is = do

184− ist <- getIState

185− case lookupCtxt n (idris_optimisation ist) of

186− [oi] -> do

187− putIState ist{ idris_optimisation =

188− addDef n oi{ inaccessible = is } (idris_optimisation ist) }

189−

190− _ -> do

191− putIState ist{ idris_optimisation =

192− addDef n (Optimise is False) (idris_optimisation ist) }

193− addIBC (IBCOpt n)

194−

195-- Get the list of (index, name) of inaccessible arguments from the type.

187-- Get the list of (index, name) of inaccessible arguments from the type.

196inaccessibleArgs :: Int -> PTerm -> [(Int, Name)]

188inaccessibleArgs :: Int -> PTerm -> [(Int, Name)]

197inaccessibleArgs i (PPi (Imp _ _ _) n Placeholder t)

189inaccessibleArgs i (PPi (Imp _ _ _) n Placeholder t)

198− = (i,n) : inaccessibleArgs (i+1) t -- unbound implicit

190+ = (i,n) : inaccessibleArgs (i+1) t -- unbound implicit

199inaccessibleArgs i (PPi plicity n ty t)

191inaccessibleArgs i (PPi plicity n ty t)

200 | InaccessibleArg `elem` pargopts plicity

192 | InaccessibleArg `elem` pargopts plicity

201 = (i,n) : inaccessibleArgs (i+1) t -- an .{erased : Implicit}

193 = (i,n) : inaccessibleArgs (i+1) t -- an .{erased : Implicit}

@@ -918,7 +910,7 @@ elabCon info syn tn codata (doc, argDocs, n, t_in, fc, forcenames)

918 checkDocs fc argDocs t_in

910 checkDocs fc argDocs t_in

919 addDocStr n doc argDocs

911 addDocStr n doc argDocs

920 addIBC (IBCDoc n)

912 addIBC (IBCDoc n)

921− saveInaccArgs n inacc

913+ fputState (opt_inaccessible . ist_optimisation n) inacc

922 addIBC (IBCOpt n)

914 addIBC (IBCOpt n)

923 return (n, cty')

915 return (n, cty')

924 where

916 where

@@ -953,9 +945,8 @@ elabClauses :: ElabInfo -> FC -> FnOpts -> Name -> [PClause] -> Idris ()

953elabClauses info fc opts n_in cs = let n = liftname info n_in in

945elabClauses info fc opts n_in cs = let n = liftname info n_in in

954 do ctxt <- getContext

946 do ctxt <- getContext

955 ist <- getIState

947 ist <- getIState

956− let inacc = case lookupCtxt n (idris_optimisation ist) of

948+ inacc <- map fst <$> fgetState (opt_inaccessible . ist_optimisation n)

957− [Optimise inacc _] -> map fst inacc

949+

958− _ -> []

959 -- Check n actually exists, with no definition yet

950 -- Check n actually exists, with no definition yet

960 let tys = lookupTy n ctxt

951 let tys = lookupTy n ctxt

961 let reflect = Reflection `elem` opts

952 let reflect = Reflection `elem` opts

@@ -975,9 +966,8 @@ elabClauses info fc opts n_in cs = let n = liftname info n_in in

975

966

976 solveDeferred n

967 solveDeferred n

977

968

978− ist <- getIState

969+ -- just ensure that the structure exists

979− let opts = addDef n (Optimise [] False) (idris_optimisation ist)

970+ fmodifyState (ist_optimisation n) id

980− in putIState (ist { idris_optimisation = opts })

981 addIBC (IBCOpt n)

971 addIBC (IBCOpt n)

982

972

983 ist <- getIState

973 ist <- getIState

src/Idris/Erasure.hs+7−8

@@ -3,6 +3,7 @@

3module Idris.Erasure (performUsageAnalysis, mkFieldName) where

5import Idris.AbsSyntax

6+import Idris.ASTUtils

6import Idris.Core.CaseTree

7import Idris.Core.CaseTree

7import Idris.Core.TT

8import Idris.Core.TT

8import Idris.Core.Evaluate

9import Idris.Core.Evaluate

@@ -12,6 +13,9 @@ import Idris.Error

12import Debug.Trace

13import Debug.Trace

13import System.IO.Unsafe

14import System.IO.Unsafe

16+import Control.Category

17+import Prelude hiding (id, (.))

18+

15import Control.Arrow

19import Control.Arrow

16import Control.Applicative

20import Control.Applicative

17import Control.Monad.State

21import Control.Monad.State

@@ -97,7 +101,7 @@ performUsageAnalysis = do

97 $ ifail ("reachable postulates:\n" ++ intercalate "\n" [" " ++ show n | n <- S.toList reachablePostulates])

101 $ ifail ("reachable postulates:\n" ++ intercalate "\n" [" " ++ show n | n <- S.toList reachablePostulates])

102

99 -- Store the usage info in the internal state.

103 -- Store the usage info in the internal state.

100− mapM_ (storeUsage cg) usage

104+ mapM_ storeUsage usage

101

105

102 return $ S.toList reachableNames

106 return $ S.toList reachableNames

103 where

107 where

@@ -124,13 +128,8 @@ performUsageAnalysis = do

124 | S.null rs = show i

128 | S.null rs = show i

125 | otherwise = show i ++ " from " ++ intercalate ", " (map show $ S.toList rs)

129 | otherwise = show i ++ " from " ++ intercalate ", " (map show $ S.toList rs)

126

130

127− storeUsage :: Ctxt CGInfo -> (Name, IntMap (Set Reason)) -> Idris ()

131+ storeUsage :: (Name, IntMap (Set Reason)) -> Idris ()

128− storeUsage cg (n, args)

132+ storeUsage (n, args) = fputState (cg_usedpos . ist_callgraph n) flat

129− | Just x <- lookupCtxtExact n cg

130− = addToCG n x{ usedpos = flat } -- functions

131−

132− | otherwise

133− = addToCG n (CGInfo [] [] [] [] flat) -- data ctors

134 where

133 where

135 flat = [(i, S.toList rs) | (i,rs) <- IM.toList args]

134 flat = [(i, S.toList rs) | (i,rs) <- IM.toList args]

136

135