Commit Graph

89 Commits

Author SHA1 Message Date
Denis Merigoux
ad02a0959d
Merge branch 'master' into aides_logement_outre_mer 2023-04-03 14:12:10 +02:00
Denis Merigoux
e80143b3ca
Last linting pass and update tests 2023-03-31 17:56:45 +02:00
Denis Merigoux
3d86a12261
Update error messages 2023-03-31 14:01:04 +02:00
Denis Merigoux
04629f58cd
Merge branch 'master' into aides_logement_outre_mer 2023-03-30 15:14:06 +02:00
Aymeric Fromherz
8780a48312 Correct test invocations 2023-03-28 22:51:03 +09:00
Aymeric Fromherz
d0ef61219f Add expected outputs for tests 2023-03-28 13:03:44 +09:00
Aymeric Fromherz
8fdd39d15a Add negative test for let_in 2023-03-28 13:01:41 +09:00
Aymeric Fromherz
71ebd3a2c7 Test for Z3 let_in 2023-03-28 12:49:14 +09:00
Denis Merigoux
bfc827296c
Merge branch 'master' into aides_logement_outre_mer 2023-03-06 14:09:51 +01:00
Louis Gesbert
8200457e43 Syntax change: require declaration of function argument names 2023-02-28 15:53:50 +01:00
Denis Merigoux
21d4360120
Add verification condition special case for scope context arguments 2023-01-20 15:55:28 -05:00
Denis Merigoux
ec6616c091
Changing encoding of direct scope call to avoid empty error confusing static analysis 2023-01-20 15:23:50 -05:00
Denis Merigoux
8405d243be
Fix compiler and tests 2023-01-20 14:10:18 -05:00
Denis Merigoux
7cffc53169
Merge branch 'master' into afromher_334 2023-01-20 14:05:38 -05:00
Louis Gesbert
c94509e0bb Remove integer division from the language
it's unlikely to be used in any law, and likely to be cause for confusion.

best of all, the new operator has a different return type, which
ensures no inconsistency with the change can get overlooked.
2022-12-13 12:35:02 +01:00
Louis Gesbert
71bb67163c Remove explicitely typed operators in tests and examples
Command used: `sed -i 's/\([-+*/><=]=\?\)[.$@^€$]/\1/g' **/*/*.catala_*`

The overload test, of course, is kept unchanged and ensures that explicit
operators still work.
2022-12-13 12:00:04 +01:00
Louis Gesbert
af2f5dbe19 Tweak error message location printing 2022-11-28 16:38:09 +01:00
Aymeric Fromherz
e37ad1de44 Reset tests 2022-11-08 22:28:02 +01:00
Aymeric Fromherz
63572b6963 Add bad test for assertions 2022-11-08 22:27:17 +01:00
Aymeric Fromherz
4af44fb519 Add debug info about encoded assertions 2022-11-08 22:25:07 +01:00
Aymeric Fromherz
9ad7362381 Add testcase from issue 2022-11-08 20:38:09 +01:00
Louis Gesbert
4d4dac6727 Some fancy unicode for error outlines
Normally I would make sure this is not by default, or at leat disableable; but
here the code we print may contain utf8 anyway, so the terminal really needs to
support it. Anyway, it's just a little fancier, doesn't add much.
2022-11-07 14:13:01 +01:00
Louis Gesbert
429911024c Add parseable line-column info to error messages
a quick fix for now, ideally we want an option for editor-friendly output.
But for now this is a very cheap way to at least have clickable error messages
which are a big time-saver.
2022-11-07 14:03:38 +01:00
Louis Gesbert
abd5a4de96 Tests: cleanup remaining whitespace 2022-09-26 14:27:47 +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
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
2c5b3dd25e Add unit tests for extension of Z3 backend to non-bool EMatch nodes 2022-09-13 16:05:33 +02:00
Denis Merigoux
d7e219b0dd
Correct test output for proof mode 2022-09-06 14:10:32 +02:00
Louis Gesbert
2e5050481d Register all existing tests through the new engine
I removed the '.out' extension for now to preserve the test output file names and avoid a million file renames.

This makes the patch easier to read, and we can do the rename easily in another patch afterwards, without mixing with semantic changes.

(beautiful script àlarrache:
```bash
for f in */*/output/*; do
  target_base=${f##*/}
  target_base=${target_base%%.*}
  echo $f | awk -F. '{
    f=$1"."$2; if ($4 == "") { mode=$3; id=$3 } else { scope="-s "$3; mode=$4; id=$3"."$4}
    printf "\n```catala-test {id=\"%s\"}\ncatala %s %s\n```\n",id,mode,scope;
  }' >> $(dirname $f)/../${target_base}.*; done
```
2022-07-08 17:06:20 +02:00
Louis Gesbert
9ef8625df7 Compiler: support cumulative exceptions
Closes #208 (implementing Solution 1, without adding an explicit syntax)

Two exceptions or more, e.g. `(j1 |- c1)` and `(j2 |- c2)` such that `c1
= c2`, are collapsed by this transformation into `((j1 |- c1) | j2 |-
c2)`, introducing an arbitrary precedence that avoids the conflict.

The transormation is not applied if any exceptions apply to the subterms
themselves: while these exceptions could be merged, that would turn more
conflicts into arbitrary outcomes than wanted.
2022-05-30 14:22:34 +02:00
Denis Merigoux
3f49824150
Merge branch 'master' into c_backend 2022-04-04 18:02:33 +02:00
Denis Merigoux
31e8f37a43
Sort VCs by alphabetical order 2022-04-04 17:51:41 +02:00
Denis Merigoux
84144c0a56
Tests now passing except for a few position and printing issues [skip ci] 2022-04-04 12:25:00 +02:00
Aymeric Fromherz
cca2e00d42 [Z3encoding] Add bad unit tests for duration 2022-03-24 17:27:03 +01:00
Aymeric Fromherz
55dd389819 [Z3encoding] Add good unit tests for duration 2022-03-24 17:23:31 +01:00
Aymeric Fromherz
cb36b9d72f [Z3backend] Bad unit tests for EInj node 2022-03-16 12:04:31 +01:00
Aymeric Fromherz
d758170cde [Z3backend] Good unit tests for EInj node 2022-03-16 12:03:24 +01:00
Aymeric Fromherz
bb57abf750 Negative tests for array length encoding 2022-03-16 11:23:36 +01:00
Aymeric Fromherz
123541dc34 Add positive test for array length 2022-03-16 11:21:54 +01:00
Aymeric Fromherz
f5a3a19a09 [Z3 encoding]: Add negative tests for rationals 2022-02-19 02:02:48 +01:00
Aymeric Fromherz
1dc1d6a3b8 Good test for rationals 2022-02-19 02:00:46 +01:00
Aymeric Fromherz
56e3720699 Add unit tests for TUnit 2022-02-17 18:42:22 +01:00
Denis Merigoux
e1dc36f1b1
Merge branch 'master' into io-qualifiers-112-part-2 2022-02-10 22:59:37 +01:00
Denis Merigoux
5004929a51
Fix #193 -- authored with @R1kM
Moved no model generation flag
Fixed bug for VC generation in the IfThenElse case
2022-02-10 16:49:01 +01:00
Denis Merigoux
2263dd7dab
Update syntax highlighting and test suite [skip ci] 2022-02-07 12:04:48 +01:00
Denis Merigoux
13b476d0a1
[skip ci] reorganized desugared to scope encoding, broke some invariants
WIP: fixed some bugs and provided documentations but one thing missing
2022-01-28 17:31:31 +01:00
Denis Merigoux
5e253ba321
Disabling exact counterexamples values from CI testing because of randomness 2022-01-26 16:24:09 +01:00
Aymeric Fromherz
661b30f638 Add bad tests for date_get_year 2022-01-17 15:05:06 +01:00
Aymeric Fromherz
c7fd00702a Fix good get year test + reset [skip ci] 2022-01-17 15:04:05 +01:00
Aymeric Fromherz
cf63e4f3d3 Restore pretty-printing of enum model [skip ci] 2022-01-14 21:10:34 +01:00