View ToneInference.hs
{-# LANGUAGE FlexibleInstances #-}
module MiniToneInference where
import Prelude hiding ((&&))
import Control.Applicative
import Control.Monad
import Data.Map.Strict (Map, (!))
import Data.Maybe (fromJust)
import Data.Monoid ((<>))
import Data.Set (isSubsetOf)
View tone-inference.rkt
#lang racket
(require racket/hash rackunit)
;;; ---------- TONES and TONE CONTEXTS ---------- ;;;
(define tone? (or/c 'id 'op 'iso 'path))
(define (tone<=? a b)
(match* (a b)
[('iso _) #t] [(_ 'path) #t]
[(x x) #t]
View Fulcrum.agda
module Fulcrum where
open import Data.Integer as
open import Data.List hiding (sum)
open import Data.List.Any; open Membership-≡
open import Data.Nat asusing (ℕ; _∸_)
open import Data.Product
open import Data.Sum
open import Relation.Binary
open import Relation.Binary.PropositionalEquality
View Unique.agda
module Unique where
-- I deal with naturals instead of integers. with a bit more effort, I could
-- probably have parameterized this over any type with decidable equality.
open import Data.Nat
open import Data.Product
open import Data.List hiding (any)
open import Data.List.Any
open import Relation.Nullary
open import Relation.Binary.PropositionalEquality
View leftpad.agda
module HillelVerificationProblems where
open import Data.Nat
open import Data.Nat.Properties.Simple using (+-right-identity; +-comm)
open import Data.List
open import Data.List.All
open import Data.List.Properties
open import Relation.Binary.PropositionalEquality
-- NB. (a ∸ b) is saturating subtraction and (a ⊔ b) is max(a,b).
View tonetheory.ml
(* A quick note about preorders; skip this if you know about them.
*
* A preorder is a relation (a ≤ b) satisfying two rules:
* 1. Reflexivity: a ≤ a.
* 2. Transitivity: if a ≤ b and b ≤ c then a ≤ c.
*
* A good example of a preorder is "lists under containment":
* let (X ≤ Y) if every element of the list X is also in Y.
*
* Preorders are like partial orders, but without requiring antisymmetry.
View Preorders.agda
{-# OPTIONS --postfix-projections #-}
module Preorders where
open import Level
open import Data.Unit hiding (_≤_)
open import Data.Product hiding (map)
open import Function hiding (id)
open import Relation.Binary public using (Reflexive; Transitive; Symmetric; _=[_]⇒_)
import Relation.Binary.PropositionalEquality as Eq
open Eq using (_≡_)
View MinimalNBE.hs
-- A simply-typed lambda calculus, and a definition of normalisation by
-- evaluation for it.
--
-- The NBE implementation is based on a presentation by Sam Lindley from 2016:
-- http://homepages.inf.ed.ac.uk/slindley/nbe/nbe-cambridge2016.pdf
--
-- Adapted to handle terms with explicitly typed contexts (Sam's slides only
-- consider open terms with the environments left implicit/untyped). This was a
-- pain in the ass to figure out.
View omega-category.agda
open import Level
-- "Wok" stands for "weak omega kategory".
mutual
record Wok {i} (Obj : Set i) : Set (suc i) where
coinductive
constructor Wok:
infix 1 Hom
infixr 9 compo
field Arr : (a b : Obj) -> Set i
field Hom : (a b : Obj) -> Wok (Arr a b)
View stuff.agda
open import Relation.Nullary
open import Data.Product
open import Function
module _ {i j} {A : Set i} {B : A -> Set j} where
-- ∀¬ and ¬∃ are interprovable constructively:
¬∃→∀¬ : ¬ (Σ A B) a -> ¬ B a; ¬∃→∀¬ = curry
¬→¬∃ : (∀ a -> ¬ B a) -> ¬ Σ A B; ¬→¬∃ = uncurry
-- So in particular, ¬∀¬ and ¬¬∃ are interprovable: