UnkindPartition

module Env
import Data.List

%default total

||| Proof that the list doesn't contain the element
data NotElem : k -> List k -> Type where
  NotElemNil : NotElem k []
  NotElemCons : (k = k' -> Void) -> NotElem k ks -> NotElem k (k' :: ks)

UnkindPartition

module Env
import Data.List

||| Proof that the list doesn't contain the element
data NotElem : k -> List k -> Type where
  NotElemNil : NotElem k []
  NotElemCons : (k = k' -> Void) -> NotElem k ks -> NotElem k (k' :: ks)

-- just to check ourselves...
proveNotElem : NotElem k ks -> Elem k ks -> Void

UnkindPartition

import Data.List

mutual

  data Ty = TyInt | TyFun Ty Ty | TyData DataDesc

  data DataDesc =
    MkDataDesc
      String         -- data type name
      (List ConDesc) -- list of constructors

UnkindPartition

{-# LANGUAGE
      FlexibleInstances,
      FlexibleContexts,
      UndecidableInstances,
      MultiParamTypeClasses,
      GADTs,
      ConstraintKinds,
      ScopedTypeVariables,
      TypeOperators
  #-}

UnkindPartition

-- http://haskell98.blogspot.com/2014/10/blog-post_10.html

import Control.Monad

rotate n (x,y) = (n+1-y, x)
rotations n = take 4 $ iterate (rotate n .) id

solutions n =
  let half    = [ 1 .. n `div` 2 ]
      quarter = liftM2 (,) half half

UnkindPartition

{-# LANGUAGE LambdaCase, DeriveDataTypeable, OverloadedStrings, GeneralizedNewtypeDeriving #-}

{-@ LIQUID "--no-case-expand" @-}
{-@ LIQUID "--trustinternals" @-}

import qualified Data.Map as Map
import qualified Data.Generics as SYB
import Data.String
import Text.PrettyPrint

UnkindPartition

{-# LANGUAGE LambdaCase, DeriveDataTypeable, OverloadedStrings, GeneralizedNewtypeDeriving #-}

import qualified Data.Map as Map
import qualified Data.Generics as SYB
import Data.String
import Text.PrettyPrint

-- Syntax

newtype Var = Var String

UnkindPartition

Hi there

UnkindPartition

	Thu Jul 24 02:16 2014 Time and Allocation Profiling Report  (Final)

	   cabal +RTS -p -RTS build --only asdf

	total time  =        3.32 secs   (3317 ticks @ 1000 us, 1 processor)
	total alloc = 1,910,155,320 bytes  (excludes profiling overheads)

COST CENTRE             MODULE                            %time %alloc

readListPrec            Distribution.Package               33.1   36.9

UnkindPartition

#!/usr/bin/perl

# A script to generate constraints based on the package versions installed
# in a cabal sandbox.
#
# Like cabal freeze / cabal-constraints, but is not limited to a single
# package or build tree.
#
# For this to work, you have either to be in a directory with
# cabal.sandbox.config, or have the environment set up