oisdk

struct Down<Element: Comparable> {
  let runDown: Element
  init(_ x: Element) { runDown = x }
}

extension Down: Equatable {}

func ==<A>(lhs: Down<A>, rhs: Down<A>) -> Bool {
  return lhs.runDown == rhs.runDown
}

oisdk

import Control.Lens
import Data.Monoid

succeedOnRewrite :: Plated a => (a -> Maybe a) -> a -> Maybe a
succeedOnRewrite f x 
  = case transformM (maybe (pure x) ((,) (Any True)) . f) x of
    (Any True, y) -> Just y
    _ -> Nothing

oisdk

module Main where

import Prelude
import Control.Monad.Eff
import Control.Monad.Eff.Console (logShow)
import Data.Lazy
import Data.Maybe
import Partial.Unsafe (unsafeCrashWith)
import TryPureScript

oisdk

dyna :: ((f, Seq a) -> a) -> (c -> (f, Maybe c)) -> c -> a
dyna a c = flip index 0 . h
  where h = uncurry (<|) . (a &&& snd) . fmap (maybe mempty h) . c

ses :: Eq a => [a] -> [a] -> [These a a]
ses as bs = dyna (selectBest . edges (length as)) (editGraph as) (as, bs)

-- | A vertex in the edit graph.
data Vertex a = Vertex { xs :: [a], ys :: [a] }
  deriving (Eq, Functor, Show)

oisdk

data Vect : List UniqueType -> UniqueType where
  Nil : Vect []
  (::) : {a : UniqueType} -> a -> Vect as -> Vect (a::as)

data U : UniqueType where MkU : U

u : U
u = MkU

v : Vect [U,U]

oisdk

{-# LANGUAGE ConstraintKinds      #-}
{-# LANGUAGE DataKinds            #-}
{-# LANGUAGE BangPatterns         #-}
{-# LANGUAGE GADTs                #-}
{-# LANGUAGE LambdaCase           #-}
{-# LANGUAGE RebindableSyntax     #-}
{-# LANGUAGE TypeFamilies         #-}
{-# LANGUAGE TypeOperators        #-}
{-# LANGUAGE UndecidableInstances #-}

oisdk

{-# LANGUAGE DataKinds, TypeOperators, GADTs, KindSignatures, FlexibleInstances, FlexibleContexts, DeriveFunctor, DeriveFoldable, ScopedTypeVariables, RankNTypes #-}

import GHC.TypeLits
import Control.Applicative
import Prelude hiding (unzip)
import Data.Monoid

class Semiring a where
  (<+>) :: a -> a -> a
  (<.>) :: a -> a -> a

oisdk

%default total

interface Eq a => VerifiedEq a where
  equalNotEqual : (x, y : a)    -> x == y = not (x /= y)
  reflexive     : (x : a)       -> x == x = True
  symmetric     : (x, y : a)    -> x == y = y == x
  transitive    : (x, y, z : a) 
               -> (fst : x == y = True)
               -> (snd : y == z = True)
               -> x == z = True

oisdk

import Control.Monad.Identity

%default total

data Binary = Z | O Binary | I Binary

Traversal : Type -> Type -> Type
Traversal s a  = { f : Type -> Type } -> Applicative f => (a -> f a) -> (s -> f s)

data Product : (Type -> Type) -> (Type -> Type) -> Type -> Type where

oisdk

{-# LANGUAGE ConstraintKinds       #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE RankNTypes            #-}
{-# LANGUAGE ScopedTypeVariables   #-}
{-# LANGUAGE TypeFamilies          #-}
{-# LANGUAGE TypeOperators         #-}
{-# LANGUAGE UnicodeSyntax         #-}
{-# LANGUAGE FlexibleContexts      #-}

module Lib where