\begin{code}
module Untyped.Reduction where
\end{code}
\begin{code}
open import Untyped
open import Untyped.RenamingSubstitution
open import Builtin
open import Builtin.Constant.Type hiding (length)
open import Agda.Builtin.String using (primStringFromList; primStringAppend)
open import Data.Bool using (Bool;true;false)
open import Data.Nat using (ℕ;suc;zero;_<‴_;_≤‴_;≤‴-refl;≤‴-step)
open import Data.Integer using (_+_;_-_;_*_;∣_∣;_<?_;_≤?_;_≟_)
open import Data.Product renaming (proj₁ to fst; proj₂ to snd)
open import Data.Sum renaming (inj₁ to inl; inj₂ to inr)
import Data.List as List
open import Data.Vec using (Vec;[];_∷_;_++_)
open import Data.Unit hiding (_≤_; _≤?_; _≟_)
import Debug.Trace as Debug
open import Function
open import Relation.Binary.PropositionalEquality hiding ([_])
open import Utils
open import Data.Fin using ()
\end{code}
\begin{code}
infix 2 _—→_
\end{code}
\begin{code}
subst∷ : ∀{n n'}{A : Set}(a : A)(as : Vec A n)(p : n ≡ n')(q : suc n ≡ suc n')
→ a ∷ subst (Vec A) p as ≡ subst (Vec A) q (a ∷ as)
subst∷ a as refl refl = refl
\end{code}
\begin{code}
data Error {n} : n ⊢ → Set where
E-error : Error error
\end{code}
\begin{code}
data FValue {n} : n ⊢ → Set where
V-ƛ : (t : suc n ⊢) → FValue (ƛ t)
V-builtin : (b : Builtin)
→ ∀{l}
→ (ts : Tel l n)
→ (p : l <‴ arity b)
→ FValue (builtin b (≤‴-step p) ts)
data Value {n} : n ⊢ → Set where
V-F : {t : n ⊢} → FValue t → Value t
V-con : (tcn : TermCon) → Value (con {n} tcn)
data Any {n : ℕ}(P : n ⊢ → Set) : ∀{m} → Tel m n → Set where
here : ∀{m t}{ts : Tel m n} → P t → Any P (t ∷ ts)
there : ∀{m t}{ts : Tel m n} → Value t → Any P ts → Any P (t ∷ ts)
_∈_ : {m n : ℕ} → n ⊢ → Tel m n → Set
t ∈ ts = Any (_≡ t) ts
VTel : ∀ l n → Tel l n → Set
VTel 0 n [] = ⊤
VTel (suc l) n (t ∷ ts) = Value {n} t × VTel l n ts
BUILTIN : ∀{n}
→ (b : Builtin)
→ (tel : Tel (arity b) n)
→ VTel (arity b) n tel
→ n ⊢
data _—→T_ {n} : ∀{m} → Tel m n → Tel m n → Set
data _—→_ {n} : n ⊢ → n ⊢ → Set where
ξ-·₁ : {L L' M : n ⊢} → L —→ L' → L · M —→ L' · M
ξ-·₂ : {L M M' : n ⊢} → FValue L → M —→ M' → L · M —→ L · M'
β-ƛ : ∀{L : suc n ⊢}{V : n ⊢} → Value V → ƛ L · V —→ L [ V ]
ξ-builtin : (b : Builtin)
{ts ts' : Tel (arity b) n}
→ ts —→T ts'
→ builtin b ≤‴-refl ts —→ builtin b ≤‴-refl ts'
β-builtin : {b : Builtin}
(ts : Tel (arity b) n)
→ (vs : VTel (arity b) n ts)
→ builtin b ≤‴-refl ts —→ BUILTIN b ts vs
sat-builtin : {b : Builtin}
→ ∀{l}
{ts : Tel l n}
{t : n ⊢}
→ Value t
→ (p : l <‴ arity b)
→ builtin b (≤‴-step p) ts · t —→ builtin b p (ts :< t)
E-·₁ : {M : n ⊢} → error · M —→ error
E-·₂ : {L : n ⊢} → FValue L → L · error —→ error
E-builtin : (b : Builtin)
(ts : Tel (arity b) n)
→ Any Error ts
→ builtin b ≤‴-refl ts —→ error
E-con : {tcn : TermCon}{L : n ⊢} → con tcn · L —→ error
data _—→T_ {n} where
here : ∀{m t t'}{ts : Tel m n} → t —→ t' → (t ∷ ts) —→T (t' ∷ ts)
there : ∀{m t}{ts ts' : Tel m n}
→ Value t → ts —→T ts' → (t ∷ ts) —→T (t ∷ ts')
\end{code}
\begin{code}
data _—→⋆_ {n} : n ⊢ → n ⊢ → Set where
refl : {t : n ⊢} → t —→⋆ t
trans—→⋆ : {t t' t'' : n ⊢} → t —→ t' → t' —→⋆ t'' → t —→⋆ t''
\end{code}
\begin{code}
VERIFYSIG : ∀{n} → Maybe Bool → n ⊢
VERIFYSIG (just Bool.false) = plc_false
VERIFYSIG (just Bool.true) = plc_true
VERIFYSIG nothing = error
BUILTIN addInteger (_ ∷ _ ∷ []) (V-con (integer i) , V-con (integer j) , _)
= con (integer (i + j))
BUILTIN subtractInteger (_ ∷ _ ∷ []) (V-con (integer i) , V-con (integer j) , _)
= con (integer (i - j))
BUILTIN multiplyInteger (_ ∷ _ ∷ []) (V-con (integer i) , V-con (integer j) , _)
= con (integer (i * j))
BUILTIN divideInteger (_ ∷ _ ∷ []) (V-con (integer i) , V-con (integer j) , _)
= decIf (∣ j ∣ Data.Nat.≟ zero) error (con (integer (div i j)))
BUILTIN quotientInteger (_ ∷ _ ∷ []) (V-con (integer i) , V-con (integer j) , _)
= decIf (∣ j ∣ Data.Nat.≟ zero) error (con (integer (quot i j)))
BUILTIN remainderInteger (_ ∷ _ ∷ []) (V-con (integer i) , V-con (integer j) , _)
= decIf (∣ j ∣ Data.Nat.≟ zero) error (con (integer (rem i j)))
BUILTIN modInteger (_ ∷ _ ∷ []) (V-con (integer i) , V-con (integer j) , _)
= decIf (∣ j ∣ Data.Nat.≟ zero) error (con (integer (mod i j)))
BUILTIN lessThanInteger (_ ∷ _ ∷ []) (V-con (integer i) , V-con (integer j) , tt) =
decIf (i <? j) plc_true plc_false
BUILTIN lessThanEqualsInteger (_ ∷ _ ∷ []) (V-con (integer i) , V-con (integer j) , tt) =
decIf (i ≤? j) plc_true plc_false
BUILTIN greaterThanInteger (_ ∷ _ ∷ []) (V-con (integer i) , V-con (integer j) , tt) =
decIf (i Builtin.Constant.Type.>? j) plc_true plc_false
BUILTIN greaterThanEqualsInteger (_ ∷ _ ∷ []) (V-con (integer i) , V-con (integer j) , tt) =
decIf (i Builtin.Constant.Type.≥? j) plc_true plc_false
BUILTIN equalsInteger (_ ∷ _ ∷ []) (V-con (integer i) , V-con (integer j) , tt) =
decIf (i ≟ j) plc_true plc_false
BUILTIN concatenate (_ ∷ _ ∷ []) (V-con (bytestring b) , V-con (bytestring b') , tt) =
con (bytestring (concat b b'))
BUILTIN takeByteString (_ ∷ _ ∷ []) (V-con (integer i) , V-con (bytestring b) , tt) =
con (bytestring (take i b))
BUILTIN dropByteString (_ ∷ _ ∷ []) (V-con (integer i) , V-con (bytestring b) , tt) =
con (bytestring (drop i b))
BUILTIN sha2-256 (_ ∷ []) (V-con (bytestring b) , tt) = con (bytestring (SHA2-256 b))
BUILTIN sha3-256 (_ ∷ []) (V-con (bytestring b) , tt) = con (bytestring (SHA3-256 b))
BUILTIN verifySignature (_ ∷ _ ∷ _ ∷ []) (V-con (bytestring k) , V-con (bytestring d) , V-con (bytestring c) , tt) = VERIFYSIG (verifySig k d c)
BUILTIN equalsByteString (_ ∷ _ ∷ []) (V-con (bytestring b) , V-con (bytestring b') , tt) =
con (bool (equals b b'))
BUILTIN ifThenElse (_ ∷ _ ∷ t ∷ _ ∷ []) (_ , V-con (bool true) , vt , _ , tt) = t
BUILTIN ifThenElse (_ ∷ _ ∷ _ ∷ u ∷ []) (_ , V-con (bool false) , _ , vu , tt) = u
BUILTIN charToString (_ ∷ []) (V-con (char c) , tt) = con (string (primStringFromList List.[ c ]))
BUILTIN append (_ ∷ _ ∷ []) (V-con (string s) , V-con (string t) , tt) =
con (string (primStringAppend s t))
BUILTIN trace (_ ∷ []) (V-con (string s) , tt) = con (Debug.trace s unit)
BUILTIN _ _ _ = error
data ProgTel {l n}(tel : Tel l n) : Set where
done : VTel l n tel → ProgTel tel
step : ∀{tel'} → tel —→T tel' → ProgTel tel
error : Any Error tel → ProgTel tel
data Progress {n}(M : n ⊢) : Set where
step : ∀{N}
→ M —→ N
→ Progress M
done :
Value M
→ Progress M
error :
Error M
→ Progress M
progress-·V : ∀{n}
→ {t : n ⊢} → Value t
→ {u : n ⊢} → Progress u
→ Progress (t · u)
progress-·V (V-con tcn) v = step E-con
progress-·V (V-F v) (step q) = step (ξ-·₂ v q)
progress-·V (V-F v) (error E-error) = step (E-·₂ v)
progress-·V (V-F (V-ƛ t)) (done v) = step (β-ƛ v)
progress-·V (V-F (V-builtin b ts p)) (done v) = step (sat-builtin v p)
progress-· : ∀{n}
→ {t : n ⊢} → Progress t
→ {u : n ⊢} → Progress u
→ Progress (t · u)
progress-· (done v) q = progress-·V v q
progress-· (step p) q = step (ξ-·₁ p)
progress-· (error E-error) q = step E-·₁
progress : (t : 0 ⊢) → Progress t
progressTel : ∀{l}(tel : Tel l 0) → ProgTel tel
progressTel [] = done tt
progressTel (t ∷ ts) with progress t
progressTel (t ∷ ts) | step p = step (here p)
progressTel (t ∷ ts) | done v with progressTel ts
progressTel (t ∷ ts) | done v | done vs = done (v , vs)
progressTel (t ∷ ts) | done v | step p = step (there v p)
progressTel (t ∷ ts) | done v | error e = error (there v e)
progressTel (t ∷ ts) | error e = error (here e)
progress (` ())
progress (ƛ t) = done (V-F (V-ƛ t))
progress (t · u) = progress-· (progress t) (progress u)
progress (con tcn) = done (V-con tcn)
progress (builtin b ≤‴-refl ts) with progressTel ts
progress (builtin b ≤‴-refl ts) | done vs = step (β-builtin ts vs)
progress (builtin b ≤‴-refl ts) | step p = step (ξ-builtin b p)
progress (builtin b ≤‴-refl ts) | error p = step (E-builtin b ts p)
progress (builtin b (≤‴-step p) ts) = done (V-F (V-builtin b ts p))
progress error = error E-error
\end{code}
\begin{code}
run : ∀(t : 0 ⊢) → ℕ
→ Σ (0 ⊢) λ t' → t —→⋆ t' × (Maybe (Value t') ⊎ Error t')
run t 0 = t , refl , inl nothing
run t (suc n) with progress t
run t (suc n) | done vt = t , refl , inl (just vt)
run t (suc n) | error et = t , refl , inr et
run t (suc n) | step {N = t'} p with run t' n
run t (suc n) | step p | t'' , q , mvt'' = t'' , trans—→⋆ p q , mvt''
\end{code}
\begin{code}
open import Data.Empty
open import Relation.Nullary
val-red : ∀{n}{t : n ⊢} → Value t → ¬ (Σ (n ⊢) (t —→_))
val-red (V-F (V-ƛ t)) (t' , ())
val-red (V-F (V-builtin b ts p)) (t' , ())
val-red (V-con tcn) (t' , ())
val-err : ∀{n}{t : n ⊢} → Value t → ¬ (Error t)
val-err (V-con tcn) ()
val-err (V-F (V-ƛ t)) ()
val-err (V-F (V-builtin b ts p)) ()
err-red : ∀{n}{t : n ⊢} → Error t → ¬ (Σ (n ⊢) (t —→_))
err-red E-error (_ , ())
errT-redT : ∀{m n}{ts : Tel m n} → Any Error ts → ¬ (Σ (Tel m n) (ts —→T_))
errT-redT (here p) (.(_ ∷ _) , here q) = err-red p (_ , q)
errT-redT (here p) (.(_ ∷ _) , there v q) = val-err v p
errT-redT (there v p) (.(_ ∷ _) , here q) = val-red v (_ , q)
errT-redT (there v p) (.(_ ∷ _) , there w q) = errT-redT p (_ , q)
valT-errT : ∀{m n}{ts : Tel m n} → VTel m n ts → ¬ (Any Error ts)
valT-errT {ts = t ∷ ts} (v , vs) (here p) = val-err v p
valT-errT {ts = t ∷ ts} (v , vs) (there w p) = valT-errT vs p
valT-redT : ∀{m n}{ts : Tel m n} → VTel m n ts → ¬ (Σ (Tel m n) (ts —→T_))
valT-redT {ts = []} _ (ts' , ())
valT-redT {ts = t ∷ ts} (v , vs) (._ , here p) = val-red v (_ , p)
valT-redT {ts = t ∷ ts} (v , vs) (._ , there v' p) = valT-redT vs (_ , p)
valUniq : ∀{n}{t : n ⊢}(v v' : Value t) → v ≡ v'
valUniq (V-F (V-ƛ t)) (V-F (V-ƛ .t)) = refl
valUniq (V-F (V-builtin b ts p)) (V-F (V-builtin .b .ts .p)) = refl
valUniq (V-con tcn) (V-con .tcn) = refl
valTUniq : ∀{m n}{ts : Tel m n}(vs vs' : VTel m n ts) → vs ≡ vs'
valTUniq {ts = []} _ _ = refl
valTUniq {ts = x ∷ ts} (v , vs) (v' , vs') =
cong₂ _,_ (valUniq v v') (valTUniq vs vs')
detT : ∀{m n}{ts ts' ts'' : Tel m n}
→ (p : ts —→T ts')(q : ts —→T ts'') → ts' ≡ ts''
det : ∀{n}{t t' t'' : n ⊢}(p : t —→ t')(q : t —→ t'') → t' ≡ t''
det (ξ-·₁ p) (ξ-·₁ q) = cong (_· _) (det p q)
det (ξ-·₁ p) (ξ-·₂ v q) = ⊥-elim (val-red (V-F v) (_ , p))
det (ξ-·₁ p) (E-·₂ v) = ⊥-elim (val-red (V-F v) (_ , p))
det (ξ-·₂ v p) (ξ-·₁ q) = ⊥-elim (val-red (V-F v) (_ , q))
det (ξ-·₂ v p) (ξ-·₂ w q) = cong (_ ·_) (det p q)
det (ξ-·₂ v p) (β-ƛ w) = ⊥-elim (val-red w (_ , p))
det (ξ-·₂ v p) (sat-builtin w q) = ⊥-elim (val-red w (_ , p))
det (ξ-·₂ () p) E-con
det (β-ƛ v) (ξ-·₂ w q) = ⊥-elim (val-red v (_ , q))
det (β-ƛ v) (β-ƛ w) = refl
det (β-ƛ (V-F ())) (E-·₂ v)
det (E-·₂ v) (β-ƛ (V-F ()))
det (ξ-builtin b p) (ξ-builtin .b q) = cong (builtin b ≤‴-refl) (detT p q)
det (ξ-builtin b p) (β-builtin ts vs) = ⊥-elim (valT-redT vs (_ , p))
det (ξ-builtin b p) (E-builtin .b e q) = ⊥-elim (errT-redT q (_ , p))
det (β-builtin ts vs) (ξ-builtin b q) = ⊥-elim (valT-redT vs (_ , q))
det (β-builtin ts vs) (β-builtin .ts ws) = cong (BUILTIN _ ts) (valTUniq vs ws)
det (β-builtin ts vs) (E-builtin b v q) = ⊥-elim (valT-errT vs q)
det (sat-builtin v p) (ξ-·₂ w q) = ⊥-elim (val-red v (_ , q))
det (sat-builtin v p) (sat-builtin w .p) = refl
det (sat-builtin (V-F ()) p) (E-·₂ w)
det E-·₁ E-·₁ = refl
det (E-·₂ v) (ξ-·₁ q) = ⊥-elim (val-red (V-F v) (_ , q))
det (E-·₂ v) (sat-builtin (V-F ()) p)
det (E-·₂ v) (E-·₂ w) = refl
det (E-·₂ ()) E-con
det (E-builtin b ts p) (ξ-builtin .b q) = ⊥-elim (errT-redT p (_ , q))
det (E-builtin b ts p) (β-builtin ts vs) = ⊥-elim (valT-errT vs p)
det (E-builtin b ts p) (E-builtin .b w q) = refl
det E-con (ξ-·₂ () q)
det E-con (E-·₂ ())
det E-con E-con = refl
detT (here p) (here q) = cong (_∷ _) (det p q)
detT (here p) (there v q) = ⊥-elim (val-red v (_ , p))
detT (there v p) (here q) = ⊥-elim (val-red v (_ , q))
detT (there v p) (there w q) = cong (_ ∷_) (detT p q)
vTel:< : ∀{l n}
→ (ts : Tel l n)
→ VTel l n ts → (t : n ⊢)
→ Value t
→ VTel (suc l) n (ts :< t)
vTel:< [] vs t v = v , tt
vTel:< (t' ∷ ts) (v' , vs) t v = v' , (vTel:< ts vs t v)
vTel++ : ∀{l l' n}
→ (ts : Tel l n)
→ VTel l n ts
→ (ts' : Tel l' n)
→ VTel l' n ts'
→ VTel (l Data.Nat.+ l') n (ts ++ ts')
vTel++ [] vs ts' vs' = vs'
vTel++ (t ∷ ts) (v' , vs) ts' vs' = v' , vTel++ ts vs ts' vs'
anyErr++ : ∀{l l' n}{ts : Tel l n} → Any Error ts → (ts' : Tel l' n) → VTel l' n ts' → Any Error (ts' ++ ts)
anyErr++ p [] _ = p
anyErr++ p (t' ∷ ts') (v' , vs') = there v' (anyErr++ p ts' vs')
—→T++ : ∀{l l' n}{ts' ts'' : Tel l n} → ts' —→T ts'' → (ts : Tel l' n) → VTel l' n ts → (ts ++ ts') —→T (ts ++ ts'')
—→T++ p [] vs = p
—→T++ p (t ∷ ts) (v , vs) = there v (—→T++ p ts vs)
\end{code}