merge with upstream

This commit is contained in:
Mathew Polzin 2021-05-03 23:07:24 -07:00
commit 647c38b2fa
230 changed files with 6674 additions and 1635 deletions

View File

@ -45,4 +45,4 @@ jobs:
run: |
scheme --version
- name: Bootstrap and install
run: c:\msys64\usr\bin\bash -l -c "cd $env:PWD && make bootstrap && make install"
run: c:\msys64\usr\bin\bash -l -c "cd $env:PWD && make bootstrap && make bootstrap-test && make install"

View File

@ -13,10 +13,19 @@ REPL/IDE mode changes:
* Added `:search` command, which searches for functions by type
* `:load`/`:l` and `:cd` commands now only accept paths surrounded by double quotes
Syntax changes:
* The syntax for parameter blocks has been updated. It now allows to declare
implicit parameters and give multiplicities for parameters. The old syntax
is still available for compatibility purposes but will be removed in the
future.
Compiler changes:
* Racket codegen now always uses `blodwen-sleep` instead of `idris2_sleep` in
order to not block the Racket runtime when `sleep` is called.
* Added `--profile` flag, which generates profile data if supported by a back
end. Currently supported by the Chez and Racket back ends.
Library changes:
@ -29,18 +38,6 @@ Library changes:
Other changes:
* The `version` field in `.ipkg` files is now used. Packages are installed into
a directory which includes its version number, and dependencies can have
version number ranges using `<=`, `<`, `>=`, `>`, `==` to express version
constraints. Version numbers must be in the form of integers, separated by
dots (e.g. `1.0`, `0.3.0`, `3.1.4.1.5` etc)
* Idris now looks in the current working directory, under a subdirectory
`depends` for local installations of packages before looking globally.
* Added an environment variable `IDRIS2_PACKAGE_PATH` for extending where to
look for packages.
Other changes:
* The `version` field in `.ipkg` files is now used. Packages are installed into
a directory which includes its version number, and dependencies can have
version number ranges using `<=`, `<`, `>=`, `>`, `==` to express version

View File

@ -32,7 +32,7 @@ of `make` in the following steps.
**NOTE**: If you're running macOS on Apple Silicon (arm64) you may need to run
"`arch -x86_64 make ...`" instead of `make` in the following steps.
### 1: Set the PREFIX
### 1: Set installation target directory
- Change the `PREFIX` in `config.mk`. The default is to install in
`$HOME/.idris2`
@ -95,8 +95,9 @@ code generator. To do so, once everything is successfully installed, type:
- `make install-api`
The API will only work if you've completed the self-hosting step, step 3, since
the intermediate code versions need to be consistent throughout.
The API will only work if you've completed the self-hosting step, step 4, since
the intermediate code versions need to be consistent throughout. Otherwise, you
will get an `Error in TTC: TTC data is in an older format` error.
### Troubleshooting

100
Makefile
View File

@ -5,7 +5,7 @@ export IDRIS2_BOOT ?= idris2
# Idris 2 executable we're building
NAME = idris2
TARGETDIR = build/exec
TARGETDIR = ${CURDIR}/build/exec
TARGET = ${TARGETDIR}/${NAME}
MAJOR=0
@ -22,6 +22,7 @@ ifeq ($(shell git status >/dev/null 2>&1; echo $$?), 0)
endif
export IDRIS2_VERSION := ${MAJOR}.${MINOR}.${PATCH}
NAME_VERSION := ${NAME}-${IDRIS2_VERSION}
IDRIS2_SUPPORT := libidris2_support${SHLIB_SUFFIX}
IDRIS2_APP_IPKG := idris2.ipkg
IDRIS2_LIB_IPKG := idris2api.ipkg
@ -37,13 +38,10 @@ else
SEP := :
endif
# Library and data paths for test
IDRIS2_TEST_LIBS ?= ${IDRIS2_CURDIR}/lib
IDRIS2_TEST_DATA ?= ${IDRIS2_CURDIR}/support
TEST_PREFIX ?= ${IDRIS2_CURDIR}/build/env
# Library and data paths for bootstrap-test
IDRIS2_BOOT_TEST_LIBS := ${IDRIS2_CURDIR}/bootstrap/${NAME}-${IDRIS2_VERSION}/lib
IDRIS2_BOOT_TEST_DATA := ${IDRIS2_CURDIR}/bootstrap/${NAME}-${IDRIS2_VERSION}/support
IDRIS2_BOOT_PREFIX := ${IDRIS2_CURDIR}/bootstrap
# These are the library path in the build dir to be used during build
export IDRIS2_BOOT_PATH := "${IDRIS2_CURDIR}/libs/prelude/build/ttc${SEP}${IDRIS2_CURDIR}/libs/base/build/ttc${SEP}${IDRIS2_CURDIR}/libs/contrib/build/ttc${SEP}${IDRIS2_CURDIR}/libs/network/build/ttc${SEP}${IDRIS2_CURDIR}/libs/test/build/ttc"
@ -51,19 +49,15 @@ export IDRIS2_BOOT_PATH := "${IDRIS2_CURDIR}/libs/prelude/build/ttc${SEP}${IDRIS
export SCHEME
.PHONY: all idris2-exec ${TARGET} testbin support support-lib support-clean clean distclean FORCE
.PHONY: all idris2-exec libdocs testenv testenv-clean support support-clean clean FORCE
all: support ${TARGET} support-lib libs
all: support ${TARGET} libs
idris2-exec: ${TARGET}
${TARGET}: src/IdrisPaths.idr
${IDRIS2_BOOT} --build ${IDRIS2_APP_IPKG}
support-lib:
mkdir -p lib
install support/c/${IDRIS2_SUPPORT} lib
# We use FORCE to always rebuild IdrisPath so that the git SHA1 info is always up to date
src/IdrisPaths.idr: FORCE
echo '-- @generated' > src/IdrisPaths.idr
@ -74,31 +68,50 @@ src/IdrisPaths.idr: FORCE
FORCE:
prelude:
${MAKE} -C libs/prelude IDRIS2=../../${TARGET} IDRIS2_PATH=${IDRIS2_BOOT_PATH}
${MAKE} -C libs/prelude IDRIS2=${TARGET} IDRIS2_PATH=${IDRIS2_BOOT_PATH}
base: prelude
${MAKE} -C libs/base IDRIS2=../../${TARGET} IDRIS2_PATH=${IDRIS2_BOOT_PATH}
${MAKE} -C libs/base IDRIS2=${TARGET} IDRIS2_PATH=${IDRIS2_BOOT_PATH}
network: prelude
${MAKE} -C libs/network IDRIS2=../../${TARGET} IDRIS2_PATH=${IDRIS2_BOOT_PATH}
${MAKE} -C libs/network IDRIS2=${TARGET} IDRIS2_PATH=${IDRIS2_BOOT_PATH}
contrib: base
${MAKE} -C libs/contrib IDRIS2=../../${TARGET} IDRIS2_PATH=${IDRIS2_BOOT_PATH}
${MAKE} -C libs/contrib IDRIS2=${TARGET} IDRIS2_PATH=${IDRIS2_BOOT_PATH}
test-lib: contrib
${MAKE} -C libs/test IDRIS2=../../${TARGET} IDRIS2_PATH=${IDRIS2_BOOT_PATH}
${MAKE} -C libs/test IDRIS2=${TARGET} IDRIS2_PATH=${IDRIS2_BOOT_PATH}
libs : prelude base contrib network test-lib
testbin:
@${MAKE} -C tests testbin IDRIS2=../${TARGET} IDRIS2_PATH=${IDRIS2_BOOT_PATH} IDRIS2_DATA=${IDRIS2_TEST_DATA} IDRIS2_LIBS=${IDRIS2_TEST_LIBS}
libdocs:
${MAKE} -C libs/prelude docs IDRIS2=${TARGET} IDRIS2_PATH=${IDRIS2_BOOT_PATH}
${MAKE} -C libs/base docs IDRIS2=${TARGET} IDRIS2_PATH=${IDRIS2_BOOT_PATH}
${MAKE} -C libs/contrib docs IDRIS2=${TARGET} IDRIS2_PATH=${IDRIS2_BOOT_PATH}
${MAKE} -C libs/network docs IDRIS2=${TARGET} IDRIS2_PATH=${IDRIS2_BOOT_PATH}
test: testbin
${TEST_PREFIX}/${NAME_VERSION} :
${MAKE} install-support PREFIX=${TEST_PREFIX}
ln -s ${IDRIS2_CURDIR}/libs/prelude/build/ttc ${TEST_PREFIX}/${NAME_VERSION}/prelude-${IDRIS2_VERSION}
ln -s ${IDRIS2_CURDIR}/libs/base/build/ttc ${TEST_PREFIX}/${NAME_VERSION}/base-${IDRIS2_VERSION}
ln -s ${IDRIS2_CURDIR}/libs/test/build/ttc ${TEST_PREFIX}/${NAME_VERSION}/test-${IDRIS2_VERSION}
ln -s ${IDRIS2_CURDIR}/libs/contrib/build/ttc ${TEST_PREFIX}/${NAME_VERSION}/contrib-${IDRIS2_VERSION}
ln -s ${IDRIS2_CURDIR}/libs/network/build/ttc ${TEST_PREFIX}/${NAME_VERSION}/network-${IDRIS2_VERSION}
testenv:
@${MAKE} ${TEST_PREFIX}/${NAME_VERSION}
@${MAKE} -C tests testbin IDRIS2=${TARGET} IDRIS2_PREFIX=${TEST_PREFIX}
testenv-clean:
$(RM) -r ${TEST_PREFIX}/${NAME_VERSION}
test: testenv
@echo
@echo "NOTE: \`${MAKE} test\` does not rebuild Idris or the libraries packaged with it; to do that run \`${MAKE}\`"
@if [ ! -x "${TARGET}" ]; then echo "ERROR: Missing IDRIS2 executable. Cannot run tests!\n"; exit 1; fi
@echo
@${MAKE} -C tests only=$(only) IDRIS2=../../../${TARGET} IDRIS2_PATH=${IDRIS2_BOOT_PATH} IDRIS2_DATA=${IDRIS2_TEST_DATA} IDRIS2_LIBS=${IDRIS2_TEST_LIBS}
@${MAKE} -C tests only=$(only) IDRIS2=${TARGET} IDRIS2_PREFIX=${TEST_PREFIX}
support:
@${MAKE} -C support/c
@ -115,12 +128,11 @@ clean-libs:
${MAKE} -C libs/network clean
${MAKE} -C libs/test clean
clean: clean-libs support-clean
clean: clean-libs support-clean testenv-clean
-${IDRIS2_BOOT} --clean ${IDRIS2_APP_IPKG}
$(RM) src/IdrisPaths.idr
${MAKE} -C tests clean
$(RM) -r build
$(RM) -r lib
install: install-idris2 install-support install-libs
@ -134,55 +146,57 @@ ifeq ($(OS), windows)
-install ${TARGET}.cmd ${PREFIX}/bin
endif
mkdir -p ${PREFIX}/lib/
install lib/${IDRIS2_SUPPORT} ${PREFIX}/lib
install support/c/${IDRIS2_SUPPORT} ${PREFIX}/lib
mkdir -p ${PREFIX}/bin/${NAME}_app
install ${TARGETDIR}/${NAME}_app/* ${PREFIX}/bin/${NAME}_app
install-support:
mkdir -p ${PREFIX}/idris2-${IDRIS2_VERSION}/support/chez
mkdir -p ${PREFIX}/idris2-${IDRIS2_VERSION}/support/racket
mkdir -p ${PREFIX}/idris2-${IDRIS2_VERSION}/support/gambit
mkdir -p ${PREFIX}/idris2-${IDRIS2_VERSION}/support/js
install support/chez/* ${PREFIX}/idris2-${IDRIS2_VERSION}/support/chez
install support/racket/* ${PREFIX}/idris2-${IDRIS2_VERSION}/support/racket
install support/gambit/* ${PREFIX}/idris2-${IDRIS2_VERSION}/support/gambit
install support/js/* ${PREFIX}/idris2-${IDRIS2_VERSION}/support/js
mkdir -p ${PREFIX}/${NAME_VERSION}/support/chez
mkdir -p ${PREFIX}/${NAME_VERSION}/support/docs
mkdir -p ${PREFIX}/${NAME_VERSION}/support/racket
mkdir -p ${PREFIX}/${NAME_VERSION}/support/gambit
mkdir -p ${PREFIX}/${NAME_VERSION}/support/js
install support/chez/* ${PREFIX}/${NAME_VERSION}/support/chez
install support/docs/* ${PREFIX}/${NAME_VERSION}/support/docs
install support/racket/* ${PREFIX}/${NAME_VERSION}/support/racket
install support/gambit/* ${PREFIX}/${NAME_VERSION}/support/gambit
install support/js/* ${PREFIX}/${NAME_VERSION}/support/js
@${MAKE} -C support/c install
@${MAKE} -C support/refc install
install-libs:
${MAKE} -C libs/prelude install IDRIS2?=../../${TARGET} IDRIS2_PATH=${IDRIS2_BOOT_PATH}
${MAKE} -C libs/base install IDRIS2?=../../${TARGET} IDRIS2_PATH=${IDRIS2_BOOT_PATH}
${MAKE} -C libs/contrib install IDRIS2?=../../${TARGET} IDRIS2_PATH=${IDRIS2_BOOT_PATH}
${MAKE} -C libs/network install IDRIS2?=../../${TARGET} IDRIS2_PATH=${IDRIS2_BOOT_PATH}
${MAKE} -C libs/test install IDRIS2?=../../${TARGET} IDRIS2_PATH=${IDRIS2_BOOT_PATH}
${MAKE} -C libs/prelude install IDRIS2?=${TARGET} IDRIS2_PATH=${IDRIS2_BOOT_PATH}
${MAKE} -C libs/base install IDRIS2?=${TARGET} IDRIS2_PATH=${IDRIS2_BOOT_PATH}
${MAKE} -C libs/contrib install IDRIS2?=${TARGET} IDRIS2_PATH=${IDRIS2_BOOT_PATH}
${MAKE} -C libs/network install IDRIS2?=${TARGET} IDRIS2_PATH=${IDRIS2_BOOT_PATH}
${MAKE} -C libs/test install IDRIS2?=${TARGET} IDRIS2_PATH=${IDRIS2_BOOT_PATH}
.PHONY: bootstrap bootstrap-build bootstrap-racket bootstrap-racket-build bootstrap-test bootstrap-clean
# Bootstrapping using SCHEME
bootstrap: support support-lib
bootstrap: support
cp support/c/${IDRIS2_SUPPORT} bootstrap/idris2_app
sed 's/libidris2_support.so/${IDRIS2_SUPPORT}/g; s|__PREFIX__|${IDRIS2_CURDIR}/bootstrap|g' \
sed 's/libidris2_support.so/${IDRIS2_SUPPORT}/g; s|__PREFIX__|${IDRIS2_BOOT_PREFIX}|g' \
bootstrap/idris2_app/idris2.ss \
> bootstrap/idris2_app/idris2-boot.ss
$(SHELL) ./bootstrap-stage1-chez.sh
IDRIS2_CG="chez" $(SHELL) ./bootstrap-stage2.sh
# Bootstrapping using racket
bootstrap-racket: support support-lib
bootstrap-racket: support
cp support/c/${IDRIS2_SUPPORT} bootstrap/idris2_app
sed 's|__PREFIX__|${IDRIS2_CURDIR}/bootstrap|g' \
sed 's|__PREFIX__|${IDRIS2_BOOT_PREFIX}|g' \
bootstrap/idris2_app/idris2.rkt \
> bootstrap/idris2_app/idris2-boot.rkt
$(SHELL) ./bootstrap-stage1-racket.sh
IDRIS2_CG="racket" $(SHELL) ./bootstrap-stage2.sh
bootstrap-test:
$(MAKE) test INTERACTIVE='' IDRIS2_PATH=${IDRIS2_BOOT_PATH} IDRIS2_TEST_DATA=${IDRIS2_BOOT_TEST_DATA} IDRIS2_TEST_LIBS=${IDRIS2_BOOT_TEST_LIBS}
$(MAKE) test INTERACTIVE='' IDRIS2_PREFIX=${IDRIS2_BOOT_PREFIX}
bootstrap-clean:
$(RM) -r bootstrap/bin bootstrap/lib bootstrap/idris2-${IDRIS2_VERSION}
$(RM) -r bootstrap/bin bootstrap/lib bootstrap/${NAME_VERSION}
$(RM) bootstrap/idris2boot* bootstrap/idris2_app/idris2-boot.* bootstrap/idris2_app/${IDRIS2_SUPPORT}

View File

@ -43,6 +43,7 @@ exceptions. The most notable user visible differences, which might cause Idris
Notably, elaborator reflection will exist, but most likely in a slightly
different form because the internal details of the elaborator are different.
+ The `Prelude` is much smaller (and easier to replace with an alternative).
Command-line option `--no-prelude` can be used to not implicitly import `Prelude`.
+ `let x = val in e` no longer computes with `x` in `e`, instead being
essentially equivalent to `(\x => e) val`. This is to make the
behaviour of `let` consistent in the presence of `case` and `with` (where

View File

@ -3,4 +3,5 @@
[ ] Change version numbers in prelude, base, contrib, network, and test ipkgs
[ ] Update bootstrap chez and racket
[ ] Tag on github with version number (in the form vX.Y.Z)
[ ] make libdocs and upload to idris-lang.org
[ ] Run release script

View File

@ -1,5 +1,6 @@
##### Options which a user might set before building go here #####
# Where to install idris2 binaries and libraries
PREFIX ?= $(HOME)/.idris2
# For Windows targets. Set to 1 to support Windows 7.

View File

@ -11,8 +11,8 @@ codegen in the list will be set as the default codegen.
Getting started
===============
To use Idris 2 as a library you need to install it with (at the top level of the
Idris2 repo)
To use Idris 2 as a library you need a self-hosting installation and
then install the `idris2api` library (at the top level of the Idris2 repo)
::

View File

@ -48,6 +48,12 @@ This will compile the expression ``Main.main``, generating an executable
``hello`` (with an extension depending on the code generator) in the
``build/exec`` directory.
If the backend supports it, you can generate profiling data by setting
the ``profile`` flag, either by starting Idris with ``--profile``, or
running ``:set profile`` at the REPL. The profile data generated will depend
on the back end you are using. Currently, the Chez and Racket back ends
support generating profile data.
There are five code generators provided in Idris 2, and (later) there will be
a system for plugging in new code generators for a variety of targets. The
default is to compile via Chez Scheme, with an alternative via Racket or Gambit.

View File

@ -0,0 +1,72 @@
********
Builtins
********
.. role:: idris(code)
:language: idris
Idris2 supports an optimised runtime representation of some types,
using the ``%builtin`` pragma.
For now only ``Nat``-like types has been implemented.
``%builtin Natural``
====================
I suggest having a look at the source for ``Nat`` (in ``Prelude.Types``) before reading this section.
The ``%builtin Natural`` pragma converts recursive/unary representations of natural numbers
into primitive ``Integer`` representations.
This massively reduces the memory usage and offers a small speed improvement,
for example with the unary representation ``the Nat 1000`` would take up about 2000 * 8 bytes
(1000 for the tag, 1000 for the pointers) whereas the ``Integer`` representation takes about 8 to 16 bytes.
Here's an example:
.. code-block:: idris
data Nat
= Z
| S Nat
%builtin Natural Nat
Note that the order of the constructors doesn't matter.
Furthermore this pragma supports GADTs
so long as any extra arguments are erased.
For example:
.. code-block:: idris
data Fin : Nat -> Type where
FZ : Fin (S k)
FS : Fin k -> Fin (S k)
%builtin Natural Fin
works because the ``k`` is always erased.
This doesn't work if the argument to the ``S``-like constructor
is ``Inf`` (sometime known as ``CoNat``) as these can be infinite
or is ``Lazy`` as it wouldn't preserve laziness semantics.
During codegen any occurance of ``Nat`` will be converted to the faster ``Integer`` implementation.
Here are the specifics for the conversion:
``Z`` => ``0``
``S k`` => ``1 + k``
.. code-block:: idris
case k of
Z => zexp
S k' => sexp
=>
.. code-block:: idris
case k of
0 => zexp
_ => let k' = k - 1 in sexp

View File

@ -21,3 +21,4 @@ This is a placeholder, to get set up with readthedocs.
records
literate
overloadedlit
builtins

View File

@ -277,12 +277,18 @@ defined as follows:
interface Applicative m => Monad (m : Type -> Type) where
(>>=) : m a -> (a -> m b) -> m b
There is also a non-binding sequencing operator, defined for ``Monad`` as:
.. code-block:: idris
v >> e = v >>= \_ => e
Inside a ``do`` block, the following syntactic transformations are
applied:
- ``x <- v; e`` becomes ``v >>= (\x => e)``
- ``v; e`` becomes ``v >>= (\_ => e)``
- ``v; e`` becomes ``v >> e``
- ``let x = v; e`` becomes ``let x = v in e``
@ -305,10 +311,10 @@ Using this we can, for example, define a function which adds two
y' <- y -- Extract value from y
pure (x' + y') -- Add them
This function will extract the values from ``x`` and ``y``, if they
are both available, or return ``Nothing`` if one or both are not ("fail fast"). Managing the
``Nothing`` cases is achieved by the ``>>=`` operator, hidden by the
``do`` notation.
This function will extract the values from ``x`` and ``y``, if they are both
available, or return ``Nothing`` if one or both are not ("fail fast"). Managing
the ``Nothing`` cases is achieved by the ``>>=`` operator, hidden by the ``do``
notation.
::
@ -318,10 +324,10 @@ are both available, or return ``Nothing`` if one or both are not ("fail fast").
Nothing
The translation of ``do`` notation is entirely syntactic, so there is no
need for the ``(>>=)`` operator to be the operator defined in the ``Monad``
interface. Idris will, in general, try to disambiguate which ``(>>=)`` you
mean by type, but you can explicitly choose with qualified do notation,
for example:
need for the ``(>>=)`` and ``(>>)`` operators to be the operator defined in the
``Monad`` interface. Idris will, in general, try to disambiguate which
operators you mean by type, but you can explicitly choose with qualified do
notation, for example:
.. code-block:: idris
@ -331,8 +337,8 @@ for example:
y' <- y -- Extract value from y
pure (x' + y') -- Add them
The ``Prelude.do`` means that Idris will use the ``(>>=)`` operator defined
in the ``Prelude``.
The ``Prelude.do`` means that Idris will use the ``(>>=)`` and ``(>>)``
operators defined in the ``Prelude``.
Pattern Matching Bind
~~~~~~~~~~~~~~~~~~~~~

View File

@ -4,5 +4,9 @@ depends = network
sourcedir = "src"
-- Set if you want the executable to generate profiling data
-- (Currently supported by Racket and Chez back ends, others ignore it)
-- opts = "--profile"
main = Idris.Main
executable = idris2

View File

@ -8,6 +8,7 @@ modules =
Algebra.ZeroOneOmega,
Compiler.ANF,
Compiler.CaseOpts,
Compiler.Common,
Compiler.CompileExpr,
Compiler.Inline,
@ -22,6 +23,7 @@ modules =
Compiler.ES.RemoveUnused,
Compiler.ES.TailRec,
Compiler.RefC.CC,
Compiler.RefC.RefC,
Compiler.Scheme.Chez,
@ -67,18 +69,22 @@ modules =
Idris.CommandLine,
Idris.Desugar,
Idris.Env,
Idris.Doc.HTML,
Idris.DocString,
Idris.Driver,
Idris.Error,
Idris.ModTree,
Idris.Package,
Idris.Package.Init,
Idris.Package.Types,
Idris.Parser,
Idris.Parser.Let,
Idris.Pretty,
Idris.Pretty.Render,
Idris.ProcessIdr,
Idris.REPL,
Idris.REPLCommon,
Idris.REPLOpts,
Idris.Resugar,
Idris.SetOptions,
Idris.Syntax,
@ -96,6 +102,10 @@ modules =
Idris.IDEMode.SyntaxHighlight,
Idris.IDEMode.TokenLine,
Idris.REPL.Common,
Idris.REPL.Opts,
Idris.REPL.FuzzySearch,
Libraries.Control.ANSI,
Libraries.Control.ANSI.CSI,
Libraries.Control.ANSI.SGR,
@ -112,6 +122,7 @@ modules =
Libraries.Data.List.Lazy,
Libraries.Data.List1,
Libraries.Data.NameMap,
Libraries.Data.PosMap,
Libraries.Data.SortedMap,
Libraries.Data.SortedSet,
Libraries.Data.String.Extra,
@ -119,6 +130,8 @@ modules =
Libraries.Data.StringMap,
Libraries.Data.StringTrie,
Libraries.System.Directory.Tree,
Libraries.Text.Bounded,
Libraries.Text.Distance.Levenshtein,
Libraries.Text.Lexer,
@ -129,6 +142,7 @@ modules =
Libraries.Text.Parser.Core,
Libraries.Text.PrettyPrint.Prettyprinter,
Libraries.Text.PrettyPrint.Prettyprinter.Doc,
Libraries.Text.PrettyPrint.Prettyprinter.Render.HTML,
Libraries.Text.PrettyPrint.Prettyprinter.Render.String,
Libraries.Text.PrettyPrint.Prettyprinter.Render.Terminal,
Libraries.Text.PrettyPrint.Prettyprinter.SimpleDocTree,
@ -164,6 +178,7 @@ modules =
TTImp.Impossible,
TTImp.Parser,
TTImp.PartialEval,
TTImp.ProcessBuiltin,
TTImp.ProcessData,
TTImp.ProcessDecls,
TTImp.ProcessDef,

View File

@ -2,6 +2,7 @@ module Control.App
import Data.IORef
||| `Error` is a type synonym for `Type`, specify for exception handling.
public export
Error : Type
Error = Type
@ -11,6 +12,8 @@ data HasErr : Error -> List Error -> Type where
Here : HasErr e (e :: es)
There : HasErr e es -> HasErr e (e' :: es)
||| States whether the program's execution path is linear or might throw exceptions so that we can know
||| whether it is safe to reference linear resources.
public export
data Path = MayThrow | NoThrow
@ -86,6 +89,11 @@ prim_app1_bind : (1 act : PrimApp1 Any a) ->
prim_app1_bind fn k w
= let MkApp1ResW x' w' = fn w in k x' w'
||| A type supports throwing and catching exceptions. See `interface Exception err e` for details.
||| @ l An implicit Path states whether the program's execution path is linear or might throw
||| exceptions. The default value is `MayThrow` which represents that the program might throw.
||| @ es A list of exception types that can be thrown. Constrained interfaces can be defined by
||| parameterising with a list of errors `es`.
export
data App : {default MayThrow l : Path} ->
(es : List Error) -> Type -> Type where
@ -255,8 +263,15 @@ new val prog
public export
interface Exception err e where
throw : err -> App e a
catch : App e a -> (err -> App e a) -> App e a
||| Throw an exception.
||| @ ev Value of the exception.
throw : (ev : err) -> App e a
||| Use with a given computation to do exception-catching.
||| If any exception is raised then the handler is executed.
||| @ act The computation to run.
||| @ k Handler to invoke if an exception is raised.
||| @ ev Value of the exception passed as an argument to the handler.
catch : (act : App e a) -> (k : (ev : err) -> App e a) -> App e a
findException : HasErr e es -> e -> OneOf es MayThrow
findException Here err = First err
@ -313,6 +328,8 @@ public export
Init : List Error
Init = [AppHasIO]
||| The only way provided by `Control.App` to run an App.
||| @ Init A concrete list of errors.
export
run : App {l} Init a -> IO a
run (MkApp prog)

View File

@ -0,0 +1,112 @@
module Control.Applicative.Const
import Data.Contravariant
import Data.Bits
public export
record Const (a : Type) (b : Type) where
constructor MkConst
runConst : a
public export
Eq a => Eq (Const a b) where
(==) = (==) `on` runConst
public export
Ord a => Ord (Const a b) where
compare = compare `on` runConst
export
Show a => Show (Const a b) where
showPrec p (MkConst v) = showCon p "MkConst" (showArg v)
public export
Semigroup a => Semigroup (Const a b) where
MkConst x <+> MkConst y = MkConst (x <+> y)
public export
Monoid a => Monoid (Const a b) where
neutral = MkConst neutral
public export
Num a => Num (Const a b) where
MkConst x + MkConst y = MkConst (x + y)
MkConst x * MkConst y = MkConst (x * y)
fromInteger = MkConst . fromInteger
public export
Neg a => Neg (Const a b) where
negate (MkConst x) = MkConst (negate x)
MkConst x - MkConst y = MkConst (x - y)
public export
Abs a => Abs (Const a b) where
abs (MkConst x) = MkConst (abs x)
public export
Fractional a => Fractional (Const a b) where
recip (MkConst x) = MkConst (recip x)
MkConst x / MkConst y = MkConst (x / y)
public export
Integral a => Integral (Const a b) where
MkConst x `div` MkConst y = MkConst (x `div` y)
MkConst x `mod` MkConst y = MkConst (x `mod` y)
public export
Bits a => Bits (Const a b) where
Index = Index {a}
MkConst x .&. MkConst y = MkConst (x .&. y)
MkConst x .|. MkConst y = MkConst (x .|. y)
MkConst x `xor` MkConst y = MkConst (x `xor` y)
shiftL (MkConst v) ix = MkConst (shiftL v ix)
shiftR (MkConst v) ix = MkConst (shiftR v ix)
bit = MkConst . bit
zeroBits = MkConst zeroBits
complement (MkConst v) = MkConst (complement v)
oneBits = MkConst oneBits
complementBit (MkConst v) ix = MkConst (complementBit v ix)
clearBit (MkConst v) ix = MkConst (clearBit v ix)
testBit (MkConst v) ix = testBit v ix
setBit (MkConst v) ix = MkConst (setBit v ix)
public export
FromString a => FromString (Const a b) where
fromString = MkConst . fromString
public export
Functor (Const a) where
map _ (MkConst v) = MkConst v
public export
Contravariant (Const a) where
contramap _ (MkConst v) = MkConst v
public export
Monoid a => Applicative (Const a) where
pure _ = MkConst neutral
MkConst x <*> MkConst y = MkConst (x <+> y)
public export
Foldable (Const a) where
foldr _ acc _ = acc
foldl _ acc _ = acc
null _ = True
public export
Traversable (Const a) where
traverse _ (MkConst v) = pure (MkConst v)
public export
Bifunctor Const where
bimap f _ (MkConst v) = MkConst (f v)
public export
Bifoldable Const where
bifoldr f _ acc (MkConst v) = f v acc
bifoldl f _ acc (MkConst v) = f acc v
binull _ = False
public export
Bitraversable Const where
bitraverse f _ (MkConst v) = MkConst <$> f v

View File

@ -1,5 +1,7 @@
module Control.Monad.Identity
import Data.Bits
public export
record Identity (a : Type) where
constructor Id
@ -43,3 +45,49 @@ public export
public export
(Monoid a) => Monoid (Identity a) where
neutral = Id (neutral)
public export
Num a => Num (Identity a) where
Id x + Id y = Id (x + y)
Id x * Id y = Id (x * y)
fromInteger = Id . fromInteger
public export
Neg a => Neg (Identity a) where
negate (Id x) = Id (negate x)
Id x - Id y = Id (x - y)
public export
Abs a => Abs (Identity a) where
abs (Id x) = Id (abs x)
public export
Fractional a => Fractional (Identity a) where
recip (Id x) = Id (recip x)
Id x / Id y = Id (x / y)
public export
Integral a => Integral (Identity a) where
Id x `div` Id y = Id (x `div` y)
Id x `mod` Id y = Id (x `mod` y)
public export
Bits a => Bits (Identity a) where
Index = Index {a}
Id x .&. Id y = Id (x .&. y)
Id x .|. Id y = Id (x .|. y)
Id x `xor` Id y = Id (x `xor` y)
shiftL (Id v) ix = Id (shiftL v ix)
shiftR (Id v) ix = Id (shiftR v ix)
bit = Id . bit
zeroBits = Id zeroBits
complement (Id v) = Id (complement v)
oneBits = Id oneBits
complementBit (Id v) ix = Id (complementBit v ix)
clearBit (Id v) ix = Id (clearBit v ix)
testBit (Id v) ix = testBit v ix
setBit (Id v) ix = Id (setBit v ix)
public export
FromString a => FromString (Identity a) where
fromString = Id . fromString

View File

@ -109,3 +109,16 @@ export
notFalseIsTrue : {1 x : Bool} -> Not (x = False) -> x = True
notFalseIsTrue {x=True} _ = Refl
notFalseIsTrue {x=False} f = absurd $ f Refl
--------------------------------------------------------------------------------
-- Decidability specialized on bool
--------------------------------------------------------------------------------
||| You can reverse decidability when bool is involved.
-- Given a contra on bool equality (a = b) -> Void, produce a proof of the opposite (that (not a) = b)
public export
invertContraBool : (a : Bool) -> (b : Bool) -> (a = b -> Void) -> (not a = b)
invertContraBool False False contra = absurd $ contra Refl
invertContraBool False True contra = Refl
invertContraBool True False contra = Refl
invertContraBool True True contra = absurd $ contra Refl

View File

@ -0,0 +1,48 @@
module Data.Contravariant
infixl 4 >$, >$<, >&<, $<
||| Contravariant functors
public export
interface Contravariant (0 f : Type -> Type) where
contramap : (a -> b) -> f b -> f a
(>$) : b -> f b -> f a
v >$ fb = contramap (const v) fb
||| If `f` is both `Functor` and `Contravariant` then by the time you factor in the
||| laws of each of those classes, it can't actually use its argument in any
||| meaningful capacity.
public export %inline
phantom : (Functor f, Contravariant f) => f a -> f b
phantom fa = () >$ (fa $> ())
||| This is an infix alias for `contramap`.
public export %inline
(>$<) : Contravariant f => (a -> b) -> f b -> f a
(>$<) = contramap
||| This is an infix version of `contramap` with the arguments flipped.
public export %inline
(>&<) : Contravariant f => f b -> (a -> b) -> f a
(>&<) = flip contramap
||| This is `>$` with its arguments flipped.
public export %inline
($<) : Contravariant f => f b -> b -> f a
($<) = flip (>$)
||| Composition of `Contravariant` is a `Functor`.
public export
[Compose] (Contravariant f, Contravariant g) => Functor (f . g) where
map = contramap . contramap
||| Composition of a `Functor` and a `Contravariant` is a `Contravariant`.
public export
[ComposeFC] (Functor f, Contravariant g) => Contravariant (f . g) where
contramap = map . contramap
||| Composition of a `Contravariant` and a `Functor` is a `Contravariant`.
public export
[ComposeCF] (Contravariant f, Functor g) => Contravariant (f . g) where
contramap = contramap . map

View File

@ -17,6 +17,14 @@ data Fin : (n : Nat) -> Type where
FZ : Fin (S k)
FS : Fin k -> Fin (S k)
||| Cast between Fins with equal indices
public export
cast : {n : Nat} -> (0 eq : m = n) -> Fin m -> Fin n
cast {n = S _} eq FZ = FZ
cast {n = Z} eq FZ impossible
cast {n = S _} eq (FS k) = FS (cast (succInjective _ _ eq) k)
cast {n = Z} eq (FS k) impossible
export
Uninhabited (Fin Z) where
uninhabited FZ impossible
@ -176,3 +184,99 @@ DecEq (Fin n) where
= case decEq f f' of
Yes p => Yes $ cong FS p
No p => No $ p . fsInjective
namespace Equality
||| Pointwise equality of Fins
||| It is sometimes complicated to prove equalities on type-changing
||| operations on Fins.
||| This inductive definition can be used to simplify proof. We can
||| recover proofs of equalities by using `homoPointwiseIsEqual`.
public export
data Pointwise : Fin m -> Fin n -> Type where
FZ : Pointwise FZ FZ
FS : Pointwise k l -> Pointwise (FS k) (FS l)
infix 6 ~~~
||| Convenient infix notation for the notion of pointwise equality of Fins
public export
(~~~) : Fin m -> Fin n -> Type
(~~~) = Pointwise
||| Pointwise equality is reflexive
export
reflexive : {k : Fin m} -> k ~~~ k
reflexive {k = FZ} = FZ
reflexive {k = FS k} = FS reflexive
||| Pointwise equality is symmetric
export
symmetric : k ~~~ l -> l ~~~ k
symmetric FZ = FZ
symmetric (FS prf) = FS (symmetric prf)
||| Pointwise equality is transitive
export
transitive : j ~~~ k -> k ~~~ l -> j ~~~ l
transitive FZ FZ = FZ
transitive (FS prf) (FS prg) = FS (transitive prf prg)
||| Pointwise equality is compatible with cast
export
castEq : {k : Fin m} -> (0 eq : m = n) -> cast eq k ~~~ k
castEq {k = FZ} Refl = FZ
castEq {k = FS k} Refl = FS (castEq _)
||| The actual proof used by cast is irrelevant
export
congCast : {n, q : Nat} -> {k : Fin m} -> {l : Fin p} ->
{0 eq1 : m = n} -> {0 eq2 : p = q} ->
k ~~~ l ->
cast eq1 k ~~~ cast eq2 l
congCast eq = transitive (castEq _) (transitive eq $ symmetric $ castEq _)
||| Last is congruent wrt index equality
export
congLast : {m, n : Nat} -> (0 _ : m = n) -> last {n=m} ~~~ last {n}
congLast {m = Z} {n = Z} eq = reflexive
congLast {m = S _} {n = S _} eq = FS (congLast (succInjective _ _ eq))
export
congShift : (m : Nat) -> k ~~~ l -> shift m k ~~~ shift m l
congShift Z prf = prf
congShift (S m) prf = FS (congShift m prf)
||| WeakenN is congruent wrt pointwise equality
export
congWeakenN : k ~~~ l -> weakenN n k ~~~ weakenN n l
congWeakenN FZ = FZ
congWeakenN (FS prf) = FS (congWeakenN prf)
||| Pointwise equality is propositional equality on Fins that have the same type
export
homoPointwiseIsEqual : {0 k, l : Fin m} -> k ~~~ l -> k === l
homoPointwiseIsEqual FZ = Refl
homoPointwiseIsEqual (FS prf) = cong FS (homoPointwiseIsEqual prf)
||| Pointwise equality is propositional equality modulo transport on Fins that
||| have provably equal types
export
hetPointwiseIsTransport :
{0 k : Fin m} -> {0 l : Fin n} ->
(eq : m === n) -> k ~~~ l -> k === rewrite eq in l
hetPointwiseIsTransport Refl = homoPointwiseIsEqual
export
finToNatQuotient : k ~~~ l -> finToNat k === finToNat l
finToNatQuotient FZ = Refl
finToNatQuotient (FS prf) = cong S (finToNatQuotient prf)
export
weakenNeutral : (k : Fin n) -> weaken k ~~~ k
weakenNeutral FZ = FZ
weakenNeutral (FS k) = FS (weakenNeutral k)
export
weakenNNeutral : (0 m : Nat) -> (k : Fin n) -> weakenN m k ~~~ k
weakenNNeutral m FZ = FZ
weakenNNeutral m (FS k) = FS (weakenNNeutral m k)

View File

@ -60,3 +60,8 @@ lowerMaybe (Just x) = x
export
raiseToMaybe : (Monoid a, Eq a) => a -> Maybe a
raiseToMaybe x = if x == neutral then Nothing else Just x
public export
filter : (a -> Bool) -> Maybe a -> Maybe a
filter _ Nothing = Nothing
filter f (Just x) = toMaybe (f x) x

View File

@ -1,5 +1,7 @@
module Data.Morphisms
import Data.Contravariant
public export
record Morphism a b where
constructor Mor
@ -21,6 +23,11 @@ record Kleislimorphism (f : Type -> Type) a b where
constructor Kleisli
applyKleisli : a -> f b
public export
record Op b a where
constructor MkOp
applyOp : a -> b
export
Functor (Morphism r) where
map f (Mor a) = Mor $ f . a
@ -65,6 +72,11 @@ Monad f => Monad (Kleislimorphism f a) where
k1 <- f r
applyKleisli (g k1) r
public export
Contravariant (Op b) where
contramap f (MkOp g) = MkOp (g . f)
v >$ (MkOp f) = MkOp \_ => f v
-- Applicative is a bit too strong, but there is no suitable superclass
export
(Semigroup a, Applicative f) => Semigroup (Kleislimorphism f r a) where
@ -89,3 +101,27 @@ Cast (Morphism a (f b)) (Kleislimorphism f a b) where
export
Cast (Kleislimorphism f a b) (Morphism a (f b)) where
cast (Kleisli f) = Mor f
export
Cast (Endomorphism a) (Op a a) where
cast (Endo f) = MkOp f
export
Cast (Op a a) (Endomorphism a) where
cast (MkOp f) = Endo f
export
Cast (Op (f b) a) (Kleislimorphism f a b) where
cast (MkOp f) = Kleisli f
export
Cast (Kleislimorphism f a b) (Op (f b) a) where
cast (Kleisli f) = MkOp f
export
Cast (Morphism a b) (Op b a) where
cast (Mor f) = MkOp f
export
Cast (Op b a) (Morphism a b) where
cast (MkOp f) = Mor f

View File

@ -30,16 +30,20 @@ namespace IntegerV
public export
data IntegerRec : Integer -> Type where
IntegerZ : IntegerRec 0
IntegerSucc : IntegerRec (n - 1) -> IntegerRec n
IntegerPred : IntegerRec ((-n) + 1) -> IntegerRec (-n)
-- adding the constant (-1 or 1) on the left keeps the view
-- similar to the inductive definition of natural numbers, and
-- is usually compatible with pattern matching on arguments
-- left-to-right.
IntegerSucc : IntegerRec (-1 + n) -> IntegerRec n
IntegerPred : IntegerRec (1 + (-n)) -> IntegerRec (-n)
||| Covering function for `IntegerRec`
public export
integerRec : (x : Integer) -> IntegerRec x
integerRec 0 = IntegerZ
integerRec x = if x > 0 then IntegerSucc (assert_total (integerRec (x - 1)))
integerRec x = if x > 0 then IntegerSucc (assert_total (integerRec (-1 + x)))
else believe_me (IntegerPred {n = -x}
(assert_total (believe_me (integerRec (x + 1)))))
(assert_total (believe_me (integerRec (1 + x)))))
namespace IntV
||| View for expressing a number as a multiplication + a remainder
@ -70,13 +74,17 @@ namespace IntV
public export
data IntRec : Int -> Type where
IntZ : IntRec 0
IntSucc : IntRec (n - 1) -> IntRec n
IntPred : IntRec ((-n) + 1) -> IntRec (-n)
-- adding the constant (-1 or 1) on the left keeps the view
-- similar to the inductive definition of natural numbers, and
-- is usually compatible with pattern matching on arguments
-- left-to-right.
IntSucc : IntRec (-1 + n) -> IntRec n
IntPred : IntRec (1 + (-n)) -> IntRec (-n)
||| Covering function for `IntRec`
public export
intRec : (x : Int) -> IntRec x
intRec 0 = IntZ
intRec x = if x > 0 then IntSucc (assert_total (intRec (x - 1)))
intRec x = if x > 0 then IntSucc (assert_total (intRec (-1 + x)))
else believe_me (IntPred {n = -x}
(assert_total (believe_me (intRec (x + 1)))))
(assert_total (believe_me (intRec (1 + x)))))

View File

@ -18,25 +18,6 @@ partial
foldl1 : (a -> a -> a) -> List a -> a
foldl1 f (x::xs) = foldl f x xs
-- This function runs fast when compiled but won't compute at compile time.
-- If you need to unpack strings at compile time, use Prelude.unpack.
%foreign
"scheme:string-unpack"
"javascript:lambda:(str)=>__prim_js2idris_array(Array.from(str))"
export
fastUnpack : String -> List Char
-- This works quickly because when string-concat builds the result, it allocates
-- enough room in advance so there's only one allocation, rather than lots!
--
-- Like fastUnpack, this function won't reduce at compile time.
-- If you need to concatenate strings at compile time, use Prelude.concat.
%foreign
"scheme:string-concat"
"javascript:lambda:(xs)=>''.concat(...__prim_idris2js_array(xs))"
export
fastConcat : List String -> String
-- This uses fastConcat internally so it won't compute at compile time.
export
fastUnlines : List String -> String
@ -132,6 +113,8 @@ export
unlines : List String -> String
unlines = pack . unlines' . map unpack
%transform "fastUnlines" unlines = fastUnlines
||| A view checking whether a string is empty
||| and, if not, returning its head and tail
public export

View File

@ -4,5 +4,8 @@ all:
install:
${IDRIS2} --install base.ipkg
docs:
${IDRIS2} --mkdoc base.ipkg
clean:
$(RM) -r build

View File

@ -31,15 +31,23 @@ export
usleep : HasIO io => (x : Int) -> So (x >= 0) => io ()
usleep sec = primIO (prim__usleep sec)
-- This one is going to vary for different back ends. Probably needs a
-- better convention. Will revisit...
%foreign "scheme:blodwen-args"
"node:lambda:() => __prim_js2idris_array(process.argv.slice(1))"
prim__getArgs : PrimIO (List String)
-- Get the number of arguments
%foreign "scheme:blodwen-arg-count"
"node:lambda:() => process.argv.length"
prim__getArgCount : PrimIO Int
-- Get argument number `n`
%foreign "scheme:blodwen-arg"
"node:lambda:n => process.argv[n]"
prim__getArg : Int -> PrimIO String
export
getArgs : HasIO io => io (List String)
getArgs = primIO prim__getArgs
getArgs = do
n <- primIO prim__getArgCount
if n > 0
then for [0..n-1] (\x => primIO $ prim__getArg x)
else pure []
%foreign libc "getenv"
"node:lambda: n => process.env[n]"

View File

@ -10,7 +10,7 @@ support : String -> String
support fn = "C:" ++ fn ++ ", libidris2_support"
%foreign support "idris2_fileErrno"
"node:support:fileErrno,support_system_directory"
"node:support:fileErrno,support_system_file"
prim__fileErrno : PrimIO Int
returnError : HasIO io => io (Either FileError a)

View File

@ -34,7 +34,7 @@ prim__close : FilePtr -> PrimIO ()
prim__error : FilePtr -> PrimIO Int
%foreign support "idris2_fileErrno"
"node:lambda:()=>-BigInt(process.__lasterr.errno)"
"node:support:fileErrno,support_system_file"
prim__fileErrno : PrimIO Int
%foreign support "idris2_seekLine"

View File

@ -7,6 +7,8 @@ modules = Control.App,
Control.App.Console,
Control.App.FileIO,
Control.Applicative.Const,
Control.Monad.Either,
Control.Monad.Error.Either,
Control.Monad.Error.Interface,
@ -35,6 +37,7 @@ modules = Control.App,
Data.Buffer,
Data.Colist,
Data.Colist1,
Data.Contravariant,
Data.DPair,
Data.Either,
Data.Fin,

View File

@ -3,77 +3,130 @@ module Data.Fin.Extra
import Data.Fin
import Data.Nat
import Syntax.WithProof
import Syntax.PreorderReasoning
%default total
||| Proof that an element **n** of Fin **m** , when converted to Nat is smaller than the bound **m**.
-------------------------------
--- `finToNat`'s properties ---
-------------------------------
||| A Fin's underlying natural number is smaller than the bound
export
elemSmallerThanBound : (n : Fin m) -> LT (finToNat n) m
elemSmallerThanBound FZ = LTESucc LTEZero
elemSmallerThanBound (FS x) = LTESucc (elemSmallerThanBound x)
||| Proof that application of finToNat the last element of Fin **S n** gives **n**.
||| Last's underlying natural number is the bound's predecessor
export
finToNatLastIsBound : {n : Nat} -> finToNat (Fin.last {n}) = n
finToNatLastIsBound {n=Z} = Refl
finToNatLastIsBound {n=S k} = rewrite finToNatLastIsBound {n=k} in Refl
finToNatLastIsBound {n=S k} = cong S finToNatLastIsBound
||| Proof that an element **n** of Fin **m** , when converted to Nat is smaller than the bound **m**.
||| Weaken does not modify the underlying natural number
export
finToNatWeakenNeutral : {m : Nat} -> {n : Fin m} -> finToNat (weaken n) = finToNat n
finToNatWeakenNeutral {n=FZ} = Refl
finToNatWeakenNeutral {m=S (S _)} {n=FS _} = cong S finToNatWeakenNeutral
finToNatWeakenNeutral : {n : Fin m} -> finToNat (weaken n) = finToNat n
finToNatWeakenNeutral = finToNatQuotient (weakenNeutral n)
-- ||| Proof that it's possible to strengthen a weakened element of Fin **m**.
-- export
-- strengthenWeakenNeutral : {m : Nat} -> (n : Fin m) -> strengthen (weaken n) = Right n
-- strengthenWeakenNeutral {m=S _} FZ = Refl
-- strengthenWeakenNeutral {m=S (S _)} (FS k) = rewrite strengthenWeakenNeutral k in Refl
||| WeakenN does not modify the underlying natural number
export
finToNatWeakenNNeutral : (0 m : Nat) -> (k : Fin n) ->
finToNat (weakenN m k) = finToNat k
finToNatWeakenNNeutral m k = finToNatQuotient (weakenNNeutral m k)
||| Proof that it's not possible to strengthen the last element of Fin **n**.
||| `Shift k` shifts the underlying natural number by `k`.
export
finToNatShift : (k : Nat) -> (a : Fin n) -> finToNat (shift k a) = k + finToNat a
finToNatShift Z a = Refl
finToNatShift (S k) a = cong S (finToNatShift k a)
-------------------------------------------------
--- Inversion function and related properties ---
-------------------------------------------------
||| Compute the Fin such that `k + invFin k = n - 1`
export
invFin : {n : Nat} -> Fin n -> Fin n
invFin FZ = last
invFin (FS k) = weaken (invFin k)
||| The inverse of a weakened element is the successor of its inverse
export
invFinWeakenIsFS : {n : Nat} -> (m : Fin n) -> invFin (weaken m) = FS (invFin m)
invFinWeakenIsFS FZ = Refl
invFinWeakenIsFS (FS k) = cong weaken (invFinWeakenIsFS k)
export
invFinLastIsFZ : {n : Nat} -> invFin (last {n}) = FZ
invFinLastIsFZ {n = Z} = Refl
invFinLastIsFZ {n = S n} = cong weaken (invFinLastIsFZ {n})
||| `invFin` is involutive (i.e. applied twice it is the identity)
export
invFinInvolutive : {n : Nat} -> (m : Fin n) -> invFin (invFin m) = m
invFinInvolutive FZ = invFinLastIsFZ
invFinInvolutive (FS k) = Calc $
|~ invFin (invFin (FS k))
~~ invFin (weaken (invFin k)) ...( Refl )
~~ FS (invFin (invFin k)) ...( invFinWeakenIsFS (invFin k) )
~~ FS k ...( cong FS (invFinInvolutive k) )
--------------------------------
--- Strengthening properties ---
--------------------------------
||| It's possible to strengthen a weakened element of Fin **m**.
export
strengthenWeakenIsRight : (n : Fin m) -> strengthen (weaken n) = Right n
strengthenWeakenIsRight FZ = Refl
strengthenWeakenIsRight (FS k) = rewrite strengthenWeakenIsRight k in Refl
||| It's not possible to strengthen the last element of Fin **n**.
export
strengthenLastIsLeft : {n : Nat} -> strengthen (Fin.last {n}) = Left (Fin.last {n})
strengthenLastIsLeft {n=Z} = Refl
strengthenLastIsLeft {n=S k} = rewrite strengthenLastIsLeft {n=k} in Refl
||| Enumerate elements of Fin **n** backwards.
||| It's possible to strengthen the inverse of a succesor
export
invFin : {n : Nat} -> Fin n -> Fin n
invFin FZ = last
invFin {n=S (S _)} (FS k) = weaken (invFin k)
strengthenNotLastIsRight : {n : Nat} -> (m : Fin n) -> strengthen (invFin (FS m)) = Right (invFin m)
strengthenNotLastIsRight m = strengthenWeakenIsRight (invFin m)
||| Proof that an inverse of a weakened element of Fin **n** is a successive of an inverse of an original element.
export
invWeakenIsSucc : {n : Nat} -> (m : Fin n) -> invFin (weaken m) = FS (invFin m)
invWeakenIsSucc FZ = Refl
invWeakenIsSucc {n=S (S _)} (FS k) = rewrite invWeakenIsSucc k in Refl
||| Proof that double inversion of Fin **n** gives the original.
export
doubleInvFinSame : {n : Nat} -> (m : Fin n) -> invFin (invFin m) = m
doubleInvFinSame {n=S Z} FZ = Refl
doubleInvFinSame {n=S (S k)} FZ = rewrite doubleInvFinSame {n=S k} FZ in Refl
doubleInvFinSame {n=S (S _)} (FS x) = trans (invWeakenIsSucc $ invFin x) (cong FS $ doubleInvFinSame x)
||| Proof that an inverse of the last element of Fin (S **n**) in FZ.
export
invLastIsFZ : {n : Nat} -> invFin (Fin.last {n}) = FZ
invLastIsFZ {n=Z} = Refl
invLastIsFZ {n=S k} = rewrite invLastIsFZ {n=k} in Refl
-- ||| Proof that it's possible to strengthen an inverse of a succesive element of Fin **n**.
-- export
-- strengthenNotLastIsRight : (m : Fin (S n)) -> strengthen (invFin (FS m)) = Right (invFin m)
-- strengthenNotLastIsRight m = strengthenWeakenNeutral (invFin m)
--
||| Either tightens the bound on a Fin or proves that it's the last.
export
strengthen' : {n : Nat} -> (m : Fin (S n)) -> Either (m = Fin.last) (m' : Fin n ** finToNat m = finToNat m')
strengthen' : {n : Nat} -> (m : Fin (S n)) ->
Either (m = Fin.last) (m' : Fin n ** finToNat m = finToNat m')
strengthen' {n = Z} FZ = Left Refl
strengthen' {n = S k} FZ = Right (FZ ** Refl)
strengthen' {n = S k} (FS m) = case strengthen' m of
Left eq => Left $ cong FS eq
Right (m' ** eq) => Right (FS m' ** cong S eq)
----------------------------
--- Weakening properties ---
----------------------------
export
weakenNZeroIdentity : (k : Fin n) -> weakenN 0 k ~~~ k
weakenNZeroIdentity FZ = FZ
weakenNZeroIdentity (FS k) = FS (weakenNZeroIdentity k)
export
shiftFSLinear : (m : Nat) -> (f : Fin n) -> shift m (FS f) ~~~ FS (shift m f)
shiftFSLinear Z f = reflexive
shiftFSLinear (S m) f = FS (shiftFSLinear m f)
export
shiftLastIsLast : (m : Nat) -> {n : Nat} ->
shift m (Fin.last {n}) ~~~ Fin.last {n=m+n}
shiftLastIsLast Z = reflexive
shiftLastIsLast (S m) = FS (shiftLastIsLast m)
-----------------------------------
--- Division-related properties ---
-----------------------------------
||| A view of Nat as a quotient of some number and a finite remainder.
public export
data FractionView : (n : Nat) -> (d : Nat) -> Type where
@ -98,6 +151,9 @@ divMod {ok=_} (S n) (S d) =
rewrite sym $ plusSuccRightSucc (q * S d) (finToNat r') in
cong S $ trans (sym $ cong (plus (q * S d)) eq') eq
-------------------
--- Conversions ---
-------------------
||| Total function to convert a nat to a Fin, given a proof
||| that it is less than the bound.
@ -113,4 +169,271 @@ natToFinToNat :
-> (lte : LT n m)
-> finToNat (natToFinLTE n lte) = n
natToFinToNat 0 (LTESucc lte) = Refl
natToFinToNat (S k) (LTESucc lte) = rewrite natToFinToNat k lte in Refl
natToFinToNat (S k) (LTESucc lte) = cong S (natToFinToNat k lte)
----------------------------------------
--- Result-type changing arithmetics ---
----------------------------------------
||| Addition of `Fin`s as bounded naturals.
||| The resulting type has the smallest possible bound
||| as illustated by the relations with the `last` function.
public export
(+) : {m, n : Nat} -> Fin m -> Fin (S n) -> Fin (m + n)
(+) FZ y = cast (cong S $ plusCommutative n (pred m)) (weakenN (pred m) y)
(+) (FS x) y = FS (x + y)
||| Multiplication of `Fin`s as bounded naturals.
||| The resulting type has the smallest possible bound
||| as illustated by the relations with the `last` function.
public export
(*) : {m, n : Nat} -> Fin (S m) -> Fin (S n) -> Fin (S (m * n))
(*) FZ _ = FZ
(*) {m = S _} (FS x) y = y + x * y
--- Properties ---
-- Relation between `+` and `*` and their counterparts on `Nat`
export
finToNatPlusHomo : {m, n : Nat} -> (x : Fin m) -> (y : Fin (S n)) ->
finToNat (x + y) = finToNat x + finToNat y
finToNatPlusHomo FZ _
= finToNatQuotient $ transitive
(castEq _)
(weakenNNeutral _ _)
finToNatPlusHomo (FS x) y = cong S (finToNatPlusHomo x y)
export
finToNatMultHomo : {m, n : Nat} -> (x : Fin (S m)) -> (y : Fin (S n)) ->
finToNat (x * y) = finToNat x * finToNat y
finToNatMultHomo FZ _ = Refl
finToNatMultHomo {m = S _} (FS x) y = Calc $
|~ finToNat (FS x * y)
~~ finToNat (y + x * y) ...( Refl )
~~ finToNat y + finToNat (x * y) ...( finToNatPlusHomo y (x * y) )
~~ finToNat y + finToNat x * finToNat y ...( cong (finToNat y +) (finToNatMultHomo x y) )
~~ finToNat (FS x) * finToNat y ...( Refl)
-- Relations to `Fin`'s `last`
export
plusPreservesLast : (m, n : Nat) -> Fin.last {n=m} + Fin.last {n} = Fin.last
plusPreservesLast Z n
= homoPointwiseIsEqual $ transitive
(castEq _)
(weakenNNeutral _ _)
plusPreservesLast (S m) n = cong FS (plusPreservesLast m n)
export
multPreservesLast : (m, n : Nat) -> Fin.last {n=m} * Fin.last {n} = Fin.last
multPreservesLast Z n = Refl
multPreservesLast (S m) n = Calc $
|~ last + (last * last)
~~ last + last ...( cong (last +) (multPreservesLast m n) )
~~ last ...( plusPreservesLast n (m * n) )
-- General addition properties
export
plusSuccRightSucc : {m, n : Nat} -> (left : Fin m) -> (right : Fin (S n)) ->
FS (left + right) ~~~ left + FS right
plusSuccRightSucc FZ right = FS $ congCast reflexive
plusSuccRightSucc (FS left) right = FS $ plusSuccRightSucc left right
-- Relations to `Fin`-specific `shift` and `weaken`
export
shiftAsPlus : {m, n : Nat} -> (k : Fin (S m)) ->
shift n k ~~~ last {n} + k
shiftAsPlus {n=Z} k =
symmetric $ transitive (castEq _) (weakenNNeutral _ _)
shiftAsPlus {n=S n} k = FS (shiftAsPlus k)
export
weakenNAsPlusFZ : {m, n : Nat} -> (k : Fin n) ->
weakenN m k = k + the (Fin (S m)) FZ
weakenNAsPlusFZ FZ = Refl
weakenNAsPlusFZ (FS k) = cong FS (weakenNAsPlusFZ k)
export
weakenNPlusHomo : {0 m, n : Nat} -> (k : Fin p) ->
weakenN n (weakenN m k) ~~~ weakenN (m + n) k
weakenNPlusHomo FZ = FZ
weakenNPlusHomo (FS k) = FS (weakenNPlusHomo k)
export
weakenNOfPlus :
{m, n : Nat} -> (k : Fin m) -> (l : Fin (S n)) ->
weakenN w (k + l) ~~~ weakenN w k + l
weakenNOfPlus FZ l
= transitive (congWeakenN (castEq _))
$ transitive (weakenNPlusHomo l)
$ symmetric (castEq _)
weakenNOfPlus (FS k) l = FS (weakenNOfPlus k l)
-- General addition properties (continued)
export
plusZeroLeftNeutral : (k : Fin (S n)) -> FZ + k ~~~ k
plusZeroLeftNeutral k = transitive (castEq _) (weakenNNeutral _ k)
export
congPlusLeft : {m, n, p : Nat} -> {k : Fin m} -> {l : Fin n} ->
(c : Fin (S p)) -> k ~~~ l -> k + c ~~~ l + c
congPlusLeft c FZ
= transitive (plusZeroLeftNeutral c)
(symmetric $ plusZeroLeftNeutral c)
congPlusLeft c (FS prf) = FS (congPlusLeft c prf)
export
plusZeroRightNeutral : (k : Fin m) -> k + FZ ~~~ k
plusZeroRightNeutral FZ = FZ
plusZeroRightNeutral (FS k) = FS (plusZeroRightNeutral k)
export
congPlusRight : {m, n, p : Nat} -> {k : Fin (S n)} -> {l : Fin (S p)} ->
(c : Fin m) -> k ~~~ l -> c + k ~~~ c + l
congPlusRight c FZ
= transitive (plusZeroRightNeutral c)
(symmetric $ plusZeroRightNeutral c)
congPlusRight {n = S _} {p = S _} c (FS prf)
= transitive (symmetric $ plusSuccRightSucc c _)
$ transitive (FS $ congPlusRight c prf)
(plusSuccRightSucc c _)
congPlusRight {p = Z} c (FS prf) impossible
export
plusCommutative : {m, n : Nat} -> (left : Fin (S m)) -> (right : Fin (S n)) ->
left + right ~~~ right + left
plusCommutative FZ right
= transitive (plusZeroLeftNeutral right)
(symmetric $ plusZeroRightNeutral right)
plusCommutative {m = S _} (FS left) right
= transitive (FS (plusCommutative left right))
(plusSuccRightSucc right left)
export
plusAssociative :
{m, n, p : Nat} ->
(left : Fin m) -> (centre : Fin (S n)) -> (right : Fin (S p)) ->
left + (centre + right) ~~~ (left + centre) + right
plusAssociative FZ centre right
= transitive (plusZeroLeftNeutral (centre + right))
(congPlusLeft right (symmetric $ plusZeroLeftNeutral centre))
plusAssociative (FS left) centre right = FS (plusAssociative left centre right)
-------------------------------------------------
--- Splitting operations and their properties ---
-------------------------------------------------
||| Converts `Fin`s that are used as indexes of parts to an index of a sum.
|||
||| For example, if you have a `Vect` that is a concatenation of two `Vect`s and
||| you have an index either in the first or the second of the original `Vect`s,
||| using this function you can get an index in the concatenated one.
public export
indexSum : {m : Nat} -> Either (Fin m) (Fin n) -> Fin (m + n)
indexSum (Left l) = weakenN n l
indexSum (Right r) = shift m r
||| Extracts an index of the first or the second part from the index of a sum.
|||
||| For example, if you have a `Vect` that is a concatenation of the `Vect`s and
||| you have an index of this `Vect`, you have get an index of either left or right
||| original `Vect` using this function.
public export
splitSum : {m : Nat} -> Fin (m + n) -> Either (Fin m) (Fin n)
splitSum {m=Z} k = Right k
splitSum {m=S m} FZ = Left FZ
splitSum {m=S m} (FS k) = mapFst FS $ splitSum k
||| Calculates the index of a square matrix of size `a * b` by indices of each side.
public export
indexProd : {n : Nat} -> Fin m -> Fin n -> Fin (m * n)
indexProd FZ = weakenN $ mult (pred m) n
indexProd (FS k) = shift n . indexProd k
||| Splits the index of a square matrix of size `a * b` to indices of each side.
public export
splitProd : {m, n : Nat} -> Fin (m * n) -> (Fin m, Fin n)
splitProd {m=S _} p = case splitSum p of
Left k => (FZ, k)
Right l => mapFst FS $ splitProd l
--- Properties ---
export
indexSumPreservesLast :
(m, n : Nat) -> indexSum {m} (Right $ Fin.last {n}) ~~~ Fin.last {n=m+n}
indexSumPreservesLast Z n = reflexive
indexSumPreservesLast (S m) n = FS (shiftLastIsLast m)
export
indexProdPreservesLast : (m, n : Nat) ->
indexProd (Fin.last {n=m}) (Fin.last {n}) = Fin.last
indexProdPreservesLast Z n = homoPointwiseIsEqual
$ transitive (weakenNZeroIdentity last)
(congLast (sym $ plusZeroRightNeutral n))
indexProdPreservesLast (S m) n = Calc $
|~ indexProd (last {n=S m}) (last {n})
~~ FS (shift n (indexProd last last)) ...( Refl )
~~ FS (shift n last) ...( cong (FS . shift n) (indexProdPreservesLast m n ) )
~~ last ...( homoPointwiseIsEqual prf )
where
prf : shift (S n) (Fin.last {n = n + m * S n}) ~~~ Fin.last {n = n + S (n + m * S n)}
prf = transitive (shiftLastIsLast (S n))
(congLast (plusSuccRightSucc n (n + m * S n)))
export
splitSumOfWeakenN : (k : Fin m) -> splitSum {m} {n} (weakenN n k) = Left k
splitSumOfWeakenN FZ = Refl
splitSumOfWeakenN (FS k) = cong (mapFst FS) $ splitSumOfWeakenN k
export
splitSumOfShift : {m : Nat} -> (k : Fin n) -> splitSum {m} {n} (shift m k) = Right k
splitSumOfShift {m=Z} k = Refl
splitSumOfShift {m=S m} k = cong (mapFst FS) $ splitSumOfShift k
export
splitOfIndexSumInverse : {m : Nat} -> (e : Either (Fin m) (Fin n)) -> splitSum (indexSum e) = e
splitOfIndexSumInverse (Left l) = splitSumOfWeakenN l
splitOfIndexSumInverse (Right r) = splitSumOfShift r
export
indexOfSplitSumInverse : {m, n : Nat} -> (f : Fin (m + n)) -> indexSum (splitSum {m} {n} f) = f
indexOfSplitSumInverse {m=Z} f = Refl
indexOfSplitSumInverse {m=S _} FZ = Refl
indexOfSplitSumInverse {m=S _} (FS f) with (indexOfSplitSumInverse f)
indexOfSplitSumInverse {m=S _} (FS f) | eq with (splitSum f)
indexOfSplitSumInverse {m=S _} (FS _) | eq | Left _ = cong FS eq
indexOfSplitSumInverse {m=S _} (FS _) | eq | Right _ = cong FS eq
export
splitOfIndexProdInverse : {m : Nat} -> (k : Fin m) -> (l : Fin n) ->
splitProd (indexProd k l) = (k, l)
splitOfIndexProdInverse FZ l
= rewrite splitSumOfWeakenN {n = mult (pred m) n} l in Refl
splitOfIndexProdInverse (FS k) l
= rewrite splitSumOfShift {m=n} $ indexProd k l in
cong (mapFst FS) $ splitOfIndexProdInverse k l
export
indexOfSplitProdInverse : {m, n : Nat} -> (f : Fin (m * n)) ->
uncurry (indexProd {m} {n}) (splitProd {m} {n} f) = f
indexOfSplitProdInverse {m = S _} f with (@@ splitSum f)
indexOfSplitProdInverse {m = S _} f | (Left l ** eq) = rewrite eq in Calc $
|~ indexSum (Left l)
~~ indexSum (splitSum f) ...( cong indexSum (sym eq) )
~~ f ...( indexOfSplitSumInverse f )
indexOfSplitProdInverse f | (Right r ** eq) with (@@ splitProd r)
indexOfSplitProdInverse f | (Right r ** eq) | ((p, q) ** eq2)
= rewrite eq in rewrite eq2 in Calc $
|~ indexProd (FS p) q
~~ shift n (indexProd p q) ...( Refl )
~~ shift n (uncurry indexProd (splitProd r)) ...( cong (shift n . uncurry indexProd) (sym eq2) )
~~ shift n r ...( cong (shift n) (indexOfSplitProdInverse r) )
~~ indexSum (splitSum f) ...( sym (cong indexSum eq) )
~~ f ...( indexOfSplitSumInverse f )

View File

@ -31,6 +31,22 @@ public export
bindLazy : (a -> LazyList b) -> LazyList a -> LazyList b
bindLazy f = foldrLazy ((++) . f) []
public export
choice : Alternative f => LazyList (f a) -> f a
choice = foldrLazy (<|>) empty
public export
choiceMap : Alternative f => (a -> f b) -> LazyList a -> f b
choiceMap g = foldrLazy ((<|>) . g) empty
public export
any : (a -> Bool) -> LazyList a -> Bool
any p = foldrLazy ((||) . p) False
public export
all : (a -> Bool) -> LazyList a -> Bool
all p = foldrLazy ((&&) . p) True
--- Interface implementations ---
public export
@ -44,7 +60,7 @@ Ord a => Ord (LazyList a) where
compare [] [] = EQ
compare [] (x :: xs) = LT
compare (x :: xs) [] = GT
compare (x :: xs) (y ::ys)
compare (x :: xs) (y :: ys)
= case compare x y of
EQ => compare xs ys
c => c
@ -77,6 +93,8 @@ Foldable LazyList where
foldl op acc [] = acc
foldl op acc (x :: xs) = foldl op (acc `op` x) xs
foldlM fm init xs = foldrLazy (\x, k, z => fm z x >>= k) pure xs init
null [] = True
null (_::_) = False
@ -107,10 +125,31 @@ traverse : Applicative f => (a -> f b) -> LazyList a -> f (List b)
traverse g [] = pure []
traverse g (x :: xs) = [| g x :: traverse g xs |]
public export %inline
for : Applicative f => LazyList a -> (a -> f b) -> f (List b)
for = flip traverse
public export
sequence : Applicative f => LazyList (f a) -> f (List a)
sequence = traverse id
public export
Zippable LazyList where
zipWith _ [] _ = []
zipWith _ _ [] = []
zipWith f (x::xs) (y::ys) = f x y :: zipWith f xs ys
zipWith3 _ [] _ _ = []
zipWith3 _ _ [] _ = []
zipWith3 _ _ _ [] = []
zipWith3 f (x::xs) (y::ys) (z::zs) = f x y z :: zipWith3 f xs ys zs
unzip xs = (fst <$> xs, snd <$> xs)
unzipWith = unzip .: map
unzip3 xs = (fst <$> xs, fst . snd <$> xs, snd . snd <$> xs)
unzipWith3 = unzip3 .: map
--- Lists creation ---
public export
@ -149,7 +188,7 @@ head' : LazyList a -> Maybe a
head' [] = Nothing
head' (x::_) = Just x
export
public export
tail' : LazyList a -> Maybe (LazyList a)
tail' [] = Nothing
tail' (_::xs) = Just xs
@ -209,3 +248,26 @@ namespace Colist1
public export
take : Fuel -> Colist1 a -> LazyList a
take fuel as = take fuel (forget as)
--- Functions for extending lists ---
public export
mergeReplicate : a -> LazyList a -> LazyList a
mergeReplicate sep [] = []
mergeReplicate sep (y::ys) = sep :: y :: mergeReplicate sep ys
public export
intersperse : a -> LazyList a -> LazyList a
intersperse sep [] = []
intersperse sep (x::xs) = x :: mergeReplicate sep xs
public export
intercalate : (sep : LazyList a) -> (xss : LazyList (LazyList a)) -> LazyList a
intercalate sep xss = choice $ intersperse sep xss
--- Functions converting lazy lists to something ---
public export
toColist : LazyList a -> Colist a
toColist [] = []
toColist (x::xs) = x :: toColist xs

View File

@ -103,3 +103,21 @@ indent n x = replicate n ' ' ++ x
public export
indentLines : (n : Nat) -> String -> String
indentLines n str = unlines $ map (indent n) $ forget $ lines str
||| Return a string of the given character repeated
||| `n` times.
export
fastReplicate : (n : Nat) -> Char -> String
fastReplicate n c = fastPack $ replicate n c
||| Left-justify a string to the given length, using the
||| specified fill character on the right.
export
justifyLeft : Nat -> Char -> String -> String
justifyLeft n c s = s ++ fastReplicate (n `minus` length s) c
||| Right-justify a string to the given length, using the
||| specified fill character on the left.
export
justifyRight : Nat -> Char -> String -> String
justifyRight n c s = fastReplicate (n `minus` length s) c ++ s

View File

@ -56,7 +56,8 @@ showChar c
'\\' => "\\\\"
'"' => "\\\""
c => if isControl c || c >= '\127'
then "\\u" ++ b16ToHexString (cast $ ord c)
then let hex = b16ToHexString (cast $ ord c)
in "\\u" ++ justifyRight 4 '0' hex
else singleton c
private

View File

@ -1,5 +1,7 @@
module Language.JSON.String.Tokens
import Data.List
import Data.String
import Data.String.Extra
import Text.Token
@ -48,7 +50,15 @@ simpleEscapeValue x
private
unicodeEscapeValue : String -> Char
unicodeEscapeValue x = chr $ cast ("0x" ++ drop 2 x)
unicodeEscapeValue x = fromHex (drop 2 $ fastUnpack x) 0
where hexVal : Char -> Int
hexVal c = if c >= 'A'
then ord c - ord 'A' + 10
else ord c - ord '0'
fromHex : List Char -> Int -> Char
fromHex [] acc = chr acc
fromHex (h :: t) acc = fromHex t (hexVal h + 16 * acc)
public export
TokenKind JSONStringTokenKind where

View File

@ -4,5 +4,8 @@ all:
install:
${IDRIS2} --install contrib.ipkg
docs:
${IDRIS2} --mkdoc contrib.ipkg
clean:
$(RM) -r build

View File

@ -176,12 +176,18 @@ longOpt ls rs descs =
in case (ads,unpack arg,rs) of
(_ :: _ :: _ , _ , r ) => (errAmbig options os, r)
([NoArg a ], [] , r ) => (Opt a, r)
([NoArg a ], '='::_ , r ) => (errNoArg os,r)
([NoArg a ], c :: _ , r ) => (errNoArg os,r)
-- ^ this is known (but not proven) to be '='
([ReqArg _ d], [] , [] ) => (errReq d os,[])
([ReqArg f _], [] , (r::rest)) => (Opt $ f r,rest)
([ReqArg f _], '='::xs, r ) => (Opt $ f (pack xs),r)
([ReqArg f _], c :: xs, r ) => (Opt $ f (pack xs),r)
-- ^ this is known (but not proven) to be '='
([OptArg f _], [] , r ) => (Opt $ f Nothing,r)
([OptArg f _], '='::xs, r ) => (Opt . f . Just $ pack xs,r)
([OptArg f _], c :: xs, r ) => (Opt . f . Just $ pack xs,r)
-- ^ this is known (but not proven) to be '='
([] , _ , r ) => (UnreqOpt $ "--" ++ ls,r)
shortOpt : Char -> String -> OptFun a

View File

@ -0,0 +1,201 @@
module System.Directory.Tree
import Data.DPair
import Data.List
import Data.Nat
import Data.Strings
import System.Directory
import System.Path
%default total
------------------------------------------------------------------------------
-- Filenames
||| A `Filename root` is anchored in `root`.
||| We use a `data` type so that Idris can easily infer `root` when passing
||| a `FileName` around. We do not use a `record` because we do not want to
||| allow users to manufacture their own `FileName`.
||| To get an absolute path, we need to append said filename to the root.
export
data FileName : Path -> Type where
MkFileName : String -> FileName root
||| Project the string out of a `FileName`.
export
fileName : FileName root -> String
fileName (MkFileName str) = str
namespace FileName
export
toRelative : FileName root -> FileName (parse "")
toRelative (MkFileName x) = MkFileName x
||| Convert a filename anchored in `root` to a filepath by appending the name
||| to the root path.
export
toFilePath : {root : Path} -> FileName root -> Path
toFilePath file = root /> fileName file
export
directoryExists : {root : Path} -> FileName root -> IO Bool
directoryExists fp = do
Right dir <- openDir (show $ toFilePath fp)
| Left _ => pure False
closeDir dir
pure True
------------------------------------------------------------------------------
-- Directory trees
||| A `Tree root` is the representation of a directory tree anchored in `root`.
||| Each directory contains a list of files and a list of subtrees waiting to be
||| explored. The fact these subtrees are IO-bound means the subtrees will be
||| lazily constructed on demand.
public export
SubTree : Path -> Type
public export
record Tree (root : Path) where
constructor MkTree
files : List (FileName root)
subTrees : List (SubTree root)
SubTree root = (dir : FileName root ** IO (Tree (root /> fileName dir)))
||| An empty tree contains no files and has no sub-directories.
export
emptyTree : Tree root
emptyTree = MkTree [] []
namespace Tree
||| No run time information is changed,
||| so we assert the identity.
export
toRelative : Tree root -> Tree (parse "")
toRelative x = believe_me x
||| Filter out files and directories that do not satisfy a given predicate.
export
filter : (filePred, dirPred : {root : _} -> FileName root -> Bool) ->
{root : _} -> Tree root -> Tree root
filter filePred dirPred (MkTree files dirs) = MkTree files' dirs' where
files' : List (FileName root)
files' = filter filePred files
dirs' : List (SubTree root)
dirs' = flip mapMaybe dirs $ \ (dname ** iot) => do
guard (dirPred dname)
pure (dname ** map (assert_total (filter filePred dirPred)) iot)
||| Sort the lists of files and directories using the given comparison functions
export
sortBy : (fileCmp, dirCmp : {root : _} -> FileName root -> FileName root -> Ordering) ->
{root : _} -> Tree root -> Tree root
sortBy fileCmp dirCmp (MkTree files dirs) = MkTree files' dirs' where
files' : List (FileName root)
files' = sortBy fileCmp files
dirs' : List (SubTree root)
dirs' = sortBy (\ d1, d2 => dirCmp (fst d1) (fst d2))
$ flip map dirs $ \ (dname ** iot) =>
(dname ** map (assert_total (sortBy fileCmp dirCmp)) iot)
||| Sort the list of files and directories alphabetically
export
sort : {root : _} -> Tree root -> Tree root
sort = sortBy cmp cmp where
cmp : {root : _} -> FileName root -> FileName root -> Ordering
cmp a b = compare (fileName a) (fileName b)
||| Exploring a filesystem from a given root to produce a tree
export
explore : (root : Path) -> IO (Tree root)
go : {root : Path} -> Directory -> Tree root -> IO (Tree root)
explore root = do
Right dir <- openDir (show root)
| Left err => pure emptyTree
assert_total (go dir emptyTree)
go dir acc = case !(dirEntry dir) of
-- If there is no next entry then we are done and can return the accumulator.
Left err => acc <$ closeDir dir
-- Otherwise we have an entry and need to categorise it
Right entry => do
-- ignore aliases for current and parent directories
let False = elem entry [".", ".."]
| _ => assert_total (go dir acc)
-- if the entry is a directory, add it to the (lazily explored)
-- list of subdirectories
let entry : FileName root = MkFileName entry
let acc = if !(directoryExists entry)
then { subTrees $= ((entry ** explore _) ::) } acc
else { files $= (entry ::) } acc
assert_total (go dir acc)
||| Depth first traversal of all of the files in a tree
export
covering
depthFirst : ({root : Path} -> FileName root -> Lazy (IO a) -> IO a) ->
{root : Path} -> Tree root -> IO a -> IO a
depthFirst check t k =
let next = foldr (\ (dir ** iot), def => depthFirst check !iot def) k t.subTrees in
foldr (\ fn, def => check fn def) next t.files
||| Finding a file in a tree (depth first search)
export
covering
findFile : {root : Path} -> String -> Tree root -> IO (Maybe Path)
findFile needle t = depthFirst check t (pure Nothing) where
check : {root : Path} -> FileName root ->
Lazy (IO (Maybe Path)) -> IO (Maybe Path)
check fn next = if fileName fn == needle
then pure (Just (toFilePath fn))
else next
||| Display a tree by printing it procedurally. Note that because directory
||| trees contain suspended computations corresponding to their subtrees this
||| has to be an `IO` function. We make it return Unit rather than a String
||| because we do not want to assume that the tree is finite.
export
covering
print : Tree root -> IO ()
print t = go [([], ".", Evidence root (pure t))] where
-- This implementation is unadulterated black magic.
-- Do NOT touch it if nothing is broken.
padding : Bool -> List Bool -> String
padding isDir = fastConcat . go [] where
go : List String -> List Bool -> List String
go acc [] = acc
go acc (b :: bs) = go (hd :: acc) bs where
hd : String
hd = if isDir && isNil acc
then if b then "" else ""
else if b then "" else " "
prefixes : Nat -> List Bool
prefixes n = snoc (replicate (pred n) True) False
covering
go : List (List Bool, String, Exists (IO . Tree)) -> IO ()
go [] = pure ()
go ((bs, fn, Evidence _ iot) :: iots) = do
t <- iot
putStrLn (padding True bs ++ fn)
let pad = padding False bs
let pads = prefixes (length t.files + length t.subTrees)
for_ (zip pads t.files) $ \ (b, fp) =>
putStrLn (pad ++ (if b then "" else "") ++ fileName fp)
let bss = map (:: bs) (prefixes (length t.subTrees))
go (zipWith (\ bs, (dir ** iot) => (bs, fileName dir, Evidence _ iot)) bss t.subTrees)
go iots

View File

@ -13,7 +13,7 @@ import Text.Quantity
import System.Info
infixr 5 </>
infixr 5 </>, />
infixr 7 <.>
@ -344,6 +344,7 @@ setFileName' name path =
else
append' path (parse name)
export
splitFileName : String -> (String, String)
splitFileName name =
case break (== '.') $ reverse $ unpack name of
@ -373,6 +374,23 @@ export
isRelative : String -> Bool
isRelative = not . isAbsolute
||| Appends the right path to the left path.
|||
||| If the path on the right is absolute, it replaces the left path.
|||
||| On Windows:
|||
||| - If the right path has a root but no volume (e.g., `\windows`), it replaces
||| everything except for the volume (if any) of left.
||| - If the right path has a volume but no root, it replaces left.
|||
||| ```idris example
||| parse "/usr" /> "local/etc" == "/usr/local/etc"
||| ```
export
(/>) : (left : Path) -> (right : String) -> Path
(/>) left right = append' left (parse right)
||| Appends the right path to the left path.
|||
||| If the path on the right is absolute, it replaces the left path.
@ -388,7 +406,7 @@ isRelative = not . isAbsolute
||| ```
export
(</>) : (left : String) -> (right : String) -> String
(</>) left right = show $ append' (parse left) (parse right)
(</>) left right = show $ parse left /> right
||| Joins path components into one.
|||
@ -397,7 +415,7 @@ export
||| ```
export
joinPath : List String -> String
joinPath xs = foldl (</>) "" xs
joinPath xs = show $ foldl (/>) (parse "") xs
||| Splits path into components.
|||
@ -505,7 +523,8 @@ fileStem path = pure $ fst $ splitFileName !(fileName path)
||| - Otherwise, the portion of the file name after the last ".".
export
extension : String -> Maybe String
extension path = pure $ snd $ splitFileName !(fileName path)
extension path = fileName path >>=
filter (/= "") . Just . snd . splitFileName
||| Updates the file name in the path.
|||

View File

@ -0,0 +1,36 @@
module Text.PrettyPrint.Prettyprinter.Render.HTML
import Data.List
import Data.Strings
export
htmlEscape : String -> String
htmlEscape s = fastAppend $ reverse $ go [] s
where
isSafe : Char -> Bool
isSafe '"' = False
isSafe '<' = False
isSafe '>' = False
isSafe '&' = False
isSafe '\'' = False
isSafe '\t' = True
isSafe '\n' = True
isSafe '\r' = True
isSafe c = (c >= ' ' && c <= '~')
htmlQuote : Char -> String
htmlQuote '"' = "&quot;"
htmlQuote '<' = "&lt;"
htmlQuote '>' = "&gt;"
htmlQuote '&' = "&amp;"
htmlQuote '\'' = "&apos;"
htmlQuote c = "&#" ++ (show $ ord c) ++ ";"
go : List String -> String -> List String
go acc "" = acc
go acc s =
case span isSafe s of
(safe, "") => safe::acc
(safe, rest) => let c = assert_total (strIndex rest 0)
escaped = htmlQuote c in
go (escaped::safe::acc) (assert_total $ strTail rest)

View File

@ -87,7 +87,7 @@ fromStream sdoc = case sdocToTreeParser sdoc of
flatten (STConcat [x, STEmpty]) = flatten x
flatten (STConcat [x, STConcat xs]) = case flatten (STConcat xs) of
(STConcat xs') => STConcat (x :: xs')
y => y
y => STConcat [x, y]
flatten x = x
internalError : SimpleDocTree ann

View File

@ -69,6 +69,7 @@ modules = Control.ANSI,
Data.Nat.Ack,
Data.Nat.Division,
Data.Nat.Equational,
Data.Nat.Exponentiation,
Data.Nat.Fact,
Data.Nat.Factor,
Data.Nat.Fib,
@ -76,15 +77,23 @@ modules = Control.ANSI,
Data.Nat.Order.Properties,
Data.Nat.Properties,
Data.Num.Implementations,
Data.OpenUnion,
Data.Order,
Data.Path,
Data.Recursion.Free,
Data.Rel.Complement,
Data.SortedMap,
Data.SortedSet,
Data.Stream.Extra,
Data.String.Extra,
Data.String.Interpolation,
Data.String.Iterator,
@ -136,6 +145,7 @@ modules = Control.ANSI,
Syntax.PreorderReasoning.Generic,
System.Console.GetOpt,
System.Directory.Tree,
System.Future,
System.Random,
System.Path,
@ -151,5 +161,6 @@ modules = Control.ANSI,
Text.PrettyPrint.Prettyprinter.Symbols,
Text.PrettyPrint.Prettyprinter.Util,
Text.PrettyPrint.Prettyprinter.SimpleDocTree,
Text.PrettyPrint.Prettyprinter.Render.HTML,
Text.PrettyPrint.Prettyprinter.Render.String,
Text.PrettyPrint.Prettyprinter.Render.Terminal

View File

@ -4,5 +4,8 @@ all:
install:
${IDRIS2} --install network.ipkg
docs:
${IDRIS2} --mkdoc network.ipkg
clean:
$(RM) -r build

View File

@ -40,6 +40,10 @@ prim__idrnet_sockaddr_family : (sockaddr : AnyPtr) -> PrimIO Int
export
prim__idrnet_sockaddr_ipv4 : (sockaddr : AnyPtr) -> PrimIO String
%foreign "C:idrnet_sockaddr_unix,libidris2_support"
export
prim__idrnet_sockaddr_unix : (sockaddr : AnyPtr) -> PrimIO String
%foreign "C:idrnet_sockaddr_ipv4_port,libidris2_support"
export
prim__idrnet_sockaddr_ipv4_port : (sockaddr : AnyPtr) -> PrimIO Int

View File

@ -70,6 +70,7 @@ getSockAddr (SAPtr ptr) = do
pure $ parseIPv4 ipv4_addr
Just AF_INET6 => pure IPv6Addr
Just AF_UNIX => map Hostname $ primIO (prim__idrnet_sockaddr_unix ptr)
Just AF_UNSPEC => pure InvalidAddress)
export

View File

@ -4,5 +4,8 @@ all:
install:
${IDRIS2} --install prelude.ipkg
docs:
${IDRIS2} --mkdoc prelude.ipkg
clean:
$(RM) -r build

View File

@ -18,6 +18,10 @@ interface Cast from to where
||| @ orig The original type
cast : (orig : from) -> to
export
Cast a a where
cast = id
-- To String
export

View File

@ -81,6 +81,14 @@ public export
(<$>) : Functor f => (func : a -> b) -> f a -> f b
(<$>) func x = map func x
||| Flipped version of `<$>`, an infix alias for `map`, applying a function across
||| everything of type 'a' in a parameterised type.
||| @ f the parameterised type
||| @ func the function to apply
public export
(<&>) : Functor f => f a -> (func : a -> b) -> f b
(<&>) x func = map func x
||| Run something for effects, replacing the return value with a given parameter.
public export
(<$) : Functor f => b -> f a -> f b
@ -243,11 +251,11 @@ interface Foldable t where
null : t elem -> Lazy Bool
null = foldr {acc = Lazy Bool} (\ _,_ => False) True
||| Similar to `foldl`, but uses a function wrapping its result in a `Monad`.
||| Consequently, the final value is wrapped in the same `Monad`.
public export
foldlM : (Foldable t, Monad m) => (funcM: a -> b -> m a) -> (init: a) -> (input: t b) -> m a
foldlM fm a0 = foldl (\ma,b => ma >>= flip fm b) (pure a0)
||| Similar to `foldl`, but uses a function wrapping its result in a `Monad`.
||| Consequently, the final value is wrapped in the same `Monad`.
public export
foldlM : Monad m => (funcM : acc -> elem -> m acc) -> (init : acc) -> (input : t elem) -> m acc
foldlM fm a0 = foldl (\ma, b => ma >>= flip fm b) (pure a0)
||| Maps each element to a value and combine them
public export

View File

@ -13,7 +13,7 @@ infixr 4 ||
infixr 7 ::, ++
-- Functor/Applicative/Monad/Algebra operators
infixl 1 >>=, =<<, >>, >=>, <=<
infixl 1 >>=, =<<, >>, >=>, <=<, <&>
infixr 2 <|>
infixl 3 <*>, *>, <*
infixr 4 <$>, $>, <$

View File

@ -412,6 +412,19 @@ Traversable List where
traverse f [] = pure []
traverse f (x::xs) = pure (::) <*> (f x) <*> (traverse f xs)
-- This works quickly because when string-concat builds the result, it allocates
-- enough room in advance so there's only one allocation, rather than lots!
--
-- Like fastUnpack, this function won't reduce at compile time.
-- If you need to concatenate strings at compile time, use Prelude.concat.
%foreign
"scheme:string-concat"
"javascript:lambda:(xs)=>''.concat(...__prim_idris2js_array(xs))"
export
fastConcat : List String -> String
%transform "fastConcat" concat {t = List} {a = String} = fastConcat
||| Check if something is a member of a list using the default Boolean equality.
public export
elem : Eq a => a -> List a -> Bool
@ -537,6 +550,9 @@ pack (x :: xs) = strCons x (pack xs)
export
fastPack : List Char -> String
-- always use 'fastPack' at run time
%transform "fastPack" pack = fastPack
||| Turns a string into a list of characters.
|||
||| ```idris example
@ -552,6 +568,17 @@ unpack str = unpack' (prim__cast_IntegerInt (natToInteger (length str)) - 1) str
then acc
else assert_total $ unpack' (pos - 1) str (assert_total (prim__strIndex str pos)::acc)
-- This function runs fast when compiled but won't compute at compile time.
-- If you need to unpack strings at compile time, use Prelude.unpack.
%foreign
"scheme:string-unpack"
"javascript:lambda:(str)=>__prim_js2idris_array(Array.from(str))"
export
fastUnpack : String -> List Char
-- always use 'fastPack' at run time
%transform "fastUnpack" unpack = fastUnpack
public export
Semigroup String where
(<+>) = (++)

View File

@ -264,10 +264,11 @@ Show Requirement where
export
checkRequirement : Requirement -> IO (Maybe String)
checkRequirement req
= do let (envvar, paths) = requirement req
Just exec <- getEnv envvar | Nothing => pathLookup paths
pure (Just exec)
= if platformSupport req
then do let (envvar, paths) = requirement req
Just exec <- getEnv envvar | Nothing => pathLookup paths
pure (Just exec)
else pure Nothing
where
requirement : Requirement -> (String, List String)
requirement C = ("CC", ["cc"])
@ -275,6 +276,10 @@ checkRequirement req
requirement Node = ("NODE", ["node"])
requirement Racket = ("RACKET", ["racket"])
requirement Gambit = ("GAMBIT", ["gsc"])
platformSupport : Requirement -> Bool
platformSupport C = not isWindows
platformSupport Racket = not isWindows
platformSupport _ = True
export
findCG : IO (Maybe String)

View File

@ -5,6 +5,9 @@
, fetchFromGitHub
, makeWrapper
, idris2-version
, racket
, gambit
, nodejs
}:
# Uses scheme to bootstrap the build of idris2
@ -28,7 +31,8 @@ stdenv.mkDerivation rec {
# The name of the main executable of pkgs.chez is `scheme`
buildFlags = [ "bootstrap" "SCHEME=scheme" ];
checkTarget = "test";
checkInputs = [ gambit nodejs ]; # racket ];
checkFlags = [ "INTERACTIVE=" ];
# TODO: Move this into its own derivation, such that this can be changed
# without having to recompile idris2 every time.

View File

@ -42,3 +42,4 @@ let
in
withTests testsTemplate templateBuildDefault
// withTests testsTemplateWithDeps templateBuildWithDeps
// { idris2Tests = idris.defaultPackage.${system}.overrideAttrs (a: { doCheck = true; }); }

265
src/Compiler/CaseOpts.idr Normal file
View File

@ -0,0 +1,265 @@
module Compiler.CaseOpts
-- Case block related transformations
import Compiler.CompileExpr
import Core.CompileExpr
import Core.Context
import Core.Context.Log
import Core.FC
import Core.TT
import Data.List
import Data.Vect
%default covering
{-
Lifting out lambdas:
case t of
C1 => \x1 => e1
...
Cn => \xn = en
where every branch begins with a lambda, can become:
\x => case t of
C1 => e1[x/x1]
,,,
Cn => en[x/xn]
-}
shiftUnder : {args : _} ->
{idx : _} ->
(0 p : IsVar n idx (x :: args ++ vars)) ->
NVar n (args ++ x :: vars)
shiftUnder First = weakenNVar (mkSizeOf args) (MkNVar First)
shiftUnder (Later p) = insertNVar (mkSizeOf args) (MkNVar p)
shiftVar : {outer, args : _} ->
{idx : _} ->
(0 p : IsVar n idx (outer ++ (x :: args ++ vars))) ->
NVar n (outer ++ (args ++ x :: vars))
shiftVar {outer = []} p = shiftUnder p
shiftVar {outer = (n::xs)} First = MkNVar First
shiftVar {outer = (y::xs)} (Later p)
= case shiftVar p of
MkNVar p' => MkNVar (Later p')
mutual
shiftBinder : {outer, args : _} ->
(new : Name) ->
CExp (outer ++ old :: (args ++ vars)) ->
CExp (outer ++ (args ++ new :: vars))
shiftBinder new (CLocal fc p)
= case shiftVar p of
MkNVar p' => CLocal fc (renameVar p')
where
renameVar : IsVar x i (outer ++ (args ++ (old :: rest))) ->
IsVar x i (outer ++ (args ++ (new :: rest)))
renameVar = believe_me -- it's the same index, so just the identity at run time
shiftBinder new (CRef fc n) = CRef fc n
shiftBinder {outer} new (CLam fc n sc)
= CLam fc n $ shiftBinder {outer = n :: outer} new sc
shiftBinder new (CLet fc n inlineOK val sc)
= CLet fc n inlineOK (shiftBinder new val)
$ shiftBinder {outer = n :: outer} new sc
shiftBinder new (CApp fc f args)
= CApp fc (shiftBinder new f) $ map (shiftBinder new) args
shiftBinder new (CCon fc c tag args)
= CCon fc c tag $ map (shiftBinder new) args
shiftBinder new (COp fc op args) = COp fc op $ map (shiftBinder new) args
shiftBinder new (CExtPrim fc p args)
= CExtPrim fc p $ map (shiftBinder new) args
shiftBinder new (CForce fc r arg) = CForce fc r $ shiftBinder new arg
shiftBinder new (CDelay fc r arg) = CDelay fc r $ shiftBinder new arg
shiftBinder new (CConCase fc sc alts def)
= CConCase fc (shiftBinder new sc)
(map (shiftBinderConAlt new) alts)
(map (shiftBinder new) def)
shiftBinder new (CConstCase fc sc alts def)
= CConstCase fc (shiftBinder new sc)
(map (shiftBinderConstAlt new) alts)
(map (shiftBinder new) def)
shiftBinder new (CPrimVal fc c) = CPrimVal fc c
shiftBinder new (CErased fc) = CErased fc
shiftBinder new (CCrash fc msg) = CCrash fc msg
shiftBinderConAlt : {outer, args : _} ->
(new : Name) ->
CConAlt (outer ++ (x :: args ++ vars)) ->
CConAlt (outer ++ (args ++ new :: vars))
shiftBinderConAlt new (MkConAlt n t args' sc)
= let sc' : CExp ((args' ++ outer) ++ (x :: args ++ vars))
= rewrite sym (appendAssociative args' outer (x :: args ++ vars)) in sc in
MkConAlt n t args' $
rewrite (appendAssociative args' outer (args ++ new :: vars))
in shiftBinder new {outer = args' ++ outer} sc'
shiftBinderConstAlt : {outer, args : _} ->
(new : Name) ->
CConstAlt (outer ++ (x :: args ++ vars)) ->
CConstAlt (outer ++ (args ++ new :: vars))
shiftBinderConstAlt new (MkConstAlt c sc) = MkConstAlt c $ shiftBinder new sc
-- If there's a lambda inside a case, move the variable so that it's bound
-- outside the case block so that we can bind it just once outside the block
liftOutLambda : {args : _} ->
(new : Name) ->
CExp (old :: args ++ vars) ->
CExp (args ++ new :: vars)
liftOutLambda = shiftBinder {outer = []}
-- If all the alternatives start with a lambda, we can have a single lambda
-- binding outside
tryLiftOut : (new : Name) ->
List (CConAlt vars) ->
Maybe (List (CConAlt (new :: vars)))
tryLiftOut new [] = Just []
tryLiftOut new (MkConAlt n t args (CLam fc x sc) :: as)
= do as' <- tryLiftOut new as
let sc' = liftOutLambda new sc
pure (MkConAlt n t args sc' :: as')
tryLiftOut _ _ = Nothing
tryLiftOutConst : (new : Name) ->
List (CConstAlt vars) ->
Maybe (List (CConstAlt (new :: vars)))
tryLiftOutConst new [] = Just []
tryLiftOutConst new (MkConstAlt c (CLam fc x sc) :: as)
= do as' <- tryLiftOutConst new as
let sc' = liftOutLambda {args = []} new sc
pure (MkConstAlt c sc' :: as')
tryLiftOutConst _ _ = Nothing
tryLiftDef : (new : Name) ->
Maybe (CExp vars) ->
Maybe (Maybe (CExp (new :: vars)))
tryLiftDef new Nothing = Just Nothing
tryLiftDef new (Just (CLam fc x sc))
= let sc' = liftOutLambda {args = []} new sc in
pure (Just sc')
tryLiftDef _ _ = Nothing
allLams : List (CConAlt vars) -> Bool
allLams [] = True
allLams (MkConAlt n t args (CLam _ _ _) :: as)
= allLams as
allLams _ = False
allLamsConst : List (CConstAlt vars) -> Bool
allLamsConst [] = True
allLamsConst (MkConstAlt c (CLam _ _ _) :: as)
= allLamsConst as
allLamsConst _ = False
-- label for next name for a lambda. These probably don't need really to be
-- unique, since we've proved things about the de Bruijn index, but it's easier
-- to see what's going on if they are.
data NextName : Type where
getName : {auto n : Ref NextName Int} ->
Core Name
getName
= do n <- get NextName
put NextName (n + 1)
pure (MN "clam" n)
-- The transformation itself
mutual
caseLam : {auto n : Ref NextName Int} ->
CExp vars -> Core (CExp vars)
-- Interesting cases first: look for case blocks where every branch is a
-- lambda
caseLam (CConCase fc sc alts def)
= if allLams alts && defLam def
then do var <- getName
-- These will work if 'allLams' and 'defLam' are consistent.
-- We only do that boolean check because it saves us doing
-- unnecessary work (say, if the last one we try fails)
let Just newAlts = tryLiftOut var alts
| Nothing => throw (InternalError "Can't happen caseLam 1")
let Just newDef = tryLiftDef var def
| Nothing => throw (InternalError "Can't happen caseLam 2")
newAlts' <- traverse caseLamConAlt newAlts
newDef' <- traverseOpt caseLam newDef
-- Q: Should we go around again?
pure (CLam fc var (CConCase fc (weaken sc) newAlts' newDef'))
else do sc' <- caseLam sc
alts' <- traverse caseLamConAlt alts
def' <- traverseOpt caseLam def
pure (CConCase fc sc' alts' def')
where
defLam : Maybe (CExp vars) -> Bool
defLam Nothing = True
defLam (Just (CLam _ _ _)) = True
defLam _ = False
-- Next case is pretty much as above. There's a boring amount of repetition
-- here because ConstCase is just a little bit different.
caseLam (CConstCase fc sc alts def)
= if allLamsConst alts && defLam def
then do var <- getName
-- These will work if 'allLams' and 'defLam' are consistent.
-- We only do that boolean check because it saves us doing
-- unnecessary work (say, if the last one we try fails)
let Just newAlts = tryLiftOutConst var alts
| Nothing => throw (InternalError "Can't happen caseLam 1")
let Just newDef = tryLiftDef var def
| Nothing => throw (InternalError "Can't happen caseLam 2")
newAlts' <- traverse caseLamConstAlt newAlts
newDef' <- traverseOpt caseLam newDef
pure (CLam fc var (CConstCase fc (weaken sc) newAlts' newDef'))
else do sc' <- caseLam sc
alts' <- traverse caseLamConstAlt alts
def' <- traverseOpt caseLam def
pure (CConstCase fc sc' alts' def')
where
defLam : Maybe (CExp vars) -> Bool
defLam Nothing = True
defLam (Just (CLam _ _ _)) = True
defLam _ = False
-- Structural recursive cases
caseLam (CLam fc x sc)
= CLam fc x <$> caseLam sc
caseLam (CLet fc x inl val sc)
= CLet fc x inl <$> caseLam val <*> caseLam sc
caseLam (CApp fc f args)
= CApp fc <$> caseLam f <*> traverse caseLam args
caseLam (CCon fc n t args)
= CCon fc n t <$> traverse caseLam args
caseLam (COp fc op args)
= COp fc op <$> traverseVect caseLam args
caseLam (CExtPrim fc p args)
= CExtPrim fc p <$> traverse caseLam args
caseLam (CForce fc r x)
= CForce fc r <$> caseLam x
caseLam (CDelay fc r x)
= CDelay fc r <$> caseLam x
-- All the others, no recursive case so just return the input
caseLam x = pure x
caseLamConAlt : {auto n : Ref NextName Int} ->
CConAlt vars -> Core (CConAlt vars)
caseLamConAlt (MkConAlt n tag args sc)
= MkConAlt n tag args <$> caseLam sc
caseLamConstAlt : {auto n : Ref NextName Int} ->
CConstAlt vars -> Core (CConstAlt vars)
caseLamConstAlt (MkConstAlt c sc) = MkConstAlt c <$> caseLam sc
export
caseLamDef : {auto c : Ref Ctxt Defs} ->
Name -> Core ()
caseLamDef n
= do defs <- get Ctxt
Just def <- lookupCtxtExact n (gamma defs) | Nothing => pure ()
let Just cexpr = compexpr def | Nothing => pure ()
setCompiled n !(doCaseLam cexpr)
where
doCaseLam : CDef -> Core CDef
doCaseLam (MkFun args def)
= do n <- newRef NextName 0
pure $ MkFun args !(caseLam def)
doCaseLam d = pure d

View File

@ -57,9 +57,9 @@ Ord UsePhase where
where
tag : UsePhase -> Int
tag Cases = 0
tag Lifted = 0
tag ANF = 0
tag VMCode = 0
tag Lifted = 1
tag ANF = 2
tag VMCode = 3
public export
record CompileData where
@ -91,7 +91,7 @@ compile {c} cg tm out
let outputDir = outputDirWithDefault d
ensureDirectoryExists tmpDir
ensureDirectoryExists outputDir
logTime "Code generation overall" $
logTime "+ Code generation overall" $
compileExpr cg c tmpDir outputDir tm out
||| execute
@ -266,7 +266,7 @@ getCompileData doLazyAnnots phase tm_in
-- to check than a NameMap!)
asize <- getNextEntry
arr <- coreLift $ newArray asize
logTime "Get names" $ getAllDesc (natHackNames' ++ keys ns) arr defs
logTime "++ Get names" $ getAllDesc (natHackNames' ++ keys ns) arr defs
let entries = mapMaybe id !(coreLift (toList arr))
let allNs = map (Resolved . fst) entries
@ -276,9 +276,9 @@ getCompileData doLazyAnnots phase tm_in
-- unknown due to cyclic modules (i.e. declared in one, defined in
-- another)
rcns <- filterM nonErased cns
logTime "Merge lambda" $ traverse_ mergeLamDef rcns
logTime "Fix arity" $ traverse_ fixArityDef rcns
logTime "Forget names" $ traverse_ mkForgetDef rcns
logTime "++ Merge lambda" $ traverse_ mergeLamDef rcns
logTime "++ Fix arity" $ traverse_ fixArityDef rcns
logTime "++ Forget names" $ traverse_ mkForgetDef rcns
compiledtm <- fixArityExp !(compileExp tm)
let mainname = MN "__mainExpression" 0
@ -286,17 +286,17 @@ getCompileData doLazyAnnots phase tm_in
namedefs <- traverse getNamedDef rcns
lifted_in <- if phase >= Lifted
then logTime "Lambda lift" $ traverse (lambdaLift doLazyAnnots) rcns
then logTime "++ Lambda lift" $ traverse (lambdaLift doLazyAnnots) rcns
else pure []
let lifted = (mainname, MkLFun [] [] liftedtm) ::
ldefs ++ concat lifted_in
anf <- if phase >= ANF
then logTime "Get ANF" $ traverse (\ (n, d) => pure (n, !(toANF d))) lifted
then logTime "++ Get ANF" $ traverse (\ (n, d) => pure (n, !(toANF d))) lifted
else pure []
vmcode <- if phase >= VMCode
then logTime "Get VM Code" $ pure (allDefs anf)
then logTime "++ Get VM Code" $ pure (allDefs anf)
else pure []
defs <- get Ctxt

View File

@ -31,13 +31,22 @@ numArgs defs (Ref _ _ n)
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))
PMDef _ args _ _ _ => pure (EraseArgs (length args) (eraseArgs gdef))
ExternDef arity => pure (Arity arity)
ForeignDef arity _ => pure (Arity arity)
Builtin {arity} f => pure (Arity arity)
_ => pure (Arity 0)
numArgs _ tm = pure (Arity 0)
mkSub : Nat -> (ns : List Name) -> List Nat -> (ns' ** SubVars ns' ns)
mkSub i _ [] = (_ ** SubRefl)
mkSub i [] ns = (_ ** SubRefl)
mkSub i (x :: xs) es
= let (ns' ** p) = mkSub (S i) xs es in
if i `elem` es
then (ns' ** DropCons p)
else (x :: ns' ** KeepCons p)
weakenVar : Var ns -> Var (a :: ns)
weakenVar (MkVar p) = (MkVar (Later p))
@ -98,23 +107,28 @@ applyNewType arity pos fn args
keepArg (CCon fc _ _ args) = keep 0 args
keepArg tm = CErased (getFC fn)
dropFrom : List Nat -> Nat -> List (CExp vs) -> List (CExp vs)
dropFrom epos i [] = []
dropFrom epos i (x :: xs)
= if i `elem` epos
then dropFrom epos (1 + i) xs
else x :: dropFrom epos (1 + i) xs
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 (CApp fc tm@(CApp _ _ _) args')
= CApp fc (dropPos epos tm) args'
dropPos epos (CApp fc f args) = CApp fc f (dropFrom epos 0 args)
dropPos epos (CCon fc c a args) = CCon fc c a (dropFrom epos 0 args)
dropPos epos tm = tm
eraseConArgs : {vars : _} ->
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
if not (isNil epos)
then dropPos epos fn' -- fn' might be lambdas, after eta expansion
else fn'
mkDropSubst : Nat -> List Nat ->
(rest : List Name) ->
@ -127,7 +141,7 @@ mkDropSubst i es rest (x :: xs)
then (vs ** DropCons sub)
else (x :: vs ** KeepCons sub)
-- Rewrite applications of Nat constructors and functions to more optimal
-- Rewrite applications of Nat-like constructors and functions to more optimal
-- versions using Integer
-- None of these should be hard coded, but we'll do it this way until we
@ -136,10 +150,10 @@ mkDropSubst i es rest (x :: xs)
-- Common.idr, so that they get compiled, as they won't be spotted by the
-- usual calls to 'getRefs'.
data Magic : Type where
MagicCCon : Namespace -> String -> (arity : Nat) -> -- checks
MagicCCon : Name -> (arity : Nat) -> -- checks
(FC -> forall vars. Vect arity (CExp vars) -> CExp vars) -> -- translation
Magic
MagicCRef : Namespace -> String -> (arity : Nat) -> -- checks
MagicCRef : Name -> (arity : Nat) -> -- checks
(FC -> FC -> forall vars. Vect arity (CExp vars) -> CExp vars) -> --translation
Magic
@ -148,11 +162,11 @@ magic ms (CLam fc x exp) = CLam fc x (magic ms exp)
magic ms e = go ms e where
fire : Magic -> CExp vars -> Maybe (CExp vars)
fire (MagicCCon ns n arity f) (CCon fc (NS ns' (UN n')) _ es)
= do guard (n == n' && ns == ns')
fire (MagicCCon n arity f) (CCon fc n' _ es)
= do guard (n == n')
map (f fc) (toVect arity es)
fire (MagicCRef ns n arity f) (CApp fc (CRef fc' (NS ns' (UN n'))) es)
= do guard (n == n' && ns == ns')
fire (MagicCRef n arity f) (CApp fc (CRef fc' n') es)
= do guard (n == n')
map (f fc fc') (toVect arity es)
fire _ _ = Nothing
@ -165,63 +179,99 @@ magic ms e = go ms e where
natMinus : FC -> FC -> forall vars. Vect 2 (CExp vars) -> CExp vars
natMinus fc fc' [m,n] = CApp fc (CRef fc' (UN "prim__sub_Integer")) [m, n]
natHack : CExp vars -> CExp vars
natHack = magic
[ MagicCCon typesNS "Z" 0
(\ fc, [] => CPrimVal fc (BI 0))
, MagicCCon typesNS "S" 1
(\ fc, [k] => CApp fc (CRef fc (UN "prim__add_Integer")) [CPrimVal fc (BI 1), k])
, MagicCRef typesNS "natToInteger" 1
-- TODO: next release remove this and use %builtin pragma
natHack : List Magic
natHack =
[ MagicCRef (NS typesNS (UN "natToInteger")) 1
(\ _, _, [k] => k)
, MagicCRef typesNS "integerToNat" 1
, MagicCRef (NS typesNS (UN "integerToNat")) 1
(\ fc, fc', [k] => CApp fc (CRef fc' (NS typesNS (UN "prim__integerToNat"))) [k])
, MagicCRef typesNS "plus" 2
, MagicCRef (NS typesNS (UN "plus")) 2
(\ fc, fc', [m,n] => CApp fc (CRef fc' (UN "prim__add_Integer")) [m, n])
, MagicCRef typesNS "mult" 2
, MagicCRef (NS typesNS (UN "mult")) 2
(\ fc, fc', [m,n] => CApp fc (CRef fc' (UN "prim__mul_Integer")) [m, n])
, MagicCRef natNS "minus" 2 natMinus
, MagicCRef (NS natNS (UN "minus")) 2 natMinus
]
-- get all transformation from %builtin pragmas
builtinMagic : Ref Ctxt Defs => Core (forall vars. CExp vars -> CExp vars)
builtinMagic = do
defs <- get Ctxt
let b = defs.builtinTransforms
let nats = concatMap builtinMagicNat $ values $ natTyNames b
pure $ magic $ natHack ++ nats
where
builtinMagicNat : NatBuiltin -> List Magic
builtinMagicNat cons =
[ MagicCCon cons.zero 0
(\ fc, [] => CPrimVal fc (BI 0))
, MagicCCon cons.succ 1
(\ fc, [k] => CApp fc (CRef fc (UN "prim__add_Integer")) [CPrimVal fc (BI 1), k])
] -- TODO: add builtin pragmas for Nat related functions (to/from Integer, add, mult, minus, compare)
isNatCon : Name -> Bool
isNatCon (NS ns (UN n))
= (n == "Z" || n == "S") && ns == typesNS
isNatCon _ = False
isNatCon : (zeroMap : NameMap ZERO) ->
(succMap : NameMap SUCC) ->
Name -> Bool
isNatCon zs ss n = isJust (lookup n zs) || isJust (lookup n ss)
natBranch : CConAlt vars -> Bool
natBranch (MkConAlt n _ _ _) = isNatCon n
natBranch : (zeroMap : NameMap ZERO) ->
(succMap : NameMap SUCC) ->
CConAlt vars -> Bool
natBranch zs ss (MkConAlt n _ _ _) = isNatCon zs ss n
trySBranch : CExp vars -> CConAlt vars -> Maybe (CExp vars)
trySBranch n (MkConAlt (NS ns (UN nm)) _ [arg] sc)
= do guard (nm == "S" && ns == typesNS)
trySBranch :
(succMap : NameMap SUCC) ->
CExp vars ->
CConAlt vars ->
Maybe (CExp vars)
trySBranch ss n (MkConAlt nm _ [arg] sc)
= do guard $ isJust $ lookup nm ss
let fc = getFC n
pure (CLet fc arg True (natMinus fc fc [n, CPrimVal fc (BI 1)]) sc)
trySBranch _ _ = Nothing
trySBranch _ _ _ = Nothing
tryZBranch : CConAlt vars -> Maybe (CExp vars)
tryZBranch (MkConAlt (NS ns (UN n)) _ [] sc)
= do guard (n == "Z" && ns == typesNS)
tryZBranch :
(zeroMap : NameMap ZERO) ->
CConAlt vars ->
Maybe (CExp vars)
tryZBranch zs (MkConAlt n _ [] sc)
= do guard $ isJust $ lookup n zs
pure sc
tryZBranch _ = Nothing
tryZBranch _ _ = Nothing
getSBranch : CExp vars -> List (CConAlt vars) -> Maybe (CExp vars)
getSBranch n [] = Nothing
getSBranch n (x :: xs) = trySBranch n x <+> getSBranch n xs
getSBranch :
(succMap : NameMap SUCC) ->
CExp vars ->
List (CConAlt vars) ->
Maybe (CExp vars)
getSBranch ss n [] = Nothing
getSBranch ss n (x :: xs) = trySBranch ss n x <+> getSBranch ss n xs
getZBranch : List (CConAlt vars) -> Maybe (CExp vars)
getZBranch [] = Nothing
getZBranch (x :: xs) = tryZBranch x <+> getZBranch xs
getZBranch :
(zeroMap : NameMap ZERO) ->
List (CConAlt vars) ->
Maybe (CExp vars)
getZBranch zs [] = Nothing
getZBranch zs (x :: xs) = tryZBranch zs x <+> getZBranch zs xs
-- Rewrite case trees on Nat to be case trees on Integer
natHackTree : CExp vars -> CExp vars
natHackTree (CConCase fc sc alts def)
= if any natBranch alts
builtinNatTree' : (zeroMap : NameMap ZERO) ->
(succMap : NameMap SUCC) ->
CExp vars -> CExp vars
builtinNatTree' zs ss (CConCase fc sc alts def)
= if any (natBranch zs ss) alts
then let defb = maybe (CCrash fc "Nat case not covered") id def
scase = maybe defb id (getSBranch sc alts)
zcase = maybe defb id (getZBranch alts) in
scase = maybe defb id (getSBranch ss sc alts)
zcase = maybe defb id (getZBranch zs alts) in
CConstCase fc sc [MkConstAlt (BI 0) zcase] (Just scase)
else CConCase fc sc alts def
natHackTree t = t
builtinNatTree' zs ss t = t
builtinNatTree : Ref Ctxt Defs => Core (CExp vars -> CExp vars)
builtinNatTree = do
defs <- get Ctxt
let b = defs.builtinTransforms
pure $ builtinNatTree' b.natZNames b.natSNames
-- Rewrite case trees on Bool/Ord to be case trees on Integer
-- TODO: Generalise to all finite enumerations
@ -248,71 +298,75 @@ boolHackTree t = t
mutual
toCExpTm : {vars : _} ->
{auto c : Ref Ctxt Defs} ->
Name -> Term vars -> Core (CExp vars)
toCExpTm n (Local fc _ _ prf)
(magic : forall vars. CExp vars -> CExp vars) ->
Name -> Term vars ->
Core (CExp vars)
toCExpTm m n (Local fc _ _ prf)
= pure $ CLocal fc prf
-- TMP HACK: extend this to all types which look like enumerations after erasure
toCExpTm n (Ref fc (DataCon tag arity) fn)
toCExpTm m n (Ref fc (DataCon tag arity) fn)
= if arity == Z && isFiniteEnum fn
then pure $ CPrimVal fc (I tag)
else -- get full name for readability, and the Nat hack
else -- get full name for readability, and %builtin Natural
pure $ CCon fc !(getFullName fn) (Just tag) []
toCExpTm n (Ref fc (TyCon tag arity) fn)
toCExpTm m n (Ref fc (TyCon tag arity) fn)
= pure $ CCon fc fn Nothing []
toCExpTm n (Ref fc _ fn)
toCExpTm m n (Ref fc _ fn)
= do full <- getFullName fn
-- ^ For readability of output code, and the Nat hack,
pure $ CApp fc (CRef fc full) []
toCExpTm n (Meta fc mn i args)
= pure $ CApp fc (CRef fc mn) !(traverse (toCExp n) args)
toCExpTm n (Bind fc x (Lam _ _ _ _) sc)
= pure $ CLam fc x !(toCExp n sc)
toCExpTm n (Bind fc x (Let _ rig val _) sc)
= do sc' <- toCExp n sc
toCExpTm m n (Meta fc mn i args)
= pure $ CApp fc (CRef fc mn) !(traverse (toCExp m n) args)
toCExpTm m n (Bind fc x (Lam _ _ _ _) sc)
= pure $ CLam fc x !(toCExp m n sc)
toCExpTm m n (Bind fc x (Let _ rig val _) sc)
= do sc' <- toCExp m n sc
pure $ branchZero (shrinkCExp (DropCons SubRefl) sc')
(CLet fc x True !(toCExp n val) sc')
(CLet fc x True !(toCExp m n val) sc')
rig
toCExpTm n (Bind fc x (Pi _ c e ty) sc)
= pure $ CCon fc (UN "->") Nothing [!(toCExp n ty),
CLam fc x !(toCExp n sc)]
toCExpTm n (Bind fc x b tm) = pure $ CErased fc
toCExpTm m n (Bind fc x (Pi _ c e ty) sc)
= pure $ CCon fc (UN "->") Nothing [!(toCExp m n ty),
CLam fc x !(toCExp m n sc)]
toCExpTm m n (Bind fc x b tm) = pure $ CErased fc
-- We'd expect this to have been dealt with in toCExp, but for completeness...
toCExpTm n (App fc tm arg)
= pure $ CApp fc !(toCExp n tm) [!(toCExp n arg)]
toCExpTm m n (App fc tm arg)
= pure $ CApp fc !(toCExp m n tm) [!(toCExp m n arg)]
-- This shouldn't be in terms any more, but here for completeness
toCExpTm n (As _ _ _ p) = toCExpTm n p
toCExpTm m n (As _ _ _ p) = toCExpTm m n p
-- TODO: Either make sure 'Delayed' is always Rig0, or add to typecase
toCExpTm n (TDelayed fc _ _) = pure $ CErased fc
toCExpTm n (TDelay fc lr _ arg)
= pure (CDelay fc lr !(toCExp n arg))
toCExpTm n (TForce fc lr arg)
= pure (CForce fc lr !(toCExp n arg))
toCExpTm n (PrimVal fc c)
toCExpTm m n (TDelayed fc _ _) = pure $ CErased fc
toCExpTm m n (TDelay fc lr _ arg)
= pure (CDelay fc lr !(toCExp m n arg))
toCExpTm m n (TForce fc lr arg)
= pure (CForce fc lr !(toCExp m n arg))
toCExpTm m n (PrimVal fc c)
= let t = constTag c in
if t == 0
then pure $ CPrimVal fc c
else pure $ CCon fc (UN (show c)) Nothing []
toCExpTm n (Erased fc _) = pure $ CErased fc
toCExpTm n (TType fc) = pure $ CCon fc (UN "Type") Nothing []
toCExpTm m n (Erased fc _) = pure $ CErased fc
toCExpTm m n (TType fc) = pure $ CCon fc (UN "Type") Nothing []
toCExp : {vars : _} ->
{auto c : Ref Ctxt Defs} ->
Name -> Term vars -> Core (CExp vars)
toCExp n tm
(magic : forall vars. CExp vars -> CExp vars) ->
Name -> Term vars ->
Core (CExp vars)
toCExp m n tm
= case getFnArgs tm of
(f, args) =>
do args' <- traverse (toCExp n) args
do args' <- traverse (toCExp m n) args
defs <- get Ctxt
f' <- toCExpTm n f
f' <- toCExpTm m n f
Arity a <- numArgs defs f
| NewTypeBy arity pos =>
do let res = applyNewType arity pos f' args'
pure $ natHack res
pure $ m res
| EraseArgs arity epos =>
do let res = eraseConArgs arity epos f' args'
pure $ natHack res
pure $ m res
let res = expandToArity a f' args'
pure $ natHack res
pure $ m res
mutual
conCases : {vars : _} ->
@ -448,7 +502,7 @@ mutual
def <- getDef n alts
if isNil cases
then pure (fromMaybe (CErased fc) def)
else pure $ boolHackTree $ natHackTree $
else pure $ boolHackTree $ !builtinNatTree $
CConCase fc (CLocal fc x) cases def
toCExpTree' n (Case _ x scTy alts@(DelayCase _ _ _ :: _))
= throw (InternalError "Unexpected DelayCase")
@ -463,7 +517,7 @@ mutual
= toCExpTree n sc
toCExpTree' n (Case _ x scTy [])
= pure $ CCrash (getLoc scTy) $ "Missing case tree in " ++ show n
toCExpTree' n (STerm _ tm) = toCExp n tm
toCExpTree' n (STerm _ tm) = toCExp !builtinMagic n tm
toCExpTree' n (Unmatched msg)
= pure $ CCrash emptyFC msg
toCExpTree' n Impossible
@ -598,13 +652,17 @@ getCFTypes args t
= pure (reverse args, !(nfToCFType (getLoc t) False t))
toCDef : {auto c : Ref Ctxt Defs} ->
Name -> ClosedTerm -> Def ->
Name -> ClosedTerm -> List Nat -> Def ->
Core CDef
toCDef n ty None
toCDef n ty _ None
= pure $ MkError $ CCrash emptyFC ("Encountered undefined name " ++ show !(getFullName n))
toCDef n ty (PMDef _ args _ tree _)
= pure $ MkFun _ !(toCExpTree n tree)
toCDef n ty (ExternDef arity)
toCDef n ty erased (PMDef _ args _ tree _)
= do let (args' ** p) = mkSub 0 args erased
comptree <- toCExpTree n tree
if isNil erased
then pure $ MkFun args comptree
else pure $ MkFun args' (shrinkCExp p comptree)
toCDef n ty _ (ExternDef arity)
= let (ns ** args) = mkArgList 0 arity in
pure $ MkFun _ (CExtPrim emptyFC !(getFullName n) (map toArgExp (getVars args)))
where
@ -614,11 +672,11 @@ toCDef n ty (ExternDef arity)
getVars : ArgList k ns -> List (Var ns)
getVars NoArgs = []
getVars (ConsArg a rest) = MkVar First :: map weakenVar (getVars rest)
toCDef n ty (ForeignDef arity cs)
toCDef n ty _ (ForeignDef arity cs)
= do defs <- get Ctxt
(atys, retty) <- getCFTypes [] !(nf defs [] ty)
pure $ MkForeign cs atys retty
toCDef n ty (Builtin {arity} op)
toCDef n ty _ (Builtin {arity} op)
= let (ns ** args) = mkArgList 0 arity in
pure $ MkFun _ (COp emptyFC op (map toArgExp (getVars args)))
where
@ -628,7 +686,7 @@ toCDef n ty (Builtin {arity} op)
getVars : ArgList k ns -> Vect k (Var ns)
getVars NoArgs = []
getVars (ConsArg a rest) = MkVar First :: map weakenVar (getVars rest)
toCDef n _ (DCon tag arity pos)
toCDef n _ _ (DCon tag arity pos)
= do let nt = snd <$> pos
defs <- get Ctxt
args <- numArgs {vars = []} defs (Ref EmptyFC (DataCon tag arity) n)
@ -637,20 +695,20 @@ toCDef n _ (DCon tag arity pos)
EraseArgs ar erased => ar `minus` length erased
Arity ar => ar
pure $ MkCon (Just tag) arity' nt
toCDef n _ (TCon tag arity _ _ _ _ _ _)
toCDef n _ _ (TCon tag arity _ _ _ _ _ _)
= pure $ MkCon Nothing arity Nothing
-- We do want to be able to compile these, but also report an error at run time
-- (and, TODO: warn at compile time)
toCDef n ty (Hole _ _)
toCDef n ty _ (Hole _ _)
= pure $ MkError $ CCrash emptyFC ("Encountered unimplemented hole " ++
show !(getFullName n))
toCDef n ty (Guess _ _ _)
toCDef n ty _ (Guess _ _ _)
= pure $ MkError $ CCrash emptyFC ("Encountered constrained hole " ++
show !(getFullName n))
toCDef n ty (BySearch _ _ _)
toCDef n ty _ (BySearch _ _ _)
= pure $ MkError $ CCrash emptyFC ("Encountered incomplete proof search " ++
show !(getFullName n))
toCDef n ty def
toCDef n ty _ def
= pure $ MkError $ CCrash emptyFC ("Encountered uncompilable name " ++
show (!(getFullName n), def))
@ -658,7 +716,8 @@ export
compileExp : {auto c : Ref Ctxt Defs} ->
ClosedTerm -> Core (CExp [])
compileExp tm
= do exp <- toCExp (UN "main") tm
= do m <- builtinMagic
exp <- toCExp m (UN "main") tm
pure exp
||| Given a name, look up an expression, and compile it to a CExp in the environment
@ -668,7 +727,7 @@ compileDef n
= do defs <- get Ctxt
Just gdef <- lookupCtxtExact n (gamma defs)
| Nothing => throw (InternalError ("Trying to compile unknown name " ++ show n))
ce <- toCDef n (type gdef)
ce <- toCDef n (type gdef) (eraseArgs gdef)
!(toFullNames (definition gdef))
setCompiled n ce

View File

@ -194,50 +194,64 @@ jsConstant (B32 i) = pure $ show i ++ "n"
jsConstant (B64 i) = pure $ show i ++ "n"
jsConstant ty = throw (InternalError $ "Unsuported constant " ++ show ty)
-- Creates the definition of a binary arithmetic operation.
-- Rounding / truncation behavior is determined from the
-- `IntKind`.
arithOp : {auto c : Ref ESs ESSt}
-> Maybe IntKind
-> (op : String)
-> (x : String)
-> (y : String)
-> Core String
arithOp (Just $ Signed $ P n) op x y = boundedIntOp (n-1) op x y
arithOp (Just $ Unsigned $ P n) op x y = boundedUIntOp n op x y
arithOp _ op x y = pure $ binOp op x y
-- Same as `arithOp` but for bitwise operations that might
-- go out of the valid range.
bitOp : {auto c : Ref ESs ESSt}
-> Maybe IntKind
-> (op : String)
-> (x : String)
-> (y : String)
-> Core String
bitOp (Just $ Signed $ P n) op x y = boundedIntBitOp (n-1) op x y
bitOp (Just $ Unsigned $ P n) op x y = boundedUIntOp n op x y
bitOp _ op x y = pure $ binOp op x y
castInt : {auto c : Ref ESs ESSt}
-> Constant
-> Constant
-> String
-> Core String
castInt from to x =
case (intKind from, intKind to) of
(Just _, Just $ Signed Unlimited) => pure x
(Just $ Signed m, Just $ Signed $ P n) =>
if P n >= m then pure x else boundedInt (n-1) x
-- Only if the precision of the target is greater
-- than the one of the source, there is no need to cast.
(Just $ Unsigned m, Just $ Signed $ P n) =>
if P n > m then pure x else boundedInt (n-1) x
(Just $ Signed _, Just $ Unsigned $ P n) => boundedUInt n x
(Just $ Unsigned m, Just $ Unsigned $ P n) =>
if P n >= m then pure x else boundedUInt n x
_ => throw $ InternalError $ "invalid cast: + " ++ show from ++ " + ' -> ' + " ++ show to
jsOp : {auto c : Ref ESs ESSt} -> PrimFn arity -> Vect arity String -> Core String
jsOp (Add IntType) [x, y] = pure $ !(boundedIntOp 63 "+" x y)
jsOp (Sub IntType) [x, y] = pure $ !(boundedIntOp 63 "-" x y)
jsOp (Mul IntType) [x, y] = pure $ !(boundedIntOp 63 "*" x y)
jsOp (Div IntType) [x, y] = pure $ !(boundedIntOp 63 "/" x y)
jsOp (Mod IntType) [x, y] = pure $ !(boundedIntOp 63 "%" x y)
jsOp (Add Bits8Type) [x, y] = pure $ !(boundedUIntOp 8 "+" x y)
jsOp (Sub Bits8Type) [x, y] = pure $ !(boundedUIntOp 8 "-" x y)
jsOp (Mul Bits8Type) [x, y] = pure $ !(boundedUIntOp 8 "*" x y)
jsOp (Div Bits8Type) [x, y] = pure $ !(boundedUIntOp 8 "/" x y)
jsOp (Mod Bits8Type) [x, y] = pure $ !(boundedUIntOp 8 "%" x y)
jsOp (Add Bits16Type) [x, y] = pure $ !(boundedUIntOp 16 "+" x y)
jsOp (Sub Bits16Type) [x, y] = pure $ !(boundedUIntOp 16 "-" x y)
jsOp (Mul Bits16Type) [x, y] = pure $ !(boundedUIntOp 16 "*" x y)
jsOp (Div Bits16Type) [x, y] = pure $ !(boundedUIntOp 16 "/" x y)
jsOp (Mod Bits16Type) [x, y] = pure $ !(boundedUIntOp 16 "%" x y)
jsOp (Add Bits32Type) [x, y] = pure $ !(boundedUIntOp 32 "+" x y)
jsOp (Sub Bits32Type) [x, y] = pure $ !(boundedUIntOp 32 "-" x y)
jsOp (Mul Bits32Type) [x, y] = pure $ !(boundedUIntOp 32 "*" x y)
jsOp (Div Bits32Type) [x, y] = pure $ !(boundedUIntOp 32 "/" x y)
jsOp (Mod Bits32Type) [x, y] = pure $ !(boundedUIntOp 32 "%" x y)
jsOp (Add Bits64Type) [x, y] = pure $ !(boundedUIntOp 64 "+" x y)
jsOp (Sub Bits64Type) [x, y] = pure $ !(boundedUIntOp 64 "-" x y)
jsOp (Mul Bits64Type) [x, y] = pure $ !(boundedUIntOp 64 "*" x y)
jsOp (Div Bits64Type) [x, y] = pure $ !(boundedUIntOp 64 "/" x y)
jsOp (Mod Bits64Type) [x, y] = pure $ !(boundedUIntOp 64 "%" x y)
jsOp (Add ty) [x, y] = pure $ binOp "+" x y
jsOp (Sub ty) [x, y] = pure $ binOp "-" x y
jsOp (Mul ty) [x, y] = pure $ binOp "*" x y
jsOp (Div ty) [x, y] = pure $ binOp "/" x y
jsOp (Mod ty) [x, y] = pure $ binOp "%" x y
jsOp (Add ty) [x, y] = arithOp (intKind ty) "+" x y
jsOp (Sub ty) [x, y] = arithOp (intKind ty) "-" x y
jsOp (Mul ty) [x, y] = arithOp (intKind ty) "*" x y
jsOp (Div ty) [x, y] = arithOp (intKind ty) "/" x y
jsOp (Mod ty) [x, y] = arithOp (intKind ty) "%" x y
jsOp (Neg ty) [x] = pure $ "(-(" ++ x ++ "))"
jsOp (ShiftL IntType) [x, y] = pure $ !(boundedIntBitOp 63 "<<" x y)
jsOp (ShiftL Bits8Type) [x, y] = pure $ !(boundedUIntOp 8 "<<" x y)
jsOp (ShiftL Bits16Type) [x, y] = pure $ !(boundedUIntOp 16 "<<" x y)
jsOp (ShiftL Bits32Type) [x, y] = pure $ !(boundedUIntOp 32 "<<" x y)
jsOp (ShiftL Bits64Type) [x, y] = pure $ !(boundedUIntOp 64 "<<" x y)
jsOp (ShiftL ty) [x, y] = pure $ binOp "<<" x y
jsOp (ShiftR IntType) [x, y] = pure $ !(boundedIntBitOp 63 ">>" x y)
jsOp (ShiftR Bits8Type) [x, y] = pure $ !(boundedUIntOp 8 ">>" x y)
jsOp (ShiftR Bits16Type) [x, y] = pure $ !(boundedUIntOp 16 ">>" x y)
jsOp (ShiftR Bits32Type) [x, y] = pure $ !(boundedUIntOp 32 ">>" x y)
jsOp (ShiftR Bits64Type) [x, y] = pure $ !(boundedUIntOp 64 ">>" x y)
jsOp (ShiftR ty) [x, y] = pure $ binOp ">>" x y
jsOp (ShiftL ty) [x, y] = bitOp (intKind ty) "<<" x y
jsOp (ShiftR ty) [x, y] = bitOp (intKind ty) ">>" x y
jsOp (BAnd ty) [x, y] = pure $ binOp "&" x y
jsOp (BOr ty) [x, y] = pure $ binOp "|" x y
jsOp (BXOr ty) [x, y] = pure $ binOp "^" x y
@ -270,58 +284,20 @@ jsOp DoubleSqrt [x] = pure $ "Math.sqrt(" ++ x ++ ")"
jsOp DoubleFloor [x] = pure $ "Math.floor(" ++ x ++ ")"
jsOp DoubleCeiling [x] = pure $ "Math.ceil(" ++ x ++ ")"
jsOp (Cast IntType CharType) [x] = pure $ "String.fromCodePoint(" ++ fromBigInt x ++ ")"
jsOp (Cast IntegerType CharType) [x] = pure $ "String.fromCodePoint(" ++ fromBigInt x ++ ")"
jsOp (Cast CharType IntType) [x] = pure $ toBigInt $ x ++ ".codePointAt(0)"
jsOp (Cast CharType IntegerType) [x] = pure $ toBigInt $ x ++ ".codePointAt(0)"
jsOp (Cast DoubleType IntType) [x] = boundedInt 63 $ "BigInt(Math.floor(" ++ x ++ "))"
jsOp (Cast DoubleType IntegerType) [x] = pure $ "BigInt(Math.floor(" ++ x ++ "))"
jsOp (Cast IntType CharType) [x] = pure $ "String.fromCodePoint(" ++ fromBigInt x ++ ")"
jsOp (Cast IntType DoubleType) [x] = pure $ "Number(" ++ x ++ ")"
jsOp (Cast IntegerType CharType) [x] = pure $ "String.fromCodePoint(" ++ fromBigInt x ++ ")"
jsOp (Cast IntegerType DoubleType) [x] = pure $ "Number(" ++ x ++ ")"
jsOp (Cast StringType DoubleType) [x] = pure $ "parseFloat(" ++ x ++ ")"
jsOp (Cast StringType IntType) [x] = boundedInt 63 $ !(jsIntegerOfString x)
jsOp (Cast StringType IntegerType) [x] = jsIntegerOfString x
jsOp (Cast IntegerType IntType) [x] = boundedInt 63 x
jsOp (Cast IntType IntegerType) [x] = pure x
jsOp (Cast StringType DoubleType) [x] = pure $ "parseFloat(" ++ x ++ ")"
jsOp (Cast Bits8Type IntType) [x] = pure x
jsOp (Cast Bits16Type IntType) [x] = pure x
jsOp (Cast Bits32Type IntType) [x] = pure x
jsOp (Cast Bits64Type IntType) [x] = pure x
jsOp (Cast Bits8Type IntegerType) [x] = pure x
jsOp (Cast Bits16Type IntegerType) [x] = pure x
jsOp (Cast Bits32Type IntegerType) [x] = pure x
jsOp (Cast Bits64Type IntegerType) [x] = pure x
jsOp (Cast IntType Bits8Type) [x] = boundedUInt 8 x
jsOp (Cast IntType Bits16Type) [x] = boundedUInt 16 x
jsOp (Cast IntType Bits32Type) [x] = boundedUInt 32 x
jsOp (Cast IntType Bits64Type) [x] = boundedUInt 64 x
jsOp (Cast IntegerType Bits8Type) [x] = boundedUInt 8 x
jsOp (Cast IntegerType Bits16Type) [x] = boundedUInt 16 x
jsOp (Cast IntegerType Bits32Type) [x] = boundedUInt 32 x
jsOp (Cast IntegerType Bits64Type) [x] = boundedUInt 64 x
jsOp (Cast Bits8Type Bits16Type) [x] = pure x
jsOp (Cast Bits8Type Bits32Type) [x] = pure x
jsOp (Cast Bits8Type Bits64Type) [x] = pure x
jsOp (Cast Bits16Type Bits8Type) [x] = boundedUInt 8 x
jsOp (Cast Bits16Type Bits32Type) [x] = pure x
jsOp (Cast Bits16Type Bits64Type) [x] = pure x
jsOp (Cast Bits32Type Bits8Type) [x] = boundedUInt 8 x
jsOp (Cast Bits32Type Bits16Type) [x] = boundedUInt 16 x
jsOp (Cast Bits32Type Bits64Type) [x] = pure x
jsOp (Cast Bits64Type Bits8Type) [x] = boundedUInt 8 x
jsOp (Cast Bits64Type Bits16Type) [x] = boundedUInt 16 x
jsOp (Cast Bits64Type Bits32Type) [x] = boundedUInt 32 x
jsOp (Cast ty StringType) [x] = pure $ "(''+" ++ x ++ ")"
jsOp (Cast ty ty2) [x] = jsCrashExp $ jsString $ "invalid cast: + " ++ show ty ++ " + ' -> ' + " ++ show ty2
jsOp (Cast ty ty2) [x] = castInt ty ty2 x
jsOp BelieveMe [_,_,x] = pure x
jsOp (Crash) [_, msg] = jsCrashExp msg

View File

@ -47,7 +47,8 @@ executeExpr c tmpDir tm
Right () <- coreLift $ writeFile outn js
| Left err => throw (FileErr outn err)
node <- coreLift findNode
coreLift_ $ system (node ++ " " ++ outn)
quoted_node <- pure $ "\"" ++ node ++ "\"" -- Windows often have a space in the path.
coreLift_ $ system (quoted_node ++ " " ++ outn)
pure ()
||| Codegen wrapper for Node implementation.

View File

@ -1,5 +1,6 @@
module Compiler.Inline
import Compiler.CaseOpts
import Compiler.CompileExpr
import Core.CompileExpr
@ -149,7 +150,7 @@ mutual
-- boost by removing unnecessary lambdas that we'll keep the special case.
eval rec env stk (CRef fc n)
= case (n == NS primIONS (UN "io_bind"), stk) of
(True, _ :: _ :: act :: cont :: world :: stk) =>
(True, act :: cont :: world :: stk) =>
do xn <- genName "act"
sc <- eval rec [] [] (CApp fc cont [CRef fc xn, world])
pure $ unload stk $
@ -415,6 +416,43 @@ mergeLam (MkFun args def)
pure $ MkFun args' exp'
mergeLam d = pure d
mutual
addRefs : NameMap Bool -> CExp vars -> NameMap Bool
addRefs ds (CRef _ n) = insert n False ds
addRefs ds (CLam _ _ sc) = addRefs ds sc
addRefs ds (CLet _ _ _ val sc) = addRefs (addRefs ds val) sc
addRefs ds (CApp _ f args) = addRefsArgs (addRefs ds f) args
addRefs ds (CCon _ _ _ args) = addRefsArgs ds args
addRefs ds (COp _ _ args) = addRefsArgs ds (toList args)
addRefs ds (CExtPrim _ _ args) = addRefsArgs ds args
addRefs ds (CForce _ _ e) = addRefs ds e
addRefs ds (CDelay _ _ e) = addRefs ds e
addRefs ds (CConCase _ sc alts def)
= let ds' = maybe ds (addRefs ds) def in
addRefsConAlts (addRefs ds' sc) alts
addRefs ds (CConstCase _ sc alts def)
= let ds' = maybe ds (addRefs ds) def in
addRefsConstAlts (addRefs ds' sc) alts
addRefs ds tm = ds
addRefsArgs : NameMap Bool -> List (CExp vars) -> NameMap Bool
addRefsArgs ds [] = ds
addRefsArgs ds (a :: as) = addRefsArgs (addRefs ds a) as
addRefsConAlts : NameMap Bool -> List (CConAlt vars) -> NameMap Bool
addRefsConAlts ds [] = ds
addRefsConAlts ds (MkConAlt _ _ _ sc :: rest)
= addRefsConAlts (addRefs ds sc) rest
addRefsConstAlts : NameMap Bool -> List (CConstAlt vars) -> NameMap Bool
addRefsConstAlts ds [] = ds
addRefsConstAlts ds (MkConstAlt _ sc :: rest)
= addRefsConstAlts (addRefs ds sc) rest
getRefs : CDef -> NameMap Bool
getRefs (MkFun args exp) = addRefs empty exp
getRefs _ = empty
export
inlineDef : {auto c : Ref Ctxt Defs} ->
Name -> Core ()
@ -424,6 +462,17 @@ inlineDef n
let Just cexpr = compexpr def | Nothing => pure ()
setCompiled n !(inline n cexpr)
-- Update the names a function refers to at runtime based on the transformation
-- results (saves generating code unnecessarily).
updateCallGraph : {auto c : Ref Ctxt Defs} ->
Name -> Core ()
updateCallGraph n
= do defs <- get Ctxt
Just def <- lookupCtxtExact n (gamma defs) | Nothing => pure ()
let Just cexpr = compexpr def | Nothing => pure ()
let refs = getRefs cexpr
ignore $ addDef n (record { refersToRuntimeM = Just refs } def)
export
fixArityDef : {auto c : Ref Ctxt Defs} ->
Name -> Core ()
@ -454,10 +503,15 @@ compileAndInlineAll
traverse_ inlineDef cns
traverse_ mergeLamDef cns
traverse_ caseLamDef cns
traverse_ fixArityDef cns
traverse_ inlineDef cns
traverse_ mergeLamDef cns
traverse_ caseLamDef cns
traverse_ fixArityDef cns
traverse_ updateCallGraph cns
where
nonErased : Name -> Core Bool
nonErased n

View File

@ -158,6 +158,61 @@ unload fc _ f [] = pure f
-- only outermost LApp must be lazy as rest will be closures
unload fc lazy f (a :: as) = unload fc Nothing (LApp fc lazy f a) as
record Used (vars : List Name) where
constructor MkUsed
used : Vect (length vars) Bool
initUsed : {vars : _} -> Used vars
initUsed {vars} = MkUsed (replicate (length vars) False)
lengthDistributesOverAppend
: (xs, ys : List a)
-> length (xs ++ ys) = length xs + length ys
lengthDistributesOverAppend [] ys = Refl
lengthDistributesOverAppend (x :: xs) ys =
cong S $ lengthDistributesOverAppend xs ys
weakenUsed : {outer : _} -> Used vars -> Used (outer ++ vars)
weakenUsed {outer} (MkUsed xs) =
MkUsed (rewrite lengthDistributesOverAppend outer vars in
(replicate (length outer) False ++ xs))
contractUsed : (Used (x::vars)) -> Used vars
contractUsed (MkUsed xs) = MkUsed (tail xs)
contractUsedMany : {remove : _} ->
(Used (remove ++ vars)) ->
Used vars
contractUsedMany {remove=[]} x = x
contractUsedMany {remove=(r::rs)} x = contractUsedMany {remove=rs} (contractUsed x)
markUsed : {vars : _} ->
(idx : Nat) ->
{0 prf : IsVar x idx vars} ->
Used vars ->
Used vars
markUsed {vars} {prf} idx (MkUsed us) =
let newUsed = replaceAt (finIdx prf) True us in
MkUsed newUsed
where
finIdx : {vars : _} -> {idx : _} ->
(0 prf : IsVar x idx vars) ->
Fin (length vars)
finIdx {idx=Z} First = FZ
finIdx {idx=S x} (Later l) = FS (finIdx l)
getUnused : Used vars ->
Vect (length vars) Bool
getUnused (MkUsed uv) = map not uv
total
dropped : (vars : List Name) ->
(drop : Vect (length vars) Bool) ->
List Name
dropped [] _ = []
dropped (x::xs) (False::us) = x::(dropped xs us)
dropped (x::xs) (True::us) = dropped xs us
mutual
makeLam : {auto l : Ref Lifts LDefs} ->
{vars : _} ->
@ -168,24 +223,27 @@ mutual
makeLam fc bound (CLam _ x sc') = makeLam fc {doLazyAnnots} {lazy} (x :: bound) sc'
makeLam {vars} fc bound sc
= do scl <- liftExp {doLazyAnnots} {lazy} sc
-- Find out which variables aren't used in the new definition, and
-- do not abstract over them in the new definition.
let scUsedL = usedVars initUsed scl
unusedContracted = contractUsedMany {remove=bound} scUsedL
unused = getUnused unusedContracted
scl' = dropUnused {outer=bound} unused scl
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 fc vars)
put Lifts (record { defs $= ((n, MkLFun (dropped vars unused) bound scl') ::) } ldefs)
pure $ LUnderApp fc n (length bound) (allVars fc vars unused)
where
allPrfs : (vs : List Name) -> List (Var vs)
allPrfs [] = []
allPrfs (v :: vs) = MkVar First :: map weaken (allPrfs vs)
allPrfs : (vs : List Name) -> (unused : Vect (length vs) Bool) -> List (Var vs)
allPrfs [] _ = []
allPrfs (v :: vs) (False::uvs) = MkVar First :: map weaken (allPrfs vs uvs)
allPrfs (v :: vs) (True::uvs) = map weaken (allPrfs vs uvs)
-- 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 : FC -> (vs : List Name) -> List (Lifted vs)
allVars fc vs = map (\ (MkVar p) => LLocal fc p) (allPrfs vs)
allVars : FC -> (vs : List Name) -> (unused : Vect (length vs) Bool) -> List (Lifted vs)
allVars fc vs unused = map (\ (MkVar p) => LLocal fc p) (allPrfs vs unused)
-- if doLazyAnnots = True then annotate function application with laziness
-- otherwise use old behaviour (thunk is a function)
@ -234,6 +292,116 @@ mutual
liftExp (CErased fc) = pure $ LErased fc
liftExp (CCrash fc str) = pure $ LCrash fc str
usedVars : {vars : _} ->
{auto l : Ref Lifts LDefs} ->
Used vars ->
Lifted vars ->
Used vars
usedVars used (LLocal {idx} fc prf) =
markUsed {prf} idx used
usedVars used (LAppName fc lazy n args) =
foldl (usedVars {vars}) used args
usedVars used (LUnderApp fc n miss args) =
foldl (usedVars {vars}) used args
usedVars used (LApp fc lazy c arg) =
usedVars (usedVars used arg) c
usedVars used (LLet fc x val sc) =
let innerUsed = contractUsed $ usedVars (weakenUsed {outer=[x]} used) sc in
usedVars innerUsed val
usedVars used (LCon fc n tag args) =
foldl (usedVars {vars}) used args
usedVars used (LOp fc lazy fn args) =
foldl (usedVars {vars}) used args
usedVars used (LExtPrim fc lazy fn args) =
foldl (usedVars {vars}) used args
usedVars used (LConCase fc sc alts def) =
let defUsed = maybe used (usedVars used {vars}) def
scDefUsed = usedVars defUsed sc in
foldl usedConAlt scDefUsed alts
where
usedConAlt : {default Nothing lazy : Maybe LazyReason} ->
Used vars -> LiftedConAlt vars -> Used vars
usedConAlt used (MkLConAlt n tag args sc) =
contractUsedMany {remove=args} (usedVars (weakenUsed used) sc)
usedVars used (LConstCase fc sc alts def) =
let defUsed = maybe used (usedVars used {vars}) def
scDefUsed = usedVars defUsed sc in
foldl usedConstAlt scDefUsed alts
where
usedConstAlt : {default Nothing lazy : Maybe LazyReason} ->
Used vars -> LiftedConstAlt vars -> Used vars
usedConstAlt used (MkLConstAlt c sc) = usedVars used sc
usedVars used (LPrimVal _ _) = used
usedVars used (LErased _) = used
usedVars used (LCrash _ _) = used
dropIdx : {vars : _} ->
{idx : _} ->
(outer : List Name) ->
(unused : Vect (length vars) Bool) ->
(0 p : IsVar x idx (outer ++ vars)) ->
Var (outer ++ (dropped vars unused))
dropIdx [] (False::_) First = MkVar First
dropIdx [] (True::_) First = assert_total $
idris_crash "INTERNAL ERROR: Referenced variable marked as unused"
dropIdx [] (False::rest) (Later p) = Var.later $ dropIdx [] rest p
dropIdx [] (True::rest) (Later p) = dropIdx [] rest p
dropIdx (_::xs) unused First = MkVar First
dropIdx (_::xs) unused (Later p) = Var.later $ dropIdx xs unused p
dropUnused : {vars : _} ->
{auto l : Ref Lifts LDefs} ->
{outer : List Name} ->
(unused : Vect (length vars) Bool) ->
(l : Lifted (outer ++ vars)) ->
Lifted (outer ++ (dropped vars unused))
dropUnused _ (LPrimVal fc val) = LPrimVal fc val
dropUnused _ (LErased fc) = LErased fc
dropUnused _ (LCrash fc msg) = LCrash fc msg
dropUnused {outer} unused (LLocal fc p) =
let (MkVar p') = dropIdx outer unused p in LLocal fc p'
dropUnused unused (LCon fc n tag args) =
let args' = map (dropUnused unused) args in
LCon fc n tag args'
dropUnused {outer} unused (LLet fc n val sc) =
let val' = dropUnused unused val
sc' = dropUnused {outer=n::outer} (unused) sc in
LLet fc n val' sc'
dropUnused unused (LApp fc lazy c arg) =
let c' = dropUnused unused c
arg' = dropUnused unused arg in
LApp fc lazy c' arg'
dropUnused unused (LOp fc lazy fn args) =
let args' = map (dropUnused unused) args in
LOp fc lazy fn args'
dropUnused unused (LExtPrim fc lazy n args) =
let args' = map (dropUnused unused) args in
LExtPrim fc lazy n args'
dropUnused unused (LAppName fc lazy n args) =
let args' = map (dropUnused unused) args in
LAppName fc lazy n args'
dropUnused unused (LUnderApp fc n miss args) =
let args' = map (dropUnused unused) args in
LUnderApp fc n miss args'
dropUnused {vars} {outer} unused (LConCase fc sc alts def) =
let alts' = map dropConCase alts in
LConCase fc (dropUnused unused sc) alts' (map (dropUnused unused) def)
where
dropConCase : LiftedConAlt (outer ++ vars) ->
LiftedConAlt (outer ++ (dropped vars unused))
dropConCase (MkLConAlt n t args sc) =
let sc' = (rewrite sym $ appendAssociative args outer vars in sc)
droppedSc = dropUnused {vars=vars} {outer=args++outer} unused sc' in
MkLConAlt n t args (rewrite appendAssociative args outer (dropped vars unused) in droppedSc)
dropUnused {vars} {outer} unused (LConstCase fc sc alts def) =
let alts' = map dropConstCase alts in
LConstCase fc (dropUnused unused sc) alts' (map (dropUnused unused) def)
where
dropConstCase : LiftedConstAlt (outer ++ vars) ->
LiftedConstAlt (outer ++ (dropped vars unused))
dropConstCase (MkLConstAlt c val) = MkLConstAlt c (dropUnused unused val)
export
liftBody : {vars : _} -> {doLazyAnnots : Bool} ->
Name -> CExp vars -> Core (Lifted vars, List (Name, LiftedDef))

74
src/Compiler/RefC/CC.idr Normal file
View File

@ -0,0 +1,74 @@
module Compiler.RefC.CC
import Core.Context
import Core.Context.Log
import Core.Options
import System
import Idris.Version
import Libraries.Utils.Path
findCC : IO String
findCC
= do Nothing <- getEnv "IDRIS2_CC"
| Just cc => pure cc
Nothing <- getEnv "CC"
| Just cc => pure cc
pure "cc"
fullprefix_dir : Dirs -> String -> String
fullprefix_dir dirs sub
= prefix_dir dirs </> "idris2-" ++ showVersion False version </> sub
export
compileCObjectFile : {auto c : Ref Ctxt Defs}
-> {default False asLibrary : Bool}
-> (sourceFile : String)
-> (objectFile : String)
-> Core (Maybe String)
compileCObjectFile {asLibrary} sourceFile objectFile =
do cc <- coreLift findCC
dirs <- getDirs
let libraryFlag = if asLibrary then "-fpic " else ""
let runccobj = cc ++ " -c " ++ libraryFlag ++ sourceFile ++
" -o " ++ objectFile ++ " " ++
"-I" ++ fullprefix_dir dirs "refc " ++
"-I" ++ fullprefix_dir dirs "include"
log "compiler.refc.cc" 10 runccobj
0 <- coreLift $ system runccobj
| _ => pure Nothing
pure (Just objectFile)
export
compileCFile : {auto c : Ref Ctxt Defs}
-> {default False asShared : Bool}
-> (objectFile : String)
-> (outFile : String)
-> Core (Maybe String)
compileCFile {asShared} objectFile outFile =
do cc <- coreLift findCC
dirs <- getDirs
let sharedFlag = if asShared then "-shared " else ""
let runcc = cc ++ " " ++ sharedFlag ++ objectFile ++
" -o " ++ outFile ++ " " ++
fullprefix_dir dirs "lib" </> "libidris2_support.a" ++ " " ++
"-lidris2_refc " ++
"-L" ++ fullprefix_dir dirs "refc " ++
clibdirs (lib_dirs dirs)
log "compiler.refc.cc" 10 runcc
0 <- coreLift $ system runcc
| _ => pure Nothing
pure (Just outFile)
where
clibdirs : List String -> String
clibdirs ds = concat (map (\d => "-L" ++ d ++ " ") ds)

View File

@ -1,42 +1,27 @@
module Compiler.RefC.RefC
import Compiler.RefC.CC
import Compiler.Common
import Compiler.CompileExpr
import Compiler.LambdaLift
import Compiler.ANF
import Compiler.Inline
import Core.Context
import Core.Context.Log
import Core.Directory
import Core.Name
import Core.Options
import Core.TT
import Data.IORef
import Data.List
import Libraries.Data.DList
import Libraries.Data.NameMap
import Data.Nat
import Data.Strings
import Data.Vect
import System
import System.Info
import System.File
import Idris.Env
import Idris.Version
import Libraries.Utils.Hex
import Libraries.Utils.Path
findCC : IO String
findCC
= do Nothing <- idrisGetEnv "IDRIS2_CC"
| Just cc => pure cc
Nothing <- idrisGetEnv "CC"
| Just cc => pure cc
pure "cc"
showcCleanStringChar : Char -> String -> String
showcCleanStringChar '+' = ("_plus" ++)
showcCleanStringChar '-' = ("__" ++)
@ -1011,7 +996,8 @@ createCFunctions n (MkAError exp) = do
pure ()
header : {auto f : Ref FunctionDefinitions (List String)}
header : {auto c : Ref Ctxt Defs}
-> {auto f : Ref FunctionDefinitions (List String)}
-> {auto o : Ref OutfileText Output}
-> {auto il : Ref IndentLevel Nat}
-> {auto e : Ref ExternalLibs (List String)}
@ -1022,7 +1008,7 @@ header = do
, "#include <idris_support.h> // for libidris2_support"]
extLibs <- get ExternalLibs
let extLibLines = map (\lib => "// add header(s) for library: " ++ lib ++ "\n") extLibs
traverse_ (\l => coreLift (putStrLn $ " header for " ++ l ++ " needed")) extLibs
traverse_ (\l => log "compiler.refc" 20 $ " header for " ++ l ++ " needed") extLibs
fns <- get FunctionDefinitions
update OutfileText (appendL (initLines ++ extLibLines ++ ["\n// function definitions"] ++ fns))
@ -1043,6 +1029,27 @@ executeExpr c _ tm
= do coreLift_ $ putStrLn "Execute expression not yet implemented for refc"
coreLift_ $ system "false"
export
generateCSourceFile : {auto c : Ref Ctxt Defs}
-> List (Name, ANFDef)
-> (outn : String)
-> Core ()
generateCSourceFile defs outn =
do _ <- newRef ArgCounter 0
_ <- newRef FunctionDefinitions []
_ <- newRef TemporaryVariableTracker []
_ <- newRef OutfileText DList.Nil
_ <- newRef ExternalLibs []
_ <- newRef IndentLevel 0
traverse_ (uncurry createCFunctions) defs
header -- added after the definition traversal in order to add all encountered function defintions
footer
fileContent <- get OutfileText
let code = fastAppend (map (++ "\n") (reify fileContent))
coreLift_ $ writeFile outn code
log "compiler.refc" 10 $ "Generated C file " ++ outn
export
compileExpr : UsePhase
-> Ref Ctxt Defs
@ -1055,52 +1062,16 @@ compileExpr ANF c _ outputDir tm outfile =
do let outn = outputDir </> outfile ++ ".c"
let outobj = outputDir </> outfile ++ ".o"
let outexec = outputDir </> outfile
coreLift_ $ mkdirAll outputDir
cdata <- getCompileData False ANF tm
let defs = anf cdata
_ <- newRef ArgCounter 0
_ <- newRef FunctionDefinitions []
_ <- newRef TemporaryVariableTracker []
_ <- newRef OutfileText DList.Nil
_ <- newRef ExternalLibs []
_ <- newRef IndentLevel 0
traverse_ (\(n, d) => createCFunctions n d) defs
header -- added after the definition traversal in order to add all encountered function defintions
footer
fileContent <- get OutfileText
let code = fastAppend (map (++ "\n") (reify fileContent))
coreLift_ $ writeFile outn code
coreLift_ $ putStrLn $ "Generated C file " ++ outn
generateCSourceFile defs outn
Just _ <- compileCObjectFile outn outobj
| Nothing => pure Nothing
compileCFile outobj outexec
cc <- coreLift findCC
dirs <- getDirs
let runccobj = cc ++ " -c " ++ outn ++ " -o " ++ outobj ++ " " ++
"-I" ++ fullprefix_dir dirs "refc " ++
"-I" ++ fullprefix_dir dirs "include"
let runcc = cc ++ " " ++ outobj ++ " -o " ++ outexec ++ " " ++
fullprefix_dir dirs "lib" </> "libidris2_support.a" ++ " " ++
"-lidris2_refc " ++
"-L" ++ fullprefix_dir dirs "refc " ++
clibdirs (lib_dirs dirs)
coreLift $ putStrLn runccobj
0 <- coreLift $ system runccobj
| _ => pure Nothing
coreLift $ putStrLn runcc
0 <- coreLift $ system runcc
| _ => pure Nothing
pure (Just outexec)
where
fullprefix_dir : Dirs -> String -> String
fullprefix_dir dirs sub
= prefix_dir dirs </> "idris2-" ++ showVersion False version </> sub
clibdirs : List String -> String
clibdirs ds = concat (map (\d => "-L" ++ d ++ " ") ds)
compileExpr _ _ _ _ _ _ = pure Nothing
export

View File

@ -78,8 +78,12 @@ schHeader chez libs
showSep "\n" (map (\x => "(load-shared-object \"" ++ escapeString x ++ "\")") libs) ++ "\n\n" ++
"(let ()\n"
schFooter : String
schFooter = "(collect 4)\n(blodwen-run-finalisers))\n"
schFooter : Bool -> String
schFooter prof
= "(collect 4)\n(blodwen-run-finalisers)\n" ++
if prof
then "(profile-dump-html))\n"
else ")\n"
showChezChar : Char -> String -> String
showChezChar '\\' = ("\\\\" ++)
@ -379,8 +383,8 @@ startChezWinSh chez appdir target = unlines
||| Compile a TT expression to Chez Scheme
compileToSS : Ref Ctxt Defs ->
String -> ClosedTerm -> (outfile : String) -> Core ()
compileToSS c appdir tm outfile
Bool -> String -> ClosedTerm -> (outfile : String) -> Core ()
compileToSS c prof appdir tm outfile
= do ds <- getDirectives Chez
libs <- findLibs ds
traverse_ copyLib libs
@ -402,7 +406,7 @@ compileToSS c appdir tm outfile
support ++ extraRuntime ++ code ++
concat (map fst fgndefs) ++
"(collect-request-handler (lambda () (collect) (blodwen-run-finalisers)))\n" ++
main ++ schFooter
main ++ schFooter prof
Right () <- coreLift $ writeFile outfile scm
| Left err => throw (FileErr outfile err)
coreLift_ $ chmodRaw outfile 0o755
@ -410,10 +414,13 @@ compileToSS c appdir tm outfile
||| Compile a Chez Scheme source file to an executable, daringly with runtime checks off.
compileToSO : {auto c : Ref Ctxt Defs} ->
String -> (appDirRel : String) -> (outSsAbs : String) -> Core ()
compileToSO chez appDirRel outSsAbs
Bool -> String -> (appDirRel : String) -> (outSsAbs : String) -> Core ()
compileToSO prof chez appDirRel outSsAbs
= do let tmpFileAbs = appDirRel </> "compileChez"
let build = "(parameterize ([optimize-level 3] [compile-file-message #f]) (compile-program " ++
let build = "(parameterize ([optimize-level 3] "
++ (if prof then "[compile-profile #t] "
else "") ++
"[compile-file-message #f]) (compile-program " ++
show outSsAbs ++ "))"
Right () <- coreLift $ writeFile tmpFileAbs build
| Left err => throw (FileErr tmpFileAbs err)
@ -451,8 +458,9 @@ compileExpr makeitso c tmpDir outputDir tm outfile
let outSsAbs = cwd </> outputDir </> outSsFile
let outSoAbs = cwd </> outputDir </> outSoFile
chez <- coreLift $ findChez
compileToSS c appDirGen tm outSsAbs
logTime "Make SO" $ when makeitso $ compileToSO chez appDirGen outSsAbs
let prof = profile !getSession
compileToSS c (makeitso && prof) appDirGen tm outSsAbs
logTime "++ Make SO" $ when makeitso $ compileToSO prof chez appDirGen outSsAbs
let outShRel = outputDir </> outfile
if isWindows
then makeShWindows chez outShRel appDirRel (if makeitso then outSoFile else outSsFile)

View File

@ -57,41 +57,63 @@ op o args = "(" ++ o ++ " " ++ showSep " " args ++ ")"
boolop : String -> List String -> String
boolop o args = "(or (and " ++ op o args ++ " 1) 0)"
add : Maybe IntKind -> String -> String -> String
add (Just $ Signed $ P n) x y = op "b+" [x, y, show (n-1)]
add (Just $ Unsigned $ P n) x y = op "b+" [x, y, show n]
add _ x y = op "+" [x, y]
sub : Maybe IntKind -> String -> String -> String
sub (Just $ Signed $ P n) x y = op "b-" [x, y, show (n-1)]
sub (Just $ Unsigned $ P n) x y = op "b-" [x, y, show n]
sub _ x y = op "-" [x, y]
mul : Maybe IntKind -> String -> String -> String
mul (Just $ Signed $ P n) x y = op "b*" [x, y, show (n-1)]
mul (Just $ Unsigned $ P n) x y = op "b*" [x, y, show n]
mul _ x y = op "*" [x, y]
div : Maybe IntKind -> String -> String -> String
div (Just $ Signed Unlimited) x y = op "quotient" [x, y]
div (Just $ Signed $ P n) x y = op "b/" [x, y, show (n-1)]
div (Just $ Unsigned $ P n) x y = op "b/" [x, y, show n]
div _ x y = op "/" [x, y]
shl : Maybe IntKind -> String -> String -> String
shl (Just $ Signed $ P n) x y = op "blodwen-bits-shl-signed"
[x, y, show (n-1)]
shl (Just $ Unsigned $ P n) x y = op "blodwen-bits-shl" [x, y, show n]
shl _ x y = op "blodwen-shl" [x, y]
castInt : Constant -> Constant -> String -> String
castInt from to x =
case (intKind from, intKind to) of
(Just _, Just $ Signed Unlimited) => x
(Just $ Signed m, Just $ Signed $ P n) =>
if P n >= m then x else op "blodwen-toSignedInt" [x,show (n-1)]
-- Only if the precision of the target is greater
-- than the one of the source, there is no need to cast.
(Just $ Unsigned m, Just $ Signed $ P n) =>
if P n > m then x else op "blodwen-toSignedInt" [x,show (n-1)]
(Just $ Signed _, Just $ Unsigned $ P n) =>
op "blodwen-toUnsignedInt" [x,show n]
(Just $ Unsigned m, Just $ Unsigned $ P n) =>
if P n >= m then x else op "blodwen-toUnsignedInt" [x,show n]
_ => "(blodwen-error-quit \"Invalid cast " ++ show from ++ "->" ++ show to ++ "\")"
||| Generate scheme for a primitive function.
schOp : PrimFn arity -> Vect arity String -> String
schOp (Add IntType) [x, y] = op "b+" [x, y, "63"]
schOp (Sub IntType) [x, y] = op "b-" [x, y, "63"]
schOp (Mul IntType) [x, y] = op "b*" [x, y, "63"]
schOp (Div IntType) [x, y] = op "b/" [x, y, "63"]
schOp (Add Bits8Type) [x, y] = op "b+" [x, y, "8"]
schOp (Sub Bits8Type) [x, y] = op "b-" [x, y, "8"]
schOp (Mul Bits8Type) [x, y] = op "b*" [x, y, "8"]
schOp (Div Bits8Type) [x, y] = op "b/" [x, y, "8"]
schOp (Add Bits16Type) [x, y] = op "b+" [x, y, "16"]
schOp (Sub Bits16Type) [x, y] = op "b-" [x, y, "16"]
schOp (Mul Bits16Type) [x, y] = op "b*" [x, y, "16"]
schOp (Div Bits16Type) [x, y] = op "b/" [x, y, "16"]
schOp (Add Bits32Type) [x, y] = op "b+" [x, y, "32"]
schOp (Sub Bits32Type) [x, y] = op "b-" [x, y, "32"]
schOp (Mul Bits32Type) [x, y] = op "b*" [x, y, "32"]
schOp (Div Bits32Type) [x, y] = op "b/" [x, y, "32"]
schOp (Add Bits64Type) [x, y] = op "b+" [x, y, "64"]
schOp (Sub Bits64Type) [x, y] = op "b-" [x, y, "64"]
schOp (Mul Bits64Type) [x, y] = op "b*" [x, y, "64"]
schOp (Div Bits64Type) [x, y] = op "b/" [x, y, "64"]
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 (Add ty) [x, y] = add (intKind ty) x y
schOp (Sub ty) [x, y] = sub (intKind ty) x y
schOp (Mul ty) [x, y] = mul (intKind ty) x y
schOp (Div ty) [x, y] = div (intKind ty) x y
schOp (Mod ty) [x, y] = op "remainder" [x, y]
schOp (Neg ty) [x] = op "-" [x]
schOp (ShiftL IntType) [x, y] = op "blodwen-bits-shl-signed" [x, y, "63"]
schOp (ShiftL Bits8Type) [x, y] = op "blodwen-bits-shl" [x, y, "8"]
schOp (ShiftL Bits16Type) [x, y] = op "blodwen-bits-shl" [x, y, "16"]
schOp (ShiftL Bits32Type) [x, y] = op "blodwen-bits-shl" [x, y, "32"]
schOp (ShiftL Bits64Type) [x, y] = op "blodwen-bits-shl" [x, y, "64"]
schOp (ShiftL ty) [x, y] = op "blodwen-shl" [x, y]
schOp (ShiftL ty) [x, y] = shl (intKind ty) x y
schOp (ShiftR ty) [x, y] = op "blodwen-shr" [x, y]
schOp (BAnd ty) [x, y] = op "blodwen-and" [x, y]
schOp (BOr ty) [x, y] = op "blodwen-or" [x, y]
@ -133,67 +155,25 @@ schOp DoubleSqrt [x] = op "flsqrt" [x]
schOp DoubleFloor [x] = op "flfloor" [x]
schOp DoubleCeiling [x] = op "flceiling" [x]
schOp (Cast IntType StringType) [x] = op "number->string" [x]
schOp (Cast IntegerType StringType) [x] = op "number->string" [x]
schOp (Cast Bits8Type StringType) [x] = op "number->string" [x]
schOp (Cast Bits16Type StringType) [x] = op "number->string" [x]
schOp (Cast Bits32Type StringType) [x] = op "number->string" [x]
schOp (Cast Bits64Type StringType) [x] = op "number->string" [x]
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 Bits8Type IntegerType) [x] = x
schOp (Cast Bits16Type IntegerType) [x] = x
schOp (Cast Bits32Type IntegerType) [x] = x
schOp (Cast Bits64Type IntegerType) [x] = x
schOp (Cast Bits16Type StringType) [x] = op "number->string" [x]
schOp (Cast Bits32Type StringType) [x] = op "number->string" [x]
schOp (Cast Bits64Type StringType) [x] = op "number->string" [x]
schOp (Cast Bits8Type StringType) [x] = op "number->string" [x]
schOp (Cast CharType IntType) [x] = op "char->integer" [x]
schOp (Cast CharType IntegerType) [x] = op "char->integer" [x]
schOp (Cast CharType StringType) [x] = op "string" [x]
schOp (Cast DoubleType IntType) [x] = op "exact-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 Bits8Type IntType) [x] = x
schOp (Cast Bits16Type IntType) [x] = x
schOp (Cast Bits32Type IntType) [x] = x
schOp (Cast Bits64Type IntType) [x] = 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]
schOp (Cast IntType Bits8Type) [x] = op "integer->bits8" [x]
schOp (Cast IntType Bits16Type) [x] = op "integer->bits16" [x]
schOp (Cast IntType Bits32Type) [x] = op "integer->bits32" [x]
schOp (Cast IntType Bits64Type) [x] = op "integer->bits64" [x]
schOp (Cast IntegerType Bits8Type) [x] = op "integer->bits8" [x]
schOp (Cast IntegerType Bits16Type) [x] = op "integer->bits16" [x]
schOp (Cast IntegerType Bits32Type) [x] = op "integer->bits32" [x]
schOp (Cast IntegerType Bits64Type) [x] = op "integer->bits64" [x]
schOp (Cast Bits8Type Bits16Type) [x] = x
schOp (Cast Bits8Type Bits32Type) [x] = x
schOp (Cast Bits8Type Bits64Type) [x] = x
schOp (Cast Bits16Type Bits8Type) [x] = op "bits16->bits8" [x]
schOp (Cast Bits16Type Bits32Type) [x] = x
schOp (Cast Bits16Type Bits64Type) [x] = x
schOp (Cast Bits32Type Bits8Type) [x] = op "bits32->bits8" [x]
schOp (Cast Bits32Type Bits16Type) [x] = op "bits32->bits16" [x]
schOp (Cast Bits32Type Bits64Type) [x] = x
schOp (Cast Bits64Type Bits8Type) [x] = op "bits64->bits8" [x]
schOp (Cast Bits64Type Bits16Type) [x] = op "bits64->bits16" [x]
schOp (Cast Bits64Type Bits32Type) [x] = op "bits64->bits32" [x]
schOp (Cast DoubleType StringType) [x] = op "number->string" [x]
schOp (Cast IntType CharType) [x] = op "cast-int-char" [x]
schOp (Cast IntType DoubleType) [x] = op "exact->inexact" [x]
schOp (Cast IntType StringType) [x] = op "number->string" [x]
schOp (Cast IntegerType DoubleType) [x] = op "exact->inexact" [x]
schOp (Cast IntType DoubleType) [x] = op "exact->inexact" [x]
schOp (Cast StringType DoubleType) [x] = op "cast-string-double" [x]
schOp (Cast IntType CharType) [x] = op "cast-int-char" [x]
schOp (Cast from to) [x] = "(blodwen-error-quit \"Invalid cast " ++ show from ++ "->" ++ show to ++ "\")"
schOp (Cast IntegerType StringType) [x] = op "number->string" [x]
schOp (Cast StringType DoubleType) [x] = op "cast-string-double" [x]
schOp (Cast StringType IntType) [x] = op "cast-string-int" [x]
schOp (Cast StringType IntegerType) [x] = op "cast-string-int" [x]
schOp (Cast from to) [x] = castInt from to x
schOp BelieveMe [_,_,x] = x
schOp Crash [_,msg] = "(blodwen-error-quit (string-append \"ERROR: \" " ++ msg ++ "))"

View File

@ -40,8 +40,8 @@ findRacoExe =
do env <- idrisGetEnv "RACKET_RACO"
pure $ (fromMaybe "/usr/bin/env raco" env) ++ " exe"
schHeader : String -> String
schHeader libs
schHeader : Bool -> String -> String
schHeader prof libs
= "#lang racket/base\n" ++
"; @generated\n" ++
"(require racket/async-channel)\n" ++ -- for asynchronous channels
@ -52,6 +52,7 @@ schHeader libs
"(require rnrs/io/ports-6)\n" ++ -- for files
"(require srfi/19)\n" ++ -- for file handling and data
"(require ffi/unsafe ffi/unsafe/define)\n" ++ -- for calling C
(if prof then "(require profile)\n" else "") ++
"(require racket/flonum)" ++ -- for float-typed transcendental functions
libs ++
"(let ()\n"
@ -386,10 +387,14 @@ compileToRKT c appdir tm outfile
support <- readDataFile "racket/support.rkt"
ds <- getDirectives Racket
extraRuntime <- getExtraRuntime ds
let scm = schHeader (concat (map fst fgndefs)) ++
let prof = profile !getSession
let runmain
= if prof
then "(profile (void " ++ main ++ ") #:order 'self)\n"
else "(void " ++ main ++ ")\n"
let scm = schHeader prof (concat (map fst fgndefs)) ++
support ++ extraRuntime ++ code ++
"(void " ++ main ++ ")\n" ++
schFooter
runmain ++ schFooter
Right () <- coreLift $ writeFile outfile scm
| Left err => throw (FileErr outfile err)
coreLift_ $ chmodRaw outfile 0o755
@ -431,7 +436,7 @@ compileExpr mkexec c tmpDir outputDir tm outfile
racket <- coreLift findRacket
ok <- the (Core Int) $ if mkexec
then logTime "Build racket" $
then logTime "+ Build racket" $
coreLift $
system (raco ++ " -o " ++ outBinAbs ++ " " ++ outRktAbs)
else pure 0

View File

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

View File

@ -59,6 +59,10 @@ mutual
measureAlts (ConstCase x y) = 1 + (measure y)
measureAlts (DefaultCase x) = 1 + (measure x)
isDefault : CaseAlt vars -> Bool
isDefault (DefaultCase _) = True
isDefault _ = False
public export
data Pat : Type where
PAs : FC -> Name -> Pat -> Pat

View File

@ -645,6 +645,61 @@ data Transform : Type where
Name -> -- name for identifying the rule
Env Term vars -> Term vars -> Term vars -> Transform
||| Types that are transformed into a faster representation
||| during codegen.
public export
data BuiltinType : Type where
||| A built-in 'Nat'-like type
||| 'NatLike : [index ->] Type'
||| 'SLike : {0 _ : index} -> NatLike [index] -> NatLike [f index]'
||| 'ZLike : {0 _ : index} -> NatLike [index]'
BuiltinNatural : BuiltinType
-- All the following aren't implemented yet
-- but are here to reduce number of TTC version changes
NaturalPlus : BuiltinType
NaturalMult : BuiltinType
NaturalToInteger : BuiltinType
IntegerToNatural : BuiltinType
export
Show BuiltinType where
show BuiltinNatural = "Natural"
show _ = "Not yet implemented"
-- Token types to make it harder to get the constructor names
-- the wrong way round.
public export data ZERO = MkZERO
public export data SUCC = MkSUCC
||| Record containing names of 'Nat'-like constructors.
public export
record NatBuiltin where
constructor MkNatBuiltin
zero : Name
succ : Name
||| Rewrite rules for %builtin pragmas
||| Seperate to 'Transform' because it must also modify case statements
||| behaviour should remain the same after this transform
public export
record BuiltinTransforms where
constructor MkBuiltinTransforms
natTyNames : NameMap NatBuiltin -- map from Nat-like names to their constructors
natZNames : NameMap ZERO -- map from Z-like names to their type constructor
natSNames : NameMap SUCC -- map from S-like names to their type constructor
-- TODO: After next release remove nat from here and use %builtin pragma instead
initBuiltinTransforms : BuiltinTransforms
initBuiltinTransforms =
let type = NS typesNS (UN "Nat")
zero = NS typesNS (UN "Z")
succ = NS typesNS (UN "S")
in MkBuiltinTransforms
{ natTyNames = singleton type (MkNatBuiltin {zero, succ})
, natZNames = singleton zero MkZERO
, natSNames = singleton succ MkSUCC
}
export
getFnName : Transform -> Maybe Name
getFnName (MkTransform _ _ app _)
@ -987,6 +1042,10 @@ record Defs where
-- ^ A mapping from names to transformation rules which update applications
-- of that name
saveTransforms : List (Name, Transform)
builtinTransforms : BuiltinTransforms
-- ^ A mapping from names to transformations resulting from a %builtin pragma
-- seperate to `transforms` because these must always fire globally so run these
-- when compiling to `CExp`.
namedirectives : NameMap (List String)
ifaceHash : Int
importHashes : List (Namespace, Int)
@ -1046,6 +1105,7 @@ initDefs
, saveAutoHints = []
, transforms = empty
, saveTransforms = []
, builtinTransforms = initBuiltinTransforms
, namedirectives = empty
, ifaceHash = 5381
, importHashes = []
@ -1938,6 +1998,20 @@ extendNS ns
= do defs <- get Ctxt
put Ctxt (record { currentNS $= (<.> ns) } defs)
export
withExtendedNS : {auto c : Ref Ctxt Defs} ->
Namespace -> Core a -> Core a
withExtendedNS ns act
= do defs <- get Ctxt
let cns = currentNS defs
put Ctxt (record { currentNS = cns <.> ns } defs)
ma <- catch (Right <$> act) (pure . Left)
defs <- get Ctxt
put Ctxt (record { currentNS = cns } defs)
case ma of
Left err => throw err
Right a => pure a
-- Get the name as it would be defined in the current namespace
-- i.e. if it doesn't have an explicit namespace already, add it,
-- otherwise leave it alone
@ -2143,6 +2217,14 @@ getWorkingDir
| Nothing => throw (InternalError "Can't get current directory")
pure d
export
withCtxt : {auto c : Ref Ctxt Defs} -> Core a -> Core a
withCtxt = wrapRef Ctxt resetCtxt
where
resetCtxt : Defs -> Core ()
resetCtxt defs = do let dir = defs.options.dirs.working_dir
coreLift_ $ changeDir dir
export
setPrefix : {auto c : Ref Ctxt Defs} -> String -> Core ()
setPrefix dir
@ -2397,8 +2479,10 @@ addLogLevel : {auto c : Ref Ctxt Defs} ->
addLogLevel lvl
= do defs <- get Ctxt
case lvl of
Nothing => put Ctxt (record { options->session->logLevel = defaultLogLevel } defs)
Just l => put Ctxt (record { options->session->logLevel $= insertLogLevel l } defs)
Nothing => put Ctxt (record { options->session->logEnabled = True,
options->session->logLevel = defaultLogLevel } defs)
Just l => put Ctxt (record { options->session->logEnabled = True,
options->session->logLevel $= insertLogLevel l } defs)
export
withLogLevel : {auto c : Ref Ctxt Defs} ->

View File

@ -16,8 +16,8 @@ logTerm : {vars : _} ->
String -> Nat -> Lazy String -> Term vars -> Core ()
logTerm str n msg tm
= do opts <- getSession
let lvl = mkLogLevel str n
if keepLog lvl (logLevel opts)
let lvl = mkLogLevel (logEnabled opts) str n
if keepLog lvl (logEnabled opts) (logLevel opts)
then do tm' <- toFullNames tm
coreLift $ putStrLn $ "LOG " ++ show lvl ++ ": " ++ msg
++ ": " ++ show tm'
@ -27,7 +27,7 @@ log' : {auto c : Ref Ctxt Defs} ->
LogLevel -> Lazy String -> Core ()
log' lvl msg
= do opts <- getSession
if keepLog lvl (logLevel opts)
if keepLog lvl (logEnabled opts) (logLevel opts)
then coreLift $ putStrLn $ "LOG " ++ show lvl ++ ": " ++ msg
else pure ()
@ -37,7 +37,7 @@ export
log : {auto c : Ref Ctxt Defs} ->
String -> Nat -> Lazy String -> Core ()
log str n msg
= do let lvl = mkLogLevel str n
= do let lvl = mkLogLevel (logEnabled !getSession) str n
log' lvl msg
export
@ -45,8 +45,8 @@ logC : {auto c : Ref Ctxt Defs} ->
String -> Nat -> Core String -> Core ()
logC str n cmsg
= do opts <- getSession
let lvl = mkLogLevel str n
if keepLog lvl (logLevel opts)
let lvl = mkLogLevel (logEnabled opts) str n
if keepLog lvl (logEnabled opts) (logLevel opts)
then do msg <- cmsg
coreLift $ putStrLn $ "LOG " ++ show lvl ++ ": " ++ msg
else pure ()

View File

@ -492,6 +492,18 @@ export %inline
(=<<) : (a -> Core b) -> Core a -> Core b
(=<<) = flip (>>=)
-- Kleisli compose
infixr 1 >=>
export %inline
(>=>) : (a -> Core b) -> (b -> Core c) -> (a -> Core c)
f >=> g = (g =<<) . f
-- Flipped kleisli compose
infixr 1 <=<
export %inline
(<=<) : (b -> Core c) -> (a -> Core b) -> (a -> Core c)
(<=<) = flip (>=>)
-- Applicative (specialised)
export %inline
pure : a -> Core a
@ -554,6 +566,11 @@ Catchable Core Error where
Right val => pure (Right val))
throw = coreFail
-- Prelude.Monad.foldlM hand specialised for Core
export
foldlC : Foldable t => (a -> b -> Core a) -> a -> t b -> Core a
foldlC fm a0 = foldl (\ma,b => ma >>= flip fm b) (pure a0)
-- Traversable (specialised)
traverse' : (a -> Core b) -> List a -> List b -> Core (List b)
traverse' f [] acc = pure (reverse acc)
@ -705,6 +722,21 @@ update x f
= do v <- get x
put x (f v)
export
wrapRef : (x : label) -> {auto ref : Ref x a} ->
(a -> Core ()) ->
Core b ->
Core b
wrapRef x onClose op
= do v <- get x
o <- catch op $ \err =>
do onClose v
put x v
throw err
onClose v
put x v
pure o
export
cond : List (Lazy Bool, Lazy a) -> a -> a
cond [] def = def

View File

@ -165,7 +165,7 @@ getCons defs (NTCon _ tn _ _ _)
Just (TCon _ _ _ _ _ _ cons _) =>
do cs' <- traverse addTy cons
pure (mapMaybe id cs')
_ => pure []
_ => throw (InternalError "Called `getCons` on something that is not a Type constructor")
where
addTy : Name -> Core (Maybe (NF [], Name, Int, Nat))
addTy cn
@ -214,24 +214,22 @@ getMissingAlts fc defs (NPrimVal _ WorldType) alts
then pure [DefaultCase (Unmatched "Coverage check")]
else pure []
getMissingAlts fc defs (NPrimVal _ c) alts
= if any isDefault alts
then pure []
= do log "coverage.missing" 50 $ "Looking for missing alts at type " ++ show c
if any isDefault alts
then do log "coverage.missing" 20 "Found default"
pure []
else pure [DefaultCase (Unmatched "Coverage check")]
where
isDefault : CaseAlt vars -> Bool
isDefault (DefaultCase _) = True
isDefault _ = False
-- Similarly for types
getMissingAlts fc defs (NType _) alts
= if any isDefault alts
then pure []
else pure [DefaultCase (Unmatched "Coverage check")]
where
isDefault : CaseAlt vars -> Bool
isDefault (DefaultCase _) = True
isDefault _ = False
= do log "coverage.missing" 50 "Looking for missing alts at type Type"
if any isDefault alts
then do log "coverage.missing" 20 "Found default"
pure []
else pure [DefaultCase (Unmatched "Coverage check")]
getMissingAlts fc defs nfty alts
= do allCons <- getCons defs nfty
= do log "coverage.missing" 50 $ "Getting constructors for: " ++ show nfty
logNF "coverage.missing" 20 "Getting constructors for" (mkEnv fc _) nfty
allCons <- getCons defs nfty
pure (filter (noneOf alts)
(map (mkAlt fc (Unmatched "Coverage check") . snd) allCons))
where
@ -396,12 +394,13 @@ getMissing : {vars : _} ->
getMissing fc n ctree
= do defs <- get Ctxt
let psIn = map (Ref fc Bound) vars
pats <- buildArgs fc defs [] [] psIn ctree
logC "coverage.missing" 20 $ map unlines $
flip traverse (concat pats) $ \ pat =>
do pat' <- toFullNames pat
pure (show pat')
pure (map (apply fc (Ref fc Func n)) pats)
patss <- buildArgs fc defs [] [] psIn ctree
let pats = concat patss
unless (null pats) $
logC "coverage.missing" 20 $ map unlines $
flip traverse pats $ \ pat =>
show <$> toFullNames pat
pure (map (apply fc (Ref fc Func n)) patss)
-- For the given name, get the names it refers to which are not themselves
-- covering.

View File

@ -12,6 +12,7 @@ import Core.TTC
import Data.List
import System.File
import Libraries.Data.PosMap
import Libraries.Utils.Binary
%default covering
@ -41,15 +42,17 @@ record Metadata where
-- to know what the recursive call is, if applicable)
currentLHS : Maybe ClosedTerm
holeLHS : List (Name, ClosedTerm)
nameLocMap : PosMap (NonEmptyFC, Name)
Show Metadata where
show (MkMetadata apps names tydecls currentLHS holeLHS)
show (MkMetadata apps names tydecls currentLHS holeLHS nameLocMap)
= "Metadata:\n" ++
" lhsApps: " ++ show apps ++ "\n" ++
" names: " ++ show names ++ "\n" ++
" type declarations: " ++ show tydecls ++ "\n" ++
" current LHS: " ++ show currentLHS ++ "\n" ++
" holes: " ++ show holeLHS
" holes: " ++ show holeLHS ++ "\n" ++
" nameLocMap: " ++ show nameLocMap
export
initMetadata : Metadata
@ -59,6 +62,7 @@ initMetadata = MkMetadata
, tydecls = []
, currentLHS = Nothing
, holeLHS = []
, nameLocMap = empty
}
-- A label for metadata in the global state
@ -71,13 +75,15 @@ TTC Metadata where
toBuf b (names m)
toBuf b (tydecls m)
toBuf b (holeLHS m)
toBuf b (nameLocMap m)
fromBuf b
= do apps <- fromBuf b
ns <- fromBuf b
tys <- fromBuf b
hlhs <- fromBuf b
pure (MkMetadata apps ns tys Nothing hlhs)
dlocs <- fromBuf b
pure (MkMetadata apps ns tys Nothing hlhs dlocs)
export
addLHS : {vars : _} ->
@ -138,6 +144,16 @@ addTyDecl loc n env tm
whenJust (isNonEmptyFC loc) $ \ neloc =>
put MD $ record { tydecls $= ( (neloc, (n', length env, bindEnv loc env tm)) ::) } meta
export
addNameLoc : {auto m : Ref MD Metadata} ->
{auto c : Ref Ctxt Defs} ->
FC -> Name -> Core ()
addNameLoc loc n
= do meta <- get MD
n' <- getFullName n
whenJust (isNonEmptyFC loc) $ \neloc =>
put MD $ record { nameLocMap $= insert (neloc, n') } meta
export
setHoleLHS : {auto m : Ref MD Metadata} ->
ClosedTerm -> Core ()
@ -233,12 +249,13 @@ TTC TTMFile where
pure (MkTTMFile ver md)
HasNames Metadata where
full gam (MkMetadata lhs ns tys clhs hlhs)
full gam (MkMetadata lhs ns tys clhs hlhs dlocs)
= pure $ MkMetadata !(traverse fullLHS lhs)
!(traverse fullTy ns)
!(traverse fullTy tys)
Nothing
!(traverse fullHLHS hlhs)
(fromList !(traverse fullDecls (toList dlocs)))
where
fullLHS : (NonEmptyFC, (Nat, ClosedTerm)) -> Core (NonEmptyFC, (Nat, ClosedTerm))
fullLHS (fc, (i, tm)) = pure (fc, (i, !(full gam tm)))
@ -249,12 +266,16 @@ HasNames Metadata where
fullHLHS : (Name, ClosedTerm) -> Core (Name, ClosedTerm)
fullHLHS (n, tm) = pure (!(full gam n), !(full gam tm))
resolved gam (MkMetadata lhs ns tys clhs hlhs)
fullDecls : (NonEmptyFC, Name) -> Core (NonEmptyFC, Name)
fullDecls (fc, n) = pure (fc, !(full gam n))
resolved gam (MkMetadata lhs ns tys clhs hlhs dlocs)
= pure $ MkMetadata !(traverse resolvedLHS lhs)
!(traverse resolvedTy ns)
!(traverse resolvedTy tys)
Nothing
!(traverse resolvedHLHS hlhs)
(fromList !(traverse resolvedDecls (toList dlocs)))
where
resolvedLHS : (NonEmptyFC, (Nat, ClosedTerm)) -> Core (NonEmptyFC, (Nat, ClosedTerm))
resolvedLHS (fc, (i, tm)) = pure (fc, (i, !(resolved gam tm)))
@ -265,6 +286,9 @@ HasNames Metadata where
resolvedHLHS : (Name, ClosedTerm) -> Core (Name, ClosedTerm)
resolvedHLHS (n, tm) = pure (!(resolved gam n), !(resolved gam tm))
resolvedDecls : (NonEmptyFC, Name) -> Core (NonEmptyFC, Name)
resolvedDecls (fc, n) = pure (fc, !(resolved gam n))
export
writeToTTM : {auto c : Ref Ctxt Defs} ->
{auto m : Ref MD Metadata} ->

View File

@ -238,6 +238,10 @@ export
preludeNS : Namespace
preludeNS = mkNamespace "Prelude"
export
numNS : Namespace
numNS = mkNamespace "Prelude.Num"
export
typesNS : Namespace
typesNS = mkNamespace "Prelude.Types"

View File

@ -219,6 +219,9 @@ parameters (defs : Defs, topopts : EvalOpts)
= evalRef env True fc Func (Resolved i) (map (EmptyFC,) args ++ stk)
(NApp fc (NMeta nm i args) stk)
-- The commented out logging here might still be useful one day, but
-- evalRef is used a lot and even these tiny checks turn out to be
-- worth skipping if we can
evalRef : {auto c : Ref Ctxt Defs} ->
{free : _} ->
Env Term free ->
@ -226,20 +229,31 @@ parameters (defs : Defs, topopts : EvalOpts)
FC -> NameType -> Name -> Stack free -> (def : Lazy (NF free)) ->
Core (NF free)
evalRef env meta fc (DataCon tag arity) fn stk def
= pure $ NDCon fc fn tag arity stk
= do -- logC "eval.ref.data" 50 $ do fn' <- toFullNames fn -- Can't use ! here, it gets lifted too far
-- pure $ "Found data constructor: " ++ show fn'
pure $ NDCon fc fn tag arity stk
evalRef env meta fc (TyCon tag arity) fn stk def
= pure $ NTCon fc fn tag arity stk
= do -- logC "eval.ref.type" 50 $ do fn' <- toFullNames fn
-- pure $ "Found type constructor: " ++ show fn'
pure $ ntCon fc fn tag arity stk
evalRef env meta fc Bound fn stk def
= pure def
= do -- logC "eval.ref.bound" 50 $ do fn' <- toFullNames fn
-- pure $ "Found bound variable: " ++ show fn'
pure def
evalRef env meta fc nt@Func n stk def
= do Just res <- lookupCtxtExact n (gamma defs)
= do -- logC "eval.ref.func" 50 $ do n' <- toFullNames n
-- pure $ "Found function: " ++ show n'
Just res <- lookupCtxtExact n (gamma defs)
| Nothing => pure def
let redok1 = evalAll topopts
let redok2 = reducibleInAny (currentNS defs :: nestedNS defs)
(fullname res)
(visibility res)
-- want to shortcut that second check, if we're evaluating
-- everything, so don't let bind unless we need that log!
let redok = redok1 || redok2
unless redok2 $ logC "eval.stuck" 5 $ pure $ "Stuck function: " ++ show !(toFullNames n)
unless redok2 $ logC "eval.stuck" 5 $ do n' <- toFullNames n
pure $ "Stuck function: " ++ show n'
if redok
then do
Just opts' <- useMeta (noCycles res) fc n defs topopts
@ -1162,8 +1176,8 @@ logNF : {vars : _} ->
String -> Nat -> Lazy String -> Env Term vars -> NF vars -> Core ()
logNF str n msg env tmnf
= do opts <- getSession
let lvl = mkLogLevel str n
when (keepLog lvl (logLevel opts)) $
let lvl = mkLogLevel (logEnabled opts) str n
when (keepLog lvl (logEnabled opts) (logLevel opts)) $
do defs <- get Ctxt
tm <- quote defs env tmnf
tm' <- toFullNames tm
@ -1178,7 +1192,7 @@ logTermNF' : {vars : _} ->
LogLevel -> Lazy String -> Env Term vars -> Term vars -> Core ()
logTermNF' lvl msg env tm
= do opts <- getSession
when (keepLog lvl (logLevel opts)) $
when (keepLog lvl (logEnabled opts) (logLevel opts)) $
do defs <- get Ctxt
tmnf <- normaliseHoles defs env tm
tm' <- toFullNames tmnf
@ -1190,7 +1204,7 @@ logTermNF : {vars : _} ->
{auto c : Ref Ctxt Defs} ->
String -> Nat -> Lazy String -> Env Term vars -> Term vars -> Core ()
logTermNF str n msg env tm
= do let lvl = mkLogLevel str n
= do let lvl = mkLogLevel (logEnabled !getSession) str n
logTermNF' lvl msg env tm
export
@ -1199,8 +1213,8 @@ logGlue : {vars : _} ->
String -> Nat -> Lazy String -> Env Term vars -> Glued vars -> Core ()
logGlue str n msg env gtm
= do opts <- getSession
let lvl = mkLogLevel str n
when (keepLog lvl (logLevel opts)) $
let lvl = mkLogLevel (logEnabled opts) str n
when (keepLog lvl (logEnabled opts) (logLevel opts)) $
do defs <- get Ctxt
tm <- getTerm gtm
tm' <- toFullNames tm
@ -1213,8 +1227,8 @@ logGlueNF : {vars : _} ->
String -> Nat -> Lazy String -> Env Term vars -> Glued vars -> Core ()
logGlueNF str n msg env gtm
= do opts <- getSession
let lvl = mkLogLevel str n
when (keepLog lvl (logLevel opts)) $
let lvl = mkLogLevel (logEnabled opts) str n
when (keepLog lvl (logEnabled opts) (logLevel opts)) $
do defs <- get Ctxt
tm <- getTerm gtm
tmnf <- normaliseHoles defs env tm
@ -1228,13 +1242,14 @@ logEnv : {vars : _} ->
String -> Nat -> String -> Env Term vars -> Core ()
logEnv str n msg env
= do opts <- getSession
when (keepLog lvl (logLevel opts)) $ do
when (logEnabled opts &&
keepLog lvl (logEnabled opts) (logLevel opts)) $ do
coreLift (putStrLn $ "LOG " ++ show lvl ++ ": " ++ msg)
dumpEnv env
where
lvl : LogLevel
lvl = mkLogLevel str n
lvl = mkLogLevel True str n
dumpEnv : {vs : List Name} -> Env Term vs -> Core ()
dumpEnv [] = pure ()

View File

@ -141,6 +141,8 @@ record Session where
findipkg : Bool
codegen : CG
directives : List String
logEnabled : Bool -- do we check logging flags at all? This is 'False' until
-- any logging is enabled.
logLevel : LogLevels
logTimings : Bool
ignoreMissingPkg : Bool -- fail silently on missing packages. This is because
@ -151,6 +153,7 @@ record Session where
dumplifted : Maybe String -- file to output lambda lifted definitions
dumpanf : Maybe String -- file to output ANF definitions
dumpvmcode : Maybe String -- file to output VM code definitions
profile : Bool -- generate profiling information, if supported
public export
record PPrinter where
@ -196,9 +199,9 @@ defaultPPrint = MkPPOpts False True False
export
defaultSession : Session
defaultSession = MkSessionOpts False False False Chez [] defaultLogLevel
defaultSession = MkSessionOpts False False False Chez [] False defaultLogLevel
False False False Nothing Nothing
Nothing Nothing
Nothing Nothing False
export
defaultElab : ElabDirectives

View File

@ -50,9 +50,10 @@ mkLogLevel' ps n = MkLogLevel (maybe [] forget ps) n
||| list. This bypasses the fact that the function `split` returns a non-empty
||| list no matter what.
export
mkLogLevel : String -> Nat -> LogLevel
mkLogLevel "" = mkLogLevel' Nothing
mkLogLevel ps = mkLogLevel' (Just (split (== '.') ps))
mkLogLevel : Bool -> String -> Nat -> LogLevel
mkLogLevel False _ = mkLogLevel' Nothing
mkLogLevel _ "" = mkLogLevel' Nothing
mkLogLevel _ ps = mkLogLevel' (Just (split (== '.') ps))
||| The unsafe constructor should only be used in places where the topic has already
||| been appropriately processed.
@ -98,7 +99,7 @@ parseLogLevel str = do
ns = tail nns in
case ns of
[] => pure (MkLogLevel [], n)
[ns] => pure (mkLogLevel n, ns)
[ns] => pure (mkLogLevel True n, ns)
_ => Nothing
lvl <- parsePositive n
pure $ c (fromInteger lvl)
@ -127,8 +128,9 @@ insertLogLevel (MkLogLevel ps n) = insert ps n
||| We keep a log if there is a prefix of its path associated to a larger number
||| in the LogLevels.
export
keepLog : LogLevel -> LogLevels -> Bool
keepLog (MkLogLevel path n) levels = go path levels where
keepLog : LogLevel -> Bool -> LogLevels -> Bool
keepLog (MkLogLevel _ Z) _ _ = True
keepLog (MkLogLevel path n) enabled levels = enabled && go path levels where
go : List String -> StringTrie Nat -> Bool
go path (MkStringTrie current) = here || there where

View File

@ -54,6 +54,22 @@ data Constant
| DoubleType
| WorldType
export
isConstantType : Name -> Maybe Constant
isConstantType (UN n) = case n of
"Int" => Just IntType
"Integer" => Just IntegerType
"Bits8" => Just Bits8Type
"Bits16" => Just Bits16Type
"Bits32" => Just Bits32Type
"Bits64" => Just Bits64Type
"String" => Just StringType
"Char" => Just CharType
"Double" => Just DoubleType
"%World" => Just WorldType
_ => Nothing
isConstantType _ = Nothing
export
constantEq : (x, y : Constant) -> Maybe (x = y)
constantEq (I x) (I y) = case decEq x y of
@ -164,6 +180,36 @@ constTag DoubleType = 11
constTag WorldType = 12
constTag _ = 0
||| Precision of integral types.
public export
data Precision = P Int | Unlimited
export
Eq Precision where
(P m) == (P n) = m == n
Unlimited == Unlimited = True
_ == _ = False
export
Ord Precision where
compare (P m) (P n) = compare m n
compare Unlimited Unlimited = EQ
compare Unlimited _ = GT
compare _ Unlimited = LT
public export
data IntKind = Signed Precision | Unsigned Precision
public export
intKind : Constant -> Maybe IntKind
intKind IntegerType = Just $ Signed Unlimited
intKind IntType = Just . Signed $ P 64
intKind Bits8Type = Just . Unsigned $ P 8
intKind Bits16Type = Just . Unsigned $ P 16
intKind Bits32Type = Just . Unsigned $ P 32
intKind Bits64Type = Just . Unsigned $ P 64
intKind _ = Nothing
-- All the internal operators, parameterised by their arity
public export
data PrimFn : Nat -> Type where
@ -388,6 +434,20 @@ Functor PiInfo where
map func AutoImplicit = AutoImplicit
map func (DefImplicit t) = (DefImplicit (func t))
export
Foldable PiInfo where
foldr f acc Implicit = acc
foldr f acc Explicit = acc
foldr f acc AutoImplicit = acc
foldr f acc (DefImplicit x) = f x acc
export
Traversable PiInfo where
traverse f Implicit = pure Implicit
traverse f Explicit = pure Explicit
traverse f AutoImplicit = pure AutoImplicit
traverse f (DefImplicit x) = map DefImplicit (f x)
export
Functor Binder where
map func (Lam fc c x ty) = Lam fc c (map func x) (func ty)

View File

@ -11,6 +11,7 @@ import Core.Options
import Core.TT
import Libraries.Data.NameMap
import Libraries.Data.PosMap
import Data.Vect
import Libraries.Utils.Binary

View File

@ -663,9 +663,8 @@ dumpHole' : {auto u : Ref UST UState} ->
dumpHole' lvl hole
= do ust <- get UST
defs <- get Ctxt
if keepLog lvl (logLevel $ session $ options defs)
then pure ()
else do
sopts <- getSession
when (keepLog lvl (logEnabled sopts) (logLevel sopts)) $ do
defs <- get Ctxt
case !(lookupCtxtExact (Resolved hole) (gamma defs)) of
Nothing => pure ()
@ -725,8 +724,9 @@ dumpConstraints : {auto u : Ref UST UState} ->
dumpConstraints str n all
= do ust <- get UST
defs <- get Ctxt
let lvl = mkLogLevel str n
when (keepLog lvl (logLevel $ session $ options defs)) $
sopts <- getSession
let lvl = mkLogLevel (logEnabled sopts) str n
when (keepLog lvl (logEnabled sopts) (logLevel sopts)) $
do let hs = toList (guesses ust) ++
toList (if all then holes ust else currentHoles ust)
case hs of

View File

@ -91,6 +91,14 @@ mutual
NErased : FC -> (imp : Bool) -> NF vars
NType : FC -> NF vars
export
ntCon : FC -> Name -> Int -> Nat -> List (FC, Closure vars) -> NF vars
ntCon fc (UN "Type") tag Z [] = NType fc
ntCon fc n tag Z [] = case isConstantType n of
Just c => NPrimVal fc c
Nothing => NTCon fc n tag Z []
ntCon fc n tag arity args = NTCon fc n tag arity args
export
getLoc : NF vars -> FC
getLoc (NBind fc _ _ _) = fc

View File

@ -9,6 +9,7 @@ import Core.Name.Namespace
import Core.Options
import Data.List
import Data.List1
import Data.Maybe
import Data.Strings
import Data.Either
@ -21,17 +22,21 @@ public export
data PkgCommand
= Build
| Install
| MkDoc
| Typecheck
| Clean
| REPL
| Init
export
Show PkgCommand where
show Build = "--build"
show Install = "--install"
show MkDoc = "--mkdoc"
show Typecheck = "--typecheck"
show Clean = "--clean"
show REPL = "--repl"
show Init = "--init"
public export
data DirCommand
@ -41,62 +46,6 @@ export
Show DirCommand where
show LibDir = "--libdir"
public export
data PkgVersion = MkPkgVersion (List Nat)
export
Show PkgVersion where
show (MkPkgVersion vs) = showSep "." (map show vs)
export
Eq PkgVersion where
MkPkgVersion p == MkPkgVersion q = p == q
export
Ord PkgVersion where
-- list ordering gives us what we want
compare (MkPkgVersion p) (MkPkgVersion q) = compare p q
-- version must be >= lowerBound and <= upperBound
-- Do we want < and > as well?
public export
record PkgVersionBounds where
constructor MkPkgVersionBounds
lowerBound : Maybe PkgVersion
lowerInclusive : Bool -- >= if true
upperBound : Maybe PkgVersion
upperInclusive : Bool -- <= if true
export
Show PkgVersionBounds where
show p = if noBounds p then "any"
else maybe "" (\v => (if p.lowerInclusive then ">= " else "> ")
++ show v ++ " ") p.lowerBound ++
maybe "" (\v => (if p.upperInclusive then "<= " else "< ") ++ show v) p.upperBound
where
noBounds : PkgVersionBounds -> Bool
noBounds p = isNothing p.lowerBound && isNothing p.upperBound
export
anyBounds : PkgVersionBounds
anyBounds = MkPkgVersionBounds Nothing True Nothing True
export
current : PkgVersionBounds
current = let (maj,min,patch) = semVer version
version = Just (MkPkgVersion [maj, min, patch]) in
MkPkgVersionBounds version True version True
export
inBounds : PkgVersion -> PkgVersionBounds -> Bool
inBounds v bounds
= maybe True (\v' => if bounds.lowerInclusive
then v >= v'
else v > v') bounds.lowerBound &&
maybe True (\v' => if bounds.upperInclusive
then v <= v'
else v < v') bounds.upperBound
||| CLOpt - possible command line options
public export
data CLOpt
@ -119,6 +68,8 @@ data CLOpt
BuildDir String |
||| Set output directory
OutputDir String |
||| Generate profile data when compiling (backend dependent)
Profile |
||| Show the installation prefix
ShowPrefix |
||| Display Idris version
@ -244,6 +195,8 @@ options = [MkOpt ["--check", "-c"] [] [CheckOnly]
(Just $ "Set build directory"),
MkOpt ["--output-dir"] [Required "dir"] (\d => [OutputDir d])
(Just $ "Set output directory"),
MkOpt ["--profile"] [] [Profile]
(Just "Generate profile data when compiling, if supported"),
optSeparator,
MkOpt ["--prefix"] [] [ShowPrefix]
@ -254,10 +207,16 @@ options = [MkOpt ["--check", "-c"] [] [CheckOnly]
(Just "Show library directory"),
optSeparator,
MkOpt ["--init"] [Optional "package file"]
(\ f => [Package Init (fromMaybe "" f)])
(Just "Interactively initialise a new project"),
MkOpt ["--build"] [Required "package file"] (\f => [Package Build f])
(Just "Build modules/executable for the given package"),
MkOpt ["--install"] [Required "package file"] (\f => [Package Install f])
(Just "Install the given package"),
MkOpt ["--mkdoc"] [Required "package file"] (\f => [Package MkDoc f])
(Just "Build documentation for the given package"),
MkOpt ["--typecheck"] [Required "package file"] (\f => [Package Typecheck f])
(Just "Typechecks the given package without code generation"),
MkOpt ["--clean"] [Required "package file"] (\f => [Package Clean f])

View File

@ -783,16 +783,17 @@ mutual
= pure [IData fc vis !(desugarData ps doc ddecl)]
desugarDecl ps (PParameters fc params pds)
= do pds' <- traverse (desugarDecl (ps ++ map fst params)) pds
params' <- traverse (\ ntm => do tm' <- desugar AnyExpr ps (snd ntm)
pure (fst ntm, tm')) params
params' <- traverse (\(n, rig, i, ntm) => do tm' <- desugar AnyExpr ps ntm
i' <- traverse (desugar AnyExpr ps) i
pure (n, rig, i', tm')) params
-- Look for implicitly bindable names in the parameters
let pnames = ifThenElse !isUnboundImplicits
(concatMap (findBindableNames True
(ps ++ map Builtin.fst params) [])
(map Builtin.snd params'))
(map (Builtin.snd . Builtin.snd . Builtin.snd) params'))
[]
let paramsb = map (\ ntm => (Builtin.fst ntm,
doBind pnames (Builtin.snd ntm))) params'
let paramsb = map (\(n, rig, info, tm) =>
(n, rig, info, doBind pnames tm)) params'
pure [IParameters fc paramsb (concat pds')]
desugarDecl ps (PUsing fc uimpls uds)
= do syn <- get Syn
@ -935,12 +936,7 @@ mutual
mkConName n = DN (show n) (MN ("__mk" ++ show n) 0)
mapDesugarPiInfo : 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)
mapDesugarPiInfo ps = traverse (desugar AnyExpr ps)
desugarDecl ps (PFixity fc Prefix prec (UN n))
= do syn <- get Syn
@ -957,7 +953,8 @@ mutual
mds' <- traverse (desugarDecl ps) mds
pure (concat mds')
desugarDecl ps (PNamespace fc ns decls)
= do ds <- traverse (desugarDecl ps) decls
= withExtendedNS ns $ do
ds <- traverse (desugarDecl ps) decls
pure [INamespace fc ns (concat ds)]
desugarDecl ps (PTransform fc n lhs rhs)
= do (bound, blhs) <- bindNames False !(desugar LHS ps lhs)
@ -991,6 +988,7 @@ mutual
Overloadable n => pure [IPragma [] (\nest, env => setNameFlag fc n Overloadable)]
Extension e => pure [IPragma [] (\nest, env => setExtension e)]
DefaultTotality tot => pure [IPragma [] (\_, _ => setDefaultTotalityOption tot)]
desugarDecl ps (PBuiltin fc type name) = pure [IBuiltin fc type name]
export
desugar : {auto s : Ref Syn SyntaxInfo} ->

127
src/Idris/Doc/HTML.idr Normal file
View File

@ -0,0 +1,127 @@
module Idris.Doc.HTML
import Core.Context
import Core.Core
import Core.Directory
import Data.Strings
import Parser.Lexer.Source
import Libraries.Text.PrettyPrint.Prettyprinter
import Libraries.Text.PrettyPrint.Prettyprinter.Render.HTML
import Libraries.Text.PrettyPrint.Prettyprinter.SimpleDocTree
import Idris.DocString
import Idris.Package.Types
import Idris.Pretty
import Idris.Version
getNS : Name -> String
getNS (NS ns _) = show ns
getNS _ = ""
hasNS : Name -> Bool
hasNS (NS _ _) = True
hasNS _ = False
tryCanonicalName : {auto c : Ref Ctxt Defs} ->
FC -> Name -> Core (Maybe Name)
tryCanonicalName fc n with (hasNS n)
tryCanonicalName fc n | True
= do defs <- get Ctxt
case !(lookupCtxtName n (gamma defs)) of
[(n, _, _)] => pure $ Just n
_ => pure Nothing
tryCanonicalName fc n | False = pure Nothing
packageInternal : {auto c : Ref Ctxt Defs} ->
Name -> Core Bool
packageInternal (NS ns _) =
do let mi = nsAsModuleIdent ns
catch ((const True) <$> nsToSource emptyFC mi) (\_ => pure False)
packageInternal _ = pure False
prettyNameRoot : Name -> String
prettyNameRoot n =
let root = htmlEscape $ nameRoot n in
if isOpName n then "(" ++ root ++ ")" else root
renderHtml : {auto c : Ref Ctxt Defs} ->
SimpleDocTree IdrisDocAnn ->
Core String
renderHtml STEmpty = pure neutral
renderHtml (STChar ' ') = pure "&ensp;"
renderHtml (STChar c) = pure $ cast c
renderHtml (STText _ text) = pure $ htmlEscape text
renderHtml (STLine _) = pure "<br>"
renderHtml (STAnn Declarations rest) = pure $ "<dl class=\"decls\">" <+> !(renderHtml rest) <+> "</dl>"
renderHtml (STAnn (Decl n) rest) = pure $ "<dt id=\"" ++ (htmlEscape $ show n) ++ "\">" <+> !(renderHtml rest) <+> "</dt>"
renderHtml (STAnn DocStringBody rest) = pure $ "<dd>" <+> !(renderHtml rest) <+> "</dd>"
renderHtml (STAnn DCon rest) = do
resthtml <- renderHtml rest
pure $ "<span class=\"name constructor\">" <+> resthtml <+> "</span>"
renderHtml (STAnn (TCon n) rest) = do
pure $ "<span class=\"name type\">" <+> (prettyNameRoot n) <+> "</span>"
renderHtml (STAnn (Fun n) rest) = do
pure $ "<span class=\"name function\">" <+> (prettyNameRoot n) <+> "</span>"
renderHtml (STAnn Header rest) = do
resthtml <- renderHtml rest
pure $ "<b>" <+> resthtml <+> "</b>"
renderHtml (STAnn (Syntax (SynRef n)) rest) = do
resthtml <- renderHtml rest
Just cName <- tryCanonicalName emptyFC n
| Nothing => pure $ "<span class=\"implicit\">" <+> resthtml <+> "</span>"
True <- packageInternal cName
| False => pure $ "<span class=\"type resolved\" title=\"" <+> (htmlEscape $ show cName) <+> "\">" <+> (htmlEscape $ nameRoot cName) <+> "</span>"
pure $ "<a class=\"type\" href=\"" ++ (htmlEscape $ getNS cName) ++ ".html#" ++ (htmlEscape $ show cName) ++ "\">" <+> (htmlEscape $ nameRoot cName) <+> "</a>"
renderHtml (STAnn ann rest) = do
resthtml <- renderHtml rest
pure $ "<!-- ann ignored START -->" ++ resthtml ++ "<!-- ann END -->"
renderHtml (STConcat docs) = pure $ fastConcat !(traverse renderHtml docs)
docDocToHtml : {auto c : Ref Ctxt Defs} ->
Doc IdrisDocAnn ->
Core String
docDocToHtml doc =
let dt = SimpleDocTree.fromStream $ layoutUnbounded doc in
renderHtml dt
htmlPreamble : String -> String -> String -> String
htmlPreamble title root class = "<!DOCTYPE html><html lang=\"en\"><head><meta charset=\"utf-8\">"
++ "<title>" ++ htmlEscape title ++ "</title>"
++ "<link rel=\"stylesheet\" href=\"" ++ root ++ "styles.css\"></head>"
++ "<body class=\"" ++ class ++ "\">"
++ "<header><strong>Idris2Doc</strong> : " ++ htmlEscape title
++ "<nav><a href=\"" ++ root ++ "index.html\">Index</a></nav></header>"
++ "<div class=\"container\">"
htmlFooter : String
htmlFooter = "</div><footer>Produced by Idris 2 version " ++ (showVersion True version) ++ "</footer></body></html>"
export
renderDocIndex : PkgDesc -> String
renderDocIndex pkg = fastConcat $
[ htmlPreamble (name pkg) "" "index"
, "<h1>Package ", name pkg, " - Namespaces</h1>"
, "<ul class=\"names\">"] ++
(map moduleLink $ modules pkg) ++
[ "</ul>"
, htmlFooter
]
where
moduleLink : (ModuleIdent, String) -> String
moduleLink (mod, filename) =
"<li><a class=\"code\" href=\"docs/" ++ (show mod) ++ ".html\">" ++ (show mod) ++ "</a></li>"
export
renderModuleDoc : {auto c : Ref Ctxt Defs} ->
ModuleIdent ->
Doc IdrisDocAnn ->
Core String
renderModuleDoc mod allModuleDocs = pure $ fastConcat
[ htmlPreamble (show mod) "../" "namespace"
, "<h1>", show mod, "</h1>"
, !(docDocToHtml allModuleDocs)
, htmlFooter
]

View File

@ -1,28 +1,71 @@
module Idris.DocString
import Core.Context
import Core.Context.Log
import Core.Core
import Core.Env
import Core.TT
import Idris.Pretty
import Idris.Pretty.Render
import Idris.REPL.Opts
import Idris.Resugar
import Idris.Syntax
import TTImp.TTImp
import TTImp.Elab.Prim
import Libraries.Data.ANameMap
import Data.List
import Data.List1
import Data.Maybe
import Libraries.Data.NameMap
import Data.Strings
import Libraries.Data.ANameMap
import Libraries.Data.NameMap
import Libraries.Data.StringMap as S
import Libraries.Data.String.Extra
%hide Data.Strings.lines
%hide Data.Strings.lines'
%hide Data.Strings.unlines
%hide Data.Strings.unlines'
import Libraries.Control.ANSI.SGR
import public Libraries.Text.PrettyPrint.Prettyprinter
import public Libraries.Text.PrettyPrint.Prettyprinter.Util
import Parser.Lexer.Source
public export
data IdrisDocAnn
= TCon Name
| DCon
| Fun Name
| Header
| Declarations
| Decl Name
| DocStringBody
| Syntax IdrisSyntax
export
styleAnn : IdrisDocAnn -> AnsiStyle
styleAnn (TCon _) = color BrightBlue
styleAnn DCon = color BrightRed
styleAnn (Fun _) = color BrightGreen
styleAnn Header = underline
styleAnn _ = []
export
tCon : Name -> Doc IdrisDocAnn -> Doc IdrisDocAnn
tCon n = annotate (TCon n)
export
dCon : Doc IdrisDocAnn -> Doc IdrisDocAnn
dCon = annotate DCon
export
fun : Name -> Doc IdrisDocAnn -> Doc IdrisDocAnn
fun n = annotate (Fun n)
export
header : Doc IdrisDocAnn -> Doc IdrisDocAnn
header d = annotate Header d <+> colon
-- Add a doc string for a name in the current namespace
export
@ -32,6 +75,8 @@ addDocString : {auto c : Ref Ctxt Defs} ->
Core ()
addDocString n_in doc
= do n <- inCurrentNS n_in
log "doc.record" 50 $
"Adding doc for " ++ show n_in ++ " (aka " ++ show n ++ " in current NS)"
syn <- get Syn
put Syn (record { docstrings $= addName n doc,
saveDocstrings $= insert n () } syn)
@ -61,119 +106,180 @@ getDocsForPrimitive constant = do
let typeString = show constant ++ " : " ++ show !(resugar [] type)
pure [typeString ++ "\n\tPrimitive"]
prettyTerm : PTerm -> Doc IdrisDocAnn
prettyTerm = reAnnotate Syntax . Idris.Pretty.prettyTerm
export
getDocsForName : {auto c : Ref Ctxt Defs} ->
getDocsForName : {auto o : Ref ROpts REPLOpts} ->
{auto c : Ref Ctxt Defs} ->
{auto s : Ref Syn SyntaxInfo} ->
FC -> Name -> Core (List String)
FC -> Name -> Core (Doc IdrisDocAnn)
getDocsForName fc n
= do syn <- get Syn
defs <- get Ctxt
all@(_ :: _) <- lookupCtxtName n (gamma defs)
let extra = case nameRoot n of
"-" => [NS numNS (UN "negate")]
_ => []
resolved <- lookupCtxtName n (gamma defs)
let all@(_ :: _) = extra ++ map fst resolved
| _ => undefinedName fc n
let ns@(_ :: _) = concatMap (\n => lookupName n (docstrings syn))
(map fst all)
| [] => pure ["No documentation for " ++ show n]
traverse showDoc ns
let ns@(_ :: _) = concatMap (\n => lookupName n (docstrings syn)) all
| [] => pure $ pretty ("No documentation for " ++ show n)
docs <- traverse showDoc ns
pure $ vcat (punctuate Line docs)
where
addNL : String -> String
addNL str = if trim str == "" then "" else str ++ "\n"
indent : String -> String
indent str = unlines $ map ("\t" ++) (forget $ lines str)
-- Avoid generating too much whitespace by not returning a single empty line
reflowDoc : String -> List (Doc IdrisDocAnn)
reflowDoc "" = []
reflowDoc str = map (indent 2 . reflow) (forget $ Extra.lines str)
showTotal : Name -> Totality -> String
showTotal : Name -> Totality -> Doc IdrisDocAnn
showTotal n tot
= case isTerminating tot of
Unchecked => ""
_ => "\nTotality: " ++ show tot
_ => header "Totality" <++> pretty tot
getConstructorDoc : Name -> Core (Maybe String)
getConstructorDoc con
prettyName : Name -> Doc IdrisDocAnn
prettyName n =
let root = nameRoot n in
if isOpName n then parens (pretty root) else pretty root
getDConDoc : Name -> Core (List (Doc IdrisDocAnn))
getDConDoc con
= do defs <- get Ctxt
Just def <- lookupCtxtExact con (gamma defs)
| Nothing => pure Nothing
| Nothing => pure []
syn <- get Syn
let [(n, str)] = lookupName con (docstrings syn)
| _ => pure Nothing
ty <- normaliseHoles defs [] (type def)
pure (Just (nameRoot n ++ " : " ++ show !(resugar [] ty)
++ "\n" ++ addNL (indent str)))
| _ => pure []
ty <- resugar [] =<< normaliseHoles defs [] (type def)
pure $ pure $ vcat $
annotate (Decl con) (hsep [dCon (prettyName n), colon, prettyTerm ty])
:: reflowDoc str
getImplDoc : Name -> Core (Maybe String)
getImplDoc : Name -> Core (List (Doc IdrisDocAnn))
getImplDoc n
= do defs <- get Ctxt
Just def <- lookupCtxtExact n (gamma defs)
| Nothing => pure Nothing
ty <- normaliseHoles defs [] (type def)
pure $ Just $ addNL $ indent $ show !(resugar [] ty)
| Nothing => pure []
ty <- resugar [] =<< normaliseHoles defs [] (type def)
pure [annotate (Decl n) $ prettyTerm ty]
getMethDoc : Method -> Core (Maybe String)
getMethDoc : Method -> Core (List (Doc IdrisDocAnn))
getMethDoc meth
= do syn <- get Syn
let [(n, str)] = lookupName meth.name (docstrings syn)
| _ => pure Nothing
pure (Just (nameRoot meth.name ++ " : " ++ show !(pterm meth.type)
++ maybe "" (\t => "\n" ++ show t) meth.totalReq
++ "\n" ++ addNL (indent str)))
| _ => pure []
ty <- pterm meth.type
let nm = prettyName meth.name
pure $ pure $ vcat [
annotate (Decl meth.name) (hsep [fun (meth.name) nm, colon, prettyTerm ty])
, annotate DocStringBody $ vcat (
toList (indent 2 . pretty . show <$> meth.totalReq)
++ reflowDoc str)
]
getIFaceDoc : (Name, IFaceInfo) -> Core String
getInfixDoc : Name -> Core (List (Doc IdrisDocAnn))
getInfixDoc n
= do let Just (fixity, assoc) = S.lookupName n (infixes !(get Syn))
| Nothing => pure []
pure $ pure $ hsep
[ pretty (show fixity)
, "operator,"
, "level"
, pretty (show assoc)
]
getPrefixDoc : Name -> Core (List (Doc IdrisDocAnn))
getPrefixDoc n
= do let Just assoc = S.lookupName n (prefixes !(get Syn))
| Nothing => pure []
pure $ ["prefix operator, level" <++> pretty (show assoc)]
getFixityDoc : Name -> Core (List (Doc IdrisDocAnn))
getFixityDoc n =
pure $ case toList !(getInfixDoc n) ++ toList !(getPrefixDoc n) of
[] => []
[f] => [header "Fixity Declaration" <++> f]
fs => [header "Fixity Declarations" <+> Line <+>
indent 2 (vcat fs)]
getIFaceDoc : (Name, IFaceInfo) -> Core (Doc IdrisDocAnn)
getIFaceDoc (n, iface)
= do let params =
case params iface of
[] => ""
ps => "Parameters: " ++ showSep ", " (map show ps) ++ "\n"
constraints <-
case parents iface of
[] => pure ""
ps => do pts <- traverse pterm ps
pure ("Constraints: " ++
showSep ", " (map show pts) ++ "\n")
[] => []
ps => [hsep (header "Parameters" :: punctuate comma (map (pretty . show) ps))]
let constraints =
case !(traverse pterm (parents iface)) of
[] => []
ps => [hsep (header "Constraints" :: punctuate comma (map (pretty . show) ps))]
mdocs <- traverse getMethDoc (methods iface)
let meths = case mapMaybe id mdocs of
[] => ""
docs => "\nMethods:\n" ++ concat docs
let meths = case concat mdocs of
[] => []
docs => [vcat [header "Methods", annotate Declarations $ vcat $ map (indent 2) docs]]
sd <- getSearchData fc False n
idocs <- case hintGroups sd of
[] => pure []
[] => pure (the (List (List (Doc IdrisDocAnn))) [])
((_, tophs) :: _) => traverse getImplDoc tophs
let insts = case mapMaybe id idocs of
[] => ""
docs => "\nImplementations:\n" ++ concat docs
pure (params ++ constraints ++ meths ++ insts)
let insts = case concat idocs of
[] => []
[doc] => [header "Implementation" <++> annotate Declarations doc]
docs => [vcat [header "Implementations"
, annotate Declarations $ vcat $ map (indent 2) docs]]
pure (vcat (params ++ constraints ++ meths ++ insts))
getExtra : Name -> GlobalDef -> Core String
getExtra : Name -> GlobalDef -> Core (List (Doc IdrisDocAnn))
getExtra n d
= do syn <- get Syn
let [] = lookupName n (ifaces syn)
| [ifacedata] => getIFaceDoc ifacedata
| _ => pure "" -- shouldn't happen, we've resolved ambiguity by now
| [ifacedata] => pure <$> getIFaceDoc ifacedata
| _ => pure [] -- shouldn't happen, we've resolved ambiguity by now
case definition d of
PMDef _ _ _ _ _
=> pure (showTotal n (totality d))
=> pure [showTotal n (totality d)]
TCon _ _ _ _ _ _ cons _
=> do cdocs <- traverse getConstructorDoc
!(traverse toFullNames cons)
case mapMaybe id cdocs of
[] => pure ""
docs => pure $ "\nConstructors:\n" ++ concat docs
_ => pure ""
=> do let tot = [showTotal n (totality d)]
cdocs <- traverse (getDConDoc <=< toFullNames) cons
let cdoc = case concat cdocs of
[] => []
[doc] => [header "Constructor" <++> annotate Declarations doc]
docs => [vcat [header "Constructors"
, annotate Declarations $ vcat $ map (indent 2) docs]]
pure (tot ++ cdoc)
_ => pure []
showDoc : (Name, String) -> Core String
showCategory : GlobalDef -> Doc IdrisDocAnn -> Doc IdrisDocAnn
showCategory d = case definition d of
TCon _ _ _ _ _ _ _ _ => tCon (fullname d)
DCon _ _ _ => dCon
PMDef _ _ _ _ _ => fun (fullname d)
ForeignDef _ _ => fun (fullname d)
Builtin _ => fun (fullname d)
_ => id
showDoc : (Name, String) -> Core (Doc IdrisDocAnn)
showDoc (n, str)
= do defs <- get Ctxt
Just def <- lookupCtxtExact n (gamma defs)
| Nothing => undefinedName fc n
ty <- normaliseHoles defs [] (type def)
let doc = show !(aliasName n) ++ " : " ++ show !(resugar [] ty)
++ "\n" ++ addNL (indent str)
ty <- resugar [] =<< normaliseHoles defs [] (type def)
let cat = showCategory def
nm <- aliasName n
let docDecl = annotate (Decl n) (hsep [cat (pretty (show nm)), colon, prettyTerm ty])
let docText = reflowDoc str
extra <- getExtra n def
pure (doc ++ extra)
fixes <- getFixityDoc n
let docBody = annotate DocStringBody $ vcat $ docText ++ (map (indent 2) (extra ++ fixes))
pure (vcat [docDecl, docBody])
export
getDocsForPTerm : {auto c : Ref Ctxt Defs} ->
getDocsForPTerm : {auto o : Ref ROpts REPLOpts} ->
{auto c : Ref Ctxt Defs} ->
{auto s : Ref Syn SyntaxInfo} ->
PTerm -> Core (List String)
getDocsForPTerm (PRef fc name) = getDocsForName fc name
getDocsForPTerm (PRef fc name) = pure $ [!(render styleAnn !(getDocsForName fc name))]
getDocsForPTerm (PPrimVal _ constant) = getDocsForPrimitive constant
getDocsForPTerm (PType _) = pure ["Type : Type\n\tThe type of all types is Type. The type of Type is Type."]
getDocsForPTerm (PString _ _) = pure ["String Literal\n\tDesugars to a fromString call"]
@ -192,7 +298,7 @@ summarise n -- n is fully qualified
Just def <- lookupCtxtExact n (gamma defs)
| _ => pure ""
let doc = case lookupName n (docstrings syn) of
[(_, doc)] => case lines doc of
[(_, doc)] => case Extra.lines doc of
("" ::: _) => Nothing
(d ::: _) => Just d
_ => Nothing

View File

@ -164,7 +164,7 @@ stMain cgs opts
let ideSocket = ideModeSocket opts
let outmode = if ide then IDEMode 0 stdin stdout else REPL False
let fname = findInput opts
o <- newRef ROpts (REPLOpts.defaultOpts fname outmode cgs)
o <- newRef ROpts (REPL.Opts.defaultOpts fname outmode cgs)
finish <- showInfo opts
when (not finish) $ do

View File

@ -7,7 +7,7 @@ import Core.Env
import Core.Options
import Core.Value
import Idris.REPLOpts
import Idris.REPL.Opts
import Idris.Resugar
import Idris.Syntax
import Idris.Pretty
@ -34,6 +34,9 @@ import Libraries.Data.String.Extra
%default covering
keyword : Doc IdrisAnn -> Doc IdrisAnn
keyword = annotate (Syntax SynKeyword)
-- | Add binding site information if the term is simply a machine-inserted name
pShowMN : {vars : _} -> Term vars -> Env t vars -> Doc IdrisAnn -> Doc IdrisAnn
pShowMN t env acc = case t of
@ -50,7 +53,7 @@ pshow env tm
= do defs <- get Ctxt
ntm <- normaliseHoles defs env tm
itm <- resugar env ntm
pure (pShowMN ntm env $ prettyTerm itm)
pure (pShowMN ntm env $ reAnnotate Syntax $ prettyTerm itm)
pshowNoNorm : {vars : _} ->
{auto c : Ref Ctxt Defs} ->
@ -59,7 +62,7 @@ pshowNoNorm : {vars : _} ->
pshowNoNorm env tm
= do defs <- get Ctxt
itm <- resugar env tm
pure (pShowMN tm env $ prettyTerm itm)
pure (pShowMN tm env $ reAnnotate Syntax $ prettyTerm itm)
ploc : {auto o : Ref ROpts REPLOpts} ->
FC -> Core (Doc IdrisAnn)

View File

@ -14,7 +14,7 @@ import TTImp.TTImp
import TTImp.Utils
import Idris.IDEMode.TokenLine
import Idris.REPLOpts
import Idris.REPL.Opts
import Idris.Resugar
import Idris.Syntax

View File

@ -2,7 +2,7 @@ module Idris.IDEMode.Commands
import Core.Core
import Core.Name
import public Idris.REPLOpts
import public Idris.REPL.Opts
import Libraries.Utils.Hex
import System.File

View File

@ -141,7 +141,7 @@ prettyHole : {vars : _} ->
{auto c : Ref Ctxt Defs} ->
{auto s : Ref Syn SyntaxInfo} ->
Defs -> Env Term vars -> Name -> Nat -> Term vars ->
Core (Doc IdrisAnn)
Core (Doc IdrisSyntax)
prettyHole defs env fn args ty
= do hdata <- holeData defs env fn args ty
case hdata.context of

View File

@ -292,6 +292,7 @@ SExpable REPLOpt where
toSExp (EvalMode mod) = SExpList [ SymbolAtom "eval", toSExp mod ]
toSExp (Editor editor) = SExpList [ SymbolAtom "editor", toSExp editor ]
toSExp (CG str) = SExpList [ SymbolAtom "cg", toSExp str ]
toSExp (Profile p) = SExpList [ SymbolAtom "profile", toSExp p ]
displayIDEResult : {auto c : Ref Ctxt Defs} ->

View File

@ -15,7 +15,7 @@ import Idris.Desugar
import Idris.Error
import Idris.Parser
import Idris.ProcessIdr
import Idris.REPLCommon
import Idris.REPL.Common
import Idris.Syntax
import Idris.Pretty

View File

@ -5,16 +5,14 @@ import Compiler.Common
import Core.Context
import Core.Core
import Core.Directory
import Core.Env
import Core.Metadata
import Core.Options
import Core.Unify
import Data.List
import Data.Maybe
import Data.So
import Libraries.Data.StringMap
import Data.Strings
import Libraries.Data.StringTrie
import Data.These
import Parser.Package
@ -22,6 +20,8 @@ import System
import System.Directory
import System.File
import Libraries.Data.StringMap
import Libraries.Data.StringTrie
import Libraries.Text.Parser
import Libraries.Text.PrettyPrint.Prettyprinter
import Libraries.Utils.Binary
@ -29,16 +29,21 @@ import Libraries.Utils.String
import Libraries.Utils.Path
import Idris.CommandLine
import Idris.Doc.HTML
import Idris.DocString
import Idris.ModTree
import Idris.ProcessIdr
import Idris.REPL
import Idris.REPLCommon
import Idris.REPLOpts
import Idris.REPL.Common
import Idris.REPL.Opts
import Idris.SetOptions
import Idris.Syntax
import Idris.Version
import IdrisPaths
import public Idris.Package.Types
import Idris.Package.Init
%hide Data.Strings.lines
%hide Data.Strings.lines'
%hide Data.Strings.unlines
@ -46,81 +51,10 @@ import IdrisPaths
%default covering
public export
record Depends where
constructor MkDepends
pkgname : String
pkgbounds : PkgVersionBounds
export
Show Depends where
show p = p.pkgname ++ " " ++ show p.pkgbounds
public export
record PkgDesc where
constructor MkPkgDesc
name : String
version : PkgVersion
authors : String
maintainers : Maybe String
license : Maybe String
brief : Maybe String
readme : Maybe String
homepage : Maybe String
sourceloc : Maybe String
bugtracker : Maybe String
depends : List Depends -- packages to add to search path
modules : List (ModuleIdent, String) -- modules to install (namespace, filename)
mainmod : Maybe (ModuleIdent, String) -- main file (i.e. file to load at REPL)
executable : Maybe String -- name of executable
options : Maybe (FC, String)
sourcedir : Maybe String
builddir : Maybe String
outputdir : Maybe String
prebuild : Maybe (FC, String) -- Script to run before building
postbuild : Maybe (FC, String) -- Script to run after building
preinstall : Maybe (FC, String) -- Script to run after building, before installing
postinstall : Maybe (FC, String) -- Script to run after installing
preclean : Maybe (FC, String) -- Script to run before cleaning
postclean : Maybe (FC, String) -- Script to run after cleaning
installDir : PkgDesc -> String
installDir p = name p ++ "-" ++ show (version p)
export
Show PkgDesc where
show pkg = "Package: " ++ name pkg ++ "\n" ++
"Version: " ++ show (version pkg) ++ "\n" ++
"Authors: " ++ authors pkg ++ "\n" ++
maybe "" (\m => "Maintainers: " ++ m ++ "\n") (maintainers pkg) ++
maybe "" (\m => "License: " ++ m ++ "\n") (license pkg) ++
maybe "" (\m => "Brief: " ++ m ++ "\n") (brief pkg) ++
maybe "" (\m => "ReadMe: " ++ m ++ "\n") (readme pkg) ++
maybe "" (\m => "HomePage: " ++ m ++ "\n") (homepage pkg) ++
maybe "" (\m => "SourceLoc: " ++ m ++ "\n") (sourceloc pkg) ++
maybe "" (\m => "BugTracker: " ++ m ++ "\n") (bugtracker pkg) ++
"Depends: " ++ show (depends pkg) ++ "\n" ++
"Modules: " ++ show (map snd (modules pkg)) ++ "\n" ++
maybe "" (\m => "Main: " ++ snd m ++ "\n") (mainmod pkg) ++
maybe "" (\m => "Exec: " ++ m ++ "\n") (executable pkg) ++
maybe "" (\m => "Opts: " ++ snd m ++ "\n") (options pkg) ++
maybe "" (\m => "SourceDir: " ++ m ++ "\n") (sourcedir pkg) ++
maybe "" (\m => "BuildDir: " ++ m ++ "\n") (builddir pkg) ++
maybe "" (\m => "OutputDir: " ++ m ++ "\n") (outputdir pkg) ++
maybe "" (\m => "Prebuild: " ++ snd m ++ "\n") (prebuild pkg) ++
maybe "" (\m => "Postbuild: " ++ snd m ++ "\n") (postbuild pkg) ++
maybe "" (\m => "Preinstall: " ++ snd m ++ "\n") (preinstall pkg) ++
maybe "" (\m => "Postinstall: " ++ snd m ++ "\n") (postinstall pkg) ++
maybe "" (\m => "Preclean: " ++ snd m ++ "\n") (preclean pkg) ++
maybe "" (\m => "Postclean: " ++ snd m ++ "\n") (postclean pkg)
initPkgDesc : String -> PkgDesc
initPkgDesc pname
= MkPkgDesc pname (MkPkgVersion [0,0]) "Anonymous" Nothing Nothing
Nothing Nothing Nothing Nothing Nothing
[] []
Nothing Nothing Nothing Nothing Nothing Nothing Nothing Nothing
Nothing Nothing Nothing Nothing
installDir p = name p
++ "-"
++ show (fromMaybe (MkPkgVersion (0 ::: [])) (version p))
data DescField : Type where
PVersion : FC -> PkgVersion -> DescField
@ -175,7 +109,7 @@ field fname
vs <- sepBy1 dot' integerLit
end <- location
pure (PVersion (MkFC fname start end)
(MkPkgVersion (fromInteger <$> forget vs)))
(MkPkgVersion (fromInteger <$> vs)))
<|> do start <- location
ignore $ exactProperty "version"
equals
@ -210,20 +144,20 @@ field fname
bound
= do lte
vs <- sepBy1 dot' integerLit
pure [LT (MkPkgVersion (fromInteger <$> forget vs)) True]
pure [LT (MkPkgVersion (fromInteger <$> vs)) True]
<|> do gte
vs <- sepBy1 dot' integerLit
pure [GT (MkPkgVersion (fromInteger <$> forget vs)) True]
pure [GT (MkPkgVersion (fromInteger <$> vs)) True]
<|> do lt
vs <- sepBy1 dot' integerLit
pure [LT (MkPkgVersion (fromInteger <$> forget vs)) False]
pure [LT (MkPkgVersion (fromInteger <$> vs)) False]
<|> do gt
vs <- sepBy1 dot' integerLit
pure [GT (MkPkgVersion (fromInteger <$> forget vs)) False]
pure [GT (MkPkgVersion (fromInteger <$> vs)) False]
<|> do eqop
vs <- sepBy1 dot' integerLit
pure [LT (MkPkgVersion (fromInteger <$> forget vs)) True,
GT (MkPkgVersion (fromInteger <$> forget vs)) True]
pure [LT (MkPkgVersion (fromInteger <$> vs)) True,
GT (MkPkgVersion (fromInteger <$> vs)) True]
mkBound : List Bound -> PkgVersionBounds -> PackageEmptyRule PkgVersionBounds
mkBound (LT b i :: bs) pkgbs
@ -271,11 +205,11 @@ addField : {auto c : Ref Ctxt Defs} ->
{auto p : Ref ParsedMods (List (FC, ModuleIdent))} ->
{auto m : Ref MainMod (Maybe (FC, ModuleIdent))} ->
DescField -> PkgDesc -> Core PkgDesc
addField (PVersion fc n) pkg = pure $ record { version = n } pkg
addField (PVersion fc n) pkg = pure $ record { version = Just n } pkg
addField (PVersionDep fc n) pkg
= do emitWarning (Deprecated "version numbers must now be of the form x.y.z")
pure pkg
addField (PAuthors fc a) pkg = pure $ record { authors = a } pkg
addField (PAuthors fc a) pkg = pure $ record { authors = Just a } pkg
addField (PMaintainers fc a) pkg = pure $ record { maintainers = Just a } pkg
addField (PLicense fc a) pkg = pure $ record { license = Just a } pkg
addField (PBrief fc a) pkg = pure $ record { brief = Just a } pkg
@ -478,16 +412,75 @@ check pkg opts =
runScript (postbuild pkg)
pure []
makeDoc : {auto c : Ref Ctxt Defs} ->
{auto s : Ref Syn SyntaxInfo} ->
{auto o : Ref ROpts REPLOpts} ->
PkgDesc ->
List CLOpt ->
Core (List Error)
makeDoc pkg opts =
do [] <- prepareCompilation pkg opts
| errs => pure errs
defs <- get Ctxt
let build = build_dir (dirs (options defs))
let docBase = build </> "docs"
let docDir = docBase </> "docs"
Right () <- coreLift $ mkdirAll docDir
| Left err => fileError docDir err
u <- newRef UST initUState
setPPrint (MkPPOpts False False True)
[] <- concat <$> for (modules pkg) (\(mod, filename) => do
let ns = miAsNamespace mod
addImport (MkImport emptyFC False mod ns)
defs <- get Ctxt
names <- allNames (gamma defs)
let allInNamespace = filter (inNS ns) names
visibleNames <- filterM (visible defs) allInNamespace
let outputFilePath = docDir </> (show mod ++ ".html")
allDocs <- annotate Declarations <$> vcat <$> for (sort visibleNames) (getDocsForName emptyFC)
Right () <- coreLift $ writeFile outputFilePath !(renderModuleDoc mod allDocs)
| Left err => fileError (docBase </> "index.html") err
pure $ the (List Error) []
)
| errs => pure errs
Right () <- coreLift $ writeFile (docBase </> "index.html") $ renderDocIndex pkg
| Left err => fileError (docBase </> "index.html") err
css <- readDataFile "docs/styles.css"
Right () <- coreLift $ writeFile (docBase </> "styles.css") css
| Left err => fileError (docBase </> "styles.css") err
runScript (postbuild pkg)
pure []
where
visible : Defs -> Name -> Core Bool
visible defs n
= do Just def <- lookupCtxtExact n (gamma defs)
| Nothing => pure False
-- TODO: if we can find out, whether a def has been declared as
-- part of an interface, hide it here
pure $ case definition def of
(DCon _ _ _) => False
_ => (visibility def /= Private)
inNS : Namespace -> Name -> Bool
inNS ns (NS xns (UN _)) = ns == xns
inNS _ _ = False
fileError : String -> FileError -> Core (List Error)
fileError filename err = pure [FileErr filename err]
-- Data.These.bitraverse hand specialised for Core
bitraverseC : (a -> Core c) -> (b -> Core d) -> These a b -> Core (These c d)
bitraverseC f g (This a) = [| This (f a) |]
bitraverseC f g (That b) = [| That (g b) |]
bitraverseC f g (Both a b) = [| Both (f a) (g b) |]
-- Prelude.Monad.foldlM hand specialised for Core
foldlC : Foldable t => (a -> b -> Core a) -> a -> t b -> Core a
foldlC fm a0 = foldl (\ma,b => ma >>= flip fm b) (pure a0)
-- Data.StringTrie.foldWithKeysM hand specialised for Core
foldWithKeysC : Monoid b => (List String -> Core b) -> (List String -> a -> Core b) -> StringTrie a -> Core b
foldWithKeysC {a} {b} fk fv = go []
@ -595,33 +588,47 @@ processPackage : {auto c : Ref Ctxt Defs} ->
(PkgCommand, String) ->
Core ()
processPackage opts (cmd, file)
= if not (isSuffixOf ".ipkg" file)
then do coreLift $ putStrLn ("Packages must have an '.ipkg' extension: " ++ show file ++ ".")
coreLift (exitWith (ExitFailure 1))
else do Right (pname, fs) <- coreLift $ parseFile file
(do desc <- parsePkgDesc file
eoi
pure desc)
| Left err => throw err
pkg <- addFields fs (initPkgDesc pname)
maybe (pure ()) setBuildDir (builddir pkg)
setOutputDir (outputdir pkg)
case cmd of
Build => do [] <- build pkg opts
| errs => coreLift (exitWith (ExitFailure 1))
pure ()
Install => do [] <- build pkg opts
| errs => coreLift (exitWith (ExitFailure 1))
install pkg opts
Typecheck => do
[] <- check pkg opts
| errs => coreLift (exitWith (ExitFailure 1))
pure ()
Clean => clean pkg opts
REPL => do
[] <- build pkg opts
| errs => coreLift (exitWith (ExitFailure 1))
runRepl (map snd $ mainmod pkg)
= withCtxt . withSyn . withROpts $ case cmd of
Init =>
do pkg <- coreLift interactive
let fp = if file == "" then pkg.name ++ ".ipkg" else file
False <- coreLift (exists fp)
| _ => throw (GenericMsg emptyFC ("File " ++ fp ++ " already exists"))
Right () <- coreLift $ writeFile fp (show $ the (Doc ()) $ pretty pkg)
| Left err => throw (FileErr fp err)
pure ()
_ =>
do let Just (dir, filename) = splitParent file
| _ => throw $ InternalError "Tried to split empty string"
let True = isSuffixOf ".ipkg" filename
| _ => do coreLift $ putStrLn ("Packages must have an '.ipkg' extension: " ++ show file ++ ".")
coreLift (exitWith (ExitFailure 1))
setWorkingDir dir
Right (pname, fs) <- coreLift $ parseFile filename (parsePkgDesc filename <* eoi)
| Left err => throw err
pkg <- addFields fs (initPkgDesc pname)
whenJust (builddir pkg) setBuildDir
setOutputDir (outputdir pkg)
case cmd of
Build => do [] <- build pkg opts
| errs => coreLift (exitWith (ExitFailure 1))
pure ()
MkDoc => do [] <- makeDoc pkg opts
| errs => coreLift (exitWith (ExitFailure 1))
pure ()
Install => do [] <- build pkg opts
| errs => coreLift (exitWith (ExitFailure 1))
install pkg opts
Typecheck => do
[] <- check pkg opts
| errs => coreLift (exitWith (ExitFailure 1))
pure ()
Clean => clean pkg opts
REPL => do
[] <- build pkg opts
| errs => coreLift (exitWith (ExitFailure 1))
runRepl (map snd $ mainmod pkg)
Init => pure () -- already handled earlier
record PackageOpts where
constructor MkPFR

View File

@ -0,0 +1,86 @@
module Idris.Package.Init
import Core.FC
import Core.Name.Namespace
import Data.List
import Data.Maybe
import Data.Strings
import Idris.Package.Types
import System.Directory
import Libraries.Utils.Path
import Libraries.System.Directory.Tree
import Libraries.Text.PrettyPrint.Prettyprinter
%default total
isModuleIdent : String -> Bool
isModuleIdent str = case unpack str of
[] => False
cs@(hd :: _) => isUpper hd && all isAlphaNum cs
packageTree : (root : Path) -> IO (Tree root)
packageTree root = filter validFile validDirectory <$> explore root where
validFile : {root : _} -> FileName root -> Bool
validFile f
= let (fname, fext) = splitFileName (fileName f) in
isModuleIdent fname && elem fext ["idr", "lidr"]
validDirectory : {root : _} -> FileName root -> Bool
validDirectory = isModuleIdent . fileName
covering
findModules : (start : Maybe String) -> IO (List (ModuleIdent, String))
findModules start = do
let prfx = fromMaybe "" start
Just dir <- maybe currentDir (pure . Just) start
| Nothing => pure []
let root = parse dir
tree <- packageTree root
mods <- go [] [([], (root ** pure tree))]
pure (sortBy (\ a, b => compare (snd a) (snd b)) mods)
where
go : List (ModuleIdent, String) ->
List (List String, (root : Path ** IO (Tree root))) ->
IO (List (ModuleIdent, String))
go acc [] = pure acc
go acc ((path, (root ** iot)) :: iots) = do
t <- liftIO iot
let mods = flip map t.files $ \ entry =>
let fname = fst (splitFileName (fileName entry)) in
let mod = unsafeFoldModuleIdent (fname :: path) in
let fp = toFilePath entry in
(mod, fp)
let dirs = flip map t.subTrees $ \ (dir ** iot) =>
(fileName dir :: path, (_ ** iot))
go (mods ++ acc) (dirs ++ iots)
export
covering
interactive : IO PkgDesc
interactive = do
pname <- putStr "Package name: " *> getLine
pauthors <- putStr "Package authors: " *> getLine
poptions <- putStr "Package options: " *> getLine
psource <- putStr "Source directory: " *> getLine
let sourcedir = mstring psource
modules <- findModules sourcedir
let pkg : PkgDesc =
{ authors := mstring pauthors
, options := (emptyFC,) <$> mstring poptions
, modules := modules
, sourcedir := sourcedir
} (initPkgDesc (fromMaybe "project" (mstring pname)))
pure pkg
where
mstring : String -> Maybe String
mstring str = case trim str of
"" => Nothing
str => Just str

245
src/Idris/Package/Types.idr Normal file
View File

@ -0,0 +1,245 @@
module Idris.Package.Types
import Core.FC
import Core.Name.Namespace
import Data.Maybe
import Data.Strings
import Idris.CommandLine
import Idris.Version
import Libraries.Text.PrettyPrint.Prettyprinter
import Libraries.Text.PrettyPrint.Prettyprinter.Util
%default total
------------------------------------------------------------------------------
-- Versions
public export
data PkgVersion = MkPkgVersion (List1 Nat)
export
Show PkgVersion where
show (MkPkgVersion vs) = showSep "." (map show (forget vs))
export
Pretty PkgVersion where
pretty = pretty . show
export
Eq PkgVersion where
MkPkgVersion p == MkPkgVersion q = p == q
export
Ord PkgVersion where
-- list ordering gives us what we want
compare (MkPkgVersion p) (MkPkgVersion q) = compare p q
------------------------------------------------------------------------------
-- Version Bounds
-- version must be >= lowerBound and <= upperBound
-- Do we want < and > as well?
public export
record PkgVersionBounds where
constructor MkPkgVersionBounds
lowerBound : Maybe PkgVersion
lowerInclusive : Bool -- >= if true
upperBound : Maybe PkgVersion
upperInclusive : Bool -- <= if true
export
Show PkgVersionBounds where
show p = if noBounds then "any" else lowerBounds ++ upperBounds
where
noBounds : Bool
noBounds = isNothing p.lowerBound && isNothing p.upperBound
lowerBounds : String
lowerBounds = case p.lowerBound of
Nothing => ""
Just v => (if p.lowerInclusive then ">= " else "> ") ++ show v ++ " "
upperBounds : String
upperBounds = case p.upperBound of
Nothing => ""
Just v => (if p.upperInclusive then "<= " else "< ") ++ show v
export
anyBounds : PkgVersionBounds
anyBounds = MkPkgVersionBounds Nothing True Nothing True
export
current : PkgVersionBounds
current = let (maj,min,patch) = semVer version
version = Just (MkPkgVersion (maj ::: [min, patch])) in
MkPkgVersionBounds version True version True
export
inBounds : Maybe PkgVersion -> PkgVersionBounds -> Bool
inBounds mv bounds
= let v = fromMaybe (MkPkgVersion (0 ::: [])) mv in
maybe True (\v' => if bounds.lowerInclusive
then v >= v'
else v > v') bounds.lowerBound &&
maybe True (\v' => if bounds.upperInclusive
then v <= v'
else v < v') bounds.upperBound
------------------------------------------------------------------------------
-- Dependencies
public export
record Depends where
constructor MkDepends
pkgname : String
pkgbounds : PkgVersionBounds
export
Show Depends where
show p = p.pkgname ++ " " ++ show p.pkgbounds
export
Pretty Depends where
pretty = pretty . show
------------------------------------------------------------------------------
-- Package description
public export
record PkgDesc where
constructor MkPkgDesc
name : String
version : Maybe PkgVersion
authors : Maybe String
maintainers : Maybe String
license : Maybe String
brief : Maybe String
readme : Maybe String
homepage : Maybe String
sourceloc : Maybe String
bugtracker : Maybe String
depends : List Depends -- packages to add to search path
modules : List (ModuleIdent, String) -- modules to install (namespace, filename)
mainmod : Maybe (ModuleIdent, String) -- main file (i.e. file to load at REPL)
executable : Maybe String -- name of executable
options : Maybe (FC, String)
sourcedir : Maybe String
builddir : Maybe String
outputdir : Maybe String
prebuild : Maybe (FC, String) -- Script to run before building
postbuild : Maybe (FC, String) -- Script to run after building
preinstall : Maybe (FC, String) -- Script to run after building, before installing
postinstall : Maybe (FC, String) -- Script to run after installing
preclean : Maybe (FC, String) -- Script to run before cleaning
postclean : Maybe (FC, String) -- Script to run after cleaning
export
initPkgDesc : String -> PkgDesc
initPkgDesc pname
= MkPkgDesc pname Nothing Nothing Nothing Nothing
Nothing Nothing Nothing Nothing Nothing
[] []
Nothing Nothing Nothing Nothing Nothing Nothing Nothing Nothing
Nothing Nothing Nothing Nothing
export
Show PkgDesc where
show pkg = "Package: " ++ name pkg ++ "\n" ++
maybe "" (\m => "Version: " ++ m ++ "\n") (show <$> version pkg) ++
maybe "" (\m => "Authors: " ++ m ++ "\n") (authors pkg) ++
maybe "" (\m => "Maintainers: " ++ m ++ "\n") (maintainers pkg) ++
maybe "" (\m => "License: " ++ m ++ "\n") (license pkg) ++
maybe "" (\m => "Brief: " ++ m ++ "\n") (brief pkg) ++
maybe "" (\m => "ReadMe: " ++ m ++ "\n") (readme pkg) ++
maybe "" (\m => "HomePage: " ++ m ++ "\n") (homepage pkg) ++
maybe "" (\m => "SourceLoc: " ++ m ++ "\n") (sourceloc pkg) ++
maybe "" (\m => "BugTracker: " ++ m ++ "\n") (bugtracker pkg) ++
"Depends: " ++ show (depends pkg) ++ "\n" ++
"Modules: " ++ show (map snd (modules pkg)) ++ "\n" ++
maybe "" (\m => "Main: " ++ snd m ++ "\n") (mainmod pkg) ++
maybe "" (\m => "Exec: " ++ m ++ "\n") (executable pkg) ++
maybe "" (\m => "Opts: " ++ snd m ++ "\n") (options pkg) ++
maybe "" (\m => "SourceDir: " ++ m ++ "\n") (sourcedir pkg) ++
maybe "" (\m => "BuildDir: " ++ m ++ "\n") (builddir pkg) ++
maybe "" (\m => "OutputDir: " ++ m ++ "\n") (outputdir pkg) ++
maybe "" (\m => "Prebuild: " ++ snd m ++ "\n") (prebuild pkg) ++
maybe "" (\m => "Postbuild: " ++ snd m ++ "\n") (postbuild pkg) ++
maybe "" (\m => "Preinstall: " ++ snd m ++ "\n") (preinstall pkg) ++
maybe "" (\m => "Postinstall: " ++ snd m ++ "\n") (postinstall pkg) ++
maybe "" (\m => "Preclean: " ++ snd m ++ "\n") (preclean pkg) ++
maybe "" (\m => "Postclean: " ++ snd m ++ "\n") (postclean pkg)
export
Pretty PkgDesc where
pretty desc = vcat
[ "package" <++> pretty desc.name
, verField "version" desc.version
, strField "authors" desc.authors
, strField "maintainers" desc.maintainers
, strField "license" desc.license
, strField "brief" desc.brief
, strField "readme" desc.readme
, strField "homepage" desc.homepage
, strField "sourceloc" desc.sourceloc
, strField "bugtracker" desc.bugtracker
, comment "packages to add to search path"
, seqField "depends" desc.depends
, comment "modules to install"
, seqField "modules" (fst <$> desc.modules)
, comment "main file (i.e. file to load at REPL)"
, field "main" (map (pretty . fst) desc.mainmod)
, comment "name of executable"
, strField "executable" desc.executable
, strField "opts" (snd <$> desc.options)
, strField "sourcedir" desc.sourcedir
, strField "builddir" desc.builddir
, strField "outputdir" desc.outputdir
, comment "script to run before building"
, strField "prebuild" (snd <$> desc.prebuild)
, comment "script to run after building"
, strField "postbuild" (snd <$> desc.postbuild)
, comment "script to run after building, before installing"
, strField "preinstall" (snd <$> desc.preinstall)
, comment "script to run after installing"
, strField "postinstall" (snd <$> desc.postinstall)
, comment "script to run before cleaning"
, strField "preclean" (snd <$> desc.preclean)
, comment "script to run after cleaning"
, strField "postclean" (snd <$> desc.postclean)
]
where
comment : String -> Doc ann
comment str =
let ws = "--" :: words str in
let commSoftLine = Union (Chara ' ') (hcat [Line, pretty "-- "]) in
Line <+> concatWith (\x, y => x <+> commSoftLine <+> y) ws
field : String -> Maybe (Doc ann) -> Doc ann
field nm Nothing = hsep [ pretty "--", pretty nm, equals ]
field nm (Just d) = hsep [ pretty nm, equals, d ]
verField : String -> Maybe PkgVersion -> Doc ann
verField nm = field nm . map pretty
strField : String -> Maybe String -> Doc ann
strField nm = field nm . map (pretty . show)
seqField : Pretty a => String -> List a -> Doc ann
seqField nm [] = hsep [ pretty "--", pretty nm, equals ]
seqField nm xs = pretty nm
<++> equals
<++> align (sep (punctuate comma (map pretty xs)))

View File

@ -53,6 +53,8 @@ plhs = MkParseOpts False False
%hide Core.Core.(>>=)
%hide Prelude.pure
%hide Core.Core.pure
%hide Prelude.(<*>)
%hide Core.Core.(<*>)
atom : FileName -> Rule PTerm
atom fname
@ -222,7 +224,7 @@ mutual
pure (POp (boundToFC fname (mergeBounds l r)) (UN "=") l.val r.val)
else fail "= not allowed")
<|>
(do b <- bounds (MkPair <$> (continue indents *> iOperator) <*> opExpr q fname indents)
(do b <- bounds [| MkPair (continue indents *> iOperator) (opExpr q fname indents) |]
(op, r) <- pure b.val
pure (POp (boundToFC fname (mergeBounds l b)) op l.val r))
<|> pure l.val
@ -424,16 +426,13 @@ mutual
(lvl, e) <- pure b.val
pure (PUnifyLog (boundToFC fname b) lvl e)
multiplicity : SourceEmptyRule (Maybe Integer)
multiplicity : SourceEmptyRule RigCount
multiplicity
= optional $ intLit
-- <|> 2 <$ symbol "&" Borrowing, not implemented
getMult : Maybe Integer -> SourceEmptyRule RigCount
getMult (Just 0) = pure erased
getMult (Just 1) = pure linear
getMult Nothing = pure top
getMult _ = fatalError "Invalid multiplicity (must be 0 or 1)"
= case !(optional $ intLit) of
(Just 0) => pure erased
(Just 1) => pure linear
Nothing => pure top
_ => fail "Invalid multiplicity (must be 0 or 1)"
pibindAll : FileName -> PiInfo PTerm ->
List (RigCount, WithBounds (Maybe Name), PTerm) ->
@ -446,35 +445,32 @@ mutual
Rule (List (RigCount, WithBounds PTerm, PTerm))
bindList fname indents
= forget <$> sepBy1 (symbol ",")
(do rigc <- multiplicity
(do rig <- multiplicity
pat <- bounds (simpleExpr fname indents)
ty <- option
(PInfer (boundToFC fname pat))
(symbol ":" *> opExpr pdef fname indents)
rig <- getMult rigc
pure (rig, pat, ty))
pibindListName : FileName -> IndentInfo ->
Rule (List (RigCount, WithBounds Name, PTerm))
pibindListName fname indents
= do rigc <- multiplicity
= do rig <- multiplicity
ns <- sepBy1 (symbol ",") (bounds binderName)
symbol ":"
ty <- expr pdef fname indents
atEnd indents
rig <- getMult rigc
pure (map (\n => (rig, map UN n, ty)) (forget ns))
<|> forget <$> sepBy1 (symbol ",")
(do rigc <- multiplicity
(do rig <- multiplicity
n <- bounds binderName
symbol ":"
ty <- expr pdef fname indents
rig <- getMult rigc
pure (rig, map UN n, ty))
where
-- _ gets treated specially here, it means "I don't care about the name"
binderName : Rule String
binderName = unqualifiedName <|> (symbol "_" *> pure "_")
binderName = unqualifiedName <|> (symbol "_" $> "_")
pibindList : FileName -> IndentInfo ->
Rule (List (RigCount, WithBounds (Maybe Name), PTerm))
@ -484,8 +480,8 @@ mutual
bindSymbol : Rule (PiInfo PTerm)
bindSymbol
= (symbol "->" *> pure Explicit)
<|> (symbol "=>" *> pure AutoImplicit)
= (symbol "->" $> Explicit)
<|> (symbol "=>" $> AutoImplicit)
explicitPi : FileName -> IndentInfo -> Rule PTerm
explicitPi fname indents
@ -581,13 +577,12 @@ mutual
letBinder : Rule LetBinder
letBinder = do s <- bounds (MkPair <$> multiplicity <*> expr plhs fname indents)
(rigc, pat) <- pure s.val
(rig, pat) <- pure s.val
ty <- option (PImplicit (boundToFC fname s))
(symbol ":" *> typeExpr (pnoeq pdef) fname indents)
(symbol "=" <|> symbol ":=")
val <- expr pnowith fname indents
alts <- block (patAlt fname)
rig <- getMult rigc
pure (MkLetBinder rig pat ty val alts)
letDecl : Rule LetDecl
@ -642,7 +637,7 @@ mutual
record_ : FileName -> IndentInfo -> Rule PTerm
record_ fname indents
= do b <- bounds (do kw <- option False (keyword "record" *> pure True) -- TODO deprecated
= do b <- bounds (do kw <- option False (keyword "record" $> True) -- TODO deprecated
symbol "{"
commit
fs <- sepBy1 (symbol ",") (field kw fname indents)
@ -653,9 +648,9 @@ mutual
field : Bool -> FileName -> IndentInfo -> Rule PFieldUpdate
field kw fname indents
= do path <- map fieldName <$> [| name :: many recFieldCompat |]
upd <- (ifThenElse kw (symbol "=") (symbol ":=") *> pure PSetField)
upd <- (ifThenElse kw (symbol "=") (symbol ":=") $> PSetField)
<|>
(symbol "$=" *> pure PSetFieldApp)
(symbol "$=" $> PSetFieldApp)
val <- opExpr plhs fname indents
pure (upd path val)
where
@ -681,8 +676,7 @@ mutual
doBlock : FileName -> IndentInfo -> Rule PTerm
doBlock fname indents
= do b <- bounds (do keyword "do"
block (doAct fname))
= do b <- bounds $ keyword "do" *> block (doAct fname)
commit
pure (PDoBlock (boundToFC fname b) Nothing (concat b.val))
<|> do nsdo <- bounds namespacedIdent
@ -710,7 +704,7 @@ mutual
val <- expr pdef fname indents
pure (n, val))
atEnd indents
(n, val) <- pure b.val
let (n, val) = b.val
pure [DoBind (boundToFC fname b) (boundToFC fname n) n.val val]
<|> do keyword "let"
commit
@ -721,14 +715,10 @@ mutual
atEnd indents
pure [DoRewrite (boundToFC fname b) b.val]
<|> do e <- bounds (expr plhs fname indents)
(do atEnd indents
pure [DoExp (boundToFC fname e) e.val])
<|> (do b <- bounds (do symbol "<-"
val <- expr pnowith fname indents
alts <- block (patAlt fname)
pure (val, alts))
(atEnd indents $> [DoExp (boundToFC fname e) e.val])
<|> (do b <- bounds $ symbol "<-" *> [| (expr pnowith fname indents, block (patAlt fname)) |]
atEnd indents
(v, alts) <- pure b.val
let (v, alts) = b.val
let fc = boundToFC fname (mergeBounds e b)
pure [DoBindPat fc e.val v alts])
@ -762,9 +752,7 @@ mutual
typeExpr q fname indents
= do arg <- bounds (opExpr q fname indents)
(do continue indents
rest <- some (do exp <- bindSymbol
op <- bounds (opExpr pdef fname indents)
pure (exp, op))
rest <- some [| (bindSymbol, bounds $ opExpr pdef fname indents) |]
pure (mkPi arg (forget rest)))
<|> pure arg.val
where
@ -824,9 +812,9 @@ mutual
visOption : Rule Visibility
visOption
= (keyword "public" *> keyword "export" *> pure Public)
<|> (keyword "export" *> pure Export)
<|> (keyword "private" *> pure Private)
= (keyword "public" *> keyword "export" $> Public)
<|> (keyword "export" $> Export)
<|> (keyword "private" $> Private)
visibility : SourceEmptyRule Visibility
visibility
@ -835,10 +823,7 @@ visibility
tyDecls : Rule Name -> String -> FileName -> IndentInfo -> Rule (List1 PTypeDecl)
tyDecls declName predoc fname indents
= do bs <- do docns <- sepBy1 (symbol ",") (do
doc <- option "" documentation
n <- bounds declName
pure (doc, n))
= do bs <- do docns <- sepBy1 (symbol ",") [| (option "" documentation, bounds declName) |]
symbol ":"
mustWork $ do ty <- expr pdef fname indents
pure $ map (\(doc, n) => (doc, n.val, boundToFC fname n, ty))
@ -849,9 +834,7 @@ tyDecls declName predoc fname indents
withFlags : SourceEmptyRule (List WithFlag)
withFlags
= do pragma "syntactic"
fs <- withFlags
pure $ Syntactic :: fs
= pragma "syntactic" *> (Syntactic ::) <$> withFlags
<|> pure []
mutual
@ -859,10 +842,7 @@ mutual
FileName -> WithBounds t -> Int ->
IndentInfo -> (lhs : PTerm) -> Rule PClause
parseRHS withArgs fname start col indents lhs
= do b <- bounds (symbol "=" *> mustWork (
do rhs <- expr pdef fname indents
ws <- option [] (whereBlock fname col)
pure (rhs, ws)))
= do b <- bounds $ symbol "=" *> mustWork [| (expr pdef fname indents, option [] $ whereBlock fname col) |]
atEnd indents
(rhs, ws) <- pure b.val
let fc = boundToFC fname (mergeBounds start b)
@ -947,13 +927,11 @@ simpleData fname start n indents
dataOpt : Rule DataOpt
dataOpt
= (exactIdent "noHints" *> pure NoHints)
<|> (exactIdent "uniqueSearch" *> pure UniqueSearch)
<|> do exactIdent "search"
ns <- forget <$> some name
pure (SearchBy ns)
<|> (exactIdent "external" *> pure External)
<|> (exactIdent "noNewtype" *> pure NoNewtype)
= (exactIdent "noHints" $> NoHints)
<|> (exactIdent "uniqueSearch" $> UniqueSearch)
<|> (exactIdent "search" *> SearchBy <$> forget <$> some name)
<|> (exactIdent "external" $> External)
<|> (exactIdent "noNewtype" $> NoNewtype)
dataBody : FileName -> Int -> WithBounds t -> Name -> IndentInfo -> PTerm ->
SourceEmptyRule PDataDecl
@ -961,10 +939,7 @@ dataBody fname mincol start n indents ty
= do atEndIndent indents
pure (MkPLater (boundToFC fname start) n ty)
<|> do b <- bounds (do keyword "where"
opts <- option [] (do symbol "["
dopts <- sepBy1 (symbol ",") dataOpt
symbol "]"
pure $ forget dopts)
opts <- option [] $ symbol "[" *> forget <$> sepBy1 (symbol ",") dataOpt <* symbol "]"
cs <- blockAfter mincol (tyDecls (mustWork dataConstructorName) "" fname)
pure (opts, concatMap forget cs))
(opts, cs) <- pure b.val
@ -1004,19 +979,19 @@ stripBraces str = pack (drop '{' (reverse (drop '}' (reverse (unpack str)))))
onoff : Rule Bool
onoff
= (exactIdent "on" *> pure True)
<|> (exactIdent "off" *> pure False)
= (exactIdent "on" $> True)
<|> (exactIdent "off" $> False)
extension : Rule LangExt
extension
= (exactIdent "ElabReflection" *> pure ElabReflection)
<|> (exactIdent "Borrowing" *> pure Borrowing)
= (exactIdent "ElabReflection" $> ElabReflection)
<|> (exactIdent "Borrowing" $> Borrowing)
totalityOpt : Rule TotalReq
totalityOpt
= (keyword "partial" *> pure PartialOK)
<|> (keyword "total" *> pure Total)
<|> (keyword "covering" *> pure CoveringOnly)
= (keyword "partial" $> PartialOK)
<|> (keyword "total" $> Total)
<|> (keyword "covering" $> CoveringOnly)
logLevel : Rule (Maybe LogLevel)
logLevel
@ -1115,10 +1090,10 @@ directive fname indents
fix : Rule Fixity
fix
= (keyword "infixl" *> pure InfixL)
<|> (keyword "infixr" *> pure InfixR)
<|> (keyword "infix" *> pure Infix)
<|> (keyword "prefix" *> pure Prefix)
= (keyword "infixl" $> InfixL)
<|> (keyword "infixr" $> InfixR)
<|> (keyword "infix" $> Infix)
<|> (keyword "prefix" $> Prefix)
namespaceHead : Rule Namespace
namespaceHead = keyword "namespace" *> mustWork namespaceId
@ -1154,22 +1129,6 @@ mutualDecls fname indents
= do ds <- bounds (keyword "mutual" *> commit *> assert_total (nonEmptyBlock (topDecl fname)))
pure (PMutual (boundToFC fname ds) (concat ds.val))
paramDecls : FileName -> IndentInfo -> Rule PDecl
paramDecls fname indents
= do b <- bounds (do keyword "parameters"
commit
symbol "("
ps <- sepBy (symbol ",")
(do x <- unqualifiedName
symbol ":"
ty <- typeExpr pdef fname indents
pure (UN x, ty))
symbol ")"
ds <- assert_total (nonEmptyBlock (topDecl fname))
pure (ps, ds))
(ps, ds) <- pure b.val
pure (PParameters (boundToFC fname b) ps (collectDefs (concat ds)))
usingDecls : FileName -> IndentInfo -> Rule PDecl
usingDecls fname indents
= do b <- bounds (do keyword "using"
@ -1217,6 +1176,20 @@ fnDirectOpt fname
cs <- block (expr pdef fname)
pure $ PForeign cs
builtinType : Rule BuiltinType
builtinType =
BuiltinNatural <$ exactIdent "Natural"
builtinDecl : FileName -> IndentInfo -> Rule PDecl
builtinDecl fname indents
= do b <- bounds (do pragma "builtin"
commit
t <- builtinType
n <- name
pure (t, n))
(t, n) <- pure b.val
pure $ PBuiltin (boundToFC fname b) t n
visOpt : FileName -> Rule (Either Visibility PFnOpt)
visOpt fname
= do vis <- visOption
@ -1260,8 +1233,7 @@ constraints fname indents
implBinds : FileName -> IndentInfo -> SourceEmptyRule (List (Name, RigCount, PTerm))
implBinds fname indents
= do symbol "{"
m <- multiplicity
rig <- getMult m
rig <- multiplicity
n <- name
symbol ":"
tm <- expr pdef fname indents
@ -1274,8 +1246,7 @@ implBinds fname indents
ifaceParam : FileName -> IndentInfo -> Rule (List Name, (RigCount, PTerm))
ifaceParam fname indents
= do symbol "("
m <- multiplicity
rig <- getMult m
rig <- multiplicity
ns <- sepBy1 (symbol ",") name
symbol ":"
tm <- expr pdef fname indents
@ -1295,9 +1266,7 @@ ifaceDecl fname indents
n <- name
paramss <- many (ifaceParam fname indents)
let params = concatMap (\ (ns, rt) => map (\ n => (n, rt)) ns) paramss
det <- option []
(do symbol "|"
sepBy (symbol ",") name)
det <- option [] $ symbol "|" *> sepBy (symbol ",") name
keyword "where"
dc <- optional recordConstructor
body <- assert_total (blockAfter col (topDecl fname))
@ -1313,19 +1282,13 @@ implDecl fname indents
let opts = mapMaybe getRight visOpts
col <- column
option () (keyword "implementation")
iname <- optional (do symbol "["
iname <- name
symbol "]"
pure iname)
iname <- optional $ symbol "[" *> name <* symbol "]"
impls <- implBinds fname indents
cons <- constraints fname indents
n <- name
params <- many (simpleExpr fname indents)
nusing <- option [] (do keyword "using"
names <- some name
pure $ forget names)
body <- optional (do keyword "where"
blockAfter col (topDecl fname))
nusing <- option [] $ keyword "using" *> forget <$> some name
body <- optional $ keyword "where" *> blockAfter col (topDecl fname)
pure $ \fc : FC =>
(PImplementation fc vis opts Single impls cons n params iname nusing
(map (collectDefs . concat) body)))
@ -1349,16 +1312,15 @@ fieldDecl fname indents
where
fieldBody : String -> PiInfo PTerm -> Rule (List PField)
fieldBody doc p
= do b <- bounds (do m <- multiplicity
rig <- getMult m
= do b <- bounds (do rig <- multiplicity
ns <- sepBy1 (symbol ",") name
symbol ":"
ty <- expr pdef fname indents
pure (\fc : FC => map (\n => MkField fc doc rig p n ty) (forget ns)))
pure (b.val (boundToFC fname b))
recordParam : FileName -> IndentInfo -> Rule (List (Name, RigCount, PiInfo PTerm, PTerm))
recordParam fname indents
typedArg : FileName -> IndentInfo -> Rule (List (Name, RigCount, PiInfo PTerm, PTerm))
typedArg fname indents
= do symbol "("
params <- pibindListName fname indents
symbol ")"
@ -1367,14 +1329,15 @@ recordParam fname indents
commit
info <- the (SourceEmptyRule (PiInfo PTerm))
(pure AutoImplicit <* keyword "auto"
<|>(do
keyword "default"
t <- simpleExpr fname indents
pure $ DefImplicit t)
<|> (keyword "default" *> DefImplicit <$> simpleExpr fname indents)
<|> pure Implicit)
params <- pibindListName fname indents
symbol "}"
pure $ map (\(c, n, tm) => (n.val, c, info, tm)) params
recordParam : FileName -> IndentInfo -> Rule (List (Name, RigCount, PiInfo PTerm, PTerm))
recordParam fname indents
= typedArg fname indents
<|> do n <- bounds name
pure [(n.val, top, Explicit, PInfer (boundToFC fname n))]
@ -1394,6 +1357,33 @@ recordDecl fname indents
pure (\fc : FC => PRecord fc doc vis n params (fst dcflds) (concat (snd dcflds))))
pure (b.val (boundToFC fname b))
paramDecls : FileName -> IndentInfo -> Rule PDecl
paramDecls fname indents
= do b1 <- bounds (keyword "parameters")
commit
args <- bounds (newParamDecls fname indents <|> oldParamDecls fname indents)
commit
declarations <- the (Rule (WithBounds (List1 (List PDecl)))) (assert_total (Core.bounds $ nonEmptyBlock (topDecl fname)))
mergedBounds <- pure $ b1 `mergeBounds` (args `mergeBounds` declarations)
pure (PParameters (boundToFC fname mergedBounds) args.val (collectDefs (concat declarations.val)))
where
oldParamDecls : FileName -> IndentInfo -> Rule (List (Name, RigCount, PiInfo PTerm, PTerm))
oldParamDecls fname indents
= do symbol "("
ps <- sepBy (symbol ",")
(do x <- unqualifiedName
symbol ":"
ty <- typeExpr pdef fname indents
pure (UN x, top, Explicit, ty))
symbol ")"
pure ps
newParamDecls : FileName -> IndentInfo -> Rule (List (Name, RigCount, PiInfo PTerm, PTerm))
newParamDecls fname indents
= map concat (some $ typedArg fname indents)
claims : FileName -> IndentInfo -> Rule (List1 PDecl)
claims fname indents
= do bs <- bounds (do
@ -1401,8 +1391,7 @@ claims fname indents
visOpts <- many (visOpt fname)
vis <- getVisibility Nothing visOpts
let opts = mapMaybe getRight visOpts
m <- multiplicity
rig <- getMult m
rig <- multiplicity
cls <- tyDecls name doc fname indents
pure $ map (\cl => the (Pair _ _) (doc, vis, opts, rig, cl)) cls)
pure $ map (\(doc, vis, opts, rig, cl) : Pair _ _ =>
@ -1459,6 +1448,8 @@ topDecl fname indents
pure [d]
<|> do d <- usingDecls fname indents
pure [d]
<|> do d <- builtinDecl fname indents
pure [d]
<|> do d <- runElabDecl fname indents
pure [d]
<|> do d <- transformDecl fname indents
@ -1466,9 +1457,9 @@ topDecl fname indents
<|> do d <- directiveDecl fname indents
pure [d]
<|> do dstr <- bounds (terminal "Expected CG directive"
(\x => case x of
CGDirective d => Just d
_ => Nothing))
(\case
CGDirective d => Just d
_ => Nothing))
pure [let cgrest = span isAlphaNum dstr.val in
PDirective (boundToFC fname dstr)
(CGAction (fst cgrest) (stripBraces (trim (snd cgrest))))]
@ -1502,8 +1493,7 @@ export
import_ : FileName -> IndentInfo -> Rule Import
import_ fname indents
= do b <- bounds (do keyword "import"
reexp <- option False (do keyword "public"
pure True)
reexp <- option False (keyword "public" $> True)
ns <- mustWork moduleIdent
nsAs <- option (miAsNamespace ns)
(do exactIdent "as"
@ -1575,6 +1565,8 @@ setOption set
pure (ShowNamespace set)
<|> do exactIdent "showtypes"
pure (ShowTypes set)
<|> do exactIdent "profile"
pure (Profile set)
<|> if set then setVarOption else fatalError "Unrecognised option"
replCmd : List String -> Rule ()
@ -1593,25 +1585,25 @@ editCmd
n <- name
pure (TypeAt (fromInteger line) (fromInteger col) n)
<|> do replCmd ["cs"]
upd <- option False (symbol "!" *> pure True)
upd <- option False (symbol "!" $> True)
line <- intLit
col <- intLit
n <- name
pure (CaseSplit upd (fromInteger line) (fromInteger col) n)
<|> do replCmd ["ac"]
upd <- option False (symbol "!" *> pure True)
upd <- option False (symbol "!" $> True)
line <- intLit
n <- name
pure (AddClause upd (fromInteger line) n)
<|> do replCmd ["ps", "proofsearch"]
upd <- option False (symbol "!" *> pure True)
upd <- option False (symbol "!" $> True)
line <- intLit
n <- name
pure (ExprSearch upd (fromInteger line) n [])
<|> do replCmd ["psnext"]
pure ExprSearchNext
<|> do replCmd ["gd"]
upd <- option False (symbol "!" *> pure True)
upd <- option False (symbol "!" $> True)
line <- intLit
n <- name
nreject <- option 0 intLit
@ -1619,17 +1611,17 @@ editCmd
<|> do replCmd ["gdnext"]
pure GenerateDefNext
<|> do replCmd ["ml", "makelemma"]
upd <- option False (symbol "!" *> pure True)
upd <- option False (symbol "!" $> True)
line <- intLit
n <- name
pure (MakeLemma upd (fromInteger line) n)
<|> do replCmd ["mc", "makecase"]
upd <- option False (symbol "!" *> pure True)
upd <- option False (symbol "!" $> True)
line <- intLit
n <- name
pure (MakeCase upd (fromInteger line) n)
<|> do replCmd ["mw", "makewith"]
upd <- option False (symbol "!" *> pure True)
upd <- option False (symbol "!" $> True)
line <- intLit
n <- name
pure (MakeWith upd (fromInteger line) n)
@ -1873,6 +1865,7 @@ loggingArgCmd parseCmd command doc = (names, Args [StringArg, NumberArg], doc, p
parserCommandsForHelp : CommandTable
parserCommandsForHelp =
[ exprArgCmd (ParseREPLCmd ["t", "type"]) Check "Check the type of an expression"
, exprArgCmd (ParseREPLCmd ["ti"]) CheckWithImplicits "Check the type of an expression, showing implicit arguments"
, nameArgCmd (ParseREPLCmd ["printdef"]) PrintDef "Show the definition of a function"
, exprArgCmd (ParseREPLCmd ["s", "search"]) TypeSearch "Search for values by type"
, nameArgCmd (ParseIdentCmd "di") DebugInfo "Show debugging information for a name"
@ -1883,6 +1876,7 @@ parserCommandsForHelp =
, stringArgCmd (ParseREPLCmd ["sh"]) RunShellCommand "Run a shell command"
, optArgCmd (ParseIdentCmd "set") SetOpt True "Set an option"
, optArgCmd (ParseIdentCmd "unset") SetOpt False "Unset an option"
, noArgCmd (ParseREPLCmd ["opts"]) GetOpts "Show current options settings"
, compileArgsCmd (ParseREPLCmd ["c", "compile"]) Compile "Compile to an executable"
, exprArgCmd (ParseIdentCmd "exec") Exec "Compile to an executable and run"
, stringArgCmd (ParseIdentCmd "directive") CGDirective "Set a codegen-specific directive"
@ -1900,6 +1894,8 @@ parserCommandsForHelp =
, noArgCmd (ParseREPLCmd ["version"]) ShowVersion "Display the Idris version"
, noArgCmd (ParseREPLCmd ["?", "h", "help"]) Help "Display this help text"
, declsArgCmd (ParseKeywordCmd "let") NewDefn "Define a new value"
, stringArgCmd (ParseREPLCmd ["lp", "loadpackage"]) ImportPackage "Load all modules of the package"
, exprArgCmd (ParseREPLCmd ["fs", "fsearch"]) FuzzyTypeSearch "Search for global definitions by sketching the names distribution of the wanted type(s)."
]
export
@ -1920,10 +1916,8 @@ eval = do
export
command : SourceEmptyRule REPLCmd
command
= do eoi
pure NOP
= eoi $> NOP
<|> nonEmptyCommand
<|> do symbol ":?"; pure Help -- special case, :? doesn't fit into above scheme
<|> do symbol ":"; cmd <- editCmd
pure (Editing cmd)
<|> symbol ":?" $> Help -- special case, :? doesn't fit into above scheme
<|> symbol ":" *> Editing <$> editCmd
<|> eval

View File

@ -4,17 +4,27 @@ import Data.List
import Data.Maybe
import Data.Strings
import Libraries.Control.ANSI.SGR
import Parser.Lexer.Source
import public Idris.Pretty.Render
import public Libraries.Text.PrettyPrint.Prettyprinter
import public Libraries.Text.PrettyPrint.Prettyprinter.Render.Terminal
import public Libraries.Text.PrettyPrint.Prettyprinter.Util
import Algebra
import Idris.REPLOpts
import Idris.REPL.Opts
import Idris.Syntax
import Libraries.Utils.Term
%default covering
public export
data IdrisSyntax
= SynHole
| SynKeyword
| SynPragma
| SynRef Name
public export
data IdrisAnn
= Warning
@ -23,8 +33,7 @@ data IdrisAnn
| FileCtxt
| Code
| Meta
| Keyword
| Pragma
| Syntax IdrisSyntax
export
colorAnn : IdrisAnn -> AnsiStyle
@ -33,9 +42,11 @@ colorAnn Error = color BrightRed <+> bold
colorAnn ErrorDesc = bold
colorAnn FileCtxt = color BrightBlue
colorAnn Code = color Magenta
colorAnn Keyword = color Red
colorAnn Pragma = color BrightMagenta
colorAnn Meta = color Green
colorAnn (Syntax SynHole) = color Green
colorAnn (Syntax SynKeyword) = color Red
colorAnn (Syntax SynPragma) = color BrightMagenta
colorAnn (Syntax (SynRef _)) = []
export
error : Doc IdrisAnn -> Doc IdrisAnn
@ -50,53 +61,57 @@ fileCtxt : Doc IdrisAnn -> Doc IdrisAnn
fileCtxt = annotate FileCtxt
export
keyword : Doc IdrisAnn -> Doc IdrisAnn
keyword = annotate Keyword
keyword : Doc IdrisSyntax -> Doc IdrisSyntax
keyword = annotate SynKeyword
export
meta : Doc IdrisAnn -> Doc IdrisAnn
meta = annotate Meta
export
hole : Doc IdrisSyntax -> Doc IdrisSyntax
hole = annotate SynHole
export
code : Doc IdrisAnn -> Doc IdrisAnn
code = annotate Code
let_ : Doc IdrisAnn
let_ : Doc IdrisSyntax
let_ = keyword (pretty "let")
in_ : Doc IdrisAnn
in_ : Doc IdrisSyntax
in_ = keyword (pretty "in")
case_ : Doc IdrisAnn
case_ : Doc IdrisSyntax
case_ = keyword (pretty "case")
of_ : Doc IdrisAnn
of_ : Doc IdrisSyntax
of_ = keyword (pretty "of")
do_ : Doc IdrisAnn
do_ : Doc IdrisSyntax
do_ = keyword (pretty "do")
with_ : Doc IdrisAnn
with_ : Doc IdrisSyntax
with_ = keyword (pretty "with")
record_ : Doc IdrisAnn
record_ : Doc IdrisSyntax
record_ = keyword (pretty "record")
impossible_ : Doc IdrisAnn
impossible_ : Doc IdrisSyntax
impossible_ = keyword (pretty "impossible")
auto_ : Doc IdrisAnn
auto_ : Doc IdrisSyntax
auto_ = keyword (pretty "auto")
default_ : Doc IdrisAnn
default_ : Doc IdrisSyntax
default_ = keyword (pretty "default")
rewrite_ : Doc IdrisAnn
rewrite_ : Doc IdrisSyntax
rewrite_ = keyword (pretty "rewrite")
export
pragma : Doc IdrisAnn -> Doc IdrisAnn
pragma = annotate Pragma
pragma : Doc IdrisSyntax -> Doc IdrisSyntax
pragma = annotate SynPragma
export
prettyRig : RigCount -> Doc ann
@ -105,7 +120,7 @@ prettyRig = elimSemi (pretty '0' <+> space)
(const emptyDoc)
mutual
prettyAlt : PClause -> Doc IdrisAnn
prettyAlt : PClause -> Doc IdrisSyntax
prettyAlt (MkPatClause _ lhs rhs _) =
space <+> pipe <++> prettyTerm lhs <++> pretty "=>" <++> prettyTerm rhs <+> semi
prettyAlt (MkWithClause _ lhs wval prf flags cs) =
@ -113,7 +128,7 @@ mutual
prettyAlt (MkImpossible _ lhs) =
space <+> pipe <++> prettyTerm lhs <++> impossible_ <+> semi
prettyCase : PClause -> Doc IdrisAnn
prettyCase : PClause -> Doc IdrisSyntax
prettyCase (MkPatClause _ lhs rhs _) =
prettyTerm lhs <++> pretty "=>" <++> prettyTerm rhs
prettyCase (MkWithClause _ lhs rhs prf flags _) =
@ -121,11 +136,11 @@ mutual
prettyCase (MkImpossible _ lhs) =
prettyTerm lhs <++> impossible_
prettyString : PStr -> Doc IdrisAnn
prettyString : PStr -> Doc IdrisSyntax
prettyString (StrLiteral _ str) = pretty str
prettyString (StrInterp _ tm) = prettyTerm tm
prettyDo : PDo -> Doc IdrisAnn
prettyDo : PDo -> Doc IdrisSyntax
prettyDo (DoExp _ tm) = prettyTerm tm
prettyDo (DoBind _ _ n tm) = pretty n <++> pretty "<-" <++> prettyTerm tm
prettyDo (DoBindPat _ l tm alts) =
@ -138,14 +153,14 @@ mutual
let_ <++> braces (angles (angles (pretty "definitions")))
prettyDo (DoRewrite _ rule) = rewrite_ <+> prettyTerm rule
prettyUpdate : PFieldUpdate -> Doc IdrisAnn
prettyUpdate : PFieldUpdate -> Doc IdrisSyntax
prettyUpdate (PSetField path v) =
concatWith (surround dot) (pretty <$> path) <++> equals <++> prettyTerm v
prettyUpdate (PSetFieldApp path v) =
concatWith (surround dot) (pretty <$> path) <++> pretty '$' <+> equals <++> prettyTerm v
export
prettyTerm : PTerm -> Doc IdrisAnn
prettyTerm : PTerm -> Doc IdrisSyntax
prettyTerm = go Open
where
startPrec : Prec
@ -154,9 +169,13 @@ mutual
appPrec = User 10
leftAppPrec : Prec
leftAppPrec = User 9
prettyOp : OpStr -> Doc IdrisSyntax
prettyOp op = if isOpName op
then annotate (SynRef op) $ pretty op
else Chara '`' <+> annotate (SynRef op) (pretty op) <+> Chara '`'
go : Prec -> PTerm -> Doc IdrisAnn
go d (PRef _ n) = pretty n
go : Prec -> PTerm -> Doc IdrisSyntax
go d (PRef _ n) = annotate (SynRef n) $ pretty n
go d (PPi _ rig Explicit Nothing arg ret) =
parenthesise (d > startPrec) $ group $
branchVal
@ -195,7 +214,7 @@ mutual
getLamNames : List (RigCount, PTerm, PTerm) -> PTerm -> (List (RigCount, PTerm, PTerm), PTerm)
getLamNames acc (PLam _ rig _ n ty sc) = getLamNames ((rig, n, ty) :: acc) sc
getLamNames acc sc = (reverse acc, sc)
prettyBindings : List (RigCount, PTerm, PTerm) -> Doc IdrisAnn
prettyBindings : List (RigCount, PTerm, PTerm) -> Doc IdrisSyntax
prettyBindings [] = neutral
prettyBindings [(rig, n, (PImplicit _))] = prettyRig rig <+> go startPrec n
prettyBindings [(rig, n, ty)] = prettyRig rig <+> go startPrec n <++> colon <++> go startPrec ty
@ -223,10 +242,10 @@ mutual
where
continuation : Doc IdrisAnn
continuation : Doc IdrisSyntax
continuation = go startPrec sc
fullLet : Doc IdrisAnn
fullLet : Doc IdrisSyntax
fullLet = parenthesise (d > startPrec) $ group $ align $
let_ <++> (group $ align $ hang 2 $ prettyRig rig <+> go startPrec n <++> equals <+> line <+> go startPrec val) <+> line
<+> in_ <++> (group $ align $ hang 2 $ continuation)
@ -269,16 +288,16 @@ mutual
go d (PUnquote _ tm) = parenthesise (d > appPrec) $ "~" <+> parens (go startPrec tm)
go d (PRunElab _ tm) = parenthesise (d > appPrec) $ pragma "%runElab" <++> go startPrec tm
go d (PPrimVal _ c) = pretty c
go d (PHole _ _ n) = meta (pretty (strCons '?' n))
go d (PHole _ _ n) = hole (pretty (strCons '?' n))
go d (PType _) = pretty "Type"
go d (PAs _ _ n p) = pretty n <+> "@" <+> go d p
go d (PDotted _ p) = dot <+> go d p
go d (PImplicit _) = "_"
go d (PInfer _) = "?"
go d (POp _ op x y) = parenthesise (d > appPrec) $ group $ go startPrec x <++> pretty op <++> go startPrec y
go d (POp _ op x y) = parenthesise (d > appPrec) $ group $ go startPrec x <++> prettyOp op <++> go startPrec y
go d (PPrefixOp _ op x) = parenthesise (d > appPrec) $ pretty op <+> go startPrec x
go d (PSectionL _ op x) = parens (pretty op <++> go startPrec x)
go d (PSectionR _ x op) = parens (go startPrec x <++> pretty op)
go d (PSectionL _ op x) = parens (prettyOp op <++> go startPrec x)
go d (PSectionR _ x op) = parens (go startPrec x <++> prettyOp op)
go d (PEq fc l r) = parenthesise (d > appPrec) $ go startPrec l <++> equals <++> go startPrec r
go d (PBracketed _ tm) = parens (go startPrec tm)
go d (PString _ xs) = parenthesise (d > appPrec) $ hsep $ punctuate "++" (prettyString <$> xs)
@ -320,29 +339,6 @@ mutual
parens (dot <+> concatWith (surround dot) (map pretty fields))
go d (PWithUnambigNames fc ns rhs) = parenthesise (d > appPrec) $ group $ with_ <++> pretty ns <+> line <+> go startPrec rhs
getPageWidth : {auto o : Ref ROpts REPLOpts} -> Core PageWidth
getPageWidth = do
consoleWidth <- getConsoleWidth
case consoleWidth of
Nothing => do
cols <- coreLift getTermCols
pure $ if cols == 0 then Unbounded else AvailablePerLine cols 1
Just 0 => pure $ Unbounded
Just cw => pure $ AvailablePerLine (cast cw) 1
export
render : {auto o : Ref ROpts REPLOpts} -> Doc IdrisAnn -> Core String
render doc = do
color <- getColor
pageWidth <- getPageWidth
let opts = MkLayoutOptions pageWidth
let layout = layoutPretty opts doc
pure $ renderString $ if color then reAnnotateS colorAnn layout else unAnnotateS layout
export
renderWithoutColor : {auto o : Ref ROpts REPLOpts} -> Doc IdrisAnn -> Core String
renderWithoutColor doc = do
pageWidth <- getPageWidth
let opts = MkLayoutOptions pageWidth
let layout = layoutPretty opts doc
pure $ renderString $ unAnnotateS layout
render = render colorAnn

View File

@ -0,0 +1,40 @@
module Idris.Pretty.Render
import Core.Core
import Idris.REPL.Opts
import Libraries.Control.ANSI.SGR
import Libraries.Text.PrettyPrint.Prettyprinter
import public Libraries.Text.PrettyPrint.Prettyprinter.Render.Terminal
import Libraries.Utils.Term
getPageWidth : {auto o : Ref ROpts REPLOpts} -> Core PageWidth
getPageWidth = do
consoleWidth <- getConsoleWidth
case consoleWidth of
Nothing => do
cols <- coreLift getTermCols
pure $ if cols == 0 then Unbounded else AvailablePerLine cols 1
Just 0 => pure $ Unbounded
Just cw => pure $ AvailablePerLine (cast cw) 1
export
render : {auto o : Ref ROpts REPLOpts} ->
(ann -> AnsiStyle) ->
Doc ann -> Core String
render stylerAnn doc = do
color <- getColor
pageWidth <- getPageWidth
let opts = MkLayoutOptions pageWidth
let layout = layoutPretty opts doc
pure $ renderString $
if color then reAnnotateS stylerAnn layout else unAnnotateS layout
export
renderWithoutColor : {auto o : Ref ROpts REPLOpts} -> Doc ann -> Core String
renderWithoutColor doc = do
pageWidth <- getPageWidth
let opts = MkLayoutOptions pageWidth
let layout = layoutPretty opts doc
pure $ renderString $ unAnnotateS layout

View File

@ -21,8 +21,8 @@ import TTImp.TTImp
import Idris.Desugar
import Idris.Parser
import Idris.REPLCommon
import Idris.REPLOpts
import Idris.REPL.Common
import Idris.REPL.Opts
import Idris.Syntax
import Idris.Pretty

View File

@ -38,10 +38,12 @@ import Idris.Parser
import Idris.Pretty
import Idris.ProcessIdr
import Idris.Resugar
import public Idris.REPLCommon
import Idris.Syntax
import Idris.Version
import public Idris.REPL.Common
import Idris.REPL.FuzzySearch
import TTImp.Elab
import TTImp.Elab.Check
import TTImp.Elab.Local
@ -58,15 +60,21 @@ import Data.List1
import Data.Maybe
import Libraries.Data.ANameMap
import Libraries.Data.NameMap
import Libraries.Data.PosMap
import Data.Stream
import Data.Strings
import Data.DPair
import Libraries.Data.String.Extra
import Libraries.Data.List.Extra
import Libraries.Text.PrettyPrint.Prettyprinter
import Libraries.Text.PrettyPrint.Prettyprinter.Util
import Libraries.Text.PrettyPrint.Prettyprinter.Render.Terminal
import Libraries.Utils.Path
import Libraries.System.Directory.Tree
import System
import System.File
import System.Directory
%hide Data.Strings.lines
%hide Data.Strings.lines'
@ -98,6 +106,9 @@ showInfo (n, idx, d)
coreLift_ $ putStrLn $
"Size change: " ++ showSep ", " scinfo
prettyTerm : PTerm -> Doc IdrisAnn
prettyTerm = reAnnotate Syntax . Idris.Pretty.prettyTerm
displayType : {auto c : Ref Ctxt Defs} ->
{auto s : Ref Syn SyntaxInfo} ->
Defs -> (Name, Int, GlobalDef) ->
@ -105,7 +116,7 @@ displayType : {auto c : Ref Ctxt Defs} ->
displayType defs (n, i, gdef)
= maybe (do tm <- resugar [] !(normaliseHoles defs [] (type gdef))
pure (pretty !(aliasName (fullname gdef)) <++> colon <++> prettyTerm tm))
(\num => prettyHole defs [] n num (type gdef))
(\num => reAnnotate Syntax <$> prettyHole defs [] n num (type gdef))
(isHole gdef)
getEnvTerm : {vars : _} ->
@ -177,6 +188,9 @@ setOpt (CG e)
case getCG (options defs) e of
Just cg => setCG cg
Nothing => iputStrLn (reflow "No such code generator available")
setOpt (Profile t)
= do pp <- getSession
setSession (record { profile = t } pp)
getOptions : {auto c : Ref Ctxt Defs} ->
{auto o : Ref ROpts REPLOpts} ->
@ -236,14 +250,6 @@ lookupDefTyName : Name -> Context ->
Core (List (Name, Int, (Def, ClosedTerm)))
lookupDefTyName = lookupNameBy (\g => (definition g, type g))
public export
data EditResult : Type where
DisplayEdit : Doc IdrisAnn -> EditResult
EditError : Doc IdrisAnn -> EditResult
MadeLemma : Maybe String -> Name -> PTerm -> String -> EditResult
MadeWith : Maybe String -> List String -> EditResult
MadeCase : Maybe String -> List String -> EditResult
updateFile : {auto r : Ref ROpts REPLOpts} ->
(List String -> List String) -> Core EditResult
updateFile update
@ -359,6 +365,16 @@ dropLamsTm Z env tm = (_ ** (env, tm))
dropLamsTm (S k) env (Bind _ _ b sc) = dropLamsTm k (b :: env) sc
dropLamsTm _ env tm = (_ ** (env, tm))
findInTree : FilePos -> Name -> PosMap (NonEmptyFC, Name) -> Maybe Name
findInTree p hint m = map snd $ head' $ filter match $ sortBy (\x, y => cmp (measure x) (measure y)) $ searchPos p m
where
cmp : FileRange -> FileRange -> Ordering
cmp ((sr1, sc1), (er1, ec1)) ((sr2, sc2), (er2, ec2)) =
compare (er1 - sr1, ec1 - sc1) (er2 - sr2, ec2 - sc2)
match : (NonEmptyFC, Name) -> Bool
match (_, n) = matches hint n && userNameRoot n == userNameRoot hint
processEdit : {auto c : Ref Ctxt Defs} ->
{auto u : Ref UST UState} ->
{auto s : Ref Syn SyntaxInfo} ->
@ -367,6 +383,11 @@ processEdit : {auto c : Ref Ctxt Defs} ->
EditCmd -> Core EditResult
processEdit (TypeAt line col name)
= do defs <- get Ctxt
meta <- get MD
-- Search the correct name by location for more precise search
-- and fallback to given name if nothing found
let name = fromMaybe name $ findInTree (line - 1, col - 1) name (nameLocMap meta)
-- Lookup the name globally
globals <- lookupCtxtName name (gamma defs)
@ -525,43 +546,6 @@ processEdit (MakeWith upd line name)
then updateFile (addMadeCase markM w (max 0 (integerToNat (cast (line - 1)))))
else pure $ MadeWith markM w
public export
data MissedResult : Type where
CasesMissing : Name -> List String -> MissedResult
CallsNonCovering : Name -> List Name -> MissedResult
AllCasesCovered : Name -> MissedResult
public export
data REPLResult : Type where
Done : REPLResult
REPLError : Doc IdrisAnn -> REPLResult
Executed : PTerm -> REPLResult
RequestedHelp : REPLResult
Evaluated : PTerm -> (Maybe PTerm) -> REPLResult
Printed : Doc IdrisAnn -> REPLResult
TermChecked : PTerm -> PTerm -> REPLResult
FileLoaded : String -> REPLResult
ModuleLoaded : String -> REPLResult
ErrorLoadingModule : String -> Error -> REPLResult
ErrorLoadingFile : String -> FileError -> REPLResult
ErrorsBuildingFile : String -> List Error -> REPLResult
NoFileLoaded : REPLResult
CurrentDirectory : String -> REPLResult
CompilationFailed: REPLResult
Compiled : String -> REPLResult
ProofFound : PTerm -> REPLResult
Missed : List MissedResult -> REPLResult
CheckedTotal : List (Name, Totality) -> REPLResult
FoundHoles : List HoleData -> REPLResult
OptionsSet : List REPLOpt -> REPLResult
LogLevelSet : Maybe LogLevel -> REPLResult
ConsoleWidthSet : Maybe Nat -> REPLResult
ColorSet : Bool -> REPLResult
VersionIs : Version -> REPLResult
DefDeclared : REPLResult
Exited : REPLResult
Edited : EditResult -> REPLResult
getItDecls :
{auto o : Ref ROpts REPLOpts} ->
Core (List ImpDecl)
@ -666,45 +650,67 @@ loadMainFile f
[] => pure (FileLoaded f)
_ => pure (ErrorsBuildingFile f errs)
docsOrSignature : {auto c : Ref Ctxt Defs} ->
{auto s : Ref Syn SyntaxInfo} ->
FC -> Name -> Core (List String)
docsOrSignature fc n
= do syn <- get Syn
defs <- get Ctxt
all@(_ :: _) <- lookupCtxtName n (gamma defs)
| _ => undefinedName fc n
let ns@(_ :: _) = concatMap (\n => lookupName n (docstrings syn))
(map fst all)
| [] => typeSummary defs
getDocsForName fc n
where
typeSummary : Defs -> Core (List String)
typeSummary defs = do Just def <- lookupCtxtExact n (gamma defs)
| Nothing => pure []
ty <- normaliseHoles defs [] (type def)
pure [(show n) ++ " : " ++ (show !(resugar [] ty))]
||| Given a REPLEval mode for evaluation,
||| produce the normalization function that normalizes terms
||| using that evaluation mode
replEval : {auto c : Ref Ctxt Defs} ->
{vs : _} ->
REPLEval -> Defs -> Env Term vs -> Term vs -> Core (Term vs)
replEval NormaliseAll = normaliseAll
replEval _ = normalise
record TermWithType where
constructor WithType
termOf : Term []
typeOf : Term []
||| Produce the elaboration of a PTerm, along with its inferred type
inferAndElab : {auto c : Ref Ctxt Defs} ->
{auto u : Ref UST UState} ->
{auto s : Ref Syn SyntaxInfo} ->
{auto m : Ref MD Metadata} ->
{auto o : Ref ROpts REPLOpts} ->
ElabMode ->
PTerm ->
Core TermWithType
inferAndElab emode itm
= do ttimp <- desugar AnyExpr [] itm
let ttimpWithIt = ILocal replFC !getItDecls ttimp
inidx <- resolveName (UN "[input]")
-- a TMP HACK to prioritise list syntax for List: hide
-- foreign argument lists. TODO: once the new FFI is fully
-- up and running we won't need this. Also, if we add
-- 'with' disambiguation we can use that instead.
catch (do hide replFC (NS primIONS (UN "::"))
hide replFC (NS primIONS (UN "Nil")))
(\err => pure ())
(tm , gty) <- elabTerm inidx emode [] (MkNested [])
[] ttimpWithIt Nothing
ty <- getTerm gty
pure (tm `WithType` ty)
||| Produce the normal form of a PTerm, along with its inferred type
inferAndNormalize : {auto c : Ref Ctxt Defs} ->
{auto u : Ref UST UState} ->
{auto s : Ref Syn SyntaxInfo} ->
{auto m : Ref MD Metadata} ->
{auto o : Ref ROpts REPLOpts} ->
REPLEval ->
PTerm ->
Core TermWithType
inferAndNormalize emode itm
= do (tm `WithType` ty) <- inferAndElab (elabMode emode) itm
logTerm "repl.eval" 10 "Elaborated input" tm
defs <- get Ctxt
let norm = replEval emode
ntm <- norm defs [] tm
logTermNF "repl.eval" 5 "Normalised" [] ntm
pure $ ntm `WithType` ty
where
elabMode : REPLEval -> ElabMode
elabMode EvalTC = InType
elabMode _ = InExpr
equivTypes : {auto c : Ref Ctxt Defs} ->
(ty1 : ClosedTerm) ->
(ty2 : ClosedTerm) ->
Core Bool
equivTypes ty1 ty2 =
do let False = isErased ty1
| _ => pure False
logTerm "typesearch.equiv" 10 "Candidate: " ty1
defs <- get Ctxt
True <- pure (!(getArity defs [] ty1) == !(getArity defs [] ty2))
| False => pure False
_ <- newRef UST initUState
b <- catch
(do res <- unify inTerm replFC [] ty1 ty2
case res of
(MkUnifyResult [] _ [] NoLazy) => pure True
_ => pure False)
(\err => pure False)
when b $ logTerm "typesearch.equiv" 20 "Accepted: " ty1
pure b
||| Process a single `REPLCmd`
|||
@ -720,29 +726,16 @@ process : {auto c : Ref Ctxt Defs} ->
process (NewDefn decls) = execDecls decls
process (Eval itm)
= do opts <- get ROpts
case evalMode opts of
let emode = evalMode opts
case emode of
Execute => do ignore (execExp itm); pure (Executed itm)
_ =>
do ttimp <- desugar AnyExpr [] itm
let ttimpWithIt = ILocal replFC !getItDecls ttimp
inidx <- resolveName (UN "[input]")
-- a TMP HACK to prioritise list syntax for List: hide
-- foreign argument lists. TODO: once the new FFI is fully
-- up and running we won't need this. Also, if we add
-- 'with' disambiguation we can use that instead.
catch (do hide replFC (NS primIONS (UN "::"))
hide replFC (NS primIONS (UN "Nil")))
(\err => pure ())
(tm, gty) <- elabTerm inidx (emode (evalMode opts)) [] (MkNested [])
[] ttimpWithIt Nothing
logTerm "repl.eval" 10 "Elaborated input" tm
do
(ntm `WithType` ty) <- inferAndNormalize emode itm
itm <- resugar [] ntm
defs <- get Ctxt
opts <- get ROpts
let norm = nfun (evalMode opts)
ntm <- norm defs [] tm
logTermNF "repl.eval" 5 "Normalised" [] ntm
itm <- resugar [] ntm
ty <- getTerm gty
let norm = replEval emode
evalResultName <- DN "it" <$> genName "evalResult"
ignore $ addDef evalResultName
$ newDef replFC evalResultName top [] ty Private
@ -753,15 +746,6 @@ process (Eval itm)
then do ity <- resugar [] !(norm defs [] ty)
pure (Evaluated itm (Just ity))
else pure (Evaluated itm Nothing)
where
emode : REPLEval -> ElabMode
emode EvalTC = InType
emode _ = InExpr
nfun : {vs : _} ->
REPLEval -> Defs -> Env Term vs -> Term vs -> Core (Term vs)
nfun NormaliseAll = normaliseAll
nfun _ = normalise
process (Check (PRef fc (UN "it")))
= do opts <- get ROpts
case evalResultName opts of
@ -774,16 +758,18 @@ process (Check (PRef fc fn))
ts => do tys <- traverse (displayType defs) ts
pure (Printed $ vsep tys)
process (Check itm)
= do inidx <- resolveName (UN "[input]")
ttimp <- desugar AnyExpr [] itm
let ttimpWithIt = ILocal replFC !getItDecls ttimp
(tm, gty) <- elabTerm inidx InExpr [] (MkNested [])
[] ttimpWithIt Nothing
= do (tm `WithType` ty) <- inferAndElab InExpr itm
defs <- get Ctxt
itm <- resugar [] !(normaliseHoles defs [] tm)
ty <- getTerm gty
-- ty <- getTerm gty
ity <- resugar [] !(normaliseScope defs [] ty)
pure (TermChecked itm ity)
process (CheckWithImplicits itm)
= do showImplicits <- showImplicits <$> getPPrint
setOpt (ShowImplicits True)
result <- process (Check itm)
setOpt (ShowImplicits showImplicits)
pure result
process (PrintDef fn)
= do defs <- get Ctxt
case !(lookupCtxtName fn (gamma defs)) of
@ -839,11 +825,12 @@ process (TypeSearch searchTerm)
let defs = flip mapMaybe defs $ \ md =>
do d <- md
guard (visibleIn curr (fullname d) (visibility d))
guard (isJust $ userNameRoot (fullname d))
pure d
allDefs <- traverse (resolved ctxt) defs
filterM (\def => equivTypes def.type ty') allDefs
put Ctxt defs
doc <- traverse (docsOrSignature replFC) $ (.fullname) <$> filteredDefs
doc <- traverse (docsOrSignature replFC) $ fullname <$> filteredDefs
pure $ Printed $ vsep $ pretty <$> (intersperse "\n" $ join doc)
process (Missing n)
= do defs <- get Ctxt
@ -932,6 +919,34 @@ process NOP
= pure Done
process ShowVersion
= pure $ VersionIs version
process (ImportPackage package) = do
defs <- get Ctxt
let searchDirs = defs.options.dirs.extra_dirs
let Just packageDir = find
(\d => isInfixOf package (fromMaybe d (fileName d)))
searchDirs
| _ => pure (REPLError (pretty "Package not found in the known search directories"))
let packageDirPath = parse packageDir
tree <- coreLift $ explore packageDirPath
fentries <- coreLift $ toPaths (toRelative tree)
errs <- for fentries \entry => do
let entry' = dropExtension entry
let sp = forget $ split (== dirSeparator) entry'
let ns = concat $ intersperse "." sp
let ns' = mkNamespace ns
catch (do addImport (MkImport emptyFC False (nsAsModuleIdent ns') ns'); pure Nothing)
(\err => pure (Just err))
let errs' = catMaybes errs
res <- case errs' of
[] => pure (pretty "Done")
onePlus => pure $ vsep !(traverse display onePlus)
pure (Printed res)
where
toPaths : {root : _} -> Tree root -> IO (List String)
toPaths tree =
depthFirst (\x => map (toFilePath x ::) . force) tree (pure [])
process (FuzzyTypeSearch expr) = fuzzySearch expr
processCatch : {auto c : Ref Ctxt Defs} ->
{auto u : Ref UST UState} ->
@ -1107,7 +1122,7 @@ mutual
m ++ (makeSpace $ c2 `minus` length m) ++ r
cmdInfo : (List String, CmdArg, String) -> String
cmdInfo (cmds, args, text) = " " ++ col 16 12 (showSep " " cmds) (show args) text
cmdInfo (cmds, args, text) = " " ++ col 18 20 (showSep " " cmds) (show args) text
export
displayErrors : {auto c : Ref Ctxt Defs} ->

View File

@ -1,20 +1,29 @@
module Idris.REPLCommon
module Idris.REPL.Common
import Core.Context
import Core.Env
import Core.Context.Log
import Core.InitPrimitives
import Core.Metadata
import Core.Options
import Core.Primitives
import Core.TT
import Core.Unify
import Core.UnifyState
import Idris.DocString
import Idris.Error
import Idris.IDEMode.Commands
import public Idris.REPLOpts
import Idris.Syntax
import Idris.IDEMode.Holes
import Idris.Pretty
import public Idris.REPL.Opts
import Idris.Resugar
import Idris.Syntax
import Idris.Version
import Libraries.Data.ANameMap
import Libraries.Text.PrettyPrint.Prettyprinter
import Data.List
import Libraries.Text.PrettyPrint.Prettyprinter
import Libraries.Text.PrettyPrint.Prettyprinter.Render.Terminal
import System.File
%default covering
@ -135,3 +144,92 @@ resetContext
put UST initUState
put Syn initSyntax
put MD initMetadata
public export
data EditResult : Type where
DisplayEdit : Doc IdrisAnn -> EditResult
EditError : Doc IdrisAnn -> EditResult
MadeLemma : Maybe String -> Name -> PTerm -> String -> EditResult
MadeWith : Maybe String -> List String -> EditResult
MadeCase : Maybe String -> List String -> EditResult
public export
data MissedResult : Type where
CasesMissing : Name -> List String -> MissedResult
CallsNonCovering : Name -> List Name -> MissedResult
AllCasesCovered : Name -> MissedResult
public export
data REPLResult : Type where
Done : REPLResult
REPLError : Doc IdrisAnn -> REPLResult
Executed : PTerm -> REPLResult
RequestedHelp : REPLResult
Evaluated : PTerm -> (Maybe PTerm) -> REPLResult
Printed : Doc IdrisAnn -> REPLResult
TermChecked : PTerm -> PTerm -> REPLResult
FileLoaded : String -> REPLResult
ModuleLoaded : String -> REPLResult
ErrorLoadingModule : String -> Error -> REPLResult
ErrorLoadingFile : String -> FileError -> REPLResult
ErrorsBuildingFile : String -> List Error -> REPLResult
NoFileLoaded : REPLResult
CurrentDirectory : String -> REPLResult
CompilationFailed: REPLResult
Compiled : String -> REPLResult
ProofFound : PTerm -> REPLResult
Missed : List MissedResult -> REPLResult
CheckedTotal : List (Name, Totality) -> REPLResult
FoundHoles : List HoleData -> REPLResult
OptionsSet : List REPLOpt -> REPLResult
LogLevelSet : Maybe LogLevel -> REPLResult
ConsoleWidthSet : Maybe Nat -> REPLResult
ColorSet : Bool -> REPLResult
VersionIs : Version -> REPLResult
DefDeclared : REPLResult
Exited : REPLResult
Edited : EditResult -> REPLResult
export
docsOrSignature : {auto o : Ref ROpts REPLOpts} ->
{auto c : Ref Ctxt Defs} ->
{auto s : Ref Syn SyntaxInfo} ->
FC -> Name -> Core (List String)
docsOrSignature fc n
= do syn <- get Syn
defs <- get Ctxt
all@(_ :: _) <- lookupCtxtName n (gamma defs)
| _ => undefinedName fc n
let ns@(_ :: _) = concatMap (\n => lookupName n (docstrings syn))
(map fst all)
| [] => typeSummary defs
pure [!(render styleAnn !(getDocsForName fc n))]
where
typeSummary : Defs -> Core (List String)
typeSummary defs = do Just def <- lookupCtxtExact n (gamma defs)
| Nothing => pure []
ty <- normaliseHoles defs [] (type def)
pure [(show n) ++ " : " ++ (show !(resugar [] ty))]
export
equivTypes : {auto c : Ref Ctxt Defs} ->
(ty1 : ClosedTerm) ->
(ty2 : ClosedTerm) ->
Core Bool
equivTypes ty1 ty2 =
do let False = isErased ty1
| _ => pure False
logTerm "typesearch.equiv" 10 "Candidate: " ty1
defs <- get Ctxt
True <- pure (!(getArity defs [] ty1) == !(getArity defs [] ty2))
| False => pure False
_ <- newRef UST initUState
b <- catch
(do res <- unify inTerm replFC [] ty1 ty2
case res of
(MkUnifyResult [] _ [] NoLazy) => pure True
_ => pure False)
(\err => pure False)
when b $ logTerm "typesearch.equiv" 20 "Accepted: " ty1
pure b

View File

@ -0,0 +1,215 @@
module Idris.REPL.FuzzySearch
import Core.AutoSearch
import Core.CaseTree
import Core.CompileExpr
import Core.Context
import Core.Context.Log
import Core.Env
import Core.InitPrimitives
import Core.LinearCheck
import Core.Metadata
import Core.Normalise
import Core.Options
import Core.Termination
import Core.TT
import Core.Unify
import Idris.Desugar
import Idris.DocString
import Idris.Error
import Idris.IDEMode.CaseSplit
import Idris.IDEMode.Commands
import Idris.IDEMode.MakeClause
import Idris.IDEMode.Holes
import Idris.ModTree
import Idris.Parser
import Idris.Pretty
import Idris.ProcessIdr
import Idris.Resugar
import Idris.Syntax
import Idris.Version
import public Idris.REPL.Common
import Data.List
import Data.List1
import Data.Maybe
import Libraries.Data.ANameMap
import Libraries.Data.NameMap
import Libraries.Data.PosMap
import Data.Stream
import Data.Strings
import Data.DPair
import Libraries.Data.String.Extra
import Libraries.Data.List.Extra
import Libraries.Text.PrettyPrint.Prettyprinter
import Libraries.Text.PrettyPrint.Prettyprinter.Util
import Libraries.Text.PrettyPrint.Prettyprinter.Render.Terminal
import Libraries.Utils.Path
import Libraries.System.Directory.Tree
import System
import System.File
import System.Directory
export
fuzzySearch : {auto c : Ref Ctxt Defs}
-> {auto u : Ref UST UState}
-> {auto s : Ref Syn SyntaxInfo}
-> {auto m : Ref MD Metadata}
-> {auto o : Ref ROpts REPLOpts}
-> PTerm
-> Core REPLResult
fuzzySearch expr = do
let Just (neg, pos) = parseExpr expr
| _ => pure (REPLError (pretty "Bad expression, expected"
<++> code (pretty "B")
<++> pretty "or"
<++> code (pretty "_ -> B")
<++> pretty "or"
<++> code (pretty "A -> B")
<+> pretty ", where"
<++> code (pretty "A")
<++> pretty "and"
<++> code (pretty "B")
<++> pretty "are spines of global names"))
defs <- branch
let curr = currentNS defs
let ctxt = gamma defs
filteredDefs <-
do names <- allNames ctxt
defs <- traverse (flip lookupCtxtExact ctxt) names
let defs = flip mapMaybe defs $ \ md =>
do d <- md
guard (visibleIn curr (fullname d) (visibility d))
guard (isJust $ userNameRoot (fullname d))
pure d
allDefs <- traverse (resolved ctxt) defs
filterM (\def => fuzzyMatch neg pos def.type) allDefs
put Ctxt defs
doc <- traverse (docsOrSignature replFC) $ fullname <$> filteredDefs
pure $ Printed $ vsep $ pretty <$> (intersperse "\n" $ join doc)
where
data NameOrConst = AName Name
| AInt
| AInteger
| ABits8
| ABits16
| ABits32
| ABits64
| AString
| AChar
| ADouble
| AWorld
| AType
eqConst : (x, y : NameOrConst) -> Bool
eqConst AInt AInt = True
eqConst AInteger AInteger = True
eqConst ABits8 ABits8 = True
eqConst ABits16 ABits16 = True
eqConst ABits32 ABits32 = True
eqConst ABits64 ABits64 = True
eqConst AString AString = True
eqConst AChar AChar = True
eqConst ADouble ADouble = True
eqConst AWorld AWorld = True
eqConst AType AType = True
eqConst _ _ = False
parseNameOrConst : PTerm -> Maybe NameOrConst
parseNameOrConst (PRef _ n) = Just (AName n)
parseNameOrConst (PPrimVal _ IntType) = Just AInt
parseNameOrConst (PPrimVal _ IntegerType) = Just AInteger
parseNameOrConst (PPrimVal _ Bits8Type) = Just ABits8
parseNameOrConst (PPrimVal _ Bits16Type) = Just ABits16
parseNameOrConst (PPrimVal _ Bits32Type) = Just ABits32
parseNameOrConst (PPrimVal _ Bits64Type) = Just ABits64
parseNameOrConst (PPrimVal _ StringType) = Just AString
parseNameOrConst (PPrimVal _ CharType) = Just AChar
parseNameOrConst (PPrimVal _ DoubleType) = Just ADouble
parseNameOrConst (PPrimVal _ WorldType) = Just AWorld
parseNameOrConst (PType _) = Just AType
parseNameOrConst _ = Nothing
parseExpr' : PTerm -> Maybe (List NameOrConst)
parseExpr' (PApp _ f x) =
[| parseNameOrConst x :: parseExpr' f |]
parseExpr' x = (:: []) <$> parseNameOrConst x
parseExpr : PTerm -> Maybe (List NameOrConst, List NameOrConst)
parseExpr (PPi _ _ _ _ a (PImplicit _)) = do
a' <- parseExpr' a
pure (a', [])
parseExpr (PPi _ _ _ _ a b) = do
a' <- parseExpr' a
b' <- parseExpr' b
pure (a', b')
parseExpr b = do
b' <- parseExpr' b
pure ([], b')
isApproximationOf : (given : Name)
-> (candidate : Name)
-> Bool
isApproximationOf (NS ns n) (NS ns' n') =
n == n' && Namespace.isApproximationOf ns ns'
isApproximationOf (UN n) (NS ns' (UN n')) =
n == n'
isApproximationOf (NS ns n) _ =
False
isApproximationOf (UN n) (UN n') =
n == n'
isApproximationOf _ _ =
False
isApproximationOf' : (given : NameOrConst)
-> (candidate : NameOrConst)
-> Bool
isApproximationOf' (AName x) (AName y) =
isApproximationOf x y
isApproximationOf' a b = eqConst a b
||| Find all name and type literal occurrences.
export
doFind : List NameOrConst -> Term vars -> List NameOrConst
doFind ns (Local fc x idx y) = ns
doFind ns (Ref fc x name) = AName name :: ns
doFind ns (Meta fc n i xs)
= foldl doFind ns xs
doFind ns (Bind fc x (Let _ c val ty) scope)
= doFind (doFind (doFind ns val) ty) scope
doFind ns (Bind fc x b scope)
= doFind (doFind ns (binderType b)) scope
doFind ns (App fc fn arg)
= doFind (doFind ns fn) arg
doFind ns (As fc s as tm) = doFind ns tm
doFind ns (TDelayed fc x y) = doFind ns y
doFind ns (TDelay fc x t y)
= doFind (doFind ns t) y
doFind ns (TForce fc r x) = doFind ns x
doFind ns (PrimVal fc c) =
fromMaybe [] ((:: []) <$> parseNameOrConst (PPrimVal fc c)) ++ ns
doFind ns (Erased fc i) = ns
doFind ns (TType fc) = AType :: ns
toFullNames' : NameOrConst -> Core NameOrConst
toFullNames' (AName x) = AName <$> toFullNames x
toFullNames' x = pure x
fuzzyMatch : (neg : List NameOrConst)
-> (pos : List NameOrConst)
-> Term vars
-> Core Bool
fuzzyMatch neg pos (Bind _ _ b sc) = do
let refsB = doFind [] (binderType b)
refsB <- traverse toFullNames' refsB
let neg' = diffBy isApproximationOf' neg refsB
fuzzyMatch neg' pos sc
fuzzyMatch (_ :: _) pos tm = pure False
fuzzyMatch [] pos tm = do
let refsB = doFind [] tm
refsB <- traverse toFullNames' refsB
pure (isNil $ diffBy isApproximationOf' pos refsB)

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