<commit_before>import Protocol
import Data.List

%language TypeProviders
%default total


-- A session type that enforces valid interactions with a door.
%provide (DoorSession : (Path -> Type)) with Protocol "door.txt"

riiing : Nat -> DoorSession("closed", "closed")
riiing Z = Noop
riiing (S k) = do
  Action "ring"
  riiing k

-- An implementation of the protocol.
door : Nat -> DoorSession ("locked", "end")
door nTimes = do
--Action  "smash"  -> Won't compile because it's not a legal action described in door.txt.
  Action  "unlock"
--Action  "unlock" -> Won't compile because it's not a legal action *in this state*.
  riiing nTimes
  Action "open"
  Action "enter"

runDoor : DoorSession (a, b) -> List String
runDoor (x >>= rest) = (runDoor x) ++ (runDoor $ rest True)
runDoor (Action x) = [x]
runDoor Noop = []


-- A session type that enforces valid interactions with a vending machine.
%provide (VendingMachineSession : (Path -> Type)) with Protocol "vending-machine.txt"

-- An implementation of the protocol.
vendingMachine : VendingMachineSession ("waiting", "vended")
vendingMachine = do
--Action "hack" -> Won't compile as it's not a legal action described in vending-machine.txt.
  Action "pay"
  Action "return"
--Action "vend" -> Won't compile as it's not a legal action *in this state*.
  Action "pay"
  Action "select"
  Action "vend"
<commit_msg>Define module Example and add section headings<commit_after>module Example

import Data.FSM.Protocol
import Data.List

%language TypeProviders
%default total

%access public export

---------------
-- Door Example
---------------

-- A session type that enforces valid interactions with a door.
%provide (DoorSession : (Path -> Type)) with Protocol "door.txt"

riiing : Nat -> DoorSession("closed", "closed")
riiing Z = Noop
riiing (S k) = do
  Action "ring"
  riiing k

-- An implementation of the protocol.
door : Nat -> DoorSession ("locked", "end")
door nTimes = do
--Action  "smash"  -> Won't compile because it's not a legal action described in door.txt.
  Action  "unlock"
--Action  "unlock" -> Won't compile because it's not a legal action *in this state*.
  riiing nTimes
  Action "open"
  Action "enter"

runDoor : DoorSession (a, b) -> List String
runDoor (x >>= rest) = (runDoor x) ++ (runDoor $ rest True)
runDoor (Action x) = [x]
runDoor Noop = []

--------------------------
-- Vending Machine Example
--------------------------

-- A session type that enforces valid interactions with a vending machine.
%provide (VendingMachineSession : (Path -> Type)) with Protocol "vending-machine.txt"

-- An implementation of the protocol.
vendingMachine : VendingMachineSession ("waiting", "vended")
vendingMachine = do
--Action "hack" -> Won't compile as it's not a legal action described in vending-machine.txt.
  Action "pay"
  Action "return"
--Action "vend" -> Won't compile as it's not a legal action *in this state*.
  Action "pay"
  Action "select"
  Action "vend"

{'fraction_non_alphanumeric': 0.14077340569877883, 'fraction_numerical': 0.0, 'mean_word_length': 3.421289355322339, 'pattern_counts': {'":': 0, '<': 3, '<?xml version=': 0, '>': 25, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 0, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
{'dir': 'git-commits-cleaned', 'id': '6231143', 'n_tokens_mistral': 924, 'n_tokens_neox': 896, 'n_words': 360}