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' into scratch-work-search-repl

Browse Source
This commit is contained in:
Mathew Polzin 2020-12-13 17:05:54 -08:00
commit a7e0df1300
135 changed files with 2199 additions and 811 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

10
CHANGELOG.md
View File

@ -17,6 +17,16 @@ Command-line options changes:
Compiler changes:
* Added new syntax for named applications and the bind-all-explicits pattern:
`f {x [= t], x [= t], ...}`
`f {x [= t], x [= t], ..., _}`
`f {}`
* Added new syntax for record updates:
`{x := t, x $= t, ...}`
* Added primitives to the parsing library used in the compiler to get more precise
boundaries to the AST nodes `FC`.
* New experimental ``refc`` code generator, which generates C with reference

59
CONTRIBUTORS
View File

@ -1,46 +1,47 @@
Thanks to the following for their help and contributions to Idris 2:
Abdelhakim Qbaich
Alex Gryzlov
Alex Silva
Andre Kuhlenschmidt
André Videla
Alex Gryzlov
Alex Silva
Andre Kuhlenschmidt
André Videla
Andy Lok
Anthony Lodi
Arnaud Bailly
Brian Wignall
Christian Rasmussen
David Smith
Edwin Brady
Arnaud Bailly
Brian Wignall
Christian Rasmussen
David Smith
Edwin Brady
Fabián Heredia Montiel
George Pollard
GhiOm
GhiOm
Guillaume Allais
Ilya Rezvov
Jan de Muijnck-Hughes
Ilya Rezvov
Jan de Muijnck-Hughes
Jeetu
Johann Rudloff
Kamil Shakirov
Kamil Shakirov
Bryn Keller
Kevin Boulain
LuoChen
Kevin Boulain
LuoChen
Marc Petit-Huguenin
MarcelineVQ
Marshall Bowers
Matthew Wilson
Matus Tejiscak
Michael Morgan
Milan Kral
Molly Miller
Mounir Boudia
Marshall Bowers
Matthew Wilson
Matus Tejiscak
Michael Morgan
Milan Kral
Molly Miller
Mounir Boudia
Nicolas Biri
Niklas Larsson
Ohad Kammar
Peter Hajdu
Niklas Larsson
Ohad Kammar
Peter Hajdu
Rohit Grover
Rui Barreiro
Simon Chatterjee
Ruslan Feizerahmanov
Simon Chatterjee
then0rTh
Theo Butler
Tim Süberkrüb
Timmy Jose
Theo Butler
Tim Süberkrüb
Timmy Jose

20
docs/source/backends/gambit.rst
View File

@ -66,3 +66,23 @@ Gambit Directives
.. code-block::
$ idris2 --codegen chez --directive extraRuntime=/path/to/extensions.scm -o main Main.idr
* ``--directive C``
Compile to C.
Gambit Environment Configurations
=================================
* ``GAMBIT_GSC_BACKEND``
The ``GAMBIT_GSC_BACKEND`` variable controls which C compiler Gambit will use during compilation. E.g. to use clang:
::
$ export GAMBIT_GSC_BACKEND=clang
Gambit after version v4.9.3 supports the ``-cc`` option, which configures
the compiler backend Gambit will use to build the binary. Currently to
get this functionality Gambit needs to be built from source, since it is
not yet available in a released version.

149
docs/source/backends/javascript.rst
View File

@ -44,8 +44,8 @@ For completion below an example of a foreign available only with ``browser`` cod
prim__setBodyInnerHTML : String -> PrimIO ()
Full Example
------------
Short Example
-------------
An interesting example is creating a foreign for the setTimeout function:
@ -59,3 +59,148 @@ An interesting example is creating a foreign for the setTimeout function:
An important note here is that the codegen is using ``BigInt`` to represent
idris ``Int``, that's why we need to apply ``Number`` to the ``delay``.
Browser Example
===============
To build JavaScript aimed to use in the browser, the code must be compiled with
the javascript codegen option. The compiler produces a JavaScript or an HTML file.
The browser needs an HTML file to load. This HTML file can be created in two ways
- If the ``.html`` suffix is given to the output file the compiler generates an HTML file
which includes a wrapping around the generated JavaScript.
- If *no* ``.html`` suffix is given, the generated file only contains the JavaScript code.
In this case manual wrapping is needed.
Example of the wrapper HTML:
.. code-block:: html
<html>
<head><meta charset='utf-8'></head>
<body>
<script type='text/javascript'>
JS code goes here
</script>
</body>
</html>
As our intention is to develop something that runs in the browser questions naturally arise:
- How to interact with HTML elements?
- More importantly, when does the generated Idris code start?
Starting point of the Idris generated code
------------------------------------------
The generated JavaScript for your program contains an entry point. The ``main`` function is compiled
to a JavaScript top-level expression, which will be evaluated during the loading of the ``script``
tag and that is the entry point for Idris generated program starting in the browser.
Interaction with HTML elements
------------------------------
As sketched in the Short Example section, the FFI must be used when interaction happens between Idris
generated code and the rest of the Browser/JS ecosystem. Information handled by the FFI is
separated into two categories. Primitive types in Idris FFI, such as Int, and everything else.
The everything else part is accessed via AnyPtr. The ``%foreign`` construction should be used
to give implementation on the JavaScript side. And an Idris function declaration to give ``Type``
declaration on the Idris side. The syntax is ``%foreign "browser:lambda:js-lambda-expression"`` .
On the Idris side, primitive types and ``PrimIO t`` types should be used as parameters,
when defining ``%foreign``. This declaration is a helper function which needs to be called
behind the ``primIO`` function. More on this can be found in the FFI chapter.
Examples for JavaScript FFI
---------------------------
console.log
-----------
.. code-block:: idris
%foreign "browser:lambda: x => console.log(x)"
prim__consoleLog : String -> PrimIO ()
consoleLog : HasIO io => String -> io ()
consoleLog x = primIO $ prim__consoleLog x
String is a primitive type in Idris and it is represented as a JavaScript String. There is no need
for any conversion between the Idris and the JavaScript.
setInterval
-----------
.. code-block:: idris
%foreign "browser:lambda: (a,i)=>setInterval(a,Number(i))"
prim__setInterval : PrimIO () -> Int -> PrimIO ()
setInterval : (HasIO io) => IO () -> Int -> io ()
setInterval a i = primIO $ prim__setInterval (toPrim a) i
The ``setInterval`` JavaScript function executes the given function in every ``x`` millisecond.
We can use Idris generated functions in the callback as far as they have the type ``IO ()`` .
But there is a difference in the parameter for the time interval. On the JavaScript side it
expects a number, meanwhile ``Int`` in Idris is represented as a ``BigInt`` in JavaScript,
for that reason the implementation of the ``%foreign`` needs to make the conversion.
HTML Dom elements
-----------------
Lets turn our attention to the Dom elements and events. As said above, anything that is not a
primitive type should be handled via the ``AnyPtr`` type in the FFI. Anything complex that is
returned by a JavaScript function should be captured in an ``AnyPtr`` value. It is advisory to
separate the ``AnyPtr`` values into categories.
.. code-block:: idris
data DomNode = MkNode AnyPtr
%foreign "browser:lambda: () => document.body"
prim__body : () -> PrimIO AnyPtr
body : HasIO io => io DomNode
body = map MkNode $ primIO $ prim__body ()
We create a ``DomNode`` type which holds an ``AnyPtr``. The ``prim__body`` function wraps a
lambda function with no parameters. In the Idris function ``body`` we pass an extra ``()`` parameter
and the we wrap the result in the ``DomNode`` type using the ``MkNode`` data constructor.
Primitive values originated in JavaScript
-----------------------------------------
As a countinuation of the previous example, the ``width`` attribute of a DOM element can be
retrieved via the FFI.
.. code-block:: idris
%foreign "browser:lambda: n=>(BigInt(n.width))"
prim__width : AnyPtr -> PrimIO Int
width : HasIO io => DomNode -> io Int
width (MkNode p) = primIO $ prim__width p
Note the ``BigInt`` conversation from the JavaScript. The ``n.width`` returns a JavaScript
``Number`` and the corresponding ``Int`` of Idris is repersented as a ``BigInt`` in JavaScript.
The implementor of the FFI function must keep these conversions in mind.
Handling JavaScript events
--------------------------
.. code-block:: idris
data DomEvent = MkEvent AnyPtr
%foreign "browser:lambda: (event, callback, node) => node.addEventListener(event, x=>callback(x)())"
prim__addEventListener : String -> (AnyPtr -> PrimIO ()) -> AnyPtr -> PrimIO ()
addEventListener : HasIO io => String -> DomNode -> (DomEvent -> IO ()) -> io ()
addEventListener event (MkNode n) callback =
primIO $ prim__addEventListener event (\ptr => toPrim $ callback $ MkEvent ptr) n
In this example shows how to attach an event handler to a particular DOM element. Values of events
are also associated with ``AnyPtr`` on the Idris side. To seperate ``DomNode`` form ``DomEvent``
we create two different types. Also it demonstrates how a simple callback function defined in
Idris can be used on the JavaScript side.

125
docs/source/reference/literate.rst
View File

@ -9,6 +9,7 @@ Idris2 supports several types of literate mode styles.
The unlit'n has been designed based such that we assume that we are parsing markdown-like languages
The unlit'n is performed by a Lexer that uses a provided literate style to recognise code blocks and code lines.
Anything else is ignored.
Idris2 also provides support for recognising both 'visible' and 'invisible' code blocks using 'native features' of each literate style.
A literate style consists of:
@ -25,35 +26,133 @@ But more importantly, a more intelligent processing of literate documents using
Bird Style Literate Files
=========================
Bird notation is a classic literate mode found in Haskell, (and Orwell) in which code lines begin with ``>``.
We treat files with an extension of ``.lidr`` as bird style literate files.
Bird notation is a classic literate mode found in Haskell, (and Orwell) in which visible code lines begin with ``>`` and hidden lines with ``<``.
Other lines are treated as documentation.
We treat files with an extension of ``.lidr`` as bird style literate files.
.. note::
We have diverged from ``lhs2tex`` in which ``<`` is traditionally used to display inactive code.
Bird-style is presented as is, and we recommended use of the other styles for much more comprehensive literate mode.
Embedding in Markdown-like documents
====================================
While Bird Style literate mode is useful, it does not lend itself well
to more modern markdown-like notations such as Org-Mode and CommonMark.
Idris2 also provides support for recognising both 'visible' and 'invisible'
code blocks and lines in both CommonMark and OrgMode documents.
code blocks and lines in both CommonMark and OrgMode documents using native code blocks and lines..
'Visible' content will be kept in the pretty printer's output while
the 'invisible' blocks and lines will be removed.
The idea being is that:
1. **Visible** content will be kept in the pretty printer's output;
2. **Invisible** content will be removed; and
3. **Specifications** will be displayed *as is* and not touched by the compiler.
OrgMode
*******
+ Org mode source blocks for idris are recognised as visible code blocks,
+ Comment blocks that begin with ``#+COMMENT: idris`` are treated as invisible code blocks.
+ Invisible code lines are denoted with ``#+IDRIS:``.
We treat files with an extension of ``.org`` as org-style literate files.
Each of the following markup is recognised regardless of case:
We treat files with an extension of ``.org`` as org-mode style literate files.
+ Org mode source blocks for idris sans options are recognised as visible code blocks::
#+begin_src idris
data Nat = Z | S Nat
#+end_src
+ Comment blocks that begin with ``#+BEGIN_COMMENT idris`` are treated as invisible code blocks::
#+begin_comment idris
data Nat = Z | S Nat
#+end_comment
+ Visible code lines, and specifications, are not supported. Invisible code lines are denoted with ``#+IDRIS:``::
#+IDRIS: data Nat = Z | S Nat
+ Specifications can be given using OrgModes plain source or example blocks::
#+begin_src
map : (f : a -> b)
-> List a
-> List b
map f _ = Nil
#+end_src
CommonMark
************
Only code blocks denoted by standard code blocks labelled as idris are recognised.
**********
We treat files with an extension of ``.md`` and ``.markdown`` as CommonMark style literate files.
+ CommonMark source blocks for idris sans options are recognised as visible code blocks::
```idris
data Nat = Z | S Nat
```
~~~idris
data Nat = Z | S Nat
~~~
+ Comment blocks of the form ``<!-- idris\n ... \n -->`` are treated as invisible code blocks::
<!-- idris
data Nat = Z | S Nat
-->
+ Code lines are not supported.
+ Specifications can be given using CommonMark's pre-formatted blocks (indented by four spaces) or unlabelled code blocks.::
Compare
```
map : (f : a -> b)
-> List a
-> List b
map f _ = Nil
```
with
map : (f : a -> b)
-> List a
-> List b
map f _ = Nil
LaTeX
*****
We treat files with an extension of ``.tex`` and ``.ltx`` as LaTeX style literate files.
+ We treat environments named ``code`` as visible code blocks::
\begin{code}
data Nat = Z | S Nat
\end{code}
+ We treat environments named ``hidden`` as invisible code blocks::
\begin{hidden}
data Nat = Z | S Nat
\end{hidden}
+ Code lines are not supported.
+ Specifications can be given using user defined environments.
We do not provide definitions for these code blocks and ask the user to define them.
With one such example using ``fancyverbatim`` and ``comment`` packages as::
\usepackage{fancyvrb}
\DefineVerbatimEnvironment
{code}{Verbatim}
{}
\usepackage{comment}
\excludecomment{hidden}

55
docs/source/tutorial/interfaces.rst
View File

@ -177,6 +177,50 @@ interface declaration, it elaborates the interface header but none of the
method types on the first pass, and elaborates the method types and any
default definitions on the second pass.
Quantities for Parameters
=========================
By default parameters that are not explicitly ascribed a type in an ``interface``
declaration are assigned the quantity ``0``. This means that the parameter is not
available to use at runtime in the methods' definitions.
For instance, ``Show a`` gives rise to a ``0``-quantified type variable ``a`` in
the type of the ``show`` method:
::
Main> :set showimplicits
Main> :t show
Prelude.show : {0 a : Type} -> Show a => a -> String
However some use cases require that some of the parameters are available at runtime.
We may for instance want to declare an interface for ``Storable`` types. The constraint
``Storable a size`` means that we can store values of type ``a`` in a ``Buffer`` in
exactly ``size`` bytes.
If the user provides a method to read a value for such a type ``a`` at a given offset,
then we can read the ``k``th element stored in the buffer by computing the appropriate
offset from ``k`` and ``size``. This is demonstrated by providing a default implementation
for the method ``peekElementOff`` implemented in terms of ``peekByteOff`` and the parameter
``size``.
.. code-block:: idris
data ForeignPtr : Type -> Type where
MkFP : Buffer -> ForeignPtr a
interface Storable (0 a : Type) (size : Nat) | a where
peekByteOff : HasIO io => ForeignPtr a -> Int -> io a
peekElemOff : HasIO io => ForeignPtr a -> Int -> io a
peekElemOff fp k = peekByteOff fp (k * cast size)
Note that ``a`` is explicitly marked as runtime irrelevant so that it is erased by the
compiler. Equivalently we could have written ``interface Sotrable a (size : Nat)``.
The meaning of ``| a`` is explained in :ref:`DeterminingParameters`.
Functors and Applicatives
=========================
@ -189,9 +233,10 @@ prelude:
.. code-block:: idris
interface Functor (f : Type -> Type) where
interface Functor (0 f : Type -> Type) where
map : (m : a -> b) -> f a -> f b
A functor allows a function to be applied across a structure, for
example to apply a function to every element in a ``List``:
@ -213,7 +258,7 @@ abstracts the notion of function application:
infixl 2 <*>
interface Functor f => Applicative (f : Type -> Type) where
interface Functor f => Applicative (0 f : Type -> Type) where
pure : a -> f a
(<*>) : f (a -> b) -> f a -> f b
@ -410,7 +455,7 @@ has an implementation of both ``Monad`` and ``Alternative``:
.. code-block:: idris
interface Applicative f => Alternative (f : Type -> Type) where
interface Applicative f => Alternative (0 f : Type -> Type) where
empty : f a
(<|>) : f a -> f a -> f a
@ -670,6 +715,8 @@ do this with a ``using`` clause in the implementation as follows:
The ``using PlusNatSemi`` clause indicates that ``PlusNatMonoid`` should
extend ``PlusNatSemi`` specifically.
.. _DeterminingParameters:
Determining Parameters
======================
@ -678,7 +725,7 @@ parameters used to find an implementation are restricted. For example:
.. code-block:: idris
interface Monad m => MonadState s (m : Type -> Type) | m where
interface Monad m => MonadState s (0 m : Type -> Type) | m where
get : m s
put : s -> m ()

160
docs/source/updates/updates.rst
View File

@ -579,6 +579,149 @@ Idris 1 took a different approach here: names which were parameters to data
types were in scope, other names were not. The Idris 2 approach is, we hope,
more consistent and easier to understand.
.. _sect-app-syntax-additions:
Function application syntax additions
-------------------------------------
From now on you can utilise the new syntax of function applications:
.. code-block:: idris
f {x1 [= e1], x2 [= e2], ...}
There are three additions here:
1. More than one argument can be written in braces, separated with commas:
.. code-block:: idris
record Dog where
constructor MkDog
name : String
age : Nat
-- Notice that `name` and `age` are explicit arguments.
-- See paragraph (2)
haveADog : Dog
haveADog = MkDog {name = "Max", age = 3}
pairOfStringAndNat : (String, Nat)
pairOfStringAndNat = MkPair {x = "year", y = 2020}
myPlus : (n : Nat) -> (k : Nat) -> Nat
myPlus {n = Z , k} = k
myPlus {n = S n', k} = S (myPlus n' k)
twoPlusTwoIsFour : myPlus {n = 2, k = 2} === 4
twoPlusTwoIsFour = Refl
2. Arguments in braces can now correspond to explicit, implicit and auto implicit
dependent function types (``Pi`` types), provided the domain type is named:
.. code-block:: idris
myPointlessFunction : (exp : String) -> {imp : String} -> {auto aut : String} -> String
myPointlessFunction exp = exp ++ imp ++ aut
callIt : String
callIt = myPointlessFunction {imp = "a ", exp = "Just ", aut = "test"}
Order of the arguments doesn't matter as long as they are in braces and the names are distinct.
It is better to stick named arguments in braces at the end of your argument list, because
regular unnamed explicit arguments are processed first and take priority:
.. code-block:: idris
myPointlessFunction' : (a : String) -> String -> (c : String) -> String
myPointlessFunction' a b c = a ++ b ++ c
badCall : String
badCall = myPointlessFunction' {a = "a", c = "c"} "b"
This snippet won't type check, because "b" in ``badCall`` is passed first,
although logically we want it to be second.
Idris will tell you that it couldn't find a spot for ``a = "a"`` (because "b" took its place),
so the application is ill-formed.
Thus if you want to use the new syntax, it is worth naming your ``Pi`` types.
3. Multiple explicit arguments can be "skipped" more easily with the following syntax:
.. code-block:: idris
f {x1 [= e1], x2 [= e2], ..., xn [= en], _}
or
.. code-block:: idris
f {}
in case none of the named arguments are wanted.
Examples:
.. code-block:: idris
import Data.Nat
record Four a b c d where
constructor MkFour
x : a
y : b
z : c
w : d
firstTwo : Four a b c d -> (a, b)
firstTwo $ MkFour {x, y, _} = (x, y)
-- firstTwo $ MkFour {x, y, z = _, w = _} = (x, y)
dontCare : (x : Nat) -> Nat -> Nat -> Nat -> (y : Nat) -> x + y = y + x
dontCare {} = plusCommutative {}
--dontCare _ _ _ _ _ = plusCommutative _ _
Last rule worth noting is the case of named applications with repeated argument names, e.g:
.. code-block:: idris
data WeirdPair : Type -> Type -> Type where
MkWeirdPair : (x : a) -> (x : b) -> WeirdPair a b
weirdSnd : WeirdPair a b -> b
--weirdSnd $ MkWeirdPair {x, x} = x
-- ^
-- Error: "Non linear pattern variable"
-- But that one is okay:
weirdSnd $ MkWeirdPair {x = _, x} = x
In this example the name ``x`` is given repeatedly to the ``Pi`` types of the data constructor ``MkWeirdPair``.
In order to deconstruct the ``WeirdPair a b`` in ``weirdSnd``, while writing the left-hand side of the pattern-matching clause
in a named manner (via the new syntax), we have to rename the first occurrence of ``x`` to any fresh name or the ``_`` as we did.
Then the definition type checks normally.
In general, duplicate names are bound sequentially on the left-hand side and must be renamed for the pattern expression to be valid.
The situation is similar on the right-hand side of pattern-matching clauses:
.. code-block:: idris
0 TypeOf : a -> Type
TypeOf _ = a
weirdId : {0 a : Type} -> (1 a : a) -> TypeOf a
weirdId a = a
zero : Nat
-- zero = weirdId { a = Z }
-- ^
-- Error: "Mismatch between: Nat and Type"
-- But this works:
zero = weirdId { a = Nat, a = Z }
Named arguments should be passed sequentially in the order they were defined in the ``Pi`` types,
regardless of their (imp)explicitness.
Better inference
----------------
@ -656,6 +799,23 @@ correspondingly:
addEntry val = record { length $= S,
content $= (val :: ) }
Another novelty - new update syntax (previous one still functional):
.. code-block:: idris
record Three a b c where
constructor MkThree
x : a
y : b
z : c
-- Yet another contrived example
mapSetMap : Three a b c -> (a -> a') -> b' -> (c -> c') -> Three a' b' c'
mapSetMap three@(MkThree x y z) f y' g = {x $= f, y := y', z $= g} three
The ``record`` keyword has been discarded for brevity, symbol ``:=`` replaces ``=``
in order to not introduce any ambiguity.
Generate definition
-------------------

1
idris2api.ipkg
View File

@ -71,6 +71,7 @@ modules =
Data.Bool.Extra,
Data.List.Extra,
Data.DList,
IdrisPaths,

2
libs/base/Control/Monad/Either.idr
View File

@ -112,6 +112,8 @@ Foldable m => Foldable (EitherT e m) where
foldr f acc (MkEitherT e)
= foldr (\x,xs => either (const acc) (`f` xs) x) acc e
null (MkEitherT e) = null e
public export
Traversable m => Traversable (EitherT e m) where
traverse f (MkEitherT x)

2
libs/base/Control/Monad/Reader.idr
View File

@ -5,7 +5,7 @@ import Control.Monad.Trans
||| A computation which runs in a static context and produces an output
public export
interface Monad m => MonadReader stateType (m : Type -> Type) | m where
interface Monad m => MonadReader stateType m | m where
||| Get the context
ask : m stateType

2
libs/base/Control/Monad/State.idr
View File

@ -5,7 +5,7 @@ import public Control.Monad.Trans
||| A computation which runs in a context and produces an output
public export
interface Monad m => MonadState stateType (m : Type -> Type) | m where
interface Monad m => MonadState stateType m | m where
||| Get the context
get : m stateType
||| Write a new context/output

3
libs/base/Control/Monad/Trans.idr
View File

@ -1,6 +1,5 @@
module Control.Monad.Trans
public export
interface MonadTrans (t : (Type -> Type) -> Type -> Type) where
interface MonadTrans t where
lift : Monad m => m a -> t m a

6
libs/base/Control/WellFounded.idr
View File

@ -9,7 +9,7 @@ data Accessible : (rel : a -> a -> Type) -> (x : a) -> Type where
Accessible rel x
public export
interface WellFounded (rel : a -> a -> Type) where
interface WellFounded a rel where
wellFounded : (x : a) -> Accessible rel x
export
@ -27,13 +27,13 @@ accInd step z (Access f) =
step z $ \y, lt => accInd step y (f y lt)
export
wfRec : WellFounded rel =>
wfRec : WellFounded a rel =>
(step : (x : a) -> ((y : a) -> rel y x -> b) -> b) ->
a -> b
wfRec step x = accRec step x (wellFounded {rel} x)
export
wfInd : WellFounded rel => {0 P : a -> Type} ->
wfInd : WellFounded a rel => {0 P : a -> Type} ->
(step : (x : a) -> ((y : a) -> rel y x -> P y) -> P x) ->
(myz : a) -> P myz
wfInd step myz = accInd step myz (wellFounded {rel} myz)

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

@ -2,7 +2,7 @@ module Data.Fin
import public Data.Maybe
import Data.Nat
import Decidable.Equality
import Decidable.Equality.Core
%default total

4
libs/base/Data/Fin/Order.idr
View File

@ -11,7 +11,7 @@ import Decidable.Order
using (k : Nat)
data FinLTE : Fin k -> Fin k -> Type where
FromNatPrf : {m : Fin k} -> {n : Fin k} -> LTE (finToNat m) (finToNat n) -> FinLTE m n
FromNatPrf : {m, n : Fin k} -> LTE (finToNat m) (finToNat n) -> FinLTE m n
implementation Preorder (Fin k) FinLTE where
transitive m n o (FromNatPrf p1) (FromNatPrf p2) =
@ -22,7 +22,7 @@ using (k : Nat)
antisymmetric m n (FromNatPrf p1) (FromNatPrf p2) =
finToNatInjective m n (LTEIsAntisymmetric (finToNat m) (finToNat n) p1 p2)
implementation Decidable [Fin k, Fin k] FinLTE where
implementation Decidable 2 [Fin k, Fin k] FinLTE where
decide m n with (decideLTE (finToNat m) (finToNat n))
decide m n | Yes prf = Yes (FromNatPrf prf)
decide m n | No disprf = No (\ (FromNatPrf prf) => disprf prf)

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

@ -2,6 +2,7 @@ module Data.List
import Data.Nat
import Data.List1
import Data.Fin
public export
isNil : List a -> Bool
@ -58,10 +59,15 @@ inBounds (S k) (x :: xs) with (inBounds k xs)
|||
||| @ ok a proof that the index is within bounds
public export
index : (n : Nat) -> (xs : List a) -> {auto ok : InBounds n xs} -> a
index : (n : Nat) -> (xs : List a) -> {auto 0 ok : InBounds n xs} -> a
index Z (x :: xs) {ok = InFirst} = x
index (S k) (_ :: xs) {ok = InLater _} = index k xs
public export
index' : (xs : List a) -> Fin (length xs) -> a
index' (x::_) FZ = x
index' (_::xs) (FS i) = index' xs i
||| Generate a list by repeatedly applying a partial function until exhausted.
||| @ f the function to iterate
||| @ x the initial value that will be the head of the list

1
libs/base/Data/List1.idr
View File

@ -117,6 +117,7 @@ Monad List1 where
export
Foldable List1 where
foldr c n (x ::: xs) = c x (foldr c n xs)
null _ = False
export
Show a => Show (List1 a) where

2
libs/base/Data/Nat/Order.idr
View File

@ -62,7 +62,7 @@ decideLTE (S x) (S y) with (decEq (S x) (S y))
decideLTE (S x) (S y) | No _ | No nGTm = No (ltesuccinjective nGTm)
public export
implementation Decidable [Nat,Nat] LTE where
implementation Decidable 2 [Nat,Nat] LTE where
decide = decideLTE
public export

6
libs/base/Data/Ref.idr
View File

@ -4,9 +4,9 @@ import public Data.IORef
import public Control.Monad.ST
public export
interface Ref m (r : Type -> Type) | m where
newRef : a -> m (r a)
readRef : r a -> m a
interface Ref m r | m where
newRef : {0 a : Type} -> a -> m (r a)
readRef : {0 a : Type} -> r a -> m a
writeRef : r a -> a -> m ()
export

1
libs/base/Data/Strings.idr
View File

@ -20,6 +20,7 @@ foldl1 f (x::xs) = foldl f x xs
-- If you need to unpack strings at compile time, use Prelude.unpack.
%foreign
"scheme:string-unpack"
"javascript:lambda:(str)=>__prim_js2idris_array(Array.from(str))"
export
fastUnpack : String -> List Char

3
libs/base/Data/Vect.idr
View File

@ -407,6 +407,9 @@ public export
implementation Foldable (Vect n) where
foldr f e xs = foldrImpl f e id xs
null [] = True
null _ = False
--------------------------------------------------------------------------------
-- Special folds
--------------------------------------------------------------------------------

8
libs/base/Decidable/Decidable.idr
View File

@ -3,16 +3,14 @@ module Decidable.Decidable
import Data.Rel
import Data.Fun
||| Interface for decidable n-ary Relations
public export
interface Decidable (ts : Vect k Type) (p : Rel ts) where
total decide : liftRel ts p Dec
interface Decidable k ts p where
total decide : liftRel (the (Vect k Type) ts) (the (Rel ts) p) Dec
||| Given a `Decidable` n-ary relation, provides a decision procedure for
||| this relation.
decision : (ts : Vect k Type) -> (p : Rel ts) -> (Decidable ts p) => liftRel ts p Dec
decision : (ts : Vect k Type) -> (p : Rel ts) -> (Decidable k ts p) => liftRel ts p Dec
decision ts p = decide {ts} {p}
using (a : Type, x : a)

28
libs/base/Decidable/Equality.idr
View File

@ -6,34 +6,10 @@ import Data.Nat
import Data.List
import Data.List1
import public Decidable.Equality.Core as Decidable.Equality
%default total
--------------------------------------------------------------------------------
-- Decidable equality
--------------------------------------------------------------------------------
||| Decision procedures for propositional equality
public export
interface DecEq t where
||| Decide whether two elements of `t` are propositionally equal
decEq : (x1 : t) -> (x2 : t) -> Dec (x1 = x2)
--------------------------------------------------------------------------------
-- Utility lemmas
--------------------------------------------------------------------------------
||| The negation of equality is symmetric (follows from symmetry of equality)
export
negEqSym : forall a, b . (a = b -> Void) -> (b = a -> Void)
negEqSym p h = p (sym h)
||| Everything is decidably equal to itself
export
decEqSelfIsYes : DecEq a => {x : a} -> decEq x x = Yes Refl
decEqSelfIsYes {x} with (decEq x x)
decEqSelfIsYes {x} | Yes Refl = Refl
decEqSelfIsYes {x} | No contra = absurd $ contra Refl
--------------------------------------------------------------------------------
--- Unit
--------------------------------------------------------------------------------

29
libs/base/Decidable/Equality/Core.idr Normal file
View File

@ -0,0 +1,29 @@
module Decidable.Equality.Core
%default total
--------------------------------------------------------------------------------
-- Decidable equality
--------------------------------------------------------------------------------
||| Decision procedures for propositional equality
public export
interface DecEq t where
||| Decide whether two elements of `t` are propositionally equal
decEq : (x1 : t) -> (x2 : t) -> Dec (x1 = x2)
--------------------------------------------------------------------------------
-- Utility lemmas
--------------------------------------------------------------------------------
||| The negation of equality is symmetric (follows from symmetry of equality)
export
negEqSym : forall a, b . (a = b -> Void) -> (b = a -> Void)
negEqSym p h = p (sym h)
||| Everything is decidably equal to itself
export
decEqSelfIsYes : DecEq a => {x : a} -> decEq x x = Yes Refl
decEqSelfIsYes {x} with (decEq x x)
decEqSelfIsYes {x} | Yes Refl = Refl
decEqSelfIsYes {x} | No contra = absurd $ contra Refl

23
libs/base/Decidable/Order.idr
View File

@ -17,28 +17,25 @@ import Data.Rel
--------------------------------------------------------------------------------
public export
interface Preorder t (po : t -> t -> Type) where
total transitive : (a : t) -> (b : t) -> (c : t) -> po a b -> po b c -> po a c
interface Preorder t po where
total transitive : (a, b, c : t) -> po a b -> po b c -> po a c
total reflexive : (a : t) -> po a a
public export
interface (Preorder t po) => Poset t (po : t -> t -> Type) where
total antisymmetric : (a : t) -> (b : t) -> po a b -> po b a -> a = b
interface (Preorder t po) => Poset t po where
total antisymmetric : (a, b : t) -> po a b -> po b a -> a = b
public export
interface (Poset t to) => Ordered t (to : t -> t -> Type) where
total order : (a : t) -> (b : t) -> Either (to a b) (to b a)
interface (Poset t to) => Ordered t to where
total order : (a, b : t) -> Either (to a b) (to b a)
public export
interface (Preorder t eq) => Equivalence t (eq : t -> t -> Type) where
total symmetric : (a : t) -> (b : t) -> eq a b -> eq b a
interface (Preorder t eq) => Equivalence t eq where
total symmetric : (a, b : t) -> eq a b -> eq b a
public export
interface (Equivalence t eq) => Congruence t (f : t -> t) (eq : t -> t -> Type) where
total congruent : (a : t) ->
(b : t) ->
eq a b ->
eq (f a) (f b)
interface (Equivalence t eq) => Congruence t f eq where
total congruent : (a, b : t) -> eq a b -> eq (f a) (f b)
public export
minimum : (Ordered t to) => t -> t -> t

5
libs/base/Language/Reflection/TTImp.idr
View File

@ -36,7 +36,8 @@ mutual
IUpdate : FC -> List IFieldUpdate -> TTImp -> TTImp
IApp : FC -> TTImp -> TTImp -> TTImp
IImplicitApp : FC -> TTImp -> Maybe Name -> TTImp -> TTImp
INamedApp : FC -> TTImp -> Name -> TTImp -> TTImp
IAutoApp : FC -> TTImp -> TTImp -> TTImp
IWithApp : FC -> TTImp -> TTImp -> TTImp
ISearch : FC -> (depth : Nat) -> TTImp
@ -100,7 +101,7 @@ mutual
ForeignFn : List TTImp -> FnOpt
-- assume safe to cancel arguments in unification
Invertible : FnOpt
Totalty : TotalReq -> FnOpt
Totality : TotalReq -> FnOpt
Macro : FnOpt
SpecArgs : List Name -> FnOpt

1
libs/base/base.ipkg
View File

@ -49,6 +49,7 @@ modules = Control.App,
Decidable.Decidable,
Decidable.Equality,
Decidable.Equality.Core,
Decidable.Order,
Language.Reflection,

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

@ -99,8 +99,8 @@ public export
decEq (x :: xs) (y :: ys) | No contra = No (contra . consInjective1)
public export
interface Shows (k : Nat) (ts : Vect k Type) where
shows : HVect ts -> Vect k String
interface Shows k ts where
shows : HVect {k} ts -> Vect k String
public export
Shows Z [] where

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

@ -254,11 +254,6 @@ export
values : SortedMap k v -> List v
values = map snd . toList
export
null : SortedMap k v -> Bool
null Empty = True
null (M _ _) = False
treeMap : (a -> b) -> Tree n k a o -> Tree n k b o
treeMap f (Leaf k v) = Leaf k (f v)
treeMap f (Branch2 t1 k t2) = Branch2 (treeMap f t1) k (treeMap f t2)
@ -289,6 +284,9 @@ export
implementation Foldable (SortedMap k) where
foldr f z = foldr f z . values
null Empty = True
null (M _ _) = False
export
implementation Traversable (SortedMap k) where
traverse _ Empty = pure Empty

6
libs/contrib/Data/SortedSet.idr
View File

@ -34,6 +34,8 @@ export
Foldable SortedSet where
foldr f e xs = foldr f e (Data.SortedSet.toList xs)
null (SetWrapper m) = null m
||| Set union. Inserts all elements of x into y
export
union : (x, y : SortedSet k) -> SortedSet k
@ -69,7 +71,3 @@ keySet = SetWrapper . map (const ())
export
singleton : Ord k => k -> SortedSet k
singleton k = insert k empty
export
null : SortedSet k -> Bool
null (SetWrapper m) = SortedMap.null m

27
libs/contrib/Decidable/Decidable/Extra.idr
View File

@ -9,26 +9,26 @@ import Decidable.Decidable
public export
NotNot : {n : Nat} -> {ts : Vect n Type} -> (r : Rel ts) -> Rel ts
NotNot r = map @{Nary} (Not . Not) r
NotNot r = map @{Nary} (Not . Not) r
[DecidablePartialApplication] {x : t} -> (tts : Decidable (t :: ts) r) => Decidable ts (r x) where
[DecidablePartialApplication] {x : t} -> (tts : Decidable (S n) (t :: ts) r) => Decidable n ts (r x) where
decide = decide @{tts} x
public export
doubleNegationElimination : {n : Nat} -> {0 ts : Vect n Type} -> {r : Rel ts} -> Decidable ts r =>
(witness : HVect ts) ->
uncurry (NotNot {ts} r) witness ->
doubleNegationElimination : {n : Nat} -> {0 ts : Vect n Type} -> {r : Rel ts} -> Decidable n ts r =>
(witness : HVect ts) ->
uncurry (NotNot {ts} r) witness ->
uncurry r witness
doubleNegationElimination {ts = [] } @{dec} [] prfnn =
doubleNegationElimination {ts = [] } @{dec} [] prfnn =
case decide @{dec} of
Yes prf => prf
No prfn => absurd $ prfnn prfn
doubleNegationElimination {ts = t :: ts} @{dec} (w :: witness) prfnn =
doubleNegationElimination {ts = t :: ts} @{dec} (w :: witness) prfnn =
doubleNegationElimination {ts} {r = r w} @{ DecidablePartialApplication @{dec} } witness prfnn
doubleNegationForall : {n : Nat} -> {0 ts : Vect n Type} -> {r : Rel ts} -> Decidable ts r =>
doubleNegationForall : {n : Nat} -> {0 ts : Vect n Type} -> {r : Rel ts} -> Decidable n ts r =>
All ts (NotNot {ts} r) -> All ts r
doubleNegationForall @{dec} forall_prf =
doubleNegationForall @{dec} forall_prf =
let prfnn : (witness : HVect ts) -> uncurry (NotNot {ts} r) witness
prfnn = uncurryAll forall_prf
prf : (witness : HVect ts) -> uncurry r witness
@ -36,15 +36,14 @@ doubleNegationForall @{dec} forall_prf =
in curryAll prf
public export
doubleNegationExists : {n : Nat} -> {0 ts : Vect n Type} -> {r : Rel ts} -> Decidable ts r =>
Ex ts (NotNot {ts} r) ->
doubleNegationExists : {n : Nat} -> {0 ts : Vect n Type} -> {r : Rel ts} -> Decidable n ts r =>
Ex ts (NotNot {ts} r) ->
Ex ts r
doubleNegationExists {ts} {r} @{dec} nnxs =
doubleNegationExists {ts} {r} @{dec} nnxs =
let witness : HVect ts
witness = extractWitness nnxs
witness = extractWitness nnxs
witnessingnn : uncurry (NotNot {ts} r) witness
witnessingnn = extractWitnessCorrect nnxs
witnessing : uncurry r witness
witnessing = doubleNegationElimination @{dec} witness witnessingnn
in introduceWitness witness witnessing

21
libs/contrib/Decidable/Order/Strict.idr
View File

@ -12,13 +12,13 @@ import Decidable.Equality
%default total
public export
interface StrictPreorder t (spo : t -> t -> Type) where
interface StrictPreorder t spo where
transitive : (a, b, c : t) -> a `spo` b -> b `spo` c -> a `spo` c
irreflexive : (a : t) -> Not (a `spo` a)
public export
asymmetric : StrictPreorder t spo => (a, b : t) -> a `spo` b -> Not (b `spo` a)
asymmetric a b aLTb bLTa = irreflexive a $
asymmetric a b aLTb bLTa = irreflexive a $
Strict.transitive a b a aLTb bLTa
public export
@ -35,10 +35,10 @@ public export
[MkPoset] {antisym : (a,b : t) -> a `leq` b -> b `leq` a -> a = b} -> Preorder t leq => Poset t leq where
antisymmetric = antisym
%hint
public export
InferPoset : {t : Type} -> {spo : t -> t -> Type} -> StrictPreorder t spo => Poset t (EqOr spo)
InferPoset : {t : Type} -> {spo : t -> t -> Type} -> StrictPreorder t spo => Poset t (EqOr spo)
InferPoset {t} {spo} = MkPoset @{MkPreorder} {antisym = antisym}
where
antisym : (a,b : t) -> EqOr spo a b -> EqOr spo b a -> a = b
@ -51,11 +51,11 @@ public export
data DecOrdering : {lt : t -> t -> Type} -> (a,b : t) -> Type where
DecLT : forall lt . (a `lt` b) -> DecOrdering {lt = lt} a b
DecEQ : forall lt . (a = b) -> DecOrdering {lt = lt} a b
DecGT : forall lt . (b `lt` a) -> DecOrdering {lt = lt} a b
DecGT : forall lt . (b `lt` a) -> DecOrdering {lt = lt} a b
public export
interface StrictPreorder t spo => StrictOrdered t (spo : t -> t -> Type) where
order : (a,b : t) -> DecOrdering {lt = spo} a b
interface StrictPreorder t spo => StrictOrdered t spo where
order : (a,b : t) -> DecOrdering {lt = spo} a b
[MkOrdered] {ord : (a,b : t) -> Either (a `leq` b) (b `leq` a)} -> Poset t leq => Ordered t leq where
order = ord
@ -76,9 +76,8 @@ public export
(tot : StrictOrdered t lt) => (pre : StrictPreorder t lt) => DecEq t where
decEq x y = case order @{tot} x y of
DecEQ x_eq_y => Yes x_eq_y
DecLT xlty => No $ \x_eq_y => absurd $ irreflexive @{pre} y
DecLT xlty => No $ \x_eq_y => absurd $ irreflexive @{pre} y
$ replace {p = \u => u `lt` y} x_eq_y xlty
-- Similarly
-- Similarly
DecGT yltx => No $ \x_eq_y => absurd $ irreflexive @{pre} y
$ replace {p = \u => y `lt` u} x_eq_y yltx

43
libs/contrib/System/Future.idr Normal file
View File

@ -0,0 +1,43 @@
module System.Future
%default total
-- Futures based Concurrency and Parallelism
export
data Future : Type -> Type where [external]
%extern prim__makeFuture : {0 a : Type} -> Lazy a -> Future a
%foreign "racket:blodwen-await-future"
"scheme:blodwen-await-future"
prim__awaitFuture : {0 a : Type} -> Future a -> a
export
fork : Lazy a -> Future a
fork = prim__makeFuture
export
await : Future a -> a
await f = prim__awaitFuture f
public export
Functor Future where
map func future = fork $ func (await future)
public export
Applicative Future where
pure v = fork v
funcF <*> v = fork $ (await funcF) (await v)
public export
Monad Future where
join = map await
v >>= func = join . fork $ func (await v)
export
performFutureIO : HasIO io => Future (IO a) -> io (Future a)
performFutureIO = primIO . prim__io_pure . map unsafePerformIO
export
forkIO : HasIO io => IO a -> io (Future a)
forkIO a = performFutureIO $ fork a

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

@ -16,7 +16,7 @@ module Text.Token
||| tokValue SKComma x = ()
||| ```
public export
interface TokenKind (k : Type) where
interface TokenKind k where
||| The type that a token of this kind converts to.
TokType : k -> Type

1
libs/contrib/contrib.ipkg
View File

@ -98,6 +98,7 @@ modules = Control.ANSI,
Text.PrettyPrint.Prettyprinter.Render.String,
Text.PrettyPrint.Prettyprinter.Render.Terminal,
System.Future,
System.Random,
System.Path,
Syntax.WithProof,

9
libs/prelude/Builtin.idr
View File

@ -182,6 +182,15 @@ public export
believe_me : a -> b
believe_me = prim__believe_me _ _
||| Assert to the usage checker that the given function uses its argument linearly.
public export
assert_linear : (1 f : a -> b) -> (1 val : a) -> b
assert_linear = believe_me id
where
id : (1 f : a -> b) -> a -> b
id f = f
export partial
idris_crash : String -> a
idris_crash = prim__crash _

8
libs/prelude/Prelude/Interfaces.idr
View File

@ -200,7 +200,7 @@ when False f = pure ()
||| function, into a single result.
||| @ t The type of the 'Foldable' parameterised type.
public export
interface Foldable (t : Type -> Type) where
interface Foldable t where
||| Successively combine the elements in a parameterised type using the
||| provided function, starting with the element that is in the final position
||| i.e. the right-most position.
@ -217,6 +217,9 @@ interface Foldable (t : Type -> Type) where
foldl : (func : acc -> elem -> acc) -> (init : acc) -> (input : t elem) -> acc
foldl f z t = foldr (flip (.) . flip f) id t z
||| Test whether the structure is empty.
null : t elem -> Bool
||| Similar to `foldl`, but uses a function wrapping its result in a `Monad`.
||| Consequently, the final value is wrapped in the same `Monad`.
public export
@ -328,7 +331,7 @@ choiceMap : (Foldable t, Alternative f) => (a -> f b) -> t a -> f b
choiceMap f = foldr (\e, a => f e <|> a) empty
public export
interface (Functor t, Foldable t) => Traversable (t : Type -> Type) where
interface (Functor t, Foldable t) => Traversable t where
||| Map each element of a structure to a computation, evaluate those
||| computations and combine the results.
traverse : Applicative f => (a -> f b) -> t a -> f (t b)
@ -342,4 +345,3 @@ sequence = traverse id
public export
for : (Traversable t, Applicative f) => t a -> (a -> f b) -> f (t b)
for = flip traverse

7
libs/prelude/Prelude/Types.idr
View File

@ -180,6 +180,8 @@ public export
Foldable Maybe where
foldr _ z Nothing = z
foldr f z (Just x) = f x z
null Nothing = True
null (Just _) = False
public export
Traversable Maybe where
@ -272,6 +274,8 @@ public export
Foldable (Either e) where
foldr f acc (Left _) = acc
foldr f acc (Right x) = f x acc
null (Left _) = True
null (Right _) = False
public export
Traversable (Either e) where
@ -341,6 +345,9 @@ Foldable List where
foldl f q [] = q
foldl f q (x::xs) = foldl f (f q x) xs
null [] = True
null (_::_) = False
public export
Applicative List where
pure x = [x]

191
src/Compiler/RefC/RefC.idr
View File

@ -14,6 +14,7 @@ import Core.TT
import Data.IORef
import Data.List
import Data.DList
import Data.NameMap
import Data.Nat
import Data.Strings
@ -29,20 +30,11 @@ import Utils.Path
findCC : IO String
findCC
= do Just cc <- getEnv "IDRIS2_CC"
| Nothing => do Just cc <- getEnv "CC"
| Nothing => pure "cc"
pure cc
pure cc
toString : List Char -> String
toString [] = ""
toString (c :: cx) = cast c ++ toString cx
natMinus : (a,b:Nat) -> Nat
natMinus a b = case isLTE b a of
(Yes prf) => minus a b
(No _) => 0
= do Nothing <- getEnv "IDRIS2_CC"
| Just cc => pure cc
Nothing <- getEnv "CC"
| Just cc => pure cc
pure "cc"
showcCleanStringChar : Char -> String -> String
showcCleanStringChar '+' = ("_plus" ++)
@ -75,9 +67,10 @@ showcCleanStringChar c
where
pad : String -> String
pad str
= case isLTE (length str) 4 of
Yes _ => toString (List.replicate (natMinus 4 (length str)) '0') ++ str
No _ => str
= let n = length str in
case isLTE n 4 of
Yes _ => fastPack (List.replicate (minus 4 n) '0') ++ str
No _ => str
showcCleanString : List Char -> String -> String
showcCleanString [] = id
@ -96,7 +89,8 @@ cName (Nested i n) = "n__" ++ cCleanString (show i) ++ "_" ++ cName n
cName (CaseBlock x y) = "case__" ++ cCleanString (show x) ++ "_" ++ cCleanString (show y)
cName (WithBlock x y) = "with__" ++ cCleanString (show x) ++ "_" ++ cCleanString (show y)
cName (Resolved i) = "fn__" ++ cCleanString (show i)
cName _ = "UNKNOWNNAME"
cName n = assert_total $ idris_crash ("INTERNAL ERROR: Unsupported name in C backend " ++ show n)
-- not really total but this way this internal error does not contaminate everything else
escapeChar : Char -> String
escapeChar '\DEL' = "127"
@ -161,7 +155,6 @@ where
showCString (c ::cs) = (showCChar c) . showCString cs
cConstant : Constant -> String
cConstant (I x) = "(Value*)makeInt32("++ show x ++")" -- (constant #:type 'i32 #:val " ++ show x ++ ")"
cConstant (BI x) = "(Value*)makeInt64("++ show x ++")" --"(constant #:type 'i64 #:val " ++ show x ++ ")"
@ -184,7 +177,8 @@ cConstant Bits8Type = "Bits8"
cConstant Bits16Type = "Bits16"
cConstant Bits32Type = "Bits32"
cConstant Bits64Type = "Bits64"
cConstant _ = "UNKNOWN"
cConstant n = assert_total $ idris_crash ("INTERNAL ERROR: Unknonw constant in C backend: " ++ show n)
-- not really total but this way this internal error does not contaminate everything else
extractConstant : Constant -> String
extractConstant (I x) = show x
@ -292,7 +286,7 @@ toPrim pn@(NS _ n)
(n == UN "prim__onCollectAny", OnCollectAny)
]
(Unknown pn)
toPrim pn = Unknown pn
toPrim pn = Unknown pn -- todo: crash rather than generate garbage?
varName : AVar -> String
@ -302,10 +296,19 @@ varName (ANull) = "NULL"
data ArgCounter : Type where
data FunctionDefinitions : Type where
data TemporaryVariableTracker : Type where
data OutfileText : Type where
data IndentLevel : Type where
data ExternalLibs : Type where
------------------------------------------------------------------------
-- Output generation: using a difference list for efficient append
data OutfileText : Type where
Output : Type
Output = DList String
------------------------------------------------------------------------
getNextCounter : {auto a : Ref ArgCounter Nat} -> Core Nat
getNextCounter = do
c <- get ArgCounter
@ -315,20 +318,13 @@ getNextCounter = do
registerVariableForAutomaticFreeing : {auto t : Ref TemporaryVariableTracker (List (List String))}
-> String
-> Core ()
registerVariableForAutomaticFreeing var = do
lists <- get TemporaryVariableTracker
case lists of
[] => do
put TemporaryVariableTracker ([[var]])
pure ()
(l :: ls) => do
put TemporaryVariableTracker ((var :: l) :: ls)
pure ()
registerVariableForAutomaticFreeing var
= update TemporaryVariableTracker $ \case
[] => [[var]]
(l :: ls) => ((var :: l) :: ls)
newTemporaryVariableLevel : {auto t : Ref TemporaryVariableTracker (List (List String))} -> Core ()
newTemporaryVariableLevel = do
lists <- get TemporaryVariableTracker
put TemporaryVariableTracker ([] :: lists)
newTemporaryVariableLevel = update TemporaryVariableTracker ([] ::)
getNewVar : {auto a : Ref ArgCounter Nat} -> {auto t : Ref TemporaryVariableTracker (List (List String))} -> Core String
@ -350,54 +346,44 @@ maxLineLengthForComment = 60
lJust : (line:String) -> (fillPos:Nat) -> (filler:Char) -> String
lJust line fillPos filler =
case isLTE (length line) fillPos of
let n = length line in
case isLTE n fillPos of
(Yes prf) =>
let missing = minus fillPos (length line)
let missing = minus fillPos n
fillBlock = pack (replicate missing filler)
in
line ++ fillBlock
(No _) => line
increaseIndentation : {auto il : Ref IndentLevel Nat} -> Core ()
increaseIndentation = do
iLevel <- get IndentLevel
put IndentLevel (S iLevel)
pure ()
increaseIndentation = update IndentLevel S
decreaseIndentation : {auto il : Ref IndentLevel Nat} -> Core ()
decreaseIndentation = do
iLevel <- get IndentLevel
case iLevel of
Z => pure ()
(S k) => do
put IndentLevel k
pure ()
decreaseIndentation = update IndentLevel pred
indentation : {auto il : Ref IndentLevel Nat} -> Core String
indentation = do
iLevel <- get IndentLevel
pure $ pack $ replicate (4 * iLevel) ' '
emit : {auto oft : Ref OutfileText (List String)} -> {auto il : Ref IndentLevel Nat} -> FC -> String -> Core ()
emit
: {auto oft : Ref OutfileText Output} ->
{auto il : Ref IndentLevel Nat} ->
FC -> String -> Core ()
emit EmptyFC line = do
lines <- get OutfileText
indent <- indentation
put OutfileText (lines ++ [indent ++ line])
pure ()
emit fc line' = do
update OutfileText (flip snoc (indent ++ line))
emit fc line = do
let comment = "// " ++ show fc
lines <- get OutfileText
indent <- indentation
let line = line'
case isLTE (length (indent ++ line)) maxLineLengthForComment of
(Yes _) => put OutfileText (lines ++ [ (lJust (indent ++ line) maxLineLengthForComment ' ') ++ " " ++ comment] )
(No _) => put OutfileText (lines ++ [indent ++ line, ((lJust "" maxLineLengthForComment ' ') ++ " " ++ comment)] )
pure ()
let indentedLine = indent ++ line
update OutfileText $ case isLTE (length indentedLine) maxLineLengthForComment of
(Yes _) => flip snoc (lJust indentedLine maxLineLengthForComment ' ' ++ " " ++ comment)
(No _) => flip appendR [indentedLine, (lJust "" maxLineLengthForComment ' ' ++ " " ++ comment)]
freeTmpVars : {auto t : Ref TemporaryVariableTracker (List (List String))}
-> {auto oft : Ref OutfileText (List String)}
-> {auto oft : Ref OutfileText Output}
-> {auto il : Ref IndentLevel Nat}
-> Core $ ()
freeTmpVars = do
@ -406,7 +392,6 @@ freeTmpVars = do
(vars :: varss) => do
traverse (\v => emit EmptyFC $ "removeReference(" ++ v ++ ");" ) vars
put TemporaryVariableTracker varss
pure ()
[] => pure ()
@ -424,7 +409,7 @@ addExternalLib extLib = do
makeArglist : {auto a : Ref ArgCounter Nat}
-> {auto t : Ref TemporaryVariableTracker (List (List String))}
-> {auto oft : Ref OutfileText (List String)}
-> {auto oft : Ref OutfileText Output}
-> {auto il : Ref IndentLevel Nat}
-> Nat
-> List AVar
@ -435,7 +420,7 @@ makeArglist missing xs = do
emit EmptyFC $ "Value_Arglist *"
++ arglist
++ " = newArglist(" ++ show missing
++ "," ++ show ((length xs) + missing)
++ "," ++ show (length xs + missing)
++ ");"
pushArgToArglist arglist xs 0
pure arglist
@ -451,16 +436,16 @@ where
++ " newReference(" ++ varName arg ++");"
pushArgToArglist arglist args (S k)
fillConstructorArgs : {auto oft : Ref OutfileText (List String)}
fillConstructorArgs : {auto oft : Ref OutfileText Output}
-> {auto il : Ref IndentLevel Nat}
-> String
-> List AVar
-> Nat
-> Core ()
fillConstructorArgs _ [] _ = pure ()
fillConstructorArgs constructor (v :: vars) k = do
emit EmptyFC $ constructor ++ "->args["++ show k ++ "] = newReference(" ++ varName v ++");"
fillConstructorArgs constructor vars (S k)
fillConstructorArgs cons (v :: vars) k = do
emit EmptyFC $ cons ++ "->args["++ show k ++ "] = newReference(" ++ varName v ++");"
fillConstructorArgs cons vars (S k)
showTag : Maybe Int -> String
@ -518,7 +503,7 @@ record ReturnStatement where
mutual
copyConstructors : {auto a : Ref ArgCounter Nat}
-> {auto t : Ref TemporaryVariableTracker (List (List String))}
-> {auto oft : Ref OutfileText (List String)}
-> {auto oft : Ref OutfileText Output}
-> {auto il : Ref IndentLevel Nat}
-> String
-> List AConAlt
@ -541,7 +526,7 @@ mutual
conBlocks : {auto a : Ref ArgCounter Nat}
-> {auto t : Ref TemporaryVariableTracker (List (List String))}
-> {auto oft : Ref OutfileText (List String)}
-> {auto oft : Ref OutfileText Output}
-> {auto il : Ref IndentLevel Nat}
-> (scrutinee:String)
-> List AConAlt
@ -573,7 +558,7 @@ mutual
constBlockSwitch : {auto a : Ref ArgCounter Nat}
-> {auto t : Ref TemporaryVariableTracker (List (List String))}
-> {auto oft : Ref OutfileText (List String)}
-> {auto oft : Ref OutfileText Output}
-> {auto il : Ref IndentLevel Nat}
-> (alts:List AConstAlt)
-> (retValVar:String)
@ -598,7 +583,7 @@ mutual
constDefaultBlock : {auto a : Ref ArgCounter Nat}
-> {auto t : Ref TemporaryVariableTracker (List (List String))}
-> {auto oft : Ref OutfileText (List String)}
-> {auto oft : Ref OutfileText Output}
-> {auto il : Ref IndentLevel Nat}
-> (def:Maybe ANF)
-> (retValVar:String)
@ -620,7 +605,7 @@ mutual
makeNonIntSwitchStatementConst :
{auto a : Ref ArgCounter Nat}
-> {auto t : Ref TemporaryVariableTracker (List (List String))}
-> {auto oft : Ref OutfileText (List String)}
-> {auto oft : Ref OutfileText Output}
-> {auto il : Ref IndentLevel Nat}
-> List AConstAlt
-> (k:Int)
@ -654,7 +639,7 @@ mutual
cStatementsFromANF : {auto a : Ref ArgCounter Nat}
-> {auto t : Ref TemporaryVariableTracker (List (List String))}
-> {auto oft : Ref OutfileText (List String)}
-> {auto oft : Ref OutfileText Output}
-> {auto il : Ref IndentLevel Nat}
-> ANF
-> Core ReturnStatement
@ -823,9 +808,9 @@ functionDefSignatureArglist : {auto c : Ref Ctxt Defs} -> Name -> Core String
functionDefSignatureArglist n = pure $ "Value *" ++ (cName !(getFullName n)) ++ "_arglist(Value_Arglist* arglist)"
getArgsNrList : {0 ty:Type} -> List ty -> Nat -> Core $ List Nat
getArgsNrList [] _ = pure []
getArgsNrList (x :: xs) k = pure $ k :: !(getArgsNrList xs (S k))
getArgsNrList : List ty -> Nat -> List Nat
getArgsNrList [] _ = []
getArgsNrList (x :: xs) k = k :: getArgsNrList xs (S k)
cTypeOfCFType : CFType -> Core $ String
@ -847,19 +832,17 @@ cTypeOfCFType (CFIORes x) = pure $ "void *"
cTypeOfCFType (CFStruct x ys) = pure $ "void *"
cTypeOfCFType (CFUser x ys) = pure $ "void *"
varNamesFromList : {0 ty : Type} -> List ty -> Nat -> Core (List String)
varNamesFromList [] _ = pure []
varNamesFromList (x :: xs) k = pure $ ("var_" ++ show k) :: !(varNamesFromList xs (S k))
varNamesFromList : List ty -> Nat -> List String
varNamesFromList str k = map (("var_" ++) . show) (getArgsNrList str k)
createFFIArgList : List CFType
-> Core $ List (String, String, CFType)
createFFIArgList cftypeList = do
sList <- traverse cTypeOfCFType cftypeList
varList <- varNamesFromList cftypeList 1
let z = zip3 sList varList cftypeList
pure z
let varList = varNamesFromList cftypeList 1
pure $ zip3 sList varList cftypeList
emitFDef : {auto oft : Ref OutfileText (List String)}
emitFDef : {auto oft : Ref OutfileText Output}
-> {auto il : Ref IndentLevel Nat}
-> (funcName:Name)
-> (arglist:List (String, String, CFType))
@ -912,18 +895,15 @@ packCFType (CFIORes x) varName = packCFType x varName
packCFType (CFStruct x xs) varName = "makeStruct(" ++ varName ++ ")"
packCFType (CFUser x xs) varName = "makeCustomUser(" ++ varName ++ ")"
discardLastArgument : {0 ty:Type} -> List ty -> List ty
discardLastArgument : List ty -> List ty
discardLastArgument [] = []
discardLastArgument (x :: []) = []
discardLastArgument (x :: y :: ys) = x :: (discardLastArgument (y :: ys))
discardLastArgument xs@(_ :: _) = init xs
createCFunctions : {auto c : Ref Ctxt Defs}
-> {auto a : Ref ArgCounter Nat}
-> {auto f : Ref FunctionDefinitions (List String)}
-> {auto t : Ref TemporaryVariableTracker (List (List String))}
-> {auto oft : Ref OutfileText (List String)}
-> {auto oft : Ref OutfileText Output}
-> {auto il : Ref IndentLevel Nat}
-> {auto e : Ref ExternalLibs (List String)}
-> Name
@ -935,7 +915,7 @@ createCFunctions n (MkAFun args anf) = do
otherDefs <- get FunctionDefinitions
put FunctionDefinitions ((fn ++ ";\n") :: (fn' ++ ";\n") :: otherDefs)
newTemporaryVariableLevel
argsNrs <- getArgsNrList args Z
let argsNrs = getArgsNrList args Z
emit EmptyFC fn
emit EmptyFC "{"
increaseIndentation
@ -966,7 +946,6 @@ createCFunctions n (MkAFun args anf) = do
createCFunctions n (MkACon tag arity) = do
emit EmptyFC $ ( "// Constructor tag " ++ show tag ++ " arity " ++ show arity) -- Nothing to compile here
pure ()
createCFunctions n (MkAForeign ccs fargs (CFIORes ret)) = do
@ -989,7 +968,7 @@ createCFunctions n (MkAForeign ccs fargs (CFIORes ret)) = do
increaseIndentation
emit EmptyFC $ "("
increaseIndentation
let commaSepArglist = addCommaToList (map (\a => "arglist->args["++ show a ++"]") !(getArgsNrList fargs Z))
let commaSepArglist = addCommaToList (map (\a => "arglist->args["++ show a ++"]") (getArgsNrList fargs Z))
traverse (emit EmptyFC) commaSepArglist
decreaseIndentation
emit EmptyFC ");"
@ -1043,7 +1022,7 @@ createCFunctions n (MkAError exp) = do
header : {auto f : Ref FunctionDefinitions (List String)}
-> {auto o : Ref OutfileText (List String)}
-> {auto o : Ref OutfileText Output}
-> {auto il : Ref IndentLevel Nat}
-> {auto e : Ref ExternalLibs (List String)}
-> Core ()
@ -1055,11 +1034,9 @@ header = do
let extLibLines = map (\lib => "// add header(s) for library: " ++ lib ++ "\n") extLibs
traverse (\l => coreLift (putStrLn $ " header for " ++ l ++ " needed")) extLibs
fns <- get FunctionDefinitions
outText <- get OutfileText
put OutfileText (initLines ++ extLibLines ++ ["\n// function definitions"] ++ fns ++ outText)
pure ()
update OutfileText (appendL (initLines ++ extLibLines ++ ["\n// function definitions"] ++ fns))
footer : {auto il : Ref IndentLevel Nat} -> {auto f : Ref OutfileText (List String)} -> Core ()
footer : {auto il : Ref IndentLevel Nat} -> {auto f : Ref OutfileText Output} -> Core ()
footer = do
emit EmptyFC ""
emit EmptyFC " // main function"
@ -1069,7 +1046,6 @@ footer = do
emit EmptyFC " trampoline(mainExprVal);"
emit EmptyFC " return 0; // bye bye"
emit EmptyFC "}"
pure ()
export
executeExpr : Ref Ctxt Defs -> (execDir : String) -> ClosedTerm -> Core ()
@ -1097,14 +1073,14 @@ compileExpr ANF c _ outputDir tm outfile =
newRef ArgCounter 0
newRef FunctionDefinitions []
newRef TemporaryVariableTracker []
newRef OutfileText []
newRef OutfileText DList.Nil
newRef ExternalLibs []
newRef IndentLevel 0
traverse (\(n, d) => createCFunctions n d) defs
header -- added after the definition traversal in order to add all encountered function defintions
footer
fileContent <- get OutfileText
let code = fastAppend (map (++ "\n") fileContent)
let code = fastAppend (map (++ "\n") (reify fileContent))
coreLift (writeFile outn code)
coreLift $ putStrLn $ "Generated C file " ++ outn
@ -1123,14 +1099,13 @@ compileExpr ANF c _ outputDir tm outfile =
clibdirs (lib_dirs dirs)
coreLift $ putStrLn runccobj
ok <- coreLift $ system runccobj
if ok == 0
then do coreLift $ putStrLn runcc
ok <- coreLift $ system runcc
if ok == 0
then pure (Just outexec)
else pure Nothing
else pure Nothing
0 <- coreLift $ system runccobj
| _ => pure Nothing
coreLift $ putStrLn runcc
0 <- coreLift $ system runcc
| _ => pure Nothing
pure (Just outexec)
where
fullprefix_dir : Dirs -> String -> String
fullprefix_dir dirs sub

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

@ -156,6 +156,9 @@ mutual
= do p' <- schExp chezExtPrim chezString 0 p
c' <- schExp chezExtPrim chezString 0 c
pure $ mkWorld $ "(blodwen-register-object " ++ p' ++ " " ++ c' ++ ")"
chezExtPrim i MakeFuture [_, work]
= do work' <- schExp chezExtPrim chezString 0 work
pure $ "(blodwen-make-future " ++ work' ++ ")"
chezExtPrim i prim args
= schExtCommon chezExtPrim chezString i prim args

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

@ -206,6 +206,7 @@ data ExtPrim = NewIORef | ReadIORef | WriteIORef
| SysOS | SysCodegen
| OnCollect
| OnCollectAny
| MakeFuture
| Unknown Name
export
@ -223,6 +224,7 @@ Show ExtPrim where
show SysCodegen = "SysCodegen"
show OnCollect = "OnCollect"
show OnCollectAny = "OnCollectAny"
show MakeFuture = "MakeFuture"
show (Unknown n) = "Unknown " ++ show n
||| Match on a user given name to get the scheme primitive
@ -241,7 +243,8 @@ toPrim pn@(NS _ n)
(n == UN "prim__os", SysOS),
(n == UN "prim__codegen", SysCodegen),
(n == UN "prim__onCollect", OnCollect),
(n == UN "prim__onCollectAny", OnCollectAny)
(n == UN "prim__onCollectAny", OnCollectAny),
(n == UN "prim__makeFuture", MakeFuture)
]
(Unknown pn)
toPrim pn = Unknown pn

19
src/Compiler/Scheme/Gambit.idr
View File

@ -38,6 +38,13 @@ findGSC =
do env <- getEnv "GAMBIT_GSC"
pure $ fromMaybe "/usr/bin/env gsc" env
findGSCBackend : IO String
findGSCBackend =
do env <- getEnv "GAMBIT_GSC_BACKEND"
pure $ case env of
Nothing => ""
Just e => " -cc " ++ e
schHeader : String
schHeader = "; @generated\n
(declare (block)
@ -387,9 +394,15 @@ compileExpr c tmpDir outputDir tm outfile
libsname <- compileToSCM c tm srcPath
libsfile <- traverse findLibraryFile $ map (<.> "a") (nub libsname)
gsc <- coreLift findGSC
let cmd = gsc ++
" -exe -cc-options \"-Wno-implicit-function-declaration\" -ld-options \"" ++
(showSep " " libsfile) ++ "\" -o \"" ++ execPath ++ "\" \"" ++ srcPath ++ "\""
gscBackend <- coreLift findGSCBackend
ds <- getDirectives Gambit
let gscCompileOpts =
case find (== "C") ds of
Nothing => gscBackend ++ " -exe -cc-options \"-Wno-implicit-function-declaration\" -ld-options \"" ++
(showSep " " libsfile) ++ "\""
Just _ => " -c"
let cmd =
gsc ++ gscCompileOpts ++ " -o \"" ++ execPath ++ "\" \"" ++ srcPath ++ "\""
ok <- coreLift $ system cmd
if ok == 0
then pure (Just execPath)

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

@ -42,6 +42,7 @@ schHeader : String -> String
schHeader libs
= "#lang racket/base\n" ++
"; @generated\n" ++
"(require racket/future)\n" ++ -- for parallelism/concurrency
"(require racket/math)\n" ++ -- for math ops
"(require racket/system)\n" ++ -- for system
"(require rnrs/bytevectors-6)\n" ++ -- for buffers
@ -95,6 +96,9 @@ mutual
= do p' <- schExp racketPrim racketString 0 p
c' <- schExp racketPrim racketString 0 c
pure $ mkWorld $ "(blodwen-register-object " ++ p' ++ " " ++ c' ++ ")"
racketPrim i MakeFuture [_, work]
= do work' <- schExp racketPrim racketString 0 work
pure $ mkWorld $ "(blodwen-make-future " ++ work' ++ ")"
racketPrim i prim args
= schExtCommon racketPrim racketString i prim args

2
src/Core/Binary.idr
View File

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

8
src/Core/Context.idr
View File

@ -2214,10 +2214,12 @@ getPrimitiveNames = pure $ catMaybes [!fromIntegerName, !fromStringName, !fromCh
export
addLogLevel : {auto c : Ref Ctxt Defs} ->
LogLevel -> Core ()
addLogLevel l
Maybe LogLevel -> Core ()
addLogLevel lvl
= do defs <- get Ctxt
put Ctxt (record { options->session->logLevel $= insertLogLevel l } defs)
case lvl of
Nothing => put Ctxt (record { options->session->logLevel = defaultLogLevel } defs)
Just l => put Ctxt (record { options->session->logLevel $= insertLogLevel l } defs)
export
withLogLevel : {auto c : Ref Ctxt Defs} ->

37
src/Core/Core.idr
View File

@ -95,8 +95,8 @@ data Error : Type where
NotRecordField : FC -> String -> Maybe Name -> Error
NotRecordType : FC -> Name -> Error
IncompatibleFieldUpdate : FC -> List String -> Error
InvalidImplicits : {vars : _} ->
FC -> Env Term vars -> List (Maybe Name) -> Term vars -> Error
InvalidArgs : {vars : _} ->
FC -> Env Term vars -> List Name -> Term vars -> Error
TryWithImplicits : {vars : _} ->
FC -> Env Term vars -> List (Name, Term vars) -> Error
BadUnboundImplicit : {vars : _} ->
@ -242,8 +242,8 @@ Show Error where
= show fc ++ ":" ++ show ty ++ " is not a record type"
show (IncompatibleFieldUpdate fc flds)
= show fc ++ ":Field update " ++ showSep "->" flds ++ " not compatible with other updates"
show (InvalidImplicits fc env ns tm)
= show fc ++ ":" ++ show ns ++ " are not valid implicit arguments in " ++ show tm
show (InvalidArgs fc env ns tm)
= show fc ++ ":" ++ show ns ++ " are not valid arguments in " ++ show tm
show (TryWithImplicits fc env imps)
= show fc ++ ":Need to bind implicits "
++ showSep "," (map (\x => show (fst x) ++ " : " ++ show (snd x)) imps)
@ -348,7 +348,7 @@ getErrorLoc (RecordTypeNeeded loc _) = Just loc
getErrorLoc (NotRecordField loc _ _) = Just loc
getErrorLoc (NotRecordType loc _) = Just loc
getErrorLoc (IncompatibleFieldUpdate loc _) = Just loc
getErrorLoc (InvalidImplicits loc _ _ _) = Just loc
getErrorLoc (InvalidArgs loc _ _ _) = Just loc
getErrorLoc (TryWithImplicits loc _ _) = Just loc
getErrorLoc (BadUnboundImplicit loc _ _ _) = Just loc
getErrorLoc (CantSolveGoal loc _ _) = Just loc
@ -486,8 +486,8 @@ unless = when . not
-- Control.Catchable in Idris 1, just copied here (but maybe no need for
-- it since we'll only have the one instance for Core Error...)
public export
interface Catchable (m : Type -> Type) t | m where
throw : t -> m a
interface Catchable m t | m where
throw : {0 a : Type} -> t -> m a
catch : m a -> (t -> m a) -> m a
export
@ -505,10 +505,16 @@ traverse' f [] acc = pure (reverse acc)
traverse' f (x :: xs) acc
= traverse' f xs (!(f x) :: acc)
%inline
export
traverse : (a -> Core b) -> List a -> Core (List b)
traverse f xs = traverse' f xs []
%inline
export
for : List a -> (a -> Core b) -> Core (List b)
for = flip traverse
export
traverseList1 : (a -> Core b) -> List1 a -> Core (List1 b)
traverseList1 f (x ::: xs) = [| f x ::: traverse f xs |]
@ -518,6 +524,7 @@ traverseVect : (a -> Core b) -> Vect n a -> Core (Vect n b)
traverseVect f [] = pure []
traverseVect f (x :: xs) = [| f x :: traverseVect f xs |]
%inline
export
traverseOpt : (a -> Core b) -> Maybe a -> Core (Maybe b)
traverseOpt f Nothing = pure Nothing
@ -530,6 +537,16 @@ traverse_ f (x :: xs)
= do f x
traverse_ f xs
%inline
export
sequence : List (Core a) -> Core (List a)
sequence (x :: xs)
= do
x' <- x
xs' <- sequence xs
pure (x' :: xs')
sequence [] = pure []
export
traverseList1_ : (a -> Core b) -> List1 a -> Core ()
traverseList1_ f (x ::: xs) = do
@ -618,6 +635,12 @@ export %inline
put : (x : label) -> {auto ref : Ref x a} -> a -> Core ()
put x {ref = MkRef io} val = coreLift (writeIORef io val)
export %inline
update : (x : label) -> {auto ref : Ref x a} -> (a -> a) -> Core ()
update x f
= do v <- get x
put x (f v)
export
cond : List (Lazy Bool, Lazy a) -> a -> a
cond [] def = def

23
src/Core/Normalise.idr
View File

@ -500,9 +500,9 @@ export
data QVar : Type where
public export
interface Quote (tm : List Name -> Type) where
interface Quote tm where
quote : {auto c : Ref Ctxt Defs} ->
{vars : _} ->
{vars : List Name} ->
Defs -> Env Term vars -> tm vars -> Core (Term vars)
quoteGen : {auto c : Ref Ctxt Defs} ->
{vars : _} ->
@ -767,9 +767,9 @@ etaContract tm = do
_ => pure tm
public export
interface Convert (tm : List Name -> Type) where
interface Convert tm where
convert : {auto c : Ref Ctxt Defs} ->
{vars : _} ->
{vars : List Name} ->
Defs -> Env Term vars ->
tm vars -> tm vars -> Core Bool
convGen : {auto c : Ref Ctxt Defs} ->
@ -1296,25 +1296,26 @@ replace : {auto c : Ref Ctxt Defs} ->
Core (Term vars)
replace = replace' 0
||| For printing purposes
export
normaliseErr : {auto c : Ref Ctxt Defs} ->
Error -> Core Error
normaliseErr (CantConvert fc env l r)
= do defs <- get Ctxt
pure $ CantConvert fc env !(normaliseHoles defs env l)
!(normaliseHoles defs env r)
pure $ CantConvert fc env !(normaliseHoles defs env l >>= toFullNames)
!(normaliseHoles defs env r >>= toFullNames)
normaliseErr (CantSolveEq fc env l r)
= do defs <- get Ctxt
pure $ CantSolveEq fc env !(normaliseHoles defs env l)
!(normaliseHoles defs env r)
pure $ CantSolveEq fc env !(normaliseHoles defs env l >>= toFullNames)
!(normaliseHoles defs env r >>= toFullNames)
normaliseErr (WhenUnifying fc env l r err)
= do defs <- get Ctxt
pure $ WhenUnifying fc env !(normaliseHoles defs env l)
!(normaliseHoles defs env r)
pure $ WhenUnifying fc env !(normaliseHoles defs env l >>= toFullNames)
!(normaliseHoles defs env r >>= toFullNames)
!(normaliseErr err)
normaliseErr (CantSolveGoal fc env g)
= do defs <- get Ctxt
pure $ CantSolveGoal fc env !(normaliseHoles defs env g)
pure $ CantSolveGoal fc env !(normaliseHoles defs env g >>= toFullNames)
normaliseErr (AllFailed errs)
= pure $ AllFailed !(traverse (\x => pure (fst x, !(normaliseErr (snd x)))) errs)
normaliseErr (InType fc n err)

2
src/Core/Options/Log.idr
View File

@ -116,7 +116,7 @@ defaultLogLevel = singleton [] 0
export
insertLogLevel : LogLevel -> LogLevels -> LogLevels
insertLogLevel (MkLogLevel ps n) = insertWith ps (maybe n (max n))
insertLogLevel (MkLogLevel ps n) = insert ps n
----------------------------------------------------------------------------------
-- CHECKING WHETHER TO LOG

4
src/Core/TT.idr
View File

@ -651,8 +651,8 @@ eqTerm (TType _) (TType _) = True
eqTerm _ _ = False
public export
interface Weaken (tm : List Name -> Type) where
weaken : tm vars -> tm (n :: vars)
interface Weaken tm where
weaken : {0 vars : List Name} -> tm vars -> tm (n :: vars)
weakenNs : SizeOf ns -> tm vars -> tm (ns ++ vars)
weakenNs p t = case sizedView p of

4
src/Core/Unify.idr
View File

@ -120,9 +120,9 @@ solvedHole : Int -> UnifyResult
solvedHole n = MkUnifyResult [] True [n] NoLazy
public export
interface Unify (tm : List Name -> Type) where
interface Unify tm where
-- Unify returns a list of ids referring to newly added constraints
unifyD : {vars : _} ->
unifyD : {vars : List Name} ->
Ref Ctxt Defs ->
Ref UST UState ->
UnifyInfo ->

40
src/Data/DList.idr Normal file
View File

@ -0,0 +1,40 @@
module Data.DList
%default total
-- Do not re-export the type so that it does not get unfolded in goals
-- and error messages!
export
DList : Type -> Type
DList a = List a -> List a
export
Nil : DList a
Nil = id
export
(::) : a -> DList a -> DList a
(::) a as = (a ::) . as
export
snoc : DList a -> a -> DList a
snoc as a = as . (a ::)
export
appendR : DList a -> List a -> DList a
appendR as bs = as . (bs ++)
export
appendL : List a -> DList a -> DList a
appendL as bs = (as ++) . bs
export
(++) : DList a -> DList a -> DList a
(++) = (.)
export
reify : DList a -> List a
reify as = as []
-- NB: No Functor instance because it's too expensive to reify, map, put back
-- Consider using a different data structure if you need mapping (e.g. a rope)

48
src/Idris/Desugar.idr
View File

@ -26,6 +26,7 @@ import TTImp.TTImp
import TTImp.Utils
import Utils.Shunting
import Utils.String
import Control.Monad.State
import Data.List
@ -149,10 +150,15 @@ mutual
pure $ IPi fc rig !(traverse (desugar side ps') p)
mn !(desugarB side ps argTy)
!(desugarB side ps' retTy)
desugarB side ps (PLam fc rig p (PRef _ n@(UN _)) argTy scope)
= pure $ ILam fc rig !(traverse (desugar side ps) p)
desugarB side ps (PLam fc rig p pat@(PRef _ n@(UN nm)) argTy scope)
= if lowerFirst nm || nm == "_"
then pure $ ILam fc rig !(traverse (desugar side ps) p)
(Just n) !(desugarB side ps argTy)
!(desugar side (n :: ps) scope)
else pure $ ILam fc rig !(traverse (desugar side ps) p)
(Just (MN "lamc" 0)) !(desugarB side ps argTy) $
ICase fc (IVar fc (MN "lamc" 0)) (Implicit fc False)
[!(desugarClause ps True (MkPatClause fc pat scope []))]
desugarB side ps (PLam fc rig p (PRef _ n@(MN _ _)) argTy scope)
= pure $ ILam fc rig !(traverse (desugar side ps) p)
(Just n) !(desugarB side ps argTy)
@ -189,10 +195,12 @@ mutual
(PApp fc (PUpdate fc fs) (PRef fc (MN "rec" 0))))
desugarB side ps (PApp fc x y)
= pure $ IApp fc !(desugarB side ps x) !(desugarB side ps y)
desugarB side ps (PAutoApp fc x y)
= pure $ IAutoApp fc !(desugarB side ps x) !(desugarB side ps y)
desugarB side ps (PWithApp fc x y)
= pure $ IWithApp fc !(desugarB side ps x) !(desugarB side ps y)
desugarB side ps (PImplicitApp fc x argn y)
= pure $ IImplicitApp fc !(desugarB side ps x) argn !(desugarB side ps y)
desugarB side ps (PNamedApp fc x argn y)
= pure $ INamedApp fc !(desugarB side ps x) argn !(desugarB side ps y)
desugarB side ps (PDelayed fc r ty)
= pure $ IDelayed fc r !(desugarB side ps ty)
desugarB side ps (PDelay fc tm)
@ -636,7 +644,8 @@ mutual
getFn : RawImp -> Core Name
getFn (IVar _ n) = pure n
getFn (IApp _ f _) = getFn f
getFn (IImplicitApp _ f _ _) = getFn f
getFn (IAutoApp _ f _) = getFn f
getFn (INamedApp _ f _ _) = getFn f
getFn tm = throw (InternalError (show tm ++ " is not a function application"))
toIDef : ImpClause -> Core ImpDecl
@ -678,28 +687,33 @@ mutual
-- pure [IReflect fc !(desugar AnyExpr ps tm)]
desugarDecl ps (PInterface fc vis cons_in tn doc params det conname body)
= do addDocString tn doc
let paramNames = map fst params
let cons = concatMap expandConstraint cons_in
cons' <- traverse (\ ntm => do tm' <- desugar AnyExpr (ps ++ map fst params)
cons' <- traverse (\ ntm => do tm' <- desugar AnyExpr (ps ++ paramNames)
(snd ntm)
pure (fst ntm, tm')) cons
params' <- traverse (\ ntm => do tm' <- desugar AnyExpr ps (snd ntm)
pure (fst ntm, tm')) params
params' <- traverse (\ (nm, (rig, tm)) =>
do tm' <- desugar AnyExpr ps tm
pure (nm, (rig, tm')))
params
-- Look for bindable names in all the constraints and parameters
let mnames = map dropNS (definedIn body)
let bnames = ifThenElse !isUnboundImplicits
(concatMap (findBindableNames True
(ps ++ mnames ++ map fst params) [])
(ps ++ mnames ++ paramNames) [])
(map Builtin.snd cons') ++
concatMap (findBindableNames True
(ps ++ mnames ++ map fst params) [])
(map Builtin.snd params'))
(ps ++ mnames ++ paramNames) [])
(map (snd . snd) params'))
[]
let paramsb = map (\ ntm => (Builtin.fst ntm,
doBind bnames (Builtin.snd ntm))) params'
let consb = map (\ ntm => (Builtin.fst ntm,
doBind bnames (Builtin.snd ntm))) cons'
let paramsb = map (\ (nm, (rig, tm)) =>
let tm' = doBind bnames tm in
(nm, (rig, tm')))
params'
let consb = map (\ (nm, tm) => (nm, doBind bnames tm)) cons'
body' <- traverse (desugarDecl (ps ++ mnames ++ map fst params)) body
body' <- traverse (desugarDecl (ps ++ mnames ++ paramNames)) body
pure [IPragma (\nest, env =>
elabInterface fc vis env nest consb
tn paramsb det conname
@ -821,7 +835,7 @@ mutual
desugarDecl ps (PDirective fc d)
= case d of
Hide n => pure [IPragma (\nest, env => hide fc n)]
Logging i => pure [ILog (topics i, verbosity i)]
Logging i => pure [ILog ((\ i => (topics i, verbosity i)) <$> i)]
LazyOn a => pure [IPragma (\nest, env => lazyActive a)]
UnboundImplicits a => do
setUnboundImplicits a

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

@ -51,13 +51,18 @@ bindImpls fc [] ty = ty
bindImpls fc ((n, r, ty) :: rest) sc
= IPi fc r Implicit (Just n) ty (bindImpls fc rest sc)
addDefaults : FC -> Name -> List Name -> List (Name, List ImpClause) ->
addDefaults : FC -> Name ->
(params : List (Name, RawImp)) -> -- parameters have been specialised, use them!
(allMethods : List Name) ->
(defaults : List (Name, List ImpClause)) ->
List ImpDecl ->
(List ImpDecl, List Name) -- Updated body, list of missing methods
addDefaults fc impName allms defs body
addDefaults fc impName params allms defs body
= let missing = dropGot allms body in
extendBody [] missing body
where
specialiseMeth : Name -> (Name, RawImp)
specialiseMeth n = (n, INamedApp fc (IVar fc n) (UN "__con") (IVar fc impName))
-- Given the list of missing names, if any are among the default definitions,
-- add them to the body
extendBody : List Name -> List Name -> List ImpDecl ->
@ -73,10 +78,12 @@ addDefaults fc impName allms defs body
-- That is, default method implementations could depend on
-- other methods.
-- (See test idris2/interface014 for an example!)
let mupdates
= map (\n => (n, IImplicitApp fc (IVar fc n)
(Just (UN "__con"))
(IVar fc impName))) allms
-- Similarly if any parameters appear in the clauses, they should
-- be substituted for the actual parameters because they are going
-- to be referring to unbound variables otherwise.
-- (See test idris2/interface018 for an example!)
let mupdates = params ++ map specialiseMeth allms
cs' = map (substNamesClause [] mupdates) cs in
extendBody ms ns
(IDef fc n (map (substLocClause fc) cs') :: body)
@ -140,11 +147,12 @@ elabImplementation {vars} fc vis opts_in pass env nest is cons iname ps impln nu
logTerm "elab.implementation" 3 ("Found interface " ++ show cn) ity
log "elab.implementation" 3 $
" with params: " ++ show (params cdata)
++ " and parents: " ++ show (parents cdata)
++ " using implicits: " ++ show impsp
++ " and methods: " ++ show (methods cdata) ++ "\n"
++ "Constructor: " ++ show (iconstructor cdata) ++ "\n"
"\n with params: " ++ show (params cdata)
++ "\n specialised to: " ++ show ps
++ "\n and parents: " ++ show (parents cdata)
++ "\n using implicits: " ++ show impsp
++ "\n and methods: " ++ show (methods cdata) ++ "\n"
++ "\nConstructor: " ++ show (iconstructor cdata) ++ "\n"
logTerm "elab.implementation" 3 "Constructor type: " conty
log "elab.implementation" 5 $ "Making implementation " ++ show impName
@ -180,7 +188,9 @@ elabImplementation {vars} fc vis opts_in pass env nest is cons iname ps impln nu
-- 1.5. Lookup default definitions and add them to to body
let (body, missing)
= addDefaults fc impName (map (dropNS . fst) (methods cdata))
= addDefaults fc impName
(zip (params cdata) ps)
(map (dropNS . fst) (methods cdata))
(defaults cdata) body_in
log "elab.implementation" 5 $ "Added defaults: body is " ++ show body
@ -212,9 +222,8 @@ elabImplementation {vars} fc vis opts_in pass env nest is cons iname ps impln nu
defs <- get Ctxt
let fldTys = getFieldArgs !(normaliseHoles defs [] conty)
log "elab.implementation" 5 $ "Field types " ++ show fldTys
let irhs = apply (IVar fc con)
(map (const (ISearch fc 500)) (parents cdata)
++ map (mkMethField methImps fldTys) fns)
let irhs = apply (autoImpsApply (IVar fc con) $ map (const (ISearch fc 500)) (parents cdata))
(map (mkMethField methImps fldTys) fns)
let impFn = IDef fc impName [PatClause fc ilhs irhs]
log "elab.implementation" 5 $ "Implementation record: " ++ show impFn
@ -267,7 +276,11 @@ elabImplementation {vars} fc vis opts_in pass env nest is cons iname ps impln nu
impsApply : RawImp -> List (Name, RawImp) -> RawImp
impsApply fn [] = fn
impsApply fn ((n, arg) :: ns)
= impsApply (IImplicitApp fc fn (Just n) arg) ns
= impsApply (INamedApp fc fn n arg) ns
autoImpsApply : RawImp -> List RawImp -> RawImp
autoImpsApply f [] = f
autoImpsApply f (x :: xs) = autoImpsApply (IAutoApp (getFC f) f x) xs
mkLam : List (Name, RigCount, PiInfo RawImp) -> RawImp -> RawImp
mkLam [] tm = tm
@ -279,11 +292,11 @@ elabImplementation {vars} fc vis opts_in pass env nest is cons iname ps impln nu
applyTo fc tm ((x, c, Explicit) :: xs)
= applyTo fc (IApp fc tm (IVar fc x)) xs
applyTo fc tm ((x, c, AutoImplicit) :: xs)
= applyTo fc (IImplicitApp fc tm (Just x) (IVar fc x)) xs
= applyTo fc (INamedApp fc tm x (IVar fc x)) xs
applyTo fc tm ((x, c, Implicit) :: xs)
= applyTo fc (IImplicitApp fc tm (Just x) (IVar fc x)) xs
= applyTo fc (INamedApp fc tm x (IVar fc x)) xs
applyTo fc tm ((x, c, DefImplicit _) :: xs)
= applyTo fc (IImplicitApp fc tm (Just x) (IVar fc x)) xs
= applyTo fc (INamedApp fc tm x (IVar fc x)) xs
-- When applying the method in the field for the record, eta expand
-- the expected arguments based on the field type, so that implicits get
@ -422,9 +435,12 @@ elabImplementation {vars} fc vis opts_in pass env nest is cons iname ps impln nu
updateApp ns (IApp fc f arg)
= do f' <- updateApp ns f
pure (IApp fc f' arg)
updateApp ns (IImplicitApp fc f x arg)
updateApp ns (IAutoApp fc f arg)
= do f' <- updateApp ns f
pure (IImplicitApp fc f' x arg)
pure (IAutoApp fc f' arg)
updateApp ns (INamedApp fc f x arg)
= do f' <- updateApp ns f
pure (INamedApp fc f' x arg)
updateApp ns tm
= throw (GenericMsg (getFC tm) "Invalid method definition")
@ -457,9 +473,9 @@ elabImplementation {vars} fc vis opts_in pass env nest is cons iname ps impln nu
= do log "elab.implementation" 3 $
"Adding transform for " ++ show top ++ " : " ++ show ty ++
"\n\tfor " ++ show iname ++ " in " ++ show ns
let lhs = IImplicitApp fc (IVar fc top)
(Just (UN "__con"))
(IVar fc iname)
let lhs = INamedApp fc (IVar fc top)
(UN "__con")
(IVar fc iname)
let Just mname = lookup (dropNS top) ns
| Nothing => pure ()
let rhs = IVar fc mname

111
src/Idris/Elab/Interface.idr
View File

@ -30,32 +30,33 @@ import Data.Maybe
-- TODO: Check all the parts of the body are legal
-- TODO: Deal with default superclass implementations
mkDataTy : FC -> List (Name, RawImp) -> RawImp
mkDataTy : FC -> List (Name, (RigCount, RawImp)) -> RawImp
mkDataTy fc [] = IType fc
mkDataTy fc ((n, ty) :: ps)
mkDataTy fc ((n, (_, ty)) :: ps)
= IPi fc top Explicit (Just n) ty (mkDataTy fc ps)
mkIfaceData : {vars : _} ->
{auto c : Ref Ctxt Defs} ->
FC -> Visibility -> Env Term vars ->
List (Maybe Name, RigCount, RawImp) ->
Name -> Name -> List (Name, RawImp) ->
Name -> Name -> List (Name, (RigCount, RawImp)) ->
List Name -> List (Name, RigCount, RawImp) -> Core ImpDecl
mkIfaceData {vars} fc vis env constraints n conName ps dets meths
= let opts = if isNil dets
then [NoHints, UniqueSearch]
else [NoHints, UniqueSearch, SearchBy dets]
retty = apply (IVar fc n) (map (IVar fc) (map fst ps))
pNames = map fst ps
retty = apply (IVar fc n) (map (IVar fc) pNames)
conty = mkTy Implicit (map jname ps) $
mkTy Explicit (map bhere constraints ++ map bname meths) retty
con = MkImpTy fc conName !(bindTypeNames [] (map fst ps ++ map fst meths ++ vars) conty) in
mkTy AutoImplicit (map bhere constraints) (mkTy Explicit (map bname meths) retty)
con = MkImpTy fc conName !(bindTypeNames [] (pNames ++ map fst meths ++ vars) conty) in
pure $ IData fc vis (MkImpData fc n
!(bindTypeNames [] (map fst ps ++ map fst meths ++ vars)
!(bindTypeNames [] (pNames ++ map fst meths ++ vars)
(mkDataTy fc ps))
opts [con])
where
jname : (Name, RawImp) -> (Maybe Name, RigCount, RawImp)
jname (n, t) = (Just n, erased, t)
jname : (Name, (RigCount, RawImp)) -> (Maybe Name, RigCount, RawImp)
jname (n, rig, t) = (Just n, rig, t)
bname : (Name, RigCount, RawImp) -> (Maybe Name, RigCount, RawImp)
bname (n, c, t) = (Just n, c, IBindHere (getFC t) (PI erased) t)
@ -86,13 +87,14 @@ namePis i ty = ty
getMethDecl : {vars : _} ->
{auto c : Ref Ctxt Defs} ->
Env Term vars -> NestedNames vars ->
(params : List (Name, RawImp)) ->
(params : List (Name, (RigCount, RawImp))) ->
(mnames : List Name) ->
(FC, RigCount, List FnOpt, n, (Bool, RawImp)) ->
Core (n, RigCount, RawImp)
getMethDecl {vars} env nest params mnames (fc, c, opts, n, (d, ty))
= do ty_imp <- bindTypeNames [] (map fst params ++ mnames ++ vars) ty
pure (n, c, stripParams (map fst params) ty_imp)
= do let paramNames = map fst params
ty_imp <- bindTypeNames [] (paramNames ++ mnames ++ vars) ty
pure (n, c, stripParams paramNames ty_imp)
where
-- We don't want the parameters to explicitly appear in the method
-- type in the record for the interface (they are parameters of the
@ -104,13 +106,9 @@ getMethDecl {vars} env nest params mnames (fc, c, opts, n, (d, ty))
else IPi fc r p mn arg (stripParams ps ret)
stripParams ps ty = ty
-- bind the auto implicit for the interface - put it after all the other
-- implicits
-- bind the auto implicit for the interface - put it first, as it may be needed
-- in other method variables, including implicit variables
bindIFace : FC -> RawImp -> RawImp -> RawImp
bindIFace _ ity (IPi fc rig Implicit n ty sc)
= IPi fc rig Implicit n ty (bindIFace fc ity sc)
bindIFace _ ity (IPi fc rig AutoImplicit n ty sc)
= IPi fc rig AutoImplicit n ty (bindIFace fc ity sc)
bindIFace fc ity sc = IPi fc top AutoImplicit (Just (UN "__con")) ity sc
-- Get the top level function for implementing a method
@ -120,28 +118,28 @@ getMethToplevel : {vars : _} ->
Name -> Name ->
(constraints : List (Maybe Name)) ->
(allmeths : List Name) ->
(params : List (Name, RawImp)) ->
(params : List (Name, (RigCount, RawImp))) ->
(FC, RigCount, List FnOpt, Name, (Bool, RawImp)) ->
Core (List ImpDecl)
getMethToplevel {vars} env vis iname cname constraints allmeths params
(fc, c, opts, n, (d, ty))
= do let ity = apply (IVar fc iname) (map (IVar fc) (map fst params))
= do let paramNames = map fst params
let ity = apply (IVar fc iname) (map (IVar fc) paramNames)
-- Make the constraint application explicit for any method names
-- which appear in other method types
let ty_constr =
bindPs params $ substNames vars (map applyCon allmeths) ty
ty_imp <- bindTypeNames [] vars (bindIFace fc ity ty_constr)
substNames vars (map applyCon allmeths) ty
ty_imp <- bindTypeNames [] vars (bindPs params $ bindIFace fc ity ty_constr)
cn <- inCurrentNS n
let tydecl = IClaim fc c vis (if d then [Inline, Invertible]
else [Inline])
(MkImpTy fc cn ty_imp)
let conapp = apply (IVar fc cname)
(map (const (Implicit fc True)) constraints ++
map (IBindVar fc) (map bindName allmeths))
(map (IBindVar fc) (map bindName allmeths))
let argns = getExplicitArgs 0 ty
-- eta expand the RHS so that we put implicits in the right place
let fnclause = PatClause fc (IImplicitApp fc (IVar fc cn)
(Just (UN "__con"))
let fnclause = PatClause fc (INamedApp fc (IVar fc cn)
(UN "__con")
conapp)
(mkLam argns
(apply (IVar fc (methName n))
@ -151,14 +149,14 @@ getMethToplevel {vars} env vis iname cname constraints allmeths params
where
-- Bind the type parameters given explicitly - there might be information
-- in there that we can't infer after all
bindPs : List (Name, RawImp) -> RawImp -> RawImp
bindPs : List (Name, (RigCount, RawImp)) -> RawImp -> RawImp
bindPs [] ty = ty
bindPs ((n, pty) :: ps) ty
= IPi (getFC pty) erased Implicit (Just n) pty (bindPs ps ty)
bindPs ((n, rig, pty) :: ps) ty
= IPi (getFC pty) rig Implicit (Just n) pty (bindPs ps ty)
applyCon : Name -> (Name, RawImp)
applyCon n = (n, IImplicitApp fc (IVar fc n)
(Just (UN "__con")) (IVar fc (UN "__con")))
applyCon n = (n, INamedApp fc (IVar fc n)
(UN "__con") (IVar fc (UN "__con")))
getExplicitArgs : Int -> RawImp -> List Name
getExplicitArgs i (IPi _ _ Explicit n _ sc)
@ -197,9 +195,8 @@ getConstraintHint {vars} fc env vis iname cname constraints meths params (cn, co
(UN ("__" ++ show iname ++ "_" ++ show con))
let tydecl = IClaim fc top vis [Inline, Hint False]
(MkImpTy fc hintname ty_imp)
let conapp = apply (IVar fc cname)
(map (IBindVar fc) (map bindName constraints) ++
map (const (Implicit fc True)) meths)
let conapp = apply (impsBind (IVar fc cname) (map bindName constraints))
(map (const (Implicit fc True)) meths)
let fnclause = PatClause fc (IApp fc (IVar fc hintname) conapp)
(IVar fc (constName cn))
let fndef = IDef fc hintname [fnclause]
@ -213,6 +210,12 @@ getConstraintHint {vars} fc env vis iname cname constraints meths params (cn, co
constName : Name -> Name
constName n = UN (bindName n)
impsBind : RawImp -> List String -> RawImp
impsBind fn [] = fn
impsBind fn (n :: ns)
= impsBind (IAutoApp fc fn (IBindVar fc n)) ns
getSig : ImpDecl -> Maybe (FC, RigCount, List FnOpt, Name, (Bool, RawImp))
getSig (IClaim _ c _ opts (MkImpTy fc n ty))
= Just (fc, c, opts, n, (False, namePis 0 ty))
@ -270,7 +273,7 @@ elabInterface : {vars : _} ->
Env Term vars -> NestedNames vars ->
(constraints : List (Maybe Name, RawImp)) ->
Name ->
(params : List (Name, RawImp)) ->
(params : List (Name, (RigCount, RawImp))) ->
(dets : List Name) ->
(conName : Maybe Name) ->
List ImpDecl ->
@ -299,9 +302,12 @@ elabInterface {vars} fc vis env nest constraints iname params dets mcon body
let implParams = getImplParams ty
updateIfaceSyn ns_iname conName
implParams (map fst params) (map snd constraints)
implParams paramNames (map snd constraints)
ns_meths ds
where
paramNames : List Name
paramNames = map fst params
nameCons : Int -> List (Maybe Name, RawImp) -> List (Name, RawImp)
nameCons i [] = []
nameCons i ((_, ty) :: rest)
@ -366,25 +372,25 @@ elabInterface {vars} fc vis env nest constraints iname params dets mcon body
Just (r, _, _, t) => pure (r, t)
Nothing => throw (GenericMsg fc ("No method named " ++ show n ++ " in interface " ++ show iname))
let ity = apply (IVar fc iname) (map (IVar fc) (map fst params))
let ity = apply (IVar fc iname) (map (IVar fc) paramNames)
-- Substitute the method names with their top level function
-- name, so they don't get implicitly bound in the name
methNameMap <- traverse (\n =>
do cn <- inCurrentNS n
pure (n, applyParams (IVar fc cn)
(map fst params)))
pure (n, applyParams (IVar fc cn) paramNames))
(map fst tydecls)
let dty = substNames vars methNameMap dty
let dty = bindPs params -- bind parameters
$ bindIFace fc ity -- bind interface (?!)
$ substNames vars methNameMap dty
dty_imp <- bindTypeNames [] (map fst tydecls ++ vars)
(bindIFace fc ity dty)
log "elab.interface" 5 $ "Default method " ++ show dn ++ " : " ++ show dty_imp
dty_imp <- bindTypeNames [] (map fst tydecls ++ vars) dty
log "elab.interface.default" 5 $ "Default method " ++ show dn ++ " : " ++ show dty_imp
let dtydecl = IClaim fc rig vis [] (MkImpTy fc dn dty_imp)
processDecl [] nest env dtydecl
let cs' = map (changeName dn) cs
log "elab.interface" 5 $ "Default method body " ++ show cs'
log "elab.interface.default" 5 $ "Default method body " ++ show cs'
processDecl [] nest env (IDef fc dn cs')
-- Reset the original context, we don't need to keep the definition
@ -392,10 +398,17 @@ elabInterface {vars} fc vis env nest constraints iname params dets mcon body
-- put Ctxt orig
pure (n, cs)
where
-- Bind the type parameters given explicitly - there might be information
-- in there that we can't infer after all
bindPs : List (Name, (RigCount, RawImp)) -> RawImp -> RawImp
bindPs [] ty = ty
bindPs ((n, (rig, pty)) :: ps) ty
= IPi (getFC pty) rig Implicit (Just n) pty (bindPs ps ty)
applyParams : RawImp -> List Name -> RawImp
applyParams tm [] = tm
applyParams tm (UN n :: ns)
= applyParams (IImplicitApp fc tm (Just (UN n)) (IBindVar fc n)) ns
= applyParams (INamedApp fc tm (UN n) (IBindVar fc n)) ns
applyParams tm (_ :: ns) = applyParams tm ns
changeNameTerm : Name -> RawImp -> RawImp
@ -403,8 +416,10 @@ elabInterface {vars} fc vis env nest constraints iname params dets mcon body
= if n == n' then IVar fc dn else IVar fc n'
changeNameTerm dn (IApp fc f arg)
= IApp fc (changeNameTerm dn f) arg
changeNameTerm dn (IImplicitApp fc f x arg)
= IImplicitApp fc (changeNameTerm dn f) x arg
changeNameTerm dn (IAutoApp fc f arg)
= IAutoApp fc (changeNameTerm dn f) arg
changeNameTerm dn (INamedApp fc f x arg)
= INamedApp fc (changeNameTerm dn f) x arg
changeNameTerm dn tm = tm
changeName : Name -> ImpClause -> ImpClause
@ -423,7 +438,7 @@ elabInterface {vars} fc vis env nest constraints iname params dets mcon body
chints <- traverse (getConstraintHint fc env vis iname conName
(map fst nconstraints)
meth_names
(map fst params)) nconstraints
paramNames) nconstraints
log "elab.interface" 5 $ "Constraint hints from " ++ show constraints ++ ": " ++ show chints
traverse (processDecl [] nest env) (concatMap snd chints)
traverse_ (\n => do mn <- inCurrentNS n

8
src/Idris/Error.idr
View File

@ -303,12 +303,12 @@ perror (NotRecordType fc ty)
perror (IncompatibleFieldUpdate fc flds)
= pure $ reflow "Field update" <++> concatWith (surround (pretty "->")) (pretty <$> flds)
<++> reflow "not compatible with other updates at" <+> colon <+> line <+> !(ploc fc)
perror (InvalidImplicits fc env [Just n] tm)
= pure $ errorDesc (code (pretty n) <++> reflow "is not a valid implicit argument in" <++> !(pshow env tm)
perror (InvalidArgs fc env [n] tm)
= pure $ errorDesc (code (pretty n) <++> reflow "is not a valid argument in" <++> !(pshow env tm)
<+> dot) <+> line <+> !(ploc fc)
perror (InvalidImplicits fc env ns tm)
perror (InvalidArgs fc env ns tm)
= pure $ errorDesc (concatWith (surround (comma <+> space)) (code . pretty <$> ns)
<++> reflow "are not valid implicit arguments in" <++> !(pshow env tm) <+> dot)
<++> reflow "are not valid arguments in" <++> !(pshow env tm) <+> dot)
<+> line <+> !(ploc fc)
perror (TryWithImplicits fc env imps)
= pure $ errorDesc (reflow "Need to bind implicits"

13
src/Idris/Package.idr
View File

@ -40,6 +40,7 @@ import IdrisPaths
%default covering
public export
record PkgDesc where
constructor MkPkgDesc
name : String
@ -67,6 +68,7 @@ record PkgDesc where
preclean : Maybe (FC, String) -- Script to run before cleaning
postclean : Maybe (FC, String) -- Script to run after cleaning
export
Show PkgDesc where
show pkg = "Package: " ++ name pkg ++ "\n" ++
"Version: " ++ version pkg ++ "\n" ++
@ -496,6 +498,17 @@ runRepl fname = do
displayErrors errs
repl {u} {s}
export
parsePkgFile : {auto c : Ref Ctxt Defs} ->
String -> Core PkgDesc
parsePkgFile file = do
Right (pname, fs) <- coreLift $ parseFile file
(do desc <- parsePkgDesc file
eoi
pure desc)
| Left (FileFail err) => throw (FileErr file err)
| Left err => throw (ParseFail (getParseErrorLoc file err) err)
addFields fs (initPkgDesc pname)
processPackage : {auto c : Ref Ctxt Defs} ->
{auto s : Ref Syn SyntaxInfo} ->

191
src/Idris/Parser.idr
View File

@ -100,13 +100,15 @@ iOperator
= operator <|> (symbol "`" *> name <* symbol "`")
data ArgType
= ExpArg PTerm
| ImpArg (Maybe Name) PTerm
= UnnamedExpArg PTerm
| UnnamedAutoArg PTerm
| NamedArg Name PTerm
| WithArg PTerm
argTerm : ArgType -> PTerm
argTerm (ExpArg t) = t
argTerm (ImpArg _ t) = t
argTerm (UnnamedExpArg t) = t
argTerm (UnnamedAutoArg t) = t
argTerm (NamedArg _ t) = t
argTerm (WithArg t) = t
mutual
@ -114,13 +116,13 @@ mutual
appExpr q fname indents
= case_ fname indents
<|> doBlock fname indents
<|> lambdaCase fname indents
<|> lam fname indents
<|> lazy fname indents
<|> if_ fname indents
<|> with_ fname indents
<|> do b <- bounds (MkPair <$> simpleExpr fname indents <*> many (argExpr q fname indents))
(f, args) <- pure b.val
pure (applyExpImp (start b) (end b) f args)
pure (applyExpImp (start b) (end b) f (concat args))
<|> do b <- bounds (MkPair <$> iOperator <*> expr pdef fname indents)
(op, arg) <- pure b.val
pure (PPrefixOp (boundToFC fname b) op arg)
@ -130,42 +132,55 @@ mutual
List ArgType ->
PTerm
applyExpImp start end f [] = f
applyExpImp start end f (ExpArg exp :: args)
applyExpImp start end f (UnnamedExpArg exp :: args)
= applyExpImp start end (PApp (MkFC fname start end) f exp) args
applyExpImp start end f (ImpArg n imp :: args)
= applyExpImp start end (PImplicitApp (MkFC fname start end) f n imp) args
applyExpImp start end f (UnnamedAutoArg imp :: args)
= applyExpImp start end (PAutoApp (MkFC fname start end) f imp) args
applyExpImp start end f (NamedArg n imp :: args)
= applyExpImp start end (PNamedApp (MkFC fname start end) f n imp) args
applyExpImp start end f (WithArg exp :: args)
= applyExpImp start end (PWithApp (MkFC fname start end) f exp) args
argExpr : ParseOpts -> FileName -> IndentInfo -> Rule ArgType
argExpr : ParseOpts -> FileName -> IndentInfo -> Rule (List ArgType)
argExpr q fname indents
= do continue indents
arg <- simpleExpr fname indents
the (SourceEmptyRule _) $ case arg of
PHole loc _ n => pure (ExpArg (PHole loc True n))
t => pure (ExpArg t)
PHole loc _ n => pure [UnnamedExpArg (PHole loc True n)]
t => pure [UnnamedExpArg t]
<|> do continue indents
arg <- implicitArg fname indents
pure (ImpArg (fst arg) (snd arg))
braceArgs fname indents
<|> if withOK q
then do continue indents
symbol "|"
arg <- expr (record {withOK = False} q) fname indents
pure (WithArg arg)
pure [WithArg arg]
else fail "| not allowed here"
where
braceArgs : FileName -> IndentInfo -> Rule (List ArgType)
braceArgs fname indents
= do start <- bounds (symbol "{")
list <- sepBy (symbol ",")
$ do x <- bounds unqualifiedName
option (NamedArg (UN x.val) $ PRef (boundToFC fname x) (UN x.val))
$ do tm <- symbol "=" *> expr pdef fname indents
pure (NamedArg (UN x.val) tm)
matchAny <- option [] (if isCons list then
do symbol ","
x <- bounds (symbol "_")
pure [NamedArg (UN "_") (PImplicit (boundToFC fname x))]
else fail "non-empty list required")
end <- bounds (symbol "}")
matchAny <- pure $ if isNil list
then [NamedArg (UN "_") (PImplicit (boundToFC fname (mergeBounds start end)))]
else matchAny
pure $ matchAny ++ list
implicitArg : FileName -> IndentInfo -> Rule (Maybe Name, PTerm)
implicitArg fname indents
= do x <- bounds (symbol "{" *> unqualifiedName)
(do tm <- symbol "=" *> commit *> expr pdef fname indents <* symbol "}"
pure (Just (UN x.val), tm))
<|> (do b <- bounds (symbol "}")
pure (Just (UN x.val), PRef (boundToFC fname (mergeBounds x b)) (UN x.val)))
<|> do symbol "@{"
commit
tm <- expr pdef fname indents
symbol "}"
pure (Nothing, tm)
<|> do symbol "@{"
commit
tm <- expr pdef fname indents
symbol "}"
pure [UnnamedAutoArg tm]
with_ : FileName -> IndentInfo -> Rule PTerm
with_ fname indents
@ -401,11 +416,8 @@ mutual
multiplicity : SourceEmptyRule (Maybe Integer)
multiplicity
= do c <- intLit
pure (Just c)
-- <|> do symbol "&"
-- pure (Just 2) -- Borrowing, not implemented
<|> pure Nothing
= optional $ intLit
-- <|> 2 <$ symbol "&" Borrowing, not implemented
getMult : Maybe Integer -> SourceEmptyRule RigCount
getMult (Just 0) = pure erased
@ -522,18 +534,38 @@ mutual
lam : FileName -> IndentInfo -> Rule PTerm
lam fname indents
= do symbol "\\"
binders <- bindList fname indents
symbol "=>"
mustContinue indents Nothing
scope <- expr pdef fname indents
pure (bindAll binders scope)
commit
switch <- optional (bounds $ keyword "case")
case switch of
Nothing => continueLam
Just r => continueLamCase r
where
bindAll : List (RigCount, WithBounds PTerm, PTerm) -> PTerm -> PTerm
bindAll [] scope = scope
bindAll ((rig, pat, ty) :: rest) scope
= PLam (boundToFC fname pat) rig Explicit pat.val ty
(bindAll rest scope)
continueLam : Rule PTerm
continueLam = do
binders <- bindList fname indents
symbol "=>"
mustContinue indents Nothing
scope <- expr pdef fname indents
pure (bindAll binders scope)
continueLamCase : WithBounds () -> Rule PTerm
continueLamCase endCase = do
b <- bounds (forget <$> nonEmptyBlock (caseAlt fname))
pure
(let fc = boundToFC fname b
fcCase = boundToFC fname endCase
n = MN "lcase" 0 in
PLam fcCase top Explicit (PRef fcCase n) (PInfer fcCase) $
PCase fc (PRef fcCase n) b.val)
letBlock : FileName -> IndentInfo -> Rule (WithBounds (Either LetBinder LetDecl))
letBlock fname indents = bounds (letBinder <||> letDecl) where
@ -570,20 +602,6 @@ mutual
(scr, alts) <- pure b.val
pure (PCase (boundToFC fname b) scr alts)
lambdaCase : FileName -> IndentInfo -> Rule PTerm
lambdaCase fname indents
= do b <- bounds (do endCase <- bounds (symbol "\\" *> keyword "case")
commit
alts <- block (caseAlt fname)
pure (endCase, alts))
(endCase, alts) <- pure b.val
pure $
(let fc = boundToFC fname b
fcCase = boundToFC fname endCase
n = MN "lcase" 0 in
PLam fcCase top Explicit (PRef fcCase n) (PInfer fcCase) $
PCase fc (PRef fcCase n) alts)
caseAlt : FileName -> IndentInfo -> Rule PClause
caseAlt fname indents
= do lhs <- bounds (opExpr plhs fname indents)
@ -613,18 +631,18 @@ mutual
record_ : FileName -> IndentInfo -> Rule PTerm
record_ fname indents
= do b <- bounds (do keyword "record"
= do b <- bounds (do kw <- option False (keyword "record" *> pure True) -- TODO deprecated
symbol "{"
commit
fs <- sepBy1 (symbol ",") (field fname indents)
fs <- sepBy1 (symbol ",") (field kw fname indents)
symbol "}"
pure fs)
pure (PUpdate (boundToFC fname b) b.val)
field : FileName -> IndentInfo -> Rule PFieldUpdate
field fname indents
field : Bool -> FileName -> IndentInfo -> Rule PFieldUpdate
field kw fname indents
= do path <- map fieldName <$> [| name :: many recFieldCompat |]
upd <- (symbol "=" *> pure PSetField)
upd <- (ifThenElse kw (symbol "=") (symbol ":=") *> pure PSetField)
<|>
(symbol "$=" *> pure PSetFieldApp)
val <- opExpr plhs fname indents
@ -830,21 +848,14 @@ mkTyConType fc [] = PType fc
mkTyConType fc (x :: xs)
= PPi fc linear Explicit Nothing (PType fc) (mkTyConType fc xs)
mkDataConType : FC -> PTerm -> List ArgType -> PTerm
mkDataConType fc ret [] = ret
mkDataConType fc ret (ExpArg x :: xs)
= PPi fc linear Explicit Nothing x (mkDataConType fc ret xs)
mkDataConType fc ret (ImpArg n (PRef fc' x) :: xs)
= if n == Just x
then PPi fc linear Implicit n (PType fc')
(mkDataConType fc ret xs)
else PPi fc linear Implicit n (PRef fc' x)
(mkDataConType fc ret xs)
mkDataConType fc ret (ImpArg n x :: xs)
= PPi fc linear Implicit n x (mkDataConType fc ret xs)
mkDataConType fc ret (WithArg a :: xs)
= PImplicit fc -- This can't happen because we parse constructors without
-- withOK set
mkDataConType : FC -> PTerm -> List ArgType -> Maybe PTerm
mkDataConType fc ret [] = Just ret
mkDataConType fc ret (UnnamedExpArg x :: xs)
= PPi fc linear Explicit Nothing x <$> mkDataConType fc ret xs
mkDataConType fc ret (UnnamedAutoArg x :: xs)
= PPi fc linear AutoImplicit Nothing x <$> mkDataConType fc ret xs
mkDataConType _ _ _ -- with and named applications not allowed in simple ADTs
= Nothing
simpleCon : FileName -> PTerm -> IndentInfo -> Rule PTypeDecl
simpleCon fname ret indents
@ -854,8 +865,9 @@ simpleCon fname ret indents
pure (cdoc, cname, params))
atEnd indents
(cdoc, cname, params) <- pure b.val
pure (let cfc = boundToFC fname b in
MkPTy cfc cname cdoc (mkDataConType cfc ret params))
let cfc = boundToFC fname b
fromMaybe (fatalError "Named arguments not allowed in ADT constructors")
(pure . MkPTy cfc cname cdoc <$> mkDataConType cfc ret (concat params))
simpleData : FileName -> WithBounds t -> Name -> IndentInfo -> Rule PDataDecl
simpleData fname start n indents
@ -942,6 +954,13 @@ totalityOpt
<|> (keyword "total" *> pure Total)
<|> (keyword "covering" *> pure CoveringOnly)
logLevel : Rule (Maybe LogLevel)
logLevel
= (Nothing <$ exactIdent "off")
<|> do topic <- optional ((:::) <$> unqualifiedName <*> many aDotIdent)
lvl <- intLit
pure (Just (mkLogLevel' topic (fromInteger lvl)))
directive : FileName -> IndentInfo -> Rule Directive
directive fname indents
= do pragma "hide"
@ -953,10 +972,9 @@ directive fname indents
-- atEnd indents
-- pure (Hide True n)
<|> do pragma "logging"
topic <- optional ((:::) <$> unqualifiedName <*> many aDotIdent)
lvl <- intLit
lvl <- logLevel
atEnd indents
pure (Logging (mkLogLevel' topic (fromInteger lvl)))
pure (Logging lvl)
<|> do pragma "auto_lazy"
b <- onoff
atEnd indents
@ -1174,16 +1192,18 @@ implBinds fname indents
pure ((n, rig, tm) :: more)
<|> pure []
ifaceParam : FileName -> IndentInfo -> Rule (List Name, PTerm)
ifaceParam : FileName -> IndentInfo -> Rule (List Name, (RigCount, PTerm))
ifaceParam fname indents
= do symbol "("
m <- multiplicity
rig <- getMult m
ns <- sepBy1 (symbol ",") name
symbol ":"
tm <- expr pdef fname indents
symbol ")"
pure (ns, tm)
pure (ns, (rig, tm))
<|> do n <- bounds name
pure ([n.val], PInfer (boundToFC fname n))
pure ([n.val], (erased, PInfer (boundToFC fname n)))
ifaceDecl : FileName -> IndentInfo -> Rule PDecl
ifaceDecl fname indents
@ -1195,7 +1215,7 @@ ifaceDecl fname indents
cons <- constraints fname indents
n <- name
paramss <- many (ifaceParam fname indents)
let params = concatMap (\ (ns, t) => map (\ n => (n, t)) ns) paramss
let params = concatMap (\ (ns, rt) => map (\ n => (n, rt)) ns) paramss
det <- option []
(do symbol "|"
sepBy (symbol ",") name)
@ -1392,9 +1412,9 @@ collectDefs [] = []
collectDefs (PDef annot cs :: ds)
= let (csWithFC, rest) = spanBy isPDef ds
cs' = cs ++ concat (map snd csWithFC)
annot' = foldr
annot' = foldr
(\fc1, fc2 => fromMaybe EmptyFC (mergeFC fc1 fc2))
annot
annot
(map fst csWithFC)
in
PDef annot' cs' :: assert_total (collectDefs rest)
@ -1759,7 +1779,7 @@ compileArgsCmd parseCmd command doc
tm <- expr pdef "(interactive)" init
pure (command tm n)
loggingArgCmd : ParseCmd -> (LogLevel -> REPLCmd) -> String -> CommandDefinition
loggingArgCmd : ParseCmd -> (Maybe LogLevel -> REPLCmd) -> String -> CommandDefinition
loggingArgCmd parseCmd command doc = (names, Args [StringArg, NumberArg], doc, parse) where
names : List String
@ -1769,9 +1789,8 @@ loggingArgCmd parseCmd command doc = (names, Args [StringArg, NumberArg], doc, p
parse = do
symbol ":"
runParseCmd parseCmd
topic <- optional ((:::) <$> unqualifiedName <*> many aDotIdent)
lvl <- intLit
pure (command (mkLogLevel' topic (fromInteger lvl)))
lvl <- logLevel
pure (command lvl)
parserCommandsForHelp : CommandTable
parserCommandsForHelp =

6
src/Idris/Pretty.idr
View File

@ -218,14 +218,14 @@ mutual
go d (PDelayed _ _ ty) = parenthesise (d > appPrec) $ "Lazy" <++> go appPrec ty
go d (PDelay _ tm) = parenthesise (d > appPrec) $ "Delay" <++> go appPrec tm
go d (PForce _ tm) = parenthesise (d > appPrec) $ "Force" <++> go appPrec tm
go d (PImplicitApp _ f Nothing a) =
go d (PAutoApp _ f a) =
parenthesise (d > appPrec) $ group $ go leftAppPrec f <++> "@" <+> braces (go startPrec a)
go d (PImplicitApp _ f (Just n) (PRef _ a)) =
go d (PNamedApp _ f n (PRef _ a)) =
parenthesise (d > appPrec) $ group $
if n == a
then go leftAppPrec f <++> braces (pretty n)
else go leftAppPrec f <++> braces (pretty n <++> equals <++> pretty a)
go d (PImplicitApp _ f (Just n) a) =
go d (PNamedApp _ f n a) =
parenthesise (d > appPrec) $ group $ go leftAppPrec f <++> braces (pretty n <++> equals <++> go d a)
go d (PSearch _ _) = pragma "%search"
go d (PQuote _ tm) = parenthesise (d > appPrec) $ "`" <+> parens (go startPrec tm)

5
src/Idris/REPL.idr
View File

@ -532,7 +532,7 @@ data REPLResult : Type where
CheckedTotal : List (Name, Totality) -> REPLResult
FoundHoles : List HoleData -> REPLResult
OptionsSet : List REPLOpt -> REPLResult
LogLevelSet : LogLevel -> REPLResult
LogLevelSet : Maybe LogLevel -> REPLResult
ConsoleWidthSet : Maybe Nat -> REPLResult
ColorSet : Bool -> REPLResult
VersionIs : Version -> REPLResult
@ -1019,7 +1019,8 @@ mutual
displayResult (FoundHoles xs) = do
let holes = concatWith (surround (pretty ", ")) (pretty . name <$> xs)
printResult (pretty (length xs) <++> pretty "holes" <+> colon <++> holes)
displayResult (LogLevelSet k) = printResult (reflow "Set loglevel to" <++> pretty k)
displayResult (LogLevelSet Nothing) = printResult (reflow "Logging turned off")
displayResult (LogLevelSet (Just k)) = printResult (reflow "Set log level to" <++> pretty k)
displayResult (ConsoleWidthSet (Just k)) = printResult (reflow "Set consolewidth to" <++> pretty k)
displayResult (ConsoleWidthSet Nothing) = printResult (reflow "Set consolewidth to auto")
displayResult (ColorSet b) = printResult (reflow (if b then "Set color on" else "Set color off"))

19
src/Idris/Resugar.idr
View File

@ -238,13 +238,17 @@ mutual
= do arg' <- toPTerm argPrec arg
app <- toPTermApp fn [(fc, Nothing, arg')]
bracket p appPrec app
toPTerm p (IAutoApp fc fn arg)
= do arg' <- toPTerm argPrec arg
app <- toPTermApp fn [(fc, Just Nothing, arg')]
bracket p appPrec app
toPTerm p (IWithApp fc fn arg)
= do arg' <- toPTerm startPrec arg
fn' <- toPTerm startPrec fn
bracket p appPrec (PWithApp fc fn' arg')
toPTerm p (IImplicitApp fc fn n arg)
toPTerm p (INamedApp fc fn n arg)
= do arg' <- toPTerm startPrec arg
app <- toPTermApp fn [(fc, Just n, arg')]
app <- toPTermApp fn [(fc, Just (Just n), arg')]
imp <- showImplicits
if imp
then bracket p startPrec app
@ -288,10 +292,13 @@ mutual
mkApp fn ((fc, Nothing, arg) :: rest)
= do let ap = sugarApp (PApp fc fn arg)
mkApp ap rest
mkApp fn ((fc, Just n, arg) :: rest)
mkApp fn ((fc, Just Nothing, arg) :: rest)
= do let ap = sugarApp (PAutoApp fc fn arg)
mkApp ap rest
mkApp fn ((fc, Just (Just n), arg) :: rest)
= do imp <- showImplicits
if imp
then do let ap = PImplicitApp fc fn n arg
then do let ap = PNamedApp fc fn n arg
mkApp ap rest
else mkApp fn rest
@ -302,9 +309,9 @@ mutual
toPTermApp (IApp fc f a) args
= do a' <- toPTerm argPrec a
toPTermApp f ((fc, Nothing, a') :: args)
toPTermApp (IImplicitApp fc f n a) args
toPTermApp (INamedApp fc f n a) args
= do a' <- toPTerm startPrec a
toPTermApp f ((fc, Just n, a') :: args)
toPTermApp f ((fc, Just (Just n), a') :: args)
toPTermApp fn@(IVar fc n) args
= do defs <- get Ctxt
case !(lookupCtxtExact n (gamma defs)) of

35
src/Idris/Syntax.idr
View File

@ -13,6 +13,7 @@ import TTImp.TTImp
import Data.ANameMap
import Data.List
import Data.Maybe
import Data.NameMap
import Data.StringMap
import Text.PrettyPrint.Prettyprinter
@ -48,7 +49,8 @@ mutual
PUpdate : FC -> List PFieldUpdate -> PTerm
PApp : FC -> PTerm -> PTerm -> PTerm
PWithApp : FC -> PTerm -> PTerm -> PTerm
PImplicitApp : FC -> PTerm -> (argn : Maybe Name) -> PTerm -> PTerm
PNamedApp : FC -> PTerm -> Name -> PTerm -> PTerm
PAutoApp : FC -> PTerm -> PTerm -> PTerm
PDelayed : FC -> LazyReason -> PTerm -> PTerm
PDelay : FC -> PTerm -> PTerm
@ -115,7 +117,8 @@ mutual
getPTermLoc (PUpdate fc _) = fc
getPTermLoc (PApp fc _ _) = fc
getPTermLoc (PWithApp fc _ _) = fc
getPTermLoc (PImplicitApp fc _ _ _) = fc
getPTermLoc (PAutoApp fc _ _) = fc
getPTermLoc (PNamedApp fc _ _ _) = fc
getPTermLoc (PDelayed fc _ _) = fc
getPTermLoc (PDelay fc _) = fc
getPTermLoc (PForce fc _) = fc
@ -222,7 +225,7 @@ mutual
public export
data Directive : Type where
Hide : Name -> Directive
Logging : LogLevel -> Directive
Logging : Maybe LogLevel -> Directive
LazyOn : Bool -> Directive
UnboundImplicits : Bool -> Directive
AmbigDepth : Nat -> Directive
@ -283,7 +286,7 @@ mutual
(constraints : List (Maybe Name, PTerm)) ->
Name ->
(doc : String) ->
(params : List (Name, PTerm)) ->
(params : List (Name, (RigCount, PTerm))) ->
(det : List Name) ->
(conName : Maybe Name) ->
List PDecl ->
@ -439,7 +442,7 @@ data REPLCmd : Type where
Total : Name -> REPLCmd
Doc : Name -> REPLCmd
Browse : Namespace -> REPLCmd
SetLog : LogLevel -> REPLCmd
SetLog : Maybe LogLevel -> REPLCmd
SetConsoleWidth : Maybe Nat -> REPLCmd
SetColor : Bool -> REPLCmd
Metavars : REPLCmd
@ -537,7 +540,7 @@ mutual
= "record { " ++ showSep ", " (map showUpdate fs) ++ " }"
showPrec d (PApp _ f a) = showPrec App f ++ " " ++ showPrec App a
showPrec d (PWithApp _ f a) = showPrec d f ++ " | " ++ showPrec d a
showPrec d (PImplicitApp _ f Nothing a)
showPrec d (PAutoApp _ f a)
= showPrec d f ++ " @{" ++ showPrec d a ++ "}"
showPrec d (PDelayed _ LInf ty)
= showCon d "Inf" $ showArg ty
@ -547,11 +550,11 @@ mutual
= showCon d "Delay" $ showArg tm
showPrec d (PForce _ tm)
= showCon d "Force" $ showArg tm
showPrec d (PImplicitApp _ f (Just n) (PRef _ a))
showPrec d (PNamedApp _ f n (PRef _ a))
= if n == a
then showPrec d f ++ " {" ++ showPrec d n ++ "}"
else showPrec d f ++ " {" ++ showPrec d n ++ " = " ++ showPrec d a ++ "}"
showPrec d (PImplicitApp _ f (Just n) a)
showPrec d (PNamedApp _ f n a)
= showPrec d f ++ " {" ++ showPrec d n ++ " = " ++ showPrec d a ++ "}"
showPrec _ (PSearch _ _) = "%search"
showPrec d (PQuote _ tm) = "`(" ++ showPrec d tm ++ ")"
@ -803,10 +806,14 @@ mapPTermM f = goPTerm where
PWithApp fc <$> goPTerm x
<*> goPTerm y
>>= f
goPTerm (PImplicitApp fc x argn y) =
PImplicitApp fc <$> goPTerm x
<*> pure argn
<*> goPTerm y
goPTerm (PAutoApp fc x y) =
PAutoApp fc <$> goPTerm x
<*> goPTerm y
>>= f
goPTerm (PNamedApp fc x n y) =
PNamedApp fc <$> goPTerm x
<*> pure n
<*> goPTerm y
>>= f
goPTerm (PDelayed fc x y) =
PDelayed fc x <$> goPTerm y
@ -966,11 +973,11 @@ mapPTermM f = goPTerm where
PUsing fc <$> goPairedPTerms mnts
<*> goPDecls ps
goPDecl (PReflect fc t) = PReflect fc <$> goPTerm t
goPDecl (PInterface fc v mnts n doc nts ns mn ps) =
goPDecl (PInterface fc v mnts n doc nrts ns mn ps) =
PInterface fc v <$> goPairedPTerms mnts
<*> pure n
<*> pure doc
<*> goPairedPTerms nts
<*> go3TupledPTerms nrts
<*> pure ns
<*> pure mn
<*> goPDecls ps

21
src/Parser/Unlit.idr
View File

@ -17,18 +17,25 @@ styleOrg : LiterateStyle
styleOrg = MkLitStyle
[ ("#+BEGIN_SRC idris","#+END_SRC")
, ("#+begin_src idris","#+end_src")
, ("#+COMMENT idris","#+END_COMMENT")
, ("#+comment idris","#+end_comment")]
, ("#+BEGIN_COMMENT idris","#+END_COMMENT")
, ("#+begin_comment idris","#+end_comment")]
["#+IDRIS:"]
[".org"]
export
styleCMark : LiterateStyle
styleCMark = MkLitStyle
[("```idris", "```"), ("~~~idris", "~~~")]
[("```idris", "```"), ("~~~idris", "~~~"), ("<!-- idris", "-->")]
Nil
[".md", ".markdown"]
export
styleTeX : LiterateStyle
styleTeX = MkLitStyle
[("\\begin{code}", "\\end{code}"), ("\\begin{hidden}", "\\end{hidden}")]
Nil
[".tex", ".ltx"]
export
isLitFile : String -> Maybe LiterateStyle
isLitFile fname =
@ -36,7 +43,9 @@ isLitFile fname =
Just s => Just s
Nothing => case isStyle styleOrg of
Just s => Just s
Nothing => isStyle styleCMark
Nothing => case isStyle styleCMark of
Just s => Just s
Nothing => isStyle styleTeX
where
hasSuffix : String -> Bool
@ -57,7 +66,9 @@ isLitLine str =
(Just l, s) => (Just l, s)
otherwise => case isLiterateLine styleCMark str of
(Just l, s) => (Just l, s)
otherwise => (Nothing, str)
otherwise => case isLiterateLine styleTeX str of
(Just l, s) => (Just l, s)
otherwise => (Nothing, str)
export
unlit : Maybe LiterateStyle -> String -> Either LiterateError String

12
src/TTImp/BindImplicits.idr
View File

@ -37,8 +37,10 @@ renameIBinds rs us (ILam fc c p n ty sc)
= pure $ ILam fc c p n !(renameIBinds rs us ty) !(renameIBinds rs us sc)
renameIBinds rs us (IApp fc fn arg)
= pure $ IApp fc !(renameIBinds rs us fn) !(renameIBinds rs us arg)
renameIBinds rs us (IImplicitApp fc fn n arg)
= pure $ IImplicitApp fc !(renameIBinds rs us fn) n !(renameIBinds rs us arg)
renameIBinds rs us (IAutoApp fc fn arg)
= pure $ IAutoApp fc !(renameIBinds rs us fn) !(renameIBinds rs us arg)
renameIBinds rs us (INamedApp fc fn n arg)
= pure $ INamedApp fc !(renameIBinds rs us fn) n !(renameIBinds rs us arg)
renameIBinds rs us (IWithApp fc fn arg)
= pure $ IWithApp fc !(renameIBinds rs us fn) !(renameIBinds rs us arg)
renameIBinds rs us (IAs fc s n pat)
@ -86,8 +88,10 @@ doBind ns (ILam fc rig p mn aty sc)
ILam fc rig p mn (doBind ns' aty) (doBind ns' sc)
doBind ns (IApp fc fn av)
= IApp fc (doBind ns fn) (doBind ns av)
doBind ns (IImplicitApp fc fn n av)
= IImplicitApp fc (doBind ns fn) n (doBind ns av)
doBind ns (IAutoApp fc fn av)
= IAutoApp fc (doBind ns fn) (doBind ns av)
doBind ns (INamedApp fc fn n av)
= INamedApp fc (doBind ns fn) n (doBind ns av)
doBind ns (IWithApp fc fn av)
= IWithApp fc (doBind ns fn) (doBind ns av)
doBind ns (IAs fc s n pat)

16
src/TTImp/Elab/Ambiguity.idr
View File

@ -97,8 +97,10 @@ expandAmbigName mode nest env orig args (IVar fc x) exp
buildAlt f [] = f
buildAlt f ((fc', Nothing, a) :: as)
= buildAlt (IApp fc' f a) as
buildAlt f ((fc', Just i, a) :: as)
= buildAlt (IImplicitApp fc' f i a) as
buildAlt f ((fc', Just Nothing, a) :: as)
= buildAlt (IAutoApp fc' f a) as
buildAlt f ((fc', Just (Just i), a) :: as)
= buildAlt (INamedApp fc' f i a) as
isPrimName : List Name -> Name -> Bool
isPrimName [] fn = False
@ -144,9 +146,12 @@ expandAmbigName mode nest env orig args (IVar fc x) exp
expandAmbigName mode nest env orig args (IApp fc f a) exp
= expandAmbigName mode nest env orig
((fc, Nothing, a) :: args) f exp
expandAmbigName mode nest env orig args (IImplicitApp fc f n a) exp
expandAmbigName mode nest env orig args (INamedApp fc f n a) exp
= expandAmbigName mode nest env orig
((fc, Just n, a) :: args) f exp
((fc, Just (Just n), a) :: args) f exp
expandAmbigName mode nest env orig args (IAutoApp fc f a) exp
= expandAmbigName mode nest env orig
((fc, Just Nothing, a) :: args) f exp
expandAmbigName elabmode nest env orig args tm exp
= do log "elab.ambiguous" 10 $ "No ambiguity " ++ show orig
pure orig
@ -315,7 +320,8 @@ checkAmbigDepth fc info
getName : RawImp -> Maybe Name
getName (IVar _ n) = Just n
getName (IApp _ f _) = getName f
getName (IImplicitApp _ f _ _) = getName f
getName (INamedApp _ f _ _) = getName f
getName (IAutoApp _ f _) = getName f
getName _ = Nothing
export

242
src/TTImp/Elab/App.idr
View File

@ -15,6 +15,7 @@ import TTImp.Elab.Check
import TTImp.TTImp
import Data.List
import Data.List1
import Data.Maybe
%default covering
@ -139,11 +140,12 @@ mutual
Name -> NF vars -> (Defs -> Closure vars -> Core (NF vars)) ->
(argdata : (Maybe Name, Nat)) ->
(expargs : List RawImp) ->
(impargs : List (Maybe Name, RawImp)) ->
(autoargs : List RawImp) ->
(namedargs : List (Name, RawImp)) ->
(knownret : Bool) ->
(expected : Maybe (Glued vars)) ->
Core (Term vars, Glued vars)
makeImplicit rig argRig elabinfo nest env fc tm x aty sc (n, argpos) expargs impargs kr expty
makeImplicit rig argRig elabinfo nest env fc tm x aty sc (n, argpos) expargs autoargs namedargs kr expty
= do defs <- get Ctxt
nm <- genMVName x
empty <- clearDefs defs
@ -155,7 +157,7 @@ mutual
do est <- get EST
put EST (addBindIfUnsolved nm argRig Implicit env metaval metaty est)
checkAppWith rig elabinfo nest env fc
fntm fnty (n, 1 + argpos) expargs impargs kr expty
fntm fnty (n, 1 + argpos) expargs autoargs namedargs kr expty
makeAutoImplicit : {vars : _} ->
{auto c : Ref Ctxt Defs} ->
@ -168,11 +170,12 @@ mutual
Name -> NF vars -> (Defs -> Closure vars -> Core (NF vars)) ->
(argpos : (Maybe Name, Nat)) ->
(expargs : List RawImp) ->
(impargs : List (Maybe Name, RawImp)) ->
(autoargs : List RawImp) ->
(namedargs : List (Name, RawImp)) ->
(knownret : Bool) ->
(expected : Maybe (Glued vars)) ->
Core (Term vars, Glued vars)
makeAutoImplicit rig argRig elabinfo nest env fc tm x aty sc (n, argpos) expargs impargs kr expty
makeAutoImplicit rig argRig elabinfo nest env fc tm x aty sc (n, argpos) expargs autoargs namedargs kr expty
-- on the LHS, just treat it as an implicit pattern variable.
-- on the RHS, add a searchable hole
= if metavarImp (elabMode elabinfo)
@ -186,7 +189,7 @@ mutual
est <- get EST
put EST (addBindIfUnsolved nm argRig AutoImplicit env metaval metaty est)
checkAppWith rig elabinfo nest env fc
fntm fnty (n, 1 + argpos) expargs impargs kr expty
fntm fnty (n, 1 + argpos) expargs autoargs namedargs kr expty
else do defs <- get Ctxt
nm <- genMVName x
-- We need the full normal form to check determining arguments
@ -199,7 +202,7 @@ mutual
let fntm = App fc tm metaval
fnty <- sc defs (toClosure defaultOpts env metaval)
checkAppWith rig elabinfo nest env fc
fntm fnty (n, 1 + argpos) expargs impargs kr expty
fntm fnty (n, 1 + argpos) expargs autoargs namedargs kr expty
where
metavarImp : ElabMode -> Bool
metavarImp (InLHS _) = True
@ -218,11 +221,12 @@ mutual
(Defs -> Closure vars -> Core (NF vars)) ->
(argpos : (Maybe Name, Nat)) ->
(expargs : List RawImp) ->
(impargs : List (Maybe Name, RawImp)) ->
(autoargs : List RawImp) ->
(namedargs : List (Name, RawImp)) ->
(knownret : Bool) ->
(expected : Maybe (Glued vars)) ->
Core (Term vars, Glued vars)
makeDefImplicit rig argRig elabinfo nest env fc tm x arg aty sc (n, argpos) expargs impargs kr expty
makeDefImplicit rig argRig elabinfo nest env fc tm x arg aty sc (n, argpos) expargs autoargs namedargs kr expty
-- on the LHS, just treat it as an implicit pattern variable.
-- on the RHS, use the default
= if metavarImp (elabMode elabinfo)
@ -236,14 +240,14 @@ mutual
est <- get EST
put EST (addBindIfUnsolved nm argRig AutoImplicit env metaval metaty est)
checkAppWith rig elabinfo nest env fc
fntm fnty (n, 1 + argpos) expargs impargs kr expty
fntm fnty (n, 1 + argpos) expargs autoargs namedargs kr expty
else do defs <- get Ctxt
empty <- clearDefs defs
aval <- quote empty env arg
let fntm = App fc tm aval
fnty <- sc defs (toClosure defaultOpts env aval)
checkAppWith rig elabinfo nest env fc
fntm fnty (n, 1 + argpos) expargs impargs kr expty
fntm fnty (n, 1 + argpos) expargs autoargs namedargs kr expty
where
metavarImp : ElabMode -> Bool
metavarImp (InLHS _) = True
@ -262,7 +266,8 @@ mutual
(_ :: _ :: _) => True
_ => False
needsDelayExpr True (IApp _ f _) = needsDelayExpr True f
needsDelayExpr True (IImplicitApp _ f _ _) = needsDelayExpr True f
needsDelayExpr True (IAutoApp _ f _) = needsDelayExpr True f
needsDelayExpr True (INamedApp _ f _ _) = needsDelayExpr True f
needsDelayExpr True (ILam _ _ _ _ _ _) = pure True
needsDelayExpr True (ICase _ _ _ _) = pure True
needsDelayExpr True (ILocal _ _ _) = pure True
@ -279,7 +284,8 @@ mutual
RawImp -> Core Bool
needsDelayLHS (IVar fc n) = pure True
needsDelayLHS (IApp _ f _) = needsDelayLHS f
needsDelayLHS (IImplicitApp _ f _ _) = needsDelayLHS f
needsDelayLHS (IAutoApp _ f _) = needsDelayLHS f
needsDelayLHS (INamedApp _ f _ _) = needsDelayLHS f
needsDelayLHS (IAlternative _ _ _) = pure True
needsDelayLHS (ISearch _ _) = pure True
needsDelayLHS (IPrimVal _ _) = pure True
@ -377,12 +383,13 @@ mutual
(argdata : (Maybe Name, Nat)) ->
(arg : RawImp) ->
(expargs : List RawImp) ->
(impargs : List (Maybe Name, RawImp)) ->
(autoargs : List RawImp) ->
(namedargs : List (Name, RawImp)) ->
(knownret : Bool) ->
(expected : Maybe (Glued vars)) ->
Core (Term vars, Glued vars)
checkRestApp rig argRig elabinfo nest env fc tm x aty sc
(n, argpos) arg_in expargs impargs knownret expty
(n, argpos) arg_in expargs autoargs namedargs knownret expty
= do defs <- get Ctxt
arg <- dotErased aty n argpos (elabMode elabinfo) argRig arg_in
kr <- if knownret
@ -399,7 +406,7 @@ mutual
logTerm "elab" 10 "...as" metaval
fnty <- sc defs (toClosure defaultOpts env metaval)
(tm, gty) <- checkAppWith rig elabinfo nest env fc
fntm fnty (n, 1 + argpos) expargs impargs kr expty
fntm fnty (n, 1 + argpos) expargs autoargs namedargs kr expty
defs <- get Ctxt
aty' <- nf defs env metaty
logNF "elab" 10 ("Now trying " ++ show nm ++ " " ++ show arg) env aty'
@ -448,7 +455,25 @@ mutual
let fntm = App fc tm argv
fnty <- sc defs (toClosure defaultOpts env argv)
checkAppWith rig elabinfo nest env fc
fntm fnty (n, 1 + argpos) expargs impargs kr expty
fntm fnty (n, 1 + argpos) expargs autoargs namedargs kr expty
export
findNamed : Name -> List (Name, RawImp) -> Maybe (List1 (Name, RawImp))
findNamed n l = case partition ((== n) . fst) l of
(x :: xs, ys) => Just (x ::: (xs ++ ys))
_ => Nothing
export
findBindAllExpPattern : List (Name, RawImp) -> Maybe RawImp
findBindAllExpPattern = lookup (UN "_")
isImplicitAs : RawImp -> Bool
isImplicitAs (IAs _ UseLeft _ (Implicit _ _)) = True
isImplicitAs _ = False
isBindAllExpPattern : Name -> Bool
isBindAllExpPattern (UN "_") = True
isBindAllExpPattern _ = False
-- Check an application of 'fntm', with type 'fnty' to the given list
-- of explicit and implicit arguments.
@ -465,25 +490,51 @@ mutual
-- function we're applying, and argument position, for
-- checking if it's okay to erase against 'safeErase'
(expargs : List RawImp) ->
(impargs : List (Maybe Name, RawImp)) ->
(autoargs : List RawImp) ->
(namedargs : List (Name, RawImp)) ->
(knownret : Bool) -> -- Do we know what the return type is yet?
-- if we do, we might be able to use it to work
-- out the types of arguments before elaborating them
(expected : Maybe (Glued vars)) ->
Core (Term vars, Glued vars)
-- Ordinary explicit argument
checkAppWith rig elabinfo nest env fc tm (NBind tfc x (Pi _ rigb Explicit aty) sc)
argdata (arg :: expargs) impargs kr expty
= do let argRig = rig |*| rigb
checkRestApp rig argRig elabinfo nest env fc
tm x aty sc argdata arg expargs impargs kr expty
-- Explicit Pi, we use provided unnamed explicit argument
checkAppWith rig elabinfo nest env fc tm ty@(NBind tfc x (Pi _ rigb Explicit aty) sc)
argdata (arg :: expargs') autoargs namedargs kr expty
= do let argRig = rig |*| rigb
checkRestApp rig argRig elabinfo nest env fc
tm x aty sc argdata arg expargs' autoargs namedargs kr expty
checkAppWith rig elabinfo nest env fc tm ty@(NBind tfc x (Pi _ rigb Explicit aty) sc)
argdata [] autoargs namedargs kr expty with (findNamed x namedargs)
-- We found a compatible named argument
checkAppWith rig elabinfo nest env fc tm ty@(NBind tfc x (Pi _ rigb Explicit aty) sc)
argdata [] autoargs namedargs kr expty | Just ((_, arg) ::: namedargs')
= do let argRig = rig |*| rigb
checkRestApp rig argRig elabinfo nest env fc
tm x aty sc argdata arg [] autoargs namedargs' kr expty
checkAppWith rig elabinfo nest env fc tm ty@(NBind tfc x (Pi _ rigb Explicit aty) sc)
argdata [] autoargs namedargs kr expty | Nothing
= case findBindAllExpPattern namedargs of
Just arg => -- Bind-all-explicit pattern is present - implicitly bind
do let argRig = rig |*| rigb
checkRestApp rig argRig elabinfo nest env fc
tm x aty sc argdata arg [] autoargs namedargs kr expty
_ =>
do defs <- get Ctxt
if all isImplicitAs (autoargs
++ map snd (filter (not . isBindAllExpPattern . fst) namedargs))
-- Only non-user implicit `as` bindings added by
-- the compiler are allowed here
then -- We are done
checkExp rig elabinfo env fc tm (glueBack defs env ty) expty
else -- Some user defined binding is present while we are out of explicit arguments, that's an error
throw (InvalidArgs fc env (map (const (UN "<auto>")) autoargs ++ map fst namedargs) tm)
-- Function type is delayed, so force the term and continue
checkAppWith rig elabinfo nest env fc tm (NDelayed dfc r ty@(NBind _ _ (Pi _ _ _ _) sc)) argdata expargs impargs kr expty
= checkAppWith rig elabinfo nest env fc (TForce dfc r tm) ty argdata expargs impargs kr expty
checkAppWith rig elabinfo nest env fc tm (NDelayed dfc r ty@(NBind _ _ (Pi _ _ _ _) sc)) argdata expargs autoargs namedargs kr expty
= checkAppWith rig elabinfo nest env fc (TForce dfc r tm) ty argdata expargs autoargs namedargs kr expty
-- If there's no more arguments given, and the plicities of the type and
-- the expected type line up, stop
checkAppWith rig elabinfo nest env fc tm ty@(NBind tfc x (Pi _ rigb Implicit aty) sc)
argdata [] [] kr (Just expty_in)
argdata [] [] [] kr (Just expty_in)
= do let argRig = rig |*| rigb
expty <- getNF expty_in
defs <- get Ctxt
@ -491,22 +542,24 @@ mutual
NBind tfc' x' (Pi _ rigb' Implicit aty') sc'
=> checkExp rig elabinfo env fc tm (glueBack defs env ty) (Just expty_in)
_ => if not (preciseInf elabinfo)
then makeImplicit rig argRig elabinfo nest env fc tm x aty sc argdata [] [] kr (Just expty_in)
then makeImplicit rig argRig elabinfo nest env fc tm x aty sc argdata [] [] [] kr (Just expty_in)
-- in 'preciseInf' mode blunder on anyway, and hope
-- that we can resolve the implicits
else handle (checkExp rig elabinfo env fc tm (glueBack defs env ty) (Just expty_in))
(\err => makeImplicit rig argRig elabinfo nest env fc tm x aty sc argdata [] [] kr (Just expty_in))
(\err => makeImplicit rig argRig elabinfo nest env fc tm x aty sc argdata [] [] [] kr (Just expty_in))
-- Same for auto
checkAppWith rig elabinfo nest env fc tm ty@(NBind tfc x (Pi _ rigb AutoImplicit aty) sc)
argdata [] [] kr (Just expty_in)
argdata [] [] [] kr (Just expty_in)
= do let argRig = rig |*| rigb
expty <- getNF expty_in
defs <- get Ctxt
case expty of
NBind tfc' x' (Pi _ rigb' AutoImplicit aty') sc'
=> checkExp rig elabinfo env fc tm (glueBack defs env ty) (Just expty_in)
_ => makeAutoImplicit rig argRig elabinfo nest env fc tm x aty sc argdata [] [] kr (Just expty_in)
_ => makeAutoImplicit rig argRig elabinfo nest env fc tm x aty sc argdata [] [] [] kr (Just expty_in)
-- Same for default
checkAppWith rig elabinfo nest env fc tm ty@(NBind tfc x (Pi _ rigb (DefImplicit aval) aty) sc)
argdata [] [] kr (Just expty_in)
argdata [] [] [] kr (Just expty_in)
= do let argRig = rigMult rig rigb
expty <- getNF expty_in
defs <- get Ctxt
@ -514,86 +567,47 @@ mutual
NBind tfc' x' (Pi _ rigb' (DefImplicit aval') aty') sc'
=> if !(convert defs env aval aval')
then checkExp rig elabinfo env fc tm (glueBack defs env ty) (Just expty_in)
else makeDefImplicit rig argRig elabinfo nest env fc tm x aval aty sc argdata [] [] kr (Just expty_in)
_ => makeDefImplicit rig argRig elabinfo nest env fc tm x aval aty sc argdata [] [] kr (Just expty_in)
else makeDefImplicit rig argRig elabinfo nest env fc tm x aval aty sc argdata [] [] [] kr (Just expty_in)
_ => makeDefImplicit rig argRig elabinfo nest env fc tm x aval aty sc argdata [] [] [] kr (Just expty_in)
-- Check next auto implicit argument
-- Check next unnamed auto implicit argument
checkAppWith rig elabinfo nest env fc tm (NBind tfc x (Pi _ rigb AutoImplicit aty) sc)
argdata expargs impargs kr expty
argdata expargs (arg :: autoargs') namedargs kr expty
= checkRestApp rig (rig |*| rigb) elabinfo nest env fc
tm x aty sc argdata arg expargs autoargs' namedargs kr expty
-- Check next named auto implicit argument
checkAppWith rig elabinfo nest env fc tm (NBind tfc x (Pi _ rigb AutoImplicit aty) sc)
argdata expargs [] namedargs kr expty
= let argRig = rig |*| rigb in
case useAutoImp [] impargs of
Nothing => makeAutoImplicit rig argRig elabinfo nest env fc tm
x aty sc argdata expargs impargs kr expty
Just (arg, impargs') =>
checkRestApp rig argRig elabinfo nest env fc
tm x aty sc argdata arg expargs impargs' kr expty
where
useAutoImp : List (Maybe Name, RawImp) -> List (Maybe Name, RawImp) ->
Maybe (RawImp, List (Maybe Name, RawImp))
useAutoImp acc [] = Nothing
useAutoImp acc ((Nothing, xtm) :: rest)
= Just (xtm, reverse acc ++ rest)
useAutoImp acc ((Just x', xtm) :: rest)
= if x == x'
then Just (xtm, reverse acc ++ rest)
else useAutoImp ((Just x', xtm) :: acc) rest
useAutoImp acc (ximp :: rest)
= useAutoImp (ximp :: acc) rest
case findNamed x namedargs of
Just ((_, arg) ::: namedargs') =>
checkRestApp rig argRig elabinfo nest env fc
tm x aty sc argdata arg expargs [] namedargs' kr expty
Nothing =>
makeAutoImplicit rig argRig elabinfo nest env fc tm
x aty sc argdata expargs [] namedargs kr expty
-- Check next implicit argument
checkAppWith rig elabinfo nest env fc tm (NBind tfc x (Pi _ rigb Implicit aty) sc)
argdata expargs impargs kr expty
argdata expargs autoargs namedargs kr expty
= let argRig = rig |*| rigb in
case useImp [] impargs of
case findNamed x namedargs of
Nothing => makeImplicit rig argRig elabinfo nest env fc tm
x aty sc argdata expargs impargs kr expty
Just (arg, impargs') =>
x aty sc argdata expargs autoargs namedargs kr expty
Just ((_, arg) ::: namedargs') =>
checkRestApp rig argRig elabinfo nest env fc
tm x aty sc argdata arg expargs impargs' kr expty
where
useImp : List (Maybe Name, RawImp) -> List (Maybe Name, RawImp) ->
Maybe (RawImp, List (Maybe Name, RawImp))
useImp acc [] = Nothing
useImp acc ((Just x', xtm) :: rest)
= if x == x'
then Just (xtm, reverse acc ++ rest)
else useImp ((Just x', xtm) :: acc) rest
useImp acc (ximp :: rest)
= useImp (ximp :: acc) rest
tm x aty sc argdata arg expargs autoargs namedargs' kr expty
-- Check next default argument
checkAppWith rig elabinfo nest env fc tm (NBind tfc x (Pi _ rigb (DefImplicit arg) aty) sc)
argdata expargs impargs kr expty
argdata expargs autoargs namedargs kr expty
= let argRig = rigMult rig rigb in
case useImp [] impargs of
case findNamed x namedargs of
Nothing => makeDefImplicit rig argRig elabinfo nest env fc tm
x arg aty sc argdata expargs impargs kr expty
Just (arg, impargs') =>
x arg aty sc argdata expargs autoargs namedargs kr expty
Just ((_, arg) ::: namedargs') =>
checkRestApp rig argRig elabinfo nest env fc
tm x aty sc argdata arg expargs impargs' kr expty
where
useImp : List (Maybe Name, RawImp) -> List (Maybe Name, RawImp) ->
Maybe (RawImp, List (Maybe Name, RawImp))
useImp acc [] = Nothing
useImp acc ((Just x', xtm) :: rest)
= if x == x'
then Just (xtm, reverse acc ++ rest)
else useImp ((Just x', xtm) :: acc) rest
useImp acc (ximp :: rest)
= useImp (ximp :: acc) rest
checkAppWith rig elabinfo nest env fc tm ty argdata [] [] kr expty
= do defs <- get Ctxt
checkExp rig elabinfo env fc tm (glueBack defs env ty) expty
checkAppWith rig elabinfo nest env fc tm ty argdata [] impargs kr expty
= case filter notInfer impargs of
[] => checkAppWith rig elabinfo nest env fc tm ty argdata [] [] kr expty
is => throw (InvalidImplicits fc env (map fst is) tm)
where
notInfer : (Maybe Name, RawImp) -> Bool
notInfer (_, Implicit _ _) = False
notInfer (n, IAs _ _ _ i) = notInfer (n, i)
notInfer _ = True
checkAppWith {vars} rig elabinfo nest env fc tm ty (n, argpos) (arg :: expargs) impargs kr expty
tm x aty sc argdata arg expargs autoargs namedargs' kr expty
-- Invent a function type if we have extra explicit arguments but type is further unknown
checkAppWith {vars} rig elabinfo nest env fc tm ty (n, argpos) (arg :: expargs) autoargs namedargs kr expty
= -- Invent a function type, and hope that we'll know enough to solve it
-- later when we unify with expty
do logNF "elab.with" 10 "Function type" env ty
@ -613,13 +627,20 @@ mutual
let expfnty = gnf env (Bind fc argn (Pi fc top Explicit argTy) (weaken retTy))
logGlue "elab.with" 10 "Expected function type" env expfnty
maybe (pure ()) (logGlue "elab.with" 10 "Expected result type" env) expty
res <- checkAppWith rig elabinfo nest env fc fntm fnty (n, 1 + argpos) expargs impargs kr expty
res <- checkAppWith rig elabinfo nest env fc fntm fnty (n, 1 + argpos) expargs autoargs namedargs kr expty
cres <- Check.convert fc elabinfo env (glueBack defs env ty) expfnty
let [] = constraints cres
| cs => do cty <- getTerm expfnty
ctm <- newConstant fc rig env (fst res) cty cs
pure (ctm, gnf env retTy)
pure res
-- Only non-user implicit `as` bindings are allowed to be present as arguments at this stage
checkAppWith rig elabinfo nest env fc tm ty argdata [] autoargs namedargs kr expty
= do defs <- get Ctxt
if all isImplicitAs (autoargs ++ map snd (filter (not . isBindAllExpPattern . fst) namedargs))
then checkExp rig elabinfo env fc tm (glueBack defs env ty) expty
else throw (InvalidArgs fc env (map (const (UN "<auto>")) autoargs ++ map fst namedargs) tm)
export
checkApp : {vars : _} ->
@ -631,14 +652,17 @@ checkApp : {vars : _} ->
NestedNames vars -> Env Term vars ->
FC -> (fn : RawImp) ->
(expargs : List RawImp) ->
(impargs : List (Maybe Name, RawImp)) ->
(autoargs : List RawImp) ->
(namedargs : List (Name, RawImp)) ->
Maybe (Glued vars) ->
Core (Term vars, Glued vars)
checkApp rig elabinfo nest env fc (IApp fc' fn arg) expargs impargs exp
= checkApp rig elabinfo nest env fc' fn (arg :: expargs) impargs exp
checkApp rig elabinfo nest env fc (IImplicitApp fc' fn nm arg) expargs impargs exp
= checkApp rig elabinfo nest env fc' fn expargs ((nm, arg) :: impargs) exp
checkApp rig elabinfo nest env fc (IVar fc' n) expargs impargs exp
checkApp rig elabinfo nest env fc (IApp fc' fn arg) expargs autoargs namedargs exp
= checkApp rig elabinfo nest env fc' fn (arg :: expargs) autoargs namedargs exp
checkApp rig elabinfo nest env fc (IAutoApp fc' fn arg) expargs autoargs namedargs exp
= checkApp rig elabinfo nest env fc' fn expargs (arg :: autoargs) namedargs exp
checkApp rig elabinfo nest env fc (INamedApp fc' fn nm arg) expargs autoargs namedargs exp
= checkApp rig elabinfo nest env fc' fn expargs autoargs ((nm, arg) :: namedargs) exp
checkApp rig elabinfo nest env fc (IVar fc' n) expargs autoargs namedargs exp
= do (ntm, arglen, nty_in) <- getVarType rig nest env fc n
nty <- getNF nty_in
prims <- getPrimitiveNames
@ -661,7 +685,7 @@ checkApp rig elabinfo nest env fc (IVar fc' n) expargs impargs exp
Just (Just n', _) => n'
_ => n
normalisePrims prims env
!(checkAppWith rig elabinfo nest env fc ntm nty (Just fn, arglen) expargs impargs False exp)
!(checkAppWith rig elabinfo nest env fc ntm nty (Just fn, arglen) expargs autoargs namedargs False exp)
where
-- If the term is an application of a primitive conversion (fromInteger etc)
@ -697,7 +721,7 @@ checkApp rig elabinfo nest env fc (IVar fc' n) expargs impargs exp
else pure elabinfo
updateElabInfo _ _ _ _ info = pure info
checkApp rig elabinfo nest env fc fn expargs impargs exp
checkApp rig elabinfo nest env fc fn expargs autoargs namedargs exp
= do (fntm, fnty_in) <- checkImp rig elabinfo nest env fn Nothing
fnty <- getNF fnty_in
checkAppWith rig elabinfo nest env fc fntm fnty (Nothing, 0) expargs impargs False exp
checkAppWith rig elabinfo nest env fc fntm fnty (Nothing, 0) expargs autoargs namedargs False exp

2
src/TTImp/Elab/Case.idr
View File

@ -405,7 +405,7 @@ checkCase rig elabinfo nest env fc scr scrty_in alts exp
= applyTo defs (IApp fc ty (Implicit fc False))
!(sc defs (toClosure defaultOpts [] (Erased fc False)))
applyTo defs ty (NBind _ x (Pi _ _ _ _) sc)
= applyTo defs (IImplicitApp fc ty (Just x) (Implicit fc False))
= applyTo defs (INamedApp fc ty x (Implicit fc False))
!(sc defs (toClosure defaultOpts [] (Erased fc False)))
applyTo defs ty _ = pure ty

6
src/TTImp/Elab/Quote.idr
View File

@ -42,8 +42,10 @@ mutual
= pure $ IUpdate fc !(traverse getUnquoteUpdate ds) !(getUnquote sc)
getUnquote (IApp fc f a)
= pure $ IApp fc !(getUnquote f) !(getUnquote a)
getUnquote (IImplicitApp fc f n a)
= pure $ IImplicitApp fc !(getUnquote f) n !(getUnquote a)
getUnquote (IAutoApp fc f a)
= pure $ IAutoApp fc !(getUnquote f) !(getUnquote a)
getUnquote (INamedApp fc f n a)
= pure $ INamedApp fc !(getUnquote f) n !(getUnquote a)
getUnquote (IWithApp fc f a)
= pure $ IWithApp fc !(getUnquote f) !(getUnquote a)
getUnquote (IAlternative fc at as)

3
src/TTImp/Elab/Record.idr
View File

@ -15,6 +15,7 @@ import TTImp.Elab.Delayed
import TTImp.TTImp
import Data.List
import Data.Maybe
%default covering
@ -39,7 +40,7 @@ applyImp f [] = f
applyImp f ((Nothing, arg) :: xs)
= applyImp (IApp (getFC f) f arg) xs
applyImp f ((Just n, arg) :: xs)
= applyImp (IImplicitApp (getFC f) f (Just n) arg) xs
= applyImp (INamedApp (getFC f) f n arg) xs
toLHS' : FC -> Rec -> (Maybe Name, RawImp)
toLHS' loc (Field mn@(Just _) n _)

10
src/TTImp/Elab/Term.idr
View File

@ -125,7 +125,7 @@ checkTerm rig elabinfo nest env (IVar fc n) exp
= -- It may actually turn out to be an application, if the expected
-- type is expecting an implicit argument, so check it as an
-- application with no arguments
checkApp rig elabinfo nest env fc (IVar fc n) [] [] exp
checkApp rig elabinfo nest env fc (IVar fc n) [] [] [] exp
checkTerm rig elabinfo nest env (IPi fc r p Nothing argTy retTy) exp
= do n <- case p of
Explicit => genVarName "arg"
@ -153,11 +153,13 @@ checkTerm rig elabinfo nest env (ICaseLocal fc uname iname args scope) exp
checkTerm rig elabinfo nest env (IUpdate fc upds rec) exp
= checkUpdate rig elabinfo nest env fc upds rec exp
checkTerm rig elabinfo nest env (IApp fc fn arg) exp
= checkApp rig elabinfo nest env fc fn [arg] [] exp
= checkApp rig elabinfo nest env fc fn [arg] [] [] exp
checkTerm rig elabinfo nest env (IAutoApp fc fn arg) exp
= checkApp rig elabinfo nest env fc fn [] [arg] [] exp
checkTerm rig elabinfo nest env (IWithApp fc fn arg) exp
= throw (GenericMsg fc "with application not implemented yet")
checkTerm rig elabinfo nest env (IImplicitApp fc fn nm arg) exp
= checkApp rig elabinfo nest env fc fn [] [(nm, arg)] exp
checkTerm rig elabinfo nest env (INamedApp fc fn nm arg) exp
= checkApp rig elabinfo nest env fc fn [] [] [(nm, arg)] exp
checkTerm rig elabinfo nest env (ISearch fc depth) (Just gexpty)
= do est <- get EST
nm <- genName "search"

133
src/TTImp/Impossible.idr
View File

@ -7,8 +7,10 @@ import Core.TT
import Core.Value
import TTImp.TTImp
import TTImp.Elab.App
import Data.List
import Data.List1
%default covering
@ -57,73 +59,75 @@ nextVar fc
put QVar (i + 1)
pure (Ref fc Bound (MN "imp" i))
badClause : Term [] -> List RawImp -> List RawImp -> List (Name, RawImp) -> Core a
badClause fn exps autos named
= throw (GenericMsg (getLoc fn)
("Badly formed impossible clause "
++ show (fn, exps, autos, named)))
mutual
processArgs : {auto c : Ref Ctxt Defs} ->
{auto q : Ref QVar Int} ->
Term [] -> NF [] ->
(expargs : List RawImp) -> (impargs : List (Maybe Name, RawImp)) ->
(expargs : List RawImp) ->
(autoargs : List RawImp) ->
(namedargs : List (Name, RawImp)) ->
Core ClosedTerm
processArgs fn (NBind fc x (Pi _ _ Explicit ty) sc) (e :: exp) imp
= do e' <- mkTerm e (Just ty) [] []
-- unnamed takes priority
processArgs fn (NBind fc x (Pi _ _ Explicit ty) sc) (e :: exps) autos named
= do e' <- mkTerm e (Just ty) [] [] []
defs <- get Ctxt
processArgs (App fc fn e') !(sc defs (toClosure defaultOpts [] e'))
exp imp
processArgs fn (NBind fc x (Pi _ _ Implicit ty) sc) exp imp
exps autos named
processArgs fn (NBind fc x (Pi _ _ Explicit ty) sc) [] autos named
= do defs <- get Ctxt
case useImp [] imp of
case findNamed x named of
Just ((_, e) ::: named') =>
do e' <- mkTerm e (Just ty) [] [] []
processArgs (App fc fn e') !(sc defs (toClosure defaultOpts [] e'))
[] autos named'
Nothing => badClause fn [] autos named
processArgs fn (NBind fc x (Pi _ _ Implicit ty) sc) exps autos named
= do defs <- get Ctxt
case findNamed x named of
Nothing => do e' <- nextVar fc
processArgs (App fc fn e')
!(sc defs (toClosure defaultOpts [] e'))
exp imp
Just (e, impargs') =>
do e' <- mkTerm e (Just ty) [] []
exps autos named
Just ((_, e) ::: named') =>
do e' <- mkTerm e (Just ty) [] [] []
processArgs (App fc fn e') !(sc defs (toClosure defaultOpts [] e'))
exp impargs'
where
useImp : List (Maybe Name, RawImp) -> List (Maybe Name, RawImp) ->
Maybe (RawImp, List (Maybe Name, RawImp))
useImp acc [] = Nothing
useImp acc ((Just x', xtm) :: rest)
= if x == x'
then Just (xtm, reverse acc ++ rest)
else useImp ((Just x', xtm) :: acc) rest
useImp acc (ximp :: rest)
= useImp (ximp :: acc) rest
processArgs fn (NBind fc x (Pi _ _ AutoImplicit ty) sc) exp imp
exps autos named'
processArgs fn (NBind fc x (Pi _ _ AutoImplicit ty) sc) exps autos named
= do defs <- get Ctxt
case useAutoImp [] imp of
Nothing => do e' <- nextVar fc
processArgs (App fc fn e')
!(sc defs (toClosure defaultOpts [] e'))
exp imp
Just (e, impargs') =>
do e' <- mkTerm e (Just ty) [] []
processArgs (App fc fn e') !(sc defs (toClosure defaultOpts [] e'))
exp impargs'
where
useAutoImp : List (Maybe Name, RawImp) -> List (Maybe Name, RawImp) ->
Maybe (RawImp, List (Maybe Name, RawImp))
useAutoImp acc [] = Nothing
useAutoImp acc ((Nothing, xtm) :: rest)
= Just (xtm, reverse acc ++ rest)
useAutoImp acc ((Just x', xtm) :: rest)
= if x == x'
then Just (xtm, reverse acc ++ rest)
else useAutoImp ((Just x', xtm) :: acc) rest
useAutoImp acc (ximp :: rest)
= useAutoImp (ximp :: acc) rest
processArgs fn ty [] [] = pure fn
processArgs fn ty exp imp
= throw (GenericMsg (getLoc fn)
("Badly formed impossible clause "
++ show (fn, exp, imp)))
case autos of
(e :: autos') => -- unnamed takes priority
do e' <- mkTerm e (Just ty) [] [] []
processArgs (App fc fn e') !(sc defs (toClosure defaultOpts [] e'))
exps autos' named
[] =>
case findNamed x named of
Nothing =>
do e' <- nextVar fc
processArgs (App fc fn e')
!(sc defs (toClosure defaultOpts [] e'))
exps [] named
Just ((_, e) ::: named') =>
do e' <- mkTerm e (Just ty) [] [] []
processArgs (App fc fn e') !(sc defs (toClosure defaultOpts [] e'))
exps [] named'
processArgs fn ty [] [] [] = pure fn
processArgs fn ty exps autos named
= badClause fn exps autos named
buildApp : {auto c : Ref Ctxt Defs} ->
{auto q : Ref QVar Int} ->
FC -> Name -> Maybe (NF []) ->
(expargs : List RawImp) -> (impargs : List (Maybe Name, RawImp)) ->
(expargs : List RawImp) ->
(autoargs : List RawImp) ->
(namedargs : List (Name, RawImp)) ->
Core ClosedTerm
buildApp fc n mty exp imp
buildApp fc n mty exps autos named
= do defs <- get Ctxt
prims <- getPrimitiveNames
when (n `elem` prims) $
@ -134,21 +138,25 @@ mutual
| [] => throw (UndefinedName fc n)
| ts => throw (AmbiguousName fc (map fst ts))
tynf <- nf defs [] ty
processArgs (Ref fc Func n') tynf exp imp
processArgs (Ref fc Func n') tynf exps autos named
mkTerm : {auto c : Ref Ctxt Defs} ->
{auto q : Ref QVar Int} ->
RawImp -> Maybe (NF []) ->
(expargs : List RawImp) -> (impargs : List (Maybe Name, RawImp)) ->
(expargs : List RawImp) ->
(autoargs : List RawImp) ->
(namedargs : List (Name, RawImp)) ->
Core ClosedTerm
mkTerm (IVar fc n) mty exp imp
= buildApp fc n mty exp imp
mkTerm (IApp fc fn arg) mty exp imp
= mkTerm fn mty (arg :: exp) imp
mkTerm (IImplicitApp fc fn nm arg) mty exp imp
= mkTerm fn mty exp ((nm, arg) :: imp)
mkTerm (IPrimVal fc c) _ _ _ = pure (PrimVal fc c)
mkTerm tm _ _ _ = nextVar (getFC tm)
mkTerm (IVar fc n) mty exps autos named
= buildApp fc n mty exps autos named
mkTerm (IApp fc fn arg) mty exps autos named
= mkTerm fn mty (arg :: exps) autos named
mkTerm (IAutoApp fc fn arg) mty exps autos named
= mkTerm fn mty exps (arg :: autos) named
mkTerm (INamedApp fc fn nm arg) mty exps autos named
= mkTerm fn mty exps autos ((nm, arg) :: named)
mkTerm (IPrimVal fc c) _ _ _ _ = pure (PrimVal fc c)
mkTerm tm _ _ _ _ = nextVar (getFC tm)
-- Given an LHS that is declared 'impossible', build a term to match from,
-- so that when we build the case tree for checking coverage, we take into
@ -159,7 +167,7 @@ getImpossibleTerm : {vars : _} ->
Env Term vars -> NestedNames vars -> RawImp -> Core ClosedTerm
getImpossibleTerm env nest tm
= do q <- newRef QVar (the Int 0)
mkTerm (applyEnv tm) Nothing [] []
mkTerm (applyEnv tm) Nothing [] [] []
where
addEnv : {vars : _} ->
FC -> Env Term vars -> List RawImp
@ -180,6 +188,7 @@ getImpossibleTerm env nest tm
-- the name to the proper one from the nested names map
applyEnv : RawImp -> RawImp
applyEnv (IApp fc fn arg) = IApp fc (applyEnv fn) arg
applyEnv (IImplicitApp fc fn n arg)
= IImplicitApp fc (applyEnv fn) n arg
applyEnv (IAutoApp fc fn arg) = IAutoApp fc (applyEnv fn) arg
applyEnv (INamedApp fc fn n arg)
= INamedApp fc (applyEnv fn) n arg
applyEnv tm = apply (expandNest tm) (addEnv (getFC tm) env)

40
src/TTImp/Interactive/CaseSplit.idr
View File

@ -218,16 +218,20 @@ updateArg allvars var con (IVar fc n)
updateArg allvars var con (IApp fc f a)
= pure $ IApp fc !(updateArg allvars var con f)
!(updateArg allvars var con a)
updateArg allvars var con (IImplicitApp fc f n a)
= pure $ IImplicitApp fc !(updateArg allvars var con f) n
!(updateArg allvars var con a)
updateArg allvars var con (IAutoApp fc f a)
= pure $ IAutoApp fc !(updateArg allvars var con f)
!(updateArg allvars var con a)
updateArg allvars var con (INamedApp fc f n a)
= pure $ INamedApp fc !(updateArg allvars var con f) n
!(updateArg allvars var con a)
updateArg allvars var con (IAs fc s n p)
= updateArg allvars var con p
updateArg allvars var con tm = pure $ Implicit (getFC tm) True
data ArgType
= Explicit FC RawImp
| Implicit FC (Maybe Name) RawImp
| Auto FC RawImp
| Named FC Name RawImp
update : {auto c : Ref Ctxt Defs} ->
List Name -> -- all the variable names
@ -235,19 +239,24 @@ update : {auto c : Ref Ctxt Defs} ->
ArgType -> Core ArgType
update allvars var con (Explicit fc arg)
= pure $ Explicit fc !(updateArg allvars var con arg)
update allvars var con (Implicit fc n arg)
= pure $ Implicit fc n !(updateArg allvars var con arg)
update allvars var con (Auto fc arg)
= pure $ Auto fc !(updateArg allvars var con arg)
update allvars var con (Named fc n arg)
= pure $ Named fc n !(updateArg allvars var con arg)
getFnArgs : RawImp -> List ArgType -> (RawImp, List ArgType)
getFnArgs (IApp fc tm a) args
= getFnArgs tm (Explicit fc a :: args)
getFnArgs (IImplicitApp fc tm n a) args
= getFnArgs tm (Implicit fc n a :: args)
getFnArgs (IAutoApp fc tm a) args
= getFnArgs tm (Auto fc a :: args)
getFnArgs (INamedApp fc tm n a) args
= getFnArgs tm (Named fc n a :: args)
getFnArgs tm args = (tm, args)
apply : RawImp -> List ArgType -> RawImp
apply f (Explicit fc a :: args) = apply (IApp fc f a) args
apply f (Implicit fc n a :: args) = apply (IImplicitApp fc f n a) args
apply f (Auto fc a :: args) = apply (IAutoApp fc f a) args
apply f (Named fc n a :: args) = apply (INamedApp fc f n a) args
apply f [] = f
-- Return a new LHS to check, replacing 'var' with an application of 'con'
@ -295,11 +304,18 @@ findUpdates defs (IVar fc n) tm = recordUpdate fc n tm
findUpdates defs (IApp _ f a) (IApp _ f' a')
= do findUpdates defs f f'
findUpdates defs a a'
findUpdates defs (IImplicitApp _ f _ a) (IImplicitApp _ f' _ a')
findUpdates defs (IAutoApp _ f a) (IAutoApp _ f' a')
= do findUpdates defs f f'
findUpdates defs a a'
findUpdates defs (IImplicitApp _ f _ a) f' = findUpdates defs f f'
findUpdates defs f (IImplicitApp _ f' _ a) = findUpdates defs f f'
findUpdates defs (IAutoApp _ f a) f'
= findUpdates defs f f'
findUpdates defs f (IAutoApp _ f' a)
= findUpdates defs f f'
findUpdates defs (INamedApp _ f _ a) (INamedApp _ f' _ a')
= do findUpdates defs f f'
findUpdates defs a a'
findUpdates defs (INamedApp _ f _ a) f' = findUpdates defs f f'
findUpdates defs f (INamedApp _ f' _ a) = findUpdates defs f f'
findUpdates defs (IAs _ _ _ f) f' = findUpdates defs f f'
findUpdates defs f (IAs _ _ _ f') = findUpdates defs f f'
findUpdates _ _ _ = pure ()

12
src/TTImp/Interactive/GenerateDef.idr
View File

@ -91,7 +91,9 @@ splittableNames (IApp _ f (IBindVar _ n))
= splittableNames f ++ [UN n]
splittableNames (IApp _ f _)
= splittableNames f
splittableNames (IImplicitApp _ f _ _)
splittableNames (IAutoApp _ f _)
= splittableNames f
splittableNames (INamedApp _ f _ _)
= splittableNames f
splittableNames _ = []
@ -114,7 +116,8 @@ trySplit loc lhsraw lhs rhs n
fixNames (IVar loc' (UN n)) = IBindVar loc' n
fixNames (IVar loc' (MN _ _)) = Implicit loc' True
fixNames (IApp loc' f a) = IApp loc' (fixNames f) (fixNames a)
fixNames (IImplicitApp loc' f t a) = IImplicitApp loc' (fixNames f) t (fixNames a)
fixNames (IAutoApp loc' f a) = IAutoApp loc' (fixNames f) (fixNames a)
fixNames (INamedApp loc' f t a) = INamedApp loc' (fixNames f) t (fixNames a)
fixNames tm = tm
updateLHS : List (Name, RawImp) -> RawImp -> RawImp
@ -127,8 +130,9 @@ trySplit loc lhsraw lhs rhs n
Nothing => IBindVar loc' n
Just tm => fixNames tm
updateLHS ups (IApp loc' f a) = IApp loc' (updateLHS ups f) (updateLHS ups a)
updateLHS ups (IImplicitApp loc' f t a)
= IImplicitApp loc' (updateLHS ups f) t (updateLHS ups a)
updateLHS ups (IAutoApp loc' f a) = IAutoApp loc' (updateLHS ups f) (updateLHS ups a)
updateLHS ups (INamedApp loc' f t a)
= INamedApp loc' (updateLHS ups f) t (updateLHS ups a)
updateLHS ups tm = tm
generateSplits : {auto m : Ref MD Metadata} ->

21
src/TTImp/Parser.idr
View File

@ -155,8 +155,10 @@ mutual
applyExpImp start end f [] = f
applyExpImp start end f (Left exp :: args)
= applyExpImp start end (IApp (MkFC fname start end) f exp) args
applyExpImp start end f (Right (n, imp) :: args)
= applyExpImp start end (IImplicitApp (MkFC fname start end) f n imp) args
applyExpImp start end f (Right (Just n, imp) :: args)
= applyExpImp start end (INamedApp (MkFC fname start end) f n imp) args
applyExpImp start end f (Right (Nothing, imp) :: args)
= applyExpImp start end (IAutoApp (MkFC fname start end) f imp) args
argExpr : FileName -> IndentInfo ->
Rule (Either RawImp (Maybe Name, RawImp))
@ -515,7 +517,8 @@ mutual
getFn : RawImp -> SourceEmptyRule Name
getFn (IVar _ n) = pure n
getFn (IApp _ f a) = getFn f
getFn (IImplicitApp _ f _ a) = getFn f
getFn (IAutoApp _ f a) = getFn f
getFn (INamedApp _ f _ a) = getFn f
getFn _ = fail "Not a function application"
clause : Nat -> FileName -> IndentInfo -> Rule (Name, ImpClause)
@ -644,14 +647,20 @@ namespaceDecl
commit
namespaceId
logLevel : Rule (Maybe (List String, Nat))
logLevel
= (Nothing <$ exactIdent "off")
<|> do topic <- option [] ((::) <$> unqualifiedName <*> many aDotIdent)
lvl <- intLit
pure (Just (topic, fromInteger lvl))
directive : FileName -> IndentInfo -> Rule ImpDecl
directive fname indents
= do pragma "logging"
commit
topic <- ((::) <$> unqualifiedName <*> many aDotIdent)
lvl <- intLit
lvl <- logLevel
atEnd indents
pure (ILog (topic, integerToNat lvl))
pure (ILog lvl)
{- Can't do IPragma due to lack of Ref Ctxt. Should we worry about this?
<|> do pragma "pair"
commit

11
src/TTImp/PartialEval.idr
View File

@ -149,7 +149,7 @@ getSpecPats fc pename fn stk fnty args sargs pats
mkRHSargs (NBind _ x (Pi _ _ _ _) sc) app (a :: as) ((_, Dynamic) :: ds)
= do defs <- get Ctxt
sc' <- sc defs (toClosure defaultOpts [] (Erased fc False))
mkRHSargs sc' (IImplicitApp fc app (Just x) (IVar fc (UN a))) as ds
mkRHSargs sc' (INamedApp fc app x (IVar fc (UN a))) as ds
mkRHSargs (NBind _ x (Pi _ _ Explicit _) sc) app as ((_, Static tm) :: ds)
= do defs <- get Ctxt
sc' <- sc defs (toClosure defaultOpts [] (Erased fc False))
@ -159,7 +159,7 @@ getSpecPats fc pename fn stk fnty args sargs pats
= do defs <- get Ctxt
sc' <- sc defs (toClosure defaultOpts [] (Erased fc False))
tm' <- unelabNoSugar [] tm
mkRHSargs sc' (IImplicitApp fc app (Just x) tm') as ds
mkRHSargs sc' (INamedApp fc app x tm') as ds
-- Type will depend on the value here (we assume a variadic function) but
-- the argument names are still needed
mkRHSargs ty app (a :: as) ((_, Dynamic) :: ds)
@ -169,7 +169,7 @@ getSpecPats fc pename fn stk fnty args sargs pats
getRawArgs : List (Maybe Name, RawImp) -> RawImp -> List (Maybe Name, RawImp)
getRawArgs args (IApp _ f arg) = getRawArgs ((Nothing, arg) :: args) f
getRawArgs args (IImplicitApp _ f (Just n) arg)
getRawArgs args (INamedApp _ f n arg)
= getRawArgs ((Just n, arg) :: args) f
getRawArgs args tm = args
@ -177,7 +177,7 @@ getSpecPats fc pename fn stk fnty args sargs pats
reapply f [] = f
reapply f ((Nothing, arg) :: args) = reapply (IApp fc f arg) args
reapply f ((Just t, arg) :: args)
= reapply (IImplicitApp fc f (Just t) arg) args
= reapply (INamedApp fc f t arg) args
dropArgs : Name -> RawImp -> RawImp
dropArgs pename tm = reapply (IVar fc pename) (dropSpec 0 sargs (getRawArgs [] tm))
@ -301,7 +301,8 @@ mkSpecDef {vars} fc gdef pename sargs fn stk
updateApp : Name -> RawImp -> RawImp
updateApp n (IApp fc f a) = IApp fc (updateApp n f) a
updateApp n (IImplicitApp fc f m a) = IImplicitApp fc (updateApp n f) m a
updateApp n (IAutoApp fc f a) = IAutoApp fc (updateApp n f) a
updateApp n (INamedApp fc f m a) = INamedApp fc (updateApp n f) m a
updateApp n f = IVar fc n
unelabDef : (vs ** (Env Term vs, Term vs, Term vs)) ->

3
src/TTImp/ProcessData.idr
View File

@ -74,7 +74,8 @@ updateNS orig ns tm = updateNSApp tm
then IVar fc ns
else IVar fc n
updateNSApp (IApp fc f arg) = IApp fc (updateNSApp f) arg
updateNSApp (IImplicitApp fc f n arg) = IImplicitApp fc (updateNSApp f) n arg
updateNSApp (IAutoApp fc f arg) = IAutoApp fc (updateNSApp f) arg
updateNSApp (INamedApp fc f n arg) = INamedApp fc (updateNSApp f) n arg
updateNSApp t = t
checkCon : {vars : _} ->

2
src/TTImp/ProcessDecls.idr
View File

@ -59,7 +59,7 @@ process eopts nest env (IRunElabDecl fc tm)
process eopts nest env (IPragma act)
= act nest env
process eopts nest env (ILog lvl)
= addLogLevel (uncurry unsafeMkLogLevel lvl)
= addLogLevel (uncurry unsafeMkLogLevel <$> lvl)
TTImp.Elab.Check.processDecl = process

4
src/TTImp/ProcessRecord.idr
View File

@ -97,7 +97,7 @@ elabRecord {vars} eopts fc env nest newns vis tn params conName_in fields
apply : RawImp -> List (Name, RawImp, PiInfo RawImp) -> RawImp
apply f [] = f
apply f ((n, arg, Explicit) :: xs) = apply (IApp (getFC f) f arg) xs
apply f ((n, arg, _ ) :: xs) = apply (IImplicitApp (getFC f) f (Just n) arg) xs
apply f ((n, arg, _ ) :: xs) = apply (INamedApp (getFC f) f n arg) xs
elabAsData : Name -> Core ()
elabAsData cname
@ -167,7 +167,7 @@ elabRecord {vars} eopts fc env nest newns vis tn params conName_in fields
let lhs = IApp fc (IVar fc projNameNS)
(if imp == Explicit
then lhs_exp
else IImplicitApp fc lhs_exp (Just (UN fldNameStr))
else INamedApp fc lhs_exp (UN fldNameStr)
(IBindVar fc fldNameStr))
let rhs = IVar fc (UN fldNameStr)
log "declare.record.projection" 5 $ "Projection " ++ show lhs ++ " = " ++ show rhs

18
src/TTImp/Reflect.idr
View File

@ -131,12 +131,17 @@ mutual
f' <- reify defs !(evalClosure defs f)
a' <- reify defs !(evalClosure defs a)
pure (IApp fc' f' a')
(NS _ (UN "IImplicitApp"), [fc, f, m, a])
(NS _ (UN "INamedApp"), [fc, f, m, a])
=> do fc' <- reify defs !(evalClosure defs fc)
f' <- reify defs !(evalClosure defs f)
m' <- reify defs !(evalClosure defs m)
a' <- reify defs !(evalClosure defs a)
pure (IImplicitApp fc' f' m' a')
pure (INamedApp fc' f' m' a')
(NS _ (UN "IAutoApp"), [fc, f, a])
=> do fc' <- reify defs !(evalClosure defs fc)
f' <- reify defs !(evalClosure defs f)
a' <- reify defs !(evalClosure defs a)
pure (IAutoApp fc' f' a')
(NS _ (UN "IWithApp"), [fc, f, a])
=> do fc' <- reify defs !(evalClosure defs fc)
f' <- reify defs !(evalClosure defs f)
@ -481,12 +486,17 @@ mutual
f' <- reflect fc defs lhs env f
a' <- reflect fc defs lhs env a
appCon fc defs (reflectionttimp "IApp") [fc', f', a']
reflect fc defs lhs env (IImplicitApp tfc f m a)
reflect fc defs lhs env (IAutoApp tfc f a)
= do fc' <- reflect fc defs lhs env tfc
f' <- reflect fc defs lhs env f
a' <- reflect fc defs lhs env a
appCon fc defs (reflectionttimp "IAutoApp") [fc', f', a']
reflect fc defs lhs env (INamedApp tfc f m a)
= do fc' <- reflect fc defs lhs env tfc
f' <- reflect fc defs lhs env f
m' <- reflect fc defs lhs env m
a' <- reflect fc defs lhs env a
appCon fc defs (reflectionttimp "IImplicitApp") [fc', f', m', a']
appCon fc defs (reflectionttimp "INamedApp") [fc', f', m', a']
reflect fc defs lhs env (IWithApp tfc f a)
= do fc' <- reflect fc defs lhs env tfc
f' <- reflect fc defs lhs env f

59
src/TTImp/TTImp.idr
View File

@ -11,6 +11,7 @@ import Core.TTC
import Core.Value
import Data.List
import Data.Maybe
%default covering
@ -68,7 +69,8 @@ mutual
IUpdate : FC -> List IFieldUpdate -> RawImp -> RawImp
IApp : FC -> RawImp -> RawImp -> RawImp
IImplicitApp : FC -> RawImp -> Maybe Name -> RawImp -> RawImp
IAutoApp : FC -> RawImp -> RawImp -> RawImp
INamedApp : FC -> RawImp -> Name -> RawImp -> RawImp
IWithApp : FC -> RawImp -> RawImp -> RawImp
ISearch : FC -> (depth : Nat) -> RawImp
@ -144,11 +146,12 @@ mutual
++ " " ++ show args ++ ") " ++ show sc ++ ")"
show (IUpdate _ flds rec)
= "(%record " ++ showSep ", " (map show flds) ++ " " ++ show rec ++ ")"
show (IApp fc f a)
= "(" ++ show f ++ " " ++ show a ++ ")"
show (IImplicitApp fc f n a)
show (INamedApp fc f n a)
= "(" ++ show f ++ " [" ++ show n ++ " = " ++ show a ++ "])"
show (IAutoApp fc f a)
= "(" ++ show f ++ " [" ++ show a ++ "])"
show (IWithApp fc f a)
= "(" ++ show f ++ " | " ++ show a ++ ")"
show (ISearch fc d)
@ -344,7 +347,7 @@ mutual
IPragma : ({vars : _} ->
NestedNames vars -> Env Term vars -> Core ()) ->
ImpDecl
ILog : (List String, Nat) -> ImpDecl
ILog : Maybe (List String, Nat) -> ImpDecl
export
Show ImpDecl where
@ -363,7 +366,8 @@ mutual
show (IRunElabDecl _ tm)
= "%runElab " ++ show tm
show (IPragma _) = "[externally defined pragma]"
show (ILog (topic, lvl)) = "%logging " ++ case topic of
show (ILog Nothing) = "%logging off"
show (ILog (Just (topic, lvl))) = "%logging " ++ case topic of
[] => show lvl
_ => concat (intersperse "." topic) ++ " " ++ show lvl
@ -396,9 +400,12 @@ lhsInCurrentNS : {auto c : Ref Ctxt Defs} ->
lhsInCurrentNS nest (IApp loc f a)
= do f' <- lhsInCurrentNS nest f
pure (IApp loc f' a)
lhsInCurrentNS nest (IImplicitApp loc f n a)
lhsInCurrentNS nest (IAutoApp loc f a)
= do f' <- lhsInCurrentNS nest f
pure (IImplicitApp loc f' n a)
pure (IAutoApp loc f' a)
lhsInCurrentNS nest (INamedApp loc f n a)
= do f' <- lhsInCurrentNS nest f
pure (INamedApp loc f' n a)
lhsInCurrentNS nest (IWithApp loc f a)
= do f' <- lhsInCurrentNS nest f
pure (IWithApp loc f' a)
@ -422,7 +429,9 @@ findIBinds (ILam fc rig p n aty sc)
= findIBinds aty ++ findIBinds sc
findIBinds (IApp fc fn av)
= findIBinds fn ++ findIBinds av
findIBinds (IImplicitApp fc fn n av)
findIBinds (IAutoApp fc fn av)
= findIBinds fn ++ findIBinds av
findIBinds (INamedApp _ fn _ av)
= findIBinds fn ++ findIBinds av
findIBinds (IWithApp fc fn av)
= findIBinds fn ++ findIBinds av
@ -456,7 +465,9 @@ findImplicits (ILam fc rig p n aty sc)
= findImplicits aty ++ findImplicits sc
findImplicits (IApp fc fn av)
= findImplicits fn ++ findImplicits av
findImplicits (IImplicitApp fc fn n av)
findImplicits (IAutoApp _ fn av)
= findImplicits fn ++ findImplicits av
findImplicits (INamedApp _ fn _ av)
= findImplicits fn ++ findImplicits av
findImplicits (IWithApp fc fn av)
= findImplicits fn ++ findImplicits av
@ -488,9 +499,12 @@ implicitsAs defs ns tm = setAs (map Just (ns ++ map UN (findIBinds tm))) tm
setAs is (IApp loc f a)
= do f' <- setAs is f
pure $ IApp loc f' a
setAs is (IImplicitApp loc f n a)
= do f' <- setAs (n :: is) f
pure $ IImplicitApp loc f' n a
setAs is (IAutoApp loc f a)
= do f' <- setAs (Nothing :: is) f
pure $ IAutoApp loc f' a
setAs is (INamedApp loc f n a)
= do f' <- setAs (Just n :: is) f
pure $ INamedApp loc f' n a
setAs is (IWithApp loc f a)
= do f' <- setAs is f
pure $ IWithApp loc f' a
@ -531,14 +545,14 @@ implicitsAs defs ns tm = setAs (map Just (ns ++ map UN (findIBinds tm))) tm
impAs loc' [] tm = tm
impAs loc' ((UN n, AutoImplicit) :: ns) tm
= impAs loc' ns $
IImplicitApp loc' tm (Just (UN n)) (IBindVar loc' n)
INamedApp loc' tm (UN n) (IBindVar loc' n)
impAs loc' ((n, Implicit) :: ns) tm
= impAs loc' ns $
IImplicitApp loc' tm (Just n)
INamedApp loc' tm n
(IAs loc' UseLeft n (Implicit loc' True))
impAs loc' ((n, DefImplicit t) :: ns) tm
= impAs loc' ns $
IImplicitApp loc' tm (Just n)
INamedApp loc' tm n
(IAs loc' UseLeft n (Implicit loc' True))
impAs loc' (_ :: ns) tm = impAs loc' ns tm
setAs is tm = pure tm
@ -610,7 +624,8 @@ getFC (ILocal x _ _) = x
getFC (ICaseLocal x _ _ _ _) = x
getFC (IUpdate x _ _) = x
getFC (IApp x _ _) = x
getFC (IImplicitApp x _ _ _) = x
getFC (INamedApp x _ _ _) = x
getFC (IAutoApp x _ _) = x
getFC (IWithApp x _ _) = x
getFC (ISearch x _) = x
getFC (IAlternative x _ _) = x
@ -644,7 +659,8 @@ export
getFn : RawImp -> RawImp
getFn (IApp _ f arg) = getFn f
getFn (IWithApp _ f arg) = getFn f
getFn (IImplicitApp _ f _ _) = getFn f
getFn (INamedApp _ f _ _) = getFn f
getFn (IAutoApp _ f _) = getFn f
getFn (IAs _ _ _ f) = getFn f
getFn (IMustUnify _ _ f) = getFn f
getFn f = f
@ -674,7 +690,7 @@ mutual
= do tag 6; toBuf b fc; toBuf b fs; toBuf b rec
toBuf b (IApp fc fn arg)
= do tag 7; toBuf b fc; toBuf b fn; toBuf b arg
toBuf b (IImplicitApp fc fn y arg)
toBuf b (INamedApp fc fn y arg)
= do tag 8; toBuf b fc; toBuf b fn; toBuf b y; toBuf b arg
toBuf b (IWithApp fc fn arg)
= do tag 9; toBuf b fc; toBuf b fn; toBuf b arg
@ -727,6 +743,8 @@ mutual
= do tag 29; toBuf b fc; toBuf b i
toBuf b (IWithUnambigNames fc ns rhs)
= do tag 30; toBuf b ns; toBuf b rhs
toBuf b (IAutoApp fc fn arg)
= do tag 31; toBuf b fc; toBuf b fn; toBuf b arg
fromBuf b
= case !getTag of
@ -760,7 +778,7 @@ mutual
pure (IApp fc fn arg)
8 => do fc <- fromBuf b; fn <- fromBuf b
y <- fromBuf b; arg <- fromBuf b
pure (IImplicitApp fc fn y arg)
pure (INamedApp fc fn y arg)
9 => do fc <- fromBuf b; fn <- fromBuf b
arg <- fromBuf b
pure (IWithApp fc fn arg)
@ -817,6 +835,9 @@ mutual
ns <- fromBuf b
rhs <- fromBuf b
pure (IWithUnambigNames fc ns rhs)
31 => do fc <- fromBuf b; fn <- fromBuf b
arg <- fromBuf b
pure (IAutoApp fc fn arg)
_ => corrupt "RawImp"
export

7
src/TTImp/Unelab.idr
View File

@ -32,7 +32,8 @@ used idx _ = False
data IArg
= Exp FC RawImp
| Imp FC (Maybe Name) RawImp
| Auto FC RawImp
| Named FC Name RawImp
data UnelabMode
= Full
@ -113,7 +114,7 @@ mutual
where
getFnArgs : RawImp -> List IArg -> (RawImp, List IArg)
getFnArgs (IApp fc f arg) args = getFnArgs f (Exp fc arg :: args)
getFnArgs (IImplicitApp fc f n arg) args = getFnArgs f (Imp fc n arg :: args)
getFnArgs (INamedApp fc f n arg) args = getFnArgs f (Named fc n arg :: args)
getFnArgs tm args = (tm, args)
-- Turn a term back into an unannotated TTImp. Returns the type of the
@ -187,7 +188,7 @@ mutual
glueBack defs env sc')
NBind _ x (Pi _ rig p ty) sc
=> do sc' <- sc defs (toClosure defaultOpts env arg)
pure (IImplicitApp fc fn' (Just x) arg',
pure (INamedApp fc fn' x arg',
glueBack defs env sc')
_ => pure (IApp fc fn' arg', gErased fc)
unelabTy' umode env (As fc s p tm)

30
src/TTImp/Utils.idr
View File

@ -38,7 +38,9 @@ findBindableNames arg env used (ILam fc rig p mn aty sc)
findBindableNames True env' used sc
findBindableNames arg env used (IApp fc fn av)
= findBindableNames False env used fn ++ findBindableNames True env used av
findBindableNames arg env used (IImplicitApp fc fn n av)
findBindableNames arg env used (INamedApp fc fn n av)
= findBindableNames False env used fn ++ findBindableNames True env used av
findBindableNames arg env used (IAutoApp fc fn av)
= findBindableNames False env used fn ++ findBindableNames True env used av
findBindableNames arg env used (IWithApp fc fn av)
= findBindableNames False env used fn ++ findBindableNames True env used av
@ -80,7 +82,9 @@ findAllNames env (ILam fc rig p mn aty sc)
findAllNames env' aty ++ findAllNames env' sc
findAllNames env (IApp fc fn av)
= findAllNames env fn ++ findAllNames env av
findAllNames env (IImplicitApp fc fn n av)
findAllNames env (INamedApp fc fn n av)
= findAllNames env fn ++ findAllNames env av
findAllNames env (IAutoApp fc fn av)
= findAllNames env fn ++ findAllNames env av
findAllNames env (IWithApp fc fn av)
= findAllNames env fn ++ findAllNames env av
@ -114,7 +118,9 @@ findIBindVars (ILam fc rig p mn aty sc)
= findIBindVars aty ++ findIBindVars sc
findIBindVars (IApp fc fn av)
= findIBindVars fn ++ findIBindVars av
findIBindVars (IImplicitApp fc fn n av)
findIBindVars (INamedApp fc fn n av)
= findIBindVars fn ++ findIBindVars av
findIBindVars (IAutoApp fc fn av)
= findIBindVars fn ++ findIBindVars av
findIBindVars (IWithApp fc fn av)
= findIBindVars fn ++ findIBindVars av
@ -170,8 +176,10 @@ mutual
(substNames' bvar bound' ps y)
substNames' bvar bound ps (IApp fc fn arg)
= IApp fc (substNames' bvar bound ps fn) (substNames' bvar bound ps arg)
substNames' bvar bound ps (IImplicitApp fc fn y arg)
= IImplicitApp fc (substNames' bvar bound ps fn) y (substNames' bvar bound ps arg)
substNames' bvar bound ps (INamedApp fc fn y arg)
= INamedApp fc (substNames' bvar bound ps fn) y (substNames' bvar bound ps arg)
substNames' bvar bound ps (IAutoApp fc fn arg)
= IAutoApp fc (substNames' bvar bound ps fn) (substNames' bvar bound ps arg)
substNames' bvar bound ps (IWithApp fc fn arg)
= IWithApp fc (substNames' bvar bound ps fn) (substNames' bvar bound ps arg)
substNames' bvar bound ps (IAlternative fc y xs)
@ -194,12 +202,14 @@ mutual
ImpClause -> ImpClause
substNamesClause' bvar bound ps (PatClause fc lhs rhs)
= let bound' = map UN (map snd (findBindableNames True bound [] lhs))
++ bound in
++ findIBindVars lhs
++ bound in
PatClause fc (substNames' bvar [] [] lhs)
(substNames' bvar bound' ps rhs)
substNamesClause' bvar bound ps (WithClause fc lhs wval flags cs)
= let bound' = map UN (map snd (findBindableNames True bound [] lhs))
++ bound in
++ findIBindVars lhs
++ bound in
WithClause fc (substNames' bvar [] [] lhs)
(substNames' bvar bound' ps wval) flags cs
substNamesClause' bvar bound ps (ImpossibleClause fc lhs)
@ -267,8 +277,10 @@ mutual
(substLoc fc' y)
substLoc fc' (IApp fc fn arg)
= IApp fc' (substLoc fc' fn) (substLoc fc' arg)
substLoc fc' (IImplicitApp fc fn y arg)
= IImplicitApp fc' (substLoc fc' fn) y (substLoc fc' arg)
substLoc fc' (INamedApp fc fn y arg)
= INamedApp fc' (substLoc fc' fn) y (substLoc fc' arg)
substLoc fc' (IAutoApp fc fn arg)
= IAutoApp fc' (substLoc fc' fn) (substLoc fc' arg)
substLoc fc' (IWithApp fc fn arg)
= IWithApp fc' (substLoc fc' fn) (substLoc fc' arg)
substLoc fc' (IAlternative fc y xs)

22
src/TTImp/WithClause.idr
View File

@ -40,7 +40,9 @@ mutual
-- TODO: Lam, Let, Case, Local, Update
getMatch lhs (IApp _ f a) (IApp loc f' a')
= matchAll lhs [(f, f'), (a, a')]
getMatch lhs (IImplicitApp _ f n a) (IImplicitApp loc f' n' a')
getMatch lhs (IAutoApp _ f a) (IAutoApp loc f' a')
= matchAll lhs [(f, f'), (a, a')]
getMatch lhs (INamedApp _ f n a) (INamedApp loc f' n' a')
= if n == n'
then matchAll lhs [(f, f'), (a, a')]
else matchFail loc
@ -49,14 +51,20 @@ mutual
-- On LHS: If there's an implicit in the parent, but not the clause, add the
-- implicit to the clause. This will propagate the implicit through to the
-- body
getMatch True (IImplicitApp fc f n a) f'
getMatch True (INamedApp fc f n a) f'
= matchAll True [(f, f'), (a, a)]
getMatch True (IAutoApp fc f a) f'
= matchAll True [(f, f'), (a, a)]
-- On RHS: Rely on unification to fill in the implicit
getMatch False (IImplicitApp fc f n a) f'
getMatch False (INamedApp fc f n a) f'
= getMatch False f f
getMatch False (IAutoApp fc f a) f'
= getMatch False f f
-- Can't have an implicit in the clause if there wasn't a matching
-- implicit in the parent
getMatch lhs f (IImplicitApp fc f' n a)
getMatch lhs f (INamedApp fc f' n a)
= matchFail fc
getMatch lhs f (IAutoApp fc f' a)
= matchFail fc
-- Alternatives are okay as long as the alternatives correspond, and
-- one of them is okay
@ -197,8 +205,10 @@ withRHS fc drop wname wargnames tm toplhs
= pure $ IUpdate fc upds !(wrhs tm) -- TODO!
wrhs (IApp fc f a)
= pure $ IApp fc !(wrhs f) !(wrhs a)
wrhs (IImplicitApp fc f n a)
= pure $ IImplicitApp fc !(wrhs f) n !(wrhs a)
wrhs (IAutoApp fc f a)
= pure $ IAutoApp fc !(wrhs f) !(wrhs a)
wrhs (INamedApp fc f n a)
= pure $ INamedApp fc !(wrhs f) n !(wrhs a)
wrhs (IWithApp fc f a) = updateWith fc f [a]
wrhs (IRewrite fc rule tm) = pure $ IRewrite fc !(wrhs rule) !(wrhs tm)
wrhs (IDelayed fc r tm) = pure $ IDelayed fc r !(wrhs tm)

2
src/Text/Token.idr
View File

@ -18,7 +18,7 @@ module Text.Token
||| tokValue SKComma x = ()
||| ```
public export
interface TokenKind (k : Type) where
interface TokenKind k where
||| The type that a token of this kind converts to.
TokType : k -> Type

17
support/chez/support.ss
View File

@ -217,6 +217,23 @@
(define (blodwen-condition-signal c) (condition-signal c))
(define (blodwen-condition-broadcast c) (condition-broadcast c))
(define-record future-internal (result ready mutex signal))
(define (blodwen-make-future work)
(let ([future (make-future-internal #f #f (make-mutex) (make-condition))])
(fork-thread (lambda ()
(let ([result (work)])
(with-mutex (future-internal-mutex future)
(set-future-internal-result! future result)
(set-future-internal-ready! future #t)
(condition-broadcast (future-internal-signal future))))))
future))
(define (blodwen-await-future ty future)
(let ([mutex (future-internal-mutex future)])
(with-mutex mutex
(if (not (future-internal-ready future))
(condition-wait (future-internal-signal future) mutex))
(future-internal-result future))))
(define (blodwen-sleep s) (sleep (make-time 'time-duration 0 s)))
(define (blodwen-usleep s)
(let ((sec (div s 1000000))

1
support/racket/support.rkt
View File

@ -212,6 +212,7 @@
(channel-put c 'ready))
(define (blodwen-sleep s) (sleep s))
(define (blodwen-usleep us) (sleep (* 0.000001 us)))
(define (blodwen-time) (current-seconds))

10
tests/Main.idr
View File

@ -44,7 +44,8 @@ idrisTests = MkTestPool []
"basic031", "basic032", "basic033", "basic034", "basic035",
"basic036", "basic037", "basic038", "basic039", "basic040",
"basic041", "basic042", "basic043", "basic044", "basic045",
"basic046", "basic047", "basic048",
"basic046", "basic047", "basic048", "basic049", "basic050",
"basic051",
-- Coverage checking
"coverage001", "coverage002", "coverage003", "coverage004",
"coverage005", "coverage006", "coverage007", "coverage008",
@ -70,7 +71,7 @@ idrisTests = MkTestPool []
"interface005", "interface006", "interface007", "interface008",
"interface009", "interface010", "interface011", "interface012",
"interface013", "interface014", "interface015", "interface016",
"interface017",
"interface017", "interface018",
-- Miscellaneous REPL
"interpreter001", "interpreter002", "interpreter003", "interpreter004",
"interpreter005",
@ -104,7 +105,7 @@ idrisTests = MkTestPool []
"real001", "real002",
-- Records, access and dependent update
"record001", "record002", "record003", "record004", "record005",
"record007",
"record006",
-- Quotation and reflection
"reflection001", "reflection002", "reflection003", "reflection004",
"reflection005", "reflection006", "reflection007", "reflection008",
@ -114,7 +115,7 @@ idrisTests = MkTestPool []
"reg008", "reg009", "reg010", "reg011", "reg012", "reg013", "reg014",
"reg015", "reg016", "reg017", "reg018", "reg019", "reg020", "reg021",
"reg022", "reg023", "reg024", "reg025", "reg026", "reg027", "reg028",
"reg029", "reg030", "reg031", "reg032", "reg033", "reg034",
"reg029", "reg030", "reg031", "reg032", "reg033", "reg034", "reg035",
-- Totality checking
"total001", "total002", "total003", "total004", "total005",
"total006", "total007", "total008", "total009", "total010",
@ -137,6 +138,7 @@ chezTests = MkTestPool [Chez]
"chez019", "chez020", "chez021", "chez022", "chez023", "chez024",
"chez025", "chez026", "chez027", "chez028", "chez029", "chez030",
"chez031",
"concurrency001",
"perf001",
"reg001"]

58
tests/chez/concurrency001/Futures.idr Normal file
View File

@ -0,0 +1,58 @@
module Futures
import Data.List
import Data.So
import System
import System.Future
import System.Info
constant : IO ()
constant = do
let a = await $ fork "String"
putStrLn a
-- Issue related to usleep in MacOS brew chez
macsleep : (us : Int) -> So (us >= 0) => IO ()
macsleep us =
if (os == "darwin")
then sleep (us `div` 10000)
else usleep us
partial
futureHelloWorld : (Int, String) -> IO (Future Unit)
futureHelloWorld (us, n) with (choose (us >= 0))
futureHelloWorld (us, n) | Left p = forkIO $ do
macsleep us
putStrLn $ "Hello " ++ n ++ "!"
partial
simpleIO : IO (List Unit)
simpleIO = do
futures <- sequence $ futureHelloWorld <$> [(30000, "World"), (10000, "Bar"), (0, "Foo"), (20000, "Idris")]
let awaited = await <$> futures
pure awaited
nonbind : IO (Future ())
nonbind = forkIO $ putStrLn "This shouldn't print"
erasureAndNonbindTest : IO ()
erasureAndNonbindTest = do
_ <- forkIO $ do
putStrLn "This line is printed"
notUsed <- forkIO $ do
macsleep 10000
putStrLn "This line is also printed"
let _ = nonbind
let n = nonbind
macsleep 20000 -- Even if not explicitly awaited, we should let threads finish before exiting
map : IO ()
map = do
future1 <- forkIO $ do
macsleep 10000
putStrLn "#2"
let future3 = map (const "#3") future1
future2 <- forkIO $ do
putStrLn "#1"
pure $ await future2
putStrLn (await future3)

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

@ -0,0 +1,10 @@
String
Hello Foo!
Hello Bar!
Hello Idris!
Hello World!
This line is printed
This line is also printed
#1
#2
#3

6
tests/chez/concurrency001/run Normal file
View File

@ -0,0 +1,6 @@
$1 --no-banner --no-color --console-width 0 --cg chez Futures.idr -p contrib --exec constant
$1 --no-banner --no-color --console-width 0 --cg chez Futures.idr -p contrib --exec simpleIO
$1 --no-banner --no-color --console-width 0 --cg chez Futures.idr -p contrib --exec erasureAndNonbindTest
$1 --no-banner --no-color --console-width 0 --cg chez Futures.idr -p contrib --exec map
rm -r build

12
tests/ideMode/ideMode001/expected
View File

@ -2,13 +2,13 @@
000038(:write-string "1/1: Building LocType (LocType.idr)" 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:372} 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 "?{_:373}_[]")))))) 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:372}_[] ?{_:373}_[])")))))) 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 ?{_:374}_[] ?{_:373}_[])")))))) 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:384} 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 "?{_:385}_[]")))))) 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:384}_[] ?{_:385}_[])")))))) 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 ?{_:386}_[] ?{_:385}_[])")))))) 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 ?{_:363}_[] ?{_:362}_[])")))))) 1)
0001ed(: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.Types.Nat} -> {0 a : Type} -> {0 n : Prelude.Types.Nat} -> ({arg:353} : (Main.Vect n[0] a[1])) -> ({arg:354} : (Main.Vect m[3] a[2])) -> (Main.Vect (Prelude.Num.+ Prelude.Types.Nat Prelude.Types.Num implementation at Prelude/Types.idr:64:1--69:33 n[2] m[4]) a[3]))))))")))))) 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 ?{_:375}_[] ?{_:374}_[])")))))) 1)
0001ed(: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.Types.Nat} -> {0 a : Type} -> {0 n : Prelude.Types.Nat} -> ({arg:365} : (Main.Vect n[0] a[1])) -> ({arg:366} : (Main.Vect m[3] a[2])) -> (Main.Vect (Prelude.Num.+ Prelude.Types.Nat Prelude.Types.Num implementation at Prelude/Types.idr:64:1--69:33 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)
0000d9(: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.Types.Nat")))))) 1)
0000d9(: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.Types.Nat")))))) 1)

12
tests/ideMode/ideMode003/expected
View File

@ -2,13 +2,13 @@
000038(:write-string "1/1: Building LocType (LocType.idr)" 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:372} 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 "?{_:373}_[]")))))) 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:372}_[] ?{_:373}_[])")))))) 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 ?{_:374}_[] ?{_:373}_[])")))))) 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:384} 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 "?{_:385}_[]")))))) 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:384}_[] ?{_:385}_[])")))))) 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 ?{_:386}_[] ?{_:385}_[])")))))) 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 ?{_:363}_[] ?{_:362}_[])")))))) 1)
0001ed(: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.Types.Nat} -> {0 a : Type} -> {0 n : Prelude.Types.Nat} -> ({arg:353} : (Main.Vect n[0] a[1])) -> ({arg:354} : (Main.Vect m[3] a[2])) -> (Main.Vect (Prelude.Num.+ Prelude.Types.Nat Prelude.Types.Num implementation at Prelude/Types.idr:64:1--69:33 n[2] m[4]) a[3]))))))")))))) 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 ?{_:375}_[] ?{_:374}_[])")))))) 1)
0001ed(: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.Types.Nat} -> {0 a : Type} -> {0 n : Prelude.Types.Nat} -> ({arg:365} : (Main.Vect n[0] a[1])) -> ({arg:366} : (Main.Vect m[3] a[2])) -> (Main.Vect (Prelude.Num.+ Prelude.Types.Nat Prelude.Types.Num implementation at Prelude/Types.idr:64:1--69:33 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)
0000d9(: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.Types.Nat")))))) 1)
0000d9(: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.Types.Nat")))))) 1)

2
tests/idris2/basic013/Implicits.idr
View File

@ -1,5 +1,5 @@
public export
interface Do (m : Type) where
interface Do (0 m : Type) where
Next : m -> Type
bind : (x : m) -> Next x

229
tests/idris2/basic049/Fld.idr Normal file
View File

@ -0,0 +1,229 @@
import Data.Maybe
import Data.Nat
namespace SuperDog
public export
record SuperDog where
constructor MkDog
supername : String
age : Int
weight : Int
namespace OrdinaryDog
public export
record OrdinaryDog where
constructor MkDog
name : String
age : Int
weight : Int
record Other a where
constructor MkOther
{imp : String}
fieldA : a
fieldB : b
------ Using new application syntax as sugar for data instantiation (be it data/record/interface) -------
myDog : OrdinaryDog
myDog = MkDog { age = 4
, weight = 12
, name = "Sam" }
mySuperDog : SuperDog
mySuperDog = MkDog { age = 3
, weight = 10
, supername = "Super-Sam" }
other : ?
other = MkOther {fieldB = the Int 1, fieldA = "hi", imp = "Secret string"}
otherOk1 : Main.other.fieldB = (the Int 1)
otherOk1 = Refl
otherOk2 : Main.other.fieldA = "hi"
otherOk2 = Refl
otherOk3 : Main.other.imp = "Secret string"
otherOk3 = Refl
same : MkDog {age = 2, name = "Rex", weight = 10} = (the OrdinaryDog $ MkDog "Rex" 2 10)
same = Refl
namespace R1
public export
record R1 where
constructor MkR
field : a
namespace R2
public export
record R2 where
constructor MkR
{auto field : a}
r1 : R1 -- explicit fields access
r1 = MkR {field = "string"}
r2_shouldNotTypecheck1 : ?
r2_shouldNotTypecheck1 = MkR {field = the Nat 22} -- fail, impossible to disambiguate
interface Show a => (num : Num a) => MyIface a where -- Some interface with
constructor MkIface
-- constraints
data MyData : a -> Type -- and a data declaration.
someFunc : a -> a -- Constraints are now elaborated as auto implicits (as one would expect)
giveBack : {x : a} -> MyData x -> a -- (previously as explicit arguments of the interface
-- constructor)
data MyDataImpl : a -> Type where -- implementation of MyData
MkMyData : (x : a) -> MyDataImpl x
-- implementation MyIface Int where
-- MyData = MyDataImpl
-- someFunc = id
-- giveBack (MkMyData x) = x
%hint
instanceMyIfaceInt : MyIface Integer -- this def, roughly speaking, is the 'same thing' as the above implementation
-- Show Int, Num Int are auto implicits of MkIface
instanceMyIfaceInt = MkIface { MyData = MyDataImpl
, someFunc = id
, giveBack = \(MkMyData x) => x
, num = %search } -- auto implicit names are preserved
instanceOk : giveBack (MkMyData 22) = 22
instanceOk = Refl
interface Show' a where -- unlike Show, Show' reduces in types
constructor MkShow'
show' : a -> String
Show' String where
show' = id
%hint
showMaybe' : Show' a => Show' (Maybe a)
showMaybe' = MkShow' { show' = fromMaybe "Nothing" . (("Just " ++ ) . show' <$>) }
showMaybe'Ok : show' (Just "nice") = "Just nice"
showMaybe'Ok = Refl
record AllFieldTypes a where
constructor MkAllFieldTypes
exp : a
{imp : a}
{auto aut : a}
testAllFieldTypesOk : MkAllFieldTypes { aut = "aut"
, exp = "exp"
, imp = "imp" }
= MkAllFieldTypes "exp" {imp = "imp"} @{"aut"}
testAllFieldTypesOk = Refl
-------------------------------------
------ The Update syntax --------
mapName : (String -> String) -> OrdinaryDog -> OrdinaryDog
mapName f = {name $= f}
setName : String -> OrdinaryDog -> OrdinaryDog
setName name' = {name := name'}
data Three : Type -> Type -> Type -> Type where
MkThree : (x : a) -> (y : b) -> (z : c) -> Three a b c
mapSetMap : (a -> a') -> b' -> (c -> c') -> Three a b c -> Three a' b' c'
mapSetMap f y' g = {x $= f, y := y', z $= g}
setNameOld : String -> OrdinaryDog -> OrdinaryDog
setNameOld name' = record {name = name'}
-------------------------------------
--------- Applications in presence of duplicate names ----------
-- Duplicate names are ok and treated sequentially
testDuplicateNames : {auto a : String} -> {auto a : String} -> String
testDuplicateNames @{a} @{a'} = show' a ++ ":" ++ show' a'
-- When binding arguments on LHS or listing arguments to
-- a function on RHS
-- unnamed arguments always take priority over named,
-- i.e they are bound/applied first,
-- regardless of their relative positions to named ones
testOrder1 : (a : String) -> (a : String) -> String
testOrder1 {a = a2} {-snd-} a1 {-fst-} = a1 ++ a2
testOrder1Ok : Main.testOrder1 "abc" "def" = "abcdef"
testOrder1Ok = Refl
-- unnamed explicit "1" is passed first, followed by named {a = "2"}
testAutoPriorityOk : Main.testOrder1 {a = "2"} "1" = "12"
testAutoPriorityOk = Refl
-- Two arguments with the same name can be successfully bound
-- if one of them is renamed in patterns.
-- As both arguments are requested by name
-- They are bound in the same order they are given
sameNamesOk : (a : String) -> (a : Nat) -> (String, Nat)
sameNamesOk {a {- = a-}, a = b} = (a, b)
-- All arguments are named and are of different `plicities`. Binds occur sequentially.
-- Arguments are renamed on LHS
eachArgType : (a : String) -> {a : String} -> {auto a : String} -> String
eachArgType {a = a1, a = a2, a = a3} = a1 ++ a2 ++ a3
eachArgTypeOk : eachArgType @{"3"} "1" {a = "2"} = "123"
eachArgTypeOk = Refl
-- Arguments with the same names are provided on RHS
-- which is ok, they are passed sequentially.
eachArgTypeOk2 : eachArgType {a = "1", a = "2", a = "3"} = "123"
eachArgTypeOk2 = Refl
----------------------------------------
--------- Bind-all-explicits pattern ----------
-- This pattern works like inexhaustible supply of
-- `_` (Match-any patterns).
-- Here to complete the definition we only
-- need to know the name of the OrdinaryDog.
-- We bind it with `{name, _}` also stating that
-- any extra explicits should be disregarded,
-- by inserting `_` into the braces.
onlyName : OrdinaryDog -> String
onlyName (MkDog {name, _ {-age, weight-} }) = name
dontCare : (x : String) -> (y : String) -> (z : String) -> String
dontCare {x, z, _} = x ++ z
dontCareOk : Main.dontCare "a" "b" "c" = "ac"
dontCareOk = Refl
-- If none of the explicit arguments are wanted
-- one `{}` can be used instead of writing an underscore for each.
dontCare2 : (x : Nat) -> Nat -> Nat -> Nat -> (y : Nat) -> x + y = y + x
dontCare2 {} = plusCommutative {}
-- dontCare2 _ _ _ _ _ = plusCommutative _ _
data Tree a = Leaf a | Node (Tree a) a (Tree a)
isNode : Tree a -> Bool
isNode (Node {}) = True
isNode _ = False
data IsNode : Tree a -> Type where
Is : IsNode (Node {})
decIsNode : (x : Tree a) -> Dec (IsNode x)
decIsNode (Node {}) = Yes Is
decIsNode (Leaf {}) = No (\case Is impossible)
------------------------------------------------

15
tests/idris2/basic049/expected Normal file
View File

@ -0,0 +1,15 @@
1/1: Building Fld (Fld.idr)
Error: While processing right hand side of r2_shouldNotTypecheck1. Ambiguous elaboration. Possible results:
Main.R2.MkR
Main.R1.MkR Type
Fld.idr:72:26--72:29
|
72 | r2_shouldNotTypecheck1 = MkR {field = the Nat 22} -- fail, impossible to disambiguate
| ^^^
Main> Main.myDog : OrdinaryDog
Main> Main.mySuperDog : SuperDog
Main> Main.other : Other String
Main> 1 hole: Main.r2_shouldNotTypecheck1
Main> Bye for now!

5
tests/idris2/basic049/input Normal file
View File

@ -0,0 +1,5 @@
:t myDog
:t mySuperDog
:t other
:m
:q

0
tests/idris2/record007/run → tests/idris2/basic049/run
View File

15
tests/idris2/basic050/Ilc.idr Normal file
View File

@ -0,0 +1,15 @@
f : (Int -> Bool) -> Int
f p = case (p 0, p 1) of
(False, False) => 0
(False, True) => 1
(True , False) => 2
(True , True) => 4
il : Int
il = f \x => x > 0
lc : Int
lc = f $ \case 0 => True ; _ => False
ilc : Int
ilc = f \case 0 => True; _ => False

6
tests/idris2/basic050/expected Normal file
View File

@ -0,0 +1,6 @@
1/1: Building Ilc (Ilc.idr)
Main> 1
Main> 2
Main> 2
Main>
Bye for now!

3
tests/idris2/basic050/input Normal file
View File

@ -0,0 +1,3 @@
il
lc
ilc

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

@ -0,0 +1,3 @@
$1 --no-color --console-width 0 --no-banner Ilc.idr < input
rm -rf build

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