Commit Graph

342 Commits

Author SHA1 Message Date
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
c07bab1377
FIXME -> TODO 2022-03-08 14:55:48 +01:00
Louis Gesbert
12ec65601d Use format strings directly in debug/error/log functions
This avoids many intermediate calls to e.g. `Format.asprintf`; should result in
some cases in "more correct" use of `Format`¹, avoid the computation of unused
debug strings, and make the code more readable.

¹ for `Format` to work as expected, all intermediate calls need to go through
it. Some cases of formatting to an intermediate string then printing through Format
again are still present, but this makes the situation better.
2022-03-08 13:04:27 +01:00
Denis Merigoux
1a7fb349eb
Merge branch 'master' into variable_state_114 2022-03-07 11:59:49 +01:00
Denis Merigoux
23766e34a9
More negative tests 2022-03-07 11:55:26 +01:00
Denis Merigoux
b9f46afcd7
Revert ocamlformat changes; creates too much conflict in other files
Changes in autoformatting should be made in a separate PR in a time where
there isn't too much pending PRs for the OCaml files
2022-03-07 11:09:47 +01:00
Denis Merigoux
8167d7ee00
Simple tests 2022-03-06 17:13:40 +01:00
Emile Rolley
7d12b5f9f1
Merge branch 'master' into refactor-clerk-w-ninja 2022-03-06 15:02:42 +01:00
Denis Merigoux
5ef7e45e11
Desugared to scope complete but untested [skip ci] 2022-03-06 14:15:09 +01:00
Denis Merigoux
cf8c6233d9
Finished translation of expressions [skip ci] 2022-03-01 20:41:01 +01:00
Denis Merigoux
5a0719b25d
Starting to translate expressions [skip ci] 2022-03-01 10:15:44 +01:00
Denis Merigoux
171e8932bc
Desugaring implemented [skip ci] 2022-02-28 18:34:32 +01:00
Denis Merigoux
518ff02696
Added desugared AST, necessary to distinguish Desugared.ScopeVar from Scopelang.ScopeVar [skip ci] 2022-02-28 17:19:39 +01:00
Denis Merigoux
1e11f6c1d5
Name resolution 2022-02-28 15:40:19 +01:00
Denis Merigoux
eb7f00f56d
Syntax: parser and highlighting 2022-02-28 14:33:07 +01:00
Emile Rolley
b0829148c7 format: add break-fun-decl in .ocamlformat 2022-02-26 19:53:56 +01:00
Emile Rolley
3a6450b42f Merge branch 'master' into refactor-clerk-w-ninja 2022-02-25 12:31:16 +01:00
Denis Merigoux
09dd02c8a0
Python backend works with exceptions avoided
Few bugs in Lcalc->Scalc fixed
2022-02-25 12:30:34 +01:00
Denis Merigoux
ddacc94de2
Correct types for make_some and make_none 2022-02-24 16:50:01 +01:00
Denis Merigoux
c65c38a2d5
Correct flag for enabling optimization 2022-02-24 16:46:02 +01:00
Denis Merigoux
756e7cb9b2
Merge branch 'master' into alain_default-option 2022-02-24 16:41:35 +01:00
Aymeric Fromherz
908be78d32
Merge pull request #205 from CatalaLang/afromher_rationals
Add support for rationals in Z3 encoding
2022-02-21 15:44:02 +01:00
Aymeric Fromherz
a463ec7db2 Use Cli.max_prec_digits 2022-02-21 14:54:40 +01:00
Alain
73fe2f876c Revert "Merge pull request #196 from CatalaLang/fixup-cmdliner"
fix cmdliner to 1.0.4

This reverts commit 8e1a1ccb63, reversing
changes made to 4812830a25.
2022-02-21 14:53:48 +01:00
Alain
4ee9b71e00 to_lcalc option type printing 2022-02-21 11:58:26 +01:00
Alain
f7b70b8f19 add typing information to make_none and make_some 2022-02-21 11:55:39 +01:00
Alain
6fe75f3486 fv --> free_vars_set
free_vars --> free_vars_list
2022-02-21 11:51:01 +01:00
Aymeric Fromherz
63704324c1 [Z3 Backend] Better error message when function has type TAny 2022-02-19 23:28:04 +01:00
Aymeric Fromherz
31c2adf0f1 Z3 Backend: Extend arithmetic operations to money 2022-02-19 23:18:23 +01:00
Aymeric Fromherz
25ff8c50fb [Z3 Backend]: Add support for rationals 2022-02-19 01:59:34 +01:00
Alain
d7b9aa9492 fixing if-then-else bug 2022-02-18 16:11:22 +01:00
Alain
5c9996e427 more comment 2022-02-18 15:59:35 +01:00
Alain
4b1f235e6c util review (bis) 2022-02-18 15:56:36 +01:00
Alain
f54b3b317c review lcalc 2022-02-18 15:55:37 +01:00
Alain
137fb8c552 util review 2022-02-18 15:54:40 +01:00
Alain
d512b27e2c fmt 2022-02-18 15:49:23 +01:00
Alain
7e1057c541 review of lcalc 2022-02-18 15:47:54 +01:00
Alain
19bf2d934f dcalc review 2022-02-18 15:31:52 +01:00
Aymeric Fromherz
dd05e4468b [Z3backend]: Do not crash when trying to print function model 2022-02-18 00:34:42 +01:00
Aymeric Fromherz
6dec7bfe04 Refactor Z3 print_model: get_const_interp is only usable for non-function expressions 2022-02-18 00:28:36 +01:00
Aymeric Fromherz
d776a10e5f format 2022-02-17 18:44:40 +01:00
Aymeric Fromherz
378ab4697a Encode TUnit in Z3 2022-02-17 18:34:30 +01:00
Emile Rolley
351c7346d6 refactor(clerk): factorize functions for building ninja rules
+ add "test cases" for Lcalc and Scalc backends.
	+ add support for Scalc and Lcalc and sort by alphabetical
	  order their type declarations.
2022-02-17 16:45:49 +01:00
Denis Merigoux
9fcc79a66f
Fix bug for encoding verification conditions from Dcalc, coming from #189 2022-02-15 17:58:18 +01:00
Denis Merigoux
48f064ccea
Adapt translation to new i/o invariants, bug discovered 2022-02-15 11:38:56 +01:00
Denis Merigoux
cab4e5c17e
Merge branch 'master' into alain_default-option 2022-02-15 10:20:53 +01:00
Denis Merigoux
21c73edfc9
Link to modules in the docs 2022-02-14 18:27:29 +01:00
Denis Merigoux
1cec4b0721
Pretty-printer for scalc 2022-02-14 18:22:26 +01:00
Denis Merigoux
b25f64c3ae
Improve printing 2022-02-14 17:01:34 +01:00
Denis Merigoux
69a7465339
Merge branch 'master' into alain_default-option 2022-02-14 12:09:11 +01:00