fdfd99e · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Fix behaviour of %hide

%hide now merely makes a name inaccessible to programs, without changing any further behaviour. This is by adding a new accessibility class "Hidden" which can only be set via a %hide directive, and only for names which are currently visible. (Note that this doesn't quite fix the behaviour completely, because it'll behave oddly for names hidden in the current module. Will fix in a future commit...) Fixes #2945

commitfdfd99e3cad2685720282598e6e8b7da911a012e authorEdwin Brady <ecb10@st-andrews.ac.uk> dateSat 13 Feb 2016, 21:27 (11 years ago) parent0c5b397

16 files changed+50−15

compare with master

unifiedsplit

idris.cabal+3 src/Idris/AbsSyntax.hs+1 src/Idris/AbsSyntaxTree.hs+2−1 src/Idris/Core/DeepSeq.hs+1 src/Idris/Core/Evaluate.hs+6−4 src/Idris/IBC.hs+6−3 src/Idris/IdrisDoc.hs+2−2 src/Idris/Parser.hs+1−1 src/Idris/Parser/Data.hs+1−1 src/Idris/Parser/Helpers.hs+2−2 src/Idris/ProofSearch.hs+1 src/Idris/REPL/Browse.hs+2−1 test/reg069/Mod.idr+12 test/reg069/expected+2 test/reg069/reg069.idr+5 test/reg069/run+3

idris.cabal+3

@@ -317,6 +317,9 @@ Extra-source-files:

317317 test/reg068/run

318318 test/reg068/*.idr

319319 test/reg068/expected

320+ test/reg069/run

321+ test/reg069/*.idr

322+ test/reg069/expected

320323

321324 test/basic001/run

322325 test/basic001/*.idr

src/Idris/AbsSyntax.hs+1

@@ -1876,6 +1876,7 @@ aiFn topname inpat expat qq imp_meths ist fc f ffc ds as asexp

18761876

18771877 notHidden n = case getAccessibility n of

18781878 Hidden -> False

1879+ Private -> False

18791880 _ -> True

18801881

18811882 getAccessibility n

src/Idris/AbsSyntaxTree.hs+2−1

@@ -352,7 +352,7 @@ idrisInit = IState initContext S.empty []

352352 emptyContext emptyContext emptyContext emptyContext

353353 emptyContext

354354 [] [] [] defaultOpts 6 [] [] [] [] emptySyntaxRules [] [] [] [] [] [] []

355− [] [] Nothing [] Nothing [] [] Nothing Nothing emptyContext Hidden False [] Nothing [] []

355+ [] [] Nothing [] Nothing [] [] Nothing Nothing emptyContext Private False [] Nothing [] []

356356 (RawOutput stdout) True defaultTheme [] (0, emptyContext) emptyContext M.empty

357357 AutomaticWidth S.empty S.empty [] Nothing Nothing [] [] M.empty [] [] []

358358 emptyContext S.empty M.empty

@@ -2320,6 +2320,7 @@ implicitNamesIn uvars ist tm

23202320

23212321 notHidden (n, _) = case getAccessibility n of

23222322 Hidden -> False

2323+ Private -> False

23232324 _ -> True

23242325

23252326 getAccessibility n

src/Idris/Core/DeepSeq.hs+1

@@ -239,6 +239,7 @@ instance NFData Accessibility where

239239 rnf Public = ()

240240 rnf Frozen = ()

241241 rnf Hidden = ()

242+ rnf Private = ()

242243

243244

244245instance NFData Totality where

src/Idris/Core/Evaluate.hs+6−4

@@ -256,7 +256,7 @@ eval traceon ctxt ntimes genv tm opts = ev ntimes [] True [] tm where

256256 [(TyDecl nt ty, _)] -> do vty <- ev ntimes stk True env ty

257257 return $ VP nt n vty

258258 [(CaseOp ci _ _ _ _ cd, acc)]

259− | (acc == Public || sUN "assert_total" `elem` stk) &&

259+ | (acc == Public || acc == Hidden || sUN "assert_total" `elem` stk) &&

260260 null (fst (cases_totcheck cd)) -> -- unoptimised version

261261 let (ns, tree) = getCases cd in

262262 if blockSimplify ci n stk

@@ -374,7 +374,7 @@ eval traceon ctxt ntimes genv tm opts = ev ntimes [] True [] tm where

374374 do let val = lookupDefAcc n (spec || atRepl || runtime) ctxt

375375 case val of

376376 [(CaseOp ci _ _ _ _ cd, acc)]

377− | acc == Public || sUN "assert_total" `elem` stk ->

377+ | acc == Public || acc == Hidden || sUN "assert_total" `elem` stk ->

378378 -- unoptimised version

379379 let (ns, tree) = getCases cd in

380380 if blockSimplify ci n stk

@@ -743,7 +743,7 @@ instance Show Def where

743743-- Frozen => doesn't reduce

744744-- Hidden => doesn't reduce and invisible to type checker

745745

746−data Accessibility = Public | Frozen | Hidden

746+data Accessibility = Hidden | Public | Frozen | Private

747747 deriving (Eq, Ord)

748748{-!

749749deriving instance NFData Accessibility

@@ -752,7 +752,8 @@ deriving instance NFData Accessibility

752752instance Show Accessibility where

753753 show Public = "public export"

754754 show Frozen = "export"

755− show Hidden = "private"

755+ show Private = "private"

756+ show Hidden = "hidden"

756757

757758-- | The result of totality checking

758759data Totality = Total [Int] -- ^ well-founded arguments

@@ -1042,6 +1043,7 @@ lookupP_all all exact n ctxt

10421043 (Operator ty _ _, a, _, _) -> return (P Ref n' ty, a)

10431044 case snd p of

10441045 Hidden -> if all then return (fst p) else []

1046+ Private -> if all then return (fst p) else []

10451047 _ -> return (fst p)

10461048 where

10471049 names = let ns = lookupCtxtName n (definitions ctxt) in

src/Idris/IBC.hs+6−3

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

4040import Codec.Archive.Zip

4141

4242ibcVersion :: Word16

43−ibcVersion = 133

43+ibcVersion = 134

4444

4545-- When IBC is being loaded - we'll load different things (and omit different

4646-- structures/definitions) depending on which phase we're in

@@ -443,6 +443,7 @@ pImps imps = mapM_ (\ (n, imp) ->

443443 do i <- getIState

444444 case lookupDefAccExact n False (tt_ctxt i) of

445445 Just (n, Hidden) -> return ()

446+ Just (n, Private) -> return ()

446447 _ -> putIState (i { idris_implicits

447448 = addDef n imp (idris_implicits i) }))

448449 imps

@@ -938,13 +939,15 @@ instance Binary Accessibility where

938939 = case x of

939940 Public -> putWord8 0

940941 Frozen -> putWord8 1

941− Hidden -> putWord8 2

942+ Private -> putWord8 2

943+ Hidden -> putWord8 3

942944 get

943945 = do i <- getWord8

944946 case i of

945947 0 -> return Public

946948 1 -> return Frozen

947− 2 -> return Hidden

949+ 2 -> return Private

950+ 3 -> return Hidden

948951 _ -> error "Corrupted binary data for Accessibility"

949952

950953safeToEnum :: (Enum a, Bounded a, Integral int) => String -> int -> a

src/Idris/IdrisDoc.hs+2−2

@@ -182,7 +182,7 @@ filterName _ = False

182182

183183

184184-- | Whether a NsItem should be included in the documentation.

185−-- It must not be Hidden and filterName must return True for the name.

185+-- It must not be Hidden/Private and filterName must return True for the name.

186186-- Also it must have Docs -- without Docs, nothing can be done.

187187filterInclude :: NsItem -- ^ Accessibility to check

188188 -> Bool -- ^ Predicate result

@@ -254,7 +254,7 @@ getAccess ist n =

254254 let res = lookupDefAcc n False (tt_ctxt ist)

255255 in case res of

256256 [(_, acc)] -> acc

257− _ -> Hidden

257+ _ -> Private

258258

259259-- | Simple predicate for whether an NsItem has Docs

260260hasDoc :: NsItem -- ^ The NsItem to test

src/Idris/Parser.hs+1−1

@@ -1679,7 +1679,7 @@ loadSource lidr f toline

16791679 (n,fc):_ -> throwError . At fc . Msg $ "import alias not unique: " ++ show n

16801680

16811681 i <- getIState

1682− putIState (i { default_access = Hidden, module_aliases = modAliases })

1682+ putIState (i { default_access = Private, module_aliases = modAliases })

16831683 clearIBC -- start a new .ibc file

16841684 -- record package info in .ibc

16851685 imps <- allImportDirs

src/Idris/Parser/Data.hs+1−1

@@ -75,7 +75,7 @@ record syn = do (doc, paramDocs, acc, opts) <- try (do

7575 getName _ = Nothing

7676

7777 toFreeze :: Maybe Accessibility -> Maybe Accessibility

78− toFreeze (Just Frozen) = Just Hidden

78+ toFreeze (Just Frozen) = Just Private

7979 toFreeze x = x

8080

8181 recordBody :: SyntaxInfo -> Name -> IdrisParser ([((Maybe (Name, FC)), Plicity, PTerm, Maybe (Docstring (Either Err PTerm)))], Maybe (Name, FC), Docstring (Either Err PTerm))

src/Idris/Parser/Helpers.hs+2−2

@@ -641,7 +641,7 @@ accessibility'

641641 : parserWarnings ist }

642642 return Frozen

643643 <|> do reserved "export"; return Frozen

644− <|> do reserved "private"; return Hidden

644+ <|> do reserved "private"; return Private

645645 <?> "accessibility modifier"

646646

647647accessibility :: IdrisParser Accessibility

@@ -660,7 +660,7 @@ addAcc n a = do i <- get

660660 (works for classes too - 'abstract' means the data/class is visible but members not) -}

661661accData :: Accessibility -> Name -> [Name] -> IdrisParser ()

662662accData Frozen n ns = do addAcc n Public -- so that it can be used in public definitions

663− mapM_ (\n -> addAcc n Hidden) ns -- so that they are invisible

663+ mapM_ (\n -> addAcc n Private) ns -- so that they are invisible

664664accData a n ns = do addAcc n a

665665 mapM_ (`addAcc` a) ns

666666

src/Idris/ProofSearch.hs+1

@@ -513,4 +513,5 @@ findInstances ist t

513513 | otherwise = []

514514 where accessible n = case lookupDefAccExact n False (tt_ctxt ist) of

515515 Just (_, Hidden) -> False

516+ Just (_, Private) -> False

516517 _ -> True

src/Idris/REPL/Browse.hs+2−1

@@ -8,7 +8,7 @@ import Data.List (isSuffixOf, nub)

88import Data.Maybe (mapMaybe)

99import qualified Data.Text as T (unpack)

1010

11−import Idris.Core.Evaluate (ctxtAlist, Accessibility(Hidden), lookupDefAccExact)

11+import Idris.Core.Evaluate (ctxtAlist, Accessibility(Private, Hidden), lookupDefAccExact)

1212import Idris.Core.TT (Name(..))

1313

1414import Idris.AbsSyntaxTree (Idris)

@@ -41,4 +41,5 @@ namesInNS ns = do let revNS = reverse ns

4141 accessible n = do ctxt <- getContext

4242 case lookupDefAccExact n False ctxt of

4343 Just (_, Hidden ) -> return False

44+ Just (_, Private ) -> return False

4445 _ -> return True

test/reg069/Mod.idrnew file+12

@@ -0,0 +1,12 @@

1+module Mod

3+-- %access public

5+export

6+natfn : Nat -> Nat

7+natfn n = (S (S n))

9+public export

10+natexp : (n : Nat) -> Nat

11+natexp k = S (natfn k)

12+

test/reg069/expectednew file+2

@@ -0,0 +1,2 @@

1+Mod.idr:11:1:

2+public export Mod.natexp can't refer to export Mod.natfn

test/reg069/reg069.idrnew file+5

@@ -0,0 +1,5 @@

1+import Mod

3+foo : natexp 4 = 7

4+foo = Refl

test/reg069/runnew file+3

@@ -0,0 +1,3 @@

1+#!/usr/bin/env bash

2+${IDRIS:-idris} $@ reg069.idr --check

3+rm -f *.ibc