oisdk

*** preview.el.orig	2018-06-11 14:08:50.000000000 -0400
--- preview.el	2018-06-11 15:35:38.000000000 -0400
***************
*** 180,186 ****
  	  (close preview-gs-close))
      (tiff (open preview-gs-open)
  	  (place preview-gs-place)
! 	  (close preview-gs-close)))
    "Define functions for generating images.
  These functions get called in the process of generating inline

oisdk

{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE PolyKinds #-}

import Prelude hiding ((.), id, Functor)
import Data.Constraint
import Data.Kind

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)