summaryrefslogtreecommitdiff
path: root/compiler/PureMicroPasses.ml (unfollow)
Commit message (Expand)AuthorFilesLines
2024-06-28Remove redundant `llbc_name` fieldNadrieril1-1/+0
2024-06-24Update charonNadrieril1-1/+0
2024-06-18Support for renaming using the rename attribute in charon (#239)Escherichia1-23/+36
2024-06-17Automatically add a @[reducible] attribute to some generated functionsSon Ho1-1/+51
2024-06-06Filter out type aliasesNadrieril1-1/+1
2024-06-05Add an option to run Aeneas as a borrow checkerSon Ho1-2/+2
2024-05-24Rename meta into spanAymeric Fromherz1-53/+53
2024-04-04Update the extractionSon Ho1-11/+10
2024-04-03added Error and EError to expressions and propagated related changesEscherichia1-1/+3
2024-03-29Cleanup and fix a mistakeSon Ho1-0/+1
2024-03-29Add some error messagesSon Ho1-4/+4
2024-03-29formatting and changed save_error condition for failing from b to not bEscherichia1-2/+5
2024-03-29added file and line arg to craise and cassertEscherichia1-11/+11
2024-03-28formattingEscherichia1-9/+14
2024-03-28changes after git rebase mainEscherichia1-1/+1
2024-03-28Should answer all comments, there are still some TODO: error message leftEscherichia1-7/+6
2024-03-28Added sanity_check and sanity_check_opt_meta helpers and changed sanity check...Escherichia1-2/+2
2024-03-28WIP: translate.ml and extract.ml do not compile. Some assert left to do and w...Escherichia1-26/+27
2024-03-20Improve the generation of pretty name and the micro passesSon Ho1-13/+38
2024-03-19Improve the pure micro passesSon Ho1-8/+46
2024-03-08Fix an issue in PureMicroPasses.filter_loop_inputsSon Ho1-13/+43
2024-03-08Make progress on propagating the changesSon Ho1-300/+31
2023-12-23Update the micro-passesSon Ho1-77/+94
2023-12-23Improve the micro passes to eliminate pattern `let f := fun x => g x`Son Ho1-2/+43
2023-12-22Fix the output type of the loops backward functionsSon Ho1-22/+3
2023-12-21Improve the pure micro passesSon Ho1-3/+33
2023-12-21Improve PureMicroPasses.filter_useless to simplify the matchesSon Ho1-1/+14
2023-12-21Implement a micro-pass to simplify the let-bindingsSon Ho1-0/+78
2023-12-21Simplify the type of the merged fwd/back functionsSon Ho1-3/+4
2023-12-21Remove some asserts which are now uselessSon Ho1-3/+0
2023-12-18Fix a minor mistake in SymbolicToPureSon Ho1-2/+7
2023-12-15Make progress on updating the codeSon Ho1-19/+29
2023-12-15Make progress on propagating the changesSon Ho1-55/+55
2023-12-15Make progress on generalizing the signature informationSon Ho1-7/+3
2023-12-13Update Pure.fun_sig_infoSon Ho1-39/+57
2023-12-13Add the num_fwd_inputs_no_fuel_no_state field in Pure.fun_sigSon Ho1-0/+5
2023-12-07Update the micro passes to inline deconstruction of tuples with one fieldSon Ho1-6/+34
2023-12-07Use a better syntax when extracting tuple types (structures with unnamed fields)Son Ho1-38/+44
2023-11-22Improve further the generation of parent clause/trait clause namesSon Ho1-2/+6
2023-11-21Add span information to the generated codeSon Ho1-3/+6
2023-11-21Add an `is_local` field to declarationsSon Ho1-0/+1
2023-11-20Fix minor issuesSon Ho1-53/+13
2023-11-16Update SymbolicToPure.eliminate_box_functionsSon Ho1-30/+45
2023-11-16Finish propagating the changes to the names and cleaningSon Ho1-12/+17
2023-11-13Add RegionsHierarchy.mlSon Ho1-4/+5
2023-11-12Prefix variants related to types with "T"Son Ho1-6/+6
2023-11-12Remove the 'r type variable from the ty type definitionSon Ho1-5/+5
2023-10-24Start taking into account non-fallible functions like core::mem::replaceSon Ho1-5/+7
2023-10-23Remove some assumed types and add more support for builtin definitionsSon Ho1-20/+22
2023-10-20Start updating to handle function pointersSon Ho1-16/+16
generated by cgit v1.2.3 (git 2.25.1) at 2024-10-19 09:35:36 +0000