idris-lang/Idris2
1
1
Fork 0
mirror of https://github.com/idris-lang/Idris2.git synced 2024-12-25 12:42:02 +03:00
Code Issues Projects Releases Wiki Activity

Merge branch 'master' into interfaces

Browse Source
This commit is contained in:
Edwin Brady 2020-12-14 13:34:31 +00:00 committed by GitHub
commit c1f58d963f
No known key found for this signature in database
GPG Key ID: 4AEE18F83AFDEB23
86 changed files with 1188 additions and 427 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

1
CONTRIBUTORS
View File

@ -39,6 +39,7 @@ Ohad Kammar
Peter Hajdu
Rohit Grover
Rui Barreiro
Ruslan Feizerahmanov
Simon Chatterjee
then0rTh
Theo Butler

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)

6
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
@ -62,6 +63,11 @@ 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

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

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

@ -11,11 +11,11 @@ public export
NotNot : {n : Nat} -> {ts : Vect n Type} -> (r : Rel ts) -> Rel ts
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 =>
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
@ -26,7 +26,7 @@ doubleNegationElimination {ts = [] } @{dec} [] 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 =
let prfnn : (witness : HVect ts) -> uncurry (NotNot {ts} r) witness
@ -36,7 +36,7 @@ doubleNegationForall @{dec} forall_prf =
in curryAll prf
public export
doubleNegationExists : {n : Nat} -> {0 ts : Vect n Type} -> {r : Rel ts} -> Decidable 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 =
@ -47,4 +47,3 @@ doubleNegationExists {ts} {r} @{dec} nnxs =
witnessing : uncurry r witness
witnessing = doubleNegationElimination @{dec} witness witnessingnn
in introduceWitness witness witnessing

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

@ -12,7 +12,7 @@ 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)
@ -54,7 +54,7 @@ data DecOrdering : {lt : t -> t -> Type} -> (a,b : t) -> Type where
DecGT : forall lt . (b `lt` a) -> DecOrdering {lt = lt} a b
public export
interface StrictPreorder t spo => StrictOrdered t (spo : t -> t -> Type) where
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
@ -81,4 +81,3 @@ public export
-- Similarly
DecGT yltx => No $ \x_eq_y => absurd $ irreflexive @{pre} y
$ replace {p = \u => y `lt` u} x_eq_y yltx

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

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]

189
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,8 +67,9 @@ showcCleanStringChar c
where
pad : String -> String
pad str
= case isLTE (length str) 4 of
Yes _ => toString (List.replicate (natMinus 4 (length str)) '0') ++ 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
@ -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

8
src/Core/Context.idr
View File

@ -2224,10 +2224,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} ->

10
src/Core/Core.idr
View File

@ -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
@ -635,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

8
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} ->

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)

39
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)
@ -681,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 (maybe [tn] (\n => [tn, n]) conname)
(\nest, env =>
elabInterface fc vis env nest consb
@ -835,7 +846,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

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

@ -52,13 +52,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 ->
@ -74,10 +79,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, INamedApp fc (IVar fc n)
(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)
@ -146,11 +153,12 @@ elabImplementation {vars} fc vis opts_in pass env nest is cons iname ps named im
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
@ -187,7 +195,9 @@ elabImplementation {vars} fc vis opts_in pass env nest is cons iname ps named im
-- 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

79
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 AutoImplicit (map bhere constraints) (mkTy Explicit (map bname meths) retty)
con = MkImpTy fc conName !(bindTypeNames [] (map fst ps ++ map fst meths ++ vars) conty) in
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,17 +118,18 @@ 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])
@ -150,10 +149,10 @@ 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, INamedApp fc (IVar fc n)
@ -274,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 ->
@ -303,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)
@ -370,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
@ -396,6 +398,13 @@ 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)
@ -429,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

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} ->

82
src/Idris/Parser.idr
View File

@ -116,7 +116,7 @@ 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
@ -416,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
@ -537,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
@ -585,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)
@ -951,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"
@ -962,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
@ -1183,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
@ -1204,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)
@ -1768,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
@ -1778,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 =

5
src/Idris/REPL.idr
View File

@ -530,7 +530,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
@ -965,7 +965,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"))

10
src/Idris/Syntax.idr
View File

@ -225,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
@ -286,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 ->
@ -442,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
@ -973,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

19
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
@ -56,6 +65,8 @@ isLitLine str =
otherwise => case isLiterateLine styleOrg str of
(Just l, s) => (Just l, s)
otherwise => case isLiterateLine styleCMark str of
(Just l, s) => (Just l, s)
otherwise => case isLiterateLine styleTeX str of
(Just l, s) => (Just l, s)
otherwise => (Nothing, str)

12
src/TTImp/Parser.idr
View File

@ -647,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

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

5
src/TTImp/TTImp.idr
View File

@ -350,7 +350,7 @@ mutual
({vars : _} ->
NestedNames vars -> Env Term vars -> Core ()) ->
ImpDecl
ILog : (List String, Nat) -> ImpDecl
ILog : Maybe (List String, Nat) -> ImpDecl
export
Show ImpDecl where
@ -369,7 +369,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

2
src/TTImp/Utils.idr
View File

@ -202,11 +202,13 @@ mutual
ImpClause -> ImpClause
substNamesClause' bvar bound ps (PatClause fc lhs rhs)
= let bound' = map UN (map snd (findBindableNames True bound [] lhs))
++ 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))
++ findIBindVars lhs
++ bound in
WithClause fc (substNames' bvar [] [] lhs)
(substNames' bvar bound' ps wval) flags cs

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

7
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", "basic049",
"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",
@ -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",

12
tests/chez/concurrency001/Futures.idr
View File

@ -11,11 +11,11 @@ constant = do
let a = await $ fork "String"
putStrLn a
-- Issue related to usleep in MacOS brew sleep
-- Issue related to usleep in MacOS brew chez
macsleep : (us : Int) -> So (us >= 0) => IO ()
macsleep us =
if (os == "darwin")
then sleep (us `div` 1000)
then sleep (us `div` 10000)
else usleep us
partial
@ -28,7 +28,7 @@ futureHelloWorld (us, n) with (choose (us >= 0))
partial
simpleIO : IO (List Unit)
simpleIO = do
futures <- sequence $ futureHelloWorld <$> [(3000, "World"), (1000, "Bar"), (0, "Foo"), (2000, "Idris")]
futures <- sequence $ futureHelloWorld <$> [(30000, "World"), (10000, "Bar"), (0, "Foo"), (20000, "Idris")]
let awaited = await <$> futures
pure awaited
@ -40,16 +40,16 @@ erasureAndNonbindTest = do
_ <- forkIO $ do
putStrLn "This line is printed"
notUsed <- forkIO $ do
macsleep 1000
macsleep 10000
putStrLn "This line is also printed"
let _ = nonbind
let n = nonbind
macsleep 2000 -- Even if not explicitly awaited, we should let threads finish before exiting
macsleep 20000 -- Even if not explicitly awaited, we should let threads finish before exiting
map : IO ()
map = do
future1 <- forkIO $ do
macsleep 1000
macsleep 10000
putStrLn "#2"
let future3 = map (const "#3") future1
future2 <- forkIO $ do

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

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

17
tests/idris2/basic051/Issue833.idr Normal file
View File

@ -0,0 +1,17 @@
module Issue833
import Data.Fin
%default total
data Singleton : Nat -> Type where
Sing : {n : Nat} -> Singleton n
f : (n : Singleton Z) -> n === Sing
f = \ Sing => Refl
g : (k : Fin 1) -> k === FZ
g = \ FZ => Refl
sym : {t, u : a} -> t === u -> u === t
sym = \Refl => Refl

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

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

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

@ -0,0 +1,3 @@
$1 --no-color --console-width 0 --no-banner --check Issue833.idr
rm -rf build

3
tests/idris2/interface003/Do.idr
View File

@ -1,5 +1,5 @@
public export
interface Do (m : Type) where
interface Do (0 m : Type) where
Next : (a : Type) -> (b : Type) -> m -> Type
bind : (x : m) -> Next a b x
@ -9,4 +9,3 @@ public export
Monad m => Do (m a) where
Next a b x = (a -> m b) -> m b
bind x = ?foo

3
tests/idris2/interface004/Do.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
@ -12,4 +12,3 @@ foo : Maybe Int -> Maybe Int -> Maybe Int
foo x y
= bind x (\x' =>
bind y (\y' => Just (x' + y')))

2
tests/idris2/interface006/Apply.idr
View File

@ -26,7 +26,7 @@ export
||| Biapplys (not to be confused with Biapplicatives)
||| @p The action of the Biapply on pairs of objects
public export
interface Bifunctor p => Biapply (p : Type -> Type -> Type) where
interface Bifunctor p => Biapply (0 p : Type -> Type -> Type) where
||| Applys a Bifunctor of functions to another Bifunctor of the same type
|||

2
tests/idris2/interface006/Bimonad.idr
View File

@ -8,7 +8,7 @@ infixl 4 >>==
||| @p the action of the first Bifunctor component on pairs of objects
||| @q the action of the second Bifunctor component on pairs of objects
interface (Biapplicative p, Biapplicative q) =>
Bimonad (p : Type -> Type -> Type) (q : Type -> Type -> Type) where
Bimonad (0 p : Type -> Type -> Type) (0 q : Type -> Type -> Type) where
bijoin : (p (p a b) (q a b), q (p a b) (q a b)) -> (p a b, q a b)
bijoin p = p >>== (id, id)

26
tests/idris2/interface018/Sized.idr Normal file
View File

@ -0,0 +1,26 @@
import Data.Buffer
%default total
public export
interface Singleton (n : Nat) where
sing : (m : Nat ** m === n)
sing = (n ** Refl)
Singleton 3 where
Singleton 5 where
export
data ForeignPtr : Type -> Type where
MkFP : Buffer -> ForeignPtr a
public export
interface Storable (0 a : Type) (n : Nat) | a where
constructor MkStorable
peekByteOff : HasIO io => ForeignPtr a -> Int -> io a
peekElemOff : HasIO io => ForeignPtr a -> Int -> io a
peekElemOff fp off = peekByteOff fp (off * cast n)
Storable Bits8 8 where
peekByteOff (MkFP b) off = getBits8 b off

18
tests/idris2/interface018/Sized2.idr Normal file
View File

@ -0,0 +1,18 @@
import Data.Buffer
export
data ForeignPtr : Type -> Type where
MkFP : Buffer -> ForeignPtr a
public export
interface Storable a where
size : Int
peekByteOff : HasIO io => ForeignPtr a -> Int -> io a
peekElemOff : HasIO io => ForeignPtr a -> Int -> io a
peekElemOff fp off = peekByteOff fp (off * size {a})
Storable Bits8 where
size = 8
peekByteOff (MkFP b) off = getBits8 b off

20
tests/idris2/interface018/Sized3.idr Normal file
View File

@ -0,0 +1,20 @@
import Data.Buffer
export
data ForeignPtr : Type -> Type where
MkFP : Buffer -> ForeignPtr a
public export
interface Storable a where
size : ForeignPtr a -> Int
peekByteOff : HasIO io => ForeignPtr a -> Int -> io a
peekElemOff : HasIO io => ForeignPtr a -> Int -> io a
peekElemOff fp off = peekByteOff fp (off * size fp)
Storable Bits8 where
size _ = 8
peekByteOff (MkFP b) off = getBits8 b off

8
tests/idris2/interface018/expected
View File

@ -1 +1,7 @@
1/1: Building LocalInterface (LocalInterface.idr)
1/1: Building Sized (Sized.idr)
Main> 3
Main> 5
Main>
Bye for now!
1/1: Building Sized2 (Sized2.idr)
1/1: Building Sized3 (Sized3.idr)

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

@ -0,0 +1,3 @@
fst (the (m : Nat ** m === 3) sing)
fst (the (m : Nat ** m === 5) sing)
:q

4
tests/idris2/interface018/run
View File

@ -1,3 +1,5 @@
$1 --no-color --console-width 0 LocalInterface.idr --check
$1 --no-color --no-banner --console-width 0 Sized.idr < input
$1 --no-color --console-width 0 Sized2.idr --check
$1 --no-color --console-width 0 Sized3.idr --check
rm -rf build

17
tests/idris2/literate011/IEdit.md
View File

@ -4,9 +4,9 @@ data Vect : Nat -> Type -> Type where
(::) : a -> Vect k a -> Vect (S k) a
```
```idris
<!-- idris
%name Vect xs, ys, zs
```
-->
```idris
dupAll : Vect n a -> Vect n (a, a)
@ -14,3 +14,16 @@ dupAll xs = zipHere xs xs
where
zipHere : forall n . Vect n a -> Vect n b -> Vect n (a, b)
```
<!-- idris
data Foobar = MkFoo
-->
```idris
showFooBar : Foobar -> String
showFooBar MkFoo = "MkFoo"
```

36
tests/idris2/literate013/LitTeX.tex Normal file
View File

@ -0,0 +1,36 @@
\documentclass{article}
\usepackage{fancyvrb}
\usepackage{comment}
\DefineVerbatimEnvironment
{code}{Verbatim}
{} % Add fancy options here if you like.
\excludecomment{hidden}
\begin{hidden}
module LitTeX
%default total
\end{hidden}
\begin{document}
\begin{code}
data V a = Empty | Extend a (V a)
\end{code}
\begin{code}
isCons : V a -> Bool
isCons Empty = False
isCons (Extend _ _) = True
\end{code}
\begin{hidden}
namespace Hidden
data U a = Empty | Extend a (U a)
\end{hidden}
\end{document}

1
tests/idris2/literate013/expected
View File

@ -1 +1,2 @@
1/1: Building Lit (Lit.lidr)
1/1: Building LitTeX (LitTeX.tex)

2
tests/idris2/literate013/run
View File

@ -1,3 +1,3 @@
$1 --no-color --console-width 0 --no-banner --check Lit.lidr
$1 --no-color --console-width 0 --no-banner --check LitTeX.tex
rm -rf build

4
tests/idris2/positivity002/Issue660.idr
View File

@ -9,3 +9,7 @@ data C : Type -> Type where
data D : Type -> Type where
MkD : {0 a : Type} -> let 0 b = List a in b -> D a
%logging off
data E : Type where

2
tests/idris2/reg029/lqueue.idr
View File

@ -1,4 +1,4 @@
interface Queue (q: Type -> Type) where
interface Queue (0 q: Type -> Type) where
empty : q a
isEmpty : q a -> Bool
snoc : q a -> a -> q a

3
tests/idris2/reg035/Implicit.idr Normal file
View File

@ -0,0 +1,3 @@
interface A where
x : Nat
f : {auto pf : x = 0} -> ()

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

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

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

@ -0,0 +1,3 @@
$1 --no-color --console-width 0 Implicit.idr --check
rm -rf build

3
tests/typedd-book/chapter07/Tree.idr
View File

@ -19,3 +19,6 @@ Foldable Tree where
foldr f acc (Node left e right) = let leftfold = foldr f acc left
rightfold = foldr f leftfold right in
f e rightfold
null Empty = True
null _ = False