wenkokke

#!/bin/bash
if [[ -z "$1" ]]; then

    echo "usage: witch [package name]"

else

    # iterate over all installed packages
    for pkg in $( brew list ); do

wenkokke

--- ./provers.src/Makefile	2013-11-24 18:48:09.000000000 +0100
+++ ./provers.src/Makefile 	2013-11-24 18:49:38.000000000 +0100
@@ -63,25 +63,25 @@
 	$(MAKE) prover9
 
 prover9: prover9.o $(OBJECTS)
-	$(CC) $(CFLAGS) -lm -o prover9 prover9.o $(OBJECTS) ../ladr/libladr.a
+	$(CC) $(CFLAGS) -o prover9 prover9.o $(OBJECTS) ../ladr/libladr.a -lm
 
 fof-prover9: fof-prover9.o $(OBJECTS)

wenkokke

diff -bur ./ladr/parse.c ./ladr/parse.c
--- ./ladr/parse.c	2009-03-17 18:04:29.000000000 +0100
+++ ./ladr/parse.c	2014-08-21 03:46:12.000000000 +0200
@@ -554,7 +554,7 @@
 
     c = getc(fp);
 
-    if (c == EOF)
+    if (c == EOF || c == (unsigned char)EOF)
       eof = TRUE;

wenkokke

{-# LANGUAGE GADTs #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE UndecidableInstances #-}

wenkokke

{-# LANGUAGE DeriveDataTypeable #-}

import           Control.Applicative ((<$>))
import           Control.Monad (filterM)
import           Data.Foldable (or)
import           Data.List (isSuffixOf,maximumBy)
import           Data.Ord (comparing)
import           Data.Traversable (traverse)
import           Development.Shake
import           Development.Shake.FilePath

wenkokke

DROPBOX_SIZE_LIMIT=3000
DROPBOX_FOLDER="$HOME/Dropbox"
DROPBOX_SHARED_INDEX="$DROPBOX_FOLDER/Shared/.index"

function share {

    current=`du -s $DROPBOX_FOLDER | cut -f1`

    # with no arguments, echo current usage
    if [ "$#" -eq 0 ]; then

wenkokke

> {-# LANGUAGE OverloadedStrings, RecordWildCards, TupleSections, DeriveFunctor #-}
> module Unlit where



> import           Control.Arrow (first,second)
> import           Data.List (foldl')
> import           Data.Text (Text)
> import qualified Data.Text    as T
> import qualified Data.Text.IO as T

wenkokke

module agda2_compute_toplevel where

import Control.Concurrent (forkIO)
import Data.List (isPrefixOf)
import System.Environment (getEnv)
import System.FilePath (splitSearchPath)
import System.IO
import System.Process
import Text.Printf (printf)

wenkokke

{-# LANGUAGE TypeFamilies, TypeOperators #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE FlexibleInstances, FlexibleContexts #-}
{-# LANGUAGE RankNTypes, ExistentialQuantification #-}
{-# LANGUAGE UndecidableInstances, NoMonomorphismRestriction #-}
{-# LANGUAGE FunctionalDependencies #-}

import Prelude hiding (and)

wenkokke

# Encoding CCGs in Agda.

Bla bla bla.

First attempt using type system to check validity of sentences. But sentences may be ambiguous, and
type raising cannot be properly handled due to the implementation of Agda implicits.

Since this blog post is literate Agda, we'll have some administrive business to get out of the way.

\begin{code}