| Age | Commit message (Collapse) | Author |
|---|
|
|
|
These became duplicates of their non-barred counterparts.
|
|
|
|
All of these changes were applied to functions of type
... -> (x : ...) -> ... == x -> ...
where x could be preceded by just making the x implicit, because it can
be uniquely deduced from the equality proof.
|
|
|
|
While they do work with Lists and there is no inherent need to know the
length, they are most often invoked in a context where a Vec needs to be
converted to a List using toList. By changing them to work with Vec,
quite a few toList calls can be dropped.
|
|
|
|
Albeit long, this commit is relatively boring.
|
|
|
|
|
|
|
|
|
|
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.
|
|
|
|
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.
|
|
|
|
|
|
|
|
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)
|
|
|
|
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
|
|
By choosing gl₁ = suc and gl₂ = id, the tail function can now be
bidirectionalized.
|
|
|
|
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.
|
|
|
|
|
|
|
|
Most conflicts stem from varying imports or added functions and a
take-both approach merges them. A notable exception is theorem-2, where
a new result sequence-cong was required. Apart from that, theorem-2
could be taken almost verbatim from feature-delete albeit its type
coming from feature-decsetoid.
Conflicts:
Bidir.agda
FinMap.agda
Generic.agda
Precond.agda
|
|
|
|
The biggest piece of this puzzle was establishing
get <$> mapMV f v == mapMV f (get v)
provided that the result of mapMV is just something.
lemma-union-not-used lost a "map just", but could be retained in
structure.
|
|
Since the generalization of lemma-checkInsert-restrict there is nothing
to show for theorem-1. So everything works with Setoids now yielding the
same results as the paper proofs.
|
|
We can actually get semantic equality there without requiring anything
else. Indeed this was already hinted in the BX for free paper that says,
that lemma-1 holds in semantic equality.
|
|
This is another step towards permitting arbitrary Setoids in bff.
|
|
The union was the only user of this type and now it uses only partial
mappings. So drop remaining uses of FinMap and make everything work with
FinMapMaybe instead.
|
|
In the presence of shape-changing updates, bff needs to shrink one of
the mappings before unifying them. As long the shape does not change,
the union becomes a disjoint union. With this insight we can adapt the
proof of theorem-1 using the adapted lemma-disjoint-union. Unfortunately
theorem-2 requires more work and assoc-enough becomes non-trivial due to
the introduction of mapMV.
|
|
|
|
agda 2.3.0.1 supported the old notation, but 2.3.2.1 needs full
qualification.
|
|
Also rename fmap to _<$>_ to match Agda naming conventions. The imported
_>>=_ appears to have different binding, so some braces were necessary.
|
