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

[ fix #657 ] RigCount for interface parameters (#808)

Browse Source
This commit is contained in:
G. Allais 2020-12-11 11:58:26 +00:00 committed by GitHub
parent 88aa55e875
commit 3f6b99e979
No known key found for this signature in database
GPG Key ID: 4AEE18F83AFDEB23
39 changed files with 299 additions and 155 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

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 ()

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)

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)

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

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)

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

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

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

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

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

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

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

5
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.
@ -331,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)
@ -345,4 +345,3 @@ sequence = traverse id
public export
for : (Traversable t, Applicative f) => t a -> (a -> f b) -> f (t b)
for = flip traverse

4
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

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

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

27
src/Idris/Desugar.idr
View File

@ -687,28 +687,33 @@ mutual
-- pure [IReflect fc !(desugar AnyExpr ps tm)]
desugarDecl ps (PInterface fc vis cons_in tn doc params det conname body)
= do addDocString tn doc
let paramNames = map fst params
let cons = concatMap expandConstraint cons_in
cons' <- traverse (\ ntm => do tm' <- desugar AnyExpr (ps ++ map fst params)
cons' <- traverse (\ ntm => do tm' <- desugar AnyExpr (ps ++ paramNames)
(snd ntm)
pure (fst ntm, tm')) cons
params' <- traverse (\ ntm => do tm' <- desugar AnyExpr ps (snd ntm)
pure (fst ntm, tm')) params
params' <- traverse (\ (nm, (rig, tm)) =>
do tm' <- desugar AnyExpr ps tm
pure (nm, (rig, tm')))
params
-- Look for bindable names in all the constraints and parameters
let mnames = map dropNS (definedIn body)
let bnames = ifThenElse !isUnboundImplicits
(concatMap (findBindableNames True
(ps ++ mnames ++ map fst params) [])
(ps ++ mnames ++ paramNames) [])
(map Builtin.snd cons') ++
concatMap (findBindableNames True
(ps ++ mnames ++ map fst params) [])
(map Builtin.snd params'))
(ps ++ mnames ++ paramNames) [])
(map (snd . snd) params'))
[]
let paramsb = map (\ ntm => (Builtin.fst ntm,
doBind bnames (Builtin.snd ntm))) params'
let consb = map (\ ntm => (Builtin.fst ntm,
doBind bnames (Builtin.snd ntm))) cons'
let paramsb = map (\ (nm, (rig, tm)) =>
let tm' = doBind bnames tm in
(nm, (rig, tm')))
params'
let consb = map (\ (nm, tm) => (nm, doBind bnames tm)) cons'
body' <- traverse (desugarDecl (ps ++ mnames ++ map fst params)) body
body' <- traverse (desugarDecl (ps ++ mnames ++ paramNames)) body
pure [IPragma (\nest, env =>
elabInterface fc vis env nest consb
tn paramsb det conname

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

@ -51,13 +51,18 @@ bindImpls fc [] ty = ty
bindImpls fc ((n, r, ty) :: rest) sc
= IPi fc r Implicit (Just n) ty (bindImpls fc rest sc)
addDefaults : FC -> Name -> List Name -> List (Name, List ImpClause) ->
addDefaults : FC -> Name ->
(params : List (Name, RawImp)) -> -- parameters have been specialised, use them!
(allMethods : List Name) ->
(defaults : List (Name, List ImpClause)) ->
List ImpDecl ->
(List ImpDecl, List Name) -- Updated body, list of missing methods
addDefaults fc impName allms defs body
addDefaults fc impName params allms defs body
= let missing = dropGot allms body in
extendBody [] missing body
where
specialiseMeth : Name -> (Name, RawImp)
specialiseMeth n = (n, INamedApp fc (IVar fc n) (UN "__con") (IVar fc impName))
-- Given the list of missing names, if any are among the default definitions,
-- add them to the body
extendBody : List Name -> List Name -> List ImpDecl ->
@ -73,10 +78,12 @@ addDefaults fc impName allms defs body
-- That is, default method implementations could depend on
-- other methods.
-- (See test idris2/interface014 for an example!)
let mupdates
= map (\n => (n, 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)
@ -140,11 +147,12 @@ elabImplementation {vars} fc vis opts_in pass env nest is cons iname ps impln nu
logTerm "elab.implementation" 3 ("Found interface " ++ show cn) ity
log "elab.implementation" 3 $
" with params: " ++ show (params cdata)
++ " and parents: " ++ show (parents cdata)
++ " using implicits: " ++ show impsp
++ " and methods: " ++ show (methods cdata) ++ "\n"
++ "Constructor: " ++ show (iconstructor cdata) ++ "\n"
"\n with params: " ++ show (params cdata)
++ "\n specialised to: " ++ show ps
++ "\n and parents: " ++ show (parents cdata)
++ "\n using implicits: " ++ show impsp
++ "\n and methods: " ++ show (methods cdata) ++ "\n"
++ "\nConstructor: " ++ show (iconstructor cdata) ++ "\n"
logTerm "elab.implementation" 3 "Constructor type: " conty
log "elab.implementation" 5 $ "Making implementation " ++ show impName
@ -180,7 +188,9 @@ elabImplementation {vars} fc vis opts_in pass env nest is cons iname ps impln nu
-- 1.5. Lookup default definitions and add them to to body
let (body, missing)
= addDefaults fc impName (map (dropNS . fst) (methods cdata))
= addDefaults fc impName
(zip (params cdata) ps)
(map (dropNS . fst) (methods cdata))
(defaults cdata) body_in
log "elab.implementation" 5 $ "Added defaults: body is " ++ show body

67
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
@ -116,12 +118,13 @@ 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 =
@ -146,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)
@ -270,7 +273,7 @@ elabInterface : {vars : _} ->
Env Term vars -> NestedNames vars ->
(constraints : List (Maybe Name, RawImp)) ->
Name ->
(params : List (Name, RawImp)) ->
(params : List (Name, (RigCount, RawImp))) ->
(dets : List Name) ->
(conName : Maybe Name) ->
List ImpDecl ->
@ -299,9 +302,12 @@ elabInterface {vars} fc vis env nest constraints iname params dets mcon body
let implParams = getImplParams ty
updateIfaceSyn ns_iname conName
implParams (map fst params) (map snd constraints)
implParams paramNames (map snd constraints)
ns_meths ds
where
paramNames : List Name
paramNames = map fst params
nameCons : Int -> List (Maybe Name, RawImp) -> List (Name, RawImp)
nameCons i [] = []
nameCons i ((_, ty) :: rest)
@ -366,25 +372,25 @@ elabInterface {vars} fc vis env nest constraints iname params dets mcon body
Just (r, _, _, t) => pure (r, t)
Nothing => throw (GenericMsg fc ("No method named " ++ show n ++ " in interface " ++ show iname))
let ity = apply (IVar fc iname) (map (IVar fc) (map fst params))
let ity = apply (IVar fc iname) (map (IVar fc) paramNames)
-- Substitute the method names with their top level function
-- name, so they don't get implicitly bound in the name
methNameMap <- traverse (\n =>
do cn <- inCurrentNS n
pure (n, applyParams (IVar fc cn)
(map fst params)))
pure (n, applyParams (IVar fc cn) paramNames))
(map fst tydecls)
let dty = substNames vars methNameMap dty
let dty = bindPs params -- bind parameters
$ bindIFace fc ity -- bind interface (?!)
$ substNames vars methNameMap dty
dty_imp <- bindTypeNames [] (map fst tydecls ++ vars)
(bindIFace fc ity dty)
log "elab.interface" 5 $ "Default method " ++ show dn ++ " : " ++ show dty_imp
dty_imp <- bindTypeNames [] (map fst tydecls ++ vars) dty
log "elab.interface.default" 5 $ "Default method " ++ show dn ++ " : " ++ show dty_imp
let dtydecl = IClaim fc rig vis [] (MkImpTy fc dn dty_imp)
processDecl [] nest env dtydecl
let cs' = map (changeName dn) cs
log "elab.interface" 5 $ "Default method body " ++ show cs'
log "elab.interface.default" 5 $ "Default method body " ++ show cs'
processDecl [] nest env (IDef fc dn cs')
-- Reset the original context, we don't need to keep the definition
@ -392,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)
@ -425,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

17
src/Idris/Parser.idr
View File

@ -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
@ -1195,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
@ -1216,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)

6
src/Idris/Syntax.idr
View File

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

6
src/TTImp/Utils.idr
View File

@ -202,12 +202,14 @@ mutual
ImpClause -> ImpClause
substNamesClause' bvar bound ps (PatClause fc lhs rhs)
= let bound' = map UN (map snd (findBindableNames True bound [] lhs))
++ bound in
++ findIBindVars lhs
++ bound in
PatClause fc (substNames' bvar [] [] lhs)
(substNames' bvar bound' ps rhs)
substNamesClause' bvar bound ps (WithClause fc lhs wval flags cs)
= let bound' = map UN (map snd (findBindableNames True bound [] lhs))
++ bound in
++ findIBindVars lhs
++ bound in
WithClause fc (substNames' bvar [] [] lhs)
(substNames' bvar bound' ps wval) flags cs
substNamesClause' bvar bound ps (ImpossibleClause fc lhs)

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

2
tests/Main.idr
View File

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

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

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

7
tests/idris2/interface018/expected Normal file
View File

@ -0,0 +1,7 @@
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

5
tests/idris2/interface018/run Executable file
View File

@ -0,0 +1,5 @@
$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

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

@ -1,14 +1,14 @@
interface Queue (q: Type -> Type) where
empty : q a
interface Queue (0 q: Type -> Type) where
empty : q a
isEmpty : q a -> Bool
snoc : q a -> a -> q a
snoc : q a -> a -> q a
head : q a -> a
tail : q a -> q a
data CatList : (Type -> Type) -> Type -> Type where
E : CatList q a
E : CatList q a
C : {0 q : Type -> Type} -> a -> q (Lazy (CatList q a)) -> CatList q a
link : (Queue q) => CatList q a -> Lazy (CatList q a) -> CatList q a
link : (Queue q) => CatList q a -> Lazy (CatList q a) -> CatList q a
link E s = s -- Just to satisfy totality for now.
link (C x xs) s = C x (snoc xs s)