jozefg

%{ Proving the Church Rosser theorem for lambda calculus in Twelf }%

%{ First, let's define the untyped lambda calculus }%

term : type.
ap  : term -> term   -> term.
lam : (term -> term) -> term.

%{ Evaluation }%

jozefg

{-# LANGUAGE DeriveFunctor, DeriveFoldable, DeriveTraversable, LambdaCase #-}
module CoC where
import           Bound
import           Control.Applicative
import           Control.Monad
import           Control.Monad.Gen
import           Control.Monad.Trans
import           Data.Foldable       hiding (elem)
import qualified Data.Map            as M
import           Data.Maybe

jozefg

module wat

data Wat : Type where
  foo : (Wat -> Wat) -> Wat

sapply : Wat -> Wat
sapply (foo x) = x (foo x)

u : Wat
u = sapply (foo (\x => sapply x))

jozefg

signature KEY =
sig
    type t
    val compare : t * t -> order
end

signature PQUEUE =
sig
    type t
    type key

jozefg

signature UNION_FIND =
sig
    type t
    eqtype set

    val new   : t -> set
    val union : set -> set -> unit
    val repr  : set -> set
    val same  : set -> set -> bool
end

jozefg

signature TYPEINFER =
sig
    type tvar =  int
    datatype monotype = TBool
                      | TArr of monotype * monotype
                      | TVar of tvar
    datatype polytype = PolyType of int list * monotype
    datatype exp = True
                 | False
                 | Var of int

jozefg

{-# LANGUAGE DeriveFunctor, GeneralizedNewtypeDeriving #-}
{-# LANGUAGE FlexibleContexts, LambdaCase #-}

-- | A humane representation of binding.
module ABT ( FreeVar (..)
           , Operator (..)
           , ABT
           , View (..)
           , view
           , fold

jozefg

module queue
import Data.Vect

-- Here's the port of the Liquid Haskell blog post on amortized
-- queues. The tricksy bit is that the "amortized" bit depends on
-- laziness. This means that while in the REPL (where Idris is lazy)
-- this is reasonably efficient. It compiles absolutely horribly
-- though because each time push or pop something we rotate the whole
-- damned thing.

jozefg

nat : type.
s   : nat -> nat.
z   : nat.

bool  : type.
true  : bool.
false : bool.

plus : nat -> nat -> nat -> type.
%mode plus +N +M -R.

jozefg

{-# LANGUAGE ImpredicativeTypes #-}
{-# LANGUAGE RankNTypes #-}
module Tail where

type CL a = forall c. (a -> c -> c) -> c -> c

t :: CL a  -> (forall c. (a -> (Bool -> c) -> (Bool -> c))
               -> (Bool -> c)
               -> (Bool -> c))
t fold cons nil = fold myCons myNil