summaryrefslogtreecommitdiff
path: root/compiler/PureMicroPasses.ml (follow)
Commit message (Collapse)AuthorAgeFilesLines
* Remove redundant `llbc_name` fieldNadrieril2024-06-281-1/+0
| | | | It's redundant with `item_meta.name`
* Update charonNadrieril2024-06-241-1/+0
|
* Support for renaming using the rename attribute in charon (#239)Escherichia2024-06-181-23/+36
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | * support for renaming using the rename attribute in charon * support for global decl * add support for renaming field * applied suggested changes and began adding support for variant * finished support for renaming variant * applied suggested changes * add tests * fixed variant and field renaming * update charon-pin * update flake.lock * Update the charon pin * Fix an issue with renaming trait method implementations * Fix an issue with the renaming of trait implementations * Fix an issue when renaming enumerations * Update the Charon pin * Fix the F* tests * Fix an issue with the spans for the loops * Fix the tests * Update a comment * Use fuel in the coq tests * Generate the template decreases clauses by default --------- Co-authored-by: Escherichia <escherichia@charlotte> Co-authored-by: Son Ho <hosonmarc@gmail.com>
* Automatically add a @[reducible] attribute to some generated functionsSon Ho2024-06-171-1/+51
|
* Filter out type aliasesNadrieril2024-06-061-1/+1
|
* Add an option to run Aeneas as a borrow checkerSon Ho2024-06-051-2/+2
|
* Rename meta into spanAymeric Fromherz2024-05-241-53/+53
|
* Merge remote-tracking branch 'origin/main' into son/cleanSon Ho2024-04-111-1/+3
|\
| * added Error and EError to expressions and propagated related changesEscherichia2024-04-031-1/+3
| |
* | Update the extractionSon Ho2024-04-041-11/+10
|/
* Cleanup and fix a mistakeSon Ho2024-03-291-0/+1
|
* Add some error messagesSon Ho2024-03-291-4/+4
|
* formatting and changed save_error condition for failing from b to not bEscherichia2024-03-291-2/+5
|
* added file and line arg to craise and cassertEscherichia2024-03-291-11/+11
|
* formattingEscherichia2024-03-281-9/+14
|
* changes after git rebase mainEscherichia2024-03-281-1/+1
|
* Should answer all comments, there are still some TODO: error message leftEscherichia2024-03-281-7/+6
|
* Added sanity_check and sanity_check_opt_meta helpers and changed sanity ↵Escherichia2024-03-281-2/+2
| | | | checks related cassert to these helpers to have a proper error message
* WIP: translate.ml and extract.ml do not compile. Some assert left to do and ↵Escherichia2024-03-281-26/+27
| | | | we need to see how translate_crate can give meta to the functions it calls
* Improve the generation of pretty name and the micro passesSon Ho2024-03-201-13/+38
|
* Improve the pure micro passesSon Ho2024-03-191-8/+46
|
* Fix an issue in PureMicroPasses.filter_loop_inputsSon Ho2024-03-081-13/+43
|
* Make progress on propagating the changesSon Ho2024-03-081-300/+31
|
* Update the micro-passesSon Ho2023-12-231-77/+94
|
* Improve the micro passes to eliminate pattern `let f := fun x => g x`Son Ho2023-12-231-2/+43
|
* Fix the output type of the loops backward functionsSon Ho2023-12-221-22/+3
|
* Improve the pure micro passesSon Ho2023-12-211-3/+33
|
* Improve PureMicroPasses.filter_useless to simplify the matchesSon Ho2023-12-211-1/+14
|
* Implement a micro-pass to simplify the let-bindingsSon Ho2023-12-211-0/+78
|
* Simplify the type of the merged fwd/back functionsSon Ho2023-12-211-3/+4
|
* Remove some asserts which are now uselessSon Ho2023-12-211-3/+0
|
* Fix a minor mistake in SymbolicToPureSon Ho2023-12-181-2/+7
|
* Make progress on updating the codeSon Ho2023-12-151-19/+29
|
* Make progress on propagating the changesSon Ho2023-12-151-55/+55
|
* Make progress on generalizing the signature informationSon Ho2023-12-151-7/+3
|
* Update Pure.fun_sig_infoSon Ho2023-12-131-39/+57
|
* Add the num_fwd_inputs_no_fuel_no_state field in Pure.fun_sigSon Ho2023-12-131-0/+5
|
* Update the micro passes to inline deconstruction of tuples with one fieldSon Ho2023-12-071-6/+34
|
* Use a better syntax when extracting tuple types (structures with unnamed fields)Son Ho2023-12-071-38/+44
|
* Improve further the generation of parent clause/trait clause namesSon Ho2023-11-221-2/+6
|
* Add span information to the generated codeSon Ho2023-11-211-3/+6
|
* Add an `is_local` field to declarationsSon Ho2023-11-211-0/+1
|
* Fix minor issuesSon Ho2023-11-201-53/+13
|
* Update SymbolicToPure.eliminate_box_functionsSon Ho2023-11-161-30/+45
|
* Finish propagating the changes to the names and cleaningSon Ho2023-11-161-12/+17
|
* Add RegionsHierarchy.mlSon Ho2023-11-131-4/+5
|
* Prefix variants related to types with "T"Son Ho2023-11-121-6/+6
|
* Remove the 'r type variable from the ty type definitionSon Ho2023-11-121-5/+5
|
* Start taking into account non-fallible functions like core::mem::replaceSon Ho2023-10-241-5/+7
|
* Remove some assumed types and add more support for builtin definitionsSon Ho2023-10-231-20/+22
|
generated by cgit v1.2.3 (git 2.25.1) at 2024-10-18 17:28:44 +0000