* Installation

The following instructions will install the interpreter and the quote
transformer into this folder.

** Windows using ghc --make:

> cd src
> ghc --make PTS\Main.hs
> ghc --make PTS\Quote\Main.hs
> move PTS\Main.exe ..\pts.exe
> move PTS\Quote\Main.exe ..\quote.exe
> cd ..

** Windows using Cygwin and GNU make

$ cd src
$ make windows
$ mv pts.exe ..
$ mv quote.exe ..
$ cd ..

** Unix using ghc --make

$ cd src
$ ghc --make PTS/Main.hs
$ ghc --make PTS/Quote/Main.hs
$ mv PTS/Main ../pts
$ mv PTS/Quote/Main ../quote
$ cd ..

** Unix using GNU make

$ cd src
$ make unix
$ mv pts ..
$ mv quote ..
$ cd ..


* Running the interpreter

The interpreter is executed with the following command:
> pts.exe fomegastar <filename>
or in Unix:
$ ./pts fomegastar <filename>

The file has to be a sequence of statements, where a statement is
either of the form "var = term;" or "term;".  In the first case, the
type of the term is inferred and the term is assigned to the variable
"var" in the environment of the interpreter.  The term and its type
are printed to the console.  In the second case, the type of the term is
inferred and the term is evaluated. The term, its type, and the
resulting value are printed to the console.

The file "sample.fos" is an example.  It implements the language
interface, the self-interpreter and the quoted version of the
polymorphic identity function from the paper.

Note that the interpreter works for several PTS instances. Besides the
option fomegastar you can also choose simplytyped (STLC), fomega,
lambdastar, coc (calculus of constructions), and fomegaomega (Fomega
with an infinite hierarchy of universes).

As it is a more general interpreter for PTS instances, the Fomega*
syntax has to be transformed into "PTS syntax".  Furthermore, we
restrict the syntax to ASCII symbols.  In addition, we added natural
numbers, and added corresponding operations to the language interface.
In effect, we have the following terms:

- Natural numbers
- Constants: Nat, *, **
- Variables: arbitrary words, excluding natural numbers and constants,
  satisfying the following conditions:
  - They are not keywords (lambda, Pi, if0, then, else, ->, add, mul,
    sub, div)
  - They do not contain any of the following characters: .:=;/()
- Binary operations on numbers: add t t, sub t t, mul t t, div t t
- If-expression (intuition: check whether the first term evaluates to zero)
  if0 t then t else t
- Abstraction: lambda t : t. t
- Application: t t
- Dependent product: Pi x : t. t
- Arrow type (syntactic sugar for the dependent product): t -> t

Fomega* terms and types have to be adapted according to the following
rules:
- t [T]		    -> t T
- \x : T. t 	    -> lambda x : T. t
- /\X :: T. t 	    -> lambda X : T. t
- box 	    	    -> **
- \x :: T. T 	    -> lambda x : T. T
- forall X :: T. T  -> Pi X : T. T
- Pi X :: T. T 	    -> Pi X : T. T


* Running the quote transformer

The quote transformer transforms an Fomega* term t (read from the
standard input) to a quoted term <t>.  In contrast to the paper
version of quoting, the operations ifzero, add, sub, mul, and div
belong to the language interface, as well.

For example, the following command: (Windows)
> echo lambda X : *. lambda x : X. x | quote.exe
or: (Unix)
$ echo "lambda X : *. lambda x : X. x" | ./quote
prints the quoted polymorphic identity function to the console.