Aymeric Fromherz
cfba9d456a
Merge branch 'afromher_verif' into afromher_334
2022-11-16 22:16:11 +01:00
Aymeric Fromherz
5a5003b22d
Do not pass free_vars to make_context
2022-11-16 21:59:48 +01:00
Aymeric Fromherz
c4756c485c
WIP: Encoding assertions to Z3
2022-11-08 22:09:35 +01:00
Denis Merigoux
d7e219b0dd
Correct test output for proof mode
2022-09-06 14:10:32 +02:00
Louis Gesbert
e10771c187
Make all supertypes use ('a, 't) gexpr as parameter instead of naked_gexpr
2022-08-29 10:57:21 +02:00
Louis Gesbert
a9c8bab2b3
Same treatment for typ and marked_typ
2022-08-29 10:57:21 +02:00
Louis Gesbert
0a23dc526d
Rename marked_expr -> expr, expr -> naked_expr throughout
...
Since the marked kind is used throughout, this should be more clear
2022-08-29 10:57:21 +02:00
Louis Gesbert
d02c02e352
Fix some warnings
2022-08-22 19:28:27 +02:00
Louis Gesbert
06dbab74d2
reformat
2022-08-22 19:28:27 +02:00
Louis Gesbert
2b6ee8dd4b
Leverage the shared AST: big cleanup (part I)
2022-08-22 19:28:21 +02:00
Louis Gesbert
988e5eff1c
Split the shared AST into a separate lib
2022-08-22 19:16:28 +02:00
Louis Gesbert
0b0e774d1c
More factorisation, in particular for variables
2022-08-12 17:18:06 +02:00
Louis Gesbert
97120c4dc2
compiler/verification: force a typed AST as input
2022-07-12 15:57:50 +02:00
Louis Gesbert
18e86621d5
Port verification code to the AST changes
2022-07-11 17:42:34 +02:00
Louis Gesbert
67179a793c
Add type annotations on all AST nodes (first pass)
2022-07-11 16:51:54 +02:00
Louis Gesbert
af0ac95682
Propagate renaming of Pos.mark* into module Marked
...
this patch is just a bunch of `sed` commands
```shell
cd compiler
sed -i 's/Pos.marked/Marked.pos/g' *.ml* **/*.ml*
sed -i 's/Pos.unmark/Marked.unmark/g' *.ml* **/*.ml*
sed -i 's/Pos\.get_position/Marked.get_mark/g' *.ml* **/*.ml*
sed -i 's/Pos\.same_pos_as/Marked.same_mark_as/g' *.ml* **/*.ml*
sed -i 's/Pos\.map_under_mark/Marked.map_under_mark/g' *.ml* **/*.ml*
sed -i 's/Pos\.mark/Marked.mark/g' *.ml* **/*.ml*
sed -i 's/Pos\.compare_marked/Marked.compare/g' *.ml* **/*.ml*
```
2022-07-11 16:51:54 +02:00
Denis Merigoux
5bd66142a6
Big reformatting
...
ocamlformat 0.19.0 -> 0.20.1
100 -> 80 columns per line
Reestablished @emilerolley's smart fun break
2022-03-08 15:03:14 +01:00
Denis Merigoux
a4002fefaf
Finished functorization
2022-01-19 10:17:19 +01:00
Denis Merigoux
bc2742961f
More functors, but still not finished
2022-01-19 10:12:20 +01:00
Denis Merigoux
2f7059c1ac
More functorization
2022-01-19 09:47:08 +01:00
Denis Merigoux
4852891e6c
Added interfaces
2022-01-18 18:59:05 +01:00
