Skip to content

Instantly share code, notes, and snippets.

Avatar

Gergő Érdi gergoerdi

View GitHub Profile
View gist:566307
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
View gist:567428
; program 9digits
; Register layout:
;
; n1-n9 the digits
;
; div the divisor to check
; ndiv n[div]
; k
; nk n[k]
;
@gergoerdi
gergoerdi / MIU.agda
Created Jun 3, 2012
The "MI to MU" puzzle from GEB
View MIU.agda
module MIU where
data Symbol : Set where
I : Symbol
U : Symbol
open import Data.List
Word : Set
Word = List Symbol
@gergoerdi
gergoerdi / gist:3376887
Created Aug 17, 2012
Untyped lambda-calculus
View gist:3376887
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
gergoerdi / gist:3376973
Created Aug 17, 2012
Untyped lambda-calculus (Haskell)
View gist:3376973
{-# 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
gergoerdi / ReadableGeneratedNames.hs
Created Oct 1, 2012
Using Tardis to turn generated names into nicely readable ones
View ReadableGeneratedNames.hs
{-# 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
gergoerdi / gist:5324462
Created Apr 6, 2013
Trying to observe a difference between `pure id <*> x` and `x`
View gist:5324462
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)
View gist:5917097
-- 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]
View Hutton2.hs
{-# 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
View families-closed.hs
{-
- Instant Insanity using Closed Type Families.
-
- See: http://stackoverflow.com/questions/26538595
-}
{-# OPTIONS_GHC -ftype-function-depth=400 #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE TypeFamilies #-}
You can’t perform that action at this time.