From fe0fd0d1524673128d1bba1241a793d38c8d4820 Mon Sep 17 00:00:00 2001 From: Burke Fetscher Date: Fri, 22 Mar 2013 16:14:03 -0500 Subject: [PATCH] Redex: remove some now extraneous code --- collects/redex/private/jdg-gen.rkt | 3 +- collects/redex/private/pat-unify.rkt | 11 +- collects/redex/private/search.rkt | 251 +-------------------------- 3 files changed, 5 insertions(+), 260 deletions(-) diff --git a/collects/redex/private/jdg-gen.rkt b/collects/redex/private/jdg-gen.rkt index 5e3447286d..4393750ce5 100644 --- a/collects/redex/private/jdg-gen.rkt +++ b/collects/redex/private/jdg-gen.rkt @@ -17,9 +17,8 @@ ;; term generation -;; pat->term pat* env -> term +;; pat->term lang pat* env env -> term (define (pat->term lang pat full-env [term-e (make-hash)]) - ;(printf "\np->t: ~s\n\n ~s\n" pat full-env) (define nt-matchers (make-hash)) (define eqs (env-eqs full-env)) (define (get-matcher nt) diff --git a/collects/redex/private/pat-unify.rkt b/collects/redex/private/pat-unify.rkt index 24ac15062f..8718b14616 100644 --- a/collects/redex/private/pat-unify.rkt +++ b/collects/redex/private/pat-unify.rkt @@ -150,7 +150,6 @@ ;; pat pat env -> (or/c p*e #f) (define (unify t u e L) - ;(-> pat? pat? env/c compiled-lang? (or/c p*e/c #f)) (parameterize ([dqs-found (make-hash)]) (define eqs (hash-copy (env-eqs e))) (define t* (bind-names t eqs L)) @@ -186,7 +185,6 @@ ;; pat pat env lang -> (or/c env #f) (define (disunify params t u e L) - ;(-> pat? pat? env/c any/c (or/c env/c #f)) (parameterize ([new-eqs (make-hash)]) (define eqs (hash-copy (env-eqs e))) (define t* (bind-names t eqs L)) @@ -243,8 +241,8 @@ (recur p)] [else (unless (groundable? p) - (error 'resolve/termable-pat - "non-termable pat at internal pattern position: ~s" p)) + (error resolve-no-nts/pat + "non-groundable pat at internal pattern position: ~s" p)) p]))) @@ -286,7 +284,6 @@ (and new-dq (match new-dq [#t (loop ok rest)] - #;[`((list)(list)) (loop ok rest)] [else (loop (cons new-dq ok) rest)])))])]))) ;; disunfy* pat* pat* eqs lang -> dq or boolean (dq is a pat*) @@ -303,15 +300,13 @@ [`((list) (list)) #f] [else - (dq new-ps new-dq)]) - #;(extend-dq (new-eqs) base-dq)])))) + (dq new-ps new-dq)])])))) (define (param-elim params unquantified-dq) (let loop ([dq-rest unquantified-dq] [ps params] [new-dq-l '()] [new-dq-r '()]) - ;(printf "~s ~s ~s ~s\n" dq-rest ps new-dq-l new-dq-r) (match dq-rest ['((list) (list)) (values ps `((list ,@new-dq-l) (list ,@new-dq-r)))] diff --git a/collects/redex/private/search.rkt b/collects/redex/private/search.rkt index 39c25236a8..b3230cbee3 100644 --- a/collects/redex/private/search.rkt +++ b/collects/redex/private/search.rkt @@ -96,12 +96,11 @@ [else (values #f fs)])) (define (choose-rule env fringe fail) - ;(-> env? (listof partial-rule?) number? (-> (or/c env? #f)) (or/c env? #f)) (cond [(empty? fringe) (values env fail)] [else - (define new-f fringe #;(prune-fringe fringe env)) + (define new-f fringe) (if new-f (push-down (car new-f) env (cdr new-f) fail) (fail-back fail))])) @@ -134,7 +133,6 @@ (define prem-cls (prem-clauses prem)) (make-partial-rule (prem-pat prem) (if (positive? bound) - #;(shuffle-clauses-stlc prem-cls (sub1 bound)) (shuffle prem-cls) (order-clauses prem-cls)) (cons n tr-loc) @@ -191,80 +189,6 @@ (and u-res (loop (p*e-e u-res) rest))]))] [else #f])])) - -(define (trim-dqs e pat) - (define p-vars - (let loop ([p pat]) - (match p - [`(name ,id ,pat) - (set-union (set id) - (loop pat))] - [`(list ,pats ...) - (apply set-union (for/list ([p pats]) - (loop p)))] - [_ (set)]))) - (struct-copy env e - [dqs (for/list ([dq (env-dqs e)]) - (trim-dq-vars dq p-vars))])) - -;; remove variables from lhs patterns from dqs -;; since we only care about constraints on the input pattern -;; if it's on one side of one equation, drop it -;; if it's on one side of two equations, eliminate it -(define (trim-dq-vars dq vs) - (define dqps0 (dq->dq-pairs dq)) - (define var-vals (make-hash)) - (define (update-vvs id val) - (hash-set! var-vals id - (set-union (set val) - (hash-ref var-vals id (set))))) - (define (eliminable? id) (set-member? vs id)) - (define dqps - (for/fold ([new-dps '()]) - ([d dqps0]) - (match d - [(dqp `(name ,(? eliminable? id) ,_) r) - (update-vvs id r) - new-dps] - [(dqp l `(name ,(? eliminable? id) ,_)) - (update-vvs id l) - new-dps] - [else - (cons d new-dps)]))) - (define-values (ls0 rs0) - (for/fold ([l '()] [r '()]) - ([(id vals) (in-hash var-vals)]) - (cond - [(< (set-count vals) 2) - (values l r)] - [else - (for/fold ([l1 l] [r1 r]) - ([a-pair (in-list (for*/list ([a vals] [b (set-remove vals a)]) - (list a b)))]) - (values (cons (first a-pair) l1) - (cons (second a-pair) r1)))]))) - (let loop ([ps dqps] - [new-ls ls0] - [new-rs rs0]) - (match ps - ['() - (list (cons 'list (reverse new-ls)) - (cons 'list (reverse new-rs)))] - [(cons (dqp (list 'name id bnd) r) ps+) - (if (set-member? vs id) - (loop ps+ new-ls new-rs) - (loop ps+ - (cons (list 'name id bnd) new-ls) - (cons r new-rs)))] - [else - (error 'disunify "bad-dq: ~s" dq)]))) - -(define-struct dqp (l r)) - -(define (dq->dq-pairs dq) - (map (λ (a b) (dqp a b)) - (cdr (first dq)) - (cdr (second dq)))) @@ -378,176 +302,3 @@ (define (set-last-gen-trace! trace) (set! most-recent-trace trace)) - -;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; - -;; the following is experimental and is not currently used.... - - -(define (prune-fringe fringe env) - (let/ec fail - (define new-f - (for/list ([a-p-rule (in-list fringe)]) - (define new-cs (for/list ([c (in-list (partial-rule-clauses a-p-rule))] - #:when (do-unification (fresh-clause-vars c) (partial-rule-pat a-p-rule) env)) - c)) - (when (empty? new-cs) - (fail #f)) - (struct-copy partial-rule - a-p-rule - [clauses new-cs]))) - (define candidate-length (length (partial-rule-clauses (car new-f)))) - (if (< candidate-length 2) - new-f - (let loop ([unchecked new-f] - [checked '()]) - (cond - [(empty? unchecked) - (reverse checked)] - [(< (length (partial-rule-clauses (car unchecked))) candidate-length) - (cons (car unchecked) (append (reverse checked) (cdr unchecked)))] - [else - (loop (cdr unchecked) (cons (car unchecked) checked))]))))) - - -(define bound-fac - (let ([memo (hash)]) - (λ (b) - (hash-ref memo b (λ () (* 1000 (- 1 (exp (- (* 1.75 b)))))))))) - -;; specific to examples/chalmers/stlc -;; waht about preferring bound variables to constants -(define (shuffle-clauses-stlc clauses bound) - (cond - [(= (length clauses) 5) ;; typeof - last 3 recur - (define-values (base v-rec) - (split-at clauses 2)) - (define v-c (car v-rec)) - (define rec (cdr v-rec)) - (if (< (bound-fac bound) (random 1000)) - (append (shuffle base) (shuffle v-rec)) - (append (shuffle v-rec) (shuffle base)))] - [(= (length clauses) 4) ;; const - all base - (shuffle clauses)] - [(= (length clauses) 3) ;; lookup - #2 recurs - (define-values (base rec) - (values (list (list-ref clauses 0) (list-ref clauses 2)) - (list (list-ref clauses 1)))) - (if (< (bound-fac bound) (random 1000)) - (append (shuffle base) (shuffle rec)) - (append (shuffle rec) (shuffle base)))])) - -(define (better-shuffle-clauses clauses bound) - (cond - [(zero? (random 2)) - (shuffle clauses)] - [(= (length clauses) 5) ;; typeof - last 3 recur - (define app-weight (* (terms/depth bound) (terms/depth bound))) - (define lam-weight (terms/depth bound)) - (define var-weight (vars/depth bound)) - (define cst-weight 3) - (define num-weight 1) - (define total (+ app-weight lam-weight var-weight cst-weight num-weight)) - (define rnd (big-random total)) - (define idx (cond [(rnd . < . app-weight) 4] - [(rnd . < . (+ lam-weight app-weight)) 3] - [(rnd . < . (+ lam-weight app-weight var-weight)) 2] - [(rnd . < . (+ lam-weight app-weight var-weight cst-weight)) 1] - [else 0])) - (define-values (h t) (split-at clauses idx)) - (cons (list-ref clauses idx) - (shuffle (append h (cdr t))))] - [(= (length clauses) 4) ;; const - all base - (shuffle clauses)] - [(= (length clauses) 3) ;; lookup - #2 recurs - (define rec-weight (vars/depth bound)) - (if ((big-random (+ rec-weight 2)) . < . 2) - (append (shuffle (list (list-ref clauses 0) (list-ref clauses 2))) - (list (list-ref clauses 2))) - (append (list (list-ref clauses 2)) - (shuffle (list (list-ref clauses 0) (list-ref clauses 2)))))] - #;[else - (shuffle clauses)])) - -(define (big-random n) - (if (n . < . 4294967087) - (random n) - (+ (random 4294967087) (big-random (- n 4294967087))))) - - -(define (shuffle-clauses-poly-stlc clauses bound) - (cond - [(equal? (clause-name (car clauses)) 'typeof) ;; typeof - last 4 recur - (define-values (base rec) - (split-at clauses 2)) - (if (< (bound-fac bound) (random 1000)) - (append (shuffle base) (shuffle rec)) - (append (shuffle rec) (shuffle base)))] - [(equal? (clause-name (car clauses)) 'const-type) ;; const - all base - (shuffle clauses)] - [(equal? (clause-name (car clauses)) 'lookup) ;; lookup - #2 recurs - (define-values (base rec) - (values (list (list-ref clauses 0) (list-ref clauses 2)) - (list (list-ref clauses 1)))) - (if (< (bound-fac bound) (random 1000)) - (append (shuffle base) (shuffle rec)) - (append (shuffle rec) (shuffle base)))] - [else - (shuffle clauses)])) - -(define-syntax (define-memo stx) - (syntax-case stx () - [(_ (f-id args ...) body) - #'(define f-id - (let ([memo (make-hash)]) - (λ (args ...) - (hash-ref memo (list args ...) - (λ () - (define res (begin body)) - (hash-set! memo (list args ...) res) - res)))))])) - -(define-memo (terms/depth d) - (cond - [(= d 0) 1] - [else - (+ 1 - (vars/depth (sub1 d)) ;; vars - (terms/depth (sub1 d)) ;; lambda - (* (terms/depth (sub1 d)) ;; app - (terms/depth (sub1 d))))])) - -(define-memo (vars/depth d) - (cond - [(= d 0) 1] - [else - (+ 1 - (vars/depth (sub1 d)))])) - - -(define (score-rule rule env) - (match rule - [(partial-rule pat clauses tr-loc bound) - (length - (filter (λ (c) - (do-unification (fresh-clause-vars c) pat env)) - clauses))])) - -(define (pick-rule rules env) - (let loop ([rs-seen '()] - [rs rules]) - (match rs - ['() rs-seen] - [(cons r rs*) - (if ((score-rule r env) . < . 2) - (cons r (append rs* rs-seen)) - (loop (cons r rs-seen) rs*))]))) - -(define (sort-rules rules env) - (define weights (sort (for/list ([i (length rules)]) - (list (score-rule (list-ref rules i) env) i)) - < - #:key first)) - (for/list ([w (in-list weights)]) - (list-ref rules (second w)))) -