rntz

open import Level renaming (zero to lzero; suc to lsuc)
open import Relation.Binary
open import Data.List
open import Data.List.Properties
open import Data.Unit hiding (_≤_)
open import Data.Product
open import Relation.Binary.PropositionalEquality
open import Data.Fin
open import Data.Nat as ℕ hiding (_≤_)

rntz

#!/bin/bash
set -e
echo "digraph {"

# Generate the node names.
find . -iname '*.agda' '!' -name '.*' |
    sed -Ee 's,^\./,,;s,.agda$,,;s,/,.,g;s/.*/"&" [label="&"];/'

# Generate edges.
find . -iname '*.agda' '!' -name '.*' |

rntz

(* A bidirectionally-typed λ-calculus looks like:

  types  A,B ∷= base | A → B
  terms  M ∷= E | λx.M
  exprs  E ∷= x | E M | (M : A)

This is an exploration of how to encode this in OCaml using _structural_
typing (polymorphic variants & equirecursive types), rather than _nominal_
typing. *)

rntz

type var = string
type tp = Base | Fn of tp * tp

(* Normal & neutral term formers. *)
type ('norm, 'neut) neutF
  = [ `Var of var
    | `App of 'neut * 'norm ]
type ('norm, 'neut) normF =
  [ ('norm, 'neut) neutF
  | `Lam of var * 'norm ]

rntz

(* A bidirectionally-typed λ-calculus looks like:

  types  A,B ∷= base | A → B
  terms  M ∷= E | λx.M
  exprs  E ∷= x | E M | (M : A)

This is an exploration of how to encode this in OCaml using _structural_
typing (polymorphic variants & equirecursive types), rather than _nominal_
typing. As you'll see, it's not entirely satisfying. *)

rntz

{-# 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)

rntz

#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]

rntz

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 as ℕ using (ℕ; _∸_)
open import Data.Product
open import Data.Sum
open import Relation.Binary
open import Relation.Binary.PropositionalEquality

rntz

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

rntz

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).