c9d2027 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Use exact name lookup for hiding

Otherwise, if we use ambiguous name lookup, we might accidentally hide things we didn't mean to. This was causing mysterious 'no such variable' errors in error reflection. Also, check that the name exists when using %hide (%hide will hide all names which match, still)

commitc9d20273f7cb8a6e212cd61abbccf419f2d7119f authorEdwin Brady <ecb10@st-andrews.ac.uk> dateFri 25 Mar 2016, 22:53 (11 years ago) parentcba27c8

7 files changed+26−13

compare with master

unifiedsplit

src/Idris/AbsSyntaxTree.hs+3−2 src/Idris/Core/TT.hs+3−2 src/Idris/DeepSeq.hs+2−2 src/Idris/Delaborate.hs+1−1 src/Idris/Directives.hs+11−2 src/Idris/IBC.hs+2−2 src/Idris/Parser.hs+4−2

src/Idris/AbsSyntaxTree.hs+3−2

@@ -1514,14 +1514,15 @@ data SyntaxInfo = Syn { using :: [Using],

15141514 maxline :: Maybe Int,

15151515 mut_nesting :: Int,

15161516 dsl_info :: DSL,

1517− syn_in_quasiquote :: Int }

1517+ syn_in_quasiquote :: Int,

1518+ syn_toplevel :: Bool }

15181519 deriving Show

15191520{-!

15201521deriving instance NFData SyntaxInfo

15211522deriving instance Binary SyntaxInfo

15221523!-}

15231524

1524−defaultSyntax = Syn [] [] [] [] [] id False False Nothing 0 initDSL 0

1525+defaultSyntax = Syn [] [] [] [] [] id False False Nothing 0 initDSL 0 True

15251526

15261527expandNS :: SyntaxInfo -> Name -> Name

15271528expandNS syn n@(NS _ _) = n

src/Idris/Core/TT.hs+3−2

@@ -645,8 +645,9 @@ deleteDefExact n = Map.adjust (Map.delete n) (nsroot n)

645645

646646updateDef :: Name -> (a -> a) -> Ctxt a -> Ctxt a

647647updateDef n f ctxt

648− = let ds = lookupCtxtName n ctxt in

649− foldr (\ (n, t) c -> addDef n (f t) c) ctxt ds

648+ = case lookupCtxtExact n ctxt of

649+ Just t -> addDef n (f t) ctxt

650+ Nothing -> ctxt

650651

651652toAlist :: Ctxt a -> [(Name, a)]

652653toAlist ctxt = let allns = map snd (Map.toList ctxt) in

src/Idris/DeepSeq.hs+2−2

@@ -681,13 +681,13 @@ instance NFData Using where

681681 rnf (UConstraint x1 x2) = rnf x1 `seq` rnf x2 `seq` ()

682682

683683instance NFData SyntaxInfo where

684− rnf (Syn x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12)

684+ rnf (Syn x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13)

685685 = rnf x1 `seq`

686686 rnf x2 `seq`

687687 rnf x3 `seq`

688688 rnf x4 `seq`

689689 rnf x5 `seq`

690− rnf x6 `seq` rnf x7 `seq` rnf x8 `seq` rnf x9 `seq` rnf x10 `seq` rnf x11 `seq` rnf x12 `seq` ()

690+ rnf x6 `seq` rnf x7 `seq` rnf x8 `seq` rnf x9 `seq` rnf x10 `seq` rnf x11 `seq` rnf x12 `seq` rnf x13 `seq` ()

691691

692692instance NFData OutputMode where

693693 rnf (RawOutput x) = () -- no instance for Handle, so this is a bit wrong

src/Idris/Delaborate.hs+1−1

@@ -488,7 +488,7 @@ pprintErr' i (ReflectionError parts orig) =

488488 else empty

489489pprintErr' i (ReflectionFailed msg err) =

490490 text "When attempting to perform error reflection, the following internal error occurred:" <>

491− indented (pprintErr' i err) <>

491+ indented (pprintErr' i err) <+> text msg <+>

492492 text ("This is probably a bug. Please consider reporting it at " ++ bugaddr)

493493pprintErr' i (ElabScriptDebug msg tm holes) =

494494 text "Elaboration halted." <>

src/Idris/Directives.hs+11−2

@@ -29,8 +29,10 @@ directiveAction (DFlag cgn flag) = do

2929directiveAction (DInclude cgn hdr) = do addHdr cgn hdr

3030 addIBC (IBCHeader cgn hdr)

3131

32−directiveAction (DHide n) = do setAccessibility n Hidden

33− addIBC (IBCAccess n Hidden)

32+directiveAction (DHide n') = do i <- getIState

33+ ns <- allNamespaces n'

34+ mapM_ (\n -> do setAccessibility n Hidden

35+ addIBC (IBCAccess n Hidden)) ns

3436

3537directiveAction (DFreeze n) = do setAccessibility n Frozen

3638 addIBC (IBCAccess n Frozen)

@@ -80,3 +82,10 @@ disambiguate n = do i <- getIState

8082 [(n', _)] -> return n'

8183 [] -> throwError (NoSuchVariable n)

8284 more -> throwError (CantResolveAlts (map fst more))

85+

86+allNamespaces :: Name -> Idris [Name]

87+allNamespaces n = do i <- getIState

88+ case lookupCtxtName n (idris_implicits i) of

89+ [(n', _)] -> return [n']

90+ [] -> throwError (NoSuchVariable n)

91+ more -> return (map fst more)

src/Idris/IBC.hs+2−2

@@ -1461,7 +1461,7 @@ instance Binary Using where

14611461 _ -> error "Corrupted binary data for Using"

14621462

14631463instance Binary SyntaxInfo where

1464− put (Syn x1 x2 x3 x4 _ _ x5 x6 _ _ x7 _)

1464+ put (Syn x1 x2 x3 x4 _ _ x5 x6 _ _ x7 _ _)

14651465 = do put x1

14661466 put x2

14671467 put x3

@@ -1477,7 +1477,7 @@ instance Binary SyntaxInfo where

14771477 x5 <- get

14781478 x6 <- get

14791479 x7 <- get

1480− return (Syn x1 x2 x3 x4 [] id x5 x6 Nothing 0 x7 0)

1480+ return (Syn x1 x2 x3 x4 [] id x5 x6 Nothing 0 x7 0 True)

14811481

14821482instance (Binary t) => Binary (PClause' t) where

14831483 put x

src/Idris/Parser.hs+4−2

@@ -608,7 +608,9 @@ fnDecl' syn = checkFixity $

608608 return (doc, argDocs, fc, opts', n, nfc, acc))

609609 ty <- typeExpr (allowImp syn)

610610 terminator

611− addAcc n acc

611+ -- If it's a top level function, note the accessibility

612+ -- rules

613+ when (syn_toplevel syn) $ addAcc n acc

612614 return (PTy doc argDocs syn fc opts' n nfc ty)

613615 <|> postulate syn

614616 <|> caf syn

@@ -1125,7 +1127,7 @@ clause syn

11251127 Nothing -> fail "Invalid clause"

11261128 (do r <- rhs syn n

11271129 let ctxt = tt_ctxt ist

1128− let wsyn = syn { syn_namespace = [] }

1130+ let wsyn = syn { syn_namespace = [], syn_toplevel = False }

11291131 (wheres, nmap) <- choice [do x <- whereBlock n wsyn

11301132 popIndent

11311133 return x,