YuMingLiao

import Data.Nat

data Parity : Nat -> Type where
  Even : Parity (n + n)
  Odd : Parity (S (n + n))

helpEven : (j : Nat) -> Parity (S j + S j) -> Parity (S (S (plus j j)))
helpEven j p = rewrite plusSuccRightSucc j j in p

helpOdd : (j : Nat) -> Parity (S (S (j + S j))) -> Parity (S (S (S (j + j))))

YuMingLiao

{ pkgs }:
with builtins;
with pkgs;
with lib.attrsets;
with stdenv;
with rec {
  deepReadDir = path:
    let 
      attrset = readDir path;
      go = name: value:

YuMingLiao

with builtins;
with (import <nixpkgs> { });
with (import <nixpkgs> { }).lib.attrsets;
with (import <nixpkgs> { }).stdenv;
with rec {
  deepReadDir = path:
    let 
      attrset = readDir path;
      go = name: value:
        if value == "directory" then

YuMingLiao

data PriorityQueue k a = Nil | Branch k a (PriorityQueue k a) (PriorityQueue k a)

empty :: Ord k => PriorityQueue k a
empty = Nil

singleton :: Ord k => k -> a -> PriorityQueue k a
singleton k a = Branch k a Nil Nil

minKeyValue :: Ord k => PriorityQueue k a -> (k, a)
minKeyValue Nil              = error "empty queue"

YuMingLiao

data Heap a = Empty | Heap a [(Heap a)]
      deriving Show
  
singleton :: Ord a => a -> Heap a
singleton a = Heap a []
  
findMin :: Heap a -> a
findMin (Heap h _) = h
  
minView :: Ord a => Heap a -> Maybe (a, Heap a)

YuMingLiao

data Tree a
  = Leaf a 
  | Node (Tree a) a (Tree a)
  deriving (Eq, Show)

dfLabel :: Tree a -> Tree Int 
dfLabel = fst . go 0 where 
  go n (Leaf _)        = (Leaf n, n+1) 
  go n (Node l _ r)    =  let 
    (l', n')  = go (n+1) l

YuMingLiao

subGraphOfFirstCommonAncestor 
o    7dbfc7
|
o o    132823,193a16
|/
o    1d7bbd
|
o

resultHeads: (fromList [("master",Tran_193a16),("mergebranch_13282313-7fb3-4097-bf3a-e29c81dcfa1d",Tran_7dbfc7)]) 

YuMingLiao

module SharedState where
import Concur.Core
import Concur.Replica
import Control.Monad
import Control.Applicative
import Control.Concurrent.STM
import Control.Concurrent.STM.TVar
import Control.Concurrent.STM.TChan
import Control.Lens
import Control.Monad.IO.Class (liftIO)

YuMingLiao

module SharedState where
import Concur.Core
import Concur.Replica
import Control.Monad
import Control.Applicative
import Control.Concurrent.STM
import Control.Concurrent.STM.TVar
import Control.Concurrent.STM.TChan
import Control.Lens
import Control.Monad.IO.Class (liftIO)

YuMingLiao

{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE AllowAmbiguousTypes #-}