Browse files

Basic Simplification Implemented.

Currently, the system can simplify most simpler expressions. For
instance, after a change from
(- (sqrt (+ x 1)) (sqrt x)) to
(/ (- (square (sqrt (+ x 1))) (square (sqrt x)))
   (+ (sqrt (+ x 1)) (sqrt x)))
the system correctly simplifies to
(/ 1 (+ (sqrt (+ x 1)) (sqrt x)))
Unfortunately, this version is apparently not any better for error that
the original version, so the simplifier throws out the result of the simplification.
  • Loading branch information...
HazardousPeach committed Mar 5, 2014
1 parent c178fb2 commit 9c4f0b445b5c4e5c52e860104c1d42ee79988186
Showing with 135 additions and 10 deletions.
  1. +1 −1 casio/brute-force.rkt
  2. +9 −3 casio/redgreen.rkt
  3. +125 −6 casio/simplify.rkt
@@ -62,4 +62,4 @@
giving up after `iters` iterations without progress"
(debug alt0 "for" iters #:from 'bfs #:tag 'enter)
(search-options (list (simplify (alt0))) '() iters))
(search-options (list (simplify alt0)) '() iters))
@@ -6,15 +6,21 @@
(require casio/programs)
(require casio/common)
(provide green? remove-red green-threshold)
(provide (all-defined-out))
(provide green? remove-red green-threshold errors-diff-score)
(define green-threshold (make-parameter 0))
(define (green? altn)
(and (alt-prev altn) ; The initial alternative is not green-tipped by convention
(> (green-threshold)
(apply + (errors-difference (alt-errors altn) (alt-errors (alt-prev altn)))))))
(errors-diff-score (alt-errors altn) (alt-errors (alt-prev altn))))))
(define (errors-diff-score e1 e2)
(let ([d (errors-difference e1 e2)])
(let*-values ([(reals infs) (partition (lambda (n) (rational? n)) d)]
[(positive-infs negative-infs) (partition (lambda (n) (> 0 n)) infs)])
(+ (apply + reals)
(* 100 (- (length positive-infs) (length negative-infs)))))))
;; Terminology clarification: the "stream" in this metaphor flows from the original program to our passed alternative.
;; "Upstream" and "up" both mean backwards in the change history, "downstream" and "down" both mean forward in the
@@ -5,6 +5,8 @@
(require casio/programs)
(require casio/points)
(require casio/common)
(require casio/redgreen)
(require racket/match)
(provide (all-defined-out))
@@ -15,16 +17,20 @@
[location (if (alt-prev altn)
(change-location (alt-change altn))
'(cdr cdr car))])
(when (*debug*) (println "Simplifying " (alt-program altn)))
(when (*debug*) (println "Simplifying " (alt-program altn) " at " (map (lambda (l) (append location l))
(define (simplify-at-locations slocations prog preerrors changes)
(if (null? slocations)
(let* ([full-location (append location (car slocations))]
[partly-simplified-prog (location-do full-location
[post-errors (errors partly-simplified-prog (*points*) (*exacts*))])
(if (< 0 (apply + (errors-difference post-errors preerrors)))
[post-errors (if (or (null? partly-simplified-prog) (not (pair? partly-simplified-prog)))
(map (lambda (x) 0) *points*)
(errors partly-simplified-prog (*points*) (*exacts*)))])
(when (*debug*) (println "Simplified to: " partly-simplified-prog))
(if (< 0 (errors-diff-score post-errors preerrors))
(simplify-at-locations (cdr slocations)
@@ -48,19 +54,20 @@
(apply-changes altn simplifying-changes))))
(define (simplify-expression expr)
(rm-fns-&-invs expr))
(decanonicalize (resolve-terms (canonicalize (rm-fns-&-invs expr)))))
(define (get-contained-vars expr)
(define (get-duplicated-vars expr)
(cond [(null? expr) '()]
(cond [(or (null? expr) (real? expr)) '()]
[(symbol? expr) (list expr)]
[(list? expr) (apply append (map get-duplicated-vars
(cdr expr)))]))
(remove-duplicates (get-duplicated-vars expr)))
(define func-inverses
'((exp . log)
(square . sqrt)))
(square . sqrt)
(- . -)))
(define (rm-fns-&-invs prog)
(define (rm-fn-&-inv expr)
@@ -83,3 +90,115 @@
(cons (car expr*) (map (lambda (x) (for-lists x f))
(cdr expr*)))
(define (canonicalize expr)
(if (pair? expr)
(let ([expr* (cons (car expr)
(map canonicalize (cdr expr)))])
(match expr*
[`(+ (+ . ,a) (+ . ,b)) (cons '+ (append a b))]
[`(+ ,a (+ . ,b)) (list* '+ a b)]
[`(+ (+ . ,a) ,b) (cons '+ (append a (list b)))]
[`(- (+ . ,a)) (cons '+ (map (lambda (expr) (list '- (canonicalize expr)))
[`(- ,a ,b) (canonicalize `(+ ,a (- ,b)))]
[a a]))
(define (decanonicalize cexpr)
(if (pair? cexpr)
(let ([expr* (cons (car cexpr)
(map decanonicalize (cdr cexpr)))])
(match expr*
[`(+ ,a ,b ,c . ,n) `(+ (+ ,a ,b) ,c ,n)]
[`(* 1 ,a) a]
[`(+ ,a (- ,b)) `(- ,a ,b)]
[`(+ (- ,a) ,b) `(- ,b ,a)]
[a a]))
(define (resolve-terms expr)
(let loop ([terms (cdr expr)] [acc '()])
(if (null? terms)
(cond [(null? acc) 0]
[(= 1 (length acc)) (car acc)]
[#t (cons '+ acc)])
(let* ([cur-term (car terms)]
[mterms (filter (lambda (t)
(equal? (term-atoms t)
(term-atoms cur-term)))
(cdr terms))])
(if (= 0 (length mterms))
(loop (cdr terms) (cons cur-term acc))
(loop (remove* mterms (cdr terms))
(append (combine-like-terms (cons (car terms) mterms))
(define (term-atoms expr)
;;(when (*debug*) (println "getting atoms for " expr))
(if (atomic expr)
(list expr)
(let ([positive-term (if (eq? (car expr) '-)
(cadr expr)
(if (atomic positive-term)
(list positive-term)
(if (real? (cadr positive-term))
(cddr positive-term)
(cdr positive-term))))))
(define (atomic expr)
(or (real? expr)
(symbol? expr)
(not (or (eq? (car expr)
(eq? (car expr)
(eq? (car expr)
(eq? (car expr)
(define (combine-like-terms terms)
;;(when (*debug*) (println "combining: " terms))
(let ([new-factor (foldr (lambda (t acc)
;;(when (*debug*) (println "adding factor: " t))
(+ acc
(cond [(real? t) t]
[(atomic t) 1]
[(and (eq? (car t) '-) (not (pair? (cadr t))))
[(and (eq? (car t) '-) (real? (cadadr t)))
(- (cadadr t))]
[(eq? (car t) '-) -1]
[(real? (cadr t)) (cadr t)]
[#t 1])))
0 terms)])
(cond [(real? (car terms)) (list new-factor)]
[(= 0 new-factor) '()]
[(atomic (car terms)) `((* ,new-factor ,(car terms)))]
[(= 1 new-factor) (if (= 1 (length terms))
(cddar terms)
`((* . ,(cddar terms))))]
[(= -1 new-factor) (list (list '- (if (= 1 (length (cddar terms)))
(caddar terms)
(cons '* (cddar terms)))))]
[#t `((* ,new-factor . ,(cddar terms)))])))
(define (symbol<? sym1 sym2)
(string<? (symbol->string sym1) (symbol->string sym2)))
(define (atom<? a1 a2)
(cond [(and (symbol? a1) (symbol? a2))
(symbol<? a1 a2)]
[(symbol? a1) #f]
[(symbol? a2) #t]
[#t (let ([vars1 (get-contained-vars a1)]
[vars2 (get-contained-vars a2)])
(let loop ([avars vars1] [bvars vars2])
(cond [(and (null? avars) (null? bvars)) #f]
[(null? avars) #t]
[(null? bvars) #f]
[#t (if (eq? (car avars) (car bvars))
(loop (cdr avars) (cdr bvars))
(symbol<? (car avars) (car bvars)))])))]))

0 comments on commit 9c4f0b4

Please sign in to comment.