suzanne.soy/cur
1
0
Fork 0
Code Issues Pull Requests Actions Packages Projects Releases Wiki Activity

NB XXX: Renamed reflection API functions

Browse Source 
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.
This commit is contained in:
William J. Bowman 2016-03-14 17:20:58 -04:00
parent 8b3159bb6f
commit 4f272dc507
No known key found for this signature in database
GPG Key ID: DDD48D26958F0D1A
9 changed files with 44 additions and 44 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

26
cur-doc/cur/scribblings/reflection.scrbl
View File

@ -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)))

4
cur-doc/cur/scribblings/stdlib/sugar.scrbl
View File

@ -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

16
cur-lib/cur/curnel/redex-lang.rkt
View File

@ -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

2
cur-lib/cur/olly.rkt
View File

@ -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))]

2
cur-lib/cur/stdlib/maybe.rkt
View File

@ -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))]))

4
cur-lib/cur/stdlib/prop.rkt
View File

@ -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

28
cur-lib/cur/stdlib/sugar.rkt
View File

@ -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))]))

2
cur-lib/cur/stdlib/tactics/base.rkt
View File

@ -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)))

4
cur-lib/cur/stdlib/typeclass.rkt
View File

@ -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))