Skip to content

Instantly share code, notes, and snippets.

Avatar

Gergő Érdi gergoerdi

View GitHub Profile
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 #-}
View families-closed-datakinds.hs
{-
- Instant Insanity using Closed Type Families and DataKinds.
-
- See: http://stackoverflow.com/questions/26538595
-}
{-# OPTIONS_GHC -ftype-function-depth=400 #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE TypeFamilies #-}
View families-open.hs
{-
- Instant Insanity using Type Families.
-
- See: The Monad Read, Issue #8 - http://www.haskell.org/wikiupload/d/dd/TMR-Issue8.pdf
-}
{-# OPTIONS_GHC -ftype-function-depth=400 #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE TypeFamilies #-}
View STLC.hs
{-# LANGUAGE GADTs, StandaloneDeriving #-}
{-# LANGUAGE DataKinds, KindSignatures, TypeFamilies, TypeOperators #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TemplateHaskell #-}
module STLC where
import Data.Singletons.Prelude
import Data.Singletons.TH
import Data.Type.Equality
@gergoerdi
gergoerdi / irreducible.agda
Last active Aug 29, 2015
Irreducibility vs. primality
View irreducible.agda
open import Relation.Binary.Core
open import Relation.Binary.PropositionalEquality
open import Data.Product
open import Data.Sum
open import Data.Nat
data Irreducible (n : ℕ) : Set where
irreducible : n ≢ 1 ( x y n ≡ x * y x ≡ 1 ⊎ y ≡ 1) Irreducible n
open import Data.Nat.Primality
@gergoerdi
gergoerdi / SymIter.agda
Last active Aug 29, 2015
Defining commutative functions
View SymIter.agda
-- From Conor McBride: https://lists.chalmers.se/pipermail/agda/2015/007768.html
open import Data.Nat using (ℕ; zero; suc)
open import Relation.Binary
open import Relation.Binary.PropositionalEquality
open import Function
symIter : {X : Set} (ℕ X) (X X) X
symIter zen more zero y = zen y
symIter zen more x zero = zen x
symIter zen more (suc x) (suc y) = more $ symIter zen more x y
View SymIterComplete.agda
-- continued from https://gist.github.com/gergoerdi/46ad83513fd9db65c286
module Complete where
open import Data.Product
record SymItery {X Y : Set} : Set where
constructor SymIter
field
zen : X
more : X X
View ToggleSync.vhdl
-- Based on http://www.edn.com/electronics-blogs/day-in-the-life-of-a-chip-designer/4435339/Synchronizer-techniques-for-multi-clock-domain-SoCs
-- via http://electronics.stackexchange.com/questions/182331/
library IEEE;
use IEEE.STD_LOGIC_1164.ALL;
entity ToggleSync is
Port ( CLK_FAST_SOURCE : in STD_LOGIC;
CLK_SLOW_TARGET : in STD_LOGIC;
PULSE_IN : in STD_LOGIC;
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
You can’t perform that action at this time.