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

WIP: next steps for the meta language #114

Draft
wants to merge 59 commits into
base: main
Choose a base branch
from
Draft
Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
59 commits
Select commit Hold shift + click to select a range
f2635cc
spec: first draft of the new meta-language semantics
zerbina Feb 4, 2025
f67aede
add a small intermediate language
zerbina Feb 4, 2025
1aa1ba8
llm: add built-in list constructors
zerbina Feb 26, 2025
751876d
llm: minor wording adjustment
zerbina Feb 26, 2025
2bc135b
langdefs: rework the language and the macro
zerbina Feb 26, 2025
51477be
implement an interpreter for the meta-language
zerbina Feb 26, 2025
4540762
remove the LLM again
zerbina Feb 26, 2025
490331c
add a 128-bit integer implementation
zerbina Feb 26, 2025
f8b54fe
Merge branch 'main' into meta-language-proof-engine
zerbina Feb 26, 2025
49e27c0
langdefs: fix type checks for sets/maps
zerbina Feb 26, 2025
bfcf92d
langdefs: fix a `fits` crash
zerbina Feb 26, 2025
6843cd6
source: remove the formatting strings
zerbina Feb 26, 2025
3cfe77e
source: remove underscore from function names
zerbina Feb 26, 2025
04a0bb0
source: use `def` for `built_ins`
zerbina Feb 26, 2025
5aa067c
source: remove `len` function
zerbina Feb 26, 2025
7dc80f1
source: add `IntVal` and `FloatVal` to `val`
zerbina Feb 26, 2025
aaf8e92
source: add missing `IntVal`/`FloatVal`
zerbina Feb 26, 2025
ae80e5a
source: fix the `Seq(StringVal(...))` construction
zerbina Feb 26, 2025
fba3f87
source: rename `true`/`false` to `True`/`False`
zerbina Feb 26, 2025
31e6964
source: turn doc comments into comments
zerbina Feb 26, 2025
d73f7ea
source: fix the `substitute` function
zerbina Feb 26, 2025
2044c33
source: fix the `utf8Bytes` signature
zerbina Feb 26, 2025
1fbaf92
source: add `Ident(string)` as `expr` constructor
zerbina Feb 26, 2025
0b044e2
source: fix `UnionTy` pattern
zerbina Feb 26, 2025
1f947c6
source: turn `==` and `!=` into functions
zerbina Feb 26, 2025
aec21f4
source: fix the `C` record type
zerbina Feb 26, 2025
efb931d
source: remove `All` context
zerbina Feb 26, 2025
1cc0fbb
source: remove `elif` usage
zerbina Feb 26, 2025
f33de6c
source: update `S-type-ident`
zerbina Feb 26, 2025
7da4d09
source: update `S-union-type` rule
zerbina Feb 26, 2025
b05f503
source: remove pattern-matching-based type equality in rules
zerbina Feb 26, 2025
3d1fa33
source: use correct `Call`-with-identifier patterns
zerbina Feb 26, 2025
790295f
source: replace wrong usages of `ttypes`
zerbina Feb 26, 2025
336166c
source: fix declaration patterns
zerbina Feb 26, 2025
f5b174e
source: fix record field name
zerbina Feb 26, 2025
14b9000
source: remove `len` usage for sets
zerbina Feb 26, 2025
7a1930c
source: update remaining record construction
zerbina Feb 26, 2025
0ffb3cb
source: replace unsupported map unpack
zerbina Feb 26, 2025
4863d2a
source: use `same` for integer equality
zerbina Feb 26, 2025
b38d86f
source: update `valEq`/`lt`/`lessEqual` implementation
zerbina Feb 26, 2025
6454cfe
source: add a record for the dynamic context
zerbina Feb 26, 2025
36563db
source: allow zero elements for `array`
zerbina Feb 26, 2025
e5aadcc
source: fix wrong integer arithmetic function names
zerbina Feb 26, 2025
02faa93
source: update `substitute` usage
zerbina Feb 26, 2025
44622a8
source: use a repetition for the `Seq` reduction
zerbina Feb 26, 2025
05da6f5
source: fix the `E-string-cons` rule
zerbina Feb 26, 2025
1598ecb
source: replace `exists`
zerbina Feb 26, 2025
5449ef8
source: fix the `E-with` rule
zerbina Feb 26, 2025
5d10e6f
source: add missing `loc` constructors
zerbina Feb 26, 2025
e1c34e4
source: update datatype indexing
zerbina Feb 26, 2025
0682fad
source: fix missing/extraneous unpacking
zerbina Feb 26, 2025
d3a32ae
source: update `S-identifier` rule
zerbina Feb 26, 2025
d998db3
source: make `toplevel` work for `Module`
zerbina Feb 26, 2025
32a2b7f
source: temporarily disable plug pattern in `B`
zerbina Feb 26, 2025
a612e97
source: fix the remaining errors
zerbina Feb 26, 2025
eb6de47
source: fix error in `S-void-short-circuit` rule
zerbina Feb 26, 2025
470dee1
source: remove unused import
zerbina Feb 26, 2025
b28ab56
source: update the module-level documentation
zerbina Feb 26, 2025
22f8a03
koch: make sure the `interpreter` module is compiled
zerbina Feb 26, 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
3 changes: 3 additions & 0 deletions koch.nim
Original file line number Diff line number Diff line change
Expand Up @@ -21,6 +21,9 @@ Commands:
Programs: seq[(string, string, bool, bool)] = @[
("tester", "tools/tester.nim", true, true),
("passtool", "tools/passtool/passtool.nim", true, true),
("interpreter", "spec/interpreter.nim", true, true),
# XXX: ^^ temporarily registered as a program because it would otherwise
# be unused
("repl", "phy/repl.nim", false, true),
("phy", "phy/phy.nim", false, true),
("skully", "skully/skully.nim", true, false)
Expand Down
Loading
Loading