diff --git a/plutus-metatheory/src/VerifiedCompilation/Purity.lagda.md b/plutus-metatheory/src/VerifiedCompilation/Purity.lagda.md new file mode 100644 index 00000000000..140c3c2d70b --- /dev/null +++ b/plutus-metatheory/src/VerifiedCompilation/Purity.lagda.md @@ -0,0 +1,25 @@ +--- +title: VerifiedCompilation.Purity +layout: page +--- + +# Definitions of Purity for Terms +``` +module VerifiedCompilation.Purity where + +``` +## Imports + +``` +open import Untyped using (_⊢; case; builtin; _·_; force; `; ƛ; delay; con; constr; error) +open import Relation.Nullary using (Dec; yes; no; ¬_) + +``` +## Untyped Purity +``` +data UPure (X : Set) : (X ⊢) → Set where + FIXME : (t : X ⊢) → UPure X t + +isUPure? : {X : Set} → (t : X ⊢) → Dec (UPure X t) +isUPure? t = yes (FIXME t) +``` diff --git a/plutus-metatheory/src/VerifiedCompilation/UCaseOfCase.lagda.md b/plutus-metatheory/src/VerifiedCompilation/UCaseOfCase.lagda.md index 5b857251aba..2bcce6d9f3f 100644 --- a/plutus-metatheory/src/VerifiedCompilation/UCaseOfCase.lagda.md +++ b/plutus-metatheory/src/VerifiedCompilation/UCaseOfCase.lagda.md @@ -34,13 +34,13 @@ open import Data.List using (List; _∷_; []) ## Translation Relation This compiler stage only applies to the very specific case where an `IfThenElse` builtin exists in a `case` expression. -It moves the `IfThenElse` outside and creates two `case` expressions with each of the possible lists of cases. +It moves the `IfThenElse` outside and creates two `case` expressions with each of the possible lists of cases. This will just be an instance of the `Translation` relation once we define the "before" and "after" patterns. ``` data CoC : Relation where - isCoC : {X : Set} → (b : X ⊢) (tn fn : ℕ) (tt tt' ft ft' alts alts' : List (X ⊢)) → + isCoC : {X : Set} {{_ : DecEq X}} → (b : X ⊢) (tn fn : ℕ) (tt tt' ft ft' alts alts' : List (X ⊢)) → Pointwise (Translation CoC) alts alts' → Pointwise (Translation CoC) tt tt' → Pointwise (Translation CoC) ft ft' → @@ -76,7 +76,7 @@ isCoCCase? t | no ¬CoCCase = no λ { (isCoCCase b tn fn alts tt ft) → ¬CoCC (isconstr tn (allterms alts))) (isconstr fn (allterms tt))) (allterms ft)) } - + data CoCForce {X : Set} : (X ⊢) → Set where isCoCForce : (b : (X ⊢)) (tn fn : ℕ) (tt' ft' alts' : List (X ⊢)) → CoCForce (force ((((force (builtin ifThenElse)) · b) · (delay (case (constr tn tt') alts'))) · (delay (case (constr fn ft') alts')))) isCoCForce? : {X : Set} {{ _ : DecEq X }} → Unary.Decidable (CoCForce {X}) @@ -103,12 +103,12 @@ isUntypedCaseOfCase? : {X : Set} {{_ : DecEq X}} → Binary.Decidable (Translati isCoC? : {X : Set} {{_ : DecEq X}} → Binary.Decidable (CoC {X}) isCoC? ast ast' with (isCoCCase? ast) ×-dec (isCoCForce? ast') ... | no ¬cf = no λ { (isCoC b tn fn tt tt' ft ft' alts alts' x x₁ x₂) → ¬cf - (isCoCCase b tn fn tt ft alts , isCoCForce b tn fn tt' ft' alts') } + (isCoCCase b tn fn tt ft alts , isCoCForce b tn fn tt' ft' alts') } ... | yes (isCoCCase b tn fn tt ft alts , isCoCForce b₁ tn₁ fn₁ tt' ft' alts') with (b ≟ b₁) ×-dec (tn ≟ tn₁) ×-dec (fn ≟ fn₁) ×-dec (decPointwise isUntypedCaseOfCase? tt tt') ×-dec (decPointwise isUntypedCaseOfCase? ft ft') ×-dec (decPointwise isUntypedCaseOfCase? alts alts') ... | yes (refl , refl , refl , ttpw , ftpw , altpw) = yes (isCoC b tn fn tt tt' ft ft' alts alts' altpw ttpw ftpw) ... | no ¬p = no λ { (isCoC .b .tn .fn .tt .tt' .ft .ft' .alts .alts' x x₁ x₂) → ¬p (refl , refl , refl , x₁ , x₂ , x) } -isUntypedCaseOfCase? {X} = translation? {X} isCoC? +isUntypedCaseOfCase? {X} = translation? {X} isCoC? ``` ## Semantic Equivalence @@ -125,11 +125,11 @@ The `stepper` function uses the CEK machine to evaluate a term. Here we call it large gas budget and begin in an empty context (which assumes the term is closed). ``` --- TODO: Several approaches are possible. +-- TODO: Several approaches are possible. --semantic_equivalence : ∀ {X set} {ast ast' : ⊥ ⊢} -- → ⊥ ⊢̂ ast ⊳̂ ast' - -- + -- -- → (stepper maxsteps (Stack.ϵ ; [] ▻ ast)) ≡ (stepper maxsteps (Stack.ε ; [] ▻ ast')) --- ∀ {s : ℕ} → stepper s ast ≡ ⇔ ∃ { s' : ℕ } [ stepper s' ast' ≡ ] +-- ∀ {s : ℕ} → stepper s ast ≡ ⇔ ∃ { s' : ℕ } [ stepper s' ast' ≡ ] ``` diff --git a/plutus-metatheory/src/VerifiedCompilation/UFloatDelay.lagda.md b/plutus-metatheory/src/VerifiedCompilation/UFloatDelay.lagda.md new file mode 100644 index 00000000000..13cfefc4cf5 --- /dev/null +++ b/plutus-metatheory/src/VerifiedCompilation/UFloatDelay.lagda.md @@ -0,0 +1,157 @@ +--- +title: VerifiedCompilation.UFloatDelay +layout: page +--- + +# Float-Delay Translation Phase +``` +module VerifiedCompilation.UFloatDelay where + +``` +## Imports + +``` +open import VerifiedCompilation.Equality using (DecEq; _≟_;decPointwise) +open import VerifiedCompilation.UntypedViews using (Pred; isCase?; isApp?; isLambda?; isForce?; isBuiltin?; isConstr?; isDelay?; isTerm?; isVar?; allTerms?; iscase; isapp; islambda; isforce; isbuiltin; isconstr; isterm; allterms; isdelay; isvar) +open import VerifiedCompilation.UntypedTranslation using (Translation; translation?; Relation; convert; reflexive) +open import Relation.Nullary.Product using (_×-dec_) +open import Untyped using (_⊢; case; builtin; _·_; force; `; ƛ; delay; con; constr; error) +import Relation.Binary.PropositionalEquality as Eq +open Eq using (_≡_; refl; _≢_) +open import Data.Empty using (⊥) +open import Function using (case_of_) +open import Agda.Builtin.Maybe using (Maybe; just; nothing) +open import Data.List using (map; all) +open import Relation.Nullary using (Dec; yes; no; ¬_) +import Relation.Binary as Binary using (Decidable) +open import Data.Product using (_,_) +open import Data.Nat using (ℕ) +open import Data.List using (List) +open import Builtin using (Builtin) +open import RawU using (TmCon) +open import VerifiedCompilation.Purity using (UPure; isUPure?) +open import Data.List.Relation.Unary.All using (All; all?) + +variable + X : Set + x x' y y' : X ⊢ +``` +## Translation Relation + +This translation "floats" delays in applied terms into the abstraction, without inlining the whole term. +This is separate from inlining because the added `delay` may make it seem like a substantial increase in code +size, and so dissuade the inliner from executing. However, it may be that the laziness inside the resulting term +is more computationally efficient. + +This translation will only preserve semantics if the instances of the bound variable are under a `force` and if the applied term is "Pure". + +This requires a function to check all the bound variables are under `force`. The `AllForced` type +is defined in terms of the de Brujin index of the bound variable, since this will be incremented under +further lambdas. +``` + +data AllForced (X : Set){{ _ : DecEq X}} : X → (X ⊢) → Set where + var : (v : X) → {v' : X} → v' ≢ v → AllForced X v (` v') + forced : (v : X) → AllForced X v (force (` v)) + force : (v : X) → AllForced X v x' → AllForced X v (force x') + delay : (v : X) → AllForced X v x' → AllForced X v (delay x') + ƛ : (v : X) → {t : (Maybe X) ⊢} + → AllForced (Maybe X) (just v) t + → AllForced X v (ƛ t) + app : (v : X) + → AllForced X v x + → AllForced X v y + → AllForced X v (x · y) + error : {v : X} → AllForced X v error + builtin : {v : X} → {b : Builtin} → AllForced X v (builtin b) + con : {v : X} → {c : TmCon} → AllForced X v (con c) + case : (v : X) → {t : X ⊢} {ts : List (X ⊢)} + → AllForced X v t + → All (AllForced X v) ts + → AllForced X v (case t ts) + constr : (v : X) → {i : ℕ} {xs : List (X ⊢)} + → All (AllForced X v) xs + → AllForced X v (constr i xs) + +{-# TERMINATING #-} +isAllForced? : {{ _ : DecEq X}} → (v : X) → (t : X ⊢) → Dec (AllForced X v t) +isAllForced? v t with isForce? isTerm? t +... | yes (isforce (isterm t)) with isVar? t +... | no ¬var with isAllForced? v t +... | yes allForced = yes (force v allForced) +... | no ¬allForced = no λ { (forced .v) → ¬var (isvar v) ; (force .v p) → ¬allForced p } +isAllForced? v t | yes (isforce (isterm _)) | yes (isvar v₁) with v₁ ≟ v +... | yes refl = yes (forced v) +... | no v₁≢v = yes (force v (var v v₁≢v)) +isAllForced? v (` x) | no ¬force with x ≟ v +... | yes refl = no λ { (var .v x≢v) → x≢v refl} +... | no x≢v = yes (var v x≢v) +isAllForced? {X} v (ƛ t) | no ¬force with isAllForced? {Maybe X} (just v) t +... | yes p = yes (ƛ v p) +... | no ¬p = no λ { (ƛ .v p) → ¬p p} +isAllForced? v (t₁ · t₂) | no ¬force with (isAllForced? v t₁) ×-dec (isAllForced? v t₂) +... | yes (pt₁ , pt₂) = yes (app v pt₁ pt₂) +... | no ¬p = no λ { (app .v x₁ x₂) → ¬p (x₁ , x₂)} +isAllForced? v (force t) | no ¬force = no λ { (forced .v) → ¬force (isforce (isterm t)) ; (force .v x) → ¬force (isforce (isterm t)) } +isAllForced? v (delay t) | no ¬force with isAllForced? v t +... | yes p = yes (delay v p) +... | no ¬p = no λ { (delay .v pp) → ¬p pp} +isAllForced? v (con x) | no ¬force = yes con +isAllForced? v (constr i xs) | no ¬force with all? (isAllForced? v) xs +... | yes p = yes (constr v p) +... | no ¬p = no λ { (constr .v p) → ¬p p } +isAllForced? v (case t ts) | no ¬force with (isAllForced? v t) ×-dec (all? (isAllForced? v) ts) +... | yes (p₁ , p₂) = yes (case v p₁ p₂) +... | no ¬p = no λ { (case .v p₁ p₂) → ¬p ((p₁ , p₂)) } +isAllForced? v (builtin b) | no ¬force = yes builtin +isAllForced? v error | no ¬force = yes error +``` +The `delay` needs to be added to all bound variables. +``` +{-# TERMINATING #-} +subs-delay : {X : Set}{{de : DecEq X}} → (v : Maybe X) → (Maybe X ⊢) → (Maybe X ⊢) +subs-delay v (` x) with v ≟ x +... | yes refl = (delay (` x)) +... | no _ = (` x) +subs-delay v (ƛ t) = ƛ (subs-delay (just v) t) -- The de Brujin index has to be incremented +subs-delay v (t · t₁) = (subs-delay v t) · (subs-delay v t₁) +subs-delay v (force t) = force (subs-delay v t) -- This doesn't immediately apply Force-Delay +subs-delay v (delay t) = delay (subs-delay v t) +subs-delay v (con x) = con x +subs-delay v (constr i xs) = constr i (map (subs-delay v) xs) +subs-delay v (case t ts) = case (subs-delay v t) (map (subs-delay v) ts) +subs-delay v (builtin b) = builtin b +subs-delay v error = error + +``` +The translation relation is then fairly striaghtforward. + +``` +data FlD {X : Set} {{de : DecEq X}} : (X ⊢) → (X ⊢) → Set₁ where + floatdelay : {y y' : X ⊢} {x x' : (Maybe X) ⊢} + → Translation FlD (subs-delay nothing x) x' + → Translation FlD y y' + → UPure X y' + → FlD (ƛ x · (delay y)) (ƛ x' · y') + +FloatDelay : {X : Set} {{_ : DecEq X}} → (ast : X ⊢) → (ast' : X ⊢) → Set₁ +FloatDelay = Translation FlD + +``` +## Decision Procedure +``` + +isFloatDelay? : {X : Set} {{de : DecEq X}} → Binary.Decidable (FloatDelay {X}) + +{-# TERMINATING #-} +isFlD? : {X : Set} {{de : DecEq X}} → Binary.Decidable (FlD {X}) +isFlD? ast ast' with (isApp? (isLambda? isTerm?) (isDelay? isTerm?)) ast +... | no ¬match = no λ { (floatdelay x x₁ x₂) → ¬match ((isapp (islambda (isterm _)) (isdelay (isterm _)))) } +... | yes (isapp (islambda (isterm t₁)) (isdelay (isterm t₂))) with (isApp? (isLambda? isTerm?) isTerm?) ast' +... | no ¬match = no λ { (floatdelay x x₁ x₂) → ¬match ((isapp (islambda (isterm _)) (isterm _))) } +... | yes (isapp (islambda (isterm t₁')) (isterm t₂')) with (isFloatDelay? (subs-delay nothing t₁) t₁') ×-dec (isFloatDelay? t₂ t₂') ×-dec (isUPure? t₂') +... | no ¬p = no λ { (floatdelay x₁ x₂ x₃) → ¬p ((x₁ , x₂ , x₃))} +... | yes (p₁ , p₂ , pure) = yes (floatdelay p₁ p₂ pure) +isFloatDelay? = translation? isFlD? + +``` diff --git a/plutus-metatheory/src/VerifiedCompilation/UForceDelay.lagda.md b/plutus-metatheory/src/VerifiedCompilation/UForceDelay.lagda.md index c98902f096e..2f800fc86a9 100644 --- a/plutus-metatheory/src/VerifiedCompilation/UForceDelay.lagda.md +++ b/plutus-metatheory/src/VerifiedCompilation/UForceDelay.lagda.md @@ -13,7 +13,7 @@ module VerifiedCompilation.UForceDelay where ``` open import VerifiedCompilation.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; translation?; Relation) +open import VerifiedCompilation.UntypedTranslation using (Translation; translation?; Relation; convert; reflexive) open import Relation.Nullary.Product using (_×-dec_) open import Data.Product using (_,_) import Relation.Binary as Binary using (Decidable) @@ -21,10 +21,12 @@ open import Relation.Nullary using (Dec; yes; no; ¬_) open import Untyped using (_⊢; case; builtin; _·_; force; `; ƛ; delay; con; constr; error) import Relation.Binary.PropositionalEquality as Eq open Eq using (_≡_; refl) +open import Relation.Binary.PropositionalEquality.Core using (cong) open import Data.Empty using (⊥) open import Agda.Builtin.Maybe using (Maybe; just; nothing) -open import Data.Nat using (ℕ; zero; suc) +open import Data.Nat using (ℕ; zero; suc; _+_) open import Untyped.RenamingSubstitution using (weaken) +open import Data.List using (List; _∷_; []) ``` ## Translation Relation @@ -41,73 +43,262 @@ cancel out precisely. Ultimately they should be equivalent. ``` -data pureFD : Relation where - forcedelay : {X : Set} → (x x' : X ⊢) → Translation pureFD x x' → pureFD (force (delay x)) x' - pushfd : {X : Set} → (x : Maybe X ⊢) → (y : X ⊢) - → pureFD (force ((ƛ x) · y)) ((ƛ (force x)) · y) - transfd : {X : Set} → (x x'' x' : X ⊢) → Translation pureFD x x'' → Translation pureFD x'' x' → pureFD x x' - appfd : {X : Set} → (x : Maybe X ⊢) → (y : X ⊢) → pureFD ((ƛ x) · y) (ƛ (x · (weaken y))) - appfd⁻¹ : {X : Set} → (x : Maybe X ⊢) → (y : X ⊢) → pureFD (ƛ (x · (weaken y))) ((ƛ x) · y) - -data FD : ℕ → ℕ → Relation where - forcefd : (n nₐ : ℕ) → {X : Set} → (x x' : X ⊢) → FD (suc n) nₐ x x' → FD n nₐ (force x) x' - delayfd : (n nₐ : ℕ) → {X : Set} → (x x' : X ⊢) → FD n nₐ x x' → FD (suc n) nₐ (delay x) x' - lastdelay : (n nₐ : ℕ) → {X : Set} → (x x' : X ⊢) → Translation (FD zero zero) x x' → FD (suc zero) zero (delay x) x' - multiappliedfd : (n nₐ : ℕ) → {X : Set} → (x y x' y' : X ⊢) - → Translation (FD zero zero) y y' - → FD n (suc nₐ) (force x) x' - → FD n nₐ (force (x · y)) (x' · y') - multiabstractfd : (n nₐ : ℕ) → {X : Set} → (x x' : Maybe X ⊢) - → FD n nₐ (force x) x' - → FD n (suc nₐ) (force (ƛ x)) (ƛ x') +data pureFD {X : Set} {{de : DecEq X}} : X ⊢ → X ⊢ → Set₁ where + forcedelay : {x x' : X ⊢} → pureFD x x' → pureFD (force (delay x)) x' + pushfd : {x x' : Maybe X ⊢} → {y y' : X ⊢} + → pureFD x x' + → pureFD y y' + → pureFD (force ((ƛ x) · y)) ((ƛ (force x')) · y') + _⨾_ : {x x'' x' : X ⊢} + → pureFD x x'' + → pureFD x'' x' + → pureFD x x' + translationfd : {x x' : X ⊢} + → Translation pureFD x x' + → pureFD x x' + + appfd : {x : Maybe X ⊢} → {y z : X ⊢} → pureFD (((ƛ x) · y) · z) (ƛ (x · (weaken z)) · y) + appfd⁻¹ : {x : Maybe X ⊢} → {y z : X ⊢} → pureFD (ƛ (x · (weaken z)) · y) (((ƛ x) · y) · z) + +_ : pureFD {Maybe ⊥} (force (delay (` nothing))) (` nothing) +_ = forcedelay (translationfd Translation.var) + +forceappdelay : pureFD {Maybe ⊥} (force ((ƛ (delay (` nothing))) · (` nothing))) ((ƛ (` nothing)) · (` nothing)) +forceappdelay = (pushfd (translationfd (Translation.delay Translation.var)) (translationfd reflexive)) ⨾ (translationfd (Translation.app (Translation.ƛ (Translation.istranslation + (forcedelay (translationfd Translation.var)))) Translation.var)) + +_ : pureFD {Maybe ⊥} (force (force (delay (delay error)))) error +_ = translationfd (Translation.force (Translation.istranslation (forcedelay (translationfd reflexive)))) ⨾ forcedelay (translationfd Translation.error) + +_ : pureFD {Maybe ⊥} (force (force (ƛ (ƛ (delay (delay (` nothing))) · (` nothing)) · (` nothing)))) (ƛ (ƛ (` nothing) · (` nothing)) · (` nothing)) +_ = (translationfd (Translation.force (Translation.istranslation (pushfd (translationfd reflexive) (translationfd reflexive))))) ⨾ ((translationfd (Translation.force (Translation.app (Translation.ƛ (Translation.istranslation (pushfd (translationfd reflexive) (translationfd reflexive)))) reflexive))) ⨾ ( pushfd (translationfd reflexive) (translationfd reflexive) ⨾ ((translationfd (Translation.app (Translation.ƛ (Translation.istranslation (pushfd (translationfd reflexive) (translationfd reflexive)))) reflexive)) ⨾ (translationfd (Translation.app (Translation.ƛ (Translation.app (Translation.ƛ (Translation.istranslation ((translationfd (Translation.force (Translation.istranslation (forcedelay (translationfd (Translation.delay Translation.var)))))) ⨾ (forcedelay (translationfd Translation.var))))) reflexive)) reflexive))))) + +test4 : {X : Set} {{_ : DecEq X}} {N : Maybe (Maybe X) ⊢} {M M' : X ⊢} → pureFD (force (((ƛ (ƛ (delay N))) · M) · M')) (((ƛ (ƛ N)) · M) · M') +test4 = (translationfd (Translation.force (Translation.istranslation appfd))) ⨾ ((pushfd (translationfd reflexive) (translationfd reflexive)) ⨾ ((translationfd (Translation.app (Translation.ƛ (Translation.istranslation (pushfd (translationfd reflexive) (translationfd reflexive)))) reflexive )) ⨾ (translationfd (Translation.app (Translation.ƛ (Translation.app (Translation.ƛ (Translation.istranslation (forcedelay (translationfd reflexive)))) reflexive)) reflexive) ⨾ appfd⁻¹))) + +data FD {X : Set} {{_ : DecEq X}} : ℕ → ℕ → X ⊢ → X ⊢ → Set₁ where + forcefd : (n nₐ : ℕ) → {x x' : X ⊢} + → FD (suc n) nₐ x x' → FD n nₐ (force x) x' + delayfd : (n nₐ : ℕ) → {x x' : X ⊢} + → FD n nₐ x x' → FD (suc n) nₐ (delay x) x' + lastdelay : (n nₐ : ℕ) → {x x' : X ⊢} + → Translation (FD zero zero) x x' + → FD (suc zero) zero (delay x) x' + multiappliedfd : (n nₐ : ℕ) → {x y x' y' : X ⊢} + → Translation (FD zero zero) y y' + → FD n (suc nₐ) (force x) x' + → FD n nₐ (force (x · y)) (x' · y') + multiabstractfd : (n nₐ : ℕ) → {x x' : Maybe X ⊢} + → FD n nₐ (force x) x' + → FD n (suc nₐ) (force (ƛ x)) (ƛ x') + +_ : FD {⊥} zero zero (force (ƛ (delay error) · error)) (ƛ error · error) +_ = multiappliedfd zero zero Translation.error + (multiabstractfd zero zero + (forcefd zero zero (lastdelay zero zero Translation.error))) + +_ : FD {⊥} zero zero (force (delay error)) error +_ = forcefd zero zero (lastdelay zero zero Translation.error) + +_ : FD {⊥} zero zero (force (force (delay (delay error)))) error +_ = forcefd zero zero + (forcefd 1 zero + (delayfd 1 zero (lastdelay zero zero Translation.error))) + +_ : FD {Maybe ⊥} zero zero (force (force (ƛ (ƛ (delay (delay (` nothing))) · (` nothing)) · (` nothing)))) (ƛ (ƛ (` nothing) · (` nothing)) · (` nothing)) +_ = forcefd zero zero + (multiappliedfd 1 zero Translation.var + (multiabstractfd 1 zero + (multiappliedfd 1 zero Translation.var + (multiabstractfd 1 zero + (forcefd 1 zero + (delayfd 1 zero (lastdelay zero zero Translation.var))))))) ForceDelay : {X : Set} {{_ : DecEq X}} → (ast : X ⊢) → (ast' : X ⊢) → Set₁ ForceDelay = Translation (FD zero zero) + +t : ⊥ ⊢ +t = force (((ƛ (ƛ (delay error))) · error) · error) + +t' : ⊥ ⊢ +t' = ((ƛ (ƛ error)) · error) · error + +test-ffdd : FD {⊥} zero zero (force (force (delay (delay error)))) (error) +test-ffdd = forcefd zero zero + (forcefd 1 zero + (delayfd 1 zero (lastdelay zero zero Translation.error))) + +_ : pureFD t t' +_ = (translationfd (Translation.force (Translation.istranslation appfd))) + ⨾ ((pushfd (translationfd reflexive) (translationfd reflexive)) + ⨾ (translationfd (Translation.app (Translation.ƛ (Translation.istranslation ((pushfd ((translationfd reflexive)) (translationfd reflexive)) + ⨾ translationfd (Translation.app (Translation.ƛ (Translation.istranslation (forcedelay (translationfd Translation.error)))) Translation.error)))) Translation.error) + ⨾ appfd⁻¹)) + +_ : pureFD {⊥} (force (ƛ (ƛ (delay error) · error) · error)) (ƛ (ƛ error · error) · error) +_ = (pushfd (translationfd reflexive) (translationfd reflexive)) + ⨾ (translationfd (Translation.app (Translation.ƛ (Translation.istranslation ((pushfd (translationfd reflexive) (translationfd reflexive)) + ⨾ translationfd (Translation.app (Translation.ƛ (Translation.istranslation (forcedelay (translationfd Translation.error)))) Translation.error)))) Translation.error)) + +``` + +## FD implies pureFD + +The two counters in `FD` track the number of forces and applications removed, +to be "consumed" later. Consequently, at any stage we should be able to put +`n` forces and `nₐ` applications back on to the current term and have a valid +`pureFD` relation. + +``` +{- +forces : {X : Set} → ℕ → X ⊢ → X ⊢ +forces zero x = x +forces (suc n) x = forces n (force x) + +-- What actually gets applied? Does it matter?.... +-- The `y` in the FD rules gets handled separately, here it just +-- matters that there is an application that can be paired +-- with a lambda. `error` has the advantage that it is always +-- in scope, even if it is semantically silly. +applications : {X : Set} → List (X ⊢) → X ⊢ → X ⊢ +applications [] x = x +applications (y ∷ args) (force x) = applications args (force (x · y)) +applications (y ∷ args) x = applications args (x · y) -- Does this ever happen? + + +forces-translation : {X : Set} {{de : DecEq X}} {x x' : X ⊢} {R : Relation} → (n : ℕ) → Translation R {{de}} x x' → Translation R {{de}} (forces n x) (forces n x') +forces-translation zero xx' = xx' +forces-translation (suc n) xx' = forces-translation n (Translation.force xx') + +apps-translation : {X : Set}{{de : DecEq X}} {x x' : X ⊢}{R : Relation} → (n : ℕ) → Translation R {{de}} x x' → Translation R {{de}} (applications n x) (applications n x') +apps-translation zero t = t +apps-translation {x = x} {x' = x'} (suc n) t = {!!} + + +FD→pureFD : {X : Set}{{de : DecEq X}} {x x' : X ⊢} → FD {{de}} zero zero x x' → pureFD {{de}} x x' + +TFD→TpureFD : {X : Set}{{de : DecEq X}} {x x' : X ⊢} → Translation (FD zero zero) x x' → Translation pureFD {{de}} x x' +TFD→TpureFD = convert FD→pureFD + +nFD→pureFD : {X : Set}{{de : DecEq X}} {x x' : X ⊢} {n nₐ : ℕ} → FD n nₐ x x' → pureFD {{de}} (forces n (applications nₐ x)) x' +nFD→pureFD {n = zero} {nₐ = zero} p = FD→pureFD p +nFD→pureFD {n = suc n} {nₐ = zero} (forcefd .(suc n) .zero p) = nFD→pureFD p -- Fixme: is this correct? It might be because the forces are encoded in n +nFD→pureFD {n = suc n} {nₐ = zero} (delayfd .n .zero p) = (translationfd (forces-translation n (Translation.istranslation (forcedelay (translationfd reflexive))))) ⨾ (nFD→pureFD p) +nFD→pureFD {n = suc .0} {nₐ = zero} (lastdelay n nₐ p) = forcedelay (translationfd (TFD→TpureFD p)) +nFD→pureFD {n = suc n} {nₐ = zero} (multiappliedfd .(suc n) .zero x p) = {!!} +nFD→pureFD {n = zero} {nₐ = suc nₐ} (forcefd .zero .(suc nₐ) p) = {!!} +nFD→pureFD {n = zero} {nₐ = suc nₐ} (multiappliedfd .zero .(suc nₐ) p p₁) = {!!} +nFD→pureFD {x' = x'} {n = zero} {nₐ = suc nₐ} (multiabstractfd .zero .nₐ p) = (translationfd (apps-translation nₐ (Translation.istranslation (pushfd (translationfd {!!}) (translationfd reflexive))))) ⨾ translationfd (apps-translation {!!} {!!}) +nFD→pureFD {n = suc n} {nₐ = suc nₐ} p = {!!} + + +nFD→pureFD {n = suc n} {args = []} (forcefd .(suc n) .[] p) = nFD→pureFD p -- Fixme: is this correct? It might be because the forces are encoded in n +nFD→pureFD {n = suc n} {args = []} (delayfd .n .[] p) = (translationfd (forces-translation n (Translation.istranslation (forcedelay (translationfd reflexive))))) ⨾ nFD→pureFD p +--nFD→pureFD {n = suc .0} {args = zero} (lastdelay n args p) = forcedelay (translationfd (TFD→TpureFD p)) +nFD→pureFD {n = suc n} {args = []} (multiappliedfd .(suc n) .[] p₁ (forcefd .(suc n) _ p)) = {!!} +nFD→pureFD {n = suc n} {args = []} (multiappliedfd .(suc n) .[] p₁ (multiappliedfd .(suc n) _ x p)) = {!!} +nFD→pureFD {n = suc n} {args = []} (multiappliedfd .(suc n) .[] p₁ (multiabstractfd .(suc n) _ p)) = (translationfd (forces-translation (suc n) (Translation.istranslation (pushfd (translationfd reflexive) (translationfd (TFD→TpureFD p₁)))))) ⨾ ((translationfd (forces-translation (suc n) (Translation.app (Translation.ƛ (Translation.istranslation {!!})) {!!}))) ⨾ {!p!}) +nFD→pureFD {n = zero} {args = (y ∷ args)} (forcefd .zero .(y ∷ args) p) = {!!} +nFD→pureFD {n = zero} {args = (y ∷ args)} (multiappliedfd .zero .(y ∷ args) p p₁) = {!!} +nFD→pureFD {n = zero} {args = (y ∷ args)} (multiabstractfd .zero .args p) = {!!} ⨾ {!!} +nFD→pureFD {n = suc n} {args = (y ∷ args)} p = {!!} + + +FD→pureFD p = {!!} +-} +{- +{-# TERMINATING #-} +FD→pureFD {x = .(force (force _))} {x' = x'} (forcefd .zero .zero (forcefd .1 .zero p)) = (translationfd (Translation.force {!!})) ⨾ (FD→pureFD (forcefd zero zero {!!})) +FD→pureFD {x = .(force (delay _))} {x' = x'} (forcefd .zero .zero (delayfd .0 .zero p)) = forcedelay (FD→pureFD p) +--FD→pureFD {x = .(force (delay _))} {x' = x'} (forcefd .zero .zero (lastdelay n args p)) = forcedelay (translationfd (TFD→TpureFD p)) +FD→pureFD {x = .(force (force (_ · _)))} {x' = .(_ · _)} (forcefd .zero .zero (multiappliedfd .1 .zero p₁ p)) = {!!} +FD→pureFD {x = .(force (_ · _))} {x' = .(_ · _)} (multiappliedfd .zero .zero p₁ (forcefd .zero .1 p)) = {!!} +FD→pureFD {x = .(force ((_ · _) · _))} {x' = .((_ · _) · _)} (multiappliedfd .zero .zero p₁ (multiappliedfd .zero .1 x₁ p)) = {!!} +FD→pureFD {x = (force (ƛ x · y))} {x' = (ƛ x' · y')} (multiappliedfd .zero .zero p₁ (multiabstractfd .zero .0 p)) = (pushfd (translationfd reflexive) (translationfd reflexive)) ⨾ (translationfd (Translation.app (Translation.ƛ (Translation.istranslation (FD→pureFD p))) (TFD→TpureFD p₁))) +-} +{- +FD→pureFD {x = .(force (force (force (force _))))} {x' = x'} (forcefd .zero .zero (forcefd .1 .zero (forcefd .2 .zero (forcefd .3 .zero p)))) = {!!} +FD→pureFD {x = .(force (force (delay _)))} {x' = x'} (forcefd .zero .zero (forcefd .1 .zero (delayfd .1 .zero p))) = (translationfd (Translation.force (Translation.istranslation (forcedelay (translationfd reflexive))))) ⨾ FD→pureFD (forcefd zero zero p) +FD→pureFD {x = .(force (force (force (delay _))))} {x' = x'} (forcefd .zero .zero (forcefd .1 .zero (forcefd .2 .zero (delayfd .2 .zero p)))) = (translationfd (Translation.force (Translation.force (Translation.istranslation (forcedelay (translationfd reflexive)))))) ⨾ (FD→pureFD (forcefd zero zero (forcefd 1 zero p))) +FD→pureFD {x = .(force (force (force (force (_ · _)))))} {x' = .(_ · _)} (forcefd .zero .zero (forcefd .1 .zero (forcefd .2 .zero (multiappliedfd .3 .zero x p)))) = {!!} +FD→pureFD {x = .(force (force (force (_ · _))))} {x' = .(_ · _)} (forcefd .zero .zero (forcefd .1 .zero (multiappliedfd .2 .zero x p))) = {!!} +FD→pureFD {x = .(force (delay _))} {x' = x'} (forcefd .zero .zero (delayfd .0 .zero p)) = forcedelay (FD→pureFD p) +FD→pureFD {x = .(force (delay _))} {x' = x'} (forcefd .zero .zero (lastdelay n args p)) = forcedelay (translationfd (TFD→TpureFD p)) +FD→pureFD {x = (force (force (x · y)))} {x' = (x' · y')} (forcefd .zero .zero (multiappliedfd .1 .zero p p₁)) = {!!} +FD→pureFD {x = (force (x · y))} {x' = (x' · y')} (multiappliedfd .zero .zero p p₁) = {!!} +-} + + +{- +FD→pureFD : FD x x' → pureFD x x' + +TFD→TpureFD : Translation FD x x' → Translation pureFD x x' +TFD→TpureFD = convert FD→pureFD + +{-# TERMINATING #-} +FD→pureFD {x = (force (force x))} {x' = x'} (ffd (forcefd .zero (forcefd .1 p))) = transfd x' (Translation.istranslation (FD→pureFD (ffd (forcefd zero (forcefd 1 p))))) reflexive +FD→pureFD {x = (force (delay x))} {x' = x'} (ffd (forcefd .zero (delayfd .0 p))) = forcedelay x x' + (Translation.istranslation (FD→pureFD (ffd p))) +FD→pureFD {x = force (force (ƛ x · y))} {x' = ƛ x' · y'} (ffd (forcefd .zero (afd .1 (appfd .1 .zero p₁ p₂)))) = transfd (force (ƛ (force x) · y)) (Translation.force (Translation.istranslation (pushfd reflexive reflexive))) (Translation.istranslation (transfd ( ((force (ƛ (force x))) · y)) (Translation.istranslation {!!}) {!!})) +FD→pureFD {x = force (force ((x · x₁) · y))} {x' = x' · y'} (ffd (forcefd .zero (afd .1 (appfd .1 .zero p₁ p₂)))) = {!!} +FD→pureFD {x = force x} {x' = x'} (ffd (forcefd .zero (afd .1 (ffd .1 args x₁)))) = FD→pureFD (ffd (forcefd zero x₁)) +FD→pureFD {x = x} {x' = x'} (ffd (tfd n (Translation.istranslation p))) = FD→pureFD (ffd p) +FD→pureFD {x = x} {x' = x'} (ffd (tfd n p)) = transfd x' (TFD→TpureFD (Translation.istranslation (ffd (tfd n p)))) reflexive +FD→pureFD {x = force ((x · y) · z)} {x' = (x' · y') · z'} (ffd (afd .zero (appfd .zero .zero p (appfd .zero .1 p₁ p₂)))) = {!!} +FD→pureFD {x = force ((ƛ x) · y)} {x' = (ƛ x') · y'} (ffd (afd .zero (appfd .zero .zero p (absfd .zero .0 p₁ p₂)))) = transfd ((ƛ (force x) · y)) (Translation.istranslation (pushfd reflexive reflexive)) (Translation.app (Translation.ƛ (Translation.istranslation (FD→pureFD (ffd (afd zero p₂))))) (TFD→TpureFD p)) +FD→pureFD {x = x} {x' = x'} (ffd (afd .zero (ffd .zero args x₁))) = FD→pureFD (ffd x₁) +-} + + + ``` ## Decision Procedure ``` +{- + isForceDelay? : {X : Set} {{_ : DecEq X}} → Binary.Decidable (Translation (FD zero zero) {X}) {-# TERMINATING #-} -isFD? : {X : Set} {{_ : DecEq X}} → (n nₐ : ℕ) → Binary.Decidable (FD n nₐ {X}) +isFD? : {X : Set} {{_ : DecEq X}} → (n args : ℕ) → Binary.Decidable (FD n args {X}) -isFD? n nₐ ast ast' with isForce? isTerm? ast +isFD? n args ast ast' with isForce? isTerm? ast -- If it doesn't start with force then it isn't going to match this translation, unless we have some delays left -isFD? zero nₐ ast ast' | no ¬force = no λ { (forcefd .zero .nₐ x .ast' xx) → ¬force (isforce (isterm x)) ; (multiappliedfd .zero .nₐ x y x' y' x₁ xx) → ¬force (isforce (isterm (x · y))) ; (multiabstractfd .zero nₐ x x' xx) → ¬force (isforce (isterm (ƛ x))) } -isFD? (suc n) nₐ ast ast' | no ¬force with (isDelay? isTerm? ast) -... | no ¬delay = no λ { (forcefd .(suc n) .nₐ x .ast' xx) → ¬force (isforce (isterm x)) ; (delayfd .n .nₐ x .ast' xx) → ¬delay (isdelay (isterm x)) ; (lastdelay n nₐ x .ast' x₁) → ¬delay (isdelay (isterm x)) ; (multiappliedfd .(suc n) .nₐ x y x' y' x₁ xx) → ¬force (isforce (isterm (x · y))) ; (multiabstractfd .(suc n) nₐ x x' xx) → ¬force (isforce (isterm (ƛ x))) } -... | yes (isdelay (isterm t)) with (isForceDelay? t ast') ×-dec (n ≟ zero) ×-dec (nₐ ≟ zero) -... | yes (p , refl , refl) = yes (lastdelay zero zero t ast' p) -... | no ¬zero with isFD? n nₐ t ast' -... | no ¬p = no λ { (delayfd .n .nₐ .t .ast' xxx) → ¬p xxx ; (lastdelay n nₐ .t .ast' x) → ¬zero (x , refl , refl)} -... | yes p = yes (delayfd n nₐ t ast' p) +isFD? zero args ast ast' | no ¬force = no λ { (forcefd .zero .args xx) → ¬force (isforce (isterm _)) ; (multiappliedfd .zero .args x xx) → ¬force (isforce (isterm (_ · _))) ; (multiabstractfd .zero args xx) → ¬force (isforce (isterm (ƛ _))) } +isFD? (suc n) args ast ast' | no ¬force with (isDelay? isTerm? ast) +... | no ¬delay = no λ { (forcefd .(suc n) .args xx) → ¬force (isforce (isterm _)) ; (delayfd .n .args xx) → ¬delay (isdelay (isterm _)) ; (lastdelay n args x) → ¬delay (isdelay (isterm _)) ; (multiappliedfd .(suc n) .args x xx) → ¬force (isforce (isterm (_ · _))) ; (multiabstractfd .(suc n) args xx) → ¬force (isforce (isterm (ƛ _)))} +... | yes (isdelay (isterm t)) with (isForceDelay? t ast') ×-dec (n ≟ zero) ×-dec (args ≟ zero) +... | yes (p , refl , refl) = yes (lastdelay zero zero p) +... | no ¬zero with isFD? n args t ast' +... | no ¬p = no λ { (delayfd .n .args xx) → ¬p xx ; (lastdelay n args x) → ¬zero (x , refl , refl)} +... | yes p = yes (delayfd n args p) -- If there is an application we can increment the application counter -isFD? n nₐ ast ast' | yes (isforce (isterm t)) with (isApp? isTerm? isTerm?) t -isFD? n nₐ ast ast' | yes (isforce (isterm t)) | yes (isapp (isterm t₁) (isterm t₂)) with (isApp? isTerm? isTerm?) ast' -isFD? n nₐ ast ast' | yes (isforce (isterm t)) | yes (isapp (isterm t₁) (isterm t₂)) | no ¬isApp = no λ { (multiappliedfd .n .nₐ .t₁ .t₂ x' y' x xx) → ¬isApp (isapp (isterm x') (isterm y')) } -isFD? n nₐ ast ast' | yes (isforce (isterm t)) | yes (isapp (isterm t₁) (isterm t₂)) | yes (isapp (isterm t₁') (isterm t₂')) with (isFD? n (suc nₐ) (force t₁) t₁') ×-dec (isForceDelay? t₂ t₂') -... | yes (pfd , pfd2) = yes (multiappliedfd n nₐ t₁ t₂ t₁' t₂' pfd2 pfd) -... | no ¬FD = no λ { (multiappliedfd .n .nₐ .t₁ .t₂ .t₁' .t₂' x xx) → ¬FD (xx , x) } +isFD? n args ast ast' | yes (isforce (isterm t)) with (isApp? isTerm? isTerm?) t +isFD? n args ast ast' | yes (isforce (isterm t)) | yes (isapp (isterm t₁) (isterm t₂)) with (isApp? isTerm? isTerm?) ast' +isFD? n args ast ast' | yes (isforce (isterm t)) | yes (isapp (isterm t₁) (isterm t₂)) | no ¬isApp = no λ { (multiappliedfd .n .args x xx) → ¬isApp (isapp (isterm _) (isterm _)) } +isFD? n args ast ast' | yes (isforce (isterm t)) | yes (isapp (isterm t₁) (isterm t₂)) | yes (isapp (isterm t₁') (isterm t₂')) with (isFD? n (suc args) (force t₁) t₁') ×-dec (isForceDelay? t₂ t₂') +... | yes (pfd , pfd2) = yes (multiappliedfd n args pfd2 pfd) +... | no ¬FD = no λ { (multiappliedfd .n .args x xx) → ¬FD (xx , x) } -- If there is a lambda we can decrement the application counter unless we have reached zero -isFD? n nₐ ast ast' | yes (isforce (isterm t)) | no ¬isApp with (isLambda? isTerm? t) -isFD? n (suc nₐ ) ast ast' | yes (isforce (isterm t)) | no ¬isApp | yes (islambda (isterm t₂)) with (isLambda? isTerm?) ast' -... | no ¬ƛ = no λ { (multiabstractfd .n .nₐ .t₂ x' xx) → ¬ƛ (islambda (isterm x')) } -... | yes (islambda (isterm t₂')) with (isFD? n nₐ (force t₂) t₂') -... | yes p = yes (multiabstractfd n nₐ t₂ t₂' p) -... | no ¬p = no λ { (multiabstractfd .n .nₐ .t₂ .t₂' xx) → ¬p xx } +isFD? n args ast ast' | yes (isforce (isterm t)) | no ¬isApp with (isLambda? isTerm? t) +isFD? n (suc args ) ast ast' | yes (isforce (isterm t)) | no ¬isApp | yes (islambda (isterm t₂)) with (isLambda? isTerm?) ast' +... | no ¬ƛ = no λ { (multiabstractfd .n .args xx) → ¬ƛ (islambda (isterm _)) } +... | yes (islambda (isterm t₂')) with (isFD? n args (force t₂) t₂') +... | yes p = yes (multiabstractfd n args p) +... | no ¬p = no λ { (multiabstractfd .n .args xx) → ¬p xx } -- If we have zero in the application counter then we can't descend further -isFD? n zero ast ast' | yes (isforce (isterm t)) | no ¬isApp | yes (islambda (isterm t₂)) = no λ { (forcefd .n .zero .(ƛ t₂) .ast' ()) } +isFD? n zero ast ast' | yes (isforce (isterm t)) | no ¬isApp | yes (islambda (isterm t₂)) = no λ { (forcefd .n .zero ()) } -- If we have matched none of the patterns then we need to consider nesting. -isFD? n nₐ ast ast' | yes (isforce (isterm t)) | no ¬isApp | no ¬ƛ with isFD? (suc n) nₐ t ast' -... | yes p = yes (forcefd n nₐ t ast' p) -... | no ¬p = no λ { (forcefd .n .nₐ .t .ast' xx) → ¬p xx ; (multiappliedfd .n .nₐ x y x' y' x₁ xx) → ¬isApp (isapp (isterm x) (isterm y)) ; (multiabstractfd .n nₐ x x' xx) → ¬ƛ (islambda (isterm x)) } +isFD? n args ast ast' | yes (isforce (isterm t)) | no ¬isApp | no ¬ƛ with isFD? (suc n) args t ast' +... | yes p = yes (forcefd n args p) +... | no ¬p = no λ { (forcefd .n .args xx) → ¬p xx ; (multiappliedfd .n .args x xx) → ¬isApp (isapp (isterm _) (isterm _)) ; (multiabstractfd .n args xx) → ¬ƛ (islambda (isterm _)) } isForceDelay? = translation? (isFD? zero zero) +-} ``` diff --git a/plutus-metatheory/src/VerifiedCompilation/UntypedTranslation.lagda.md b/plutus-metatheory/src/VerifiedCompilation/UntypedTranslation.lagda.md index 4c1c1f604e9..6c6300774d5 100644 --- a/plutus-metatheory/src/VerifiedCompilation/UntypedTranslation.lagda.md +++ b/plutus-metatheory/src/VerifiedCompilation/UntypedTranslation.lagda.md @@ -12,6 +12,8 @@ import Relation.Unary as Unary using (Decidable) import Relation.Binary as Binary using (Decidable) open import Relation.Nullary.Product 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) @@ -26,168 +28,233 @@ 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. +we can build a decision procedure to apply them recursivley down the AST structure. ``` -Relation = { X : Set } → (X ⊢) → (X ⊢) → Set₁ +Relation = { X : Set } → {{_ : DecEq X}} → (X ⊢) → (X ⊢) → Set₁ -data Translation (R : Relation) : { X : Set } → (X ⊢) → (X ⊢) → Set₁ where - istranslation : { X : Set } → (ast ast' : X ⊢) → R ast ast' → Translation R ast ast' - var : { X : Set } → {x : X} → Translation R (` x) (` x) -- We assume we won't want to translate variables individually? - ƛ : { X : Set } → {x x' : Maybe X ⊢} +data Translation (R : Relation) { X : Set } {{_ : DecEq X}} : (X ⊢) → (X ⊢) → Set₁ where + istranslation : {ast ast' : X ⊢} → R ast ast' → Translation R ast ast' + var : {x : X} → Translation R (` x) (` x) -- We assume we won't want to translate variables individually? + ƛ : {x x' : Maybe X ⊢} → Translation R x x' ---------------------- - → Translation R (ƛ x) (ƛ x') - app : { X : Set } → {f t f' t' : X ⊢} → + → Translation R (ƛ x) (ƛ x') + app : {f t f' t' : X ⊢} → Translation R f f' → Translation R t t' → Translation R (f · t) (f' · t') - force : { X : Set } → {t t' : X ⊢} → + force : {t t' : X ⊢} → Translation R t t' → - Translation R (force t) (force t') - delay : { X : Set } → {t t' : X ⊢} → + Translation R (force t) (force t') + delay : {t t' : X ⊢} → Translation R t t' → - Translation R (delay t) (delay t') - con : { X : Set } → {tc : TmCon} → Translation R {X} (con tc) (con tc) - constr : { X : Set } → {xs xs' : List (X ⊢)} { n : ℕ } + Translation R (delay t) (delay t') + con : {tc : TmCon} → Translation R {X} (con tc) (con tc) + constr : {xs xs' : List (X ⊢)} { n : ℕ } → Pointwise (Translation R) xs xs' ------------------------ → Translation R (constr n xs) (constr n xs') - case : { X : Set } → {p p' : X ⊢} {alts alts' : List (X ⊢)} + case : {p p' : X ⊢} {alts alts' : List (X ⊢)} → Pointwise (Translation R) alts alts' -- recursive translation for the other case patterns → Translation R p p' ------------------------ → Translation R (case p alts) (case p' alts') - builtin : { X : Set } → {b : Builtin} → Translation R {X} (builtin b) (builtin b) - error : { X : Set } → Translation R {X} error error + builtin : {b : Builtin} → Translation R {X} (builtin b) (builtin b) + error : Translation R {X} error error ``` For the decision procedure we have the rather dissapointing 110 lines to demonstrate to Agda that, having determine that we aren't in the translation pattern, we are in fact, still not in the translation pattern -for each pair of term types. +for each pair of term types. + ``` --- Yes, I know, but for now... -{-# TERMINATING #-} -translation? : {X' : Set} {{ _ : DecEq X'}} → {R : Relation} → ({ X : Set } {{ _ : DecEq X}} → Binary.Decidable (R {X})) → Binary.Decidable (Translation R {X'}) -translation? isR? ast ast' with (isR? ast ast') -... | yes p = yes (istranslation ast ast' p) +open import Data.Product + +translation? + : {X' : Set} {{ _ : DecEq X'}} {R : Relation} + → ({ X : Set } {{ _ : DecEq X}} → Binary.Decidable (R {X})) + → Binary.Decidable (Translation R {X'}) + +decPointwiseTranslation? + : {X' : Set} {{ _ : DecEq X'}} {R : Relation} + → ({ X : Set } {{ _ : DecEq X}} → 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 (isR? ast ast') +... | yes p = yes (istranslation p) translation? isR? (` x) ast' | no ¬p with (` x) ≟ ast' ... | yes refl = yes var ... | no ¬x=x = no λ { - (istranslation _ _ xx) → ¬p (xx); + (istranslation xx) → ¬p xx; var → ¬x=x refl } translation? isR? (ƛ ast) (ƛ ast') | no ¬p with translation? isR? ast ast' ... | yes p = yes (ƛ p) -... | no ¬pp = no (λ { (istranslation .(ƛ ast) .(ƛ ast') x) → ¬p x ; (ƛ xxx) → ¬pp xxx}) -translation? isR? (ƛ ast) (` x) | no ¬p = no λ { (istranslation _ _ x₁) → ¬p x₁ } -translation? isR? (ƛ ast) (ast'' · ast''') | no ¬p = no λ { (istranslation _ _ x₁) → ¬p x₁ } -translation? isR? (ƛ ast) (force ast'') | no ¬p = no λ { (istranslation _ _ x₁) → ¬p x₁ } -translation? isR? (ƛ ast) (delay ast'') | no ¬p = no λ { (istranslation _ _ x₁) → ¬p x₁ } -translation? isR? (ƛ ast) (con x) | no ¬p = no λ { (istranslation _ _ x₁) → ¬p x₁ } -translation? isR? (ƛ ast) (constr i xs) | no ¬p = no λ { (istranslation _ _ x₁) → ¬p x₁ } -translation? isR? (ƛ ast) (case ast'' ts) | no ¬p = no λ { (istranslation _ _ x₁) → ¬p x₁ } -translation? isR? (ƛ ast) (builtin b) | no ¬p = no λ { (istranslation _ _ x₁) → ¬p x₁ } -translation? isR? (ƛ ast) error | no ¬p = no λ { (istranslation _ _ x₁) → ¬p x₁ } - -translation? isR? (ast · ast₁) (` x) | no ¬p = no λ { (istranslation _ _ x₁) → ¬p x₁ } -translation? isR? (ast · ast₁) (ƛ ast') | no ¬p = no λ { (istranslation _ _ x₁) → ¬p x₁ } +... | no ¬pp = no (λ { (istranslation x) → ¬p x ; (ƛ xxx) → ¬pp xxx}) +translation? isR? (ƛ ast) (` x) | no ¬p = no λ { (istranslation x₁) → ¬p x₁ } +translation? isR? (ƛ ast) (ast'' · ast''') | no ¬p = no λ { (istranslation x₁) → ¬p x₁ } +translation? isR? (ƛ ast) (force ast'') | no ¬p = no λ { (istranslation x₁) → ¬p x₁ } +translation? isR? (ƛ ast) (delay ast'') | no ¬p = no λ { (istranslation x₁) → ¬p x₁ } +translation? isR? (ƛ ast) (con x) | no ¬p = no λ { (istranslation x₁) → ¬p x₁ } +translation? isR? (ƛ ast) (constr i xs) | no ¬p = no λ { (istranslation x₁) → ¬p x₁ } +translation? isR? (ƛ ast) (case ast'' ts) | no ¬p = no λ { (istranslation x₁) → ¬p x₁ } +translation? isR? (ƛ ast) (builtin b) | no ¬p = no λ { (istranslation x₁) → ¬p x₁ } +translation? isR? (ƛ ast) error | no ¬p = no λ { (istranslation x₁) → ¬p x₁ } + +translation? isR? (ast · ast₁) (` x) | no ¬p = no λ { (istranslation x₁) → ¬p x₁ } +translation? isR? (ast · ast₁) (ƛ ast') | no ¬p = no λ { (istranslation x₁) → ¬p x₁ } translation? isR? (ast · ast₁) (ast' · ast'') | no ¬p with (translation? isR? ast ast') ×-dec (translation? isR? ast₁ ast'') ... | yes (p , q) = yes (app p q) -... | no ¬ppqq = no λ { (istranslation _ _ x) → ¬p x ; (app ppp ppp₁) → ¬ppqq (ppp , ppp₁)} -translation? isR? (ast · ast₁) (force ast') | no ¬p = no λ { (istranslation _ _ x₁) → ¬p x₁ } -translation? isR? (ast · ast₁) (delay ast') | no ¬p = no λ { (istranslation _ _ x₁) → ¬p x₁ } -translation? isR? (ast · ast₁) (con x) | no ¬p = no λ { (istranslation _ _ x₁) → ¬p x₁ } -translation? isR? (ast · ast₁) (constr i xs) | no ¬p = no λ { (istranslation _ _ x₁) → ¬p x₁ } -translation? isR? (ast · ast₁) (case ast' ts) | no ¬p = no λ { (istranslation _ _ x₁) → ¬p x₁ } -translation? isR? (ast · ast₁) (builtin b) | no ¬p = no λ { (istranslation _ _ x₁) → ¬p x₁ } -translation? isR? (ast · ast₁) error | no ¬p = no λ { (istranslation _ _ x₁) → ¬p x₁ } - -translation? isR? (force ast) (` x) | no ¬p = no λ { (istranslation _ _ x₁) → ¬p x₁ } -translation? isR? (force ast) (ƛ ast') | no ¬p = no λ { (istranslation _ _ x₁) → ¬p x₁ } -translation? isR? (force ast) (ast' · ast'') | no ¬p = no λ { (istranslation _ _ x₁) → ¬p x₁ } +... | no ¬ppqq = no λ { (istranslation x) → ¬p x ; (app ppp ppp₁) → ¬ppqq (ppp , ppp₁)} +translation? isR? (ast · ast₁) (force ast') | no ¬p = no λ { (istranslation x₁) → ¬p x₁ } +translation? isR? (ast · ast₁) (delay ast') | no ¬p = no λ { (istranslation x₁) → ¬p x₁ } +translation? isR? (ast · ast₁) (con x) | no ¬p = no λ { (istranslation x₁) → ¬p x₁ } +translation? isR? (ast · ast₁) (constr i xs) | no ¬p = no λ { (istranslation x₁) → ¬p x₁ } +translation? isR? (ast · ast₁) (case ast' ts) | no ¬p = no λ { (istranslation x₁) → ¬p x₁ } +translation? isR? (ast · ast₁) (builtin b) | no ¬p = no λ { (istranslation x₁) → ¬p x₁ } +translation? isR? (ast · ast₁) error | no ¬p = no λ { (istranslation x₁) → ¬p x₁ } + +translation? isR? (force ast) (` x) | no ¬p = no λ { (istranslation x₁) → ¬p x₁ } +translation? isR? (force ast) (ƛ ast') | no ¬p = no λ { (istranslation x₁) → ¬p x₁ } +translation? isR? (force ast) (ast' · ast'') | no ¬p = no λ { (istranslation x₁) → ¬p x₁ } translation? isR? (force ast) (force ast') | no ¬p with translation? isR? ast ast' ... | yes p = yes (force p) -... | no ¬pp = no λ { (istranslation .(force ast) .(force ast') x) → ¬p x ; (force xxx) → ¬pp xxx } -translation? isR? (force ast) (delay ast') | no ¬p = no λ { (istranslation _ _ x₁) → ¬p x₁ } -translation? isR? (force ast) (con x) | no ¬p = no λ { (istranslation _ _ x₁) → ¬p x₁ } -translation? isR? (force ast) (constr i xs) | no ¬p = no λ { (istranslation _ _ x₁) → ¬p x₁ } -translation? isR? (force ast) (case ast' ts) | no ¬p = no λ { (istranslation _ _ x₁) → ¬p x₁ } -translation? isR? (force ast) (builtin b) | no ¬p = no λ { (istranslation _ _ x₁) → ¬p x₁ } -translation? isR? (force ast) error | no ¬p = no λ { (istranslation _ _ x₁) → ¬p x₁ } - -translation? isR? (delay ast) (` x) | no ¬p = no λ { (istranslation _ _ x₁) → ¬p x₁ } -translation? isR? (delay ast) (ƛ ast') | no ¬p = no λ { (istranslation _ _ x₁) → ¬p x₁ } -translation? isR? (delay ast) (ast' · ast'') | no ¬p = no λ { (istranslation _ _ x₁) → ¬p x₁ } -translation? isR? (delay ast) (force ast') | no ¬p = no λ { (istranslation _ _ x₁) → ¬p x₁ } +... | no ¬pp = no λ { (istranslation x) → ¬p x ; (force xxx) → ¬pp xxx } +translation? isR? (force ast) (delay ast') | no ¬p = no λ { (istranslation x₁) → ¬p x₁ } +translation? isR? (force ast) (con x) | no ¬p = no λ { (istranslation x₁) → ¬p x₁ } +translation? isR? (force ast) (constr i xs) | no ¬p = no λ { (istranslation x₁) → ¬p x₁ } +translation? isR? (force ast) (case ast' ts) | no ¬p = no λ { (istranslation x₁) → ¬p x₁ } +translation? isR? (force ast) (builtin b) | no ¬p = no λ { (istranslation x₁) → ¬p x₁ } +translation? isR? (force ast) error | no ¬p = no λ { (istranslation x₁) → ¬p x₁ } + +translation? isR? (delay ast) (` x) | no ¬p = no λ { (istranslation x₁) → ¬p x₁ } +translation? isR? (delay ast) (ƛ ast') | no ¬p = no λ { (istranslation x₁) → ¬p x₁ } +translation? isR? (delay ast) (ast' · ast'') | no ¬p = no λ { (istranslation x₁) → ¬p x₁ } +translation? isR? (delay ast) (force ast') | no ¬p = no λ { (istranslation x₁) → ¬p x₁ } translation? isR? (delay ast) (delay ast') | no ¬p with translation? isR? ast ast' ... | yes p = yes (delay p) -... | no ¬pp = no λ { (istranslation .(delay ast) .(delay ast') x) → ¬p x ; (delay xxx) → ¬pp xxx } -translation? isR? (delay ast) (con x) | no ¬p = no λ { (istranslation _ _ x₁) → ¬p x₁ } -translation? isR? (delay ast) (constr i xs) | no ¬p = no λ { (istranslation _ _ x₁) → ¬p x₁ } -translation? isR? (delay ast) (case ast' ts) | no ¬p = no λ { (istranslation _ _ x₁) → ¬p x₁ } -translation? isR? (delay ast) (builtin b) | no ¬p = no λ { (istranslation _ _ x₁) → ¬p x₁ } -translation? isR? (delay ast) error | no ¬p = no λ { (istranslation _ _ x₁) → ¬p x₁ } - -translation? isR? (con x) (` x₁) | no ¬p = no λ { (istranslation _ _ x₁) → ¬p x₁ } -translation? isR? (con x) (ƛ ast') | no ¬p = no λ { (istranslation _ _ x₁) → ¬p x₁ } -translation? isR? (con x) (ast' · ast'') | no ¬p = no λ { (istranslation _ _ x₁) → ¬p x₁ } -translation? isR? (con x) (force ast') | no ¬p = no λ { (istranslation _ _ x₁) → ¬p x₁ } -translation? isR? (con x) (delay ast') | no ¬p = no λ { (istranslation _ _ x₁) → ¬p x₁ } +... | no ¬pp = no λ { (istranslation x) → ¬p x ; (delay xxx) → ¬pp xxx } +translation? isR? (delay ast) (con x) | no ¬p = no λ { (istranslation x₁) → ¬p x₁ } +translation? isR? (delay ast) (constr i xs) | no ¬p = no λ { (istranslation x₁) → ¬p x₁ } +translation? isR? (delay ast) (case ast' ts) | no ¬p = no λ { (istranslation x₁) → ¬p x₁ } +translation? isR? (delay ast) (builtin b) | no ¬p = no λ { (istranslation x₁) → ¬p x₁ } +translation? isR? (delay ast) error | no ¬p = no λ { (istranslation x₁) → ¬p x₁ } + +translation? isR? (con x) (` x₁) | no ¬p = no λ { (istranslation x₁) → ¬p x₁ } +translation? isR? (con x) (ƛ ast') | no ¬p = no λ { (istranslation x₁) → ¬p x₁ } +translation? isR? (con x) (ast' · ast'') | no ¬p = no λ { (istranslation x₁) → ¬p x₁ } +translation? isR? (con x) (force ast') | no ¬p = no λ { (istranslation x₁) → ¬p x₁ } +translation? isR? (con x) (delay ast') | no ¬p = no λ { (istranslation x₁) → ¬p x₁ } translation? isR? (con x) (con x₁) | no ¬p with x ≟ x₁ ... | yes refl = yes con -... | no ¬x≟x₁ = no λ { (istranslation .(con x) .(con x₁) xx) → ¬p xx ; con → ¬x≟x₁ refl } -translation? isR? (con x) (constr i xs) | no ¬p = no λ { (istranslation _ _ x₁) → ¬p x₁ } -translation? isR? (con x) (case ast' ts) | no ¬p = no λ { (istranslation _ _ x₁) → ¬p x₁ } -translation? isR? (con x) (builtin b) | no ¬p = no λ { (istranslation _ _ x₁) → ¬p x₁ } -translation? isR? (con x) error | no ¬p = no λ { (istranslation _ _ x₁) → ¬p x₁ } - -translation? isR? (constr i xs) (` x) | no ¬p = no λ { (istranslation _ _ x₁) → ¬p x₁ } -translation? isR? (constr i xs) (ƛ ast') | no ¬p = no λ { (istranslation _ _ x₁) → ¬p x₁ } -translation? isR? (constr i xs) (ast' · ast'') | no ¬p = no λ { (istranslation _ _ x₁) → ¬p x₁ } -translation? isR? (constr i xs) (force ast') | no ¬p = no λ { (istranslation _ _ x₁) → ¬p x₁ } -translation? isR? (constr i xs) (delay ast') | no ¬p = no λ { (istranslation _ _ x₁) → ¬p x₁ } -translation? isR? (constr i xs) (con x) | no ¬p = no λ { (istranslation _ _ x₁) → ¬p x₁ } -translation? isR? (constr i xs) (constr i₁ xs₁) | no ¬p with (i ≟ i₁) ×-dec (decPointwise (translation? isR?) xs xs₁) +... | no ¬x≟x₁ = no λ { (istranslation xx) → ¬p xx ; con → ¬x≟x₁ refl } +translation? isR? (con x) (constr i xs) | no ¬p = no λ { (istranslation x₁) → ¬p x₁ } +translation? isR? (con x) (case ast' ts) | no ¬p = no λ { (istranslation x₁) → ¬p x₁ } +translation? isR? (con x) (builtin b) | no ¬p = no λ { (istranslation x₁) → ¬p x₁ } +translation? isR? (con x) error | no ¬p = no λ { (istranslation x₁) → ¬p x₁ } + +translation? isR? (constr i xs) (` x) | no ¬p = no λ { (istranslation x₁) → ¬p x₁ } +translation? isR? (constr i xs) (ƛ ast') | no ¬p = no λ { (istranslation x₁) → ¬p x₁ } +translation? isR? (constr i xs) (ast' · ast'') | no ¬p = no λ { (istranslation x₁) → ¬p x₁ } +translation? isR? (constr i xs) (force ast') | no ¬p = no λ { (istranslation x₁) → ¬p x₁ } +translation? isR? (constr i xs) (delay ast') | no ¬p = no λ { (istranslation x₁) → ¬p x₁ } +translation? isR? (constr i xs) (con x) | no ¬p = no λ { (istranslation x₁) → ¬p x₁ } +translation? isR? (constr i xs) (constr i₁ xs₁) | no ¬p with (i ≟ i₁) ×-dec (decPointwiseTranslation? isR? xs xs₁) ... | yes (refl , pxs) = yes (constr pxs) -... | no ¬ixs = no λ { (istranslation _ _ x) → ¬p x ; (constr x) → ¬ixs (refl , x) } -translation? isR? (constr i xs) (case ast' ts) | no ¬p = no λ { (istranslation _ _ x₁) → ¬p x₁ } -translation? isR? (constr i xs) (builtin b) | no ¬p = no λ { (istranslation _ _ x₁) → ¬p x₁ } -translation? isR? (constr i xs) error | no ¬p = no λ { (istranslation _ _ x₁) → ¬p x₁ } - -translation? isR? (case ast ts) (` x) | no ¬p = no λ { (istranslation _ _ x₁) → ¬p x₁ } -translation? isR? (case ast ts) (ƛ ast') | no ¬p = no λ { (istranslation _ _ x₁) → ¬p x₁ } -translation? isR? (case ast ts) (ast' · ast'') | no ¬p = no λ { (istranslation _ _ x₁) → ¬p x₁ } -translation? isR? (case ast ts) (force ast') | no ¬p = no λ { (istranslation _ _ x₁) → ¬p x₁ } -translation? isR? (case ast ts) (delay ast') | no ¬p = no λ { (istranslation _ _ x₁) → ¬p x₁ } -translation? isR? (case ast ts) (con x) | no ¬p = no λ { (istranslation _ _ x₁) → ¬p x₁ } -translation? isR? (case ast ts) (constr i xs) | no ¬p = no λ { (istranslation _ _ x₁) → ¬p x₁ } -translation? isR? (case ast ts) (case ast' ts₁) | no ¬p with (translation? isR? ast ast') ×-dec (decPointwise (translation? isR?) ts ts₁) +... | no ¬ixs = no λ { (istranslation x) → ¬p x ; (constr x) → ¬ixs (refl , x) } +translation? isR? (constr i xs) (case ast' ts) | no ¬p = no λ { (istranslation x₁) → ¬p x₁ } +translation? isR? (constr i xs) (builtin b) | no ¬p = no λ { (istranslation x₁) → ¬p x₁ } +translation? isR? (constr i xs) error | no ¬p = no λ { (istranslation x₁) → ¬p x₁ } + +translation? isR? (case ast ts) (` x) | no ¬p = no λ { (istranslation x₁) → ¬p x₁ } +translation? isR? (case ast ts) (ƛ ast') | no ¬p = no λ { (istranslation x₁) → ¬p x₁ } +translation? isR? (case ast ts) (ast' · ast'') | no ¬p = no λ { (istranslation x₁) → ¬p x₁ } +translation? isR? (case ast ts) (force ast') | no ¬p = no λ { (istranslation x₁) → ¬p x₁ } +translation? isR? (case ast ts) (delay ast') | no ¬p = no λ { (istranslation x₁) → ¬p x₁ } +translation? isR? (case ast ts) (con x) | no ¬p = no λ { (istranslation x₁) → ¬p x₁ } +translation? isR? (case ast ts) (constr i xs) | no ¬p = no λ { (istranslation x₁) → ¬p x₁ } +translation? isR? (case ast ts) (case ast' ts₁) | no ¬p with (translation? isR? ast ast') ×-dec (decPointwiseTranslation? isR? ts ts₁) ... | yes ( pa , pts ) = yes (case pts pa) -... | no ¬papts = no λ { (istranslation _ _ x) → ¬p x ; (case x xxx) → ¬papts (xxx , x) } -translation? isR? (case ast ts) (builtin b) | no ¬p = no λ { (istranslation _ _ x₁) → ¬p x₁ } -translation? isR? (case ast ts) error | no ¬p = no λ { (istranslation _ _ x₁) → ¬p x₁ } - -translation? isR? (builtin b) (` x) | no ¬p = no λ { (istranslation _ _ x₁) → ¬p x₁ } -translation? isR? (builtin b) (ƛ ast') | no ¬p = no λ { (istranslation _ _ x₁) → ¬p x₁ } -translation? isR? (builtin b) (ast' · ast'') | no ¬p = no λ { (istranslation _ _ x₁) → ¬p x₁ } -translation? isR? (builtin b) (force ast') | no ¬p = no λ { (istranslation _ _ x₁) → ¬p x₁ } -translation? isR? (builtin b) (delay ast') | no ¬p = no λ { (istranslation _ _ x₁) → ¬p x₁ } -translation? isR? (builtin b) (con x) | no ¬p = no λ { (istranslation _ _ x₁) → ¬p x₁ } -translation? isR? (builtin b) (constr i xs) | no ¬p = no λ { (istranslation _ _ x₁) → ¬p x₁ } -translation? isR? (builtin b) (case ast' ts) | no ¬p = no λ { (istranslation _ _ x₁) → ¬p x₁ } +... | no ¬papts = no λ { (istranslation x) → ¬p x ; (case x xxx) → ¬papts (xxx , x) } +translation? isR? (case ast ts) (builtin b) | no ¬p = no λ { (istranslation x₁) → ¬p x₁ } +translation? isR? (case ast ts) error | no ¬p = no λ { (istranslation x₁) → ¬p x₁ } + +translation? isR? (builtin b) (` x) | no ¬p = no λ { (istranslation x₁) → ¬p x₁ } +translation? isR? (builtin b) (ƛ ast') | no ¬p = no λ { (istranslation x₁) → ¬p x₁ } +translation? isR? (builtin b) (ast' · ast'') | no ¬p = no λ { (istranslation x₁) → ¬p x₁ } +translation? isR? (builtin b) (force ast') | no ¬p = no λ { (istranslation x₁) → ¬p x₁ } +translation? isR? (builtin b) (delay ast') | no ¬p = no λ { (istranslation x₁) → ¬p x₁ } +translation? isR? (builtin b) (con x) | no ¬p = no λ { (istranslation x₁) → ¬p x₁ } +translation? isR? (builtin b) (constr i xs) | no ¬p = no λ { (istranslation x₁) → ¬p x₁ } +translation? isR? (builtin b) (case ast' ts) | no ¬p = no λ { (istranslation x₁) → ¬p x₁ } translation? isR? (builtin b) (builtin b₁) | no ¬p with b ≟ b₁ ... | yes refl = yes builtin -... | no ¬b=b₁ = no λ { (istranslation _ _ x) → ¬p x ; builtin → ¬b=b₁ refl } -translation? isR? (builtin b) error | no ¬p = no λ { (istranslation _ _ x₁) → ¬p x₁ } - -translation? isR? error (` x) | no ¬p = no λ { (istranslation _ _ x₁) → ¬p x₁ } -translation? isR? error (ƛ ast') | no ¬p = no λ { (istranslation _ _ x₁) → ¬p x₁ } -translation? isR? error (ast' · ast'') | no ¬p = no λ { (istranslation _ _ x₁) → ¬p x₁ } -translation? isR? error (force ast') | no ¬p = no λ { (istranslation _ _ x₁) → ¬p x₁ } -translation? isR? error (delay ast') | no ¬p = no λ { (istranslation _ _ x₁) → ¬p x₁ } -translation? isR? error (con x) | no ¬p = no λ { (istranslation _ _ x₁) → ¬p x₁ } -translation? isR? error (constr i xs) | no ¬p = no λ { (istranslation _ _ x₁) → ¬p x₁ } -translation? isR? error (case ast' ts) | no ¬p = no λ { (istranslation _ _ x₁) → ¬p x₁ } -translation? isR? error (builtin b) | no ¬p = no λ { (istranslation _ _ x₁) → ¬p x₁ } +... | no ¬b=b₁ = no λ { (istranslation x) → ¬p x ; builtin → ¬b=b₁ refl } +translation? isR? (builtin b) error | no ¬p = no λ { (istranslation x₁) → ¬p x₁ } + +translation? isR? error (` x) | no ¬p = no λ { (istranslation x₁) → ¬p x₁ } +translation? isR? error (ƛ ast') | no ¬p = no λ { (istranslation x₁) → ¬p x₁ } +translation? isR? error (ast' · ast'') | no ¬p = no λ { (istranslation x₁) → ¬p x₁ } +translation? isR? error (force ast') | no ¬p = no λ { (istranslation x₁) → ¬p x₁ } +translation? isR? error (delay ast') | no ¬p = no λ { (istranslation x₁) → ¬p x₁ } +translation? isR? error (con x) | no ¬p = no λ { (istranslation x₁) → ¬p x₁ } +translation? isR? error (constr i xs) | no ¬p = no λ { (istranslation x₁) → ¬p x₁ } +translation? isR? error (case ast' ts) | no ¬p = no λ { (istranslation x₁) → ¬p x₁ } +translation? isR? error (builtin b) | no ¬p = no λ { (istranslation x₁) → ¬p x₁ } translation? isR? error error | no ¬p = yes error ``` +# 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 : {{deX : DecEq X}} → (∀ {Y : Set} {{deY : DecEq Y}} {y y' : Y ⊢} → R {{deY}} y y' → S {{deY}} y y') → (Pointwise (R {{deX}}) xs xs' → Pointwise (S {{deX}}) 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 : {{deX : DecEq X}} → (∀ {Y : Set} {{deY : DecEq Y}} {y y' : Y ⊢} → R y y' → S y y') → (Translation R {{deX}} x x' → Translation S {{deX}} x x') +convert f (Translation.istranslation xx') = Translation.istranslation (f xx') +convert f Translation.var = Translation.var +convert f (Translation.ƛ xx') = Translation.ƛ (convert f xx') +convert f (Translation.app xx' xx'') = Translation.app (convert f xx') (convert f xx'') +convert f (Translation.force xx') = Translation.force (convert f xx') +convert f (Translation.delay xx') = Translation.delay (convert f xx') +convert f Translation.con = Translation.con +convert {R = R} {S = S} f (Translation.constr x) = Translation.constr (convert-pointwise {R = Translation R} {S = Translation S} (convert f) x) +convert f (case Pointwise.[] xx') = case Pointwise.[] (convert f xx') +convert {R = R} {S = S} f (case (x∼y Pointwise.∷ x) xx') = Translation.case (convert-pointwise {R = Translation R} {S = Translation S} (convert f) (x∼y Pointwise.∷ x)) (convert f xx') +convert f Translation.builtin = Translation.builtin +convert f Translation.error = Translation.error + +pointwise-reflexive : (∀ {X : Set} {{deX : DecEq X}} {x : X ⊢} → Translation R {{deX}} x x) → (∀ {X : Set} {{deX : DecEq X}} {xs : List (X ⊢)} → Pointwise (Translation R {{deX}}) xs xs) +pointwise-reflexive f {xs = List.[]} = Pointwise.[] +pointwise-reflexive f {xs = x List.∷ xs} = f Pointwise.∷ pointwise-reflexive f + +{-# TERMINATING #-} +reflexive : {{deX : DecEq X}} → Translation R {{deX}} x x +reflexive {x = ` x} = var +reflexive {x = ƛ x} = ƛ reflexive +reflexive {x = x · x₁} = app reflexive reflexive +reflexive {x = force x} = force reflexive +reflexive {x = delay x} = delay reflexive +reflexive {x = con x} = con +reflexive {x = constr i xs} = constr (pointwise-reflexive reflexive) +reflexive {x = case x ts} = case (pointwise-reflexive reflexive) reflexive +reflexive {x = builtin b} = builtin +reflexive {x = error} = error +``` diff --git a/plutus-metatheory/src/VerifiedCompilation/UntypedViews.lagda.md b/plutus-metatheory/src/VerifiedCompilation/UntypedViews.lagda.md index 6b80c4fc9e5..559fc0edd2c 100644 --- a/plutus-metatheory/src/VerifiedCompilation/UntypedViews.lagda.md +++ b/plutus-metatheory/src/VerifiedCompilation/UntypedViews.lagda.md @@ -29,7 +29,7 @@ to recognise that pattern and extract the variables. Following suggestions from Philip Wadler: creating Views for each Term type and then allowing them to accept arbitrary sub-views should make this reusable. We can create patterns using nested calls to these views, and decide them with nested calls to the -decision procedures. +decision procedures. ``` Pred : Set₁