sigrid/idris2

.gitignore+1−1

@@ -10,7 +10,7 @@ · 9 unmodified lines
10		10
11	/dist/idris2.c	11	/dist/idris2.c
12		12
13	/docs/_build/	13	/docs/build/
14		14
15	/libs/**/build	15	/libs/**/build
16	/tests/**/output	16	/tests/**/output

INSTALL.md+1−1

@@ -2,7 +2,7 @@ · 1 unmodified line
2		2
3	Idris 2 is built using Idris, and provides support for two default code	3	Idris 2 is built using Idris, and provides support for two default code
4	generation targets: Chez Scheme, and Racket. To build from source, it requires	4	generation targets: Chez Scheme, and Racket. To build from source, it requires
5	at least Idris version 1.3.2 (see https://www.idris-lang.org/download). You	5	at least Idris version 1.3.2 (see https://www.idris-lang.org/pages/download.html). You
6	can also build from the generated C.	6	can also build from the generated C.
7		7
8	## Quick summary:	8	## Quick summary:

README.md+2−0

@@ -1,6 +1,8 @@
1	Idris 2	1	Idris 2
2	=======	2	=======
3		3
		4	[![Build Status](https://travis-ci.org/edwinb/Idris2.svg?branch=master)](https://travis-ci.org/edwinb/Idris2)
		5
4	This is a pre-alpha implementation of Idris 2, the successor to Idris.	6	This is a pre-alpha implementation of Idris 2, the successor to Idris.
5		7
6	* Please note: To build, this requires Idris version 1.3.2 *	8	* Please note: To build, this requires Idris version 1.3.2 *

docs/Makefile+14−177

@@ -1,183 +1,20 @@
1	# Makefile for Sphinx documentation	1	# Minimal makefile for Sphinx documentation
2	#	2	#
3		3
4	# You can set these variables from the command line.	4	# You can set these variables from the command line, and also
5	SPHINXOPTS =	5	# from the environment for the first two.
6	SPHINXBUILD = sphinx-build	6	SPHINXOPTS ?=
7	PAPER =	7	SPHINXBUILD ?= sphinx-build
8	BUILDDIR = _build	8	SOURCEDIR = source
9		9	BUILDDIR = build
10	# User-friendly check for sphinx-build
11	ifeq ($(shell which $(SPHINXBUILD) >/dev/null 2>&1; echo $$?), 1)
12	$(error The '$(SPHINXBUILD)' command was not found. Make sure you have Sphinx installed, then set the SPHINXBUILD environment variable to point to the full path of the '$(SPHINXBUILD)' executable. Alternatively you can add the directory with the executable to your PATH. If you don't have Sphinx installed, grab it from https://www.sphinx-doc.org/)
13	endif
14
15	# Internal variables.
16	PAPEROPT_a4 = -D latex_paper_size=a4
17	PAPEROPT_letter = -D latex_paper_size=letter
18	ALLSPHINXOPTS = -d $(BUILDDIR)/doctrees $(PAPEROPT_$(PAPER)) $(SPHINXOPTS) .
19	# the i18n builder cannot share the environment and doctrees with the others
20	I18NSPHINXOPTS = $(PAPEROPT_$(PAPER)) $(SPHINXOPTS) .
21
22	.PHONY: help clean html dirhtml singlehtml pickle json htmlhelp qthelp devhelp epub latex latexpdf text man changes linkcheck doctest coverage gettext
23		10
		11	# Put it first so that "make" without argument is like "make help".
24	help:	12	help:
25	@echo "Please use \`make <target>' where <target> is one of"	13	@$(SPHINXBUILD) -M help "$(SOURCEDIR)" "$(BUILDDIR)" $(SPHINXOPTS) $(O)
26	@echo " html to make standalone HTML files"
27	@echo " dirhtml to make HTML files named index.html in directories"
28	@echo " singlehtml to make a single large HTML file"
29	@echo " pickle to make pickle files"
30	@echo " json to make JSON files"
31	@echo " htmlhelp to make HTML files and a HTML help project"
32	@echo " qthelp to make HTML files and a qthelp project"
33	@echo " devhelp to make HTML files and a Devhelp project"
34	@echo " epub to make an epub"
35	@echo " latex to make LaTeX files, you can set PAPER=a4 or PAPER=letter"
36	@echo " latexpdf to make LaTeX files and run them through pdflatex"
37	@echo " latexpdfja to make LaTeX files and run them through platex/dvipdfmx"
38	@echo " text to make text files"
39	@echo " man to make manual pages"
40	@echo " texinfo to make Texinfo files"
41	@echo " info to make Texinfo files and run them through makeinfo"
42	@echo " gettext to make PO message catalogs"
43	@echo " changes to make an overview of all changed/added/deprecated items"
44	@echo " xml to make Docutils-native XML files"
45	@echo " pseudoxml to make pseudoxml-XML files for display purposes"
46	@echo " linkcheck to check all external links for integrity"
47	@echo " doctest to run all doctests embedded in the documentation (if enabled)"
48	@echo " coverage to run coverage check of the documentation (if enabled)"
49
50	clean:
51	rm -rf $(BUILDDIR)/*
52
53	html:
54	$(SPHINXBUILD) -b html $(ALLSPHINXOPTS) $(BUILDDIR)/html
55	@echo
56	@echo "Build finished. The HTML pages are in $(BUILDDIR)/html."
57
58	dirhtml:
59	$(SPHINXBUILD) -b dirhtml $(ALLSPHINXOPTS) $(BUILDDIR)/dirhtml
60	@echo
61	@echo "Build finished. The HTML pages are in $(BUILDDIR)/dirhtml."
62
63	singlehtml:
64	$(SPHINXBUILD) -b singlehtml $(ALLSPHINXOPTS) $(BUILDDIR)/singlehtml
65	@echo
66	@echo "Build finished. The HTML page is in $(BUILDDIR)/singlehtml."
67
68	pickle:
69	$(SPHINXBUILD) -b pickle $(ALLSPHINXOPTS) $(BUILDDIR)/pickle
70	@echo
71	@echo "Build finished; now you can process the pickle files."
72
73	json:
74	$(SPHINXBUILD) -b json $(ALLSPHINXOPTS) $(BUILDDIR)/json
75	@echo
76	@echo "Build finished; now you can process the JSON files."
77
78	htmlhelp:
79	$(SPHINXBUILD) -b htmlhelp $(ALLSPHINXOPTS) $(BUILDDIR)/htmlhelp
80	@echo
81	@echo "Build finished; now you can run HTML Help Workshop with the" \
82	".hhp project file in $(BUILDDIR)/htmlhelp."
83
84	qthelp:
85	$(SPHINXBUILD) -b qthelp $(ALLSPHINXOPTS) $(BUILDDIR)/qthelp
86	@echo
87	@echo "Build finished; now you can run "qcollectiongenerator" with the" \
88	".qhcp project file in $(BUILDDIR)/qthelp, like this:"
89	@echo "# qcollectiongenerator $(BUILDDIR)/qthelp/IdrisManual.qhcp"
90	@echo "To view the help file:"
91	@echo "# assistant -collectionFile $(BUILDDIR)/qthelp/IdrisManual.qhc"
92
93	devhelp:
94	$(SPHINXBUILD) -b devhelp $(ALLSPHINXOPTS) $(BUILDDIR)/devhelp
95	@echo
96	@echo "Build finished."
97	@echo "To view the help file:"
98	@echo "# mkdir -p $$HOME/.local/share/devhelp/IdrisManual"
99	@echo "# ln -s $(BUILDDIR)/devhelp $$HOME/.local/share/devhelp/IdrisManual"
100	@echo "# devhelp"
101
102	epub:
103	$(SPHINXBUILD) -b epub $(ALLSPHINXOPTS) $(BUILDDIR)/epub
104	@echo
105	@echo "Build finished. The epub file is in $(BUILDDIR)/epub."
106
107	latex:
108	$(SPHINXBUILD) -b latex $(ALLSPHINXOPTS) $(BUILDDIR)/latex
109	@echo
110	@echo "Build finished; the LaTeX files are in $(BUILDDIR)/latex."
111	@echo "Run \`make' in that directory to run these through (pdf)latex" \
112	"(use \`make latexpdf' here to do that automatically)."
113
114	latexpdf:
115	$(SPHINXBUILD) -b latex $(ALLSPHINXOPTS) $(BUILDDIR)/latex
116	@echo "Running LaTeX files through pdflatex..."
117	$(MAKE) -C $(BUILDDIR)/latex all-pdf
118	@echo "pdflatex finished; the PDF files are in $(BUILDDIR)/latex."
119
120	latexpdfja:
121	$(SPHINXBUILD) -b latex $(ALLSPHINXOPTS) $(BUILDDIR)/latex
122	@echo "Running LaTeX files through platex and dvipdfmx..."
123	$(MAKE) -C $(BUILDDIR)/latex all-pdf-ja
124	@echo "pdflatex finished; the PDF files are in $(BUILDDIR)/latex."
125
126	text:
127	$(SPHINXBUILD) -b text $(ALLSPHINXOPTS) $(BUILDDIR)/text
128	@echo
129	@echo "Build finished. The text files are in $(BUILDDIR)/text."
130
131	man:
132	$(SPHINXBUILD) -b man $(ALLSPHINXOPTS) $(BUILDDIR)/man
133	@echo
134	@echo "Build finished. The manual pages are in $(BUILDDIR)/man."
135
136	texinfo:
137	$(SPHINXBUILD) -b texinfo $(ALLSPHINXOPTS) $(BUILDDIR)/texinfo
138	@echo
139	@echo "Build finished. The Texinfo files are in $(BUILDDIR)/texinfo."
140	@echo "Run \`make' in that directory to run these through makeinfo" \
141	"(use \`make info' here to do that automatically)."
142
143	info:
144	$(SPHINXBUILD) -b texinfo $(ALLSPHINXOPTS) $(BUILDDIR)/texinfo
145	@echo "Running Texinfo files through makeinfo..."
146	make -C $(BUILDDIR)/texinfo info
147	@echo "makeinfo finished; the Info files are in $(BUILDDIR)/texinfo."
148
149	gettext:
150	$(SPHINXBUILD) -b gettext $(I18NSPHINXOPTS) $(BUILDDIR)/locale
151	@echo
152	@echo "Build finished. The message catalogs are in $(BUILDDIR)/locale."
153
154	changes:
155	$(SPHINXBUILD) -b changes $(ALLSPHINXOPTS) $(BUILDDIR)/changes
156	@echo
157	@echo "The overview file is in $(BUILDDIR)/changes."
158
159	linkcheck:
160	$(SPHINXBUILD) -b linkcheck $(ALLSPHINXOPTS) $(BUILDDIR)/linkcheck
161	@echo
162	@echo "Link check complete; look for any errors in the above output " \
163	"or in $(BUILDDIR)/linkcheck/output.txt."
164
165	doctest:
166	$(SPHINXBUILD) -b doctest $(ALLSPHINXOPTS) $(BUILDDIR)/doctest
167	@echo "Testing of doctests in the sources finished, look at the " \
168	"results in $(BUILDDIR)/doctest/output.txt."
169
170	coverage:
171	$(SPHINXBUILD) -b coverage $(ALLSPHINXOPTS) $(BUILDDIR)/coverage
172	@echo "Testing of coverage in the sources finished, look at the " \
173	"results in $(BUILDDIR)/coverage/python.txt."
174		14
175	xml:	15	.PHONY: help Makefile
176	$(SPHINXBUILD) -b xml $(ALLSPHINXOPTS) $(BUILDDIR)/xml
177	@echo
178	@echo "Build finished. The XML files are in $(BUILDDIR)/xml."
179		16
180	pseudoxml:	17	# Catch-all target: route all unknown targets to Sphinx using the new
181	$(SPHINXBUILD) -b pseudoxml $(ALLSPHINXOPTS) $(BUILDDIR)/pseudoxml	18	# "make mode" option. $(O) is meant as a shortcut for $(SPHINXOPTS).
182	@echo	19	%: Makefile
183	@echo "Build finished. The pseudo-XML files are in $(BUILDDIR)/pseudoxml."	20	@$(SPHINXBUILD) -M $@ "$(SOURCEDIR)" "$(BUILDDIR)" $(SPHINXOPTS) $(O)

docs/README.md+6−1

 Python should be installed by default on most systems.
 Sphinx can be installed either through your hosts package manager or using pip/easy_install.
+Recommended way is to use virtual environment for building documentation.
 *Note* [ReadTheDocs](https://readthedocs.org) works with Sphinx
  `v1.2.2`. If you install a more recent version of sphinx then
  of readthedocs and be ignored. In the past we had several code-blocks
  disappear because of that.
-The ReadTheDocs theme can be installed using pip as follows:
+The ReadTheDocs theme can be installed in virtual environment using pip as follows:
 ```sh
+python3 -m venv idris2docs_venv
+source idris2docs_venv/bin/activate
+pip install --upgrade pip
 pip install sphinx_rtd_theme
 ```
 ## Build Instructions
 ```sh
+cd docs
 make html
 make latexpdf
 ```

docs/make.bat+35−263

@@ -1,263 +1,35 @@
1	@ECHO OFF	1	@ECHO OFF
2		2
3	REM Command file for Sphinx documentation	3	pushd %~dp0
4		4
5	if "%SPHINXBUILD%" == "" (	5	REM Command file for Sphinx documentation
6	set SPHINXBUILD=sphinx-build	6
7	)	7	if "%SPHINXBUILD%" == "" (
8	set BUILDDIR=_build	8	set SPHINXBUILD=sphinx-build
9	set ALLSPHINXOPTS=-d %BUILDDIR%/doctrees %SPHINXOPTS% .	9	)
10	set I18NSPHINXOPTS=%SPHINXOPTS% .	10	set SOURCEDIR=source
11	if NOT "%PAPER%" == "" (	11	set BUILDDIR=build
12	set ALLSPHINXOPTS=-D latex_paper_size=%PAPER% %ALLSPHINXOPTS%	12
13	set I18NSPHINXOPTS=-D latex_paper_size=%PAPER% %I18NSPHINXOPTS%	13	if "%1" == "" goto help
14	)	14
15		15	%SPHINXBUILD% >NUL 2>NUL
16	if "%1" == "" goto help	16	if errorlevel 9009 (
17		17	echo.
18	if "%1" == "help" (	18	echo.The 'sphinx-build' command was not found. Make sure you have Sphinx
19	:help	19	echo.installed, then set the SPHINXBUILD environment variable to point
20	echo.Please use `make ^<target^>` where ^<target^> is one of	20	echo.to the full path of the 'sphinx-build' executable. Alternatively you
21	echo. html to make standalone HTML files	21	echo.may add the Sphinx directory to PATH.
22	echo. dirhtml to make HTML files named index.html in directories	22	echo.
23	echo. singlehtml to make a single large HTML file	23	echo.If you don't have Sphinx installed, grab it from
24	echo. pickle to make pickle files	24	echo.http://sphinx-doc.org/
25	echo. json to make JSON files	25	exit /b 1
26	echo. htmlhelp to make HTML files and a HTML help project	26	)
27	echo. qthelp to make HTML files and a qthelp project	27
28	echo. devhelp to make HTML files and a Devhelp project	28	%SPHINXBUILD% -M %1 %SOURCEDIR% %BUILDDIR% %SPHINXOPTS% %O%
29	echo. epub to make an epub	29	goto end
30	echo. latex to make LaTeX files, you can set PAPER=a4 or PAPER=letter	30
31	echo. text to make text files	31	:help
32	echo. man to make manual pages	32	%SPHINXBUILD% -M help %SOURCEDIR% %BUILDDIR% %SPHINXOPTS% %O%
33	echo. texinfo to make Texinfo files	33
34	echo. gettext to make PO message catalogs	34	:end
35	echo. changes to make an overview over all changed/added/deprecated items	35	popd
36	echo. xml to make Docutils-native XML files
37	echo. pseudoxml to make pseudoxml-XML files for display purposes
38	echo. linkcheck to check all external links for integrity
39	echo. doctest to run all doctests embedded in the documentation if enabled
40	echo. coverage to run coverage check of the documentation if enabled
41	goto end
42	)
43
44	if "%1" == "clean" (
45	for /d %%i in (%BUILDDIR%\*) do rmdir /q /s %%i
46	del /q /s %BUILDDIR%\*
47	goto end
48	)
49
50
51	REM Check if sphinx-build is available and fallback to Python version if any
52	%SPHINXBUILD% 2> nul
53	if errorlevel 9009 goto sphinx_python
54	goto sphinx_ok
55
56	:sphinx_python
57
58	set SPHINXBUILD=python -m sphinx.__init__
59	%SPHINXBUILD% 2> nul
60	if errorlevel 9009 (
61	echo.
62	echo.The 'sphinx-build' command was not found. Make sure you have Sphinx
63	echo.installed, then set the SPHINXBUILD environment variable to point
64	echo.to the full path of the 'sphinx-build' executable. Alternatively you
65	echo.may add the Sphinx directory to PATH.
66	echo.
67	echo.If you don't have Sphinx installed, grab it from
68	echo.https://www.sphinx-doc.org/
69	exit /b 1
70	)
71
72	:sphinx_ok
73
74
75	if "%1" == "html" (
76	%SPHINXBUILD% -b html %ALLSPHINXOPTS% %BUILDDIR%/html
77	if errorlevel 1 exit /b 1
78	echo.
79	echo.Build finished. The HTML pages are in %BUILDDIR%/html.
80	goto end
81	)
82
83	if "%1" == "dirhtml" (
84	%SPHINXBUILD% -b dirhtml %ALLSPHINXOPTS% %BUILDDIR%/dirhtml
85	if errorlevel 1 exit /b 1
86	echo.
87	echo.Build finished. The HTML pages are in %BUILDDIR%/dirhtml.
88	goto end
89	)
90
91	if "%1" == "singlehtml" (
92	%SPHINXBUILD% -b singlehtml %ALLSPHINXOPTS% %BUILDDIR%/singlehtml
93	if errorlevel 1 exit /b 1
94	echo.
95	echo.Build finished. The HTML pages are in %BUILDDIR%/singlehtml.
96	goto end
97	)
98
99	if "%1" == "pickle" (
100	%SPHINXBUILD% -b pickle %ALLSPHINXOPTS% %BUILDDIR%/pickle
101	if errorlevel 1 exit /b 1
102	echo.
103	echo.Build finished; now you can process the pickle files.
104	goto end
105	)
106
107	if "%1" == "json" (
108	%SPHINXBUILD% -b json %ALLSPHINXOPTS% %BUILDDIR%/json
109	if errorlevel 1 exit /b 1
110	echo.
111	echo.Build finished; now you can process the JSON files.
112	goto end
113	)
114
115	if "%1" == "htmlhelp" (
116	%SPHINXBUILD% -b htmlhelp %ALLSPHINXOPTS% %BUILDDIR%/htmlhelp
117	if errorlevel 1 exit /b 1
118	echo.
119	echo.Build finished; now you can run HTML Help Workshop with the ^
120	.hhp project file in %BUILDDIR%/htmlhelp.
121	goto end
122	)
123
124	if "%1" == "qthelp" (
125	%SPHINXBUILD% -b qthelp %ALLSPHINXOPTS% %BUILDDIR%/qthelp
126	if errorlevel 1 exit /b 1
127	echo.
128	echo.Build finished; now you can run "qcollectiongenerator" with the ^
129	.qhcp project file in %BUILDDIR%/qthelp, like this:
130	echo.^> qcollectiongenerator %BUILDDIR%\qthelp\IdrisManual.qhcp
131	echo.To view the help file:
132	echo.^> assistant -collectionFile %BUILDDIR%\qthelp\IdrisManual.ghc
133	goto end
134	)
135
136	if "%1" == "devhelp" (
137	%SPHINXBUILD% -b devhelp %ALLSPHINXOPTS% %BUILDDIR%/devhelp
138	if errorlevel 1 exit /b 1
139	echo.
140	echo.Build finished.
141	goto end
142	)
143
144	if "%1" == "epub" (
145	%SPHINXBUILD% -b epub %ALLSPHINXOPTS% %BUILDDIR%/epub
146	if errorlevel 1 exit /b 1
147	echo.
148	echo.Build finished. The epub file is in %BUILDDIR%/epub.
149	goto end
150	)
151
152	if "%1" == "latex" (
153	%SPHINXBUILD% -b latex %ALLSPHINXOPTS% %BUILDDIR%/latex
154	if errorlevel 1 exit /b 1
155	echo.
156	echo.Build finished; the LaTeX files are in %BUILDDIR%/latex.
157	goto end
158	)
159
160	if "%1" == "latexpdf" (
161	%SPHINXBUILD% -b latex %ALLSPHINXOPTS% %BUILDDIR%/latex
162	cd %BUILDDIR%/latex
163	make all-pdf
164	cd %~dp0
165	echo.
166	echo.Build finished; the PDF files are in %BUILDDIR%/latex.
167	goto end
168	)
169
170	if "%1" == "latexpdfja" (
171	%SPHINXBUILD% -b latex %ALLSPHINXOPTS% %BUILDDIR%/latex
172	cd %BUILDDIR%/latex
173	make all-pdf-ja
174	cd %~dp0
175	echo.
176	echo.Build finished; the PDF files are in %BUILDDIR%/latex.
177	goto end
178	)
179
180	if "%1" == "text" (
181	%SPHINXBUILD% -b text %ALLSPHINXOPTS% %BUILDDIR%/text
182	if errorlevel 1 exit /b 1
183	echo.
184	echo.Build finished. The text files are in %BUILDDIR%/text.
185	goto end
186	)
187
188	if "%1" == "man" (
189	%SPHINXBUILD% -b man %ALLSPHINXOPTS% %BUILDDIR%/man
190	if errorlevel 1 exit /b 1
191	echo.
192	echo.Build finished. The manual pages are in %BUILDDIR%/man.
193	goto end
194	)
195
196	if "%1" == "texinfo" (
197	%SPHINXBUILD% -b texinfo %ALLSPHINXOPTS% %BUILDDIR%/texinfo
198	if errorlevel 1 exit /b 1
199	echo.
200	echo.Build finished. The Texinfo files are in %BUILDDIR%/texinfo.
201	goto end
202	)
203
204	if "%1" == "gettext" (
205	%SPHINXBUILD% -b gettext %I18NSPHINXOPTS% %BUILDDIR%/locale
206	if errorlevel 1 exit /b 1
207	echo.
208	echo.Build finished. The message catalogs are in %BUILDDIR%/locale.
209	goto end
210	)
211
212	if "%1" == "changes" (
213	%SPHINXBUILD% -b changes %ALLSPHINXOPTS% %BUILDDIR%/changes
214	if errorlevel 1 exit /b 1
215	echo.
216	echo.The overview file is in %BUILDDIR%/changes.
217	goto end
218	)
219
220	if "%1" == "linkcheck" (
221	%SPHINXBUILD% -b linkcheck %ALLSPHINXOPTS% %BUILDDIR%/linkcheck
222	if errorlevel 1 exit /b 1
223	echo.
224	echo.Link check complete; look for any errors in the above output ^
225	or in %BUILDDIR%/linkcheck/output.txt.
226	goto end
227	)
228
229	if "%1" == "doctest" (
230	%SPHINXBUILD% -b doctest %ALLSPHINXOPTS% %BUILDDIR%/doctest
231	if errorlevel 1 exit /b 1
232	echo.
233	echo.Testing of doctests in the sources finished, look at the ^
234	results in %BUILDDIR%/doctest/output.txt.
235	goto end
236	)
237
238	if "%1" == "coverage" (
239	%SPHINXBUILD% -b coverage %ALLSPHINXOPTS% %BUILDDIR%/coverage
240	if errorlevel 1 exit /b 1
241	echo.
242	echo.Testing of coverage in the sources finished, look at the ^
243	results in %BUILDDIR%/coverage/python.txt.
244	goto end
245	)
246
247	if "%1" == "xml" (
248	%SPHINXBUILD% -b xml %ALLSPHINXOPTS% %BUILDDIR%/xml
249	if errorlevel 1 exit /b 1
250	echo.
251	echo.Build finished. The XML files are in %BUILDDIR%/xml.
252	goto end
253	)
254
255	if "%1" == "pseudoxml" (
256	%SPHINXBUILD% -b pseudoxml %ALLSPHINXOPTS% %BUILDDIR%/pseudoxml
257	if errorlevel 1 exit /b 1
258	echo.
259	echo.Build finished. The pseudo-XML files are in %BUILDDIR%/pseudoxml.
260	goto end
261	)
262
263	:end

docs/source/app/index.rstrenamed from docs/app/index.rst+1−1

@@ -1,4 +1,4 @@
1	.. _proofs-index:	1	.. _app-index:
2		2
3	################################	3	################################
4	Structuring Idris 2 Applications	4	Structuring Idris 2 Applications

docs/source/backends/chez.rstrenamed from docs/backends/chez.rst+0−0

File renamed without changes.

docs/source/backends/index.rstrenamed from docs/backends/index.rst+0−0

File renamed without changes.

docs/source/backends/racket.rstrenamed from docs/backends/racket.rst+0−0

File renamed without changes.

docs/source/conf.pyrenamed from docs/conf.py+40−173

@@ -1,32 +1,42 @@
1	# -- coding: utf-8 --	1	# Configuration file for the Sphinx documentation builder.
2	#	2	#
3	# Idris Manual documentation build configuration file, created by	3	# Idris Manual documentation build configuration file, created by
4	# sphinx-quickstart on Sat Feb 28 20:41:47 2015.	4	# sphinx-quickstart on Apr 13, 2020.
5	#	5	#
6	# This file is execfile()d with the current directory set to its	6	# This file is execfile()d with the current directory set to its
7	# containing dir.	7	# containing dir.
8	#	8	#
9	# Note that not all possible configuration values are present in this	9	# This file only contains a selection of the most common options. For a full
10	# autogenerated file.	10	# list see the documentation:
11	#	11	# https://www.sphinx-doc.org/en/master/usage/configuration.html
12	# All configuration values have a default; values that are commented out
13	# serve to show the default.
14
15	import sys
16	import os
17		12
18	# True if the readthedocs theme is locally installed	13	# -- Path setup --------------------------------------------------------------
19	on_rtd = os.environ.get('READTHEDOCS', None) == 'True'
20		14
21	# If extensions (or modules to document with autodoc) are in another directory,	15	# If extensions (or modules to document with autodoc) are in another directory,
22	# add these directories to sys.path here. If the directory is relative to the	16	# add these directories to sys.path here. If the directory is relative to the
23	# documentation root, use os.path.abspath to make it absolute, like shown here.	17	# documentation root, use os.path.abspath to make it absolute, like shown here.
24	#sys.path.insert(0, os.path.abspath('.'))	18	#
		19	import os
		20	import sys
		21	import sphinx_rtd_theme
		22	# sys.path.insert(0, os.path.abspath('.'))
		23
		24
		25	# -- Project information -----------------------------------------------------
		26
		27	# General information about the project.
		28	project = 'Idris2'
		29	copyright = '2020, The Idris Community'
		30	author = 'The Idris Community'
		31
		32	# The short X.Y version.
		33	version = '0.0'
		34
		35	# The full version, including alpha/beta/rc tags
		36	release = '0.0'
25		37
26	# -- General configuration ------------------------------------------------
27		38
28	# If your documentation needs a minimal Sphinx version, state it here.	39	# -- General configuration ---------------------------------------------------
29	#needs_sphinx = '1.0'
30		40
31	# Add any Sphinx extension module names here, as strings. They can be	41	# Add any Sphinx extension module names here, as strings. They can be
32	# extensions coming with Sphinx (named 'sphinx.ext.*') or your custom	42	# extensions coming with Sphinx (named 'sphinx.ext.*') or your custom
@@ -35,183 +45,40 @@ extensions = [ · 2 unmodified lines
35	'sphinx.ext.todo',	45	'sphinx.ext.todo',
36	# 'sphinx.ext.pngmath', # imgmath is not supported on readthedocs.	46	# 'sphinx.ext.pngmath', # imgmath is not supported on readthedocs.
37	'sphinx.ext.ifconfig',	47	'sphinx.ext.ifconfig',
38	'recommonmark'	48	"sphinx_rtd_theme",
39	]	49	]
40		50
41	# Add any paths that contain templates here, relative to this directory.	51	# Add any paths that contain templates here, relative to this directory.
42	templates_path = ['_templates']	52	templates_path = ['_templates']
43		53
44	# The suffix of source filenames.
45	source_suffix = ['.rst','.md']
46
47	# The encoding of source files.
48	#source_encoding = 'utf-8-sig'
49
50	# The master toctree document.
51	master_doc = 'index'
52
53	# General information about the project.
54	project = u'Idris2'
55	copyright = u'2019, The Idris Community'
56	author = u'The Idris Community'
57
58	# The version info for the project you're documenting, acts as replacement for
59	# \|version\| and \|release\|, also used in various other places throughout the
60	# built documents.
61	#
62	# The short X.Y version.
63	version = '0.0'
64	# The full version, including alpha/beta/rc tags.
65	release = '0.0'
66
67	# The language for content autogenerated by Sphinx. Refer to documentation
68	# for a list of supported languages.
69	#
70	# This is also used if you do content translation via gettext catalogs.
71	# Usually you set "language" from the command line for these cases.
72	language = None
73
74	# There are two options for replacing \|today\|: either, you set today to some
75	# non-false value, then it is used:
76	#today = ''
77	# Else, today_fmt is used as the format for a strftime call.
78	#today_fmt = '%B %d, %Y'
79
80	# List of patterns, relative to source directory, that match files and	54	# List of patterns, relative to source directory, that match files and
81	# directories to ignore when looking for source files.	55	# directories to ignore when looking for source files.
82	exclude_patterns = ['_build']	56	# This pattern also affects html_static_path and html_extra_path.
83		57	exclude_patterns = []
84	# The reST default role (used for this markup: `text`) to use for all
85	# documents.
86	#default_role = None
87		58
88	# If true, '()' will be appended to :func: etc. cross-reference text.
89	#add_function_parentheses = True
90		59
91	# If true, the current module name will be prepended to all description	60	# -- Options for HTML output -------------------------------------------------
92	# unit titles (such as .. function::).
93	#add_module_names = True
94		61
95	# If true, sectionauthor and moduleauthor directives will be shown in the	62	# The master toctree document.
96	# output. They are ignored by default.	63	master_doc = 'index'
97	#show_authors = False
98
99	# The name of the Pygments (syntax highlighting) style to use.
100	pygments_style = 'sphinx'
101
102	# A list of ignored prefixes for module index sorting.
103	#modindex_common_prefix = []
104
105	# If true, keep warnings as "system message" paragraphs in the built documents.
106	#keep_warnings = False
107
108	# If true, `todo` and `todoList` produce output, else they produce nothing.
109	todo_include_todos = True
110
111
112	# -- Options for HTML output ----------------------------------------------
113		64
114	# The theme to use for HTML and HTML Help pages. See the documentation for	65	# The theme to use for HTML and HTML Help pages. See the documentation for
115	# a list of builtin themes.	66	# a list of builtin themes.
116	html_theme = "default"	67	# # Read The Docs Themes specific settings
117		68	html_theme = 'sphinx_rtd_theme'
118	if not on_rtd: # only import and set the theme if we're building docs locally	69	html_theme_options = {
119	try:	70	'display_version': True,
120	import sphinx_rtd_theme	71	'prev_next_buttons_location': 'bottom'
121	html_theme = 'sphinx_rtd_theme'	72	}
122	html_theme_path = [sphinx_rtd_theme.get_html_theme_path()]
123	except ImportError:
124	html_theme = "default"
125
126	# Theme options are theme-specific and customize the look and feel of a theme
127	# further. For a list of options available for each theme, see the
128	# documentation.
129	#html_theme_options = {}
130
131	# Add any paths that contain custom themes here, relative to this directory.
132	#html_theme_path = []
133
134	# The name for this set of Sphinx documents. If None, it defaults to
135	# "<project> v<release> documentation".
136	#html_title = None
137		73
138	# A shorter title for the navigation bar. Default is the same as html_title.
139	#html_short_title = None
140		74
141	# The name of an image file (relative to this directory) to place at the top
142	# of the sidebar.
143	#html_logo = None
144		75
145	# The name of an image file (within the static path) to use as favicon of the
146	# docs. This file should be a Windows icon file (.ico) being 16x16 or 32x32
147	# pixels large.
148	#html_favicon = None
149		76
150	# Add any paths that contain custom static files (such as style sheets) here,	77	# Add any paths that contain custom static files (such as style sheets) here,
151	# relative to this directory. They are copied after the builtin static files,	78	# relative to this directory. They are copied after the builtin static files,
152	# so a file named "default.css" will overwrite the builtin "default.css".	79	# so a file named "default.css" will overwrite the builtin "default.css".
153	html_static_path = ['_static']	80	html_static_path = ['_static']
154		81
155	# Add any extra paths that contain custom files (such as robots.txt or
156	# .htaccess) here, relative to this directory. These files are copied
157	# directly to the root of the documentation.
158	#html_extra_path = []
159
160	# If not '', a 'Last updated on:' timestamp is inserted at every page bottom,
161	# using the given strftime format.
162	#html_last_updated_fmt = '%b %d, %Y'
163
164	# If true, SmartyPants will be used to convert quotes and dashes to
165	# typographically correct entities.
166	#html_use_smartypants = True
167
168	# Custom sidebar templates, maps document names to template names.
169	#html_sidebars = {}
170
171	# Additional templates that should be rendered to pages, maps page names to
172	# template names.
173	#html_additional_pages = {}
174
175	# If false, no module index is generated.
176	#html_domain_indices = True
177
178	# If false, no index is generated.
179	#html_use_index = True
180
181	# If true, the index is split into individual pages for each letter.
182	#html_split_index = False
183
184	# If true, links to the reST sources are added to the pages.
185	#html_show_sourcelink = True
186
187	# If true, "Created using Sphinx" is shown in the HTML footer. Default is True.
188	#html_show_sphinx = True
189
190	# If true, "(C) Copyright ..." is shown in the HTML footer. Default is True.
191	#html_show_copyright = True
192
193	# If true, an OpenSearch description file will be output, and all pages will
194	# contain a <link> tag referring to it. The value of this option must be the
195	# base URL from which the finished HTML is served.
196	#html_use_opensearch = ''
197
198	# This is the file name suffix for HTML files (e.g. ".xhtml").
199	#html_file_suffix = None
200
201	# Language to be used for generating the HTML full-text search index.
202	# Sphinx supports the following languages:
203	# 'da', 'de', 'en', 'es', 'fi', 'fr', 'hu', 'it', 'ja'
204	# 'nl', 'no', 'pt', 'ro', 'ru', 'sv', 'tr'
205	#html_search_language = 'en'
206
207	# A dictionary with options for the search language support, empty by default.
208	# Now only 'ja' uses this config value
209	#html_search_options = {'type': 'default'}
210
211	# The name of a javascript file (relative to the configuration directory) that
212	# implements a search results scorer. If empty, the default will be used.
213	#html_search_scorer = 'scorer.js'
214
215	# Output file base name for HTML help builder.	82	# Output file base name for HTML help builder.
216	htmlhelp_basename = 'IdrisManualdoc'	83	htmlhelp_basename = 'IdrisManualdoc'
217		84
@@ -305,7 +172,7 @@ latex_show_url = 'footnote' · 87 unmodified lines
305		172
306	# The name of an image file (relative to this directory) to place at the top of	173	# The name of an image file (relative to this directory) to place at the top of
307	# the title page.	174	# the title page.
308	latex_logo = '../icons/idris-512x512.png'	175	latex_logo = '../../icons/idris-512x512.png'
309		176
310	# For "manual" documents, if this is true, then toplevel headings are parts,	177	# For "manual" documents, if this is true, then toplevel headings are parts,
311	# not chapters.	178	# not chapters.

docs/source/faq/faq.rstrenamed from docs/faq/faq.rst+0−0

File renamed without changes.

docs/source/ffi/ffi.rstrenamed from docs/ffi/ffi.rst+0−0

File renamed without changes.

docs/source/ffi/index.rstrenamed from docs/ffi/index.rst+0−0

File renamed without changes.

docs/source/ffi/readline.rstrenamed from docs/ffi/readline.rst+0−0

File renamed without changes.

docs/source/index.rstrenamed from docs/index.rst+0−0

File renamed without changes.

docs/source/listing/idris-prompt-helloworld.txtrenamed from docs/listing/idris-prompt-helloworld.txt+0−0

File renamed without changes.

docs/source/listing/idris-prompt-interp.txtrenamed from docs/listing/idris-prompt-interp.txt+0−0

File renamed without changes.

docs/source/listing/idris-prompt-start.txtrenamed from docs/listing/idris-prompt-start.txt+0−0

File renamed without changes.

docs/source/proofs/definitional.rstrenamed from docs/proofs/definitional.rst+0−0

File renamed without changes.

docs/source/proofs/index.rstrenamed from docs/proofs/index.rst+0−0

File renamed without changes.

docs/source/proofs/inductive.rstrenamed from docs/proofs/inductive.rst+0−0

File renamed without changes.

docs/source/proofs/patterns.rstrenamed from docs/proofs/patterns.rst+0−0

File renamed without changes.

docs/source/proofs/pluscomm.rstrenamed from docs/proofs/pluscomm.rst+0−0

File renamed without changes.

docs/source/proofs/propositional.rstrenamed from docs/proofs/propositional.rst+0−0

File renamed without changes.

docs/source/reference/envvars.rstrenamed from docs/reference/envvars.rst+0−0

File renamed without changes.

docs/source/reference/index.rstrenamed from docs/reference/index.rst+0−0

File renamed without changes.

docs/source/reference/packages.rstrenamed from docs/reference/packages.rst+0−0

File renamed without changes.

docs/source/tutorial/conclusions.rstrenamed from docs/tutorial/conclusions.rst+16−14

docs/source/tutorial/index.rstrenamed from docs/tutorial/index.rst+0−0

File renamed without changes.

docs/source/tutorial/interactive.rstrenamed from docs/tutorial/interactive.rst+1−1

@@ -165,7 +165,7 @@ then ``:ps 96 vzipWith_rhs_1`` will give · 164 unmodified lines
165		165
166	.. code-block:: idris	166	.. code-block:: idris
167		167
168	[]	168	[]
169		169
170	This works because it is searching for a ``Vect`` of length 0, of	170	This works because it is searching for a ``Vect`` of length 0, of
171	which the empty vector is the only possibility. Similarly, and perhaps	171	which the empty vector is the only possibility. Similarly, and perhaps

docs/source/tutorial/interfaces.rstrenamed from docs/tutorial/interfaces.rst+11−9

     Main> :t Ord
     Prelude.Ord : Type -> Type
-So, ``(Ord a, Show a)`` is an ordinary pair of ``Type``s, with two constraints
+So, ``(Ord a, Show a)`` is an ordinary pair of ``Types``, with two constraints
 as the first and second element of the pair.
 Note: Interfaces and ``mutual`` blocks
 .. code-block:: idris
+    import Data.Strings
     readNumber : IO (Maybe Nat)
     readNumber = do
       input <- getLine
       if all isDigit (unpack input)
-         then pure (Just (cast input))
+         then pure (Just (stringToNatOrZ input))
          else pure Nothing
 If we then use it to write a function to read two numbers, returning
     readNumbers : IO (Maybe (Nat, Nat))
     readNumbers
       = do Just x_ok <- readNumber
                 | Nothing => pure Nothing
            Just y_ok <- readNumber
                 | Nothing => pure Nothing
            pure (Just (x_ok, y_ok))
 While ``do`` notation gives an alternative meaning to sequencing,
 idioms give an alternative meaning to *application*. The notation and
 larger example in this section is inspired by Conor McBride and Ross
-Paterson’s paper “Applicative Programming with Effects” [1]_.
+Paterson’s paper “Applicative Programming with Effects” [#ConorRoss]_.
 First, let us revisit ``m_add`` above. All it is really doing is
 applying an operator to two values extracted from ``Maybe Int``. We
         _        <*> _        = Nothing
 Using ``<*>`` we can use this implementation as follows, where a function
-application ``[| f a1 …an |]`` is translated into ``pure f <*> a1 <*>
+application ``[ f a1 …an |]`` is translated into ``pure f <*> a1 <*>
 … <*> an``:
 .. code-block:: idris
     m_add' : Maybe Int -> Maybe Int -> Maybe Int
-    m_add' x y = [| x + y |]
+    m_add' x y = [ x + y |]
 An error-handling interpreter
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 Idiom notation is commonly useful when defining evaluators. McBride
-and Paterson describe such an evaluator [1]_, for a language similar
+and Paterson describe such an evaluator [#ConorRoss]_, for a language similar
 to the following:
 .. code-block:: idris
 parameter used to find an implementation.
-.. [1] Conor McBride and Ross Paterson. 2008. Applicative programming
+.. [#ConorRoss] Conor McBride and Ross Paterson. 2008. Applicative programming
        with effects. J. Funct. Program. 18, 1 (January 2008),
        1-13. DOI=10.1017/S0956796807006326
        http://dx.doi.org/10.1017/S0956796807006326

docs/source/tutorial/interp.rstrenamed from docs/tutorial/interp.rst+0−0

File renamed without changes.

docs/source/tutorial/introduction.rstrenamed from docs/tutorial/introduction.rst+5−4

@@ -21,7 +21,7 @@ In a language with dependent types, however, the distinction is less · 20 unmodified lines
21	clear. Dependent types allow types to “depend” on values — in other	21	clear. Dependent types allow types to “depend” on values — in other
22	words, types are a first class language construct and can be	22	words, types are a first class language construct and can be
23	manipulated like any other value. The standard example is the type of	23	manipulated like any other value. The standard example is the type of
24	lists of a given length [1]_, ``Vect n a``, where ``a`` is the element	24	lists of a given length [#fn1]_, ``Vect n a``, where ``a`` is the element
25	type and ``n`` is the length of the list and can be an arbitrary term.	25	type and ``n`` is the length of the list and can be an arbitrary term.
26		26
27	When types can contain values, and where those values describe	27	When types can contain values, and where those values describe
@@ -69,6 +69,7 @@ so that you can try them out easily. They can be found under · 41 unmodified lines
69	``samples``. It is, however, strongly recommended that you type	69	``samples``. It is, however, strongly recommended that you type
70	them in yourself, rather than simply loading and reading them.	70	them in yourself, rather than simply loading and reading them.
71		71
72	.. [1]	72	.. rubric:: Footnotes
73	Typically, and perhaps confusingly, referred to in the dependently	73
74	typed programming literature as “vectors”	74	.. [#fn1] Typically, and perhaps confusingly, referred to in the dependently
		75	typed programming literature as "vectors".

docs/source/tutorial/miscellany.rstrenamed from docs/tutorial/miscellany.rst+3−3

 ==================
 We have already seen implicit arguments, which allows arguments to be
-omitted when they can be inferred by the type checker, e.g.
+omitted when they can be inferred by the type checker [#IdrisType]_, e.g.
 .. code-block:: idris
 begins with a greater than sign ``>``, for example:
 .. code-block:: literate-idris
+   :force:
     > module literate
 hierarchy — ``myid``\ ’s first argument is a ``Type``, which cannot be
 at a lower level than required if it is applied to itself.
-.. [1]
+.. [#IdrisType] https://github.com/david-christiansen/idris-type-providers
-   https://github.com/david-christiansen/idris-type-providers

docs/source/tutorial/modules.rstrenamed from docs/tutorial/modules.rst+1−0

@@ -148,6 +148,7 @@ Additionally, a module can re-export a module it has imported, by using · 147 unmodified lines
148	the ``public`` modifier on an ``import``. For example:	148	the ``public`` modifier on an ``import``. For example:
149		149
150	.. code-block:: idris	150	.. code-block:: idris
		151	:force:
151		152
152	module A	153	module A
153		154

docs/source/tutorial/multiplicities.rstrenamed from docs/tutorial/multiplicities.rst+1−1

@@ -423,7 +423,7 @@ unrestricted multiplicity · 422 unmodified lines
423	.. code-block:: idris	423	.. code-block:: idris
424		424
425	sumLengths : {m, n : _} -> Vect m a -> Vect n a —> Nat	425	sumLengths : {m, n : _} -> Vect m a -> Vect n a —> Nat
426	sumLengths xs ys = vLen xs + vLen xs	426	sumLengths xs ys = vlen xs + vlen xs
427		427
428	Remember that giving no multiplicity on a binder, as with ``m`` and ``n`` here,	428	Remember that giving no multiplicity on a binder, as with ``m`` and ``n`` here,
429	means that the variable has unrestricted usage.	429	means that the variable has unrestricted usage.

docs/source/tutorial/packages.rstrenamed from docs/tutorial/packages.rst+0−0

File renamed without changes.

docs/source/tutorial/starting.rstrenamed from docs/tutorial/starting.rst+0−0

File renamed without changes.

docs/source/tutorial/theorems.rstrenamed from docs/tutorial/theorems.rst+2−2

@@ -97,7 +97,7 @@ real distinction between proofs and programs. A proof, as far as we are · 96 unmodified lines
97	concerned here, is merely a program with a precise enough type to	97	concerned here, is merely a program with a precise enough type to
98	guarantee a particular property of interest.	98	guarantee a particular property of interest.
99		99
100	We won’t go into details here, but the Curry-Howard correspondence [1]_	100	We won’t go into details here, but the Curry-Howard correspondence [#Timothy]_
101	explains this relationship. The proof itself is immediate, because	101	explains this relationship. The proof itself is immediate, because
102	``plus Z n`` normalises to ``n`` by the definition of ``plus``:	102	``plus Z n`` normalises to ``n`` by the definition of ``plus``:
103		103
@@ -450,7 +450,7 @@ example from a C library) where totality can be shown by an external · 346 unmodified lines
450	argument.	450	argument.
451		451
452		452
453	.. [1] Timothy G. Griffin. 1989. A formulae-as-type notion of	453	.. [#Timothy] Timothy G. Griffin. 1989. A formulae-as-type notion of
454	control. In Proceedings of the 17th ACM SIGPLAN-SIGACT	454	control. In Proceedings of the 17th ACM SIGPLAN-SIGACT
455	symposium on Principles of programming languages (POPL	455	symposium on Principles of programming languages (POPL
456	'90). ACM, New York, NY, USA, 47-58. DOI=10.1145/96709.96714	456	'90). ACM, New York, NY, USA, 47-58. DOI=10.1145/96709.96714

docs/source/tutorial/typesfuns.rstrenamed from docs/tutorial/typesfuns.rst+3−7

       odd : Nat -> Bool
       odd Z = False
       odd (S k) = even k
     test : List Nat
     test = [c (S 1), c Z, d (S Z)]
       where c : Nat -> Nat
             c x = 42 + x
             d : Nat -> Nat
             d y = c (y + 1 + z y)
                   where z : Nat -> Nat
 -  ``libs/base/Data/List.idr``
--  ``libs/base/Data/List.idr``
 -  ``libs/base/Data/Vect.idr``
--  ``libs/base/Data/VectType.idr``
 Functions include filtering, appending, reversing, and so on.
 Aside: Anonymous functions and operator sections
         fst : a
         snd : b
-Using the ``class`` record from earlier, the size of the class can be
+Using the ``Class`` record from earlier, the size of the class can be
 restricted using a ``Vect`` and the size included in the type by parameterising
 the record with the size.  For example:

docs/source/tutorial/views.rstrenamed from docs/tutorial/views.rst+2−2

@@ -31,7 +31,7 @@ The ``with`` rule — matching intermediate values · 30 unmodified lines
31		31
32	Very often, we need to match on the result of an intermediate	32	Very often, we need to match on the result of an intermediate
33	computation. Idris provides a construct for this, the ``with``	33	computation. Idris provides a construct for this, the ``with``
34	rule, inspired by views in ``Epigram`` [1]_, which takes account of	34	rule, inspired by views in ``Epigram`` [#McBridgeMcKinna]_, which takes account of
35	the fact that matching on a value in a dependently typed language can	35	the fact that matching on a value in a dependently typed language can
36	affect what we know about the forms of other values. In its simplest	36	affect what we know about the forms of other values. In its simplest
37	form, the ``with`` rule adds another argument to the function being	37	form, the ``with`` rule adds another argument to the function being
@@ -151,6 +151,6 @@ it is: · 113 unmodified lines
151	For full details on ``rewrite`` in particular, please refer to the theorem	151	For full details on ``rewrite`` in particular, please refer to the theorem
152	proving tutorial, in Section :ref:`proofs-index`.	152	proving tutorial, in Section :ref:`proofs-index`.
153		153
154	.. [1] Conor McBride and James McKinna. 2004. The view from the	154	.. [#McBridgeMcKinna] Conor McBride and James McKinna. 2004. The view from the
155	left. J. Funct. Program. 14, 1 (January 2004),	155	left. J. Funct. Program. 14, 1 (January 2004),
156	69-111. https://doi.org/10.1017/S0956796803004829	156	69-111. https://doi.org/10.1017/S0956796803004829

docs/source/typedd/typedd.rstrenamed from docs/typedd/typedd.rst+0−0

File renamed without changes.

docs/source/updates/updates.rstrenamed from docs/updates/updates.rst+2−2

@@ -140,7 +140,7 @@ unrestricted multiplicity · 139 unmodified lines
140	.. code-block:: idris	140	.. code-block:: idris
141		141
142	sumLengths : {m, n : _} -> Vect m a -> Vect n a —> Nat	142	sumLengths : {m, n : _} -> Vect m a -> Vect n a —> Nat
143	sumLengths xs ys = vLen xs + vLen xs	143	sumLengths xs ys = vlen xs + vlen xs
144		144
145	Remember that giving no multiplicity on a binder, as with ``m`` and ``n`` here,	145	Remember that giving no multiplicity on a binder, as with ``m`` and ``n`` here,
146	means that the variable has unrestricted usage.	146	means that the variable has unrestricted usage.
@@ -263,7 +263,7 @@ Idris 1, it won't attempt significant backtracking. If you have deeply nested · 116 unmodified lines
263	ambiguous names (beyond a small threshold, default 3) Idris 2 will report an	263	ambiguous names (beyond a small threshold, default 3) Idris 2 will report an
264	error. You can change this threshold with a directive, for example:	264	error. You can change this threshold with a directive, for example:
265		265
266	.. code_block:: idris	266	.. code-block:: idris
267		267
268	%ambiguity_depth 10	268	%ambiguity_depth 10
269		269

idris2.ipkg+1−0

@@ -4,6 +4,7 @@ modules = · 3 unmodified lines
4	Compiler.Common,	4	Compiler.Common,
5	Compiler.CompileExpr,	5	Compiler.CompileExpr,
6	Compiler.Inline,	6	Compiler.Inline,
		7	Compiler.LambdaLift,
7	Compiler.Scheme.Chez,	8	Compiler.Scheme.Chez,
8	-- Compiler.Scheme.Chicken,	9	-- Compiler.Scheme.Chicken,
9	Compiler.Scheme.Racket,	10	Compiler.Scheme.Racket,

libs/network/Network/Socket/Raw.idr+12−0

 -- ---------------------------------------------------------- [ Socket Utilies ]
+||| Put a value in a buffer
+export
+sock_poke : BufPtr -> Int -> Int -> IO ()
+sock_poke (BPtr ptr) offset val = cCall () "idrnet_poke" [ptr, offset, val]
+||| Take a value from a buffer
+export
+sock_peek : BufPtr -> Int -> IO Int
+sock_peek (BPtr ptr) offset = cCall Int "idrnet_peek" [ptr, offset]
 ||| Frees a given pointer
+export
 sock_free : BufPtr -> IO ()
 sock_free (BPtr ptr) = cCall () "idrnet_free" [ptr]
 ||| Allocates an amount of memory given by the ByteLength parameter.
 |||
 ||| Used to allocate a mutable pointer to be given to the Recv functions.
+export
 sock_alloc : ByteLength -> IO BufPtr
 sock_alloc bl = map BPtr $ cCall AnyPtr "idrnet_malloc" [bl]

libs/network/idris_net.c+10−0

@@ -56,6 +56,16 @@ void idrnet_free(void* ptr) { · 55 unmodified lines
56	free(ptr);	56	free(ptr);
57	}	57	}
58		58
		59	unsigned int idrnet_peek(void *ptr, unsigned int offset) {
		60	unsigned char buf_c = (unsigned char) ptr;
		61	return (unsigned int) buf_c[offset];
		62	}
		63
		64	void idrnet_poke(void *ptr, unsigned int offset, char val) {
		65	char buf_c = (char)ptr;
		66	buf_c[offset] = val;
		67	}
		68
59		69
60	int idrnet_socket(int domain, int type, int protocol) {	70	int idrnet_socket(int domain, int type, int protocol) {
61	#ifdef _WIN32	71	#ifdef _WIN32

libs/network/idris_net.h+2−0

@@ -31,6 +31,8 @@ typedef struct idrnet_recvfrom_result { · 30 unmodified lines
31	// Memory management functions	31	// Memory management functions
32	void* idrnet_malloc(int size);	32	void* idrnet_malloc(int size);
33	void idrnet_free(void* ptr);	33	void idrnet_free(void* ptr);
		34	unsigned int idrnet_peek(void *ptr, unsigned int offset);
		35	void idrnet_poke(void *ptr, unsigned int offset, char val);
34		36
35	// Gets value of errno	37	// Gets value of errno
36	int idrnet_errno();	38	int idrnet_errno();

libs/network/test.c+15−0

@@ -31,10 +31,25 @@ void test_sockaddr_port_returns_explicitly_assigned_port() { · 30 unmodified lines
31	close(sock);	31	close(sock);
32	}	32	}
33		33
		34	void test_peek_and_poke_buffer() {
		35	void *buf = idrnet_malloc(100);
		36	assert(buf > 0);
		37
		38	for (int i = 0; i < 100; i++) {
		39	idrnet_poke(buf,i,7*i);
		40	}
		41
		42	for(int i = 0; i < 100; i++) {
		43	assert (idrnet_peek(buf,i) == (0xff & 7*i));
		44	}
		45	idrnet_free(buf);
		46	}
		47
34		48
35	int main(int argc, char**argv) {	49	int main(int argc, char**argv) {
36	test_sockaddr_port_returns_explicitly_assigned_port();	50	test_sockaddr_port_returns_explicitly_assigned_port();
37	test_sockaddr_port_returns_random_port_when_bind_port_is_0();	51	test_sockaddr_port_returns_random_port_when_bind_port_is_0();
		52	test_peek_and_poke_buffer();
38		53
39	printf("network library tests SUCCESS\n");	54	printf("network library tests SUCCESS\n");
40	return 0;	55	return 0;

libs/prelude/Prelude.idr+1−0

@@ -364,6 +364,7 @@ Integral Integer where · 363 unmodified lines
364	-- all other possibilities fail. I don't plan to provide a nicer syntax for	364	-- all other possibilities fail. I don't plan to provide a nicer syntax for
365	-- this...	365	-- this...
366	%defaulthint	366	%defaulthint
		367	%inline
367	public export	368	public export
368	defaultInteger : Num Integer	369	defaultInteger : Num Integer
369	defaultInteger = %search	370	defaultInteger = %search

src/Compiler/Common.idr+52−14

 import Compiler.CompileExpr
 import Compiler.Inline
+import Compiler.LambdaLift
 import Core.Context
 import Core.Directory
     build b (x :: xs) = do addToStringBuffer b x
                            build b xs
-dumpCases : {auto c : Ref Ctxt Defs} ->
+dumpCases : Defs -> String -> List Name ->
-            String -> List Name ->
             Core ()
-dumpCases fn cns
+dumpCases defs fn cns
-    = do defs <- get Ctxt
+    = do cstrs <- traverse dumpCase cns
-         cstrs <- traverse (dumpCase defs) cns
          Right () <- coreLift $ writeFile fn (fastAppend cstrs)
                | Left err => throw (FileErr fn err)
          pure ()
     fullShow (DN _ n) = show n
     fullShow n = show n
-    dumpCase : Defs -> Name -> Core String
+    dumpCase : Name -> Core String
-    dumpCase defs n
+    dumpCase n
         = case !(lookupCtxtExact n (gamma defs)) of
                Nothing => pure ""
                Just d =>
-                    case compexpr d of
+                    case namedcompexpr d of
                          Nothing => pure ""
                          Just def => pure (fullShow n ++ " = " ++ show def ++ "\n")
+dumpLifted : String -> List (Name, LiftedDef) -> Core ()
+dumpLifted fn lns
+    = do let cstrs = map dumpDef lns
+         Right () <- coreLift $ writeFile fn (fastAppend cstrs)
+               | Left err => throw (FileErr fn err)
+         pure ()
+  where
+    fullShow : Name -> String
+    fullShow (DN _ n) = show n
+    fullShow n = show n
+    dumpDef : (Name, LiftedDef) -> String
+    dumpDef (n, d) = fullShow n ++ " = " ++ show d ++ "\n"
+public export
+record CompileData where
+  constructor MkCompileData
+  allNames : List Name -- names which need to be compiled
+  nameTags : NameTags -- a mapping from type names to constructor tags
+  mainExpr : CExp [] -- main expression to execute
+  lambdaLifted : List (Name, LiftedDef)
+       -- ^ lambda lifted definitions, if required. Only the top level names
+       -- will be in the context, and (for the moment...) I don't expect to
+       -- need to look anything up, so it's just an alist.
 -- Find all the names which need compiling, from a given expression, and compile
--- them to CExp form (and update that in the Defs)
+-- them to CExp form (and update that in the Defs).
+-- Return the names, the type tags, and a compiled version of the expression
 export
-findUsedNames : {auto c : Ref Ctxt Defs} ->
+getCompileData : {auto c : Ref Ctxt Defs} ->
-                Term vars -> Core (List Name, NameTags)
+                 ClosedTerm -> Core CompileData
-findUsedNames tm
+getCompileData tm
     = do defs <- get Ctxt
          sopts <- getSession
          let ns = getRefs (Resolved (-1)) tm
          logTime ("Compile defs " ++ show (length cns) ++ "/" ++ show asize) $
            traverse_ (compileDef tycontags) cns
          logTime "Inline" $ traverse_ inlineDef cns
+         logTime "Merge lambda" $ traverse_ mergeLamDef cns
+         logTime "Fix arity" $ traverse_ fixArityDef cns
+         logTime "Forget names" $ traverse_ mkForgetDef cns
+         lifted <- logTime "Lambda lift" $ traverse lambdaLift cns
+         compiledtm <- fixArityExp !(compileExp tycontags tm)
+         defs <- get Ctxt
          maybe (pure ())
                (\f => do coreLift $ putStrLn $ "Dumping case trees to " ++ f
-                         dumpCases f cns)
+                         dumpCases defs f cns)
                (dumpcases sopts)
-         pure (cns, tycontags)
+         maybe (pure ())
+               (\f => do coreLift $ putStrLn $ "Dumping lambda lifted defs to " ++ f
+                         dumpLifted f (concat lifted))
+               (dumplifted sopts)
+         pure (MkCompileData cns tycontags compiledtm (concat lifted))
   where
     primTags : Int -> NameTags -> List Constant -> NameTags
     primTags t tags [] = tags

src/Compiler/CompileExpr.idr+103−29

 data Args
     = NewTypeBy Nat Nat
+    | EraseArgs Nat (List Nat)
     | Arity Nat
 ||| Extract the number of arguments from a term, or return that it's
 numArgs : Defs -> Term vars -> Core Args
 numArgs defs (Ref _ (TyCon tag arity) n) = pure (Arity arity)
 numArgs defs (Ref _ _ n)
-    = case !(lookupDefExact n (gamma defs)) of
+    = do Just gdef <- lookupCtxtExact n (gamma defs)
-           Just (DCon _ arity Nothing) => pure (Arity arity)
+              | Nothing => pure (Arity 0)
-           Just (DCon _ arity (Just pos)) => pure (NewTypeBy arity pos)
+         case definition gdef of
-           Just (PMDef _ args _ _ _) => pure (Arity (length args))
+           DCon _ arity Nothing => pure (EraseArgs arity (eraseArgs gdef))
-           Just (ExternDef arity) => pure (Arity arity)
+           DCon _ arity (Just (_, pos)) => pure (NewTypeBy arity pos)
-           Just (ForeignDef arity _) => pure (Arity arity)
+           PMDef _ args _ _ _ => pure (Arity (length args))
-           Just (Builtin {arity} f) => pure (Arity arity)
+           ExternDef arity => pure (Arity arity)
+           ForeignDef arity _ => pure (Arity arity)
+           Builtin {arity} f => pure (Arity arity)
            _ => pure (Arity 0)
 numArgs _ tm = pure (Arity 0)
              (etaExpand (i + 1) k (weaken exp)
                   (MkVar First :: map weakenVar args))
+export
 expandToArity : Nat -> CExp vars -> List (CExp vars) -> CExp vars
 -- No point in applying to anything
 expandToArity _ (CErased fc) _ = CErased fc
     keepArg (CCon fc _ _ args) = keep 0 args
     keepArg tm = CErased (getFC fn)
+dropPos : List Nat -> CExp vs -> CExp vs
+dropPos epos (CLam fc x sc) = CLam fc x (dropPos epos sc)
+dropPos epos (CCon fc c a args) = CCon fc c a (drop 0 args)
+  where
+    drop : Nat -> List (CExp vs) -> List (CExp vs)
+    drop i [] = []
+    drop i (x :: xs)
+        = if i `elem` epos
+             then drop (1 + i) xs
+             else x :: drop (1 + i) xs
+dropPos epos tm = tm
+eraseConArgs : Nat -> List Nat -> CExp vars -> List (CExp vars) -> CExp vars
+eraseConArgs arity epos fn args
+    = let fn' = expandToArity arity fn args in
+          dropPos epos fn' -- fn' might be lambdas, after eta expansion
+mkDropSubst : Nat -> List Nat ->
+              (rest : List Name) ->
+              (vars : List Name) ->
+              (vars' ** SubVars (vars' ++ rest) (vars ++ rest))
+mkDropSubst i es rest [] = ([] ** SubRefl)
+mkDropSubst i es rest (x :: xs)
+    = let (vs ** sub) = mkDropSubst (1 + i) es rest xs in
+          if i `elem` es
+             then (vs ** DropCons sub)
+             else (x :: vs ** KeepCons sub)
 -- Rewrite applications of Nat constructors and functions to more optimal
 -- versions using Integer
 trySBranch : CExp vars -> CConAlt vars -> Maybe (CExp vars)
 trySBranch n (MkConAlt (NS ["Prelude"] (UN "S")) _ [arg] sc)
     = let fc = getFC n in
-          Just (CLet fc arg (CApp fc (CRef fc (UN "prim__sub_Integer"))
+          Just (CLet fc arg True (CApp fc (CRef fc (UN "prim__sub_Integer"))
                     [n, CPrimVal fc (BI 1)]) sc)
 trySBranch _ _ = Nothing
   toCExpTm tags n (Bind fc x (Let Rig0 val _) sc)
       = pure $ shrinkCExp (DropCons SubRefl) !(toCExp tags n sc)
   toCExpTm tags n (Bind fc x (Let _ val _) sc)
-      = pure $ CLet fc x !(toCExp tags n val) !(toCExp tags n sc)
+      = pure $ CLet fc x True !(toCExp tags n val) !(toCExp tags n sc)
   toCExpTm tags n (Bind fc x (Pi c e ty) sc)
       = pure $ CCon fc (UN "->") 1 [!(toCExp tags n ty),
                                     CLam fc x !(toCExp tags n sc)]
                       | NewTypeBy arity pos =>
                             do let res = applyNewType arity pos !(toCExpTm tags n f) args'
                                pure $ natHack res
+                      | EraseArgs arity epos =>
+                            do let res = eraseConArgs arity epos !(toCExpTm tags n f) args'
+                               pure $ natHack res
                    let res = expandToArity a !(toCExpTm tags n f) args'
                    pure $ natHack res
 mutual
-  -- In the below, treat %World, and newtypes, as default cases
   conCases : {auto c : Ref Ctxt Defs} ->
              NameTags -> Name -> List (CaseAlt vars) ->
              Core (List (CConAlt vars))
   conCases tags n [] = pure []
-  conCases tags n (ConCase x tag args sc :: ns)
+  conCases {vars} tags n (ConCase x tag args sc :: ns)
       = do defs <- get Ctxt
-           case !(lookupDefExact x (gamma defs)) of
+           Just gdef <- lookupCtxtExact x (gamma defs)
-                Just (DCon _ arity (Just pos)) => conCases tags n ns -- skip it
+                | Nothing => -- primitive type match
-                _ => do let tag' = case lookup x tags of
+                     do xn <- getFullName x
+                        let tag' = case lookup x tags of
                                         Just t => t
                                         _ => tag
-                        xn <- getFullName x
                         pure $ MkConAlt xn tag' args !(toCExpTree tags n sc)
                                   :: !(conCases tags n ns)
+           case (definition gdef) of
+                DCon _ arity (Just pos) => conCases tags n ns -- skip it
+                _ => do xn <- getFullName x
+                        let (args' ** sub)
+                            = mkDropSubst 0 (eraseArgs gdef) vars args
+                        let tag' = case lookup x tags of
+                                        Just t => t
+                                        _ => tag
+                        pure $ MkConAlt xn tag' args'
+                                    (shrinkCExp sub !(toCExpTree tags n sc))
+                                  :: !(conCases tags n ns)
   conCases tags n (_ :: ns) = conCases tags n ns
   constCases : {auto c : Ref Ctxt Defs} ->
   getDef : {auto c : Ref Ctxt Defs} ->
            FC -> CExp vars ->
            NameTags -> Name -> List (CaseAlt vars) ->
-           Core (Maybe (CExp vars))
+           Core (Bool, Maybe (CExp vars))
-  getDef fc scr tags n [] = pure Nothing
+  getDef fc scr tags n [] = pure (False, Nothing)
   getDef fc scr tags n (DefaultCase sc :: ns)
-      = pure $ Just !(toCExpTree tags n sc)
+      = pure $ (False, Just !(toCExpTree tags n sc))
   getDef fc scr tags n (ConstCase WorldVal sc :: ns)
-      = pure $ Just !(toCExpTree tags n sc)
+      = pure $ (False, Just !(toCExpTree tags n sc))
   getDef {vars} fc scr tags n (ConCase x tag args sc :: ns)
       = do defs <- get Ctxt
            case !(lookupDefExact x (gamma defs)) of
-                Just (DCon _ arity (Just pos)) =>
+                -- If the flag is False, we still take the
+                -- default, but need to evaluate the scrutinee of the
+                -- case anyway - if the data structure contains a %World,
+                -- that we've erased, it means it has interacted with the
+                -- outside world, so we need to evaluate to keep the
+                -- side effect.
+                Just (DCon _ arity (Just (noworld, pos))) =>
                      let env : SubstCEnv args vars = mkSubst 0 pos args in
-                         pure $ Just (substs env !(toCExpTree tags n sc))
+                         pure $ (not noworld,
+                                 Just (substs env !(toCExpTree tags n sc)))
                 _ => getDef fc scr tags n ns
     where
       mkSubst : Nat -> Nat -> (args : List Name) -> SubstCEnv args vars
   toCExpTree tags n alts@(Case _ x scTy (DelayCase ty arg sc :: rest))
       = let fc = getLoc scTy in
             pure $
-              CLet fc arg (CForce fc (CLocal (getLoc scTy) x)) $
+              CLet fc arg True (CForce fc (CLocal (getLoc scTy) x)) $
-              CLet fc ty (CErased fc)
+              CLet fc ty True (CErased fc)
                    !(toCExpTree tags n sc)
   toCExpTree tags n alts = toCExpTree' tags n alts
       = let fc = getLoc scTy in
             do defs <- get Ctxt
                cases <- conCases tags n alts
-               def <- getDef fc (CLocal fc x) tags n alts
+               (keepSc, def) <- getDef fc (CLocal fc x) tags n alts
                if isNil cases
-                  then pure (fromMaybe (CErased fc) def)
+                  then (if keepSc
+                           then pure $ CLet fc (MN "eff" 0) False
+                                            (CLocal fc x)
+                                            (weaken (fromMaybe (CErased fc) def))
+                           else pure (fromMaybe (CErased fc) def))
                   else pure $ natHackTree $
                             CConCase fc (CLocal fc x) cases def
   toCExpTree' tags n (Case _ x scTy alts@(DelayCase _ _ _ :: _))
   toCExpTree' tags n (Case fc x scTy alts@(ConstCase _ _ :: _))
       = let fc = getLoc scTy in
             do cases <- constCases tags n alts
-               def <- getDef fc (CLocal fc x) tags n alts
+               (keepSc, def) <- getDef fc (CLocal fc x) tags n alts
                if isNil cases
-                  then pure (fromMaybe (CErased fc) def)
+                  then (if keepSc
+                           then pure $ CLet fc (MN "eff" 0) False
+                                            (CLocal fc x)
+                                            (weaken (fromMaybe (CErased fc) def))
+                           else pure (fromMaybe (CErased fc) def))
                   else pure $ CConstCase fc (CLocal fc x) cases def
   toCExpTree' tags n (Case _ x scTy alts@(DefaultCase sc :: _))
       = toCExpTree tags n sc
     getVars NoArgs = []
     getVars (ConsArg a rest) = MkVar First :: map weakenVar (getVars rest)
 toCDef tags n _ (DCon tag arity pos)
-    = pure $ MkCon (fromMaybe tag $ lookup n tags) arity pos
+    = let nt = maybe Nothing (Just . snd) pos in
+          pure $ MkCon (fromMaybe tag $ lookup n tags) arity nt
 toCDef tags n _ (TCon tag arity _ _ _ _ _ _)
     = pure $ MkCon (fromMaybe tag $ lookup n tags) arity Nothing
 -- We do want to be able to compile these, but also report an error at run time
 compileExp : {auto c : Ref Ctxt Defs} ->
              NameTags -> ClosedTerm -> Core (CExp [])
 compileExp tags tm
-    = toCExp tags (UN "main") tm
+    = do exp <- toCExp tags (UN "main") tm
+         pure exp
 ||| Given a name, look up an expression, and compile it to a CExp in the environment
 export
          ce <- toCDef tags n (type gdef)
                              !(toFullNames (definition gdef))
          setCompiled n ce
+export
+mkForgetDef : {auto c : Ref Ctxt Defs} ->
+              Name -> Core ()
+mkForgetDef n
+    = do defs <- get Ctxt
+         Just gdef <- lookupCtxtExact n (gamma defs)
+              | Nothing => throw (InternalError ("Trying to compile unknown name " ++ show n))
+         case compexpr gdef of
+              Nothing => pure ()
+              Just cdef => do let ncdef = forgetDef cdef
+                              setNamedCompiled n ncdef

src/Compiler/Inline.idr+207−35

@@ -1,5 +1,7 @@
1	module Compiler.Inline	1	module Compiler.Inline
2		2
		3	import Compiler.CompileExpr
		4
3	import Core.CompileExpr	5	import Core.CompileExpr
4	import Core.Context	6	import Core.Context
5	import Core.FC	7	import Core.FC
@@ -14,26 +16,12 @@ data EEnv : List Name -> List Name -> Type where · 8 unmodified lines
14	Nil : EEnv free []	16	Nil : EEnv free []
15	(::) : CExp free -> EEnv free vars -> EEnv free (x :: vars)	17	(::) : CExp free -> EEnv free vars -> EEnv free (x :: vars)
16		18
17	weakenEnv : EEnv free vars -> EEnv (x :: free) vars
18	weakenEnv [] = []
19	weakenEnv (e :: env) = weaken e :: weakenEnv env
20
21	weakenNsEnv : (xs : List Name) -> EEnv free vars -> EEnv (xs ++ free) vars
22	weakenNsEnv [] env = env
23	weakenNsEnv (x :: xs) env = weakenEnv (weakenNsEnv xs env)
24
25	extend : EEnv free vars -> (args : List (CExp free)) -> (args' : List Name) ->	19	extend : EEnv free vars -> (args : List (CExp free)) -> (args' : List Name) ->
26	LengthMatch args args' -> EEnv free (args' ++ vars)	20	LengthMatch args args' -> EEnv free (args' ++ vars)
27	extend env [] [] NilMatch = env	21	extend env [] [] NilMatch = env
28	extend env (a :: xs) (n :: ns) (ConsMatch w)	22	extend env (a :: xs) (n :: ns) (ConsMatch w)
29	= a :: extend env xs ns w	23	= a :: extend env xs ns w
30		24
31	extendLoc : FC -> EEnv free vars -> (args' : List Name) ->
32	EEnv (args' ++ free) (args' ++ vars)
33	extendLoc fc env [] = env
34	extendLoc fc env (n :: ns)
35	= CLocal fc First :: weakenEnv (extendLoc fc env ns)
36
37	Stack : List Name -> Type	25	Stack : List Name -> Type
38	Stack vars = List (CExp vars)	26	Stack vars = List (CExp vars)
39		27
@@ -58,13 +46,46 @@ takeFromStack env (e :: es) (a :: as) · 18 unmodified lines
58	takeFromStack env stk [] = pure (env, stk)	46	takeFromStack env stk [] = pure (env, stk)
59	takeFromStack env [] args = Nothing	47	takeFromStack env [] args = Nothing
60		48
61	thinAll : (ns : List Name) -> CExp (outer ++ inner) -> CExp (outer ++ ns ++ inner)	49	data LVar : Type where
62	thinAll [] exp = exp	50
63	thinAll {outer} {inner} (n :: ns) exp	51	genName : {auto l : Ref LVar Int} ->
64	= thin {outer} {inner = ns ++ inner} n (thinAll ns exp)	52	String -> Core Name
		53	genName n
		54	= do i <- get LVar
		55	put LVar (i + 1)
		56	pure (MN n i)
		57
		58	refToLocal : Name -> (x : Name) -> CExp vars -> CExp (x :: vars)
		59	refToLocal x new tm = refsToLocals (Add new x None) tm
		60
		61	mutual
		62	used : Name -> CExp free -> Bool
		63	used n (CRef _ n') = n == n'
		64	used n (CLam _ _ sc) = used n sc
		65	used n (CLet _ _ _ val sc) = used n val \|\| used n sc
		66	used n (CApp _ x args) = used n x \|\| or (map Delay (map (used n) args))
		67	used n (CCon _ _ _ args) = or (map Delay (map (used n) args))
		68	used n (COp _ _ args) = or (map Delay (map (used n) args))
		69	used n (CExtPrim _ _ args) = or (map Delay (map (used n) args))
		70	used n (CForce _ x) = used n x
		71	used n (CDelay _ x) = used n x
		72	used n (CConCase fc sc alts def)
		73	= used n sc \|\| or (map Delay (map (usedCon n) alts))
		74	\|\| maybe False (used n) def
		75	used n (CConstCase fc sc alts def)
		76	= used n sc \|\| or (map Delay (map (usedConst n) alts))
		77	\|\| maybe False (used n) def
		78	used _ tm = False
		79
		80	usedCon : Name -> CConAlt free -> Bool
		81	usedCon n (MkConAlt _ _ _ sc) = used n sc
		82
		83	usedConst : Name -> CConstAlt free -> Bool
		84	usedConst n (MkConstAlt _ sc) = used n sc
65		85
66	mutual	86	mutual
67	evalLocal : {auto c : Ref Ctxt Defs} ->	87	evalLocal : {auto c : Ref Ctxt Defs} ->
		88	{auto l : Ref LVar Int} ->
68	FC -> List Name -> Stack free ->	89	FC -> List Name -> Stack free ->
69	EEnv free vars ->	90	EEnv free vars ->
70	{idx : Nat} -> .(IsVar x idx (vars ++ free)) ->	91	{idx : Nat} -> .(IsVar x idx (vars ++ free)) ->
@@ -72,11 +93,14 @@ mutual · 1 unmodified line
72	evalLocal {vars = []} fc rec stk env p	93	evalLocal {vars = []} fc rec stk env p
73	= pure $ unload stk (CLocal fc p)	94	= pure $ unload stk (CLocal fc p)
74	evalLocal {vars = x :: xs} fc rec stk (v :: env) First	95	evalLocal {vars = x :: xs} fc rec stk (v :: env) First
75	= eval rec env stk (weakenNs xs v)	96	= case stk of
		97	[] => pure v
		98	_ => eval rec env stk (weakenNs xs v)
76	evalLocal {vars = x :: xs} fc rec stk (_ :: env) (Later p)	99	evalLocal {vars = x :: xs} fc rec stk (_ :: env) (Later p)
77	= evalLocal fc rec stk env p	100	= evalLocal fc rec stk env p
78		101
79	tryApply : {auto c : Ref Ctxt Defs} ->	102	tryApply : {auto c : Ref Ctxt Defs} ->
		103	{auto l : Ref LVar Int} ->
80	List Name -> Stack free -> EEnv free vars -> CDef ->	104	List Name -> Stack free -> EEnv free vars -> CDef ->
81	Core (Maybe (CExp free))	105	Core (Maybe (CExp free))
82	tryApply {free} {vars} rec stk env (MkFun args exp)	106	tryApply {free} {vars} rec stk env (MkFun args exp)
@@ -89,6 +113,7 @@ mutual · 6 unmodified lines
89	tryApply rec stk env _ = pure Nothing	113	tryApply rec stk env _ = pure Nothing
90		114
91	eval : {auto c : Ref Ctxt Defs} ->	115	eval : {auto c : Ref Ctxt Defs} ->
		116	{auto l : Ref LVar Int} ->
92	List Name -> EEnv free vars -> Stack free -> CExp (vars ++ free) ->	117	List Name -> EEnv free vars -> Stack free -> CExp (vars ++ free) ->
93	Core (CExp free)	118	Core (CExp free)
94	eval rec env stk (CLocal fc p) = evalLocal fc rec stk env p	119	eval rec env stk (CLocal fc p) = evalLocal fc rec stk env p
@@ -100,18 +125,21 @@ mutual · 5 unmodified lines
100	\| Nothing => pure (unload stk (CRef fc n))	125	\| Nothing => pure (unload stk (CRef fc n))
101	let arity = getArity def	126	let arity = getArity def
102	if (Inline `elem` flags gdef) && (not (n `elem` rec))	127	if (Inline `elem` flags gdef) && (not (n `elem` rec))
103	then do ap <- tryApply (n :: rec) stk env def	128	then do ap <- tryApply (n :: rec) stk env def
104	pure $ maybe (unloadApp arity stk (CRef fc n)) id ap	129	pure $ maybe (unloadApp arity stk (CRef fc n)) id ap
105	else pure $ unloadApp arity stk (CRef fc n)	130	else pure $ unloadApp arity stk (CRef fc n)
106	eval {vars} {free} rec env [] (CLam fc x sc)	131	eval {vars} {free} rec env [] (CLam fc x sc)
107	= do let thinsc = thin x {outer = x :: vars} {inner = free} sc	132	= do xn <- genName "lamv"
108	sc' <- eval rec (CLocal fc First :: weakenEnv env) [] thinsc	133	sc' <- eval rec (CRef fc xn :: env) [] sc
109	pure $ CLam fc x sc'	134	pure $ CLam fc x (refToLocal xn x sc')
110	eval rec env (e :: stk) (CLam fc x sc) = eval rec (e :: env) stk sc	135	eval rec env (e :: stk) (CLam fc x sc) = eval rec (e :: env) stk sc
111	eval {vars} {free} rec env stk (CLet fc x val sc)	136	eval {vars} {free} rec env stk (CLet fc x inl val sc)
112	= do let thinsc = thin x {outer = x :: vars} {inner = free} sc	137	= do xn <- genName "letv"
113	sc' <- eval rec (CLocal fc First :: weakenEnv env) [] thinsc	138	sc' <- eval rec (CRef fc xn :: env) [] sc
114	pure $ unload stk $ CLet fc x !(eval rec env [] val) sc'	139	if inl && used xn sc'
		140	then do val' <- eval rec env [] val
		141	pure (unload stk $ CLet fc x inl val' (refToLocal xn x sc'))
		142	else pure sc'
115	eval rec env stk (CApp fc f args)	143	eval rec env stk (CApp fc f args)
116	= eval rec env (!(traverse (eval rec env []) args) ++ stk) f	144	= eval rec env (!(traverse (eval rec env []) args) ++ stk) f
117	eval rec env stk (CCon fc n t args)	145	eval rec env stk (CCon fc n t args)
@@ -144,22 +172,34 @@ mutual · 26 unmodified lines
144	eval rec env stk (CErased fc) = pure $ unload stk $ CErased fc	172	eval rec env stk (CErased fc) = pure $ unload stk $ CErased fc
145	eval rec env stk (CCrash fc str) = pure $ unload stk $ CCrash fc str	173	eval rec env stk (CCrash fc str) = pure $ unload stk $ CCrash fc str
146		174
		175	extendLoc : {auto l : Ref LVar Int} ->
		176	FC -> EEnv free vars -> (args' : List Name) ->
		177	Core (Bounds args', EEnv free (args' ++ vars))
		178	extendLoc fc env [] = pure (None, env)
		179	extendLoc fc env (n :: ns)
		180	= do xn <- genName "cv"
		181	(bs', env') <- extendLoc fc env ns
		182	pure (Add n xn bs', CRef fc xn :: env')
		183
147	evalAlt : {auto c : Ref Ctxt Defs} ->	184	evalAlt : {auto c : Ref Ctxt Defs} ->
		185	{auto l : Ref LVar Int} ->
148	FC -> List Name -> EEnv free vars -> Stack free -> CConAlt (vars ++ free) ->	186	FC -> List Name -> EEnv free vars -> Stack free -> CConAlt (vars ++ free) ->
149	Core (CConAlt free)	187	Core (CConAlt free)
150	evalAlt {free} {vars} fc rec env stk (MkConAlt n t args sc)	188	evalAlt {free} {vars} fc rec env stk (MkConAlt n t args sc)
151	= do let sc' = thinAll {outer=args ++ vars} {inner=free} args	189	= do (bs, env') <- extendLoc fc env args
152	(rewrite sym (appendAssociative args vars free) in sc)	190	scEval <- eval rec env' stk
153	scEval <- eval rec (extendLoc fc env args) (map (weakenNs args) stk) sc'	191	(rewrite sym (appendAssociative args vars free) in sc)
154	pure $ MkConAlt n t args scEval	192	pure $ MkConAlt n t args (refsToLocals bs scEval)
155		193
156	evalConstAlt : {auto c : Ref Ctxt Defs} ->	194	evalConstAlt : {auto c : Ref Ctxt Defs} ->
		195	{auto l : Ref LVar Int} ->
157	List Name -> EEnv free vars -> Stack free -> CConstAlt (vars ++ free) ->	196	List Name -> EEnv free vars -> Stack free -> CConstAlt (vars ++ free) ->
158	Core (CConstAlt free)	197	Core (CConstAlt free)
159	evalConstAlt rec env stk (MkConstAlt c sc)	198	evalConstAlt rec env stk (MkConstAlt c sc)
160	= MkConstAlt c <$> eval rec env stk sc	199	= MkConstAlt c <$> eval rec env stk sc
161		200
162	pickAlt : {auto c : Ref Ctxt Defs} ->	201	pickAlt : {auto c : Ref Ctxt Defs} ->
		202	{auto l : Ref LVar Int} ->
163	List Name -> EEnv free vars -> Stack free ->	203	List Name -> EEnv free vars -> Stack free ->
164	CExp free -> List (CConAlt (vars ++ free)) ->	204	CExp free -> List (CConAlt (vars ++ free)) ->
165	Maybe (CExp (vars ++ free)) ->	205	Maybe (CExp (vars ++ free)) ->
@@ -180,6 +220,7 @@ mutual · 14 unmodified lines
180	pickAlt rec env stk _ _ _ = pure Nothing	220	pickAlt rec env stk _ _ _ = pure Nothing
181		221
182	pickConstAlt : {auto c : Ref Ctxt Defs} ->	222	pickConstAlt : {auto c : Ref Ctxt Defs} ->
		223	{auto l : Ref LVar Int} ->
183	List Name -> EEnv free vars -> Stack free ->	224	List Name -> EEnv free vars -> Stack free ->
184	CExp free -> List (CConstAlt (vars ++ free)) ->	225	CExp free -> List (CConstAlt (vars ++ free)) ->
185	Maybe (CExp (vars ++ free)) ->	226	Maybe (CExp (vars ++ free)) ->
@@ -192,10 +233,124 @@ mutual · 6 unmodified lines
192	else pickConstAlt rec env stk (CPrimVal fc c) alts def	233	else pickConstAlt rec env stk (CPrimVal fc c) alts def
193	pickConstAlt rec env stk _ _ _ = pure Nothing	234	pickConstAlt rec env stk _ _ _ = pure Nothing
194		235
		236	-- Inlining may have messed with function arity (e.g. by adding lambdas to
		237	-- the LHS to avoid needlessly making a closure) so fix them up here. This
		238	-- needs to be right because typically back ends need to know whether a
		239	-- name is under- or over-applied
		240	fixArityTm : {auto c : Ref Ctxt Defs} ->
		241	CExp vars -> List (CExp vars) -> Core (CExp vars)
		242	fixArityTm (CRef fc n) args
		243	= do defs <- get Ctxt
		244	Just gdef <- lookupCtxtExact n (gamma defs)
		245	\| Nothing => pure (unload args (CRef fc n))
		246	let Just def = compexpr gdef
		247	\| Nothing => pure (unload args (CRef fc n))
		248	let arity = getArity def
		249	pure $ expandToArity arity (CApp fc (CRef fc n) []) args
		250	fixArityTm (CLam fc x sc) args
		251	= pure $ expandToArity Z (CLam fc x !(fixArityTm sc [])) args
		252	fixArityTm (CLet fc x inl val sc) args
		253	= pure $ expandToArity Z
		254	(CLet fc x inl !(fixArityTm val []) !(fixArityTm sc [])) args
		255	fixArityTm (CApp fc f fargs) args
		256	= fixArityTm f (!(traverse (\tm => fixArityTm tm []) fargs) ++ args)
		257	fixArityTm (CCon fc n t args) []
		258	= pure $ CCon fc n t !(traverse (\tm => fixArityTm tm []) args)
		259	fixArityTm (COp fc op args) []
		260	= pure $ COp fc op !(traverseArgs args)
		261	where
		262	traverseArgs : Vect n (CExp vs) -> Core (Vect n (CExp vs))
		263	traverseArgs [] = pure []
		264	traverseArgs (a :: as) = pure $ !(fixArityTm a []) :: !(traverseArgs as)
		265	fixArityTm (CExtPrim fc p args) []
		266	= pure $ CExtPrim fc p !(traverse (\tm => fixArityTm tm []) args)
		267	fixArityTm (CForce fc tm) args
		268	= pure $ expandToArity Z (CForce fc !(fixArityTm tm [])) args
		269	fixArityTm (CDelay fc tm) args
		270	= pure $ expandToArity Z (CDelay fc !(fixArityTm tm [])) args
		271	fixArityTm (CConCase fc sc alts def) args
		272	= pure $ expandToArity Z
		273	(CConCase fc !(fixArityTm sc [])
		274	!(traverse fixArityAlt alts)
		275	!(traverseOpt (\tm => fixArityTm tm []) def)) args
		276	where
		277	fixArityAlt : CConAlt vars -> Core (CConAlt vars)
		278	fixArityAlt (MkConAlt n t a sc)
		279	= pure $ MkConAlt n t a !(fixArityTm sc [])
		280	fixArityTm (CConstCase fc sc alts def) args
		281	= pure $ expandToArity Z
		282	(CConstCase fc !(fixArityTm sc [])
		283	!(traverse fixArityConstAlt alts)
		284	!(traverseOpt (\tm => fixArityTm tm []) def)) args
		285	where
		286	fixArityConstAlt : CConstAlt vars -> Core (CConstAlt vars)
		287	fixArityConstAlt (MkConstAlt c sc)
		288	= pure $ MkConstAlt c !(fixArityTm sc [])
		289	fixArityTm t [] = pure t
		290	fixArityTm t args = pure $ expandToArity Z t args
		291
		292	export
		293	fixArityExp : {auto c : Ref Ctxt Defs} ->
		294	CExp vars -> Core (CExp vars)
		295	fixArityExp tm = fixArityTm tm []
		296
		297	fixArity : {auto c : Ref Ctxt Defs} ->
		298	CDef -> Core CDef
		299	fixArity (MkFun args exp) = pure $ MkFun args !(fixArityTm exp [])
		300	fixArity (MkError exp) = pure $ MkError !(fixArityTm exp [])
		301	fixArity d = pure d
		302
		303	getLams : Int -> SubstCEnv done args -> CExp (done ++ args) ->
		304	(args' ** (SubstCEnv args' args, CExp (args' ++ args)))
		305	getLams {done} i env (CLam fc x sc)
		306	= getLams {done = x :: done} (i + 1) (CRef fc (MN "ext" i) :: env) sc
		307	getLams {done} i env sc = (done ** (env, sc))
		308
		309	mkBounds : (xs : _) -> Bounds xs
		310	mkBounds [] = None
		311	mkBounds (x :: xs) = Add x x (mkBounds xs)
		312
		313	getNewArgs : SubstCEnv done args -> List Name
		314	getNewArgs [] = []
		315	getNewArgs (CRef _ n :: xs) = n :: getNewArgs xs
		316	getNewArgs {done = x :: xs} (_ :: sub) = x :: getNewArgs sub
		317
		318	-- Move any lambdas in the body of the definition into the lhs list of vars.
		319	-- Annoyingly, the indices will need fixing up because the order in the top
		320	-- level definition goes left to right (i.e. first argument has lowest index,
		321	-- not the highest, as you'd expect if they were all lambdas).
		322	mergeLambdas : (args : List Name) -> CExp args -> (args' ** CExp args')
		323	mergeLambdas args (CLam fc x sc)
		324	= let (args' ** (env, exp')) = getLams 0 [] (CLam fc x sc)
		325	expNs = substs env exp'
		326	newArgs = reverse $ getNewArgs env
		327	expLocs = mkLocals {later = args} {vars=[]} (mkBounds newArgs)
		328	(rewrite appendNilRightNeutral args in expNs) in
		329	(_ ** expLocs)
		330	mergeLambdas args exp = (args ** exp)
		331
		332	doEval : {auto c : Ref Ctxt Defs} ->
		333	Name -> CExp args -> Core (CExp args)
		334	doEval n exp
		335	= do l <- newRef LVar (the Int 0)
		336	log 10 (show n ++ ": " ++ show exp)
		337	exp' <- eval [] [] [] exp
		338	log 10 ("Inlined: " ++ show exp')
		339	pure exp'
		340
195	inline : {auto c : Ref Ctxt Defs} ->	341	inline : {auto c : Ref Ctxt Defs} ->
196	CDef -> Core CDef	342	Name -> CDef -> Core CDef
197	inline (MkFun args exp) = MkFun args <$> eval [] [] [] exp	343	inline n (MkFun args def)
198	inline d = pure d	344	= pure $ MkFun args !(doEval n def)
		345	inline n d = pure d
		346
		347	-- merge lambdas from expression into top level arguments
		348	mergeLam : {auto c : Ref Ctxt Defs} ->
		349	CDef -> Core CDef
		350	mergeLam (MkFun args def)
		351	= do let (args' ** exp') = mergeLambdas args def
		352	pure $ MkFun args' exp'
		353	mergeLam d = pure d
199		354
200	export	355	export
201	inlineDef : {auto c : Ref Ctxt Defs} ->	356	inlineDef : {auto c : Ref Ctxt Defs} ->
@@ -204,5 +359,22 @@ inlineDef n · 2 unmodified lines
204	= do defs <- get Ctxt	359	= do defs <- get Ctxt
205	Just def <- lookupCtxtExact n (gamma defs) \| Nothing => pure ()	360	Just def <- lookupCtxtExact n (gamma defs) \| Nothing => pure ()
206	let Just cexpr = compexpr def \| Nothing => pure ()	361	let Just cexpr = compexpr def \| Nothing => pure ()
207	setCompiled n !(inline cexpr)	362	setCompiled n !(inline n cexpr)
208		363
		364	export
		365	fixArityDef : {auto c : Ref Ctxt Defs} ->
		366	Name -> Core ()
		367	fixArityDef n
		368	= do defs <- get Ctxt
		369	Just def <- lookupCtxtExact n (gamma defs) \| Nothing => pure ()
		370	let Just cexpr = compexpr def \| Nothing => pure ()
		371	setCompiled n !(fixArity cexpr)
		372
		373	export
		374	mergeLamDef : {auto c : Ref Ctxt Defs} ->
		375	Name -> Core ()
		376	mergeLamDef n
		377	= do defs <- get Ctxt
		378	Just def <- lookupCtxtExact n (gamma defs) \| Nothing => pure ()
		379	let Just cexpr = compexpr def \| Nothing => pure ()
		380	setCompiled n !(mergeLam cexpr)

src/Compiler/LambdaLift.idr+237−0

@@ -0,0 +1,237 @@
	1	module Compuler.LambdaLift
	2
	3	import Core.CompileExpr
	4	import Core.Context
	5	import Core.Core
	6	import Core.TT
	7
	8	import Data.Vect
	9
	10	%default covering
	11
	12	mutual
	13	public export
	14	data Lifted : List Name -> Type where
	15	LLocal : {idx : Nat} -> FC -> .(IsVar x idx vars) -> Lifted vars
	16	-- A known function applied to exactly the right number of arguments,
	17	-- so the runtime can Just Go
	18	LAppName : FC -> Name -> List (Lifted vars) -> Lifted vars
	19	-- A known function applied to too few arguments, so the runtime should
	20	-- make a closure and wait for the remaining arguments
	21	LUnderApp : FC -> Name -> (missing : Nat) ->
	22	(args : List (Lifted vars)) -> Lifted vars
	23	-- A closure applied to one more argument (so, for example a closure
	24	-- which is waiting for another argument before it can run).
	25	-- The runtime should add the argument to the closure and run the result
	26	-- if it is now fully applied.
	27	LApp : FC -> (closure : Lifted vars) -> (arg : Lifted vars) -> Lifted vars
	28	LLet : FC -> (x : Name) -> Lifted vars ->
	29	Lifted (x :: var) -> Lifted vars
	30	LCon : FC -> Name -> (tag : Int) -> List (Lifted vars) -> Lifted vars
	31	LOp : FC -> PrimFn arity -> Vect arity (Lifted vars) -> Lifted vars
	32	LExtPrim : FC -> (p : Name) -> List (Lifted vars) -> Lifted vars
	33	LConCase : FC -> Lifted vars ->
	34	List (LiftedConAlt vars) ->
	35	Maybe (Lifted vars) -> Lifted vars
	36	LConstCase : FC -> Lifted vars ->
	37	List (LiftedConstAlt vars) ->
	38	Maybe (Lifted vars) -> Lifted vars
	39	LPrimVal : FC -> Constant -> Lifted vars
	40	LErased : FC -> Lifted vars
	41	LCrash : FC -> String -> Lifted vars
	42
	43	public export
	44	data LiftedConAlt : List Name -> Type where
	45	MkLConAlt : Name -> (tag : Int) -> (args : List Name) ->
	46	Lifted (args ++ vars) -> LiftedConAlt vars
	47
	48	public export
	49	data LiftedConstAlt : List Name -> Type where
	50	MkLConstAlt : Constant -> Lifted vars -> LiftedConstAlt vars
	51
	52	public export
	53	data LiftedDef : Type where
	54	-- We take the outer scope and the function arguments separately so that
	55	-- we don't have to reshuffle de Bruijn indices, which is expensive.
	56	-- This should be compiled as a function which takes 'args' first,
	57	-- then 'scope'.
	58	MkLFun : (args : List Name) -> -- function arguments
	59	(scope : List Name) -> -- outer scope
	60	Lifted (scope ++ args) -> LiftedDef
	61	MkLCon : (tag : Int) -> (arity : Nat) -> (nt : Maybe Nat) -> LiftedDef
	62	MkLForeign : (ccs : List String) ->
	63	(fargs : List CFType) ->
	64	CFType ->
	65	LiftedDef
	66	MkLError : Lifted [] -> LiftedDef
	67
	68	mutual
	69	export
	70	Show (Lifted vs) where
	71	show (LLocal {x} _ _) = "!" ++ show x
	72	show (LAppName fc n args)
	73	= show n ++ "(" ++ showSep ", " (map show args) ++ ")"
	74	show (LUnderApp fc n m args)
	75	= "<" ++ show n ++ " underapp " ++ show m ++ ">(" ++
	76	showSep ", " (map show args) ++ ")"
	77	show (LApp fc c arg)
	78	= show c ++ " @ (" ++ show arg ++ ")"
	79	show (LLet fc x val sc)
	80	= "%let " ++ show x ++ " = " ++ show val ++ " in " ++ show sc
	81	show (LCon fc n t args)
	82	= "%con " ++ show n ++ "(" ++ showSep ", " (map show args) ++ ")"
	83	show (LOp fc op args)
	84	= "%op " ++ show op ++ "(" ++ showSep ", " (toList (map show args)) ++ ")"
	85	show (LExtPrim fc p args)
	86	= "%extprim " ++ show p ++ "(" ++ showSep ", " (map show args) ++ ")"
	87	show (LConCase fc sc alts def)
	88	= "%case " ++ show sc ++ " of { "
	89	++ showSep "\| " (map show alts) ++ " " ++ show def
	90	show (LConstCase fc sc alts def)
	91	= "%case " ++ show sc ++ " of { "
	92	++ showSep "\| " (map show alts) ++ " " ++ show def
	93	show (LPrimVal _ x) = show x
	94	show (LErased _) = "___"
	95	show (LCrash _ x) = "%CRASH(" ++ show x ++ ")"
	96
	97	export
	98	Show (LiftedConAlt vs) where
	99	show (MkLConAlt n t args sc)
	100	= "%conalt " ++ show n ++
	101	"(" ++ showSep ", " (map show args) ++ ") => " ++ show sc
	102
	103	export
	104	Show (LiftedConstAlt vs) where
	105	show (MkLConstAlt c sc)
	106	= "%constalt(" ++ show c ++ ") => " ++ show sc
	107
	108	export
	109	Show LiftedDef where
	110	show (MkLFun args scope exp) = show args ++ show scope ++ ": " ++ show exp
	111	show (MkLCon tag arity pos)
	112	= "Constructor tag " ++ show tag ++ " arity " ++ show arity ++
	113	maybe "" (\n => " (newtype by " ++ show n ++ ")") pos
	114	show (MkLForeign ccs args ret)
	115	= "Foreign call " ++ show ccs ++ " " ++
	116	show args ++ " -> " ++ show ret
	117	show (MkLError exp) = "Error: " ++ show exp
	118
	119
	120	data Lifts : Type where
	121
	122	record LDefs where
	123	constructor MkLDefs
	124	basename : Name -- top level name we're lifting from
	125	defs : List (Name, LiftedDef) -- new definitions we made
	126	nextName : Int -- name of next definition to lift
	127
	128	genName : {auto l : Ref Lifts LDefs} ->
	129	Core Name
	130	genName
	131	= do ldefs <- get Lifts
	132	let i = nextName ldefs
	133	put Lifts (record { nextName = i + 1 } ldefs)
	134	pure $ mkName (basename ldefs) i
	135	where
	136	mkName : Name -> Int -> Name
	137	mkName (NS ns b) i = NS ns (mkName b i)
	138	mkName (UN n) i = MN n i
	139	mkName n i = MN (show n) i
	140
	141	unload : FC -> Lifted vars -> List (Lifted vars) -> Core (Lifted vars)
	142	unload fc f [] = pure f
	143	unload fc f (a :: as) = unload fc (LApp fc f a) as
	144
	145	mutual
	146	makeLam : {auto l : Ref Lifts LDefs} ->
	147	{vars : _} ->
	148	FC -> (bound : List Name) ->
	149	CExp (bound ++ vars) -> Core (Lifted vars)
	150	makeLam fc bound (CLam _ x sc') = makeLam fc (x :: bound) sc'
	151	makeLam {vars} fc bound sc
	152	= do scl <- liftExp sc
	153	n <- genName
	154	ldefs <- get Lifts
	155	put Lifts (record { defs $= ((n, MkLFun vars bound scl) ::) } ldefs)
	156	-- TODO: an optimisation here would be to spot which variables
	157	-- aren't used in the new definition, and not abstract over them
	158	-- in the new definition. Given that we have to do some messing
	159	-- about with indices anyway, it's probably not costly to do.
	160	pure $ LUnderApp fc n (length bound) (allVars vars)
	161	where
	162	allPrfs : (vs : List Name) -> List (Var vs)
	163	allPrfs [] = []
	164	allPrfs (v :: vs) = MkVar First :: map weaken (allPrfs vs)
	165
	166	-- apply to all the variables. 'First' will be first in the last, which
	167	-- is good, because the most recently bound name is the first argument to
	168	-- the resulting function
	169	allVars : (vs : List Name) -> List (Lifted vs)
	170	allVars vs = map (\ (MkVar p) => LLocal fc p) (allPrfs vs)
	171
	172	liftExp : {auto l : Ref Lifts LDefs} ->
	173	CExp vars -> Core (Lifted vars)
	174	liftExp (CLocal fc prf) = pure $ LLocal fc prf
	175	liftExp (CRef fc n) = pure $ LAppName fc n [] -- probably shouldn't happen!
	176	liftExp (CLam fc x sc) = makeLam fc [x] sc
	177	liftExp (CLet fc x _ val sc) = pure $ LLet fc x !(liftExp val) !(liftExp sc)
	178	liftExp (CApp fc (CRef _ n) args) -- names are applied exactly in compileExp
	179	= pure $ LAppName fc n !(traverse liftExp args)
	180	liftExp (CApp fc f args)
	181	= unload fc !(liftExp f) !(traverse liftExp args)
	182	liftExp (CCon fc n t args) = pure $ LCon fc n t !(traverse liftExp args)
	183	liftExp (COp fc op args)
	184	= pure $ LOp fc op !(traverseArgs args)
	185	where
	186	traverseArgs : Vect n (CExp vars) -> Core (Vect n (Lifted vars))
	187	traverseArgs [] = pure []
	188	traverseArgs (a :: as) = pure $ !(liftExp a) :: !(traverseArgs as)
	189	liftExp (CExtPrim fc p args) = pure $ LExtPrim fc p !(traverse liftExp args)
	190	liftExp (CForce fc tm) = liftExp (CApp fc tm [CErased fc])
	191	liftExp (CDelay fc tm) = liftExp (CLam fc (MN "x" 0) (weaken tm))
	192	liftExp (CConCase fc sc alts def)
	193	= pure $ LConCase fc !(liftExp sc) !(traverse liftConAlt alts)
	194	!(traverseOpt liftExp def)
	195	where
	196	liftConAlt : CConAlt vars -> Core (LiftedConAlt vars)
	197	liftConAlt (MkConAlt n t args sc) = pure $ MkLConAlt n t args !(liftExp sc)
	198	liftExp (CConstCase fc sc alts def)
	199	= pure $ LConstCase fc !(liftExp sc) !(traverse liftConstAlt alts)
	200	!(traverseOpt liftExp def)
	201	where
	202	liftConstAlt : CConstAlt vars -> Core (LiftedConstAlt vars)
	203	liftConstAlt (MkConstAlt c sc) = pure $ MkLConstAlt c !(liftExp sc)
	204	liftExp (CPrimVal fc c) = pure $ LPrimVal fc c
	205	liftExp (CErased fc) = pure $ LErased fc
	206	liftExp (CCrash fc str) = pure $ LCrash fc str
	207
	208	liftBody : Name -> CExp vars -> Core (Lifted vars, List (Name, LiftedDef))
	209	liftBody n tm
	210	= do l <- newRef Lifts (MkLDefs n [] 0)
	211	tml <- liftExp {l} tm
	212	ldata <- get Lifts
	213	pure (tml, defs ldata)
	214
	215	lambdaLiftDef : Name -> CDef -> Core (List (Name, LiftedDef))
	216	lambdaLiftDef n (MkFun args exp)
	217	= do (expl, defs) <- liftBody n exp
	218	pure ((n, MkLFun args [] expl) :: defs)
	219	lambdaLiftDef n (MkCon t a nt) = pure [(n, MkLCon t a nt)]
	220	lambdaLiftDef n (MkForeign ccs fargs ty) = pure [(n, MkLForeign ccs fargs ty)]
	221	lambdaLiftDef n (MkError exp)
	222	= do (expl, defs) <- liftBody n exp
	223	pure ((n, MkLError expl) :: defs)
	224
	225	-- Return the lambda lifted definitions required for the given name.
	226	-- If the name hasn't been compiled yet (via CompileExpr.compileDef) then
	227	-- this will return an empty list
	228	-- An empty list an error, because on success you will always get at least
	229	-- one definition, the lifted definition for the given name.
	230	export
	231	lambdaLift : {auto c : Ref Ctxt Defs} ->
	232	Name -> Core (List (Name, LiftedDef))
	233	lambdaLift n
	234	= do defs <- get Ctxt
	235	Just def <- lookupCtxtExact n (gamma defs) \| Nothing => pure []
	236	let Just cexpr = compexpr def \| Nothing => pure []
	237	lambdaLiftDef n cexpr

src/Compiler/Scheme/Chez.idr+38−31

 chezString cs = strCons '"' (showChezString (unpack cs) "\"")
 mutual
-  tySpec : CExp vars -> Core String
+  tySpec : NamedCExp -> Core String
   -- Primitive types have been converted to names for the purpose of matching
   -- on types
-  tySpec (CCon fc (UN "Int") _ []) = pure "int"
+  tySpec (NmCon fc (UN "Int") _ []) = pure "int"
-  tySpec (CCon fc (UN "String") _ []) = pure "string"
+  tySpec (NmCon fc (UN "String") _ []) = pure "string"
-  tySpec (CCon fc (UN "Double") _ []) = pure "double"
+  tySpec (NmCon fc (UN "Double") _ []) = pure "double"
-  tySpec (CCon fc (UN "Char") _ []) = pure "char"
+  tySpec (NmCon fc (UN "Char") _ []) = pure "char"
-  tySpec (CCon fc (NS _ n) _ [_])
+  tySpec (NmCon fc (NS _ n) _ [_])
      = cond [(n == UN "Ptr", pure "void*")]
           (throw (GenericMsg fc ("Can't pass argument of type " ++ show n ++ " to foreign function")))
-  tySpec (CCon fc (NS _ n) _ [])
+  tySpec (NmCon fc (NS _ n) _ [])
      = cond [(n == UN "Unit", pure "void"),
              (n == UN "AnyPtr", pure "void*")]
           (throw (GenericMsg fc ("Can't pass argument of type " ++ show n ++ " to foreign function")))
   handleRet "void" op = op ++ " " ++ mkWorld (schConstructor 0 [])
   handleRet _ op = mkWorld op
-  getFArgs : CExp vars -> Core (List (CExp vars, CExp vars))
+  getFArgs : NamedCExp -> Core (List (NamedCExp, NamedCExp))
-  getFArgs (CCon fc _ 0 _) = pure []
+  getFArgs (NmCon fc _ 0 _) = pure []
-  getFArgs (CCon fc _ 1 [ty, val, rest]) = pure $ (ty, val) :: !(getFArgs rest)
+  getFArgs (NmCon fc _ 1 [ty, val, rest]) = pure $ (ty, val) :: !(getFArgs rest)
   getFArgs arg = throw (GenericMsg (getFC arg) ("Badly formed c call argument list " ++ show arg))
-  chezExtPrim : Int -> SVars vars -> ExtPrim -> List (CExp vars) -> Core String
+  chezExtPrim : Int -> ExtPrim -> List NamedCExp -> Core String
-  chezExtPrim i vs CCall [ret, CPrimVal fc (Str fn), fargs, world]
+  chezExtPrim i CCall [ret, NmPrimVal fc (Str fn), fargs, world]
       = do args <- getFArgs fargs
            argTypes <- traverse tySpec (map fst args)
            retType <- tySpec ret
-           argsc <- traverse (schExp chezExtPrim chezString 0 vs) (map snd args)
+           argsc <- traverse (schExp chezExtPrim chezString 0) (map snd args)
            pure $ handleRet retType ("((foreign-procedure #f " ++ show fn ++ " ("
                     ++ showSep " " argTypes ++ ") " ++ retType ++ ") "
                     ++ showSep " " argsc ++ ")")
-  chezExtPrim i vs CCall [ret, fn, args, world]
+  chezExtPrim i CCall [ret, fn, args, world]
       = pure "(error \"bad ffi call\")"
       -- throw (InternalError ("C FFI calls must be to statically known functions (" ++ show fn ++ ")"))
-  chezExtPrim i vs GetStr [world]
+  chezExtPrim i GetStr [world]
       = pure $ mkWorld "(get-line (current-input-port))"
-  chezExtPrim i vs GetField [CPrimVal _ (Str s), _, _, struct,
+  chezExtPrim i GetField [NmPrimVal _ (Str s), _, _, struct,
-                             CPrimVal _ (Str fld), _]
+                             NmPrimVal _ (Str fld), _]
-      = do structsc <- schExp chezExtPrim chezString 0 vs struct
+      = do structsc <- schExp chezExtPrim chezString 0 struct
            pure $ "(ftype-ref " ++ s ++ " (" ++ fld ++ ") " ++ structsc ++ ")"
-  chezExtPrim i vs GetField [_,_,_,_,_,_]
+  chezExtPrim i GetField [_,_,_,_,_,_]
       = pure "(error \"bad setField\")"
-  chezExtPrim i vs SetField [CPrimVal _ (Str s), _, _, struct,
+  chezExtPrim i SetField [NmPrimVal _ (Str s), _, _, struct,
-                             CPrimVal _ (Str fld), _, val, world]
+                             NmPrimVal _ (Str fld), _, val, world]
-      = do structsc <- schExp chezExtPrim chezString 0 vs struct
+      = do structsc <- schExp chezExtPrim chezString 0 struct
-           valsc <- schExp chezExtPrim chezString 0 vs val
+           valsc <- schExp chezExtPrim chezString 0 val
            pure $ mkWorld $
               "(ftype-set! " ++ s ++ " (" ++ fld ++ ") " ++ structsc ++
               " " ++ valsc ++ ")"
-  chezExtPrim i vs SetField [_,_,_,_,_,_,_,_]
+  chezExtPrim i SetField [_,_,_,_,_,_,_,_]
       = pure "(error \"bad setField\")"
-  chezExtPrim i vs SysCodegen []
+  chezExtPrim i SysCodegen []
       = pure $ "\"chez\""
-  chezExtPrim i vs prim args
+  chezExtPrim i prim args
-      = schExtCommon chezExtPrim chezString i vs prim args
+      = schExtCommon chezExtPrim chezString i prim args
 -- Reference label for keeping track of loaded external libraries
 data Loaded : Type where
     applyLams n (Nothing :: as) = applyLams ("(" ++ n ++ " #f)") as
     applyLams n (Just a :: as) = applyLams ("(" ++ n ++ " " ++ a ++ ")") as
+    getVal : String -> String
+    getVal str = "(vector-ref " ++ str ++ "1)"
     mkFun : List CFType -> CFType -> String -> String
     mkFun args ret n
         = let argns = mkNs 0 args in
 startChez target = unlines
     [ "#!/bin/sh"
     , ""
-    , "export LD_LIBRARY_PATH=$LD_LIBRARY_PATH:`dirname " ++ target ++ "`"
+    , "export LD_LIBRARY_PATH=\"$LD_LIBRARY_PATH:$(dirname \"" ++ target ++ "\")\""
-    , target ++ " \"$@\""
+    , "\"" ++ target ++ "\" \"$@\""
     ]
 ||| Compile a TT expression to Chez Scheme
     = do ds <- getDirectives Chez
          libs <- findLibs ds
          traverse_ copyLib libs
-         (ns, tags) <- findUsedNames tm
+         cdata <- getCompileData tm
+         let ns = allNames cdata
+         let tags = nameTags cdata
+         let ctm = forget (mainExpr cdata)
          defs <- get Ctxt
          l <- newRef {t = List String} Loaded ["libc", "libc 6"]
          s <- newRef {t = List String} Structs []
          fgndefs <- traverse getFgnCall ns
          compdefs <- traverse (getScheme chezExtPrim chezString defs) ns
          let code = fastAppend (map snd fgndefs ++ compdefs)
-         main <- schExp chezExtPrim chezString 0 [] !(compileExp tags tm)
+         main <- schExp chezExtPrim chezString 0 ctm
          chez <- coreLift findChez
          support <- readDataFile "chez/support.ss"
          let scm = schHeader chez (map snd libs) ++

src/Compiler/Scheme/Common.idr+119−122

@@ -85,6 +85,7 @@ schOp (Div IntType) [x, y] = op "b/" [x, y, "63"] · 84 unmodified lines
85	schOp (Add ty) [x, y] = op "+" [x, y]	85	schOp (Add ty) [x, y] = op "+" [x, y]
86	schOp (Sub ty) [x, y] = op "-" [x, y]	86	schOp (Sub ty) [x, y] = op "-" [x, y]
87	schOp (Mul ty) [x, y] = op "*" [x, y]	87	schOp (Mul ty) [x, y] = op "*" [x, y]
		88	schOp (Div IntegerType) [x, y] = op "quotient" [x, y]
88	schOp (Div ty) [x, y] = op "/" [x, y]	89	schOp (Div ty) [x, y] = op "/" [x, y]
89	schOp (Mod ty) [x, y] = op "remainder" [x, y]	90	schOp (Mod ty) [x, y] = op "remainder" [x, y]
90	schOp (Neg ty) [x] = op "-" [x]	91	schOp (Neg ty) [x] = op "-" [x]
@@ -136,12 +137,12 @@ schOp (Cast DoubleType StringType) [x] = op "number->string" [x] · 45 unmodified lines
136	schOp (Cast CharType StringType) [x] = op "string" [x]	137	schOp (Cast CharType StringType) [x] = op "string" [x]
137		138
138	schOp (Cast IntType IntegerType) [x] = x	139	schOp (Cast IntType IntegerType) [x] = x
139	schOp (Cast DoubleType IntegerType) [x] = op "floor" [x]	140	schOp (Cast DoubleType IntegerType) [x] = op "exact-floor" [x]
140	schOp (Cast CharType IntegerType) [x] = op "char->integer" [x]	141	schOp (Cast CharType IntegerType) [x] = op "char->integer" [x]
141	schOp (Cast StringType IntegerType) [x] = op "cast-string-int" [x]	142	schOp (Cast StringType IntegerType) [x] = op "cast-string-int" [x]
142		143
143	schOp (Cast IntegerType IntType) [x] = x	144	schOp (Cast IntegerType IntType) [x] = x
144	schOp (Cast DoubleType IntType) [x] = op "floor" [x]	145	schOp (Cast DoubleType IntType) [x] = op "exact-floor" [x]
145	schOp (Cast StringType IntType) [x] = op "cast-string-int" [x]	146	schOp (Cast StringType IntType) [x] = op "cast-string-int" [x]
146	schOp (Cast CharType IntType) [x] = op "char->integer" [x]	147	schOp (Cast CharType IntType) [x] = op "char->integer" [x]
147		148
@@ -234,7 +235,7 @@ toPrim pn = Unknown pn · 86 unmodified lines
234		235
235	export	236	export
236	mkWorld : String -> String	237	mkWorld : String -> String
237	mkWorld res = res -- MkIORes is a newtype now! schConstructor 0 ["#f", res, "#f"] -- MkIORes	238	mkWorld res = res -- MkIORes is a newtype now! schConstructor 0 [res, "#f"] -- MkIORes
238		239
239	schConstant : (String -> String) -> Constant -> String	240	schConstant : (String -> String) -> Constant -> String
240	schConstant _ (I x) = show x	241	schConstant _ (I x) = show x
@@ -258,82 +259,79 @@ schCaseDef Nothing = "" · 17 unmodified lines
258	schCaseDef (Just tm) = "(else " ++ tm ++ ")"	259	schCaseDef (Just tm) = "(else " ++ tm ++ ")"
259		260
260	export	261	export
261	schArglist : SVars ns -> String	262	schArglist : List Name -> String
262	schArglist [] = ""	263	schArglist [] = ""
263	schArglist [x] = x	264	schArglist [x] = schName x
264	schArglist (x :: xs) = x ++ " " ++ schArglist xs	265	schArglist (x :: xs) = schName x ++ " " ++ schArglist xs
265		266
266	parameters (schExtPrim : {vars : _} -> Int -> SVars vars -> ExtPrim -> List (CExp vars) -> Core String,	267	parameters (schExtPrim : Int -> ExtPrim -> List NamedCExp -> Core String,
267	schString : String -> String)	268	schString : String -> String)
268	mutual	269	mutual
269	schConAlt : Int -> SVars vars -> String -> CConAlt vars -> Core String	270	schConAlt : Int -> String -> NamedConAlt -> Core String
270	schConAlt {vars} i vs target (MkConAlt n tag args sc)	271	schConAlt i target (MkNConAlt n tag args sc)
271	= let vs' = extendSVars args vs in	272	= pure $ "((" ++ show tag ++ ") "
272	pure $ "((" ++ show tag ++ ") "	273	++ bindArgs 1 args !(schExp i sc) ++ ")"
273	++ bindArgs 1 args vs' !(schExp i vs' sc) ++ ")"
274	where	274	where
275	bindArgs : Int -> (ns : List Name) -> SVars (ns ++ vars) -> String -> String	275	bindArgs : Int -> (ns : List Name) -> String -> String
276	bindArgs i [] vs body = body	276	bindArgs i [] body = body
277	bindArgs i (n :: ns) (v :: vs) body	277	bindArgs i (n :: ns) body
278	= "(let ((" ++ v ++ " " ++ "(vector-ref " ++ target ++ " " ++ show i ++ "))) "	278	= "(let ((" ++ schName n ++ " " ++ "(vector-ref " ++ target ++ " " ++ show i ++ "))) "
279	++ bindArgs (i + 1) ns vs body ++ ")"	279	++ bindArgs (i + 1) ns body ++ ")"
280		280
281	schConstAlt : Int -> SVars vars -> String -> CConstAlt vars -> Core String	281	schConstAlt : Int -> String -> NamedConstAlt -> Core String
282	schConstAlt i vs target (MkConstAlt c exp)	282	schConstAlt i target (MkNConstAlt c exp)
283	= pure $ "((equal? " ++ target ++ " " ++ schConstant schString c ++ ") " ++ !(schExp i vs exp) ++ ")"	283	= pure $ "((equal? " ++ target ++ " " ++ schConstant schString c ++ ") " ++ !(schExp i exp) ++ ")"
284		284
285	-- oops, no traverse for Vect in Core	285	-- oops, no traverse for Vect in Core
286	schArgs : Int -> SVars vars -> Vect n (CExp vars) -> Core (Vect n String)	286	schArgs : Int -> Vect n NamedCExp -> Core (Vect n String)
287	schArgs i vs [] = pure []	287	schArgs i [] = pure []
288	schArgs i vs (arg :: args) = pure $ !(schExp i vs arg) :: !(schArgs i vs args)	288	schArgs i (arg :: args) = pure $ !(schExp i arg) :: !(schArgs i args)
289		289
290	export	290	export
291	schExp : Int -> SVars vars -> CExp vars -> Core String	291	schExp : Int -> NamedCExp -> Core String
292	schExp i vs (CLocal fc el) = pure $ lookupSVar el vs	292	schExp i (NmLocal fc n) = pure $ schName n
293	schExp i vs (CRef fc n) = pure $ schName n	293	schExp i (NmRef fc n) = pure $ schName n
294	schExp i vs (CLam fc x sc)	294	schExp i (NmLam fc x sc)
295	= do let vs' = extendSVars [x] vs	295	= do sc' <- schExp i sc
296	sc' <- schExp i vs' sc	296	pure $ "(lambda (" ++ schName x ++ ") " ++ sc' ++ ")"
297	pure $ "(lambda (" ++ lookupSVar First vs' ++ ") " ++ sc' ++ ")"	297	schExp i (NmLet fc x val sc)
298	schExp i vs (CLet fc x val sc)	298	= do val' <- schExp i val
299	= do let vs' = extendSVars [x] vs	299	sc' <- schExp i sc
300	val' <- schExp i vs val	300	pure $ "(let ((" ++ schName x ++ " " ++ val' ++ ")) " ++ sc' ++ ")"
301	sc' <- schExp i vs' sc	301	schExp i (NmApp fc x [])
302	pure $ "(let ((" ++ lookupSVar First vs' ++ " " ++ val' ++ ")) " ++ sc' ++ ")"	302	= pure $ "(" ++ !(schExp i x) ++ ")"
303	schExp i vs (CApp fc x [])	303	schExp i (NmApp fc x args)
304	= pure $ "(" ++ !(schExp i vs x) ++ ")"	304	= pure $ "(" ++ !(schExp i x) ++ " " ++ showSep " " !(traverse (schExp i) args) ++ ")"
305	schExp i vs (CApp fc x args)	305	schExp i (NmCon fc x tag args)
306	= pure $ "(" ++ !(schExp i vs x) ++ " " ++ showSep " " !(traverse (schExp i vs) args) ++ ")"	306	= pure $ schConstructor tag !(traverse (schExp i) args)
307	schExp i vs (CCon fc x tag args)	307	schExp i (NmOp fc op args)
308	= pure $ schConstructor tag !(traverse (schExp i vs) args)	308	= pure $ schOp op !(schArgs i args)
309	schExp i vs (COp fc op args)	309	schExp i (NmExtPrim fc p args)
310	= pure $ schOp op !(schArgs i vs args)	310	= schExtPrim i (toPrim p) args
311	schExp i vs (CExtPrim fc p args)	311	schExp i (NmForce fc t) = pure $ "(" ++ !(schExp i t) ++ ")"
312	= schExtPrim i vs (toPrim p) args	312	schExp i (NmDelay fc t) = pure $ "(lambda () " ++ !(schExp i t) ++ ")"
313	schExp i vs (CForce fc t) = pure $ "(" ++ !(schExp i vs t) ++ ")"	313	schExp i (NmConCase fc sc alts def)
314	schExp i vs (CDelay fc t) = pure $ "(lambda () " ++ !(schExp i vs t) ++ ")"	314	= do tcode <- schExp (i+1) sc
315	schExp i vs (CConCase fc sc alts def)	315	defc <- maybe (pure Nothing) (\v => pure (Just !(schExp i v))) def
316	= do tcode <- schExp (i+1) vs sc
317	defc <- maybe (pure Nothing) (\v => pure (Just !(schExp i vs v))) def
318	let n = "sc" ++ show i	316	let n = "sc" ++ show i
319	pure $ "(let ((" ++ n ++ " " ++ tcode ++ ")) (case (get-tag " ++ n ++ ") "	317	pure $ "(let ((" ++ n ++ " " ++ tcode ++ ")) (case (get-tag " ++ n ++ ") "
320	++ showSep " " !(traverse (schConAlt (i+1) vs n) alts)	318	++ showSep " " !(traverse (schConAlt (i+1) n) alts)
321	++ schCaseDef defc ++ "))"	319	++ schCaseDef defc ++ "))"
322	schExp i vs (CConstCase fc sc alts def)	320	schExp i (NmConstCase fc sc alts def)
323	= do defc <- maybe (pure Nothing) (\v => pure (Just !(schExp i vs v))) def	321	= do defc <- maybe (pure Nothing) (\v => pure (Just !(schExp i v))) def
324	tcode <- schExp (i+1) vs sc	322	tcode <- schExp (i+1) sc
325	let n = "sc" ++ show i	323	let n = "sc" ++ show i
326	pure $ "(let ((" ++ n ++ " " ++ tcode ++ ")) (cond "	324	pure $ "(let ((" ++ n ++ " " ++ tcode ++ ")) (cond "
327	++ showSep " " !(traverse (schConstAlt (i+1) vs n) alts)	325	++ showSep " " !(traverse (schConstAlt (i+1) n) alts)
328	++ schCaseDef defc ++ "))"	326	++ schCaseDef defc ++ "))"
329	schExp i vs (CPrimVal fc c) = pure $ schConstant schString c	327	schExp i (NmPrimVal fc c) = pure $ schConstant schString c
330	schExp i vs (CErased fc) = pure "'erased"	328	schExp i (NmErased fc) = pure "'erased"
331	schExp i vs (CCrash fc msg) = pure $ "(blodwen-error-quit " ++ show msg ++ ")"	329	schExp i (NmCrash fc msg) = pure $ "(blodwen-error-quit " ++ show msg ++ ")"
332		330
333	-- Need to convert the argument (a list of scheme arguments that may	331	-- Need to convert the argument (a list of scheme arguments that may
334	-- have been constructed at run time) to a scheme list to be passed to apply	332	-- have been constructed at run time) to a scheme list to be passed to apply
335	readArgs : Int -> SVars vars -> CExp vars -> Core String	333	readArgs : Int -> NamedCExp -> Core String
336	readArgs i vs tm = pure $ "(blodwen-read-args " ++ !(schExp i vs tm) ++ ")"	334	readArgs i tm = pure $ "(blodwen-read-args " ++ !(schExp i tm) ++ ")"
337		335
338	fileOp : String -> String	336	fileOp : String -> String
339	fileOp op = "(blodwen-file-op (lambda () " ++ op ++ "))"	337	fileOp op = "(blodwen-file-op (lambda () " ++ op ++ "))"
@@ -341,92 +339,91 @@ parameters (schExtPrim : {vars : _} -> Int -> SVars vars -> ExtPrim -> List (CEx · 1 unmodified line
341	-- External primitives which are common to the scheme codegens (they can be	339	-- External primitives which are common to the scheme codegens (they can be
342	-- overridden)	340	-- overridden)
343	export	341	export
344	schExtCommon : Int -> SVars vars -> ExtPrim -> List (CExp vars) -> Core String	342	schExtCommon : Int -> ExtPrim -> List NamedCExp -> Core String
345	schExtCommon i vs SchemeCall [ret, CPrimVal fc (Str fn), args, world]	343	schExtCommon i SchemeCall [ret, NmPrimVal fc (Str fn), args, world]
346	= pure $ mkWorld ("(apply " ++ fn ++" "	344	= pure $ mkWorld ("(apply " ++ fn ++" "
347	++ !(readArgs i vs args) ++ ")")	345	++ !(readArgs i args) ++ ")")
348	schExtCommon i vs SchemeCall [ret, fn, args, world]	346	schExtCommon i SchemeCall [ret, fn, args, world]
349	= pure $ mkWorld ("(apply (eval (string->symbol " ++ !(schExp i vs fn) ++")) "	347	= pure $ mkWorld ("(apply (eval (string->symbol " ++ !(schExp i fn) ++")) "
350	++ !(readArgs i vs args) ++ ")")	348	++ !(readArgs i args) ++ ")")
351	schExtCommon i vs PutStr [arg, world]	349	schExtCommon i PutStr [arg, world]
352	= pure $ "(display " ++ !(schExp i vs arg) ++ ") " ++ mkWorld (schConstructor 0 []) -- code for MkUnit	350	= pure $ "(begin (display " ++ !(schExp i arg) ++ ") " ++ mkWorld (schConstructor 0 []) ++ ")" -- code for MkUnit
353	schExtCommon i vs GetStr [world]	351	schExtCommon i GetStr [world]
354	= pure $ mkWorld "(blodwen-get-line (current-input-port))"	352	= pure $ mkWorld "(blodwen-get-line (current-input-port))"
355	schExtCommon i vs PutChar [arg, world]	353	schExtCommon i PutChar [arg, world]
356	= pure $ "(display " ++ !(schExp i vs arg) ++ ") " ++ mkWorld (schConstructor 0 []) -- code for MkUnit	354	= pure $ "(begin (display " ++ !(schExp i arg) ++ ") " ++ mkWorld (schConstructor 0 []) ++ ")" -- code for MkUnit
357	schExtCommon i vs GetChar [world]	355	schExtCommon i GetChar [world]
358	= pure $ mkWorld "(blodwen-get-char (current-input-port))"	356	= pure $ mkWorld "(blodwen-get-char (current-input-port))"
359	schExtCommon i vs FileOpen [file, mode, bin, world]	357	schExtCommon i FileOpen [file, mode, bin, world]
360	= pure $ mkWorld $ fileOp $ "(blodwen-open "	358	= pure $ mkWorld $ fileOp $ "(blodwen-open "
361	++ !(schExp i vs file) ++ " "	359	++ !(schExp i file) ++ " "
362	++ !(schExp i vs mode) ++ " "	360	++ !(schExp i mode) ++ " "
363	++ !(schExp i vs bin) ++ ")"	361	++ !(schExp i bin) ++ ")"
364	schExtCommon i vs FileClose [file, world]	362	schExtCommon i FileClose [file, world]
365	= pure $ "(blodwen-close-port " ++ !(schExp i vs file) ++ ") " ++ mkWorld (schConstructor 0 [])	363	= pure $ "(blodwen-close-port " ++ !(schExp i file) ++ ") " ++ mkWorld (schConstructor 0 [])
366	schExtCommon i vs FileReadLine [file, world]	364	schExtCommon i FileReadLine [file, world]
367	= pure $ mkWorld $ fileOp $ "(blodwen-get-line " ++ !(schExp i vs file) ++ ")"	365	= pure $ mkWorld $ fileOp $ "(blodwen-get-line " ++ !(schExp i file) ++ ")"
368	schExtCommon i vs FileWriteLine [file, str, world]	366	schExtCommon i FileWriteLine [file, str, world]
369	= pure $ mkWorld $ fileOp $ "(blodwen-putstring "	367	= pure $ mkWorld $ fileOp $ "(blodwen-putstring "
370	++ !(schExp i vs file) ++ " "	368	++ !(schExp i file) ++ " "
371	++ !(schExp i vs str) ++ ")"	369	++ !(schExp i str) ++ ")"
372	schExtCommon i vs FileEOF [file, world]	370	schExtCommon i FileEOF [file, world]
373	= pure $ mkWorld $ "(blodwen-eof " ++ !(schExp i vs file) ++ ")"	371	= pure $ mkWorld $ "(blodwen-eof " ++ !(schExp i file) ++ ")"
374	schExtCommon i vs FileModifiedTime [file, world]	372	schExtCommon i FileModifiedTime [file, world]
375	= pure $ mkWorld $ fileOp $ "(blodwen-file-modified-time "	373	= pure $ mkWorld $ fileOp $ "(blodwen-file-modified-time "
376	++ !(schExp i vs file) ++ ")"	374	++ !(schExp i file) ++ ")"
377	schExtCommon i vs NewIORef [_, val, world]	375	schExtCommon i NewIORef [_, val, world]
378	= pure $ mkWorld $ "(box " ++ !(schExp i vs val) ++ ")"	376	= pure $ mkWorld $ "(box " ++ !(schExp i val) ++ ")"
379	schExtCommon i vs ReadIORef [_, ref, world]	377	schExtCommon i ReadIORef [_, ref, world]
380	= pure $ mkWorld $ "(unbox " ++ !(schExp i vs ref) ++ ")"	378	= pure $ mkWorld $ "(unbox " ++ !(schExp i ref) ++ ")"
381	schExtCommon i vs WriteIORef [_, ref, val, world]	379	schExtCommon i WriteIORef [_, ref, val, world]
382	= pure $ mkWorld $ "(set-box! "	380	= pure $ mkWorld $ "(set-box! "
383	++ !(schExp i vs ref) ++ " "	381	++ !(schExp i ref) ++ " "
384	++ !(schExp i vs val) ++ ")"	382	++ !(schExp i val) ++ ")"
385	schExtCommon i vs NewArray [_, size, val, world]	383	schExtCommon i NewArray [_, size, val, world]
386	= pure $ mkWorld $ "(make-vector " ++ !(schExp i vs size) ++ " "	384	= pure $ mkWorld $ "(make-vector " ++ !(schExp i size) ++ " "
387	++ !(schExp i vs val) ++ ")"	385	++ !(schExp i val) ++ ")"
388	schExtCommon i vs ArrayGet [_, arr, pos, world]	386	schExtCommon i ArrayGet [_, arr, pos, world]
389	= pure $ mkWorld $ "(vector-ref " ++ !(schExp i vs arr) ++ " "	387	= pure $ mkWorld $ "(vector-ref " ++ !(schExp i arr) ++ " "
390	++ !(schExp i vs pos) ++ ")"	388	++ !(schExp i pos) ++ ")"
391	schExtCommon i vs ArraySet [_, arr, pos, val, world]	389	schExtCommon i ArraySet [_, arr, pos, val, world]
392	= pure $ mkWorld $ "(vector-set! " ++ !(schExp i vs arr) ++ " "	390	= pure $ mkWorld $ "(vector-set! " ++ !(schExp i arr) ++ " "
393	++ !(schExp i vs pos) ++ " "	391	++ !(schExp i pos) ++ " "
394	++ !(schExp i vs val) ++ ")"	392	++ !(schExp i val) ++ ")"
395	schExtCommon i vs VoidElim [_, _]	393	schExtCommon i VoidElim [_, _]
396	= pure "(display \"Error: Executed 'void'\")"	394	= pure "(display \"Error: Executed 'void'\")"
397	schExtCommon i vs SysOS []	395	schExtCommon i SysOS []
398	= pure $ show os	396	= pure $ show os
399	schExtCommon i vs (Unknown n) args	397	schExtCommon i (Unknown n) args
400	= throw (InternalError ("Can't compile unknown external primitive " ++ show n))	398	= throw (InternalError ("Can't compile unknown external primitive " ++ show n))
401	schExtCommon i vs Stdin [] = pure "(current-input-port)"	399	schExtCommon i Stdin [] = pure "(current-input-port)"
402	schExtCommon i vs Stdout [] = pure "(current-output-port)"	400	schExtCommon i Stdout [] = pure "(current-output-port)"
403	schExtCommon i vs Stderr [] = pure "(current-error-port)"	401	schExtCommon i Stderr [] = pure "(current-error-port)"
404	schExtCommon i vs prim args	402	schExtCommon i prim args
405	= throw (InternalError ("Badly formed external primitive " ++ show prim	403	= throw (InternalError ("Badly formed external primitive " ++ show prim
406	++ " " ++ show args))	404	++ " " ++ show args))
407		405
408	schDef : {auto c : Ref Ctxt Defs} ->	406	schDef : {auto c : Ref Ctxt Defs} ->
409	Name -> CDef -> Core String	407	Name -> NamedDef -> Core String
410	schDef n (MkFun args exp)	408	schDef n (MkNmFun args exp)
411	= let vs = initSVars args in	409	= pure $ "(define " ++ schName !(getFullName n) ++ " (lambda (" ++ schArglist args ++ ") "
412	pure $ "(define " ++ schName !(getFullName n) ++ " (lambda (" ++ schArglist vs ++ ") "	410	++ !(schExp 0 exp) ++ "))\n"
413	++ !(schExp 0 vs exp) ++ "))\n"	411	schDef n (MkNmError exp)
414	schDef n (MkError exp)	412	= pure $ "(define (" ++ schName !(getFullName n) ++ " . any-args) " ++ !(schExp 0 exp) ++ ")\n"
415	= pure $ "(define (" ++ schName !(getFullName n) ++ " . any-args) " ++ !(schExp 0 [] exp) ++ ")\n"	413	schDef n (MkNmForeign _ _ _) = pure "" -- compiled by specific back end
416	schDef n (MkForeign _ _ _) = pure "" -- compiled by specific back end	414	schDef n (MkNmCon t a _) = pure "" -- Nothing to compile here
417	schDef n (MkCon t a _) = pure "" -- Nothing to compile here
418		415
419	-- Convert the name to scheme code	416	-- Convert the name to scheme code
420	-- (There may be no code generated, for example if it's a constructor)	417	-- (There may be no code generated, for example if it's a constructor)
421	export	418	export
422	getScheme : {auto c : Ref Ctxt Defs} ->	419	getScheme : {auto c : Ref Ctxt Defs} ->
423	(schExtPrim : {vars : _} -> Int -> SVars vars -> ExtPrim -> List (CExp vars) -> Core String) ->	420	(schExtPrim : Int -> ExtPrim -> List NamedCExp -> Core String) ->
424	(schString : String -> String) ->	421	(schString : String -> String) ->
425	Defs -> Name -> Core String	422	Defs -> Name -> Core String
426	getScheme schExtPrim schString defs n	423	getScheme schExtPrim schString defs n
427	= case !(lookupCtxtExact n (gamma defs)) of	424	= case !(lookupCtxtExact n (gamma defs)) of
428	Nothing => throw (InternalError ("Compiling undefined name " ++ show n))	425	Nothing => throw (InternalError ("Compiling undefined name " ++ show n))
429	Just d => case compexpr d of	426	Just d => case namedcompexpr d of
430	Nothing =>	427	Nothing =>
431	throw (InternalError ("No compiled definition for " ++ show n))	428	throw (InternalError ("No compiled definition for " ++ show n))
432	Just d => schDef schExtPrim schString n d	429	Just d => schDef schExtPrim schString n d

src/Compiler/Scheme/Racket.idr+20−16

 racketString cs = strCons '"' (showRacketString (unpack cs) "\"")
 mutual
-  racketPrim : Int -> SVars vars -> ExtPrim -> List (CExp vars) -> Core String
+  racketPrim : Int -> ExtPrim -> List NamedCExp -> Core String
-  racketPrim i vs CCall [ret, fn, args, world]
+  racketPrim i CCall [ret, fn, args, world]
       = throw (InternalError ("Can't compile C FFI calls to Racket yet"))
-  racketPrim i vs GetField [CPrimVal _ (Str s), _, _, struct,
+  racketPrim i GetField [NmPrimVal _ (Str s), _, _, struct,
-                             CPrimVal _ (Str fld), _]
+                             NmPrimVal _ (Str fld), _]
-      = do structsc <- schExp racketPrim racketString 0 vs struct
+      = do structsc <- schExp racketPrim racketString 0 struct
            pure $ "(" ++ s ++ "-" ++ fld ++ " " ++ structsc ++ ")"
-  racketPrim i vs GetField [_,_,_,_,_,_]
+  racketPrim i GetField [_,_,_,_,_,_]
       = pure "(error \"bad setField\")"
-  racketPrim i vs SetField [CPrimVal _ (Str s), _, _, struct,
+  racketPrim i SetField [NmPrimVal _ (Str s), _, _, struct,
-                             CPrimVal _ (Str fld), _, val, world]
+                         NmPrimVal _ (Str fld), _, val, world]
-      = do structsc <- schExp racketPrim racketString 0 vs struct
+      = do structsc <- schExp racketPrim racketString 0 struct
-           valsc <- schExp racketPrim racketString 0 vs val
+           valsc <- schExp racketPrim racketString 0 val
            pure $ mkWorld $
                 "(set-" ++ s ++ "-" ++ fld ++ "! " ++ structsc ++ " " ++ valsc ++ ")"
-  racketPrim i vs SetField [_,_,_,_,_,_,_,_]
+  racketPrim i SetField [_,_,_,_,_,_,_,_]
       = pure "(error \"bad setField\")"
-  racketPrim i vs SysCodegen []
+  racketPrim i SysCodegen []
       = pure $ "\"racket\""
-  racketPrim i vs prim args
+  racketPrim i prim args
-      = schExtCommon racketPrim racketString i vs prim args
+      = schExtCommon racketPrim racketString i prim args
 -- Reference label for keeping track of loaded external libraries
 data Loaded : Type where
 compileToRKT : Ref Ctxt Defs ->
                ClosedTerm -> (outfile : String) -> Core ()
 compileToRKT c tm outfile
-    = do (ns, tags) <- findUsedNames tm
+    = do cdata <- getCompileData tm
+         let ns = allNames cdata
+         let tags = nameTags cdata
+         let ctm = forget (mainExpr cdata)
          defs <- get Ctxt
          l <- newRef {t = List String} Loaded []
          s <- newRef {t = List String} Structs []
          fgndefs <- traverse getFgnCall ns
          compdefs <- traverse (getScheme racketPrim racketString defs) ns
          let code = fastAppend (map snd fgndefs ++ compdefs)
-         main <- schExp racketPrim racketString 0 [] !(compileExp tags tm)
+         main <- schExp racketPrim racketString 0 ctm
          support <- readDataFile "racket/support.rkt"
          let scm = schHeader (concat (map fst fgndefs)) ++
                    support ++ code ++

src/Core/Binary.idr+1−1

@@ -27,7 +27,7 @@ import Data.Buffer · 26 unmodified lines
27	-- TTC files can only be compatible if the version number is the same	27	-- TTC files can only be compatible if the version number is the same
28	export	28	export
29	ttcVersion : Int	29	ttcVersion : Int
30	ttcVersion = 20	30	ttcVersion = 22
31		31
32	export	32	export
33	checkTTCVersion : String -> Int -> Int -> Core ()	33	checkTTCVersion : String -> Int -> Int -> Core ()

src/Core/CaseTree.idr+15−1

 %default covering
 mutual
+  ||| Case trees in A-normal forms
+  ||| i.e. we may only dispatch on variables, not expressions
   public export
   data CaseTree : List Name -> Type where
+       ||| case x return scTy of { p1 => e1 ; ... }
        Case : {name : _} ->
               (idx : Nat) ->
               IsVar name idx vars ->
               (scTy : Term vars) -> List (CaseAlt vars) ->
               CaseTree vars
+       ||| RHS: no need for further inspection
        STerm : Term vars -> CaseTree vars
+       ||| error from a partial match
        Unmatched : (msg : String) -> CaseTree vars
+       ||| Absurd context
        Impossible : CaseTree vars
+  ||| Case alternatives. Unlike arbitrary patterns, they can be at most
+  ||| one constructor deep.
   public export
   data CaseAlt : List Name -> Type where
+       ||| Constructor for a data type; bind the arguments and subterms.
        ConCase : Name -> (tag : Int) -> (args : List Name) ->
                  CaseTree (args ++ vars) -> CaseAlt vars
+       ||| Lazy match for the Delay type use for codata types
        DelayCase : (ty : Name) -> (arg : Name) ->
                    CaseTree (ty :: arg :: vars) -> CaseAlt vars
+       ||| Match against a literal
        ConstCase : Constant -> CaseTree vars -> CaseAlt vars
+       ||| Catch-all case
        DefaultCase : CaseTree vars -> CaseAlt vars
 public export
   export
   eqTree : CaseTree vs -> CaseTree vs' -> Bool
   eqTree (Case i _ _ alts) (Case i' _ _ alts')
-      = i == i && and (map Delay (zipWith eqAlt alts alts'))
+      = i == i
+       && length alts == length alts
+       && and (zipWith (\ a, b => Delay (eqAlt a b)) alts alts')
   eqTree (STerm t) (STerm t') = eqTerm t t'
   eqTree (Unmatched _) (Unmatched _) = True
   eqTree Impossible Impossible = True

src/Core/CompileExpr.idr+300−38

@@ -19,7 +19,8 @@ mutual · 18 unmodified lines
19	-- Lambda expression	19	-- Lambda expression
20	CLam : FC -> (x : Name) -> CExp (x :: vars) -> CExp vars	20	CLam : FC -> (x : Name) -> CExp (x :: vars) -> CExp vars
21	-- Let bindings	21	-- Let bindings
22	CLet : FC -> (x : Name) -> CExp vars -> CExp (x :: vars) -> CExp vars	22	CLet : FC -> (x : Name) -> (inlineOK : Bool) -> -- Don't inline if set
		23	CExp vars -> CExp (x :: vars) -> CExp vars
23	-- Application of a defined function. The length of the argument list is	24	-- Application of a defined function. The length of the argument list is
24	-- exactly the same length as expected by its definition (so saturate with	25	-- exactly the same length as expected by its definition (so saturate with
25	-- lambdas if necessary, or overapply with additional CApps)	26	-- lambdas if necessary, or overapply with additional CApps)
@@ -53,6 +54,53 @@ mutual · 27 unmodified lines
53	data CConstAlt : List Name -> Type where	54	data CConstAlt : List Name -> Type where
54	MkConstAlt : Constant -> CExp vars -> CConstAlt vars	55	MkConstAlt : Constant -> CExp vars -> CConstAlt vars
55		56
		57	mutual
		58	\|\|\| NamedCExp - as above, but without the name index, so with explicit
		59	\|\|\| names, which are faster (but less safe) to manipulate in the inliner.
		60	\|\|\| You can, howeveer, assume that name bindings are unique - translation
		61	\|\|\| to this form (and the liner) ensure that, even if the type doesn't
		62	\|\|\| guarantee it!
		63	public export
		64	data NamedCExp : Type where
		65	NmLocal : FC -> Name -> NamedCExp
		66	NmRef : FC -> Name -> NamedCExp
		67	-- Lambda expression
		68	NmLam : FC -> (x : Name) -> NamedCExp -> NamedCExp
		69	-- Let bindings
		70	NmLet : FC -> (x : Name) -> NamedCExp -> NamedCExp -> NamedCExp
		71	-- Application of a defined function. The length of the argument list is
		72	-- exactly the same length as expected by its definition (so saturate with
		73	-- lambdas if necessary, or overapply with additional CApps)
		74	NmApp : FC -> NamedCExp -> List NamedCExp -> NamedCExp
		75	-- A saturated constructor application
		76	NmCon : FC -> Name -> (tag : Int) -> List NamedCExp -> NamedCExp
		77	-- Internally defined primitive operations
		78	NmOp : FC -> PrimFn arity -> Vect arity NamedCExp -> NamedCExp
		79	-- Externally defined primitive operations
		80	NmExtPrim : FC -> (p : Name) -> List NamedCExp -> NamedCExp
		81	-- A forced (evaluated) value
		82	NmForce : FC -> NamedCExp -> NamedCExp
		83	-- A delayed value
		84	NmDelay : FC -> NamedCExp -> NamedCExp
		85	-- A case match statement
		86	NmConCase : FC -> (sc : NamedCExp) -> List NamedConAlt -> Maybe NamedCExp -> NamedCExp
		87	NmConstCase : FC -> (sc : NamedCExp) -> List NamedConstAlt -> Maybe NamedCExp -> NamedCExp
		88	-- A primitive value
		89	NmPrimVal : FC -> Constant -> NamedCExp
		90	-- An erased value
		91	NmErased : FC -> NamedCExp
		92	-- Some sort of crash?
		93	NmCrash : FC -> String -> NamedCExp
		94
		95	public export
		96	data NamedConAlt : Type where
		97	MkNConAlt : Name -> (tag : Int) -> (args : List Name) ->
		98	NamedCExp -> NamedConAlt
		99
		100	public export
		101	data NamedConstAlt : Type where
		102	MkNConstAlt : Constant -> NamedCExp -> NamedConstAlt
		103
56	-- Argument type descriptors for foreign function calls	104	-- Argument type descriptors for foreign function calls
57	public export	105	public export
58	data CFType : Type where	106	data CFType : Type where
@@ -83,42 +131,156 @@ data CDef : Type where · 24 unmodified lines
83	-- to run, discarding arguments, no matter how many arguments are passed	131	-- to run, discarding arguments, no matter how many arguments are passed
84	MkError : CExp [] -> CDef	132	MkError : CExp [] -> CDef
85		133
		134	public export
		135	data NamedDef : Type where
		136	-- Normal function definition
		137	MkNmFun : (args : List Name) -> NamedCExp -> NamedDef
		138	-- Constructor
		139	MkNmCon : (tag : Int) -> (arity : Nat) -> (nt : Maybe Nat) -> NamedDef
		140	-- Foreign definition
		141	MkNmForeign : (ccs : List String) ->
		142	(fargs : List CFType) ->
		143	CFType ->
		144	NamedDef
		145	-- A function which will fail at runtime (usually due to being a hole) so needs
		146	-- to run, discarding arguments, no matter how many arguments are passed
		147	MkNmError : NamedCExp -> NamedDef
		148
86	mutual	149	mutual
87	export	150	export
88	Show (CExp vars) where	151	Show NamedCExp where
89	show (CLocal {x} _ y) = "!" ++ show x	152	show (NmLocal _ x) = "!" ++ show x
90	show (CRef _ x) = show x	153	show (NmRef _ x) = show x
91	show (CLam _ x y) = "(%lam " ++ show x ++ " " ++ show y ++ ")"	154	show (NmLam _ x y) = "(%lam " ++ show x ++ " " ++ show y ++ ")"
92	show (CLet _ x y z) = "(%let " ++ show x ++ " " ++ show y ++ " " ++ show z ++ ")"	155	show (NmLet _ x y z) = "(%let " ++ show x ++ " " ++ show y ++ " " ++ show z ++ ")"
93	show (CApp _ x xs)	156	show (NmApp _ x xs)
94	= assert_total $ "(" ++ show x ++ " " ++ show xs ++ ")"	157	= assert_total $ "(" ++ show x ++ " " ++ show xs ++ ")"
95	show (CCon _ x tag xs)	158	show (NmCon _ x tag xs)
96	= assert_total $ "(%con " ++ show x ++ " " ++ show tag ++ " " ++ show xs ++ ")"	159	= assert_total $ "(%con " ++ show x ++ " " ++ show tag ++ " " ++ show xs ++ ")"
97	show (COp _ op xs)	160	show (NmOp _ op xs)
98	= assert_total $ "(" ++ show op ++ " " ++ show xs ++ ")"	161	= assert_total $ "(" ++ show op ++ " " ++ show xs ++ ")"
99	show (CExtPrim _ p xs)	162	show (NmExtPrim _ p xs)
100	= assert_total $ "(%extern " ++ show p ++ " " ++ show xs ++ ")"	163	= assert_total $ "(%extern " ++ show p ++ " " ++ show xs ++ ")"
101	show (CForce _ x) = "(%force " ++ show x ++ ")"	164	show (NmForce _ x) = "(%force " ++ show x ++ ")"
102	show (CDelay _ x) = "(%delay " ++ show x ++ ")"	165	show (NmDelay _ x) = "(%delay " ++ show x ++ ")"
103	show (CConCase _ sc xs def)	166	show (NmConCase _ sc xs def)
104	= assert_total $ "(%case " ++ show sc ++ " " ++ show xs ++ " " ++ show def ++ ")"	167	= assert_total $ "(%case " ++ show sc ++ " " ++ show xs ++ " " ++ show def ++ ")"
105	show (CConstCase _ sc xs def)	168	show (NmConstCase _ sc xs def)
106	= assert_total $ "(%case " ++ show sc ++ " " ++ show xs ++ " " ++ show def ++ ")"	169	= assert_total $ "(%case " ++ show sc ++ " " ++ show xs ++ " " ++ show def ++ ")"
107	show (CPrimVal _ x) = show x	170	show (NmPrimVal _ x) = show x
108	show (CErased _) = "___"	171	show (NmErased _) = "___"
109	show (CCrash _ x) = "(CRASH " ++ show x ++ ")"	172	show (NmCrash _ x) = "(CRASH " ++ show x ++ ")"
110		173
111	export	174	export
112	Show (CConAlt vars) where	175	Show NamedConAlt where
113	show (MkConAlt x tag args exp)	176	show (MkNConAlt x tag args exp)
114	= "(%concase " ++ show x ++ " " ++ show tag ++ " " ++	177	= "(%concase " ++ show x ++ " " ++ show tag ++ " " ++
115	show args ++ " " ++ show exp ++ ")"	178	show args ++ " " ++ show exp ++ ")"
116		179
117	export	180	export
118	Show (CConstAlt vars) where	181	Show NamedConstAlt where
119	show (MkConstAlt x exp)	182	show (MkNConstAlt x exp)
120	= "(%constcase " ++ show x ++ " " ++ show exp ++ ")"	183	= "(%constcase " ++ show x ++ " " ++ show exp ++ ")"
121		184
		185	export
		186	data Names : List Name -> Type where
		187	Nil : Names []
		188	(::) : Name -> Names xs -> Names (x :: xs)
		189
		190	elem : Name -> Names xs -> Bool
		191	elem n [] = False
		192	elem n (x :: xs) = if n == x then True else elem n xs
		193
		194	tryNext : Name -> Name
		195	tryNext (UN n) = MN n 0
		196	tryNext (MN n i) = MN n (1 + i)
		197	tryNext n = MN (nameRoot n) 0
		198
		199	uniqueName : Name -> Names vs -> Name
		200	uniqueName s ns =
		201	if s `elem` ns
		202	then uniqueName (tryNext s) ns
		203	else s
		204
		205	export
		206	getLocName : (idx : Nat) -> Names vars -> .(IsVar name idx vars) -> Name
		207	getLocName Z (x :: xs) First = x
		208	getLocName (S k) (x :: xs) (Later p) = getLocName k xs p
		209
		210	export
		211	addLocs : (args : List Name) -> Names vars -> Names (args ++ vars)
		212	addLocs [] ns = ns
		213	addLocs (x :: xs) ns
		214	= let rec = addLocs xs ns in
		215	uniqueName x rec :: rec
		216
		217	conArgs : (args : List Name) -> Names (args ++ vars) -> List Name
		218	conArgs [] ns = []
		219	conArgs (a :: as) (n :: ns) = n :: conArgs as ns
		220
		221	mutual
		222	forgetExp : Names vars -> CExp vars -> NamedCExp
		223	forgetExp locs (CLocal fc p) = NmLocal fc (getLocName _ locs p)
		224	forgetExp locs (CRef fc n) = NmRef fc n
		225	forgetExp locs (CLam fc x sc)
		226	= let locs' = addLocs [x] locs in
		227	NmLam fc (getLocName _ locs' First) (forgetExp locs' sc)
		228	forgetExp locs (CLet fc x _ val sc)
		229	= let locs' = addLocs [x] locs in
		230	NmLet fc (getLocName _ locs' First)
		231	(forgetExp locs val)
		232	(forgetExp locs' sc)
		233	forgetExp locs (CApp fc f args)
		234	= NmApp fc (forgetExp locs f) (map (forgetExp locs) args)
		235	forgetExp locs (CCon fc n t args)
		236	= NmCon fc n t (map (forgetExp locs) args)
		237	forgetExp locs (COp fc op args)
		238	= NmOp fc op (map (forgetExp locs) args)
		239	forgetExp locs (CExtPrim fc p args)
		240	= NmExtPrim fc p (map (forgetExp locs) args)
		241	forgetExp locs (CForce fc f)
		242	= NmForce fc (forgetExp locs f)
		243	forgetExp locs (CDelay fc f)
		244	= NmDelay fc (forgetExp locs f)
		245	forgetExp locs (CConCase fc sc alts def)
		246	= NmConCase fc (forgetExp locs sc) (map (forgetConAlt locs) alts)
		247	(map (forgetExp locs) def)
		248	forgetExp locs (CConstCase fc sc alts def)
		249	= NmConstCase fc (forgetExp locs sc) (map (forgetConstAlt locs) alts)
		250	(map (forgetExp locs) def)
		251	forgetExp locs (CPrimVal fc c) = NmPrimVal fc c
		252	forgetExp locs (CErased fc) = NmErased fc
		253	forgetExp locs (CCrash fc msg) = NmCrash fc msg
		254
		255	forgetConAlt : Names vars -> CConAlt vars -> NamedConAlt
		256	forgetConAlt locs (MkConAlt n t args exp)
		257	= let args' = addLocs args locs in
		258	MkNConAlt n t (conArgs args args') (forgetExp args' exp)
		259
		260	forgetConstAlt : Names vars -> CConstAlt vars -> NamedConstAlt
		261	forgetConstAlt locs (MkConstAlt c exp)
		262	= MkNConstAlt c (forgetExp locs exp)
		263
		264	export
		265	forget : {vars : _} -> CExp vars -> NamedCExp
		266	forget {vars} exp
		267	= forgetExp (addLocs vars [])
		268	(rewrite appendNilRightNeutral vars in exp)
		269
		270	export
		271	forgetDef : CDef -> NamedDef
		272	forgetDef (MkFun args def)
		273	= let ns = addLocs args []
		274	args' = conArgs args ns in
		275	MkNmFun args' (forget def)
		276	forgetDef (MkCon t a nt) = MkNmCon t a nt
		277	forgetDef (MkForeign ccs fargs ty) = MkNmForeign ccs fargs ty
		278	forgetDef (MkError err) = MkNmError (forget err)
		279
		280	export
		281	Show (CExp vars) where
		282	show exp = show (forget exp)
		283
122	export	284	export
123	Show CFType where	285	Show CFType where
124	show CFUnit = "Unit"	286	show CFUnit = "Unit"
@@ -144,19 +306,30 @@ Show CDef where · 19 unmodified lines
144	show args ++ " -> " ++ show ret	306	show args ++ " -> " ++ show ret
145	show (MkError exp) = "Error: " ++ show exp	307	show (MkError exp) = "Error: " ++ show exp
146		308
		309	export
		310	Show NamedDef where
		311	show (MkNmFun args exp) = show args ++ ": " ++ show exp
		312	show (MkNmCon tag arity pos)
		313	= "Constructor tag " ++ show tag ++ " arity " ++ show arity ++
		314	maybe "" (\n => " (newtype by " ++ show n ++ ")") pos
		315	show (MkNmForeign ccs args ret)
		316	= "Foreign call " ++ show ccs ++ " " ++
		317	show args ++ " -> " ++ show ret
		318	show (MkNmError exp) = "Error: " ++ show exp
		319
147	mutual	320	mutual
148	export	321	export
149	thin : (n : Name) -> CExp (outer ++ inner) -> CExp (outer ++ n :: inner)	322	thin : (n : Name) -> CExp (outer ++ inner) -> CExp (outer ++ n :: inner)
150	thin n (CLocal fc prf)	323	thin n (CLocal fc prf)
151	= let MkVar var' = insertVar {n} _ prf in	324	= let MkNVar var' = insertNVar {n} _ prf in
152	CLocal fc var'	325	CLocal fc var'
153	thin _ (CRef fc x) = CRef fc x	326	thin _ (CRef fc x) = CRef fc x
154	thin {outer} {inner} n (CLam fc x sc)	327	thin {outer} {inner} n (CLam fc x sc)
155	= let sc' = thin {outer = x :: outer} {inner} n sc in	328	= let sc' = thin {outer = x :: outer} {inner} n sc in
156	CLam fc x sc'	329	CLam fc x sc'
157	thin {outer} {inner} n (CLet fc x val sc)	330	thin {outer} {inner} n (CLet fc x inl val sc)
158	= let sc' = thin {outer = x :: outer} {inner} n sc in	331	= let sc' = thin {outer = x :: outer} {inner} n sc in
159	CLet fc x (thin n val) sc'	332	CLet fc x inl (thin n val) sc'
160	thin n (CApp fc x xs)	333	thin n (CApp fc x xs)
161	= CApp fc (thin n x) (assert_total (map (thin n) xs))	334	= CApp fc (thin n x) (assert_total (map (thin n) xs))
162	thin n (CCon fc x tag xs)	335	thin n (CCon fc x tag xs)
@@ -194,15 +367,15 @@ mutual · 31 unmodified lines
194	(ns : List Name) -> CExp (outer ++ inner) ->	367	(ns : List Name) -> CExp (outer ++ inner) ->
195	CExp (outer ++ (ns ++ inner))	368	CExp (outer ++ (ns ++ inner))
196	insertNames ns (CLocal fc prf)	369	insertNames ns (CLocal fc prf)
197	= let MkVar var' = insertVarNames {ns} _ prf in	370	= let MkNVar var' = insertNVarNames {ns} _ prf in
198	CLocal fc var'	371	CLocal fc var'
199	insertNames _ (CRef fc x) = CRef fc x	372	insertNames _ (CRef fc x) = CRef fc x
200	insertNames {outer} {inner} ns (CLam fc x sc)	373	insertNames {outer} {inner} ns (CLam fc x sc)
201	= let sc' = insertNames {outer = x :: outer} {inner} ns sc in	374	= let sc' = insertNames {outer = x :: outer} {inner} ns sc in
202	CLam fc x sc'	375	CLam fc x sc'
203	insertNames {outer} {inner} ns (CLet fc x val sc)	376	insertNames {outer} {inner} ns (CLet fc x inl val sc)
204	= let sc' = insertNames {outer = x :: outer} {inner} ns sc in	377	= let sc' = insertNames {outer = x :: outer} {inner} ns sc in
205	CLet fc x (insertNames ns val) sc'	378	CLet fc x inl (insertNames ns val) sc'
206	insertNames ns (CApp fc x xs)	379	insertNames ns (CApp fc x xs)
207	= CApp fc (insertNames ns x) (assert_total (map (insertNames ns) xs))	380	= CApp fc (insertNames ns x) (assert_total (map (insertNames ns) xs))
208	insertNames ns (CCon fc x tag xs)	381	insertNames ns (CCon fc x tag xs)
@@ -244,7 +417,7 @@ mutual · 35 unmodified lines
244	embed (CLocal fc prf) = CLocal fc (varExtend prf)	417	embed (CLocal fc prf) = CLocal fc (varExtend prf)
245	embed (CRef fc n) = CRef fc n	418	embed (CRef fc n) = CRef fc n
246	embed (CLam fc x sc) = CLam fc x (embed sc)	419	embed (CLam fc x sc) = CLam fc x (embed sc)
247	embed (CLet fc x val sc) = CLet fc x (embed val) (embed sc)	420	embed (CLet fc x inl val sc) = CLet fc x inl (embed val) (embed sc)
248	embed (CApp fc f args) = CApp fc (embed f) (assert_total (map embed args))	421	embed (CApp fc f args) = CApp fc (embed f) (assert_total (map embed args))
249	embed (CCon fc n t args) = CCon fc n t (assert_total (map embed args))	422	embed (CCon fc n t args) = CCon fc n t (assert_total (map embed args))
250	embed (COp fc p args) = COp fc p (assert_total (map embed args))	423	embed (COp fc p args) = COp fc p (assert_total (map embed args))
@@ -282,9 +455,9 @@ mutual · 31 unmodified lines
282	shrinkCExp sub (CLam fc x sc)	455	shrinkCExp sub (CLam fc x sc)
283	= let sc' = shrinkCExp (KeepCons sub) sc in	456	= let sc' = shrinkCExp (KeepCons sub) sc in
284	CLam fc x sc'	457	CLam fc x sc'
285	shrinkCExp sub (CLet fc x val sc)	458	shrinkCExp sub (CLet fc x inl val sc)
286	= let sc' = shrinkCExp (KeepCons sub) sc in	459	= let sc' = shrinkCExp (KeepCons sub) sc in
287	CLet fc x (shrinkCExp sub val) sc'	460	CLet fc x inl (shrinkCExp sub val) sc'
288	shrinkCExp sub (CApp fc x xs)	461	shrinkCExp sub (CApp fc x xs)
289	= CApp fc (shrinkCExp sub x) (assert_total (map (shrinkCExp sub) xs))	462	= CApp fc (shrinkCExp sub x) (assert_total (map (shrinkCExp sub) xs))
290	shrinkCExp sub (CCon fc x tag xs)	463	shrinkCExp sub (CCon fc x tag xs)
@@ -321,11 +494,12 @@ Weaken CExp where · 30 unmodified lines
321		494
322	-- Substitute some explicit terms for names in a term, and remove those	495	-- Substitute some explicit terms for names in a term, and remove those
323	-- names from the scope	496	-- names from the scope
324	public export	497	namespace SubstCEnv
325	data SubstCEnv : List Name -> List Name -> Type where	498	public export
326	Nil : SubstCEnv [] vars	499	data SubstCEnv : List Name -> List Name -> Type where
327	(::) : CExp vars ->	500	Nil : SubstCEnv [] vars
328	SubstCEnv ds vars -> SubstCEnv (d :: ds) vars	501	(::) : CExp vars ->
		502	SubstCEnv ds vars -> SubstCEnv (d :: ds) vars
329		503
330	findDrop : {drop : _} -> {idx : Nat} ->	504	findDrop : {drop : _} -> {idx : Nat} ->
331	FC -> .(IsVar name idx (drop ++ vars)) ->	505	FC -> .(IsVar name idx (drop ++ vars)) ->
@@ -352,9 +526,9 @@ mutual · 20 unmodified lines
352	substEnv {outer} env (CLam fc x sc)	526	substEnv {outer} env (CLam fc x sc)
353	= let sc' = substEnv {outer = x :: outer} env sc in	527	= let sc' = substEnv {outer = x :: outer} env sc in
354	CLam fc x sc'	528	CLam fc x sc'
355	substEnv {outer} env (CLet fc x val sc)	529	substEnv {outer} env (CLet fc x inl val sc)
356	= let sc' = substEnv {outer = x :: outer} env sc in	530	= let sc' = substEnv {outer = x :: outer} env sc in
357	CLet fc x (substEnv env val) sc'	531	CLet fc x inl (substEnv env val) sc'
358	substEnv env (CApp fc x xs)	532	substEnv env (CApp fc x xs)
359	= CApp fc (substEnv env x) (assert_total (map (substEnv env) xs))	533	= CApp fc (substEnv env x) (assert_total (map (substEnv env) xs))
360	substEnv env (CCon fc x tag xs)	534	substEnv env (CCon fc x tag xs)
@@ -394,12 +568,81 @@ export · 33 unmodified lines
394	substs : SubstCEnv drop vars -> CExp (drop ++ vars) -> CExp vars	568	substs : SubstCEnv drop vars -> CExp (drop ++ vars) -> CExp vars
395	substs env tm = substEnv {outer = []} env tm	569	substs env tm = substEnv {outer = []} env tm
396		570
		571	resolveRef : (done : List Name) -> Bounds bound -> FC -> Name ->
		572	Maybe (CExp (later ++ (done ++ bound ++ vars)))
		573	resolveRef done None fc n = Nothing
		574	resolveRef {later} {vars} done (Add {xs} new old bs) fc n
		575	= if n == old
		576	then rewrite appendAssociative later done (new :: xs ++ vars) in
		577	let MkNVar p = weakenNVar {inner = new :: xs ++ vars}
		578	(later ++ done) First in
		579	Just (CLocal fc p)
		580	else rewrite appendAssociative done [new] (xs ++ vars)
		581	in resolveRef (done ++ [new]) bs fc n
		582
		583	mutual
		584	export
		585	mkLocals : {later, vars : _} ->
		586	Bounds bound ->
		587	CExp (later ++ vars) -> CExp (later ++ (bound ++ vars))
		588	mkLocals bs (CLocal {idx} {x} fc p)
		589	= let MkNVar p' = addVars bs p in CLocal {x} fc p'
		590	mkLocals {later} {vars} bs (CRef fc var)
		591	= maybe (CRef fc var) id (resolveRef [] bs fc var)
		592	mkLocals {later} {vars} bs (CLam fc x sc)
		593	= let sc' = mkLocals bs {later = x :: later} {vars} sc in
		594	CLam fc x sc'
		595	mkLocals {later} {vars} bs (CLet fc x inl val sc)
		596	= let sc' = mkLocals bs {later = x :: later} {vars} sc in
		597	CLet fc x inl (mkLocals bs val) sc'
		598	mkLocals bs (CApp fc f xs)
		599	= CApp fc (mkLocals bs f) (assert_total (map (mkLocals bs) xs))
		600	mkLocals bs (CCon fc x tag xs)
		601	= CCon fc x tag (assert_total (map (mkLocals bs) xs))
		602	mkLocals bs (COp fc x xs)
		603	= COp fc x (assert_total (map (mkLocals bs) xs))
		604	mkLocals bs (CExtPrim fc x xs)
		605	= CExtPrim fc x (assert_total (map (mkLocals bs) xs))
		606	mkLocals bs (CForce fc x)
		607	= CForce fc (mkLocals bs x)
		608	mkLocals bs (CDelay fc x)
		609	= CDelay fc (mkLocals bs x)
		610	mkLocals bs (CConCase fc sc xs def)
		611	= CConCase fc (mkLocals bs sc)
		612	(assert_total (map (mkLocalsConAlt bs) xs))
		613	(assert_total (map (mkLocals bs) def))
		614	mkLocals bs (CConstCase fc sc xs def)
		615	= CConstCase fc (mkLocals bs sc)
		616	(assert_total (map (mkLocalsConstAlt bs) xs))
		617	(assert_total (map (mkLocals bs) def))
		618	mkLocals bs (CPrimVal fc x) = CPrimVal fc x
		619	mkLocals bs (CErased fc) = CErased fc
		620	mkLocals bs (CCrash fc x) = CCrash fc x
		621
		622	mkLocalsConAlt : Bounds bound ->
		623	CConAlt (later ++ vars) -> CConAlt (later ++ (bound ++ vars))
		624	mkLocalsConAlt {bound} {later} {vars} bs (MkConAlt x tag args sc)
		625	= let sc' : CExp ((args ++ later) ++ vars)
		626	= rewrite sym (appendAssociative args later vars) in sc in
		627	MkConAlt x tag args
		628	(rewrite appendAssociative args later (bound ++ vars) in
		629	mkLocals bs sc')
		630
		631	mkLocalsConstAlt : Bounds bound ->
		632	CConstAlt (later ++ vars) -> CConstAlt (later ++ (bound ++ vars))
		633	mkLocalsConstAlt bs (MkConstAlt x sc) = MkConstAlt x (mkLocals bs sc)
		634
		635	export
		636	refsToLocals : Bounds bound -> CExp vars -> CExp (bound ++ vars)
		637	refsToLocals None tm = tm
		638	refsToLocals bs y = mkLocals {later = []} bs y
		639
397	export	640	export
398	getFC : CExp args -> FC	641	getFC : CExp args -> FC
399	getFC (CLocal fc _) = fc	642	getFC (CLocal fc _) = fc
400	getFC (CRef fc _) = fc	643	getFC (CRef fc _) = fc
401	getFC (CLam fc _ _) = fc	644	getFC (CLam fc _ _) = fc
402	getFC (CLet fc _ _ _) = fc	645	getFC (CLet fc _ _ _ _) = fc
403	getFC (CApp fc _ _) = fc	646	getFC (CApp fc _ _) = fc
404	getFC (CCon fc _ _ _) = fc	647	getFC (CCon fc _ _ _) = fc
405	getFC (COp fc _ _) = fc	648	getFC (COp fc _ _) = fc
@@ -411,3 +654,22 @@ getFC (CConstCase fc _ _ _) = fc · 5 unmodified lines
411	getFC (CPrimVal fc _) = fc	654	getFC (CPrimVal fc _) = fc
412	getFC (CErased fc) = fc	655	getFC (CErased fc) = fc
413	getFC (CCrash fc _) = fc	656	getFC (CCrash fc _) = fc
		657
		658	namespace NamedCExp
		659	export
		660	getFC : NamedCExp -> FC
		661	getFC (NmLocal fc _) = fc
		662	getFC (NmRef fc _) = fc
		663	getFC (NmLam fc _ _) = fc
		664	getFC (NmLet fc _ _ _) = fc
		665	getFC (NmApp fc _ _) = fc
		666	getFC (NmCon fc _ _ _) = fc
		667	getFC (NmOp fc _ _) = fc
		668	getFC (NmExtPrim fc _ _) = fc
		669	getFC (NmForce fc _) = fc
		670	getFC (NmDelay fc _) = fc
		671	getFC (NmConCase fc _ _ _) = fc
		672	getFC (NmConstCase fc _ _ _) = fc
		673	getFC (NmPrimVal fc _) = fc
		674	getFC (NmErased fc) = fc
		675	getFC (NmCrash fc _) = fc

src/Core/Context.idr+21−4

                  Def
     Builtin : {arity : Nat} -> PrimFn arity -> Def
     DCon : (tag : Int) -> (arity : Nat) ->
-           (newtypeArg : Maybe Nat) -> -- if only constructor, and only one
+           (newtypeArg : Maybe (Bool, Nat)) ->
-                                       -- argument is non-Rig0, flag it here,
+               -- if only constructor, and only one argument is non-Rig0,
+               -- flag it here. The Nat is the unerased argument position.
+               -- The Bool is 'True' if there is no %World token in the
+               -- structure, which means it is safe to completely erase
+               -- when pattern matching (otherwise we still have to ensure
+               -- that the value is inspected, to make sure external effects
+               -- happen)
            Def -- data constructor
     TCon : (tag : Int) -> (arity : Nat) ->
            (parampos : List Nat) -> -- parameters
   linearChecked : Bool -- Flag whether we've already checked its linearity
   definition : Def
   compexpr : Maybe CDef
+  namedcompexpr : Maybe NamedDef
   sizeChange : List SCCall
 export
 newDef fc n rig vars ty vis def
     = MkGlobalDef fc n ty [] [] []
                   rig vars vis unchecked [] Nothing Nothing False False False def
-                  Nothing []
+                  Nothing Nothing []
 -- Rewrite rules, applied after type checking, for runtime code only
 -- LHS and RHS must have the same type, but we don't (currently) require that
     = do addDef n (MkGlobalDef emptyFC n ty [] [] [] RigW [] Public tot
                                [Inline] Nothing Nothing
                                False False True (Builtin op)
-                               Nothing [])
+                               Nothing Nothing [])
          pure ()
 export
          addDef n (record { compexpr = Just cexp } gdef)
          pure ()
+export
+setNamedCompiled : {auto c : Ref Ctxt Defs} ->
+                   Name -> NamedDef -> Core ()
+setNamedCompiled n cexp
+    = do defs <- get Ctxt
+         Just gdef <- lookupCtxtExact n (gamma defs)
+              | Nothing => pure ()
+         addDef n (record { namedcompexpr = Just cexp } gdef)
+         pure ()
 -- Record that the name has been linearity checked so we don't need to do
 -- it again
 export

src/Core/Env.idr+3−7

                  {idx : Nat} ->
                  (ns : List Name) ->
                  .(IsVar x idx vars) -> Env tm vars ->
-                 Binder (tm (reverse ns ++ vars))
+                 Binder (tm (reverseOnto vars ns))
 getBinderUnder {idx = Z} {vars = v :: vs} ns First (b :: env)
-    = rewrite appendAssociative (reverse ns) [v] vs in
+    = rewrite revOnto vs (v :: ns) in map (weakenNs (reverse (v :: ns))) b
-			 rewrite revNs [v] ns in
-         map (weakenNs (reverse (v :: ns))) b
 getBinderUnder {idx = S k} {vars = v :: vs} ns (Later lp) (b :: env)
-    = rewrite appendAssociative (reverse ns) [v] vs in
+    = getBinderUnder (v :: ns) lp env
-			 rewrite revNs [v] ns in
-         getBinderUnder (v :: ns) lp env
 export
 getBinder : Weaken tm =>

src/Core/LinearCheck.idr+3−3

@@ -188,9 +188,9 @@ mutual · 187 unmodified lines
188	getName (x :: xs) (Later p) = getName xs p	188	getName (x :: xs) (Later p) = getName xs p
189		189
190	rigSafe : RigCount -> RigCount -> Core ()	190	rigSafe : RigCount -> RigCount -> Core ()
191	rigSafe Rig1 RigW = throw (LinearMisuse fc (getName vars prf) Rig1 RigW)	191	rigSafe Rig1 RigW = throw (LinearMisuse fc name Rig1 RigW)
192	rigSafe Rig0 RigW = throw (LinearMisuse fc (getName vars prf) Rig0 RigW)	192	rigSafe Rig0 RigW = throw (LinearMisuse fc name Rig0 RigW)
193	rigSafe Rig0 Rig1 = throw (LinearMisuse fc (getName vars prf) Rig0 Rig1)	193	rigSafe Rig0 Rig1 = throw (LinearMisuse fc name Rig0 Rig1)
194	rigSafe _ _ = pure ()	194	rigSafe _ _ = pure ()
195		195
196	-- count the usage if we're in a linear context. If not, the usage doesn't	196	-- count the usage if we're in a linear context. If not, the usage doesn't

src/Core/Name.idr+1−1

@@ -56,7 +56,7 @@ showSep sep (x :: xs) = x ++ sep ++ showSep sep xs · 55 unmodified lines
56	\|\|\| Check whether a given character is a valid identifier character	56	\|\|\| Check whether a given character is a valid identifier character
57	export	57	export
58	identChar : Char -> Bool	58	identChar : Char -> Bool
59	identChar x = isAlphaNum x \|\| x == '_' \|\| x == '\''	59	identChar x = isAlphaNum x \|\| x == '_' \|\| x == '\'' \|\| x > chr 127
60		60
61	export Show Name where	61	export Show Name where
62	show (NS ns n) = showSep "." (reverse ns) ++ "." ++ show n	62	show (NS ns n) = showSep "." (reverse ns) ++ "." ++ show n

src/Core/Normalise.idr+75−92

     eval env locs (Local fc mrig idx prf) stk
         = evalLocal env fc mrig idx prf stk locs
     eval env locs (Ref fc nt fn) stk
-        = evalRef env locs False fc nt fn stk (NApp fc (NRef nt fn) stk)
+        = evalRef env False fc nt fn stk (NApp fc (NRef nt fn) stk)
     eval {vars} {free} env locs (Meta fc name idx args) stk
-        = evalMeta env locs fc name idx (closeArgs args) stk
+        = evalMeta env fc name idx (closeArgs args) stk
       where
         -- Yes, it's just a map, but specialising it by hand since we
         -- use this a *lot* and it saves the run time overhead of making
     eval env locs (Erased fc i) stk = pure $ NErased fc i
     eval env locs (TType fc) stk = pure $ NType fc
-    evalLocal : {vars : _} ->
+    evalLocClosure : Env Term free ->
-                Env Term free ->
+                     FC -> Maybe Bool ->
-                FC -> Maybe Bool ->
+                     Stack free ->
-                (idx : Nat) -> .(IsVar name idx (vars ++ free)) ->
+                     Closure free ->
-                Stack free ->
+                     Core (NF free)
-                LocalEnv free vars ->
+    evalLocClosure env fc mrig stk (MkClosure opts locs' env' tm')
-                Core (NF free)
-    evalLocal {vars = []} env fc mrig idx prf stk locs
-        = if not (holesOnly topopts || argHolesOnly topopts) && isLet mrig idx env
-             then
-               case getBinder prf env of
-                    Let _ val _ => eval env [] val stk
-                    _ => pure $ NApp fc (NLocal mrig idx prf) stk
-             else pure $ NApp fc (NLocal mrig idx prf) stk
-      where
-        isLet' : Nat -> Env tm vars -> Bool
-        isLet' Z (Let _ _ _ :: env) = True
-        isLet' Z _ = False
-        isLet' (S k) (b :: env) = isLet' k env
-        isLet' (S k) [] = False
-        isLet : Maybe Bool -> Nat -> Env tm vars -> Bool
-        isLet (Just t) _ _ = t
-        isLet _ n env = isLet' n env
-    evalLocal env fc mrig Z First stk (MkClosure opts locs' env' tm' :: locs)
         = evalWithOpts defs opts env' locs' tm' stk
-    evalLocal {free} {vars = x :: xs}
+    evalLocClosure {free} env fc mrig stk (MkNFClosure nf)
-              env fc mrig Z First stk (MkNFClosure nf :: locs)
         = applyToStack nf stk
       where
         applyToStack : NF free -> Stack free -> Core (NF free)
             = do arg' <- sc defs arg
                  applyToStack arg' stk
         applyToStack (NApp fc (NRef nt fn) args) stk
-            = evalRef {vars = xs} env locs False fc nt fn (args ++ stk)
+            = evalRef env False fc nt fn (args ++ stk)
                       (NApp fc (NRef nt fn) args)
         applyToStack (NApp fc (NLocal mrig idx p) args) stk
-          = let MkVar p' = insertVarNames {outer=[]} {ns = xs} idx p in
+          = evalLocal env fc mrig _ p (args ++ stk) []
-               evalLocal env fc mrig _ p' (args ++ stk) locs
         applyToStack (NDCon fc n t a args) stk
             = pure $ NDCon fc n t a (args ++ stk)
         applyToStack (NTCon fc n t a args) stk
             = pure $ NTCon fc n t a (args ++ stk)
         applyToStack nf _ = pure nf
+    evalLocal : {vars : _} ->
+                Env Term free ->
+                FC -> Maybe Bool ->
+                (idx : Nat) -> .(IsVar name idx (vars ++ free)) ->
+                Stack free ->
+                LocalEnv free vars ->
+                Core (NF free)
+    -- If it's one of the free variables, we are done unless the free
+    -- variable maps to a let-binding
+    evalLocal {vars = []} env fc mrig idx prf stk locs
+        = if not (holesOnly topopts || argHolesOnly topopts)
+             -- if we know it's not a let, no point in even running `getBinder`
+             && fromMaybe True mrig
+             then
+               case getBinder prf env of
+                    Let _ val _ => eval env [] val stk
+                    _ => pure $ NApp fc (NLocal mrig idx prf) stk
+             else pure $ NApp fc (NLocal mrig idx prf) stk
+    evalLocal env fc mrig Z First stk (x :: locs)
+        = evalLocClosure env fc mrig stk x
     evalLocal {vars = x :: xs} {free}
               env fc mrig (S idx) (Later p) stk (_ :: locs)
         = evalLocal {vars = xs} env fc mrig idx p stk locs
-    evalMeta : {vars : _} ->
+    evalMeta : Env Term free ->
-               Env Term free -> LocalEnv free vars ->
                FC -> Name -> Int -> List (Closure free) ->
                Stack free -> Core (NF free)
-    evalMeta {vars} env locs fc nm i args stk
+    evalMeta env fc nm i args stk
-        = evalRef env locs True fc Func (Resolved i) (args ++ stk)
+        = evalRef env True fc Func (Resolved i) (args ++ stk)
                   (NApp fc (NMeta nm i args) stk)
-    evalRef : {vars : _} ->
+    evalRef : Env Term free ->
-              Env Term free -> LocalEnv free vars ->
               (isMeta : Bool) ->
               FC -> NameType -> Name -> Stack free -> (def : Lazy (NF free)) ->
               Core (NF free)
-    evalRef env locs meta fc (DataCon tag arity) fn stk def
+    evalRef env meta fc (DataCon tag arity) fn stk def
         = pure $ NDCon fc fn tag arity stk
-    evalRef env locs meta fc (TyCon tag arity) fn stk def
+    evalRef env meta fc (TyCon tag arity) fn stk def
         = pure $ NTCon fc fn tag arity stk
-    evalRef env locs meta fc Bound fn stk def
+    evalRef env meta fc Bound fn stk def
         = pure def
-    evalRef env locs meta fc nt n stk def
+    evalRef env meta fc nt n stk def
         = do Just res <- lookupCtxtExact n (gamma defs)
                   | Nothing => pure def
              let redok = evalAll topopts ||
                    opts' <- if noCycles res
                                then useMeta fc n defs topopts
                                else pure topopts
-                   evalDef env locs opts' meta fc
+                   evalDef env opts' meta fc
                            (multiplicity res) (definition res) (flags res) stk def
                 else pure def
     getCaseBound : List (Closure free) ->
                    (args : List Name) ->
-                   LocalEnv free vars ->
+                   LocalEnv free more ->
-                   Maybe (LocalEnv free (args ++ vars))
+                   Maybe (LocalEnv free (args ++ more))
-    getCaseBound [] [] loc = Just loc
+    getCaseBound []            []        loc = Just loc
-    getCaseBound [] (x :: xs) loc = Nothing -- mismatched arg length
+    getCaseBound []            (_ :: _)  loc = Nothing -- mismatched arg length
-    getCaseBound (arg :: args) [] loc = Nothing -- mismatched arg length
+    getCaseBound (arg :: args) []        loc = Nothing -- mismatched arg length
-    getCaseBound (arg :: args) (n :: ns) loc
+    getCaseBound (arg :: args) (n :: ns) loc = (arg ::) <$> getCaseBound args ns loc
-         = do loc' <- getCaseBound args ns loc
-              pure (arg :: loc')
     evalConAlt : Env Term free ->
-                 LocalEnv free (more ++ vars) -> EvalOpts -> FC ->
+                 LocalEnv free more -> EvalOpts -> FC ->
                  Stack free ->
                  (args : List Name) ->
                  List (Closure free) ->
                  CaseTree (args ++ more) ->
                  (default : Core (NF free)) ->
                  Core (NF free)
-    evalConAlt {more} {vars} env loc opts fc stk args args' sc def
+    evalConAlt env loc opts fc stk args args' sc def
-         = maybe def (\bound =>
+         = maybe def (\bound => evalTree env bound opts fc stk sc def)
-                            let loc' : LocalEnv _ ((args ++ more) ++ vars)
-                                = rewrite sym (appendAssociative args more vars) in
-                                          bound in
-                                evalTree env loc' opts fc stk sc def)
                      (getCaseBound args' args loc)
     tryAlt : Env Term free ->
-             LocalEnv free (more ++ vars) -> EvalOpts -> FC ->
+             LocalEnv free more -> EvalOpts -> FC ->
              Stack free -> NF free -> CaseAlt more ->
              (default : Core (NF free)) -> Core (NF free)
     -- Ordinary constructor matching
-    tryAlt {more} {vars} env loc opts fc stk (NDCon _ nm tag' arity args') (ConCase x tag args sc) def
+    tryAlt {more} env loc opts fc stk (NDCon _ nm tag' arity args') (ConCase x tag args sc) def
          = if tag == tag'
               then evalConAlt env loc opts fc stk args args' sc def
               else def
     -- Type constructor matching, in typecase
-    tryAlt {more} {vars} env loc opts fc stk (NTCon _ nm tag' arity args') (ConCase nm' tag args sc) def
+    tryAlt {more} env loc opts fc stk (NTCon _ nm tag' arity args') (ConCase nm' tag args sc) def
          = if nm == nm'
               then evalConAlt env loc opts fc stk args args' sc def
               else def
     tryAlt env loc opts fc stk (NType _) (ConCase (UN "Type") tag [] sc) def
          = evalTree env loc opts fc stk sc def
     -- Arrow matching, in typecase
-    tryAlt {more} {vars}
+    tryAlt {more}
            env loc opts fc stk (NBind pfc x (Pi r e aty) scty) (ConCase (UN "->") tag [s,t] sc) def
-       = evalConAlt {more} {vars} env loc opts fc stk [s,t]
+       = evalConAlt {more} env loc opts fc stk [s,t]
                   [MkNFClosure aty,
                    MkNFClosure (NBind pfc x (Lam r e aty) scty)]
                   sc def
     tryAlt _ _ _ _ _ _ _ def = def
     findAlt : Env Term free ->
-              LocalEnv free (args ++ vars) -> EvalOpts -> FC ->
+              LocalEnv free args -> EvalOpts -> FC ->
               Stack free -> NF free -> List (CaseAlt args) ->
               (default : Core (NF free)) -> Core (NF free)
     findAlt env loc opts fc stk val [] def = def
     findAlt env loc opts fc stk val (x :: xs) def
          = tryAlt env loc opts fc stk val x (findAlt env loc opts fc stk val xs def)
-    evalTree : {vars : _} ->
+    evalTree : Env Term free -> LocalEnv free args ->
-               Env Term free -> LocalEnv free (args ++ vars) ->
                EvalOpts -> FC ->
                Stack free -> CaseTree args ->
                (default : Core (NF free)) -> Core (NF free)
-    evalTree {args} {vars} {free} env loc opts fc stk (Case idx x _ alts) def
+    evalTree env loc opts fc stk (Case idx x _ alts) def
-      = do let x' : IsVar _ _ ((args ++ vars) ++ free)
+      = do xval <- evalLocal env fc Nothing idx (varExtend x) [] loc
-               = rewrite sym (appendAssociative args vars free) in
-                         varExtend x
-           xval <- evalLocal env fc Nothing idx x' [] loc
            findAlt env loc opts fc stk xval alts def
-    evalTree {args} {vars} {free} env loc opts fc stk (STerm tm) def
+    evalTree env loc opts fc stk (STerm tm) def
-          = do let tm' : Term ((args ++ vars) ++ free)
+          = do case fuel opts of
-                    = rewrite sym (appendAssociative args vars free) in
+                    Nothing => evalWithOpts defs opts env loc (embed tm) stk
-                              embed tm
-               case fuel opts of
-                    Nothing => evalWithOpts defs opts env loc tm' stk
                     Just Z => def
                     Just (S k) =>
                          do let opts' = record { fuel = Just k } opts
-                            evalWithOpts defs opts' env loc tm' stk
+                            evalWithOpts defs opts' env loc (embed tm) stk
     evalTree env loc opts fc stk _ def = def
     -- Take arguments from the stack, as long as there's enough.
            = rewrite sym (plusSuccRightSucc got k) in
                      takeStk k stk (arg :: acc)
-    extendFromStack : (args : List Name) ->
+    argsFromStack : (args : List Name) ->
-                      LocalEnv free vars -> Stack free ->
+                    Stack free ->
-                      Maybe (LocalEnv free (args ++ vars), Stack free)
+                    Maybe (LocalEnv free args, Stack free)
-    extendFromStack [] loc stk = Just (loc, stk)
+    argsFromStack [] stk = Just ([], stk)
-    extendFromStack (n :: ns) loc [] = Nothing
+    argsFromStack (n :: ns) [] = Nothing
-    extendFromStack (n :: ns) loc (arg :: args)
+    argsFromStack (n :: ns) (arg :: args)
-         = do (loc', stk') <- extendFromStack ns loc args
+         = do (loc', stk') <- argsFromStack ns args
               pure (arg :: loc', stk')
     evalOp : (Vect arity (NF free) -> Maybe (NF free)) ->
         evalAll [] = pure []
         evalAll (c :: cs) = pure $ !(evalClosure defs c) :: !(evalAll cs)
-    evalDef : {vars : _} ->
+    evalDef : Env Term free -> EvalOpts ->
-              Env Term free -> LocalEnv free vars -> EvalOpts ->
               (isMeta : Bool) -> FC ->
               RigCount -> Def -> List DefFlag ->
               Stack free -> (def : Lazy (NF free)) ->
               Core (NF free)
-    evalDef {vars} env locs opts meta fc rigd (PMDef r args tree _ _) flags stk def
+    evalDef env opts meta fc rigd (PMDef r args tree _ _) flags stk def
        -- If evaluating the definition fails (e.g. due to a case being
        -- stuck) return the default.
        -- We can use the definition if one of the following is true:
        --   + It's a metavariable and we're not in 'argHolesOnly'
        --   + It's inlinable and we're in 'tcInline'
         = if alwaysReduce r
-             || (not (holesOnly opts) && not (argHolesOnly opts) && not (tcInline opts))
+             || (not (holesOnly opts || argHolesOnly opts || tcInline opts))
              || (meta && rigd /= Rig0)
              || (meta && holesOnly opts)
              || (tcInline opts && elem TCInline flags)
-             then case extendFromStack args locs stk of
+             then case argsFromStack args stk of
                        Nothing => pure def
                        Just (locs', stk') =>
                             evalTree env locs' opts fc stk' tree (pure def)
              else pure def
-    evalDef {vars} env locs opts meta fc rigd (Builtin op) flags stk def
+    evalDef env opts meta fc rigd (Builtin op) flags stk def
         = evalOp (getOp op) stk def
     -- All other cases, use the default value, which is already applied to
     -- the stack
-    evalDef env locs opts _ _ _ _ _ stk def = pure def
+    evalDef env opts _ _ _ _ _ stk def = pure def
 -- Make sure implicit argument order is right... 'vars' is used so we'll
 -- write it explicitly, but it does appear after the parameters in 'eval'!

src/Core/Options.idr+3−1

   logTimings : Bool
   debugElabCheck : Bool -- do conversion check to verify results of elaborator
   dumpcases : Maybe String -- file to output compiled case trees
+  dumplifted : Maybe String -- file to output lambda lifted definitions
 public export
 record PPrinter where
 defaultPPrint = MkPPOpts False True False
 defaultSession : Session
-defaultSession = MkSessionOpts False False False Chez 0 False False Nothing
+defaultSession = MkSessionOpts False False False Chez 0 False False
+                               Nothing Nothing
 defaultElab : ElabDirectives
 defaultElab = MkElabDirectives True True PartialOK 3

src/Core/TT.idr+47−12

 public export
 data Term : List Name -> Type where
      Local : {name : _} ->
-             FC -> Maybe Bool ->
+             FC -> (isLet : Maybe Bool) ->
              (idx : Nat) -> .(IsVar name idx vars) -> Term vars
      Ref : FC -> NameType -> (name : Name) -> Term vars
      -- Metavariables and the scope they are applied to
 notCovering : Totality
 notCovering = MkTotality Unchecked (MissingCases [])
+public export
+data NVar : Name -> List Name -> Type where
+     MkNVar : {i : Nat} -> .(IsVar n i vars) -> NVar n vars
+export
+insertNVar : {outer : List Name} ->
+            (idx : Nat) ->
+            .(IsVar name idx (outer ++ inner)) ->
+            NVar name (outer ++ n :: inner)
+insertNVar {outer = []} idx x = MkNVar (Later x)
+insertNVar {outer = (name :: xs)} Z First = MkNVar First
+insertNVar {n} {outer = (x :: xs)} (S i) (Later y)
+    = let MkNVar prf = insertNVar {n} i y in
+          MkNVar (Later prf)
 export
 insertVar : {outer : _} ->
             (idx : Nat) ->
    = let MkVar x' = weakenVar xs x in
          MkVar (Later x')
+export
+weakenNVar : (ns : List Name) -> {idx : Nat} -> .(IsVar name idx inner) ->
+             NVar name (ns ++ inner)
+weakenNVar [] x = MkNVar x
+weakenNVar (y :: xs) x
+   = let MkNVar x' = weakenNVar xs x in
+         MkNVar (Later x')
 export
 insertVarNames : {outer, ns : _} ->
                  (idx : Nat) ->
     = let MkVar prf = insertVarNames {ns} i x in
           MkVar (Later prf)
+export
+insertNVarNames : {outer, ns : _} ->
+                  (idx : Nat) ->
+                  .(IsVar name idx (outer ++ inner)) ->
+                  NVar name (outer ++ (ns ++ inner))
+insertNVarNames {ns} {outer = []} idx prf = weakenNVar ns prf
+insertNVarNames {outer = (y :: xs)} Z First = MkNVar First
+insertNVarNames {ns} {outer = (y :: xs)} (S i) (Later x)
+    = let MkNVar prf = insertNVarNames {ns} i x in
+          MkNVar (Later prf)
 export
 thin : {outer, inner : _} ->
        (n : Name) -> Term (outer ++ inner) -> Term (outer ++ n :: inner)
 thin n (Local fc r idx prf)
-    = let MkVar var' = insertVar {n} idx prf in
+    = let MkNVar var' = insertNVar {n} idx prf in
           Local fc r _ var'
 thin n (Ref fc nt name) = Ref fc nt name
 thin n (Meta fc name idx args) = Meta fc name idx (map (thin n) args)
               (ns : List Name) -> Term (outer ++ inner) ->
               Term (outer ++ (ns ++ inner))
 insertNames ns (Local fc r idx prf)
-    = let MkVar prf' = insertVarNames {ns} idx prf in
+    = let MkNVar prf' = insertNVarNames {ns} idx prf in
           Local fc r _ prf'
 insertNames ns (Ref fc nt name) = Ref fc nt name
 insertNames ns (Meta fc name idx args)
        None : Bounds []
        Add : (x : Name) -> Name -> Bounds xs -> Bounds (x :: xs)
+export
 addVars : {later, bound : _} ->
           {idx : Nat} ->
           Bounds bound -> .(IsVar name idx (later ++ vars)) ->
-          Var (later ++ (bound ++ vars))
+          NVar name (later ++ (bound ++ vars))
-addVars {later = []} {bound} bs p = weakenVar bound p
+addVars {later = []} {bound} bs p = weakenNVar bound p
-addVars {later = (x :: xs)} bs First = MkVar First
+addVars {later = (x :: xs)} bs First = MkNVar First
 addVars {later = (x :: xs)} bs (Later p)
-  = let MkVar p' = addVars {later = xs} bs p in
+  = let MkNVar p' = addVars {later = xs} bs p in
-        MkVar (Later p')
+        MkNVar (Later p')
 resolveRef : (done : List Name) -> Bounds bound -> FC -> Name ->
              Maybe (Term (later ++ (done ++ bound ++ vars)))
 resolveRef {later} {vars} done (Add {xs} new old bs) fc n
     = if n == old
          then rewrite appendAssociative later done (new :: xs ++ vars) in
-              let MkVar p = weakenVar {inner = new :: xs ++ vars}
+              let MkNVar p = weakenNVar {inner = new :: xs ++ vars}
-                                      (later ++ done) First in
+                                        (later ++ done) First in
-                    Just (Local fc Nothing _ p)
+                     Just (Local fc Nothing _ p)
          else rewrite appendAssociative done [new] (xs ++ vars)
                 in resolveRef (done ++ [new]) bs fc n
            Bounds bound ->
            Term (later ++ vars) -> Term (later ++ (bound ++ vars))
 mkLocals bs (Local fc r idx p)
-    = let MkVar p' = addVars bs p in Local fc r _ p'
+    = let MkNVar p' = addVars bs p in Local fc r _ p'
 mkLocals bs (Ref fc Bound name)
     = maybe (Ref fc Bound name) id (resolveRef [] bs fc name)
 mkLocals bs (Ref fc nt name)

src/Core/TTC.idr+5−6

@@ -583,7 +583,7 @@ mutual · 582 unmodified lines
583	toBuf b (CLocal fc {x} {idx} h) = do tag 0; toBuf b fc; toBuf b x; toBuf b idx	583	toBuf b (CLocal fc {x} {idx} h) = do tag 0; toBuf b fc; toBuf b x; toBuf b idx
584	toBuf b (CRef fc n) = do tag 1; toBuf b fc; toBuf b n	584	toBuf b (CRef fc n) = do tag 1; toBuf b fc; toBuf b n
585	toBuf b (CLam fc x sc) = do tag 2; toBuf b fc; toBuf b x; toBuf b sc	585	toBuf b (CLam fc x sc) = do tag 2; toBuf b fc; toBuf b x; toBuf b sc
586	toBuf b (CLet fc x val sc) = do tag 3; toBuf b fc; toBuf b x; toBuf b val; toBuf b sc	586	toBuf b (CLet fc x inl val sc) = do tag 3; toBuf b fc; toBuf b x; toBuf b inl; toBuf b val; toBuf b sc
587	toBuf b (CApp fc f as) = assert_total $ do tag 4; toBuf b fc; toBuf b f; toBuf b as	587	toBuf b (CApp fc f as) = assert_total $ do tag 4; toBuf b fc; toBuf b f; toBuf b as
588	toBuf b (CCon fc t n as) = assert_total $ do tag 5; toBuf b fc; toBuf b t; toBuf b n; toBuf b as	588	toBuf b (CCon fc t n as) = assert_total $ do tag 5; toBuf b fc; toBuf b t; toBuf b n; toBuf b as
589	toBuf b (COp {arity} fc op as) = assert_total $ do tag 6; toBuf b fc; toBuf b arity; toBuf b op; toBuf b as	589	toBuf b (COp {arity} fc op as) = assert_total $ do tag 6; toBuf b fc; toBuf b arity; toBuf b op; toBuf b as
@@ -608,8 +608,8 @@ mutual · 18 unmodified lines
608	x <- fromBuf b; sc <- fromBuf b	608	x <- fromBuf b; sc <- fromBuf b
609	pure (CLam fc x sc)	609	pure (CLam fc x sc)
610	3 => do fc <- fromBuf b	610	3 => do fc <- fromBuf b
611	x <- fromBuf b; val <- fromBuf b; sc <- fromBuf b	611	x <- fromBuf b; inl <- fromBuf b; val <- fromBuf b; sc <- fromBuf b
612	pure (CLet fc x val sc)	612	pure (CLet fc x inl val sc)
613	4 => do fc <- fromBuf b	613	4 => do fc <- fromBuf b
614	f <- fromBuf b; as <- fromBuf b	614	f <- fromBuf b; as <- fromBuf b
615	pure (CApp fc f as)	615	pure (CApp fc f as)
@@ -944,10 +944,10 @@ TTC GlobalDef where · 328 unmodified lines
944	sc <- fromBuf b	944	sc <- fromBuf b
945	pure (MkGlobalDef loc name ty eargs seargs specargs	945	pure (MkGlobalDef loc name ty eargs seargs specargs
946	mul vars vis	946	mul vars vis
947	tot fl refs refsR inv c True def cdef sc)	947	tot fl refs refsR inv c True def cdef Nothing sc)
948	else pure (MkGlobalDef loc name (Erased loc False) [] [] []	948	else pure (MkGlobalDef loc name (Erased loc False) [] [] []
949	RigW [] Public unchecked [] refs refsR	949	RigW [] Public unchecked [] refs refsR
950	False False True def cdef [])	950	False False True def cdef Nothing [])
951		951
952	TTC Transform where	952	TTC Transform where
953	toBuf b (MkTransform {vars} env lhs rhs)	953	toBuf b (MkTransform {vars} env lhs rhs)
@@ -973,4 +973,3 @@ Core.Context.decode gam idx update (Coded bin) · 19 unmodified lines
973	when update $ coreLift $ writeArray arr idx (Decoded def')	973	when update $ coreLift $ writeArray arr idx (Decoded def')
974	pure def'	974	pure def'
975	Core.Context.decode gam idx update (Decoded def) = pure def	975	Core.Context.decode gam idx update (Decoded def) = pure def
976

src/Core/Unify.idr+12−17

 unifyArgs mode loc env [] [] = pure success
 unifyArgs mode loc env (cx :: cxs) (cy :: cys)
     = do res <- unify (lower mode) loc env cx cy
-         case constraints res of
+         cs <- unifyArgs mode loc env cxs cys
-              [] => do cs <- unifyArgs mode loc env cxs cys
+         pure (union res cs)
-                       pure (union res cs)
-              _ => do cs <- unifyArgs mode loc env cxs cys
-                      -- TODO: Fix this bit! See p59 Ulf's thesis
---                       c <- addConstraint
---                                (MkSeqConstraint loc env
---                                    (map (quote gam env) (cx :: cxs))
---                                    (map (quote gam env) (cy :: cys)))
-                      pure (union res cs) -- [c]
 unifyArgs mode loc env _ _ = ufail loc ""
 -- Get the variables in an application argument list; fail if any arguments
   Unify Term where
     unifyD _ _ mode loc env x y
           = do defs <- get Ctxt
-               ust <- get UST
+               empty <- clearDefs defs
-               when (logging ust) $
+               if !(convert empty env x y)
-                  do logTerm 0 "TOP LEVEL Unifying: " x
-                     logTerm 0 "          with: " y
-               if x == y
                   then do log 10 $ "Skipped unification (equal already): "
                                  ++ show x ++ " and " ++ show y
                           pure success
                           unify mode loc env xnf ynf
     unifyWithLazyD _ _ mode loc env x y
           = do defs <- get Ctxt
-               if x == y
+               empty <- clearDefs defs
+               if !(convert empty env x y)
                   then do log 10 $ "Skipped unification (equal already): "
                                  ++ show x ++ " and " ++ show y
                           pure success
   Unify Closure where
     unifyD _ _ mode loc env x y
         = do defs <- get Ctxt
-             unify mode loc env !(evalClosure defs x) !(evalClosure defs y)
+             empty <- clearDefs defs
+             if !(convert empty env x y)
+                then pure success
+                else do xnf <- evalClosure defs x
+                        ynf <- evalClosure defs y
+                        unify mode loc env xnf ynf
 export
 setInvertible : {auto c : Ref Ctxt Defs} ->

src/Idris/CommandLine.idr+4−0

   Metadata String |
    ||| Dump cases before compiling
   DumpCases String |
+   ||| Dump lambda lifted defs before compiling
+  DumpLifted String |
    ||| Run a REPL command then exit immediately
   RunREPL String |
   FindIPKG |
               Nothing, -- dump metadata information from the given ttm file
            MkOpt ["--dumpcases"] ["output file"] (\f => [DumpCases f])
               Nothing, -- dump case trees to the given file
+           MkOpt ["--dumplifted"] ["output file"] (\f => [DumpLifted f])
+              Nothing, -- dump case trees to the given file
            MkOpt ["--debug-elab-check"] [] [DebugElabCheck]
               Nothing -- do more elaborator checks (currently conversion in LinearCheck)
            ]

src/Idris/Desugar.idr+43−17

          let op = nameRoot opn
          case lookup op (infixes syn) of
               Nothing =>
-                let ops = unpack opChars in
+                  if any isOpChar (unpack op)
-                    if any (\x => x `elem` ops) (unpack op)
+                     then throw (GenericMsg fc $ "Unknown operator '" ++ op ++ "'")
-                       then throw (GenericMsg fc $ "Unknown operator '" ++ op ++ "'")
+                     else do rtoks <- toTokList r
-                       else do rtoks <- toTokList r
+                             pure (Expr l :: Op fc opn backtickPrec :: rtoks)
-                               pure (Expr l :: Op fc opn backtickPrec :: rtoks)
               Just (Prefix, _) =>
                       throw (GenericMsg fc $ "'" ++ op ++ "' is a prefix operator")
               Just (fix, prec) =>
   getDecl AsType d@(PRecord fc vis n ps _ _)
       = Just (PData fc vis (MkPLater fc n (mkRecType ps)))
     where
-      mkRecType : List (Name, PTerm) -> PTerm
+      mkRecType : List (Name, RigCount, PiInfo PTerm, PTerm) -> PTerm
       mkRecType [] = PType fc
-      mkRecType ((n, t) :: ts) = PPi fc RigW Explicit (Just n) t (mkRecType ts)
+      mkRecType ((n, c, p, t) :: ts) = PPi fc c p (Just n) t (mkRecType ts)
   getDecl AsType d@(PFixity _ _ _ _) = Just d
   getDecl AsType d@(PDirective _ _) = Just d
   getDecl AsType d = Nothing
           = map (\x => (Nothing, x)) (pairToCons p)
   desugarDecl ps (PImplementation fc vis pass is cons tn params impname nusing body)
-      = do is' <- traverse (\ ntm => do tm' <- desugar AnyExpr ps (snd (snd ntm))
+      = do is' <- traverse (\ (n,c,tm) => do tm' <- desugar AnyExpr ps tm
-                                        pure (fst ntm, fst (snd ntm), tm')) is
+                                             pure (n, c, tm')) is
-           cons' <- traverse (\ ntm => do tm' <- desugar AnyExpr ps (snd ntm)
+           let _ = the (List (Name, RigCount, RawImp)) is'
-                                          pure (fst ntm, tm')) cons
+           cons' <- traverse (\ (n, tm) => do tm' <- desugar AnyExpr ps tm
+                                              pure (n, tm')) cons
+           let _ = the (List (Maybe Name, RawImp)) cons'
            params' <- traverse (desugar AnyExpr ps) params
+           let _ = the (List RawImp) params'
            -- Look for bindable names in all the constraints and parameters
            let bnames = if !isUnboundImplicits
                         then
                         concatMap (findBindableNames True ps []) (map snd cons') ++
                         concatMap (findBindableNames True ps []) params'
                         else []
            let paramsb = map (doBind bnames) params'
            let isb = map (\ (n, r, tm) => (n, r, doBind bnames tm)) is'
-           let consb = map (\ (n, tm) => (n, doBind bnames tm)) cons'
+           let _ = the (List (Name, RigCount, RawImp)) isb
+           let consb = map (\(n, tm) => (n, doBind bnames tm)) cons'
+           let _ = the (List (Maybe Name, RawImp)) consb
            body' <- maybe (pure Nothing)
                           (\b => do b' <- traverse (desugarDecl ps) b
                              elabImplementation fc vis pass env nest isb consb
                                                 tn paramsb impname nusing
                                                 body')]
   desugarDecl ps (PRecord fc vis tn params conname_in fields)
-      = do params' <- traverse (\ ntm => do tm' <- desugar AnyExpr ps (snd ntm)
+      = do params' <- traverse (\ (n,c,p,tm) =>
-                                            pure (fst ntm, tm')) params
+                          do tm' <- desugar AnyExpr ps tm
+                             p'  <- mapDesugarPiInfo ps p
+                             pure (n, c, p', tm'))
+                        params
+           let _ = the (List (Name, RigCount, PiInfo RawImp, RawImp)) params'
            let fnames = map fname fields
+           let _ = the (List Name) fnames
            -- Look for bindable names in the parameters
            let bnames = if !isUnboundImplicits
                         then concatMap (findBindableNames True
                                          (ps ++ fnames ++ map fst params) [])
-                                       (map snd params')
+                                       (map (\(_,_,_,d) => d) params')
                         else []
-           let paramsb = map (\ (n, tm) => (n, doBind bnames tm)) params'
+           let _ = the (List (String, String)) bnames
+           let paramsb = map (\ (n, c, p, tm) => (n, c, p, doBind bnames tm)) params'
+           let _ = the (List (Name, RigCount, PiInfo RawImp, RawImp)) paramsb
            fields' <- traverse (desugarField (ps ++ map fname fields ++
                                               map fst params)) fields
+           let _ = the (List IField) fields'
            let conname = maybe (mkConName tn) id conname_in
+           let _ = the Name conname
            -- True flag set so that the parent namespace can look inside the
            -- record definition
            pure [IRecord fc (Just (nameRoot tn))
       mkConName : Name -> Name
       mkConName (NS ns (UN n)) = NS ns (DN n (MN ("__mk" ++ n) 0))
       mkConName n = DN (show n) (MN ("__mk" ++ show n) 0)
+      mapDesugarPiInfo : {auto s : Ref Syn SyntaxInfo} -> {auto c : Ref Ctxt Defs}
+                  -> {auto u : Ref UST UState} -> {auto m : Ref MD Metadata}
+                  -> List Name -> PiInfo PTerm -> Core (PiInfo RawImp)
+      mapDesugarPiInfo ps Implicit         = pure   Implicit
+      mapDesugarPiInfo ps Explicit         = pure   Explicit
+      mapDesugarPiInfo ps AutoImplicit     = pure   AutoImplicit
+      mapDesugarPiInfo ps (DefImplicit tm) = pure $ DefImplicit
+                                                  !(desugar AnyExpr ps tm)
   desugarDecl ps (PFixity fc Prefix prec (UN n))
       = do syn <- get Syn

src/Idris/Elab/Implementation.idr+5−5

                log 5 $ "Added defaults: body is " ++ show body
                log 5 $ "Missing methods: " ++ show missing
+               -- Add the 'using' hints
+               log 10 $ "Open hints: " ++ (show (impName :: nusing))
+               traverse_ (\n => do n' <- checkUnambig fc n
+                                   addOpenHint n') nusing
                -- 2. Elaborate top level function types for this interface
                defs <- get Ctxt
                fns <- topMethTypes [] impName methImps impsp (params cdata)
                let hs = openHints defs
                maybe (pure ()) (\x => addOpenHint impName) impln
-               -- Also add the 'using' hints
-               log 10 $ "Open hints: " ++ (show (impName :: nusing))
-               traverse_ (\n => do n' <- checkUnambig fc n
-                                   addOpenHint n') nusing
                -- Make sure we don't use this name to solve parent constraints
                -- when elaborating the record, or we'll end up in a cycle!
                setFlag fc impName BlockedHint

src/Idris/IDEMode/MakeClause.idr+1−1

@@ -9,7 +9,7 @@ import Parser.Unlit · 8 unmodified lines
9	showRHSName : Name -> String	9	showRHSName : Name -> String
10	showRHSName n	10	showRHSName n
11	= let fn = show (dropNS n) in	11	= let fn = show (dropNS n) in
12	if any (flip elem (unpack opChars)) (unpack fn)	12	if any isOpChar (unpack fn)
13	then "op"	13	then "op"
14	else fn	14	else fn
15		15

src/Idris/IDEMode/Parser.idr+4−18

+||| Slightly different lexer than the source language because we are more free
+||| as to what can be identifiers, and fewer tokens are supported. But otherwise,
+||| we can reuse the standard stuff
 module Idris.IDEMode.Parser
 import Idris.IDEMode.Commands
 import Parser.Support
 import Text.Lexer
--- Slightly different lexer than the source language because we are more free
--- as to what can be identifiers, and fewer tokens are supported. But otherwise,
--- we can reuse the standard stuff
 %hide Lexer.symbols
 symbols : List String
 symbols = ["(", ":", ")"]
-ident : Lexer
-ident = pred startIdent <+> many (pred validIdent)
-  where
-    startIdent : Char -> Bool
-    startIdent '_' = True
-    startIdent x = isAlpha x
-    validIdent : Char -> Bool
-    validIdent '_' = True
-    validIdent '-' = True
-    validIdent '\'' = True
-    validIdent x = isAlphaNum x
 ideTokens : TokenMap Token
 ideTokens =
     map (\x => (exact x, Symbol)) symbols ++
     [(digits, \x => Literal (cast x)),
      (stringLit, \x => StrLit (stripQuotes x)),
-     (ident, Ident),
+     (identRelaxed, Ident),
      (space, Comment)]
   where
     stripQuotes : String -> String

src/Idris/IDEMode/TokenLine.idr+4−17

+||| Tokenise a source line for easier processing
 module Idris.IDEMode.TokenLine
--- Tokenise a source line for easier processing
+import Parser.Lexer
 import Text.Lexer
 public export
   | Equal
   | Other String
-ident : Lexer
-ident = pred startIdent <+> many (pred validIdent)
-  where
-    startIdent : Char -> Bool
-    startIdent '_' = True
-    startIdent x = isAlpha x
-    validIdent : Char -> Bool
-    validIdent '_' = True
-    validIdent '\'' = True
-    validIdent x = isAlphaNum x
 holeIdent : Lexer
-holeIdent = is '?' <+> ident
+holeIdent = is '?' <+> identStrict
 srcTokens : TokenMap SourcePart
 srcTokens =
-    [(ident, Name),
+    [(identStrict, Name),
      (holeIdent, \x => HoleName (assert_total (strTail x))),
      (space, Whitespace),
      (is '{', const LBrace),
            -- number to read when storing spans in the file
            (srctoks, (l, c, rest)) =>
               map tok srctoks ++ (if rest == "" then [] else [Other rest])

src/Idris/Parser.idr+38−8

                    rig <- getMult rigc
                    pure (rig, pat, ty))
-  pibindList : FileName -> FilePos -> IndentInfo ->
+  pibindListName : FileName -> FilePos -> IndentInfo ->
-               Rule (List (RigCount, Maybe Name, PTerm))
+                   Rule (List (RigCount, Name, PTerm))
-  pibindList fname start indents
+  pibindListName fname start indents
        = do rigc <- multiplicity
             ns <- sepBy1 (symbol ",") unqualifiedName
             symbol ":"
             ty <- expr pdef fname indents
             atEnd indents
             rig <- getMult rigc
-            pure (map (\n => (rig, Just (UN n), ty)) ns)
+            pure (map (\n => (rig, UN n, ty)) ns)
      <|> sepBy1 (symbol ",")
                 (do rigc <- multiplicity
                     n <- name
                     symbol ":"
                     ty <- expr pdef fname indents
                     rig <- getMult rigc
-                    pure (rig, Just n, ty))
+                    pure (rig, n, ty))
+  pibindList : FileName -> FilePos -> IndentInfo ->
+               Rule (List (RigCount, Maybe Name, PTerm))
+  pibindList fname start indents
+    = do params <- pibindListName fname start indents
+         pure $ map (\(rig, n, ty) => (rig, Just n, ty)) params
   bindSymbol : Rule (PiInfo PTerm)
   bindSymbol
   record_ fname indents
       = do start <- location
            keyword "record"
-           commit
            symbol "{"
+           commit
            fs <- sepBy1 (symbol ",") (field fname indents)
            symbol "}"
            end <- location
              end <- location
              pure (map (\n => MkField (MkFC fname start end)
                                       rig p n ty) ns)
+recordParam : FileName -> IndentInfo -> Rule (List (Name, RigCount, PiInfo PTerm,  PTerm))
+recordParam fname indents
+    = do symbol "("
+         start <- location
+         params <- pibindListName fname start indents
+         symbol ")"
+         pure $ map (\(c, n, tm) => (n, c, Explicit, tm)) params
+  <|> do symbol "{"
+         commit
+         info <- the (EmptyRule (PiInfo PTerm))
+                 (pure  AutoImplicit <* keyword "auto"
+              <|>(do
+                  keyword "default"
+                  t <- simpleExpr fname indents
+                  pure $ DefImplicit t)
+              <|> pure      Implicit)
+         start <- location
+         params <- pibindListName fname start indents
+         symbol "}"
+         pure $ map (\(c, n, tm) => (n, c, info, tm)) params
+  <|> do start <- location
+         n <- name
+         end <- location
+         pure [(n, RigW, Explicit, PInfer (MkFC fname start end))]
 recordDecl : FileName -> IndentInfo -> Rule PDecl
 recordDecl fname indents
          vis <- visibility
          col <- column
          keyword "record"
-         commit
          n <- name
-         params <- many (ifaceParam fname indents)
+         paramss <- many (recordParam fname indents)
+         let params = concat paramss
          keyword "where"
          dcflds <- blockWithOptHeaderAfter col ctor (fieldDecl fname)
          end <- location

src/Idris/Resugar.idr+13−4

@@ -340,14 +340,23 @@ mutual · 339 unmodified lines
340	toPRecord : {auto c : Ref Ctxt Defs} ->	340	toPRecord : {auto c : Ref Ctxt Defs} ->
341	{auto s : Ref Syn SyntaxInfo} ->	341	{auto s : Ref Syn SyntaxInfo} ->
342	ImpRecord ->	342	ImpRecord ->
343	Core (Name, List (Name, PTerm), Maybe Name, List PField)	343	Core (Name, List (Name, RigCount, PiInfo PTerm, PTerm), Maybe Name, List PField)
344	toPRecord (MkImpRecord fc n ps con fs)	344	toPRecord (MkImpRecord fc n ps con fs)
345	= do ps' <- traverse (\ (n, ty) =>	345	= do ps' <- traverse (\ (n, c, p, ty) =>
346	do ty' <- toPTerm startPrec ty	346	do ty' <- toPTerm startPrec ty
347	pure (n, ty')) ps	347	p' <- mapPiInfo p
		348	pure (n, c, p', ty')) ps
348	fs' <- traverse toPField fs	349	fs' <- traverse toPField fs
349	pure (n, ps', Just con, fs')	350	pure (n, ps', Just con, fs')
350		351	where
		352	mapPiInfo : {auto c : Ref Ctxt Defs} ->
		353	{auto s : Ref Syn SyntaxInfo} ->
		354	PiInfo RawImp -> Core (PiInfo PTerm)
		355	mapPiInfo Explicit = pure Explicit
		356	mapPiInfo Implicit = pure Implicit
		357	mapPiInfo AutoImplicit = pure AutoImplicit
		358	mapPiInfo (DefImplicit p) = pure $ DefImplicit !(toPTerm startPrec p)
		359
351	toPFnOpt : {auto c : Ref Ctxt Defs} ->	360	toPFnOpt : {auto c : Ref Ctxt Defs} ->
352	{auto s : Ref Syn SyntaxInfo} ->	361	{auto s : Ref Syn SyntaxInfo} ->
353	FnOpt -> Core PFnOpt	362	FnOpt -> Core PFnOpt

src/Idris/SetOptions.idr+3−0

 preOptions (DumpCases f :: opts)
     = do setSession (record { dumpcases = Just f } !getSession)
          preOptions opts
+preOptions (DumpLifted f :: opts)
+    = do setSession (record { dumplifted = Just f } !getSession)
+         preOptions opts
 preOptions (_ :: opts) = preOptions opts
 -- Options to be processed after type checking. Returns whether execution

src/Idris/Syntax.idr+9−2

        PRecord : FC ->
                  Visibility ->
                  Name ->
-                 (params : List (Name, PTerm)) ->
+                 (params : List (Name, RigCount, PiInfo PTerm, PTerm)) ->
                  (conName : Maybe Name) ->
                  List PField ->
                  PDecl
                              <*> pure ns
                              <*> goMPDecls mps
     goPDecl (PRecord fc v n nts mn fs) =
-      PRecord fc v n <$> goPairedPTerms nts
+      PRecord fc v n <$> go4TupledPTerms nts
                      <*> pure mn
                      <*> goPFields fs
     goPDecl (PMutual fc ps) = PMutual fc <$> goPDecls ps
       (::) . (\ c => (a, b, c)) <$> goPTerm t
                                 <*> go3TupledPTerms ts
+    go4TupledPTerms : List (a, b, PiInfo PTerm, PTerm) -> Core (List (a, b, PiInfo PTerm, PTerm))
+    go4TupledPTerms [] = pure []
+    go4TupledPTerms ((a, b, p, t) :: ts) =
+      (\ p, d, ts => (a, b, p, d) :: ts) <$> goPiInfo p
+                                         <*> goPTerm t
+                                         <*> go4TupledPTerms ts
     goPDos : List PDo -> Core (List PDo)
     goPDos []        = pure []
     goPDos (d :: ds) = (::) <$> goPDo d <*> goPDos ds

src/Parser/Lexer.idr+87−31

@@ -40,20 +40,58 @@ export · 39 unmodified lines
40	Show (TokenData Token) where	40	Show (TokenData Token) where
41	show t = show (line t, col t, tok t)	41	show t = show (line t, col t, tok t)
42		42
		43	\|\|\| In `comment` we are careful not to parse closing delimiters as
		44	\|\|\| valid comments. i.e. you may not write many dashes followed by
		45	\|\|\| a closing brace and call it a valid comment.
43	comment : Lexer	46	comment : Lexer
44	comment = is '-' <+> is '-' <+> many (isNot '\n')	47	comment
45		48	= is '-' <+> is '-' -- comment opener
46	toEndComment : (k : Nat) -> Recognise (k /= 0)	49	<+> many (is '-') <+> reject (is '}') -- not a closing delimiter
47	toEndComment Z = empty	50	<+> many (isNot '\n') -- till the end of line
48	toEndComment (S k)	51
49	= some (pred (\c => c /= '-' && c /= '{' && c /= '"'))	52	mutual
50	<+> toEndComment (S k)	53
51	<\|> is '{' <+> is '-' <+> toEndComment (S (S k))	54	\|\|\| The mutually defined functions represent different states in a
52	<\|> is '-' <+> is '}' <+> toEndComment k	55	\|\|\| small automaton.
53	<\|> comment <+> toEndComment (S k)	56	\|\|\| `toEndComment` is the default state and it will munch through
54	<\|> stringLit <+> toEndComment (S k)	57	\|\|\| the input until we detect a special character (a dash, an
55	<\|> is '{' <+> toEndComment (S k)	58	\|\|\| opening brace, or a double quote) and then switch to the
56	<\|> is '-' <+> toEndComment (S k)	59	\|\|\| appropriate state.
		60	toEndComment : (k : Nat) -> Recognise (k /= 0)
		61	toEndComment Z = empty
		62	toEndComment (S k)
		63	= some (pred (\c => c /= '-' && c /= '{' && c /= '"'))
		64	<+> toEndComment (S k)
		65	<\|> is '{' <+> singleBrace k
		66	<\|> is '-' <+> singleDash k
		67	<\|> stringLit <+> toEndComment (S k)
		68
		69	\|\|\| After reading a single brace, we may either finish reading an
		70	\|\|\| opening delimiter or ignore it (e.g. it could be an implicit
		71	\|\|\| binder).
		72	singleBrace : (k : Nat) -> Lexer
		73	singleBrace k
		74	= is '-' <+> many (is '-') -- opening delimiter
		75	<+> singleDash (S k) -- handles the {----} special case
		76	<\|> toEndComment (S k) -- not a valid comment
		77
		78	\|\|\| After reading a single dash, we may either find another one,
		79	\|\|\| meaning we may have started reading a line comment, or find
		80	\|\|\| a closing brace meaning we have found a closing delimiter.
		81	singleDash : (k : Nat) -> Lexer
		82	singleDash k
		83	= is '-' <+> doubleDash k -- comment or closing delimiter
		84	<\|> is '}' <+> toEndComment k -- closing delimiter
		85	<\|> toEndComment (S k) -- not a valid comment
		86
		87	\|\|\| After reading a double dash, we are potentially reading a line
		88	\|\|\| comment unless the series of uninterrupted dashes is ended with
		89	\|\|\| a closing brace in which case it is a closing delimiter.
		90	doubleDash : (k : Nat) -> Lexer
		91	doubleDash k = many (is '-') <+> choice -- absorb all dashes
		92	[ is '}' <+> toEndComment k -- closing delimiter
		93	, many (isNot '\n') <+> toEndComment (S k) -- line comment
		94	]
57		95
58	blockComment : Lexer	96	blockComment : Lexer
59	blockComment = is '{' <+> is '-' <+> toEndComment 1	97	blockComment = is '{' <+> is '-' <+> toEndComment 1
@@ -61,20 +99,40 @@ blockComment = is '{' <+> is '-' <+> toEndComment 1 · 1 unmodified line
61	docComment : Lexer	99	docComment : Lexer
62	docComment = is '\|' <+> is '\|' <+> is '\|' <+> many (isNot '\n')	100	docComment = is '\|' <+> is '\|' <+> is '\|' <+> many (isNot '\n')
63		101
64	ident : Lexer	102	-- Identifier Lexer
65	ident = pred startIdent <+> many (pred validIdent)	103	--
66	where	104	-- There are two variants, a strict ident and a relaxed ident.
67	startIdent : Char -> Bool	105	-- Prime definitions recieve a boolean determining if it is relaxed.
68	startIdent '_' = True	106
69	startIdent x = isAlpha x \|\| x > chr 127	107	startIdent : Char -> Bool
		108	startIdent '_' = True
		109	startIdent x = isAlpha x \|\| x > chr 127
		110
		111	%inline
		112	validIdent' : Bool -> Char -> Bool
		113	validIdent' _ '_' = True
		114	validIdent' r '-' = r
		115	validIdent' _ '\'' = True
		116	validIdent' _ x = isAlphaNum x \|\| x > chr 127
		117
		118	%inline
		119	ident' : Bool -> Lexer
		120	ident' relaxed =
		121	(pred $ startIdent) <+>
		122	(many . pred $ validIdent' relaxed)
		123
		124	-- This are the two identifier lexer specializations
70		125
71	validIdent : Char -> Bool	126	export
72	validIdent '_' = True	127	identStrict : Lexer
73	validIdent '\'' = True	128	identStrict = ident' False
74	validIdent x = isAlphaNum x \|\| x > chr 127	129
		130	export
		131	identRelaxed : Lexer
		132	identRelaxed = ident' True
75		133
76	holeIdent : Lexer	134	holeIdent : Lexer
77	holeIdent = is '?' <+> ident	135	holeIdent = is '?' <+> identStrict
78		136
79	doubleLit : Lexer	137	doubleLit : Lexer
80	doubleLit	138	doubleLit
@@ -121,12 +179,13 @@ symbols · 40 unmodified lines
121	"(", ")", "{", "}", "[", "]", ",", ";", "_",	179	"(", ")", "{", "}", "[", "]", ",", ";", "_",
122	"`(", "`"]	180	"`(", "`"]
123		181
		182
124	export	183	export
125	opChars : String	184	isOpChar : Char -> Bool
126	opChars = ":!#$%&*+./<=>?@\\^\|-~"	185	isOpChar c = c `elem` (unpack ":!#$%&*+./<=>?@\\^\|-~")
127		186
128	validSymbol : Lexer	187	validSymbol : Lexer
129	validSymbol = some (oneOf opChars)	188	validSymbol = some (pred isOpChar)
130		189
131	-- Valid symbols which have a special meaning so can't be operators	190	-- Valid symbols which have a special meaning so can't be operators
132	export	191	export
@@ -136,9 +195,6 @@ reservedSymbols · 3 unmodified lines
136	["%", "\\", ":", "=", "\|", "\|\|\|", "<-", "->", "=>", "?", "!",	195	["%", "\\", ":", "=", "\|", "\|\|\|", "<-", "->", "=>", "?", "!",
137	"&", "**", ".."]	196	"&", "**", ".."]
138		197
139	symbolChar : Char -> Bool
140	symbolChar c = c `elem` unpack opChars
141
142	fromHexLit : String -> Integer	198	fromHexLit : String -> Integer
143	fromHexLit str	199	fromHexLit str
144	= if length str <= 2	200	= if length str <= 2
@@ -161,7 +217,7 @@ rawTokens = · 16 unmodified lines
161	(digits, \x => Literal (cast x)),	217	(digits, \x => Literal (cast x)),
162	(stringLit, \x => StrLit (stripQuotes x)),	218	(stringLit, \x => StrLit (stripQuotes x)),
163	(charLit, \x => CharLit (stripQuotes x)),	219	(charLit, \x => CharLit (stripQuotes x)),
164	(ident, \x => if x `elem` keywords then Keyword x else Ident x),	220	(identStrict, \x => if x `elem` keywords then Keyword x else Ident x),
165	(space, Comment),	221	(space, Comment),
166	(validSymbol, Symbol),	222	(validSymbol, Symbol),
167	(symbol, Unrecognised)]	223	(symbol, Unrecognised)]

src/TTImp/Elab/Case.idr+6−7

     -- Replace a variable in the argument list; if the reference is to
     -- a variable kept in the outer environment (therefore not an argument
     -- in the list) don't consume it
-    replace : {idx : Nat} -> .(IsVar name idx vs) ->
+    replace : (idx : Nat) -> RawImp -> List RawImp -> List RawImp
-              RawImp -> List RawImp -> List RawImp
+    replace Z lhs (old :: xs)
-    replace First lhs (old :: xs)
        = let lhs' = case old of
                          IAs loc' side n _ => IAs loc' side n lhs
                          _ => lhs in
              lhs' :: xs
-    replace (Later p) lhs (x :: xs)
+    replace (S k) lhs (x :: xs)
-        = x :: replace p lhs xs
+        = x :: replace k lhs xs
     replace _ _ xs = xs
     mkSplit : Maybe (Var vs) ->
               RawImp -> List RawImp ->
               List RawImp
     mkSplit Nothing lhs args = reverse (lhs :: args)
-    mkSplit (Just (MkVar prf)) lhs args
+    mkSplit (Just (MkVar {i} prf)) lhs args
-        = reverse (replace prf lhs args)
+        = reverse (replace i lhs args)
     -- Names used in the pattern we're matching on, so don't bind them
     -- in the generated case block

src/TTImp/Elab/Check.idr+8−3

     dropSub (DropCons sub) = pure sub
     dropSub _ = throw (InternalError "Badly formed weakened environment")
+    -- This helps persuade the erasure checker that it can erase IsVar,
+    -- because there's no matching on it in removeArgVars below.
+    dropLater : IsVar name (S idx) (v :: vs) -> IsVar name idx vs
+    dropLater (Later p) = p
     -- Remove any instance of the top level local variable from an
     -- application. Fail if it turns out to be necessary.
     -- NOTE: While this isn't strictly correct given the type of the hole
     -- in scope.
     removeArgVars : List (Term (n :: vs)) -> Maybe (List (Term vs))
     removeArgVars [] = pure []
-    removeArgVars (Local fc r _ (Later p) :: args)
+    removeArgVars (Local fc r (S k) p :: args)
         = do args' <- removeArgVars args
-             pure (Local fc r _ p :: args')
+             pure (Local fc r _ (dropLater p) :: args')
-    removeArgVars (Local fc r _ First :: args)
+    removeArgVars (Local fc r Z p :: args)
         = removeArgVars args
     removeArgVars (a :: args)
         = do a' <- shrinkTerm a (DropCons SubRefl)

src/TTImp/Parser.idr+34−14

                    pure (rig, UN n, ty))
-  pibindList : FileName -> FilePos -> IndentInfo ->
+  pibindListName : FileName -> FilePos -> IndentInfo ->
-               Rule (List (RigCount, Maybe Name, RawImp))
+                   Rule (List (RigCount, Name, RawImp))
-  pibindList fname start indents
+  pibindListName fname start indents
        = do rigc <- multiplicity
             ns <- sepBy1 (symbol ",") unqualifiedName
             symbol ":"
             ty <- expr fname indents
             atEnd indents
             rig <- getMult rigc
-            pure (map (\n => (rig, Just (UN n), ty)) ns)
+            pure (map (\n => (rig, UN n, ty)) ns)
      <|> sepBy1 (symbol ",")
                 (do rigc <- multiplicity
                     n <- name
                     symbol ":"
                     ty <- expr fname indents
                     rig <- getMult rigc
-                    pure (rig, Just n, ty))
+                    pure (rig, n, ty))
+  pibindList : FileName -> FilePos -> IndentInfo ->
+               Rule (List (RigCount, Maybe Name, RawImp))
+  pibindList fname start indents
+    = do params <- pibindListName fname start indents
+         pure $ map (\(rig, n, ty) => (rig, Just n, ty)) params
   autoImplicitPi : FileName -> IndentInfo -> Rule RawImp
   autoImplicitPi fname indents
   record_ fname indents
       = do start <- location
            keyword "record"
-           commit
            symbol "{"
+           commit
            fs <- sepBy1 (symbol ",") (field fname indents)
            symbol "}"
            sc <- expr fname indents
          end <- location
          pure (MkImpData (MkFC fname start end) n ty opts cs)
-ifaceParam : FileName -> IndentInfo -> Rule (Name, RawImp)
+recordParam : FileName -> IndentInfo -> Rule (List (Name, RigCount, PiInfo RawImp, RawImp))
-ifaceParam fname indents
+recordParam fname indents
     = do symbol "("
-         n <- name
+         start <- location
-         symbol ":"
+         params <- pibindListName fname start indents
-         tm <- expr fname indents
          symbol ")"
-         pure (n, tm)
+         pure $ map (\(c, n, tm) => (n, c, Explicit, tm)) params
+  <|> do symbol "{"
+         commit
+         start <- location
+         info <- the (EmptyRule (PiInfo RawImp))
+                 (pure  AutoImplicit <* keyword "auto"
+              <|>(do
+                  keyword "default"
+                  t <- simpleExpr fname indents
+                  pure $ DefImplicit t)
+              <|> pure      Implicit)
+         params <- pibindListName fname start indents
+         symbol "}"
+         pure $ map (\(c, n, tm) => (n, c, info, tm)) params
   <|> do start <- location
          n <- name
          end <- location
-         pure (n, Implicit (MkFC fname start end) False)
+         pure [(n, RigW, Explicit, Implicit (MkFC fname start end) False)]
 fieldDecl : FileName -> IndentInfo -> Rule (List IField)
 fieldDecl fname indents
          keyword "record"
          commit
          n <- name
-         params <- many (ifaceParam fname indents)
+         paramss <- many (recordParam fname indents)
+         let params = concat paramss
          keyword "where"
          exactIdent "constructor"
          dc <- name

src/TTImp/ProcessData.idr+15−11

                 else pure rest
 -- If exactly one argument is unerased, return its position
-getRelevantArg : Defs -> Nat -> Maybe Nat -> NF [] -> Core (Maybe Nat)
+getRelevantArg : Defs -> Nat -> Maybe Nat -> Bool -> NF [] ->
-getRelevantArg defs i rel (NBind fc _ (Pi Rig0 _ _) sc)
+                 Core (Maybe (Bool, Nat))
-    = getRelevantArg defs (1 + i) rel
+getRelevantArg defs i rel world (NBind fc _ (Pi Rig0 _ _) sc)
+    = getRelevantArg defs (1 + i) rel world
            !(sc defs (toClosure defaultOpts [] (Erased fc False)))
--- %World is never inspected, so might as well be deleted from data types
+-- %World is never inspected, so might as well be deleted from data types,
-getRelevantArg defs i rel (NBind fc _ (Pi _ _ (NPrimVal _ WorldType)) sc)
+-- although it needs care when compiling to ensure that the function that
-    = getRelevantArg defs (1 + i) rel
+-- returns the IO/%World type isn't erased
+getRelevantArg defs i rel world (NBind fc _ (Pi _ _ (NPrimVal _ WorldType)) sc)
+    = getRelevantArg defs (1 + i) rel False
            !(sc defs (toClosure defaultOpts [] (Erased fc False)))
-getRelevantArg defs i Nothing (NBind fc _ (Pi _ _ _) sc) -- found a relevant arg
+getRelevantArg defs i Nothing world (NBind fc _ (Pi _ _ _) sc) -- found a relevant arg
-    = getRelevantArg defs (1 + i) (Just i)
+    = getRelevantArg defs (1 + i) (Just i) world
            !(sc defs (toClosure defaultOpts [] (Erased fc False)))
-getRelevantArg defs i (Just _) (NBind _ _ (Pi _ _ _) sc) -- more than one relevant
+getRelevantArg defs i (Just _) world (NBind _ _ (Pi _ _ _) sc) -- more than one relevant
     = pure Nothing
-getRelevantArg defs i rel tm = pure rel
+getRelevantArg defs i rel world tm
+    = pure (maybe Nothing (\r => Just (world, r)) rel)
 -- If there's one constructor with only one non-Rig0 argument, flag it as
 -- a newtype for optimisation
               List Constructor -> Core ()
 findNewtype [con]
     = do defs <- get Ctxt
-         Just arg <- getRelevantArg defs 0 Nothing !(nf defs [] (type con))
+         Just arg <- getRelevantArg defs 0 Nothing True !(nf defs [] (type con))
               | Nothing => pure ()
          updateDef (name con)
                (\d => case d of

src/TTImp/ProcessRecord.idr+32−19

 import TTImp.Unelab
 import TTImp.Utils
-mkDataTy : FC -> List (Name, RawImp) -> RawImp
+mkDataTy : FC -> List (Name, RigCount, PiInfo RawImp, RawImp) -> RawImp
 mkDataTy fc [] = IType fc
-mkDataTy fc ((n, ty) :: ps)
+mkDataTy fc ((n, c, p, ty) :: ps)
-    = IPi fc RigW Explicit (Just n) ty (mkDataTy fc ps)
+    = IPi fc c p (Just n) ty (mkDataTy fc ps)
 elabRecord : {vars : _} ->
              {auto c : Ref Ctxt Defs} ->
              List ElabOpt -> FC -> Env Term vars ->
              NestedNames vars -> Maybe String ->
              Visibility -> Name ->
-             (params : List (Name, RawImp)) ->
+             (params : List (Name, RigCount, PiInfo RawImp, RawImp)) ->
              (conName : Name) ->
              List IField ->
              Core ()
          defs <- get Ctxt
          Just conty <- lookupTyExact conName (gamma defs)
              | Nothing => throw (InternalError ("Adding " ++ show tn ++ "failed"))
-         let recTy = apply (IVar fc tn) (map (IVar fc) (map fst params))
          -- Go into new namespace, if there is one, for getters
          case newns of
-              Nothing => elabGetters conName recTy 0 [] [] conty
+              Nothing => elabGetters conName 0 [] [] conty
               Just ns =>
                    do let cns = currentNS defs
                       let nns = nestedNS defs
                       extendNS [ns]
                       newns <- getNS
-                      elabGetters conName recTy 0 [] [] conty
+                      elabGetters conName 0 [] [] conty
                       defs <- get Ctxt
                       -- Record that the current namespace is allowed to look
                       -- at private names in the nested namespace
                       put Ctxt (record { currentNS = cns,
                                          nestedNS = newns :: nns } defs)
   where
-    jname : (Name, RawImp) -> (Maybe Name, RigCount, PiInfo RawImp, RawImp)
+    paramTelescope : List (Maybe Name, RigCount, PiInfo RawImp, RawImp)
-    jname (n, t) = (Just n, Rig0, Implicit, t)
+    paramTelescope = map jname params
+      where
+        jname : (Name, RigCount, PiInfo RawImp, RawImp)
+             -> (Maybe Name, RigCount, PiInfo RawImp, RawImp)
+        -- Record type parameters are implicit in the constructor
+        -- and projections
+        jname (n, _, _, t) = (Just n, Rig0, Implicit, t)
     fname : IField -> Name
     fname (MkIField fc c p n ty) = n
     mkTy ((n, c, imp, argty) :: args) ret
         = IPi fc c imp n argty (mkTy args ret)
+    recTy : RawImp
+    recTy = apply (IVar fc tn) (map (\(n, c, p, tm) => (n, IVar fc n, p)) params)
+      where
+        ||| Apply argument to list of explicit or implicit named arguments
+        apply : RawImp -> List (Name, RawImp, PiInfo RawImp) -> RawImp
+        apply f [] = f
+        apply f ((n, arg, Explicit) :: xs) = apply (IApp         (getFC f) f          arg) xs
+        apply f ((n, arg, _       ) :: xs) = apply (IImplicitApp (getFC f) f (Just n) arg) xs
     elabAsData : Name -> Core ()
     elabAsData cname
-        = do let retty = apply (IVar fc tn) (map (IVar fc) (map fst params))
+        = do let conty = mkTy paramTelescope $
-             let conty = mkTy (map jname params) $
+                         mkTy (map farg fields) recTy
-                         mkTy (map farg fields) retty
              let con = MkImpTy fc cname !(bindTypeNames [] (map fst params ++
                                            map fname fields ++ vars) conty)
              let dt = MkImpData fc tn !(bindTypeNames [] (map fst params ++
     -- Generate getters from the elaborated record constructor type
     elabGetters : {vs : _} ->
-                  Name -> RawImp ->
+                  Name ->
                   (done : Nat) -> -- number of explicit fields processed
                   List (Name, RawImp) -> -- names to update in types
                     -- (for dependent records, where a field's type may depend
                     -- on an earlier projection)
                   Env Term vs -> Term vs ->
                   Core ()
-    elabGetters con recTy done upds tyenv (Bind bfc n b@(Pi rc imp ty_chk) sc)
+    elabGetters con done upds tyenv (Bind bfc n b@(Pi rc imp ty_chk) sc)
         = if (n `elem` map fst params) || (n `elem` vars)
-             then elabGetters con recTy
+             then elabGetters con
                               (if imp == Explicit && not (n `elem` vars)
                                   then S done else done)
                               upds (b :: tyenv) sc
                    let rname = MN "rec" 0
                    gty <- bindTypeNames []
                                  (map fst params ++ map fname fields ++ vars) $
-                                    mkTy (map jname params) $
+                                    mkTy paramTelescope $
                                       IPi fc RigW Explicit (Just rname) recTy ty'
                    log 5 $ "Projection " ++ show gname ++ " : " ++ show gty
                    let lhs_exp
                    processDecl [] nest env
                        (IDef fc gname [PatClause fc lhs (IVar fc fldName)])
                    let upds' = (n, IApp fc (IVar fc gname) (IVar fc rname)) :: upds
-                   elabGetters con recTy
+                   elabGetters con
                                (if imp == Explicit
                                    then S done else done)
                                upds' (b :: tyenv) sc
-    elabGetters con recTy done upds _ _ = pure ()
+    elabGetters con done upds _ _ = pure ()
 export
 processRecord : {auto c : Ref Ctxt Defs} ->

src/TTImp/TTImp.idr+1−1

@@ -264,7 +264,7 @@ mutual · 263 unmodified lines
264	public export	264	public export
265	data ImpRecord : Type where	265	data ImpRecord : Type where
266	MkImpRecord : FC -> (n : Name) ->	266	MkImpRecord : FC -> (n : Name) ->
267	(params : List (Name, RawImp)) ->	267	(params : List (Name, RigCount, PiInfo RawImp, RawImp)) ->
268	(conName : Name) ->	268	(conName : Name) ->
269	(fields : List IField) ->	269	(fields : List IField) ->
270	ImpRecord	270	ImpRecord

src/Utils/Binary.idr+1−1

@@ -114,7 +114,7 @@ initBinaryS s · 113 unmodified lines
114	extendBinary : Int -> Binary -> Core Binary	114	extendBinary : Int -> Binary -> Core Binary
115	extendBinary need (MkBin buf l s u)	115	extendBinary need (MkBin buf l s u)
116	= do let newsize = s * 2	116	= do let newsize = s * 2
117	let s' = if newsize < need	117	let s' = if (newsize - l) < need
118	then newsize + need	118	then newsize + need
119	else newsize	119	else newsize
120	Just buf' <- coreLift $ resizeBuffer buf s'	120	Just buf' <- coreLift $ resizeBuffer buf s'

support/chez/support.ss+8−5

 (define b+ (lambda (x y bits) (remainder (+ x y) (expt 2 bits))))
 (define b- (lambda (x y bits) (remainder (- x y) (expt 2 bits))))
 (define b* (lambda (x y bits) (remainder (* x y) (expt 2 bits))))
-(define b/ (lambda (x y bits) (remainder (floor (/ x y)) (expt 2 bits))))
+(define b/ (lambda (x y bits) (remainder (exact-floor (/ x y)) (expt 2 bits))))
 (define blodwen-shl (lambda (x y) (ash x y)))
 (define blodwen-shr (lambda (x y) (ash x (- y))))
 (define cast-string-int
   (lambda (x)
     (floor (cast-num (string->number (destroy-prefix x))))))
+(define exact-floor
+  (lambda (x)
+    (inexact->exact (floor x))))
 (define cast-string-double
   (lambda (x)
     (cast-num (string->number (destroy-prefix x)))))
 (define either-left
   (lambda (x)
-    (vector 0 #f #f x)))
+    (vector 0 x)))
 (define either-right
   (lambda (x)
-    (vector 1 #f #f x)))
+    (vector 1 x)))
 (define blodwen-error-quit
   (lambda (msg)
 (define (blodwen-args)
   (define (blodwen-build-args args)
     (if (null? args)
-        (vector 0 '())
+        (vector 0) ; Prelude.List
-        (vector 1 '() (car args) (blodwen-build-args (cdr args)))))
+        (vector 1 (car args) (blodwen-build-args (cdr args)))))
     (blodwen-build-args (command-line)))
 (define (blodwen-hasenv var)

support/chicken/support.scm+4−1

 (define b+ (lambda (x y bits) (remainder (+ x y) (expt 2 bits))))
 (define b- (lambda (x y bits) (remainder (- x y) (expt 2 bits))))
 (define b* (lambda (x y bits) (remainder (* x y) (expt 2 bits))))
-(define b/ (lambda (x y bits) (remainder (/ x y) (expt 2 bits))))
+(define b/ (lambda (x y bits) (remainder (exact-floor (/ x y)) (expt 2 bits))))
 (define blodwen-shl (lambda (x y) (arithmetic-shift x y)))
 (define blodwen-shr (lambda (x y) (arithmetic-shift x (- y))))
 (define cast-string-int
   (lambda (x)
     (floor (cast-num (string->number (destroy-prefix x))))))
+(define exact-floor
+  (lambda (x)
+    (inexact->exact (floor x))))
 (define cast-string-double
   (lambda (x)
     (cast-num (string->number (destroy-prefix x)))))

support/racket/support.rkt+5−5

@@ -6,7 +6,7 @@ · 5 unmodified lines
6	(define b+ (lambda (x y bits) (remainder (+ x y) (expt 2 bits))))	6	(define b+ (lambda (x y bits) (remainder (+ x y) (expt 2 bits))))
7	(define b- (lambda (x y bits) (remainder (- x y) (expt 2 bits))))	7	(define b- (lambda (x y bits) (remainder (- x y) (expt 2 bits))))
8	(define b* (lambda (x y bits) (remainder (* x y) (expt 2 bits))))	8	(define b* (lambda (x y bits) (remainder (* x y) (expt 2 bits))))
9	(define b/ (lambda (x y bits) (remainder (/ x y) (expt 2 bits))))	9	(define b/ (lambda (x y bits) (remainder (exact-floor (/ x y)) (expt 2 bits))))
10		10
11	(define blodwen-shl (lambda (x y) (arithmetic-shift x y)))	11	(define blodwen-shl (lambda (x y) (arithmetic-shift x y)))
12	(define blodwen-shr (lambda (x y) (arithmetic-shift x (- y))))	12	(define blodwen-shr (lambda (x y) (arithmetic-shift x (- y))))
@@ -42,11 +42,11 @@ · 29 unmodified lines
42		42
43	(define either-left	43	(define either-left
44	(lambda (x)	44	(lambda (x)
45	(vector 0 #f #f x)))	45	(vector 0 x)))
46		46
47	(define either-right	47	(define either-right
48	(lambda (x)	48	(lambda (x)
49	(vector 1 #f #f x)))	49	(vector 1 x)))
50		50
51	(define blodwen-error-quit	51	(define blodwen-error-quit
52	(lambda (msg)	52	(lambda (msg)
@@ -244,8 +244,8 @@ · 191 unmodified lines
244	(define (blodwen-args)	244	(define (blodwen-args)
245	(define (blodwen-build-args args)	245	(define (blodwen-build-args args)
246	(if (null? args)	246	(if (null? args)
247	(vector 0 '())	247	(vector 0) ; Prelude.List
248	(vector 1 '() (car args) (blodwen-build-args (cdr args)))))	248	(vector 1 (car args) (blodwen-build-args (cdr args)))))
249	(blodwen-build-args	249	(blodwen-build-args
250	(cons (path->string (find-system-path 'run-file))	250	(cons (path->string (find-system-path 'run-file))
251	(vector->list (current-command-line-arguments)))))	251	(vector->list (current-command-line-arguments)))))

tests/Main.idr+6−5

        "lazy001",
        "nest001", "nest002",
        "perf001", "perf002", "perf003",
-       "record001", "record002",
+       "record001", "record002", "record003",
        "rewrite001",
        "qtt001", "qtt002", "qtt003",
        "search001", "search002", "search003", "search004", "search005",
        "params001",
        -- Performance: things which have been slow in the past, or which
        -- pose interesting challenges for the elaborator
-       "perf001", "perf002", "perf003",
+       "perf001", "perf002", "perf003", "perf004",
        -- Parse errors
        "perror001", "perror002", "perror003", "perror004", "perror005",
        "perror006",
        -- interesting interactions between features
        "real001", "real002",
        -- Records, access and dependent update
-       "record001", "record002",
+       "record001", "record002", "record003",
        -- Miscellaneous regressions
        "reg001", "reg002", "reg003", "reg004", "reg005", "reg006", "reg007",
        "reg008", "reg009", "reg010", "reg011", "reg012", "reg013", "reg014",
-       "reg015",
+       "reg015", "reg016",
        -- Totality checking
        "total001", "total002", "total003", "total004", "total005",
        "total006",
 chezTests
    = ["chez001", "chez002", "chez003", "chez004", "chez005", "chez006",
       "chez007", "chez008", "chez009", "chez010", "chez011", "chez012",
-      "chez013", "chez014"]
+      "chez013", "chez014", "chez015", "chez016",
+      "reg001"]
 ideModeTests : List String
 ideModeTests

tests/chez/chez015/Numbers.idr+34−0

@@ -0,0 +1,34 @@
	1	module Main
	2
	3	import Data.List
	4
	5	large : (a: Type) -> a
	6	-- integer larger than 64 bits
	7	large Integer = 3518437212345678901234567890123
	8	-- int close to 2ˆ63
	9	-- we expect some operations will overflow
	10	large Int = 3518437212345678901234567890
	11
	12	small : (a: Type) -> a
	13	small Integer = 437
	14	small Int = 377
	15
	16	numOps : (Num a) => List ( a -> a -> a )
	17	numOps = [ (+), (*) ]
	18
	19	negOps : (Neg a) => List (a -> a -> a)
	20	negOps = [ (-) ]
	21
	22	integralOps : (Integral a) => List (a -> a -> a)
	23	integralOps = [ div, mod ]
	24
	25	binOps : (Num a, Neg a, Integral a) => List (a -> a -> a)
	26	binOps = numOps ++ negOps ++ integralOps
	27
	28	main : IO ()
	29	main = do
	30	putStrLn $ show (results Integer)
	31	putStrLn $ show (results Int)
	32	where
	33	results : (a:Type) -> (Num a, Neg a, Integral a) => List a
	34	results a = map (\ op => large a `op` small a) binOps

tests/chez/chez015/expected+4−0

@@ -0,0 +1,4 @@
	1	[3518437212327232157160858338944, 1537557061787000452679295093927559, 3518437212327232157160858338070, 8051343735302590748651849744, 379]
	2	[8650625671965379659, 5435549321212129090, 8650625671965378905, 365458446121836181, 357]
	3	1/1: Building Numbers (Numbers.idr)
	4	Main> Main> Bye for now!

tests/chez/chez015/input+2−0

@@ -0,0 +1,2 @@
	1	:exec main
	2	:q

tests/chez/chez015/run+3−0

@@ -0,0 +1,3 @@
	1	$1 --no-banner Numbers.idr < input
	2
	3	rm -rf build

tests/chez/chez016/expected+3−0

@@ -0,0 +1,3 @@
	1	Running Chez program located in folder with spaces
	2	1/1: Building Main (Main.idr)
	3	Main> Main> Bye for now!

tests/chez/chez016/folder with spaces/Main.idr+2−0

@@ -0,0 +1,2 @@
	1	main : IO ()
	2	main = putStrLn "Running Chez program located in folder with spaces"

tests/chez/chez016/input+2−0

@@ -0,0 +1,2 @@
	1	:exec main
	2	:q

tests/chez/chez016/run+7−0

@@ -0,0 +1,7 @@
	1	# Get the absolute path to idris2 because we run idris2 from another folder than the current
	2	IDRIS2_EXEC="$(realpath "$1")"
	3
	4	cd "folder with spaces" \|\| exit
	5
	6	"$IDRIS2_EXEC" --no-banner Main.idr < ../input
	7	rm -rf build

tests/chez/reg001/expected+10−0

@@ -0,0 +1,10 @@
	1	3
	2	4.2
	3	"1.2"
	4	4
	5	1
	6	"2.7"
	7	5.9
	8	2
	9	2
	10	2

tests/chez/reg001/numbers.idr+21−0

@@ -0,0 +1,21 @@
	1	-- the commented-out cases are still wrong,
	2	-- but fixing them as well would make other tests fail for mysterious reasons
	3	-- see https://github.com/edwinb/Idris2/pull/281
	4	main : IO ()
	5	main = do
	6	printLn $ 3
	7	printLn $ 4.2
	8	printLn $ "1.2"
	9
	10	printLn $ cast {to = Int} 4.8
	11	printLn $ cast {to = Integer} 1.2
	12	printLn $ cast {to = String} 2.7
	13
	14	-- printLn $ cast {to = Int} "1.2"
	15	-- printLn $ cast {to = Integer} "2.7"
	16	printLn $ cast {to = Double} "5.9"
	17
	18	printLn $ (the Int 6 `div` the Int 3)
	19	printLn $ (the Integer 6 `div` the Integer 3)
	20	printLn $ (cast {to = Int} "6.6" `div` cast "3.9")
	21	-- printLn $ (cast {to = Integer} "6.6" `div` cast "3.9")

tests/chez/reg001/run+3−0

@@ -0,0 +1,3 @@
	1	$1 numbers.idr -x main
	2
	3	rm -rf build

tests/ideMode/ideMode001/expected+1−1

@@ -8,7 +8,7 @@ · 7 unmodified lines
8	0000ed(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 7 18) (:end 7 21)) ((:name "ys") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "(Main.Vect ?{_:192}_[] ?{_:191}_[])")))))) 1)	8	0000ed(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 7 18) (:end 7 21)) ((:name "ys") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "(Main.Vect ?{_:192}_[] ?{_:191}_[])")))))) 1)
9	0000d8(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 6 16) (:end 7 1)) ((:name "ys") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "(Main.Vect m a)")))))) 1)	9	0000d8(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 6 16) (:end 7 1)) ((:name "ys") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "(Main.Vect m a)")))))) 1)
10	0000ed(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 6 11) (:end 6 14)) ((:name "ys") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "(Main.Vect ?{_:182}_[] ?{_:181}_[])")))))) 1)	10	0000ed(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 6 11) (:end 6 14)) ((:name "ys") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "(Main.Vect ?{_:182}_[] ?{_:181}_[])")))))) 1)
11	0001ca(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 5 1) (:end 6 1)) ((:name "Main.append") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "{0 m : Prelude.Nat} -> {0 a : Type} -> {0 n : Prelude.Nat} -> (({arg:172} : (Main.Vect n[0] a[1])) -> (({arg:173} : (Main.Vect m[3] a[2])) -> (Main.Vect (Prelude.+ Prelude.Nat Prelude.Num implementation at Prelude.idr:630:1--637:1 n[2] m[4]) a[3])))")))))) 1)	11	0001ca(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 5 1) (:end 6 1)) ((:name "Main.append") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "{0 m : Prelude.Nat} -> {0 a : Type} -> {0 n : Prelude.Nat} -> (({arg:172} : (Main.Vect n[0] a[1])) -> (({arg:173} : (Main.Vect m[3] a[2])) -> (Main.Vect (Prelude.+ Prelude.Nat Prelude.Num implementation at Prelude.idr:631:1--638:1 n[2] m[4]) a[3])))")))))) 1)
12	0000cb(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 5 47) (:end 6 1)) ((:name "a") (:namespace "") (:decor :type) (:implicit :False) (:key "") (:doc-overview "") (:type "Type")))))) 1)	12	0000cb(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 5 47) (:end 6 1)) ((:name "a") (:namespace "") (:decor :type) (:implicit :False) (:key "") (:doc-overview "") (:type "Type")))))) 1)
13	0000d3(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 5 44) (:end 5 45)) ((:name "m") (:namespace "") (:decor :type) (:implicit :False) (:key "") (:doc-overview "") (:type "Prelude.Nat")))))) 1)	13	0000d3(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 5 44) (:end 5 45)) ((:name "m") (:namespace "") (:decor :type) (:implicit :False) (:key "") (:doc-overview "") (:type "Prelude.Nat")))))) 1)
14	0000d3(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 5 40) (:end 5 42)) ((:name "n") (:namespace "") (:decor :type) (:implicit :False) (:key "") (:doc-overview "") (:type "Prelude.Nat")))))) 1)	14	0000d3(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 5 40) (:end 5 42)) ((:name "n") (:namespace "") (:decor :type) (:implicit :False) (:key "") (:doc-overview "") (:type "Prelude.Nat")))))) 1)

tests/ideMode/ideMode003/expected+1−1

@@ -8,7 +8,7 @@ · 7 unmodified lines
8	0000ed(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 7 18) (:end 7 21)) ((:name "ys") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "(Main.Vect ?{_:192}_[] ?{_:191}_[])")))))) 1)	8	0000ed(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 7 18) (:end 7 21)) ((:name "ys") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "(Main.Vect ?{_:192}_[] ?{_:191}_[])")))))) 1)
9	0000d8(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 6 16) (:end 7 1)) ((:name "ys") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "(Main.Vect m a)")))))) 1)	9	0000d8(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 6 16) (:end 7 1)) ((:name "ys") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "(Main.Vect m a)")))))) 1)
10	0000ed(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 6 11) (:end 6 14)) ((:name "ys") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "(Main.Vect ?{_:182}_[] ?{_:181}_[])")))))) 1)	10	0000ed(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 6 11) (:end 6 14)) ((:name "ys") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "(Main.Vect ?{_:182}_[] ?{_:181}_[])")))))) 1)
11	0001ca(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 5 1) (:end 6 1)) ((:name "Main.append") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "{0 m : Prelude.Nat} -> {0 a : Type} -> {0 n : Prelude.Nat} -> (({arg:172} : (Main.Vect n[0] a[1])) -> (({arg:173} : (Main.Vect m[3] a[2])) -> (Main.Vect (Prelude.+ Prelude.Nat Prelude.Num implementation at Prelude.idr:630:1--637:1 n[2] m[4]) a[3])))")))))) 1)	11	0001ca(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 5 1) (:end 6 1)) ((:name "Main.append") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "{0 m : Prelude.Nat} -> {0 a : Type} -> {0 n : Prelude.Nat} -> (({arg:172} : (Main.Vect n[0] a[1])) -> (({arg:173} : (Main.Vect m[3] a[2])) -> (Main.Vect (Prelude.+ Prelude.Nat Prelude.Num implementation at Prelude.idr:631:1--638:1 n[2] m[4]) a[3])))")))))) 1)
12	0000cb(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 5 47) (:end 6 1)) ((:name "a") (:namespace "") (:decor :type) (:implicit :False) (:key "") (:doc-overview "") (:type "Type")))))) 1)	12	0000cb(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 5 47) (:end 6 1)) ((:name "a") (:namespace "") (:decor :type) (:implicit :False) (:key "") (:doc-overview "") (:type "Type")))))) 1)
13	0000d3(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 5 44) (:end 5 45)) ((:name "m") (:namespace "") (:decor :type) (:implicit :False) (:key "") (:doc-overview "") (:type "Prelude.Nat")))))) 1)	13	0000d3(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 5 44) (:end 5 45)) ((:name "m") (:namespace "") (:decor :type) (:implicit :False) (:key "") (:doc-overview "") (:type "Prelude.Nat")))))) 1)
14	0000d3(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 5 40) (:end 5 42)) ((:name "n") (:namespace "") (:decor :type) (:implicit :False) (:key "") (:doc-overview "") (:type "Prelude.Nat")))))) 1)	14	0000d3(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 5 40) (:end 5 42)) ((:name "n") (:namespace "") (:decor :type) (:implicit :False) (:key "") (:doc-overview "") (:type "Prelude.Nat")))))) 1)

tests/idris2/basic037/Comments.idr+16−0

@@ -1,3 +1,11 @@
		1	{-------------------------}
		2	-- These should be
		3	-- ignored
		4	{- {---------------} -}
		5
		6	-- Comments should have the right to be empty:
		7	--
		8
1	-- This is a valid comment {-	9	-- This is a valid comment {-
2	-- It should not lead to a parse error if nested in a	10	-- It should not lead to a parse error if nested in a
3	-- multiline comment	11	-- multiline comment
@@ -21,3 +29,11 @@ myString = "Similarly, this is a valid string literal {- " · 17 unmodified lines
21	-- So we should be able to put it in a multiline comment	29	-- So we should be able to put it in a multiline comment
22		30
23	-}	31	-}
		32
		33
		34	{------------- Some people {---- like ---}
		35	{- comments with
		36	weird
		37	----------}
		38	closing delimiters
		39	--}

tests/idris2/basic037/Issue279.idr+12−0

@@ -0,0 +1,12 @@
	1	module Main
	2
	3	{-- comment 1 --}
	4
	5	someFunction : IO ()
	6
	7	{-- comment 2 --}
	8
	9	main : IO ()
	10	main = do
	11	someFunction
	12	pure ()

tests/idris2/basic037/expected+2−0

@@ -1,2 +1,4 @@
1	1/1: Building Comments (Comments.idr)	1	1/1: Building Comments (Comments.idr)
2	Main> Bye for now!	2	Main> Bye for now!
		3	1/1: Building Issue279 (Issue279.idr)
		4	Main> Bye for now!

tests/idris2/basic037/run+1−0

@@ -1,3 +1,4 @@
1	echo ':q' \| $1 --no-banner --no-prelude Comments.idr	1	echo ':q' \| $1 --no-banner --no-prelude Comments.idr
		2	echo ':q' \| $1 --no-banner Issue279.idr
2		3
3	rm -rf build	4	rm -rf build

tests/idris2/perf004/bigdpair.idr+30−0

@@ -0,0 +1,30 @@
	1	import Data.Vect
	2
	3	MkBig : Nat -> Type
	4	MkBig Z = Int
	5	MkBig (S k) = ((n ** Vect n Int), MkBig k)
	6
	7	bigEx : (n : Nat) -> MkBig n
	8	bigEx Z = 94
	9	bigEx (S k) = ((2 ** [0,0]), bigEx k)
	10
	11	data VWrap : Type -> Type where
	12	MkVWrap : (0 n : Nat) -> Vect n a -> VWrap a
	13
	14	MkBig' : Nat -> Type
	15	MkBig' Z = Int
	16	MkBig' (S k) = (VWrap Int, MkBig' k)
	17
	18	namespace Foo
	19	public
	20	export
	21	bigEx' : (n : Nat) -> MkBig' n
	22	bigEx' Z = 94
	23	bigEx' (S k) = (MkVWrap 1 [0], bigEx' k)
	24
	25	eqBigs : bigEx 1000000 = bigEx 1000000
	26	eqBigs = Refl
	27
	28	eqBigs' : bigEx' 800000 = bigEx' 800000
	29	eqBigs' = Refl
	30

tests/idris2/perf004/expected+1−0

@@ -0,0 +1 @@
		1	1/1: Building bigdpair (bigdpair.idr)

tests/idris2/perf004/run+3−0

@@ -0,0 +1,3 @@
	1	$1 --check bigdpair.idr
	2
	3	rm -rf build

tests/idris2/record003/Record.idr+33−0

@@ -0,0 +1,33 @@
	1	\|\|\| Test extended record syntax
	2	data NotZero : Nat -> Type where
	3	Is : {n : Nat} -> NotZero (S n)
	4
	5	record Positive (n : Nat) {auto 0 pos : NotZero n} where
	6	constructor Check
	7
	8	a : Positive 1
	9	a = Check
	10
	11	b : Positive 2
	12	b = Check
	13
	14	{- Will not type-check
	15	c : Positive 0
	16	-}
	17
	18	data KindOfString = ASCII \| UTF
	19
	20	UTForASCII : KindOfString -> Type
	21	UTForASCII UTF = String
	22	UTForASCII ASCII = List Char --- Just to demonstrate
	23
	24	record FlexiString { default UTF k : KindOfString} where
	25	constructor MkFlexiString
	26	val : UTForASCII k
	27
	28	c : FlexiString
	29	c = MkFlexiString "hello"
	30
	31	d : FlexiString {k = ASCII}
	32	d = MkFlexiString ['h', 'i']
	33

tests/idris2/record003/expected+1−0

@@ -0,0 +1 @@
		1	1/1: Building Record (Record.idr)

tests/idris2/record003/run+3−0

@@ -0,0 +1,3 @@
	1	$1 -c --no-banner Record.idr
	2
	3	rm -rf build

tests/idris2/reg016/Using.idr+14−0

@@ -0,0 +1,14 @@
	1	module Using
	2
	3	interface MagmaT a where
	4	op: a -> a -> a
	5
	6	interface MagmaT a => SemigroupT a where
	7	assoc: (x, y, z: a) -> (x `op` y) `op` z = x `op` (y `op` z)
	8
	9	[NamedMagma] MagmaT Bool where
	10	False `op` False = False
	11	_ `op` _ = True
	12
	13	[NamedSemigroup] SemigroupT Bool using NamedMagma where
	14	assoc = ?hole

tests/idris2/reg016/expected+1−0

@@ -0,0 +1 @@
		1	1/1: Building Using (Using.idr)

tests/idris2/reg016/run+3−0

@@ -0,0 +1,3 @@
	1	$1 Using.idr --check
	2
	3	rm -rf build

tests/idris2/total006/expected+1−1

@@ -1,6 +1,6 @@
1	1/1: Building Total (Total.idr)	1	1/1: Building Total (Total.idr)
2	Main> Main.count is total	2	Main> Main.count is total
3	Main> Main.badCount is possibly not terminating due to recursive path Main.badCount -> Prelude.Functor implementation at Prelude.idr:873:1--877:1 -> Prelude.map	3	Main> Main.badCount is possibly not terminating due to recursive path Main.badCount -> Prelude.Functor implementation at Prelude.idr:874:1--878:1 -> Prelude.map
4	Main> Main.process is total	4	Main> Main.process is total
5	Main> Main.badProcess is possibly not terminating due to recursive path Main.badProcess -> Main.badProcess -> Main.badProcess	5	Main> Main.badProcess is possibly not terminating due to recursive path Main.badProcess -> Main.badProcess -> Main.badProcess
6	Main> Main.doubleInt is total	6	Main> Main.doubleInt is total

tests/ttimp/record003/Record.yaff+35−0

@@ -0,0 +1,35 @@
	1	data Nat : Type where
	2	Z : Nat
	3	S : Nat -> Nat
	4
	5	data NotZero : Nat -> Type where
	6	Is : {n : Nat} -> NotZero (S n)
	7
	8	record Positive (n : Nat) {auto 0 pos : NotZero n} where
	9	constructor Check
	10
	11	a : Positive (S Z)
	12	a = Check
	13
	14	b : Positive (S (S Z))
	15	b = Check
	16
	17
	18	data KindOfString : Type where
	19	ASCII : KindOfString
	20	UTF : KindOfString
	21
	22	UTForASCII : KindOfString -> Type
	23	UTForASCII UTF = String
	24	UTForASCII ASCII = Nat -- Just as demonstration
	25
	26	record FlexiString { default UTF k : KindOfString} where
	27	constructor MkFlexiString
	28	val : UTForASCII k
	29
	30	c : FlexiString
	31	c = MkFlexiString "hello"
	32
	33	d : FlexiString {k = ASCII}
	34	d = MkFlexiString Z
	35

tests/ttimp/record003/expected+6−0

@@ -0,0 +1,6 @@
	1	Processing as TTImp
	2	Written TTC
	3	Yaffle> Bye for now!
	4	Processing as TTC
	5	Read TTC
	6	Yaffle> Bye for now!

tests/ttimp/record003/input+2−0

@@ -0,0 +1,2 @@
	1	:q
	2

tests/ttimp/record003/run+4−0

@@ -0,0 +1,4 @@
	1	$1 --yaffle Record.yaff < input
	2	$1 --yaffle build/ttc/Record.ttc < input
	3
	4	rm -rf build

Merge remote-tracking branch 'upstream'

Keyboard shortcuts

General

Issues and pull requests

Issues, pull requests and Inbox

Repository code

@@ -7,33 +7,35 @@ Further Reading · 6 unmodified lines
7	Further information about Idris programming, and programming with	7	Further information about Idris programming, and programming with
8	dependent types in general, can be obtained from various sources:	8	dependent types in general, can be obtained from various sources:
9		9
10	- `Type-Driven Development with Idris <https://www.manning.com/books/type-driven-development-with-idris>`_	10	* `Type-Driven Development with Idris <https://www.manning.com/books/type-driven-development-with-idris>`_
11	by Edwin Brady, available from `Manning <https://www.manning.com>`_.	11	by Edwin Brady, available from `Manning <https://www.manning.com>`_.
12		12
13	- The Idris web site (http://www.idris-lang.org/) and by asking	13	* The Idris web site (http://www.idris-lang.org/) and by asking
14	questions on the mailing list.	14	questions on the mailing list.
15		15
16	- The IRC channel ``#idris``, on	16	* The IRC channel ``#idris``, on
17	`webchat.freenode.net <https://webchat.freenode.net/>`__.	17	`webchat.freenode.net <https://webchat.freenode.net/>`__.
18		18
19	- The wiki (https://github.com/idris-lang/Idris-dev/wiki/) has further	19	* The wiki (https://github.com/idris-lang/Idris-dev/wiki/) has further
20	user provided information, in particular:	20	user provided information, in particular:
21		21
22	- https://github.com/idris-lang/Idris-dev/wiki/Manual	22	* https://github.com/idris-lang/Idris-dev/wiki/Manual
23		23
24	- https://github.com/idris-lang/Idris-dev/wiki/Language-Features	24	* https://github.com/idris-lang/Idris-dev/wiki/Language-Features
25		25
26	- Examining the prelude and exploring the ``samples`` in the	26	* Examining the prelude and exploring the ``samples`` in the
27	distribution. The Idris 2 source can be found online at:	27	distribution. The Idris 2 source can be found online at:
28	https://github.com/edwinb/Idris2.	28
		29	* https://github.com/edwinb/Idris2.
29		30
30	- Existing projects on the ``Idris Hackers`` web space:	31	* Existing projects on the ``Idris Hackers`` web space:
31	http://idris-hackers.github.io.	32
		33	* http://idris-hackers.github.io.
32		34
33	- Various papers (e.g. [1]_, [2]_, and [3]_). Although these mostly	35	* Various papers (e.g. [#BradyHammond2012]_, [#Brady]_, and [#BradyHammond2010]_). Although these mostly
34	describe older versions of Idris.	36	describe older versions of Idris.
35		37
36	.. [1] Edwin Brady and Kevin Hammond. 2012. Resource-Safe systems	38	.. [#BradyHammond2012] Edwin Brady and Kevin Hammond. 2012. Resource-Safe systems
37	programming with embedded domain specific languages. In	39	programming with embedded domain specific languages. In
38	Proceedings of the 14th international conference on Practical	40	Proceedings of the 14th international conference on Practical
39	Aspects of Declarative Languages (PADL'12), Claudio Russo and	41	Aspects of Declarative Languages (PADL'12), Claudio Russo and
@@ -41,14 +43,14 @@ dependent types in general, can be obtained from various sources: · 1 unmodified line
41	242-257. DOI=10.1007/978-3-642-27694-1_18	43	242-257. DOI=10.1007/978-3-642-27694-1_18
42	http://dx.doi.org/10.1007/978-3-642-27694-1_18	44	http://dx.doi.org/10.1007/978-3-642-27694-1_18
43		45
44	.. [2] Edwin C. Brady. 2011. IDRIS ---: systems programming meets full	46	.. [#Brady] Edwin C. Brady. 2011. IDRIS ---: systems programming meets full
45	dependent types. In Proceedings of the 5th ACM workshop on	47	dependent types. In Proceedings of the 5th ACM workshop on
46	Programming languages meets program verification (PLPV	48	Programming languages meets program verification (PLPV
47	'11). ACM, New York, NY, USA,	49	'11). ACM, New York, NY, USA,
48	43-54. DOI=10.1145/1929529.1929536	50	43-54. DOI=10.1145/1929529.1929536
49	http://doi.acm.org/10.1145/1929529.1929536	51	http://doi.acm.org/10.1145/1929529.1929536
50		52
51	.. [3] Edwin C. Brady and Kevin Hammond. 2010. Scrapping your	53	.. [#BradyHammond2010] Edwin C. Brady and Kevin Hammond. 2010. Scrapping your
52	inefficient engine: using partial evaluation to improve	54	inefficient engine: using partial evaluation to improve
53	domain-specific language implementation. In Proceedings of the	55	domain-specific language implementation. In Proceedings of the
54	15th ACM SIGPLAN international conference on Functional	56	15th ACM SIGPLAN international conference on Functional