Commit Graph

16 Commits

Author SHA1 Message Date
Thomas E. Hansen
bdbc0c72bf Make the linter happy 2022-10-05 14:30:08 +02:00
Thomas E. Hansen
cfe18b3d01 [ papers ] A bit of tidying up and clarification 2022-10-05 14:30:08 +02:00
Thomas E. Hansen
8c76118f2f [ papers ] Finish Search.CTL
* Switch to `Inf` to actually use codata/corecursion.
* Add `%hint`s to mark the interface implementations as such, despite
  use of a record for `DepthInv` (this is necessary for other stuff).
* Pass in `Oh` to `reaches10.evidence` in order for things to work.

With huge thanks to gallais for helping me put the final things in
place!

Co-authored-by: Guillaume Allais <guillaume.allais@ens-lyon.org>
2022-10-05 14:30:08 +02:00
Thomas E. Hansen
0d72964f21 [ papers ] Missed some public exports 2022-10-05 14:30:08 +02:00
Thomas E. Hansen
8ca48e0033 [ papers ] Implement reaches10 proof
Seems to be very slow though...
And Idris is unable to find the depth-inv instance for `r10Proof`.
Could be that auto-search is not as strong as Agda's? Or more likely,
I've set things up slightly wrong...
2022-10-05 14:30:08 +02:00
Thomas E. Hansen
b3a8d344e4 [ papers ] Implement proof-search for EF, AF, EG, AG
This also caught an implementation error in the Global formula
definitions:
AG f = A[ f U (f AND' Completed) ]
and **not**
AG f = A[ (f U f) AND' Completed ]
(both of which are valid parsings of the original
 AG f = A[ f u f AND' Completed]
 )
2022-10-05 14:30:08 +02:00
Thomas E. Hansen
f96b25a3d7 [ papers ] Keep AF, EF, AG, EG naming consistent 2022-10-05 14:30:08 +02:00
Thomas E. Hansen
81df879c77 [ papers ] Define Finally operators 2022-10-05 14:30:08 +02:00
Thomas E. Hansen
58b6ccdaf3 [ papers ] Change to LazyList for Computation Tree
This makes more sense in terms of `EU` being efficient and only
evaluating as much as it needs to. However, I'm not sure `model.follow`
is implemented correctly (Agda delays the call to `model.followAll`,
which I'm unsure if we can do (and if so, how to do it) in Idris)...
2022-10-05 14:30:08 +02:00
Thomas E. Hansen
68f8e69ea2 [ papers ] Impl.t proof-search for AU and EU
This reveals an unfortunate problem/misunderstanding: For `ExistsUntil`
to make sense, in terms of evaluation speedups, the list needs to be
lazy. Which is _not_ what `Lazy (List a)` does /!\
I need to switch to LazyList...
2022-10-05 14:30:08 +02:00
Thomas E. Hansen
40780c8f85 [ papers ] Figure out isCompleted by trial and error
And here's a good case against allowing custom unicode syntax:
〈$〉 is `<$>`, i.e. the infix notation for `map`. That's fine; If you
happen to know it!
ESPECIALLY, if your paper defines 〈_〉 as custom notation for a guarded
expression! Then there is **no way** to tell that the expression 〈$〉
is not a guarded expression over `$`, but is instead the alias for
`map`!! You just have to magically know this beforehand!

We also need an explicit `Lazy` annotation for Idris to be happy with
the implicit `ms` in the `IsCompleted` constructor.
2022-10-05 14:30:08 +02:00
Thomas E. Hansen
67218e3eac [ papers ] Move LTE' outside parameters block 2022-10-05 14:30:08 +02:00
Thomas E. Hansen
3e0d5acfa4 [ papers ] Map depth-invariant prfs for AU and EU
The proofs of depth-invariance for Always Until and Exists Until require
mapping the proofs over the Formulae's internal `All` and `Any`
respectively. Idris provides some functions for this, but they erase the
list and so don't quite work. Instead we need to implement our own,
which don't erase the list.
2022-10-05 14:30:08 +02:00
Thomas E. Hansen
40e1a53ab2 [ papers ] Cleaned things up a bit; utterly confused
Don't you love when papers introduce syntax and functions which you've
never seen before and don't seem to match the types of the existing
stuff?

P.S. YEET! (aka. that's probably enough for today ^^)
2022-10-05 14:30:08 +02:00
Thomas E. Hansen
db30dd8d4a [ papers ] Fix things by adding a parameter block
The original Agda code declares the module with L and Sigma (Lbls and
Sts) with type Set. This is apparently close to a parameter block, which
solves the unification error I was having with `now`! Huge thanks to
gallais for showing me that!
2022-10-05 14:30:08 +02:00
Thomas E. Hansen
0c72f83fe8 [ papers ] Start implem.g the model-checking part of Liam's paper
I should have put this under version-control WAAAAAY sooner than this!
Oh well, better late than never...

There are some fun problems to solve in terms of type-mismatch and
erasure, but that's for another day.
2022-10-05 14:30:08 +02:00