From 57ece3f787ff2cf4d75d043ccc7bda29d4c4856c Mon Sep 17 00:00:00 2001 From: "William J. Bowman" Date: Tue, 10 Nov 2015 16:16:33 -0500 Subject: [PATCH] More documentation fixes --- scribblings/curnel.scrbl | 25 ++++++++++--------------- scribblings/defs.rkt | 3 +-- scribblings/reflection.scrbl | 9 ++------- scribblings/stdlib/bool.scrbl | 8 +++++--- scribblings/stdlib/sugar.scrbl | 13 ++++--------- scribblings/stdlib/tactics.scrbl | 27 ++++++++++++--------------- 6 files changed, 34 insertions(+), 51 deletions(-) diff --git a/scribblings/curnel.scrbl b/scribblings/curnel.scrbl index 4deb113..1bad8e1 100644 --- a/scribblings/curnel.scrbl +++ b/scribblings/curnel.scrbl @@ -1,28 +1,27 @@ #lang scribble/manual -@(require "defs.rkt") +@(require + "defs.rkt" + scribble/eval) @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. +The core of @racketmodname[cur] is essentially TT with an impredicative universe @racket[(Type 0)]. 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"))) +@(define curnel-eval (curnel-sandbox "")) -@defform[(Type n)]{ +@defform*[((Type n) + Type)]{ Define the universe of types at level @racket[n], where @racket[n] is any natural number. - +@racket[Type] is a synonym for @racket[(Type 0)]. Cur is impredicative +in @racket[(Type 0)], although this is likely to change to a more +restricted impredicative universe. @examples[#:eval curnel-eval (Type 0)] @@ -31,10 +30,6 @@ Define the universe of types at level @racket[n], where @racket[n] is any natura (Type 1)] } -@defidform[Type]{ -A synonym for @racket[(Type 0)]. - - @examples[#:eval curnel-eval Type] } diff --git a/scribblings/defs.rkt b/scribblings/defs.rkt index 39c6b73..67fd99f 100644 --- a/scribblings/defs.rkt +++ b/scribblings/defs.rkt @@ -3,8 +3,7 @@ (require scribble/base scribble/manual - racket/sandbox - scribble/eval) + racket/sandbox) (provide (all-defined-out)) (define (todo . ls) diff --git a/scribblings/reflection.scrbl b/scribblings/reflection.scrbl index 3bfef87..be97572 100644 --- a/scribblings/reflection.scrbl +++ b/scribblings/reflection.scrbl @@ -2,6 +2,7 @@ @(require "defs.rkt" + scribble/eval (for-label (only-in racket local-expand))) @title{Reflection} @@ -10,13 +11,7 @@ various parts of the language implementation as Racket forms at @gtech{phase} 1. The reflection features are @emph{unstable} and may change without warning. Many of these features are extremely hacky. -@(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 (require cur/stdlib/bool) (require cur/stdlib/nat)"))) +@(define curnel-eval (curnel-sandbox "(require cur/stdlib/bool cur/stdlib/nat)")) @defproc[(cur-expand [syn syntax?] [id identifier?] ...) syntax?]{ diff --git a/scribblings/stdlib/bool.scrbl b/scribblings/stdlib/bool.scrbl index 28ce96d..b38f11f 100644 --- a/scribblings/stdlib/bool.scrbl +++ b/scribblings/stdlib/bool.scrbl @@ -1,8 +1,10 @@ #lang scribble/manual -@(require "../defs.rkt") +@(require + "../defs.rkt" + scribble/eval) -@(define curnel-eval "(require cur/stdlib/bool cur/stdlib/sugar)") +@(define curnel-eval (curnel-sandbox "(require cur/stdlib/bool cur/stdlib/sugar)")) @title{Bool} @defmodule[cur/stdlib/bool] @@ -49,4 +51,4 @@ The boolean @racket[or]. True if and only if either @racket[x] or @racket[y] is (or true true) (or false true) (or false false)] -} \ No newline at end of file +} diff --git a/scribblings/stdlib/sugar.scrbl b/scribblings/stdlib/sugar.scrbl index 7f045cc..9a8f6c2 100644 --- a/scribblings/stdlib/sugar.scrbl +++ b/scribblings/stdlib/sugar.scrbl @@ -1,15 +1,10 @@ #lang scribble/manual -@(require "../defs.rkt") +@(require + "../defs.rkt" + scribble/eval) -@;(TODO Move this to defs.rkt) -@(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 (require cur/stdlib/bool) (require cur/stdlib/sugar)"))) +@(define curnel-eval (curnel-sandbox "(require cur/stdlib/bool cur/stdlib/sugar)")) @title{Sugar} diff --git a/scribblings/stdlib/tactics.scrbl b/scribblings/stdlib/tactics.scrbl index b6d92f1..23d0b1b 100644 --- a/scribblings/stdlib/tactics.scrbl +++ b/scribblings/stdlib/tactics.scrbl @@ -1,19 +1,15 @@ #lang scribble/manual -@(require "../defs.rkt") +@(require + "../defs.rkt" + scribble/eval) @title{Tactics} As Coq has shown, tactics have proven useful for doing complex proofs. In Cur, tactics are not built-in or provided by the language. However, any user can use meta-programming to add tactics to Cur. A tactic system ships in the standard library, written entirely in user-land code. -@(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 (require cur/stdlib/tactics/base) (require cur/stdlib/tactics/standard) (require cur/stdlib/bool) (require cur/stdlib/nat)"))) +@(define curnel-eval (curnel-sandbox "(require cur/stdlib/tactics/base cur/stdlib/tactics/standard cur/stdlib/bool cur/stdlib/nat)")) @section{Proof State and Defining Tactics} @defmodule[cur/stdlib/tactics/base] @@ -57,17 +53,17 @@ Returns an empty partial @tech{proof}, i.e., the identity function. [current-goal natural-number/c] [proof (or/c syntax? procedure?)] [theorem syntax?])]{ -A structure representing the @deftech{proof state} for the proof of the current theorem. +A structure representing the @deftech{proof state} for the proof of the current @tech{theorem}. -The environment @racket[env] is a map of assumptions local to the theorem from symbols (names) to the +The @deftech{environment} @racket[env] is a map of assumptions local to the @tech{proof} from symbols (names) to the type of the assumption as a syntax object. -The list of goals @racket[goals] is a map from natural numbers to goals, types as syntax objects. -The current goal @racket[current-goal] is a natural number indexing into @racket[goals], representing +The list of @deftech{goals} @racket[goals] is a map from natural numbers to goals, types as syntax objects. +The @deftech{current goal} @racket[current-goal] is a natural number indexing into @racket[goals], representing the goal currently in focus. -The @racket[proof] is the @tech{proof} of the theorem so far. The @racket[proof] is either a +The @racket[proof] is the @tech{proof} of the @tech{theorem} so far. The @racket[proof] is either a syntax object if complete, or a procedure which expects a proof to replace the current holes in the @racket[proof]. -The @racket[theorem] is the original statement of the theorem to be proved. +The @racket[theorem] is the original statement of the @tech{theorem} to be proved. } @defproc[(new-proof-state [prop syntax?]) @@ -148,7 +144,8 @@ tactic is defined and a theorem has been defined but not proved. } @defform[(define-theorem name prop)]{ -Defines a new theorem. +Defines a new @deftech{theorem}. Theorem are Cur types that can be +inhabited using the tactic language starting with @racket[proof]. } @defform[(proof (tactic args ...) ...)]{