Commit Graph

342 Commits

Author SHA1 Message Date
Aymeric Fromherz
5b345b4782 format 2022-03-08 20:23:45 +01:00
Aymeric Fromherz
2fa2f36c1d Optimize if_then_else when both branches are identical 2022-03-08 17:38:14 +01:00
Aymeric Fromherz
89d69c2316 Implement equality function on dcalc expressions 2022-03-08 17:35:08 +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