ffb50e2 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Insert namespace information to declaration-level %runElab

commitffb50e2023d55533c127e4e3bb632d4aac75dba8 authorDavid Raymond Christiansen <david@davidchristiansen.dk> dateWed 26 Aug 2015, 11:36 (11 years ago) parent822142a

6 files changed+19−16

compare with master

unifiedsplit

src/Idris/AbsSyntaxTree.hs+4−3 src/Idris/DeepSeq.hs+2−2 src/Idris/Elab/RunElab.hs+3−3 src/Idris/ElabDecls.hs+2−2 src/Idris/IBC.hs+7−5 src/Idris/Parser.hs+1−1

src/Idris/AbsSyntaxTree.hs+4−3

@@ -675,7 +675,8 @@ data PDecl' t

675675 | PProvider (Docstring (Either Err t)) SyntaxInfo FC FC (ProvideWhat' t) Name -- ^ Type provider. The first t is the type, the second is the term. The second FC is precise highlighting location.

676676 | PTransform FC Bool t t -- ^ Source-to-source transformation rule. If

677677 -- bool is True, lhs and rhs must be convertible

678− | PRunElabDecl FC t

678+ | PRunElabDecl FC t [String] -- ^ FC is decl-level, for errors, and

679+ -- Strings represent the namespace

679680 deriving Functor

680681{-!

681682deriving instance Binary PDecl'

@@ -841,8 +842,8 @@ mapPDeclFC f g (PProvider doc syn fc nfc what n) =

841842 PProvider doc syn (f fc) (g nfc) (fmap (mapPTermFC f g) what) n

842843mapPDeclFC f g (PTransform fc safe l r) =

843844 PTransform (f fc) safe (mapPTermFC f g l) (mapPTermFC f g r)

844−mapPDeclFC f g (PRunElabDecl fc script) =

845− PRunElabDecl (f fc) (mapPTermFC f g script)

845+mapPDeclFC f g (PRunElabDecl fc script ns) =

846+ PRunElabDecl (f fc) (mapPTermFC f g script) ns

846847

847848-- | Get all the names declared in a declaration

848849declared :: PDecl -> [Name]

src/Idris/DeepSeq.hs+2−2

@@ -196,8 +196,8 @@ instance (NFData t) => NFData (PDecl' t) where

196196 rnf x5 `seq` rnf x6 `seq` ()

197197 rnf (PTransform x1 x2 x3 x4)

198198 = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` rnf x4 `seq` ()

199− rnf (PRunElabDecl x1 x2)

200− = rnf x1 `seq` rnf x2 `seq` ()

199+ rnf (PRunElabDecl x1 x2 x3)

200+ = rnf x1 `seq` rnf x2 `seq` x3 `seq` ()

201201

202202instance NFData t => NFData (ProvideWhat' t) where

203203 rnf (ProvTerm ty tm) = rnf ty `seq` rnf tm `seq` ()

src/Idris/Elab/RunElab.hs+3−3

@@ -25,8 +25,8 @@ mustBeElabScript ty =

2525 OK _ -> return ()

2626 Error e -> ierror e

2727

28−elabRunElab :: ElabInfo -> FC -> PTerm -> Idris ()

29−elabRunElab info fc script' =

28+elabRunElab :: ElabInfo -> FC -> PTerm -> [String] -> Idris ()

29+elabRunElab info fc script' ns =

3030 do -- First elaborate the script itself

3131 (script, scriptTy) <- elabVal info ERHS script'

3232 mustBeElabScript scriptTy

@@ -35,7 +35,7 @@ elabRunElab info fc script' =

3535 (ElabResult tyT' defer is ctxt' newDecls highlights, log) <-

3636 tclift $ elaborate ctxt (idris_datatypes ist) (sMN 0 "toplLevelElab") elabScriptTy initEState

3737 (transformErr RunningElabScript

38− (erun fc (do tm <- runElabAction ist fc [] script [] --TODO namespace from parser

38+ (erun fc (do tm <- runElabAction ist fc [] script ns

3939 EState is _ impls highlights <- getAux

4040 ctxt <- get_context

4141 let ds = [] -- todo

src/Idris/ElabDecls.hs+2−2

@@ -266,7 +266,7 @@ elabDecl' what info (PProvider doc syn fc nfc provWhat n)

266266elabDecl' what info (PTransform fc safety old new)

267267 = do elabTransform info fc safety old new

268268 return ()

269−elabDecl' what info (PRunElabDecl fc script)

270− = do elabRunElab info fc script

269+elabDecl' what info (PRunElabDecl fc script ns)

270+ = do elabRunElab info fc script ns

271271 return ()

272272elabDecl' _ _ _ = return () -- skipped this time

src/Idris/IBC.hs+7−5

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

4040import Codec.Archive.Zip

4141

4242ibcVersion :: Word16

43−ibcVersion = 118

43+ibcVersion = 119

4444

4545data IBCFile = IBCFile { ver :: Word16,

4646 sourcefile :: FilePath,

@@ -1262,9 +1262,10 @@ instance (Binary t) => Binary (PDecl' t) where

12621262 put x2

12631263 put x3

12641264 put x4

1265− PRunElabDecl x1 x2 -> do putWord8 17

1266− put x1

1267− put x2

1265+ PRunElabDecl x1 x2 x3 -> do putWord8 17

1266+ put x1

1267+ put x2

1268+ put x3

12681269 get

12691270 = do i <- getWord8

12701271 case i of

@@ -1376,7 +1377,8 @@ instance (Binary t) => Binary (PDecl' t) where

13761377 return (PTransform x1 x2 x3 x4)

13771378 17 -> do x1 <- get

13781379 x2 <- get

1379− return (PRunElabDecl x1 x2)

1380+ x3 <- get

1381+ return (PRunElabDecl x1 x2 x3)

13801382 _ -> error "Corrupted binary data for PDecl'"

13811383

13821384instance Binary t => Binary (ProvideWhat' t) where

src/Idris/Parser.hs+1−1

@@ -1393,7 +1393,7 @@ runElabDecl syn =

13931393 return (spanFC fc fc'))

13941394 script <- expr syn <?> "elaborator script"

13951395 highlightP kwFC AnnKeyword

1396− return $ PRunElabDecl kwFC script

1396+ return $ PRunElabDecl kwFC script (syn_namespace syn)

13971397 <?> "top-level elaborator script"

13981398

13991399{- * Loading and parsing -}