oisdk

{-# OPTIONS --safe --cubical #-}

module Bits where

open import Cubical.Data.Nat as ℕ using (ℕ; suc; zero)
open import Agda.Primitive using (Level)
open import Cubical.Foundations.Function

variable
  a : Level

oisdk

import Numeric.Natural
import Data.Function

-- R a = Fix (ContT a [])
newtype R a = R { r :: (R a -> [a]) -> [a] }

bfUnfold :: (a -> (b,a,a)) -> a -> [b]
bfUnfold f t = g t (fix (R . flip id)) (fix (flip r))
  where
    g b fw bw = x : r fw (bw . R . g ys . R . g zs)

oisdk

isPal :: forall a. Eq a => [a] -> Bool
isPal xs = getAll (fst (go xs xs)) where
  go (y:ys) (_:_:zs) = f y =<< go ys zs
  go (_:ys) [_]      = pure ys
  go ys     []       = pure ys
  
  f y ~(z:zs)        = (All (y == z), zs)
  

oisdk

{-# LANGUAGE DeriveFunctor, LambdaCase, FlexibleContexts, FlexibleInstances, MultiParamTypeClasses, UndecidableInstances, RankNTypes, GeneralizedNewtypeDeriving #-}

import Data.Semigroup hiding (Sum(..))
import Control.Applicative
import Control.Monad
import Data.Functor.Classes
import Control.Monad.State
import qualified Data.Set as Set
import Data.Set (Set)

oisdk

{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications    #-}

import Data.Semigroup
import Control.Arrow
import Data.Align
import Data.Coerce
import Data.Tuple

newtype Stream a = Stream [a]

oisdk

{-# LANGUAGE DeriveFunctor, LambdaCase #-}

import Control.Applicative hiding (many)
import Control.Monad

newtype Parser a = Parser { runParser :: String -> [(a, String)] } deriving Functor

instance Applicative Parser where
    pure x = Parser (\s -> [(x,s)])
    fs <*> xs = fs >>= (\f -> xs >>= (\x -> pure (f x)))

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