6.2.901.900
3.2 Sugar
The curnel forms are sort of terrible for actually writing code. Functions and applications are
limited to single artity. Functions type must be specified using the dependent forall, even
when the dependency is not used. Inductive elimination can only be done via the primitive eliminator
and not via pattern matching. However, with the full force of Racket’s syntactic extension system, we
can define not only simply notation, but redefine what application means, or define a pattern matcher
that expands into the eliminator.
This library defines various syntactic extensions making Cur easier to write than writing raw TT.
A non-dependent function type Equivalent to (forall (_ : t1) t2), where _ indicates an variable that is not used.
Examples: |
| > (data And : (-> Type (-> Type Type)) | | (conj : (forall (A : Type) (forall (B : Type) (-> A (-> B ((And A) B))))))) |
| | > ((((conj Bool) Bool) true) false) | '((((conj Bool) Bool) true) false) |
|
A non-dependent multi-arity function type that supports automatic currying.
Examples: |
| > (data And : (->* Type Type Type) | | (conj : (forall (A : Type) (forall (B : Type) (->* A B ((And A) B)))))) |
| | > ((((conj Bool) Bool) true) false) | '((((conj Bool) Bool) true) false) |
|
(forall* (a : t) ... type)
|
| (∀* (a : t) ... type) |
A multi-arity function type that supports automatic currying.
Examples: |
| > (data And : (->* Type Type Type) | | (conj : (forall* (A : Type) (B : Type) | | (->* A B ((And A) B))))) |
| | > ((((conj Bool) Bool) true) false) | '((((conj Bool) Bool) true) false) |
|
(lambda* (a : t) ... body)
|
| (λ* (a : t) ... body) |
Defines a multi-arity procedure that supports automatic currying.
Examples: |
| > ((lambda (x : Bool) (lambda (y : Bool) y)) true) | '(λ (y1 : Bool) y1) | | > ((lambda* (x : Bool) (y : Bool) y) true) | '(λ (y1 : Bool) y1) |
|
Defines multi-arity procedure application via automatic currying.
Examples: |
| > (data And : (->* Type Type Type) | | (conj : (forall* (A : Type) (B : Type) | | (->* A B ((And A) B))))) |
| | > (conj Bool Bool true false) | '((((conj Bool) Bool) true) false) |
|
(define name body)
|
| (define (name (x : t) ...) body) |
Like the define provided by cur/curnel/redex-lang, but supports
defining curried functions via lambda*.
(elim type motive-result-type e ...)
|
Like the elim provided by cur/curnel/redex-lang, but supports
automatically curries the remaining arguments e ....
Examples: |
| > (require cur/stdlib/bool) | | > (elim Bool Type (lambda (x : Bool) Bool) | | false | | true | | true) |
| 'false |
|
(define-type name type)
|
| (define-type (name (a : t) ...) body) |
Like define, but uses forall* instead of lambda*.
(case e [pattern maybe-IH body] ...)
|
| |
| pattern | | = | | constructor | | | | | | | | | | | | | | (constructor (x : t) ...) | | | | | | | | maybe-IH | | = | | | | | | | | | IH: ((x : t) ...) |
|
A pattern-matcher-like syntax for inductive elimination. Actually does not do pattern matching and
relies on the constructors patterns being specified in the same order as when the inductive type was
defined.
Examples: |
| > (require cur/stdlib/nat) | | > (case z | | [z true] | | [(s (n : Nat)) | | IH: ((_ : Bool)) | | false]) |
| 'true |
|
(case* type motive-result-type e (parameters ...) motive [pattern maybe-IH body] ...)
|
| |
| pattern | | = | | constructor | | | | | | | | | | | | | | (constructor (x : t) ...) | | | | | | | | maybe-IH | | = | | | | | | | | | 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 And, because case is not very smart.
Don’t worry about all that output from requiring prop
Examples: |
| > (require cur/stdlib/nat) | | > (case* Nat Type z () (lambda (x : Nat) Bool) | | [z true] | | [(s (n : Nat)) | | IH: ((_ : Bool)) | | false]) |
| 'true | | > (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]) |
| 'true |
|
(let (clause ...) body)
|
| |
| clause | | = | | (id expr) | | | | | | | ((id : type) expr) |
|
Evaluates the expressions expr from each clause, left to right, and binds them to each
id. If a type is not given for the id, attempts to infer the type of the
corresponding expr, raising a syntax error if no type can be inferred.
Examples: |
| > (let ([x Type] | | [y (λ (x : (Type 1)) x)]) | | (y x)) |
| '(Unv 0) | | > (let ([x uninferrable-expr] | | [y (λ (x : (Type 1)) x)]) | | (y x)) |
| eval:20:0: cur: term is ill-typed: | at: uninferrable-expr | in: uninferrable-expr |
|
Check that expression e has type type, causing a type-error if not, and producing
(void) if so.
Examples: |
| > (:: z Nat) | | > (:: true Nat) | eval:22:0: ::: Term true does not have expected type Nat. | Inferred type was Bool | in: (:: true Nat) |
|
Like 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.
Example: |
| > (lambda (x : (run (if true Bool Nat))) x) | '(λ (x1 : Bool) x1) |
|
Like run, but uses step/syn to evaluate only one step and prints intermediate
results before returning the result of evaluation.
Example: |
| > (step (plus z z)) | ((λ (n2 : Nat) (((((elim Nat (Unv 0)) (λ (x1 : Nat) Nat)) n2) (λ (x1 : Nat) (λ (ih-n1 : Nat) (s ih-n1)))) z)) z) | 'z |
|
Like step, but expands to natural calls to step.
Example: |
| > (step-n 3 (plus z z)) | ((λ (n2 : Nat) (((((elim Nat (Unv 0)) (λ (x1 : Nat) Nat)) n2) (λ (x1 : Nat) (λ (ih-n1 : Nat) (s ih-n1)))) z)) z) | (((((elim Nat (Unv 0)) (λ (x1 : Nat) Nat)) z) (λ (x1 : Nat) (λ (ih-n1 : Nat) (s ih-n1)))) z) | z |
| 'z |
|
Print the type of expr, at compile-time. Similar to Coq’s Check.
Example: |
| > (query-type Bool) | "Bool" has type "(Type 0)" |
|