From 4f272dc5073100fc8e433d5f993e27db2cb98c10 Mon Sep 17 00:00:00 2001 From: "William J. Bowman" Date: Mon, 14 Mar 2016 17:20:58 -0400 Subject: [PATCH] NB XXX: Renamed reflection API functions The names of reflection API functions were previously confusing. They included weird patterns that only made sense inside the Cur implementation. As they are Racket functions, they ought to somehow indicate that these functions are for Cur, which they did not. --- cur-doc/cur/scribblings/reflection.scrbl | 26 ++++++++++---------- cur-doc/cur/scribblings/stdlib/sugar.scrbl | 4 ++-- cur-lib/cur/curnel/redex-lang.rkt | 16 ++++++------- cur-lib/cur/olly.rkt | 2 +- cur-lib/cur/stdlib/maybe.rkt | 2 +- cur-lib/cur/stdlib/prop.rkt | 4 ++-- cur-lib/cur/stdlib/sugar.rkt | 28 +++++++++++----------- cur-lib/cur/stdlib/tactics/base.rkt | 2 +- cur-lib/cur/stdlib/typeclass.rkt | 4 ++-- 9 files changed, 44 insertions(+), 44 deletions(-) diff --git a/cur-doc/cur/scribblings/reflection.scrbl b/cur-doc/cur/scribblings/reflection.scrbl index 1fae978..839c56d 100644 --- a/cur-doc/cur/scribblings/reflection.scrbl +++ b/cur-doc/cur/scribblings/reflection.scrbl @@ -30,52 +30,52 @@ phase 1 in Cur.} ] } -@defproc[(type-infer/syn [syn syntax?]) +@defproc[(cur-type-infer [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 #'(λ (x : Type) x)) +(eval:alts (cur-type-infer #'(λ (x : Type) x)) (eval:result @racket[#'(Π (x : (Type 0)) (Type 0))] "" "")) -(eval:alts (type-infer/syn #'Type) +(eval:alts (cur-type-infer #'Type) (eval:result @racket[#'(Type 1)] "" "")) ] } -@defproc[(type-check/syn? [syn syntax?]) +@defproc[(cur-type-check? [syn syntax?]) boolean?]{ Returns @racket[#t] if the Cur term @racket[syn] is well-typed, or @racket[#f] otherwise. @examples[ -(eval:alts (type-check/syn? #'(λ (x : Type) x)) +(eval:alts (cur-type-check? #'(λ (x : Type) x)) (eval:result @racket[#t] "" "")) -(eval:alts (type-check/syn? #'Type) +(eval:alts (cur-type-check? #'Type) (eval:result @racket[#t] "" "")) -(eval:alts (type-check/syn? #'x) +(eval:alts (cur-type-check? #'x) (eval:result @racket[#f] "" "")) ] } -@defproc[(normalize/syn [syn syntax?]) +@defproc[(cur-normalize [syn syntax?]) syntax?]{ Runs the Cur term @racket[syn] to a value. @examples[ -(eval:alts (normalize/syn #'((λ (x : Type) x) Bool)) +(eval:alts (cur-normalize #'((λ (x : Type) x) Bool)) (eval:result @racket[#'Bool] "" "")) -(eval:alts (normalize/syn #'(sub1 (s (s z)))) +(eval:alts (cur-normalize #'(sub1 (s (s z)))) (eval:result @racket[#'(s z)] "" "")) ] } -@defproc[(step/syn [syn syntax?]) +@defproc[(cur-step [syn syntax?]) syntax?]{ Runs the Cur term @racket[syn] for one step. @examples[ -(eval:alts (step/syn #'((λ (x : Type) x) Bool)) +(eval:alts (cur-step #'((λ (x : Type) x) Bool)) (eval:result @racket[#'Bool] "" "")) -(eval:alts (step/syn #'(sub1 (s (s z)))) +(eval:alts (cur-step #'(sub1 (s (s z)))) (eval:result @racket[#'(((((elim Nat (Type 0)) (λ (x2 : Nat) Nat)) z) (λ (x2 : Nat) (λ (ih-n2 : Nat) x2))) diff --git a/cur-doc/cur/scribblings/stdlib/sugar.scrbl b/cur-doc/cur/scribblings/stdlib/sugar.scrbl index 8ac3e75..e06c21a 100644 --- a/cur-doc/cur/scribblings/stdlib/sugar.scrbl +++ b/cur-doc/cur/scribblings/stdlib/sugar.scrbl @@ -169,7 +169,7 @@ Check that expression @racket[e] has type @racket[type], causing a type-error if } @defform[(run syn)]{ -Like @racket[normalize/syn], but is a syntactic form to be used in surface syntax. +Like @racket[cur-normalize], but is a syntactic form to be used in surface syntax. Allows a Cur term to be written by computing part of the term from another Cur term. @@ -179,7 +179,7 @@ another Cur term. } @defform[(step syn)]{ -Like @racket[run], but uses @racket[step/syn] to evaluate only one step and prints intermediate +Like @racket[run], but uses @racket[cur-step] to evaluate only one step and prints intermediate results before returning the result of evaluation. @examples[#:eval curnel-eval diff --git a/cur-lib/cur/curnel/redex-lang.rkt b/cur-lib/cur/curnel/redex-lang.rkt index ea67832..dddd82d 100644 --- a/cur-lib/cur/curnel/redex-lang.rkt +++ b/cur-lib/cur/curnel/redex-lang.rkt @@ -60,10 +60,10 @@ (all-from-out racket/syntax) cur->datum cur-expand - type-infer/syn - type-check/syn? - normalize/syn - step/syn + cur-type-infer + cur-type-check? + cur-normalize + cur-step cur-equal?)) (begin-for-syntax @@ -224,12 +224,12 @@ ;; Reflection tools - (define (normalize/syn syn) + (define (cur-normalize syn) (datum->cur syn (eval-cur syn))) - (define (step/syn syn) + (define (cur-step syn) (datum->cur syn (term (step ,(delta) ,(subst-bindings (cur->datum syn)))))) @@ -239,14 +239,14 @@ (and (judgment-holds (equivalent ,(delta) ,(eval-cur e1) ,(eval-cur e2))) #t)) ;; TODO: Document local-env - (define (type-infer/syn syn #:local-env [env '()]) + (define (cur-type-infer syn #:local-env [env '()]) (parameterize ([gamma (for/fold ([gamma (gamma)]) ([(x t) (in-dict env)]) (extend-Γ/syn (thunk gamma) x t))]) (let ([t (type-infer/term (eval-cur syn))]) (and t (datum->cur syn t))))) - (define (type-check/syn? syn type) + (define (cur-type-check? syn type) (type-check/term? (eval-cur syn) (eval-cur type))) ;; Takes a Cur term syn and an arbitrary number of identifiers ls. The cur term is diff --git a/cur-lib/cur/olly.rkt b/cur-lib/cur/olly.rkt index bb064c2..186df48 100644 --- a/cur-lib/cur/olly.rkt +++ b/cur-lib/cur/olly.rkt @@ -32,7 +32,7 @@ (coq-defns (format "~a~a~n" (coq-defns) str))) (define (constructor-args syn) - (syntax-parse (type-infer/syn syn) + (syntax-parse (cur-type-infer syn) #:datum-literals (Π :) [(Π (x:id : t) body) (cons #'x (constructor-args #'body))] diff --git a/cur-lib/cur/stdlib/maybe.rkt b/cur-lib/cur/stdlib/maybe.rkt index 6f70d48..9625d77 100644 --- a/cur-lib/cur/stdlib/maybe.rkt +++ b/cur-lib/cur/stdlib/maybe.rkt @@ -9,5 +9,5 @@ (define-syntax (some/i syn) (syntax-case syn () [(_ a) - (let ([a-ty (type-infer/syn #'a)]) + (let ([a-ty (cur-type-infer #'a)]) #`(some #,a-ty a))])) diff --git a/cur-lib/cur/stdlib/prop.rkt b/cur-lib/cur/stdlib/prop.rkt index d70b69f..3030ad7 100644 --- a/cur-lib/cur/stdlib/prop.rkt +++ b/cur-lib/cur/stdlib/prop.rkt @@ -31,8 +31,8 @@ (define-syntax (conj/i syn) (syntax-case syn () [(_ a b) - (let ([a-type (type-infer/syn #'a)] - [b-type (type-infer/syn #'b)]) + (let ([a-type (cur-type-infer #'a)] + [b-type (cur-type-infer #'b)]) #`(conj #,a-type #,b-type a b))])) (define thm:and-is-symmetric diff --git a/cur-lib/cur/stdlib/sugar.rkt b/cur-lib/cur/stdlib/sugar.rkt index dc42302..958362d 100644 --- a/cur-lib/cur/stdlib/sugar.rkt +++ b/cur-lib/cur/stdlib/sugar.rkt @@ -162,7 +162,7 @@ #:attr types ;; TODO: Detect failure, report error/suggestions (for/list ([e (attribute indices)]) - (or (type-infer/syn e) + (or (cur-type-infer e) (raise-syntax-error 'match (format @@ -183,7 +183,7 @@ (lambda (return) ;; NB: unhygenic ;; Normalize at compile-time, for efficiency at run-time - (normalize/syn + (cur-normalize #`((lambda ;; TODO: utteraly fragile; relines on the indices being referred to by name, not computed ;; works only for simple type familes and simply matches on them @@ -244,7 +244,7 @@ (define/syntax-parse type:inductive-type-declaration (cur-expand type-syn)) (let ([ih-name (quasisyntax/loc src #,(format-id name-syn "ih-~a" name-syn))] ;; Normalize at compile-time, for efficiency at run-time - [ih-type (normalize/syn #`(#,motive #,@(attribute type.indices) #,name-syn))]) + [ih-type (cur-normalize #`(#,motive #,@(attribute type.indices) #,name-syn))]) (dict-set! ih-dict (syntax->datum name-syn) ih-name) (append decls (list #`(#,ih-name : #,ih-type))))))) @@ -256,7 +256,7 @@ (or maybe-return-type ;; Ignore errors when trying to infer this type; other attempt might succeed (with-handlers ([values (lambda _ #f)]) - (type-infer/syn #:local-env (attribute p.local-env) #'b))))) + (cur-type-infer #:local-env (attribute p.local-env) #'b))))) (define-syntax-class (match-clause D motive) (pattern @@ -292,7 +292,7 @@ (~optional (~seq #:in ~! t) #:defaults - ([t (or (type-infer/syn #'d) + ([t (or (cur-type-infer #'d) (raise-syntax-error 'match "Could not infer discrimnant's type. Try using #:in to declare it." @@ -318,7 +318,7 @@ (elim D.inductive-name #,(or - (type-infer/syn (attribute return-type)) + (cur-type-infer (attribute return-type)) (raise-syntax-error 'match "Could not infer type of motive. Sorry, you'll have to use elim." @@ -337,14 +337,14 @@ #:attr type (cond [(attribute t) ;; TODO: Code duplication in :: - (unless (type-check/syn? #'e #'t) + (unless (cur-type-check? #'e #'t) (raise-syntax-error 'let (format "Term ~a does not have expected type ~a. Inferred type was ~a" - (cur->datum #'e) (cur->datum #'t) (cur->datum (type-infer/syn #'e))) + (cur->datum #'e) (cur->datum #'t) (cur->datum (cur-type-infer #'e))) #'e (quasisyntax/loc #'x (x e)))) #'t] - [(type-infer/syn #'e)] + [(cur-type-infer #'e)] [else (raise-syntax-error 'let @@ -362,22 +362,22 @@ [(_ pf t) (begin ;; TODO: Code duplication in let-clause pattern - (unless (type-check/syn? #'pf #'t) + (unless (cur-type-check? #'pf #'t) (raise-syntax-error ':: (format "Term ~a does not have expected type ~a. Inferred type was ~a" - (cur->datum #'pf) (cur->datum #'t) (cur->datum (type-infer/syn #'pf))) + (cur->datum #'pf) (cur->datum #'t) (cur->datum (cur-type-infer #'pf))) syn)) #'(void))])) (define-syntax (run syn) (syntax-case syn () - [(_ expr) (normalize/syn #'expr)])) + [(_ expr) (cur-normalize #'expr)])) (define-syntax (step syn) (syntax-case syn () [(_ expr) - (let ([t (step/syn #'expr)]) + (let ([t (cur-step #'expr)]) (displayln (cur->datum t)) t)])) @@ -393,6 +393,6 @@ (syntax-case syn () [(_ term) (begin - (printf "\"~a\" has type \"~a\"~n" (syntax->datum #'term) (syntax->datum (type-infer/syn #'term))) + (printf "\"~a\" has type \"~a\"~n" (syntax->datum #'term) (syntax->datum (cur-type-infer #'term))) ;; Void is undocumented and a hack, but sort of works #'(void))])) diff --git a/cur-lib/cur/stdlib/tactics/base.rkt b/cur-lib/cur/stdlib/tactics/base.rkt index c504222..ce2ef26 100644 --- a/cur-lib/cur/stdlib/tactics/base.rkt +++ b/cur-lib/cur/stdlib/tactics/base.rkt @@ -220,7 +220,7 @@ [pf (proof-state-proof ps)]) (unless (proof-state-proof-complete? ps) (raise-syntax-error 'qed "Proof contains holes" (pf (current-hole-pretty-symbol)))) - (unless (type-check/syn? pf t) + (unless (cur-type-check? pf t) (raise-syntax-error 'qed "Invalid proof" pf t)) pf))) diff --git a/cur-lib/cur/stdlib/typeclass.rkt b/cur-lib/cur/stdlib/typeclass.rkt index 3c26dc3..dc24209 100644 --- a/cur-lib/cur/stdlib/typeclass.rkt +++ b/cur-lib/cur/stdlib/typeclass.rkt @@ -38,7 +38,7 @@ #`(define-syntax (#,name syn) (syntax-case syn () [(_ arg args (... ...)) - #`(#,(format-id syn "~a-~a" '#,name (type-infer/syn #'arg)) + #`(#,(format-id syn "~a-~a" '#,name (cur-type-infer #'arg)) arg args (... ...))]))))])) @@ -57,7 +57,7 @@ #`(begin #,@(for/list ([def (syntax->list #'(defs ...))]) (let-values ([(name body) (process-def def)]) - (unless (type-check/syn? + (unless (cur-type-check? body #`(#,(dict-ref (dict-ref typeclasses (syntax->datum #'class))