gergoerdi

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

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

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

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

import Data.Vect

%default total

permutations : Vect n a -> Vect (fact n) (Vect n a)
permutations [] = [[]]
permutations {n = S n} (x :: xs) = rewrite multCommutative (S n) (fact n) in
                                   concat $ map (inserts x) (permutations xs)
  where
    inserts : a -> Vect k a -> Vect (S k) (Vect (S k) a)

gergoerdi

import Data.Vect
import Data.Fin

%default total

fins : Vect n (Fin n)
fins {n = Z} = []
fins {n = S n} = FZ :: map FS fins

permutations : {n : Nat} -> Vect (fact n) (Vect n a -> Vect n a)

gergoerdi

import Data.Vect
import Data.Fin

%default total

fins : Vect n (Fin n)
fins {n = Z} = []
fins {n = S n} = FZ :: map FS fins

Permutation : Nat -> Type

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

open import Data.Product
open import Function using (_∘_; id)

data Cont : Set₁ where
  _<|_ : (S : Set) → (P : S → Set) → Cont

[_]C : Cont → Set → Set
[ S <| P ]C X = Σ[ s ∈ S ] (P s → X)

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]