suzanne.soy/cur
1
0
Fork 0
Code Issues Pull Requests Actions Packages Projects Releases Wiki Activity

Updated documentation

Browse Source
This commit is contained in:
William J. Bowman 2016-01-18 14:03:42 -05:00
parent c3f5719b30
commit ed57d034dc
No known key found for this signature in database
GPG Key ID: DDD48D26958F0D1A
4 changed files with 63 additions and 77 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
cur-doc/cur/scribblings/stdlib/list.scrbl
View File

@ -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.
}

123
cur-doc/cur/scribblings/stdlib/sugar.scrbl
View File

@ -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)]

2
cur-doc/cur/scribblings/stdlib/typeclass.scrbl
View File

@ -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 ...)]{

13
cur-test/cur/tests/stdlib/maybe.rkt
View File

@ -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)