------------------------------------------------------------------------
-- Examples involving simple λ-calculi
------------------------------------------------------------------------

{-# OPTIONS --without-K #-}

module README.Lambda where

------------------------------------------------------------------------
-- An untyped λ-calculus with constants

-- Some developments from "Operational Semantics Using the Partiality
-- Monad" by Danielsson, implemented using both the quotient
-- inductive-inductive partiality monad, and the delay monad.
--
-- These developments to a large extent mirror developments in
-- "Coinductive big-step operational semantics" by Leroy and Grall.

-- The syntax of, and a type system for, the untyped λ-calculus with
-- constants.

import Lambda.Syntax

-- Most of a virtual machine.

import Lambda.Virtual-machine

-- A compiler.

import Lambda.Compiler

-- A definitional interpreter.

import Lambda.Partiality-monad.Inductive.Interpreter
import Lambda.Delay-monad.Interpreter

-- A type soundness result.

import Lambda.Partiality-monad.Inductive.Type-soundness
import Lambda.Delay-monad.Type-soundness

-- A virtual machine.

import Lambda.Partiality-monad.Inductive.Virtual-machine
import Lambda.Delay-monad.Virtual-machine

-- Compiler correctness.

import Lambda.Partiality-monad.Inductive.Compiler-correctness
import Lambda.Delay-monad.Compiler-correctness

------------------------------------------------------------------------
-- An untyped λ-calculus without constants

-- A variant of the development above. The development above uses a
-- well-scoped variant of the untyped λ-calculus with constants. This
-- development does not use constants. This means that the interpreter
-- cannot crash, so the type soundness result has been omitted.

import Lambda.Simplified.Syntax
import Lambda.Simplified.Virtual-machine
import Lambda.Simplified.Compiler
import Lambda.Simplified.Partiality-monad.Inductive.Interpreter
import Lambda.Simplified.Delay-monad.Interpreter
import Lambda.Simplified.Partiality-monad.Inductive.Virtual-machine
import Lambda.Simplified.Delay-monad.Virtual-machine
import Lambda.Simplified.Partiality-monad.Inductive.Compiler-correctness
import Lambda.Simplified.Delay-monad.Compiler-correctness