gergoerdi

{-# LANGUAGE PatternSynonyms #-}
{-# LANGUAGE ViewPatterns #-}
{-# LANGUAGE TypeSynonymInstances, FlexibleInstances #-}
{-# LANGUAGE DeriveFunctor #-}

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

data HuttonF a = IntF Int | AddF a a deriving Functor
type Hutton = Fix HuttonF

gergoerdi

-- http://twistedoakstudios.com/blog/Post4706_breaking-a-toy-hash-function

import Data.List (findIndex)
import Control.Monad (guard)
import Data.Maybe (fromMaybe)
import Data.SBV.Bridge.Boolector
import Control.Monad.State
import Control.Applicative

codebook :: [Char]

gergoerdi

import Control.Applicative.Free
import Control.Applicative

import Control.Monad.Identity
import Data.Monoid

count :: (Functor eff) => Free eff a -> Int
count = getSum . runIdentity . analyze (const $ Identity $ Sum 1)

test :: (Functor eff) => Free eff a -> (Int, Int)

gergoerdi

{-# LANGUAGE DataKinds, KindSignatures #-}
{-# LANGUAGE GADTs, StandaloneDeriving #-}
import Prelude hiding (mapM)
import Data.Traversable (mapM)

import Control.Monad.Tardis
import Control.Monad.Free
import Data.Stream (Stream(..))
import qualified Data.Stream as Stream
import Data.Set (Set)

gergoerdi

{-# LANGUAGE GADTs #-}
{-# LANGUAGE DataKinds #-}
data Nat = Z | Suc Nat

data Fin n where
    FZ :: Fin (Suc n)
    FS :: Fin n -> Fin (Suc n)

inj :: Fin n -> Fin (Suc n)
inj FZ = FZ

gergoerdi

module Lambda where

open import Data.Nat
open import Data.Fin

data Exp : ℕ → Set where
  Var : {n : ℕ} → Fin n → Exp n
  Lam : {n : ℕ} → Exp (suc n) → Exp n
  _·_ : {n m : ℕ} → Exp n → Exp m → Exp (n ⊓ m)

gergoerdi

module MIU where

data Symbol : Set where
  I : Symbol
  U : Symbol

open import Data.List

Word : Set
Word = List Symbol

gergoerdi

; program 9digits
; Register layout:
;
;	n1-n9		the digits
;
;	div			the divisor to check
;	ndiv		n[div]
;	k
;	nk			n[k]
;

gergoerdi

  1. clr z
  2. jz a 7
  3. dec a
  4. inc z
  5. inc b
  6. jmp 2
  7. jz z 11
  8. dec z
  9. inc a
 10. jmp 7