▼Cur
On this page:
call-with-env
with-env
cur-expand
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-method-type
cur-constructor-telescope-length
cur-constructor-recursive-index-ls
7.7
  top  ← prev  up  next → 

2 Reflection

 (require cur) package: cur-lib
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

(call-with-env env thunk) → any

  env : (listof (cons/c syntax? syntax?))
  thunk : (-> any)
Calls thunk with the lexical environment extended by env. env should be in reverse dependency order; the 0th element of

env may depend on the 1st, the 1st may depend on the 2nd, etc.

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

syntax

(with-env env e)

Syntax that expands to (call-with-env env (thunk e)).

NOTE: This function 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-expand syn [#:local-env env] id ...) → syntax?

  syn : syntax?
  env : (listof (cons/c syntax? 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.

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

TODO: Figure out how to get evaluator to pretend to be at phase 1 so these examples work properly.

Examples:
> (define-syntax-rule (computed-type _) Type)
> (cur-expand #'(λ (x : (computed-type bla)) x))

#'(λ (x : Type) 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-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-method-type target motive) → syntax?

  target : syntax?
  motive : syntax?
Given an a target (a constructor for some type D applied to its invariant parameters) and a motive for eliminating it, return the type of the method required for this constructor when eliminating D.

Examples:
> (cur-method-type #'s #'(lambda (x : Nat) Nat))

#'Nat

> (cur-method-type #'s #'(lambda (x : Nat) Nat))

#'(Π (x : Nat) (Π (ih : Nat) Nat))

> (cur-method-type #'(nil Nat) #'(lambda (x : (List Nat)) Nat))

#'Nat

> (cur-method-type #'(cons Nat) #'(lambda (x : (List Nat)) Nat))

#'(Π (a : Nat) (Π (rest : (List Nat)) (Π (ih : Nat) Nat)))

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  ← prev  up  next →