6.2.901.900
2 Reflection
To support the addition of new user-defined language features, cur provides access to
various parts of the language implementation as Racket forms at phase 1.
The reflection features are unstable and may change without warning.
Many of these features are extremely hacky.
(cur-expand syn id ...) → syntax?
|
| syn : syntax? |
| id : identifier? |
Expands the Cur term
syn until the expansion reaches a either
Curnel form or one of
the identifiers
id. See also
local-expand.
TODO: Figure out how to get evaluator to pretend to be at phase 1 so these examples work properly.
The examples in this file do not currently run in the REPL, but should work if used at
phase 1 in Cur.
Examples: |
| > (define-syntax-rule (computed-type _) Type) | | | > (cur-expand #'(lambda (x : (computed-type bla)) x)) | #'(lambda (x : Type) x) |
|
(type-infer/syn syn) → (or/c syntax? #f)
|
| syn : syntax? |
Returns the type of the Cur term syn, or #f if no type could be inferred.
Examples: |
| > (type-infer/syn #'(lambda (x : Type) x)) | #'(forall (x : (Type 0)) (Type 0)) | | > (type-infer/syn #'Type) | #'(Type 1) |
|
(type-check/syn? syn) → boolean?
|
| syn : syntax? |
Returns #t if the Cur term syn is well-typed, or #f otherwise.
Examples: |
| > (type-check/syn? #'(lambda (x : Type) x)) | #t | | > (type-check/syn? #'Type) | #t | | > (type-check/syn? #'x) | #f |
|
(normalize/syn syn) → syntax?
|
| syn : syntax? |
Runs the Cur term syn to a value.
Examples: |
| > (normalize/syn #'((lambda (x : Type) x) Bool)) | #'Bool | | > (normalize/syn #'(sub1 (s (s z)))) | #'(s z) |
|
(step/syn syn) → syntax?
|
| syn : syntax? |
Runs the Cur term syn for one step.
Examples: |
| > (step/syn #'((lambda (x : Type) x) Bool)) | #'Bool | | > (step/syn #'(sub1 (s (s z)))) | #'(((((elim Nat (Type 0)) (lambda (x2 : Nat) Nat)) z) (lambda (x2 : Nat) (lambda (ih-n2 : Nat) x2))) (s (s z))) |
|
(cur-equal? e1 e2) → boolean?
|
| e1 : syntax? |
| e2 : syntax? |
Returns #t if the Cur terms e1 and e2 and equivalent according to
equal modulo α and β-equivalence.
Examples: |
| > (cur-equal? #'(lambda (a : Type) a) #'(lambda (b : Type) b)) | #t | | > (cur-equal? #'((lambda (a : Type) a) Bool) #'Bool) | #t | | > (cur-equal? #'(lambda (a : Type) (sub1 (s z))) #'(lambda (a : Type) z)) | #f |
|
(cur->datum s) → (or/c symbol? list?)
|
| s : syntax? |
Converts
s to a datum representation of the
curnel form, after expansion.
Example: |
| > (cur-?datum #'(lambda (a : Type) a)) | '(λ (a : (Unv 0) a)) |
|