Effectful Staging Project
       Joint work with Yukiyoshi Kameyama and Chung-chieh Shan

Staging with effects of delimited dynamic extent

     Shifting the Stage: Staging with Delimited Control
     Yukiyoshi Kameyama, Oleg Kiselyov, and Chung-chieh Shan
     PEPM 2009.

circle-shift.pdf		The PEPM09 paper

	Mechanizations of the staged lambda-calculus with shift/reset
circle-shift-1.elf		lambda-circle calculus with shift/reset:
  two-stage calculus with delimited control effects.
  This Twelf code defines the calculus and its static (type checking)
  and dynamic semantics.
  The code proves the type soundness (type preservation and progress)
  of the type system. The code uses the intrinsic encoding of the calculus.
  The code contains many examples, including the staged Gibonacci example
  with memoization and let-insertion.
  See "HOW TO RUN TWELF CODE" at the end of this file.


circle-shift-n.elf		Multi-staged calculus with delimited control
  The calculus has arbitrarily many stages, and is an extension of
  lambda-circle with delimited control.
  This Twelf code defines the calculus and its static (type checking)
  and dynamic semantics.
  The code proves the type soundness (type preservation and progress)
  of the type system. The code uses the intrinsic encoding of the calculus.
  See "HOW TO RUN TWELF CODE" at the end of this file.


circle-shift.elf		The old version of circle-shift-1.elf,
		mainly of historical interest. This old version
		used an extrinsic encoding of the calculus. It was
		written before the paper, giving us the needed
		experience with the calculus. The main difference 
		from the calculus in the paper is the distinction 
		between `pure' and `impure' types. Present-stage
		computations that cannot have control effects
		have pure types, without answer-type annotations, and 
		so are implicitly answer-type polymorphic.
		The `pure' type and computation distinction makes 
		the type system quite complex.
  		See "HOW TO RUN TWELF CODE" at the end of this file.


	Gibonacci example -- generating efficient specialized
	versions of the generalized Fibonacci function in direct style. 
	The code files below describe a progression of attempts,
	from inefficient unstaged Gibonacci, memoized Gibonacci, 
	naively staged and inefficient function and finally to the
	efficient memoization with let-insertion. The dangers of scope
	extrusion are well illustrated. The specialized Gibonacci generator
	is written in direct, rather than monadic or CPS style.
fib.ml				With the explicit fix-point combinator
fib1.ml				Without the explicit fix-point combinator
				All the code is in MetaOCaml

	Generating optimal specialized code for the longest common 
	subsequence: another example of dynamic meta-programming in 
	direct style
lcs.ml				The complete MetaOCaml code


		Generating a family of Gaussian Elimination codes
		in direct style, without either functors or monads
ge_unstaged.ml			Unstaged, textbook Gaussian elimination code,
				in OCaml
ge_gen.ml			Staged ge_unstaged.ml, in MetaOCaml.
				The staged code generates
				a family of GE codes (with or without 
				determinant computation, etc). We pay 
				no performance penalty for the added
				flexibility. 

		Matrix Multiplication and Markov Chains:
		the Band Markov Chains problem
band_markov_orig.ml		The original code by Walid Taha,
				downloaded from 
				http://metaocaml.org/examples/band-markov.ml
				This code is used here for reference and
				comparison with the implementation below.

band_markov_lc.ml		Re-writing of the original code using
				delimited control rather than mutation,
				while checking for the restriction imposed by
				the circle-shift-1 calculus.




Translating the staging away

     Closing the Stage: From staged code to typed closures
     Yukiyoshi Kameyama, Oleg Kiselyov, and Chung-chieh Shan
     PEPM 2008.

metafx.pdf			The paper

meta-scheme.scm			Examples of the staged code and its translation 
  This file contains the complete code for all the examples in the paper
  plus extra examples. 
  The source language is MetaOCaml. The target language is supposed to be 
  System F. We try to emulate it in plain OCaml, using first-class (record)
  polymorphism where needed.


lambda-am1.elf		The implementation of the lambda^a_{v1} calculus
  This is the two-stage calculus with run and cross-stage persistence,
  which is a close model of MetaOCaml (restricted to two stages).
  The calculus is the source language of the translation.
  This Twelf code defines the syntax, static and the dynamic semantics
  of the calculus, and proves several meta-theorems (context
  decomposition, subject reduction for primitive reductions).
  See "HOW TO RUN TWELF CODE" at the end of this file.

power-count.ml			Specializing the power function while
 determining the number of multiplications in the generated code.
 It is easiest to write this example if we use a side effect such as
 mutable state in MetaOCaml, but such an extension (a piece of state of
 type int) has not been shown sound except through our translation. 
 Second, we can write this example in pure MetaOCaml (more awkwardly) using 
 our environment-passing translation.

 
HOW TO RUN TWELF CODE
---------------------

First, one needs the Twelf, or more precisely, twelf-server.
Twelf can be downloaded from
       http://twelf.plparty.org/wiki/Main_Page

Each of the *.elf files mentioned earlier comes with the corresponding
*.cfg file to run the .elf file.

To `run', for example, circle-shift-1.elf, verifying the theorems
and running the sample code and unit tests, one should enter on
the command line

   echo "make circle-shift-1.cfg" | twelf/bin/twelf-server
If everything checks, one would see at the very end:
   %% OK %%