module VerifiedCompilation.UntypedTranslation where open import Untyped using (_⊢; `; ƛ; case; constr; _·_; force; delay; con; builtin; error) import Relation.Unary as Unary using (Decidable) import Relation.Binary as Binary using (Decidable) open import Relation.Nullary using (_×-dec_) open import Data.Product using (_,_) open import Data.List using (List; []; _∷_) open import Data.List.Relation.Binary.Pointwise.Base using (Pointwise) open import Relation.Nullary using (Dec; yes; no; ¬_) open import VerifiedCompilation.UntypedViews using (Pred; ListPred) open import Utils as U using (Maybe) open import RawU using (TmCon; tmCon; decTag; TyTag; ⟦_⟧tag; decTagCon; tmCon2TagCon) open import Data.List using (List; [_]) open import Data.Nat using (ℕ; eq?) open import Data.List.Relation.Binary.Pointwise.Base using (Pointwise) open import Builtin using (Builtin) import Relation.Binary.PropositionalEquality as Eq open Eq using (_≡_; refl) open import VerifiedCompilation.Equality using (DecEq; _≟_; decPointwise)
The generic type of a Translation is that it matches one (or more) patterns on the left to one (or more) patterns on the right. If there are decision procedures to identify those patterns, we can build a decision procedure to apply them recursivley down the AST structure.
Relation = { X : Set } → → (X ⊢) → (X ⊢) → Set₁
data Translation (R : Relation) { X : Set } : (X ⊢) → (X ⊢) → Set₁
data TransMatch (R : Relation) { X : Set } : (X ⊢) → (X ⊢) → Set₁ where
var : {x : X} → TransMatch R (` x) (` x) -- We assume we won't want to translate variables individually?
ƛ : {x x' : Maybe X ⊢}
→ Translation R x x'
----------------------
→ TransMatch R (ƛ x) (ƛ x')
app : {f t f' t' : X ⊢} →
Translation R f f' →
Translation R t t' →
TransMatch R (f · t) (f' · t')
force : {t t' : X ⊢} →
Translation R t t' →
TransMatch R (force t) (force t')
delay : {t t' : X ⊢} →
Translation R t t' →
TransMatch R (delay t) (delay t')
con : {tc : TmCon} → TransMatch R {X} (con tc) (con tc)
constr : {xs xs' : List (X ⊢)} { n : ℕ }
→ Pointwise (Translation R) xs xs'
------------------------
→ TransMatch R (constr n xs) (constr n xs')
case : {p p' : X ⊢} {alts alts' : List (X ⊢)}
→ Pointwise (Translation R) alts alts' -- recursive translation for the other case patterns
→ Translation R p p'
------------------------
→ TransMatch R (case p alts) (case p' alts')
builtin : {b : Builtin} → TransMatch R {X} (builtin b) (builtin b)
error : TransMatch R {X} error error
data Translation R {X} where
istranslation : {ast ast' : X ⊢} → R ast ast' → Translation R ast ast'
match : {ast ast' : X ⊢} → TransMatch R ast ast' → Translation R ast ast'
For the decision procedure we have the rather dissapointing 110 lines to demonstrate to Agda that, having determined that we aren’t in the translation pattern, we are in fact, still not in the translation pattern for each pair of term types.
open import Data.Product
untypedIx : {X : Set} → X ⊢ → ℕ
untypedIx (` x) = 1
untypedIx (ƛ t) = 2
untypedIx (t · t₁) = 3
untypedIx (force t) = 4
untypedIx (delay t) = 5
untypedIx (con x) = 6
untypedIx (constr i xs) = 7
untypedIx (case t ts) = 8
untypedIx (builtin b) = 9
untypedIx error = 10
matchIx : {R : Relation}{X : Set}{a b : X ⊢} → TransMatch R a b → untypedIx a ≡ untypedIx b
matchIx var = refl
matchIx (ƛ x) = refl
matchIx (app x x₁) = refl
matchIx (force x) = refl
matchIx (delay x) = refl
matchIx con = refl
matchIx (constr x) = refl
matchIx (case x x₁) = refl
matchIx builtin = refl
matchIx error = refl
translation?
: {X' : Set} {R : Relation}
→ ({ X : Set } → Binary.Decidable (R {X}))
→ Binary.Decidable (Translation R {X'})
decPointwiseTranslation?
: {X' : Set} {R : Relation}
→ ({ X : Set } → Binary.Decidable (R {X}))
→ Binary.Decidable (Pointwise (Translation R {X'}))
decPointwiseTranslation? isR? [] [] = yes Pointwise.[]
decPointwiseTranslation? isR? [] (x ∷ ys) = no (λ ())
decPointwiseTranslation? isR? (x ∷ xs) [] = no (λ ())
decPointwiseTranslation? isR? (x ∷ xs) (y ∷ ys)
with translation? isR? x y | decPointwiseTranslation? isR? xs ys
... | yes p | yes q = yes (p Pointwise.∷ q)
... | yes _ | no ¬q = no λ where (_ Pointwise.∷ xs~ys) → ¬q xs~ys
... | no ¬p | _ = no λ where (x∼y Pointwise.∷ _) → ¬p x∼y
translation? {_} ⦃ de ⦄ isR? ast ast' with (untypedIx ast) Data.Nat.≟ (untypedIx ast')
translation? {X} ⦃ de ⦄ isR? (` x) (` x₁) | yes _ with x ≟ x₁
... | yes refl = yes (match var)
... | no x≠x₁ with isR? {X} (` x) (` x₁)
... | yes p = yes (istranslation p)
... | no ¬p = no λ { (istranslation x) → ¬p x ; (match var) → x≠x₁ refl }
translation? {_} ⦃ de ⦄ isR? (ƛ ast) (ƛ ast') | yes _ with translation? isR? ast ast'
... | yes t = yes (match (ƛ t))
... | no ¬t with isR? (ƛ ast) (ƛ ast')
... | yes p = yes (istranslation p)
... | no ¬p = no λ { (istranslation x) → ¬p x ; (match (ƛ x)) → ¬t x }
translation? {_} ⦃ de ⦄ isR? (ast · ast₁) (ast' · ast₁') | yes _ with (translation? isR? ast ast') ×-dec (translation? isR? ast₁ ast₁')
... | yes t = yes (match (app (t .proj₁) (t .proj₂)))
... | no ¬t with isR? (ast · ast₁) (ast' · ast₁')
... | yes p = yes (istranslation p)
... | no ¬p = no λ { (istranslation x) → ¬p x ; (match (app x x₁)) → ¬t (x , x₁) }
translation? {_} ⦃ de ⦄ isR? (force ast) (force ast') | yes _ with translation? isR? ast ast'
... | yes t = yes (match (force t))
... | no ¬t with isR? (force ast) (force ast')
... | yes p = yes (istranslation p)
... | no ¬p = no λ { (istranslation x) → ¬p x ; (match (force x)) → ¬t x }
translation? {_} ⦃ de ⦄ isR? (delay ast) (delay ast') | yes _ with translation? isR? ast ast'
... | yes t = yes (match (delay t))
... | no ¬t with isR? (delay ast) (delay ast')
... | yes p = yes (istranslation p)
... | no ¬p = no λ { (istranslation x) → ¬p x ; (match (delay x)) → ¬t x }
translation? {X} ⦃ de ⦄ isR? (con x) (con x₁) | yes _ with x ≟ x₁
... | yes refl = yes (match con)
... | no x≠x₁ with isR? {X} (con x) (con x₁)
... | yes p = yes (istranslation p)
... | no ¬p = no λ { (istranslation x) → ¬p x ; (match con) → x≠x₁ refl }
translation? {_} ⦃ de ⦄ isR? (constr i xs) (constr i₁ xs₁) | yes _ with (i ≟ i₁) ×-dec (decPointwiseTranslation? isR? xs xs₁)
... | yes (refl , snd) = yes (match (constr snd))
... | no ¬t with isR? (constr i xs) (constr i₁ xs₁)
... | yes p = yes (istranslation p)
... | no ¬p = no λ { (istranslation x) → ¬p x ; (match (constr x)) → ¬t (refl , x)}
translation? {_} ⦃ de ⦄ isR? (case ast ts) (case ast' ts₁) | yes _ with (translation? isR? ast ast') ×-dec (decPointwiseTranslation? isR? ts ts₁)
... | yes ( pa , pts ) = yes (match (case pts pa))
... | no ¬papts with isR? (case ast ts) (case ast' ts₁)
... | yes p = yes (istranslation p)
... | no ¬p = no λ { (istranslation x) → ¬p x ; (match (case x xxx)) → ¬papts (xxx , x) }
translation? {X} ⦃ de ⦄ isR? (builtin b) (builtin b₁) | yes _ with b ≟ b₁
... | yes refl = yes (match builtin)
... | no b≠b₁ with isR? {X} (builtin b) (builtin b₁)
... | yes p = yes (istranslation p)
... | no ¬p = no λ { (istranslation x) → ¬p x ; (match builtin) → b≠b₁ refl }
translation? {_} ⦃ de ⦄ isR? error error | yes _ = yes (match error)
translation? {_} ⦃ de ⦄ isR? ast ast' | no ast≠ast' with isR? ast ast'
... | yes p = yes (istranslation p)
... | no ¬p = no λ { (istranslation x) → ¬p x ; (match tm) → ast≠ast' (matchIx tm) }
These functions can be useful when showing equivilence etc. between translation relations.
variable
R S : Relation
X : Set
x x' : X ⊢
xs xs' : List (X ⊢)
convert-pointwise : → (∀ {Y : Set} {y y' : Y ⊢} → R y y' → S y y') → (Pointwise (R ) xs xs' → Pointwise (S ) xs xs')
convert-pointwise f Pointwise.[] = Pointwise.[]
convert-pointwise {R = R} {S = S} f (x∼y Pointwise.∷ p) = f x∼y Pointwise.∷ convert-pointwise {R = R} {S = S} f p
{-# TERMINATING #-}
convert : → (∀ {Y : Set} {y y' : Y ⊢} → R y y' → S y y') → (Translation R x x' → Translation S x x')
convert f (Translation.istranslation xx') = Translation.istranslation (f xx')
convert f (match var) = match var
convert f (match (ƛ x)) = match (ƛ (convert f x))
convert f (match (app x x₁)) = match (app (convert f x) (convert f x₁))
convert f (match (force x)) = match (force (convert f x))
convert f (match (delay x)) = match (delay (convert f x))
convert f (match con) = match con
convert {R = R} {S = S} f (match (constr x)) = match (constr (convert-pointwise {R = Translation R} {S = Translation S} (convert f) x))
convert f (match (case Pointwise.[] xx')) = match (case Pointwise.[] (convert f xx'))
convert {R = R} {S = S} f (match (case (x∼y Pointwise.∷ x) x₁)) = match (case (convert-pointwise {R = Translation R} {S = Translation S} (convert f) (x∼y Pointwise.∷ x)) (convert f x₁))
convert f (match builtin) = match builtin
convert f (match error) = match error
pointwise-reflexive : (∀ {X : Set} {x : X ⊢} → Translation R x x) → (∀ {X : Set} {xs : List (X ⊢)} → Pointwise (Translation R ) xs xs)
pointwise-reflexive f {xs = List.[]} = Pointwise.[]
pointwise-reflexive f {xs = x List.∷ xs} = f Pointwise.∷ pointwise-reflexive f
{-# TERMINATING #-}
reflexive : → Translation R x x
reflexive {x = ` x} = match var
reflexive {x = ƛ x} = match (ƛ reflexive)
reflexive {x = x · x₁} = match (app reflexive reflexive)
reflexive {x = force x} = match (force reflexive)
reflexive {x = delay x} = match (delay reflexive)
reflexive {x = con x} = match con
reflexive {x = constr i xs} = match (constr (pointwise-reflexive reflexive))
reflexive {x = case x ts} = match (case (pointwise-reflexive reflexive) reflexive)
reflexive {x = builtin b} = match builtin
reflexive {x = error} = match error