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

Add redex enum support for cross patterns

Browse Source
This commit is contained in:
Max New 2013-11-18 20:13:44 -06:00
parent 1e6786eedf
commit 0b663736fb
5 changed files with 119 additions and 71 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

110
pkgs/redex-pkgs/redex-lib/redex/private/enum.rkt
View File

@ -5,6 +5,7 @@
racket/list
racket/math
racket/match
racket/promise
racket/set
"enumerator.rkt"
@ -17,7 +18,7 @@
(provide
(contract-out
[lang-enumerators (-> (listof nt?) lang-enum?)]
[lang-enumerators (-> (listof nt?) (promise/c (listof nt?)) lang-enum?)]
[pat-enumerator (-> lang-enum?
any/c ;; pattern
enum?)]
@ -25,7 +26,10 @@
[lang-enum? (-> any/c boolean?)]
[enum? (-> any/c boolean?)]))
(struct lang-enum (enums unused-var/e))
;; nt-enums : hash[sym -o> enum]
;; cc-enums : promise/c (hash[sym -o> enum])
;; unused-var/e : enum
(struct lang-enum (nt-enums delayed-cc-enums unused-var/e))
(struct repeat (n terms) #:transparent)
(struct name-ref (name) #:transparent)
(struct misname-ref (name tag) #:transparent)
@ -36,59 +40,64 @@
;; Top level exports
(define enum-ith decode)
(define (lang-enumerators lang)
(define l-enums (make-hash))
(define (lang-enumerators lang cc-lang)
(define (make-lang-table! ht lang)
(define (enumerate-lang! cur-lang enum-f)
(for ([nt (in-list cur-lang)])
(hash-set! ht
(nt-name nt)
(with-handlers ([exn:fail:redex? fail/e])
(enum-f (nt-rhs nt)
nt-enums)))))
(define-values (fin-lang rec-lang) (sep-lang lang))
(enumerate-lang! fin-lang
(λ (rhs enums)
(enumerate-rhss rhs l-enum)))
(enumerate-lang! rec-lang
(λ (rhs enums)
(thunk/e +inf.f
(λ ()
(enumerate-rhss rhs l-enum)))))
ht)
(define nt-enums (make-hash))
(define cc-enums (delay (make-hash)))
(define unused-var/e
(apply except/e
var/e
(used-vars lang)))
(define (enumerate-lang! cur-lang enum-f)
(for ([nt (in-list cur-lang)])
(hash-set! l-enums
(nt-name nt)
(with-handlers ([exn:fail:redex? fail/e])
(enum-f (nt-rhs nt)
l-enums)))))
(define-values (fin-lang rec-lang) (sep-lang lang))
(enumerate-lang! fin-lang
(λ (rhs enums)
(enumerate-rhss rhs enums unused-var/e)))
(enumerate-lang! rec-lang
(λ (rhs enums)
(thunk/e +inf.f
(λ ()
(enumerate-rhss rhs enums unused-var/e)))))
(define l-enum
(lang-enum nt-enums cc-enums unused-var/e))
(make-lang-table! nt-enums lang)
(define filled-cc-enums
(delay (make-lang-table! (force cc-enums) (force cc-lang))))
(lang-enum l-enums unused-var/e))
(struct-copy lang-enum l-enum [delayed-cc-enums filled-cc-enums]))
(define (pat-enumerator l-enum pat)
(map/e
to-term
(λ (_)
(redex-error 'pat-enum "Enumerator is not a bijection"))
(pat/e pat
(lang-enum-enums l-enum)
(lang-enum-unused-var/e l-enum))))
(pat/e pat l-enum)))
(define (enumerate-rhss rhss l-enums unused/e)
(define (enumerate-rhss rhss l-enum)
(apply sum/e
(for/list ([production (in-list rhss)])
(pat/e (rhs-pattern production)
l-enums
unused/e))))
(pat/e (rhs-pattern production) l-enum))))
(define (pat/e pat l-enums unused/e)
(define (pat/e pat l-enum)
(match-define (ann-pat nv pp-pat) (preprocess pat))
(map/e
ann-pat
(λ (ap)
(values (ann-pat-ann ap)
(ann-pat-pat ap)))
(env/e nv l-enums unused/e)
(pat-refs/e pp-pat l-enums unused/e)))
(env/e nv l-enum)
(pat-refs/e pp-pat l-enum)))
;; (: pat-refs/e : Pat (HashTable Symbol (Enum Pat)) (Enum Symbol) -> Enum RefPat)
(define (pat-refs/e pat nt-enums unused/e)
(define (pat-refs/e pat l-enum)
(define (loop pat)
(match-a-pattern
pat
@ -105,10 +114,10 @@
[`(variable-prefix ,s)
(var-prefix/e s)]
[`variable-not-otherwise-mentioned
unused/e]
(lang-enum-unused-var/e l-enum)]
[`hole (const/e the-hole)]
[`(nt ,id)
(hash-ref nt-enums id)]
(lang-enum-get-nt-enum l-enum id)]
[`(name ,n ,pat)
(const/e (name-ref n))]
[`(mismatch-name ,n ,tag)
@ -129,7 +138,7 @@
[`(side-condition ,p ,g ,e)
(unsupported pat)]
[`(cross ,s)
(unsupported pat)]
(lang-enum-get-cross-enum l-enum s)]
[`(list ,sub-pats ...)
(list/e
(for/list ([sub-pat (in-list sub-pats)])
@ -151,10 +160,10 @@
(const/e pat)]))
(loop pat))
(define/match (env/e nv l-enums unused/e)
[((env names misnames nreps) _ _)
(define/match (env/e nv l-enum)
[((env names misnames nreps) _)
(define (val/e p)
(pat-refs/e p l-enums unused/e))
(pat-refs/e p l-enum))
(define/match (misvals/e p-ts)
[((cons p ts))
@ -171,7 +180,7 @@
(define tpats/e
(hash-traverse/e val/e tpats))
(many/e
(cons/e (env/e nv l-enums unused/e)
(cons/e (env/e nv l-enum)
tpats/e))])
(define names-env
(hash-traverse/e val/e names))
@ -193,15 +202,14 @@
;; to-term : (ann-pat t-env pat-with-refs) -> redex term
(define/match (to-term ap)
[((ann-pat nv term))
((refs-to-fn term) nv)])
(strip-hide-holes ((refs-to-fn term) nv))])
;; refs-to-fn : RefPat -> (TEnv -> Term)
(define (refs-to-fn refpat)
(match refpat
[(ann-pat _ _)
(define term
(to-term refpat))
(λ (_) term)]
[(ann-pat nv term)
(λ (_)
((refs-to-fn term) nv))]
[(decomp ctx-refs termpat-refs)
(define ctx-fn (refs-to-fn ctx-refs))
(define term-fn (refs-to-fn termpat-refs))
@ -237,6 +245,12 @@
[_ (sequence-fn (list (refs-to-fn subrefpat)))]))))]
[else (λ (_) refpat)]))
(define (strip-hide-holes term)
(match term
[(hide-hole t) (strip-hide-holes t)]
[(list ts ...) (map strip-hide-holes ts)]
[_ term]))
(define (plug-hole ctx term)
(define (plug ctx)
(match ctx
@ -255,3 +269,11 @@
(λ (x)
(for/list ([f (in-list fs)])
(f x))))
;; lang-enum-get-nt-enum : lang-enum Symbol -> Enum
(define (lang-enum-get-nt-enum l-enum s)
(hash-ref (lang-enum-nt-enums l-enum) s))
;; lang-enum-get-cross-enum : lang-enum Symbol -> Enum
(define (lang-enum-get-cross-enum l-enum s)
(hash-ref (force (lang-enum-delayed-cc-enums l-enum)) s))

7
pkgs/redex-pkgs/redex-lib/redex/private/matcher.rkt
View File

@ -163,7 +163,7 @@ See match-a-pattern.rkt for more details
literals
nt-map
collapsible-nts
(lang-enumerators lang))]
#f)]
[non-list-nt-table (build-non-list-nt-label lang)]
[list-nt-table (build-list-nt-label lang)]
[do-compilation
@ -209,7 +209,10 @@ See match-a-pattern.rkt for more details
(do-compilation across-ht across-list-ht compatible-context-language)
compatible-context-language)))
(do-compilation clang-ht clang-list-ht lang)
(struct-copy compiled-lang clang [delayed-cclang compatible-context-language])))
(define enumerators
(lang-enumerators lang compatible-context-language))
(struct-copy compiled-lang clang [delayed-cclang compatible-context-language]
[enum-table enumerators])))
;; mk-uf-sets : (listof (listof sym)) -> (hash[symbol -o> uf-set?])
;; in the result hash, each nt maps to a uf-set that represents

11
pkgs/redex-pkgs/redex-lib/redex/private/pat-unify.rkt
View File

@ -1,10 +1,11 @@
#lang unstable/2d racket/base
(require racket/list
racket/contract
racket/set
racket/match
(require racket/contract
racket/function
racket/list
racket/match
racket/promise
racket/set
"match-a-pattern.rkt"
"matcher.rkt"
"lang-struct.rkt"
@ -849,7 +850,7 @@
(define empty-lang
(compiled-lang
#f #f #f #f #f #f #f #f #f #f '() #f (hash)
(lang-enumerators '())))
(lang-enumerators '() (delay '()))))
(define unique-name-nums (make-parameter 0))

45
pkgs/redex-pkgs/redex-lib/redex/private/preprocess-lang.rkt
View File

@ -24,10 +24,10 @@
;; sorts rhs's so that recursive ones go last
(define (sep-lang lang)
(define (filter-edges edges lang)
(for/fold ([ht (hash)])
(for/fold ([filtered (hash)])
([nt (in-list lang)])
(define name (nt-name nt))
(hash-set ht name (hash-ref edges name))))
(hash-set filtered name (hash-ref edges name))))
(define edges (find-edges lang))
(define cyclic-nts (find-cycles edges))
(define-values (cyclic non-cyclic)
@ -55,10 +55,22 @@
(λ (rhs)
(let loop ([pat (rhs-pattern rhs)]
[s (set)])
(match-a-pattern/single-base-case
(match-a-pattern
pat
[`(name ,name ,pat)
[`any s]
[`number s]
[`string s]
[`natural s]
[`integer s]
[`real s]
[`boolean s]
[`variable s]
[`(variable-except ,var ...) s]
[`(variable-prefix ,var) s]
[`variable-not-otherwise-mentioned s]
[`hole s]
[`(nt ,id) (set-add s id)]
[`(name ,var ,pat)
(loop pat s)]
[`(mismatch-name ,name ,pat)
(loop pat s)]
@ -66,7 +78,8 @@
(set-union (loop p1 s)
(loop p2 s))]
[`(hide-hole ,p) (loop p s)]
[`(side-condition ,p ,_ ,_) (loop p s)]
[`(side-condition ,p ,_1 ,_2) (loop p s)]
[`(cross ,id) (set-add s id)]
[`(list ,sub-pats ...)
(fold-map/set
(λ (sub-pat)
@ -75,11 +88,7 @@
(loop pat s)]
[else (loop sub-pat s)]))
sub-pats)]
[_ (match pat
[`(nt ,id)
(set-add s id)]
[_ s])
])))
[(? (compose not pair?)) s])))
(nt-rhs nt))))
(hash)
lang))
@ -96,8 +105,7 @@
(λ (next)
(rec next
(set-add seen cur)))
(set->list (hash-ref edges
cur)))]))
(set->list (hash-ref edges cur (set))))]))
(set-add s v)
s))
(set)
@ -120,8 +128,7 @@
[`(variable-prefix ,s) #f]
[`variable-not-otherwise-mentioned #f]
[`hole #f]
[`(nt ,id)
(set-member? recs id)]
[`(nt ,id) (set-member? recs id)]
[`(name ,name ,pat)
(rec pat)]
[`(mismatch-name ,name ,pat)
@ -130,9 +137,8 @@
(or (rec p1)
(rec p2))]
[`(hide-hole ,p) (rec p)]
;; not sure about these 2, but they are unsupported by enum anyway
[`(side-condition ,p ,g ,e) #f]
[`(cross ,s) #f]
[`(side-condition ,p ,g ,e) #f]
[`(cross ,s) (set-member? recs s)]
[`(list ,sub-pats ...)
(ormap (λ (sub-pat)
(match sub-pat
@ -220,7 +226,6 @@
;; directly-used-nts : pat -> (setof symbol)
(define (directly-used-nts pat)
(match-a-pattern/single-base-case pat
[`(name ,n ,p)
(directly-used-nts p)]
[`(mismatch-name ,n ,p)
@ -243,6 +248,7 @@
sub-pats)]
[_ (match pat
[`(nt ,id) (set id)]
[`(cross ,id) (set id)]
[_ (set)])]))
;; used-vars : lang -> (listof symbol)
@ -274,7 +280,6 @@
(set-union (loop p1)
(loop p2))]
[`(hide-hole ,p) (loop p)]
;; not sure about these 2, but they are unsupported by enum anyway
[`(side-condition ,p ,g ,e) (set)]
[`(cross ,s) (set)]
[`(list ,sub-pats ...)

17
pkgs/redex-pkgs/redex-test/redex/tests/enum-test.rkt
View File

@ -155,3 +155,20 @@
(try-it 4 Holes ctx)
(try-it 100 Holes i)
(try-it 100 Holes i2)
(try-it 1 Holes hole)
(try-it 100 Holes (in-hole hole number))
;; Cross test
(define-language CrossLang
(e (e e)
(λ (x) e)
x)
(x variable-not-otherwise-mentioned))
(try-it 100 CrossLang e)
(try-it 100 CrossLang x)
(try-it 100 CrossLang (cross e))
(try-it 1 CrossLang (cross x))
(try-it 100 CrossLang (in-hole (cross x) e))
(try-it 100 CrossLang (in-hole (cross e) x))