bf0fe16 · Idris-dev · git.iko.soy

CHANGELOG+19−6

compare with master

unifiedsplit

@@ -9,20 +9,31 @@ Language updates

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.

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

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

14+ at some point in the future.

15+* Changed scoping rules for unbound implicits: any name which would be a

16+ valid unbound implicit is now *always* an unbound implicit. This is much

17+ more resilient to changes in inputs, but does require that function names

18+ be explicitly qualified when in argument position.

12* Dependent pairs now can be specified using a telescope-style syntax, without

19* Dependent pairs now can be specified using a telescope-style syntax, without

13−requirement of nesting, e.g. it is possible to now write (a : Type ** n : Nat

20+ requirement of nesting, e.g. it is possible to now write the following:

14−** Vect n a).

21+ (a : Type ** n : Nat ** Vect n a)

22+

15

23

16Library updates

24Library updates

17---------------

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

18

26

19* The 'Neg' class now represents numeric types which can be negative. As

27* The 'Neg' class now represents numeric types which can be negative. As

20−such, the (-) operator and 'abs' have been moved there from 'Num'.

28+ such, the (-) operator and 'abs' have been moved there from 'Num'.

21* A special version of (-) on 'Nat' requires that the second argument is

29* A special version of (-) on 'Nat' requires that the second argument is

22−smaller than or equal to the first. 'minus' retains the old behaviour,

30+ smaller than or equal to the first. 'minus' retains the old behaviour,

23−returning Z if there is an underflow.

31+ returning Z if there is an underflow.

32+* The (+), (-), and (*) operations on Fin have been removed.

24* New Logging Effects have been added to facilitate logging of effectful

33* New Logging Effects have been added to facilitate logging of effectful

25 programmes.

34 programmes.

35+* Elaborator reflection is now a part of the prelude. It is no longer

36+ necessary to import Language.Reflection.Elab.

26

37

27Tool updates

38Tool updates

28------------

39------------

@@ -31,8 +42,10 @@ Tool updates

31

42

32Miscellaneous updates

43Miscellaneous updates

33---------------------

44---------------------

45+* Disable the deprecation warnings for %elim and old-style tactic scripts

46+ with the --no-elim-deprecation-warnings and --no-tactic-deprecation-warnings

47+ flags.

34

48

35−[None so far]

36

49

37New in 0.9.19:

50New in 0.9.19:

38--------------

51--------------

config.mk+4

@@ -26,11 +26,15 @@ ifneq (, $(findstring cygwin, $(MACHINE)))

26else

27ifneq (, $(findstring mingw, $(MACHINE)))

28 OS :=windows

29+else

30+ifneq (, $(findstring windows, $(MACHINE)))

31+ OS :=windows

29else

32else

30 OS :=unix

33 OS :=unix

31endif

34endif

32endif

35endif

33endif

36endif

37+endif

34

38

35ifeq ($(OS),darwin)

39ifeq ($(OS),darwin)

36 SHLIB_SUFFIX :=.dylib

40 SHLIB_SUFFIX :=.dylib

docs/reference/elaborator-reflection.rst+9−7

@@ -11,11 +11,6 @@ For details, see Edwin Brady's 2013 paper in the Journal of Functional Programmi

11Elaborator reflection makes the elaboration type as well as a selection of its tactics available to Idris code.

12This means that metaprograms written in Idris can have complete control over the elaboration process, generating arbitrary code, and they have access to all of the facilities available in the elaborator, such as higher-order unification, type checking, and emitting auxiliary definitions.

13

14−WARNING

15−=======

16−

17−Elaborator reflection is a new, **experimental** feature. It **will change**. You've been warned.

18−

19The Elaborator State

14The Elaborator State

20====================

15====================

21

16

@@ -81,8 +76,15 @@ Interactively Building Elab Scripts

81

76

82To build an ``Elab`` script interactively, use the ``:elab`` command at the REPL.

77To build an ``Elab`` script interactively, use the ``:elab`` command at the REPL.

83It takes the name of a hole as an argument.

78It takes the name of a hole as an argument.

84−The interface is largely the same as in Idris's interactive prover, except all meta-commands start with colon.

79+To list all available holes, use the command ``:m``.

85−For example, use ``:qed`` instead of ``qed``, ``:abandon`` instead of ``abandon``, and ``:undo`` instead of ``undo``.

80+

81+In interactive elaboration shell, the following commands are available:

82+- ``:q`` - Quits the elaboration shell (gives up on proving current lemma).

83+- ``:abandon`` - Same as :q

84+- ``:state`` - Displays the current state of the term being constructed.

85+- ``:term`` - Displays the current proof term complete with its yet-to-be-filled holes.

86+- ``:undo`` - Undoes the last tactic.

87+- ``:qed`` - Once the elaboration shell tells you "No more goals," you get to type this in celebration! (Completes the construction and exits the shell)

86

88

87

89

88Failure

90Failure

docs/reference/tactics.rst+10−6

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

1***************************

2−Tactics and Theorem Proving

2+DEPRECATED: Tactics and Theorem Proving

3***************************

4

5+.. warning::

6+ The interactive theorem-proving interface documented here has been

7+ deprecated in favor of :ref:`elaborator-reflection`.

8+

5Idris supports interactive theorem proving, and the analyse of context

9Idris supports interactive theorem proving, and the analyse of context

6through holes. To list all unproven holes, use the command ``:m``.

10through holes. To list all unproven holes, use the command ``:m``.

7This will display their qualified names and the expected types. To

11This will display their qualified names and the expected types. To

@@ -15,12 +19,12 @@ Basic commands

15==============

19==============

16

20

17- ``:q`` - Quits the prover (gives up on proving current lemma).

21- ``:q`` - Quits the prover (gives up on proving current lemma).

18−- ``abandon`` - Same as :q

22+- ``:abandon`` - Same as :q

19−- ``state`` - Displays the current state of the proof.

23+- ``:state`` - Displays the current state of the proof.

20−- ``term`` - Displays the current proof term complete with its

24+- ``:term`` - Displays the current proof term complete with its

21 yet-to-be-filled holes (is only really useful for debugging).

25 yet-to-be-filled holes (is only really useful for debugging).

22−- ``undo`` - Undoes the last tactic.

26+- ``:undo`` - Undoes the last tactic.

23−- ``qed`` - Once the interactive theorem prover tells you "No more

27+- ``:qed`` - Once the interactive theorem prover tells you "No more

24 goals," you get to type this in celebration! (Completes the proof and

28 goals," you get to type this in celebration! (Completes the proof and

25 exits the prover)

29 exits the prover)

26

30

docs/tutorial/starting.rst+2

@@ -66,6 +66,8 @@ Some useful options to the Idris command are:

66

67- ``--check`` type check the file and its dependencies without starting the interactive environment.

68

69+- ``--package pkg`` add package as dependency, e.g. ``--package contrib`` to make use of the contrib package.

70+

69- ``--help`` display usage summary and command line options.

71- ``--help`` display usage summary and command line options.

70

72

71The Interactive Environment

73The Interactive Environment

idris.cabal+15−1

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

1Name: idris

2−Version: 0.9.19

2+Version: 0.9.19.1

3License: BSD3

4License-file: LICENSE

5Author: Edwin Brady

@@ -143,6 +143,13 @@ Extra-source-files:

143 libs/effects/Effect/Logging/*.idr

144 libs/effects/*.idr

145

146+ libs/pruviloj/Makefile

147+ libs/pruviloj/pruviloj.ipkg

148+ libs/pruviloj/*.idr

149+ libs/pruviloj/Pruviloj/*.idr

150+ libs/pruviloj/Pruviloj/Derive/*.idr

151+ libs/pruviloj/Pruviloj/Internals/*.idr

152+

146 test/Makefile

153 test/Makefile

147 test/runtest.pl

154 test/runtest.pl

148 test/reg001/run

155 test/reg001/run

@@ -346,6 +353,9 @@ Extra-source-files:

346 test/basic014/run

353 test/basic014/run

347 test/basic014/*.idr

354 test/basic014/*.idr

348 test/basic014/expected

355 test/basic014/expected

356+ test/basic015/run

357+ test/basic015/*.idr

358+ test/basic015/expected

349

359

350 test/bignum001/run

360 test/bignum001/run

351 test/bignum001/*.idr

361 test/bignum001/*.idr

@@ -599,6 +609,10 @@ Extra-source-files:

599 test/proofsearch003/*.idr

609 test/proofsearch003/*.idr

600 test/proofsearch003/expected

610 test/proofsearch003/expected

601

611

612+ test/pruviloj001/run

613+ test/pruviloj001/*.idr

614+ test/pruviloj001/expected

615+

602 test/quasiquote001/run

616 test/quasiquote001/run

603 test/quasiquote001/*.idr

617 test/quasiquote001/*.idr

604 test/quasiquote001/expected

618 test/quasiquote001/expected

jsrts/Runtime-browser.js+4

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

1+var i$getLine = function() {

2+ return prompt("Prelude.getLine");

3+}

4+

1var i$putStr = function(s) {

5var i$putStr = function(s) {

2 console.log(s);

6 console.log(s);

3};

7};

libs/Makefile+6−1

@@ -3,6 +3,7 @@ build:

3 $(MAKE) -C base build

4 $(MAKE) -C contrib build

5 $(MAKE) -C effects build

6+ $(MAKE) -C pruviloj build

6

7

8

8install:

9install:

@@ -10,24 +11,28 @@ install:

10 $(MAKE) -C base install

11 $(MAKE) -C base install

11 $(MAKE) -C contrib install

12 $(MAKE) -C contrib install

12 $(MAKE) -C effects install

13 $(MAKE) -C effects install

14+ $(MAKE) -C pruviloj install

13

15

14clean:

16clean:

15 $(MAKE) -C prelude clean

17 $(MAKE) -C prelude clean

16 $(MAKE) -C base clean

18 $(MAKE) -C base clean

17 $(MAKE) -C contrib clean

19 $(MAKE) -C contrib clean

18 $(MAKE) -C effects clean

20 $(MAKE) -C effects clean

21+ $(MAKE) -C pruviloj clean

19

22

20doc:

23doc:

21 $(MAKE) -C prelude doc

24 $(MAKE) -C prelude doc

22 $(MAKE) -C base doc

25 $(MAKE) -C base doc

23 $(MAKE) -C contrib doc

26 $(MAKE) -C contrib doc

24 $(MAKE) -C effects doc

27 $(MAKE) -C effects doc

28+ $(MAKE) -C pruviloj doc

25

29

26doc_clean:

30doc_clean:

27 $(MAKE) -C prelude doc_clean

31 $(MAKE) -C prelude doc_clean

28 $(MAKE) -C base doc_clean

32 $(MAKE) -C base doc_clean

29 $(MAKE) -C contrib doc_clean

33 $(MAKE) -C contrib doc_clean

30− $(MAKE) -C effects doc_clean

34+ $(MAKE) -C effects doc_clean

35+ $(MAKE) -C pruviloj doc_clean

31

36

32

37

33.PHONY: build install clean doc doc_clean

38.PHONY: build install clean doc doc_clean

libs/base/Data/Fin.idr+2−20

@@ -42,7 +42,7 @@ finToNatInjective FZ FZ Refl = Refl

42finToNatInjective (FS m) FZ Refl impossible

43finToNatInjective FZ (FS n) Refl impossible

44finToNatInjective (FS m) (FS n) prf =

45− cong (finToNatInjective m n (succInjective (finToNat m) (finToNat n) prf))

45+ cong (finToNatInjective m n (succInjective (finToNat m) (finToNat n) prf))

46

47instance Cast (Fin n) Nat where

48 cast x = finToNat x

@@ -94,7 +94,7 @@ instance Ord (Fin n) where

94 compare FZ (FS _) = LT

95 compare (FS _) FZ = GT

96 compare (FS x) (FS y) = compare x y

97−

97+

98instance MinBound (Fin (S n)) where

99 minBound = FZ

100

@@ -102,24 +102,6 @@ instance MaxBound (Fin (S n)) where

102 maxBound = last

103

104

105−||| Add two Fins, extending the bound

106−(+) : Fin n -> Fin m -> Fin (n + m)

107−(+) {n=S n} {m=m} FZ f' = rewrite plusCommutative n m in weaken (weakenN n f')

108−(+) (FS f) f' = FS (f + f')

109−

110−||| Substract two Fins, keeping the bound of the minuend

111−(-) : Fin n -> Fin m -> Fin n

112−FZ - _ = FZ

113−f - FZ = f

114−(FS f) - (FS f') = weaken $ f - f'

115−

116−||| Multiply two Fins, extending the bound

117−(*) : Fin n -> Fin m -> Fin (n * m)

118−(*) {n=Z} f f' = FinZElim f

119−(*) {m=Z} f f' = FinZElim f'

120−(*) {n=S n} {m=S m} FZ f' = FZ

121−(*) {n=S n} {m=S m} (FS f) f' = f' + (f * f')

122−

123-- Construct a Fin from an integer literal which must fit in the given Fin

105-- Construct a Fin from an integer literal which must fit in the given Fin

124

106

125natToFin : Nat -> (n : Nat) -> Maybe (Fin n)

107natToFin : Nat -> (n : Nat) -> Maybe (Fin n)

libs/base/Debug/Error.idr+1−1

@@ -8,7 +8,7 @@ import System

8||| @ loc The source location to display for the error

9||| @ message The error to print

10partial

11−error : {default tactics {sourceLocation} loc : SourceLocation} ->

11+error : {default (%runElab sourceLocation) loc : SourceLocation} ->

12 (message : String) ->

13 a

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

libs/base/base.ipkg+1−1

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

1package base

2

3−opts = "--nobasepkgs --total -i ../prelude"

3+opts = "--nobasepkgs --total --no-elim-deprecation-warnings -i ../prelude"

4modules = System,

5

6 Debug.Error, Debug.Trace,

libs/contrib/Classes/Verified.idr+13−16

@@ -17,12 +17,10 @@ class Functor f => VerifiedFunctor (f : Type -> Type) where

17 (g1 : a -> b) -> (g2 : b -> c) ->

18 map (g2 . g1) x = (map g2 . map g1) x

19

20−

21−

22class (Applicative f, VerifiedFunctor f) => VerifiedApplicative (f : Type -> Type) where

20class (Applicative f, VerifiedFunctor f) => VerifiedApplicative (f : Type -> Type) where

23 applicativeMap : (x : f a) -> (g : a -> b) ->

21 applicativeMap : (x : f a) -> (g : a -> b) ->

24 map g x = pure g <*> x

22 map g x = pure g <*> x

25− applicativeIdentity : (x : f a) -> pure id <*> x = x

23+ applicativeIdentity : (x : f a) -> pure Basics.id <*> x = x

26 applicativeComposition : (x : f a) -> (g1 : f (a -> b)) -> (g2 : f (b -> c)) ->

24 applicativeComposition : (x : f a) -> (g1 : f (a -> b)) -> (g2 : f (b -> c)) ->

27 ((pure (.) <*> g2) <*> g1) <*> x = g2 <*> (g1 <*> x)

25 ((pure (.) <*> g2) <*> g1) <*> x = g2 <*> (g1 <*> x)

28 applicativeHomomorphism : (x : a) -> (g : a -> b) ->

26 applicativeHomomorphism : (x : a) -> (g : a -> b) ->

@@ -30,14 +28,13 @@ class (Applicative f, VerifiedFunctor f) => VerifiedApplicative (f : Type -> Typ

30 applicativeInterchange : (x : a) -> (g : f (a -> b)) ->

28 applicativeInterchange : (x : a) -> (g : f (a -> b)) ->

31 g <*> pure x = pure (\g' : a -> b => g' x) <*> g

29 g <*> pure x = pure (\g' : a -> b => g' x) <*> g

32

30

33−

34class (Monad m, VerifiedApplicative m) => VerifiedMonad (m : Type -> Type) where

31class (Monad m, VerifiedApplicative m) => VerifiedMonad (m : Type -> Type) where

35 monadApplicative : (mf : m (a -> b)) -> (mx : m a) ->

32 monadApplicative : (mf : m (a -> b)) -> (mx : m a) ->

36 mf <*> mx = mf >>= \f =>

33 mf <*> mx = mf >>= \f =>

37 mx >>= \x =>

34 mx >>= \x =>

38 pure (f x)

35 pure (f x)

39 monadLeftIdentity : (x : a) -> (f : a -> m b) -> return x >>= f = f x

36 monadLeftIdentity : (x : a) -> (f : a -> m b) -> return x >>= f = f x

40− monadRightIdentity : (mx : m a) -> mx >>= return = mx

37+ monadRightIdentity : (mx : m a) -> mx >>= Monad.return = mx

41 monadAssociativity : (mx : m a) -> (f : a -> m b) -> (g : b -> m c) ->

38 monadAssociativity : (mx : m a) -> (f : a -> m b) -> (g : b -> m c) ->

42 (mx >>= f) >>= g = mx >>= (\x => f x >>= g)

39 (mx >>= f) >>= g = mx >>= (\x => f x >>= g)

43

40

@@ -53,8 +50,8 @@ instance VerifiedSemigroup (List a) where

53

50

54

51

55class (VerifiedSemigroup a, Monoid a) => VerifiedMonoid a where

52class (VerifiedSemigroup a, Monoid a) => VerifiedMonoid a where

56− total monoidNeutralIsNeutralL : (l : a) -> l <+> neutral = l

53+ total monoidNeutralIsNeutralL : (l : a) -> l <+> Algebra.neutral = l

57− total monoidNeutralIsNeutralR : (r : a) -> neutral <+> r = r

54+ total monoidNeutralIsNeutralR : (r : a) -> Algebra.neutral <+> r = r

58

55

59-- instance VerifiedMonoid Nat where

56-- instance VerifiedMonoid Nat where

60-- monoidNeutralIsNeutralL = plusZeroRightNeutral

57-- monoidNeutralIsNeutralL = plusZeroRightNeutral

@@ -65,8 +62,8 @@ instance VerifiedMonoid (List a) where

65 monoidNeutralIsNeutralR xs = Refl

62 monoidNeutralIsNeutralR xs = Refl

66

63

67class (VerifiedMonoid a, Group a) => VerifiedGroup a where

64class (VerifiedMonoid a, Group a) => VerifiedGroup a where

68− total groupInverseIsInverseL : (l : a) -> l <+> inverse l = neutral

65+ total groupInverseIsInverseL : (l : a) -> l <+> inverse l = Algebra.neutral

69− total groupInverseIsInverseR : (r : a) -> inverse r <+> r = neutral

66+ total groupInverseIsInverseR : (r : a) -> inverse r <+> r = Algebra.neutral

70

67

71class (VerifiedGroup a, AbelianGroup a) => VerifiedAbelianGroup a where

68class (VerifiedGroup a, AbelianGroup a) => VerifiedAbelianGroup a where

72 total abelianGroupOpIsCommutative : (l, r : a) -> l <+> r = r <+> l

69 total abelianGroupOpIsCommutative : (l, r : a) -> l <+> r = r <+> l

@@ -77,12 +74,12 @@ class (VerifiedAbelianGroup a, Ring a) => VerifiedRing a where

77 total ringOpIsDistributiveR : (l, c, r : a) -> (l <+> c) <.> r = (l <.> r) <+> (c <.> r)

74 total ringOpIsDistributiveR : (l, c, r : a) -> (l <+> c) <.> r = (l <.> r) <+> (c <.> r)

78

75

79class (VerifiedRing a, RingWithUnity a) => VerifiedRingWithUnity a where

76class (VerifiedRing a, RingWithUnity a) => VerifiedRingWithUnity a where

80− total ringWithUnityIsUnityL : (l : a) -> l <.> unity = l

77+ total ringWithUnityIsUnityL : (l : a) -> l <.> Algebra.unity = l

81− total ringWithUnityIsUnityR : (r : a) -> unity <.> r = r

78+ total ringWithUnityIsUnityR : (r : a) -> Algebra.unity <.> r = r

82

79

83--class (VerifiedRingWithUnity a, Field a) => VerifiedField a where

80--class (VerifiedRingWithUnity a, Field a) => VerifiedField a where

84−-- total fieldInverseIsInverseL : (l : a) -> (notId : Not (l = neutral)) -> l <.> (inverseM l notId) = unity

81+-- total fieldInverseIsInverseL : (l : a) -> (notId : Not (l = neutral)) -> l <.> (inverseM l notId) = Algebra.unity

85−-- total fieldInverseIsInverseR : (r : a) -> (notId : Not (r = neutral)) -> (inverseM r notId) <.> r = unity

82+-- total fieldInverseIsInverseR : (r : a) -> (notId : Not (r = neutral)) -> (inverseM r notId) <.> r = Algebra.unity

86

83

87

84

88class JoinSemilattice a => VerifiedJoinSemilattice a where

85class JoinSemilattice a => VerifiedJoinSemilattice a where

@@ -96,10 +93,10 @@ class MeetSemilattice a => VerifiedMeetSemilattice a where

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

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

97

94

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

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

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

96+ total boundedJoinSemilatticeBottomIsBottom : (e : a) -> join e Algebra.bottom = e

100

97

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

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

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

99+ total boundedMeetSemilatticeTopIsTop : (e : a) -> meet e Algebra.top = e

103

100

104class (VerifiedJoinSemilattice a, VerifiedMeetSemilattice a) => VerifiedLattice a where

101class (VerifiedJoinSemilattice a, VerifiedMeetSemilattice a) => VerifiedLattice a where

105 total latticeMeetAbsorbsJoin : (l, r : a) -> meet l (join l r) = l

102 total latticeMeetAbsorbsJoin : (l, r : a) -> meet l (join l r) = l

@@ -110,7 +107,7 @@ class (VerifiedBoundedJoinSemilattice a, VerifiedBoundedMeetSemilattice a, Verif

110

107

111--class (VerifiedRingWithUnity a, VerifiedAbelianGroup b, Module a b) => VerifiedModule a b where

108--class (VerifiedRingWithUnity a, VerifiedAbelianGroup b, Module a b) => VerifiedModule a b where

112-- total moduleScalarMultiplyComposition : (x,y : a) -> (v : b) -> x <#> (y <#> v) = (x <.> y) <#> v

109-- total moduleScalarMultiplyComposition : (x,y : a) -> (v : b) -> x <#> (y <#> v) = (x <.> y) <#> v

113−-- total moduleScalarUnityIsUnity : (v : b) -> unity {a} <#> v = v

110+-- total moduleScalarUnityIsUnity : (v : b) -> Algebra.unity {a} <#> v = v

114-- total moduleScalarMultDistributiveWRTVectorAddition : (s : a) -> (v, w : b) -> s <#> (v <+> w) = (s <#> v) <+> (s <#> w)

111-- total moduleScalarMultDistributiveWRTVectorAddition : (s : a) -> (v, w : b) -> s <#> (v <+> w) = (s <#> v) <+> (s <#> w)

115-- total moduleScalarMultDistributiveWRTModuleAddition : (s, t : a) -> (v : b) -> (s <+> t) <#> v = (s <#> v) <+> (t <#> v)

112-- total moduleScalarMultDistributiveWRTModuleAddition : (s, t : a) -> (v : b) -> (s <+> t) <#> v = (s <#> v) <+> (t <#> v)

116

113

libs/contrib/Control/Algebra.idr+1−1

@@ -113,7 +113,7 @@ class Ring a => RingWithUnity a where

113||| forall a b c, a <.> (b <+> c) == (a <.> b) <+> (a <.> c)

114||| forall a b c, (a <+> b) <.> c == (a <.> c) <+> (b <.> c)

115class RingWithUnity a => Field a where

116− inverseM : (x : a) -> Not (x = neutral) -> a

116+ inverseM : (x : a) -> Not (x = Algebra.neutral) -> a

117

118sum' : (Foldable t, Monoid a) => t a -> a

119sum' = concat

libs/contrib/Data/Heap.idr+10−19

@@ -133,21 +133,21 @@ instance Ord a => Monoid (MaxiphobicHeap a) where

133-- Properties

134--------------------------------------------------------------------------------

135

136+total

136−total absurdBoolDischarge : False = True -> Void

137+absurdBoolDischarge : False = True -> Void

137−absurdBoolDischarge p = replace {P = disjointTy} p ()

138+absurdBoolDischarge Refl impossible

138− where

139− total disjointTy : Bool -> Type

140− disjointTy False = ()

141− disjointTy True = Void

142

139

140+total

143−total isEmptySizeZero : (h : MaxiphobicHeap a) -> (isEmpty h = True) -> size h = Z

141+isEmptySizeZero : (h : MaxiphobicHeap a) -> (isEmpty h = True) -> size h = Z

144isEmptySizeZero Empty p = Refl

142isEmptySizeZero Empty p = Refl

145−isEmptySizeZero (Node s l e r) p = ?isEmptySizeZeroNodeAbsurd

143+isEmptySizeZero (Node s l e r) Refl impossible

146

144

145+total

147−total emptyHeapValid : Ord a => isValidHeap (empty {a}) = True

146+emptyHeapValid : Ord a => isValidHeap (empty {a}) = True

148emptyHeapValid = Refl

147emptyHeapValid = Refl

149

148

149+total

150−total singletonHeapValid : Ord a => (e : a) -> isValidHeap $ singleton e = True

150+singletonHeapValid : Ord a => (e : a) -> isValidHeap $ singleton e = True

151singletonHeapValid e = Refl

152

153{-

@@ -161,16 +161,7 @@ mergePreservesValidHeaps (Node ls ll le lr) (Node rs rl re rr) lp rp =

161 ?mergePreservesValidHeapsBody

162-}

163

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

165−-- Proofs

166−--------------------------------------------------------------------------------

167

164

168−isEmptySizeZeroNodeAbsurd = proof {

169− intros;

170− refine void;

171− refine absurdBoolDischarge;

172− exact p;

173−}

174

165

175--------------------------------------------------------------------------------

166--------------------------------------------------------------------------------

176-- Debug

167-- Debug

libs/effects/Effects.idr+6−11

@@ -254,9 +254,8 @@ execEff : Env m xs -> (p : EffElem e res xs) ->

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

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

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

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

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

257+execEff (val :: env) (There p) eff k

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

258+ = execEff env p eff (\v, env' => k v (val :: env'))

260

259

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

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

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

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

@@ -271,11 +270,7 @@ eff env (liftP prf effP) k

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

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

272eff env (new (MkEff resTy newEff) res {prf=Refl} effP) k

271eff env (new (MkEff resTy newEff) res {prf=Refl} effP) k

273 = eff (res :: env) effP (\p', (val :: envk) => k p' envk)

272 = eff (res :: env) effP (\p', (val :: envk) => k p' envk)

274−-- FIXME:

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

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

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

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

273+eff env (l :- prog) k

279 = let env' = unlabel env in

274 = let env' = unlabel env in

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

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

281

276

@@ -325,8 +320,8 @@ run prog {env} = eff env prog (\r, env => pure r)

325|||

320|||

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

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

327%no_implicit

322%no_implicit

328−runPure : (prog : EffM id a xs xs') ->

323+runPure : (prog : EffM Basics.id a xs xs') ->

329− {default MkDefaultEnv env : Env id xs} -> a

324+ {default MkDefaultEnv env : Env Basics.id xs} -> a

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

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

331

326

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

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

@@ -346,7 +341,7 @@ runInit env prog = eff env prog (\r, env => pure r)

346||| @env The environment to use.

341||| @env The environment to use.

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

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

348%no_implicit

343%no_implicit

349−runPureInit : (env : Env id xs) -> (prog : EffM id a xs xs') -> a

344+runPureInit : (env : Env Basics.id xs) -> (prog : EffM Basics.id a xs xs') -> a

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

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

351

346

352%no_implicit

347%no_implicit

libs/prelude/Language/Reflection/Elab.idr+17

@@ -139,6 +139,7 @@ data Elab : Type -> Type where

139 prim__Compute : Elab ()

140 prim__Normalise : (List (TTName, Binder TT)) -> TT -> Elab TT

141 prim__Whnf : TT -> Elab TT

142+ prim__Converts : (List (TTName, Binder TT)) -> TT -> TT -> Elab ()

142

143

143 prim__DeclareType : TyDecl -> Elab ()

144 prim__DeclareType : TyDecl -> Elab ()

144 prim__DefineFunction : FunDefn -> Elab ()

145 prim__DefineFunction : FunDefn -> Elab ()

@@ -373,6 +374,22 @@ namespace Tactics

373 whnf : (term : TT) -> Elab TT

374 whnf : (term : TT) -> Elab TT

374 whnf term = prim__Whnf term

375 whnf term = prim__Whnf term

375

376

377+ ||| Check that two terms are convertable in the current context and

378+ ||| in some environment.

379+ |||

380+ ||| @ env a lexical environment to compare the terms in (see `getEnv`)

381+ ||| @ term1 the first term to convert

382+ ||| @ term2 the second term to convert

383+ convertsInEnv : (env : List (TTName, Binder TT)) -> (term1, term2 : TT) -> Elab ()

384+ convertsInEnv env term1 term2 = prim__Converts env term1 term2

385+

386+ ||| Check that two terms are convertable in the current context and environment

387+ |||

388+ ||| @ term1 the first term to convert

389+ ||| @ term2 the second term to convert

390+ converts : (term1, term2 : TT) -> Elab ()

391+ converts term1 term2 = convertsInEnv !getEnv term1 term2

392+

376 ||| Find the source context for the elaboration script

393 ||| Find the source context for the elaboration script

377 getSourceLocation : Elab SourceLocation

394 getSourceLocation : Elab SourceLocation

378 getSourceLocation = prim__SourceLocation

395 getSourceLocation = prim__SourceLocation

libs/prelude/Prelude.idr+1

@@ -30,6 +30,7 @@ import public Prelude.File

30import public Prelude.Doubles

31import public Decidable.Equality

32import public Language.Reflection

33+import public Language.Reflection.Elab

33import public Language.Reflection.Errors

34import public Language.Reflection.Errors

34

35

35%access public

36%access public

libs/prelude/Prelude/Applicative.idr+4

@@ -72,3 +72,7 @@ when False f = pure ()

72||| Note: In Haskell, `choice` is called `asum`.

73choice : (Foldable t, Alternative f) => t (f a) -> f a

74choice x = foldr (<|>) empty x

75+

76+||| A fused version of choice and map.

77+choiceMap : (Foldable t, Alternative f) => (a -> f b) -> t a -> f b

78+choiceMap f x = foldr (\elt, acc => f elt <|> acc) empty x

libs/prelude/Prelude/Chars.idr+2−2

@@ -7,7 +7,7 @@ import Prelude.List

7import Prelude.Cast

8import Builtins

9

10−||| Return the ASCII representation of the character.

10+||| Convert the number to its ASCII equivalent.

11chr : Int -> Char

12chr x = if (x >= 0 && x < 0x110000)

13 then assert_total (prim__intToChar x)

@@ -16,7 +16,7 @@ chr x = if (x >= 0 && x < 0x110000)

16instance Cast Int Char where

17 cast = chr

18

19−||| Convert the number to its ASCII equivalent.

19+||| Return the ASCII representation of the character.

20ord : Char -> Int

21ord x = prim__charToInt x

22

libs/prelude/Prelude/Stream.idr+9

@@ -109,6 +109,15 @@ partial -- and the call to foldr isn't guarded anyway!

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

110scanr f (x :: xs) = f x (foldr f xs) :: scanr f xs

111

112+||| Produce a Stream repeating a sequence

113+||| @ xs the sequence to repeat

114+||| @ ok proof that the list is non-empty

115+cycle : (xs : List a) -> {auto ok : NonEmpty xs} -> Stream a

116+cycle {a} (x :: xs) {ok = IsNonEmpty} = x :: cycle' xs

117+ where cycle' : List a -> Stream a

118+ cycle' [] = x :: cycle' xs

119+ cycle' (y :: ys) = y :: cycle' ys

120+

112instance Applicative Stream where

121instance Applicative Stream where

113 pure = repeat

122 pure = repeat

114 (<*>) = zipWith apply

123 (<*>) = zipWith apply

libs/prelude/prelude.ipkg+1−1

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

1package prelude

2

3−opts = "--nobuiltins --total"

3+opts = "--nobuiltins --total --no-elim-deprecation-warnings"

4modules = Builtins, Prelude, IO,

5

6 Prelude.Algebra, Prelude.Basics, Prelude.Bool, Prelude.Cast,

libs/pruviloj/Makefilenew file+21

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

1+IDRIS := idris

2+PKG := pruviloj

3+

4+build:

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

6+

7+clean:

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

9+

10+install:

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

12+

13+rebuild: clean build

14+

15+doc:

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

17+

18+doc_clean:

19+ rm -rf ${PKG}_doc

20+

21+.PHONY: build clean install rebuild doc doc_clean

libs/pruviloj/Pruviloj.idrnew file+3

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

1+module Pruviloj

2+

3+import public Pruviloj.Core

libs/pruviloj/Pruviloj/Core.idrnew file+144

@@ -0,0 +1,144 @@

1+||| Core tactics for working with Elab reflection. These will be used

2+||| by most reasonable scripts, and they may be candidates for

3+||| eventual Prelude inclusion.

4+module Pruviloj.Core

5+

6+

7+import Language.Reflection.Elab

8+import Language.Reflection.Utils

9+

10+data Infer : Type where

11+ MkInfer : (a : Type) -> a -> Infer

12+

13+||| Run something for effects, throwing away the return value

14+ignore : Functor f => f a -> f ()

15+ignore x = map (const ()) x

16+

17+||| Do nothing

18+skip : Applicative f => f ()

19+skip = pure ()

20+

21+||| Attempt to apply a tactic. If it fails, do nothing.

22+try : Alternative f => f a -> f ()

23+try tac = ignore tac <|> pure ()

24+

25+||| Solve the goal using the most recent applicable hypothesis

26+hypothesis : Elab ()

27+hypothesis =

28+ do hyps <- map fst <$> getEnv

29+ flip choiceMap hyps $ \n =>

30+ do fill (Var n)

31+ solve

32+

33+

34+||| Generate a unique name (using `gensym`) that looks like some

35+||| previous name, for ease of debugging code generators.

36+nameFrom : TTName -> Elab TTName

37+nameFrom (UN x) =

38+ gensym $ if length x == 0 || ("_" `isPrefixOf` x)

39+ then "x"

40+ else x

41+nameFrom (NS n ns) =

42+ nameFrom n -- throw out namespaces here, because we want to

43+ -- generate bound var names

44+nameFrom (MN x n) =

45+ gensym $ if length n == 0 || ("_" `isPrefixOf` n)

46+ then "n"

47+ else n

48+nameFrom (SN x) = gensym "SN"

49+nameFrom NErased = gensym "wasErased"

50+

51+||| Get the name at the head of the term, if it exists.

52+headName : Raw -> Maybe TTName

53+headName (RApp f _) = headName f

54+headName (Var n) = Just n

55+headName x = Nothing

56+

57+||| Create a new hole with a given type without changing the

58+||| focus. Return the name of the hole.

59+|||

60+||| @ hint the hint to pass to `gensym`

61+||| @ ty the type of the new hole

62+newHole : (hint : String) -> (ty : Raw) -> Elab TTName

63+newHole hint ty =

64+ do hn <- gensym hint

65+ claim hn ty

66+ return hn

67+

68+||| Use a term to solve a hole

69+|||

70+||| @ tm the term that has the right type for the hole

71+exact : (tm : Raw) -> Elab ()

72+exact tm = do apply tm []

73+ solve

74+

75+||| Introduce as many names as possible, returning them.

76+intros : Elab (List TTName)

77+intros = do g <- snd <$> getGoal

78+ go g

79+ where go : TT -> Elab (List TTName)

80+ go (Bind n (Pi _ _) body) =

81+ do n' <- nameFrom n

82+ intro n'

83+ (n' ::) <$> go body

84+ go _ = return []

85+

86+||| Run a tactic inside of a particular hole, if it still exists. If

87+||| it has been solved, do nothing.

88+inHole : TTName -> Elab () -> Elab ()

89+inHole h todo =

90+ when (h `elem` !getHoles) $

91+ do focus h

92+ todo

93+

94+||| Restrict a polymorphic type to () for contexts where it doesn't

95+||| matter. This is nice for sticking `debug` in a context where

96+||| Idris can't solve the type.

97+simple : {m : Type -> Type} -> m () -> m ()

98+simple x = x

99+

100+||| Replace the current goal with one that's definitionally

101+||| equal. Return the name of the new goal, and ensure that it's

102+||| focused.

103+|||

104+||| @ newGoal A type that is equivalent to the current goal

105+equiv : (newGoal : Raw) -> Elab TTName

106+equiv newGoal =

107+ do h <- gensym "goal"

108+ claim h newGoal

109+ fill (Var h); solve

110+ focus h

111+ return h

112+

113+||| Remember a term built with elaboration for later use. If the

114+||| current goal is `h`, then `remember n ty` puts a fresh hole at

115+||| the front of the queue, with the old goal `h` second. The

116+||| contents of this hole end up let-bound in the scope of

117+||| `h`. Return the name of the new hole, in case it will be used

118+||| later.

119+|||

120+||| @ n the name to be used to save the term

121+||| @ ty the type to inhabit

122+remember : (n : TTName) -> (ty : Raw) -> Elab TTName

123+remember n ty =

124+ do todo <- gensym "rememberThis"

125+ claim todo ty

126+ letbind n ty (Var todo)

127+ focus todo

128+ return todo

129+

130+||| Repeat a given tactic until it fails. Fails if the tactic fails on

131+||| the first attempt; succeeds otherwise.

132+repeatUntilFail : Elab () -> Elab ()

133+repeatUntilFail tac =

134+ do tac

135+ repeatUntilFail tac <|> return ()

136+

137+||| If the current goal is a pattern-bound variable, bind it with the

138+||| expected name. Otherwise fail.

139+bindPat : Elab ()

140+bindPat = do compute

141+ g <- snd <$> getGoal

142+ case g of

143+ Bind n (PVTy _) _ => patbind n

144+ _ => fail [TermPart g, TextPart "isn't looking for a pattern."]

libs/pruviloj/Pruviloj/Derive/Eliminators.idrnew file+274

@@ -0,0 +1,274 @@

1+module Pruviloj.Derive.Eliminators

2+

3+import Language.Reflection.Utils

4+import Data.Vect

5+

6+import Pruviloj.Core

7+import Pruviloj.Internals.TyConInfo

8+import Pruviloj.Internals

9+import Pruviloj.Renamers

10+

11+

12+%access private

13+

14+bindParams : TyConInfo -> Elab ()

15+bindParams info = traverse_ (uncurry forall) (getParams info)

16+

17+||| Bind indices at new names and return a renamer that's used to

18+||| rewrite an application of something to their designated global

19+||| names

20+bindIndices : TyConInfo -> Elab Renamer

21+bindIndices info = bind' (getIndices info) (const Nothing)

22+ where bind' : List (TTName, Raw) -> Renamer -> Elab Renamer

23+ bind' [] ren = return ren

24+ bind' ((n, t) :: ixs) ren = do n' <- nameFrom n

25+ forall n' (alphaRaw ren t)

26+ bind' ixs (extend ren n n')

27+

28+||| Return the renaming required to use the result type for this

29+||| binding of the indices

30+bindTarget : TyConInfo -> Elab (TTName, Renamer)

31+bindTarget info = do ren <- bindIndices info

32+ tn <- gensym "target"

33+ forall tn (alphaRaw ren $ result info)

34+ return (tn, ren)

35+

36+elabMotive : TyConInfo -> Elab ()

37+elabMotive info = do attack

38+ ren <- bindIndices info

39+ x <- gensym "scrutinee"

40+ forall x (alphaRaw ren $ result info)

41+ fill `(Type)

42+ solve -- the attack

43+ solve -- the motive type hole

44+

45+

46+

47+

48+headsMatch : Raw -> Raw -> Bool

49+headsMatch x y =

50+ case (headName x, headName y) of

51+ (Just n1, Just n2) => n1 == n2

52+ _ => False

53+

54+||| Make an induction hypothesis if one is called for

55+mkIh : TyConInfo -> (motiveName : TTName) -> (recArg : TTName) -> (argty, fam : Raw) -> Elab ()

56+mkIh info motiveName recArg argty fam =

57+ case !(stealBindings argty (const Nothing)) of

58+ (argArgs, argRes) =>

59+ if headsMatch argRes fam

60+ then do ih <- gensym "ih"

61+ ihT <- newHole "ihT" `(Type)

62+ forall ih (Var ihT)

63+ focus ihT

64+ attack

65+ for_ {b=()} argArgs $ \(n, b) =>

66+ forall n (getBinderTy b)

67+ let argTm : Raw = mkApp (Var recArg) (map (Var . fst) argArgs)

68+ argTmTy <- forgetTypes (snd !(check argTm))

69+ argHoles <- apply (Var motiveName)

70+ (replicate (length (getIndices info))

71+ (True, 0) ++

72+ [(False,1)])

73+ argH <- snd <$> last argHoles

74+ focus argH

75+ fill argTm; solve

76+ solve -- attack

77+ solve -- ihT

78+ else return ()

79+

80+elabMethodTy : TyConInfo -> TTName -> List CtorArg -> Raw -> Raw -> Elab ()

81+elabMethodTy info motiveName [] res ctorApp =

82+ do argHoles <- apply (Var motiveName)

83+ (replicate (length (getIndices info)) (True, 0) ++

84+ [(False, 1)])

85+ argH <- snd <$> last argHoles

86+ focus argH; fill ctorApp; solve

87+ solve

88+elabMethodTy info motiveName (CtorParameter arg :: args) res ctorApp =

89+ elabMethodTy info motiveName args res (RApp ctorApp (Var (argName arg)))

90+elabMethodTy info motiveName (CtorField arg :: args) res ctorApp =

91+ do let n = argName arg

92+ let t = argTy arg

93+ attack; forall n t

94+ mkIh info motiveName n t (result info)

95+ elabMethodTy info motiveName args res (RApp ctorApp (Var n))

96+ solve

97+

98+

99+

100+elabMethod : TyConInfo -> (motiveName, ctorN : TTName) -> List CtorArg -> Raw -> Elab ()

101+elabMethod info motiveName ctorN ctorArgs resTy =

102+ do elabMethodTy info motiveName ctorArgs resTy (Var ctorN)

103+

104+

105+||| Bind a method for a constructor

106+bindMethod : TyConInfo -> (motiveName, cn : TTName) -> List CtorArg -> Raw -> Elab ()

107+bindMethod info motiveName cn cargs cty =

108+ do n <- nameFrom cn

109+ h <- newHole "methTy" `(Type)

110+ forall n (Var h)

111+ focus h; elabMethod info motiveName cn cargs cty

112+

113+getElimTy : TyConInfo -> List (TTName, List CtorArg, Raw) -> Elab Raw

114+getElimTy info ctors =

115+ do ty <- runElab `(Type) $

116+ do bindParams info

117+ (scrut, iren) <- bindTarget info

118+ motiveN <- gensym "P"

119+ motiveH <- newHole "motive" `(Type)

120+ forall motiveN (Var motiveH)

121+ focus motiveH

122+ elabMotive info

123+

124+ for_ {b=()} ctors $ \(cn, cargs, cresty) =>

125+ bindMethod info motiveN cn cargs cresty

126+ let ret = mkApp (Var motiveN)

127+ (map (Var . fst)

128+ (getIndices info) ++

129+ [Var scrut])

130+ apply (alphaRaw iren ret) []

131+ solve

132+ forgetTypes (fst ty)

133+

134+

135+

136+data ElimArg = IHArgument TTName | NormalArgument TTName

137+

138+instance Show ElimArg where

139+ show (IHArgument x) = "IHArgument " ++ show x

140+ show (NormalArgument x) = "NormalArgument " ++ show x

141+

142+getElimClause : TyConInfo -> (elimn : TTName) -> (methCount : Nat) ->

143+ (TTName, List CtorArg, Raw) -> Nat -> Elab FunClause

144+getElimClause info elimn methCount (cn, args, resTy) whichCon =

145+ elabPatternClause

146+ (do -- Establish a hole for each parameter

147+ for (getParams info) {b=()} $ \(n, ty) =>

148+ do claim n ty

149+ unfocus n

150+

151+

152+ -- Establish a hole for each argument to the constructor

153+ for {b=()} args $ \arg =>

154+ case arg of

155+ CtorParameter _ => return ()

156+ CtorField arg => do claim (argName arg) (argTy arg)

157+ unfocus (argName arg)

158+

159+ -- Establish a hole for the scrutinee (infer type)

160+ scrutinee <- newHole "scrutinee" resTy

161+

162+

163+ -- Apply the eliminator to the proper holes

164+ let paramApp : Raw = mkApp (Var elimn) $

165+ map (Var . fst) (getParams info)

166+

167+ -- We leave the RHS with a function type: motive -> method* -> res

168+ -- to make it easier to map methods to constructors

169+ holes <- apply paramApp (replicate (length (getIndices info))

170+ (True, 0) ++

171+ [(False, 1)])

172+ scr <- snd <$> last holes

173+ focus scr; fill (Var scrutinee); solve

174+ solve

175+

176+ -- Fill the scrutinee with the concrete constructor pattern

177+ focus scrutinee

178+ apply (mkApp (Var cn) $

179+ map (\x => case x of

180+ CtorParameter param => Var (argName param)

181+ CtorField arg => Var (argName arg))

182+ args)

183+ []

184+ solve)

185+ (do motiveN <- gensym "motive"

186+ intro motiveN

187+ prevMethods <- doTimes whichCon intro1

188+ methN <- gensym "useThisMethod"

189+ intro methN

190+ nextMethods <- intros

191+

192+ argSpec <- Foldable.concat <$>

193+ for args

194+ (\x =>

195+ case x of

196+ CtorParameter _ => return List.Nil

197+ CtorField arg =>

198+ do let n = argName arg

199+ let t = argTy arg

200+ (argArgs, argRes) <- stealBindings t (const Nothing)

201+ if headsMatch argRes (result info) --recursive

202+ then return [ NormalArgument n

203+ , IHArgument n

204+ ]

205+ else return [NormalArgument n])

206+

207+ argHs <- apply (Var methN) (replicate (List.length argSpec) (True, 0))

208+ solve

209+

210+ -- Now build the recursive calls for the induction hypotheses

211+ for_ {a=(ElimArg, TTName)} {b=()}

212+ !(zipH argSpec (map snd argHs))

213+ (\(spec, nh) =>

214+ case spec of

215+ NormalArgument n => do focus nh

216+ apply (Var n) []

217+ solve

218+ IHArgument n =>

219+ do focus nh

220+ attack

221+ local <- intros

222+ ihHs <- apply (Var elimn) $

223+ replicate (length (TyConInfo.args info)) (True, 0) ++

224+ [(False, 1)] ++

225+ replicate (S methCount) (True, 0)

226+ solve -- application

227+

228+ let (arg::motive::methods) = map snd $ drop (length (TyConInfo.args info)) ihHs

229+ focus arg

230+

231+ apply (mkApp (Var n) (map Var local)) []; solve

232+ solve -- attack

233+

234+

235+ focus motive; fill (Var motiveN); solve

236+ let methodArgs : List TTName = toList prevMethods ++ [methN] ++ nextMethods

237+ remaining <- zipH methods methodArgs

238+

239+ for_ {b=()} remaining $ \todo =>

240+ do focus (fst todo)

241+ fill (Var (snd todo))

242+ solve))

243+

244+

245+

246+ where bindLam : List (TTName, Binder Raw) -> Raw -> Raw

247+ bindLam [] x = x

248+ bindLam ((n, b)::rest) x = RBind n (Lam (getBinderTy b)) $ bindLam rest x

249+

250+getElimClauses : TyConInfo -> (elimn : TTName) ->

251+ List (TTName, List CtorArg, Raw) -> Elab (List FunClause)

252+getElimClauses info elimn ctors =

253+ let methodCount = length ctors

254+ in traverse (\(i, con) => getElimClause info elimn methodCount con i)

255+ (enumerate ctors)

256+

257+instance Show FunClause where

258+ show (MkFunClause x y) = "(MkFunClause " ++ show x ++ " " ++ show y ++ ")"

259+

260+abstract

261+deriveElim : (tyn, elimn : TTName) -> Elab ()

262+deriveElim tyn elimn =

263+ do -- Begin with some basic sanity checking: the type name uniquely

264+ -- determines a datatype

265+ (MkDatatype tyn tyconArgs tyconRes ctors') <- lookupDatatypeExact tyn

266+

267+ info <- getTyConInfo tyconArgs (Var tyn)

268+ ctors <- traverse (processCtorArgs info) ctors'

269+ declareType $ Declare elimn [] !(getElimTy info ctors)

270+ clauses <- getElimClauses info elimn ctors

271+

272+ defineFunction $ DefineFun elimn clauses

273+ return ()

274+

libs/pruviloj/Pruviloj/Induction.idrnew file+162

@@ -0,0 +1,162 @@

1+module Pruviloj.Induction

2+

3+import Language.Reflection.Utils

4+

5+import Pruviloj.Core

6+import Pruviloj.Derive.Eliminators

7+import Pruviloj.Internals.TyConInfo

8+import Pruviloj.Internals

9+import Pruviloj.Renamers

10+

11+

12+%access private

13+

14+-- To perform induction:

15+-- 1. Type check the thing to do induction on

16+-- 2. If its type is not an inductive family, error

17+-- 3. Ensure that there exists an eliminator for the family

18+-- 4. Abstract the goal over the scrutinee to get the motive

19+-- 5. Apply the eliminator to the scrutinee and motive, with holes for methods

20+-- 6. Return these holes

21+

22+

23+elimN : TTName -> TTName

24+elimN n = NS (SN $ MetaN (UN "elim") n) ["Eliminators", "Induction", "Pruviloj"]

25+

26+mutual

27+ alphaEqual : (subst : TTName -> Maybe TTName) -> Raw -> Raw -> Bool

28+ alphaEqual subst (Var n) (Var m) =

29+ case subst n of

30+ Just n' => n' == m -- both are bound if this has been put in the subst

31+ Nothing => n == m -- free

32+ alphaEqual subst (RBind n b tm) (RBind m b' tm') =

33+ alphaEqualBinders subst b b' &&

34+ alphaEqual (extend subst n m) tm tm'

35+ alphaEqual subst (RApp f x) (RApp g y) =

36+ alphaEqual subst f g && alphaEqual subst x y

37+ alphaEqual subst RType RType = True

38+ alphaEqual subst (RUType u) (RUType u') = u == u'

39+ alphaEqual subst (RForce tm) (RForce tm') = alphaEqual subst tm tm'

40+ alphaEqual subst (RConstant c) (RConstant c') = c == c'

41+ alphaEqual subst _ _ = False

42+

43+ alphaEqualBinders : (subst : TTName -> Maybe TTName) -> Binder Raw -> Binder Raw -> Bool

44+ alphaEqualBinders subst (Lam tm) (Lam tm') =

45+ alphaEqual subst tm tm'

46+ alphaEqualBinders subst (Pi tm1 tm2) (Pi tm1' tm2') =

47+ alphaEqual subst tm1 tm1' &&

48+ alphaEqual subst tm2 tm2'

49+ alphaEqualBinders subst (Let tm1 tm2) (Let tm1' tm2') =

50+ alphaEqual subst tm1 tm1' &&

51+ alphaEqual subst tm2 tm2'

52+ alphaEqualBinders subst (NLet tm1 tm2) (NLet tm1' tm2') =

53+ alphaEqual subst tm1 tm1' &&

54+ alphaEqual subst tm2 tm2'

55+ alphaEqualBinders subst (Hole tm) (Hole tm') =

56+ alphaEqual subst tm tm'

57+ alphaEqualBinders subst (GHole tm) (GHole tm') =

58+ alphaEqual subst tm tm'

59+ alphaEqualBinders subst (Guess tm1 tm2) (Guess tm1' tm2') =

60+ alphaEqual subst tm1 tm1' &&

61+ alphaEqual subst tm2 tm2'

62+ alphaEqualBinders subst (PVar tm) (PVar tm') =

63+ alphaEqual subst tm tm'

64+ alphaEqualBinders subst (PVTy tm) (PVTy tm') =

65+ alphaEqual subst tm tm'

66+ alphaEqualBinders subst _ _ = False

67+

68+generalize : (hint : String) -> (ctxt, subject : Raw) -> Elab (TTName, Raw)

69+generalize hint ctxt subj = do n <- gensym hint

70+ return (n, !(gen' n ctxt subj))

71+ where

72+ mutual

73+ gen' : TTName -> Raw -> Raw -> Elab Raw

74+ gen' var outer inner = if alphaEqual (const Nothing) outer inner

75+ then return (Var var)

76+ else breakAndRecurse var outer inner

77+

78+ genB : TTName -> Binder Raw -> Raw -> Elab (Binder Raw)

79+ genB n (Lam ty) inner = [| Lam (gen' n ty inner) |]

80+ genB n (Pi ty ty') inner = [| Pi (gen' n ty inner) (gen' n ty' inner) |]

81+ genB n (Let ty val) inner = [| Let (gen' n ty inner) (gen' n val inner) |]

82+ genB n (NLet ty val) inner = [| NLet (gen' n ty inner) (gen' n val inner) |]

83+ genB n (Hole ty) inner = [| Hole (gen' n ty inner) |]

84+ genB n (GHole ty) inner = [| GHole (gen' n ty inner) |]

85+ genB n (Guess ty val) inner = [| Guess (gen' n ty inner) (gen' n val inner) |]

86+ genB n (PVar ty) inner = [| PVar (gen' n ty inner) |]

87+ genB n (PVTy ty) inner = [| PVTy (gen' n ty inner) |]

88+

89+ breakAndRecurse : TTName -> Raw -> Raw -> Elab Raw

90+ breakAndRecurse var (RBind n b tm) inner =

91+ -- Prevent variable capture by alpha-converting to a unique name

92+ do n' <- nameFrom n

93+ b' <- genB var b inner

94+ body' <- gen' var (alphaRaw (rename n n') tm) inner

95+ return $ RBind n' b' body'

96+ breakAndRecurse var (RApp tm tm') inner =

97+ [| RApp (gen' var tm inner) (gen' var tm' inner) |]

98+ breakAndRecurse var other inner = return other

99+

100+

101+countBinders : TT -> Nat

102+countBinders (Bind _ _ tm) = S (countBinders tm)

103+countBinders _ = Z

104+

105+

106+

107+indexVals : Raw -> TyConInfo -> List Raw

108+indexVals tm info =

109+ do let (var, tyArgs) = unApply tm

110+ let argsTogether = zip tyArgs (args info)

111+ (argVal, TyConIndex _) <- argsTogether

112+ | _ => empty

113+ return argVal

114+

115+makeMotive : (info : TyConInfo) -> (subj, subjTy, goal : Raw) -> Elab ()

116+makeMotive info sub subjTy goal =

117+ makeMotive' (indexVals subjTy info) goal

118+ where

119+ makeMotive' : List Raw -> Raw -> Elab ()

120+ makeMotive' [] r = do (n, r') <- generalize "subj" r sub

121+ attack

122+ intro n

123+ exact r'

124+ solve -- attack

125+ makeMotive' (i :: is) r = do (n, r') <- generalize "i" r i

126+ attack

127+ intro n

128+ makeMotive' is r'

129+ solve --attack

130+

131+||| Perform induction on some expression to solve the current

132+||| goal. Return a list of new holes to be solved.

133+public

134+induction : Raw -> Elab (List TTName)

135+induction subj =

136+ do g <- goalType

137+ (_, ty) <- check subj

138+ ty' <- forgetTypes ty

139+ case headName ty' of

140+ Nothing => fail [TermPart ty, TextPart "is not an inductive family"]

141+ Just fam =>

142+ do let elim = elimN fam

143+ (_,_,elimTy) <- (lookupTyExact elim) <|> (do deriveElim fam elim

144+ lookupTyExact elim)

145+ tydef <- lookupDatatypeExact fam

146+ info <- getTyConInfo (tyConArgs tydef) (tyConRes tydef)

147+ argHoles <- apply (Var elim)

148+ (replicate (length (args info)) (True, 0) ++

149+ [(False, 0), (False, 0)] ++ -- scrutinee, motive

150+ replicate (length (constructors tydef)) (False, 1))

151+ solve

152+

153+ -- Apply the eliminator to our scrutinee

154+ scrutH <- snd <$> unsafeNth (length (args info)) argHoles

155+ focus scrutH

156+ apply subj []

157+ solve

158+

159+ motiveH <- snd <$> unsafeNth (length (args info) + 1) argHoles

160+ focus motiveH; makeMotive info subj ty' g

161+

162+ return (map snd (drop (2 + length (tyConArgs tydef)) argHoles))

libs/pruviloj/Pruviloj/Internals.idrnew file+158

@@ -0,0 +1,158 @@

1+||| Internal details of the library, not for public consumption.

2+module Pruviloj.Internals

3+

4+

5+import Pruviloj.Core

6+import Pruviloj.Renamers

7+

8+import Data.Vect

9+

10+||| Get the name of a reflected type constructor argument.

11+tyConArgName : TyConArg -> TTName

12+tyConArgName (TyConParameter a) = argName a

13+tyConArgName (TyConIndex a) = argName a

14+

15+||| Modify the name of a reflected type constructor argument.

16+setTyConArgName : TyConArg -> TTName -> TyConArg

17+setTyConArgName (TyConParameter a) n = TyConParameter (record {argName = n} a)

18+setTyConArgName (TyConIndex a) n = TyConIndex (record {argName = n} a)

19+

20+||| Modify the type of a reflected type constructor argument using some function.

21+updateTyConArgTy : (Raw -> Raw) -> TyConArg -> TyConArg

22+updateTyConArgTy f (TyConParameter a) =

23+ TyConParameter (record {argTy = f (argTy a) } a)

24+updateTyConArgTy f (TyConIndex a) =

25+ TyConIndex (record {argTy = f (argTy a) } a)

26+

27+unApply : Raw -> (Raw, List Raw)

28+unApply tm = unApply' tm []

29+ where unApply' : Raw -> List Raw -> (Raw, List Raw)

30+ unApply' (RApp f x) xs = unApply' f (x::xs)

31+ unApply' notApp xs = (notApp, xs)

32+

33+mkApp : Raw -> List Raw -> Raw

34+mkApp f [] = f

35+mkApp f (x :: xs) = mkApp (RApp f x) xs

36+

37+||| Grab the binders from around a term, alpha-converting to make

38+||| their names unique

39+partial

40+stealBindings : Raw -> (nsubst : TTName -> Maybe TTName) -> Elab (List (TTName, Binder Raw), Raw)

41+stealBindings (RBind n b tm) nsubst =

42+ do n' <- nameFrom n

43+ (bindings, result) <- stealBindings tm (extend nsubst n n')

44+ return ((n', map (alphaRaw nsubst) b) :: bindings, result)

45+stealBindings tm nsubst = return ([], alphaRaw nsubst tm)

46+

47+||| Get the last element of a list. Fail on empty lists.

48+last : List a -> Elab a

49+last [] = fail [TextPart "Unexpected empty list"]

50+last [x] = return x

51+last (_::x::xs) = last (x::xs)

52+

53+||| Grab the binders from around a term, assuming that they have been

54+||| previously uniquified

55+extractBinders : Raw -> (List (TTName, Binder Raw), Raw)

56+extractBinders (RBind n b tm) = let (bs, res) = extractBinders tm

57+ in ((n, b) :: bs, res)

58+extractBinders tm = ([], tm)

59+

60+

61+||| Get the type annotation from a binder

62+getBinderTy : Binder t -> t

63+getBinderTy (Lam t) = t

64+getBinderTy (Pi t _) = t

65+getBinderTy (Let t _) = t

66+getBinderTy (NLet t _) = t

67+getBinderTy (Hole t) = t

68+getBinderTy (GHole t) = t

69+getBinderTy (Guess t _) = t

70+getBinderTy (PVar t) = t

71+getBinderTy (PVTy t) = t

72+

73+||| Map a list `[x1, x2, ..., xn]` to `[(0, x1), (1, x2), ..., (n-1, xn)]`

74+enumerate : List a -> List (Nat, a)

75+enumerate xs = enumerate' xs 0

76+ where enumerate' : List a -> Nat -> List (Nat, a)

77+ enumerate' [] _ = []

78+ enumerate' (x::xs) n = (n, x) :: enumerate' xs (S n)

79+

80+getSigmaArgs : Raw -> Elab (Raw, Raw)

81+getSigmaArgs `(MkSigma {a=~_} {P=~_} ~rhsTy ~lhs) = return (rhsTy, lhs)

82+getSigmaArgs arg = fail [TextPart "Not a sigma constructor"]

83+

84+bindPats : List (TTName, Binder Raw) -> Raw -> Raw

85+bindPats [] res = res

86+bindPats ((n, b)::bs) res = RBind n (PVar (getBinderTy b)) $ bindPats bs res

87+

88+bindPatTys : List (TTName, Binder Raw) -> Raw -> Raw

89+bindPatTys [] res = res

90+bindPatTys ((n, b)::bs) res = RBind n (PVTy (getBinderTy b)) $ bindPatTys bs res

91+

92+

93+||| Helper for elaborating pattern clauses. This helper takes care of

94+||| inferring the type of the left-hand side and bringing that

95+||| information onward to the right-hand side.

96+|||

97+||| While elaborating the left-hand side, the proof term contains a

98+||| Sigma type. This is part of the type inference going on and will

99+||| be removed.

100+|||

101+||| @ lhs the tactic script to establish the left-hand side of the

102+||| clause. It should cause an application of the term being

103+||| defined. Any holes left behind will be converted to pattern

104+||| variables with the same name.

105+||| @ rhs the tactic script to establish the right side of the clause.

106+||| It will be run in a context where the pattern variables are

107+||| already bound, and should leave behind no holes.

108+partial

109+elabPatternClause : (lhs, rhs : Elab ()) -> Elab FunClause

110+elabPatternClause lhs rhs =

111+ do -- Elaborate the LHS in a context where its type will be solved via unification

112+ (pat, _) <- runElab `(Sigma Type id) $

113+ do th <- newHole "finalTy" `(Type)

114+ patH <- newHole "pattern" (Var th)

115+ fill `(MkSigma ~(Var th) ~(Var patH) : Sigma Type id)

116+ solve

117+ focus patH

118+ lhs

119+ -- Convert all remaining holes to pattern variables

120+ traverse_ {b=()} (\h => focus h *> patvar h) !getHoles

121+ let (pvars, sigma) = extractBinders !(forgetTypes pat)

122+ (rhsTy, lhsTm) <- getSigmaArgs sigma

123+ rhsTm <- runElab (bindPatTys pvars rhsTy) $

124+ do -- Introduce all the pattern variables from the LHS

125+ repeatUntilFail bindPat <|> return ()

126+ rhs

127+ realRhs <- forgetTypes (fst rhsTm)

128+ return $ MkFunClause (bindPats pvars lhsTm) realRhs

129+

130+||| Introduce a unique binder name, returning it

131+intro1 : Elab TTName

132+intro1 = do g <- snd <$> getGoal

133+ case g of

134+ Bind n (Pi _ _) _ => do n' <- nameFrom n

135+ intro n'

136+ return n'

137+ _ => fail [ TextPart "Can't intro1 because goal"

138+ , TermPart g

139+ , TextPart "isn't a function type."]

140+

141+

142+||| Repeat an action some number of times, saving the results.

143+doTimes : Applicative m => (n : Nat) -> m a -> m (Vect n a)

144+doTimes Z x = pure []

145+doTimes (S k) x = [| x :: (doTimes k x) |]

146+

147+||| Zip two lists, failing if their lengths don't match.

148+zipH : List a -> List b -> Elab (List (a, b))

149+zipH [] [] = return []

150+zipH (x::xs) (y::ys) = ((x, y) ::) <$> zipH xs ys

151+zipH _ _ = fail [TextPart "length mismatch"]

152+

153+unsafeNth : Nat -> List a -> Elab a

154+unsafeNth _ [] = fail [TextPart "Ran out of list elements"]

155+unsafeNth Z (x :: _) = return x

156+unsafeNth (S k) (_ :: xs) = unsafeNth k xs

157+

158+

libs/pruviloj/Pruviloj/Internals/TyConInfo.idrnew file+108

@@ -0,0 +1,108 @@

1+module Pruviloj.Derive.TyConInfo

2+

3+import Pruviloj.Core

4+import Pruviloj.Internals

5+import Pruviloj.Renamers

6+

7+import Language.Reflection.Utils

8+

9+

10+

11+||| A representation of a type constructor in which all argument names

12+||| are made unique and they are separated into params and then

13+||| indices.

14+record TyConInfo where

15+ constructor MkTyConInfo

16+ ||| Invariant: the names of the args have been made unique

17+ args : List TyConArg

18+ ||| The type constructor, applied to its arguments

19+ result : Raw

20+

21+%name TyConInfo info

22+

23+getParams : TyConInfo -> List (TTName, Raw)

24+getParams info = mapMaybe param (args info)

25+ where param : TyConArg -> Maybe (TTName, Raw)

26+ param (TyConParameter a) = Just (argName a, argTy a)

27+ param _ = Nothing

28+

29+getIndices : TyConInfo -> List (TTName, Raw)

30+getIndices info = mapMaybe index (args info)

31+ where index : TyConArg -> Maybe (TTName, Raw)

32+ index (TyConIndex a) = Just (argName a, argTy a)

33+ index _ = Nothing

34+

35+||| Rename a bound variable across a telescope

36+renameIn : (from, to : TTName) -> List (TTName, Raw) -> List (TTName, Raw)

37+renameIn from to [] = []

38+renameIn from to ((n, ty)::tele) =

39+ (n, alphaRaw (rename from to) ty) ::

40+ if from == n

41+ then tele

42+ else renameIn from to tele

43+

44+||| Rename a free variable in type constructor info (used to implement

45+||| alpha-conversion for unique binder names, hence the odd name)

46+alphaTyConInfo : (TTName -> Maybe TTName) -> TyConInfo -> TyConInfo

47+alphaTyConInfo ren (MkTyConInfo [] res) = MkTyConInfo [] (alphaRaw ren res)

48+alphaTyConInfo ren (MkTyConInfo (tcArg::tcArgs) res) =

49+ let MkTyConInfo tcArgs' res' = alphaTyConInfo (restrict ren (tyConArgName tcArg)) (MkTyConInfo tcArgs res)

50+ tcArg' = updateTyConArgTy (alphaRaw ren) tcArg

51+ in MkTyConInfo (tcArg'::tcArgs') res'

52+

53+getTyConInfo' : List TyConArg -> Raw -> (TTName -> Maybe TTName) -> Elab TyConInfo

54+getTyConInfo' [] res _ = return (MkTyConInfo [] res)

55+getTyConInfo' (tcArg::tcArgs) res ren =

56+ do let n = tyConArgName tcArg

57+ n' <- nameFrom n

58+ let ren' = extend ren n n'

59+ -- n' is globally unique so we don't worry about scope

60+ next <- getTyConInfo' tcArgs (RApp res (Var n')) ren'

61+ return $ alphaTyConInfo ren' $

62+ record {args = setTyConArgName tcArg n' :: args next} next

63+

64+getTyConInfo : List TyConArg -> Raw -> Elab TyConInfo

65+getTyConInfo args res = getTyConInfo' args res (const Nothing)

66+

67+||| Convert the parameter names in a constructor to their global unique versions

68+processCtorArgs : TyConInfo -> (TTName, List CtorArg, Raw) -> Elab (TTName, List CtorArg, Raw)

69+processCtorArgs info (cn, cargs, resTy) =

70+ do (args', ty') <- convert' (const Nothing) cargs resTy info

71+ return (cn, args', ty')

72+ where

73+ ||| Find the name that was assigned to a given parameter

74+ ||| by comparing positions in the TyConInfo

75+ findParam : TTName -> List Raw -> List TyConArg -> Elab TTName

76+ findParam paramN (Var n :: args) (TyConParameter a :: tcArgs) =

77+ if n == paramN

78+ then return (argName a)

79+ else findParam paramN args tcArgs

80+ findParam paramN (_ :: args) (_ :: tcArgs) =

81+ findParam paramN args tcArgs

82+ findParam paramN _ _ = fail [ TextPart "Parameter"

83+ , NamePart paramN

84+ , TextPart "not found."

85+ ]

86+

87+ convert' : (TTName -> Maybe TTName) ->

88+ List CtorArg -> Raw ->

89+ TyConInfo -> Elab (List CtorArg, Raw)

90+ convert' subst [] ty info = return ([], alphaRaw subst ty)

91+ convert' subst (CtorField a :: args) ty info =

92+ do n' <- nameFrom (argName a)

93+ let a' = record {

94+ argName = n'

95+ , argTy = alphaRaw subst (argTy a)

96+ } a

97+ let subst' = extend subst (argName a) n'

98+ (args', ty') <- convert' subst' args ty info

99+ return (CtorField a' :: args', ty')

100+ convert' subst (CtorParameter a :: ctorArgs) ty info =

101+ do n' <- findParam (argName a) (snd (unApply ty)) (args info)

102+ let a' = record {

103+ argName = n'

104+ , argTy = alphaRaw subst (argTy a)

105+ } a

106+ let subst' = extend subst (argName a) n'

107+ (args', ty') <- convert' subst' ctorArgs ty info

108+ return (CtorParameter a' :: args', ty')

libs/pruviloj/Pruviloj/Renamers.idrnew file+39

@@ -0,0 +1,39 @@

1+module Pruviloj.Renamers

2+

3+import Language.Reflection.Utils

4+

5+||| A renamer keeps track of names to be substituted

6+Renamer : Type

7+Renamer = TTName -> Maybe TTName

8+

9+||| Cause a renamer to forget a renaming

10+restrict : Renamer -> TTName -> Renamer

11+restrict f n n' = if n == n' then Nothing else f n'

12+

13+||| Extend a renamer with a new renaming

14+extend : Renamer -> TTName -> TTName -> Renamer

15+extend f n n' n'' = if n'' == n then Just n' else f n''

16+

17+||| Create a new renamer

18+|||

19+||| @ from the old name

20+||| @ to the new name

21+rename : (from, to : TTName) -> Renamer

22+rename from to = extend (const Nothing) from to

23+

24+||| Alpha-convert `Raw` terms

25+||| @ subst a renamer

26+partial

27+alphaRaw : (subst : Renamer) -> Raw -> Raw

28+alphaRaw subst (Var n) with (subst n)

29+ alphaRaw subst (Var n) | Nothing = Var n

30+ alphaRaw subst (Var n) | Just n' = Var n'

31+alphaRaw subst (RBind n b tm) =

32+ let subst' = restrict subst n

33+ b' = map (alphaRaw subst) b

34+ in RBind n b' (alphaRaw subst' tm)

35+alphaRaw subst (RApp tm tm') = RApp (alphaRaw subst tm) (alphaRaw subst tm')

36+alphaRaw subst RType = RType

37+alphaRaw subst (RUType x) = RUType x

38+alphaRaw subst (RForce tm) = RForce (alphaRaw subst tm)

39+alphaRaw subst (RConstant c) = RConstant c

libs/pruviloj/README.txtnew file+45

@@ -0,0 +1,45 @@

1+ ___ _

2+ / \ _ / \ _

3+| | | / \| | / \

4+| | | _ _ _ _ _ \_/| | ___ \_/

5+| ---/ \ \/ \ \/ \ \/ \| |/ \/ \

6+| | | -/| | || | || || || | || |

7+| | | | | | |\ | /| || || | || |

8+\_/ \_/ \___/ \_/ \_/\_/\___/| |

9+ _/ |

10+ |__/

11+ a proof automation and program construction toolkit

12+

13+

14+Pruviloj is a library of tactics that work with Idris's elaborator

15+reflection. In addition to a library of small tactics, it contains

16+code for generating eliminators for inductive datatypes and using

17+those eliminators to do induction.

18+

19+

20+Q: How do I use Pruviloj?

21+A: Call Idris with the "-p pruviloj" option and add:

22+ import Pruviloj

23+ to the top of your file. If you want to do induction, then

24+ add:

25+ import Pruviloj.Induction

26+ as well.

27+

28+

29+Q: How do I find out what's available?

30+A: Use ":browse Pruviloj.Core" after importing the library.

31+ Pruviloj.Induction exports only one name: "induction".

32+ Use ":doc" to read the built-in documentation.

33+

34+

35+Q: How do I use the tactics?

36+A: Please read the Idris documentation on elaborator reflection.

37+ The syntax to invoke a tactic script is "%runElab script". To

38+ interactively work with a hole, use ":elab holeName".

39+

40+

41+Q: Where does the name come from?

42+A: "Pruviloj" is Esperanto for "proof tools". The stress goes on

43+ the penultimate syllable, and in IPA the pronunciation is written

44+ [pruˈvi.loi̯]. Perhaps confusingly for Esperantists, the Pruviloj

45+ library also contains utilities for code generation.

libs/pruviloj/pruviloj.ipkgnew file+10

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

1+package pruviloj

2+

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

4+modules = Pruviloj

5+ , Pruviloj.Core

6+ , Pruviloj.Derive.Eliminators

7+ , Pruviloj.Induction

8+ , Pruviloj.Internals

9+ , Pruviloj.Internals.TyConInfo

10+ , Pruviloj.Renamers

src/IRTS/CodegenJavaScript.hs+14−6

@@ -27,6 +27,7 @@ import Data.Word

27import Data.Traversable hiding (mapM)

28import System.IO

29import System.Directory

30+import System.FilePath

30

31

31import qualified Data.Map.Strict as M

32import qualified Data.Map.Strict as M

32import qualified Data.Text as T

33import qualified Data.Text as T

@@ -113,6 +114,10 @@ codegenJS_all target definitions includes libs filename outputType = do

113 let js = concatMap (translateDecl info) bytecode

114 let js = concatMap (translateDecl info) bytecode

114 let full = concatMap processFunction js

115 let full = concatMap processFunction js

115 let code = deadCodeElim full

116 let code = deadCodeElim full

117+ let ext = takeExtension filename

118+ let isHtml = target == JavaScript && ext == ".html"

119+ let htmlPrologue = T.pack "<!doctype html><html><head><script>\n"

120+ let htmlEpilogue = T.pack "\n</script></head><body></body></html>"

116 let (cons, opt) = optimizeConstructors code

121 let (cons, opt) = optimizeConstructors code

117 let (header, rt) = case target of

122 let (header, rt) = case target of

118 Node -> ("#!/usr/bin/env node\n", "-node")

123 Node -> ("#!/usr/bin/env node\n", "-node")

@@ -132,12 +137,15 @@ codegenJS_all target definitions includes libs filename outputType = do

132 ++ idrRuntime

137 ++ idrRuntime

133 ++ tgtRuntime

138 ++ tgtRuntime

134 )

139 )

135− writeSourceText filename ( T.pack runtime

140+ let jsSource = T.pack runtime

136− `T.append` T.concat (map compileJS opt)

141+ `T.append` T.concat (map compileJS opt)

137− `T.append` T.concat (map compileJS cons)

142+ `T.append` T.concat (map compileJS cons)

138− `T.append` main

143+ `T.append` main

139− `T.append` invokeMain

144+ `T.append` invokeMain

140− )

145+ let source = if isHtml

146+ then htmlPrologue `T.append` jsSource `T.append` htmlEpilogue

147+ else jsSource

148+ writeSourceText filename source

141 setPermissions filename (emptyPermissions { readable = True

149 setPermissions filename (emptyPermissions { readable = True

142 , executable = target == Node

150 , executable = target == Node

143 , writable = True

151 , writable = True

src/Idris/AbsSyntaxTree.hs+87−32

@@ -506,10 +506,12 @@ data Opt = Filename String

506 | Client String

507 | ShowOrigErr

508 | AutoWidth -- ^ Automatically adjust terminal width

509− | AutoSolve -- ^ Automatically issue "solve" tactic in interactive prover

509+ | AutoSolve -- ^ Automatically issue "solve" tactic in old-style interactive prover

510 | UseConsoleWidth ConsoleWidth

511 | DumpHighlights

512 | DesugarNats

513+ | NoElimDeprecationWarnings -- ^ Don't show deprecation warnings for %elim

514+ | NoOldTacticDeprecationWarnings -- ^ Don't show deprecation warnings for old-style tactics

513 deriving (Show, Eq)

515 deriving (Show, Eq)

514

516

515data ElabShellCmd = EQED | EAbandon | EUndo | EProofState | EProofTerm

517data ElabShellCmd = EQED | EAbandon | EUndo | EProofState | EProofTerm

@@ -1818,20 +1820,35 @@ pprintPTerm ppo bnd docArgs infixes = prettySe (ppopt_depth ppo) startPrec bnd

1818 TypeOrTerm -> id

1820 TypeOrTerm -> id

1819 IsType -> annName pairTy

1821 IsType -> annName pairTy

1820 IsTerm -> annName pairCon

1822 IsTerm -> annName pairCon

1821− prettySe d p bnd (PDPair _ _ pun l t r) =

1823+ prettySe d p bnd dpair@(PDPair _ _ pun l t r)

1822− depth d $

1824+ | Just elts <- dPairElts dpair

1825+ = depth d . enclose (annotated lparen) (annotated rparen) .

1826+ align . group . vsep . punctuate (space <> annotated (text "**")) $

1827+ ppElts elts bnd

1828+ | otherwise

1829+ = depth d $

1823− annotated lparen <>

1830+ annotated lparen <>

1824− left <+>

1831+ left <+>

1825− annotated (text "**") <+>

1832+ annotated (text "**") <+>

1826− prettySe (decD d) startPrec (addBinding bnd) r <>

1833+ prettySe (decD d) startPrec (addBinding bnd) r <>

1827− annotated rparen

1834+ annotated rparen

1828 where annotated = case pun of

1835 where annotated = case pun of

1829 IsType -> annName sigmaTy

1836 IsType -> annName sigmaTy

1830 IsTerm -> annName sigmaCon

1837 IsTerm -> annName sigmaCon

1831 TypeOrTerm -> id

1838 TypeOrTerm -> id

1839+

1832 (left, addBinding) = case (l, pun) of

1840 (left, addBinding) = case (l, pun) of

1833 (PRef _ _ n, IsType) -> (bindingOf n False <+> text ":" <+> prettySe (decD d) startPrec bnd t, ((n, False) :))

1841 (PRef _ _ n, IsType) -> (bindingOf n False <+> text ":" <+> prettySe (decD d) startPrec bnd t, ((n, False) :))

1834 _ -> (prettySe (decD d) startPrec bnd l, id)

1842 _ -> (prettySe (decD d) startPrec bnd l, id)

1843+

1844+ ppElts [] bs = []

1845+ ppElts [(_, v)] bs = [prettySe (decD d) startPrec bs v]

1846+ ppElts ((PRef _ _ n, t):rs) bs

1847+ | IsType <- pun

1848+ = (bindingOf n False <+> colon <+>

1849+ prettySe (decD d) startPrec bs t) : ppElts rs ((n, False):bs)

1850+ ppElts ((l, t):rs) bs

1851+ = (prettySe (decD d) startPrec bs l) : ppElts rs bs

1835 prettySe d p bnd (PAlternative ns a as) =

1852 prettySe d p bnd (PAlternative ns a as) =

1836 lparen <> text "|" <> prettyAs <> text "|" <> rparen

1853 lparen <> text "|" <> prettyAs <> text "|" <> rparen

1837 where

1854 where

@@ -1949,6 +1966,11 @@ pprintPTerm ppo bnd docArgs infixes = prettySe (ppopt_depth ppo) startPrec bnd

1949 | otherwise = Just [x, y]

1966 | otherwise = Just [x, y]

1950 pairElts _ = Nothing

1967 pairElts _ = Nothing

1951

1968

1969+ dPairElts :: PTerm -> Maybe [(PTerm, PTerm)]

1970+ dPairElts (PDPair _ _ _ l t r) | Just elts <- dPairElts r = Just ((l, t):elts)

1971+ | otherwise = Just [(l, t), (Placeholder, r)]

1972+ dPairElts _ = Nothing

1973+

1952 natns = "Prelude.Nat."

1974 natns = "Prelude.Nat."

1953

1975

1954 snat :: PPOption -> Maybe Int -> Int -> PTerm -> Maybe Integer

1976 snat :: PPOption -> Maybe Int -> Int -> PTerm -> Maybe Integer

@@ -2247,41 +2269,74 @@ boundNamesIn tm = S.toList (ni 0 S.empty tm)

2247

2269

2248-- Return names which are valid implicits in the given term (type).

2270-- Return names which are valid implicits in the given term (type).

2249implicitNamesIn :: [Name] -> IState -> PTerm -> [Name]

2271implicitNamesIn :: [Name] -> IState -> PTerm -> [Name]

2250−implicitNamesIn uvars ist tm = nub $ ni 0 [] tm

2272+implicitNamesIn uvars ist tm

2273+ = let (imps, fns) = execState (ni 0 [] tm) ([], []) in

2274+ nub imps \\ nub fns

2251 where

2275 where

2276+ addImp n = do (imps, fns) <- get

2277+ put (n : imps, fns)

2278+ addFn n = do (imps, fns) <- get

2279+ put (imps, n: fns)

2280+

2281+ notCAF [] = False

2282+ notCAF (PExp _ _ _ _ : _) = True

2283+ notCAF (_ : xs) = notCAF xs

2284+

2285+ notHidden (n, _) = case getAccessibility n of

2286+ Hidden -> False

2287+ _ -> True

2288+

2289+ getAccessibility n

2290+ = case lookupDefAccExact n False (tt_ctxt ist) of

2291+ Just (n,t) -> t

2292+ _ -> Public

2293+

2252− ni 0 env (PRef _ _ n)

2294+ ni 0 env (PRef _ _ n@(NS _ _))

2253 | not (n `elem` env)

2295 | not (n `elem` env)

2254− = case lookupTy n (tt_ctxt ist) of

2296+ -- Never implicitly bind if there's a namespace

2255− [] -> [n]

2297+ = addFn n

2256− _ -> if n `elem` uvars then [n] else []

2298+ ni 0 env (PRef _ _ n)

2299+ | not (n `elem` env) && implicitable n || n `elem` uvars = addImp n

2257 ni 0 env (PApp _ f@(PRef _ _ n) as)

2300 ni 0 env (PApp _ f@(PRef _ _ n) as)

2258− | n `elem` uvars = ni 0 env f ++ concatMap (ni 0 env) (map getTm as)

2301+ | n `elem` uvars = do ni 0 env f

2302+ mapM_ (ni 0 env) (map getTm as)

2303+ | otherwise = do case lookupTy n (tt_ctxt ist) of

2304+ [] -> return ()

2305+ _ -> addFn n

2259− | otherwise = concatMap (ni 0 env) (map getTm as)

2306+ mapM_ (ni 0 env) (map getTm as)

2260− ni 0 env (PApp _ f as) = ni 0 env f ++ concatMap (ni 0 env) (map getTm as)

2307+ ni 0 env (PApp _ f as) = do ni 0 env f

2308+ mapM_ (ni 0 env) (map getTm as)

2261− ni 0 env (PAppBind _ f as) = ni 0 env f ++ concatMap (ni 0 env) (map getTm as)

2309+ ni 0 env (PAppBind _ f as) = do ni 0 env f

2310+ mapM_ (ni 0 env) (map getTm as)

2262− ni 0 env (PCase _ c os) = ni 0 env c ++

2311+ ni 0 env (PCase _ c os) = do ni 0 env c

2263 -- names in 'os', not counting the names bound in the cases

2312 -- names in 'os', not counting the names bound in the cases

2264− (nub (concatMap (ni 0 env) (map snd os))

2313+ mapM_ (ni 0 env) (map snd os)

2314+ (imps, fns) <- get

2315+ put ([] ,[])

2265− \\ nub (concatMap (ni 0 env) (map fst os)))

2316+ mapM_ (ni 0 env) (map fst os)

2317+ (impsfst, _) <- get

2318+ put (nub imps \\ nub impsfst, fns)

2266− ni 0 env (PIfThenElse _ c t f) = concatMap (ni 0 env) [c, t, f]

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

2267− ni 0 env (PLam fc n _ ty sc) = ni 0 env ty ++ ni 0 (n:env) sc

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

2268− ni 0 env (PPi p n _ ty sc) = ni 0 env ty ++ ni 0 (n:env) sc

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

2269− ni 0 env (PRewrite _ l r _) = ni 0 env l ++ ni 0 env r

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

2270− ni 0 env (PTyped l r) = ni 0 env l ++ ni 0 env r

2323+ ni 0 env (PTyped l r) = do ni 0 env l; ni 0 env r

2271− ni 0 env (PPair _ _ _ l r) = ni 0 env l ++ ni 0 env r

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

2272− ni 0 env (PDPair _ _ _ (PRef _ _ n) t r) = ni 0 env t ++ ni 0 (n:env) r

2325+ ni 0 env (PDPair _ _ _ (PRef _ _ n) t r) = do ni 0 env t; ni 0 (n:env) r

2273− ni 0 env (PDPair _ _ _ l t r) = ni 0 env l ++ ni 0 env t ++ ni 0 env r

2326+ ni 0 env (PDPair _ _ _ l t r) = do ni 0 env l

2327+ ni 0 env t

2328+ ni 0 env r

2274− ni 0 env (PAlternative ns a as) = concatMap (ni 0 env) as

2329+ ni 0 env (PAlternative ns a as) = mapM_ (ni 0 env) as

2275 ni 0 env (PHidden tm) = ni 0 env tm

2330 ni 0 env (PHidden tm) = ni 0 env tm

2276 ni 0 env (PUnifyLog tm) = ni 0 env tm

2331 ni 0 env (PUnifyLog tm) = ni 0 env tm

2277 ni 0 env (PDisamb _ tm) = ni 0 env tm

2332 ni 0 env (PDisamb _ tm) = ni 0 env tm

2278 ni 0 env (PNoImplicits tm) = ni 0 env tm

2333 ni 0 env (PNoImplicits tm) = ni 0 env tm

2279

2334

2280− ni i env (PQuasiquote tm ty) = ni (i + 1) env tm ++

2335+ ni i env (PQuasiquote tm ty) = do ni (i + 1) env tm

2281− maybe [] (ni i env) ty

2336+ maybe (return ()) (ni i env) ty

2282 ni i env (PUnquote tm) = ni (i - 1) env tm

2337 ni i env (PUnquote tm) = ni (i - 1) env tm

2283

2338

2284− ni i env tm = concatMap (ni i env) (children tm)

2339+ ni i env tm = mapM_ (ni i env) (children tm)

2285

2340

2286-- Return names which are free in the given term.

2341-- Return names which are free in the given term.

2287namesIn :: [(Name, PTerm)] -> IState -> PTerm -> [Name]

2342namesIn :: [(Name, PTerm)] -> IState -> PTerm -> [Name]

src/Idris/CmdOptions.hs+2

@@ -148,6 +148,8 @@ parseFlags = many $

148

149 <|> (UseConsoleWidth <$> option (str >>= parseConsoleWidth) (long "consolewidth" <> metavar "WIDTH" <> help "Select console width: auto, infinite, nat"))

150 <|> flag' DumpHighlights (long "highlight" <> help "Emit source code highlighting")

151+ <|> flag' NoElimDeprecationWarnings (long "no-elim-deprecation-warnings" <> help "Disable deprecation warnings for %elim")

152+ <|> flag' NoOldTacticDeprecationWarnings (long "no-tactic-deprecation-warnings" <> help "Disable deprecation warnings for the old tactic sublanguage")

151

153

152 where

154 where

153 getExt s = case maybeRead s of

155 getExt s = case maybeRead s of

src/Idris/Core/Elaborate.hs+2−1

@@ -502,9 +502,10 @@ matchProblems all = processTactic' (MatchProblems all)

502unifyProblems :: Elab' aux ()

503unifyProblems = processTactic' UnifyProblems

504

505−defer :: [Name] -> Name -> Elab' aux ()

505+defer :: [Name] -> Name -> Elab' aux Name

506defer ds n = do n' <- unique_hole n

507 processTactic' (Defer ds n')

508+ return n'

508

509

509deferType :: Name -> Raw -> [Name] -> Elab' aux ()

510deferType :: Name -> Raw -> [Name] -> Elab' aux ()

510deferType n ty ns = processTactic' (DeferType n ty ns)

511deferType n ty ns = processTactic' (DeferType n ty ns)

src/Idris/Core/ProofState.hs+8−7

@@ -429,7 +429,8 @@ defer :: [Name] -> Name -> RunTactic

429defer dropped n ctxt env (Bind x (Hole t) (P nt x' ty)) | x == x' =

430 do let env' = filter (\(n, t) -> n `notElem` dropped) env

431 action (\ps -> let hs = holes ps in

432+ ps { usedns = n : usedns ps,

432− ps { holes = hs \\ [x] })

433+ holes = hs \\ [x] })

433 ps <- get

434 ps <- get

434 return (Bind n (GHole (length env') (psnames ps) (mkTy (reverse env') t))

435 return (Bind n (GHole (length env') (psnames ps) (mkTy (reverse env') t))

435 (mkApp (P Ref n ty) (map getP (reverse env'))))

436 (mkApp (P Ref n ty) (map getP (reverse env'))))

@@ -620,19 +621,19 @@ introTy ty n ctxt env _ = fail "Can't introduce here."

620

621

621intro :: Maybe Name -> RunTactic

622intro :: Maybe Name -> RunTactic

622intro mn ctxt env (Bind x (Hole t) (P _ x' _)) | x == x' =

623intro mn ctxt env (Bind x (Hole t) (P _ x' _)) | x == x' =

623− do let n = case mn of

624− Just name -> name

625− Nothing -> x

626− let t' = case t of

624+ do let t' = case t of

627 x@(Bind y (Pi _ s _) _) -> x

625 x@(Bind y (Pi _ s _) _) -> x

628 _ -> hnf ctxt env t

626 _ -> hnf ctxt env t

629 case t' of

627 case t' of

630 Bind y (Pi _ s _) t ->

628 Bind y (Pi _ s _) t ->

629+ let n = case mn of

630+ Just name -> name

631+ Nothing -> y

631 -- It's important that this be subst and not updsubst,

632 -- It's important that this be subst and not updsubst,

632 -- because we want to substitute even in portions of

633 -- because we want to substitute even in portions of

633 -- terms that we know do not contain holes.

634 -- terms that we know do not contain holes.

634− let t' = subst y (P Bound n s) t in

635+ t' = subst y (P Bound n s) t

635− return $ Bind n (Lam s) (Bind x (Hole t') (P Bound x t'))

636+ in return $ Bind n (Lam s) (Bind x (Hole t') (P Bound x t'))

636 _ -> lift $ tfail $ CantIntroduce t'

637 _ -> lift $ tfail $ CantIntroduce t'

637intro n ctxt env _ = fail "Can't introduce here."

638intro n ctxt env _ = fail "Can't introduce here."

638

639

src/Idris/DeepSeq.hs+3−1

@@ -162,7 +162,9 @@ instance NFData Opt where

162 rnf (AutoWidth) = ()

163 rnf (AutoSolve) = ()

164 rnf (UseConsoleWidth cw) = rnf cw `seq` ()

165− rnf (DumpHighlights) = ()

165+ rnf DumpHighlights = ()

166+ rnf NoElimDeprecationWarnings = ()

167+ rnf NoOldTacticDeprecationWarnings = ()

166

168

167

169

168instance NFData TIData where

170instance NFData TIData where

src/Idris/Elab/Term.hs+12−7

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

611 [] -> False

612 _ -> True

613 bindable (NS _ _) = False

614− bindable (UN xs) = True

615 bindable n = implicitable n

614 bindable n = implicitable n

616 elab' ina _ f@(PInferRef fc hls n) = elab' ina (Just fc) (PApp NoFC f [])

615 elab' ina _ f@(PInferRef fc hls n) = elab' ina (Just fc) (PApp NoFC f [])

617 elab' ina fc' tm@(PRef fc hls n)

616 elab' ina fc' tm@(PRef fc hls n)

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

981 let n' = metavarName (namespace info) n

980 let n' = metavarName (namespace info) n

982 attack

981 attack

983 psns <- getPSnames

982 psns <- getPSnames

984− defer unique_used n'

983+ n' <- defer unique_used n'

985 solve

984 solve

986 highlightSource nfc (AnnName n' (Just MetavarOutput) Nothing Nothing)

985 highlightSource nfc (AnnName n' (Just MetavarOutput) Nothing Nothing)

987 elab' ina fc (PProof ts) = do compute; mapM_ (runTac True ist (elabFC info) fn) ts

986 elab' ina fc (PProof ts) = do compute; mapM_ (runTac True ist (elabFC info) fn) ts

@@ -1057,10 +1056,9 @@ elab ist info emode opts fn tm

1057

1056

1058 let args' = filter (\(n, _) -> n `notElem` argsDropped) args

1057 let args' = filter (\(n, _) -> n `notElem` argsDropped) args

1059

1058

1059+ attack

1060− cname <- unique_hole' True (mkCaseName fn)

1060+ cname' <- defer argsDropped (mkN (mkCaseName fn))

1061− let cname' = mkN cname

1061+ solve

1062−-- elab' ina fc (PMetavar cname')

1063− attack; defer argsDropped cname'; solve

1064

1062

1065 -- if the scrutinee is one of the 'args' in env, we should

1063 -- if the scrutinee is one of the 'args' in env, we should

1066 -- inspect it directly, rather than adding it as a new argument

1064 -- inspect it directly, rather than adding it as a new argument

@@ -1623,7 +1621,7 @@ findHighlight n = do ctxt <- get_context

1623 Nothing -> case lookupTyExact n ctxt of

1621 Nothing -> case lookupTyExact n ctxt of

1624 Just _ -> return $ AnnName n Nothing Nothing Nothing

1622 Just _ -> return $ AnnName n Nothing Nothing Nothing

1625 Nothing -> lift . tfail . InternalMsg $

1623 Nothing -> lift . tfail . InternalMsg $

1626− "Can't find name" ++ show n

1624+ "Can't find name " ++ show n

1627

1625

1628-- Try again to solve auto implicits

1626-- Try again to solve auto implicits

1629solveAuto :: IState -> Name -> Bool -> (Name, [FailContext]) -> ElabD ()

1627solveAuto :: IState -> Name -> Bool -> (Name, [FailContext]) -> ElabD ()

@@ -1963,6 +1961,13 @@ runElabAction ist fc env tm ns = do tm' <- eval tm

1963 = do tm' <- reifyTT tm

1961 = do tm' <- reifyTT tm

1964 ctxt <- get_context

1962 ctxt <- get_context

1965 fmap fst . checkClosed . reflect $ whnf ctxt tm'

1963 fmap fst . checkClosed . reflect $ whnf ctxt tm'

1964+ | n == tacN "prim__Converts", [env, tm1, tm2] <- args

1965+ = do env' <- reifyEnv env

1966+ tm1' <- reifyTT tm1

1967+ tm2' <- reifyTT tm2

1968+ ctxt <- get_context

1969+ lift $ converts ctxt env' tm1' tm2'

1970+ returnUnit

1966 | n == tacN "prim__DeclareType", [decl] <- args

1971 | n == tacN "prim__DeclareType", [decl] <- args

1967 = do (RDeclare n args res) <- reifyTyDecl decl

1972 = do (RDeclare n args res) <- reifyTyDecl decl

1968 ctxt <- get_context

1973 ctxt <- get_context

src/Idris/ParseData.hs+12−2

@@ -157,11 +157,21 @@ DefaultEliminator ::= 'noelim'?

157 -}

158dataOpts :: DataOpts -> IdrisParser DataOpts

159dataOpts opts

160+ = do fc <- reservedFC "%elim"

161+ warnElim fc

160− = do reserved "%elim"; dataOpts (DefaultEliminator : DefaultCaseFun : opts)

162+ dataOpts (DefaultEliminator : DefaultCaseFun : opts)

163+ <|> do fc <- reservedFC "%case"

164+ warnElim fc

161− <|> do reserved "%case"; dataOpts (DefaultCaseFun : opts)

165+ dataOpts (DefaultCaseFun : opts)

162 <|> do reserved "%error_reverse"; dataOpts (DataErrRev : opts)

166 <|> do reserved "%error_reverse"; dataOpts (DataErrRev : opts)

163 <|> return opts

167 <|> return opts

164 <?> "data options"

168 <?> "data options"

169+ where warnElim fc =

170+ do ist <- get

171+ let cmdline = opt_cmdline (idris_options ist)

172+ unless (NoElimDeprecationWarnings `elem` cmdline) $

173+ put ist { parserWarnings =

174+ (fc, Msg "Eliminator generation is deprecated. Use an eliminator generator in a library instead.") : parserWarnings ist }

165

175

166{- | Parses a data type declaration

176{- | Parses a data type declaration

167Data ::= DocComment? Accessibility? DataI DefaultEliminator FnName TypeSig ExplicitTypeDataRest?

177Data ::= DocComment? Accessibility? DataI DefaultEliminator FnName TypeSig ExplicitTypeDataRest?

src/Idris/ParseExpr.hs+10

@@ -331,6 +331,14 @@ caseOption syn = do lhs <- expr (syn { inPattern = True })

331 return (lhs, r)

332 <?> "case option"

333

334+warnTacticDeprecation :: FC -> IdrisParser ()

335+warnTacticDeprecation fc =

336+ do ist <- get

337+ let cmdline = opt_cmdline (idris_options ist)

338+ unless (NoOldTacticDeprecationWarnings `elem` cmdline) $

339+ put ist { parserWarnings =

340+ (fc, Msg "This style of tactic proof is deprecated. See %runElab for the replacement.") : parserWarnings ist }

341+

334{- | Parses a proof block

342{- | Parses a proof block

335@

343@

336ProofExpr ::=

344ProofExpr ::=

@@ -342,6 +350,7 @@ proofExpr :: SyntaxInfo -> IdrisParser PTerm

342proofExpr syn = do kw <- reservedFC "proof"

350proofExpr syn = do kw <- reservedFC "proof"

343 ts <- indentedBlock1 (tactic syn)

351 ts <- indentedBlock1 (tactic syn)

344 highlightP kw AnnKeyword

352 highlightP kw AnnKeyword

353+ warnTacticDeprecation kw

345 return $ PProof ts

354 return $ PProof ts

346 <?> "proof block"

355 <?> "proof block"

347

356

@@ -356,6 +365,7 @@ tacticsExpr :: SyntaxInfo -> IdrisParser PTerm

356tacticsExpr syn = do kw <- reservedFC "tactics"

365tacticsExpr syn = do kw <- reservedFC "tactics"

357 ts <- indentedBlock1 (tactic syn)

366 ts <- indentedBlock1 (tactic syn)

358 highlightP kw AnnKeyword

367 highlightP kw AnnKeyword

368+ warnTacticDeprecation kw

359 return $ PTactics ts

369 return $ PTactics ts

360 <?> "tactics block"

370 <?> "tactics block"

361

371

src/Idris/ParseHelpers.hs+2−1

@@ -100,7 +100,8 @@ reportParserWarnings = do ist <- getIState

100 mapM_ (uncurry iWarn)

101 (map (\ (fc, err) -> (fc, pprintErr ist err)) .

102 reverse .

103− nub $

103+ nubBy (\(fc, err) (fc', err') ->

104+ FC' fc == FC' fc' && err == err') $

104 parserWarnings ist)

105 parserWarnings ist)

105 clearParserWarnings

106 clearParserWarnings

106

107

src/Idris/Prover.hs+24−20

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

1+

1{-# LANGUAGE PatternGuards #-}

2{-# LANGUAGE PatternGuards #-}

2module Idris.Prover (prover, showProof, showRunElab) where

3module Idris.Prover (prover, showProof, showRunElab) where

3

4

@@ -5,7 +6,7 @@ module Idris.Prover (prover, showProof, showRunElab) where

5-- This exludes (<$>) as fmap, because wl-pprint uses it for newline

6-- This exludes (<$>) as fmap, because wl-pprint uses it for newline

6import Prelude (Eq(..), Show(..),

7import Prelude (Eq(..), Show(..),

7 Bool(..), Either(..), Maybe(..), String,

8 Bool(..), Either(..), Maybe(..), String,

8− (.), ($), (++), (||),

9+ (.), ($), (++), (||), (&&),

9 concatMap, id, elem, error, fst, flip, foldl, foldr, init,

10 concatMap, id, elem, error, fst, flip, foldl, foldr, init,

10 length, lines, map, not, null, repeat, reverse, tail, zip)

11 length, lines, map, not, null, repeat, reverse, tail, zip)

11

12

@@ -89,7 +90,10 @@ prove mode opt ctxt lit n ty

89 (tm, prf) <-

90 (tm, prf) <-

90 if mode

91 if mode

91 then elabloop n True ("-" ++ show n) [] (ES (ps, initEState) "" Nothing) [] Nothing []

92 then elabloop n True ("-" ++ show n) [] (ES (ps, initEState) "" Nothing) [] Nothing []

93+ else do iputStrLn $ "Warning: this interactive prover is deprecated and will be removed " ++

94+ "in a future release. Please see :elab for a similar feature that "++

95+ "will replace it."

92− else ploop n True ("-" ++ show n) [] (ES (ps, initEState) "" Nothing) Nothing

96+ ploop n True ("-" ++ show n) [] (ES (ps, initEState) "" Nothing) Nothing

93 logLvl 1 $ "Adding " ++ show tm

97 logLvl 1 $ "Adding " ++ show tm

94 i <- getIState

98 i <- getIState

95 let shower = if mode

99 let shower = if mode

@@ -145,16 +149,16 @@ elabStep st e =

145 return (res, ctxt)

149 return (res, ctxt)

146 ((_,_,_,_,e,_,_):_) -> lift $ Error e

150 ((_,_,_,_,e,_,_):_) -> lift $ Error e

147

151

148−dumpState :: IState -> [(Name, Type, Term)] -> ProofState -> Idris ()

152+dumpState :: IState -> Bool -> [(Name, Type, Term)] -> ProofState -> Idris ()

149−dumpState ist menv ps | [] <- holes ps =

153+dumpState ist inElab menv ps | [] <- holes ps =

150 do let nm = thname ps

154 do let nm = thname ps

151 rendered <- iRender $ prettyName True False [] nm <> colon <+> text "No more goals."

155 rendered <- iRender $ prettyName True False [] nm <> colon <+> text "No more goals."

152 iputGoal rendered

156 iputGoal rendered

153−dumpState ist menv ps | (h : hs) <- holes ps = do

157+dumpState ist inElab menv ps | (h : hs) <- holes ps = do

154 let OK ty = goalAtFocus ps

158 let OK ty = goalAtFocus ps

155 let OK env = envAtFocus ps

159 let OK env = envAtFocus ps

156 let state = prettyOtherGoals hs <> line <>

160 let state = prettyOtherGoals hs <> line <>

157− prettyAssumptions ty env <> line <>

161+ prettyAssumptions inElab ty env <> line <>

158 prettyMetaValues (reverse menv) <>

162 prettyMetaValues (reverse menv) <>

159 prettyGoal (zip (assumptionNames env) (repeat False)) ty

163 prettyGoal (zip (assumptionNames env) (repeat False)) ty

160 rendered <- iRender state

164 rendered <- iRender state

@@ -172,18 +176,18 @@ dumpState ist menv ps | (h : hs) <- holes ps = do

172 assumptionNames :: Env -> [Name]

176 assumptionNames :: Env -> [Name]

173 assumptionNames = map fst

177 assumptionNames = map fst

174

178

175− prettyPs :: Binder Type -> [(Name, Bool)] -> Env -> Doc OutputAnnotation

179+ prettyPs :: Bool -> Binder Type -> [(Name, Bool)] -> Env -> Doc OutputAnnotation

176− prettyPs g bnd [] = empty

180+ prettyPs all g bnd [] = empty

177− prettyPs g bnd ((n@(MN _ r), _) : bs)

181+ prettyPs all g bnd ((n@(MN _ r), _) : bs)

178− | r == txt "rewrite_rule" = prettyPs g ((n, False):bnd) bs

182+ | not all && r == txt "rewrite_rule" = prettyPs all g ((n, False):bnd) bs

179− prettyPs g bnd ((n@(MN _ _), _) : bs)

183+ prettyPs all g bnd ((n@(MN _ _), _) : bs)

180− | not (n `elem` freeEnvNames bs || n `elem` goalNames g) = prettyPs g bnd bs

184+ | not (all || n `elem` freeEnvNames bs || n `elem` goalNames g) = prettyPs all g bnd bs

181− prettyPs g bnd ((n, Let t v) : bs) =

185+ prettyPs all g bnd ((n, Let t v) : bs) =

182 line <> bindingOf n False <+> text "=" <+> tPretty bnd v <+> colon <+>

186 line <> bindingOf n False <+> text "=" <+> tPretty bnd v <+> colon <+>

183− align (tPretty bnd t) <> prettyPs g ((n, False):bnd) bs

187+ align (tPretty bnd t) <> prettyPs all g ((n, False):bnd) bs

184− prettyPs g bnd ((n, b) : bs) =

188+ prettyPs all g bnd ((n, b) : bs) =

185 line <> bindingOf n False <+> colon <+>

189 line <> bindingOf n False <+> colon <+>

186− align (tPretty bnd (binderTy b)) <> prettyPs g ((n, False):bnd) bs

190+ align (tPretty bnd (binderTy b)) <> prettyPs all g ((n, False):bnd) bs

187

191

188 prettyMetaValues [] = empty

192 prettyMetaValues [] = empty

189 prettyMetaValues mvs =

193 prettyMetaValues mvs =

@@ -210,12 +214,12 @@ dumpState ist menv ps | (h : hs) <- holes ps = do

210 text "---------- Goal: ----------" <$$>

214 text "---------- Goal: ----------" <$$>

211 bindingOf h False <+> colon <+> align (prettyG bnd ty)

215 bindingOf h False <+> colon <+> align (prettyG bnd ty)

212

216

213− prettyAssumptions g env =

217+ prettyAssumptions inElab g env =

214 if length env == 0 then

218 if length env == 0 then

215 empty

219 empty

216 else

220 else

217 text "---------- Assumptions: ----------" <>

221 text "---------- Assumptions: ----------" <>

218− nest nestingSize (prettyPs g [] $ reverse env)

222+ nest nestingSize (prettyPs inElab g [] $ reverse env)

219

223

220 prettyOtherGoals hs =

224 prettyOtherGoals hs =

221 if length hs == 0 then

225 if length hs == 0 then

@@ -273,7 +277,7 @@ undoElab prf env st (h:hs) = do (prf', env', st') <- undoStep prf env st h

273elabloop :: Name -> Bool -> String -> [String] -> ElabState EState -> [ElabShellHistory] -> Maybe History -> [(Name, Type, Term)] -> Idris (Term, [String])

277elabloop :: Name -> Bool -> String -> [String] -> ElabState EState -> [ElabShellHistory] -> Maybe History -> [(Name, Type, Term)] -> Idris (Term, [String])

274elabloop fn d prompt prf e prev h env

278elabloop fn d prompt prf e prev h env

275 = do ist <- getIState

279 = do ist <- getIState

276− when d $ dumpState ist env (proof e)

280+ when d $ dumpState ist True env (proof e)

277 (x, h') <-

281 (x, h') <-

278 case idris_outputmode ist of

282 case idris_outputmode ist of

279 RawOutput _ ->

283 RawOutput _ ->

@@ -390,7 +394,7 @@ ploop :: Name -> Bool -> String -> [String] -> ElabState EState -> Maybe History

390ploop fn d prompt prf e h

394ploop fn d prompt prf e h

391 = do i <- getIState

395 = do i <- getIState

392 let autoSolve = opt_autoSolve (idris_options i)

396 let autoSolve = opt_autoSolve (idris_options i)

393− when d $ dumpState i [] (proof e)

397+ when d $ dumpState i False [] (proof e)

394 (x, h') <-

398 (x, h') <-

395 case idris_outputmode i of

399 case idris_outputmode i of

396 RawOutput _ ->

400 RawOutput _ ->

test/basic002/expected+4

@@ -1 +1,5 @@

1+test006.idr:25:23-28:

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

3+test006.idr:32:23-28:

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

1[False, True, False, True, False, True]

5[False, True, False, True, False, True]

test/basic002/run+1−1

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

1#!/usr/bin/env bash

2−idris $@ test006.idr -o test006

2+idris $@ --nocolour --consolewidth 80 test006.idr -o test006

3./test006

4rm -f test006 test006.ibc

test/basic009/expected+11−2

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

1MAIN-PASS

2−Faulty.idr:6:7:When checking type of Faulty.fault:

2+Faulty.idr:7:7:When checking right hand side of fault:

3−Can't disambiguate name: A.num, B.C.num

3+Type mismatch between

4+ 0 = 0 (Type of Refl)

5+and

6+ num = 0 (Expected type)

7+

8+Specifically:

9+ Type mismatch between

10+ 0

11+ and

12+ num

4Multiple.idr:3:1:import alias not unique: "X"

13Multiple.idr:3:1:import alias not unique: "X"

test/basic015/basic015.idrnew file+73

@@ -0,0 +1,73 @@

1+{-

2+data Nat = Z | S Nat

3+

4+plus : Nat -> Nat -> Nat

5+plus Z y = y

6+plus (S x) y = S (plus x y)

7+-}

8+

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

10+ Nil : Vect Z a

11+ (::) : a -> Vect k a -> Vect (S k) a

12+

13+%name Vect xs, ys, zs

14+

15+append : Vect n a -> Vect m a -> Vect (n + m) a

16+append [] ys = ys

17+append (x :: xs) ys = x :: append xs ys

18+

19+

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

21+zipWith f [] ys = []

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

23+

24+create_empties : Vect m (Vect 0 elem)

25+create_empties {m = Z} = []

26+create_empties {m = (S k)} = [] :: create_empties

27+

28+transpose_helper : (row : Vect m elem) -> (rest_trans : Vect m (Vect k elem)) ->

29+ Vect m (Vect (S k) elem)

30+transpose_helper [] [] = []

31+transpose_helper (rowval :: xs) (restrow :: ys) = (rowval :: restrow) :: transpose_helper xs ys

32+

33+transpose_vec : Vect n (Vect m elem) -> Vect m (Vect n elem)

34+transpose_vec [] = create_empties

35+transpose_vec (row :: rest) = let rest_trans = transpose_vec rest in

36+ transpose_helper row rest_trans

37+

38+

39+

40+

41+

42+

43+

44+

45+------- A main program to read dimensions, generate and tranpose a vector

46+

47+instance Functor (Vect m) where

48+ map m [] = []

49+ map m (x :: xs) = m x :: map m xs

50+

51+instance Show a => Show (Vect m a) where

52+ show x = show (toList x)

53+ where

54+ toList : Vect m a -> List a

55+ toList [] = []

56+ toList (y :: xs) = y :: toList xs

57+

58+countTo : (m : Nat) -> Vect m Int

59+countTo Z = []

60+countTo (S k) = 0 :: map (+1) (countTo k)

61+

62+mkVect : (n, m : Nat) -> Vect n (Vect m Int)

63+mkVect Z m = []

64+mkVect (S k) m = countTo m :: map (map (+ cast m)) (mkVect k m)

65+

66+main : IO ()

67+main = do putStr "Rows: "

68+ let r : Nat = 5

69+ putStr "Columns: "

70+ let c : Nat = 6

71+ printLn (mkVect r c)

72+ putStrLn "Transposed:"

73+ printLn (transpose_vec (mkVect r c))

test/basic015/expectednew file+3

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

1+Rows: Columns: [[0, 1, 2, 3, 4, 5], [6, 7, 8, 9, 10, 11], [12, 13, 14, 15, 16, 17], [18, 19, 20, 21, 22, 23], [24, 25, 26, 27, 28, 29]]

2+Transposed:

3+[[0, 6, 12, 18, 24], [1, 7, 13, 19, 25], [2, 8, 14, 20, 26], [3, 9, 15, 21, 27], [4, 10, 16, 22, 28], [5, 11, 17, 23, 29]]

test/basic015/runnew file+4

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

1+#!/usr/bin/env bash

2+idris $@ basic015.idr -o basic015

3+./basic015

4+rm -f basic015 *.ibc

test/classes001/ClassName.idr+1−1

@@ -21,7 +21,7 @@ badShow = MkMyShow (const "hej")

21test1 : twiceAString 2 = "22"

22test1 = Refl

23

24−test2 : twiceAString @{badShow} 2 = "hejhej"

24+test2 : twiceAString @{ClassName.badShow} 2 = "hejhej"

25test2 = Refl

26

27

test/docs003/expected+1

@@ -15,6 +15,7 @@ Instances:

15 Functor Stream

16 Functor Provider

17 Functor Binder

18+ Functor Elab

18 Functor PrimIO

19 Functor PrimIO

19 Functor Maybe

20 Functor Maybe

20 Functor (Either e)

21 Functor (Either e)

test/dsl003/DSLPi.idr+1−1

@@ -43,5 +43,5 @@ test2 = specs ((x, y : INT) -> x === y)

43test3 : Spec []

44test3 = ForAll INT . ForAll INT . ItHolds $ Var (FS FZ) === Var FZ

45

46−test4 : test2 = test3

46+test4 : DSLPi.test2 = DSLPi.test3

47test4 = Refl

test/effects003/expected+2

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

1+hangman.idr:204:8-13:

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

1------------

3------------

2

4

36 guesses left

56 guesses left

test/effects003/hangman.idr+4

@@ -223,3 +223,7 @@ were caught by the type checker:

223

224main : IO ()

225main = run runGame

226+

227+-- Local Variables:

228+-- idris-load-packages: ("effects")

229+-- End:

test/effects003/run+1−1

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

1#!/usr/bin/env bash

2−idris $@ hangman.idr -p effects -o hangman

2+idris $@ hangman.idr --consolewidth 80 --nocolour -p effects -o hangman

3./hangman < input

4rm -f hangman *.ibc

test/error003/expected+1−1

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

1ErrorReflection.idr:68:5:When checking right hand side of bad:

2−DSL type error: (t(503) => t'(504)) doesn't match ()

2+DSL type error: (t(504) => t'(503)) doesn't match ()

test/primitives001/substring.idr+5−5

@@ -13,19 +13,19 @@ foo = "Hello! here's the thing"

13firstSentence : String

14firstSentence = "Idris 是一个通用的依赖类型纯函数式编程语言，其类型系统与 Agda 以及 Epigram 相似。"

15

16−emptyTest : prim__strSubstr 100000 14 firstSentence = ""

16+emptyTest : prim__strSubstr 100000 14 Main.firstSentence = ""

17emptyTest = Refl

18

19−multiTest : prim__strSubstr 10 5 firstSentence = "用的依赖类"

19+multiTest : prim__strSubstr 10 5 Main.firstSentence = "用的依赖类"

20multiTest = Refl

21

22−negative : prim__strSubstr (-10) 5 firstSentence = "Idris"

22+negative : prim__strSubstr (-10) 5 Main.firstSentence = "Idris"

23negative = Refl

24

25−negativeEnd : prim__strSubstr 0 (-1) firstSentence = ""

25+negativeEnd : prim__strSubstr 0 (-1) Main.firstSentence = ""

26negativeEnd = Refl

27

28−negativeLength : prim__strSubstr 4 (-4) firstSentence = ""

28+negativeLength : prim__strSubstr 4 (-4) Main.firstSentence = ""

29negativeLength = Refl

30

31main : IO ()

test/proof001/expected+4

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

1+test029.idr:29:25-30:

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

3+test029.idr:36:25-30:

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

test/proof001/run+1−1

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

1#!/usr/bin/env bash

2−idris $@ test029.idr --check test029

2+idris $@ test029.idr --consolewidth 80 --nocolour --check test029

3rm -f *.ibc

test/proof002/expected+6

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

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

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

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

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

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

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

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

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

2When checking right hand side of testReflect1:

8When checking right hand side of testReflect1:

3When checking an application of function Reflect.getJust:

9When checking an application of function Reflect.getJust:

test/proof003/run+1−1

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

1#!/usr/bin/env bash

2−idris $@ test015.idr -o test015

2+idris $@ test015.idr --nocolour --consolewidth 80 --no-tactic-deprecation-warnings -o test015

3./test015

4rm -f test015 Parity.ibc test015.ibc

test/proof003/test015.idr+1−1

@@ -106,7 +106,7 @@ Main.ntbEven = proof {

106-- There is almost certainly an easier proof. I don't care, for now :)

107

108Main.adc_lemma_2 = proof {

109− intro w,v,num0,v1,num1,x,bx,x1,bx1,bit0,b0,bit1,b1,c,bc

109+ intro v,w,num0,v1,num1,x,bx,x1,bx1,bit0,b0,bit1,b1,c,bc

110 rewrite sym (plusZeroRightNeutral x);

111 rewrite sym (plusZeroRightNeutral v1);

112 rewrite sym (plusZeroRightNeutral (plus (plus x v) v1));

test/proof008/expected+2

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

1+ClaimAndUnfocus.idr:8:27-32:

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

test/proof008/run+1−1

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

1#!/usr/bin/env bash

2−idris --check $@ ClaimAndUnfocus.idr

2+idris --nocolour --consolewidth 80 --check $@ ClaimAndUnfocus.idr

3rm -f *.ibc

test/proof009/expected+1

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

1+Warning: this interactive prover is deprecated and will be removed in a future release. Please see :elab for a similar feature that will replace it.

1

2

3

3---------- Goal: ----------

4---------- Goal: ----------

test/proofsearch001/proofsearch001.idr+1−1

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

1%default total

2

3class C a (f : Bool -> Bool) | a where {}

4−instance C Int not where {}

4+instance C Int Bool.not where {}

5

6foo : C Int g => {auto pf : g True = False} -> Unit

7foo = ()

test/pruviloj001/expectednew file

No changes to the content.

test/pruviloj001/pruviloj001.idrnew file+77

@@ -0,0 +1,77 @@

1+-- Demonstrate that partial tactics can produce total programs and

2+-- that the basic parts of Pruviloj are doing what they should.

3+

4+import Pruviloj

5+import Pruviloj.Induction

6+

7+%default total

8+

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

10+||| solve the goal

11+partial

12+auto : Elab ()

13+auto = do compute

14+ attack

15+ try $ repeatUntilFail intro'

16+ hs <- map fst <$> getEnv

17+ for_ hs $

18+ \ih => try (rewriteWith (Var ih))

19+ hypothesis <|> search

20+ solve

21+

22+

23+||| ; in Coq (roughly)

24+andThen : Elab (List TTName) -> Elab a -> Elab ()

25+andThen tac1 tac2 =

26+ do hs <- tac1

27+ for_ hs $ \h =>

28+ inHole h $ ignore tac2

29+

30+||| Common pattern of proofs by induction.

31+partial

32+mush : Elab ()

33+mush =

34+ do n <- gensym "j"

35+ intro n

36+ try intros

37+ induction (Var n) `andThen` auto

38+

39+plusAssoc : (j, k, l : Nat) -> plus (plus j k) l = plus j (plus k l)

40+plusAssoc = %runElab mush

41+

42+plusZeroR : (k : Nat) -> plus k Z = k

43+plusZeroR = %runElab mush

44+

45+plusSRightS : (left : Nat) -> (right : Nat) -> S (left + right) = left + (S right)

46+plusSRightS = %runElab mush

47+

48+multOneLNeutral : (right : Nat) -> 1 * right = right

49+multOneLNeutral = %runElab mush

50+

51+multOneRNeutral : (left : Nat) -> left * 1 = left

52+multOneRNeutral = %runElab mush

53+

54+plusMinusLeftCancel : (left : Nat) -> (right : Nat) -> (right' : Nat) ->

55+ minus (left + right) (left + right') = minus right right'

56+plusMinusLeftCancel = %runElab mush

57+

58+powerOneNeutral : (base : Nat) -> power base 1 = base

59+powerOneNeutral = %runElab mush

60+

61+-- this silly tactic is controllable by introducing the non-inductive arg first

62+mapPreservesLen : (f : a -> b) -> (l : List a) ->

63+ length (map f l) = length l

64+mapPreservesLen f = %runElab mush

65+

66+lenAppend : (left : List a) -> (right : List a) ->

67+ length (left ++ right) = length left + length right

68+lenAppend = %runElab mush

69+

70+appendNilRightId : (l : List a) ->

71+ l ++ [] = l

72+appendNilRightId = %runElab mush

73+

74+-- Local Variables:

75+-- idris-load-packages: ("pruviloj")

76+-- End:

77+

test/pruviloj001/runnew file+3

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

1+#!/usr/bin/env bash

2+idris $@ -p pruviloj --check --nocolour --consolewidth 70 pruviloj001.idr

3+rm -f *.ibc

test/quasiquote004/expected+6

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

1+Quasiquote004.idr:39:26-31:

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

3+Quasiquote004.idr:42:28-33:

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

5+Quasiquote004.idr:50:27-32:

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

1Quasiquote004.idr:50:25:

7Quasiquote004.idr:50:25:

2When checking right hand side of Quasiquote004.getMeNat':

8When checking right hand side of Quasiquote004.getMeNat':

3Not a Nat goal

9Not a Nat goal

test/quasiquote006/quasiquote006.idr+2−2

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

2a : TTName

3a = `{Nat}

4

5−aOK : a = NS (UN "Nat") ["Nat", "Prelude"]

5+aOK : Main.a = NS (UN "Nat") ["Nat", "Prelude"]

6aOK = Refl

7

8b : TTName

@@ -17,5 +17,5 @@ d = `{(::)}

17d : TTName

18d = `{List.(::)}

19

20−dOK : d = NS (UN "::") ["List", "Prelude"]

20+dOK : Main.d = NS (UN "::") ["List", "Prelude"]

21dOK = Refl

test/reg001/reg001.idr+1−1

@@ -7,7 +7,7 @@ import Data.Fin

7import Control.Isomorphism

8

9class Functor f => VerifiedFunctor (f : Type -> Type) where

10− identity : (fa : f a) -> map id fa = fa

10+ identity : (fa : f a) -> map Basics.id fa = fa

11

12data Imp : Type where

13 MkImp : {any : Type} -> any -> Imp

test/reg017/expected+4

@@ -1 +1,5 @@

1+reg017.idr:5:17-24:

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

3+reg017.idr:8:17-24:

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

14

54

test/reg017/run+1−1

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

1#!/usr/bin/env bash

2−idris $@ reg017.idr -o reg017

2+idris $@ --nocolour --consolewidth 80 reg017.idr -o reg017

3./reg017

4rm -f reg017 *.ibc

test/reg028/expected+2

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

1reg028.idr:5:1:

2tbad.bad is possibly not total due to: with block in tbad.bad

3+reg028a.idr:17:14-19:

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

3reg028a.idr:11:1:

5reg028a.idr:11:1:

4tbad.qsort' is possibly not total due to: with block in tbad.qsort'

6tbad.qsort' is possibly not total due to: with block in tbad.qsort'

test/reg041/ott.idr+1−1

@@ -37,6 +37,6 @@ EQ two False two False = one

37EQ (pi s t) f (pi s' t') g = pi s $ \x => pi s' $ \y => EQ s x s' y ~> EQ (t x) (f x) (t' y) (g y)

38EQ _ _ _ _ = zero

39

40−example : <| (id == id in (two ~> two)) |>

40+example : <| (Basics.id == Basics.id in (OTT.two ~> OTT.two)) |>

41example = ?prf

42

test/reg044/expected+2

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

1+reg044.idr:4:6-11:

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

1reg044.idr:4:4:When checking right hand side of Main.pf:

3reg044.idr:4:4:When checking right hand side of Main.pf:

2Type mismatch between

4Type mismatch between

3 b = b (Type of Refl)

5 b = b (Type of Refl)

test/reg047/reg047.idr+5−5

@@ -3,7 +3,7 @@ module test

3data TTSigma : (A : Type) -> (B : A -> Type) -> Type where

4 sigma : (A : Type) -> (B : A -> Type) -> (a : A) -> B a -> TTSigma A B

5

6−data Nat = zero | succ Nat

6+data Nat = Zero | Succ Nat

7

8Id : (A : Type) -> A -> A -> Type

9Id A = (=) {A = A} {B = A}

@@ -11,8 +11,8 @@ Id A = (=) {A = A} {B = A}

11IdRefl : (A : Type) -> (a : A) -> Id A a a

12IdRefl A a = Refl {x = a}

13

14−zzz : Id Nat zero zero

14+zzz : Id Nat Zero Zero

15−zzz = IdRefl Nat zero

15+zzz = IdRefl Nat Zero

16

17−eep : TTSigma Nat (\ a => Id Nat a zero)

17+eep : TTSigma Nat (\ a => Id Nat a Zero)

18−eep = sigma Nat (\ a => Id Nat a zero) zero zzz

18+eep = sigma Nat (\ a => Id Nat a Zero) Zero zzz

test/reg047/reg047a.idr+7−7

@@ -3,7 +3,7 @@ module test

3data TTSigma : (A : Type) -> (B : A -> Type) -> Type where

4 sigma : (A : Type) -> (B : A -> Type) -> (a : A) -> B a -> TTSigma A B

5

6−data MNat = zero | succ MNat

6+data MNat = Zero | Succ MNat

7

8Id : (A : Type) -> A -> A -> Type

9Id = \A,x,y => x = y -- {a = A} {b = A}

@@ -11,14 +11,14 @@ Id = \A,x,y => x = y -- {a = A} {b = A}

11IdRefl : (A : Type) -> (a : A) -> Id A a a

12IdRefl A a = Refl {x = a}

13

14−zzzz : Id MNat zero zero

14+zzzz : Id MNat Zero Zero

15−zzzz = IdRefl MNat zero

15+zzzz = IdRefl MNat Zero

16

17−eep : TTSigma MNat (\ c => Id MNat c zero)

17+eep : TTSigma MNat (\ c => Id MNat c Zero)

18−eep = (sigma MNat (\b => Id MNat b zero) zero zzzz)

18+eep = (sigma MNat (\b => Id MNat b Zero) Zero zzzz)

19

20−eep2 : TTSigma MNat (\ c => Id MNat c zero)

20+eep2 : TTSigma MNat (\ c => Id MNat c Zero)

21−eep2 = (sigma MNat (\b => Id MNat b zero) zero (IdRefl MNat zero))

21+eep2 = (sigma MNat (\b => Id MNat b Zero) Zero (IdRefl MNat Zero))

22

23

24

test/sourceLocation001/expected+8

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

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

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

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

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

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

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

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

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

1Testing using definition

9Testing using definition

2FileLoc "SourceLoc.idr" (16, 11) (16, 17)

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

3Testing using inline tactics

11Testing using inline tactics

test/sourceLocation001/run+1−1

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

1#!/usr/bin/env bash

2−idris $@ SourceLoc.idr -o sourceLocation001

2+idris $@ --nocolour --consolewidth 80 SourceLoc.idr -o sourceLocation001

3./sourceLocation001

4rm -f sourceLocation001 *.ibc

test/totality002/expected+2

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

1+test017.idr:94:26-31:

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

1test017a.idr:7:1:

3test017a.idr:7:1:

2scg.vtrans is possibly not total due to recursive path scg.vtrans --> scg.vtrans

4scg.vtrans is possibly not total due to recursive path scg.vtrans --> scg.vtrans

3test017b.idr:4:1:

5test017b.idr:4:1:

test/totality003/run+2−2

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

1#!/usr/bin/env bash

2−idris --consolewidth 80 $@ totality003.idr --check

2+idris --nocolour --consolewidth 80 $@ totality003.idr --check

3−idris --consolewidth 80 $@ totality003a.idr --check

3+idris --nocolour --consolewidth 80 $@ totality003a.idr --check

4rm -f *.ibc

test/tutorial002/expected+6

@@ -0,0 +1,6 @@

1+tutorial002.idr:41:25-30:

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

3+tutorial002.idr:48:18-23:

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

5+tutorial002.idr:54:18-23:

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

test/tutorial002/run+1−1

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

1#!/usr/bin/env bash

2−idris $@ tutorial002.idr --check

2+idris $@ --nocolour --consolewidth 80 tutorial002.idr --check

3rm -f *.ibc

test/tutorial004/expected+4

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

1+tutorial004.idr:46:14-19:

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

3+tutorial004.idr:53:14-19:

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

test/tutorial004/run+1−1

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

1#!/usr/bin/env bash

2−idris $@ tutorial004.idr --check

2+idris $@ tutorial004.idr --check --nocolour --consolewidth 80

3rm -f *.ibc