PLT-8253: Literate Agda

marlowe-agda.cabal

@@ -299,19 +299,19 @@ library
     MAlonzo.Code.Relation.Unary
     MAlonzo.Code.Relation.Binary
     MAlonzo.Code.Algebra
-    MAlonzo.Code.Marlowe.Examples.Escrow
+    MAlonzo.Code.Marlowe.Examples.Operate
     MAlonzo.Code.Marlowe.Semantics.Reduce.Properties
     MAlonzo.Code.Marlowe.Semantics.Operate
     MAlonzo.Code.Marlowe.Semantics.Reduce
     MAlonzo.Code.Marlowe.Semantics.Evaluate
+    MAlonzo.Code.Marlowe.Semantics.Evaluate.Properties
     MAlonzo.Code.Marlowe.Semantics.Operate.Properties
     MAlonzo.Code.Marlowe.Language.State.Properties
     MAlonzo.Code.Marlowe.Language.State
     MAlonzo.Code.Marlowe.Language.Transaction
     MAlonzo.Code.Marlowe.Language.Contract
     MAlonzo.Code.Marlowe.Language.Input
     MAlonzo.Code.Contrib.Data.List.AssocList
-    MAlonzo.Code.Contrib.Data.List.Membership
     MAlonzo.Code.Contrib.Data.Nat.Properties
     MAlonzo.Code.Induction
     MAlonzo.RTE
@@ -551,19 +551,19 @@ library
     MAlonzo.Code.Relation.Unary
     MAlonzo.Code.Relation.Binary
     MAlonzo.Code.Algebra
-    MAlonzo.Code.Marlowe.Examples.Escrow
+    MAlonzo.Code.Marlowe.Examples.Operate
     MAlonzo.Code.Marlowe.Semantics.Reduce.Properties
     MAlonzo.Code.Marlowe.Semantics.Operate
     MAlonzo.Code.Marlowe.Semantics.Reduce
     MAlonzo.Code.Marlowe.Semantics.Evaluate
+    MAlonzo.Code.Marlowe.Semantics.Evaluate.Properties
     MAlonzo.Code.Marlowe.Semantics.Operate.Properties
     MAlonzo.Code.Marlowe.Language.State.Properties
     MAlonzo.Code.Marlowe.Language.State
     MAlonzo.Code.Marlowe.Language.Transaction
     MAlonzo.Code.Marlowe.Language.Contract
     MAlonzo.Code.Marlowe.Language.Input
     MAlonzo.Code.Contrib.Data.List.AssocList
-    MAlonzo.Code.Contrib.Data.List.Membership
     MAlonzo.Code.Contrib.Data.Nat.Properties
     MAlonzo.Code.Induction
     MAlonzo.RTE

src/Marlowe/Examples/Escrow.lagda.md

@@ -21,10 +21,10 @@ open import Relation.Binary using (DecidableEquality)
 open import Relation.Binary.PropositionalEquality using (cong; cong₂)
 open import Relation.Nullary using (yes; no)
 
-open import Marlowe.Language.Contract as C
-open import Marlowe.Language.Input as I
-open import Marlowe.Language.State as S
-open import Marlowe.Language.Transaction as T
+open import Marlowe.Language.Contract as Contract
+open import Marlowe.Language.Input as Input
+open import Marlowe.Language.State as State
+open import Marlowe.Language.Transaction as Transaction
 ```
 
 ```
@@ -74,10 +74,10 @@ mkToken c₁ n₁ ≟-Token mkToken c₂ n₂ with c₁ ≟ c₂ | n₁ ≟ n₂
 ```
 
 ```
-open C.Parameterized _≟-Party_ _≟-Token_
-open S.Parameterized _≟-Party_ _≟-Token_
-open T.Parameterized _≟-Party_ _≟-Token_
-open I.Parameterized _≟-Party_ _≟-Token_
+open Contract.Parameterized _≟-Party_ _≟-Token_
+open State.Parameterized _≟-Party_ _≟-Token_
+open Transaction.Parameterized _≟-Party_ _≟-Token_
+open Input.Parameterized _≟-Party_ _≟-Token_
 ```
 
 ## Escrow

src/Marlowe/Examples/Operate.lagda.md

@@ -21,21 +21,21 @@ open import Relation.Binary using (Decidable; DecidableEquality)
 import Relation.Binary.PropositionalEquality as Eq
 open Eq using (_≡_; refl)
 
-open import Marlowe.Language.Contract as C
-open import Marlowe.Language.Input as I
-open import Marlowe.Language.State as S
-open import Marlowe.Language.Transaction as T
+open import Marlowe.Language.Contract as Contract
+open import Marlowe.Language.Input as Input
+open import Marlowe.Language.State as State
+open import Marlowe.Language.Transaction as Transaction
 ```
 
 ### Token and Party
 
 `Token` and `Party` here are simply strings.
 
 ```
-open C.Parameterized _≟_ _≟_
-open I.Parameterized _≟_ _≟_
-open S.Parameterized _≟_ _≟_
-open T.Parameterized _≟_ _≟_
+open Contract.Parameterized _≟_ _≟_
+open Input.Parameterized _≟_ _≟_
+open State.Parameterized _≟_ _≟_
+open Transaction.Parameterized _≟_ _≟_
 
 open import Marlowe.Semantics.Reduce _≟_ _≟_
 open import Marlowe.Semantics.Operate _≟_ _≟_

src/Marlowe/Language/State/Properties.lagda.md

@@ -40,8 +40,6 @@ open PosixTime using (getPosixTime)
 open C.Parameterized _≟-Party_ _≟-Token_
 open S.Parameterized _≟-Party_ _≟-Token_
 open T.Parameterized _≟-Party_ _≟-Token_
-
-open Decidable _≟-AccountId×Token_ renaming (_↑_ to _↑-AccountId×Token_)
 ```
 
 ```

src/Marlowe/Semantics/Evaluate.lagda.md

@@ -16,8 +16,8 @@ module Marlowe.Semantics.Evaluate
 
 ```
 open import Data.Bool using (Bool; false; true; _∧_; _∨_; if_then_else_; not)
-open import Data.Integer using (ℤ; -_; _-_; +_; _+_; _*_; _≟_; _<?_; _≤?_; ∣_∣; 0ℤ; 1ℤ; NonZero)
-open import Data.Integer.DivMod using (_div_)
+open import Data.Integer as ℤ using (ℤ; -_; _-_; +_; _+_; _*_; _≟_; _<?_; _≤?_; ∣_∣; 0ℤ; 1ℤ; NonZero)
+open import Data.Integer.DivMod as ℤ using ()
 open import Data.Nat as ℕ using ()
 open import Data.Product using (_,_; _×_; proj₁; proj₂)
 open import Data.Product.Properties using (≡-dec)
@@ -61,9 +61,9 @@ open Decidable _≟-ValueId_ renaming (_‼_default_ to _‼ᵛ_default_) using
 ℰ⟦ DivValue x y ⟧ e s = ℰ⟦ x ⟧ e s / ℰ⟦ y ⟧ e s
   where
     _/_ : ℤ → ℤ → ℤ
-    _/_ num den with ∣ den ∣ ℕ.≟ 0
+    _/_ num den with den ℤ.≟ 0ℤ
     ... | yes _ = 0ℤ
-    ... | no ¬p = (num div den) { fromWitnessFalse ¬p }
+    ... | no ¬p = (num ℤ./ den) {{ ℤ.≢-nonZero ¬p }}
 ℰ⟦ ChoiceValue c ⟧ _ s = c ‼ᶜ choices s default 0ℤ
 ℰ⟦ TimeIntervalStart ⟧ e _ = + getPosixTime (startTime (timeInterval e))
 ℰ⟦ TimeIntervalEnd ⟧ e _ = + getPosixTime (endTime (timeInterval e))

src/Marlowe/Semantics/Operate.lagda.md

@@ -231,11 +231,13 @@ there
 
 # Big-step semantics
 
+## Fix interval
+
 ```
 data _↝_ : Configuration → Configuration → Set where
 
   trim-interval : ∀ {c as cs bs tₘ tₛ Δₜ ws ps }
-    → (tₛ + Δₜ) ≥ tₘ
+    → tₛ + Δₜ ≥ tₘ
     → ⟪ c
       , ⟨ as , cs , bs , mkPosixTime tₘ ⟩
       , mkEnvironment (mkInterval (mkPosixTime tₛ) Δₜ)
@@ -266,15 +268,7 @@ fixInterval : ∀ (B : Configuration) → FixInterval B
 fixInterval ⟪ _ , ⟨ _ , _ , _ , mkPosixTime tₘ ⟩ , mkEnvironment (mkInterval (mkPosixTime tₛ) Δₜ) , _ , _ ⟫ with tₛ + Δₜ <? tₘ
 ... | yes p = error p
 ... | no p = trim (trim-interval (≮⇒≥ p))
-
-record Result : Set where
-  constructor ⟦_,_,_⟧
-  field
-    warnings : List TransactionWarning
-    payments : List Payment
-    state : State
 ```
-
 ### Warnings
 
 ```
@@ -290,6 +284,15 @@ convertReduceWarnings = map convertReduceWarning
 
 ## Big-step reduction rules
 
+```
+record Result : Set where
+  constructor ⟦_,_,_⟧
+  field
+    warnings : List TransactionWarning
+    payments : List Payment
+    state : State
+```
+
 ```
 data _⇓_ : Contract × State → Result → Set where
 
@@ -348,11 +351,17 @@ data _⇓_ : Contract × State → Result → Set where
   → (s : State)
   → List TransactionInput
   → (Σ[ r ∈ Result ] (c , s) ⇓ r) ⊎ TransactionError
+```
+
+Close
 
--- Close
+```
 ⇓-eval Close s@(⟨ [] , _ , _ , _ ⟩) [] = inj₁ (⟦ [] , [] , s ⟧ , done refl)
+```
+
+When
 
--- When
+```
 ⇓-eval
   (When cs (mkTimeout (mkPosixTime t)) c) s@(⟨ _ , _ , _ , mkPosixTime tₘ ⟩) ((mkTransactionInput i@(mkInterval (mkPosixTime tₛ) Δₜ) _) ∷ is)
     with fixInterval ⟪ When cs (mkTimeout (mkPosixTime t)) c , s , mkEnvironment i , [] , [] ⟫
@@ -386,8 +395,11 @@ data _⇓_ : Contract × State → Result → Set where
     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 {ts} {cs} {t} {c} {_} {e = mkEnvironment i} {[]} {[]} tₑ<t B↝C C×i⇒D d×s×is⇓r)
 ... | inj₂ e = inj₂ e
+```
+
+Otherwise
 
--- Otherwise
+```
 ⇓-eval c s []
     with ⇀-eval ⟪ c , s , mkEnvironment (mkInterval (mkPosixTime 0) 0) , [] , [] ⟫
 ... | _ , _ , inj₂ _ = inj₂ TEAmbiguousTimeIntervalError

src/Marlowe/Semantics/Reduce/Properties.lagda.md

@@ -22,6 +22,7 @@ open import Data.List.Relation.Unary.Any using (lookup; _∷=_)
 open import Data.Nat as ℕ
 open import Data.Nat.Properties as ℕ
 open import Data.Product using (_×_; _,_; proj₁; proj₂)
+open import Data.Product.Properties using (≡-dec)
 open import Function.Base using (_∘_; _$_; _|>_)
 open import Relation.Nullary using (Dec; yes; no; ¬_)
 open import Relation.Nullary.Negation using (contradiction)
@@ -41,7 +42,7 @@ open import Marlowe.Semantics.Evaluate _≟-Party_ _≟-Token_
 open import Marlowe.Semantics.Reduce _≟-Party_ _≟-Token_
 
 open import Contrib.Data.List.AssocList
-open Decidable _≟-AccountId×Token_ renaming (_∈?_ to _∈?-AccountId×Token_)
+open Decidable (≡-dec _≟-AccountId_ _≟-Token_) renaming (_∈?_ to _∈?-AccountId×Token_)
 
 open State
 open Configuration