Updated Pure definition in the metatheory #6964
Conversation
|
Currently this definition of Purity also causes the certifier to say "no" to some of the tests. We should, obviously, fix that before we merge this. |
| -- case applied to constr would reduce, and possibly be pure. | ||
| case : {i : ℕ} {t : X ⊢}{vs ts : List (X ⊢)} | ||
| → lookup? i ts ≡ just t | ||
| → Pure t |
There was a problem hiding this comment.
No, it's t applied to vs that needs to be Pure.
Anyway, do feel free to just omit case. Perhaps with a comment of what we discussed here.
| sat-det sat-t sat-t₁ refl = trans (sym sat-t) sat-t₁ | ||
|
|
||
| data Pure {X : Set} : (X ⊢) → Set where | ||
| force : {t : X ⊢} → Pure t → Pure (force t) |
There was a problem hiding this comment.
No, delay b is pure, force (delay b) isn't necessarily pure. Except when b is pure, which you also need to handle, because the implementation does.
There was a problem hiding this comment.
Did we agree that we only force delays (and builtins), so we don't need to handle force applied to arbitrary things?
|
|
||
| unsat-builtin : {t₁ t₂ : X ⊢} {arity args : ℕ} | ||
| → saturation t₁ ≡ just (arity , args) | ||
| → arity > (suc args) |
There was a problem hiding this comment.
This doesn't take wrong interleaving into account, I'll write it up separately.
But it complies with the current (wrong) implementation, so it's fine.
The previous Pure definition was just a stub. This works, although there are some differences from the Haskell and some open questions about some of the details.