Inline Phase
module VerifiedCompilation.UInline where
Imports
open import Function using (_∘_)
open import Untyped.Equality using (DecEq; _≟_; decPointwise)
open import VerifiedCompilation.UntypedViews using (Pred; isCase?; isApp?; isLambda?; isForce?; isBuiltin?; isConstr?; isDelay?; isTerm?; allTerms?; iscase; isapp; islambda; isforce; isbuiltin; isconstr; isterm; allterms; isdelay)
open import VerifiedCompilation.UntypedTranslation using (Translation; TransMatch; translation?; Relation; convert; reflexive)
import Relation.Binary as Binary using (Decidable)
open import Data.Empty using (⊥-elim)
open import Data.Nat using (ℕ; suc; zero)
open import Data.String using (String; _++_)
open import Data.Fin using (Fin; suc; zero)
import Data.Fin as Fin using (_≟_)
open import Data.List using (List; []; _∷_)
open import Data.List.Relation.Binary.Pointwise.Base using (Pointwise)
open import Data.Product using (_×_; Σ; ∃; Σ-syntax; ∃-syntax; proj₁; proj₂)
renaming (_,_ to infixl 5 _,_)
open import Untyped.RenamingSubstitution using (_[_]; Sub; _↑ˢ; lifts; extend; weaken)
open import Agda.Builtin.Maybe using (Maybe; just; nothing)
open import Untyped using (_⊢; case; builtin; _·_; force; `; ƛ; delay; con; constr; error; extricateU; extricateUList)
open import RawU using (Untyped)
open import Evaluator.Base using (prettyPrintUTm)
open import Relation.Binary using (DecidableEquality)
open import Relation.Nullary using (Dec; yes; no; ¬_)
open import Untyped.RenamingSubstitution using (weaken)
open import Data.Empty using (⊥)
import Relation.Binary.PropositionalEquality as Eq
open Eq using (_≡_; refl)
open import VerifiedCompilation.Certificate using (Proof?; _>>=_; InlineHints; var; expand; ƛ; ƛ↓; _·_; _·↓; force; delay; con; builtin; error; constr; case; abort; proof; inlineT)
Zippers, and relating two zippers
infix 4 _≽_
infix 8 _↝
variable
X Y : ℕ
variable
x y : Fin X
variable
σ : Sub X Y
variable
L M N L′ M′ N′ : X ⊢
data _↝ (X : ℕ) : Set where
□ : X ↝
_·_ : X ↝ → (X ⊢) → X ↝
variable
z z′ : X ↝
_↑ᶻ : X ↝ → (suc X) ↝
□ ↑ᶻ = □
(z · M) ↑ᶻ = (z ↑ᶻ) · weaken M
injᶻˡ : (z · M ≡ z′ · M′) → z ≡ z′
injᶻˡ refl = refl
injᶻʳ : (z · M ≡ z′ · M′) → M ≡ M′
injᶻʳ refl = refl
_≟ᶻ_ : DecidableEquality (X ↝)
□ ≟ᶻ □ = yes refl
(z · M) ≟ᶻ (z′ · M′) with z ≟ᶻ z′ | M ≟ M′
... | yes refl | yes refl = yes refl
... | no z≠z′ | _ = no (z≠z′ ∘ injᶻˡ)
... | yes refl | no M≠M′ = no (M≠M′ ∘ injᶻʳ)
(z · M) ≟ᶻ □ = no λ()
□ ≟ᶻ (z′ · M′) = no λ()
data _≽_ {X : ℕ} : X ↝ → X ↝ → Set where
□ : □ ≽ □
keep : ∀ {z z′} (M : X ⊢) → z ≽ z′ → (z · M) ≽ (z′ · M)
drop : ∀ {z z′} (M : X ⊢) → z ≽ z′ → (z · M) ≽ (z′ · M)
variable
zz : z ≽ z′
_↑ᶻᶻ : z ≽ z′ → (z ↑ᶻ) ≽ (z′ ↑ᶻ)
□ ↑ᶻᶻ = □
(keep M zᵃ) ↑ᶻᶻ = keep (weaken M) (zᵃ ↑ᶻᶻ)
(drop M zᵃ) ↑ᶻᶻ = drop (weaken M) (zᵃ ↑ᶻᶻ)
idᶻᶻ : (z : X ↝) → z ≽ z
idᶻᶻ □ = □
idᶻᶻ (z · M) = keep M (idᶻᶻ z)
_≟ᶻᶻ_ : (zz zz′ : z ≽ z′) → Maybe (zz ≡ zz′)
□ ≟ᶻᶻ □ = just refl
keep M zz ≟ᶻᶻ keep M′ zz′ with M ≟ M′ | zz ≟ᶻᶻ zz′
... | yes refl | just refl = just refl
... | _ | _ = nothing
drop M zz ≟ᶻᶻ drop M′ zz′ with M ≟ M′ | zz ≟ᶻᶻ zz′
... | yes refl | just refl = just refl
... | _ | _ = nothing
{-# CATCHALL #-}
zz ≟ᶻᶻ zz′ = nothing
Inline relation
data Inline {X : ℕ} :
(σ : Sub X X)
{z z′ : X ↝}
(zz : z ≽ z′)
(M M′ : X ⊢)
→ Set where
` :
(x : Fin X)
→
Inline σ (idᶻᶻ z) (` x) (` x)
`↓ :
(r : Inline σ zz (σ x) M′)
→
Inline σ zz (` x) M′
ƛ□ :
Inline (lifts σ) □ N N′
→
Inline σ □ (ƛ N) (ƛ N′)
ƛ :
(t : Inline (extend (σ ↑ˢ) (weaken M)) (zz ↑ᶻᶻ) N N′)
→
Inline σ (keep M zz) (ƛ N) (ƛ N′)
ƛ↓ :
(t : Inline (extend (σ ↑ˢ) (weaken M)) (zz ↑ᶻᶻ) N (weaken N′))
→
Inline σ (drop M zz) (ƛ N) N′
_·_ :
(r : Inline σ (keep M zz) L L′)
(s : Inline σ □ M M′)
→
Inline σ zz (L · M) (L′ · M′)
_·↓ :
(r : Inline σ (drop M zz) L N′)
→
Inline σ zz (L · M) N′
force :
(r : Inline σ □ M M′)
→
Inline σ zz (force M) (force M′)
delay :
(r : Inline σ □ M M′)
→
Inline σ zz (delay M) (delay M′)
con :
∀ {c}
→
Inline σ zz (con c) (con c)
builtin :
∀ {b}
→
Inline σ zz (builtin b) (builtin b)
constr :
∀ {i Ms M′s}
(rs : Pointwise (Inline σ □) Ms M′s)
→
Inline σ zz (constr i Ms) (constr i M′s)
case :
∀ {Ms M′s}
(r : Inline σ □ M M′)
(rs : Pointwise (Inline σ □) Ms M′s)
→
Inline σ zz (case M Ms) (case M′ M′s)
error : Inline σ zz error error
Check aided by hints
checkPointwise :
(hs : List InlineHints)
(σ : Sub X X)
(zz : z ≽ z′)
(Ms M′s : List (X ⊢))
→ Proof? (Pointwise (Inline σ zz) Ms M′s)
check : (h : InlineHints)
(σ : Sub X X)
(zz : z ≽ z′)
(M M′ : X ⊢)
→ Proof? (Inline σ zz M M′)
check {z = z} {z′ = z′} var σ zz M@(` x) M′@(` x′)
with x Fin.≟ x′ | z ≟ᶻ z′
... | yes refl | yes refl
with zz ≟ᶻᶻ idᶻᶻ z
... | just refl = proof (` x)
... | nothing = abort inlineT M M′
check var σ zz M@(` x) M′@(` x′)
| _ | _ = abort inlineT M M′
check (expand h) σ zz (` x) M′ =
do r ← check h σ zz (σ x) M′
proof (`↓ r)
check (ƛ h) σ □ (ƛ N) (ƛ N′) =
do t ← check h (lifts σ) □ N N′
proof (ƛ□ t)
check (ƛ h) σ (keep M zz) (ƛ N) (ƛ N′) =
do t ← check h (extend (σ ↑ˢ) (weaken M)) (zz ↑ᶻᶻ) N N′
proof (ƛ t)
check (ƛ↓ h) σ (drop M zz) (ƛ N) N′ =
do t ← check h (extend (σ ↑ˢ) (weaken M)) (zz ↑ᶻᶻ) N (weaken N′)
proof (ƛ↓ t)
check (h · h′) σ zz (L · M) (L′ · M′) =
do r ← check h σ (keep M zz) L L′
s ← check h′ σ □ M M′
proof (r · s)
check (h ·↓) σ zz (L · M) N′ =
do r ← check h σ (drop M zz) L N′
proof (r ·↓)
check (force h) σ zz (force M) (force M′) =
do r ← check h σ □ M M′
proof (force r)
check (delay h) σ zz (delay M) (delay M′) =
do r ← check h σ □ M M′
proof (delay r)
check con σ zz M@(con c) M′@(con c′)
with c ≟ c′
... | yes refl = proof con
... | no _ = abort inlineT M M′
check builtin σ zz M@(builtin b) M′@(builtin b′)
with b ≟ b′
... | yes refl = proof builtin
... | no _ = abort inlineT M M′
check (constr hs) σ zz M@(constr i Ms) M′@(constr i′ M′s) with i ≟ i′
... | yes refl =
do rs ← checkPointwise hs σ □ Ms M′s
proof (constr rs)
... | no _ = abort inlineT M M′
check (case h hs) σ zz (case M Ms) (case M′ M′s) =
do r ← check h σ □ M M′
rs ← checkPointwise hs σ □ Ms M′s
proof (case r rs)
check error σ zz error error = proof error
check h σ zz M M′ = abort inlineT M M′
checkPointwise [] σ zz [] [] = proof Pointwise.[]
checkPointwise (h ∷ hs) σ zz (M ∷ Ms) (M′ ∷ M′s) =
do p ← check h σ zz M M′
ps ← checkPointwise hs σ zz Ms M′s
proof (p Pointwise.∷ ps)
checkPointwise _ _ _ Ms M′s = abort inlineT Ms M′s
Top-level check
top-check : (h : InlineHints) (M M′ : 0 ⊢)
→ Proof? (Inline (λ()) □ M M′)
top-check h M M′ = check h (λ()) □ M M′
Lemmas
reflexiveᴬ : {A : Set} → (_≟_ : DecidableEquality A) → (a : A) → (a ≟ a) ≡ yes refl
reflexiveᴬ _≟_ a with a ≟ a
... | yes refl = refl
... | no ¬p = ⊥-elim (¬p refl)
reflexiveᶻᶻ : (zz : z ≽ z′) → zz ≟ᶻᶻ zz ≡ just refl
reflexiveᶻᶻ □ = refl
reflexiveᶻᶻ (keep M zz) rewrite reflexiveᴬ _≟_ M | reflexiveᶻᶻ zz = refl
reflexiveᶻᶻ (drop M zz) rewrite reflexiveᴬ _≟_ M | reflexiveᶻᶻ zz = refl
Completeness
completePointwise :
(σ : Sub X X)
(zz : z ≽ z′)
(Ms M′s : List (X ⊢))
(rs : Pointwise (Inline σ zz) Ms M′s)
→ ∃[ hs ] (checkPointwise hs σ zz Ms M′s ≡ proof rs)
complete :
(σ : Sub X X)
(zz : z ≽ z′)
(M M′ : X ⊢)
(s : Inline σ zz M M′)
→ ∃[ h ] (check h σ zz M M′ ≡ proof s)
complete σ zz (L · M) N′ (r ·↓)
with complete σ (drop M zz) L N′ r
... | (h , e) = (h ·↓ , e′)
where
e′ : check (h ·↓) σ zz (L · M) N′ ≡ proof (r ·↓)
e′ rewrite e = refl
complete {z = z} σ .(idᶻᶻ z) .(` x) .(` x) (` x) = (var , e′)
where
e′ : check var σ (idᶻᶻ z) (` x) (` x) ≡ proof (` x)
e′ rewrite reflexiveᴬ Fin._≟_ x | reflexiveᴬ _≟ᶻ_ z | reflexiveᶻᶻ (idᶻᶻ z) = refl
complete σ zz (` x) M′ (`↓ s)
with complete σ zz (σ x) M′ s
... | (h , e) = (expand h , e′)
where
e′ : check (expand h) σ zz (` x) M′ ≡ proof (`↓ s)
e′ rewrite e = refl
complete σ □ (ƛ N) (ƛ N′) (ƛ□ t)
with complete (lifts σ) □ N N′ t
... | (h , e) = (ƛ h , e′)
where
e′ : check (ƛ h) σ □ (ƛ N) (ƛ N′) ≡ proof (ƛ□ t)
e′ rewrite e = refl
complete σ (keep M zz) (ƛ N) (ƛ N′) (ƛ t)
with complete (extend (σ ↑ˢ) (weaken M)) (zz ↑ᶻᶻ) N N′ t
... | (h , e) = (ƛ h , e′)
where
e′ : check (ƛ h) σ (keep M zz) (ƛ N) (ƛ N′) ≡ proof (ƛ t)
e′ rewrite e = refl
complete σ zz (L · M) (L′ · M′) (r · s)
with complete σ (keep M zz) L L′ r | complete σ □ M M′ s
... | (h , e) | (h′ , e′) = (h · h′ , e″)
where
e″ : check (h · h′) σ zz (L · M) (L′ · M′) ≡ proof (r · s)
e″ rewrite e | e′ = refl
complete σ zz (force M) (force M′) (force r)
with complete σ □ M M′ r
... | (h , e) = (force h , e′)
where
e′ : check (force h) σ zz (force M) (force M′) ≡ proof (force r)
e′ rewrite e = refl
complete σ zz (delay M) (delay M′) (delay r)
with complete σ □ M M′ r
... | (h , e) = (delay h , e′)
where
e′ : check (delay h) σ zz (delay M) (delay M′) ≡ proof (delay r)
e′ rewrite e = refl
complete σ zz (con c) .(con c) con = (con , e)
where
e : check con σ zz (con c) (con c) ≡ proof con
e rewrite reflexiveᴬ _≟_ c = refl
complete σ zz (builtin b) .(builtin b) builtin = (builtin , e)
where
e : check builtin σ zz (builtin b) (builtin b) ≡ proof builtin
e rewrite reflexiveᴬ _≟_ b = refl
complete σ zz (constr i Ms) (constr .i M′s) (constr rs)
with completePointwise σ □ Ms M′s rs
... | (hs , e) = (constr hs , e′)
where
e′ : check (constr hs) σ zz (constr i Ms) (constr i M′s) ≡ proof (constr rs)
e′ rewrite reflexiveᴬ _≟_ i | e = refl
complete σ zz (case M Ms) (case M′ M′s) (case r rs)
with complete σ □ M M′ r | completePointwise σ □ Ms M′s rs
... | (h , e) | (hs , e′) = (case h hs , e″)
where
e″ : check (case h hs) σ zz (case M Ms) (case M′ M′s) ≡ proof (case r rs)
e″ rewrite e | e′ = refl
complete σ zz error error error = (error , refl)
complete σ (drop M zz) (ƛ N) N′ (ƛ↓ t)
with complete (extend (σ ↑ˢ) (weaken M)) (zz ↑ᶻᶻ) N (weaken N′) t
... | (h , e) = (ƛ↓ h , e′)
where
e′ : check (ƛ↓ h) σ (drop M zz) (ƛ N) N′ ≡ proof (ƛ↓ t)
e′ rewrite e = refl
completePointwise σ zz [] [] Pointwise.[] = ([] , refl)
completePointwise σ zz (M ∷ Ms) (M′ ∷ M′s) (p Pointwise.∷ ps)
with complete σ zz M M′ p | completePointwise σ zz Ms M′s ps
... | (h , e) | (hs , e′) = ((h ∷ hs) , e″)
where
e″ : checkPointwise (h ∷ hs) σ zz (M ∷ Ms) (M′ ∷ M′s) ≡ proof (p Pointwise.∷ ps)
e″ rewrite e | e′ = refl