oisdk

module Fold where

open import Level using (_⊔_)
open import Data.Nat as ℕ using (ℕ; suc; zero; _+_)
open import Data.List hiding (sum)
open import Relation.Binary.PropositionalEquality

record Fold {a b} (A : Set a) (B : Set b) : Set (a ⊔ b) where
  field
    ⟦_⟧[]  : B

oisdk

open import Data.Empty
open import Relation.Nullary

infix 0 ⌊_⌋
⌊_⌋ : ∀ {a} → Set a → Set a
⌊ A ⌋ = ¬ ¬ A

pure : ∀ {a} {A : Set a} → A → ⌊ A ⌋
pure x = λ z → z x

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