85e91ef · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Added '%access' directive and updated libs

%access sets the 'default' accessibility to public, private or abstract. If there are *no* access modifiers in a file, everything is public (this is the same behaviour as a Haskell module with no export list). If there are *any* access modifiers in a file, then declarations with no accessibility modifier take the %access setting as default. The default %access setting is 'private'.

commit85e91ef64c4d00161412d093a93a65a45033c717 authorEdwin Brady <eb@cs.st-andrews.ac.uk> dateThu 29 Dec 2011, 16:49 (15 years ago) parent9265e7c

8 files changed+41−18

compare with master

unifiedsplit

lib/builtins.idr+2 lib/io.idr+13−10 lib/prelude/list.idr+2 lib/prelude/nat.idr+2 lib/prelude/vect.idr+2 lib/system.idr+2 src/Idris/AbsSyntax.hs+2−1 src/Idris/Parser.hs+16−7

lib/builtins.idr+2

@@ -1,3 +1,5 @@

1+%access public

13data Exists : (a : Set) -> (P : a -> Set) -> Set where

24 Ex_intro : {P : a -> Set} -> (x : a) -> P x -> Exists a P;

lib/io.idr+13−10

@@ -1,10 +1,14 @@

11import prelude.list;

3−data IO a = prim__IO a;

3+%access public

5+abstract data IO a = prim__IO a;

7+abstract

58io_bind : IO a -> (a -> IO b) -> IO b;

69io_bind (prim__IO v) k = k v;

710

11+abstract

812io_return : a -> IO a;

913io_return x = prim__IO x;

1014

@@ -14,7 +18,6 @@ io_return x = prim__IO x;

1418-- run__IO : IO () -> IO ();

1519-- run__IO (prim__IO v) = prim__IO v;

1620

17−

1922

2023interpFTy : FTy -> Set;

@@ -34,16 +37,16 @@ ForeignTy xs t = mkForeign' (rev xs) (IO (interpFTy t)) where {

3437

3538namespace foreign {

3639

37−infixr 7 :: ;

40+ infixr 7 :: ;

3841

39−data FEnv : List FTy -> Set where

40− Nil : FEnv Nil

41− | (::) : {xs:List FTy} ->

42− interpFTy x -> FEnv xs -> FEnv (x ::xs);

42+ data FEnv : List FTy -> Set where

43+ Nil : FEnv Nil

44+ | (::) : {xs:List FTy} ->

45+ interpFTy x -> FEnv xs -> FEnv (x ::xs);

4346

44−data Foreign : Set -> Set where

45− FFun : String -> (xs:List FTy) -> (t:FTy) ->

46− Foreign (ForeignTy xs t);

47+ data Foreign : Set -> Set where

48+ FFun : String -> (xs:List FTy) -> (t:FTy) ->

49+ Foreign (ForeignTy xs t);

4750

4851}

4952

lib/prelude/list.idr+2

@@ -3,6 +3,8 @@ module prelude.list;

33import prelude.maybe;

44import builtins;

6+%access public

68infixr 7 :: ;

810data List a = Nil | (::) a (List a);

lib/prelude/nat.idr+2

@@ -2,6 +2,8 @@ module prelude.nat;

33import builtins;

5+%access public

57data Nat = O | S Nat;

79plus : Nat -> Nat -> Nat;

lib/prelude/vect.idr+2

@@ -2,6 +2,8 @@ module prelude.vect;

33import prelude.nat;

5+%access public

57data Fin : Nat -> Set where

68 fO : Fin (S k)

79 | fS : Fin k -> Fin (S k);

lib/system.idr+2

@@ -2,6 +2,8 @@ module system;

33import prelude;

5+%access public

57getArgs : IO (List String);

68getArgs = do { n <- numArgs;

79 ga' [] 0 n; }

src/Idris/AbsSyntax.hs+2−1

@@ -51,6 +51,7 @@ data IState = IState { tt_ctxt :: Context,

5151 errLine :: Maybe Int,

5252 lastParse :: Maybe Name,

5353 hide_list :: [(Name, Maybe Accessibility)],

54+ default_access :: Accessibility,

5455 ibc_write :: [IBCWrite]

5556 }

5657

@@ -71,7 +72,7 @@ data IBCWrite = IBCFix FixDecl

7172

7273idrisInit = IState initContext [] [] emptyContext emptyContext emptyContext

7374 "" defaultOpts 6 [] [] [] [] [] [] [] []

74− Nothing Nothing Nothing [] []

75+ Nothing Nothing Nothing [] Hidden []

7576

7677-- The monad for the main REPL - reading and processing files and updating

7778-- global state (hence the IO inner monad).

src/Idris/Parser.hs+16−7

@@ -110,10 +110,12 @@ loadSource lidr f

110110 namespaces (x:xs) ds = [PNamespace x (namespaces xs ds)]

111111

112112addHides :: [(Name, Maybe Accessibility)] -> Idris ()

113−addHides xs = let (hs, as) = partition isNothing xs in

114− if null as then return ()

115− else mapM_ doHide

116− (map (\ (n, _) -> (n, Hidden)) hs ++

113+addHides xs = do i <- getIState

114+ let defh = default_access i

115+ let (hs, as) = partition isNothing xs

116+ if null as then return ()

117+ else mapM_ doHide

118+ (map (\ (n, _) -> (n, defh)) hs ++

117119 map (\ (n, Just a) -> (n, a)) as)

118120 where isNothing (_, Nothing) = True

119121 isNothing _ = False

@@ -484,11 +486,15 @@ pName = do i <- getState

484486pfName = try pName

485487 <|> do lchar '('; o <- operator; lchar ')'; return (UN o)

486488

489+pAccessibility' :: IParser Accessibility

490+pAccessibility'

491+ = do reserved "public"; return Public

492+ <|> do reserved "abstract"; return Frozen

493+ <|> do reserved "private"; return Hidden

494+

487495pAccessibility :: IParser (Maybe Accessibility)

488496pAccessibility

489− = do reserved "public"; return (Just Public)

490− <|> do reserved "abstract"; return (Just Frozen)

491− <|> do reserved "private"; return (Just Hidden)

497+ = do acc <- pAccessibility'; return (Just acc)

492498 <|> return Nothing

493499

494500addAcc :: Name -> Maybe Accessibility -> IParser ()

@@ -908,6 +914,9 @@ pDirective = try (do lchar '%'; reserved "lib"; lib <- strlit;

908914 <|> try (do lchar '%'; reserved "freeze"; n <- iName []

909915 return [PDirective (do setAccessibility n Frozen

910916 addIBC (IBCAccess n Frozen))])

917+ <|> try (do lchar '%'; reserved "access"; acc <- pAccessibility'

918+ return [PDirective (do i <- getIState

919+ putIState (i { default_access = acc }))])

911920 <|> do lchar '%'; reserved "logging"; i <- natural;

912921 return [PDirective (setLogLevel (fromInteger i))]

913922