Commit Graph

20 Commits

Author SHA1 Message Date
Denis Merigoux
7cffc53169
Merge branch 'master' into afromher_334 2023-01-20 14:05:38 -05:00
Louis Gesbert
660e5775de Rename utils to catala_utils 2022-11-28 16:38:09 +01:00
Aymeric Fromherz
cfba9d456a Merge branch 'afromher_verif' into afromher_334 2022-11-16 22:16:11 +01:00
Aymeric Fromherz
fe9ef4f8cb Remove map of free_vars_typ from VC generation 2022-11-16 22:08:07 +01:00
Aymeric Fromherz
5f36bee94f Extend verification_condition with field for assertions in scope 2022-11-08 20:48:43 +01: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
ae2801be6d Move mode handling code from dcalc to shared_ast
Handling code should now be reasonably well sorted between `Shared_ast.{Var,Expr,Scope,Program}`

The function parameters (e.g. `make_let_in`) could be removed from the
scope handling functions since now the types are compatible, which
makes them much easier to read.
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
a7bdc0a114
Add condition for focusing the proof mode on a single scope 2022-03-17 17:44:24 +01: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
777f194178
.mlis and ocamldoc [skip-ci] 2022-01-18 15:13:16 +01:00