AndrasKovacs

import Data.Map ((!), fromList, Map)

data Direction  = L | R 
type Symbol     = Char
type State      = Maybe Int
type Rules      = Map (State, Symbol) (Symbol, Direction, State)

turingMachine :: Rules -> Symbol -> [Symbol] -> [Symbol]
turingMachine rules blank tape = let

AndrasKovacs

import qualified Data.Vector as V
import qualified Data.Vector.Unboxed as UV
import qualified Data.ByteString.Char8 as B
 
import Data.Ix
import Text.Printf
import Data.List
import Data.Ord
import System.Environment
 

AndrasKovacs

module NatInduction where

data ℕ : Set where
  zero : ℕ
  suc  : ℕ → ℕ 

ℕ-ind : (prop        : ℕ → Set)
      → (zero_proof  : prop zero)
      → (ind_hyp     : ∀ n → prop n → prop (suc n))
      → (n           : ℕ)

AndrasKovacs

import System.Environment
import Data.Word
import Data.Char
import Control.Arrow
import Data.Function
 
infixr 5 :>
data Mem = {- UNPACK -} !Word8 :> Mem
 
eval :: Mem -> Mem -> String -> IO (Mem, Mem)

AndrasKovacs

{-# LANGUAGE LambdaCase #-}

import qualified Data.Attoparsec.Text as P
import qualified Data.Text as T
import qualified Data.Text.IO as TIO

import Control.Applicative
import Data.Char
import Data.List
import Data.Word 

AndrasKovacs

{-# LANGUAGE LambdaCase #-}

import qualified Data.PQueue.Min as Q
import Control.Arrow
import Data.Function

data Tree 
    = Empty
    | Leaf {weight :: Double} 
    | Node {weight :: Double, _left, _right :: Tree}

AndrasKovacs

{-# LANGUAGE RankNTypes, TypeSynonymInstances, FlexibleInstances #-}

type ChNat a = (a -> a) -> a -> a

generalize :: ChNat Int -> (forall a. ChNat a)
generalize n = foldr (.) id . replicate (fromEnum n)

instance Num (ChNat Int) where
    fromInteger = toEnum . fromIntegral
    a + b  = \f -> a f . b f

AndrasKovacs

import Control.Monad.Cont 
import Data.Function


getLabel   = ContT fix
goto label = lift label
getLoop x  = ContT (\k -> let f x' = ContT (\_ -> k (f, x')) in k (f, x)) 


gotoTest :: IO ()

AndrasKovacs

module NatProps where

open import Relation.Binary.PropositionalEquality
open import Relation.Nullary
open import Data.Sum
open import Function

data ℕ : Set where
  zero : ℕ
  suc  : ℕ → ℕ

AndrasKovacs

import qualified Criterion.Main   as Crit

import qualified Test.Tasty.QuickCheck as QC
import qualified Test.Tasty as Tasty	

import Data.List 
import Data.List.Split
import System.Random