Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

New Term Encoding #158

Closed
wants to merge 152 commits into from
Closed
Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
152 commits
Select commit Hold shift + click to select a range
3082237
add age counter
oflatt Apr 25, 2023
030bc20
working on it
oflatt May 4, 2023
772be1b
it builds lol
oflatt May 5, 2023
fa7f415
trying out new terms proposal
oflatt May 5, 2023
e082fba
not working due to cycles lol
oflatt May 8, 2023
73a454a
fix up terms
oflatt May 8, 2023
2576d72
implement function extraction
oflatt May 16, 2023
aac7758
Merge remote-tracking branch 'mwillsey/main' into oflatt-check-proofs
oflatt May 16, 2023
7bf7f68
oops
oflatt May 16, 2023
851bdb5
significant proof checker progress
oflatt May 16, 2023
514e122
some progress
oflatt May 17, 2023
c578a77
manual congruence
oflatt May 18, 2023
c8dfc13
Revert "manual congruence"
oflatt May 19, 2023
8fef331
proof caching
oflatt May 22, 2023
e07e1e6
fix global variable desugaring
oflatt May 23, 2023
b72d076
fixed up primitive computation
oflatt May 23, 2023
f37c053
small cleanup
oflatt May 23, 2023
2ff44db
working on resugar
oflatt May 24, 2023
85b4dbd
resugar in files
oflatt May 24, 2023
028d5a1
resugar in main
oflatt May 24, 2023
c9d99d4
weird perf behavior
oflatt May 24, 2023
760742a
add resugaring
oflatt May 24, 2023
ad0c885
Merge remote-tracking branch 'mwillsey/main' into oflatt-check-proofs
oflatt May 24, 2023
3a1ac5b
fix perf problems with proofs
oflatt May 24, 2023
251650b
fix more prim stuff
oflatt May 25, 2023
740603e
fix proof bug, big refactor
oflatt May 25, 2023
6d2c96c
fix another bug
oflatt May 25, 2023
f1398fc
magic iteration action
oflatt May 25, 2023
358e5b6
rebuilding fixes
oflatt May 27, 2023
97dffa4
Merge remote-tracking branch 'mwillsey/main' into oflatt-terms
oflatt May 27, 2023
2ced42f
simplify terms.rkt
oflatt May 29, 2023
89722c7
oops
oflatt May 29, 2023
c214aea
working on terms
oflatt May 29, 2023
974ac94
Merge branch 'oflatt-terms' into oflatt-check-proofs
oflatt May 29, 2023
41b8d9b
builds
oflatt May 29, 2023
00553c0
fix desugaring bug
oflatt May 29, 2023
60bdf5d
terms example much simpler
oflatt May 29, 2023
9ed86a3
saturate parent again
oflatt May 29, 2023
b36e536
progress on terms desugaring
oflatt May 29, 2023
fd6a2cb
more progress
oflatt May 30, 2023
ac93a94
running into terrible assert failure
oflatt May 30, 2023
beab8e2
fix another desugar bug
oflatt May 30, 2023
6fca4bb
better term desugaring
oflatt May 30, 2023
8fa87da
revert rebuilding
oflatt May 30, 2023
5a65a4c
remove unecessary thing
oflatt May 30, 2023
ec5b7c2
Fix subtleties in rebuilding
ezrosent May 31, 2023
f827031
Merge remote-tracking branch 'eli/fix_rebuilding' into oflatt-check-p…
oflatt Jun 1, 2023
6087c04
fix another bug
oflatt Jun 1, 2023
844acf9
bug in function extract
oflatt Jun 1, 2023
7b16640
desugar simplify
oflatt Jun 1, 2023
43dc6bf
remove old print
oflatt Jun 1, 2023
1ae0470
add compiler passes
oflatt Jun 1, 2023
ba14ec1
a bunch of cleanup
oflatt Jun 1, 2023
016173e
we need to fix extraction
oflatt Jun 2, 2023
381578e
tweaks for tutorial example
oflatt Jun 7, 2023
c5fba38
Merge remote-tracking branch 'mwillsey/main' into oflatt-check-proofs
oflatt Jun 17, 2023
5df5100
oh no bad bug
oflatt Jun 17, 2023
5c577a2
fix up fibonacci-demand for terms
oflatt Jun 19, 2023
145bcf5
another bug
oflatt Jun 21, 2023
7e6b1bf
let bindings correctly
oflatt Jun 25, 2023
2ed98ee
add optimization but without canonicalization"
oflatt Jun 25, 2023
7051d63
actually i already did that
oflatt Jun 25, 2023
9d6a697
get rid of define, fix bug in terms
oflatt Jun 27, 2023
3d4359c
Merge remote-tracking branch 'mwillsey/main' into oflatt-check-proofs
oflatt Jun 27, 2023
b56cc58
revert let binding encoding
oflatt Jun 28, 2023
6a75838
Revert "revert let binding encoding"
oflatt Jun 28, 2023
82fcefa
filter equality with global variables
oflatt Jun 28, 2023
09970c2
fix saturation bug
oflatt Jun 29, 2023
e4be2f3
Merge branch 'oflatt-fix-saturate' into oflatt-check-proofs
oflatt Jun 29, 2023
a48ab7e
extract based on parent relationship
oflatt Jun 29, 2023
c42f20f
don't find value in debug
oflatt Jun 29, 2023
b35fc6f
extract as an action or query
oflatt Jun 29, 2023
3bd3fc6
desugar set when it should be union
oflatt Jun 29, 2023
014602d
desugar set to union
oflatt Jun 29, 2023
34166fe
this doesn't work anymore
oflatt Jun 29, 2023
0107881
some desugaring fixes
oflatt Jun 30, 2023
1a20c17
remove a print
oflatt Jul 3, 2023
b16986c
use print-table
oflatt Jul 3, 2023
49ea01b
fix another benchmark
oflatt Jul 3, 2023
7cd5c07
more bug fixes
oflatt Jul 3, 2023
6fdd8d4
clean up
oflatt Jul 3, 2023
ebaef6d
fix up primitive queries
oflatt Jul 3, 2023
165b9fa
another normal form bug
oflatt Jul 3, 2023
11a19a5
small test
oflatt Jul 3, 2023
f2bdfbd
fix desugar global variables
oflatt Jul 3, 2023
2d72cb3
fix bug in vec
oflatt Jul 4, 2023
c144d17
vec tests
oflatt Jul 4, 2023
0a099ff
fix bug in filtering for primitives
oflatt Jul 4, 2023
1d8fc26
rebuild non-eq tables too
oflatt Jul 4, 2023
f54c71c
add cache to fact desugaring
oflatt Jul 4, 2023
537709c
working on rebuild for custom containers"
oflatt Jul 5, 2023
f99cb4b
fix vec rebuild!
oflatt Jul 5, 2023
87980ad
rebuild for set
oflatt Jul 5, 2023
4317f73
more cleanup
oflatt Jul 5, 2023
fc26920
better error for unbound func
oflatt Jul 5, 2023
54fcf8f
fix bug in query-extract
oflatt Jul 5, 2023
3fb0749
working on fixing extract variants
oflatt Jul 5, 2023
da28665
fix extract variants actually
oflatt Jul 5, 2023
f77ac65
fix bug in term encoding with initialization
oflatt Jul 6, 2023
f490892
remove some prints
oflatt Jul 6, 2023
772e95d
fix defaults
oflatt Jul 6, 2023
39ff518
better resugaring
oflatt Jul 7, 2023
e0268da
remove prints again
oflatt Jul 7, 2023
28169e6
horrible bug with fail
oflatt Jul 7, 2023
eed65ff
fix another global var bug ugh
oflatt Jul 7, 2023
b1f2751
another desugar bug
oflatt Jul 7, 2023
8687f7b
eq-able containers work better
oflatt Jul 7, 2023
7698927
working on vec again
oflatt Jul 10, 2023
5d8042b
Merge remote-tracking branch 'mwillsey/main' into oflatt-check-proofs
oflatt Jul 12, 2023
9d30e57
fix find
oflatt Jul 12, 2023
642fd7b
unecessary dot
oflatt Jul 12, 2023
f613690
more desugar fixes for unbound vars
oflatt Jul 12, 2023
ed9643b
new desugar tests
oflatt Jul 12, 2023
5f604a4
proofs tests no longer relevant
oflatt Jul 12, 2023
f6efd47
no longer need presort table
oflatt Jul 13, 2023
fa7e52e
canonical vars don't need to be updated
oflatt Jul 13, 2023
557269f
gj intersection sizes from Eli
oflatt Jul 14, 2023
3597d3a
resugar checks
oflatt Jul 14, 2023
9c1651d
trying to fix parent table
oflatt Jul 14, 2023
11a513e
fix another parent table bug
oflatt Jul 15, 2023
aba7771
working on computable functions in queries
oflatt Jul 17, 2023
c144590
fix bug in computed funcs
oflatt Jul 17, 2023
e5b5771
remove prints
oflatt Jul 17, 2023
3a0ad69
some cleanup
oflatt Jul 17, 2023
a99b3ab
revert all the computable stuff
oflatt Jul 17, 2023
1b08b87
delete slow test for now
oflatt Jul 17, 2023
e3a7a35
all tests pass
oflatt Jul 17, 2023
1b74867
remove rebuild and cleanup
oflatt Jul 17, 2023
3dec0c5
delete random file
oflatt Jul 19, 2023
b3b8192
another random file
oflatt Jul 19, 2023
cb752f4
Merge remote-tracking branch 'mwillsey/main' into oflatt-check-proofs
oflatt Jul 20, 2023
ce73bc0
remove iteration
oflatt Jul 20, 2023
4e897cb
no longer using racket script
oflatt Jul 20, 2023
c249579
fix minimize script XD
oflatt Jul 20, 2023
045a0f5
add yihong's microbenchmark
oflatt Jul 20, 2023
3397a24
Add some query compilation logging
mwillsey Jul 20, 2023
4eb5dfe
Fix naive saturation
mwillsey Jul 24, 2023
bb68824
Convert parent tuples to filters
mwillsey Jul 24, 2023
746e355
Fix bug in check GJ instructions
mwillsey Jul 24, 2023
74534bb
Further refine the query compiler
mwillsey Jul 25, 2023
42605e3
disable query compiler changes
oflatt Jul 27, 2023
b3e6536
more cleanup
oflatt Jul 27, 2023
fb554d3
tell query compiler to do top-down
oflatt Jul 27, 2023
f3a3e2a
try more heuristics
oflatt Jul 27, 2023
e49d688
less crazy heuristic
oflatt Jul 27, 2023
f4486cb
math micro change to not using match limit for consistency
oflatt Jul 27, 2023
bc49523
simplify
oflatt Jul 27, 2023
b7b1c1d
generate queries as if parent table wasn't there
oflatt Jul 28, 2023
6de9d40
remove panic
oflatt Jul 28, 2023
0605460
print variable costs
oflatt Jul 31, 2023
4a6c539
clean up a bit
oflatt Jul 31, 2023
98dad42
cleanup
oflatt Jul 31, 2023
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
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