Skip to content

Commit

Permalink
More concise
Browse files Browse the repository at this point in the history
  • Loading branch information
@yveshauser @zeme-wana
yveshauser authored and zeme-wana committed Jan 9, 2024
1 parent 25a33e7 commit 68675f0
Show file tree
Hide file tree
Showing 2 changed files with 45 additions and 55 deletions.
74 changes: 40 additions & 34 deletions src/Marlowe/Semantics/Operate.agda
View file
Original file line number Diff line number Diff line change
Expand Up @@ -166,7 +166,7 @@ applicable? {s} {e} INotify (Notify o)
∀ {C : Configuration}
→ (w : Waiting C)
→ (i : Input)
→ (Σ[ D ∈ Configuration ] (((w , i) ⇒ D) × Quiescent D)) ⊎ TransactionError
→ (Σ[ D ∈ Configuration ] ((w , i) ⇒ D)) ⊎ TransactionError
⇒-eval {⟪ When [] (mkTimeout (mkPosixTime tₒ)) c , s , e , ws , ps ⟫} (waiting tₑ<t) (NormalInput ic) = inj₂ TEApplyNoMatchError

⇒-eval (waiting {mkCase a cₐ ∷ cs} {t} {c} {s} {e} {ws} {ps} tₑ<t) (NormalInput ic)
Expand All @@ -175,32 +175,40 @@ applicable? {s} {e} INotify (Notify o)
-- here
⇒-eval (waiting {mkCase _ cₐ ∷ cs} {_} {_} {s} {e} {ws} {ps} tₑ<t) (NormalInput ic) | just (deposit-input {a} {p} {t} {_} {n} ℰ⟦v⟧≡+n)
with ⇀-eval ⟪ cₐ , record s { accounts = ((a , t) , n) ↑-update (accounts s) } , e , ws , ps ⟫
... | D , Reduce-until-quiescent C⇀⋆D q = inj₁ (D , Deposit (here refl) ℰ⟦v⟧≡+n tₑ<t q C⇀⋆D , q)
... | _ , Ambiguous-time-interval _ _ = inj₂ TEAmbiguousTimeIntervalError
... | D , C⇀⋆D , inj₁ q = inj₁ (D , Deposit (here refl) ℰ⟦v⟧≡+n tₑ<t q C⇀⋆D)
... | _ , _ , inj₂ _ = inj₂ TEAmbiguousTimeIntervalError
⇒-eval (waiting {mkCase _ cₐ ∷ cs} {_} {_} {s} {e} {ws} {ps} tₑ<t) (NormalInput ic) | just (choice-input {i} {n} {bs} p)
with ⇀-eval ⟪ cₐ , record s { choices = (i , unChosenNum n) ↑-ChoiceId (choices s) } , e , ws , ps ⟫
... | D , Reduce-until-quiescent C⇀⋆D q = inj₁ (D , Choice (here refl) p tₑ<t q C⇀⋆D , q)
... | _ , Ambiguous-time-interval _ _ = inj₂ TEAmbiguousTimeIntervalError
... | D , C⇀⋆D , inj₁ q = inj₁ (D , Choice (here refl) p tₑ<t q C⇀⋆D)
... | _ , _ , inj₂ q = inj₂ TEAmbiguousTimeIntervalError
⇒-eval (waiting {mkCase _ cₐ ∷ cs} {_} {_} {s} {e} {ws} {ps} tₑ<t) (NormalInput ic) | just (notify-input {o} o≡true)
with ⇀-eval ⟪ cₐ , s , e , ws , ps ⟫
... | D , Reduce-until-quiescent C⇀⋆D q = inj₁ (D , Notify {s = s} {o = o} {e = e} (here refl) o≡true tₑ<t q C⇀⋆D , q)
... | _ , Ambiguous-time-interval _ _ = inj₂ TEAmbiguousTimeIntervalError
... | D , C⇀⋆D , inj₁ q = inj₁ (D , Notify {s = s} {o = o} {e = e} (here refl) o≡true tₑ<t q C⇀⋆D)
... | _ , _ , inj₂ _ = inj₂ TEAmbiguousTimeIntervalError

-- there
⇒-eval (waiting {(_ ∷ cs)} {_} {c} tₑ<t) i@(NormalInput (IDeposit x x₁ x₂ x₃)) | nothing
with ⇒-eval (waiting {cs} {_} {c} tₑ<t) i
... | inj₁ (D , (Deposit x x₁ x₂ x₃ x₄) , q) = inj₁ (D , (Deposit (there x) x₁ x₂ x₃ x₄ , q))
... | inj₁ (D , (Deposit x x₁ x₂ x₃ x₄)) = inj₁ (D , (Deposit (there x) x₁ x₂ x₃ x₄))
... | inj₂ e = inj₂ e
⇒-eval (waiting {(_ ∷ cs)} {_} {c} {s} tₑ<t) i@(NormalInput (IChoice x x₁)) | nothing
with ⇒-eval (waiting {cs} {_} {c} {s} tₑ<t) i
... | inj₁ (D , (Choice x x₁ x₂ x₃ x₄) , q) = inj₁ (D , (Choice (there x) x₁ x₂ x₃ x₄ , q))
... | inj₁ (D , (Choice x x₁ x₂ x₃ x₄)) = inj₁ (D , (Choice (there x) x₁ x₂ x₃ x₄))
... | inj₂ e = inj₂ e
⇒-eval (waiting {(_ ∷ cs)} {_} {c} tₑ<t) i@(NormalInput INotify) | nothing
with ⇒-eval (waiting {cs} {_} {c} tₑ<t) i
... | inj₁ (D , (Notify x x₁ x₂ x₃ x₄) , q) = inj₁ (D , (Notify (there x) x₁ x₂ x₃ x₄ , q))
... | inj₁ (D , (Notify x x₁ x₂ x₃ x₄)) = inj₁ (D , (Notify (there x) x₁ x₂ x₃ x₄))
... | inj₂ e = inj₂ e


fixInterval : TimeInterval → State → IntervalResult
fixInterval i@(mkInterval (mkPosixTime tₛ) Δₜ) s@(⟨ _ , _ , _ , mkPosixTime tₘ ⟩) =
if (tₛ + Δₜ) <ᵇ tₘ
then mkIntervalError (IntervalInPastError (mkPosixTime tₘ) i)
else IntervalTrimmed
(mkEnvironment (mkInterval (mkPosixTime (tₛ ⊔ tₘ)) (Δₜ ∸ (tₘ ∸ tₛ))))
(record s { minTime = mkPosixTime (tₛ ⊔ tₘ) })

record Result : Set where
constructor ⟦_,_,_⟧
field
Expand Down Expand Up @@ -254,20 +262,15 @@ data _⇓_ : Contract × State → Result → Set where
, s
⟧

fixInterval : TimeInterval → State → IntervalResult
fixInterval i@(mkInterval (mkPosixTime tₛ) Δₜ) s@(⟨ _ , _ , _ , mkPosixTime tₘ ⟩) =
if (tₛ + Δₜ) <ᵇ tₘ
then mkIntervalError (IntervalInPastError (mkPosixTime tₘ) i)
else IntervalTrimmed
(mkEnvironment (mkInterval (mkPosixTime (tₛ ⊔ tₘ)) (Δₜ ∸ (tₘ ∸ tₛ))))
(record s { minTime = mkPosixTime (tₛ ⊔ tₘ) })


{-# TERMINATING #-} -- TODO: use sized types instead
⇓-eval :
∀ (c : Contract)
→ (s : State)
→ List TransactionInput
→ (Σ[ r ∈ Result ] (c , s) ⇓ r) ⊎ TransactionError

-- Close
⇓-eval Close s@(⟨ [] , _ , _ , _ ⟩) [] = inj₁ (⟦ [] , [] , s ⟧ , done refl)

Expand All @@ -276,45 +279,48 @@ fixInterval i@(mkInterval (mkPosixTime tₛ) Δₜ) s@(⟨ _ , _ , _ , mkPosixTi
(When cs (mkTimeout (mkPosixTime t)) _) s ((mkTransactionInput i@(mkInterval (mkPosixTime tₛ) Δₜ) _) ∷ is) with (tₛ + Δₜ) <? t
... | no t≤tₑ
with ⇀-eval ⟪ When cs (mkTimeout (mkPosixTime t)) _ , s , mkEnvironment i , [] , [] ⟫
... | _ , Ambiguous-time-interval _ _ = inj₂ TEAmbiguousTimeIntervalError
... | D , Reduce-until-quiescent C×i⇒D ¬q
... | _ , _ , inj₂ _ = inj₂ TEAmbiguousTimeIntervalError
... | D , C×i⇒D , inj₁ q
with ⇓-eval (contract D) (state D) is
... | inj₁ (⟦ ws , ps , s ⟧ , d×s×is⇓r) = inj₁ (⟦ ws ++ convertReduceWarnings (warnings D) , ps ++ payments D , s ⟧ , reduce-until-quiescent refl refl C×i⇒D ¬q d×s×is⇓r)
... | inj₁ (⟦ ws , ps , s ⟧ , d×s×is⇓r) = inj₁ (⟦ ws ++ convertReduceWarnings (warnings D) , ps ++ payments D , s ⟧ , reduce-until-quiescent refl refl C×i⇒D q d×s×is⇓r)
... | inj₂ e = inj₂ e

⇓-eval
(When cs (mkTimeout (mkPosixTime t)) c) s ((mkTransactionInput i@(mkInterval (mkPosixTime tₛ) Δₜ) (ts ∷ tss)) ∷ is)
(When cs (mkTimeout (mkPosixTime t)) c) s ((mkTransactionInput i@(mkInterval (mkPosixTime tₛ) Δₜ) []) ∷ is)
| yes tₑ<t
with ⇒-eval (waiting {cs} {t} {c} {s} {e = mkEnvironment i} {[]} {[]} tₑ<t) ts -- TODO: fixInterval
... | inj₂ _ = inj₂ TEUselessTransaction
... | inj₁ (D , C×i⇒D , _)
with ⇀-eval ⟪ When cs (mkTimeout (mkPosixTime t)) _ , s , mkEnvironment i , [] , [] ⟫
... | _ , _ , inj₂ _ = inj₂ TEAmbiguousTimeIntervalError
... | D , C×i⇒D , inj₁ q
with ⇓-eval (contract D) (state D) is
... | inj₁ (⟦ ws , ps , s ⟧ , d×s×is⇓r) = inj₁ (⟦ ws ++ convertReduceWarnings (warnings D) , ps ++ payments D , s ⟧ , apply-input tₑ<t C×i⇒D d×s×is⇓r)
... | inj₁ (⟦ ws , ps , s ⟧ , d×s×is⇓r) = inj₁ (⟦ ws ++ convertReduceWarnings (warnings D) , ps ++ payments D , s ⟧ , reduce-until-quiescent refl refl C×i⇒D q d×s×is⇓r)
... | inj₂ e = inj₂ e

⇓-eval
(When cs (mkTimeout (mkPosixTime t)) c) s ((mkTransactionInput i@(mkInterval (mkPosixTime tₛ) Δₜ) []) ∷ is)
(When cs (mkTimeout (mkPosixTime t)) c) s ((mkTransactionInput i@(mkInterval (mkPosixTime tₛ) Δₜ) (ts ∷ tss)) ∷ is)
| yes tₑ<t
with ⇀-eval ⟪ When cs (mkTimeout (mkPosixTime t)) _ , s , mkEnvironment i , [] , [] ⟫
... | _ , Ambiguous-time-interval _ _ = inj₂ TEAmbiguousTimeIntervalError
... | D , Reduce-until-quiescent C×i⇒D ¬q
with fixInterval i s
... | mkIntervalError e = inj₂ (TEIntervalError e)
... | IntervalTrimmed e′ s′
with ⇒-eval (waiting {cs} {t} {c} {s} {e = mkEnvironment i} {[]} {[]} tₑ<t) ts -- TODO: fixInterval in apply-input
... | inj₂ _ = inj₂ TEUselessTransaction
... | inj₁ (D , C×i⇒D)
with ⇓-eval (contract D) (state D) is
... | inj₁ (⟦ ws , ps , s ⟧ , d×s×is⇓r) = inj₁ (⟦ ws ++ convertReduceWarnings (warnings D) , ps ++ payments D , s ⟧ , reduce-until-quiescent refl refl C×i⇒D ¬q d×s×is⇓r)
... | inj₁ (⟦ ws , ps , s ⟧ , d×s×is⇓r) = inj₁ (⟦ ws ++ convertReduceWarnings (warnings D) , ps ++ payments D , s ⟧ , apply-input tₑ<t C×i⇒D d×s×is⇓r)
... | inj₂ e = inj₂ e

-- Otherwise
⇓-eval c s []
with ⇀-eval ⟪ c , s , mkEnvironment (mkInterval (mkPosixTime 0) 0) , [] , [] ⟫
... | _ , Ambiguous-time-interval _ _ = inj₂ TEAmbiguousTimeIntervalError
... | D , Reduce-until-quiescent C×i⇒D q
... | _ , _ , inj₂ _ = inj₂ TEAmbiguousTimeIntervalError
... | D , C×i⇒D , inj₁ q
with ⇓-eval (contract D) (state D) []
... | inj₁ (⟦ ws , ps , s ⟧ , d×s×is⇓r) = inj₁ (⟦ ws ++ convertReduceWarnings (warnings D) , ps ++ payments D , s ⟧ , reduce-until-quiescent refl refl C×i⇒D q d×s×is⇓r)
... | inj₂ e = inj₂ e

⇓-eval c s ((mkTransactionInput i _) ∷ is)
with ⇀-eval ⟪ c , s , mkEnvironment i , [] , [] ⟫
... | _ , Ambiguous-time-interval _ _ = inj₂ TEAmbiguousTimeIntervalError
... | D , Reduce-until-quiescent C×i⇒D q
... | _ , _ , inj₂ _ = inj₂ TEAmbiguousTimeIntervalError
... | D , C×i⇒D , inj₁ q
with ⇓-eval (contract D) (state D) is
... | inj₁ (⟦ ws , ps , s ⟧ , d×s×is⇓r) = inj₁ (⟦ ws ++ convertReduceWarnings (warnings D) , ps ++ payments D , s ⟧ , reduce-until-quiescent refl refl C×i⇒D q d×s×is⇓r)
... | inj₂ e = inj₂ e
Expand Down
26 changes: 5 additions & 21 deletions src/Marlowe/Semantics/Reduce.agda
View file
Original file line number Diff line number Diff line change
Expand Up @@ -435,33 +435,17 @@ progress
... | no ¬o≡true = step (AssertFalse (¬-not ¬o≡true))


-- TODO: probably remove
data _⇀ₙ_ : Configuration → Configuration → Set where

Reduce-until-quiescent : ∀ {C D}
→ C ⇀⋆ D
→ Quiescent D
-------------
→ C ⇀ₙ D

Ambiguous-time-interval : ∀ {C D}
→ C ⇀⋆ D
→ AmbiguousTimeInterval D
-------------------------
→ C ⇀ₙ D

-- Evaluator

{-# TERMINATING #-} -- TODO: use sized types instead
⇀-eval :
∀ (C : Configuration)
→ Σ[ D ∈ Configuration ] (C ⇀ₙ D)
→ Σ[ D ∈ Configuration ] ((C ⇀⋆ D) × (Quiescent D ⊎ AmbiguousTimeInterval D))
⇀-eval C with progress C
... | quiescent q = C , Reduce-until-quiescent (C ∎) q
... | ambiguousTimeInterval a = C , Ambiguous-time-interval (C ∎) a
... | quiescent q = C , (C ∎) , inj₁ q
... | ambiguousTimeInterval a = C , (C ∎) , inj₂ a
... | step {D} C⇀D with ⇀-eval D
... | E , Reduce-until-quiescent D⇀⋆E s = E , Reduce-until-quiescent (C ⇀⟨ C⇀D ⟩ D⇀⋆E) s
... | E , Ambiguous-time-interval D⇀⋆E a = E , Ambiguous-time-interval (C ⇀⟨ C⇀D ⟩ D⇀⋆E) a
... | E , D⇀⋆E , q⊎a = E , (C ⇀⟨ C⇀D ⟩ D⇀⋆E) , q⊎a

-- Examples

Expand Down Expand Up @@ -505,4 +489,4 @@ private
, [ accountId₁ [ token₁ , 5 ]↦ mkParty (unAccountId accountId₁) ]
⟫

_ = ⇀-eval config₂ ≡ (config₀ , Reduce-until-quiescent (config₂ ⇀⟨ IfTrue refl ⟩ config₁ ⇀⟨ CloseRefund ⟩ config₀ ∎) close)
_ = ⇀-eval config₂ ≡ (config₀ , (config₂ ⇀⟨ IfTrue refl ⟩ config₁ ⇀⟨ CloseRefund ⟩ config₀ ∎) , inj₁ close)

0 comments on commit 68675f0

Please sign in to comment.