git.iko.soy/Idris-dev
on master help sign in
Merge branch 'master' into cabal-library
67da31aBrian McKenna
.gitignore+4
compare with master
unifiedsplit
@@ -11,6 +11,8 @@ cabal.sandbox.config
11*.swp
11*.swp
12*~
12*~
13.DS_Store
13.DS_Store
14+.hpc
15+*.tix
14custom.mk
16custom.mk
15test/output
17test/output
16test/test???/output
18test/test???/output
@@ -25,3 +27,5 @@ tutorial/*.out
25tutorial/*.toc
27tutorial/*.toc
26tutorial/*.fdb_latexmk
28tutorial/*.fdb_latexmk
27tutorial/*.fls
29tutorial/*.fls
30+tags
31+TAGS
.travis.yml+2−1
@@ -19,6 +19,7 @@ script:
19 - cabal copy
19 - cabal copy
20 - make -j2 $TESTS
20 - make -j2 $TESTS
21env:
21env:
22+ # TESTS=doc
22− - TESTS=test
23+ - TESTS=test_c
23 - TESTS=test_java
24 - TESTS=test_java
24 - TESTS=test_llvm
25 - TESTS=test_llvm
CHANGELOG+4
@@ -1,3 +1,7 @@
1+New in 0.9.11:
2+-------------
3+* Agda-style equational reasoning (in Syntax.PreorderReasoning)
4+
1New in 0.9.10:
5New in 0.9.10:
2--------------
6--------------
3
7
CONTRIBUTING.mdnew file+117
@@ -0,0 +1,117 @@
1+# Contributing to Idris-Dev
2+
3+The Idris Community welcomes pull requests, bug reporting, and bug squashing!
4+However, we cannot do it all ourself, and want to make it as easy as possible to contribute changes to get things working.
5+Here are a few guidelines that we would like contributors to follow so that we can have a chance of keeping on top of things.
6+
7+## Getting Started
8+
9+1. Make sure you are familiar with [Git](http://git-scm.com/book).
10+1. Make sure you have a [GitHub account](https://github.com/signup/free).
11+1. Make sure you are familiar with: [Idris](http://eb.host.cs.st-andrews.ac.uk/writings/idris-tutorial.pdf).
12+1. Make sure you can install `Idris`:
13+ * [Mac OS X](https://github.com/idris-lang/Idris-dev/wiki/Idris-on-OS-X-using-Homebrew)
14+ * [Ubuntu](https://github.com/idris-lang/Idris-dev/wiki/Idris-on-Ubuntu)
15+ * [Debian](https://github.com/idris-lang/Idris-dev/wiki/Idris-on-Debian)
16+ * [Windows](https://github.com/idris-lang/Idris-dev/wiki/Idris-on-Windows)
17+
18+# Issue Reporting
19+
20+Before you report an issue, or wish to add cool functionality please try and check to see if there are existing [issues](https://github.com/idris-lang/Idris-dev/issues) and [pull requests](https://github.com/idris-lang/Idris-dev/pulls).
21+We do not want you wasting your time, duplicating somebody's work!
22+
23+## The Campsite Rule
24+
25+A basic rule when contributing to Idris is the **campsite rule**: leave the codebase in better condition than you found it.
26+Please clean up any messes that you find, and don't leave behind new messes for the next contributor.
27+
28+## Making Changes
29+
30+Idris developers and hackers try to adhere to something similar to the [successful git branching model](http://nvie.com/posts/a-successful-git-branching-model/).
31+The steps are straightforward.
32+
33+For those new to the project:
34+
35+1. Fork the `idris-dev` repo e.g.
36+
37+ $ git clone git@github.com/<your github user name>/Idris-dev.git
38+ $ git remote add upstream git@github.com:idris-lang/Idris-dev.git
39+
40+For those already contributing to the project:
41+
42+1. Ensure your existing clone is up-to-date with current HEAD e.g.
43+
44+ $ git fetch upstream
45+ $ git merge upstream/master
46+
47+The remaining steps are the same:
48+
49+1. Create, and checkout onto, a topic branch on which to base you work.
50+ * This is typically the master branch.
51+ * For your own sanity, please avoid working on the `master` branch.
52+
53+ $ git branch fix/master/my_contrib master
54+ $ git checkout fix/master/my_contrib
55+
56+1. Make commits of logical units.
57+1. Check for unnecessary whitespace with
58+
59+ $ git diff --check
60+
61+1. Make sure your commit messages are along the lines of:
62+
63+ Short (50 chars or less) summary of changes
64+
65+ More detailed explanatory text, if necessary. Wrap it to about 72
66+ characters or so. In some contexts, the first line is treated as the
67+ subject of an email and the rest of the text as the body. The blank
68+ line separating the summary from the body is critical (unless you omit
69+ the body entirely); tools like rebase can get confused if you run the
70+ two together.
71+
72+ Further paragraphs come after blank lines.
73+
74+ - Bullet points are okay, too
75+
76+ - Typically a hyphen or asterisk is used for the bullet, preceded by a
77+ single space, with blank lines in between, but conventions vary here
78+
79+1. Make sure you have added any necessary tests for your changes.
80+1. Run all the tests to assure nothing else was accidentally broken.
81+
82+ $ make test
83+
84+1. Push your changes to a topic branch in your fork of the repository.
85+
86+ $ git push origin fix/master/my_contrib
87+
88+1. Go to GitHub and submit a pull request to `idris-dev`
89+
90+From there you will have to wait on one of the `idris-dev` committers to respond to the request.
91+This response might be an accept or some changes/improvements/alternatives will be suggest.
92+We do not guarantee that all requests will be accepted.
93+
94+## Increases chances of acceptance.
95+
96+To help increase the chance of your pull request being accepted:
97+
98+1. Run the tests.
99+1. Update the documentation, the surrounding one, examples elsewhere, guides, whatever is affected by your contribution
100+1. Use appropriate code formatting for both `Idris` and `Haskell`.
101+
102+## Additional Resources
103+
104+* [Idris Wiki](https://github.com/idris-lang/Idris-dev/wiki);
105+* [Zen Of Idris](https://github.com/idris-lang/Idris-dev/wiki/The-Zen-of-Idris);
106+* Idris FAQs: [Official](http://www.idris-lang.org/documentation/faq/); [Unofficial](https://github.com/idris-lang/Idris-dev/wiki/Unofficial-FAQ);
107+* [Idris Manual](https://github.com/idris-lang/Idris-dev/wiki/Manual);
108+* [Idris Tutorial](http://eb.host.cs.st-andrews.ac.uk/writings/idris-tutorial.pdf);
109+* [Idris News](http://www.idris-lang.org/news/);
110+* [other Idris docs](http://www.idris-lang.org/documentation/).
111+* [Using Pull Requests](https://help.github.com/articles/using-pull-requests)
112+* [General GitHub Documentation](https://help.github.com/).
113+
114+
115+Adapted from the most excellent contributing files from the [Puppet project](https://github.com/puppetlabs/puppet) and [Factroy Girl Rails](https://github.com/thoughtbot/factory_girl_rails/blob/master/CONTRIBUTING.md)
116+
117+
Makefile+4−2
@@ -1,4 +1,4 @@
1−.PHONY: build configure doc install linecount nodefault pinstall lib_clean relib test
1+.PHONY: build configure doc install linecount nodefault pinstall lib_clean relib test_c test
2
2
3include config.mk
3include config.mk
4-include custom.mk
4-include custom.mk
@@ -13,7 +13,9 @@ pinstall: dist/setup-config
13build: dist/setup-config
13build: dist/setup-config
14 $(CABAL) build $(CABALFLAGS)
14 $(CABAL) build $(CABALFLAGS)
15
15
16−test:
16+test: doc test_c
17+
18+test_c:
17 $(MAKE) -C test IDRIS=../dist/build/idris
19 $(MAKE) -C test IDRIS=../dist/build/idris
18
20
19test_java:
21test_java:
contribs/idrislang.sty+19−1
@@ -8,6 +8,8 @@
8%% + Defines a `numbers' and `default' listings style.
8%% + Defines a `numbers' and `default' listings style.
9%% + Defines a `code' environment for typesetting idris.
9%% + Defines a `code' environment for typesetting idris.
10%% + \begin{code}[...] ... \end{code}
10%% + \begin{code}[...] ... \end{code}
11+%% + Defines an input command for externally defined idris files.
12+%% + \inputIdrisListing[...]{file.idr}
11%% + Defines commands typesetting the name Idris.
13%% + Defines commands typesetting the name Idris.
12%% + \Idris{}
14%% + \Idris{}
13%% + \idris{}
15%% + \idris{}
@@ -46,6 +48,8 @@
46\lstdefinelanguage{idris}{%
48\lstdefinelanguage{idris}{%
47 sensitive,%
49 sensitive,%
48%% ----------------------------------------------------------- [ Default Style ]
50%% ----------------------------------------------------------- [ Default Style ]
51+ xleftmargin=\parindent,
52+ tabsize=2,
49 basicstyle=\ttfamily,
53 basicstyle=\ttfamily,
50 flexiblecolumns=false,
54 flexiblecolumns=false,
51 commentstyle=\footnotesize\sffamily,
55 commentstyle=\footnotesize\sffamily,
@@ -163,7 +167,8 @@
163
167
164\lstdefinestyle{default}{%
168\lstdefinestyle{default}{%
165 xleftmargin=\parindent,
169 xleftmargin=\parindent,
166− tabsize=2
170+ tabsize=2,
171+ basicstyle=\ttfamily
167}
172}
168\lstdefinestyle{numbers}{%
173\lstdefinestyle{numbers}{%
169 xleftmargin=\parindent,
174 xleftmargin=\parindent,
@@ -186,5 +191,18 @@
186 \lstset{style=default, #1}}
191 \lstset{style=default, #1}}
187 }
192 }
188 {}
193 {}
194+%% ---------------------------------------------------------- [ Input Listings ]
195+%% Command to add externally defined Idris code to the document.
196+\newcommand{\inputIdrisListing}[2][]{%
197+\begingroup
198+ \ifthenelse{\boolean{literate}}{%
199+ \lstset{language=literateidris}}{%
200+ \lstset{language=idris}}
201+ \ifthenelse{\boolean{numbers}}{%
202+ \lstset{style=numbers}}{%
203+ \lstset{style=default}}
204+ \lstinputlisting[#1]{#2}
205+\endgroup
206+}
189\endinput
207\endinput
190%% --------------------------------------------------------------------- [ EOF ]
208%% --------------------------------------------------------------------- [ EOF ]
idris.cabal+5−4
@@ -1,5 +1,5 @@
1Name: idris
1Name: idris
2−Version: 0.9.10
2+Version: 0.9.10.1
3License: BSD3
3License: BSD3
4License-file: LICENSE
4License-file: LICENSE
5Author: Edwin Brady
5Author: Edwin Brady
@@ -87,6 +87,7 @@ Extra-source-files:
87 libs/base/Makefile
87 libs/base/Makefile
88 libs/base/Network/*.idr
88 libs/base/Network/*.idr
89 libs/base/System/Concurrency/*.idr
89 libs/base/System/Concurrency/*.idr
90+ libs/base/Syntax/*.idr
90
91
91
92
92 libs/effects/Makefile
93 libs/effects/Makefile
@@ -102,8 +103,6 @@ Extra-source-files:
102 llvm/*.c
103 llvm/*.c
103 llvm/Makefile
104 llvm/Makefile
104
105
105− tutorial/examples/*.idr
106−
107 test/Makefile
106 test/Makefile
108 test/runtest.pl
107 test/runtest.pl
109 test/reg001/run
108 test/reg001/run
@@ -286,6 +285,9 @@ Extra-source-files:
286 test/test033/expected
285 test/test033/expected
287 test/test034/run
286 test/test034/run
288 test/test034/expected
287 test/test034/expected
288+ test/test035/run
289+ test/test035/expected
290+ test/test035/*.idr
289
291
290source-repository head
292source-repository head
291 type: git
293 type: git
@@ -511,7 +513,6 @@ Executable idris
511 , haskeline >= 0.7
513 , haskeline >= 0.7
512 , language-java >= 0.2.6
514 , language-java >= 0.2.6
513 , mtl
515 , mtl
514− --, parsec >= 3
515 , parsers == 0.9
516 , parsers == 0.9
516 , pretty
517 , pretty
517 , process
518 , process
libs/base/Control/Isomorphism.idrnew file+122
@@ -0,0 +1,122 @@
1+module Control.Isomorphism
2+
3+import Syntax.PreorderReasoning
4+
5+%default total
6+
7+-- An isomorphism between two types
8+data Iso : Type -> Type -> Type where
9+ MkIso : (to : a -> b) ->
10+ (from : b -> a) ->
11+ (toFrom : (y : b) -> to (from y) = y) ->
12+ (fromTo : (x : a) -> from (to x) = x) ->
13+ Iso a b
14+
15+-- Isomorphism properties
16+
17+isoRefl : Iso a a
18+isoRefl = MkIso id id (\x => refl) (\x => refl)
19+
20+isoTrans : Iso a b -> Iso b c -> Iso a c
21+isoTrans (MkIso to from toFrom fromTo) (MkIso to' from' toFrom' fromTo') =
22+ MkIso (\x => to' (to x))
23+ (\y => from (from' y))
24+ (\y => (to' (to (from (from' y)))) ={ cong (toFrom (from' y)) }=
25+ (to' (from' y)) ={ toFrom' y }=
26+ y QED)
27+ (\x => (from (from' (to' (to x)))) ={ cong (fromTo' (to x)) }=
28+ (from (to x)) ={ fromTo x }=
29+ x QED)
30+
31+
32+
33+-- Isomorphisms over sums
34+
35+eitherComm : Iso (Either a b) (Either b a)
36+eitherComm = MkIso swap swap swapSwap swapSwap
37+ where swap : Either a b -> Either b a
38+ swap (Left x) = Right x
39+ swap (Right x) = Left x
40+ swapSwap : (e : Either a b) -> swap (swap e) = e
41+ swapSwap (Left x) = refl
42+ swapSwap (Right x) = refl
43+
44+eitherAssoc : Iso (Either (Either a b) c) (Either a (Either b c))
45+eitherAssoc = MkIso eitherAssoc1 eitherAssoc2 ok1 ok2
46+ where eitherAssoc1 : Either (Either a b) c -> Either a (Either b c)
47+ eitherAssoc1 (Left (Left x)) = Left x
48+ eitherAssoc1 (Left (Right x)) = Right (Left x)
49+ eitherAssoc1 (Right x) = Right (Right x)
50+
51+ eitherAssoc2 : Either a (Either b c) -> Either (Either a b) c
52+ eitherAssoc2 (Left x) = Left (Left x)
53+ eitherAssoc2 (Right (Left x)) = Left (Right x)
54+ eitherAssoc2 (Right (Right x)) = Right x
55+
56+ ok1 : (x : Either a (Either b c)) -> eitherAssoc1 (eitherAssoc2 x) = x
57+ ok1 (Left x) = refl
58+ ok1 (Right (Left x)) = refl
59+ ok1 (Right (Right x)) = refl
60+
61+ ok2 : (x : Either (Either a b) c) -> eitherAssoc2 (eitherAssoc1 x) = x
62+ ok2 (Left (Left x)) = refl
63+ ok2 (Left (Right x)) = refl
64+ ok2 (Right x) = refl
65+
66+eitherBotLeft : Iso (Either _|_ a) a
67+eitherBotLeft = MkIso to from ok1 ok2
68+ where to : Either _|_ a -> a
69+ to (Left x) = FalseElim x
70+ to (Right x) = x
71+ from : a -> Either _|_ a
72+ from = Right
73+ ok1 : (x : a) -> to (from x) = x
74+ ok1 x = refl
75+ ok2 : (x : Either _|_ a) -> from (to x) = x
76+ ok2 (Left x) = FalseElim x
77+ ok2 (Right x) = refl
78+
79+eitherBotRight : Iso (Either a _|_) a
80+eitherBotRight = isoTrans eitherComm eitherBotLeft
81+
82+-- Isomorphisms over products
83+pairComm : Iso (a, b) (b, a)
84+pairComm = MkIso swap swap swapSwap swapSwap
85+ where swap : (a, b) -> (b, a)
86+ swap (x, y) = (y, x)
87+ swapSwap : (x : (a, b)) -> swap (swap x) = x
88+ swapSwap (x, y) = refl
89+
90+pairAssoc : Iso (a, (b, c)) ((a, b), c)
91+pairAssoc = MkIso to from ok1 ok2
92+ where
93+ to : (a, (b, c)) -> ((a, b), c)
94+ to (x, (y, z)) = ((x, y), z)
95+ from : ((a, b), c) -> (a, (b, c))
96+ from ((x, y), z) = (x, (y, z))
97+ ok1 : (x : ((a, b), c)) -> to (from x) = x
98+ ok1 ((x, y), z) = refl
99+ ok2 : (x : (a, (b, c))) -> from (to x) = x
100+ ok2 (x, (y, z)) = refl
101+
102+pairUnitRight : Iso (a, ()) a
103+pairUnitRight = MkIso fst (\x => (x, ())) (\x => refl) ok
104+ where ok : (x : (a, ())) -> (fst x, ()) = x
105+ ok (x, ()) = refl
106+
107+pairUnitLeft : Iso ((), a) a
108+pairUnitLeft = isoTrans pairComm pairUnitRight
109+
110+pairBotLeft : Iso (_|_, a) _|_
111+pairBotLeft = MkIso fst FalseElim (\x => FalseElim x) (\y => FalseElim (fst y))
112+
113+pairBotRight : Iso (a, _|_) _|_
114+pairBotRight = isoTrans pairComm pairBotLeft
115+
116+
117+-- Enable preorder reasoning syntax over isomorphisms
118+qed : (a : Type) -> Iso a a
119+qed a = isoRefl
120+
121+step : (a : Type) -> Iso a b -> Iso b c -> Iso a c
122+step a iso1 iso2 = isoTrans iso1 iso2
libs/base/Data/Vect/Quantifiers.idr+2−2
@@ -5,8 +5,8 @@ data Any : (P : a -> Type) -> Vect n a -> Type where
5 There : {P : a -> Type} -> {xs : Vect n a} -> Any P xs -> Any P (x :: xs)
5 There : {P : a -> Type} -> {xs : Vect n a} -> Any P xs -> Any P (x :: xs)
6
6
7anyNilAbsurd : {P : a -> Type} -> Any P Nil -> _|_
7anyNilAbsurd : {P : a -> Type} -> Any P Nil -> _|_
8−anyNilAbsurd Here impossible
8+anyNilAbsurd (Here _) impossible
9−anyNilAbsurd There impossible
9+anyNilAbsurd (There _) impossible
10
10
11anyElim : {xs : Vect n a} -> {P : a -> Type} -> (Any P xs -> b) -> (P x -> b) -> Any P (x :: xs) -> b
11anyElim : {xs : Vect n a} -> {P : a -> Type} -> (Any P xs -> b) -> (P x -> b) -> Any P (x :: xs) -> b
12anyElim _ f (Here p) = f p
12anyElim _ f (Here p) = f p
libs/base/Language/Reflection.idr+2
@@ -177,6 +177,8 @@ data Tactic = Try Tactic Tactic
177 -- ^ focus a named hole
177 -- ^ focus a named hole
178 | Rewrite TT
178 | Rewrite TT
179 -- ^ rewrite using the reflected rep. of a equality proof
179 -- ^ rewrite using the reflected rep. of a equality proof
180+ | Induction TTName
181+ -- ^ do induction on the particular expression
180 | LetTac TTName TT
182 | LetTac TTName TT
181 -- ^ name a reflected term
183 -- ^ name a reflected term
182 | LetTacTy TTName TT TT
184 | LetTacTy TTName TT TT
libs/base/Syntax/PreorderReasoning.idrnew file+15
@@ -0,0 +1,15 @@
1+module Syntax.PreorderReasoning
2+
3+-- QED is first to get the precedence to work out. It's just refl with an explicit argument.
4+syntax [expr] "QED" = qed expr
5+-- foo ={ prf }= bar ={ prf' }= fnord QED
6+-- is a proof that foo is related to fnord, with the intermediate step being bar, justified by prf and prf'
7+syntax [from] "={" [prf] "}=" [to] = step from prf to
8+
9+namespace Equal
10+ using (a : Type, x : a, y : a, z : a)
11+ qed : (x : a) -> x = x
12+ qed x = the (x = x) refl
13+ step : (x : a) -> x = y -> (y = z) -> x = z
14+ step x refl refl = refl
15+
libs/base/base.ipkg+7−2
@@ -16,15 +16,20 @@ modules = System,
16
16
17 Language.Reflection, Language.Reflection.Utils, Language.Reflection.Errors,
17 Language.Reflection, Language.Reflection.Utils, Language.Reflection.Errors,
18
18
19+ Syntax.PreorderReasoning,
20+
19− Data.Morphisms,
21+ Data.Morphisms,
20− Data.Bits, Data.Mod2,
22+ Data.Bits, Data.Mod2,
21 Data.ZZ, Data.Sign,
23 Data.ZZ, Data.Sign,
22 Data.SortedMap, Data.SortedSet, Data.BoundedList,
24 Data.SortedMap, Data.SortedSet, Data.BoundedList,
23 Data.Vect, Data.HVect, Data.Vect.Quantifiers,
25 Data.Vect, Data.HVect, Data.Vect.Quantifiers,
24 Data.Floats, Data.Complex, Data.Heap,
26 Data.Floats, Data.Complex, Data.Heap,
25
27
28+ Control.Isomorphism,
26 Control.Monad.Identity,
29 Control.Monad.Identity,
27 Control.Monad.RWS,
30 Control.Monad.RWS,
28 Control.Monad.State, Control.Monad.Writer, Control.Monad.Reader,
31 Control.Monad.State, Control.Monad.Writer, Control.Monad.Reader,
29 Control.Category, Control.Arrow,
32 Control.Category, Control.Arrow,
30 Control.Catchable, Control.IOExcept
33 Control.Catchable, Control.IOExcept
34+
35+
libs/prelude/Decidable/Equality.idr+38
@@ -1,6 +1,7 @@
1module Decidable.Equality
1module Decidable.Equality
2
2
3import Builtins
3import Builtins
4+import Prelude.Basics
4import Prelude.Either
5import Prelude.Either
5import Prelude.List
6import Prelude.List
6import Prelude.Vect
7import Prelude.Vect
@@ -177,3 +178,40 @@ instance DecEq a => DecEq (Vect n a) where
177 decEq (x :: xs) (x :: xs) | (Yes refl, Yes refl) = Yes refl
178 decEq (x :: xs) (x :: xs) | (Yes refl, Yes refl) = Yes refl
178 decEq (x :: xs) (y :: ys) | (_, No nEqTl) = No (\p => nEqTl (vectInjective2 p))
179 decEq (x :: xs) (y :: ys) | (_, No nEqTl) = No (\p => nEqTl (vectInjective2 p))
179 decEq (x :: xs) (y :: ys) | (No nEqHd, _) = No (\p => nEqHd (vectInjective1 p))
180 decEq (x :: xs) (y :: ys) | (No nEqHd, _) = No (\p => nEqHd (vectInjective1 p))
181+
182+
183+-- For the primitives, we have to cheat because we don't have access to their
184+-- internal implementations.
185+
186+--------------------------------------------------------------------------------
187+-- Int
188+--------------------------------------------------------------------------------
189+
190+instance DecEq Int where
191+ decEq x y = if x == y then Yes (really_believe_me {a = x=x} {b = x=y} refl)
192+ else No (really_believe_me _|_)
193+
194+--------------------------------------------------------------------------------
195+-- Char
196+--------------------------------------------------------------------------------
197+
198+instance DecEq Char where
199+ decEq x y = if x == y then Yes (really_believe_me {a = x=x} {b = x=y} refl)
200+ else No (really_believe_me _|_)
201+
202+--------------------------------------------------------------------------------
203+-- Integer
204+--------------------------------------------------------------------------------
205+
206+instance DecEq Integer where
207+ decEq x y = if x == y then Yes (really_believe_me {a = x=x} {b = x=y} refl)
208+ else No (really_believe_me _|_)
209+
210+--------------------------------------------------------------------------------
211+-- Float
212+--------------------------------------------------------------------------------
213+
214+instance DecEq Float where
215+ decEq x y = if x == y then Yes (really_believe_me {a = x=x} {b = x=y} refl)
216+ else No (really_believe_me _|_)
217+
libs/prelude/Prelude.idr+1−1
@@ -410,7 +410,7 @@ syntax "[" [start] "," [next] ".." [end] "]"
410 = enumFromThenTo start (next - start) end
410 = enumFromThenTo start (next - start) end
411
411
412syntax "[" [start] "..]"
412syntax "[" [start] "..]"
413− = enumFrom start 1
413+ = enumFrom start
414syntax "[" [start] "," [next] "..]"
414syntax "[" [start] "," [next] "..]"
415 = enumFromThen start (next - start)
415 = enumFromThen start (next - start)
416
416
libs/prelude/Prelude/Fin.idr+16−8
@@ -3,6 +3,8 @@ module Prelude.Fin
3import Prelude.Nat
3import Prelude.Nat
4import Prelude.Either
4import Prelude.Either
5
5
6+%default total
7+
6data Fin : Nat -> Type where
8data Fin : Nat -> Type where
7 fZ : Fin (S k)
9 fZ : Fin (S k)
8 fS : Fin k -> Fin (S k)
10 fS : Fin k -> Fin (S k)
@@ -12,19 +14,25 @@ instance Eq (Fin n) where
12 (==) (fS k) (fS k') = k == k'
14 (==) (fS k) (fS k') = k == k'
13 (==) _ _ = False
15 (==) _ _ = False
14
16
17+FinZAbsurd : Fin Z -> _|_
18+FinZAbsurd fZ impossible
19+
20+FinZElim : Fin Z -> a
21+FinZElim x = FalseElim (FinZAbsurd x)
22+
15−finToNat : Fin n -> Nat -> Nat
23+finToNat : Fin n -> Nat
16−finToNat fZ a = a
24+finToNat fZ = Z
17−finToNat (fS x) a = finToNat x (S a)
25+finToNat (fS k) = S (finToNat k)
18
26
19instance Cast (Fin n) Nat where
27instance Cast (Fin n) Nat where
20− cast x = finToNat x Z
28+ cast x = finToNat x
21
29
22−finToInt : Fin n -> Integer -> Integer
30+finToInteger : Fin n -> Integer
23−finToInt fZ a = a
31+finToInteger fZ = 0
24−finToInt (fS x) a = finToInt x (a + 1)
32+finToInteger (fS k) = 1 + finToInteger k
25
33
26instance Cast (Fin n) Integer where
34instance Cast (Fin n) Integer where
27− cast x = finToInt x 0
35+ cast x = finToInteger x
28
36
29weaken : Fin n -> Fin (S n)
37weaken : Fin n -> Fin (S n)
30weaken fZ = fZ
38weaken fZ = fZ
libs/prelude/Prelude/List.idr+4−5
@@ -15,10 +15,13 @@ import Prelude.Nat
15infixr 7 ::
15infixr 7 ::
16infixl 8 ++
16infixl 8 ++
17
17
18−data List a
18+%elim data List a
19 = Nil
19 = Nil
20 | (::) a (List a)
20 | (::) a (List a)
21
21
22+-- Name hints for interactive editing
23+%name List xs, ys, zs, ws
24+
22--------------------------------------------------------------------------------
25--------------------------------------------------------------------------------
23-- Syntactic tests
26-- Syntactic tests
24--------------------------------------------------------------------------------
27--------------------------------------------------------------------------------
@@ -461,10 +464,6 @@ sort xs =
461-- Conversions
464-- Conversions
462--------------------------------------------------------------------------------
465--------------------------------------------------------------------------------
463
466
464−maybeToList : Maybe a -> List a
465−maybeToList Nothing = []
466−maybeToList (Just j) = [j]
467−
468listToMaybe : List a -> Maybe a
467listToMaybe : List a -> Maybe a
469listToMaybe [] = Nothing
468listToMaybe [] = Nothing
470listToMaybe (x::xs) = Just x
469listToMaybe (x::xs) = Just x
libs/prelude/Prelude/Nat.idr+4−1
@@ -10,10 +10,13 @@ import Prelude.Classes
10%access public
10%access public
11%default total
11%default total
12
12
13−data Nat
13+%elim data Nat
14 = Z
14 = Z
15 | S Nat
15 | S Nat
16
16
17+-- name hints for interactive editing
18+%name Nat k,j,i,n,m
19+
17--------------------------------------------------------------------------------
20--------------------------------------------------------------------------------
18-- Syntactic tests
21-- Syntactic tests
19--------------------------------------------------------------------------------
22--------------------------------------------------------------------------------
libs/prelude/Prelude/Vect.idr+30−19
@@ -11,9 +11,12 @@ import Prelude.Nat
11
11
12infixr 7 ::
12infixr 7 ::
13
13
14−data Vect : Nat -> Type -> Type where
14+%elim data Vect : Nat -> Type -> Type where
15 Nil : Vect Z a
15 Nil : Vect Z a
16− (::) : a -> Vect n a -> Vect (S n) a
16+ (::) : (x : a) -> (xs : Vect n a) -> Vect (S n) a
17+
18+-- Hints for interactive editing
19+%name Vect xs,ys,zs,ws
17
20
18--------------------------------------------------------------------------------
21--------------------------------------------------------------------------------
19-- Indexing into vectors
22-- Indexing into vectors
@@ -51,15 +54,14 @@ replaceAt (fS k) y (x::xs) = x :: replaceAt k y xs
51-- Subvectors
54-- Subvectors
52--------------------------------------------------------------------------------
55--------------------------------------------------------------------------------
53
56
54−take : Fin n -> Vect n a -> (p ** Vect p a)
57+take : {n : Nat} -> (m : Fin (S n)) -> Vect n a -> Vect (cast m) a
58+take (fS k) [] = FinZElim k
55−take fZ xs = (_ ** [])
59+take fZ _ = []
56−take (fS k) [] impossible
57−take (fS k) (x::xs) with (take k xs)
60+take (fS k) (x::xs) = x :: take k xs
58− | (_ ** tail) = (_ ** x::tail)
59
61
60−drop : Fin n -> Vect n a -> (p ** Vect p a)
62+drop : (m : Fin (S n)) -> Vect n a -> Vect (n - cast m) a
61−drop fZ xs = (_ ** xs)
62−drop (fS k) [] impossible
63+drop (fS k) [] = FinZElim k
64+drop fZ xs ?= xs
63drop (fS k) (x::xs) = drop k xs
65drop (fS k) (x::xs) = drop k xs
64
66
65--------------------------------------------------------------------------------
67--------------------------------------------------------------------------------
@@ -143,15 +145,13 @@ reverse = reverse' []
143 reverse' acc [] ?= acc
145 reverse' acc [] ?= acc
144 reverse' acc (x::xs) ?= reverse' (x::acc) xs
146 reverse' acc (x::xs) ?= reverse' (x::acc) xs
145
147
146−total intersperse' : a -> Vect m a -> (p ** Vect p a)
148+intersperse : a -> Vect n a -> Vect (n + pred n) a
147−intersperse' sep [] = (_ ** [])
149+intersperse sep [] = []
148−intersperse' sep (y::ys) with (intersperse' sep ys)
150+intersperse sep (x::xs) = x :: intersperse' sep xs
149− | (_ ** tail) = (_ ** sep::y::tail)
151+ where
150−
151−total intersperse : a -> Vect m a -> (p ** Vect p a)
152+ intersperse' : a -> Vect n a -> Vect (n + n) a
152−intersperse sep [] = (_ ** [])
153+ intersperse' sep [] = []
153−intersperse sep (x::xs) with (intersperse' sep xs)
154+ intersperse' sep (x::xs) ?= sep :: x :: intersperse' sep xs
154− | (_ ** tail) = (_ ** x::tail)
155
155
156--------------------------------------------------------------------------------
156--------------------------------------------------------------------------------
157-- Membership tests
157-- Membership tests
@@ -311,6 +311,12 @@ range {n=S _} = fZ :: map fS range
311-- Proofs
311-- Proofs
312--------------------------------------------------------------------------------
312--------------------------------------------------------------------------------
313
313
314+Prelude.Vect.drop_lemma_1 = proof {
315+ intros;
316+ rewrite sym (minusZeroRight n);
317+ trivial;
318+}
319+
314Prelude.Vect.reverse'_lemma_2 = proof {
320Prelude.Vect.reverse'_lemma_2 = proof {
315 intros;
321 intros;
316 rewrite (plusSuccRightSucc m n1);
322 rewrite (plusSuccRightSucc m n1);
@@ -323,3 +329,8 @@ Prelude.Vect.reverse'_lemma_1 = proof {
323 exact value;
329 exact value;
324}
330}
325
331
332+Prelude.Vect.intersperse'_lemma_1 = proof {
333+ intros;
334+ rewrite (plusSuccRightSucc n1 n1);
335+ trivial;
336+}
src/Idris/AbsSyntax.hs+39−28
@@ -167,6 +167,25 @@ addDocStr n doc
167 = do i <- getIState
167 = do i <- getIState
168 putIState $ i { idris_docstrings = addDef n doc (idris_docstrings i) }
168 putIState $ i { idris_docstrings = addDef n doc (idris_docstrings i) }
169
169
170+addNameHint :: Name -> Name -> Idris ()
171+addNameHint ty n
172+ = do i <- getIState
173+ ty' <- case lookupCtxtName ty (idris_implicits i) of
174+ [(tyn, _)] -> return tyn
175+ [] -> throwError (NoSuchVariable ty)
176+ tyns -> throwError (CantResolveAlts (map show (map fst tyns)))
177+ let ns' = case lookupCtxt ty' (idris_namehints i) of
178+ [ns] -> ns ++ [n]
179+ _ -> [n]
180+ putIState $ i { idris_namehints = addDef ty' ns' (idris_namehints i) }
181+
182+getNameHints :: IState -> Name -> [Name]
183+getNameHints i (UN "->") = [UN "f",UN "g"]
184+getNameHints i n =
185+ case lookupCtxt n (idris_namehints i) of
186+ [ns] -> ns
187+ _ -> []
188+
170addToCalledG :: Name -> [Name] -> Idris ()
189addToCalledG :: Name -> [Name] -> Idris ()
171addToCalledG n ns = return () -- TODO
190addToCalledG n ns = return () -- TODO
172
191
@@ -178,10 +197,10 @@ addInstance :: Bool -> Name -> Name -> Idris ()
178addInstance int n i
197addInstance int n i
179 = do ist <- getIState
198 = do ist <- getIState
180 case lookupCtxt n (idris_classes ist) of
199 case lookupCtxt n (idris_classes ist) of
181− [CI a b c d ins] ->
200+ [CI a b c d e ins] ->
182− do let cs = addDef n (CI a b c d (addI i ins)) (idris_classes ist)
201+ do let cs = addDef n (CI a b c d e (addI i ins)) (idris_classes ist)
183 putIState $ ist { idris_classes = cs }
202 putIState $ ist { idris_classes = cs }
184− _ -> do let cs = addDef n (CI (MN 0 "none") [] [] [] [i]) (idris_classes ist)
203+ _ -> do let cs = addDef n (CI (MN 0 "none") [] [] [] [] [i]) (idris_classes ist)
185 putIState $ ist { idris_classes = cs }
204 putIState $ ist { idris_classes = cs }
186 where addI i ins | int = i : ins
205 where addI i ins | int = i : ins
187 | chaser n = ins ++ [i]
206 | chaser n = ins ++ [i]
@@ -371,7 +390,7 @@ ihWarn :: Handle -> FC -> String -> Idris ()
371ihWarn h fc err = do i <- getIState
390ihWarn h fc err = do i <- getIState
372 case idris_outputmode i of
391 case idris_outputmode i of
373 RawOutput -> runIO $ hPutStrLn h (show fc ++ ":" ++ err)
392 RawOutput -> runIO $ hPutStrLn h (show fc ++ ":" ++ err)
374− IdeSlave n -> runIO $ hPutStrLn h $ convSExp "warning" (fc_fname fc, fc_line fc, err) n
393+ IdeSlave n -> runIO $ hPutStrLn h $ convSExp "warning" (fc_fname fc, fc_line fc, fc_column fc, err) n
375
394
376setLogLevel :: Int -> Idris ()
395setLogLevel :: Int -> Idris ()
377setLogLevel l = do i <- getIState
396setLogLevel l = do i <- getIState
@@ -631,11 +650,12 @@ inferTy = MN 0 "__Infer"
631inferCon = MN 0 "__infer"
650inferCon = MN 0 "__infer"
632inferDecl = PDatadecl inferTy
651inferDecl = PDatadecl inferTy
633 PType
652 PType
634− [("", inferCon, PPi impl (MN 0 "A") PType (
653+ [("", inferCon, PPi impl (MN 0 "iType") PType (
635− PPi expl (MN 0 "a") (PRef bi (MN 0 "A"))
654+ PPi expl (MN 0 "ival") (PRef bi (MN 0 "iType"))
636 (PRef bi inferTy)), bi)]
655 (PRef bi inferTy)), bi)]
656+inferOpts = []
637
657
638−infTerm t = PApp bi (PRef bi inferCon) [pimp (MN 0 "A") Placeholder True, pexp t]
658+infTerm t = PApp bi (PRef bi inferCon) [pimp (MN 0 "iType") Placeholder True, pexp t]
639infP = P (TCon 6 0) inferTy (TType (UVal 0))
659infP = P (TCon 6 0) inferTy (TType (UVal 0))
640
660
641getInferTerm, getInferType :: Term -> Term
661getInferTerm, getInferType :: Term -> Term
@@ -646,7 +666,7 @@ getInferTerm tm = tm -- error ("getInferTerm " ++ show tm)
646getInferType (Bind n b sc) = Bind n b $ getInferType sc
666getInferType (Bind n b sc) = Bind n b $ getInferType sc
647getInferType (App (App _ ty) _) = ty
667getInferType (App (App _ ty) _) = ty
648
668
649−-- Handy primitives: Unit, False, Pair, MkPair, =, mkForeign
669+-- Handy primitives: Unit, False, Pair, MkPair, =, mkForeign, Elim type class
650
670
651primNames = [unitTy, unitCon,
671primNames = [unitTy, unitCon,
652 falseTy, pairTy, pairCon,
672 falseTy, pairTy, pairCon,
@@ -656,9 +676,11 @@ unitTy = MN 0 "__Unit"
656unitCon = MN 0 "__II"
676unitCon = MN 0 "__II"
657unitDecl = PDatadecl unitTy PType
677unitDecl = PDatadecl unitTy PType
658 [("", unitCon, PRef bi unitTy, bi)]
678 [("", unitCon, PRef bi unitTy, bi)]
679+unitOpts = [DefaultEliminator]
659
680
660falseTy = MN 0 "__False"
681falseTy = MN 0 "__False"
661falseDecl = PDatadecl falseTy PType []
682falseDecl = PDatadecl falseTy PType []
683+falseOpts = []
662
684
663pairTy = MN 0 "__Pair"
685pairTy = MN 0 "__Pair"
664pairCon = MN 0 "__MkPair"
686pairCon = MN 0 "__MkPair"
@@ -670,6 +692,7 @@ pairDecl = PDatadecl pairTy (piBind [(n "A", PType), (n "B", PType)] PType)
670 (PApp bi (PRef bi pairTy) [pexp (PRef bi (n "A")),
692 (PApp bi (PRef bi pairTy) [pexp (PRef bi (n "A")),
671 pexp (PRef bi (n "B"))])))), bi)]
693 pexp (PRef bi (n "B"))])))), bi)]
672 where n a = MN 0 a
694 where n a = MN 0 a
695+pairOpts = []
673
696
674eqTy = UN "="
697eqTy = UN "="
675eqCon = UN "refl"
698eqCon = UN "refl"
@@ -683,6 +706,14 @@ eqDecl = PDatadecl eqTy (piBind [(n "a", PType), (n "b", PType),
683 pexp (PRef bi (n "x")),
706 pexp (PRef bi (n "x")),
684 pexp (PRef bi (n "x"))])), bi)]
707 pexp (PRef bi (n "x"))])), bi)]
685 where n a = MN 0 a
708 where n a = MN 0 a
709+eqOpts = []
710+
711+elimName = UN "__Elim"
712+elimMethElimTy = UN "__elimTy"
713+elimMethElim = UN "elim"
714+elimDecl = PClass "Type class for eliminators" defaultSyntax bi [] elimName [(UN "scrutineeType", PType)]
715+ [PTy "" defaultSyntax bi [TotalFn] elimMethElimTy PType,
716+ PTy "" defaultSyntax bi [TotalFn] elimMethElim (PRef bi elimMethElimTy)]
686
717
687-- Defined in builtins.idr
718-- Defined in builtins.idr
688sigmaTy = UN "Exists"
719sigmaTy = UN "Exists"
@@ -1361,26 +1392,6 @@ findStatics ist tm = trace (showImp Nothing True False tm) $
1361 return (PPi p n t sc')
1392 return (PPi p n t sc')
1362 pos ns ss t = return t
1393 pos ns ss t = return t
1363
1394
1364−-- Debugging/logging stuff
1365−
1366−dumpDecls :: [PDecl] -> String
1367−dumpDecls [] = ""
1368−dumpDecls (d:ds) = dumpDecl d ++ "\n" ++ dumpDecls ds
1369−
1370−dumpDecl (PFix _ f ops) = show f ++ " " ++ showSep ", " ops
1371−dumpDecl (PTy _ _ _ _ n t) = "tydecl " ++ show n ++ " : " ++ showImp Nothing True False t
1372−dumpDecl (PClauses _ _ n cs) = "pat " ++ show n ++ "\t" ++ showSep "\n\t" (map (showCImp True) cs)
1373−dumpDecl (PData _ _ _ _ d) = showDImp True d
1374−dumpDecl (PParams _ ns ps) = "params {" ++ show ns ++ "\n" ++ dumpDecls ps ++ "}\n"
1375−dumpDecl (PNamespace n ps) = "namespace {" ++ n ++ "\n" ++ dumpDecls ps ++ "}\n"
1376−dumpDecl (PSyntax _ syn) = "syntax " ++ show syn
1377−dumpDecl (PClass _ _ _ cs n ps ds)
1378− = "class " ++ show cs ++ " " ++ show n ++ " " ++ show ps ++ "\n" ++ dumpDecls ds
1379−dumpDecl (PInstance _ _ cs n _ t _ ds)
1380− = "instance " ++ show cs ++ " " ++ show n ++ " " ++ show t ++ "\n" ++ dumpDecls ds
1381−dumpDecl _ = "..."
1382−-- dumpDecl (PImport i) = "import " ++ i
1383−
1384-- for 6.12/7 compatibility
1395-- for 6.12/7 compatibility
1385data EitherErr a b = LeftErr a | RightOK b
1396data EitherErr a b = LeftErr a | RightOK b
1386
1397
src/Idris/AbsSyntaxTree.hs+45−9
@@ -92,6 +92,7 @@ data IState = IState {
92 idris_dsls :: Ctxt DSL,
92 idris_dsls :: Ctxt DSL,
93 idris_optimisation :: Ctxt OptInfo,
93 idris_optimisation :: Ctxt OptInfo,
94 idris_datatypes :: Ctxt TypeInfo,
94 idris_datatypes :: Ctxt TypeInfo,
95+ idris_namehints :: Ctxt [Name],
95 idris_patdefs :: Ctxt ([([Name], Term, Term)], [PTerm]), -- not exported
96 idris_patdefs :: Ctxt ([([Name], Term, Term)], [PTerm]), -- not exported
96 -- ^ list of lhs/rhs, and a list of missing clauses
97 -- ^ list of lhs/rhs, and a list of missing clauses
97 idris_flags :: Ctxt [FnOpt],
98 idris_flags :: Ctxt [FnOpt],
@@ -183,12 +184,14 @@ data IBCWrite = IBCFix FixDecl
183 | IBCDoc Name
184 | IBCDoc Name
184 | IBCCoercion Name
185 | IBCCoercion Name
185 | IBCDef Name -- i.e. main context
186 | IBCDef Name -- i.e. main context
187+ | IBCNameHint (Name, Name)
186 | IBCLineApp FilePath Int PTerm
188 | IBCLineApp FilePath Int PTerm
187 deriving Show
189 deriving Show
188
190
189idrisInit = IState initContext [] [] emptyContext emptyContext emptyContext
191idrisInit = IState initContext [] [] emptyContext emptyContext emptyContext
190 emptyContext emptyContext emptyContext emptyContext
192 emptyContext emptyContext emptyContext emptyContext
191 emptyContext emptyContext emptyContext emptyContext
193 emptyContext emptyContext emptyContext emptyContext
194+ emptyContext
192 [] [] defaultOpts 6 [] [] [] [] [] [] [] [] [] [] [] []
195 [] [] defaultOpts 6 [] [] [] [] [] [] [] [] [] [] [] []
193 [] Nothing Nothing [] [] [] Hidden False [] Nothing [] [] RawOutput
196 [] Nothing Nothing [] [] [] Hidden False [] Nothing [] [] RawOutput
194 True defaultTheme stdout
197 True defaultTheme stdout
@@ -392,6 +395,14 @@ inlinable = elem Inlinable
392dictionary :: FnOpts -> Bool
395dictionary :: FnOpts -> Bool
393dictionary = elem Dictionary
396dictionary = elem Dictionary
394
397
398+
399+-- | Data declaration options
400+data DataOpt = Codata -- Set if the the data-type is coinductive
401+ | DefaultEliminator -- Set if an eliminator should be generated for data type
402+ deriving (Show, Eq)
403+
404+type DataOpts = [DataOpt]
405+
395-- | Top-level declarations such as compiler directives, definitions,
406-- | Top-level declarations such as compiler directives, definitions,
396-- datatypes and typeclasses.
407-- datatypes and typeclasses.
397data PDecl' t
408data PDecl' t
@@ -400,7 +411,7 @@ data PDecl' t
400 | PPostulate String SyntaxInfo FC FnOpts Name t -- ^ Postulate
411 | PPostulate String SyntaxInfo FC FnOpts Name t -- ^ Postulate
401 | PClauses FC FnOpts Name [PClause' t] -- ^ Pattern clause
412 | PClauses FC FnOpts Name [PClause' t] -- ^ Pattern clause
402 | PCAF FC Name t -- ^ Top level constant
413 | PCAF FC Name t -- ^ Top level constant
403− | PData String SyntaxInfo FC Bool (PData' t) -- ^ Data declaration. The Bool argument is True for codata.
414+ | PData String SyntaxInfo FC DataOpts (PData' t) -- ^ Data declaration.
404 | PParams FC [(Name, t)] [PDecl' t] -- ^ Params block
415 | PParams FC [(Name, t)] [PDecl' t] -- ^ Params block
405 | PNamespace String [PDecl' t] -- ^ New namespace
416 | PNamespace String [PDecl' t] -- ^ New namespace
406 | PRecord String SyntaxInfo FC Name t String Name t -- ^ Record declaration
417 | PRecord String SyntaxInfo FC Name t String Name t -- ^ Record declaration
@@ -627,6 +638,7 @@ mapPT f t = f (mpt t) where
627
638
628data PTactic' t = Intro [Name] | Intros | Focus Name
639data PTactic' t = Intro [Name] | Intros | Focus Name
629 | Refine Name [Bool] | Rewrite t
640 | Refine Name [Bool] | Rewrite t
641+ | Induction Name
630 | Equiv t
642 | Equiv t
631 | MatchRefine Name
643 | MatchRefine Name
632 | LetTac Name t | LetTacTy Name t t
644 | LetTac Name t | LetTacTy Name t t
@@ -654,6 +666,7 @@ instance Sized a => Sized (PTactic' a) where
654 size (Focus nm) = 1 + size nm
666 size (Focus nm) = 1 + size nm
655 size (Refine nm bs) = 1 + size nm + length bs
667 size (Refine nm bs) = 1 + size nm + length bs
656 size (Rewrite t) = 1 + size t
668 size (Rewrite t) = 1 + size t
669+ size (Induction t) = 1 + size t
657 size (LetTac nm t) = 1 + size nm + size t
670 size (LetTac nm t) = 1 + size nm + size t
658 size (Exact t) = 1 + size t
671 size (Exact t) = 1 + size t
659 size Compute = 1
672 size Compute = 1
@@ -737,6 +750,7 @@ type PArg = PArg' PTerm
737data ClassInfo = CI { instanceName :: Name,
750data ClassInfo = CI { instanceName :: Name,
738 class_methods :: [(Name, (FnOpts, PTerm))],
751 class_methods :: [(Name, (FnOpts, PTerm))],
739 class_defaults :: [(Name, (Name, PDecl))], -- method name -> default impl
752 class_defaults :: [(Name, (Name, PDecl))], -- method name -> default impl
753+ class_default_superclasses :: [PDecl],
740 class_params :: [Name],
754 class_params :: [Name],
741 class_instances :: [Name] }
755 class_instances :: [Name] }
742 deriving Show
756 deriving Show
@@ -745,9 +759,21 @@ deriving instance Binary ClassInfo
745deriving instance NFData ClassInfo
759deriving instance NFData ClassInfo
746!-}
760!-}
747
761
762+-- An argument is conditionally forceable iff its forceability
763+-- depends on the collapsibility of the whole type.
764+data Forceability = Conditional | Unconditional deriving (Show, Enum, Bounded, Eq, Ord)
765+
766+{-!
767+deriving instance Binary Forceability
768+deriving instance NFData Forceability
769+!-}
770+
748data OptInfo = Optimise { collapsible :: Bool,
771data OptInfo = Optimise { collapsible :: Bool,
749 isnewtype :: Bool,
772 isnewtype :: Bool,
773+ -- The following should actually be (IntMap Forceability)
774+ -- but the corresponding Binary instance seems to be broken.
775+ -- Let's store a list and convert it to IntMap whenever needed.
750− forceable :: [Int], -- argument positions
776+ forceable :: [(Int, Forceability)],
751 recursive :: [Int] }
777 recursive :: [Int] }
752 deriving Show
778 deriving Show
753{-!
779{-!
@@ -869,13 +895,23 @@ instance Show PClause where
869instance Show PData where
895instance Show PData where
870 show d = showDImp False d
896 show d = showDImp False d
871
897
898+showDecls :: Bool -> [PDecl] -> String
899+showDecls _ [] = ""
900+showDecls i (d:ds) = showDeclImp i d ++ "\n" ++ showDecls i ds
901+
872showDeclImp _ (PFix _ f ops) = show f ++ " " ++ showSep ", " ops
902showDeclImp _ (PFix _ f ops) = show f ++ " " ++ showSep ", " ops
873−showDeclImp t (PTy _ _ _ _ n ty) = show n ++ " : " ++ showImp Nothing t False ty
903+showDeclImp i (PTy _ _ _ _ n t) = "tydecl " ++ showCG n ++ " : " ++ showImp Nothing i False t
874−showDeclImp t (PPostulate _ _ _ _ n ty) = show n ++ " : " ++ showImp Nothing t False ty
875−showDeclImp _ (PClauses _ _ n c) = showSep "\n" (map show c)
904+showDeclImp i (PClauses _ _ n cs) = "pat " ++ showCG n ++ "\t" ++ showSep "\n\t" (map (showCImp i) cs)
876−showDeclImp _ (PData _ _ _ _ d) = show d
905+showDeclImp _ (PData _ _ _ _ d) = showDImp True d
877−showDeclImp _ (PParams f ns ps) = "parameters " ++ show ns ++ "\n" ++
906+showDeclImp i (PParams _ ns ps) = "params {" ++ show ns ++ "\n" ++ showDecls i ps ++ "}\n"
878− showSep "\n" (map show ps)
907+showDeclImp i (PNamespace n ps) = "namespace {" ++ n ++ "\n" ++ showDecls i ps ++ "}\n"
908+showDeclImp _ (PSyntax _ syn) = "syntax " ++ show syn
909+showDeclImp i (PClass _ _ _ cs n ps ds)
910+ = "class " ++ show cs ++ " " ++ show n ++ " " ++ show ps ++ "\n" ++ showDecls i ds
911+showDeclImp i (PInstance _ _ cs n _ t _ ds)
912+ = "instance " ++ show cs ++ " " ++ show n ++ " " ++ show t ++ "\n" ++ showDecls i ds
913+showDeclImp _ _ = "..."
914+-- showDeclImp (PImport i) = "import " ++ i
879
915
880
916
881showCImp :: Bool -> PClause -> String
917showCImp :: Bool -> PClause -> String
@@ -1121,7 +1157,7 @@ showName ist bnd impl colour n = case ist of
1121 Just i -> if colour then colourise n (idris_colourTheme i) else showbasic n
1157 Just i -> if colour then colourise n (idris_colourTheme i) else showbasic n
1122 Nothing -> showbasic n
1158 Nothing -> showbasic n
1123 where name = if impl then show n else showbasic n
1159 where name = if impl then show n else showbasic n
1124− showbasic n@(UN _) = show n
1160+ showbasic n@(UN _) = showCG n
1125 showbasic (MN _ s) = s
1161 showbasic (MN _ s) = s
1126 showbasic (NS n s) = showSep "." (reverse s) ++ "." ++ showbasic n
1162 showbasic (NS n s) = showSep "." (reverse s) ++ "." ++ showbasic n
1127 showbasic (SN s) = show s
1163 showbasic (SN s) = show s
src/Idris/CaseSplit.hs+141−71
@@ -3,6 +3,7 @@
3module Idris.CaseSplit(splitOnLine, replaceSplits,
3module Idris.CaseSplit(splitOnLine, replaceSplits,
4 getClause, getProofClause,
4 getClause, getProofClause,
5 mkWith,
5 mkWith,
6+ nameMissing,
6 getUniq, nameRoot) where
7 getUniq, nameRoot) where
7
8
8-- splitting a variable in a pattern clause
9-- splitting a variable in a pattern clause
@@ -71,38 +72,68 @@ split n t'
71 logLvl 3 ("Split:\n" ++
72 logLvl 3 ("Split:\n" ++
72 (showSep "\n" (map show (mapMaybe id newPats))))
73 (showSep "\n" (map show (mapMaybe id newPats))))
73 logLvl 3 "----"
74 logLvl 3 "----"
74− let newPats' = mergeAllPats ctxt t (mapMaybe id newPats)
75+ let newPats' = mergeAllPats ist n t (mapMaybe id newPats)
75 iLOG ("Name updates " ++ showSep "\n"
76 iLOG ("Name updates " ++ showSep "\n"
76 (map (\ (p, u) -> show u ++ " " ++ show p) newPats'))
77 (map (\ (p, u) -> show u ++ " " ++ show p) newPats'))
77 return (map snd newPats')
78 return (map snd newPats')
78
79
79data MergeState = MS { namemap :: [(Name, Name)],
80data MergeState = MS { namemap :: [(Name, Name)],
81+ invented :: [(Name, Name)],
82+ explicit :: [Name],
80 updates :: [(Name, PTerm)] }
83 updates :: [(Name, PTerm)] }
81
84
82addUpdate n tm = do ms <- get
85addUpdate n tm = do ms <- get
83 put (ms { updates = ((n, stripNS tm) : updates ms) } )
86 put (ms { updates = ((n, stripNS tm) : updates ms) } )
84
87
88+inventName ist ty n =
89+ do ms <- get
90+ let supp = case ty of
91+ Nothing -> []
92+ Just t -> getNameHints ist t
93+ let nsupp = case n of
94+ MN i ('_':_) -> mkSupply (supp ++ varlist)
95+ MN i n -> mkSupply (UN n : supp ++ varlist)
96+ x -> mkSupply (x : supp)
97+ let badnames = map snd (namemap ms) ++ map snd (invented ms) ++
98+ explicit ms
99+ case lookup n (invented ms) of
100+ Just n' -> return n'
101+ Nothing ->
102+ do let n' = uniqueNameFrom nsupp badnames
103+ put (ms { invented = (n, n') : invented ms })
104+ return n'
105+
106+mkSupply ns = mkSupply' ns (map nextName ns)
107+ where mkSupply' xs ns' = xs ++ mkSupply ns'
108+
109+varlist = map (UN . (:[])) "xyzwstuv" -- EB's personal preference :)
110+
85stripNS tm = mapPT dens tm where
111stripNS tm = mapPT dens tm where
86 dens (PRef fc n) = PRef fc (nsroot n)
112 dens (PRef fc n) = PRef fc (nsroot n)
87 dens t = t
113 dens t = t
88
114
89−mergeAllPats :: Context -> PTerm -> [PTerm] -> [(PTerm, [(Name, PTerm)])]
115+mergeAllPats :: IState -> Name -> PTerm -> [PTerm] -> [(PTerm, [(Name, PTerm)])]
90−mergeAllPats ctxt t [] = []
116+mergeAllPats ist cv t [] = []
91−mergeAllPats ctxt t (p : ps)
117+mergeAllPats ist cv t (p : ps)
92− = let (p', MS _ u) = runState (mergePat ctxt t p) (MS [] [])
118+ = let (p', MS _ _ _ u) = runState (mergePat ist t p Nothing)
119+ (MS [] [] (filter (/=cv) (patvars t)) [])
93− ps' = mergeAllPats ctxt t ps in
120+ ps' = mergeAllPats ist cv t ps in
94− ((p, u) : ps')
121+ ((p', u) : ps')
95−
122+ where patvars (PRef _ n) = [n]
123+ patvars (PApp _ _ as) = concatMap (patvars . getTm) as
124+ patvars (PPatvar _ n) = [n]
125+ patvars _ = []
126+
96−mergePat :: Context -> PTerm -> PTerm -> State MergeState PTerm
127+mergePat :: IState -> PTerm -> PTerm -> Maybe Name -> State MergeState PTerm
97-- If any names are unified, make sure they stay unified. Always prefer
128-- If any names are unified, make sure they stay unified. Always prefer
98-- user provided name (first pattern)
129-- user provided name (first pattern)
99−mergePat ctxt (PPatvar fc n) new
130+mergePat ist (PPatvar fc n) new t
100− = mergePat ctxt (PRef fc n) new
131+ = mergePat ist (PRef fc n) new t
101−mergePat ctxt old (PPatvar fc n)
132+mergePat ist old (PPatvar fc n) t
102− = mergePat ctxt old (PRef fc n)
133+ = mergePat ist old (PRef fc n) t
103−mergePat ctxt orig@(PRef fc n) new@(PRef _ n')
134+mergePat ist orig@(PRef fc n) new@(PRef _ n') t
104− | isDConName n' ctxt = do addUpdate n new;
135+ | isDConName n' (tt_ctxt ist) = do addUpdate n new
105− return new
136+ return new
106 | otherwise
137 | otherwise
107 = do ms <- get
138 = do ms <- get
108 case lookup n' (namemap ms) of
139 case lookup n' (namemap ms) of
@@ -110,36 +141,49 @@ mergePat ctxt orig@(PRef fc n) new@(PRef _ n')
110 return (PRef fc x)
141 return (PRef fc x)
111 Nothing -> do put (ms { namemap = ((n', n) : namemap ms) })
142 Nothing -> do put (ms { namemap = ((n', n) : namemap ms) })
112 return (PRef fc n)
143 return (PRef fc n)
113−mergePat ctxt (PApp _ _ args) (PApp fc f args')
144+mergePat ist (PApp _ _ args) (PApp fc f args') t
114− = do newArgs <- zipWithM mergeArg args args'
145+ = do newArgs <- zipWithM mergeArg args (zip args' (argTys ist f))
115 return (PApp fc f newArgs)
146 return (PApp fc f newArgs)
147+ where mergeArg x (y, t)
116− where mergeArg x y = do tm' <- mergePat ctxt (getTm x) (getTm y)
148+ = do tm' <- mergePat ist (getTm x) (getTm y) t
117− case x of
149+ case x of
118− (PImp _ _ _ _ _ _) ->
150+ (PImp _ _ _ _ _ _) ->
119− return (y { machine_inf = machine_inf x,
151+ return (y { machine_inf = machine_inf x,
120− getTm = tm' })
152+ getTm = tm' })
121− _ -> return (y { getTm = tm' })
153+ _ -> return (y { getTm = tm' })
122−mergePat ctxt (PRef fc n) t = do tm <- tidy t
154+mergePat ist (PRef fc n) tm ty = do tm <- tidy ist tm ty
123− addUpdate n tm
155+ addUpdate n tm
124− return tm
156+ return tm
125−mergePat ctxt x y = return y
157+mergePat ist x y t = return y
126
158
127mergeUserImpl :: PTerm -> PTerm -> PTerm
159mergeUserImpl :: PTerm -> PTerm -> PTerm
128mergeUserImpl x y = x
160mergeUserImpl x y = x
129
161
162+argTys :: IState -> PTerm -> [Maybe Name]
163+argTys ist (PRef fc n)
164+ = case lookupTy n (tt_ctxt ist) of
165+ [ty] -> map (tyName . snd) (getArgTys ty) ++ repeat Nothing
166+ _ -> repeat Nothing
167+ where tyName (Bind _ (Pi _) _) = Just (UN "->")
168+ tyName t | (P _ n _, _) <- unApply t = Just n
169+ | otherwise = Nothing
170+argTys _ _ = repeat Nothing
171+
172+tidy :: IState -> PTerm -> Maybe Name -> State MergeState PTerm
130−tidy orig@(PRef fc n)
173+tidy ist orig@(PRef fc n) ty
131 = do ms <- get
174 = do ms <- get
132 case lookup n (namemap ms) of
175 case lookup n (namemap ms) of
133 Just x -> return (PRef fc x)
176 Just x -> return (PRef fc x)
134 Nothing -> case n of
177 Nothing -> case n of
135 (UN _) -> return orig
178 (UN _) -> return orig
136− _ -> return Placeholder
179+ _ -> do n' <- inventName ist ty n
180+ return (PRef fc n')
137−tidy (PApp fc f args)
181+tidy ist (PApp fc f args) ty
138− = do args' <- mapM tidyArg args
182+ = do args' <- zipWithM tidyArg args (argTys ist f)
139 return (PApp fc f args')
183 return (PApp fc f args')
140− where tidyArg x = do tm' <- tidy (getTm x)
184+ where tidyArg x ty' = do tm' <- tidy ist (getTm x) ty'
141− return (x { getTm = tm' })
185+ return (x { getTm = tm' })
142−tidy tm = return tm
186+tidy ist tm ty = return tm
143
187
144
188
145-- mapPT tidyVar tm
189-- mapPT tidyVar tm
@@ -177,17 +221,17 @@ replaceVar ctxt n t (PApp fc f pats) = PApp fc f (map substArg pats)
177 subst (PApp fc (PRef _ t) pats)
221 subst (PApp fc (PRef _ t) pats)
178 | isTConName t ctxt = Placeholder -- infer types
222 | isTConName t ctxt = Placeholder -- infer types
179 subst (PApp fc f pats) = PApp fc f (map substArg pats)
223 subst (PApp fc f pats) = PApp fc f (map substArg pats)
180− subst (PEq fc l r) = PEq fc (subst l) (subst r)
224+ subst (PEq fc l r) = Placeholder -- PEq fc (subst l) (subst r)
181 subst x = x
225 subst x = x
182
226
183 substArg arg = arg { getTm = subst (getTm arg) }
227 substArg arg = arg { getTm = subst (getTm arg) }
184
228
185replaceVar ctxt n t pat = pat
229replaceVar ctxt n t pat = pat
186
230
187−splitOnLine :: Int -- ^ line number
231+splitOnLine :: Int -- ^ line number
188− -> Name -- ^ variable
232+ -> Name -- ^ variable
189− -> FilePath -- ^ name of file
233+ -> FilePath -- ^ name of file
190− -> Idris [[(Name, PTerm)]]
234+ -> Idris [[(Name, PTerm)]]
191splitOnLine l n fn = do
235splitOnLine l n fn = do
192-- let (before, later) = splitAt (l-1) (lines inp)
236-- let (before, later) = splitAt (l-1) (lines inp)
193-- i <- getIState
237-- i <- getIState
@@ -201,7 +245,7 @@ replaceSplits :: String -> [[(Name, PTerm)]] -> Idris [String]
201replaceSplits l ups = updateRHSs 1 (map (rep (expandBraces l)) ups)
245replaceSplits l ups = updateRHSs 1 (map (rep (expandBraces l)) ups)
202 where
246 where
203 rep str [] = str ++ "\n"
247 rep str [] = str ++ "\n"
204− rep str ((n, tm) : ups) = rep (updatePat False (show n) (nshow False tm) str) ups
248+ rep str ((n, tm) : ups) = rep (updatePat False (show n) (nshow tm) str) ups
205
249
206 updateRHSs i [] = return []
250 updateRHSs i [] = return []
207 updateRHSs i (x : xs) = do (x', i') <- updateRHS i x
251 updateRHSs i (x : xs) = do (x', i') <- updateRHS i x
@@ -220,11 +264,10 @@ replaceSplits l ups = updateRHSs 1 (map (rep (expandBraces l)) ups)
220
264
221 -- TMP HACK: If there are Nats, we don't want to show as numerals since
265 -- TMP HACK: If there are Nats, we don't want to show as numerals since
222 -- this isn't supported in a pattern, so special case here
266 -- this isn't supported in a pattern, so special case here
223− nshow brack (PRef _ (UN "Z")) = "Z"
267+ nshow (PRef _ (UN "Z")) = "Z"
224− nshow brack (PApp _ (PRef _ (UN "S")) [x]) =
268+ nshow (PApp _ (PRef _ (UN "S")) [x]) =
225− if brack then "(S " else "S " ++ nshow True (getTm x) ++
269+ "S " ++ addBrackets (nshow (getTm x))
226− if brack then ")" else ""
227− nshow _ t = show t
270+ nshow t = show t
228
271
229 -- if there's any {n} replace with {n=n}
272 -- if there's any {n} replace with {n=n}
230 expandBraces ('{' : xs)
273 expandBraces ('{' : xs)
@@ -242,9 +285,9 @@ replaceSplits l ups = updateRHSs 1 (map (rep (expandBraces l)) ups)
242 '{' : space ++ updatePat False n tm rest'
285 '{' : space ++ updatePat False n tm rest'
243 updatePat True n tm xs@(c:rest) | length xs > length n
286 updatePat True n tm xs@(c:rest) | length xs > length n
244 = let (before, after@(next:_)) = splitAt (length n) xs in
287 = let (before, after@(next:_)) = splitAt (length n) xs in
245− if (before == n && not (isAlpha next))
288+ if (before == n && not (isAlphaNum next))
246 then addBrackets tm ++ updatePat False n tm after
289 then addBrackets tm ++ updatePat False n tm after
247− else c : updatePat (not (isAlpha c)) n tm rest
290+ else c : updatePat (not (isAlphaNum c)) n tm rest
248 updatePat start n tm (c:rest) = c : updatePat (not (isAlpha c)) n tm rest
291 updatePat start n tm (c:rest) = c : updatePat (not (isAlpha c)) n tm rest
249
292
250 addBrackets tm | ' ' `elem` tm = "(" ++ tm ++ ")"
293 addBrackets tm | ' ' `elem` tm = "(" ++ tm ++ ")"
@@ -263,25 +306,37 @@ nameRoot acc nm =
263 (before, ('_' : after)) -> nameRoot (acc ++ [before]) after
306 (before, ('_' : after)) -> nameRoot (acc ++ [before]) after
264 _ -> showSep "_" (acc ++ [nm])
307 _ -> showSep "_" (acc ++ [nm])
265
308
266−getClause :: Int -> -- ^ Line type is declared on
309+getClause :: Int -- ^ line number that the type is declared on
267− Name -> -- ^ Function name
310+ -> Name -- ^ Function name
268− FilePath -> -- ^ Source file name
311+ -> FilePath -- ^ Source file name
269− Idris String
312+ -> Idris String
270getClause l fn fp = do ty <- getInternalApp fp l
313getClause l fn fp = do ty <- getInternalApp fp l
314+ ist <- get
271− let ap = mkApp ty [1..]
315+ let ap = mkApp ist ty []
272 return (show fn ++ " " ++ ap ++
316 return (show fn ++ " " ++ ap ++
273 "= ?" ++ show fn ++ "_rhs")
317 "= ?" ++ show fn ++ "_rhs")
274− where mkApp (PPi (Exp _ _ _ False) (MN _ _) _ sc) (n : ns)
318+ where mkApp i (PPi (Exp _ _ _ False) (MN _ _) ty sc) used
319+ = let n = getNameFrom i used ty in
275− = "x" ++ show n ++ " " ++ mkApp sc ns
320+ show n ++ " " ++ mkApp i sc (n : used)
276− mkApp (PPi (Exp _ _ _ False) n _ sc) ns
321+ mkApp i (PPi (Exp _ _ _ False) n _ sc) used
277− = show n ++ " " ++ mkApp sc ns
322+ = show n ++ " " ++ mkApp i sc (n : used)
278− mkApp (PPi _ _ _ sc) ns = mkApp sc ns
323+ mkApp i (PPi _ _ _ sc) used = mkApp i sc used
279− mkApp _ _ = ""
324+ mkApp i _ _ = ""
280−
325+
326+ getNameFrom i used (PPi _ _ _ _)
327+ = uniqueNameFrom (mkSupply [UN "f", UN "g"]) used
328+ getNameFrom i used (PApp fc f as) = getNameFrom i used f
329+ getNameFrom i used (PEq _ _ _) = uniqueNameFrom [UN "prf"] used
330+ getNameFrom i used (PRef fc f)
331+ = case getNameHints i f of
332+ [] -> uniqueName (UN "x") used
333+ ns -> uniqueNameFrom (mkSupply ns) used
334+ getNameFrom i used _ = uniqueName (UN "x") used
335+
281−getProofClause :: Int -> -- ^ Line type is declared on
336+getProofClause :: Int -- ^ line number that the type is declared
282− Name -> -- ^ Function name
337+ -> Name -- ^ Function name
283− FilePath -> -- ^ Source file name
338+ -> FilePath -- ^ Source file name
284− Idris String
339+ -> Idris String
285getProofClause l fn fp
340getProofClause l fn fp
286 = do ty <- getInternalApp fp l
341 = do ty <- getInternalApp fp l
287 return (mkApp ty ++ " = ?" ++ show fn ++ "_rhs")
342 return (mkApp ty ++ " = ?" ++ show fn ++ "_rhs")
@@ -292,19 +347,34 @@ getProofClause l fn fp
292-- match clause
347-- match clause
293
348
294mkWith :: String -> Name -> String
349mkWith :: String -> Name -> String
295−mkWith str n = let ind = getIndent str
296− str' = replicate ind ' ' ++
297− replaceRHS str "with (_)"
350+mkWith str n = let str' = replaceRHS str "with (_)"
298− newpat = replicate (ind + 2) ' ' ++
351+ newpat = " " ++
299 replaceRHS str "| with_pat = ?" ++ show n ++ "_rhs" in
352 replaceRHS str "| with_pat = ?" ++ show n ++ "_rhs" in
300 str' ++ "\n" ++ newpat
353 str' ++ "\n" ++ newpat
301
354
302− where getIndent s = length (takeWhile isSpace s)
303−
304− replaceRHS [] str = str
355+ where replaceRHS [] str = str
305 replaceRHS ('?':'=': rest) str = str
356 replaceRHS ('?':'=': rest) str = str
306 replaceRHS ('=': rest) str
357 replaceRHS ('=': rest) str
307 | not ('=' `elem` rest) = str
358 | not ('=' `elem` rest) = str
308 replaceRHS (x : rest) str = x : replaceRHS rest str
359 replaceRHS (x : rest) str = x : replaceRHS rest str
309
360
361+-- Replace _ with names in missing clauses
362+
363+nameMissing :: [PTerm] -> Idris [PTerm]
364+nameMissing ps = do ist <- get
365+ newPats <- mapM nm ps
366+ let newPats' = mergeAllPats ist (UN "_") (base (head ps))
367+ newPats
368+ return (map fst newPats')
369+ where
370+ base (PApp fc f args) = PApp fc f (map (fmap (const (PRef fc (UN "_")))) args)
371+ base t = t
372+
373+ nm ptm = do mptm <- elabNewPat ptm
374+ case mptm of
375+ Nothing -> return ptm
376+ Just ptm' -> return ptm'
377+
378+
379+
310
380
src/Idris/Completion.hs+1
@@ -38,6 +38,7 @@ tacticArgs = [ ("intro", Nothing) -- FIXME syntax for intro (fresh name)
38 , ("let", Nothing) -- FIXME syntax for let
38 , ("let", Nothing) -- FIXME syntax for let
39 , ("focus", Just ExprTArg)
39 , ("focus", Just ExprTArg)
40 , ("exact", Just ExprTArg)
40 , ("exact", Just ExprTArg)
41+ , ("equiv", Just ExprTArg)
41 , ("applyTactic", Just ExprTArg)
42 , ("applyTactic", Just ExprTArg)
42 , ("reflect", Just ExprTArg)
43 , ("reflect", Just ExprTArg)
43 , ("fill", Just ExprTArg)
44 , ("fill", Just ExprTArg)
src/Idris/Core/Elaborate.hs+5−2
@@ -305,6 +305,9 @@ expandLet n v = processTactic' (ExpandLet n v)
305rewrite :: Raw -> Elab' aux ()
305rewrite :: Raw -> Elab' aux ()
306rewrite tm = processTactic' (Rewrite tm)
306rewrite tm = processTactic' (Rewrite tm)
307
307
308+induction :: Name -> Elab' aux ()
309+induction nm = processTactic' (Induction nm)
310+
308equiv :: Raw -> Elab' aux ()
311equiv :: Raw -> Elab' aux ()
309equiv tm = processTactic' (Equiv tm)
312equiv tm = processTactic' (Equiv tm)
310
313
@@ -392,7 +395,7 @@ prepare_apply fn imps =
392 = do ctxt <- get_context
395 = do ctxt <- get_context
393 case lookupTy n ctxt of
396 case lookupTy n ctxt of
394 [] -> lift $ tfail $ NoSuchVariable n
397 [] -> lift $ tfail $ NoSuchVariable n
395− _ -> fail $ "Too many arguments for " ++ show fn
398+ _ -> lift $ tfail $ TooManyArguments n
396 | otherwise = fail $ "Too many arguments for " ++ show fn
399 | otherwise = fail $ "Too many arguments for " ++ show fn
397
400
398 doClaim ((i, _), n, t) = do claim n t
401 doClaim ((i, _), n, t) = do claim n t
@@ -419,7 +422,6 @@ apply' fillt fn imps =
419 do args <- prepare_apply fn (map fst imps)
422 do args <- prepare_apply fn (map fst imps)
420 env <- get_env
423 env <- get_env
421 g <- goal
424 g <- goal
422− fillt (raw_apply fn (map Var args))
423 -- _Don't_ solve the arguments we're specifying by hand.
425 -- _Don't_ solve the arguments we're specifying by hand.
424 -- (remove from unified list before calling end_unify)
426 -- (remove from unified list before calling end_unify)
425 -- HMMM: Actually, if we get it wrong, the typechecker will complain!
427 -- HMMM: Actually, if we get it wrong, the typechecker will complain!
@@ -439,6 +441,7 @@ apply' fillt fn imps =
439 keepGiven dont hunis hs
441 keepGiven dont hunis hs
440 put (ES (p { dontunify = dont, unified = (n, unify),
442 put (ES (p { dontunify = dont, unified = (n, unify),
441 notunified = notunify ++ notunified p }, a) s prev)
443 notunified = notunify ++ notunified p }, a) s prev)
444+ fillt (raw_apply fn (map Var args))
442 ptm <- get_term
445 ptm <- get_term
443 g <- goal
446 g <- goal
444-- trace ("Goal " ++ show g ++ "\n" ++ show (fn, imps, unify) ++ "\n" ++ show ptm) $
447-- trace ("Goal " ++ show g ++ "\n" ++ show (fn, imps, unify) ++ "\n" ++ show ptm) $
src/Idris/Core/Evaluate.hs+1−8
@@ -632,13 +632,6 @@ instance Show Def where
632 show ns' ++ " " ++ show sc' ++ "\n\n" ++
632 show ns' ++ " " ++ show sc' ++ "\n\n" ++
633 if inlc then "Inlinable\n" else "Not inlinable\n"
633 if inlc then "Inlinable\n" else "Not inlinable\n"
634
634
635−-- We need this for serialising Def. Fortunately, it never gets used because
636−-- we'll never serialise a primitive operator
637−
638−instance Binary (a -> b) where
639− put x = return ()
640− get = error "Getting a function"
641−
642-------
635-------
643
636
644-- Frozen => doesn't reduce
637-- Frozen => doesn't reduce
@@ -767,7 +760,7 @@ addCasedef n ci@(CaseInfo alwaysInline tcdict)
767 OK (CaseDef args_ct sc_ct _),
760 OK (CaseDef args_ct sc_ct _),
768 OK (CaseDef args_inl sc_inl _),
761 OK (CaseDef args_inl sc_inl _),
769 OK (CaseDef args_rt sc_rt _)) ->
762 OK (CaseDef args_rt sc_rt _)) ->
770− let inl = alwaysInline -- || tcdict
763+ let inl = alwaysInline -- tcdict
771 inlc = (inl || small n args_ct sc_ct) && (not asserted)
764 inlc = (inl || small n args_ct sc_ct) && (not asserted)
772 inlr = inl || small n args_rt sc_rt
765 inlr = inl || small n args_rt sc_rt
773 cdef = CaseDefs (args_tot, sc_tot)
766 cdef = CaseDefs (args_tot, sc_tot)
src/Idris/Core/ProofState.hs+57−20
@@ -69,6 +69,7 @@ data Tactic = Attack
69 | LetBind Name Raw Raw
69 | LetBind Name Raw Raw
70 | ExpandLet Name Term
70 | ExpandLet Name Term
71 | Rewrite Raw
71 | Rewrite Raw
72+ | Induction Name
72 | Equiv Raw
73 | Equiv Raw
73 | PatVar Name
74 | PatVar Name
74 | PatBind Name
75 | PatBind Name
@@ -566,28 +567,63 @@ rewrite tm ctxt env (Bind x (Hole t) xp@(P _ x' _)) | x == x' =
566 (scv, sct) <- lift $ check ctxt env sc
567 (scv, sct) <- lift $ check ctxt env sc
567 return scv
568 return scv
568 _ -> fail "Not an equality type"
569 _ -> fail "Not an equality type"
569− where
570− -- to make the P for rewrite, replace syntactic occurrences of l in ty with
571− -- an x, and put \x : lt in front
572− mkP lt l r ty | l == ty = lt
573− mkP lt l r (App f a) = let f' = if (r /= f) then mkP lt l r f else f
574− a' = if (r /= a) then mkP lt l r a else a in
575− App f' a'
576− mkP lt l r (Bind n b sc)
577− = let b' = mkPB b
578− sc' = if (r /= sc) then mkP lt l r sc else sc in
579− Bind n b' sc'
580− where mkPB (Let t v) = let t' = if (r /= t) then mkP lt l r t else t
581− v' = if (r /= v) then mkP lt l r v else v in
582− Let t' v'
583− mkPB b = let ty = binderTy b
584− ty' = if (r /= ty) then mkP lt l r ty else ty in
585− b { binderTy = ty' }
586− mkP lt l r x = x
587−
588− rname = MN 0 "replaced"
570+ where rname = MN 0 "replaced"
589rewrite _ _ _ _ = fail "Can't rewrite here"
571rewrite _ _ _ _ = fail "Can't rewrite here"
590
572
573+-- To make the P for rewrite, replace syntactic occurrences of l in ty with
574+-- an x, and put \x : lt in front
575+mkP :: TT Name -> TT Name -> TT Name -> TT Name -> TT Name
576+mkP lt l r ty | l == ty = lt
577+mkP lt l r (App f a) = let f' = if (r /= f) then mkP lt l r f else f
578+ a' = if (r /= a) then mkP lt l r a else a in
579+ App f' a'
580+mkP lt l r (Bind n b sc)
581+ = let b' = mkPB b
582+ sc' = if (r /= sc) then mkP lt l r sc else sc in
583+ Bind n b' sc'
584+ where mkPB (Let t v) = let t' = if (r /= t) then mkP lt l r t else t
585+ v' = if (r /= v) then mkP lt l r v else v in
586+ Let t' v'
587+ mkPB b = let ty = binderTy b
588+ ty' = if (r /= ty) then mkP lt l r ty else ty in
589+ b { binderTy = ty' }
590+mkP lt l r x = x
591+
592+induction :: Name -> RunTactic
593+induction nm ctxt env (Bind x (Hole t) (P _ x' _)) | x == x' = do
594+ (tmv, tmt) <- lift $ check ctxt env (Var nm)
595+ let tmt' = normalise ctxt env tmt
596+ case unApply tmt' of
597+ (P _ tnm _, pms@[]) -> do
598+ case lookupTy (SN (ElimN tnm)) ctxt of
599+ [elimTy] -> do
600+ let args = getArgTys elimTy
601+ let pmargs = take (length pms) args -- TODO: Fill these correctly when having multiple parameters working
602+ let args' = drop (length pms) args
603+ let propTy = head args'
604+ let consargs = init $ tail args -- TODO: This is incorrect when type has indicies, get indicies and use the correct count
605+ let scr = last $ tail args
606+ let prop = Bind nm (Lam tmt') t -- TODO: Make this work for types with indicies
607+ let res = substV prop $ bindConsArgs consargs (mkApp (P Ref (SN (ElimN tnm)) (TType (UVal 0))) ([prop] ++ map makeConsArg consargs ++ [tmv]))
608+ action (\ps -> ps {holes = holes ps \\ [x]})
609+ mapM_ addConsHole (reverse consargs)
610+ let res' = forget $ res
611+ (scv, sct) <- lift $ check ctxt env res'
612+ let scv' = specialise ctxt env [] scv
613+ return scv'
614+ [] -> fail $ "Induction needs an eliminator for " ++ show nm
615+ xs -> fail $ "Multiple definitions found when searching for the eliminator of " ++ show nm
616+ (P _ nm _, _) -> fail "Induction not yet supported for types with arguments"
617+ _ -> fail "Unkown type for induction"
618+ where scname = MN 0 "scarg"
619+ makeConsArg (nm, ty) = P Bound nm ty
620+ bindConsArgs ((nm, ty):args) v = Bind nm (Hole ty) $ bindConsArgs args v
621+ bindConsArgs [] v = v
622+ addConsHole (nm, ty) =
623+ action (\ps -> ps { holes = nm : holes ps })
624+induction tm ctxt env _ = do fail "Can't do induction here"
625+
626+
591equiv :: Raw -> RunTactic
627equiv :: Raw -> RunTactic
592equiv tm ctxt env (Bind x (Hole t) sc) =
628equiv tm ctxt env (Bind x (Hole t) sc) =
593 do (tmv, tmt) <- lift $ check ctxt env tm
629 do (tmv, tmt) <- lift $ check ctxt env tm
@@ -819,6 +855,7 @@ process t h = tactic (Just h) (mktac t)
819 mktac (LetBind n t v) = letbind n t v
855 mktac (LetBind n t v) = letbind n t v
820 mktac (ExpandLet n b) = expandLet n b
856 mktac (ExpandLet n b) = expandLet n b
821 mktac (Rewrite t) = rewrite t
857 mktac (Rewrite t) = rewrite t
858+ mktac (Induction t) = induction t
822 mktac (Equiv t) = equiv t
859 mktac (Equiv t) = equiv t
823 mktac (PatVar n) = patvar n
860 mktac (PatVar n) = patvar n
824 mktac (PatBind n) = patbind n
861 mktac (PatBind n) = patbind n
src/Idris/Core/TT.hs+15−6
@@ -85,6 +85,7 @@ data Err = Msg String
85 | UnifyScope Name Name Term [(Name, Type)]
85 | UnifyScope Name Name Term [(Name, Type)]
86 | CantInferType String
86 | CantInferType String
87 | NonFunctionType Term Term
87 | NonFunctionType Term Term
88+ | TooManyArguments Name
88 | CantIntroduce Term
89 | CantIntroduce Term
89 | NoSuchVariable Name
90 | NoSuchVariable Name
90 | NoTypeDecl Name
91 | NoTypeDecl Name
@@ -237,6 +238,7 @@ data SpecialName = WhereN Int Name Name
237 | ParentN Name String
238 | ParentN Name String
238 | MethodN Name
239 | MethodN Name
239 | CaseN Name
240 | CaseN Name
241+ | ElimN Name
240 deriving (Eq, Ord)
242 deriving (Eq, Ord)
241{-!
243{-!
242deriving instance Binary SpecialName
244deriving instance Binary SpecialName
@@ -269,19 +271,21 @@ instance Show SpecialName where
269 show (MethodN m) = "method " ++ show m
271 show (MethodN m) = "method " ++ show m
270 show (ParentN p c) = show p ++ "#" ++ c
272 show (ParentN p c) = show p ++ "#" ++ c
271 show (CaseN n) = "case block in " ++ show n
273 show (CaseN n) = "case block in " ++ show n
274+ show (ElimN n) = "<<" ++ show n ++ " eliminator>>"
272
275
273-- Show a name in a way decorated for code generation, not human reading
276-- Show a name in a way decorated for code generation, not human reading
274showCG :: Name -> String
277showCG :: Name -> String
275showCG (UN n) = n
278showCG (UN n) = n
276−showCG (NS n s) = showSep "." (reverse s) ++ "." ++ show n
279+showCG (NS n s) = showSep "." (reverse s) ++ "." ++ showCG n
277showCG (MN _ "underscore") = "_"
280showCG (MN _ "underscore") = "_"
278showCG (MN i s) = "{" ++ s ++ show i ++ "}"
281showCG (MN i s) = "{" ++ s ++ show i ++ "}"
279showCG (SN s) = showCG' s
282showCG (SN s) = showCG' s
280− where showCG' (WhereN i p c) = show p ++ ":" ++ show c ++ ":" ++ show i
283+ where showCG' (WhereN i p c) = showCG p ++ ":" ++ showCG c ++ ":" ++ show i
281− showCG' (InstanceN cl inst) = '@':show cl ++ '$':showSep ":" inst
284+ showCG' (InstanceN cl inst) = '@':showCG cl ++ '$':showSep ":" inst
282− showCG' (MethodN m) = '!':show m
285+ showCG' (MethodN m) = '!':showCG m
283− showCG' (ParentN p c) = show p ++ "#" ++ show c
286+ showCG' (ParentN p c) = showCG p ++ "#" ++ show c
284− showCG' (CaseN c) = show c ++ "_case"
287+ showCG' (CaseN c) = showCG c ++ "_case"
288+ showCG' (ElimN sn) = showCG sn ++ "_elim"
285showCG NErased = "_"
289showCG NErased = "_"
286
290
287
291
@@ -831,6 +835,11 @@ getRetTy (Bind n (PVTy _) sc) = getRetTy sc
831getRetTy (Bind n (Pi _) sc) = getRetTy sc
835getRetTy (Bind n (Pi _) sc) = getRetTy sc
832getRetTy sc = sc
836getRetTy sc = sc
833
837
838+uniqueNameFrom :: [Name] -> [Name] -> Name
839+uniqueNameFrom (s : supply) hs
840+ | s `elem` hs = uniqueNameFrom supply hs
841+ | otherwise = s
842+
834uniqueName :: Name -> [Name] -> Name
843uniqueName :: Name -> [Name] -> Name
835uniqueName n hs | n `elem` hs = uniqueName (nextName n) hs
844uniqueName n hs | n `elem` hs = uniqueName (nextName n) hs
836 | otherwise = n
845 | otherwise = n
src/Idris/Coverage.hs−4
@@ -198,10 +198,6 @@ genAll i args
198 = PPair fc (getTm l) (getTm r)
198 = PPair fc (getTm l) (getTm r)
199 resugar t = t
199 resugar t = t
200
200
201− getForceable i n = case lookupCtxt n (idris_optimisation i) of
202− [o] -> forceable o
203− _ -> []
204−
205 dropForce force (x : xs) i | i `elem` force
201 dropForce force (x : xs) i | i `elem` force
206 = upd Placeholder x : dropForce force xs (i + 1)
202 = upd Placeholder x : dropForce force xs (i + 1)
207 dropForce force (x : xs) i = x : dropForce force xs (i + 1)
203 dropForce force (x : xs) i = x : dropForce force xs (i + 1)
src/Idris/DataOpts.hs+160−158
@@ -5,78 +5,118 @@ module Idris.DataOpts where
5-- Forcing, detagging and collapsing
5-- Forcing, detagging and collapsing
6
6
7import Idris.AbsSyntax
7import Idris.AbsSyntax
8+import Idris.AbsSyntaxTree
8import Idris.Core.TT
9import Idris.Core.TT
9
10
11+import Control.Applicative
12+import qualified Data.IntMap as M
10import Data.List
13import Data.List
11import Data.Maybe
14import Data.Maybe
12import Debug.Trace
15import Debug.Trace
13
16
17+type ForceMap = M.IntMap Forceability
18+
14−-- Calculate the forceable arguments to a constructor and update the set of
19+-- Calculate the forceable arguments to a constructor
15−-- optimisations
20+-- and update the set of optimisations.
16−
17−forceArgs :: Name -> Type -> Idris ()
21+forceArgs :: Name -> Name -> Type -> Idris ()
18−forceArgs n t = do i <- getIState
22+forceArgs typeName n t = do
19− let fargs = force i 0 t
23+ ist <- getIState
24+ let fargs = getForcedArgs ist typeName t
20− copt <- case lookupCtxt n (idris_optimisation i) of
25+ copt = case lookupCtxt n (idris_optimisation ist) of
21− [] -> return $ Optimise False False [] []
26+ [] -> Optimise False False [] []
22− (op:_) -> return op
27+ op:_ -> op
23− let opts = addDef n (copt { forceable = fargs }) (idris_optimisation i)
28+ opts = addDef n (copt { forceable = M.toList fargs }) (idris_optimisation ist)
24− putIState (i { idris_optimisation = opts })
29+ putIState (ist { idris_optimisation = opts })
25− addIBC (IBCOpt n)
30+ addIBC (IBCOpt n)
26− iLOG $ "Forced: " ++ show n ++ " " ++ show fargs ++ "\n from " ++
31+ iLOG $ "Forced: " ++ show n ++ " " ++ show fargs ++ "\n from " ++ show t
27− show t
32+
33+getForcedArgs :: IState -> Name -> Type -> ForceMap
34+getForcedArgs ist typeName t = addCollapsibleArgs 0 t $ forcedInTarget 0 t
28 where
35 where
29− force :: IState -> Int -> Term -> [Int]
36+ maxUnion = M.unionWith max
30− force ist i (Bind _ (Pi ty) sc)
31− | collapsibleIn ist ty
32− = nub $ i : (force ist (i + 1) $ instantiate (P Bound (MN i "?") Erased) sc)
33− | otherwise = force ist (i + 1) $ instantiate (P Bound (MN i "?") Erased) sc
34− force _ _ sc@(App f a)
35− | (_, args) <- unApply sc
36− = nub $ concatMap guarded args
37− force _ _ _ = []
38−
39− collapsibleIn i t
40− | (P _ tn _, _) <- unApply t
41− = case lookupCtxt tn (idris_optimisation i) of
42− [oi] -> collapsible oi
43− _ -> False
44− | otherwise = False
45−
46− isF (P _ (MN force "?") _) = Just force
47− isF _ = Nothing
48−
49− guarded :: Term -> [Int]
50− guarded t@(App f a)
51−-- | (P (TCon _ _) _ _, args) <- unApply t
52−-- = mapMaybe isF args ++ concatMap guarded args
53− | (P (DCon _ _) _ _, args) <- unApply t
54− = mapMaybe isF args ++ concatMap guarded args
55− guarded t = mapMaybe isF [t]
56
37
57−-- Calculate whether a collection of constructors is collapsible
38+ -- Label all occurrences of the variable bound in Pi in the rest of
39+ -- the term with the number i so that we can recognize them anytime later.
40+ label i = instantiate $ P Bound (MN i "ctor_arg") Erased
41+
42+ addCollapsibleArgs :: Int -> Type -> ForceMap -> ForceMap
43+ addCollapsibleArgs i (Bind vn (Pi ty) rest) alreadyForceable
44+ = addCollapsibleArgs (i+1) (label i rest) (forceable $ unApply ty)
45+ where
46+ -- forceable takes an un-applied type of a ctor argument
47+ forceable (P _ tn _, args)
48+ -- if `ty' is collapsible, the argument is unconditionally forceable
49+ | isCollapsible tn
50+ = M.insert i Unconditional alreadyForceable
51+
52+ -- a recursive occurrence with known indices is conditionally forceable
53+ | tn == typeName
54+ = M.insertWith max i Conditional alreadyForceable
55+
56+ forceable _ = alreadyForceable
57+
58+ isCollapsible :: Name -> Bool
59+ isCollapsible n = case lookupCtxt n (idris_optimisation ist) of
60+ [oi] -> collapsible oi
61+ _ -> False
62+
63+ addCollapsibleArgs _ _ fs = fs
58
64
65+ forcedInTarget :: Int -> Type -> ForceMap
66+ forcedInTarget i (Bind _ (Pi _) rest) = forcedInTarget (i+1) (label i rest)
67+ forcedInTarget i t@(App f a) | (_, as) <- unApply t = unionMap guardedArgs as
68+ forcedInTarget _ _ = M.empty
69+
70+ guardedArgs :: Term -> ForceMap
71+ guardedArgs t@(App f a) | (P (DCon _ _) _ _, args) <- unApply t
72+ = unionMap bareArg args `maxUnion` unionMap guardedArgs args
73+ guardedArgs t = bareArg t
74+
75+ bareArg :: Term -> ForceMap
76+ bareArg (P _ (MN i "ctor_arg") _) = M.singleton i Unconditional
77+ bareArg _ = M.empty
78+
79+ unionMap :: (a -> ForceMap) -> [a] -> ForceMap
80+ unionMap f = M.unionsWith max . map f
81+
82+-- Calculate whether a collection of constructors is collapsible
83+-- and update the state accordingly.
59collapseCons :: Name -> [(Name, Type)] -> Idris ()
84collapseCons :: Name -> [(Name, Type)] -> Idris ()
60−collapseCons ty cons =
85+collapseCons tn ctors = do
61− do i <- getIState
86+ ist <- getIState
62− let cons' = map (\ (n, t) -> (n, map snd (getArgTys t))) cons
87+ case ctors of
63− allFR <- mapM (forceRec i) cons'
88+ _
64− if and allFR then detaggable (map getRetTy (map snd cons))
89+ | all (ctorCollapsible ist) ctors
90+ , disjointTerms ctorTargetArgs
91+ -> mapM_ setCollapsible (tn : map fst ctors)
92+
93+ [(cn, ct)]
65− else checkNewType cons'
94+ -> checkNewType ist cn ct
95+
96+ _ -> return () -- nothing can be done
66 where
97 where
98+ ctorTargetArgs = map (snd . unApply . getRetTy . snd) ctors
99+
100+ ctorArity :: Type -> Int
101+ ctorArity = length . getArgTys
102+
103+ ctorCollapsible :: IState -> (Name, Type) -> Bool
104+ ctorCollapsible ist (n, t) = all (`M.member` forceMap) [0 .. ctorArity t - 1]
105+ where
106+ forceMap = case lookupCtxt n (idris_optimisation ist) of
107+ oi:_ -> M.fromList $ forceable oi
108+ _ -> M.empty
109+
67 -- one constructor; if one remaining argument, treat as newtype
110 -- one constructor; if one remaining argument, treat as newtype
68− checkNewType [(n, ts)] = do
111+ checkNewType :: IState -> Name -> Type -> Idris ()
69− i <- getIState
112+ checkNewType ist cn ct
70− case lookupCtxt n (idris_optimisation i) of
113+ | oi:_ <- lookupCtxt cn opt
71− (oi:_) -> do let remaining = length ts - length (forceable oi)
114+ , length (getArgTys ct) == 1 + forcedCnt (M.fromList $ forceable oi)
72− if remaining == 1 then
115+ = putIState ist{ idris_optimisation = opt' oi }
116+ | otherwise = return ()
117+ where
118+ opt = idris_optimisation ist
73− do let oi' = oi { isnewtype = True }
119+ opt' oi = addDef cn oi{ isnewtype = True } opt
74− let opts = addDef n oi' (idris_optimisation i)
75− putIState (i { idris_optimisation = opts })
76− else return ()
77− _ -> return ()
78−
79− checkNewType _ = return ()
80
120
81 setCollapsible :: Name -> Idris ()
121 setCollapsible :: Name -> Idris ()
82 setCollapsible n
122 setCollapsible n
@@ -91,79 +131,49 @@ collapseCons ty cons =
91 putIState (i { idris_optimisation = opts })
131 putIState (i { idris_optimisation = opts })
92 addIBC (IBCOpt n)
132 addIBC (IBCOpt n)
93
133
94− forceRec :: IState -> (Name, [Type]) -> Idris Bool
134+ disjointTerms :: [[Term]] -> Bool
95− forceRec i (n, ts)
135+ disjointTerms [] = True
96− = case lookupCtxt n (idris_optimisation i) of
136+ disjointTerms [xs] = True
97− (oi:_) -> checkFR (forceable oi) 0 ts
137+ disjointTerms (xs : xss) =
98− _ -> return False
99− checkFR fs i [] = return True
100− checkFR fs i (_ : xs) | i `elem` fs = checkFR fs (i + 1) xs
101− checkFR fs i (t : xs)
102− -- must be recursive or type is not collapsible
103− = do let (rtf, rta) = unApply $ getRetTy t
104− if (ty `elem` freeNames rtf)
105− then checkFR fs (i+1) xs
106− else return False
107−
108− detaggable :: [Type] -> Idris ()
109− detaggable rtys
110− = do let rtyArgs = map (snd . unApply) rtys
111− -- if every rtyArgs is disjoint with every other, it's detaggable,
138+ -- xs is disjoint with every pattern from xss
112− -- therefore also collapsible given forceable/recursive check
139+ all (or . zipWith disjoint xs) xss
113− if disjoint rtyArgs
114− then mapM_ setCollapsible (ty : map fst cons)
115− else return ()
116−
117− disjoint :: [[Term]] -> Bool
118− disjoint [] = True
119− disjoint [x] = True
140+ -- and xss is pairwise disjoint, too
120− disjoint (x : xs) = anyDisjoint x xs && disjoint xs
141+ && disjointTerms xss
121−
142+
122− anyDisjoint x [] = True
143+ -- Return True if the two patterns are provably disjoint.
123− anyDisjoint x (y : ys) = disjointCons x y
144+ -- Return False if they're not or if unsure.
124−
145+ disjoint :: Term -> Term -> Bool
125− disjointCons [] [] = False
146+ disjoint x y = case (cx, cy) of
126− disjointCons [] y = False
147+ -- data constructors -> compare their names
127− disjointCons x [] = False
128− disjointCons (x : xs) (y : ys)
129− = disjointCon x y || disjointCons xs ys
130−
131− disjointCon x y = let (cx, _) = unApply x
132− (cy, _) = unApply y in
133− case (cx, cy) of
134− (P (DCon _ _) nx _, P (DCon _ _) ny _) -> nx /= ny
148+ (P (DCon _ _) nx _, P (DCon _ _) ny _)
149+ | nx /= ny -> True
150+ | otherwise -> or $ zipWith disjoint xargs yargs
135− _ -> False
151+ _ -> False
152+ where
153+ (cx, xargs) = unApply x
154+ (cy, yargs) = unApply y
136
155
137class Optimisable term where
156class Optimisable term where
138 applyOpts :: term -> Idris term
157 applyOpts :: term -> Idris term
139 stripCollapsed :: term -> Idris term
158 stripCollapsed :: term -> Idris term
140
159
141instance (Optimisable a, Optimisable b) => Optimisable (a, b) where
160instance (Optimisable a, Optimisable b) => Optimisable (a, b) where
142− applyOpts (x, y) = do x' <- applyOpts x
161+ applyOpts (x, y) = (,) <$> applyOpts x <*> applyOpts y
143− y' <- applyOpts y
144− return (x', y')
145− stripCollapsed (x, y) = do x' <- stripCollapsed x
162+ stripCollapsed (x, y) = (,) <$> stripCollapsed x <*> stripCollapsed y
146− y' <- stripCollapsed y
147− return (x', y')
148−
149
163
150instance (Optimisable a, Optimisable b) => Optimisable (vs, a, b) where
164instance (Optimisable a, Optimisable b) => Optimisable (vs, a, b) where
151− applyOpts (v, x, y) = do x' <- applyOpts x
165+ applyOpts (v, x, y) = (,,) v <$> applyOpts x <*> applyOpts y
152− y' <- applyOpts y
153− return (v, x', y')
154− stripCollapsed (v, x, y) = do x' <- stripCollapsed x
155− y' <- stripCollapsed y
166+ stripCollapsed (v, x, y) = (,,) v <$> stripCollapsed x <*> stripCollapsed y
156− return (v, x', y')
157
167
158instance Optimisable a => Optimisable [a] where
168instance Optimisable a => Optimisable [a] where
159 applyOpts = mapM applyOpts
169 applyOpts = mapM applyOpts
160 stripCollapsed = mapM stripCollapsed
170 stripCollapsed = mapM stripCollapsed
161
171
162instance Optimisable a => Optimisable (Either a (a, a)) where
172instance Optimisable a => Optimisable (Either a (a, a)) where
163− applyOpts (Left t) = do t' <- applyOpts t; return $ Left t'
173+ applyOpts (Left t) = Left <$> applyOpts t
164− applyOpts (Right t) = do t' <- applyOpts t; return $ Right t'
174+ applyOpts (Right t) = Right <$> applyOpts t
165− stripCollapsed (Left t) = do t' <- stripCollapsed t; return $ Left t'
175+ stripCollapsed (Left t) = Left <$> stripCollapsed t
166− stripCollapsed (Right t) = do t' <- stripCollapsed t; return $ Right t'
176+ stripCollapsed (Right t) = Right <$> stripCollapsed t
167
177
168-- Raw is for compile time optimisation (before type checking)
178-- Raw is for compile time optimisation (before type checking)
169-- Term is for run time optimisation (after type checking, collapsing allowed)
179-- Term is for run time optimisation (after type checking, collapsing allowed)
@@ -175,41 +185,39 @@ instance Optimisable Raw where
175 | (Var n, args) <- raw_unapply t -- MAGIC HERE
185 | (Var n, args) <- raw_unapply t -- MAGIC HERE
176 = do args' <- mapM applyOpts args
186 = do args' <- mapM applyOpts args
177 i <- getIState
187 i <- getIState
178− case lookupCtxt n (idris_optimisation i) of
188+ return $ case lookupCtxt n (idris_optimisation i) of
179− (oi:_) -> return $ applyDataOpt oi n args'
189+ oi:_ -> applyDataOpt oi n args'
180− _ -> return (raw_apply (Var n) args')
190+ _ -> raw_apply (Var n) args'
181− | otherwise = do f' <- applyOpts f
191+ | otherwise = RApp <$> applyOpts f <*> applyOpts a
182− a' <- applyOpts a
192+
183− return (RApp f' a')
184− applyOpts (RBind n b t) = do b' <- applyOpts b
193+ applyOpts (RBind n b t) = RBind n <$> applyOpts b <*> applyOpts t
185− t' <- applyOpts t
186− return (RBind n b' t')
187− applyOpts (RForce t) = applyOpts t
194+ applyOpts (RForce t) = applyOpts t
188 applyOpts t = return t
195 applyOpts t = return t
189
196
190 stripCollapsed t = return t
197 stripCollapsed t = return t
191
198
192instance Optimisable t => Optimisable (Binder t) where
199instance Optimisable t => Optimisable (Binder t) where
193− applyOpts (Let t v) = do t' <- applyOpts t
200+ applyOpts (Let t v) = Let <$> applyOpts t <*> applyOpts v
194− v' <- applyOpts v
195− return (Let t' v')
196 applyOpts b = do t' <- applyOpts (binderTy b)
201 applyOpts b = do t' <- applyOpts (binderTy b)
197 return (b { binderTy = t' })
202 return (b { binderTy = t' })
198− stripCollapsed (Let t v) = do t' <- stripCollapsed t
203+ stripCollapsed (Let t v) = Let <$> stripCollapsed t <*> stripCollapsed v
199− v' <- stripCollapsed v
200− return (Let t' v')
201 stripCollapsed b = do t' <- stripCollapsed (binderTy b)
204 stripCollapsed b = do t' <- stripCollapsed (binderTy b)
202 return (b { binderTy = t' })
205 return (b { binderTy = t' })
203
206
207+forcedArgSeq :: OptInfo -> [Maybe Forceability]
208+forcedArgSeq oi = map (\i -> M.lookup i forceMap) [0..]
209+ where
210+ forceMap = M.fromList $ forceable oi
211+
212+forcedCnt :: ForceMap -> Int
213+forcedCnt = length . filter (== Unconditional) . M.elems
204
214
205applyDataOpt :: OptInfo -> Name -> [Raw] -> Raw
215applyDataOpt :: OptInfo -> Name -> [Raw] -> Raw
206−applyDataOpt oi n args
216+applyDataOpt oi n args
207− = let args' = zipWith doForce (map (\x -> x `elem` (forceable oi)) [0..])
217+ = raw_apply (Var n) $ zipWith doForce (forcedArgSeq oi) args
208− args in
209− raw_apply (Var n) args'
210 where
218 where
211− doForce True a = RForce a
219+ doForce (Just Unconditional) a = RForce a
212− doForce False a = a
220+ doForce _ a = a
213
221
214-- Run-time: do everything
222-- Run-time: do everything
215
223
@@ -268,10 +276,10 @@ instance Optimisable (TT Name) where
268
276
269applyDataOptRT :: OptInfo -> Name -> Int -> Int -> [Term] -> Term
277applyDataOptRT :: OptInfo -> Name -> Int -> Int -> [Term] -> Term
270applyDataOptRT oi n tag arity args
278applyDataOptRT oi n tag arity args
271− | length args == arity = doOpts n args (collapsible oi) (forceable oi)
279+ | length args == arity = doOpts n args (collapsible oi) (M.fromList $ forceable oi)
272 | otherwise = let extra = satArgs (arity - length args)
280 | otherwise = let extra = satArgs (arity - length args)
273 tm = doOpts n (args ++ map (\n -> P Bound n Erased) extra)
281 tm = doOpts n (args ++ map (\n -> P Bound n Erased) extra)
274− (collapsible oi) (forceable oi) in
282+ (collapsible oi) (M.fromList $ forceable oi) in
275 bind extra tm
283 bind extra tm
276 where
284 where
277 satArgs n = map (\i -> MN i "sat") [1..n]
285 satArgs n = map (\i -> MN i "sat") [1..n]
@@ -285,18 +293,12 @@ applyDataOptRT oi n tag arity args
285 doOpts (NS (UN "S") ["Nat", "Prelude"]) [k] _ _
293 doOpts (NS (UN "S") ["Nat", "Prelude"]) [k] _ _
286 = App (App (P Ref (UN "prim__addBigInt") Erased) k) (Constant (BI 1))
294 = App (App (P Ref (UN "prim__addBigInt") Erased) k) (Constant (BI 1))
287
295
288− doOpts n args True f = Erased
296+ doOpts n args True _ = Erased
289− doOpts n args _ forced
297+ doOpts n args _ forceMap
290− = let args' = filter keep (zip (map (\x -> x `elem` forced) [0..])
291− args) in
292− if isnewtype oi
298+ | isnewtype oi = case args' of
293− then case args' of
294− [(_, val)] -> val
299+ [val] -> val
295− _ -> error "Can't happen (not isnewtype)"
300+ _ -> error $ "Can't happen (newtype not a singleton): " ++ show args'
296− else
301+ | otherwise = mkApp ctor' args'
302+ where
297− mkApp (P (DCon tag (arity - length forced)) n Erased)
303+ ctor' = (P (DCon tag (arity - forcedCnt forceMap)) n Erased)
298− (map snd args')
304+ args' = [t | (f, t) <- zip (forcedArgSeq oi) args, f /= Just Unconditional]
299−
300− keep (forced, _) = not forced
301−
302−
src/Idris/DeepSeq.hs+13−2
@@ -2,11 +2,16 @@ module Idris.DeepSeq where
2
2
3import Idris.Core.TT
3import Idris.Core.TT
4import Idris.AbsSyntax
4import Idris.AbsSyntax
5+import Idris.AbsSyntaxTree
5
6
6import Control.DeepSeq
7import Control.DeepSeq
7
8
8-- All generated by 'derive'
9-- All generated by 'derive'
9
10
11+instance NFData Forceability where
12+ rnf Conditional = ()
13+ rnf Unconditional = ()
14+
10instance NFData Raw where
15instance NFData Raw where
11 rnf (Var x1) = rnf x1 `seq` ()
16 rnf (Var x1) = rnf x1 `seq` ()
12 rnf (RBind x1 x2 x3) = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` ()
17 rnf (RBind x1 x2 x3) = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` ()
@@ -31,6 +36,7 @@ instance NFData SpecialName where
31 rnf (ParentN x1 x2) = rnf x1 `seq` rnf x2 `seq` ()
36 rnf (ParentN x1 x2) = rnf x1 `seq` rnf x2 `seq` ()
32 rnf (MethodN x1) = rnf x1 `seq` ()
37 rnf (MethodN x1) = rnf x1 `seq` ()
33 rnf (CaseN x1) = rnf x1 `seq` ()
38 rnf (CaseN x1) = rnf x1 `seq` ()
39+ rnf (ElimN x1) = rnf x1 `seq` ()
34
40
35instance NFData IntTy where
41instance NFData IntTy where
36 rnf (ITFixed x1) = rnf x1 `seq` ()
42 rnf (ITFixed x1) = rnf x1 `seq` ()
@@ -164,6 +170,10 @@ instance NFData FnOpt where
164 rnf Reflection = ()
170 rnf Reflection = ()
165 rnf (Specialise x1) = rnf x1 `seq` ()
171 rnf (Specialise x1) = rnf x1 `seq` ()
166
172
173+instance NFData DataOpt where
174+ rnf Codata = ()
175+ rnf DefaultEliminator = ()
176+
167instance (NFData t) => NFData (PDecl' t) where
177instance (NFData t) => NFData (PDecl' t) where
168 rnf (PFix x1 x2 x3) = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` ()
178 rnf (PFix x1 x2 x3) = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` ()
169 rnf (PTy x1 x2 x3 x4 x5 x6)
179 rnf (PTy x1 x2 x3 x4 x5 x6)
@@ -271,6 +281,7 @@ instance (NFData t) => NFData (PTactic' t) where
271 rnf (Focus x1) = rnf x1 `seq` ()
281 rnf (Focus x1) = rnf x1 `seq` ()
272 rnf (Refine x1 x2) = rnf x1 `seq` rnf x2 `seq` ()
282 rnf (Refine x1 x2) = rnf x1 `seq` rnf x2 `seq` ()
273 rnf (Rewrite x1) = rnf x1 `seq` ()
283 rnf (Rewrite x1) = rnf x1 `seq` ()
284+ rnf (Induction x1) = rnf x1 `seq` ()
274 rnf (Equiv x1) = rnf x1 `seq` ()
285 rnf (Equiv x1) = rnf x1 `seq` ()
275 rnf (MatchRefine x1) = rnf x1 `seq` ()
286 rnf (MatchRefine x1) = rnf x1 `seq` ()
276 rnf (LetTac x1 x2) = rnf x1 `seq` rnf x2 `seq` ()
287 rnf (LetTac x1 x2) = rnf x1 `seq` rnf x2 `seq` ()
@@ -315,9 +326,9 @@ instance (NFData t) => NFData (PArg' t) where
315 rnf x2 `seq` rnf x3 `seq` rnf x4 `seq` rnf x5 `seq` rnf x6 `seq` ()
326 rnf x2 `seq` rnf x3 `seq` rnf x4 `seq` rnf x5 `seq` rnf x6 `seq` ()
316
327
317instance NFData ClassInfo where
328instance NFData ClassInfo where
318− rnf (CI x1 x2 x3 x4 x5)
329+ rnf (CI x1 x2 x3 x4 x5 x6)
319 = rnf x1 `seq`
330 = rnf x1 `seq`
320− rnf x2 `seq` rnf x3 `seq` rnf x4 `seq` rnf x5 `seq` ()
331+ rnf x2 `seq` rnf x3 `seq` rnf x4 `seq` rnf x5 `seq` rnf x6 `seq` ()
321
332
322instance NFData OptInfo where
333instance NFData OptInfo where
323 rnf (Optimise x1 x2 x3 x4)
334 rnf (Optimise x1 x2 x3 x4)
src/Idris/Delaborate.hs+2
@@ -154,6 +154,8 @@ pshow i (NonFunctionType f ty)
154 let colour = idris_colourRepl i in
154 let colour = idris_colourRepl i in
155 showImp (Just i) imps colour (delab i f) ++ " does not have a function type ("
155 showImp (Just i) imps colour (delab i f) ++ " does not have a function type ("
156 ++ showImp (Just i) imps colour (delab i ty) ++ ")"
156 ++ showImp (Just i) imps colour (delab i ty) ++ ")"
157+pshow i (TooManyArguments f)
158+ = "Too many arguments for " ++ show f
157pshow i (CantIntroduce ty)
159pshow i (CantIntroduce ty)
158 = let imps = opt_showimp (idris_options i) in
160 = let imps = opt_showimp (idris_options i) in
159 let colour = idris_colourRepl i in
161 let colour = idris_colourRepl i in
src/Idris/ElabDecls.hs+354−34
@@ -33,6 +33,12 @@ import Data.List
33import Data.Maybe
33import Data.Maybe
34import Debug.Trace
34import Debug.Trace
35
35
36+import qualified Data.Map as Map
37+import Data.Char(isLetter, toLower)
38+import Data.List.Split (splitOn)
39+
40+import Util.Pretty(pretty)
41+
36recheckC fc env t
42recheckC fc env t
37 = do -- t' <- applyOpts (forget t) (doesn't work, or speed things up...)
43 = do -- t' <- applyOpts (forget t) (doesn't work, or speed things up...)
38 ctxt <- getContext
44 ctxt <- getContext
@@ -143,9 +149,10 @@ elabPostulate info syn doc fc opts n ty
143 -- remove it from the deferred definitions list
149 -- remove it from the deferred definitions list
144 solveDeferred n
150 solveDeferred n
145
151
146−elabData :: ElabInfo -> SyntaxInfo -> String -> FC -> Bool -> PData -> Idris ()
152+elabData :: ElabInfo -> SyntaxInfo -> String -> FC -> DataOpts -> PData -> Idris ()
147−elabData info syn doc fc codata (PLaterdecl n t_in)
153+elabData info syn doc fc opts (PLaterdecl n t_in)
154+ = do let codata = Codata `elem` opts
148− = do iLOG (show (fc, doc))
155+ iLOG (show (fc, doc))
149 checkUndefined fc n
156 checkUndefined fc n
150 ctxt <- getContext
157 ctxt <- getContext
151 i <- getIState
158 i <- getIState
@@ -161,8 +168,9 @@ elabData info syn doc fc codata (PLaterdecl n t_in)
161 logLvl 2 $ "---> " ++ show cty
168 logLvl 2 $ "---> " ++ show cty
162 updateContext (addTyDecl n (TCon 0 0) cty) -- temporary, to check cons
169 updateContext (addTyDecl n (TCon 0 0) cty) -- temporary, to check cons
163
170
164−elabData info syn doc fc codata (PDatadecl n t_in dcons)
171+elabData info syn doc fc opts (PDatadecl n t_in dcons)
172+ = do let codata = Codata `elem` opts
165− = do iLOG (show fc)
173+ iLOG (show fc)
166 undef <- isUndefined fc n
174 undef <- isUndefined fc n
167 ctxt <- getContext
175 ctxt <- getContext
168 i <- getIState
176 i <- getIState
@@ -173,6 +181,9 @@ elabData info syn doc fc codata (PDatadecl n t_in dcons)
173 (errAt "data declaration " n (erun fc (build i info False n t)))
181 (errAt "data declaration " n (erun fc (build i info False n t)))
174 def' <- checkDef fc defer
182 def' <- checkDef fc defer
175 let def'' = map (\(n, (i, top, t)) -> (n, (i, top, t, True))) def'
183 let def'' = map (\(n, (i, top, t)) -> (n, (i, top, t, True))) def'
184+ -- if n is defined already, make sure it is just a type declaration
185+ -- with the same type we've just elaborated
186+ checkDefinedAs fc n t' (tt_ctxt i)
176 addDeferredTyCon def''
187 addDeferredTyCon def''
177 mapM_ (elabCaseBlock info []) is
188 mapM_ (elabCaseBlock info []) is
178 (cty, _) <- recheckC fc [] t'
189 (cty, _) <- recheckC fc [] t'
@@ -194,7 +205,17 @@ elabData info syn doc fc codata (PDatadecl n t_in dcons)
194 collapseCons n cons
205 collapseCons n cons
195 updateContext (addDatatype (Data n ttag cty cons))
206 updateContext (addDatatype (Data n ttag cty cons))
196 mapM_ (checkPositive n) cons
207 mapM_ (checkPositive n) cons
208+ if DefaultEliminator `elem` opts then evalStateT (elabEliminator params n t dcons info) Map.empty
209+ else return ()
197 where
210 where
211+ checkDefinedAs fc n t ctxt
212+ = case lookupDef n ctxt of
213+ [] -> return ()
214+ [TyDecl _ ty] ->
215+ case converts ctxt [] t ty of
216+ OK () -> return ()
217+ _ -> tclift $ tfail (At fc (AlreadyDefined n))
218+ _ -> tclift $ tfail (At fc (AlreadyDefined n))
198 -- parameters are names which are unchanged across the structure,
219 -- parameters are names which are unchanged across the structure,
199 -- which appear exactly once in the return type of a constructor
220 -- which appear exactly once in the return type of a constructor
200
221
@@ -245,12 +266,253 @@ elabData info syn doc fc codata (PDatadecl n t_in dcons)
245 | otherwise = count n ts
266 | otherwise = count n ts
246 mParam args (_ : rest) = Nothing : mParam args rest
267 mParam args (_ : rest) = Nothing : mParam args rest
247
268
269+type EliminatorState = StateT (Map.Map String Int) Idris
270+
271+-- TODO: Use uniqueName for generating names, rewrite everything to use idris_implicits instead of manual splitting, generally just rewrite
272+elabEliminator :: [Int] -> Name -> PTerm -> [(String, Name, PTerm, FC)] -> ElabInfo -> EliminatorState ()
273+elabEliminator paramPos n ty cons info = do
274+ elimLog $ "Elaborating eliminator"
275+ let (cnstrs, _) = splitPi ty
276+ let (splittedTy@(pms, idxs)) = splitPms cnstrs
277+ generalParams <- namePis False pms
278+ motiveIdxs <- namePis False idxs
279+ let motive = mkMotive n paramPos generalParams motiveIdxs
280+ consTerms <- mapM (\(c@(_,cnm,_,_)) -> do
281+ name <- freshName $ "elim_" ++ simpleName cnm
282+ consTerm <- extractConsTerm c generalParams
283+ return (name, expl, consTerm)) cons
284+ scrutineeIdxs <- namePis False idxs
285+ let motiveConstr = [(motiveName, expl, motive)]
286+ let scrutinee = (scrutineeName, expl, applyCons n (interlievePos paramPos generalParams scrutineeIdxs 0))
287+ let eliminatorTy = piConstr (generalParams ++ motiveConstr ++ consTerms ++ scrutineeIdxs ++ [scrutinee]) (applyMotive (map (\(n,_,_) -> PRef elimFC n) scrutineeIdxs) (PRef elimFC scrutineeName))
288+ let eliminatorTyDecl = PTy (show n) defaultSyntax elimFC [TotalFn] elimDeclName eliminatorTy
289+ let clauseConsElimArgs = map getPiName consTerms
290+ let clauseGeneralArgs' = map getPiName generalParams ++ [motiveName] ++ clauseConsElimArgs
291+ let clauseGeneralArgs = map (\arg -> pexp (PRef elimFC arg)) clauseGeneralArgs'
292+ let elimSig = "-- eliminator signature: " ++ showImp Nothing True True eliminatorTy
293+ eliminatorClauses <- mapM (\(cns, cnsElim) -> generateEliminatorClauses cns cnsElim clauseGeneralArgs generalParams) (zip cons clauseConsElimArgs)
294+ let eliminatorDef = PClauses emptyFC [TotalFn] elimDeclName eliminatorClauses
295+ elimLog $ "-- eliminator definition: " ++ showDeclImp True eliminatorDef
296+ Control.Monad.State.lift $ idrisCatch (elabDecl EAll info eliminatorTyDecl) (\err -> return ())
297+ -- Do not elaborate clauses if there aren't any
298+ case eliminatorClauses of
299+ [] -> return ()
300+ _ -> Control.Monad.State.lift $ idrisCatch (elabDecl EAll info eliminatorDef) (\err -> return ())
301+ where elimLog :: String -> EliminatorState ()
302+ elimLog s = Control.Monad.State.lift (logLvl 2 s)
303+
304+ elimFC :: FC
305+ elimFC = fileFC "(eliminator)"
306+
307+ elimDeclName :: Name
308+ elimDeclName = SN $ ElimN n
309+
310+ applyNS :: Name -> [String] -> Name
311+ applyNS n [] = n
312+ applyNS n ns = NS n ns
313+
314+ splitPi :: PTerm -> ([(Name, Plicity, PTerm)], PTerm)
315+ splitPi = splitPi' []
316+ where splitPi' :: [(Name, Plicity, PTerm)] -> PTerm -> ([(Name, Plicity, PTerm)], PTerm)
317+ splitPi' acc (PPi pl n tyl tyr) = splitPi' ((n, pl, tyl):acc) tyr
318+ splitPi' acc t = (reverse acc, t)
319+
320+ splitPms :: [(Name, Plicity, PTerm)] -> ([(Name, Plicity, PTerm)], [(Name, Plicity, PTerm)])
321+ splitPms cnstrs = (map fst pms, map fst idxs)
322+ where (pms, idxs) = partition (\c -> snd c `elem` paramPos) (zip cnstrs [0..])
323+
324+ isMachineGenerated :: Name -> Bool
325+ isMachineGenerated (MN _ _) = True
326+ isMachineGenerated _ = False
327+
328+ namePis :: Bool -> [(Name, Plicity, PTerm)] -> EliminatorState [(Name, Plicity, PTerm)]
329+ namePis keepOld pms = do names <- mapM (mkPiName keepOld) pms
330+ let oldNames = map fst names
331+ let params = map snd names
332+ return $ map (\(n, pl, ty) -> (n, pl, removeParamPis oldNames params ty)) params
333+
334+ mkPiName :: Bool -> (Name, Plicity, PTerm) -> EliminatorState (Name, (Name, Plicity, PTerm))
335+ mkPiName keepOld (n, pl, piarg) | not (isMachineGenerated n) && keepOld = do return (n, (n, pl, piarg))
336+ mkPiName _ (oldName, pl, piarg) = do name <- freshName $ keyOf piarg
337+ return (oldName, (name, pl, piarg))
338+ where keyOf :: PTerm -> String
339+ keyOf (PRef _ name) | isLetter (nameStart name) = (toLower $ nameStart name):"__"
340+ keyOf (PApp _ tyf _) = keyOf tyf
341+ keyOf PType = "ty__"
342+ keyOf _ = "carg__"
343+ nameStart :: Name -> Char
344+ nameStart n = nameStart' (simpleName n)
345+ where nameStart' :: String -> Char
346+ nameStart' "" = ' '
347+ nameStart' ns = head ns
348+
349+ simpleName :: Name -> String
350+ simpleName (NS n _) = simpleName n
351+ simpleName (MN i n) = n ++ show i
352+ simpleName n = show n
353+
354+ nameSpaces :: Name -> [String]
355+ nameSpaces (NS _ ns) = ns
356+ nameSpaces _ = []
357+
358+ freshName :: String -> EliminatorState Name
359+ freshName key = do
360+ nameMap <- get
361+ let i = fromMaybe 0 (Map.lookup key nameMap)
362+ let name = key ++ show i
363+ put $ Map.insert key (i+1) nameMap
364+ return (UN name)
365+
366+ scrutineeName :: Name
367+ scrutineeName = UN "scrutinee"
368+
369+ scrutineeArgName :: Name
370+ scrutineeArgName = UN "scrutineeArg"
371+
372+ motiveName :: Name
373+ motiveName = UN "prop"
374+
375+ mkMotive :: Name -> [Int] -> [(Name, Plicity, PTerm)] -> [(Name, Plicity, PTerm)] -> PTerm
376+ mkMotive n paramPos params indicies =
377+ let scrutineeTy = (scrutineeArgName, expl, applyCons n (interlievePos paramPos params indicies 0))
378+ in piConstr (indicies ++ [scrutineeTy]) PType
379+
380+ piConstr :: [(Name, Plicity, PTerm)] -> PTerm -> PTerm
381+ piConstr [] ty = ty
382+ piConstr ((n, pl, tyb):tyr) ty = PPi pl n tyb (piConstr tyr ty)
383+
384+ interlievePos :: [Int] -> [a] -> [a] -> Int -> [a]
385+ interlievePos idxs [] l2 i = l2
386+ interlievePos idxs l1 [] i = l1
387+ interlievePos idxs (x:xs) l2 i | i `elem` idxs = x:(interlievePos idxs xs l2 (i+1))
388+ interlievePos idxs l1 (y:ys) i = y:(interlievePos idxs l1 ys (i+1))
389+
390+ replaceParams :: [Int] -> [(Name, Plicity, PTerm)] -> PTerm -> PTerm
391+ replaceParams paramPos params cns =
392+ let (_, cnsResTy) = splitPi cns
393+ in case cnsResTy of
394+ PApp _ _ args ->
395+ let oldParams = paramNamesOf 0 paramPos args
396+ in removeParamPis oldParams params cns
397+ _ -> cns
398+
399+ removeParamPis :: [Name] -> [(Name, Plicity, PTerm)] -> PTerm -> PTerm
400+ removeParamPis oldParams params (PPi pl n tyb tyr) =
401+ case findIndex (== n) oldParams of
402+ Nothing -> (PPi pl n (removeParamPis oldParams params tyb) (removeParamPis oldParams params tyr))
403+ Just i -> (removeParamPis oldParams params tyr)
404+ removeParamPis oldParams params (PRef _ n) =
405+ case findIndex (== n) oldParams of
406+ Nothing -> (PRef elimFC n)
407+ Just i -> let (newname,_,_) = params !! i in (PRef elimFC (newname))
408+ removeParamPis oldParams params (PApp _ cns args) =
409+ PApp elimFC (removeParamPis oldParams params cns) $ replaceParamArgs args
410+ where replaceParamArgs :: [PArg] -> [PArg]
411+ replaceParamArgs [] = []
412+ replaceParamArgs (arg:args) =
413+ case extractName (getTm arg) of
414+ [] -> arg:replaceParamArgs args
415+ [n] ->
416+ case findIndex (== n) oldParams of
417+ Nothing -> arg:replaceParamArgs args
418+ Just i -> let (newname,_,_) = params !! i in arg {getTm = PRef elimFC newname}:replaceParamArgs args
419+ removeParamPis oldParams params t = t
420+
421+ paramNamesOf :: Int -> [Int] -> [PArg] -> [Name]
422+ paramNamesOf i paramPos [] = []
423+ paramNamesOf i paramPos (arg:args) = (if i `elem` paramPos then extractName (getTm arg) else []) ++ paramNamesOf (i+1) paramPos args
424+
425+ extractName :: PTerm -> [Name]
426+ extractName (PRef _ n) = [n]
427+ extractName _ = []
428+
429+ splitArgPms :: PTerm -> ([PTerm], [PTerm])
430+ splitArgPms (PApp _ f args) = splitArgPms' args
431+ where splitArgPms' :: [PArg] -> ([PTerm], [PTerm])
432+ splitArgPms' cnstrs = (map (getTm . fst) pms, map (getTm . fst) idxs)
433+ where (pms, idxs) = partition (\c -> snd c `elem` paramPos) (zip cnstrs [0..])
434+ splitArgPms _ = ([],[])
435+
436+
437+ implicitIndexes :: (String, Name, PTerm, FC) -> EliminatorState [(Name, Plicity, PTerm)]
438+ implicitIndexes (cns@(doc, cnm, ty, fc)) = do
439+ i <- Control.Monad.State.lift getIState
440+ implargs' <- case lookupCtxt cnm (idris_implicits i) of
441+ [] -> do fail $ "Error while showing implicits for " ++ show cnm
442+ [args] -> do return args
443+ _ -> do fail $ "Ambigous name for " ++ show cnm
444+ let implargs = mapMaybe convertImplPi implargs'
445+ let (_, cnsResTy) = splitPi ty
446+ case cnsResTy of
447+ PApp _ _ args ->
448+ let oldParams = paramNamesOf 0 paramPos args
449+ in return $ filter (\(n,_,_) -> not (n `elem` oldParams))implargs
450+ _ -> return implargs
451+
452+ extractConsTerm :: (String, Name, PTerm, FC) -> [(Name, Plicity, PTerm)] -> EliminatorState PTerm
453+ extractConsTerm (doc, cnm, ty, fc) generalParameters = do
454+ let cons' = replaceParams paramPos generalParameters ty
455+ let (args, resTy) = splitPi cons'
456+ implidxs <- implicitIndexes (doc, cnm, ty, fc)
457+ consArgs <- namePis True args
458+ let recArgs = findRecArgs consArgs
459+ let recMotives = map applyRecMotive recArgs
460+ let (_, consIdxs) = splitArgPms resTy
461+ return $ piConstr (implidxs ++ consArgs ++ recMotives) (applyMotive consIdxs (applyCons cnm consArgs))
462+ where applyRecMotive :: (Name, Plicity, PTerm) -> (Name, Plicity, PTerm)
463+ applyRecMotive (n,_,ty) = (UN $ "ih" ++ simpleName n, expl, applyMotive idxs (PRef elimFC n))
464+ where (_, idxs) = splitArgPms ty
465+
466+ findRecArgs :: [(Name, Plicity, PTerm)] -> [(Name, Plicity, PTerm)]
467+ findRecArgs [] = []
468+ findRecArgs (ty@(_,_,PRef _ tn):rs) | simpleName tn == simpleName n = ty:findRecArgs rs
469+ findRecArgs (ty@(_,_,PApp _ (PRef _ tn) _):rs) | simpleName tn == simpleName n = ty:findRecArgs rs
470+ findRecArgs (ty:rs) = findRecArgs rs
471+
472+ applyCons :: Name -> [(Name, Plicity, PTerm)] -> PTerm
473+ applyCons tn targs = PApp elimFC (PRef elimFC tn) (map convertArg targs)
474+
475+ convertArg :: (Name, Plicity, PTerm) -> PArg
476+ convertArg (n, _, _) = pexp (PRef elimFC n)
477+
478+ applyMotive :: [PTerm] -> PTerm -> PTerm
479+ applyMotive idxs t = PApp elimFC (PRef elimFC motiveName) (map pexp idxs ++ [pexp t])
480+
481+ getPiName :: (Name, Plicity, PTerm) -> Name
482+ getPiName (name,_,_) = name
483+
484+ convertImplPi :: PArg -> Maybe (Name, Plicity, PTerm)
485+ convertImplPi (PImp {getTm = t, pname = n}) = Just (n, expl, t)
486+ convertImplPi _ = Nothing
487+
488+ generateEliminatorClauses :: (String, Name, PTerm, FC) -> Name -> [PArg] -> [(Name, Plicity, PTerm)] -> EliminatorState PClause
489+ generateEliminatorClauses (doc, cnm, ty, fc) cnsElim generalArgs generalParameters = do
490+ let cons' = replaceParams paramPos generalParameters ty
491+ let (args, resTy) = splitPi cons'
492+ i <- Control.Monad.State.lift getIState
493+ implidxs <- implicitIndexes (doc, cnm, ty, fc)
494+ let (_, generalIdxs') = splitArgPms resTy
495+ let generalIdxs = map pexp generalIdxs'
496+ consArgs <- namePis True args
497+ let lhsPattern = PApp elimFC (PRef elimFC elimDeclName) (generalArgs ++ generalIdxs ++ [pexp $ applyCons cnm consArgs])
498+ let recArgs = findRecArgs consArgs
499+ let recElims = map applyRecElim recArgs
500+ let rhsExpr = PApp elimFC (PRef elimFC cnsElim) (map convertArg implidxs ++ map convertArg consArgs ++ recElims)
501+ return $ PClause elimFC elimDeclName lhsPattern [] rhsExpr []
502+ where applyRecElim :: (Name, Plicity, PTerm) -> PArg
503+ applyRecElim (constr@(recCnm,_,recTy)) = pexp $ PApp elimFC (PRef elimFC elimDeclName) (generalArgs ++ map pexp idxs ++ [pexp $ PRef elimFC recCnm])
504+ where (_, idxs) = splitArgPms recTy
505+
248-- | Elaborate primitives
506-- | Elaborate primitives
249
507
250elabPrims :: Idris ()
508elabPrims :: Idris ()
251elabPrims = do mapM_ (elabDecl EAll toplevel)
509elabPrims = do mapM_ (elabDecl EAll toplevel)
252− (map (PData "" defaultSyntax (fileFC "builtin") False)
510+ (map (\(opt, decl) -> PData "" defaultSyntax (fileFC "builtin") opt decl)
511+ (zip
512+ [inferOpts, unitOpts, falseOpts, pairOpts, eqOpts]
253− [inferDecl, unitDecl, falseDecl, pairDecl, eqDecl])
513+ [inferDecl, unitDecl, falseDecl, pairDecl, eqDecl]))
514+ addNameHint eqTy (UN "prf")
515+ elabDecl EAll toplevel elimDecl
254 mapM_ elabPrim primitives
516 mapM_ elabPrim primitives
255 -- Special case prim__believe_me because it doesn't work on just constants
517 -- Special case prim__believe_me because it doesn't work on just constants
256 elabBelieveMe
518 elabBelieveMe
@@ -400,7 +662,7 @@ elabTransform info fc safe lhs_in rhs_in
400elabRecord :: ElabInfo -> SyntaxInfo -> String -> FC -> Name ->
662elabRecord :: ElabInfo -> SyntaxInfo -> String -> FC -> Name ->
401 PTerm -> String -> Name -> PTerm -> Idris ()
663 PTerm -> String -> Name -> PTerm -> Idris ()
402elabRecord info syn doc fc tyn ty cdoc cn cty
664elabRecord info syn doc fc tyn ty cdoc cn cty
403− = do elabData info syn doc fc False (PDatadecl tyn ty [(cdoc, cn, cty, fc)])
665+ = do elabData info syn doc fc [] (PDatadecl tyn ty [(cdoc, cn, cty, fc)])
404 cty' <- implicit syn cn cty
666 cty' <- implicit syn cn cty
405 i <- getIState
667 i <- getIState
406 cty <- case lookupTy cn (tt_ctxt i) of
668 cty <- case lookupTy cn (tt_ctxt i) of
@@ -531,7 +793,7 @@ elabCon info syn tn codata (doc, n, t_in, fc)
531 addIBC (IBCDef n)
793 addIBC (IBCDef n)
532 addDocStr n doc
794 addDocStr n doc
533 addIBC (IBCDoc n)
795 addIBC (IBCDoc n)
534− forceArgs n cty'
796+ forceArgs tn n cty'
535 return (n, cty')
797 return (n, cty')
536 where
798 where
537 tyIs (Bind n b sc) = tyIs sc
799 tyIs (Bind n b sc) = tyIs sc
@@ -638,7 +900,7 @@ elabClauses info fc opts n_in cs = let n = liftname info n_in in
638 Just _ -> logLvl 5 $ "Partially evaluated:\n" ++ show pats
900 Just _ -> logLvl 5 $ "Partially evaluated:\n" ++ show pats
639 _ -> return ()
901 _ -> return ()
640
902
641− let optpdef = map debind optpats -- $ map (simple_lhs (tt_ctxt ist)) optpats
903+ let optpdef = map debind optpats -- \$ map (simple_lhs (tt_ctxt ist)) optpats
642 tree@(CaseDef scargs sc _) <- tclift $
904 tree@(CaseDef scargs sc _) <- tclift $
643 simpleCase tcase False reflect CompileTime fc pdef
905 simpleCase tcase False reflect CompileTime fc pdef
644 cov <- coverage
906 cov <- coverage
@@ -797,7 +1059,7 @@ elabPE info fc caller r =
797
1059
798 mkSpecialised ist specapp_in = do
1060 mkSpecialised ist specapp_in = do
799 let (specTy, specapp) = getSpecTy ist specapp_in
1061 let (specTy, specapp) = getSpecTy ist specapp_in
800− let (n, newnm, [(lhs, rhs)]) = getSpecClause ist specapp
1062+ let (n, newnm, pats) = getSpecClause ist specapp
801 let undef = case lookupDef newnm (tt_ctxt ist) of
1063 let undef = case lookupDef newnm (tt_ctxt ist) of
802 [] -> True
1064 [] -> True
803 _ -> False
1065 _ -> False
@@ -812,10 +1074,12 @@ elabPE info fc caller r =
812 iLOG $ "PE definition type : " ++ (show specTy)
1074 iLOG $ "PE definition type : " ++ (show specTy)
813 ++ "\n" ++ show opts
1075 ++ "\n" ++ show opts
814 logLvl 2 $ "PE definition " ++ show newnm ++ ":\n" ++
1076 logLvl 2 $ "PE definition " ++ show newnm ++ ":\n" ++
1077+ showSep "\n"
1078+ (map (\ (lhs, rhs) ->
815− (showImp Nothing True False lhs ++ " = " ++
1079+ (showImp Nothing True False lhs ++ " = " ++
816− showImp Nothing True False rhs)
1080+ showImp Nothing True False rhs)) pats)
817 elabType info defaultSyntax "" fc opts newnm specTy
1081 elabType info defaultSyntax "" fc opts newnm specTy
818− let def = [PClause fc newnm lhs [] rhs []]
1082+ let def = map (\ (lhs, rhs) -> PClause fc newnm lhs [] rhs []) pats
819 elabClauses info fc opts newnm def
1083 elabClauses info fc opts newnm def
820 logLvl 1 $ "Specialised " ++ show newnm)
1084 logLvl 1 $ "Specialised " ++ show newnm)
821 -- if it doesn't work, just don't specialise. Could happen for lots
1085 -- if it doesn't work, just don't specialise. Could happen for lots
@@ -918,7 +1182,18 @@ checkPossible info fc tcgen fname lhs_in
918-- b <- inferredDiff fc (delab' i lhs_tm True) lhs
1182-- b <- inferredDiff fc (delab' i lhs_tm True) lhs
919-- return (not b) -- then return (Just lhs_tm) else return Nothing
1183-- return (not b) -- then return (Just lhs_tm) else return Nothing
920-- trace (show (delab' i lhs_tm True) ++ "\n" ++ show lhs) $ return (not b)
1184-- trace (show (delab' i lhs_tm True) ++ "\n" ++ show lhs) $ return (not b)
921− err@(Error _) -> return False
1185+ Error err -> return (impossibleError err)
1186+ where impossibleError (CantUnify _ topx topy e _ _)
1187+ = not (sameFam topx topy || not (impossibleError e))
1188+ impossibleError (CantConvert _ _ _) = False
1189+ impossibleError (At _ e) = impossibleError e
1190+ impossibleError (Elaborating _ _ e) = impossibleError e
1191+ impossibleError _ = True
1192+
1193+ sameFam topx topy
1194+ = case (unApply topx, unApply topy) of
1195+ ((P _ x _, _), (P _ y _, _)) -> x == y
1196+ _ -> False
922
1197
923elabClause :: ElabInfo -> FnOpts -> (Int, PClause) ->
1198elabClause :: ElabInfo -> FnOpts -> (Int, PClause) ->
924 Idris (Either Term (Term, Term))
1199 Idris (Either Term (Term, Term))
@@ -926,7 +1201,8 @@ elabClause info opts (_, PClause fc fname lhs_in [] PImpossible [])
926 = do let tcgen = Dictionary `elem` opts
1201 = do let tcgen = Dictionary `elem` opts
927 b <- checkPossible info fc tcgen fname lhs_in
1202 b <- checkPossible info fc tcgen fname lhs_in
928 case b of
1203 case b of
1204+ True -> tclift $ tfail (At fc
929− True -> ifail $ show fc ++ ":" ++ show lhs_in ++ " is a possible case"
1205+ (Msg $ show lhs_in ++ " is a valid case"))
930 False -> do ptm <- mkPatTm lhs_in
1206 False -> do ptm <- mkPatTm lhs_in
931 return (Left ptm)
1207 return (Left ptm)
932elabClause info opts (cnum, PClause fc fname lhs_in withs rhs_in whereblock)
1208elabClause info opts (cnum, PClause fc fname lhs_in withs rhs_in whereblock)
@@ -1268,6 +1544,8 @@ elabClass info syn doc fc constraints tn ps ds
1268 (map (pexp . PRef fc) (map fst ps))
1544 (map (pexp . PRef fc) (map fst ps))
1269 -- build data declaration
1545 -- build data declaration
1270 let mdecls = filter tydecl ds -- method declarations
1546 let mdecls = filter tydecl ds -- method declarations
1547+ let idecls = filter instdecl ds -- default superclass instance declarations
1548+ mapM_ checkDefaultSuperclassInstance idecls
1271 let mnames = map getMName mdecls
1549 let mnames = map getMName mdecls
1272 logLvl 2 $ "Building methods " ++ show mnames
1550 logLvl 2 $ "Building methods " ++ show mnames
1273 ims <- mapM (tdecl mnames) mdecls
1551 ims <- mapM (tdecl mnames) mdecls
@@ -1276,7 +1554,7 @@ elabClass info syn doc fc constraints tn ps ds
1276 let (methods, imethods)
1554 let (methods, imethods)
1277 = unzip (map (\ ( x,y,z) -> (x, y)) ims)
1555 = unzip (map (\ ( x,y,z) -> (x, y)) ims)
1278 let defaults = map (\ (x, (y, z)) -> (x,y)) defs
1556 let defaults = map (\ (x, (y, z)) -> (x,y)) defs
1279− addClass tn (CI cn (map nodoc imethods) defaults (map fst ps) [])
1557+ addClass tn (CI cn (map nodoc imethods) defaults idecls (map fst ps) [])
1280 -- build instance constructor type
1558 -- build instance constructor type
1281 -- decorate names of functions to ensure they can't be referred
1559 -- decorate names of functions to ensure they can't be referred
1282 -- to elsewhere in the class declaration
1560 -- to elsewhere in the class declaration
@@ -1286,7 +1564,7 @@ elabClass info syn doc fc constraints tn ps ds
1286 let cons = [("", cn, cty, fc)]
1564 let cons = [("", cn, cty, fc)]
1287 let ddecl = PDatadecl tn tty cons
1565 let ddecl = PDatadecl tn tty cons
1288 logLvl 5 $ "Class data " ++ showDImp True ddecl
1566 logLvl 5 $ "Class data " ++ showDImp True ddecl
1289− elabData info (syn { no_imp = no_imp syn ++ mnames }) doc fc False ddecl
1567+ elabData info (syn { no_imp = no_imp syn ++ mnames }) doc fc [] ddecl
1290 -- for each constraint, build a top level function to chase it
1568 -- for each constraint, build a top level function to chase it
1291 logLvl 5 $ "Building functions"
1569 logLvl 5 $ "Building functions"
1292 let usyn = syn { using = map (\ (x,y) -> UImplicit x y) ps
1570 let usyn = syn { using = map (\ (x,y) -> UImplicit x y) ps
@@ -1298,7 +1576,6 @@ elabClass info syn doc fc constraints tn ps ds
1298 mapM_ (elabDecl EAll info) (concat fns)
1576 mapM_ (elabDecl EAll info) (concat fns)
1299 -- add the default definitions
1577 -- add the default definitions
1300 mapM_ (elabDecl EAll info) (concat (map (snd.snd) defs))
1578 mapM_ (elabDecl EAll info) (concat (map (snd.snd) defs))
1301− i <- getIState
1302 addIBC (IBCClass tn)
1579 addIBC (IBCClass tn)
1303 where
1580 where
1304 nodoc (n, (_, o, t)) = (n, (o, t))
1581 nodoc (n, (_, o, t)) = (n, (o, t))
@@ -1309,6 +1586,17 @@ elabClass info syn doc fc constraints tn ps ds
1309 mdec (NS x n) = NS (mdec x) n
1586 mdec (NS x n) = NS (mdec x) n
1310 mdec x = x
1587 mdec x = x
1311
1588
1589+ -- TODO: probably should normalise
1590+ checkDefaultSuperclassInstance (PInstance _ fc cs n ps _ _ _)
1591+ = do when (not $ null cs) . tclift
1592+ $ tfail (At fc (Msg $ "Default superclass instances can't have constraints."))
1593+ i <- getIState
1594+ let t = PApp fc (PRef fc n) (map pexp ps)
1595+ let isConstrained = any (== t) constraints
1596+ when (not isConstrained) . tclift
1597+ $ tfail (At fc (Msg $ "Default instances must be for a superclass constraint on the containing class."))
1598+ return ()
1599+
1312 impbind [] x = x
1600 impbind [] x = x
1313 impbind ((n, ty): ns) x = PPi impl n ty (impbind ns x)
1601 impbind ((n, ty): ns) x = PPi impl n ty (impbind ns x)
1314 conbind (ty : ns) x = PPi constraint (MN 0 "class") ty (conbind ns x)
1602 conbind (ty : ns) x = PPi constraint (MN 0 "class") ty (conbind ns x)
@@ -1340,6 +1628,8 @@ elabClass info syn doc fc constraints tn ps ds
1340
1628
1341 tydecl (PTy _ _ _ _ _ _) = True
1629 tydecl (PTy _ _ _ _ _ _) = True
1342 tydecl _ = False
1630 tydecl _ = False
1631+ instdecl (PInstance _ _ _ _ _ _ _ _) = True
1632+ instdecl _ = False
1343 clause (PClauses _ _ _ _) = True
1633 clause (PClauses _ _ _ _) = True
1344 clause _ = False
1634 clause _ = False
1345
1635
@@ -1425,15 +1715,12 @@ elabInstance info syn fc cs n ps t expn ds
1425 [c] -> return c
1715 [c] -> return c
1426 _ -> ifail $ show fc ++ ":" ++ show n ++ " is not a type class"
1716 _ -> ifail $ show fc ++ ":" ++ show n ++ " is not a type class"
1427 let constraint = PApp fc (PRef fc n) (map pexp ps)
1717 let constraint = PApp fc (PRef fc n) (map pexp ps)
1428− let iname = case expn of
1718+ let iname = mkiname n ps expn
1429− Nothing -> SN (InstanceN n (map show ps))
1430− -- UN ('@':show n ++ "$" ++ show ps)
1431− Just nm -> nm
1432 nty <- elabType' True info syn "" fc [] iname t
1719 nty <- elabType' True info syn "" fc [] iname t
1433 -- if the instance type matches any of the instances we have already,
1720 -- if the instance type matches any of the instances we have already,
1434 -- and it's not a named instance, then it's overlapping, so report an error
1721 -- and it's not a named instance, then it's overlapping, so report an error
1435 case expn of
1722 case expn of
1436− Nothing -> do mapM_ (checkNotOverlapping i (delab i nty))
1723+ Nothing -> do mapM_ (maybe (return ()) overlapping . findOverlapping i (delab i nty))
1437 (class_instances ci)
1724 (class_instances ci)
1438 addInstance intInst n iname
1725 addInstance intInst n iname
1439 Just _ -> addInstance intInst n iname
1726 Just _ -> addInstance intInst n iname
@@ -1447,6 +1734,9 @@ elabInstance info syn fc cs n ps t expn ds
1447 PApp _ _ args -> getWParams args
1734 PApp _ _ args -> getWParams args
1448 _ -> return []) ps
1735 _ -> return []) ps
1449 let pnames = map pname (concat (nub wparams))
1736 let pnames = map pname (concat (nub wparams))
1737+ let superclassInstances = map (substInstance ips pnames) (class_default_superclasses ci)
1738+ undefinedSuperclassInstances <- filterM (fmap not . isOverlapping i) superclassInstances
1739+ mapM_ (elabDecl EAll info) undefinedSuperclassInstances
1450 let all_meths = map (nsroot . fst) (class_methods ci)
1740 let all_meths = map (nsroot . fst) (class_methods ci)
1451 let mtys = map (\ (n, (op, t)) ->
1741 let mtys = map (\ (n, (op, t)) ->
1452 let t_in = substMatchesShadow ips pnames t
1742 let t_in = substMatchesShadow ips pnames t
@@ -1473,7 +1763,7 @@ elabInstance info syn fc cs n ps t expn ds
1473 let idecls = [PClauses fc [Dictionary] iname
1763 let idecls = [PClauses fc [Dictionary] iname
1474 [PClause fc iname lhs [] rhs wb]]
1764 [PClause fc iname lhs [] rhs wb]]
1475 iLOG (show idecls)
1765 iLOG (show idecls)
1476− mapM (elabDecl EAll info) idecls
1766+ mapM_ (elabDecl EAll info) idecls
1477 addIBC (IBCInstance intInst n iname)
1767 addIBC (IBCInstance intInst n iname)
1478-- -- for each constraint, build a top level function to chase it
1768-- -- for each constraint, build a top level function to chase it
1479-- logLvl 5 $ "Building functions"
1769-- logLvl 5 $ "Building functions"
@@ -1484,20 +1774,50 @@ elabInstance info syn fc cs n ps t expn ds
1484 [PConstant (AType (ATInt ITNative))] -> True
1774 [PConstant (AType (ATInt ITNative))] -> True
1485 _ -> False
1775 _ -> False
1486
1776
1487− checkNotOverlapping i t n
1777+ mkiname n' ps' expn' =
1778+ case expn' of
1779+ Nothing -> SN (InstanceN n' (map show ps'))
1780+ Just nm -> nm
1781+
1782+ substInstance ips pnames (PInstance syn _ cs n ps t expn ds)
1783+ = PInstance syn fc cs n (map (substMatchesShadow ips pnames) ps) (substMatchesShadow ips pnames t) expn ds
1784+
1785+ isOverlapping i (PInstance syn _ _ n ps t expn _)
1786+ = case lookupCtxtName n (idris_classes i) of
1787+ [(n, ci)] -> let iname = (mkiname n ps expn) in
1788+ case lookupTy iname (tt_ctxt i) of
1789+ [] -> elabFindOverlapping i ci iname syn t
1790+ (_:_) -> return True
1791+ _ -> return False -- couldn't find class, just let elabInstance fail later
1792+
1793+ -- TODO: largely based upon elabType' - should try to abstract
1794+ elabFindOverlapping i ci iname syn t
1795+ = do ty' <- addUsingConstraints syn fc t
1796+ ty' <- implicit syn iname ty'
1797+ let ty = addImpl i ty'
1798+ ctxt <- getContext
1799+ ((tyT, _, _), _) <-
1800+ tclift $ elaborate ctxt iname (TType (UVal 0)) []
1801+ (errAt "type of " iname (erun fc (build i info False iname ty)))
1802+ ctxt <- getContext
1803+ (cty, _) <- recheckC fc [] tyT
1804+ let nty = normalise ctxt [] cty
1805+ return $ any (isJust . findOverlapping i (delab i nty)) (class_instances ci)
1806+
1807+ findOverlapping i t n
1488− | take 2 (show n) == "@@" = return ()
1808+ | take 2 (show n) == "@@" = Nothing
1489 | otherwise
1809 | otherwise
1490 = case lookupTy n (tt_ctxt i) of
1810 = case lookupTy n (tt_ctxt i) of
1491 [t'] -> let tret = getRetType t
1811 [t'] -> let tret = getRetType t
1492 tret' = getRetType (delab i t') in
1812 tret' = getRetType (delab i t') in
1493 case matchClause i tret' tret of
1813 case matchClause i tret' tret of
1494− Right ms -> overlapping tret tret'
1814+ Right ms -> Just tret'
1495 Left _ -> case matchClause i tret tret' of
1815 Left _ -> case matchClause i tret tret' of
1496− Right ms -> overlapping tret tret'
1816+ Right ms -> Just tret'
1497− Left _ -> return ()
1817+ Left _ -> Nothing
1498− _ -> return ()
1818+ _ -> Nothing
1499− overlapping t t' = tclift $ tfail (At fc (Msg $
1819+ overlapping t' = tclift $ tfail (At fc (Msg $
1500− "Overlapping instance: " ++ show t' ++ " already defined"))
1820+ "Overlapping instance: " ++ show t' ++ " already defined"))
1501 getRetType (PPi _ _ _ sc) = getRetType sc
1821 getRetType (PPi _ _ _ sc) = getRetType sc
1502 getRetType t = t
1822 getRetType t = t
1503
1823
@@ -1709,7 +2029,7 @@ elabDecl' what info (PRecord doc s f tyn ty cdoc cn cty)
1709 elabRecord info s doc f tyn ty cdoc cn cty
2029 elabRecord info s doc f tyn ty cdoc cn cty
1710 | otherwise
2030 | otherwise
1711 = do iLOG $ "Elaborating [type of] " ++ show tyn
2031 = do iLOG $ "Elaborating [type of] " ++ show tyn
1712− elabData info s doc f False (PLaterdecl tyn ty)
2032+ elabData info s doc f [] (PLaterdecl tyn ty)
1713elabDecl' _ info (PDSL n dsl)
2033elabDecl' _ info (PDSL n dsl)
1714 = do i <- getIState
2034 = do i <- getIState
1715 putIState (i { idris_dsls = addDef n dsl (idris_dsls i) })
2035 putIState (i { idris_dsls = addDef n dsl (idris_dsls i) })
src/Idris/ElabTerm.hs+17−12
@@ -47,14 +47,16 @@ build ist info pattern fn tm
47 when (not pattern) $
47 when (not pattern) $
48 mapM_ (\n -> when (n `elem` hs) $
48 mapM_ (\n -> when (n `elem` hs) $
49 do focus n
49 do focus n
50+ g <- goal
50− try (resolveTC 7 fn ist)
51+ try (resolveTC 7 g fn ist)
51 (movelast n)) ivs
52 (movelast n)) ivs
52 ivs <- get_instances
53 ivs <- get_instances
53 hs <- get_holes
54 hs <- get_holes
54 when (not pattern) $
55 when (not pattern) $
55 mapM_ (\n -> when (n `elem` hs) $
56 mapM_ (\n -> when (n `elem` hs) $
56 do focus n
57 do focus n
58+ g <- goal
57− resolveTC 7 fn ist) ivs
59+ resolveTC 7 g fn ist) ivs
58 tm <- get_term
60 tm <- get_term
59 ctxt <- get_context
61 ctxt <- get_context
60 when (not pattern) $ do matchProblems; unifyProblems
62 when (not pattern) $ do matchProblems; unifyProblems
@@ -150,12 +152,12 @@ elab ist info pattern tcgen fn tm
150 (elab' ina (PRef fc unitTy))
152 (elab' ina (PRef fc unitTy))
151 elab' ina (PFalse fc) = elab' ina (PRef fc falseTy)
153 elab' ina (PFalse fc) = elab' ina (PRef fc falseTy)
152 elab' ina (PResolveTC (FC "HACK" _ _)) -- for chasing parent classes
154 elab' ina (PResolveTC (FC "HACK" _ _)) -- for chasing parent classes
153− = resolveTC 5 fn ist
155+ = do g <- goal; resolveTC 5 g fn ist
154 elab' ina (PResolveTC fc)
156 elab' ina (PResolveTC fc)
155 | True = do c <- unique_hole (MN 0 "class")
157 | True = do c <- unique_hole (MN 0 "class")
156 instanceArg c
158 instanceArg c
157 | otherwise = do g <- goal
159 | otherwise = do g <- goal
158− try (resolveTC 2 fn ist)
160+ try (resolveTC 2 g fn ist)
159 (do c <- unique_hole (MN 0 "class")
161 (do c <- unique_hole (MN 0 "class")
160 instanceArg c)
162 instanceArg c)
161 elab' ina (PRefl fc t)
163 elab' ina (PRefl fc t)
@@ -414,7 +416,7 @@ elab ist info pattern tcgen fn tm
414 hs <- get_holes
416 hs <- get_holes
415 if all (\n -> not (n `elem` hs)) (freeNames g)
417 if all (\n -> not (n `elem` hs)) (freeNames g)
416 -- let insts = filter tcname $ map fst (ctxtAlist (tt_ctxt ist))
418 -- let insts = filter tcname $ map fst (ctxtAlist (tt_ctxt ist))
417− then try (resolveTC 7 fn ist)
419+ then try (resolveTC 7 g fn ist)
418 (movelast n)
420 (movelast n)
419 else movelast n)
421 else movelast n)
420 (ivs' \\ ivs)
422 (ivs' \\ ivs)
@@ -639,7 +641,7 @@ findInstances :: IState -> Term -> [Name]
639findInstances ist t
641findInstances ist t
640 | (P _ n _, _) <- unApply t
642 | (P _ n _, _) <- unApply t
641 = case lookupCtxt n (idris_classes ist) of
643 = case lookupCtxt n (idris_classes ist) of
642− [CI _ _ _ _ ins] -> ins
644+ [CI _ _ _ _ _ ins] -> ins
643 _ -> []
645 _ -> []
644 | otherwise = []
646 | otherwise = []
645
647
@@ -649,10 +651,10 @@ proofSearch' ist top n hints
649 = proofSearch (elab ist toplevel False False (MN 0 "tac")) top n hints ist
651 = proofSearch (elab ist toplevel False False (MN 0 "tac")) top n hints ist
650
652
651
653
652−resolveTC :: Int -> Name -> IState -> ElabD ()
654+resolveTC :: Int -> Term -> Name -> IState -> ElabD ()
653−resolveTC 0 fn ist = fail $ "Can't resolve type class"
655+resolveTC 0 topg fn ist = fail $ "Can't resolve type class"
654−resolveTC 1 fn ist = try' (trivial' ist) (resolveTC 0 fn ist) True
656+resolveTC 1 topg fn ist = try' (trivial' ist) (resolveTC 0 topg fn ist) True
655−resolveTC depth fn ist
657+resolveTC depth topg fn ist
656 = do hnf_compute
658 = do hnf_compute
657 g <- goal
659 g <- goal
658 ptm <- get_term
660 ptm <- get_term
@@ -701,7 +703,7 @@ resolveTC depth fn ist
701
703
702 blunderbuss t d [] = do -- c <- get_env
704 blunderbuss t d [] = do -- c <- get_env
703 -- ps <- get_probs
705 -- ps <- get_probs
704− lift $ tfail $ CantResolve t
706+ lift $ tfail $ CantResolve topg
705 blunderbuss t d (n:ns)
707 blunderbuss t d (n:ns)
706 | n /= fn && tcname n = try' (resolve n d)
708 | n /= fn && tcname n = try' (resolve n d)
707 (blunderbuss t d ns) True
709 (blunderbuss t d ns) True
@@ -729,7 +731,7 @@ resolveTC depth fn ist
729 t' <- goal
731 t' <- goal
730 let (tc', ttype) = unApply t'
732 let (tc', ttype) = unApply t'
731 let depth' = if t == t' then depth - 1 else depth
733 let depth' = if t == t' then depth - 1 else depth
732− resolveTC depth' fn ist)
734+ resolveTC depth' topg fn ist)
733 (filter (\ (x, y) -> not x) (zip (map fst imps) args))
735 (filter (\ (x, y) -> not x) (zip (map fst imps) args))
734 -- if there's any arguments left, we've failed to resolve
736 -- if there's any arguments left, we've failed to resolve
735 hs <- get_holes
737 hs <- get_holes
@@ -838,6 +840,9 @@ runTac autoSolve ist tac
838 elab ist toplevel False False (MN 0 "tac") tm
840 elab ist toplevel False False (MN 0 "tac") tm
839 rewrite (Var letn)
841 rewrite (Var letn)
840 when autoSolve solveAll
842 when autoSolve solveAll
843+ runT (Induction nm)
844+ = do induction nm
845+ when autoSolve solveAll
841 runT (LetTac n tm)
846 runT (LetTac n tm)
842 = do attack
847 = do attack
843 tyn <- unique_hole (MN 0 "letty")
848 tyn <- unique_hole (MN 0 "letty")
src/Idris/IBC.hs+52−16
@@ -23,7 +23,7 @@ import Debug.Trace
23import Paths_idris
23import Paths_idris
24
24
25ibcVersion :: Word8
25ibcVersion :: Word8
26−ibcVersion = 44
26+ibcVersion = 48
27
27
28data IBCFile = IBCFile { ver :: Word8,
28data IBCFile = IBCFile { ver :: Word8,
29 sourcefile :: FilePath,
29 sourcefile :: FilePath,
@@ -51,7 +51,8 @@ data IBCFile = IBCFile { ver :: Word8,
51 ibc_docstrings :: [(Name, String)],
51 ibc_docstrings :: [(Name, String)],
52 ibc_transforms :: [(Term, Term)],
52 ibc_transforms :: [(Term, Term)],
53 ibc_coercions :: [Name],
53 ibc_coercions :: [Name],
54− ibc_lineapps :: [(FilePath, Int, PTerm)]
54+ ibc_lineapps :: [(FilePath, Int, PTerm)],
55+ ibc_namehints :: [(Name, Name)]
55 }
56 }
56 deriving Show
57 deriving Show
57{-!
58{-!
@@ -59,7 +60,7 @@ deriving instance Binary IBCFile
59!-}
60!-}
60
61
61initIBC :: IBCFile
62initIBC :: IBCFile
62−initIBC = IBCFile ibcVersion "" [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] []
63+initIBC = IBCFile ibcVersion "" [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] []
63
64
64loadIBC :: FilePath -> Idris ()
65loadIBC :: FilePath -> Idris ()
65loadIBC fp = do iLOG $ "Loading ibc " ++ fp
66loadIBC fp = do iLOG $ "Loading ibc " ++ fp
@@ -137,6 +138,8 @@ ibc i (IBCTotal n a) f = return f { ibc_total = (n,a) : ibc_total f }
137ibc i (IBCTrans t) f = return f { ibc_transforms = t : ibc_transforms f }
138ibc i (IBCTrans t) f = return f { ibc_transforms = t : ibc_transforms f }
138ibc i (IBCLineApp fp l t) f
139ibc i (IBCLineApp fp l t) f
139 = return f { ibc_lineapps = (fp,l,t) : ibc_lineapps f }
140 = return f { ibc_lineapps = (fp,l,t) : ibc_lineapps f }
141+ibc i (IBCNameHint (n, ty)) f
142+ = return f { ibc_namehints = (n, ty) : ibc_namehints f }
140
143
141process :: IBCFile -> FilePath -> Idris ()
144process :: IBCFile -> FilePath -> Idris ()
142process i fn
145process i fn
@@ -172,6 +175,7 @@ process i fn
172 pCoercions (ibc_coercions i)
175 pCoercions (ibc_coercions i)
173 pTrans (ibc_transforms i)
176 pTrans (ibc_transforms i)
174 pLineApps (ibc_lineapps i)
177 pLineApps (ibc_lineapps i)
178+ pNameHints (ibc_namehints i)
175
179
176timestampOlder :: FilePath -> FilePath -> IO ()
180timestampOlder :: FilePath -> FilePath -> IO ()
177timestampOlder src ibc = do srct <- getModificationTime src
181timestampOlder src ibc = do srct <- getModificationTime src
@@ -221,7 +225,7 @@ pClasses cs = mapM_ (\ (n, c) ->
221 -- Don't lose instances from previous IBCs, which
225 -- Don't lose instances from previous IBCs, which
222 -- could have loaded in any order
226 -- could have loaded in any order
223 let is = case lookupCtxt n (idris_classes i) of
227 let is = case lookupCtxt n (idris_classes i) of
224− [CI _ _ _ _ ins] -> ins
228+ [CI _ _ _ _ _ ins] -> ins
225 _ -> []
229 _ -> []
226 let c' = c { class_instances =
230 let c' = c { class_instances =
227 class_instances c ++ is }
231 class_instances c ++ is }
@@ -319,6 +323,9 @@ pTrans ts = mapM_ addTrans ts
319pLineApps :: [(FilePath, Int, PTerm)] -> Idris ()
323pLineApps :: [(FilePath, Int, PTerm)] -> Idris ()
320pLineApps ls = mapM_ (\ (f, i, t) -> addInternalApp f i t) ls
324pLineApps ls = mapM_ (\ (f, i, t) -> addInternalApp f i t) ls
321
325
326+pNameHints :: [(Name, Name)] -> Idris ()
327+pNameHints ns = mapM_ (\ (n, ty) -> addNameHint n ty) ns
328+
322----- Generated by 'derive'
329----- Generated by 'derive'
323
330
324instance Binary SizeChange where
331instance Binary SizeChange where
@@ -410,6 +417,7 @@ instance Binary SpecialName where
410 MethodN x1 -> do putWord8 3
417 MethodN x1 -> do putWord8 3
411 put x1
418 put x1
412 CaseN x1 -> do putWord8 4; put x1
419 CaseN x1 -> do putWord8 4; put x1
420+ ElimN x1 -> do putWord8 5; put x1
413 get
421 get
414 = do i <- getWord8
422 = do i <- getWord8
415 case i of
423 case i of
@@ -427,6 +435,8 @@ instance Binary SpecialName where
427 return (MethodN x1)
435 return (MethodN x1)
428 4 -> do x1 <- get
436 4 -> do x1 <- get
429 return (CaseN x1)
437 return (CaseN x1)
438+ 5 -> do x1 <- get
439+ return (ElimN x1)
430 _ -> error "Corrupted binary data for SpecialName"
440 _ -> error "Corrupted binary data for SpecialName"
431
441
432
442
@@ -797,10 +807,7 @@ instance Binary Def where
797 1 -> do x1 <- get
807 1 -> do x1 <- get
798 x2 <- get
808 x2 <- get
799 return (TyDecl x1 x2)
809 return (TyDecl x1 x2)
800− 2 -> do x1 <- get
810+ -- Operator isn't written, don't read
801− x2 <- get
802− x3 <- get
803− return (Operator x1 x2 x3)
804 3 -> do x1 <- get
811 3 -> do x1 <- get
805 x2 <- get
812 x2 <- get
806 x3 <- get
813 x3 <- get
@@ -823,6 +830,20 @@ instance Binary Accessibility where
823 2 -> return Hidden
830 2 -> return Hidden
824 _ -> error "Corrupted binary data for Accessibility"
831 _ -> error "Corrupted binary data for Accessibility"
825
832
833+safeToEnum :: (Enum a, Bounded a, Integral int) => String -> int -> a
834+safeToEnum label x' = result
835+ where
836+ x = fromIntegral x'
837+ result
838+ | x < fromEnum (minBound `asTypeOf` result)
839+ || x > fromEnum (maxBound `asTypeOf` result)
840+ = error $ label ++ ": corrupted binary representation in IBC"
841+ | otherwise = toEnum x
842+
843+instance Binary Forceability where
844+ put = putWord8 . fromIntegral . fromEnum
845+ get = safeToEnum "Forceability" `fmap` getWord8
846+
826instance Binary PReason where
847instance Binary PReason where
827 put x
848 put x
828 = case x of
849 = case x of
@@ -870,7 +891,7 @@ instance Binary Totality where
870 _ -> error "Corrupted binary data for Totality"
891 _ -> error "Corrupted binary data for Totality"
871
892
872instance Binary IBCFile where
893instance Binary IBCFile where
873− put x@(IBCFile x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 x21 x22 x23 x24 x25 x26 x27)
894+ put x@(IBCFile x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 x21 x22 x23 x24 x25 x26 x27 x28)
874 = {-# SCC "putIBCFile" #-}
895 = {-# SCC "putIBCFile" #-}
875 do put x1
896 do put x1
876 put x2
897 put x2
@@ -899,6 +920,7 @@ instance Binary IBCFile where
899 put x25
920 put x25
900 put x26
921 put x26
901 put x27
922 put x27
923+ put x28
902 get
924 get
903 = do x1 <- get
925 = do x1 <- get
904 if x1 == ibcVersion then
926 if x1 == ibcVersion then
@@ -928,9 +950,19 @@ instance Binary IBCFile where
928 x25 <- get
950 x25 <- get
929 x26 <- get
951 x26 <- get
930 x27 <- get
952 x27 <- get
953+ x28 <- get
931− return (IBCFile x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 x21 x22 x23 x24 x25 x26 x27)
954+ return (IBCFile x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 x21 x22 x23 x24 x25 x26 x27 x28)
932 else return (initIBC { ver = x1 })
955 else return (initIBC { ver = x1 })
933
956
957+instance Binary DataOpt where
958+ put x = case x of
959+ Codata -> putWord8 0
960+ DefaultEliminator -> putWord8 1
961+ get = do i <- getWord8
962+ case i of
963+ 0 -> return Codata
964+ 1 -> return DefaultEliminator
965+
934instance Binary FnOpt where
966instance Binary FnOpt where
935 put x
967 put x
936 = case x of
968 = case x of
@@ -1225,7 +1257,7 @@ instance Binary Using where
1225 1 -> do x1 <- get; x2 <- get; return (UConstraint x1 x2)
1257 1 -> do x1 <- get; x2 <- get; return (UConstraint x1 x2)
1226
1258
1227instance Binary SyntaxInfo where
1259instance Binary SyntaxInfo where
1228− put (Syn x1 x2 x3 x4 x5 x6 x7 x8)
1260+ put (Syn x1 x2 x3 x4 _ x5 x6 x7)
1229 = do put x1
1261 = do put x1
1230 put x2
1262 put x2
1231 put x3
1263 put x3
@@ -1233,7 +1265,6 @@ instance Binary SyntaxInfo where
1233 put x5
1265 put x5
1234 put x6
1266 put x6
1235 put x7
1267 put x7
1236− put x8
1237 get
1268 get
1238 = do x1 <- get
1269 = do x1 <- get
1239 x2 <- get
1270 x2 <- get
@@ -1242,8 +1273,7 @@ instance Binary SyntaxInfo where
1242 x5 <- get
1273 x5 <- get
1243 x6 <- get
1274 x6 <- get
1244 x7 <- get
1275 x7 <- get
1245− x8 <- get
1246− return (Syn x1 x2 x3 x4 x5 x6 x7 x8)
1276+ return (Syn x1 x2 x3 x4 id x5 x6 x7)
1247
1277
1248instance (Binary t) => Binary (PClause' t) where
1278instance (Binary t) => Binary (PClause' t) where
1249 put x
1279 put x
@@ -1576,6 +1606,8 @@ instance (Binary t) => Binary (PTactic' t) where
1576 put x1
1606 put x1
1577 Fill x1 -> do putWord8 18
1607 Fill x1 -> do putWord8 18
1578 put x1
1608 put x1
1609+ Induction x1 -> do putWord8 19
1610+ put x1
1579 get
1611 get
1580 = do i <- getWord8
1612 = do i <- getWord8
1581 case i of
1613 case i of
@@ -1613,6 +1645,8 @@ instance (Binary t) => Binary (PTactic' t) where
1613 return (Reflect x1)
1645 return (Reflect x1)
1614 18 -> do x1 <- get
1646 18 -> do x1 <- get
1615 return (Fill x1)
1647 return (Fill x1)
1648+ 19 -> do x1 <- get
1649+ return (Induction x1)
1616 _ -> error "Corrupted binary data for PTactic'"
1650 _ -> error "Corrupted binary data for PTactic'"
1617
1651
1618
1652
@@ -1727,17 +1761,19 @@ instance (Binary t) => Binary (PArg' t) where
1727
1761
1728
1762
1729instance Binary ClassInfo where
1763instance Binary ClassInfo where
1730− put (CI x1 x2 x3 x4 _)
1764+ put (CI x1 x2 x3 x4 x5 _)
1731 = do put x1
1765 = do put x1
1732 put x2
1766 put x2
1733 put x3
1767 put x3
1734 put x4
1768 put x4
1769+ put x5
1735 get
1770 get
1736 = do x1 <- get
1771 = do x1 <- get
1737 x2 <- get
1772 x2 <- get
1738 x3 <- get
1773 x3 <- get
1739 x4 <- get
1774 x4 <- get
1775+ x5 <- get
1740− return (CI x1 x2 x3 x4 [])
1776+ return (CI x1 x2 x3 x4 x5 [])
1741
1777
1742instance Binary OptInfo where
1778instance Binary OptInfo where
1743 put (Optimise x1 x2 x3 x4)
1779 put (Optimise x1 x2 x3 x4)
src/Idris/IdeSlave.hs+3
@@ -66,6 +66,9 @@ instance (SExpable a, SExpable b) => SExpable (a, b) where
66instance (SExpable a, SExpable b, SExpable c) => SExpable (a, b, c) where
66instance (SExpable a, SExpable b, SExpable c) => SExpable (a, b, c) where
67 toSExp (l, m, n) = SexpList [toSExp l, toSExp m, toSExp n]
67 toSExp (l, m, n) = SexpList [toSExp l, toSExp m, toSExp n]
68
68
69+instance (SExpable a, SExpable b, SExpable c, SExpable d) => SExpable (a, b, c, d) where
70+ toSExp (l, m, n, o) = SexpList [toSExp l, toSExp m, toSExp n, toSExp o]
71+
69escape :: String -> String
72escape :: String -> String
70escape = concatMap escapeChar
73escape = concatMap escapeChar
71 where
74 where
src/Idris/ParseData.hs+23−13
@@ -70,13 +70,19 @@ record syn = do (doc, acc) <- try (do
70{- | Parses data declaration type (normal or codata)
70{- | Parses data declaration type (normal or codata)
71DataI ::= 'data' | 'codata';
71DataI ::= 'data' | 'codata';
72-}
72-}
73−dataI :: IdrisParser Bool
73+dataI :: IdrisParser DataOpts
74−dataI = do reserved "data"; return False
74+dataI = do reserved "data"; return []
75− <|> do reserved "codata"; return True
75+ <|> do reserved "codata"; return [Codata]
76+
77+{- | Parses if a data should not have a default eliminator
78+DefaultEliminator ::= 'noelim'?
79+ -}
80+defaultEliminator :: IdrisParser DataOpts
81+defaultEliminator = do option [] (do reserved "%elim"; return [DefaultEliminator])
76
82
77{- | Parses a data type declaration
83{- | Parses a data type declaration
78−Data ::= DocComment? Accessibility? DataI FnName TypeSig ExplicitTypeDataRest?
84+Data ::= DocComment? Accessibility? DataI DefaultEliminator FnName TypeSig ExplicitTypeDataRest?
79− | DocComment? Accessibility? DataI FnName Name* DataRest?
85+ | DocComment? Accessibility? DataI DefaultEliminator FnName Name* DataRest?
80 ;
86 ;
81Constructor' ::= Constructor KeepTerminator;
87Constructor' ::= Constructor KeepTerminator;
82ExplicitTypeDataRest ::= 'where' OpenBlock Constructor'* CloseBlock;
88ExplicitTypeDataRest ::= 'where' OpenBlock Constructor'* CloseBlock;
@@ -90,29 +96,31 @@ SimpleConstructorList ::=
90 ;
96 ;
91-}
97-}
92data_ :: SyntaxInfo -> IdrisParser PDecl
98data_ :: SyntaxInfo -> IdrisParser PDecl
93−data_ syn = do (doc, acc, co) <- try (do
99+data_ syn = do (doc, acc, dataOpts) <- try (do
94 doc <- option "" (docComment '|')
100 doc <- option "" (docComment '|')
95 pushIndent
101 pushIndent
96 acc <- optional accessibility
102 acc <- optional accessibility
103+ elim <- defaultEliminator
97 co <- dataI
104 co <- dataI
105+ let dataOpts = combineDataOpts(elim ++ co)
98− return (doc, acc, co))
106+ return (doc, acc, dataOpts))
99 fc <- getFC
107 fc <- getFC
100 tyn_in <- fnName
108 tyn_in <- fnName
101 (do try (lchar ':')
109 (do try (lchar ':')
102 popIndent
110 popIndent
103 ty <- typeExpr (allowImp syn)
111 ty <- typeExpr (allowImp syn)
104 let tyn = expandNS syn tyn_in
112 let tyn = expandNS syn tyn_in
105− option (PData doc syn fc co (PLaterdecl tyn ty)) (do
113+ option (PData doc syn fc dataOpts (PLaterdecl tyn ty)) (do
106 reserved "where"
114 reserved "where"
107 cons <- indentedBlock (constructor syn)
115 cons <- indentedBlock (constructor syn)
108 accData acc tyn (map (\ (_, n, _, _) -> n) cons)
116 accData acc tyn (map (\ (_, n, _, _) -> n) cons)
109− return $ PData doc syn fc co (PDatadecl tyn ty cons))) <|> (do
117+ return $ PData doc syn fc dataOpts (PDatadecl tyn ty cons))) <|> (do
110 args <- many name
118 args <- many name
111 let ty = bindArgs (map (const PType) args) PType
119 let ty = bindArgs (map (const PType) args) PType
112 let tyn = expandNS syn tyn_in
120 let tyn = expandNS syn tyn_in
113− option (PData doc syn fc co (PLaterdecl tyn ty)) (do
121+ option (PData doc syn fc dataOpts (PLaterdecl tyn ty)) (do
114 try (lchar '=') <|> do reserved "where"
122 try (lchar '=') <|> do reserved "where"
115− let kw = (if co then "co" else "") ++ "data "
123+ let kw = (if DefaultEliminator `elem` dataOpts then "" else "%noelim ") ++ (if Codata `elem` dataOpts then "co" else "") ++ "data "
116 let n = show tyn_in ++ " "
124 let n = show tyn_in ++ " "
117 let s = kw ++ n
125 let s = kw ++ n
118 let as = concat (intersperse " " $ map show args) ++ " "
126 let as = concat (intersperse " " $ map show args) ++ " "
@@ -129,14 +137,16 @@ data_ syn = do (doc, acc, co) <- try (do
129 do let cty = bindArgs cargs conty
137 do let cty = bindArgs cargs conty
130 return (doc, x, cty, cfc)) cons
138 return (doc, x, cty, cfc)) cons
131 accData acc tyn (map (\ (_, n, _, _) -> n) cons')
139 accData acc tyn (map (\ (_, n, _, _) -> n) cons')
132− return $ PData doc syn fc co (PDatadecl tyn ty cons')))
140+ return $ PData doc syn fc dataOpts (PDatadecl tyn ty cons')))
133 <?> "data type declaration"
141 <?> "data type declaration"
134 where
142 where
135 mkPApp :: FC -> PTerm -> [PTerm] -> PTerm
143 mkPApp :: FC -> PTerm -> [PTerm] -> PTerm
136 mkPApp fc t [] = t
144 mkPApp fc t [] = t
137 mkPApp fc t xs = PApp fc t (map pexp xs)
145 mkPApp fc t xs = PApp fc t (map pexp xs)
138 bindArgs :: [PTerm] -> PTerm -> PTerm
146 bindArgs :: [PTerm] -> PTerm -> PTerm
139− bindArgs xs t = foldr (PPi expl (MN 0 "t")) t xs
147+ bindArgs xs t = foldr (PPi expl (MN 0 "_t")) t xs
148+ combineDataOpts :: DataOpts -> DataOpts
149+ combineDataOpts opts = if Codata `elem` opts then delete DefaultEliminator opts else opts
140
150
141
151
142{- | Parses a type constructor declaration
152{- | Parses a type constructor declaration
src/Idris/ParseExpr.hs+127−37
@@ -42,8 +42,10 @@ allowImp syn = syn { implicitAllowed = True }
42disallowImp :: SyntaxInfo -> SyntaxInfo
42disallowImp :: SyntaxInfo -> SyntaxInfo
43disallowImp syn = syn { implicitAllowed = False }
43disallowImp syn = syn { implicitAllowed = False }
44
44
45−{- | Parses an expression as a whole
45+{-| Parses an expression as a whole
46+@
46 FullExpr ::= Expr EOF_t;
47 FullExpr ::= Expr EOF_t;
48+@
47 -}
49 -}
48fullExpr :: SyntaxInfo -> IdrisParser PTerm
50fullExpr :: SyntaxInfo -> IdrisParser PTerm
49fullExpr syn = do x <- expr syn
51fullExpr syn = do x <- expr syn
@@ -53,7 +55,9 @@ fullExpr syn = do x <- expr syn
53
55
54
56
55{- |Parses an expression
57{- |Parses an expression
58+@
56 Expr ::= Expr';
59 Expr ::= Expr';
60+@
57-}
61-}
58expr :: SyntaxInfo -> IdrisParser PTerm
62expr :: SyntaxInfo -> IdrisParser PTerm
59expr syn = do i <- get
63expr syn = do i <- get
@@ -61,10 +65,10 @@ expr syn = do i <- get
61
65
62{- | Parses either an internally defined expression or
66{- | Parses either an internally defined expression or
63 a user-defined one
67 a user-defined one
64−
68+@
65Expr' ::= "External (User-defined) Syntax"
69Expr' ::= "External (User-defined) Syntax"
66 | InternalExpr;
70 | InternalExpr;
67−
71+@
68 -}
72 -}
69expr' :: SyntaxInfo -> IdrisParser PTerm
73expr' :: SyntaxInfo -> IdrisParser PTerm
70expr' syn = try (externalExpr syn)
74expr' syn = try (externalExpr syn)
@@ -92,7 +96,7 @@ simpleExternalExpr syn = do i <- get
92 _ -> False
96 _ -> False
93 isSimple _ = False
97 isSimple _ = False
94
98
95−{- | Tries to parse a user-defined expression given a list of syntactic extensions -}
99+{- | Tries to parse a user-defined expression given a list of syntactic extensions -}
96extensions :: SyntaxInfo -> [Syntax] -> IdrisParser PTerm
100extensions :: SyntaxInfo -> [Syntax] -> IdrisParser PTerm
97extensions syn rules = choice (map (try . extension syn) (filter isValid rules))
101extensions syn rules = choice (map (try . extension syn) (filter isValid rules))
98 <?> "user-defined expression"
102 <?> "user-defined expression"
@@ -160,8 +164,8 @@ extension syn (Rule ssym ptm _)
160 update ns (PGoal fc r n sc) = PGoal fc (update ns r) n (update ns sc)
164 update ns (PGoal fc r n sc) = PGoal fc (update ns r) n (update ns sc)
161 update ns t = t
165 update ns t = t
162
166
163−{- |Parses a (normal) built-in expression
167+{- | Parses a (normal) built-in expression
164−
168+@
165InternalExpr ::=
169InternalExpr ::=
166 App
170 App
167 | MatchApp
171 | MatchApp
@@ -173,8 +177,9 @@ InternalExpr ::=
173 | Let
177 | Let
174 | RewriteTerm
178 | RewriteTerm
175 | Pi
179 | Pi
176− | DoBlock
180+ | DoBlock
177 ;
181 ;
182+@
178-}
183-}
179internalExpr :: SyntaxInfo -> IdrisParser PTerm
184internalExpr :: SyntaxInfo -> IdrisParser PTerm
180internalExpr syn =
185internalExpr syn =
@@ -193,8 +198,10 @@ internalExpr syn =
193 <?> "expression"
198 <?> "expression"
194
199
195{- | Parses a case expression
200{- | Parses a case expression
201+@
196CaseExpr ::=
202CaseExpr ::=
197 'case' Expr 'of' OpenBlock CaseOption+ CloseBlock;
203 'case' Expr 'of' OpenBlock CaseOption+ CloseBlock;
204+@
198-}
205-}
199caseExpr :: SyntaxInfo -> IdrisParser PTerm
206caseExpr :: SyntaxInfo -> IdrisParser PTerm
200caseExpr syn = do reserved "case"; fc <- getFC
207caseExpr syn = do reserved "case"; fc <- getFC
@@ -204,9 +211,11 @@ caseExpr syn = do reserved "case"; fc <- getFC
204 <?> "case expression"
211 <?> "case expression"
205
212
206{- | Parses a case in a case expression
213{- | Parses a case in a case expression
214+@
207CaseOption ::=
215CaseOption ::=
208 Expr '=>' Expr Terminator
216 Expr '=>' Expr Terminator
209 ;
217 ;
218+@
210-}
219-}
211caseOption :: SyntaxInfo -> IdrisParser (PTerm, PTerm)
220caseOption :: SyntaxInfo -> IdrisParser (PTerm, PTerm)
212caseOption syn = do lhs <- expr (syn { inPattern = True })
221caseOption syn = do lhs <- expr (syn { inPattern = True })
@@ -215,9 +224,11 @@ caseOption syn = do lhs <- expr (syn { inPattern = True })
215 <?> "case option"
224 <?> "case option"
216
225
217{- | Parses a proof block
226{- | Parses a proof block
227+@
218ProofExpr ::=
228ProofExpr ::=
219 'proof' OpenBlock Tactic'* CloseBlock
229 'proof' OpenBlock Tactic'* CloseBlock
220 ;
230 ;
231+@
221-}
232-}
222proofExpr :: SyntaxInfo -> IdrisParser PTerm
233proofExpr :: SyntaxInfo -> IdrisParser PTerm
223proofExpr syn = do reserved "proof"
234proofExpr syn = do reserved "proof"
@@ -225,10 +236,12 @@ proofExpr syn = do reserved "proof"
225 return $ PProof ts
236 return $ PProof ts
226 <?> "proof block"
237 <?> "proof block"
227
238
228−{- | Parses a tactics block
239+{- | Parses a tactics block
240+@
229TacticsExpr :=
241TacticsExpr :=
230 'tactics' OpenBlock Tactic'* CloseBlock
242 'tactics' OpenBlock Tactic'* CloseBlock
231;
243;
244+@
232-}
245-}
233tacticsExpr :: SyntaxInfo -> IdrisParser PTerm
246tacticsExpr :: SyntaxInfo -> IdrisParser PTerm
234tacticsExpr syn = do reserved "tactics"
247tacticsExpr syn = do reserved "tactics"
@@ -236,7 +249,8 @@ tacticsExpr syn = do reserved "tactics"
236 return $ PTactics ts
249 return $ PTactics ts
237 <?> "tactics block"
250 <?> "tactics block"
238
251
239−{- | Parses a simple expresion
252+{- | Parses a simple expression
253+@
240SimpleExpr ::=
254SimpleExpr ::=
241 '![' Term ']'
255 '![' Term ']'
242 | '?' Name
256 | '?' Name
@@ -257,6 +271,7 @@ SimpleExpr ::=
257 | '_'
271 | '_'
258 | {- External (User-defined) Simple Expression -}
272 | {- External (User-defined) Simple Expression -}
259 ;
273 ;
274+@
260-}
275-}
261simpleExpr :: SyntaxInfo -> IdrisParser PTerm
276simpleExpr :: SyntaxInfo -> IdrisParser PTerm
262simpleExpr syn =
277simpleExpr syn =
@@ -267,6 +282,7 @@ simpleExpr syn =
267 tm <- option Placeholder (do lchar '{'; t <- expr syn; lchar '}';
282 tm <- option Placeholder (do lchar '{'; t <- expr syn; lchar '}';
268 return t)
283 return t)
269 return (PRefl fc tm)
284 return (PRefl fc tm)
285+ <|> do reserved "elim_for"; fc <- getFC; t <- fnName; return (PRef fc (SN $ ElimN t))
270 <|> proofExpr syn
286 <|> proofExpr syn
271 <|> tacticsExpr syn
287 <|> tacticsExpr syn
272 <|> caseExpr syn
288 <|> caseExpr syn
@@ -295,7 +311,8 @@ simpleExpr syn =
295 <?> "expression"
311 <?> "expression"
296
312
297
313
298−{- |Parses the rest of an expression in braces
314+{- |Parses the rest of an expression in braces
315+@
299Bracketed ::=
316Bracketed ::=
300 ')'
317 ')'
301 | Expr ')'
318 | Expr ')'
@@ -305,6 +322,7 @@ Bracketed ::=
305 | Expr Operator ')'
322 | Expr Operator ')'
306 | Name ':' Expr '**' Expr ')'
323 | Name ':' Expr '**' Expr ')'
307 ;
324 ;
325+@
308-}
326-}
309bracketed :: SyntaxInfo -> IdrisParser PTerm
327bracketed :: SyntaxInfo -> IdrisParser PTerm
310bracketed syn =
328bracketed syn =
@@ -377,15 +395,17 @@ modifyConst syn fc (PConstant (BI x))
377modifyConst syn fc x = x
395modifyConst syn fc x = x
378
396
379{- | Parses a list literal expression e.g. [1,2,3]
397{- | Parses a list literal expression e.g. [1,2,3]
398+@
380ListExpr ::=
399ListExpr ::=
381 '[' ExprList? ']'
400 '[' ExprList? ']'
382;
401;
383−
402+@
403+@
384ExprList ::=
404ExprList ::=
385 Expr
405 Expr
386 | Expr ',' ExprList
406 | Expr ',' ExprList
387 ;
407 ;
388−
408+@
389 -}
409 -}
390listExpr :: SyntaxInfo -> IdrisParser PTerm
410listExpr :: SyntaxInfo -> IdrisParser PTerm
391listExpr syn = do lchar '['; fc <- getFC; xs <- sepBy (expr syn) (lchar ','); lchar ']'
411listExpr syn = do lchar '['; fc <- getFC; xs <- sepBy (expr syn) (lchar ','); lchar ']'
@@ -398,22 +418,26 @@ listExpr syn = do lchar '['; fc <- getFC; xs <- sepBy (expr syn) (lchar ','); lc
398
418
399
419
400{- | Parses an alternative expression
420{- | Parses an alternative expression
421+@
401 Alt ::= '(|' Expr_List '|)';
422 Alt ::= '(|' Expr_List '|)';
402
423
403 Expr_List ::=
424 Expr_List ::=
404 Expr'
425 Expr'
405 | Expr' ',' Expr_List
426 | Expr' ',' Expr_List
406 ;
427 ;
428+@
407-}
429-}
408alt :: SyntaxInfo -> IdrisParser PTerm
430alt :: SyntaxInfo -> IdrisParser PTerm
409alt syn = do symbol "(|"; alts <- sepBy1 (expr' syn) (lchar ','); symbol "|)"
431alt syn = do symbol "(|"; alts <- sepBy1 (expr' syn) (lchar ','); symbol "|)"
410 return (PAlternative False alts)
432 return (PAlternative False alts)
411
433
412{- | Parses a possibly hidden simple expression
434{- | Parses a possibly hidden simple expression
435+@
413HSimpleExpr ::=
436HSimpleExpr ::=
414 '.' SimpleExpr
437 '.' SimpleExpr
415 | SimpleExpr
438 | SimpleExpr
416 ;
439 ;
440+@
417-}
441-}
418hsimpleExpr :: SyntaxInfo -> IdrisParser PTerm
442hsimpleExpr :: SyntaxInfo -> IdrisParser PTerm
419hsimpleExpr syn =
443hsimpleExpr syn =
@@ -424,9 +448,11 @@ hsimpleExpr syn =
424 <?> "expression"
448 <?> "expression"
425
449
426{- | Parses a matching application expression
450{- | Parses a matching application expression
451+@
427MatchApp ::=
452MatchApp ::=
428 SimpleExpr '<==' FnName
453 SimpleExpr '<==' FnName
429 ;
454 ;
455+@
430-}
456-}
431matchApp :: SyntaxInfo -> IdrisParser PTerm
457matchApp :: SyntaxInfo -> IdrisParser PTerm
432matchApp syn = do ty <- simpleExpr syn
458matchApp syn = do ty <- simpleExpr syn
@@ -451,9 +477,11 @@ unifyLog syn = do lchar '%'; reserved "unifyLog";
451 <?> "unification log expression"
477 <?> "unification log expression"
452
478
453{- | Parses a no implicits expression
479{- | Parses a no implicits expression
480+@
454NoImplicits ::=
481NoImplicits ::=
455 '%' 'noImplicits' SimpleExpr
482 '%' 'noImplicits' SimpleExpr
456 ;
483 ;
484+@
457-}
485-}
458noImplicits :: SyntaxInfo -> IdrisParser PTerm
486noImplicits :: SyntaxInfo -> IdrisParser PTerm
459noImplicits syn = do lchar '%'; reserved "noImplicits";
487noImplicits syn = do lchar '%'; reserved "noImplicits";
@@ -462,10 +490,12 @@ noImplicits syn = do lchar '%'; reserved "noImplicits";
462 <?> "no implicits expression"
490 <?> "no implicits expression"
463
491
464{- | Parses a function application expression
492{- | Parses a function application expression
493+@
465App ::=
494App ::=
466 'mkForeign' Arg Arg*
495 'mkForeign' Arg Arg*
467 | SimpleExpr Arg+
496 | SimpleExpr Arg+
468 ;
497 ;
498+@
469-}
499-}
470app :: SyntaxInfo -> IdrisParser PTerm
500app :: SyntaxInfo -> IdrisParser PTerm
471app syn = do f <- reserved "mkForeign"
501app syn = do f <- reserved "mkForeign"
@@ -499,12 +529,14 @@ app syn = do f <- reserved "mkForeign"
499 = desugar (syn { dsl_info = d }) i (getTm a)
529 = desugar (syn { dsl_info = d }) i (getTm a)
500 dslify i t = t
530 dslify i t = t
501
531
502−{- |Parses a function argument
532+{-| Parses a function argument
533+@
503Arg ::=
534Arg ::=
504 ImplicitArg
535 ImplicitArg
505 | ConstraintArg
536 | ConstraintArg
506 | SimpleExpr
537 | SimpleExpr
507 ;
538 ;
539+@
508-}
540-}
509arg :: SyntaxInfo -> IdrisParser PArg
541arg :: SyntaxInfo -> IdrisParser PArg
510arg syn = implicitArg syn
542arg syn = implicitArg syn
@@ -513,10 +545,12 @@ arg syn = implicitArg syn
513 return (pexp e)
545 return (pexp e)
514 <?> "function argument"
546 <?> "function argument"
515
547
516−{- |Parses an implicit function argument
548+{-| Parses an implicit function argument
549+@
517ImplicitArg ::=
550ImplicitArg ::=
518 '{' Name ('=' Expr)? '}'
551 '{' Name ('=' Expr)? '}'
519 ;
552 ;
553+@
520-}
554-}
521implicitArg :: SyntaxInfo -> IdrisParser PArg
555implicitArg :: SyntaxInfo -> IdrisParser PArg
522implicitArg syn = do lchar '{'
556implicitArg syn = do lchar '{'
@@ -528,10 +562,12 @@ implicitArg syn = do lchar '{'
528 return (pimp n v False)
562 return (pimp n v False)
529 <?> "implicit function argument"
563 <?> "implicit function argument"
530
564
531−{- |Parses a constraint argument (for selecting a named type class instance)
565+{-| Parses a constraint argument (for selecting a named type class instance)
566+
532−ConstraintArg ::=
567+> ConstraintArg ::=
533− '@{' Expr '}'
568+> '@{' Expr '}'
534− ;
569+> ;
570+
535-}
571-}
536constraintArg :: SyntaxInfo -> IdrisParser PArg
572constraintArg :: SyntaxInfo -> IdrisParser PArg
537constraintArg syn = do symbol "@{"
573constraintArg syn = do symbol "@{"
@@ -541,18 +577,22 @@ constraintArg syn = do symbol "@{"
541 <?> "constraint argument"
577 <?> "constraint argument"
542
578
543
579
544−{- |Parses a record field setter expression
580+{-| Parses a record field setter expression
581+@
545RecordType ::=
582RecordType ::=
546 'record' '{' FieldTypeList '}';
583 'record' '{' FieldTypeList '}';
547−
584+@
585+@
548FieldTypeList ::=
586FieldTypeList ::=
549 FieldType
587 FieldType
550 | FieldType ',' FieldTypeList
588 | FieldType ',' FieldTypeList
551 ;
589 ;
552−
590+@
591+@
553FieldType ::=
592FieldType ::=
554 FnName '=' Expr
593 FnName '=' Expr
555 ;
594 ;
595+@
556-}
596-}
557recordType :: SyntaxInfo -> IdrisParser PTerm
597recordType :: SyntaxInfo -> IdrisParser PTerm
558recordType syn
598recordType syn
@@ -579,17 +619,21 @@ recordType syn
579 applyAll fc ((n, e) : es) x
619 applyAll fc ((n, e) : es) x
580 = applyAll fc es (PApp fc (PRef fc (mkType n)) [pexp e, pexp x])
620 = applyAll fc es (PApp fc (PRef fc (mkType n)) [pexp e, pexp x])
581
621
582−{- |Creates setters for record types on necessary functions -}
622+-- | Creates setters for record types on necessary functions
583mkType :: Name -> Name
623mkType :: Name -> Name
584mkType (UN n) = UN ("set_" ++ n)
624mkType (UN n) = UN ("set_" ++ n)
585mkType (MN 0 n) = MN 0 ("set_" ++ n)
625mkType (MN 0 n) = MN 0 ("set_" ++ n)
586mkType (NS n s) = NS (mkType n) s
626mkType (NS n s) = NS (mkType n) s
587
627
588−{- |Parses a type signature
628+{- | Parses a type signature
629+@
589TypeSig ::=
630TypeSig ::=
590 ':' Expr
631 ':' Expr
591 ;
632 ;
633+@
634+@
592TypeExpr ::= ConstraintList? Expr;
635TypeExpr ::= ConstraintList? Expr;
636+@
593 -}
637 -}
594typeExpr :: SyntaxInfo -> IdrisParser PTerm
638typeExpr :: SyntaxInfo -> IdrisParser PTerm
595typeExpr syn = do cs <- if implicitAllowed syn then constraintList syn else return []
639typeExpr syn = do cs <- if implicitAllowed syn then constraintList syn else return []
@@ -597,15 +641,19 @@ typeExpr syn = do cs <- if implicitAllowed syn then constraintList syn else retu
597 return (bindList (PPi constraint) (map (\x -> (MN 0 "c", x)) cs) sc)
641 return (bindList (PPi constraint) (map (\x -> (MN 0 "c", x)) cs) sc)
598 <?> "type signature"
642 <?> "type signature"
599
643
600−{- |Parses a lambda expression
644+{- | Parses a lambda expression
645+@
601Lambda ::=
646Lambda ::=
602 '\\' TypeOptDeclList '=>' Expr
647 '\\' TypeOptDeclList '=>' Expr
603 | '\\' SimpleExprList '=>' Expr
648 | '\\' SimpleExprList '=>' Expr
604 ;
649 ;
650+@
651+@
605SimpleExprList ::=
652SimpleExprList ::=
606 SimpleExpr
653 SimpleExpr
607 | SimpleExpr ',' SimpleExprList
654 | SimpleExpr ',' SimpleExprList
608 ;
655 ;
656+@
609-}
657-}
610lambda :: SyntaxInfo -> IdrisParser PTerm
658lambda :: SyntaxInfo -> IdrisParser PTerm
611lambda syn = do lchar '\\'
659lambda syn = do lchar '\\'
@@ -627,10 +675,12 @@ lambda syn = do lchar '\\'
627 (PCase fc (PRef fc (MN i "lamp"))
675 (PCase fc (PRef fc (MN i "lamp"))
628 [(x, pmList xs sc)])
676 [(x, pmList xs sc)])
629
677
630−{- |Parses a term rewrite expression
678+{- | Parses a term rewrite expression
679+@
631RewriteTerm ::=
680RewriteTerm ::=
632 'rewrite' Expr ('==>' Expr)? 'in' Expr
681 'rewrite' Expr ('==>' Expr)? 'in' Expr
633 ;
682 ;
683+@
634-}
684-}
635rewriteTerm :: SyntaxInfo -> IdrisParser PTerm
685rewriteTerm :: SyntaxInfo -> IdrisParser PTerm
636rewriteTerm syn = do reserved "rewrite"
686rewriteTerm syn = do reserved "rewrite"
@@ -644,6 +694,7 @@ rewriteTerm syn = do reserved "rewrite"
644 <?> "term rewrite expression"
694 <?> "term rewrite expression"
645
695
646{- |Parses a let binding
696{- |Parses a let binding
697+@
647Let ::=
698Let ::=
648 'let' Name TypeSig'? '=' Expr 'in' Expr
699 'let' Name TypeSig'? '=' Expr 'in' Expr
649| 'let' Expr' '=' Expr' 'in' Expr
700| 'let' Expr' '=' Expr' 'in' Expr
@@ -651,6 +702,7 @@ Let ::=
651TypeSig' ::=
702TypeSig' ::=
652 ':' Expr'
703 ':' Expr'
653 ;
704 ;
705+@
654 -}
706 -}
655let_ :: SyntaxInfo -> IdrisParser PTerm
707let_ :: SyntaxInfo -> IdrisParser PTerm
656let_ syn = try (do reserved "let"; n <- name;
708let_ syn = try (do reserved "let"; n <- name;
@@ -665,10 +717,13 @@ let_ syn = try (do reserved "let"; n <- name;
665 return (PCase fc v [(pat, sc)]))
717 return (PCase fc v [(pat, sc)]))
666 <?> "let binding"
718 <?> "let binding"
667
719
668−{- |Parses a quote goal
720+{- | Parses a quote goal
721+
722+@
669QuoteGoal ::=
723QuoteGoal ::=
670 'quoteGoal' Name 'by' Expr 'in' Expr
724 'quoteGoal' Name 'by' Expr 'in' Expr
671 ;
725 ;
726+@
672 -}
727 -}
673quoteGoal :: SyntaxInfo -> IdrisParser PTerm
728quoteGoal :: SyntaxInfo -> IdrisParser PTerm
674quoteGoal syn = do reserved "quoteGoal"; n <- name;
729quoteGoal syn = do reserved "quoteGoal"; n <- name;
@@ -680,13 +735,15 @@ quoteGoal syn = do reserved "quoteGoal"; n <- name;
680 return (PGoal fc r n sc)
735 return (PGoal fc r n sc)
681 <?> "quote goal expression"
736 <?> "quote goal expression"
682
737
683−{- |Parses a dependent type signature
738+{- | Parses a dependent type signature
739+@
684Pi ::=
740Pi ::=
685 '|'? Static? '(' TypeDeclList ')' DocComment '->' Expr
741 '|'? Static? '(' TypeDeclList ')' DocComment '->' Expr
686 | '|'? Static? '{' TypeDeclList '}' '->' Expr
742 | '|'? Static? '{' TypeDeclList '}' '->' Expr
687 | '{' 'auto' TypeDeclList '}' '->' Expr
743 | '{' 'auto' TypeDeclList '}' '->' Expr
688 | '{' 'default' TypeDeclList '}' '->' Expr
744 | '{' 'default' TypeDeclList '}' '->' Expr
689 ;
745 ;
746+@
690 -}
747 -}
691
748
692pi :: SyntaxInfo -> IdrisParser PTerm
749pi :: SyntaxInfo -> IdrisParser PTerm
@@ -728,10 +785,13 @@ pi syn =
728 <?> "dependent type signature"
785 <?> "dependent type signature"
729
786
730{- | Parses a type constraint list
787{- | Parses a type constraint list
788+
789+@
731ConstraintList ::=
790ConstraintList ::=
732 '(' Expr_List ')' '=>'
791 '(' Expr_List ')' '=>'
733 | Expr '=>'
792 | Expr '=>'
734 ;
793 ;
794+@
735-}
795-}
736constraintList :: SyntaxInfo -> IdrisParser [PTerm]
796constraintList :: SyntaxInfo -> IdrisParser [PTerm]
737constraintList syn = try (do lchar '('
797constraintList syn = try (do lchar '('
@@ -745,16 +805,20 @@ constraintList syn = try (do lchar '('
745 <|> return []
805 <|> return []
746 <?> "type constraint list"
806 <?> "type constraint list"
747
807
748−{- |Parses a type declaration list
808+{- | Parses a type declaration list
809+@
749TypeDeclList ::=
810TypeDeclList ::=
750 FunctionSignatureList
811 FunctionSignatureList
751 | NameList TypeSig
812 | NameList TypeSig
752 ;
813 ;
814+@
753
815
816+@
754FunctionSignatureList ::=
817FunctionSignatureList ::=
755 Name TypeSig
818 Name TypeSig
756 | Name TypeSig ',' FunctionSignatureList
819 | Name TypeSig ',' FunctionSignatureList
757 ;
820 ;
821+@
758-}
822-}
759typeDeclList :: SyntaxInfo -> IdrisParser [(Name, PTerm)]
823typeDeclList :: SyntaxInfo -> IdrisParser [(Name, PTerm)]
760typeDeclList syn = try (sepBy1 (do x <- fnName
824typeDeclList syn = try (sepBy1 (do x <- fnName
@@ -768,13 +832,17 @@ typeDeclList syn = try (sepBy1 (do x <- fnName
768 return (map (\x -> (x, t)) ns)
832 return (map (\x -> (x, t)) ns)
769 <?> "type declaration list"
833 <?> "type declaration list"
770
834
771−{- |Parses a type declaration list with optional parameters
835+{- | Parses a type declaration list with optional parameters
836+@
772TypeOptDeclList ::=
837TypeOptDeclList ::=
773 NameOrPlaceholder TypeSig?
838 NameOrPlaceholder TypeSig?
774 | NameOrPlaceholder TypeSig? ',' TypeOptDeclList
839 | NameOrPlaceholder TypeSig? ',' TypeOptDeclList
775 ;
840 ;
841+@
776
842
843+@
777NameOrPlaceHolder ::= Name | '_';
844NameOrPlaceHolder ::= Name | '_';
845+@
778-}
846-}
779tyOptDeclList :: SyntaxInfo -> IdrisParser [(Name, PTerm)]
847tyOptDeclList :: SyntaxInfo -> IdrisParser [(Name, PTerm)]
780tyOptDeclList syn = sepBy1 (do x <- nameOrPlaceholder
848tyOptDeclList syn = sepBy1 (do x <- nameOrPlaceholder
@@ -789,13 +857,17 @@ tyOptDeclList syn = sepBy1 (do x <- nameOrPlaceholder
789 return (MN 0 "underscore")
857 return (MN 0 "underscore")
790 <?> "name or placeholder"
858 <?> "name or placeholder"
791
859
792−{- |Parses a list comprehension
860+{- | Parses a list comprehension
861+@
793Comprehension ::= '[' Expr '|' DoList ']';
862Comprehension ::= '[' Expr '|' DoList ']';
863+@
794
864
865+@
795DoList ::=
866DoList ::=
796 Do
867 Do
797 | Do ',' DoList
868 | Do ',' DoList
798 ;
869 ;
870+@
799-}
871-}
800comprehension :: SyntaxInfo -> IdrisParser PTerm
872comprehension :: SyntaxInfo -> IdrisParser PTerm
801comprehension syn
873comprehension syn
@@ -814,12 +886,16 @@ comprehension syn
814 [pexp e])
886 [pexp e])
815 addGuard x = x
887 addGuard x = x
816
888
817−{- |Parses a do-block
889+{- | Parses a do-block
890+@
818Do' ::= Do KeepTerminator;
891Do' ::= Do KeepTerminator;
892+@
819
893
894+@
820DoBlock ::=
895DoBlock ::=
821 'do' OpenBlock Do'+ CloseBlock
896 'do' OpenBlock Do'+ CloseBlock
822 ;
897 ;
898+@
823 -}
899 -}
824doBlock :: SyntaxInfo -> IdrisParser PTerm
900doBlock :: SyntaxInfo -> IdrisParser PTerm
825doBlock syn
901doBlock syn
@@ -828,7 +904,8 @@ doBlock syn
828 return (PDoBlock ds)
904 return (PDoBlock ds)
829 <?> "do block"
905 <?> "do block"
830
906
831−{- |Parses an expression inside a do block
907+{- | Parses an expression inside a do block
908+@
832Do ::=
909Do ::=
833 'let' Name TypeSig'? '=' Expr
910 'let' Name TypeSig'? '=' Expr
834 | 'let' Expr' '=' Expr
911 | 'let' Expr' '=' Expr
@@ -836,6 +913,7 @@ Do ::=
836 | Expr' '<-' Expr
913 | Expr' '<-' Expr
837 | Expr
914 | Expr
838 ;
915 ;
916+@
839-}
917-}
840do_ :: SyntaxInfo -> IdrisParser PDo
918do_ :: SyntaxInfo -> IdrisParser PDo
841do_ syn
919do_ syn
@@ -868,8 +946,10 @@ do_ syn
868 return (DoExp fc e)
946 return (DoExp fc e)
869 <?> "do block expression"
947 <?> "do block expression"
870
948
871−{- |Parses an expression in idiom brackets
949+{- | Parses an expression in idiom brackets
950+@
872Idiom ::= '[|' Expr '|]';
951Idiom ::= '[|' Expr '|]';
952+@
873-}
953-}
874idiom :: SyntaxInfo -> IdrisParser PTerm
954idiom :: SyntaxInfo -> IdrisParser PTerm
875idiom syn
955idiom syn
@@ -881,6 +961,8 @@ idiom syn
881 <?> "expression in idiom brackets"
961 <?> "expression in idiom brackets"
882
962
883{- |Parses a constant or literal expression
963{- |Parses a constant or literal expression
964+
965+@
884Constant ::=
966Constant ::=
885 'Integer'
967 'Integer'
886 | 'Int'
968 | 'Int'
@@ -901,6 +983,7 @@ Constant ::=
901 | String_t
983 | String_t
902 | Char_t
984 | Char_t
903 ;
985 ;
986+@
904-}
987-}
905constant :: IdrisParser Idris.Core.TT.Const
988constant :: IdrisParser Idris.Core.TT.Const
906constant = do reserved "Integer";return (AType (ATInt ITBig))
989constant = do reserved "Integer";return (AType (ATInt ITBig))
@@ -923,17 +1006,22 @@ constant = do reserved "Integer";return (AType (ATInt ITBig))
923 <|> try (do c <- charLiteral; return $ Ch c)
1006 <|> try (do c <- charLiteral; return $ Ch c)
924 <?> "constant or literal"
1007 <?> "constant or literal"
925
1008
926−{- |Parses a static modifier
1009+{- | Parses a static modifier
1010+
1011+@
927Static ::=
1012Static ::=
928 '[' static ']'
1013 '[' static ']'
929;
1014;
1015+@
930-}
1016-}
931static :: IdrisParser Static
1017static :: IdrisParser Static
932static = do lchar '['; reserved "static"; lchar ']'; return Static
1018static = do lchar '['; reserved "static"; lchar ']'; return Static
933 <|> return Dynamic
1019 <|> return Dynamic
934 <?> "static modifier"
1020 <?> "static modifier"
935
1021
936−{- | Parses a tactic script
1022+{- | Parses a tactic script
1023+
1024+@
937Tactic ::= 'intro' NameList?
1025Tactic ::= 'intro' NameList?
938 | 'intros'
1026 | 'intros'
939 | 'refine' Name Imp+
1027 | 'refine' Name Imp+
@@ -967,7 +1055,7 @@ TacticSeq ::=
967 Tactic ';' Tactic
1055 Tactic ';' Tactic
968 | Tactic ';' TacticSeq
1056 | Tactic ';' TacticSeq
969 ;
1057 ;
970−
1058+@
971-}
1059-}
972
1060
973tactic :: SyntaxInfo -> IdrisParser PTactic
1061tactic :: SyntaxInfo -> IdrisParser PTactic
@@ -986,6 +1074,8 @@ tactic syn = do reserved "intro"; ns <- sepBy (indentPropHolds gtProp *> name) (
986 <|> do reserved "rewrite"; t <- (indentPropHolds gtProp *> expr syn);
1074 <|> do reserved "rewrite"; t <- (indentPropHolds gtProp *> expr syn);
987 i <- get
1075 i <- get
988 return $ Rewrite (desugar syn i t)
1076 return $ Rewrite (desugar syn i t)
1077+ <|> do reserved "induction"; nm <- (indentPropHolds gtProp *> name);
1078+ return $ Induction nm
989 <|> do reserved "equiv"; t <- (indentPropHolds gtProp *> expr syn);
1079 <|> do reserved "equiv"; t <- (indentPropHolds gtProp *> expr syn);
990 i <- get
1080 i <- get
991 return $ Equiv (desugar syn i t)
1081 return $ Equiv (desugar syn i t)
@@ -1040,7 +1130,7 @@ tactic syn = do reserved "intro"; ns <- sepBy (indentPropHolds gtProp *> name) (
1040 mergeSeq [t] = t
1130 mergeSeq [t] = t
1041 mergeSeq (t:ts) = TSeq t (mergeSeq ts)
1131 mergeSeq (t:ts) = TSeq t (mergeSeq ts)
1042
1132
1043−{- | Parses a tactic as a whole -}
1133+-- | Parses a tactic as a whole
1044fullTactic :: SyntaxInfo -> IdrisParser PTactic
1134fullTactic :: SyntaxInfo -> IdrisParser PTactic
1045fullTactic syn = do t <- tactic syn
1135fullTactic syn = do t <- tactic syn
1046 eof
1136 eof
src/Idris/ParseOps.hs+23−14
@@ -29,8 +29,8 @@ import qualified Data.HashSet as HS
29import qualified Data.Text as T
29import qualified Data.Text as T
30import qualified Data.ByteString.UTF8 as UTF8
30import qualified Data.ByteString.UTF8 as UTF8
31
31
32−{- |Creates table for fixity declarations to build expression parser using
32+-- | Creates table for fixity declarations to build expression parser
33− pre-build and user-defined operator/fixity declarations -}
33+-- using pre-build and user-defined operator/fixity declarations
34table :: [FixDecl] -> OperatorTable IdrisParser PTerm
34table :: [FixDecl] -> OperatorTable IdrisParser PTerm
35table fixes
35table fixes
36 = [[prefix "-" (\fc x -> PApp fc (PRef fc (UN "-"))
36 = [[prefix "-" (\fc x -> PApp fc (PRef fc (UN "-"))
@@ -40,7 +40,7 @@ table fixes
40 [binary "=" PEq AssocLeft],
40 [binary "=" PEq AssocLeft],
41 [binary "->" (\fc x y -> PPi expl (MN 42 "__pi_arg") x y) AssocRight]]
41 [binary "->" (\fc x y -> PPi expl (MN 42 "__pi_arg") x y) AssocRight]]
42
42
43−{- |Calculates table for fixtiy declarations -}
43+-- | Calculates table for fixtiy declarations
44toTable :: [FixDecl] -> OperatorTable IdrisParser PTerm
44toTable :: [FixDecl] -> OperatorTable IdrisParser PTerm
45toTable fs = map (map toBin)
45toTable fs = map (map toBin)
46 (groupBy (\ (Fix x _) (Fix y _) -> prec x == prec y) fs)
46 (groupBy (\ (Fix x _) (Fix y _) -> prec x == prec y) fs)
@@ -52,20 +52,20 @@ toTable fs = map (map toBin)
52 assoc (Infixr _) = AssocRight
52 assoc (Infixr _) = AssocRight
53 assoc (InfixN _) = AssocNone
53 assoc (InfixN _) = AssocNone
54
54
55−{- |Binary operator -}
55+-- | Binary operator
56binary :: String -> (FC -> PTerm -> PTerm -> PTerm) -> Assoc -> Operator IdrisParser PTerm
56binary :: String -> (FC -> PTerm -> PTerm -> PTerm) -> Assoc -> Operator IdrisParser PTerm
57binary name f = Infix (do fc <- getFC
57binary name f = Infix (do fc <- getFC
58 reservedOp name
58 reservedOp name
59 doc <- option "" (docComment '^')
59 doc <- option "" (docComment '^')
60 return (f fc))
60 return (f fc))
61
61
62−{- |Prefix operator -}
62+-- | Prefix operator
63prefix :: String -> (FC -> PTerm -> PTerm) -> Operator IdrisParser PTerm
63prefix :: String -> (FC -> PTerm -> PTerm) -> Operator IdrisParser PTerm
64prefix name f = Prefix (do reservedOp name
64prefix name f = Prefix (do reservedOp name
65 fc <- getFC
65 fc <- getFC
66 return (f fc))
66 return (f fc))
67
67
68−{- |Backtick operator -}
68+-- | Backtick operator
69backtick :: Operator IdrisParser PTerm
69backtick :: Operator IdrisParser PTerm
70backtick = Infix (do lchar '`'; n <- fnName
70backtick = Infix (do lchar '`'; n <- fnName
71 lchar '`'
71 lchar '`'
@@ -75,22 +75,29 @@ backtick = Infix (do lchar '`'; n <- fnName
75{- | Parses an operator in function position i.e. enclosed by `()', with an
75{- | Parses an operator in function position i.e. enclosed by `()', with an
76 optional namespace
76 optional namespace
77
77
78+@
78 OperatorFront ::= (Identifier_t '.')? '(' Operator_t ')';
79 OperatorFront ::= (Identifier_t '.')? '(' Operator_t ')';
80+@
81+
79-}
82-}
80operatorFront :: IdrisParser Name
83operatorFront :: IdrisParser Name
81operatorFront = maybeWithNS (lchar '(' *> operator <* lchar ')') False []
84operatorFront = maybeWithNS (lchar '(' *> operator <* lchar ')') False []
82
85
83{- | Parses a function (either normal name or operator)
86{- | Parses a function (either normal name or operator)
87+
88+@
84− FnName ::= Name | OperatorFront;
89+ FnName ::= Name | OperatorFront;
90+@
85-}
91-}
86fnName :: IdrisParser Name
92fnName :: IdrisParser Name
87fnName = try operatorFront <|> name <?> "function name"
93fnName = try operatorFront <|> name <?> "function name"
88
94
89{- | Parses a fixity declaration
95{- | Parses a fixity declaration
90−
96+@
91Fixity ::=
97Fixity ::=
92 FixityType Natural_t OperatorList Terminator
98 FixityType Natural_t OperatorList Terminator
93 ;
99 ;
100+@
94-}
101-}
95fixity :: IdrisParser PDecl
102fixity :: IdrisParser PDecl
96fixity = do pushIndent
103fixity = do pushIndent
@@ -121,12 +128,14 @@ fixity = do pushIndent
121 extractName (Fix _ n) = n
128 extractName (Fix _ n) = n
122
129
123{- | Parses a fixity declaration type (i.e. infix or prefix, associtavity)
130{- | Parses a fixity declaration type (i.e. infix or prefix, associtavity)
131+@
124−FixityType ::=
132+ FixityType ::=
125− 'infixl'
133+ 'infixl'
126− | 'infixr'
134+ | 'infixr'
127− | 'infix'
135+ | 'infix'
128− | 'prefix'
136+ | 'prefix'
129− ;
137+ ;
138+@
130 -}
139 -}
131fixityType :: IdrisParser (Int -> Fixity)
140fixityType :: IdrisParser (Int -> Fixity)
132fixityType = do reserved "infixl"; return Infixl
141fixityType = do reserved "infixl"; return Infixl
src/Idris/Parser.hs+47−17
@@ -437,16 +437,35 @@ namespace syn =
437 return [PNamespace n (concat ds)]
437 return [PNamespace n (concat ds)]
438 <?> "namespace declaration"
438 <?> "namespace declaration"
439
439
440−{- |Parses a methods block (for type classes and instances)
440+{- |Parses a methods block (for instances)
441− MethodsBlock ::= 'where' OpenBlock FnDecl* CloseBlock
441+ InstanceBlock ::= 'where' OpenBlock FnDecl* CloseBlock
442 -}
442 -}
443−methodsBlock :: SyntaxInfo -> IdrisParser [PDecl]
443+instanceBlock :: SyntaxInfo -> IdrisParser [PDecl]
444−methodsBlock syn = do reserved "where"
444+instanceBlock syn = do reserved "where"
445− openBlock
445+ openBlock
446− ds <- many (fnDecl syn)
446+ ds <- many (fnDecl syn)
447− closeBlock
447+ closeBlock
448− return (concat ds)
448+ return (concat ds)
449+ <?> "instance block"
450+
451+{- |Parses a methods and instances block (for type classes)
452+
453+MethodOrInstance ::=
454+ FnDecl
455+ | Instance
456+ ;
457+
458+ClassBlock ::=
459+ 'where' OpenBlock MethodOrInstance* CloseBlock
460+ ;
461+-}
462+classBlock :: SyntaxInfo -> IdrisParser [PDecl]
463+classBlock syn = do reserved "where"
464+ openBlock
465+ ds <- many ((notEndBlock >> instance_ syn) <|> fnDecl syn)
466+ closeBlock
467+ return (concat ds)
449− <?> "methods block"
468+ <?> "class block"
450
469
451{- |Parses a type class declaration
470{- |Parses a type class declaration
452
471
@@ -456,7 +475,7 @@ ClassArgument ::=
456 ;
475 ;
457
476
458Class ::=
477Class ::=
459− DocComment_t? Accessibility? 'class' ConstraintList? Name ClassArgument* MethodsBlock?
478+ DocComment_t? Accessibility? 'class' ConstraintList? Name ClassArgument* ClassBlock?
460 ;
479 ;
461-}
480-}
462class_ :: SyntaxInfo -> IdrisParser [PDecl]
481class_ :: SyntaxInfo -> IdrisParser [PDecl]
@@ -467,7 +486,7 @@ class_ syn = do (doc, acc) <- try (do
467 reserved "class"; fc <- getFC; cons <- constraintList syn; n_in <- name
486 reserved "class"; fc <- getFC; cons <- constraintList syn; n_in <- name
468 let n = expandNS syn n_in
487 let n = expandNS syn n_in
469 cs <- many carg
488 cs <- many carg
470− ds <- option [] (methodsBlock syn)
489+ ds <- option [] (classBlock syn)
471 accData acc n (concatMap declared ds)
490 accData acc n (concatMap declared ds)
472 return [PClass doc syn fc cons n cs ds]
491 return [PClass doc syn fc cons n cs ds]
473 <?> "type-class declaration"
492 <?> "type-class declaration"
@@ -481,7 +500,7 @@ class_ syn = do (doc, acc) <- try (do
481{- |Parses a type class instance declaration
500{- |Parses a type class instance declaration
482
501
483 Instance ::=
502 Instance ::=
484− 'instance' InstanceName? ConstraintList? Name SimpleExpr* MethodsBlock?
503+ 'instance' InstanceName? ConstraintList? Name SimpleExpr* InstanceBlock?
485 ;
504 ;
486
505
487 InstanceName ::= '[' Name ']';
506 InstanceName ::= '[' Name ']';
@@ -494,9 +513,9 @@ instance_ syn = do reserved "instance"; fc <- getFC
494 args <- many (simpleExpr syn)
513 args <- many (simpleExpr syn)
495 let sc = PApp fc (PRef fc cn) (map pexp args)
514 let sc = PApp fc (PRef fc cn) (map pexp args)
496 let t = bindList (PPi constraint) (map (\x -> (MN 0 "c", x)) cs) sc
515 let t = bindList (PPi constraint) (map (\x -> (MN 0 "c", x)) cs) sc
497− ds <- option [] (methodsBlock syn)
516+ ds <- option [] (instanceBlock syn)
498 return [PInstance syn fc cs cn args t en ds]
517 return [PInstance syn fc cs cn args t en ds]
499− <?> "instance declaratioN"
518+ <?> "instance declaration"
500 where instanceName :: IdrisParser Name
519 where instanceName :: IdrisParser Name
501 instanceName = do lchar '['; n_in <- fnName; lchar ']'
520 instanceName = do lchar '['; n_in <- fnName; lchar ']'
502 let n = expandNS syn n_in
521 let n = expandNS syn n_in
@@ -797,6 +816,7 @@ Directive' ::= 'lib' CodeGen String_t
797 | 'default' Totality
816 | 'default' Totality
798 | 'logging' Natural
817 | 'logging' Natural
799 | 'dynamic' StringList
818 | 'dynamic' StringList
819+ | 'name' Name NameList
800 | 'language' 'TypeProviders'
820 | 'language' 'TypeProviders'
801 | 'language' 'ErrorReflection'
821 | 'language' 'ErrorReflection'
802 ;
822 ;
@@ -839,6 +859,12 @@ directive syn = do try (lchar '%' *> reserved "lib"); cgn <- codegen_; lib <- st
839 Left lib -> addIBC (IBCDyLib (lib_name lib))
859 Left lib -> addIBC (IBCDyLib (lib_name lib))
840 Right msg ->
860 Right msg ->
841 fail $ msg)]
861 fail $ msg)]
862+ <|> do try (lchar '%' *> reserved "name")
863+ ty <- iName []
864+ ns <- sepBy1 name (lchar ',')
865+ return [PDirective
866+ (do mapM_ (addNameHint ty) ns
867+ mapM_ (\n -> addIBC (IBCNameHint (ty, n))) ns)]
842 <|> do try (lchar '%' *> reserved "language"); ext <- pLangExt;
868 <|> do try (lchar '%' *> reserved "language"); ext <- pLangExt;
843 return [PDirective (addLangExt ext)]
869 return [PDirective (addLangExt ext)]
844 <?> "directive"
870 <?> "directive"
@@ -919,7 +945,8 @@ findFC :: Doc -> (FC, String)
919findFC x = let s = show (plain x) in
945findFC x = let s = show (plain x) in
920 case span (/= ':') s of
946 case span (/= ':') s of
921 (failname, ':':rest) -> case span isDigit rest of
947 (failname, ':':rest) -> case span isDigit rest of
948+ (line, ':':rest') -> case span isDigit rest' of
922− (line, ':':rest') -> (FC failname (read line) 0, drop 2 (dropWhile (/= ':') rest'))
949+ (col, ':':msg) -> (FC failname (read line) (read col), msg)
923
950
924-- | A program is a list of declarations, possibly with associated
951-- | A program is a list of declarations, possibly with associated
925-- documentation strings.
952-- documentation strings.
@@ -1021,7 +1048,7 @@ loadSource h lidr f
1021 f file pos
1048 f file pos
1022 unless (null ds') $ do
1049 unless (null ds') $ do
1023 let ds = namespaces mname ds'
1050 let ds = namespaces mname ds'
1024− logLvl 3 (dumpDecls ds)
1051+ logLvl 3 (showDecls True ds)
1025 i <- getIState
1052 i <- getIState
1026 logLvl 10 (show (toAlist (idris_implicits i)))
1053 logLvl 10 (show (toAlist (idris_implicits i)))
1027 logLvl 3 (show (idris_infixes i))
1054 logLvl 3 (show (idris_infixes i))
@@ -1047,7 +1074,10 @@ loadSource h lidr f
1047 -- Redo totality check for deferred names
1074 -- Redo totality check for deferred names
1048 let deftots = idris_defertotcheck i
1075 let deftots = idris_defertotcheck i
1049 iLOG $ "Totality checking " ++ show deftots
1076 iLOG $ "Totality checking " ++ show deftots
1077+ mapM_ (\x -> do tot <- getTotality x
1078+ case tot of
1050− mapM_ (\x -> setTotality x Unchecked) (map snd deftots)
1079+ Total _ -> setTotality x Unchecked
1080+ _ -> return ()) (map snd deftots)
1051 mapM_ buildSCG deftots
1081 mapM_ buildSCG deftots
1052 mapM_ checkDeclTotality deftots
1082 mapM_ checkDeclTotality deftots
1053
1083
src/Idris/REPL.hs+25−18
@@ -224,9 +224,7 @@ ideslave orig mods
224 do clearErr
224 do clearErr
225 putIState (orig { idris_options = idris_options i,
225 putIState (orig { idris_options = idris_options i,
226 idris_outputmode = (IdeSlave id) })
226 idris_outputmode = (IdeSlave id) })
227− idrisCatch (do mod <- loadModule' stdout filename
227+ loadInputs stdout [filename]
228− return ())
229− (setAndReport)
230 isetPrompt (mkPrompt [filename])
228 isetPrompt (mkPrompt [filename])
231 -- Report either success or failure
229 -- Report either success or failure
232 i <- getIState
230 i <- getIState
@@ -346,7 +344,7 @@ processInput stvar cmd orig inputs
346 , idris_colourTheme = idris_colourTheme i
344 , idris_colourTheme = idris_colourTheme i
347 }
345 }
348 clearErr
346 clearErr
349− mod <- loadModule stdout f
347+ mod <- loadInputs stdout [f]
350 return (Just [f])
348 return (Just [f])
351 Success (ModImport f) ->
349 Success (ModImport f) ->
352 do clearErr
350 do clearErr
@@ -629,7 +627,8 @@ process h fn (AddMissing updatefile l n)
629
627
630 extras <- case lookupCtxt n' (idris_patdefs i) of
628 extras <- case lookupCtxt n' (idris_patdefs i) of
631 [] -> return ""
629 [] -> return ""
630+ [(_, tms)] -> do tms' <- nameMissing tms
632− [(_, tms)] -> showNew (show n ++ "_rhs") 1 indent tms
631+ showNew (show n ++ "_rhs") 1 indent tms'
633 let (nonblank, rest) = span (not . all isSpace) (tyline:later)
632 let (nonblank, rest) = span (not . all isSpace) (tyline:later)
634 if updatefile
633 if updatefile
635 then do let fb = fn ++ "~"
634 then do let fb = fn ++ "~"
@@ -708,7 +707,7 @@ process h fn (DoProofSearch updatefile l n hints)
708 if updatefile then
707 if updatefile then
709 do let fb = fn ++ "~"
708 do let fb = fn ++ "~"
710 runIO $ writeFile fb (unlines before ++
709 runIO $ writeFile fb (unlines before ++
711− updateMeta tyline (show n) newmv ++ "\n"
710+ updateMeta False tyline (show n) newmv ++ "\n"
712 ++ unlines later)
711 ++ unlines later)
713 runIO $ copyFile fb fn
712 runIO $ copyFile fb fn
714 else ihPrintResult h newmv
713 else ihPrintResult h newmv
@@ -726,16 +725,23 @@ process h fn (DoProofSearch updatefile l n hints)
726 nsroot (SN (WhereN _ _ n)) = nsroot n
725 nsroot (SN (WhereN _ _ n)) = nsroot n
727 nsroot n = n
726 nsroot n = n
728
727
729− updateMeta ('?':cs) n new
728+ updateMeta brack ('?':cs) n new
730 | length cs >= length n
729 | length cs >= length n
731 = case splitAt (length n) cs of
730 = case splitAt (length n) cs of
732 (mv, c:cs) ->
731 (mv, c:cs) ->
733 if (isSpace c && mv == n)
732 if (isSpace c && mv == n)
734− then new ++ (c : cs)
733+ then addBracket brack new ++ (c : cs)
735− else '?' : mv ++ c : updateMeta cs n new
734+ else '?' : mv ++ c : updateMeta True cs n new
736− (mv, []) -> if (mv == n) then new else '?' : mv
735+ (mv, []) -> if (mv == n) then addBracket brack new else '?' : mv
736+ updateMeta brack ('=':cs) n new = '=':updateMeta False cs n new
737+ updateMeta brack (c:cs) n new
737− updateMeta (c:cs) n new = c : updateMeta cs n new
738+ = c : updateMeta (brack || not (isSpace c)) cs n new
738− updateMeta [] n new = ""
739+ updateMeta brack [] n new = ""
740+
741+ addBracket False new = new
742+ addBracket True new@('(':xs) | last xs == ')' = new
743+ addBracket True new | any isSpace new = '(' : new ++ ")"
744+ | otherwise = new
739
745
740process h fn (Spec t)
746process h fn (Spec t)
741 = do (tm, ty) <- elabVal toplevel False t
747 = do (tm, ty) <- elabVal toplevel False t
@@ -1094,6 +1100,7 @@ idrisMain opts =
1094 let nobanner = NoBanner `elem` opts
1100 let nobanner = NoBanner `elem` opts
1095 let idesl = Ideslave `elem` opts
1101 let idesl = Ideslave `elem` opts
1096 let runrepl = not (NoREPL `elem` opts)
1102 let runrepl = not (NoREPL `elem` opts)
1103+ let verbose = runrepl || Verbose `elem` opts
1097 let output = opt getOutput opts
1104 let output = opt getOutput opts
1098 let ibcsubdir = opt getIBCSubDir opts
1105 let ibcsubdir = opt getIBCSubDir opts
1099 let importdirs = opt getImportDir opts
1106 let importdirs = opt getImportDir opts
@@ -1126,14 +1133,13 @@ idrisMain opts =
1126 setREPL runrepl
1133 setREPL runrepl
1127 setQuiet (quiet || isJust script)
1134 setQuiet (quiet || isJust script)
1128 setIdeSlave idesl
1135 setIdeSlave idesl
1129− setVerbose runrepl
1136+ setVerbose verbose
1130 setCmdLine opts
1137 setCmdLine opts
1131 setOutputTy outty
1138 setOutputTy outty
1132 setCodegen cgn
1139 setCodegen cgn
1133 setTargetTriple trpl
1140 setTargetTriple trpl
1134 setTargetCPU tcpu
1141 setTargetCPU tcpu
1135 setOptLevel optimize
1142 setOptLevel optimize
1136− when (Verbose `elem` opts) $ setVerbose True
1137 mapM_ makeOption opts
1143 mapM_ makeOption opts
1138 -- if we have the --bytecode flag, drop into the bytecode assembler
1144 -- if we have the --bytecode flag, drop into the bytecode assembler
1139 case bcs of
1145 case bcs of
@@ -1178,10 +1184,11 @@ idrisMain opts =
1178
1184
1179 historyFile <- fmap (</> "repl" </> "history") getIdrisUserDataDir
1185 historyFile <- fmap (</> "repl" </> "history") getIdrisUserDataDir
1180
1186
1181− when (runrepl && not idesl) $ initScript
1187+ when (runrepl && not idesl) $ do
1188+ initScript
1182− stvar <- runIO $ newMVar ist
1189+ stvar <- runIO $ newMVar ist
1183− when (runrepl && not idesl) $ startServer ist stvar inputs
1190+ startServer ist stvar inputs
1184− when (runrepl && not idesl) $ runInputT (replSettings (Just historyFile)) $ repl ist stvar inputs
1191+ runInputT (replSettings (Just historyFile)) $ repl ist stvar inputs
1185 when (idesl) $ ideslaveStart ist inputs
1192 when (idesl) $ ideslaveStart ist inputs
1186 ok <- noErrors
1193 ok <- noErrors
1187 when (not ok) $ runIO (exitWith (ExitFailure 1))
1194 when (not ok) $ runIO (exitWith (ExitFailure 1))
src/Pkg/Package.hs+1−1
@@ -70,7 +70,7 @@ installPkg pkgdesc
70 mapM_ (installObj (pkgname pkgdesc)) (objs pkgdesc)
70 mapM_ (installObj (pkgname pkgdesc)) (objs pkgdesc)
71
71
72buildMods :: [Opt] -> [Name] -> IO ()
72buildMods :: [Opt] -> [Name] -> IO ()
73−buildMods opts ns = do let f = map (toPath . show) ns
73+buildMods opts ns = do let f = map (toPath . showCG) ns
74-- putStrLn $ "MODULE: " ++ show f
74-- putStrLn $ "MODULE: " ++ show f
75 idris (map Filename f ++ opts)
75 idris (map Filename f ++ opts)
76 return ()
76 return ()
test/reg028/expected+2−2
@@ -1,2 +1,2 @@
1−reg028.idr:5:1:tbad.bad is possibly not total due to: {tbad.bad12}
1+reg028.idr:5:1:tbad.bad is possibly not total due to: {tbad.bad16}
2−reg028a.idr:11:1:tbad.qsort' is possibly not total due to: {tbad.qsort'14}
2+reg028a.idr:11:1:tbad.qsort' is possibly not total due to: {tbad.qsort'18}
test/test032/expected+3−3
@@ -1,8 +1,8 @@
1Type checking ./test032.idr
1Type checking ./test032.idr
2isElem x [] = ?isElem_rhs_1
2isElem x [] = ?isElem_rhs_1
3−isElem x (_ :: _) = ?isElem_rhs_3
3+isElem x (y :: xs) = ?isElem_rhs_3
4
4
5− localZipWith f (_ :: _) (_ :: _) = ?localZipWith_rhs_1
5+ localZipWith f (_ :: _) (x :: ys) = ?localZipWith_rhs_1
6
6
7f x :: (map f xs)
7f x :: (map f xs)
8isElem2 x (y :: ys) with (_)
8isElem2 x (y :: ys) with (_)
@@ -10,5 +10,5 @@ isElem2 x (y :: ys) with (_)
10 isElem3 x (x :: ys) | (Yes refl) = ?isElem3_rhs_3
10 isElem3 x (x :: ys) | (Yes refl) = ?isElem3_rhs_3
11
11
12 [] => ?bar_1
12 [] => ?bar_1
13− (_ :: _) => ?bar_2
13+ (x :: ys) => ?bar_2
14
14
test/test035/expectednew file

No changes to the content.

test/test035/runnew file+3
@@ -0,0 +1,3 @@
1+#!/usr/bin/env bash
2+idris --check $@ test035.idr
3+rm -f *.ibc
test/test035/test035.idrnew file+9
@@ -0,0 +1,9 @@
1+module Main
2+
3+import Syntax.PreorderReasoning
4+import Control.Isomorphism
5+
6+stupidProof : Iso (Either a b) (Either a b)
7+stupidProof {a} {b} = (Either a b) ={ eitherComm }=
8+ (Either b a) ={ eitherComm }=
9+ (Either a b) QED