More work on docs

info.rkt

@@ -2,7 +2,7 @@
 (define collection "cur")
 (define deps '("base" "rackunit-lib" ("redex-lib" #:version "1.6")))
 (define build-deps '("scribble-lib" "racket-doc"))
-(define scribblings '(("scribblings/cur.scrbl" ())))
+(define scribblings '(("scribblings/cur.scrbl" (multi-page))))
 (define pkg-desc "Dependent types with parenthesis and meta-programming.")
 (define version "0.1")
 (define pkg-authors '(wilbowma))

scribblings/cur.scrbl

@@ -1,25 +1,77 @@
 #lang scribble/manual
-@require[@for-label[cur racket/base]]
+@(require
+   racket/function)
+
+@(define (todo . args)
+   (apply margin-note* "TODO: " args))
+
+@(define (gtech x)
+   (tech x #:doc '(lib "scribblings/guide/guide.scrbl")))
 
 @title{Cur}
-@author{wilbowma (William J. Bowman @url{https://www.williamjbowman.com/})}
+@author[@author+email["William J. Bowman" "wjb@williamjbowman.com"]]
 
 @defmodule[cur #:lang]
 
-Cur is a simple dependently-typed language that arbitrary Racket meta-programs can manipulate. The
+The language @racketmodname[cur] is a dependently-typed language that arbitrary Racket meta-programs
-core logic of @racketmod[#:lang cur] is essentially UTT (@todo{citation needed}). The trusted core
+can manipulate.
-provides nothing beyond this logic. However, Racket meta-programming provides features such as
+The core language of @racketmodname[cur] is essentially TT@todo{citation
-modules, top-level definitions, multi-arity functions, implicit partial application, syntax notations,
+e.g. https://eb.host.cs.st-andrews.ac.uk/writings/thesis.pdf chapter 2}.
-a tactic DSL, interactive tactics, and a programming language meta-theory DSL. All these features are
+The trusted core provides nothing beyond this language.
-provided by user-land code
+However, untrusted user-land code provides, via Racket meta-programming, features such as modules, top-level
+definitions, multi-arity functions, implicit partial application, syntax notations, a tactic DSL,
+interactive tactics, and a programming language meta-theory DSL.
+These features run at compile time and generate @tech{curnel forms}, forms in the core language,
+which are type-checked before they are run.
 
-Arbitrary @racketmod[racket] code can run at @tech{phases} higher than 0, but @racketmod[racket] code at
+Arbitrary @racketmodname[racket] code can run at @gtech{phases} higher than 0, but
-@tech{phase} 0 is unsupported and should result in an error. The language @racket[#:lang cur] exports
+@racketmodname[racket] code at @gtech{phase} 0 is unsupported and should result in a syntax error.
-everything in @racketmod[racket], @racketmod[racket/syntax], and @racketmod[syntax/parse] at
+The language @racketmodname[cur] exports everything in @racketmodname[racket],
-@tech{phase} 1.
+@racketmodname[racket/syntax], and @racketmodname[syntax/parse] at @gtech{phase} 1.
 
-Cur provides reflection features to enables more advanced meta-programming. Cur exports Racket
+The language @racketmodname[cur] provides reflection features to equip users with the tools necessary
-functions at @tech{phase} 1 for type checking Cur terms, performing naïve type inference on Cur terms,
+to write advanced meta-programs.
-deciding equivalence between Cur terms, expanding macros in Cur terms, and evaluating Cur terms at
+These features in includes compile-time functions for type-checking, performing naïve type inference,
-compile-time. Programmers can use these reflection feature with little fear, as the resulting
+deciding equivalence between @racketmodname[cur] terms, expanding macros in @racketmodname[cur] forms,
-@tech{phase} 0 terms will always be type-checked again.
+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[]
+
+@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}