Matteo Manighetti
7ae65be566
Upgrade sessions to use Alt-Ergo 2.6.0
2025-01-14 19:48:35 +01:00
Paul Patault
b7d4770c7d
coma: simplify examples
2024-10-17 20:00:12 +02:00
Andrei Paskevich
523ee1a95a
coma: a properer fix
2024-10-16 12:58:53 +02:00
Andrei Paskevich
c962acdf40
coma: name VC goals "handler'vc" instead of "vc_handler"
2024-10-16 12:46:59 +02:00
Jean-Christophe Filliatre
3e5786b626
binary_search coma: lo <= hi is an invariant
2024-10-10 14:19:22 +02:00
Jean-Christophe Filliatre
ddec251ca7
coma binary_search: alternative version without let
2024-10-10 09:21:37 +02:00
Jean-Christophe Filliatre
44896456ad
coma example: binary search
2024-10-09 19:09:20 +02:00
Paul Patault
bb708cfec0
coma: added examples
2024-08-08 11:09:46 +02:00
Paul Patault
000fd2d347
coma: update stdlib + examples
2024-08-08 11:09:46 +02:00
Paul Patault
bf775596c8
coma: generalize let%attr in let%span
...
+ creusot patches
+ CI patches
2024-08-08 11:09:30 +02:00
Paul Patault
9ef8eabe50
coma: examples of the paper
2024-08-08 09:06:08 +02:00
Andrei Paskevich
b956a79701
coma: weird handlers (wip)
2024-08-08 09:06:08 +02:00
Andrei Paskevich
b8d7dabd30
coma: update examples/coma/asm.coma
2024-08-08 09:06:08 +02:00
Jean-Christophe Filliatre
626ba943e7
coma: assembly code example
2024-08-08 09:06:08 +02:00
Andrei Paskevich
cc48752b42
coma: accept Church's dot in handler applications
...
h x g . fun x -> e is h x g (fun x -> e)
h x g . -> e is h x g (-> e)
h x g . e is h x g (e)
The dot binds stronger than post-definition blocks:
h x g . e [ f -> d ] is h x g (e) [ f -> d ]
In other words, e above can be an application, assertion, assignment
or a parenthesized expression, including (!..) and (?..).
2024-08-08 09:06:08 +02:00
Andrei Paskevich
4ab78a9f61
coma: eliminate trivial equalities more aggressively
2024-08-08 09:06:08 +02:00
Paul Patault
25de89f4cc
coma: tests with polymorphism
2024-08-08 09:06:08 +02:00
Andrei Paskevich
a5cbb9b2fd
coma_logic: test & fix
2024-08-08 09:06:08 +02:00
Andrei Paskevich
cfa3c44778
coma: effect inference
2024-08-08 09:06:08 +02:00
Andrei Paskevich
6be7f4230d
coma: minor
2024-08-08 09:06:08 +02:00
Andrei Paskevich
47da32fdc5
coma: effect inference (wip)
...
coma: effect inference (wip)
2024-08-08 09:06:08 +02:00
Andrei Paskevich
56d73fbc85
examples/re.coma: better spec
2024-08-08 09:06:08 +02:00
Paul Patault
ec40aa57b7
coma: WIP RE
2024-08-08 09:06:08 +02:00
Andrei Paskevich
d6807794a6
coma: restrict the place of preconditions and let-bindings in prototypes
...
Preconditions and let-bindings are not allowed before type and data
parameters. As they are handled before name resolution, moving them
inside the handler body might otherwise provoke an illegal capture.
2024-08-08 09:06:08 +02:00
Andrei Paskevich
c06ff36f93
coma: remove unneeded barriers from re.coma
2024-08-08 09:06:08 +02:00
