34f63d4 · Idris-dev · git.iko.soy

CHANGELOG+1−1

compare with master

unifiedsplit

@@ -7,7 +7,7 @@ New in 0.9.14:

7* Clearly distinguish between type providers and postulate providers at the use site

8* Allow dependent function syntax to be overridden in dsl blocks, similarly to

9 functions and let. The keyword for this is "pi".

10−* Experimental 'neweffects' library, with simplified API

10+* Updated 'effects' library, with simplified API

11* All new JavaScript backend (avoids callstack overflows)

12* Add support for %lib directive for NodeJS

13* Quasiquotes and quasiquote patterns allow easier work with reflected terms.

idris.cabal+12−6

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

1Name: idris

2−Version: 0.9.13.1

2+Version: 0.9.14

3License: BSD3

4License-file: LICENSE

5Author: Edwin Brady

@@ -117,11 +117,6 @@ Extra-source-files:

117 libs/effects/Effect/*.idr

118 libs/effects/*.idr

119

120− libs/neweffects/Makefile

121− libs/neweffects/effects.ipkg

122− libs/neweffects/Effect/*.idr

123− libs/neweffects/*.idr

124−

125 llvm/*.c

120 llvm/*.c

126 llvm/Makefile

121 llvm/Makefile

127

122

@@ -257,6 +252,12 @@ Extra-source-files:

257 test/reg045/run

252 test/reg045/run

258 test/reg045/*.idr

253 test/reg045/*.idr

259 test/reg045/expected

254 test/reg045/expected

255+ test/reg046/run

256+ test/reg046/*.idr

257+ test/reg046/expected

258+ test/reg047/run

259+ test/reg047/*.idr

260+ test/reg047/expected

260

261

261 test/basic001/run

262 test/basic001/run

262 test/basic001/*.idr

263 test/basic001/*.idr

@@ -438,6 +439,10 @@ Extra-source-files:

438 test/quasiquote002/run

439 test/quasiquote002/run

439 test/quasiquote002/*.idr

440 test/quasiquote002/*.idr

440 test/quasiquote002/expected

441 test/quasiquote002/expected

442+ test/quasiquote003/run

443+ test/quasiquote003/*.idr

444+ test/quasiquote003/expected

445+

441

446

442 test/records001/run

447 test/records001/run

443 test/records001/*.idr

448 test/records001/*.idr

@@ -609,6 +614,7 @@ Library

609 , IRTS.CodegenCommon

614 , IRTS.CodegenCommon

610 , IRTS.CodegenJava

615 , IRTS.CodegenJava

611 , IRTS.CodegenJavaScript

616 , IRTS.CodegenJavaScript

617+ , IRTS.JavaScript.AST

612 , IRTS.Compiler

618 , IRTS.Compiler

613 , IRTS.Defunctionalise

619 , IRTS.Defunctionalise

614 , IRTS.DumpBC

620 , IRTS.DumpBC

libs/Makefile−5

@@ -2,32 +2,27 @@ build:

2 $(MAKE) -C prelude build

3 $(MAKE) -C base build

4 $(MAKE) -C effects build

5− $(MAKE) -C neweffects build

6

5

7

6

8install:

7install:

9 $(MAKE) -C prelude install

8 $(MAKE) -C prelude install

10 $(MAKE) -C base install

9 $(MAKE) -C base install

11 $(MAKE) -C effects install

10 $(MAKE) -C effects install

12− $(MAKE) -C neweffects install

13

11

14clean:

12clean:

15 $(MAKE) -C prelude clean

13 $(MAKE) -C prelude clean

16 $(MAKE) -C base clean

14 $(MAKE) -C base clean

17 $(MAKE) -C effects clean

15 $(MAKE) -C effects clean

18− $(MAKE) -C neweffects clean

19

16

20doc:

17doc:

21 $(MAKE) -C prelude doc

18 $(MAKE) -C prelude doc

22 $(MAKE) -C base doc

19 $(MAKE) -C base doc

23 $(MAKE) -C effects doc

20 $(MAKE) -C effects doc

24− $(MAKE) -C neweffects doc

25

21

26doc_clean:

22doc_clean:

27 $(MAKE) -C prelude doc_clean

23 $(MAKE) -C prelude doc_clean

28 $(MAKE) -C base doc_clean

24 $(MAKE) -C base doc_clean

29 $(MAKE) -C effects doc_clean

25 $(MAKE) -C effects doc_clean

30− $(MAKE) -C neweffects doc_clean

31

26

32

27

33.PHONY: build install clean doc doc_clean

28.PHONY: build install clean doc doc_clean

libs/effects/Effect/Exception.idr+1−1

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

26EXCEPTION : Type -> EFFECT

27EXCEPTION t = MkEff () (Exception t)

28

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

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

30raise err = call $ Raise err

31

32

libs/effects/Effect/File.idr+5−5

@@ -105,24 +105,24 @@ open : (fname : String)

105 -> (m : Mode)

106 -> { [FILE_IO ()] ==> [FILE_IO (if result

107 then OpenFile m

108− else ())] } Eff e Bool

108+ else ())] } Eff Bool

109open f m = call $ Open f m

110

111

112||| Close a file.

113−close : { [FILE_IO (OpenFile m)] ==> [FILE_IO ()] } Eff e ()

113+close : { [FILE_IO (OpenFile m)] ==> [FILE_IO ()] } Eff ()

114close = call $ Close

115

116||| Read a line from the file.

117−readLine : { [FILE_IO (OpenFile Read)] } Eff e String

117+readLine : { [FILE_IO (OpenFile Read)] } Eff String

118readLine = call $ ReadLine

119

120||| Write a line to a file.

121−writeLine : String -> { [FILE_IO (OpenFile Write)] } Eff e ()

121+writeLine : String -> { [FILE_IO (OpenFile Write)] } Eff ()

122writeLine str = call $ WriteLine str

123

124||| End of file?

125−eof : { [FILE_IO (OpenFile Read)] } Eff e Bool

125+eof : { [FILE_IO (OpenFile Read)] } Eff Bool

126eof = call $ EOF

127

128-- --------------------------------------------------------------------- [ EOF ]

libs/effects/Effect/Memory.idr+8−8

@@ -101,7 +101,7 @@ RAW_MEMORY : Type -> EFFECT

101RAW_MEMORY t = MkEff t RawMemory

102

103allocate : (n : Nat) ->

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

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

105allocate size = call $ Allocate size

106

107initialize : {i : Nat} ->

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

109 Bits8 ->

110 (size : Nat) ->

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

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

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

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

114initialize c size prf = call $ Initialize c size prf

115

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

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

117free = call Free

118

119peek : {i : Nat} ->

120 (offset : Nat) ->

121 (size : Nat) ->

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

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

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

124peek offset size prf = call $ Peek offset size prf

125

126poke : {n : Nat} ->

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

128 (offset : Nat) ->

129 Vect size Bits8 ->

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

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

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

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

133poke offset content prf = call $ Poke offset content prf

134

135private

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

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

137getRawPtr = call $ GetRawPtr

138

139private

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

146 (size : Nat) ->

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

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

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

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

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

151move' src_ptr dst_offset src_offset size dst_bounds src_bounds

152 = call $ Move src_ptr dst_offset src_offset size dst_bounds src_bounds

@@ -162,7 +162,7 @@ move : {dst_size : Nat} ->

162 (size : Nat) ->

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

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

165− Eff m ()

165+ Eff ()

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

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

168 (\v =>

libs/effects/Effect/Random.idr+5−5

@@ -17,14 +17,14 @@ RND : EFFECT

17RND = MkEff Integer Random

18

19||| Generates a random Integer in a given range

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

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

21rndInt lower upper = do v <- call $ getRandom

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

23

24||| Generate a random number in Fin (S `k`)

25|||

26||| Note that rndFin k takes values 0, 1, ..., k.

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

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

28rndFin k = do let v = assert_total $ !(call getRandom) `prim__sremBigInt` (cast (S k))

29 return (toFin v)

30 where toFin : Integer -> Fin (S k)

@@ -33,15 +33,15 @@ rndFin k = do let v = assert_total $ !(call getRandom) `prim__sremBigInt` (cast

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

34

35||| Select a random element from a vector

36−rndSelect' : Vect (S k) a -> { [RND] } Eff IO a

36+rndSelect' : Vect (S k) a -> { [RND] } Eff a

37rndSelect' {k} xs = return (Vect.index !(rndFin k) xs)

38

39||| Select a random element from a list, or Nothing if the list is empty

40−rndSelect : List a -> { [RND] } Eff IO (Maybe a)

40+rndSelect : List a -> { [RND] } Eff (Maybe a)

41rndSelect [] = return Nothing

42rndSelect (x::xs) = return (Just !(rndSelect' (x::(fromList xs))))

43

44||| Sets the random seed

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

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

46srand n = call $ setSeed n

47

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

@@ -18,6 +18,6 @@ instance Handler Selection List where

18SELECT : EFFECT

19SELECT = MkEff () Selection

20

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

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

22select xs = call $ Select xs

23

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

@@ -8,30 +8,30 @@ data State : Effect where

8 Get : { a } State a

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

10

11−using (m : Type -> Type)

11+-- using (m : Type -> Type)

12− instance Handler State m where

12+instance Handler State m where

13 handle st Get k = k st st

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 : { [STATE x] } Eff x

20get = call $ Get

21

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

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

23put val = call $ Put val

24

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

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

26putM val = call $ Put val

27

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

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

29update f = put (f !get)

30

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

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

32updateM f = putM (f !get)

33

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

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

35locally newst prog = do st <- get

36 putM newst

37 val <- prog

libs/effects/Effect/StdIO.idr+5−5

@@ -39,22 +39,22 @@ STDIO : EFFECT

39STDIO = MkEff () StdIO

40

41||| Write a string to standard output.

42−putStr : String -> { [STDIO] } Eff e ()

42+putStr : String -> { [STDIO] } Eff ()

43putStr s = call $ PutStr s

44

45||| Write a character to standard output.

46−putChar : Char -> { [STDIO] } Eff e ()

46+putChar : Char -> { [STDIO] } Eff ()

47putChar c = call $ PutCh c

48

49||| Write a string to standard output, terminating with a newline.

50−putStrLn : String -> { [STDIO] } Eff e ()

50+putStrLn : String -> { [STDIO] } Eff ()

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

52

53||| Read a string from standard input.

54−getStr : { [STDIO] } Eff e String

54+getStr : { [STDIO] } Eff String

55getStr = call $ GetStr

56

57||| Read a character from standard input.

58−getChar : { [STDIO] } Eff e Char

58+getChar : { [STDIO] } Eff Char

59getChar = call $ GetCh

60

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

@@ -30,14 +30,14 @@ instance Handler System (IOExcept a) where

30SYSTEM : EFFECT

31SYSTEM = MkEff () System

32

33−getArgs : Handler System e => { [SYSTEM] } Eff e (List String)

33+getArgs : { [SYSTEM] } Eff (List String)

34getArgs = call Args

35

36−time : Handler System e => { [SYSTEM] } Eff e Int

36+time : { [SYSTEM] } Eff Int

37time = call Time

38

39−getEnv : Handler System e => String -> { [SYSTEM] } Eff e (Maybe String)

39+getEnv : String -> { [SYSTEM] } Eff (Maybe String)

40getEnv s = call $ GetEnv s

41

42−system : Handler System e => String -> { [SYSTEM] } Eff e Int

42+system : String -> { [SYSTEM] } Eff Int

43system s = call $ CSystem s

libs/effects/Effects.idr+56−75

@@ -55,15 +55,14 @@ syntax "{" [inst] "==>" "{" {b} "}" [outst] "}" [eff]

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

56

57-- --------------------------------------- [ Properties and Proof Construction ]

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

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

58+data SubList : List a -> List a -> Type where

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

59+ SubNil : SubList [] []

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

60+ Keep : SubList xs ys -> SubList (x :: xs) (x :: ys)

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

61+ Drop : SubList xs ys -> SubList xs (x :: ys)

63

62

64− subListId : SubList xs xs

63+subListId : SubList xs xs

65− subListId {xs = Nil} = SubNil

64+subListId {xs = Nil} = SubNil

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

65+subListId {xs = x :: xs} = Keep subListId

67

66

68namespace Env

67namespace Env

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

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

@@ -129,41 +128,32 @@ relabel {xs = []} l [] = []

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

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

130

129

131-- ------------------------------------------------- [ The Language of Effects ]

130-- ------------------------------------------------- [ The Language of Effects ]

132−||| Definition of an Effect.

131+||| Definition of a language of effectful programs.

133|||

132|||

134−||| @ m The computation context

135||| @ x The return type of the result.

133||| @ x The return type of the result.

136||| @ es The list of allowed side-effects.

134||| @ es The list of allowed side-effects.

137||| @ ce Function to compute a new list of allowed side-effects.

135||| @ ce Function to compute a new list of allowed side-effects.

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

139− -> (x : Type)

136+data Eff : (x : Type)

140 -> (es : List EFFECT)

137 -> (es : List EFFECT)

141 -> (ce : x -> List EFFECT) -> Type where

138 -> (ce : x -> List EFFECT) -> Type where

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

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

143− with_val : (val : a) -> Eff m () xs (\v => xs' val) ->

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

144− Eff m a xs xs'

141+ Eff a xs xs'

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

142+ ebind : Eff a xs xs' ->

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

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

147 callP : (prf : EffElem e a xs) ->

144 callP : (prf : EffElem e a xs) ->

148 (eff : e t a b) ->

145 (eff : e t a b) ->

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

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

150

147

151 liftP : (prf : SubList ys xs) ->

148 liftP : (prf : SubList ys xs) ->

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

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

153− newInit : Handler e m =>

154− res ->

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

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

157− catch : Catchable m err =>

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

159− Eff m a xs xs'

160

150

161 (:-) : (l : ty) ->

151 (:-) : (l : ty) ->

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

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

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

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

164

154

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

155+(>>=) : Eff a xs xs' ->

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

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

167(>>=) = ebind

157(>>=) = ebind

168

158

169-- namespace SimpleBind

159-- namespace SimpleBind

@@ -172,28 +162,28 @@ data Eff : (m : Type -> Type)

172-- (>>=) = ebind

162-- (>>=) = ebind

173

163

174||| Run a subprogram which results in an effect state the same as the input.

164||| Run a subprogram which results in an effect state the same as the input.

175−staticEff : Eff m a xs (\v => xs) -> Eff m a xs (\v => xs)

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

176staticEff = id

166staticEff = id

177

167

178||| Explicitly give the expected set of result effects for an effectful

168||| Explicitly give the expected set of result effects for an effectful

179||| operation.

169||| operation.

180−toEff : .(xs' : List EFFECT) -> Eff m a xs (\v => xs') -> Eff m a xs (\v => xs')

170+toEff : .(xs' : List EFFECT) -> Eff a xs (\v => xs') -> Eff a xs (\v => xs')

181toEff xs' = id

171toEff xs' = id

182

172

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

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

184return x = value x

174return x = value x

185

175

186-- ------------------------------------------------------ [ for idiom brackets ]

176-- ------------------------------------------------------ [ for idiom brackets ]

187

177

188infixl 2 <$>

178infixl 2 <$>

189

179

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

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

191pure = value

181pure = value

192

182

193syntax pureM [val] = with_val val (pure ())

183syntax pureM [val] = with_val val (pure ())

194

184

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

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

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

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

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

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

198 arg <- v

188 arg <- v

199 return (fn arg)

189 return (fn arg)

@@ -213,7 +203,7 @@ execEff {e} {a} {res} {resk} (val :: env) (There p) eff k

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

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

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

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

215

205

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

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

217eff env (value x) k = k x env

207eff env (value x) k = k x env

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

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

219eff env (prog `ebind` c) k

209eff env (prog `ebind` c) k

@@ -222,11 +212,6 @@ eff env (callP prf effP) k = execEff env prf effP k

222eff env (liftP prf effP) k

212eff env (liftP prf effP) k

223 = let env' = dropEnv env prf in

213 = let env' = dropEnv env prf in

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

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

225−eff env (newInit r prog) k

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

227−eff env (catch prog handler) k

228− = catch (eff env prog k)

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

230-- FIXME:

215-- FIXME:

231-- xs is needed explicitly because otherwise the pattern binding for

216-- xs is needed explicitly because otherwise the pattern binding for

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

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

@@ -249,84 +234,80 @@ syntax MkDefaultEnv = with Env

249

234

250call : {a, b: _} -> {e : Effect} ->

235call : {a, b: _} -> {e : Effect} ->

251 (eff : e t a b) ->

236 (eff : e t a b) ->

237+ {default tactics { search 100; }

252− {auto prf : EffElem e a xs} ->

238+ prf : EffElem e a xs} ->

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

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

254call e {prf} = callP prf e

240call e {prf} = callP prf e

255

241

256implicit

242implicit

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

243+lift : Eff t ys ys' ->

244+ {default tactics { search 100; }

258− {auto prf : SubList ys xs} ->

245+ prf : SubList ys xs} ->

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

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

260lift e {prf} = liftP prf e

247lift e {prf} = liftP prf e

261

248

262

249

263−new : Handler e m =>

264− {default default r : res} ->

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

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

267−new {r} e = newInit r e

268−

269-- --------------------------------------------------------- [ Running Effects ]

250-- --------------------------------------------------------- [ Running Effects ]

270−

271||| Run an effectful program.

251||| Run an effectful program.

272|||

252|||

273−||| The content (`m`) in which to run the program is taken from the environment in which the program is called.

253+||| The content (`m`) in which to run the program is taken from the

254+||| environment in which the program is called. The `env` argument is

274−||| The `env` argument is implicit and initialised automatically.

255+||| implicit and initialised automatically.

275|||

256|||

276||| @prog The effectful program to run.

257||| @prog The effectful program to run.

277−run : Applicative m => {default MkDefaultEnv env : Env m xs} -> (prog : Eff m a xs xs') -> m a

258+run : Applicative m => {default MkDefaultEnv env : Env m xs}

259+ -> (prog : Eff a xs xs') -> m a

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

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

279

261

280−||| Run an effectful program in the identity context `id`.

262+||| Run an effectful program in the identity context.

281|||

263|||

282||| A helper function useful for when the given context is 'pure'.

264||| A helper function useful for when the given context is 'pure'.

283||| The `env` argument is implicit and initialised automatically.

265||| The `env` argument is implicit and initialised automatically.

284|||

266|||

285||| @prog The effectful program to run.

267||| @prog The effectful program to run.

286−runPure : {default MkDefaultEnv env : Env id xs} -> (prog : Eff id a xs xs') -> a

268+runPure : {default MkDefaultEnv env : Env id xs} -> (prog : Eff a xs xs') -> a

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

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

288

270

289−||| Run an effectful program with a default value for the environment context.

271+||| Run an effectful program in a given context `m` with a default value for the environment.

290|||

272|||

291−||| This is useful for when no default value exists for a given resource type.

273+||| This is useful for when there is no default environment for the given context.

292|||

274|||

293−||| @val The default value for the resource type.

275+||| @env The environment to use.

294||| @prog The effectful program to run.

276||| @prog The effectful program to run.

295−runInit : Applicative m => (val : Env m xs) -> (prog : Eff m a xs xs') -> m a

277+runInit : Applicative m => (env : Env m xs) -> (prog : Eff a xs xs') -> m a

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

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

297

279

298−||| Run an effectful program in the identity context `id` with a given default value for the environment context.

280+||| Run an effectful program with a given default value for the environment.

299|||

281|||

300−||| A helper function useful for when the given context is 'pure'.

282+||| A helper function useful for when the given context is 'pure' and there is no default environment.

301|||

283|||

302−||| @val The default value for the resource type.

284+||| @env The environment to use.

303||| @prog The effectful program to run.

285||| @prog The effectful program to run.

304−runPureInit : (val : Env id xs) -> (prog : Eff id a xs xs') -> a

286+runPureInit : (env : Env id xs) -> (prog : Eff a xs xs') -> a

305runPureInit env prog = eff env prog (\r, env => r)

287runPureInit env prog = eff env prog (\r, env => r)

306

288

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

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

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

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

309

291

310−runEnv : Applicative m => Env m xs -> Eff m a xs xs' ->

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

311 m (x : a ** Env m (xs' x))

293 m (x : a ** Env m (xs' x))

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

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

313

295

314-- ----------------------------------------------- [ some higher order things ]

296-- ----------------------------------------------- [ some higher order things ]

315

297

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

298+mapE : (a -> {xs} Eff b) -> List a -> {xs} Eff (List b)

317mapE f [] = pure []

299mapE f [] = pure []

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

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

319

301

320

302

321−mapVE : Applicative m =>

322− (a -> {xs} Eff m b) ->

303+mapVE : (a -> {xs} Eff b) ->

323− Vect n a ->

304+ Vect n a ->

324− {xs} Eff m (Vect n b)

305+ {xs} Eff (Vect n b)

325mapVE f [] = pure []

306mapVE f [] = pure []

326mapVE f (x :: xs) = [| f x :: mapVE f xs |]

307mapVE f (x :: xs) = [| f x :: mapVE f xs |]

327

308

328

309

329−when : Applicative m => Bool -> Lazy ({xs} Eff m ()) -> {xs} Eff m ()

310+when : Bool -> Lazy ({xs} Eff ()) -> {xs} Eff ()

330when True e = Force e

311when True e = Force e

331when False e = pure ()

312when False e = pure ()

332

313

libs/effects/Makefile+5−13

@@ -1,22 +1,14 @@

1−IDRIS := idris

1+IDRIS := idris

2−

3−PKG := effects

4

2

5build:

3build:

6− $(IDRIS) --build ${PKG}.ipkg

4+ $(IDRIS) --build effects.ipkg

7

5

8clean:

6clean:

9− $(IDRIS) --clean ${PKG}.ipkg

7+ $(IDRIS) --clean effects.ipkg

10

8

11install:

9install:

12− $(IDRIS) --install ${PKG}.ipkg

10+ $(IDRIS) --install effects.ipkg

13

11

14rebuild: clean build

12rebuild: clean build

15

13

16−doc:

17− $(IDRIS) --mkdoc ${PKG}.ipkg

18−

19−doc_clean:

20− rm -rf ${PKG}_doc

21−

22−.PHONY: build clean install rebuild doc doc_clean

14+.PHONY: build clean install rebuild

libs/neweffects/Makefiledeleted−14

@@ -1,14 +0,0 @@

1−IDRIS := idris

2−

3−build:

4− $(IDRIS) --build effects.ipkg

5−

6−clean:

7− $(IDRIS) --clean effects.ipkg

8−

9−install:

10− $(IDRIS) --install effects.ipkg

11−

12−rebuild: clean build

13−

14−.PHONY: build clean install rebuild

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

The content is the same.

libs/neweffects/Effect/Exception.idr → libs/oldeffects/Effect/Exception.idrrenamed+1−1

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

26EXCEPTION : Type -> EFFECT

27EXCEPTION t = MkEff () (Exception t)

28

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

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

30raise err = call $ Raise err

31

32

libs/neweffects/Effect/File.idr → libs/oldeffects/Effect/File.idrrenamed+5−5

@@ -105,24 +105,24 @@ open : (fname : String)

105 -> (m : Mode)

106 -> { [FILE_IO ()] ==> [FILE_IO (if result

107 then OpenFile m

108− else ())] } Eff Bool

108+ else ())] } Eff e Bool

109open f m = call $ Open f m

110

111

112||| Close a file.

113−close : { [FILE_IO (OpenFile m)] ==> [FILE_IO ()] } Eff ()

113+close : { [FILE_IO (OpenFile m)] ==> [FILE_IO ()] } Eff e ()

114close = call $ Close

115

116||| Read a line from the file.

117−readLine : { [FILE_IO (OpenFile Read)] } Eff String

117+readLine : { [FILE_IO (OpenFile Read)] } Eff e String

118readLine = call $ ReadLine

119

120||| Write a line to a file.

121−writeLine : String -> { [FILE_IO (OpenFile Write)] } Eff ()

121+writeLine : String -> { [FILE_IO (OpenFile Write)] } Eff e ()

122writeLine str = call $ WriteLine str

123

124||| End of file?

125−eof : { [FILE_IO (OpenFile Read)] } Eff Bool

125+eof : { [FILE_IO (OpenFile Read)] } Eff e Bool

126eof = call $ EOF

127

128-- --------------------------------------------------------------------- [ EOF ]

libs/neweffects/Effect/Memory.idr → libs/oldeffects/Effect/Memory.idrrenamed+8−8

@@ -101,7 +101,7 @@ RAW_MEMORY : Type -> EFFECT

101RAW_MEMORY t = MkEff t RawMemory

102

103allocate : (n : Nat) ->

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

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

105allocate size = call $ Allocate size

106

107initialize : {i : Nat} ->

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

109 Bits8 ->

110 (size : Nat) ->

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

112− Eff () [RAW_MEMORY (MemoryChunk n i)]

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

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

114initialize c size prf = call $ Initialize c size prf

115

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

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

117free = call Free

118

119peek : {i : Nat} ->

120 (offset : Nat) ->

121 (size : Nat) ->

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

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

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

124peek offset size prf = call $ Peek offset size prf

125

126poke : {n : Nat} ->

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

128 (offset : Nat) ->

129 Vect size Bits8 ->

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

131− Eff () [RAW_MEMORY (MemoryChunk n i)]

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

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

133poke offset content prf = call $ Poke offset content prf

134

135private

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

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

137getRawPtr = call $ GetRawPtr

138

139private

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

146 (size : Nat) ->

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

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

149− Eff () [RAW_MEMORY (MemoryChunk dst_size dst_init)]

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

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

151move' src_ptr dst_offset src_offset size dst_bounds src_bounds

152 = call $ Move src_ptr dst_offset src_offset size dst_bounds src_bounds

@@ -162,7 +162,7 @@ move : {dst_size : Nat} ->

162 (size : Nat) ->

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

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

165− Eff ()

165+ Eff m ()

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

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

168 (\v =>

libs/neweffects/Effect/Monad.idr → libs/oldeffects/Effect/Monad.idrrenamed

The content is the same.

libs/neweffects/Effect/Random.idr → libs/oldeffects/Effect/Random.idrrenamed+5−5

@@ -17,14 +17,14 @@ RND : EFFECT

17RND = MkEff Integer Random

18

19||| Generates a random Integer in a given range

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

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

21rndInt lower upper = do v <- call $ getRandom

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

23

24||| Generate a random number in Fin (S `k`)

25|||

26||| Note that rndFin k takes values 0, 1, ..., k.

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

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

28rndFin k = do let v = assert_total $ !(call getRandom) `prim__sremBigInt` (cast (S k))

29 return (toFin v)

30 where toFin : Integer -> Fin (S k)

@@ -33,15 +33,15 @@ rndFin k = do let v = assert_total $ !(call getRandom) `prim__sremBigInt` (cast

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

34

35||| Select a random element from a vector

36−rndSelect' : Vect (S k) a -> { [RND] } Eff a

36+rndSelect' : Vect (S k) a -> { [RND] } Eff IO a

37rndSelect' {k} xs = return (Vect.index !(rndFin k) xs)

38

39||| Select a random element from a list, or Nothing if the list is empty

40−rndSelect : List a -> { [RND] } Eff (Maybe a)

40+rndSelect : List a -> { [RND] } Eff IO (Maybe a)

41rndSelect [] = return Nothing

42rndSelect (x::xs) = return (Just !(rndSelect' (x::(fromList xs))))

43

44||| Sets the random seed

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

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

46srand n = call $ setSeed n

47

libs/neweffects/Effect/Select.idr → libs/oldeffects/Effect/Select.idrrenamed+1−1

@@ -18,6 +18,6 @@ instance Handler Selection List where

18SELECT : EFFECT

19SELECT = MkEff () Selection

20

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

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

22select xs = call $ Select xs

23

libs/neweffects/Effect/State.idr → libs/oldeffects/Effect/State.idrrenamed+6−6

@@ -16,22 +16,22 @@ using (m : Type -> Type)

16STATE : Type -> EFFECT

17STATE t = MkEff t State

18

19−get : { [STATE x] } Eff x

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

20get = call $ Get

21

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

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

23put val = call $ Put val

24

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

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

26putM val = call $ Put val

27

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

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

29update f = put (f !get)

30

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

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

32updateM f = putM (f !get)

33

34−locally : x -> ({ [STATE x] } Eff t) -> { [STATE y] } Eff 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/neweffects/Effect/StdIO.idr → libs/oldeffects/Effect/StdIO.idrrenamed+5−5

@@ -39,22 +39,22 @@ STDIO : EFFECT

39STDIO = MkEff () StdIO

40

41||| Write a string to standard output.

42−putStr : String -> { [STDIO] } Eff ()

42+putStr : String -> { [STDIO] } Eff e ()

43putStr s = call $ PutStr s

44

45||| Write a character to standard output.

46−putChar : Char -> { [STDIO] } Eff ()

46+putChar : Char -> { [STDIO] } Eff e ()

47putChar c = call $ PutCh c

48

49||| Write a string to standard output, terminating with a newline.

50−putStrLn : String -> { [STDIO] } Eff ()

50+putStrLn : String -> { [STDIO] } Eff e ()

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

52

53||| Read a string from standard input.

54−getStr : { [STDIO] } Eff String

54+getStr : { [STDIO] } Eff e String

55getStr = call $ GetStr

56

57||| Read a character from standard input.

58−getChar : { [STDIO] } Eff Char

58+getChar : { [STDIO] } Eff e Char

59getChar = call $ GetCh

60

libs/neweffects/Effect/System.idr → libs/oldeffects/Effect/System.idrrenamed+4−4

@@ -30,14 +30,14 @@ instance Handler System (IOExcept a) where

30SYSTEM : EFFECT

31SYSTEM = MkEff () System

32

33−getArgs : { [SYSTEM] } Eff (List String)

33+getArgs : Handler System e => { [SYSTEM] } Eff e (List String)

34getArgs = call Args

35

36−time : { [SYSTEM] } Eff Int

36+time : Handler System e => { [SYSTEM] } Eff e Int

37time = call Time

38

39−getEnv : String -> { [SYSTEM] } Eff (Maybe String)

39+getEnv : Handler System e => String -> { [SYSTEM] } Eff e (Maybe String)

40getEnv s = call $ GetEnv s

41

42−system : String -> { [SYSTEM] } Eff Int

42+system : Handler System e => String -> { [SYSTEM] } Eff e Int

43system s = call $ CSystem s

libs/neweffects/Effects.idr → libs/oldeffects/Effects.idrrenamed+102−59

@@ -10,7 +10,7 @@ import Effect.Default

10%access public

11-- ----------------------------------------------------------------- [ Effects ]

12||| The Effect type describes effectful computations.

13−|||

13+|||

14||| This type is parameterised by:

15||| + The input resource.

16||| + The return type of the computation.

@@ -28,11 +28,11 @@ data EFFECT : Type where

28||| underlying computation context `m` for execution.

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

30 ||| How to handle the effect.

31− |||

31+ |||

32 ||| @ r The resource being handled.

33 ||| @ eff The effect to be applied.

34 ||| @ k The continuation to pass the result of the effect

35− covering handle : (r : res) -> (eff : e t res resk) ->

35+ covering handle : (r : res) -> (eff : e t res resk) ->

36 (k : ((x : t) -> resk x -> m a)) -> m a

37

38||| Get the resource type (handy at the REPL to find out about an effect)

@@ -48,27 +48,28 @@ resourceType (MkEff t e) = t

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

49

50-- The state transition is dependent on a result `b`, a bound variable.

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

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

52 = eff inst (\b => outst)

53

54--- A simple state transition

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

56

57-- --------------------------------------- [ Properties and Proof Construction ]

58+using (xs : List a, ys : List a)

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

59+ data SubList : List a -> List a -> Type where

59− SubNil : SubList [] []

60+ SubNil : SubList {a} [] []

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

61+ Keep : SubList xs ys -> SubList (x :: xs) (x :: ys)

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

62+ Drop : SubList xs ys -> SubList xs (x :: ys)

62

63

63−subListId : SubList xs xs

64+ subListId : SubList xs xs

64−subListId {xs = Nil} = SubNil

65+ subListId {xs = Nil} = SubNil

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

66+ subListId {xs = x :: xs} = Keep subListId

66

67

67namespace Env

68namespace Env

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

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

69 Nil : Env m Nil

70 Nil : Env m Nil

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

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

71−

72+

72data EffElem : Effect -> Type ->

73data EffElem : Effect -> Type ->

73 List EFFECT -> Type where

74 List EFFECT -> Type where

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

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

@@ -128,62 +129,71 @@ relabel {xs = []} l [] = []

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

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

129

130

130-- ------------------------------------------------- [ The Language of Effects ]

131-- ------------------------------------------------- [ The Language of Effects ]

131−||| Definition of a language of effectful programs.

132+||| Definition of an Effect.

132−|||

133+|||

134+||| @ m The computation context

133||| @ x The return type of the result.

135||| @ x The return type of the result.

134||| @ es The list of allowed side-effects.

136||| @ es The list of allowed side-effects.

135||| @ ce Function to compute a new list of allowed side-effects.

137||| @ ce Function to compute a new list of allowed side-effects.

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

136−data Eff : (x : Type)

139+ -> (x : Type)

137 -> (es : List EFFECT)

140 -> (es : List EFFECT)

138 -> (ce : x -> List EFFECT) -> Type where

141 -> (ce : x -> List EFFECT) -> Type where

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

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

140− with_val : (val : a) -> Eff () xs (\v => xs' val) ->

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

141− Eff a xs xs'

144+ Eff m a xs xs'

142− ebind : Eff a xs xs' ->

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

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

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

144 callP : (prf : EffElem e a xs) ->

147 callP : (prf : EffElem e a xs) ->

145 (eff : e t a b) ->

148 (eff : e t a b) ->

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

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

147

150

148 liftP : (prf : SubList ys xs) ->

151 liftP : (prf : SubList ys xs) ->

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

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

150−

153+ newInit : Handler e m =>

154+ res ->

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

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

157+ catch : Catchable m err =>

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

159+ Eff m a xs xs'

160+

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

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

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

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

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

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

154−

164+

155−(>>=) : Eff a xs xs' ->

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

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

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

157−(>>=) = ebind

167+(>>=) = ebind

158

168

159-- namespace SimpleBind

169-- namespace SimpleBind

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

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

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

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

162−-- (>>=) = ebind

172+-- (>>=) = ebind

163

173

164||| Run a subprogram which results in an effect state the same as the input.

174||| Run a subprogram which results in an effect state the same as the input.

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

175+staticEff : Eff m a xs (\v => xs) -> Eff m a xs (\v => xs)

166staticEff = id

176staticEff = id

167

177

168||| Explicitly give the expected set of result effects for an effectful

178||| Explicitly give the expected set of result effects for an effectful

169||| operation.

179||| operation.

170−toEff : .(xs' : List EFFECT) -> Eff a xs (\v => xs') -> Eff a xs (\v => xs')

180+toEff : .(xs' : List EFFECT) -> Eff m a xs (\v => xs') -> Eff m a xs (\v => xs')

171toEff xs' = id

181toEff xs' = id

172

182

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

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

174return x = value x

184return x = value x

175

185

176-- ------------------------------------------------------ [ for idiom brackets ]

186-- ------------------------------------------------------ [ for idiom brackets ]

177

187

178infixl 2 <$>

188infixl 2 <$>

179

189

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

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

181pure = value

191pure = value

182

192

183syntax pureM [val] = with_val val (pure ())

193syntax pureM [val] = with_val val (pure ())

184

194

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

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

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

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

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

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

188 arg <- v

198 arg <- v

189 return (fn arg)

199 return (fn arg)

@@ -203,15 +213,20 @@ execEff {e} {a} {res} {resk} (val :: env) (There p) eff k

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

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

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

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

205

215

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

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

207eff env (value x) k = k x env

217eff env (value x) k = k x env

208−eff env (with_val x prog) k = eff env prog (\p', env' => k x env')

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

209eff env (prog `ebind` c) k

219eff env (prog `ebind` c) k

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

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

211eff env (callP prf effP) k = execEff env prf effP k

221eff env (callP prf effP) k = execEff env prf effP k

212eff env (liftP prf effP) k

222eff env (liftP prf effP) k

213 = let env' = dropEnv env prf in

223 = let env' = dropEnv env prf in

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

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

225+eff env (newInit r prog) k

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

227+eff env (catch prog handler) k

228+ = catch (eff env prog k)

229+ (\e => eff env (handler e) k)

215-- FIXME:

230-- FIXME:

216-- xs is needed explicitly because otherwise the pattern binding for

231-- xs is needed explicitly because otherwise the pattern binding for

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

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

@@ -234,56 +249,84 @@ syntax MkDefaultEnv = with Env

234

249

235call : {a, b: _} -> {e : Effect} ->

250call : {a, b: _} -> {e : Effect} ->

236 (eff : e t a b) ->

251 (eff : e t a b) ->

237− {default tactics { search 100; }

238− prf : EffElem e a xs} ->

252+ {auto prf : EffElem e a xs} ->

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

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

240call e {prf} = callP prf e

254call e {prf} = callP prf e

241

255

242implicit

256implicit

243−lift : Eff t ys ys' ->

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

244− {default tactics { search 100; }

245− prf : SubList ys xs} ->

258+ {auto prf : SubList ys xs} ->

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

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

247lift e {prf} = liftP prf e

260lift e {prf} = liftP prf e

248

261

249

262

263+new : Handler e m =>

264+ {default default r : res} ->

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

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

267+new {r} e = newInit r e

268+

250-- --------------------------------------------------------- [ Running Effects ]

269-- --------------------------------------------------------- [ Running Effects ]

251

270

252−||| Run an effectful program

271+||| Run an effectful program.

272+|||

273+||| The content (`m`) in which to run the program is taken from the environment in which the program is called.

274+||| The `env` argument is implicit and initialised automatically.

275+|||

276+||| @prog The effectful program to run.

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

277+run : Applicative m => {default MkDefaultEnv env : Env m xs} -> (prog : Eff m a xs xs') -> m a

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

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

255

279

280+||| Run an effectful program in the identity context `id`.

281+|||

282+||| A helper function useful for when the given context is 'pure'.

283+||| The `env` argument is implicit and initialised automatically.

284+|||

285+||| @prog The effectful program to run.

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

286+runPure : {default MkDefaultEnv env : Env id xs} -> (prog : Eff id a xs xs') -> a

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

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

258

288

289+||| Run an effectful program with a default value for the environment context.

290+|||

291+||| This is useful for when no default value exists for a given resource type.

292+|||

293+||| @val The default value for the resource type.

294+||| @prog The effectful program to run.

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

295+runInit : Applicative m => (val : Env m xs) -> (prog : Eff m a xs xs') -> m a

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

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

261

297

298+||| Run an effectful program in the identity context `id` with a given default value for the environment context.

299+|||

300+||| A helper function useful for when the given context is 'pure'.

301+|||

302+||| @val The default value for the resource type.

303+||| @prog The effectful program to run.

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

304+runPureInit : (val : Env id xs) -> (prog : Eff id a xs xs') -> a

263runPureInit env prog = eff env prog (\r, env => r)

305runPureInit env prog = eff env prog (\r, env => r)

264

306

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

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

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

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

267

309

268−runEnv : Applicative m => Env m xs -> Eff a xs xs' ->

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

269 m (x : a ** Env m (xs' x))

311 m (x : a ** Env m (xs' x))

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

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

271

313

272-- ----------------------------------------------- [ some higher order things ]

314-- ----------------------------------------------- [ some higher order things ]

273

315

274−mapE : (a -> {xs} Eff b) -> List a -> {xs} Eff (List b)

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

275mapE f [] = pure []

317mapE f [] = pure []

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

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

277

319

278

320

321+mapVE : Applicative m =>

279−mapVE : (a -> {xs} Eff b) ->

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

280− Vect n a ->

323+ Vect n a ->

281− {xs} Eff (Vect n b)

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

282mapVE f [] = pure []

325mapVE f [] = pure []

283mapVE f (x :: xs) = [| f x :: mapVE f xs |]

326mapVE f (x :: xs) = [| f x :: mapVE f xs |]

284

327

285

328

286−when : Bool -> Lazy ({xs} Eff ()) -> {xs} Eff ()

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

287when True e = Force e

330when True e = Force e

288when False e = pure ()

331when False e = pure ()

289

332

libs/oldeffects/Makefilenew file+22

@@ -0,0 +1,22 @@

1+IDRIS := idris

2+

3+PKG := effects

4+

5+build:

6+ $(IDRIS) --build ${PKG}.ipkg

7+

8+clean:

9+ $(IDRIS) --clean ${PKG}.ipkg

10+

11+install:

12+ $(IDRIS) --install ${PKG}.ipkg

13+

14+rebuild: clean build

15+

16+doc:

17+ $(IDRIS) --mkdoc ${PKG}.ipkg

18+

19+doc_clean:

20+ rm -rf ${PKG}_doc

21+

22+.PHONY: build clean install rebuild doc doc_clean

libs/neweffects/effects.ipkg → libs/oldeffects/effects.ipkgrenamed+1−1

@@ -1,4 +1,4 @@

1−package neweffects

1+package oldeffects

2

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

4modules = Effects, Effect.Default,

libs/prelude/Builtins.idr+8

@@ -15,6 +15,14 @@ FalseElim : _|_ -> a

15||| For 'symbol syntax. 'foo becomes Symbol_ "foo"

16data Symbol_ : String -> Type where

17

18+-- Eq_ : a -> a -> Type

19+-- Eq_ x y = (=) _ _ x y

20+

21+infix 5 ~=~

22+

23+(~=~) : a -> b -> Type

24+(~=~) x y = (=) _ _ x y

25+

18-- ------------------------------------------------------ [ For rewrite tactic ]

26-- ------------------------------------------------------ [ For rewrite tactic ]

19||| Perform substitution in a term according to some equality.

27||| Perform substitution in a term according to some equality.

20|||

28|||

libs/prelude/Prelude/Algebra.idr+8−8

@@ -177,7 +177,7 @@ class MeetSemilattice a => VerifiedMeetSemilattice a where

177 total meetSemilatticeMeetIsIdempotent : (e : a) -> meet e e = e

178

179||| Sets equipped with a binary operation that is commutative, associative and

180−||| idempotent and supplied with a neutral element. Must satisfy the following

180+||| idempotent and supplied with a unitary element. Must satisfy the following

181||| laws:

182|||

183||| + Associativity of join:

@@ -186,8 +186,8 @@ class MeetSemilattice a => VerifiedMeetSemilattice a where

186||| forall a b, join a b == join b a

187||| + Idempotency of join:

188||| forall a, join a a == a

189−||| + Bottom:

189+||| + Bottom (Unitary Element):

190−||| forall a, join a bottom == bottom

190+||| forall a, join a bottom == a

191|||

192||| Join semilattices capture the notion of sets with a "least upper bound"

193||| equipped with a "bottom" element.

@@ -195,10 +195,10 @@ class JoinSemilattice a => BoundedJoinSemilattice a where

195 bottom : a

196

197class (VerifiedJoinSemilattice a, BoundedJoinSemilattice a) => VerifiedBoundedJoinSemilattice a where

198− total boundedJoinSemilatticeBottomIsBottom : (e : a) -> join e bottom = bottom

198+ total boundedJoinSemilatticeBottomIsBottom : (e : a) -> join e bottom = e

199

200||| Sets equipped with a binary operation that is commutative, associative and

201−||| idempotent and supplied with a neutral element. Must satisfy the following

201+||| idempotent and supplied with a unitary element. Must satisfy the following

202||| laws:

203|||

204||| + Associativity of meet:

@@ -207,8 +207,8 @@ class (VerifiedJoinSemilattice a, BoundedJoinSemilattice a) => VerifiedBoundedJo

207||| forall a b, meet a b == meet b a

208||| + Idempotency of meet:

209||| forall a, meet a a == a

210−||| + Top:

210+||| + Top (Unitary Element):

211−||| forall a, meet a top == top

211+||| forall a, meet a top == a

212|||

213||| Meet semilattices capture the notion of sets with a "greatest lower bound"

214||| equipped with a "top" element.

@@ -216,7 +216,7 @@ class MeetSemilattice a => BoundedMeetSemilattice a where

216 top : a

217

218class (VerifiedMeetSemilattice a, BoundedMeetSemilattice a) => VerifiedBoundedMeetSemilattice a where

219− total boundedMeetSemilatticeTopIsTop : (e : a) -> meet e top = top

219+ total boundedMeetSemilatticeTopIsTop : (e : a) -> meet e top = e

220

221||| Sets equipped with two binary operations that are both commutative,

222||| associative and idempotent, along with absorbtion laws for relating the two

libs/prelude/Prelude/Classes.idr+7

@@ -124,6 +124,13 @@ instance Ord String where

124 GT

125

126

127+instance Ord Bool where

128+ compare True True = EQ

129+ compare False False = EQ

130+ compare False True = LT

131+ compare True False = GT

132+

133+

127instance (Ord a, Ord b) => Ord (a, b) where

134instance (Ord a, Ord b) => Ord (a, b) where

128 compare (xl, xr) (yl, yr) =

135 compare (xl, xr) (yl, yr) =

129 if xl /= yl

136 if xl /= yl

libs/prelude/Prelude/Stream.idr+3−1

@@ -72,6 +72,7 @@ diag ((x::xs)::xss) = x :: diag (map tail xss)

72||| Fold a Stream corecursively. Since there is no Nil, no initial value is used.

73||| @ f the combining function

74||| @ xs the Stream to fold up

75+partial -- the recursive call isn't guarded!

75foldr : (f : a -> Inf b -> b) -> (xs : Stream a) -> b

76foldr : (f : a -> Inf b -> b) -> (xs : Stream a) -> b

76foldr f (x :: xs) = f x (foldr f xs)

77foldr f (x :: xs) = f x (foldr f xs)

77

78

@@ -86,8 +87,9 @@ scanl f acc (x :: xs) = acc :: scanl f (f acc x) xs

86||| @ f the combining function

87||| @ f the combining function

87||| @ xs the Stream to fold up

88||| @ xs the Stream to fold up

88-- Reusing the head of the corecursion in the obvious way doesn't productivity check

89-- Reusing the head of the corecursion in the obvious way doesn't productivity check

90+partial -- and the call to foldr isn't guarded anyway!

89scanr : (f : a -> Inf b -> b) -> (xs : Stream a) -> Stream b

91scanr : (f : a -> Inf b -> b) -> (xs : Stream a) -> Stream b

90−scanr f (x :: Delay xs) = f x (foldr f xs) :: scanr f xs

92+scanr f (x :: xs) = f x (foldr f xs) :: scanr f xs

91

93

92||| Produce a Stream repeating a sequence

94||| Produce a Stream repeating a sequence

93||| @ xs the sequence to repeat

95||| @ xs the sequence to repeat

llvm/Makefile+3−2

@@ -1,13 +1,14 @@

1include ../config.mk

2

3+PKG_CONFIG_CFLAGS:=$(shell (pkg-config --version >/dev/null 2>&1) && pkg-config --cflags bdw-gc)

3−CFLAGS:=-Wextra -fPIC -Wno-unused-parameter $(CFLAGS)

4+CFLAGS:=-Wextra -fPIC -Wno-unused-parameter $(PKG_CONFIG_CFLAGS) $(CFLAGS)

4SOURCES=defs.c

5SOURCES=defs.c

5OBJECTS=$(SOURCES:.c=.o)

6OBJECTS=$(SOURCES:.c=.o)

6LIB=libidris_rts.a

7LIB=libidris_rts.a

7

8

8build: $(SOURCES) $(LIB)

9build: $(SOURCES) $(LIB)

9

10

10−$(LIB): $(OBJECTS)

11+$(LIB): $(OBJECTS)

11 ar r $@ $(OBJECTS)

12 ar r $@ $(OBJECTS)

12 ranlib $@

13 ranlib $@

13

14

src/IRTS/CodegenJavaScript.hs+13−350

@@ -1,6 +1,9 @@

1{-# LANGUAGE PatternGuards #-}

2+{-# LANGUAGE OverloadedStrings #-}

2module IRTS.CodegenJavaScript (codegenJavaScript, codegenNode, JSTarget(..)) where

3module IRTS.CodegenJavaScript (codegenJavaScript, codegenNode, JSTarget(..)) where

3

4

5+import IRTS.JavaScript.AST

6+

4import Idris.AbsSyntax hiding (TypeCase)

7import Idris.AbsSyntax hiding (TypeCase)

5import IRTS.Bytecode

8import IRTS.Bytecode

6import IRTS.Lang

9import IRTS.Lang

@@ -25,6 +28,8 @@ import System.IO

25import System.Directory

28import System.Directory

26

29

27import qualified Data.Map.Strict as M

30import qualified Data.Map.Strict as M

31+import qualified Data.Text as T

32+import qualified Data.Text.IO as TIO

28

33

29

34

30data CompileInfo = CompileInfo { compileInfoApplyCases :: [Int]

35data CompileInfo = CompileInfo { compileInfoApplyCases :: [Int]

@@ -79,290 +84,6 @@ initCompileInfo bc =

79data JSTarget = Node | JavaScript deriving Eq

84data JSTarget = Node | JavaScript deriving Eq

80

85

81

86

82−data JSType = JSIntTy

83− | JSStringTy

84− | JSIntegerTy

85− | JSFloatTy

86− | JSCharTy

87− | JSPtrTy

88− | JSForgotTy

89− deriving Eq

90−

91−

92−data JSInteger = JSBigZero

93− | JSBigOne

94− | JSBigInt Integer

95− | JSBigIntExpr JS

96− deriving Eq

97−

98−

99−data JSNum = JSInt Int

100− | JSFloat Double

101− | JSInteger JSInteger

102− deriving Eq

103−

104−

105−data JSWord = JSWord8 Word8

106− | JSWord16 Word16

107− | JSWord32 Word32

108− | JSWord64 Word64

109− deriving Eq

110−

111−

112−data JSAnnotation = JSConstructor deriving Eq

113−

114−

115−instance Show JSAnnotation where

116− show JSConstructor = "constructor"

117−

118−

119−data JS = JSRaw String

120− | JSIdent String

121− | JSFunction [String] JS

122− | JSType JSType

123− | JSSeq [JS]

124− | JSReturn JS

125− | JSApp JS [JS]

126− | JSNew String [JS]

127− | JSError String

128− | JSBinOp String JS JS

129− | JSPreOp String JS

130− | JSPostOp String JS

131− | JSProj JS String

132− | JSNull

133− | JSUndefined

134− | JSThis

135− | JSTrue

136− | JSFalse

137− | JSArray [JS]

138− | JSString String

139− | JSNum JSNum

140− | JSWord JSWord

141− | JSAssign JS JS

142− | JSAlloc String (Maybe JS)

143− | JSIndex JS JS

144− | JSSwitch JS [(JS, JS)] (Maybe JS)

145− | JSCond [(JS, JS)]

146− | JSTernary JS JS JS

147− | JSParens JS

148− | JSWhile JS JS

149− | JSFFI String [JS]

150− | JSAnnotation JSAnnotation JS

151− | JSNoop

152− deriving Eq

153−

154−

155−data FFI = FFICode Char | FFIArg Int | FFIError String

156−

157−ffi :: String -> [String] -> String

158−ffi code args = let parsed = ffiParse code in

159− case ffiError parsed of

160− Just err -> error err

161− Nothing -> renderFFI parsed args

162− where

163− ffiParse :: String -> [FFI]

164− ffiParse "" = []

165− ffiParse ['%'] = [FFIError $ "FFI - Invalid positional argument"]

166− ffiParse ('%':'%':ss) = FFICode '%' : ffiParse ss

167− ffiParse ('%':s:ss)

168− | isDigit s =

169− FFIArg (read $ s : takeWhile isDigit ss) : ffiParse (dropWhile isDigit ss)

170− | otherwise =

171− [FFIError "FFI - Invalid positional argument"]

172− ffiParse (s:ss) = FFICode s : ffiParse ss

173−

174−

175− ffiError :: [FFI] -> Maybe String

176− ffiError [] = Nothing

177− ffiError ((FFIError s):xs) = Just s

178− ffiError (x:xs) = ffiError xs

179−

180−

181− renderFFI :: [FFI] -> [String] -> String

182− renderFFI [] _ = ""

183− renderFFI (FFICode c : fs) args = c : renderFFI fs args

184− renderFFI (FFIArg i : fs) args

185− | i < length args && i >= 0 = args !! i ++ renderFFI fs args

186− | otherwise = error "FFI - Argument index out of bounds"

187−

188−compileJS :: JS -> String

189−compileJS = compileJS' 0

190−

191−compileJS' :: Int -> JS -> String

192−compileJS' indent JSNoop = ""

193−

194−compileJS' indent (JSAnnotation annotation js) =

195− "/** @" ++ show annotation ++ " */\n" ++ compileJS' indent js

196−

197−compileJS' indent (JSFFI raw args) =

198− ffi raw (map (compileJS' indent) args)

199−

200−compileJS' indent (JSRaw code) =

201− code

202−

203−compileJS' indent (JSIdent ident) =

204− ident

205−

206−compileJS' indent (JSFunction args body) =

207− replicate indent ' ' ++ "function("

208− ++ intercalate "," args

209− ++ "){\n"

210− ++ compileJS' (indent + 2) body

211− ++ "\n}\n"

212−

213−compileJS' indent (JSType ty)

214− | JSIntTy <- ty = "i$Int"

215− | JSStringTy <- ty = "i$String"

216− | JSIntegerTy <- ty = "i$Integer"

217− | JSFloatTy <- ty = "i$Float"

218− | JSCharTy <- ty = "i$Char"

219− | JSPtrTy <- ty = "i$Ptr"

220− | JSForgotTy <- ty = "i$Forgot"

221−

222−compileJS' indent (JSSeq seq) =

223− intercalate ";\n" (

224− map (

225− (replicate indent ' ' ++) . (compileJS' indent)

226− ) $ filter (/= JSNoop) seq

227− ) ++ ";"

228−

229−compileJS' indent (JSReturn val) =

230− "return " ++ compileJS' indent val

231−

232−compileJS' indent (JSApp lhs rhs)

233− | JSFunction {} <- lhs =

234− concat ["(", compileJS' indent lhs, ")(", args, ")"]

235− | otherwise =

236− concat [compileJS' indent lhs, "(", args, ")"]

237− where args :: String

238− args = intercalate "," $ map (compileJS' 0) rhs

239−

240−compileJS' indent (JSNew name args) =

241− "new " ++ name ++ "(" ++ intercalate "," (map (compileJS' 0) args) ++ ")"

242−

243−compileJS' indent (JSError exc) =

244− "throw new Error(\"" ++ exc ++ "\")"

245−

246−compileJS' indent (JSBinOp op lhs rhs) =

247− compileJS' indent lhs ++ " " ++ op ++ " " ++ compileJS' indent rhs

248−

249−compileJS' indent (JSPreOp op val) =

250− op ++ compileJS' indent val

251−

252−compileJS' indent (JSProj obj field)

253− | JSFunction {} <- obj =

254− concat ["(", compileJS' indent obj, ").", field]

255− | JSAssign {} <- obj =

256− concat ["(", compileJS' indent obj, ").", field]

257− | otherwise =

258− compileJS' indent obj ++ '.' : field

259−

260−compileJS' indent JSNull =

261− "null"

262−

263−compileJS' indent JSUndefined =

264− "undefined"

265−

266−compileJS' indent JSThis =

267− "this"

268−

269−compileJS' indent JSTrue =

270− "true"

271−

272−compileJS' indent JSFalse =

273− "false"

274−

275−compileJS' indent (JSArray elems) =

276− "[" ++ intercalate "," (map (compileJS' 0) elems) ++ "]"

277−

278−compileJS' indent (JSString str) =

279− "\"" ++ str ++ "\""

280−

281−compileJS' indent (JSNum num)

282− | JSInt i <- num = show i

283− | JSFloat f <- num = show f

284− | JSInteger JSBigZero <- num = "i$ZERO"

285− | JSInteger JSBigOne <- num = "i$ONE"

286− | JSInteger (JSBigInt i) <- num = show i

287− | JSInteger (JSBigIntExpr e) <- num = "i$bigInt(" ++ compileJS' indent e ++ ")"

288−

289−compileJS' indent (JSAssign lhs rhs) =

290− compileJS' indent lhs ++ " = " ++ compileJS' indent rhs

291−

292−compileJS' 0 (JSAlloc name (Just val@(JSNew _ _))) =

293− "var " ++ name ++ " = " ++ compileJS' 0 val ++ ";\n"

294−

295−compileJS' indent (JSAlloc name val) =

296− "var " ++ name ++ maybe "" ((" = " ++) . compileJS' indent) val

297−

298−compileJS' indent (JSIndex lhs rhs) =

299− compileJS' indent lhs ++ "[" ++ compileJS' indent rhs ++ "]"

300−

301−compileJS' indent (JSCond branches) =

302− intercalate " else " $ map createIfBlock branches

303− where

304− createIfBlock (JSNoop, e@(JSSeq _)) =

305− "{\n"

306− ++ compileJS' (indent + 2) e

307− ++ "\n" ++ replicate indent ' ' ++ "}"

308− createIfBlock (JSNoop, e) =

309− "{\n"

310− ++ compileJS' (indent + 2) e

311− ++ ";\n" ++ replicate indent ' ' ++ "}"

312− createIfBlock (cond, e@(JSSeq _)) =

313− "if (" ++ compileJS' indent cond ++") {\n"

314− ++ compileJS' (indent + 2) e

315− ++ "\n" ++ replicate indent ' ' ++ "}"

316− createIfBlock (cond, e) =

317− "if (" ++ compileJS' indent cond ++") {\n"

318− ++ replicate (indent + 2) ' ' ++ compileJS' (indent + 2) e

319− ++ ";\n" ++ replicate indent ' ' ++ "}"

320−

321−compileJS' indent (JSSwitch val [(_,JSSeq seq)] Nothing) =

322− let (h,t) = splitAt 1 seq in

323− (concatMap (compileJS' indent) h ++ ";\n")

324− ++ (intercalate ";\n" $ map ((replicate indent ' ' ++) . compileJS' indent) t)

325−

326−compileJS' indent (JSSwitch val branches def) =

327− "switch(" ++ compileJS' indent val ++ "){\n"

328− ++ concatMap mkBranch branches

329− ++ mkDefault def

330− ++ replicate indent ' ' ++ "}"

331− where

332− mkBranch :: (JS, JS) -> String

333− mkBranch (tag, code) =

334− replicate (indent + 2) ' ' ++ "case " ++ compileJS' indent tag ++ ":\n"

335− ++ compileJS' (indent + 4) code

336− ++ "\n" ++ (replicate (indent + 4) ' ' ++ "break;\n")

337−

338− mkDefault :: Maybe JS -> String

339− mkDefault Nothing = ""

340− mkDefault (Just def) =

341− replicate (indent + 2) ' ' ++ "default:\n"

342− ++ compileJS' (indent + 4)def

343− ++ "\n"

344−

345−

346−compileJS' indent (JSTernary cond true false) =

347− let c = compileJS' indent cond

348− t = compileJS' indent true

349− f = compileJS' indent false in

350− "(" ++ c ++ ")?(" ++ t ++ "):(" ++ f ++ ")"

351−

352−compileJS' indent (JSParens js) =

353− "(" ++ compileJS' indent js ++ ")"

354−

355−compileJS' indent (JSWhile cond body) =

356− "while (" ++ compileJS' indent cond ++ ") {\n"

357− ++ compileJS' (indent + 2) body

358− ++ "\n" ++ replicate indent ' ' ++ "}"

359−

360−compileJS' indent (JSWord word)

361− | JSWord8 b <- word = "new Uint8Array([" ++ show b ++ "])"

362− | JSWord16 b <- word = "new Uint16Array([" ++ show b ++ "])"

363− | JSWord32 b <- word = "new Uint32Array([" ++ show b ++ "])"

364− | JSWord64 b <- word = "i$bigInt(\"" ++ show b ++ "\")"

365−

366codegenJavaScript :: CodeGenerator

87codegenJavaScript :: CodeGenerator

367codegenJavaScript ci =

88codegenJavaScript ci =

368 codegenJS_all JavaScript (simpleDecls ci)

89 codegenJS_all JavaScript (simpleDecls ci)

@@ -406,12 +127,12 @@ codegenJS_all target definitions includes libs filename outputType = do

406 ++ idrRuntime

127 ++ idrRuntime

407 ++ tgtRuntime

128 ++ tgtRuntime

408 )

129 )

409− writeFile filename ( runtime

130+ TIO.writeFile filename ( T.pack runtime

410− ++ concatMap compileJS opt

131+ `T.append` T.concat (map compileJS opt)

411− ++ concatMap compileJS cons

132+ `T.append` T.concat (map compileJS cons)

412− ++ main

133+ `T.append` main

413− ++ invokeMain

134+ `T.append` invokeMain

414− )

135+ )

415 setPermissions filename (emptyPermissions { readable = True

136 setPermissions filename (emptyPermissions { readable = True

416 , executable = target == Node

137 , executable = target == Node

417 , writable = True

138 , writable = True

@@ -478,7 +199,7 @@ codegenJS_all target definitions includes libs filename outputType = do

478 getIncludes :: [FilePath] -> IO [String]

199 getIncludes :: [FilePath] -> IO [String]

479 getIncludes = mapM readFile

200 getIncludes = mapM readFile

480

201

481− main :: String

202+ main :: T.Text

482 main =

203 main =

483 compileJS $ JSAlloc "main" (Just $

204 compileJS $ JSAlloc "main" (Just $

484 JSFunction [] (

205 JSFunction [] (

@@ -532,7 +253,7 @@ codegenJS_all target definitions includes libs filename outputType = do

532 )

253 )

533 ]

254 ]

534

255

535− invokeMain :: String

256+ invokeMain :: T.Text

536 invokeMain = compileJS $ JSApp (JSIdent "main") []

257 invokeMain = compileJS $ JSApp (JSIdent "main") []

537

258

538optimizeConstructors :: [JS] -> ([JS], [JS])

259optimizeConstructors :: [JS] -> ([JS], [JS])

@@ -890,64 +611,6 @@ jsMKCON info r t rs =

890 ]

611 ]

891 )

612 )

892

613

893−jsInstanceOf :: JS -> String -> JS

894−jsInstanceOf obj cls = JSBinOp "instanceof" obj (JSIdent cls)

895−

896−jsOr :: JS -> JS -> JS

897−jsOr lhs rhs = JSBinOp "||" lhs rhs

898−

899−jsAnd :: JS -> JS -> JS

900−jsAnd lhs rhs = JSBinOp "&&" lhs rhs

901−

902−jsMeth :: JS -> String -> [JS] -> JS

903−jsMeth obj meth args = JSApp (JSProj obj meth) args

904−

905−jsCall :: String -> [JS] -> JS

906−jsCall fun args = JSApp (JSIdent fun) args

907−

908−jsTypeOf :: JS -> JS

909−jsTypeOf js = JSPreOp "typeof " js

910−

911−jsEq :: JS -> JS -> JS

912−jsEq lhs@(JSNum (JSInteger _)) rhs = JSApp (JSProj lhs "equals") [rhs]

913−jsEq lhs rhs@(JSNum (JSInteger _)) = JSApp (JSProj lhs "equals") [rhs]

914−jsEq lhs rhs = JSBinOp "==" lhs rhs

915−

916−jsNotEq :: JS -> JS -> JS

917−jsNotEq lhs rhs = JSBinOp "!=" lhs rhs

918−

919−jsIsNumber :: JS -> JS

920−jsIsNumber js = (jsTypeOf js) `jsEq` (JSString "number")

921−

922−jsIsNull :: JS -> JS

923−jsIsNull js = JSBinOp "==" js JSNull

924−

925−jsBigInt :: JS -> JS

926−jsBigInt (JSString "0") = JSNum (JSInteger JSBigZero)

927−jsBigInt (JSString "1") = JSNum (JSInteger JSBigOne)

928−jsBigInt js = JSNum $ JSInteger $ JSBigIntExpr js

929−

930−jsUnPackBits :: JS -> JS

931−jsUnPackBits js = JSIndex js $ JSNum (JSInt 0)

932−

933−jsPackUBits8 :: JS -> JS

934−jsPackUBits8 js = JSNew "Uint8Array" [JSArray [js]]

935−

936−jsPackUBits16 :: JS -> JS

937−jsPackUBits16 js = JSNew "Uint16Array" [JSArray [js]]

938−

939−jsPackUBits32 :: JS -> JS

940−jsPackUBits32 js = JSNew "Uint32Array" [JSArray [js]]

941−

942−jsPackSBits8 :: JS -> JS

943−jsPackSBits8 js = JSNew "Int8Array" [JSArray [js]]

944−

945−jsPackSBits16 :: JS -> JS

946−jsPackSBits16 js = JSNew "Int16Array" [JSArray [js]]

947−

948−jsPackSBits32 :: JS -> JS

949−jsPackSBits32 js = JSNew "Int32Array" [JSArray [js]]

950−

951jsCASE :: CompileInfo -> Bool -> Reg -> [(Int, [BC])] -> Maybe [BC] -> JS

614jsCASE :: CompileInfo -> Bool -> Reg -> [(Int, [BC])] -> Maybe [BC] -> JS

952jsCASE info safe reg cases def =

615jsCASE info safe reg cases def =

953 JSSwitch (tag safe $ translateReg reg) (

616 JSSwitch (tag safe $ translateReg reg) (

src/IRTS/Compiler.hs+1−1

@@ -297,7 +297,7 @@ irTerm vs env tm@(App f a) = case unApply tm of

297 -- hence it takes a lambda: \unerased_argname_list -> resulting_LExp.

298 let padLams = padLambdas used (length args) arity

299

300− case compare arity (length args) of

300+ case compare (length args) arity of

301

302 -- overapplied

303 GT -> ifail ("overapplied data constructor: " ++ show tm)

src/IRTS/JavaScript/AST.hsnew file+397

@@ -0,0 +1,397 @@

1+{-# LANGUAGE PatternGuards #-}

2+{-# LANGUAGE OverloadedStrings #-}

3+module IRTS.JavaScript.AST where

4+

5+import Data.Word

6+import Data.Char (isDigit)

7+

8+import qualified Data.Text as T

9+

10+data JSType = JSIntTy

11+ | JSStringTy

12+ | JSIntegerTy

13+ | JSFloatTy

14+ | JSCharTy

15+ | JSPtrTy

16+ | JSForgotTy

17+ deriving Eq

18+

19+

20+data JSInteger = JSBigZero

21+ | JSBigOne

22+ | JSBigInt Integer

23+ | JSBigIntExpr JS

24+ deriving Eq

25+

26+

27+data JSNum = JSInt Int

28+ | JSFloat Double

29+ | JSInteger JSInteger

30+ deriving Eq

31+

32+

33+data JSWord = JSWord8 Word8

34+ | JSWord16 Word16

35+ | JSWord32 Word32

36+ | JSWord64 Word64

37+ deriving Eq

38+

39+

40+data JSAnnotation = JSConstructor deriving Eq

41+

42+

43+instance Show JSAnnotation where

44+ show JSConstructor = "constructor"

45+

46+

47+data JS = JSRaw String

48+ | JSIdent String

49+ | JSFunction [String] JS

50+ | JSType JSType

51+ | JSSeq [JS]

52+ | JSReturn JS

53+ | JSApp JS [JS]

54+ | JSNew String [JS]

55+ | JSError String

56+ | JSBinOp String JS JS

57+ | JSPreOp String JS

58+ | JSPostOp String JS

59+ | JSProj JS String

60+ | JSNull

61+ | JSUndefined

62+ | JSThis

63+ | JSTrue

64+ | JSFalse

65+ | JSArray [JS]

66+ | JSString String

67+ | JSNum JSNum

68+ | JSWord JSWord

69+ | JSAssign JS JS

70+ | JSAlloc String (Maybe JS)

71+ | JSIndex JS JS

72+ | JSSwitch JS [(JS, JS)] (Maybe JS)

73+ | JSCond [(JS, JS)]

74+ | JSTernary JS JS JS

75+ | JSParens JS

76+ | JSWhile JS JS

77+ | JSFFI String [JS]

78+ | JSAnnotation JSAnnotation JS

79+ | JSNoop

80+ deriving Eq

81+

82+

83+data FFI = FFICode Char | FFIArg Int | FFIError String

84+

85+ffi :: String -> [String] -> T.Text

86+ffi code args = let parsed = ffiParse code in

87+ case ffiError parsed of

88+ Just err -> error err

89+ Nothing -> renderFFI parsed args

90+ where

91+ ffiParse :: String -> [FFI]

92+ ffiParse "" = []

93+ ffiParse ['%'] = [FFIError $ "FFI - Invalid positional argument"]

94+ ffiParse ('%':'%':ss) = FFICode '%' : ffiParse ss

95+ ffiParse ('%':s:ss)

96+ | isDigit s =

97+ FFIArg (

98+ read $ s : takeWhile isDigit ss

99+ ) : ffiParse (dropWhile isDigit ss)

100+ | otherwise =

101+ [FFIError "FFI - Invalid positional argument"]

102+ ffiParse (s:ss) = FFICode s : ffiParse ss

103+

104+

105+ ffiError :: [FFI] -> Maybe String

106+ ffiError [] = Nothing

107+ ffiError ((FFIError s):xs) = Just s

108+ ffiError (x:xs) = ffiError xs

109+

110+

111+ renderFFI :: [FFI] -> [String] -> T.Text

112+ renderFFI [] _ = ""

113+ renderFFI (FFICode c : fs) args = c `T.cons` renderFFI fs args

114+ renderFFI (FFIArg i : fs) args

115+ | i < length args && i >= 0 =

116+ T.pack (args !! i)

117+ `T.append` renderFFI fs args

118+ | otherwise = error "FFI - Argument index out of bounds"

119+

120+compileJS :: JS -> T.Text

121+compileJS = compileJS' 0

122+

123+compileJS' :: Int -> JS -> T.Text

124+compileJS' indent JSNoop = ""

125+

126+compileJS' indent (JSAnnotation annotation js) =

127+ "/** @"

128+ `T.append` T.pack (show annotation)

129+ `T.append` " */\n"

130+ `T.append` compileJS' indent js

131+

132+compileJS' indent (JSFFI raw args) =

133+ ffi raw (map (T.unpack . compileJS' indent) args)

134+

135+compileJS' indent (JSRaw code) =

136+ T.pack code

137+

138+compileJS' indent (JSIdent ident) =

139+ T.pack ident

140+

141+compileJS' indent (JSFunction args body) =

142+ T.replicate indent " " `T.append` "function("

143+ `T.append` T.intercalate "," (map T.pack args)

144+ `T.append` "){\n"

145+ `T.append` compileJS' (indent + 2) body

146+ `T.append` "\n}\n"

147+

148+compileJS' indent (JSType ty)

149+ | JSIntTy <- ty = "i$Int"

150+ | JSStringTy <- ty = "i$String"

151+ | JSIntegerTy <- ty = "i$Integer"

152+ | JSFloatTy <- ty = "i$Float"

153+ | JSCharTy <- ty = "i$Char"

154+ | JSPtrTy <- ty = "i$Ptr"

155+ | JSForgotTy <- ty = "i$Forgot"

156+

157+compileJS' indent (JSSeq seq) =

158+ T.intercalate ";\n" (

159+ map (

160+ (T.replicate indent " " `T.append`) . (compileJS' indent)

161+ ) $ filter (/= JSNoop) seq

162+ ) `T.append` ";"

163+

164+compileJS' indent (JSReturn val) =

165+ "return " `T.append` compileJS' indent val

166+

167+compileJS' indent (JSApp lhs rhs)

168+ | JSFunction {} <- lhs =

169+ T.concat ["(", compileJS' indent lhs, ")(", args, ")"]

170+ | otherwise =

171+ T.concat [compileJS' indent lhs, "(", args, ")"]

172+ where args :: T.Text

173+ args = T.intercalate "," $ map (compileJS' 0) rhs

174+

175+compileJS' indent (JSNew name args) =

176+ "new "

177+ `T.append` T.pack name

178+ `T.append` "("

179+ `T.append` T.intercalate "," (map (compileJS' 0) args)

180+ `T.append` ")"

181+

182+compileJS' indent (JSError exc) =

183+ "(function(){throw new Error(\"" `T.append` T.pack exc `T.append` "\")})()"

184+

185+compileJS' indent (JSBinOp op lhs rhs) =

186+ compileJS' indent lhs

187+ `T.append` " "

188+ `T.append` T.pack op

189+ `T.append` " "

190+ `T.append` compileJS' indent rhs

191+

192+compileJS' indent (JSPreOp op val) =

193+ T.pack op `T.append` compileJS' indent val

194+

195+compileJS' indent (JSProj obj field)

196+ | JSFunction {} <- obj =

197+ T.concat ["(", compileJS' indent obj, ").", T.pack field]

198+ | JSAssign {} <- obj =

199+ T.concat ["(", compileJS' indent obj, ").", T.pack field]

200+ | otherwise =

201+ compileJS' indent obj `T.append` ('.' `T.cons` T.pack field)

202+

203+compileJS' indent JSNull =

204+ "null"

205+

206+compileJS' indent JSUndefined =

207+ "undefined"

208+

209+compileJS' indent JSThis =

210+ "this"

211+

212+compileJS' indent JSTrue =

213+ "true"

214+

215+compileJS' indent JSFalse =

216+ "false"

217+

218+compileJS' indent (JSArray elems) =

219+ "[" `T.append` T.intercalate "," (map (compileJS' 0) elems) `T.append` "]"

220+

221+compileJS' indent (JSString str) =

222+ "\"" `T.append` T.pack str `T.append` "\""

223+

224+compileJS' indent (JSNum num)

225+ | JSInt i <- num = T.pack (show i)

226+ | JSFloat f <- num = T.pack (show f)

227+ | JSInteger JSBigZero <- num = T.pack "i$ZERO"

228+ | JSInteger JSBigOne <- num = T.pack "i$ONE"

229+ | JSInteger (JSBigInt i) <- num = T.pack (show i)

230+ | JSInteger (JSBigIntExpr e) <- num =

231+ "i$bigInt(" `T.append` compileJS' indent e `T.append` ")"

232+

233+compileJS' indent (JSAssign lhs rhs) =

234+ compileJS' indent lhs `T.append` " = " `T.append` compileJS' indent rhs

235+

236+compileJS' 0 (JSAlloc name (Just val@(JSNew _ _))) =

237+ "var "

238+ `T.append` T.pack name

239+ `T.append` " = "

240+ `T.append` compileJS' 0 val

241+ `T.append` ";\n"

242+

243+compileJS' indent (JSAlloc name val) =

244+ "var "

245+ `T.append` T.pack name

246+ `T.append` maybe "" ((" = " `T.append`) . compileJS' indent) val

247+

248+compileJS' indent (JSIndex lhs rhs) =

249+ compileJS' indent lhs

250+ `T.append` "["

251+ `T.append` compileJS' indent rhs

252+ `T.append` "]"

253+

254+compileJS' indent (JSCond branches) =

255+ T.intercalate " else " $ map createIfBlock branches

256+ where

257+ createIfBlock (JSNoop, e@(JSSeq _)) =

258+ "{\n"

259+ `T.append` compileJS' (indent + 2) e

260+ `T.append` "\n" `T.append` T.replicate indent " " `T.append` "}"

261+ createIfBlock (JSNoop, e) =

262+ "{\n"

263+ `T.append` compileJS' (indent + 2) e

264+ `T.append` ";\n" `T.append` T.replicate indent " " `T.append` "}"

265+ createIfBlock (cond, e@(JSSeq _)) =

266+ "if (" `T.append` compileJS' indent cond `T.append`") {\n"

267+ `T.append` compileJS' (indent + 2) e

268+ `T.append` "\n" `T.append` T.replicate indent " " `T.append` "}"

269+ createIfBlock (cond, e) =

270+ "if (" `T.append` compileJS' indent cond `T.append`") {\n"

271+ `T.append` T.replicate (indent + 2) " "

272+ `T.append` compileJS' (indent + 2) e

273+ `T.append` ";\n"

274+ `T.append` T.replicate indent " "

275+ `T.append` "}"

276+

277+compileJS' indent (JSSwitch val [(_,JSSeq seq)] Nothing) =

278+ let (h,t) = splitAt 1 seq in

279+ (T.concat (map (compileJS' indent) h) `T.append` ";\n")

280+ `T.append` (

281+ T.intercalate ";\n" $ map (

282+ (T.replicate indent " " `T.append`) . compileJS' indent

283+ ) t

284+ )

285+

286+compileJS' indent (JSSwitch val branches def) =

287+ "switch(" `T.append` compileJS' indent val `T.append` "){\n"

288+ `T.append` T.concat (map mkBranch branches)

289+ `T.append` mkDefault def

290+ `T.append` T.replicate indent " " `T.append` "}"

291+ where

292+ mkBranch :: (JS, JS) -> T.Text

293+ mkBranch (tag, code) =

294+ T.replicate (indent + 2) " "

295+ `T.append` "case "

296+ `T.append` compileJS' indent tag

297+ `T.append` ":\n"

298+ `T.append` compileJS' (indent + 4) code

299+ `T.append` "\n"

300+ `T.append` (T.replicate (indent + 4) " " `T.append` "break;\n")

301+

302+ mkDefault :: Maybe JS -> T.Text

303+ mkDefault Nothing = ""

304+ mkDefault (Just def) =

305+ T.replicate (indent + 2) " " `T.append` "default:\n"

306+ `T.append` compileJS' (indent + 4)def

307+ `T.append` "\n"

308+

309+

310+compileJS' indent (JSTernary cond true false) =

311+ let c = compileJS' indent cond

312+ t = compileJS' indent true

313+ f = compileJS' indent false in

314+ "("

315+ `T.append` c

316+ `T.append` ")?("

317+ `T.append` t

318+ `T.append` "):("

319+ `T.append` f

320+ `T.append` ")"

321+

322+compileJS' indent (JSParens js) =

323+ "(" `T.append` compileJS' indent js `T.append` ")"

324+

325+compileJS' indent (JSWhile cond body) =

326+ "while (" `T.append` compileJS' indent cond `T.append` ") {\n"

327+ `T.append` compileJS' (indent + 2) body

328+ `T.append` "\n" `T.append` T.replicate indent " " `T.append` "}"

329+

330+compileJS' indent (JSWord word)

331+ | JSWord8 b <- word =

332+ "new Uint8Array([" `T.append` T.pack (show b) `T.append` "])"

333+ | JSWord16 b <- word =

334+ "new Uint16Array([" `T.append` T.pack (show b) `T.append` "])"

335+ | JSWord32 b <- word =

336+ "new Uint32Array([" `T.append` T.pack (show b) `T.append` "])"

337+ | JSWord64 b <- word =

338+ "i$bigInt(\"" `T.append` T.pack (show b) `T.append` "\")"

339+

340+jsInstanceOf :: JS -> String -> JS

341+jsInstanceOf obj cls = JSBinOp "instanceof" obj (JSIdent cls)

342+

343+jsOr :: JS -> JS -> JS

344+jsOr lhs rhs = JSBinOp "||" lhs rhs

345+

346+jsAnd :: JS -> JS -> JS

347+jsAnd lhs rhs = JSBinOp "&&" lhs rhs

348+

349+jsMeth :: JS -> String -> [JS] -> JS

350+jsMeth obj meth args = JSApp (JSProj obj meth) args

351+

352+jsCall :: String -> [JS] -> JS

353+jsCall fun args = JSApp (JSIdent fun) args

354+

355+jsTypeOf :: JS -> JS

356+jsTypeOf js = JSPreOp "typeof " js

357+

358+jsEq :: JS -> JS -> JS

359+jsEq lhs@(JSNum (JSInteger _)) rhs = JSApp (JSProj lhs "equals") [rhs]

360+jsEq lhs rhs@(JSNum (JSInteger _)) = JSApp (JSProj lhs "equals") [rhs]

361+jsEq lhs rhs = JSBinOp "==" lhs rhs

362+

363+jsNotEq :: JS -> JS -> JS

364+jsNotEq lhs rhs = JSBinOp "!=" lhs rhs

365+

366+jsIsNumber :: JS -> JS

367+jsIsNumber js = (jsTypeOf js) `jsEq` (JSString "number")

368+

369+jsIsNull :: JS -> JS

370+jsIsNull js = JSBinOp "==" js JSNull

371+

372+jsBigInt :: JS -> JS

373+jsBigInt (JSString "0") = JSNum (JSInteger JSBigZero)

374+jsBigInt (JSString "1") = JSNum (JSInteger JSBigOne)

375+jsBigInt js = JSNum $ JSInteger $ JSBigIntExpr js

376+

377+jsUnPackBits :: JS -> JS

378+jsUnPackBits js = JSIndex js $ JSNum (JSInt 0)

379+

380+jsPackUBits8 :: JS -> JS

381+jsPackUBits8 js = JSNew "Uint8Array" [JSArray [js]]

382+

383+jsPackUBits16 :: JS -> JS

384+jsPackUBits16 js = JSNew "Uint16Array" [JSArray [js]]

385+

386+jsPackUBits32 :: JS -> JS

387+jsPackUBits32 js = JSNew "Uint32Array" [JSArray [js]]

388+

389+jsPackSBits8 :: JS -> JS

390+jsPackSBits8 js = JSNew "Int8Array" [JSArray [js]]

391+

392+jsPackSBits16 :: JS -> JS

393+jsPackSBits16 js = JSNew "Int16Array" [JSArray [js]]

394+

395+jsPackSBits32 :: JS -> JS

396+jsPackSBits32 js = JSNew "Int32Array" [JSArray [js]]

397+

src/Idris/AbsSyntax.hs+21−16

@@ -482,7 +482,10 @@ addDeferred' nt ns

482 i <- getIState

483 putIState $ i { idris_metavars = map (\(n, (i, top, _, isTopLevel)) -> (n, (top, i, isTopLevel))) ns ++

484 idris_metavars i }

485+ where

486+ -- 'tidyNames' is to generate user accessible names in case they are

487+ -- needed in tactic scripts

485− where tidyNames used (Bind (MN i x) b sc)

488+ tidyNames used (Bind (MN i x) b sc)

486 = let n' = uniqueName (UN x) used in

489 = let n' = uniqueName (UN x) used in

487 Bind n' b $ tidyNames (n':used) sc

490 Bind n' b $ tidyNames (n':used) sc

488 tidyNames used (Bind n b sc)

491 tidyNames used (Bind n b sc)

@@ -853,7 +856,7 @@ expandParams dec ps ns infs tm = en tm

853 | n `elem` (map fst ps ++ ns) && t /= Placeholder

856 | n `elem` (map fst ps ++ ns) && t /= Placeholder

854 = let n' = mkShadow n in

857 = let n' = mkShadow n in

855 PDPair f p (PRef f' n') (en t) (en (shadow n n' r))

858 PDPair f p (PRef f' n') (en t) (en (shadow n n' r))

856− en (PEq f l r) = PEq f (en l) (en r)

859+ en (PEq f lt rt l r) = PEq f (en lt) (en rt) (en l) (en r)

857 en (PRewrite f l r g) = PRewrite f (en l) (en r) (fmap en g)

860 en (PRewrite f l r g) = PRewrite f (en l) (en r) (fmap en g)

858 en (PTyped l r) = PTyped (en l) (en r)

861 en (PTyped l r) = PTyped (en l) (en r)

859 en (PPair f p l r) = PPair f p (en l) (en r)

862 en (PPair f p l r) = PPair f p (en l) (en r)

@@ -1022,7 +1025,7 @@ getPriority i tm = 1 -- pri tm

1022 pri (PTrue _ _) = 0

1025 pri (PTrue _ _) = 0

1023 pri (PFalse _) = 0

1026 pri (PFalse _) = 0

1024 pri (PRefl _ _) = 1

1027 pri (PRefl _ _) = 1

1025− pri (PEq _ l r) = max 1 (max (pri l) (pri r))

1028+ pri (PEq _ _ _ l r) = max 1 (max (pri l) (pri r))

1026 pri (PRewrite _ l r _) = max 1 (max (pri l) (pri r))

1029 pri (PRewrite _ l r _) = max 1 (max (pri l) (pri r))

1027 pri (PApp _ f as) = max 1 (max (pri f) (foldr max 0 (map (pri.getTm) as)))

1030 pri (PApp _ f as) = max 1 (max (pri f) (foldr max 0 (map (pri.getTm) as)))

1028 pri (PAppBind _ f as) = max 1 (max (pri f) (foldr max 0 (map (pri.getTm) as)))

1031 pri (PAppBind _ f as) = max 1 (max (pri f) (foldr max 0 (map (pri.getTm) as)))

@@ -1096,8 +1099,6 @@ addUsingConstraints syn fc t

1096 let ns = namesIn [] ist t

1099 let ns = namesIn [] ist t

1097 let cs = getConstraints t -- check declared constraints

1100 let cs = getConstraints t -- check declared constraints

1098 let addconsts = uconsts \\ cs

1101 let addconsts = uconsts \\ cs

1099− -- if all names in the arguments of addconsts appear in ns,

1100− -- add the constraint implicitly

1101 return (doAdd addconsts ns t)

1102 return (doAdd addconsts ns t)

1102 where uconsts = filter uconst (using syn)

1103 where uconsts = filter uconst (using syn)

1103 uconst (UConstraint _ _) = True

1104 uconst (UConstraint _ _) = True

@@ -1191,7 +1192,8 @@ getUnboundImplicits i sc tm = []

1191-- argument position.

1192-- argument position.

1192

1193

1193-- This has become a right mess already. Better redo it some time...

1194-- This has become a right mess already. Better redo it some time...

1194−

1195+-- TODO: This is obsoleted by the new way of elaborating types, but there's still

1196+-- a couple of places which use it. Clean them up!

1195implicit :: ElabInfo -> SyntaxInfo -> Name -> PTerm -> Idris PTerm

1197implicit :: ElabInfo -> SyntaxInfo -> Name -> PTerm -> Idris PTerm

1196implicit info syn n ptm = implicit' info syn [] n ptm

1198implicit info syn n ptm = implicit' info syn [] n ptm

1197

1199

@@ -1288,7 +1290,7 @@ implicitise syn ignore ist tm = -- trace ("INCOMING " ++ showImp True tm) $

1288 put (PTacImplicit 10 l n scr Placeholder : decls,

1290 put (PTacImplicit 10 l n scr Placeholder : decls,

1289 nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))

1291 nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))

1290 imps True (n:env) sc

1292 imps True (n:env) sc

1291− imps top env (PEq _ l r)

1293+ imps top env (PEq _ _ _ l r)

1292 = do (decls, ns) <- get

1294 = do (decls, ns) <- get

1293 let isn = namesIn uvars ist l ++ namesIn uvars ist r

1295 let isn = namesIn uvars ist l ++ namesIn uvars ist r

1294 put (decls, nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))

1296 put (decls, nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))

@@ -1357,10 +1359,12 @@ addImpl' inpat env infns ist ptm

1357 | not (f `elem` map fst env) = handleErr $ aiFn inpat inpat qq ist fc f ds []

1359 | not (f `elem` map fst env) = handleErr $ aiFn inpat inpat qq ist fc f ds []

1358 ai qq env ds (PHidden (PRef fc f))

1360 ai qq env ds (PHidden (PRef fc f))

1359 | not (f `elem` map fst env) = handleErr $ aiFn inpat False qq ist fc f ds []

1361 | not (f `elem` map fst env) = handleErr $ aiFn inpat False qq ist fc f ds []

1360− ai qq env ds (PEq fc l r)

1362+ ai qq env ds (PEq fc lt rt l r)

1363+ = let lt' = ai qq env ds lt

1364+ rt' = ai qq env ds rt

1361− = let l' = ai qq env ds l

1365+ l' = ai qq env ds l

1362 r' = ai qq env ds r in

1366 r' = ai qq env ds r in

1363− PEq fc l' r'

1367+ PEq fc lt' rt' l' r'

1364 ai qq env ds (PRewrite fc l r g)

1368 ai qq env ds (PRewrite fc l r g)

1365 = let l' = ai qq env ds l

1369 = let l' = ai qq env ds l

1366 r' = ai qq env ds r

1370 r' = ai qq env ds r

@@ -1398,7 +1402,7 @@ addImpl' inpat env infns ist ptm

1398 ai qq env ds (PApp fc f as)

1402 ai qq env ds (PApp fc f as)

1399 = let f' = ai qq env ds f

1403 = let f' = ai qq env ds f

1400 as' = map (fmap (ai qq env ds)) as in

1404 as' = map (fmap (ai qq env ds)) as in

1401− mkPApp fc 1 f' as'

1405+ mkPApp fc 1 f' as'

1402 ai qq env ds (PCase fc c os)

1406 ai qq env ds (PCase fc c os)

1403 = let c' = ai qq env ds c in

1407 = let c' = ai qq env ds c in

1404 -- leave os alone, because they get lifted into a new pattern match

1408 -- leave os alone, because they get lifted into a new pattern match

@@ -1423,8 +1427,8 @@ addImpl' inpat env infns ist ptm

1423 sc' = ai qq ((n, Nothing):env) ds sc in

1427 sc' = ai qq ((n, Nothing):env) ds sc in

1424 PGoal fc r' n sc'

1428 PGoal fc r' n sc'

1425 ai qq env ds (PHidden tm) = PHidden (ai qq env ds tm)

1429 ai qq env ds (PHidden tm) = PHidden (ai qq env ds tm)

1426− ai qq env ds (PProof ts) = PProof (map (fmap (ai qq env ds)) ts)

1430+ -- Don't do PProof or PTactics since implicits get added when scope is

1427− ai qq env ds (PTactics ts) = PTactics (map (fmap (ai qq env ds)) ts)

1431+ -- properly known in ElabTerm.runTac

1428 ai qq env ds (PRefl fc tm) = PRefl fc (ai qq env ds tm)

1432 ai qq env ds (PRefl fc tm) = PRefl fc (ai qq env ds tm)

1429 ai qq env ds (PUnifyLog tm) = PUnifyLog (ai qq env ds tm)

1433 ai qq env ds (PUnifyLog tm) = PUnifyLog (ai qq env ds tm)

1430 ai qq env ds (PNoImplicits tm) = PNoImplicits (ai qq env ds tm)

1434 ai qq env ds (PNoImplicits tm) = PNoImplicits (ai qq env ds tm)

@@ -1698,7 +1702,8 @@ matchClause' names i x y = checkRpts $ match (fullApp x) (fullApp y) where

1698 | not names && (not (isConName n (tt_ctxt i) ||

1702 | not names && (not (isConName n (tt_ctxt i) ||

1699 isFnName n (tt_ctxt i)) || tm == Placeholder)

1703 isFnName n (tt_ctxt i)) || tm == Placeholder)

1700 = return [(n, tm)]

1704 = return [(n, tm)]

1701− match (PEq _ l r) (PEq _ l' r') = do ml <- match' l l'

1705+ match (PEq _ _ _ l r) (PEq _ _ _ l' r')

1706+ = do ml <- match' l l'

1702 mr <- match' r r'

1707 mr <- match' r r'

1703 return (ml ++ mr)

1708 return (ml ++ mr)

1704 match (PRewrite _ l r _) (PRewrite _ l' r' _)

1709 match (PRewrite _ l r _) (PRewrite _ l' r' _)

@@ -1789,7 +1794,7 @@ substMatchShadow n shs tm t = sm shs t where

1789 | otherwise = PPi p x (sm xs t) (sm (x : xs) sc)

1794 | otherwise = PPi p x (sm xs t) (sm (x : xs) sc)

1790 sm xs (PApp f x as) = fullApp $ PApp f (sm xs x) (map (fmap (sm xs)) as)

1795 sm xs (PApp f x as) = fullApp $ PApp f (sm xs x) (map (fmap (sm xs)) as)

1791 sm xs (PCase f x as) = PCase f (sm xs x) (map (pmap (sm xs)) as)

1796 sm xs (PCase f x as) = PCase f (sm xs x) (map (pmap (sm xs)) as)

1792− sm xs (PEq f x y) = PEq f (sm xs x) (sm xs y)

1797+ sm xs (PEq f xt yt x y) = PEq f (sm xs xt) (sm xs yt) (sm xs x) (sm xs y)

1793 sm xs (PRewrite f x y tm) = PRewrite f (sm xs x) (sm xs y)

1798 sm xs (PRewrite f x y tm) = PRewrite f (sm xs x) (sm xs y)

1794 (fmap (sm xs) tm)

1799 (fmap (sm xs) tm)

1795 sm xs (PTyped x y) = PTyped (sm xs x) (sm xs y)

1800 sm xs (PTyped x y) = PTyped (sm xs x) (sm xs y)

@@ -1813,7 +1818,7 @@ shadow n n' t = sm t where

1813 sm (PApp f x as) = PApp f (sm x) (map (fmap sm) as)

1818 sm (PApp f x as) = PApp f (sm x) (map (fmap sm) as)

1814 sm (PAppBind f x as) = PAppBind f (sm x) (map (fmap sm) as)

1819 sm (PAppBind f x as) = PAppBind f (sm x) (map (fmap sm) as)

1815 sm (PCase f x as) = PCase f (sm x) (map (pmap sm) as)

1820 sm (PCase f x as) = PCase f (sm x) (map (pmap sm) as)

1816− sm (PEq f x y) = PEq f (sm x) (sm y)

1821+ sm (PEq f xt yt x y) = PEq f (sm xt) (sm yt) (sm x) (sm y)

1817 sm (PRewrite f x y tm) = PRewrite f (sm x) (sm y) (fmap sm tm)

1822 sm (PRewrite f x y tm) = PRewrite f (sm x) (sm y) (fmap sm tm)

1818 sm (PTyped x y) = PTyped (sm x) (sm y)

1823 sm (PTyped x y) = PTyped (sm x) (sm y)

1819 sm (PPair f p x y) = PPair f p (sm x) (sm y)

1824 sm (PPair f p x y) = PPair f p (sm x) (sm y)

src/Idris/AbsSyntaxTree.hs+25−21

@@ -681,7 +681,7 @@ data PTerm = PQuote Raw

681 | PFalse FC -- ^ _|_

682 | PRefl FC PTerm

683 | PResolveTC FC

684− | PEq FC PTerm PTerm -- ^ Equality type: A = B

684+ | PEq FC PTerm PTerm PTerm PTerm -- ^ Heterogeneous equality type: A = B

685 | PRewrite FC PTerm PTerm (Maybe PTerm)

686 | PPair FC PunInfo PTerm PTerm

687 | PDPair FC PunInfo PTerm PTerm PTerm

@@ -723,7 +723,7 @@ mapPT f t = f (mpt t) where

723 mpt (PApp fc t as) = PApp fc (mapPT f t) (map (fmap (mapPT f)) as)

724 mpt (PAppBind fc t as) = PAppBind fc (mapPT f t) (map (fmap (mapPT f)) as)

725 mpt (PCase fc c os) = PCase fc (mapPT f c) (map (pmap (mapPT f)) os)

726− mpt (PEq fc l r) = PEq fc (mapPT f l) (mapPT f r)

726+ mpt (PEq fc lt rt l r) = PEq fc (mapPT f lt) (mapPT f rt) (mapPT f l) (mapPT f r)

727 mpt (PTyped l r) = PTyped (mapPT f l) (mapPT f r)

728 mpt (PPair fc p l r) = PPair fc p (mapPT f l) (mapPT f r)

729 mpt (PDPair fc p l t r) = PDPair fc p (mapPT f l) (mapPT f t) (mapPT f r)

@@ -761,6 +761,8 @@ data PTactic' t = Intro [Name] | Intros | Focus Name

761 | GoalType String (PTactic' t)

762 | TCheck t

763 | TEval t

764+ | TDocStr (Either Name Const)

765+ | TSearch t

764 | Qed | Abandon

766 | Qed | Abandon

765 deriving (Show, Eq, Functor)

767 deriving (Show, Eq, Functor)

766{-!

768{-!

@@ -1086,7 +1088,7 @@ eqDecl = PDatadecl eqTy (piBindp impl [(n "A", PType), (n "B", PType)]

1086 pimp (n "B") Placeholder False,

1088 pimp (n "B") Placeholder False,

1087 pexp (PRef bi (n "x")),

1089 pexp (PRef bi (n "x")),

1088 pexp (PRef bi (n "x"))])), bi, [])]

1090 pexp (PRef bi (n "x"))])), bi, [])]

1089− where n a = sMN 0 a

1091+ where n a = sUN a

1090 reflDoc = parseDocstring . T.pack $

1092 reflDoc = parseDocstring . T.pack $

1091 "A proof that `x` in fact equals `x`. To construct this, you must have already " ++

1093 "A proof that `x` in fact equals `x`. To construct this, you must have already " ++

1092 "shown that both sides are in fact equal."

1094 "shown that both sides are in fact equal."

@@ -1096,7 +1098,7 @@ eqDecl = PDatadecl eqTy (piBindp impl [(n "A", PType), (n "B", PType)]

1096eqParamDoc = [(n "A", parseDocstring . T.pack $ "the type of the left side of the equality"),

1098eqParamDoc = [(n "A", parseDocstring . T.pack $ "the type of the left side of the equality"),

1097 (n "B", parseDocstring . T.pack $ "the type of the right side of the equality")

1099 (n "B", parseDocstring . T.pack $ "the type of the right side of the equality")

1098 ]

1100 ]

1099− where n a = sMN 0 a

1101+ where n a = sUN a

1100

1102

1101eqOpts = []

1103eqOpts = []

1102

1104

@@ -1128,7 +1130,7 @@ instance Show PTerm where

1128 showsPrec _ tm = (displayS . renderPretty 1.0 10000000 . prettyImp defaultPPOption) tm

1130 showsPrec _ tm = (displayS . renderPretty 1.0 10000000 . prettyImp defaultPPOption) tm

1129

1131

1130instance Show PDecl where

1132instance Show PDecl where

1131− showsPrec _ d = (displayS . renderPretty 1.0 10000000 . showDeclImp defaultPPOption) d

1133+ showsPrec _ d = (displayS . renderPretty 1.0 10000000 . showDeclImp verbosePPOption) d

1132

1134

1133instance Show PClause where

1135instance Show PClause where

1134 showsPrec _ c = (displayS . renderPretty 1.0 10000000 . showCImp verbosePPOption) c

1136 showsPrec _ c = (displayS . renderPretty 1.0 10000000 . showCImp verbosePPOption) c

@@ -1242,7 +1244,7 @@ pprintPTerm ppo bnd docArgs infixes = prettySe 10 bnd

1242 rbrace <+> text "->" </> prettySe 10 ((n, True):bnd) sc

1244 rbrace <+> text "->" </> prettySe 10 ((n, True):bnd) sc

1243 prettySe p bnd (PApp _ (PRef _ f) args) -- normal names, no explicit args

1245 prettySe p bnd (PApp _ (PRef _ f) args) -- normal names, no explicit args

1244 | UN nm <- basename f

1246 | UN nm <- basename f

1245− , not (ppopt_impl ppo) && null (getExps args) =

1247+ , not (ppopt_impl ppo) && null (getShowArgs args) =

1246 prettyName True (ppopt_impl ppo) bnd f

1248 prettyName True (ppopt_impl ppo) bnd f

1247 prettySe p bnd (PAppBind _ (PRef _ f) [])

1249 prettySe p bnd (PAppBind _ (PRef _ f) [])

1248 | not (ppopt_impl ppo) = text "!" <> prettyName True (ppopt_impl ppo) bnd f

1250 | not (ppopt_impl ppo) = text "!" <> prettyName True (ppopt_impl ppo) bnd f

@@ -1250,14 +1252,16 @@ pprintPTerm ppo bnd docArgs infixes = prettySe 10 bnd

1250 | UN nm <- basename op

1252 | UN nm <- basename op

1251 , not (tnull nm) &&

1253 , not (tnull nm) &&

1252 (not (ppopt_impl ppo)) && (not $ isAlpha (thead nm)) =

1254 (not (ppopt_impl ppo)) && (not $ isAlpha (thead nm)) =

1253− case getExps args of

1255+ case getShowArgs args of

1254 [] -> opName True

1256 [] -> opName True

1255− [x] -> group (opName True <$> group (prettySe 0 bnd x))

1257+ [x] -> group (opName True <$> group (prettySe 0 bnd (getTm x)))

1256 [l,r] -> let precedence = fromMaybe 20 (fmap prec f)

1258 [l,r] -> let precedence = fromMaybe 20 (fmap prec f)

1257− in bracket p precedence $ inFix l r

1259+ in bracket p precedence $ inFix (getTm l) (getTm r)

1260+ (l@(PExp _ _ _ _) : r@(PExp _ _ _ _) : rest) ->

1258− (l:r:rest) -> bracket p 1 $

1261+ bracket p 1 $

1259− enclose lparen rparen (inFix l r) <+>

1262+ enclose lparen rparen (inFix (getTm l) (getTm r)) <+>

1260− align (group (vsep (map (prettyArgSe bnd) rest)))

1263+ align (group (vsep (map (prettyArgS bnd) rest)))

1264+ as -> opName True <+> align (vsep (map (prettyArgS bnd) as))

1261 where opName isPrefix = prettyName isPrefix (ppopt_impl ppo) bnd op

1265 where opName isPrefix = prettyName isPrefix (ppopt_impl ppo) bnd op

1262 f = getFixity (opStr op)

1266 f = getFixity (opStr op)

1263 left l = case f of

1267 left l = case f of

@@ -1299,7 +1303,7 @@ pprintPTerm ppo bnd docArgs infixes = prettySe 10 bnd

1299 prettySe p bnd (PTrue _ IsTerm) = annName unitCon $ text "()"

1303 prettySe p bnd (PTrue _ IsTerm) = annName unitCon $ text "()"

1300 prettySe p bnd (PTrue _ TypeOrTerm) = text "()"

1304 prettySe p bnd (PTrue _ TypeOrTerm) = text "()"

1301 prettySe p bnd (PFalse _) = annName falseTy $ text "_|_"

1305 prettySe p bnd (PFalse _) = annName falseTy $ text "_|_"

1302− prettySe p bnd (PEq _ l r) =

1306+ prettySe p bnd (PEq _ _ _ l r) =

1303 bracket p 2 . align . group $

1307 bracket p 2 . align . group $

1304 prettySe 10 bnd l <+> eq <$> group (prettySe 10 bnd r)

1308 prettySe 10 bnd l <+> eq <$> group (prettySe 10 bnd r)

1305 where eq = annName eqTy (text "=")

1309 where eq = annName eqTy (text "=")

@@ -1462,7 +1466,7 @@ prettyName infixParen showNS bnd n

1462 where fullName = text nameSpace <> parenthesise (text (baseName n))

1466 where fullName = text nameSpace <> parenthesise (text (baseName n))

1463 baseName (UN n) = T.unpack n

1467 baseName (UN n) = T.unpack n

1464 baseName (NS n ns) = baseName n

1468 baseName (NS n ns) = baseName n

1465− baseName (MN i s) = T.unpack s

1469+ baseName (MN i s) = T.unpack s

1466 baseName n | n == falseTy = "_|_"

1470 baseName n | n == falseTy = "_|_"

1467 baseName other = show other

1471 baseName other = show other

1468 nameSpace = case n of

1472 nameSpace = case n of

@@ -1552,7 +1556,7 @@ showName ist bnd ppo colour n = case ist of

1552 Nothing -> showbasic n

1556 Nothing -> showbasic n

1553 where name = if ppopt_impl ppo then show n else showbasic n

1557 where name = if ppopt_impl ppo then show n else showbasic n

1554 showbasic n@(UN _) = showCG n

1558 showbasic n@(UN _) = showCG n

1555− showbasic (MN _ s) = str s

1559+ showbasic (MN i s) = str s

1556 showbasic (NS n s) = showSep "." (map str (reverse s)) ++ "." ++ showbasic n

1560 showbasic (NS n s) = showSep "." (map str (reverse s)) ++ "." ++ showbasic n

1557 showbasic (SN s) = show s

1561 showbasic (SN s) = show s

1558 fst3 (x, _, _) = x

1562 fst3 (x, _, _) = x

@@ -1596,7 +1600,7 @@ instance Sized PTerm where

1596 size (PFalse fc) = 1

1600 size (PFalse fc) = 1

1597 size (PRefl fc _) = 1

1601 size (PRefl fc _) = 1

1598 size (PResolveTC fc) = 1

1602 size (PResolveTC fc) = 1

1599− size (PEq fc left right) = 1 + size left + size right

1603+ size (PEq fc _ _ left right) = 1 + size left + size right

1600 size (PRewrite fc left right _) = 1 + size left + size right

1604 size (PRewrite fc left right _) = 1 + size left + size right

1601 size (PPair fc _ left right) = 1 + size left + size right

1605 size (PPair fc _ left right) = 1 + size left + size right

1602 size (PDPair fs _ left ty right) = 1 + size left + size ty + size right

1606 size (PDPair fs _ left ty right) = 1 + size left + size ty + size right

@@ -1634,7 +1638,7 @@ allNamesIn tm = nub $ ni [] tm

1634 ni env (PLam n ty sc) = ni env ty ++ ni (n:env) sc

1638 ni env (PLam n ty sc) = ni env ty ++ ni (n:env) sc

1635 ni env (PPi p n ty sc) = niTacImp env p ++ ni env ty ++ ni (n:env) sc

1639 ni env (PPi p n ty sc) = niTacImp env p ++ ni env ty ++ ni (n:env) sc

1636 ni env (PHidden tm) = ni env tm

1640 ni env (PHidden tm) = ni env tm

1637− ni env (PEq _ l r) = ni env l ++ ni env r

1641+ ni env (PEq _ _ _ l r) = ni env l ++ ni env r

1638 ni env (PRewrite _ l r _) = ni env l ++ ni env r

1642 ni env (PRewrite _ l r _) = ni env l ++ ni env r

1639 ni env (PTyped l r) = ni env l ++ ni env r

1643 ni env (PTyped l r) = ni env l ++ ni env r

1640 ni env (PPair _ _ l r) = ni env l ++ ni env r

1644 ni env (PPair _ _ l r) = ni env l ++ ni env r

@@ -1659,7 +1663,7 @@ boundNamesIn tm = nub $ ni tm

1659 ni (PLam n ty sc) = n : (ni ty ++ ni sc)

1663 ni (PLam n ty sc) = n : (ni ty ++ ni sc)

1660 ni (PLet n ty val sc) = n : (ni ty ++ ni val ++ ni sc)

1664 ni (PLet n ty val sc) = n : (ni ty ++ ni val ++ ni sc)

1661 ni (PPi p n ty sc) = niTacImp p ++ (n : (ni ty ++ ni sc))

1665 ni (PPi p n ty sc) = niTacImp p ++ (n : (ni ty ++ ni sc))

1662− ni (PEq _ l r) = ni l ++ ni r

1666+ ni (PEq _ _ _ l r) = ni l ++ ni r

1663 ni (PRewrite _ l r _) = ni l ++ ni r

1667 ni (PRewrite _ l r _) = ni l ++ ni r

1664 ni (PTyped l r) = ni l ++ ni r

1668 ni (PTyped l r) = ni l ++ ni r

1665 ni (PPair _ _ l r) = ni l ++ ni r

1669 ni (PPair _ _ l r) = ni l ++ ni r

@@ -1695,7 +1699,7 @@ implicitNamesIn uvars ist tm = nub $ ni [] tm

1695 \\ nub (concatMap (ni env) (map fst os)))

1699 \\ nub (concatMap (ni env) (map fst os)))

1696 ni env (PLam n ty sc) = ni env ty ++ ni (n:env) sc

1700 ni env (PLam n ty sc) = ni env ty ++ ni (n:env) sc

1697 ni env (PPi p n ty sc) = niTacImp env p ++ ni env ty ++ ni (n:env) sc

1701 ni env (PPi p n ty sc) = niTacImp env p ++ ni env ty ++ ni (n:env) sc

1698− ni env (PEq _ l r) = ni env l ++ ni env r

1702+ ni env (PEq _ _ _ l r) = ni env l ++ ni env r

1699 ni env (PRewrite _ l r _) = ni env l ++ ni env r

1703 ni env (PRewrite _ l r _) = ni env l ++ ni env r

1700 ni env (PTyped l r) = ni env l ++ ni env r

1704 ni env (PTyped l r) = ni env l ++ ni env r

1701 ni env (PPair _ _ l r) = ni env l ++ ni env r

1705 ni env (PPair _ _ l r) = ni env l ++ ni env r

@@ -1728,7 +1732,7 @@ namesIn uvars ist tm = nub $ ni [] tm

1728 \\ nub (concatMap (ni env) (map fst os)))

1732 \\ nub (concatMap (ni env) (map fst os)))

1729 ni env (PLam n ty sc) = ni env ty ++ ni (n:env) sc

1733 ni env (PLam n ty sc) = ni env ty ++ ni (n:env) sc

1730 ni env (PPi p n ty sc) = niTacImp env p ++ ni env ty ++ ni (n:env) sc

1734 ni env (PPi p n ty sc) = niTacImp env p ++ ni env ty ++ ni (n:env) sc

1731− ni env (PEq _ l r) = ni env l ++ ni env r

1735+ ni env (PEq _ _ _ l r) = ni env l ++ ni env r

1732 ni env (PRewrite _ l r _) = ni env l ++ ni env r

1736 ni env (PRewrite _ l r _) = ni env l ++ ni env r

1733 ni env (PTyped l r) = ni env l ++ ni env r

1737 ni env (PTyped l r) = ni env l ++ ni env r

1734 ni env (PPair _ _ l r) = ni env l ++ ni env r

1738 ni env (PPair _ _ l r) = ni env l ++ ni env r

@@ -1759,7 +1763,7 @@ usedNamesIn vars ist tm = nub $ ni [] tm

1759 ni env (PCase _ c os) = ni env c ++ concatMap (ni env) (map snd os)

1763 ni env (PCase _ c os) = ni env c ++ concatMap (ni env) (map snd os)

1760 ni env (PLam n ty sc) = ni env ty ++ ni (n:env) sc

1764 ni env (PLam n ty sc) = ni env ty ++ ni (n:env) sc

1761 ni env (PPi p n ty sc) = niTacImp env p ++ ni env ty ++ ni (n:env) sc

1765 ni env (PPi p n ty sc) = niTacImp env p ++ ni env ty ++ ni (n:env) sc

1762− ni env (PEq _ l r) = ni env l ++ ni env r

1766+ ni env (PEq _ _ _ l r) = ni env l ++ ni env r

1763 ni env (PRewrite _ l r _) = ni env l ++ ni env r

1767 ni env (PRewrite _ l r _) = ni env l ++ ni env r

1764 ni env (PTyped l r) = ni env l ++ ni env r

1768 ni env (PTyped l r) = ni env l ++ ni env r

1765 ni env (PPair _ _ l r) = ni env l ++ ni env r

1769 ni env (PPair _ _ l r) = ni env l ++ ni env r

src/Idris/CaseSplit.hs+3−3

@@ -231,7 +231,7 @@ replaceVar ctxt n t (PApp fc f pats) = PApp fc f (map substArg pats)

231 subst (PApp fc (PRef _ t) pats)

232 | isTConName t ctxt = Placeholder -- infer types

233 subst (PApp fc f pats) = PApp fc f (map substArg pats)

234− subst (PEq fc l r) = Placeholder -- PEq fc (subst l) (subst r)

234+ subst (PEq fc _ _ l r) = Placeholder -- PEq fc (subst l) (subst r)

235 subst x = x

236

237 substArg arg = arg { getTm = subst (getTm arg) }

@@ -276,7 +276,7 @@ replaceSplits l ups = updateRHSs 1 (map (rep (expandBraces l)) ups)

276 -- this isn't supported in a pattern, so special case here

277 nshow (PRef _ (UN z)) | z == txt "Z" = "Z"

278 nshow (PApp _ (PRef _ (UN s)) [x]) | s == txt "S" =

279− "S " ++ addBrackets (nshow (getTm x))

279+ "(S " ++ addBrackets (nshow (getTm x)) ++ ")"

280 nshow t = show t

281

282 -- if there's any {n} replace with {n=n}

@@ -349,7 +349,7 @@ getClause l fn fp

349 getNameFrom i used (PPi _ _ _ _)

350 = uniqueNameFrom (mkSupply [sUN "f", sUN "g"]) used

351 getNameFrom i used (PApp fc f as) = getNameFrom i used f

352− getNameFrom i used (PEq _ _ _) = uniqueNameFrom [sUN "prf"] used

352+ getNameFrom i used (PEq _ _ _ _ _) = uniqueNameFrom [sUN "prf"] used

353 getNameFrom i used (PRef fc f)

354 = case getNameHints i f of

355 [] -> uniqueName (sUN "x") used

src/Idris/Core/Elaborate.hs+4−2

@@ -514,8 +514,10 @@ apply' fillt fn imps =

514 put (ES (p { dontunify = dont, unified = (n, unify),

515 notunified = notunify ++ notunified p }, a) s prev)

516 fillt (raw_apply fn (map (Var . snd) args))

517−-- trace ("Goal " ++ show g ++ "\n" ++ show (fn, imps, unify) ++ "\n" ++ show ptm) $

517+ ulog <- getUnifyLog

518+ g <- goal

519+ traceWhen ulog ("Goal " ++ show g ++ " -- when elaborating " ++ show fn) $

518− end_unify

520+ end_unify

519 return $! (map (\(argName, argHole) -> (argName, updateUnify unify argHole)) args)

521 return $! (map (\(argName, argHole) -> (argName, updateUnify unify argHole)) args)

520 where updateUnify us n = case lookup n us of

522 where updateUnify us n = case lookup n us of

521 Just (P _ t _) -> t

523 Just (P _ t _) -> t

src/Idris/Core/ProofState.hs+14−8

@@ -213,7 +213,8 @@ unify' ctxt env topx topy =

213 "\nHoles: " ++ show (holes ps)

214 ++ "\nInjective: " ++ show (injective ps)

215 ++ "\n") $

216− lift $ unify ctxt env topx topy inj (holes ps) while

216+ lift $ unify ctxt env topx topy inj (holes ps)

217+ (map fst (notunified ps)) while

217 let notu = filter (\ (n, t) -> case t of

218 let notu = filter (\ (n, t) -> case t of

218 P _ _ _ -> False

219 P _ _ _ -> False

219 _ -> n `elem` dont) u

220 _ -> n `elem` dont) u

@@ -233,6 +234,7 @@ unify' ctxt env topx topy =

233 (fails ++ problems ps)

234 (fails ++ problems ps)

234 (injective ps)

235 (injective ps)

235 (holes ps)

236 (holes ps)

237+ (map fst (notunified ps))

236 let (notu', probs_notu) = mergeNotunified env (notu ++ notunified ps)

238 let (notu', probs_notu) = mergeNotunified env (notu ++ notunified ps)

237 traceWhen (unifylog ps)

239 traceWhen (unifylog ps)

238 ("Now solved: " ++ show ns' ++

240 ("Now solved: " ++ show ns' ++

@@ -558,7 +560,7 @@ solve _ _ h@(Bind x t sc)

558 = do ps <- get

560 = do ps <- get

559 case findType x sc of

561 case findType x sc of

560 Just t -> lift $ tfail (CantInferType (show t))

562 Just t -> lift $ tfail (CantInferType (show t))

561− _ -> fail $ "Not a guess " ++ show h ++ "\n" ++ show (holes ps, pterm ps)

563+ _ -> lift $ tfail (IncompleteTerm h)

562 where findType x (Bind n (Let t v) sc)

564 where findType x (Bind n (Let t v) sc)

563 = findType x v `mplus` findType x sc

565 = findType x v `mplus` findType x sc

564 findType x (Bind n t sc)

566 findType x (Bind n t sc)

@@ -859,8 +861,8 @@ mergeNotunified env ns = mnu ns [] [] where

859 mnu [] ns_acc ps_acc = (reverse ns_acc, reverse ps_acc)

861 mnu [] ns_acc ps_acc = (reverse ns_acc, reverse ps_acc)

860 mnu ((n, t):ns) ns_acc ps_acc

862 mnu ((n, t):ns) ns_acc ps_acc

861 | Just t' <- lookup n ns, t /= t'

863 | Just t' <- lookup n ns, t /= t'

862− = mnu ns ((n,t') : ns_acc)

864+ = mnu ns ((n,t') : ns_acc)

863− ((t,t',env,Msg "", [],Unify) : ps_acc)

865+ ((t,t',env,CantUnify True t t' (Msg "") [] 0, [],Match) : ps_acc)

864 | otherwise = mnu ns ((n,t) : ns_acc) ps_acc

866 | otherwise = mnu ns ((n,t) : ns_acc) ps_acc

865

867

866updateNotunified [] nu = nu

868updateNotunified [] nu = nu

@@ -869,10 +871,11 @@ updateNotunified ns nu = up nu where

869 up ((n, t) : nus) = let t' = updateSolved ns t in

871 up ((n, t) : nus) = let t' = updateSolved ns t in

870 ((n, t') : up nus)

872 ((n, t') : up nus)

871

873

874+-- FIXME: Why not just pass the whole proof state?

872−updateProblems :: Context -> [(Name, TT Name)] -> Fails -> [Name] -> [Name]

875+updateProblems :: Context -> [(Name, TT Name)] -> Fails -> [Name] -> [Name] -> [Name]

873 -> ([(Name, TT Name)], Fails)

876 -> ([(Name, TT Name)], Fails)

874−updateProblems ctxt [] ps inj holes = ([], ps)

877+-- updateProblems ctxt [] ps inj holes = ([], ps)

875−updateProblems ctxt ns ps inj holes = up ns ps where

878+updateProblems ctxt ns ps inj holes usupp = up ns ps where

876 up ns [] = (ns, [])

879 up ns [] = (ns, [])

877 up ns ((x, y, env, err, while, um) : ps) =

880 up ns ((x, y, env, err, while, um) : ps) =

878 let x' = updateSolved ns x

881 let x' = updateSolved ns x

@@ -880,7 +883,7 @@ updateProblems ctxt ns ps inj holes = up ns ps where

880 err' = updateError ns err

883 err' = updateError ns err

881 env' = updateEnv ns env in

884 env' = updateEnv ns env in

882-- trace ("Updating " ++ show (x',y')) $

885-- trace ("Updating " ++ show (x',y')) $

883− case unify ctxt env' x' y' inj holes while of

886+ case unify ctxt env' x' y' inj holes usupp while of

884 OK (v, []) -> -- trace ("Added " ++ show v ++ " from " ++ show (x', y')) $

887 OK (v, []) -> -- trace ("Added " ++ show v ++ " from " ++ show (x', y')) $

885 up (ns ++ v) ps

888 up (ns ++ v) ps

886 e -> -- trace ("Failed " ++ show e) $

889 e -> -- trace ("Failed " ++ show e) $

@@ -921,6 +924,7 @@ processTactic EndUnify ps

921 ns' = map (\ (n, t) -> (n, updateSolved ns t)) ns

924 ns' = map (\ (n, t) -> (n, updateSolved ns t)) ns

922 (ns'', probs') = updateProblems (context ps) ns' (problems ps)

925 (ns'', probs') = updateProblems (context ps) ns' (problems ps)

923 (injective ps) (holes ps)

926 (injective ps) (holes ps)

927+ (map fst (notunified ps))

924 tm' = updateSolved ns'' (pterm ps) in

928 tm' = updateSolved ns'' (pterm ps) in

925 traceWhen (unifylog ps) ("Dropping holes: " ++ show (map fst ns'')) $

929 traceWhen (unifylog ps) ("Dropping holes: " ++ show (map fst ns'')) $

926 return (ps { pterm = tm',

930 return (ps { pterm = tm',

@@ -943,6 +947,7 @@ processTactic UnifyProblems ps

943 (problems ps)

947 (problems ps)

944 (injective ps)

948 (injective ps)

945 (holes ps)

949 (holes ps)

950+ (map fst (notunified ps))

946 pterm' = updateSolved ns' (pterm ps) in

951 pterm' = updateSolved ns' (pterm ps) in

947 traceWhen (unifylog ps) ("Dropping holes: " ++ show (map fst ns')) $

952 traceWhen (unifylog ps) ("Dropping holes: " ++ show (map fst ns')) $

948 return (ps { pterm = pterm', solved = Nothing, problems = probs',

953 return (ps { pterm = pterm', solved = Nothing, problems = probs',

@@ -976,6 +981,7 @@ processTactic t ps

976 [s] (problems ps')

981 [s] (problems ps')

977 (injective ps')

982 (injective ps')

978 (holes ps')

983 (holes ps')

984+ (map fst (notunified ps))

979 _ -> ([], problems ps')

985 _ -> ([], problems ps')

980 -- rechecking problems may find more solutions, so

986 -- rechecking problems may find more solutions, so

981 -- apply them here

987 -- apply them here

src/Idris/Core/TT.hs+1−1

@@ -384,7 +384,7 @@ tcname _ = False

384

385implicitable (NS n _) = implicitable n

386implicitable (UN xs) | T.null xs = False

387− | otherwise = isLower (T.head xs)

387+ | otherwise = isLower (T.head xs) || T.head xs == '_'

388implicitable (MN _ x) = not (tnull x) && thead x /= '_'

389implicitable _ = False

390

src/Idris/Core/Unify.hs+8−11

@@ -242,9 +242,10 @@ hasv (App f a) = hasv f || hasv a

242hasv (Bind x b sc) = hasv (binderTy b) || hasv sc

243hasv _ = False

244

245−unify :: Context -> Env -> TT Name -> TT Name -> [Name] -> [Name] -> [FailContext] ->

245+unify :: Context -> Env -> TT Name -> TT Name ->

246+ [Name] -> [Name] -> [Name] -> [FailContext] ->

246 TC ([(Name, TT Name)], Fails)

247 TC ([(Name, TT Name)], Fails)

247−unify ctxt env topx topy inj holes from =

248+unify ctxt env topx topy inj holes usersupp from =

248-- traceWhen (hasv topx || hasv topy)

249-- traceWhen (hasv topx || hasv topy)

249-- ("Unifying " ++ show topx ++ "\nAND\n" ++ show topy ++ "\n") $

250-- ("Unifying " ++ show topx ++ "\nAND\n" ++ show topy ++ "\n") $

250 -- don't bother if topx and topy are different at the head

251 -- don't bother if topx and topy are different at the head

@@ -428,18 +429,12 @@ unify ctxt env topx topy inj holes from =

428

429

429 unApp fn bnames appx@(App fx ax) appy@(App fy ay)

430 unApp fn bnames appx@(App fx ax) appy@(App fy ay)

430 | (injectiveApp fx && injectiveApp fy)

431 | (injectiveApp fx && injectiveApp fy)

431− || (injectiveApp fx && rigid appx && metavarApp appy && numArgs appx == numArgs appy)

432− || (injectiveApp fy && rigid appy && metavarApp appx && numArgs appx == numArgs appy)

433 || (injectiveApp fx && metavarApp fy && ax == ay)

432 || (injectiveApp fx && metavarApp fy && ax == ay)

434 || (injectiveApp fy && metavarApp fx && ax == ay)

433 || (injectiveApp fy && metavarApp fx && ax == ay)

435 = do let (headx, _) = unApply fx

434 = do let (headx, _) = unApply fx

436 let (heady, _) = unApply fy

435 let (heady, _) = unApply fy

437 -- fail quickly if the heads are disjoint

436 -- fail quickly if the heads are disjoint

438 checkHeads headx heady

437 checkHeads headx heady

439−-- if True then -- (injective fx || injective fy || fx == fy) then

440−-- if (injective fx && metavarApp appy) ||

441−-- (injective fy && metavarApp appx) ||

442−-- (injective fx && injective fy) || fx == fy

443 uplus

438 uplus

444 (do hf <- un' True bnames fx fy

439 (do hf <- un' True bnames fx fy

445 let ax' = hnormalise hf ctxt env (substNames hf ax)

440 let ax' = hnormalise hf ctxt env (substNames hf ax)

@@ -503,7 +498,8 @@ unify ctxt env topx topy inj holes from =

503 _ -> False

498 _ -> False

504

499

505 metavar t = case t of

500 metavar t = case t of

501+ P _ x _ -> (x `notElem` usersupp &&

506− P _ x _ -> (x `elem` holes || holeIn env x)

502+ (x `elem` holes || holeIn env x))

507 || globmetavar t

503 || globmetavar t

508 _ -> False

504 _ -> False

509 pat t = case t of

505 pat t = case t of

@@ -624,12 +620,13 @@ envPos x i ((y, _) : ys) | x == y = i

624-- ASSUMPTION: inputs are in normal form

620-- ASSUMPTION: inputs are in normal form

625

621

626recoverable t@(App _ _) _

622recoverable t@(App _ _) _

627− | (P _ (UN l) _, _) <- unApply t, l == txt "Lazy" = False

623+ | (P _ (UN l) _, _) <- unApply t, l == txt "Lazy'" = False

628recoverable _ t@(App _ _)

624recoverable _ t@(App _ _)

629− | (P _ (UN l) _, _) <- unApply t, l == txt "Lazy" = False

625+ | (P _ (UN l) _, _) <- unApply t, l == txt "Lazy'" = False

630recoverable (P (DCon _ _) x _) (P (DCon _ _) y _) = x == y

626recoverable (P (DCon _ _) x _) (P (DCon _ _) y _) = x == y

631recoverable (P (TCon _ _) x _) (P (TCon _ _) y _) = x == y

627recoverable (P (TCon _ _) x _) (P (TCon _ _) y _) = x == y

632recoverable (Constant _) (P (DCon _ _) y _) = False

628recoverable (Constant _) (P (DCon _ _) y _) = False

629+recoverable (Constant x) (Constant y) = x == y

633recoverable (P (DCon _ _) x _) (Constant _) = False

630recoverable (P (DCon _ _) x _) (Constant _) = False

634recoverable (Constant _) (P (TCon _ _) y _) = False

631recoverable (Constant _) (P (TCon _ _) y _) = False

635recoverable (P (TCon _ _) x _) (Constant _) = False

632recoverable (P (TCon _ _) x _) (Constant _) = False

src/Idris/Coverage.hs+6−7

@@ -360,9 +360,7 @@ calcTotality fc n pats

360 _ -> []

361 case mapMaybe (checkLHS i) (map (\ (_, l, r) -> l) pats) of

362 (failure : _) -> return failure

363− _ -> if (Coinductive `elem` opts)

364− then calcProd i fc n pats

365− else checkSizeChange n

363+ _ -> checkSizeChange n

366 where

364 where

367 checkLHS i (P _ fn _)

365 checkLHS i (P _ fn _)

368 = case lookupTotal fn (tt_ctxt i) of

366 = case lookupTotal fn (tt_ctxt i) of

@@ -471,7 +469,7 @@ buildSCG (_, n) = do

471 do logLvl 2 $ "Building SCG for " ++ show n ++ " from\n"

469 do logLvl 2 $ "Building SCG for " ++ show n ++ " from\n"

472 ++ show pats ++ "\n" ++ show sc

470 ++ show pats ++ "\n" ++ show sc

473 let newscg = buildSCG' ist (rights pats) args

471 let newscg = buildSCG' ist (rights pats) args

474− logLvl 5 $ show newscg

472+ logLvl 5 $ "SCG is: " ++ show newscg

475 addToCG n ( cg { scg = newscg } )

473 addToCG n ( cg { scg = newscg } )

476 [] -> logLvl 5 $ "Could not build SCG for " ++ show n ++ "\n"

474 [] -> logLvl 5 $ "Could not build SCG for " ++ show n ++ "\n"

477 x -> error $ "buildSCG: " ++ show (n, x)

475 x -> error $ "buildSCG: " ++ show (n, x)

@@ -489,13 +487,14 @@ delazy' all (Bind n b sc) = Bind n (fmap (delazy' all) b) (delazy' all sc)

489delazy' all t = t

487delazy' all t = t

490

488

491data Guardedness = Toplevel | Unguarded | Guarded

489data Guardedness = Toplevel | Unguarded | Guarded

490+ deriving Show

492

491

493buildSCG' :: IState -> [(Term, Term)] -> [Name] -> [SCGEntry]

492buildSCG' :: IState -> [(Term, Term)] -> [Name] -> [SCGEntry]

494buildSCG' ist pats args = nub $ concatMap scgPat pats where

493buildSCG' ist pats args = nub $ concatMap scgPat pats where

495 scgPat (lhs, rhs) = let lhs' = delazy lhs

494 scgPat (lhs, rhs) = let lhs' = delazy lhs

496 rhs' = delazy rhs

495 rhs' = delazy rhs

497 (f, pargs) = unApply (dePat lhs') in

496 (f, pargs) = unApply (dePat lhs') in

498− findCalls Toplevel (dePat rhs') (patvars lhs') pargs

497+ findCalls Toplevel (dePat rhs') (patvars lhs') pargs

499

498

500 findCalls guarded ap@(App f a) pvs pargs

499 findCalls guarded ap@(App f a) pvs pargs

501 -- under a call to "assert_total", don't do any checking, just believe

500 -- under a call to "assert_total", don't do any checking, just believe

@@ -506,10 +505,10 @@ buildSCG' ist pats args = nub $ concatMap scgPat pats where

506 -- immediate call, as long as the call is guarded.

505 -- immediate call, as long as the call is guarded.

507 -- Then check its arguments

506 -- Then check its arguments

508 | (P _ (UN del) _, [_,_,arg]) <- unApply ap,

507 | (P _ (UN del) _, [_,_,arg]) <- unApply ap,

509− guarded <- Guarded,

508+ Guarded <- guarded,

510 del == txt "Delay"

509 del == txt "Delay"

511 = let (capp, args) = unApply arg in

510 = let (capp, args) = unApply arg in

512− concatMap (\x -> findCalls Toplevel x pvs pargs) args

511+ concatMap (\x -> findCalls guarded x pvs pargs) args

513 | (P _ n _, args) <- unApply ap

512 | (P _ n _, args) <- unApply ap

514 = let nguarded = case guarded of

513 = let nguarded = case guarded of

515 Unguarded -> Unguarded

514 Unguarded -> Unguarded

src/Idris/DSL.hs+3−2

@@ -39,7 +39,8 @@ expandDo dsl (PAppBind fc t args) = PAppBind fc (expandDo dsl t)

39 (map (fmap (expandDo dsl)) args)

40expandDo dsl (PCase fc s opts) = PCase fc (expandDo dsl s)

41 (map (pmap (expandDo dsl)) opts)

42−expandDo dsl (PEq fc l r) = PEq fc (expandDo dsl l) (expandDo dsl r)

42+expandDo dsl (PEq fc lt rt l r) = PEq fc (expandDo dsl lt) (expandDo dsl rt)

43+ (expandDo dsl l) (expandDo dsl r)

43expandDo dsl (PPair fc p l r) = PPair fc p (expandDo dsl l) (expandDo dsl r)

44expandDo dsl (PPair fc p l r) = PPair fc p (expandDo dsl l) (expandDo dsl r)

44expandDo dsl (PDPair fc p l t r) = PDPair fc p (expandDo dsl l) (expandDo dsl t)

45expandDo dsl (PDPair fc p l t r) = PDPair fc p (expandDo dsl l) (expandDo dsl t)

45 (expandDo dsl r)

46 (expandDo dsl r)

@@ -98,7 +99,7 @@ var dsl n t i = v' i t where

98 v' i (PTyped l r) = PTyped (v' i l) (v' i r)

99 v' i (PTyped l r) = PTyped (v' i l) (v' i r)

99 v' i (PApp f x as) = PApp f (v' i x) (fmap (fmap (v' i)) as)

100 v' i (PApp f x as) = PApp f (v' i x) (fmap (fmap (v' i)) as)

100 v' i (PCase f t as) = PCase f (v' i t) (fmap (pmap (v' i)) as)

101 v' i (PCase f t as) = PCase f (v' i t) (fmap (pmap (v' i)) as)

101− v' i (PEq f l r) = PEq f (v' i l) (v' i r)

102+ v' i (PEq f lt rt l r) = PEq f (v' i lt) (v' i rt) (v' i l) (v' i r)

102 v' i (PPair f p l r) = PPair f p (v' i l) (v' i r)

103 v' i (PPair f p l r) = PPair f p (v' i l) (v' i r)

103 v' i (PDPair f p l t r) = PDPair f p (v' i l) (v' i t) (v' i r)

104 v' i (PDPair f p l t r) = PDPair f p (v' i l) (v' i t) (v' i r)

104 v' i (PAlternative a as) = PAlternative a $ map (v' i) as

105 v' i (PAlternative a as) = PAlternative a $ map (v' i) as

src/Idris/DeepSeq.hs+1−1

@@ -205,7 +205,7 @@ instance NFData PTerm where

205 rnf (PFalse x1) = rnf x1 `seq` ()

206 rnf (PRefl x1 x2) = rnf x1 `seq` rnf x2 `seq` ()

207 rnf (PResolveTC x1) = rnf x1 `seq` ()

208− rnf (PEq x1 x2 x3) = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` ()

208+ rnf (PEq x1 x2 x3 x4 x5) = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` rnf x4 `seq` rnf x5 `seq` ()

209 rnf (PRewrite x1 x2 x3 x4)

210 = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` rnf x4 `seq` ()

211 rnf (PPair x1 x2 x3 x4) = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` rnf x4 `seq` ()

src/Idris/Delaborate.hs+65−9

@@ -12,8 +12,9 @@ import Idris.Core.Evaluate

12import Idris.Docstrings (overview, renderDocstring)

13import Idris.ErrReverse

14

15−import Data.List (intersperse)

15+import Data.List (intersperse, nub)

16import qualified Data.Text as T

17+import Control.Monad.State

17

18

18import Debug.Trace

19import Debug.Trace

19

20

@@ -96,9 +97,10 @@ delabTy' ist imps tm fullname mvs = de [] imps tm

96 | n == sUN "Sigma"

97 | n == sUN "Sigma"

97 = PDPair un IsType (PRef un x) (de env [] ty)

98 = PDPair un IsType (PRef un x) (de env [] ty)

98 (de ((x,x):env) [] (instantiate (P Bound x ty) r))

99 (de ((x,x):env) [] (instantiate (P Bound x ty) r))

99− deFn env (P _ n _) [_,_,l,r]

100+ deFn env (P _ n _) [lt,rt,l,r]

100 | n == pairCon = PPair un IsTerm (de env [] l) (de env [] r)

101 | n == pairCon = PPair un IsTerm (de env [] l) (de env [] r)

101− | n == eqTy = PEq un (de env [] l) (de env [] r)

102+ | n == eqTy = PEq un (de env [] lt) (de env [] rt)

103+ (de env [] l) (de env [] r)

102 | n == sUN "Sg_intro" = PDPair un IsTerm (de env [] l) Placeholder

104 | n == sUN "Sg_intro" = PDPair un IsTerm (de env [] l) Placeholder

103 (de env [] r)

105 (de env [] r)

104 deFn env f@(P _ n _) args

106 deFn env f@(P _ n _) args

@@ -165,9 +167,14 @@ pprintErr' i (InternalMsg s) =

165 text ("Please consider reporting at " ++ bugaddr)

167 text ("Please consider reporting at " ++ bugaddr)

166 ]

168 ]

167pprintErr' i (CantUnify _ x_in y_in e sc s) =

169pprintErr' i (CantUnify _ x_in y_in e sc s) =

170+ let (x_ns, y_ns, nms) = renameMNs x_in y_in

168− let (x, y) = addImplicitDiffs (delab i x_in) (delab i y_in) in

171+ (x, y) = addImplicitDiffs (delab i x_ns) (delab i y_ns) in

169− text "Can't unify" <> indented (annTm x_in (pprintTerm' i (map (\ (n, b) -> (n, False)) sc) x)) <$>

172+ text "Can't unify" <> indented (annTm x_ns

173+ (pprintTerm' i (map (\ (n, b) -> (n, False)) sc

174+ ++ zip nms (repeat False)) x)) <$>

175+ text "with" <> indented (annTm y_ns

170− text "with" <> indented (annTm y_in (pprintTerm' i (map (\ (n, b) -> (n, False)) sc) y)) <>

176+ (pprintTerm' i (map (\ (n, b) -> (n, False)) sc

177+ ++ zip nms (repeat False)) y)) <>

171 case e of

178 case e of

172 Msg "" -> empty

179 Msg "" -> empty

173 _ -> line <> line <> text "Specifically:" <>

180 _ -> line <> line <> text "Specifically:" <>

@@ -263,6 +270,34 @@ pprintErr' i (ReflectionFailed msg err) =

263 indented (pprintErr' i err) <>

270 indented (pprintErr' i err) <>

264 text ("This is probably a bug. Please consider reporting it at " ++ bugaddr)

271 text ("This is probably a bug. Please consider reporting it at " ++ bugaddr)

265

272

273+-- Make sure the machine invented names are shown helpfully to the user, so

274+-- that any names which differ internally also differ visibly

275+-- FIXME: I can't actually contrive an error to test this! Will revisit later...

276+renameMNs :: Term -> Term -> (Term, Term, [Name])

277+renameMNs x y = let ns = nub $ allTTNames x ++ allTTNames y

278+ newnames = evalState (getRenames [] ns) 1 in

279+ (rename newnames x, rename newnames y, map snd newnames)

280+ where

281+ getRenames :: [(Name, Name)] -> [Name] -> State Int [(Name, Name)]

282+ getRenames acc [] = return acc

283+ getRenames acc (n@(MN i x) : xs) | UN x `elem` xs

284+ = do idx <- get

285+ put (idx + 1)

286+ let x' = sUN (str x ++ show idx)

287+ getRenames ((n, x') : acc) xs

288+ getRenames acc (x : xs) = getRenames acc xs

289+

290+ rename :: [(Name, Name)] -> Term -> Term

291+ rename ns (P nt x t) | Just x' <- lookup x ns = P nt x' t

292+ rename ns (App f a) = App (rename ns f) (rename ns a)

293+ rename ns (Bind x b sc)

294+ = let b' = fmap (rename ns) b

295+ sc' = rename ns sc in

296+ case lookup x ns of

297+ Just x' -> Bind x' b' sc'

298+ Nothing -> Bind x b' sc'

299+ rename ns x = x

300+

266-- If the two terms only differ in their implicits, mark the implicits which

301-- If the two terms only differ in their implicits, mark the implicits which

267-- differ as AlwaysShow so that they appear in errors

302-- differ as AlwaysShow so that they appear in errors

268addImplicitDiffs :: PTerm -> PTerm -> (PTerm, PTerm)

303addImplicitDiffs :: PTerm -> PTerm -> (PTerm, PTerm)

@@ -295,10 +330,30 @@ addImplicitDiffs x y

295 addI (PRefl fc a) (PRefl fc' b)

330 addI (PRefl fc a) (PRefl fc' b)

296 = let (a', b') = addI a b in

331 = let (a', b') = addI a b in

297 (PRefl fc a', PRefl fc' b')

332 (PRefl fc a', PRefl fc' b')

298− addI (PEq fc a b) (PEq fc' c d)

333+ addI (PEq fc at bt a b) (PEq fc' ct dt c d)

334+ | trace (show (at,bt)) False = undefined

335+ | at `expLike` ct && bt `expLike` dt

299 = let (a', c') = addI a c

336 = let (a', c') = addI a c

300 (b', d') = addI b d in

337 (b', d') = addI b d in

301− (PEq fc a' b', PEq fc' c' d')

338+ (PEq fc at bt a' b', PEq fc' ct dt c' d')

339+ | otherwise

340+ = let (at', ct') = addI at ct

341+ (bt', dt') = addI bt dt

342+ (a', c') = addI a c

343+ (b', d') = addI b d

344+ showa = if at `expLike` ct then [] else [AlwaysShow]

345+ showb = if bt `expLike` dt then [] else [AlwaysShow] in

346+ (PApp fc (PRef fc eqTy) [(pimp (sUN "A") at' True)

347+ { argopts = showa },

348+ (pimp (sUN "B") bt' True)

349+ { argopts = showb },

350+ pexp a', pexp b'],

351+ PApp fc (PRef fc eqTy) [(pimp (sUN "A") ct' True)

352+ { argopts = showa },

353+ (pimp (sUN "B") dt' True)

354+ { argopts = showb },

355+ pexp c', pexp d'])

356+

302 addI (PPair fc pi a b) (PPair fc' pi' c d)

357 addI (PPair fc pi a b) (PPair fc' pi' c d)

303 = let (a', c') = addI a c

358 = let (a', c') = addI a c

304 (b', d') = addI b d in

359 (b', d') = addI b d in

@@ -321,7 +376,8 @@ addImplicitDiffs x y

321 = n == n' && expLike s s' && expLike t t'

376 = n == n' && expLike s s' && expLike t t'

322 expLike (PPair _ _ x y) (PPair _ _ x' y') = expLike x x' && expLike y y'

377 expLike (PPair _ _ x y) (PPair _ _ x' y') = expLike x x' && expLike y y'

323 expLike (PDPair _ _ x _ y) (PDPair _ _ x' _ y') = expLike x x' && expLike y y'

378 expLike (PDPair _ _ x _ y) (PDPair _ _ x' _ y') = expLike x x' && expLike y y'

379+ expLike (PEq _ xt yt x y) (PEq _ xt' yt' x' y')

324− expLike (PEq _ x y) (PEq _ x' y') = expLike x x' && expLike y y'

380+ = expLike x x' && expLike y y'

325 expLike (PRefl _ x) (PRefl _ x') = expLike x x'

381 expLike (PRefl _ x) (PRefl _ x') = expLike x x'

326 expLike x y = x == y

382 expLike x y = x == y

327

383

src/Idris/ElabDecls.hs+64−30

@@ -136,11 +136,11 @@ elabType' norm info syn doc argDocs fc opts n ty' = {- let ty' = piBind (params

136 (cty, ty, inacc) <- buildType info syn fc opts n ty'

137

138 addStatics n cty ty

139− logLvl 2 $ "Rechecked to " ++ show cty

140 let nty = cty -- normalise ctxt [] cty

139 let nty = cty -- normalise ctxt [] cty

141 -- if the return type is something coinductive, freeze the definition

140 -- if the return type is something coinductive, freeze the definition

142 ctxt <- getContext

141 ctxt <- getContext

143 let nty' = normalise ctxt [] nty

142 let nty' = normalise ctxt [] nty

143+ logLvl 2 $ "Rechecked to " ++ show nty'

144

145 -- Add normalised type to internals

146 i <- getIState

@@ -863,19 +863,31 @@ elabRecord info syn doc fc tyn ty opts cdoc cn cty_in

863 _ -> ifail "Something went inexplicably wrong"

864 cimp <- case lookupCtxt cn (idris_implicits i) of

865 [imps] -> return imps

866+ ppos <- case lookupCtxt tyn (idris_datatypes i) of

867+ [ti] -> return $ param_pos ti

866− let ptys = getProjs [] (renameBs cimp cty)

868+ let cty_imp = renameBs cimp cty

869+ let ptys = getProjs [] cty_imp

867 let ptys_u = getProjs [] cty

870 let ptys_u = getProjs [] cty

868− let recty = getRecTy cty

871+ let recty = getRecTy cty_imp

872+ let recty_u = getRecTy cty

873+

874+ let paramNames = getPNames recty ppos

869

875

870 -- rename indices when we generate the getter/setter types, so

876 -- rename indices when we generate the getter/setter types, so

871 -- that they don't clash with the names of the projections

877 -- that they don't clash with the names of the projections

872 -- we're generating

878 -- we're generating

873− let index_names_in = getRecNameMap "_in" recty

879+ let index_names_in = getRecNameMap "_in" ppos recty

874 let recty_in = substMatches index_names_in recty

880 let recty_in = substMatches index_names_in recty

875

881

876− logLvl 1 $ show (recty, ptys)

882+ logLvl 3 $ show (recty, recty_u, ppos, paramNames, ptys)

883+ -- Substitute indices with projection functions, and parameters with

884+ -- the updated parameter name

877− let substs = map (\ (n, _) -> (n, PApp fc (PRef fc n)

885+ let substs = map (\ (n, _) ->

886+ if n `elem` paramNames

887+ then (n, PRef fc (mkp n))

888+ else (n, PApp fc (PRef fc n)

878− [pexp (PRef fc rec)])) ptys

889+ [pexp (PRef fc rec)]))

890+ ptys

879

891

880 -- Generate projection functions

892 -- Generate projection functions

881 proj_decls <- mapM (mkProj recty_in substs cimp) (zip ptys [0..])

893 proj_decls <- mapM (mkProj recty_in substs cimp) (zip ptys [0..])

@@ -884,7 +896,7 @@ elabRecord info syn doc fc tyn ty opts cdoc cn cty_in

884 let implBinds = getImplB id cty'

896 let implBinds = getImplB id cty'

885

897

886 -- Generate update functions

898 -- Generate update functions

887− update_decls <- mapM (mkUpdate recty index_names_in extraImpls

899+ update_decls <- mapM (mkUpdate recty_u index_names_in extraImpls

888 (getFieldNames cty')

900 (getFieldNames cty')

889 implBinds (length nonImp)) (zip nonImp [0..])

901 implBinds (length nonImp)) (zip nonImp [0..])

890 mapM_ (elabDecl EAll info) (concat proj_decls)

902 mapM_ (elabDecl EAll info) (concat proj_decls)

@@ -896,6 +908,14 @@ elabRecord info syn doc fc tyn ty opts cdoc cn cty_in

896 isNonImp (PExp _ _ _ _, a) = Just a

908 isNonImp (PExp _ _ _ _, a) = Just a

897 isNonImp _ = Nothing

909 isNonImp _ = Nothing

898

910

911+ getPNames (PApp _ _ as) ppos = getpn as ppos

912+ where

913+ getpn as [] = []

914+ getpn as (i:is) | length as > i,

915+ PRef _ n <- getTm (as!!i) = n : getpn as is

916+ | otherwise = getpn as is

917+ getPNames _ _ = []

918+

899 tryElabDecl info (fn, ty, val)

919 tryElabDecl info (fn, ty, val)

900 = do i <- getIState

920 = do i <- getIState

901 idrisCatch (do elabDecl' EAll info ty

921 idrisCatch (do elabDecl' EAll info ty

@@ -932,15 +952,21 @@ elabRecord info syn doc fc tyn ty opts cdoc cn cty_in

932 getRecTy (PPi _ n ty s) = getRecTy s

952 getRecTy (PPi _ n ty s) = getRecTy s

933 getRecTy t = t

953 getRecTy t = t

934

954

955+ -- make sure we pick a consistent name for parameters; any name will do

956+ -- otherwise

935− getRecNameMap x (PApp fc t args) = mapMaybe (toMN . getTm) args

957+ getRecNameMap x ppos (PApp fc t args)

958+ = mapMaybe toMN (zip [0..] (map getTm args))

936 where

959 where

960+ toMN (i, PRef fc n)

961+ | i `elem` ppos = Just (n, PRef fc (mkp n))

937− toMN (PRef fc n) = Just (n, PRef fc (sMN 0 (show n ++ x)))

962+ | otherwise = Just (n, PRef fc (sMN 0 (show n ++ x)))

938 toMN _ = Nothing

963 toMN _ = Nothing

939− getRecNameMap x _ = []

964+ getRecNameMap x _ _ = []

940

965

941 rec = sMN 0 "rec"

966 rec = sMN 0 "rec"

942

967

968+ -- only UNs propagate properly as parameters (bit of a hack then...)

943− mkp (UN n) = sMN 0 ("p_" ++ str n)

969+ mkp (UN n) = sUN ("_p_" ++ str n)

944 mkp (MN i n) = sMN i ("p_" ++ str n)

970 mkp (MN i n) = sMN i ("p_" ++ str n)

945 mkp (NS n s) = NS (mkp n) s

971 mkp (NS n s) = NS (mkp n) s

946

972

@@ -953,18 +979,19 @@ elabRecord info syn doc fc tyn ty opts cdoc cn cty_in

953 mkType (NS n s) = NS (mkType n) s

979 mkType (NS n s) = NS (mkType n) s

954

980

955 mkProj recty substs cimp ((pn_in, pty), pos)

981 mkProj recty substs cimp ((pn_in, pty), pos)

956− = do let pn = expandNS syn pn_in

982+ = do let pn = expandNS syn pn_in -- projection name

983+ -- use pn_in in the indices, consistently, to avoid clash

957 let pfnTy = PTy emptyDocstring [] defaultSyntax fc [] pn

984 let pfnTy = PTy emptyDocstring [] defaultSyntax fc [] pn

958 (PPi expl rec recty

985 (PPi expl rec recty

959 (substMatches substs pty))

986 (substMatches substs pty))

960 let pls = repeat Placeholder

987 let pls = repeat Placeholder

961 let before = pos

988 let before = pos

962 let after = length substs - (pos + 1)

989 let after = length substs - (pos + 1)

963− let args = take before pls ++ PRef fc (mkp pn) : take after pls

990+ let args = take before pls ++ PRef fc (mkp pn_in) : take after pls

964 let iargs = map implicitise (zip cimp args)

991 let iargs = map implicitise (zip cimp args)

965 let lhs = PApp fc (PRef fc pn)

992 let lhs = PApp fc (PRef fc pn)

966 [pexp (PApp fc (PRef fc cn) iargs)]

993 [pexp (PApp fc (PRef fc cn) iargs)]

967− let rhs = PRef fc (mkp pn)

994+ let rhs = PRef fc (mkp pn_in)

968 let pclause = PClause fc pn lhs [] rhs []

995 let pclause = PClause fc pn lhs [] rhs []

969 return [pfnTy, PClauses fc [] pn [pclause]]

996 return [pfnTy, PClauses fc [] pn [pclause]]

970

997

@@ -1425,7 +1452,8 @@ checkPossible info fc tcgen fname lhs_in

1425 | otherwise = False -- name is different, unrecoverable

1452 | otherwise = False -- name is different, unrecoverable

1426

1453

1427getFixedInType i env (PExp _ _ _ _ : is) (Bind n (Pi t) sc)

1454getFixedInType i env (PExp _ _ _ _ : is) (Bind n (Pi t) sc)

1455+ = nub $ getFixedInType i env [] t ++

1428− = getFixedInType i (n : env) is (instantiate (P Bound n t) sc)

1456+ getFixedInType i (n : env) is (instantiate (P Bound n t) sc)

1429getFixedInType i env (_ : is) (Bind n (Pi t) sc)

1457getFixedInType i env (_ : is) (Bind n (Pi t) sc)

1430 = getFixedInType i (n : env) is (instantiate (P Bound n t) sc)

1458 = getFixedInType i (n : env) is (instantiate (P Bound n t) sc)

1431getFixedInType i env is tm@(App f a)

1459getFixedInType i env is tm@(App f a)

@@ -1472,8 +1500,8 @@ paramNames args env (p : ps)

1472 _ -> paramNames args env ps

1500 _ -> paramNames args env ps

1473 | otherwise = paramNames args env ps

1501 | otherwise = paramNames args env ps

1474

1502

1475−propagateParams :: [Name] -> Type -> PTerm -> PTerm

1503+propagateParams :: IState -> [Name] -> Type -> PTerm -> PTerm

1476−propagateParams ps t tm@(PApp _ (PRef fc n) args)

1504+propagateParams i ps t tm@(PApp _ (PRef fc n) args)

1477 = PApp fc (PRef fc n) (addP t args)

1505 = PApp fc (PRef fc n) (addP t args)

1478 where addP (Bind n _ sc) (t : ts)

1506 where addP (Bind n _ sc) (t : ts)

1479 | Placeholder <- getTm t,

1507 | Placeholder <- getTm t,

@@ -1482,9 +1510,15 @@ propagateParams ps t tm@(PApp _ (PRef fc n) args)

1482 = t { getTm = PRef fc n } : addP sc ts

1510 = t { getTm = PRef fc n } : addP sc ts

1483 addP (Bind n _ sc) (t : ts) = t : addP sc ts

1511 addP (Bind n _ sc) (t : ts) = t : addP sc ts

1484 addP _ ts = ts

1512 addP _ ts = ts

1485−propagateParams ps t (PRef fc n)

1513+propagateParams i ps t (PRef fc n)

1514+ = case lookupCtxt n (idris_implicits i) of

1515+ [is] -> let ps' = filter (isImplicit is) ps in

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

1516+ PApp fc (PRef fc n) (map (\x -> pimp x (PRef fc x) True) ps')

1517+ _ -> PRef fc n

1518+ where isImplicit [] n = False

1519+ isImplicit (PImp _ _ _ x _ : is) n | x == n = True

1520+ isImplicit (_ : is) n = isImplicit is n

1487−propagateParams ps t x = x

1521+propagateParams i ps t x = x

1488

1522

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

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

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

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

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

1516 _ -> []

1550 _ -> []

1517 let params = getParamsInType i [] fn_is fn_ty

1551 let params = getParamsInType i [] fn_is fn_ty

1518 let lhs = mkLHSapp $ stripUnmatchable i $

1552 let lhs = mkLHSapp $ stripUnmatchable i $

1519− propagateParams params fn_ty (addImplPat i (stripLinear i lhs_in))

1553+ propagateParams i params fn_ty (addImplPat i (stripLinear i lhs_in))

1520 logLvl 5 ("LHS: " ++ show fc ++ " " ++ showTmImpls lhs)

1554 logLvl 5 ("LHS: " ++ show fc ++ " " ++ showTmImpls lhs)

1521 logLvl 4 ("Fixed parameters: " ++ show params ++ " from " ++ show lhs_in ++

1555 logLvl 4 ("Fixed parameters: " ++ show params ++ " from " ++ show lhs_in ++

1522 "\n" ++ show (fn_ty, fn_is))

1556 "\n" ++ show (fn_ty, fn_is))

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

1711 [t] -> t

1745 [t] -> t

1712 _ -> []

1746 _ -> []

1713 let params = getParamsInType i [] fn_is fn_ty

1747 let params = getParamsInType i [] fn_is fn_ty

1714− let lhs = propagateParams params fn_ty (addImplPat i (stripLinear i lhs_in))

1748+ let lhs = propagateParams i params fn_ty (addImplPat i (stripLinear i lhs_in))

1715 logLvl 2 ("LHS: " ++ show lhs)

1749 logLvl 2 ("LHS: " ++ show lhs)

1716 ((lhs', dlhs, []), _) <-

1750 ((lhs', dlhs, []), _) <-

1717 tclift $ elaborate ctxt (sMN 0 "patLHS") infP []

1751 tclift $ elaborate ctxt (sMN 0 "patLHS") infP []

@@ -1719,11 +1753,11 @@ elabClause info opts (_, PWith fc fname lhs_in withs wval_in withblock)

1719 (erun fc (buildTC i info ELHS opts fname (infTerm lhs))) )

1753 (erun fc (buildTC i info ELHS opts fname (infTerm lhs))) )

1720 let lhs_tm = orderPats (getInferTerm lhs')

1754 let lhs_tm = orderPats (getInferTerm lhs')

1721 let lhs_ty = getInferType lhs'

1755 let lhs_ty = getInferType lhs'

1722− let ret_ty = getRetTy lhs_ty

1756+ let ret_ty = getRetTy (explicitNames (normalise ctxt [] lhs_ty))

1723 logLvl 3 (show lhs_tm)

1757 logLvl 3 (show lhs_tm)

1724 (clhs, clhsty) <- recheckC fc [] lhs_tm

1758 (clhs, clhsty) <- recheckC fc [] lhs_tm

1725 logLvl 5 ("Checked " ++ show clhs)

1759 logLvl 5 ("Checked " ++ show clhs)

1726− let bargs = getPBtys lhs_tm

1760+ let bargs = getPBtys (explicitNames (normalise ctxt [] lhs_tm))

1727 let wval = addImplBound i (map fst bargs) wval_in

1761 let wval = addImplBound i (map fst bargs) wval_in

1728 logLvl 5 ("Checking " ++ showTmImpls wval)

1762 logLvl 5 ("Checking " ++ showTmImpls wval)

1729 -- Elaborate wval in this context

1763 -- Elaborate wval in this context

@@ -1744,8 +1778,8 @@ elabClause info opts (_, PWith fc fname lhs_in withs wval_in withblock)

1744 mapM_ (elabCaseBlock info opts) is

1778 mapM_ (elabCaseBlock info opts) is

1745 logLvl 5 ("Checked wval " ++ show wval')

1779 logLvl 5 ("Checked wval " ++ show wval')

1746 (cwval, cwvalty) <- recheckC fc [] (getInferTerm wval')

1780 (cwval, cwvalty) <- recheckC fc [] (getInferTerm wval')

1747− let cwvaltyN = explicitNames cwvalty

1781+ let cwvaltyN = explicitNames (normalise ctxt [] cwvalty)

1748− let cwvalN = explicitNames cwval

1782+ let cwvalN = explicitNames (normalise ctxt [] cwval)

1749 logLvl 5 ("With type " ++ show cwvalty ++ "\nRet type " ++ show ret_ty)

1783 logLvl 5 ("With type " ++ show cwvalty ++ "\nRet type " ++ show ret_ty)

1750 let pvars = map fst (getPBtys cwvalty)

1784 let pvars = map fst (getPBtys cwvalty)

1751 -- we need the unelaborated term to get the names it depends on

1785 -- we need the unelaborated term to get the names it depends on

@@ -1760,12 +1794,12 @@ elabClause info opts (_, PWith fc fname lhs_in withs wval_in withblock)

1760 -- (ps : Xs) -> (withval : cwvalty) -> (ps' : Xs') -> ret_ty

1794 -- (ps : Xs) -> (withval : cwvalty) -> (ps' : Xs') -> ret_ty

1761 let wargval = getRetTy cwvalN

1795 let wargval = getRetTy cwvalN

1762 let wargtype = getRetTy cwvaltyN

1796 let wargtype = getRetTy cwvaltyN

1763− logLvl 5 ("Abstract over " ++ show wargval)

1797+ logLvl 5 ("Abstract over " ++ show wargval ++ " in " ++ show wargtype)

1764 let wtype = bindTyArgs Pi (bargs_pre ++

1798 let wtype = bindTyArgs Pi (bargs_pre ++

1765 (sMN 0 "warg", wargtype) :

1799 (sMN 0 "warg", wargtype) :

1766 map (abstract (sMN 0 "warg") wargval wargtype) bargs_post)

1800 map (abstract (sMN 0 "warg") wargval wargtype) bargs_post)

1767 (substTerm wargval (P Bound (sMN 0 "warg") wargtype) ret_ty)

1801 (substTerm wargval (P Bound (sMN 0 "warg") wargtype) ret_ty)

1768− logLvl 3 ("New function type " ++ show wtype)

1802+ logLvl 5 ("New function type " ++ show wtype)

1769 let wname = sMN windex (show fname)

1803 let wname = sMN windex (show fname)

1770

1804

1771 let imps = getImps wtype -- add to implicits context

1805 let imps = getImps wtype -- add to implicits context

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

1824 logLvl 2 ("Matching " ++ showTmImpls tm ++ " against " ++

1858 logLvl 2 ("Matching " ++ showTmImpls tm ++ " against " ++

1825 showTmImpls toplhs)

1859 showTmImpls toplhs)

1826 case matchClause i toplhs tm of

1860 case matchClause i toplhs tm of

1827− Left (a,b) -> trace ("matchClause: " ++ show a ++ " =/= " ++ show b) (ifail $ show fc ++ ":with clause does not match top level")

1861+ Left (a,b) -> ifail $ show fc ++ ":with clause does not match top level"

1828 Right mvars ->

1862 Right mvars ->

1829 do logLvl 3 ("Match vars : " ++ show mvars)

1863 do logLvl 3 ("Match vars : " ++ show mvars)

1830 lhs <- updateLHS n wname mvars ns ns' (fullApp tm) w

1864 lhs <- updateLHS n wname mvars ns ns' (fullApp tm) w

src/Idris/ElabQuasiquote.hs+5−3

@@ -106,10 +106,12 @@ extractUnquotes (PCase fc expr cases)

106extractUnquotes (PRefl fc x)

107 = do (x', ex) <- extractUnquotes x

108 return (PRefl fc x', ex)

109−extractUnquotes (PEq fc a b)

109+extractUnquotes (PEq fc at bt a b)

110+ = do (at', ex1) <- extractUnquotes at

111+ (bt', ex2) <- extractUnquotes bt

110− = do (a', ex1) <- extractUnquotes a

112+ (a', ex1) <- extractUnquotes a

111 (b', ex2) <- extractUnquotes b

113 (b', ex2) <- extractUnquotes b

112− return (PEq fc a' b', ex1 ++ ex2)

114+ return (PEq fc at' bt' a' b', ex1 ++ ex2)

113extractUnquotes (PRewrite fc x y z)

115extractUnquotes (PRewrite fc x y z)

114 = do (x', ex1) <- extractUnquotes x

116 = do (x', ex1) <- extractUnquotes x

115 (y', ex2) <- extractUnquotes y

117 (y', ex2) <- extractUnquotes y

src/Idris/ElabTerm.hs+96−44

@@ -14,7 +14,7 @@ import Idris.Core.Elaborate hiding (Tactic(..))

14import Idris.Core.TT

15import Idris.Core.Evaluate

16import Idris.Core.Unify

17−import Idris.Core.Typecheck (check)

17+import Idris.Core.Typecheck (check, recheck)

18import Idris.ErrReverse (errReverse)

19import Idris.ElabQuasiquote (extractUnquotes)

20

@@ -245,18 +245,33 @@ elab ist info emode opts fn tm

245 elab' ina (PResolveTC (FC "HACK" _ _)) -- for chasing parent classes

246 = do g <- goal; resolveTC 5 g fn ist

247 elab' ina (PResolveTC fc)

248− | True = do c <- getNameFrom (sMN 0 "class")

248+ = do c <- getNameFrom (sMN 0 "class")

249− instanceArg c

250− | otherwise = do g <- goal

251− try (resolveTC 2 g fn ist)

252− (do c <- getNameFrom (sMN 0 "class")

253− instanceArg c)

249+ instanceArg c

254 elab' ina (PRefl fc t)

250 elab' ina (PRefl fc t)

255 = elab' ina (PApp fc (PRef fc eqCon) [pimp (sMN 0 "A") Placeholder True,

251 = elab' ina (PApp fc (PRef fc eqCon) [pimp (sMN 0 "A") Placeholder True,

256 pimp (sMN 0 "x") t False])

252 pimp (sMN 0 "x") t False])

253+ elab' ina (PEq fc Placeholder Placeholder l r)

254+ = try (do tyn <- getNameFrom (sMN 0 "aqty")

255+ claim tyn RType

256+ movelast tyn

257+ elab' ina (PApp fc (PRef fc eqTy)

258+ [pimp (sUN "A") (PRef fc tyn) True,

259+ pimp (sUN "B") (PRef fc tyn) False,

260+ pexp l, pexp r]))

261+ (do atyn <- getNameFrom (sMN 0 "aqty")

262+ btyn <- getNameFrom (sMN 0 "bqty")

263+ claim atyn RType

264+ movelast atyn

265+ claim btyn RType

266+ movelast btyn

267+ elab' ina (PApp fc (PRef fc eqTy)

268+ [pimp (sUN "A") (PRef fc atyn) True,

269+ pimp (sUN "B") (PRef fc btyn) False,

270+ pexp l, pexp r]))

271+

257− elab' ina (PEq fc l r) = elab' ina (PApp fc (PRef fc eqTy)

272+ elab' ina (PEq fc lt rt l r) = elab' ina (PApp fc (PRef fc eqTy)

258− [pimp (sMN 0 "A") Placeholder True,

273+ [pimp (sUN "A") lt True,

259− pimp (sMN 0 "B") Placeholder False,

274+ pimp (sUN "B") rt False,

260 pexp l, pexp r])

275 pexp l, pexp r])

261 elab' ina@(_, a, inty, qq) (PPair fc _ l r)

276 elab' ina@(_, a, inty, qq) (PPair fc _ l r)

262 = do hnf_compute

277 = do hnf_compute

@@ -374,7 +389,8 @@ elab ist info emode opts fn tm

374 elabE (True, a, True, qq) sc

389 elabE (True, a, True, qq) sc

375 solve

390 solve

376 elab' ina@(_, a, inty, qq) (PLet n ty val sc)

391 elab' ina@(_, a, inty, qq) (PLet n ty val sc)

377− = do attack;

392+ = do attack

393+ ivs <- get_instances

378 tyn <- getNameFrom (sMN 0 "letty")

394 tyn <- getNameFrom (sMN 0 "letty")

379 claim tyn RType

395 claim tyn RType

380 valn <- getNameFrom (sMN 0 "letval")

396 valn <- getNameFrom (sMN 0 "letval")

@@ -388,6 +404,17 @@ elab ist info emode opts fn tm

388 elabE (True, a, True, qq) ty

404 elabE (True, a, True, qq) ty

389 focus valn

405 focus valn

390 elabE (True, a, True, qq) val

406 elabE (True, a, True, qq) val

407+ ivs' <- get_instances

408+ when (not pattern) $

409+ mapM_ (\n -> do focus n

410+ g <- goal

411+ hs <- get_holes

412+ if all (\n -> n == tyn || not (n `elem` hs)) (freeNames g)

413+ -- let insts = filter tcname $ map fst (ctxtAlist (tt_ctxt ist))

414+ then try (resolveTC 7 g fn ist)

415+ (movelast n)

416+ else movelast n)

417+ (ivs' \\ ivs)

391 env <- get_env

418 env <- get_env

392 elabE (True, a, inty, qq) sc

419 elabE (True, a, inty, qq) sc

393 -- HACK: If the name leaks into its type, it may leak out of

420 -- HACK: If the name leaks into its type, it may leak out of

@@ -485,7 +512,9 @@ elab ist info emode opts fn tm

485 -- we can unify with them

512 -- we can unify with them

486 case lookupCtxt f (idris_classes ist) of

513 case lookupCtxt f (idris_classes ist) of

487 [] -> return ()

514 [] -> return ()

488− _ -> mapM_ setInjective (map getTm args)

515+ _ -> do mapM_ setInjective (map getTm args)

516+ -- maybe more things are solvable now

517+ unifyProblems

489 ctxt <- get_context

518 ctxt <- get_context

490 let guarded = isConName f ctxt

519 let guarded = isConName f ctxt

491-- trace ("args is " ++ show args) $ return ()

520-- trace ("args is " ++ show args) $ return ()

@@ -498,10 +527,11 @@ elab ist info emode opts fn tm

498 -- Sort so that the implicit tactics and alternatives go last

527 -- Sort so that the implicit tactics and alternatives go last

499 let (ns', eargs) = unzip $

528 let (ns', eargs) = unzip $

500 sortBy cmpArg (zip ns args)

529 sortBy cmpArg (zip ns args)

530+ ulog <- getUnifyLog

501 elabArgs ist (ina || not isinf, guarded, inty, qq)

531 elabArgs ist (ina || not isinf, guarded, inty, qq)

502 [] fc False f ns'

532 [] fc False f ns'

503 (f == sUN "Force")

533 (f == sUN "Force")

504− (map (\x -> (False, getTm x)) eargs) -- TODO: remove this False arg

534+ (map (\x -> getTm x) eargs) -- TODO: remove this False arg

505 solve

535 solve

506 ivs' <- get_instances

536 ivs' <- get_instances

507 -- Attempt to resolve any type classes which have 'complete' types,

537 -- Attempt to resolve any type classes which have 'complete' types,

@@ -525,16 +555,23 @@ elab ist info emode opts fn tm

525 -- FIXME: Better would be to allow alternative resolution to be

555 -- FIXME: Better would be to allow alternative resolution to be

526 -- retried after more information is in.

556 -- retried after more information is in.

527 cmpArg (_, x) (_, y)

557 cmpArg (_, x) (_, y)

558+ | constraint x && not (constraint y) = LT

559+ | constraint y && not (constraint x) = GT

560+ | otherwise

528 = compare (conDepth 0 (getTm x) + priority x + alt x)

561 = compare (conDepth 0 (getTm x) + priority x + alt x)

529 (conDepth 0 (getTm y) + priority y + alt y)

562 (conDepth 0 (getTm y) + priority y + alt y)

530 where alt t = case getTm t of

563 where alt t = case getTm t of

531 PAlternative False _ -> 5

564 PAlternative False _ -> 5

532− PAlternative True _ -> 1

565+ PAlternative True _ -> 2

533 PTactics _ -> 150

566 PTactics _ -> 150

534− PLam _ _ _ -> 2

567+ PLam _ _ _ -> 3

535− PRewrite _ _ _ _ -> 3

568+ PRewrite _ _ _ _ -> 4

536− _ -> 0

569+ PResolveTC _ -> 0

537−

570+ _ -> 1

571+

572+ constraint (PConstraint _ _ _ _) = True

573+ constraint _ = False

574+

538 -- Score a point for every level where there is a non-constructor

575 -- Score a point for every level where there is a non-constructor

539 -- function (so higher score --> done later)

576 -- function (so higher score --> done later)

540 -- Only relevant when on lhs

577 -- Only relevant when on lhs

@@ -546,6 +583,7 @@ elab ist info emode opts fn tm

546 conDepth d (PPatvar _ _) = 0

583 conDepth d (PPatvar _ _) = 0

547 conDepth d (PAlternative _ as) = maximum (map (conDepth d) as)

584 conDepth d (PAlternative _ as) = maximum (map (conDepth d) as)

548 conDepth d Placeholder = 0

585 conDepth d Placeholder = 0

586+ conDepth d (PResolveTC _) = 0

549 conDepth d t = max (100 - d) 1

587 conDepth d t = max (100 - d) 1

550

588

551 checkIfInjective n = do

589 checkIfInjective n = do

@@ -558,7 +596,14 @@ elab ist info emode opts fn tm

558 case lookupCtxt c (idris_classes ist) of

596 case lookupCtxt c (idris_classes ist) of

559 [] -> return ()

597 [] -> return ()

560 _ -> -- type class, set as injective

598 _ -> -- type class, set as injective

561− mapM_ setinjArg args

599+ do mapM_ setinjArg args

600+ -- maybe we can solve more things now...

601+ ulog <- getUnifyLog

602+ probs <- get_probs

603+ traceWhen ulog ("Injective now " ++ show args ++ "\n" ++ qshow probs) $

604+ unifyProblems

605+ probs <- get_probs

606+ traceWhen ulog (qshow probs) $ return ()

562 _ -> return ()

607 _ -> return ()

563

608

564 setinjArg (P _ n _) = setinj n

609 setinjArg (P _ n _) = setinj n

@@ -715,12 +760,16 @@ elab ist info emode opts fn tm

715 -- original goal in the original proof state.

760 -- original goal in the original proof state.

716 env <- get_env

761 env <- get_env

717 loadState

762 loadState

718− case fmap (explicitNames . binderVal) $ lookup nTm env of

763+ let quoted = fmap (explicitNames . binderVal) $ lookup nTm env

719− Just q

764+

765+ case quoted of

766+ Just q -> do ctxt <- get_context

767+ (q', _, _) <- lift $ recheck ctxt [(uq, Lam Erased) | uq <- unquoteNames] (forget q) q

768+ if pattern

720− | pattern -> reflectQuotePattern unquoteNames q

769+ then reflectQuotePattern unquoteNames q'

721− | otherwise -> do fill $ reflectQuote unquoteNames q

770+ else do fill $ reflectQuote unquoteNames q'

722− solve

771+ solve

723− Nothing -> fail "Broken elaboration of quasiquote"

772+ Nothing -> lift . tfail . Msg $ "Broken elaboration of quasiquote"

724

773

725 -- Finally fill in the terms or patterns from the unquotes. This

774 -- Finally fill in the terms or patterns from the unquotes. This

726 -- happens last so that their holes still exist while elaborating

775 -- happens last so that their holes still exist while elaborating

@@ -792,16 +841,17 @@ elab ist info emode opts fn tm

792 do ty <- goal

841 do ty <- goal

793 env <- get_env

842 env <- get_env

794 let (tyh, _) = unApply (normalise (tt_ctxt ist) env ty)

843 let (tyh, _) = unApply (normalise (tt_ctxt ist) env ty)

795− let tries = if pattern then [t, mkDelay t] else [mkDelay t, t]

844+ let tries = if pattern then [t, mkDelay env t] else [mkDelay env t, t]

796 case tyh of

845 case tyh of

797 P _ (UN l) _ | l == txt "Lazy'"

846 P _ (UN l) _ | l == txt "Lazy'"

798 -> return (PAlternative False tries)

847 -> return (PAlternative False tries)

799 _ -> return t

848 _ -> return t

800 where

849 where

801− mkDelay (PAlternative b xs) = PAlternative b (map mkDelay xs)

850+ mkDelay env (PAlternative b xs) = PAlternative b (map (mkDelay env) xs)

851+ mkDelay env t

802− mkDelay t = let fc = fileFC "Delay" in

852+ = let fc = fileFC "Delay" in

803− addImpl ist (PApp fc (PRef fc (sUN "Delay"))

853+ addImplBound ist (map fst env) (PApp fc (PRef fc (sUN "Delay"))

804− [pexp t])

854+ [pexp t])

805

855

806 -- case is tricky enough without implicit coercions! If they are needed,

856 -- case is tricky enough without implicit coercions! If they are needed,

807 -- they can go in the branches separately.

857 -- they can go in the branches separately.

@@ -817,11 +867,12 @@ elab ist info emode opts fn tm

817 (PCoerced tm, _) -> tm

867 (PCoerced tm, _) -> tm

818 (_, []) -> t

868 (_, []) -> t

819 (_, cs) -> PAlternative False [t ,

869 (_, cs) -> PAlternative False [t ,

820− PAlternative True (map (mkCoerce t) cs)]

870+ PAlternative True (map (mkCoerce env t) cs)]

821 return t'

871 return t'

822 where

872 where

823− mkCoerce t n = let fc = fileFC "Coercion" in -- line never appears!

873+ mkCoerce env t n = let fc = fileFC "Coercion" in -- line never appears!

874+ addImplBound ist (map fst env)

824− addImpl ist (PApp fc (PRef fc n) [pexp (PCoerced t)])

875+ (PApp fc (PRef fc n) [pexp (PCoerced t)])

825

876

826 -- | Elaborate the arguments to a function

877 -- | Elaborate the arguments to a function

827 elabArgs :: IState -- ^ The current Idris state

878 elabArgs :: IState -- ^ The current Idris state

@@ -832,17 +883,13 @@ elab ist info emode opts fn tm

832 -> Name -- ^ Name of the function being applied

883 -> Name -- ^ Name of the function being applied

833 -> [(Name, Name)] -- ^ (Argument Name, Hole Name)

884 -> [(Name, Name)] -- ^ (Argument Name, Hole Name)

834 -> Bool -- ^ under a 'force'

885 -> Bool -- ^ under a 'force'

835− -> [(Bool, PTerm)] -- ^ (Laziness, argument)

886+ -> [PTerm] -- ^ (Laziness, argument)

836 -> ElabD ()

887 -> ElabD ()

837 elabArgs ist ina failed fc retry f [] force _ = return ()

888 elabArgs ist ina failed fc retry f [] force _ = return ()

838− elabArgs ist ina failed fc r f (n:ns) force ((_, Placeholder) : args)

889+ elabArgs ist ina failed fc r f (n:ns) force (Placeholder : args)

839 = elabArgs ist ina failed fc r f ns force args

890 = elabArgs ist ina failed fc r f ns force args

840− elabArgs ist ina failed fc r f ((argName, holeName):ns) force ((lazy, t) : args)

891+ elabArgs ist ina failed fc r f ((argName, holeName):ns) force (t : args)

841− | lazy && not pattern

842− = elabArg argName holeName (PApp bi (PRef bi (sUN "Delay"))

843− [pimp (sUN "a") Placeholder True,

844− pexp t])

845− | otherwise = elabArg argName holeName t

892+ = do elabArg argName holeName t

846 where elabArg argName holeName t =

893 where elabArg argName holeName t =

847 do now_elaborating fc f argName

894 do now_elaborating fc f argName

848 wrapErr f argName $ do

895 wrapErr f argName $ do

@@ -854,7 +901,11 @@ elab ist info emode opts fn tm

854 failed' <- -- trace (show (n, t, hs, tm)) $

901 failed' <- -- trace (show (n, t, hs, tm)) $

855 -- traceWhen (not (null cs)) (show ty ++ "\n" ++ showImp True t) $

902 -- traceWhen (not (null cs)) (show ty ++ "\n" ++ showImp True t) $

856 case holeName `elem` hs of

903 case holeName `elem` hs of

904+ True -> do focus holeName;

905+ g <- goal

906+ ulog <- getUnifyLog

907+ traceWhen ulog ("Elaborating argument " ++ show (argName, holeName, g)) $

857− True -> do focus holeName; elab ina t; return failed

908+ elab ina t; return failed

858 False -> return failed

909 False -> return failed

859 done_elaborating_arg f argName

910 done_elaborating_arg f argName

860 elabArgs ist ina failed fc r f ns force args

911 elabArgs ist ina failed fc r f ns force args

@@ -1087,9 +1138,10 @@ runTac :: Bool -> IState -> Name -> PTactic -> ElabD ()

1087runTac autoSolve ist fn tac

1138runTac autoSolve ist fn tac

1088 = do env <- get_env

1139 = do env <- get_env

1089 g <- goal

1140 g <- goal

1141+ let tac' = fmap (addImplBound ist (map fst env)) tac

1090 if autoSolve

1142 if autoSolve

1091− then runT (fmap (addImplBound ist (map fst env)) tac)

1143+ then runT tac'

1092− else no_errors (runT (fmap (addImplBound ist (map fst env)) tac))

1144+ else no_errors (runT tac')

1093 (Just (CantSolveGoal g (map (\(n, b) -> (n, binderTy b)) env)))

1145 (Just (CantSolveGoal g (map (\(n, b) -> (n, binderTy b)) env)))

1094 where

1146 where

1095 runT (Intro []) = do g <- goal

1147 runT (Intro []) = do g <- goal

src/Idris/IBC.hs+10−6

@@ -31,7 +31,7 @@ import Codec.Compression.Zlib (compress)

31import Util.Zlib (decompressEither)

32

33ibcVersion :: Word8

34−ibcVersion = 74

34+ibcVersion = 75

35

36data IBCFile = IBCFile { ver :: Word8,

37 sourcefile :: FilePath,

@@ -1406,10 +1406,12 @@ instance Binary PTerm where

1406 put x2

1407 PResolveTC x1 -> do putWord8 15

1408 put x1

1409− PEq x1 x2 x3 -> do putWord8 16

1409+ PEq x1 x2 x3 x4 x5 -> do putWord8 16

1410− put x1

1410+ put x1

1411− put x2

1411+ put x2

1412− put x3

1412+ put x3

1413+ put x4

1414+ put x5

1413 PRewrite x1 x2 x3 x4 -> do putWord8 17

1415 PRewrite x1 x2 x3 x4 -> do putWord8 17

1414 put x1

1416 put x1

1415 put x2

1417 put x2

@@ -1523,7 +1525,9 @@ instance Binary PTerm where

1523 16 -> do x1 <- get

1525 16 -> do x1 <- get

1524 x2 <- get

1526 x2 <- get

1525 x3 <- get

1527 x3 <- get

1528+ x4 <- get

1529+ x5 <- get

1526− return (PEq x1 x2 x3)

1530+ return (PEq x1 x2 x3 x4 x5)

1527 17 -> do x1 <- get

1531 17 -> do x1 <- get

1528 x2 <- get

1532 x2 <- get

1529 x3 <- get

1533 x3 <- get

src/Idris/IdrisDoc.hs+1−1

@@ -285,7 +285,7 @@ extractPTermNames (PMatchApp _ n) = [n]

285extractPTermNames (PCase _ p ps) = let (ps1, ps2) = unzip ps

286 in concatMap extract (p:(ps1 ++ ps2))

287extractPTermNames (PRefl _ p) = extract p

288−extractPTermNames (PEq _ p1 p2) = concatMap extract [p1, p2]

288+extractPTermNames (PEq _ _ _ p1 p2) = concatMap extract [p1, p2]

289extractPTermNames (PRewrite _ a b m) | Just c <- m =

290 concatMap extract [a, b, c]

291extractPTermNames (PRewrite _ a b _) = concatMap extract [a, b]

src/Idris/Interactive.hs+15−9

@@ -27,6 +27,7 @@ import System.IO

27import Data.Char

28import Data.Maybe (fromMaybe)

29

30+import Debug.Trace

30

31

31caseSplitAt :: Handle -> FilePath -> Bool -> Int -> Name -> Idris ()

32caseSplitAt :: Handle -> FilePath -> Bool -> Int -> Name -> Idris ()

32caseSplitAt h fn updatefile l n

33caseSplitAt h fn updatefile l n

@@ -248,12 +249,15 @@ makeLemma h fn updatefile l n

248 [] -> ierror (NoSuchVariable n)

249 [] -> ierror (NoSuchVariable n)

249 ns -> ierror (CantResolveAlts (map fst ns))

250 ns -> ierror (CantResolveAlts (map fst ns))

250 i <- getIState

251 i <- getIState

252+ margs <- case lookup n (idris_metavars i) of

253+ Just (_, arity, _) -> return arity

254+ _ -> return (-1)

251

255

252 if (not isProv) then do

256 if (not isProv) then do

253 let skip = guessImps (tt_ctxt i) mty

257 let skip = guessImps (tt_ctxt i) mty

254

258

255 let lem = show n ++ " : " ++ show (stripMNBind skip (delab i mty))

259 let lem = show n ++ " : " ++ show (stripMNBind skip (delab i mty))

256− let lem_app = show n ++ appArgs skip mty

260+ let lem_app = show n ++ appArgs skip margs mty

257

261

258 if updatefile then

262 if updatefile then

259 do let fb = fn ++ "~"

263 do let fb = fn ++ "~"

@@ -271,7 +275,7 @@ makeLemma h fn updatefile l n

271 in runIO . hPutStrLn h $ convSExp "return" good n

275 in runIO . hPutStrLn h $ convSExp "return" good n

272

276

273 else do -- provisional definition

277 else do -- provisional definition

274− let lem_app = show n ++ appArgs [] mty ++

278+ let lem_app = show n ++ appArgs [] (-1) mty ++

275 " = ?" ++ show n ++ "_rhs"

279 " = ?" ++ show n ++ "_rhs"

276 if updatefile then

280 if updatefile then

277 do let fb = fn ++ "~"

281 do let fb = fn ++ "~"

@@ -288,15 +292,17 @@ makeLemma h fn updatefile l n

288

292

289 where getIndent s = length (takeWhile isSpace s)

293 where getIndent s = length (takeWhile isSpace s)

290

294

291− appArgs skip (Bind n@(UN c) (Pi _) sc)

295+ appArgs skip 0 _ = ""

296+ appArgs skip i (Bind n@(UN c) (Pi _) sc)

292− | thead c /= '_' && n `notElem` skip

297+ | (thead c /= '_' && n `notElem` skip)

293− = " " ++ show n ++ appArgs skip sc

298+ = " " ++ show n ++ appArgs skip (i - 1) sc

294− appArgs skip (Bind _ (Pi _) sc) = appArgs skip sc

299+ appArgs skip i (Bind _ (Pi _) sc) = appArgs skip (i - 1) sc

295− appArgs skip _ = ""

300+ appArgs skip i _ = ""

296

301

297 stripMNBind skip (PPi b n@(UN c) ty sc)

302 stripMNBind skip (PPi b n@(UN c) ty sc)

298− | thead c /= '_' &&

303+ | (thead c /= '_' && n `notElem` skip) ||

304+ take 4 (str c) == "__pi" -- keep in type, but not in app

299− n `notElem` skip = PPi b n ty (stripMNBind skip sc)

305+ = PPi b n ty (stripMNBind skip sc)

300 stripMNBind skip (PPi b _ ty sc) = stripMNBind skip sc

306 stripMNBind skip (PPi b _ ty sc) = stripMNBind skip sc

301 stripMNBind skip t = t

307 stripMNBind skip t = t

302

308

src/Idris/Output.hs+12−1

@@ -78,6 +78,17 @@ ihPrintFunTypes h bnd n overloads = do ist <- getIState

78 ppOverload ppo infixes n tm =

79 fullName n <+> colon <+> align (pprintPTerm ppo bnd [] infixes tm)

80

81+ihRenderOutput :: Handle -> Doc OutputAnnotation -> Idris ()

82+ihRenderOutput h doc =

83+ do i <- getIState

84+ case idris_outputmode i of

85+ RawOutput -> do out <- iRender doc

86+ runIO $ putStrLn (displayDecorated (consoleDecorate i) out)

87+ IdeSlave n ->

88+ do (str, spans) <- fmap displaySpans . iRender . fmap (fancifyAnnots i) $ doc

89+ let out = [toSExp str, toSExp spans]

90+ runIO . putStrLn $ convSExp "write-decorated" out n

91+

81ihRenderResult :: Handle -> Doc OutputAnnotation -> Idris ()

92ihRenderResult :: Handle -> Doc OutputAnnotation -> Idris ()

82ihRenderResult h d = do ist <- getIState

93ihRenderResult h d = do ist <- getIState

83 case idris_outputmode ist of

94 case idris_outputmode ist of

@@ -85,7 +96,7 @@ ihRenderResult h d = do ist <- getIState

85 IdeSlave n -> ideSlaveReturnAnnotated n h d

96 IdeSlave n -> ideSlaveReturnAnnotated n h d

86

97

87ideSlaveReturnWithStatus :: String -> Integer -> Handle -> Doc OutputAnnotation -> Idris ()

98ideSlaveReturnWithStatus :: String -> Integer -> Handle -> Doc OutputAnnotation -> Idris ()

88−ideSlaveReturnWithStatus status n h out = do

99+ideSlaveReturnWithStatus status n h out = do

89 ist <- getIState

100 ist <- getIState

90 (str, spans) <- fmap displaySpans .

101 (str, spans) <- fmap displaySpans .

91 iRender .

102 iRender .

src/Idris/ParseExpr.hs+33−15

@@ -780,23 +780,26 @@ TypeSig' ::=

780@

781 -}

782let_ :: SyntaxInfo -> IdrisParser PTerm

783−let_ syn = try (do reserved "let"; fc <- getFC; n <- name;

783+let_ syn = try (do reserved "let"

784− ty <- option Placeholder (do lchar ':'; expr' syn)

784+ ls <- indentedBlock (let_binding syn)

785− lchar '='

786− v <- expr syn

787− ts <- option [] (do lchar '|'

788− sepBy1 (do_alt syn) (lchar '|'))

789 reserved "in"; sc <- expr syn

785 reserved "in"; sc <- expr syn

790− case ts of

786+ return (buildLets ls sc))

791− [] -> return (PLet n ty v sc)

792− alts -> return (PCase fc v ((PRef fc n, sc) : ts)))

793− <|> (do reserved "let"; fc <- getFC; pat <- expr' (syn { inPattern = True } )

794− symbol "="; v <- expr syn

795− ts <- option [] (do lchar '|'

796− sepBy1 (do_alt syn) (lchar '|'))

797− reserved "in"; sc <- expr syn

798− return (PCase fc v ((pat, sc) : ts)))

799 <?> "let binding"

787 <?> "let binding"

788+ where buildLets [] sc = sc

789+ buildLets ((fc,PRef _ n,ty,v,[]):ls) sc

790+ = PLet n ty v (buildLets ls sc)

791+ buildLets ((fc,pat,ty,v,alts):ls) sc

792+ = PCase fc v ((pat, buildLets ls sc) : alts)

793+

794+let_binding syn = do fc <- getFC;

795+ pat <- expr' (syn { inPattern = True })

796+ ty <- option Placeholder (do lchar ':'; expr' syn)

797+ lchar '='

798+ v <- expr syn

799+ ts <- option [] (do lchar '|'

800+ sepBy1 (do_alt syn) (lchar '|'))

801+ return (fc,pat,ty,v,ts)

802+

800

803

801{- | Parses a quote goal

804{- | Parses a quote goal

802

805

@@ -1285,6 +1288,21 @@ tactic syn = do reserved "intro"; ns <- sepBy (indentPropHolds gtProp *> name) (

1285 t <- (indentPropHolds gtProp *> expr syn);

1288 t <- (indentPropHolds gtProp *> expr syn);

1286 i <- get

1289 i <- get

1287 return $ TCheck (desugar syn i t))

1290 return $ TCheck (desugar syn i t))

1291+ <|> try (do reserved "doc"

1292+ whiteSpace

1293+ c <- constant

1294+ eof

1295+ return (TDocStr (Right c)))

1296+ <|> try (do reserved "doc"

1297+ whiteSpace

1298+ n <- (fnName <|> (string "_|_" >> return falseTy))

1299+ eof

1300+ return (TDocStr (Left n)))

1301+ <|> try (do reserved "search"

1302+ whiteSpace

1303+ t <- (indentPropHolds gtProp *> expr syn);

1304+ i <- get

1305+ return $ TSearch (desugar syn i t))

1288 <?> "prover command")

1306 <?> "prover command")

1289 <?> "tactic"

1307 <?> "tactic"

1290 where

1308 where

src/Idris/ParseHelpers.hs+4−2

@@ -439,7 +439,8 @@ closeBlock = do ist <- get

439 Nothing : xs -> lchar '}' >> return xs <?> "end of block"

440 Just lvl : xs -> (do i <- indent

441 isParen <- lookAheadMatches (char ')')

442+ isIn <- lookAheadMatches (reserved "in")

442− if i >= lvl && not isParen

443+ if i >= lvl && not (isParen || isIn)

443 then fail "not end of block"

444 then fail "not end of block"

444 else return xs)

445 else return xs)

445 <|> (do notOpenBraces

446 <|> (do notOpenBraces

@@ -462,7 +463,8 @@ keepTerminator = do lchar ';'; return ()

462 <|> do c <- indent; l <- lastIndent

463 <|> do c <- indent; l <- lastIndent

463 unless (c <= l) $ fail "not a terminator"

464 unless (c <= l) $ fail "not a terminator"

464 <|> do isParen <- lookAheadMatches (oneOf ")}|")

465 <|> do isParen <- lookAheadMatches (oneOf ")}|")

466+ isIn <- lookAheadMatches (reserved "in")

465− unless isParen $ fail "not a terminator"

467+ unless (isIn || isParen) $ fail "not a terminator"

466 <|> lookAhead eof

468 <|> lookAhead eof

467

469

468-- | Checks if application expression does not end

470-- | Checks if application expression does not end

src/Idris/ParseOps.hs+1−1

@@ -38,7 +38,7 @@ table fixes

38 ++ toTable (reverse fixes) ++

39 [[backtick],

40 [binary "$" (\fc x y -> flatten $ PApp fc x [pexp y]) AssocRight],

41− [binary "=" PEq AssocLeft]]

41+ [binary "=" (\fc x y -> PEq fc Placeholder Placeholder x y) AssocLeft]]

42 where

43 flatten :: PTerm -> PTerm -- flatten application

44 flatten (PApp fc (PApp _ f as) bs) = flatten (PApp fc f (as ++ bs))

src/Idris/Parser.hs+3−1

@@ -739,7 +739,9 @@ rhs syn n = do lchar '='; expr syn

739 <|> do reserved "impossible"; return PImpossible

740 <?> "function right hand side"

741 where mkN :: Name -> Name

742+ mkN (UN x) = if (tnull x || not (isAlpha (thead x)))

743+ then sUN "infix_op_lemma_1"

742− mkN (UN x) = sUN (str x++"_lemma_1")

744+ else sUN (str x++"_lemma_1")

743 mkN (NS x n) = NS (mkN x) n

745 mkN (NS x n) = NS (mkN x) n

744 n' :: Name

746 n' :: Name

745 n' = mkN n

747 n' = mkN n

src/Idris/Prover.hs+45−19

@@ -9,6 +9,7 @@ import Idris.Core.Typecheck

9import Idris.AbsSyntax

10import Idris.AbsSyntaxTree

11import Idris.Delaborate

12+import Idris.Docs (getDocs, pprintDocs, pprintConstDocs)

12import Idris.ElabDecls

13import Idris.ElabDecls

13import Idris.ElabTerm

14import Idris.ElabTerm

14import Idris.Parser hiding (params)

15import Idris.Parser hiding (params)

@@ -17,6 +18,7 @@ import Idris.DataOpts

17import Idris.Completion

18import Idris.Completion

18import Idris.IdeSlave

19import Idris.IdeSlave

19import Idris.Output

20import Idris.Output

21+import Idris.TypeSearch (searchByType)

20

22

21import Text.Trifecta.Result(Result(..))

23import Text.Trifecta.Result(Result(..))

22

24

@@ -98,6 +100,8 @@ elabStep st e = case runStateT eCheck st of

98 OK (a, st') -> return (a, st')

100 OK (a, st') -> return (a, st')

99 Error a -> ierror a

101 Error a -> ierror a

100 where eCheck = do res <- e

102 where eCheck = do res <- e

103+ matchProblems True

104+ unifyProblems

101 probs' <- get_probs

105 probs' <- get_probs

102 case probs' of

106 case probs' of

103 [] -> do tm <- get_term

107 [] -> do tm <- get_term

@@ -180,6 +184,8 @@ receiveInput e =

180 ideslavePutSExp "return" good

184 ideslavePutSExp "return" good

181 receiveInput e

185 receiveInput e

182 Just (Interpret cmd) -> return (Just cmd)

186 Just (Interpret cmd) -> return (Just cmd)

187+ Just (TypeOf str) -> return (Just (":t " ++ str))

188+ Just (DocsFor str) -> return (Just (":doc " ++ str))

183 _ -> return Nothing

189 _ -> return Nothing

184

190

185ploop :: Name -> Bool -> String -> [String] -> ElabState [PDecl] -> Maybe History -> Idris (Term, [String])

191ploop :: Name -> Bool -> String -> [String] -> ElabState [PDecl] -> Maybe History -> Idris (Term, [String])

@@ -211,21 +217,23 @@ ploop fn d prompt prf e h

211 (case cmd of

217 (case cmd of

212 Failure err -> return (False, e, False, prf, Left . Msg . show . fixColour (idris_colourRepl i) $ err)

218 Failure err -> return (False, e, False, prf, Left . Msg . show . fixColour (idris_colourRepl i) $ err)

213 Success Undo -> do (_, st) <- elabStep e loadState

219 Success Undo -> do (_, st) <- elabStep e loadState

214− return (True, st, False, init prf, Right "")

220+ return (True, st, False, init prf, Right $ iPrintResult "")

215− Success ProofState -> return (True, e, False, prf, Right "")

221+ Success ProofState -> return (True, e, False, prf, Right $ iPrintResult "")

216 Success ProofTerm -> do tm <- lifte e get_term

222 Success ProofTerm -> do tm <- lifte e get_term

217 iputStrLn $ "TT: " ++ show tm ++ "\n"

223 iputStrLn $ "TT: " ++ show tm ++ "\n"

218− return (False, e, False, prf, Right "")

224+ return (False, e, False, prf, Right $ iPrintResult "")

219 Success Qed -> do hs <- lifte e get_holes

225 Success Qed -> do hs <- lifte e get_holes

220 when (not (null hs)) $ ifail "Incomplete proof"

226 when (not (null hs)) $ ifail "Incomplete proof"

221 iputStrLn "Proof completed!"

227 iputStrLn "Proof completed!"

222− return (False, e, True, prf, Right "")

228+ return (False, e, True, prf, Right $ iPrintResult "")

223 Success (TCheck (PRef _ n)) -> checkNameType n

229 Success (TCheck (PRef _ n)) -> checkNameType n

224 Success (TCheck t) -> checkType t

230 Success (TCheck t) -> checkType t

225 Success (TEval t) -> evalTerm t e

231 Success (TEval t) -> evalTerm t e

232+ Success (TDocStr x) -> docStr x

233+ Success (TSearch t) -> search t

226 Success tac -> do (_, e) <- elabStep e saveState

234 Success tac -> do (_, e) <- elabStep e saveState

227 (_, st) <- elabStep e (runTac autoSolve i fn tac)

235 (_, st) <- elabStep e (runTac autoSolve i fn tac)

228− return (True, st, False, prf ++ [step], Right ""))

236+ return (True, st, False, prf ++ [step], Right $ iPrintResult ""))

229 (\err -> return (False, e, False, prf, Left err))

237 (\err -> return (False, e, False, prf, Left err))

230 ideslavePutSExp "write-proof-state" (prf', length prf')

238 ideslavePutSExp "write-proof-state" (prf', length prf')

231 case res of

239 case res of

@@ -234,7 +242,7 @@ ploop fn d prompt prf e h

234 Right ok ->

242 Right ok ->

235 if done then do (tm, _) <- elabStep st get_term

243 if done then do (tm, _) <- elabStep st get_term

236 return (tm, prf')

244 return (tm, prf')

237− else do iPrintResult ok

245+ else do ok

238 ploop fn d prompt prf' st h'

246 ploop fn d prompt prf' st h'

239 where envCtxt env ctxt = foldl (\c (n, b) -> addTyDecl n Bound (binderTy b) c) ctxt env

247 where envCtxt env ctxt = foldl (\c (n, b) -> addTyDecl n Bound (binderTy b) c) ctxt env

240 checkNameType n = do

248 checkNameType n = do

@@ -250,11 +258,11 @@ ploop fn d prompt prf e h

250 putIState ist'

258 putIState ist'

251 -- Unlike the REPL, metavars have no special treatment, to

259 -- Unlike the REPL, metavars have no special treatment, to

252 -- make it easier to see how to prove with them.

260 -- make it easier to see how to prove with them.

253− case lookupNames n ctxt' of

261+ let action = case lookupNames n ctxt' of

254− [] -> ihPrintError h $ "No such variable " ++ show n

262+ [] -> ihPrintError h $ "No such variable " ++ show n

255− ts -> ihPrintFunTypes h bnd n (map (\n -> (n, delabTy ist' n)) ts)

263+ ts -> ihPrintFunTypes h bnd n (map (\n -> (n, delabTy ist' n)) ts)

256 putIState ist

264 putIState ist

257− return (False, e, False, prf, Right ""))

265+ return (False, e, False, prf, Right action))

258 (\err -> do putIState ist ; ierror err)

266 (\err -> do putIState ist ; ierror err)

259

267

260 checkType t = do

268 checkType t = do

@@ -269,14 +277,14 @@ ploop fn d prompt prf e h

269 ty' = normaliseC ctxt [] ty

277 ty' = normaliseC ctxt [] ty

270 h = idris_outh ist

278 h = idris_outh ist

271 infixes = idris_infixes ist

279 infixes = idris_infixes ist

272− case tm of

280+ action = case tm of

273− TType _ ->

281+ TType _ ->

274− ihPrintTermWithType h (prettyImp ppo PType) type1Doc

282+ ihPrintTermWithType h (prettyImp ppo PType) type1Doc

275− _ -> let bnd = map (\x -> (fst x, False)) env in

283+ _ -> let bnd = map (\x -> (fst x, False)) env in

276− ihPrintTermWithType h (pprintPTerm ppo bnd [] infixes (delab ist tm))

284+ ihPrintTermWithType h (pprintPTerm ppo bnd [] infixes (delab ist tm))

277− (pprintPTerm ppo bnd [] infixes (delab ist ty))

285+ (pprintPTerm ppo bnd [] infixes (delab ist ty))

278 putIState ist

286 putIState ist

279− return (False, e, False, prf, Right ""))

287+ return (False, e, False, prf, Right action))

280 (\err -> do putIState ist { tt_ctxt = ctxt } ; ierror err)

288 (\err -> do putIState ist { tt_ctxt = ctxt } ; ierror err)

281

289

282 evalTerm t e = withErrorReflection $

290 evalTerm t e = withErrorReflection $

@@ -295,7 +303,25 @@ ploop fn d prompt prf e h

295 infixes = idris_infixes ist

303 infixes = idris_infixes ist

296 tmDoc = pprintPTerm ppo bnd [] infixes (delab ist' tm')

304 tmDoc = pprintPTerm ppo bnd [] infixes (delab ist' tm')

297 tyDoc = pprintPTerm ppo bnd [] infixes (delab ist' ty')

305 tyDoc = pprintPTerm ppo bnd [] infixes (delab ist' ty')

298− ihPrintTermWithType (idris_outh ist') tmDoc tyDoc

306+ action = ihPrintTermWithType (idris_outh ist') tmDoc tyDoc

299 putIState ist

307 putIState ist

300− return (False, e, False, prf, Right ""))

308+ return (False, e, False, prf, Right action))

301 (\err -> do putIState ist ; ierror err)

309 (\err -> do putIState ist ; ierror err)

310+ docStr :: Either Name Const -> Idris (Bool, ElabState [PDecl], Bool, [String], Either Err (Idris ()))

311+ docStr (Left n) = do ist <- getIState

312+ let h = idris_outh ist

313+ idrisCatch (case lookupCtxtName n (idris_docstrings ist) of

314+ [] -> return (False, e, False, prf,

315+ Left . Msg $ "No documentation for " ++ show n)

316+ ns -> do toShow <- mapM (showDoc ist) ns

317+ return (False, e, False, prf,

318+ Right $ ihRenderResult h (vsep toShow)))

319+ (\err -> do putIState ist ; ierror err)

320+ where showDoc ist (n, d) = do doc <- getDocs n

321+ return $ pprintDocs ist doc

322+ docStr (Right c) = do ist <- getIState

323+ let h = idris_outh ist

324+ return (False, e, False, prf, Right . ihRenderResult h $ pprintConstDocs ist c (constDocs c))

325+ search t = do ist <- getIState

326+ let h = idris_outh ist

327+ return (False, e, False, prf, Right $ searchByType h t)

src/Idris/REPL.hs+2

@@ -473,6 +473,8 @@ ideslaveProcess fn Help = process stdout fn Help

473ideslaveProcess fn (ChangeDirectory f) = do process stdout fn (ChangeDirectory f)

474 iPrintResult "changed directory to"

475ideslaveProcess fn (Eval t) = process stdout fn (Eval t)

476+ideslaveProcess fn (NewDefn decls) = do process stdout fn (NewDefn decls)

477+ iPrintResult "defined"

476ideslaveProcess fn (ExecVal t) = process stdout fn (ExecVal t)

478ideslaveProcess fn (ExecVal t) = process stdout fn (ExecVal t)

477ideslaveProcess fn (Check (PRef x n)) = process stdout fn (Check (PRef x n))

479ideslaveProcess fn (Check (PRef x n)) = process stdout fn (Check (PRef x n))

478ideslaveProcess fn (Check t) = process stdout fn (Check t)

480ideslaveProcess fn (Check t) = process stdout fn (Check t)

src/Idris/TypeSearch.hs+11−8

@@ -20,20 +20,20 @@ import qualified Data.Set as S

20import qualified Data.Text as T (pack, isPrefixOf)

21

22import Idris.AbsSyntax (addUsingConstraints, addImpl, getContext, getIState, putIState, implicit)

23−import Idris.AbsSyntaxTree (class_instances, ClassInfo, defaultSyntax, Idris,

23+import Idris.AbsSyntaxTree (class_instances, ClassInfo, defaultSyntax, Idris,

24− IState (idris_classes, idris_docstrings, tt_ctxt),

24+ IState (idris_classes, idris_docstrings, tt_ctxt, idris_outputmode),

25− implicitAllowed, prettyDocumentedIst, prettyIst, PTerm, toplevel)

25+ implicitAllowed, OutputMode(..), prettyDocumentedIst, prettyIst, PTerm, toplevel)

26import Idris.Core.Evaluate (Context (definitions), Def (Function, TyDecl, CaseOp), normaliseC)

27import Idris.Core.TT hiding (score)

28import Idris.Core.Unify (match_unify)

29import Idris.Delaborate (delabTy)

30import Idris.Docstrings (noDocs, overview)

31import Idris.ElabDecls (elabType')

32−import Idris.Output (ihRenderResult)

32+import Idris.Output (ihRenderOutput, ihPrintResult, ihRenderResult)

33

34import System.IO (Handle)

35

36−import Util.Pretty (text, char, (<>), Doc)

36+import Util.Pretty (text, char, vsep, (<>), Doc)

37

38searchByType :: Handle -> PTerm -> Idris ()

39searchByType h pterm = do

@@ -49,12 +49,15 @@ searchByType h pterm = do

49 [ let docInfo = (n, delabTy i n, fmap (overview . fst) (lookupCtxtExact n (idris_docstrings i))) in

50 displayScore score <> char ' ' <> prettyDocumentedIst i docInfo

51 | (n, score) <- names']

52+ case idris_outputmode i of

53+ RawOutput -> do mapM_ (ihRenderOutput h) docs

54+ ihPrintResult h ""

52− mapM_ (ihRenderResult h) docs

55+ IdeSlave n -> ihRenderResult h (vsep docs)

53− where

56+ where

54 numLimit = 50

57 numLimit = 50

55 syn = defaultSyntax { implicitAllowed = True } -- syntax

58 syn = defaultSyntax { implicitAllowed = True } -- syntax

56 n = sMN 0 "searchType" -- name

59 n = sMN 0 "searchType" -- name

57−

60+

58-- | Conduct a type-directed search using a given match predicate

61-- | Conduct a type-directed search using a given match predicate

59searchUsing :: (IState -> Type -> [(Name, Type)] -> [(Name, a)])

62searchUsing :: (IState -> Type -> [(Name, Type)] -> [(Name, a)])

60 -> IState -> Type -> [(Name, a)]

63 -> IState -> Type -> [(Name, a)]

test/basic009/expected+1−1

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

1MAIN-PASS

2Faulty.idr:6:7:When elaborating type of Faulty.fault:

3−When elaborating an application of type constructor =:

3+When elaborating argument x to type constructor =:

4 Can't disambiguate name: A.num, B.C.num

5Multiple.idr:3:1:import alias not unique: "X"

test/effects001/test021.idr+1−1

@@ -9,7 +9,7 @@ data Count : Type where

9

10FileIO : Type -> Type -> Type

11FileIO st t

12− = { [FILE_IO st, STDIO, Count ::: STATE Int] } Eff IO t

12+ = { [FILE_IO st, STDIO, Count ::: STATE Int] } Eff t

13

14readFile : FileIO (OpenFile Read) (List String)

15readFile = readAcc [] where

test/effects001/test021a.idr+1−1

@@ -17,7 +17,7 @@ Env = List (String, Integer)

17-- Evaluator t

18-- = Eff m [EXCEPTION String, RND, STATE Env] t

19

20−eval : Expr -> { [EXCEPTION String, STDIO, RND, STATE Env] } Eff IO Integer

20+eval : Expr -> { [EXCEPTION String, STDIO, RND, STATE Env] } Eff Integer

21eval (Var x) = do vs <- get

22 case lookup x vs of

23 Nothing => raise ("No such variable " ++ x)

test/effects002/test025.idr+1−1

@@ -6,7 +6,7 @@ import Control.IOExcept

6

7MemoryIO : Type -> Type -> Type -> Type

8MemoryIO td ts r = { [ Dst ::: RAW_MEMORY td

9− , Src ::: RAW_MEMORY ts ] } Eff (IOExcept String) r

9+ , Src ::: RAW_MEMORY ts ] } Eff r

10

11inpVect : Vect 5 Bits8

12inpVect = map prim__truncInt_B8 [0, 1, 2, 3, 5]

test/error003/ErrorReflection.idr+1−1

@@ -58,7 +58,7 @@ dslerr (CantUnify _ tm1 tm2 _ _ _) = do tm1' <- getTmTy tm1

58 tm2' <- getTmTy tm2

59 ty1 <- reifyTy tm1'

60 ty2 <- reifyTy tm2'

61− return [TextPart $ "DSL type error: " ++ (show ty1) ++ " doesn't match " ++(show ty2)]

61+ Just [TextPart $ "DSL type error: " ++ (show ty1) ++ " doesn't match " ++(show ty2)]

62dslerr _ = Nothing

63

64

test/proof002/expected+1−1

@@ -1,7 +1,7 @@

1Reflect.idr:207:38:When elaborating right hand side of testReflect1:

2When elaborating an application of function Reflect.getJust:

3 Can't unify

4− IsJust (Just x)

4+ IsJust (Just x2)

5 with

6 IsJust (prove (getProof x))

7

test/quasiquote001/QuasiquoteBasics.idr+4−8

@@ -13,22 +13,18 @@ twoElems : TT

13twoElems = `(with List [(), ()])

14

15copy : TT -> TT

16−copy q = `((~q,~q))

16+copy q = `((~q,~q) : (Type, Type))

17

18thing : TT -> TT

19thing tm = `(with List [Type, ~tm])

20

21−getTyArg : TT -> Maybe TT

22−getTyArg `(~f ~x) = Just x

23−getTyArg _ = Nothing

24−

25

21

26

22

27

23

28namespace Main

24namespace Main

29 main : IO ()

25 main : IO ()

30− main = do putStrLn . show $ thing (copy nat)

26+ main = do putStrLn . show $ twoElems

31 putStrLn "--------------"

27 putStrLn "--------------"

32− putStrLn . show $ getTyArg nat

28+ putStrLn . show . thing $ copy nat

33 putStrLn "--------------"

29 putStrLn "--------------"

34− putStrLn . show $ getTyArg (twoElems)

30+ putStrLn . show . copy . copy $ `(Type)

test/quasiquote001/expected+3−3

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

1−(App (App (App (P (DCon 1 3) (NS (UN ::) ["List", "Prelude"]) (Bind (UN a) (Pi (TType (UVar -1))) (Bind (MN 0 "_t") (Pi (V 0)) (Bind (MN 2 "_t") (Pi (App (P (TCon 0 0) (NS (UN List) ["List", "Prelude"]) Erased) (V 1))) (App (P (TCon 0 0) (NS (UN List) ["List", "Prelude"]) Erased) (V 2)))))) (TType (UVal 0))) (TType (UVal 0))) (App (App (App (P (DCon 1 3) (NS (UN ::) ["List", "Prelude"]) (Bind (UN a) (Pi (TType (UVar -1))) (Bind (MN 0 "_t") (Pi (V 0)) (Bind (MN 2 "_t") (Pi (App (P (TCon 0 0) (NS (UN List) ["List", "Prelude"]) Erased) (V 1))) (App (P (TCon 0 0) (NS (UN List) ["List", "Prelude"]) Erased) (V 2)))))) (TType (UVal 0))) (App (App (App (App (P (DCon 0 4) (MN 0 "__MkPair") (Bind (MN 0 "A") (Pi (TType (UVar 36))) (Bind (MN 0 "B") (Pi (TType (UVar 38))) (Bind (MN 0 "a") (Pi (V 1)) (Bind (MN 0 "b") (Pi (V 1)) (App (App (P (TCon 0 0) (MN 0 "__Pair") (Bind (MN 1 "A") (Pi (TType (UVar 28))) (Bind (MN 1 "B") (Pi (TType (UVar 30))) (TType (UVar 32))))) (V 3)) (V 2))))))) (P Bound (MN 106 "A") (TType (UVal 0)))) (P Bound (MN 107 "B") (TType (UVal 0)))) (P (TCon 15 0) (NS (UN Nat) ["Nat", "Prelude"]) (TType (UVar -1)))) (P (TCon 15 0) (NS (UN Nat) ["Nat", "Prelude"]) (TType (UVar -1))))) (App (P (DCon 0 1) (NS (UN Nil) ["List", "Prelude"]) (Bind (UN a) (Pi (TType (UVar -1))) (App (P (TCon 0 0) (NS (UN List) ["List", "Prelude"]) Erased) (V 0)))) (TType (UVal 0)))))

1+(App (App (App (P (DCon 1 3) (NS (UN ::) ["List", "Prelude"]) (Bind (UN a) (Pi (TType (UVar -1))) (Bind (MN 0 "_t") (Pi (V 0)) (Bind (MN 2 "_t") (Pi (App (P (TCon 0 0) (NS (UN List) ["List", "Prelude"]) Erased) (V 1))) (App (P (TCon 0 0) (NS (UN List) ["List", "Prelude"]) Erased) (V 2)))))) (P (TCon 7 0) (MN 0 "__Unit") (TType (UVar 6)))) (P (DCon 0 0) (MN 0 "__II") (P (TCon 0 0) (MN 0 "__Unit") (TType (UVar 6))))) (App (App (App (P (DCon 1 3) (NS (UN ::) ["List", "Prelude"]) (Bind (UN a) (Pi (TType (UVar -1))) (Bind (MN 0 "_t") (Pi (V 0)) (Bind (MN 2 "_t") (Pi (App (P (TCon 0 0) (NS (UN List) ["List", "Prelude"]) Erased) (V 1))) (App (P (TCon 0 0) (NS (UN List) ["List", "Prelude"]) Erased) (V 2)))))) (P (TCon 7 0) (MN 0 "__Unit") (TType (UVar 6)))) (P (DCon 0 0) (MN 0 "__II") (P (TCon 0 0) (MN 0 "__Unit") (TType (UVar 6))))) (App (P (DCon 0 1) (NS (UN Nil) ["List", "Prelude"]) (Bind (UN a) (Pi (TType (UVar -1))) (App (P (TCon 0 0) (NS (UN List) ["List", "Prelude"]) Erased) (V 0)))) (P (TCon 7 0) (MN 0 "__Unit") (TType (UVar 6))))))

2--------------

3−Nothing

3+(App (App (App (P (DCon 1 3) (NS (UN ::) ["List", "Prelude"]) (Bind (UN a) (Pi (TType (UVar -1))) (Bind (MN 0 "_t") (Pi (V 0)) (Bind (MN 2 "_t") (Pi (App (P (TCon 0 0) (NS (UN List) ["List", "Prelude"]) Erased) (V 1))) (App (P (TCon 0 0) (NS (UN List) ["List", "Prelude"]) Erased) (V 2)))))) (TType (UVar 110))) (TType (UVar 112))) (App (App (App (P (DCon 1 3) (NS (UN ::) ["List", "Prelude"]) (Bind (UN a) (Pi (TType (UVar -1))) (Bind (MN 0 "_t") (Pi (V 0)) (Bind (MN 2 "_t") (Pi (App (P (TCon 0 0) (NS (UN List) ["List", "Prelude"]) Erased) (V 1))) (App (P (TCon 0 0) (NS (UN List) ["List", "Prelude"]) Erased) (V 2)))))) (TType (UVar 114))) (App (App (App (App (P (DCon 0 4) (MN 0 "__MkPair") (Bind (MN 0 "A") (Pi (TType (UVar 36))) (Bind (MN 0 "B") (Pi (TType (UVar 38))) (Bind (MN 0 "a") (Pi (V 1)) (Bind (MN 0 "b") (Pi (V 1)) (App (App (P (TCon 0 0) (MN 0 "__Pair") (Bind (MN 1 "A") (Pi (TType (UVar 28))) (Bind (MN 1 "B") (Pi (TType (UVar 30))) (TType (UVar 32))))) (V 3)) (V 2))))))) (TType (UVar 108))) (TType (UVar 110))) (P (TCon 15 0) (NS (UN Nat) ["Nat", "Prelude"]) (TType (UVar -1)))) (P (TCon 15 0) (NS (UN Nat) ["Nat", "Prelude"]) (TType (UVar -1))))) (App (P (DCon 0 1) (NS (UN Nil) ["List", "Prelude"]) (Bind (UN a) (Pi (TType (UVar -1))) (App (P (TCon 0 0) (NS (UN List) ["List", "Prelude"]) Erased) (V 0)))) (TType (UVar 116)))))

4--------------

5−Just (App (App (App (P (DCon 1 3) (NS (UN ::) ["List", "Prelude"]) (Bind (UN a) (Pi (TType (UVar -1))) (Bind (MN 0 "_t") (Pi (V 0)) (Bind (MN 2 "_t") (Pi (App (P (TCon 0 0) (NS (UN List) ["List", "Prelude"]) Erased) (V 1))) (App (P (TCon 0 0) (NS (UN List) ["List", "Prelude"]) Erased) (V 2)))))) (P (TCon 0 0) (MN 0 "__Unit") (TType (UVar 6)))) (P (DCon 0 0) (MN 0 "__II") (P (TCon 0 0) (MN 0 "__Unit") (TType (UVar 6))))) (App (P (DCon 0 1) (NS (UN Nil) ["List", "Prelude"]) (Bind (UN a) (Pi (TType (UVar -1))) (App (P (TCon 0 0) (NS (UN List) ["List", "Prelude"]) Erased) (V 0)))) (P (TCon 0 0) (MN 0 "__Unit") (TType (UVar 6)))))

5+(App (App (App (App (P (DCon 0 4) (MN 0 "__MkPair") (Bind (MN 0 "A") (Pi (TType (UVar 36))) (Bind (MN 0 "B") (Pi (TType (UVar 38))) (Bind (MN 0 "a") (Pi (V 1)) (Bind (MN 0 "b") (Pi (V 1)) (App (App (P (TCon 0 0) (MN 0 "__Pair") (Bind (MN 1 "A") (Pi (TType (UVar 28))) (Bind (MN 1 "B") (Pi (TType (UVar 30))) (TType (UVar 32))))) (V 3)) (V 2))))))) (TType (UVar 108))) (TType (UVar 110))) (App (App (App (App (P (DCon 0 4) (MN 0 "__MkPair") (Bind (MN 0 "A") (Pi (TType (UVar 36))) (Bind (MN 0 "B") (Pi (TType (UVar 38))) (Bind (MN 0 "a") (Pi (V 1)) (Bind (MN 0 "b") (Pi (V 1)) (App (App (P (TCon 0 0) (MN 0 "__Pair") (Bind (MN 1 "A") (Pi (TType (UVar 28))) (Bind (MN 1 "B") (Pi (TType (UVar 30))) (TType (UVar 32))))) (V 3)) (V 2))))))) (TType (UVar 108))) (TType (UVar 110))) (TType (UVar 110))) (TType (UVar 110)))) (App (App (App (App (P (DCon 0 4) (MN 0 "__MkPair") (Bind (MN 0 "A") (Pi (TType (UVar 36))) (Bind (MN 0 "B") (Pi (TType (UVar 38))) (Bind (MN 0 "a") (Pi (V 1)) (Bind (MN 0 "b") (Pi (V 1)) (App (App (P (TCon 0 0) (MN 0 "__Pair") (Bind (MN 1 "A") (Pi (TType (UVar 28))) (Bind (MN 1 "B") (Pi (TType (UVar 30))) (TType (UVar 32))))) (V 3)) (V 2))))))) (TType (UVar 108))) (TType (UVar 110))) (TType (UVar 110))) (TType (UVar 110))))

test/quasiquote003/NoInfer.idrnew file+10

@@ -0,0 +1,10 @@

1+module NoInfer

2+

3+import Language.Reflection

4+import Language.Reflection.Utils

5+

6+zzz2 : TT

7+zzz2 = `(fZ : Fin 3)

8+

9+zzz : TT

10+zzz = `(fZ)

test/quasiquote003/expectednew file+2

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

1+NoInfer.idr:10:5:When elaborating right hand side of zzz:

2+No such variable k

test/quasiquote003/runnew file+3

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

1+#!/usr/bin/env bash

2+idris $@ --check NoInfer.idr

3+rm -f *.ibc

test/records003/records003.idr−1

@@ -45,4 +45,3 @@ main = do print (record { event->organiser->name } test)

45 print (record { organiser->age } idm_gbg)

46 print (record { year } idm_gbg)

47

48−

test/reg046/expectednew file

No changes to the content.

test/reg046/reg046.idrnew file+19

@@ -0,0 +1,19 @@

1+module test

2+

3+data MyList : (A : Type) -> Type where

4+ nil : (A : Type) -> MyList A

5+ cons : (A : Type) -> A -> MyList A -> MyList A

6+

7+elimList : (A : Type) ->

8+ (m : MyList A -> Type) ->

9+ (f1 : m (nil A)) ->

10+ (f2 : (a : A) -> (as : MyList A) -> m as -> m (cons A a as)) ->

11+ (e : MyList A) ->

12+ m e

13+elimList A m f1 f2 (nil A) = f1

14+elimList A m f1 f2 (cons A a as) = f2 a as (elimList A m f1 f2 as)

15+

16+append : (A : Type) -> (b : MyList A) -> (c : MyList A) -> MyList A

17+append A b c = (elimList A (\ d => MyList A) c

18+ (\ d => \ e => \ f => cons A d f)

19+ b)

test/reg046/runnew file+3

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

1+#!/usr/bin/env bash

2+idris $@ reg046.idr --check

3+rm -f reg046 *.ibc

test/reg047/expectednew file

No changes to the content.

test/reg047/reg047.idrnew file+18

@@ -0,0 +1,18 @@

1+module test

2+

3+data TTSigma : (A : Type) -> (B : A -> Type) -> Type where

4+ sigma : (A : Type) -> (B : A -> Type) -> (a : A) -> B a -> TTSigma A B

5+

6+data Nat = zero | succ Nat

7+

8+Id : (A : Type) -> A -> A -> Type

9+Id A = (=) {a0 = A} {b0 = A}

10+

11+Refl : (A : Type) -> (a : A) -> Id A a a

12+Refl A a = refl {a}

13+

14+zzz : Id Nat zero zero

15+zzz = Refl Nat zero

16+

17+eep : TTSigma Nat (\ a => Id Nat a zero)

18+eep = sigma Nat (\ a => Id Nat a zero) zero zzz

test/reg047/reg047a.idrnew file+24

@@ -0,0 +1,24 @@

1+module test

2+

3+data TTSigma : (A : Type) -> (B : A -> Type) -> Type where

4+ sigma : (A : Type) -> (B : A -> Type) -> (a : A) -> B a -> TTSigma A B

5+

6+data MNat = zero | succ MNat

7+

8+Id : (A : Type) -> A -> A -> Type

9+Id = \A,x,y => x = y -- {a = A} {b = A}

10+

11+Refl : (A : Type) -> (a : A) -> Id A a a

12+Refl A a = refl {a}

13+

14+zzzz : Id MNat zero zero

15+zzzz = Refl MNat zero

16+

17+eep : TTSigma MNat (\ c => Id MNat c zero)

18+eep = (sigma MNat (\b => Id MNat b zero) zero zzzz)

19+

20+eep2 : TTSigma MNat (\ c => Id MNat c zero)

21+eep2 = (sigma MNat (\b => Id MNat b zero) zero (Refl MNat zero))

22+

23+

24+

test/reg047/runnew file+4

@@ -0,0 +1,4 @@

1+#!/usr/bin/env bash

2+idris $@ reg047.idr --check --nobuiltins

3+idris $@ reg047a.idr --check

4+rm -f *.ibc