30f55ce · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Merge remote-tracking branch 'upstream/master' into wip/tactical

30f55ceDavid Raymond Christiansen11 years ago

CHANGELOG+3

compare with master

unifiedsplit

@@ -7,10 +7,13 @@ Language updates

7* Improved unification by implementing a pattern unification rule

8* The syntax `{{n}} quotes n without resolving it, allowing short syntax

9 for defining new names. `{n} still quotes n to an existing name in scope.

10+* A new primitive operator prim__strSubstr for more efficient extraction of

11+ substrings. External code generators should implement this.

10* The previous syntax for tactic proofs and the previous interactive prover

12* The previous syntax for tactic proofs and the previous interactive prover

11 are now deprecated in favour of reflected elaboration. They will be removed

13 are now deprecated in favour of reflected elaboration. They will be removed

12 at some point in the future.

14 at some point in the future.

16+

14Library updates

17Library updates

15---------------

18---------------

CONTRIBUTORS+1

@@ -44,3 +44,4 @@ Dirk Ullrich

44Leif Warner

45Daniel Waterworth

46Jonas Westerlund

47+Sean Hunt

codegen/idris-codegen-c/Main.hs+4−11

@@ -16,21 +16,18 @@ import Paths_idris

17import Util.System

19−data Opts = Opts { really :: Bool,

20− inputs :: [FilePath],

19+data Opts = Opts { inputs :: [FilePath],

21 interface :: Bool,

20 interface :: Bool,

22 output :: FilePath }

21 output :: FilePath }

24showUsage = do putStrLn "A code generator which is intended to be called by the compiler, not by a user."

23showUsage = do putStrLn "A code generator which is intended to be called by the compiler, not by a user."

25− putStrLn "To call the code generator manually, pass the --yes-really option.\n"

26− putStrLn "Usage: idris-codegen-c [--yes-really] <ibc-files> [-o <output-file>]"

24+ putStrLn "Usage: idris-codegen-c <ibc-files> [-o <output-file>]"

27 exitWith ExitSuccess

25 exitWith ExitSuccess

29getOpts :: IO Opts

27getOpts :: IO Opts

30getOpts = do xs <- getArgs

28getOpts = do xs <- getArgs

31− return $ process (Opts False [] False "a.out") xs

29+ return $ process (Opts [] False "a.out") xs

32 where

30 where

33− process opts ("--yes-really":xs) = process (opts { really = True }) xs

34 process opts ("-o":o:xs) = process (opts { output = o }) xs

31 process opts ("-o":o:xs) = process (opts { output = o }) xs

35 process opts ("--interface":xs) = process (opts { interface = True }) xs

32 process opts ("--interface":xs) = process (opts { interface = True }) xs

36 process opts (x:xs) = process (opts { inputs = x:inputs opts }) xs

33 process opts (x:xs) = process (opts { inputs = x:inputs opts }) xs

@@ -50,8 +47,4 @@ main :: IO ()

50main = do opts <- getOpts

47main = do opts <- getOpts

51 if (null (inputs opts))

48 if (null (inputs opts))

52 then showUsage

49 then showUsage

53− else if (not $ really opts)

54− then do putStrLn "This code generator is intended to be called by the Idris compiler. \

55− \Please pass Idris the '--codegen' flag to choose a backend."

56− exitWith ExitSuccess

57− else runMain (c_main opts)

50+ else runMain (c_main opts)

codegen/idris-codegen-javascript/Main.hs+5−11

@@ -13,21 +13,19 @@ import System.Exit

14import Paths_idris

16−data Opts = Opts { really :: Bool

16+data Opts = Opts {

17− , inputs :: [FilePath]

17+ inputs :: [FilePath]

18 , output :: FilePath

19 }

21showUsage = do putStrLn "A code generator which is intended to be called by the compiler, not by a user."

22− putStrLn "To call the code generator manually, pass the --yes-really option.\n"

23− putStrLn "Usage: idris-codegen-c [--yes-really] <ibc-files> [-o <output-file>]"

22+ putStrLn "Usage: idris-codegen-javascript <ibc-files> [-o <output-file>]"

24 exitWith ExitSuccess

23 exitWith ExitSuccess

26getOpts :: IO Opts

25getOpts :: IO Opts

27getOpts = do xs <- getArgs

26getOpts = do xs <- getArgs

28− return $ process (Opts False [] "main.js") xs

27+ return $ process (Opts [] "main.js") xs

29 where

28 where

30− process opts ("--yes-really":xs) = process (opts { really = True }) xs

31 process opts ("-o":o:xs) = process (opts { output = o }) xs

29 process opts ("-o":o:xs) = process (opts { output = o }) xs

32 process opts (x:xs) = process (opts { inputs = x:inputs opts }) xs

30 process opts (x:xs) = process (opts { inputs = x:inputs opts }) xs

33 process opts [] = opts

31 process opts [] = opts

@@ -43,8 +41,4 @@ main :: IO ()

43main = do opts <- getOpts

41main = do opts <- getOpts

44 if (null (inputs opts))

42 if (null (inputs opts))

45 then showUsage

43 then showUsage

46− else if (not $ really opts)

47− then do putStrLn "This code generator is intended to be called by the Idris compiler. \

48− \Please pass Idris the '--codegen' flag to choose a backend."

49− exitWith ExitSuccess

50− else runMain (jsMain opts)

44+ else runMain (jsMain opts)

codegen/idris-codegen-node/Main.hs+4−11

@@ -13,21 +13,18 @@ import System.Exit

14import Paths_idris

16−data Opts = Opts { really :: Bool

17− , inputs :: [FilePath]

16+data Opts = Opts { inputs :: [FilePath]

18 , output :: FilePath

17 , output :: FilePath

19 }

18 }

21showUsage = do putStrLn "A code generator which is intended to be called by the compiler, not by a user."

20showUsage = do putStrLn "A code generator which is intended to be called by the compiler, not by a user."

22− putStrLn "To call the code generator manually, pass the --yes-really option.\n"

23− putStrLn "Usage: idris-codegen-c [--yes-really] <ibc-files> [-o <output-file>]"

21+ putStrLn "Usage: idris-codegen-node <ibc-files> [-o <output-file>]"

24 exitWith ExitSuccess

22 exitWith ExitSuccess

26getOpts :: IO Opts

24getOpts :: IO Opts

27getOpts = do xs <- getArgs

25getOpts = do xs <- getArgs

28− return $ process (Opts False [] "main.js") xs

26+ return $ process (Opts [] "main.js") xs

29 where

27 where

30− process opts ("--yes-really":xs) = process (opts { really = True }) xs

31 process opts ("-o":o:xs) = process (opts { output = o }) xs

28 process opts ("-o":o:xs) = process (opts { output = o }) xs

32 process opts (x:xs) = process (opts { inputs = x:inputs opts }) xs

29 process opts (x:xs) = process (opts { inputs = x:inputs opts }) xs

33 process opts [] = opts

30 process opts [] = opts

@@ -43,8 +40,4 @@ main :: IO ()

43main = do opts <- getOpts

40main = do opts <- getOpts

44 if (null (inputs opts))

41 if (null (inputs opts))

45 then showUsage

42 then showUsage

46− else if (not $ really opts)

47− then do putStrLn "This code generator is intended to be called by the Idris compiler. \

48− \Please pass Idris the '--codegen' flag to choose a backend."

49− exitWith ExitSuccess

50− else runMain (jsMain opts)

43+ else runMain (jsMain opts)

docs/faq/faq.rst+1−1

@@ -74,7 +74,7 @@ Booleans is defined as follows in the library:

74 ifThenElse True t e = t

75 ifThenElse False t e = e

77−The type ``Lazy a`` for ``t`` and ``f`` indicates that those arguments will

77+The type ``Lazy a`` for ``t`` and ``e`` indicates that those arguments will

78only be evaluated if they are used, that is, they are evaluated lazily.

80Evaluation at the REPL doesn't behave as I expect. What's going on?

docs/reference/documenting.rst+1−1

@@ -9,7 +9,7 @@ for a reader’s edification and are ignored by the compiler, and inline

9API documentation, which the compiler parses and stores for future

10reference. To consult the documentation for a declaration ``f``, write

11``:doc f`` at the REPL or use the appropriate command in your editor

12−(``C-c C-d`` in Emacs, in Vim).

12+(``C-c C-d`` in Emacs, ``<LocalLeader>h`` in Vim).

14Comments

15========

docs/reference/syntax-guide.rst+117

@@ -4,6 +4,89 @@ Syntax Guide

5Examples are mostly adapted from the Idris tutorial.

7+Source File Structure

8+---------------------

10+Source files consist of:

11+

12+1. An optional :ref:`syntax-module-headers`.

13+2. Zero or more :ref:`syntax-imports`.

14+3. Zero or more declarations, e.g. :ref:`syntax-variables`,

15+ :ref:`syntax-data-types`, etc.

16+

17+For example:

18+

19+.. code:: idris

20+

21+ module MyModule -- module header

22+

23+ import Data.Vect -- an import

24+

25+ %default total -- a directive

26+

27+ foo : Nat -- a declaration

28+ foo = 5

29+

30+.. _syntax-module-headers:

31+

32+Module Header

33+~~~~~~~~~~~~~

34+

35+A file can start with a module header, introduced by the ``module`` keyword:

36+

37+.. code-block:: idris

38+

39+ module Semantics

40+

41+Module names can be hierarchical, with parts separated by ``.``:

42+

43+.. code-block:: idris

44+

45+ module Semantics.Transform

46+

47+Each file can define only a single module, which includes everything defined in

48+that file.

49+

50+Like with declarations, a :ref:`docstring <syntax-comments>` can be used to

51+provide documentation for a module:

52+

53+.. code-block:: idris

54+

55+ ||| Implementation of predicate transformer semantics.

56+ module Semantics.Transform

57+

58+.. _syntax-imports:

59+

60+Imports

61+~~~~~~~

62+

63+An ``import`` makes the names in another module available for use by the current

64+module:

65+

66+.. code-block:: idris

67+

68+ import Data.Vect

69+

70+All the declarations in an imported module are available for use in the file.

71+In a case where a name is ambiguous --- e.g. because it is imported from

72+multiple modules, or appears in multiple visible namespaces --- the ambiguity can be resolved using :ref:`syntax-qualified-names`. (Often, the compiler can

73+resolve the ambiguity for you, using the types involved.)

74+

75+Imported modules can be given aliases to make qualified names more compact:

76+

77+.. code-block:: idris

78+

79+ import Data.Vect as V

80+

81+Note that names made visible by import are not, by default, re-exported to

82+users of the module being written. This can be done using ``import public``:

83+

84+.. code-block:: idris

85+

86+ import public Data.Vect

87+

88+.. _syntax-variables:

89+

7Variables

90Variables

8---------

91---------

@@ -43,6 +126,8 @@ a more interesting example:

43 MyListType : Type

126 MyListType : Type

44 MyListType = List Int

127 MyListType = List Int

128

129+.. _syntax-data-types:

130+

46Data types

131Data types

47~~~~~~~~~~

132~~~~~~~~~~

133

@@ -246,6 +331,36 @@ Options

246Misc

331Misc

247----

332----

248

333

334+.. _syntax-qualified-names:

335+

336+Qualified Names

337+~~~~~~~~~~~~~~~

338+

339+If multiple declarations with the same name are visible, using the name can

340+result in an ambiguous situation. The compiler will attempt to resolve the

341+ambiguity using the types involved. If it's unable --- for example, because

342+the declarations with the same name also have the same type signatures --- the

343+situation can be cleared up using a *qualified name*.

344+

345+A qualified name has the symbol's namespace prefixed, separated by a ``.``:

346+

347+.. code-block:: idris

348+

349+ Data.Vect.length

350+

351+This would specifically reference a ``length`` declaration from ``Data.Vect``.

352+

353+Qualified names can be written using two different shorthands:

354+

355+1. Names in modules that are :ref:`imported <syntax-imports>` using an alias

356+ can be qualified by the alias.

357+

358+2. The name can be qualified by the *shortest unique suffix* of the

359+ namespace in question. For example, the ``length`` case above can likely

360+ be shortened to ``Vect.length``.

361+

362+.. _syntax-comments:

363+

249Comments

364Comments

250~~~~~~~~

365~~~~~~~~

251

366

@@ -264,6 +379,8 @@ Multi line String literals

264 this is a

379 this is a

265 string literal"""

380 string literal"""

266

381

382+.. _syntax-directives:

383+

267Directives

384Directives

268----------

385----------

269

386

idris.cabal+2−1

@@ -550,6 +550,7 @@ Extra-source-files:

550 test/primitives001/run

551 test/primitives001/*.idr

552 test/primitives001/expected

553+ test/primitives001/input

553 test/primitives002/run

554 test/primitives002/run

554 test/primitives002/expected

555 test/primitives002/expected

555 test/primitives003/run

556 test/primitives003/run

@@ -933,7 +934,7 @@ Library

933 , trifecta >= 1.1 && < 1.6

934 , trifecta >= 1.1 && < 1.6

934 , uniplate >=1.6 && < 1.7

935 , uniplate >=1.6 && < 1.7

935 , unordered-containers < 0.3

936 , unordered-containers < 0.3

936− , utf8-string <= 1

937+ , utf8-string < 1.1

937 , vector < 0.11

938 , vector < 0.11

938 , vector-binary-instances < 0.3

939 , vector-binary-instances < 0.3

939 , zip-archive > 0.2.3.5 && < 0.2.4

940 , zip-archive > 0.2.3.5 && < 0.2.4

jsrts/Runtime-node.js+12−6

@@ -10,14 +10,20 @@ var i$getLine = (function() {

11 return function() {

12 var ret = "";

13−

13+ var b = new Buffer(1024);

14+ var i = 0;

14 while(true) {

15 while(true) {

15− var b = new Buffer(1);

16− fs.readSync(0, b, 0, 1 )

16+ fs.readSync(0, b, i, 1 )

17− if (b[0] == 10)

17+ if (b[i] == 10) {

18+ ret = b.toString('utf8', 0, i);

18 break;

19 break;

19− else

20+ }

20− ret += String.fromCharCode(b[0]);

21+ i++;

22+ if (i == b.length) {

23+ nb = new Buffer (b.length*2);

24+ b.copy(nb)

25+ b = nb;

26+ }

21 }

27 }

23 return ret;

29 return ret;

libs/base/Data/Vect.idr+561−7

@@ -1,11 +1,571 @@

1module Data.Vect

3+import public Data.Fin

3import Language.Reflection

4import Language.Reflection

4−import public Data.VectType

6%access public

7%default total

9+infixr 7 ::

10+

11+||| Vectors: Generic lists with explicit length in the type

12+%elim

13+data Vect : Nat -> Type -> Type where

14+ ||| Empty vector

15+ Nil : Vect Z a

16+ ||| A non-empty vector of length `S k`, consisting of a head element and

17+ ||| the rest of the list, of length `k`.

18+ (::) : (x : a) -> (xs : Vect k a) -> Vect (S k) a

19+

20+-- Hints for interactive editing

21+%name Vect xs,ys,zs,ws

22+

23+--------------------------------------------------------------------------------

24+-- Length

25+--------------------------------------------------------------------------------

26+

27+||| Calculate the length of a `Vect`.

28+|||

29+||| **Note**: this is only useful if you don't already statically know the length

30+||| and you want to avoid matching the implicit argument for erasure reasons.

31+||| @ n the length (provably equal to the return value)

32+||| @ xs the vector

33+length : (xs : Vect n a) -> Nat

34+length [] = 0

35+length (x::xs) = 1 + length xs

36+

37+||| Show that the length function on vectors in fact calculates the length

38+private lengthCorrect : (n : Nat) -> (xs : Vect n a) -> length xs = n

39+lengthCorrect Z [] = Refl

40+lengthCorrect (S n) (x :: xs) = rewrite lengthCorrect n xs in Refl

41+

42+--------------------------------------------------------------------------------

43+-- Indexing into vectors

44+--------------------------------------------------------------------------------

45+

46+||| All but the first element of the vector

47+tail : Vect (S n) a -> Vect n a

48+tail (x::xs) = xs

49+

50+||| Only the first element of the vector

51+head : Vect (S n) a -> a

52+head (x::xs) = x

53+

54+||| The last element of the vector

55+last : Vect (S n) a -> a

56+last (x::[]) = x

57+last (x::y::ys) = last $ y::ys

58+

59+||| All but the last element of the vector

60+init : Vect (S n) a -> Vect n a

61+init (x::[]) = []

62+init (x::y::ys) = x :: init (y::ys)

63+

64+||| Extract a particular element from a vector

65+index : Fin n -> Vect n a -> a

66+index FZ (x::xs) = x

67+index (FS k) (x::xs) = index k xs

68+

69+

70+||| Insert an element at a particular index

71+insertAt : Fin (S n) -> a -> Vect n a -> Vect (S n) a

72+insertAt FZ y xs = y :: xs

73+insertAt (FS k) y (x::xs) = x :: insertAt k y xs

74+insertAt (FS k) y [] = absurd k

75+

76+||| Construct a new vector consisting of all but the indicated element

77+deleteAt : Fin (S n) -> Vect (S n) a -> Vect n a

78+deleteAt FZ (x::xs) = xs

79+deleteAt {n = S m} (FS k) (x::xs) = x :: deleteAt k xs

80+deleteAt {n = Z} (FS k) (x::xs) = absurd k

81+deleteAt _ [] impossible

82+

83+||| Replace an element at a particlar index with another

84+replaceAt : Fin n -> t -> Vect n t -> Vect n t

85+replaceAt FZ y (x::xs) = y :: xs

86+replaceAt (FS k) y (x::xs) = x :: replaceAt k y xs

87+

88+||| Replace the element at a particular index with the result of applying a function to it

89+||| @ i the index to replace at

90+||| @ f the update function

91+||| @ xs the vector to replace in

92+updateAt : (i : Fin n) -> (f : t -> t) -> (xs : Vect n t) -> Vect n t

93+updateAt FZ f (x::xs) = f x :: xs

94+updateAt (FS k) f (x::xs) = x :: updateAt k f xs

95+

96+--------------------------------------------------------------------------------

97+-- Subvectors

98+--------------------------------------------------------------------------------

99+

100+||| Get the first n elements of a Vect

101+||| @ n the number of elements to take

102+take : (n : Nat) -> Vect (n + m) a -> Vect n a

103+take Z xs = []

104+take (S k) (x :: xs) = x :: take k xs

105+

106+||| Remove the first n elements of a Vect

107+||| @ n the number of elements to remove

108+drop : (n : Nat) -> Vect (n + m) a -> Vect m a

109+drop Z xs = xs

110+drop (S k) (x :: xs) = drop k xs

111+

112+||| Take the longest prefix of a Vect such that all elements satisfy some

113+||| Boolean predicate.

114+|||

115+||| @ p the predicate

116+takeWhile : (p : a -> Bool) -> Vect n a -> (q ** Vect q a)

117+takeWhile p [] = (_ ** [])

118+takeWhile p (x::xs) =

119+ let (len ** ys) = takeWhile p xs

120+ in if p x then

121+ (S len ** x :: ys)

122+ else

123+ (_ ** [])

124+

125+||| Remove the longest prefix of a Vect such that all removed elements satisfy some

126+||| Boolean predicate.

127+|||

128+||| @ p the predicate

129+dropWhile : (p : a -> Bool) -> Vect n a -> (q ** Vect q a)

130+dropWhile p [] = (_ ** [])

131+dropWhile p (x::xs) =

132+ if p x then

133+ dropWhile p xs

134+ else

135+ (_ ** x::xs)

136+

137+--------------------------------------------------------------------------------

138+-- Transformations

139+--------------------------------------------------------------------------------

140+

141+||| Reverse the order of the elements of a vector

142+reverse : Vect n a -> Vect n a

143+reverse xs = go [] xs

144+ where go : Vect n a -> Vect m a -> Vect (n+m) a

145+ go {n} acc [] = rewrite plusZeroRightNeutral n in acc

146+ go {n} {m=S m} acc (x :: xs) = rewrite sym $ plusSuccRightSucc n m

147+ in go (x::acc) xs

148+

149+||| Alternate an element between the other elements of a vector

150+||| @ sep the element to intersperse

151+||| @ xs the vector to separate with `sep`

152+intersperse : (sep : a) -> (xs : Vect n a) -> Vect (n + pred n) a

153+intersperse sep [] = []

154+intersperse sep (x::xs) = x :: intersperse' sep xs

155+ where

156+ intersperse' : a -> Vect n a -> Vect (n + n) a

157+ intersperse' sep [] = []

158+ intersperse' {n=S n} sep (x::xs) = rewrite sym $ plusSuccRightSucc n n

159+ in sep :: x :: intersperse' sep xs

160+

161+--------------------------------------------------------------------------------

162+-- Conversion from list (toList is provided by Foldable)

163+--------------------------------------------------------------------------------

164+

165+

166+fromList' : Vect n a -> (l : List a) -> Vect (length l + n) a

167+fromList' ys [] = ys

168+fromList' {n} ys (x::xs) =

169+ rewrite (plusSuccRightSucc (length xs) n) ==>

170+ Vect (plus (length xs) (S n)) a in

171+ fromList' (x::ys) xs

172+

173+||| Convert a list to a vector.

174+|||

175+||| The length of the list should be statically known.

176+fromList : (l : List a) -> Vect (length l) a

177+fromList l =

178+ rewrite (sym $ plusZeroRightNeutral (length l)) in

179+ reverse $ fromList' [] l

180+

181+--------------------------------------------------------------------------------

182+-- Building (bigger) vectors

183+--------------------------------------------------------------------------------

184+

185+||| Append two vectors

186+(++) : Vect m a -> Vect n a -> Vect (m + n) a

187+(++) [] ys = ys

188+(++) (x::xs) ys = x :: xs ++ ys

189+

190+||| Repeate some value n times

191+||| @ n the number of times to repeat it

192+||| @ x the value to repeat

193+replicate : (n : Nat) -> (x : a) -> Vect n a

194+replicate Z x = []

195+replicate (S k) x = x :: replicate k x

196+

197+--------------------------------------------------------------------------------

198+-- Zips and unzips

199+--------------------------------------------------------------------------------

200+

201+||| Combine two equal-length vectors pairwise with some function

202+zipWith : (a -> b -> c) -> Vect n a -> Vect n b -> Vect n c

203+zipWith f [] [] = []

204+zipWith f (x::xs) (y::ys) = f x y :: zipWith f xs ys

205+

206+||| Combine three equal-length vectors into a vector with some function

207+zipWith3 : (a -> b -> c -> d) -> Vect n a -> Vect n b -> Vect n c -> Vect n d

208+zipWith3 f [] [] [] = []

209+zipWith3 f (x::xs) (y::ys) (z::zs) = f x y z :: zipWith3 f xs ys zs

210+

211+||| Combine two equal-length vectors pairwise

212+zip : Vect n a -> Vect n b -> Vect n (a, b)

213+zip = zipWith (\x,y => (x,y))

214+

215+||| Combine three equal-length vectors elementwise into a vector of tuples

216+zip3 : Vect n a -> Vect n b -> Vect n c -> Vect n (a, b, c)

217+zip3 = zipWith3 (\x,y,z => (x,y,z))

218+

219+||| Convert a vector of pairs to a pair of vectors

220+unzip : Vect n (a, b) -> (Vect n a, Vect n b)

221+unzip [] = ([], [])

222+unzip ((l, r)::xs) with (unzip xs)

223+ | (lefts, rights) = (l::lefts, r::rights)

224+

225+||| Convert a vector of three-tuples to a triplet of vectors

226+unzip3 : Vect n (a, b, c) -> (Vect n a, Vect n b, Vect n c)

227+unzip3 [] = ([], [], [])

228+unzip3 ((l,c,r)::xs) with (unzip3 xs)

229+ | (lefts, centers, rights) = (l::lefts, c::centers, r::rights)

230+

231+--------------------------------------------------------------------------------

232+-- Equality

233+--------------------------------------------------------------------------------

234+

235+instance (Eq a) => Eq (Vect n a) where

236+ (==) [] [] = True

237+ (==) (x::xs) (y::ys) = x == y && xs == ys

238+

239+

240+--------------------------------------------------------------------------------

241+-- Order

242+--------------------------------------------------------------------------------

243+

244+instance Ord a => Ord (Vect n a) where

245+ compare [] [] = EQ

246+ compare (x::xs) (y::ys) = compare x y `thenCompare` compare xs ys

247+

248+

249+--------------------------------------------------------------------------------

250+-- Maps

251+--------------------------------------------------------------------------------

252+

253+instance Functor (Vect n) where

254+ map f [] = []

255+ map f (x::xs) = f x :: map f xs

256+

257+

258+||| Map a partial function across a vector, returning those elements for which

259+||| the function had a value.

260+|||

261+||| The first projection of the resulting pair (ie the length) will always be

262+||| at most the length of the input vector. This is not, however, guaranteed

263+||| by the type.

264+|||

265+||| @ f the partial function (expressed by returning `Maybe`)

266+||| @ xs the vector to check for results

267+mapMaybe : (f : a -> Maybe b) -> (xs : Vect n a) -> (m : Nat ** Vect m b)

268+mapMaybe f [] = (_ ** [])

269+mapMaybe f (x::xs) =

270+ let (len ** ys) = mapMaybe f xs

271+ in case f x of

272+ Just y => (S len ** y :: ys)

273+ Nothing => ( len ** ys)

274+

275+

276+--------------------------------------------------------------------------------

277+-- Folds

278+--------------------------------------------------------------------------------

279+

280+foldrImpl : (t -> acc -> acc) -> acc -> (acc -> acc) -> Vect n t -> acc

281+foldrImpl f e go [] = go e

282+foldrImpl f e go (x::xs) = foldrImpl f e (go . (f x)) xs

283+

284+instance Foldable (Vect n) where

285+ foldr f e xs = foldrImpl f e id xs

286+

287+--------------------------------------------------------------------------------

288+-- Special folds

289+--------------------------------------------------------------------------------

290+

291+||| Flatten a vector of equal-length vectors

292+concat : Vect m (Vect n a) -> Vect (m * n) a

293+concat [] = []

294+concat (v::vs) = v ++ concat vs

295+

296+||| Foldr without seeding the accumulator

297+foldr1 : (t -> t -> t) -> Vect (S n) t -> t

298+foldr1 f (x::xs) = foldr f x xs

299+

300+||| Foldl without seeding the accumulator

301+foldl1 : (t -> t -> t) -> Vect (S n) t -> t

302+foldl1 f (x::xs) = foldl f x xs

303+--------------------------------------------------------------------------------

304+-- Scans

305+--------------------------------------------------------------------------------

306+

307+scanl : (b -> a -> b) -> b -> Vect n a -> Vect (S n) b

308+scanl f q [] = [q]

309+scanl f q (x::xs) = q :: scanl f (f q x) xs

310+

311+--------------------------------------------------------------------------------

312+-- Membership tests

313+--------------------------------------------------------------------------------

314+

315+||| Search for an item using a user-provided test

316+||| @ p the equality test

317+||| @ e the item to search for

318+||| @ xs the vector to search in

319+elemBy : (p : a -> a -> Bool) -> (e : a) -> (xs : Vect n a) -> Bool

320+elemBy p e [] = False

321+elemBy p e (x::xs) = p e x || elemBy p e xs

322+

323+||| Use the default Boolean equality on elements to search for an item

324+||| @ x what to search for

325+||| @ xs where to search

326+elem : Eq a => (x : a) -> (xs : Vect n a) -> Bool

327+elem = elemBy (==)

328+

329+||| Find the association of some key with a user-provided comparison

330+||| @ p the comparison operator for keys (True if they match)

331+||| @ e the key to look for

332+lookupBy : (p : a -> a -> Bool) -> (e : a) -> (xs : Vect n (a, b)) -> Maybe b

333+lookupBy p e [] = Nothing

334+lookupBy p e ((l, r)::xs) = if p e l then Just r else lookupBy p e xs

335+

336+||| Find the assocation of some key using the default Boolean equality test

337+lookup : Eq a => a -> Vect n (a, b) -> Maybe b

338+lookup = lookupBy (==)

339+

340+||| Check if any element of xs is found in elems by a user-provided comparison

341+||| @ p the comparison operator

342+||| @ elems the vector to search

343+||| @ xs what to search for

344+hasAnyBy : (p : a -> a -> Bool) -> (elems : Vect m a) -> (xs : Vect n a) -> Bool

345+hasAnyBy p elems [] = False

346+hasAnyBy p elems (x::xs) = elemBy p x elems || hasAnyBy p elems xs

347+

348+||| Check if any element of xs is found in elems using the default Boolean equality test

349+hasAny : Eq a => Vect m a -> Vect n a -> Bool

350+hasAny = hasAnyBy (==)

351+

352+--------------------------------------------------------------------------------

353+-- Searching with a predicate

354+--------------------------------------------------------------------------------

355+

356+||| Find the first element of the vector that satisfies some test

357+||| @ p the test to satisfy

358+find : (p : a -> Bool) -> (xs : Vect n a) -> Maybe a

359+find p [] = Nothing

360+find p (x::xs) = if p x then Just x else find p xs

361+

362+||| Find the index of the first element of the vector that satisfies some test

363+findIndex : (a -> Bool) -> Vect n a -> Maybe (Fin n)

364+findIndex p [] = Nothing

365+findIndex p (x :: xs) = if p x then Just 0 else map FS (findIndex p xs)

366+

367+||| Find the indices of all elements that satisfy some test

368+findIndices : (a -> Bool) -> Vect m a -> List (Fin m)

369+findIndices p [] = []

370+findIndices p (x :: xs) = let is = map FS $ findIndices p xs

371+ in if p x then 0 :: is else is

372+

373+elemIndexBy : (a -> a -> Bool) -> a -> Vect m a -> Maybe (Fin m)

374+elemIndexBy p e = findIndex $ p e

375+

376+elemIndex : Eq a => a -> Vect m a -> Maybe (Fin m)

377+elemIndex = elemIndexBy (==)

378+

379+elemIndicesBy : (a -> a -> Bool) -> a -> Vect m a -> List (Fin m)

380+elemIndicesBy p e = findIndices $ p e

381+

382+elemIndices : Eq a => a -> Vect m a -> List (Fin m)

383+elemIndices = elemIndicesBy (==)

384+

385+--------------------------------------------------------------------------------

386+-- Filters

387+--------------------------------------------------------------------------------

388+

389+||| Find all elements of a vector that satisfy some test

390+filter : (a -> Bool) -> Vect n a -> (p ** Vect p a)

391+filter p [] = ( _ ** [] )

392+filter p (x::xs) =

393+ let (_ ** tail) = filter p xs

394+ in if p x then

395+ (_ ** x::tail)

396+ else

397+ (_ ** tail)

398+

399+||| Make the elements of some vector unique by some test

400+nubBy : (a -> a -> Bool) -> Vect n a -> (p ** Vect p a)

401+nubBy = nubBy' []

402+ where

403+ nubBy' : Vect m a -> (a -> a -> Bool) -> Vect n a -> (p ** Vect p a)

404+ nubBy' acc p [] = (_ ** [])

405+ nubBy' acc p (x::xs) with (elemBy p x acc)

406+ | True = nubBy' acc p xs

407+ | False with (nubBy' (x::acc) p xs)

408+ | (_ ** tail) = (_ ** x::tail)

409+

410+||| Make the elements of some vector unique by the default Boolean equality

411+nub : Eq a => Vect n a -> (p ** Vect p a)

412+nub = nubBy (==)

413+

414+deleteBy : (a -> a -> Bool) -> a -> Vect n a -> (p ** Vect p a)

415+deleteBy _ _ [] = (_ ** [])

416+deleteBy eq x (y::ys) =

417+ let (len ** zs) = deleteBy eq x ys

418+ in if x `eq` y then (_ ** ys) else (S len ** y ::zs)

419+

420+delete : (Eq a) => a -> Vect n a -> (p ** Vect p a)

421+delete = deleteBy (==)

422+

423+--------------------------------------------------------------------------------

424+-- Splitting and breaking lists

425+--------------------------------------------------------------------------------

426+

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

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

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

430+||| @ n the index to split at

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

432+splitAt : (n : Nat) -> (xs : Vect (n + m) a) -> (Vect n a, Vect m a)

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

434+

435+partition : (a -> Bool) -> Vect n a -> ((p ** Vect p a), (q ** Vect q a))

436+partition p [] = ((_ ** []), (_ ** []))

437+partition p (x::xs) =

438+ let ((leftLen ** lefts), (rightLen ** rights)) = partition p xs in

439+ if p x then

440+ ((S leftLen ** x::lefts), (rightLen ** rights))

441+ else

442+ ((leftLen ** lefts), (S rightLen ** x::rights))

443+

444+--------------------------------------------------------------------------------

445+-- Predicates

446+--------------------------------------------------------------------------------

447+

448+isPrefixOfBy : (a -> a -> Bool) -> Vect m a -> Vect n a -> Bool

449+isPrefixOfBy p [] right = True

450+isPrefixOfBy p left [] = False

451+isPrefixOfBy p (x::xs) (y::ys) = p x y && isPrefixOfBy p xs ys

452+

453+isPrefixOf : Eq a => Vect m a -> Vect n a -> Bool

454+isPrefixOf = isPrefixOfBy (==)

455+

456+isSuffixOfBy : (a -> a -> Bool) -> Vect m a -> Vect n a -> Bool

457+isSuffixOfBy p left right = isPrefixOfBy p (reverse left) (reverse right)

458+

459+isSuffixOf : Eq a => Vect m a -> Vect n a -> Bool

460+isSuffixOf = isSuffixOfBy (==)

461+

462+--------------------------------------------------------------------------------

463+-- Conversions

464+--------------------------------------------------------------------------------

465+

466+maybeToVect : Maybe a -> (p ** Vect p a)

467+maybeToVect Nothing = (_ ** [])

468+maybeToVect (Just j) = (_ ** [j])

469+

470+vectToMaybe : Vect n a -> Maybe a

471+vectToMaybe [] = Nothing

472+vectToMaybe (x::xs) = Just x

473+

474+--------------------------------------------------------------------------------

475+-- Misc

476+--------------------------------------------------------------------------------

477+

478+catMaybes : Vect n (Maybe a) -> (p ** Vect p a)

479+catMaybes [] = (_ ** [])

480+catMaybes (Nothing::xs) = catMaybes xs

481+catMaybes ((Just j)::xs) =

482+ let (_ ** tail) = catMaybes xs

483+ in (_ ** j::tail)

484+

485+diag : Vect n (Vect n a) -> Vect n a

486+diag [] = []

487+diag ((x::xs)::xss) = x :: diag (map tail xss)

488+

489+range : {n : Nat} -> Vect n (Fin n)

490+range {n=Z} = []

491+range {n=S _} = FZ :: map FS range

492+

493+||| Transpose a Vect of Vects, turning rows into columns and vice versa.

494+|||

495+||| As the types ensure rectangularity, this is an involution, unlike `Prelude.List.transpose`.

496+transpose : {n : Nat} -> Vect m (Vect n a) -> Vect n (Vect m a)

497+transpose [] = replicate _ []

498+transpose (x :: xs) = zipWith (::) x (transpose xs)

499+

500+--------------------------------------------------------------------------------

501+-- Applicative/Monad/Traversable

502+--------------------------------------------------------------------------------

503+

504+instance Applicative (Vect k) where

505+ pure = replicate _

506+

507+ fs <*> vs = zipWith apply fs vs

508+

509+||| This monad is different from the List monad, (>>=)

510+||| uses the diagonal.

511+instance Monad (Vect n) where

512+ m >>= f = diag (map f m)

513+

514+instance Traversable (Vect n) where

515+ traverse f [] = pure Vect.Nil

516+ traverse f (x::xs) = [| Vect.(::) (f x) (traverse f xs) |]

517+

518+--------------------------------------------------------------------------------

519+-- Show

520+--------------------------------------------------------------------------------

521+

522+instance Show a => Show (Vect n a) where

523+ show = show . toList

524+

525+--------------------------------------------------------------------------------

526+-- Properties

527+--------------------------------------------------------------------------------

528+

529+vectConsCong : (x : a) -> (xs : Vect n a) -> (ys : Vect m a) -> (xs = ys) -> (x :: xs = x :: ys)

530+vectConsCong x xs xs Refl = Refl

531+

532+vectNilRightNeutral : (xs : Vect n a) -> xs ++ [] = xs

533+vectNilRightNeutral [] = Refl

534+vectNilRightNeutral (x :: xs) =

535+ vectConsCong _ _ _ (vectNilRightNeutral xs)

536+

537+vectAppendAssociative : (x : Vect xLen a) -> (y : Vect yLen a) -> (z : Vect zLen a) -> x ++ (y ++ z) = (x ++ y) ++ z

538+vectAppendAssociative [] y z = Refl

539+vectAppendAssociative (x :: xs) ys zs =

540+ vectConsCong _ _ _ (vectAppendAssociative xs ys zs)

541+

542+--------------------------------------------------------------------------------

543+-- DecEq

544+--------------------------------------------------------------------------------

545+

546+vectInjective1 : {xs, ys : Vect n a} -> {x, y : a} -> x :: xs = y :: ys -> x = y

547+vectInjective1 {x=x} {y=x} {xs=xs} {ys=xs} Refl = Refl

548+

549+vectInjective2 : {xs, ys : Vect n a} -> {x, y : a} -> x :: xs = y :: ys -> xs = ys

550+vectInjective2 {x=x} {y=x} {xs=xs} {ys=xs} Refl = Refl

551+

552+instance DecEq a => DecEq (Vect n a) where

553+ decEq [] [] = Yes Refl

554+ decEq (x :: xs) (y :: ys) with (decEq x y)

555+ decEq (x :: xs) (x :: ys) | Yes Refl with (decEq xs ys)

556+ decEq (x :: xs) (x :: xs) | Yes Refl | Yes Refl = Yes Refl

557+ decEq (x :: xs) (x :: ys) | Yes Refl | No neq = No (neq . vectInjective2)

558+ decEq (x :: xs) (y :: ys) | No neq = No (neq . vectInjective1)

559+

560+{- The following definition is elaborated in a wrong case-tree. Examination pending.

561+instance DecEq a => DecEq (Vect n a) where

562+ decEq [] [] = Yes Refl

563+ decEq (x :: xs) (y :: ys) with (decEq x y, decEq xs ys)

564+ decEq (x :: xs) (x :: xs) | (Yes Refl, Yes Refl) = Yes Refl

565+ decEq (x :: xs) (y :: ys) | (_, No nEqTl) = No (\p => nEqTl (vectInjective2 p))

566+ decEq (x :: xs) (y :: ys) | (No nEqHd, _) = No (\p => nEqHd (vectInjective1 p))

567+-}

568+

9--------------------------------------------------------------------------------

569--------------------------------------------------------------------------------

10-- Elem

570-- Elem

11--------------------------------------------------------------------------------

571--------------------------------------------------------------------------------

@@ -33,12 +593,6 @@ isElem x (y :: xs) with (decEq x y)

33 isElem x (y :: xs) | (No xneqy) | (Yes xinxs) = Yes (There xinxs)

593 isElem x (y :: xs) | (No xneqy) | (Yes xinxs) = Yes (There xinxs)

34 isElem x (y :: xs) | (No xneqy) | (No xninxs) = No (neitherHereNorThere xneqy xninxs)

594 isElem x (y :: xs) | (No xneqy) | (No xninxs) = No (neitherHereNorThere xneqy xninxs)

595

36−||| A tactic for discovering where, if anywhere, an element is in a vector

37−||| @ n how many elements to search before giving up

38−findElem : (n : Nat) -> List (TTName, Binder TT) -> TT -> Tactic

39−findElem Z ctxt goal = Refine "Here" `Seq` Solve

40−findElem (S n) ctxt goal = GoalType "Elem" (Try (Refine "Here" `Seq` Solve) (Refine "There" `Seq` (Solve `Seq` findElem n ctxt goal)))

41−

42replaceElem : (xs : Vect k t) -> Elem x xs -> (y : t) -> (ys : Vect k t ** Elem y ys)

596replaceElem : (xs : Vect k t) -> Elem x xs -> (y : t) -> (ys : Vect k t ** Elem y ys)

43replaceElem (x::xs) Here y = (y :: xs ** Here)

597replaceElem (x::xs) Here y = (y :: xs ** Here)

44replaceElem (x::xs) (There xinxs) y with (replaceElem xs xinxs y)

598replaceElem (x::xs) (There xinxs) y with (replaceElem xs xinxs y)

libs/base/Data/VectType.idrdeleted−601

@@ -1,601 +0,0 @@

1−module Data.VectType

2−

3−import public Data.Fin

4−

5−%access public

6−%default total

7−

8−namespace Vect {

9−

10−infixr 7 ::

11−

12−||| Vectors: Generic lists with explicit length in the type

13−%elim

14−data Vect : Nat -> Type -> Type where

15− ||| Empty vector

16− Nil : Vect Z a

17− ||| A non-empty vector of length `S k`, consisting of a head element and

18− ||| the rest of the list, of length `k`.

19− (::) : (x : a) -> (xs : Vect k a) -> Vect (S k) a

20−

21−-- Hints for interactive editing

22−%name Vect xs,ys,zs,ws

23−

24−--------------------------------------------------------------------------------

25−-- Length

26−--------------------------------------------------------------------------------

27−

28−||| Calculate the length of a `Vect`.

29−|||

30−||| **Note**: this is only useful if you don't already statically know the length

31−||| and you want to avoid matching the implicit argument for erasure reasons.

32−||| @ n the length (provably equal to the return value)

33−||| @ xs the vector

34−length : (xs : Vect n a) -> Nat

35−length [] = 0

36−length (x::xs) = 1 + length xs

37−

38−||| Show that the length function on vectors in fact calculates the length

39−private lengthCorrect : (n : Nat) -> (xs : Vect n a) -> length xs = n

40−lengthCorrect Z [] = Refl

41−lengthCorrect (S n) (x :: xs) = rewrite lengthCorrect n xs in Refl

42−

43−--------------------------------------------------------------------------------

44−-- Indexing into vectors

45−--------------------------------------------------------------------------------

46−

47−||| All but the first element of the vector

48−tail : Vect (S n) a -> Vect n a

49−tail (x::xs) = xs

50−

51−||| Only the first element of the vector

52−head : Vect (S n) a -> a

53−head (x::xs) = x

54−

55−||| The last element of the vector

56−last : Vect (S n) a -> a

57−last (x::[]) = x

58−last (x::y::ys) = last $ y::ys

59−

60−||| All but the last element of the vector

61−init : Vect (S n) a -> Vect n a

62−init (x::[]) = []

63−init (x::y::ys) = x :: init (y::ys)

64−

65−||| Extract a particular element from a vector

66−index : Fin n -> Vect n a -> a

67−index FZ (x::xs) = x

68−index (FS k) (x::xs) = index k xs

69−

70−

71−||| Insert an element at a particular index

72−insertAt : Fin (S n) -> a -> Vect n a -> Vect (S n) a

73−insertAt FZ y xs = y :: xs

74−insertAt (FS k) y (x::xs) = x :: insertAt k y xs

75−insertAt (FS k) y [] = absurd k

76−

77−||| Construct a new vector consisting of all but the indicated element

78−deleteAt : Fin (S n) -> Vect (S n) a -> Vect n a

79−deleteAt FZ (x::xs) = xs

80−deleteAt {n = S m} (FS k) (x::xs) = x :: deleteAt k xs

81−deleteAt {n = Z} (FS k) (x::xs) = absurd k

82−deleteAt _ [] impossible

83−

84−||| Replace an element at a particlar index with another

85−replaceAt : Fin n -> t -> Vect n t -> Vect n t

86−replaceAt FZ y (x::xs) = y :: xs

87−replaceAt (FS k) y (x::xs) = x :: replaceAt k y xs

88−

89−||| Replace the element at a particular index with the result of applying a function to it

90−||| @ i the index to replace at

91−||| @ f the update function

92−||| @ xs the vector to replace in

93−updateAt : (i : Fin n) -> (f : t -> t) -> (xs : Vect n t) -> Vect n t

94−updateAt FZ f (x::xs) = f x :: xs

95−updateAt (FS k) f (x::xs) = x :: updateAt k f xs

96−

97−--------------------------------------------------------------------------------

98−-- Subvectors

99−--------------------------------------------------------------------------------

100−

101−||| Get the first n elements of a Vect

102−||| @ n the number of elements to take

103−take : (n : Nat) -> Vect (n + m) a -> Vect n a

104−take Z xs = []

105−take (S k) (x :: xs) = x :: take k xs

106−

107−||| Remove the first n elements of a Vect

108−||| @ n the number of elements to remove

109−drop : (n : Nat) -> Vect (n + m) a -> Vect m a

110−drop Z xs = xs

111−drop (S k) (x :: xs) = drop k xs

112−

113−||| Take the longest prefix of a Vect such that all elements satisfy some

114−||| Boolean predicate.

115−|||

116−||| @ p the predicate

117−takeWhile : (p : a -> Bool) -> Vect n a -> (q ** Vect q a)

118−takeWhile p [] = (_ ** [])

119−takeWhile p (x::xs) =

120− let (len ** ys) = takeWhile p xs

121− in if p x then

122− (S len ** x :: ys)

123− else

124− (_ ** [])

125−

126−||| Remove the longest prefix of a Vect such that all removed elements satisfy some

127−||| Boolean predicate.

128−|||

129−||| @ p the predicate

130−dropWhile : (p : a -> Bool) -> Vect n a -> (q ** Vect q a)

131−dropWhile p [] = (_ ** [])

132−dropWhile p (x::xs) =

133− if p x then

134− dropWhile p xs

135− else

136− (_ ** x::xs)

137−

138−--------------------------------------------------------------------------------

139−-- Transformations

140−--------------------------------------------------------------------------------

141−

142−||| Reverse the order of the elements of a vector

143−reverse : Vect n a -> Vect n a

144−reverse xs = go [] xs

145− where go : Vect n a -> Vect m a -> Vect (n+m) a

146− go {n} acc [] = rewrite plusZeroRightNeutral n in acc

147− go {n} {m=S m} acc (x :: xs) = rewrite sym $ plusSuccRightSucc n m

148− in go (x::acc) xs

149−

150−||| Alternate an element between the other elements of a vector

151−||| @ sep the element to intersperse

152−||| @ xs the vector to separate with `sep`

153−intersperse : (sep : a) -> (xs : Vect n a) -> Vect (n + pred n) a

154−intersperse sep [] = []

155−intersperse sep (x::xs) = x :: intersperse' sep xs

156− where

157− intersperse' : a -> Vect n a -> Vect (n + n) a

158− intersperse' sep [] = []

159− intersperse' {n=S n} sep (x::xs) = rewrite sym $ plusSuccRightSucc n n

160− in sep :: x :: intersperse' sep xs

161−

162−--------------------------------------------------------------------------------

163−-- Conversion from list (toList is provided by Foldable)

164−--------------------------------------------------------------------------------

165−

166−

167−fromList' : Vect n a -> (l : List a) -> Vect (length l + n) a

168−fromList' ys [] = ys

169−fromList' {n} ys (x::xs) =

170− rewrite (plusSuccRightSucc (length xs) n) ==>

171− Vect (plus (length xs) (S n)) a in

172− fromList' (x::ys) xs

173−

174−||| Convert a list to a vector.

175−|||

176−||| The length of the list should be statically known.

177−fromList : (l : List a) -> Vect (length l) a

178−fromList l =

179− rewrite (sym $ plusZeroRightNeutral (length l)) in

180− reverse $ fromList' [] l

181−

182−--------------------------------------------------------------------------------

183−-- Building (bigger) vectors

184−--------------------------------------------------------------------------------

185−

186−||| Append two vectors

187−(++) : Vect m a -> Vect n a -> Vect (m + n) a

188−(++) [] ys = ys

189−(++) (x::xs) ys = x :: xs ++ ys

190−

191−||| Repeate some value n times

192−||| @ n the number of times to repeat it

193−||| @ x the value to repeat

194−replicate : (n : Nat) -> (x : a) -> Vect n a

195−replicate Z x = []

196−replicate (S k) x = x :: replicate k x

197−

198−--------------------------------------------------------------------------------

199−-- Zips and unzips

200−--------------------------------------------------------------------------------

201−

202−||| Combine two equal-length vectors pairwise with some function

203−zipWith : (a -> b -> c) -> Vect n a -> Vect n b -> Vect n c

204−zipWith f [] [] = []

205−zipWith f (x::xs) (y::ys) = f x y :: zipWith f xs ys

206−

207−||| Combine three equal-length vectors into a vector with some function

208−zipWith3 : (a -> b -> c -> d) -> Vect n a -> Vect n b -> Vect n c -> Vect n d

209−zipWith3 f [] [] [] = []

210−zipWith3 f (x::xs) (y::ys) (z::zs) = f x y z :: zipWith3 f xs ys zs

211−

212−||| Combine two equal-length vectors pairwise

213−zip : Vect n a -> Vect n b -> Vect n (a, b)

214−zip = zipWith (\x,y => (x,y))

215−

216−||| Combine three equal-length vectors elementwise into a vector of tuples

217−zip3 : Vect n a -> Vect n b -> Vect n c -> Vect n (a, b, c)

218−zip3 = zipWith3 (\x,y,z => (x,y,z))

219−

220−||| Convert a vector of pairs to a pair of vectors

221−unzip : Vect n (a, b) -> (Vect n a, Vect n b)

222−unzip [] = ([], [])

223−unzip ((l, r)::xs) with (unzip xs)

224− | (lefts, rights) = (l::lefts, r::rights)

225−

226−||| Convert a vector of three-tuples to a triplet of vectors

227−unzip3 : Vect n (a, b, c) -> (Vect n a, Vect n b, Vect n c)

228−unzip3 [] = ([], [], [])

229−unzip3 ((l,c,r)::xs) with (unzip3 xs)

230− | (lefts, centers, rights) = (l::lefts, c::centers, r::rights)

231−

232−--------------------------------------------------------------------------------

233−-- Equality

234−--------------------------------------------------------------------------------

235−

236−instance (Eq a) => Eq (Vect n a) where

237− (==) [] [] = True

238− (==) (x::xs) (y::ys) =

239− if x == y then

240− xs == ys

241− else

242− False

243−

244−

245−--------------------------------------------------------------------------------

246−-- Order

247−--------------------------------------------------------------------------------

248−

249−instance Ord a => Ord (Vect n a) where

250− compare [] [] = EQ

251− compare (x::xs) (y::ys) =

252− if x /= y then

253− compare x y

254− else

255− compare xs ys

256−

257−

258−--------------------------------------------------------------------------------

259−-- Maps

260−--------------------------------------------------------------------------------

261−

262−instance Functor (Vect n) where

263− map f [] = []

264− map f (x::xs) = f x :: map f xs

265−

266−

267−||| Map a partial function across a vector, returning those elements for which

268−||| the function had a value.

269−|||

270−||| The first projection of the resulting pair (ie the length) will always be

271−||| at most the length of the input vector. This is not, however, guaranteed

272−||| by the type.

273−|||

274−||| @ f the partial function (expressed by returning `Maybe`)

275−||| @ xs the vector to check for results

276−mapMaybe : (f : a -> Maybe b) -> (xs : Vect n a) -> (m : Nat ** Vect m b)

277−mapMaybe f [] = (_ ** [])

278−mapMaybe f (x::xs) =

279− let (len ** ys) = mapMaybe f xs

280− in case f x of

281− Just y => (S len ** y :: ys)

282− Nothing => ( len ** ys)

283−

284−

285−--------------------------------------------------------------------------------

286−-- Folds

287−--------------------------------------------------------------------------------

288−

289−total foldrImpl : (t -> acc -> acc) -> acc -> (acc -> acc) -> Vect n t -> acc

290−foldrImpl f e go [] = go e

291−foldrImpl f e go (x::xs) = foldrImpl f e (go . (f x)) xs

292−

293−instance Foldable (Vect n) where

294− foldr f e xs = foldrImpl f e id xs

295−

296−--------------------------------------------------------------------------------

297−-- Special folds

298−--------------------------------------------------------------------------------

299−

300−||| Flatten a vector of equal-length vectors

301−concat : Vect m (Vect n a) -> Vect (m * n) a

302−concat [] = []

303−concat (v::vs) = v ++ concat vs

304−

305−||| Foldr without seeding the accumulator

306−foldr1 : (t -> t -> t) -> Vect (S n) t -> t

307−foldr1 f (x::xs) = foldr f x xs

308−

309−||| Foldl without seeding the accumulator

310−foldl1 : (t -> t -> t) -> Vect (S n) t -> t

311−foldl1 f (x::xs) = foldl f x xs

312−--------------------------------------------------------------------------------

313−-- Scans

314−--------------------------------------------------------------------------------

315−

316−scanl : (b -> a -> b) -> b -> Vect n a -> Vect (S n) b

317−scanl f q [] = [q]

318−scanl f q (x::xs) = q :: scanl f (f q x) xs

319−

320−--------------------------------------------------------------------------------

321−-- Membership tests

322−--------------------------------------------------------------------------------

323−

324−||| Search for an item using a user-provided test

325−||| @ p the equality test

326−||| @ e the item to search for

327−||| @ xs the vector to search in

328−elemBy : (p : a -> a -> Bool) -> (e : a) -> (xs : Vect n a) -> Bool

329−elemBy p e [] = False

330−elemBy p e (x::xs) with (p e x)

331− | True = True

332− | False = elemBy p e xs

333−

334−||| Use the default Boolean equality on elements to search for an item

335−||| @ x what to search for

336−||| @ xs where to search

337−elem : Eq a => (x : a) -> (xs : Vect n a) -> Bool

338−elem = elemBy (==)

339−

340−||| Find the association of some key with a user-provided comparison

341−||| @ p the comparison operator for keys (True if they match)

342−||| @ e the key to look for

343−lookupBy : (p : a -> a -> Bool) -> (e : a) -> (xs : Vect n (a, b)) -> Maybe b

344−lookupBy p e [] = Nothing

345−lookupBy p e ((l, r)::xs) with (p e l)

346− | True = Just r

347− | False = lookupBy p e xs

348−

349−||| Find the assocation of some key using the default Boolean equality test

350−lookup : Eq a => a -> Vect n (a, b) -> Maybe b

351−lookup = lookupBy (==)

352−

353−||| Check if any element of xs is found in elems by a user-provided comparison

354−||| @ p the comparison operator

355−||| @ elems the vector to search

356−||| @ xs what to search for

357−hasAnyBy : (p : a -> a -> Bool) -> (elems : Vect m a) -> (xs : Vect n a) -> Bool

358−hasAnyBy p elems [] = False

359−hasAnyBy p elems (x::xs) with (elemBy p x elems)

360− | True = True

361− | False = hasAnyBy p elems xs

362−

363−||| Check if any element of xs is found in elems using the default Boolean equality test

364−hasAny : Eq a => Vect m a -> Vect n a -> Bool

365−hasAny = hasAnyBy (==)

366−

367−--------------------------------------------------------------------------------

368−-- Searching with a predicate

369−--------------------------------------------------------------------------------

370−

371−||| Find the first element of the vector that satisfies some test

372−||| @ p the test to satisfy

373−find : (p : a -> Bool) -> (xs : Vect n a) -> Maybe a

374−find p [] = Nothing

375−find p (x::xs) with (p x)

376− | True = Just x

377− | False = find p xs

378−

379−||| Find the index of the first element of the vector that satisfies some test

380−findIndex : (a -> Bool) -> Vect n a -> Maybe (Fin n)

381−findIndex p [] = Nothing

382−findIndex p (x :: xs) with (p x)

383− | True = Just 0

384− | False = map FS (findIndex p xs)

385−

386−||| Find the indices of all elements that satisfy some test

387−total findIndices : (a -> Bool) -> Vect m a -> (p ** Vect p Nat)

388−findIndices = findIndices' 0

389− where

390− total findIndices' : Nat -> (a -> Bool) -> Vect m a -> (p ** Vect p Nat)

391− findIndices' cnt p [] = (_ ** [])

392− findIndices' cnt p (x::xs) with (findIndices' (S cnt) p xs)

393− | (_ ** tail) =

394− if p x then

395− (_ ** cnt::tail)

396− else

397− (_ ** tail)

398−

399−elemIndexBy : (a -> a -> Bool) -> a -> Vect m a -> Maybe (Fin m)

400−elemIndexBy p e = findIndex $ p e

401−

402−elemIndex : Eq a => a -> Vect m a -> Maybe (Fin m)

403−elemIndex = elemIndexBy (==)

404−

405−total elemIndicesBy : (a -> a -> Bool) -> a -> Vect m a -> (p ** Vect p Nat)

406−elemIndicesBy p e = findIndices $ p e

407−

408−total elemIndices : Eq a => a -> Vect m a -> (p ** Vect p Nat)

409−elemIndices = elemIndicesBy (==)

410−

411−--------------------------------------------------------------------------------

412−-- Filters

413−--------------------------------------------------------------------------------

414−

415−||| Find all elements of a vector that satisfy some test

416−total filter : (a -> Bool) -> Vect n a -> (p ** Vect p a)

417−filter p [] = ( _ ** [] )

418−filter p (x::xs) with (filter p xs)

419− | (_ ** tail) =

420− if p x then

421− (_ ** x::tail)

422− else

423− (_ ** tail)

424−

425−||| Make the elements of some vector unique by some test

426−nubBy : (a -> a -> Bool) -> Vect n a -> (p ** Vect p a)

427−nubBy = nubBy' []

428− where

429− nubBy' : Vect m a -> (a -> a -> Bool) -> Vect n a -> (p ** Vect p a)

430− nubBy' acc p [] = (_ ** [])

431− nubBy' acc p (x::xs) with (elemBy p x acc)

432− | True = nubBy' acc p xs

433− | False with (nubBy' (x::acc) p xs)

434− | (_ ** tail) = (_ ** x::tail)

435−

436−||| Make the elements of some vector unique by the default Boolean equality

437−nub : Eq a => Vect n a -> (p ** Vect p a)

438−nub = nubBy (==)

439−

440−deleteBy : (a -> a -> Bool) -> a -> Vect n a -> (p ** Vect p a)

441−deleteBy _ _ [] = (_ ** [])

442−deleteBy eq x (y::ys) =

443− let (len ** zs) = deleteBy eq x ys

444− in if x `eq` y then (_ ** ys) else (S len ** y ::zs)

445−

446−delete : (Eq a) => a -> Vect n a -> (p ** Vect p a)

447−delete = deleteBy (==)

448−

449−--------------------------------------------------------------------------------

450−-- Splitting and breaking lists

451−--------------------------------------------------------------------------------

452−

453−||| A tuple where the first element is a Vect of the n first elements and

454−||| the second element is a Vect of the remaining elements of the original Vect

455−||| It is equivalent to (take n xs, drop n xs)

456−||| @ n the index to split at

457−||| @ xs the Vect to split in two

458−splitAt : (n : Nat) -> (xs : Vect (n + m) a) -> (Vect n a, Vect m a)

459−splitAt n xs = (take n xs, drop n xs)

460−

461−partition : (a -> Bool) -> Vect n a -> ((p ** Vect p a), (q ** Vect q a))

462−partition p [] = ((_ ** []), (_ ** []))

463−partition p (x::xs) =

464− let ((leftLen ** lefts), (rightLen ** rights)) = partition p xs in

465− if p x then

466− ((S leftLen ** x::lefts), (rightLen ** rights))

467− else

468− ((leftLen ** lefts), (S rightLen ** x::rights))

469−

470−--------------------------------------------------------------------------------

471−-- Predicates

472−--------------------------------------------------------------------------------

473−

474−isPrefixOfBy : (a -> a -> Bool) -> Vect m a -> Vect n a -> Bool

475−isPrefixOfBy p [] right = True

476−isPrefixOfBy p left [] = False

477−isPrefixOfBy p (x::xs) (y::ys) with (p x y)

478− | True = isPrefixOfBy p xs ys

479− | False = False

480−

481−isPrefixOf : Eq a => Vect m a -> Vect n a -> Bool

482−isPrefixOf = isPrefixOfBy (==)

483−

484−isSuffixOfBy : (a -> a -> Bool) -> Vect m a -> Vect n a -> Bool

485−isSuffixOfBy p left right = isPrefixOfBy p (reverse left) (reverse right)

486−

487−isSuffixOf : Eq a => Vect m a -> Vect n a -> Bool

488−isSuffixOf = isSuffixOfBy (==)

489−

490−--------------------------------------------------------------------------------

491−-- Conversions

492−--------------------------------------------------------------------------------

493−

494−total maybeToVect : Maybe a -> (p ** Vect p a)

495−maybeToVect Nothing = (_ ** [])

496−maybeToVect (Just j) = (_ ** [j])

497−

498−total vectToMaybe : Vect n a -> Maybe a

499−vectToMaybe [] = Nothing

500−vectToMaybe (x::xs) = Just x

501−

502−--------------------------------------------------------------------------------

503−-- Misc

504−--------------------------------------------------------------------------------

505−

506−catMaybes : Vect n (Maybe a) -> (p ** Vect p a)

507−catMaybes [] = (_ ** [])

508−catMaybes (Nothing::xs) = catMaybes xs

509−catMaybes ((Just j)::xs) with (catMaybes xs)

510− | (_ ** tail) = (_ ** j::tail)

511−

512−diag : Vect n (Vect n a) -> Vect n a

513−diag [] = []

514−diag ((x::xs)::xss) = x :: diag (map tail xss)

515−

516−range : Vect n (Fin n)

517−range {n=Z} = []

518−range {n=S _} = FZ :: map FS range

519−

520−||| Transpose a Vect of Vects, turning rows into columns and vice versa.

521−|||

522−||| As the types ensure rectangularity, this is an involution, unlike `Prelude.List.transpose`.

523−transpose : Vect m (Vect n a) -> Vect n (Vect m a)

524−transpose [] = replicate _ []

525−transpose (x :: xs) = zipWith (::) x (transpose xs)

526−

527−--------------------------------------------------------------------------------

528−-- Applicative/Monad/Traversable

529−--------------------------------------------------------------------------------

530−

531−instance Applicative (Vect k) where

532− pure = replicate _

533−

534− fs <*> vs = zipWith apply fs vs

535−

536−||| This monad is different from the List monad, (>>=)

537−||| uses the diagonal.

538−instance Monad (Vect n) where

539− m >>= f = diag (map f m)

540−

541−instance Traversable (Vect n) where

542− traverse f [] = pure Vect.Nil

543− traverse f (x::xs) = [| Vect.(::) (f x) (traverse f xs) |]

544−

545−--------------------------------------------------------------------------------

546−-- Show

547−--------------------------------------------------------------------------------

548−

549−instance Show a => Show (Vect n a) where

550− show = show . toList

551−

552−--------------------------------------------------------------------------------

553−-- Properties

554−--------------------------------------------------------------------------------

555−

556−vectConsCong : (x : a) -> (xs : Vect n a) -> (ys : Vect m a) -> (xs = ys) -> (x :: xs = x :: ys)

557−vectConsCong x xs xs Refl = Refl

558−

559−vectNilRightNeutral : (xs : Vect n a) -> xs ++ [] = xs

560−vectNilRightNeutral [] = Refl

561−vectNilRightNeutral (x :: xs) =

562− vectConsCong _ _ _ (vectNilRightNeutral xs)

563−

564−vectAppendAssociative : (x : Vect xLen a) -> (y : Vect yLen a) -> (z : Vect zLen a) -> x ++ (y ++ z) = (x ++ y) ++ z

565−vectAppendAssociative [] y z = Refl

566−vectAppendAssociative (x :: xs) ys zs =

567− vectConsCong _ _ _ (vectAppendAssociative xs ys zs)

568−

569−}

570−

571−--------------------------------------------------------------------------------

572−-- DecEq

573−--------------------------------------------------------------------------------

574−

575−total

576−vectInjective1 : {xs, ys : Vect n a} -> {x, y : a} -> x :: xs = y :: ys -> x = y

577−vectInjective1 {x=x} {y=x} {xs=xs} {ys=xs} Refl = Refl

578−

579−total

580−vectInjective2 : {xs, ys : Vect n a} -> {x, y : a} -> x :: xs = y :: ys -> xs = ys

581−vectInjective2 {x=x} {y=x} {xs=xs} {ys=xs} Refl = Refl

582−

583−instance DecEq a => DecEq (Vect n a) where

584− decEq [] [] = Yes Refl

585− decEq (x :: xs) (y :: ys) with (decEq x y)

586− decEq (x :: xs) (x :: ys) | Yes Refl with (decEq xs ys)

587− decEq (x :: xs) (x :: xs) | Yes Refl | Yes Refl = Yes Refl

588− decEq (x :: xs) (x :: ys) | Yes Refl | No neq = No (neq . vectInjective2)

589− decEq (x :: xs) (y :: ys) | No neq = No (neq . vectInjective1)

590−

591−{- The following definition is elaborated in a wrong case-tree. Examination pending.

592−instance DecEq a => DecEq (Vect n a) where

593− decEq [] [] = Yes Refl

594− decEq (x :: xs) (y :: ys) with (decEq x y, decEq xs ys)

595− decEq (x :: xs) (x :: xs) | (Yes Refl, Yes Refl) = Yes Refl

596− decEq (x :: xs) (y :: ys) | (_, No nEqTl) = No (\p => nEqTl (vectInjective2 p))

597− decEq (x :: xs) (y :: ys) | (No nEqHd, _) = No (\p => nEqHd (vectInjective1 p))

598−-}

599−

600−-- For the primitives, we have to cheat because we don't have access to their

601−-- internal implementations.

libs/base/base.ipkg+1−1

@@ -13,7 +13,7 @@ modules = System,

14 Data.Morphisms,

15 Data.Bits, Data.Mod2,

16− Data.Fin, Data.Vect, Data.VectType,

16+ Data.Fin, Data.Vect,

17 Data.HVect, Data.Vect.Quantifiers,

18 Data.Complex,

19 Data.Erased, Data.List,

libs/prelude/Prelude/Cast.idr+1−1

@@ -3,7 +3,7 @@ module Prelude.Cast

3import Prelude.Bool

4import public Builtins

6−||| Type class for transforming a instance of a data type to another type.

6+||| Type class for transforming an instance of a data type to another type.

7class Cast from to where

8 ||| Perform a cast operation.

9 |||

libs/prelude/Prelude/Classes.idr+6

@@ -71,6 +71,12 @@ instance Eq Ordering where

71 GT == GT = True

72 _ == _ = False

74+||| Compose two comparisons into the lexicographic product

75+thenCompare : Ordering -> Lazy Ordering -> Ordering

76+thenCompare LT y = LT

77+thenCompare EQ y = y

78+thenCompare GT y = GT

79+

74||| The Ord class defines comparison operations on ordered data types.

80||| The Ord class defines comparison operations on ordered data types.

75class Eq a => Ord a where

81class Eq a => Ord a where

76 compare : a -> a -> Ordering

82 compare : a -> a -> Ordering

libs/prelude/Prelude/List.idr+3−4

@@ -52,13 +52,12 @@ data NonEmpty : (xs : List a) -> Type where

52 ||| The proof that a cons cell is non-empty

53 IsNonEmpty : NonEmpty (x :: xs)

55−private

55+instance Uninhabited (NonEmpty []) where

56−nonEmptyNil : NonEmpty [] -> Void

57−nonEmptyNil IsNonEmpty impossible

56+ uninhabited IsNonEmpty impossible

59||| Decide whether a list is non-empty

58||| Decide whether a list is non-empty

60nonEmpty : (xs : List a) -> Dec (NonEmpty xs)

59nonEmpty : (xs : List a) -> Dec (NonEmpty xs)

61−nonEmpty [] = No nonEmptyNil

60+nonEmpty [] = No absurd

62nonEmpty (x :: xs) = Yes IsNonEmpty

61nonEmpty (x :: xs) = Yes IsNonEmpty

64||| Satisfiable if `k` is a valid index into `xs`

63||| Satisfiable if `k` is a valid index into `xs`

libs/prelude/Prelude/Strings.idr+9−6

@@ -308,12 +308,15 @@ length : String -> Nat

308length = fromInteger . prim__zextInt_BigInt . prim_lenString

309

310||| Returns a substring of a given string

311+|||

311−||| @index The (zero based) index of the string to extract. If this is

312+||| @ index The (zero based) index of the string to extract. If this is

312−||| beyond the end of the String, the function returns the empty string.

313+||| beyond the end of the string, the function returns the empty

314+||| string.

313−||| @len The desired length of the substring. Truncated if this exceeds

315+||| @ len The desired length of the substring. Truncated if this exceeds

314−||| the length of the input.

316+||| the length of the input.

317+||| @ subject The string to return a portion of

315−substr : (index : Nat) -> (len : Nat) -> String -> String

318+substr : (index : Nat) -> (len : Nat) -> (subject : String) -> String

316−substr i len = pack . List.take len . drop i . unpack

319+substr i len subject = prim__strSubstr (cast i) (cast len) subject

317

320

318||| Lowercases all characters in the string.

321||| Lowercases all characters in the string.

319|||

322|||

rts/idris_rts.c+11

@@ -594,6 +594,17 @@ VAL idris_strIndex(VM* vm, VAL str, VAL i) {

594 return MKINT((i_int)idx);

595}

596

597+VAL idris_substr(VM* vm, VAL offset, VAL length, VAL str) {

598+ char *start = idris_utf8_advance(GETSTR(str), GETINT(offset));

599+ char *end = idris_utf8_advance(start, GETINT(length));

600+ Closure* newstr = allocate(sizeof(Closure) + (end - start) +1, 0);

601+ SETTY(newstr, STRING);

602+ newstr -> info.str = (char*)newstr + sizeof(Closure);

603+ memcpy(newstr -> info.str, start, end - start);

604+ *(newstr -> info.str + (end - start) + 1) = '\0';

605+ return newstr;

606+}

607+

597VAL idris_strRev(VM* vm, VAL str) {

608VAL idris_strRev(VM* vm, VAL str) {

598 char *xstr = GETSTR(str);

609 char *xstr = GETSTR(str);

599 Closure* cl = allocate(sizeof(Closure) +

610 Closure* cl = allocate(sizeof(Closure) +

rts/idris_rts.h+1

@@ -314,6 +314,7 @@ VAL idris_strTail(VM* vm, VAL str);

314VAL idris_strCons(VM* vm, VAL x, VAL xs);

315VAL idris_strIndex(VM* vm, VAL str, VAL i);

316VAL idris_strRev(VM* vm, VAL str);

317+VAL idris_substr(VM* vm, VAL offset, VAL length, VAL str);

317

318

318// system infox

319// system infox

319// used indices:

320// used indices:

rts/idris_utf8.c+26

@@ -78,6 +78,32 @@ unsigned idris_utf8_index(char* s, int idx) {

78 return top;

79}

81+char* idris_utf8_advance(char* str, int i) {

82+ while (i > 0 && *str != '\0') {

83+ // In a UTF8 single-byte char, the highest bit is 0. In the

84+ // first byte of a multi-byte char, the highest two bits are

85+ // 11, but the rest of the bytes start with 10. So we can

86+ // decrement our character counter when we see something other

87+ // than 10 at the front.

88+

89+ // This is a bit of an overapproximation, as invalid multibyte

90+ // sequences that are too long will be treated as if they are

91+ // OK, but it's always paying attention to null-termination.

92+ if ((*str & 0xc0) != 0x80) {

93+ i--;

94+ }

95+ str++;

96+ }

97+ // Now we've found the first byte of the last character. Advance

98+ // to the end of it, or the end of the string, whichever is first.

99+ // Here, we don't risk overrunning the end of the string because

100+ // ('\0' & 0xc0) != 0x80.

101+ while ((*str & 0xc0) == 0x80) { str++; }

102+

103+ return str;

104+}

105+

106+

81char* idris_utf8_fromChar(int x) {

107char* idris_utf8_fromChar(int x) {

82 char* str;

108 char* str;

83 int bytes = 0, top = 0;

109 int bytes = 0, top = 0;

rts/idris_utf8.h+3−1

@@ -18,5 +18,7 @@ unsigned idris_utf8_index(char* s, int j);

18char* idris_utf8_fromChar(int x);

19// Reverse a UTF8 encoded string, putting the result in 'result'

20char* idris_utf8_rev(char* s, char* result);

21−

21+// Advance a pointer into a string by i UTF8 characters.

22+// Return original pointer if i <= 0.

23+char* idris_utf8_advance(char* str, int i);

22#endif

24#endif

src/IRTS/CodegenC.hs+1

@@ -559,6 +559,7 @@ doOp v LStrCons [x, y] = v ++ "idris_strCons(vm, " ++ creg x ++ "," ++ creg y ++

559doOp v LStrIndex [x, y] = v ++ "idris_strIndex(vm, " ++ creg x ++ "," ++ creg y ++ ")"

560doOp v LStrRev [x] = v ++ "idris_strRev(vm, " ++ creg x ++ ")"

561doOp v LStrLen [x] = v ++ "idris_strlen(vm, " ++ creg x ++ ")"

562+doOp v LStrSubstr [x,y,z] = v ++ "idris_substr(vm, " ++ creg x ++ "," ++ creg y ++ "," ++ creg z ++ ")"

562

563

563doOp v LFork [x] = v ++ "MKPTR(vm, vmThread(vm, " ++ cname (sMN 0 "EVAL") ++ ", " ++ creg x ++ "))"

564doOp v LFork [x] = v ++ "MKPTR(vm, vmThread(vm, " ++ cname (sMN 0 "EVAL") ++ ", " ++ creg x ++ "))"

564doOp v LPar [x] = v ++ creg x -- "MKPTR(vm, vmThread(vm, " ++ cname (MN 0 "EVAL") ++ ", " ++ creg x ++ "))"

565doOp v LPar [x] = v ++ creg x -- "MKPTR(vm, vmThread(vm, " ++ cname (MN 0 "EVAL") ++ ", " ++ creg x ++ "))"

src/IRTS/CodegenJavaScript.hs+9

@@ -1140,6 +1140,15 @@ jsOP _ reg op args = JSAssign (translateReg reg) jsOP'

1140 JSNum (JSInt 1),

1141 JSBinOp "-" (JSProj v "length") (JSNum (JSInt 1))

1142 ]

1143+ | LStrSubstr <- op

1144+ , (offset:length:string:_) <- args =

1145+ let off = translateReg offset

1146+ len = translateReg length

1147+ str = translateReg string

1148+ in JSApp (JSProj str "substr") [

1149+ jsCall "Math.max" [JSNum (JSInt 0), off],

1150+ jsCall "Math.max" [JSNum (JSInt 0), len]

1151+ ]

1143

1152

1144 | LSystemInfo <- op

1153 | LSystemInfo <- op

1145 , (arg:_) <- args = jsCall "i$systemInfo" [translateReg arg]

1154 , (arg:_) <- args = jsCall "i$systemInfo" [translateReg arg]

src/IRTS/Compiler.hs+4−84

@@ -44,8 +44,7 @@ import System.Directory

44import System.Environment

45import System.FilePath ((</>), addTrailingPathSeparator)

47−-- | Given a 'main' term to compiler, return the IRs which can be used to

47+-- | Compile to simplified forms and return CodegenInfo

48−-- generate code.

49compile :: Codegen -> FilePath -> Maybe Term -> Idris CodegenInfo

48compile :: Codegen -> FilePath -> Maybe Term -> Idris CodegenInfo

50compile codegen f mtm

49compile codegen f mtm

51 = do checkMVs -- check for undefined metavariables

50 = do checkMVs -- check for undefined metavariables

@@ -74,7 +73,7 @@ compile codegen f mtm

74 Just _ -> False

73 Just _ -> False

76 let defs = defsIn ++ maindef

75 let defs = defsIn ++ maindef

77− -- iputStrLn $ showSep "\n" (map show defs)

76+

78 -- Inlined top level LDecl made here

77 -- Inlined top level LDecl made here

79 let defsInlined = inlineAll defs

78 let defsInlined = inlineAll defs

80 let defsUniq = map (allocUnique (addAlist defsInlined emptyContext))

79 let defsUniq = map (allocUnique (addAlist defsInlined emptyContext))

@@ -90,7 +89,7 @@ compile codegen f mtm

90 let defuns = inline defuns_in

89 let defuns = inline defuns_in

91 logLvl 5 $ show defuns

90 logLvl 5 $ show defuns

92 logLvl 1 "Resolving variables for CG"

91 logLvl 1 "Resolving variables for CG"

93− -- iputStrLn $ showSep "\n" (map show (toAlist defuns))

92+

94 let checked = simplifyDefs defuns (toAlist defuns)

93 let checked = simplifyDefs defuns (toAlist defuns)

95 outty <- outputTy

94 outty <- outputTy

96 dumpCases <- getDumpCases

95 dumpCases <- getDumpCases

@@ -109,13 +108,6 @@ compile codegen f mtm

109 hdrs impdirs objs libs flags

108 hdrs impdirs objs libs flags

110 NONE c (toAlist defuns)

109 NONE c (toAlist defuns)

111 tagged iface exports

110 tagged iface exports

112−-- runIO $ case codegen of

113−-- ViaC -> codegenC cginfo

114−-- ViaJava -> codegenJava cginfo

115−-- ViaJavaScript -> codegenJavaScript cginfo

116−-- ViaNode -> codegenNode cginfo

117−-- ViaLLVM -> codegenLLVM cginfo

118−-- Bytecode -> dumpBC c f

119 Error e -> ierror e

111 Error e -> ierror e

120 where checkMVs = do i <- getIState

112 where checkMVs = do i <- getIState

121 case map fst (idris_metavars i) \\ primDefs of

113 case map fst (idris_metavars i) \\ primDefs of

@@ -125,9 +117,6 @@ compile codegen f mtm

125 case idris_totcheckfail i of

117 case idris_totcheckfail i of

126 [] -> return ()

118 [] -> return ()

127 ((fc, msg):fs) -> ierror . At fc . Msg $ "Cannot compile:\n " ++ msg

119 ((fc, msg):fs) -> ierror . At fc . Msg $ "Cannot compile:\n " ++ msg

128− inDir d h = do let f = d </> h

129− ex <- doesFileExist f

130− if ex then return f else return h

131

120

132generate :: Codegen -> FilePath -> CodegenInfo -> IO ()

121generate :: Codegen -> FilePath -> CodegenInfo -> IO ()

133generate codegen mainmod ir

122generate codegen mainmod ir

@@ -136,7 +125,7 @@ generate codegen mainmod ir

136 Via "c" -> codegenC ir

125 Via "c" -> codegenC ir

137 -- Any external code generator

126 -- Any external code generator

138 Via cg -> do let cmd = "idris-codegen-" ++ cg

127 Via cg -> do let cmd = "idris-codegen-" ++ cg

139− args = ["--yes-really", mainmod, "-o", outputFile ir] ++ compilerFlags ir

128+ args = [mainmod, "-o", outputFile ir] ++ compilerFlags ir

140 exit <- rawSystem cmd args

129 exit <- rawSystem cmd args

141 when (exit /= ExitSuccess) $

130 when (exit /= ExitSuccess) $

142 putStrLn ("FAILURE: " ++ show cmd ++ " " ++ show args)

131 putStrLn ("FAILURE: " ++ show cmd ++ " " ++ show args)

@@ -485,75 +474,6 @@ doForeign vs env (ret : fname : world : args)

485 deNS n = n

474 deNS n = n

486doForeign vs env xs = ifail "Badly formed foreign function call"

475doForeign vs env xs = ifail "Badly formed foreign function call"

487

476

488−{-

489− - | (_, (Constant (Str fgnName) : fgnArgTys : ret : [])) <- unApply fgn

490− = case getFTypes fgnArgTys of

491− Nothing -> ifail $ "Foreign type specification is not a constant list: " ++ show (fgn:args)

492− Just tys -> do

493− args' <- mapM (irTerm vs env) (init args)

494− return $ LForeign LANG_C (mkIty' ret) fgnName (zip tys args')

495−

496− | otherwise = ifail "Badly formed foreign function call"

497− where

498− getFTypes :: TT Name -> Maybe [FType]

499− getFTypes tm = case unApply tm of

500− -- nil : {a : Type} -> List a

501− (nil, [_]) -> Just []

502− -- cons : {a : Type} -> a -> List a -> List a

503− (cons, [_, ty, xs]) -> (mkIty' ty :) <$> getFTypes xs

504− _ -> Nothing

505−

506− mkIty' (P _ (UN ty) _) = mkIty (str ty)

507− mkIty' (App (P _ (UN fi) _) (P _ (UN intTy) _))

508− | fi == txt "FIntT"

509− = mkIntIty (str intTy)

510−

511− mkIty' (App (App (P _ (UN ff) _) _) (App (P _ (UN fa) _) (App (P _ (UN io) _) _)))

512− | ff == txt "FFunction"

513− , fa == txt "FAny"

514− , io == txt "IO"

515− = FFunctionIO

516−

517− mkIty' (App (App (P _ (UN ff) _) _) _)

518− | ff == txt "FFunction"

519− = FFunction

520−

521− mkIty' _ = FAny

522−

523− -- would be better if these FInt types were evaluated at compile time

524− -- TODO: add %eval directive for such things

525− -- Issue #1742 on the issue tracker.

526− -- https://github.com/idris-lang/Idris-dev/issues/1742

527− mkIty "FFloat" = FArith ATFloat

528− mkIty "FInt" = mkIntIty "ITNative"

529− mkIty "FChar" = mkIntIty "ITChar"

530− mkIty "FByte" = mkIntIty "IT8"

531− mkIty "FShort" = mkIntIty "IT16"

532− mkIty "FLong" = mkIntIty "IT64"

533− mkIty "FBits8" = mkIntIty "IT8"

534− mkIty "FBits16" = mkIntIty "IT16"

535− mkIty "FBits32" = mkIntIty "IT32"

536− mkIty "FBits64" = mkIntIty "IT64"

537− mkIty "FString" = FString

538− mkIty "FPtr" = FPtr

539− mkIty "FManagedPtr" = FManagedPtr

540− mkIty "FUnit" = FUnit

541− mkIty "FFunction" = FFunction

542− mkIty "FFunctionIO" = FFunctionIO

543− mkIty "FBits8x16" = FArith (ATInt (ITVec IT8 16))

544− mkIty "FBits16x8" = FArith (ATInt (ITVec IT16 8))

545− mkIty "FBits32x4" = FArith (ATInt (ITVec IT32 4))

546− mkIty "FBits64x2" = FArith (ATInt (ITVec IT64 2))

547− mkIty x = error $ "Unknown type " ++ x

548−

549− mkIntIty "ITNative" = FArith (ATInt ITNative)

550− mkIntIty "ITChar" = FArith (ATInt ITChar)

551− mkIntIty "IT8" = FArith (ATInt (ITFixed IT8))

552− mkIntIty "IT16" = FArith (ATInt (ITFixed IT16))

553− mkIntIty "IT32" = FArith (ATInt (ITFixed IT32))

554− mkIntIty "IT64" = FArith (ATInt (ITFixed IT64))

555−-}

556−

557irTree :: [Name] -> SC -> Idris LExp

477irTree :: [Name] -> SC -> Idris LExp

558irTree args tree = do

478irTree args tree = do

559 logLvl 3 $ "Compiling " ++ show args ++ "\n" ++ show tree

479 logLvl 3 $ "Compiling " ++ show args ++ "\n" ++ show tree

src/IRTS/Lang.hs+1−1

@@ -74,7 +74,7 @@ data PrimFn = LPlus ArithTy | LMinus ArithTy | LTimes ArithTy

75 | LFSqrt | LFFloor | LFCeil | LFNegate

78 | LReadStr | LWriteStr

80 -- system info

src/Idris/AbsSyntax.hs+146−112

@@ -31,6 +31,8 @@ import Data.Maybe

31import qualified Data.Set as S

32import Data.Word (Word)

34+import Data.Generics.Uniplate.Data (descend, descendM)

35+

34import Debug.Trace

36import Debug.Trace

36import System.IO.Error(isUserError, ioeGetErrorString, tryIOError)

38import System.IO.Error(isUserError, ioeGetErrorString, tryIOError)

@@ -800,6 +802,18 @@ setEvalTypes n = do i <- getIState

800 let opt' = opts { opt_evaltypes = n }

802 let opt' = opts { opt_evaltypes = n }

801 putIState $ i { idris_options = opt' }

803 putIState $ i { idris_options = opt' }

802

804

805+getDesugarNats :: Idris Bool

806+getDesugarNats = do i <- getIState

807+ let opts = idris_options i

808+ return (opt_desugarnats opts)

809+

810+

811+setDesugarNats :: Bool -> Idris ()

812+setDesugarNats n = do i <- getIState

813+ let opts = idris_options i

814+ let opt' = opts { opt_desugarnats = n }

815+ putIState $ i { idris_options = opt' }

816+

803setQuiet :: Bool -> Idris ()

817setQuiet :: Bool -> Idris ()

804setQuiet q = do i <- getIState

818setQuiet q = do i <- getIState

805 let opts = idris_options i

819 let opts = idris_options i

@@ -980,7 +994,7 @@ expandParams :: (Name -> Name) -> [(Name, PTerm)] ->

980 [Name] -> -- all names

994 [Name] -> -- all names

981 [Name] -> -- names with no declaration

995 [Name] -> -- names with no declaration

982 PTerm -> PTerm

996 PTerm -> PTerm

983−expandParams dec ps ns infs tm = en tm

997+expandParams dec ps ns infs tm = en 0 tm

984 where

998 where

985 -- if we shadow a name (say in a lambda binding) that is used in a call to

999 -- if we shadow a name (say in a lambda binding) that is used in a call to

986 -- a lifted function, we need access to both names - once in the scope of the

1000 -- a lifted function, we need access to both names - once in the scope of the

@@ -992,69 +1006,76 @@ expandParams dec ps ns infs tm = en tm

992 mkShadow (MN i n) = MN (i+1) n

1006 mkShadow (MN i n) = MN (i+1) n

993 mkShadow (NS x s) = NS (mkShadow x) s

1007 mkShadow (NS x s) = NS (mkShadow x) s

994

1008

1009+ en :: Int -- ^ The quotation level - only transform terms that are used, not terms

1010+ -- that are merely mentioned.

1011+ -> PTerm -> PTerm

995− en (PLam fc n nfc t s)

1012+ en 0 (PLam fc n nfc t s)

996 | n `elem` (map fst ps ++ ns)

1013 | n `elem` (map fst ps ++ ns)

997 = let n' = mkShadow n in

1014 = let n' = mkShadow n in

998− PLam fc n' nfc (en t) (en (shadow n n' s))

1015+ PLam fc n' nfc (en 0 t) (en 0 (shadow n n' s))

999− | otherwise = PLam fc n nfc (en t) (en s)

1016+ | otherwise = PLam fc n nfc (en 0 t) (en 0 s)

1000− en (PPi p n nfc t s)

1017+ en 0 (PPi p n nfc t s)

1001 | n `elem` (map fst ps ++ ns)

1018 | n `elem` (map fst ps ++ ns)

1002 = let n' = mkShadow n in -- TODO THINK SHADOWING TacImp?

1019 = let n' = mkShadow n in -- TODO THINK SHADOWING TacImp?

1003− PPi (enTacImp p) n' nfc (en t) (en (shadow n n' s))

1020+ PPi (enTacImp 0 p) n' nfc (en 0 t) (en 0 (shadow n n' s))

1004− | otherwise = PPi (enTacImp p) n nfc (en t) (en s)

1021+ | otherwise = PPi (enTacImp 0 p) n nfc (en 0 t) (en 0 s)

1005− en (PLet fc n nfc ty v s)

1022+ en 0 (PLet fc n nfc ty v s)

1006 | n `elem` (map fst ps ++ ns)

1023 | n `elem` (map fst ps ++ ns)

1007 = let n' = mkShadow n in

1024 = let n' = mkShadow n in

1008− PLet fc n' nfc (en ty) (en v) (en (shadow n n' s))

1025+ PLet fc n' nfc (en 0 ty) (en 0 v) (en 0 (shadow n n' s))

1009− | otherwise = PLet fc n nfc (en ty) (en v) (en s)

1026+ | otherwise = PLet fc n nfc (en 0 ty) (en 0 v) (en 0 s)

1010 -- FIXME: Should only do this in a type signature!

1027 -- FIXME: Should only do this in a type signature!

1011− en (PDPair f hls p (PRef f' fcs n) t r)

1028+ en 0 (PDPair f hls p (PRef f' fcs n) t r)

1012 | n `elem` (map fst ps ++ ns) && t /= Placeholder

1029 | n `elem` (map fst ps ++ ns) && t /= Placeholder

1013 = let n' = mkShadow n in

1030 = let n' = mkShadow n in

1014− PDPair f hls p (PRef f' fcs n') (en t) (en (shadow n n' r))

1031+ PDPair f hls p (PRef f' fcs n') (en 0 t) (en 0 (shadow n n' r))

1015− en (PRewrite f l r g) = PRewrite f (en l) (en r) (fmap en g)

1032+ en 0 (PRewrite f l r g) = PRewrite f (en 0 l) (en 0 r) (fmap (en 0) g)

1016− en (PTyped l r) = PTyped (en l) (en r)

1033+ en 0 (PTyped l r) = PTyped (en 0 l) (en 0 r)

1017− en (PPair f hls p l r) = PPair f hls p (en l) (en r)

1034+ en 0 (PPair f hls p l r) = PPair f hls p (en 0 l) (en 0 r)

1018− en (PDPair f hls p l t r) = PDPair f hls p (en l) (en t) (en r)

1035+ en 0 (PDPair f hls p l t r) = PDPair f hls p (en 0 l) (en 0 t) (en 0 r)

1019− en (PAlternative ns a as) = PAlternative ns a (map en as)

1036+ en 0 (PAlternative ns a as) = PAlternative ns a (map (en 0) as)

1020− en (PHidden t) = PHidden (en t)

1037+ en 0 (PHidden t) = PHidden (en 0 t)

1021− en (PUnifyLog t) = PUnifyLog (en t)

1038+ en 0 (PUnifyLog t) = PUnifyLog (en 0 t)

1022− en (PDisamb ds t) = PDisamb ds (en t)

1039+ en 0 (PDisamb ds t) = PDisamb ds (en 0 t)

1023− en (PNoImplicits t) = PNoImplicits (en t)

1040+ en 0 (PNoImplicits t) = PNoImplicits (en 0 t)

1024− en (PDoBlock ds) = PDoBlock (map (fmap en) ds)

1041+ en 0 (PDoBlock ds) = PDoBlock (map (fmap (en 0)) ds)

1025− en (PProof ts) = PProof (map (fmap en) ts)

1042+ en 0 (PProof ts) = PProof (map (fmap (en 0)) ts)

1026− en (PTactics ts) = PTactics (map (fmap en) ts)

1043+ en 0 (PTactics ts) = PTactics (map (fmap (en 0)) ts)

1027−

1044+

1028− en (PQuote (Var n))

1045+ en 0 (PQuote (Var n))

1029 | n `nselem` ns = PQuote (Var (dec n))

1046 | n `nselem` ns = PQuote (Var (dec n))

1030− en (PApp fc (PInferRef fc' hl n) as)

1047+ en 0 (PApp fc (PInferRef fc' hl n) as)

1031 | n `nselem` ns = PApp fc (PInferRef fc' hl (dec n))

1048 | n `nselem` ns = PApp fc (PInferRef fc' hl (dec n))

1032− (map (pexp . (PRef fc hl)) (map fst ps) ++ (map (fmap en) as))

1049+ (map (pexp . (PRef fc hl)) (map fst ps) ++ (map (fmap (en 0)) as))

1033− en (PApp fc (PRef fc' hl n) as)

1050+ en 0 (PApp fc (PRef fc' hl n) as)

1034 | n `elem` infs = PApp fc (PInferRef fc' hl (dec n))

1051 | n `elem` infs = PApp fc (PInferRef fc' hl (dec n))

1035− (map (pexp . (PRef fc hl)) (map fst ps) ++ (map (fmap en) as))

1052+ (map (pexp . (PRef fc hl)) (map fst ps) ++ (map (fmap (en 0)) as))

1036 | n `nselem` ns = PApp fc (PRef fc' hl (dec n))

1053 | n `nselem` ns = PApp fc (PRef fc' hl (dec n))

1037− (map (pexp . (PRef fc hl)) (map fst ps) ++ (map (fmap en) as))

1054+ (map (pexp . (PRef fc hl)) (map fst ps) ++ (map (fmap (en 0)) as))

1038− en (PAppBind fc (PRef fc' hl n) as)

1055+ en 0 (PAppBind fc (PRef fc' hl n) as)

1039 | n `elem` infs = PAppBind fc (PInferRef fc' hl (dec n))

1056 | n `elem` infs = PAppBind fc (PInferRef fc' hl (dec n))

1040− (map (pexp . (PRef fc hl)) (map fst ps) ++ (map (fmap en) as))

1057+ (map (pexp . (PRef fc hl)) (map fst ps) ++ (map (fmap (en 0)) as))

1041 | n `nselem` ns = PAppBind fc (PRef fc' hl (dec n))

1058 | n `nselem` ns = PAppBind fc (PRef fc' hl (dec n))

1042− (map (pexp . (PRef fc hl)) (map fst ps) ++ (map (fmap en) as))

1059+ (map (pexp . (PRef fc hl)) (map fst ps) ++ (map (fmap (en 0)) as))

1043− en (PRef fc hl n)

1060+ en 0 (PRef fc hl n)

1044 | n `elem` infs = PApp fc (PInferRef fc hl (dec n))

1061 | n `elem` infs = PApp fc (PInferRef fc hl (dec n))

1045 (map (pexp . (PRef fc hl)) (map fst ps))

1062 (map (pexp . (PRef fc hl)) (map fst ps))

1046 | n `nselem` ns = PApp fc (PRef fc hl (dec n))

1063 | n `nselem` ns = PApp fc (PRef fc hl (dec n))

1047 (map (pexp . (PRef fc hl)) (map fst ps))

1064 (map (pexp . (PRef fc hl)) (map fst ps))

1048− en (PInferRef fc hl n)

1065+ en 0 (PInferRef fc hl n)

1049 | n `nselem` ns = PApp fc (PInferRef fc hl (dec n))

1066 | n `nselem` ns = PApp fc (PInferRef fc hl (dec n))

1050 (map (pexp . (PRef fc hl)) (map fst ps))

1067 (map (pexp . (PRef fc hl)) (map fst ps))

1051− en (PApp fc f as) = PApp fc (en f) (map (fmap en) as)

1068+ en 0 (PApp fc f as) = PApp fc (en 0 f) (map (fmap (en 0)) as)

1052− en (PAppBind fc f as) = PAppBind fc (en f) (map (fmap en) as)

1069+ en 0 (PAppBind fc f as) = PAppBind fc (en 0 f) (map (fmap (en 0)) as)

1053− en (PCase fc c os) = PCase fc (en c) (map (pmap en) os)

1070+ en 0 (PCase fc c os) = PCase fc (en 0 c) (map (pmap (en 0)) os)

1054− en (PIfThenElse fc c t f) = PIfThenElse fc (en c) (en t) (en f)

1071+ en 0 (PIfThenElse fc c t f) = PIfThenElse fc (en 0 c) (en 0 t) (en 0 f)

1055− en (PRunElab fc tm ns) = PRunElab fc (en tm) ns

1072+ en 0 (PRunElab fc tm ns) = PRunElab fc (en 0 tm) ns

1056− en (PConstSugar fc tm) = PConstSugar fc (en tm)

1073+ en 0 (PConstSugar fc tm) = PConstSugar fc (en 0 tm)

1057− en t = t

1074+

1075+ en ql (PQuasiquote tm ty) = PQuasiquote (en (ql + 1) tm) (fmap (en ql) ty)

1076+ en ql (PUnquote tm) = PUnquote (en (ql - 1) tm)

1077+

1078+ en ql t = descend (en ql) t

1058

1079

1059 nselem x [] = False

1080 nselem x [] = False

1060 nselem x (y : xs) | nseq x y = True

1081 nselem x (y : xs) | nseq x y = True

@@ -1062,8 +1083,8 @@ expandParams dec ps ns infs tm = en tm

1062

1083

1063 nseq x y = nsroot x == nsroot y

1084 nseq x y = nsroot x == nsroot y

1064

1085

1065− enTacImp (TacImp aos st scr) = TacImp aos st (en scr)

1086+ enTacImp ql (TacImp aos st scr) = TacImp aos st (en ql scr)

1066− enTacImp other = other

1087+ enTacImp ql other = other

1067

1088

1068expandParamsD :: Bool -> -- True = RHS only

1089expandParamsD :: Bool -> -- True = RHS only

1069 IState ->

1090 IState ->

@@ -2102,44 +2123,46 @@ substMatchShadow n shs tm t = sm shs t where

2102 fullApp x = x

2123 fullApp x = x

2103

2124

2104shadow :: Name -> Name -> PTerm -> PTerm

2125shadow :: Name -> Name -> PTerm -> PTerm

2105−shadow n n' t = sm t where

2126+shadow n n' t = sm 0 t where

2106− sm (PRef fc hl x) | n == x = PRef fc hl n'

2127+ sm 0 (PRef fc hl x) | n == x = PRef fc hl n'

2107− sm (PLam fc x xfc t sc) | n /= x = PLam fc x xfc (sm t) (sm sc)

2128+ sm 0 (PLam fc x xfc t sc) | n /= x = PLam fc x xfc (sm 0 t) (sm 0 sc)

2108− | otherwise = PLam fc x xfc (sm t) sc

2129+ | otherwise = PLam fc x xfc (sm 0 t) sc

2109− sm (PPi p x fc t sc) | n /= x = PPi p x fc (sm t) (sm sc)

2130+ sm 0 (PPi p x fc t sc) | n /= x = PPi p x fc (sm 0 t) (sm 0 sc)

2110− | otherwise = PPi p x fc (sm t) sc

2131+ | otherwise = PPi p x fc (sm 0 t) sc

2111− sm (PLet fc x xfc t v sc) | n /= x = PLet fc x xfc (sm t) (sm v) (sm sc)

2132+ sm 0 (PLet fc x xfc t v sc) | n /= x = PLet fc x xfc (sm 0 t) (sm 0 v) (sm 0 sc)

2112− | otherwise = PLet fc x xfc (sm t) (sm v) sc

2133+ | otherwise = PLet fc x xfc (sm 0 t) (sm 0 v) sc

2113− sm (PApp f x as) = PApp f (sm x) (map (fmap sm) as)

2134+ sm 0 (PApp f x as) = PApp f (sm 0 x) (map (fmap (sm 0)) as)

2114− sm (PAppBind f x as) = PAppBind f (sm x) (map (fmap sm) as)

2135+ sm 0 (PAppBind f x as) = PAppBind f (sm 0 x) (map (fmap (sm 0)) as)

2115− sm (PCase f x as) = PCase f (sm x) (map (pmap sm) as)

2136+ sm 0 (PCase f x as) = PCase f (sm 0 x) (map (pmap (sm 0)) as)

2116− sm (PIfThenElse fc c t f) = PIfThenElse fc (sm c) (sm t) (sm f)

2137+ sm 0 (PIfThenElse fc c t f) = PIfThenElse fc (sm 0 c) (sm 0 t) (sm 0 f)

2117− sm (PRewrite f x y tm) = PRewrite f (sm x) (sm y) (fmap sm tm)

2138+ sm 0 (PRewrite f x y tm) = PRewrite f (sm 0 x) (sm 0 y) (fmap (sm 0) tm)

2118− sm (PTyped x y) = PTyped (sm x) (sm y)

2139+ sm 0 (PTyped x y) = PTyped (sm 0 x) (sm 0 y)

2119− sm (PPair f hls p x y) = PPair f hls p (sm x) (sm y)

2140+ sm 0 (PPair f hls p x y) = PPair f hls p (sm 0 x) (sm 0 y)

2120− sm (PDPair f hls p x t y) = PDPair f hls p (sm x) (sm t) (sm y)

2141+ sm 0 (PDPair f hls p x t y) = PDPair f hls p (sm 0 x) (sm 0 t) (sm 0 y)

2121− sm (PAlternative ms a as) = PAlternative ms a (map sm as)

2142+ sm 0 (PAlternative ms a as) = PAlternative ms a (map (sm 0) as)

2122− sm (PTactics ts) = PTactics (map (fmap sm) ts)

2143+ sm 0 (PTactics ts) = PTactics (map (fmap (sm 0)) ts)

2123− sm (PProof ts) = PProof (map (fmap sm) ts)

2144+ sm 0 (PProof ts) = PProof (map (fmap (sm 0)) ts)

2124− sm (PHidden x) = PHidden (sm x)

2145+ sm 0 (PHidden x) = PHidden (sm 0 x)

2125− sm (PUnifyLog x) = PUnifyLog (sm x)

2146+ sm 0 (PUnifyLog x) = PUnifyLog (sm 0 x)

2126− sm (PNoImplicits x) = PNoImplicits (sm x)

2147+ sm 0 (PNoImplicits x) = PNoImplicits (sm 0 x)

2127− sm (PCoerced t) = PCoerced (sm t)

2148+ sm 0 (PCoerced t) = PCoerced (sm 0 t)

2128− sm x = x

2149+ sm ql (PQuasiquote tm ty) = PQuasiquote (sm (ql + 1) tm) (fmap (sm ql) ty)

2150+ sm ql (PUnquote tm) = PUnquote (sm (ql - 1) tm)

2151+ sm ql x = descend (sm ql) x

2129

2152

2130-- | Rename any binders which are repeated (so that we don't have to mess

2153-- | Rename any binders which are repeated (so that we don't have to mess

2131-- about with shadowing anywhere else).

2154-- about with shadowing anywhere else).

2132mkUniqueNames :: [Name] -> [(Name, Name)] -> PTerm -> PTerm

2155mkUniqueNames :: [Name] -> [(Name, Name)] -> PTerm -> PTerm

2133mkUniqueNames env shadows tm

2156mkUniqueNames env shadows tm

2134− = evalState (mkUniq initMap tm) (S.fromList env) where

2157+ = evalState (mkUniq 0 initMap tm) (S.fromList env) where

2135

2158

2136 initMap = M.fromList shadows

2159 initMap = M.fromList shadows

2137

2160

2138 inScope :: S.Set Name

2161 inScope :: S.Set Name

2139 inScope = S.fromList $ boundNamesIn tm

2162 inScope = S.fromList $ boundNamesIn tm

2140

2163

2141− mkUniqA nmap arg = do t' <- mkUniq nmap (getTm arg)

2164+ mkUniqA ql nmap arg = do t' <- mkUniq ql nmap (getTm arg)

2142− return (arg { getTm = t' })

2165+ return (arg { getTm = t' })

2143

2166

2144 -- Initialise the unique name with the environment length (so we're not

2167 -- Initialise the unique name with the environment length (so we're not

2145 -- looking for too long...)

2168 -- looking for too long...)

@@ -2149,10 +2172,11 @@ mkUniqueNames env shadows tm

2149

2172

2150 -- FIXME: Probably ought to do this for completeness! It's fine as

2173 -- FIXME: Probably ought to do this for completeness! It's fine as

2151 -- long as there are no bindings inside tactics though.

2174 -- long as there are no bindings inside tactics though.

2152− mkUniqT nmap tac = return tac

2175+ mkUniqT _ nmap tac = return tac

2153

2176

2177+ mkUniq :: Int -- ^ The number of quotations that we're under

2154− mkUniq :: M.Map Name Name -> PTerm -> State (S.Set Name) PTerm

2178+ -> M.Map Name Name -> PTerm -> State (S.Set Name) PTerm

2155− mkUniq nmap (PLam fc n nfc ty sc)

2179+ mkUniq 0 nmap (PLam fc n nfc ty sc)

2156 = do env <- get

2180 = do env <- get

2157 (n', sc') <-

2181 (n', sc') <-

2158 if n `S.member` env

2182 if n `S.member` env

@@ -2162,10 +2186,10 @@ mkUniqueNames env shadows tm

2162 else return (n, sc)

2186 else return (n, sc)

2163 put (S.insert n' env)

2187 put (S.insert n' env)

2164 let nmap' = M.insert n n' nmap

2188 let nmap' = M.insert n n' nmap

2165− ty' <- mkUniq nmap ty

2189+ ty' <- mkUniq 0 nmap ty

2166− sc'' <- mkUniq nmap' sc'

2190+ sc'' <- mkUniq 0 nmap' sc'

2167 return $! PLam fc n' nfc ty' sc''

2191 return $! PLam fc n' nfc ty' sc''

2168− mkUniq nmap (PPi p n fc ty sc)

2192+ mkUniq 0 nmap (PPi p n fc ty sc)

2169 = do env <- get

2193 = do env <- get

2170 (n', sc') <-

2194 (n', sc') <-

2171 if n `S.member` env

2195 if n `S.member` env

@@ -2175,10 +2199,10 @@ mkUniqueNames env shadows tm

2175 else return (n, sc)

2199 else return (n, sc)

2176 put (S.insert n' env)

2200 put (S.insert n' env)

2177 let nmap' = M.insert n n' nmap

2201 let nmap' = M.insert n n' nmap

2178− ty' <- mkUniq nmap ty

2202+ ty' <- mkUniq 0 nmap ty

2179− sc'' <- mkUniq nmap' sc'

2203+ sc'' <- mkUniq 0 nmap' sc'

2180 return $! PPi p n' fc ty' sc''

2204 return $! PPi p n' fc ty' sc''

2181− mkUniq nmap (PLet fc n nfc ty val sc)

2205+ mkUniq 0 nmap (PLet fc n nfc ty val sc)

2182 = do env <- get

2206 = do env <- get

2183 (n', sc') <-

2207 (n', sc') <-

2184 if n `S.member` env

2208 if n `S.member` env

@@ -2188,28 +2212,28 @@ mkUniqueNames env shadows tm

2188 else return (n, sc)

2212 else return (n, sc)

2189 put (S.insert n' env)

2213 put (S.insert n' env)

2190 let nmap' = M.insert n n' nmap

2214 let nmap' = M.insert n n' nmap

2191− ty' <- mkUniq nmap ty; val' <- mkUniq nmap val

2215+ ty' <- mkUniq 0 nmap ty; val' <- mkUniq 0 nmap val

2192− sc'' <- mkUniq nmap' sc'

2216+ sc'' <- mkUniq 0 nmap' sc'

2193 return $! PLet fc n' nfc ty' val' sc''

2217 return $! PLet fc n' nfc ty' val' sc''

2194− mkUniq nmap (PApp fc t args)

2218+ mkUniq 0 nmap (PApp fc t args)

2195− = do t' <- mkUniq nmap t

2219+ = do t' <- mkUniq 0 nmap t

2196− args' <- mapM (mkUniqA nmap) args

2220+ args' <- mapM (mkUniqA 0 nmap) args

2197 return $! PApp fc t' args'

2221 return $! PApp fc t' args'

2198− mkUniq nmap (PAppBind fc t args)

2222+ mkUniq 0 nmap (PAppBind fc t args)

2199− = do t' <- mkUniq nmap t

2223+ = do t' <- mkUniq 0 nmap t

2200− args' <- mapM (mkUniqA nmap) args

2224+ args' <- mapM (mkUniqA 0 nmap) args

2201 return $! PAppBind fc t' args'

2225 return $! PAppBind fc t' args'

2202− mkUniq nmap (PCase fc t alts)

2226+ mkUniq 0 nmap (PCase fc t alts)

2203− = do t' <- mkUniq nmap t

2227+ = do t' <- mkUniq 0 nmap t

2204− alts' <- mapM (\(x,y)-> do x' <- mkUniq nmap x; y' <- mkUniq nmap y

2228+ alts' <- mapM (\(x,y)-> do x' <- mkUniq 0 nmap x; y' <- mkUniq 0 nmap y

2205 return (x', y')) alts

2229 return (x', y')) alts

2206 return $! PCase fc t' alts'

2230 return $! PCase fc t' alts'

2207− mkUniq nmap (PIfThenElse fc c t f)

2231+ mkUniq 0 nmap (PIfThenElse fc c t f)

2208− = liftM3 (PIfThenElse fc) (mkUniq nmap c) (mkUniq nmap t) (mkUniq nmap f)

2232+ = liftM3 (PIfThenElse fc) (mkUniq 0 nmap c) (mkUniq 0 nmap t) (mkUniq 0 nmap f)

2209− mkUniq nmap (PPair fc hls p l r)

2233+ mkUniq 0 nmap (PPair fc hls p l r)

2210− = do l' <- mkUniq nmap l; r' <- mkUniq nmap r

2234+ = do l' <- mkUniq 0 nmap l; r' <- mkUniq 0 nmap r

2211 return $! PPair fc hls p l' r'

2235 return $! PPair fc hls p l' r'

2212− mkUniq nmap (PDPair fc hls p (PRef fc' hls' n) t sc)

2236+ mkUniq 0 nmap (PDPair fc hls p (PRef fc' hls' n) t sc)

2213 | t /= Placeholder

2237 | t /= Placeholder

2214 = do env <- get

2238 = do env <- get

2215 (n', sc') <- if n `S.member` env

2239 (n', sc') <- if n `S.member` env

@@ -2218,27 +2242,37 @@ mkUniqueNames env shadows tm

2218 else return (n, sc)

2242 else return (n, sc)

2219 put (S.insert n' env)

2243 put (S.insert n' env)

2220 let nmap' = M.insert n n' nmap

2244 let nmap' = M.insert n n' nmap

2221− t' <- mkUniq nmap t

2245+ t' <- mkUniq 0 nmap t

2222− sc'' <- mkUniq nmap' sc'

2246+ sc'' <- mkUniq 0 nmap' sc'

2223 return $! PDPair fc hls p (PRef fc' hls' n') t' sc''

2247 return $! PDPair fc hls p (PRef fc' hls' n') t' sc''

2224− mkUniq nmap (PDPair fc hls p l t r)

2248+ mkUniq 0 nmap (PDPair fc hls p l t r)

2225− = do l' <- mkUniq nmap l; t' <- mkUniq nmap t; r' <- mkUniq nmap r

2249+ = do l' <- mkUniq 0 nmap l; t' <- mkUniq 0 nmap t; r' <- mkUniq 0 nmap r

2226 return $! PDPair fc hls p l' t' r'

2250 return $! PDPair fc hls p l' t' r'

2227− mkUniq nmap (PAlternative ns b as)

2251+ mkUniq 0 nmap (PAlternative ns b as)

2228 -- store the nmap and defer the rest until we've pruned the set

2252 -- store the nmap and defer the rest until we've pruned the set

2229 -- during elaboration

2253 -- during elaboration

2230 = return $ PAlternative (M.toList nmap ++ ns) b as

2254 = return $ PAlternative (M.toList nmap ++ ns) b as

2231− mkUniq nmap (PHidden t) = liftM PHidden (mkUniq nmap t)

2255+ mkUniq 0 nmap (PHidden t) = liftM PHidden (mkUniq 0 nmap t)

2232− mkUniq nmap (PUnifyLog t) = liftM PUnifyLog (mkUniq nmap t)

2256+ mkUniq 0 nmap (PUnifyLog t) = liftM PUnifyLog (mkUniq 0 nmap t)

2233− mkUniq nmap (PDisamb n t) = liftM (PDisamb n) (mkUniq nmap t)

2257+ mkUniq 0 nmap (PDisamb n t) = liftM (PDisamb n) (mkUniq 0 nmap t)

2234− mkUniq nmap (PNoImplicits t) = liftM PNoImplicits (mkUniq nmap t)

2258+ mkUniq 0 nmap (PNoImplicits t) = liftM PNoImplicits (mkUniq 0 nmap t)

2235− mkUniq nmap (PProof ts) = liftM PProof (mapM (mkUniqT nmap) ts)

2259+ mkUniq 0 nmap (PProof ts) = liftM PProof (mapM (mkUniqT 0 nmap) ts)

2236− mkUniq nmap (PTactics ts) = liftM PTactics (mapM (mkUniqT nmap) ts)

2260+ mkUniq 0 nmap (PTactics ts) = liftM PTactics (mapM (mkUniqT 0 nmap) ts)

2237− mkUniq nmap (PRunElab fc ts ns) = liftM (\tm -> PRunElab fc tm ns) (mkUniq nmap ts)

2261+ mkUniq 0 nmap (PRunElab fc ts ns) = liftM (\tm -> PRunElab fc tm ns) (mkUniq 0 nmap ts)

2238− mkUniq nmap (PConstSugar fc tm) = liftM (PConstSugar fc) (mkUniq nmap tm)

2262+ mkUniq 0 nmap (PConstSugar fc tm) = liftM (PConstSugar fc) (mkUniq 0 nmap tm)

2239− mkUniq nmap (PCoerced tm) = liftM PCoerced (mkUniq nmap tm)

2263+ mkUniq 0 nmap (PCoerced tm) = liftM PCoerced (mkUniq 0 nmap tm)

2240− mkUniq nmap t = return $ shadowAll (M.toList nmap) t

2264+ mkUniq 0 nmap t = return $ shadowAll (M.toList nmap) t

2241 where

2265 where

2242 shadowAll [] t = t

2266 shadowAll [] t = t

2243 shadowAll ((n, n') : ns) t = shadow n n' (shadowAll ns t)

2267 shadowAll ((n, n') : ns) t = shadow n n' (shadowAll ns t)

2244

2268

2269+ mkUniq ql nmap (PQuasiquote tm ty) =

2270+ do tm' <- mkUniq (ql + 1) nmap tm

2271+ ty' <- case ty of

2272+ Nothing -> return Nothing

2273+ Just t -> fmap Just $ mkUniq ql nmap t

2274+ return $! PQuasiquote tm' ty'

2275+ mkUniq ql nmap (PUnquote tm) = fmap PUnquote (mkUniq (ql - 1) nmap tm)

2276+

2277+ mkUniq ql nmap tm = descendM (mkUniq ql nmap) tm

2278+

src/Idris/AbsSyntaxTree.hs+169−134

@@ -28,7 +28,7 @@ import qualified Control.Monad.Trans.Class as Trans (lift)

29import Data.Data (Data)

30import Data.Function (on)

31−import Data.Generics.Uniplate.Data (universe)

31+import Data.Generics.Uniplate.Data (universe, children)

32import Data.List hiding (group)

33import Data.Char

34import qualified Data.Map.Strict as M

@@ -90,8 +90,9 @@ data IOption = IOption { opt_logLevel :: Int,

90 opt_autoImport :: [FilePath], -- ^ e.g. Builtins+Prelude

91 opt_optimise :: [Optimisation],

92 opt_printdepth :: Maybe Int,

93− opt_evaltypes :: Bool -- ^ normalise types in :t

93+ opt_evaltypes :: Bool, -- ^ normalise types in :t

94+ opt_desugarnats :: Bool

94− }

95+ }

95 deriving (Show, Eq)

96 deriving (Show, Eq)

97defaultOpts = IOption { opt_logLevel = 0

98defaultOpts = IOption { opt_logLevel = 0

@@ -117,10 +118,12 @@ defaultOpts = IOption { opt_logLevel = 0

117 , opt_optimise = defaultOptimise

118 , opt_optimise = defaultOptimise

118 , opt_printdepth = Just 5000

119 , opt_printdepth = Just 5000

119 , opt_evaltypes = True

120 , opt_evaltypes = True

121+ , opt_desugarnats = False

120 }

122 }

121

123

122data PPOption = PPOption {

124data PPOption = PPOption {

123 ppopt_impl :: Bool -- ^^ whether to show implicits

125 ppopt_impl :: Bool -- ^^ whether to show implicits

126+ , ppopt_desugarnats :: Bool

124 , ppopt_pinames :: Bool -- ^^ whether to show names in pi bindings

127 , ppopt_pinames :: Bool -- ^^ whether to show names in pi bindings

125 , ppopt_depth :: Maybe Int

128 , ppopt_depth :: Maybe Int

126} deriving (Show)

129} deriving (Show)

@@ -133,12 +136,14 @@ defaultOptimise = [PETransform]

133-- | Pretty printing options with default verbosity.

136-- | Pretty printing options with default verbosity.

134defaultPPOption :: PPOption

137defaultPPOption :: PPOption

135defaultPPOption = PPOption { ppopt_impl = False,

138defaultPPOption = PPOption { ppopt_impl = False,

139+ ppopt_desugarnats = False,

136 ppopt_pinames = False,

140 ppopt_pinames = False,

137 ppopt_depth = Just 200 }

141 ppopt_depth = Just 200 }

138

142

139-- | Pretty printing options with the most verbosity.

143-- | Pretty printing options with the most verbosity.

140verbosePPOption :: PPOption

144verbosePPOption :: PPOption

141verbosePPOption = PPOption { ppopt_impl = True,

145verbosePPOption = PPOption { ppopt_impl = True,

146+ ppopt_desugarnats = True,

142 ppopt_pinames = True,

147 ppopt_pinames = True,

143 ppopt_depth = Just 200 }

148 ppopt_depth = Just 200 }

144

149

@@ -147,7 +152,8 @@ ppOption :: IOption -> PPOption

147ppOption opt = PPOption {

152ppOption opt = PPOption {

148 ppopt_impl = opt_showimp opt,

153 ppopt_impl = opt_showimp opt,

149 ppopt_pinames = False,

154 ppopt_pinames = False,

150− ppopt_depth = opt_printdepth opt

155+ ppopt_depth = opt_printdepth opt,

156+ ppopt_desugarnats = opt_desugarnats opt

151}

157}

152

158

153-- | Get pretty printing options from an idris state record.

159-- | Get pretty printing options from an idris state record.

@@ -503,6 +509,7 @@ data Opt = Filename String

503 | AutoSolve -- ^ Automatically issue "solve" tactic in old-style interactive prover

509 | AutoSolve -- ^ Automatically issue "solve" tactic in old-style interactive prover

504 | UseConsoleWidth ConsoleWidth

510 | UseConsoleWidth ConsoleWidth

505 | DumpHighlights

511 | DumpHighlights

512+ | DesugarNats

506 | NoElimDeprecationWarnings -- ^ Don't show deprecation warnings for %elim

513 | NoElimDeprecationWarnings -- ^ Don't show deprecation warnings for %elim

507 | NoOldTacticDeprecationWarnings -- ^ Don't show deprecation warnings for old-style tactics

514 | NoOldTacticDeprecationWarnings -- ^ Don't show deprecation warnings for old-style tactics

508 deriving (Show, Eq)

515 deriving (Show, Eq)

@@ -1655,7 +1662,7 @@ pprintPTerm ppo bnd docArgs infixes = prettySe (ppopt_depth ppo) startPrec bnd

1655 prettySe d p bnd (PPatvar fc n) = pretty n

1662 prettySe d p bnd (PPatvar fc n) = pretty n

1656 prettySe d p bnd e

1663 prettySe d p bnd e

1657 | Just str <- slist d p bnd e = depth d $ str

1664 | Just str <- slist d p bnd e = depth d $ str

1658− | Just n <- snat d p e = depth d $ annotate (AnnData "Nat" "") (text (show n))

1665+ | Just n <- snat ppo d p e = depth d $ annotate (AnnData "Nat" "") (text (show n))

1659 prettySe d p bnd (PRef fc _ n) = prettyName True (ppopt_impl ppo) bnd n

1666 prettySe d p bnd (PRef fc _ n) = prettyName True (ppopt_impl ppo) bnd n

1660 prettySe d p bnd (PLam fc n nfc ty sc) =

1667 prettySe d p bnd (PLam fc n nfc ty sc) =

1661 depth d . bracket p startPrec . group . align . hang 2 $

1668 depth d . bracket p startPrec . group . align . hang 2 $

@@ -1946,15 +1953,20 @@ pprintPTerm ppo bnd docArgs infixes = prettySe (ppopt_depth ppo) startPrec bnd

1946

1953

1947 natns = "Prelude.Nat."

1954 natns = "Prelude.Nat."

1948

1955

1949− snat :: Maybe Int -> Int -> PTerm -> Maybe Integer

1956+ snat :: PPOption -> Maybe Int -> Int -> PTerm -> Maybe Integer

1957+ snat ppo d p e

1958+ | ppopt_desugarnats ppo = Nothing

1959+ | otherwise = snat' d p e

1960+ where

1961+ snat' :: Maybe Int -> Int -> PTerm -> Maybe Integer

1950− snat (Just x) _ _ | x <= 0 = Nothing

1962+ snat' (Just x) _ _ | x <= 0 = Nothing

1951− snat d p (PRef _ _ z)

1963+ snat' d p (PRef _ _ z)

1952− | show z == (natns++"Z") || show z == "Z" = Just 0

1964+ | show z == (natns++"Z") || show z == "Z" = Just 0

1953− snat d p (PApp _ s [PExp {getTm=n}])

1965+ snat' d p (PApp _ s [PExp {getTm=n}])

1954− | show s == (natns++"S") || show s == "S",

1966+ | show s == (natns++"S") || show s == "S",

1955− Just n' <- snat (decD d) p n

1967+ Just n' <- snat' (decD d) p n

1956− = Just $ 1 + n'

1968+ = Just $ 1 + n'

1957− snat _ _ _ = Nothing

1969+ snat' _ _ _ = Nothing

1958

1970

1959 bracket outer inner doc

1971 bracket outer inner doc

1960 | outer > inner = lparen <> doc <> rparen

1972 | outer > inner = lparen <> doc <> rparen

@@ -2167,160 +2179,183 @@ getPArity _ = 0

2167-- Return all names, free or globally bound, in the given term.

2179-- Return all names, free or globally bound, in the given term.

2168

2180

2169allNamesIn :: PTerm -> [Name]

2181allNamesIn :: PTerm -> [Name]

2170−allNamesIn tm = nub $ ni [] tm

2182+allNamesIn tm = nub $ ni 0 [] tm

2171 where -- TODO THINK added niTacImp, but is it right?

2183 where -- TODO THINK added niTacImp, but is it right?

2172− ni env (PRef _ _ n)

2184+ ni 0 env (PRef _ _ n)

2173 | not (n `elem` env) = [n]

2185 | not (n `elem` env) = [n]

2174− ni env (PPatvar _ n) = [n]

2186+ ni 0 env (PPatvar _ n) = [n]

2175− ni env (PApp _ f as) = ni env f ++ concatMap (ni env) (map getTm as)

2187+ ni 0 env (PApp _ f as) = ni 0 env f ++ concatMap (ni 0 env) (map getTm as)

2176− ni env (PAppBind _ f as) = ni env f ++ concatMap (ni env) (map getTm as)

2188+ ni 0 env (PAppBind _ f as) = ni 0 env f ++ concatMap (ni 0 env) (map getTm as)

2177− ni env (PCase _ c os) = ni env c ++ concatMap (ni env) (map snd os)

2189+ ni 0 env (PCase _ c os) = ni 0 env c ++ concatMap (ni 0 env) (map snd os)

2178− ni env (PIfThenElse _ c t f) = ni env c ++ ni env t ++ ni env f

2190+ ni 0 env (PIfThenElse _ c t f) = ni 0 env c ++ ni 0 env t ++ ni 0 env f

2179− ni env (PLam fc n _ ty sc) = ni env ty ++ ni (n:env) sc

2191+ ni 0 env (PLam fc n _ ty sc) = ni 0 env ty ++ ni 0 (n:env) sc

2180− ni env (PPi p n _ ty sc) = niTacImp env p ++ ni env ty ++ ni (n:env) sc

2192+ ni 0 env (PPi p n _ ty sc) = niTacImp 0 env p ++ ni 0 env ty ++ ni 0 (n:env) sc

2181− ni env (PLet _ n _ ty val sc) = ni env ty ++ ni env val ++ ni (n:env) sc

2193+ ni 0 env (PLet _ n _ ty val sc) = ni 0 env ty ++ ni 0 env val ++ ni 0 (n:env) sc

2182− ni env (PHidden tm) = ni env tm

2194+ ni 0 env (PHidden tm) = ni 0 env tm

2183− ni env (PRewrite _ l r _) = ni env l ++ ni env r

2195+ ni 0 env (PRewrite _ l r _) = ni 0 env l ++ ni 0 env r

2184− ni env (PTyped l r) = ni env l ++ ni env r

2196+ ni 0 env (PTyped l r) = ni 0 env l ++ ni 0 env r

2185− ni env (PPair _ _ _ l r) = ni env l ++ ni env r

2197+ ni 0 env (PPair _ _ _ l r) = ni 0 env l ++ ni 0 env r

2186− ni env (PDPair _ _ _ (PRef _ _ n) Placeholder r) = n : ni env r

2198+ ni 0 env (PDPair _ _ _ (PRef _ _ n) Placeholder r) = n : ni 0 env r

2187− ni env (PDPair _ _ _ (PRef _ _ n) t r) = ni env t ++ ni (n:env) r

2199+ ni 0 env (PDPair _ _ _ (PRef _ _ n) t r) = ni 0 env t ++ ni 0 (n:env) r

2188− ni env (PDPair _ _ _ l t r) = ni env l ++ ni env t ++ ni env r

2200+ ni 0 env (PDPair _ _ _ l t r) = ni 0 env l ++ ni 0 env t ++ ni 0 env r

2189− ni env (PAlternative ns a ls) = concatMap (ni env) ls

2201+ ni 0 env (PAlternative ns a ls) = concatMap (ni 0 env) ls

2190− ni env (PUnifyLog tm) = ni env tm

2202+ ni 0 env (PUnifyLog tm) = ni 0 env tm

2191− ni env (PDisamb _ tm) = ni env tm

2203+ ni 0 env (PDisamb _ tm) = ni 0 env tm

2192− ni env (PNoImplicits tm) = ni env tm

2204+ ni 0 env (PNoImplicits tm) = ni 0 env tm

2193− ni env _ = []

2205+

2194−

2206+ ni i env (PQuasiquote tm ty) = ni (i+1) env tm ++ maybe [] (ni i env) ty

2207+ ni i env (PUnquote tm) = ni (i - 1) env tm

2208+

2209+ ni i env tm = concatMap (ni i env) (children tm)

2210+

2195− niTacImp env (TacImp _ _ scr) = ni env scr

2211+ niTacImp i env (TacImp _ _ scr) = ni i env scr

2196− niTacImp _ _ = []

2212+ niTacImp _ _ _ = []

2197

2213

2198

2214

2199-- Return all names defined in binders in the given term

2215-- Return all names defined in binders in the given term

2200boundNamesIn :: PTerm -> [Name]

2216boundNamesIn :: PTerm -> [Name]

2201−boundNamesIn tm = S.toList (ni S.empty tm)

2217+boundNamesIn tm = S.toList (ni 0 S.empty tm)

2202 where -- TODO THINK Added niTacImp, but is it right?

2218 where -- TODO THINK Added niTacImp, but is it right?

2219+ ni :: Int -> S.Set Name -> PTerm -> S.Set Name

2203− ni set (PApp _ f as) = niTms (ni set f) (map getTm as)

2220+ ni 0 set (PApp _ f as) = niTms 0 (ni 0 set f) (map getTm as)

2204− ni set (PAppBind _ f as) = niTms (ni set f) (map getTm as)

2221+ ni 0 set (PAppBind _ f as) = niTms 0 (ni 0 set f) (map getTm as)

2205− ni set (PCase _ c os) = niTms (ni set c) (map snd os)

2222+ ni 0 set (PCase _ c os) = niTms 0 (ni 0 set c) (map snd os)

2206− ni set (PIfThenElse _ c t f) = niTms set [c, t, f]

2223+ ni 0 set (PIfThenElse _ c t f) = niTms 0 set [c, t, f]

2207− ni set (PLam fc n _ ty sc) = S.insert n $ ni (ni set ty) sc

2224+ ni 0 set (PLam fc n _ ty sc) = S.insert n $ ni 0 (ni 0 set ty) sc

2208− ni set (PLet fc n nfc ty val sc) = S.insert n $ ni (ni (ni set ty) val) sc

2225+ ni 0 set (PLet fc n nfc ty val sc) = S.insert n $ ni 0 (ni 0 (ni 0 set ty) val) sc

2209− ni set (PPi p n _ ty sc) = niTacImp (S.insert n $ ni (ni set ty) sc) p

2226+ ni 0 set (PPi p n _ ty sc) = niTacImp 0 (S.insert n $ ni 0 (ni 0 set ty) sc) p

2210− ni set (PRewrite _ l r _) = ni (ni set l) r

2227+ ni 0 set (PRewrite _ l r _) = ni 0 (ni 0 set l) r

2211− ni set (PTyped l r) = ni (ni set l) r

2228+ ni 0 set (PTyped l r) = ni 0 (ni 0 set l) r

2212− ni set (PPair _ _ _ l r) = ni (ni set l) r

2229+ ni 0 set (PPair _ _ _ l r) = ni 0 (ni 0 set l) r

2213− ni set (PDPair _ _ _ (PRef _ _ n) t r) = ni (ni set t) r

2230+ ni 0 set (PDPair _ _ _ (PRef _ _ n) t r) = ni 0 (ni 0 set t) r

2214− ni set (PDPair _ _ _ l t r) = ni (ni (ni set l) t) r

2231+ ni 0 set (PDPair _ _ _ l t r) = ni 0 (ni 0 (ni 0 set l) t) r

2215− ni set (PAlternative ns a as) = niTms set as

2232+ ni 0 set (PAlternative ns a as) = niTms 0 set as

2216− ni set (PHidden tm) = ni set tm

2233+ ni 0 set (PHidden tm) = ni 0 set tm

2217− ni set (PUnifyLog tm) = ni set tm

2234+ ni 0 set (PUnifyLog tm) = ni 0 set tm

2218− ni set (PDisamb _ tm) = ni set tm

2235+ ni 0 set (PDisamb _ tm) = ni 0 set tm

2219− ni set (PNoImplicits tm) = ni set tm

2236+ ni 0 set (PNoImplicits tm) = ni 0 set tm

2220− ni set _ = set

2237+

2221−

2238+ ni i set (PQuasiquote tm ty) = ni (i + 1) set tm `S.union` maybe S.empty (ni i set) ty

2239+ ni i set (PUnquote tm) = ni (i - 1) set tm

2240+

2241+ ni i set tm = foldr S.union set (map (ni i set) (children tm))

2242+

2243+ niTms :: Int -> S.Set Name -> [PTerm] -> S.Set Name

2222− niTms set [] = set

2244+ niTms i set [] = set

2223− niTms set (x : xs) = niTms (ni set x) xs

2245+ niTms i set (x : xs) = niTms i (ni i set x) xs

2224−

2246+

2225− niTacImp set (TacImp _ _ scr) = ni set scr

2247+ niTacImp i set (TacImp _ _ scr) = ni i set scr

2226− niTacImp set _ = set

2248+ niTacImp i set _ = set

2227

2249

2228-- Return names which are valid implicits in the given term (type).

2250-- Return names which are valid implicits in the given term (type).

2229implicitNamesIn :: [Name] -> IState -> PTerm -> [Name]

2251implicitNamesIn :: [Name] -> IState -> PTerm -> [Name]

2230−implicitNamesIn uvars ist tm = nub $ ni [] tm

2252+implicitNamesIn uvars ist tm = nub $ ni 0 [] tm

2231 where

2253 where

2232− ni env (PRef _ _ n)

2254+ ni 0 env (PRef _ _ n)

2233 | not (n `elem` env)

2255 | not (n `elem` env)

2234 = case lookupTy n (tt_ctxt ist) of

2256 = case lookupTy n (tt_ctxt ist) of

2235 [] -> [n]

2257 [] -> [n]

2236 _ -> if n `elem` uvars then [n] else []

2258 _ -> if n `elem` uvars then [n] else []

2237− ni env (PApp _ f@(PRef _ _ n) as)

2259+ ni 0 env (PApp _ f@(PRef _ _ n) as)

2238− | n `elem` uvars = ni env f ++ concatMap (ni env) (map getTm as)

2260+ | n `elem` uvars = ni 0 env f ++ concatMap (ni 0 env) (map getTm as)

2239− | otherwise = concatMap (ni env) (map getTm as)

2261+ | otherwise = concatMap (ni 0 env) (map getTm as)

2240− ni env (PApp _ f as) = ni env f ++ concatMap (ni env) (map getTm as)

2262+ ni 0 env (PApp _ f as) = ni 0 env f ++ concatMap (ni 0 env) (map getTm as)

2241− ni env (PAppBind _ f as) = ni env f ++ concatMap (ni env) (map getTm as)

2263+ ni 0 env (PAppBind _ f as) = ni 0 env f ++ concatMap (ni 0 env) (map getTm as)

2242− ni env (PCase _ c os) = ni env c ++

2264+ ni 0 env (PCase _ c os) = ni 0 env c ++

2243 -- names in 'os', not counting the names bound in the cases

2265 -- names in 'os', not counting the names bound in the cases

2244− (nub (concatMap (ni env) (map snd os))

2266+ (nub (concatMap (ni 0 env) (map snd os))

2245− \\ nub (concatMap (ni env) (map fst os)))

2267+ \\ nub (concatMap (ni 0 env) (map fst os)))

2246− ni env (PIfThenElse _ c t f) = concatMap (ni env) [c, t, f]

2268+ ni 0 env (PIfThenElse _ c t f) = concatMap (ni 0 env) [c, t, f]

2247− ni env (PLam fc n _ ty sc) = ni env ty ++ ni (n:env) sc

2269+ ni 0 env (PLam fc n _ ty sc) = ni 0 env ty ++ ni 0 (n:env) sc

2248− ni env (PPi p n _ ty sc) = ni env ty ++ ni (n:env) sc

2270+ ni 0 env (PPi p n _ ty sc) = ni 0 env ty ++ ni 0 (n:env) sc

2249− ni env (PRewrite _ l r _) = ni env l ++ ni env r

2271+ ni 0 env (PRewrite _ l r _) = ni 0 env l ++ ni 0 env r

2250− ni env (PTyped l r) = ni env l ++ ni env r

2272+ ni 0 env (PTyped l r) = ni 0 env l ++ ni 0 env r

2251− ni env (PPair _ _ _ l r) = ni env l ++ ni env r

2273+ ni 0 env (PPair _ _ _ l r) = ni 0 env l ++ ni 0 env r

2252− ni env (PDPair _ _ _ (PRef _ _ n) t r) = ni env t ++ ni (n:env) r

2274+ ni 0 env (PDPair _ _ _ (PRef _ _ n) t r) = ni 0 env t ++ ni 0 (n:env) r

2253− ni env (PDPair _ _ _ l t r) = ni env l ++ ni env t ++ ni env r

2275+ ni 0 env (PDPair _ _ _ l t r) = ni 0 env l ++ ni 0 env t ++ ni 0 env r

2254− ni env (PAlternative ns a as) = concatMap (ni env) as

2276+ ni 0 env (PAlternative ns a as) = concatMap (ni 0 env) as

2255− ni env (PHidden tm) = ni env tm

2277+ ni 0 env (PHidden tm) = ni 0 env tm

2256− ni env (PUnifyLog tm) = ni env tm

2278+ ni 0 env (PUnifyLog tm) = ni 0 env tm

2257− ni env (PDisamb _ tm) = ni env tm

2279+ ni 0 env (PDisamb _ tm) = ni 0 env tm

2258− ni env (PNoImplicits tm) = ni env tm

2280+ ni 0 env (PNoImplicits tm) = ni 0 env tm

2259− ni env _ = []

2281+

2282+ ni i env (PQuasiquote tm ty) = ni (i + 1) env tm ++

2283+ maybe [] (ni i env) ty

2284+ ni i env (PUnquote tm) = ni (i - 1) env tm

2285+

2286+ ni i env tm = concatMap (ni i env) (children tm)

2260

2287

2261-- Return names which are free in the given term.

2288-- Return names which are free in the given term.

2262namesIn :: [(Name, PTerm)] -> IState -> PTerm -> [Name]

2289namesIn :: [(Name, PTerm)] -> IState -> PTerm -> [Name]

2263−namesIn uvars ist tm = nub $ ni [] tm

2290+namesIn uvars ist tm = nub $ ni 0 [] tm

2264 where

2291 where

2265− ni env (PRef _ _ n)

2292+ ni 0 env (PRef _ _ n)

2266 | not (n `elem` env)

2293 | not (n `elem` env)

2267 = case lookupTy n (tt_ctxt ist) of

2294 = case lookupTy n (tt_ctxt ist) of

2268 [] -> [n]

2295 [] -> [n]

2269 _ -> if n `elem` (map fst uvars) then [n] else []

2296 _ -> if n `elem` (map fst uvars) then [n] else []

2270− ni env (PApp _ f as) = ni env f ++ concatMap (ni env) (map getTm as)

2297+ ni 0 env (PApp _ f as) = ni 0 env f ++ concatMap (ni 0 env) (map getTm as)

2271− ni env (PAppBind _ f as) = ni env f ++ concatMap (ni env) (map getTm as)

2298+ ni 0 env (PAppBind _ f as) = ni 0 env f ++ concatMap (ni 0 env) (map getTm as)

2272− ni env (PCase _ c os) = ni env c ++

2299+ ni 0 env (PCase _ c os) = ni 0 env c ++

2273 -- names in 'os', not counting the names bound in the cases

2300 -- names in 'os', not counting the names bound in the cases

2274− (nub (concatMap (ni env) (map snd os))

2301+ (nub (concatMap (ni 0 env) (map snd os))

2275− \\ nub (concatMap (ni env) (map fst os)))

2302+ \\ nub (concatMap (ni 0 env) (map fst os)))

2276− ni env (PIfThenElse _ c t f) = concatMap (ni env) [c, t, f]

2303+ ni 0 env (PIfThenElse _ c t f) = concatMap (ni 0 env) [c, t, f]

2277− ni env (PLam fc n nfc ty sc) = ni env ty ++ ni (n:env) sc

2304+ ni 0 env (PLam fc n nfc ty sc) = ni 0 env ty ++ ni 0 (n:env) sc

2278− ni env (PPi p n _ ty sc) = niTacImp env p ++ ni env ty ++ ni (n:env) sc

2305+ ni 0 env (PPi p n _ ty sc) = niTacImp 0 env p ++ ni 0 env ty ++ ni 0 (n:env) sc

2279− ni env (PRewrite _ l r _) = ni env l ++ ni env r

2306+ ni 0 env (PRewrite _ l r _) = ni 0 env l ++ ni 0 env r

2280− ni env (PTyped l r) = ni env l ++ ni env r

2307+ ni 0 env (PTyped l r) = ni 0 env l ++ ni 0 env r

2281− ni env (PPair _ _ _ l r) = ni env l ++ ni env r

2308+ ni 0 env (PPair _ _ _ l r) = ni 0 env l ++ ni 0 env r

2282− ni env (PDPair _ _ _ (PRef _ _ n) t r) = ni env t ++ ni (n:env) r

2309+ ni 0 env (PDPair _ _ _ (PRef _ _ n) t r) = ni 0 env t ++ ni 0 (n:env) r

2283− ni env (PDPair _ _ _ l t r) = ni env l ++ ni env t ++ ni env r

2310+ ni 0 env (PDPair _ _ _ l t r) = ni 0 env l ++ ni 0 env t ++ ni 0 env r

2284− ni env (PAlternative ns a as) = concatMap (ni env) as

2311+ ni 0 env (PAlternative ns a as) = concatMap (ni 0 env) as

2285− ni env (PHidden tm) = ni env tm

2312+ ni 0 env (PHidden tm) = ni 0 env tm

2286− ni env (PUnifyLog tm) = ni env tm

2313+ ni 0 env (PUnifyLog tm) = ni 0 env tm

2287− ni env (PDisamb _ tm) = ni env tm

2314+ ni 0 env (PDisamb _ tm) = ni 0 env tm

2288− ni env (PNoImplicits tm) = ni env tm

2315+ ni 0 env (PNoImplicits tm) = ni 0 env tm

2289− ni env _ = []

2316+

2290−

2317+ ni i env (PQuasiquote tm ty) = ni (i + 1) env tm ++ maybe [] (ni i env) ty

2318+ ni i env (PUnquote tm) = ni (i - 1) env tm

2319+

2320+ ni i env tm = concatMap (ni i env) (children tm)

2321+

2291− niTacImp env (TacImp _ _ scr) = ni env scr

2322+ niTacImp i env (TacImp _ _ scr) = ni i env scr

2292− niTacImp _ _ = []

2323+ niTacImp _ _ _ = []

2293

2324

2294-- Return which of the given names are used in the given term.

2325-- Return which of the given names are used in the given term.

2295

2326

2296usedNamesIn :: [Name] -> IState -> PTerm -> [Name]

2327usedNamesIn :: [Name] -> IState -> PTerm -> [Name]

2297−usedNamesIn vars ist tm = nub $ ni [] tm

2328+usedNamesIn vars ist tm = nub $ ni 0 [] tm

2298 where -- TODO THINK added niTacImp, but is it right?

2329 where -- TODO THINK added niTacImp, but is it right?

2299− ni env (PRef _ _ n)

2330+ ni 0 env (PRef _ _ n)

2300 | n `elem` vars && not (n `elem` env)

2331 | n `elem` vars && not (n `elem` env)

2301 = case lookupDefExact n (tt_ctxt ist) of

2332 = case lookupDefExact n (tt_ctxt ist) of

2302 Nothing -> [n]

2333 Nothing -> [n]

2303 _ -> []

2334 _ -> []

2304− ni env (PApp _ f as) = ni env f ++ concatMap (ni env) (map getTm as)

2335+ ni 0 env (PApp _ f as) = ni 0 env f ++ concatMap (ni 0 env) (map getTm as)

2305− ni env (PAppBind _ f as) = ni env f ++ concatMap (ni env) (map getTm as)

2336+ ni 0 env (PAppBind _ f as) = ni 0 env f ++ concatMap (ni 0 env) (map getTm as)

2306− ni env (PCase _ c os) = ni env c ++ concatMap (ni env) (map snd os)

2337+ ni 0 env (PCase _ c os) = ni 0 env c ++ concatMap (ni 0 env) (map snd os)

2307− ni env (PIfThenElse _ c t f) = concatMap (ni env) [c, t, f]

2338+ ni 0 env (PIfThenElse _ c t f) = concatMap (ni 0 env) [c, t, f]

2308− ni env (PLam fc n _ ty sc) = ni env ty ++ ni (n:env) sc

2339+ ni 0 env (PLam fc n _ ty sc) = ni 0 env ty ++ ni 0 (n:env) sc

2309− ni env (PPi p n _ ty sc) = niTacImp env p ++ ni env ty ++ ni (n:env) sc

2340+ ni 0 env (PPi p n _ ty sc) = niTacImp 0 env p ++ ni 0 env ty ++ ni 0 (n:env) sc

2310− ni env (PRewrite _ l r _) = ni env l ++ ni env r

2341+ ni 0 env (PRewrite _ l r _) = ni 0 env l ++ ni 0 env r

2311− ni env (PTyped l r) = ni env l ++ ni env r

2342+ ni 0 env (PTyped l r) = ni 0 env l ++ ni 0 env r

2312− ni env (PPair _ _ _ l r) = ni env l ++ ni env r

2343+ ni 0 env (PPair _ _ _ l r) = ni 0 env l ++ ni 0 env r

2313− ni env (PDPair _ _ _ (PRef _ _ n) t r) = ni env t ++ ni (n:env) r

2344+ ni 0 env (PDPair _ _ _ (PRef _ _ n) t r) = ni 0 env t ++ ni 0 (n:env) r

2314− ni env (PDPair _ _ _ l t r) = ni env l ++ ni env t ++ ni env r

2345+ ni 0 env (PDPair _ _ _ l t r) = ni 0 env l ++ ni 0 env t ++ ni 0 env r

2315− ni env (PAlternative ns a as) = concatMap (ni env) as

2346+ ni 0 env (PAlternative ns a as) = concatMap (ni 0 env) as

2316− ni env (PHidden tm) = ni env tm

2347+ ni 0 env (PHidden tm) = ni 0 env tm

2317− ni env (PUnifyLog tm) = ni env tm

2348+ ni 0 env (PUnifyLog tm) = ni 0 env tm

2318− ni env (PDisamb _ tm) = ni env tm

2349+ ni 0 env (PDisamb _ tm) = ni 0 env tm

2319− ni env (PNoImplicits tm) = ni env tm

2350+ ni 0 env (PNoImplicits tm) = ni 0 env tm

2320− ni env _ = []

2351+

2321−

2352+ ni i env (PQuasiquote tm ty) = ni (i + 1) env tm ++ maybe [] (ni i env) ty

2353+ ni i env (PUnquote tm) = ni (i - 1) env tm

2354+

2355+ ni i env tm = concatMap (ni i env) (children tm)

2356+

2322− niTacImp env (TacImp _ _ scr) = ni env scr

2357+ niTacImp i env (TacImp _ _ scr) = ni i env scr

2323− niTacImp _ _ = []

2358+ niTacImp _ _ _ = []

2324

2359

2325-- Return the list of inaccessible (= dotted) positions for a name.

2360-- Return the list of inaccessible (= dotted) positions for a name.

2326getErasureInfo :: IState -> Name -> [Int]

2361getErasureInfo :: IState -> Name -> [Int]

src/Idris/Completion.hs+1

@@ -87,6 +87,7 @@ completeOption = completeWord Nothing " \t" completeOpt

87 , "originalerrors"

88 , "autosolve"

89 , "nobanner"

90+ , "desugarnats"

90 ]

91 ]

92completeConsoleWidth :: CompletionFunc Idris

93completeConsoleWidth :: CompletionFunc Idris

src/Idris/DeepSeq.hs+5−1

@@ -84,6 +84,7 @@ instance NFData PrimFn where

84 rnf (LStrCons) = ()

85 rnf (LStrIndex) = ()

86 rnf (LStrRev) = ()

87+ rnf (LStrSubstr) = ()

87 rnf (LReadStr) = ()

88 rnf (LReadStr) = ()

88 rnf (LWriteStr) = ()

89 rnf (LWriteStr) = ()

89 rnf (LSystemInfo) = ()

90 rnf (LSystemInfo) = ()

@@ -124,6 +125,7 @@ instance NFData Opt where

124 rnf (WarnPartial) = ()

125 rnf (WarnPartial) = ()

125 rnf (WarnReach) = ()

126 rnf (WarnReach) = ()

126 rnf (EvalTypes) = ()

127 rnf (EvalTypes) = ()

128+ rnf (DesugarNats) = ()

127 rnf (NoCoverage) = ()

129 rnf (NoCoverage) = ()

128 rnf (ErrContext) = ()

130 rnf (ErrContext) = ()

129 rnf (ShowImpl) = ()

131 rnf (ShowImpl) = ()

@@ -193,7 +195,8 @@ instance NFData IOption where

193 opt_autoImport

195 opt_autoImport

194 opt_optimise

196 opt_optimise

195 opt_printdepth

197 opt_printdepth

196− opt_evaltypes) =

198+ opt_evaltypes

199+ opt_desugarnats) =

197 rnf opt_logLevel

200 rnf opt_logLevel

198 `seq` rnf opt_typecase

201 `seq` rnf opt_typecase

199 `seq` rnf opt_typeintype

202 `seq` rnf opt_typeintype

@@ -217,6 +220,7 @@ instance NFData IOption where

217 `seq` rnf opt_optimise

220 `seq` rnf opt_optimise

218 `seq` rnf opt_printdepth

221 `seq` rnf opt_printdepth

219 `seq` rnf opt_evaltypes

222 `seq` rnf opt_evaltypes

223+ `seq` rnf opt_desugarnats

220 `seq` ()

224 `seq` ()

221

225

222instance NFData LanguageExt where

226instance NFData LanguageExt where

src/Idris/Delaborate.hs+5−1

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

1{-# LANGUAGE PatternGuards #-}

2{-# OPTIONS_GHC -fwarn-incomplete-patterns #-}

3−module Idris.Delaborate (annName, bugaddr, delab, delab', delabMV, delabSugared, delabTy, delabTy', fancifyAnnots, pprintDelab, pprintDelabTy, pprintErr, resugar) where

3+module Idris.Delaborate (annName, bugaddr, delab, delab', delabMV, delabSugared, delabTy, delabTy', fancifyAnnots, pprintDelab, pprintNoDelab, pprintDelabTy, pprintErr, resugar) where

5-- Convert core TT back into high level syntax, primarily for display

6-- purposes.

@@ -226,6 +226,10 @@ pprintDelab :: IState -> Term -> Doc OutputAnnotation

226pprintDelab ist tm = annotate (AnnTerm [] tm)

227 (prettyIst ist (delabSugared ist tm))

228

229+pprintNoDelab :: IState -> Term -> Doc OutputAnnotation

230+pprintNoDelab ist tm = annotate (AnnTerm [] tm)

231+ (prettyIst ist (delab ist tm))

232+

229-- | Pretty-print the type of some name

233-- | Pretty-print the type of some name

230pprintDelabTy :: IState -> Name -> Doc OutputAnnotation

234pprintDelabTy :: IState -> Name -> Doc OutputAnnotation

231pprintDelabTy i n

235pprintDelabTy i n

src/Idris/Elab/Clause.hs+13−3

@@ -162,7 +162,7 @@ elabClauses info' fc opts n_in cs =

162 simpleCase tcase (UnmatchedCase "Error") reflect CompileTime fc inacc atys pdef erInfo

163 cov <- coverage

164 pmissing <-

165− if cov && not (hasDefault cs)

165+ if cov && not (hasDefault pats_raw)

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

167 -- missing <- genMissing n scargs sc

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

@@ -291,10 +291,20 @@ elabClauses info' fc opts n_in cs =

291 depat acc (Bind n (PVar t) sc) = depat (n : acc) (instantiate (P Bound n t) sc)

292 depat acc x = (acc, x)

293

294+

295+ getPVs (Bind x (PVar _) tm) = let (vs, tm') = getPVs tm

296+ in (x:vs, tm')

297+ getPVs tm = ([], tm)

298+

299+ isPatVar vs (P Bound n _) = n `elem` vs

300+ isPatVar _ _ = False

301+

294− hasDefault cs | (PClause _ _ last _ _ _ :_) <- reverse cs

302+ hasDefault cs | (Right (lhs, rhs) : _) <- reverse cs

295− , (PApp fn s args) <- last = all ((==Placeholder) . getTm) args

303+ , (pvs, tm) <- getPVs (explicitNames lhs)

304+ , (f, args) <- unApply tm = all (isPatVar pvs) args

296 hasDefault _ = False

305 hasDefault _ = False

297

306

307+

298 getLHS (_, l, _) = l

308 getLHS (_, l, _) = l

299

309

300 simple_lhs ctxt (Right (x, y)) = Right (normalise ctxt [] x, y)

310 simple_lhs ctxt (Right (x, y)) = Right (normalise ctxt [] x, y)

src/Idris/Primitives.hs+8−1

@@ -15,6 +15,8 @@ import Data.Char

15import Data.Function (on)

16import qualified Data.Vector.Unboxed as V

18+import Debug.Trace

19+

18data Prim = Prim { p_name :: Name,

20data Prim = Prim { p_name :: Name,

19 p_type :: Type,

21 p_type :: Type,

20 p_arity :: Int,

22 p_arity :: Int,

@@ -165,6 +167,8 @@ primitives =

165 (2, LStrIndex) partial,

167 (2, LStrIndex) partial,

166 Prim (sUN "prim__strRev") (ty [StrType] StrType) 1 (p_strRev)

168 Prim (sUN "prim__strRev") (ty [StrType] StrType) 1 (p_strRev)

167 (1, LStrRev) total,

169 (1, LStrRev) total,

170+ Prim (sUN "prim__strSubstr") (ty [AType (ATInt ITNative), AType (ATInt ITNative), StrType] StrType) 3 (p_strSubstr)

171+ (3, LStrSubstr) total,

168

172

169 Prim (sUN "prim__readString") (ty [WorldType] StrType) 1 (p_cantreduce)

173 Prim (sUN "prim__readString") (ty [WorldType] StrType) 1 (p_cantreduce)

170 (1, LReadStr) total, -- total is okay, because we have 'WorldType'

174 (1, LReadStr) total, -- total is okay, because we have 'WorldType'

@@ -493,7 +497,7 @@ p_floatSqrt = p_fPrim sqrt

493p_floatFloor = p_fPrim (fromInteger . floor)

497p_floatFloor = p_fPrim (fromInteger . floor)

494p_floatCeil = p_fPrim (fromInteger . ceiling)

498p_floatCeil = p_fPrim (fromInteger . ceiling)

495

499

496−p_strLen, p_strHead, p_strTail, p_strIndex, p_strCons, p_strRev :: [Const] -> Maybe Const

500+p_strLen, p_strHead, p_strTail, p_strIndex, p_strCons, p_strRev, p_strSubstr :: [Const] -> Maybe Const

497p_strLen [Str xs] = Just $ I (length xs)

501p_strLen [Str xs] = Just $ I (length xs)

498p_strLen _ = Nothing

502p_strLen _ = Nothing

499p_strHead [Str (x:xs)] = Just $ Ch x

503p_strHead [Str (x:xs)] = Just $ Ch x

@@ -507,6 +511,9 @@ p_strCons [Ch x, Str xs] = Just $ Str (x:xs)

507p_strCons _ = Nothing

511p_strCons _ = Nothing

508p_strRev [Str xs] = Just $ Str (reverse xs)

512p_strRev [Str xs] = Just $ Str (reverse xs)

509p_strRev _ = Nothing

513p_strRev _ = Nothing

514+p_strSubstr [I offset, I length, Str input] = Just $ Str (take length (drop offset input))

515+p_strSubstr _ = Nothing

516+

510

517

511p_cantreduce :: a -> Maybe b

518p_cantreduce :: a -> Maybe b

512p_cantreduce _ = Nothing

519p_cantreduce _ = Nothing

src/Idris/REPL.hs+4−1

@@ -808,7 +808,7 @@ process fn (Eval t)

808 logLvl 3 $ "Raw: " ++ show (tm', ty')

809 logLvl 10 $ "Debug: " ++ showEnvDbg [] tm'

810 let tmDoc = pprintDelab ist tm'

811− tyDoc = pprintDelab ist ty'

811+ tyDoc = pprintDelab ist ty'

812 iPrintTermWithType tmDoc tyDoc

813 where perhapsForce tm | termSmallerThan 100 tm = force tm

814 | otherwise = tm

@@ -1266,6 +1266,9 @@ process fn (UnsetOpt WarnReach) = fmodifyState opts_idrisCmdline $ delete Warn

1266process fn (SetOpt EvalTypes) = setEvalTypes True

1267process fn (UnsetOpt EvalTypes) = setEvalTypes False

1268

1269+process fn (SetOpt DesugarNats) = setDesugarNats True

1270+process fn (UnsetOpt DesugarNats) = setDesugarNats False

1271+

1269process fn (SetOpt _) = iPrintError "Not a valid option"

1272process fn (SetOpt _) = iPrintError "Not a valid option"

1270process fn (UnsetOpt _) = iPrintError "Not a valid option"

1273process fn (UnsetOpt _) = iPrintError "Not a valid option"

1271process fn (SetColour ty c) = setColour ty c

1274process fn (SetColour ty c) = setColour ty c

src/Idris/REPLParser.hs+1

@@ -260,6 +260,7 @@ optArg cmd name = do

260 <|> do discard (P.symbol "nobanner") ; return NoBanner

261 <|> do discard (P.symbol "warnreach"); return WarnReach

262 <|> do discard (P.symbol "evaltypes"); return EvalTypes

263+ <|> do discard (P.symbol "desugarnats"); return DesugarNats

263

264

264proofArg :: (Bool -> Int -> Name -> Command) -> String -> P.IdrisParser (Either String Command)

265proofArg :: (Bool -> Int -> Name -> Command) -> String -> P.IdrisParser (Either String Command)

265proofArg cmd name = do

266proofArg cmd name = do

test/meta002/Tacs.idr+40

@@ -52,6 +52,45 @@ test1 = %runElab triv

52test2 : Nat

53test2 = %runElab triv

55+obvious : Elab ()

56+obvious = do g <- goalType

57+ case g of

58+ `(() : Type) =>

59+ do fill `(() : ())

60+ solve

61+ `((~a, ~b) : Type) =>

62+ do aH <- gensym "a"

63+ bH <- gensym "b"

64+ claim aH a

65+ claim bH b

66+ fill `(MkPair {A=~a} {B=~b} ~(Var aH) ~(Var bH))

67+ solve

68+ focus aH; obvious

69+ focus bH; obvious

70+ `(Either ~a ~b) =>

71+ (do h <- gensym "a"

72+ claim h a

73+ fill `(Left {a=~a} {b=~b} ~(Var h))

74+ solve

75+ focus h; obvious) <|>

76+ -- This second h didn't work at one point - this

77+ -- test makes sure the fix stays fixed. The

78+ -- uniquification of binder names didn't

79+ -- appropriately treat quotation.

80+ (do h <- gensym "a"

81+ claim h b

82+ fill `(Right {a=~a} {b=~b} ~(Var h))

83+ solve

84+ focus h; obvious)

85+

86+easy : ()

87+easy = %runElab obvious

88+

89+

90+easy2 : ((), ((), (Either () Void)))

91+easy2 = %runElab obvious

92+

93+

56namespace STLC

95namespace STLC

@@ -254,3 +293,4 @@ namespace STLC

254 -- Tacs.idr line 247 col 14:

293 -- Tacs.idr line 247 col 14:

255 -- When elaborating right hand side of testElab3:

294 -- When elaborating right hand side of testElab3:

256 -- Unifying ty and Tacs.STLC.ARR ty t would lead to infinite value

295 -- Unifying ty and Tacs.STLC.ARR ty t would lead to infinite value

296+

test/meta002/expected+1−1

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

1−Tacs.idr:251:15:

1+Tacs.idr:290:15:

2When checking right hand side of testElab3:

3Unifying ty and ARR ty t would lead to infinite value

test/primitives001/expected+22

@@ -3,3 +3,25 @@

3("abc", "123")

4([1, 2], [3, 4, 5])

5([1, 2], [3, 4, 5])

6+ello! here's the thing

7+22

8+0

9+用的依赖类

10+Idris

11+[]

12+is 是一个通用

13+8

14+is 是一个通用的依赖类型纯函数式编程语言，其类型系统与 Agda 以及 Epigram 相似。

15+48

16+Idris 是一个通用的依赖类型纯函

17+18

18+

19+0

20+is is a

21+8

22+is is a general-purpose purely functional programming language with dependent types.

23+85

24+Idris is a general

25+18

26+

27+0

test/primitives001/inputnew file+2

@@ -0,0 +1,2 @@

1+Idris 是一个通用的依赖类型纯函数式编程语言，其类型系统与 Agda 以及 Epigram 相似。

2+Idris is a general-purpose purely functional programming language with dependent types.

test/primitives001/run+3−1

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

1#!/usr/bin/env bash

2idris $@ test005.idr -o test005

3./test005

4+idris $@ substring.idr -o substring

5+./substring < input

4−rm -f test005 test005.ibc

6+rm -f test005 substring *.ibc

test/primitives001/substring.idrnew file+58

@@ -0,0 +1,58 @@

1+-- This is a test of the substring primitive, both in the Idris

2+-- evaluator and in some backend. It attempts to exercise that

3+-- negative indices are equivalent to 0, that it works for mixed

4+-- single- and multi-byte characters, and that overshooting the end

5+-- doesn't break things.

7+-- Single byte test

8+foo : String

9+foo = "Hello! here's the thing"

10+

11+-- The first sentence of the Chinese wikipedia article on Idris (to

12+-- get mixed single-and-multibyte chars)

13+firstSentence : String

14+firstSentence = "Idris 是一个通用的依赖类型纯函数式编程语言，其类型系统与 Agda 以及 Epigram 相似。"

15+

16+emptyTest : prim__strSubstr 100000 14 firstSentence = ""

17+emptyTest = Refl

18+

19+multiTest : prim__strSubstr 10 5 firstSentence = "用的依赖类"

20+multiTest = Refl

21+

22+negative : prim__strSubstr (-10) 5 firstSentence = "Idris"

23+negative = Refl

24+

25+negativeEnd : prim__strSubstr 0 (-1) firstSentence = ""

26+negativeEnd = Refl

27+

28+negativeLength : prim__strSubstr 4 (-4) firstSentence = ""

29+negativeLength = Refl

30+

31+main : IO ()

32+main = do putStrLn $ prim__strSubstr 1 1004 foo

33+ printLn $ length $ prim__strSubstr 1 1000 foo

34+ printLn $ length $ prim__strSubstr 1000 2 firstSentence

35+ putStrLn $ prim__strSubstr 10 5 firstSentence

36+ putStrLn $ prim__strSubstr (-10) 5 firstSentence

37+ putStrLn $ "[" ++ prim__strSubstr 0 (-1) firstSentence ++ "]"

38+ -- Multi-byte dynamic string

39+ input <- getLine

40+ putStrLn $ prim__strSubstr 3 8 input

41+ putStrLn $ show (length (prim__strSubstr 3 8 input))

42+ putStrLn $ prim__strSubstr 3 8000 input

43+ putStrLn $ show (length (prim__strSubstr 3 8000 input))

44+ putStrLn $ prim__strSubstr (-13) 18 input

45+ putStrLn $ show (length (prim__strSubstr (-13) 18 input))

46+ putStrLn $ prim__strSubstr 4 (-4) input

47+ putStrLn $ show (length (prim__strSubstr 4 (-4) input))

48+ -- Single-byte dynamic string

49+ input <- getLine

50+ putStrLn $ prim__strSubstr 3 8 input

51+ putStrLn $ show (length (prim__strSubstr 3 8 input))

52+ putStrLn $ prim__strSubstr 3 8000 input

53+ putStrLn $ show (length (prim__strSubstr 3 8000 input))

54+ putStrLn $ prim__strSubstr (-13) 18 input

55+ putStrLn $ show (length (prim__strSubstr (-13) 18 input))

56+ putStrLn $ prim__strSubstr 4 (-4) input

57+ putStrLn $ show (length (prim__strSubstr 4 (-4) input))

58+

test/tutorial006/expected+1−1

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

1tutorial006a.idr:5:23-25:When checking right hand side of vapp:

2−When checking argument xs to constructor Data.VectType.Vect.:::

2+When checking argument xs to constructor Data.Vect.:::

3 Type mismatch between

4 Vect (k + k) a (Type of vapp xs xs)

5 and