Filtration by memory model #78
Conversation
eventstructure.v
Outdated
|
|
||
| Definition sca_suffix : E -> seq E := suffix (fica_lt). | ||
|
|
||
| Definition contr_loc f : E -> seq E := |
eventstructure.v
Outdated
| Definition sca_suffix : E -> seq E := suffix (fica_lt). | ||
|
|
||
| Definition contr_loc f : E -> seq E := | ||
| fun e => (f ∘ (same_loc (lab e) \o lab)ᶠ) e. |
There was a problem hiding this comment.
This one looks a bit cryptic. For example, there are two o notations, both of them denote some kind of composition, but different ))
Also ^f notation is non-standard and a bit misleading.
Finally, you can apply eta conversion here: (fun x => f x) == f
There was a problem hiding this comment.
we can't apply eta conversion because we use e inside of (same_loc (lab e) \o lab)ᶠ)
relations.v
Outdated
| Variables (f g : T -> seq T) (p : pred T). | ||
|
|
||
| Definition composition := | ||
| fun x => do y <- g x; f y. |
There was a problem hiding this comment.
This is Kleisli composition. You can use notation (>=>) if you will import monae.
relations.v
Outdated
|
|
||
| End Operations. | ||
|
|
||
| Notation "p 'ᶠ'" := (fun_of_pred p) (at level 10). |
There was a problem hiding this comment.
I remember we were discussing that this is related to "tests" from Kleene Algebras with Tests, but currently we cannot use the notation from relation-algebra. So until I will fix the blocking problem in relation-algebra let's either:
- do not use any notation for this;
- use the same notation as in
relation-algebra, so later we'll be able to migrate smoothly.
I prefer the second solution.
|
should we close this PR for now? |
Let it be here for a while. We'll return to this. |
No description provided.