From bfc72d8fd36de39c6688a671a28733d8cbf019c7 Mon Sep 17 00:00:00 2001 From: "William J. Bowman" Date: Tue, 22 Sep 2015 18:18:26 -0400 Subject: [PATCH] Documented reflection features --- curnel/redex-lang.rkt | 1 + scribblings/cur.scrbl | 16 ++++-- scribblings/curnel.scrbl | 1 + scribblings/reflection.scrbl | 102 +++++++++++++++++++++++++++++++++++ 4 files changed, 116 insertions(+), 4 deletions(-) create mode 100644 scribblings/reflection.scrbl diff --git a/curnel/redex-lang.rkt b/curnel/redex-lang.rkt index 55584d4..1f03626 100644 --- a/curnel/redex-lang.rkt +++ b/curnel/redex-lang.rkt @@ -224,6 +224,7 @@ ;; TODO: Oops, run doesn't return a cur term but a redex term ;; wrapped in syntax bla. This is bad. +;; TODO: Should be provided by user-land code. (define-syntax (run syn) (syntax-case syn () [(_ expr) (normalize/syn #'expr)])) diff --git a/scribblings/cur.scrbl b/scribblings/cur.scrbl index dc0c42a..faa4682 100644 --- a/scribblings/cur.scrbl +++ b/scribblings/cur.scrbl @@ -10,10 +10,9 @@ The language @racketmodname[cur] is a dependently-typed language that arbitrary Racket meta-programs can manipulate. -The core language of @racketmodname[cur] is essentially TT@todo{citation -e.g. https://eb.host.cs.st-andrews.ac.uk/writings/thesis.pdf chapter 2}. +The core language of @racketmodname[cur] is essentially TT. The trusted core provides nothing beyond this language. -However, untrusted user-land code provides, via Racket meta-programming, features such as modules, top-level +However, untrusted code provides, via Racket meta-programming, features such as modules, top-level definitions, multi-arity functions, implicit partial application, syntax notations, a tactic DSL, interactive tactics, and a programming language meta-theory DSL. These features run at compile time and generate @tech{curnel forms}, forms in the core language, @@ -32,7 +31,16 @@ and evaluating @racketmodname[cur] forms at compile-time. Programmers can use these reflection feature with little fear, as the resulting @tech{curnel forms} will always be type-checked prior to running. +The @tech{curnel forms} are provided by the trusted core of the language. +The reflection forms and procedures are provided by mostly untrusted, but privileged, code. +These features require knowledge of and manipulation of the language implementation and could not be +implemented by a user via a library. +Everything else in @racketmodname[cur] is provided by untrusted user-land code---code that any user +(with sufficient meta-programming expertise) could write and ship as a library. + +@todo{Some repetition} + @local-table-of-contents[] @include-section{curnel.scrbl} -@;@include-section{reflection.scrbl} +@include-section{reflection.scrbl} diff --git a/scribblings/curnel.scrbl b/scribblings/curnel.scrbl index 53d9bc0..e5fa16d 100644 --- a/scribblings/curnel.scrbl +++ b/scribblings/curnel.scrbl @@ -130,3 +130,4 @@ Binds @racket[id] to the result of @racket[expr]. (sub1 (s z)) (sub1 z)] } +@todo{Document @racket[require] and @racket[provide]} diff --git a/scribblings/reflection.scrbl b/scribblings/reflection.scrbl new file mode 100644 index 0000000..810020d --- /dev/null +++ b/scribblings/reflection.scrbl @@ -0,0 +1,102 @@ +#lang scribble/manual + +@(require + "defs.rkt" + (for-label (only-in racket local-expand))) + +@title{Reflection} +To support the addition of new user-defined language features, @racketmodname[cur] provides access to +various parts of the language implementation as Racket forms at @gtech{phase} 1. +The reflection features are @emph{unstable} and may change without warning. +Many of these features are extremely hacky. + +@(require racket/sandbox scribble/eval) +@(define curnel-eval + (parameterize ([sandbox-output 'string] + [sandbox-error-output 'string] + [sandbox-eval-limits #f] + [sandbox-memory-limit #f]) + (make-module-evaluator "#lang cur (require cur/stdlib/bool) (require cur/stdlib/nat)"))) + +@defproc[(cur-expand [syn syntax?] [id identifier?] ...) + syntax?]{ +Expands the Cur term @racket[syn] until the expansion reaches a either @tech{Curnel form} or one of +the identifiers @racket[id]. See also @racket[local-expand]. + +@todo{Figure out how to get evaluator to pretend to be at phase 1 so these examples work properly.} + +@margin-note{The examples in this file do not currently run in the REPL, but should work if used at +phase 1 in Cur.} + +@examples[ +(eval:alts (define-syntax-rule (computed-type _) Type) (void)) +(eval:alts (cur-expand #'(lambda (x : (computed-type bla)) x)) + (eval:result @racket[#'(lambda (x : Type) x)] "" "")) +] +} + +@defproc[(type-infer/syn [syn syntax?]) + (or/c syntax? #f)]{ +Returns the type of the Cur term @racket[syn], or @racket[#f] if no type could be inferred. + +@examples[ +(eval:alts (type-infer/syn #'(lambda (x : Type) x)) + (eval:result @racket[#'(Π (x : (Unv 0)) (Unv 0))] "" "")) +(eval:alts (type-infer/syn #'Type) + (eval:result @racket[#'(Unv 1)] "" "")) +] +} + +@defproc[(type-check/syn? [syn syntax?]) + boolean?]{ +Returns @racket[#t] if the Cur term @racket[syn] is well-typed, or @racket[#f] otherwise. + +@examples[ +(eval:alts (type-infer/syn #'(lambda (x : Type) x)) + (eval:result @racket[#'(Π (x : (Unv 0)) (Unv 0))] "" "")) +(eval:alts (type-infer/syn #'Type) + (eval:result @racket[#'(Unv 1)] "" "")) +] +} + +@defproc[(normalize/syn [syn syntax?]) + syntax?]{ +Runs the Cur term @racket[syn] to a value. + +@examples[ +(eval:alts (normalize/syn #'((lambda (x : Type) x) Bool)) + (eval:result @racket[#'Bool] "" "")) +(eval:alts (normalize/syn #'(sub1 (s (s z)))) + (eval:result @racket[#'(s z)] "" "")) +] +} + + +@defform[(run syn)]{ +Like @racket[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. + +@margin-note{This one is a real working example, assuming the @racketmodname[cur/stdlib/bool] and +@racketmodname[cur/stdlib/nat] are loaded. Also, could be moved outside the privileged code.} + +@examples[#:eval curnel-eval + (lambda (x : (run (if btrue bool nat))) x)] + +} + +@defproc[(cur-equal? [e1 syntax?] [e2 syntax?]) + boolean?]{ +Returns @racket[#t] if the Cur terms @racket[e1] and @racket[e2] and equivalent according to +equal modulo α and β-equivalence. +@examples[ + + +(eval:alts (cur-equal? #'(lambda (a : Type) a) #'(lambda (b : Type) b)) + (eval:result @racket[#t] "" "")) +(eval:alts (cur-equal? #'((lambda (a : Type) a) Bool) #'Bool) + (eval:result @racket[#t] "" "")) +(eval:alts (cur-equal? #'(lambda (a : Type) (sub1 (s z))) #'(lambda (a : Type) z)) + (eval:result @racket[#f] "" "")) +] +} +