183 Commits

Author	SHA1	Message	Date
Denis Merigoux	11d4a34783	Better printing, tests, fix parser ommission	2022-02-04 15:10:47 +01:00
Denis Merigoux	d8c120bf97	Propagate visibility down, missing handling in scope_to_dcalc	2022-02-04 14:41:22 +01:00
Denis Merigoux	0d90dcea00	Better optimizations with values instead of literals	2022-02-02 10:30:39 +01:00
Denis Merigoux	6cf1b768d2	Fix bug in Python backend producing unreachable code	2022-02-01 15:41:53 +01:00
Denis Merigoux	8ad752eba5	Type refactoring in scope_to_dcalc	2022-01-31 18:09:14 +01:00
Denis Merigoux	edeba14692	Just typechecking for compiler	2022-01-31 15:28:19 +01:00
Denis Merigoux	effc2b24e4	Optimizations for defaults in Dcalc	2022-01-31 15:27:58 +01:00
Denis Merigoux	73ce2f142f	Fixed last bug around rule refactoring	2022-01-31 13:55:25 +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	0a9e6db5f4	Fix UTF8 lexing. ... By what magic did it work until now?	2022-01-28 11:09:44 +01:00
Denis Merigoux	05a0bfc9b7	Added parsing support for #112, missing all later compilation steps	2022-01-27 18:03:47 +01:00
Denis Merigoux	228330d0cf	Fix	2022-01-26 17:15:06 +01:00
Denis Merigoux	5e253ba321	Disabling exact counterexamples values from CI testing because of randomness	2022-01-26 16:24:09 +01:00
Denis Merigoux	f7f010a902	Update asset and fix missing link in doc	2022-01-21 20:16:07 +01:00
Denis Merigoux	42d79e5169	Merge branch 'master' into proof_platform	2022-01-21 09:55:34 +01:00
Denis Merigoux	757c3eddb6	Remove mathematical symbols replacement	2022-01-19 14:43:42 +01:00
Denis Merigoux	54c090289b	Revamped CLI doc	2022-01-19 11:20:25 +01:00
Denis Merigoux	d2977b48ce	Documentation pass	2022-01-19 10:54:16 +01:00
Denis Merigoux	a4002fefaf	Finished functorization	2022-01-19 10:17:19 +01:00
Denis Merigoux	bc2742961f	More functors, but still not finished	2022-01-19 10:12:20 +01:00
Denis Merigoux	2f7059c1ac	More functorization	2022-01-19 09:47:08 +01:00
Denis Merigoux	4852891e6c	Added interfaces	2022-01-18 18:59:05 +01:00
Denis Merigoux	b11e3329b3	Functorize VC solving IO [skip ci]	2022-01-18 18:51:02 +01:00
Denis Merigoux	2e1dc4740a	Restore build [skip ci]	2022-01-18 17:59:15 +01:00
Denis Merigoux	777f194178	.mlis and ocamldoc [skip-ci]	2022-01-18 15:13:16 +01:00
Aymeric Fromherz	400a777891	Support common case for getYear: Comparison against a literal [skip ci]	2022-01-17 15:02:56 +01:00
Aymeric Fromherz	cf63e4f3d3	Restore pretty-printing of enum model [skip ci]	2022-01-14 21:10:34 +01:00
Aymeric Fromherz	2548b4ad5e	Pretty-print structs, temporarily disable pretty-printing of enum model during refactoring [skip ci]	2022-01-14 21:02:34 +01:00
Aymeric Fromherz	0b011a5e3a	Support TTuple type [skip ci]	2022-01-14 20:37:45 +01:00
Aymeric Fromherz	7fa271b9f4	Construct Z3 sort corresponding to a struct [skip ci]	2022-01-14 20:35:22 +01:00
Aymeric Fromherz	89e41b3a33	Encode ETupleAccess node [skip ci]	2022-01-14 20:17:27 +01:00
Aymeric Fromherz	850718be17	Add support for structs in the Z3 encoding context [skip ci]	2022-01-14 20:08:42 +01:00
Aymeric Fromherz	6c749fdbfe	Pretty-print enums in Z3 model [skip ci]	2022-01-14 19:23:26 +01:00
Aymeric Fromherz	06b845316d	Allow match bodies in VCs to refer to the value corresponding to the destructed enum [skip ci]	2022-01-14 19:01:54 +01:00
Aymeric Fromherz	3c21182dea	Finish encoding arms of EMatch in VCs [skip ci]	2022-01-14 18:33:56 +01:00
Aymeric Fromherz	a7abe630e7	More progress towards encoding arms of EMatch in VCs [skip ci]	2022-01-14 18:24:32 +01:00
Aymeric Fromherz	ffee0d815d	Wrap up the find_or_create_enum function [skip ci]	2022-01-14 17:42:12 +01:00
Aymeric Fromherz	7c1e808880	Translate the type TEnum to Z3	2022-01-14 17:42:12 +01:00
Aymeric Fromherz	a1e12a22b1	Create or retrieve Z3 enum types [skip ci]	2022-01-14 17:42:12 +01:00
Aymeric Fromherz	ae0935f035	Z3 encoding: Add a map from enumnames to Z3 sorts to the context [skip ci]	2022-01-14 17:42:12 +01:00
Aymeric Fromherz	1932277c80	Fix printing of negative money amounts [skip ci]	2022-01-14 11:45:47 +01:00
Aymeric Fromherz	951e50637f	Actually plug date pretty printing into Z3 encoding [skip ci]	2022-01-14 02:08:04 +01:00
Aymeric Fromherz	50ad5e3044	Print dates generated by Z3 model [skip ci]	2022-01-14 02:04:55 +01:00
Aymeric Fromherz	977e985e4c	Encode dates to Z3 [skip ci]	2022-01-14 01:54:33 +01:00
Aymeric Fromherz	d89eea0481	Encode comparison operators on money [skip ci]	2022-01-13 20:11:28 +01:00
Aymeric Fromherz	827f5cb916	encode money to Z3 [skip ci]	2022-01-13 20:02:14 +01:00
Aymeric Fromherz	50d0ee0909	Start printing z3 model results according to their type [skip ci]	2022-01-13 19:52:58 +01:00
Denis Merigoux	428ae95c62	[skip ci] Added a walkthrough example for ProLaLa + tweaked tests output order of vcs	2022-01-13 16:58:43 +01:00
Denis Merigoux	5a6f4485e7	Matching subscope variables also [skip ci]	2022-01-13 16:00:09 +01:00
Denis Merigoux	a9454a0aac	Correctly match ignored part of expressions in VC generation [skip ci]	2022-01-13 12:15:37 +01:00