git.iko.soy/Idris-dev
on master help sign in
Merge remote-tracking branch 'refs/remotes/upstream/master' into wip/tactical
commit8a07216215bad578a37401201ed7f9aa588cdb21 authorDavid Raymond Christiansen <david@davidchristiansen.dk> dateWed 27 May 2015, 10:21 (11 years ago) parent9b949955f33e4a
40 files changed+708−307
compare with master
unifiedsplit
CHANGELOG+6 config.mk+4−1 docs/faq/faq.rst+24 docs/index.rst+2 docs/proofs/pluscomm.rst+2−2 docs/reference/ide-protocol.rst+191 docs/tutorial/provisional.rst+13−4 docs/tutorial/typesfuns.rst+4−4 idris.cabal+9−6 jsrts/Runtime-node.js+2−2 libs/base/Data/Complex.idr+3−1 libs/base/Language/Reflection/Utils.idr+113−97 libs/contrib/Data/Heap.idr+2−2 libs/prelude/Prelude.idr+1−100 libs/prelude/Prelude/Show.idr+187 libs/prelude/prelude.ipkg+1−1 rts/Makefile+2−2 src/IRTS/CodegenC.hs+1−1 src/IRTS/CodegenJavaScript.hs+5−5 src/Idris/AbsSyntax.hs+6−6 src/Idris/Core/Binary.hs−6 src/Idris/Delaborate.hs+4−4 src/Idris/Elab/Class.hs+44−16 src/Idris/Parser.hs+12−6 test/basic006/expected+2−2 test/disambig001/disambig001.idr+1−1 test/disambig001/expected+1−1 test/proof002/expected+4−4 test/quasiquote001/expected+3−3 test/reg007/expected+4−4 test/reg023/expected+2−2 test/reg044/expected+4−4 test/reg054/expected+2−2 test/reg065/expected test/reg065/reg065.idr+26 test/reg065/run+3 test/tutorial006/expected+8−8 test/unique001/expected+6−6 test/unique002/expected+2−2 test/unique003/expected+2−2
CHANGELOG+6
@@ -1,3 +1,9 @@
1+New in 0.9.19:
2+--------------
3+* The Show class has been moved into Prelude.Show and augmented with the method
4+ showPrec, which allows correct parenthesization of showed terms. This comes
5+ with the type Prec of precedences and a few helper functions.
6+
17New in 0.9.18:
28--------------
39* GHC 7.10 compatibility
config.mk+4−1
@@ -1,8 +1,11 @@
11CC ?=cc
2+AR ?=ar
3+RANLIB ?=ranlib
4+
25CABAL :=cabal
36# IDRIS_ENABLE_STATS should not be set in final release
47# Any flags defined here which alter the RTS API must also be added to src/IRTS/CodegenC.hs
5−CFLAGS :=-O2 -Wall -DHAS_PTHREAD -DIDRIS_ENABLE_STATS -msse2 $(CFLAGS)
8+CFLAGS :=-O2 -Wall -DHAS_PTHREAD -DIDRIS_ENABLE_STATS $(CFLAGS)
69
710#CABALFLAGS :=
811## Disable building of Effects
docs/faq/faq.rst+24
@@ -99,6 +99,30 @@ the difference between:
9999 Idris> \n, m => n + (S m)
100100 \n => \m => plus n (S m) : Nat -> Nat -> Nat
101101
102+I have an obviously terminating program, but Idris says it possibly isn't total. Why is that?
103+=============================================================================================
104+
105+Idris can't decide in general whether a program is terminating due to
106+the undecidability of the `Halting Problem
107+<https://en.wikipedia.org/wiki/Halting_problem>`_. It is possible, however,
108+to identify some programs which are definitely terminating. Idris does this
109+using "size change termination" which looks for recursive paths from a
110+function back to itself. On such a path, there must be at least one
111+argument which converges to a base case.
112+
113+- Mutually recursive functions are supported
114+- However, all functions on the path must be fully applied. In particular,
115+ higher order applications are not supported
116+- Idris identifies arguments which converge to a base case by looking for
117+ recursive calls to syntactically smaller arguments of inputs. e.g.
118+ ``k`` is syntactially smaller than ``S (S k)`` because ``k`` is a
119+ subterm of ``S (S k)``, but ``(k, k)`` is
120+ not syntactically smaller than ``(S k, S k)``.
121+
122+If you have a function which you believe to be terminating, but Idris does
123+not, you can either restructure the program, or use the ``assert_total``
124+function.
125+
102126When will Idris be self-hosting?
103127================================
104128
docs/index.rst+2
@@ -104,6 +104,7 @@ Language Reference
104104 reference/uniqueness-types
105105 reference/ffi
106106 reference/erasure
107+ reference/ide-protocol
107108
108109.. _guides:
109110
@@ -115,3 +116,4 @@ Short Guides
115116 :maxdepth: 1
116117
117118 guides/type-providers-ffi
119+
docs/proofs/pluscomm.rst+2−2
@@ -88,9 +88,9 @@ error:
8888::
8989
9090 When elaborating right hand side of four_eq_five:
91− Can't unify
91+ Type mismatch between
9292 x = x (Type of Refl)
93− with
93+ and
9494 4 = 5 (Expected type)
9595
9696Type checking equality proofs
docs/reference/ide-protocol.rstnew file+191
@@ -0,0 +1,191 @@
1+********************
2+The IDE Protocol
3+********************
4+
5+The Idris REPL has two modes of interaction: a human-readable syntax designed for direct use in a terminal, and a machine-readable syntax designed for using Idris as a backend for external tools.
6+
7+Protocol Overview
8+-----------------
9+
10+The communication protocol is of asynchronous request-reply style: a single request from the client is handled by Idris at a time.
11+Idris waits for a request on its standard input stream, and outputs the answer or answers to standard output.
12+The result of a request can be either success, failure, or intermediate output; and furthermore, before the result is delivered, there might be additional meta-messages.
13+
14+
15+A reply can consist of multiple messages: any number of messages to inform the user about the progress of the request or other informational output, and finally a result, either ``ok`` or ``error``.
16+
17+The wire format is the length of the message in characters, encoded in 6 characters hexadecimal, followed by the message encoded as S-expression (sexp).
18+Additionally, each request includes a unique integer (counting upwards), which is repeated in all messages corresponding to that request.
19+
20+An example interaction from loading the file ``/home/hannes/empty.idr`` looks as follows on the wire:::
21+
22+ 00002a((:load-file "/home/hannes/empty.idr") 1)
23+ 000039(:write-string "Type checking /home/hannes/empty.idr" 1)
24+ 000025(:set-prompt "/home/hannes/empty" 1)
25+ 000032(:return (:ok "Loaded /home/hannes/empty.idr") 1)
26+
27+
28+The first message is the request from idris-mode to load the specific file, which length is hex 2a, decimal 42 (including the newline at the end).
29+The request identifier is set to 1.
30+The first message from Idris is to write the string ``Type checking /home/hannes/empty.idr'', another is to set the prompt to ``*/home/hannes/empty''.
31+The answer, starting with ``:return`` is ``ok``, and additional information is that the file was loaded.
32+
33+There are three atoms in the wire language: numbers, strings, and symbols.
34+The only compound object is a list, which is surrounded by parenthesis.
35+The syntax is::
36+
37+ A ::= NUM | '"' STR '"' | ':' ALPHA+
38+ S ::= A | '(' S* ')' | nil
39+
40+where ``NUM`` is either 0 or a positive integer, ``ALPHA`` is an alphabetical character, and ``STR`` is the contents of a string, with ``"`` escaped by a backslash.
41+The atom ``nil`` is accepted instead of ``()`` for compatibility with some regexp pretty-printing routines.
42+
43+The state of the Idris process is mainly the active file, which needs to be kept synchronized between the editor and Idris.
44+This is achieved by the already seen ``:load-file`` command.
45+
46+The available commands include:
47+
48+ ``(:load-file FILENAME)``
49+ Load the named file
50+
51+ ``(:interpret STRING)``
52+ Interpret ``STRING`` at the Idris REPL, returning a highlighted result
53+
54+ ``(:repl-completions STRING)``
55+ Return the result of tab-completing ``STRING`` as a REPL command
56+
57+ ``(:type-of STRING)``
58+ Return the type of the name, written with Idris syntax in the ``STRING``.
59+ The reply may contain highlighting information.
60+
61+ ``(:case-split LINE NAME)``
62+ Generate a case-split for the pattern variable ``NAME`` on program line ``LINE``.
63+ The pattern-match cases to be substituted are returned as a string with no highlighting.
64+
65+ ``(:add-clause LINE NAME)``
66+ Generate an initial pattern-match clause for the function declared as ``NAME`` on program line ``LINE``.
67+ The initial clause is returned as a string with no highlighting.
68+
69+ ``(:add-proof-clause LINE NAME)``
70+ Add a clause driven by the ``<==`` syntax.
71+
72+ ``(:add-missing LINE NAME)``
73+ Add the missing cases discovered by totality checking the function declared as ``NAME`` on program line ``LINE``.
74+ The missing clauses are returned as a string with no highlighting.
75+
76+ ``(:make-with LINE NAME)``
77+ Create a with-rule pattern match template for the clause of function ``NAME`` on line ``LINE``.
78+ The new code is returned with no highlighting.
79+
80+ ``(:proof-search LINE NAME HINTS)``
81+ Attempt to fill out the metavariable on ``LINE```named ``NAME`` by proof search.
82+ ``HINTS`` is a possibly-empty list of additional things to try while searching.
83+
84+ ``(:docs-for NAME)``
85+ Look up the documentation for ``NAME``, and return it as a highlighted string.
86+
87+ ``(:metavariables WIDTH)``
88+ List the currently-active metavariables, with their types pretty-printed with ``WIDTH`` columns.
89+
90+ ``(:who-calls NAME)``
91+ Get a list of callers of ``NAME``
92+
93+ ``(:calls-who NAME)``
94+ Get a list of callees of ``NAME``
95+
96+ ``(:browse-namespace NAMESPACE)``
97+ Return the contents of ``NAMESPACE``, like ``:browse`` at the command-line REPL
98+
99+ ``(:normalise-term TM)``
100+ Return a highlighted string consisting of the results of normalising the serialised term ``TM`` (which would previously have been sent as the ``tt-term`` property of a string)
101+
102+ ``(:show-term-implicits TM)``
103+ Return a highlighted string consisting of the results of making all arguments in serialised term ``TM`` (which would previously have been sent as the ``tt-term`` property of a string) explicit.
104+
105+ ``(:hide-term-implicits TM)``
106+ Return a highlighted string consisting of the results of making all arguments in serialised term ``TM`` (which would previously have been sent as the ``tt-term`` property of a string) follow their usual implicitness setting.
107+
108+ ``(:elaborate-term TM)``
109+ Return a highlighted string consisting of the the core language term corresponding to serialised term ``TM`` (which would previously have been sent as the ``tt-term`` property of a string).
110+
111+ ``(:print-definition NAME)``
112+ Return the definition of ``NAME`` as a highlighted string
113+
114+
115+
116+Possible replies include a normal final reply:::
117+
118+ (:return (:ok SEXP [HIGHLIGHTING]))
119+ (:return (:error String [HIGHLIGHTING]))
120+
121+A normal intermediate reply:::
122+
123+ (:output (:ok SEXP [HIGHLIGHTING]))
124+ (:output (:error String [HIGHLIGHTING]))
125+
126+Informational and/or abnormal replies:::
127+
128+ (:write-string String)
129+ (:set-prompt String)
130+ (:warning (FilePath (LINE COL) (LINE COL) String [HIGHLIGHTING]))
131+
132+Proof mode replies:::
133+
134+ (:start-proof-mode)
135+ (:write-proof-state [String] [HIGHLIGHTING])
136+ (:end-proof-mode)
137+ (:write-goal String)
138+
139+Output Highlighting
140+-------------------
141+
142+Idris mode supports highlighting the output from Idris.
143+In reality, this highlighting is controlled by the Idris compiler.
144+Some of the return forms from Idris support an optional extra parameter: a list mapping spans of text to metadata about that text.
145+Clients can then use this list both to highlight the displayed output and to enable richer interaction by having more metadata present.
146+For example, the Emacs mode allows right-clicking identifiers to get a menu with access to documentation and type signatures.
147+
148+
149+A particular semantic span is a three element list.
150+The first element of the list is the index at which the span begins, the second element is the number of characters included in the span, and the third is the semantic data itself.
151+The semantic data is a list of lists.
152+The head of each list is a key that denotes what kind of metadata is in the list, and the tail is the metadata itself.
153+
154+The following keys are available:
155+ ``name``
156+ gives a reference to the fully-qualified Idris name
157+ ``implicit``
158+ provides a Boolean value that is True if the region is the name of an implicit argument
159+ ``decor``
160+ describes the category of a token, which can be ``type``, ``function``, ``data``, ``keyword``, or ``bound``.
161+
162+ ``source-loc``
163+ states that the region refers to a source code location. Its body is a collection of key-value pairs, with the following possibilities:
164+
165+ ``filename``
166+ provides the filename
167+
168+ ``start``
169+ provides the line and column that the source location starts at as a two-element tail
170+
171+ ``end``
172+ provides the line and column that the source location ends at as a two-element tail
173+
174+ ``text-formatting``
175+ provides an attribute of formatted text. This is for use with natural-language text, not code, and is presently emitted only from inline documentation. The potential values are ``bold``, ``italic``, and ``underline``.
176+
177+ ``tt-term``
178+ A serialized representation of the Idris core term corresponding to the region of text.
179+
180+Source Code Highlighting
181+------------------------
182+
183+Idris supports instructing editors how to color their code.
184+When elaborating source code or REPL input, Idris will locate regions of the source code corresponding to names, and emit information about these names using the same metadata as output highlighting.
185+
186+These messages will arrive as replies to the command that caused elaboration to occur, such as ``:load-file`` or ``:interpret``.
187+They have the format:::
188+
189+ (:output (:ok (:highlight-source POSNS)))
190+
191+where ``POSNS``is a list of positions to highlight. Each of these is a two-element list whose first element is a position (encoded as for the ``source-loc`` property above) and whose second element is highlighting metadata in the same format used for output.
docs/tutorial/provisional.rst+13−4
@@ -35,15 +35,15 @@ Unfortunately, the type checker rejects this:
3535::
3636
3737 viewsbroken.idr:12:10:When elaborating right hand side of ViewsBroken.parity:
38− Can't unify
38+ Type mismatch between
3939 Parity (plus (S j) (S j))
40− with
40+ and
4141 Parity (S (S (plus j j)))
4242
4343 Specifically:
44− Can't unify
44+ Type mismatch between
4545 plus (S j) (S j)
46− with
46+ and
4747 S (S (plus j j))
4848
4949The type checker is telling us that ``(j+1)+(j+1)`` and ``2+j+j`` do not
@@ -71,6 +71,15 @@ Provisional definitions are written in the same way as ordinary
7171definitions, except that they introduce the right hand side with a
7272``?=`` rather than ``=``. We define ``parity`` as follows:
7373
74+.. code-block:: idris
75+
76+ parity : (n:Nat) -> Parity n
77+ parity Z = Even {n=Z}
78+ parity (S Z) = Odd {n=Z}
79+ parity (S (S k)) with (parity k)
80+ parity (S (S (j + j))) | Even ?= Even {n=S j}
81+ parity (S (S (S (j + j)))) | Odd ?= Odd {n=S j}
82+
7483When written in this form, instead of reporting a type error, Idris
7584will insert a metavariable standing for a theorem which will correct the
7685type error. Idris tells us we have two proof obligations, with names
docs/tutorial/typesfuns.rst+4−4
@@ -309,15 +309,15 @@ following:
309309 $ idris vbroken.idr --check
310310 vbroken.idr:9:23:When elaborating right hand side of Vect.++:
311311 When elaborating an application of constructor Vect.:::
312− Can't unify
312+ Type mismatch between
313313 Vect (k + k) a (Type of xs ++ xs)
314− with
314+ and
315315 Vect (plus k m) a (Expected type)
316316
317317 Specifically:
318− Can't unify
318+ Type mismatch between
319319 plus k k
320− with
320+ and
321321 plus k m
322322
323323
idris.cabal+9−6
@@ -1,5 +1,5 @@
11Name: idris
2−Version: 0.9.18
2+Version: 0.9.18.1
33License: BSD3
44License-file: LICENSE
55Author: Edwin Brady
@@ -114,7 +114,7 @@ Extra-source-files:
114114 libs/contrib/Classes/*.idr
115115 libs/contrib/Control/*.idr
116116 libs/contrib/Control/Isomorphism/*.idr
117− libs/contrib/Control/Algebra/*.idr
117+ libs/contrib/Control/Algebra/*.idr
118118 libs/contrib/Data/*.idr
119119 libs/contrib/Decidable/*.idr
120120 libs/contrib/Network/*.idr
@@ -314,6 +314,9 @@ Extra-source-files:
314314 test/reg064/run
315315 test/reg064/*.idr
316316 test/reg064/expected
317+ test/reg065/run
318+ test/reg065/*.idr
319+ test/reg065/expected
317320
318321 test/basic001/run
319322 test/basic001/*.idr
@@ -888,7 +891,7 @@ Library
888891 , pretty < 1.2
889892 , process < 1.3
890893 , split < 0.3
891− , text < 1.3
894+ , text >=1.2.1.0 && < 1.3
892895 , time >= 1.4 && < 1.6
893896 , transformers < 0.5
894897 , transformers-compat >= 0.3
@@ -911,7 +914,7 @@ Library
911914 , TemplateHaskell
912915
913916 ghc-prof-options: -auto-all -caf-all
914− ghc-options: -threaded -rtsopts
917+ ghc-options: -threaded -rtsopts -O2
915918
916919 if os(linux)
917920 cpp-options: -DLINUX
@@ -955,7 +958,7 @@ Executable idris
955958 , transformers
956959
957960 ghc-prof-options: -auto-all -caf-all
958− ghc-options: -threaded -rtsopts -funbox-strict-fields
961+ ghc-options: -threaded -rtsopts -funbox-strict-fields -O2
959962
960963Executable idris-c
961964 Main-is: Main.hs
@@ -968,7 +971,7 @@ Executable idris-c
968971 , transformers
969972
970973 ghc-prof-options: -auto-all -caf-all
971− ghc-options: -threaded -rtsopts -funbox-strict-fields
974+ ghc-options: -threaded -rtsopts -funbox-strict-fields -O2
972975
973976Executable idris-javascript
974977 Main-is: Main.hs
jsrts/Runtime-node.js+2−2
@@ -1,7 +1,7 @@
11var i$putStr = (function() {
2− var util = require('util');
2+ var fs = require('fs');
33 return function(s) {
4− util.print(s);
4+ fs.write(1,s);
55 };
66})();
77
libs/base/Data/Complex.idr+3−1
@@ -22,7 +22,9 @@ instance Eq a => Eq (Complex a) where
2222 (==) a b = realPart a == realPart b && imagPart a == imagPart b
2323
2424instance Show a => Show (Complex a) where
25− show (r:+i) = "("++show r++":+"++show i++")"
25+ showPrec d (r :+ i) = showParens (d >= plus_i) $ showPrec plus_i r ++ " :+ " ++ showPrec plus_i i
26+ where plus_i : Prec
27+ plus_i = User 6
2628
2729
2830
libs/base/Language/Reflection/Utils.idr+113−97
@@ -64,23 +64,23 @@ binderTy (PVTy t) = t
6464
6565mutual
6666 instance Show SpecialName where
67− show (WhereN i n1 n2) = "(WhereN " ++ show i ++ " " ++
68− show n1 ++ " " ++ show n2 ++ ")"
69− show (WithN i n) = "(WithN " ++ show i ++ " " ++ show n ++ ")"
70− show (InstanceN i ss) = "(InstanceN " ++ show i ++ " " ++ show ss ++ ")"
71− show (ParentN n s) = "(ParentN " ++ show n ++ " " ++ show s ++ ")"
72− show (MethodN n) = "(MethodN " ++ show n ++ ")"
73− show (CaseN n) = "(CaseN " ++ show n ++ ")"
74− show (ElimN n) = "(ElimN " ++ show n ++ ")"
75− show (InstanceCtorN n) = "(InstanceCtorN " ++ show n ++ ")"
76− show (MetaN parent meta) = "(MetaN " ++ show parent ++ " " ++ show meta ++ ")"
67+ showPrec d (WhereN i n1 n2) = showCon d "WhereN" $ showArg i ++
68+ showArg n1 ++ showArg n2
69+ showPrec d (WithN i n) = showCon d "WithN" $ showArg i ++ showArg n
70+ showPrec d (InstanceN i ss) = showCon d "InstanceN" $ showArg i ++ showArg ss
71+ showPrec d (ParentN n s) = showCon d "ParentN" $ showArg n ++ showArg s
72+ showPrec d (MethodN n) = showCon d "MethodN" $ showArg n
73+ showPrec d (CaseN n) = showCon d "CaseN" $ showArg n
74+ showPrec d (ElimN n) = showCon d "ElimN" $ showArg n
75+ showPrec d (InstanceCtorN n) = showCon d "InstanceCtorN" $ showArg n
76+ showPrec d (MetaN parent meta) = showCon d "MetaN" $ showArg parent ++ showArg meta
7777
7878 instance Show TTName where
79− show (UN str) = "(UN " ++ show str ++ ")"
80− show (NS n ns) = "(NS " ++ show n ++ " " ++ show ns ++ ")"
81− show (MN i str) = "(MN " ++ show i ++ " " ++ show str ++ ")"
82− show (SN sn) = "(SN " ++ assert_total (show sn) ++ ")"
83− show NErased = "NErased"
79+ showPrec d (UN str) = showCon d "UN" $ showArg str
80+ showPrec d (NS n ns) = showCon d "NS" $ showArg n ++ showArg ns
81+ showPrec d (MN i str) = showCon d "MN" $ showArg i ++ showArg str
82+ showPrec d (SN sn) = showCon d "SN" $ assert_total (showArg sn)
83+ showPrec d NErased = "NErased"
8484
8585mutual
8686 instance Eq TTName where
@@ -104,28 +104,44 @@ mutual
104104 _ == _ = False
105105
106106instance Show TTUExp where
107− show (UVar i) = "(UVar " ++ show i ++ ")"
108− show (UVal i) = "(UVal " ++ show i ++ ")"
107+ showPrec d (UVar i) = showCon d "UVar" $ showArg i
108+ showPrec d (UVal i) = showCon d "UVal" $ showArg i
109109
110110instance Eq TTUExp where
111111 (UVar i) == (UVar j) = i == j
112112 (UVal i) == (UVal j) = i == j
113113 x == y = False
114114
115+instance Show NativeTy where
116+ show IT8 = "IT8"
117+ show IT16 = "IT16"
118+ show IT32 = "IT32"
119+ show IT64 = "IT64"
120+
121+instance Show IntTy where
122+ showPrec d (ITFixed t) = showCon d "ITFixed" $ showArg t
123+ showPrec d ITNative = "ITNative"
124+ showPrec d ITBig = "ITBig"
125+ showPrec d ITChar = "ITChar"
126+
127+instance Show ArithTy where
128+ showPrec d (ATInt t) = showCon d "ATInt" $ showArg t
129+ showPrec d ATFloat = "ATFloat"
130+
115131instance Show Const where
116− show (I i) = "(I " ++ show i ++ ")"
117− show (BI n) = "(BI " ++ show n ++ ")"
118− show (Fl f) = "(Fl " ++ show f ++ ")"
119− show (Ch c) = "(Ch " ++ show c ++ ")"
120− show (Str str) = "(Str " ++ show str ++ ")"
121− show (B8 b) = "(B8 ...)"
122− show (B16 b) = "(B16 ...)"
123− show (B32 b) = "(B32 ...)"
124− show (B64 b) = "(B64 ...)"
125− show (AType x) = "(AType ...)"
126− show StrType = "StrType"
127− show VoidType = "VoidType"
128− show Forgot = "Forgot"
132+ showPrec d (I i) = showCon d "I" $ showArg i
133+ showPrec d (BI n) = showCon d "BI" $ showArg n
134+ showPrec d (Fl f) = showCon d "Fl" $ showArg f
135+ showPrec d (Ch c) = showCon d "Ch" $ showArg c
136+ showPrec d (Str str) = showCon d "Str" $ showArg str
137+ showPrec d (B8 b) = showCon d "B8" $ showArg b
138+ showPrec d (B16 b) = showCon d "B16" $ showArg b
139+ showPrec d (B32 b) = showCon d "B32" $ showArg b
140+ showPrec d (B64 b) = showCon d "B64" $ showArg b
141+ showPrec d (AType x) = showCon d "AType" $ showArg x
142+ showPrec d StrType = "StrType"
143+ showPrec d VoidType = "VoidType"
144+ showPrec d Forgot = "Forgot"
129145
130146instance Eq NativeTy where
131147 IT8 == IT8 = True
@@ -164,10 +180,10 @@ instance Eq Const where
164180
165181
166182instance Show NameType where
167− show Bound = "Bound"
168− show Ref = "Ref"
169− show (DCon t ar) = "(DCon " ++ show t ++ " " ++ show ar ++ ")"
170− show (TCon t ar) = "(TCon " ++ show t ++ " " ++ show ar ++ ")"
183+ showPrec d Bound = "Bound"
184+ showPrec d Ref = "Ref"
185+ showPrec d (DCon t ar) = showCon d "DCon" $ showArg t ++ showArg ar
186+ showPrec d (TCon t ar) = showCon d "TCon" $ showArg t ++ showArg ar
171187
172188instance Eq NameType where
173189 Bound == Bound = True
@@ -177,15 +193,15 @@ instance Eq NameType where
177193 x == y = False
178194
179195instance (Show a) => Show (Binder a) where
180− show (Lam t) = "(Lam " ++ show t ++ ")"
181− show (Pi t _) = "(Pi " ++ show t ++ ")"
182− show (Let t1 t2) = "(Let " ++ show t1 ++ " " ++ show t2 ++ ")"
183− show (NLet t1 t2) = "(NLet " ++ show t1 ++ " " ++ show t2 ++ ")"
184− show (Hole t) = "(Hole " ++ show t ++ ")"
185− show (GHole t) = "(GHole " ++ show t ++ ")"
186− show (Guess t1 t2) = "(Guess " ++ show t1 ++ " " ++ show t2 ++ ")"
187− show (PVar t) = "(PVar " ++ show t ++ ")"
188− show (PVTy t) = "(PVTy " ++ show t ++ ")"
196+ showPrec d (Lam t) = showCon d "Lam" $ showArg t
197+ showPrec d (Pi t1 t2) = showCon d "Pi" $ showArg t1 ++ showArg t2
198+ showPrec d (Let t1 t2) = showCon d "Let" $ showArg t1 ++ showArg t2
199+ showPrec d (NLet t1 t2) = showCon d "NLet" $ showArg t1 ++ showArg t2
200+ showPrec d (Hole t) = showCon d "Hole" $ showArg t
201+ showPrec d (GHole t) = showCon d "GHole" $ showArg t
202+ showPrec d (Guess t1 t2) = showCon d "Guess" $ showArg t1 ++ showArg t2
203+ showPrec d (PVar t) = showCon d "PVar" $ showArg t
204+ showPrec d (PVTy t) = showCon d "PVTy" $ showArg t
189205
190206instance (Eq a) => Eq (Binder a) where
191207 (Lam t) == (Lam t') = t == t'
@@ -200,17 +216,17 @@ instance (Eq a) => Eq (Binder a) where
200216 x == y = False
201217
202218instance Show TT where
203− show = my_show
204− where %assert_total my_show : TT -> String
205− my_show (P nt n t) = "(P " ++ show nt ++ " " ++ show n ++ " " ++ show t ++ ")"
206− my_show (V i) = "(V " ++ show i ++ ")"
207− my_show (Bind n b t) = "(Bind " ++ show n ++ " " ++ show b ++ " " ++ show t ++ ")"
208− my_show (App t1 t2) = "(App " ++ show t1 ++ " " ++ show t2 ++ ")"
209− my_show (TConst c) = "(TConst " ++ show c ++ ")"
210− my_show (Proj tm i) = "(Proj " ++ show tm ++ " " ++ show i ++ ")"
211− my_show Erased = "Erased"
212− my_show Impossible = "Impossible"
213− my_show (TType u) = "(TType " ++ show u ++ ")"
219+ showPrec = my_show
220+ where %assert_total my_show : Prec -> TT -> String
221+ my_show d (P nt n t) = showCon d "P" $ showArg nt ++ showArg n ++ showArg t
222+ my_show d (V i) = showCon d "V" $ showArg i
223+ my_show d (Bind n b t) = showCon d "Bind" $ showArg n ++ showArg b ++ showArg t
224+ my_show d (App t1 t2) = showCon d "App" $ showArg t1 ++ showArg t2
225+ my_show d (TConst c) = showCon d "TConst" $ showArg c
226+ my_show d (Proj tm i) = showCon d "Proj" $ showArg tm ++ showArg i
227+ my_show d Erased = "Erased"
228+ my_show d Impossible = "Impossible"
229+ my_show d (TType u) = showCon d "TType" $ showArg u
214230
215231instance Eq TT where
216232 a == b = equalp a b
@@ -251,53 +267,53 @@ forget tm = fe [] tm
251267 fe env Impossible = Nothing
252268
253269instance Show Raw where
254− show r = my_show r
255− where %assert_total my_show : Raw -> String
256− my_show (Var n) = "(Var " ++ show n ++ ")"
257− my_show (RBind n b tm) = "(RBind " ++ show n ++ " " ++ show b ++ " " ++ my_show tm ++ ")"
258− my_show (RApp tm tm') = "(RApp " ++ my_show tm ++ " " ++ my_show tm' ++ ")"
259− my_show RType = "RType"
260− my_show (RForce tm) = "(RForce " ++ my_show tm ++ ")"
261− my_show (RConstant c) = "(RConstant " ++ show c ++ ")"
270+ showPrec = my_show
271+ where %assert_total my_show : Prec -> Raw -> String
272+ my_show d (Var n) = showCon d "Var" $ showArg n
273+ my_show d (RBind n b tm) = showCon d "RBind" $ showArg n ++ showArg b ++ " " ++ my_show App tm
274+ my_show d (RApp tm tm') = showCon d "RApp" $ " " ++ my_show App tm ++ " " ++ my_show App tm'
275+ my_show d RType = "RType"
276+ my_show d (RForce tm) = showCon d "RForce" $ " " ++ my_show App tm
277+ my_show d (RConstant c) = showCon d "RConstant" $ showArg c
262278
263279instance Show SourceLocation where
264− show (FileLoc filename line col) = "FileLoc \"" ++ filename ++ "\" " ++ show line ++ " " ++ show col
280+ showPrec d (FileLoc filename line col) = showCon d "FileLoc" $ showArg filename ++ showArg line ++ showArg col
265281
266282instance Show Err where
267− show (Msg x) = "Msg \"" ++ x ++ "\""
268− show (InternalMsg x) = "InternalMsg \"" ++ x ++ "\""
269− show (CantUnify x tm tm' err xs y) = "CantUnify " ++ show x ++
270− " ( " ++ show tm ++ ") (" ++ show tm' ++ ") (" ++ show err ++ ") " ++
271− show xs ++ " " ++ show y
272− show (InfiniteUnify n tm xs) = "InfiniteUnify " ++ show n ++ show tm ++ show xs
273− show (CantConvert tm tm' xs) = "CantConvert " ++ show tm ++ show tm' ++ show xs
274− show (CantSolveGoal tm ctxt) = "CantSolveGoal " ++ show tm ++ " " ++ show ctxt
275− show (UnifyScope n n' tm xs) = "UnifyScope " ++ show n ++ " " ++ show n' ++ " " ++ show tm ++ " " ++ show xs
276− show (CantInferType x) = "CantInferType " ++ show x
277− show (NonFunctionType tm tm') = "NonFunctionType " ++ show tm ++ show tm'
278− show (NotEquality tm tm') = "NotEquality " ++ show tm ++ " " ++ show tm'
279− show (TooManyArguments n) = "TooManyArguments " ++ show n
280− show (CantIntroduce tm) = "CantIntroduce " ++ show tm
281− show (NoSuchVariable n) = "NoSuchVariable " ++ show n
282− show (WithFnType tm) = "WithFnType " ++ show tm
283− show (CantMatch tm) = "CantMatch " ++ show tm
284− show (NoTypeDecl n) = "NoTypeDecl " ++ show n
285− show (NotInjective tm tm' x) = "NotInjective " ++ show tm ++ " " ++ show tm'
286− show (CantResolve tm) = "CantResolve " ++ show tm
287− show (InvalidTCArg n tm) = "InvalidTCName " ++ show n ++ " (" ++ show tm ++ ")"
288− show (CantResolveAlts xs) = "CantResolveAlts " ++ show xs
289− show (IncompleteTerm tm) = "IncompleteTerm " ++ show tm
290− show (NoEliminator s tm) = "NoEliminator " ++ show s ++ " " ++ show tm
291− show UniverseError = "UniverseError"
292− show ProgramLineComment = "ProgramLineComment"
293− show (Inaccessible n) = "Inaccessible " ++ show n
294− show (UnknownImplicit n f) = "UnknownImplicit " ++ show n ++ " " ++ show f
295− show (NonCollapsiblePostulate n) = "NonCollapsiblePostulate " ++ show n
296− show (AlreadyDefined n) = "AlreadyDefined " ++ show n
297− show (ProofSearchFail err) = "ProofSearchFail " ++ show err
298− show (NoRewriting tm) = "NoRewriting " ++ show tm
299− show (ProviderError x) = "ProviderError \"" ++ show x ++ "\""
300− show (LoadingFailed x err) = "LoadingFailed " ++ show x ++ " (" ++ show err ++ ")"
283+ showPrec d (Msg x) = showCon d "Msg" $ showArg x
284+ showPrec d (InternalMsg x) = showCon d "InternalMsg" $ showArg x
285+ showPrec d (CantUnify x tm tm' err xs y) = showCon d "CantUnify" $ showArg x ++
286+ showArg tm ++ showArg tm' ++ showArg err ++
287+ showArg xs ++ showArg y
288+ showPrec d (InfiniteUnify n tm xs) = showCon d "InfiniteUnify" $ showArg n ++ showArg tm ++ showArg xs
289+ showPrec d (CantConvert tm tm' xs) = showCon d "CantConvert" $ showArg tm ++ showArg tm' ++ showArg xs
290+ showPrec d (CantSolveGoal tm ctxt) = showCon d "CantSolveGoal" $ showArg tm ++ showArg ctxt
291+ showPrec d (UnifyScope n n' tm xs) = showCon d "UnifyScope" $ showArg n ++ showArg n' ++ showArg tm ++ showArg xs
292+ showPrec d (CantInferType x) = showCon d "CantInferType" $ showArg x
293+ showPrec d (NonFunctionType tm tm') = showCon d "NonFunctionType" $ showArg tm ++ showArg tm'
294+ showPrec d (NotEquality tm tm') = showCon d "NotEquality" $ showArg tm ++ showArg tm'
295+ showPrec d (TooManyArguments n) = showCon d "TooManyArguments" $ showArg n
296+ showPrec d (CantIntroduce tm) = showCon d "CantIntroduce" $ showArg tm
297+ showPrec d (NoSuchVariable n) = showCon d "NoSuchVariable" $ showArg n
298+ showPrec d (WithFnType tm) = showCon d "WithFnType" $ showArg tm
299+ showPrec d (CantMatch tm) = showCon d "CantMatch" $ showArg tm
300+ showPrec d (NoTypeDecl n) = showCon d "NoTypeDecl" $ showArg n
301+ showPrec d (NotInjective tm tm' x) = showCon d "NotInjective" $ showArg tm ++ showArg tm'
302+ showPrec d (CantResolve tm) = showCon d "CantResolve" $ showArg tm
303+ showPrec d (InvalidTCArg n tm) = showCon d "InvalidTCName" $ showArg n ++ showArg tm
304+ showPrec d (CantResolveAlts xs) = showCon d "CantResolveAlts" $ showArg xs
305+ showPrec d (IncompleteTerm tm) = showCon d "IncompleteTerm" $ showArg tm
306+ showPrec d (NoEliminator s tm) = showCon d "NoEliminator" $ showArg s ++ showArg tm
307+ showPrec d UniverseError = "UniverseError"
308+ showPrec d ProgramLineComment = "ProgramLineComment"
309+ showPrec d (Inaccessible n) = showCon d "Inaccessible" $ showArg n
310+ showPrec d (UnknownImplicit n f) = showCon d "UnknownImplicit" $ showArg n ++ showArg f
311+ showPrec d (NonCollapsiblePostulate n) = showCon d "NonCollapsiblePostulate" $ showArg n
312+ showPrec d (AlreadyDefined n) = showCon d "AlreadyDefined" $ showArg n
313+ showPrec d (ProofSearchFail err) = showCon d "ProofSearchFail" $ showArg err
314+ showPrec d (NoRewriting tm) = showCon d "NoRewriting" $ showArg tm
315+ showPrec d (ProviderError x) = showCon d "ProviderError" $ showArg x
316+ showPrec d (LoadingFailed x err) = showCon d "LoadingFailed" $ showArg x ++ showArg err
301317
302318-------------------------
303319-- Idiom brackets for Raw
libs/contrib/Data/Heap.idr+2−2
@@ -114,8 +114,8 @@ sort = Heap.toList . Heap.fromList
114114--------------------------------------------------------------------------------
115115
116116instance Show a => Show (MaxiphobicHeap a) where
117− show Empty = "Empty"
118− show (Node s l e r) = "Node (" ++ show l ++ " " ++ show e ++ " " ++ show r ++ ")"
117+ showPrec d Empty = "Empty"
118+ showPrec d (Node s l e r) = showCon d "Node" $ " _" ++ showArg l ++ showArg e ++ showArg r
119119
120120instance Eq a => Eq (MaxiphobicHeap a) where
121121 Empty == Empty = True
libs/prelude/Prelude.idr+1−100
@@ -24,6 +24,7 @@ import public Prelude.Uninhabited
2424import public Prelude.Pairs
2525import public Prelude.Stream
2626import public Prelude.Providers
27+import public Prelude.Show
2728import public Decidable.Equality
2829import public Language.Reflection
2930import public Language.Reflection.Errors
@@ -37,106 +38,6 @@ decAsBool (Yes _) = True
3738decAsBool (No _) = False
3839
3940
40−-- Show and instances
41−
42−class Show a where
43− partial show : a -> String
44−
45−instance Show Int where
46− show = prim__toStrInt
47−
48−instance Show Integer where
49− show = prim__toStrBigInt
50−
51−instance Show Float where
52− show = prim__floatToStr
53−
54−
55−firstCharIs : (Char -> Bool) -> String -> Bool
56−firstCharIs p s with (strM s)
57− firstCharIs p "" | StrNil = False
58− firstCharIs p (strCons c cs) | StrCons c cs = p c
59−
60−protectEsc : (Char -> Bool) -> String -> String -> String
61−protectEsc p f s = f ++ (if firstCharIs p s then "\\&" else "") ++ s
62−
63−showLitChar : Char -> String -> String
64−showLitChar '\a' = ("\\a" ++)
65−showLitChar '\b' = ("\\b" ++)
66−showLitChar '\f' = ("\\f" ++)
67−showLitChar '\n' = ("\\n" ++)
68−showLitChar '\r' = ("\\r" ++)
69−showLitChar '\t' = ("\\t" ++)
70−showLitChar '\v' = ("\\v" ++)
71−showLitChar '\SO' = protectEsc (== 'H') "\\SO"
72−showLitChar '\DEL' = ("\\DEL" ++)
73−showLitChar '\\' = ("\\\\" ++)
74−showLitChar c = case getAt (cast (cast {to=Int} c)) asciiTab of
75− Just k => strCons '\\' . (k ++)
76− Nothing => if (c > '\DEL')
77− then strCons '\\' . protectEsc isDigit (show (cast {to=Int} c))
78− else strCons c
79− where asciiTab : List String
80− asciiTab = ["NUL", "SOH", "STX", "ETX", "EOT", "ENQ", "ACK", "BEL",
81− "BS", "HT", "LF", "VT", "FF", "CR", "SO", "SI",
82− "DLE", "DC1", "DC2", "DC3", "DC4", "NAK", "SYN", "ETB",
83− "CAN", "EM", "SUB", "ESC", "FS", "GS", "RS", "US"]
84−
85− getAt : Nat -> List String -> Maybe String
86− getAt Z (x :: xs) = Just x
87− getAt (S k) (x :: xs) = getAt k xs
88− getAt _ [] = Nothing
89−
90−showLitString : List Char -> String -> String
91−showLitString [] = id
92−showLitString ('"'::cs) = ("\\\"" ++) . showLitString cs
93−showLitString (c ::cs) = showLitChar c . showLitString cs
94−
95−instance Show Char where
96− show '\'' = "'\\''"
97− show c = strCons '\'' (showLitChar c "'")
98−
99−instance Show String where
100− show cs = strCons '"' (showLitString (cast cs) "\"")
101−
102−instance Show Nat where
103− show n = show (the Integer (cast n))
104−
105−instance Show Bool where
106− show True = "True"
107− show False = "False"
108−
109−instance Show () where
110− show () = "()"
111−
112−instance Show Bits8 where
113− show b = b8ToString b
114−
115−instance Show Bits16 where
116− show b = b16ToString b
117−
118−instance Show Bits32 where
119− show b = b32ToString b
120−
121−instance Show Bits64 where
122− show b = b64ToString b
123−
124−instance (Show a, Show b) => Show (a, b) where
125− show (x, y) = "(" ++ show x ++ ", " ++ show y ++ ")"
126−
127−instance Show a => Show (List a) where
128− show xs = "[" ++ show' "" xs ++ "]" where
129− show' acc [] = acc
130− show' acc [x] = acc ++ show x
131− show' acc (x :: xs) = show' (acc ++ show x ++ ", ") xs
132−
133−instance Show a => Show (Maybe a) where
134− show Nothing = "Nothing"
135− show (Just x) = "Just " ++ show x
136−
137−instance (Show a, {y : a} -> Show (p y)) => Show (Sigma a p) where
138− show (y ** prf) = "(" ++ show y ++ " ** " ++ show prf ++ ")"
139−
14041---- Functor instances
14142
14243instance Functor PrimIO where
libs/prelude/Prelude/Show.idrnew file+187
@@ -0,0 +1,187 @@
1+module Prelude.Show
2+
3+import Builtins
4+
5+import Prelude.Basics
6+import Prelude.Bits
7+import Prelude.Bool
8+import Prelude.Cast
9+import Prelude.Chars
10+import Prelude.Classes
11+import Prelude.List
12+import Prelude.Maybe
13+import Prelude.Nat
14+import Prelude.Strings
15+
16+%default total
17+
18+||| The precedence of an Idris operator or syntactic context.
19+data Prec = Open | Eq | Dollar | Backtick | User Nat | PrefixMinus | App
20+
21+||| Gives the constructor index of the Prec as a helper for writing instances.
22+precCon : Prec -> Integer
23+precCon Open = 0
24+precCon Eq = 1
25+precCon Dollar = 2
26+precCon Backtick = 3
27+precCon (User n) = 4
28+precCon PrefixMinus = 5
29+precCon App = 6
30+
31+instance Eq Prec where
32+ (==) (User m) (User n) = m == n
33+ (==) x y = precCon x == precCon y
34+
35+instance Ord Prec where
36+ compare (User m) (User n) = compare m n
37+ compare x y = compare (precCon x) (precCon y)
38+
39+||| Things that have a canonical `String` representation.
40+class Show a where
41+ ||| Convert a value to its `String` representation.
42+ |||
43+ ||| @ a the value to convert
44+ partial
45+ show : (x : a) -> String
46+ show = showPrec Open
47+
48+ ||| Convert a value to its `String` representation in a certain precedence
49+ ||| context.
50+ |||
51+ ||| A value should produce parentheses around itself if and only if the given
52+ ||| precedence context is greater than or equal to the precedence of the
53+ ||| outermost operation represented in the produced `String`. *This is
54+ ||| different from Haskell*, which requires it to be strictly greater. `Open`
55+ ||| should thus always produce *no* outermost parens, `App` should always
56+ ||| produce outermost parens except on atomic values and those that provide
57+ ||| their own bracketing, like `Pair` and `List`.
58+ |||
59+ ||| @ d the precedence context.
60+ ||| @ a the value to convert
61+ partial
62+ showPrec : (d : Prec) -> (x : a) -> String
63+ showPrec _ = show
64+
65+||| Surround a `String` with parentheses depending on a condition.
66+|||
67+||| @ b whether to add parentheses
68+showParens : (b : Bool) -> String -> String
69+showParens False s = s
70+showParens True s = "(" ++ s ++ ")"
71+
72+||| A helper for the common case of showing a non-infix constructor with at
73+||| least one argument, for use with `showArg`.
74+|||
75+||| Apply `showCon` to the precedence context, the constructor name, and the
76+||| args shown with `showArg` and concatenated. Example:
77+||| ```
78+||| data Ann a = MkAnn String a
79+|||
80+||| instance Show a => Show (Ann a) where
81+||| showPrec d (MkAnn s x) = showCon d "MkAnn" $ showArg s ++ showArg x
82+||| ```
83+showCon : (d : Prec) -> (conName : String) -> (shownArgs : String) -> String
84+showCon d conName shownArgs = showParens (d >= App) $ conName ++ shownArgs
85+
86+||| A helper for the common case of showing a non-infix constructor with at
87+||| least one argument, for use with `showCon`.
88+|||
89+||| This adds a space to the front so the results can be directly
90+||| concatenated. See `showCon` for details and an example.
91+showArg : Show a => (x : a) -> String
92+showArg x = " " ++ showPrec App x
93+
94+instance Show Int where
95+ show = prim__toStrInt
96+
97+instance Show Integer where
98+ show = prim__toStrBigInt
99+
100+instance Show Double where
101+ show = prim__floatToStr
102+
103+firstCharIs : (Char -> Bool) -> String -> Bool
104+firstCharIs p s with (strM s)
105+ firstCharIs p "" | StrNil = False
106+ firstCharIs p (strCons c cs) | StrCons c cs = p c
107+
108+protectEsc : (Char -> Bool) -> String -> String -> String
109+protectEsc p f s = f ++ (if firstCharIs p s then "\\&" else "") ++ s
110+
111+showLitChar : Char -> String -> String
112+showLitChar '\a' = ("\\a" ++)
113+showLitChar '\b' = ("\\b" ++)
114+showLitChar '\f' = ("\\f" ++)
115+showLitChar '\n' = ("\\n" ++)
116+showLitChar '\r' = ("\\r" ++)
117+showLitChar '\t' = ("\\t" ++)
118+showLitChar '\v' = ("\\v" ++)
119+showLitChar '\SO' = protectEsc (== 'H') "\\SO"
120+showLitChar '\DEL' = ("\\DEL" ++)
121+showLitChar '\\' = ("\\\\" ++)
122+showLitChar c = case getAt (cast (cast {to=Int} c)) asciiTab of
123+ Just k => strCons '\\' . (k ++)
124+ Nothing => if (c > '\DEL')
125+ then strCons '\\' . protectEsc isDigit (show (cast {to=Int} c))
126+ else strCons c
127+ where asciiTab : List String
128+ asciiTab = ["NUL", "SOH", "STX", "ETX", "EOT", "ENQ", "ACK", "BEL",
129+ "BS", "HT", "LF", "VT", "FF", "CR", "SO", "SI",
130+ "DLE", "DC1", "DC2", "DC3", "DC4", "NAK", "SYN", "ETB",
131+ "CAN", "EM", "SUB", "ESC", "FS", "GS", "RS", "US"]
132+
133+ getAt : Nat -> List String -> Maybe String
134+ getAt Z (x :: xs) = Just x
135+ getAt (S k) (x :: xs) = getAt k xs
136+ getAt _ [] = Nothing
137+
138+showLitString : List Char -> String -> String
139+showLitString [] = id
140+showLitString ('"'::cs) = ("\\\"" ++) . showLitString cs
141+showLitString (c ::cs) = showLitChar c . showLitString cs
142+
143+instance Show Char where
144+ show '\'' = "'\\''"
145+ show c = strCons '\'' (showLitChar c "'")
146+
147+instance Show String where
148+ show cs = strCons '"' (showLitString (cast cs) "\"")
149+
150+instance Show Nat where
151+ show n = show (the Integer (cast n))
152+
153+instance Show Bool where
154+ show True = "True"
155+ show False = "False"
156+
157+instance Show () where
158+ show () = "()"
159+
160+instance Show Bits8 where
161+ show b = b8ToString b
162+
163+instance Show Bits16 where
164+ show b = b16ToString b
165+
166+instance Show Bits32 where
167+ show b = b32ToString b
168+
169+instance Show Bits64 where
170+ show b = b64ToString b
171+
172+instance (Show a, Show b) => Show (a, b) where
173+ show (x, y) = "(" ++ show x ++ ", " ++ show y ++ ")"
174+
175+instance Show a => Show (List a) where
176+ show xs = "[" ++ show' "" xs ++ "]" where
177+ show' acc [] = acc
178+ show' acc [x] = acc ++ show x
179+ show' acc (x :: xs) = show' (acc ++ show x ++ ", ") xs
180+
181+instance Show a => Show (Maybe a) where
182+ showPrec d Nothing = "Nothing"
183+ showPrec d (Just x) = showCon d "Just" $ showArg x
184+
185+instance (Show a, {y : a} -> Show (p y)) => Show (Sigma a p) where
186+ show (y ** prf) = "(" ++ show y ++ " ** " ++ show prf ++ ")"
187+
libs/prelude/prelude.ipkg+1−1
@@ -6,7 +6,7 @@ modules = Builtins, Prelude, IO,
66 Prelude.Algebra, Prelude.Basics, Prelude.Bool, Prelude.Cast,
77 Prelude.Classes, Prelude.Nat, Prelude.List,
88 Prelude.Maybe, Prelude.Monad, Prelude.Applicative, Prelude.Either,
9− Prelude.Strings, Prelude.Chars, Prelude.Functor,
9+ Prelude.Strings, Prelude.Chars, Prelude.Show, Prelude.Functor,
1010 Prelude.Foldable, Prelude.Traversable, Prelude.Bits, Prelude.Stream,
1111 Prelude.Uninhabited, Prelude.Pairs, Prelude.Providers,
1212
rts/Makefile+2−2
@@ -30,8 +30,8 @@ LIBTARGET = libidris_rts.a
3030build: $(LIBTARGET) $(DYLIBTARGET)
3131
3232$(LIBTARGET) : $(OBJS)
33− ar r $(LIBTARGET) $(OBJS)
34− ranlib $(LIBTARGET)
33+ $(AR) r $(LIBTARGET) $(OBJS)
34+ $(RANLIB) $(LIBTARGET)
3535
3636install :
3737 mkdir -p $(TARGET)
src/IRTS/CodegenC.hs+1−1
@@ -77,7 +77,7 @@ codegenC' defs out exec incs objs libs flags exports iface dbg
7777 let args = [gccDbg dbg] ++
7878 gccFlags iface ++
7979 -- # Any flags defined here which alter the RTS API must also be added to config.mk
80− ["-DHAS_PTHREAD", "-DIDRIS_ENABLE_STATS", "-msse2",
80+ ["-DHAS_PTHREAD", "-DIDRIS_ENABLE_STATS",
8181 "-I."] ++ objs ++ ["-x", "c"] ++ envFlags ++
8282 (if (exec == Executable) then [] else ["-c"]) ++
8383 [tmpn] ++
src/IRTS/CodegenJavaScript.hs+5−5
@@ -1329,7 +1329,7 @@ translateBC info bc
13291329 | NULL r <- bc = jsNULL info r
13301330 | CALL n <- bc = jsCALL info n
13311331 | TAILCALL n <- bc = jsTAILCALL info n
1332− | FOREIGNCALL r _ (FStr n) args
1332+ | FOREIGNCALL r _ (FStr n) args
13331333 <- bc = jsFOREIGN info r n (map fcall args)
13341334 | TOPBASE n <- bc = jsTOPBASE info n
13351335 | BASETOP n <- bc = jsBASETOP info n
@@ -1346,7 +1346,7 @@ translateBC info bc
13461346 | otherwise = JSRaw $ "//" ++ show bc
13471347 where fcall (t, arg) = (toFType t, arg)
13481348
1349−toAType (FCon i)
1349+toAType (FCon i)
13501350 | i == sUN "JS_IntChar" = ATInt ITChar
13511351 | i == sUN "JS_IntNative" = ATInt ITNative
13521352toAType t = error (show t ++ " not defined in toAType")
@@ -1359,14 +1359,14 @@ toFnType (FApp c [_,r])
13591359 | c == sUN "JS_FnBase" = FFunction
13601360toFnType t = error (show t ++ " not defined in toFnType")
13611361
1362−toFType (FCon c)
1362+toFType (FCon c)
13631363 | c == sUN "JS_Str" = FString
13641364 | c == sUN "JS_Float" = FArith ATFloat
13651365 | c == sUN "JS_Ptr" = FPtr
13661366 | c == sUN "JS_Unit" = FUnit
1367−toFType (FApp c [_,ity])
1367+toFType (FApp c [_,ity])
13681368 | c == sUN "JS_IntT" = FArith (toAType ity)
1369−toFType (FApp c [_,fty])
1369+toFType (FApp c [_,fty])
13701370 | c == sUN "JS_FnT" = toFnType fty
13711371toFType t = error (show t ++ " not yet defined in toFType")
13721372
src/Idris/AbsSyntax.hs+6−6
@@ -1623,12 +1623,12 @@ addImpl' inpat env infns imp_meths ist ptm
16231623-- names with zero explicit arguments, don't add implicits.
16241624
16251625aiFn :: Bool -> Bool -> Bool
1626− -> [Name]
1627− -> IState -> FC
1628− -> Name -- ^ function being applied
1629− -> FC -> [[T.Text]]
1630− -> [PArg] -> -- ^ initial arguments
1631− Either Err PTerm
1626+ -> [Name]
1627+ -> IState -> FC
1628+ -> Name -- ^ function being applied
1629+ -> FC -> [[T.Text]]
1630+ -> [PArg] -- ^ initial arguments
1631+ -> Either Err PTerm
16321632aiFn inpat True qq imp_meths ist fc f ffc ds []
16331633 = case lookupDef f (tt_ctxt ist) of
16341634 [] -> Right $ PPatvar ffc f
src/Idris/Core/Binary.hs−6
@@ -311,12 +311,6 @@ instance Binary Name where
311311 return (SymRef x1)
312312 _ -> error "Corrupted binary data for Name"
313313
314−instance Binary T.Text where
315− put x = put (E.encodeUtf8 x)
316− get = do x <- get
317− return $!! (E.decodeUtf8 x)
318−
319−
320314instance Binary SpecialName where
321315 put x
322316 = case x of
src/Idris/Delaborate.hs+4−4
@@ -231,14 +231,14 @@ pprintErr' i (InternalMsg s) =
231231pprintErr' i (CantUnify _ (x_in, xprov) (y_in, yprov) e sc s) =
232232 let (x_ns, y_ns, nms) = renameMNs x_in y_in
233233 (x, y) = addImplicitDiffs (delab i x_ns) (delab i y_ns) in
234− text "Can't unify" <> indented (annTm x_ns
234+ text "Type mismatch between" <> indented (annTm x_ns
235235 (pprintTerm' i (map (\ (n, b) -> (n, False)) sc
236236 ++ zip nms (repeat False)) x))
237237 <> case xprov of
238238 Nothing -> empty
239239 Just t -> text " (" <> pprintProv i sc t <> text ")"
240240 <$>
241− text "with" <> indented (annTm y_ns
241+ text "and" <> indented (annTm y_ns
242242 (pprintTerm' i (map (\ (n, b) -> (n, False)) sc
243243 ++ zip nms (repeat False)) y))
244244 <> case yprov of
@@ -257,10 +257,10 @@ pprintErr' i (CantConvert x_in y_in env) =
257257 let (x_ns, y_ns, nms) = renameMNs x_in y_in
258258 (x, y) = addImplicitDiffs (delab i (flagUnique x_ns))
259259 (delab i (flagUnique y_ns)) in
260− text "Can't convert" <>
260+ text "Type mismatch between" <>
261261 indented (annTm x_ns (pprintTerm' i (map (\ (n, b) -> (n, False)) env)
262262 x)) <$>
263− text "with" <>
263+ text "and" <>
264264 indented (annTm y_ns (pprintTerm' i (map (\ (n, b) -> (n, False)) env)
265265 y)) <>
266266 if (opt_errContext (idris_options i)) then line <> showSc i env else empty
src/Idris/Elab/Class.hs+44−16
@@ -1,4 +1,5 @@
11{-# LANGUAGE PatternGuards #-}
2+{-# OPTIONS_GHC -fwarn-missing-signatures #-}
23module Idris.Elab.Class(elabClass) where
34
45import Idris.AbsSyntax
@@ -47,6 +48,7 @@ import qualified Data.Set as S
4748import qualified Data.Text as T
4849import Data.Char(isLetter, toLower)
4950import Data.List.Split (splitOn)
51+import Data.Generics.Uniplate.Data (transform)
5052
5153import Util.Pretty(pretty, text)
5254
@@ -83,6 +85,7 @@ elabClass info syn_in doc fc constraints tn tnfc ps pDocs fds ds mcn cd
8385 let (methods, imethods)
8486 = unzip (map (\ (x, y, z) -> (x, y)) ims)
8587 let defaults = map (\ (x, (y, z)) -> (x,y)) defs
88+
8689 -- build instance constructor type
8790 let cty = impbind [(pn, pt) | (pn, _, pt) <- ps] $ conbind constraints
8891 $ pibind (map (\ (n, ty) -> (nsroot n, ty)) methods)
@@ -92,6 +95,7 @@ elabClass info syn_in doc fc constraints tn tnfc ps pDocs fds ds mcn cd
9295 let ddecl = PDatadecl tn NoFC tty cons
9396
9497 logLvl 5 $ "Class data " ++ show (showDImp verbosePPOption ddecl)
98+
9599 -- Elaborate the data declaration
96100 elabData info (syn { no_imp = no_imp syn ++ mnames,
97101 imp_methods = mnames }) doc pDocs fc [] ddecl
@@ -118,7 +122,7 @@ elabClass info syn_in doc fc constraints tn tnfc ps pDocs fds ds mcn cd
118122 [(pnfc, AnnBoundName pn False) | (pn, pnfc, _) <- ps] ++
119123 [(fdfc, AnnBoundName fc False) | (fc, fdfc) <- fds] ++
120124 maybe [] (\(conN, conNFC) -> [(conNFC, AnnName conN Nothing Nothing Nothing)]) mcn
121−
125+
122126 where
123127 nodoc (n, (_, _, o, t)) = (n, (o, t))
124128
@@ -132,11 +136,6 @@ elabClass info syn_in doc fc constraints tn tnfc ps pDocs fds ds mcn cd
132136 chkUniq (PPi _ _ _ _ sc) t = chkUniq sc t
133137 chkUniq _ t = t
134138
135− mdec :: Name -> Name
136− mdec (UN n) = SN (MethodN (UN n))
137− mdec (NS x n) = NS (mdec x) n
138− mdec x = x
139−
140139 -- TODO: probably should normalise
141140 checkDefaultSuperclassInstance :: PDecl -> Idris ()
142141 checkDefaultSuperclassInstance (PInstance _ _ _ fc cs n _ ps _ _ _)
@@ -171,7 +170,7 @@ elabClass info syn_in doc fc constraints tn tnfc ps pDocs fds ds mcn cd
171170 defdecl mtys c d@(PClauses fc opts n cs) =
172171 case lookup n mtys of
173172 Just (nfc, syn, o, ty) ->
174− do let ty' = insertConstraint c ty
173+ do let ty' = insertConstraint c (map fst mtys) ty
175174 let ds = map (decorateid defaultdec)
176175 [PTy emptyDocstring [] syn fc [] n nfc ty',
177176 PClauses fc (o ++ opts) n cs]
@@ -215,10 +214,16 @@ elabClass info syn_in doc fc constraints tn tnfc ps pDocs fds ds mcn cd
215214 return [PTy emptyDocstring [] syn fc [] cfn NoFC ty,
216215 PClauses fc [Dictionary] cfn [PClause fc cfn lhs [] rhs []]]
217216
218− -- Generate a top level function which looks up a method in a given
217+ -- | Generate a top level function which looks up a method in a given
219218 -- dictionary (this is inlinable, always)
219+ tfun :: Name -- ^ The name of the class
220+ -> PTerm -- ^ A constraint for the class, to be inserted under the implicit bindings
221+ -> SyntaxInfo -> [Name] -- ^ All the method names
222+ -> (Name, (FC, Docstring (Either Err PTerm), FnOpts, PTerm))
223+ -- ^ The present declaration
224+ -> Idris [PDecl]
220225 tfun cn c syn all (m, (mfc, doc, o, ty))
221− = do let ty' = expandMethNS syn (insertConstraint c ty)
226+ = do let ty' = expandMethNS syn (insertConstraint c all ty)
222227 let mnames = take (length all) $ map (\x -> sMN x "meth") [0..]
223228 let capp = PApp fc (PRef fc cn) (map (pexp . PRef fc) mnames)
224229 let margs = getMArgs ty
@@ -236,6 +241,7 @@ elabClass info syn_in doc fc constraints tn tnfc ps pDocs fds ds mcn cd
236241 getMArgs (PPi (Constraint _ _) n _ ty sc) = CA : getMArgs sc
237242 getMArgs _ = []
238243
244+ getMeth :: [Name] -> [Name] -> Name -> PTerm
239245 getMeth (m:ms) (a:as) x | x == a = PRef fc m
240246 | otherwise = getMeth ms as x
241247
@@ -249,10 +255,24 @@ elabClass info syn_in doc fc constraints tn tnfc ps pDocs fds ds mcn cd
249255 rhsArgs (CA : xs) ns = pconst (PResolveTC fc) : rhsArgs xs ns
250256 rhsArgs [] _ = []
251257
252− insertConstraint c (PPi p@(Imp _ _ _ _) n fc ty sc)
253− = PPi p n fc ty (insertConstraint c sc)
254− insertConstraint c sc = PPi (constraint { pstatic = Static })
255− (sMN 0 "class") NoFC c sc
258+ insertConstraint :: PTerm -> [Name] -> PTerm -> PTerm
259+ insertConstraint c all (PPi p@(Imp _ _ _ _) n fc ty sc)
260+ = PPi p n fc ty (insertConstraint c all sc)
261+ insertConstraint c all sc = let dictN = sMN 0 "class"
262+ in PPi (constraint { pstatic = Static })
263+ dictN NoFC c
264+ (constrainMeths (map basename all)
265+ dictN sc)
266+ where
267+ -- After we insert the constraint into the lookup, we need to
268+ -- ensure that the same dictionary is used to resolve lookups
269+ -- to the other methods in the class
270+ constrainMeths :: [Name] -> Name -> PTerm -> PTerm
271+ constrainMeths allM dictN tm = transform (addC allM dictN) tm
272+ addC allM dictN m@(PRef fc n)
273+ | n `elem` allM = PApp NoFC m [pconst (PRef NoFC dictN)]
274+ | otherwise = m
275+ addC _ _ tm = tm
256276
257277 -- make arguments explicit and don't bind class parameters
258278 toExp ns e (PPi (Imp l s p _) n fc ty sc)
@@ -261,6 +281,13 @@ elabClass info syn_in doc fc constraints tn tnfc ps pDocs fds ds mcn cd
261281 toExp ns e (PPi p n fc ty sc) = PPi p n fc ty (toExp ns e sc)
262282 toExp ns e sc = sc
263283
284+-- | Get the method declaration name corresponding to a user-provided name
285+mdec :: Name -> Name
286+mdec (UN n) = SN (MethodN (UN n))
287+mdec (NS x n) = NS (mdec x) n
288+mdec x = x
289+
290+-- | Get the docstring corresponding to a member, if one exists
264291memberDocs :: PDecl -> Maybe (Name, Docstring (Either Err PTerm))
265292memberDocs (PTy d _ _ _ _ n _ _) = Just (basename n, d)
266293memberDocs (PPostulate _ d _ _ _ n _) = Just (basename n, d)
@@ -270,17 +297,18 @@ memberDocs (PClass d _ _ _ n _ _ _ _ _ _ _) = Just (basename n, d)
270297memberDocs _ = Nothing
271298
272299
273−-- In a top level type for a method, expand all the method names namespaces
300+-- | In a top level type for a method, expand all the method names' namespaces
274301-- so that we don't have to disambiguate later
275−expandMethNS :: SyntaxInfo
302+expandMethNS :: SyntaxInfo
276303 -> PTerm -> PTerm
277304expandMethNS syn = mapPT expand
278305 where
279306 expand (PRef fc n) | n `elem` imp_methods syn = PRef fc $ expandNS syn n
280307 expand t = t
281308
309+-- | Find the determining parameter locations
282310findDets :: Name -> [Name] -> Idris [Int]
283−findDets n ns =
311+findDets n ns =
284312 do i <- getIState
285313 return $ case lookupTyExact n (tt_ctxt i) of
286314 Just ty -> getDetPos 0 ns ty
src/Idris/Parser.hs+12−6
@@ -1271,12 +1271,18 @@ parseImports fname input
12711271
12721272-- | There should be a better way of doing this...
12731273findFC :: Doc -> (FC, String)
1274−findFC x = let s = show (plain x) in
1275− case span (/= ':') s of
1276− (failname, ':':rest) -> case span isDigit rest of
1277− (line, ':':rest') -> case span isDigit rest' of
1278− (col, ':':msg) -> let pos = (read line, read col) in
1279− (FC failname pos pos, msg)
1274+findFC x = let s = show (plain x) in findFC' s
1275+ where findFC' s = case span (/= ':') s of
1276+ -- Horrid kludge to prevent crashes on Windows
1277+ (prefix, ':':'\\':rest) ->
1278+ case findFC' rest of
1279+ (NoFC, msg) -> (NoFC, msg)
1280+ (FileFC f, msg) -> (FileFC (prefix ++ ":\\" ++ f), msg)
1281+ (FC f start end, msg) -> (FC (prefix ++ ":\\" ++ f) start end, msg)
1282+ (failname, ':':rest) -> case span isDigit rest of
1283+ (line, ':':rest') -> case span isDigit rest' of
1284+ (col, ':':msg) -> let pos = (read line, read col) in
1285+ (FC failname pos pos, msg)
12801286
12811287-- | Check if the coloring matches the options and corrects if necessary
12821288fixColour :: Bool -> ANSI.Doc -> ANSI.Doc
test/basic006/expected+2−2
@@ -1,8 +1,8 @@
11test020a.idr:16:18:When elaborating right hand side of foo:
22When elaborating an application of function Prelude.List.reverse:
3− Can't unify
3+ Type mismatch between
44 Vect n a (Type of xs)
5− with
5+ and
66 List a (Expected type)
77[3, 2, 1]
88"Number 42"
test/disambig001/disambig001.idr+1−1
@@ -8,5 +8,5 @@ import Effect.System
88main : IO ()
99main = do
1010 args <- System.getArgs
11− putStrLn (concat args)
11+ putStrLn (concat (drop 1 args))
1212
test/disambig001/expected+1−1
@@ -1 +1 @@
1−./disambig001foobar
1+foobar
test/proof002/expected+4−4
@@ -1,13 +1,13 @@
11Reflect.idr:208:38:
22When elaborating right hand side of testReflect1:
33When elaborating an application of function Reflect.getJust:
4− Can't unify
4+ Type mismatch between
55 IsJust (Just x1) (Type of ItIsJust)
6− with
6+ and
77 IsJust (prove (getProof x)) (Expected type)
88
99 Specifically:
10− Can't unify
10+ Type mismatch between
1111 Just x
12− with
12+ and
1313 Nothing
test/quasiquote001/expected+3−3
@@ -1,5 +1,5 @@
1−(App (App (App (P (DCon 1 3) (NS (UN "::") ["List", "Prelude"]) (Bind (UN "a") (Pi (TType (UVar -1))) (Bind (MN 0 "_t") (Pi (V 0)) (Bind (MN 2 "_t") (Pi (App (P (TCon 0 0) (NS (UN "List") ["List", "Prelude"]) Erased) (V 1))) (App (P (TCon 0 0) (NS (UN "List") ["List", "Prelude"]) Erased) (V 2)))))) (P (TCon 8 0) (UN "Unit") (TType (UVar -1)))) (P (DCon 0 0) (UN "MkUnit") (P (TCon 0 0) (UN "Unit") Erased))) (App (App (App (P (DCon 1 3) (NS (UN "::") ["List", "Prelude"]) (Bind (UN "a") (Pi (TType (UVar -1))) (Bind (MN 0 "_t") (Pi (V 0)) (Bind (MN 2 "_t") (Pi (App (P (TCon 0 0) (NS (UN "List") ["List", "Prelude"]) Erased) (V 1))) (App (P (TCon 0 0) (NS (UN "List") ["List", "Prelude"]) Erased) (V 2)))))) (P (TCon 8 0) (UN "Unit") (TType (UVar -1)))) (P (DCon 0 0) (UN "MkUnit") (P (TCon 0 0) (UN "Unit") Erased))) (App (P (DCon 0 1) (NS (UN "Nil") ["List", "Prelude"]) (Bind (UN "a") (Pi (TType (UVar -1))) (App (P (TCon 0 0) (NS (UN "List") ["List", "Prelude"]) Erased) (V 0)))) (P (TCon 8 0) (UN "Unit") (TType (UVar -1))))))
1+App (App (App (P (DCon 1 3) (NS (UN "::") ["List", "Prelude"]) (Bind (UN "a") (Pi (TType (UVar -1)) (TType (UVar -1))) (Bind (MN 0 "_t") (Pi (V 0) (TType (UVar -1))) (Bind (MN 2 "_t") (Pi (App (P (TCon 0 0) (NS (UN "List") ["List", "Prelude"]) Erased) (V 1)) (TType (UVar -1))) (App (P (TCon 0 0) (NS (UN "List") ["List", "Prelude"]) Erased) (V 2)))))) (P (TCon 8 0) (UN "Unit") (TType (UVar -1)))) (P (DCon 0 0) (UN "MkUnit") (P (TCon 0 0) (UN "Unit") Erased))) (App (App (App (P (DCon 1 3) (NS (UN "::") ["List", "Prelude"]) (Bind (UN "a") (Pi (TType (UVar -1)) (TType (UVar -1))) (Bind (MN 0 "_t") (Pi (V 0) (TType (UVar -1))) (Bind (MN 2 "_t") (Pi (App (P (TCon 0 0) (NS (UN "List") ["List", "Prelude"]) Erased) (V 1)) (TType (UVar -1))) (App (P (TCon 0 0) (NS (UN "List") ["List", "Prelude"]) Erased) (V 2)))))) (P (TCon 8 0) (UN "Unit") (TType (UVar -1)))) (P (DCon 0 0) (UN "MkUnit") (P (TCon 0 0) (UN "Unit") Erased))) (App (P (DCon 0 1) (NS (UN "Nil") ["List", "Prelude"]) (Bind (UN "a") (Pi (TType (UVar -1)) (TType (UVar -1))) (App (P (TCon 0 0) (NS (UN "List") ["List", "Prelude"]) Erased) (V 0)))) (P (TCon 8 0) (UN "Unit") (TType (UVar -1)))))
22--------------
3−(App (App (App (P (DCon 1 3) (NS (UN "::") ["List", "Prelude"]) (Bind (UN "a") (Pi (TType (UVar -1))) (Bind (MN 0 "_t") (Pi (V 0)) (Bind (MN 2 "_t") (Pi (App (P (TCon 0 0) (NS (UN "List") ["List", "Prelude"]) Erased) (V 1))) (App (P (TCon 0 0) (NS (UN "List") ["List", "Prelude"]) Erased) (V 2)))))) (TType (UVar 24))) (TType (UVar 25))) (App (App (App (P (DCon 1 3) (NS (UN "::") ["List", "Prelude"]) (Bind (UN "a") (Pi (TType (UVar -1))) (Bind (MN 0 "_t") (Pi (V 0)) (Bind (MN 2 "_t") (Pi (App (P (TCon 0 0) (NS (UN "List") ["List", "Prelude"]) Erased) (V 1))) (App (P (TCon 0 0) (NS (UN "List") ["List", "Prelude"]) Erased) (V 2)))))) (TType (UVar 26))) (App (App (App (App (P (DCon 0 4) (NS (UN "MkPair") ["Builtins"]) (Bind (UN "A") (Pi (TType (UVar -1))) (Bind (UN "B") (Pi (TType (UVar -1))) (Bind (UN "a") (Pi (V 1)) (Bind (UN "b") (Pi (V 1)) (App (App (P (TCon 0 0) (NS (UN "Pair") ["Builtins"]) Erased) (V 3)) (V 2))))))) (TType (UVar 22))) (TType (UVar 23))) (P (TCon 8 0) (NS (UN "Nat") ["Nat", "Prelude"]) (TType (UVar -1)))) (P (TCon 8 0) (NS (UN "Nat") ["Nat", "Prelude"]) (TType (UVar -1))))) (App (P (DCon 0 1) (NS (UN "Nil") ["List", "Prelude"]) (Bind (UN "a") (Pi (TType (UVar -1))) (App (P (TCon 0 0) (NS (UN "List") ["List", "Prelude"]) Erased) (V 0)))) (TType (UVar 27)))))
3+App (App (App (P (DCon 1 3) (NS (UN "::") ["List", "Prelude"]) (Bind (UN "a") (Pi (TType (UVar -1)) (TType (UVar -1))) (Bind (MN 0 "_t") (Pi (V 0) (TType (UVar -1))) (Bind (MN 2 "_t") (Pi (App (P (TCon 0 0) (NS (UN "List") ["List", "Prelude"]) Erased) (V 1)) (TType (UVar -1))) (App (P (TCon 0 0) (NS (UN "List") ["List", "Prelude"]) Erased) (V 2)))))) (TType (UVar 24))) (TType (UVar 25))) (App (App (App (P (DCon 1 3) (NS (UN "::") ["List", "Prelude"]) (Bind (UN "a") (Pi (TType (UVar -1)) (TType (UVar -1))) (Bind (MN 0 "_t") (Pi (V 0) (TType (UVar -1))) (Bind (MN 2 "_t") (Pi (App (P (TCon 0 0) (NS (UN "List") ["List", "Prelude"]) Erased) (V 1)) (TType (UVar -1))) (App (P (TCon 0 0) (NS (UN "List") ["List", "Prelude"]) Erased) (V 2)))))) (TType (UVar 26))) (App (App (App (App (P (DCon 0 4) (NS (UN "MkPair") ["Builtins"]) (Bind (UN "A") (Pi (TType (UVar -1)) (TType (UVar -1))) (Bind (UN "B") (Pi (TType (UVar -1)) (TType (UVar -1))) (Bind (UN "a") (Pi (V 1) (TType (UVar -1))) (Bind (UN "b") (Pi (V 1) (TType (UVar -1))) (App (App (P (TCon 0 0) (NS (UN "Pair") ["Builtins"]) Erased) (V 3)) (V 2))))))) (TType (UVar 22))) (TType (UVar 23))) (P (TCon 8 0) (NS (UN "Nat") ["Nat", "Prelude"]) (TType (UVar -1)))) (P (TCon 8 0) (NS (UN "Nat") ["Nat", "Prelude"]) (TType (UVar -1))))) (App (P (DCon 0 1) (NS (UN "Nil") ["List", "Prelude"]) (Bind (UN "a") (Pi (TType (UVar -1)) (TType (UVar -1))) (App (P (TCon 0 0) (NS (UN "List") ["List", "Prelude"]) Erased) (V 0)))) (TType (UVar 27))))
44--------------
5−(App (App (App (App (P (DCon 0 4) (NS (UN "MkPair") ["Builtins"]) (Bind (UN "A") (Pi (TType (UVar -1))) (Bind (UN "B") (Pi (TType (UVar -1))) (Bind (UN "a") (Pi (V 1)) (Bind (UN "b") (Pi (V 1)) (App (App (P (TCon 0 0) (NS (UN "Pair") ["Builtins"]) Erased) (V 3)) (V 2))))))) (TType (UVar 22))) (TType (UVar 23))) (App (App (App (App (P (DCon 0 4) (NS (UN "MkPair") ["Builtins"]) (Bind (UN "A") (Pi (TType (UVar -1))) (Bind (UN "B") (Pi (TType (UVar -1))) (Bind (UN "a") (Pi (V 1)) (Bind (UN "b") (Pi (V 1)) (App (App (P (TCon 0 0) (NS (UN "Pair") ["Builtins"]) Erased) (V 3)) (V 2))))))) (TType (UVar 22))) (TType (UVar 23))) (TType (UVar 24))) (TType (UVar 24)))) (App (App (App (App (P (DCon 0 4) (NS (UN "MkPair") ["Builtins"]) (Bind (UN "A") (Pi (TType (UVar -1))) (Bind (UN "B") (Pi (TType (UVar -1))) (Bind (UN "a") (Pi (V 1)) (Bind (UN "b") (Pi (V 1)) (App (App (P (TCon 0 0) (NS (UN "Pair") ["Builtins"]) Erased) (V 3)) (V 2))))))) (TType (UVar 22))) (TType (UVar 23))) (TType (UVar 24))) (TType (UVar 24))))
5+App (App (App (App (P (DCon 0 4) (NS (UN "MkPair") ["Builtins"]) (Bind (UN "A") (Pi (TType (UVar -1)) (TType (UVar -1))) (Bind (UN "B") (Pi (TType (UVar -1)) (TType (UVar -1))) (Bind (UN "a") (Pi (V 1) (TType (UVar -1))) (Bind (UN "b") (Pi (V 1) (TType (UVar -1))) (App (App (P (TCon 0 0) (NS (UN "Pair") ["Builtins"]) Erased) (V 3)) (V 2))))))) (TType (UVar 22))) (TType (UVar 23))) (App (App (App (App (P (DCon 0 4) (NS (UN "MkPair") ["Builtins"]) (Bind (UN "A") (Pi (TType (UVar -1)) (TType (UVar -1))) (Bind (UN "B") (Pi (TType (UVar -1)) (TType (UVar -1))) (Bind (UN "a") (Pi (V 1) (TType (UVar -1))) (Bind (UN "b") (Pi (V 1) (TType (UVar -1))) (App (App (P (TCon 0 0) (NS (UN "Pair") ["Builtins"]) Erased) (V 3)) (V 2))))))) (TType (UVar 22))) (TType (UVar 23))) (TType (UVar 24))) (TType (UVar 24)))) (App (App (App (App (P (DCon 0 4) (NS (UN "MkPair") ["Builtins"]) (Bind (UN "A") (Pi (TType (UVar -1)) (TType (UVar -1))) (Bind (UN "B") (Pi (TType (UVar -1)) (TType (UVar -1))) (Bind (UN "a") (Pi (V 1) (TType (UVar -1))) (Bind (UN "b") (Pi (V 1) (TType (UVar -1))) (App (App (P (TCon 0 0) (NS (UN "Pair") ["Builtins"]) Erased) (V 3)) (V 2))))))) (TType (UVar 22))) (TType (UVar 23))) (TType (UVar 24))) (TType (UVar 24)))
test/reg007/expected+4−4
@@ -1,12 +1,12 @@
11reg007.lidr:8:1:A.n is already defined
22reg007.lidr:12:11-17:When elaborating right hand side of hurrah:
3−Can't unify
3+Type mismatch between
44 n = lala (Type of isSame)
5−with
5+and
66 0 = 1 (Expected type)
77
88Specifically:
9− Can't unify
9+ Type mismatch between
1010 1
11− with
11+ and
1212 0
test/reg023/expected+2−2
@@ -1,5 +1,5 @@
11reg023.idr:7:5:When elaborating right hand side of bad:
2−Can't unify
2+Type mismatch between
33 Nat (Type of 0)
4−with
4+and
55 f Nat (Expected type)
test/reg044/expected+4−4
@@ -1,11 +1,11 @@
11reg044.idr:4:4:When elaborating right hand side of Main.pf:
2−Can't unify
2+Type mismatch between
33 b = b (Type of Refl)
4−with
4+and
55 a = b (Expected type)
66
77Specifically:
8− Can't unify
8+ Type mismatch between
99 b
10− with
10+ and
1111 a
test/reg054/expected+2−2
@@ -6,7 +6,7 @@ When elaborating argument x to Main.weird:
66 No explicit types on left hand side: Char
77reg054.idr:37:1-8:When elaborating left hand side of tctrick:
88When elaborating an application of Main.tctrick:
9− Can't unify
9+ Type mismatch between
1010 Maybe a1 (Type of Just x)
11− with
11+ and
1212 a (Expected type)
test/reg065/expectednew file

No changes to the content.

test/reg065/reg065.idrnew file+26
@@ -0,0 +1,26 @@
1+||| Test that dependent type class definitions work.
2+|||
3+||| Fixes a regression where previous methods used in a later method's
4+||| type would lead to "can't resolve type class" errors
5+module TypeClassDep
6+
7+import Data.Vect
8+
9+
10+class Foo a where
11+ getLen : Nat
12+ item : a -> Vect getLen a
13+
14+instance Foo () where
15+ getLen = 3
16+ item () = [(), (), ()]
17+
18+instance Foo String where
19+ getLen = 1
20+ item str = [str]
21+
22+check1 : item () = with Vect [(),(),()]
23+check1 = Refl
24+
25+check2 : item "halløjsa" = with Vect ["halløjsa"]
26+check2 = Refl
test/reg065/runnew file+3
@@ -0,0 +1,3 @@
1+#!/usr/bin/env bash
2+idris $@ reg065.idr --check
3+rm -f *.ibc
test/tutorial006/expected+8−8
@@ -1,25 +1,25 @@
11tutorial006a.idr:5:23-25:
22When elaborating right hand side of vapp:
33When elaborating argument xs to constructor Data.VectType.Vect.:::
4− Can't unify
4+ Type mismatch between
55 Vect (n + n) a (Type of vapp xs xs)
6− with
6+ and
77 Vect (plus n m) a (Expected type)
88
99 Specifically:
10− Can't unify
10+ Type mismatch between
1111 plus n n
12− with
12+ and
1313 plus n m
1414tutorial006b.idr:10:10:
1515When elaborating right hand side of with block in Main.parity:
16−Can't unify
16+Type mismatch between
1717 Parity (plus (S j) (S j)) (Type of even)
18−with
18+and
1919 Parity (S (S (plus j j))) (Expected type)
2020
2121Specifically:
22− Can't unify
22+ Type mismatch between
2323 plus (S j) (S j)
24− with
24+ and
2525 S (S (plus j j))
test/unique001/expected+6−6
@@ -2,17 +2,17 @@
2219,18,17,16,15,14,13,12,11,10,9,8,7,6,5,4,3,2,1,0,END
3338,36,34,32,30,28,26,24,22,20,18,16,14,12,10,8,6,4,2,0,END
4438,36,34,32,30,28,26,24,22,20,18,16,14,12,10,8,6,4,2,0,END
5−unique001a.idr:33:11:Can't convert
5+unique001a.idr:33:11:Type mismatch between
66 Int -> String
7−with
7+and
88 UniqueType (Int -> String)
9−unique001a.idr:44:12:Can't convert
9+unique001a.idr:44:12:Type mismatch between
1010 Int -> String
11−with
11+and
1212 UniqueType (Int -> String)
13−unique001a.idr:55:12:Can't convert
13+unique001a.idr:55:12:Type mismatch between
1414 UniqueType (Int -> String)
15−with
15+and
1616 Int -> String
1717unique001b.idr:16:7:Borrowed name xs must not be used on RHS
1818unique001c.idr:46:6:Unique name f is used more than once
test/unique002/expected+2−2
@@ -1,5 +1,5 @@
11unique002.idr:15:5:Unique name xs is used more than once
2−unique002a.idr:15:5:Can't convert
2+unique002a.idr:15:5:Type mismatch between
33 Int -> String
4−with
4+and
55 UniqueType (Int -> String)
test/unique003/expected+2−2
@@ -1,4 +1,4 @@
1−unique003.idr:18:5:Can't convert
1+unique003.idr:18:5:Type mismatch between
22 Int -> String
3−with
3+and
44 UniqueType (Int -> String)