| Age | Commit message (Collapse) | Author |
|---|
|
|
|
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.
|
|
|
|
This is an improved version of getVec-to-getList in that it also
transports the corresponding free theorem.
|
|
By choosing gl₁ = suc and gl₂ = id, the tail function can now be
bidirectionalized.
|
|
There is no way for Agda to infer these functions or even the intended
index Setoid, so making these explicit is rather required.
|
|
|
|
|
|
This allows passing both getlen and get as a single parameter. It also
allows to make the free theorem a prerequisite instead of a postulate.
|
|
|
|
The representation chosen is to give both an injection gl₁ and a
function gl₂ (formerly getlen), such that by choosing a non-identity for
gl₁ partiality of getlen can be expressed. An alternative would have
been to allow getlen to return a Maybe ℕ and have get return
maybe (Vec A) ⊤ (getlen n)
thus sending all inputs for which getlen yields nothing to tt. It seems
that while there is no way to obtain a such a getlen predicate from an
arbitrary index Setoid I, it should be possible to manufacture a Setoid
from a predicate. Thanks to Stefan Mehner for the insightful discussion.
|
|
|
|
|
|
|
