Commit Graph

2506 Commits

Author SHA1 Message Date
Louis Gesbert
abd5a4de96 Tests: cleanup remaining whitespace 2022-09-26 14:27:47 +02:00
Louis Gesbert
3ceb9ec80c Clerk: don't stop on 1st error on tests 2022-09-26 14:24:49 +02:00
Louis Gesbert
c18de3b980 Tweak the order in which typing is done 2022-09-26 14:11:25 +02:00
Louis Gesbert
76569bb1af Fix position on type error concerning sub-scope variable 2022-09-26 14:11:25 +02:00
Louis Gesbert
498429e4b7 Fix type-checking error getting delayed
The issue was coming from Bindlib: it stores variable bindings as closures, so
`Bindlib.box_apply f bx` actually delays the application of `f` until the term
is substituted or unboxed (likely long after we are out of the `try..with`
block).

The proposed fix is to make sure we run the wrapper outside of bindlib
applications, on explicitely unboxed terms.
2022-09-26 14:11:25 +02:00
Louis Gesbert
8bf6b5b821 Type arrow return types first 2022-09-26 14:11:25 +02:00
Louis Gesbert
2c3be946ec Keep type positions on the right-hand side upon unification of types
This should result in more predictable error messages. Right-hand is arbitrary,
but has been found empirically to give better results.
2022-09-26 14:11:25 +02:00
Louis Gesbert
43e4efeeb8 Some typing error tests improvements 2022-09-26 14:11:25 +02:00
Catala nix updated
e53f6b6087 update lock files 2022-09-26 00:28:43 +00:00
Louis Gesbert
84c1063509
Change the clerk tests to use inline output (#340) 2022-09-23 17:06:05 +02:00
Louis Gesbert
8c1696d0ff Inline tests: cleanup trailing whitespace 2022-09-23 16:56:21 +02:00
Louis Gesbert
fe6fabb1b0 Clerk tests: update README 2022-09-23 16:41:22 +02:00
Louis Gesbert
005de24ee7 Inline tests: ensure proper escaping of output
and that the input is not truncated with --reset
2022-09-23 14:52:04 +02:00
Louis Gesbert
0c0ef1ae1a Add test return codes
Simply re-generated with 'make tests CLERK_OPTS=--reset'
2022-09-23 14:50:02 +02:00
Louis Gesbert
0ab7a0f9ce Turn all existing tests to inline tests
Done using
```bash
process() { FILE=$1; awk 'match($0, /^```catala-test *{ *id *= *"(.*)" *}/, a) {print "```catala-test-inline"; f="'"$(dirname $FILE)/output/$(basename $FILE)"'." a[1]; getline; print "$ " $0; while ((getline<f) > 0) print; next} {print}' $FILE >$FILE.new; mv $FILE.new $FILE; }
for f in tests/test_*/*/*.catala_* examples/**/*.catala_*; do process $f; git add $f; done
for d in $(find -name output -type d); do git rm -r $d; done
```
2022-09-23 14:45:10 +02:00
Louis Gesbert
b9c0453fc9 Clerk tests: add ability to have tests with inlined output
Reduces the number of files, and makes tracking and diffing tests much easier.
2022-09-23 13:50:56 +02:00
Denis Merigoux
19beb91262
gnu gedit syntax highlighting (#336) 2022-09-20 14:37:12 +02:00
Denis Merigoux
754174390b
Merge branch 'master' into yueli_master 2022-09-20 12:01:11 +02:00
Louis Gesbert
58f7e6bab8
Clerk: don't default to infinite ninja jobs (#337) 2022-09-20 11:51:37 +02:00
Louis Gesbert
6cb8ee7916 Clerk: don't default to infinite ninja jobs 2022-09-20 11:30:29 +02:00
Denis Merigoux
c7f07435fc
Moved doc around 2022-09-20 10:50:43 +02:00
Denis Merigoux
cc8c460fb3
Remove chinese language support as it is not yet supported by the compiler 2022-09-20 10:44:46 +02:00
YueLiPicasso
9c3b001f21 gnu gedit syntax highlighting 2022-09-20 16:15:46 +08:00
Denis Merigoux
f1d0831d86
LégiFrance<->Catala connector (#329) 2022-09-19 11:14:21 +02:00
Catala nix updated
fbd6b07372 update lock files 2022-09-19 00:26:12 +00:00
Louis Gesbert
1b97f55c00 Add a few tests on typing errors
the `err6` test also highlights that Typecheck errors get overly delayed
2022-09-15 17:28:05 +02:00
Aymeric Fromherz
e7c3ef604e
Do not hardfail when pretty-printing unknown Z3 variables (#333)
This PR extends PR #331, by avoiding hard failures when pretty-printing
a Z3 model when generating a counterexample.
#331 added some Z3 variables to encode EMatch nodes that are only used
internally in the encoding, and do not correspond to any source
variable. When trying to retrieve the source variable corresponding to
this Z3 variable for pretty-printing purposes (stored in a map in the
context, called ctx.z3_vars), we thus had a hard OCaml failure due to a
Not_found exception.

This PR fixes this by ignoring internal variables during pretty-printing
of the counterexample. It also adds some unit tests for #331, although,
since counterexample generation is disabled in tests/, this specific
issue would not have been caught.

Fixes #332
2022-09-13 20:20:56 +02:00
Aymeric Fromherz
2c5b3dd25e Add unit tests for extension of Z3 backend to non-bool EMatch nodes 2022-09-13 16:05:33 +02:00
Aymeric Fromherz
7f07274c1f Ignore unfound (i.e., internal) variables during Z3 model printing 2022-09-13 15:54:26 +02:00
Denis Merigoux
99627ff3dc
Better Z3 encoding of EMatch nodes (#331)
Now that #272 was merged and that type information is available at every
AST node, this PR improves the Z3 encoding of pattern matching in the
verification backend. To do so, it implements the second solution
presented in #241.

Fixes #241
2022-09-13 11:49:55 +02:00
Aymeric Fromherz
fee64d6f6f format 2022-09-13 10:37:30 +02:00
Aymeric Fromherz
b7854eb6f3 Z3Backend: Use type information inside AST node for match translation 2022-09-13 10:33:02 +02:00
Aymeric Fromherz
ea13981c5d Match annotation type in io.mli and in Z3 backend 2022-09-12 18:10:02 +02:00
Aymeric Fromherz
0592cdab2a Z3encoding: Use auxiliary variable for encoding type-generic EMatch 2022-09-12 17:52:55 +02:00
Catala nix updated
f6840f45b3 update lock files 2022-09-12 00:25:43 +00:00
Denis Merigoux
6e64f769a0
Update assets and rename executable 2022-09-08 15:16:39 +02:00
Denis Merigoux
a4207c9d9e
Last corrections 2022-09-08 14:54:02 +02:00
Denis Merigoux
1df20c18ac
Fixing discrepancies with LegiFrance in French housing benefits 2022-09-08 12:30:16 +02:00
Denis Merigoux
3188ac5e13
Starting to fix diffs 2022-09-07 17:51:48 +02:00
Denis Merigoux
dba9b40ff6
Restore diff checking 2022-09-07 17:51:41 +02:00
Denis Merigoux
3accabe03a
Update assets 2022-09-07 17:26:40 +02:00
Denis Merigoux
3756a6fb22
Fix french housing benefits 2022-09-07 17:14:36 +02:00
Denis Merigoux
8445174a5b
Improvements to expiration checking 2022-09-07 17:14:22 +02:00
Denis Merigoux
0670dd697f
Correct expiration checking 2022-09-07 13:03:12 +02:00
Denis Merigoux
09fc71c625
Differenciating API requests depending on text ID (beginning) 2022-09-06 18:32:26 +02:00
Denis Merigoux
19ba5ce923
Don't process everything at the same time 2022-09-06 18:00:22 +02:00
Denis Merigoux
1990b0b970
Code compiles 2022-09-06 17:25:57 +02:00
Denis Merigoux
2ffafdbd3a
Bring back files from ancient git history 2022-09-06 15:56:36 +02:00
Denis Merigoux
166f0a732d
Opam update for static binaries 2022-09-06 14:42:45 +02:00
Denis Merigoux
0e3616d8ef
Update assets 2022-09-06 14:27:56 +02:00