ulfnorell / agda-prelude Goto Github PK
View Code? Open in Web Editor NEWProgramming library for Agda
License: MIT License
Programming library for Agda
License: MIT License
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?
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 {!!}
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/?
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
-}
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.
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
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)
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
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
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?’.
@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.
Not in scope:
⦇
at /Users/jeremybi/Projects/agda-prelude/src/Prelude/Applicative.agda:21,12-13
when scope checking ⦇
make: *** [compile-main] Error 1
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?
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
.
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.
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 ?
Typechecking Prelude.Fin does not work for latest agda. I hope this to be resolved as soon as @jespercockx finalizes his changes.
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
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
I am currently writing code involving quite a lot of String
manipulation, and currently agda-prelude doesn't offer much functionality for plain String
s 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:
Sequence-like methods:
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
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
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.
Agda is complaining that primFloatLess
is not in scope when typechecking Builtin.Float.
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.
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.
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 "...
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:
because "lift" is not in scope.
PS. I'm using the development version of Agda.
or not?
cd agda-prelude/agda-ffi ?? No such directory
/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.
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
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)
A declarative, efficient, and flexible JavaScript library for building user interfaces.
🖖 Vue.js is a progressive, incrementally-adoptable JavaScript framework for building UI on the web.
TypeScript is a superset of JavaScript that compiles to clean JavaScript output.
An Open Source Machine Learning Framework for Everyone
The Web framework for perfectionists with deadlines.
A PHP framework for web artisans
Bring data to life with SVG, Canvas and HTML. 📊📈🎉
JavaScript (JS) is a lightweight interpreted programming language with first-class functions.
Some thing interesting about web. New door for the world.
A server is a program made to process requests and deliver data to clients.
Machine learning is a way of modeling and interpreting data that allows a piece of software to respond intelligently.
Some thing interesting about visualization, use data art
Some thing interesting about game, make everyone happy.
We are working to build community through open source technology. NB: members must have two-factor auth.
Open source projects and samples from Microsoft.
Google ❤️ Open Source for everyone.
Alibaba Open Source for everyone
Data-Driven Documents codes.
China tencent open source team.