| Age | Commit message (Collapse) | Author |
|---|
|
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.
|
|
|
|
|
|
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
|
|
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.
|
|
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.
|
|
It is unused, has no proofs and starts to get into the way of
refactoring the union function type.
|
|
Also rename fmap to _<$>_ to match Agda naming conventions. The imported
_>>=_ appears to have different binding, so some braces were necessary.
|
|
Also adapt depending modules. Long lines generally become shorter. The
misleading name "EqInst" (hiding the decidability) got discarded.
|
|
And update Bidir and Precond, cause they import BFF.
|
|
This should make it easier to see what is assumed.
|
|
The case is not interesting, because it is too restricted. The defined
get-type requires a bijection between input length and output length.
Since it requires polymorphism we get a reverse get-len via free
theorems and both compositions are required to be identities. Thus the
case is restricted without providing new insights.
|
|
|
|
It is a definition based on Vec but with less assumptions. The VecBFF
has therefore been renamed to VecRevBFF.
VecBFF uses get : \forall n \exists m -> Vec A n -> Vec a m
VecRevBFF uses get : \forall m \exists n -> Vec A n -> Vec a m
|
|
|
|
|
|
|
