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

%{ 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

module Bracket where

data Lam = Var Int | Ap Lam Lam | Lam Lam deriving Show
data SK  = S | K | SKAp SK SK deriving Show

data SKH = Var' Int | S' | K' | SKAp' SKH SKH

-- Remove one variable
bracket :: SKH -> SKH
bracket (Var' 0) = SKAp' (SKAp' S' K') K'

jozefg

module regex where
open import Data.Char using (Char;  _≟_)
open import Data.List using (List ; _∷_ ; [])
open import Relation.Binary.PropositionalEquality
open import Relation.Nullary
open import Data.Empty using (⊥)

-- Reason for this is because it simplifies pattern matching.
String : Set
String = List Char

jozefg

#! /usr/bin/env python3

import os
import os.path as path
import re
import collections
from ascii_graph import Pyasciigraph
import sys

imports_re = re.compile('^import (qualified )?([a-z\.A-Z0-9]+)')

jozefg

module general where
open import Function
import Data.Nat      as N
import Data.Fin      as F
import Data.Maybe    as M
import Relation.Nullary as R

data General (S : Set)(T : S -> Set)(X : Set) : Set where
  !!    : X -> General S T X
  _??_  : (s : S) -> (T s -> General S T X) -> General S T X

jozefg

open import Level
open import Relation.Nullary
open import Relation.Binary

module binary (ord : DecTotalOrder zero zero zero) where

A = DecTotalOrder.Carrier ord
open DecTotalOrder {{...}}

module bound where

jozefg

{-# OPTIONS --without-K #-}
module j-to-j where
open import Level

-- Gives rise to the annoying induction principle.
data _≡_ {A : Set} : A → A → Set where
  refl : ∀ {a : A} → a ≡ a

-- Ignore the "Level" junk in here. It's needed because
-- we're trying to eliminate into a Set1 (U1 in Peter's

jozefg

Operator iterate : (0; 1; 0).
[iterate(N; F; B)] =def= [natrec(N; B; _.x.so_apply(F; x))].

Operator top : ().
[top] =def= [⋂(void; _.void)].

Theorem top-is-top :
  [⋂(base; x.
   ⋂(base; y.
   =(x; y; top)))] {

jozefg

Operator Russell : ().
[Russell] =def= [{x : U{i} | not(member(x; x))}].

Tactic break-plus {
  @{ [x : _ + _ |- _] => elim <x> }
}.

Theorem u-in-u-wf : [member(member(U{i}; U{i}); U{i'})] {
  unfold <member>; eq-eq-base; unfold <bunion>; auto;
  csubst [ceq(U{i}; lam(x.snd(x)) pair(inr(<>); U{i}))]