git.iko.soy/Idris-dev
on master help sign in
Merge remote-tracking branch 'refs/remotes/upstream/master' into wip/tactical
8a07216David Raymond Christiansen
CHANGELOG+6
compare with master
unifiedsplit
@@ -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+
1New in 0.9.18:
7New in 0.9.18:
2--------------
8--------------
3* GHC 7.10 compatibility
9* GHC 7.10 compatibility
config.mk+4−1
@@ -1,8 +1,11 @@
1CC ?=cc
1CC ?=cc
2+AR ?=ar
3+RANLIB ?=ranlib
4+
2CABAL :=cabal
5CABAL :=cabal
3# IDRIS_ENABLE_STATS should not be set in final release
6# IDRIS_ENABLE_STATS should not be set in final release
4# Any flags defined here which alter the RTS API must also be added to src/IRTS/CodegenC.hs
7# 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)
6
9
7#CABALFLAGS :=
10#CABALFLAGS :=
8## Disable building of Effects
11## Disable building of Effects
docs/faq/faq.rst+24
@@ -99,6 +99,30 @@ the difference between:
99 Idris> \n, m => n + (S m)
99 Idris> \n, m => n + (S m)
100 \n => \m => plus n (S m) : Nat -> Nat -> Nat
100 \n => \m => plus n (S m) : Nat -> Nat -> Nat
101
101
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+
102When will Idris be self-hosting?
126When will Idris be self-hosting?
103================================
127================================
104
128
docs/index.rst+2
@@ -104,6 +104,7 @@ Language Reference
104 reference/uniqueness-types
104 reference/uniqueness-types
105 reference/ffi
105 reference/ffi
106 reference/erasure
106 reference/erasure
107+ reference/ide-protocol
107
108
108.. _guides:
109.. _guides:
109
110
@@ -115,3 +116,4 @@ Short Guides
115 :maxdepth: 1
116 :maxdepth: 1
116
117
117 guides/type-providers-ffi
118 guides/type-providers-ffi
119+
docs/proofs/pluscomm.rst+2−2
@@ -88,9 +88,9 @@ error:
88::
88::
89
89
90 When elaborating right hand side of four_eq_five:
90 When elaborating right hand side of four_eq_five:
91− Can't unify
91+ Type mismatch between
92 x = x (Type of Refl)
92 x = x (Type of Refl)
93− with
93+ and
94 4 = 5 (Expected type)
94 4 = 5 (Expected type)
95
95
96Type checking equality proofs
96Type 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:
35::
35::
36
36
37 viewsbroken.idr:12:10:When elaborating right hand side of ViewsBroken.parity:
37 viewsbroken.idr:12:10:When elaborating right hand side of ViewsBroken.parity:
38− Can't unify
38+ Type mismatch between
39 Parity (plus (S j) (S j))
39 Parity (plus (S j) (S j))
40− with
40+ and
41 Parity (S (S (plus j j)))
41 Parity (S (S (plus j j)))
42
42
43 Specifically:
43 Specifically:
44− Can't unify
44+ Type mismatch between
45 plus (S j) (S j)
45 plus (S j) (S j)
46− with
46+ and
47 S (S (plus j j))
47 S (S (plus j j))
48
48
49The type checker is telling us that ``(j+1)+(j+1)`` and ``2+j+j`` do not
49The 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
71definitions, except that they introduce the right hand side with a
71definitions, except that they introduce the right hand side with a
72``?=`` rather than ``=``. We define ``parity`` as follows:
72``?=`` rather than ``=``. We define ``parity`` as follows:
73
73
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+
74When written in this form, instead of reporting a type error, Idris
83When written in this form, instead of reporting a type error, Idris
75will insert a metavariable standing for a theorem which will correct the
84will insert a metavariable standing for a theorem which will correct the
76type error. Idris tells us we have two proof obligations, with names
85type error. Idris tells us we have two proof obligations, with names
docs/tutorial/typesfuns.rst+4−4
@@ -309,15 +309,15 @@ following:
309 $ idris vbroken.idr --check
309 $ idris vbroken.idr --check
310 vbroken.idr:9:23:When elaborating right hand side of Vect.++:
310 vbroken.idr:9:23:When elaborating right hand side of Vect.++:
311 When elaborating an application of constructor Vect.:::
311 When elaborating an application of constructor Vect.:::
312− Can't unify
312+ Type mismatch between
313 Vect (k + k) a (Type of xs ++ xs)
313 Vect (k + k) a (Type of xs ++ xs)
314− with
314+ and
315 Vect (plus k m) a (Expected type)
315 Vect (plus k m) a (Expected type)
316
316
317 Specifically:
317 Specifically:
318− Can't unify
318+ Type mismatch between
319 plus k k
319 plus k k
320− with
320+ and
321 plus k m
321 plus k m
322
322
323
323
idris.cabal+9−6
@@ -1,5 +1,5 @@
1Name: idris
1Name: idris
2−Version: 0.9.18
2+Version: 0.9.18.1
3License: BSD3
3License: BSD3
4License-file: LICENSE
4License-file: LICENSE
5Author: Edwin Brady
5Author: Edwin Brady
@@ -114,7 +114,7 @@ Extra-source-files:
114 libs/contrib/Classes/*.idr
114 libs/contrib/Classes/*.idr
115 libs/contrib/Control/*.idr
115 libs/contrib/Control/*.idr
116 libs/contrib/Control/Isomorphism/*.idr
116 libs/contrib/Control/Isomorphism/*.idr
117− libs/contrib/Control/Algebra/*.idr
117+ libs/contrib/Control/Algebra/*.idr
118 libs/contrib/Data/*.idr
118 libs/contrib/Data/*.idr
119 libs/contrib/Decidable/*.idr
119 libs/contrib/Decidable/*.idr
120 libs/contrib/Network/*.idr
120 libs/contrib/Network/*.idr
@@ -314,6 +314,9 @@ Extra-source-files:
314 test/reg064/run
314 test/reg064/run
315 test/reg064/*.idr
315 test/reg064/*.idr
316 test/reg064/expected
316 test/reg064/expected
317+ test/reg065/run
318+ test/reg065/*.idr
319+ test/reg065/expected
317
320
318 test/basic001/run
321 test/basic001/run
319 test/basic001/*.idr
322 test/basic001/*.idr
@@ -888,7 +891,7 @@ Library
888 , pretty < 1.2
891 , pretty < 1.2
889 , process < 1.3
892 , process < 1.3
890 , split < 0.3
893 , split < 0.3
891− , text < 1.3
894+ , text >=1.2.1.0 && < 1.3
892 , time >= 1.4 && < 1.6
895 , time >= 1.4 && < 1.6
893 , transformers < 0.5
896 , transformers < 0.5
894 , transformers-compat >= 0.3
897 , transformers-compat >= 0.3
@@ -911,7 +914,7 @@ Library
911 , TemplateHaskell
914 , TemplateHaskell
912
915
913 ghc-prof-options: -auto-all -caf-all
916 ghc-prof-options: -auto-all -caf-all
914− ghc-options: -threaded -rtsopts
917+ ghc-options: -threaded -rtsopts -O2
915
918
916 if os(linux)
919 if os(linux)
917 cpp-options: -DLINUX
920 cpp-options: -DLINUX
@@ -955,7 +958,7 @@ Executable idris
955 , transformers
958 , transformers
956
959
957 ghc-prof-options: -auto-all -caf-all
960 ghc-prof-options: -auto-all -caf-all
958− ghc-options: -threaded -rtsopts -funbox-strict-fields
961+ ghc-options: -threaded -rtsopts -funbox-strict-fields -O2
959
962
960Executable idris-c
963Executable idris-c
961 Main-is: Main.hs
964 Main-is: Main.hs
@@ -968,7 +971,7 @@ Executable idris-c
968 , transformers
971 , transformers
969
972
970 ghc-prof-options: -auto-all -caf-all
973 ghc-prof-options: -auto-all -caf-all
971− ghc-options: -threaded -rtsopts -funbox-strict-fields
974+ ghc-options: -threaded -rtsopts -funbox-strict-fields -O2
972
975
973Executable idris-javascript
976Executable idris-javascript
974 Main-is: Main.hs
977 Main-is: Main.hs
jsrts/Runtime-node.js+2−2
@@ -1,7 +1,7 @@
1var i$putStr = (function() {
1var i$putStr = (function() {
2− var util = require('util');
2+ var fs = require('fs');
3 return function(s) {
3 return function(s) {
4− util.print(s);
4+ fs.write(1,s);
5 };
5 };
6})();
6})();
7
7
libs/base/Data/Complex.idr+3−1
@@ -22,7 +22,9 @@ instance Eq a => Eq (Complex a) where
22 (==) a b = realPart a == realPart b && imagPart a == imagPart b
22 (==) a b = realPart a == realPart b && imagPart a == imagPart b
23
23
24instance Show a => Show (Complex a) where
24instance 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
26
28
27
29
28
30
libs/base/Language/Reflection/Utils.idr+113−97
@@ -64,23 +64,23 @@ binderTy (PVTy t) = t
64
64
65mutual
65mutual
66 instance Show SpecialName where
66 instance Show SpecialName where
67− show (WhereN i n1 n2) = "(WhereN " ++ show i ++ " " ++
67+ showPrec d (WhereN i n1 n2) = showCon d "WhereN" $ showArg i ++
68− show n1 ++ " " ++ show n2 ++ ")"
68+ showArg n1 ++ showArg n2
69− show (WithN i n) = "(WithN " ++ show i ++ " " ++ show n ++ ")"
69+ showPrec d (WithN i n) = showCon d "WithN" $ showArg i ++ showArg n
70− show (InstanceN i ss) = "(InstanceN " ++ show i ++ " " ++ show ss ++ ")"
70+ showPrec d (InstanceN i ss) = showCon d "InstanceN" $ showArg i ++ showArg ss
71− show (ParentN n s) = "(ParentN " ++ show n ++ " " ++ show s ++ ")"
71+ showPrec d (ParentN n s) = showCon d "ParentN" $ showArg n ++ showArg s
72− show (MethodN n) = "(MethodN " ++ show n ++ ")"
72+ showPrec d (MethodN n) = showCon d "MethodN" $ showArg n
73− show (CaseN n) = "(CaseN " ++ show n ++ ")"
73+ showPrec d (CaseN n) = showCon d "CaseN" $ showArg n
74− show (ElimN n) = "(ElimN " ++ show n ++ ")"
74+ showPrec d (ElimN n) = showCon d "ElimN" $ showArg n
75− show (InstanceCtorN n) = "(InstanceCtorN " ++ show n ++ ")"
75+ showPrec d (InstanceCtorN n) = showCon d "InstanceCtorN" $ showArg n
76− show (MetaN parent meta) = "(MetaN " ++ show parent ++ " " ++ show meta ++ ")"
76+ showPrec d (MetaN parent meta) = showCon d "MetaN" $ showArg parent ++ showArg meta
77
77
78 instance Show TTName where
78 instance Show TTName where
79− show (UN str) = "(UN " ++ show str ++ ")"
79+ showPrec d (UN str) = showCon d "UN" $ showArg str
80− show (NS n ns) = "(NS " ++ show n ++ " " ++ show ns ++ ")"
80+ showPrec d (NS n ns) = showCon d "NS" $ showArg n ++ showArg ns
81− show (MN i str) = "(MN " ++ show i ++ " " ++ show str ++ ")"
81+ showPrec d (MN i str) = showCon d "MN" $ showArg i ++ showArg str
82− show (SN sn) = "(SN " ++ assert_total (show sn) ++ ")"
82+ showPrec d (SN sn) = showCon d "SN" $ assert_total (showArg sn)
83− show NErased = "NErased"
83+ showPrec d NErased = "NErased"
84
84
85mutual
85mutual
86 instance Eq TTName where
86 instance Eq TTName where
@@ -104,28 +104,44 @@ mutual
104 _ == _ = False
104 _ == _ = False
105
105
106instance Show TTUExp where
106instance Show TTUExp where
107− show (UVar i) = "(UVar " ++ show i ++ ")"
107+ showPrec d (UVar i) = showCon d "UVar" $ showArg i
108− show (UVal i) = "(UVal " ++ show i ++ ")"
108+ showPrec d (UVal i) = showCon d "UVal" $ showArg i
109
109
110instance Eq TTUExp where
110instance Eq TTUExp where
111 (UVar i) == (UVar j) = i == j
111 (UVar i) == (UVar j) = i == j
112 (UVal i) == (UVal j) = i == j
112 (UVal i) == (UVal j) = i == j
113 x == y = False
113 x == y = False
114
114
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+
115instance Show Const where
131instance Show Const where
116− show (I i) = "(I " ++ show i ++ ")"
132+ showPrec d (I i) = showCon d "I" $ showArg i
117− show (BI n) = "(BI " ++ show n ++ ")"
133+ showPrec d (BI n) = showCon d "BI" $ showArg n
118− show (Fl f) = "(Fl " ++ show f ++ ")"
134+ showPrec d (Fl f) = showCon d "Fl" $ showArg f
119− show (Ch c) = "(Ch " ++ show c ++ ")"
135+ showPrec d (Ch c) = showCon d "Ch" $ showArg c
120− show (Str str) = "(Str " ++ show str ++ ")"
136+ showPrec d (Str str) = showCon d "Str" $ showArg str
121− show (B8 b) = "(B8 ...)"
137+ showPrec d (B8 b) = showCon d "B8" $ showArg b
122− show (B16 b) = "(B16 ...)"
138+ showPrec d (B16 b) = showCon d "B16" $ showArg b
123− show (B32 b) = "(B32 ...)"
139+ showPrec d (B32 b) = showCon d "B32" $ showArg b
124− show (B64 b) = "(B64 ...)"
140+ showPrec d (B64 b) = showCon d "B64" $ showArg b
125− show (AType x) = "(AType ...)"
141+ showPrec d (AType x) = showCon d "AType" $ showArg x
126− show StrType = "StrType"
142+ showPrec d StrType = "StrType"
127− show VoidType = "VoidType"
143+ showPrec d VoidType = "VoidType"
128− show Forgot = "Forgot"
144+ showPrec d Forgot = "Forgot"
129
145
130instance Eq NativeTy where
146instance Eq NativeTy where
131 IT8 == IT8 = True
147 IT8 == IT8 = True
@@ -164,10 +180,10 @@ instance Eq Const where
164
180
165
181
166instance Show NameType where
182instance Show NameType where
167− show Bound = "Bound"
183+ showPrec d Bound = "Bound"
168− show Ref = "Ref"
184+ showPrec d Ref = "Ref"
169− show (DCon t ar) = "(DCon " ++ show t ++ " " ++ show ar ++ ")"
185+ showPrec d (DCon t ar) = showCon d "DCon" $ showArg t ++ showArg ar
170− show (TCon t ar) = "(TCon " ++ show t ++ " " ++ show ar ++ ")"
186+ showPrec d (TCon t ar) = showCon d "TCon" $ showArg t ++ showArg ar
171
187
172instance Eq NameType where
188instance Eq NameType where
173 Bound == Bound = True
189 Bound == Bound = True
@@ -177,15 +193,15 @@ instance Eq NameType where
177 x == y = False
193 x == y = False
178
194
179instance (Show a) => Show (Binder a) where
195instance (Show a) => Show (Binder a) where
180− show (Lam t) = "(Lam " ++ show t ++ ")"
196+ showPrec d (Lam t) = showCon d "Lam" $ showArg t
181− show (Pi t _) = "(Pi " ++ show t ++ ")"
197+ showPrec d (Pi t1 t2) = showCon d "Pi" $ showArg t1 ++ showArg t2
182− show (Let t1 t2) = "(Let " ++ show t1 ++ " " ++ show t2 ++ ")"
198+ showPrec d (Let t1 t2) = showCon d "Let" $ showArg t1 ++ showArg t2
183− show (NLet t1 t2) = "(NLet " ++ show t1 ++ " " ++ show t2 ++ ")"
199+ showPrec d (NLet t1 t2) = showCon d "NLet" $ showArg t1 ++ showArg t2
184− show (Hole t) = "(Hole " ++ show t ++ ")"
200+ showPrec d (Hole t) = showCon d "Hole" $ showArg t
185− show (GHole t) = "(GHole " ++ show t ++ ")"
201+ showPrec d (GHole t) = showCon d "GHole" $ showArg t
186− show (Guess t1 t2) = "(Guess " ++ show t1 ++ " " ++ show t2 ++ ")"
202+ showPrec d (Guess t1 t2) = showCon d "Guess" $ showArg t1 ++ showArg t2
187− show (PVar t) = "(PVar " ++ show t ++ ")"
203+ showPrec d (PVar t) = showCon d "PVar" $ showArg t
188− show (PVTy t) = "(PVTy " ++ show t ++ ")"
204+ showPrec d (PVTy t) = showCon d "PVTy" $ showArg t
189
205
190instance (Eq a) => Eq (Binder a) where
206instance (Eq a) => Eq (Binder a) where
191 (Lam t) == (Lam t') = t == t'
207 (Lam t) == (Lam t') = t == t'
@@ -200,17 +216,17 @@ instance (Eq a) => Eq (Binder a) where
200 x == y = False
216 x == y = False
201
217
202instance Show TT where
218instance Show TT where
203− show = my_show
219+ showPrec = my_show
204− where %assert_total my_show : TT -> String
220+ where %assert_total my_show : Prec -> TT -> String
205− my_show (P nt n t) = "(P " ++ show nt ++ " " ++ show n ++ " " ++ show t ++ ")"
221+ my_show d (P nt n t) = showCon d "P" $ showArg nt ++ showArg n ++ showArg t
206− my_show (V i) = "(V " ++ show i ++ ")"
222+ my_show d (V i) = showCon d "V" $ showArg i
207− my_show (Bind n b t) = "(Bind " ++ show n ++ " " ++ show b ++ " " ++ show t ++ ")"
223+ my_show d (Bind n b t) = showCon d "Bind" $ showArg n ++ showArg b ++ showArg t
208− my_show (App t1 t2) = "(App " ++ show t1 ++ " " ++ show t2 ++ ")"
224+ my_show d (App t1 t2) = showCon d "App" $ showArg t1 ++ showArg t2
209− my_show (TConst c) = "(TConst " ++ show c ++ ")"
225+ my_show d (TConst c) = showCon d "TConst" $ showArg c
210− my_show (Proj tm i) = "(Proj " ++ show tm ++ " " ++ show i ++ ")"
226+ my_show d (Proj tm i) = showCon d "Proj" $ showArg tm ++ showArg i
211− my_show Erased = "Erased"
227+ my_show d Erased = "Erased"
212− my_show Impossible = "Impossible"
228+ my_show d Impossible = "Impossible"
213− my_show (TType u) = "(TType " ++ show u ++ ")"
229+ my_show d (TType u) = showCon d "TType" $ showArg u
214
230
215instance Eq TT where
231instance Eq TT where
216 a == b = equalp a b
232 a == b = equalp a b
@@ -251,53 +267,53 @@ forget tm = fe [] tm
251 fe env Impossible = Nothing
267 fe env Impossible = Nothing
252
268
253instance Show Raw where
269instance Show Raw where
254− show r = my_show r
270+ showPrec = my_show
255− where %assert_total my_show : Raw -> String
271+ where %assert_total my_show : Prec -> Raw -> String
256− my_show (Var n) = "(Var " ++ show n ++ ")"
272+ my_show d (Var n) = showCon d "Var" $ showArg n
257− my_show (RBind n b tm) = "(RBind " ++ show n ++ " " ++ show b ++ " " ++ my_show tm ++ ")"
273+ my_show d (RBind n b tm) = showCon d "RBind" $ showArg n ++ showArg b ++ " " ++ my_show App tm
258− my_show (RApp tm tm') = "(RApp " ++ my_show tm ++ " " ++ my_show tm' ++ ")"
274+ my_show d (RApp tm tm') = showCon d "RApp" $ " " ++ my_show App tm ++ " " ++ my_show App tm'
259− my_show RType = "RType"
275+ my_show d RType = "RType"
260− my_show (RForce tm) = "(RForce " ++ my_show tm ++ ")"
276+ my_show d (RForce tm) = showCon d "RForce" $ " " ++ my_show App tm
261− my_show (RConstant c) = "(RConstant " ++ show c ++ ")"
277+ my_show d (RConstant c) = showCon d "RConstant" $ showArg c
262
278
263instance Show SourceLocation where
279instance 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
265
281
266instance Show Err where
282instance Show Err where
267− show (Msg x) = "Msg \"" ++ x ++ "\""
283+ showPrec d (Msg x) = showCon d "Msg" $ showArg x
268− show (InternalMsg x) = "InternalMsg \"" ++ x ++ "\""
284+ showPrec d (InternalMsg x) = showCon d "InternalMsg" $ showArg x
269− show (CantUnify x tm tm' err xs y) = "CantUnify " ++ show x ++
285+ showPrec d (CantUnify x tm tm' err xs y) = showCon d "CantUnify" $ showArg x ++
270− " ( " ++ show tm ++ ") (" ++ show tm' ++ ") (" ++ show err ++ ") " ++
286+ showArg tm ++ showArg tm' ++ showArg err ++
271− show xs ++ " " ++ show y
287+ showArg xs ++ showArg y
272− show (InfiniteUnify n tm xs) = "InfiniteUnify " ++ show n ++ show tm ++ show xs
288+ showPrec d (InfiniteUnify n tm xs) = showCon d "InfiniteUnify" $ showArg n ++ showArg tm ++ showArg xs
273− show (CantConvert tm tm' xs) = "CantConvert " ++ show tm ++ show tm' ++ show xs
289+ showPrec d (CantConvert tm tm' xs) = showCon d "CantConvert" $ showArg tm ++ showArg tm' ++ showArg xs
274− show (CantSolveGoal tm ctxt) = "CantSolveGoal " ++ show tm ++ " " ++ show ctxt
290+ showPrec d (CantSolveGoal tm ctxt) = showCon d "CantSolveGoal" $ showArg tm ++ showArg ctxt
275− show (UnifyScope n n' tm xs) = "UnifyScope " ++ show n ++ " " ++ show n' ++ " " ++ show tm ++ " " ++ show xs
291+ showPrec d (UnifyScope n n' tm xs) = showCon d "UnifyScope" $ showArg n ++ showArg n' ++ showArg tm ++ showArg xs
276− show (CantInferType x) = "CantInferType " ++ show x
292+ showPrec d (CantInferType x) = showCon d "CantInferType" $ showArg x
277− show (NonFunctionType tm tm') = "NonFunctionType " ++ show tm ++ show tm'
293+ showPrec d (NonFunctionType tm tm') = showCon d "NonFunctionType" $ showArg tm ++ showArg tm'
278− show (NotEquality tm tm') = "NotEquality " ++ show tm ++ " " ++ show tm'
294+ showPrec d (NotEquality tm tm') = showCon d "NotEquality" $ showArg tm ++ showArg tm'
279− show (TooManyArguments n) = "TooManyArguments " ++ show n
295+ showPrec d (TooManyArguments n) = showCon d "TooManyArguments" $ showArg n
280− show (CantIntroduce tm) = "CantIntroduce " ++ show tm
296+ showPrec d (CantIntroduce tm) = showCon d "CantIntroduce" $ showArg tm
281− show (NoSuchVariable n) = "NoSuchVariable " ++ show n
297+ showPrec d (NoSuchVariable n) = showCon d "NoSuchVariable" $ showArg n
282− show (WithFnType tm) = "WithFnType " ++ show tm
298+ showPrec d (WithFnType tm) = showCon d "WithFnType" $ showArg tm
283− show (CantMatch tm) = "CantMatch " ++ show tm
299+ showPrec d (CantMatch tm) = showCon d "CantMatch" $ showArg tm
284− show (NoTypeDecl n) = "NoTypeDecl " ++ show n
300+ showPrec d (NoTypeDecl n) = showCon d "NoTypeDecl" $ showArg n
285− show (NotInjective tm tm' x) = "NotInjective " ++ show tm ++ " " ++ show tm'
301+ showPrec d (NotInjective tm tm' x) = showCon d "NotInjective" $ showArg tm ++ showArg tm'
286− show (CantResolve tm) = "CantResolve " ++ show tm
302+ showPrec d (CantResolve tm) = showCon d "CantResolve" $ showArg tm
287− show (InvalidTCArg n tm) = "InvalidTCName " ++ show n ++ " (" ++ show tm ++ ")"
303+ showPrec d (InvalidTCArg n tm) = showCon d "InvalidTCName" $ showArg n ++ showArg tm
288− show (CantResolveAlts xs) = "CantResolveAlts " ++ show xs
304+ showPrec d (CantResolveAlts xs) = showCon d "CantResolveAlts" $ showArg xs
289− show (IncompleteTerm tm) = "IncompleteTerm " ++ show tm
305+ showPrec d (IncompleteTerm tm) = showCon d "IncompleteTerm" $ showArg tm
290− show (NoEliminator s tm) = "NoEliminator " ++ show s ++ " " ++ show tm
306+ showPrec d (NoEliminator s tm) = showCon d "NoEliminator" $ showArg s ++ showArg tm
291− show UniverseError = "UniverseError"
307+ showPrec d UniverseError = "UniverseError"
292− show ProgramLineComment = "ProgramLineComment"
308+ showPrec d ProgramLineComment = "ProgramLineComment"
293− show (Inaccessible n) = "Inaccessible " ++ show n
309+ showPrec d (Inaccessible n) = showCon d "Inaccessible" $ showArg n
294− show (UnknownImplicit n f) = "UnknownImplicit " ++ show n ++ " " ++ show f
310+ showPrec d (UnknownImplicit n f) = showCon d "UnknownImplicit" $ showArg n ++ showArg f
295− show (NonCollapsiblePostulate n) = "NonCollapsiblePostulate " ++ show n
311+ showPrec d (NonCollapsiblePostulate n) = showCon d "NonCollapsiblePostulate" $ showArg n
296− show (AlreadyDefined n) = "AlreadyDefined " ++ show n
312+ showPrec d (AlreadyDefined n) = showCon d "AlreadyDefined" $ showArg n
297− show (ProofSearchFail err) = "ProofSearchFail " ++ show err
313+ showPrec d (ProofSearchFail err) = showCon d "ProofSearchFail" $ showArg err
298− show (NoRewriting tm) = "NoRewriting " ++ show tm
314+ showPrec d (NoRewriting tm) = showCon d "NoRewriting" $ showArg tm
299− show (ProviderError x) = "ProviderError \"" ++ show x ++ "\""
315+ showPrec d (ProviderError x) = showCon d "ProviderError" $ showArg x
300− show (LoadingFailed x err) = "LoadingFailed " ++ show x ++ " (" ++ show err ++ ")"
316+ showPrec d (LoadingFailed x err) = showCon d "LoadingFailed" $ showArg x ++ showArg err
301
317
302-------------------------
318-------------------------
303-- Idiom brackets for Raw
319-- Idiom brackets for Raw
libs/contrib/Data/Heap.idr+2−2
@@ -114,8 +114,8 @@ sort = Heap.toList . Heap.fromList
114--------------------------------------------------------------------------------
114--------------------------------------------------------------------------------
115
115
116instance Show a => Show (MaxiphobicHeap a) where
116instance Show a => Show (MaxiphobicHeap a) where
117− show Empty = "Empty"
117+ showPrec d Empty = "Empty"
118− show (Node s l e r) = "Node (" ++ show l ++ " " ++ show e ++ " " ++ show r ++ ")"
118+ showPrec d (Node s l e r) = showCon d "Node" $ " _" ++ showArg l ++ showArg e ++ showArg r
119
119
120instance Eq a => Eq (MaxiphobicHeap a) where
120instance Eq a => Eq (MaxiphobicHeap a) where
121 Empty == Empty = True
121 Empty == Empty = True
libs/prelude/Prelude.idr+1−100
@@ -24,6 +24,7 @@ import public Prelude.Uninhabited
24import public Prelude.Pairs
24import public Prelude.Pairs
25import public Prelude.Stream
25import public Prelude.Stream
26import public Prelude.Providers
26import public Prelude.Providers
27+import public Prelude.Show
27import public Decidable.Equality
28import public Decidable.Equality
28import public Language.Reflection
29import public Language.Reflection
29import public Language.Reflection.Errors
30import public Language.Reflection.Errors
@@ -37,106 +38,6 @@ decAsBool (Yes _) = True
37decAsBool (No _) = False
38decAsBool (No _) = False
38
39
39
40
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−
140---- Functor instances
41---- Functor instances
141
42
142instance Functor PrimIO where
43instance 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,
6 Prelude.Algebra, Prelude.Basics, Prelude.Bool, Prelude.Cast,
6 Prelude.Algebra, Prelude.Basics, Prelude.Bool, Prelude.Cast,
7 Prelude.Classes, Prelude.Nat, Prelude.List,
7 Prelude.Classes, Prelude.Nat, Prelude.List,
8 Prelude.Maybe, Prelude.Monad, Prelude.Applicative, Prelude.Either,
8 Prelude.Maybe, Prelude.Monad, Prelude.Applicative, Prelude.Either,
9− Prelude.Strings, Prelude.Chars, Prelude.Functor,
9+ Prelude.Strings, Prelude.Chars, Prelude.Show, Prelude.Functor,
10 Prelude.Foldable, Prelude.Traversable, Prelude.Bits, Prelude.Stream,
10 Prelude.Foldable, Prelude.Traversable, Prelude.Bits, Prelude.Stream,
11 Prelude.Uninhabited, Prelude.Pairs, Prelude.Providers,
11 Prelude.Uninhabited, Prelude.Pairs, Prelude.Providers,
12
12
rts/Makefile+2−2
@@ -30,8 +30,8 @@ LIBTARGET = libidris_rts.a
30build: $(LIBTARGET) $(DYLIBTARGET)
30build: $(LIBTARGET) $(DYLIBTARGET)
31
31
32$(LIBTARGET) : $(OBJS)
32$(LIBTARGET) : $(OBJS)
33− ar r $(LIBTARGET) $(OBJS)
33+ $(AR) r $(LIBTARGET) $(OBJS)
34− ranlib $(LIBTARGET)
34+ $(RANLIB) $(LIBTARGET)
35
35
36install :
36install :
37 mkdir -p $(TARGET)
37 mkdir -p $(TARGET)
src/IRTS/CodegenC.hs+1−1
@@ -77,7 +77,7 @@ codegenC' defs out exec incs objs libs flags exports iface dbg
77 let args = [gccDbg dbg] ++
77 let args = [gccDbg dbg] ++
78 gccFlags iface ++
78 gccFlags iface ++
79 -- # Any flags defined here which alter the RTS API must also be added to config.mk
79 -- # 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",
81 "-I."] ++ objs ++ ["-x", "c"] ++ envFlags ++
81 "-I."] ++ objs ++ ["-x", "c"] ++ envFlags ++
82 (if (exec == Executable) then [] else ["-c"]) ++
82 (if (exec == Executable) then [] else ["-c"]) ++
83 [tmpn] ++
83 [tmpn] ++
src/IRTS/CodegenJavaScript.hs+5−5
@@ -1329,7 +1329,7 @@ translateBC info bc
1329 | NULL r <- bc = jsNULL info r
1329 | NULL r <- bc = jsNULL info r
1330 | CALL n <- bc = jsCALL info n
1330 | CALL n <- bc = jsCALL info n
1331 | TAILCALL n <- bc = jsTAILCALL info n
1331 | TAILCALL n <- bc = jsTAILCALL info n
1332− | FOREIGNCALL r _ (FStr n) args
1332+ | FOREIGNCALL r _ (FStr n) args
1333 <- bc = jsFOREIGN info r n (map fcall args)
1333 <- bc = jsFOREIGN info r n (map fcall args)
1334 | TOPBASE n <- bc = jsTOPBASE info n
1334 | TOPBASE n <- bc = jsTOPBASE info n
1335 | BASETOP n <- bc = jsBASETOP info n
1335 | BASETOP n <- bc = jsBASETOP info n
@@ -1346,7 +1346,7 @@ translateBC info bc
1346 | otherwise = JSRaw $ "//" ++ show bc
1346 | otherwise = JSRaw $ "//" ++ show bc
1347 where fcall (t, arg) = (toFType t, arg)
1347 where fcall (t, arg) = (toFType t, arg)
1348
1348
1349−toAType (FCon i)
1349+toAType (FCon i)
1350 | i == sUN "JS_IntChar" = ATInt ITChar
1350 | i == sUN "JS_IntChar" = ATInt ITChar
1351 | i == sUN "JS_IntNative" = ATInt ITNative
1351 | i == sUN "JS_IntNative" = ATInt ITNative
1352toAType t = error (show t ++ " not defined in toAType")
1352toAType t = error (show t ++ " not defined in toAType")
@@ -1359,14 +1359,14 @@ toFnType (FApp c [_,r])
1359 | c == sUN "JS_FnBase" = FFunction
1359 | c == sUN "JS_FnBase" = FFunction
1360toFnType t = error (show t ++ " not defined in toFnType")
1360toFnType t = error (show t ++ " not defined in toFnType")
1361
1361
1362−toFType (FCon c)
1362+toFType (FCon c)
1363 | c == sUN "JS_Str" = FString
1363 | c == sUN "JS_Str" = FString
1364 | c == sUN "JS_Float" = FArith ATFloat
1364 | c == sUN "JS_Float" = FArith ATFloat
1365 | c == sUN "JS_Ptr" = FPtr
1365 | c == sUN "JS_Ptr" = FPtr
1366 | c == sUN "JS_Unit" = FUnit
1366 | c == sUN "JS_Unit" = FUnit
1367−toFType (FApp c [_,ity])
1367+toFType (FApp c [_,ity])
1368 | c == sUN "JS_IntT" = FArith (toAType ity)
1368 | c == sUN "JS_IntT" = FArith (toAType ity)
1369−toFType (FApp c [_,fty])
1369+toFType (FApp c [_,fty])
1370 | c == sUN "JS_FnT" = toFnType fty
1370 | c == sUN "JS_FnT" = toFnType fty
1371toFType t = error (show t ++ " not yet defined in toFType")
1371toFType t = error (show t ++ " not yet defined in toFType")
1372
1372
src/Idris/AbsSyntax.hs+6−6
@@ -1623,12 +1623,12 @@ addImpl' inpat env infns imp_meths ist ptm
1623-- names with zero explicit arguments, don't add implicits.
1623-- names with zero explicit arguments, don't add implicits.
1624
1624
1625aiFn :: Bool -> Bool -> Bool
1625aiFn :: Bool -> Bool -> Bool
1626− -> [Name]
1626+ -> [Name]
1627− -> IState -> FC
1627+ -> IState -> FC
1628− -> Name -- ^ function being applied
1628+ -> Name -- ^ function being applied
1629− -> FC -> [[T.Text]]
1629+ -> FC -> [[T.Text]]
1630− -> [PArg] -> -- ^ initial arguments
1630+ -> [PArg] -- ^ initial arguments
1631− Either Err PTerm
1631+ -> Either Err PTerm
1632aiFn inpat True qq imp_meths ist fc f ffc ds []
1632aiFn inpat True qq imp_meths ist fc f ffc ds []
1633 = case lookupDef f (tt_ctxt ist) of
1633 = case lookupDef f (tt_ctxt ist) of
1634 [] -> Right $ PPatvar ffc f
1634 [] -> Right $ PPatvar ffc f
src/Idris/Core/Binary.hs−6
@@ -311,12 +311,6 @@ instance Binary Name where
311 return (SymRef x1)
311 return (SymRef x1)
312 _ -> error "Corrupted binary data for Name"
312 _ -> error "Corrupted binary data for Name"
313
313
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−
320instance Binary SpecialName where
314instance Binary SpecialName where
321 put x
315 put x
322 = case x of
316 = case x of
src/Idris/Delaborate.hs+4−4
@@ -231,14 +231,14 @@ pprintErr' i (InternalMsg s) =
231pprintErr' i (CantUnify _ (x_in, xprov) (y_in, yprov) e sc s) =
231pprintErr' i (CantUnify _ (x_in, xprov) (y_in, yprov) e sc s) =
232 let (x_ns, y_ns, nms) = renameMNs x_in y_in
232 let (x_ns, y_ns, nms) = renameMNs x_in y_in
233 (x, y) = addImplicitDiffs (delab i x_ns) (delab i y_ns) in
233 (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
235 (pprintTerm' i (map (\ (n, b) -> (n, False)) sc
235 (pprintTerm' i (map (\ (n, b) -> (n, False)) sc
236 ++ zip nms (repeat False)) x))
236 ++ zip nms (repeat False)) x))
237 <> case xprov of
237 <> case xprov of
238 Nothing -> empty
238 Nothing -> empty
239 Just t -> text " (" <> pprintProv i sc t <> text ")"
239 Just t -> text " (" <> pprintProv i sc t <> text ")"
240 <$>
240 <$>
241− text "with" <> indented (annTm y_ns
241+ text "and" <> indented (annTm y_ns
242 (pprintTerm' i (map (\ (n, b) -> (n, False)) sc
242 (pprintTerm' i (map (\ (n, b) -> (n, False)) sc
243 ++ zip nms (repeat False)) y))
243 ++ zip nms (repeat False)) y))
244 <> case yprov of
244 <> case yprov of
@@ -257,10 +257,10 @@ pprintErr' i (CantConvert x_in y_in env) =
257 let (x_ns, y_ns, nms) = renameMNs x_in y_in
257 let (x_ns, y_ns, nms) = renameMNs x_in y_in
258 (x, y) = addImplicitDiffs (delab i (flagUnique x_ns))
258 (x, y) = addImplicitDiffs (delab i (flagUnique x_ns))
259 (delab i (flagUnique y_ns)) in
259 (delab i (flagUnique y_ns)) in
260− text "Can't convert" <>
260+ text "Type mismatch between" <>
261 indented (annTm x_ns (pprintTerm' i (map (\ (n, b) -> (n, False)) env)
261 indented (annTm x_ns (pprintTerm' i (map (\ (n, b) -> (n, False)) env)
262 x)) <$>
262 x)) <$>
263− text "with" <>
263+ text "and" <>
264 indented (annTm y_ns (pprintTerm' i (map (\ (n, b) -> (n, False)) env)
264 indented (annTm y_ns (pprintTerm' i (map (\ (n, b) -> (n, False)) env)
265 y)) <>
265 y)) <>
266 if (opt_errContext (idris_options i)) then line <> showSc i env else empty
266 if (opt_errContext (idris_options i)) then line <> showSc i env else empty
src/Idris/Elab/Class.hs+44−16
@@ -1,4 +1,5 @@
1{-# LANGUAGE PatternGuards #-}
1{-# LANGUAGE PatternGuards #-}
2+{-# OPTIONS_GHC -fwarn-missing-signatures #-}
2module Idris.Elab.Class(elabClass) where
3module Idris.Elab.Class(elabClass) where
3
4
4import Idris.AbsSyntax
5import Idris.AbsSyntax
@@ -47,6 +48,7 @@ import qualified Data.Set as S
47import qualified Data.Text as T
48import qualified Data.Text as T
48import Data.Char(isLetter, toLower)
49import Data.Char(isLetter, toLower)
49import Data.List.Split (splitOn)
50import Data.List.Split (splitOn)
51+import Data.Generics.Uniplate.Data (transform)
50
52
51import Util.Pretty(pretty, text)
53import Util.Pretty(pretty, text)
52
54
@@ -83,6 +85,7 @@ elabClass info syn_in doc fc constraints tn tnfc ps pDocs fds ds mcn cd
83 let (methods, imethods)
85 let (methods, imethods)
84 = unzip (map (\ (x, y, z) -> (x, y)) ims)
86 = unzip (map (\ (x, y, z) -> (x, y)) ims)
85 let defaults = map (\ (x, (y, z)) -> (x,y)) defs
87 let defaults = map (\ (x, (y, z)) -> (x,y)) defs
88+
86 -- build instance constructor type
89 -- build instance constructor type
87 let cty = impbind [(pn, pt) | (pn, _, pt) <- ps] $ conbind constraints
90 let cty = impbind [(pn, pt) | (pn, _, pt) <- ps] $ conbind constraints
88 $ pibind (map (\ (n, ty) -> (nsroot n, ty)) methods)
91 $ 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
92 let ddecl = PDatadecl tn NoFC tty cons
95 let ddecl = PDatadecl tn NoFC tty cons
93
96
94 logLvl 5 $ "Class data " ++ show (showDImp verbosePPOption ddecl)
97 logLvl 5 $ "Class data " ++ show (showDImp verbosePPOption ddecl)
98+
95 -- Elaborate the data declaration
99 -- Elaborate the data declaration
96 elabData info (syn { no_imp = no_imp syn ++ mnames,
100 elabData info (syn { no_imp = no_imp syn ++ mnames,
97 imp_methods = mnames }) doc pDocs fc [] ddecl
101 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
118 [(pnfc, AnnBoundName pn False) | (pn, pnfc, _) <- ps] ++
122 [(pnfc, AnnBoundName pn False) | (pn, pnfc, _) <- ps] ++
119 [(fdfc, AnnBoundName fc False) | (fc, fdfc) <- fds] ++
123 [(fdfc, AnnBoundName fc False) | (fc, fdfc) <- fds] ++
120 maybe [] (\(conN, conNFC) -> [(conNFC, AnnName conN Nothing Nothing Nothing)]) mcn
124 maybe [] (\(conN, conNFC) -> [(conNFC, AnnName conN Nothing Nothing Nothing)]) mcn
121−
125+
122 where
126 where
123 nodoc (n, (_, _, o, t)) = (n, (o, t))
127 nodoc (n, (_, _, o, t)) = (n, (o, t))
124
128
@@ -132,11 +136,6 @@ elabClass info syn_in doc fc constraints tn tnfc ps pDocs fds ds mcn cd
132 chkUniq (PPi _ _ _ _ sc) t = chkUniq sc t
136 chkUniq (PPi _ _ _ _ sc) t = chkUniq sc t
133 chkUniq _ t = t
137 chkUniq _ t = t
134
138
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−
140 -- TODO: probably should normalise
139 -- TODO: probably should normalise
141 checkDefaultSuperclassInstance :: PDecl -> Idris ()
140 checkDefaultSuperclassInstance :: PDecl -> Idris ()
142 checkDefaultSuperclassInstance (PInstance _ _ _ fc cs n _ ps _ _ _)
141 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
171 defdecl mtys c d@(PClauses fc opts n cs) =
170 defdecl mtys c d@(PClauses fc opts n cs) =
172 case lookup n mtys of
171 case lookup n mtys of
173 Just (nfc, syn, o, ty) ->
172 Just (nfc, syn, o, ty) ->
174− do let ty' = insertConstraint c ty
173+ do let ty' = insertConstraint c (map fst mtys) ty
175 let ds = map (decorateid defaultdec)
174 let ds = map (decorateid defaultdec)
176 [PTy emptyDocstring [] syn fc [] n nfc ty',
175 [PTy emptyDocstring [] syn fc [] n nfc ty',
177 PClauses fc (o ++ opts) n cs]
176 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
215 return [PTy emptyDocstring [] syn fc [] cfn NoFC ty,
214 return [PTy emptyDocstring [] syn fc [] cfn NoFC ty,
216 PClauses fc [Dictionary] cfn [PClause fc cfn lhs [] rhs []]]
215 PClauses fc [Dictionary] cfn [PClause fc cfn lhs [] rhs []]]
217
216
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
219 -- dictionary (this is inlinable, always)
218 -- 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]
220 tfun cn c syn all (m, (mfc, doc, o, ty))
225 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)
222 let mnames = take (length all) $ map (\x -> sMN x "meth") [0..]
227 let mnames = take (length all) $ map (\x -> sMN x "meth") [0..]
223 let capp = PApp fc (PRef fc cn) (map (pexp . PRef fc) mnames)
228 let capp = PApp fc (PRef fc cn) (map (pexp . PRef fc) mnames)
224 let margs = getMArgs ty
229 let margs = getMArgs ty
@@ -236,6 +241,7 @@ elabClass info syn_in doc fc constraints tn tnfc ps pDocs fds ds mcn cd
236 getMArgs (PPi (Constraint _ _) n _ ty sc) = CA : getMArgs sc
241 getMArgs (PPi (Constraint _ _) n _ ty sc) = CA : getMArgs sc
237 getMArgs _ = []
242 getMArgs _ = []
238
243
244+ getMeth :: [Name] -> [Name] -> Name -> PTerm
239 getMeth (m:ms) (a:as) x | x == a = PRef fc m
245 getMeth (m:ms) (a:as) x | x == a = PRef fc m
240 | otherwise = getMeth ms as x
246 | otherwise = getMeth ms as x
241
247
@@ -249,10 +255,24 @@ elabClass info syn_in doc fc constraints tn tnfc ps pDocs fds ds mcn cd
249 rhsArgs (CA : xs) ns = pconst (PResolveTC fc) : rhsArgs xs ns
255 rhsArgs (CA : xs) ns = pconst (PResolveTC fc) : rhsArgs xs ns
250 rhsArgs [] _ = []
256 rhsArgs [] _ = []
251
257
258+ insertConstraint :: PTerm -> [Name] -> PTerm -> PTerm
252− insertConstraint c (PPi p@(Imp _ _ _ _) n fc ty sc)
259+ insertConstraint c all (PPi p@(Imp _ _ _ _) n fc ty sc)
253− = PPi p n fc ty (insertConstraint c sc)
260+ = PPi p n fc ty (insertConstraint c all sc)
261+ insertConstraint c all sc = let dictN = sMN 0 "class"
254− insertConstraint c sc = PPi (constraint { pstatic = Static })
262+ in PPi (constraint { pstatic = Static })
255− (sMN 0 "class") NoFC c sc
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
256
276
257 -- make arguments explicit and don't bind class parameters
277 -- make arguments explicit and don't bind class parameters
258 toExp ns e (PPi (Imp l s p _) n fc ty sc)
278 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
261 toExp ns e (PPi p n fc ty sc) = PPi p n fc ty (toExp ns e sc)
281 toExp ns e (PPi p n fc ty sc) = PPi p n fc ty (toExp ns e sc)
262 toExp ns e sc = sc
282 toExp ns e sc = sc
263
283
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
264memberDocs :: PDecl -> Maybe (Name, Docstring (Either Err PTerm))
291memberDocs :: PDecl -> Maybe (Name, Docstring (Either Err PTerm))
265memberDocs (PTy d _ _ _ _ n _ _) = Just (basename n, d)
292memberDocs (PTy d _ _ _ _ n _ _) = Just (basename n, d)
266memberDocs (PPostulate _ d _ _ _ n _) = Just (basename n, d)
293memberDocs (PPostulate _ d _ _ _ n _) = Just (basename n, d)
@@ -270,17 +297,18 @@ memberDocs (PClass d _ _ _ n _ _ _ _ _ _ _) = Just (basename n, d)
270memberDocs _ = Nothing
297memberDocs _ = Nothing
271
298
272
299
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
274-- so that we don't have to disambiguate later
301-- so that we don't have to disambiguate later
275−expandMethNS :: SyntaxInfo
302+expandMethNS :: SyntaxInfo
276 -> PTerm -> PTerm
303 -> PTerm -> PTerm
277expandMethNS syn = mapPT expand
304expandMethNS syn = mapPT expand
278 where
305 where
279 expand (PRef fc n) | n `elem` imp_methods syn = PRef fc $ expandNS syn n
306 expand (PRef fc n) | n `elem` imp_methods syn = PRef fc $ expandNS syn n
280 expand t = t
307 expand t = t
281
308
309+-- | Find the determining parameter locations
282findDets :: Name -> [Name] -> Idris [Int]
310findDets :: Name -> [Name] -> Idris [Int]
283−findDets n ns =
311+findDets n ns =
284 do i <- getIState
312 do i <- getIState
285 return $ case lookupTyExact n (tt_ctxt i) of
313 return $ case lookupTyExact n (tt_ctxt i) of
286 Just ty -> getDetPos 0 ns ty
314 Just ty -> getDetPos 0 ns ty
src/Idris/Parser.hs+12−6
@@ -1271,12 +1271,18 @@ parseImports fname input
1271
1271
1272-- | There should be a better way of doing this...
1272-- | There should be a better way of doing this...
1273findFC :: Doc -> (FC, String)
1273findFC :: Doc -> (FC, String)
1274−findFC x = let s = show (plain x) in
1274+findFC x = let s = show (plain x) in findFC' s
1275− case span (/= ':') s of
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)
1276− (failname, ':':rest) -> case span isDigit rest of
1282+ (failname, ':':rest) -> case span isDigit rest of
1277− (line, ':':rest') -> case span isDigit rest' of
1283+ (line, ':':rest') -> case span isDigit rest' of
1278− (col, ':':msg) -> let pos = (read line, read col) in
1284+ (col, ':':msg) -> let pos = (read line, read col) in
1279− (FC failname pos pos, msg)
1285+ (FC failname pos pos, msg)
1280
1286
1281-- | Check if the coloring matches the options and corrects if necessary
1287-- | Check if the coloring matches the options and corrects if necessary
1282fixColour :: Bool -> ANSI.Doc -> ANSI.Doc
1288fixColour :: Bool -> ANSI.Doc -> ANSI.Doc
test/basic006/expected+2−2
@@ -1,8 +1,8 @@
1test020a.idr:16:18:When elaborating right hand side of foo:
1test020a.idr:16:18:When elaborating right hand side of foo:
2When elaborating an application of function Prelude.List.reverse:
2When elaborating an application of function Prelude.List.reverse:
3− Can't unify
3+ Type mismatch between
4 Vect n a (Type of xs)
4 Vect n a (Type of xs)
5− with
5+ and
6 List a (Expected type)
6 List a (Expected type)
7[3, 2, 1]
7[3, 2, 1]
8"Number 42"
8"Number 42"
test/disambig001/disambig001.idr+1−1
@@ -8,5 +8,5 @@ import Effect.System
8main : IO ()
8main : IO ()
9main = do
9main = do
10 args <- System.getArgs
10 args <- System.getArgs
11− putStrLn (concat args)
11+ putStrLn (concat (drop 1 args))
12
12
test/disambig001/expected+1−1
@@ -1 +1 @@
1−./disambig001foobar
1+foobar
test/proof002/expected+4−4
@@ -1,13 +1,13 @@
1Reflect.idr:208:38:
1Reflect.idr:208:38:
2When elaborating right hand side of testReflect1:
2When elaborating right hand side of testReflect1:
3When elaborating an application of function Reflect.getJust:
3When elaborating an application of function Reflect.getJust:
4− Can't unify
4+ Type mismatch between
5 IsJust (Just x1) (Type of ItIsJust)
5 IsJust (Just x1) (Type of ItIsJust)
6− with
6+ and
7 IsJust (prove (getProof x)) (Expected type)
7 IsJust (prove (getProof x)) (Expected type)
8
8
9 Specifically:
9 Specifically:
10− Can't unify
10+ Type mismatch between
11 Just x
11 Just x
12− with
12+ and
13 Nothing
13 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)))))
2--------------
2--------------
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))))
4--------------
4--------------
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 @@
1reg007.lidr:8:1:A.n is already defined
1reg007.lidr:8:1:A.n is already defined
2reg007.lidr:12:11-17:When elaborating right hand side of hurrah:
2reg007.lidr:12:11-17:When elaborating right hand side of hurrah:
3−Can't unify
3+Type mismatch between
4 n = lala (Type of isSame)
4 n = lala (Type of isSame)
5−with
5+and
6 0 = 1 (Expected type)
6 0 = 1 (Expected type)
7
7
8Specifically:
8Specifically:
9− Can't unify
9+ Type mismatch between
10 1
10 1
11− with
11+ and
12 0
12 0
test/reg023/expected+2−2
@@ -1,5 +1,5 @@
1reg023.idr:7:5:When elaborating right hand side of bad:
1reg023.idr:7:5:When elaborating right hand side of bad:
2−Can't unify
2+Type mismatch between
3 Nat (Type of 0)
3 Nat (Type of 0)
4−with
4+and
5 f Nat (Expected type)
5 f Nat (Expected type)
test/reg044/expected+4−4
@@ -1,11 +1,11 @@
1reg044.idr:4:4:When elaborating right hand side of Main.pf:
1reg044.idr:4:4:When elaborating right hand side of Main.pf:
2−Can't unify
2+Type mismatch between
3 b = b (Type of Refl)
3 b = b (Type of Refl)
4−with
4+and
5 a = b (Expected type)
5 a = b (Expected type)
6
6
7Specifically:
7Specifically:
8− Can't unify
8+ Type mismatch between
9 b
9 b
10− with
10+ and
11 a
11 a
test/reg054/expected+2−2
@@ -6,7 +6,7 @@ When elaborating argument x to Main.weird:
6 No explicit types on left hand side: Char
6 No explicit types on left hand side: Char
7reg054.idr:37:1-8:When elaborating left hand side of tctrick:
7reg054.idr:37:1-8:When elaborating left hand side of tctrick:
8When elaborating an application of Main.tctrick:
8When elaborating an application of Main.tctrick:
9− Can't unify
9+ Type mismatch between
10 Maybe a1 (Type of Just x)
10 Maybe a1 (Type of Just x)
11− with
11+ and
12 a (Expected type)
12 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 @@
1tutorial006a.idr:5:23-25:
1tutorial006a.idr:5:23-25:
2When elaborating right hand side of vapp:
2When elaborating right hand side of vapp:
3When elaborating argument xs to constructor Data.VectType.Vect.:::
3When elaborating argument xs to constructor Data.VectType.Vect.:::
4− Can't unify
4+ Type mismatch between
5 Vect (n + n) a (Type of vapp xs xs)
5 Vect (n + n) a (Type of vapp xs xs)
6− with
6+ and
7 Vect (plus n m) a (Expected type)
7 Vect (plus n m) a (Expected type)
8
8
9 Specifically:
9 Specifically:
10− Can't unify
10+ Type mismatch between
11 plus n n
11 plus n n
12− with
12+ and
13 plus n m
13 plus n m
14tutorial006b.idr:10:10:
14tutorial006b.idr:10:10:
15When elaborating right hand side of with block in Main.parity:
15When elaborating right hand side of with block in Main.parity:
16−Can't unify
16+Type mismatch between
17 Parity (plus (S j) (S j)) (Type of even)
17 Parity (plus (S j) (S j)) (Type of even)
18−with
18+and
19 Parity (S (S (plus j j))) (Expected type)
19 Parity (S (S (plus j j))) (Expected type)
20
20
21Specifically:
21Specifically:
22− Can't unify
22+ Type mismatch between
23 plus (S j) (S j)
23 plus (S j) (S j)
24− with
24+ and
25 S (S (plus j j))
25 S (S (plus j j))
test/unique001/expected+6−6
@@ -2,17 +2,17 @@
219,18,17,16,15,14,13,12,11,10,9,8,7,6,5,4,3,2,1,0,END
219,18,17,16,15,14,13,12,11,10,9,8,7,6,5,4,3,2,1,0,END
338,36,34,32,30,28,26,24,22,20,18,16,14,12,10,8,6,4,2,0,END
338,36,34,32,30,28,26,24,22,20,18,16,14,12,10,8,6,4,2,0,END
438,36,34,32,30,28,26,24,22,20,18,16,14,12,10,8,6,4,2,0,END
438,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
6 Int -> String
6 Int -> String
7−with
7+and
8 UniqueType (Int -> String)
8 UniqueType (Int -> String)
9−unique001a.idr:44:12:Can't convert
9+unique001a.idr:44:12:Type mismatch between
10 Int -> String
10 Int -> String
11−with
11+and
12 UniqueType (Int -> String)
12 UniqueType (Int -> String)
13−unique001a.idr:55:12:Can't convert
13+unique001a.idr:55:12:Type mismatch between
14 UniqueType (Int -> String)
14 UniqueType (Int -> String)
15−with
15+and
16 Int -> String
16 Int -> String
17unique001b.idr:16:7:Borrowed name xs must not be used on RHS
17unique001b.idr:16:7:Borrowed name xs must not be used on RHS
18unique001c.idr:46:6:Unique name f is used more than once
18unique001c.idr:46:6:Unique name f is used more than once
test/unique002/expected+2−2
@@ -1,5 +1,5 @@
1unique002.idr:15:5:Unique name xs is used more than once
1unique002.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
3 Int -> String
3 Int -> String
4−with
4+and
5 UniqueType (Int -> String)
5 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
2 Int -> String
2 Int -> String
3−with
3+and
4 UniqueType (Int -> String)
4 UniqueType (Int -> String)