Skip to content

Scheme immutable lists/pairs and proof refactor #1194

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.

Sign up for GitHub

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

Merged
merged 10 commits into from
Jul 20, 2025
Merged

Scheme immutable lists/pairs and proof refactor #1194

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
10 commits
Select commit Hold shift + click to select a range
483412c
start proof refactor
pylasnier Jul 2, 2025
a3f2832
lists, verified but bare and missing some stuff
pylasnier Jul 10, 2025
34faa32
proof refactor, start of lists
pylasnier Jul 11, 2025
2f1875c
HOL changes
pylasnier Jul 11, 2025
8af456c
lambda list semantics, progress
pylasnier Jul 14, 2025
b61c742
compile and proven lambda lists
pylasnier Jul 16, 2025
83bf740
factor out nested constructor rels
pylasnier Jul 16, 2025
46a5312
pair and null testing
pylasnier Jul 16, 2025
00ff2d3
list length example
pylasnier Jul 16, 2025
d15e185
Merge branch 'master' into scheme
pylasnier Jul 16, 2025
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 compiler/scheme/examples/Makefile
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -12,7 +12,7 @@ else
EVALFLAG = -DEVAL
endif

CAKEOPT = --sexp=true
CAKEOPT = --sexp=true --call=false --skip_type_inference=true

ifeq ($(OS),Darwin)
# These options avoid linker warnings on macOS
Expand Down
14 changes: 5 additions & 9 deletions compiler/scheme/examples/list.scm
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,9 +1,5 @@
(letrec (
(cons (lambda (car cdr) (lambda (b) (if b car cdr))))
(car (lambda (cons) (cons #t)))
(cdr (lambda (cons) (cons #f)))
(nil 999)
(nil? (lambda (l) (eqv? l nil)))
(length (lambda (l) (if (nil? l) 0 (+ 1 (length (cdr l))))))
(index (lambda (n l) (if (eqv? n 0) (car l) (index (- n 1) (cdr l)))))
) (index 1 (cons 10 (cons 20 (cons 30 nil)))))
(letrec
((length (lambda (x)
(if (null? x) 0
(+ 1 (length (cdr x)))))))
((lambda x (length x)) 1 2 3 5 5 5 5))
Loading