Permalink
Browse files

Better readme and other improvements

  • Loading branch information...
1 parent 4c34b3b commit bb868ec1fea3dd22815c36997617549bb18ce716 @andrejbauer andrejbauer committed Nov 7, 2012
Showing with 57 additions and 21 deletions.
  1. +1 −0 .gitignore
  2. +3 −0 Makefile
  3. +28 −13 README.markdown
  4. +12 −8 ctx.ml
  5. +2 −0 lexer.mll
  6. +2 −0 syntax.ml
  7. +9 −0 tt.odocl
View
1 .gitignore
@@ -3,6 +3,7 @@ _build
tt.native
tt.byte
parser.conflicts
+tt.docdir
# Backup files
*~
View
3 Makefile
@@ -3,3 +3,6 @@ all:
clean:
ocamlbuild -clean
+
+doc:
+ ocamlbuild -use-menhir -docflag -keep-code -lib unix tt.docdir/index.html
View
41 README.markdown
@@ -1,11 +1,19 @@
-A minimalist implementation of type theory with universes indexed by numerals and
-dependent products. The concrete syntax is as follows:
+A minimalist implementation of type theory with universes and dependent products. The
+concrete syntax is as follows:
* The universes are `Type 0`, `Type 1`, `Type 2`, ...
* A dependent product is written as `forall x : T1, T2`
* A function is written as `fun x : T => e`
* Application is written as `e1 e2`
+## Compilation
+
+You need `ocamlbuild` and `make`. You can type
+
+* `make` to make the `tt.native` executable.
+* `make clean` to clean up.
+* `make doc` to generate HTML documentation (see the generated `tt.docdir/index.html`).
+
## Usage
Type `Help.` in the interactive shell to see what the type system can do. Here is a sample
@@ -31,17 +39,24 @@ session:
## Source code
The purpose of the implementation is to keep the source uncomplicated and short. The
-essential bits of source code can be found in the following files:
+essential bits of source code can be found in the following files. It should be possible
+for you to just read the entire source code. You should start with the core
+
+* `syntax.ml` -- abstract syntax
+* `ctx.ml` -- contexts
+* `infer.ml` -- type inference and normalization
+
+and continue with the infrastructure
+
+* `tt.ml` -- interactive top level
+* `error.ml` -- error reporting
+* `lexer.mll` and `parser.mly` -- concrete sytnax
+* `beautify.ml` and `print.ml` -- pretty printing
-* `concrete.ml` the abstract syntax
-* `syntax.ml` compiled form of abstract syntax, where abstractions are Ocaml functions, normalization
-* `infer.ml` type checking
-The rest of the files are just logistics:
+## Inefficiency
-* `lexer.mll` lexical analysis of concrete syntax
-* `parser.mly` parser which converts concrete syntax to abstract syntax
-* `print.ml` pretty-printing of expressions
-* `common.ml` commonly used functions
-* `error.ml` printing of errors
-* `tt.ml` toplevel interactive shell
+The code is meant to be short and sweet, and close to how type theory is presented on
+paper. Therefore, it is not suitable for a real implementation, as it will get horribly
+inefficient as soon as you try anything complicated. But it should be useful for
+experimentation.
View
20 ctx.ml
@@ -1,17 +1,21 @@
-(* Contexts *)
-let lookup = List.assoc
+(** Handling of contexts.
+
+ A context is represented as an associative list which maps a variable [x]
+ to a pair [(t,e)] where [t] is its type and [e] is its value (optional).
+*)
-let index x ctx =
- let rec index k = function
- | [] -> raise Not_found
- | y :: ys -> if x = y then k else index (k+1) ys
- in
- index 0 ctx
+let lookup = List.assoc
+(** [lookup_ty x ctx] returns the type of [x] in context [ctx]. *)
let lookup_ty x ctx = fst (lookup x ctx)
+(** [lookup_ty x ctx] returns the value of [x] in context [ctx], or [None]
+ if [x] has no assigned value. *)
let lookup_value x ctx = snd (lookup x ctx)
+(** [extend x t ctx] returns [ctx] extended with variable [x] of type [t],
+ whereas [extend x t ~value:e ctx] returns [ctx] extended with variable [x]
+ of type [t] and assigned value [e]. *)
let extend x t ?value ctx = (x, (t, value)) :: ctx
View
2 lexer.mll
@@ -1,4 +1,6 @@
{
+ (** The lexer. *)
+
open Parser
let reserved = [
View
2 syntax.ml
@@ -1,3 +1,4 @@
+(** Abstract syntax of expressions and toplevel directives. *)
(** During substitution we generate fresh variable names. Because we want pretty printing,
each freshly generated variable name should "remember" its preferred form. Thus a
@@ -21,6 +22,7 @@ type expr =
| Lambda of abstraction
| App of expr * expr
+(** An abstraction [(x,t,e)] indicates that [x] of type [t] is bound in [e]. *)
and abstraction = variable * expr * expr
(** Toplevel directives. *)
View
9 tt.odocl
@@ -0,0 +1,9 @@
+Syntax
+Error
+Ctx
+Infer
+Tt
+Beautify
+Print
+
+

0 comments on commit bb868ec

Please sign in to comment.