▼Cur
On this page:
cur-type-infer
cur-type-check?
cur-reflect-id
cur-rename
cur-normalize
cur-step
cur-equal?
cur->datum
cur-constructors-for
cur-data-parameters
cur-constructor-telescope-length
cur-constructor-recursive-index-ls
8.12
  top  contents    up   

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.

The reflection API enforces type safety; all terms are first expanded, then type checked, then reduced; individual API function may not complete this route—e.g, cur-expand stops after expansion—but no API functions will reduce before type checking, or type check before expansion.

Because these functions must be used during the dynamic extent of a syntax transformer application by the expander (see local-expand), the examples in this file do not currently run in the REPL, so these examples may contain typos.

Changed in version 0.20 of package cur-lib: Removed declare-data!, call-local-data-scope, local-data-scope—we can’t implement these in the new Curnel, and they were hacks to begin with.

procedure

(cur-type-infer syn [#:local-env env]) → (or/c syntax? #f)

  syn : syntax?
  env : (listof (cons/c syntax? syntax?)) = '()
Returns the type of the Cur term syn, or #f if no type could be inferred.

If #:local-env is specified, infers types under an extended lexical environment via with-env.

Examples:
> (cur-type-infer #'(λ (x : Type) x))

#'(Π (x : (Type 0)) (Type 0))

> (cur-type-infer #'Type)

#'(Type 1)

> (cur-type-infer #'X #:local-env '((#'X . #'(Type 0))))

#'(Type 0)

> (define-syntax-rule (cur-type-infer& t) (cur-type-infer t))
> #`(λ (X : (Type 0)) (cur-type-infer& X))

#`(λ (X : (Type 0)) (cur-type-infer& X))

NOTE: This #:local-env keyword argument is deprecated; use a macro to delay the function call until the binder is expanded. See cur-type-infer for an example., instead.

procedure

(cur-type-check? term type [#:local-env env]) → boolean?

  term : syntax?
  type : syntax?
  env : (listof (cons/c syntax? syntax?)) = '()
Returns #t if the Cur term term is well-typed with a subtype of type, or #f otherwise.

If #:local-env is specified, checks the type under an extended lexical environment via with-env.

Examples:
> (cur-type-check? #'(λ (x : Type) x) #'(Π (x : (Type 1)) Type))

#t

> (cur-type-check? #'Type #'(Type 1))

#t

> (cur-type-check? #'x #'Nat)

#f

> (cur-type-check? #'x #'Nat #:local-env `((#'x . #'Nat)))

#t

NOTE: This #:local-env keyword argument is deprecated; use a macro to delay the function call until the binder is expanded. See cur-type-infer for an example., instead.

procedure

(cur-reflect-id id) → identifier?

  id : identifier?
Return the original name of id for identifiers that have been renamed during expansion or type-checking, if one exists.

Added in version 0.20 of package cur-lib.

procedure

(cur-rename new old term) → syntax?

  new : identifier?
  old : identifier?
  term : syntax?
Replace old by new in term, without evaluating or expanding term. While cur-normalize can be used to substitute into a term, cur-rename can be useful when you want to keep a term in the surface syntax.

Example:
> (cur-rename #'Y #'X #'((λ (X : (Type 0)) X) X))

#<syntax:eval:1:0 ((λ (X : (Type 0)) X) Y)>

Added in version 0.20 of package cur-lib.

procedure

(cur-normalize syn [#:local-env env]) → syntax?

  syn : syntax?
  env : (listof (cons/c syntax? syntax?)) = '()
Runs the Cur term syn to a value.

If #:local-env is specified, runs under an extended lexical environment via with-env.

Examples:
> (cur-normalize #'((λ (x : Type) x) Bool))

#'Bool

> (cur-normalize #'(sub1 (s (s z))))

#'(s z)

NOTE: This #:local-env keyword argument is deprecated; use a macro to delay the function call until the binder is expanded. See cur-type-infer for an example., instead.

procedure

(cur-step syn [#:local-env env]) → syntax?

  syn : syntax?
  env : (listof (cons/c syntax? syntax?)) = '()
Runs the Cur term syn for one step.

If #:local-env is specified, runs under an extended lexical environment via with-env.

Examples:
> (cur-step #'((λ (x : Type) x) Bool))

#'Bool

> (cur-step #'(sub1 (s (s z))))

#'(elim Nat (λ (x2 : Nat) Nat) (z (λ (x2 : Nat) (λ (ih-n2 : Nat) x2))) (s (s z)))

NOTE: This #:local-env keyword argument is deprecated; use a macro to delay the function call until the binder is expanded. See cur-type-infer for an example., instead.

procedure

(cur-equal? e1 e2 [#:local-env env]) → boolean?

  e1 : syntax?
  e2 : syntax?
  env : (listof (cons/c syntax? syntax?)) = '()
Returns #t if the Cur terms e1 and e2 and equivalent according to equal modulo α and β-equivalence.

If #:local-env is specified, runs under an extended lexical environment via with-env.

Examples:
> (cur-equal? #'(λ (a : (Type 0)) a) #'(λ (b : Type) b))

#t

> (cur-equal? #'((λ (a : (Type 0)) a) Bool) #'Bool)

#t

> (cur-equal? #'(λ (a : (Type 0)) (sub1 (s z))) #'(λ (a : (Type 0)) z))

#f

NOTE: This #:local-env keyword argument is deprecated; use a macro to delay the function call until the binder is expanded. See cur-type-infer for an example., instead.

procedure

(cur->datum s [#:local-env env]) → (or/c symbol? list?)

  s : syntax?
  env : (listof (cons/c syntax? syntax?)) = '()
Converts s to a datum representation of the curnel form, after expansion.

If #:local-env is specified, runs under an extended lexical environment via with-env.

Example:
> (cur->datum #'(λ (a : (Type 0)) a))

'(λ (a : (Type 0)) a)

NOTE: This #:local-env keyword argument is deprecated; use a macro to delay the function call until the binder is expanded. See cur-type-infer for an example., instead.

procedure

(cur-constructors-for D) → (listof identifier?)

  D : identifier?
Returns a list of constructors for the inductively defined type D.

Example:
> (cur-constructors-for #'Nat)

'(#'z  #'s)

procedure

(cur-data-parameters D) → natural-number/c

  D : identifier?
Return the number of invariant parameters for the inductively defined type D.

Examples:
> (cur-data-parameters #'Nat)

0

> (cur-data-parameters #'List)

1

procedure

(cur-constructor-telescope-length c) → natural-number/c

  c : identifier?
Return the number of arguments to the constructor c.

Examples:
> (cur-constructor-telescope-length #'z)

0

> (cur-constructor-telescope-length #'s)

1

> (cur-constructor-telescope-length #'cons)

3

procedure

(cur-constructor-recursive-index-ls c)

 → (listof natural-number/c)
  c : identifier?
Return a 0-indexed list of the positions of the recursive arguments of constructor c.

Examples:
> (cur-constructor-recursive-index-ls #'z)

'()

> (cur-constructor-recursive-index-ls #'s)

'(0)

> (cur-constructor-recursive-index-ls #'cons)

'(2)

  top  contents    up