ulfnorell/agda-prelude

Programming library for Agda

agda-prelude's Issues

Cannot type check Prelude.Applicative

Freshly cloned today:

/home/ollie/work/agda-prelude/src/Prelude/Applicative.agda:21,12-13
Not in scope:
  ⦇
  at /home/ollie/work/agda-prelude/src/Prelude/Applicative.agda:21,12-13
when scope checking ⦇

The line is

  a <* b = ⦇ const a b ⦈

I'm on Agda 2.5.1.1

Fails to build with Agda 2.6.4

/build/source/src/Prelude/Nat.agda:10,1-24
Failed to solve the following constraints:
  Resolve instance argument _r_639 : Ord/Laws _A_638
  Candidates
    OrdA : (Ord/Laws A)
    OrdLawsBool : (Ord/Laws Bool)
    (stuck)
  Resolve instance argument _OrdA_621 : Ord/Laws _A_620
  Candidates
    OrdA : Ord/Laws A
    OrdLawsBool : Ord/Laws Bool
    (stuck)
  Resolve instance argument _r_605 : Ord _A_604
  Candidates
    overlap Ord/Laws.super OrdA : Ord A
    OrdBool : Ord Bool
    (stuck)
  Resolve instance argument _OrdA_645 : Ord/Laws _A_644
  Candidates
    OrdA : Ord/Laws A
    OrdLawsBool : Ord/Laws Bool
    (stuck)
  b < a =< _y_647 < _x_646 (blocked on _OrdA_645)
  a < b =< _x_646 < _y_647 (blocked on _OrdA_645)
  b < b =< _x_640 < _x_640 (blocked on _r_639)
  b < a =< _y_623 < _x_622 (blocked on _OrdA_621)
  a ≤ b =< _x_622 ≤ _y_623 (blocked on _OrdA_621)
  _x_606 ≤ _y_607 =< a ≤ b (blocked on _r_605)
  a < b =< _x_606 < _y_607 (blocked on _r_605)
when scope checking the declaration
  open import Prelude.Ord
/build/source/src/Prelude/Nat.agda:10,1-24
Unsolved metas at the following locations:
  /build/source/src/Prelude/Ord.agda:242,24-33
  /build/source/src/Prelude/Ord.agda:242,34-37
  /build/source/src/Prelude/Ord.agda:242,24-37
  /build/source/src/Prelude/Ord.agda:244,32-48
  /build/source/src/Prelude/Ord.agda:244,49-50
  /build/source/src/Prelude/Ord.agda:244,51-54
  /build/source/src/Prelude/Ord.agda:250,35-48
  /build/source/src/Prelude/Ord.agda:251,32-44
  /build/source/src/Prelude/Ord.agda:251,45-46
  /build/source/src/Prelude/Ord.agda:251,47-50
when scope checking the declaration
  open import Prelude.Ord

This might be related to the following entry in the changelog:

[Breaking] The algorithm for resolution of instance arguments has been simplified. It will now only rely on the type of instances to determine which candidate it should use, and no longer on their values.

Generalise Tactic.Nat to work with other libraries

Currently, the tactics in Tactic.Nat work well with agda-prelude but not the standard library. For example,

  open import Tactic.Nat

  module Prelude where
    open import Prelude

    test-by : {a b : Nat} → suc a ≤ b → a ≤ suc b
    test-by a₊₁≤b = by a₊₁≤b -- this works

  module StandardLibrary where
    open import Data.Nat

    test-by : {a b : ℕ} → suc a ≤ b → a ≤ suc b
    test-by a₊₁≤b = by a₊₁≤b -- this doesn't

I have started to generalise Tactic.Nat here, but there is a roadblock due to agda/agda#1363. In effect, this test of Tactic.Nat.Subtract.By fails.

UPDATE: I'll look for a workaround to agda/agda#1363 by moving test calls to the macros outside of the parameterized module.

UPDATE UPDATE: I realise now that a better approach is to create an adapter for Tactic.Nat rather than trying to generalise it. I'm developing that now.

Deriving Eq for reflection syntax extremely slow

Below is the code for deriving Eq on the reflected syntax. It's working, but it's extremely slow. I'm not sure if it is due to Agda or the implementation of derivingEq though.

open import Prelude
open import Data.List
open import Builtin.Reflection
open import Tactic.Deriving.Eq

unquoteDecl eqAny = derivingEq (quote Any) eqAny
instance 
  EqAny : ∀ {a b} {A : Set a} {B : A → Set b} {l : List A} → 
          {{_ : Eq A}} {{_ : ∀ {x} → Eq (B x)}} → Eq (Any B l)
  EqAny = record { _==_ = eqAny }

unquoteDecl eq≡ = derivingEq (quote _≡_) eq≡

unquoteDecl eqVisibility = derivingEq (quote Visibility) eqVisibility

instance
  EqVisibility : Eq Visibility
  EqVisibility = record { _==_ = eqVisibility }

unquoteDecl eqRelevance = derivingEq (quote Relevance) eqRelevance

instance
  EqRelevance : Eq Relevance
  EqRelevance = record { _==_ = eqRelevance }

instance
  Eq≡ : ∀ {a} {A : Set a} {x y : A} {{_ : Eq A}} → Eq (x ≡ y)
  Eq≡ = record { _==_ = eq≡ }

unquoteDecl eqArgInfo = derivingEq (quote ArgInfo) eqArgInfo

instance
  EqArgInfo : Eq ArgInfo
  EqArgInfo = record { _==_ = eqArgInfo }

unquoteDecl eqArg = derivingEq (quote Arg) eqArg

instance
  EqArg : ∀ {A : Set} → {{_ : Eq A}} → Eq (Arg A)
  EqArg = record { _==_ = eqArg }

unquoteDecl eqAbs = derivingEq (quote Abs) eqAbs

instance
  EqAbs : ∀ {A : Set} → {{_ : Eq A}} → Eq (Abs A)
  EqAbs = record { _==_ = eqAbs }

unquoteDecl eqLiteral = derivingEq (quote Literal) eqLiteral

instance
  EqLiteral : Eq Literal
  EqLiteral = record { _==_ = eqLiteral }

{-# TERMINATING #-}
eqSort : (s₁ s₂ : Sort) → Dec (s₁ ≡ s₂)
eqType : (ty₁ ty₂ : Type) → Dec (ty₁ ≡ ty₂)
eqTerm : (t₁ t₂ : Term) → Dec (t₁ ≡ t₂)
eqPattern : (p₁ p₂ : Pattern) → Dec (p₁ ≡ p₂)
eqClause : (c₁ c₂ : Clause) → Dec (c₁ ≡ c₂)

instance
  EqSort : Eq Sort
  EqSort = record { _==_ = eqSort }

  EqType : Eq Type
  EqType = record { _==_ = eqType }

  EqTerm : Eq Term
  EqTerm = record { _==_ = eqTerm }

  EqPattern : Eq Pattern
  EqPattern = record { _==_ = eqPattern }

  EqClause : Eq Clause
  EqClause = record { _==_ = eqClause }

unquoteDef eqSort = deriveEqDef (quote Sort) (quote eqSort)
unquoteDef eqType = deriveEqDef (quote Type) (quote eqType)
unquoteDef eqTerm = deriveEqDef (quote Term) (quote eqTerm)
unquoteDef eqPattern = deriveEqDef (quote Pattern) (quote eqPattern)
unquoteDef eqClause = deriveEqDef (quote Clause) (quote eqClause)

Indexed monads?

@UlfNorell would you be interested in a PR that generalizes monads to indexed monads (and similarly for applicative functors)? I recently wrote some code for them that shouldn't be hard to adapt to the style of the Prelude.

Need help with List

Hello,

I could not compile this code. Can anyone help?

module test1 where

open import Prelude

main : IO ⊤
main = let list : List String
           list = [ "0" , "1" ]
       in case index list 0 of λ where
            nothing  -> putStrLn "nothing"
            (just x) -> putStrLn x

output:

test1.agda:7,21-30
Σ _A_6 _B_7 !=< String
when checking that the inferred type of an application
  Σ _A_6 _B_7
matches the expected type
  String

Support for JS backend

The library does not support the JS backend, this would be a matter of having a few COMPILED_JS pragmas.

I might want to give it a try, but only if there is hope for it to be merged.

Latest agda breaks Prelude.Fin due to Irrelevance.

Typechecking Prelude.Fin does not work for latest agda. I hope this to be resolved as soon as @jespercockx finalizes his changes.

The Container module

Hello I'm working with adding some properties and functions on lists. Currently all properties of Lists are located in Container/List/ are there any specific reason why those are located there? If not may I change the location to Prelude/List/?

Builtin.Float doesn't typecheck

Agda is complaining that primFloatLess is not in scope when typechecking Builtin.Float.

inv-suc-monotone

inv-suc-monotone : ∀{t v} → suc t < suc v → t < v
inv-suc-monotone (diff! k) = diff k (add-suc-r k _) 

https://github.com/UlfNorell/agda-prelude/blob/master/src/Prelude/Nat.agda#L128

reright fails in a universe-polymorphic case

This simple use of reright fails b/c I recognise only A as the dependency of x≡y, ignoring the fact that A itself depends on a. I'm assigning this to myself, of course.

fails : ∀ (a : Level) (A : Set a) (x y : A) (x≡y : x ≡ y) → Set
fails a A x y x≡y = reright x≡y {!!}

Possible code merge

Hello,

I've found myself preferring to use agda-prelude as the basis library for my hobby projects, but since it is missing a lot of proofs I started writing my own extension library. I though it may be of interest to integrate some of the things I've written here into the main library. (https://gitlab.com/tmore/agda-prelude-extras/-/tree/master/src/Prelude/Extras)

I would probably have done so if there where any general guidlines on naming conventions and location of properties.
Would it be of interest if i merged some of the things from my library into the main one? And if so how would you prefer the directory structure and naming convention?

Need help with do notation

I could not compile this code. Can anyone help?

module test1 where

open import Prelude

main : IO ⊤
main = if true
            then do
                putStrLn "True"
                putStrLn "not False"
            else do
                putStrLn "False"
                putStrLn "not True"

error:

/mnt/Archive/Documents/Agda/test1.agda:10,13-13
/mnt/Archive/Documents/Agda/test1.agda:10,13: Parse error
else<ERROR>
 do
                putStrLn "...

Not able to use it

cd agda-prelude/agda-ffi ?? No such directory

Error when importing Vec

When importing Vec, I get the following error:

/Users/v/vic/dev/agda/agda-prelude/src/Prelude/Vec.agda:125,3-86
Repeated variables in pattern: y
when scope checking the left-hand side
less-trans {{OrdLawsVec {A = A}}} {x ∷ xs} {y ∷ ys} {y ∷ zs}
(head< lt) (tail< lt₁)
in the definition of OrdLawsVec

Using Agda version 2.5.3-e3f5983-dirty.

Triggers internal agda error.

agda/agda#3805

inferFunRange failing

Why does inferFunRange fail in the code below? I expected Agda to report "inferFunRange succeeded (x : A) → F x → Set".

open import Prelude
open import Tactic.Reflection

macro
  test-inferFunRange : Tactic
  test-inferFunRange hole = do
    goal ← inferFunRange hole -|
    typeError ( strErr "inferFunRange succeeded" ∷ termErr goal ∷ [] )

bar : Nat
bar = 0

record R (A : Set) : Set₁ where
  field
    F : A → Set

  foo : (x : A) → F x → Set
  foo = case bar of (λ _ → test-inferFunRange {!!})
  {- Error:
       A → Set !=< Set of type Set₁
       when checking that the expression F has type Set
  -}

Generalized collection / sequence etc functions.

There's a similar issue on the topic for a few years earlier, but I really believe it would be a good idea to have generalized names for common container / sequence / etc operations.

The main purpose of such type classes would to make programming easier, not formalisms.

Two examples classes:

"Sized" giving a general notion of the size of some object

record Sized {a} (A : Set a) : Set a where
  field
    size : A → Nat
open Sized {{...}} public

instance
  SizedNat : Sized Nat
  size {{SizedNat}} n = n

  SizedList : Sized (List A)
  size {{SizedList}} = length

"Collection" generalizing the concept of a multi-set. (Excluding extensionality of course)

record Collection {a b} (A : Set a) (C : Set b) : Set (a ⊔ b) where
  field
    insert : A → C → C
    remove : A → C → C
    removeOne : A → C → C
    member : A → C → Bool
    occurences : A → C → Nat
open Collection {{...}} public

record Collection/Laws {a b} (A : Set a) (C : Set b) : Set (a ⊔ b) where
  field
    overlap {{super}} : Collection A C
    insert-member : (a : A) → (c : C) → member a (insert a c) ≡ true
    insert-remove : (a : A) → (c : C) → member a (remove a c) ≡ false
    remove-local : (a a' : A) → (c : C) → a' ≢ a
                 → member a' (remove a c) ≡ member a' c
    insert-local : (a a' : A) → (c : C) → (a' ≢ a)
                 → member a' (insert a c) ≡ member a' c

instance
  CollectionList : {{_ : Eq A}} → Collection A (List A)
  insert {{CollectionList}} = _∷_
  remove {{CollectionList}} a = List.filter (λ x → not (x ==? a))
  removeOne {{CollectionList}} a List.[] = List.[]
  removeOne {{CollectionList}} a (x ∷ xs) =
    if x ==? a then xs else x ∷ removeOne a xs
  member {{CollectionList}} = List.elem
  occurences {{CollectionList}} x xs = List.length (List.filter (_==? x) xs)


  CollectionString : Collection Char String
  insert {{CollectionString}} c str =
    packString (List.singleton c) <> str
  remove {{CollectionString}} c str = packString (remove c (unpackString str))
  removeOne {{CollectionString}} c str =  packString (removeOne c (unpackString str))
  member {{CollectionString}} c str = member c (unpackString str)
  occurences {{CollectionString}} c str = occurences c (unpackString str)

Support agda 2.6.2 and standard-library 1.7

Currently there is an error like:

/build/source/src/Builtin/Reflection.agda:112,39-40
Modality !=< Relevance
when checking that the expression r has type Relevance

See:

• NixOS/nixpkgs#130424 (comment)
• https://hydra.nixos.org/build/148413831/nixlog/1/tail

modules using Tactic.Nat are failing

I forgot to re-run the tests before issuing PR #31, so... stuff like Numeric.Nat.Modulo is failing. I need either change

open import Tactic.Nat

to

open import Tactic.Nat (quote _≤_) (quote id) (quote id)

or perhaps create a Tactic.Nat.Prelude so that we can simply say

open import Tactic.Nat.Prelude

Please tag releases

For packaging purposes, it would be great if there was some kind of tagging going on. Recently this no longer works with 2.4.2 (Parse error TERMINATING<ERROR> #-} showNat′ : Nat → List C...) so it'd be great if there was some way to match up commits with ‘what version of Agda should work here?’.

does not compile with Agda 2.6.0

This is the error I get:

agda-prelude/src/Numeric/Nat/Pow.agda:71,16-23 Invalid goal: ((_ Semiring.* a ^ (q +N q)) ((_ Semiring.* a) a) ≡ (_ Semiring.* a ^ (q *N 2)) ((_ Semiring.* a) a)) when checking that the expression unquote auto has type a ^ (q + q) * (a * a) ≡ a ^ (q * 2) * (a * a)

How could one fix it?

Error with Agda 2.6.1

An error from Prelude/List.agda.

.../agda-prelude/src/Prelude/List.agda:218,24-25
Variable generalization failed.
  - Probable cause
      There were unsolved constraints that obscured the dependencies
      between the generalized variables.
  - Suggestion
      The most reliable solution is to provide enough information to make
      the dependencies clear, but simply mentioning the variables in the
      right order should also work.
  - Further information
    - Dependency analysis suggested this (likely incorrect) order:
        A ℓ x y xs ys
    - After constraint solving it looks like A actually depends on ℓ
    - The dependency I error is
      .../agda-prelude/src/Prelude/List.agda:218,24-25
      Cannot instantiate the metavariable _855 to solution ℓ
      since it contains the variable genTel
      which is not in scope of the metavariable
when checking that the expression
{_<_ = _<₁_ : A → A → Set ℓ} →
Comparison _<₁_ x y →
Comparison (LessList _<₁_) xs ys →
Comparison (LessList _<₁_) (x ∷ xs) (y ∷ ys)
has type _821

Error when using derivingEq with implicit constructor argument

Minimal test case:

open import Prelude
open import Tactic.Deriving.Eq

data Test : Set where
  test : {x : Nat} → Vec Nat x → Test

unquoteDecl testEq = derivingEq (quote Test) testEq

Error message:

.x₁ != .x of type Nat
when checking that the expression x₁ has type Vec Nat .x

Explicit parameter-like argument is ignored by derivingEq

Minimal test case:

open import Prelude
open import Tactic.Deriving.Eq

data Test : Nat → Set where
   test : (x : Nat) → Test x

unquoteDecl testEq = derivingEq (quote Test) testEq

Error message:

The constructor test expects 1 arguments (including hidden ones),
but has been given 0 (including hidden ones)
when checking that the pattern test has type Test n

is there a 2.5.2 release?

or not?

Applicative doesn't type check

Not in scope:
⦇
at /Users/jeremybi/Projects/agda-prelude/src/Prelude/Applicative.agda:21,12-13
when scope checking ⦇
make: *** [compile-main] Error 1

Change name of mempty to mId.

The record definition of monoid has the name of mempty for the id.

It was probably copied from haskell.
https://wiki.haskell.org/Monoid

The better name is "mId" or something similar that would reflect that it is an id.

reright may fail when called from inside a parameterised module

reright fails when called from within a parameterised module that references types that depend on those parameters. I've traced the reason to agda/agda#1890.

  open import Prelude
  open import Tactic.Reflection.Reright

  module _ (l : Level) where
    postulate P : Set

    test : (p : P)
             (A : Set)
             (x y : A)
             (x≡y : x ≡ y)
             → Set
    test _ _ _ _ x≡y = reright x≡y ?

Can't load Tactic.Nat.Reflect

because "lift" is not in scope.

PS. I'm using the development version of Agda.

Failed to import Prelude

I failed to import Prelude with this error. Can anyone help?

module test where

open import Prelude

main : IO ⊤
main = do
    putStrLn "Hi"
    putStrLn "Hello"

error:

Failed to find source of module Agda.Builtin.Maybe in any of the
following locations:
  /mnt/Archive/Documents/Agda/test/Agda/Builtin/Maybe.agda
  /mnt/Archive/Documents/Agda/test/Agda/Builtin/Maybe.lagda
  /home/notooth/agda-stdlib-1.4/src/Agda/Builtin/Maybe.agda
  /home/notooth/agda-stdlib-1.4/src/Agda/Builtin/Maybe.lagda
  /home/notooth/.cabal/store/ghc-8.8.4/Agda-2.6.1.2-736f5763c1ca9cad98da5a6573a324d3abce161397486492e1d8dfc976da26c5/share/lib/prim/Agda/Builtin/Maybe.agda
  /home/notooth/.cabal/store/ghc-8.8.4/Agda-2.6.1.2-736f5763c1ca9cad98da5a6573a324d3abce161397486492e1d8dfc976da26c5/share/lib/prim/Agda/Builtin/Maybe.lagda
when scope checking the declaration
  open import Agda.Builtin.Maybe public

Update tests

All the tests should be checked and possibly updated. At least test/DeriveEqTest.agda does not work anymore.

P.s. I'm making changes to some utilities like Tactic.Reflection.Free, so it would be nice to know that I'm not breaking something.

String manipulation functions / generalize list functions?

I am currently writing code involving quite a lot of String manipulation, and currently agda-prelude doesn't offer much functionality for plain Strings yet. I can go via List Char, but that will definitely be slower and feels overly complicated just to e.g. split a string.

The question then is how these functions should be added. Should the existing functions in Data.List be generalized and moved to Container.Foldable? What about functions which don't find into any existing class like a monomorphic functor for strings? What about sequence-like methods?

The other option would be to have multiple distinct specialized functions. However, if we use the same
names we have to put them in a separate modules as both Prelude.String and Prelude.List are imported in Prelude. One could also add some kind of prefix to the functions, eg "s" for all String
specializations to get sLength, sDrop etc..

My preference would be to generalize the functions. This would unify the functions for all types
and one doesn't need qualified imports for all the containers data types. The main drawback
is that it complicates the types and it could make type inference harder.

Any thoughts?

Container.Foldable candidates:

• length
• null
• elem
• sum
• product
• maximum
• minimum
• any
• all

Sequence-like methods:

• take
• drop
• filter
• isPrefixOf

Substitution in Tactic.Reflection.Subtitute is buggy

Consider this code :

open import Agda.Builtin.Reflection
open import Reflection
open import Prelude.Nat
open import Prelude.Bool
open import Prelude.Unit
open import Prelude.List
open import Tactic.Reflection.Substitute

fff : Term
fff = pat-lam [ clause (   arg (arg-info visible relevant) (var "a")
                        ∷ (arg (arg-info visible relevant) (var "b"))
                        ∷ []) (var 0 [ arg (arg-info visible relevant) (var 2 []) ]) ] []

ggg : Term
ggg = substTerm (safe (def (quote Nat) []) _ ∷ []) fff

postulate
  B : Term → Set

aaa : B ggg
aaa = {!!}

Inspecting the hole with normalization gives this output :

Goal: B
      (pat-lam
       [
       clause (vArg (var "a") ∷ [ vArg (var "b") ])
       (var 1 [ vArg (def (quote Nat) []) ])
       ]
       [])

There seem to be at least two errors in the algorithm :
a. https://github.com/UlfNorell/agda-prelude/blob/master/src/Tactic/Reflection/Substitute.agda#L79
b. https://github.com/UlfNorell/agda-prelude/blob/master/src/Tactic/Reflection/Substitute.agda#L101

The example shows the "b" error. You should not use reverse.

what branch for 2.5.3? :)