oisdk

module Scratch where

open import Data.Nat as ℕ using (ℕ; suc; zero)
open import Data.Product
open import Function
open import Relation.Nullary
open import Relation.Nullary.Decidable
open import Data.Empty

module GTE where

oisdk

module Data.Nat.Order.Builtin where

open import Data.Nat as ℕ using (ℕ; suc; zero; Ordering; less; equal; greater)
open import Agda.Builtin.Nat using (_-_; _<_; _==_; _+_)
open import Data.Bool
open import Relation.Binary.PropositionalEquality
open import Relation.Binary.PropositionalEquality.TrustMe

less-hom : ∀ n m → ((n < m) ≡ true) → m ≡ suc (n + (m - n - 1))
less-hom zero zero ()

oisdk

module NatLiteral where

open import Data.Nat as ℕ using (ℕ; suc; zero)
open import Relation.Nullary
open import Relation.Nullary.Decidable
open import Data.Unit

record Literal (A : Set) : Set₁ where
  field
    bounds    : ℕ → Set

oisdk

zipo :: Functor f => (f (Fix f -> a) -> f (Fix f) -> a) -> Fix f -> Fix f -> a
zipo alg = c where c = (\x -> alg x . unfix) . fmap c . unfix

newtype Fix f = Fix (f (Fix f))

unfix :: Fix f -> f (Fix f)
unfix (Fix f) = f

oisdk

import Data.Functor.Foldable

zipo :: (Recursive f, Recursive g)
     => (Base f (g -> c) -> Base g g -> c)
     -> f -> g -> c
zipo alg xs = cata (\x -> alg x . project) xs 


zipoFix :: Functor f => (f (Fix f -> a) -> f (Fix f) -> a) -> Fix f -> Fix f -> a
zipoFix = zipo

oisdk

from itertools import islice, chain


class Chunk:
    def __init__(self, iterator, size):
        self._iterator = chain([next(iterator)], islice(iterator, size-1))

    def __next__(self):
        return next(self._iterator)

oisdk

{-# options_ghc -Wall #-}

{-# LANGUAGE GADTs                 #-}
{-# LANGUAGE ScopedTypeVariables   #-}
{-# LANGUAGE RankNTypes            #-}
{-# LANGUAGE BangPatterns          #-}
{-# LANGUAGE FlexibleInstances     #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE StandaloneDeriving    #-}
{-# LANGUAGE UndecidableInstances  #-}

oisdk

{-# LANGUAGE TypeFamilies        #-}
{-# LANGUAGE TypeInType          #-}
{-# LANGUAGE GADTs               #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeOperators       #-}
{-# LANGUAGE PatternSynonyms     #-}
{-# LANGUAGE ViewPatterns        #-}

{-# OPTIONS_GHC -fno-warn-unticked-promoted-constructors #-}

oisdk

import Data.Fin
import Data.Vect
import Prelude.WellFounded

%default total

data Tree : Nat -> Type -> Type where
  Leaf : Tree Z a
  Node : a -> (n : Nat) -> Tree n a -> Tree m a -> Tree (S (n + m)) a

oisdk

import Data.List
import GHC.Base (build)
import qualified Data.Set as Set
import Control.Monad.State
import Test.QuickCheck

toFact n = unfoldl (uncurry go) (n,1)
  where
    go 0 _ = Nothing
    go n m = case n `quotRem` m of