edwinb/Idris2-boot
1
1
Fork 0
mirror of https://github.com/edwinb/Idris2-boot.git synced 2024-09-11 16:05:51 +03:00
Code Issues Projects Releases Wiki Activity

Merge branch 'master' into fix-chez-in-folder-with-spaces

Browse Source
This commit is contained in:
Christian Rasmussen 2020-04-21 15:01:01 +02:00 committed by GitHub
commit 2a3213d10a
No known key found for this signature in database
GPG Key ID: 4AEE18F83AFDEB23
106 changed files with 1383 additions and 1011 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
.gitignore vendored
View File

@ -10,7 +10,7 @@
/dist/idris2.c
/docs/_build/
/docs/build/
/libs/**/build
/tests/**/output

2
INSTALL.md
View File

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

2
README.md
View File

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

191
docs/Makefile
View File

@ -1,183 +1,20 @@
# Makefile for Sphinx documentation
# Minimal makefile for Sphinx documentation
#
# You can set these variables from the command line.
SPHINXOPTS =
SPHINXBUILD = sphinx-build
PAPER =
BUILDDIR = _build
# User-friendly check for sphinx-build
ifeq ($(shell which $(SPHINXBUILD) >/dev/null 2>&1; echo $$?), 1)
$(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/)
endif
# Internal variables.
PAPEROPT_a4 = -D latex_paper_size=a4
PAPEROPT_letter = -D latex_paper_size=letter
ALLSPHINXOPTS = -d $(BUILDDIR)/doctrees $(PAPEROPT_$(PAPER)) $(SPHINXOPTS) .
# the i18n builder cannot share the environment and doctrees with the others
I18NSPHINXOPTS = $(PAPEROPT_$(PAPER)) $(SPHINXOPTS) .
.PHONY: help clean html dirhtml singlehtml pickle json htmlhelp qthelp devhelp epub latex latexpdf text man changes linkcheck doctest coverage gettext
# You can set these variables from the command line, and also
# from the environment for the first two.
SPHINXOPTS ?=
SPHINXBUILD ?= sphinx-build
SOURCEDIR = source
BUILDDIR = build
# Put it first so that "make" without argument is like "make help".
help:
@echo "Please use \`make <target>' where <target> is one of"
@echo " html to make standalone HTML files"
@echo " dirhtml to make HTML files named index.html in directories"
@echo " singlehtml to make a single large HTML file"
@echo " pickle to make pickle files"
@echo " json to make JSON files"
@echo " htmlhelp to make HTML files and a HTML help project"
@echo " qthelp to make HTML files and a qthelp project"
@echo " devhelp to make HTML files and a Devhelp project"
@echo " epub to make an epub"
@echo " latex to make LaTeX files, you can set PAPER=a4 or PAPER=letter"
@echo " latexpdf to make LaTeX files and run them through pdflatex"
@echo " latexpdfja to make LaTeX files and run them through platex/dvipdfmx"
@echo " text to make text files"
@echo " man to make manual pages"
@echo " texinfo to make Texinfo files"
@echo " info to make Texinfo files and run them through makeinfo"
@echo " gettext to make PO message catalogs"
@echo " changes to make an overview of all changed/added/deprecated items"
@echo " xml to make Docutils-native XML files"
@echo " pseudoxml to make pseudoxml-XML files for display purposes"
@echo " linkcheck to check all external links for integrity"
@echo " doctest to run all doctests embedded in the documentation (if enabled)"
@echo " coverage to run coverage check of the documentation (if enabled)"
@$(SPHINXBUILD) -M help "$(SOURCEDIR)" "$(BUILDDIR)" $(SPHINXOPTS) $(O)
clean:
rm -rf $(BUILDDIR)/*
.PHONY: help Makefile
html:
$(SPHINXBUILD) -b html $(ALLSPHINXOPTS) $(BUILDDIR)/html
@echo
@echo "Build finished. The HTML pages are in $(BUILDDIR)/html."
dirhtml:
$(SPHINXBUILD) -b dirhtml $(ALLSPHINXOPTS) $(BUILDDIR)/dirhtml
@echo
@echo "Build finished. The HTML pages are in $(BUILDDIR)/dirhtml."
singlehtml:
$(SPHINXBUILD) -b singlehtml $(ALLSPHINXOPTS) $(BUILDDIR)/singlehtml
@echo
@echo "Build finished. The HTML page is in $(BUILDDIR)/singlehtml."
pickle:
$(SPHINXBUILD) -b pickle $(ALLSPHINXOPTS) $(BUILDDIR)/pickle
@echo
@echo "Build finished; now you can process the pickle files."
json:
$(SPHINXBUILD) -b json $(ALLSPHINXOPTS) $(BUILDDIR)/json
@echo
@echo "Build finished; now you can process the JSON files."
htmlhelp:
$(SPHINXBUILD) -b htmlhelp $(ALLSPHINXOPTS) $(BUILDDIR)/htmlhelp
@echo
@echo "Build finished; now you can run HTML Help Workshop with the" \
".hhp project file in $(BUILDDIR)/htmlhelp."
qthelp:
$(SPHINXBUILD) -b qthelp $(ALLSPHINXOPTS) $(BUILDDIR)/qthelp
@echo
@echo "Build finished; now you can run "qcollectiongenerator" with the" \
".qhcp project file in $(BUILDDIR)/qthelp, like this:"
@echo "# qcollectiongenerator $(BUILDDIR)/qthelp/IdrisManual.qhcp"
@echo "To view the help file:"
@echo "# assistant -collectionFile $(BUILDDIR)/qthelp/IdrisManual.qhc"
devhelp:
$(SPHINXBUILD) -b devhelp $(ALLSPHINXOPTS) $(BUILDDIR)/devhelp
@echo
@echo "Build finished."
@echo "To view the help file:"
@echo "# mkdir -p $$HOME/.local/share/devhelp/IdrisManual"
@echo "# ln -s $(BUILDDIR)/devhelp $$HOME/.local/share/devhelp/IdrisManual"
@echo "# devhelp"
epub:
$(SPHINXBUILD) -b epub $(ALLSPHINXOPTS) $(BUILDDIR)/epub
@echo
@echo "Build finished. The epub file is in $(BUILDDIR)/epub."
latex:
$(SPHINXBUILD) -b latex $(ALLSPHINXOPTS) $(BUILDDIR)/latex
@echo
@echo "Build finished; the LaTeX files are in $(BUILDDIR)/latex."
@echo "Run \`make' in that directory to run these through (pdf)latex" \
"(use \`make latexpdf' here to do that automatically)."
latexpdf:
$(SPHINXBUILD) -b latex $(ALLSPHINXOPTS) $(BUILDDIR)/latex
@echo "Running LaTeX files through pdflatex..."
$(MAKE) -C $(BUILDDIR)/latex all-pdf
@echo "pdflatex finished; the PDF files are in $(BUILDDIR)/latex."
latexpdfja:
$(SPHINXBUILD) -b latex $(ALLSPHINXOPTS) $(BUILDDIR)/latex
@echo "Running LaTeX files through platex and dvipdfmx..."
$(MAKE) -C $(BUILDDIR)/latex all-pdf-ja
@echo "pdflatex finished; the PDF files are in $(BUILDDIR)/latex."
text:
$(SPHINXBUILD) -b text $(ALLSPHINXOPTS) $(BUILDDIR)/text
@echo
@echo "Build finished. The text files are in $(BUILDDIR)/text."
man:
$(SPHINXBUILD) -b man $(ALLSPHINXOPTS) $(BUILDDIR)/man
@echo
@echo "Build finished. The manual pages are in $(BUILDDIR)/man."
texinfo:
$(SPHINXBUILD) -b texinfo $(ALLSPHINXOPTS) $(BUILDDIR)/texinfo
@echo
@echo "Build finished. The Texinfo files are in $(BUILDDIR)/texinfo."
@echo "Run \`make' in that directory to run these through makeinfo" \
"(use \`make info' here to do that automatically)."
info:
$(SPHINXBUILD) -b texinfo $(ALLSPHINXOPTS) $(BUILDDIR)/texinfo
@echo "Running Texinfo files through makeinfo..."
make -C $(BUILDDIR)/texinfo info
@echo "makeinfo finished; the Info files are in $(BUILDDIR)/texinfo."
gettext:
$(SPHINXBUILD) -b gettext $(I18NSPHINXOPTS) $(BUILDDIR)/locale
@echo
@echo "Build finished. The message catalogs are in $(BUILDDIR)/locale."
changes:
$(SPHINXBUILD) -b changes $(ALLSPHINXOPTS) $(BUILDDIR)/changes
@echo
@echo "The overview file is in $(BUILDDIR)/changes."
linkcheck:
$(SPHINXBUILD) -b linkcheck $(ALLSPHINXOPTS) $(BUILDDIR)/linkcheck
@echo
@echo "Link check complete; look for any errors in the above output " \
"or in $(BUILDDIR)/linkcheck/output.txt."
doctest:
$(SPHINXBUILD) -b doctest $(ALLSPHINXOPTS) $(BUILDDIR)/doctest
@echo "Testing of doctests in the sources finished, look at the " \
"results in $(BUILDDIR)/doctest/output.txt."
coverage:
$(SPHINXBUILD) -b coverage $(ALLSPHINXOPTS) $(BUILDDIR)/coverage
@echo "Testing of coverage in the sources finished, look at the " \
"results in $(BUILDDIR)/coverage/python.txt."
xml:
$(SPHINXBUILD) -b xml $(ALLSPHINXOPTS) $(BUILDDIR)/xml
@echo
@echo "Build finished. The XML files are in $(BUILDDIR)/xml."
pseudoxml:
$(SPHINXBUILD) -b pseudoxml $(ALLSPHINXOPTS) $(BUILDDIR)/pseudoxml
@echo
@echo "Build finished. The pseudo-XML files are in $(BUILDDIR)/pseudoxml."
# Catch-all target: route all unknown targets to Sphinx using the new
# "make mode" option. $(O) is meant as a shortcut for $(SPHINXOPTS).
%: Makefile
@$(SPHINXBUILD) -M $@ "$(SOURCEDIR)" "$(BUILDDIR)" $(SPHINXOPTS) $(O)

7
docs/README.md
View File

@ -11,6 +11,7 @@ To build the manual the following dependencies must be met. We assume that you h
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
@ -18,9 +19,12 @@ Sphinx can be installed either through your hosts package manager or using pip/e
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
```
@ -32,6 +36,7 @@ LaTeX can be install either using your systems package manager or direct from Te
## Build Instructions
```sh
cd docs
make html
make latexpdf
```

298
docs/make.bat
View File

@ -1,263 +1,35 @@
@ECHO OFF
REM Command file for Sphinx documentation
if "%SPHINXBUILD%" == "" (
set SPHINXBUILD=sphinx-build
)
set BUILDDIR=_build
set ALLSPHINXOPTS=-d %BUILDDIR%/doctrees %SPHINXOPTS% .
set I18NSPHINXOPTS=%SPHINXOPTS% .
if NOT "%PAPER%" == "" (
set ALLSPHINXOPTS=-D latex_paper_size=%PAPER% %ALLSPHINXOPTS%
set I18NSPHINXOPTS=-D latex_paper_size=%PAPER% %I18NSPHINXOPTS%
)
if "%1" == "" goto help
if "%1" == "help" (
:help
echo.Please use `make ^<target^>` where ^<target^> is one of
echo. html to make standalone HTML files
echo. dirhtml to make HTML files named index.html in directories
echo. singlehtml to make a single large HTML file
echo. pickle to make pickle files
echo. json to make JSON files
echo. htmlhelp to make HTML files and a HTML help project
echo. qthelp to make HTML files and a qthelp project
echo. devhelp to make HTML files and a Devhelp project
echo. epub to make an epub
echo. latex to make LaTeX files, you can set PAPER=a4 or PAPER=letter
echo. text to make text files
echo. man to make manual pages
echo. texinfo to make Texinfo files
echo. gettext to make PO message catalogs
echo. changes to make an overview over all changed/added/deprecated items
echo. xml to make Docutils-native XML files
echo. pseudoxml to make pseudoxml-XML files for display purposes
echo. linkcheck to check all external links for integrity
echo. doctest to run all doctests embedded in the documentation if enabled
echo. coverage to run coverage check of the documentation if enabled
goto end
)
if "%1" == "clean" (
for /d %%i in (%BUILDDIR%\*) do rmdir /q /s %%i
del /q /s %BUILDDIR%\*
goto end
)
REM Check if sphinx-build is available and fallback to Python version if any
%SPHINXBUILD% 2> nul
if errorlevel 9009 goto sphinx_python
goto sphinx_ok
:sphinx_python
set SPHINXBUILD=python -m sphinx.__init__
%SPHINXBUILD% 2> nul
if errorlevel 9009 (
echo.
echo.The 'sphinx-build' command was not found. Make sure you have Sphinx
echo.installed, then set the SPHINXBUILD environment variable to point
echo.to the full path of the 'sphinx-build' executable. Alternatively you
echo.may add the Sphinx directory to PATH.
echo.
echo.If you don't have Sphinx installed, grab it from
echo.https://www.sphinx-doc.org/
exit /b 1
)
:sphinx_ok
if "%1" == "html" (
%SPHINXBUILD% -b html %ALLSPHINXOPTS% %BUILDDIR%/html
if errorlevel 1 exit /b 1
echo.
echo.Build finished. The HTML pages are in %BUILDDIR%/html.
goto end
)
if "%1" == "dirhtml" (
%SPHINXBUILD% -b dirhtml %ALLSPHINXOPTS% %BUILDDIR%/dirhtml
if errorlevel 1 exit /b 1
echo.
echo.Build finished. The HTML pages are in %BUILDDIR%/dirhtml.
goto end
)
if "%1" == "singlehtml" (
%SPHINXBUILD% -b singlehtml %ALLSPHINXOPTS% %BUILDDIR%/singlehtml
if errorlevel 1 exit /b 1
echo.
echo.Build finished. The HTML pages are in %BUILDDIR%/singlehtml.
goto end
)
if "%1" == "pickle" (
%SPHINXBUILD% -b pickle %ALLSPHINXOPTS% %BUILDDIR%/pickle
if errorlevel 1 exit /b 1
echo.
echo.Build finished; now you can process the pickle files.
goto end
)
if "%1" == "json" (
%SPHINXBUILD% -b json %ALLSPHINXOPTS% %BUILDDIR%/json
if errorlevel 1 exit /b 1
echo.
echo.Build finished; now you can process the JSON files.
goto end
)
if "%1" == "htmlhelp" (
%SPHINXBUILD% -b htmlhelp %ALLSPHINXOPTS% %BUILDDIR%/htmlhelp
if errorlevel 1 exit /b 1
echo.
echo.Build finished; now you can run HTML Help Workshop with the ^
.hhp project file in %BUILDDIR%/htmlhelp.
goto end
)
if "%1" == "qthelp" (
%SPHINXBUILD% -b qthelp %ALLSPHINXOPTS% %BUILDDIR%/qthelp
if errorlevel 1 exit /b 1
echo.
echo.Build finished; now you can run "qcollectiongenerator" with the ^
.qhcp project file in %BUILDDIR%/qthelp, like this:
echo.^> qcollectiongenerator %BUILDDIR%\qthelp\IdrisManual.qhcp
echo.To view the help file:
echo.^> assistant -collectionFile %BUILDDIR%\qthelp\IdrisManual.ghc
goto end
)
if "%1" == "devhelp" (
%SPHINXBUILD% -b devhelp %ALLSPHINXOPTS% %BUILDDIR%/devhelp
if errorlevel 1 exit /b 1
echo.
echo.Build finished.
goto end
)
if "%1" == "epub" (
%SPHINXBUILD% -b epub %ALLSPHINXOPTS% %BUILDDIR%/epub
if errorlevel 1 exit /b 1
echo.
echo.Build finished. The epub file is in %BUILDDIR%/epub.
goto end
)
if "%1" == "latex" (
%SPHINXBUILD% -b latex %ALLSPHINXOPTS% %BUILDDIR%/latex
if errorlevel 1 exit /b 1
echo.
echo.Build finished; the LaTeX files are in %BUILDDIR%/latex.
goto end
)
if "%1" == "latexpdf" (
%SPHINXBUILD% -b latex %ALLSPHINXOPTS% %BUILDDIR%/latex
cd %BUILDDIR%/latex
make all-pdf
cd %~dp0
echo.
echo.Build finished; the PDF files are in %BUILDDIR%/latex.
goto end
)
if "%1" == "latexpdfja" (
%SPHINXBUILD% -b latex %ALLSPHINXOPTS% %BUILDDIR%/latex
cd %BUILDDIR%/latex
make all-pdf-ja
cd %~dp0
echo.
echo.Build finished; the PDF files are in %BUILDDIR%/latex.
goto end
)
if "%1" == "text" (
%SPHINXBUILD% -b text %ALLSPHINXOPTS% %BUILDDIR%/text
if errorlevel 1 exit /b 1
echo.
echo.Build finished. The text files are in %BUILDDIR%/text.
goto end
)
if "%1" == "man" (
%SPHINXBUILD% -b man %ALLSPHINXOPTS% %BUILDDIR%/man
if errorlevel 1 exit /b 1
echo.
echo.Build finished. The manual pages are in %BUILDDIR%/man.
goto end
)
if "%1" == "texinfo" (
%SPHINXBUILD% -b texinfo %ALLSPHINXOPTS% %BUILDDIR%/texinfo
if errorlevel 1 exit /b 1
echo.
echo.Build finished. The Texinfo files are in %BUILDDIR%/texinfo.
goto end
)
if "%1" == "gettext" (
%SPHINXBUILD% -b gettext %I18NSPHINXOPTS% %BUILDDIR%/locale
if errorlevel 1 exit /b 1
echo.
echo.Build finished. The message catalogs are in %BUILDDIR%/locale.
goto end
)
if "%1" == "changes" (
%SPHINXBUILD% -b changes %ALLSPHINXOPTS% %BUILDDIR%/changes
if errorlevel 1 exit /b 1
echo.
echo.The overview file is in %BUILDDIR%/changes.
goto end
)
if "%1" == "linkcheck" (
%SPHINXBUILD% -b linkcheck %ALLSPHINXOPTS% %BUILDDIR%/linkcheck
if errorlevel 1 exit /b 1
echo.
echo.Link check complete; look for any errors in the above output ^
or in %BUILDDIR%/linkcheck/output.txt.
goto end
)
if "%1" == "doctest" (
%SPHINXBUILD% -b doctest %ALLSPHINXOPTS% %BUILDDIR%/doctest
if errorlevel 1 exit /b 1
echo.
echo.Testing of doctests in the sources finished, look at the ^
results in %BUILDDIR%/doctest/output.txt.
goto end
)
if "%1" == "coverage" (
%SPHINXBUILD% -b coverage %ALLSPHINXOPTS% %BUILDDIR%/coverage
if errorlevel 1 exit /b 1
echo.
echo.Testing of coverage in the sources finished, look at the ^
results in %BUILDDIR%/coverage/python.txt.
goto end
)
if "%1" == "xml" (
%SPHINXBUILD% -b xml %ALLSPHINXOPTS% %BUILDDIR%/xml
if errorlevel 1 exit /b 1
echo.
echo.Build finished. The XML files are in %BUILDDIR%/xml.
goto end
)
if "%1" == "pseudoxml" (
%SPHINXBUILD% -b pseudoxml %ALLSPHINXOPTS% %BUILDDIR%/pseudoxml
if errorlevel 1 exit /b 1
echo.
echo.Build finished. The pseudo-XML files are in %BUILDDIR%/pseudoxml.
goto end
)
:end
@ECHO OFF
pushd %~dp0
REM Command file for Sphinx documentation
if "%SPHINXBUILD%" == "" (
set SPHINXBUILD=sphinx-build
)
set SOURCEDIR=source
set BUILDDIR=build
if "%1" == "" goto help
%SPHINXBUILD% >NUL 2>NUL
if errorlevel 9009 (
echo.
echo.The 'sphinx-build' command was not found. Make sure you have Sphinx
echo.installed, then set the SPHINXBUILD environment variable to point
echo.to the full path of the 'sphinx-build' executable. Alternatively you
echo.may add the Sphinx directory to PATH.
echo.
echo.If you don't have Sphinx installed, grab it from
echo.http://sphinx-doc.org/
exit /b 1
)
%SPHINXBUILD% -M %1 %SOURCEDIR% %BUILDDIR% %SPHINXOPTS% %O%
goto end
:help
%SPHINXBUILD% -M help %SOURCEDIR% %BUILDDIR% %SPHINXOPTS% %O%
:end
popd

2
docs/app/index.rst → docs/source/app/index.rst
View File

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

0
docs/backends/chez.rst → docs/source/backends/chez.rst
View File

0
docs/backends/index.rst → docs/source/backends/index.rst
View File

0
docs/backends/racket.rst → docs/source/backends/racket.rst
View File

215
docs/conf.py → docs/source/conf.py
View File

@ -1,32 +1,42 @@
# -*- coding: utf-8 -*-
# Configuration file for the Sphinx documentation builder.
#
# Idris Manual documentation build configuration file, created by
# sphinx-quickstart on Sat Feb 28 20:41:47 2015.
# Idris Manual documentation build configuration file, created by
# sphinx-quickstart on Apr 13, 2020.
#
# This file is execfile()d with the current directory set to its
# containing dir.
#
# Note that not all possible configuration values are present in this
# autogenerated file.
#
# All configuration values have a default; values that are commented out
# serve to show the default.
# This file only contains a selection of the most common options. For a full
# list see the documentation:
# https://www.sphinx-doc.org/en/master/usage/configuration.html
import sys
import os
# True if the readthedocs theme is locally installed
on_rtd = os.environ.get('READTHEDOCS', None) == 'True'
# -- Path setup --------------------------------------------------------------
# If extensions (or modules to document with autodoc) are in another directory,
# add these directories to sys.path here. If the directory is relative to the
# documentation root, use os.path.abspath to make it absolute, like shown here.
#sys.path.insert(0, os.path.abspath('.'))
#
import os
import sys
import sphinx_rtd_theme
# sys.path.insert(0, os.path.abspath('.'))
# -- General configuration ------------------------------------------------
# If your documentation needs a minimal Sphinx version, state it here.
#needs_sphinx = '1.0'
# -- Project information -----------------------------------------------------
# General information about the project.
project = 'Idris2'
copyright = '2020, The Idris Community'
author = 'The Idris Community'
# The short X.Y version.
version = '0.0'
# The full version, including alpha/beta/rc tags
release = '0.0'
# -- General configuration ---------------------------------------------------
# Add any Sphinx extension module names here, as strings. They can be
# extensions coming with Sphinx (named 'sphinx.ext.*') or your custom
@ -35,183 +45,40 @@ extensions = [
'sphinx.ext.todo',
# 'sphinx.ext.pngmath', # imgmath is not supported on readthedocs.
'sphinx.ext.ifconfig',
'recommonmark'
"sphinx_rtd_theme",
]
# Add any paths that contain templates here, relative to this directory.
templates_path = ['_templates']
# The suffix of source filenames.
source_suffix = ['.rst','.md']
# List of patterns, relative to source directory, that match files and
# directories to ignore when looking for source files.
# This pattern also affects html_static_path and html_extra_path.
exclude_patterns = []
# The encoding of source files.
#source_encoding = 'utf-8-sig'
# -- Options for HTML output -------------------------------------------------
# The master toctree document.
master_doc = 'index'
# General information about the project.
project = u'Idris2'
copyright = u'2019, The Idris Community'
author = u'The Idris Community'
# The version info for the project you're documenting, acts as replacement for
# |version| and |release|, also used in various other places throughout the
# built documents.
#
# The short X.Y version.
version = '0.0'
# The full version, including alpha/beta/rc tags.
release = '0.0'
# The language for content autogenerated by Sphinx. Refer to documentation
# for a list of supported languages.
#
# This is also used if you do content translation via gettext catalogs.
# Usually you set "language" from the command line for these cases.
language = None
# There are two options for replacing |today|: either, you set today to some
# non-false value, then it is used:
#today = ''
# Else, today_fmt is used as the format for a strftime call.
#today_fmt = '%B %d, %Y'
# List of patterns, relative to source directory, that match files and
# directories to ignore when looking for source files.
exclude_patterns = ['_build']
# The reST default role (used for this markup: `text`) to use for all
# documents.
#default_role = None
# If true, '()' will be appended to :func: etc. cross-reference text.
#add_function_parentheses = True
# If true, the current module name will be prepended to all description
# unit titles (such as .. function::).
#add_module_names = True
# If true, sectionauthor and moduleauthor directives will be shown in the
# output. They are ignored by default.
#show_authors = False
# The name of the Pygments (syntax highlighting) style to use.
pygments_style = 'sphinx'
# A list of ignored prefixes for module index sorting.
#modindex_common_prefix = []
# If true, keep warnings as "system message" paragraphs in the built documents.
#keep_warnings = False
# If true, `todo` and `todoList` produce output, else they produce nothing.
todo_include_todos = True
# -- Options for HTML output ----------------------------------------------
# The theme to use for HTML and HTML Help pages. See the documentation for
# a list of builtin themes.
html_theme = "default"
# # Read The Docs Themes specific settings
html_theme = 'sphinx_rtd_theme'
html_theme_options = {
'display_version': True,
'prev_next_buttons_location': 'bottom'
}
if not on_rtd: # only import and set the theme if we're building docs locally
try:
import sphinx_rtd_theme
html_theme = 'sphinx_rtd_theme'
html_theme_path = [sphinx_rtd_theme.get_html_theme_path()]
except ImportError:
html_theme = "default"
# Theme options are theme-specific and customize the look and feel of a theme
# further. For a list of options available for each theme, see the
# documentation.
#html_theme_options = {}
# Add any paths that contain custom themes here, relative to this directory.
#html_theme_path = []
# The name for this set of Sphinx documents. If None, it defaults to
# "<project> v<release> documentation".
#html_title = None
# A shorter title for the navigation bar. Default is the same as html_title.
#html_short_title = None
# The name of an image file (relative to this directory) to place at the top
# of the sidebar.
#html_logo = None
# The name of an image file (within the static path) to use as favicon of the
# docs. This file should be a Windows icon file (.ico) being 16x16 or 32x32
# pixels large.
#html_favicon = None
# Add any paths that contain custom static files (such as style sheets) here,
# relative to this directory. They are copied after the builtin static files,
# so a file named "default.css" will overwrite the builtin "default.css".
html_static_path = ['_static']
# Add any extra paths that contain custom files (such as robots.txt or
# .htaccess) here, relative to this directory. These files are copied
# directly to the root of the documentation.
#html_extra_path = []
# If not '', a 'Last updated on:' timestamp is inserted at every page bottom,
# using the given strftime format.
#html_last_updated_fmt = '%b %d, %Y'
# If true, SmartyPants will be used to convert quotes and dashes to
# typographically correct entities.
#html_use_smartypants = True
# Custom sidebar templates, maps document names to template names.
#html_sidebars = {}
# Additional templates that should be rendered to pages, maps page names to
# template names.
#html_additional_pages = {}
# If false, no module index is generated.
#html_domain_indices = True
# If false, no index is generated.
#html_use_index = True
# If true, the index is split into individual pages for each letter.
#html_split_index = False
# If true, links to the reST sources are added to the pages.
#html_show_sourcelink = True
# If true, "Created using Sphinx" is shown in the HTML footer. Default is True.
#html_show_sphinx = True
# If true, "(C) Copyright ..." is shown in the HTML footer. Default is True.
#html_show_copyright = True
# If true, an OpenSearch description file will be output, and all pages will
# contain a <link> tag referring to it. The value of this option must be the
# base URL from which the finished HTML is served.
#html_use_opensearch = ''
# This is the file name suffix for HTML files (e.g. ".xhtml").
#html_file_suffix = None
# Language to be used for generating the HTML full-text search index.
# Sphinx supports the following languages:
# 'da', 'de', 'en', 'es', 'fi', 'fr', 'hu', 'it', 'ja'
# 'nl', 'no', 'pt', 'ro', 'ru', 'sv', 'tr'
#html_search_language = 'en'
# A dictionary with options for the search language support, empty by default.
# Now only 'ja' uses this config value
#html_search_options = {'type': 'default'}
# The name of a javascript file (relative to the configuration directory) that
# implements a search results scorer. If empty, the default will be used.
#html_search_scorer = 'scorer.js'
# Output file base name for HTML help builder.
htmlhelp_basename = 'IdrisManualdoc'
@ -305,7 +172,7 @@ latex_show_url = 'footnote'
# The name of an image file (relative to this directory) to place at the top of
# the title page.
latex_logo = '../icons/idris-512x512.png'
latex_logo = '../../icons/idris-512x512.png'
# For "manual" documents, if this is true, then toplevel headings are parts,
# not chapters.

0
docs/faq/faq.rst → docs/source/faq/faq.rst
View File

0
docs/ffi/ffi.rst → docs/source/ffi/ffi.rst
View File

0
docs/ffi/index.rst → docs/source/ffi/index.rst
View File

0
docs/ffi/readline.rst → docs/source/ffi/readline.rst
View File

0
docs/index.rst → docs/source/index.rst
View File

0
docs/listing/idris-prompt-helloworld.txt → docs/source/listing/idris-prompt-helloworld.txt
View File

0
docs/listing/idris-prompt-interp.txt → docs/source/listing/idris-prompt-interp.txt
View File

0
docs/listing/idris-prompt-start.txt → docs/source/listing/idris-prompt-start.txt
View File

0
docs/proofs/definitional.rst → docs/source/proofs/definitional.rst
View File

0
docs/proofs/index.rst → docs/source/proofs/index.rst
View File

0
docs/proofs/inductive.rst → docs/source/proofs/inductive.rst
View File

0
docs/proofs/patterns.rst → docs/source/proofs/patterns.rst
View File

0
docs/proofs/pluscomm.rst → docs/source/proofs/pluscomm.rst
View File

0
docs/proofs/propositional.rst → docs/source/proofs/propositional.rst
View File

0
docs/reference/envvars.rst → docs/source/reference/envvars.rst
View File

0
docs/reference/index.rst → docs/source/reference/index.rst
View File

0
docs/reference/packages.rst → docs/source/reference/packages.rst
View File

30
docs/tutorial/conclusions.rst → docs/source/tutorial/conclusions.rst
View File

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

0
docs/tutorial/index.rst → docs/source/tutorial/index.rst
View File

2
docs/tutorial/interactive.rst → docs/source/tutorial/interactive.rst
View File

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

20
docs/tutorial/interfaces.rst → docs/source/tutorial/interfaces.rst
View File

@ -164,7 +164,7 @@ see this at the REPL:
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
@ -282,11 +282,13 @@ which reads a number from the console, returning a value of the form
.. 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
@ -325,9 +327,9 @@ case back as follows:
readNumbers : IO (Maybe (Nat, Nat))
readNumbers
= do Just x_ok <- readNumber
= do Just x_ok <- readNumber
| Nothing => pure Nothing
Just y_ok <- readNumber
Just y_ok <- readNumber
| Nothing => pure Nothing
pure (Just (x_ok, y_ok))
@ -432,7 +434,7 @@ Idiom brackets
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
@ -468,19 +470,19 @@ above (this is defined in the Idris library):
_ <*> _ = 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
@ -653,7 +655,7 @@ is declared with the ``| m`` after the interface declaration. We call ``m`` a
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

0
docs/tutorial/interp.rst → docs/source/tutorial/interp.rst
View File

9
docs/tutorial/introduction.rst → docs/source/tutorial/introduction.rst
View File

@ -21,7 +21,7 @@ In a language with *dependent types*, however, the distinction is less
clear. Dependent types allow types to “depend” on values — in other
words, types are a *first class* language construct and can be
manipulated like any other value. The standard example is the type of
lists of a given length [1]_, ``Vect n a``, where ``a`` is the element
lists of a given length [#fn1]_, ``Vect n a``, where ``a`` is the element
type and ``n`` is the length of the list and can be an arbitrary term.
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
``samples``. It is, however, strongly recommended that you type
them in yourself, rather than simply loading and reading them.
.. [1]
Typically, and perhaps confusingly, referred to in the dependently
typed programming literature as “vectors”
.. rubric:: Footnotes
.. [#fn1] Typically, and perhaps confusingly, referred to in the dependently
typed programming literature as "vectors".

6
docs/tutorial/miscellany.rst → docs/source/tutorial/miscellany.rst
View File

@ -14,7 +14,7 @@ Implicit arguments
==================
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
@ -101,6 +101,7 @@ literate programs, everything is assumed to be a comment unless the line
begins with a greater than sign ``>``, for example:
.. code-block:: literate-idris
:force:
> module literate
@ -161,5 +162,4 @@ The application of ``myid`` to itself leads to a cycle in the universe
hierarchy — ``myid``\ ’s first argument is a ``Type``, which cannot be
at a lower level than required if it is applied to itself.
.. [1]
https://github.com/david-christiansen/idris-type-providers
.. [#IdrisType] https://github.com/david-christiansen/idris-type-providers

1
docs/tutorial/modules.rst → docs/source/tutorial/modules.rst
View File

@ -148,6 +148,7 @@ Additionally, a module can re-export a module it has imported, by using
the ``public`` modifier on an ``import``. For example:
.. code-block:: idris
:force:
module A

2
docs/tutorial/multiplicities.rst → docs/source/tutorial/multiplicities.rst
View File

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

0
docs/tutorial/packages.rst → docs/source/tutorial/packages.rst
View File

0
docs/tutorial/starting.rst → docs/source/tutorial/starting.rst
View File

4
docs/tutorial/theorems.rst → docs/source/tutorial/theorems.rst
View File

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

10
docs/tutorial/typesfuns.rst → docs/source/tutorial/typesfuns.rst
View File

@ -221,12 +221,12 @@ of how this works in practice:
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
@ -753,12 +753,8 @@ For more details of the functions available on ``List`` and
- ``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
@ -1052,7 +1048,7 @@ name. For example, a pair type could be defined as follows:
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:

4
docs/tutorial/views.rst → docs/source/tutorial/views.rst
View File

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

0
docs/typedd/typedd.rst → docs/source/typedd/typedd.rst
View File

4
docs/updates/updates.rst → docs/source/updates/updates.rst
View File

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

1
idris2.ipkg
View File

@ -4,6 +4,7 @@ modules =
Compiler.Common,
Compiler.CompileExpr,
Compiler.Inline,
Compiler.LambdaLift,
Compiler.Scheme.Chez,
-- Compiler.Scheme.Chicken,
Compiler.Scheme.Racket,

12
libs/network/Network/Socket/Raw.idr
View File

@ -23,7 +23,18 @@ data SockaddrPtr = SAPtr AnyPtr
-- ---------------------------------------------------------- [ 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]
@ -34,6 +45,7 @@ sockaddr_free (SAPtr 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]

10
libs/network/idris_net.c
View File

@ -56,6 +56,16 @@ void idrnet_free(void* ptr) {
free(ptr);
}
unsigned int idrnet_peek(void *ptr, unsigned int offset) {
unsigned char *buf_c = (unsigned char*) ptr;
return (unsigned int) buf_c[offset];
}
void idrnet_poke(void *ptr, unsigned int offset, char val) {
char *buf_c = (char*)ptr;
buf_c[offset] = val;
}
int idrnet_socket(int domain, int type, int protocol) {
#ifdef _WIN32

2
libs/network/idris_net.h
View File

@ -31,6 +31,8 @@ typedef struct idrnet_recvfrom_result {
// Memory management functions
void* idrnet_malloc(int size);
void idrnet_free(void* ptr);
unsigned int idrnet_peek(void *ptr, unsigned int offset);
void idrnet_poke(void *ptr, unsigned int offset, char val);
// Gets value of errno
int idrnet_errno();

15
libs/network/test.c
View File

@ -31,10 +31,25 @@ void test_sockaddr_port_returns_explicitly_assigned_port() {
close(sock);
}
void test_peek_and_poke_buffer() {
void *buf = idrnet_malloc(100);
assert(buf > 0);
for (int i = 0; i < 100; i++) {
idrnet_poke(buf,i,7*i);
}
for(int i = 0; i < 100; i++) {
assert (idrnet_peek(buf,i) == (0xff & 7*i));
}
idrnet_free(buf);
}
int main(int argc, char**argv) {
test_sockaddr_port_returns_explicitly_assigned_port();
test_sockaddr_port_returns_random_port_when_bind_port_is_0();
test_peek_and_poke_buffer();
printf("network library tests SUCCESS\n");
return 0;

1
libs/prelude/Prelude.idr
View File

@ -364,6 +364,7 @@ Integral Integer where
-- all other possibilities fail. I don't plan to provide a nicer syntax for
-- this...
%defaulthint
%inline
public export
defaultInteger : Num Integer
defaultInteger = %search

63
src/Compiler/Common.idr
View File

@ -2,6 +2,7 @@ module Compiler.Common
import Compiler.CompileExpr
import Compiler.Inline
import Compiler.LambdaLift
import Core.Context
import Core.Directory
@ -101,12 +102,10 @@ fastAppend xs
build b (x :: xs) = do addToStringBuffer b x
build b xs
dumpCases : {auto c : Ref Ctxt Defs} ->
String -> List Name ->
dumpCases : Defs -> String -> List Name ->
Core ()
dumpCases fn cns
= do defs <- get Ctxt
cstrs <- traverse (dumpCase defs) cns
dumpCases defs fn cns
= do cstrs <- traverse dumpCase cns
Right () <- coreLift $ writeFile fn (fastAppend cstrs)
| Left err => throw (FileErr fn err)
pure ()
@ -115,8 +114,8 @@ dumpCases fn cns
fullShow (DN _ n) = show n
fullShow n = show n
dumpCase : Defs -> Name -> Core String
dumpCase defs n
dumpCase : Name -> Core String
dumpCase n
= case !(lookupCtxtExact n (gamma defs)) of
Nothing => pure ""
Just d =>
@ -124,12 +123,38 @@ dumpCases fn cns
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} ->
Term vars -> Core (List Name, NameTags)
findUsedNames tm
getCompileData : {auto c : Ref Ctxt Defs} ->
ClosedTerm -> Core CompileData
getCompileData tm
= do defs <- get Ctxt
sopts <- getSession
let ns = getRefs (Resolved (-1)) tm
@ -154,12 +179,24 @@ findUsedNames 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

122
src/Compiler/CompileExpr.idr
View File

@ -23,6 +23,7 @@ NameTags = NameMap Int
data Args
= NewTypeBy Nat Nat
| EraseArgs Nat (List Nat)
| Arity Nat
||| Extract the number of arguments from a term, or return that it's
@ -30,13 +31,15 @@ data Args
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
Just (DCon _ arity Nothing) => pure (Arity arity)
Just (DCon _ arity (Just pos)) => pure (NewTypeBy arity pos)
Just (PMDef _ args _ _ _) => pure (Arity (length args))
Just (ExternDef arity) => pure (Arity arity)
Just (ForeignDef arity _) => pure (Arity arity)
Just (Builtin {arity} f) => pure (Arity arity)
= do Just gdef <- lookupCtxtExact n (gamma defs)
| Nothing => pure (Arity 0)
case definition gdef of
DCon _ arity Nothing => pure (EraseArgs arity (eraseArgs gdef))
DCon _ arity (Just (_, pos)) => pure (NewTypeBy arity pos)
PMDef _ args _ _ _ => pure (Arity (length args))
ExternDef arity => pure (Arity arity)
ForeignDef arity _ => pure (Arity arity)
Builtin {arity} f => pure (Arity arity)
_ => pure (Arity 0)
numArgs _ tm = pure (Arity 0)
@ -60,6 +63,7 @@ etaExpand i (S k) exp args
(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
@ -96,6 +100,34 @@ applyNewType arity pos fn args
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
@ -130,7 +162,7 @@ natBranch (MkConAlt n _ _ _) = isNatCon n
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
@ -184,7 +216,7 @@ mutual
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)]
@ -219,6 +251,9 @@ mutual
| 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
@ -227,22 +262,35 @@ mutual
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 (DCon _ arity (Just pos)) => conCases tags n ns -- skip it
_ => do let tag' = case lookup x tags of
Just gdef <- lookupCtxtExact x (gamma defs)
| Nothing => -- primitive type match
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} ->
NameTags -> Name -> List (CaseAlt vars) ->
Core (List (CConstAlt vars))
constCases tags n [] = pure []
constCases tags n (ConstCase WorldVal sc :: ns)
= constCases tags n ns
constCases tags n (ConstCase x sc :: ns)
= pure $ MkConstAlt x !(toCExpTree tags n sc) ::
!(constCases tags n ns)
@ -251,16 +299,25 @@ mutual
getDef : {auto c : Ref Ctxt Defs} ->
FC -> CExp vars ->
NameTags -> Name -> List (CaseAlt vars) ->
Core (Maybe (CExp vars))
getDef fc scr tags n [] = pure Nothing
Core (Bool, Maybe (CExp vars))
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 $ (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
@ -277,8 +334,8 @@ mutual
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 ty (CErased fc)
CLet fc arg True (CForce fc (CLocal (getLoc scTy) x)) $
CLet fc ty True (CErased fc)
!(toCExpTree tags n sc)
toCExpTree tags n alts = toCExpTree' tags n alts
@ -289,9 +346,13 @@ mutual
= 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 _ _ _ :: _))
@ -299,9 +360,13 @@ mutual
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
@ -452,7 +517,8 @@ toCDef tags n ty (Builtin {arity} op)
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
@ -472,10 +538,10 @@ toCDef tags n ty def
export
compileExp : {auto c : Ref Ctxt Defs} ->
NameTags -> ClosedTerm -> Core NamedCExp
NameTags -> ClosedTerm -> Core (CExp [])
compileExp tags tm
= do exp <- toCExp tags (UN "main") tm
pure (forget exp)
pure exp
||| Given a name, look up an expression, and compile it to a CExp in the environment
export

218
src/Compiler/Inline.idr
View File

@ -1,5 +1,7 @@
module Compiler.Inline
import Compiler.CompileExpr
import Core.CompileExpr
import Core.Context
import Core.FC
@ -53,73 +55,6 @@ genName n
put LVar (i + 1)
pure (MN n i)
resolveRef : (done : List Name) -> Bounds bound -> FC -> Name ->
Maybe (CExp (later ++ (done ++ bound ++ vars)))
resolveRef done None fc n = Nothing
resolveRef {later} {vars} done (Add {xs} new old bs) fc n
= if n == old
then rewrite appendAssociative later done (new :: xs ++ vars) in
let MkNVar p = weakenNVar {inner = new :: xs ++ vars}
(later ++ done) First in
Just (CLocal fc p)
else rewrite appendAssociative done [new] (xs ++ vars)
in resolveRef (done ++ [new]) bs fc n
mutual
mkLocals : {later, vars : _} ->
Bounds bound ->
CExp (later ++ vars) -> CExp (later ++ (bound ++ vars))
mkLocals bs (CLocal {idx} {x} fc p)
= let MkNVar p' = addVars bs p in CLocal {x} fc p'
mkLocals {later} {vars} bs (CRef fc var)
= maybe (CRef fc var) id (resolveRef [] bs fc var)
mkLocals {later} {vars} bs (CLam fc x sc)
= let sc' = mkLocals bs {later = x :: later} {vars} sc in
CLam fc x sc'
mkLocals {later} {vars} bs (CLet fc x val sc)
= let sc' = mkLocals bs {later = x :: later} {vars} sc in
CLet fc x (mkLocals bs val) sc'
mkLocals bs (CApp fc f xs)
= CApp fc (mkLocals bs f) (assert_total (map (mkLocals bs) xs))
mkLocals bs (CCon fc x tag xs)
= CCon fc x tag (assert_total (map (mkLocals bs) xs))
mkLocals bs (COp fc x xs)
= COp fc x (assert_total (map (mkLocals bs) xs))
mkLocals bs (CExtPrim fc x xs)
= CExtPrim fc x (assert_total (map (mkLocals bs) xs))
mkLocals bs (CForce fc x)
= CForce fc (mkLocals bs x)
mkLocals bs (CDelay fc x)
= CDelay fc (mkLocals bs x)
mkLocals bs (CConCase fc sc xs def)
= CConCase fc (mkLocals bs sc)
(assert_total (map (mkLocalsConAlt bs) xs))
(assert_total (map (mkLocals bs) def))
mkLocals bs (CConstCase fc sc xs def)
= CConstCase fc (mkLocals bs sc)
(assert_total (map (mkLocalsConstAlt bs) xs))
(assert_total (map (mkLocals bs) def))
mkLocals bs (CPrimVal fc x) = CPrimVal fc x
mkLocals bs (CErased fc) = CErased fc
mkLocals bs (CCrash fc x) = CCrash fc x
mkLocalsConAlt : Bounds bound ->
CConAlt (later ++ vars) -> CConAlt (later ++ (bound ++ vars))
mkLocalsConAlt {bound} {later} {vars} bs (MkConAlt x tag args sc)
= let sc' : CExp ((args ++ later) ++ vars)
= rewrite sym (appendAssociative args later vars) in sc in
MkConAlt x tag args
(rewrite appendAssociative args later (bound ++ vars) in
mkLocals bs sc')
mkLocalsConstAlt : Bounds bound ->
CConstAlt (later ++ vars) -> CConstAlt (later ++ (bound ++ vars))
mkLocalsConstAlt bs (MkConstAlt x sc) = MkConstAlt x (mkLocals bs sc)
refsToLocals : Bounds bound -> CExp vars -> CExp (bound ++ vars)
refsToLocals None tm = tm
refsToLocals bs y = mkLocals {later = []} bs y
refToLocal : Name -> (x : Name) -> CExp vars -> CExp (x :: vars)
refToLocal x new tm = refsToLocals (Add new x None) tm
@ -127,7 +62,7 @@ mutual
used : Name -> CExp free -> Bool
used n (CRef _ n') = n == n'
used n (CLam _ _ sc) = used n sc
used n (CLet _ _ val sc) = used n val || used n sc
used n (CLet _ _ _ val sc) = used n val || used n sc
used n (CApp _ x args) = used n x || or (map Delay (map (used n) args))
used n (CCon _ _ _ args) = or (map Delay (map (used n) args))
used n (COp _ _ args) = or (map Delay (map (used n) args))
@ -198,12 +133,12 @@ mutual
sc' <- eval rec (CRef fc xn :: env) [] sc
pure $ CLam fc x (refToLocal xn x sc')
eval rec env (e :: stk) (CLam fc x sc) = eval rec (e :: env) stk sc
eval {vars} {free} rec env stk (CLet fc x val sc)
eval {vars} {free} rec env stk (CLet fc x inl val sc)
= do xn <- genName "letv"
sc' <- eval rec (CRef fc xn :: env) [] sc
if used xn sc'
if inl && used xn sc'
then do val' <- eval rec env [] val
pure (unload stk $ CLet fc x val' (refToLocal xn x sc'))
pure (unload stk $ CLet fc x inl val' (refToLocal xn x sc'))
else pure sc'
eval rec env stk (CApp fc f args)
= eval rec env (!(traverse (eval rec env []) args) ++ stk) f
@ -298,12 +233,124 @@ mutual
else pickConstAlt rec env stk (CPrimVal fc c) alts def
pickConstAlt rec env stk _ _ _ = pure Nothing
inline : {auto c : Ref Ctxt Defs} ->
CDef -> Core CDef
inline (MkFun args exp)
-- Inlining may have messed with function arity (e.g. by adding lambdas to
-- the LHS to avoid needlessly making a closure) so fix them up here. This
-- needs to be right because typically back ends need to know whether a
-- name is under- or over-applied
fixArityTm : {auto c : Ref Ctxt Defs} ->
CExp vars -> List (CExp vars) -> Core (CExp vars)
fixArityTm (CRef fc n) args
= do defs <- get Ctxt
Just gdef <- lookupCtxtExact n (gamma defs)
| Nothing => pure (unload args (CRef fc n))
let Just def = compexpr gdef
| Nothing => pure (unload args (CRef fc n))
let arity = getArity def
pure $ expandToArity arity (CApp fc (CRef fc n) []) args
fixArityTm (CLam fc x sc) args
= pure $ expandToArity Z (CLam fc x !(fixArityTm sc [])) args
fixArityTm (CLet fc x inl val sc) args
= pure $ expandToArity Z
(CLet fc x inl !(fixArityTm val []) !(fixArityTm sc [])) args
fixArityTm (CApp fc f fargs) args
= fixArityTm f (!(traverse (\tm => fixArityTm tm []) fargs) ++ args)
fixArityTm (CCon fc n t args) []
= pure $ CCon fc n t !(traverse (\tm => fixArityTm tm []) args)
fixArityTm (COp fc op args) []
= pure $ COp fc op !(traverseArgs args)
where
traverseArgs : Vect n (CExp vs) -> Core (Vect n (CExp vs))
traverseArgs [] = pure []
traverseArgs (a :: as) = pure $ !(fixArityTm a []) :: !(traverseArgs as)
fixArityTm (CExtPrim fc p args) []
= pure $ CExtPrim fc p !(traverse (\tm => fixArityTm tm []) args)
fixArityTm (CForce fc tm) args
= pure $ expandToArity Z (CForce fc !(fixArityTm tm [])) args
fixArityTm (CDelay fc tm) args
= pure $ expandToArity Z (CDelay fc !(fixArityTm tm [])) args
fixArityTm (CConCase fc sc alts def) args
= pure $ expandToArity Z
(CConCase fc !(fixArityTm sc [])
!(traverse fixArityAlt alts)
!(traverseOpt (\tm => fixArityTm tm []) def)) args
where
fixArityAlt : CConAlt vars -> Core (CConAlt vars)
fixArityAlt (MkConAlt n t a sc)
= pure $ MkConAlt n t a !(fixArityTm sc [])
fixArityTm (CConstCase fc sc alts def) args
= pure $ expandToArity Z
(CConstCase fc !(fixArityTm sc [])
!(traverse fixArityConstAlt alts)
!(traverseOpt (\tm => fixArityTm tm []) def)) args
where
fixArityConstAlt : CConstAlt vars -> Core (CConstAlt vars)
fixArityConstAlt (MkConstAlt c sc)
= pure $ MkConstAlt c !(fixArityTm sc [])
fixArityTm t [] = pure t
fixArityTm t args = pure $ expandToArity Z t args
export
fixArityExp : {auto c : Ref Ctxt Defs} ->
CExp vars -> Core (CExp vars)
fixArityExp tm = fixArityTm tm []
fixArity : {auto c : Ref Ctxt Defs} ->
CDef -> Core CDef
fixArity (MkFun args exp) = pure $ MkFun args !(fixArityTm exp [])
fixArity (MkError exp) = pure $ MkError !(fixArityTm exp [])
fixArity d = pure d
getLams : Int -> SubstCEnv done args -> CExp (done ++ args) ->
(args' ** (SubstCEnv args' args, CExp (args' ++ args)))
getLams {done} i env (CLam fc x sc)
= getLams {done = x :: done} (i + 1) (CRef fc (MN "ext" i) :: env) sc
getLams {done} i env sc = (done ** (env, sc))
mkBounds : (xs : _) -> Bounds xs
mkBounds [] = None
mkBounds (x :: xs) = Add x x (mkBounds xs)
getNewArgs : SubstCEnv done args -> List Name
getNewArgs [] = []
getNewArgs (CRef _ n :: xs) = n :: getNewArgs xs
getNewArgs {done = x :: xs} (_ :: sub) = x :: getNewArgs sub
-- Move any lambdas in the body of the definition into the lhs list of vars.
-- Annoyingly, the indices will need fixing up because the order in the top
-- level definition goes left to right (i.e. first argument has lowest index,
-- not the highest, as you'd expect if they were all lambdas).
mergeLambdas : (args : List Name) -> CExp args -> (args' ** CExp args')
mergeLambdas args (CLam fc x sc)
= let (args' ** (env, exp')) = getLams 0 [] (CLam fc x sc)
expNs = substs env exp'
newArgs = reverse $ getNewArgs env
expLocs = mkLocals {later = args} {vars=[]} (mkBounds newArgs)
(rewrite appendNilRightNeutral args in expNs) in
(_ ** expLocs)
mergeLambdas args exp = (args ** exp)
doEval : {auto c : Ref Ctxt Defs} ->
Name -> CExp args -> Core (CExp args)
doEval n exp
= do l <- newRef LVar (the Int 0)
MkFun args <$> eval [] [] [] exp
inline d = pure d
log 10 (show n ++ ": " ++ show exp)
exp' <- eval [] [] [] exp
log 10 ("Inlined: " ++ show exp')
pure exp'
inline : {auto c : Ref Ctxt Defs} ->
Name -> CDef -> Core CDef
inline n (MkFun args def)
= pure $ MkFun args !(doEval n def)
inline n d = pure d
-- merge lambdas from expression into top level arguments
mergeLam : {auto c : Ref Ctxt Defs} ->
CDef -> Core CDef
mergeLam (MkFun args def)
= do let (args' ** exp') = mergeLambdas args def
pure $ MkFun args' exp'
mergeLam d = pure d
export
inlineDef : {auto c : Ref Ctxt Defs} ->
@ -312,5 +359,22 @@ inlineDef n
= do defs <- get Ctxt
Just def <- lookupCtxtExact n (gamma defs) | Nothing => pure ()
let Just cexpr = compexpr def | Nothing => pure ()
setCompiled n !(inline cexpr)
setCompiled n !(inline n cexpr)
export
fixArityDef : {auto c : Ref Ctxt Defs} ->
Name -> Core ()
fixArityDef n
= do defs <- get Ctxt
Just def <- lookupCtxtExact n (gamma defs) | Nothing => pure ()
let Just cexpr = compexpr def | Nothing => pure ()
setCompiled n !(fixArity cexpr)
export
mergeLamDef : {auto c : Ref Ctxt Defs} ->
Name -> Core ()
mergeLamDef n
= do defs <- get Ctxt
Just def <- lookupCtxtExact n (gamma defs) | Nothing => pure ()
let Just cexpr = compexpr def | Nothing => pure ()
setCompiled n !(mergeLam cexpr)

237
src/Compiler/LambdaLift.idr Normal file
View File

@ -0,0 +1,237 @@
module Compuler.LambdaLift
import Core.CompileExpr
import Core.Context
import Core.Core
import Core.TT
import Data.Vect
%default covering
mutual
public export
data Lifted : List Name -> Type where
LLocal : {idx : Nat} -> FC -> .(IsVar x idx vars) -> Lifted vars
-- A known function applied to exactly the right number of arguments,
-- so the runtime can Just Go
LAppName : FC -> Name -> List (Lifted vars) -> Lifted vars
-- A known function applied to too few arguments, so the runtime should
-- make a closure and wait for the remaining arguments
LUnderApp : FC -> Name -> (missing : Nat) ->
(args : List (Lifted vars)) -> Lifted vars
-- A closure applied to one more argument (so, for example a closure
-- which is waiting for another argument before it can run).
-- The runtime should add the argument to the closure and run the result
-- if it is now fully applied.
LApp : FC -> (closure : Lifted vars) -> (arg : Lifted vars) -> Lifted vars
LLet : FC -> (x : Name) -> Lifted vars ->
Lifted (x :: var) -> Lifted vars
LCon : FC -> Name -> (tag : Int) -> List (Lifted vars) -> Lifted vars
LOp : FC -> PrimFn arity -> Vect arity (Lifted vars) -> Lifted vars
LExtPrim : FC -> (p : Name) -> List (Lifted vars) -> Lifted vars
LConCase : FC -> Lifted vars ->
List (LiftedConAlt vars) ->
Maybe (Lifted vars) -> Lifted vars
LConstCase : FC -> Lifted vars ->
List (LiftedConstAlt vars) ->
Maybe (Lifted vars) -> Lifted vars
LPrimVal : FC -> Constant -> Lifted vars
LErased : FC -> Lifted vars
LCrash : FC -> String -> Lifted vars
public export
data LiftedConAlt : List Name -> Type where
MkLConAlt : Name -> (tag : Int) -> (args : List Name) ->
Lifted (args ++ vars) -> LiftedConAlt vars
public export
data LiftedConstAlt : List Name -> Type where
MkLConstAlt : Constant -> Lifted vars -> LiftedConstAlt vars
public export
data LiftedDef : Type where
-- We take the outer scope and the function arguments separately so that
-- we don't have to reshuffle de Bruijn indices, which is expensive.
-- This should be compiled as a function which takes 'args' first,
-- then 'scope'.
MkLFun : (args : List Name) -> -- function arguments
(scope : List Name) -> -- outer scope
Lifted (scope ++ args) -> LiftedDef
MkLCon : (tag : Int) -> (arity : Nat) -> (nt : Maybe Nat) -> LiftedDef
MkLForeign : (ccs : List String) ->
(fargs : List CFType) ->
CFType ->
LiftedDef
MkLError : Lifted [] -> LiftedDef
mutual
export
Show (Lifted vs) where
show (LLocal {x} _ _) = "!" ++ show x
show (LAppName fc n args)
= show n ++ "(" ++ showSep ", " (map show args) ++ ")"
show (LUnderApp fc n m args)
= "<" ++ show n ++ " underapp " ++ show m ++ ">(" ++
showSep ", " (map show args) ++ ")"
show (LApp fc c arg)
= show c ++ " @ (" ++ show arg ++ ")"
show (LLet fc x val sc)
= "%let " ++ show x ++ " = " ++ show val ++ " in " ++ show sc
show (LCon fc n t args)
= "%con " ++ show n ++ "(" ++ showSep ", " (map show args) ++ ")"
show (LOp fc op args)
= "%op " ++ show op ++ "(" ++ showSep ", " (toList (map show args)) ++ ")"
show (LExtPrim fc p args)
= "%extprim " ++ show p ++ "(" ++ showSep ", " (map show args) ++ ")"
show (LConCase fc sc alts def)
= "%case " ++ show sc ++ " of { "
++ showSep "| " (map show alts) ++ " " ++ show def
show (LConstCase fc sc alts def)
= "%case " ++ show sc ++ " of { "
++ showSep "| " (map show alts) ++ " " ++ show def
show (LPrimVal _ x) = show x
show (LErased _) = "___"
show (LCrash _ x) = "%CRASH(" ++ show x ++ ")"
export
Show (LiftedConAlt vs) where
show (MkLConAlt n t args sc)
= "%conalt " ++ show n ++
"(" ++ showSep ", " (map show args) ++ ") => " ++ show sc
export
Show (LiftedConstAlt vs) where
show (MkLConstAlt c sc)
= "%constalt(" ++ show c ++ ") => " ++ show sc
export
Show LiftedDef where
show (MkLFun args scope exp) = show args ++ show scope ++ ": " ++ show exp
show (MkLCon tag arity pos)
= "Constructor tag " ++ show tag ++ " arity " ++ show arity ++
maybe "" (\n => " (newtype by " ++ show n ++ ")") pos
show (MkLForeign ccs args ret)
= "Foreign call " ++ show ccs ++ " " ++
show args ++ " -> " ++ show ret
show (MkLError exp) = "Error: " ++ show exp
data Lifts : Type where
record LDefs where
constructor MkLDefs
basename : Name -- top level name we're lifting from
defs : List (Name, LiftedDef) -- new definitions we made
nextName : Int -- name of next definition to lift
genName : {auto l : Ref Lifts LDefs} ->
Core Name
genName
= do ldefs <- get Lifts
let i = nextName ldefs
put Lifts (record { nextName = i + 1 } ldefs)
pure $ mkName (basename ldefs) i
where
mkName : Name -> Int -> Name
mkName (NS ns b) i = NS ns (mkName b i)
mkName (UN n) i = MN n i
mkName n i = MN (show n) i
unload : FC -> Lifted vars -> List (Lifted vars) -> Core (Lifted vars)
unload fc f [] = pure f
unload fc f (a :: as) = unload fc (LApp fc f a) as
mutual
makeLam : {auto l : Ref Lifts LDefs} ->
{vars : _} ->
FC -> (bound : List Name) ->
CExp (bound ++ vars) -> Core (Lifted vars)
makeLam fc bound (CLam _ x sc') = makeLam fc (x :: bound) sc'
makeLam {vars} fc bound sc
= do scl <- liftExp sc
n <- genName
ldefs <- get Lifts
put Lifts (record { defs $= ((n, MkLFun vars bound scl) ::) } ldefs)
-- TODO: an optimisation here would be to spot which variables
-- aren't used in the new definition, and not abstract over them
-- in the new definition. Given that we have to do some messing
-- about with indices anyway, it's probably not costly to do.
pure $ LUnderApp fc n (length bound) (allVars vars)
where
allPrfs : (vs : List Name) -> List (Var vs)
allPrfs [] = []
allPrfs (v :: vs) = MkVar First :: map weaken (allPrfs vs)
-- apply to all the variables. 'First' will be first in the last, which
-- is good, because the most recently bound name is the first argument to
-- the resulting function
allVars : (vs : List Name) -> List (Lifted vs)
allVars vs = map (\ (MkVar p) => LLocal fc p) (allPrfs vs)
liftExp : {auto l : Ref Lifts LDefs} ->
CExp vars -> Core (Lifted vars)
liftExp (CLocal fc prf) = pure $ LLocal fc prf
liftExp (CRef fc n) = pure $ LAppName fc n [] -- probably shouldn't happen!
liftExp (CLam fc x sc) = makeLam fc [x] sc
liftExp (CLet fc x _ val sc) = pure $ LLet fc x !(liftExp val) !(liftExp sc)
liftExp (CApp fc (CRef _ n) args) -- names are applied exactly in compileExp
= pure $ LAppName fc n !(traverse liftExp args)
liftExp (CApp fc f args)
= unload fc !(liftExp f) !(traverse liftExp args)
liftExp (CCon fc n t args) = pure $ LCon fc n t !(traverse liftExp args)
liftExp (COp fc op args)
= pure $ LOp fc op !(traverseArgs args)
where
traverseArgs : Vect n (CExp vars) -> Core (Vect n (Lifted vars))
traverseArgs [] = pure []
traverseArgs (a :: as) = pure $ !(liftExp a) :: !(traverseArgs as)
liftExp (CExtPrim fc p args) = pure $ LExtPrim fc p !(traverse liftExp args)
liftExp (CForce fc tm) = liftExp (CApp fc tm [CErased fc])
liftExp (CDelay fc tm) = liftExp (CLam fc (MN "x" 0) (weaken tm))
liftExp (CConCase fc sc alts def)
= pure $ LConCase fc !(liftExp sc) !(traverse liftConAlt alts)
!(traverseOpt liftExp def)
where
liftConAlt : CConAlt vars -> Core (LiftedConAlt vars)
liftConAlt (MkConAlt n t args sc) = pure $ MkLConAlt n t args !(liftExp sc)
liftExp (CConstCase fc sc alts def)
= pure $ LConstCase fc !(liftExp sc) !(traverse liftConstAlt alts)
!(traverseOpt liftExp def)
where
liftConstAlt : CConstAlt vars -> Core (LiftedConstAlt vars)
liftConstAlt (MkConstAlt c sc) = pure $ MkLConstAlt c !(liftExp sc)
liftExp (CPrimVal fc c) = pure $ LPrimVal fc c
liftExp (CErased fc) = pure $ LErased fc
liftExp (CCrash fc str) = pure $ LCrash fc str
liftBody : Name -> CExp vars -> Core (Lifted vars, List (Name, LiftedDef))
liftBody n tm
= do l <- newRef Lifts (MkLDefs n [] 0)
tml <- liftExp {l} tm
ldata <- get Lifts
pure (tml, defs ldata)
lambdaLiftDef : Name -> CDef -> Core (List (Name, LiftedDef))
lambdaLiftDef n (MkFun args exp)
= do (expl, defs) <- liftBody n exp
pure ((n, MkLFun args [] expl) :: defs)
lambdaLiftDef n (MkCon t a nt) = pure [(n, MkLCon t a nt)]
lambdaLiftDef n (MkForeign ccs fargs ty) = pure [(n, MkLForeign ccs fargs ty)]
lambdaLiftDef n (MkError exp)
= do (expl, defs) <- liftBody n exp
pure ((n, MkLError expl) :: defs)
-- Return the lambda lifted definitions required for the given name.
-- If the name hasn't been compiled yet (via CompileExpr.compileDef) then
-- this will return an empty list
-- An empty list an error, because on success you will always get at least
-- one definition, the lifted definition for the given name.
export
lambdaLift : {auto c : Ref Ctxt Defs} ->
Name -> Core (List (Name, LiftedDef))
lambdaLift n
= do defs <- get Ctxt
Just def <- lookupCtxtExact n (gamma defs) | Nothing => pure []
let Just cexpr = compexpr def | Nothing => pure []
lambdaLiftDef n cexpr

14
src/Compiler/Scheme/Chez.idr
View File

@ -203,15 +203,13 @@ cCall fc cfn clib args ret
applyLams n (Just a :: as) = applyLams ("(" ++ n ++ " " ++ a ++ ")") as
getVal : String -> String
getVal str = "(vector-ref " ++ str ++ "2)"
getVal str = "(vector-ref " ++ str ++ "1)"
mkFun : List CFType -> CFType -> String -> String
mkFun args ret n
= let argns = mkNs 0 args in
"(lambda (" ++ showSep " " (mapMaybe id argns) ++ ") " ++
(case ret of
CFIORes _ => getVal (applyLams n argns) ++ ")"
_ => applyLams n argns ++ ")")
(applyLams n argns ++ ")")
notWorld : CFType -> Bool
notWorld CFWorld = False
@ -330,14 +328,18 @@ compileToSS c tm outfile
= 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) ++

7
src/Compiler/Scheme/Common.idr
View File

@ -85,6 +85,7 @@ schOp (Div IntType) [x, y] = op "b/" [x, y, "63"]
schOp (Add ty) [x, y] = op "+" [x, y]
schOp (Sub ty) [x, y] = op "-" [x, y]
schOp (Mul ty) [x, y] = op "*" [x, y]
schOp (Div IntegerType) [x, y] = op "quotient" [x, y]
schOp (Div ty) [x, y] = op "/" [x, y]
schOp (Mod ty) [x, y] = op "remainder" [x, y]
schOp (Neg ty) [x] = op "-" [x]
@ -136,12 +137,12 @@ schOp (Cast DoubleType StringType) [x] = op "number->string" [x]
schOp (Cast CharType StringType) [x] = op "string" [x]
schOp (Cast IntType IntegerType) [x] = x
schOp (Cast DoubleType IntegerType) [x] = op "floor" [x]
schOp (Cast DoubleType IntegerType) [x] = op "exact-floor" [x]
schOp (Cast CharType IntegerType) [x] = op "char->integer" [x]
schOp (Cast StringType IntegerType) [x] = op "cast-string-int" [x]
schOp (Cast IntegerType IntType) [x] = x
schOp (Cast DoubleType IntType) [x] = op "floor" [x]
schOp (Cast DoubleType IntType) [x] = op "exact-floor" [x]
schOp (Cast StringType IntType) [x] = op "cast-string-int" [x]
schOp (Cast CharType IntType) [x] = op "char->integer" [x]
@ -234,7 +235,7 @@ toPrim pn = Unknown pn
export
mkWorld : String -> String
mkWorld res = schConstructor 0 ["#f", res, "#f"] -- MkIORes
mkWorld res = res -- MkIORes is a newtype now! schConstructor 0 [res, "#f"] -- MkIORes
schConstant : (String -> String) -> Constant -> String
schConstant _ (I x) = show x

16
src/Compiler/Scheme/Racket.idr
View File

@ -180,15 +180,11 @@ cCall fc cfn libspec args ret
applyLams n (Just (a, ty) :: as)
= applyLams ("(" ++ n ++ " " ++ cToRkt ty a ++ ")") as
getVal : CFType -> String -> String
getVal ty str = rktToC ty ("(vector-ref " ++ str ++ "2)")
mkFun : List CFType -> CFType -> String -> String
mkFun args ret n
= let argns = mkNs 0 args in
(case ret of
CFIORes rt => getVal rt (applyLams n argns) ++ ")"
_ => applyLams n argns ++ ")")
"(lambda (" ++ showSep " " (map fst (mapMaybe id argns)) ++ ") " ++
(applyLams n argns ++ ")")
notWorld : CFType -> Bool
notWorld CFWorld = False
@ -291,14 +287,18 @@ getFgnCall n
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 ++

2
src/Core/Binary.idr
View File

@ -27,7 +27,7 @@ import Data.Buffer
-- TTC files can only be compatible if the version number is the same
export
ttcVersion : Int
ttcVersion = 21
ttcVersion = 22
export
checkTTCVersion : String -> Int -> Int -> Core ()

16
src/Core/CaseTree.idr
View File

@ -6,24 +6,36 @@ import Data.NameMap
%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
@ -65,7 +77,9 @@ mutual
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

94
src/Core/CompileExpr.idr
View File

@ -19,7 +19,8 @@ mutual
-- Lambda expression
CLam : FC -> (x : Name) -> CExp (x :: vars) -> CExp vars
-- Let bindings
CLet : FC -> (x : Name) -> CExp vars -> CExp (x :: vars) -> CExp vars
CLet : FC -> (x : Name) -> (inlineOK : Bool) -> -- Don't inline if set
CExp vars -> CExp (x :: vars) -> CExp vars
-- Application of a defined function. The length of the argument list is
-- exactly the same length as expected by its definition (so saturate with
-- lambdas if necessary, or overapply with additional CApps)
@ -224,7 +225,7 @@ mutual
forgetExp locs (CLam fc x sc)
= let locs' = addLocs [x] locs in
NmLam fc (getLocName _ locs' First) (forgetExp locs' sc)
forgetExp locs (CLet fc x val sc)
forgetExp locs (CLet fc x _ val sc)
= let locs' = addLocs [x] locs in
NmLet fc (getLocName _ locs' First)
(forgetExp locs val)
@ -326,9 +327,9 @@ mutual
thin {outer} {inner} n (CLam fc x sc)
= let sc' = thin {outer = x :: outer} {inner} n sc in
CLam fc x sc'
thin {outer} {inner} n (CLet fc x val sc)
thin {outer} {inner} n (CLet fc x inl val sc)
= let sc' = thin {outer = x :: outer} {inner} n sc in
CLet fc x (thin n val) sc'
CLet fc x inl (thin n val) sc'
thin n (CApp fc x xs)
= CApp fc (thin n x) (assert_total (map (thin n) xs))
thin n (CCon fc x tag xs)
@ -372,9 +373,9 @@ mutual
insertNames {outer} {inner} ns (CLam fc x sc)
= let sc' = insertNames {outer = x :: outer} {inner} ns sc in
CLam fc x sc'
insertNames {outer} {inner} ns (CLet fc x val sc)
insertNames {outer} {inner} ns (CLet fc x inl val sc)
= let sc' = insertNames {outer = x :: outer} {inner} ns sc in
CLet fc x (insertNames ns val) sc'
CLet fc x inl (insertNames ns val) sc'
insertNames ns (CApp fc x xs)
= CApp fc (insertNames ns x) (assert_total (map (insertNames ns) xs))
insertNames ns (CCon fc x tag xs)
@ -416,7 +417,7 @@ mutual
embed (CLocal fc prf) = CLocal fc (varExtend prf)
embed (CRef fc n) = CRef fc n
embed (CLam fc x sc) = CLam fc x (embed sc)
embed (CLet fc x val sc) = CLet fc x (embed val) (embed sc)
embed (CLet fc x inl val sc) = CLet fc x inl (embed val) (embed sc)
embed (CApp fc f args) = CApp fc (embed f) (assert_total (map embed args))
embed (CCon fc n t args) = CCon fc n t (assert_total (map embed args))
embed (COp fc p args) = COp fc p (assert_total (map embed args))
@ -454,9 +455,9 @@ mutual
shrinkCExp sub (CLam fc x sc)
= let sc' = shrinkCExp (KeepCons sub) sc in
CLam fc x sc'
shrinkCExp sub (CLet fc x val sc)
shrinkCExp sub (CLet fc x inl val sc)
= let sc' = shrinkCExp (KeepCons sub) sc in
CLet fc x (shrinkCExp sub val) sc'
CLet fc x inl (shrinkCExp sub val) sc'
shrinkCExp sub (CApp fc x xs)
= CApp fc (shrinkCExp sub x) (assert_total (map (shrinkCExp sub) xs))
shrinkCExp sub (CCon fc x tag xs)
@ -525,9 +526,9 @@ mutual
substEnv {outer} env (CLam fc x sc)
= let sc' = substEnv {outer = x :: outer} env sc in
CLam fc x sc'
substEnv {outer} env (CLet fc x val sc)
substEnv {outer} env (CLet fc x inl val sc)
= let sc' = substEnv {outer = x :: outer} env sc in
CLet fc x (substEnv env val) sc'
CLet fc x inl (substEnv env val) sc'
substEnv env (CApp fc x xs)
= CApp fc (substEnv env x) (assert_total (map (substEnv env) xs))
substEnv env (CCon fc x tag xs)
@ -567,12 +568,81 @@ export
substs : SubstCEnv drop vars -> CExp (drop ++ vars) -> CExp vars
substs env tm = substEnv {outer = []} env tm
resolveRef : (done : List Name) -> Bounds bound -> FC -> Name ->
Maybe (CExp (later ++ (done ++ bound ++ vars)))
resolveRef done None fc n = Nothing
resolveRef {later} {vars} done (Add {xs} new old bs) fc n
= if n == old
then rewrite appendAssociative later done (new :: xs ++ vars) in
let MkNVar p = weakenNVar {inner = new :: xs ++ vars}
(later ++ done) First in
Just (CLocal fc p)
else rewrite appendAssociative done [new] (xs ++ vars)
in resolveRef (done ++ [new]) bs fc n
mutual
export
mkLocals : {later, vars : _} ->
Bounds bound ->
CExp (later ++ vars) -> CExp (later ++ (bound ++ vars))
mkLocals bs (CLocal {idx} {x} fc p)
= let MkNVar p' = addVars bs p in CLocal {x} fc p'
mkLocals {later} {vars} bs (CRef fc var)
= maybe (CRef fc var) id (resolveRef [] bs fc var)
mkLocals {later} {vars} bs (CLam fc x sc)
= let sc' = mkLocals bs {later = x :: later} {vars} sc in
CLam fc x sc'
mkLocals {later} {vars} bs (CLet fc x inl val sc)
= let sc' = mkLocals bs {later = x :: later} {vars} sc in
CLet fc x inl (mkLocals bs val) sc'
mkLocals bs (CApp fc f xs)
= CApp fc (mkLocals bs f) (assert_total (map (mkLocals bs) xs))
mkLocals bs (CCon fc x tag xs)
= CCon fc x tag (assert_total (map (mkLocals bs) xs))
mkLocals bs (COp fc x xs)
= COp fc x (assert_total (map (mkLocals bs) xs))
mkLocals bs (CExtPrim fc x xs)
= CExtPrim fc x (assert_total (map (mkLocals bs) xs))
mkLocals bs (CForce fc x)
= CForce fc (mkLocals bs x)
mkLocals bs (CDelay fc x)
= CDelay fc (mkLocals bs x)
mkLocals bs (CConCase fc sc xs def)
= CConCase fc (mkLocals bs sc)
(assert_total (map (mkLocalsConAlt bs) xs))
(assert_total (map (mkLocals bs) def))
mkLocals bs (CConstCase fc sc xs def)
= CConstCase fc (mkLocals bs sc)
(assert_total (map (mkLocalsConstAlt bs) xs))
(assert_total (map (mkLocals bs) def))
mkLocals bs (CPrimVal fc x) = CPrimVal fc x
mkLocals bs (CErased fc) = CErased fc
mkLocals bs (CCrash fc x) = CCrash fc x
mkLocalsConAlt : Bounds bound ->
CConAlt (later ++ vars) -> CConAlt (later ++ (bound ++ vars))
mkLocalsConAlt {bound} {later} {vars} bs (MkConAlt x tag args sc)
= let sc' : CExp ((args ++ later) ++ vars)
= rewrite sym (appendAssociative args later vars) in sc in
MkConAlt x tag args
(rewrite appendAssociative args later (bound ++ vars) in
mkLocals bs sc')
mkLocalsConstAlt : Bounds bound ->
CConstAlt (later ++ vars) -> CConstAlt (later ++ (bound ++ vars))
mkLocalsConstAlt bs (MkConstAlt x sc) = MkConstAlt x (mkLocals bs sc)
export
refsToLocals : Bounds bound -> CExp vars -> CExp (bound ++ vars)
refsToLocals None tm = tm
refsToLocals bs y = mkLocals {later = []} bs y
export
getFC : CExp args -> FC
getFC (CLocal fc _) = fc
getFC (CRef fc _) = fc
getFC (CLam fc _ _) = fc
getFC (CLet fc _ _ _) = fc
getFC (CLet fc _ _ _ _) = fc
getFC (CApp fc _ _) = fc
getFC (CCon fc _ _ _) = fc
getFC (COp fc _ _) = fc

10
src/Core/Context.idr
View File

@ -65,8 +65,14 @@ data Def : Type where
Def
Builtin : {arity : Nat} -> PrimFn arity -> Def
DCon : (tag : Int) -> (arity : Nat) ->
(newtypeArg : Maybe Nat) -> -- if only constructor, and only one
-- argument is non-Rig0, flag it here,
(newtypeArg : Maybe (Bool, Nat)) ->
-- 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

10
src/Core/Env.idr
View File

@ -75,15 +75,11 @@ getBinderUnder : Weaken tm =>
{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 revNs [v] ns in
map (weakenNs (reverse (v :: ns))) b
= rewrite revOnto vs (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
rewrite revNs [v] ns in
getBinderUnder (v :: ns) lp env
= getBinderUnder (v :: ns) lp env
export
getBinder : Weaken tm =>

139
src/Core/Normalise.idr
View File

@ -72,9 +72,9 @@ parameters (defs : Defs, topopts : EvalOpts)
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
@ -120,16 +120,14 @@ parameters (defs : Defs, topopts : EvalOpts)
eval env locs (Erased fc i) stk = pure $ NErased fc i
eval env locs (TType fc) stk = pure $ NType fc
evalLocClosure : {vars : _} ->
Env Term free ->
evalLocClosure : Env Term free ->
FC -> Maybe Bool ->
Stack free ->
Closure free ->
LocalEnv free vars ->
Core (NF free)
evalLocClosure env fc mrig stk (MkClosure opts locs' env' tm') locs
evalLocClosure env fc mrig stk (MkClosure opts locs' env' tm')
= evalWithOpts defs opts env' locs' tm' stk
evalLocClosure {free} {vars = xs} env fc mrig stk (MkNFClosure nf) locs
evalLocClosure {free} env fc mrig stk (MkNFClosure nf)
= applyToStack nf stk
where
applyToStack : NF free -> Stack free -> Core (NF free)
@ -137,11 +135,10 @@ parameters (defs : Defs, topopts : EvalOpts)
= 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 MkNVar p' = insertNVarNames {outer=[]} {ns = xs} idx p in
evalLocal env fc mrig _ p' (args ++ stk) locs
= evalLocal env fc mrig _ p (args ++ stk) []
applyToStack (NDCon fc n t a args) stk
= pure $ NDCon fc n t a (args ++ stk)
applyToStack (NTCon fc n t a args) stk
@ -155,49 +152,41 @@ parameters (defs : Defs, topopts : EvalOpts)
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) && isLet mrig idx env
= 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
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 (x :: locs)
= evalLocClosure env fc mrig 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 : _} ->
Env Term free -> LocalEnv free vars ->
evalMeta : Env Term free ->
FC -> Name -> Int -> List (Closure free) ->
Stack free -> Core (NF free)
evalMeta {vars} env locs fc nm i args stk
= evalRef env locs True fc Func (Resolved i) (args ++ stk)
evalMeta env fc nm i args stk
= evalRef env True fc Func (Resolved i) (args ++ stk)
(NApp fc (NMeta nm i args) stk)
evalRef : {vars : _} ->
Env Term free -> LocalEnv free vars ->
evalRef : Env Term free ->
(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 ||
@ -209,48 +198,42 @@ parameters (defs : Defs, topopts : EvalOpts)
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 ->
Maybe (LocalEnv free (args ++ vars))
getCaseBound [] [] loc = Just loc
getCaseBound [] (x :: xs) loc = Nothing -- mismatched arg length
getCaseBound (arg :: args) [] loc = Nothing -- mismatched arg length
getCaseBound (arg :: args) (n :: ns) loc
= do loc' <- getCaseBound args ns loc
pure (arg :: loc')
LocalEnv free more ->
Maybe (LocalEnv free (args ++ more))
getCaseBound [] [] loc = Just loc
getCaseBound [] (_ :: _) loc = Nothing -- mismatched arg length
getCaseBound (arg :: args) [] loc = Nothing -- mismatched arg length
getCaseBound (arg :: args) (n :: ns) loc = (arg ::) <$> getCaseBound args ns 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
= maybe def (\bound =>
let loc' : LocalEnv _ ((args ++ more) ++ vars)
= rewrite sym (appendAssociative args more vars) in
bound in
evalTree env loc' opts fc stk sc def)
evalConAlt env loc opts fc stk args args' sc def
= maybe def (\bound => evalTree env bound 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
@ -263,9 +246,9 @@ parameters (defs : Defs, topopts : EvalOpts)
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
@ -292,34 +275,27 @@ parameters (defs : Defs, topopts : EvalOpts)
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 : _} ->
Env Term free -> LocalEnv free (args ++ vars) ->
evalTree : Env Term free -> LocalEnv free args ->
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
= do let x' : IsVar _ _ ((args ++ vars) ++ free)
= rewrite sym (appendAssociative args vars free) in
varExtend x
xval <- evalLocal env fc Nothing idx x' [] loc
evalTree env loc opts fc stk (Case idx x _ alts) def
= do xval <- evalLocal env fc Nothing idx (varExtend x) [] loc
findAlt env loc opts fc stk xval alts def
evalTree {args} {vars} {free} env loc opts fc stk (STerm tm) def
= do let tm' : Term ((args ++ vars) ++ free)
= rewrite sym (appendAssociative args vars free) in
embed tm
case fuel opts of
Nothing => evalWithOpts defs opts env loc tm' stk
evalTree env loc opts fc stk (STerm tm) def
= do case fuel opts of
Nothing => evalWithOpts defs opts env loc (embed 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.
@ -338,13 +314,13 @@ parameters (defs : Defs, topopts : EvalOpts)
= rewrite sym (plusSuccRightSucc got k) in
takeStk k stk (arg :: acc)
extendFromStack : (args : List Name) ->
LocalEnv free vars -> Stack free ->
Maybe (LocalEnv free (args ++ vars), Stack free)
extendFromStack [] loc stk = Just (loc, stk)
extendFromStack (n :: ns) loc [] = Nothing
extendFromStack (n :: ns) loc (arg :: args)
= do (loc', stk') <- extendFromStack ns loc args
argsFromStack : (args : List Name) ->
Stack free ->
Maybe (LocalEnv free args, Stack free)
argsFromStack [] stk = Just ([], stk)
argsFromStack (n :: ns) [] = Nothing
argsFromStack (n :: ns) (arg :: args)
= do (loc', stk') <- argsFromStack ns args
pure (arg :: loc', stk')
evalOp : (Vect arity (NF free) -> Maybe (NF free)) ->
@ -365,13 +341,12 @@ parameters (defs : Defs, topopts : EvalOpts)
evalAll [] = pure []
evalAll (c :: cs) = pure $ !(evalClosure defs c) :: !(evalAll cs)
evalDef : {vars : _} ->
Env Term free -> LocalEnv free vars -> EvalOpts ->
evalDef : Env Term free -> 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:
@ -382,20 +357,20 @@ parameters (defs : Defs, topopts : EvalOpts)
-- + 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'!

4
src/Core/Options.idr
View File

@ -99,6 +99,7 @@ record Session where
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
@ -143,7 +144,8 @@ defaultPPrint : PPrinter
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

2
src/Core/TT.idr
View File

@ -405,7 +405,7 @@ data UseSide = UseLeft | UseRight
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

6
src/Core/TTC.idr
View File

@ -583,7 +583,7 @@ mutual
toBuf b (CLocal fc {x} {idx} h) = do tag 0; toBuf b fc; toBuf b x; toBuf b idx
toBuf b (CRef fc n) = do tag 1; toBuf b fc; toBuf b n
toBuf b (CLam fc x sc) = do tag 2; toBuf b fc; toBuf b x; toBuf b sc
toBuf b (CLet fc x val sc) = do tag 3; toBuf b fc; toBuf b x; toBuf b val; toBuf b sc
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
toBuf b (CApp fc f as) = assert_total $ do tag 4; toBuf b fc; toBuf b f; toBuf b as
toBuf b (CCon fc t n as) = assert_total $ do tag 5; toBuf b fc; toBuf b t; toBuf b n; toBuf b as
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
x <- fromBuf b; sc <- fromBuf b
pure (CLam fc x sc)
3 => do fc <- fromBuf b
x <- fromBuf b; val <- fromBuf b; sc <- fromBuf b
pure (CLet fc x val sc)
x <- fromBuf b; inl <- fromBuf b; val <- fromBuf b; sc <- fromBuf b
pure (CLet fc x inl val sc)
4 => do fc <- fromBuf b
f <- fromBuf b; as <- fromBuf b
pure (CApp fc f as)

4
src/Idris/CommandLine.idr
View File

@ -71,6 +71,8 @@ data CLOpt
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 |
@ -147,6 +149,8 @@ options = [MkOpt ["--check", "-c"] [] [CheckOnly]
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)
]

51
src/Idris/Desugar.idr
View File

@ -547,9 +547,9 @@ mutual
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
@ -691,20 +691,26 @@ mutual
= 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))
pure (fst ntm, fst (snd ntm), tm')) is
cons' <- traverse (\ ntm => do tm' <- desugar AnyExpr ps (snd ntm)
pure (fst ntm, tm')) cons
= do is' <- traverse (\ (n,c,tm) => do tm' <- desugar AnyExpr ps tm
pure (n, c, tm')) is
let _ = the (List (Name, RigCount, RawImp)) is'
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
@ -713,21 +719,32 @@ mutual
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)
pure (fst ntm, tm')) params
= do params' <- traverse (\ (n,c,p,tm) =>
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))
@ -739,6 +756,16 @@ mutual
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

10
src/Idris/Elab/Implementation.idr
View File

@ -169,6 +169,11 @@ elabImplementation {vars} fc vis pass env nest is cons iname ps impln nusing mbo
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)
@ -199,11 +204,6 @@ elabImplementation {vars} fc vis pass env nest is cons iname ps impln nusing mbo
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

46
src/Idris/Parser.idr
View File

@ -398,23 +398,29 @@ mutual
rig <- getMult rigc
pure (rig, pat, ty))
pibindList : FileName -> FilePos -> IndentInfo ->
Rule (List (RigCount, Maybe Name, PTerm))
pibindList fname start indents
pibindListName : FileName -> FilePos -> IndentInfo ->
Rule (List (RigCount, Name, PTerm))
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
@ -624,8 +630,8 @@ mutual
record_ fname indents
= do start <- location
keyword "record"
commit
symbol "{"
commit
fs <- sepBy1 (symbol ",") (field fname indents)
symbol "}"
end <- location
@ -1263,6 +1269,30 @@ fieldDecl fname indents
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
@ -1270,9 +1300,9 @@ 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

17
src/Idris/Resugar.idr
View File

@ -340,14 +340,23 @@ mutual
toPRecord : {auto c : Ref Ctxt Defs} ->
{auto s : Ref Syn SyntaxInfo} ->
ImpRecord ->
Core (Name, List (Name, PTerm), Maybe Name, List PField)
Core (Name, List (Name, RigCount, PiInfo PTerm, PTerm), Maybe Name, List PField)
toPRecord (MkImpRecord fc n ps con fs)
= do ps' <- traverse (\ (n, ty) =>
= do ps' <- traverse (\ (n, c, p, ty) =>
do ty' <- toPTerm startPrec ty
pure (n, ty')) ps
p' <- mapPiInfo p
pure (n, c, p', ty')) ps
fs' <- traverse toPField fs
pure (n, ps', Just con, fs')
where
mapPiInfo : {auto c : Ref Ctxt Defs} ->
{auto s : Ref Syn SyntaxInfo} ->
PiInfo RawImp -> Core (PiInfo PTerm)
mapPiInfo Explicit = pure Explicit
mapPiInfo Implicit = pure Implicit
mapPiInfo AutoImplicit = pure AutoImplicit
mapPiInfo (DefImplicit p) = pure $ DefImplicit !(toPTerm startPrec p)
toPFnOpt : {auto c : Ref Ctxt Defs} ->
{auto s : Ref Syn SyntaxInfo} ->
FnOpt -> Core PFnOpt

3
src/Idris/SetOptions.idr
View File

@ -89,6 +89,9 @@ preOptions (FindIPKG :: opts)
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

11
src/Idris/Syntax.idr
View File

@ -223,7 +223,7 @@ mutual
PRecord : FC ->
Visibility ->
Name ->
(params : List (Name, PTerm)) ->
(params : List (Name, RigCount, PiInfo PTerm, PTerm)) ->
(conName : Maybe Name) ->
List PField ->
PDecl
@ -828,7 +828,7 @@ mapPTermM f = goPTerm where
<*> 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
@ -884,6 +884,13 @@ mapPTermM f = goPTerm where
(::) . (\ 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

62
src/Parser/Lexer.idr
View File

@ -40,20 +40,58 @@ export
Show (TokenData Token) where
show t = show (line t, col t, tok t)
||| In `comment` we are careful not to parse closing delimiters as
||| valid comments. i.e. you may not write many dashes followed by
||| a closing brace and call it a valid comment.
comment : Lexer
comment = is '-' <+> is '-' <+> many (isNot '\n')
comment
= is '-' <+> is '-' -- comment opener
<+> many (is '-') <+> reject (is '}') -- not a closing delimiter
<+> many (isNot '\n') -- till the end of line
toEndComment : (k : Nat) -> Recognise (k /= 0)
toEndComment Z = empty
toEndComment (S k)
= some (pred (\c => c /= '-' && c /= '{' && c /= '"'))
<+> toEndComment (S k)
<|> is '{' <+> is '-' <+> toEndComment (S (S k))
<|> is '-' <+> is '}' <+> toEndComment k
<|> comment <+> toEndComment (S k)
<|> stringLit <+> toEndComment (S k)
<|> is '{' <+> toEndComment (S k)
<|> is '-' <+> toEndComment (S k)
mutual
||| The mutually defined functions represent different states in a
||| small automaton.
||| `toEndComment` is the default state and it will munch through
||| the input until we detect a special character (a dash, an
||| opening brace, or a double quote) and then switch to the
||| appropriate state.
toEndComment : (k : Nat) -> Recognise (k /= 0)
toEndComment Z = empty
toEndComment (S k)
= some (pred (\c => c /= '-' && c /= '{' && c /= '"'))
<+> toEndComment (S k)
<|> is '{' <+> singleBrace k
<|> is '-' <+> singleDash k
<|> stringLit <+> toEndComment (S k)
||| After reading a single brace, we may either finish reading an
||| opening delimiter or ignore it (e.g. it could be an implicit
||| binder).
singleBrace : (k : Nat) -> Lexer
singleBrace k
= is '-' <+> many (is '-') -- opening delimiter
<+> singleDash (S k) -- handles the {----} special case
<|> toEndComment (S k) -- not a valid comment
||| After reading a single dash, we may either find another one,
||| meaning we may have started reading a line comment, or find
||| a closing brace meaning we have found a closing delimiter.
singleDash : (k : Nat) -> Lexer
singleDash k
= is '-' <+> doubleDash k -- comment or closing delimiter
<|> is '}' <+> toEndComment k -- closing delimiter
<|> toEndComment (S k) -- not a valid comment
||| After reading a double dash, we are potentially reading a line
||| comment unless the series of uninterrupted dashes is ended with
||| a closing brace in which case it is a closing delimiter.
doubleDash : (k : Nat) -> Lexer
doubleDash k = many (is '-') <+> choice -- absorb all dashes
[ is '}' <+> toEndComment k -- closing delimiter
, many (isNot '\n') <+> toEndComment (S k) -- line comment
]
blockComment : Lexer
blockComment = is '{' <+> is '-' <+> toEndComment 1

48
src/TTImp/Parser.idr
View File

@ -226,23 +226,30 @@ mutual
pure (rig, UN n, ty))
pibindList : FileName -> FilePos -> IndentInfo ->
Rule (List (RigCount, Maybe Name, RawImp))
pibindList fname start indents
pibindListName : FileName -> FilePos -> IndentInfo ->
Rule (List (RigCount, Name, RawImp))
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
@ -370,8 +377,8 @@ mutual
record_ fname indents
= do start <- location
keyword "record"
commit
symbol "{"
commit
fs <- sepBy1 (symbol ",") (field fname indents)
symbol "}"
sc <- expr fname indents
@ -550,18 +557,30 @@ dataDecl fname indents
end <- location
pure (MkImpData (MkFC fname start end) n ty opts cs)
ifaceParam : FileName -> IndentInfo -> Rule (Name, RawImp)
ifaceParam fname indents
recordParam : FileName -> IndentInfo -> Rule (List (Name, RigCount, PiInfo RawImp, RawImp))
recordParam fname indents
= do symbol "("
n <- name
symbol ":"
tm <- expr fname indents
start <- location
params <- pibindListName fname start 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
@ -593,7 +612,8 @@ recordDecl 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

24
src/TTImp/ProcessData.idr
View File

@ -195,16 +195,24 @@ getDetags fc tys
else pure rest
-- If exactly one argument is unerased, return its position
getRelevantArg : Defs -> Nat -> Maybe Nat -> NF [] -> Core (Maybe Nat)
getRelevantArg defs i rel (NBind fc _ (Pi Rig0 _ _) sc)
= getRelevantArg defs (1 + i) rel
getRelevantArg : Defs -> Nat -> Maybe Nat -> Bool -> NF [] ->
Core (Maybe (Bool, Nat))
getRelevantArg defs i rel world (NBind fc _ (Pi Rig0 _ _) sc)
= getRelevantArg defs (1 + i) rel world
!(sc defs (toClosure defaultOpts [] (Erased fc False)))
getRelevantArg defs i Nothing (NBind fc _ (Pi _ _ _) sc) -- found a relevant arg
= getRelevantArg defs (1 + i) (Just i)
-- %World is never inspected, so might as well be deleted from data types,
-- although it needs care when compiling to ensure that the function that
-- 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 (Just _) (NBind _ _ (Pi _ _ _) sc) -- more than one relevant
getRelevantArg defs i Nothing world (NBind fc _ (Pi _ _ _) sc) -- found a relevant arg
= getRelevantArg defs (1 + i) (Just i) world
!(sc defs (toClosure defaultOpts [] (Erased fc False)))
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
@ -213,7 +221,7 @@ findNewtype : {auto c : Ref Ctxt Defs} ->
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

51
src/TTImp/ProcessRecord.idr
View File

@ -15,10 +15,10 @@ import TTImp.TTImp
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)
= IPi fc RigW Explicit (Just n) ty (mkDataTy fc ps)
mkDataTy fc ((n, c, p, ty) :: ps)
= IPi fc c p (Just n) ty (mkDataTy fc ps)
elabRecord : {vars : _} ->
{auto c : Ref Ctxt Defs} ->
@ -27,7 +27,7 @@ elabRecord : {vars : _} ->
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 ()
@ -37,24 +37,29 @@ elabRecord {vars} eopts fc env nest newns vis tn params conName_in fields
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)
jname (n, t) = (Just n, Rig0, Implicit, t)
where
paramTelescope : List (Maybe Name, RigCount, PiInfo RawImp, RawImp)
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
@ -69,11 +74,19 @@ elabRecord {vars} eopts fc env nest newns vis tn params conName_in fields
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))
let conty = mkTy (map jname params) $
mkTy (map farg fields) retty
= do let conty = mkTy paramTelescope $
mkTy (map farg fields) recTy
let con = MkImpTy fc cname !(bindTypeNames [] (map fst params ++
map fname fields ++ vars) conty)
let dt = MkImpData fc tn !(bindTypeNames [] (map fst params ++
@ -89,16 +102,16 @@ elabRecord {vars} eopts fc env nest newns vis tn params conName_in fields
-- 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
@ -111,7 +124,7 @@ elabRecord {vars} eopts fc env nest newns vis tn params conName_in fields
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
@ -134,11 +147,11 @@ elabRecord {vars} eopts fc env nest newns vis tn params conName_in fields
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} ->

2
src/TTImp/TTImp.idr
View File

@ -264,7 +264,7 @@ mutual
public export
data ImpRecord : Type where
MkImpRecord : FC -> (n : Name) ->
(params : List (Name, RawImp)) ->
(params : List (Name, RigCount, PiInfo RawImp, RawImp)) ->
(conName : Name) ->
(fields : List IField) ->
ImpRecord

13
support/chez/support.ss
View File

@ -6,7 +6,7 @@
(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))))
@ -26,6 +26,9 @@
(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)))))
@ -42,11 +45,11 @@
(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)
@ -237,8 +240,8 @@
(define (blodwen-args)
(define (blodwen-build-args args)
(if (null? args)
(vector 0 '())
(vector 1 '() (car args) (blodwen-build-args (cdr args)))))
(vector 0) ; Prelude.List
(vector 1 (car args) (blodwen-build-args (cdr args)))))
(blodwen-build-args (command-line)))
(define (blodwen-hasenv var)

5
support/chicken/support.scm
View File

@ -6,7 +6,7 @@
(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))))
@ -26,6 +26,9 @@
(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)))))

10
support/racket/support.rkt
View File

@ -6,7 +6,7 @@
(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))))
@ -42,11 +42,11 @@
(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)
@ -244,8 +244,8 @@
(define (blodwen-args)
(define (blodwen-build-args args)
(if (null? args)
(vector 0 '())
(vector 1 '() (car args) (blodwen-build-args (cdr args)))))
(vector 0) ; Prelude.List
(vector 1 (car args) (blodwen-build-args (cdr args)))))
(blodwen-build-args
(cons (path->string (find-system-path 'run-file))
(vector->list (current-command-line-arguments)))))

9
tests/Main.idr
View File

@ -17,7 +17,7 @@ ttimpTests
"lazy001",
"nest001", "nest002",
"perf001", "perf002", "perf003",
"record001", "record002",
"record001", "record002", "record003",
"rewrite001",
"qtt001", "qtt002", "qtt003",
"search001", "search002", "search003", "search004", "search005",
@ -77,11 +77,11 @@ idrisTests
-- 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",
@ -98,7 +98,8 @@ chezTests : List String
chezTests
= ["chez001", "chez002", "chez003", "chez004", "chez005", "chez006",
"chez007", "chez008", "chez009", "chez010", "chez011", "chez012",
"chez013", "chez014", "chez016"]
"chez013", "chez014", "chez015", "chez016",
"reg001"]
ideModeTests : List String
ideModeTests

34
tests/chez/chez015/Numbers.idr Normal file
View File

@ -0,0 +1,34 @@
module Main
import Data.List
large : (a: Type) -> a
-- integer larger than 64 bits
large Integer = 3518437212345678901234567890123
-- int close to 2ˆ63
-- we expect some operations will overflow
large Int = 3518437212345678901234567890
small : (a: Type) -> a
small Integer = 437
small Int = 377
numOps : (Num a) => List ( a -> a -> a )
numOps = [ (+), (*) ]
negOps : (Neg a) => List (a -> a -> a)
negOps = [ (-) ]
integralOps : (Integral a) => List (a -> a -> a)
integralOps = [ div, mod ]
binOps : (Num a, Neg a, Integral a) => List (a -> a -> a)
binOps = numOps ++ negOps ++ integralOps
main : IO ()
main = do
putStrLn $ show (results Integer)
putStrLn $ show (results Int)
where
results : (a:Type) -> (Num a, Neg a, Integral a) => List a
results a = map (\ op => large a `op` small a) binOps

4
tests/chez/chez015/expected Normal file
View File

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

2
tests/chez/chez015/input Normal file
View File

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

3
tests/chez/chez015/run Executable file
View File

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

10
tests/chez/reg001/expected Normal file
View File

@ -0,0 +1,10 @@
3
4.2
"1.2"
4
1
"2.7"
5.9
2
2
2

21
tests/chez/reg001/numbers.idr Normal file
View File

@ -0,0 +1,21 @@
-- the commented-out cases are still wrong,
-- but fixing them as well would make other tests fail for mysterious reasons
-- see https://github.com/edwinb/Idris2/pull/281
main : IO ()
main = do
printLn $ 3
printLn $ 4.2
printLn $ "1.2"
printLn $ cast {to = Int} 4.8
printLn $ cast {to = Integer} 1.2
printLn $ cast {to = String} 2.7
-- printLn $ cast {to = Int} "1.2"
-- printLn $ cast {to = Integer} "2.7"
printLn $ cast {to = Double} "5.9"
printLn $ (the Int 6 `div` the Int 3)
printLn $ (the Integer 6 `div` the Integer 3)
printLn $ (cast {to = Int} "6.6" `div` cast "3.9")
-- printLn $ (cast {to = Integer} "6.6" `div` cast "3.9")

3
tests/chez/reg001/run Executable file
View File

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

2
tests/ideMode/ideMode001/expected
View File

@ -8,7 +8,7 @@
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)
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)
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)
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)
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)
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)
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)
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)

2
tests/ideMode/ideMode003/expected
View File

@ -8,7 +8,7 @@
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)
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)
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)
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)
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)
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)
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)
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)

16
tests/idris2/basic037/Comments.idr
View File

@ -1,3 +1,11 @@
{-------------------------}
-- These should be
-- ignored
{- {---------------} -}
-- Comments should have the right to be empty:
--
-- This is a valid comment {-
-- It should not lead to a parse error if nested in a
-- multiline comment
@ -21,3 +29,11 @@ myString = "Similarly, this is a valid string literal {- "
-- So we should be able to put it in a multiline comment
-}
{------------- Some people {---- like ---}
{- comments with
weird
----------}
closing delimiters
--}

12
tests/idris2/basic037/Issue279.idr Normal file
View File

@ -0,0 +1,12 @@
module Main
{-- comment 1 --}
someFunction : IO ()
{-- comment 2 --}
main : IO ()
main = do
someFunction
pure ()

2
tests/idris2/basic037/expected
View File

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

1
tests/idris2/basic037/run
View File

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

33
tests/idris2/record003/Record.idr Normal file
View File

@ -0,0 +1,33 @@
||| Test extended record syntax
data NotZero : Nat -> Type where
Is : {n : Nat} -> NotZero (S n)
record Positive (n : Nat) {auto 0 pos : NotZero n} where
constructor Check
a : Positive 1
a = Check
b : Positive 2
b = Check
{- Will not type-check
c : Positive 0
-}
data KindOfString = ASCII | UTF
UTForASCII : KindOfString -> Type
UTForASCII UTF = String
UTForASCII ASCII = List Char --- Just to demonstrate
record FlexiString { default UTF k : KindOfString} where
constructor MkFlexiString
val : UTForASCII k
c : FlexiString
c = MkFlexiString "hello"
d : FlexiString {k = ASCII}
d = MkFlexiString ['h', 'i']

1
tests/idris2/record003/expected Normal file
View File

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

3
tests/idris2/record003/run Executable file
View File

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

14
tests/idris2/reg016/Using.idr Normal file
View File

@ -0,0 +1,14 @@
module Using
interface MagmaT a where
op: a -> a -> a
interface MagmaT a => SemigroupT a where
assoc: (x, y, z: a) -> (x `op` y) `op` z = x `op` (y `op` z)
[NamedMagma] MagmaT Bool where
False `op` False = False
_ `op` _ = True
[NamedSemigroup] SemigroupT Bool using NamedMagma where
assoc = ?hole

1
tests/idris2/reg016/expected Normal file
View File

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

Some files were not shown because too many files have changed in this diff Show More