VerifiedCompilation.UntypedTranslation

Generic Translation Relations for Untyped Plutus Core

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) }

Relations between Translations

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