brought back syntax locations (for better error messages) in redex main forms and improved define-relation
svn: r15214
This commit is contained in:
Robby Findler
parent
ed4f066bb6
commit
f9ba83cc1c
|
|
@ -26,15 +26,19 @@
|
|||
(identifier-prune-lexical-context #'whatever '(#%app #%datum))
|
||||
(let loop ([stx stx])
|
||||
(syntax-case stx (quote)
|
||||
[(quote x) (list (quote-syntax/prune quote)
|
||||
(syntax->datum #'x))]
|
||||
[(a . b) (cons (loop #'a) (loop #'b))]
|
||||
[(quote x)
|
||||
(list (quote-syntax/prune quote)
|
||||
(syntax->datum #'x))]
|
||||
[(a . b)
|
||||
(datum->syntax (identifier-prune-lexical-context #'whatever '(#%app))
|
||||
(cons (loop #'a) (loop #'b))
|
||||
stx)]
|
||||
[x
|
||||
(identifier? #'x)
|
||||
(datum->syntax (identifier-prune-lexical-context #'x)
|
||||
(syntax-e #'x))]
|
||||
[() '()]
|
||||
[_ (syntax->datum stx)]))))
|
||||
(identifier-prune-lexical-context #'x)]
|
||||
[() (datum->syntax #f '() stx)]
|
||||
[_ (datum->syntax (identifier-prune-lexical-context #'whatever '(#%datum))
|
||||
(syntax->datum stx) stx)]))))
|
||||
|
||||
(define-syntax (term-match/single stx)
|
||||
(syntax-case stx ()
|
||||
|
|
@ -1005,21 +1009,26 @@
|
|||
(define (internal-define-metafunction orig-stx prev-metafunction stx relation?)
|
||||
(syntax-case stx ()
|
||||
[(lang . rest)
|
||||
(let ([syn-error-name (if prev-metafunction
|
||||
'define-metafunction/extension
|
||||
'define-metafunction)])
|
||||
(let ([syn-error-name (if relation?
|
||||
'define-relation
|
||||
(if prev-metafunction
|
||||
'define-metafunction/extension
|
||||
'define-metafunction))])
|
||||
(unless (identifier? #'lang)
|
||||
(raise-syntax-error syn-error-name "expected an identifier in the language position" orig-stx #'lang))
|
||||
(when (null? (syntax-e #'rest))
|
||||
(raise-syntax-error syn-error-name "no clauses" orig-stx))
|
||||
(prune-syntax
|
||||
(let-values ([(contract-name dom-ctcs codom-contract pats)
|
||||
(split-out-contract orig-stx syn-error-name #'rest)])
|
||||
(with-syntax ([(((original-names lhs-clauses ...) rhs stuff ...) ...) pats]
|
||||
(split-out-contract orig-stx syn-error-name #'rest relation?)])
|
||||
(with-syntax ([(((original-names lhs-clauses ...) raw-rhses ...) ...) pats]
|
||||
[(lhs-for-lw ...)
|
||||
(with-syntax ([((lhs-for-lw _ _ ...) ...) pats])
|
||||
(with-syntax ([((lhs-for-lw _ ...) ...) pats])
|
||||
(map (λ (x) (to-lw/proc (datum->syntax #f (cdr (syntax-e x)) x)))
|
||||
(syntax->list #'(lhs-for-lw ...))))])
|
||||
(with-syntax ([((rhs stuff ...) ...) (if relation?
|
||||
#'((,(and (term raw-rhses) ...)) ...)
|
||||
#'((raw-rhses ...) ...))])
|
||||
(parameterize ([is-term-fn?
|
||||
(let ([names (syntax->list #'(original-names ...))])
|
||||
(λ (x) (and (not (null? names))
|
||||
|
|
@ -1057,7 +1066,7 @@
|
|||
(with-syntax ([(side-conditions-rewritten ...)
|
||||
(map (λ (x) (rewrite-side-conditions/check-errs
|
||||
lang-nts
|
||||
'define-metafunction
|
||||
syn-error-name
|
||||
#t
|
||||
x))
|
||||
(syntax->list (syntax ((side-condition lhs tl-withs) ...))))]
|
||||
|
|
@ -1065,18 +1074,19 @@
|
|||
(and dom-ctcs
|
||||
(rewrite-side-conditions/check-errs
|
||||
lang-nts
|
||||
'define-metafunction
|
||||
syn-error-name
|
||||
#f
|
||||
dom-ctcs))]
|
||||
[codom-side-conditions-rewritten
|
||||
(rewrite-side-conditions/check-errs
|
||||
lang-nts
|
||||
'define-metafunction
|
||||
syn-error-name
|
||||
#f
|
||||
codom-contract)]
|
||||
[(rhs-fns ...)
|
||||
(map (λ (lhs rhs bindings)
|
||||
(let-values ([(names names/ellipses) (extract-names lang-nts 'define-metafunction #t lhs)])
|
||||
(let-values ([(names names/ellipses)
|
||||
(extract-names lang-nts syn-error-name #t lhs)])
|
||||
(with-syntax ([(names ...) names]
|
||||
[(names/ellipses ...) names/ellipses]
|
||||
[rhs rhs]
|
||||
|
|
@ -1150,7 +1160,7 @@
|
|||
#,relation?)))
|
||||
(term-define-fn name name2))
|
||||
'disappeared-use
|
||||
(map syntax-local-introduce (syntax->list #'(original-names ...))))))))))))))]
|
||||
(map syntax-local-introduce (syntax->list #'(original-names ...)))))))))))))))]
|
||||
[(_ prev-metafunction name lang clauses ...)
|
||||
(begin
|
||||
(unless (identifier? #'name)
|
||||
|
|
@ -1166,11 +1176,11 @@
|
|||
(syntax->list (syntax (clauses ...))))
|
||||
(raise-syntax-error 'define-metafunction "missing error check for bad syntax" stx))]))
|
||||
|
||||
(define (split-out-contract stx syn-error-name rest)
|
||||
(define (split-out-contract stx syn-error-name rest relation?)
|
||||
;; initial test determines if a contract is specified or not
|
||||
(cond
|
||||
[(pair? (syntax-e (car (syntax->list rest))))
|
||||
(values #f #f #'any (check-clauses stx syn-error-name rest))]
|
||||
(values #f #f #'any (check-clauses stx syn-error-name rest relation?))]
|
||||
[else
|
||||
(syntax-case rest ()
|
||||
[(id colon more ...)
|
||||
|
|
@ -1187,7 +1197,7 @@
|
|||
(raise-syntax-error syn-error-name "expected a range contract to follow the arrow" stx (car more)))
|
||||
(let ([doms (reverse dom-pats)]
|
||||
[codomain (cadr more)]
|
||||
[clauses (check-clauses stx syn-error-name (cddr more))])
|
||||
[clauses (check-clauses stx syn-error-name (cddr more) relation?)])
|
||||
(values #'id doms codomain clauses))]
|
||||
[else
|
||||
(loop (cdr more) (cons (car more) dom-pats))])))]
|
||||
|
|
@ -1198,19 +1208,21 @@
|
|||
stx
|
||||
rest)])]))
|
||||
|
||||
(define (check-clauses stx syn-error-name rest)
|
||||
(define (check-clauses stx syn-error-name rest relation?)
|
||||
(syntax-case rest ()
|
||||
[([(lhs ...) roc1 roc2 ...] ...)
|
||||
rest]
|
||||
[([(lhs ...) rhs ...] ...)
|
||||
(begin
|
||||
(for-each
|
||||
(λ (clause)
|
||||
(syntax-case clause ()
|
||||
[(a b) (void)]
|
||||
[x (raise-syntax-error syn-error-name "expected a pattern and a right-hand side" stx clause)]))
|
||||
(syntax->list #'([(lhs ...) rhs ...] ...)))
|
||||
(raise-syntax-error syn-error-name "error checking failed.3" stx))]
|
||||
(if relation?
|
||||
rest
|
||||
(begin
|
||||
(for-each
|
||||
(λ (clause)
|
||||
(syntax-case clause ()
|
||||
[(a b) (void)]
|
||||
[x (raise-syntax-error syn-error-name "expected a pattern and a right-hand side" stx clause)]))
|
||||
(syntax->list #'([(lhs ...) rhs ...] ...)))
|
||||
(raise-syntax-error syn-error-name "error checking failed.3" stx)))]
|
||||
[([x roc ...] ...)
|
||||
(begin
|
||||
(for-each
|
||||
|
|
|
|||
|
|
@ -656,6 +656,23 @@
|
|||
(test (term (<: 1 2 1 3 4)) #t)
|
||||
(test (term (<: 1 2 3 1 4)) #t)
|
||||
(test (term (<: 1 2 3 4 1)) #t))
|
||||
|
||||
(let ()
|
||||
(define-relation empty-language
|
||||
[(<: number_1 number_1)])
|
||||
(test (term (<: 1 1)) #t)
|
||||
(test (term (<: 1 2)) #f))
|
||||
|
||||
(let ()
|
||||
(define-relation empty-language
|
||||
[(<: number_1 number_2 number_3)
|
||||
,(= (term number_1) (term number_2))
|
||||
,(= (term number_2) (term number_3))])
|
||||
(test (term (<: 1 2 3)) #f)
|
||||
(test (term (<: 1 1 2)) #f)
|
||||
(test (term (<: 1 2 2)) #f)
|
||||
(test (term (<: 1 1 1)) #t))
|
||||
|
||||
|
||||
; ;; ; ;; ;
|
||||
; ; ; ; ;
|
||||
|
|
|
|||
|
|
@ -982,11 +982,8 @@ and @scheme[#f] otherwise.
|
|||
|
||||
@defform/subs[#:literals ()
|
||||
(define-relation language-exp
|
||||
[(name @#,ttpattern ...) @#,tttterm extras ...]
|
||||
...)
|
||||
([extras (side-condition scheme-expression)
|
||||
(where tl-pat @#,tttterm)]
|
||||
[tl-pat identifier (tl-pat-ele ...)]
|
||||
[(name @#,ttpattern ...) @#,tttterm ...] ...)
|
||||
([tl-pat identifier (tl-pat-ele ...)]
|
||||
[tl-pat-ele tl-pat (code:line tl-pat ... (code:comment "a literal ellipsis"))])]{
|
||||
|
||||
The @scheme[define-relation] form builds a relation on
|
||||
|
|
@ -995,21 +992,22 @@ expressions. The first argument indicates the language used
|
|||
to resolve non-terminals in the pattern expressions. Each of
|
||||
the rhs-expressions is implicitly wrapped in @|tttterm|.
|
||||
|
||||
If specified, the side-conditions are collected with
|
||||
@scheme[and] and used as guards on the case being matched. The
|
||||
argument to each side-condition should be a Scheme
|
||||
expression, and the pattern variables in the @|ttpattern| are
|
||||
bound in that expression.
|
||||
Relations are like metafunctions in that they are called with
|
||||
arguments and return results (unlike in, say, prolog, where a relation
|
||||
definition would be able to synthesize some of the arguments based on
|
||||
the values of others).
|
||||
|
||||
Unlike metafunctions, relations check all possible ways to match each
|
||||
case, looking for a true result and if none of the clauses match, then
|
||||
the result is @scheme[#f].
|
||||
the result is @scheme[#f]. If there are multiple expressions on
|
||||
the right-hand side of a relation, then all of them must be satisfied
|
||||
in order for that clause of the relation to be satisfied.
|
||||
|
||||
Note that relations are assumed to always return the same results
|
||||
for the same inputs, and their results are cached, unless
|
||||
Note that relations are assumed to always return the same results for
|
||||
the same inputs, and their results are cached, unless
|
||||
@scheme[caching-enable?] is set to @scheme[#f]. Accordingly, if a
|
||||
metafunction is called with the same inputs twice, then its body is
|
||||
only evaluated a single time.
|
||||
relation is called with the same inputs twice, then its right-hand
|
||||
sides are evaluated only once.
|
||||
}
|
||||
|
||||
@defparam[current-traced-metafunctions traced-metafunctions (or/c 'all (listof symbol?))]{
|
||||
|
|
|
|||
Loading…
Reference in New Issue
Block a user