------------------------------------------------------------------------
-- Code related to the paper Beating the Productivity Checker Using
-- Embedded Languages
--
-- Nils Anders Danielsson
------------------------------------------------------------------------

module Productivity where

------------------------------------------------------------------------
-- Making Programs Guarded

-- A definition of the stream of Fibonacci numbers, as well
-- as a definition of the Hamming numbers.

import StreamProg

------------------------------------------------------------------------
-- Several Types at Once

-- By indexing the program and WHNF types on a universe one can handle
-- several types at the same time.

import Universe

-- Breadth-first labelling of trees, /almost/ implementing the classic
-- tie-the-recursive-knot algorithm due to Jeremy Gibbons and Geraint
-- Jones (see "Linear-time Breadth-first Tree Algorithms: An Exercise
-- in the Arithmetic of Folds and Zips", or Chris Okasaki's
-- explanation in "Breadth-First Numbering: Lessons from a Small
-- Exercise in Algorithm Design"). Proper sharing is not maintained,
-- though, so this implementation is far from being linear in the size
-- of the tree.

import Stream
import Tree
import BreadthFirst.Universe
import BreadthFirst.Programs
import BreadthFirst

-- A simplified variant of the code above, without any correctness
-- statement or proof.

import BreadthFirstWithoutProof

------------------------------------------------------------------------
-- Making Proofs Guarded

-- Proofs of the map-iterate property and iterate fusion.

import MapIterate

-- A formalisation of parts of Ralf Hinze's paper "Streams and Unique
-- Fixed Points".

import Stream
import Stream.Programs
import Stream.Equality
import Stream.Pointwise
import Hinze.Lemmas
import Hinze.Section2-4
import Hinze.Section3
import Hinze.Simplified.Section2-4
import Hinze.Simplified.Section3

-- Code not mentioned in the paper:

-- An investigation of various ways to define the semantics of an
-- untyped λ-calculus and a virtual machine, and a discussion of
-- compiler correctness. The module Lambda.Closure.Relational uses the
-- language-based technique to establish guardedness.

import Lambda
import Lambda.Closure.Relational

------------------------------------------------------------------------
-- Destructors

-- A somewhat more elaborate/complicated variant of the method which
-- can handle functions like tail.

import SingletonChunks

-- Code not mentioned in the paper:

-- Another variant which can handle tail. I believe that this one has
-- limited applicability.

import LargeCombinators

------------------------------------------------------------------------
-- Other Chunk Sizes

-- A generalised variant of (parts of) SingletonChunks, plus some
-- extra examples.

import ArbitraryChunks

-- Implementations of the Thue-Morse sequence, using non-uniform chunk
-- sizes.

import ThueMorse
import ThueMorseLeq

------------------------------------------------------------------------
-- Nested Applications

-- An example which shows that nested applications of the defined
-- function can be handled.

import Nested

-- Code not mentioned in the paper:

-- A solution to a problem posed by Venanzio Capretta: The equation
--
--   φ s = s ⋎ φ (evens (φ s))
--
-- has at most one solution. (Notice the nested uses of φ, and the use
-- of evens which removes every other element from its input.)

import VenanziosProblem

------------------------------------------------------------------------
-- Related Work

-- Formalisation of subtyping for recursive types, partly based on
-- "Coinductive Axiomatization of Recursive Type Equality and
-- Subtyping" by Michael Brandt and Fritz Henglein.

import RecursiveTypes

-- The following modules use the language-based technique to establish
-- guardedness. The last of them was briefly discussed in the paper.

import RecursiveTypes.Subtyping.Semantic.Coinductive
import RecursiveTypes.Subtyping.Axiomatic.Coinductive
import RecursiveTypes.Subtyping.Axiomatic.Inductive

-- An implementation of "A Unifying Approach to Recursive and
-- Co-recursive Definitions" by Pietro Di Gianantonio and Marino
-- Miculan. Contains one postulate.

import Contractive
import Contractive.Function
import Contractive.Stream
import Contractive.Examples

------------------------------------------------------------------------
-- Appendix

-- A sound, inductive approximation of stream equality.

import InductiveStreamEquality