gistfile1.txt

open import Preliminaries

module lecture.Lecture3Start where

  open Vector using (Vec ; [] ; _::_)
  open Nat using (_+_)
  open List using (_++_ ; [_] ; ++-assoc)

  String = List Char

  lit : Char → String
  lit c = c :: []

  -- We're making up our own little DSL for data description.  First,
  -- we'll define "data formats":

  data Format : Set where
    bit : Format
    char : Format
    nat : Format
    vec : (F : Format) (n : Nat) → Format
    _then_ : (F1 : Format) (F2 : Data F1 → Format) → Format
    done : Format
    error : Format

  Data : Format → Set
  Data bit = Bool
  Data char = Char
  Data nat  = Nat
  Data (vec F n) = Vec (Data F) n
  Data done = Unit
  Data error = Void
  Data (F1 then F2) = Σ \(d : Data F1) → Data (F2 d)

    
  write : (F : Format) → Data F → String
  write f df = {!!}

  read : (F : Format) → String → Maybe (Data F × String)
  read f s = {!!}
  
  -- We want read and write to make a round trip that amounts to
  -- identity.
  readwrite : (F : Format) (d : Data F) → read F (write F d) == Some(d , [])
  readwrite x = {!!}

  module Example where

  -- An example: a format of numbers followed by 2x2 vectors
  -- f : Format
  -- f = nat then vec (vec bit 2) 2)