f707c76 · Idris-dev · git.iko.soy

CHANGELOG+1

compare with master

unifiedsplit

@@ -19,6 +19,7 @@ New in 0.9.12:

19 plus (n, m : Nat) -> Nat

20* Allow the auto-solve behavior in the prover to be disabled, for easier debugging

21 of proof automation. Use ":set autosolve" and ":unset autosolve".

22+* Updated 'effects' library

22

23

23New in 0.9.11:

24New in 0.9.11:

24--------------

25--------------

contribs/idrislang.sty+7−80

@@ -24,6 +24,7 @@

24\RequirePackage{ifthen}

25\RequirePackage{listings}

26\RequirePackage{xspace}

27+\RequirePackage{textcomp}

27%% ----------------------------------------------------------------- [ Options ]

28%% ----------------------------------------------------------------- [ Options ]

28\newboolean{literate}

29\newboolean{literate}

29\setboolean{literate}{false}

30\setboolean{literate}{false}

@@ -48,8 +49,9 @@

48\lstdefinelanguage{idris}{%

49\lstdefinelanguage{idris}{%

49 sensitive,%

50 sensitive,%

50%% ----------------------------------------------------------- [ Default Style ]

51%% ----------------------------------------------------------- [ Default Style ]

51− xleftmargin=\parindent,

52+ xleftmargin=1.5em,

52 tabsize=2,

53 tabsize=2,

54+ upquote=true,

53 basicstyle=\ttfamily,

55 basicstyle=\ttfamily,

54 flexiblecolumns=false,

56 flexiblecolumns=false,

55 commentstyle=\footnotesize\sffamily,

57 commentstyle=\footnotesize\sffamily,

@@ -63,78 +65,9 @@

63 total, trivial, try, using, where, with

65 total, trivial, try, using, where, with

64},

66},

65%% ------------------------------------------------------- [ Prelude Functions ]

67%% ------------------------------------------------------- [ Prelude Functions ]

66−%% Generated using

67−%% find lib/ -name "*.idr" | xargs grep -e "^[a-zA-Z0-9]* :" | awk -F : '{printf $2", "}'

68 morekeywords={%

69− class, data, instance, record, dsl, postulate, default, assert_total,

69+ class, data, instance, record, dsl, postulate, default,

70 lambda, variable, index_first, index_next

71− % trace, unsafePerformPrimIO, FInt, FChar, FByte, FShort, FLong,

72− % FBits8, FBits16, FBits32, FBits64, FBits8x16, FBits16x8,

73− % FBits32x4, FBits64x2, interpFTy, ForeignTy, mkForeignPrim,

74− % mkLazyForeignPrim, liftPrimIO, fork, unsafePerformIO, listens,

75− % censor, Writer, liftReaderT, asks, Reader, modify, gets, State,

76− % RWS, nGTSm, decideNatLTE, lte, vectInjective1, vectInjective2,

77− % run, myID, send, msgWaiting, recv, recvWithSender, create,

78− % sendToThread, checkMsgs, getMsg, viewB8x16, viewB16x8, viewB32x4,

79− % viewB64x2, pow, exp, log, pi, sin, cos, tan, asin, acos, atan,

80− % atan2, sinh, cosh, tanh, sqrt, floor, ceiling, count, countFrom,

81− % curry, uncurry, uniformB8x16, uniformB16x8, uniformB32x4,

82− % uniformB64x2, putStr, putStrLn, print, getLine, putChar, getChar,

83− % fopen, openFile, closeFile, fread, fwrite, feof, ferror, nullPtr,

84− % nullStr, validFile, while, readFile, userSuppliedName, seq, try,

85− % mkPair, getUName, unApply, mkApp, binderTy, divCeil, nextPow2,

86− % nextBytes, machineTy, bitsUsed, natToBits, getPad, pad8, pad16,

87− % pad32, pad64, shiftLeft, shiftRightLogical, shiftRightArithmetic,

88− % and, or, xor, plus, minus, times, sdiv, udiv, srem, urem, lt, lte,

89− % eq, gte, gt, complement, zeroExtend, intToBits, bitsToInt, bitAt,

90− % getBit, setBit, unsetBit, bitsToStr, findElem, replaceElem,

91− % replaceByElem, mapElem, anyNilAbsurd, anyElim, any, negAnyAll,

92− % notAllHere, notAllThere, all, length, index, weaken, take, toList,

93− % fromList, replicate, foldl, foldr, map, pad, zeroBoundIsEmpty,

94− % empty, insert, delete, contains, fromList, toList, applyKleisli,

95− % applyMor, applyEndo, absZ, negZ, negNat, minusNatZ, plusZ, subZ,

96− % multZ, fromInt, natPlusZPlus, natMultZMult, doubleNegElim,

97− % posInjective, negSInjective, posNotNeg, plusZeroLeftNeutralZ,

98− % plusZeroRightNeutralZ, plusCommutativeZ, modBin, modComp, div,

99− % rem, intToMod, modToStr, branch4, branch5, branch6, branch7,

100− % merge1, merge2, merge3, treeLookup, treeInsert, delType,

101− % treeDelete, treeToList, empty, lookup, insert, delete, fromList,

102− % toList, getWitness, getProof, FalseElim, replace, sym, trans,

103− % lazy, par, malloc, Not, id, the, const, fst, snd, flip, cong,

104− % boolElim, not, intToBool, boolOp, div, mod, strHead, strTail,

105− % strCons, strIndex, reverse, null, getArgs, getEnv, setEnv,

106− % unsetEnv, getEnvironment, exit, usleep, sequence, toHexDigit,

107− % b8ToString, b16ToString, b32ToString, b64ToString, tail, head,

108− % last, init, index, deleteAt, replaceAt, take, drop, fromList,

109− % replicate, zipWith, zip, unzip, concat, elemBy, elem, lookupBy,

110− % lookup, hasAnyBy, hasAny, find, findIndex, elemIndexBy, elemIndex,

111− % nubBy, nub, isPrefixOfBy, isPrefixOf, isSuffixOfBy, isSuffixOf,

112− % catMaybes, diag, range, isLeft, isRight, choose, either, lefts,

113− % rights, partitionEithers, fromEither, maybeToEither, strM, unpack,

114− % pack, span, break, split, ltrim, trim, words, lines, foldr1,

115− % unwords, length, realPart, imagPart, mkPolar, cis, magnitude,

116− % phase, conjugate, isNothing, isJust, maybe, fromMaybe, toMaybe,

117− % justInjective, lowerMaybe, raiseToMaybe, isNil, isCons, head,

118− % tail, last, init, take, drop, takeWhile, dropWhile, list, length,

119− % repeat, replicate, zipWith, zipWith3, zip, zip3, unzip, unzip3,

120− % mapMaybe, toList, reverse, intersperse, intercalate, elemBy, elem,

121− % lookupBy, lookup, hasAnyBy, hasAny, find, findIndex, findIndices,

122− % elemIndexBy, elemIndex, elemIndicesBy, elemIndices, filter, nubBy,

123− % nub, span, break, split, partition, isPrefixOfBy, isPrefixOf,

124− % isSuffixOfBy, isSuffixOf, sorted, mergeBy, merge, sort,

125− % maybeToList, listToMaybe, catMaybes, appendNilRightNeutral,

126− % appendAssociative, lengthAppend, mapPreservesLength,

127− % mapDistributesOverAppend, mapFusion, hasAnyByNilFalse,

128− % hasAnyNilFalse, fromIntegerNat, toIntegerNat, hyper, log2, gcd,

129− % liftA, liftA2, liftA3, guard, when, finToNat, finToInt, weaken,

130− % strengthen, last, natToFin, integerToFin, fromInteger, flatten,

131− % return, isUpper, isLower, isAlpha, isDigit, isAlphaNum, isSpace,

132− % isNL, toUpper, toLower, isHexDigit, isValidHeap, merge, insert,

133− % findMinimum, deleteMinimum, toList, fromList, sort, main, foldl,

134− % concat, concatMap, and, or, any, all, sum, product, Vars,

135− % getAction, setInfo, getInfo, lift, output, queryVars, postVars,

136− % cookieVars, queryVar, getOutput, getHeaders, flushHeaders, flush,

137− % getVars, getContent, getCgiEnv, runCGI, mult

138 },

71 },

139%% ---------------------------------------------------------------- [ Comments ]

72%% ---------------------------------------------------------------- [ Comments ]

140 morecomment=[l]--,%

73 morecomment=[l]--,%

@@ -166,13 +99,9 @@

166%% -------------------------------------------------- [ Default Listings Style ]

99%% -------------------------------------------------- [ Default Listings Style ]

167

100

168\lstdefinestyle{default}{%

101\lstdefinestyle{default}{%

169− xleftmargin=\parindent,

170− tabsize=2,

171 basicstyle=\ttfamily

102 basicstyle=\ttfamily

172}

103}

173\lstdefinestyle{numbers}{%

104\lstdefinestyle{numbers}{%

174− xleftmargin=\parindent,

175− tabsize=2,

176 numbers=left,

105 numbers=left,

177 numbersep=10pt,

106 numbersep=10pt,

178 numberstyle=\footnotesize\sffamily,

107 numberstyle=\footnotesize\sffamily,

@@ -186,11 +115,9 @@

186 {\ifthenelse{\boolean{literate}}{%

115 {\ifthenelse{\boolean{literate}}{%

187 \lstset{language=literateidris}}{%

116 \lstset{language=literateidris}}{%

188 \lstset{language=idris}}

117 \lstset{language=idris}}

189− \ifthenelse{\boolean{numbers}}{%

118+ \ifthenelse{\boolean{numbers}}{%

190− \lstset{style=numbers, #1}}{%

119+ \lstset{style=numbers, #1}}{%

191− \lstset{style=default, #1}}

120+ \lstset{style=default, #1}}}{}

192− }

193− {}

194%% ---------------------------------------------------------- [ Input Listings ]

121%% ---------------------------------------------------------- [ Input Listings ]

195%% Command to add externally defined Idris code to the document.

122%% Command to add externally defined Idris code to the document.

196\newcommand{\inputIdrisListing}[2][]{%

123\newcommand{\inputIdrisListing}[2][]{%

idris.cabal+8−4

@@ -97,10 +97,10 @@ Extra-source-files:

97 libs/effects/Effect/*.idr

98 libs/effects/*.idr

99

100− libs/neweffects/Makefile

100+ libs/oldeffects/Makefile

101− libs/neweffects/neweffects.ipkg

101+ libs/oldeffects/oldeffects.ipkg

102− libs/neweffects/Effect/*.idr

102+ libs/oldeffects/Effect/*.idr

103− libs/neweffects/*.idr

103+ libs/oldeffects/*.idr

104

105 libs/javascript/*.idr

106 libs/javascript/JavaScript/*.idr

@@ -382,6 +382,10 @@ Extra-source-files:

382 test/totality003/*.idr

383 test/totality003/expected

384

385+ test/tutorial001/run

386+ test/tutorial001/*.idr

387+ test/tutorial001/expected

388+

385source-repository head

389source-repository head

386 type: git

390 type: git

387 location: git://github.com/idris-lang/Idris-dev.git

391 location: git://github.com/idris-lang/Idris-dev.git

libs/Makefile+3−3

@@ -2,7 +2,7 @@ build:

2 $(MAKE) -C prelude build

3 $(MAKE) -C base build

4 $(MAKE) -C effects build

5− $(MAKE) -C neweffects build

5+ $(MAKE) -C oldeffects build

6 $(MAKE) -C javascript build

7

8

@@ -10,14 +10,14 @@ install:

10 $(MAKE) -C prelude install

11 $(MAKE) -C base install

12 $(MAKE) -C effects install

13− $(MAKE) -C neweffects install

13+ $(MAKE) -C oldeffects install

14 $(MAKE) -C javascript install

15

16clean:

17 $(MAKE) -C prelude clean

18 $(MAKE) -C base clean

19 $(MAKE) -C effects clean

20− $(MAKE) -C neweffects clean

20+ $(MAKE) -C oldeffects clean

21 $(MAKE) -C javascript clean

22

23.PHONY: build install clean

libs/base/Language/Reflection/Errors.idr+1−1

@@ -3,7 +3,7 @@ module Language.Reflection.Errors

3import Language.Reflection

4

5data SourceLocation : Type where

6− FileLoc : (filename : String) -> (line : Int) -> (col : Int) -> SourceLocation

6+ FileLoc : (filename : String) -> (start : (Int, Int)) -> (end : (Int, Int)) -> SourceLocation

7

8%name SourceLocation loc

9

libs/neweffects/Effect/Default.idr → libs/effects/Effect/Default.idrrenamed

The content is the same.

libs/effects/Effect/Exception.idr+6−4

@@ -4,12 +4,15 @@ import Effects

4import System

5import Control.IOExcept

6

7−data Exception : Type -> Type -> Type -> Type -> Type where

7+data Exception : Type -> Effect where

8− Raise : a -> Exception a () () b

8+ Raise : a -> { () } Exception a b

9

10instance Handler (Exception a) Maybe where

11 handle _ (Raise e) k = Nothing

12

13+instance Handler (Exception a) List where

14+ handle _ (Raise e) k = []

15+

13instance Show a => Handler (Exception a) IO where

16instance Show a => Handler (Exception a) IO where

14 handle _ (Raise e) k = do print e

17 handle _ (Raise e) k = do print e

15 believe_me (exit 1)

18 believe_me (exit 1)

@@ -23,7 +26,7 @@ instance Handler (Exception a) (Either a) where

23EXCEPTION : Type -> EFFECT

26EXCEPTION : Type -> EFFECT

24EXCEPTION t = MkEff () (Exception t)

27EXCEPTION t = MkEff () (Exception t)

25

28

26−raise : a -> Eff m [EXCEPTION a] b

29+raise : a -> { [EXCEPTION a ] } Eff m b

27raise err = Raise err

30raise err = Raise err

28

31

29

32

@@ -31,7 +34,6 @@ raise err = Raise err

31

34

32

35

33

36

34−

35-- TODO: Catching exceptions mid program?

37-- TODO: Catching exceptions mid program?

36-- probably need to invoke a new interpreter

38-- probably need to invoke a new interpreter

37

39

libs/effects/Effect/File.idr+24−31

@@ -6,62 +6,55 @@ import Control.IOExcept

6data OpenFile : Mode -> Type where

7 FH : File -> OpenFile m

8

9−data FileIO : Effect where

9+openOK : Mode -> Bool -> Type

10− Open : String -> (m : Mode) -> FileIO () (Either () (OpenFile m)) Bool

11− Close : FileIO (OpenFile m) () ()

10+openOK m True = OpenFile m

11+openOK m False = ()

12

13− ReadLine : FileIO (OpenFile Read) (OpenFile Read) String

13+data FileIO : Effect where

14− WriteLine : String -> FileIO (OpenFile Write) (OpenFile Write) ()

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

15− EOF : FileIO (OpenFile Read) (OpenFile Read) Bool

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

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

16

17

18+ ReadLine : {OpenFile Read} FileIO String

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

20+ EOF : {OpenFile Read} FileIO Bool

17

21

18instance Handler FileIO IO where

22instance Handler FileIO IO where

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

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

20 valid <- validFile h

24 valid <- validFile h

21− if valid then k (Right (FH h)) True

25+ if valid then k True (FH h)

22− else k (Left ()) False

26+ else k False ()

23 handle (FH h) Close k = do closeFile h

27 handle (FH h) Close k = do closeFile h

24 k () ()

28 k () ()

25 handle (FH h) ReadLine k = do str <- fread h

29 handle (FH h) ReadLine k = do str <- fread h

26− k (FH h) str

30+ k str (FH h)

27 handle (FH h) (WriteLine str) k = do fwrite h str

31 handle (FH h) (WriteLine str) k = do fwrite h str

28− k (FH h) ()

32+ k () (FH h)

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

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

30− k (FH h) e

34+ k e (FH h)

31−

32−instance Handler FileIO (IOExcept String) where

33− handle () (Open fname m) k

34− = do h <- ioe_lift (openFile fname m)

35− valid <- ioe_lift (validFile h)

36− if valid then k (Right (FH h)) True

37− else k (Left ()) False

38− handle (FH h) Close k = do ioe_lift (closeFile h); k () ()

39− handle (FH h) ReadLine k = do str <- ioe_lift (fread h)

40− k (FH h) str

41− handle (FH h) (WriteLine str) k = do ioe_lift (fwrite h str)

42− k (FH h) ()

43− handle (FH h) EOF k = do e <- ioe_lift (feof h)

44− k (FH h) e

45

35

46FILE_IO : Type -> EFFECT

36FILE_IO : Type -> EFFECT

47FILE_IO t = MkEff t FileIO

37FILE_IO t = MkEff t FileIO

48

38

49open : Handler FileIO e =>

39open : Handler FileIO e =>

50− String -> (m : Mode) -> EffM e [FILE_IO ()]

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

51− [FILE_IO (Either () (OpenFile m))] Bool

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

52open f m = Open f m

42open f m = Open f m

53

43

54close : Handler FileIO e =>

44close : Handler FileIO e =>

55− EffM e [FILE_IO (OpenFile m)] [FILE_IO ()] ()

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

56close = Close

46close = Close

57

47

48+readLine : Handler FileIO e =>

58−readLine : Handler FileIO e => Eff e [FILE_IO (OpenFile Read)] String

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

59readLine = ReadLine

50readLine = ReadLine

60

51

52+writeLine : Handler FileIO e =>

61−writeLine : Handler FileIO e => String -> Eff e [FILE_IO (OpenFile Write)] ()

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

62writeLine str = WriteLine str

54writeLine str = WriteLine str

63

55

56+eof : Handler FileIO e =>

64−eof : Handler FileIO e => Eff e [FILE_IO (OpenFile Read)] Bool

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

65eof = EOF

58eof = EOF

66

59

67

60

libs/effects/Effect/Memory.idr+31−25

@@ -12,29 +12,30 @@ data MemoryChunk : Nat -> Nat -> Type where

12abstract

13data RawMemory : Effect where

14 Allocate : (n : Nat) ->

15− RawMemory () (MemoryChunk n 0) ()

15+ RawMemory () () (\v => MemoryChunk n 0)

16− Free : RawMemory (MemoryChunk n i) () ()

16+ Free : RawMemory () (MemoryChunk n i) (\v => ())

17 Initialize : Bits8 ->

18 (size : Nat) ->

19 so (i + size <= n) ->

20− RawMemory (MemoryChunk n i) (MemoryChunk n (i + size)) ()

20+ RawMemory () (MemoryChunk n i) (\v => MemoryChunk n (i + size))

21 Peek : (offset : Nat) ->

22 (size : Nat) ->

23 so (offset + size <= i) ->

24− RawMemory (MemoryChunk n i) (MemoryChunk n i) (Vect size Bits8)

24+ RawMemory (Vect size Bits8)

25+ (MemoryChunk n i) (\v => MemoryChunk n i)

25 Poke : (offset : Nat) ->

26 Poke : (offset : Nat) ->

26 (Vect size Bits8) ->

27 (Vect size Bits8) ->

27 so (offset <= i && offset + size <= n) ->

28 so (offset <= i && offset + size <= n) ->

28− RawMemory (MemoryChunk n i) (MemoryChunk n (max i (offset + size))) ()

29+ RawMemory () (MemoryChunk n i) (\v => MemoryChunk n (max i (offset + size)))

29 Move : (src : MemoryChunk src_size src_init) ->

30 Move : (src : MemoryChunk src_size src_init) ->

30 (dst_offset : Nat) ->

31 (dst_offset : Nat) ->

31 (src_offset : Nat) ->

32 (src_offset : Nat) ->

32 (size : Nat) ->

33 (size : Nat) ->

33 so (dst_offset <= dst_init && dst_offset + size <= dst_size) ->

34 so (dst_offset <= dst_init && dst_offset + size <= dst_size) ->

34 so (src_offset + size <= src_init) ->

35 so (src_offset + size <= src_init) ->

35− RawMemory (MemoryChunk dst_size dst_init)

36+ RawMemory () (MemoryChunk dst_size dst_init)

36− (MemoryChunk dst_size (max dst_init (dst_offset + size))) ()

37+ (\v => MemoryChunk dst_size (max dst_init (dst_offset + size)))

37− GetRawPtr : RawMemory (MemoryChunk n i) (MemoryChunk n i) (MemoryChunk n i)

38+ GetRawPtr : RawMemory (MemoryChunk n i) (MemoryChunk n i) (\v => MemoryChunk n i)

38

39

39private

40private

40do_malloc : Nat -> IOExcept String Ptr

41do_malloc : Nat -> IOExcept String Ptr

@@ -79,27 +80,28 @@ do_poke ptr offset (b::bs)

79instance Handler RawMemory (IOExcept String) where

80instance Handler RawMemory (IOExcept String) where

80 handle () (Allocate n) k

81 handle () (Allocate n) k

81 = do ptr <- do_malloc n

82 = do ptr <- do_malloc n

82− k (CH ptr) ()

83+ k () (CH ptr)

83− handle (CH ptr) (Initialize {i} c size _) k

84+ handle {-{res = MemoryChunk _ offset}-} (CH ptr) (Initialize {i} c size _) k

84− = ioe_lift (do_memset ptr i c size) $> k (CH ptr) ()

85+ = ioe_lift (do_memset ptr i c size) $> k () (CH ptr)

85 handle (CH ptr) (Free) k

86 handle (CH ptr) (Free) k

86 = ioe_lift (do_free ptr) $> k () ()

87 = ioe_lift (do_free ptr) $> k () ()

87 handle (CH ptr) (Peek offset size _) k

88 handle (CH ptr) (Peek offset size _) k

88 = do res <- ioe_lift (do_peek ptr offset size)

89 = do res <- ioe_lift (do_peek ptr offset size)

89− k (CH ptr) res

90+ k res (CH ptr)

90 handle (CH ptr) (Poke offset content _) k

91 handle (CH ptr) (Poke offset content _) k

91 = do ioe_lift (do_poke ptr offset content)

92 = do ioe_lift (do_poke ptr offset content)

92− k (CH ptr) ()

93+ k () (CH ptr)

93 handle (CH dest_ptr) (Move (CH src_ptr) dest_offset src_offset size _ _) k

94 handle (CH dest_ptr) (Move (CH src_ptr) dest_offset src_offset size _ _) k

94 = do ioe_lift (do_memmove dest_ptr src_ptr dest_offset src_offset size)

95 = do ioe_lift (do_memmove dest_ptr src_ptr dest_offset src_offset size)

95− k (CH dest_ptr) ()

96+ k () (CH dest_ptr)

96 handle chunk (GetRawPtr) k

97 handle chunk (GetRawPtr) k

97 = k chunk chunk

98 = k chunk chunk

98

99

99RAW_MEMORY : Type -> EFFECT

100RAW_MEMORY : Type -> EFFECT

100RAW_MEMORY t = MkEff t RawMemory

101RAW_MEMORY t = MkEff t RawMemory

101

102

103+allocate : (n : Nat) ->

102−allocate : (n : Nat) -> EffM m [RAW_MEMORY ()] [RAW_MEMORY (MemoryChunk n 0)] ()

104+ Eff m () [RAW_MEMORY ()] (\v => [RAW_MEMORY (MemoryChunk n 0)])

103allocate size = Allocate size

105allocate size = Allocate size

104

106

105initialize : {i : Nat} ->

107initialize : {i : Nat} ->

@@ -107,17 +109,18 @@ initialize : {i : Nat} ->

107 Bits8 ->

109 Bits8 ->

108 (size : Nat) ->

110 (size : Nat) ->

109 so (i + size <= n) ->

111 so (i + size <= n) ->

112+ Eff m () [RAW_MEMORY (MemoryChunk n i)]

110− EffM m [RAW_MEMORY (MemoryChunk n i)] [RAW_MEMORY (MemoryChunk n (i + size))] ()

113+ (\v => [RAW_MEMORY (MemoryChunk n (i + size))])

111initialize c size prf = Initialize c size prf

114initialize c size prf = Initialize c size prf

112

115

113−free : EffM m [RAW_MEMORY (MemoryChunk n i)] [RAW_MEMORY ()] ()

116+free : Eff m () [RAW_MEMORY (MemoryChunk n i)] (\v => [RAW_MEMORY ()])

114free = Free

117free = Free

115

118

116peek : {i : Nat} ->

119peek : {i : Nat} ->

117 (offset : Nat) ->

120 (offset : Nat) ->

118 (size : Nat) ->

121 (size : Nat) ->

119 so (offset + size <= i) ->

122 so (offset + size <= i) ->

120− Eff m [RAW_MEMORY (MemoryChunk n i)] (Vect size Bits8)

123+ { [RAW_MEMORY (MemoryChunk n i)] } Eff m (Vect size Bits8)

121peek offset size prf = Peek offset size prf

124peek offset size prf = Peek offset size prf

122

125

123poke : {n : Nat} ->

126poke : {n : Nat} ->

@@ -125,11 +128,12 @@ poke : {n : Nat} ->

125 (offset : Nat) ->

128 (offset : Nat) ->

126 Vect size Bits8 ->

129 Vect size Bits8 ->

127 so (offset <= i && offset + size <= n) ->

130 so (offset <= i && offset + size <= n) ->

131+ Eff m () [RAW_MEMORY (MemoryChunk n i)]

128− EffM m [RAW_MEMORY (MemoryChunk n i)] [RAW_MEMORY (MemoryChunk n (max i (offset + size)))] ()

132+ (\v => [RAW_MEMORY (MemoryChunk n (max i (offset + size)))])

129poke offset content prf = Poke offset content prf

133poke offset content prf = Poke offset content prf

130

134

131private

135private

132−getRawPtr : Eff m [RAW_MEMORY (MemoryChunk n i)] (MemoryChunk n i)

136+getRawPtr : { [RAW_MEMORY (MemoryChunk n i)] } Eff m (MemoryChunk n i)

133getRawPtr = GetRawPtr

137getRawPtr = GetRawPtr

134

138

135private

139private

@@ -142,8 +146,8 @@ move' : {dst_size : Nat} ->

142 (size : Nat) ->

146 (size : Nat) ->

143 so (dst_offset <= dst_init && dst_offset + size <= dst_size) ->

147 so (dst_offset <= dst_init && dst_offset + size <= dst_size) ->

144 so (src_offset + size <= src_init) ->

148 so (src_offset + size <= src_init) ->

145− EffM m [RAW_MEMORY (MemoryChunk dst_size dst_init)]

149+ Eff m () [RAW_MEMORY (MemoryChunk dst_size dst_init)]

146− [RAW_MEMORY (MemoryChunk dst_size (max dst_init (dst_offset + size)))] ()

150+ (\v => [RAW_MEMORY (MemoryChunk dst_size (max dst_init (dst_offset + size)))])

147move' src_ptr dst_offset src_offset size dst_bounds src_bounds

151move' src_ptr dst_offset src_offset size dst_bounds src_bounds

148 = Move src_ptr dst_offset src_offset size dst_bounds src_bounds

152 = Move src_ptr dst_offset src_offset size dst_bounds src_bounds

149

153

@@ -158,10 +162,12 @@ move : {dst_size : Nat} ->

158 (size : Nat) ->

162 (size : Nat) ->

159 so (dst_offset <= dst_init && dst_offset + size <= dst_size) ->

163 so (dst_offset <= dst_init && dst_offset + size <= dst_size) ->

160 so (src_offset + size <= src_init) ->

164 so (src_offset + size <= src_init) ->

165+ Eff m ()

161− EffM m [ Dst ::: RAW_MEMORY (MemoryChunk dst_size dst_init)

166+ [ Dst ::: RAW_MEMORY (MemoryChunk dst_size dst_init)

162 , Src ::: RAW_MEMORY (MemoryChunk src_size src_init)]

167 , Src ::: RAW_MEMORY (MemoryChunk src_size src_init)]

168+ (\v =>

163− [ Dst ::: RAW_MEMORY (MemoryChunk dst_size (max dst_init (dst_offset + size)))

169+ [ Dst ::: RAW_MEMORY (MemoryChunk dst_size (max dst_init (dst_offset + size)))

164− , Src ::: RAW_MEMORY (MemoryChunk src_size src_init)] ()

170+ , Src ::: RAW_MEMORY (MemoryChunk src_size src_init)])

165move dst_offset src_offset size dst_bounds src_bounds

171move dst_offset src_offset size dst_bounds src_bounds

166 = do src_ptr <- Src :- getRawPtr

172 = do src_ptr <- Src :- getRawPtr

167 Dst :- move' src_ptr dst_offset src_offset size dst_bounds src_bounds

173 Dst :- move' src_ptr dst_offset src_offset size dst_bounds src_bounds

libs/effects/Effect/Monad.idr+4−4

@@ -5,17 +5,17 @@ import Effects

5-- Eff is a monad too, so we can happily use it in a monad transformer.

6

7using (xs : List EFFECT, m : Type -> Type)

8− instance Functor (EffM m xs xs) where

8+ instance Functor (\a => EffM m a xs (\v => xs)) where

9 map f prog = do t <- prog

10 value (f t)

11

12− instance Applicative (EffM m xs xs) where

12+ instance Applicative (\a => EffM m a xs (\v => xs)) where

13 pure = value

14 (<$>) f a = do f' <- f

15 a' <- a

16 value (f' a')

17

18− instance Monad (EffM m xs xs) where

18+ instance Monad (\a => Eff m a xs (\v => xs)) where

19− (>>=) = ebind

19+ (>>=) = Effects.(>>=)

20

21

libs/effects/Effect/Random.idr+14−6

@@ -2,24 +2,32 @@ module Effect.Random

2

3import Effects

4

5−data Random : Type -> Type -> Type -> Type where

5+data Random : Effect where

6− getRandom : Random Integer Integer Integer

6+ getRandom : { Integer } Random Integer

7− setSeed : Integer -> Random Integer Integer ()

7+ setSeed : Integer -> { Integer } Random ()

8

9using (m : Type -> Type)

10 instance Handler Random m where

11 handle seed getRandom k

12 = let seed' = (1664525 * seed + 1013904223) `prim__sremBigInt` (pow 2 32) in

13 k seed' seed'

14− handle seed (setSeed n) k = k n ()

14+ handle seed (setSeed n) k = k () n

15

16RND : EFFECT

17RND = MkEff Integer Random

18

19−rndInt : Integer -> Integer -> Eff m [RND] Integer

19+rndInt : Integer -> Integer -> { [RND] } Eff m Integer

20rndInt lower upper = do v <- getRandom

21 return (v `prim__sremBigInt` (upper - lower) + lower)

22

23+rndFin : (k : Nat) -> { [RND] } Eff m (Fin (S k))

24+rndFin k = do let v = !getRandom `prim__sremBigInt` (cast k)

25+ return (toFin v)

26+ where toFin : Integer -> Fin (S k)

27+ toFin x = case integerToFin x (S k) of

28+ Just v => v

29+ Nothing => toFin (assert_smaller x (x - cast (S k)))

30+

23−srand : Integer -> Eff m [RND] ()

31+srand : Integer -> { [RND] } Eff m ()

24srand n = setSeed n

32srand n = setSeed n

25

33

libs/effects/Effect/Select.idr+4−4

@@ -3,21 +3,21 @@ module Effect.Select

3import Effects

4

5data Selection : Effect where

6− Select : List a -> Selection () () a

6+ Select : List a -> { () } Selection a

7

8instance Handler Selection Maybe where

9 handle _ (Select xs) k = tryAll xs where

10 tryAll [] = Nothing

11− tryAll (x :: xs) = case k () x of

11+ tryAll (x :: xs) = case k x () of

12 Nothing => tryAll xs

13 Just v => Just v

14

15instance Handler Selection List where

16− handle r (Select xs) k = concatMap (k r) xs

16+ handle r (Select xs) k = concatMap (\x => k x r) xs

17

18SELECT : EFFECT

19SELECT = MkEff () Selection

20

21−select : List a -> Eff m [SELECT] a

21+select : List a -> { [SELECT] } Eff m a

22select xs = Select xs

23

libs/effects/Effect/State.idr+9−9

@@ -5,33 +5,33 @@ import Effects

5%access public

6

7data State : Effect where

8− Get : State a a a

8+ Get : { a } State a

9− Put : b -> State a b ()

9+ Put : b -> { a ==> b } State ()

10

11using (m : Type -> Type)

12 instance Handler State m where

13 handle st Get k = k st st

14− handle st (Put n) k = k n ()

14+ handle st (Put n) k = k () n

15

16STATE : Type -> EFFECT

17STATE t = MkEff t State

18

19−get : Eff m [STATE x] x

19+get : { [STATE x] } Eff m x

20get = Get

21

22−put : x -> Eff m [STATE x] ()

22+put : x -> { [STATE x] } Eff m ()

23put val = Put val

24

25−putM : y -> EffM m [STATE x] [STATE y] ()

25+putM : y -> { [STATE x] ==> [STATE y] } Eff m ()

26putM val = Put val

27

28−update : (x -> x) -> Eff m [STATE x] ()

28+update : (x -> x) -> { [STATE x] } Eff m ()

29update f = put (f !get)

30

31−updateM : (x -> y) -> EffM m [STATE x] [STATE y] ()

31+updateM : (x -> y) -> { [STATE x] ==> [STATE y] } Eff m ()

32updateM f = putM (f !get)

33

34−locally : x -> Eff m [STATE x] t -> Eff m [STATE y] t

34+locally : x -> ({ [STATE x] } Eff m t) -> { [STATE y] } Eff m t

35locally newst prog = do st <- get

36 putM newst

37 val <- prog

libs/effects/Effect/StdIO.idr+19−36

@@ -4,57 +4,40 @@ import Effects

4import Control.IOExcept

5

6data StdIO : Effect where

7− PutStr : String -> StdIO () () ()

7+ PutStr : String -> { () } StdIO ()

8− GetStr : StdIO () () String

8+ GetStr : { () } StdIO String

9+ PutCh : Char -> { () } StdIO ()

10+ GetCh : { () } StdIO Char

9

11

10instance Handler StdIO IO where

12instance Handler StdIO IO where

11 handle () (PutStr s) k = do putStr s; k () ()

13 handle () (PutStr s) k = do putStr s; k () ()

12− handle () GetStr k = do x <- getLine; k () x

14+ handle () GetStr k = do x <- getLine; k x ()

15+ handle () (PutCh c) k = do putChar c; k () ()

16+ handle () GetCh k = do x <- getChar; k x ()

13

17

14instance Handler StdIO (IOExcept a) where

18instance Handler StdIO (IOExcept a) where

15− handle () (PutStr s) k = do ioe_lift (putStr s); k () ()

19+ handle () (PutStr s) k = do ioe_lift $ putStr s; k () ()

16− handle () GetStr k = do x <- ioe_lift getLine; k () x

20+ handle () GetStr k = do x <- ioe_lift $ getLine; k x ()

17−

21+ handle () (PutCh c) k = do ioe_lift $ putChar c; k () ()

18−-- Handle effects in a pure way, for simulating IO for unit testing/proof

22+ handle () GetCh k = do x <- ioe_lift $ getChar; k x ()

19−

20−data IOStream a = MkStream (List String -> (a, List String))

21−

22−instance Handler StdIO IOStream where

23− handle () (PutStr s) k

24− = MkStream (\x => case k () () of

25− MkStream f => let (res, str) = f x in

26− (res, s :: str))

27− handle {a} () GetStr k

28− = MkStream (\x => case x of

29− [] => cont "" []

30− (t :: ts) => cont t ts)

31− where

32− cont : String -> List String -> (a, List String)

33− cont t ts = case k () t of

34− MkStream f => f ts

35

23

36--- The Effect and associated functions

24--- The Effect and associated functions

37

25

38STDIO : EFFECT

26STDIO : EFFECT

39STDIO = MkEff () StdIO

27STDIO = MkEff () StdIO

40

28

41−putStr : Handler StdIO e => String -> Eff e [STDIO] ()

29+putStr : Handler StdIO e => String -> { [STDIO] } Eff e ()

42putStr s = PutStr s

30putStr s = PutStr s

43

31

32+putChar : Handler StdIO e => Char -> { [STDIO] } Eff e ()

33+putChar c = PutCh c

34+

44−putStrLn : Handler StdIO e => String -> Eff e [STDIO] ()

35+putStrLn : Handler StdIO e => String -> { [STDIO] } Eff e ()

45putStrLn s = putStr (s ++ "\n")

36putStrLn s = putStr (s ++ "\n")

46

37

47−getStr : Handler StdIO e => Eff e [STDIO] String

38+getStr : Handler StdIO e => { [STDIO] } Eff e String

48getStr = GetStr

39getStr = GetStr

49

40

50−mkStrFn : Env IOStream xs ->

41+getChar : Handler StdIO e => { [STDIO] } Eff e Char

51− Eff IOStream xs a ->

42+getChar = GetCh

52− List String -> (a, List String)

53−mkStrFn {a} env p input = case mkStrFn' of

54− MkStream f => f input

55− where injStream : a -> IOStream a

56− injStream v = MkStream (\x => (v, []))

57− mkStrFn' : IOStream a

58− mkStrFn' = runWith injStream env p

59−

60

43

libs/neweffects/Effect/System.idr → libs/effects/Effect/System.idrrenamed

The content is the same.

libs/effects/Effects.idr+150−142

@@ -2,20 +2,34 @@ module Effects

2

3import Language.Reflection

4import Control.Catchable

5+import Effect.Default

5

6

6%access public

7%access public

7

8

8---- Effects

9---- Effects

9

10

10Effect : Type

11Effect : Type

11−Effect = Type -> Type -> Type -> Type

12+Effect = (x : Type) -> Type -> (x -> Type) -> Type

12

13

13%error_reverse

14%error_reverse

14data EFFECT : Type where

15data EFFECT : Type where

15 MkEff : Type -> Effect -> EFFECT

16 MkEff : Type -> Effect -> EFFECT

16

17

17class Handler (e : Effect) (m : Type -> Type) where

18class Handler (e : Effect) (m : Type -> Type) where

18− handle : res -> (eff : e res res' t) -> (res' -> t -> m a) -> m a

19+ handle : res -> (eff : e t res resk) ->

20+ ((x : t) -> resk x -> m a) -> m a

21+

22+-- Get the resource type (handy at the REPL to find out about an effect)

23+resourceType : EFFECT -> Type

24+resourceType (MkEff t e) = t

25+

26+-- A bit of syntactic sugar ('syntax' is not very flexible so we only go

27+-- up to a small number of parameters...)

28+

29+syntax "{" [inst] "}" [eff] = eff inst (\result => inst)

30+syntax "{" [inst] "==>" "{" {b} "}" [outst] "}" [eff]

31+ = eff inst (\b => outst)

32+syntax "{" [inst] "==>" [outst] "}" [eff] = eff inst (\result => outst)

19

33

20---- Properties and proof construction

34---- Properties and proof construction

21

35

@@ -29,11 +43,12 @@ using (xs : List a, ys : List a)

29 subListId {xs = Nil} = SubNil

43 subListId {xs = Nil} = SubNil

30 subListId {xs = x :: xs} = Keep subListId

44 subListId {xs = x :: xs} = Keep subListId

31

45

46+namespace Env

32−data Env : (m : Type -> Type) -> List EFFECT -> Type where

47+ data Env : (m : Type -> Type) -> List EFFECT -> Type where

33− Nil : Env m Nil

48+ Nil : Env m Nil

34− (::) : Handler eff m => a -> Env m xs -> Env m (MkEff a eff :: xs)

49+ (::) : Handler eff m => a -> Env m xs -> Env m (MkEff a eff :: xs)

35−

50+

36−data EffElem : (Type -> Type -> Type -> Type) -> Type ->

51+data EffElem : Effect -> Type ->

37 List EFFECT -> Type where

52 List EFFECT -> Type where

38 Here : EffElem x a (MkEff a x :: xs)

53 Here : EffElem x a (MkEff a x :: xs)

39 There : EffElem x a xs -> EffElem x a (y :: xs)

54 There : EffElem x a xs -> EffElem x a (y :: xs)

@@ -79,7 +94,7 @@ reflectListEffElem _ = Refine "Here" `Seq` Solve

79

94

80%reflection

95%reflection

81reflectSubList : List a -> Tactic

96reflectSubList : List a -> Tactic

82−reflectSubList [] = Refine "SubNil" `Seq` Solve

97+reflectSubList [] = Refine "subListId" `Seq` Solve

83reflectSubList (x :: xs)

98reflectSubList (x :: xs)

84 = Try (Refine "subListId" `Seq` Solve)

99 = Try (Refine "subListId" `Seq` Solve)

85 (Try (Refine "Keep" `Seq` (Solve `Seq` reflectSubList xs))

100 (Try (Refine "Keep" `Seq` (Solve `Seq` reflectSubList xs))

@@ -87,22 +102,39 @@ reflectSubList (x :: xs)

87reflectSubList (x ++ y) = Refine "subListId" `Seq` Solve

102reflectSubList (x ++ y) = Refine "subListId" `Seq` Solve

88reflectSubList _ = Refine "subListId" `Seq` Solve

103reflectSubList _ = Refine "subListId" `Seq` Solve

89

104

105+%reflection

106+reflectDefaultList : List a -> Tactic

107+reflectDefaultList [] = Refine "enil" `Seq` Solve

108+reflectDefaultList (x :: xs)

109+ = Refine "econs" `Seq`

110+ (Solve `Seq`

111+ (Instance `Seq`

112+ (Refine "default" `Seq`

113+ (Solve `Seq`

114+ (Instance `Seq`

115+ (reflectDefaultList xs))))))

116+reflectDefaultList (x ++ y) = Refine "Nil" `Seq` Solve

117+reflectDefaultList _ = Refine "Nil" `Seq` Solve

118+

90%reflection

119%reflection

91reflectEff : (P : Type) -> Tactic

120reflectEff : (P : Type) -> Tactic

92reflectEff (EffElem m a xs)

121reflectEff (EffElem m a xs)

93 = reflectListEffElem xs `Seq` Solve

122 = reflectListEffElem xs `Seq` Solve

94reflectEff (SubList xs ys)

123reflectEff (SubList xs ys)

95 = reflectSubList ys `Seq` Solve

124 = reflectSubList ys `Seq` Solve

125+reflectEff (Env m xs)

126+ = reflectDefaultList xs `Seq` Solve

96

127

128+updateResTy : (val : t) ->

97−updateResTy : (xs : List EFFECT) -> EffElem e a xs -> e a b t ->

129+ (xs : List EFFECT) -> EffElem e a xs -> e t a b ->

98 List EFFECT

130 List EFFECT

99−updateResTy {b} (MkEff a e :: xs) Here n = (MkEff b e) :: xs

131+updateResTy {b} val (MkEff a e :: xs) Here n = (MkEff (b val) e) :: xs

100−updateResTy (x :: xs) (There p) n = x :: updateResTy xs p n

132+updateResTy val (x :: xs) (There p) n = x :: updateResTy val xs p n

101

133

102−updateResTyImm : (xs : List EFFECT) -> EffElem e a xs -> Type ->

134+-- updateResTyImm : (xs : List EFFECT) -> EffElem e a xs -> Type ->

103− List EFFECT

135+-- List EFFECT

104−updateResTyImm (MkEff a e :: xs) Here b = (MkEff b e) :: xs

136+-- updateResTyImm (MkEff a e :: xs) Here b = (MkEff b e) :: xs

105−updateResTyImm (x :: xs) (There p) b = x :: updateResTyImm xs p b

137+-- updateResTyImm (x :: xs) (There p) b = x :: updateResTyImm xs p b

106

138

107infix 5 :::, :-, :=

139infix 5 :::, :-, :=

108

140

@@ -110,93 +142,67 @@ data LRes : lbl -> Type -> Type where

110 (:=) : (x : lbl) -> res -> LRes x res

142 (:=) : (x : lbl) -> res -> LRes x res

111

143

112(:::) : lbl -> EFFECT -> EFFECT

144(:::) : lbl -> EFFECT -> EFFECT

113−(:::) {lbl} x (MkEff r eff) = MkEff (LRes x r) eff

145+(:::) {lbl} x (MkEff r e) = MkEff (LRes x r) e

146+

147+using (lbl : Type)

148+ instance Default a => Default (LRes lbl a) where

149+ default = lbl := default

114

150

115private

151private

116unlabel : {l : ty} -> Env m [l ::: x] -> Env m [x]

152unlabel : {l : ty} -> Env m [l ::: x] -> Env m [x]

117unlabel {m} {x = MkEff a eff} [l := v] = [v]

153unlabel {m} {x = MkEff a eff} [l := v] = [v]

118

154

119private

155private

120−relabel : (l : ty) -> Env m [x] -> Env m [l ::: x]

156+relabel : (l : ty) -> Env m xs -> Env m (map (\x => l ::: x) xs)

157+relabel {xs = []} l [] = []

121−relabel {x = MkEff a eff} l [v] = [l := v]

158+relabel {xs = (MkEff a e :: xs)} l (v :: vs) = (l := v) :: relabel l vs

122

159

123-- the language of Effects

160-- the language of Effects

124

161

125−data EffM : (m : Type -> Type) ->

162+data Eff : (m : Type -> Type) ->

163+ (x : Type) ->

126− List EFFECT -> List EFFECT -> Type -> Type where

164+ List EFFECT -> (x -> List EFFECT) -> Type where

127− value : a -> EffM m xs xs a

165+ value : a -> Eff m a xs (\v => xs)

166+ with_val : (val : a) -> Eff m () xs (\v => xs' val) ->

167+ Eff m a xs xs'

128− ebind : EffM m xs xs' a -> (a -> EffM m xs' xs'' b) -> EffM m xs xs'' b

168+ ebind : Eff m a xs xs' ->

169+ ((val : a) -> Eff m b (xs' val) xs'') -> Eff m b xs xs''

129− effect : (prf : EffElem e a xs) ->

170+ effect : (prf : EffElem e a xs) ->

130− (eff : e a b t) ->

171+ (eff : e t a b) ->

131− EffM m xs (updateResTy xs prf eff) t

172+ Eff m t xs (\v => updateResTy v xs prf eff)

173+

132− lift : (prf : SubList ys xs) ->

174+ lift : (prf : SubList ys xs) ->

133− EffM m ys ys' t -> EffM m xs (updateWith ys' xs prf) t

175+ Eff m t ys ys' -> Eff m t xs (\v => updateWith (ys' v) xs prf)

134− new : Handler e m =>

176+ newInit : Handler e m =>

177+ res ->

135− res -> EffM m (MkEff res e :: xs) (MkEff res' e :: xs') a ->

178+ Eff m a (MkEff res e :: xs) (\v => (MkEff res' e :: xs')) ->

136− EffM m xs xs' a

179+ Eff m a xs (\v => xs')

137− test : (prf : EffElem e (Either l r) xs) ->

138− EffM m (updateResTyImm xs prf l) xs' t ->

139− EffM m (updateResTyImm xs prf r) xs' t ->

140− EffM m xs xs' t

141− test_lbl : {x : lbl} ->

142− (prf : EffElem e (LRes x (Either l r)) xs) ->

143− EffM m (updateResTyImm xs prf (LRes x l)) xs' t ->

144− EffM m (updateResTyImm xs prf (LRes x r)) xs' t ->

145− EffM m xs xs' t

146− catch : Catchable m err =>

180+ catch : Catchable m err =>

147− EffM m xs xs' a -> (err -> EffM m xs xs' a) ->

181+ Eff m a xs xs' -> (err -> Eff m a xs xs') ->

148− EffM m xs xs' a

182+ Eff m a xs xs'

149− (:-) : (l : ty) -> EffM m [x] [y] t -> EffM m [l ::: x] [l ::: y] t

183+

150−

184+ (:-) : (l : ty) ->

151−syntax [tag] ":!" [val] = !(tag :- val)

185+ Eff m t [x] xs' -> -- [x] (\v => xs) ->

152−

186+ Eff m t [l ::: x] (\v => map (l :::) (xs' v))

153−-- Eff : List (EFFECT m) -> Type -> Type

187+

154−

188+(>>=) : Eff m a xs xs' ->

155−-- For making proofs implicitly for 'test' and 'test_lbl'

189+ ((val : a) -> Eff m b (xs' val) xs'') -> Eff m b xs xs''

156−

190+(>>=) = ebind

157−syntax if_valid then [e] else [t] =

191+

158− test (tactics { byReflection reflectEff; }) t e

159−

160−syntax if_valid [lbl] then [e] else [t] =

161− test_lbl {x=lbl} (tactics { byReflection reflectEff; }) t e

162−

163−syntax if_error then [t] else [e] =

164− test (tactics { byReflection reflectEff; }) t e

165−

166−syntax if_error [lbl] then [t] else [e] =

167− test_lbl {x=lbl} (tactics { byReflection reflectEff; }) t e

168−

169−-- These may read better in some contexts

170−

171−syntax if_right then [e] else [t] =

172− test (tactics { byReflection reflectEff; }) t e

173−

174−syntax if_right [lbl] then [e] else [t] =

175− test_lbl {x=lbl} (tactics { byReflection reflectEff; }) t e

176−

177−syntax if_left then [t] else [e] =

178− test (tactics { byReflection reflectEff; }) t e

179−

180−syntax if_left [lbl] then [t] else [e] =

181− test_lbl {x=lbl} (tactics { byReflection reflectEff; }) t e

182−

183−

184−-- for 'do' notation

185−

186−return : a -> EffM m xs xs a

192+return : a -> Eff m a xs (\v => xs)

187return x = value x

193return x = value x

188

194

189−(>>=) : EffM m xs xs' a -> (a -> EffM m xs' xs'' b) -> EffM m xs xs'' b

190−(>>=) = ebind

191−

192-- for idiom brackets

195-- for idiom brackets

193

196

194infixl 2 <$>

197infixl 2 <$>

195

198

196−pure : a -> EffM m xs xs a

199+pure : a -> Eff m a xs (\v => xs)

197pure = value

200pure = value

198

201

199−(<$>) : EffM m xs xs (a -> b) -> EffM m xs xs a -> EffM m xs xs b

202+syntax pureM [val] = with_val val (pure ())

203+

204+(<$>) : Eff m (a -> b) xs (\v => xs) ->

205+ Eff m a xs (\v => xs) -> Eff m b xs (\v => xs)

200(<$>) prog v = do fn <- prog

206(<$>) prog v = do fn <- prog

201 arg <- v

207 arg <- v

202 return (fn arg)

208 return (fn arg)

@@ -205,53 +211,28 @@ pure = value

205

211

206private

212private

207execEff : Env m xs -> (p : EffElem e res xs) ->

213execEff : Env m xs -> (p : EffElem e res xs) ->

208− (eff : e res b a) ->

214+ (eff : e a res resk) ->

209− (Env m (updateResTy xs p eff) -> a -> m t) -> m t

215+ ((v : a) -> Env m (updateResTy v xs p eff) -> m t) -> m t

210execEff (val :: env) Here eff' k

216execEff (val :: env) Here eff' k

211− = handle val eff' (\res, v => k (res :: env) v)

217+ = handle val eff' (\v, res => k v (res :: env))

218+-- FIXME: Teach the elaborator to propagate parameters here

212−execEff {e} {res} {b} {a} (val :: env) (There p) eff k

219+execEff {e} {a} {res} {resk} (val :: env) (There p) eff k

213− = execEff {e} {res} {b} {a} env p eff (\env', v => k (val :: env') v)

220+ = execEff {e} {a} {res} {resk} env p eff (\v, env' => k v (val :: env'))

214−

215−private

216−testEff : Env m xs -> (p : EffElem e (Either l r) xs) ->

217− (Env m (updateResTyImm xs p l) -> m b) ->

218− (Env m (updateResTyImm xs p r) -> m b) ->

219− m b

220−testEff (Left err :: env) Here lk rk = lk (err :: env)

221−testEff (Right ok :: env) Here lk rk = rk (ok :: env)

222−testEff (val :: env) (There p) lk rk

223− = testEff env p (\envk => lk (val :: envk))

224− (\envk => rk (val :: envk))

225−

226−private

227−testEffLbl : {x : lblTy} ->

228− Env m xs -> (p : EffElem e (LRes x (Either l r)) xs) ->

229− (Env m (updateResTyImm xs p (LRes x l)) -> m b) ->

230− (Env m (updateResTyImm xs p (LRes x r)) -> m b) ->

231− m b

232−testEffLbl ((lbl := Left err) :: env) Here lk rk = lk ((lbl := err) :: env)

233−testEffLbl ((lbl := Right ok) :: env) Here lk rk = rk ((lbl := ok) :: env)

234−testEffLbl (val :: env) (There p) lk rk

235− = testEffLbl env p (\envk => lk (val :: envk))

236− (\envk => rk (val :: envk))

237

221

238-- Q: Instead of m b, implement as StateT (Env m xs') m b, so that state

222-- Q: Instead of m b, implement as StateT (Env m xs') m b, so that state

239-- updates can be propagated even through failing computations?

223-- updates can be propagated even through failing computations?

240

224

241−eff : Env m xs -> EffM m xs xs' a -> (Env m xs' -> a -> m b) -> m b

225+eff : Env m xs -> Eff m a xs xs' -> ((x : a) -> Env m (xs' x) -> m b) -> m b

242−eff env (value x) k = k env x

226+eff env (value x) k = k x env

227+eff env (with_val x prog) k = eff env prog (\p', env' => k x env')

243eff env (prog `ebind` c) k

228eff env (prog `ebind` c) k

244− = eff env prog (\env', p' => eff env' (c p') k)

229+ = eff env prog (\p', env' => eff env' (c p') k)

245eff env (effect prf effP) k = execEff env prf effP k

230eff env (effect prf effP) k = execEff env prf effP k

246eff env (lift prf effP) k

231eff env (lift prf effP) k

247 = let env' = dropEnv env prf in

232 = let env' = dropEnv env prf in

248− eff env' effP (\envk, p' => k (rebuildEnv envk prf env) p')

233+ eff env' effP (\p', envk => k p' (rebuildEnv envk prf env))

249−eff env (new r prog) k

234+eff env (newInit r prog) k

250− = eff (r :: env) prog (\(v :: envk), p' => k envk p')

235+ = eff (r :: env) prog (\p' => \ (v :: envk) => k p' envk)

251−eff env (test prf l r) k

252− = testEff env prf (\envk => eff envk l k) (\envk => eff envk r k)

253−eff env (test_lbl prf l r) k

254− = testEffLbl env prf (\envk => eff envk l k) (\envk => eff envk r k)

255eff env (catch prog handler) k

236eff env (catch prog handler) k

256 = catch (eff env prog k)

237 = catch (eff env prog k)

257 (\e => eff env (handler e) k)

238 (\e => eff env (handler e) k)

@@ -261,48 +242,75 @@ eff env (catch prog handler) k

261-- end so that everything is in scope when it needs to be.

242-- end so that everything is in scope when it needs to be.

262eff {xs = [l ::: x]} env (l :- prog) k

243eff {xs = [l ::: x]} env (l :- prog) k

263 = let env' = unlabel env in

244 = let env' = unlabel env in

264− eff env' prog (\envk, p' => k (relabel l envk) p')

245+ eff env' prog (\p', envk => k p' (relabel l envk))

246+

247+-- yuck :) Haven't got type class instances working nicely in tactic

248+-- proofs yet, so just brute force it.

249+syntax MkDefaultEnv = with Env

250+ (| [], [default], [default, default],

251+ [default, default, default],

252+ [default, default, default, default],

253+ [default, default, default, default, default],

254+ [default, default, default, default, default, default],

255+ [default, default, default, default, default, default, default],

256+ [default, default, default, default, default, default, default, default] |)

265

257

266implicit

258implicit

267−lift' : EffM m ys ys' t ->

259+lift' : Eff m t ys ys' ->

268 {default tactics { byReflection reflectEff; }

260 {default tactics { byReflection reflectEff; }

269 prf : SubList ys xs} ->

261 prf : SubList ys xs} ->

270− EffM m xs (updateWith ys' xs prf) t

262+ Eff m t xs (\v => updateWith (ys' v) xs prf)

271lift' e {prf} = lift prf e

263lift' e {prf} = lift prf e

272

264

273implicit

265implicit

274effect' : {a, b: _} -> {e : Effect} ->

266effect' : {a, b: _} -> {e : Effect} ->

275− (eff : e a b t) ->

267+ (eff : e t a b) ->

276 {default tactics { byReflection reflectEff; }

268 {default tactics { byReflection reflectEff; }

277 prf : EffElem e a xs} ->

269 prf : EffElem e a xs} ->

278− EffM m xs (updateResTy xs prf eff) t

270+ Eff m t xs (\v => updateResTy v xs prf eff)

279effect' e {prf} = effect prf e

271effect' e {prf} = effect prf e

280

272

273+new : Handler e m =>

274+ {default default r : res} ->

275+ Eff m a (MkEff res e :: xs) (\v => (MkEff res' e :: xs')) ->

276+ Eff m a xs (\v => xs')

277+new {r} e = newInit r e

281

278

282−run : Applicative m => Env m xs -> EffM m xs xs' a -> m a

279+run : Applicative m => {default MkDefaultEnv env : Env m xs} -> Eff m a xs xs' -> m a

283−run env prog = eff env prog (\env, r => pure r)

280+run {env} prog = eff env prog (\r, env => pure r)

284

281

285−runEnv : Applicative m => Env m xs -> EffM m xs xs' a -> m (Env m xs', a)

282+runPure : {default MkDefaultEnv env : Env id xs} -> Eff id a xs xs' -> a

286−runEnv env prog = eff env prog (\env, r => pure (env, r))

283+runPure {env} prog = eff env prog (\r, env => r)

287

284

288−runPure : Env id xs -> EffM id xs xs' a -> a

285+runInit : Applicative m => Env m xs -> Eff m a xs xs' -> m a

289−runPure env prog = eff env prog (\env, r => r)

286+runInit env prog = eff env prog (\r, env => pure r)

290

287

291−-- runPureEnv : Env id xs -> EffM id xs xs' a -> (Env id xs', a)

288+runPureInit : Env id xs -> Eff id a xs xs' -> a

292−-- runPureEnv env prog = eff env prog (\env, r => (env, r))

289+runPureInit env prog = eff env prog (\r, env => r)

293

290

294−runWith : (a -> m a) -> Env m xs -> EffM m xs xs' a -> m a

291+runWith : (a -> m a) -> Env m xs -> Eff m a xs xs' -> m a

295−runWith inj env prog = eff env prog (\env, r => inj r)

292+runWith inj env prog = eff env prog (\r, env => inj r)

296

293

297−Eff : (Type -> Type) -> List EFFECT -> Type -> Type

294+runEnv : Applicative m => Env m xs -> Eff m a xs xs' ->

298−Eff m xs t = EffM m xs xs t

295+ m (x : a ** Env m (xs' x))

296+runEnv env prog = eff env prog (\r, env => pure (r ** env))

299

297

300-- some higher order things

298-- some higher order things

301

299

302−mapE : Applicative m => (a -> Eff m xs b) -> List a -> Eff m xs (List b)

300+mapE : Applicative m => (a -> {xs} Eff m b) -> List a -> {xs} Eff m (List b)

303mapE f [] = pure []

301mapE f [] = pure []

304mapE f (x :: xs) = [| f x :: mapE f xs |]

302mapE f (x :: xs) = [| f x :: mapE f xs |]

305

303

304+

305+mapVE : Applicative m =>

306+ (a -> {xs} Eff m b) ->

307+ Vect n a ->

308+ {xs} Eff m (Vect n b)

309+mapVE f [] = pure []

310+mapVE f (x :: xs) = [| f x :: mapVE f xs |]

311+

312+

306−when : Applicative m => Bool -> Eff m xs () -> Eff m xs ()

313+when : Applicative m => Bool -> ({xs} Eff m ()) -> {xs} Eff m ()

307when True e = e

314when True e = e

308when False e = pure ()

315when False e = pure ()

316+

libs/effects/effects.ipkg+3−2

@@ -1,8 +1,9 @@

1package effects

2

3opts = "--nobasepkgs -i ../prelude -i ../base"

4−modules = Effects,

4+modules = Effects, Effect.Default,

5+

5 Effect.Exception, Effect.File, Effect.State,

6 Effect.Exception, Effect.File, Effect.State,

6 Effect.Random, Effect.StdIO, Effect.Select,

7 Effect.Random, Effect.StdIO, Effect.Select,

7− Effect.Memory, Effect.Monad

8+ Effect.Memory, Effect.System

8

9

libs/neweffects/Effect/File.idrdeleted−62

@@ -1,62 +0,0 @@

1−module Effect.File

2−

3−import Effects

4−import Control.IOExcept

5−

6−data OpenFile : Mode -> Type where

7− FH : File -> OpenFile m

8−

9−openOK : Mode -> Bool -> Type

10−openOK m True = OpenFile m

11−openOK m False = ()

12−

13−data FileIO : Effect where

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

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

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

17−

18− ReadLine : {OpenFile Read} FileIO String

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

20− EOF : {OpenFile Read} FileIO Bool

21−

22−instance Handler FileIO IO where

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

24− valid <- validFile h

25− if valid then k True (FH h)

26− else k False ()

27− handle (FH h) Close k = do closeFile h

28− k () ()

29− handle (FH h) ReadLine k = do str <- fread h

30− k str (FH h)

31− handle (FH h) (WriteLine str) k = do fwrite h str

32− k () (FH h)

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

34− k e (FH h)

35−

36−FILE_IO : Type -> EFFECT

37−FILE_IO t = MkEff t FileIO

38−

39−open : Handler FileIO e =>

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

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

42−open f m = Open f m

43−

44−close : Handler FileIO e =>

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

46−close = Close

47−

48−readLine : Handler FileIO e =>

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

50−readLine = ReadLine

51−

52−writeLine : Handler FileIO e =>

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

54−writeLine str = WriteLine str

55−

56−eof : Handler FileIO e =>

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

58−eof = EOF

59−

60−

61−

62−

libs/neweffects/Effect/Random.idrdeleted−33

@@ -1,33 +0,0 @@

1−module Effect.Random

2−

3−import Effects

4−

5−data Random : Effect where

6− getRandom : { Integer } Random Integer

7− setSeed : Integer -> { Integer } Random ()

8−

9−using (m : Type -> Type)

10− instance Handler Random m where

11− handle seed getRandom k

12− = let seed' = (1664525 * seed + 1013904223) `prim__sremBigInt` (pow 2 32) in

13− k seed' seed'

14− handle seed (setSeed n) k = k () n

15−

16−RND : EFFECT

17−RND = MkEff Integer Random

18−

19−rndInt : Integer -> Integer -> { [RND] } Eff m Integer

20−rndInt lower upper = do v <- getRandom

21− return (v `prim__sremBigInt` (upper - lower) + lower)

22−

23−rndFin : (k : Nat) -> { [RND] } Eff m (Fin (S k))

24−rndFin k = do let v = !getRandom `prim__sremBigInt` (cast k)

25− return (toFin v)

26− where toFin : Integer -> Fin (S k)

27− toFin x = case integerToFin x (S k) of

28− Just v => v

29− Nothing => toFin (assert_smaller x (x - cast (S k)))

30−

31−srand : Integer -> { [RND] } Eff m ()

32−srand n = setSeed n

33−

libs/neweffects/Effect/StdIO.idrdeleted−43

@@ -1,43 +0,0 @@

1−module Effect.StdIO

2−

3−import Effects

4−import Control.IOExcept

5−

6−data StdIO : Effect where

7− PutStr : String -> { () } StdIO ()

8− GetStr : { () } StdIO String

9− PutCh : Char -> { () } StdIO ()

10− GetCh : { () } StdIO Char

11−

12−instance Handler StdIO IO where

13− handle () (PutStr s) k = do putStr s; k () ()

14− handle () GetStr k = do x <- getLine; k x ()

15− handle () (PutCh c) k = do putChar c; k () ()

16− handle () GetCh k = do x <- getChar; k x ()

17−

18−instance Handler StdIO (IOExcept a) where

19− handle () (PutStr s) k = do ioe_lift $ putStr s; k () ()

20− handle () GetStr k = do x <- ioe_lift $ getLine; k x ()

21− handle () (PutCh c) k = do ioe_lift $ putChar c; k () ()

22− handle () GetCh k = do x <- ioe_lift $ getChar; k x ()

23−

24−--- The Effect and associated functions

25−

26−STDIO : EFFECT

27−STDIO = MkEff () StdIO

28−

29−putStr : Handler StdIO e => String -> { [STDIO] } Eff e ()

30−putStr s = PutStr s

31−

32−putChar : Handler StdIO e => Char -> { [STDIO] } Eff e ()

33−putChar c = PutCh c

34−

35−putStrLn : Handler StdIO e => String -> { [STDIO] } Eff e ()

36−putStrLn s = putStr (s ++ "\n")

37−

38−getStr : Handler StdIO e => { [STDIO] } Eff e String

39−getStr = GetStr

40−

41−getChar : Handler StdIO e => { [STDIO] } Eff e Char

42−getChar = GetCh

43−

libs/neweffects/Effects.idrdeleted−311

@@ -1,311 +0,0 @@

1−module Effects

2−

3−import Language.Reflection

4−import Control.Catchable

5−import Effect.Default

6−

7−%access public

8−

9−---- Effects

10−

11−Effect : Type

12−Effect = (x : Type) -> Type -> (x -> Type) -> Type

13−

14−%error_reverse

15−data EFFECT : Type where

16− MkEff : Type -> Effect -> EFFECT

17−

18−class Handler (e : Effect) (m : Type -> Type) where

19− handle : res -> (eff : e t res resk) ->

20− ((x : t) -> resk x -> m a) -> m a

21−

22−-- Get the resource type (handy at the REPL to find out about an effect)

23−resourceType : EFFECT -> Type

24−resourceType (MkEff t e) = t

25−

26−-- A bit of syntactic sugar ('syntax' is not very flexible so we only go

27−-- up to a small number of parameters...)

28−

29−syntax "{" [inst] "}" [eff] = eff inst (\result => inst)

30−syntax "{" [inst] "==>" "{" {b} "}" [outst] "}" [eff]

31− = eff inst (\b => outst)

32−syntax "{" [inst] "==>" [outst] "}" [eff] = eff inst (\result => outst)

33−

34−---- Properties and proof construction

35−

36−using (xs : List a, ys : List a)

37− data SubList : List a -> List a -> Type where

38− SubNil : SubList {a} [] []

39− Keep : SubList xs ys -> SubList (x :: xs) (x :: ys)

40− Drop : SubList xs ys -> SubList xs (x :: ys)

41−

42− subListId : SubList xs xs

43− subListId {xs = Nil} = SubNil

44− subListId {xs = x :: xs} = Keep subListId

45−

46−namespace Env

47− data Env : (m : Type -> Type) -> List EFFECT -> Type where

48− Nil : Env m Nil

49− (::) : Handler eff m => a -> Env m xs -> Env m (MkEff a eff :: xs)

50−

51−data EffElem : Effect -> Type ->

52− List EFFECT -> Type where

53− Here : EffElem x a (MkEff a x :: xs)

54− There : EffElem x a xs -> EffElem x a (y :: xs)

55−

56−-- make an environment corresponding to a sub-list

57−dropEnv : Env m ys -> SubList xs ys -> Env m xs

58−dropEnv [] SubNil = []

59−dropEnv (v :: vs) (Keep rest) = v :: dropEnv vs rest

60−dropEnv (v :: vs) (Drop rest) = dropEnv vs rest

61−

62−updateWith : (ys' : List a) -> (xs : List a) ->

63− SubList ys xs -> List a

64−updateWith (y :: ys) (x :: xs) (Keep rest) = y :: updateWith ys xs rest

65−updateWith ys (x :: xs) (Drop rest) = x :: updateWith ys xs rest

66−updateWith [] [] SubNil = []

67−updateWith (y :: ys) [] SubNil = y :: ys

68−updateWith [] (x :: xs) (Keep rest) = []

69−

70−-- put things back, replacing old with new in the sub-environment

71−rebuildEnv : Env m ys' -> (prf : SubList ys xs) ->

72− Env m xs -> Env m (updateWith ys' xs prf)

73−rebuildEnv [] SubNil env = env

74−rebuildEnv (x :: xs) (Keep rest) (y :: env) = x :: rebuildEnv xs rest env

75−rebuildEnv xs (Drop rest) (y :: env) = y :: rebuildEnv xs rest env

76−rebuildEnv (x :: xs) SubNil [] = x :: xs

77−

78−---- The Effect EDSL itself ----

79−

80−-- some proof automation

81−

82−%reflection

83−reflectListEffElem : List a -> Tactic

84−reflectListEffElem [] = Refine "Here" `Seq` Solve

85−reflectListEffElem (x :: xs)

86− = Try (Refine "Here" `Seq` Solve)

87− (Refine "There" `Seq` (Solve `Seq` reflectListEffElem xs))

88−-- TMP HACK! FIXME!

89−-- The evaluator needs a 'function case' to know its a reflection function

90−-- until we propagate that information! Without this, the _ case won't get

91−-- matched.

92−reflectListEffElem (x ++ y) = Refine "Here" `Seq` Solve

93−reflectListEffElem _ = Refine "Here" `Seq` Solve

94−

95−%reflection

96−reflectSubList : List a -> Tactic

97−reflectSubList [] = Refine "subListId" `Seq` Solve

98−reflectSubList (x :: xs)

99− = Try (Refine "subListId" `Seq` Solve)

100− (Try (Refine "Keep" `Seq` (Solve `Seq` reflectSubList xs))

101− (Refine "Drop" `Seq` (Solve `Seq` reflectSubList xs)))

102−reflectSubList (x ++ y) = Refine "subListId" `Seq` Solve

103−reflectSubList _ = Refine "subListId" `Seq` Solve

104−

105−%reflection

106−reflectDefaultList : List a -> Tactic

107−reflectDefaultList [] = Refine "enil" `Seq` Solve

108−reflectDefaultList (x :: xs)

109− = Refine "econs" `Seq`

110− (Solve `Seq`

111− (Instance `Seq`

112− (Refine "default" `Seq`

113− (Solve `Seq`

114− (Instance `Seq`

115− (reflectDefaultList xs))))))

116−reflectDefaultList (x ++ y) = Refine "Nil" `Seq` Solve

117−reflectDefaultList _ = Refine "Nil" `Seq` Solve

118−

119−%reflection

120−reflectEff : (P : Type) -> Tactic

121−reflectEff (EffElem m a xs)

122− = reflectListEffElem xs `Seq` Solve

123−reflectEff (SubList xs ys)

124− = reflectSubList ys `Seq` Solve

125−reflectEff (Env m xs)

126− = reflectDefaultList xs `Seq` Solve

127−

128−updateResTy : (val : t) ->

129− (xs : List EFFECT) -> EffElem e a xs -> e t a b ->

130− List EFFECT

131−updateResTy {b} val (MkEff a e :: xs) Here n = (MkEff (b val) e) :: xs

132−updateResTy val (x :: xs) (There p) n = x :: updateResTy val xs p n

133−

134−-- updateResTyImm : (xs : List EFFECT) -> EffElem e a xs -> Type ->

135−-- List EFFECT

136−-- updateResTyImm (MkEff a e :: xs) Here b = (MkEff b e) :: xs

137−-- updateResTyImm (x :: xs) (There p) b = x :: updateResTyImm xs p b

138−

139−infix 5 :::, :-, :=

140−

141−data LRes : lbl -> Type -> Type where

142− (:=) : (x : lbl) -> res -> LRes x res

143−

144−(:::) : lbl -> EFFECT -> EFFECT

145−(:::) {lbl} x (MkEff r e) = MkEff (LRes x r) e

146−

147−using (lbl : Type)

148− instance Default a => Default (LRes lbl a) where

149− default = lbl := default

150−

151−private

152−unlabel : {l : ty} -> Env m [l ::: x] -> Env m [x]

153−unlabel {m} {x = MkEff a eff} [l := v] = [v]

154−

155−private

156−relabel : (l : ty) -> Env m xs -> Env m (map (\x => l ::: x) xs)

157−relabel {xs = []} l [] = []

158−relabel {xs = (MkEff a e :: xs)} l (v :: vs) = (l := v) :: relabel l vs

159−

160−-- the language of Effects

161−

162−data Eff : (m : Type -> Type) ->

163− (x : Type) ->

164− List EFFECT -> (x -> List EFFECT) -> Type where

165− value : a -> Eff m a xs (\v => xs)

166− ebind : Eff m a xs xs' ->

167− ((val : a) -> Eff m b (xs' val) xs'') -> Eff m b xs xs''

168− effect : (prf : EffElem e a xs) ->

169− (eff : e t a b) ->

170− Eff m t xs (\v => updateResTy v xs prf eff)

171−

172− lift : (prf : SubList ys xs) ->

173− Eff m t ys ys' -> Eff m t xs (\v => updateWith (ys' v) xs prf)

174− newInit : Handler e m =>

175− res ->

176− Eff m a (MkEff res e :: xs) (\v => (MkEff res' e :: xs')) ->

177− Eff m a xs (\v => xs')

178− catch : Catchable m err =>

179− Eff m a xs xs' -> (err -> Eff m a xs xs') ->

180− Eff m a xs xs'

181−

182− (:-) : (l : ty) ->

183− Eff m t [x] xs' -> -- [x] (\v => xs) ->

184− Eff m t [l ::: x] (\v => map (l :::) (xs' v))

185−

186−(>>=) : Eff m a xs xs' ->

187− ((val : a) -> Eff m b (xs' val) xs'') -> Eff m b xs xs''

188−(>>=) = ebind

189−

190−return : a -> Eff m a xs (\v => xs)

191−return x = value x

192−

193−-- for idiom brackets

194−

195−infixl 2 <$>

196−

197−pure : a -> Eff m a xs (\v => xs)

198−pure = value

199−

200−(<$>) : Eff m (a -> b) xs (\v => xs) ->

201− Eff m a xs (\v => xs) -> Eff m b xs (\v => xs)

202−(<$>) prog v = do fn <- prog

203− arg <- v

204− return (fn arg)

205−

206−-- an interpreter

207−

208−private

209−execEff : Env m xs -> (p : EffElem e res xs) ->

210− (eff : e a res resk) ->

211− ((v : a) -> Env m (updateResTy v xs p eff) -> m t) -> m t

212−execEff (val :: env) Here eff' k

213− = handle val eff' (\v, res => k v (res :: env))

214−-- FIXME: Teach the elaborator to propagate parameters here

215−execEff {e} {a} {res} {resk} (val :: env) (There p) eff k

216− = execEff {e} {a} {res} {resk} env p eff (\v, env' => k v (val :: env'))

217−

218−-- Q: Instead of m b, implement as StateT (Env m xs') m b, so that state

219−-- updates can be propagated even through failing computations?

220−

221−eff : Env m xs -> Eff m a xs xs' -> ((x : a) -> Env m (xs' x) -> m b) -> m b

222−eff env (value x) k = k x env

223−eff env (prog `ebind` c) k

224− = eff env prog (\p', env' => eff env' (c p') k)

225−eff env (effect prf effP) k = execEff env prf effP k

226−eff env (lift prf effP) k

227− = let env' = dropEnv env prf in

228− eff env' effP (\p', envk => k p' (rebuildEnv envk prf env))

229−eff env (newInit r prog) k

230− = eff (r :: env) prog (\p' => \ (v :: envk) => k p' envk)

231−eff env (catch prog handler) k

232− = catch (eff env prog k)

233− (\e => eff env (handler e) k)

234−-- FIXME:

235−-- xs is needed explicitly because otherwise the pattern binding for

236−-- 'l' appears too late. Solution seems to be to reorder patterns at the

237−-- end so that everything is in scope when it needs to be.

238−eff {xs = [l ::: x]} env (l :- prog) k

239− = let env' = unlabel env in

240− eff env' prog (\p', envk => k p' (relabel l envk))

241−

242−-- yuck :) Haven't got type class instances working nicely in tactic

243−-- proofs yet, so just brute force it.

244−syntax MkDefaultEnv = with Env

245− (| [], [default], [default, default],

246− [default, default, default],

247− [default, default, default, default],

248− [default, default, default, default, default],

249− [default, default, default, default, default, default],

250− [default, default, default, default, default, default, default],

251− [default, default, default, default, default, default, default, default] |)

252−

253−implicit

254−lift' : Eff m t ys ys' ->

255− {default tactics { byReflection reflectEff; }

256− prf : SubList ys xs} ->

257− Eff m t xs (\v => updateWith (ys' v) xs prf)

258−lift' e {prf} = lift prf e

259−

260−implicit

261−effect' : {a, b: _} -> {e : Effect} ->

262− (eff : e t a b) ->

263− {default tactics { byReflection reflectEff; }

264− prf : EffElem e a xs} ->

265− Eff m t xs (\v => updateResTy v xs prf eff)

266−effect' e {prf} = effect prf e

267−

268−new : Handler e m =>

269− {default default r : res} ->

270− Eff m a (MkEff res e :: xs) (\v => (MkEff res' e :: xs')) ->

271− Eff m a xs (\v => xs')

272−new {r} e = newInit r e

273−

274−run : Applicative m => {default MkDefaultEnv env : Env m xs} -> Eff m a xs xs' -> m a

275−run {env} prog = eff env prog (\r, env => pure r)

276−

277−runPure : {default MkDefaultEnv env : Env id xs} -> Eff id a xs xs' -> a

278−runPure {env} prog = eff env prog (\r, env => r)

279−

280−runInit : Applicative m => Env m xs -> Eff m a xs xs' -> m a

281−runInit env prog = eff env prog (\r, env => pure r)

282−

283−runPureInit : Env id xs -> Eff id a xs xs' -> a

284−runPureInit env prog = eff env prog (\r, env => r)

285−

286−runWith : (a -> m a) -> Env m xs -> Eff m a xs xs' -> m a

287−runWith inj env prog = eff env prog (\r, env => inj r)

288−

289−runEnv : Applicative m => Env m xs -> Eff m a xs xs' ->

290− m (x : a ** Env m (xs' x))

291−runEnv env prog = eff env prog (\r, env => pure (r ** env))

292−

293−-- some higher order things

294−

295−mapE : Applicative m => (a -> {xs} Eff m b) -> List a -> {xs} Eff m (List b)

296−mapE f [] = pure []

297−mapE f (x :: xs) = [| f x :: mapE f xs |]

298−

299−

300−mapVE : Applicative m =>

301− (a -> {xs} Eff m b) ->

302− Vect n a ->

303− {xs} Eff m (Vect n b)

304−mapVE f [] = pure []

305−mapVE f (x :: xs) = [| f x :: mapVE f xs |]

306−

307−

308−when : Applicative m => Bool -> ({xs} Eff m ()) -> {xs} Eff m ()

309−when True e = e

310−when False e = pure ()

311−

libs/neweffects/Effect/Exception.idr → libs/oldeffects/Effect/Exception.idrrenamed+4−6

@@ -4,15 +4,12 @@ import Effects

4import System

5import Control.IOExcept

6

7−data Exception : Type -> Effect where

7+data Exception : Type -> Type -> Type -> Type -> Type where

8− Raise : a -> { () } Exception a b

8+ Raise : a -> Exception a () () b

9

10instance Handler (Exception a) Maybe where

11 handle _ (Raise e) k = Nothing

12

13−instance Handler (Exception a) List where

14− handle _ (Raise e) k = []

15−

16instance Show a => Handler (Exception a) IO where

13instance Show a => Handler (Exception a) IO where

17 handle _ (Raise e) k = do print e

14 handle _ (Raise e) k = do print e

18 believe_me (exit 1)

15 believe_me (exit 1)

@@ -26,7 +23,7 @@ instance Handler (Exception a) (Either a) where

26EXCEPTION : Type -> EFFECT

23EXCEPTION : Type -> EFFECT

27EXCEPTION t = MkEff () (Exception t)

24EXCEPTION t = MkEff () (Exception t)

28

25

29−raise : a -> { [EXCEPTION a ] } Eff m b

26+raise : a -> Eff m [EXCEPTION a] b

30raise err = Raise err

27raise err = Raise err

31

28

32

29

@@ -34,6 +31,7 @@ raise err = Raise err

34

31

35

32

36

33

34+

37-- TODO: Catching exceptions mid program?

35-- TODO: Catching exceptions mid program?

38-- probably need to invoke a new interpreter

36-- probably need to invoke a new interpreter

39

37

libs/oldeffects/Effect/File.idrnew file+69

@@ -0,0 +1,69 @@

1+module Effect.File

2+

3+import Effects

4+import Control.IOExcept

5+

6+data OpenFile : Mode -> Type where

7+ FH : File -> OpenFile m

8+

9+data FileIO : Effect where

10+ Open : String -> (m : Mode) -> FileIO () (Either () (OpenFile m)) Bool

11+ Close : FileIO (OpenFile m) () ()

12+

13+ ReadLine : FileIO (OpenFile Read) (OpenFile Read) String

14+ WriteLine : String -> FileIO (OpenFile Write) (OpenFile Write) ()

15+ EOF : FileIO (OpenFile Read) (OpenFile Read) Bool

16+

17+

18+instance Handler FileIO IO where

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

20+ valid <- validFile h

21+ if valid then k (Right (FH h)) True

22+ else k (Left ()) False

23+ handle (FH h) Close k = do closeFile h

24+ k () ()

25+ handle (FH h) ReadLine k = do str <- fread h

26+ k (FH h) str

27+ handle (FH h) (WriteLine str) k = do fwrite h str

28+ k (FH h) ()

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

30+ k (FH h) e

31+

32+instance Handler FileIO (IOExcept String) where

33+ handle () (Open fname m) k

34+ = do h <- ioe_lift (openFile fname m)

35+ valid <- ioe_lift (validFile h)

36+ if valid then k (Right (FH h)) True

37+ else k (Left ()) False

38+ handle (FH h) Close k = do ioe_lift (closeFile h); k () ()

39+ handle (FH h) ReadLine k = do str <- ioe_lift (fread h)

40+ k (FH h) str

41+ handle (FH h) (WriteLine str) k = do ioe_lift (fwrite h str)

42+ k (FH h) ()

43+ handle (FH h) EOF k = do e <- ioe_lift (feof h)

44+ k (FH h) e

45+

46+FILE_IO : Type -> EFFECT

47+FILE_IO t = MkEff t FileIO

48+

49+open : Handler FileIO e =>

50+ String -> (m : Mode) -> EffM e [FILE_IO ()]

51+ [FILE_IO (Either () (OpenFile m))] Bool

52+open f m = Open f m

53+

54+close : Handler FileIO e =>

55+ EffM e [FILE_IO (OpenFile m)] [FILE_IO ()] ()

56+close = Close

57+

58+readLine : Handler FileIO e => Eff e [FILE_IO (OpenFile Read)] String

59+readLine = ReadLine

60+

61+writeLine : Handler FileIO e => String -> Eff e [FILE_IO (OpenFile Write)] ()

62+writeLine str = WriteLine str

63+

64+eof : Handler FileIO e => Eff e [FILE_IO (OpenFile Read)] Bool

65+eof = EOF

66+

67+

68+

69+

libs/neweffects/Effect/Memory.idr → libs/oldeffects/Effect/Memory.idrrenamed+25−31

@@ -12,30 +12,29 @@ data MemoryChunk : Nat -> Nat -> Type where

12abstract

13data RawMemory : Effect where

14 Allocate : (n : Nat) ->

15− RawMemory () () (\v => MemoryChunk n 0)

15+ RawMemory () (MemoryChunk n 0) ()

16− Free : RawMemory () (MemoryChunk n i) (\v => ())

16+ Free : RawMemory (MemoryChunk n i) () ()

17 Initialize : Bits8 ->

18 (size : Nat) ->

19 so (i + size <= n) ->

20− RawMemory () (MemoryChunk n i) (\v => MemoryChunk n (i + size))

20+ RawMemory (MemoryChunk n i) (MemoryChunk n (i + size)) ()

21 Peek : (offset : Nat) ->

22 (size : Nat) ->

23 so (offset + size <= i) ->

24− RawMemory (Vect size Bits8)

24+ RawMemory (MemoryChunk n i) (MemoryChunk n i) (Vect size Bits8)

25− (MemoryChunk n i) (\v => MemoryChunk n i)

26 Poke : (offset : Nat) ->

25 Poke : (offset : Nat) ->

27 (Vect size Bits8) ->

26 (Vect size Bits8) ->

28 so (offset <= i && offset + size <= n) ->

27 so (offset <= i && offset + size <= n) ->

29− RawMemory () (MemoryChunk n i) (\v => MemoryChunk n (max i (offset + size)))

28+ RawMemory (MemoryChunk n i) (MemoryChunk n (max i (offset + size))) ()

30 Move : (src : MemoryChunk src_size src_init) ->

29 Move : (src : MemoryChunk src_size src_init) ->

31 (dst_offset : Nat) ->

30 (dst_offset : Nat) ->

32 (src_offset : Nat) ->

31 (src_offset : Nat) ->

33 (size : Nat) ->

32 (size : Nat) ->

34 so (dst_offset <= dst_init && dst_offset + size <= dst_size) ->

33 so (dst_offset <= dst_init && dst_offset + size <= dst_size) ->

35 so (src_offset + size <= src_init) ->

34 so (src_offset + size <= src_init) ->

36− RawMemory () (MemoryChunk dst_size dst_init)

35+ RawMemory (MemoryChunk dst_size dst_init)

37− (\v => MemoryChunk dst_size (max dst_init (dst_offset + size)))

36+ (MemoryChunk dst_size (max dst_init (dst_offset + size))) ()

38− GetRawPtr : RawMemory (MemoryChunk n i) (MemoryChunk n i) (\v => MemoryChunk n i)

37+ GetRawPtr : RawMemory (MemoryChunk n i) (MemoryChunk n i) (MemoryChunk n i)

39

38

40private

39private

41do_malloc : Nat -> IOExcept String Ptr

40do_malloc : Nat -> IOExcept String Ptr

@@ -80,28 +79,27 @@ do_poke ptr offset (b::bs)

80instance Handler RawMemory (IOExcept String) where

79instance Handler RawMemory (IOExcept String) where

81 handle () (Allocate n) k

80 handle () (Allocate n) k

82 = do ptr <- do_malloc n

81 = do ptr <- do_malloc n

83− k () (CH ptr)

82+ k (CH ptr) ()

84− handle {-{res = MemoryChunk _ offset}-} (CH ptr) (Initialize {i} c size _) k

83+ handle (CH ptr) (Initialize {i} c size _) k

85− = ioe_lift (do_memset ptr i c size) $> k () (CH ptr)

84+ = ioe_lift (do_memset ptr i c size) $> k (CH ptr) ()

86 handle (CH ptr) (Free) k

85 handle (CH ptr) (Free) k

87 = ioe_lift (do_free ptr) $> k () ()

86 = ioe_lift (do_free ptr) $> k () ()

88 handle (CH ptr) (Peek offset size _) k

87 handle (CH ptr) (Peek offset size _) k

89 = do res <- ioe_lift (do_peek ptr offset size)

88 = do res <- ioe_lift (do_peek ptr offset size)

90− k res (CH ptr)

89+ k (CH ptr) res

91 handle (CH ptr) (Poke offset content _) k

90 handle (CH ptr) (Poke offset content _) k

92 = do ioe_lift (do_poke ptr offset content)

91 = do ioe_lift (do_poke ptr offset content)

93− k () (CH ptr)

92+ k (CH ptr) ()

94 handle (CH dest_ptr) (Move (CH src_ptr) dest_offset src_offset size _ _) k

93 handle (CH dest_ptr) (Move (CH src_ptr) dest_offset src_offset size _ _) k

95 = do ioe_lift (do_memmove dest_ptr src_ptr dest_offset src_offset size)

94 = do ioe_lift (do_memmove dest_ptr src_ptr dest_offset src_offset size)

96− k () (CH dest_ptr)

95+ k (CH dest_ptr) ()

97 handle chunk (GetRawPtr) k

96 handle chunk (GetRawPtr) k

98 = k chunk chunk

97 = k chunk chunk

99

98

100RAW_MEMORY : Type -> EFFECT

99RAW_MEMORY : Type -> EFFECT

101RAW_MEMORY t = MkEff t RawMemory

100RAW_MEMORY t = MkEff t RawMemory

102

101

103−allocate : (n : Nat) ->

104− Eff m () [RAW_MEMORY ()] (\v => [RAW_MEMORY (MemoryChunk n 0)])

102+allocate : (n : Nat) -> EffM m [RAW_MEMORY ()] [RAW_MEMORY (MemoryChunk n 0)] ()

105allocate size = Allocate size

103allocate size = Allocate size

106

104

107initialize : {i : Nat} ->

105initialize : {i : Nat} ->

@@ -109,18 +107,17 @@ initialize : {i : Nat} ->

109 Bits8 ->

107 Bits8 ->

110 (size : Nat) ->

108 (size : Nat) ->

111 so (i + size <= n) ->

109 so (i + size <= n) ->

112− Eff m () [RAW_MEMORY (MemoryChunk n i)]

113− (\v => [RAW_MEMORY (MemoryChunk n (i + size))])

110+ EffM m [RAW_MEMORY (MemoryChunk n i)] [RAW_MEMORY (MemoryChunk n (i + size))] ()

114initialize c size prf = Initialize c size prf

111initialize c size prf = Initialize c size prf

115

112

116−free : Eff m () [RAW_MEMORY (MemoryChunk n i)] (\v => [RAW_MEMORY ()])

113+free : EffM m [RAW_MEMORY (MemoryChunk n i)] [RAW_MEMORY ()] ()

117free = Free

114free = Free

118

115

119peek : {i : Nat} ->

116peek : {i : Nat} ->

120 (offset : Nat) ->

117 (offset : Nat) ->

121 (size : Nat) ->

118 (size : Nat) ->

122 so (offset + size <= i) ->

119 so (offset + size <= i) ->

123− { [RAW_MEMORY (MemoryChunk n i)] } Eff m (Vect size Bits8)

120+ Eff m [RAW_MEMORY (MemoryChunk n i)] (Vect size Bits8)

124peek offset size prf = Peek offset size prf

121peek offset size prf = Peek offset size prf

125

122

126poke : {n : Nat} ->

123poke : {n : Nat} ->

@@ -128,12 +125,11 @@ poke : {n : Nat} ->

128 (offset : Nat) ->

125 (offset : Nat) ->

129 Vect size Bits8 ->

126 Vect size Bits8 ->

130 so (offset <= i && offset + size <= n) ->

127 so (offset <= i && offset + size <= n) ->

131− Eff m () [RAW_MEMORY (MemoryChunk n i)]

132− (\v => [RAW_MEMORY (MemoryChunk n (max i (offset + size)))])

128+ EffM m [RAW_MEMORY (MemoryChunk n i)] [RAW_MEMORY (MemoryChunk n (max i (offset + size)))] ()

133poke offset content prf = Poke offset content prf

129poke offset content prf = Poke offset content prf

134

130

135private

131private

136−getRawPtr : { [RAW_MEMORY (MemoryChunk n i)] } Eff m (MemoryChunk n i)

132+getRawPtr : Eff m [RAW_MEMORY (MemoryChunk n i)] (MemoryChunk n i)

137getRawPtr = GetRawPtr

133getRawPtr = GetRawPtr

138

134

139private

135private

@@ -146,8 +142,8 @@ move' : {dst_size : Nat} ->

146 (size : Nat) ->

142 (size : Nat) ->

147 so (dst_offset <= dst_init && dst_offset + size <= dst_size) ->

143 so (dst_offset <= dst_init && dst_offset + size <= dst_size) ->

148 so (src_offset + size <= src_init) ->

144 so (src_offset + size <= src_init) ->

149− Eff m () [RAW_MEMORY (MemoryChunk dst_size dst_init)]

145+ EffM m [RAW_MEMORY (MemoryChunk dst_size dst_init)]

150− (\v => [RAW_MEMORY (MemoryChunk dst_size (max dst_init (dst_offset + size)))])

146+ [RAW_MEMORY (MemoryChunk dst_size (max dst_init (dst_offset + size)))] ()

151move' src_ptr dst_offset src_offset size dst_bounds src_bounds

147move' src_ptr dst_offset src_offset size dst_bounds src_bounds

152 = Move src_ptr dst_offset src_offset size dst_bounds src_bounds

148 = Move src_ptr dst_offset src_offset size dst_bounds src_bounds

153

149

@@ -162,12 +158,10 @@ move : {dst_size : Nat} ->

162 (size : Nat) ->

158 (size : Nat) ->

163 so (dst_offset <= dst_init && dst_offset + size <= dst_size) ->

159 so (dst_offset <= dst_init && dst_offset + size <= dst_size) ->

164 so (src_offset + size <= src_init) ->

160 so (src_offset + size <= src_init) ->

165− Eff m ()

166− [ Dst ::: RAW_MEMORY (MemoryChunk dst_size dst_init)

161+ EffM m [ Dst ::: RAW_MEMORY (MemoryChunk dst_size dst_init)

167 , Src ::: RAW_MEMORY (MemoryChunk src_size src_init)]

162 , Src ::: RAW_MEMORY (MemoryChunk src_size src_init)]

168− (\v =>

169− [ Dst ::: RAW_MEMORY (MemoryChunk dst_size (max dst_init (dst_offset + size)))

163+ [ Dst ::: RAW_MEMORY (MemoryChunk dst_size (max dst_init (dst_offset + size)))

170− , Src ::: RAW_MEMORY (MemoryChunk src_size src_init)])

164+ , Src ::: RAW_MEMORY (MemoryChunk src_size src_init)] ()

171move dst_offset src_offset size dst_bounds src_bounds

165move dst_offset src_offset size dst_bounds src_bounds

172 = do src_ptr <- Src :- getRawPtr

166 = do src_ptr <- Src :- getRawPtr

173 Dst :- move' src_ptr dst_offset src_offset size dst_bounds src_bounds

167 Dst :- move' src_ptr dst_offset src_offset size dst_bounds src_bounds

libs/neweffects/Effect/Monad.idr → libs/oldeffects/Effect/Monad.idrrenamed+4−4

@@ -5,17 +5,17 @@ import Effects

5-- Eff is a monad too, so we can happily use it in a monad transformer.

6

7using (xs : List EFFECT, m : Type -> Type)

8− instance Functor (\a => EffM m a xs (\v => xs)) where

8+ instance Functor (EffM m xs xs) where

9 map f prog = do t <- prog

10 value (f t)

11

12− instance Applicative (\a => EffM m a xs (\v => xs)) where

12+ instance Applicative (EffM m xs xs) where

13 pure = value

14 (<$>) f a = do f' <- f

15 a' <- a

16 value (f' a')

17

18− instance Monad (\a => Eff m a xs (\v => xs)) where

18+ instance Monad (EffM m xs xs) where

19− (>>=) = Effects.(>>=)

19+ (>>=) = ebind

20

21

libs/oldeffects/Effect/Random.idrnew file+25

@@ -0,0 +1,25 @@

1+module Effect.Random

2+

3+import Effects

4+

5+data Random : Type -> Type -> Type -> Type where

6+ getRandom : Random Integer Integer Integer

7+ setSeed : Integer -> Random Integer Integer ()

8+

9+using (m : Type -> Type)

10+ instance Handler Random m where

11+ handle seed getRandom k

12+ = let seed' = (1664525 * seed + 1013904223) `prim__sremBigInt` (pow 2 32) in

13+ k seed' seed'

14+ handle seed (setSeed n) k = k n ()

15+

16+RND : EFFECT

17+RND = MkEff Integer Random

18+

19+rndInt : Integer -> Integer -> Eff m [RND] Integer

20+rndInt lower upper = do v <- getRandom

21+ return (v `prim__sremBigInt` (upper - lower) + lower)

22+

23+srand : Integer -> Eff m [RND] ()

24+srand n = setSeed n

25+

libs/neweffects/Effect/Select.idr → libs/oldeffects/Effect/Select.idrrenamed+4−4

@@ -3,21 +3,21 @@ module Effect.Select

3import Effects

4

5data Selection : Effect where

6− Select : List a -> { () } Selection a

6+ Select : List a -> Selection () () a

7

8instance Handler Selection Maybe where

9 handle _ (Select xs) k = tryAll xs where

10 tryAll [] = Nothing

11− tryAll (x :: xs) = case k x () of

11+ tryAll (x :: xs) = case k () x of

12 Nothing => tryAll xs

13 Just v => Just v

14

15instance Handler Selection List where

16− handle r (Select xs) k = concatMap (\x => k x r) xs

16+ handle r (Select xs) k = concatMap (k r) xs

17

18SELECT : EFFECT

19SELECT = MkEff () Selection

20

21−select : List a -> { [SELECT] } Eff m a

21+select : List a -> Eff m [SELECT] a

22select xs = Select xs

23

libs/neweffects/Effect/State.idr → libs/oldeffects/Effect/State.idrrenamed+9−9

@@ -5,33 +5,33 @@ import Effects

5%access public

6

7data State : Effect where

8− Get : { a } State a

8+ Get : State a a a

9− Put : b -> { a ==> b } State ()

9+ Put : b -> State a b ()

10

11using (m : Type -> Type)

12 instance Handler State m where

13 handle st Get k = k st st

14− handle st (Put n) k = k () n

14+ handle st (Put n) k = k n ()

15

16STATE : Type -> EFFECT

17STATE t = MkEff t State

18

19−get : { [STATE x] } Eff m x

19+get : Eff m [STATE x] x

20get = Get

21

22−put : x -> { [STATE x] } Eff m ()

22+put : x -> Eff m [STATE x] ()

23put val = Put val

24

25−putM : y -> { [STATE x] ==> [STATE y] } Eff m ()

25+putM : y -> EffM m [STATE x] [STATE y] ()

26putM val = Put val

27

28−update : (x -> x) -> { [STATE x] } Eff m ()

28+update : (x -> x) -> Eff m [STATE x] ()

29update f = put (f !get)

30

31−updateM : (x -> y) -> { [STATE x] ==> [STATE y] } Eff m ()

31+updateM : (x -> y) -> EffM m [STATE x] [STATE y] ()

32updateM f = putM (f !get)

33

34−locally : x -> ({ [STATE x] } Eff m t) -> { [STATE y] } Eff m t

34+locally : x -> Eff m [STATE x] t -> Eff m [STATE y] t

35locally newst prog = do st <- get

36 putM newst

37 val <- prog

libs/oldeffects/Effect/StdIO.idrnew file+60

@@ -0,0 +1,60 @@

1+module Effect.StdIO

2+

3+import Effects

4+import Control.IOExcept

5+

6+data StdIO : Effect where

7+ PutStr : String -> StdIO () () ()

8+ GetStr : StdIO () () String

9+

10+instance Handler StdIO IO where

11+ handle () (PutStr s) k = do putStr s; k () ()

12+ handle () GetStr k = do x <- getLine; k () x

13+

14+instance Handler StdIO (IOExcept a) where

15+ handle () (PutStr s) k = do ioe_lift (putStr s); k () ()

16+ handle () GetStr k = do x <- ioe_lift getLine; k () x

17+

18+-- Handle effects in a pure way, for simulating IO for unit testing/proof

19+

20+data IOStream a = MkStream (List String -> (a, List String))

21+

22+instance Handler StdIO IOStream where

23+ handle () (PutStr s) k

24+ = MkStream (\x => case k () () of

25+ MkStream f => let (res, str) = f x in

26+ (res, s :: str))

27+ handle {a} () GetStr k

28+ = MkStream (\x => case x of

29+ [] => cont "" []

30+ (t :: ts) => cont t ts)

31+ where

32+ cont : String -> List String -> (a, List String)

33+ cont t ts = case k () t of

34+ MkStream f => f ts

35+

36+--- The Effect and associated functions

37+

38+STDIO : EFFECT

39+STDIO = MkEff () StdIO

40+

41+putStr : Handler StdIO e => String -> Eff e [STDIO] ()

42+putStr s = PutStr s

43+

44+putStrLn : Handler StdIO e => String -> Eff e [STDIO] ()

45+putStrLn s = putStr (s ++ "\n")

46+

47+getStr : Handler StdIO e => Eff e [STDIO] String

48+getStr = GetStr

49+

50+mkStrFn : Env IOStream xs ->

51+ Eff IOStream xs a ->

52+ List String -> (a, List String)

53+mkStrFn {a} env p input = case mkStrFn' of

54+ MkStream f => f input

55+ where injStream : a -> IOStream a

56+ injStream v = MkStream (\x => (v, []))

57+ mkStrFn' : IOStream a

58+ mkStrFn' = runWith injStream env p

59+

60+

libs/oldeffects/Effects.idrnew file+308

@@ -0,0 +1,308 @@

1+module Effects

2+

3+import Language.Reflection

4+import Control.Catchable

5+

6+%access public

7+

8+---- Effects

9+

10+Effect : Type

11+Effect = Type -> Type -> Type -> Type

12+

13+%error_reverse

14+data EFFECT : Type where

15+ MkEff : Type -> Effect -> EFFECT

16+

17+class Handler (e : Effect) (m : Type -> Type) where

18+ handle : res -> (eff : e res res' t) -> (res' -> t -> m a) -> m a

19+

20+---- Properties and proof construction

21+

22+using (xs : List a, ys : List a)

23+ data SubList : List a -> List a -> Type where

24+ SubNil : SubList {a} [] []

25+ Keep : SubList xs ys -> SubList (x :: xs) (x :: ys)

26+ Drop : SubList xs ys -> SubList xs (x :: ys)

27+

28+ subListId : SubList xs xs

29+ subListId {xs = Nil} = SubNil

30+ subListId {xs = x :: xs} = Keep subListId

31+

32+data Env : (m : Type -> Type) -> List EFFECT -> Type where

33+ Nil : Env m Nil

34+ (::) : Handler eff m => a -> Env m xs -> Env m (MkEff a eff :: xs)

35+

36+data EffElem : (Type -> Type -> Type -> Type) -> Type ->

37+ List EFFECT -> Type where

38+ Here : EffElem x a (MkEff a x :: xs)

39+ There : EffElem x a xs -> EffElem x a (y :: xs)

40+

41+-- make an environment corresponding to a sub-list

42+dropEnv : Env m ys -> SubList xs ys -> Env m xs

43+dropEnv [] SubNil = []

44+dropEnv (v :: vs) (Keep rest) = v :: dropEnv vs rest

45+dropEnv (v :: vs) (Drop rest) = dropEnv vs rest

46+

47+updateWith : (ys' : List a) -> (xs : List a) ->

48+ SubList ys xs -> List a

49+updateWith (y :: ys) (x :: xs) (Keep rest) = y :: updateWith ys xs rest

50+updateWith ys (x :: xs) (Drop rest) = x :: updateWith ys xs rest

51+updateWith [] [] SubNil = []

52+updateWith (y :: ys) [] SubNil = y :: ys

53+updateWith [] (x :: xs) (Keep rest) = []

54+

55+-- put things back, replacing old with new in the sub-environment

56+rebuildEnv : Env m ys' -> (prf : SubList ys xs) ->

57+ Env m xs -> Env m (updateWith ys' xs prf)

58+rebuildEnv [] SubNil env = env

59+rebuildEnv (x :: xs) (Keep rest) (y :: env) = x :: rebuildEnv xs rest env

60+rebuildEnv xs (Drop rest) (y :: env) = y :: rebuildEnv xs rest env

61+rebuildEnv (x :: xs) SubNil [] = x :: xs

62+

63+---- The Effect EDSL itself ----

64+

65+-- some proof automation

66+

67+%reflection

68+reflectListEffElem : List a -> Tactic

69+reflectListEffElem [] = Refine "Here" `Seq` Solve

70+reflectListEffElem (x :: xs)

71+ = Try (Refine "Here" `Seq` Solve)

72+ (Refine "There" `Seq` (Solve `Seq` reflectListEffElem xs))

73+-- TMP HACK! FIXME!

74+-- The evaluator needs a 'function case' to know its a reflection function

75+-- until we propagate that information! Without this, the _ case won't get

76+-- matched.

77+reflectListEffElem (x ++ y) = Refine "Here" `Seq` Solve

78+reflectListEffElem _ = Refine "Here" `Seq` Solve

79+

80+%reflection

81+reflectSubList : List a -> Tactic

82+reflectSubList [] = Refine "SubNil" `Seq` Solve

83+reflectSubList (x :: xs)

84+ = Try (Refine "subListId" `Seq` Solve)

85+ (Try (Refine "Keep" `Seq` (Solve `Seq` reflectSubList xs))

86+ (Refine "Drop" `Seq` (Solve `Seq` reflectSubList xs)))

87+reflectSubList (x ++ y) = Refine "subListId" `Seq` Solve

88+reflectSubList _ = Refine "subListId" `Seq` Solve

89+

90+%reflection

91+reflectEff : (P : Type) -> Tactic

92+reflectEff (EffElem m a xs)

93+ = reflectListEffElem xs `Seq` Solve

94+reflectEff (SubList xs ys)

95+ = reflectSubList ys `Seq` Solve

96+

97+updateResTy : (xs : List EFFECT) -> EffElem e a xs -> e a b t ->

98+ List EFFECT

99+updateResTy {b} (MkEff a e :: xs) Here n = (MkEff b e) :: xs

100+updateResTy (x :: xs) (There p) n = x :: updateResTy xs p n

101+

102+updateResTyImm : (xs : List EFFECT) -> EffElem e a xs -> Type ->

103+ List EFFECT

104+updateResTyImm (MkEff a e :: xs) Here b = (MkEff b e) :: xs

105+updateResTyImm (x :: xs) (There p) b = x :: updateResTyImm xs p b

106+

107+infix 5 :::, :-, :=

108+

109+data LRes : lbl -> Type -> Type where

110+ (:=) : (x : lbl) -> res -> LRes x res

111+

112+(:::) : lbl -> EFFECT -> EFFECT

113+(:::) {lbl} x (MkEff r eff) = MkEff (LRes x r) eff

114+

115+private

116+unlabel : {l : ty} -> Env m [l ::: x] -> Env m [x]

117+unlabel {m} {x = MkEff a eff} [l := v] = [v]

118+

119+private

120+relabel : (l : ty) -> Env m [x] -> Env m [l ::: x]

121+relabel {x = MkEff a eff} l [v] = [l := v]

122+

123+-- the language of Effects

124+

125+data EffM : (m : Type -> Type) ->

126+ List EFFECT -> List EFFECT -> Type -> Type where

127+ value : a -> EffM m xs xs a

128+ ebind : EffM m xs xs' a -> (a -> EffM m xs' xs'' b) -> EffM m xs xs'' b

129+ effect : (prf : EffElem e a xs) ->

130+ (eff : e a b t) ->

131+ EffM m xs (updateResTy xs prf eff) t

132+ lift : (prf : SubList ys xs) ->

133+ EffM m ys ys' t -> EffM m xs (updateWith ys' xs prf) t

134+ new : Handler e m =>

135+ res -> EffM m (MkEff res e :: xs) (MkEff res' e :: xs') a ->

136+ EffM m xs xs' a

137+ test : (prf : EffElem e (Either l r) xs) ->

138+ EffM m (updateResTyImm xs prf l) xs' t ->

139+ EffM m (updateResTyImm xs prf r) xs' t ->

140+ EffM m xs xs' t

141+ test_lbl : {x : lbl} ->

142+ (prf : EffElem e (LRes x (Either l r)) xs) ->

143+ EffM m (updateResTyImm xs prf (LRes x l)) xs' t ->

144+ EffM m (updateResTyImm xs prf (LRes x r)) xs' t ->

145+ EffM m xs xs' t

146+ catch : Catchable m err =>

147+ EffM m xs xs' a -> (err -> EffM m xs xs' a) ->

148+ EffM m xs xs' a

149+ (:-) : (l : ty) -> EffM m [x] [y] t -> EffM m [l ::: x] [l ::: y] t

150+

151+syntax [tag] ":!" [val] = !(tag :- val)

152+

153+-- Eff : List (EFFECT m) -> Type -> Type

154+

155+-- For making proofs implicitly for 'test' and 'test_lbl'

156+

157+syntax if_valid then [e] else [t] =

158+ test (tactics { byReflection reflectEff; }) t e

159+

160+syntax if_valid [lbl] then [e] else [t] =

161+ test_lbl {x=lbl} (tactics { byReflection reflectEff; }) t e

162+

163+syntax if_error then [t] else [e] =

164+ test (tactics { byReflection reflectEff; }) t e

165+

166+syntax if_error [lbl] then [t] else [e] =

167+ test_lbl {x=lbl} (tactics { byReflection reflectEff; }) t e

168+

169+-- These may read better in some contexts

170+

171+syntax if_right then [e] else [t] =

172+ test (tactics { byReflection reflectEff; }) t e

173+

174+syntax if_right [lbl] then [e] else [t] =

175+ test_lbl {x=lbl} (tactics { byReflection reflectEff; }) t e

176+

177+syntax if_left then [t] else [e] =

178+ test (tactics { byReflection reflectEff; }) t e

179+

180+syntax if_left [lbl] then [t] else [e] =

181+ test_lbl {x=lbl} (tactics { byReflection reflectEff; }) t e

182+

183+

184+-- for 'do' notation

185+

186+return : a -> EffM m xs xs a

187+return x = value x

188+

189+(>>=) : EffM m xs xs' a -> (a -> EffM m xs' xs'' b) -> EffM m xs xs'' b

190+(>>=) = ebind

191+

192+-- for idiom brackets

193+

194+infixl 2 <$>

195+

196+pure : a -> EffM m xs xs a

197+pure = value

198+

199+(<$>) : EffM m xs xs (a -> b) -> EffM m xs xs a -> EffM m xs xs b

200+(<$>) prog v = do fn <- prog

201+ arg <- v

202+ return (fn arg)

203+

204+-- an interpreter

205+

206+private

207+execEff : Env m xs -> (p : EffElem e res xs) ->

208+ (eff : e res b a) ->

209+ (Env m (updateResTy xs p eff) -> a -> m t) -> m t

210+execEff (val :: env) Here eff' k

211+ = handle val eff' (\res, v => k (res :: env) v)

212+execEff {e} {res} {b} {a} (val :: env) (There p) eff k

213+ = execEff {e} {res} {b} {a} env p eff (\env', v => k (val :: env') v)

214+

215+private

216+testEff : Env m xs -> (p : EffElem e (Either l r) xs) ->

217+ (Env m (updateResTyImm xs p l) -> m b) ->

218+ (Env m (updateResTyImm xs p r) -> m b) ->

219+ m b

220+testEff (Left err :: env) Here lk rk = lk (err :: env)

221+testEff (Right ok :: env) Here lk rk = rk (ok :: env)

222+testEff (val :: env) (There p) lk rk

223+ = testEff env p (\envk => lk (val :: envk))

224+ (\envk => rk (val :: envk))

225+

226+private

227+testEffLbl : {x : lblTy} ->

228+ Env m xs -> (p : EffElem e (LRes x (Either l r)) xs) ->

229+ (Env m (updateResTyImm xs p (LRes x l)) -> m b) ->

230+ (Env m (updateResTyImm xs p (LRes x r)) -> m b) ->

231+ m b

232+testEffLbl ((lbl := Left err) :: env) Here lk rk = lk ((lbl := err) :: env)

233+testEffLbl ((lbl := Right ok) :: env) Here lk rk = rk ((lbl := ok) :: env)

234+testEffLbl (val :: env) (There p) lk rk

235+ = testEffLbl env p (\envk => lk (val :: envk))

236+ (\envk => rk (val :: envk))

237+

238+-- Q: Instead of m b, implement as StateT (Env m xs') m b, so that state

239+-- updates can be propagated even through failing computations?

240+

241+eff : Env m xs -> EffM m xs xs' a -> (Env m xs' -> a -> m b) -> m b

242+eff env (value x) k = k env x

243+eff env (prog `ebind` c) k

244+ = eff env prog (\env', p' => eff env' (c p') k)

245+eff env (effect prf effP) k = execEff env prf effP k

246+eff env (lift prf effP) k

247+ = let env' = dropEnv env prf in

248+ eff env' effP (\envk, p' => k (rebuildEnv envk prf env) p')

249+eff env (new r prog) k

250+ = eff (r :: env) prog (\(v :: envk), p' => k envk p')

251+eff env (test prf l r) k

252+ = testEff env prf (\envk => eff envk l k) (\envk => eff envk r k)

253+eff env (test_lbl prf l r) k

254+ = testEffLbl env prf (\envk => eff envk l k) (\envk => eff envk r k)

255+eff env (catch prog handler) k

256+ = catch (eff env prog k)

257+ (\e => eff env (handler e) k)

258+-- FIXME:

259+-- xs is needed explicitly because otherwise the pattern binding for

260+-- 'l' appears too late. Solution seems to be to reorder patterns at the

261+-- end so that everything is in scope when it needs to be.

262+eff {xs = [l ::: x]} env (l :- prog) k

263+ = let env' = unlabel env in

264+ eff env' prog (\envk, p' => k (relabel l envk) p')

265+

266+implicit

267+lift' : EffM m ys ys' t ->

268+ {default tactics { byReflection reflectEff; }

269+ prf : SubList ys xs} ->

270+ EffM m xs (updateWith ys' xs prf) t

271+lift' e {prf} = lift prf e

272+

273+implicit

274+effect' : {a, b: _} -> {e : Effect} ->

275+ (eff : e a b t) ->

276+ {default tactics { byReflection reflectEff; }

277+ prf : EffElem e a xs} ->

278+ EffM m xs (updateResTy xs prf eff) t

279+effect' e {prf} = effect prf e

280+

281+

282+run : Applicative m => Env m xs -> EffM m xs xs' a -> m a

283+run env prog = eff env prog (\env, r => pure r)

284+

285+runEnv : Applicative m => Env m xs -> EffM m xs xs' a -> m (Env m xs', a)

286+runEnv env prog = eff env prog (\env, r => pure (env, r))

287+

288+runPure : Env id xs -> EffM id xs xs' a -> a

289+runPure env prog = eff env prog (\env, r => r)

290+

291+-- runPureEnv : Env id xs -> EffM id xs xs' a -> (Env id xs', a)

292+-- runPureEnv env prog = eff env prog (\env, r => (env, r))

293+

294+runWith : (a -> m a) -> Env m xs -> EffM m xs xs' a -> m a

295+runWith inj env prog = eff env prog (\env, r => inj r)

296+

297+Eff : (Type -> Type) -> List EFFECT -> Type -> Type

298+Eff m xs t = EffM m xs xs t

299+

300+-- some higher order things

301+

302+mapE : Applicative m => (a -> Eff m xs b) -> List a -> Eff m xs (List b)

303+mapE f [] = pure []

304+mapE f (x :: xs) = [| f x :: mapE f xs |]

305+

306+when : Applicative m => Bool -> Eff m xs () -> Eff m xs ()

307+when True e = e

308+when False e = pure ()

libs/neweffects/Makefile → libs/oldeffects/Makefilerenamed+3−3

@@ -1,13 +1,13 @@

1IDRIS := idris

2

3build:

4− $(IDRIS) --build neweffects.ipkg

4+ $(IDRIS) --build oldeffects.ipkg

5

6clean:

7− $(IDRIS) --clean neweffects.ipkg

7+ $(IDRIS) --clean oldeffects.ipkg

8

9install:

10− $(IDRIS) --install neweffects.ipkg

10+ $(IDRIS) --install oldeffects.ipkg

11

12rebuild: clean build

13

libs/neweffects/neweffects.ipkg → libs/oldeffects/oldeffects.ipkgrenamed+3−4

@@ -1,9 +1,8 @@

1−package neweffects

1+package oldeffects

2

3opts = "--nobasepkgs -i ../prelude -i ../base"

4−modules = Effects, Effect.Default,

4+modules = Effects,

5−

6 Effect.Exception, Effect.File, Effect.State,

5 Effect.Exception, Effect.File, Effect.State,

7 Effect.Random, Effect.StdIO, Effect.Select,

6 Effect.Random, Effect.StdIO, Effect.Select,

8− Effect.Memory, Effect.System

7+ Effect.Memory, Effect.Monad

9

8

src/Idris/AbsSyntax.hs+11−9

@@ -357,15 +357,15 @@ addNameIdx' i n

357getHdrs :: Codegen -> Idris [String]

358getHdrs tgt = do i <- getIState; return (forCodegen tgt $ idris_hdrs i)

359

360−setErrLine :: Int -> Idris ()

360+setErrSpan :: FC -> Idris ()

361−setErrLine x = do i <- getIState;

361+setErrSpan x = do i <- getIState;

362− case (errLine i) of

362+ case (errSpan i) of

363− Nothing -> putIState $ i { errLine = Just x }

363+ Nothing -> putIState $ i { errSpan = Just x }

364 Just _ -> return ()

365

366clearErr :: Idris ()

367clearErr = do i <- getIState

368− putIState $ i { errLine = Nothing }

368+ putIState $ i { errSpan = Nothing }

369

370getSO :: Idris (Maybe String)

371getSO = do i <- getIState

@@ -392,6 +392,8 @@ getName = do i <- getIState;

392 putIState $ (i { idris_name = idx + 1 })

393 return idx

394

395+-- InternalApp keeps track of the real function application for making case splits from, not the application the

396+-- programmer wrote, which doesn't have the whole context in any case other than top level definitions

395addInternalApp :: FilePath -> Int -> PTerm -> Idris ()

397addInternalApp :: FilePath -> Int -> PTerm -> Idris ()

396addInternalApp fp l t

398addInternalApp fp l t

397 = do i <- getIState

399 = do i <- getIState

@@ -650,7 +652,7 @@ ihWarn h fc err = do i <- getIState

650 do err' <- iRender . fmap (fancifyAnnots i) $ err

652 do err' <- iRender . fmap (fancifyAnnots i) $ err

651 let (str, spans) = displaySpans err'

653 let (str, spans) = displaySpans err'

652 runIO . hPutStrLn h $

654 runIO . hPutStrLn h $

653− convSExp "warning" (fc_fname fc, fc_line fc, fc_column fc, str, spans) n

655+ convSExp "warning" (fc_fname fc, fc_start fc, fc_end fc, str, spans) n

654

656

655setLogLevel :: Int -> Idris ()

657setLogLevel :: Int -> Idris ()

656setLogLevel l = do i <- getIState

658setLogLevel l = do i <- getIState

@@ -907,7 +909,7 @@ iLOG = logLvl 1

907

909

908noErrors :: Idris Bool

910noErrors :: Idris Bool

909noErrors = do i <- getIState

911noErrors = do i <- getIState

910− case errLine i of

912+ case errSpan i of

911 Nothing -> return True

913 Nothing -> return True

912 _ -> return False

914 _ -> return False

913

915

@@ -1069,14 +1071,14 @@ expandParamsD rhs ist dec ps ns (PData doc argDocs syn fc co pd)

1069 (map econ cons)

1071 (map econ cons)

1070 else PDatadecl n (expandParams dec ps ns [] ty) (map econ cons)

1072 else PDatadecl n (expandParams dec ps ns [] ty) (map econ cons)

1071 econ (doc, argDocs, n, t, fc, fs)

1073 econ (doc, argDocs, n, t, fc, fs)

1072− = (doc, argDocs, dec n, piBindp impl ps (expandParams dec ps ns [] t), fc, fs)

1074+ = (doc, argDocs, dec n, piBindp expl ps (expandParams dec ps ns [] t), fc, fs)

1073expandParamsD rhs ist dec ps ns (PRecord doc syn fc tn tty cdoc cn cty)

1075expandParamsD rhs ist dec ps ns (PRecord doc syn fc tn tty cdoc cn cty)

1074 = if tn `elem` ns

1076 = if tn `elem` ns

1075 then PRecord doc syn fc (dec tn) (piBind ps (expandParams dec ps ns [] tty))

1077 then PRecord doc syn fc (dec tn) (piBind ps (expandParams dec ps ns [] tty))

1076 cdoc (dec cn) conty

1078 cdoc (dec cn) conty

1077 else PRecord doc syn fc (dec tn) (expandParams dec ps ns [] tty)

1079 else PRecord doc syn fc (dec tn) (expandParams dec ps ns [] tty)

1078 cdoc (dec cn) conty

1080 cdoc (dec cn) conty

1079− where conty = piBindp impl ps (expandParams dec ps ns [] cty)

1081+ where conty = piBindp expl ps (expandParams dec ps ns [] cty)

1080expandParamsD rhs ist dec ps ns (PParams f params pds)

1082expandParamsD rhs ist dec ps ns (PParams f params pds)

1081 = PParams f (ps ++ map (mapsnd (expandParams dec ps ns [])) params)

1083 = PParams f (ps ++ map (mapsnd (expandParams dec ps ns [])) params)

1082 (map (expandParamsD True ist dec ps ns) pds)

1084 (map (expandParamsD True ist dec ps ns) pds)

src/Idris/AbsSyntaxTree.hs+3−2

@@ -135,11 +135,12 @@ data IState = IState {

135 idris_cgflags :: [(Codegen, String)],

136 idris_hdrs :: [(Codegen, String)],

137 proof_list :: [(Name, [String])],

138− errLine :: Maybe Int,

138+ errSpan :: Maybe FC,

139 parserWarnings :: [(FC, Err)],

140 lastParse :: Maybe Name,

141 indent_stack :: [Int],

142 brace_stack :: [Maybe Int],

143+ lastTokenSpan :: Maybe FC, -- ^ What was the span of the latest token parsed?

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

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

144 default_access :: Accessibility,

145 default_access :: Accessibility,

145 default_total :: Bool,

146 default_total :: Bool,

@@ -224,7 +225,7 @@ idrisInit = IState initContext [] [] emptyContext emptyContext emptyContext

224 emptyContext emptyContext emptyContext emptyContext

225 emptyContext emptyContext emptyContext emptyContext

225 emptyContext emptyContext

226 emptyContext emptyContext

226 [] [] defaultOpts 6 [] [] [] [] [] [] [] [] [] [] [] [] []

227 [] [] defaultOpts 6 [] [] [] [] [] [] [] [] [] [] [] [] []

227− [] Nothing [] Nothing [] [] [] Hidden False [] Nothing [] [] RawOutput

228+ [] Nothing [] Nothing [] [] Nothing [] Hidden False [] Nothing [] [] RawOutput

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

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

229 AutomaticWidth

230 AutomaticWidth

230

231

src/Idris/Core/Elaborate.hs+5−2

@@ -627,9 +627,12 @@ no_errors tac err

627 ps' <- get_probs

628 if (length ps' > length ps) then

629 case reverse ps' of

630− ((x,y,env,err,_) : _) ->

630+ ((x,y,env,inerr,_) : _) ->

631 let env' = map (\(x, b) -> (x, binderTy b)) env in

632+ lift $ tfail $

633+ case err of

632− lift $ tfail $ CantUnify False x y err env' 0

634+ Nothing -> CantUnify False x y inerr env' 0

635+ Just e -> e

633 else return $! ()

636 else return $! ()

634

637

635-- Try a tactic, if it fails, try another

638-- Try a tactic, if it fails, try another

src/Idris/Core/ProofState.hs+2−1

@@ -491,7 +491,8 @@ solve ctxt env (Bind x (Guess ty val) sc)

491 = do ps <- get

492 let (uh, uns) = unified ps

493 case lookup x (notunified ps) of

494+ Just tm -> -- trace ("NEED MATCH: " ++ show (tm, val)) $

494− Just tm -> match_unify' ctxt env tm val

495+ match_unify' ctxt env tm val

495 _ -> return []

496 _ -> return []

496 action (\ps -> ps { holes = holes ps \\ [x],

497 action (\ps -> ps { holes = holes ps \\ [x],

497 solved = Just (x, val),

498 solved = Just (x, val),

src/Idris/Core/TT.hs+9−6

@@ -44,8 +44,8 @@ data Option = TTypeInTType

44

45-- | Source location. These are typically produced by the parser 'Idris.Parser.getFC'

46data FC = FC { fc_fname :: String, -- ^ Filename

47− fc_line :: Int, -- ^ Line number

47+ fc_start :: (Int, Int), -- ^ Line and column numbers for the start of the location span

48− fc_column :: Int -- ^ Column number

48+ fc_end :: (Int, Int) -- ^ Line and column numbers for the end of the location span

49 }

50

51-- | Ignore source location equality (so deriving classes do not compare FCs)

@@ -57,7 +57,7 @@ newtype FC' = FC' { unwrapFC :: FC }

57

58instance Eq FC' where

59 FC' fc == FC' fc' = fcEq fc fc'

60− where fcEq (FC n l c) (FC n' l' c') = n == n' && l == l' && c == c'

60+ where fcEq (FC n s e) (FC n' s' e') = n == n' && s == s' && e == e'

61

62-- | Empty source location

63emptyFC :: FC

@@ -65,7 +65,7 @@ emptyFC = fileFC ""

65

66-- | Source location with file only

67fileFC :: String -> FC

68−fileFC s = FC s 0 0

68+fileFC s = FC s (0, 0) (0, 0)

69

70{-!

71deriving instance Binary FC

@@ -73,10 +73,13 @@ deriving instance NFData FC

73!-}

74

75instance Sized FC where

76− size (FC f l c) = 1 + length f

76+ size (FC f s e) = 4 + length f

77

78instance Show FC where

79− show (FC f l c) = f ++ ":" ++ show l ++ ":" ++ show c

79+ show (FC f s e) = f ++ ":" ++ showLC s e

80+ where showLC (sl, sc) (el, ec) | sl == el && sc == ec = show sl ++ ":" ++ show sc

81+ | sl == el = show sl ++ ":" ++ show sc ++ "-" ++ show ec

82+ | otherwise = show sl ++ ":" ++ show sc ++ "-" ++ show el ++ ":" ++ show ec

80

83

81-- | Output annotation for pretty-printed name - decides colour

84-- | Output annotation for pretty-printed name - decides colour

82data NameOutput = TypeOutput | FunOutput | DataOutput

85data NameOutput = TypeOutput | FunOutput | DataOutput

src/Idris/Core/Unify.hs+4−2

@@ -372,8 +372,8 @@ unify ctxt env topx topy inj holes =

372

373 unApp fn bnames appx@(App fx ax) appy@(App fy ay)

374 | (injectiveApp fx && injectiveApp fy)

375− || (injectiveApp fx && rigid appx && metavarApp appy)

375+ || (injectiveApp fx && rigid appx && metavarApp appy && numArgs appx == numArgs appy)

376− || (injectiveApp fy && rigid appy && metavarApp appx)

376+ || (injectiveApp fy && rigid appy && metavarApp appx && numArgs appx == numArgs appy)

377 || (injectiveApp fx && metavarApp fy && ax == ay)

378 || (injectiveApp fy && metavarApp fx && ax == ay)

379 = do let (headx, _) = unApply fx

@@ -418,6 +418,8 @@ unify ctxt env topx topy inj holes =

418 vs <- combine bnames as as'

419 unArgs vs xs ys

420

421+ numArgs tm = let (f, args) = unApply tm in length args

422+

421 metavarApp tm = let (f, args) = unApply tm in

423 metavarApp tm = let (f, args) = unApply tm in

422 (metavar f &&

424 (metavar f &&

423 all (\x -> metavarApp x) args

425 all (\x -> metavarApp x) args

src/Idris/ElabDecls.hs+4−4

@@ -108,8 +108,8 @@ elabType' norm info syn doc argDocs fc opts n ty' = {- let ty' = piBind (params

108 -- Add normalised type to internals

109 rep <- useREPL

110 when rep $ do

111− addInternalApp (fc_fname fc) (fc_line fc) (mergeTy ty' (delab i nty'))

111+ addInternalApp (fc_fname fc) (fst . fc_start $ fc) (mergeTy ty' (delab i nty')) -- TODO: Should use span instead of line and filename?

112− addIBC (IBCLineApp (fc_fname fc) (fc_line fc) (mergeTy ty' (delab i nty')))

112+ addIBC (IBCLineApp (fc_fname fc) (fst . fc_start $ fc) (mergeTy ty' (delab i nty')))

113

114 let (t, _) = unApply (getRetTy nty')

115 let corec = case t of

@@ -1408,8 +1408,8 @@ elabClause info opts (cnum, PClause fc fname lhs_in withs rhs_in whereblock)

1408

1409 rep <- useREPL

1410 when rep $ do

1411− addInternalApp (fc_fname fc) (fc_line fc) (delabMV i clhs)

1411+ addInternalApp (fc_fname fc) (fst . fc_start $ fc) (delabMV i clhs) -- TODO: Should use span instead of line and filename?

1412− addIBC (IBCLineApp (fc_fname fc) (fc_line fc) (delabMV i clhs))

1412+ addIBC (IBCLineApp (fc_fname fc) (fst . fc_start $ fc) (delabMV i clhs))

1413

1414 logLvl 5 ("Checked " ++ show clhs ++ "\n" ++ show clhsty)

1415 -- Elaborate where block

src/Idris/ElabTerm.hs+16−2

@@ -73,8 +73,11 @@ build ist info pattern opts fn tm

73 tm <- get_term

74 ctxt <- get_context

75 probs <- get_probs

76+ u <- getUnifyLog

76

77

78+ when (not pattern) $

79+ traceWhen u ("Remaining problems:\n" ++ show probs) $

77− when (not pattern) $ do matchProblems True; unifyProblems

80+ do matchProblems True; unifyProblems

78 probs <- get_probs

81 probs <- get_probs

79 case probs of

82 case probs of

80 [] -> return ()

83 [] -> return ()

@@ -459,6 +462,8 @@ elab ist info pattern opts fn tm

459-- trace ("ns is " ++ show ns) $ return ()

462-- trace ("ns is " ++ show ns) $ return ()

460 -- mark any type class arguments as injective

463 -- mark any type class arguments as injective

461 mapM_ checkIfInjective (map snd ns)

464 mapM_ checkIfInjective (map snd ns)

465+ unifyProblems -- try again with the new information,

466+ -- to help with disambiguation

462 -- Sort so that the implicit tactics and alternatives go last

467 -- Sort so that the implicit tactics and alternatives go last

463 let (ns', eargs) = unzip $

468 let (ns', eargs) = unzip $

464 sortBy cmpArg (zip ns args)

469 sortBy cmpArg (zip ns args)

@@ -481,12 +486,21 @@ elab ist info pattern opts fn tm

481 (movelast n)

486 (movelast n)

482 else movelast n)

487 else movelast n)

483 (ivs' \\ ivs)

488 (ivs' \\ ivs)

484− where -- normal < tactic < default tactic

489+ where -- normal < alternatives < lambdas < rewrites < tactic < default tactic

490+ -- reason for lambdas after alternatives is that having

491+ -- the alternative resolved can help with typechecking the lambda

492+ -- or the rewrite. Rewrites/tactics need as much information

493+ -- as possible about the type.

494+ -- FIXME: Better would be to allow alternative resolution to be

495+ -- retried after more information is in.

485 cmpArg (_, x) (_, y)

496 cmpArg (_, x) (_, y)

486 = compare (conDepth 0 (getTm x) + priority x + alt x)

497 = compare (conDepth 0 (getTm x) + priority x + alt x)

487 (conDepth 0 (getTm y) + priority y + alt y)

498 (conDepth 0 (getTm y) + priority y + alt y)

488 where alt t = case getTm t of

499 where alt t = case getTm t of

489 PAlternative False _ -> 5

500 PAlternative False _ -> 5

501+ PAlternative True _ -> 1

502+ PLam _ _ _ -> 2

503+ PRewrite _ _ _ _ -> 3

490 _ -> 0

504 _ -> 0

491

505

492 -- Score a point for every level where there is a non-constructor

506 -- Score a point for every level where there is a non-constructor

src/Idris/Error.hs+8−13

@@ -23,7 +23,7 @@ iucheck = do tit <- typeInType

23 when (not tit) $

24 do ist <- getIState

25 (tclift $ ucheck (idris_constraints ist)) `idrisCatch`

26− (\e -> do setErrLine (getErrLine e)

26+ (\e -> do setErrSpan (getErrSpan e)

27 iputStrLn (pshow ist e))

28

29showErr :: Err -> Idris String

@@ -43,9 +43,9 @@ setAndReport :: Err -> Idris ()

43setAndReport e = do ist <- getIState

44 let h = idris_outh ist

45 case e of

46− At fc@(FC f l c) e -> do setErrLine l

46+ At fc e -> do setErrSpan fc

47− ihWarn h fc $ pprintErr ist e

47+ ihWarn h fc $ pprintErr ist e

48− _ -> do setErrLine (getErrLine e)

48+ _ -> do setErrSpan (getErrSpan e)

49 ihputStrLn h $ pshow ist e

50

51ifail :: String -> Idris a

@@ -56,7 +56,7 @@ ierror = throwError

56

57tclift :: TC a -> Idris a

58tclift (OK v) = return v

59−tclift (Error err@(At (FC f l c) e)) = do setErrLine l ; throwError err

59+tclift (Error err@(At fc e)) = do setErrSpan fc; throwError err

60tclift (Error err) = throwError err

61

62tctry :: TC a -> TC a -> Idris a

@@ -65,11 +65,6 @@ tctry tc1 tc2

65 OK v -> return v

66 Error err -> tclift tc2

67

68−getErrLine :: Err -> Int

68+getErrSpan :: Err -> FC

69−getErrLine (At (FC _ l _) _) = l

69+getErrSpan (At fc _) = fc

70−getErrLine _ = 0

70+getErrSpan _ = emptyFC

71−

72−getErrColumn :: Err -> Int

73−getErrColumn (At (FC _ _ c) _) = c

74−getErrColumn _ = 0

75−

src/Idris/IBC.hs+5−3

@@ -28,7 +28,7 @@ import Codec.Compression.Zlib (compress)

28import Util.Zlib (decompressEither)

29

30ibcVersion :: Word8

31−ibcVersion = 63

31+ibcVersion = 64

32

33

34data IBCFile = IBCFile { ver :: Word8,

@@ -577,13 +577,15 @@ instance Binary CGInfo where

577 return (CGInfo x1 x2 [] x4 x5)

578

579instance Binary FC where

580− put (FC x1 x2 x3)

580+ put (FC x1 (x2, x3) (x4, x5))

581 = do put x1

582 put (x2 * 65536 + x3)

583+ put (x4 * 65536 + x5)

583 get

584 get

584 = do x1 <- get

585 = do x1 <- get

585 x2x3 <- get

586 x2x3 <- get

587+ x4x5 <- get

586− return (FC x1 (x2x3 `div` 65536) (x2x3 `mod` 65536))

588+ return (FC x1 (x2x3 `div` 65536, x2x3 `mod` 65536) (x4x5 `div` 65536, x4x5 `mod` 65536))

587

589

588

590

589instance Binary Name where

591instance Binary Name where

src/Idris/IdeSlave.hs+4−4

@@ -89,10 +89,10 @@ instance SExpable OutputAnnotation where

89 (SymbolAtom "implicit", BoolAtom imp)]

90 toSExp AnnConstData = toSExp [(SymbolAtom "decor", SymbolAtom "data")]

91 toSExp AnnConstType = toSExp [(SymbolAtom "decor", SymbolAtom "type")]

92− toSExp (AnnFC (FC f l c)) = toSExp [(SymbolAtom "source-loc",

92+ toSExp (AnnFC (FC f (sl, sc) (el, ec))) = toSExp [(SymbolAtom "source-loc",

93− ((SymbolAtom "filename", StringAtom f),

93+ ((SymbolAtom "filename", StringAtom f),

94− (SymbolAtom "line", IntegerAtom (toInteger l)),

94+ (SymbolAtom "start", IntegerAtom (toInteger sl), IntegerAtom (toInteger sc)),

95− (SymbolAtom "column", IntegerAtom (toInteger c))))]

95+ (SymbolAtom "end", IntegerAtom (toInteger el), IntegerAtom (toInteger ec))))]

96

97escape :: String -> String

98escape = concatMap escapeChar

src/Idris/ParseHelpers.hs+11−6

@@ -1,5 +1,4 @@

1−{-# LANGUAGE GeneralizedNewtypeDeriving, ConstraintKinds, PatternGuards #-}

1+{-# LANGUAGE GeneralizedNewtypeDeriving, ConstraintKinds, PatternGuards, OverlappingInstances, StandaloneDeriving #-}

2−{-# LANGUAGE StandaloneDeriving #-}

3module Idris.ParseHelpers where

2module Idris.ParseHelpers where

4

3

5import Prelude hiding (pi)

4import Prelude hiding (pi)

@@ -43,13 +42,19 @@ import Debug.Trace

43type IdrisParser = StateT IState IdrisInnerParser

42type IdrisParser = StateT IState IdrisInnerParser

44

43

45newtype IdrisInnerParser a = IdrisInnerParser { runInnerParser :: Parser a }

44newtype IdrisInnerParser a = IdrisInnerParser { runInnerParser :: Parser a }

46− deriving (Monad, Functor, MonadPlus, Applicative, Alternative, CharParsing, LookAheadParsing{-, Parsing-}, DeltaParsing, MarkParsing Delta, Monoid)

45+ deriving (Monad, Functor, MonadPlus, Applicative, Alternative, CharParsing, LookAheadParsing, DeltaParsing, MarkParsing Delta, Monoid, TokenParsing)

47

46

48deriving instance Parsing IdrisInnerParser

47deriving instance Parsing IdrisInnerParser

49

48

50−instance TokenParsing IdrisInnerParser where

49+instance TokenParsing IdrisParser where

51 someSpace = many (simpleWhiteSpace <|> singleLineComment <|> multiLineComment) *> pure ()

50 someSpace = many (simpleWhiteSpace <|> singleLineComment <|> multiLineComment) *> pure ()

52−

51+ token p = do s <- get

52+ (FC fn (sl, sc) _) <- getFC --TODO: Update after fixing getFC

53+ r <- p

54+ (FC fn _ (el, ec)) <- getFC

55+ whiteSpace

56+ put (s { lastTokenSpan = Just (FC fn (sl, sc) (el, ec)) })

57+ return r

53-- | Generalized monadic parsing constraint type

58-- | Generalized monadic parsing constraint type

54type MonadicParsing m = (DeltaParsing m, LookAheadParsing m, TokenParsing m, Monad m)

59type MonadicParsing m = (DeltaParsing m, LookAheadParsing m, TokenParsing m, Monad m)

55

60

@@ -333,7 +338,7 @@ getFC :: MonadicParsing m => m FC

333getFC = do s <- position

338getFC = do s <- position

334 let (dir, file) = splitFileName (fileName s)

339 let (dir, file) = splitFileName (fileName s)

335 let f = if dir == addTrailingPathSeparator "." then file else fileName s

340 let f = if dir == addTrailingPathSeparator "." then file else fileName s

336− return $ FC f (lineNum s) (columnNum s)

341+ return $ FC f (lineNum s, columnNum s) (lineNum s, columnNum s) -- TODO: Change to actual spanning

337

342

338{-* Syntax helpers-}

343{-* Syntax helpers-}

339-- | Bind constraints to term

344-- | Bind constraints to term

src/Idris/Parser.hs+3−3

@@ -1131,7 +1131,7 @@ parseProg syn fname input mrk

1131 case idris_outputmode i of

1132 RawOutput -> ihputStrLn (idris_outh i) (show doc)

1133 IdeSlave n -> ihWarn (idris_outh i) fc (P.text msg)

1134− putIState (i { errLine = Just (fc_line fc) }) -- Just errl })

1134+ putIState (i { errSpan = Just fc })

1135 return []

1136 Success (x, i) -> do putIState i

1137 reportParserWarnings

@@ -1149,7 +1149,7 @@ parseProg syn fname input mrk

1149loadModule :: Handle -> FilePath -> Idris String

1150loadModule outh f

1151 = idrisCatch (loadModule' outh f)

1152− (\e -> do setErrLine (getErrLine e)

1152+ (\e -> do setErrSpan (getErrSpan e)

1153 ist <- getIState

1154 msg <- showErr e

1155 ihputStrLn outh msg

@@ -1197,7 +1197,7 @@ loadFromIFile h (LIDR fn) = loadSource' h True fn

1197loadSource' :: Handle -> Bool -> FilePath -> Idris ()

1198loadSource' h lidr r

1199 = idrisCatch (loadSource h lidr r)

1200− (\e -> do setErrLine (getErrLine e)

1200+ (\e -> do setErrSpan (getErrSpan e)

1201 ist <- getIState

1202 ihRenderError h (pprintErr ist e))

1203

src/Idris/REPL.hs+6−6

@@ -238,7 +238,7 @@ ideslave orig mods

238 isetPrompt (mkPrompt [filename])

239 -- Report either success or failure

240 i <- getIState

241− case (errLine i) of

241+ case (errSpan i) of

242 Nothing -> iPrintResult $ "loaded " ++ filename

243 Just x -> iPrintError $ "didn't load " ++ filename

244 ideslave orig [filename]

@@ -246,7 +246,7 @@ ideslave orig mods

246 case splitName name of

247 Left err -> iPrintError err

248 Right n -> process stdout "(ideslave)"

249− (Check (PRef (FC "(ideslave)" 0 0) n))

249+ (Check (PRef (FC "(ideslave)" (0,0) (0,0)) n))

250 Just (IdeSlave.DocsFor name) ->

251 case splitName name of

252 Left err -> iPrintError err

@@ -412,7 +412,7 @@ edit f orig

412 = do i <- getIState

413 env <- runIO $ getEnvironment

414 let editor = getEditor env

415− let line = case errLine i of

415+ let line = case errSpan i of

416 Just l -> " +" ++ show l ++ " "

417 Nothing -> " "

418 let cmd = editor ++ line ++ fixName f

@@ -1125,7 +1125,7 @@ loadInputs h inputs

1125 -- to check everything worked consistently (in particular, will catch

1126 -- if the ibc version is out of date) if we weren't loading per

1127 -- module

1128− case errLine inew of

1128+ case errSpan inew of

1129 Nothing ->

1130 do putIState ist

1131 when (not loadCode) $ tryLoad $ nub (concat ifiles)

@@ -1133,10 +1133,10 @@ loadInputs h inputs

1133 putIState inew)

1134 (\e -> do i <- getIState

1135 case e of

1136− At f _ -> do setErrLine (fc_line f)

1136+ At f _ -> do setErrSpan f

1137 ihRenderError stdout $ pprintErr i e

1138 ProgramLineComment -> return () -- fail elsewhere

1139− _ -> do setErrLine 3 -- FIXME! Propagate it

1139+ _ -> do setErrSpan emptyFC -- FIXME! Propagate it

1140 iputStrLn (pshow i e))

1141 where -- load all files, stop if any fail

1142 tryLoad :: [IFileType] -> Idris ()

src/Idris/Unlit.hs+2−2

@@ -24,8 +24,8 @@ check f l [x] = return ()

24check f l [] = return ()

25

26chkAdj :: FilePath -> Int -> LineType -> LineType -> TC ()

27−chkAdj f l Prog Comm = tfail $ At (FC f l 0) ProgramLineComment --TODO: Include column?

27+chkAdj f l Prog Comm = tfail $ At (FC f (l, 0) (l, 0)) ProgramLineComment --TODO: Span correctly

28−chkAdj f l Comm Prog = tfail $ At (FC f l 0) ProgramLineComment --TODO: Include column?

28+chkAdj f l Comm Prog = tfail $ At (FC f (l, 0) (l, 0)) ProgramLineComment --TODO: Span correctly

29chkAdj f l _ _ = return ()

30

31

src/Pkg/Package.hs+2−2

@@ -52,7 +52,7 @@ buildPkg warnonly (install, fp)

52 Nothing -> exitWith (ExitFailure 1)

53 Just ist -> do

54 -- Quit with error code if there was a problem

55− case errLine ist of

55+ case errSpan ist of

56 Just _ -> exitWith (ExitFailure 1)

57 _ -> return ()

58 -- Also give up if there are metavariables to solve

@@ -85,7 +85,7 @@ checkPkg warnonly quit fpath

85 when quit $ case res of

86 Nothing -> exitWith (ExitFailure 1)

87 Just res' -> do

88− case errLine res' of

88+ case errSpan res' of

89 Just _ -> exitWith (ExitFailure 1)

90 _ -> return ()

91

test/README+1

@@ -12,5 +12,6 @@ primitives: Primitive types

12proof: Theorem proving, tactics

13sugar: Syntactic sugar, syntax extensions

14totality: Totality checking

15+tutorial: Examples from the tutorial

15

16

16reg: Regression tests, covering previous bug fixes

17reg: Regression tests, covering previous bug fixes

test/effects001/test021.idr+7−9

@@ -5,11 +5,11 @@ import Effect.State

5import Effect.StdIO

6import Control.IOExcept

7

8−data FName = Count | NotCount

8+data Count : Type where

9

10FileIO : Type -> Type -> Type

11FileIO st t

12− = Eff (IOExcept String) [FILE_IO st, STDIO, Count ::: STATE Int] t

12+ = { [FILE_IO st, STDIO, Count ::: STATE Int] } Eff IO t

13

14readFile : FileIO (OpenFile Read) (List String)

15readFile = readAcc [] where

@@ -22,14 +22,12 @@ readFile = readAcc [] where

22 else return (reverse acc)

23

24testFile : FileIO () ()

25−testFile = do open "testFile" Read

25+testFile = do True <- open "testFile" Read | False => putStrLn "Error!"

26− if_valid then do putStrLn (show !readFile)

26+ putStrLn (show !readFile)

27− close

27+ close

28− putStrLn (show !(Count :- get))

28+ putStrLn (show !(Count :- get))

29− else putStrLn ("Error!")

30

29

31main : IO ()

30main : IO ()

32−main = do ioe_run (run [(), (), Count := 0] testFile)

31+main = run testFile

33− (\err => print err) (\ok => return ())

34

32

35

33

test/effects001/test021a.idr+2−2

@@ -17,7 +17,7 @@ Env = List (String, Integer)

17-- Evaluator t

18-- = Eff m [EXCEPTION String, RND, STATE Env] t

19

20−eval : Expr -> Eff IO [EXCEPTION String, STDIO, RND, STATE Env] Integer

20+eval : Expr -> { [EXCEPTION String, STDIO, RND, STATE Env] } Eff IO Integer

21eval (Var x) = do vs <- get

22 case lookup x vs of

23 Nothing => raise ("No such variable " ++ x)

@@ -32,7 +32,7 @@ testExpr : Expr

32testExpr = Add (Add (Var "foo") (Val 42)) (Random 100)

33

34runEval : List (String, Integer) -> Expr -> IO Integer

35−runEval args expr = run [(), (), 123456, args] (eval expr)

35+runEval args expr = runInit [(), (), 123456, args] (eval expr)

36

37main : IO ()

38main = do let x = 42

test/effects002/test025.idr+4−4

@@ -5,8 +5,8 @@ import Effect.Memory

5import Control.IOExcept

6

7MemoryIO : Type -> Type -> Type -> Type

8−MemoryIO td ts r = Eff (IOExcept String) [ Dst ::: RAW_MEMORY td

8+MemoryIO td ts r = { [ Dst ::: RAW_MEMORY td

9− , Src ::: RAW_MEMORY ts ] r

9+ , Src ::: RAW_MEMORY ts ] } Eff (IOExcept String) r

10

11inpVect : Vect 5 Bits8

12inpVect = map prim__truncInt_B8 [0, 1, 2, 3, 5]

@@ -28,7 +28,7 @@ testMemory = do Src :- allocate 5

28 return (map (prim__zextB8_Int) res)

29

30main : IO ()

31−main = do ioe_run (run [Dst := (), Src := ()] testMemory)

31+main = ioe_run (runInit [Dst := (), Src := ()] testMemory)

32− (\err => print err) (\ok => print ok)

32+ (\err => print err) (\ok => print ok)

33

34

test/tutorial001/expectednew file

No changes to the content.

test/tutorial001/runnew file+3

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

1+#!/usr/bin/env bash

2+idris --check tutorial001.idr

3+rm -f *.ibc

test/tutorial001/tutorial001.idrnew file+9

@@ -0,0 +1,9 @@

1+foo : Int -> Int

2+foo x = case isLT of

3+ Yes => x*2

4+ No => x*4

5+ where

6+ data MyLT = Yes | No

7+ isLT : MyLT

8+ isLT = if x < 20 then Yes else No

9+