copumpkin

module Unify where

-- Translated from http://strictlypositive.org/unify.ps.gz

open import Data.Empty
import Data.Maybe as Maybe
open Maybe hiding (map)
open import Data.Nat
open import Data.Fin
open import Data.Product hiding (map)

polytypic

// So called van Laarhoven lenses, named after their discoverer, have a number
// of nice properties as explained by Russell O'Connor:
//
//   http://r6.ca/blog/20120623T104901Z.html
//
// Unfortunately their typing (in Haskell)
//
//   type Lens s t a b = forall f. Functor f => (a -> f b) -> (s -> f t)
//
// seems to be well outside of what can be achieved in F#.

rntz

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

AndrasKovacs

{-# language Strict, LambdaCase, BlockArguments #-}
{-# options_ghc -Wincomplete-patterns #-}

{-
Minimal demo of "glued" evaluation in the style of Olle Fredriksson:

  https://github.com/ollef/sixty

The main idea is that during elaboration, we need different evaluation