# input-output-hk/plutus-metatheory

more scope safe progress

 @@ -4,6 +4,7 @@ module Scoped.Reduction where \begin{code} open import Scoped open import Scoped.RenamingSubstitution open import Data.Sum renaming (inj₁ to inl; inj₂ to inr) open import Data.Product @@ -28,13 +29,17 @@ data Error {n} : ScopedTm n → Set where E-Λ· : ∀{K}{L : ScopedTm (T n)}{M : ScopedTm n} → Error (Λ K L · M) E-ƛ·⋆ : ∀{B : ScopedTy ∥ n ∥}{L : ScopedTm (S n)}{A : ScopedTy ∥ n ∥} → Error (ƛ B L ·⋆ A) -- place holder for stuff that isn't implemented yet... todo : {M : ScopedTm n} → Error M data _—→_ {n} : ScopedTm n → ScopedTm n → Set where ξ-· : {L L' M : ScopedTm n} → L —→ L' → L · M —→ L' · M ξ-·⋆ : {L L' : ScopedTm n}{A : ScopedTy ∥ n ∥} → L —→ L' → L ·⋆ A —→ L' ·⋆ A β-ƛ : {A : ScopedTy ∥ n ∥}{L : ScopedTm (S n)}{M : ScopedTm n} → (ƛ A L) · M —→ {!!} → (ƛ A L) · M —→ (L [ M ]) β-Λ : ∀{K}{L : ScopedTm (T n)}{A : ScopedTy ∥ n ∥} → (Λ K L) ·⋆ A —→ {!!} → (Λ K L) ·⋆ A —→ (L [ A ]⋆) \end{code} \begin{code} @@ -44,32 +49,34 @@ data _—→⋆_ {n} : ScopedTm n → ScopedTm n → Set where \end{code} \begin{code} progress : (t : ScopedTm Z) → (Value {Z} t ⊎ Error t) ⊎ Σ (ScopedTm Z) λ t' → t —→ t' progress : (t : ScopedTm Z) → (Value {Z} t ⊎ Error t) ⊎ Σ (ScopedTm Z) λ t' → t —→ t' progress ( ()) progress (Λ K t) = inl (inl (V-Λ K t)) progress (t ·⋆ A) with progress t progress (.(ƛ B t) ·⋆ A) | inl (inl (V-ƛ B t)) = inl (inr E-ƛ·⋆) progress (.(Λ K t) ·⋆ A) | inl (inl (V-Λ K t)) = inr ({!!} , β-Λ) progress (.(Λ K t) ·⋆ A) | inl (inl (V-Λ K t)) = inr (t [ A ]⋆ , β-Λ) progress (t ·⋆ A) | inl (inr p) = inl (inr (E-·⋆ p)) progress (t ·⋆ A) | inr (t' , p) = inr (t' ·⋆ A , ξ-·⋆ p) progress (ƛ A t) = inl (inl (V-ƛ A t)) progress (t · u) with progress t progress (.(ƛ A t) · u) | inl (inl (V-ƛ A t)) = inr ({!!} , β-ƛ) progress (.(ƛ A t) · u) | inl (inl (V-ƛ A t)) = inr (t [ u ] , β-ƛ) progress (.(Λ K t) · u) | inl (inl (V-Λ K t)) = inl (inr E-Λ·) progress (t · u) | inl (inr p) = inl (inr (E-· p)) progress (t · u) | inr (t' , p) = inr (t' · u , ξ-· p) progress (con x) = {!!} progress (con x) = inl (inr todo) progress (error p) = inl (inr (E-error p)) progress (builtin x) = {!!} progress (builtin x) = inl (inr todo) \end{code} \begin{code} open import Data.Nat open import Data.Maybe run : (t : ScopedTm Z) → ℕ → Σ (ScopedTm Z) λ t' → t —→⋆ t' × (Maybe (Value t') ⊎ Error t') run t 0 = t , (refl , inl nothing) run : (t : ScopedTm Z) → ℕ → Σ (ScopedTm Z) λ t' → t —→⋆ t' × (Maybe (Value t') ⊎ Error t') run t 0 = t , (refl , inl nothing) -- out of fuel run t (suc n) with progress t run t (suc n) | inl (inl vt) = t , refl , inl (just vt) run t (suc n) | inl (inr et) = t , refl , inr et