From ed57d034dc8b8c38d74ebcb3a0481fcef724dd4b Mon Sep 17 00:00:00 2001 From: "William J. Bowman" Date: Mon, 18 Jan 2016 14:03:42 -0500 Subject: [PATCH] Updated documentation --- cur-doc/cur/scribblings/stdlib/list.scrbl | 2 +- cur-doc/cur/scribblings/stdlib/sugar.scrbl | 123 ++++++++---------- .../cur/scribblings/stdlib/typeclass.scrbl | 2 +- cur-test/cur/tests/stdlib/maybe.rkt | 13 +- 4 files changed, 63 insertions(+), 77 deletions(-) diff --git a/cur-doc/cur/scribblings/stdlib/list.scrbl b/cur-doc/cur/scribblings/stdlib/list.scrbl index 294e7b1..804fff8 100644 --- a/cur-doc/cur/scribblings/stdlib/list.scrbl +++ b/cur-doc/cur/scribblings/stdlib/list.scrbl @@ -12,7 +12,7 @@ This library defines the datatype @racket[List] and several functions on them. @deftogether[(@defthing[List (-> Type Type)] @defthing[nil (forall (A : Type) (List A))] - @defthing[cons (forall* (A : Type) (a : A) (-> (List A) (List A)))])]{ + @defthing[cons (forall (A : Type) (a : A) (-> (List A) (List A)))])]{ The polymorphic list datatype. } diff --git a/cur-doc/cur/scribblings/stdlib/sugar.scrbl b/cur-doc/cur/scribblings/stdlib/sugar.scrbl index 877221f..1499bc2 100644 --- a/cur-doc/cur/scribblings/stdlib/sugar.scrbl +++ b/cur-doc/cur/scribblings/stdlib/sugar.scrbl @@ -4,7 +4,7 @@ "../defs.rkt" scribble/eval) -@(define curnel-eval (curnel-sandbox "(require cur/stdlib/nat cur/stdlib/bool cur/stdlib/sugar)")) +@(define curnel-eval (curnel-sandbox "(require cur/stdlib/nat cur/stdlib/bool cur/stdlib/sugar cur/stdlib/list)")) @title{Sugar} @@ -18,46 +18,36 @@ that expands into the eliminator. @defmodule[cur/stdlib/sugar] This library defines various syntactic extensions making Cur easier to write than writing raw TT. -@defform*[((-> t1 t2) - (→ t1 t2))]{ -A non-dependent function type Equivalent to @racket[(forall (_ : t1) t2)], where @racket[_] indicates an variable that is not used. +@defform*[((-> decl decl ... type) + (→ decl decl ... type) + (forall decl decl ... type) + (∀ decl decl ... type)) + #:grammar + [(decl + type + (code:line (identifier : type)))]]{ +A multi-artiy function type that supports dependent and non-dependent type declarations and automatic currying. @examples[#:eval curnel-eval - (data And : (-> Type (-> Type Type)) - (conj : (forall (A : Type) (forall (B : Type) (-> A (-> B ((And A) B))))))) + (data And : (-> Type Type) + (conj : (-> (A : Type) (B : Type) A B ((And A) B)))) ((((conj Bool) Bool) true) false)] } -@defform*[((->* t ...) - (→* t ...))]{ -A non-dependent multi-arity function type that supports automatic currying. - @examples[#:eval curnel-eval - (data And : (->* Type Type Type) - (conj : (forall (A : Type) (forall (B : Type) (->* A B ((And A) B)))))) - ((((conj Bool) Bool) true) false)] -} - - -@defform*[((forall* (a : t) ... type) - (∀* (a : t) ... type))]{ -A multi-arity function type that supports automatic currying. - -@examples[#:eval curnel-eval - (data And : (->* Type Type Type) - (conj : (forall* (A : Type) (B : Type) - (->* A B ((And A) B))))) + (data And : (forall Type Type Type) + (conj : (forall (A : Type) (B : Type) A B ((And A) B)))) ((((conj Bool) Bool) true) false)] } -@defform*[((lambda* (a : t) ... body) - (λ* (a : t) ... body))]{ +@defform*[((lambda (a : t) ... body) + (λ (a : t) ... body))]{ Defines a multi-arity procedure that supports automatic currying. @examples[#:eval curnel-eval ((lambda (x : Bool) (lambda (y : Bool) y)) true) - ((lambda* (x : Bool) (y : Bool) y) true) + ((lambda (x : Bool) (y : Bool) y) true) ] } @@ -65,20 +55,19 @@ Defines a multi-arity procedure that supports automatic currying. Defines multi-arity procedure application via automatic currying. @examples[#:eval curnel-eval - (data And : (->* Type Type Type) - (conj : (forall* (A : Type) (B : Type) - (->* A B ((And A) B))))) + (data And : (-> Type Type Type) + (conj : (-> (A : Type) (B : Type) A B ((And A) B)))) (conj Bool Bool true false)] } @defform*[((define name body) (define (name (x : t) ...) body))]{ -Like the @racket[define] provided by @racketmodname[cur/curnel/redex-lang], but supports -defining curried functions via @racket[lambda*]. +Like the @racket[define] provided by @racketmodname[cur], but supports +defining curried functions via @racket[lambda]. } @defform[(elim type motive-result-type e ...)]{ -Like the @racket[elim] provided by @racketmodname[cur/curnel/redex-lang], but supports +Like the @racket[elim] provided by @racketmodname[cur], but supports automatically curries the remaining arguments @racket[e ...]. @examples[#:eval curnel-eval @@ -90,12 +79,16 @@ automatically curries the remaining arguments @racket[e ...]. @defform*[((define-type name type) (define-type (name (a : t) ...) body))]{ -Like @racket[define], but uses @racket[forall*] instead of @racket[lambda*]. +Like @racket[define], but uses @racket[forall] instead of @racket[lambda]. } -@defform[(match e [pattern body] ...) +@defform[(match e [maybe-in] [maybe-return] [pattern body] ...) #:grammar - [(pattern + [(maybe-in + (code:line #:in type)) + (maybe-return + (code:line #:return type)) + (pattern constructor (code:line (constructor (x : t) ...)))]]{ A pattern-matcher-like syntax for inductive elimination. @@ -108,6 +101,9 @@ Generates a call to the inductive eliminator for @racket[e]. Currently does not work on inductive type-families as types indices are not inferred. +If @racket[#:in] is not specified, attempts to infer the type of @racket[e]. +If @racket[#:return] is not specified, attempts to infer the return type of the @racket[match]. + @examples[#:eval curnel-eval (match z [z true] @@ -116,42 +112,32 @@ are not inferred. @examples[#:eval curnel-eval (match (s z) + #:in Nat + #:return Bool [z true] [(s (n : Nat)) (not (recur n))])] + +@examples[#:eval curnel-eval + ((match (nil Bool) + #:in (List Bool) + [(nil (A : Type)) + (lambda (n : Nat) + (none A))] + [(cons (A : Type) (a : A) (rest : (List A))) + (lambda (n : Nat) + (match n + [z (some A a)] + [(s (n-1 : Nat)) + ((recur rest) n-1)]))]) + z)] + } @defform[(recur id)]{ -A form valid only in the body of a @racket[match] clause. Generates a -reference to the induction hypothesis for @racket[x]. -} - - -@defform[(case* type motive-result-type e (parameters ...) motive [pattern maybe-IH body] ...) - #:grammar - [(pattern - constructor - (code:line) - (code:line (constructor (x : t) ...))) - (maybe-IH - (code:line) - (code:line IH: ((x : t) ...)))]]{ -A pattern-matcher-like syntax for inductive elimination that does not try to infer the type or motive. -Necessary for more advanced types, like @racket[And], because @racket[case] is not very smart. - -@margin-note{Don't worry about all that output from requiring prop} -@examples[#:eval curnel-eval - (case* Nat Type z () (lambda (x : Nat) Bool) - [z true] - [(s (n : Nat)) - IH: ((_ : Bool)) - false]) - (require cur/stdlib/prop) - (case* And Type (conj Bool Nat true z) (Bool Nat) - (lambda* (A : Type) (B : Type) (ab : (And A B)) A) - [(conj (A : Type) (B : Type) (a : A) (b : B)) - IH: () - a])] +A form valid only in the body of a @racket[match] clause. +Generates a reference to the induction hypothesis for @racket[x] +inferred by a @racket[match] clause. } @defform[(let (clause ...) body) @@ -182,8 +168,9 @@ Check that expression @racket[e] has type @racket[type], causing a type-error if } @defform[(run syn)]{ -Like @racket[normalize/syn], but is a syntactic form which allows a Cur term to be written by -computing part of the term from another Cur term. +Like @racket[normalize/syn], but is a syntactic form to be used in surface syntax. +Allows a Cur term to be written by computing part of the term from +another Cur term. @examples[#:eval curnel-eval (lambda (x : (run (if true Bool Nat))) x)] diff --git a/cur-doc/cur/scribblings/stdlib/typeclass.scrbl b/cur-doc/cur/scribblings/stdlib/typeclass.scrbl index db1826a..e358494 100644 --- a/cur-doc/cur/scribblings/stdlib/typeclass.scrbl +++ b/cur-doc/cur/scribblings/stdlib/typeclass.scrbl @@ -21,7 +21,7 @@ are @racket[t ...]. @examples[#:eval curnel-eval (typeclass (Eqv (A : Type)) - (equal? : (forall* (a : A) (b : A) Bool)))] + (equal? : (forall (a : A) (b : A) Bool)))] } @defform[(impl (class param) defs ...)]{ diff --git a/cur-test/cur/tests/stdlib/maybe.rkt b/cur-test/cur/tests/stdlib/maybe.rkt index 5444667..fbf56e7 100644 --- a/cur-test/cur/tests/stdlib/maybe.rkt +++ b/cur-test/cur/tests/stdlib/maybe.rkt @@ -11,11 +11,10 @@ (some Bool true)) ;; Disabled until #22 fixed #;(check-equal? - (case Maybe Type (some Bool true) (Bool) - (lambda (A : Type) (x : (Maybe A)) A) - [(none (A : Type)) IH: () - false] - [(some (A : Type) (x : A)) IH: () - ;; TODO: Don't know how to use dependency yet - (if x true false)]) + (match (some Bool true) + [(none (A : Type)) + false] + [(some (A : Type) (x : A)) + ;; TODO: Don't know how to use dependency yet + (if x true false)]) true)