| Age | Commit message (Collapse) | Author |
|---|
|
It fails to infer the type of MaybeFunctor._<$>_, so give it explicitly.
|
|
Generalizing both Vecs in the type of get to instances of Shaped. Thus allowing
trees and other data structures to be used.
|
|
One can use PartialShapeShape instead, so there is limited utility for
this type. It is not used directly and there also is no PartialVecShape.
|
|
Albeit long, this commit is relatively boring.
|
|
|
|
Example inspired in VoigtlaenderHMW13. Note that Vec (α × β) (length s)
is not Shaped in this way since its real index is only a number.
|
|
|
|
|
|
Add IsShaped and Shaped records describing shapely types as in Jay95.
Implement bff on Shaped and rewrite PartialVecVec to use the vector
shape retaining all proofs on the vector implementation.
|
|
The intent is to replace some uses of Vec with a structure that also
happens to be a functor. RawFunctors from the standard library provide
no laws though, so we define a Functor structure that adds the laws. As
an additional law congruence is added, because
* Other standard library structures in Algebra.Structures also require
congruence.
* Otherwise the identity law would have to reason about different
identities.
|
|
|
|
|
|
Beyond allowing default values during shape updates, this branch simplifies
working with shapes other than Vec.
|
|
|
|
|
|
This allows bff to be more precise with regard to its failure modes,
even though we are not yet making use of that projected precision. It
allows inserting a default value for entries that could not be recovered
in a shape changing update as described in VoigtlaenderHMW13.
|
|
|
|
The reduction in proof length is impressive.
|
|
|
|
|
|
|
|
It is now lemma-get-sequenceV and thus no longer applies the free
theorem for the function. Apart making the proof shorter, it also makes
the main use of the free theorem more visible in theorem-2.
|
|
This makes a few proofs easier and eliminates the need for sequence-map
entirely.
|
|
|
|
|
|
|
|
|
|
This is possible using the PartialVecVec implementation.
|
|
|
|
It allows defining get functions that are only defined for some vector
lengths. It retains backwards compatibility with the previous state via
a VecVec compatibility module. The biggest benefit is that now standard
library functions such as tail, take and drop can be passed to bff.
Conflicts: heavy
BFF.agda (imports, bff type clash)
Bidir.agda (imports, heavy bff type clash in theorem-{1,2} and
lemma-get-mapMV)
Generic.agda (imports)
Precond.agda (imports, bff type clash in assoc-enough)
|
|
|
|
The branch enables shape updates in variety of flavours:
* explicitly passing the desired target shape
* providing a plugin sput : ℕ → ℕ → Maybe ℕ
* providing a right-inverse to getlen
It also provides a backwards compatibility function to facilitate
shape-retaining updates.
|
|
|
|
We can now exploit getlen being rightinvertible and it works for drop
and sieve.
|
|
For building on the sieve example.
|
|
|
|
|
|
|
|
Unlike the original version in VoigtlaenderHMW13, we do not request an
sput : ℕ → ℕ → Maybe ℕ
function for determining the updated source shape from the original
source and updated view shape. Instead we ask the caller directly to
provide the result of sput together with a proof that its getlen matches
with the provided, updated view.
The precondition assoc-enough is not enriched in this way and still
requires a non-changing shape. I.e. it says what it said before.
|
|
|
|
|
|
|
|
The new lemma replaces two uses of lemma-fromFunc-tabulate, because the
latter exposes the implementation of FinMapMaybe, whereas the former
argues about the behaviour of FinMapMaybe. The aim of not exposing the
implementation (apart from brevity) is to enable refactoring.
|
|
|
|
Most of the became unused by using the convenience functions introduced
in the parent commit.
|
|
|
|
These two features heavily interconnect. As such it makes sense to
integrate them properly. This non-trivial merge does that work. Compared
to feature-partial-getlen a few definitions moved from FreeTheorems.agda
to GetTypes.agda. Many types changed compared to both branches.
Conflicts:
BFF.agda
Bidir.agda
FreeTheorems.agda
Precond.agda
conflict in GetTypes.agda not detected by merge
|
|
* Remove let patter , match = foo usage
* Remove Qualified.infix-symbol usage
* Add non-obvious absurd patterns
* Qualify constructors
|
|
This branch brings three main benefits:
* Only one explicit parameter is needed to ask for a get function.
* The postulated free theorems are mostly turned into preconditions,
i.e. the only use of the postulates is in LiftGet.
* We can now convert list based get functions to vec based ones and back
including the (now) accompanying free theorem.
|
|
|
