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

lib/builtins.idr+2

compare with master

unifiedsplit

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

1+%access public

2+

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

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

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

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

3

5

lib/io.idr+13−10

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

1import prelude.list;

2

3−data IO a = prim__IO a;

3+%access public

4

5+abstract data IO a = prim__IO a;

6+

7+abstract

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

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

6io_bind (prim__IO v) k = k v;

9io_bind (prim__IO v) k = k v;

7

10

11+abstract

8io_return : a -> IO a;

12io_return : a -> IO a;

9io_return x = prim__IO x;

13io_return x = prim__IO x;

10

14

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

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

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

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

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

16

20

17−

19

22

20interpFTy : FTy -> Set;

23interpFTy : FTy -> Set;

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

34

37

35namespace foreign {

38namespace foreign {

36

39

37−infixr 7 :: ;

40+ infixr 7 :: ;

38

41

39−data FEnv : List FTy -> Set where

42+ data FEnv : List FTy -> Set where

40− Nil : FEnv Nil

43+ Nil : FEnv Nil

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

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

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

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

43

46

44−data Foreign : Set -> Set where

47+ data Foreign : Set -> Set where

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

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

46− Foreign (ForeignTy xs t);

49+ Foreign (ForeignTy xs t);

47

50

48}

51}

49

52

lib/prelude/list.idr+2

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

3import prelude.maybe;

4import builtins;

5

6+%access public

7+

6infixr 7 :: ;

8infixr 7 :: ;

7

9

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

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

lib/prelude/nat.idr+2

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

2

3import builtins;

4

5+%access public

6+

5data Nat = O | S Nat;

7data Nat = O | S Nat;

6

8

7plus : Nat -> Nat -> Nat;

9plus : Nat -> Nat -> Nat;

lib/prelude/vect.idr+2

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

2

3import prelude.nat;

4

5+%access public

6+

5data Fin : Nat -> Set where

7data Fin : Nat -> Set where

6 fO : Fin (S k)

8 fO : Fin (S k)

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

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

lib/system.idr+2

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

2

3import prelude;

4

5+%access public

6+

5getArgs : IO (List String);

7getArgs : IO (List String);

6getArgs = do { n <- numArgs;

8getArgs = do { n <- numArgs;

7 ga' [] 0 n; }

9 ga' [] 0 n; }

src/Idris/AbsSyntax.hs+2−1

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

51 errLine :: Maybe Int,

52 lastParse :: Maybe Name,

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

54+ default_access :: Accessibility,

54 ibc_write :: [IBCWrite]

55 ibc_write :: [IBCWrite]

55 }

56 }

56

57

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

71

72

72idrisInit = IState initContext [] [] emptyContext emptyContext emptyContext

73idrisInit = IState initContext [] [] emptyContext emptyContext emptyContext

73 "" defaultOpts 6 [] [] [] [] [] [] [] []

74 "" defaultOpts 6 [] [] [] [] [] [] [] []

74− Nothing Nothing Nothing [] []

75+ Nothing Nothing Nothing [] Hidden []

75

76

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

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

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

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

src/Idris/Parser.hs+16−7

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

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

111

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

113+addHides xs = do i <- getIState

114+ let defh = default_access i

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

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

114− if null as then return ()

116+ if null as then return ()

115− else mapM_ doHide

117+ else mapM_ doHide

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

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

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

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

118 where isNothing (_, Nothing) = True

120 where isNothing (_, Nothing) = True

119 isNothing _ = False

121 isNothing _ = False

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

484pfName = try pName

486pfName = try pName

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

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

486

488

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+

487pAccessibility :: IParser (Maybe Accessibility)

495pAccessibility :: IParser (Maybe Accessibility)

488pAccessibility

496pAccessibility

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

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

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

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

492 <|> return Nothing

498 <|> return Nothing

493

499

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

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

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

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

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

909 return [PDirective (do setAccessibility n Frozen

915 return [PDirective (do setAccessibility n Frozen

910 addIBC (IBCAccess n Frozen))])

916 addIBC (IBCAccess n Frozen))])

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

918+ return [PDirective (do i <- getIState

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

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

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

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

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

913

922