From f73f4a2c98be86c1766fd5bd5524c58c0e618902 Mon Sep 17 00:00:00 2001 From: "William J. Bowman" Date: Tue, 22 Sep 2015 15:29:49 -0400 Subject: [PATCH] Finished documenting curnel forms --- scribblings/cur.scrbl | 49 ++------------- scribblings/curnel.scrbl | 132 +++++++++++++++++++++++++++++++++++++++ 2 files changed, 137 insertions(+), 44 deletions(-) create mode 100644 scribblings/curnel.scrbl diff --git a/scribblings/cur.scrbl b/scribblings/cur.scrbl index d583f59..dc0c42a 100644 --- a/scribblings/cur.scrbl +++ b/scribblings/cur.scrbl @@ -1,14 +1,9 @@ #lang scribble/manual @(require + "defs.rkt" racket/function) -@(define (todo . args) - (apply margin-note* "TODO: " args)) - -@(define (gtech x) - (tech x #:doc '(lib "scribblings/guide/guide.scrbl"))) - -@title{Cur} +@title[#:style '(toc)]{Cur} @author[@author+email["William J. Bowman" "wjb@williamjbowman.com"]] @defmodule[cur #:lang] @@ -37,41 +32,7 @@ and evaluating @racketmodname[cur] forms at compile-time. Programmers can use these reflection feature with little fear, as the resulting @tech{curnel forms} will always be type-checked prior to running. -@table-of-contents[] +@local-table-of-contents[] -@section{Curnel Forms} -@deftech{Curnel forms} are the core forms provided @racketmodname[cur]. -These form come directly from the trusted core and are all that remain at @gtech{runtime}. -The core of @racketmodname[cur] is essentially TT. -For a very understandable in-depth look at TT, see chapter 2 of -@hyperlink["https://eb.host.cs.st-andrews.ac.uk/writings/thesis.pdf" - "Practical Implementation of a Dependently Typed Functional Programming Language"], by -Edwin C. Brady. - -@(require racket/sandbox scribble/eval) -@(define curnel-eval - (parameterize ([sandbox-output 'string] - [sandbox-error-output 'string] - [sandbox-memory-limit 500]) - (make-module-evaluator "#lang cur"))) - - -@;(require (for-label cur/curnel/redex-lang)) -@defform*[((lambda (id : type-expr) body-expr) - (λ (id : type-expr) body-expr))]{ -Produces a single arity procedure, binding the identifier id in body-expr and in the type of -body-expr. -Both type-expr and body-expr can contain non-curnel forms, such as macros.} -@examples[#:eval curnel-eval - (lambda (x : Type) x) - (lambda (x : Type) x)] - -@examples[#:eval curnel-eval - (define-syntax-rule (computed-type _) Type) - (lambda (x : (computed-type bool)) x) - (lambda (x : Type) x)] - -@examples[#:eval curnel-eval - (lambda (a : Type) (lambda (x : a) x))] - -@section{Reflection Forms} +@include-section{curnel.scrbl} +@;@include-section{reflection.scrbl} diff --git a/scribblings/curnel.scrbl b/scribblings/curnel.scrbl new file mode 100644 index 0000000..53d9bc0 --- /dev/null +++ b/scribblings/curnel.scrbl @@ -0,0 +1,132 @@ +#lang scribble/manual + +@(require "defs.rkt") + +@title{Curnel Forms} +@deftech{Curnel forms} are the core forms provided @racketmodname[cur]. +These forms come directly from the trusted core and are all that remain after macro expansion. +@todo{Link to guide regarding macro expansion} +The core of @racketmodname[cur] is essentially TT. +For a very understandable in-depth look at TT, see chapter 2 of +@hyperlink["https://eb.host.cs.st-andrews.ac.uk/writings/thesis.pdf" + "Practical Implementation of a Dependently Typed Functional Programming Language"], by +Edwin C. Brady. + +@(require racket/sandbox scribble/eval) +@(define curnel-eval + (parameterize ([sandbox-output 'string] + [sandbox-error-output 'string] + [sandbox-eval-limits #f] + [sandbox-memory-limit #f]) + (make-module-evaluator "#lang cur"))) + +@defform[(Type n)]{ +Define the universe of types at level @racket[n], where @racket[n] is any natural number. + + +@examples[#:eval curnel-eval + (Type 0)] + +@examples[#:eval curnel-eval + (Type 1)] +} + +@defidform[Type]{ +A synonym for @racket[(Type 0)]. + + +@examples[#:eval curnel-eval + Type] +} + +@defform*[((lambda (id : type-expr) body-expr) + (λ (id : type-expr) body-expr))]{ +Produces a single arity procedure, binding the identifier @racket[id] of type @racket[type-expr] in @racket[body-expr] and in the type of +@racket[body-expr]. +Both @racket[type-expr] and @racket[body-expr] can contain non-curnel forms, such as macros. + +Currently, Cur will return the underlying representation of a procedure when a @racket[lambda] is +evaluated at the top-level. Do not rely on this representation. + +@examples[#:eval curnel-eval + (lambda (x : Type) x)] + +@examples[#:eval curnel-eval + (λ (x : Type) (lambda (y : x) y))] + + +@defform[(#%app procedure argument)]{ +Applies the single arity @racket[procedure] to @racket[argument]. +} + +@examples[#:eval curnel-eval + ((lambda (x : (Type 1)) x) Type)] + +@examples[#:eval curnel-eval + (#%app (lambda (x : (Type 1)) x) Type)] +} + +@defform*[((forall (id : type-expr) body-expr) + (∀ (id : type-expr) body-expr))]{ +Produces a dependent function type, binding the identifier @racket[id] of type @racket[type-expr] in @racket[body-expr]. + + +@examples[#:eval curnel-eval + (forall (x : Type) Type)] + +@examples[#:eval curnel-eval + (lambda (x : (forall (x : (Type 1)) Type)) + (x Type))] +} + +@defform[(data id : type-expr (id* : type-expr*) ...)]{ +Defines an inductive datatype named @racket[id] of type @racket[type-expr], with constructors +@racket[id*] each with the corresponding type @racket[type-expr*]. +Currently, Cur does not attempt to ensure the well-foundedness of the inductive definition. +For instance, Cur does not currently perform strict positivity checking. + + +@margin-note{The reader should pretend the errors that read "void: expected more" are not there.} + +@examples[#:eval curnel-eval + (data Bool : Type + (true : Bool) + (false : Bool)) + ((lambda (x : Bool) x) true) + (data False : Type) + (data And : (forall (A : Type) (forall (B : Type) Type)) + (conj : (forall (A : Type) (forall (B : Type) (forall (a : A) (forall (b : B) ((And A) B))))))) + ((((conj Bool) Bool) true) false)] +} + +@defform[(elim type-expr expr motive method* ...)]{ +Eliminates the expression @racket[expr] of the inductively defined type @racket[type-expr], using +@racket[motive], where the methods for each constructor for @racket[type-expr] are given by +@racket[method*]. + +The following example runs @racket[(sub1 (s z))]. + +@examples[#:eval curnel-eval + (data Nat : Type + (z : Nat) + (s : (forall (n : Nat) Nat))) + (elim Nat (s z) (lambda (x : Nat) Nat) + z + (lambda (n : Nat) (lambda (IH : Nat) n)))] +} + +@defform[(define id expr)]{ +Binds @racket[id] to the result of @racket[expr]. + +@examples[#:eval curnel-eval + (data Nat : Type + (z : Nat) + (s : (forall (n : Nat) Nat))) + (define sub1 (lambda (n : Nat) + (elim Nat n (lambda (x : Nat) Nat) + z + (lambda (n : Nat) (lambda (IH : Nat) n))))) + (sub1 (s (s z))) + (sub1 (s z)) + (sub1 z)] +}