gshen42

----------------------------------------------------------------------
-- First, let's define the original `Expr`

data Fix f = Fix (f (Fix f))

fold :: Functor f => (f a -> a) -> Fix f -> a
fold alg (Fix x) = alg $ fmap (fold alg) x

-- Sum of two functors
data (f :+: g) x = Inl (f x) | Inr (g x) deriving (Functor)

gshen42

open import Data.Nat using (ℕ; zero; suc; _+_; _*_; _≤_; z≤n; s≤s; _<_)
open import Data.Nat.Properties using (*-distribˡ-+; *-comm; +-assoc; +-comm)
open import Data.Nat.DivMod using (_/_; m*n/n≡m; +-distrib-/; _%_; %-distribˡ-+; m*n%n≡0)
open import Relation.Binary.PropositionalEquality as Eq using (_≡_; refl; _≢_; cong; sym; subst)
open Eq.≡-Reasoning using (begin_; _≡⟨⟩_; step-≡;  _∎)

module Sum where

sum : ℕ → ℕ
sum 0       = 0

gshen42

module ParserCombinator where

import Data.Char
import Control.Applicative

newtype Parser a = Parser { runParser :: String -> [(a, String)] }

instance Monad Parser where
  -- _>>=_ :: Parser a -> (a -> Parser b) -> Parser b
  p >>= f = Parser $ \s -> do

gshen42

open import Data.Nat using (ℕ)

-- the whole module is parameterized over the number of processes n
module cbcast (n : ℕ) where

open import Data.Bool using (Bool; true; false; _∧_)
open import Data.Nat using (_+_; _≤_; _<_; _≟_; _≤?_)
open import Data.Nat.Properties using (≤-trans; 1+n≰n; +-comm)
open import Data.Fin as Fin using (Fin)
open import Data.Vec using (Vec; []; _∷_; lookup; allFin; map; foldr)

gshen42

unlist2 :: [a] -> [b] 
        -> (a -> [a] -> b -> [b] -> c -> c)
        -> (a -> [a] -> c)
        -> (b -> [b] -> c)
        -> c
        -> c
unlist2 l1 l2 hcc hcn hnc hnn= case (l1, l2) of
    (x:xs, y:ys) -> hcc x xs y ys (unlist2 xs ys hcc hcn hnc hnn)
    (x:xs, [])   -> hcn x xs  
    ([], y:ys)   -> hnc y ys

gshen42

Require Import Coq.Init.Nat.
Require Import Coq.Arith.PeanoNat.

(*
   A vector clock [vclock] is a total map from index to clock and is represented
   as a function from natural numbers to natural numbers. For index not in the
   map, the defualt clock is 0.
 *)
Definition vclock : Type := nat -> nat.