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

Redex: rework metafunction compilation/search for parameters

Browse Source
This commit is contained in:
Burke Fetscher 2013-03-20 23:03:22 -05:00
parent bdf1866e80
commit 40fc96cacf
2 changed files with 63 additions and 35 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

46
collects/redex/private/reduction-semantics.rkt
View File

@ -29,7 +29,8 @@
racket/list
syntax/parse
syntax/parse/experimental/contract
syntax/name))
syntax/name
racket/syntax))
(define (language-nts lang)
(hash-map (compiled-lang-ht lang) (λ (x y) x)))
@ -1143,7 +1144,7 @@
prev-metafunction
(λ ()
(raise-syntax-error syn-error-name "expected a previously defined metafunction" orig-stx prev-metafunction))))
(let*-values ([(contract-name dom-ctc codom-contracts pats)
(let*-values ([(contract-name dom-ctcs codom-contracts pats)
(split-out-contract orig-stx syn-error-name #'rest #f)]
[(name _) (defined-name (list contract-name) pats orig-stx)])
(when (and prev-metafunction (eq? (syntax-e #'name) (syntax-e prev-metafunction)))
@ -1160,7 +1161,7 @@
#,prev-metafunction
name
name-predicate
#,dom-ctc
#,dom-ctcs
#,codom-contracts
#,pats
#,syn-error-name))
@ -1204,9 +1205,9 @@
(define-syntax (generate-metafunction stx)
(syntax-case stx ()
[(_ orig-stx lang prev-metafunction name name-predicate dom-ctc codom-contracts pats syn-error-name)
[(_ orig-stx lang prev-metafunction name name-predicate dom-ctcs codom-contracts pats syn-error-name)
(let ([prev-metafunction (and (syntax-e #'prev-metafunction) #'prev-metafunction)]
[dom-ctc (syntax-e #'dom-ctc)]
[dom-ctcs (syntax-e #'dom-ctcs)]
[codom-contracts (syntax-e #'codom-contracts)]
[pats (syntax-e #'pats)]
[syn-error-name (syntax-e #'syn-error-name)])
@ -1271,12 +1272,12 @@
(syntax-column lhs)))
pats)]
[(dom-side-conditions-rewritten dom-names dom-names/ellipses)
(if dom-ctc
(if dom-ctcs
(rewrite-side-conditions/check-errs
lang-nts
syn-error-name
#f
dom-ctc)
dom-ctcs)
#'(any () ()))]
[((codom-side-conditions-rewritten codom-names codom-names/ellipses) ...)
(map (λ (codom-contract)
@ -1356,7 +1357,7 @@
#`(extend-lhs-pats #,(term-fn-get-id (syntax-local-value prev-metafunction))
new-lhs-pats)
#`new-lhs-pats)))
#,(if dom-ctc #'dsc #f)
#,(if dom-ctcs #'dsc #f)
`(codom-side-conditions-rewritten ...)
'name))))
'disappeared-use
@ -1404,11 +1405,12 @@
(define clause-stx
(with-syntax ([(prem-rw ...) ps-rw]
[(eqs ...) extra-eqdqs]
[(prev-lhs-pat ...) prev-lhs-pats]
[(((lhs-pat-ps ...) prev-lhs-pat) ...)
(map fix-and-extract-dq-vars prev-lhs-pats)]
[(mf-clauses ...) mf-clausess]
[(rhs-pat) rhs-pats])
#`((clause '(list lhs-pat rhs-pat)
(list eqs ... (dqn 'lhs-pat 'prev-lhs-pat) ...)
(list eqs ... (dqn '(lhs-pat-ps ...) 'prev-lhs-pat 'lhs-pat) ...)
(list prem-rw ... mf-clauses ...)
#,lang
'#,name)
@ -1417,6 +1419,30 @@
(cons #'lhs-pat prev-lhs-pats)))))
(reverse rev-clauses))
(define-for-syntax (fix-and-extract-dq-vars pat)
(define new-ids (hash))
(let recur ([pat pat])
(syntax-case pat (list name)
[(name vname p)
(with-syntax ([((vs ...) new-p) (recur #'p)]
[new-vn (datum->syntax #'vname
(let* ([vn (syntax-e #'vname)]
[vn-sym (format "~s_" vn)])
(hash-ref new-ids vn
(λ ()
(define new
(syntax-e (generate-temporary vn-sym)))
(set! new-ids (hash-set new-ids vn new))
new)))
#'vname)])
#'((new-vn vs ...) (name new-vn new-p)))]
[(list ps ...)
(with-syntax* ([(((vs ...) new-ps) ...) (map recur (syntax->list #'(ps ...)))]
[(u-vs ...) (remove-duplicates (syntax->list #'(vs ... ...)) #:key syntax-e)])
#'((u-vs ...) (list new-ps ...)))]
[pat
#'(() pat)])))
(define-for-syntax (check-arity-consistency mode contracts full-def)
(when (and contracts (not (= (length mode) (length contracts))))
(raise-syntax-error

52
collects/redex/private/search.rkt
View File

@ -29,7 +29,8 @@
(define-struct prem (mk-clauses pat) #:transparent)
;; eq/dqs : (listof (or/c eq? dq?))
(define-struct eqn (lhs rhs) #:transparent)
(define-struct dqn (lhs rhs) #:transparent)
;; ps : (listof symbol?) - the universally quantified variables ("parameters")
(define-struct dqn (ps lhs rhs) #:transparent)
(define (prem-clauses prem) ((prem-mk-clauses prem)))
(define-struct partial-rule (pat clauses tr-loc bound)
@ -164,36 +165,31 @@
(define (do-unification clse input env)
(match clse
[(clause head-pat eq/dqs prems lang name)
(define-values (eqs dqs) (partition eqn? eq/dqs))
(define env1
(let loop ([e env]
[eqdqs eq/dqs])
(match eqdqs
['() e]
[(cons eqdq rest)
(match eqdq
[(eqn lhs rhs)
(loop e rest)]
[(dqn lhs rhs)
(define u-res (disunify lhs rhs e lang))
(and u-res
(loop (trim-dqs u-res rhs) rest))])])))
[dqs dqs])
(match dqs
['() e]
[(cons (dqn ps lhs rhs) rest)
(dqn ps lhs rhs)
(define u-res (disunify ps lhs rhs e lang))
(and u-res
(loop u-res rest))])))
(define head-p*e (and env1 (unify input head-pat env1 lang)))
(cond
[head-p*e
(define res-p (p*e-p head-p*e))
(let loop ([e (p*e-e head-p*e)]
[eqdqs eq/dqs])
(match eqdqs
[eqs eqs])
(match eqs
['()
(p*e (p*e-p head-p*e) e)]
[(cons eqdq rest)
(match eqdq
[(eqn lhs rhs)
(define u-res (unify lhs rhs e lang))
(and u-res
(loop (p*e-e u-res) rest))]
[(dqn lhs rhs)
(loop e rest)])]))]
[(cons (eqn lhs rhs) rest)
(eqn lhs rhs)
(define u-res (unify lhs rhs e lang))
(and u-res
(loop (p*e-e u-res) rest))]))]
[else #f])]))
(define (trim-dqs e pat)
@ -302,9 +298,15 @@
[(eqn lhs rhs)
(eqn (fresh-pat-vars lhs instantiations)
(fresh-pat-vars rhs instantiations))]
[(dqn lhs rhs)
(dqn (fresh-pat-vars lhs instantiations)
(fresh-pat-vars rhs (make-hash)))]))]
[(dqn ps lhs rhs)
(dqn (map (λ (id) (hash-ref instantiations id
(λ ()
(define unique-id (make-uid id))
(hash-set! instantiations id unique-id)
unique-id)))
ps)
(fresh-pat-vars lhs instantiations)
(fresh-pat-vars rhs instantiations))]))]
[prems (for/list ([p (clause-prems clause-raw)])
(match p
[(prem mk-clauses pat)