Giter Club home page Giter Club logo

agda-test's People

Watchers

avatar avatar

agda-test's Issues

How much shadowing should be allowed?

From [email protected] on November 29, 2007 23:51:40

I am quite fond of shadowing when writing programs. I think it is a good safety feature. Often
you might do an intermediate computation which makes an earlier argument x meaningless and
it is a good thing that you can no longer refer to it, having to a more local similar thing a name
like x' just increases the change of a silly mistake. This practice is currently disallowed by with.
Here's a silly example:

g : Set -> Set
g = ?

f : Set -> Set
f p with g p
... | p = ?

this gives the error:

Repeated variables in left hand side: p
when scope checking the left-hand side f p in the definition of f

I think that the original p should get replaced by _ in the helper function if its name has been
captured.

Original issue: http://code.google.com/p/agda/issues/detail?id=30

Coverage checker panic

From nils.anders.danielsson on March 10, 2008 17:37:00

-- Contrived example:

module Panic where

data [_](a : Set) : Set where
[] : [ a ]
∷ : a -> [ a ] -> [ a ]

data Ty : Set where
id : Ty
→ : Ty -> Ty -> Ty

fun : [ Ty ] -> Ty -> Ty
fun [] τ = τ
fun (σ ∷ σs) τ = σ → fun σs τ

data T : Ty -> Set where
c₁ : forall ts -> T (fun ts id)
c₂ : T (id → id)

foo : forall ts {a} -> T (fun ts a) -> _
foo (._ ∷ []) c₂ = ?

-- Error message:

-- Panic.agda:20,1-21
-- Panic: failed to split: CantSplit Panic.c₁
-- when checking the definition of foo

-- The error message should be improved.

Original issue: http://code.google.com/p/agda/issues/detail?id=50

Can not refine

From [email protected] on November 26, 2007 16:39:31

On line 37 p should be of type False, but Agda cannot see it
I even changed the def. of <N to make this more explicit but it didn't make
a difference

If I write acc-zero _ () instead I get
.x <N zero should be empty, but it isn't (as far as I can see)
but I do not understand why it cannot is it

Attachment: test.agda

Original issue: http://code.google.com/p/agda/issues/detail?id=27

more clever lifting of local functions

From [email protected] on January 09, 2008 18:44:06

The following little file type checks:

data Ty : Set where
ι : Ty
→ : Ty -> Ty -> Ty

data Con : Set where
ε : Con
< : Con -> Ty -> Con

data Var : Con -> Ty -> Set where
vZ : forall {Γ σ} -> Var (Γ < σ) σ
vS : forall {Γ σ}{τ : Ty} -> Var Γ σ -> Var (Γ < τ) σ

stren : forall {Γ σ} -> Var Γ σ -> Con
stren (vZ {Γ}) = Γ
stren (vS {τ = τ} v) = stren v < τ

/ : forall Γ {σ} -> Var Γ σ -> Con
Γ / v = stren v

thin : forall {Γ σ τ}(v : Var Γ σ) -> Var (Γ / v) τ -> Var Γ τ
thin vZ v' = vS v'
thin (vS v) vZ = vZ
thin (vS v) (vS v') = vS (thin v v')

However if I make stren a local function:

/ : forall Γ {σ} -> Var Γ σ -> Con
Γ / v = stren v where
stren : forall {Γ σ} -> Var Γ σ -> Con
stren (vZ {Γ}) = Γ
stren (vS {τ = τ} v) = stren v < τ

Then the definition of thin doesn't type check anymore highlighting the v' on the right hand side
of the last line:

(.Γ < .τ) != .Γ of type Con
when checking that the expression v' has type
Var (.Γ / v) (_79 v v')

Also if I change thin to:

thin vZ v' = vS v'
thin (vS v) v' = ? and examine the context of the produced goal the type of v' looks a bit weird:

v' : Var (.Bug._.stren (.Γ < .τ) (vS v) (vS v)) .τ

making stren global again yields:

v' : Var (stren (vS v)) .τ

The function stren is rather pointless... but that's beside the point :)

Original issue: http://code.google.com/p/agda/issues/detail?id=44

@-pattern causes panic

From [email protected] on October 24, 2007 12:50:19

The use of a@ in this code fragment

accSucc : (x : Nat) → Acc Nat Lt x → Acc Nat Lt (succ x)
accSucc x a@(acc .x h) = acc (succ x) (\ y p → ltcase y x p (Acc Nat Lt) h a)

causes a Panic:

BUG-THINGOUTOFCXT.agda:26,77–78
Panic: thing out of context ([CtxId 147,CtxId 146] not prefix of
[CtxId 149,CtxId 148,CtxId 147,CtxId 146])
when checking that the expression a has type Acc Nat Lt x

Attachment: Bug.agda

Original issue: http://code.google.com/p/agda/issues/detail?id=11

primitive integers doesn't work

From [email protected] on October 24, 2007 12:46:38

The module Bug for some reason yields the following error message:

Bug.agda:17,7–10
No binding for builtin thing ZERO, use {-# BUILTIN ZERO name #-} to
bind it to ‘name’
when checking that the expression bar has type 0 ≡ 0

If a BUILTIN ZERO pragma is added (see Bug2 ), then Agda panics: Bug2 .agda:25,7–10
Panic: Pattern match failure in do expression at
src/full/TypeChecking/Conversion.hs:119:6–29
when checking that the expression bar has type 0 ≡ 0

The modules are defined as follows:

module Bug where

postulate
ℤ : Set
Float : Set
≡ : ℤ → ℤ → Set

{-# BUILTIN INTEGER ℤ #-}
{-# BUILTIN FLOAT Float #-}

primitive primRound : Float → ℤ

ℤ−0 : ℤ
ℤ−0 = primRound 0.0

foo : ℤ−0 ≡ ℤ−0
foo = bar
where postulate bar : ℤ−0 ≡ ℤ−0

module Bug2 where

data ℕ : Set where
zero : ℕ
suc : ℕ → ℕ

{-# BUILTIN NATURAL ℕ #-}
{-# BUILTIN ZERO zero #-}
{-# BUILTIN SUC suc #-}

postulate
ℤ : Set
Float : Set
≡ : ℤ → ℤ → Set

{-# BUILTIN INTEGER ℤ #-}
{-# BUILTIN FLOAT Float #-}

primitive primRound : Float → ℤ

ℤ−0 : ℤ
ℤ−0 = primRound 0.0

foo : ℤ−0 ≡ ℤ−0
foo = bar
where postulate bar : ℤ−0 ≡ ℤ−0

Original issue: http://code.google.com/p/agda/issues/detail?id=10

incorrect highlighting of operators with unsolved metas

From [email protected] on October 24, 2007 12:37:07

Recently there was no highlighting for operators with termination problems,
and now there is no highlighting for operators with unsolved meta
variables. Example:

module Bug where

foo_ : {a : Set} → Set1 → Set1
foo_ x = x

bar : Set1
bar = foo Set

The last occurrence of foo should be highlighted, but it is not.

The reason for these problems is that operator ranges are represented in a
stupid way. We can fix the particular problem above with another hack, but
I would prefer if the root of these problems could be fixed.

Original issue: http://code.google.com/p/agda/issues/detail?id=7

Togglin the --no-coverage-check flag is not working in emacs

From [email protected] on January 26, 2008 02:18:32

Problem:

In emacs, I want to use the --no-coverage-check flag, so I write

{-# OPTIONS --no-coverage-check #-}

Now, I do not want to use it, so I erase the previous line, but Agda
continues working in "no coverage check" mode.

What version of the product are you using? Darcs version pulled after
2008-01-16

On what operating system? Ubuntu, 7.10

Original issue: http://code.google.com/p/agda/issues/detail?id=46

prettyTCM loops

From [email protected] on October 24, 2007 12:54:44

running

agda -v10 Bad2.agda

loops. As far as our analysis is concerned, pretty printing of the term

bad2 x + bad2 (succ x)

hangs agda.

Pretty printing of terms is invoked in

Termination/TermCheck.hs

termTerm :: MutualNames → QName → [DeBruijnPat] → Term → TCM Calls
termTerm names f pats0 t0 = do
reportSDoc “term.check.clause” 10
(sep [ text “termination checking clause of” <+> prettyTCM f
, nest 2 $ text “lhs:” <+> hsep (map prettyTCM pats0)
, nest 2 $ text “rhs:” <+> prettyTCM t0
])

in

prettyTCM t0

Original issue: http://code.google.com/p/agda/issues/detail?id=13

Can't build Agda 2.1.2 on Ubuntu Gutsy

From [email protected] on December 29, 2007 17:31:01

Compilation stops with the following error:
error: ../../undefined.h: No such file or directory

The complete build log:
$ runhaskell Setup.hs configure --user --prefix=/home/user/cabal
Configuring Agda-2.1.2...
Warning: No license-file field.
checking for gcc... gcc
checking for C compiler default output file name... a.out
checking whether the C compiler works... yes
checking whether we are cross compiling... no
checking for suffix of executables...
checking for suffix of object files... o
checking whether we are using the GNU C compiler... yes
checking whether gcc accepts -g... yes
checking for gcc option to accept ISO C89... none needed
checking for ghc... ghc
checking for ghc version... 6.6.1
checking for alex... alex
checking for alex version... 2.1.0
checking for happy... happy
checking for happy version... 1.16
checking for haddock... haddock
checking for haddock version... 0.8
checking for latex... latex
checking for pdflatex... pdflatex
checking for a BSD-compatible install... /usr/bin/install -c
checking for wget... wget
checking for false... false
checking for find... find
checking for diff... diff
checking for darcs... darcs
checking for mkdir... mkdir
checking for hasktags... hasktags
checking for runhaskell... runhaskell
configure: creating ./config.status
config.status: creating mk/config.mk

$ runhaskell Setup.hs build
Preprocessing library Agda-2.1.2...
Building Agda-2.1.2...

dist/build/Syntax/Parser/Parser.hs:29:0:
error: ../../undefined.h: No such file or directory

Original issue: http://code.google.com/p/agda/issues/detail?id=43

Eta expansion is not performed before "magic with" abstraction

From nils.anders.danielsson on December 11, 2007 01:24:53

module Bug where

data ≡ {a : Set} (x : a) : a -> Set where
≡-refl : x ≡ x

record × (a b : Set) : Set where
field
proj₁ : a
proj₂ : b

open ×

foo : forall {a b} (x : a × b) ->
record {proj₁ = proj₁ x; proj₂ = proj₂ x} ≡ x
foo x with proj₁ x | proj₂ x
foo x | x₁ | x₂ = ?

-- ?0 : record {proj₁ = x₁; proj₂ = x₂} ≡ x

Original issue: http://code.google.com/p/agda/issues/detail?id=37

Constraint solving could be more flexible

From nils.anders.danielsson on October 19, 2007 17:10:51

module Bug where

data K : Set where
a : K
b : K

data T : K -> Set where
ta : T a
tb : T b

f : forall k -> T k
f a = ta
f b = tb

data D : forall {k} (t : T k) -> Set where
c : forall {k} -> D (f k)

-- This function does not type check. It would type check if the
-- constraint k = a were solved before the constraint f k = f a.

foo : forall {t : T a} -> D t -> D t -> Set
foo c (c {k = a}) = K

Original issue: http://code.google.com/p/agda/issues/detail?id=2

computation gives up in mutual definition

From [email protected] on January 11, 2008 15:59:15

I tried to define thinning for a fragment of a typed syntax for dependent types:

In the attached fil the penultimate line doesn't type check because (at least) agda is not
computing the line "nil' = nil" (this line is necessary to get around constructors of data types not
being in scope of the types of mutually defined functions.

If you insert text after the comment on the penultimate line into the goal on the same line it and
do "C-u C-c C-d" then the expression "thin⁺ nil' σ ρ" has type "Ty (insert nil' σ)". "nil'" should
compute to "nil" and "insert nil σ" should then compute to "Γ < σ" and it should then have the
right type.

At least I think it should!

Attachment: DependentThinning.agda

Original issue: http://code.google.com/p/agda/issues/detail?id=45

the termination checker can't see dotted patterns

From [email protected] on October 24, 2007 12:44:47

It should be possible to detect termination when an argument is smaller
than a dotted pattern. For instance, the following code should terminate:

module Test where

data Nat : Set where
zero : Nat
suc : Nat → Nat

data Bool : Set where
true : Bool
false : Bool

&& : Bool → Bool → Bool
true && b = b
false && b = false

data Ty : {_ : Nat} → Set where
Base : forall {n} → Ty {suc n}
Arr : forall {n} → Ty {n} → Ty {n} → Ty {suc n}

subty : forall {n} → Ty {n} → Ty {n} → Bool
subty Base Base = true
subty (Arr σ τ) (Arr σ’ τ’) = subty σ’ σ && subty τ τ’
subty _ _ = false

Currently the termination checker cannot see that in both the two recursive
calls of subty the first (hidden) argument is strictly smaller than on the LHS.

Andreas: Discussed that with Ulf. The internal syntax erases the dotted
patterns constructed during pattern checking. This is an optimization for
speeding up execution, but the “logical” reading (fully reconstruced form)
of the second clause is

subty {suc n} (Arr {n} σ τ) (Arr {n} σ’ τ’) = subty {n} σ’ σ && subty {n} τ τ’

To keep internally a fully reconstructed form is probably not only useful
for the termination checker but also for other static analyses.

To print back the fully reconstructed form, as for instance Twelf does, is
also a good feedback to the user: He sees how the system “understood” his
input, and he can check that it understood it correctly. See
Main.PrintReconstructedTerms feature request.

Original issue: http://code.google.com/p/agda/issues/detail?id=9

working with records

From [email protected] on November 16, 2007 14:36:08

I define the record
record DLO : Set1 where
I : Set
< : I -> I -> Bool
irreflL : (a : I) -> F(a < a)
transL : {a b c : I} -> T(a < b) -> T(b < c) -> T(a < c)
linear : {a b c : I}-> F(a < b) -> F(b < c) -> F(a < c)

I want now to construct an elem of this record
record{ I = True;
< = (a b : True) -> false;
irreflL = ?;
transL = ?;
linear = ?
} Bug 1 ) If I have "?;" then emacs agda will go well but will not put the ?
in a green box Bug 2 ) If I want to refine any of the last 2 ? with "{a b c} p q -> ?"
agda will do refine as "({a b c} p q -> ?) ?"
Seems that if I only want to refine with "\p q -> ?" it works OK

Original issue: http://code.google.com/p/agda/issues/detail?id=22

Agda crashes on poorly formatted interface files

From nils.anders.danielsson on November 12, 2007 21:51:04

Truncate a valid interface file to just the first eight bytes, and make
Agda try to read this file. You will get the following error:

agda: user error (Codec.Compression.Zlib: premature end of compressed stream)

This can most likely be fixed by forcing the entire interface in
Interaction.Imports.readInterface.

Truncated interface files occur in practice, since Agda sometimes runs out
of stack space when trying to write an interface file. (This might also be
a bug.)

Original issue: http://code.google.com/p/agda/issues/detail?id=21

Interleaving type checking and termination checking

From [email protected] on December 17, 2007 10:48:29

What steps will reproduce the problem? 1. Define this module:

module bug where
A : Set
A = A -- non-terminating definition should give an error, not a loop
q : A
q = ? -- including this definition makes agda loop

  1. run agda bug.agda What is the expected output? What do you see instead? An error like "bug.A does NOT pass the termination check".
    Instead, agda loops. What version of the product are you using? On what operating system? Agda 2 version 2.1.3
    compiled from darcs repo 071212 or so. Please provide any additional information below. The emacs mode gets confused when agda does not respond. Ctrl-g gives back
    the cursor, but the process is still tied up in the background.

/Patrik

Original issue: http://code.google.com/p/agda/issues/detail?id=42

pragma suppresses shed

From [email protected] on November 21, 2007 17:58:28

{-# OPTIONS --dont-termination-check #-}

module Foo where

f : Set
f = ?

Loading this file with C-x-l doesn't turn the question mark into a nice green shed. It just stays
as a question mark. Removing the pragma and reloading causes the shed to appear.

module Foo where

f : Set
f = { }0

I wonder if this is related to Defect 20...

James

Original issue: http://code.google.com/p/agda/issues/detail?id=25

Incomprehensible error message related to open in let

From nils.anders.danielsson on December 11, 2007 20:38:29

module Bug where

record Foo (F : Set -> Set) : Set1 where

record Bar (F : Set -> Set) : Set1 where
field foo : Foo F
open Foo foo public
field bar : Set

Error message:

Let-definitions cannot do pattern matching or be recursive.
when scope checking
let open module _ = Foo foo public in (bar : Set) -> Prop

The let definition above does not use pattern matching, nor is it recursive.

Original issue: http://code.google.com/p/agda/issues/detail?id=41

Strange behaviour of open import public renaming

From nils.anders.danielsson on December 11, 2007 15:38:22

A.agda:

module A where

data B : Set where

Bug.agda:

module Bug where

open import A public using () renaming (B to C)
open import A

Foo : Set
Foo = C

Error message:

Bug.agda:7,7-8
Ambiguous name C. It could refer to any one of
.Bug._.B bound at A.agda:3,6-7
B bound at A.agda:3,6-7
when scope checking C

C has only been brought into scope once, so this is strange.

Maybe one should not import a module twice, but in that case an error
should be reported when the second import statement is checked.

Original issue: http://code.google.com/p/agda/issues/detail?id=38

the termination checker can't see dotted patterns

From [email protected] on October 24, 2007 12:40:20

It should be possible to detect termination when an argument is smaller
than a dotted pattern. For instance, the following code should terminate:

module Test where

data Nat : Set where
zero : Nat
suc : Nat → Nat

data Bool : Set where
true : Bool
false : Bool

&& : Bool → Bool → Bool
true && b = b
false && b = false

data Ty : {_ : Nat} → Set where
Base : forall {n} → Ty {suc n}
Arr : forall {n} → Ty {n} → Ty {n} → Ty {suc n}

subty : forall {n} → Ty {n} → Ty {n} → Bool
subty Base Base = true
subty (Arr σ τ) (Arr σ’ τ’) = subty σ’ σ && subty τ τ’
subty _ _ = false

Currently the termination checker cannot see that in both the two recursive
calls of subty the first (hidden) argument is strictly smaller than on the LHS.

Andreas: Discussed that with Ulf. The internal syntax erases the dotted
patterns constructed during pattern checking. This is an optimization for
speeding up execution, but the “logical” reading (fully reconstruced form)
of the second clause is

subty {suc n} (Arr {n} σ τ) (Arr {n} σ’ τ’) = subty {n} σ’ σ && subty {n} τ τ’

To keep internally a fully reconstructed form is probably not only useful
for the termination checker but also for other static analyses.

To print back the fully reconstructed form, as for instance Twelf does, is
also a good feedback to the user: He sees how the system “understood” his
input, and he can check that it understood it correctly. See <a
href= http://appserv.cs.chalmers.se/users/ulfn/wiki/agda.php?n=Main.PrintReconstructedTerms>Main.PrintReconstructedTerms feature request.

Original issue: http://code.google.com/p/agda/issues/detail?id=8

Hidden argument not handled correctly when with function is generated

From nils.anders.danielsson on October 19, 2007 17:18:08

module Bug where

infix 4 ≡

data ≡ {a : Set} (x : a) : a -> Set where
≡-refl : x ≡ x

postulate
≡-subst : {a : Set} -> (P : a -> Set)
-> forall {x y} -> x ≡ y -> P x -> P y
Kind : Set
simple : Kind
Ty : Kind -> Set
⊢_ : forall {k} -> Ty k -> Set
⌜_⌝⋆ : Ty simple -> Ty simple
lemma : forall τ -> τ ≡ ⌜ τ ⌝⋆

module SubstDef (• : forall {k} -> Ty k -> Set) where
postulate SubstKit : Set

module Subst {• : forall {k} -> Ty k -> Set}
(kit : SubstDef.SubstKit •) where

infixl 48 _/⊢

postulate
_/⊢ : forall {τ : Ty simple} -> ⊢ τ -> ⊢ τ

postulate
varKit : SubstDef.SubstKit ⊢_

open module VarSubst = Subst varKit

data ⊢↦_ : forall {k} -> Ty k -> Set where
foo : (τ : Ty simple) -> ⊢ τ -> ⊢↦ τ

postulate
↦_ : forall {τ : Ty simple} -> ⊢ τ -> ⊢↦ τ

⌜_⌝↦ : forall {τ} -> ⊢↦ τ -> ⊢↦ ⌜ τ ⌝⋆
⌜ foo τ e ⌝↦ = ↦ ≡-subst ⊢_ (lemma τ) e

_/⊢↦ : forall {k} {τ : Ty k} -> ⊢↦ τ -> ⊢↦ τ
(foo τ e) /⊢↦ = foo τ (e /⊢)

⌜/⊢↦⌝-lemma : forall {σ : Ty simple} (e : ⊢↦ σ)
-> (⌜ e ⌝↦ /⊢↦) ≡ (⌜ e /⊢↦ ⌝↦)
⌜/⊢↦⌝-lemma (foo τ e) = helper τ e ⌜ τ ⌝⋆ (lemma τ)
where
helper
: forall (τ : Ty simple) (e : ⊢_ {simple} τ) (σ : Ty simple)
-> (eq : τ ≡ σ)
-> ≡ {⊢↦_ {simple} σ}
(/⊢↦ {simple} {σ}
(↦ {σ} (≡-subst {Ty simple} (⊢_ {simple}) {τ} {σ}
eq e)))
(↦_ {σ} (≡-subst {Ty simple} (⊢_ {simple}) {τ} {σ}
eq (Subst./⊢ {{k} x -> ⊢ {k} x}
varKit {τ} e)))
helper τ e ._ ≡-refl = rhs
where postulate rhs : _
⌜/⊢↦⌝-lemma (foo τ e) with ⌜ τ ⌝⋆ | lemma τ
... | ._ | ≡-refl = rhs
where postulate rhs : _

-- The generation of a local with function fails here. The function
-- generated is almost identical to the function "helper" above, with
-- the exception that the eta-expanded version of ⊢_ towards the end
-- has become {\k x -> ⊢_ {k} x} instead of {{k} x -> ⊢_ {k} x}.

Original issue: http://code.google.com/p/agda/issues/detail?id=3

A name leaks into scope

From nils.anders.danielsson on November 30, 2007 11:40:36

module Bug where

record M : Set1 where
field
f : Set

module MOps (m : M) where
open M m public

postulate m : M

-- This works:

-- private
-- module MO = MOps m
-- open MO hiding (f)
-- open MO public using (f)

-- This works:

-- open MOps m using (f)
-- open MOps m hiding (f)

-- This doesn't:

open MOps m hiding (f)
open MOps m using (f)

postulate foo : f -> Set

Error message:

Ambiguous name f. It could refer to any one of
.Bug...f bound at /home/nad/work/lib/Bug.agda:5,5-6
..f bound at /home/nad/work/lib/Bug.agda:5,5-6
when scope checking f

Original issue: http://code.google.com/p/agda/issues/detail?id=31

Recommend Projects

  • React photo React

    A declarative, efficient, and flexible JavaScript library for building user interfaces.

  • Vue.js photo Vue.js

    🖖 Vue.js is a progressive, incrementally-adoptable JavaScript framework for building UI on the web.

  • Typescript photo Typescript

    TypeScript is a superset of JavaScript that compiles to clean JavaScript output.

  • TensorFlow photo TensorFlow

    An Open Source Machine Learning Framework for Everyone

  • Django photo Django

    The Web framework for perfectionists with deadlines.

  • D3 photo D3

    Bring data to life with SVG, Canvas and HTML. 📊📈🎉

Recommend Topics

  • javascript

    JavaScript (JS) is a lightweight interpreted programming language with first-class functions.

  • web

    Some thing interesting about web. New door for the world.

  • server

    A server is a program made to process requests and deliver data to clients.

  • Machine learning

    Machine learning is a way of modeling and interpreting data that allows a piece of software to respond intelligently.

  • Game

    Some thing interesting about game, make everyone happy.

Recommend Org

  • Facebook photo Facebook

    We are working to build community through open source technology. NB: members must have two-factor auth.

  • Microsoft photo Microsoft

    Open source projects and samples from Microsoft.

  • Google photo Google

    Google ❤️ Open Source for everyone.

  • D3 photo D3

    Data-Driven Documents codes.