58fc44e · Idris-dev · git.iko.soy

.travis.yml+2

compare with master

unifiedsplit

@@ -66,6 +66,8 @@ before_install:

66 fi

67

68install:

69+ - which cabal

70+ - which ghc

69 - cabal --version

71 - cabal --version

70 - echo "$(ghc --version) [$(ghc --print-project-git-commit-id 2> /dev/null || echo '?')]"

72 - echo "$(ghc --version) [$(ghc --print-project-git-commit-id 2> /dev/null || echo '?')]"

71 - if [ -f $HOME/.cabal/packages/hackage.haskell.org/00-index.tar.gz ];

73 - if [ -f $HOME/.cabal/packages/hackage.haskell.org/00-index.tar.gz ];

CHANGELOG.md+26

@@ -1,3 +1,29 @@

1+# New in 0.99.1:

2+

3+## Language updates

4+

5+* New language extensions, in addition to the existing `TypeProviders` and

6+ `ErrorReflection`:

7+ + `ElabReflection`, which must be enabled to use `%runElab`

8+ + `UniquenessTypes`, which must be enabled to use `UniqueType`

9+ + `DSLNotation`, which must be enabled to define a `dsl` block

10+ + `FirstClassReflection`, which must be enabled to define a `%reflection`

11+ function

12+

13+## Tool Updates

14+

15++ Idris' logging output has been updated to more accurately reflect

16+ its progress through the compiler. Idris, when verbose, will report

17+ explicitly: Type Checking; Totality Checking; IBC Generation;

18+ Compiling; and Code Generation.

19+

20+

21+## Library Updates

22+

23++ Terminating programs has been improved with more appropriate

24+ functions (`exitWith`, `exitFailure`, and `exitSuccess`) and a data

25+ structure (`ExitCode`) to capture a program's return code.

26+

1# New in 0.99:

27# New in 0.99:

2

28

3## Language updates

29## Language updates

CONTRIBUTORS+1

@@ -206,6 +206,7 @@ TorosFanny

206Trevor Elliott

207uwap

208Vitaly Bragilevsky

209+Vyacheslav Shebanov

209xged

210xged

210XIE Yuheng

211XIE Yuheng

211Yacine Hmito

212Yacine Hmito

docs/conf.py+1−1

@@ -33,7 +33,7 @@ on_rtd = os.environ.get('READTHEDOCS', None) == 'True'

33# ones.

34extensions = [

35 'sphinx.ext.todo',

36− 'sphinx.ext.pngmath',

36+ 'sphinx.ext.imgmath',

37 'sphinx.ext.ifconfig',

38]

39

docs/reference/misc.rst+1−1

@@ -273,7 +273,7 @@ That is, ``{x}`` behaves like ``{x=x}``.

273

274

275Existence of an implementation

276−========================

276+==============================

277

278In order to show that an implementation of some interface is defined for some

279type, one could use the ``%implementation`` keyword:

docs/reference/packages.rst+8−1

@@ -97,7 +97,7 @@ external ``C`` libraries, the following options are available:

97 which must be present for the package to be usable.

98

99+ ``objs = <objs>``, which takes a comma separated list of additional

100− files to be installed (object files, headers), perhaps generated

100+ files to be installed (object files, headers), perhaps generated

101 by the ``Makefile``.

102

103Testing

@@ -112,6 +112,11 @@ The following option is available:

112.. IMPORTANT::

113 The modules containing the test functions must also be added to the list of modules.

114

115+Comments

116+---------

117+

118+Package files support comments using the standard Idris singleline ``--`` and multiline ``{- -}`` format.

119+

115Using Package files

120Using Package files

116===================

121===================

117

122

@@ -127,6 +132,8 @@ Given an Idris package file ``text.ipkg`` it can be used with the Idris compiler

127

132

128+ ``idris --mkdoc test.ipkg`` will build HTML documentation for your package in the folder ``test_doc`` in your project's root directory.

133+ ``idris --mkdoc test.ipkg`` will build HTML documentation for your package in the folder ``test_doc`` in your project's root directory.

129

134

135++ ``idris --installdoc test.ipkg`` will install the packages documentation into Idris' central documentation folder located at ``idris --docdir``.

136+

130+ ``idris --checkpkg test.ipkg`` will type check all modules in the package only. This differs from build that type checks **and** generates code.

137+ ``idris --checkpkg test.ipkg`` will type check all modules in the package only. This differs from build that type checks **and** generates code.

131

138

132+ ``idris --testpkg test.ipkg`` will compile and run any embedded tests you have specified in the ``tests`` parameter.

139+ ``idris --testpkg test.ipkg`` will compile and run any embedded tests you have specified in the ``tests`` parameter.

docs/tutorial/index.rst−1

@@ -24,7 +24,6 @@ This is the Idris Tutorial. It will teach you about programming in the Idris Lan

24 interfaces

25 modules

26 packages

27− testing

28 interp

27 interp

29 views

28 views

30 theorems

29 theorems

docs/tutorial/packages.rst+101−15

@@ -31,14 +31,18 @@ package file would be::

31

32

33Other examples of package files can be found in the ``libs`` directory

34−of the main Idris repository, and in `third-party libraries <https://github.com/idris-lang/Idris-dev/wiki/Libraries>`_.

34+of the main Idris repository, and in `third-party libraries

35−More details including a complete listing of available fields can be found in :ref:`ref-sect-packages`.

35+<https://github.com/idris-lang/Idris-dev/wiki/Libraries>`_.

36

37

38Using Package files

39===================

40

41−Given an Idris package file ``maths.ipkg`` it can be used with the Idris compiler as follows:

41+

42+Idris itself is aware about packages, and special commands are

43+available to help with, for example, building packages, installing

44+packages, and cleaning packages. For instance, given the ``maths``

45+package from earlier we can use Idris as follows:

42

46

43+ ``idris --build maths.ipkg`` will build all modules in the package

47+ ``idris --build maths.ipkg`` will build all modules in the package

44

48

@@ -48,20 +52,102 @@ Given an Idris package file ``maths.ipkg`` it can be used with the Idris compile

48+ ``idris --clean maths.ipkg`` will delete all intermediate code and

52+ ``idris --clean maths.ipkg`` will delete all intermediate code and

49 executable files generated when building.

53 executable files generated when building.

50

54

51−+ ``idris --mkdoc maths.ipkg`` will build HTML documentation for your

52− package in the folder ``maths_doc`` in your project's root

53− directory.

54−

55−+ ``idris --checkpkg maths.ipkg`` will type check all modules in the

56− package only. This differs from build that type checks **and**

57− generates code.

58−

59−+ ``idris --testpkg maths.ipkg`` will compile and run any embedded

60− tests you have specified in the ``tests`` parameter. More

61− information about testing is given in the next section.

62−

63Once the maths package has been installed, the command line option

55Once the maths package has been installed, the command line option

64``--package maths`` makes it accessible (abbreviated to ``-p maths``).

56``--package maths`` makes it accessible (abbreviated to ``-p maths``).

65For example::

57For example::

66

58

67 idris -p maths Main.idr

59 idris -p maths Main.idr

60+

61+

62+Testing Idris Packages

63+======================

64+

65+The integrated build system includes a simple testing framework.

66+This framework collects functions listed in the ``ipkg`` file under ``tests``.

67+All test functions must return ``IO ()``.

68+

69+

70+When you enter ``idris --testpkg yourmodule.ipkg``,

71+the build system creates a temporary file in a fresh environment on your machine

72+by listing the ``tests`` functions under a single ``main`` function.

73+It compiles this temporary file to an executable and then executes it.

74+

75+

76+The tests themselves are responsible for reporting their success or failure.

77+Test functions commonly use ``putStrLn`` to report test results.

78+The test framework does not impose any standards for reporting and consequently

79+does not aggregate test results.

80+

81+

82+For example, lets take the following list of functions that are defined in a module called ``NumOps`` for a sample package ``maths``.

83+

84+.. name: Math/NumOps.idr

85+.. code-block:: idris

86+

87+ module Maths.NumOps

88+

89+ %access export -- to make functions under test visible

90+

91+ double : Num a => a -> a

92+ double a = a + a

93+

94+ triple : Num a => a -> a

95+ triple a = a + double a

96+

97+A simple test module, with a qualified name of ``Test.NumOps`` can be declared as

98+

99+.. name: Math/TestOps.idr

100+.. code-block:: idris

101+

102+ module Test.NumOps

103+

104+ import Maths.NumOps

105+

106+ %access export -- to make the test functions visible

107+

108+ assertEq : Eq a => (given : a) -> (expected : a) -> IO ()

109+ assertEq g e = if g == e

110+ then putStrLn "Test Passed"

111+ else putStrLn "Test Failed"

112+

113+ assertNotEq : Eq a => (given : a) -> (expected : a) -> IO ()

114+ assertNotEq g e = if not (g == e)

115+ then putStrLn "Test Passed"

116+ else putStrLn "Test Failed"

117+

118+ testDouble : IO ()

119+ testDouble = assertEq (double 2) 4

120+

121+ testTriple : IO ()

122+ testTriple = assertNotEq (triple 2) 5

123+

124+

125+The functions ``assertEq`` and ``assertNotEq`` are used to run expected passing, and failing, equality tests.

126+The actual tests are ``testDouble`` and ``testTriple``, and are declared in the ``maths.ipkg`` file as follows::

127+

128+ package maths

129+

130+ modules = Maths.NumOps

131+ , Test.NumOps

132+

133+ tests = Test.NumOps.testDouble

134+ , Test.NumOps.testTriple

135+

136+

137+The testing framework can then be invoked using ``idris --testpkg maths.ipkg``::

138+

139+ > idris --testpkg maths.ipkg

140+ Type checking ./Maths/NumOps.idr

141+ Type checking ./Test/NumOps.idr

142+ Type checking /var/folders/63/np5g0d5j54x1s0z12rf41wxm0000gp/T/idristests144128232716531729.idr

143+ Test Passed

144+ Test Passed

145+

146+Note how both tests have reported success by printing ``Test Passed``

147+as we arranged for with the ``assertEq`` and ``assertNoEq`` functions.

148+

149+More information

150+================

151+

152+More details, including a complete listing of available fields, can be

153+found in the reference manual in :ref:`ref-sect-packages`.

docs/tutorial/syntax.rst+1−1

@@ -92,7 +92,7 @@ forms. For example, a ``for`` loop binds a variable on each iteration:

92

93.. code-block:: idris

94

95− syntax for {x} in [xs] ":" [body] = forLoop xs (\x => body)

95+ syntax for {x} "in" [xs] ":" [body] = forLoop xs (\x => body)

96

97 main : IO ()

98 main = do for x in [1..10]:

docs/tutorial/testing.rstdeleted−85

@@ -1,85 +0,0 @@

1−.. _tut-sect-testing:

2−

3−**********************

4−Testing Idris Packages

5−**********************

6−

7−The integrated build system includes a simple testing framework.

8−This framework collects functions listed in the ``ipkg`` file under ``tests``.

9−All test functions must return ``IO ()``.

10−

11−

12−When you enter ``idris --testpkg yourmodule.ipkg``,

13−the build system creates a temporary file in a fresh environment on your machine

14−by listing the ``tests`` functions under a single ``main`` function.

15−It compiles this temporary file to an executable and then executes it.

16−

17−

18−The tests themselves are responsible for reporting their success or failure.

19−Test functions commonly use ``putStrLn`` to report test results.

20−The test framework does not impose any standards for reporting and consequently

21−does not aggregate test results.

22−

23−

24−For example, lets take the following list of functions that are defined in a module called ``NumOps`` for a sample package ``maths``.

25−

26−.. name: Math/NumOps.idr

27−.. code-block:: idris

28−

29− module Maths.NumOps

30−

31− double : Num a => a -> a

32− double a = a + a

33−

34− triple : Num a => a -> a

35− triple a = a + double a

36−

37−A simple test module, with a qualified name of ``Test.NumOps`` can be declared as

38−

39−.. name: Math/TestOps.idr

40−.. code-block:: idris

41−

42− module Test.NumOps

43−

44− import Maths.NumOps

45−

46− assertEq : Eq a => (given : a) -> (expected : a) -> IO ()

47− assertEq g e = if g == e

48− then putStrLn "Test Passed"

49− else putStrLn "Test Failed"

50−

51− assertNotEq : Eq a => (given : a) -> (expected : a) -> IO ()

52− assertNotEq g e = if not (g == e)

53− then putStrLn "Test Passed"

54− else putStrLn "Test Failed"

55−

56− testDouble : IO ()

57− testDouble = assertEq (double 2) 4

58−

59− testTriple : IO ()

60− testTriple = assertNotEq (triple 2) 5

61−

62−

63−The functions ``assertEq`` and ``assertNotEq`` are used to run expected passing, and failing, equality tests.

64−The actual tests are ``testDouble`` and ``testTriple``, and are declared in the ``maths.ipkg`` file as follows::

65−

66− package maths

67−

68− modules = Maths.NumOps

69− , Test.NumOps

70−

71− tests = Test.NumOps.testDouble

72− , Test.NumOps.testTriple

73−

74−

75−The testing framework can then be invoked using ``idris --testpkg maths.ipkg``::

76−

77− > idris --testpkg maths.ipkg

78− Type checking ./Maths/NumOps.idr

79− Type checking ./Test/NumOps.idr

80− Type checking /var/folders/63/np5g0d5j54x1s0z12rf41wxm0000gp/T/idristests144128232716531729.idr

81− Test Passed

82− Test Passed

83−

84−Note how both tests have reported success by printing ``Test Passed``

85−as we arranged for with the ``assertEq`` and ``assertNoEq`` functions.

idris.cabal+8−1

@@ -289,7 +289,6 @@ Library

289 , vector < 0.12

290 , vector-binary-instances < 0.3

291 , zip-archive > 0.2.3.5 && < 0.4

292− , safe == 0.3.9

293 , fsnotify >= 0.2 && < 2.2

292 , fsnotify >= 0.2 && < 2.2

294 , async < 2.2

293 , async < 2.2

295

294

@@ -302,6 +301,14 @@ Library

302 else

301 else

303 build-depends: process < 1.5

302 build-depends: process < 1.5

304

303

304+ -- safe 0.3.10 is having issues with cabal 1.20 and ghc 7.6.3, the

305+ -- hvr ghc ppa doesn't provide a new enough cabal library. Temporary

306+ -- fix until hvr ghc ppa is fixed or we deprecate support for 7.6.3.

307+ if impl(ghc < 7.8.4)

308+ build-depends: safe == 0.3.9

309+ else

310+ build-depends: safe >= 0.3.9

311+

305 Extensions: MultiParamTypeClasses

312 Extensions: MultiParamTypeClasses

306 , DeriveFoldable

313 , DeriveFoldable

307 , DeriveTraversable

314 , DeriveTraversable

libs/base/Data/String/Views.idr+2

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

1module Data.String.Views

2

3+%access public export

4+

3||| View for traversing a String one character at a time

5||| View for traversing a String one character at a time

4data StrList : String -> Type where

6data StrList : String -> Type where

5 SNil : StrList ""

7 SNil : StrList ""

libs/base/Debug/Error.idr+3−6

@@ -12,9 +12,6 @@ error : {default (%runElab sourceLocation) loc : SourceLocation} ->

12 (message : String) ->

13 a

14error {loc = FileLoc filename (line, col) _} message =

15− believe_me . unsafePerformIO $

16− do let place = filename ++ " line " ++ show line ++ " column " ++ show col

15+ let place = filename ++ " line " ++ show line ++ " column " ++ show col

17− let message' = place ++ ": " ++ message

16+ message' = place ++ ": " ++ message in

18− putStrLn message'

17+ idris_crash message'

19− exit 1

20−

libs/base/System.idr+33−4

@@ -54,11 +54,41 @@ getEnvironment = getAllPairs 0 []

54 then pure $ reverse $ map splitEq acc

55 else getAllPairs (n + 1) (envPair :: acc)

56

57+||| Programs can either terminate successfully, or end in a caught

58+||| failure.

59+data ExitCode : Type where

60+ ||| Terminate successfully.

61+ ExitSuccess : ExitCode

62+ ||| Program terminated for some prescribed reason.

63+ |||

64+ ||| @errNo A non-zero numerical value indicating failure.

65+ ||| @prf Proof that the int value is non-zero.

66+ ExitFailure : (errNo : Int)

67+ -> {auto prf : So (not $ errNo == 0)}

68+ -> ExitCode

69+

57||| Quit with a particular exit code

70||| Quit with a particular exit code

58−exit : Int -> IO ()

71+exit : Int -> IO a

59−exit code = foreign FFI_C "exit" (Int -> IO ()) code

72+exit code = believe_me $ foreign FFI_C "exit" (Int -> IO ()) code

73+

74+||| Terminate the program with an `ExitCode`. This code indicates the

75+||| success of the program's execution, and returns the success code

76+||| to the program's caller.

77+|||

78+||| @code The `ExitCode` for program.

79+exitWith : (code : ExitCode) -> IO a

80+exitWith ExitSuccess = exit 0

81+exitWith (ExitFailure errNo) = exit errNo

82+

83+||| Exit the program indicating failure.

84+exitFailure : IO a

85+exitFailure = exitWith (ExitFailure 1)

60

86

87+||| Exit the program after a successful run.

88+exitSuccess : IO a

89+exitSuccess = exitWith ExitSuccess

90+

61−||| Get the numbers of seconds since 1st January 1970, 00:00 UTC

91+||| Get the numbers of seconds since 1st January 1970, 00:00 UTC

62time : IO Integer

92time : IO Integer

63time = do MkRaw t <- foreign FFI_C "idris_time" (IO (Raw Integer))

93time = do MkRaw t <- foreign FFI_C "idris_time" (IO (Raw Integer))

64 pure t

94 pure t

@@ -69,4 +99,3 @@ usleep i = foreign FFI_C "usleep" (Int -> IO ()) i

69

99

70system : String -> IO Int

100system : String -> IO Int

71system cmd = foreign FFI_C "system" (String -> IO Int) cmd

101system cmd = foreign FFI_C "system" (String -> IO Int) cmd

72−

libs/contrib/CFFI/Types.idr+3−1

@@ -126,13 +126,15 @@ offsetsPacked xs = offsets' xs [] 0

126 offsets' [] acc _ = reverse acc

127 offsets' (x::xs) acc pos = offsets' xs (pos::acc) (sizeOf x)

128

129+%language ElabReflection -- needed for 'error', which finds a line number

130+

129private

131private

130indexOrFail : Nat -> List a -> a

132indexOrFail : Nat -> List a -> a

131indexOrFail i xs = case index' i xs of

133indexOrFail i xs = case index' i xs of

132 Just x => x

134 Just x => x

133 Nothing => error "Out of bounds access"

135 Nothing => error "Out of bounds access"

134

136

135−||| The offset of a firld in a composite type

137+||| The offset of a field in a composite type

136export

138export

137offset : Composite -> Nat -> Int

139offset : Composite -> Nat -> Int

138offset (STRUCT xs) i = indexOrFail i (offsetsStruct xs)

140offset (STRUCT xs) i = indexOrFail i (offsetsStruct xs)

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

@@ -17,7 +17,7 @@ implementation Handler (Exception a) List where

17

18implementation Show a => Handler (Exception a) IO where

19 handle _ (Raise e) k = do printLn e

20− believe_me (exit 1)

20+ (exit 1)

21

22implementation Handler (Exception a) (IOExcept a) where

23 handle _ (Raise e) k = ioe_fail e

@@ -30,4 +30,3 @@ EXCEPTION t = MkEff () (Exception t)

30

31raise : a -> Eff b [EXCEPTION a]

32raise err = call $ Raise err

33−

libs/prelude/Builtins.idr+7

@@ -2,6 +2,7 @@

2

3%access public export

4%default total

5+%language UniquenessTypes

5

6

6||| The canonical single-element type, also known as the trivially

7||| The canonical single-element type, also known as the trivially

7||| true proposition.

8||| true proposition.

@@ -177,6 +178,12 @@ assert_total x = x

177assert_unreachable : a

178assert_unreachable : a

178-- compiled as primitive

179-- compiled as primitive

179

180

181+||| Abort immediately with an error message

182+idris_crash : (msg : String) -> a

183+-- compiled as primitive

184+

185+%used idris_crash msg

186+

180||| Subvert the type checker. This function is abstract, so it will not reduce in

187||| Subvert the type checker. This function is abstract, so it will not reduce in

181||| the type checker. Use it with care - it can result in segfaults or worse!

188||| the type checker. Use it with care - it can result in segfaults or worse!

182export

189export

libs/prelude/Prelude.idr+11−3

@@ -37,6 +37,8 @@ import public Language.Reflection.Errors

37%access public export

38%default total

39

40+%language ElabReflection

41+

40-- Things that can't be elsewhere for import cycle reasons

42-- Things that can't be elsewhere for import cycle reasons

41-- See comment after declaration of void in Builtins.idr

43-- See comment after declaration of void in Builtins.idr

42-- for explanation of this definition's location

44-- for explanation of this definition's location

@@ -144,9 +146,14 @@ natRange n = List.reverse (go n)

144 where go Z = []

146 where go Z = []

145 go (S n) = n :: go n

147 go (S n) = n :: go n

146

148

149+

147-- predefine Nat versions of Enum, so we can use them in the default impls

150-- predefine Nat versions of Enum, so we can use them in the default impls

151+countFrom : Num n => n -> n -> Stream n

152+countFrom start diff = start :: countFrom (start + diff) diff

153+

148total natEnumFromThen : Nat -> Nat -> Stream Nat

154total natEnumFromThen : Nat -> Nat -> Stream Nat

149−natEnumFromThen n next = n :: natEnumFromThen next (minus next n)

155+natEnumFromThen n next = countFrom n (minus next n)

156+

150total natEnumFromTo : Nat -> Nat -> List Nat

157total natEnumFromTo : Nat -> Nat -> List Nat

151natEnumFromTo n m = if n <= m

158natEnumFromTo n m = if n <= m

152 then go n m

159 then go n m

@@ -195,7 +202,7 @@ Enum Integer where

195 succ n = n + 1

202 succ n = n + 1

196 toNat n = cast n

203 toNat n = cast n

197 fromNat n = cast n

204 fromNat n = cast n

198− enumFromThen n inc = n :: enumFromThen (inc + n) inc

205+ enumFromThen n inc = countFrom n (inc - n)

199 enumFromTo n m = if n <= m

206 enumFromTo n m = if n <= m

200 then go n m

207 then go n m

201 else List.reverse $ go m n

208 else List.reverse $ go m n

@@ -224,7 +231,8 @@ Enum Int where

224 go' acc (S k) m = go' (m :: acc) k (m - 1)

231 go' acc (S k) m = go' (m :: acc) k (m - 1)

225 go : Int -> Int -> List Int

232 go : Int -> Int -> List Int

226 go n m = go' [] (cast {to = Nat} (m - n)) m

233 go n m = go' [] (cast {to = Nat} (m - n)) m

227− enumFromThen n inc = n :: enumFromThen (inc + n) inc

234+ enumFromThen n inc = countFrom n (inc - n)

235+

228 enumFromThenTo n next m = if n == m then [n]

236 enumFromThenTo n next m = if n == m then [n]

229 else if next - n == 0 || next - n < 0 /= m - n < 0 then []

237 else if next - n == 0 || next - n < 0 /= m - n < 0 then []

230 else go (natRange (S (divNatNZ (cast {to=Nat} (abs (m - n))) (S (cast {to=Nat} ((abs (next - n)) - 1))) SIsNotZ)))

238 else go (natRange (S (divNatNZ (cast {to=Nat} (abs (m - n))) (S (cast {to=Nat} ((abs (next - n)) - 1))) SIsNotZ)))

libs/prelude/Prelude/Nat.idr+13−8

@@ -91,6 +91,12 @@ hyper (S pn) a (S pb) = hyper pn a (hyper (S pn) a pb)

91-- Comparisons

92--------------------------------------------------------------------------------

93

94+||| Proofs that `n` or `m` is not equal to Z

95+data NotBothZero : (n, m : Nat) -> Type where

96+ LeftIsNotZero : NotBothZero (S n) m

97+ RightIsNotZero : NotBothZero n (S m)

98+

99+

94||| Proofs that `n` is less than or equal to `m`

100||| Proofs that `n` is less than or equal to `m`

95||| @ n the smaller number

101||| @ n the smaller number

96||| @ m the larger number

102||| @ m the larger number

@@ -386,16 +392,15 @@ log2 (S n) = log2NZ (S n) SIsNotZ

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

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

387-- GCD and LCM

393-- GCD and LCM

388--------------------------------------------------------------------------------

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

389−partial

390−gcd : Nat -> Nat -> Nat

395+gcd : (a: Nat) -> (b: Nat) -> .{auto ok: NotBothZero a b} -> Nat

391−gcd a Z = a

396+gcd a Z = a

397+gcd Z b = b

392−gcd a b = assert_total (gcd b (a `modNat` b))

398+gcd a (S b) = assert_total $ gcd (S b) (modNatNZ a (S b) SIsNotZ)

393

399

394−partial

395lcm : Nat -> Nat -> Nat

400lcm : Nat -> Nat -> Nat

396−lcm _ Z = Z

401+lcm _ Z = Z

397−lcm Z _ = Z

402+lcm Z _ = Z

398−lcm x y = divNat (x * y) (gcd x y)

403+lcm a (S b) = assert_total $ divNat (a * (S b)) (gcd a (S b))

399

404

400

405

401--------------------------------------------------------------------------------

406--------------------------------------------------------------------------------

libs/prelude/Prelude/Strings.idr+19−14

@@ -45,7 +45,8 @@ foldl1 f (x::xs) = foldl f x xs

45||| ```

46partial

47strHead : String -> Char

48+strHead "" = idris_crash "Prelude.Strings: attempt to take the head of an empty string"

48−strHead = prim__strHead

49+strHead x = prim__strHead x

49

50

50||| Returns the characters specified after the head of the string.

51||| Returns the characters specified after the head of the string.

51|||

52|||

@@ -59,7 +60,8 @@ strHead = prim__strHead

59||| ```

60||| ```

60partial

61partial

61strTail : String -> String

62strTail : String -> String

63+strTail "" = idris_crash "Prelude.Strings: attempt to take the tail of an empty string"

62−strTail = prim__strTail

64+strTail xs = prim__strTail xs

63

65

64||| Adds a character to the front of the specified string.

66||| Adds a character to the front of the specified string.

65|||

67|||

@@ -72,6 +74,18 @@ strTail = prim__strTail

72strCons : Char -> String -> String

74strCons : Char -> String -> String

73strCons = prim__strCons

75strCons = prim__strCons

74

76

77+||| Returns the length of the string.

78+|||

79+||| ```idris example

80+||| length ""

81+||| ```

82+||| ```idris example

83+||| length "ABC"

84+||| ```

85+length : String -> Nat

86+length = fromInteger . prim__zextInt_BigInt . prim_lenString

87+

88+

75||| Returns the nth character (starting from 0) of the specified string.

89||| Returns the nth character (starting from 0) of the specified string.

76|||

90|||

77||| Precondition: '0 < i < length s' for 'strIndex s i'.

91||| Precondition: '0 < i < length s' for 'strIndex s i'.

@@ -81,7 +95,9 @@ strCons = prim__strCons

81||| ```

95||| ```

82partial

96partial

83strIndex : String -> Int -> Char

97strIndex : String -> Int -> Char

98+strIndex x i = if (i < 0 || i >= cast (length x))

99+ then idris_crash "Prelude.Strings: String index out of bounds"

84−strIndex = prim__strIndex

100+ else prim__strIndex x i

85

101

86||| Reverses the elements within a String.

102||| Reverses the elements within a String.

87|||

103|||

@@ -297,17 +313,6 @@ unlines' (l::ls) = l ++ '\n' :: unlines' ls

297unlines : List String -> String

313unlines : List String -> String

298unlines = pack . unlines' . map unpack

314unlines = pack . unlines' . map unpack

299

315

300−||| Returns the length of the string.

301−|||

302−||| ```idris example

303−||| length ""

304−||| ```

305−||| ```idris example

306−||| length "ABC"

307−||| ```

308−length : String -> Nat

309−length = fromInteger . prim__zextInt_BigInt . prim_lenString

310−

311||| Returns a substring of a given string

316||| Returns a substring of a given string

312|||

317|||

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

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

rts/idris_rts.c+5

@@ -595,6 +595,11 @@ VAL idris_readStr(VM* vm, FILE* h) {

595 return ret;

596}

597

598+void idris_crash(char* msg) {

599+ fprintf(stderr, "%s\n", msg);

600+ exit(1);

601+}

602+

598VAL idris_strHead(VM* vm, VAL str) {

603VAL idris_strHead(VM* vm, VAL str) {

599 return idris_strIndex(vm, str, 0);

604 return idris_strIndex(vm, str, 0);

600}

605}

rts/idris_rts.h+3

@@ -364,6 +364,9 @@ VAL idris_pokeDouble(VAL ptr, VAL offset, VAL data);

364VAL idris_peekSingle(VM* vm, VAL ptr, VAL offset);

365VAL idris_pokeSingle(VAL ptr, VAL offset, VAL data);

366

367+// Crash with a message (used for partial primitives)

368+void idris_crash(char* msg);

369+

367// String primitives

370// String primitives

368VAL idris_concat(VM* vm, VAL l, VAL r);

371VAL idris_concat(VM* vm, VAL l, VAL r);

369VAL idris_strlt(VM* vm, VAL l, VAL r);

372VAL idris_strlt(VM* vm, VAL l, VAL r);

src/IRTS/CodegenC.hs+1

@@ -617,6 +617,7 @@ doOp v (LIntCh ITNative) args = v ++ creg (last args)

617doOp v (LIntCh ITChar) args = doOp v (LIntCh ITNative) args

618

619doOp v LSystemInfo [x] = v ++ "idris_systemInfo(vm, " ++ creg x ++ ")"

620+doOp v LCrash [x] = "idris_crash(GETSTR(" ++ creg x ++ "))"

620doOp v LNoOp args = v ++ creg (last args)

621doOp v LNoOp args = v ++ creg (last args)

621

622

622-- Pointer primitives (declared as %extern in Builtins.idr)

623-- Pointer primitives (declared as %extern in Builtins.idr)

src/IRTS/Compiler.hs+9−3

@@ -52,8 +52,9 @@ import System.Process

52

53-- | Compile to simplified forms and return CodegenInfo

54compile :: Codegen -> FilePath -> Maybe Term -> Idris CodegenInfo

55−compile codegen f mtm

55+compile codegen f mtm = do

56+ logCodeGen 1 "Compiling Output."

56− = do checkMVs -- check for undefined metavariables

57+ checkMVs -- check for undefined metavariables

57 checkTotality -- refuse to compile if there are totality problems

58 checkTotality -- refuse to compile if there are totality problems

58 exports <- findExports

59 exports <- findExports

59 let rootNames = case mtm of

60 let rootNames = case mtm of

@@ -108,7 +109,7 @@ compile codegen f mtm

108 Just f -> runIO $ writeFile f (dumpDefuns defuns)

109 Just f -> runIO $ writeFile f (dumpDefuns defuns)

109 triple <- Idris.AbsSyntax.targetTriple

110 triple <- Idris.AbsSyntax.targetTriple

110 cpu <- Idris.AbsSyntax.targetCPU

111 cpu <- Idris.AbsSyntax.targetCPU

111− logCodeGen 1 "Building output"

112+ logCodeGen 1 "Generating Code."

112 case checked of

113 case checked of

113 OK c -> do return $ CodegenInfo f outty triple cpu

114 OK c -> do return $ CodegenInfo f outty triple cpu

114 hdrs impdirs objs libs flags

115 hdrs impdirs objs libs flags

@@ -258,6 +259,11 @@ irTerm top vs env tm@(App _ f a) = do

258 | u == txt "assert_unreachable"

259 | u == txt "assert_unreachable"

259 -> return $ LError $ "ABORT: Reached an unreachable case in " ++ show top

260 -> return $ LError $ "ABORT: Reached an unreachable case in " ++ show top

260

261

262+ (P _ (UN u) _, [_, msg])

263+ | u == txt "idris_crash"

264+ -> do msg' <- irTerm top vs env msg

265+ return $ LOp LCrash [msg']

266+

261 -- TMP HACK - until we get inlining.

267 -- TMP HACK - until we get inlining.

262 (P _ (UN r) _, [_, _, _, _, _, arg])

268 (P _ (UN r) _, [_, _, _, _, _, arg])

263 | r == txt "replace"

269 | r == txt "replace"

src/IRTS/Lang.hs+2

@@ -92,6 +92,8 @@ data PrimFn = LPlus ArithTy | LMinus ArithTy | LTimes ArithTy

92 | LPar -- evaluate argument anywhere, possibly on another

93 -- core or another machine. 'id' is a valid implementation

94 | LExternal Name

95+ | LCrash

96+

95 | LNoOp

97 | LNoOp

96 deriving (Show, Eq, Generic)

98 deriving (Show, Eq, Generic)

97

99

src/IRTS/System.hs+6−1

@@ -6,7 +6,7 @@ License : BSD3

6Maintainer : The Idris Community.

7-}

8{-# LANGUAGE CPP #-}

9−module IRTS.System( getDataFileName

9+module IRTS.System( getIdrisDataFileByName

10 , getCC

11 , getLibFlags

12 , getIdrisDataDir

@@ -42,6 +42,11 @@ getIdrisDataDir = do

42 return ddir

43 Just ddir -> return ddir

44

45+getIdrisDataFileByName :: String -> IO FilePath

46+getIdrisDataFileByName fn = do

47+ dir <- getIdrisDataDir

48+ return $ dir </> fn

49+

45overrideIdrisSubDirWith :: String -- ^ Sub directory in `getDataDir` location.

50overrideIdrisSubDirWith :: String -- ^ Sub directory in `getDataDir` location.

46 -> String -- ^ Environment variable to get new location from.

51 -> String -- ^ Environment variable to get new location from.

47 -> IO FilePath

52 -> IO FilePath

src/Idris/AbsSyntax.hs+4−8

@@ -142,14 +142,10 @@ addImported pub f

142 putIState $ i { idris_imported = nub $ (f, pub) : idris_imported i }

143

144addLangExt :: LanguageExt -> Idris ()

145−addLangExt TypeProviders = do i <- getIState

146− putIState $ i {

147− idris_language_extensions = TypeProviders : idris_language_extensions i

148− }

149−addLangExt ErrorReflection = do i <- getIState

145+addLangExt e = do i <- getIState

150− putIState $ i {

146+ putIState $ i {

151− idris_language_extensions = ErrorReflection : idris_language_extensions i

147+ idris_language_extensions = e : idris_language_extensions i

152− }

148+ }

153

149

154-- | Transforms are organised by the function being applied on the lhs

150-- | Transforms are organised by the function being applied on the lhs

155-- of the transform, to make looking up appropriate transforms quicker

151-- of the transform, to make looking up appropriate transforms quicker

src/Idris/AbsSyntaxTree.hs+6−2

@@ -120,7 +120,7 @@ defaultOpts = IOption { opt_logLevel = 0

120 , opt_showimp = False

121 , opt_errContext = False

122 , opt_repl = True

123− , opt_verbose = True

123+ , opt_verbose = False

124 , opt_nobanner = False

125 , opt_quiet = False

126 , opt_codegen = Via IBCFormat "c"

@@ -184,7 +184,8 @@ ppOption opt = PPOption {

184ppOptionIst :: IState -> PPOption

185ppOptionIst = ppOption . idris_options

186

187−data LanguageExt = TypeProviders | ErrorReflection

187+data LanguageExt = TypeProviders | ErrorReflection | UniquenessTypes

188+ | DSLNotation | ElabReflection | FCReflection

188 deriving (Show, Eq, Read, Ord, Generic)

189 deriving (Show, Eq, Read, Ord, Generic)

189

190

190-- | The output mode in use

191-- | The output mode in use

@@ -335,6 +336,7 @@ primDefs = [ sUN "unsafePerformPrimIO"

335 , sUN "mkForeignPrim"

336 , sUN "mkForeignPrim"

336 , sUN "void"

337 , sUN "void"

337 , sUN "assert_unreachable"

338 , sUN "assert_unreachable"

339+ , sUN "idris_crash"

338 ]

340 ]

339

341

340-- information that needs writing for the current module's .ibc file

342-- information that needs writing for the current module's .ibc file

@@ -2470,6 +2472,8 @@ implicitNamesIn uvars ist tm

2470 ni 0 env (PIfThenElse _ c t f) = mapM_ (ni 0 env) [c, t, f]

2472 ni 0 env (PIfThenElse _ c t f) = mapM_ (ni 0 env) [c, t, f]

2471 ni 0 env (PLam fc n _ ty sc) = do ni 0 env ty; ni 0 (n:env) sc

2473 ni 0 env (PLam fc n _ ty sc) = do ni 0 env ty; ni 0 (n:env) sc

2472 ni 0 env (PPi p n _ ty sc) = do ni 0 env ty; ni 0 (n:env) sc

2474 ni 0 env (PPi p n _ ty sc) = do ni 0 env ty; ni 0 (n:env) sc

2475+ ni 0 env (PLet fc n _ ty val sc) = do ni 0 env ty;

2476+ ni 0 env val; ni 0 (n:env) sc

2473 ni 0 env (PRewrite _ _ l r _) = do ni 0 env l; ni 0 env r

2477 ni 0 env (PRewrite _ _ l r _) = do ni 0 env l; ni 0 env r

2474 ni 0 env (PTyped l r) = do ni 0 env l; ni 0 env r

2478 ni 0 env (PTyped l r) = do ni 0 env l; ni 0 env r

2475 ni 0 env (PPair _ _ _ l r) = do ni 0 env l; ni 0 env r

2479 ni 0 env (PPair _ _ _ l r) = do ni 0 env l; ni 0 env r

src/Idris/Core/Elaborate.hs+6−7

@@ -463,18 +463,17 @@ equiv :: Raw -> Elab' aux ()

463equiv tm = processTactic' (Equiv tm)

464

465-- | Turn the current hole into a pattern variable with the provided

466−-- name, made unique if MN

466+-- name, made unique if not the same as the head of the hole queue

467patvar :: Name -> Elab' aux ()

468patvar n@(SN _) = do apply (Var n) []; solve

469patvar n = do env <- get_env

470 hs <- get_holes

471 if (n `elem` map fst env) then do apply (Var n) []; solve

472− else do n' <- case n of

472+ else do n' <- case hs of

473− UN _ -> return $! n

473+ (h : hs) -> if n == h then return n

474− MN _ _ -> unique_hole n

474+ else unique_hole n

475− NS _ _ -> return $! n

475+ _ -> unique_hole n

476− x -> return $! n

477− processTactic' (PatVar n')

476+ processTactic' (PatVar n)

478

477

479-- | Turn the current hole into a pattern variable with the provided

478-- | Turn the current hole into a pattern variable with the provided

480-- name, but don't make MNs unique.

479-- name, but don't make MNs unique.

src/Idris/Core/Evaluate.hs+18−6

@@ -72,6 +72,16 @@ data Value = VP NameType Name Value

72-- | VLazy Env [Value] Term

73 | VTmp Int

74

75+canonical :: Value -> Bool

76+canonical (VP (DCon _ _ _) _ _) = True

77+canonical (VApp f a) = canonical f

78+canonical (VConstant _) = True

79+canonical (VType _) = True

80+canonical (VUType _) = True

81+canonical VErased = True

82+canonical _ = False

83+

84+

75instance Show Value where

85instance Show Value where

76 show x = show $ evalState (quote 100 x) initEval

86 show x = show $ evalState (quote 100 x) initEval

77

87

@@ -254,6 +264,8 @@ eval traceon ctxt ntimes genv tm opts = ev ntimes [] True [] tm where

254 atRepl = AtREPL `elem` opts

264 atRepl = AtREPL `elem` opts

255 unfold = Unfold `elem` opts

265 unfold = Unfold `elem` opts

256

266

267+ noFree = all canonical . map snd

268+

257 -- returns 'True' if the function should block

269 -- returns 'True' if the function should block

258 -- normal evaluation should return false

270 -- normal evaluation should return false

259 blockSimplify (CaseInfo inl always dict) n stk

271 blockSimplify (CaseInfo inl always dict) n stk

@@ -274,11 +286,11 @@ eval traceon ctxt ntimes genv tm opts = ev ntimes [] True [] tm where

274 ev ntimes_in stk top env (P Ref n ty)

286 ev ntimes_in stk top env (P Ref n ty)

275 = do let limit = if simpl then 100 else 10000

287 = do let limit = if simpl then 100 else 10000

276 (u, ntimes) <- usable spec unfold limit n ntimes_in

288 (u, ntimes) <- usable spec unfold limit n ntimes_in

277− let red = u && (tcReducible n ctxt || spec || atRepl

289+ let red = u && (tcReducible n ctxt || spec || (atRepl && noFree env)

278 || runtime || unfold

290 || runtime || unfold

279 || sUN "assert_total" `elem` stk)

291 || sUN "assert_total" `elem` stk)

280 if red then

292 if red then

281− do let val = lookupDefAccExact n (spec || unfold || atRepl || runtime) ctxt

293+ do let val = lookupDefAccExact n (spec || unfold || (atRepl && noFree env) || runtime) ctxt

282 case val of

294 case val of

283 Just (Function _ tm, Public) ->

295 Just (Function _ tm, Public) ->

284 ev ntimes (n:stk) True env tm

296 ev ntimes (n:stk) True env tm

@@ -347,7 +359,7 @@ eval traceon ctxt ntimes genv tm opts = ev ntimes [] True [] tm where

347 evApply ntimes' stk top env [l',t',arg'] d'

359 evApply ntimes' stk top env [l',t',arg'] d'

348 -- Treat "assert_total" specially, as long as it's defined!

360 -- Treat "assert_total" specially, as long as it's defined!

349 ev ntimes stk top env (App _ (App _ (P _ n@(UN at) _) _) arg)

361 ev ntimes stk top env (App _ (App _ (P _ n@(UN at) _) _) arg)

350− | Just (CaseOp _ _ _ _ _ _, _) <- lookupDefAccExact n (spec || atRepl || runtime) ctxt,

362+ | Just (CaseOp _ _ _ _ _ _, _) <- lookupDefAccExact n (spec || (atRepl && noFree env)|| runtime) ctxt,

351 at == txt "assert_total" && not (simpl || unfold)

363 at == txt "assert_total" && not (simpl || unfold)

352 = ev ntimes (n : stk) top env arg

364 = ev ntimes (n : stk) top env arg

353 ev ntimes stk top env (App _ f a)

365 ev ntimes stk top env (App _ f a)

@@ -376,7 +388,7 @@ eval traceon ctxt ntimes genv tm opts = ev ntimes [] True [] tm where

376 = apply ntimes stk top env f args

388 = apply ntimes stk top env f args

377

389

378 reapply ntimes stk top env f@(VP Ref n ty) args

390 reapply ntimes stk top env f@(VP Ref n ty) args

379− = let val = lookupDefAccExact n (spec || atRepl || runtime) ctxt in

391+ = let val = lookupDefAccExact n (spec || (atRepl && noFree env) || runtime) ctxt in

380 case val of

392 case val of

381 Just (CaseOp ci _ _ _ _ cd, acc) ->

393 Just (CaseOp ci _ _ _ _ cd, acc) ->

382 let (ns, tree) = getCases cd in

394 let (ns, tree) = getCases cd in

@@ -398,11 +410,11 @@ eval traceon ctxt ntimes genv tm opts = ev ntimes [] True [] tm where

398 apply ntimes_in stk top env f@(VP Ref n ty) args

410 apply ntimes_in stk top env f@(VP Ref n ty) args

399 = do let limit = if simpl then 100 else 10000

411 = do let limit = if simpl then 100 else 10000

400 (u, ntimes) <- usable spec unfold limit n ntimes_in

412 (u, ntimes) <- usable spec unfold limit n ntimes_in

401− let red = u && (tcReducible n ctxt || spec || atRepl

413+ let red = u && (tcReducible n ctxt || spec || (atRepl && noFree env)

402 || unfold || runtime

414 || unfold || runtime

403 || sUN "assert_total" `elem` stk)

415 || sUN "assert_total" `elem` stk)

404 if red then

416 if red then

405− do let val = lookupDefAccExact n (spec || unfold || atRepl || runtime) ctxt

417+ do let val = lookupDefAccExact n (spec || unfold || (atRepl && noFree env) || runtime) ctxt

406 case val of

418 case val of

407 Just (CaseOp ci _ _ _ _ cd, acc)

419 Just (CaseOp ci _ _ _ _ cd, acc)

408 | acc == Public || acc == Hidden ->

420 | acc == Public || acc == Hidden ->

src/Idris/Core/ProofState.hs+20−13

@@ -1002,6 +1002,18 @@ updateProblems ps updates probs = rec 10 updates probs

1002 (x', y', newx || newy,

1003 updateEnv ns env, updateError ns err, fc, fa)

1004

1005+orderUpdateSolved :: [(Name, Term)] -> ProofTerm -> (ProofTerm, [Name])

1006+orderUpdateSolved ns tm = update [] ns tm

1007+ where

1008+ update done [] t = (t, done)

1009+ update done ((n, P _ n' _) : ns) t | n == n' = update done ns t

1010+ update done (n : ns) t = update (fst n : done)

1011+ (map (updateMatch n) ns)

1012+ (updateSolved [n] t)

1013+

1014+ -- Update the later solutions too

1015+ updateMatch n (x, tm) = (x, updateSolvedTerm [n] tm)

1016+

1005-- attempt to solve remaining problems with match_unify

1017-- attempt to solve remaining problems with match_unify

1006matchProblems :: Bool -> ProofState -> [(Name, TT Name)] -> Fails

1018matchProblems :: Bool -> ProofState -> [(Name, TT Name)] -> Fails

1007 -> ([(Name, TT Name)], Fails)

1019 -> ([(Name, TT Name)], Fails)

@@ -1065,30 +1077,25 @@ processTactic (ComputeLet n) ps

1065 (getProofTerm (pterm ps)) }, "")

1077 (getProofTerm (pterm ps)) }, "")

1066processTactic UnifyProblems ps

1078processTactic UnifyProblems ps

1067 = do let (ns', probs') = updateProblems ps [] (map setReady (problems ps))

1079 = do let (ns', probs') = updateProblems ps [] (map setReady (problems ps))

1068− pterm' = orderUpdateSolved ns' (pterm ps)

1080+ (pterm', dropped) = orderUpdateSolved ns' (pterm ps)

1069− traceWhen (unifylog ps) ("(UnifyProblems) Dropping holes: " ++ show (map fst ns')) $

1081+ traceWhen (unifylog ps) ("(UnifyProblems) Dropping holes: " ++ show dropped) $

1070 return (ps { pterm = pterm', solved = Nothing, problems = probs',

1082 return (ps { pterm = pterm', solved = Nothing, problems = probs',

1071 previous = Just ps, plog = "",

1083 previous = Just ps, plog = "",

1072 notunified = updateNotunified ns' (notunified ps),

1084 notunified = updateNotunified ns' (notunified ps),

1073− recents = recents ps ++ map fst ns',

1085+ recents = recents ps ++ dropped,

1074 dotted = filter (notIn ns') (dotted ps),

1086 dotted = filter (notIn ns') (dotted ps),

1075− holes = holes ps \\ (map fst ns') }, plog ps)

1087+ holes = holes ps \\ dropped }, plog ps)

1076 where notIn ns (h, _) = h `notElem` map fst ns

1088 where notIn ns (h, _) = h `notElem` map fst ns

1077− orderUpdateSolved [] t = t

1078− orderUpdateSolved (n : ns) t = orderUpdateSolved ns (updateSolved [n] t)

1079processTactic (MatchProblems all) ps

1089processTactic (MatchProblems all) ps

1080 = do let (ns', probs') = matchProblems all ps [] (map setReady (problems ps))

1090 = do let (ns', probs') = matchProblems all ps [] (map setReady (problems ps))

1081 (ns'', probs'') = matchProblems all ps ns' probs'

1091 (ns'', probs'') = matchProblems all ps ns' probs'

1082− pterm' = orderUpdateSolved ns'' (resetProofTerm (pterm ps))

1092+ (pterm', dropped) = orderUpdateSolved ns'' (resetProofTerm (pterm ps))

1083− traceWhen (unifylog ps) ("(MatchProblems) Dropping holes: " ++ show ns'') $

1093+ traceWhen (unifylog ps) ("(MatchProblems) Dropping holes: " ++ show dropped) $

1084 return (ps { pterm = pterm', solved = Nothing, problems = probs'',

1094 return (ps { pterm = pterm', solved = Nothing, problems = probs'',

1085 previous = Just ps, plog = "",

1095 previous = Just ps, plog = "",

1086 notunified = updateNotunified ns'' (notunified ps),

1096 notunified = updateNotunified ns'' (notunified ps),

1087− recents = recents ps ++ map fst ns'',

1097+ recents = recents ps ++ dropped,

1088− holes = holes ps \\ (map fst ns'') }, plog ps)

1098+ holes = holes ps \\ dropped }, plog ps)

1089− where

1090− orderUpdateSolved [] t = t

1091− orderUpdateSolved (n : ns) t = orderUpdateSolved ns (updateSolved [n] t)

1092processTactic t ps

1099processTactic t ps

1093 = case holes ps of

1100 = case holes ps of

1094 [] -> case t of

1101 [] -> case t of

src/Idris/Core/ProofTerm.hs+4−4

@@ -170,10 +170,10 @@ updateSolvedTerm' xs x = updateSolved' xs x where

170 _ -> let (t', _) = updateSolved' xs t in

171 (updsubst n v t', True)

172 updateSolved' xs tm@(Bind n b t)

173− | otherwise = let (t', ut) = updateSolved' xs t

173+ = let (t', ut) = updateSolved' xs t

174− (b', ub) = updateSolvedB' xs b in

174+ (b', ub) = updateSolvedB' xs b in

175− if ut || ub then (Bind n b' t', True)

175+ if ut || ub then (Bind n b' t', True)

176− else (tm, False)

176+ else (tm, False)

177 updateSolved' xs t@(App Complete f a) = (t, False)

178 updateSolved' xs t@(App s f a)

179 = let (f', uf) = updateSolved' xs f

src/Idris/Elab/Clause.hs+8−1

@@ -75,6 +75,8 @@ elabClauses info' fc opts n_in cs =

75 -- Check n actually exists, with no definition yet

76 let tys = lookupTy n ctxt

77 let reflect = Reflection `elem` opts

78+ when (reflect && FCReflection `notElem` idris_language_extensions ist) $

79+ ierror $ At fc (Msg "You must turn on the FirstClassReflection extension to use %reflection")

78 checkUndefined n ctxt

80 checkUndefined n ctxt

79 unless (length tys > 1) $ do

81 unless (length tys > 1) $ do

80 fty <- case tys of

82 fty <- case tys of

@@ -1025,7 +1027,12 @@ elabClause info opts (_, PWith fc fname lhs_in withs wval_in pn_in withblock)

1025

1027

1026 logElab 5 ("Checked " ++ show clhs)

1028 logElab 5 ("Checked " ++ show clhs)

1027 let bargs = getPBtys (explicitNames (normalise ctxt [] lhs_tm))

1029 let bargs = getPBtys (explicitNames (normalise ctxt [] lhs_tm))

1030+ wval <- case wval_in of

1031+ Placeholder -> ierror $ At fc $

1032+ Msg "No expression for the with block to inspect.\nYou need to replace the _ with an expression."

1033+ _ -> return $

1034+ rhs_trans info $

1028− let wval = rhs_trans info $ addImplBound i (map fst bargs) wval_in

1035+ addImplBound i (map fst bargs) wval_in

1029 logElab 5 ("Checking " ++ showTmImpls wval)

1036 logElab 5 ("Checking " ++ showTmImpls wval)

1030 -- Elaborate wval in this context

1037 -- Elaborate wval in this context

1031 ((wvalElab, defer, is, ctxt', newDecls, highlights, newGName), _) <-

1038 ((wvalElab, defer, is, ctxt', newDecls, highlights, newGName), _) <-

src/Idris/Elab/Term.hs+13−5

@@ -295,7 +295,7 @@ elab ist info emode opts fn tm

295

296 -- | elabE elaborates an expression, possibly wrapping implicit coercions

297 -- and forces/delays. If you make a recursive call in elab', it is

298− -- normally correct to call elabE - the ones that don't are desugarings

298+ -- normally correct to call elabE - the ones that don't are `desugarings

299 -- typically

300 elabE :: ElabCtxt -> Maybe FC -> PTerm -> ElabD ()

301 elabE ina fc' t =

@@ -372,7 +372,10 @@ elab ist info emode opts fn tm

372 solve

373 highlightSource fc' (AnnType "Type" "The type of types")

374 elab' ina fc (PUniverse fc' u) =

375+ do unless (UniquenessTypes `elem` idris_language_extensions ist

376+ || e_qq ina) $

377+ lift $ tfail $ At fc' (Msg "You must turn on the UniquenessTypes extension to use UniqueType or AnyType")

375− do apply (RUType u) []

378+ apply (RUType u) []

376 solve

379 solve

377 highlightSource fc' (AnnType (show u) "The type of unique types")

380 highlightSource fc' (AnnType (show u) "The type of unique types")

378-- elab' (_,_,inty) (PConstant c)

381-- elab' (_,_,inty) (PConstant c)

@@ -702,14 +705,14 @@ elab ist info emode opts fn tm

702 solve

705 solve

703 highlightSource nfc (AnnBoundName n False)

706 highlightSource nfc (AnnBoundName n False)

704 elab' ina fc (PPi p n nfc Placeholder sc)

707 elab' ina fc (PPi p n nfc Placeholder sc)

705− = do attack; arg n (is_scoped p) (sMN 0 "ty")

708+ = do attack; arg n (is_scoped p) (sMN 0 "phTy")

706 addAutoBind p n

709 addAutoBind p n

707 addPSname n -- okay for proof search

710 addPSname n -- okay for proof search

708 elabE (ina { e_inarg = True, e_intype = True }) fc sc

711 elabE (ina { e_inarg = True, e_intype = True }) fc sc

709 solve

712 solve

710 highlightSource nfc (AnnBoundName n False)

713 highlightSource nfc (AnnBoundName n False)

711 elab' ina fc (PPi p n nfc ty sc)

714 elab' ina fc (PPi p n nfc ty sc)

712− = do attack; tyn <- getNameFrom (sMN 0 "ty")

715+ = do attack; tyn <- getNameFrom (sMN 0 "piTy")

713 claim tyn RType

716 claim tyn RType

714 n' <- case n of

717 n' <- case n of

715 MN _ _ -> unique_hole n

718 MN _ _ -> unique_hole n

@@ -1036,6 +1039,9 @@ elab ist info emode opts fn tm

1036 elab' ina fc (PElabError e) = lift $ tfail e

1039 elab' ina fc (PElabError e) = lift $ tfail e

1037 elab' ina mfc (PRewrite fc substfn rule sc newg)

1040 elab' ina mfc (PRewrite fc substfn rule sc newg)

1038 = elabRewrite (elab' ina mfc) ist fc substfn rule sc newg

1041 = elabRewrite (elab' ina mfc) ist fc substfn rule sc newg

1042+ -- A common error case if trying to typecheck an autogenerated case block

1043+ elab' ina _ c@(PCase fc Placeholder opts)

1044+ = lift $ tfail (Msg "No expression for the case to inspect.\nYou need to replace the _ with an expression.")

1039 elab' ina _ c@(PCase fc scr opts)

1045 elab' ina _ c@(PCase fc scr opts)

1040 = do attack

1046 = do attack

1041

1047

@@ -1278,7 +1284,9 @@ elab ist info emode opts fn tm

1278 dotterm

1284 dotterm

1279 elab' ina fc t

1285 elab' ina fc t

1280 elab' ina fc (PRunElab fc' tm ns) =

1286 elab' ina fc (PRunElab fc' tm ns) =

1287+ do unless (ElabReflection `elem` idris_language_extensions ist) $

1288+ lift $ tfail $ At fc' (Msg "You must turn on the ElabReflection extension to use %runElab")

1281− do attack

1289+ attack

1282 n <- getNameFrom (sMN 0 "tacticScript")

1290 n <- getNameFrom (sMN 0 "tacticScript")

1283 let scriptTy = RApp (Var (sNS (sUN "Elab")

1291 let scriptTy = RApp (Var (sNS (sUN "Elab")

1284 ["Elab", "Reflection", "Language"]))

1292 ["Elab", "Reflection", "Language"]))

src/Idris/ElabDecls.hs+6−1

@@ -284,6 +284,8 @@ elabDecl' what info (PRecord doc rsyn fc opts name nfc ps pdocs fs cname cdoc cs

284-}

285elabDecl' _ info (PDSL n dsl)

286 = do i <- getIState

287+ unless (DSLNotation `elem` idris_language_extensions i) $

288+ ifail "You must turn on the DSLNotation extension to use a dsl block"

287 putIState (i { idris_dsls = addDef n dsl (idris_dsls i) })

289 putIState (i { idris_dsls = addDef n dsl (idris_dsls i) })

288 addIBC (IBCDSL n)

290 addIBC (IBCDSL n)

289elabDecl' what info (PDirective i)

291elabDecl' what info (PDirective i)

@@ -296,6 +298,9 @@ elabDecl' what info (PTransform fc safety old new)

296 = do elabTransform info fc safety old new

298 = do elabTransform info fc safety old new

297 return ()

299 return ()

298elabDecl' what info (PRunElabDecl fc script ns)

300elabDecl' what info (PRunElabDecl fc script ns)

301+ = do i <- getIState

302+ unless (ElabReflection `elem` idris_language_extensions i) $

303+ ierror $ At fc (Msg "You must turn on the ElabReflection extension to use %runElab")

299− = do elabRunElab info fc script ns

304+ elabRunElab info fc script ns

300 return ()

305 return ()

301elabDecl' _ _ _ = return () -- skipped this time

306elabDecl' _ _ _ = return () -- skipped this time

src/Idris/IBC.hs+3−2

@@ -220,7 +220,8 @@ writeArchive fp i = do let a = L.foldl (\x y -> addEntryToArchive y x) emptyArch

220

221writeIBC :: FilePath -> FilePath -> Idris ()

222writeIBC src f

223+ = do

223− = do logIBC 1 $ "Writing ibc " ++ show f

224+ logIBC 1 $ "Writing IBC for: " ++ show f

224 i <- getIState

225 i <- getIState

225-- case (Data.List.map fst (idris_metavars i)) \\ primDefs of

226-- case (Data.List.map fst (idris_metavars i)) \\ primDefs of

226-- (_:_) -> ifail "Can't write ibc when there are unsolved metavariables"

227-- (_:_) -> ifail "Can't write ibc when there are unsolved metavariables"

@@ -313,7 +314,7 @@ ibc i (IBCCG n) f = case lookupCtxtExact n (idris_callgraph i) of

313 _ -> ifail "IBC write failed"

314 _ -> ifail "IBC write failed"

314ibc i (IBCCoercion n) f = return f { ibc_coercions = n : ibc_coercions f }

315ibc i (IBCCoercion n) f = return f { ibc_coercions = n : ibc_coercions f }

315ibc i (IBCAccess n a) f = return f { ibc_access = (n,a) : ibc_access f }

316ibc i (IBCAccess n a) f = return f { ibc_access = (n,a) : ibc_access f }

316−ibc i (IBCFlags n) f

317+ibc i (IBCFlags n) f

317 = case lookupCtxtExact n (idris_flags i) of

318 = case lookupCtxtExact n (idris_flags i) of

318 Just a -> return f { ibc_flags = (n,a): ibc_flags f }

319 Just a -> return f { ibc_flags = (n,a): ibc_flags f }

319 _ -> ifail "IBC write failed"

320 _ -> ifail "IBC write failed"

src/Idris/IdrisDoc.hs+2−2

@@ -19,7 +19,7 @@ import Idris.Docs

19import Idris.Docstrings (nullDocstring)

20import qualified Idris.Docstrings as Docstrings

21import Idris.Parser.Helpers (opChars)

22−import IRTS.System (getDataFileName)

22+import IRTS.System (getIdrisDataFileByName)

23

24import Control.Applicative ((<|>))

25import Control.Monad (forM_)

@@ -708,5 +708,5 @@ copyDependencies :: FilePath -- ^ The base directory to which

708 -- dependencies should be written

709 -> IO ()

710copyDependencies dir =

711− do styles <- getDataFileName $ "idrisdoc" </> "styles.css"

711+ do styles <- getIdrisDataFileByName $ "idrisdoc" </> "styles.css"

712 copyFile styles (dir </> "styles.css")

src/Idris/Info.hs+5

@@ -22,6 +22,7 @@ module Idris.Info

22 , getIdrisHistoryFile

23 , getIdrisInstalledPackages

24 , getIdrisLoggingCategories

25+ , getIdrisDataFileByName

25 ) where

26 ) where

26

27

27import Idris.AbsSyntax (loggingCatsStr)

28import Idris.AbsSyntax (loggingCatsStr)

@@ -34,6 +35,7 @@ import Version_idris (gitHash)

34import Data.Version

35import Data.Version

35import System.Directory

36import System.Directory

36import System.FilePath

37import System.FilePath

38+

37getIdrisDataDir :: IO String

39getIdrisDataDir :: IO String

38getIdrisDataDir = S.getIdrisDataDir

40getIdrisDataDir = S.getIdrisDataDir

39

41

@@ -88,3 +90,6 @@ getIdrisInstalledPackages = installedPackages

88

90

89getIdrisLoggingCategories :: IO [String]

91getIdrisLoggingCategories :: IO [String]

90getIdrisLoggingCategories = return $ words loggingCatsStr

92getIdrisLoggingCategories = return $ words loggingCatsStr

93+

94+getIdrisDataFileByName :: String -> IO FilePath

95+getIdrisDataFileByName = S.getIdrisDataFileByName

src/Idris/Package.hs+3−2

@@ -145,7 +145,7 @@ replPkg copts fp = do

145 case mergeOptions copts (idris_opts pkgdesc) of

146 Left emsg -> ifail emsg

147 Right opts -> do

148−

148+

149 putIState orig

150 dir <- runIO getCurrentDirectory

151 runIO $ setCurrentDirectory $ dir </> sourcedir pkgdesc

@@ -266,7 +266,8 @@ testPkg copts fp = do

266 exitWith (ExitFailure 1)

267 Right opts -> do

268 m_ist <- idris opts

269+ let texe = if isWindows then addExtension tmpn' ".exe" else tmpn'

269− exitCode <- rawSystem tmpn' []

270+ exitCode <- rawSystem texe []

270 return (m_ist, exitCode)

271 return (m_ist, exitCode)

271 case m_ist of

272 case m_ist of

272 Nothing -> exitWith (ExitFailure 1)

273 Nothing -> exitWith (ExitFailure 1)

src/Idris/Parser.hs+6−2

@@ -1429,6 +1429,10 @@ directive syn = do try (lchar '%' *> reserved "lib")

1429pLangExt :: IdrisParser LanguageExt

1430pLangExt = (reserved "TypeProviders" >> return TypeProviders)

1431 <|> (reserved "ErrorReflection" >> return ErrorReflection)

1432+ <|> (reserved "UniquenessTypes" >> return UniquenessTypes)

1433+ <|> (reserved "DSLNotation" >> return DSLNotation)

1434+ <|> (reserved "ElabReflection" >> return ElabReflection)

1435+ <|> (reserved "FirstClassReflection" >> return FCReflection)

1432

1436

1433{-| Parses a totality

1437{-| Parses a totality

1434

1438

@@ -1799,7 +1803,7 @@ loadSource lidr f toline

1799 setContext ctxt')

1803 setContext ctxt')

1800 (map snd (idris_totcheck i))

1804 (map snd (idris_totcheck i))

1801 -- build size change graph from simplified definitions

1805 -- build size change graph from simplified definitions

1802− logLvl 1 "Totality checking"

1806+ logLvl 1 $ "Totality checking " ++ f

1803 i <- getIState

1807 i <- getIState

1804 mapM_ buildSCG (idris_totcheck i)

1808 mapM_ buildSCG (idris_totcheck i)

1805 mapM_ checkDeclTotality (idris_totcheck i)

1809 mapM_ checkDeclTotality (idris_totcheck i)

@@ -1822,7 +1826,7 @@ loadSource lidr f toline

1822

1826

1823 logLvl 1 ("Finished " ++ f)

1827 logLvl 1 ("Finished " ++ f)

1824 ibcsd <- valIBCSubDir i

1828 ibcsd <- valIBCSubDir i

1825− logLvl 1 "Universe checking"

1829+ logLvl 1 $ "Universe checking " ++ f

1826 iucheck

1830 iucheck

1827 let ibc = ibcPathNoFallback ibcsd f

1831 let ibc = ibcPathNoFallback ibcsd f

1828 i <- getIState

1832 i <- getIState

test/TestData.hs+4−2

@@ -70,7 +70,8 @@ testFamiliesData = [

70 ( 15, ANY ),

71 ( 16, ANY ),

72 ( 17, ANY ),

73− ( 18, ANY )]),

73+ ( 18, ANY ),

74+ ( 19, ANY )]),

74 ("bignum", "Bignum",

75 ("bignum", "Bignum",

75 [ ( 1, ANY ),

76 [ ( 1, ANY ),

76 ( 2, ANY )]),

77 ( 2, ANY )]),

@@ -178,7 +179,8 @@ testFamiliesData = [

178 ( 4, ANY ),

179 ( 4, ANY ),

179 ( 5, ANY ),

180 ( 5, ANY ),

180 ( 6, ANY ),

181 ( 6, ANY ),

181− ( 7, ANY )]),

182+ ( 7, ANY ),

183+ ( 8, ANY )]),

182 ("prelude", "Prelude",

184 ("prelude", "Prelude",

183 [ ( 1, ANY )]),

185 [ ( 1, ANY )]),

184 ("primitives", "Primitive types",

186 ("primitives", "Primitive types",

test/basic019/basic019.idrnew file+10

@@ -0,0 +1,10 @@

1+printRange : (t : Type) -> (Show t, Num t, Enum t) => IO ()

2+printRange t = do printLn [(the t 1)..10]

3+ printLn [(the t 10),9..1]

4+ printLn (take 10 [(the t 1)..])

5+ printLn (take 10 [(the t 1),3..])

6+

7+main : IO ()

8+main = do printRange Nat

9+ printRange Int

10+ printRange Integer

test/basic019/expectednew file+12

@@ -0,0 +1,12 @@

1+[1, 2, 3, 4, 5, 6, 7, 8, 9, 10]

2+[10, 9, 8, 7, 6, 5, 4, 3, 2, 1]

3+[1, 2, 3, 4, 5, 6, 7, 8, 9, 10]

4+[1, 3, 5, 7, 9, 11, 13, 15, 17, 19]

5+[1, 2, 3, 4, 5, 6, 7, 8, 9, 10]

6+[10, 9, 8, 7, 6, 5, 4, 3, 2, 1]

7+[1, 2, 3, 4, 5, 6, 7, 8, 9, 10]

8+[1, 3, 5, 7, 9, 11, 13, 15, 17, 19]

9+[1, 2, 3, 4, 5, 6, 7, 8, 9, 10]

10+[10, 9, 8, 7, 6, 5, 4, 3, 2, 1]

11+[1, 2, 3, 4, 5, 6, 7, 8, 9, 10]

12+[1, 3, 5, 7, 9, 11, 13, 15, 17, 19]

test/basic019/runnew file+4

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

1+#!/usr/bin/env bash

2+${IDRIS:-idris} $@ basic019.idr -o basic019

3+./basic019

4+rm -f basic019 *.ibc

test/dsl001/expected+4−4

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

124

212

3testFac : Int

4−testFac = PE_interp_f79b3e31 [] (PE_fromInteger_d6648df 4)

4+testFac = PE_interp_e04a79ff [] (PE_fromInteger_d6648df 4)

5−PE_interp_f79b3e31 : Env G -> Int -> Int

5+PE_interp_e04a79ff : Env G -> Int -> Int

6−PE_interp_f79b3e31 (3arg) = \x =>

6+PE_interp_e04a79ff (3arg) = \x =>

7 ifThenElse (PE_==_ba2f651f x

8 (PE_fromInteger_d6648df 0))

9 (Delay (PE_fromInteger_d6648df 1))

10− (Delay (PE_*_ba2f651f (PE_interp_f79b3e31 (x ::

10+ (Delay (PE_*_ba2f651f (PE_interp_e04a79ff (x ::

11 (3arg))

12 (PE_-_ba2f651f x

13 (PE_fromInteger_d6648df 1)))

test/dsl001/input+1−1

@@ -1,2 +1,2 @@

1:printdef testFac

2−:printdef PE_interp_f79b3e31

2+:printdef PE_interp_e04a79ff

test/dsl001/test001.idr+2

@@ -3,6 +3,8 @@ module Main

3import Data.Vect

4import Data.Fin

5

6+%language DSLNotation

7+

6data Ty = TyInt | TyBool| TyFun Ty Ty

8data Ty = TyInt | TyBool| TyFun Ty Ty

7

9

8interpTy : Ty -> Type

10interpTy : Ty -> Type

test/dsl002/Resimp.idr+1

@@ -3,6 +3,7 @@ module Resimp

3import public Data.Vect

4import public Data.Fin

5

6+%language DSLNotation

6%access public export

7%access public export

7

8

8-- IO operations which read a resource

9-- IO operations which read a resource

test/dsl003/DSLPi.idr+2

@@ -3,6 +3,8 @@ module DSLPi

3import Data.Fin

4import Data.Vect

5

6+%language DSLNotation

7+

6data Ty = BOOL | INT | UNIT | ARR Ty Ty

8data Ty = BOOL | INT | UNIT | ARR Ty Ty

7

9

8arr_ : _ -> Ty -> Ty -> Ty

10arr_ : _ -> Ty -> Ty -> Ty

test/dsl004/Door0.idr+3−1

@@ -1,6 +1,8 @@

1import IOu

2

3+%language UniquenessTypes

4+

3−data Result : (a : Type) -> (a -> Type) -> Type* where

5+data Result : (a : Type) -> (a -> Type) -> AnyType where

4 Res : {k : a -> Type} -> (val : a) -> k val -> Result a k

6 Res : {k : a -> Type} -> (val : a) -> k val -> Result a k

5

7

6

8

test/dsl004/Door1.idr+2

@@ -2,6 +2,8 @@ import IOu

2

3import Data.Vect

4

5+%language UniquenessTypes

6+

5data Result : (a : AnyType) -> (a -> AnyType) -> AnyType where

7data Result : (a : AnyType) -> (a -> AnyType) -> AnyType where

6 Res : {k : a -> AnyType} -> (val : a) -> (h : k val) -> Result a k

8 Res : {k : a -> AnyType} -> (val : a) -> (h : k val) -> Result a k

7

9

test/dsl004/Door2.idr+2

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

1import IOu

2

3+%language UniquenessTypes

4+

3data DoorState = OPEN | CLOSED

5data DoorState = OPEN | CLOSED

4

6

5data DoorH : DoorState -> UniqueType where

7data DoorH : DoorState -> UniqueType where

test/dsl004/Door3.idr+2

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

1import IOu

2

3+%language UniquenessTypes

4+

3data DoorState = OPEN | CLOSED

5data DoorState = OPEN | CLOSED

4

6

5data DoorH : DoorState -> UniqueType where

7data DoorH : DoorState -> UniqueType where

test/dsl004/IOu.idr+2

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

1module IOu

2

3+%language UniquenessTypes

4+

3-------- An IO type supporting possibly unique values

5-------- An IO type supporting possibly unique values

4

6

5data IOu : AnyType -> AnyType where

7data IOu : AnyType -> AnyType where

test/interactive010/expected+2−2

@@ -4,9 +4,9 @@ a is not an implicit argument of Prelude.Interfaces./

4Usage is :doc <functionname>

5Usage is :wc <functionname>

6Usage is :printdef <functionname>

7−pat {ty504} : Type toplevel.u. pat {__interface505} : Prelude.Interfaces.Fractional {ty504}. Prelude.Interfaces./ {ty504} {__interface505}

7+pat {ty503} : Type toplevel.u. pat {__interface504} : Prelude.Interfaces.Fractional {ty503}. Prelude.Interfaces./ {ty503} {__interface504}

8

9− : pty {ty504} : Type toplevel.u. pty {__interface505} : Prelude.Interfaces.Fractional {ty504}. {ty504} -> {ty504} -> {ty504}

9+ : pty {ty503} : Type toplevel.u. pty {__interface504} : Prelude.Interfaces.Fractional {ty503}. {ty503} -> {ty503} -> {ty503}

10(input):1:1: error: expected: ":",

11 dependent type signature,

12 end of input

test/meta001/Finite.idr+2

@@ -4,6 +4,8 @@ import Data.Fin

4import Language.Reflection.Elab

5import Language.Reflection.Utils

6

7+%language ElabReflection

8+

7-- Test various features of reflected elaboration, including looking

9-- Test various features of reflected elaboration, including looking

8-- up datatypes, defining functions, and totality checking

10-- up datatypes, defining functions, and totality checking

9

11

test/meta002/AgdaStyleReflection.idr+1−1

@@ -13,7 +13,7 @@ import Language.Reflection.Utils

13import Pruviloj

14

15%default total

16−

16+%language ElabReflection

17

18

19||| Function arguments as provided at the application site

test/meta002/DataDef.idr+2

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

1module DataDef

2

3+%language ElabReflection

4+

3foo : Elab ()

5foo : Elab ()

4foo = do declareDatatype $ Declare `{{DataDef.N}} [MkFunArg `{{n}} `(Nat) Explicit NotErased] `(Type)

6foo = do declareDatatype $ Declare `{{DataDef.N}} [MkFunArg `{{n}} `(Nat) Explicit NotErased] `(Type)

5 defineDatatype $ DefineDatatype `{{DataDef.N}} [

7 defineDatatype $ DefineDatatype `{{DataDef.N}} [

test/meta002/Deriving.idr+2

@@ -1,6 +1,8 @@

1||| Test some deriving features

2module Deriving

3

4+%language ElabReflection

5+

4-- NB: test disabled due to excess memory consumption

6-- NB: test disabled due to excess memory consumption

5

7

6import Pruviloj

8import Pruviloj

test/meta002/Tacs.idr+1

@@ -16,6 +16,7 @@ import Language.Reflection.Utils

16import Pruviloj.Core

17

18%default total

19+%language ElabReflection

19

20

20-- Tactics can now query the elaborator and bind variables

21-- Tactics can now query the elaborator and bind variables

21

22

test/meta002/expected+2−2

@@ -1,7 +1,7 @@

1−DataDef.idr:72:1-9:

1+DataDef.idr:74:1-9:

2While running an elaboration script, the following error occurred:

3Prelude.Either.Either is already defined as a datatype.

4−Tacs.idr:298:15:

4+Tacs.idr:299:15:

5When checking right hand side of testElab3 with expected type

6 DPair Ty (Tm [])

7

test/meta003/BadDef.idr+2

@@ -2,6 +2,8 @@ module BadDef

2

3import Language.Reflection.Elab

4

5+%language ElabReflection

6+

5mkN : String -> TTName

7mkN : String -> TTName

6mkN n = NS (UN n) ["BadDef"]

8mkN n = NS (UN n) ["BadDef"]

7

9

test/meta003/expected+1−1

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

1−BadDef.idr:12:1-9:

1+BadDef.idr:14:1-9:

2While running an elaboration script, the following error occurred:

3Type mismatch between

4 ()

test/meta004/expected+1−1

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

1−meta004.idr:48:1-9:

1+meta004.idr:50:1-9:

2While running an elaboration script, the following error occurred:

3Not an impossible case

test/meta004/meta004.idr+2

@@ -2,6 +2,8 @@ import Data.Fin

2import Language.Reflection.Utils

3import Pruviloj.Core

4

5+%language ElabReflection

6+

5rename : TTName -> TTName -> Raw -> Raw

7rename : TTName -> TTName -> Raw -> Raw

6rename old new (RBind name b body) = RBind name (map (rename old new) b) (rename old new body)

8rename old new (RBind name b body) = RBind name (map (rename old new) b) (rename old new body)

7rename old new (RApp f arg) = RApp (rename old new f) (rename old new arg)

9rename old new (RApp f arg) = RApp (rename old new f) (rename old new arg)

test/pkg008/expectednew file+13

@@ -0,0 +1,13 @@

1+Entering directory `./src'

2+Type checking ./NumOps.idr

3+Type checking ./Test.idr

4+Leaving directory `./src'

5+Test Passed

6+Test Passed

7+Entering directory `./src'

8+Leaving directory `./src'

9+Entering directory `./src'

10+Removed: NumOps.ibc

11+Removed: Test.ibc

12+Removed: 00maths-idx.ibc

13+Leaving directory `./src'

test/pkg008/maths.ipkgnew file+9

@@ -0,0 +1,9 @@

1+package maths

2+

3+sourcedir = src

4+

5+modules = NumOps

6+ , Test

7+

8+tests = Test.testDouble

9+ , Test.testTriple

test/pkg008/runnew file+9

@@ -0,0 +1,9 @@

1+#!/usr/bin/env bash

2+

3+${IDRIS:-idris} $@ --build maths.ipkg

4+${IDRIS:-idris} $@ --testpkg maths.ipkg | grep -v -e "idris"

5+

6+# Idris only appears in the randomly generated name of test so we grep

7+# to remove it to make output consistent.

8+

9+${IDRIS:-idris} $@ --clean maths.ipkg

test/pkg008/src/NumOps.idrnew file+9

@@ -0,0 +1,9 @@

1+module NumOps

2+

3+%access export -- to make functions under test visible

4+

5+double : Num a => a -> a

6+double a = a + a

7+

8+triple : Num a => a -> a

9+triple a = a + double a

test/pkg008/src/Test.idrnew file+21

@@ -0,0 +1,21 @@

1+module Test

2+

3+import NumOps

4+

5+%access export -- to make the test functions visible

6+

7+assertEq : Eq a => (given : a) -> (expected : a) -> IO ()

8+assertEq g e = if g == e

9+ then putStrLn "Test Passed"

10+ else putStrLn "Test Failed"

11+

12+assertNotEq : Eq a => (given : a) -> (expected : a) -> IO ()

13+assertNotEq g e = if not (g == e)

14+ then putStrLn "Test Passed"

15+ else putStrLn "Test Failed"

16+

17+testDouble : IO ()

18+testDouble = assertEq (double 2) 4

19+

20+testTriple : IO ()

21+testTriple = assertNotEq (triple 2) 5

test/proof002/Reflect.idr+1

@@ -4,6 +4,7 @@ import Decidable.Equality

4

5%access public export

6%default total

7+%language FirstClassReflection

7

8

8using (xs : List a, ys : List a, G : List (List a))

9using (xs : List a, ys : List a, G : List (List a))

9

10

test/proof002/expected+3−3

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

1−Reflect.idr:174:21-26:

1+Reflect.idr:175:21-26:

2This style of tactic proof is deprecated. See %runElab for the replacement.

3−Reflect.idr:183:21-26:

3+Reflect.idr:184:21-26:

4This style of tactic proof is deprecated. See %runElab for the replacement.

5−Reflect.idr:191:15-20:

5+Reflect.idr:192:15-20:

6This style of tactic proof is deprecated. See %runElab for the replacement.

7test030a.idr:12:26-14:1:

8When checking right hand side of testReflect1 with expected type

test/pruviloj001/pruviloj001.idr+1

@@ -5,6 +5,7 @@ import Pruviloj

5import Pruviloj.Induction

6

7%default total

8+%language ElabReflection

8

9

9||| Try some simplification and rewriting heuristics, then attempt to

10||| Try some simplification and rewriting heuristics, then attempt to

10||| solve the goal

11||| solve the goal

test/sourceLocation001/SourceLoc.idr+1

@@ -6,6 +6,7 @@ import Language.Reflection

6import Language.Reflection.Utils

7

8%default total

9+%language DSLNotation

9

10

10||| A "function" that returns where it is called in the source

11||| A "function" that returns where it is called in the source

11getLoc : {default tactics { sourceLocation } x : SourceLocation} -> SourceLocation

12getLoc : {default tactics { sourceLocation } x : SourceLocation} -> SourceLocation

test/sourceLocation001/expected+8−8

@@ -1,19 +1,19 @@

1−SourceLoc.idr:11:19-26:

1+SourceLoc.idr:12:19-26:

2This style of tactic proof is deprecated. See %runElab for the replacement.

3−SourceLoc.idr:20:19-24:

3+SourceLoc.idr:21:19-24:

4This style of tactic proof is deprecated. See %runElab for the replacement.

5−SourceLoc.idr:40:20-27:

5+SourceLoc.idr:41:20-27:

6This style of tactic proof is deprecated. See %runElab for the replacement.

7−SourceLoc.idr:98:18-23:

7+SourceLoc.idr:99:18-23:

8This style of tactic proof is deprecated. See %runElab for the replacement.

9Testing using definition

10−FileLoc "SourceLoc.idr" (16, 11) (16, 17)

10+FileLoc "SourceLoc.idr" (17, 11) (17, 17)

11Testing using inline tactics

12−FileLoc "SourceLoc.idr" (20, 17) (20, 17)

12+FileLoc "SourceLoc.idr" (21, 17) (21, 17)

13Testing using metavariable with later definition

14−FileLoc "SourceLoc.idr" (98, 16) (98, 16)

14+FileLoc "SourceLoc.idr" (99, 16) (99, 16)

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

16Success!

17−Error at FileLoc "SourceLoc.idr" (72, 23) (72, 26)

17+Error at FileLoc "SourceLoc.idr" (73, 23) (73, 26)

18Success!

19Success!

test/tactics001/Tactics.idr+1−1

@@ -4,7 +4,7 @@ import Language.Reflection.Elab

4

5import Data.Vect

6

7−

7+%language ElabReflection

8%default total

9

10-- Test that basic proofs with new-style tactics work

test/unique001/unique001.idr+2

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

1module Main

2

3+%language UniquenessTypes

4+

3data UList : Type -> UniqueType where

5data UList : Type -> UniqueType where

4 Nil : UList a

6 Nil : UList a

5 (::) : a -> UList a -> UList a

7 (::) : a -> UList a -> UList a

test/unique004/expected+10−10

@@ -1,26 +1,26 @@

1−unique001a.idr:33:11:Type mismatch between

1+unique001a.idr:35:11:Type mismatch between

2 Int -> String

3and

4 UniqueType (Int -> String)

5−unique001a.idr:44:12:Type mismatch between

5+unique001a.idr:46:12:Type mismatch between

6 Int -> String

7and

8 UniqueType (Int -> String)

9−unique001a.idr:55:12:Type mismatch between

9+unique001a.idr:57:12:Type mismatch between

10 UniqueType (Int -> String)

11and

12 Int -> String

13−unique001b.idr:16:7:Borrowed name xs must not be used on RHS

13+unique001b.idr:18:7:Borrowed name xs must not be used on RHS

14−unique001c.idr:46:6:Unique name f is used more than once

14+unique001c.idr:47:6:Unique name f is used more than once

15−unique001d.idr:3:7:Borrowed name x must not be used on RHS

15+unique001d.idr:4:7:Borrowed name x must not be used on RHS

16−unique001e.idr:3:10:

16+unique001e.idr:4:10:

17Constructor Main.Nil has a UniqueType, but the data type does not

18−unique002.idr:15:5:Unique name xs is used more than once

18+unique002.idr:17:5:Unique name xs is used more than once

19−unique002a.idr:15:5:Type mismatch between

19+unique002a.idr:17:5:Type mismatch between

20 Int -> String

21and

22 UniqueType (Int -> String)

23−unique003.idr:18:5:Type mismatch between

23+unique003.idr:20:5:Type mismatch between

24 Int -> String

25and

26 UniqueType (Int -> String)

test/unique004/unique001a.idr+2

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

1module Main

2

3+%language UniquenessTypes

4+

3data UList : Type -> UniqueType where

5data UList : Type -> UniqueType where

4 Nil : UList a

6 Nil : UList a

5 (::) : a -> UList a -> UList a

7 (::) : a -> UList a -> UList a

test/unique004/unique001b.idr+2

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

1module Main

2

3+%language UniquenessTypes

4+

3data UList : Type -> UniqueType where

5data UList : Type -> UniqueType where

4 Nil : UList a

6 Nil : UList a

5 (::) : a -> UList a -> UList a

7 (::) : a -> UList a -> UList a

test/unique004/unique001c.idr+1

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

1+%language UniquenessTypes

1

2

2data UList : Type -> UniqueType where

3data UList : Type -> UniqueType where

3 UNil : UList a

4 UNil : UList a

test/unique004/unique001d.idr+1

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

1+%language UniquenessTypes

1

2

2steal : {a : UniqueType} -> Borrowed a -> a

3steal : {a : UniqueType} -> Borrowed a -> a

3steal (Read x) = x

4steal (Read x) = x

test/unique004/unique001e.idr+1

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

1+%language UniquenessTypes

1

2

2data BadList : UniqueType -> Type where

3data BadList : UniqueType -> Type where

3 Nil : {a : UniqueType} -> BadList a

4 Nil : {a : UniqueType} -> BadList a

test/unique004/unique002.idr+2

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

1+%language UniquenessTypes

2+

1data UList : Type -> UniqueType where

3data UList : Type -> UniqueType where

2 Nil : UList a

4 Nil : UList a

3 (::) : a -> UList a -> UList a

5 (::) : a -> UList a -> UList a

test/unique004/unique002a.idr+2

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

1+%language UniquenessTypes

2+

1data UList : Type -> UniqueType where

3data UList : Type -> UniqueType where

2 Nil : UList a

4 Nil : UList a

3 (::) : a -> UList a -> UList a

5 (::) : a -> UList a -> UList a

test/unique004/unique003.idr+2

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

1module Main

2

3+%language UniquenessTypes

4+

3data UList : Type -> UniqueType where

5data UList : Type -> UniqueType where

4 Nil : UList a

6 Nil : UList a

5 (::) : a -> UList a -> UList a

7 (::) : a -> UList a -> UList a