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

Updated documentation and examples to new elim

Browse Source
This commit is contained in:
William J. Bowman 2015-09-25 17:50:03 -04:00
parent de3a4d9cf3
commit b64d20319f
No known key found for this signature in database
GPG Key ID: DDD48D26958F0D1A
4 changed files with 26 additions and 16 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
examples/stlc.rkt
View File

@ -23,7 +23,7 @@
(extend-gamma : (->* Gamma Var stlc-type Gamma)))
(define (lookup-gamma (g : Gamma) (x : Var))
(case* Gamma g (lambda* (g : Gamma) (Maybe stlc-type))
(case* Gamma Type g () (lambda* (g : Gamma) (Maybe stlc-type))
[emp-gamma (none stlc-type)]
[(extend-gamma (g1 : Gamma) (v1 : Var) (t1 : stlc-type))
IH: ((ih-g1 : (Maybe stlc-type)))

4
oll.rkt
View File

@ -239,9 +239,9 @@
(data Var : Type (avar : (-> Nat Var)))
(define (var-equal? (v1 : Var) (v2 : Var))
(case* Var v1 (lambda (v : Var) Bool)
(case* Var Type v1 () (lambda (v : Var) Bool)
[(avar (n1 : Nat)) IH: ()
(case* Var v2 (lambda (v : Var) Bool)
(case* Var Type v2 () (lambda (v : Var) Bool)
[(avar (n2 : Nat)) IH: ()
(nat-equal? n1 n2)])]))
(module+ test

23
scribblings/curnel.scrbl
View File

@ -96,10 +96,11 @@ For instance, Cur does not currently perform strict positivity checking.
((((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*].
@defform[(elim type motive-result-type)]{
Returns the inductive eliminator for @racket[type] where the result type of the motive is
@racket[motive-result-type]. The eliminator expects a motive, methods for each of the constructors of the
inductive type @racket[type], parameters @racket[p ...] for the inductive @racket[type], and finally a
type of @racket[(type p ...)].
The following example runs @racket[(sub1 (s z))].
@ -107,9 +108,11 @@ The following example runs @racket[(sub1 (s z))].
(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)))]
(((((elim Nat Type)
(lambda (x : Nat) Nat))
z)
(lambda (n : Nat) (lambda (IH : Nat) n)))
(s z))]
}
@defform[(define id expr)]{
@ -120,9 +123,9 @@ Binds @racket[id] to the result of @racket[expr].
(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)))))
(((((elim Nat Type) (lambda (x : Nat) Nat))
z)
(lambda (n : Nat) (lambda (IH : Nat) n))) n)))
(sub1 (s (s z)))
(sub1 (s z))
(sub1 z)]

13
scribblings/stdlib/sugar.scrbl
View File

@ -105,7 +105,7 @@ defined.
false])]
}
@defform[(case* type e motive [pattern maybe-IH body] ...)
@defform[(case* type motive-result-type e (parameters ...) motive [pattern maybe-IH body] ...)
#:grammar
[(pattern
constructor
@ -117,13 +117,20 @@ defined.
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
(require cur/stdlib/nat)
(case* Nat z (lambda (x : Bool) Nat)
(case* Nat Type z () (lambda (x : Nat) Bool)
[z true]
[(s (n : Nat))
IH: ((_ : Bool))
false])]
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])]
}
@defform[(run syn)]{