8c19e30 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Record internal name of 'with' functions

8c19e30Edwin Brady13 years ago

src/Idris/AbsSyntax.hs+12

compare with master

unifiedsplit

@@ -235,6 +235,18 @@ getName = do i <- getIState;

235 putIState $ (i { idris_name = idx + 1 })

236 return idx

237

238+addInternalName :: FilePath -> Int -> Name -> Int -> Idris ()

239+addInternalName fp l n w

240+ = do i <- getIState

241+ putIState (i { idris_linename = ((fp, l), (n, w)) : idris_linename i })

242+

243+getInternalName :: FilePath -> Int -> Name -- ^ default name

244+ -> Idris (Name, Int)

245+getInternalName fp l n = do i <- getIState

246+ case lookup (fp, l) (idris_linename i) of

247+ Nothing -> return (n, 0)

248+ Just n' -> return n'

249+

238checkUndefined :: FC -> Name -> Idris ()

250checkUndefined :: FC -> Name -> Idris ()

239checkUndefined fc n

251checkUndefined fc n

240 = do i <- getContext

252 = do i <- getContext

src/Idris/AbsSyntaxTree.hs+5−1

@@ -100,6 +100,9 @@ data IState = IState {

100 idris_log :: String,

101 idris_options :: IOption,

102 idris_name :: Int,

103+ idris_linename :: [((FilePath, Int), (Name, Int))],

104+ -- ^ internal name for function defined on that line,

105+ -- number of 'with' arguments

103 idris_metavars :: [Name], -- ^ The currently defined but not proven metavariables

106 idris_metavars :: [Name], -- ^ The currently defined but not proven metavariables

104 idris_coercions :: [Name],

107 idris_coercions :: [Name],

105 idris_transforms :: [(Term, Term)],

108 idris_transforms :: [(Term, Term)],

@@ -176,12 +179,13 @@ data IBCWrite = IBCFix FixDecl

176 | IBCDoc Name

179 | IBCDoc Name

177 | IBCCoercion Name

180 | IBCCoercion Name

178 | IBCDef Name -- i.e. main context

181 | IBCDef Name -- i.e. main context

182+ | IBCLineName FilePath Int Name Int

179 deriving Show

183 deriving Show

180

184

181idrisInit = IState initContext [] [] emptyContext emptyContext emptyContext

185idrisInit = IState initContext [] [] emptyContext emptyContext emptyContext

182 emptyContext emptyContext emptyContext emptyContext

186 emptyContext emptyContext emptyContext emptyContext

183 emptyContext emptyContext emptyContext emptyContext

187 emptyContext emptyContext emptyContext emptyContext

184− [] "" defaultOpts 6 [] [] [] [] [] [] [] [] [] [] []

188+ [] "" defaultOpts 6 [] [] [] [] [] [] [] [] [] [] [] []

185 [] Nothing Nothing [] [] [] Hidden False [] Nothing [] [] RawOutput

189 [] Nothing Nothing [] [] [] Hidden False [] Nothing [] [] RawOutput

186 True defaultTheme

190 True defaultTheme

187

191

src/Idris/ElabDecls.hs+3

@@ -1009,6 +1009,9 @@ elabClause info opts (_, PWith fc fname lhs_in withs wval_in withblock)

1009 (substTerm wargval (P Bound (MN 0 "warg") wargtype) ret_ty)

1010 logLvl 3 ("New function type " ++ show wtype)

1011 let wname = MN windex (show fname)

1012+ addInternalName (fc_fname fc) (fc_line fc) wname (length withs)

1013+ addIBC (IBCLineName (fc_fname fc) (fc_line fc) wname (length withs))

1014+

1012 let imps = getImps wtype -- add to implicits context

1015 let imps = getImps wtype -- add to implicits context

1013 putIState (i { idris_implicits = addDef wname imps (idris_implicits i) })

1016 putIState (i { idris_implicits = addDef wname imps (idris_implicits i) })

1014 addIBC (IBCDef wname)

1017 addIBC (IBCDef wname)

src/Idris/IBC.hs+14−5

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

23import Paths_idris

25ibcVersion :: Word8

26−ibcVersion = 42

26+ibcVersion = 43

28data IBCFile = IBCFile { ver :: Word8,

29 sourcefile :: FilePath,

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

50 ibc_defs :: [(Name, Def)],

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

52 ibc_transforms :: [(Term, Term)],

53− ibc_coercions :: [Name]

53+ ibc_coercions :: [Name],

54+ ibc_linenames :: [(FilePath, Int, Name, Int)]

54 }

55 }

55 deriving Show

56 deriving Show

56{-!

57{-!

@@ -58,7 +59,7 @@ deriving instance Binary IBCFile

58!-}

59!-}

60initIBC :: IBCFile

61initIBC :: IBCFile

61−initIBC = IBCFile ibcVersion "" [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] []

62+initIBC = IBCFile ibcVersion "" [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] []

63loadIBC :: FilePath -> Idris ()

64loadIBC :: FilePath -> Idris ()

64loadIBC fp = do iLOG $ "Loading ibc " ++ fp

65loadIBC fp = do iLOG $ "Loading ibc " ++ fp

@@ -134,6 +135,8 @@ ibc i (IBCAccess n a) f = return f { ibc_access = (n,a) : ibc_access f }

134ibc i (IBCFlags n a) f = return f { ibc_flags = (n,a) : ibc_flags f }

135ibc i (IBCFlags n a) f = return f { ibc_flags = (n,a) : ibc_flags f }

135ibc i (IBCTotal n a) f = return f { ibc_total = (n,a) : ibc_total f }

136ibc i (IBCTotal n a) f = return f { ibc_total = (n,a) : ibc_total f }

136ibc i (IBCTrans t) f = return f { ibc_transforms = t : ibc_transforms f }

137ibc i (IBCTrans t) f = return f { ibc_transforms = t : ibc_transforms f }

138+ibc i (IBCLineName fp l n w) f

139+ = return f { ibc_linenames = (fp,l,n, w) : ibc_linenames f }

137

140

138process :: IBCFile -> FilePath -> Idris ()

141process :: IBCFile -> FilePath -> Idris ()

139process i fn

142process i fn

@@ -168,6 +171,7 @@ process i fn

168 pDocs (ibc_docstrings i)

171 pDocs (ibc_docstrings i)

169 pCoercions (ibc_coercions i)

172 pCoercions (ibc_coercions i)

170 pTrans (ibc_transforms i)

173 pTrans (ibc_transforms i)

174+ pLineNames (ibc_linenames i)

171

175

172timestampOlder :: FilePath -> FilePath -> IO ()

176timestampOlder :: FilePath -> FilePath -> IO ()

173timestampOlder src ibc = do srct <- getModificationTime src

177timestampOlder src ibc = do srct <- getModificationTime src

@@ -312,6 +316,9 @@ pCoercions ns = mapM_ (\ n -> addCoercion n) ns

312pTrans :: [(Term, Term)] -> Idris ()

316pTrans :: [(Term, Term)] -> Idris ()

313pTrans ts = mapM_ addTrans ts

317pTrans ts = mapM_ addTrans ts

314

318

319+pLineNames :: [(FilePath, Int, Name, Int)] -> Idris ()

320+pLineNames ls = mapM_ (\ (f, i, n, w) -> addInternalName f i n w) ls

321+

315----- Generated by 'derive'

322----- Generated by 'derive'

316

323

317instance Binary SizeChange where

324instance Binary SizeChange where

@@ -861,7 +868,7 @@ instance Binary Totality where

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

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

862

869

863instance Binary IBCFile where

870instance Binary IBCFile where

864− 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 x25 x26)

871+ 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 x25 x26 x27)

865 = {-# SCC "putIBCFile" #-}

872 = {-# SCC "putIBCFile" #-}

866 do put x1

873 do put x1

867 put x2

874 put x2

@@ -889,6 +896,7 @@ instance Binary IBCFile where

889 put x24

896 put x24

890 put x25

897 put x25

891 put x26

898 put x26

899+ put x27

892 get

900 get

893 = do x1 <- get

901 = do x1 <- get

894 if x1 == ibcVersion then

902 if x1 == ibcVersion then

@@ -917,7 +925,8 @@ instance Binary IBCFile where

917 x24 <- get

925 x24 <- get

918 x25 <- get

926 x25 <- get

919 x26 <- get

927 x26 <- get

928+ x27 <- get

920− return (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 x25 x26)

929+ return (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 x25 x26 x27)

921 else return (initIBC { ver = x1 })

930 else return (initIBC { ver = x1 })

922

931

923instance Binary FnOpt where

932instance Binary FnOpt where