[Agda] A different implementation of --without-K
Andreas Abel
andreas.abel at ifi.lmu.de
Thu Nov 28 23:34:38 CET 2013
Dear Jesper,
while you are at it, you might wanna look at my version of --without-K.
Maybe you can integrate some ideas from this into your approach.
I am attaching a patch against the latest darcs verion of Agda. The
patch contains some documentation of my approach, in the diff to the
release notes.
On 28.11.2013 16:50, Jesper Cockx wrote:
> I added parameter reconstruction to my implementation, as suggested by
> Nils. This rules out the examples WithoutK5.agda, WithoutK6.agda and
> WithoutK9.agda in test/fail (i.e. all the variants of weak-K). Some
> other examples (WithoutK4.agda, WithoutK7.agda, WithoutK8.agda and
> WithoutK10.agda) are still accepted, but it seems to me that these don't
> rely on K in an essential way. At least, I am able to define them (in a
> more complicated way) even when the normal --without-K is enabled. So it
> seems to be a feature of my flag that these examples are accepted, not a
> bug.
Yes, some of the fail test cases seem only to be there to document what
*is* rejected. I do not know what purpose this serves, since I would
expect only stuff there that *must be* rejected. For my version of
--without-K, I had to move some of these cases to test/succeed.
(see the patch).
I am a bit busy these days so I spare myself of lengthy explanations
now, but do come back with questions!
Cheers,
Andreas
> However, I am not convinced that parameter reconstruction is the correct
> way to go, as it seriously hampers reasoning about many parametrized
> types. Here are two examples that fail when either --without-K or the
> new version of --new-without-K is enabled:
>
> data Unit {l} : Set l where
> tt : Unit
>
> test₁ : ∀ {l} → _≡_ {l} tt tt → Set₁
> test₁ refl = Set
>
> data Box (A : Set) : Set where
> [_] : A → Box A
>
> test₂ : (x y : Bool) → [ x ] ≡ [ y ] → x ≡ y
> test₂ x .x refl = refl
>
> I wonder if there isn't a better way to handle parameters that doesn't
> rule out natural-looking code like this.
>
> @Dan: Thank you for the encouragement, I'll let you know when I have a
> version of the proof that I can show. I agree that we need a more
> principled solution for defining higher inductive types. The current
> implementation of --new-without-K doesn't distinguish individual data
> types (yet), but I'll look into it later.
>
> Jesper Cockx
>
>
>
>
> On Fri, Nov 22, 2013 at 9:16 PM, Dan Licata <drl at cs.cmu.edu
> <mailto:drl at cs.cmu.edu>> wrote:
>
> Hi Jesper,
>
> I think it's great that you're working out the theory of without-K---it
> would be wonderful to know that it actually works!
>
> One comment about allowing injectivity and disjointness in unification:
> it would be nice if there were a way to turn this on or off for
> individual datatypes. The reason is that we use datatypes to implement
> higher inductives types, and the constructors for those are not
> necessarily injective or disjoint. Right now, there is a hack for
> preventing disjointness from "leaking" outside the implementation of the
> higher inductive type (make the constructor take an extra argument of
> type (unit -> unit)), but it would be nice if there were a more
> principled solution. I just thought I'd comment, in case this fits into
> your new implementation.
>
> -Dan
>
> On Nov22, Jesper Cockx wrote:
> > Dear all,
> >
> > Lately I have been working on a proof of correctness for the
> --without-K
> > flag in Agda (someone should do it, right?). The proof itself is
> not quite
> > ready for prime time, but during my investigations I actually
> discovered a
> > more general (and, in my eyes, simpler) formulation of pattern
> matching
> > without K. In order to play around with this idea, I implemented
> a new flag
> > to Agda. Since a good number of people here seem interested in this
> > subject, I thought I'd share it.
> >
> > The idea is as follows: Suppose we want to split on a variable x
> of type "D
> > us" for some data type D with constructors "c_j : Delta_j -> D vs_j".
> > Instead of putting certain syntactic restrictions on the indices
> "us" (as
> > in the current implementation of --without-K), we limit the
> algorithm for
> > unification of "us" with "vs_j". We do this by refusing to deleting
> > reflexive equations of the form "x = x" where x is a variable.
> All other
> > unification steps (solution, injectivity, disjointness, and
> acyclicity)
> > keep working as usual. So for example, we allow unifying "suc x"
> with "suc
> > zero" or "suc x" with "suc y" (where y != x), but not "suc x"
> with "suc x".
> > This should rule out any definitions that depend on K (if my proof is
> > correct). It is also more general than the current
> implementation, since
> > the current implementation guarantees that we will never
> encounter "x = x"
> > during unification.
> >
> > In the attachment, you can find a patch to darcs agda. At the
> moment, it
> > adds a new flag called --new-without-K that restricts the unification
> > algorithm as described above. Here is an example of the error
> message:
> >
> > K : (A : Set) (x : A) → (p : x ≡ x) → p ≡ refl
> > K A x refl = refl
> >
> > Cannot eliminate reflexive equation x = x of type A because K has
> > been disabled.
> > when checking that the pattern refl has type x ≡ x
> >
> > One advantage is that this solves the problem where you can split
> on a
> > variable of type "something ≡ x", but not "x ≡ something" (see
> > https://lists.chalmers.se/pipermail/agda/2013/005407.html and
> > https://lists.chalmers.se/pipermail/agda/2013/005428.html). For
> example,
> > the following examples typecheck with --new-without-K enabled
> (but not with
> > the old --without-K):
> >
> > foo : (k l m : ℕ) → k ≡ l + m → {!!}
> > foo .(l + m) l m refl = {!!}
> >
> > bar : (n : ℕ) → n ≤ n → {!!}
> > bar .zero z≤n = {!!}
> > bar .(suc m) (s≤s {m} p) = {!!}
> >
> > I also added two tests to /test/succeed and /test/fail.
> >
> > What I'd like you to do, is:
> > 1. Try out my modification on your favorite examples,
> > 2. Tell me what you think,
> > 3. If you think it's good, add it to the main Agda branch.
> >
> > Best regards,
> > Jesper Cockx
>
>
> > _______________________________________________
> > Agda mailing list
> > Agda at lists.chalmers.se <mailto:Agda at lists.chalmers.se>
> > https://lists.chalmers.se/mailman/listinfo/agda
>
>
>
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>
--
Andreas Abel <>< Du bist der geliebte Mensch.
Theoretical Computer Science, University of Munich
Oettingenstr. 67, D-80538 Munich, GERMANY
andreas.abel at ifi.lmu.de
http://www2.tcs.ifi.lmu.de/~abel/
-------------- next part --------------
2 patches for repository abel at code.haskell.org:/home/srv/code/Agda:
Tue Oct 29 18:36:40 CET 2013 Andreas Abel <andreas.abel at ifi.lmu.de>
* Rolled forward Andreas new --without-K semantics.
Thu Oct 31 17:36:22 CET 2013 Andreas Abel <andreas.abel at ifi.lmu.de>
* Updated error message (probably associated with fix for issue 590).
New patches:
[Rolled forward Andreas new --without-K semantics.
Andreas Abel <andreas.abel at ifi.lmu.de>**20131029173640
Ignore-this: 97859aac0da013c3a1061da8a0258016
] move ./test/fail/WithoutKDisjointSum.agda ./test/succeed/WithoutKDisjointSum.agda
move ./test/fail/WithoutKRestrictive.agda ./test/succeed/WithoutKRestrictive.agda
move ./test/fail/WithoutKRestrictiveNoUniPoly.agda ./test/succeed/WithoutKRestrictiveNoUniPoly.agda
hunk ./doc/release-notes/2-3-4.txt 500
Which is a good thing!
+* --without-K is less restrictive. [Issue 712]
+ The handling of parameters differs from Agda 2.3.2 as follows:
+
+ 1. Parameters that occur in constructor indices are classified as
+ `non-linear' and treated just as indices.
+
+ 2. Parameters that are linear (i.e, fail 1.) and `big', i.e.,
+
+ a) levels or
+ b) type arguments of equal size (universe level) as the data type
+
+ are disregarded by the analysis.
+
+ New specification of --without-K:
+
+ If the flag is activated, then Agda only accepts certain
+ case-splits. If the type of the variable to be split is D ts,
+ where D is a data (or record) type, pars stands for the small
+ parameters among ts, and ixs the indices among ts (including
+ non-linear parameters), then the following requirements must be
+ satisfied:
+
+ * The indices ixs must be applications of constructors (or literals)
+ to distinct variables. Constructors are usually not applied to
+ parameters, but for the purposes of this check constructor
+ small parameters are treated as other arguments. Big parameters
+ and levels are ignored.
+
+ * These distinct variables must not be free in pars.
+
+ Examples:
+
+ * List type.
+
+ data List {a} (A : Set a) : Set a where
+ [] : List A
+ _∷_ : (x : A) (xs : List A) → List A
+
+ Parameter a is considered big since it is a level.
+ A is considered big because its level (a) is not strictly below
+ the level of the data type (also a).
+
+ * Small parameter.
+
+ data D {A : Set} (f : Unit → A) : A → Set where
+ d : ∀ {x} → D f x
+
+ A is big, f is small. This means that f will be considered as
+ constructor argument, just like x, (but not as index).
+
+ * Equality type.
+
+ data _≡_ {A : Set} (x : A) : A → Set where
+ refl : x ≡ x
+
+ Parameter A is big. x is non-linear, because it occurs in the
+ index in constructor refl.
+
+ * Big versus non-linear:
+
+ data _≡_ (A : Set) : Set → Set where
+ refl : A ≡ A
+
+ The parameter A is non-linear and treated as index.
+
+
Compiler backends
=================
hunk ./src/full/Agda/TypeChecking/Rules/LHS/Split.hs 372
def <- getConstInfo d
typedArgs <- args `withTypesFrom` defType def
+{- OLD
let noPars = case theDef def of
Datatype { dataPars = n } -> n
Record { recPars = n } -> n
hunk ./src/full/Agda/TypeChecking/Rules/LHS/Split.hs 379
_ -> __IMPOSSIBLE__
(pars, ixs) = genericSplitAt noPars typedArgs
return (map fst pars, ixs)
+-}
+ -- Andreas, 2013-05-30:
+ -- * treat non-linear parameters as indices
+ -- * ignore big parameters
+ let (noPars, smallPars, nonLinPars) = case theDef def of
+ Datatype { dataPars = n, dataSmallPars = Perm _ sps, dataNonLinPars = nl }
+ -> (n, sps, permPicks $ doDrop nl)
+ Record { recPars = n } -> (n, [0..n-1], []) -- TODO: smallness for record pars
+ _ -> __IMPOSSIBLE__
+ (pars0, ixs0) = genericSplitAt noPars typedArgs
+ -- Andreas, 2013-05-30 take only the small parameters
+ pars = map (pars0 !!) (smallPars \\ nonLinPars)
+ -- add the non-linear parameters to the indices
+ ixs = map (pars0 !!) nonLinPars ++ ixs0
+ return (map fst pars, ixs)
_ -> __IMPOSSIBLE__
hunk ./src/full/Agda/TypeChecking/Rules/LHS/Split.hs 422
constructorApplication (Lit {}) _ = return (Just [])
constructorApplication (Shared p) t = constructorApplication (derefPtr p) t
constructorApplication (Con c conArgs) (El _ (Def d es)) = do
+ let dataArgs = fromMaybe __IMPOSSIBLE__ $ allApplyElims es
conDef <- getConInfo c
dataDef <- getConstInfo d
hunk ./src/full/Agda/TypeChecking/Rules/LHS/Split.hs 426
+{- OLD
let noPars = case theDef dataDef of
Datatype { dataPars = n } -> n
Record { recPars = n } -> n
hunk ./src/full/Agda/TypeChecking/Rules/LHS/Split.hs 431
_ -> __IMPOSSIBLE__
- dataArgs = fromMaybe __IMPOSSIBLE__ $ allApplyElims es
pars = genericTake noPars dataArgs
allArgs = pars ++ conArgs
hunk ./src/full/Agda/TypeChecking/Rules/LHS/Split.hs 444
]
constructorApplications =<< allArgs `withTypesFrom` defType conDef
+-}
+
+ let (noPars, smallPars) = case theDef dataDef of
+ Datatype { dataPars = n, dataSmallPars = Perm _ is }
+ -> (n, is)
+ Record { recPars = n } -> (n, [0..n-1])
+ _ -> __IMPOSSIBLE__
+
+ dataPars = take noPars dataArgs
+
+ allArgs <- (dataPars ++ conArgs) `withTypesFrom` defType conDef
+
+ -- skip big parameters during reconstruction
+ let ixs = drop noPars allArgs
+ pars = map (allArgs !!) smallPars
+
+ reportSDoc "tc.lhs.split.well-formed" 20 $
+ fsep [ text "Reconstructed parameters:"
+ , nest 2 $
+ prettyTCM (Con c []) <+>
+ text "(:" <+> prettyTCM (defType conDef) <> text ")" <+>
+ text "<<" <+> prettyTCM (map fst pars) <+> text ">>" <+>
+ prettyTCM conArgs
+ ]
+
+ constructorApplications $ pars ++ ixs
constructorApplication _ _ = return Nothing
hunk ./test/fail/Issue765.err 2
Issue765.agda:63,11-15
-The index
+The indices
+ sup (inj₁ m) ⊥-elim
sup (inj₁ n) ⊥-elim
hunk ./test/fail/Issue765.err 5
-is not a constructor (or literal) applied to variables (note that
+are not constructors (or literals) applied to variables (note that
parameters count as constructor arguments)
when checking that the pattern refl has type
sup (inj₁ m) ⊥-elim ≡ sup (inj₁ n) ⊥-elim
hunk ./test/fail/Issue865Big.err 4
Issue865Big.agda:9,7-11
The variables
A
-which are used (perhaps as constructor parameters) in the index
-expressions
A
hunk ./test/fail/Issue865Big.err 5
-are free in the parameters
+in the indices
A
hunk ./test/fail/Issue865Big.err 7
+ A
+are not distinct (note that parameters count as constructor
+arguments)
when checking that the pattern refl has type A ≡ A
hunk ./test/fail/WithoutK-PatternMatchingLambdas1.err 4
WithoutK-PatternMatchingLambdas1.agda:11,18-22
The variables
x
-which are used (perhaps as constructor parameters) in the index
-expressions
x
hunk ./test/fail/WithoutK-PatternMatchingLambdas1.err 5
-are free in the parameters
- {_}
+in the indices
x
hunk ./test/fail/WithoutK-PatternMatchingLambdas1.err 7
+ x
+are not distinct (note that parameters count as constructor
+arguments)
when checking that the pattern refl has type x ≡ x
hunk ./test/fail/WithoutK-PatternSynonyms1.err 4
WithoutK-PatternSynonyms1.agda:13,12-13
The variables
x
-which are used (perhaps as constructor parameters) in the index
-expressions
x
hunk ./test/fail/WithoutK-PatternSynonyms1.err 5
-are free in the parameters
- {_}
+in the indices
x
hunk ./test/fail/WithoutK-PatternSynonyms1.err 7
+ x
+are not distinct (note that parameters count as constructor
+arguments)
when checking that the pattern refl has type x ≡ x
hunk ./test/fail/WithoutK1.err 4
WithoutK1.agda:13,7-11
The variables
x
-which are used (perhaps as constructor parameters) in the index
-expressions
x
hunk ./test/fail/WithoutK1.err 5
-are free in the parameters
- {_}
+in the indices
x
hunk ./test/fail/WithoutK1.err 7
+ x
+are not distinct (note that parameters count as constructor
+arguments)
when checking that the pattern refl has type x ≡ x
conflictor [
hunk ./test/fail/WithoutK10.err 8
- {A} (λ {unit → x}) {A} {x}
+ {A}
+ (λ { unit → x
+ })
+ {A} {x}
hunk ./test/fail/WithoutK10.err 9
- (λ { unit → x
- })
- {A} {x}
+ (λ { unit → x }) {A} {x}
]
:
hunk ./test/fail/WithoutK10.err 8
- {A} (λ {unit → x}) {A} {x}
+ (λ {unit → x}) {A} {x}
hunk ./test/fail/WithoutK3.err 4
WithoutK3.agda:25,9-13
The variables
A
-which are used (perhaps as constructor parameters) in the index
-expressions
- {A}
+ x
+ A
y
hunk ./test/fail/WithoutK3.err 7
-are free in the parameters
+in the indices
{A}
x
hunk ./test/fail/WithoutK3.err 10
+ {A}
+ y
+are not distinct (note that parameters count as constructor
+arguments)
when checking that the pattern refl has type _≅_ {A} x {A} y
hunk ./test/fail/WithoutK4.err 2
WithoutK4.agda:10,16-20
-The index
+The indices
+ x
f y
hunk ./test/fail/WithoutK4.err 5
-is not a constructor (or literal) applied to variables (note that
+are not constructors (or literals) applied to variables (note that
parameters count as constructor arguments)
when checking that the pattern refl has type x ≡ f y
hunk ./test/fail/WithoutK5.err 3
WithoutK5.agda:12,24-28
The variables
- A
a
hunk ./test/fail/WithoutK5.err 4
-which are used (perhaps as constructor parameters) in the index
-expressions
+ a
+in the indices
refl
hunk ./test/fail/WithoutK5.err 7
-are free in the parameters
- {_≡_ {A} a a}
refl
hunk ./test/fail/WithoutK5.err 8
+are not distinct (note that parameters count as constructor
+arguments)
when checking that the pattern refl has type
_≡_ {_≡_ {A} a a} refl refl
hunk ./test/fail/WithoutK6.err 1
-WithoutK6.agda:11,28-42
+WithoutK6.agda:11,45-59
The variables
hunk ./test/fail/WithoutK6.err 3
- A
a
hunk ./test/fail/WithoutK6.err 4
-which are used (perhaps as constructor parameters) in the index
-expressions
+ a
+in the indices
+ refl a
refl a
hunk ./test/fail/WithoutK6.err 8
- q
-are free in the parameters
- {_≡_ {A} a a}
+are not distinct (note that parameters count as constructor
+arguments)
when checking that the pattern refl .(refl a) has type
hunk ./test/fail/WithoutK6.err 11
-_≡_ {_≡_ {A} a a} (refl a) q
+_≡_ {_≡_ {A} a a} (refl a) (refl a)
hunk ./test/fail/WithoutK9.err 1
-WithoutK9.agda:17,26-30
+WithoutK9.agda:17,21-25
The variables
A
x
hunk ./test/fail/WithoutK9.err 8
which are used (perhaps as constructor parameters) in the index
expressions
refl
+ q
are free in the parameters
{E._≡_ x}
hunk ./test/fail/WithoutK9.err 11
- refl
-when checking that the pattern refl has type
-_≡_ {E._≡_ x} refl refl
+when checking that the pattern refl has type _≡_ {E._≡_ x} refl q
hunk ./test/fail/WithoutKDisjointSum.err 1
-WithoutKDisjointSum.agda:15,1-16
-The variables
- .A₁
- .B₁
-which are used (perhaps as constructor parameters) in the index
-expressions
- inr b₁
-are free in the parameters
- {_}
- {_}
- inl a₁
-when checking that the clause distinct a b () has type
-{A B : Set} (a : A) (b : B) → inl a ≡ inr b → ⊥
rmfile ./test/fail/WithoutKDisjointSum.err
hunk ./test/fail/WithoutKRestrictive.err 1
-WithoutKRestrictive.agda:46,23-27
-The index
- x ∷ xs
-is not a constructor (or literal) applied to variables (note that
-parameters count as constructor arguments)
-when checking that the pattern refl has type
-_≡_ {lzero} {List {lzero} A} ys (x ∷ xs)
rmfile ./test/fail/WithoutKRestrictive.err
hunk ./test/fail/WithoutKRestrictiveNoUniPoly.err 1
-WithoutKRestrictiveNoUniPoly.agda:57,23-27
-The variables
- A
-which are used (perhaps as constructor parameters) in the index
-expressions
- x ∷ xs
-are free in the parameters
- {List A}
- ys
-when checking that the pattern refl has type
-_≡_ {List A} ys (x ∷ xs)
rmfile ./test/fail/WithoutKRestrictiveNoUniPoly.err
conflictor [
hunk ./test/interaction/Issue388.out 11
+(agda2-highlight-load-and-delete-action)
]
:
hunk ./test/interaction/Issue388.out 9
-Agda2> Agda2> Agda2> (agda2-info-action "*Error*" "Issue388.agda:11,11-16\nThe variables\n A₁\nwhich are used (perhaps as constructor parameters) in the index\nexpressions\n d A₁\nare free in the parameters\n D A₁\nwhen checking that the expression ? has type Set" nil)
-((last . 3) . (agda2-goto '("Issue388.agda" . 191)))
-(agda2-status-action "")
+Agda2> Agda2> Agda2> ((last . 2) . (agda2-make-case-action '("Foo A (p .(d A)) = ?")))
+((last . 1) . (agda2-goals-action '(0)))
[Updated error message (probably associated with fix for issue 590).
Andreas Abel <andreas.abel at ifi.lmu.de>**20131031163622
Ignore-this: ed59c296cb016af4d87e9d8a37e10dd
] conflictor {{
:
hunk ./test/interaction/Issue388.out 11
+(agda2-highlight-load-and-delete-action)
:
hunk ./test/interaction/Issue388.out 9
-Agda2> Agda2> Agda2> (agda2-info-action "*Error*" "Issue388.agda:11,11-16\nThe variables\n A₁\nwhich are used (perhaps as constructor parameters) in the index\nexpressions\n d A₁\nare free in the parameters\n D A₁\nwhen checking that the expression ? has type Set" nil)
-((last . 3) . (agda2-goto '("Issue388.agda" . 191)))
-(agda2-status-action "")
+Agda2> Agda2> Agda2> ((last . 2) . (agda2-make-case-action '("Foo A (p .(d A)) = ?")))
+((last . 1) . (agda2-goals-action '(0)))
}} []
hunk ./test/interaction/Issue388.out 9
-Agda2> Agda2> Agda2> (agda2-info-action "*Error*" "Issue388.agda:11,11-16\nThe variables\n A₁\nwhich are used (perhaps as constructor parameters) in the index\nexpressions\n d A₁\nare free in the parameters\n D A₁\nwhen checking that the expression ? has type Set" nil)
-((last . 3) . (agda2-goto '("Issue388.agda" . 191)))
-(agda2-status-action "")
+Agda2> Agda2> Agda2> ((last . 2) . (agda2-make-case-action '("Foo A (p .(d A)) = ?")))
+((last . 1) . (agda2-goals-action '(0)))
:
hunk ./test/interaction/Issue388.out 10
+((last . 3) . (agda2-next-goal))
Context:
[[ issue 730 ] BUILTIN NATURAL now binds ZERO and SUC
ulfn at chalmers.se**20131127183458
Ignore-this: 891799ff423bcb066b50ac022b404ccd
- consequently trying to bind them separately gives an error message
explaining the new order of things
]
[[ issue981 ] functions with absurd clauses mistakenly considered projection-like
ulfn at chalmers.se**20131127123634
Ignore-this: b4039f7cdcc29b57468027549c81a2d6
]
[[ issue 147 ] Use non-mixfix form in the "Don't know how to parse" error message.
gelisam at gmail.com**20131124024118
Ignore-this: 9fd49fec15ffb0bf16ffcdd96affff71
]
[Added nofib/N-queens.
Nils Anders Danielsson <nils.anders.danielsson at gmail.com>**20131122105622
Ignore-this: aa6ecc5be74f9e25e21a81ba1a2c3a5e
]
[[ issue 970 ] fixed impossible when inlining with-function calls
ulfn at chalmers.se**20131120103505
Ignore-this: 47e7ec70916170c1e8f6794f24b7e37f
]
[[ issue 952 ] refactored parser to prepare for parsing of labeled implicit functions
ulfn at chalmers.se**20131115193331
Ignore-this: e34e5ead15512bb15d6bf2ff5428e64
]
[Postpone size constraint solving to make sizes work with extended lambda.
Andreas Abel <andreas.abel at ifi.lmu.de>**20131123194504
Ignore-this: d8784cd37b7cab85d4d8ee21b306fb11
Solver now not invoked after checking extended lambda definition.
]
[Micro-refactoring: a use of defaultDefn.
Andreas Abel <andreas.abel at ifi.lmu.de>**20131123174115
Ignore-this: f8e6d6bc414fe4277b47c055d7b4cf0
]
[[ Issue 977 ] Postulates are now allowed in old-style mutual blocks.
Andreas Abel <andreas.abel at ifi.lmu.de>**20131123153656
Ignore-this: 7515e1918d581704343d3ec5d10da671
They were already allowed in new-style mutual blocks.
]
[Tiny refactor: more direct implementation of notAllowedInMutual in Concrete.Definitions.
Andreas Abel <andreas.abel at ifi.lmu.de>**20131123150701
Ignore-this: 8d3242485e1a8495c0778914147a1ff7
]
[Rolled back emacs key bindings for comment region.
Andreas Abel <andreas.abel at ifi.lmu.de>**20131122211123
Ignore-this: 9a14a50cb99e7cd3a456574b2861bba0
]
[[ issue 957 ] Now there is a proper error stating that Agsy does not support copatterns yet.
Andreas Abel <andreas.abel at ifi.lmu.de>**20131122094410
Ignore-this: 4cd9d5cd1d87e884013176754e460848
]
[Refined test cases for termination checking with projections.
Andreas Abel <andreas.abel at ifi.lmu.de>**20131122063211
Ignore-this: 26c39ba90e6fba3c9e6a00a6d7df8395
]
[Fixed issue 959: match against record pattern must succeed, even before record pattern translation.
Andreas Abel <andreas.abel at ifi.lmu.de>**20131122063054
Ignore-this: c172a37be7c24074ad1257ac8c00eb3e
Needed for type-checking copattern clauses which happenes before record pattern translation.
]
[Refactor: removed Arg from matchPattern (was unused).
Andreas Abel <andreas.abel at ifi.lmu.de>**20131122060522
Ignore-this: 7116f1c4112a43296af9d7ee9f5d8706
]
[Updated error messages for Size< move to Common.Size.
Andreas Abel <andreas.abel at ifi.lmu.de>**20131120160904
Ignore-this: 4bfa34142770dd5dcf69034c63fcc2c7
]
[Fixed bug in termination checker that would drop coinductive projections silently when comparing elimination of variable to variable pattern.
Andreas Abel <andreas.abel at ifi.lmu.de>**20131120145750
Ignore-this: f27ef9831e490cf0dabb95fb98789671
]
[More low-level debug message in Reduce.
Andreas Abel <andreas.abel at ifi.lmu.de>**20131119095934
Ignore-this: cbfe0ea4663af7d3a85c672296cc4dd5
]
[It feels safer to start out with no eta-expansion for coinductive records from the start.
Andreas Abel <andreas.abel at ifi.lmu.de>**20131119095831
Ignore-this: b443f3c80df4c96d209baa1bdc098c84
I think Agda actually did eta-expand some coinductive record metas before this change,
so this might actually fix a potential bug.
]
[Documentation: Some more examples for permutations.
Andreas Abel <andreas.abel at ifi.lmu.de>**20131119095658
Ignore-this: 54333a18d0578a45f7373255cc03e58c
]
[Added Size< to test/Common/Size.agda.
Andreas Abel <andreas.abel at ifi.lmu.de>**20131119095624
Ignore-this: 25113c55e0b79b1494c701af4fff388c
]
[Fixed a bug involving copatterns and dot patterns.
Andreas Abel <andreas.abel at ifi.lmu.de>**20131119094253
Ignore-this: 3ae5959d73c81abe2d0e5971e971b12e
Coverage checker output wrong split tree, leading to a failing reduction.
]
[[ emacs-mode ] Default key bindings for (un)comment-region.
Andreas Abel <andreas.abel at ifi.lmu.de>**20131118141956
Ignore-this: 60dc27bc65182a4f8a187fe7177f3bf2
]
[Allow empty hiding and renaming lists in the parser.
Andreas Abel <andreas.abel at ifi.lmu.de>**20131118141757
Ignore-this: 132621901d77aeb92dcf8376fefe0b09
They should not be errors since it is semantically meaningful,
even though it's pointless.
It might well be that during interactive editing,
the hiding list becomes empty temporarily.
]
[Make Agda compile again with ghc-6.12.1.
james at cs.ioc.ee**20131118115012
Ignore-this: 83ebca9b8b171398d05da9bb65d59a4b
]
[[ LaTeX-backend ] Add test suite
Stevan Andjelkovic <stevan.andjelkovic at strath.ac.uk>**20131115112648
Ignore-this: 73a56c597c7dc216ed207b8927426359
]
[[LaTeX-backend] remove trailing/leading spaces after/before begin/end-code blocks
Stevan Andjelkovic <stevan.andjelkovic at strath.ac.uk>**20131115113234
Ignore-this: ba73eb1e227cccf537f2822a056f5b71
]
[Test case related to issue 840.
Nils Anders Danielsson <nils.anders.danielsson at gmail.com>**20131115173711
Ignore-this: aada68e518da3f6839596e39a0bec217
]
[[ issue 963 ] renamed Agda.Prim to Agda.Primitive
ulfn at chalmers.se**20131115110242
Ignore-this: 962c4f821f1ba7eecab63316bd2be921
]
[[ issue 952 ] Printing alpha renamed implicit fun types with labeled preserved
ulfn at chalmers.se**20131115104147
Ignore-this: 5c7628eec249ef785e911f98125535f4
- If A is already in scope {A : Set} -> T A is printed as
{A = A1 : Set} -> T A1
- This syntax is not (yet?) parsed
]
[tested with ghc-7.2.2 and ghc-7.4.2
ulfn at chalmers.se**20131114165736
Ignore-this: 4a929cfb21951d53400d65c6685e01b1
- ghc-7.0.2 segfaults on my machine so left it out of the cabal file
]
[[ issue 962 ] ghc-7.0.3 gives incomplete pattern warnings for lambda matches
ulfn at chalmers.se**20131114122214
Ignore-this: d05df67d0597065fbc0e6f02661b74e
]
[[ issue 961 ] added TypeSynonymInstances to Agda.TypeChecking.Primitive
ulfn at chalmers.se**20131114111053
Ignore-this: 337d54b14c329b3582ed321a3c93ace8
- needed for compilation on ghc-7.0.4
]
[Fixed issue 157.
Nils Anders Danielsson <nils.anders.danielsson at gmail.com>**20131114104706
Ignore-this: b91b91dbf5cfabee59f8b9d87db3fa30
]
[Tried to fix issue 960.
Nils Anders Danielsson <nils.anders.danielsson at gmail.com>**20131114104743
Ignore-this: 1563d4fd89732399c9e987fba58dd171
]
[[ issue 157 ] now overlays unsolved meta and error highlighting
ulfn at chalmers.se**20131113210450
Ignore-this: 917ed2ea4b419478273e75afeb07c531
- the black text property needs to be removed from the default highlighting
for this to look nice (otherwise you get black underlined text instead of
red at the overlap)
]
[[ issue 59 ] expand with-function calls that may have been inserted during type checking
ulfn at chalmers.se**20131113190723
Ignore-this: 41e9bd465083b78085a71e1047079823
- they now match the inlined clauses
- metavariable instantiation is sufficiently paranoid about cycles that
it wasn't actually possible to exploit this to do something bad, but
it was an easy fix
]
[[ issue 59 ] added another case to the test/fail test
ulfn at chalmers.se**20131113183339
Ignore-this: 64a0ad14f21a4603644707c2488dbb65
]
[added some debug printing to MetaVars.Occurs
ulfn at chalmers.se**20131113181755
Ignore-this: 7af1c7b9833f94d781d317ffeff91280
]
[[LaTeX-backend] Remove excessive spacing after aligned stuff in agda.sty
Stevan Andjelkovic <stevan.andjelkovic at strath.ac.uk>**20131112165139
Ignore-this: e1ef3a26e8fd201814bd8d5621b9771f
]
[[ issue 59 ] fix bug where a with-function call could get inlined in the wrong function
ulfn at chalmers.se**20131113160110
Ignore-this: 71c18a0328fafc1aa7139857172ac42b
]
[[ issue 953 ] documented in release notes
ulfn at chalmers.se**20131113110035
Ignore-this: cc51b2e12f4eb86bc5ab052ea5b240ae
- also test case for parameterised anonymous module
]
[[ issue 953 ] fixed
ulfn at chalmers.se**20131113104718
Ignore-this: 5522c7bc1affa2773204de56122acf28
- you can now omit the top-level module, or, equivalently, define it as
module _ where
]
[[ issue 953 ] the parser now inserts module _ where if no top-level module is defined
ulfn at chalmers.se**20131113092653
Ignore-this: 88bad1867651dd360caf1f27c12ea9bc
- todo: handle that when checking module name
]
[[ with-termination ] use getBodyUnraised
ulfn at chalmers.se**20131113075750
Ignore-this: 8b7376a94207e569a791e7dc3c5719b6
]
[[ issue 157 ] fixed unsolved meta highlighting hiding error highlighting
ulfn at chalmers.se**20131113075655
Ignore-this: 6385d8a8a5d008fbcd23ad3db0f9c150
]
[[ issue 945 ] correct output for interaction test
ulfn at chalmers.se**20131113075631
Ignore-this: 6c70f0e09feefbb5ec7460ac7e4e53c6
]
[Failed to apply the theory of decorations.
Andreas Abel <andreas.abel at ifi.lmu.de>**20131113165346
Ignore-this: 865cb6247897f554367b8ecd04821252
]
[The beautiful categorical theory of decorations (aka one-place-functors).
Andreas Abel <andreas.abel at ifi.lmu.de>**20131113165305
Ignore-this: 62a0a4607fafe7678609af1ae2007f1b
Unfortunately, without applications yet.
]
[Refactor: clauseArgs is an instance of patternsToElims.
Andreas Abel <andreas.abel at ifi.lmu.de>**20131113165122
Ignore-this: 3a4c2642e9a15e337a4dd9908b3086f
]
[Improved the previous fix.
Nils Anders Danielsson <nils.anders.danielsson at gmail.com>**20131112144155
Ignore-this: 98099146fb6b8c2e9c63387f3053256c
+ The presence of a comment in the source actually broke the fix...
+ The new test case should run much faster.
]
[Updated test case after fix for issue 945.
Andreas Abel <andreas.abel at ifi.lmu.de>**20131112143622
Ignore-this: 5750a71fbd368a4c33125c85eab88753
]
[Tried to fix race condition reported by Andreas.
Nils Anders Danielsson <nils.anders.danielsson at gmail.com>**20131112140239
Ignore-this: 8dd143007ba0417265d784e01910c5ae
]
[[issue 945] auto -l now reports whether or not it timed out
ulfn at chalmers.se**20131111200148
Ignore-this: 2362fa89debf796d0e4f361af2e38f09
]
[Updated error message for issue 949.
Andreas Abel <andreas.abel at ifi.lmu.de>**20131112002337
Ignore-this: 13989e06a3cc978b5fe60cd1c6e73fa2
]
[[ issue 950 ] Better split error messages for copatterns.
Andreas Abel <andreas.abel at ifi.lmu.de>**20131112002252
Ignore-this: 44bdb40fcbc7f3a65fc0240389ff760f
]
[[ issue 951 ] Hidden function types cannot be printed as {A} -> B, only as {x : A} -> B.
Andreas Abel <andreas.abel at ifi.lmu.de>**20131111233833
Ignore-this: 777447c0f112ae3612d60a4df3137292
]
[[ issue 949 ] Better error message for wrong named argument.
Andreas Abel <andreas.abel at ifi.lmu.de>**20131111214701
Ignore-this: 909b5fbf3aac87748a5a9d253d4dbde7
Refactored checkArguments to make that work.
]
[Partial review of new module Termination.Inlining.
Andreas Abel <andreas.abel at ifi.lmu.de>**20131111190124
Ignore-this: ff5241031ac333bd2e7bf7b68d82d820
- Great to have this issue fixed!!!
- Added comments and preconditions.
- Replaced helper function allArgs by use of allApplyElims.
- Moved helper function getRHS into Substitute as getBodyUnraised.
- Operate inTopContext.
- Use caseMaybeM.
- Check for omission of withExprClause could be more general.
- Test Issue59 does not test calls from clauses with dot patterns.
Did not review the main work horse: inline.
Looks like my review did not break anything.
Please review my review!
]
[Cut some long-retired code.
Andreas Abel <andreas.abel at ifi.lmu.de>**20131111175941
Ignore-this: 6a82a5af4e750b195b4b04ea2fc34dd4
]
[A more precise comment in TermCheck.
Andreas Abel <andreas.abel at ifi.lmu.de>**20131111175912
Ignore-this: 6fdf706c2f3783530ff6fb08d5bddd93
]
[Refactor: new utilities caseMaybe and caseMaybeM.
Andreas Abel <andreas.abel at ifi.lmu.de>**20131111175839
Ignore-this: 8b37245aed9c0304a61cb6928fc9308f
- Use @caseMaybe m err f@ instead of @flip (maybe err) m f at .
- Use
caseMaybeM query default $ \ x -> interesting
instead of
m <- query
case m of
Nothing -> default
Just x -> interesting
if @query@ and @default@ are short pieces of code.
]
[Added -fwarn-pointless-pragmas, removed possibly pointless pragmas.
Nils Anders Danielsson <nils.anders.danielsson at gmail.com>**20131111152552
Ignore-this: 2d89c53802eccd3adffb30045f2c42a8
+ I could either remove INLINE or SPECIALIZE INLINE. I tested both
options, and they seem to give more or less the same performance,
both when profiling and when not (at least on my current setup, and
for the given test case).
]
[Removed -fwarn-unused-imports warning.
Andrés Sicard-Ramírez <andres.sicard.ramirez at gmail.com>**20131108145005
Ignore-this: f84c1aacce712ff05ab382ab28ad4f93
]
[Replaced __GLASGOW_HASKELL__ < 707 with !(MIN_VERSION_base(4,7,0)).
Nils Anders Danielsson <nils.anders.danielsson at gmail.com>**20131111134018
Ignore-this: 781065a38a15d8a5cde02bf4b37fcb10
]
[[issue 59] fixed termination checking of with-functions
ulfn at chalmers.se**20131111111805
Ignore-this: bd1debe5c3c7df8c6a65221489ec913c
- See Agda.Termination.Inlining
- Before termination checking with-functions are inlined, which
means that the termination checker runs on something very close to
the source program instead of the desugared program using a helper
function
- A minor disadvantage is that you can no longer have termination
paths going through with-expressions, like the following:
bla n with n
... | zero = zero
... | suc m = bla m
since this is transformed into (something like)
bla n | zero = zero
bla n | (suc m) = bla m _
before termination checking. This is only a problem if you do with
on a variable, which you never need to do. The standard library
checks without changes, so I don't think it's an issue.
]
[fixed clause rhs getting reified with the wrong context
ulfn at chalmers.se**20131111110033
Ignore-this: ecf028ab7cbf727c8fb107c2add4c2bf
- updated Agsy no longer generate the wrong rhs as a work-around
]
[added a function clauseArgs to compute terms corresponding to the lhs of a clause
ulfn at chalmers.se**20131111105917
Ignore-this: 4ad6a7b4139796256dfbee67711320c7
]
[turned ClauseBody into a functor in the rhs
ulfn at chalmers.se**20131110070353
Ignore-this: fe38aed7d7f3afa675a59cf58f8bd587
]
[haddock syntax errors
ulfn at chalmers.se**20131110070206
Ignore-this: 9b79d5503cc7f741f03bd42653ea64f
]
[added a field funWith to the representation of function definitions
ulfn at chalmers.se**20131109171851
Ignore-this: fa0015373009742ad30b859d68fcf149
- keeps track of if the function is a generated with function and which
is the parent function
- not used for anything at the moment, but it might come in handy shortly
]
[[release notes] documented improvements to make case
ulfn at chalmers.se**20131109144751
Ignore-this: e3bd86cdc9251b99ff611d9b37520023
]
[[issue 811] fixed the remaining problems
ulfn at chalmers.se**20131109143632
Ignore-this: b891fcd26845f0038ed680dd6e4470cf
- make case now always binds a variable at its left-most explicit occurrence
- if there are no explicit occurrences it's bound at the left-most implicit
occurrence
]
[[issue 157] Unsolved metas are now highlighted in the emacs mode also when there are errors
ulfn at chalmers.se**20131109102758
Ignore-this: fa255575ff15fbd29b9301814985586a
]
[[build] use -j3 when building on ghc >= 7.7
ulfn at chalmers.se**20131109091031
Ignore-this: 42e3314074cd54705fe99b291a873ac5
]
[[issue 493] using/hiding/renaming can now appear in arbitrary order
ulfn at chalmers.se**20131109083035
Ignore-this: 29bbeee49697d14db1282bd40b48a6e0
]
[[issue 947] empty where blocks are now allowed
ulfn at chalmers.se**20131109061146
Ignore-this: cc97ac61033bb3e26969fa4e514a5bf6
]
[[test] put the horrible sed mangling of error messages in test/fail in a separate bash script
ulfn at chalmers.se**20131108165920
Ignore-this: 4daf71adceb5e8f6ab3dc6f27dcc3768
]
[moved reifyWhen into Reify and removed ReifyWhen class
ulfn at chalmers.se**20131108134448
Ignore-this: 4d215e5d5c77cee5d35c6606154767ab
- some of the class constraints used would break in ghc-7.8
]
[[ghc-7.7] TCMT needs to be a newtype in the hs-boot file as well with ghc-7.7
ulfn at chalmers.se**20131108134343
Ignore-this: d756e7aa1662dc6f091140adf0fa4cf0
]
[[malonzo] produce phased inline directives for nat/int conversion functions
ulfn at chalmers.se**20131108134310
Ignore-this: 2ee7f710213be91cfbec6275fada630d
]
[fixed some warnings emitted by ghc-7.7
ulfn at chalmers.se**20131108134215
Ignore-this: ccbcc755104011d08dcbedd5839e8a71
]
[[cabal] relaxed array constraint to allow ghc-7.7 array lib
ulfn at chalmers.se**20131108134145
Ignore-this: 987365d2d1b8d7cd996d9e7dccfc6d56
]
[don't use deprecated Data.Binary.runGetState
ulfn at chalmers.se**20131101084044
Ignore-this: 6eefed48c34058dcf76cb1f9322192a8
- can now actually build with 0.6 =< binary < 0.8 as claimed
- on the other hand binary-0.5 is no longer supported
]
[base-4.7 has more functor instances (added #ifdef)
ulfn at chalmers.se**20131101083946
Ignore-this: ae4379c3791ba2d73b564bf927367bd9
]
[[build] relaxed some package constraints to make Agda build on ghc-7.7
ulfn at chalmers.se**20131030083832
Ignore-this: f97de5644ef11fe26ddc1ff1a04aa1f9
]
[Refactored checkArguments (use of ifBlockedType, eliminated aux defs).
Andreas Abel <andreas.abel at ifi.lmu.de>**20131108224546
Ignore-this: 12cbe77e12867cdb05e3dc052a8a9318
]
[Issue 731 is fixed: Level primitives needed to display constraints.
Andreas Abel <andreas.abel at ifi.lmu.de>**20131108210451
Ignore-this: 17de05b54a406d3fe52798e1242a2238
]
[[issue 762] fixed impossible issue
ulfn at chalmers.se**20131108080113
Ignore-this: 13555d893726bd8c7012f273d65c3781
- auto still doesn't like open metavariables
]
[Fixed issue 532. open public is now accepted in records even before the last field.
Andreas Abel <andreas.abel at ifi.lmu.de>**20131108141942
Ignore-this: a9f7fdcfbdc7f4b59efa9ec3d96922d1
]
[Fixed issue 899. Instance candidates are now considered module judgmental equality.
Andreas Abel <andreas.abel at ifi.lmu.de>**20131107221853
Ignore-this: 96d35bcf803d120bf89edb53fe3870b3
]
[[Issue 670] Drop parameters of projection(like) functions found by instance search.
Andreas Abel <andreas.abel at ifi.lmu.de>**20131107213701
Ignore-this: b22675a2f9ba9131d1c2aa2b4c8de837
]
[Changed error messages forgotten by patch "Removed commented-out import statements".
Andreas Abel <andreas.abel at ifi.lmu.de>**20131107202248
Ignore-this: cbc3b641afcd4b23da9d6a712cc28744
Yes, even removing commented-out lines can break the test suite!
E.g., fail/ImpossibleTest (my long-term favorite test case)!
]
[Fixed issue 906, 942. When comparing copattern spines in the termination checker, projections appearing earlier in the record are considered smaller wrt. structural ordering.
Andreas Abel <andreas.abel at ifi.lmu.de>**20131107201742
Ignore-this: 3d852043835363ded7309984e078b5ca
This reflects the dependency order.
Needed for defining dependent records by copattern matching.
]
[Removed commented-out import statements, moved some import statements.
Nils Anders Danielsson <nils.anders.danielsson at gmail.com>**20131107135555
Ignore-this: 967dfb7710c2a2b2bb8b62685881bd21
]
[[issue 835] fixed: unsolved constraints now print with range if there is one
ulfn at chalmers.se**20131107141413
Ignore-this: 31f7663a7a537d4b4997a4891ab30e8
]
[[issue 756] fixed: lets and extended lambdas are no longer valid in dot patterns
ulfn at chalmers.se**20131107133455
Ignore-this: f8b739883795290191e27e07e027064f
]
[Restored highlighting of proper projections. Clarifies projection copatterns a lot!
Andreas Abel <andreas.abel at ifi.lmu.de>**20131107163035
Ignore-this: 5dcae99e57cea475cb47bfa884027e13
]
[removed gratuitous line breaks when pretty printing records and extended lambdas
ulfn at chalmers.se**20131107112325
Ignore-this: 93f34c64ae068342b5acef20770f0249
]
[[issue 535] fixed part one
ulfn at chalmers.se**20131107102315
Ignore-this: 3e2bd27d8c16c0d825612671b6719ebf
- make case now uses named implicits to avoid unnecessary implicit arguments
]
[Issue 590: Reverted to the old behaviour.
Nils Anders Danielsson <nils.anders.danielsson at gmail.com>**20131101110026
Ignore-this: c2b2c0aa86d010adabaa4ce39b81a9d8
]
[Changed the way in which records and extended lambdas are printed.
Nils Anders Danielsson <nils.anders.danielsson at gmail.com>**20131030163006
Ignore-this: 2d6cf9953f676916301dc1a2066f0f46
]
[[interaction test] minor update to error message after fix to issue 936
ulfn at chalmers.se**20131106213757
Ignore-this: 7e4d45127ee110cf02cffdfaa5368bcf
]
[[issue 535] changed clause patterns and constructor argument patterns to NamedArgs
ulfn at chalmers.se**20131106213013
Ignore-this: 8ab3a8d0b7202c492d3bf6d484c0f7c7
- this paves the way for pretty printing patterns with named implicit args
]
[Highlighting test cases have changed due to the fix for issue 936.
Andreas Abel <andreas.abel at ifi.lmu.de>**20131106134942
Ignore-this: 3b6025c435cf99d4c4c534824fa6feb3
]
[Fixed issue 940: copatterns in parametrized modules.
Andreas Abel <andreas.abel at ifi.lmu.de>**20131106134747
Ignore-this: 2c7bdecffcb35436c5fbe5d77c5f859c
Projection function was applied to module parameters twice
because of a use of typeOfConst instead of defType <.> getConstInfo.
]
[Less frequent annoying debug messages from reifier.
Andreas Abel <andreas.abel at ifi.lmu.de>**20131106134331
Ignore-this: 667be5ec8b6d11a44795e233f7ac9473
]
[[issue 936] added output for interaction test
ulfn at chalmers.se**20131106103437
Ignore-this: a41b71302c79dc08cf7c2db2dbcbcf67
]
[[issue 936] don't create highlighting info for Agda.Prim
ulfn at chalmers.se**20131106103206
Ignore-this: dbb79041eda31a2efd1ea69261e0680a
]
[Interaction test case for Issue 936. No highlighting should be generated for Agda.Prim.
Andreas Abel <andreas.abel at ifi.lmu.de>**20131106103247
Ignore-this: 5e62efb591eaf3e50ba703692c424306
]
[[issue892] fixed completely
ulfn at chalmers.se**20131106093418
Ignore-this: 1405adfb6b5de5c4603c5cc70ff33850
- the problem was that the scope checker didn't handle
module application properly in the presence of open public
]
[[issue 892] fixed one part of the problem
ulfn at chalmers.se**20131106085729
Ignore-this: ead9f0bc1e5f06eced8df130c8a3fa1d
- make sure the empty name used for the record parameter inside
record modules doesn't leak into the types of the functions
]
[[interaction test] updated output with missing highlighting command
ulfn at chalmers.se**20131106083419
Ignore-this: a1acb8182a1e1cdb9f561c6c18b0f3a7
]
[[interaction test] slight change to regexp for ignoring temp file paths
ulfn at chalmers.se**20131106083308
Ignore-this: ae7fd10294695e35b0b40c825f7e074c
]
[Fixed issue 939: irrelevant projection pattern should put us in irrelevant mode.
Andreas Abel <andreas.abel at ifi.lmu.de>**20131105161416
Ignore-this: b89d7870a085b48da9adfec936b33cb8
Added 'Arg' to the 'clauseType' to keep track
whether we have to check the RHS in irrelevant mode.
Q: Anything todo about dot-patterns here?
]
[Fixed coverage checker for dependent copatterns (related to Issue 937).
Andreas Abel <andreas.abel at ifi.lmu.de>**20131105111322
Ignore-this: e1700b6c15d5e5d9c14b2644a078ca3a
]
[Fixed issue 937: Split on copattern did not apply the function to the free variables of the section.
Andreas Abel <andreas.abel at ifi.lmu.de>**20131105011700
Ignore-this: 5c64a93cd76a6a637c3bca6998e8da97
]
[Slightly nicer debug printing.
Andreas Abel <andreas.abel at ifi.lmu.de>**20131105011514
Ignore-this: 986720388979f3c9b11080b25f72aaec
]
[Commenting: Explanations about definitions living in top-level.
Andreas Abel <andreas.abel at ifi.lmu.de>**20131105011052
Ignore-this: d33125522bd0ecefbd227e7a93386b16
]
[Minor clean up of give in BasicOps.
Andreas Abel <andreas.abel at ifi.lmu.de>**20131105010948
Ignore-this: cbfeeb955ab25fd03454f5994f7dc958
]
[Boilerplate lowerMeta is now instance of generic traversal, and other small refactorings.
Andreas Abel <andreas.abel at ifi.lmu.de>**20131104214835
Ignore-this: a252147dbbe526b5d709a33e9a91affb
]
[Generic traversal for Syntax.Concrete. (Just mapExpr for now.)
Andreas Abel <andreas.abel at ifi.lmu.de>**20131104214645
Ignore-this: af38acb1f7db5ba3f301517269bcb0fd
]
[More pointless refactorings, using <.>.
Andreas Abel <andreas.abel at ifi.lmu.de>**20131104214539
Ignore-this: 4092709ded556e381ae0624ebd925c98
]
[Fewer of these scope debug messages (only from -v 40 now).
Andreas Abel <andreas.abel at ifi.lmu.de>**20131104214447
Ignore-this: fb9c90bf024f7985d0b737bd7c130749
]
[Auxiliary function addClauses.
Andreas Abel <andreas.abel at ifi.lmu.de>**20131104210723
Ignore-this: a3cd52510892a69f2039dd1cf33a60c
]
[Fixed issue 933: glitch in SyntacticEquality.
Andreas Abel <andreas.abel at ifi.lmu.de>**20131103001531
Ignore-this: 847124fe9553cf88c91fbe71853eab33
]
[Now Agda.Prim contains the level primitives and is automatically imported.
Andreas Abel <andreas.abel at ifi.lmu.de>**20131102192052
Ignore-this: e4b5f15beebaf96504b63f497c2424ef
Removed tons duplicate level builtin declarations from the test suite.
A problem remains in interaction/Error-in-imported-module:
An invalid emacs command is created there (with unterminated string).
(agda2-highlight-load-and-delete-action "
I suspect that is because an __IMPOSSIBLE__, indicating a violated invariant,
is swallowed by a too general exception handler (Control.Exception.bracket)
in Agda.Interaction.Highlighting.Emacs.lispifyHighlightingInfo.
Probably an invariant concerning stModuleToSource is broken by my attempt
to fit the auto-import of Agda.Prim in a suitable place in
Agda.Interaction.Imports.
]
[More tests that pattern variables do not shadow constructors, for copatterns and flexible arity.
Andreas Abel <andreas.abel at ifi.lmu.de>**20131102104931
Ignore-this: 1e0dea37d01512e99ebb01dfd266d21b
]
[forMaybe is just flip mapMaybe.
Andreas Abel <andreas.abel at ifi.lmu.de>**20131101182334
Ignore-this: 5f6e3842022493dbc4fd8d3aba35bdf9
]
[Clarified noShadowingOfConstructors code. No need to normalize type!
Andreas Abel <andreas.abel at ifi.lmu.de>**20131101182251
Ignore-this: a5947db148c19b0fa50831956c49d29f
Q: Should that not be checked for record constructors as well?
]
[Cosmetics: separated constructor tools from datatype tools.
Andreas Abel <andreas.abel at ifi.lmu.de>**20131101182055
Ignore-this: eb831ec41192e380c5629595fb24ee76
]
[Pointless refactoring in DisplayForm.hs.
Andreas Abel <andreas.abel at ifi.lmu.de>**20131101175857
Ignore-this: 96f1640a9307e3ff886bfc2c302fe343
]
[ElimView now only reduces projection-like functions.
Andreas Abel <andreas.abel at ifi.lmu.de>**20131101175756
Ignore-this: dce570d9eab10cb0aa75b9a4b0b2dee
This makes checkInternal more faithful, it reduces now
really only projection-like functions, which it needs
for bidirectional type-checking.
]
[Cosmetics: removed commented out code concerning elimView, added comments.
Andreas Abel <andreas.abel at ifi.lmu.de>**20131101170908
Ignore-this: a20492d6d768f4a08aff511166450768
]
[removed unnecessary check from CheckInternal
ulfn at chalmers.se**20131101133156
Ignore-this: 93ac693607651488ee48494b2c58b5e4
]
[[release-notes] documented C-c C-h
ulfn at chalmers.se**20131101094948
Ignore-this: 59304397e3e627a03285b35fb8b50066
]
[removed non-sensical functional dependency
ulfn at chalmers.se**20131101083922
Ignore-this: b69a734567d6fcf61d7b53d51a85bbad
]
[Merged in 2.3.2.2 patches.
Nils Anders Danielsson <nils.anders.danielsson at gmail.com>**20130927202200
Ignore-this: 25d9dd780c50c7d8d3192a85a2614d48
]
[TAG 2.3.2.2
Nils Anders Danielsson <nils.anders.danielsson at gmail.com>**20130927195945
Ignore-this: 6f31e10da86878c3851eb5056ae7bd1
]
[Preparation for release (2.3.2.2).
Nils Anders Danielsson <nils.anders.danielsson at gmail.com>**20130927185638
Ignore-this: 7daf94e79cc11707be3a2493d23b01b5
]
[Fixed a misspelling in Olle Fredriksson's name.
Andreas Abel <andreas.abel at ifi.lmu.de>**20131101105944
Ignore-this: f640091b2be22d9d47b0f9ec4969d895
]
[Fixed issue 930.
Andreas Abel <andreas.abel at ifi.lmu.de>**20131031162734
Ignore-this: ce5ebc2afd84dcc4377159c99d8f77a4
Each of the two things fixes this issue:
* When sort comparison fails but type comparison succeeds,
try sort comparison again instead of throwing the old
sort error.
* Fix sort comparison: pointwise comparison of Max not allowed
if any term contains a meta (could be buried in a neutral level).
]
[Removed superfluous option --universe-polymorphism from two tests.
Andreas Abel <andreas.abel at ifi.lmu.de>**20131031162417
Ignore-this: be75aaf52cc8d8c6abf67dda578ee422
]
[HCAR November 2013.
Andreas Abel <andreas.abel at ifi.lmu.de>**20131031125201
Ignore-this: ad18488a202cf341d88a1ddb0c15578b
]
[Added more author spellings.
Andreas Abel <andreas.abel at ifi.lmu.de>**20131031124921
Ignore-this: d6642b7954bc0b380eec507d417ed34
]
[Removed Resp_MakeCaseAction, which was a special case of Resp_MakeCase.
Nils Anders Danielsson <nils.anders.danielsson at gmail.com>**20131030162357
Ignore-this: 6d437ff557b6fa4e19f61ca1f9aa29b0
+ The Resp_MakeCase constructor's type was also modified.
]
[Fixed issue 590.
Nils Anders Danielsson <nils.anders.danielsson at gmail.com>**20131030162253
Ignore-this: 7d7fab4873dd5eb0aa8b402859f8b091
]
[Added a task to the release procedure.
Nils Anders Danielsson <nils.anders.danielsson at gmail.com>**20130927200839
Ignore-this: 5fdc06d62e426c470ed9ad6d121944bc
]
[Updated the copyright year range.
Nils Anders Danielsson <nils.anders.danielsson at gmail.com>**20130927195920
Ignore-this: f4cafecd4c8adf3a4f687bf3fcaa877e
]
[Release notes for Agda 2.3.2.2.
Nils Anders Danielsson <nils.anders.danielsson at gmail.com>**20130927185432
Ignore-this: fa852bb353bef4989af8a5cbd513be1d
]
[Added some disclaimers to the README.
Nils Anders Danielsson <nils.anders.danielsson at gmail.com>**20130927183935
Ignore-this: 6057f47299e2c2311466bd6a589883b
]
[Renamed GhcTop to EmacsTop.
Nils Anders Danielsson <nils.anders.danielsson at gmail.com>**20131030110343
Ignore-this: a7c6a6d54ef4161c3a2229779f35981a
]
[Added default include dir $HOME/.cabal/share/Agda-x.y.z/lib/prim.
Andreas Abel <andreas.abel at ifi.lmu.de>**20131030201747
Ignore-this: c5cdce4f0f8c606e103769d38cc48b03
The path is communicated to Agda by cabal's generated Paths_Agda module.
Contains an empty module Agda.Prim so far.
Failed test suite machinery deletes the user- and version- specific parts of
this path.
]
[Fixed a broken failed test case (wrong filename instead of intended error).
Andreas Abel <andreas.abel at ifi.lmu.de>**20131030201240
Ignore-this: 4b383e2b21560be5cfcaa32d4e04ae0f
]
[Cosmetics: renamed some identifiers and added a comment.
Andreas Abel <andreas.abel at ifi.lmu.de>**20131030194330
Ignore-this: 3d631a09d7a3c2bb1ffe0fd435a3f556
]
[Refactor: lenses for Options to modify the TCState.
Andreas Abel <andreas.abel at ifi.lmu.de>**20131030192811
Ignore-this: 9a078f12ae5852b31fb8ec5c3ab1e42d
]
[Cosmetics: structured file to separate lenses for different TCState components.
Andreas Abel <andreas.abel at ifi.lmu.de>**20131030160209
Ignore-this: d78dee5fff10e0f12e69b813135c489b
]
[Fixed 2 comments in Syntax.Internal.
Andreas Abel <andreas.abel at ifi.lmu.de>**20131030153503
Ignore-this: ea0c6e51c9697b9c74682e817f2f4e70
]
[Fixed an issue with verbosity not honored before successful load (see also issue 641).
Andreas Abel <andreas.abel at ifi.lmu.de>**20131030153400
Ignore-this: 44ef5ab38e0250df9de2b217ed1fba17
]
[A debug message for inverseScopeLookup.
Andreas Abel <andreas.abel at ifi.lmu.de>**20131029213945
Ignore-this: 436dc22a5c8872da219b3a6105115be7
]
[Tiny code modernization: use of unless, isNothing instead of case-of.
Andreas Abel <andreas.abel at ifi.lmu.de>**20131029195722
Ignore-this: 7738373ecdccf2f082c81f6d33ef2f1e
]
[A debug message on shadowed pattern vars.
Andreas Abel <andreas.abel at ifi.lmu.de>**20131029173548
Ignore-this: a72d381ed3eae08e5877d6e08592476a
]
[Micro-refactoring in AbstractToConcrete.
Andreas Abel <andreas.abel at ifi.lmu.de>**20131029173436
Ignore-this: 1044fddcb52944403c2004209d7a4d1
]
[Fixed issue 927: DontCare no longer impossible in variable linearity analysis in Miller unification.
Andreas Abel <andreas.abel at ifi.lmu.de>**20131029154814
Ignore-this: daf10c0081f29dcbec8870d866005053
]
[Use smart constructor dontCare instead of DontCare consistently.
Andreas Abel <andreas.abel at ifi.lmu.de>**20131029154709
Ignore-this: 5c546e38983b7b93c03cd7c6b68fdc51
]
[Cosmetics: print debug messages in proper context in MetaVars.assignV.
Andreas Abel <andreas.abel at ifi.lmu.de>**20131029154515
Ignore-this: 979eff21c7325860d39b4d2ed2d94b6a
]
[Added commented-out import Common.Level.
Andreas Abel <andreas.abel at ifi.lmu.de>**20131027220328
Ignore-this: ff9f4eb37a7f8b43f3b67ea787b555ea
]
[Fixed broken compilation of Reduce.hs (issue 926) and removed a stupidity in Patterns/Match.hs.
andreas.abel at ifi.lmu.de**20131027195649
Ignore-this: f2b931556f90e9da7a54a35db5e260b
]
[Fixed issue 907. We now reduce with previous function clauses to check the current one.
andreas.abel at ifi.lmu.de**20131027134818
Ignore-this: af21de0785cb80be0541e495520041a3
]
[Refactoring in preparation of issue 907: distinguish function signatures from other type signatures in A.Axiom.
andreas.abel at ifi.lmu.de**20131027132955
Ignore-this: 5be890585cba027608e32fffa561a0df
Now, function signatures are added as empty Functions instead of
Axioms during declaration checking.
This means we can add their function clauses later, one by one.
Detailed change list:
Added FunSig boolean type and an extra such argument to A.Axiom.
Removed three redundant definitions of A.axiomName.
Added emptyFunction as template for Function Definition in Signature.
Refactored a bit in Rules/Data.
]
[Optimization for underapplied redex is wrong for copatterns and functions of flexible arity. Removed.
andreas.abel at ifi.lmu.de**20131027132656
Ignore-this: ab26bc84a912f5aa8eb34c644b982974
]
[Cosmetics: removed excessive indentation in let dataDef.
andreas.abel at ifi.lmu.de**20131027131533
Ignore-this: ae619cdd2dbb02c614261e181c9a2be7
]
[New lens for modifying funClauses in Signature.
andreas.abel at ifi.lmu.de**20131027131350
Ignore-this: 4be2310f75cc0db01acd2185409a6fd4
]
[Refactor: defaultDefn creates Definition with usual defaults.
andreas.abel at ifi.lmu.de**20131027130912
Ignore-this: e2cbdef6d4a1122e6643a49dfe254ece
]
[Removed TypeChecking.RebindClause. This module has been an empty shell for years.
andreas.abel at ifi.lmu.de**20131027130143
Ignore-this: 176142c5b137fe72f3ada0c126605eb0
]
[Small refactoring and documentation of normalization for the purpose of telescope reordering.
andreas.abel at ifi.lmu.de**20131027123710
Ignore-this: 53fd0ec772c5cb7786d21aaa0931c08c
]
[Tiny optimization of getContextTerms.
andreas.abel at ifi.lmu.de**20131027123428
Ignore-this: fdb71039335b1a756e2aa3d241cd1b08
]
[Updated comment for instantiateFull (has been wrong for a long time).
andreas.abel at ifi.lmu.de**20131027123136
Ignore-this: 40a7572a8b309f930bf7c334a71659c
]
[Tiny refactor: moved mlevel to TypeChecking.Level.
andreas.abel at ifi.lmu.de**20131027122934
Ignore-this: ef0b74f148153ee94192da56078027c6
]
[Debug message for looping over terms in termination checker.
andreas.abel at ifi.lmu.de**20131027122751
Ignore-this: f04acf27a52b1bcb494ed950793f7d02
]
[Removed harmful special matching against irrelevant args (has been sleeping for a long time in previously dead code).
andreas.abel at ifi.lmu.de**20131027122512
Ignore-this: fc55b0e02c272219fd2b5e8e7a966ab3
]
[Debug message in Patterns.Match.
andreas.abel at ifi.lmu.de**20131027122328
Ignore-this: 5892bd4f72ec7ad24565a996830673da
]
[Tiny improve: preserve argInfo in Patterns.Match.
andreas.abel at ifi.lmu.de**20131027122150
Ignore-this: 246c210f8e20a3c9f298c21f0d9f4ae5
]
[Tiny refactor: moved (<$) operator (flip ($>)) to Utils.Monad.
andreas.abel at ifi.lmu.de**20131027122008
Ignore-this: b9583f16a333c14f2dcb5ec55d5701c9
]
[Successful test case TerminationOnIrrelevantArgument: whitespace, verbosity options.
andreas.abel at ifi.lmu.de**20131027121401
Ignore-this: bae7aeae101011462f3a31b31c348137
]
[Failed test cases Makefile: reactivated TwoCompilers test case.
andreas.abel at ifi.lmu.de**20131027121218
Ignore-this: 3ee3fdfca1e0e62202d20eba282266ac
]
[Refactor: funCompiled :: Maybe CompiledClauses need for partial function definitions (see Issue 907).
andreas.abel at ifi.lmu.de**20131026131835
Ignore-this: c0dfb7ff6a601fd790a9a42545f6efc9
]
[Tiny refactor: use getBody in Epic.Injection.
andreas.abel at ifi.lmu.de**20131026123619
Ignore-this: b0a17936b0060e100eae87ac6f08bbc4
]
[Tiny refactor: use getBody in Reduce.hs.
andreas.abel at ifi.lmu.de**20131026123402
Ignore-this: 57dd226d2cfb02dbf04d51434060f7f5
]
[Cosmetics: cleaned import list in Reduce.hs.
andreas.abel at ifi.lmu.de**20131026123228
Ignore-this: c9aada8796e67bc9cf2f4631483c481c
]
[Tiny refactor: 'for' for functors and a use in Injectivity.
andreas.abel at ifi.lmu.de**20131026122427
Ignore-this: a015d94bd7e8ad18f557b62601ed3cfa
]
[Cosmetics: indentation in Reduce.app
andreas.abel at ifi.lmu.de**20131026121545
Ignore-this: 1b53f2f07b360e2f1e93239e446d4506
]
[Cosmetics: removed long retired code.
andreas.abel at ifi.lmu.de**20131026121504
Ignore-this: 6e8dbd99cb900f3491093398dbf4060b
]
[Small refactor: new function getBody for clause bodies, use in Injectivity.
andreas.abel at ifi.lmu.de**20131026121053
Ignore-this: 45cc9c21f8e02ffceaabf88b3b6d8b8f
]
[Cosmetics: some section headings in Substitute.hs
andreas.abel at ifi.lmu.de**20131026120941
Ignore-this: 91f8bfeec8ecd939bee47e4cfe91057b
]
[Proper error message when function type is eliminated by a projection copattern.
andreas.abel at ifi.lmu.de**20131026100258
Ignore-this: bfa61ea4dcc2b077b1b0e03cdf3b7320
]
[Cosmetics: removal of excessive indentation.
andreas.abel at ifi.lmu.de**20131026090018
Ignore-this: a8a813f8b7e468abfcad1e6355b88b99
]
[Issue 790 is fixed.
andreas.abel at ifi.lmu.de**20131025231708
Ignore-this: fbde85194f38b22dc1ecf6e8b68c965e
]
[Original test case for Issue 920 by Jesper Cockx.
andreas.abel at ifi.lmu.de**20131025224203
Ignore-this: 8101bf83e0543489d96f569628bf1e0a
]
[Fixed issue 920. Non-linear variables can be attempted to be pruned, but not more.
andreas.abel at ifi.lmu.de**20131025223249
Ignore-this: 7f3d3063570b6c5d6688529a3993f999
]
[Mostly cosmetic restructuring in assignV; use subst instead of abs followed by app.
andreas.abel at ifi.lmu.de**20131025213946
Ignore-this: 79bf19f0dcc516d133a47ac983515ba4
]
[Attempted to install double-checking of meta solutions.
andreas.abel at ifi.lmu.de**20131025213740
Ignore-this: c93feb3553fca081edd7a69eb5d80e3b
Failed because sort metas have inaccurate type.
TODO: clean up sort metas. (Larger refactoring, I guess.)
]
[Fixed issue 924 (never ending normalization in unifier).
andreas.abel at ifi.lmu.de**20131024191416
Ignore-this: b88d96e1d145cdcdcb73f3f33961ae4d
Normalization is now only invoked when unifyAtom is inconclusive.
(Normalization is needed for eta-contraction of flexible vars,
see issue 423).
]
[Issue 893 is fixed by checking with-function-types in internal syntax.
andreas.abel at ifi.lmu.de**20131022195921
Ignore-this: 6cb9e928423d0323fc33ad9068828484
]
[Cosmetics in Coverage.hs: recTel is unused.
andreas.abel at ifi.lmu.de**20131022194624
Ignore-this: 2e35abf725785420dd000a1f9111f253
]
[Using the bidirectional checker for With function types.
andreas.abel at ifi.lmu.de**20131022194501
Ignore-this: 9d85b111cb4ef22e94c2985fa3b5aabe
]
[A bidirectional type checker for Syntax.Internal.
andreas.abel at ifi.lmu.de**20131022194212
Ignore-this: 301b7734aa996fdf1763be6ae03248a0
]
[Made I.Type a functor and fixed unbound dB indices in an error message about bad overloaded constructors.
andreas.abel at ifi.lmu.de**20131022194049
Ignore-this: d46db83284d420e636475fbcc825c047
]
[Factored out getDefType to get type of possibly projection-like function applied to the parameters; added applyDef to apply a projection(like) to its first argument.
andreas.abel at ifi.lmu.de**20131022192338
Ignore-this: e74b4476b2144db922fc4ec3071642fc
]
[Tiny refactor: moved name Suggest class to Internal.hs.
andreas.abel at ifi.lmu.de**20131022191820
Ignore-this: 9e81bd7d9833f73a299822ef7e8b3ac2
]
[Factored out a test to tell whether a Def is eligible as type of the principle argument of a projection-like function.
andreas.abel at ifi.lmu.de**20131022191245
Ignore-this: a4ed56553f771f7570e080179b97e323
]
[Factored out getConType to get the type of a constructor applied to the parameters.
andreas.abel at ifi.lmu.de**20131022190847
Ignore-this: e66898189ad9ce3af85a069829826ebe
]
[Documented in Signature.hs that a projection has to cease being one after the record argument has been applied.
andreas.abel at ifi.lmu.de**20131022190409
Ignore-this: ea40b4ce052a39806ed7c6a9428990c1
]
[Cosmetics: some cleanup in Signature.hs (reformatting, deleting of long-retired funs).
andreas.abel at ifi.lmu.de**20131022185909
Ignore-this: f2bc47f52e6b52a1726d3c9dbedd75c4
]
[Some comments added to Rules/Record.hs and Monad/Base.hs to track the addition of record parameters to the field telescope.
andreas.abel at ifi.lmu.de**20131022185649
Ignore-this: 4027b7d6fcd8373b8abddcc904420880
]
[Another, larger testcase for With from the std-lib.
andreas.abel at ifi.lmu.de**20131022183658
Ignore-this: 7c6258c8a1faaba6917c93bae52f5835
]
[A test case for With extracted from std-lib.
andreas.abel at ifi.lmu.de**20131022183553
Ignore-this: 2e4b09c663dd9491fdfb40dd4fb9cb8a
]
[Rolled back addition of ignoreSorts.
andreas.abel at ifi.lmu.de**20131022182816
Ignore-this: b0e5ef14961bb4d194beb00967bddf4d
]
[Added ignoreSorts and envIgnoreSorts to ignore sorts during conversion checking. Did not do the job, however.
andreas.abel at ifi.lmu.de**20131022182534
Ignore-this: 4cd6dfffe6deee59001e8e4e3dc49b0d
]
[Tiny refactor: levelType to get primLevel as a Type.
andreas.abel at ifi.lmu.de**20131022182113
Ignore-this: 1e420e0c315f0b9e157ab9bdb59d640f
]
[Tiny: fixed capitalization in error message about wrong constructor.
andreas.abel at ifi.lmu.de**20131022181904
Ignore-this: e7de5a4c41fdd9fa090b840b73c48d24
]
[In Common.hs, zapped some retired code and added defaultDom.
andreas.abel at ifi.lmu.de**20131022175957
Ignore-this: 63f22c7db8cca1c9e86e116ccd8a4342
]
[Added import Level to some test cases to print debug messages.
andreas.abel at ifi.lmu.de**20131022175722
Ignore-this: 9676719e2bd358a0bc2c559d0c679521
]
[The test case for issue 921 is actually a failing one.
andreas.abel at ifi.lmu.de**20131022175619
Ignore-this: d85a1b8c6a7792b387f18e9972ef9205
]
[Fixed a long-sleeping bug in Builtin.hs. NATEQUALS result was checked against Nat instead of Bool.
andreas.abel at ifi.lmu.de**20131022174042
Ignore-this: 310b6c3118db8f2256cf0d066049cd1b
]
[Issue 901 is fixed by eta-expanding projected metas.
andreas.abel at ifi.lmu.de**20131021205103
Ignore-this: 7d2e555abc1017fe8a1fdc124e6d3ca2
]
[Fixed issue 922. Instance search for unused/irrelevant metas was started in wrong context.
andreas.abel at ifi.lmu.de**20131021202551
Ignore-this: 18800b6ae7fc53880802017f2ec981cd
]
[Inessential changes to Copatterns testcase.
andreas.abel at ifi.lmu.de**20131020181119
Ignore-this: 968de22acf4d24f0f8802b85cc43bf57
]
[Fixed a problem with duplicate DontCare constructors related to irrelevant projections.
andreas.abel at ifi.lmu.de**20131020173646
Ignore-this: 1611ca7234a31c0f008eb43d1bd24c44
]
[Fixed the displayform problem caused by the big Elims refactoring.
andreas.abel at ifi.lmu.de**20131020172030
Ignore-this: a57ea5d19ab4c530c3f8791bed330731
]
[Fixed issue 921. Non-reducing definitions (blocked by failed termination check) yielded an impossible situation.
andreas.abel at ifi.lmu.de**20131020170107
Ignore-this: bb9c74a718b34bcfc7379cb46fd3fc35
]
[After Elims refactor, fixed a problem in with-abstraction and one with irrelevant projections.
andreas.abel at ifi.lmu.de**20131020155250
Ignore-this: f8bf841b5ba37369ee047166a0c327db
]
[Refactor: Added projDropPars and original projection name to Projection.
andreas.abel at ifi.lmu.de**20131020100535
Ignore-this: 1970118bb16ba434d8302e43d2c7a4c8
This is part of the big spine representation refactoring.
Issues with display forms remain.
Also, I discovered a bug introduced by short-cut projection reductions,
which does not respect irrelevance (Issue543a).
]
[Refactor: I.ConP now also carries ConHead instead of QName.
andreas.abel at ifi.lmu.de**20131019131820
Ignore-this: 1669cf83b221864db5ff2dfc264c0535
]
[Big refactoring: internal syntax in spine form.
andreas.abel at ifi.lmu.de**20131019114605
Ignore-this: b7306bcc42e353f2f6685a578755da52
]
[Fixed issue 918 (internal error triggered by termination checker).
andreas.abel at ifi.lmu.de**20131014185429
Ignore-this: c301b4b054087449cd6bad9193220413
]
[Removed trailing implicit insertion in Def.hs. This fixes issue 919.
andreas.abel at ifi.lmu.de**20131013135133
Ignore-this: daa5e4a5b474e541b948fec97e89dca
]
[Termination checker now moves hidden lambdas to lhs (used for copatterns).
andreas.abel at ifi.lmu.de**20131012044326
Ignore-this: 79a6d7baf34fc3d7516a0e3bf66151a5
]
[Make trailing implicit insertion do nothing for copatterns (see Def.hs).
andreas.abel at ifi.lmu.de**20131002115736
Ignore-this: 30f0c395e097a2650b1c38b47eded21d
]
[changed shortcut for helper function to C-c C-h and cleaned up names a bit
ulfn at chalmers.se**20130925144404
Ignore-this: b31a2605c93281a4018ee30ff19dfae
]
[allow implicit arguments to created helper functions
ulfn at chalmers.se**20130925143957
Ignore-this: 2b727ba6fa50a7452b0359e95aab3d8d
]
[omit types that can be inferred (print as forall) when printing helper function type
ulfn at chalmers.se**20130924115928
Ignore-this: 7fc4107b4ea1f9b16552b4bfdaa4aeef
]
[copy type signature to kill-ring in helper function command
ulfn at chalmers.se**20130924104710
Ignore-this: 466ae606b829b916197d738d06a4585d
]
[added a command to generate the type signature for a helper function
ulfn at chalmers.se**20130923141405
Ignore-this: 5808e57eba824424b1085ae8455a41b0
- currently C-c C-j
- writing f e1 .. en in a hole will (try to) generate a type signature for a
function f such that f e1 .. en would be accepted in the hole.
]
[Fixed issue 911.
Nils Anders Danielsson <nils.anders.danielsson at gmail.com>**20130923161210
Ignore-this: 59d4a9f85cdf84deb9566c125844103d
]
[Support for Alex 3.1.*.
Andrés Sicard-Ramírez <andres.sicard.ramirez at gmail.com>**20130918221708
Ignore-this: ea707fef36878c266beea0d482c84a9c
]
[[term] Removed a TODO note.
Nils Anders Danielsson <nils.anders.danielsson at gmail.com>**20130919102345
Ignore-this: 7ea73240bdf34416567e9c99da8d4c16
]
[[term] Partial support for J and refl.
Nils Anders Danielsson <nils.anders.danielsson at gmail.com>**20130918160143
Ignore-this: 493cad1f2b8485bc846f7428eb39d2c
]
[[term] Modified an error message.
Nils Anders Danielsson <nils.anders.danielsson at gmail.com>**20130918161556
Ignore-this: 4742b6f6e75a19839292223533dc2cd6
]
[[term] Added some code.
Nils Anders Danielsson <nils.anders.danielsson at gmail.com>**20130918161259
Ignore-this: 51d699ea0fe9bac6553cac8ed570e20
]
[Restored test removed by Andreas.
Nils Anders Danielsson <nils.anders.danielsson at gmail.com>**20130918160843
Ignore-this: e852ad2ea4880dafbb80ee25a92db729
]
[[term] Fixed bug in checking rule for lambda.
Nils Anders Danielsson <nils.anders.danielsson at gmail.com>**20130918160129
Ignore-this: e80ff4f4da69e00a82bbf4f4c7e27e6e
]
[[term] Fixed bug in pretty-printer.
Nils Anders Danielsson <nils.anders.danielsson at gmail.com>**20130918140756
Ignore-this: 160a6d0ded890e4f48c348af2ee4299c
]
[[term] Fixed bug in checking rule for lambda.
Nils Anders Danielsson <nils.anders.danielsson at gmail.com>**20130918114145
Ignore-this: d883c5ca342a0f73e325ff9b1c2ab02e
]
[[term] Removed K.
Nils Anders Danielsson <nils.anders.danielsson at gmail.com>**20130918095324
Ignore-this: dc0e4d77e561319ed8a20e6638c6c3a5
]
[Fixed Issue637.out.
Andreas Abel <andreas.abel at ifi.lmu.de>**20130918100338
Ignore-this: 8b2bd5377f9896245439ae429d6a09ef
]
[Removed verbosity from some tests.
Andreas Abel <andreas.abel at ifi.lmu.de>**20130918100306
Ignore-this: 3cfe8a609fc8df5161b9f90d22e60758
]
[Tiny code simplification in LHS.Implicit.
Andreas Abel <andreas.abel at ifi.lmu.de>**20130918100216
Ignore-this: a3b309998bb8a09df67b3748f4090209
]
[Copatterns in internal syntax.
Andreas Abel <andreas.abel at ifi.lmu.de>**20130918100128
Ignore-this: 7463dea4a469ec14528c888464374bf1
Release notes and initial work for With.
Unsupported yet: With, Auto, Compilers.
]
[A debug message for eta record in Conversion.
Andreas Abel <andreas.abel at ifi.lmu.de>**20130917101541
Ignore-this: 6fa6a78d89c1b8cdde6dcbb53790bed2
]
[Fixity for <.> in Utils.Monad.
Andreas Abel <andreas.abel at ifi.lmu.de>**20130917101455
Ignore-this: dcb29ac0bab1008619a89ef64f922738
]
[Added a comment to Internal.ConP.
Andreas Abel <andreas.abel at ifi.lmu.de>**20130917101406
Ignore-this: 6e864415017c7431c1393c7ff7ed837
]
[Refactor: put spineToLhs into a type class.
Andreas Abel <andreas.abel at ifi.lmu.de>**20130917101319
Ignore-this: 8750fdda88f637d0cbc5d390078947a3
]
[Better error message when lhs gives too many arguments.
Andreas Abel <andreas.abel at ifi.lmu.de>**20130916095042
Ignore-this: 1f28f3292de35d5aad1463dea2ca69e3
]
[Copatterns: raise error if record field (open R r) is used in copattern instead of projection.
Andreas Abel <andreas.abel at ifi.lmu.de>**20130913051813
Ignore-this: fc8355e8c018e045f86c37803689cd33
]
[Some things work now with copatterns.
Andreas Abel <andreas.abel at ifi.lmu.de>**20130712142237
Ignore-this: da6e6fcddaee52ca1a18378a39fdb23e
TODO:
* fix termination checker
* make traling hidden arguments and copatterns work together
* fix compilers
* with
]
[Copatterns in Internal syntax (incomplete, breaks --copattern tests from suite)
Andreas Abel <andreas.abel at ifi.lmu.de>**20130706102551
Ignore-this: f9294857c2b7facd255b58f330bab158
]
[[term] Fixed bug in substs.
Nils Anders Danielsson <nils.anders.danielsson at gmail.com>**20130918094803
Ignore-this: eb6e7aaa533a9b23d9b3843e24603528
]
[[term] Tried to fix bug in evaluator.
Nils Anders Danielsson <nils.anders.danielsson at gmail.com>**20130918094141
Ignore-this: aa3c5bcceac7346172fb1904fe4d2c27
]
[[term] Generalised bang, replaced all uses of (!!) with bang.
Nils Anders Danielsson <nils.anders.danielsson at gmail.com>**20130918093848
Ignore-this: fe301c39a5aabbac73ecd7e08cfb47b
+ The function bang now supports infinite lists.
]
[[term] Modified the treatment of blocking in the checking rule for lambdas.
Nils Anders Danielsson <nils.anders.danielsson at gmail.com>**20130918090839
Ignore-this: 7dc05194497f2eede272e5b75fb9c941
]
[[term] Made the evaluator (whnf) more complete.
Nils Anders Danielsson <nils.anders.danielsson at gmail.com>**20130918085412
Ignore-this: f46792a859d374e08091bf9a58a6d03a
]
[[term] Added checking rule for projection applications.
Nils Anders Danielsson <nils.anders.danielsson at gmail.com>**20130918081128
Ignore-this: ab3c0ce8ece1497bb502897f098d4e8a
]
[[term] Noted some problems.
Nils Anders Danielsson <nils.anders.danielsson at gmail.com>**20130918073504
Ignore-this: 38f9063f19421f787168be5f0f17ecf5
]
[[term] Refactoring: Turned isApply into a top-level function.
Nils Anders Danielsson <nils.anders.danielsson at gmail.com>**20130918071853
Ignore-this: 6aa8ed8d478ff438f2a541b9603342ed
]
[[term] Partial support for checking lambdas.
Nils Anders Danielsson <nils.anders.danielsson at gmail.com>**20130918064740
Ignore-this: 9e2ebf4244d97847ec8cfa2aeb484a9
]
[[term] Added var :: Var -> TermView.
Nils Anders Danielsson <nils.anders.danielsson at gmail.com>**20130918065054
Ignore-this: b7d03d0389b102f8f11e154d2c4456a5
]
[Turned off eta-contraction that results in partially applied record constructors.
andreas.abel at ifi.lmu.de**20130918053847
Ignore-this: 7887879cc52c6eb52e6e09b50580acd1
For instance, \ y -> x , y is no longer contracted to _,_ x.
Should we do this also for data constructors?
Like no longer contracting \ y -> suc y to suc?
]
[Inessential: Haddock for Syntax.Internal.conFields extended.
andreas.abel at ifi.lmu.de**20130918053648
Ignore-this: 6b3af97a80ea44618eb482c230b5e4fc
]
[Fixed issue 889: Miller pattern unification extension works only for fully applied record constructors (full application was not checked).
andreas.abel at ifi.lmu.de**20130917154313
Ignore-this: 78172095d1f9cbf69331ba66b35ab39c
]
[[term] Partial bug-fix: Infinite loop due to self-instantiation.
Nils Anders Danielsson <nils.anders.danielsson at gmail.com>**20130917222148
Ignore-this: 611cfacc40428681d2330b357b874b03
]
[[term] Added TODO note.
Nils Anders Danielsson <nils.anders.danielsson at gmail.com>**20130917221726
Ignore-this: bf7ae58c84dc2a56682edecdeaed5e1d
]
[[term] Inference rule for the equality type.
Nils Anders Danielsson <nils.anders.danielsson at gmail.com>**20130917215108
Ignore-this: de8d1b0f086bcb40f207069109a1258d
]
[[term] Added some Show instances.
Nils Anders Danielsson <nils.anders.danielsson at gmail.com>**20130917214053
Ignore-this: f203bfb6fe9c80d57b23c983e45a3eb3
]
[[term] Bug fix: Number of args now checked after insertion of implicit args.
Nils Anders Danielsson <nils.anders.danielsson at gmail.com>**20130917212350
Ignore-this: 1a575570b68b58d27beb682c81d643e7
]
[[term] Fixed another substitution bug.
Nils Anders Danielsson <nils.anders.danielsson at gmail.com>**20130917210912
Ignore-this: a6f68e9121ec87f69f99f70106f418c3
]
[[term] Fixed bug by switching to parallel substitutions.
Nils Anders Danielsson <nils.anders.danielsson at gmail.com>**20130917205737
Ignore-this: 202b0ddc2d31ffd6cda3d6661d69ddc2
+ The previous substitution-related bug "fix" wasn't correct.
]
[[term] Pattern matching is now only allowed for /data/ constructors.
Nils Anders Danielsson <nils.anders.danielsson at gmail.com>**20130917193721
Ignore-this: 10a18aeaa838eae018580a64ddcfc99e
]
[[term] Added Show instances for Clause and Definition.
Nils Anders Danielsson <nils.anders.danielsson at gmail.com>**20130917185726
Ignore-this: 5dcb0f87983290112fdf94deaaf5dcdb
]
[[term] Made the scope checker stricter.
Nils Anders Danielsson <nils.anders.danielsson at gmail.com>**20130917185151
Ignore-this: 33478a2262179506029cd7f5ad83d0ad
+ The scope checker now ensures that constructors are fully applied,
and that constructor type signatures end with the data type applied
to its parameters.
]
[[term] Added Eq instance for Expr.
Nils Anders Danielsson <nils.anders.danielsson at gmail.com>**20130917173019
Ignore-this: 6ced323febf9d1eaea6b4489271ef80b
]
[[term] Fixed bug in substsTerm.
Nils Anders Danielsson <nils.anders.danielsson at gmail.com>**20130917163456
Ignore-this: b6966c824177839c9146eed2318b84cd
+ This bug was tracked down together with Andreas Abel.
]
[[term] Added Show instance for Tel.
Nils Anders Danielsson <nils.anders.danielsson at gmail.com>**20130917163345
Ignore-this: d54bf1bff7c4878b622ced241ec79c36
]
[[term] Fixed bug: Added missing module header.
Nils Anders Danielsson <nils.anders.danielsson at gmail.com>**20130917154357
Ignore-this: 8c4687c542fd387e66f8b2ba76199bf2
]
[[term] Implemented "Set = Set".
Nils Anders Danielsson <nils.anders.danielsson at gmail.com>**20130917154239
Ignore-this: a54d9b531e91d4a8f51cdea2acad5829
]
[[term] Implemented checkRec.
Nils Anders Danielsson <nils.anders.danielsson at gmail.com>**20130917153444
Ignore-this: d0b6752cb4345972447c1571620f29b4
+ This and some preceding patches were implemented together with
Andreas Abel.
]
[[term] Added field names to the TypeSig type.
Nils Anders Danielsson <nils.anders.danielsson at gmail.com>**20130917153037
Ignore-this: 901730200cd06e1bd92e71d85b4693d7
]
[[term] Added Subst and Weaken instances for Telescope.
Nils Anders Danielsson <nils.anders.danielsson at gmail.com>**20130917152807
Ignore-this: 2580d074ef628dc5edec344010383a87
]
[[term] Made absApply more general.
Nils Anders Danielsson <nils.anders.danielsson at gmail.com>**20130917152738
Ignore-this: 9ba47c20d79b20eea4dd526fffaadfdb
]
[[term] Cosmetic changes.
Nils Anders Danielsson <nils.anders.danielsson at gmail.com>**20130917152710
Ignore-this: d8fa7f01d32d0ce4e70a2f019a0d06e3
]
[[term] Added the Substs class, removed substTel.
Nils Anders Danielsson <nils.anders.danielsson at gmail.com>**20130917152640
Ignore-this: 40bffc2032f677913351d94bb6c8abd3
]
[[term] Tried to fix a bug.
Nils Anders Danielsson <nils.anders.danielsson at gmail.com>**20130917151620
Ignore-this: 8b1835755c54b7ba14f941dcc341cfe
+ When a constructor was added the wrong telescope was saved.
]
[Fixed issue 903: possible IMPOSSIBLE in meta assignment.
andreas.abel at ifi.lmu.de**20130917112929
Ignore-this: b1fab163f1a22048557708a13502d4c3
]
[Tried to fix issue 873.
Nils Anders Danielsson <nils.anders.danielsson at gmail.com>**20130917103833
Ignore-this: d561a1b7b2b22d7041835ade25c0d629
]
[Fixed whitespace issues.
Nils Anders Danielsson <nils.anders.danielsson at gmail.com>**20130917095913
Ignore-this: ef75ab648b4cae918df9c2862edfc6bf
]
[Fix the remaining bug of issue 848
guillaume.brunerie at gmail.com**20130917093731
Ignore-this: 9fef28b69e959d18d67b8874053915e4
The previous fix of issue 848 did not allow having several (or nested) anonymous
where modules (because the module was actually called "_"). Now a fresh name is
generated.
]
[Added a comment.
Nils Anders Danielsson <nils.anders.danielsson at gmail.com>**20130917095324
Ignore-this: bfa72729a0396df635eaf7de64d8b0ac
]
[Test case for issue 902.
Nils Anders Danielsson <nils.anders.danielsson at gmail.com>**20130917095205
Ignore-this: 18ff3c5da4354dca0dfbbf826fe26cb4
]
[fix printing of module applications
Andrea Vezzosi <sanzhiyan at gmail.com>**20130916191852
Ignore-this: 21858a2f7040afbaba3fbf64d17f0723
]
[Test case for issue 898.
Nils Anders Danielsson <nils.anders.danielsson at gmail.com>**20130917093211
Ignore-this: 906a9203cd1e350171f92dbdf5af062c
]
[Fix printing of extended lambdas starting with an hidden argument
Andrea Vezzosi <sanzhiyan at gmail.com>**20130908041241
Ignore-this: c18cd4fb7764addd7b90f3eac0228d41
]
[[term] simple equality check include meta instantiation
ulfn at chalmers.se**20130917094032
Ignore-this: a1c61221a37cc5fbb6c8488260a6d071
]
[[term] fixed bug with src locations in scope checker
ulfn at chalmers.se**20130917074329
Ignore-this: 211f1bb446f8bf017bfa6c5813ed41ff
]
[[term] start on type checker with simple deBruijn term representation
ulfn at chalmers.se**20130917074227
Ignore-this: 3e7f27416eee7486e60a9d99aba57e37
]
[[term] cpp'ing different implementations
ulfn at chalmers.se**20130916070558
Ignore-this: fd3422781eb5d5fdca0a3e963555a177
]
[[term] replaced funky unicode arrow-on-top with 's
ulfn at chalmers.se**20130916070527
Ignore-this: e8f6b8bd57fa4a7190c3c507c47e778a
]
[A performance issue was fixed in hashable 1.2.1.0.
Andrés Sicard-Ramírez <andres.sicard.ramirez at gmail.com>**20130916111435
Ignore-this: c22bad5fb7721c1cb44b7881d8e9c5d5
]
[Removed unnecessary import in Context.hs, to please the precise-imports-Nazi.
andreas.abel at ifi.lmu.de**20130915100136
Ignore-this: a7cdfa9277f75c7a424f3311b1ae3d83
]
[Fixed two more ill-scoped debug messages in Record.hs.
Andreas Abel <andreas.abel at ifi.lmu.de>**20130915093204
Ignore-this: 43c45075bf0816bec188ac8cbd1e9c36
]
[Language change: Module parameters are now hidden in the types of projections.
Andreas Abel <andreas.abel at ifi.lmu.de>**20130915091429
Ignore-this: 2740a9b6ee74276f63e6e0ec8d20bffb
]
[Fixed scope for printing debug messages in top (empty) context.
Andreas Abel <andreas.abel at ifi.lmu.de>**20130913152244
Ignore-this: 9ebadf4d07212d03a899d0161aef293
]
[Inessential: a more detailed debug message.
Andreas Abel <andreas.abel at ifi.lmu.de>**20130912210602
Ignore-this: ce18406296a6eeb2bbeb210d5aebc768
]
[Some benchmark runs on Andreas laptops.
Andreas Abel <andreas.abel at ifi.lmu.de>**20130615113046
Ignore-this: 56fccb83791cfb207dfe68d64be3c20c
]
[More examples.
Nils Anders Danielsson <nils.anders.danielsson at gmail.com>**20130913200752
Ignore-this: 64760303e4a9be7b0d36f944a4ecb3d5
]
[Added some examples.
Nils Anders Danielsson <nils.anders.danielsson at gmail.com>**20130913155843
Ignore-this: 33f051c9cc0785845974dce7f40855b4
]
[[term] added an Agda prelude to allow examples to be checked by Agda
ulfn at chalmers.se**20130913145105
Ignore-this: 17fb7bc4edc74c29dab4576e264613b4
]
[[term] allow _ and ' in names
ulfn at chalmers.se**20130913145047
Ignore-this: 804d65a89a9151a265d32a1d0c8c1d22
]
[[term] added postulate syntax
ulfn at chalmers.se**20130913144840
Ignore-this: bfe0ec6943e3989e422deab0172e1e75
]
[[term] added Sigma and True to Basic example
ulfn at chalmers.se**20130913144029
Ignore-this: 48caed732076710e0ed868577c0ec4f3
]
[[term] fixed bad scope checking of dependent records
ulfn at chalmers.se**20130913143906
Ignore-this: b0d3e2bf9173794f46a3dee16bb04bb6
]
[[term] silly bug in grammar
ulfn at chalmers.se**20130913143847
Ignore-this: 234b6ea8b68963722d9499b7d94e622d
]
[[term] allow record with no fields
ulfn at chalmers.se**20130913142942
Ignore-this: cdf878d6047d03e3f13528cdd397ff38
]
[[term] top-level module and optional imports
ulfn at chalmers.se**20130913142857
Ignore-this: 5c07df61ff6e05dc46ef5e338b790a38
]
[Added a rough, incomplete sketch of the language.
Nils Anders Danielsson <nils.anders.danielsson at gmail.com>**20130913142011
Ignore-this: 609dd49ee960f4d94e25ab5a3446023f
]
[Fixed/detected messages are now sent to stderr.
Nils Anders Danielsson <nils.anders.danielsson at gmail.com>**20130913141235
Ignore-this: d106bfb6ea54fa5d38b8f76664ed358c
]
[[term] fail if dist doesn't exist after creating it
ulfn at chalmers.se**20130913141816
Ignore-this: 5179ccdf1fc60e54481eb47a3383a1ad
]
[[term] create the dist directory if it doesn't exist
ulfn at chalmers.se**20130913141645
Ignore-this: 11761b9593bbed3affa6db64788fa04c
]
[[term] fixed whitespace
ulfn at chalmers.se**20130913141032
Ignore-this: 3337906c32ca437e0d0dadd6a621f224
]
[[term] fixed bug in implicit argument insertion
ulfn at chalmers.se**20130913140930
Ignore-this: dc2ac21ffb01a91a24a0f2bb0ad79540
]
[[term] pretty printing abstract syntax
ulfn at chalmers.se**20130913133746
Ignore-this: aff93e172209f5ba3baee4f01019161a
]
[[term] scope checking
ulfn at chalmers.se**20130913124336
Ignore-this: c170cfd443b1e2be1a09614fe5337f47
]
[[term] also (x : A) (y : B) -> C
ulfn at chalmers.se**20130912142301
Ignore-this: 75c6d0037f1ca1e0c59daeb509c5495
]
[[term] relaxed syntax for telescopes: (x y z : A)
ulfn at chalmers.se**20130912142109
Ignore-this: 3c30795e40f138b111a696ec35708eb3
]
[[term] workaround bnfc silliness
ulfn at chalmers.se**20130912140004
Ignore-this: dfc5f4bb1e26eb7b9637a295d65c848d
]
[[term] more complete syntax
ulfn at chalmers.se**20130912135930
Ignore-this: a0c9f44f4afed94e221f0b45439820de
]
[[term] fixed bug in bnfc layout handling
ulfn at chalmers.se**20130912135842
Ignore-this: 5c69cd2aa873d2f5199af156382324cb
]
[[term] natural number example
ulfn at chalmers.se**20130912125410
Ignore-this: b1241d1ac246c686d8dee53a94d0e4a8
]
[[term] first approximation of syntax
ulfn at chalmers.se**20130912124159
Ignore-this: ab69fd29c5535bbf2696c2bc391c1f13
]
[benchmark run
ulfn at chalmers.se**20130902144603
Ignore-this: 46029692b2a0b4249d85d77bcb19ca11
]
[Directory for yet another term representation prototype.
Nils Anders Danielsson <nils.anders.danielsson at gmail.com>**20130912124051
Ignore-this: 74be9fae5c0f07bf7bc72eb4a253171e
]
[[test] changed interaction test for issue 637 to force the stack overflow to happen in actual type checking
ulfn at chalmers.se**20130902142911
Ignore-this: 3f32bad588161e69225439d214e15630
- setting the stack to 8 bytes resulted in stack overflow before reaching the
exception handler for me
- upped the stack size to 1000 bytes and changed example to check that sum [1..100] == 5050, which
requires some actual stack
]
[[test] generic cleanup for tests using compiler
ulfn at chalmers.se**20130902095327
Ignore-this: c267d0db97311b752ee16e08bccb5bf3
]
[[test] removed verbosity from a couple of tests
ulfn at chalmers.se**20130902095255
Ignore-this: b1bdc72a3f04e955c3ab498527835d71
]
[Reverted to the old --without-K semantics.
Nils Anders Danielsson <nils.anders.danielsson at gmail.com>**20130829143124
Ignore-this: 76356e6df20f0eaba19e514aa9aecda0
]
[Added --without-K fail tests.
Andrés Sicard-Ramírez <andres.sicard.ramirez at gmail.com>**20130726204930
Ignore-this: 3eb0edb38097387f5e1a87180acabd97
]
[Fixed issue 681.
Nils Anders Danielsson <nils.anders.danielsson at gmail.com>**20130821153116
Ignore-this: c1a28ab27de4721ecc7e966717cd7de8
]
[Added support for haskell-src-exts 1.14.0.
Nils Anders Danielsson <nils.anders.danielsson at gmail.com>**20130820091850
Ignore-this: 1140b3f5b75d7c3ced5fa266e8bc2e88
]
[Fixed issue 882. primTrustMe weaker now, only reduces to refl if its arguments are beta-iota-equal.
andreas.abel at ifi.lmu.de**20130722132318
Ignore-this: 49eb00d985b38e7fb750351377556a09
]
[Allowed more versions of hashtables.
Andrés Sicard-Ramírez <andres.sicard.ramirez at gmail.com>**20130711223723
Ignore-this: 90fd751b69aeb33be40b10b1642c562a
]
[Fixed issue 877.
Andrés Sicard-Ramírez <andres.sicard.ramirez at gmail.com>**20130711162144
Ignore-this: 4fa54da0b398407435b422faf292d03
]
[Cosmetic changes in Substitute.hs.
andreas.abel at ifi.lmu.de**20130711195122
Ignore-this: ddb3cf086a2b1adc25146ba0d7c686cc
]
[Fixed issue 856: Agda reported conversion error when postponing could still make the necessary eta-law available.
andreas.abel at ifi.lmu.de**20130711194800
Ignore-this: 1e0cca9b5d7642dead54d4fb6d704403
]
[Restrict to hashable-1.1.x to prevent later versions which make Agda library-test 10x slower.
andreas.abel at ifi.lmu.de**20130711193301
Ignore-this: a4c686ed2b8e1b6b0238ef1ff63aa128
Performance bug confirmed on ghc-7.4.1 with hashable-1.2.0.10.
See also https://github.com/tibbe/hashable/issues/57.
]
[Fixed issue 878: another no longer IMPOSSIBLE case in checking eliminations for equality.
andreas.abel at ifi.lmu.de**20130710082923
Ignore-this: c99aaa7afb24db832c240f6e7201d73d
]
[Added the -fwarn-unused-imports warning.
Andrés Sicard-Ramírez <andres.sicard.ramirez at gmail.com>**20130701140633
Ignore-this: 6147cfb4515df5d36afac8c226442ff0
Thanks to Juan Pedro Villa-Isaza for testing the patch on Windows (using
the Haskell Platform).
]
[Fixed issue 876.
Andrés Sicard-Ramírez <andres.sicard.ramirez at gmail.com>**20130627223545
Ignore-this: c90f0cdec427f39ceeb8e9841356d8cf
]
[Refactor: cleaned compareElims code, case two applications.
andreas.abel at ifi.lmu.de**20130622174808
Ignore-this: ee4eecdfb4024811879deb3f25fbe459
]
[Fixed issue 874: compareElims failed at meta type.
andreas.abel at ifi.lmu.de**20130622171812
Ignore-this: b5c269fd9194998c8d17a055d54c72e9
]
[Fixed issue 854 (part 2), infeasible conversion check.
andreas.abel at ifi.lmu.de**20130621202240
Ignore-this: d2d074eb43a1b7e689b25465e0fdcab2
compareTerm first tries syntactic equality.
However, this was implemented by first doing instantiateFull passes.
These have to traverse the whole terms, even if they were different.
A new function checkSyntacticEquality integrates instantiateFull and
(==) on Term. It only traverses and instanatiates as long as the
two candidates terms are equal.
This removes average-case quadratic complexity of conversion checking
and replaces it with worst-case quadratic complexity.
]
[Testcase for issue 854 (part 2). Agda seems to loop, but it is only an infeasable conversion check.
andreas.abel at ifi.lmu.de**20130621201928
Ignore-this: 22215603ed8c9f1b3deef592eafdd930
]
[More debug printing for reducer.
andreas.abel at ifi.lmu.de**20130620231250
Ignore-this: 955871e5f6e9c014d7ea794c3dbc956a
]
[Added interaction test case for issue 734.
Andrés Sicard-Ramírez <andres.sicard.ramirez at gmail.com>**20130617145349
Ignore-this: 56c5da37d663b98d0c9c1a180a12c2ab
]
[Refactor: make primClauses a list, instead of Maybe a list.
andreas.abel at ifi.lmu.de**20130617125849
Ignore-this: cbf09d0f7eab20305f16aba0e3bf619c
]
[Fixed issue 866.
Andrés Sicard-Ramírez <andres.sicard.ramirez at gmail.com>**20130615174752
Ignore-this: 8895770b4ff40b28aaae53e4c1b03955
]
[Fixed issue 867, added missing level primitives to MAlonzo.
andreas.abel at ifi.lmu.de**20130615143427
Ignore-this: d380f29aa1bbf5878e2d1254676c0a1
]
[Fixed issue 870 (IMPOSSIBLE due to unreduced sort).
andreas.abel at ifi.lmu.de**20130615130549
Ignore-this: d310bcd2da340a0a49b7309f3c1f7132
]
[New reduction strategy: reduce projection redexes eagerly. Fixes issue 854.
andreas.abel at ifi.lmu.de**20130615100524
Ignore-this: dc7f02f2df26d8f32206e6db4eadc80b
In internal syntax, record values now carry list of field names.
If a projection is applied to a record value, the respective field
is extracted. These reductions happen outside of TCM, just as
beta-reductions, e.g. also during substitution.
Saves 2% on standard library (down 5 sec from 240 sec).
]
[Benchmark run after fixing issue 854.
andreas.abel at ifi.lmu.de**20130615100348
Ignore-this: f28457c95372993240563396f944d72c
]
[Tried to understand the Serializer and added some comments.
Andreas Abel <andreas.abel at ifi.lmu.de>**20130614170803
Ignore-this: b2d10ebb2fcc31b5dffb89616868519
]
[Issue #756 fixed serialization bug for KindOfName
Andrea Vezzosi <sanzhiyan at gmail.com>**20130613151016
Ignore-this: 50cac4fef03c8b8c670b37277c75bc63
]
[Added information for updating the Agda wiki to to the release procedure.
Andrés Sicard-Ramírez <andres.sicard.ramirez at gmail.com>**20130611132535
Ignore-this: c36d757286975ad6ff43d6b283f5e544
]
[Rolled back some changes related to Agda-2.3.2.1 release.
Andrés Sicard-Ramírez <andres.sicard.ramirez at gmail.com>**20130604162902
Ignore-this: 3c88895330bfb7e27f1aa3ba06e6a2f6
]
[TAG 2.3.2.1
Andrés Sicard-Ramírez <andres.sicard.ramirez at gmail.com>**20130604161920
Ignore-this: 6fcbb91c132e48c543c3181e3b0f1851
]
[Added announce on the Agda mailing list to the release procedure.
Andrés Sicard-Ramírez <andres.sicard.ramirez at gmail.com>**20130604160556
Ignore-this: 7751465245b6e68dacc6d95bb4193cc7
]
[Updated tested-with field.
Andrés Sicard-Ramírez <andres.sicard.ramirez at gmail.com>**20130604160408
Ignore-this: d890429719e67d1690a438ab98bd0d70
]
[Preparation for Agda-2.3.2.1 release.
Andrés Sicard-Ramírez <andres.sicard.ramirez at gmail.com>**20130604160326
Ignore-this: 1977d4bc6a465fc8051529739b6f6746
]
[Added some debug printouts (-vmalonzo.definition:10).
Nils Anders Danielsson <nils.anders.danielsson at gmail.com>**20130610152143
Ignore-this: b7ffe148c51894670cf4f861c1b83af7
]
[Remember linear parameters that are dropped during apply (see Issue 865).
Andreas Abel <andreas.abel at ifi.lmu.de>**20130604095636
Ignore-this: 8fe3d4149d14b90a03510d967c003deb
Delayed dropping (Drop a) that allows to pick up dropped stuff again,
e.g. when abstracting a module telescope.
]
[Forgotten changed interaction output for 857.
Andreas Abel <andreas.abel at ifi.lmu.de>**20130604082126
Ignore-this: 225fa46f9ca15be0a440df6423040cba
]
[Fixed fix for 857. Now skip arguments of absurd lambda.
andreas.abel at ifi.lmu.de**20130603192407
Ignore-this: 98e5b9a767484227eb8b23158fb88bfc
]
[Added test case for issue 857.
Nils Anders Danielsson <nils.anders.danielsson at gmail.com>**20130603094937
Ignore-this: bff320fa9b5f4f0c86b6932c1b9112d4
]
[Fixed issue 857 (absurd lambda equality) again.
andreas.abel at ifi.lmu.de**20130602152946
Ignore-this: d0a9f558bd5aa340a248ea2d0047ca9b
Undid representation of \ () as \ x -> x.
Created aux definition as before, but now accept two absurd
defs as equal.
Printer also honors absurd lambdas.
]
[Make --without-K less restrictive [Issue 712].
andreas.abel at ifi.lmu.de**20130530143843
Ignore-this: 6f9b69a9f63609f33b1b0eb7fd68955f
We distinguish parameters into three groups:
* non-linear ones (like in the identity type) which we treat as indices
* big ones (like A in List A) which we ignore in the analysis
* the rest, which we treat as before.
Fixes issue 712 and several examples from the mailing list.
]
[Refactor: Clarified code of Data.fitsIn.
andreas.abel at ifi.lmu.de**20130530083309
Ignore-this: 3280e1ddb7fd6501e323e854d8986650
]
[Forbid matching on coinductive records.
andreas.abel at ifi.lmu.de**20130530065933
Ignore-this: f4751b849bc1c34061f1ea28a4b3df3d
]
[Respect singular in error message for IndicesNotConstructorApplications.
andreas.abel at ifi.lmu.de**20130530063636
Ignore-this: ec5e1b3715663f44cd3052c9f5cf7e50
]
[Added another test case related to issue 690.
Nils Anders Danielsson <nils.anders.danielsson at gmail.com>**20130528210703
Ignore-this: f6cf1002937dbef0a4e90e54646f425c
]
[make Agda compile again with ghc 6.12.1 by switching on type synonym instances in various places.
james at cs.ioc.ee**20130527115239
Ignore-this: 9a191d9a9f27d7b440df4a2ca79f37fd
src/full/Agda/Syntax/Concrete/Pretty.hs
src/full/Agda/Syntax/Internal/Generic.hs
src/full/Agda/Syntax/Translation/ConcreteToAbstract.hs
src/full/Agda/Termination/TermCheck.hs
src/full/Agda/TypeChecking/Abstract.hs
src/full/Agda/TypeChecking/DisplayForm.hs
src/full/Agda/TypeChecking/Free.hs
src/full/Agda/TypeChecking/MetaVars/Mention.hs
src/full/Agda/TypeChecking/MetaVars/Occurs.hs
src/full/Agda/TypeChecking/Polarity.hs
src/full/Agda/TypeChecking/Positivity.hs
src/full/Agda/TypeChecking/Quote.hs
src/full/Agda/TypeChecking/Rules/LHS/Unify.hs
]
[Release notes for fix 857: absurd lambdas.
Andreas Abel <andreas.abel at ifi.lmu.de>**20130524230542
Ignore-this: a648a4932d1391dd757624ea558fef4c
]
[Typo in release notes fixed.
Andreas Abel <andreas.abel at ifi.lmu.de>**20130524230502
Ignore-this: 9e8d77ec783ff4a53316afe537a77d81
]
[Fixed issue 857: absurd lambdas are equal now.
andreas.abel at ifi.lmu.de**20130524224841
Ignore-this: 24f344fb36d99ef30b5fd212d04b07a7
Absurd lambdas are now internally represented as \ x -> x,
with () as variable name for x.
]
[How not to fix issue 856 (test case asserting not pruning in blocked things).
Andreas Abel <andreas.abel at ifi.lmu.de>**20130523140833
Ignore-this: 94292823d064849f3f6a9bbce43adb47
]
[Fixed issue 734: goal types were normalized too far.
Andreas Abel <andreas.abel at ifi.lmu.de>**20130522170351
Ignore-this: 7d7d6dc87227e22f2ce9b065899b59e4
]
[Refactor: introduce type Projection for info associated with projections.
Andreas Abel <andreas.abel at ifi.lmu.de>**20130520184301
Ignore-this: afb4a57ac87de014044d5b71fa15ea1c
]
[Debug only: downgrading a debug level.
Andreas Abel <andreas.abel at ifi.lmu.de>**20130520184433
Ignore-this: c02448d25b60e936987b11557de7c205
]
[Added failed tests for the --without-K option.
Andrés Sicard-Ramírez <andres.sicard.ramirez at gmail.com>**20130521042536
Ignore-this: 76667b25cba9debeb84d25568fc030bb
]
[Fixed (parts of?) the Emacs side of issue 850.
Nils Anders Danielsson <nils.anders.danielsson at gmail.com>**20130522125254
Ignore-this: 93dd0fe416d47c200ce1d5962984a8df
]
[Fixed issue 852: report all (generated) calls failing termination checking.
Andreas Abel <andreas.abel at ifi.lmu.de>**20130520144457
Ignore-this: 9a261e21e050c161365a870477d66541
Behavior is not back to what it was before the lasy callInfo
generation suggested by Andrea Vezzosi, but we keep the performance gains!
]
[Switched to simplification (instead of normalisation) in emacs interaction.
Andreas Abel <andreas.abel at ifi.lmu.de>**20130520103315
Ignore-this: ae266d841c7feaca1b3682d5ff565bbd
This is for experimentation purposes.
Key-bindings for full normalisation should also be added.
]
[Fixed compilation of Agda (bad code in last patch).
Andreas Abel <andreas.abel at ifi.lmu.de>**20130520092951
Ignore-this: c1428bdbe51caf9c80caab034918f510
]
[Put the simplifier behind the normalize command C-c C-n for experimentation purposes.
Andreas Abel <andreas.abel at ifi.lmu.de>**20130519205010
Ignore-this: 50d9c7be8fa3bcd305dcbe9690912b98
]
[A simplifier (issue 850).
Andreas Abel <andreas.abel at ifi.lmu.de>**20130519204433
Ignore-this: 6e28bfb63120e32fdb2b5fdef370c156
The simplifier only unfolds definitions if later a constructor/literal pattern is matched.
]
[Irritating error message oscillation (Issue720).
Andreas Abel <andreas.abel at ifi.lmu.de>**20130519172046
Ignore-this: 77f9eda9874373b9f8415d8939f21bee
Rollback of a changed error message contained in the last patch.
]
[Compiled clause matcher: slightly optimized stack pushes.
Andreas Abel <andreas.abel at ifi.lmu.de>**20130519175214
Ignore-this: 97df18232a9a757b05a062232d8bdcc2
]
[Commented and compacted the code of the compiled clause matcher.
Andreas Abel <andreas.abel at ifi.lmu.de>**20130519171910
Ignore-this: 8087193f4f96f654a9625071d0e29def
This involves a slight, but according to my experiments,
insignificant deoptimization:
There might be more test for the empty stack and more prepends
of the empty list to the stack which might not get optimized
away by GHC. However, the code is shorter, more comprehensible,
and avoids cut-n-paste now.
]
[Reverted an incorrect (?) modification.
Nils Anders Danielsson <nils.anders.danielsson at gmail.com>**20130519151843
Ignore-this: 368bf04b86dbc6b2639e535df25bac30
]
[Lazy printing of callInfo in termination checker.
Andreas Abel <andreas.abel at ifi.lmu.de>**20130519145334
Ignore-this: ef6f70d89c30f68f641928bf5c61566b
Saves 12% on the std-lib!
Suggested by Andrea Vezzosi.
]
[Refactor: better interface for getDefs, exposing the Monoid.
Andreas Abel <andreas.abel at ifi.lmu.de>**20130519000611
Ignore-this: 97773d78f9bcc284cbd448ac30cb9322
]
[Refactor: use Foldable.mapM_, of course.
Andreas Abel <andreas.abel at ifi.lmu.de>**20130518234506
Ignore-this: 8ebce5dd05a2cc152b42ade9f89dcf7a
]
[Refactored Andrea Vezzosi's cyclicity test (pre-termination check).
Andreas Abel <andreas.abel at ifi.lmu.de>**20130518224420
Ignore-this: 51972aea350d631d56b94e97568bb69c
Code to extract used definitions reimplemented in Syntax.Internal.Defs.
]
[Avoid termination-checking non-recursive definitions.
Andrea Vezzosi <sanzhiyan at gmail.com>**20130518002211
Ignore-this: 233c7a88bce80d2588f6e57a07ef91d5
]
[Improved fix for issue 848: open anonymous where-module.
Andreas Abel <andreas.abel at ifi.lmu.de>**20130517090622
Ignore-this: 8ded8ca2c5baaf99c9afaf240aaf61fe
]
[Added a toy benchmark.
Nils Anders Danielsson <nils.anders.danielsson at gmail.com>**20130515125606
Ignore-this: 8d9dcf3abc4c78eeb4c5e822c3341631
]
[Finished new postponement strategy for conversion checking dependent things.
Andreas Abel <andreas.abel at ifi.lmu.de>**20130515091241
Ignore-this: 7627b7701686b9f24574faaced40dcb2
If check2 depends on equality check1 of two terms, and check1 gets
stuck, we no longer postpone check2, but we rather created a blocked
version of one of the two terms and use this in check2.
This allows the conversion check to proceed a bit further in some
cases, e.g.
f : (x y : Nat) -> C x y
f a1 b1 =?= f a2 b2
If we get stuck on a1 =?= a2, we now still try b1 =?= b2, substituting
for x a version of a1 which is blocked by problem a1 =?= a2.
]
[Improved on fix for 846, restoring unsolved metas for fail/Issue399.
Andreas Abel <andreas.abel at ifi.lmu.de>**20130514234452
Ignore-this: f567b92e70c94336a08318476ec11c4e
Stealing constraints is the answer!
]
[Forgotten changed errors (fix of issue 846).
Andreas Abel <andreas.abel at ifi.lmu.de>**20130514225035
Ignore-this: 8fb8393ebf9ffd626c4dec5b400245bb
]
[Fixed issue 846: Improved conversion check for pi-types, which makes instance search smarter.
Andreas Abel <andreas.abel at ifi.lmu.de>**20130514221149
Ignore-this: c2e81a410a3bd2e8c2d36bbd31d935c0
The problem with 846 was that some hole was instantiated by some
ill-typed record constructor (under unsolved constraints), leading to
a crash during attempted eta-reduction.
]
[Some debug messages for record eta-contraction for analyzing issue 846.
Andreas Abel <andreas.abel at ifi.lmu.de>**20130514165616
Ignore-this: 8ea90de417cace0676ff2138c1bc7eec
]
[Fixed issue 849: coverage checker unsound.
Andreas Abel <andreas.abel at ifi.lmu.de>**20130514164531
Ignore-this: 971f11eeb68c7a9bc66569e2bf80525b
A dot pattern which could not be parsed into a pattern used to match any constructor pattern. This lets functions with missing clauses pass the coverage checker.
]
[Fixed issue 847 (in a slightly different way).
Nils Anders Danielsson <nils.anders.danielsson at gmail.com>**20130514145149
Ignore-this: 9a57f8cdc16512578a6ee43a264566e1
]
[Cosmetic change.
Nils Anders Danielsson <nils.anders.danielsson at gmail.com>**20130430084758
Ignore-this: c6a163958afb759009ec5543b9d89c6b
]
[Fixed Issue 848: allow anonymous module in where clause.
Andreas Abel <andreas.abel at ifi.lmu.de>**20130514142851
Ignore-this: 5fd3ea98005d705e9b55667f47111d12
]
[Fixed issue 847: body of abstract definitions was ignored during termination checking.
Andreas Abel <andreas.abel at ifi.lmu.de>**20130514141551
Ignore-this: e8358745d4a1f9691665191060593161
]
[Fixed issue 843: incorrect translation of let-bound patterns into projections.
Andreas Abel <andreas.abel at ifi.lmu.de>**20130506150241
Ignore-this: 7c50007f9957283053828f2f15262fc6
]
[WontFix issue 836: constructors/fields also qualified by data/record name.
Andreas Abel <andreas.abel at ifi.lmu.de>**20130502121532
Ignore-this: d74e76dddcced131b9b7d2231cbc4701
]
[Fixed issue 842: Too short lhs in function with varying arity.
Andreas Abel <andreas.abel at ifi.lmu.de>**20130503100729
Ignore-this: 4953c77273f6f55493c2fcb5412fa7ae
]
[Data module imports in successful test cases.
Andreas Abel <andreas.abel at ifi.lmu.de>**20130501190123
Ignore-this: ebf47147c08577791faa900b90ffd69d
This is neccessary if we want to fix Issue 836.
]
[Refactor: Inlined some single-use local definitions and added a comment.
Andreas Abel <andreas.abel at ifi.lmu.de>**20130501100818
Ignore-this: f3b4cc75d4d8be93d346ac82968a786
]
[Fixed issue 841. In interactive refine, new holes could be numbered wrongly.
Andreas Abel <andreas.abel at ifi.lmu.de>**20130501093706
Ignore-this: 9ea862e4a5715c87b264a7c2b93cfc84
Fixed by improving position information for speculated new metas.
Now, the appended new metas are located at the end of the hole, making
sure they get numbered last.
]
[Initial draft of HCAR entry for May 2013.
Nils Anders Danielsson <nils.anders.danielsson at gmail.com>**20130430084603
Ignore-this: 8be6ac868c8ff14c4352d56c5295ea9f
]
[The function inactivate-input-method is obsolete in Emacs 24.3.
Nils Anders Danielsson <nils.anders.danielsson at gmail.com>**20130422122717
Ignore-this: 1a65e9fecd737c51bccdfac4efda6982
]
[Text is now inserted at the end of the *agda2* buffer.
Nils Anders Danielsson <nils.anders.danielsson at gmail.com>**20130422122707
Ignore-this: a84c0d3c5d14640951012270fd4f60e3
]
[Made "cabal haddock" work.
Nils Anders Danielsson <nils.anders.danielsson at gmail.com>**20130422122046
Ignore-this: c6a704c420ca677a19715b6a61591512
]
[Fix issue 833 by fixing the type-checking for section arguments.
Dominique Devriese <dominique.devriese at cs.kuleuven.be>**20130412125806
Ignore-this: 57166bd710682777c9f44752420ce4fa
]
[Fixed issue 830.
Andreas Abel <andreas.abel at ifi.lmu.de>**20130413110718
Ignore-this: ac17b77ed29368b0ef7fc87992a6d0dc
When checking that sort of constructor type fits in data sort,
constructor type was not unfolded.
]
[Fixed bug: GHC options were given in reverse order.
Nils Anders Danielsson <nils.anders.danielsson at gmail.com>**20130405221250
Ignore-this: b8c5e4fc5e5306f65888731c86139292
]
[Changed the bindings for ⊸ and ⅋.
Nils Anders Danielsson <nils.anders.danielsson at gmail.com>**20130403125717
Ignore-this: fdddf91783309453c7c9293da2ad3e61
]
[Input methods for missing linear logic operators
jeanphilippe.bernardy at gmail.com**20130328103755
Ignore-this: 142e9194613d1e22efbe87bbd8bd9df9
]
[Fix for issue 641: -v is now reset when a file is reloaded (in Emacs).
Nils Anders Danielsson <nils.anders.danielsson at gmail.com>**20130324164811
Ignore-this: 5dcb806b4ebf580c89502543459bd6bd
]
[Fixing issue 829: need to keep original clause in catch-all expansion.
Andreas Abel <andreas.abel at ifi.lmu.de>**20130324125756
Ignore-this: 16dd9b9e7bbada11ea61cec0abf7656a
Bug was introduced in fix for 827.
]
[Fixed issue 827: incomplete case tree caused by record pattern translation.
Andreas Abel <andreas.abel at ifi.lmu.de>**20130322185311
Ignore-this: db28870f546533e8a4bd9e63c1fc6f50
Solution: expand catch-alls if a record match is on the same column.
]
[Print name of the function when incomplete matching during evaluation.
Andreas Abel <andreas.abel at ifi.lmu.de>**20130322185031
Ignore-this: d0f6c706fbeb096f1528f68665e118fe
]
[A prettyTCM instance for Internal.Pattern (debugging only).
Andreas Abel <andreas.abel at ifi.lmu.de>**20130322184513
Ignore-this: ab5576ba4bd50bd9896e6db8d63cd898
]
[Fixed issue 279-3 (constructor from instantiated module assigned wrong parameters on lhs).
Andreas Abel <andreas.abel at ifi.lmu.de>**20130322121202
Ignore-this: c381ac455666933086cde9e6fbd74b45
Fixed by adding an extra check for the parameters.
]
[Release notes and test case for the restriction of eta-expanding implicit patterns to the case of record types with constructor (issue 473, 635).
Andreas Abel <andreas.abel at ifi.lmu.de>**20130322092510
Ignore-this: c8d0e82c74d8c08f7c4faaaca36e3f37
]
[Better error message if invoking case split in a goal that is already solved (see issue 289).
Andreas Abel <andreas.abel at ifi.lmu.de>**20130322090709
Ignore-this: ca9657e0088a614edb0ed9718af0fe03
]
[Fixed issue 635: only eta-expand implicit patterns of record type with a constructor.
Andreas Abel <andreas.abel at ifi.lmu.de>**20130321221639
Ignore-this: 17b6b6c4362a5052b9c8d7ec2ac05374
Otherwise, case splitting might emit recCon-NOT-PRINTED patterns that cannot be parsed.
]
[Fixing issue 665 and 824. Fold back eta-expanded implicit patterns in with-clauses, if they meet a dot-pattern of the parent clause.
Andreas Abel <andreas.abel at ifi.lmu.de>**20130321181203
Ignore-this: ad6c213f1488053ca44c8fe578791626
]
[Tiny refactor: added patNoRange for PatRange noRange.
Andreas Abel <andreas.abel at ifi.lmu.de>**20130321144036
Ignore-this: 47df2d4174a97bcc341a32aa192e6316
]
[Keep track in record patterns whether they are eta-expanded implicit patterns (reduces issue 825 to 824).
Andreas Abel <andreas.abel at ifi.lmu.de>**20130321135527
Ignore-this: edc0be7d227f46a4a1c46634e2790d7
In strip for with clauses, eta expand implicit pattern on the fly if
parent clause has expanded implicit pattern.
]
[When resolving an ambiguous name in a pattern, ignore defined names and fields (see issue 822).
Andreas Abel <andreas.abel at ifi.lmu.de>**20130321092839
Ignore-this: f6dd880eb2bb3f9fc03bdb4113043115
This allows constructor names in pattern which are ambiguous in the
sense that they also have a non-constructor definition.
]
[Fixed issue 822.
Andreas Abel <andreas.abel at ifi.lmu.de>**20130321083828
Ignore-this: ce10bd962c65857f26e07b8ed8321f5a
Parsing patterns went wrong in the presence of ambiguous names
of different kinds.
If one defined a name first as non-constructor and then as
constructor, it would not accept it as possible constructor.
]
[Put agda.sty in latex dir instead of current dir
csfnf at swansea.ac.uk**20130319143334
Ignore-this: 4038edb6f68f7fb48ecfeff2ebb0b73b
]
[Fixed issue 826, unfolding corecursion now instantiates metas.
Andreas Abel <andreas.abel at ifi.lmu.de>**20130320161342
Ignore-this: 10b0dfd7263cc01b631af83858a64702
]
[Testcases to ensure --no-termination-check prevents disabling of reductions.
Andreas Abel <andreas.abel at ifi.lmu.de>**20130320150710
Ignore-this: 1297fc9ecad0cf28e9e76dd2f2a53407
For instance, in the positivity checker.
]
[Tried to fix broken jump-to-position-mentioned-in-info-buffer functionality.
Nils Anders Danielsson <nils.anders.danielsson at gmail.com>**20130315123954
Ignore-this: 158378b3c25e763792c8996501981513
]
[Fixed compilation.
Andrés Sicard-Ramírez <andres.sicard.ramirez at gmail.com>**20130315144015
Ignore-this: 3ccc460fe0eb8cec3590fd27b56e4d8a
]
[Russels paradox with --type-in-type, by Paolo Capriotti.
Andreas Abel <andreas.abel at ifi.lmu.de>**20130315124305
Ignore-this: 6b69e43c3a5ac42c0c46477d70a0fd86
]
[Release notes for flexible function arity.
Andreas Abel <andreas.abel at ifi.lmu.de>**20130315123053
Ignore-this: 236764161f49f1637030334af09c904b
]
[Reactivated flexible function arity (issue 727).
Andreas Abel <andreas.abel at ifi.lmu.de>**20130315122054
Ignore-this: 6454bd465721be1c577d3f0ee147f721
Compilers probably need to be updated to this feature.
]
[Fixed issue 821: invalid IMPOSSIBLE in comparison of spines.
Andreas Abel <andreas.abel at ifi.lmu.de>**20130315112601
Ignore-this: a89e91dcd3895455bce9bf43a734f4d6
]
[Another test case for issue 807.
Andreas Abel <andreas.abel at ifi.lmu.de>**20130315104604
Ignore-this: 9cd5864552a9df9104d478208d02228c
]
[Fixed issue 807 (connected to issue 655).
Andreas Abel <andreas.abel at ifi.lmu.de>**20130315103554
Ignore-this: 632affa77c14dcc6c437ac18e1ec71e1
Problem was a circumvention of the code that generates helper
functions for coinduction when checking an alias.
New solution for 655:
Added new flag envExpandLast to type checking context, which is turned
off when checking aliases.
]
[Comment and type signature for domainFree.
Andreas Abel <andreas.abel at ifi.lmu.de>**20130315090700
Ignore-this: 68520650a39510a82f4ebfa66ab53662
]
[Refactor: fused checkMeta and inferMeta into checkOrInferMeta.
Andreas Abel <andreas.abel at ifi.lmu.de>**20130315090009
Ignore-this: bcc04c99b4aa1673dc8e8dec585f6172
]
[Unified 4 definitions of unScope.
Andreas Abel <andreas.abel at ifi.lmu.de>**20130315015459
Ignore-this: 95caf229066582e0e8b957fe6de9f4b7
]
[Removed a stale comment.
Andreas Abel <andreas.abel at ifi.lmu.de>**20130315010002
Ignore-this: e01f0148382d6a20200057a5d242c083
]
[Factored out checkRecordExpression and checkRecordUpdate.
Andreas Abel <andreas.abel at ifi.lmu.de>**20130315005921
Ignore-this: 31165ad98c0471532678bc5b7b7f659a
]
[Factored out checkExtendedLambda.
Andreas Abel <andreas.abel at ifi.lmu.de>**20130315003555
Ignore-this: 92c4abe3130dcba3f88084dcd4221c49
]
[Refactor: use LensHiding (function visible).
Andreas Abel <andreas.abel at ifi.lmu.de>**20130315002104
Ignore-this: a30b1582dc0c636856524af9418d88e
]
[Factored out function checkAbsurdLambda.
Andreas Abel <andreas.abel at ifi.lmu.de>**20130315001944
Ignore-this: 67e124620a738f7b35233a3be89915a8
]
[Comment on WildP and undone attempt to fix 819.
Andreas Abel <andreas.abel at ifi.lmu.de>**20130314065503
Ignore-this: 9453878950f48ae43343b9ab9b5e3d50
]
[Minimal fix for 818: error message instead of panic when with clause has wrong number of arguments.
Andreas Abel <andreas.abel at ifi.lmu.de>**20130308202059
Ignore-this: 647dc2def08d5c3a79c56d126ec8022f
]
[Allowed QuickCheck-2.6.
Andrés Sicard-Ramírez <andres.sicard.ramirez at gmail.com>**20130307153732
Ignore-this: c3d9dcf1a8936f00f8de4d411d55811b
]
[Add blackbold B and 0-9 to agda-input.el
Stevan Andjelkovic <stevan.andjelkovic at strath.ac.uk>**20130305164058
Ignore-this: 10319bf95e1a1aa38f260858269bb054
]
[Fixed issue 810: intro tactic for constructors skips hidden abstractions.
Andreas Abel <andreas.abel at ifi.lmu.de>**20130305155213
Ignore-this: 5b2cbe416c14c8e65e70061f75fda348
]
[Fixed issue 814 (crash in elimView in case of unapplied projection).
Andreas Abel <andreas.abel at ifi.lmu.de>**20130305115741
Ignore-this: c020497ae66b9b7332945239842144f4
]
[More verbosity info.
Andreas Abel <andreas.abel at ifi.lmu.de>**20130305113145
Ignore-this: b2321c03ee9b461d8ee34459e41be8ff
]
[Verbosity info in test case.
Andreas Abel <andreas.abel at ifi.lmu.de>**20130305113035
Ignore-this: 40b1c9d244dfbd8feb9e32aba098b9a
]
[Removed debug printing in test case 778b.
Andreas Abel <andreas.abel at ifi.lmu.de>**20130305112940
Ignore-this: 196c6d2db1980303cbe7acf2da386455
]
[Addressing issue 811: assign earlier variables during unification.
Andreas Abel <andreas.abel at ifi.lmu.de>**20130305112753
Ignore-this: 63f6a17a834700c3556f9673193f4487
The goal is better splitting behavior, dotting later rather than
earlier variables.
But also, we want to dot hidden variables rather than visible ones.
This does not work perfectly yet, but the behavior is no worse than
the current one.
A full solution would probably need a global look at all flexible
variables!?
]
[Inessential: added debug message.
Andreas Abel <andreas.abel at ifi.lmu.de>**20130305111357
Ignore-this: fa0c10695a4cef1ade0fd458fb3e5fb0
]
[Refactor: changed FlexibleVars to dedicated decoration (instead of Arg).
Andreas Abel <andreas.abel at ifi.lmu.de>**20130305110156
Ignore-this: 2497a6c3883f1df211afa74c3f188a00
]
[Refactor: Unifier's FlexibleVars are now Arg Nats instead of just Nats.
Andreas Abel <andreas.abel at ifi.lmu.de>**20130305001458
Ignore-this: 7d0e3998d29f8feb1fae65767a0c3e68
]
[Make test/lib-succeed/Issue784 work with latest std-lib
csfnf at swansea.ac.uk**20130304170350
Ignore-this: 2b00ba0ebc562b3ee97e16d141a3cd42
]
[Fix for issue 778 (improved extended lambda implementation)
csfnf at swansea.ac.uk**20130304195236
Ignore-this: 9d449c13c5de411176124fb0d97272b9
]
[Documented the new key translations in the release notes.
Nils Anders Danielsson <nils.anders.danielsson at gmail.com>**20130304185618
Ignore-this: e637f4d32b055c176439dcd9fd628af5
]
[More characters. Contributed by John Wiegley.
Nils Anders Danielsson <nils.anders.danielsson at gmail.com>**20130304185118
Ignore-this: 80ec1fecf2dd0b3974a334849b0d7a6a
]
[Refactor Syntax.Common: added lenses for Hiding and Relevance.
Andreas Abel <andreas.abel at ifi.lmu.de>**20130301170703
Ignore-this: 7b34f615de19934bfb44be631101903a
]
[Refactor: put application cases of checkExpr into checkApplication.
Andreas Abel <andreas.abel at ifi.lmu.de>**20130301125931
Ignore-this: 5daae86ff311d0f4c74e4517178fb9a4
This reduces the monster checkExpr a bit.
]
[Added Args to Syntax.Abstract.
Andreas Abel <andreas.abel at ifi.lmu.de>**20130301125554
Ignore-this: a3ee7c75474f27bb723162fb1ffd9c6f
]
[Refactor: use case in inferHead instead of top-level pattern matching.
Andreas Abel <andreas.abel at ifi.lmu.de>**20130301123815
Ignore-this: d1a5c5aba1ca2628730b7db5c3644e1d
]
[The Epic backend no longer prints the epic package's version number.
Nils Anders Danielsson <nils.anders.danielsson at gmail.com>**20130228165453
Ignore-this: 2760edb08025b4f79eb11be4c657e13b
]
[Removed absolute path from test output.
Nils Anders Danielsson <nils.anders.danielsson at gmail.com>**20130228164312
Ignore-this: 4e3ad0d8af718070e22c0b8e71c78824
]
[Fixed issue 804, NO_TERMINATION_CHECK is now accepted also within mutual block.
Andreas Abel <andreas.abel at ifi.lmu.de>**20130228161322
Ignore-this: 6c04b11e3550093a9d6c1b84b4488cf7
]
[Added a second test case for issue 802.
Nils Anders Danielsson <nils.anders.danielsson at gmail.com>**20130228115850
Ignore-this: cd4d87faf34425c9887ac640b181b6ca
]
[Modified the pretty-printing of CoverageCantSplitOn errors.
Nils Anders Danielsson <nils.anders.danielsson at gmail.com>**20130218164257
Ignore-this: 19a23364d6f552682a16bd558c755a9d
]
[Added SplitError constructor to TypeError, avoided use of GenericError.
Nils Anders Danielsson <nils.anders.danielsson at gmail.com>**20130218164006
Ignore-this: 54b1a05d0d1869144e49327c2a0cc238
]
[All debug messages at level 1 are now displayed in the Agda info buffer.
Nils Anders Danielsson <nils.anders.danielsson at gmail.com>**20130218155744
Ignore-this: 68a4fdee3a0ff5021748704194954ca2
]
[Stopped using 'reportX "" 0' inside verboseS blocks.
Nils Anders Danielsson <nils.anders.danielsson at gmail.com>**20130215150527
Ignore-this: 20937035682a51f554b492a245c8d6c1
]
[Fixed issue 800. With display form problem (permuted args).
Andreas Abel <andreas.abel at ifi.lmu.de>**20130228105212
Ignore-this: 386c8c823452ba5800ffc791900481c7
]
[Fix the last faulty patch (ProjP sneaked in there) addressing Issue802.
Andreas Abel <andreas.abel at ifi.lmu.de>**20130227184349
Ignore-this: 65372e83f1f2ef5d3d96976c2f2182a1
]
[Fixed issue 802. Index arguments of data types should always have polarity Mixed.
Andreas Abel <andreas.abel at ifi.lmu.de>**20130227155149
Ignore-this: ccf98ca3daecace8fbea599b692177f2
]
[Issue 385 is fixed along with 653.
Andreas Abel <andreas.abel at ifi.lmu.de>**20130227121513
Ignore-this: 6d70f2e3214c50c2e78fcec64ee328b7
]
[No longer unfold functions which fail the termination check (fixes issue 653).
Andreas Abel <andreas.abel at ifi.lmu.de>**20130227120321
Ignore-this: a927b1b5affc58c24587fb3a081fb443
The problem was that the positivity checker looped.
Now termination checking is done first.
]
[Fixed issue 801 by doing termination checking before injectivity checking.
Andreas Abel <andreas.abel at ifi.lmu.de>**20130227103636
Ignore-this: 53f28e17c7b23876fe306d1a9821f468
]
[Refactoring: pulled getDefFreeVars out (InternalToAbstract).
Andreas Abel <andreas.abel at ifi.lmu.de>**20130227093829
Ignore-this: 7e299fe87cf25c8292b61c94e480c0e
]
[Fixed a problem with debug messages for 'with' causing a panic.
Andreas Abel <andreas.abel at ifi.lmu.de>**20130226214624
Ignore-this: f67ead53fb1ee02aa4877dc3423c3f98
]
[Refactor: put abstractToConcrete into TCM for debugging purposes.
Andreas Abel <andreas.abel at ifi.lmu.de>**20130226214441
Ignore-this: cec96b341b3334f9203d4f2b8b8f3f34
]
[Fixed a problem with free variables in type checking extended lambdas.
Andreas Abel <andreas.abel at ifi.lmu.de>**20130226152254
Ignore-this: de5e611a144f34602adfc4664522ab31
This surfaced in connection with issue 778.
The problem was that in the presence of where-blocks the wrong number
of free variables was picked.
]
[Fixed issue 799.
Andreas Abel <andreas.abel at ifi.lmu.de>**20130226035226
Ignore-this: 860b20e1858721352f782d023e30f6a5
Agda had ignored hidden underscores following a constructor even if
these were more than the parameters of the data type.
]
[Issue 4 is fixed (again) by making 'ConcreteMode' the default (issue 796).
Andreas Abel <andreas.abel at ifi.lmu.de>**20130221094354
Ignore-this: 8760dbeaefcafacb849af35a23a5f0ad
]
[Fixed issue 782, lexing of keyword 'to' in 'renaming' directive.
Andreas Abel <andreas.abel at ifi.lmu.de>**20130221093347
Ignore-this: 83a09eb5dd557850634cfc80c7c2837d
]
[Simplified allRight auxiliary function.
Andreas Abel <andreas.abel at ifi.lmu.de>**20121201212708
Ignore-this: e4494f45f1baa4aaa91778f5211a02c4
]
[Initial mode is now ConcreteMode, not AbstractMode (fixes original case of issue 796).
Andreas Abel <andreas.abel at ifi.lmu.de>**20130220234349
Ignore-this: 84b2d7abdc88efa295d28d1212600d9e
That is in accordance to my intuition (abstract is not the default).
]
[Fixed issue 780 (internal error in getTypeMeta).
Andreas Abel <andreas.abel at ifi.lmu.de>**20130220000500
Ignore-this: 63a3b8e026311e9a3d69ea2bd68d316c
By disabling instance search for irrelevant sort metas. (Not intended anyway.)
]
[Updated error message in connection with issue 795.
Andreas Abel <andreas.abel at ifi.lmu.de>**20130219231101
Ignore-this: 99367532eb019a5970d0dbfb07a4bf34
]
[Constructor-headedness (injectivity check) no longer ignores abstract. Fixes 796.
Andreas Abel <andreas.abel at ifi.lmu.de>**20130219230923
Ignore-this: ca3e16a140bddfc815ebe60ed0973c9d
Effect: less programs will type-check, however, changing an abstract
definition in one module will not break type-checking a module
importing the first one (at least not due to failing constructor-headedness).
]
[Fixed KillRange instances for Relevance and ArgInfo.
andreas.abel at ifi.lmu.de**20130219170725
Ignore-this: 4db13bf7476f0daa3d991c38d20db419
]
[Factorize Arg.
Guilhem Moulin <guilhem.moulin at chalmers.se>**20130219161229
Ignore-this: 3a5d21da7e75a23275bf2c8c1243c383
]
[Fixed issue 797. Print location of unsolved emptyness constraint.
Andreas Abel <andreas.abel at ifi.lmu.de>**20130219155420
Ignore-this: eb1f3077f44f598d19432e19660060db
]
[Test case for issue 795.
Andreas Abel <andreas.abel at ifi.lmu.de>**20130218154828
Ignore-this: 9941a3cff6432e92be519f28495fa4f2
]
[Removed error on failing occurs check, because it is not always sound to throw it. Fixes issue 795.
Andreas Abel <andreas.abel at ifi.lmu.de>**20130218153438
Ignore-this: 9156d7d0077a56bb21ef087fa2daf09e
I think it had been disabled before, but I had reenabled it in May 2012.
Now constraint solving is more complete.
However, because the error is not thrown even in situations where it
would be justified, instance search is weaker now. (See last example
in test/fail/Issue723.)
]
[Release notes for removal of matrix-shaped orders in termination checker (Issue 787).
Andreas Abel <andreas.abel at ifi.lmu.de>**20130218151648
Ignore-this: 190ef6c481e5372f519e54bc73eaa1da
]
[Disabled matrix-shaped orders in the termination checker. Fixes issue 787.
Andreas Abel <andreas.abel at ifi.lmu.de>**20130218132050
Ignore-this: baeb8f786702a36da37d1f15b76f50a0
Matrix-shaped orders do not work together correctly with the
idempotency check from size-change termination.
Research is needed how these two features could be integrated.
It seems best to remove matrix-shaped orders for now.
The standard library does not use them.
]
[Fixed Issue794 by disabling an "optimization" for compiling irrelevant arguments.
Andreas Abel <andreas.abel at ifi.lmu.de>**20130216133146
Ignore-this: f54b8908bc70ec542f02bf409d30cb51
]
[Latex-backend: fix escaping of ~, ^ and \
Stevan Andjelkovic <stevan.andjelkovic at strath.ac.uk>**20130127195655
Ignore-this: 8e9c110d7d22ee0dfdf02d7ae501056c
]
[Use UTF-8 also for stdin (when --interaction is used).
Nils Anders Danielsson <nils.anders.danielsson at gmail.com>**20130128134526
Ignore-this: d4d4bff88ab1bd274344578d513320d3
]
[Restored old lower bound for Win32.
Nils Anders Danielsson <nils.anders.danielsson at gmail.com>**20130128134429
Ignore-this: 3c63ecdae66e8a5a0c3eb054b306143
]
[Explicitly set stdout to utf8
Jason Dagit <dagitj at gmail.com>**20130119052112
Ignore-this: b5459c1f61d3ff263623f8b88885d428
]
[Bump the Win32 version requirement for ghc-7.6
Jason Dagit <dagitj at gmail.com>**20130119052027
Ignore-this: 20ffa91e820ac39e0d6daa8f3e2e413c
]
[Fixed issue 784.
Andreas Abel <andreas.abel at ifi.lmu.de>**20130120204611
Ignore-this: e77705e68affd1f06aad288e425d175a
]
[Patch for hashable-1.2.x simplified.
Dirk Ullrich <dirk.ullrich at gmail.com>**20121222221956
Ignore-this: e3822d98932ad1bbb05cb26ef39b1e73
Instances for hashable-1.x can be defined by using `hashWithSalt', too.
]
[Fix issue 773: make instance arguments examples work again.
Dominique Devriese <dominique.devriese at cs.kuleuven.be>**20121225222236
Ignore-this: 2d82a154811ef47e7942abd2c404ef96
]
[Patch for allowing hashable-1.2.x
Dirk Ullrich <dirk.ullrich at gmail.com>**20121215154704
Ignore-this: b880357f43c4e7ce46c92c49915dda2
]
[A new benchmark file.
Nils Anders Danielsson <nils.anders.danielsson at gmail.com>**20121218130118
Ignore-this: 39039eb30c7c62f685b68d7e9958def2
]
[eliminate a hack in InteractionTop.hs by putting 'stInteractionOutputCallback' into 'PersistentTCState'
divipp at gmail.com**20121217124756
Ignore-this: 9c932442a8b9e9c099b575ce07c47ee1
]
[LaTeX-backend: add two new colour schemes to agda.sty (b/w and conor).
Stevan Andjelkovic <stevan.andjelkovic at strath.ac.uk>**20121123154729
Ignore-this: 7b4efff033952c5d4f68ec5d6b91cd65
]
[Fixed issue 729 by thawing the type of an abstract alias before checking.
Andreas Abel <andreas.abel at ifi.lmu.de>**20121122173800
Ignore-this: 35b9c996795cdf21d85201067a07c787
]
[Rolled back second fix attempt for 729 which makes types in types sigs optional.
Andreas Abel <andreas.abel at ifi.lmu.de>**20121122164926
Ignore-this: cacea57b500dfe89dac67401916e294c
]
[Started to make types in type signatures optional (another attempt to fix 729).
Andreas Abel <andreas.abel at ifi.lmu.de>**20121122164811
Ignore-this: 3bea61061f4f2ed01fb8cc97bd89f3e8
]
[Rolled back fix attempt for 729, having a better idea.
Andreas Abel <andreas.abel at ifi.lmu.de>**20121122162131
Ignore-this: 4702c12613f4552849c3b2eaa1e342c5
]
[An attempt to fix issue 729 by introducing FunDef with NoTypeSig.
Andreas Abel <andreas.abel at ifi.lmu.de>**20121122161335
Ignore-this: 974353834d83b01d12d4dce6cd234054
]
[An unused unfreeseMeta function.
Andreas Abel <andreas.abel at ifi.lmu.de>**20121122161911
Ignore-this: a7e520e4d9776724cabb68e88a1f1667
]
[Use modifyMetaStore in updateMetaVar.
Andreas Abel <andreas.abel at ifi.lmu.de>**20121122161545
Ignore-this: 1a9b113af12557bd75b9f815ac727cbf
]
[IMPOSSIBLE instead of error in ConcreteToAbstract.
Andreas Abel <andreas.abel at ifi.lmu.de>**20121122161508
Ignore-this: 3058021df4fc6db13605e95ab6012117
]
[Some comments in Concrete.Definitions.
Andreas Abel <andreas.abel at ifi.lmu.de>**20121122161429
Ignore-this: c9ea5c9031af1a342d85c2dac5decdfa
]
[Fixed issue 765.
Nils Anders Danielsson <nils.anders.danielsson at gmail.com>**20121122160703
Ignore-this: 6f49e40ddb739b6288e0cac92878bf2a
]
[Cosmetic change (?), contributed by John Wiegley (?).
Nils Anders Danielsson <nils.anders.danielsson at gmail.com>**20121120100807
Ignore-this: aab42a36c68842b4a0ed6f32cece1998
]
[Fixed showPat.
Andrés Sicard-Ramírez <andres.sicard.ramirez at gmail.com>**20121119013638
Ignore-this: 2b48207fa3baf7e603b0a52903a47e82
]
[Revert the commenting-out of some tests.
Andreas Abel <andreas.abel at ifi.lmu.de>**20121119105514
Ignore-this: e689d96b76cbf00d8d67e043feea9284
]
[Edit made by the HCAR editor, Janis Voigtländer.
Nils Anders Danielsson <nils.anders.danielsson at gmail.com>**20121119094142
Ignore-this: 2d2d2a2a71af92e106fa212b167b7c41
]
[Allowed abstract mutual. (Issue 761)
Andreas Abel <andreas.abel at ifi.lmu.de>**20121118224320
Ignore-this: 3e9a41150ae1fa0945e2c454a58bc6b0
Disallowed redundant abstract (like in abstract abstract).
Changed error message about useless abstract.
]
[Fixed a typo in UselessPrivate error message.
Andreas Abel <andreas.abel at ifi.lmu.de>**20121118224018
Ignore-this: ddf37eb16eb1471b5d0c60cfa72481c2
]
[Abstract record declarations are now treated as abstract data declarations. (Issue 759)
Andreas Abel <andreas.abel at ifi.lmu.de>**20121118215532
Ignore-this: c9e5008493456d72d2bc6f99ddb554a1
Now there is a better error message when one tries to construct an abstract record.
]
[Added AGDA_TEST_FLAGS to Makefile debug output.
Andreas Abel <andreas.abel at ifi.lmu.de>**20121118211018
Ignore-this: 342c7f039e9563637b618e96233088f6
]
[Rolled back special verbosity for 0 and 1. (Did not perform better.)
Andreas Abel <andreas.abel at ifi.lmu.de>**20121118210211
Ignore-this: efa2e6a304ba6139752e78ba877b8af8
]
[Deactivated debug messages in eta contractions.
Andreas Abel <andreas.abel at ifi.lmu.de>**20121118205039
Ignore-this: 3551f2e60a4c6a6be230757879043655
Seems to save 5% on std-lib.
]
[Single out verbosity levels 0 and 1. (Attempt to optimize reportS).
Andreas Abel <andreas.abel at ifi.lmu.de>**20121118204756
Ignore-this: 2544751089256efab78b6263410b074a
]
[Fixed eta-contraction for abstract record values (see issue 759).
Andreas Abel <andreas.abel at ifi.lmu.de>**20121118185013
Ignore-this: 88dc8767504acd455c69b90020617098
]
[Moved notInScope to Base.
Andreas Abel <andreas.abel at ifi.lmu.de>**20121118164525
Ignore-this: b5dd9606a65df1c002bff9dbd6a7fe8c
]
[A use of unless.
Andreas Abel <andreas.abel at ifi.lmu.de>**20121118160738
Ignore-this: 90e19045647b84629f158cd969bb1594
]
[Added sym and trans to test/Common.Equality.
Andreas Abel <andreas.abel at ifi.lmu.de>**20121118160538
Ignore-this: 6028da6dbf3c1f367c6eb814bdbefe15
]
[A debug printout for checking declarations.
Andreas Abel <andreas.abel at ifi.lmu.de>**20121118155610
Ignore-this: fe04b1abacc35b508da1886f6cad1bad
]
[Fixed issue 755. Polarity info should not be available for abstract definitions.
Andreas Abel <andreas.abel at ifi.lmu.de>**20121118155500
Ignore-this: 493d0bb5bb7ee5204c48b5c8d32f3460
]
[Removed unused IsAbstract field from NiceModuleMacro.
Andreas Abel <andreas.abel at ifi.lmu.de>**20121117234357
Ignore-this: 5a13106fe51449555ec86ea3d92ed929
]
[Complain if private is used without effect. (Issue 760.)
Andreas Abel <andreas.abel at ifi.lmu.de>**20121117165850
Ignore-this: 863d7e2afc9bf2df1487522d74475df0
]
[Fixed issue 754 (internal error due to ill-formed sparse matrices).
Andreas Abel <andreas.abel at ifi.lmu.de>**20121113185126
Ignore-this: 859f0996e9420e128c0e83bf1eedbf2b
Supremum and infinium of two different-shaped matrices now implemented.
]
[Exclude mtl-2.1. It is severly bugged.
Andreas Abel <andreas.abel at ifi.lmu.de>**20121113160958
Ignore-this: 3c48faf3942573b4896f7f3b9291ed1e
Agda will just <<loop>> if you install it in a system with mtl-2.1.
Can you spot the bug in mtl-2.1?
state :: (s -> (a, s)) -> m a
state f = do
s <- get
let ~(a, s) = f s
put s
return a
modify :: MonadState s m => (s -> s) -> m ()
modify f = state (\s -> ((), f s))
I wonder how this passed the testsuite of Eward (which testsuite?).
Another instance of the reason why recursive-by-default let is harmful...
]
[Release notes stub for Version 2.3.4.
Andreas Abel <andreas.abel at ifi.lmu.de>**20121112020941
Ignore-this: 701ca09fa212c2d8ef58bef3a4884c9e
]
[Restored -Werror in Agda.cabal (disabled for release).
Andreas Abel <andreas.abel at ifi.lmu.de>**20121112020236
Ignore-this: 7db1b446424ebf593ca557ddb29ee91c
]
[Removed unnecessary GADTs pragma.
Andrés Sicard-Ramírez <andres.sicard.ramirez at gmail.com>**20121110162146
Ignore-this: df35bc750050539f74e34ff2ac6da28a
]
[Bumped version number to 2.3.3.
andreas.abel at ifi.lmu.de**20121112013740
Ignore-this: c9d622fe77a8ad4c2339cf538b2e5776
]
[TAG 2.3.2
andreas.abel at ifi.lmu.de**20121112002455
Ignore-this: 47f901c8b3f0c10c935a645e75cef8da
]
Patch bundle hash:
c43da333ec9b9acac77244782bac44d5f52c3890
More information about the Agda
mailing list