ffb50e2 · Idris-dev · git.iko.soy

src/Idris/AbsSyntaxTree.hs+4−3

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

675 | 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.

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

677 -- 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

679 deriving Functor

680 deriving Functor

680{-!

681{-!

681deriving instance Binary PDecl'

682deriving instance Binary PDecl'

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

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

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

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

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

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

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

844−mapPDeclFC f g (PRunElabDecl fc script) =

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

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

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

846

847

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

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

848declared :: PDecl -> [Name]

849declared :: PDecl -> [Name]

src/Idris/DeepSeq.hs+2−2

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

196 rnf x5 `seq` rnf x6 `seq` ()

197 rnf (PTransform x1 x2 x3 x4)

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

199− rnf (PRunElabDecl x1 x2)

199+ rnf (PRunElabDecl x1 x2 x3)

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

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

201

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

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

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

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

25 OK _ -> return ()

26 Error e -> ierror e

27

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

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

29−elabRunElab info fc script' =

29+elabRunElab info fc script' ns =

30 do -- First elaborate the script itself

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

32 mustBeElabScript scriptTy

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

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

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

37 (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

39 EState is _ impls highlights <- getAux

40 ctxt <- get_context

41 let ds = [] -- todo

src/Idris/ElabDecls.hs+2−2

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

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

267 = do elabTransform info fc safety old new

268 return ()

269−elabDecl' what info (PRunElabDecl fc script)

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

270− = do elabRunElab info fc script

270+ = do elabRunElab info fc script ns

271 return ()

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

src/Idris/IBC.hs+7−5

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

40import Codec.Archive.Zip

41

42ibcVersion :: Word16

43−ibcVersion = 118

43+ibcVersion = 119

44

45data IBCFile = IBCFile { ver :: Word16,

46 sourcefile :: FilePath,

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

1262 put x2

1263 put x3

1264 put x4

1265− PRunElabDecl x1 x2 -> do putWord8 17

1265+ PRunElabDecl x1 x2 x3 -> do putWord8 17

1266− put x1

1266+ put x1

1267− put x2

1267+ put x2

1268+ put x3

1268 get

1269 get

1269 = do i <- getWord8

1270 = do i <- getWord8

1270 case i of

1271 case i of

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

1376 return (PTransform x1 x2 x3 x4)

1377 return (PTransform x1 x2 x3 x4)

1377 17 -> do x1 <- get

1378 17 -> do x1 <- get

1378 x2 <- get

1379 x2 <- get

1380+ x3 <- get

1379− return (PRunElabDecl x1 x2)

1381+ return (PRunElabDecl x1 x2 x3)

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

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

1381

1383

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

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

src/Idris/Parser.hs+1−1

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

1393 return (spanFC fc fc'))

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

1395 highlightP kwFC AnnKeyword

1396− return $ PRunElabDecl kwFC script

1396+ return $ PRunElabDecl kwFC script (syn_namespace syn)

1397 <?> "top-level elaborator script"

1398

1399{- * Loading and parsing -}