d34b7fc · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Merge remote-tracking branch 'upstream/master' into idrisdoc

d34b7fcPhilip Rasmussen13 years ago

libs/effects/Effect/File.idr+85−14

compare with master

unifiedsplit

@@ -1,24 +1,78 @@

1+-- -------------------------------------------------------- [ Effectful FileIO ]

1module Effect.File

2module Effect.File

3import Effects

4import Effects

4import Control.IOExcept

5import Control.IOExcept

8+||| A Dependent type to describe File Handles. File handles are

9+||| parameterised with the current state of the file: Closed; Open for

10+||| reading; and Open for writing.

11+|||

12+||| @ m The file mode.

6−data OpenFile : Mode -> Type where

13+data OpenFile : (m : Mode) -> Type where

7 FH : File -> OpenFile m

14 FH : File -> OpenFile m

9openOK : Mode -> Bool -> Type

16openOK : Mode -> Bool -> Type

10openOK m True = OpenFile m

17openOK m True = OpenFile m

11openOK m False = ()

18openOK m False = ()

20+-- ------------------------------------------------------------ [ The Protocol ]

21+

22+||| Here the protocol for resource access is defined as an effect.

23+||| The state transitions diagram for the protocol is as follows:

24+|||

25+||| digraph G {

26+|||

27+||| empty; read; write; // States

28+|||

29+||| empty -> read [label="Open R"];

30+||| read -> empty [label="Close"];

31+||| read -> read [label="ReadLine"];

32+||| read -> read [label="EOF"];

33+|||

34+||| empty -> write [label="Open W"];

35+||| write -> empty [label="Close"];

36+||| write -> write [label="WriteLine"];

37+|||

38+||| }

13data FileIO : Effect where

39data FileIO : Effect where

40+ ||| Open a file with the specified mode.

41+ |||

42+ ||| Opening a file successful moves the state from 'empty' to the

43+ ||| specified mode. If not successful the state is still 'empty'.

44+ |||

45+ ||| @ fname The file name to be opened.

46+ ||| @ m The file mode.

47+ Open : (fname: String)

14− Open : String -> (m : Mode) ->

48+ -> (m : Mode)

49+ -> {() ==> {res} if res

50+ then OpenFile m

15− {() ==> {res} if res then OpenFile m else ()} FileIO Bool

51+ else ()} FileIO Bool

52+

53+ ||| Close a file.

54+ |||

55+ ||| Closing a file moves the state from Open to closed.

16− Close : {OpenFile m ==> ()} FileIO ()

56+ Close : {OpenFile m ==> ()} FileIO ()

17−

57+

58+ ||| Read a line from the file.

59+ |||

60+ ||| Only files that are open for reading can be read.

18− ReadLine : {OpenFile Read} FileIO String

61+ ReadLine : {OpenFile Read} FileIO String

62+

63+ ||| Write a line to a file.

64+ |||

65+ ||| Only file that are open for writing can be written to.

19− WriteLine : String -> {OpenFile Write} FileIO ()

66+ WriteLine : String -> {OpenFile Write} FileIO ()

67+

68+ ||| End of file?

69+ |||

70+ ||| Only files open for reading can be tested for EOF

20− EOF : {OpenFile Read} FileIO Bool

71+ EOF : {OpenFile Read} FileIO Bool

21−

72+

73+-- ------------------------------------------------------------ [ The Handlers ]

74+

75+--- An implementation of the resource access protocol for the IO Context.

22instance Handler FileIO IO where

76instance Handler FileIO IO where

23 handle () (Open fname m) k = do h <- openFile fname m

77 handle () (Open fname m) k = do h <- openFile fname m

24 valid <- validFile h

78 valid <- validFile h

@@ -33,30 +87,47 @@ instance Handler FileIO IO where

33 handle (FH h) EOF k = do e <- feof h

87 handle (FH h) EOF k = do e <- feof h

34 k e (FH h)

88 k e (FH h)

90+-- -------------------------------------------------------------- [ The Effect ]

36FILE_IO : Type -> EFFECT

91FILE_IO : Type -> EFFECT

37FILE_IO t = MkEff t FileIO

92FILE_IO t = MkEff t FileIO

94+-- ------------------------------------------------------------ [ The Bindings ]

95+--

96+-- Bind the IO context handlers to functions. These functions will run

97+-- in the IO context.

98+--

99+

100+||| Open a file with the specified mode.

101+|||

102+||| @ fname The file name to be opened.

103+||| @ m The file mode.

39open : Handler FileIO e =>

104open : Handler FileIO e =>

105+ (fname : String)

40− String -> (m : Mode) ->

106+ -> (m : Mode)

41− { [FILE_IO ()] ==> [FILE_IO (if result then OpenFile m else ())] } Eff e Bool

107+ -> { [FILE_IO ()] ==> [FILE_IO (if result

108+ then OpenFile m

109+ else ())] } Eff e Bool

42open f m = Open f m

110open f m = Open f m

111

112+

113+||| Close a file.

44close : Handler FileIO e =>

114close : Handler FileIO e =>

45 { [FILE_IO (OpenFile m)] ==> [FILE_IO ()] } Eff e ()

115 { [FILE_IO (OpenFile m)] ==> [FILE_IO ()] } Eff e ()

46close = Close

116close = Close

117

118+||| Read a line from the file.

48readLine : Handler FileIO e =>

119readLine : Handler FileIO e =>

49 { [FILE_IO (OpenFile Read)] } Eff e String

120 { [FILE_IO (OpenFile Read)] } Eff e String

50readLine = ReadLine

121readLine = ReadLine

122

123+||| Write a line to a file.

52writeLine : Handler FileIO e =>

124writeLine : Handler FileIO e =>

53 String -> { [FILE_IO (OpenFile Write)] } Eff e ()

125 String -> { [FILE_IO (OpenFile Write)] } Eff e ()

54writeLine str = WriteLine str

126writeLine str = WriteLine str

127

128+||| End of file?

56eof : Handler FileIO e =>

129eof : Handler FileIO e =>

57 { [FILE_IO (OpenFile Read)] } Eff e Bool

130 { [FILE_IO (OpenFile Read)] } Eff e Bool

58eof = EOF

131eof = EOF

132

60−

133+-- --------------------------------------------------------------------- [ EOF ]

61−

62−

libs/prelude/Prelude/Fin.idr+6

@@ -98,6 +98,12 @@ instance MaxBound (Fin (S n)) where

98(+) {n=S n} {m=m} fZ f' = rewrite plusCommutative n m in weaken (weakenN n f')

99(+) (fS f) f' = fS (f + f')

100

101+||| Substract two Fins, keeping the bound of the minuend

102+(-) : Fin n -> Fin m -> Fin n

103+fZ - _ = fZ

104+f - fZ = f

105+(fS f) - (fS f') = weaken $ f - f'

106+

101||| Multiply two Fins, extending the bound

107||| Multiply two Fins, extending the bound

102(*) : Fin n -> Fin m -> Fin (n * m)

108(*) : Fin n -> Fin m -> Fin (n * m)

103(*) {n=Z} f f' = FinZElim f

109(*) {n=Z} f f' = FinZElim f

libs/prelude/Prelude/Vect.idr+8

@@ -381,6 +381,14 @@ nub = nubBy (==)

381-- Splitting and breaking lists

382--------------------------------------------------------------------------------

383

384+||| A tuple where the first element is a Vect of the n first elements and

385+||| the second element is a Vect of the remaining elements of the original Vect

386+||| It is equivalent to (take n xs, drop n xs)

387+||| @ m the index to split at

388+||| @ xs the Vect to split in two

389+splitAt : {n : Nat} -> (m : Fin (S n)) -> (xs : Vect n a) -> (Vect (cast m) a, Vect (n - cast m) a)

390+splitAt n xs = (take n xs, drop n xs)

391+

384--------------------------------------------------------------------------------

392--------------------------------------------------------------------------------

385-- Predicates

393-- Predicates

386--------------------------------------------------------------------------------

394--------------------------------------------------------------------------------

src/Idris/Coverage.hs+18−4

@@ -51,13 +51,18 @@ mkPatTm t = do i <- getIState

51-- This will only work after the given clauses have been typechecked and the

52-- names are fully explicit!

54−genClauses :: FC -> Name -> [Term] -> [PClause] -> Idris [PTerm]

54+genClauses :: FC -> Name -> [Term] -> [PTerm] -> Idris [PTerm]

55genClauses fc n xs given

56 = do i <- getIState

57− let lhss = map (getLHS i) xs

57+ let lhs_tms = map (\x -> delab' i x True True) xs

58+ -- if a placeholder was given, don't bother generating cases for it

59+ let lhs_tms' = zipWith mergePlaceholders lhs_tms given

60+ let lhss = map pUnApply lhs_tms'

61+

58 let argss = transpose lhss

62 let argss = transpose lhss

59 let all_args = map (genAll i) argss

63 let all_args = map (genAll i) argss

60 logLvl 5 $ "COVERAGE of " ++ show n

64 logLvl 5 $ "COVERAGE of " ++ show n

65+ logLvl 5 $ show lhss

61 logLvl 5 $ show (map length argss) ++ "\n" ++ show (map length all_args)

66 logLvl 5 $ show (map length argss) ++ "\n" ++ show (map length all_args)

62 logLvl 10 $ show argss ++ "\n" ++ show all_args

67 logLvl 10 $ show argss ++ "\n" ++ show all_args

63 logLvl 1 $ "Original: \n" ++

68 logLvl 1 $ "Original: \n" ++

@@ -82,8 +87,8 @@ genClauses fc n xs given

82 | (f, args) <- unApply term = map (\t -> delab' i t True True) args

87 | (f, args) <- unApply term = map (\t -> delab' i t True True) args

83 | otherwise = []

88 | otherwise = []

85− lhsApp (PClause _ _ l _ _ _) = l

90+ pUnApply (PApp _ _ args) = map getTm args

86− lhsApp (PWith _ _ l _ _ _) = l

91+ pUnApply _ = []

88 -- Return whether the given clause matches none of the input clauses

93 -- Return whether the given clause matches none of the input clauses

89 -- (xs)

94 -- (xs)

@@ -92,6 +97,14 @@ genClauses fc n xs given

92 Left miss -> True) xs

97 Left miss -> True) xs

100+ mergePlaceholders :: PTerm -> PTerm -> PTerm

101+ mergePlaceholders x Placeholder = Placeholder

102+ mergePlaceholders (PApp fc f args) (PApp fc' f' args')

103+ = PApp fc' f' (zipWith mergePArg args args')

104+ where mergePArg x y = let xtm = mergePlaceholders (getTm x) (getTm y) in

105+ x { getTm = xtm}

106+ mergePlaceholders x _ = x

107+

95 mkClauses :: [PArg] -> [[PTerm]] -> [PTerm]

108 mkClauses :: [PArg] -> [[PTerm]] -> [PTerm]

96 mkClauses parg args

109 mkClauses parg args

97 | all (== [Placeholder]) args = []

110 | all (== [Placeholder]) args = []

@@ -114,6 +127,7 @@ fnub' acc [] = acc

114

127

115-- quick check for constructor equality

128-- quick check for constructor equality

116quickEq :: PTerm -> PTerm -> Bool

129quickEq :: PTerm -> PTerm -> Bool

130+quickEq (PConstant n) (PConstant n') = n == n'

117quickEq (PRef _ n) (PRef _ n') = n == n'

131quickEq (PRef _ n) (PRef _ n') = n == n'

118quickEq (PApp _ t as) (PApp _ t' as')

132quickEq (PApp _ t as) (PApp _ t' as')

119 | length as == length as'

133 | length as == length as'

src/Idris/ElabDecls.hs+11−6

@@ -908,8 +908,10 @@ elabClauses info fc opts n_in cs = let n = liftname info n_in in

908 tclift $ tfail $ At fc (NoTypeDecl n)

909 [ty] -> return ty

910 let atys = map snd (getArgTys fty)

911− pats_in <- mapM (elabClause info opts)

911+ cs_elab <- mapM (elabClause info opts)

912 (zip [0..] cs)

913+ let (pats_in, cs_full) = unzip cs_elab

914+

913 logLvl 3 $ "Elaborated patterns:\n" ++ show pats_in

915 logLvl 3 $ "Elaborated patterns:\n" ++ show pats_in

914

916

915 -- if the return type of 'ty' is collapsible, the optimised version should

917 -- if the return type of 'ty' is collapsible, the optimised version should

@@ -994,7 +996,7 @@ elabClauses info fc opts n_in cs = let n = liftname info n_in in

994 cov <- coverage

996 cov <- coverage

995 pmissing <-

997 pmissing <-

996 if cov && not (hasDefault cs)

998 if cov && not (hasDefault cs)

997− then do missing <- genClauses fc n (map getLHS pdef) cs

999+ then do missing <- genClauses fc n (map getLHS pdef) cs_full

998 -- missing <- genMissing n scargs sc

1000 -- missing <- genMissing n scargs sc

999 missing' <- filterM (checkPossible info fc True n) missing

1001 missing' <- filterM (checkPossible info fc True n) missing

1000 let clhs = map getLHS pdef

1002 let clhs = map getLHS pdef

@@ -1352,16 +1354,19 @@ propagateParams ps t (PRef fc n)

1352 = PApp fc (PRef fc n) (map (\x -> pimp x (PRef fc x) True) ps)

1354 = PApp fc (PRef fc n) (map (\x -> pimp x (PRef fc x) True) ps)

1353propagateParams ps t x = x

1355propagateParams ps t x = x

1354

1356

1357+-- Return the elaborated LHS/RHS, and the original LHS with implicits added

1355elabClause :: ElabInfo -> FnOpts -> (Int, PClause) ->

1358elabClause :: ElabInfo -> FnOpts -> (Int, PClause) ->

1356− Idris (Either Term (Term, Term))

1359+ Idris (Either Term (Term, Term), PTerm)

1357elabClause info opts (_, PClause fc fname lhs_in [] PImpossible [])

1360elabClause info opts (_, PClause fc fname lhs_in [] PImpossible [])

1358 = do let tcgen = Dictionary `elem` opts

1361 = do let tcgen = Dictionary `elem` opts

1362+ i <- get

1363+ let lhs = addImpl i lhs_in

1359 b <- checkPossible info fc tcgen fname lhs_in

1364 b <- checkPossible info fc tcgen fname lhs_in

1360 case b of

1365 case b of

1361 True -> tclift $ tfail (At fc

1366 True -> tclift $ tfail (At fc

1362 (Msg $ show lhs_in ++ " is a valid case"))

1367 (Msg $ show lhs_in ++ " is a valid case"))

1363 False -> do ptm <- mkPatTm lhs_in

1368 False -> do ptm <- mkPatTm lhs_in

1364− return (Left ptm)

1369+ return (Left ptm, lhs)

1365elabClause info opts (cnum, PClause fc fname lhs_in withs rhs_in whereblock)

1370elabClause info opts (cnum, PClause fc fname lhs_in withs rhs_in whereblock)

1366 = do let tcgen = Dictionary `elem` opts

1371 = do let tcgen = Dictionary `elem` opts

1367 ctxt <- getContext

1372 ctxt <- getContext

@@ -1502,7 +1507,7 @@ elabClause info opts (cnum, PClause fc fname lhs_in withs rhs_in whereblock)

1502 when (rev || ErrorReverse `elem` opts) $ do

1507 when (rev || ErrorReverse `elem` opts) $ do

1503 addIBC (IBCErrRev (crhs, clhs))

1508 addIBC (IBCErrRev (crhs, clhs))

1504 addErrRev (crhs, clhs)

1509 addErrRev (crhs, clhs)

1505− return $ Right (clhs, crhs)

1510+ return $ (Right (clhs, crhs), lhs)

1506 where

1511 where

1507 mkLHSapp t@(PRef _ _) = trace ("APP " ++ show t) $ PApp fc t []

1512 mkLHSapp t@(PRef _ _) = trace ("APP " ++ show t) $ PApp fc t []

1508 mkLHSapp t = t

1513 mkLHSapp t = t

@@ -1669,7 +1674,7 @@ elabClause info opts (_, PWith fc fname lhs_in withs wval_in withblock)

1669 mapM_ (elabCaseBlock info opts) is

1674 mapM_ (elabCaseBlock info opts) is

1670 logLvl 5 ("Checked RHS " ++ show rhs')

1675 logLvl 5 ("Checked RHS " ++ show rhs')

1671 (crhs, crhsty) <- recheckC fc [] rhs'

1676 (crhs, crhsty) <- recheckC fc [] rhs'

1672− return $ Right (clhs, crhs)

1677+ return $ (Right (clhs, crhs), lhs)

1673 where

1678 where

1674 getImps (Bind n (Pi _) t) = pexp Placeholder : getImps t

1679 getImps (Bind n (Pi _) t) = pexp Placeholder : getImps t

1675 getImps _ = []

1680 getImps _ = []

src/Idris/IBC.hs+5−2

@@ -400,8 +400,11 @@ pPatdefs ds

400pDefs :: [Name] -> [(Name, Def)] -> Idris ()

401pDefs syms ds

402 = mapM_ (\ (n, d) ->

403− do i <- getIState

404− let d' = updateDef d

403+ do let d' = updateDef d

404+ case d' of

405+ TyDecl _ _ -> return ()

406+ _ -> solveDeferred n

407+ i <- getIState

405 logLvl 5 $ "Added " ++ show (n, d')

408 logLvl 5 $ "Added " ++ show (n, d')

406 putIState (i { tt_ctxt = addCtxtDef n d' (tt_ctxt i) })) ds

409 putIState (i { tt_ctxt = addCtxtDef n d' (tt_ctxt i) })) ds

407 where

410 where