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}

wenkokke

\begin{code}
open import Level using (_⊔_)
open import Data.Vec using (Vec; []; _∷_)
open import Data.Nat as Nat using (ℕ; zero; suc)
open import Data.Sum using (_⊎_; inj₁; inj₂)
open import Data.Product using (∃; _×_; _,_; proj₁; proj₂)
open import Data.Empty using (⊥-elim)
open import Relation.Nullary
open import Relation.Binary
open import Relation.Binary.PropositionalEquality using (_≡_; refl)

wenkokke

open import Level                                      using (_⊔_)
open import Function                                   using (_∘_)
open import Data.Vec                                   using (Vec; []; _∷_; foldr)
open import Data.Nat                                   using (ℕ; zero; suc; _+_)
open import Data.Nat.Properties.Simple                 using (+-right-identity; +-suc)
open import Data.Sum                                   using (_⊎_; inj₁; inj₂)
open import Data.Product                               using (∃; _×_; _,_; proj₁; proj₂)
open import Data.Empty                                 using (⊥-elim)
open import Relation.Nullary                           using (Dec; yes; no; ¬_)
open import Relation.Binary                            using (module DecTotalOrder; DecTotalOrder; Rel)

wenkokke

{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE OverloadedStrings, FlexibleInstances #-}
{-# LANGUAGE GADTs, DataKinds, KindSignatures, TypeFamilies #-}
module Logic where

import Text.Printf (printf)
import Data.String.Utils (join)

-- | encoding of natural numbers for use with datakinds
data Nat where

wenkokke

{-# LANGUAGE GADTs, RankNTypes, TypeFamilies, DataKinds #-}
{-# LANGUAGE KindSignatures, TypeOperators, MultiParamTypeClasses #-}

module STL where

import Prelude hiding (True,False)
import qualified Data.Bool as B

type Name = String
type Entity = Int

wenkokke

\usepackage{array}
\usepackage{stmaryrd}

% display a one-level tower
\newcommand{\tower}[4][]{%
  \begin{array}{c|c}
    #4 & #3
    \\ \hline
    \multicolumn{2}{c}{#2}
    \\

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;