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

git.iko.soy/Idris-dev

Record internal name of 'with' functions

Can look up by source file and line to get the internal name and the number of 'with' arguments, so thatJ case splitting has enough information to generate syntactically correct cases.

commit8c19e305f1e286886191c6e2f4228c80de5499ff authorEdwin Brady <ecb10@st-andrews.ac.uk> dateFri 25 Oct 2013, 18:27 (13 years ago) parent232fe96

4 files changed+34−6

compare with master

unifiedsplit

src/Idris/AbsSyntax.hs+12 src/Idris/AbsSyntaxTree.hs+5−1 src/Idris/ElabDecls.hs+3 src/Idris/IBC.hs+14−5

src/Idris/AbsSyntax.hs+12

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

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

236236 return idx

237237

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+

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

239251checkUndefined fc n

240252 = do i <- getContext

src/Idris/AbsSyntaxTree.hs+5−1

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

100100 idris_log :: String,

101101 idris_options :: IOption,

102102 idris_name :: Int,

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

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

105+ -- number of 'with' arguments

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

104107 idris_coercions :: [Name],

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

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

176179 | IBCDoc Name

177180 | IBCCoercion Name

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

182+ | IBCLineName FilePath Int Name Int

179183 deriving Show

180184

181185idrisInit = IState initContext [] [] emptyContext emptyContext emptyContext

182186 emptyContext emptyContext emptyContext emptyContext

183187 emptyContext emptyContext emptyContext emptyContext

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

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

185189 [] Nothing Nothing [] [] [] Hidden False [] Nothing [] [] RawOutput

186190 True defaultTheme

187191

src/Idris/ElabDecls.hs+3

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

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

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

10111011 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+

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

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

10141017 addIBC (IBCDef wname)

src/Idris/IBC.hs+14−5

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

2323import Paths_idris

2424

2525ibcVersion :: Word8

26−ibcVersion = 42

26+ibcVersion = 43

2727

2828data IBCFile = IBCFile { ver :: Word8,

2929 sourcefile :: FilePath,

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

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

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

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

53− ibc_coercions :: [Name]

53+ ibc_coercions :: [Name],

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

5455 }

5556 deriving Show

5657{-!

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

5859!-}

5960

6061initIBC :: IBCFile

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

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

6263

6364loadIBC :: FilePath -> Idris ()

6465loadIBC 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 }

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

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

136137ibc 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 }

137140

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

139142process i fn

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

168171 pDocs (ibc_docstrings i)

169172 pCoercions (ibc_coercions i)

170173 pTrans (ibc_transforms i)

174+ pLineNames (ibc_linenames i)

171175

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

173177timestampOlder src ibc = do srct <- getModificationTime src

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

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

313317pTrans ts = mapM_ addTrans ts

314318

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

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

321+

315322----- Generated by 'derive'

316323

317324instance Binary SizeChange where

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

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

862869

863870instance 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)

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

866873 do put x1

867874 put x2

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

889896 put x24

890897 put x25

891898 put x26

899+ put x27

892900 get

893901 = do x1 <- get

894902 if x1 == ibcVersion then

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

917925 x24 <- get

918926 x25 <- get

919927 x26 <- 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)

928+ x27 <- get

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)

921930 else return (initIBC { ver = x1 })

922931

923932instance Binary FnOpt where