Skip to content

Commit

Permalink
Cleanup from terms PR (#176)
Browse files Browse the repository at this point in the history
* add age counter

* working on it

* it builds lol

* trying out new terms proposal

* not working due to cycles lol

* fix up terms

* implement function extraction

* oops

* significant proof checker progress

* some progress

* manual congruence

* Revert "manual congruence"

This reverts commit c578a77.

* proof caching

* fix global variable desugaring

* fixed up primitive computation

* small cleanup

* working on resugar

* resugar in files

* resugar in main

* weird perf behavior

* add resugaring

* fix perf problems with proofs

* fix more prim stuff

* fix proof bug, big refactor

* fix another bug

* magic iteration action

* rebuilding fixes

* simplify terms.rkt

* oops

* working on terms

* builds

* fix desugaring bug

* terms example much simpler

* saturate parent again

* progress on terms desugaring

* more progress

* running into terrible assert failure

* fix another desugar bug

* better term desugaring

* revert rebuilding

* remove unecessary thing

* Fix subtleties in rebuilding

* fix another bug

* bug in function extract

* desugar simplify

* remove old print

* add compiler passes

* a bunch of cleanup

* we need to fix extraction

* tweaks for tutorial example

* oh no bad bug

* fix up fibonacci-demand for terms

* another bug

* let bindings correctly

* add optimization but without canonicalization"

* actually i already did that

* get rid of define, fix bug in terms

* revert let binding encoding

* Revert "revert let binding encoding"

This reverts commit b56cc58.

* filter equality with global variables

* fix saturation bug

* extract based on parent relationship

* don't find value in debug

* extract as an action or query

* desugar set when it should be union

* desugar set to union

* this doesn't work anymore

* some desugaring fixes

* remove a print

* use print-table

* fix another benchmark

* more bug fixes

* clean up

* fix up primitive queries

* another normal form bug

* small test

* fix desugar global variables

* fix bug in vec

* vec tests

* fix bug in filtering for primitives

* rebuild non-eq tables too

* add cache to fact desugaring

* working on rebuild for custom containers"

* fix vec rebuild!

* rebuild for set

* more cleanup

* better error for unbound func

* fix bug in query-extract

* working on fixing extract variants

* fix extract variants actually

* fix bug in term encoding with initialization

* remove some prints

* fix defaults

* better resugaring

* remove prints again

* horrible bug with fail

* fix another global var bug ugh

* another desugar bug

* eq-able containers work better

* working on vec again

* fix find

* unecessary dot

* more desugar fixes for unbound vars

* new desugar tests

* proofs tests no longer relevant

* no longer need presort table

* canonical vars don't need to be updated

* gj intersection sizes from Eli

* resugar checks

* trying to fix parent table

* fix another parent table bug

* working on computable functions in queries

* fix bug in computed funcs

* remove prints

* some cleanup

* revert all the computable stuff

* delete slow test for now

* all tests pass

* remove rebuild and cleanup

* delete random file

* another random file

* remove iteration

* no longer using racket script

* fix minimize script XD

* add yihong's microbenchmark

* Add some query compilation logging

Co-authored-by: Oliver Flatt <oflatt@gmail.com>

* Fix naive saturation

Co-authored-by: Oliver Flatt <oflatt@gmail.com>

* Convert parent tuples to filters

Also push them up in queries.

Co-authored-by: Oliver Flatt <oflatt@gmail.com>

* Fix bug in check GJ instructions

Co-authored-by: Oliver Flatt <oflatt@gmail.com>

* Further refine the query compiler

Co-authored-by: Oliver Flatt <oflatt@gmail.com>

* disable query compiler changes

* more cleanup

* tell query compiler to do top-down

* try more heuristics

* less crazy heuristic

* math micro change to not using match limit for consistency

* simplify

* generate queries as if parent table wasn't there

* remove panic

* print variable costs

* clean up a bit

* cleanup

* re-add rebuilding

* fix a bug with globals

* globals broke seminaive

* timestamps for globals

* fix seminaive for globals

* oops

* some fixes from @ezrosent

* backing out query compiler changes

* more gj back out

* refactor fact desugaring

* remove unneeded arg to primitive apply

---------

Co-authored-by: Eli Rosenthal <ezr@google.com>
Co-authored-by: Max Willsey <me@mwillsey.com>
  • Loading branch information
3 people authored Aug 2, 2023
1 parent 8fa258e commit 8fc012f
Show file tree
Hide file tree
Showing 77 changed files with 2,225 additions and 2,347 deletions.
2 changes: 1 addition & 1 deletion Makefile
Original file line number Diff line number Diff line change
@@ -1,6 +1,6 @@
.PHONY: all web test nits docs serve

RUST_SRC=$(shell find -type f -wholename '*/src/*.rs' -or -name 'Cargo.toml')
RUST_SRC=$(shell find . -type f -wholename '*/src/*.rs' -or -name 'Cargo.toml')
TESTS=$(shell find tests/ -type f -name '*.egg' -not -name '*repro-*')

WWW=${PWD}/target/www/
Expand Down
6 changes: 3 additions & 3 deletions README.md
Original file line number Diff line number Diff line change
Expand Up @@ -180,9 +180,9 @@ defines a named value. This is the same as a 0-arity function with a given, sing

Example:
```
(define one 1)
(define two 2)
(define three (+ one two))
(let one 1)
(let two 2)
(let three (+ one two))
(extract three); extracts 3 as a i64
```

Expand Down
17 changes: 13 additions & 4 deletions scripts/minimize.rkt
Original file line number Diff line number Diff line change
Expand Up @@ -26,7 +26,7 @@
(define ITERATIONS 1)
(define RANDOM-SAMPLE-FACTOR 1)
(define MUST-NOT-STRINGS `())
(define TARGET-STRINGS `("invalid default for"))
(define TARGET-STRINGS `("src/lib.rs:250"))

(define (desugar line)
(match line
Expand All @@ -40,18 +40,16 @@
(define-values (egglog-process egglog-output egglog-in err)
(subprocess (current-output-port) #f #f egglog-binary))

(displayln "(" egglog-in)
(for ([line program])
(writeln (desugar line) egglog-in))
(displayln ")" egglog-in)
(close-output-port egglog-in)

(when (not (sync/timeout TIMEOUT egglog-process))
(displayln "Timed out"))
(subprocess-kill egglog-process #t)
(displayln "checking output")
(flush-output)
(define err-str (read-string 800 err))
(define err-str (read-string 10000 err))
(close-input-port err)
(define still-unsound (and (string? err-str)
(for/and ([must-not-string MUST-NOT-STRINGS])
Expand Down Expand Up @@ -117,7 +115,18 @@
(random-and-sequential program)))
(first (sort programs (lambda (a b) (< (length a) (length b))))))



(define (minimize port-in port-out)
#;((define-values (process out in err) (subprocess #f #f #f "cargo"))
(define err-str (read-string 800 err))
(when (not (string=? err-str ""))
(error err-str))
(close-input-port out)
(close-output-port in)
(close-input-port err)
(subprocess-wait process))

(define egglog (read-lines port-in))
(pretty-print egglog)

Expand Down
Loading

0 comments on commit 8fc012f

Please sign in to comment.