beala

-- Fun with sbv, a theorem prover to haskell.
-- In this file I:
--  - Implement a bit twiddling reverse function.
--  - Use SMT to prove the twiddling function correct.
--  - Implement and prove correct some simple bit conversion functions.
--  - Use the reverse function and sbv's SAT solver to find bytes that are palindromes.

import Data.SBV

-- Functions for reversing 8 bits.

beala

{-# LANGUAGE DeriveFunctor #-}

import Control.Monad.Free
import Data.List

data FizzBuzz f a = FizzBuzz (Factor f) String a deriving Functor
newtype Factor a = Factor a

-- A fizz buzz action that produces a String if the Integral is a factor.
fizzbuzz :: (Show a, Integral a) => a -> String -> Free (FizzBuzz a) ()

beala

/* Lift a stateful computation State[S,A] to State[(S, Seq[(S,A)]), A]
 * where the (S, Seq[(S,A)]) is a history of the computation's state at
 * each step: (currentState, Seq[(stateBeforeStep, resultOfStep)])
 */
def trace[S,A](iter: State[S,A]): State[(S, Seq[(S,A)]),A] = for {
  preStateAndHistory <- get[(S, Seq[(S,A)])]
  preState = preStateAndHistory._1
  history = preStateAndHistory._2
  (postState, result) = runState(for {
    result <- iter

beala

import Control.Applicative

-- Declare a struct with two readers `a` and `b`.
data Env = E {a :: Int, b :: Int}

-- Applicative (r -> _) lets us, eg, take a function that operates on Ints,
-- and instead have it operate on an Env that contains Ints. Since the new
-- function reads from the environment, we call it the Reader applicative
-- (or monad if >>= is defined).

beala

import Control.Concurrent
import qualified Data.Graph.Inductive.Graph as Gr
import Data.Graph.Inductive.PatriciaTree
import qualified Data.Map.Strict as M
import Control.Monad.Trans.Either
import Control.Monad.Trans (liftIO)
import System.IO

data State = NotStarted | Started | Finished deriving (Show)
type NodeStateMap = M.Map Gr.Node State

beala

λ: newtype Fix f = Nest {unFix :: f (Fix f)}

λ: :t Nest []
Nest [] :: Fix []

λ: :t Nest [Nest []]
Nest [Nest []] :: Fix []

beala

(add-to-list 'load-path "~/src/haskell-mode")
(load "haskell-mode-autoloads.el")

(add-hook 'haskell-mode-hook 'interactive-haskell-mode)

(add-hook 'haskell-mode-hook 'turn-on-haskell-indent)

(custom-set-variables
  '(haskell-process-suggest-remove-import-lines t)
  '(haskell-process-auto-import-loaded-modules t)

beala

### Keybase proof

I hereby claim:

  * I am beala on github.
  * I am beala (https://keybase.io/beala) on keybase.
  * I have a public key whose fingerprint is 0BCE 27F8 FBED 34C0 B936  7625 1D7D CA76 C811 1C0C

To claim this, I am signing this object:

beala

Raspberry Pi using the rpi optimized NaCl found here: https://wiki.projectmeshnet.org/Install_on_Raspberry_Pi

[~/mesh/cjdns][raspberrypi]
pi$ ./cjdroute --bench
1379192988 INFO RandomSeed.c:57 Attempting to seed random number generator
1379192988 INFO RandomSeed.c:72 Trying random seed [RtlGenRandom() (Windows)] Failed
1379192988 INFO RandomSeed.c:72 Trying random seed [sysctl(KERN_ARND) (BSD)] Failed
1379192988 INFO RandomSeed.c:68 Trying random seed [/dev/urandom] Success
1379192988 INFO RandomSeed.c:72 Trying random seed [sysctl(RANDOM_UUID) (Linux)] Failed
1379192988 INFO RandomSeed.c:68 Trying random seed [/proc/sys/kernel/random/uuid (Linux)] Success

beala

def printer x
  def helper
    puts x
  end
  helper
end

printer "test" # NameError: undefined local variable or method `x' for main:Object

def printer x