idris-lang/Idris2
1
1
Fork 0
mirror of https://github.com/idris-lang/Idris2.git synced 2024-09-21 10:18:23 +03:00
Code Issues Projects Releases Wiki Activity

Merge branch 'master' of github.com:idris-lang/Idris2 into javascript

Browse Source
This commit is contained in:
Rui Barreiro 2020-06-17 23:48:39 +01:00
commit f8f09858e8
139 changed files with 2241 additions and 782 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
.gitignore vendored
View File

@ -34,3 +34,5 @@ idris2docs_venv
/bootstrap/idris2_app/libidris2_support.*
/bootstrap/idris2boot
/bootstrap/idris2boot.rkt
/custom.mk

6
INSTALL.md
View File

@ -7,6 +7,9 @@ The requirements are:
* A Scheme compiler; either Chez Scheme (default), or Racket.
* `bash`, with `realpath`. On Linux, you probably already have this.
On a Mac, you can install this with `brew install coreutils`.
On FreeBSD, OpenBSD and NetBSD, you can install `realpath` and `GNU make`
using a package manager. For instance, on OpenBSD you can install all of them
with `pkg_add coreutuls gmake` command.
On Windows, it has been reported that installing via `MSYS2` works
(https://www.msys2.org/). On Windows older than Windows 8, you may need to
@ -19,6 +22,9 @@ by setting the environment variable `IDRIS2_CG=racket` before running `make`.
If you install Chez Scheme from source files, building it locally,
make sure you run `./configure --threads` to build multithreading support in.
**NOTE**: On FreeBSD, OpenBSD and NetBSD you need to use `gmake` command instead
of `make` in the following steps.
1: Set the PREFIX
-----------------

3
Makefile
View File

@ -144,8 +144,6 @@ ifeq ($(OS), darwin)
else
sed -i 's|__PREFIX__|${IDRIS2_CURDIR}/bootstrap|g' bootstrap/idris2_app/idris2-boot.ss
endif
SCHEME=${SCHEME} \
IDRIS2_VERSION=${IDRIS2_VERSION} \
sh ./bootstrap.sh
# Bootstrapping using racket
@ -159,7 +157,6 @@ ifeq ($(OS), darwin)
else
sed -i 's|__PREFIX__|${IDRIS2_CURDIR}/bootstrap|g' bootstrap/idris2_app/idris2-boot.rkt
endif
IDRIS2_VERSION=${IDRIS2_VERSION} \
sh ./bootstrap-rkt.sh
bootstrap-test:

1
README.md
View File

@ -34,6 +34,7 @@ exceptions. The most notable user visible differences, which might cause Idris
(such as data constructors), or which have different concrete argument
types (such as record projections). It may struggle to resolve ambiguities
if one name requires an interface to be resolved.
+ The `cong` function now takes its congruence explicitly as its first argument.
+ Minor differences in the meaning of export modifiers `private`, `export`,
and `public export`, which now refer to visibility of names from other
*namespaces* rather than visibility from other *files*.

9
bootstrap-rkt.sh
View File

@ -40,9 +40,8 @@ IDRIS2_BOOT_PATH="${BOOT_PATH_BASE}/prelude${SEP}${BOOT_PATH_BASE}/base${SEP}${B
# PREFIX must be the "clean" build root, without cygpath -m
# Otherwise, we get 'git: Bad address'
echo ${PREFIX}
DYLIB_PATH="${PREFIX}/lib"
make libs IDRIS2_CG=racket PREFIX=${PREFIX} LD_LIBRARY_PATH=${DYLIB_PATH}
make install IDRIS2_CG=racket PREFIX=${PREFIX} LD_LIBRARY_PATH=${DYLIB_PATH}
make clean IDRIS2_BOOT=${PREFIX}/bin/idris2 LD_LIBRARY_PATH=${DYLIB_PATH}
make all IDRIS2_BOOT=${PREFIX}/bin/idris2 IDRIS2_CG=racket IDRIS2_PATH=${IDRIS2_BOOT_PATH} LD_LIBRARY_PATH=${DYLIB_PATH}
${MAKE} libs IDRIS2_CG=racket PREFIX=${PREFIX} LD_LIBRARY_PATH=${DYLIB_PATH}
${MAKE} install IDRIS2_CG=racket PREFIX=${PREFIX} LD_LIBRARY_PATH=${DYLIB_PATH}
${MAKE} clean IDRIS2_BOOT=${PREFIX}/bin/idris2 LD_LIBRARY_PATH=${DYLIB_PATH}
${MAKE} all IDRIS2_BOOT=${PREFIX}/bin/idris2 IDRIS2_CG=racket IDRIS2_PATH=${IDRIS2_BOOT_PATH} LD_LIBRARY_PATH=${DYLIB_PATH}

9
bootstrap.sh
View File

@ -46,8 +46,7 @@ IDRIS2_BOOT_PATH="${BOOT_PATH_BASE}/prelude${SEP}${BOOT_PATH_BASE}/base${SEP}${B
# PREFIX must be the "clean" build root, without cygpath -m
# Otherwise, we get 'git: Bad address'
echo ${PREFIX}
make libs SCHEME=${SCHEME} PREFIX=${PREFIX}
make install SCHEME=${SCHEME} PREFIX=${PREFIX}
make clean IDRIS2_BOOT=${PREFIX}/bin/idris2
make all IDRIS2_BOOT=${PREFIX}/bin/idris2 SCHEME=${SCHEME} IDRIS2_PATH=${IDRIS2_BOOT_PATH}
${MAKE} libs SCHEME=${SCHEME} PREFIX=${PREFIX}
${MAKE} install SCHEME=${SCHEME} PREFIX=${PREFIX}
${MAKE} clean IDRIS2_BOOT=${PREFIX}/bin/idris2
${MAKE} all IDRIS2_BOOT=${PREFIX}/bin/idris2 SCHEME=${SCHEME} IDRIS2_PATH=${IDRIS2_BOOT_PATH}

12
bootstrap/idris2-boot vendored
View File

@ -1,5 +1,15 @@
#!/bin/sh
DIR="`realpath $0`"
case `uname -s` in
OpenBSD|FreeBSD|NetBSD)
DIR="`grealpath $0`"
;;
*)
DIR="`realpath $0`"
;;
esac
export LD_LIBRARY_PATH="$LD_LIBRARY_PATH:`dirname "$DIR"`/"idris2_app""
export PATH="`dirname "$DIR"`/"idris2_app":$PATH"
${SCHEME} --script "`dirname $DIR`"/"idris2_app/idris2-boot.so" "$@"

12
bootstrap/idris2-rktboot vendored
View File

@ -1,5 +1,15 @@
#!/bin/sh
DIR="`realpath $0`"
case `uname -s` in
OpenBSD|FreeBSD|NetBSD)
DIR="`grealpath $0`"
;;
*)
DIR="`realpath $0`"
;;
esac
export LD_LIBRARY_PATH="$LD_LIBRARY_PATH:`dirname "$DIR"`/"idris2_app""
export PATH="`dirname "$DIR"`/"idris2_app":$PATH"
"`dirname $DIR`"/"idris2_app/idris2-boot" "$@"

8
bootstrap/idris2_app/idris2.rkt
View File

@ -7325,9 +7325,9 @@
(define Racket-Scheme-Compiler-n--8783-872-callback (lambda (arg-0 arg-1 arg-2 arg-3 arg-4 arg-5 arg-6 arg-7 arg-8 arg-9 arg-10 arg-11) (let ((sc0 arg-11)) (case (vector-ref sc0 0) ((10) (let ((e-0 (vector-ref sc0 1))) (let ((e-1 (vector-ref sc0 2))) (Racket-Scheme-Compiler-n--8783-872-callback arg-0 arg-1 arg-2 arg-3 arg-4 arg-5 arg-6 arg-7 arg-8 arg-9 (vector 1 e-0 arg-10) e-1))))(else (let ((args (List-Data-reverse 'erased arg-10))) (lambda (eta-0) (let ((act-24 ((Core-Core-traverse 'erased 'erased (lambda (eta-1) (Racket-Scheme-Compiler-cftySpec arg-4 eta-1)) (List-Data-filter 'erased (lambda (eta-1) (Racket-Scheme-Compiler-n--8783-871-notWorld arg-0 arg-1 arg-2 arg-3 arg-4 arg-5 arg-6 arg-7 arg-8 eta-1)) args)) eta-0))) (let ((sc0 act-24)) (case (vector-ref sc0 0) ((0) (let ((e-2 (vector-ref sc0 1))) (vector 0 e-2))) (else (let ((act-25 ((Racket-Scheme-Compiler-cftySpec arg-4 arg-11) eta-0))) (let ((sc1 act-25)) (case (vector-ref sc1 0) ((0) (let ((e-2 (vector-ref sc1 1))) (vector 0 e-2))) (else (vector 1 (Racket-Scheme-Compiler-n--8783-870-mkFun arg-0 arg-1 arg-2 arg-3 arg-4 arg-5 arg-6 arg-7 arg-8 args arg-11 arg-9)))))))))))))))))
(define Racket-Scheme-Compiler-n--8783-869-applyLams (lambda (arg-0 arg-1 arg-2 arg-3 arg-4 arg-5 arg-6 arg-7 arg-8 arg-9 arg-10) (let ((sc0 arg-10)) (case (vector-ref sc0 0) ((0) arg-9) (else (let ((e-2 (vector-ref sc0 1))) (let ((e-3 (vector-ref sc0 2))) (let ((sc1 e-2)) (case (vector-ref sc1 0) ((0) (Racket-Scheme-Compiler-n--8783-869-applyLams arg-0 arg-1 arg-2 arg-3 arg-4 arg-5 arg-6 arg-7 arg-8 (Strings-Prelude-C-43C-43 "(" (Strings-Prelude-C-43C-43 arg-9 " #f)")) e-3)) (else (let ((e-6 (vector-ref sc1 1))) (let ((sc2 e-6)) (let ((e-9 (vector-ref sc2 1))) (let ((e-10 (vector-ref sc2 2))) (Racket-Scheme-Compiler-n--8783-869-applyLams arg-0 arg-1 arg-2 arg-3 arg-4 arg-5 arg-6 arg-7 arg-8 (Strings-Prelude-C-43C-43 "(" (Strings-Prelude-C-43C-43 arg-9 (Strings-Prelude-C-43C-43 " " (Strings-Prelude-C-43C-43 (Racket-Scheme-Compiler-cToRkt e-10 e-9) ")")))) e-3)))))))))))))))
(define Racket-Scheme-Compiler-useCC (lambda (arg-0 arg-1 arg-2 arg-3 arg-4 arg-5 arg-6 arg-7) (let ((sc0 arg-5)) (case (vector-ref sc0 0) ((0) (lambda (eta-0) (Core-Core-throw_Catchable__Core_Error 'erased (vector 47 arg-4 "No recognised foreign calling convention") eta-0))) (else (let ((e-2 (vector-ref sc0 1))) (let ((e-3 (vector-ref sc0 2))) (Racket-Scheme-Compiler-case--9479-1473 e-2 e-3 arg-7 arg-6 arg-4 arg-3 arg-2 arg-1 arg-0 (Common-Compiler-parseCC e-2)))))))))
(define Racket-Scheme-Compiler-startRacketWinSh (lambda (arg-0 arg-1 arg-2) (Strings-Data-unlines (vector 1 "#!/bin/sh" (vector 1 "DIR=\"`realpath \"$0\"`\"" (vector 1 (Strings-Prelude-C-43C-43 "export PATH=\"`dirname \"$DIR\"`/\"" (Strings-Prelude-C-43C-43 arg-1 "\":$PATH\"")) (vector 1 (Strings-Prelude-C-43C-43 arg-0 (Strings-Prelude-C-43C-43 "\"" (Strings-Prelude-C-43C-43 arg-2 "\" \"$@\""))) (vector 0 ))))))))
(define Racket-Scheme-Compiler-startRacketWinSh (lambda (arg-0 arg-1 arg-2) (Strings-Data-unlines (vector 1 "#!/bin/sh" (vector 1 "" (vector 1 "case `uname -s` in " (vector 1 " OpenBSD|FreeBSD|NetBSD) " (vector 1 " DIR=\"`grealpath $0`\"" (vector 1 " ;; " (vector 1 " " (vector 1 " *) " (vector 1 " DIR=\"`realpath $0`\" " (vector 1 " ;; " (vector 1 "esac " (vector 1 "" (vector 1 (Strings-Prelude-C-43C-43 "export PATH=\"`dirname \"$DIR\"`/\"" (Strings-Prelude-C-43C-43 arg-1 "\":$PATH\"")) (vector 1 (Strings-Prelude-C-43C-43 arg-0 (Strings-Prelude-C-43C-43 "\"" (Strings-Prelude-C-43C-43 arg-2 "\" \"$@\""))) (vector 0 ))))))))))))))))))
(define Racket-Scheme-Compiler-startRacketCmd (lambda (arg-0 arg-1 arg-2) (Strings-Data-unlines (vector 1 "@echo off" (vector 1 "set APPDIR=%~dp0" (vector 1 (Strings-Prelude-C-43C-43 "set PATH=%APPDIR%\\" (Strings-Prelude-C-43C-43 arg-1 ";%PATH%")) (vector 1 (Strings-Prelude-C-43C-43 arg-0 (Strings-Prelude-C-43C-43 "\"" (Strings-Prelude-C-43C-43 arg-2 "\" %*"))) (vector 0 ))))))))
(define Racket-Scheme-Compiler-startRacket (lambda (arg-0 arg-1 arg-2) (Strings-Data-unlines (vector 1 "#!/bin/sh" (vector 1 "" (vector 1 "DIR=\"`realpath $0`\"" (vector 1 (Strings-Prelude-C-43C-43 "export LD_LIBRARY_PATH=\"$LD_LIBRARY_PATH:`dirname \"$DIR\"`/\"" (Strings-Prelude-C-43C-43 arg-1 "\"\"")) (vector 1 (Strings-Prelude-C-43C-43 arg-0 (Strings-Prelude-C-43C-43 "\"`dirname \"$DIR\"`\"/\"" (Strings-Prelude-C-43C-43 arg-2 "\" \"$@\""))) (vector 0 )))))))))
(define Racket-Scheme-Compiler-startRacket (lambda (arg-0 arg-1 arg-2) (Strings-Data-unlines (vector 1 "#!/bin/sh" (vector 1 "" (vector 1 "case `uname -s` in " (vector 1 " OpenBSD|FreeBSD|NetBSD) " (vector 1 " DIR=\"`grealpath $0`\"" (vector 1 " ;; " (vector 1 " " (vector 1 " *) " (vector 1 " DIR=\"`realpath $0`\" " (vector 1 " ;; " (vector 1 "esac " (vector 1 "" (vector 1 (Strings-Prelude-C-43C-43 "export LD_LIBRARY_PATH=\"$LD_LIBRARY_PATH:`dirname \"$DIR\"`/\"" (Strings-Prelude-C-43C-43 arg-1 "\"\"")) (vector 1 (Strings-Prelude-C-43C-43 arg-0 (Strings-Prelude-C-43C-43 "\"`dirname \"$DIR\"`\"/\"" (Strings-Prelude-C-43C-43 arg-2 "\" \"$@\""))) (vector 0 ))))))))))))))))))
(define Racket-Scheme-Compiler-showRacketString (lambda (arg-0) (let ((sc0 arg-0)) (case (vector-ref sc0 0) ((0) (lambda (eta-0) eta-0)) (else (let ((e-2 (vector-ref sc0 1))) (let ((e-3 (vector-ref sc0 2))) (let ((sc1 e-2)) (cond ((equal? sc1 #\") (lambda (eta-0) (Strings-Prelude-C-43C-43 "\\\"" ((Racket-Scheme-Compiler-showRacketString e-3) eta-0))))(else (lambda (eta-0) ((Racket-Scheme-Compiler-showRacketChar e-2) ((Racket-Scheme-Compiler-showRacketString e-3) eta-0)))))))))))))
(define Racket-Scheme-Compiler-showRacketChar (lambda (arg-0) (let ((sc0 arg-0)) (cond ((equal? sc0 #\\) (lambda (arg-1) (Strings-Prelude-C-43C-43 "\\\\" arg-1)))(else (Racket-Scheme-Compiler-case--8220-334 arg-0 (Prelude-C-124C-124 (Prelude-C-60_Ord__Char arg-0 (Prelude-chr 32)) (lambda () (Prelude-C-62_Ord__Char arg-0 (Prelude-chr 126))))))))))
(define Racket-Scheme-Compiler-schemeCall (lambda (arg-0 arg-1 arg-2 arg-3) (let ((call (Strings-Prelude-C-43C-43 "(" (Strings-Prelude-C-43C-43 arg-1 (Strings-Prelude-C-43C-43 " " (Strings-Prelude-C-43C-43 (Name-Core-showSep " " (Prelude-map_Functor__List 'erased 'erased (lambda (eta-0) (Common-Scheme-Compiler-schName eta-0)) arg-2)) ")")))))) (let ((sc0 arg-3)) (case (vector-ref sc0 0) ((11) (lambda (eta-0) (vector 1 (Common-Scheme-Compiler-mkWorld call))))(else (lambda (eta-0) (vector 1 call))))))))
@ -7386,9 +7386,9 @@
(define Chez-Scheme-Compiler-n--8803-1177-applyLams (lambda (arg-0 arg-1 arg-2 arg-3 arg-4 arg-5 arg-6 arg-7 arg-8 arg-9) (let ((sc0 arg-9)) (case (vector-ref sc0 0) ((0) arg-8) (else (let ((e-2 (vector-ref sc0 1))) (let ((e-3 (vector-ref sc0 2))) (let ((sc1 e-2)) (case (vector-ref sc1 0) ((0) (Chez-Scheme-Compiler-n--8803-1177-applyLams arg-0 arg-1 arg-2 arg-3 arg-4 arg-5 arg-6 arg-7 (Strings-Prelude-C-43C-43 "(" (Strings-Prelude-C-43C-43 arg-8 " #f)")) e-3)) (else (let ((e-6 (vector-ref sc1 1))) (Chez-Scheme-Compiler-n--8803-1177-applyLams arg-0 arg-1 arg-2 arg-3 arg-4 arg-5 arg-6 arg-7 (Strings-Prelude-C-43C-43 "(" (Strings-Prelude-C-43C-43 arg-8 (Strings-Prelude-C-43C-43 " " (Strings-Prelude-C-43C-43 e-6 ")")))) e-3))))))))))))
(define Chez-Scheme-Compiler-useCC (lambda (arg-0 arg-1 arg-2 arg-3 arg-4 arg-5 arg-6) (let ((sc0 arg-4)) (case (vector-ref sc0 0) ((0) (lambda (eta-0) (Core-Core-throw_Catchable__Core_Error 'erased (vector 47 arg-3 "No recognised foreign calling convention") eta-0))) (else (let ((e-2 (vector-ref sc0 1))) (let ((e-3 (vector-ref sc0 2))) (Chez-Scheme-Compiler-case--9252-1575 e-2 e-3 arg-6 arg-5 arg-3 arg-2 arg-1 arg-0 (Common-Compiler-parseCC e-2)))))))))
(define Chez-Scheme-Compiler-tySpec (lambda (arg-0) (let ((sc0 arg-0)) (case (vector-ref sc0 0) ((5) (let ((e-0 (vector-ref sc0 1))) (let ((e-1 (vector-ref sc0 2))) (let ((e-3 (vector-ref sc0 4))) (let ((sc1 e-1)) (case (vector-ref sc1 0) ((1) (let ((e-4 (vector-ref sc1 1))) (let ((sc2 e-4)) (cond ((equal? sc2 "Int") (let ((sc3 e-3)) (case (vector-ref sc3 0) ((0) (lambda (eta-0) (vector 1 "int")))(else (lambda (eta-0) (Core-Core-throw_Catchable__Core_Error 'erased (vector 47 (NamedCExp-CompileExpr-Core-getFC arg-0) (Strings-Prelude-C-43C-43 "Can't pass argument of type " (Strings-Prelude-C-43C-43 (CompileExpr-Core-show_Show__NamedCExp arg-0) " to foreign function"))) eta-0)))))) ((equal? sc2 "String") (let ((sc3 e-3)) (case (vector-ref sc3 0) ((0) (lambda (eta-0) (vector 1 "string")))(else (lambda (eta-0) (Core-Core-throw_Catchable__Core_Error 'erased (vector 47 (NamedCExp-CompileExpr-Core-getFC arg-0) (Strings-Prelude-C-43C-43 "Can't pass argument of type " (Strings-Prelude-C-43C-43 (CompileExpr-Core-show_Show__NamedCExp arg-0) " to foreign function"))) eta-0)))))) ((equal? sc2 "Double") (let ((sc3 e-3)) (case (vector-ref sc3 0) ((0) (lambda (eta-0) (vector 1 "double")))(else (lambda (eta-0) (Core-Core-throw_Catchable__Core_Error 'erased (vector 47 (NamedCExp-CompileExpr-Core-getFC arg-0) (Strings-Prelude-C-43C-43 "Can't pass argument of type " (Strings-Prelude-C-43C-43 (CompileExpr-Core-show_Show__NamedCExp arg-0) " to foreign function"))) eta-0)))))) ((equal? sc2 "Char") (let ((sc3 e-3)) (case (vector-ref sc3 0) ((0) (lambda (eta-0) (vector 1 "char")))(else (lambda (eta-0) (Core-Core-throw_Catchable__Core_Error 'erased (vector 47 (NamedCExp-CompileExpr-Core-getFC arg-0) (Strings-Prelude-C-43C-43 "Can't pass argument of type " (Strings-Prelude-C-43C-43 (CompileExpr-Core-show_Show__NamedCExp arg-0) " to foreign function"))) eta-0))))))(else (lambda (eta-0) (Core-Core-throw_Catchable__Core_Error 'erased (vector 47 (NamedCExp-CompileExpr-Core-getFC arg-0) (Strings-Prelude-C-43C-43 "Can't pass argument of type " (Strings-Prelude-C-43C-43 (CompileExpr-Core-show_Show__NamedCExp arg-0) " to foreign function"))) eta-0))))))) ((0) (let ((e-6 (vector-ref sc1 2))) (let ((sc2 e-3)) (case (vector-ref sc2 0) ((1) (let ((e-13 (vector-ref sc2 2))) (let ((sc3 e-13)) (case (vector-ref sc3 0) ((0) (Core-Core-cond 'erased (vector 1 (vector 0 (lambda () (Name-Core-C-61C-61_Eq__Name e-6 (vector 1 "Ptr"))) (lambda () (lambda (eta-0) (vector 1 "void*")))) (vector 1 (vector 0 (lambda () (Name-Core-C-61C-61_Eq__Name e-6 (vector 1 "GCPtr"))) (lambda () (lambda (eta-0) (vector 1 "void*")))) (vector 1 (vector 0 (lambda () (Name-Core-C-61C-61_Eq__Name e-6 (vector 1 "Buffer"))) (lambda () (lambda (eta-0) (vector 1 "u8*")))) (vector 0 )))) (lambda (eta-0) (Core-Core-throw_Catchable__Core_Error 'erased (vector 47 e-0 (Strings-Prelude-C-43C-43 "Can't pass argument of type " (Strings-Prelude-C-43C-43 (Name-Core-show_Show__Name e-6) " to foreign function"))) eta-0))))(else (lambda (eta-0) (Core-Core-throw_Catchable__Core_Error 'erased (vector 47 (NamedCExp-CompileExpr-Core-getFC arg-0) (Strings-Prelude-C-43C-43 "Can't pass argument of type " (Strings-Prelude-C-43C-43 (CompileExpr-Core-show_Show__NamedCExp arg-0) " to foreign function"))) eta-0))))))) ((0) (Core-Core-cond 'erased (vector 1 (vector 0 (lambda () (Name-Core-C-61C-61_Eq__Name e-6 (vector 1 "Unit"))) (lambda () (lambda (eta-0) (vector 1 "void")))) (vector 1 (vector 0 (lambda () (Name-Core-C-61C-61_Eq__Name e-6 (vector 1 "AnyPtr"))) (lambda () (lambda (eta-0) (vector 1 "void*")))) (vector 1 (vector 0 (lambda () (Name-Core-C-61C-61_Eq__Name e-6 (vector 1 "GCAnyPtr"))) (lambda () (lambda (eta-0) (vector 1 "void*")))) (vector 0 )))) (lambda (eta-0) (Core-Core-throw_Catchable__Core_Error 'erased (vector 47 e-0 (Strings-Prelude-C-43C-43 "Can't pass argument of type " (Strings-Prelude-C-43C-43 (Name-Core-show_Show__Name e-6) " to foreign function"))) eta-0))))(else (lambda (eta-0) (Core-Core-throw_Catchable__Core_Error 'erased (vector 47 (NamedCExp-CompileExpr-Core-getFC arg-0) (Strings-Prelude-C-43C-43 "Can't pass argument of type " (Strings-Prelude-C-43C-43 (CompileExpr-Core-show_Show__NamedCExp arg-0) " to foreign function"))) eta-0)))))))(else (lambda (eta-0) (Core-Core-throw_Catchable__Core_Error 'erased (vector 47 (NamedCExp-CompileExpr-Core-getFC arg-0) (Strings-Prelude-C-43C-43 "Can't pass argument of type " (Strings-Prelude-C-43C-43 (CompileExpr-Core-show_Show__NamedCExp arg-0) " to foreign function"))) eta-0)))))))))(else (lambda (eta-0) (Core-Core-throw_Catchable__Core_Error 'erased (vector 47 (NamedCExp-CompileExpr-Core-getFC arg-0) (Strings-Prelude-C-43C-43 "Can't pass argument of type " (Strings-Prelude-C-43C-43 (CompileExpr-Core-show_Show__NamedCExp arg-0) " to foreign function"))) eta-0)))))))
(define Chez-Scheme-Compiler-startChezWinSh (lambda (arg-0 arg-1 arg-2) (Strings-Data-unlines (vector 1 "#!/bin/sh" (vector 1 "DIR=\"`realpath \"$0\"`\"" (vector 1 (Strings-Prelude-C-43C-43 "CHEZ=$(cygpath \"" (Strings-Prelude-C-43C-43 arg-0 "\")")) (vector 1 (Strings-Prelude-C-43C-43 "export PATH=\"`dirname \"$DIR\"`/\"" (Strings-Prelude-C-43C-43 arg-1 "\":$PATH\"")) (vector 1 (Strings-Prelude-C-43C-43 "$CHEZ --script \"$(dirname \"$DIR\")/" (Strings-Prelude-C-43C-43 arg-2 "\" \"$@\"")) (vector 0 )))))))))
(define Chez-Scheme-Compiler-startChezWinSh (lambda (arg-0 arg-1 arg-2) (Strings-Data-unlines (vector 1 "#!/bin/sh" (vector 1 "" (vector 1 "case `uname -s` in " (vector 1 " OpenBSD|FreeBSD|NetBSD) " (vector 1 " DIR=\"`grealpath $0`\"" (vector 1 " ;; " (vector 1 " " (vector 1 " *) " (vector 1 " DIR=\"`realpath $0`\" " (vector 1 " ;; " (vector 1 "esac " (vector 1 "" (vector 1 (Strings-Prelude-C-43C-43 "CHEZ=$(cygpath \"" (Strings-Prelude-C-43C-43 arg-0 "\")")) (vector 1 (Strings-Prelude-C-43C-43 "export PATH=\"`dirname \"$DIR\"`/\"" (Strings-Prelude-C-43C-43 arg-1 "\":$PATH\"")) (vector 1 (Strings-Prelude-C-43C-43 "$CHEZ --script \"$(dirname \"$DIR\")/" (Strings-Prelude-C-43C-43 arg-2 "\" \"$@\"")) (vector 0 )))))))))))))))))))
(define Chez-Scheme-Compiler-startChezCmd (lambda (arg-0 arg-1 arg-2) (Strings-Data-unlines (vector 1 "@echo off" (vector 1 "set APPDIR=%~dp0" (vector 1 (Strings-Prelude-C-43C-43 "set PATH=%APPDIR%\\" (Strings-Prelude-C-43C-43 arg-1 ";%PATH%")) (vector 1 (Strings-Prelude-C-43C-43 "\"" (Strings-Prelude-C-43C-43 arg-0 (Strings-Prelude-C-43C-43 "\" --script \"%APPDIR%/" (Strings-Prelude-C-43C-43 arg-2 "\" %*")))) (vector 0 ))))))))
(define Chez-Scheme-Compiler-startChez (lambda (arg-0 arg-1) (Strings-Data-unlines (vector 1 "#!/bin/sh" (vector 1 "" (vector 1 "DIR=\"`realpath $0`\"" (vector 1 (Strings-Prelude-C-43C-43 "export LD_LIBRARY_PATH=\"$LD_LIBRARY_PATH:`dirname \"$DIR\"`/\"" (Strings-Prelude-C-43C-43 arg-0 "\"\"")) (vector 1 (Strings-Prelude-C-43C-43 "\"`dirname \"$DIR\"`\"/\"" (Strings-Prelude-C-43C-43 arg-1 "\" \"$@\"")) (vector 0 )))))))))
(define Chez-Scheme-Compiler-startChez (lambda (arg-0 arg-1) (Strings-Data-unlines (vector 1 "#!/bin/sh" (vector 1 "" (vector 1 "case `uname -s` in " (vector 1 " OpenBSD|FreeBSD|NetBSD) " (vector 1 " DIR=\"`grealpath $0`\"" (vector 1 " ;; " (vector 1 " " (vector 1 " *) " (vector 1 " DIR=\"`realpath $0`\" " (vector 1 " ;; " (vector 1 "esac " (vector 1 "" (vector 1 (Strings-Prelude-C-43C-43 "export LD_LIBRARY_PATH=\"$LD_LIBRARY_PATH:`dirname \"$DIR\"`/\"" (Strings-Prelude-C-43C-43 arg-0 "\"\"")) (vector 1 (Strings-Prelude-C-43C-43 "\"`dirname \"$DIR\"`\"/\"" (Strings-Prelude-C-43C-43 arg-1 "\" \"$@\"")) (vector 0 ))))))))))))))))))
(define Chez-Scheme-Compiler-showChezString (lambda (arg-0) (let ((sc0 arg-0)) (case (vector-ref sc0 0) ((0) (lambda (eta-0) eta-0)) (else (let ((e-2 (vector-ref sc0 1))) (let ((e-3 (vector-ref sc0 2))) (let ((sc1 e-2)) (cond ((equal? sc1 #\") (lambda (eta-0) (Strings-Prelude-C-43C-43 "\\\"" ((Chez-Scheme-Compiler-showChezString e-3) eta-0))))(else (lambda (eta-0) ((Chez-Scheme-Compiler-showChezChar e-2) ((Chez-Scheme-Compiler-showChezString e-3) eta-0)))))))))))))
(define Chez-Scheme-Compiler-showChezChar (lambda (arg-0) (let ((sc0 arg-0)) (cond ((equal? sc0 #\\) (lambda (arg-1) (Strings-Prelude-C-43C-43 "\\\\" arg-1)))(else (Chez-Scheme-Compiler-case--8090-452 arg-0 (Prelude-C-124C-124 (Prelude-C-60_Ord__Char arg-0 (Prelude-chr 32)) (lambda () (Prelude-C-62_Ord__Char arg-0 (Prelude-chr 126))))))))))
(define Chez-Scheme-Compiler-schemeCall (lambda (arg-0 arg-1 arg-2 arg-3) (let ((call (Strings-Prelude-C-43C-43 "(" (Strings-Prelude-C-43C-43 arg-1 (Strings-Prelude-C-43C-43 " " (Strings-Prelude-C-43C-43 (Name-Core-showSep " " (Prelude-map_Functor__List 'erased 'erased (lambda (eta-0) (Common-Scheme-Compiler-schName eta-0)) arg-2)) ")")))))) (let ((sc0 arg-3)) (case (vector-ref sc0 0) ((11) (lambda (eta-0) (vector 1 (Common-Scheme-Compiler-mkWorld call))))(else (lambda (eta-0) (vector 1 call))))))))

13
bootstrap/idris2_app/idris2.ss
View File

@ -10,7 +10,10 @@
(let ()
(define (blodwen-os)
(case (machine-type)
[(i3le ti3le a6le ta6le) "unix"]
[(i3le ti3le a6le ta6le) "unix"] ; GNU/Linux
[(i3ob ti3ob a6ob ta6ob) "unix"] ; OpenBSD
[(i3fb ti3fb a6fb ta6fb) "unix"] ; FreeBSD
[(i3nb ti3nb a6nb ta6nb) "unix"] ; NetBSD
[(i3osx ti3osx a6osx ta6osx) "darwin"]
[(i3nt ti3nt a6nt ta6nt) "windows"]
[else "unknown"]))
@ -7305,9 +7308,9 @@
(define Racket-Scheme-Compiler-n--8783-872-callback (lambda (arg-0 arg-1 arg-2 arg-3 arg-4 arg-5 arg-6 arg-7 arg-8 arg-9 arg-10 arg-11) (let ((sc0 arg-11)) (case (vector-ref sc0 0) ((10) (let ((e-0 (vector-ref sc0 1))) (let ((e-1 (vector-ref sc0 2))) (Racket-Scheme-Compiler-n--8783-872-callback arg-0 arg-1 arg-2 arg-3 arg-4 arg-5 arg-6 arg-7 arg-8 arg-9 (vector 1 e-0 arg-10) e-1))))(else (let ((args (List-Data-reverse 'erased arg-10))) (lambda (eta-0) (let ((act-24 ((Core-Core-traverse 'erased 'erased (lambda (eta-1) (Racket-Scheme-Compiler-cftySpec arg-4 eta-1)) (List-Data-filter 'erased (lambda (eta-1) (Racket-Scheme-Compiler-n--8783-871-notWorld arg-0 arg-1 arg-2 arg-3 arg-4 arg-5 arg-6 arg-7 arg-8 eta-1)) args)) eta-0))) (let ((sc0 act-24)) (case (vector-ref sc0 0) ((0) (let ((e-2 (vector-ref sc0 1))) (vector 0 e-2))) (else (let ((act-25 ((Racket-Scheme-Compiler-cftySpec arg-4 arg-11) eta-0))) (let ((sc1 act-25)) (case (vector-ref sc1 0) ((0) (let ((e-2 (vector-ref sc1 1))) (vector 0 e-2))) (else (vector 1 (Racket-Scheme-Compiler-n--8783-870-mkFun arg-0 arg-1 arg-2 arg-3 arg-4 arg-5 arg-6 arg-7 arg-8 args arg-11 arg-9)))))))))))))))))
(define Racket-Scheme-Compiler-n--8783-869-applyLams (lambda (arg-0 arg-1 arg-2 arg-3 arg-4 arg-5 arg-6 arg-7 arg-8 arg-9 arg-10) (let ((sc0 arg-10)) (case (vector-ref sc0 0) ((0) arg-9) (else (let ((e-2 (vector-ref sc0 1))) (let ((e-3 (vector-ref sc0 2))) (let ((sc1 e-2)) (case (vector-ref sc1 0) ((0) (Racket-Scheme-Compiler-n--8783-869-applyLams arg-0 arg-1 arg-2 arg-3 arg-4 arg-5 arg-6 arg-7 arg-8 (Strings-Prelude-C-43C-43 "(" (Strings-Prelude-C-43C-43 arg-9 " #f)")) e-3)) (else (let ((e-6 (vector-ref sc1 1))) (let ((sc2 e-6)) (let ((e-9 (vector-ref sc2 1))) (let ((e-10 (vector-ref sc2 2))) (Racket-Scheme-Compiler-n--8783-869-applyLams arg-0 arg-1 arg-2 arg-3 arg-4 arg-5 arg-6 arg-7 arg-8 (Strings-Prelude-C-43C-43 "(" (Strings-Prelude-C-43C-43 arg-9 (Strings-Prelude-C-43C-43 " " (Strings-Prelude-C-43C-43 (Racket-Scheme-Compiler-cToRkt e-10 e-9) ")")))) e-3)))))))))))))))
(define Racket-Scheme-Compiler-useCC (lambda (arg-0 arg-1 arg-2 arg-3 arg-4 arg-5 arg-6 arg-7) (let ((sc0 arg-5)) (case (vector-ref sc0 0) ((0) (lambda (eta-0) (Core-Core-throw_Catchable__Core_Error 'erased (vector 47 arg-4 "No recognised foreign calling convention") eta-0))) (else (let ((e-2 (vector-ref sc0 1))) (let ((e-3 (vector-ref sc0 2))) (Racket-Scheme-Compiler-case--9479-1473 e-2 e-3 arg-7 arg-6 arg-4 arg-3 arg-2 arg-1 arg-0 (Common-Compiler-parseCC e-2)))))))))
(define Racket-Scheme-Compiler-startRacketWinSh (lambda (arg-0 arg-1 arg-2) (Strings-Data-unlines (vector 1 "#!/bin/sh" (vector 1 "DIR=\"`realpath \"$0\"`\"" (vector 1 (Strings-Prelude-C-43C-43 "export PATH=\"`dirname \"$DIR\"`/\"" (Strings-Prelude-C-43C-43 arg-1 "\":$PATH\"")) (vector 1 (Strings-Prelude-C-43C-43 arg-0 (Strings-Prelude-C-43C-43 "\"" (Strings-Prelude-C-43C-43 arg-2 "\" \"$@\""))) (vector 0 ))))))))
(define Racket-Scheme-Compiler-startRacketWinSh (lambda (arg-0 arg-1 arg-2) (Strings-Data-unlines (vector 1 "#!/bin/sh" (vector 1 "" (vector 1 "case `uname -s` in " (vector 1 " OpenBSD|FreeBSD|NetBSD) " (vector 1 " DIR=\"`grealpath $0`\"" (vector 1 " ;; " (vector 1 " " (vector 1 " *) " (vector 1 " DIR=\"`realpath $0`\" " (vector 1 " ;; " (vector 1 "esac " (vector 1 "" (vector 1 (Strings-Prelude-C-43C-43 "export PATH=\"`dirname \"$DIR\"`/\"" (Strings-Prelude-C-43C-43 arg-1 "\":$PATH\"")) (vector 1 (Strings-Prelude-C-43C-43 arg-0 (Strings-Prelude-C-43C-43 "\"" (Strings-Prelude-C-43C-43 arg-2 "\" \"$@\""))) (vector 0 ))))))))))))))))))
(define Racket-Scheme-Compiler-startRacketCmd (lambda (arg-0 arg-1 arg-2) (Strings-Data-unlines (vector 1 "@echo off" (vector 1 "set APPDIR=%~dp0" (vector 1 (Strings-Prelude-C-43C-43 "set PATH=%APPDIR%\\" (Strings-Prelude-C-43C-43 arg-1 ";%PATH%")) (vector 1 (Strings-Prelude-C-43C-43 arg-0 (Strings-Prelude-C-43C-43 "\"" (Strings-Prelude-C-43C-43 arg-2 "\" %*"))) (vector 0 ))))))))
(define Racket-Scheme-Compiler-startRacket (lambda (arg-0 arg-1 arg-2) (Strings-Data-unlines (vector 1 "#!/bin/sh" (vector 1 "" (vector 1 "DIR=\"`realpath $0`\"" (vector 1 (Strings-Prelude-C-43C-43 "export LD_LIBRARY_PATH=\"$LD_LIBRARY_PATH:`dirname \"$DIR\"`/\"" (Strings-Prelude-C-43C-43 arg-1 "\"\"")) (vector 1 (Strings-Prelude-C-43C-43 arg-0 (Strings-Prelude-C-43C-43 "\"`dirname \"$DIR\"`\"/\"" (Strings-Prelude-C-43C-43 arg-2 "\" \"$@\""))) (vector 0 )))))))))
(define Racket-Scheme-Compiler-startRacket (lambda (arg-0 arg-1 arg-2) (Strings-Data-unlines (vector 1 "#!/bin/sh" (vector 1 "" (vector 1 "case `uname -s` in " (vector 1 " OpenBSD|FreeBSD|NetBSD) " (vector 1 " DIR=\"`grealpath $0`\"" (vector 1 " ;; " (vector 1 " " (vector 1 " *) " (vector 1 " DIR=\"`realpath $0`\" " (vector 1 " ;; " (vector 1 "esac " (vector 1 "" (vector 1 (Strings-Prelude-C-43C-43 "export LD_LIBRARY_PATH=\"$LD_LIBRARY_PATH:`dirname \"$DIR\"`/\"" (Strings-Prelude-C-43C-43 arg-1 "\"\"")) (vector 1 (Strings-Prelude-C-43C-43 arg-0 (Strings-Prelude-C-43C-43 "\"`dirname \"$DIR\"`\"/\"" (Strings-Prelude-C-43C-43 arg-2 "\" \"$@\""))) (vector 0 ))))))))))))))))))
(define Racket-Scheme-Compiler-showRacketString (lambda (arg-0) (let ((sc0 arg-0)) (case (vector-ref sc0 0) ((0) (lambda (eta-0) eta-0)) (else (let ((e-2 (vector-ref sc0 1))) (let ((e-3 (vector-ref sc0 2))) (let ((sc1 e-2)) (cond ((equal? sc1 #\") (lambda (eta-0) (Strings-Prelude-C-43C-43 "\\\"" ((Racket-Scheme-Compiler-showRacketString e-3) eta-0))))(else (lambda (eta-0) ((Racket-Scheme-Compiler-showRacketChar e-2) ((Racket-Scheme-Compiler-showRacketString e-3) eta-0)))))))))))))
(define Racket-Scheme-Compiler-showRacketChar (lambda (arg-0) (let ((sc0 arg-0)) (cond ((equal? sc0 #\\) (lambda (arg-1) (Strings-Prelude-C-43C-43 "\\\\" arg-1)))(else (Racket-Scheme-Compiler-case--8220-334 arg-0 (Prelude-C-124C-124 (Prelude-C-60_Ord__Char arg-0 (Prelude-chr 32)) (lambda () (Prelude-C-62_Ord__Char arg-0 (Prelude-chr 126))))))))))
(define Racket-Scheme-Compiler-schemeCall (lambda (arg-0 arg-1 arg-2 arg-3) (let ((call (Strings-Prelude-C-43C-43 "(" (Strings-Prelude-C-43C-43 arg-1 (Strings-Prelude-C-43C-43 " " (Strings-Prelude-C-43C-43 (Name-Core-showSep " " (Prelude-map_Functor__List 'erased 'erased (lambda (eta-0) (Common-Scheme-Compiler-schName eta-0)) arg-2)) ")")))))) (let ((sc0 arg-3)) (case (vector-ref sc0 0) ((11) (lambda (eta-0) (vector 1 (Common-Scheme-Compiler-mkWorld call))))(else (lambda (eta-0) (vector 1 call))))))))
@ -7366,9 +7369,9 @@
(define Chez-Scheme-Compiler-n--8803-1177-applyLams (lambda (arg-0 arg-1 arg-2 arg-3 arg-4 arg-5 arg-6 arg-7 arg-8 arg-9) (let ((sc0 arg-9)) (case (vector-ref sc0 0) ((0) arg-8) (else (let ((e-2 (vector-ref sc0 1))) (let ((e-3 (vector-ref sc0 2))) (let ((sc1 e-2)) (case (vector-ref sc1 0) ((0) (Chez-Scheme-Compiler-n--8803-1177-applyLams arg-0 arg-1 arg-2 arg-3 arg-4 arg-5 arg-6 arg-7 (Strings-Prelude-C-43C-43 "(" (Strings-Prelude-C-43C-43 arg-8 " #f)")) e-3)) (else (let ((e-6 (vector-ref sc1 1))) (Chez-Scheme-Compiler-n--8803-1177-applyLams arg-0 arg-1 arg-2 arg-3 arg-4 arg-5 arg-6 arg-7 (Strings-Prelude-C-43C-43 "(" (Strings-Prelude-C-43C-43 arg-8 (Strings-Prelude-C-43C-43 " " (Strings-Prelude-C-43C-43 e-6 ")")))) e-3))))))))))))
(define Chez-Scheme-Compiler-useCC (lambda (arg-0 arg-1 arg-2 arg-3 arg-4 arg-5 arg-6) (let ((sc0 arg-4)) (case (vector-ref sc0 0) ((0) (lambda (eta-0) (Core-Core-throw_Catchable__Core_Error 'erased (vector 47 arg-3 "No recognised foreign calling convention") eta-0))) (else (let ((e-2 (vector-ref sc0 1))) (let ((e-3 (vector-ref sc0 2))) (Chez-Scheme-Compiler-case--9252-1575 e-2 e-3 arg-6 arg-5 arg-3 arg-2 arg-1 arg-0 (Common-Compiler-parseCC e-2)))))))))
(define Chez-Scheme-Compiler-tySpec (lambda (arg-0) (let ((sc0 arg-0)) (case (vector-ref sc0 0) ((5) (let ((e-0 (vector-ref sc0 1))) (let ((e-1 (vector-ref sc0 2))) (let ((e-3 (vector-ref sc0 4))) (let ((sc1 e-1)) (case (vector-ref sc1 0) ((1) (let ((e-4 (vector-ref sc1 1))) (let ((sc2 e-4)) (cond ((equal? sc2 "Int") (let ((sc3 e-3)) (case (vector-ref sc3 0) ((0) (lambda (eta-0) (vector 1 "int")))(else (lambda (eta-0) (Core-Core-throw_Catchable__Core_Error 'erased (vector 47 (NamedCExp-CompileExpr-Core-getFC arg-0) (Strings-Prelude-C-43C-43 "Can't pass argument of type " (Strings-Prelude-C-43C-43 (CompileExpr-Core-show_Show__NamedCExp arg-0) " to foreign function"))) eta-0)))))) ((equal? sc2 "String") (let ((sc3 e-3)) (case (vector-ref sc3 0) ((0) (lambda (eta-0) (vector 1 "string")))(else (lambda (eta-0) (Core-Core-throw_Catchable__Core_Error 'erased (vector 47 (NamedCExp-CompileExpr-Core-getFC arg-0) (Strings-Prelude-C-43C-43 "Can't pass argument of type " (Strings-Prelude-C-43C-43 (CompileExpr-Core-show_Show__NamedCExp arg-0) " to foreign function"))) eta-0)))))) ((equal? sc2 "Double") (let ((sc3 e-3)) (case (vector-ref sc3 0) ((0) (lambda (eta-0) (vector 1 "double")))(else (lambda (eta-0) (Core-Core-throw_Catchable__Core_Error 'erased (vector 47 (NamedCExp-CompileExpr-Core-getFC arg-0) (Strings-Prelude-C-43C-43 "Can't pass argument of type " (Strings-Prelude-C-43C-43 (CompileExpr-Core-show_Show__NamedCExp arg-0) " to foreign function"))) eta-0)))))) ((equal? sc2 "Char") (let ((sc3 e-3)) (case (vector-ref sc3 0) ((0) (lambda (eta-0) (vector 1 "char")))(else (lambda (eta-0) (Core-Core-throw_Catchable__Core_Error 'erased (vector 47 (NamedCExp-CompileExpr-Core-getFC arg-0) (Strings-Prelude-C-43C-43 "Can't pass argument of type " (Strings-Prelude-C-43C-43 (CompileExpr-Core-show_Show__NamedCExp arg-0) " to foreign function"))) eta-0))))))(else (lambda (eta-0) (Core-Core-throw_Catchable__Core_Error 'erased (vector 47 (NamedCExp-CompileExpr-Core-getFC arg-0) (Strings-Prelude-C-43C-43 "Can't pass argument of type " (Strings-Prelude-C-43C-43 (CompileExpr-Core-show_Show__NamedCExp arg-0) " to foreign function"))) eta-0))))))) ((0) (let ((e-6 (vector-ref sc1 2))) (let ((sc2 e-3)) (case (vector-ref sc2 0) ((1) (let ((e-13 (vector-ref sc2 2))) (let ((sc3 e-13)) (case (vector-ref sc3 0) ((0) (Core-Core-cond 'erased (vector 1 (vector 0 (lambda () (Name-Core-C-61C-61_Eq__Name e-6 (vector 1 "Ptr"))) (lambda () (lambda (eta-0) (vector 1 "void*")))) (vector 1 (vector 0 (lambda () (Name-Core-C-61C-61_Eq__Name e-6 (vector 1 "GCPtr"))) (lambda () (lambda (eta-0) (vector 1 "void*")))) (vector 1 (vector 0 (lambda () (Name-Core-C-61C-61_Eq__Name e-6 (vector 1 "Buffer"))) (lambda () (lambda (eta-0) (vector 1 "u8*")))) (vector 0 )))) (lambda (eta-0) (Core-Core-throw_Catchable__Core_Error 'erased (vector 47 e-0 (Strings-Prelude-C-43C-43 "Can't pass argument of type " (Strings-Prelude-C-43C-43 (Name-Core-show_Show__Name e-6) " to foreign function"))) eta-0))))(else (lambda (eta-0) (Core-Core-throw_Catchable__Core_Error 'erased (vector 47 (NamedCExp-CompileExpr-Core-getFC arg-0) (Strings-Prelude-C-43C-43 "Can't pass argument of type " (Strings-Prelude-C-43C-43 (CompileExpr-Core-show_Show__NamedCExp arg-0) " to foreign function"))) eta-0))))))) ((0) (Core-Core-cond 'erased (vector 1 (vector 0 (lambda () (Name-Core-C-61C-61_Eq__Name e-6 (vector 1 "Unit"))) (lambda () (lambda (eta-0) (vector 1 "void")))) (vector 1 (vector 0 (lambda () (Name-Core-C-61C-61_Eq__Name e-6 (vector 1 "AnyPtr"))) (lambda () (lambda (eta-0) (vector 1 "void*")))) (vector 1 (vector 0 (lambda () (Name-Core-C-61C-61_Eq__Name e-6 (vector 1 "GCAnyPtr"))) (lambda () (lambda (eta-0) (vector 1 "void*")))) (vector 0 )))) (lambda (eta-0) (Core-Core-throw_Catchable__Core_Error 'erased (vector 47 e-0 (Strings-Prelude-C-43C-43 "Can't pass argument of type " (Strings-Prelude-C-43C-43 (Name-Core-show_Show__Name e-6) " to foreign function"))) eta-0))))(else (lambda (eta-0) (Core-Core-throw_Catchable__Core_Error 'erased (vector 47 (NamedCExp-CompileExpr-Core-getFC arg-0) (Strings-Prelude-C-43C-43 "Can't pass argument of type " (Strings-Prelude-C-43C-43 (CompileExpr-Core-show_Show__NamedCExp arg-0) " to foreign function"))) eta-0)))))))(else (lambda (eta-0) (Core-Core-throw_Catchable__Core_Error 'erased (vector 47 (NamedCExp-CompileExpr-Core-getFC arg-0) (Strings-Prelude-C-43C-43 "Can't pass argument of type " (Strings-Prelude-C-43C-43 (CompileExpr-Core-show_Show__NamedCExp arg-0) " to foreign function"))) eta-0)))))))))(else (lambda (eta-0) (Core-Core-throw_Catchable__Core_Error 'erased (vector 47 (NamedCExp-CompileExpr-Core-getFC arg-0) (Strings-Prelude-C-43C-43 "Can't pass argument of type " (Strings-Prelude-C-43C-43 (CompileExpr-Core-show_Show__NamedCExp arg-0) " to foreign function"))) eta-0)))))))
(define Chez-Scheme-Compiler-startChezWinSh (lambda (arg-0 arg-1 arg-2) (Strings-Data-unlines (vector 1 "#!/bin/sh" (vector 1 "DIR=\"`realpath \"$0\"`\"" (vector 1 (Strings-Prelude-C-43C-43 "CHEZ=$(cygpath \"" (Strings-Prelude-C-43C-43 arg-0 "\")")) (vector 1 (Strings-Prelude-C-43C-43 "export PATH=\"`dirname \"$DIR\"`/\"" (Strings-Prelude-C-43C-43 arg-1 "\":$PATH\"")) (vector 1 (Strings-Prelude-C-43C-43 "$CHEZ --script \"$(dirname \"$DIR\")/" (Strings-Prelude-C-43C-43 arg-2 "\" \"$@\"")) (vector 0 )))))))))
(define Chez-Scheme-Compiler-startChezWinSh (lambda (arg-0 arg-1 arg-2) (Strings-Data-unlines (vector 1 "#!/bin/sh" (vector 1 "" (vector 1 "case `uname -s` in " (vector 1 " OpenBSD|FreeBSD|NetBSD) " (vector 1 " DIR=\"`grealpath $0`\"" (vector 1 " ;; " (vector 1 " " (vector 1 " *) " (vector 1 " DIR=\"`realpath $0`\" " (vector 1 " ;; " (vector 1 "esac " (vector 1 "" (vector 1 (Strings-Prelude-C-43C-43 "CHEZ=$(cygpath \"" (Strings-Prelude-C-43C-43 arg-0 "\")")) (vector 1 (Strings-Prelude-C-43C-43 "export PATH=\"`dirname \"$DIR\"`/\"" (Strings-Prelude-C-43C-43 arg-1 "\":$PATH\"")) (vector 1 (Strings-Prelude-C-43C-43 "$CHEZ --script \"$(dirname \"$DIR\")/" (Strings-Prelude-C-43C-43 arg-2 "\" \"$@\"")) (vector 0 )))))))))))))))))))
(define Chez-Scheme-Compiler-startChezCmd (lambda (arg-0 arg-1 arg-2) (Strings-Data-unlines (vector 1 "@echo off" (vector 1 "set APPDIR=%~dp0" (vector 1 (Strings-Prelude-C-43C-43 "set PATH=%APPDIR%\\" (Strings-Prelude-C-43C-43 arg-1 ";%PATH%")) (vector 1 (Strings-Prelude-C-43C-43 "\"" (Strings-Prelude-C-43C-43 arg-0 (Strings-Prelude-C-43C-43 "\" --script \"%APPDIR%/" (Strings-Prelude-C-43C-43 arg-2 "\" %*")))) (vector 0 ))))))))
(define Chez-Scheme-Compiler-startChez (lambda (arg-0 arg-1) (Strings-Data-unlines (vector 1 "#!/bin/sh" (vector 1 "" (vector 1 "DIR=\"`realpath $0`\"" (vector 1 (Strings-Prelude-C-43C-43 "export LD_LIBRARY_PATH=\"$LD_LIBRARY_PATH:`dirname \"$DIR\"`/\"" (Strings-Prelude-C-43C-43 arg-0 "\"\"")) (vector 1 (Strings-Prelude-C-43C-43 "\"`dirname \"$DIR\"`\"/\"" (Strings-Prelude-C-43C-43 arg-1 "\" \"$@\"")) (vector 0 )))))))))
(define Chez-Scheme-Compiler-startChez (lambda (arg-0 arg-1) (Strings-Data-unlines (vector 1 "#!/bin/sh" (vector 1 "" (vector 1 "case `uname -s` in " (vector 1 " OpenBSD|FreeBSD|NetBSD) " (vector 1 " DIR=\"`grealpath $0`\"" (vector 1 " ;; " (vector 1 " " (vector 1 " *) " (vector 1 " DIR=\"`realpath $0`\" " (vector 1 " ;; " (vector 1 "esac " (vector 1 "" (vector 1 (Strings-Prelude-C-43C-43 "export LD_LIBRARY_PATH=\"$LD_LIBRARY_PATH:`dirname \"$DIR\"`/\"" (Strings-Prelude-C-43C-43 arg-0 "\"\"")) (vector 1 (Strings-Prelude-C-43C-43 "\"`dirname \"$DIR\"`\"/\"" (Strings-Prelude-C-43C-43 arg-1 "\" \"$@\"")) (vector 0 ))))))))))))))))))
(define Chez-Scheme-Compiler-showChezString (lambda (arg-0) (let ((sc0 arg-0)) (case (vector-ref sc0 0) ((0) (lambda (eta-0) eta-0)) (else (let ((e-2 (vector-ref sc0 1))) (let ((e-3 (vector-ref sc0 2))) (let ((sc1 e-2)) (cond ((equal? sc1 #\") (lambda (eta-0) (Strings-Prelude-C-43C-43 "\\\"" ((Chez-Scheme-Compiler-showChezString e-3) eta-0))))(else (lambda (eta-0) ((Chez-Scheme-Compiler-showChezChar e-2) ((Chez-Scheme-Compiler-showChezString e-3) eta-0)))))))))))))
(define Chez-Scheme-Compiler-showChezChar (lambda (arg-0) (let ((sc0 arg-0)) (cond ((equal? sc0 #\\) (lambda (arg-1) (Strings-Prelude-C-43C-43 "\\\\" arg-1)))(else (Chez-Scheme-Compiler-case--8090-452 arg-0 (Prelude-C-124C-124 (Prelude-C-60_Ord__Char arg-0 (Prelude-chr 32)) (lambda () (Prelude-C-62_Ord__Char arg-0 (Prelude-chr 126))))))))))
(define Chez-Scheme-Compiler-schemeCall (lambda (arg-0 arg-1 arg-2 arg-3) (let ((call (Strings-Prelude-C-43C-43 "(" (Strings-Prelude-C-43C-43 arg-1 (Strings-Prelude-C-43C-43 " " (Strings-Prelude-C-43C-43 (Name-Core-showSep " " (Prelude-map_Functor__List 'erased 'erased (lambda (eta-0) (Common-Scheme-Compiler-schName eta-0)) arg-2)) ")")))))) (let ((sc0 arg-3)) (case (vector-ref sc0 0) ((11) (lambda (eta-0) (vector 1 (Common-Scheme-Compiler-mkWorld call))))(else (lambda (eta-0) (vector 1 call))))))))

5
config.mk
View File

@ -36,7 +36,6 @@ else
SHLIB_SUFFIX := .so
CFLAGS += -fPIC
endif
export OS
ifeq ($(OS),bsd)
@ -44,3 +43,7 @@ ifeq ($(OS),bsd)
else
MAKE := make
endif
export MAKE
# Add a custom.mk file to override any of the configurations
-include custom.mk

72
docs/source/backends/custom.rst Normal file
View File

@ -0,0 +1,72 @@
**********************************
Building Idris 2 with new backends
**********************************
The way to extend Idris 2 with new backends is to use it as
a library. The module ``Idris.Driver`` exports the function
``mainWithCodegens``, that takes a list of ``(String, Codegen)``,
starting idris with these codegens in addition to the built-in ones.
Getting started
===============
To use Idris 2 as a library you need to install it with (the ipkg file
is at the top level of the Idris2 repo)
::
idris2 --build idris2api.ipkg
idris2 --install idris2api.ipkg
Now create a file containing
.. code-block:: idris
module Main
import Core.Context
import Compiler.Common
import Idris.Driver
compile : Ref Ctxt Defs -> (execDir : String) ->
ClosedTerm -> (outfile : String) -> Core (Maybe String)
compile defs dir term file = do coreLift $ putStrLn "I'd rather not."
pure $ Nothing
execute : Ref Ctxt Defs -> (execDir : String) -> ClosedTerm -> Core ()
execute defs dir term = do coreLift $ putStrLn "Maybe in an hour."
lazyCodegen : Codegen
lazyCodegen = MkCG compile execute
main : IO ()
main = mainWithCodegens [("lazy", lazyCodegen)]
Build it with
::
$ idris2 -p idris2 -p contrib -p network Lazy.idr -o lazy-idris2
Now you have an idris2 with an added backend.
::
$ ./build/exec/lazy-idris2
____ __ _ ___
/ _/___/ /____(_)____ |__ \
/ // __ / ___/ / ___/ __/ / Version 0.2.0-d8c7f08bd
_/ // /_/ / / / (__ ) / __/ https://www.idris-lang.org
/___/\__,_/_/ /_/____/ /____/ Type :? for help
Welcome to Idris 2. Enjoy yourself!
With codegen for: lazy
Main>
It will not be overly eager to actually compile any code with the new backend though
::
$ ./build/exec/lazy --cg lazy Hello.idr -o hello
I'd rather not.
$

1
docs/source/backends/index.rst
View File

@ -60,3 +60,4 @@ or via the `IDRIS2_CG` environment variable.
chez
racket
gambit
custom

3
idris2.ipkg
View File

@ -61,6 +61,7 @@ modules =
Idris.CommandLine,
Idris.Desugar,
Idris.Driver,
Idris.Elab.Implementation,
Idris.Elab.Interface,
Idris.Error,
@ -69,6 +70,7 @@ modules =
Idris.IDEMode.MakeClause,
Idris.IDEMode.Parser,
Idris.IDEMode.REPL,
Idris.IDEMode.SyntaxHighlight,
Idris.IDEMode.TokenLine,
Idris.IDEMode.Holes,
Idris.ModTree,
@ -145,6 +147,7 @@ modules =
TTImp.WithClause,
Utils.Binary,
Utils.Either,
Utils.Hex,
Utils.Octal,
Utils.Shunting,

4
idris2api.ipkg
View File

@ -60,6 +60,7 @@ modules =
Idris.CommandLine,
Idris.Desugar,
Idris.Driver,
Idris.Elab.Implementation,
Idris.Elab.Interface,
Idris.Error,
@ -68,6 +69,7 @@ modules =
Idris.IDEMode.MakeClause,
Idris.IDEMode.Parser,
Idris.IDEMode.REPL,
Idris.IDEMode.SyntaxHighlight,
Idris.IDEMode.TokenLine,
Idris.IDEMode.Holes,
Idris.ModTree,
@ -119,6 +121,7 @@ modules =
TTImp.Elab.Quote,
TTImp.Elab.Record,
TTImp.Elab.Rewrite,
TTImp.Elab.RunElab,
TTImp.Elab.Term,
TTImp.Elab.Utils,
TTImp.Impossible,
@ -143,6 +146,7 @@ modules =
TTImp.WithClause,
Utils.Binary,
Utils.Either,
Utils.Hex,
Utils.Octal,
Utils.Shunting,

33
libs/base/Control/App/FileIO.idr
View File

@ -16,12 +16,16 @@ toFileEx FileExists = FileExists
public export
interface Has [Exception IOError] e => FileIO e where
withFile : String -> Mode ->
withFile : String -> Mode ->
(onError : IOError -> App e a) ->
(onOpen : File -> App e a) ->
(onOpen : File -> App e a) ->
App e a
fGetStr : File -> App e String
fGetChars : File -> Int -> App e String
fGetChar : File -> App e Char
fPutStr : File -> String -> App e ()
fPutStrLn : File -> String -> App e ()
fflush : File -> App e ()
fEOF : File -> App e Bool
-- TODO : Add Binary File IO with buffers
@ -41,23 +45,32 @@ readFile f
else do str <- fGetStr h
read (str :: acc) h
fileOp : IO (Either FileError a) -> Has [PrimIO, Exception IOError] e => App e a
fileOp fileRes
= do Right res <- primIO $ fileRes
| Left err => throw (FileErr (toFileEx err))
pure res
export
Has [PrimIO, Exception IOError] e => FileIO e where
withFile fname m onError proc
= do Right h <- primIO $ openFile fname m
| Left err => onError (FileErr (toFileEx err))
res <- catch (proc h) onError
primIO $ closeFile h
pure res
fGetStr f
= do Right str <- primIO $ fGetLine f
| Left err => throw (FileErr (toFileEx err))
pure str
fGetStr f = fileOp (fGetLine f)
fPutStr f str
= do Right () <- primIO $ File.fPutStr f str
| Left err => throw (FileErr (toFileEx err))
pure ()
fGetChars f n = fileOp (fGetChars f n)
fGetChar f = fileOp (fGetChar f)
fPutStr f str = fileOp (fPutStr f str)
fPutStrLn f str = fileOp (File.fPutStrLn f str)
fflush f = primIO $ fflush f
fEOF f = primIO $ fEOF f

99
libs/base/Data/Bool.idr Normal file
View File

@ -0,0 +1,99 @@
module Data.Bool
%default total
export
notInvolutive : (x : Bool) -> not (not x) = x
notInvolutive True = Refl
notInvolutive False = Refl
-- AND
export
andSameNeutral : (x : Bool) -> x && x = x
andSameNeutral False = Refl
andSameNeutral True = Refl
export
andFalseFalse : (x : Bool) -> x && False = False
andFalseFalse False = Refl
andFalseFalse True = Refl
export
andTrueNeutral : (x : Bool) -> x && True = x
andTrueNeutral False = Refl
andTrueNeutral True = Refl
export
andAssociative : (x, y, z : Bool) -> x && (y && z) = (x && y) && z
andAssociative True _ _ = Refl
andAssociative False _ _ = Refl
export
andCommutative : (x, y : Bool) -> x && y = y && x
andCommutative x True = andTrueNeutral x
andCommutative x False = andFalseFalse x
export
andNotFalse : (x : Bool) -> x && not x = False
andNotFalse False = Refl
andNotFalse True = Refl
-- OR
export
orSameNeutral : (x : Bool) -> x || x = x
orSameNeutral False = Refl
orSameNeutral True = Refl
export
orFalseNeutral : (x : Bool) -> x || False = x
orFalseNeutral False = Refl
orFalseNeutral True = Refl
export
orTrueTrue : (x : Bool) -> x || True = True
orTrueTrue False = Refl
orTrueTrue True = Refl
export
orAssociative : (x, y, z : Bool) -> x || (y || z) = (x || y) || z
orAssociative True _ _ = Refl
orAssociative False _ _ = Refl
export
orCommutative : (x, y : Bool) -> x || y = y || x
orCommutative x True = orTrueTrue x
orCommutative x False = orFalseNeutral x
export
orNotTrue : (x : Bool) -> x || not x = True
orNotTrue False = Refl
orNotTrue True = Refl
-- interaction & De Morgan's laws
export
orSameAndRightNeutral : (x, y : Bool) -> x || (x && y) = x
orSameAndRightNeutral False _ = Refl
orSameAndRightNeutral True _ = Refl
export
andDistribOrR : (x, y, z : Bool) -> x && (y || z) = (x && y) || (x && z)
andDistribOrR False _ _ = Refl
andDistribOrR True _ _ = Refl
export
orDistribAndR : (x, y, z : Bool) -> x || (y && z) = (x || y) && (x || z)
orDistribAndR False _ _ = Refl
orDistribAndR True _ _ = Refl
export
notAndIsOr : (x, y : Bool) -> not (x && y) = not x || not y
notAndIsOr False _ = Refl
notAndIsOr True _ = Refl
export
notOrIsAnd : (x, y : Bool) -> not (x || y) = not x && not y
notOrIsAnd False _ = Refl
notOrIsAnd True _ = Refl

64
libs/base/Data/Bool/Xor.idr Normal file
View File

@ -0,0 +1,64 @@
module Data.Bool.Xor
import Data.Bool
%default total
public export
xor : Bool -> Bool -> Bool
xor True True = False
xor False False = False
xor _ _ = True
export
xorSameFalse : (b : Bool) -> xor b b = False
xorSameFalse False = Refl
xorSameFalse True = Refl
export
xorFalseNeutral : (b : Bool) -> xor False b = b
xorFalseNeutral False = Refl
xorFalseNeutral True = Refl
export
xorTrueNot : (b : Bool) -> xor True b = not b
xorTrueNot False = Refl
xorTrueNot True = Refl
export
notXor : (a, b : Bool) -> not (xor a b) = xor (not a) b
notXor True b = rewrite xorFalseNeutral b in
rewrite xorTrueNot b in
notInvolutive b
notXor False b = rewrite xorFalseNeutral b in
sym $ xorTrueNot b
export
notXorCancel : (a, b : Bool) -> xor (not a) (not b) = xor a b
notXorCancel True b = rewrite xorFalseNeutral (not b) in
sym $ xorTrueNot b
notXorCancel False b = rewrite xorFalseNeutral b in
rewrite xorTrueNot (not b) in
notInvolutive b
export
xorAssociative : (a, b, c : Bool) -> xor (xor a b) c = xor a (xor b c)
xorAssociative False b c =
rewrite xorFalseNeutral b in
sym $ xorFalseNeutral (xor b c)
xorAssociative True b c =
rewrite xorTrueNot b in
rewrite xorTrueNot (xor b c) in
sym $ notXor b c
export
xorCommutative : (a, b : Bool) -> xor a b = xor b a
xorCommutative False False = Refl
xorCommutative False True = Refl
xorCommutative True False = Refl
xorCommutative True True = Refl
export
xorNotTrue : (a : Bool) -> a `xor` (not a) = True
xorNotTrue False = Refl
xorNotTrue True = Refl

8
libs/base/Data/Fin.idr
View File

@ -79,6 +79,14 @@ weakenN : (n : Nat) -> Fin m -> Fin (m + n)
weakenN n FZ = FZ
weakenN n (FS f) = FS (weakenN n f)
||| Weaken the bound on a Fin using a constructive comparison
public export
weakenLTE : Fin n -> LTE n m -> Fin m
weakenLTE FZ LTEZero impossible
weakenLTE (FS _) LTEZero impossible
weakenLTE FZ (LTESucc y) = FZ
weakenLTE (FS x) (LTESucc y) = FS $ weakenLTE x y
||| Attempt to tighten the bound on a Fin.
||| Return `Left` if the bound could not be tightened, or `Right` if it could.
export

49
libs/base/Data/Nat.idr
View File

@ -319,6 +319,11 @@ plusLeftLeftRightZero left right p =
rewrite plusZeroRightNeutral left in
p
plusLteMonotoneRight : (p, q, r : Nat) -> q `LTE` r -> (q+p) `LTE` (r+p)
plusLteMonotoneRight p Z r LTEZero = rewrite plusCommutative r p in
lteAddRight p
plusLteMonotoneRight p (S q) (S r) (LTESucc l) = LTESucc $ plusLteMonotoneRight p q r l
-- Proofs on *
export
@ -426,6 +431,14 @@ minusPlusZero : (n, m : Nat) -> minus n (n + m) = Z
minusPlusZero Z _ = Refl
minusPlusZero (S n) m = minusPlusZero n m
export
plusMinusLte : (n, m : Nat) -> LTE n m -> (minus m n) + n = m
plusMinusLte Z m _ = rewrite minusZeroRight m in
plusZeroRightNeutral m
plusMinusLte (S _) Z lte = absurd lte
plusMinusLte (S n) (S m) lte = rewrite sym $ plusSuccRightSucc (minus m n) n in
cong S $ plusMinusLte n m (fromLteSucc lte)
export
minusMinusMinusPlus : (left, centre, right : Nat) ->
minus (minus left centre) right = minus left (centre + right)
@ -506,9 +519,9 @@ maximumCommutative Z (S _) = Refl
maximumCommutative (S _) Z = Refl
maximumCommutative (S k) (S j) = rewrite maximumCommutative k j in Refl
-- maximumIdempotent : (n : Nat) -> maximum n n = n
-- maximumIdempotent Z = Refl
-- maximumIdempotent (S k) = cong $ maximumIdempotent k
maximumIdempotent : (n : Nat) -> maximum n n = n
maximumIdempotent Z = Refl
maximumIdempotent (S k) = cong S $ maximumIdempotent k
minimumAssociative : (l, c, r : Nat) ->
minimum l (minimum c r) = minimum (minimum l c) r
@ -523,9 +536,9 @@ minimumCommutative Z (S _) = Refl
minimumCommutative (S _) Z = Refl
minimumCommutative (S k) (S j) = rewrite minimumCommutative k j in Refl
-- minimumIdempotent : (n : Nat) -> minimum n n = n
-- minimumIdempotent Z = Refl
-- minimumIdempotent (S k) = cong (minimumIdempotent k)
minimumIdempotent : (n : Nat) -> minimum n n = n
minimumIdempotent Z = Refl
minimumIdempotent (S k) = cong S $ minimumIdempotent k
minimumZeroZeroLeft : (left : Nat) -> minimum left 0 = Z
minimumZeroZeroLeft left = rewrite minimumCommutative left 0 in Refl
@ -541,18 +554,18 @@ maximumSuccSucc : (left, right : Nat) ->
S (maximum left right) = maximum (S left) (S right)
maximumSuccSucc _ _ = Refl
-- sucMaxL : (l : Nat) -> maximum (S l) l = (S l)
-- sucMaxL Z = Refl
-- sucMaxL (S l) = cong $ sucMaxL l
sucMaxL : (l : Nat) -> maximum (S l) l = (S l)
sucMaxL Z = Refl
sucMaxL (S l) = cong S $ sucMaxL l
-- sucMaxR : (l : Nat) -> maximum l (S l) = (S l)
-- sucMaxR Z = Refl
-- sucMaxR (S l) = cong $ sucMaxR l
sucMaxR : (l : Nat) -> maximum l (S l) = (S l)
sucMaxR Z = Refl
sucMaxR (S l) = cong S $ sucMaxR l
-- sucMinL : (l : Nat) -> minimum (S l) l = l
-- sucMinL Z = Refl
-- sucMinL (S l) = cong $ sucMinL l
sucMinL : (l : Nat) -> minimum (S l) l = l
sucMinL Z = Refl
sucMinL (S l) = cong S $ sucMinL l
-- sucMinR : (l : Nat) -> minimum l (S l) = l
-- sucMinR Z = Refl
-- sucMinR (S l) = cong $ sucMinR l
sucMinR : (l : Nat) -> minimum l (S l) = l
sucMinR Z = Refl
sucMinR (S l) = cong S $ sucMinR l

48
libs/base/Data/So.idr
View File

@ -1,5 +1,9 @@
module Data.So
import Data.Bool
%default total
||| Ensure that some run-time Boolean test has been performed.
|||
||| This lifts a Boolean predicate to the type level. See the function `choose`
@ -14,7 +18,7 @@ data So : Bool -> Type where
Oh : So True
export
implementation Uninhabited (So False) where
Uninhabited (So False) where
uninhabited Oh impossible
||| Perform a case analysis on a Boolean, providing clients with a `So` proof
@ -23,3 +27,45 @@ choose : (b : Bool) -> Either (So b) (So (not b))
choose True = Left Oh
choose False = Right Oh
export
eqToSo : b = True -> So b
eqToSo Refl = Oh
export
soToEq : So b -> b = True
soToEq Oh = Refl
||| If `b` is True, `not b` can't be True
export
soToNotSoNot : So b -> Not (So (not b))
soToNotSoNot Oh = uninhabited
||| If `not b` is True, `b` can't be True
export
soNotToNotSo : So (not b) -> Not (So b)
soNotToNotSo = flip soToNotSoNot
export
soAnd : {a : Bool} -> So (a && b) -> (So a, So b)
soAnd soab with (choose a)
soAnd {a=True} soab | Left Oh = (Oh, soab)
soAnd {a=True} soab | Right prf = absurd prf
soAnd {a=False} soab | Right prf = absurd soab
export
andSo : (So a, So b) -> So (a && b)
andSo (Oh, Oh) = Oh
export
soOr : {a : Bool} -> So (a || b) -> Either (So a) (So b)
soOr soab with (choose a)
soOr {a=True} _ | Left Oh = Left Oh
soOr {a=False} _ | Left Oh impossible
soOr {a=False} soab | Right Oh = Right soab
soOr {a=True} _ | Right Oh impossible
export
orSo : Either (So a) (So b) -> So (a || b)
orSo (Left Oh) = Oh
orSo (Right Oh) = rewrite orTrueTrue a in
Oh

4
libs/base/System.idr
View File

@ -39,9 +39,9 @@ prim_getEnv : String -> PrimIO (Ptr String)
%foreign support "idris2_getEnvPair"
prim_getEnvPair : Int -> PrimIO (Ptr String)
%foreign libc "setenv"
%foreign support "idris2_setenv"
prim_setEnv : String -> String -> Int -> PrimIO Int
%foreign libc "setenv"
%foreign support "idris2_unsetenv"
prim_unsetEnv : String -> PrimIO Int
export

2
libs/base/base.ipkg
View File

@ -9,6 +9,8 @@ modules = Control.App,
Control.Monad.Trans,
Control.WellFounded,
Data.Bool,
Data.Bool.Xor,
Data.Buffer,
Data.Either,
Data.Fin,

36
libs/contrib/Data/Bool/Extra.idr
View File

@ -1,36 +0,0 @@
module Data.Bool.Extra
public export
andSameNeutral : (x : Bool) -> x && x = x
andSameNeutral False = Refl
andSameNeutral True = Refl
public export
andFalseFalse : (x : Bool) -> x && False = False
andFalseFalse False = Refl
andFalseFalse True = Refl
public export
andTrueNeutral : (x : Bool) -> x && True = x
andTrueNeutral False = Refl
andTrueNeutral True = Refl
public export
orSameNeutral : (x : Bool) -> x || x = x
orSameNeutral False = Refl
orSameNeutral True = Refl
public export
orFalseNeutral : (x : Bool) -> x || False = x
orFalseNeutral False = Refl
orFalseNeutral True = Refl
public export
orTrueTrue : (x : Bool) -> x || True = True
orTrueTrue False = Refl
orTrueTrue True = Refl
public export
orSameAndRightNeutral : (x, right : Bool) -> x || (x && right) = x
orSameAndRightNeutral False _ = Refl
orSameAndRightNeutral True _ = Refl

1
libs/contrib/Data/Fin/Extra.idr
View File

@ -5,7 +5,6 @@ import Data.Nat
%default total
||| Proof that an element **n** of Fin **m** , when converted to Nat is smaller than the bound **m**.
export
elemSmallerThanBound : (n : Fin m) -> LT (finToNat n) m

160
libs/contrib/Data/Logic/Propositional.idr Normal file
View File

@ -0,0 +1,160 @@
module Data.Logic.Propositional
%default total
-- Idris uses intuitionistic logic, so it does not validate the
-- principle of excluded middle (PEM) or similar theorems of classical
-- logic. But it does validate certain relations among these
-- propositions, and that's what's in this file.
||| The principle of excluded middle
PEM : Type -> Type
PEM p = Either p (Not p)
||| Double negation elimination
DNE : Type -> Type
DNE p = Not $ Not p -> p
||| The consensus theorem (at least, the interesting part)
Consensus : Type -> Type -> Type -> Type
Consensus p q r = (q, r) -> Either (p, q) (Not p, r)
||| Peirce's law
Peirce : Type -> Type -> Type
Peirce p q = ((p -> q) -> p) -> p
||| Not sure if this one has a name, so call it Frege's law
Frege : Type -> Type -> Type -> Type
Frege p q r = (p -> r) -> (q -> r) -> ((p -> q) -> q) -> r
||| The converse of contraposition: (p -> q) -> Not q -> Not p
Transposition : Type -> Type -> Type
Transposition p q = (Not q -> Not p) -> p -> q
||| This isn't a good name.
Switch : Type -> Type
Switch p = (Not p -> p) -> p
-- PEM and the others can't be proved outright, but it is possible to
-- prove the double negations (DN) of all of them.
||| The double negation of a proposition
DN : Type -> Type
DN p = Not $ Not p
pemDN : DN $ PEM p
pemDN f = f $ Right $ \x => f $ Left x
dneDN : DN $ DNE p
dneDN f = f $ \g => void $ g $ \x => f $ \_ => x
consensusDN : DN $ Consensus p q r
consensusDN f = f $ \(y, z) => Right (\x => f $ \(_, _) => Left (x, y), z)
peirceDN : DN $ Peirce p q
peirceDN f = f $ \g => g $ \x => void $ f $ \_ => x
fregeDN : DN $ Frege p q r
fregeDN f = f $ \g, h, i => h $ i $ \x => void $ f $ \_, _, _ => g x
transpositionDN : DN $ Transposition p q
transpositionDN f = f $ \g, x => void $ g (\y => f $ \_, _ => y) x
switchDN : DN $ Switch p
switchDN f = f $ \g => g $ \x => f $ \_ => x
-- It's easy to prove all these theorems assuming PEM.
dnePEM : PEM p -> DNE p
dnePEM (Left l) _ = l
dnePEM (Right r) f = void $ f r
consensusPEM : PEM p -> Consensus p q r
consensusPEM (Left l) (y, _) = Left (l, y)
consensusPEM (Right r) (_, z) = Right (r, z)
peircePEM : PEM p -> Peirce p q
peircePEM (Left l) _ = l
peircePEM (Right r) f = f $ \x => void $ r x
fregePEM : PEM p -> Frege p q r
fregePEM (Left l) f _ _ = f l
fregePEM (Right r) _ g h = g $ h $ \x => void $ r x
transpositionPEM : PEM p -> Transposition q p
transpositionPEM (Left l) _ _ = l
transpositionPEM (Right r) f x = void $ f r x
switchPEM : PEM p -> Switch p
switchPEM (Left l) _ = l
switchPEM (Right r) f = f r
-- It's trivial to prove these theorems assuming double negation
-- elimination (DNE), since their double negations can all be proved.
||| Eliminate double negations
EDN : DN p -> DNE p -> p
EDN f g = g f
pemDNE : DNE $ PEM p -> PEM p
pemDNE = EDN pemDN
-- It's possible to prove the theorems assuming Peirce's law, but some
-- thought must be given to choosing the right instances. Peirce's law
-- is therefore weaker than PEM on an instance-by-instance basis, but
-- all the instances together are equivalent.
pemPeirce : Peirce (PEM p) Void -> PEM p
pemPeirce f = f $ \g => Right $ \x => g $ Left x
dnePeirce : Peirce p Void -> DNE p
dnePeirce f g = f $ \h => void $ g h
consensusPeirce : Peirce (Consensus p q r) Void -> Consensus p q r
consensusPeirce f (y, z) =
f (\g, (_, _) => Right (\x => g (\_ => Left (x, y)), z)) (y, z)
fregePeirce : Peirce (Frege p q r) Void -> Frege p q r
fregePeirce f g h i =
f (\j, _, _, _ => h $ i $ \x => void $ j $ \_, _, _ => g x) g h i
transpositionPeirce : Peirce (Transposition p q) Void -> Transposition p q
transpositionPeirce f g x =
f (\h, _, _ => void $ g (\y => h $ \_, _ => y) x) (\j, _ => g j x) x
-- There are a variety of single axioms sufficient for deriving all of
-- classical logic. The earliest of these is known as Nicod's axiom,
-- but it is written using only nand operators and doesn't lend itself
-- to Idris's type system. Meredith's axiom, on the other hand, is
-- written using implication and negation.
||| Meredith's axiom, sufficient for deriving all of classical logic
Meredith : (p, q, r, s, t : Type) -> Type
Meredith p q r s t =
((((p -> q) -> Not r -> Not s) -> r) -> t) -> (t -> p) -> s -> p
-- The Meredith axiom implies all of classical logic, and so in
-- particular it implies PEM, and therefore cannot be proved in
-- intuitionistic logic. As usual, however, its double negation can be
-- proved.
meredithDN : DN $ Meredith p q r s t
meredithDN f =
f $ \g, h, x =>
h $ g $ \i =>
void $ i
(\y => void $ f $ \_, _, _ => y)
(\z => f $ \_, _, _ => h $ g $ \_ => z)
x
-- Meredith can be proved assuming PEM, since the type system itself
-- takes care of the rest.
meredithPEM : PEM p -> Meredith p q r s t
meredithPEM (Left l) _ _ _ = l
meredithPEM (Right r) f g x =
g $ f $ \h =>
void $ h
(\y => void $ r y)
(\z => r $ g $ f (\_ => z))
x

58
libs/contrib/Data/Nat/Ack.idr Normal file
View File

@ -0,0 +1,58 @@
||| Properties of Ackermann functions
module Data.Nat.Ack
%default total
-- Primitive recursive functions are functions that can be calculated
-- by programs that don't use unbounded loops. Almost all common
-- mathematical functions are primitive recursive.
-- Uncomputable functions are functions that can't be calculated by
-- any programs at all. One example is the Busy Beaver function:
-- BB(k) = the maximum number of steps that can be executed by a
-- halting Turing machine with k states.
-- The values of the Busy Beaver function are unimaginably large for
-- any but the smallest inputs.
-- The Ackermann function is the most well-known example of a total
-- computable function that is not primitive recursive, i.e. a general
-- recursive function. It grows strictly faster than any primitive
-- recursive function, but also strictly slower than a function like
-- the Busy Beaver.
-- There are many variations of the Ackermann function. Here is one
-- common definition
-- (see https://sites.google.com/site/pointlesslargenumberstuff/home/2/ackermann)
-- that uses nested recursion:
ackRec : Nat -> Nat -> Nat
-- Base rule
ackRec Z m = S m
-- Prime rule
ackRec (S k) Z = ackRec k 1
-- Catastrophic rule
ackRec (S k) (S j) = ackRec k $ ackRec (S k) j
-- The so-called "base rule" and "prime rule" work together to ensure
-- termination. Happily, the Idris totality checker has no issues.
-- An unusual "repeating" defintion of the function is given in the
-- book The Little Typer:
ackRep : Nat -> Nat -> Nat
ackRep Z = (+) 1
ackRep (S k) = repeat (ackRep k)
where
repeat : (Nat -> Nat) -> Nat -> Nat
repeat f Z = f 1
repeat f (S k) = f (repeat f k)
-- These two definitions don't look like they define the same
-- function, but they do:
ackRepRec : (n, m : Nat) -> ackRep n m = ackRec n m
ackRepRec Z _ = Refl
ackRepRec (S k) Z = ackRepRec k 1
ackRepRec (S k) (S j) =
rewrite sym $ ackRepRec (S k) j in
ackRepRec k $ ackRep (S k) j

56
libs/contrib/Data/Nat/Fact.idr Normal file
View File

@ -0,0 +1,56 @@
||| Properties of factorial functions
module Data.Nat.Fact
import Data.Nat
%default total
||| Recursive definition of factorial.
factRec : Nat -> Nat
factRec Z = 1
factRec (S k) = (S k) * factRec k
||| Tail-recursive accumulator for factItr.
factAcc : Nat -> Nat -> Nat
factAcc Z acc = acc
factAcc (S k) acc = factAcc k $ (S k) * acc
||| Iterative definition of factorial.
factItr : Nat -> Nat
factItr n = factAcc n 1
----------------------------------------
||| Multiplicand-shuffling lemma.
multShuffle : (a, b, c : Nat) -> a * (b * c) = b * (a * c)
multShuffle a b c =
rewrite multAssociative a b c in
rewrite multCommutative a b in
sym $ multAssociative b a c
||| Multiplication of the accumulator.
factAccMult : (a, b, c : Nat) ->
a * factAcc b c = factAcc b (a * c)
factAccMult _ Z _ = Refl
factAccMult a (S k) c =
rewrite factAccMult a k (S k * c) in
rewrite multShuffle a (S k) c in
Refl
||| Addition of accumulators.
factAccPlus : (a, b, c : Nat) ->
factAcc a b + factAcc a c = factAcc a (b + c)
factAccPlus Z _ _ = Refl
factAccPlus (S k) b c =
rewrite factAccPlus k (S k * b) (S k * c) in
rewrite sym $ multDistributesOverPlusRight (S k) b c in
Refl
||| The recursive and iterative definitions are the equivalent.
factRecItr : (n : Nat) -> factRec n = factItr n
factRecItr Z = Refl
factRecItr (S k) =
rewrite factRecItr k in
rewrite factAccMult k k 1 in
rewrite multOneRightNeutral k in
factAccPlus k 1 k

50
libs/contrib/Data/Nat/Fib.idr Normal file
View File

@ -0,0 +1,50 @@
||| Properties of Fibonacci functions
module Data.Nat.Fib
import Data.Nat
%default total
||| Recursive definition of Fibonacci.
fibRec : Nat -> Nat
fibRec Z = Z
fibRec (S Z) = S Z
fibRec (S (S k)) = fibRec (S k) + fibRec k
||| Accumulator for fibItr.
fibAcc : Nat -> Nat -> Nat -> Nat
fibAcc Z a _ = a
fibAcc (S k) a b = fibAcc k b (a + b)
||| Iterative definition of Fibonacci.
fibItr : Nat -> Nat
fibItr n = fibAcc n 0 1
||| Addend shuffling lemma.
plusLemma : (a, b, c, d : Nat) -> (a + b) + (c + d) = (a + c) + (b + d)
plusLemma a b c d =
rewrite sym $ plusAssociative a b (c + d) in
rewrite plusAssociative b c d in
rewrite plusCommutative b c in
rewrite sym $ plusAssociative c b d in
plusAssociative a c (b + d)
||| Helper lemma for fibacc.
fibAdd : (n, a, b, c, d : Nat) ->
fibAcc n a b + fibAcc n c d = fibAcc n (a + c) (b + d)
fibAdd Z _ _ _ _ = Refl
fibAdd (S Z) _ _ _ _ = Refl
fibAdd (S (S k)) a b c d =
rewrite fibAdd k (a + b) (b + (a + b)) (c + d) (d + (c + d)) in
rewrite plusLemma b (a + b) d (c + d) in
rewrite plusLemma a b c d in
Refl
||| Iterative and recursive Fibonacci definitions are equivalent.
fibEq : (n : Nat) -> fibRec n = fibItr n
fibEq Z = Refl
fibEq (S Z) = Refl
fibEq (S (S k)) =
rewrite fibEq k in
rewrite fibEq (S k) in
fibAdd k 1 1 0 1

4
libs/contrib/Data/SortedMap.idr
View File

@ -215,6 +215,10 @@ insert k v (M _ t) =
Left t' => (M _ t')
Right t' => (M _ t')
export
singleton : Ord k => k -> v -> SortedMap k v
singleton k v = insert k v empty
export
insertFrom : Foldable f => f (k, v) -> SortedMap k v -> SortedMap k v
insertFrom = flip $ foldl $ flip $ uncurry insert

44
libs/contrib/Debug/Buffer.idr Normal file
View File

@ -0,0 +1,44 @@
module Debug.Buffer
import Data.Buffer
import Data.List
import Data.String.Extra
toHex : Int -> Int -> String
toHex d n = pack $ reverse $ foldl toHexDigit [] (slice d n [])
where
toHexDigit : List Char ->Int -> List Char
toHexDigit acc i = chr (if i < 10 then i + ord '0' else (i-10) + ord 'A')::acc
slice : Int -> Int -> List Int -> List Int
slice 0 _ acc = acc
slice d n acc = slice (d-1) (n `div` 16) ((n `mod` 16)::acc)
showSep : String -> Nat -> List String -> String
showSep sep _ [] = ""
showSep sep n [x] = x ++ replicate (3*n) ' '
showSep sep Z (x :: xs) = x ++ sep ++ showSep sep Z xs
showSep sep (S n) (x :: xs) = x ++ sep ++ showSep sep n xs
renderRow : List Int -> String
renderRow dat = showSep " " 16 (map (toHex 2) dat) ++
" " ++ pack (map (\i => if i > 0x1f && i < 0x80 then chr i else '.') dat)
group : Nat -> List a -> List (List a)
group n xs = worker [] xs
where
worker : List (List a) -> List a -> List (List a)
worker acc [] = reverse acc
worker acc ys = worker ((take n ys)::acc) (drop n ys)
export
dumpBuffer : Buffer -> IO String
dumpBuffer buf = do
size <- rawSize buf
dat <- bufferData buf
let rows = group 16 dat
let hex = showSep "\n" 0 (map renderRow rows)
pure $ hex ++ "\n\ntotal size = " ++ show size
export
printBuffer : Buffer -> IO ()
printBuffer buf = putStrLn $ !(dumpBuffer buf)

2
libs/contrib/Text/Lexer.idr
View File

@ -1,6 +1,6 @@
module Text.Lexer
import Data.Bool.Extra
import Data.Bool
import Data.List
import Data.Nat

12
libs/contrib/Text/Lexer/Core.idr
View File

@ -1,7 +1,7 @@
module Text.Lexer.Core
import public Control.Delayed
import Data.Bool.Extra
import Data.Bool
import Data.List
import Data.Nat
import Data.Strings
@ -76,10 +76,10 @@ reject = Lookahead False
||| of a list. The resulting recogniser will consume input if the produced
||| recognisers consume and the list is non-empty.
export
concatMap : (a -> Recognise c) -> (xs : List a) ->
concatMap : (a -> Recognise c) -> (xs : List a) ->
Recognise (c && (isCons xs))
concatMap {c} _ [] = rewrite andFalseFalse c in Empty
concatMap {c} f (x :: xs)
concatMap {c} f (x :: xs)
= rewrite andTrueNeutral c in
rewrite sym (orSameAndRightNeutral c (isCons xs)) in
SeqEmpty (f x) (Core.concatMap f xs)
@ -111,7 +111,7 @@ isJust (Just x) = True
export
unpack' : String -> List Char
unpack' str
unpack' str
= case strUncons str of
Nothing => []
Just (x, xs) => x :: unpack' xs
@ -182,12 +182,12 @@ tokenise pred line col acc tmap str
(incol, []) => c + cast (length incol)
(incol, _) => cast (length incol)
getFirstToken : TokenMap a -> List Char ->
getFirstToken : TokenMap a -> List Char ->
Maybe (TokenData a, Int, Int, List Char)
getFirstToken [] str = Nothing
getFirstToken ((lex, fn) :: ts) str
= case scan lex [] str of
Just (tok, rest) => Just (MkToken line col (fn (pack (reverse tok))),
Just (tok, rest) => Just (MkToken line col (fn (pack (reverse tok))),
line + cast (countNLs tok),
getCols tok col, rest)
Nothing => getFirstToken ts str

2
libs/contrib/Text/Parser.idr
View File

@ -1,6 +1,6 @@
module Text.Parser
import Data.Bool.Extra
import Data.Bool
import Data.List
import Data.Nat

10
libs/contrib/contrib.ipkg
View File

@ -10,14 +10,22 @@ modules = Control.Delayed,
Data.List.Views.Extra,
Data.List.Palindrome,
Data.Bool.Extra,
Data.Fin.Extra,
Data.Logic.Propositional,
Data.Nat.Ack,
Data.Nat.Equational,
Data.Nat.Fact,
Data.Nat.Factor,
Data.Nat.Fib,
Data.SortedMap,
Data.SortedSet,
Data.String.Extra,
Debug.Buffer,
Language.JSON,
Language.JSON.Data,
Language.JSON.Lexer,

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

@ -75,7 +75,7 @@ schHeader chez libs
"(case (machine-type)\n" ++
" [(i3le ti3le a6le ta6le) (load-shared-object \"libc.so.6\")]\n" ++
" [(i3osx ti3osx a6osx ta6osx) (load-shared-object \"libc.dylib\")]\n" ++
" [(i3nt ti3nt a6nt ta6nt) (load-shared-object \"msvcrt.dll\")" ++
" [(i3nt ti3nt a6nt ta6nt) (load-shared-object \"msvcrt.dll\")" ++
" (load-shared-object \"ws2_32.dll\")]\n" ++
" [else (load-shared-object \"libc.so\")])\n\n" ++
showSep "\n" (map (\x => "(load-shared-object \"" ++ escapeString x ++ "\")") libs) ++ "\n\n" ++
@ -341,7 +341,16 @@ startChez : String -> String -> String
startChez appdir target = unlines
[ "#!/bin/sh"
, ""
, "DIR=\"`realpath $0`\""
, "case `uname -s` in "
, " OpenBSD|FreeBSD|NetBSD) "
, " DIR=\"`grealpath $0`\""
, " ;; "
, " "
, " *) "
, " DIR=\"`realpath $0`\" "
, " ;; "
, "esac "
, ""
, "export LD_LIBRARY_PATH=\"$LD_LIBRARY_PATH:`dirname \"$DIR\"`/\"" ++ appdir ++ "\"\""
, "\"`dirname \"$DIR\"`\"/\"" ++ target ++ "\" \"$@\""
]
@ -357,7 +366,17 @@ startChezCmd chez appdir target = unlines
startChezWinSh : String -> String -> String -> String
startChezWinSh chez appdir target = unlines
[ "#!/bin/sh"
, "DIR=\"`realpath \"$0\"`\""
, ""
, "case `uname -s` in "
, " OpenBSD|FreeBSD|NetBSD) "
, " DIR=\"`grealpath $0`\""
, " ;; "
, " "
, " *) "
, " DIR=\"`realpath $0`\" "
, " ;; "
, "esac "
, ""
, "CHEZ=$(cygpath \"" ++ chez ++"\")"
, "export PATH=\"`dirname \"$DIR\"`/\"" ++ appdir ++ "\":$PATH\""
, "$CHEZ --script \"$(dirname \"$DIR\")/" ++ target ++ "\" \"$@\""
@ -440,7 +459,7 @@ compileExpr makeitso c execDir tm outfile
logTime "Make SO" $ when makeitso $ compileToSO chez appDirGen outSsAbs
let outShRel = execDir </> outfile
if isWindows
then makeShWindows chez outShRel appDirRel (if makeitso then outSoFile else outSsFile)
then makeShWindows chez outShRel appDirRel (if makeitso then outSoFile else outSsFile)
else makeSh outShRel appDirRel (if makeitso then outSoFile else outSsFile)
coreLift $ chmodRaw outShRel 0o755
pure (Just outShRel)

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

@ -56,14 +56,8 @@ showRacketChar : Char -> String -> String
showRacketChar '\\' = ("\\\\" ++)
showRacketChar c
= if c < chr 32 || c > chr 126
then (("\\u" ++ pad (asHex (cast c))) ++)
then (("\\u" ++ leftPad '0' 4 (asHex (cast c))) ++)
else strCons c
where
pad : String -> String
pad str
= case isLTE (length str) 4 of
Yes _ => pack (List.replicate (minus 4 (length str)) '0') ++ str
No _ => str
showRacketString : List Char -> String -> String
showRacketString [] = id
@ -320,7 +314,16 @@ startRacket : String -> String -> String -> String
startRacket racket appdir target = unlines
[ "#!/bin/sh"
, ""
, "DIR=\"`realpath $0`\""
, "case `uname -s` in "
, " OpenBSD|FreeBSD|NetBSD) "
, " DIR=\"`grealpath $0`\""
, " ;; "
, " "
, " *) "
, " DIR=\"`realpath $0`\" "
, " ;; "
, "esac "
, ""
, "export LD_LIBRARY_PATH=\"$LD_LIBRARY_PATH:`dirname \"$DIR\"`/\"" ++ appdir ++ "\"\""
, racket ++ "\"`dirname \"$DIR\"`\"/\"" ++ target ++ "\" \"$@\""
]
@ -336,7 +339,17 @@ startRacketCmd racket appdir target = unlines
startRacketWinSh : String -> String -> String -> String
startRacketWinSh racket appdir target = unlines
[ "#!/bin/sh"
, "DIR=\"`realpath \"$0\"`\""
, ""
, "case `uname -s` in "
, " OpenBSD|FreeBSD|NetBSD) "
, " DIR=\"`grealpath $0`\""
, " ;; "
, " "
, " *) "
, " DIR=\"`realpath $0`\" "
, " ;; "
, "esac "
, ""
, "export PATH=\"`dirname \"$DIR\"`/\"" ++ appdir ++ "\":$PATH\""
, racket ++ "\"" ++ target ++ "\" \"$@\""
]
@ -390,7 +403,7 @@ compileExpr mkexec c execDir tm outfile
coreLift $ mkdirAll appDirGen
Just cwd <- coreLift currentDir
| Nothing => throw (InternalError "Can't get current directory")
let ext = if isWindows then ".exe" else ""
let outRktFile = appDirRel </> outfile <.> "rkt"
let outBinFile = appDirRel </> outfile <.> ext
@ -430,4 +443,3 @@ executeExpr c execDir tm
export
codegenRacket : Codegen
codegenRacket = MkCG (compileExpr True) executeExpr

2
src/Core/Binary.idr
View File

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

2
src/Core/Context.idr
View File

@ -1619,7 +1619,7 @@ addDirective : {auto c : Ref Ctxt Defs} ->
String -> String -> Core ()
addDirective c str
= do defs <- get Ctxt
case getCG c of
case getCG (options defs) c of
Nothing => -- warn, rather than fail, because the CG may exist
-- but be unknown to this particular instance
coreLift $ putStrLn $ "Unknown code generator " ++ c

36
src/Core/Options.idr
View File

@ -42,6 +42,7 @@ data CG = Chez
| Racket
| Gambit
| Node
| Other String
export
Eq CG where
@ -49,6 +50,7 @@ Eq CG where
Racket == Racket = True
Gambit == Gambit = True
Node == Node = True
Other s == Other t = s == t
_ == _ = False
export
@ -57,20 +59,8 @@ Show CG where
show Racket = "racket"
show Gambit = "gambit"
show Node = "node"
show (Other s) = s
export
availableCGs : List (String, CG)
availableCGs
= [("chez", Chez),
("racket", Racket),
("gambit", Gambit),
("node", Node)]
export
getCG : String -> Maybe CG
getCG cg = lookup (toLower cg) availableCGs
-- Name options, to be saved in TTC
public export
record PairNames where
constructor MkPairNs
@ -146,6 +136,20 @@ record Options where
rewritenames : Maybe RewriteNames
primnames : PrimNames
extensions : List LangExt
additionalCGs : List (String, CG)
export
availableCGs : Options -> List (String, CG)
availableCGs o
= [("chez", Chez),
("racket", Racket),
("node", Node),
("gambit", Gambit)] ++ additionalCGs o
export
getCG : Options -> String -> Maybe CG
getCG o cg = lookup (toLower cg) (availableCGs o)
defaultDirs : Dirs
defaultDirs = MkDirs "." Nothing "build"
@ -168,7 +172,7 @@ export
defaults : Options
defaults = MkOptions defaultDirs defaultPPrint defaultSession
defaultElab Nothing Nothing
(MkPrimNs Nothing Nothing Nothing)
(MkPrimNs Nothing Nothing Nothing) []
[]
-- Reset the options which are set by source files
@ -208,3 +212,7 @@ setExtension e = record { extensions $= (e ::) }
export
isExtension : LangExt -> Options -> Bool
isExtension e opts = e `elem` extensions opts
export
addCG : (String, CG) -> Options -> Options
addCG cg = record { additionalCGs $= (cg::) }

7
src/Core/TTC.idr
View File

@ -733,14 +733,17 @@ TTC CG where
toBuf b Chez = tag 0
toBuf b Racket = tag 2
toBuf b Gambit = tag 3
toBuf b Node = tag 4
toBuf b (Other s) = do tag 4; toBuf b s
toBuf b Node = tag 5
fromBuf b
= case !getTag of
0 => pure Chez
2 => pure Racket
3 => pure Gambit
4 => pure Node
4 => do s <- fromBuf b
pure (Other s)
5 => pure Node
_ => corrupt "CG"
export

105
src/Idris/CommandLine.idr
View File

@ -93,6 +93,24 @@ data CLOpt
DebugElabCheck |
BlodwenPaths
||| Extract the host and port to bind the IDE socket to
export
ideSocketModeAddress : List CLOpt -> (String, Int)
ideSocketModeAddress [] = ("localhost", 38398)
ideSocketModeAddress (IdeModeSocket hp :: _) =
let (h, p) = Strings.break (== ':') hp
port = fromMaybe 38398 (portPart p >>= parsePositive)
host = if h == "" then "localhost" else h
in (host, port)
where
portPart : String -> Maybe String
portPart p = if p == ""
then Nothing
else Just $ assert_total $ prim__strTail p
ideSocketModeAddress (_ :: rest) = ideSocketModeAddress rest
formatSocketAddress : (String, Int) -> String
formatSocketAddress (host, port) = host ++ ":" ++ show port
ActType : List String -> Type
ActType [] = List CLOpt
@ -119,48 +137,54 @@ options = [MkOpt ["--check", "-c"] [] [CheckOnly]
MkOpt ["--package", "-p"] ["package"] (\f => [PkgPath f])
(Just "Add a package as a dependency"),
MkOpt ["--ide-mode"] [] [IdeMode]
(Just "Run the REPL with machine-readable syntax"),
MkOpt ["--ide-mode-socket"] [] [IdeModeSocket "localhost:38398"]
(Just "Run the ide socket mode on default host and port (localhost:38398)"),
MkOpt ["--ide-mode-socket-with"] ["host:port"] (\hp => [IdeModeSocket hp])
(Just "Run the ide socket mode on given host and port"),
MkOpt [] [] [] Nothing,
MkOpt ["--prefix"] [] [ShowPrefix]
(Just "Show installation prefix"),
MkOpt ["--paths"] [] [BlodwenPaths]
(Just "Show paths"),
MkOpt ["--libdir"] [] [Directory LibDir]
(Just "Show library directory"),
MkOpt [] [] [] Nothing,
MkOpt ["--build"] ["package file"] (\f => [Package Build f])
(Just "Build modules/executable for the given package"),
MkOpt ["--install"] ["package file"] (\f => [Package Install f])
(Just "Install the given package"),
MkOpt ["--clean"] ["package file"] (\f => [Package Clean f])
(Just "Clean intermediate files/executables for the given package"),
MkOpt ["--repl"] ["package file"] (\f => [Package REPL f])
(Just "Build the given package and launch a REPL instance."),
MkOpt ["--find-ipkg"] [] [FindIPKG]
(Just "Find and use an .ipkg file in a parent directory"),
MkOpt ["--libdir"] [] [Directory LibDir]
(Just "Show library directory"),
MkOpt [] [] [] Nothing,
MkOpt ["--ide-mode"] [] [IdeMode]
(Just "Run the REPL with machine-readable syntax"),
MkOpt ["--ide-mode-socket"] [] [IdeModeSocket $ formatSocketAddress (ideSocketModeAddress [])]
(Just $ "Run the ide socket mode on default host and port (" ++ formatSocketAddress (ideSocketModeAddress []) ++ ")"),
MkOpt ["--ide-mode-socket-with"] ["host:port"] (\hp => [IdeModeSocket hp])
(Just "Run the ide socket mode on given host and port"),
MkOpt [] [] [] Nothing,
MkOpt ["--client"] ["REPL command"] (\f => [RunREPL f])
(Just "Run a REPL command then quit immediately"),
MkOpt ["--timing"] [] [Timing]
(Just "Display timing logs"),
MkOpt [] [] [] Nothing,
MkOpt ["--no-banner"] [] [NoBanner]
(Just "Suppress the banner"),
MkOpt ["--quiet", "-q"] [] [Quiet]
(Just "Quiet mode; display fewer messages"),
MkOpt ["--verbose"] [] [Verbose]
(Just "Verbose mode (default)"),
MkOpt [] [] [] Nothing,
MkOpt ["--version", "-v"] [] [Version]
(Just "Display version string"),
MkOpt ["--help", "-h", "-?"] [] [Help]
(Just "Display help text"),
MkOpt ["--timing"] [] [Timing]
(Just "Display timing logs"),
MkOpt ["--find-ipkg"] [] [FindIPKG]
(Just "Find and use an .ipkg file in a parent directory"),
MkOpt ["--client"] ["REPL command"] (\f => [RunREPL f])
(Just "Run a REPL command then quit immediately"),
-- Internal debugging options
MkOpt ["--yaffle", "--ttimp"] ["ttimp file"] (\f => [Yaffle f])
Nothing, -- run ttimp REPL rather than full Idris
@ -178,21 +202,30 @@ options = [MkOpt ["--check", "-c"] [] [CheckOnly]
Nothing -- do more elaborator checks (currently conversion in LinearCheck)
]
optUsage : OptDesc -> String
optUsage d
= maybe "" -- Don't show anything if there's no help string (that means
-- it's an internal option)
(\h => " " ++
let optshow = showSep "," (flags d) ++ " " ++
showSep " " (map (\x => "<" ++ x ++ ">") (argdescs d)) in
optshow ++ pack (List.replicate (minus 26 (length optshow)) ' ')
++ h ++ "\n") (help d)
optsUsage : (options : List OptDesc) -> String
optsUsage options = let optsShow = map optShow options
maxOpt = foldr (\(opt, _), acc => max acc (length opt)) 0 optsShow in
concatMap (optUsage maxOpt) optsShow
where
showSep : String -> List String -> String
showSep sep [] = ""
showSep sep [x] = x
showSep sep (x :: xs) = x ++ sep ++ showSep sep xs
optShow : OptDesc -> (String, Maybe String)
optShow (MkOpt [] _ _ _) = ("", Just "")
optShow (MkOpt flags argdescs action help) = (showSep ", " flags ++ " " ++
showSep " " (map (\x => "<" ++ x ++ ">") argdescs),
help)
optUsage : Nat -> (String, Maybe String) -> String
optUsage maxOpt (optshow, help) = maybe "" -- Don't show anything if there's no help string (that means
-- it's an internal option)
(\h => " " ++ optshow ++
pack (List.replicate (minus (maxOpt + 2) (length optshow)) ' ') ++
h ++ "\n")
help
export
versionMsg : String
versionMsg = "Idris 2, version " ++ showVersion True version
@ -202,7 +235,7 @@ usage : String
usage = versionMsg ++ "\n" ++
"Usage: idris2 [options] [input file]\n\n" ++
"Available options:\n" ++
concatMap optUsage options
optsUsage options
processArgs : String -> (args : List String) -> List String -> ActType args ->
Either String (List CLOpt, List String)
@ -247,19 +280,3 @@ getCmdOpts : IO (Either String (List CLOpt))
getCmdOpts = do (_ :: opts) <- getArgs
| _ => pure (Left "Invalid command line")
pure $ getOpts opts
portPart : String -> Maybe String
portPart p = if p == ""
then Nothing
else Just $ assert_total $ prim__strTail p
||| Extract the host and port to bind the IDE socket to
public export
ideSocketModeHostPort : List CLOpt -> (String, Int)
ideSocketModeHostPort [] = ("localhost", 38398)
ideSocketModeHostPort (IdeModeSocket hp :: _) =
let (h, p) = Strings.break (== ':') hp
port = fromMaybe 38398 (portPart p >>= parsePositive)
host = if h == "" then "localhost" else h
in (host, port)
ideSocketModeHostPort (_ :: rest) = ideSocketModeHostPort rest

240
src/Idris/Driver.idr Normal file
View File

@ -0,0 +1,240 @@
module Idris.Driver
import Compiler.Common
import Core.Core
import Core.InitPrimitives
import Core.Metadata
import Core.Unify
import Idris.CommandLine
import Idris.IDEMode.REPL
import Idris.ModTree
import Idris.Package
import Idris.ProcessIdr
import Idris.REPL
import Idris.SetOptions
import Idris.Syntax
import Idris.Version
import IdrisPaths
import Data.List
import Data.So
import Data.Strings
import System
import System.Directory
import System.File
import Utils.Path
import Yaffle.Main
%default covering
findInput : List CLOpt -> Maybe String
findInput [] = Nothing
findInput (InputFile f :: fs) = Just f
findInput (_ :: fs) = findInput fs
-- Add extra data from the "IDRIS2_x" environment variables
updateEnv : {auto c : Ref Ctxt Defs} ->
Core ()
updateEnv
= do defs <- get Ctxt
bprefix <- coreLift $ getEnv "IDRIS2_PREFIX"
the (Core ()) $ case bprefix of
Just p => setPrefix p
Nothing => setPrefix yprefix
bpath <- coreLift $ getEnv "IDRIS2_PATH"
the (Core ()) $ case bpath of
Just path => do traverse_ addExtraDir (map trim (split (==pathSeparator) path))
Nothing => pure ()
bdata <- coreLift $ getEnv "IDRIS2_DATA"
the (Core ()) $ case bdata of
Just path => do traverse_ addDataDir (map trim (split (==pathSeparator) path))
Nothing => pure ()
blibs <- coreLift $ getEnv "IDRIS2_LIBS"
the (Core ()) $ case blibs of
Just path => do traverse_ addLibDir (map trim (split (==pathSeparator) path))
Nothing => pure ()
cg <- coreLift $ getEnv "IDRIS2_CG"
the (Core ()) $ case cg of
Just e => case getCG (options defs) e of
Just cg => setCG cg
Nothing => throw (InternalError ("Unknown code generator " ++ show e))
Nothing => pure ()
-- IDRIS2_PATH goes first so that it overrides this if there's
-- any conflicts. In particular, that means that setting IDRIS2_PATH
-- for the tests means they test the local version not the installed
-- version
defs <- get Ctxt
addPkgDir "prelude"
addPkgDir "base"
addDataDir (dir_prefix (dirs (options defs)) </>
("idris2-" ++ showVersion False version) </> "support")
addLibDir (dir_prefix (dirs (options defs)) </>
("idris2-" ++ showVersion False version) </> "lib")
Just cwd <- coreLift $ currentDir
| Nothing => throw (InternalError "Can't get current directory")
addLibDir cwd
updateREPLOpts : {auto o : Ref ROpts REPLOpts} ->
Core ()
updateREPLOpts
= do opts <- get ROpts
ed <- coreLift $ getEnv "EDITOR"
the (Core ()) $ case ed of
Just e => put ROpts (record { editor = e } opts)
Nothing => pure ()
showInfo : {auto c : Ref Ctxt Defs}
-> {auto o : Ref ROpts REPLOpts}
-> List CLOpt
-> Core Bool
showInfo Nil = pure False
showInfo (BlodwenPaths :: _)
= do defs <- get Ctxt
iputStrLn (toString (dirs (options defs)))
pure True
showInfo (_::rest) = showInfo rest
tryYaffle : List CLOpt -> Core Bool
tryYaffle [] = pure False
tryYaffle (Yaffle f :: _) = do yaffleMain f []
pure True
tryYaffle (c :: cs) = tryYaffle cs
tryTTM : List CLOpt -> Core Bool
tryTTM [] = pure False
tryTTM (Metadata f :: _) = do dumpTTM f
pure True
tryTTM (c :: cs) = tryTTM cs
banner : String
banner = " ____ __ _ ___ \n" ++
" / _/___/ /____(_)____ |__ \\ \n" ++
" / // __ / ___/ / ___/ __/ / Version " ++ showVersion True version ++ "\n" ++
" _/ // /_/ / / / (__ ) / __/ https://www.idris-lang.org \n" ++
" /___/\\__,_/_/ /_/____/ /____/ Type :? for help \n" ++
"\n" ++
"Welcome to Idris 2. Enjoy yourself!"
checkVerbose : List CLOpt -> Bool
checkVerbose [] = False
checkVerbose (Verbose :: _) = True
checkVerbose (_ :: xs) = checkVerbose xs
stMain : List (String, Codegen) -> List CLOpt -> Core ()
stMain cgs opts
= do False <- tryYaffle opts
| True => pure ()
False <- tryTTM opts
| True => pure ()
defs <- initDefs
let updated = foldl (\o, (s, _) => addCG (s, Other s) o) (options defs) cgs
c <- newRef Ctxt (record { options = updated } defs)
s <- newRef Syn initSyntax
setCG {c} $ maybe Chez (Other . fst) (head' cgs)
addPrimitives
setWorkingDir "."
updateEnv
let ide = ideMode 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)
finish <- showInfo opts
if finish
then pure ()
else do
-- If there's a --build or --install, just do that then quit
done <- processPackageOpts opts
when (not done) $
do True <- preOptions opts
| False => pure ()
when (checkVerbose opts) $ -- override Quiet if implicitly set
setOutput (REPL False)
u <- newRef UST initUState
m <- newRef MD initMetadata
updateREPLOpts
session <- getSession
when (not $ nobanner session) $ do
iputStrLn banner
when (isCons cgs) $ iputStrLn ("With codegen for: " ++
fastAppend (map (\(s, _) => s ++ " ") cgs))
fname <- if findipkg session
then findIpkg fname
else pure fname
setMainFile fname
the (Core ()) $ case fname of
Nothing => logTime "Loading prelude" $
when (not $ noprelude session) $
readPrelude True
Just f => logTime "Loading main file" $
(loadMainFile f >>= displayErrors)
doRepl <- postOptions opts
if doRepl then
if ide || ideSocket then
if not ideSocket
then do
setOutput (IDEMode 0 stdin stdout)
replIDE {c} {u} {m}
else do
let (host, port) = ideSocketModeAddress opts
f <- coreLift $ initIDESocketFile host port
case f of
Left err => do
coreLift $ putStrLn err
coreLift $ exitWith (ExitFailure 1)
Right file => do
setOutput (IDEMode 0 file file)
replIDE {c} {u} {m}
else do
repl {c} {u} {m}
showTimeRecord
else
-- exit with an error code if there was an error, otherwise
-- just exit
do ropts <- get ROpts
showTimeRecord
case errorLine ropts of
Nothing => pure ()
Just _ => coreLift $ exitWith (ExitFailure 1)
-- Run any options (such as --version or --help) which imply printing a
-- message then exiting. Returns wheter the program should continue
quitOpts : List CLOpt -> IO Bool
quitOpts [] = pure True
quitOpts (Version :: _)
= do putStrLn versionMsg
pure False
quitOpts (Help :: _)
= do putStrLn usage
pure False
quitOpts (ShowPrefix :: _)
= do putStrLn yprefix
pure False
quitOpts (_ :: opts) = quitOpts opts
export
mainWithCodegens : List (String, Codegen) -> IO ()
mainWithCodegens cgs = do Right opts <- getCmdOpts
| Left err => do putStrLn err
putStrLn usage
continue <- quitOpts opts
if continue
then
coreRun (stMain cgs opts)
(\err : Error => do putStrLn ("Uncaught error: " ++ show err)
exitWith (ExitFailure 1))
(\res => pure ())
else pure ()

191
src/Idris/Error.idr
View File

@ -7,12 +7,17 @@ import Core.Env
import Core.Options
import Core.Value
import Idris.REPLOpts
import Idris.Resugar
import Idris.Syntax
import Parser.Source
import Data.List
import Data.List.Extra
import Data.Maybe
import Data.Stream
import Data.Strings
import System.File
%default covering
@ -35,64 +40,86 @@ pshowNoNorm env tm
itm <- resugar env tm
pure (show itm)
ploc : {auto o : Ref ROpts REPLOpts} ->
FC -> Core String
ploc EmptyFC = pure ""
ploc (MkFC _ s e) = do
let sr = integerToNat $ cast $ fst s
let sc = integerToNat $ cast $ snd s
let er = integerToNat $ cast $ fst e
let ec = integerToNat $ cast $ snd e
source <- lines <$> getCurrentElabSource
if sr == er
then pure $ show (sr + 1) ++ "\t" ++ fromMaybe "" (elemAt source sr)
++ "\n\t" ++ repeatChar sc ' ' ++ repeatChar (ec `minus` sc) '^' ++ "\n"
else pure $ addLineNumbers sr $ extractRange sr er source
where
extractRange : Nat -> Nat -> List a -> List a
extractRange s e xs = take ((e `minus` s) + 1) (drop s xs)
repeatChar : Nat -> Char -> String
repeatChar n c = pack $ take n (repeat c)
addLineNumbers : Nat -> List String -> String
addLineNumbers st xs = snd $ foldl (\(i, s), l => (S i, s ++ show (i + 1) ++ "\t" ++ l ++ "\n")) (st, "") xs
export
perror : {auto c : Ref Ctxt Defs} ->
{auto s : Ref Syn SyntaxInfo} ->
{auto o : Ref ROpts REPLOpts} ->
Error -> Core String
perror (Fatal err) = perror err
perror (CantConvert _ env l r)
= pure $ "Mismatch between:\n\t" ++ !(pshow env l) ++ "\nand\n\t" ++ !(pshow env r)
perror (CantSolveEq _ env l r)
perror (CantConvert fc env l r)
= pure $ "Mismatch between:\n\t" ++ !(pshow env l) ++ "\nand\n\t" ++ !(pshow env r) ++ "\nat:\n" ++ !(ploc fc)
perror (CantSolveEq fc env l r)
= pure $ "Can't solve constraint between:\n\t" ++ !(pshow env l) ++
"\nand\n\t" ++ !(pshow env r)
perror (PatternVariableUnifies _ env n tm)
"\nand\n\t" ++ !(pshow env r) ++ "\nat:\n" ++ !(ploc fc)
perror (PatternVariableUnifies fc env n tm)
= pure $ "Pattern variable " ++ showPVar n ++
" unifies with:\n\t" ++ !(pshow env tm)
" unifies with:\n\t" ++ !(pshow env tm) ++ "\nat:\n" ++ !(ploc fc)
where
showPVar : Name -> String
showPVar (PV n _) = showPVar n
showPVar n = show n
perror (CyclicMeta _ env n tm)
perror (CyclicMeta fc env n tm)
= pure $ "Cycle detected in solution of metavariable "
++ show !(prettyName n) ++ " = "
++ !(pshow env tm)
++ !(pshow env tm) ++ " at:\n" ++ !(ploc fc)
perror (WhenUnifying _ env x y err)
= pure $ "When unifying " ++ !(pshow env x) ++ " and " ++ !(pshow env y) ++ "\n"
++ !(perror err)
perror (ValidCase _ env (Left tm))
= pure $ !(pshow env tm) ++ " is not a valid impossible case"
perror (ValidCase fc env (Left tm))
= pure $ !(pshow env tm) ++ " is not a valid impossible case at:\n" ++ !(ploc fc)
perror (ValidCase _ env (Right err))
= pure $ "Impossible pattern gives an error:\n" ++ !(perror err)
perror (UndefinedName _ x) = pure $ "Undefined name " ++ show x
perror (InvisibleName _ n (Just ns))
perror (UndefinedName fc x) = pure $ "Undefined name " ++ show x ++ " at:\n" ++ !(ploc fc)
perror (InvisibleName fc n (Just ns))
= pure $ "Name " ++ show n ++ " is inaccessible since " ++
showSep "." (reverse ns) ++ " is not explicitly imported"
perror (InvisibleName _ x Nothing)
= pure $ "Name " ++ show x ++ " is private"
showSep "." (reverse ns) ++ " is not explicitly imported at:\n" ++ !(ploc fc)
perror (InvisibleName fc x Nothing)
= pure $ "Name " ++ show x ++ " is private at:\n" ++ !(ploc fc)
perror (BadTypeConType fc n)
= pure $ "Return type of " ++ show n ++ " must be Type"
= pure $ "Return type of " ++ show n ++ " must be Type at:\n" ++ !(ploc fc)
perror (BadDataConType fc n fam)
= pure $ "Return type of " ++ show n ++ " must be in " ++ show fam
= pure $ "Return type of " ++ show n ++ " must be in " ++ show fam ++ " at:\n" ++ !(ploc fc)
perror (NotCovering fc n IsCovering)
= pure $ "Internal error (Coverage of " ++ show n ++ ")"
perror (NotCovering fc n (MissingCases cs))
= pure $ !(prettyName n) ++ " is not covering. Missing cases:\n\t" ++
= pure $ !(prettyName n) ++ " is not covering at:\n" ++ !(ploc fc) ++ "Missing cases:\n\t" ++
showSep "\n\t" !(traverse (pshow []) cs)
perror (NotCovering fc n (NonCoveringCall ns))
= pure $ !(prettyName n) ++ " is not covering:\n\t" ++
= pure $ !(prettyName n) ++ " is not covering at:\n" ++ !(ploc fc) ++ "\n\t" ++
"Calls non covering function"
++ case ns of
[fn] => " " ++ show fn
_ => "s: " ++ showSep ", " (map show ns)
perror (NotTotal fc n r)
= pure $ !(prettyName n) ++ " is not total:\n\t" ++ show r
= pure $ !(prettyName n) ++ " is not total:\n\t" ++ show r ++ "\nat:\n" ++ !(ploc fc)
perror (LinearUsed fc count n)
= pure $ "There are " ++ show count ++ " uses of linear name " ++ sugarName n
= pure $ "There are " ++ show count ++ " uses of linear name " ++ sugarName n ++ " at:\n" ++ !(ploc fc)
perror (LinearMisuse fc n exp ctx)
= pure $ if isErased exp
then show n ++ " is not accessible in this context"
else "Trying to use " ++ showRig exp ++ " name " ++ sugarName n ++
" in " ++ showRel ctx ++ " context"
= if isErased exp
then pure $ show n ++ " is not accessible in this context at:\n" ++ !(ploc fc)
else pure $ "Trying to use " ++ showRig exp ++ " name " ++ sugarName n ++
" in " ++ showRel ctx ++ " context at:\n" ++ !(ploc fc)
where
showRig : RigCount -> String
showRig = elimSemi "irrelevant"
@ -106,26 +133,27 @@ perror (LinearMisuse fc n exp ctx)
perror (BorrowPartial fc env tm arg)
= pure $ !(pshow env tm) ++
" borrows argument " ++ !(pshow env arg) ++
" so must be fully applied"
" so must be fully applied at:\n" ++ !(ploc fc)
perror (BorrowPartialType fc env tm)
= pure $ !(pshow env tm) ++
" borrows, so must return a concrete type"
perror (AmbiguousName fc ns) = pure $ "Ambiguous name " ++ show ns
" borrows, so must return a concrete type at:\n" ++ !(ploc fc)
perror (AmbiguousName fc ns) = pure $ "Ambiguous name " ++ show ns ++ " at:\n" ++ !(ploc fc)
perror (AmbiguousElab fc env ts)
= do pp <- getPPrint
setPPrint (record { fullNamespace = True } pp)
let res = "Ambiguous elaboration. Possible correct results:\n\t" ++
let res = "Ambiguous elaboration at:\n" ++ !(ploc fc) ++ "Possible correct results:\n\t" ++
showSep "\n\t" !(traverse (pshow env) ts)
setPPrint pp
pure res
perror (AmbiguousSearch fc env tgt ts)
= pure $ "Multiple solutions found in search of:\n\t"
++ !(pshowNoNorm env tgt)
++ "\nat:\n" ++ !(ploc fc)
++ "\nPossible correct results:\n\t" ++
showSep "\n\t" !(traverse (pshowNoNorm env) ts)
perror (AmbiguityTooDeep fc n ns)
= pure $ "Maximum ambiguity depth exceeded in " ++ show !(getFullName n)
++ ": " ++ showSep " --> " (map show !(traverse getFullName ns))
++ ": " ++ showSep " --> " (map show !(traverse getFullName ns)) ++ " at:\n" ++ !(ploc fc)
perror (AllFailed ts)
= case allUndefined ts of
Just e => perror e
@ -143,35 +171,35 @@ perror (AllFailed ts)
allUndefined [(_, UndefinedName loc e)] = Just (UndefinedName loc e)
allUndefined ((_, UndefinedName _ e) :: es) = allUndefined es
allUndefined _ = Nothing
perror (RecordTypeNeeded _ _)
= pure "Can't infer type for this record update"
perror (RecordTypeNeeded fc _)
= pure $ "Can't infer type for this record update at:\n" ++ !(ploc fc)
perror (NotRecordField fc fld Nothing)
= pure $ fld ++ " is not part of a record type"
= pure $ fld ++ " is not part of a record type at:\n" ++ !(ploc fc)
perror (NotRecordField fc fld (Just ty))
= pure $ "Record type " ++ show ty ++ " has no field " ++ fld
= pure $ "Record type " ++ show ty ++ " has no field " ++ fld ++ " at:\n" ++ !(ploc fc)
perror (NotRecordType fc ty)
= pure $ show ty ++ " is not a record type"
= pure $ show ty ++ " is not a record type at:\n" ++ !(ploc fc)
perror (IncompatibleFieldUpdate fc flds)
= pure $ "Field update " ++ showSep "->" flds ++
" not compatible with other updates"
perror (InvalidImplicits _ env [Just n] tm)
= pure $ show n ++ " is not a valid implicit argument in " ++ !(pshow env tm)
perror (InvalidImplicits _ env ns tm)
" not compatible with other updates at:\n" ++ !(ploc fc)
perror (InvalidImplicits fc env [Just n] tm)
= pure $ show n ++ " is not a valid implicit argument in " ++ !(pshow env tm) ++ " at:\n" ++ !(ploc fc)
perror (InvalidImplicits fc env ns tm)
= pure $ showSep ", " (map show ns) ++
" are not valid implicit arguments in " ++ !(pshow env tm)
perror (TryWithImplicits _ env imps)
" are not valid implicit arguments in " ++ !(pshow env tm) ++ " at:\n" ++ !(ploc fc)
perror (TryWithImplicits fc env imps)
= pure $ "Need to bind implicits "
++ showSep ", " !(traverse (tshow env) imps)
++ showSep ", " !(traverse (tshow env) imps) ++ " at:\n" ++ !(ploc fc)
where
tshow : {vars : _} ->
Env Term vars -> (Name, Term vars) -> Core String
tshow env (n, ty) = pure $ show n ++ " : " ++ !(pshow env ty)
perror (BadUnboundImplicit _ env n ty)
perror (BadUnboundImplicit fc env n ty)
= pure $ "Can't bind name " ++ nameRoot n ++ " with type " ++ !(pshow env ty)
++ " here. Try binding explicitly."
perror (CantSolveGoal _ env g)
++ " here at:\n" ++ !(ploc fc) ++ "Try binding explicitly."
perror (CantSolveGoal fc env g)
= let (_ ** (env', g')) = dropEnv env g in
pure $ "Can't find an implementation for " ++ !(pshow env' g')
pure $ "Can't find an implementation for " ++ !(pshow env' g') ++ " at:\n" ++ !(ploc fc)
where
-- For display, we don't want to see the full top level type; just the
-- return type
@ -182,9 +210,9 @@ perror (CantSolveGoal _ env g)
dropEnv env (Bind _ n b@(Let _ _ _) sc) = dropEnv (b :: env) sc
dropEnv env tm = (_ ** (env, tm))
perror (DeterminingArg _ n i env g)
perror (DeterminingArg fc n i env g)
= pure $ "Can't find an implementation for " ++ !(pshow env g) ++ "\n" ++
"since I can't infer a value for argument " ++ show n
"since I can't infer a value for argument " ++ show n ++ " at:\n" ++ !(ploc fc)
perror (UnsolvedHoles hs)
= pure $ "Unsolved holes:\n" ++ showHoles hs
where
@ -192,49 +220,49 @@ perror (UnsolvedHoles hs)
showHoles [] = ""
showHoles ((fc, n) :: hs) = show n ++ " introduced at " ++ show fc ++ "\n"
++ showHoles hs
perror (CantInferArgType _ env n h ty)
perror (CantInferArgType fc env n h ty)
= pure $ "Can't infer type for argument " ++ show n ++ "\n" ++
"Got " ++ !(pshow env ty) ++ " with hole " ++ show h
perror (SolvedNamedHole _ env h tm)
"Got " ++ !(pshow env ty) ++ " with hole " ++ show h ++ " at:\n" ++ !(ploc fc)
perror (SolvedNamedHole fc env h tm)
= pure $ "Named hole " ++ show h ++ " has been solved by unification\n"
++ "Result: " ++ !(pshow env tm)
++ "Result: " ++ !(pshow env tm) ++ " at:\n" ++ !(ploc fc)
perror (VisibilityError fc vx x vy y)
= pure $ show vx ++ " " ++ sugarName !(toFullNames x) ++
" cannot refer to " ++ show vy ++ " " ++ sugarName !(toFullNames y)
perror (NonLinearPattern _ n) = pure $ "Non linear pattern " ++ sugarName n
perror (BadPattern _ n) = pure $ "Pattern not allowed here: " ++ show n
perror (NoDeclaration _ n) = pure $ "No type declaration for " ++ show n
perror (AlreadyDefined _ n) = pure $ show n ++ " is already defined"
perror (NotFunctionType _ env tm)
= pure $ !(pshow env tm) ++ " is not a function type"
perror (RewriteNoChange _ env rule ty)
" cannot refer to " ++ show vy ++ " " ++ sugarName !(toFullNames y) ++ " at:\n" ++ !(ploc fc)
perror (NonLinearPattern fc n) = pure $ "Non linear pattern " ++ sugarName n ++ " at:\n" ++ !(ploc fc)
perror (BadPattern fc n) = pure $ "Pattern not allowed here: " ++ show n ++ " at:\n" ++ !(ploc fc)
perror (NoDeclaration fc n) = pure $ "No type declaration for " ++ show n ++ " at:\n" ++ !(ploc fc)
perror (AlreadyDefined fc n) = pure $ show n ++ " is already defined"
perror (NotFunctionType fc env tm)
= pure $ !(pshow env tm) ++ " is not a function type at:\n" ++ !(ploc fc)
perror (RewriteNoChange fc env rule ty)
= pure $ "Rewriting by " ++ !(pshow env rule) ++
" did not change type " ++ !(pshow env ty)
" did not change type " ++ !(pshow env ty) ++ " at:\n" ++ !(ploc fc)
perror (NotRewriteRule fc env rule)
= pure $ !(pshow env rule) ++ " is not a rewrite rule type"
perror (CaseCompile _ n DifferingArgNumbers)
= pure $ "Patterns for " ++ !(prettyName n) ++ " have differing numbers of arguments"
perror (CaseCompile _ n DifferingTypes)
= pure $ "Patterns for " ++ !(prettyName n) ++ " require matching on different types"
perror (CaseCompile _ n UnknownType)
= pure $ "Can't infer type to match in " ++ !(prettyName n)
= pure $ !(pshow env rule) ++ " is not a rewrite rule type at:\n" ++ !(ploc fc)
perror (CaseCompile fc n DifferingArgNumbers)
= pure $ "Patterns for " ++ !(prettyName n) ++ " have differing numbers of arguments at:\n" ++ !(ploc fc)
perror (CaseCompile fc n DifferingTypes)
= pure $ "Patterns for " ++ !(prettyName n) ++ " require matching on different types at:\n" ++ !(ploc fc)
perror (CaseCompile fc n UnknownType)
= pure $ "Can't infer type to match in " ++ !(prettyName n) ++ " at:\n" ++ !(ploc fc)
perror (CaseCompile fc n (NotFullyApplied cn))
= pure $ "Constructor " ++ show !(toFullNames cn) ++ " is not fully applied"
= pure $ "Constructor " ++ show !(toFullNames cn) ++ " is not fully applied at:\n" ++ !(ploc fc)
perror (CaseCompile fc n (MatchErased (_ ** (env, tm))))
= pure $ "Attempt to match on erased argument " ++ !(pshow env tm) ++
" in " ++ !(prettyName n)
perror (BadDotPattern _ env reason x y)
" in " ++ !(prettyName n) ++ " at\n:" ++ !(ploc fc)
perror (BadDotPattern fc env reason x y)
= pure $ "Can't match on " ++ !(pshow env x) ++
" (" ++ show reason ++ ")"
perror (MatchTooSpecific _ env tm)
" (" ++ show reason ++ ") at\n" ++ !(ploc fc)
perror (MatchTooSpecific fc env tm)
= pure $ "Can't match on " ++ !(pshow env tm) ++
" as it has a polymorphic type"
perror (BadImplicit _ str)
= pure $ "Can't infer type for unbound implicit name " ++ str ++ "\n" ++
"Try making it a bound implicit."
perror (BadRunElab _ env script)
= pure $ "Bad elaborator script " ++ !(pshow env script)
perror (GenericMsg _ str) = pure str
" as it has a polymorphic type at:\n" ++ !(ploc fc)
perror (BadImplicit fc str)
= pure $ "Can't infer type for unbound implicit name " ++ str ++ " at\n" ++
!(ploc fc) ++ "Try making it a bound implicit."
perror (BadRunElab fc env script)
= pure $ "Bad elaborator script " ++ !(pshow env script) ++ " at:\n" ++ !(ploc fc)
perror (GenericMsg fc str) = pure $ str ++ " at:\n" ++ !(ploc fc)
perror (TTCError msg) = pure $ "Error in TTC file: " ++ show msg
perror (FileErr fname err)
= pure $ "File error in " ++ fname ++ ": " ++ show err
@ -267,6 +295,7 @@ perror (InRHS fc n err)
export
pwarning : {auto c : Ref Ctxt Defs} ->
{auto s : Ref Syn SyntaxInfo} ->
{auto o : Ref ROpts REPLOpts} ->
Warning -> Core String
pwarning (UnreachableClause fc env tm)
= pure $ "Warning: unreachable clause: " ++ !(pshow env tm)
@ -274,6 +303,7 @@ pwarning (UnreachableClause fc env tm)
export
display : {auto c : Ref Ctxt Defs} ->
{auto s : Ref Syn SyntaxInfo} ->
{auto o : Ref ROpts REPLOpts} ->
Error -> Core String
display err
= pure $ maybe "" (\f => show f ++ ":") (getErrorLoc err) ++
@ -282,6 +312,7 @@ display err
export
displayWarning : {auto c : Ref Ctxt Defs} ->
{auto s : Ref Syn SyntaxInfo} ->
{auto o : Ref ROpts REPLOpts} ->
Warning -> Core String
displayWarning w
= pure $ maybe "" (\f => show f ++ ":") (getWarningLoc w) ++

16
src/Idris/IDEMode/Commands.idr
View File

@ -3,6 +3,7 @@ module Idris.IDEMode.Commands
import Core.Core
import Core.Name
import public Idris.REPLOpts
import Utils.Hex
import System.File
@ -253,21 +254,14 @@ export
version : Int -> Int -> SExp
version maj min = toSExp (SymbolAtom "protocol-version", maj, min)
%foreign "C:fprintf,libc 6"
prim__printfHex : AnyPtr -> String -> Int -> PrimIO ()
hex : File -> Int -> IO ()
hex (FHandle h) num
= primIO $ prim__printfHex h "%06x" num
sendLine : File -> String -> IO ()
sendLine f st =
sendStr : File -> String -> IO ()
sendStr f st =
map (const ()) (fPutStr f st)
export
send : SExpable a => File -> a -> Core ()
send f resp
= do let r = show (toSExp resp) ++ "\n"
coreLift $ hex f (cast (length r))
coreLift $ sendLine f r
coreLift $ sendStr f $ leftPad '0' 6 (asHex (cast (length r)))
coreLift $ sendStr f r
coreLift $ fflush f

2
src/Idris/IDEMode/Parser.idr
View File

@ -36,7 +36,7 @@ idelex str
-- Add the EndInput token so that we'll have a line and column
-- number to read when storing spans in the file
(tok, (l, c, "")) => Right (filter notComment tok ++
[MkToken l c EndInput])
[MkToken l c l c EndInput])
(_, fail) => Left fail
where
notComment : TokenData Token -> Bool

230
src/Idris/Main.idr
View File

@ -1,232 +1,6 @@
module Main
import Core.Core
import Core.InitPrimitives
import Core.Metadata
import Core.Unify
import Idris.CommandLine
import Idris.IDEMode.REPL
import Idris.ModTree
import Idris.Package
import Idris.ProcessIdr
import Idris.REPL
import Idris.SetOptions
import Idris.Syntax
import Idris.Version
import IdrisPaths
import Data.So
import Data.Strings
import System
import System.Directory
import System.File
import Utils.Path
import Yaffle.Main
%default covering
findInput : List CLOpt -> Maybe String
findInput [] = Nothing
findInput (InputFile f :: fs) = Just f
findInput (_ :: fs) = findInput fs
-- Add extra data from the "IDRIS2_x" environment variables
updateEnv : {auto c : Ref Ctxt Defs} ->
Core ()
updateEnv
= do bprefix <- coreLift $ getEnv "IDRIS2_PREFIX"
the (Core ()) $ case bprefix of
Just p => setPrefix p
Nothing => setPrefix yprefix
bpath <- coreLift $ getEnv "IDRIS2_PATH"
the (Core ()) $ case bpath of
Just path => do traverse_ addExtraDir (map trim (split (==pathSeparator) path))
Nothing => pure ()
bdata <- coreLift $ getEnv "IDRIS2_DATA"
the (Core ()) $ case bdata of
Just path => do traverse_ addDataDir (map trim (split (==pathSeparator) path))
Nothing => pure ()
blibs <- coreLift $ getEnv "IDRIS2_LIBS"
the (Core ()) $ case blibs of
Just path => do traverse_ addLibDir (map trim (split (==pathSeparator) path))
Nothing => pure ()
cg <- coreLift $ getEnv "IDRIS2_CG"
the (Core ()) $ case cg of
Just e => case getCG e of
Just cg => setCG cg
Nothing => throw (InternalError ("Unknown code generator " ++ show e))
Nothing => pure ()
-- IDRIS2_PATH goes first so that it overrides this if there's
-- any conflicts. In particular, that means that setting IDRIS2_PATH
-- for the tests means they test the local version not the installed
-- version
defs <- get Ctxt
addPkgDir "prelude"
addPkgDir "base"
addDataDir (dir_prefix (dirs (options defs)) </>
("idris2-" ++ showVersion False version) </> "support")
addLibDir (dir_prefix (dirs (options defs)) </>
("idris2-" ++ showVersion False version) </> "lib")
Just cwd <- coreLift $ currentDir
| Nothing => throw (InternalError "Can't get current directory")
addLibDir cwd
updateREPLOpts : {auto o : Ref ROpts REPLOpts} ->
Core ()
updateREPLOpts
= do opts <- get ROpts
ed <- coreLift $ getEnv "EDITOR"
the (Core ()) $ case ed of
Just e => put ROpts (record { editor = e } opts)
Nothing => pure ()
showInfo : {auto c : Ref Ctxt Defs}
-> {auto o : Ref ROpts REPLOpts}
-> List CLOpt
-> Core Bool
showInfo Nil = pure False
showInfo (BlodwenPaths :: _)
= do defs <- get Ctxt
iputStrLn (toString (dirs (options defs)))
pure True
showInfo (_::rest) = showInfo rest
tryYaffle : List CLOpt -> Core Bool
tryYaffle [] = pure False
tryYaffle (Yaffle f :: _) = do yaffleMain f []
pure True
tryYaffle (c :: cs) = tryYaffle cs
tryTTM : List CLOpt -> Core Bool
tryTTM [] = pure False
tryTTM (Metadata f :: _) = do dumpTTM f
pure True
tryTTM (c :: cs) = tryTTM cs
banner : String
banner = " ____ __ _ ___ \n" ++
" / _/___/ /____(_)____ |__ \\ \n" ++
" / // __ / ___/ / ___/ __/ / Version " ++ showVersion True version ++ "\n" ++
" _/ // /_/ / / / (__ ) / __/ https://www.idris-lang.org \n" ++
" /___/\\__,_/_/ /_/____/ /____/ Type :? for help \n" ++
"\n" ++
"Welcome to Idris 2. Enjoy yourself!"
checkVerbose : List CLOpt -> Bool
checkVerbose [] = False
checkVerbose (Verbose :: _) = True
checkVerbose (_ :: xs) = checkVerbose xs
stMain : List CLOpt -> Core ()
stMain opts
= do False <- tryYaffle opts
| True => pure ()
False <- tryTTM opts
| True => pure ()
defs <- initDefs
c <- newRef Ctxt defs
s <- newRef Syn initSyntax
addPrimitives
setWorkingDir "."
updateEnv
let ide = ideMode 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)
finish <- showInfo opts
if finish
then pure ()
else do
-- If there's a --build or --install, just do that then quit
done <- processPackageOpts opts
when (not done) $
do True <- preOptions opts
| False => pure ()
when (checkVerbose opts) $ -- override Quiet if implicitly set
setOutput (REPL False)
u <- newRef UST initUState
m <- newRef MD initMetadata
updateREPLOpts
session <- getSession
when (not $ nobanner session) $
iputStrLn banner
fname <- if findipkg session
then findIpkg fname
else pure fname
setMainFile fname
the (Core ()) $ case fname of
Nothing => logTime "Loading prelude" $
when (not $ noprelude session) $
readPrelude True
Just f => logTime "Loading main file" $
(loadMainFile f >>= displayErrors)
doRepl <- postOptions opts
if doRepl then
if ide || ideSocket then
if not ideSocket
then do
setOutput (IDEMode 0 stdin stdout)
replIDE {c} {u} {m}
else do
let (host, port) = ideSocketModeHostPort opts
f <- coreLift $ initIDESocketFile host port
case f of
Left err => do
coreLift $ putStrLn err
coreLift $ exitWith (ExitFailure 1)
Right file => do
setOutput (IDEMode 0 file file)
replIDE {c} {u} {m}
else do
repl {c} {u} {m}
showTimeRecord
else
-- exit with an error code if there was an error, otherwise
-- just exit
do ropts <- get ROpts
showTimeRecord
case errorLine ropts of
Nothing => pure ()
Just _ => coreLift $ exitWith (ExitFailure 1)
-- Run any options (such as --version or --help) which imply printing a
-- message then exiting. Returns wheter the program should continue
quitOpts : List CLOpt -> IO Bool
quitOpts [] = pure True
quitOpts (Version :: _)
= do putStrLn versionMsg
pure False
quitOpts (Help :: _)
= do putStrLn usage
pure False
quitOpts (ShowPrefix :: _)
= do putStrLn yprefix
pure False
quitOpts (_ :: opts) = quitOpts opts
import Idris.Driver
main : IO ()
main = do Right opts <- getCmdOpts
| Left err =>
do putStrLn err
putStrLn usage
continue <- quitOpts opts
if continue
then
coreRun (stMain opts)
(\err : Error =>
do putStrLn ("Uncaught error: " ++ show err)
exitWith (ExitFailure 1))
(\res => pure ())
else pure ()
main = mainWithCodegens []

178
src/Idris/Parser.idr
View File

@ -9,6 +9,7 @@ import TTImp.TTImp
import public Text.Parser
import Data.List
import Data.List.Views
import Data.Maybe
import Data.Strings
%default covering
@ -48,41 +49,32 @@ plhs = MkParseOpts False False
atom : FileName -> Rule PTerm
atom fname
= do start <- location
= do (start, end) <- position
exactIdent "Type"
end <- location
pure (PType (MkFC fname start end))
<|> do start <- location
<|> do (start, end) <- position
x <- name
end <- location
pure (PRef (MkFC fname start end) x)
<|> do start <- location
<|> do (start, end) <- position
x <- constant
end <- location
pure (PPrimVal (MkFC fname start end) x)
<|> do start <- location
<|> do (start, end) <- position
symbol "_"
end <- location
pure (PImplicit (MkFC fname start end))
<|> do start <- location
<|> do (start, end) <- position
symbol "?"
end <- location
pure (PInfer (MkFC fname start end))
<|> do start <- location
<|> do (start, end) <- position
x <- holeName
end <- location
pure (PHole (MkFC fname start end) False x)
<|> do start <- location
<|> do (start, end) <- position
pragma "MkWorld"
end <- location
pure (PPrimVal (MkFC fname start end) WorldVal)
<|> do start <- location
<|> do (start, end) <- position
pragma "World"
end <- location
pure (PPrimVal (MkFC fname start end) WorldType)
<|> do start <- location
<|> do (start, end) <- position
pragma "search"
end <- location
pure (PSearch (MkFC fname start end) 50)
whereBlock : FileName -> Int -> Rule (List PDecl)
@ -121,6 +113,11 @@ data ArgType
| ImpArg (Maybe Name) PTerm
| WithArg PTerm
argTerm : ArgType -> PTerm
argTerm (ExpArg t) = t
argTerm (ImpArg _ t) = t
argTerm (WithArg t) = t
mutual
appExpr : ParseOpts -> FileName -> IndentInfo -> Rule PTerm
appExpr q fname indents
@ -133,12 +130,12 @@ mutual
<|> do start <- location
f <- simpleExpr fname indents
args <- many (argExpr q fname indents)
end <- location
end <- pure $ endPos $ getPTermLoc $ fromMaybe f $ argTerm <$> last' args
pure (applyExpImp start end f args)
<|> do start <- location
op <- iOperator
arg <- expr pdef fname indents
end <- location
end <- pure $ endPos $ getPTermLoc arg
pure (PPrefixOp (MkFC fname start end) op arg)
<|> fail "Expected 'case', 'if', 'do', application or operator expression"
where
@ -166,7 +163,7 @@ mutual
<|> if withOK q
then do continue indents
symbol "|"
arg <- expr (record { withOK = False} q) fname indents
arg <- expr (record {withOK = False} q) fname indents
pure (WithArg arg)
else fail "| not allowed here"
@ -180,8 +177,8 @@ mutual
tm <- expr pdef fname indents
symbol "}"
pure (Just (UN x), tm))
<|> (do symbol "}"
end <- location
<|> (do end <- endLocation
symbol "}"
pure (Just (UN x), PRef (MkFC fname start end) (UN x)))
<|> do symbol "@{"
commit
@ -220,7 +217,7 @@ mutual
then do continue indents
symbol "="
r <- opExpr q fname indents
end <- location
end <- pure $ endPos $ getPTermLoc r
pure (POp (MkFC fname start end) (UN "=") l r)
else fail "= not allowed")
<|>
@ -228,7 +225,7 @@ mutual
op <- iOperator
middle <- location
r <- opExpr q fname indents
end <- location
end <- pure $ endPos $ getPTermLoc r
pure (POp (MkFC fname start end) op l r))
<|> pure l
@ -237,10 +234,10 @@ mutual
= do x <- unqualifiedName
symbol ":"
ty <- expr pdef fname indents
loc <- location
loc <- pure $ endPos $ getPTermLoc ty
symbol "**"
rest <- dpair fname loc indents <|> expr pdef fname indents
end <- location
end <- pure $ endPos $ getPTermLoc rest
pure (PDPair (MkFC fname start end)
(PRef (MkFC fname start loc) (UN x))
ty
@ -249,7 +246,7 @@ mutual
loc <- location
symbol "**"
rest <- dpair fname loc indents <|> expr pdef fname indents
end <- location
end <- pure $ endPos $ getPTermLoc rest
pure (PDPair (MkFC fname start end)
l
(PImplicit (MkFC fname start end))
@ -275,8 +272,8 @@ mutual
pure p
<|> do e <- expr pdef fname indents
(do op <- iOperator
end <- endLocation
symbol ")"
end <- location
pure (PSectionR (MkFC fname start end) e op)
<|>
-- all the other bracketed expressions
@ -289,14 +286,14 @@ mutual
listRange : FileName -> FilePos -> IndentInfo -> List PTerm -> Rule PTerm
listRange fname start indents xs
= do symbol "]"
end <- location
= do end <- endLocation
symbol "]"
let fc = MkFC fname start end
rstate <- getInitRange xs
pure (PRangeStream fc (fst rstate) (snd rstate))
<|> do y <- expr pdef fname indents
end <- endLocation
symbol "]"
end <- location
let fc = MkFC fname start end
rstate <- getInitRange xs
pure (PRange fc (fst rstate) (snd rstate) y)
@ -304,16 +301,17 @@ mutual
listExpr : FileName -> FilePos -> IndentInfo -> Rule PTerm
listExpr fname start indents
= do ret <- expr pnowith fname indents
let endRet = getPTermLoc ret
symbol "|"
conds <- sepBy1 (symbol ",") (doAct fname indents)
end <- pure $ endPos $ fromMaybe endRet (map getLoc $ join $ last' <$> last' conds)
symbol "]"
end <- location
pure (PComprehension (MkFC fname start end) ret (concat conds))
<|> do xs <- sepBy (symbol ",") (expr pdef fname indents)
(do symbol ".."
listRange fname start indents xs)
<|> (do symbol "]"
end <- location
<|> (do end <- endLocation
symbol "]"
pure (PList (MkFC fname start end) xs))
-- A pair, dependent pair, or just a single expression
@ -360,7 +358,7 @@ mutual
symbol "@"
commit
expr <- simpleExpr fname indents
end <- location
end <- pure $ endPos $ getPTermLoc expr
pure (PAs (MkFC fname start end) (UN x) expr)
<|> atom fname
<|> binder fname indents
@ -370,31 +368,31 @@ mutual
symbol ".("
commit
e <- expr pdef fname indents
end <- endLocation
symbol ")"
end <- location
pure (PDotted (MkFC fname start end) e)
<|> do start <- location
symbol "`("
e <- expr pdef fname indents
end <- endLocation
symbol ")"
end <- location
pure (PQuote (MkFC fname start end) e)
<|> do start <- location
symbol "`{{"
n <- name
end <- endLocation
symbol "}}"
end <- location
pure (PQuoteName (MkFC fname start end) n)
<|> do start <- location
symbol "`["
ns <- nonEmptyBlock (topDecl fname)
end <- endLocation
symbol "]"
end <- location
pure (PQuoteDecl (MkFC fname start end) (collectDefs (concat ns)))
<|> do start <- location
symbol "~"
e <- simpleExpr fname indents
end <- location
end <- pure $ endPos $ getPTermLoc e
pure (PUnquote (MkFC fname start end) e)
<|> do start <- location
symbol "("
@ -405,24 +403,24 @@ mutual
<|> do start <- location
symbol "!"
e <- simpleExpr fname indents
end <- location
end <- pure $ endPos $ getPTermLoc e
pure (PBang (MkFC fname start end) e)
<|> do start <- location
symbol "[|"
e <- expr pdef fname indents
end <- pure $ endPos $ getPTermLoc e
symbol "|]"
end <- location
pure (PIdiom (MkFC fname start end) e)
<|> do start <- location
pragma "runElab"
e <- expr pdef fname indents
end <- location
end <- pure $ endPos $ getPTermLoc e
pure (PRunElab (MkFC fname start end) e)
<|> do start <- location
pragma "logging"
lvl <- intLit
e <- expr pdef fname indents
end <- location
end <- pure $ endPos $ getPTermLoc e
pure (PUnifyLog (MkFC fname start end) (integerToNat lvl) e)
multiplicity : SourceEmptyRule (Maybe Integer)
@ -502,7 +500,7 @@ mutual
symbol ")"
exp <- bindSymbol
scope <- typeExpr pdef fname indents
end <- location
end <- pure $ endPos $ getPTermLoc scope
pure (pibindAll (MkFC fname start end) exp binders scope)
autoImplicitPi : FileName -> IndentInfo -> Rule PTerm
@ -515,7 +513,7 @@ mutual
symbol "}"
symbol "->"
scope <- typeExpr pdef fname indents
end <- location
end <- pure $ endPos $ getPTermLoc scope
pure (pibindAll (MkFC fname start end) AutoImplicit binders scope)
defaultImplicitPi : FileName -> IndentInfo -> Rule PTerm
@ -529,7 +527,7 @@ mutual
symbol "}"
symbol "->"
scope <- typeExpr pdef fname indents
end <- location
end <- pure $ endPos $ getPTermLoc scope
pure (pibindAll (MkFC fname start end) (DefImplicit t) binders scope)
forall_ : FileName -> IndentInfo -> Rule PTerm
@ -545,7 +543,7 @@ mutual
Just (UN n), PImplicit nfc)) ns
symbol "."
scope <- typeExpr pdef fname indents
end <- location
end <- pure $ endPos $ getPTermLoc scope
pure (pibindAll (MkFC fname start end) Implicit binders scope)
implicitPi : FileName -> IndentInfo -> Rule PTerm
@ -556,7 +554,7 @@ mutual
symbol "}"
symbol "->"
scope <- typeExpr pdef fname indents
end <- location
end <- pure $ endPos $ getPTermLoc scope
pure (pibindAll (MkFC fname start end) Implicit binders scope)
lam : FileName -> IndentInfo -> Rule PTerm
@ -567,7 +565,7 @@ mutual
symbol "=>"
mustContinue indents Nothing
scope <- expr pdef fname indents
end <- location
end <- pure $ endPos $ getPTermLoc scope
pure (bindAll (MkFC fname start end) binders scope)
where
bindAll : FC -> List (RigCount, PTerm, PTerm) -> PTerm -> PTerm
@ -581,7 +579,7 @@ mutual
= do start <- location
rigc <- multiplicity
pat <- expr plhs fname indents
tyend <- location
tyend <- pure $ endPos $ getPTermLoc pat
ty <- option (PImplicit (MkFC fname start tyend))
(do symbol ":"
typeExpr (pnoeq pdef) fname indents)
@ -589,6 +587,7 @@ mutual
val <- expr pnowith fname indents
alts <- block (patAlt fname)
end <- location
end <- pure $ fromMaybe end (endPos <$> getPClauseLoc <$> last' alts)
rig <- getMult rigc
pure (start, end, rig, pat, ty, val, alts)
@ -622,7 +621,7 @@ mutual
res <- nonEmptyBlock (letBinder fname)
commitKeyword indents "in"
scope <- typeExpr pdef fname indents
end <- location
end <- pure $ endPos $ getPTermLoc scope
pure (buildLets fname res scope)
<|> do start <- location
@ -631,7 +630,7 @@ mutual
ds <- nonEmptyBlock (topDecl fname)
commitKeyword indents "in"
scope <- typeExpr pdef fname indents
end <- location
end <- pure $ endPos $ getPTermLoc scope
pure (PLocal (MkFC fname start end) (collectDefs (concat ds)) scope)
case_ : FileName -> IndentInfo -> Rule PTerm
@ -642,16 +641,19 @@ mutual
commitKeyword indents "of"
alts <- block (caseAlt fname)
end <- location
end <- pure $ fromMaybe end (endPos <$> getPClauseLoc <$> last' alts)
pure (PCase (MkFC fname start end) scr alts)
lambdaCase : FileName -> IndentInfo -> Rule PTerm
lambdaCase fname indents
= do start <- location
symbol "\\" *> keyword "case"
endCase <- location
symbol "\\"
endCase <- endLocation
keyword "case"
commit
alts <- block (caseAlt fname)
end <- location
end <- pure $ fromMaybe end (endPos <$> getPClauseLoc <$> last' alts)
pure $
(let fc = MkFC fname start end
fcCase = MkFC fname start endCase
@ -670,12 +672,12 @@ mutual
= do symbol "=>"
mustContinue indents Nothing
rhs <- expr pdef fname indents
end <- pure $ endPos $ getPTermLoc rhs
atEnd indents
end <- location
pure (MkPatClause (MkFC fname start end) lhs rhs [])
<|> do keyword "impossible"
<|> do end <- endLocation
keyword "impossible"
atEnd indents
end <- location
pure (MkImpossible (MkFC fname start end) lhs)
if_ : FileName -> IndentInfo -> Rule PTerm
@ -698,8 +700,8 @@ mutual
symbol "{"
commit
fs <- sepBy1 (symbol ",") (field fname indents)
end <- endLocation
symbol "}"
end <- location
pure (PUpdate (MkFC fname start end) fs)
field : FileName -> IndentInfo -> Rule PFieldUpdate
@ -728,7 +730,7 @@ mutual
rule <- expr pdef fname indents
commitKeyword indents "in"
tm <- expr pdef fname indents
end <- location
end <- pure $ endPos $ getPTermLoc tm
pure (PRewrite (MkFC fname start end) rule tm)
doBlock : FileName -> IndentInfo -> Rule PTerm
@ -737,6 +739,7 @@ mutual
keyword "do"
actions <- block (doAct fname)
end <- location
end <- pure $ fromMaybe end $ map (endPos . getLoc) $ join $ last' <$> last' actions
pure (PDoBlock (MkFC fname start end) (concat actions))
lowerFirst : String -> Bool
@ -758,8 +761,8 @@ mutual
validPatternVar n
symbol "<-"
val <- expr pdef fname indents
end <- pure $ endPos $ getPTermLoc val
atEnd indents
end <- location
pure [DoBind (MkFC fname start end) n val]
<|> do keyword "let"
res <- block (letBinder fname)
@ -769,24 +772,26 @@ mutual
keyword "let"
res <- block (topDecl fname)
end <- location
end <- pure $ fromMaybe end $ map (endPos . getPDeclLoc) $ join $ last' <$> last' res
atEnd indents
pure [DoLetLocal (MkFC fname start end) (concat res)]
<|> do start <- location
keyword "rewrite"
rule <- expr pdef fname indents
end <- pure $ endPos $ getPTermLoc rule
atEnd indents
end <- location
pure [DoRewrite (MkFC fname start end) rule]
<|> do start <- location
e <- expr plhs fname indents
(do atEnd indents
end <- location
end <- pure $ endPos $ getPTermLoc e
pure [DoExp (MkFC fname start end) e])
<|> (do symbol "<-"
val <- expr pnowith fname indents
alts <- block (patAlt fname)
atEnd indents
end <- location
end <- pure $ fromMaybe end $ (endPos . getPClauseLoc) <$> last' alts
atEnd indents
pure [DoBindPat (MkFC fname start end) e val alts])
patAlt : FileName -> IndentInfo -> Rule PClause
@ -799,22 +804,22 @@ mutual
= do start <- location
exactIdent "Lazy"
tm <- simpleExpr fname indents
end <- location
end <- pure $ endPos $ getPTermLoc tm
pure (PDelayed (MkFC fname start end) LLazy tm)
<|> do start <- location
exactIdent "Inf"
tm <- simpleExpr fname indents
end <- location
end <- pure $ endPos $ getPTermLoc tm
pure (PDelayed (MkFC fname start end) LInf tm)
<|> do start <- location
exactIdent "Delay"
tm <- simpleExpr fname indents
end <- location
end <- pure $ endPos $ getPTermLoc tm
pure (PDelay (MkFC fname start end) tm)
<|> do start <- location
exactIdent "Force"
tm <- simpleExpr fname indents
end <- location
end <- pure $ endPos $ getPTermLoc tm
pure (PForce (MkFC fname start end) tm)
binder : FileName -> IndentInfo -> Rule PTerm
@ -836,6 +841,7 @@ mutual
op <- opExpr pdef fname indents
pure (exp, op))
end <- location
end <- pure $ fromMaybe end $ (endPos . getPTermLoc . snd) <$> last' rest
pure (mkPi start end arg rest))
<|> pure arg
where
@ -872,7 +878,7 @@ tyDecl fname indents
symbol ":"
mustWork $
do ty <- expr pdef fname indents
end <- location
end <- pure $ endPos $ getPTermLoc ty
atEnd indents
pure (MkPTy (MkFC fname start end) n doc ty)
@ -903,9 +909,9 @@ mutual
ws <- nonEmptyBlock (clause (S withArgs) fname)
end <- location
pure (MkWithClause (MkFC fname start end) lhs wval flags ws)
<|> do keyword "impossible"
<|> do end <- endLocation
keyword "impossible"
atEnd indents
end <- location
pure (MkImpossible (MkFC fname start end) lhs)
ifThenElse : Bool -> Lazy t -> Lazy t -> t
@ -933,7 +939,7 @@ mutual
= do symbol "|"
start <- location
tm <- expr plhs fname indents
end <- location
end <- pure $ endPos $ getPTermLoc tm
pure (MkFC fname start end, tm)
mkTyConType : FC -> List Name -> PTerm
@ -959,12 +965,13 @@ mkDataConType fc ret (WithArg a :: xs)
simpleCon : FileName -> PTerm -> IndentInfo -> Rule PTypeDecl
simpleCon fname ret indents
= do start <- location
= do start <- location
cdoc <- option "" documentation
cname <- name
params <- many (argExpr plhs fname indents)
atEnd indents
end <- location
end <- pure $ fromMaybe end $ (endPos . getPTermLoc . argTerm) <$> last' params
atEnd indents
pure (let cfc = MkFC fname start end in
MkPTy cfc cname cdoc (mkDataConType cfc ret params))
@ -979,6 +986,7 @@ simpleData fname start n indents
cons <- sepBy1 (symbol "|")
(simpleCon fname conRetTy indents)
end <- location
end <- pure $ fromMaybe end $ (endPos . getPTypeDeclLoc) <$> last' cons
pure (MkPData (MkFC fname start end) n
(mkTyConType tyfc params) [] cons)
@ -1009,6 +1017,7 @@ dataBody fname mincol start n indents ty
pure dopts)
cs <- blockAfter mincol (tyDecl fname)
end <- location
end <- pure $ fromMaybe end $ (endPos . getPTypeDeclLoc) <$> last' cs
pure (MkPData (MkFC fname start end) n ty opts cs)
gadtData : FileName -> Int -> FilePos -> Name -> IndentInfo -> Rule PDataDecl
@ -1034,6 +1043,7 @@ dataDecl fname indents
vis <- visibility
dat <- dataDeclBody fname indents
end <- location
end <- pure $ endPos $ getPDataDeclLoc dat
pure (PData (MkFC fname start end) vis dat)
stripBraces : String -> String
@ -1176,7 +1186,7 @@ transformDecl fname indents
lhs <- expr plhs fname indents
symbol "="
rhs <- expr pnowith fname indents
end <- location
end <- pure $ endPos $ getPTermLoc rhs
pure (PTransform (MkFC fname start end) n lhs rhs)
runElabDecl : FileName -> IndentInfo -> Rule PDecl
@ -1184,7 +1194,7 @@ runElabDecl fname indents
= do start <- location
pragma "runElab"
tm <- expr pnowith fname indents
end <- location
end <- pure $ endPos $ getPTermLoc tm
pure (PRunElabDecl (MkFC fname start end) tm)
mutualDecls : FileName -> IndentInfo -> Rule PDecl
@ -1194,6 +1204,7 @@ mutualDecls fname indents
commit
ds <- assert_total (nonEmptyBlock (topDecl fname))
end <- location
end <- pure $ fromMaybe end $ map (endPos . getPDeclLoc) $ join $ last' <$> last' ds
pure (PMutual (MkFC fname start end) (concat ds))
paramDecls : FileName -> IndentInfo -> Rule PDecl
@ -1210,6 +1221,7 @@ paramDecls fname indents
symbol ")"
ds <- assert_total (nonEmptyBlock (topDecl fname))
end <- location
end <- pure $ fromMaybe end $ map (endPos . getPDeclLoc) $ join $ last' <$> last' ds
pure (PParameters (MkFC fname start end) ps (collectDefs (concat ds)))
usingDecls : FileName -> IndentInfo -> Rule PDecl
@ -1228,6 +1240,7 @@ usingDecls fname indents
symbol ")"
ds <- assert_total (nonEmptyBlock (topDecl fname))
end <- location
end <- pure $ fromMaybe end $ map (endPos . getPDeclLoc) $ join $ last' <$> last' ds
pure (PUsing (MkFC fname start end) us (collectDefs (concat ds)))
fnOpt : Rule PFnOpt
@ -1345,12 +1358,13 @@ ifaceDecl fname indents
pure (Just n))
body <- assert_total (blockAfter col (topDecl fname))
end <- location
end <- pure $ fromMaybe end $ map (endPos . getPDeclLoc) $ join $ last' <$> last' body
pure (PInterface (MkFC fname start end)
vis cons n doc params det dc (collectDefs (concat body)))
implDecl : FileName -> IndentInfo -> Rule PDecl
implDecl fname indents
= do start <- location
= do start <- location
doc <- option "" documentation
visOpts <- many (visOpt fname)
vis <- getVisibility Nothing visOpts
@ -1399,7 +1413,7 @@ fieldDecl fname indents
ns <- sepBy1 (symbol ",") name
symbol ":"
ty <- expr pdef fname indents
end <- location
end <- pure $ endPos $ getPTermLoc ty
pure (map (\n => MkField (MkFC fname start end)
rig p n ty) ns)
recordParam : FileName -> IndentInfo -> Rule (List (Name, RigCount, PiInfo PTerm, PTerm))
@ -1459,7 +1473,7 @@ claim fname indents
m <- multiplicity
rig <- getMult m
cl <- tyDecl fname indents
end <- location
end <- pure $ endPos $ getPTypeDeclLoc cl
pure (PClaim (MkFC fname start end) rig vis opts cl)
definition : FileName -> IndentInfo -> Rule PDecl
@ -1467,7 +1481,7 @@ definition fname indents
= do start <- location
doc <- option "" documentation
nd <- clause 0 fname indents
end <- location
end <- pure $ endPos $ getPClauseLoc nd
pure (PDef (MkFC fname start end) [nd])
fixDecl : FileName -> IndentInfo -> Rule (List PDecl)
@ -1489,7 +1503,7 @@ directiveDecl fname indents
<|>
(do pragma "runElab"
tm <- expr pdef fname indents
end <- location
end <- pure $ endPos $ getPTermLoc tm
atEnd indents
pure (PReflect (MkFC fname start end) tm))

1
src/Idris/ProcessIdr.idr
View File

@ -224,6 +224,7 @@ processMod : {auto c : Ref Ctxt Defs} ->
Core (Maybe (List Error))
processMod srcf ttcf msg sourcecode
= catch (do
setCurrentElabSource sourcecode
-- Just read the header to start with (this is to get the imports and
-- see if we can avoid rebuilding if none have changed)
modh <- readHeader srcf

23
src/Idris/REPL.idr
View File

@ -154,9 +154,10 @@ setOpt (Editor e)
= do opts <- get ROpts
put ROpts (record { editor = e } opts)
setOpt (CG e)
= case getCG e of
Just cg => setCG cg
Nothing => iputStrLn "No such code generator available"
= do defs <- get Ctxt
case getCG (options defs) e of
Just cg => setCG cg
Nothing => iputStrLn "No such code generator available"
getOptions : {auto c : Ref Ctxt Defs} ->
{auto o : Ref ROpts REPLOpts} ->
@ -170,7 +171,8 @@ getOptions = do
]
export
findCG : {auto c : Ref Ctxt Defs} -> Core Codegen
findCG : {auto o : Ref ROpts REPLOpts} ->
{auto c : Ref Ctxt Defs} -> Core Codegen
findCG
= do defs <- get Ctxt
case codegen (session (options defs)) of
@ -178,6 +180,10 @@ findCG
Racket => pure codegenRacket
Gambit => pure codegenGambit
Node => pure codegenNode
Other s => case !(getCodegen s) of
Just cg => pure cg
Nothing => do coreLift $ putStrLn ("No such code generator: " ++ s)
coreLift $ exitWith (ExitFailure 1)
anyAt : (FC -> Bool) -> FC -> a -> Bool
anyAt p loc y = p loc
@ -350,12 +356,12 @@ processEdit (ExprSearch upd line name hints all)
dropLams _ env tm = (_ ** (env, tm))
processEdit (GenerateDef upd line name)
= do defs <- get Ctxt
Just (_, n', _, _) <- findTyDeclAt (\p, n => onLine line p)
Just (_, n', _, _) <- findTyDeclAt (\p, n => onLine (line - 1) p)
| Nothing => pure (EditError ("Can't find declaration for " ++ show name ++ " on line " ++ show line))
case !(lookupDefExact n' (gamma defs)) of
Just None =>
catch
(do Just (fc, cs) <- makeDef (\p, n => onLine line p) n'
(do Just (fc, cs) <- makeDef (\p, n => onLine (line - 1) p) n'
| Nothing => processEdit (AddClause upd line name)
Just srcLine <- getSourceLine line
| Nothing => pure (EditError "Source line not found")
@ -435,6 +441,7 @@ execExp : {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
execExp ctm
= do ttimp <- desugar AnyExpr [] (PApp replFC (PRef replFC (UN "unsafePerformIO")) ctm)
@ -735,7 +742,9 @@ interpret inp
= case parseRepl inp of
Left err => pure $ REPLError (show err)
Right Nothing => pure Done
Right (Just cmd) => processCatch cmd
Right (Just cmd) => do
setCurrentElabSource inp
processCatch cmd
mutual
export

38
src/Idris/REPLOpts.idr
View File

@ -1,7 +1,9 @@
module Idris.REPLOpts
import Compiler.Common
import Idris.Syntax
import Data.List
import Data.Strings
import System.File
@ -22,11 +24,16 @@ record REPLOpts where
editor : String
errorLine : Maybe Int
idemode : OutputMode
currentElabSource : String
-- TODO: Move extraCodegens from here, it doesn't belong, but there's nowhere
-- better to stick it now.
extraCodegens : List (String, Codegen)
export
defaultOpts : Maybe String -> OutputMode -> REPLOpts
defaultOpts fname outmode
= MkREPLOpts False NormaliseAll fname "" "vim" Nothing outmode
defaultOpts : Maybe String -> OutputMode -> List (String, Codegen) -> REPLOpts
defaultOpts fname outmode cgs
= MkREPLOpts False NormaliseAll fname "" "vim" Nothing outmode "" cgs
export
data ROpts : Type where
@ -79,3 +86,28 @@ getSourceLine l
findLine Z (l :: ls) = Just l
findLine (S k) (l :: ls) = findLine k ls
findLine _ [] = Nothing
export
setCurrentElabSource : {auto o : Ref ROpts REPLOpts} ->
String -> Core ()
setCurrentElabSource src
= do opts <- get ROpts
put ROpts (record { currentElabSource = src } opts)
export
getCurrentElabSource : {auto o : Ref ROpts REPLOpts} ->
Core String
getCurrentElabSource
= do opts <- get ROpts
pure (currentElabSource opts)
addCodegen : {auto o : Ref ROpts REPLOpts} ->
String -> Codegen -> Core ()
addCodegen s cg = do opts <- get ROpts
put ROpts (record { extraCodegens $= ((s,cg)::) } opts)
export
getCodegen : {auto o : Ref ROpts REPLOpts} ->
String -> Core (Maybe Codegen)
getCodegen s = do opts <- get ROpts
pure $ lookup s (extraCodegens opts)

11
src/Idris/SetOptions.idr
View File

@ -62,13 +62,14 @@ preOptions (NoPrelude :: opts)
= do setSession (record { noprelude = True } !getSession)
preOptions opts
preOptions (SetCG e :: opts)
= case getCG e of
Just cg => do setCG cg
preOptions opts
Nothing =>
= do defs <- get Ctxt
case getCG (options defs) e of
Just cg => do setCG cg
preOptions opts
Nothing =>
do coreLift $ putStrLn "No such code generator"
coreLift $ putStrLn $ "Code generators available: " ++
showSep ", " (map fst availableCGs)
showSep ", " (map fst (availableCGs (options defs)))
coreLift $ exitWith (ExitFailure 1)
preOptions (PkgPath p :: opts)
= do addPkgDir p

84
src/Idris/Syntax.idr
View File

@ -100,6 +100,57 @@ mutual
-- with-disambiguation
PWithUnambigNames : FC -> List Name -> PTerm -> PTerm
export
getPTermLoc : PTerm -> FC
getPTermLoc (PRef fc _) = fc
getPTermLoc (PPi fc _ _ _ _ _) = fc
getPTermLoc (PLam fc _ _ _ _ _) = fc
getPTermLoc (PLet fc _ _ _ _ _ _) = fc
getPTermLoc (PCase fc _ _) = fc
getPTermLoc (PLocal fc _ _) = fc
getPTermLoc (PUpdate fc _) = fc
getPTermLoc (PApp fc _ _) = fc
getPTermLoc (PWithApp fc _ _) = fc
getPTermLoc (PImplicitApp fc _ _ _) = fc
getPTermLoc (PDelayed fc _ _) = fc
getPTermLoc (PDelay fc _) = fc
getPTermLoc (PForce fc _) = fc
getPTermLoc (PSearch fc _) = fc
getPTermLoc (PPrimVal fc _) = fc
getPTermLoc (PQuote fc _) = fc
getPTermLoc (PQuoteName fc _) = fc
getPTermLoc (PQuoteDecl fc _) = fc
getPTermLoc (PUnquote fc _) = fc
getPTermLoc (PRunElab fc _) = fc
getPTermLoc (PHole fc _ _) = fc
getPTermLoc (PType fc) = fc
getPTermLoc (PAs fc _ _) = fc
getPTermLoc (PDotted fc _) = fc
getPTermLoc (PImplicit fc) = fc
getPTermLoc (PInfer fc) = fc
getPTermLoc (POp fc _ _ _) = fc
getPTermLoc (PPrefixOp fc _ _) = fc
getPTermLoc (PSectionL fc _ _) = fc
getPTermLoc (PSectionR fc _ _) = fc
getPTermLoc (PEq fc _ _) = fc
getPTermLoc (PBracketed fc _) = fc
getPTermLoc (PDoBlock fc _) = fc
getPTermLoc (PBang fc _) = fc
getPTermLoc (PIdiom fc _) = fc
getPTermLoc (PList fc _) = fc
getPTermLoc (PPair fc _ _) = fc
getPTermLoc (PDPair fc _ _ _) = fc
getPTermLoc (PUnit fc) = fc
getPTermLoc (PIfThenElse fc _ _ _) = fc
getPTermLoc (PComprehension fc _ _) = fc
getPTermLoc (PRewrite fc _ _) = fc
getPTermLoc (PRange fc _ _ _) = fc
getPTermLoc (PRangeStream fc _ _) = fc
getPTermLoc (PRecordFieldAccess fc _ _) = fc
getPTermLoc (PRecordProjection fc _) = fc
getPTermLoc (PUnifyLog fc _ _) = fc
getPTermLoc (PWithUnambigNames fc _ _) = fc
public export
data PFieldUpdate : Type where
PSetField : (path : List String) -> PTerm -> PFieldUpdate
@ -134,6 +185,10 @@ mutual
data PTypeDecl : Type where
MkPTy : FC -> (n : Name) -> (doc: String) -> (type : PTerm) -> PTypeDecl
export
getPTypeDeclLoc : PTypeDecl -> FC
getPTypeDeclLoc (MkPTy fc _ _ _) = fc
public export
data PDataDecl : Type where
MkPData : FC -> (tyname : Name) -> (tycon : PTerm) ->
@ -141,6 +196,11 @@ mutual
(datacons : List PTypeDecl) -> PDataDecl
MkPLater : FC -> (tyname : Name) -> (tycon : PTerm) -> PDataDecl
export
getPDataDeclLoc : PDataDecl -> FC
getPDataDeclLoc (MkPData fc _ _ _ _) = fc
getPDataDeclLoc (MkPLater fc _ _) = fc
public export
data PClause : Type where
MkPatClause : FC -> (lhs : PTerm) -> (rhs : PTerm) ->
@ -149,6 +209,12 @@ mutual
List WithFlag -> List PClause -> PClause
MkImpossible : FC -> (lhs : PTerm) -> PClause
export
getPClauseLoc : PClause -> FC
getPClauseLoc (MkPatClause fc _ _ _) = fc
getPClauseLoc (MkWithClause fc _ _ _ _) = fc
getPClauseLoc (MkImpossible fc _) = fc
public export
data Directive : Type where
Hide : Name -> Directive
@ -244,6 +310,24 @@ mutual
PRunElabDecl : FC -> PTerm -> PDecl
PDirective : FC -> Directive -> PDecl
export
getPDeclLoc : PDecl -> FC
getPDeclLoc (PClaim fc _ _ _ _) = fc
getPDeclLoc (PDef fc _) = fc
getPDeclLoc (PData fc _ _) = fc
getPDeclLoc (PParameters fc _ _) = fc
getPDeclLoc (PUsing fc _ _) = fc
getPDeclLoc (PReflect fc _) = fc
getPDeclLoc (PInterface fc _ _ _ _ _ _ _ _) = fc
getPDeclLoc (PImplementation fc _ _ _ _ _ _ _ _ _ _) = fc
getPDeclLoc (PRecord fc _ _ _ _ _) = fc
getPDeclLoc (PMutual fc _) = fc
getPDeclLoc (PFixity fc _ _ _) = fc
getPDeclLoc (PNamespace fc _ _) = fc
getPDeclLoc (PTransform fc _ _ _) = fc
getPDeclLoc (PRunElabDecl fc _) = fc
getPDeclLoc (PDirective fc _) = fc
definedInData : PDataDecl -> List Name
definedInData (MkPData _ n _ _ cons) = n :: map getName cons
where

2
src/Parser/Lexer/Package.idr
View File

@ -56,7 +56,7 @@ lex : String -> Either (Int, Int, String) (List (TokenData Token))
lex str =
case lexTo (const False) rawTokens str of
(tokenData, (l, c, "")) =>
Right $ (filter (useful . tok) tokenData) ++ [MkToken l c EndOfInput]
Right $ (filter (useful . tok) tokenData) ++ [MkToken l c l c EndOfInput]
(_, fail) => Left fail
where
useful : Token -> Bool

2
src/Parser/Lexer/Source.idr
View File

@ -232,7 +232,7 @@ lexTo pred str
-- Add the EndInput token so that we'll have a line and column
-- number to read when storing spans in the file
(tok, (l, c, "")) => Right (filter notComment tok ++
[MkToken l c EndInput])
[MkToken l c l c EndInput])
(_, fail) => Left fail
where
notComment : TokenData Token -> Bool

15
src/Parser/Rule/Common.idr
View File

@ -17,7 +17,20 @@ export
location : {token : _} -> EmptyRule token (Int, Int)
location
= do tok <- peek
pure (line tok, col tok)
pure (tok.line, tok.col)
export
endLocation : {token : _} -> EmptyRule token (Int, Int)
endLocation
= do tok <- peek
pure (tok.endLine, tok.endCol)
export
position : {token : _} -> EmptyRule token ((Int, Int), (Int, Int))
position
= do tok <- peek
pure ((tok.line, tok.col), (tok.endLine, tok.endCol))
export
column : {token : _ } -> EmptyRule token Int

10
src/Text/Lexer/Core.idr
View File

@ -135,6 +135,8 @@ record TokenData a where
constructor MkToken
line : Int
col : Int
endLine : Int
endCol : Int
tok : a
export
@ -168,9 +170,11 @@ tokenise pred line col acc tmap str
getFirstToken [] str = Nothing
getFirstToken ((lex, fn) :: ts) str
= case scan lex [] str of
Just (tok, rest) => Just (MkToken line col (fn (fastPack (reverse tok))),
line + cast (countNLs tok),
getCols tok col, rest)
Just (tok, rest) =>
let line' = line + cast (countNLs tok)
col' = getCols tok col in
Just (MkToken line col line' col' (fn (fastPack (reverse tok))),
line', col', rest)
Nothing => getFirstToken ts str
||| Given a mapping from lexers to token generating functions (the

16
src/Text/Literate.idr
View File

@ -64,13 +64,13 @@ rawTokens delims ls =
||| Merge the tokens into a single source file.
reduce : List (TokenData Token) -> List String -> String
reduce [] acc = fastAppend (reverse acc)
reduce (MkToken _ _ (Any x) :: rest) acc = reduce rest (blank_content::acc)
reduce (MkToken _ _ _ _ (Any x) :: rest) acc = reduce rest (blank_content::acc)
where
-- Preserve the original document's line count.
blank_content : String
blank_content = fastAppend (replicate (length (lines x)) "\n")
reduce (MkToken _ _ (CodeLine m src) :: rest) acc =
reduce (MkToken _ _ _ _ (CodeLine m src) :: rest) acc =
if m == trim src
then reduce rest ("\n"::acc)
else reduce rest ((substr (length m + 1) -- remove space to right of marker.
@ -78,11 +78,11 @@ reduce (MkToken _ _ (CodeLine m src) :: rest) acc =
src
)::acc)
reduce (MkToken _ _ (CodeBlock l r src) :: rest) acc with (lines src) -- Strip the deliminators surrounding the block.
reduce (MkToken _ _ (CodeBlock l r src) :: rest) acc | [] = reduce rest acc -- 1
reduce (MkToken _ _ (CodeBlock l r src) :: rest) acc | (s :: ys) with (snocList ys)
reduce (MkToken _ _ (CodeBlock l r src) :: rest) acc | (s :: []) | Empty = reduce rest acc -- 2
reduce (MkToken _ _ (CodeBlock l r src) :: rest) acc | (s :: (srcs ++ [f])) | (Snoc f srcs rec) =
reduce (MkToken _ _ _ _ (CodeBlock l r src) :: rest) acc with (lines src) -- Strip the deliminators surrounding the block.
reduce (MkToken _ _ _ _ (CodeBlock l r src) :: rest) acc | [] = reduce rest acc -- 1
reduce (MkToken _ _ _ _ (CodeBlock l r src) :: rest) acc | (s :: ys) with (snocList ys)
reduce (MkToken _ _ _ _ (CodeBlock l r src) :: rest) acc | (s :: []) | Empty = reduce rest acc -- 2
reduce (MkToken _ _ _ _ (CodeBlock l r src) :: rest) acc | (s :: (srcs ++ [f])) | (Snoc f srcs rec) =
reduce rest ("\n" :: unlines srcs :: acc)
-- [ NOTE ] 1 & 2 shouldn't happen as code blocks are well formed i.e. have two deliminators.
@ -184,7 +184,7 @@ isLiterateLine : (specification : LiterateStyle)
-> (str : String)
-> Pair (Maybe String) String
isLiterateLine (MkLitStyle delims markers _) str with (lex (rawTokens delims markers) str)
isLiterateLine (MkLitStyle delims markers _) str | ([MkToken _ _ (CodeLine m str')], (_,_, "")) = (Just m, str')
isLiterateLine (MkLitStyle delims markers _) str | ([MkToken _ _ _ _ (CodeLine m str')], (_,_, "")) = (Just m, str')
isLiterateLine (MkLitStyle delims markers _) str | (_, _) = (Nothing, str)
||| Given a 'literate specification' embed the given code using the

15
src/Utils/Hex.idr
View File

@ -1,5 +1,6 @@
module Utils.Hex
import Data.List
import Data.Primitives.Views
%default total
@ -26,13 +27,23 @@ hexDigit _ = 'X' -- TMP HACK: Ideally we'd have a bounds proof, generated below
||| Convert a positive integer into a list of (lower case) hexadecimal characters
export
asHex : Int -> String
asHex n = pack $ asHex' n []
asHex n =
if n > 0
then pack $ asHex' n []
else "0"
where
asHex' : Int -> List Char -> List Char
asHex' 0 hex = hex
asHex' n hex with (n `divides` 16)
asHex' (16 * div + rem) hex | DivBy div rem _ =
assert_total $ asHex' div (hexDigit rem :: hex)
asHex' (assert_smaller n div) (hexDigit rem :: hex)
export
leftPad : Char -> Nat -> String -> String
leftPad paddingChar padToLength str =
if length str < padToLength
then pack (List.replicate (minus padToLength (length str)) paddingChar) ++ str
else str
export
fromHexDigit : Char -> Maybe Int

2
support/c/idris_file.c
View File

@ -107,7 +107,7 @@ char* idris2_readLine(FILE* f) {
return buffer; // freed by RTS if not NULL
}
char* idris_readChars(int num, FILE* f) {
char* idris2_readChars(int num, FILE* f) {
char *buffer = malloc((num+1)*sizeof(char));
size_t len;
len = fread(buffer, sizeof(char), (size_t)num, f);

2
support/c/idris_file.h
View File

@ -18,7 +18,7 @@ int idris2_fpoll(FILE* f);
// Treat as a Ptr String (might be NULL)
char* idris2_readLine(FILE* f);
char* idris_readChars(int num, FILE* f);
char* idris2_readChars(int num, FILE* f);
int idris2_writeLine(FILE* f, char* str);

17
support/c/idris_support.c
View File

@ -5,6 +5,7 @@
#include <stdio.h>
#include <string.h>
#include <time.h>
#include <stdlib.h>
#ifdef _WIN32
extern char **_environ;
@ -73,3 +74,19 @@ int idris2_time() {
char* idris2_getEnvPair(int i) {
return *(environ + i);
}
int idris2_setenv(const char *name, const char *value, int overwrite) {
#ifdef _WIN32
return win32_modenv(name, value, overwrite);
#else
return setenv(name, value, overwrite);
#endif
}
int idris2_unsetenv(const char *name) {
#ifdef _WIN32
return win32_modenv(name, "", 1);
#else
return unsetenv(name);
#endif
}

7
support/c/windows/win_utils.c
View File

@ -67,9 +67,14 @@ void win32_gettime(int64_t* sec, int64_t* nsec)
*nsec = (t.QuadPart % 10000000)*100;
*sec = t.QuadPart / 10000000;
*sec -= 11644473600; // LDAP epoch to Unix epoch
*sec -= 11644473600; // LDAP epoch to Unix epoch
}
void win32_sleep(int ms) {
Sleep(ms);
}
int win32_modenv(const char* name, const char* value, int overwrite) {
if (!overwrite && getenv(name)) return 0;
return _putenv_s(name, value);
}

1
support/c/windows/win_utils.h
View File

@ -8,3 +8,4 @@ FILE *win32_u8fopen(const char *path, const char *mode);
FILE *win32_u8popen(const char *path, const char *mode);
void win32_gettime(int64_t* sec, int64_t* nsec);
void win32_sleep(int ms);
int win32_modenv(const char* name, const char* value, int overwrite);

5
support/chez/support.ss
View File

@ -1,6 +1,9 @@
(define (blodwen-os)
(case (machine-type)
[(i3le ti3le a6le ta6le) "unix"]
[(i3le ti3le a6le ta6le) "unix"] ; GNU/Linux
[(i3ob ti3ob a6ob ta6ob) "unix"] ; OpenBSD
[(i3fb ti3fb a6fb ta6fb) "unix"] ; FreeBSD
[(i3nb ti3nb a6nb ta6nb) "unix"] ; NetBSD
[(i3osx ti3osx a6osx ta6osx) "darwin"]
[(i3nt ti3nt a6nt ta6nt) "windows"]
[else "unknown"]))

2
tests/Main.idr
View File

@ -113,7 +113,7 @@ chezTests
= ["chez001", "chez002", "chez003", "chez004", "chez005", "chez006",
"chez007", "chez008", "chez009", "chez010", "chez011", "chez012",
"chez013", "chez014", "chez015", "chez016", "chez017", "chez018",
"chez019", "chez020", "chez021", "chez022",
"chez019", "chez020", "chez021", "chez022", "chez023", "chez024",
"reg001"]
nodeTests : List String

1
tests/chez/chez004/expected
View File

@ -5,5 +5,6 @@
"there!"
65535
[0, 94, 0, 0, 0, 65, 65, 65, 65, 0, 123, 20, 174, 71, 225, 154, 87, 64, 0, 0, 72, 101, 108, 108, 111, 32, 116, 104, 101, 114, 101, 33, 255, 255, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0]
[0, 94, 0, 0, 0, 65, 65, 65, 65, 0, 123, 20, 174, 71, 225, 154, 87, 64, 0, 0, 72, 101, 108, 108, 111, 32, 116, 104, 101, 114, 101, 33, 255, 255, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0]
1/1: Building Buffer (Buffer.idr)
Main> Main> Bye for now!

12
tests/chez/chez006/expected
View File

@ -16,6 +16,12 @@ strangeId' _
Main> Bye for now!
1/1: Building TypeCase2 (TypeCase2.idr)
TypeCase2.idr:5:14--5:17:While processing left hand side of strangeId at TypeCase2.idr:5:1--6:1:
Can't match on Nat (Erased argument)
TypeCase2.idr:9:5--9:9:While processing left hand side of foo at TypeCase2.idr:9:1--10:1:
Can't match on Nat (Erased argument)
Can't match on Nat (Erased argument) at
5 strangeId {a=Nat} x = x+1
^^^
TypeCase2.idr:9:5--9:8:While processing left hand side of foo at TypeCase2.idr:9:1--10:1:
Can't match on Nat (Erased argument) at
9 foo Nat = "Nat"
^^^

14
tests/chez/chez010/run
View File

@ -1,4 +1,14 @@
make all > /dev/null
case `uname -s` in
OpenBSD|FreeBSD|NetBSD)
MAKE=gmake
;;
*)
MAKE=make
;;
esac
${MAKE} all > /dev/null
$1 --no-banner CB.idr < input
rm -rf build
make clean > /dev/null
${MAKE} clean > /dev/null

14
tests/chez/chez013/run
View File

@ -1,4 +1,14 @@
make all > /dev/null
case `uname -s` in
OpenBSD|FreeBSD|NetBSD)
MAKE=gmake
;;
*)
MAKE=make
;;
esac
${MAKE} all > /dev/null
$1 --no-banner Struct.idr < input
rm -rf build
make clean > /dev/null
${MAKE} clean > /dev/null

14
tests/chez/chez022/run
View File

@ -1,4 +1,14 @@
make all > /dev/null
case `uname -s` in
OpenBSD|FreeBSD|NetBSD)
MAKE=gmake
;;
*)
MAKE=make
;;
esac
${MAKE} all > /dev/null
$1 --no-banner usealloc.idr < input
rm -rf build
make clean > /dev/null
${MAKE} clean > /dev/null

39
tests/chez/chez023/File.idr Normal file
View File

@ -0,0 +1,39 @@
import System.File
import Control.App
import Control.App.FileIO
import Control.App.Console
testFileReadOps : File -> Has [Console, FileIO] e => App e ()
testFileReadOps file = do
testStr <- fGetChars file 6
putStrLn testStr
chr <- fGetChar file
putStrLn (show chr)
rest <- fGetStr file
putStrLn rest
testFileWriteOps : File -> Has [Console, FileIO] e => App e ()
testFileWriteOps file = do
fPutStr file "Hello "
fPutStrLn file "Idris!"
fPutStrLn file "Another line"
runTests : Has [Console, FileIO] e => App e ()
runTests = do
withFile "test.txt" WriteTruncate
(\err => putStrLn $ "Failed to open file in write mode: " ++ show err)
(\file => testFileWriteOps file)
withFile "test.txt" Read
(\err => putStrLn $ "Failed to open file in read mode: " ++ show err)
(\file => testFileReadOps file)
prog : App Init ()
prog =
handle runTests
(\() => putStrLn "No exceptions occurred")
(\err: IOError =>
putStrLn $ "Caught file error : " ++ show err)
main : IO ()
main = run prog

7
tests/chez/chez023/expected Normal file
View File

@ -0,0 +1,7 @@
Hello
'I'
dris!
No exceptions occurred
1/1: Building File (File.idr)
Main> Main> Bye for now!

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

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

3
tests/chez/chez023/run Normal file
View File

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

26
tests/chez/chez024/Envy.idr Normal file
View File

@ -0,0 +1,26 @@
module Main
import System
main : IO ()
main = do
ok <- setEnv "HELLO" "HI" True
printLn ok
Just str <- getEnv "HELLO"
| Nothing => pure ()
putStrLn str
ok <- setEnv "HELLO" "HO" False
printLn ok
Just str <- getEnv "HELLO"
| Nothing => pure ()
putStrLn str
ok <- setEnv "HELLO" "EH" True
printLn ok
Just str <- getEnv "HELLO"
| Nothing => pure ()
putStrLn str
ok <- unsetEnv "HELLO"
printLn ok
Just str <- getEnv "HELLO"
| Nothing => putStrLn "Nothing there"
pure ()

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

@ -0,0 +1,10 @@
True
HI
True
HI
True
EH
True
Nothing there
1/1: Building Envy (Envy.idr)
Main> Main> Bye for now!

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

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

3
tests/chez/chez024/run Normal file
View File

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

38
tests/ideMode/ideMode001/expected
View File

@ -1,26 +1,26 @@
000018(:protocol-version 2 0)
000038(:write-string "1/1: Building LocType (LocType.idr)" 1)
0000ca(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 7 23) (:end 7 25)) ((:name "x") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "a")))))) 1)
0000d8(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 7 38) (:end 8 1)) ((:name "ys") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "(Main.Vect m a)")))))) 1)
0000df(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 7 35) (:end 7 38)) ((:name "xs") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "(Main.Vect {k:269} a)")))))) 1)
0000d3(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 7 9) (:end 7 11)) ((:name "x") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "?{_:270}_[]")))))) 1)
0000ca(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 7 23) (:end 7 24)) ((:name "x") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "a")))))) 1)
0000d9(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 7 38) (:end 7 40)) ((:name "ys") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "(Main.Vect m a)")))))) 1)
0000df(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 7 35) (:end 7 37)) ((:name "xs") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "(Main.Vect {k:269} a)")))))) 1)
0000d3(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 7 9) (:end 7 10)) ((:name "x") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "?{_:270}_[]")))))) 1)
0000ed(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 7 14) (:end 7 16)) ((:name "xs") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "(Main.Vect ?{k:269}_[] ?{_:270}_[])")))))) 1)
0000ed(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 7 18) (:end 7 21)) ((:name "ys") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "(Main.Vect ?{_:271}_[] ?{_:270}_[])")))))) 1)
0000d8(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 6 16) (:end 7 1)) ((:name "ys") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "(Main.Vect m a)")))))) 1)
0000ed(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 6 11) (:end 6 14)) ((:name "ys") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "(Main.Vect ?{_:260}_[] ?{_:259}_[])")))))) 1)
0001ca(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 5 1) (:end 6 1)) ((:name "Main.append") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "{0 m : Prelude.Nat} -> {0 a : Type} -> {0 n : Prelude.Nat} -> (({arg:250} : (Main.Vect n[0] a[1])) -> (({arg:251} : (Main.Vect m[3] a[2])) -> (Main.Vect (Prelude.+ Prelude.Nat Prelude.Num implementation at Prelude.idr:849:1--856:1 n[2] m[4]) a[3])))")))))) 1)
0000cb(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 5 47) (:end 6 1)) ((:name "a") (:namespace "") (:decor :type) (:implicit :False) (:key "") (:doc-overview "") (:type "Type")))))) 1)
0000ed(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 7 18) (:end 7 20)) ((:name "ys") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "(Main.Vect ?{_:271}_[] ?{_:270}_[])")))))) 1)
0000d9(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 6 16) (:end 6 18)) ((:name "ys") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "(Main.Vect m a)")))))) 1)
0000ed(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 6 11) (:end 6 13)) ((:name "ys") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "(Main.Vect ?{_:260}_[] ?{_:259}_[])")))))) 1)
0001cb(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 5 1) (:end 5 48)) ((:name "Main.append") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "{0 m : Prelude.Nat} -> {0 a : Type} -> {0 n : Prelude.Nat} -> (({arg:250} : (Main.Vect n[0] a[1])) -> (({arg:251} : (Main.Vect m[3] a[2])) -> (Main.Vect (Prelude.+ Prelude.Nat Prelude.Num implementation at Prelude.idr:849:1--856:1 n[2] m[4]) a[3])))")))))) 1)
0000cc(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 5 47) (:end 5 48)) ((:name "a") (:namespace "") (:decor :type) (:implicit :False) (:key "") (:doc-overview "") (:type "Type")))))) 1)
0000d3(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 5 44) (:end 5 45)) ((:name "m") (:namespace "") (:decor :type) (:implicit :False) (:key "") (:doc-overview "") (:type "Prelude.Nat")))))) 1)
0000d3(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 5 40) (:end 5 42)) ((:name "n") (:namespace "") (:decor :type) (:implicit :False) (:key "") (:doc-overview "") (:type "Prelude.Nat")))))) 1)
0000cc(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 5 29) (:end 5 31)) ((:name "a") (:namespace "") (:decor :type) (:implicit :False) (:key "") (:doc-overview "") (:type "Type")))))) 1)
0000d3(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 5 27) (:end 5 29)) ((:name "m") (:namespace "") (:decor :type) (:implicit :False) (:key "") (:doc-overview "") (:type "Prelude.Nat")))))) 1)
0000cc(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 5 17) (:end 5 19)) ((:name "a") (:namespace "") (:decor :type) (:implicit :False) (:key "") (:doc-overview "") (:type "Type")))))) 1)
0000d3(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 5 15) (:end 5 17)) ((:name "n") (:namespace "") (:decor :type) (:implicit :False) (:key "") (:doc-overview "") (:type "Prelude.Nat")))))) 1)
0000cb(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 3 41) (:end 5 1)) ((:name "a") (:namespace "") (:decor :type) (:implicit :False) (:key "") (:doc-overview "") (:type "Type")))))) 1)
0000d3(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 5 40) (:end 5 41)) ((:name "n") (:namespace "") (:decor :type) (:implicit :False) (:key "") (:doc-overview "") (:type "Prelude.Nat")))))) 1)
0000cc(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 5 29) (:end 5 30)) ((:name "a") (:namespace "") (:decor :type) (:implicit :False) (:key "") (:doc-overview "") (:type "Type")))))) 1)
0000d3(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 5 27) (:end 5 28)) ((:name "m") (:namespace "") (:decor :type) (:implicit :False) (:key "") (:doc-overview "") (:type "Prelude.Nat")))))) 1)
0000cc(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 5 17) (:end 5 18)) ((:name "a") (:namespace "") (:decor :type) (:implicit :False) (:key "") (:doc-overview "") (:type "Type")))))) 1)
0000d3(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 5 15) (:end 5 16)) ((:name "n") (:namespace "") (:decor :type) (:implicit :False) (:key "") (:doc-overview "") (:type "Prelude.Nat")))))) 1)
0000cc(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 3 41) (:end 3 42)) ((:name "a") (:namespace "") (:decor :type) (:implicit :False) (:key "") (:doc-overview "") (:type "Type")))))) 1)
0000d3(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 3 38) (:end 3 39)) ((:name "k") (:namespace "") (:decor :type) (:implicit :False) (:key "") (:doc-overview "") (:type "Prelude.Nat")))))) 1)
0000cc(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 3 25) (:end 3 27)) ((:name "a") (:namespace "") (:decor :type) (:implicit :False) (:key "") (:doc-overview "") (:type "Type")))))) 1)
0000d3(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 3 23) (:end 3 25)) ((:name "k") (:namespace "") (:decor :type) (:implicit :False) (:key "") (:doc-overview "") (:type "Prelude.Nat")))))) 1)
0000cc(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 3 13) (:end 3 15)) ((:name "a") (:namespace "") (:decor :type) (:implicit :False) (:key "") (:doc-overview "") (:type "Type")))))) 1)
0000cb(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 2 19) (:end 3 6)) ((:name "a") (:namespace "") (:decor :type) (:implicit :False) (:key "") (:doc-overview "") (:type "Type")))))) 1)
0000cc(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 3 25) (:end 3 26)) ((:name "a") (:namespace "") (:decor :type) (:implicit :False) (:key "") (:doc-overview "") (:type "Type")))))) 1)
0000d3(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 3 23) (:end 3 24)) ((:name "k") (:namespace "") (:decor :type) (:implicit :False) (:key "") (:doc-overview "") (:type "Prelude.Nat")))))) 1)
0000cc(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 3 13) (:end 3 14)) ((:name "a") (:namespace "") (:decor :type) (:implicit :False) (:key "") (:doc-overview "") (:type "Type")))))) 1)
0000cc(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 2 19) (:end 2 20)) ((:name "a") (:namespace "") (:decor :type) (:implicit :False) (:key "") (:doc-overview "") (:type "Type")))))) 1)
000015(:return (:ok ()) 1)
Alas the file is done, aborting

38
tests/ideMode/ideMode003/expected
View File

@ -1,27 +1,27 @@
000018(:protocol-version 2 0)
000038(:write-string "1/1: Building LocType (LocType.idr)" 1)
0000ca(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 7 23) (:end 7 25)) ((:name "x") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "a")))))) 1)
0000d8(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 7 38) (:end 8 1)) ((:name "ys") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "(Main.Vect m a)")))))) 1)
0000df(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 7 35) (:end 7 38)) ((:name "xs") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "(Main.Vect {k:269} a)")))))) 1)
0000d3(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 7 9) (:end 7 11)) ((:name "x") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "?{_:270}_[]")))))) 1)
0000ca(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 7 23) (:end 7 24)) ((:name "x") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "a")))))) 1)
0000d9(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 7 38) (:end 7 40)) ((:name "ys") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "(Main.Vect m a)")))))) 1)
0000df(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 7 35) (:end 7 37)) ((:name "xs") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "(Main.Vect {k:269} a)")))))) 1)
0000d3(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 7 9) (:end 7 10)) ((:name "x") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "?{_:270}_[]")))))) 1)
0000ed(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 7 14) (:end 7 16)) ((:name "xs") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "(Main.Vect ?{k:269}_[] ?{_:270}_[])")))))) 1)
0000ed(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 7 18) (:end 7 21)) ((:name "ys") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "(Main.Vect ?{_:271}_[] ?{_:270}_[])")))))) 1)
0000d8(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 6 16) (:end 7 1)) ((:name "ys") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "(Main.Vect m a)")))))) 1)
0000ed(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 6 11) (:end 6 14)) ((:name "ys") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "(Main.Vect ?{_:260}_[] ?{_:259}_[])")))))) 1)
0001ca(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 5 1) (:end 6 1)) ((:name "Main.append") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "{0 m : Prelude.Nat} -> {0 a : Type} -> {0 n : Prelude.Nat} -> (({arg:250} : (Main.Vect n[0] a[1])) -> (({arg:251} : (Main.Vect m[3] a[2])) -> (Main.Vect (Prelude.+ Prelude.Nat Prelude.Num implementation at Prelude.idr:849:1--856:1 n[2] m[4]) a[3])))")))))) 1)
0000cb(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 5 47) (:end 6 1)) ((:name "a") (:namespace "") (:decor :type) (:implicit :False) (:key "") (:doc-overview "") (:type "Type")))))) 1)
0000ed(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 7 18) (:end 7 20)) ((:name "ys") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "(Main.Vect ?{_:271}_[] ?{_:270}_[])")))))) 1)
0000d9(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 6 16) (:end 6 18)) ((:name "ys") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "(Main.Vect m a)")))))) 1)
0000ed(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 6 11) (:end 6 13)) ((:name "ys") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "(Main.Vect ?{_:260}_[] ?{_:259}_[])")))))) 1)
0001cb(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 5 1) (:end 5 48)) ((:name "Main.append") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "{0 m : Prelude.Nat} -> {0 a : Type} -> {0 n : Prelude.Nat} -> (({arg:250} : (Main.Vect n[0] a[1])) -> (({arg:251} : (Main.Vect m[3] a[2])) -> (Main.Vect (Prelude.+ Prelude.Nat Prelude.Num implementation at Prelude.idr:849:1--856:1 n[2] m[4]) a[3])))")))))) 1)
0000cc(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 5 47) (:end 5 48)) ((:name "a") (:namespace "") (:decor :type) (:implicit :False) (:key "") (:doc-overview "") (:type "Type")))))) 1)
0000d3(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 5 44) (:end 5 45)) ((:name "m") (:namespace "") (:decor :type) (:implicit :False) (:key "") (:doc-overview "") (:type "Prelude.Nat")))))) 1)
0000d3(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 5 40) (:end 5 42)) ((:name "n") (:namespace "") (:decor :type) (:implicit :False) (:key "") (:doc-overview "") (:type "Prelude.Nat")))))) 1)
0000cc(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 5 29) (:end 5 31)) ((:name "a") (:namespace "") (:decor :type) (:implicit :False) (:key "") (:doc-overview "") (:type "Type")))))) 1)
0000d3(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 5 27) (:end 5 29)) ((:name "m") (:namespace "") (:decor :type) (:implicit :False) (:key "") (:doc-overview "") (:type "Prelude.Nat")))))) 1)
0000cc(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 5 17) (:end 5 19)) ((:name "a") (:namespace "") (:decor :type) (:implicit :False) (:key "") (:doc-overview "") (:type "Type")))))) 1)
0000d3(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 5 15) (:end 5 17)) ((:name "n") (:namespace "") (:decor :type) (:implicit :False) (:key "") (:doc-overview "") (:type "Prelude.Nat")))))) 1)
0000cb(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 3 41) (:end 5 1)) ((:name "a") (:namespace "") (:decor :type) (:implicit :False) (:key "") (:doc-overview "") (:type "Type")))))) 1)
0000d3(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 5 40) (:end 5 41)) ((:name "n") (:namespace "") (:decor :type) (:implicit :False) (:key "") (:doc-overview "") (:type "Prelude.Nat")))))) 1)
0000cc(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 5 29) (:end 5 30)) ((:name "a") (:namespace "") (:decor :type) (:implicit :False) (:key "") (:doc-overview "") (:type "Type")))))) 1)
0000d3(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 5 27) (:end 5 28)) ((:name "m") (:namespace "") (:decor :type) (:implicit :False) (:key "") (:doc-overview "") (:type "Prelude.Nat")))))) 1)
0000cc(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 5 17) (:end 5 18)) ((:name "a") (:namespace "") (:decor :type) (:implicit :False) (:key "") (:doc-overview "") (:type "Type")))))) 1)
0000d3(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 5 15) (:end 5 16)) ((:name "n") (:namespace "") (:decor :type) (:implicit :False) (:key "") (:doc-overview "") (:type "Prelude.Nat")))))) 1)
0000cc(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 3 41) (:end 3 42)) ((:name "a") (:namespace "") (:decor :type) (:implicit :False) (:key "") (:doc-overview "") (:type "Type")))))) 1)
0000d3(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 3 38) (:end 3 39)) ((:name "k") (:namespace "") (:decor :type) (:implicit :False) (:key "") (:doc-overview "") (:type "Prelude.Nat")))))) 1)
0000cc(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 3 25) (:end 3 27)) ((:name "a") (:namespace "") (:decor :type) (:implicit :False) (:key "") (:doc-overview "") (:type "Type")))))) 1)
0000d3(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 3 23) (:end 3 25)) ((:name "k") (:namespace "") (:decor :type) (:implicit :False) (:key "") (:doc-overview "") (:type "Prelude.Nat")))))) 1)
0000cc(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 3 13) (:end 3 15)) ((:name "a") (:namespace "") (:decor :type) (:implicit :False) (:key "") (:doc-overview "") (:type "Type")))))) 1)
0000cb(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 2 19) (:end 3 6)) ((:name "a") (:namespace "") (:decor :type) (:implicit :False) (:key "") (:doc-overview "") (:type "Type")))))) 1)
0000cc(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 3 25) (:end 3 26)) ((:name "a") (:namespace "") (:decor :type) (:implicit :False) (:key "") (:doc-overview "") (:type "Type")))))) 1)
0000d3(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 3 23) (:end 3 24)) ((:name "k") (:namespace "") (:decor :type) (:implicit :False) (:key "") (:doc-overview "") (:type "Prelude.Nat")))))) 1)
0000cc(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 3 13) (:end 3 14)) ((:name "a") (:namespace "") (:decor :type) (:implicit :False) (:key "") (:doc-overview "") (:type "Type")))))) 1)
0000cc(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 2 19) (:end 2 20)) ((:name "a") (:namespace "") (:decor :type) (:implicit :False) (:key "") (:doc-overview "") (:type "Type")))))) 1)
000015(:return (:ok ()) 1)
000037(:return (:ok "Main.Vect : Nat -> Type -> Type" ()) 2)
Alas the file is done, aborting

2
tests/idris2/api001/Hello.idr Normal file
View File

@ -0,0 +1,2 @@
main : IO ()
main = putStrLn "Hello"

19
tests/idris2/api001/LazyCodegen.idr Normal file
View File

@ -0,0 +1,19 @@
module Main
import Core.Context
import Compiler.Common
import Idris.Driver
compile : Ref Ctxt Defs -> (execDir : String) ->
ClosedTerm -> (outfile : String) -> Core (Maybe String)
compile defs dir term file = do coreLift $ putStrLn "I'd rather not."
pure $ Nothing
execute : Ref Ctxt Defs -> (execDir : String) -> ClosedTerm -> Core ()
execute defs dir term = do coreLift $ putStrLn "Maybe in an hour."
lazyCodegen : Codegen
lazyCodegen = MkCG compile execute
main : IO ()
main = mainWithCodegens [("lazy", lazyCodegen)]

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

@ -0,0 +1 @@
I'd rather not.

3
tests/idris2/api001/run Normal file
View File

@ -0,0 +1,3 @@
$1 --no-banner -p idris2 -p contrib -p network LazyCodegen.idr -o lazy-idris2 > /dev/null
./build/exec/lazy-idris2 --no-banner --cg lazy Hello.idr -o hello
rm -rf build

4
tests/idris2/basic001/expected
View File

@ -5,4 +5,8 @@ Mismatch between:
S Z
and
Z
at:
1 zipWith plus (Cons Z Nil) (Cons (S Z) (Cons Z Nil))
^^^^^^^^^^^^^^^^^^^^^^^
Main> Bye for now!

7
tests/idris2/basic003/expected
View File

@ -1,8 +1,11 @@
1/1: Building Ambig1 (Ambig1.idr)
Main> Bye for now!
1/1: Building Ambig2 (Ambig2.idr)
Ambig2.idr:26:21--26:28:While processing right hand side of keepUnique at Ambig2.idr:26:1--28:1:
Ambiguous elaboration. Possible correct results:
Ambig2.idr:26:21--26:27:While processing right hand side of keepUnique at Ambig2.idr:26:1--28:1:
Ambiguous elaboration at:
26 keepUnique {b} xs = toList (fromList xs)
^^^^^^
Possible correct results:
Main.Set.toList ?arg
Main.Vect.toList ?arg
Main> Bye for now!

4
tests/idris2/basic005/expected
View File

@ -1,5 +1,5 @@
1/1: Building NoInfer (NoInfer.idr)
NoInfer.idr:1:7--1:9:Unsolved holes:
Main.{_:1} introduced at NoInfer.idr:1:7--1:9
NoInfer.idr:1:7--1:8:Unsolved holes:
Main.{_:1} introduced at NoInfer.idr:1:7--1:8
Main> Bye for now!

11
tests/idris2/basic011/expected
View File

@ -1,8 +1,15 @@
1/1: Building Dots1 (Dots1.idr)
1/1: Building Dots2 (Dots2.idr)
Dots2.idr:2:7--2:9:While processing left hand side of foo at Dots2.idr:2:1--4:1:
Can't match on ?x [no locals in scope] (Non linear pattern variable)
Dots2.idr:2:7--2:8:While processing left hand side of foo at Dots2.idr:2:1--4:1:
Can't match on ?x [no locals in scope] (Non linear pattern variable) at
2 foo x x = x + x
^
1/1: Building Dots3 (Dots3.idr)
Dots3.idr:5:29--5:30:While processing left hand side of addBaz at Dots3.idr:5:1--6:1:
Pattern variable z unifies with:
?y [no locals in scope]
at:
5 addBaz (x + y) (AddThings x z) = x + y
^

14
tests/idris2/basic014/expected
View File

@ -1,5 +1,11 @@
1/1: Building Rewrite (Rewrite.idr)
Rewrite.idr:15:25--17:1:While processing right hand side of wrongCommutes at Rewrite.idr:15:1--17:1:
Rewriting by m + k = k + m did not change type S k + m = m + S k
Rewrite.idr:19:26--20:1:While processing right hand side of wrongCommutes2 at Rewrite.idr:19:1--20:1:
Nat is not a rewrite rule type
Rewrite.idr:15:25--15:57:While processing right hand side of wrongCommutes at Rewrite.idr:15:1--17:1:
Rewriting by m + k = k + m did not change type S k + m = m + S k at:
15 wrongCommutes (S k) m = rewrite plusCommutes m k in ?bar
^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
Rewrite.idr:19:26--19:43:While processing right hand side of wrongCommutes2 at Rewrite.idr:19:1--20:1:
Nat is not a rewrite rule type at:
19 wrongCommutes2 (S k) m = rewrite m in ?bar
^^^^^^^^^^^^^^^^^

18
tests/idris2/basic016/expected
View File

@ -1,20 +1,32 @@
1/1: Building Eta (Eta.idr)
Eta.idr:14:10--15:1:While processing right hand side of etaBad at Eta.idr:14:1--15:1:
Eta.idr:14:10--14:14:While processing right hand side of etaBad at Eta.idr:14:1--15:1:
When unifying \x => (\y => (MkTest ?_ ?_)) = \x => (\y => (MkTest ?_ ?_)) and MkTest = \x => (\y => (MkTest ?_ ?_))
Mismatch between:
Nat
and
Integer
at:
14 etaBad = Refl
^^^^
1/1: Building Eta2 (Eta2.idr)
Eta2.idr:2:8--4:1:While processing right hand side of test at Eta2.idr:2:1--4:1:
Eta2.idr:2:8--2:12:While processing right hand side of test at Eta2.idr:2:1--4:1:
When unifying \x => (S ?_) = \x => (S ?_) and S = \x => (S ?_)
Mismatch between:
a
and
Nat
Eta2.idr:5:44--6:1:While processing right hand side of test2 at Eta2.idr:5:1--6:1:
at:
2 test = Refl
^^^^
Eta2.idr:5:44--5:48:While processing right hand side of test2 at Eta2.idr:5:1--6:1:
When unifying \x => (S ?_) = \x => (S ?_) and S = \x => (S ?_)
Mismatch between:
a
and
Nat
at:
5 test2 = {a : _} -> the (S = \x : a => S _) Refl
^^^^

7
tests/idris2/basic018/expected
View File

@ -1,3 +1,6 @@
1/1: Building Fin (Fin.idr)
Fin.idr:34:7--36:1:While processing right hand side of bar at Fin.idr:34:1--36:1:
Can't find an implementation for IsJust (integerToFin 8 5)
Fin.idr:34:7--34:8:While processing right hand side of bar at Fin.idr:34:1--36:1:
Can't find an implementation for IsJust (integerToFin 8 5) at:
34 bar = 8
^

14
tests/idris2/basic022/expected
View File

@ -1,7 +1,13 @@
1/1: Building Erase (Erase.idr)
Erase.idr:5:5--5:11:While processing left hand side of bad at Erase.idr:5:1--6:1:
Can't match on False (Erased argument)
Erase.idr:19:18--19:22:While processing left hand side of minusBad at Erase.idr:19:1--20:1:
Can't match on LeZ (Erased argument)
Erase.idr:5:5--5:10:While processing left hand side of bad at Erase.idr:5:1--6:1:
Can't match on False (Erased argument) at
5 bad False = True
^^^^^
Erase.idr:19:18--19:21:While processing left hand side of minusBad at Erase.idr:19:1--20:1:
Can't match on LeZ (Erased argument) at
19 minusBad (S k) Z LeZ = S k
^^^
Main> \m => minus (S (S m)) m prf
Main> Bye for now!

6
tests/idris2/basic030/expected
View File

@ -1,7 +1,11 @@
1/1: Building arity (arity.idr)
arity.idr:4:16--4:22:While processing right hand side of foo at arity.idr:4:1--7:1:
arity.idr:4:16--4:21:While processing right hand side of foo at arity.idr:4:1--7:1:
When unifying (1 _ : Nat) -> MyN and MyN
Mismatch between:
(1 _ : Nat) -> MyN
and
MyN
at:
4 foo x y = case MkN x of
^^^^^

5
tests/idris2/basic031/expected
View File

@ -1,3 +1,6 @@
1/1: Building erased (erased.idr)
erased.idr:7:17--7:21:While processing left hand side of nameOf at erased.idr:7:1--8:1:
Can't match on Bool (Erased argument)
Can't match on Bool (Erased argument) at
7 nameOf (MyMaybe Bool) = "MyMaybe Bool"
^^^^

14
tests/idris2/basic033/expected
View File

@ -1,5 +1,11 @@
1/1: Building unboundimps (unboundimps.idr)
unboundimps.idr:18:11--18:14:While processing type of len' at unboundimps.idr:18:1--19:1:
Undefined name xs
unboundimps.idr:19:16--19:18:While processing type of append' at unboundimps.idr:19:1--21:1:
Undefined name n
unboundimps.idr:18:11--18:13:While processing type of len' at unboundimps.idr:18:1--18:20:
Undefined name xs at:
18 len': Env xs -> Nat
^^
unboundimps.idr:19:16--19:17:While processing type of append' at unboundimps.idr:19:1--19:49:
Undefined name n at:
19 append' : Vect n a -> Vect m a -> Vect (n + m) a
^

6
tests/idris2/basic034/expected
View File

@ -1,7 +1,11 @@
1/1: Building lets (lets.idr)
lets.idr:22:39--23:14:While processing right hand side of dolet2 at lets.idr:21:1--26:1:
lets.idr:22:39--22:40:While processing right hand side of dolet2 at lets.idr:21:1--26:1:
When unifying Maybe Int and Maybe String
Mismatch between:
Int
and
String
at:
22 = do let Just x' : Maybe String = x
^

7
tests/idris2/coverage003/expected
View File

@ -1,6 +1,9 @@
1/1: Building Cover (Cover.idr)
Cover.idr:16:1--16:8:While processing left hand side of badBar at Cover.idr:16:1--17:1:
Can't match on 0 as it has a polymorphic type
Cover.idr:16:1--16:7:While processing left hand side of badBar at Cover.idr:16:1--17:1:
Can't match on 0 as it has a polymorphic type at:
16 badBar Z = Z
^^^^^^
Main> Main.foo:
foo (0, S _)
foo (S _, _)

7
tests/idris2/coverage004/expected
View File

@ -1,6 +1,9 @@
1/1: Building Cover (Cover.idr)
Cover.idr:14:1--14:5:While processing left hand side of bad at Cover.idr:14:1--15:1:
Can't match on Just (fromInteger 0) as it has a polymorphic type
Cover.idr:14:1--14:4:While processing left hand side of bad at Cover.idr:14:1--15:1:
Can't match on Just (fromInteger 0) as it has a polymorphic type at:
14 bad (Just 0) _ = False
^^^
Main> Main.okay:
okay (S _) IsNat
okay False IsBool

10
tests/idris2/coverage007/expected
View File

@ -1,3 +1,9 @@
1/1: Building eq (eq.idr)
eq.idr:27:1--29:1:badeq x y p is not a valid impossible case
eq.idr:30:1--31:1:badeqL xs ys p is not a valid impossible case
eq.idr:27:1--27:23:badeq x y p is not a valid impossible case at:
27 badeq x y p impossible
^^^^^^^^^^^^^^^^^^^^^^
eq.idr:30:1--30:26:badeqL xs ys p is not a valid impossible case at:
30 badeqL xs ys p impossible
^^^^^^^^^^^^^^^^^^^^^^^^^

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