idris-lang/Idris2
1
1
Fork 0
mirror of https://github.com/idris-lang/Idris2.git synced 2024-11-27 13:40:15 +03:00
Code Issues Projects Releases Wiki Activity

Merge branch 'main' into constant_fin

Browse Source
This commit is contained in:
André Videla 2023-07-18 23:46:07 +09:00 committed by GitHub
commit a39bfc6ce3
No known key found for this signature in database
GPG Key ID: 4AEE18F83AFDEB23
41 changed files with 463 additions and 149 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

13
CHANGELOG.md
View File

@ -171,6 +171,9 @@
* `Eq` and `Ord` implementations for `Fin n` now run in constant time.
* Adds `getTermCols` and `getTermLines` to the base library. They return the size of the
terminal if either stdin or stdout is a tty.
#### System
* Changes `getNProcessors` to return the number of online processors rather than
@ -196,9 +199,15 @@
#### Papers
* In `Control.DivideAndConquer`: a port of the paper
`A Type-Based Approach to Divide-And-Conquer Recursion in Coq`
"A Type-Based Approach to Divide-And-Conquer Recursion in Coq"
by Pedro Abreu, Benjamin Delaware, Alex Hubers, Christa Jenkins,
J. Garret Morris, and Aaron Stump
J. Garret Morris, and Aaron Stump.
[https://doi.org/10.1145/3571196](https://doi.org/10.1145/3571196)
* Ports the first half of "Deferring the Details and Deriving Programs" by Liam
O'Connor as `Data.ProofDelay`.
[https://doi.org/10.1145/3331554.3342605](https://doi.org/10.1145/3331554.3342605)
[http://liamoc.net/images/deferring.pdf](http://liamoc.net/images/deferring.pdf)
### Other Changes

2
docs/source/conf.py
View File

@ -26,7 +26,7 @@ import sphinx_rtd_theme
# General information about the project.
project = 'Idris2'
copyright = '2020, The Idris Community'
copyright = '2020-2023, The Idris Community'
author = 'The Idris Community'
# The short X.Y version.

2
libs/base/Control/Function.idr
View File

@ -53,7 +53,7 @@ public export
public export
[BiinjFromComp] {f : a -> b -> c} -> {g : c -> d} ->
Biinjective (g .: f) => Biinjective f where
biinjective = biinjective {f = (g .: f)} . cong g
biinjective prf = biinjective {f = (g .: f)} $ cong g prf
public export
[FlipBiinjective] {f : a -> b -> c} ->

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

@ -59,6 +59,20 @@ accInd : {0 rel : a -> a -> Type} -> {0 P : a -> Type} ->
accInd step z (Access f) =
step z $ \y, lt => accInd step y (f y lt)
||| Depedently-typed induction for creating extrinsic proofs on results of `accInd`.
export
accIndProp : {0 P : a -> Type} ->
(step : (x : a) -> ((y : a) -> rel y x -> P y) -> P x) ->
{0 RP : (x : a) -> P x -> Type} ->
(ih : (x : a) ->
(f : (y : a) -> rel y x -> P y) ->
((y : a) -> (isRel : rel y x) -> RP y (f y isRel)) ->
RP x (step x f)) ->
(z : a) -> (0 acc : Accessible rel z) -> RP z (accInd step z acc)
accIndProp step ih z (Access rec) =
ih z (\y, lt => accInd step y (rec y lt))
(\y, lt => accIndProp {RP} step ih y (rec y lt))
||| Simply-typed recursion based on well-founded-ness.
|||
||| This is `accRec` applied to accessibility derived from a `WellFounded`
@ -79,6 +93,19 @@ wfInd : (0 _ : WellFounded a rel) => {0 P : a -> Type} ->
(myz : a) -> P myz
wfInd step myz = accInd step myz (wellFounded {rel} myz)
||| Depedently-typed induction for creating extrinsic proofs on results of `wfInd`.
export
wfIndProp : (0 _ : WellFounded a rel) =>
{0 P : a -> Type} ->
(step : (x : a) -> ((y : a) -> rel y x -> P y) -> P x) ->
{0 RP : (x : a) -> P x -> Type} ->
(ih : (x : a) ->
(f : (y : a) -> rel y x -> P y) ->
((y : a) -> (isRel : rel y x) -> RP y (f y isRel)) ->
RP x (step x f)) ->
(myz : a) -> RP myz (wfInd step myz)
wfIndProp step ih myz = accIndProp {RP} step ih myz (wellFounded {rel} myz)
||| Types that have a concept of size. The size must be a natural number.
public export
interface Sized a where

11
libs/base/Data/Bool.idr
View File

@ -71,6 +71,17 @@ orNotTrue : (x : Bool) -> x || not x = True
orNotTrue False = Refl
orNotTrue True = Refl
export
orBothFalse : {0 x, y : Bool} -> (0 prf : x || y = False) -> (x = False, y = False)
orBothFalse prf = unerase $ orBothFalse' prf
where
unerase : (0 prf : (x = False, y = False)) -> (x = False, y = False)
unerase (p, q) = (irrelevantEq p, irrelevantEq q)
orBothFalse' : {x, y : Bool} -> x || y = False -> (x = False, y = False)
orBothFalse' {x = False} yFalse = (Refl, yFalse)
orBothFalse' {x = True} trueFalse = absurd trueFalse
-- interaction & De Morgan's laws
export

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

@ -43,7 +43,7 @@ using (k : Nat)
connex {x = FZ} _ = Left $ FromNatPrf LTEZero
connex {y = FZ} _ = Right $ FromNatPrf LTEZero
connex {x = FS k} {y = FS j} prf =
case connex {rel = FinLTE} $ prf . (cong FS) of
case connex {rel = FinLTE} $ \c => prf $ cong FS c of
Left (FromNatPrf p) => Left $ FromNatPrf $ LTESucc p
Right (FromNatPrf p) => Right $ FromNatPrf $ LTESucc p

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

@ -279,7 +279,7 @@ infix 7 \\
|||
||| In the following example, the result is `[2, 4]`.
||| ```idris example
||| [1, 2, 3, 4] // [1, 3]
||| [1, 2, 3, 4] \\ [1, 3]
||| ```
|||
public export

14
libs/base/Data/List/Quantifiers.idr
View File

@ -166,6 +166,20 @@ namespace All
HList : List Type -> Type
HList = All id
export
splitAt : (xs : List a) -> All p (xs ++ ys) -> (All p xs, All p ys)
splitAt [] pxs = ([], pxs)
splitAt (_ :: xs) (px :: pxs) = mapFst (px ::) (splitAt xs pxs)
export
take : (xs : List a) -> All p (xs ++ ys) -> All p xs
take xs pxs = fst (splitAt xs pxs)
export
drop : (xs : List a) -> All p (xs ++ ys) -> All p ys
drop xs pxs = snd (splitAt xs pxs)
------------------------------------------------------------------------
-- Relationship between all and any

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

@ -123,7 +123,7 @@ Connex Nat LTE where
connex {x = Z} _ = Left LTEZero
connex {y = Z} _ = Right LTEZero
connex {x = S _} {y = S _} prf =
case connex $ prf . (cong S) of
case connex $ \xy => prf $ cong S xy of
Left jk => Left $ LTESucc jk
Right kj => Right $ LTESucc kj

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

@ -259,7 +259,7 @@ replaceAtDiffIndexPreserves : (xs : Vect n a) -> (i, j : Fin n) -> Not (i = j) -
replaceAtDiffIndexPreserves (_::_) FZ FZ co _ = absurd $ co Refl
replaceAtDiffIndexPreserves (_::_) FZ (FS _) _ _ = Refl
replaceAtDiffIndexPreserves (_::_) (FS _) FZ _ _ = Refl
replaceAtDiffIndexPreserves (_::_) (FS z) (FS w) co y = replaceAtDiffIndexPreserves _ z w (co . cong FS) y
replaceAtDiffIndexPreserves (_::_) (FS z) (FS w) co y = replaceAtDiffIndexPreserves _ z w (\zw => co $ cong FS zw) y
--------------------------------------------------------------------------------
-- Transformations

2
libs/base/Decidable/Equality/Core.idr
View File

@ -45,7 +45,7 @@ decEqCong $ No contra = No $ \c => contra $ inj f c
public export
decEqInj : (0 _ : Injective f) => Dec (f x = f y) -> Dec (x = y)
decEqInj $ Yes prf = Yes $ inj f prf
decEqInj $ No contra = No $ contra . cong f
decEqInj $ No contra = No $ \c => contra $ cong f c
public export
decEqCong2 : (0 _ : Biinjective f) => Dec (x = y) -> Lazy (Dec (v = w)) -> Dec (f x v = f y w)

27
libs/base/System/Term.idr Normal file
View File

@ -0,0 +1,27 @@
module System.Term
%default total
libterm : String -> String
libterm s = "C:" ++ s ++ ", libidris2_support, idris_term.h"
%foreign libterm "idris2_setupTerm"
prim__setupTerm : PrimIO ()
%foreign libterm "idris2_getTermCols"
prim__getTermCols : PrimIO Int
%foreign libterm "idris2_getTermLines"
prim__getTermLines : PrimIO Int
export
setupTerm : IO ()
setupTerm = primIO prim__setupTerm
export
getTermCols : IO Int
getTermCols = primIO prim__getTermCols
export
getTermLines : IO Int
getTermLines = primIO prim__getTermLines

3
libs/base/base.ipkg
View File

@ -127,4 +127,5 @@ modules = Control.App,
System.File.Virtual,
System.Info,
System.REPL,
System.Signal
System.Signal,
System.Term

49
libs/contrib/Data/List/Sufficient.idr
View File

@ -1,32 +1,23 @@
||| 'Sufficient' lists: a structurally inductive view of lists xs
||| as given by xs = non-empty prefix + sufficient suffix
|||
||| Useful for termination arguments for function definitions
||| which provably consume a non-empty (but otherwise arbitrary) prefix
||| *without* having to resort to ancillary WF induction on length etc.
||| e.g. lexers, parsers etc.
|||
||| Credited by Conor McBride as originally due to James McKinna
||| WellFounded on List suffixes
module Data.List.Sufficient
||| Sufficient view
public export
data Sufficient : (xs : List a) -> Type where
SuffAcc : {xs : List a}
-> (suff_ih : {x : a} -> {pre, suff : List a}
-> xs = x :: (pre ++ suff)
-> Sufficient suff)
-> Sufficient xs
import Control.WellFounded
||| Sufficient view covering property
export
sufficient : (xs : List a) -> Sufficient xs
sufficient [] = SuffAcc (\case _ impossible)
sufficient (x :: xs) with (sufficient xs)
sufficient (x :: xs) | suffxs@(SuffAcc suff_ih)
= SuffAcc (\case Refl => prf Refl)
where prf : {pre, suff : List a}
-> xs = pre ++ suff
-> Sufficient suff
prf {pre = []} Refl = suffxs
prf {pre = (y :: ys)} eq = suff_ih eq
%default total
public export
data Suffix : (ys,xs : List a) -> Type where
IsSuffix : (x : a) -> (zs : List a)
-> (0 ford : xs = x :: zs ++ ys) -> Suffix ys xs
SuffixAccessible : (xs : List a) -> Accessible Suffix xs
SuffixAccessible [] = Access (\y => \case (IsSuffix x zs _) impossible)
SuffixAccessible ws@(x :: xs) =
let fact1@(Access f) = SuffixAccessible xs
in Access $ \ys => \case
(IsSuffix x [] Refl) => fact1
(IsSuffix x (z :: zs) Refl) => f ys (IsSuffix z zs Refl)
public export
WellFounded (List a) Suffix where
wellFounded = SuffixAccessible

1
libs/papers/Control/DivideAndConquer.idr
View File

@ -2,6 +2,7 @@
||| A Type-Based Approach to Divide-And-Conquer Recursion in Coq
||| by Pedro Abreu, Benjamin Delaware, Alex Hubers, Christa Jenkins,
||| J. Garret Morris, and Aaron Stump
||| https://doi.org/10.1145/3571196
|||
||| The original paper relies on Coq's impredicative Set axiom,
||| something we don't have access to in Idris 2. We can however

6
libs/papers/Data/Container.idr
View File

@ -288,12 +288,12 @@ namespace Derivative
toPair v = case fromSum {c = Pair (Derivative c) d} {d = Pair c (Derivative d)} v of
Left p => let (MkExtension (shp1 ** p1) chld1, MkExtension shp2 chld2) = fromPair {c = Derivative c} p in
MkExtension ((shp1, shp2) ** Left p1) $ \ (p' ** neq) => case p' of
Left p1' => chld1 (p1' ** (neq . cong Left))
Left p1' => chld1 (p1' ** (\prf => neq $ cong Left prf))
Right p2' => chld2 p2'
Right p => let (MkExtension shp1 chld1, MkExtension (shp2 ** p2) chld2) = fromPair {c} {d = Derivative d} p in
MkExtension ((shp1, shp2) ** Right p2) $ \ (p' ** neq) => case p' of
Left p1' => chld1 p1'
Right p2' => chld2 (p2' ** (neq . cong Right))
Right p2' => chld2 (p2' ** (\prf => neq $ cong Right prf))
export
fromPair : Extension (Derivative (Pair c d)) x ->
@ -323,7 +323,7 @@ namespace Derivative
right = toCompose
$ MkExtension (shp1 ** p1)
$ \ (p1' ** neqp1) => MkExtension (shp2 p1')
$ \ p2' => chld ((p1' ** p2') ** (neqp1 . cong fst))
$ \ p2' => chld ((p1' ** p2') ** (\prf => neqp1 $ cong fst prf))
export
toCompose : ((s : _) -> DecEq (Position c s)) -> ((s : _) -> DecEq (Position d s)) ->

149
libs/papers/Data/ProofDelay.idr Normal file
View File

@ -0,0 +1,149 @@
||| The contents of this module are based on the paper
||| Deferring the Details and Deriving Programs
||| by Liam O'Connor
||| https://doi.org/10.1145/3331554.3342605
module Data.ProofDelay
import Data.Nat
import Data.List.Quantifiers
%default total
||| A type `x` which can only be computed once some, delayed, proof obligations
||| have been fulfilled.
public export
record PDelay (x : Type) where
constructor Prf
||| List of propositions we need to prove.
goals : List Type
||| Given the proofs required (i.e. the goals), actually compute the value x.
prove : HList goals -> x
||| A value which can immediately be constructed (i.e. no delayed proofs).
public export
pure : tx -> PDelay tx
pure x = Prf [] (const x)
||| Delay the full computation of `x` until `later`.
public export
later : {tx : _} -> PDelay tx
later = Prf (tx :: []) (\(x :: []) => x)
-- pronounced "apply"
||| We can compose `PDelay` computations.
public export
(<*>) : PDelay (a -> b) -> PDelay a -> PDelay b
(Prf goals1 prove1) <*> (Prf goals2 prove2) =
Prf (goals1 ++ goals2) $ \hl =>
let (left , right) = splitAt _ hl in
prove1 left (prove2 right)
------------------------------------------------------------------------
-- Example uses
||| An ordered list type.
|||
||| [27](https://dl.acm.org/doi/10.1145/2503778.2503786)
public export
data OList : (m, n : Nat) -> Type where
Nil : (m `LTE` n) -> OList m n
Cons : (x : Nat) -> (m `LTE` x) -> OList x n -> OList m n
||| A binary search tree carrying proofs of the ordering in the leaves.
|||
||| [31](https://dl.acm.org/doi/10.1145/2628136.2628163)
public export
data BST : (m, n : Nat) -> Type where
Leaf : (m `LTE` n) -> BST m n
Branch : (x : Nat) -> (l : BST m x) -> (r : BST x n) -> BST m n
-- OList
||| OList `Nil`, but delaying the proof obligation.
public export
nil : {m, n : Nat} -> PDelay (OList m n)
nil = [| Nil later |]
||| OList `Cons`, but delaying the proof obligations.
public export
cons : {m, n : Nat} -> (x : Nat) -> PDelay (OList x n) -> PDelay (OList m n)
cons x xs =
let cx : ? -- Idris can figure out the type
cx = Cons x
in [| cx later xs |]
||| Extracting an actual `OList` from the delayed version requires providing the
||| unergonomic proofs.
public export
example : OList 1 5
example =
let structure : ?
structure = 1 `cons` (2 `cons` (3 `cons` (4 `cons` (5 `cons` nil))))
proofs : HList ?
proofs = LTESucc LTEZero
:: LTESucc LTEZero
:: LTESucc (LTESucc LTEZero)
:: LTESucc (LTESucc (LTESucc LTEZero))
:: LTESucc (LTESucc (LTESucc (LTESucc LTEZero)))
:: LTESucc (LTESucc (LTESucc (LTESucc (LTESucc LTEZero))))
:: []
in structure.prove proofs
-- BST
||| BST `Leaf`, but delaying the proof obligation.
public export
leaf : {m, n : Nat} -> PDelay (BST m n)
leaf = [| Leaf later |]
||| BST `Branch`, but delaying the proof obligations.
public export
branch : {m, n : Nat}
-> (x : Nat)
-> (l : PDelay (BST m x))
-> (r : PDelay (BST x n))
-> PDelay (BST m n)
branch x l r =
let bx : ?
bx = Branch x
in [| bx l r |]
||| Once again, extracting the actual `BST` requires providing the uninteresting
||| proofs.
public export
example2 : BST 2 10
example2 =
let structure : ?
structure = branch 3
(branch 2 leaf leaf)
(branch 5
(branch 4 leaf leaf)
(branch 10 leaf leaf))
-- we _could_ construct the proofs by hand, but Idris can just also find
-- them (as long as we tell it which proof to find)
proofs : HList ?
proofs = the ( 2 `LTE` 2) %search
:: the ( 2 `LTE` 3) %search
:: the ( 3 `LTE` 4) %search
:: the ( 4 `LTE` 5) %search
:: the ( 5 `LTE` 10) %search
:: the (10 `LTE` 10) %search
:: []
{- proofs = LTESucc (LTESucc LTEZero)
- :: LTESucc (LTESucc LTEZero)
- :: LTESucc (LTESucc (LTESucc LTEZero))
- :: LTESucc (LTESucc (LTESucc (LTESucc LTEZero)))
- :: LTESucc (LTESucc (LTESucc (LTESucc (LTESucc LTEZero))))
- :: LTESucc (LTESucc (LTESucc (LTESucc (LTESucc (LTESucc
- (LTESucc (LTESucc (LTESucc (LTESucc LTEZero)))))))))
- :: []
-}
in structure.prove proofs

6
libs/papers/Search/Auto.idr
View File

@ -259,8 +259,8 @@ thinApart FZ FZ neq = absurd (neq Refl)
thinApart FZ (FS y') neq = (y' ** Refl)
thinApart (FS FZ) FZ neq = (FZ ** Refl)
thinApart (FS (FS x)) FZ neq = (FZ ** Refl)
thinApart (FS x@FZ) (FS y) neq = bimap FS (cong FS) (thinApart x y (neq . cong FS))
thinApart (FS x@(FS{})) (FS y) neq = bimap FS (cong FS) (thinApart x y (neq . cong FS))
thinApart (FS x@FZ) (FS y) neq = bimap FS (\prf => cong FS prf) (thinApart x y (\prf => neq $ cong FS prf))
thinApart (FS x@(FS{})) (FS y) neq = bimap FS (\prf => cong FS prf) (thinApart x y (\prf => neq $ cong FS prf))
public export
data Thicken : (x, y : Fin n) -> Type where
@ -462,7 +462,7 @@ apply r args = let (premises, rest) = splitAt r.arity args in
mkVars : (m : Nat) -> (vars : SnocList Name ** length vars = m)
mkVars Z = ([<] ** Refl)
mkVars m@(S m') = bimap (:< UN (Basic $ "_invalidName" ++ show m)) (cong S) (mkVars m')
mkVars m@(S m') = bimap (:< UN (Basic $ "_invalidName" ++ show m)) (\prf => cong S prf) (mkVars m')
solveAcc : {m : _} -> Nat -> HintDB -> PartialProof m -> Space Proof
solveAcc idx rules (MkPartialProof 0 goals k)

2
libs/papers/papers.ipkg
View File

@ -26,6 +26,8 @@ modules = Control.DivideAndConquer,
Data.OpenUnion,
Data.ProofDelay,
Data.Recursion.Free,
Data.Tree.Perfect,

6
libs/prelude/Prelude/Basics.idr
View File

@ -99,18 +99,18 @@ public export
||| Equality is a congruence.
public export
cong : (0 f : t -> u) -> (p : a = b) -> f a = f b
cong : (0 f : t -> u) -> (0 p : a = b) -> f a = f b
cong f Refl = Refl
||| Two-holed congruence.
export
-- These are natural in equational reasoning.
cong2 : (0 f : t1 -> t2 -> u) -> (p1 : a = b) -> (p2 : c = d) -> f a c = f b d
cong2 : (0 f : t1 -> t2 -> u) -> (0 p1 : a = b) -> (0 p2 : c = d) -> f a c = f b d
cong2 f Refl Refl = Refl
||| Irrelevant equalities can always be made relevant
export
irrelevantEq : (0 _ : a === b) -> a === b
irrelevantEq : (0 _ : a ~=~ b) -> a ~=~ b
irrelevantEq Refl = Refl
--------------

2
src/Core/Case/CaseBuilder.idr
View File

@ -381,7 +381,7 @@ conTypeEq (CName x tag) (CName x' tag')
Yes Refl => Just Refl
No contra => Nothing
conTypeEq CDelay CDelay = Just Refl
conTypeEq (CConst x) (CConst y) = cong CConst <$> constantEq x y
conTypeEq (CConst x) (CConst y) = (\xy => cong CConst xy) <$> constantEq x y
conTypeEq _ _ = Nothing
data Group : List Name -> -- variables in scope

2
src/Core/Name.idr
View File

@ -410,7 +410,7 @@ nameEq (NS xs x) (NS ys y) with (decEq xs ys)
nameEq (NS ys x) (NS ys y) | (Yes Refl) | Nothing = Nothing
nameEq (NS ys y) (NS ys y) | (Yes Refl) | (Just Refl) = Just Refl
nameEq (NS xs x) (NS ys y) | (No contra) = Nothing
nameEq (UN x) (UN y) = map (cong UN) (userNameEq x y)
nameEq (UN x) (UN y) = map (\xy => cong UN xy) (userNameEq x y)
nameEq (MN x t) (MN x' t') with (decEq x x')
nameEq (MN x t) (MN x t') | (Yes Refl) with (decEq t t')
nameEq (MN x t) (MN x t) | (Yes Refl) | (Yes Refl) = Just Refl

2
src/Core/TT.idr
View File

@ -189,7 +189,7 @@ constantEq (Ch x) (Ch y) = case decEq x y of
Yes Refl => Just Refl
No contra => Nothing
constantEq (Db x) (Db y) = Nothing -- no DecEq for Doubles!
constantEq (PrT x) (PrT y) = cong PrT <$> primTypeEq x y
constantEq (PrT x) (PrT y) = (\xy => cong PrT xy) <$> primTypeEq x y
constantEq WorldVal WorldVal = Just Refl
constantEq _ _ = Nothing

2
src/Libraries/Utils/Term.idr
View File

@ -2,6 +2,8 @@ module Libraries.Utils.Term
%default total
-- TODO: remove this file and use System.Term after version following 0.6.0 is released
libterm : String -> String
libterm s = "C:" ++ s ++ ", libidris2_support, idris_term.h"

4
src/TTImp/Elab/Local.idr
View File

@ -54,9 +54,7 @@ localHelper {vars} nest env nestdecls_in func
else nestdeclsVis
let defNames = definedInBlock emptyNS nestdeclsMult
names' <- traverse (applyEnv f)
(nub defNames) -- binding names must be unique
-- fixes bug #115
names' <- traverse (applyEnv f) defNames
let nest' = { names $= (names' ++) } nest
let env' = dropLinear env
-- We don't want to keep rechecking delayed elaborators in the

29
src/TTImp/TTImp.idr
View File

@ -13,6 +13,8 @@ import Data.List
import Data.List1
import Data.Maybe
import Libraries.Data.SortedSet
%default covering
-- Information about names in nested blocks
@ -772,7 +774,7 @@ export
definedInBlock : Namespace -> -- namespace to resolve names
List ImpDecl -> List Name
definedInBlock ns decls =
concatMap (defName ns) decls
SortedSet.toList $ foldl (defName ns) empty decls
where
getName : ImpTy -> Name
getName (MkImpTy _ _ n _) = n
@ -788,16 +790,17 @@ definedInBlock ns decls =
DN _ _ => NS ns n
_ => n
defName : Namespace -> ImpDecl -> List Name
defName ns (IClaim _ _ _ _ ty) = [expandNS ns (getName ty)]
defName ns (IData _ _ _ (MkImpData _ n _ _ cons))
= expandNS ns n :: map (expandNS ns) (map getName cons)
defName ns (IData _ _ _ (MkImpLater _ n _)) = [expandNS ns n]
defName ns (IParameters _ _ pds) = concatMap (defName ns) pds
defName ns (IFail _ _ nds) = concatMap (defName ns) nds
defName ns (INamespace _ n nds) = concatMap (defName (ns <.> n)) nds
defName ns (IRecord _ fldns _ _ (MkImpRecord _ n _ opts con flds))
= expandNS ns con :: all
defName : Namespace -> SortedSet Name -> ImpDecl -> SortedSet Name
defName ns acc (IClaim _ _ _ _ ty) = insert (expandNS ns (getName ty)) acc
defName ns acc (IDef _ nm _) = insert (expandNS ns nm) acc
defName ns acc (IData _ _ _ (MkImpData _ n _ _ cons))
= foldl (flip insert) acc $ expandNS ns n :: map (expandNS ns . getName) cons
defName ns acc (IData _ _ _ (MkImpLater _ n _)) = insert (expandNS ns n) acc
defName ns acc (IParameters _ _ pds) = foldl (defName ns) acc pds
defName ns acc (IFail _ _ nds) = foldl (defName ns) acc nds
defName ns acc (INamespace _ n nds) = foldl (defName (ns <.> n)) acc nds
defName ns acc (IRecord _ fldns _ _ (MkImpRecord _ n _ opts con flds))
= foldl (flip insert) acc $ expandNS ns con :: all
where
fldns' : Namespace
fldns' = maybe ns (\ f => ns <.> mkNamespace f) fldns
@ -822,8 +825,8 @@ definedInBlock ns decls =
all : List Name
all = expandNS ns n :: map (expandNS fldns') (fnsRF ++ fnsUN)
defName ns (IPragma _ pns _) = map (expandNS ns) pns
defName _ _ = []
defName ns acc (IPragma _ pns _) = foldl (flip insert) acc $ map (expandNS ns) pns
defName _ acc _ = acc
export
isIVar : RawImp' nm -> Maybe (FC, nm)

14
support/c/idris_term.c
View File

@ -36,13 +36,23 @@ void idris2_setupTerm() {
int idris2_getTermCols() {
struct winsize ts;
ioctl(0, TIOCGWINSZ, &ts);
int err = ioctl(0, TIOCGWINSZ, &ts);
if (err) {
err = ioctl(1, TIOCGWINSZ, &ts);
}
if (err)
return 0;
return (int)ts.ws_col;
}
int idris2_getTermLines() {
struct winsize ts;
ioctl(0, TIOCGWINSZ, &ts);
int err = ioctl(0, TIOCGWINSZ, &ts);
if (err) {
err = ioctl(1, TIOCGWINSZ, &ts);
}
if (err)
return 0;
return (int)ts.ws_row;
}

4
tests/Main.idr
View File

@ -42,7 +42,7 @@ idrisTestsBasic = MkTestPool "Fundamental language features" [] Nothing
"basic051", "basic052", "basic053", "basic054", "basic055",
"basic056", "basic057", "basic058", "basic059", "basic060",
"basic061", "basic062", "basic063", "basic064", "basic065",
"basic066", "basic067", "basic068", "basic069",
"basic066", "basic067", "basic068", "basic069", "basic070",
"idiom001",
"dotted001",
"rewrite001",
@ -204,7 +204,7 @@ idrisTestsAllSchemes : Requirement -> TestPool
idrisTestsAllSchemes cg = MkTestPool
("Test across all scheme backends: " ++ show cg ++ " instance")
[] (Just cg)
[ "scheme001"
[ "scheme001", "scheme002"
, "channels001", "channels002", "channels003", "channels004", "channels005"
, "channels006"
]

7
tests/allschemes/scheme002/TermSize.idr Normal file
View File

@ -0,0 +1,7 @@
import System.Term
main : IO ()
main = do
width <- getTermCols
height <- getTermLines
printLn "Success \{show $ width > 0} \{show $ height > 0}"

1
tests/allschemes/scheme002/expected Normal file
View File

@ -0,0 +1 @@
"Success False False"

13
tests/allschemes/scheme002/run Executable file
View File

@ -0,0 +1,13 @@
rm -rf build
# observe that errors are correctly reported as zero.
$1 --exec main TermSize.idr </dev/null
# The following should report True True, but the ci scripts don't
# provide a terminal
# $1 --exec main TermSize.idr
# The following should also report True True if the output is a terminal,
# but the testing framework redirects output.
# idris2 --exec main tests/allschemes/scheme002/TermSize.idr </dev/null

2
tests/base/deriving_traversable/expected
View File

@ -65,7 +65,7 @@ LOG derive.traversable.clauses:1:
traverseIVect : {0 m : _} -> {0 a, b : Type} -> {0 f : Type -> Type} -> Applicative f => (a -> f b) -> IVect {n = m} a -> f (IVect {n = m} b)
traverseIVect f (MkIVect x2) = MkIVect <$> (traverse f x2)
LOG derive.traversable.clauses:1:
traverseEqMap : {0 key, eq : _} -> {0 a, b : Type} -> {0 f : Type -> Type} -> Applicative f => (a -> f b) -> EqMap key {{conArg:13922} = eq} a -> f (EqMap key {{conArg:13922} = eq} b)
traverseEqMap : {0 key, eq : _} -> {0 a, b : Type} -> {0 f : Type -> Type} -> Applicative f => (a -> f b) -> EqMap key {{conArg:13919} = eq} a -> f (EqMap key {{conArg:13919} = eq} b)
traverseEqMap f (MkEqMap x3) = MkEqMap <$> (traverse (traverse f) x3)
LOG derive.traversable.clauses:1:
traverseTree : {0 l : _} -> {0 a, b : Type} -> {0 f : Type -> Type} -> Applicative f => (a -> f b) -> Tree l a -> f (Tree l b)

4
tests/idris2/basic070/Issue2592.idr Normal file
View File

@ -0,0 +1,4 @@
bar = 3
where wat = 2
baz = 3
where wat = 2

6
tests/idris2/basic070/Issue2593.idr Normal file
View File

@ -0,0 +1,6 @@
two: Nat
two = 2
bar: a -> a
bar x = x where
wat = two

9
tests/idris2/basic070/Issue2782.idr Normal file
View File

@ -0,0 +1,9 @@
foo : Integer
foo =
let z : Int
z = 1
y = 1
in y
fee : Integer
fee = y

9
tests/idris2/basic070/Issue3016.idr Normal file
View File

@ -0,0 +1,9 @@
import Data.String
test str = len
where
xs = words str
len = length xs
parameters (n : Nat) (strs : List String)
len = List.length strs

14
tests/idris2/basic070/expected Normal file
View File

@ -0,0 +1,14 @@
1/1: Building Issue3016 (Issue3016.idr)
1/1: Building Issue2782 (Issue2782.idr)
Error: While processing right hand side of fee. Undefined name y.
Issue2782:9:7--9:8
5 | y = 1
6 | in y
7 |
8 | fee : Integer
9 | fee = y
^
1/1: Building Issue2592 (Issue2592.idr)
1/1: Building Issue2593 (Issue2593.idr)

6
tests/idris2/basic070/run Executable file
View File

@ -0,0 +1,6 @@
rm -rf build
$1 --no-color --console-width 0 --no-banner --check Issue3016.idr
$1 --no-color --console-width 0 --no-banner --check Issue2782.idr
$1 --no-color --console-width 0 --no-banner --check Issue2592.idr
$1 --no-color --console-width 0 --no-banner --check Issue2593.idr

138
tests/idris2/evaluator002/expected
View File

@ -1,89 +1,89 @@
1/2: Building Lib (Lib.idr)
LOG eval.stuck.outofscope:5: Stuck function: Lib.{_:2558}
LOG eval.stuck.outofscope:5: Stuck function: Lib.{_:2559}
LOG eval.stuck.outofscope:5: Stuck function: Lib.{_:2559}
LOG eval.stuck.outofscope:5: Stuck function: Lib.{_:2559}
LOG eval.stuck.outofscope:5: Stuck function: Lib.{_:2559}
LOG eval.stuck.outofscope:5: Stuck function: Lib.{_:2559}
LOG eval.stuck.outofscope:5: Stuck function: Lib.{_:2558}
LOG eval.stuck.outofscope:5: Stuck function: Lib.{_:2558}
LOG eval.stuck.outofscope:5: Stuck function: Lib.{_:2558}
LOG eval.stuck.outofscope:5: Stuck function: Lib.{_:2555}
LOG eval.stuck.outofscope:5: Stuck function: Lib.{_:2556}
LOG eval.stuck.outofscope:5: Stuck function: Lib.{_:2556}
LOG eval.stuck.outofscope:5: Stuck function: Lib.{_:2556}
LOG eval.stuck.outofscope:5: Stuck function: Lib.{_:2556}
LOG eval.stuck.outofscope:5: Stuck function: Lib.{_:2556}
LOG eval.stuck.outofscope:5: Stuck function: Lib.{_:2555}
LOG eval.stuck.outofscope:5: Stuck function: Lib.{_:2555}
LOG eval.stuck.outofscope:5: Stuck function: Lib.{_:2555}
LOG eval.stuck.outofscope:5: Stuck function: Lib.{a:2559}
LOG eval.stuck.outofscope:5: Stuck function: Lib.{_:2556}
LOG eval.stuck.outofscope:5: Stuck function: {_:2561}
LOG eval.stuck.outofscope:5: Stuck function: Lib.{a:2562}
LOG eval.stuck.outofscope:5: Stuck function: Lib.{_:2559}
LOG eval.stuck.outofscope:5: Stuck function: {_:2564}
LOG eval.stuck.outofscope:5: Stuck function: Lib.{a:2565}
LOG eval.stuck.outofscope:5: Stuck function: Lib.{a:2565}
LOG eval.stuck.outofscope:5: Stuck function: Lib.{a:2565}
LOG eval.stuck.outofscope:5: Stuck function: Lib.{_:2566}
LOG eval.stuck.outofscope:5: Stuck function: Lib.{_:2567}
LOG eval.stuck.outofscope:5: Stuck function: Lib.{_:2567}
LOG eval.stuck.outofscope:5: Stuck function: Lib.{_:2567}
LOG eval.stuck.outofscope:5: Stuck function: Lib.{_:2567}
LOG eval.stuck.outofscope:5: Stuck function: Lib.{_:2567}
LOG eval.stuck.outofscope:5: Stuck function: Lib.{_:2566}
LOG eval.stuck.outofscope:5: Stuck function: Lib.{_:2566}
LOG eval.stuck.outofscope:5: Stuck function: Lib.{_:2566}
LOG eval.stuck.outofscope:5: Stuck function: Lib.{a:2570}
LOG eval.stuck.outofscope:5: Stuck function: Lib.{a:2570}
LOG eval.stuck.outofscope:5: Stuck function: Lib.{a:2570}
LOG eval.stuck.outofscope:5: Stuck function: Lib.{a:2570}
LOG eval.stuck.outofscope:5: Stuck function: Lib.{a:2570}
LOG eval.stuck.outofscope:5: Stuck function: Lib.{_:2567}
LOG eval.stuck.outofscope:5: Stuck function: {_:2573}
LOG eval.stuck.outofscope:5: Stuck function: Lib.{b:2574}
LOG eval.stuck.outofscope:5: Stuck function: Lib.{a:2562}
LOG eval.stuck.outofscope:5: Stuck function: Lib.{a:2562}
LOG eval.stuck.outofscope:5: Stuck function: Lib.{_:2563}
LOG eval.stuck.outofscope:5: Stuck function: Lib.{_:2564}
LOG eval.stuck.outofscope:5: Stuck function: Lib.{_:2564}
LOG eval.stuck.outofscope:5: Stuck function: Lib.{_:2564}
LOG eval.stuck.outofscope:5: Stuck function: Lib.{_:2564}
LOG eval.stuck.outofscope:5: Stuck function: Lib.{_:2564}
LOG eval.stuck.outofscope:5: Stuck function: Lib.{_:2563}
LOG eval.stuck.outofscope:5: Stuck function: Lib.{_:2563}
LOG eval.stuck.outofscope:5: Stuck function: Lib.{_:2563}
LOG eval.stuck.outofscope:5: Stuck function: Lib.{a:2567}
LOG eval.stuck.outofscope:5: Stuck function: Lib.{a:2567}
LOG eval.stuck.outofscope:5: Stuck function: Lib.{a:2567}
LOG eval.stuck.outofscope:5: Stuck function: Lib.{a:2567}
LOG eval.stuck.outofscope:5: Stuck function: Lib.{a:2567}
LOG eval.stuck.outofscope:5: Stuck function: Lib.{_:2564}
LOG eval.stuck.outofscope:5: Stuck function: {_:2570}
LOG eval.stuck.outofscope:5: Stuck function: Lib.{b:2571}
LOG eval.stuck.outofscope:5: Stuck function: Lib.{a:2572}
LOG eval.stuck.outofscope:5: Stuck function: Lib.{a:2572}
LOG eval.stuck.outofscope:5: Stuck function: Lib.{a:2572}
LOG eval.stuck.outofscope:5: Stuck function: Lib.{a:2575}
LOG eval.stuck.outofscope:5: Stuck function: Lib.{a:2575}
LOG eval.stuck.outofscope:5: Stuck function: Lib.{a:2575}
LOG eval.stuck.outofscope:5: Stuck function: Lib.{a:2575}
LOG eval.stuck.outofscope:5: Stuck function: Lib.{a:2578}
LOG eval.stuck.outofscope:5: Stuck function: Lib.{a:2578}
LOG eval.stuck.outofscope:5: Stuck function: Lib.{a:2578}
LOG eval.stuck.outofscope:5: Stuck function: Lib.{a:2578}
LOG eval.stuck.outofscope:5: Stuck function: Prelude.Types.List.reverse
LOG eval.stuck.outofscope:5: Stuck function: Lib.{_:2593}
LOG eval.stuck.outofscope:5: Stuck function: Lib.{_:2594}
LOG eval.stuck.outofscope:5: Stuck function: Lib.{_:2594}
LOG eval.stuck.outofscope:5: Stuck function: Lib.{_:2594}
LOG eval.stuck.outofscope:5: Stuck function: Lib.{_:2594}
LOG eval.stuck.outofscope:5: Stuck function: Lib.{_:2594}
LOG eval.stuck.outofscope:5: Stuck function: Lib.{_:2594}
LOG eval.stuck.outofscope:5: Stuck function: Lib.{_:2594}
LOG eval.stuck.outofscope:5: Stuck function: {_:2597}
LOG eval.stuck.outofscope:5: Stuck function: Lib.{b:2598}
LOG eval.stuck.outofscope:5: Stuck function: Lib.{a:2599}
LOG eval.stuck.outofscope:5: Stuck function: Lib.{a:2599}
LOG eval.stuck.outofscope:5: Stuck function: Lib.{a:2599}
LOG eval.stuck.outofscope:5: Stuck function: Lib.{a:2601}
LOG eval.stuck.outofscope:5: Stuck function: Lib.{a:2601}
LOG eval.stuck.outofscope:5: Stuck function: Lib.{_:2590}
LOG eval.stuck.outofscope:5: Stuck function: Lib.{_:2591}
LOG eval.stuck.outofscope:5: Stuck function: Lib.{_:2591}
LOG eval.stuck.outofscope:5: Stuck function: Lib.{_:2591}
LOG eval.stuck.outofscope:5: Stuck function: Lib.{_:2591}
LOG eval.stuck.outofscope:5: Stuck function: Lib.{_:2591}
LOG eval.stuck.outofscope:5: Stuck function: Lib.{_:2591}
LOG eval.stuck.outofscope:5: Stuck function: Lib.{_:2591}
LOG eval.stuck.outofscope:5: Stuck function: {_:2594}
LOG eval.stuck.outofscope:5: Stuck function: Lib.{b:2595}
LOG eval.stuck.outofscope:5: Stuck function: Lib.{a:2596}
LOG eval.stuck.outofscope:5: Stuck function: Lib.{a:2596}
LOG eval.stuck.outofscope:5: Stuck function: Lib.{a:2596}
LOG eval.stuck.outofscope:5: Stuck function: Lib.{a:2598}
LOG eval.stuck.outofscope:5: Stuck function: Lib.{a:2598}
LOG eval.stuck.outofscope:5: Stuck function: Lib.accMapAux
2/2: Building Main (Main.idr)
LOG eval.stuck.outofscope:5: Stuck function: Main.{b:2603}
LOG eval.stuck.outofscope:5: Stuck function: Main.{b:2600}
LOG eval.stuck.outofscope:5: Stuck function: Main.{a:2601}
LOG eval.stuck.outofscope:5: Stuck function: Main.{a:2601}
LOG eval.stuck.outofscope:5: Stuck function: Main.{b:2600}
LOG eval.stuck.outofscope:5: Stuck function: Main.{b:2600}
LOG eval.stuck.outofscope:5: Stuck function: Main.{a:2601}
LOG eval.stuck.outofscope:5: Stuck function: Main.{a:2604}
LOG eval.stuck.outofscope:5: Stuck function: Main.{a:2604}
LOG eval.stuck.outofscope:5: Stuck function: Main.{b:2603}
LOG eval.stuck.outofscope:5: Stuck function: Main.{b:2603}
LOG eval.stuck.outofscope:5: Stuck function: Main.{a:2604}
LOG eval.stuck.outofscope:5: Stuck function: Main.{a:2601}
LOG eval.stuck.outofscope:5: Stuck function: Main.{a:2601}
LOG eval.stuck.outofscope:5: Stuck function: Main.{a:2607}
LOG eval.stuck.outofscope:5: Stuck function: Main.{a:2607}
LOG eval.stuck.outofscope:5: Stuck function: Main.{a:2607}
LOG eval.stuck.outofscope:5: Stuck function: Main.{a:2604}
LOG eval.stuck.outofscope:5: Stuck function: Main.{a:2604}
LOG eval.stuck.outofscope:5: Stuck function: Main.{a:2601}
LOG eval.stuck.outofscope:5: Stuck function: Main.{a:2601}
LOG eval.stuck.outofscope:5: Stuck function: Main.{a:2610}
LOG eval.stuck.outofscope:5: Stuck function: Main.{a:2610}
LOG eval.stuck.outofscope:5: Stuck function: Main.{a:2612}
LOG eval.stuck.outofscope:5: Stuck function: Main.{a:2610}
LOG eval.stuck.outofscope:5: Stuck function: Main.{a:2604}
LOG eval.stuck.outofscope:5: Stuck function: Main.{a:2604}
LOG eval.stuck.outofscope:5: Stuck function: Main.{a:2613}
LOG eval.stuck.outofscope:5: Stuck function: Main.{a:2613}
LOG eval.stuck.outofscope:5: Stuck function: Main.{a:2615}
LOG eval.stuck.outofscope:5: Stuck function: Main.{a:2613}
LOG eval.stuck.outofscope:5: Stuck function: Main.{a:2613}
LOG eval.stuck.outofscope:5: Stuck function: Main.{a:2604}
LOG eval.stuck.outofscope:5: Stuck function: Main.{a:2604}
LOG eval.stuck.outofscope:5: Stuck function: Main.{a:2604}
LOG eval.stuck.outofscope:5: Stuck function: Main.{ty:2624}
LOG eval.stuck.outofscope:5: Stuck function: Main.{a:2604}
LOG eval.stuck.outofscope:5: Stuck function: Main.{ty:2624}
LOG eval.stuck.outofscope:5: Stuck function: Main.{a:2604}
LOG eval.stuck.outofscope:5: Stuck function: Main.{a:2610}
LOG eval.stuck.outofscope:5: Stuck function: Main.{a:2601}
LOG eval.stuck.outofscope:5: Stuck function: Main.{a:2601}
LOG eval.stuck.outofscope:5: Stuck function: Main.{a:2601}
LOG eval.stuck.outofscope:5: Stuck function: Main.{ty:2621}
LOG eval.stuck.outofscope:5: Stuck function: Main.{a:2601}
LOG eval.stuck.outofscope:5: Stuck function: Main.{ty:2621}
LOG eval.stuck.outofscope:5: Stuck function: Main.{a:2601}
LOG eval.stuck.outofscope:5: Stuck function: Lib.accMap
Main> LOG eval.stuck:5: Stuck function: Lib.accMapAux
LOG eval.stuck:5: Stuck function: Lib.accMapAux

12
tests/idris2/spec001/expected
View File

@ -27,18 +27,18 @@ LOG specialise:5: Already specialised _PE.PE_fold_3a845f1ca594c582
LOG specialise:5: New RHS: (alg[0] (Prelude.Types.bimap (Builtin.Pair a[1] a[1]) (Builtin.Pair (Desc.Mu (Desc.Sum Desc.Stop (Desc.Prod Desc.Rec Desc.Rec))) (Desc.Mu (Desc.Sum Desc.Stop (Desc.Prod Desc.Rec Desc.Rec)))) Builtin.Unit Builtin.Unit (Prelude.Basics.id Builtin.Unit) \({arg:2} : (Builtin.Pair (Desc.Mu (Desc.Sum Desc.Stop (Desc.Prod Desc.Rec Desc.Rec))) (Desc.Mu (Desc.Sum Desc.Stop (Desc.Prod Desc.Rec Desc.Rec))))) => (Prelude.Types.bimap a[2] (Desc.Mu (Desc.Sum Desc.Stop (Desc.Prod Desc.Rec Desc.Rec))) a[2] (Desc.Mu (Desc.Sum Desc.Stop (Desc.Prod Desc.Rec Desc.Rec))) (_PE.PE_fold_3a845f1ca594c582 a[2] alg[1]) (_PE.PE_fold_3a845f1ca594c582 a[2] alg[1]) {arg:2}[0]) t[2]))
LOG specialise:5: Already specialised _PE.PE_fold_3a845f1ca594c582
1/1: Building Desc2 (Desc2.idr)
LOG specialise.declare:5: Specialising Main.fold ($resolved2668) -> _PE.PE_fold_8abb50b713fe8e5e by (0, Static Prelude.Types.Nat), (1, Static Prelude.Basics.List), (2, Static (Prelude.Interfaces.MkFunctor Prelude.Basics.List \{0 b : Type} => \{0 a : Type} => \(func : ({arg:8738} : a[0]) -> b[2]) => \({arg:8743} : (Prelude.Basics.List a[1])) => (Prelude.Types.List.mapImpl b[3] a[2] func[1] {arg:8743}[0]))), (3, Dynamic)
LOG specialise.declare:5: Specialising Main.fold ($resolved2668) -> _PE.PE_fold_8abb50b713fe8e5e by (0, Static Prelude.Types.Nat), (1, Static Prelude.Basics.List), (2, Static (Prelude.Interfaces.MkFunctor Prelude.Basics.List \{0 b : Type} => \{0 a : Type} => \(func : ({arg:8742} : a[0]) -> b[2]) => \({arg:8747} : (Prelude.Basics.List a[1])) => (Prelude.Types.List.mapImpl b[3] a[2] func[1] {arg:8747}[0]))), (3, Dynamic)
LOG specialise:3: Specialised type _PE.PE_fold_8abb50b713fe8e5e: ({arg:840} : ({arg:842} : (Prelude.Basics.List Prelude.Types.Nat)) -> Prelude.Types.Nat) -> ({arg:847} : (Main.Mu Prelude.Basics.List)) -> Prelude.Types.Nat
LOG specialise:5: Attempting to specialise:
(((((Main.fold [a = a]) [f = f]) [fun = fun]) alg) ((Main.MkMu [f = f]) t)) = (alg ((((((Prelude.Interfaces.(<$>) [b = a]) [a = (Main.Mu f)]) [f = f]) [{conArg:8792} = fun]) ((((Main.fold [a = a]) [f = f]) [fun = fun]) alg)) t))
(((((Main.fold [a = a]) [f = f]) [fun = fun]) alg) ((Main.MkMu [f = f]) t)) = (alg ((((((Prelude.Interfaces.(<$>) [b = a]) [a = (Main.Mu f)]) [f = f]) [{conArg:8796} = fun]) ((((Main.fold [a = a]) [f = f]) [fun = fun]) alg)) t))
LOG specialise:5: New patterns for _PE.PE_fold_8abb50b713fe8e5e:
((_PE.PE_fold_8abb50b713fe8e5e alg) ((Main.MkMu [f = Prelude.Basics.List]) t)) = (alg ((((((Prelude.Interfaces.(<$>) [b = Prelude.Types.Nat]) [a = (Main.Mu Prelude.Basics.List)]) [f = Prelude.Basics.List]) [{conArg:8792} = ((Prelude.Interfaces.MkFunctor [f = Prelude.Basics.List]) (%lam Rig0 Implicit (Just b) %type (%lam Rig0 Implicit (Just a) %type (%lam RigW Explicit (Just func) (%pi RigW Explicit (Just {arg:8738}) a b) (%lam RigW Explicit (Just {arg:8743}) (Prelude.Basics.List a) ((((Prelude.Types.List.mapImpl [b = b]) [a = a]) func) {arg:8743}))))))]) ((((Main.fold [a = Prelude.Types.Nat]) [f = Prelude.Basics.List]) [fun = ((Prelude.Interfaces.MkFunctor [f = Prelude.Basics.List]) (%lam Rig0 Implicit (Just b) %type (%lam Rig0 Implicit (Just a) %type (%lam RigW Explicit (Just func) (%pi RigW Explicit (Just {arg:8738}) a b) (%lam RigW Explicit (Just {arg:8743}) (Prelude.Basics.List a) ((((Prelude.Types.List.mapImpl [b = b]) [a = a]) func) {arg:8743}))))))]) alg)) t))
LOG specialise.declare:5: Specialising Main.fold ($resolved2668) -> _PE.PE_fold_a727631bc09e3761 by (0, Static Prelude.Types.Nat), (1, Static Prelude.Basics.List), (2, Static (Prelude.Interfaces.MkFunctor Prelude.Basics.List \{0 b : Type} => \{0 a : Type} => \(func : ({arg:8738} : a[0]) -> b[2]) => \({arg:8743} : (Prelude.Basics.List a[1])) => (Prelude.Types.List.mapAppend a[2] b[3] (Prelude.Basics.Lin b[3]) func[1] {arg:8743}[0]))), (3, Dynamic)
((_PE.PE_fold_8abb50b713fe8e5e alg) ((Main.MkMu [f = Prelude.Basics.List]) t)) = (alg ((((((Prelude.Interfaces.(<$>) [b = Prelude.Types.Nat]) [a = (Main.Mu Prelude.Basics.List)]) [f = Prelude.Basics.List]) [{conArg:8796} = ((Prelude.Interfaces.MkFunctor [f = Prelude.Basics.List]) (%lam Rig0 Implicit (Just b) %type (%lam Rig0 Implicit (Just a) %type (%lam RigW Explicit (Just func) (%pi RigW Explicit (Just {arg:8742}) a b) (%lam RigW Explicit (Just {arg:8747}) (Prelude.Basics.List a) ((((Prelude.Types.List.mapImpl [b = b]) [a = a]) func) {arg:8747}))))))]) ((((Main.fold [a = Prelude.Types.Nat]) [f = Prelude.Basics.List]) [fun = ((Prelude.Interfaces.MkFunctor [f = Prelude.Basics.List]) (%lam Rig0 Implicit (Just b) %type (%lam Rig0 Implicit (Just a) %type (%lam RigW Explicit (Just func) (%pi RigW Explicit (Just {arg:8742}) a b) (%lam RigW Explicit (Just {arg:8747}) (Prelude.Basics.List a) ((((Prelude.Types.List.mapImpl [b = b]) [a = a]) func) {arg:8747}))))))]) alg)) t))
LOG specialise.declare:5: Specialising Main.fold ($resolved2668) -> _PE.PE_fold_a727631bc09e3761 by (0, Static Prelude.Types.Nat), (1, Static Prelude.Basics.List), (2, Static (Prelude.Interfaces.MkFunctor Prelude.Basics.List \{0 b : Type} => \{0 a : Type} => \(func : ({arg:8742} : a[0]) -> b[2]) => \({arg:8747} : (Prelude.Basics.List a[1])) => (Prelude.Types.List.mapAppend a[2] b[3] (Prelude.Basics.Lin b[3]) func[1] {arg:8747}[0]))), (3, Dynamic)
LOG specialise:3: Specialised type _PE.PE_fold_a727631bc09e3761: ({arg:840} : ({arg:842} : (Prelude.Basics.List Prelude.Types.Nat)) -> Prelude.Types.Nat) -> ({arg:847} : (Main.Mu Prelude.Basics.List)) -> Prelude.Types.Nat
LOG specialise:5: Attempting to specialise:
(((((Main.fold [a = a]) [f = f]) [fun = fun]) alg) ((Main.MkMu [f = f]) t)) = (alg ((((((Prelude.Interfaces.(<$>) [b = a]) [a = (Main.Mu f)]) [f = f]) [{conArg:8792} = fun]) ((((Main.fold [a = a]) [f = f]) [fun = fun]) alg)) t))
(((((Main.fold [a = a]) [f = f]) [fun = fun]) alg) ((Main.MkMu [f = f]) t)) = (alg ((((((Prelude.Interfaces.(<$>) [b = a]) [a = (Main.Mu f)]) [f = f]) [{conArg:8796} = fun]) ((((Main.fold [a = a]) [f = f]) [fun = fun]) alg)) t))
LOG specialise:5: New patterns for _PE.PE_fold_a727631bc09e3761:
((_PE.PE_fold_a727631bc09e3761 alg) ((Main.MkMu [f = Prelude.Basics.List]) t)) = (alg ((((((Prelude.Interfaces.(<$>) [b = Prelude.Types.Nat]) [a = (Main.Mu Prelude.Basics.List)]) [f = Prelude.Basics.List]) [{conArg:8792} = ((Prelude.Interfaces.MkFunctor [f = Prelude.Basics.List]) (%lam Rig0 Implicit (Just b) %type (%lam Rig0 Implicit (Just a) %type (%lam RigW Explicit (Just func) (%pi RigW Explicit (Just {arg:8738}) a b) (%lam RigW Explicit (Just {arg:8743}) (Prelude.Basics.List a) (((((Prelude.Types.List.mapAppend [a = a]) [b = b]) (Prelude.Basics.Lin [a = b])) func) {arg:8743}))))))]) ((((Main.fold [a = Prelude.Types.Nat]) [f = Prelude.Basics.List]) [fun = ((Prelude.Interfaces.MkFunctor [f = Prelude.Basics.List]) (%lam Rig0 Implicit (Just b) %type (%lam Rig0 Implicit (Just a) %type (%lam RigW Explicit (Just func) (%pi RigW Explicit (Just {arg:8738}) a b) (%lam RigW Explicit (Just {arg:8743}) (Prelude.Basics.List a) (((((Prelude.Types.List.mapAppend [a = a]) [b = b]) (Prelude.Basics.Lin [a = b])) func) {arg:8743}))))))]) alg)) t))
((_PE.PE_fold_a727631bc09e3761 alg) ((Main.MkMu [f = Prelude.Basics.List]) t)) = (alg ((((((Prelude.Interfaces.(<$>) [b = Prelude.Types.Nat]) [a = (Main.Mu Prelude.Basics.List)]) [f = Prelude.Basics.List]) [{conArg:8796} = ((Prelude.Interfaces.MkFunctor [f = Prelude.Basics.List]) (%lam Rig0 Implicit (Just b) %type (%lam Rig0 Implicit (Just a) %type (%lam RigW Explicit (Just func) (%pi RigW Explicit (Just {arg:8742}) a b) (%lam RigW Explicit (Just {arg:8747}) (Prelude.Basics.List a) (((((Prelude.Types.List.mapAppend [a = a]) [b = b]) (Prelude.Basics.Lin [a = b])) func) {arg:8747}))))))]) ((((Main.fold [a = Prelude.Types.Nat]) [f = Prelude.Basics.List]) [fun = ((Prelude.Interfaces.MkFunctor [f = Prelude.Basics.List]) (%lam Rig0 Implicit (Just b) %type (%lam Rig0 Implicit (Just a) %type (%lam RigW Explicit (Just func) (%pi RigW Explicit (Just {arg:8742}) a b) (%lam RigW Explicit (Just {arg:8747}) (Prelude.Basics.List a) (((((Prelude.Types.List.mapAppend [a = a]) [b = b]) (Prelude.Basics.Lin [a = b])) func) {arg:8747}))))))]) alg)) t))
LOG specialise:5: Already specialised _PE.PE_fold_a727631bc09e3761
LOG specialise:5: New RHS: (alg[0] (Prelude.Types.List.mapAppend (Main.Mu Prelude.Basics.List) Prelude.Types.Nat (Prelude.Basics.Lin Prelude.Types.Nat) (_PE.PE_fold_a727631bc09e3761 alg[0]) t[1]))
LOG specialise:5: Already specialised _PE.PE_fold_a727631bc09e3761

4
tests/idris2/with010/NestedWith.idr
View File

@ -8,5 +8,5 @@ interface DecEq a where
(DecEq a, DecEq b) => DecEq (a, b) where
decEq (x, y) (a, b) with (decEq x a) | (decEq y b)
_ | Yes eqL | Yes eqR = Yes (cong2 (,) eqL eqR)
_ | No neqL | _ = No (neqL . cong fst)
_ | _ | No neqR = No (neqR . cong snd)
_ | No neqL | _ = No $ \prf => neqL $ cong fst prf
_ | _ | No neqR = No $ \prf => neqR $ cong snd prf