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

{-
 - Instant Insanity using Closed Type Families.
 -
 - See:  http://stackoverflow.com/questions/26538595
 -}

{-# OPTIONS_GHC -ftype-function-depth=400 #-}

{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE TypeFamilies #-}

gergoerdi

{-
 - Instant Insanity using Closed Type Families and DataKinds.
 -
 - See:  http://stackoverflow.com/questions/26538595
 -}

{-# OPTIONS_GHC -ftype-function-depth=400 #-}

{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE TypeFamilies #-}

gergoerdi

{-
 - 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 #-}

gergoerdi

{-# 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

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

-- 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

gergoerdi

-- 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

gergoerdi

-- 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;

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