|
| 1 | +--- |
| 2 | +title: VerifiedCompilation.Purity |
| 3 | +layout: page |
| 4 | +--- |
| 5 | + |
| 6 | +# Definitions of Purity for Terms |
| 7 | +``` |
| 8 | +module Untyped.Purity where |
| 9 | +
|
| 10 | +``` |
| 11 | +## Imports |
| 12 | + |
| 13 | +``` |
| 14 | +open import Untyped using (_⊢; case; builtin; _·_; force; `; ƛ; delay; con; constr; error) |
| 15 | +open import Relation.Nullary using (Dec; yes; no; ¬_; _×-dec_) |
| 16 | +open import Builtin using (Builtin; arity; arity₀) |
| 17 | +open import Utils as U using (Maybe;nothing;just) |
| 18 | +open import RawU using (TmCon) |
| 19 | +open import Data.Product using (_,_; _×_) |
| 20 | +open import Data.Nat using (ℕ; zero; suc; _>_; _>?_) |
| 21 | +open import Data.List using (List; _∷_; []) |
| 22 | +open import Data.List.Relation.Unary.All using (All) |
| 23 | +open import Data.Maybe using (Maybe; just; nothing; from-just) |
| 24 | +open import Data.Maybe.Properties using (just-injective) |
| 25 | +open import Agda.Builtin.Equality using (_≡_; refl) |
| 26 | +open import Relation.Nullary.Negation using (contradiction) |
| 27 | +open import Relation.Binary.PropositionalEquality.Core using (trans; _≢_; subst; sym; cong) |
| 28 | +open import Data.Empty using (⊥) |
| 29 | +open import Function.Base using (case_of_) |
| 30 | +open import Untyped.CEK using (lookup?) |
| 31 | +open import VerifiedCompilation.UntypedViews using (isDelay?; isTerm?; isLambda?; isdelay; isterm; islambda) |
| 32 | +-- FIXME: This moves to Untyped.Reduction in a PR #7008... |
| 33 | +open import VerifiedCompilation.UCaseReduce using (iterApp) |
| 34 | +``` |
| 35 | +## Saturation |
| 36 | + |
| 37 | +The `sat` function is used to measure whether a builtin at the bottom of a |
| 38 | +sub-tree of `force` and applications is now saturated and ready to reduce. |
| 39 | + |
| 40 | +``` |
| 41 | +-- TODO: This code will move to Untyped.Reduction once we merge |
| 42 | +-- PR #7008. |
| 43 | +
|
| 44 | +data Arity : Set where |
| 45 | + no-builtin : Arity |
| 46 | + want : ℕ → ℕ → Arity |
| 47 | +
|
| 48 | +-- This is a Phil Wadler approved hack... |
| 49 | +postulate |
| 50 | + interleave-error : ∀ {A : Set} → A |
| 51 | +
|
| 52 | +sat : {X : Set} → X ⊢ → Arity |
| 53 | +sat (` x) = no-builtin |
| 54 | +sat (ƛ t) = no-builtin |
| 55 | +sat (t · t₁) with sat t |
| 56 | +... | no-builtin = no-builtin |
| 57 | +... | want zero zero = want zero zero -- This will reduce the left first... |
| 58 | +... | want zero (suc a₁) = want zero a₁ |
| 59 | +... | want (suc a₀) a₁ = interleave-error |
| 60 | +sat (force t) with sat t |
| 61 | +... | no-builtin = no-builtin |
| 62 | +... | want zero a₁ = interleave-error |
| 63 | +... | want (suc a₀) a₁ = want a₀ a₁ |
| 64 | +sat (delay t) = no-builtin |
| 65 | +sat (con x) = no-builtin |
| 66 | +sat (constr i xs) = no-builtin |
| 67 | +sat (case t ts) = no-builtin |
| 68 | +-- We assume no spontaneously reducing builtins! |
| 69 | +sat (builtin b) = want (arity₀ b) (arity b) |
| 70 | +sat error = no-builtin |
| 71 | +
|
| 72 | +data Pure {X : Set} : (X ⊢) → Set where |
| 73 | + force : {t : X ⊢} → Pure t → Pure (force (delay t)) |
| 74 | +
|
| 75 | + constr : {i : ℕ} {xs : List (X ⊢)} → All Pure xs → Pure (constr i xs) |
| 76 | +
|
| 77 | + -- case applied to constr would reduce, and possibly be pure. |
| 78 | + case : {i : ℕ} {t : X ⊢}{vs ts : List (X ⊢)} |
| 79 | + → lookup? i ts ≡ just t |
| 80 | + → Pure (iterApp t vs) |
| 81 | + → Pure (case (constr i vs) ts) |
| 82 | + -- case applied to anything else is Unknown |
| 83 | +
|
| 84 | + -- This assumes there are no builtins with arity 0 |
| 85 | + -- Or, if there are, they can just be replaced by a |
| 86 | + -- constant before this stage! |
| 87 | + builtin : {b : Builtin} → Pure (builtin b) |
| 88 | +
|
| 89 | + -- To be pure, a term needs to be still unsaturated |
| 90 | + -- after it has been force'd or had something applied |
| 91 | + -- hence, unsat-builtin₀ and unsat-builtin₁ have |
| 92 | + -- (suc (suc _)) requirements. |
| 93 | + unsat-builtin₀ : {t : X ⊢} {a₀ a₁ : ℕ} |
| 94 | + → sat t ≡ want (suc (suc a₀)) a₁ |
| 95 | + → Pure t |
| 96 | + → Pure (force t) |
| 97 | +
|
| 98 | + -- unsat-builtin₀₋₁ handles the case where |
| 99 | + -- we consume the last type argument but |
| 100 | + -- still have some unsaturated term args. |
| 101 | + unsat-builtin₀₋₁ : {t : X ⊢} {a₁ : ℕ} |
| 102 | + → sat t ≡ want (suc zero) (suc a₁) |
| 103 | + → Pure t |
| 104 | + → Pure (force t) |
| 105 | +
|
| 106 | + unsat-builtin₁ : {t t₁ : X ⊢} {a₁ : ℕ} |
| 107 | + → sat t ≡ want zero (suc (suc a₁)) |
| 108 | + → Pure t |
| 109 | + → Pure t₁ |
| 110 | + → Pure (t · t₁) |
| 111 | +
|
| 112 | + -- This is deliberately not able to cover all applications |
| 113 | + -- ƛ (error) · t -- not pure |
| 114 | + -- ƛ ƛ (error) · t · n -- not pure |
| 115 | + -- ƛ ƛ ( (` nothing) · (` just nothing) ) · (ƛ error) · t -- not pure |
| 116 | + -- Double application is considered impure (Unknown) by |
| 117 | + -- the Haskell implementation at the moment. |
| 118 | + app : {l : Maybe X ⊢} {r : X ⊢} |
| 119 | + → Pure l |
| 120 | + → Pure r |
| 121 | + → Pure ((ƛ l) · r) |
| 122 | +
|
| 123 | + var : {v : X} → Pure (` v) |
| 124 | + delay : {t : X ⊢} → Pure (delay t) |
| 125 | + ƛ : {t : (Maybe X) ⊢} → Pure (ƛ t) |
| 126 | + con : {c : TmCon} → Pure (con c) |
| 127 | + -- errors are not pure ever. |
| 128 | +
|
| 129 | +isPure? : {X : Set} → (t : X ⊢) → Dec (Pure t) |
| 130 | +
|
| 131 | +allPure? : {X : Set} → (ts : List (X ⊢)) → Dec (All Pure ts) |
| 132 | +allPure? [] = yes All.[] |
| 133 | +allPure? (t ∷ ts) with (isPure? t) ×-dec (allPure? ts) |
| 134 | +... | yes (p , ps) = yes (p All.∷ ps) |
| 135 | +... | no ¬p = no λ { (px All.∷ x) → ¬p (px , x) } |
| 136 | +
|
| 137 | +{-# TERMINATING #-} |
| 138 | +isPure? (` x) = yes var |
| 139 | +isPure? (ƛ t) = yes ƛ |
| 140 | +isPure? (l · r) with isLambda? (isTerm?) l |
| 141 | +... | yes (islambda (isterm l₁)) with (isPure? l₁) ×-dec (isPure? r) |
| 142 | +... | yes (pl , pr) = yes (app pl pr) |
| 143 | +... | no ¬pl-pr = no λ { (app pl pr) → ¬pl-pr (pl , pr) } |
| 144 | +isPure? (l · r) | no ¬lambda with sat l in sat-l |
| 145 | +... | no-builtin = no (λ { (unsat-builtin₁ sat-l₁ pl pr) → contradiction (trans (sym sat-l) sat-l₁) (λ ()) ; (app xx xx₁) → ¬lambda (islambda (isterm _)) }) |
| 146 | +... | want zero zero = no (λ { (unsat-builtin₁ sat-l₁ xx xx₁) → contradiction ((trans (sym sat-l) sat-l₁)) (λ ()) }) |
| 147 | +... | want zero (suc zero) = no (λ { (unsat-builtin₁ sat-l₁ xx xx₁) → contradiction ((trans (sym sat-l) sat-l₁)) (λ ()) }) |
| 148 | +... | want (suc x) x₁ = no (λ { (unsat-builtin₁ sat-l₁ xx xx₁) → contradiction ((trans (sym sat-l) sat-l₁)) (λ ()) }) |
| 149 | +... | want zero (suc (suc a₁)) with (isPure? l) ×-dec (isPure? r) |
| 150 | +... | yes (pl , pr) = yes (unsat-builtin₁ sat-l pl pr) |
| 151 | +... | no ¬pl-pr = no (λ { (unsat-builtin₁ x xx xx₁) → ¬pl-pr (xx , xx₁) }) |
| 152 | +isPure? (force t) with isDelay? (isTerm?) t |
| 153 | +... | no ¬delay with sat t in sat-t |
| 154 | +... | no-builtin = no (λ { |
| 155 | + (force xx) → ¬delay (isdelay (isterm _)) ; |
| 156 | + (unsat-builtin₀ sat-t₁ pt) → contradiction (trans (sym sat-t) sat-t₁) λ (); |
| 157 | + (unsat-builtin₀₋₁ sat-t₁ pt) → contradiction (trans (sym sat-t) sat-t₁) λ () |
| 158 | + }) |
| 159 | +... | want zero x₁ = no λ { |
| 160 | + (unsat-builtin₀ sat-t₁ pt) → contradiction (trans (sym sat-t) sat-t₁) (λ ()); |
| 161 | + (unsat-builtin₀₋₁ sat-t₁ pt) → contradiction (trans (sym sat-t) sat-t₁) λ () |
| 162 | + } |
| 163 | +... | want (suc zero) zero = no λ { |
| 164 | + (unsat-builtin₀ sat-t₁ pt) → contradiction (trans (sym sat-t) sat-t₁) (λ ()); |
| 165 | + (unsat-builtin₀₋₁ sat-t₁ pt) → contradiction (trans (sym sat-t) sat-t₁) λ () |
| 166 | + } |
| 167 | +... | want (suc zero) (suc x₁) with isPure? t |
| 168 | +... | no ¬pt = no λ { (unsat-builtin₀ x xx) → ¬pt xx ; (unsat-builtin₀₋₁ x xx) → ¬pt xx } |
| 169 | +... | yes pt = yes (unsat-builtin₀₋₁ sat-t pt) |
| 170 | +isPure? (force t) | no ¬delay | want (suc (suc x)) x₁ with isPure? t |
| 171 | +... | no ¬pt = no λ {(unsat-builtin₀ x pt) → ¬pt pt; (unsat-builtin₀₋₁ x xx) → ¬pt xx} |
| 172 | +... | yes pt = yes (unsat-builtin₀ sat-t pt) |
| 173 | +isPure? (force t) | yes (isdelay (isterm tt)) with isPure? tt |
| 174 | +... | yes p = yes (force p) |
| 175 | +... | no ¬p = no λ { (force x) → ¬p x } |
| 176 | +isPure? (delay t) = yes delay |
| 177 | +isPure? (con x) = yes con |
| 178 | +isPure? (constr i xs) with allPure? xs |
| 179 | +... | yes pp = yes (constr pp) |
| 180 | +... | no ¬pp = no λ { (constr x) → ¬pp x } |
| 181 | +isPure? (case (` x) ts) = no λ () |
| 182 | +isPure? (case (ƛ t) ts) = no λ () |
| 183 | +isPure? (case (t · t₁) ts) = no λ () |
| 184 | +isPure? (case (force t) ts) = no λ () |
| 185 | +isPure? (case (delay t) ts) = no λ () |
| 186 | +isPure? (case (con x) ts) = no λ () |
| 187 | +isPure? (case (constr i vs) ts) with lookup? i ts in lookup-i |
| 188 | +... | nothing = no λ { (case lookup≡just pt·vs) → contradiction (trans (sym lookup-i) lookup≡just) λ () } |
| 189 | +... | just t with isPure? (iterApp t vs) |
| 190 | +... | yes pt·vs = yes (case lookup-i pt·vs) |
| 191 | +... | no ¬p = no λ { (case lookup≡just pt·vs) → contradiction (subst (λ x → Pure (iterApp x vs)) (just-injective (trans (sym lookup≡just) lookup-i)) pt·vs) ¬p } |
| 192 | +isPure? (case (case t ts₁) ts) = no λ () |
| 193 | +isPure? (case (builtin b) ts) = no λ () |
| 194 | +isPure? (case error ts) = no λ () |
| 195 | +isPure? (builtin b) = yes builtin |
| 196 | +isPure? error = no λ () |
| 197 | +``` |
0 commit comments