PLT-8253: Literate Agda

src/Marlowe/Language/Contract.agda → src/Marlowe/Language/Contract.lagda.md

@@ -1,3 +1,9 @@
+---
+title: Marlowe.Language.Contract
+layout: page
+---
+
+```
 module Marlowe.Language.Contract where
 
 open import Agda.Builtin.Int using (Int)
@@ -11,7 +17,13 @@ open import Data.String as String using (String)
 open import Relation.Binary using (DecidableEquality)
 open import Relation.Binary.PropositionalEquality using (cong; cong₂; _≡_; _≢_)
 open import Relation.Nullary using (yes; no)
+```
+
+## Domain
+
+TODO: abstract the domain in the Agda module system
 
+```
 data ByteString : Set where
   mkByteString : String → ByteString
 
@@ -113,7 +125,15 @@ _≟-AccountId×Token_ = let _eq_ = ≡-dec _≟-AccountId_ _≟-Token_ in λ x
 
 _≟-Party×Token_ : DecidableEquality (Party × Token)
 _≟-Party×Token_ = let _eq_ = ≡-dec _≟-Party_ _≟-Token_ in λ x y → x eq y
+```
+
+## Values and observations 
+
+Values and observations are language terms that interact with most of the
+other constructs. Value evaluates to an integer and observation evaluates to
+a boolean respectively. They are defined in a mutually recursive way as follows:
 
+```
 data Observation : Set
 
 data Value : Set where
@@ -142,23 +162,30 @@ data Observation where
   ValueEQ : Value → Value → Observation
   TrueObs : Observation
   FalseObs : Observation
+```
 
-
+```
 data Bound : Set where
   mkBound : Int → Int → Bound
 
-
 data Action : Set where
   Deposit : AccountId → Party → Token → Value → Action
   Choice : ChoiceId → List Bound → Action
   Notify : Observation → Action
 
-
 data Payee : Set where
   mkAccount : AccountId → Payee
   mkParty : Party → Payee
+```
 
+## Contract
 
+Marlowe is a continuation-based language, this means that a Contract can
+either be a Close or another construct that recursively has a Contract.
+Eventually, all contracts end up with a Close construct. Case and Contract
+are defined in a mutually recursive way as follows:
+
+```
 data Contract : Set
 
 data Case : Set where
@@ -172,10 +199,11 @@ data Contract where
   Let : ValueId → Value → Contract → Contract
   Assert : Observation → Contract → Contract
 
-
 getAction : Case → Action
 getAction (mkCase action _) = action
+```
 
+```
 maxTimeout : Contract → ℕ
 maxTimeout Close = 0
 maxTimeout (Pay _ _ _ _ c) = maxTimeout c
@@ -184,3 +212,4 @@ maxTimeout (When [] (mkTimeout (mkPosixTime t)) c) = t ⊔ maxTimeout c
 maxTimeout (When ((mkCase _ x) ∷ xs) t c) = maxTimeout x ⊔ maxTimeout (When xs t c)
 maxTimeout (Let x x₁ c) = maxTimeout c
 maxTimeout (Assert x c) = maxTimeout c
+```

src/Marlowe/Language/Input.agda → src/Marlowe/Language/Input.lagda.md

@@ -1,7 +1,11 @@
+---
+title: Marlowe.Language.Input
+layout: page
+---
 
+```
 module Marlowe.Language.Input where
 
-
 open import Agda.Builtin.Int using (Int)
 open import Agda.Builtin.List using (List)
 open import Data.Bool using (Bool; _∧_)
@@ -11,31 +15,27 @@ open import Data.List using (any)
 open import Marlowe.Language.Contract using (AccountId; Bound; ChoiceId; Party; Token)
 open import Relation.Nullary.Decidable using (⌊_⌋)
 
-
 data ChosenNum : Set where
   mkChosenNum : Int → ChosenNum
 
 unChosenNum : ChosenNum → Int
 unChosenNum (mkChosenNum num) = num
 
-
 _inBounds_ : ChosenNum → List Bound → Bool
 _inBounds_ (mkChosenNum num) bounds =
   any inBound bounds
     where
       inBound : Bound → Bool
       inBound (Bound.mkBound l u) = ⌊ l ≤? num ⌋ ∧ ⌊ num ≤? u ⌋
 
-
 data InputContent : Set where
   IDeposit : AccountId → Party → Token → ℕ → InputContent
   IChoice : ChoiceId → ChosenNum → InputContent
   INotify : InputContent
 
-
 data Input : Set where
   NormalInput : InputContent → Input
 
-
 getInputContent : Input → InputContent
-getInputContent (Input.NormalInput input) = input
+getInputContent (NormalInput input) = input where open Input
+```

src/Marlowe/Language/State.agda → src/Marlowe/Language/State.lagda.md

@@ -1,3 +1,9 @@
+---
+title: Marlowe.Language.State
+layout: page
+---
+
+```
 module Marlowe.Language.State where
 
 open import Agda.Builtin.Int using (Int)
@@ -68,3 +74,4 @@ _↑-update_ : (p : (AccountId × Token) × ℕ) (abs : AssocList (AccountId ×
 (a , b) ↑-update abs with a ∈? abs
 ... | yes p = p ∷= (a , proj₂ (lookup p) + b)
 ... | no _ = (a , b) ∷ abs
+```

src/Marlowe/Language/Transaction.agda → src/Marlowe/Language/Transaction.lagda.md

@@ -1,3 +1,9 @@
+---
+title: Marlowe.Language.Transaction
+layout: page
+---
+
+```
 module Marlowe.Language.Transaction where
 
 open import Agda.Builtin.Int using (Int)
@@ -41,13 +47,24 @@ data TransactionError : Set where
   TEIntervalError : IntervalError → TransactionError
   TEUselessTransaction : TransactionError
   TEHashMismatch : TransactionError
+```
+
+## TransactionInput
 
+We use transactions to move contracts forward. Transactions are comprised
+of a list of inputs (possibly empty) to be applied within a TimeInterval
+
+```
 record TransactionInput : Set where
   constructor mkTransactionInput
   field
     timeInterval : TimeInterval
     inputs : List Input
+```
+
+## TransactionOutput
 
+```
 data TransactionOutput : Set where
   mkTransactionOutput : List TransactionWarning → List Payment → State → Contract → TransactionOutput
   mkError : TransactionError → TransactionOutput
@@ -60,3 +77,4 @@ projₚ t (a [ t′ , n ]↦ _) = 1ₜ t (t′ , n)
 
 filter-payments : Token → List Payment → List Payment
 filter-payments t = filter (λ {(_ [ t′ , _ ]↦ _) → (t ≟-Token t′)})
+```