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.
|
|
||
| unsat-builtin : {t₁ t₂ : X ⊢} {arity args : ℕ} | ||
| → saturation t₁ ≡ just (arity , args) | ||
| → arity > (suc args) |
There was a problem hiding this comment.
Still wrong as per the previous discussion. Apply IfThenElse True is impure, because it fails due to a missing force, but this logic here doesn't recognize that.
The implementation is being fixed.
| unsat-builtin₀ : {t : X ⊢} {a₀ a₁ : ℕ} | ||
| → sat t ≡ want (suc (suc a₀)) a₁ | ||
| → Pure t | ||
| → Pure (force t) |
There was a problem hiding this comment.
What if the builtin only takes one type argument?
There was a problem hiding this comment.
This is a valid question...
| → sat t ≡ want zero (suc (suc a₁)) | ||
| → Pure t | ||
| → Pure t₁ | ||
| → Pure (t · t₁) |
There was a problem hiding this comment.
What if the builtin takes only one term argument?
There was a problem hiding this comment.
Then nothing applied to it will be pure! :)
There was a problem hiding this comment.
Worth a comment for dummies like myself.
| ... | want zero (suc zero) = want zero zero | ||
| ... | want zero (suc (suc a₁)) = want zero (suc a₁) |
There was a problem hiding this comment.
These two look like they can be a single want zero (suc a1) clause?
| → sat t ≡ want zero (suc (suc a₁)) | ||
| → Pure t | ||
| → Pure t₁ | ||
| → Pure (t · t₁) |
There was a problem hiding this comment.
Worth a comment for dummies like myself.
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.