summaryrefslogtreecommitdiff
path: root/compiler/ExtractBuiltin.ml (follow)
Commit message (Collapse)AuthorAgeFilesLines
* Add an option to run Aeneas as a borrow checkerSon Ho2024-06-051-11/+13
|
* Factor out code in ExtractBuiltin.mlSon Ho2024-05-291-162/+122
|
* Update compiler/ExtractBuiltin.mlSon HO2024-04-261-1/+1
| | | Co-authored-by: Zyad Hassan <88045115+zhassan-aws@users.noreply.github.com>
* Update the backend and ExtractBuiltin.mlSon Ho2024-04-251-1/+4
|
* Merge branch 'main' into core-option-unwrapSon Ho2024-04-251-0/+25
|\
| * compiler: introduce Lean-only translationsRyan Lahfa2024-04-241-10/+25
| | | | | | | | | | | | | | | | | | | | On the long run, all backends will not have equivalent or equal support for extraction. This introduces a function to filter out some Lean-only definitions in our various arrays of core functions. Signed-off-by: Ryan Lahfa <ryan.lahfa@inria.fr>
| * compiler: map `core::option::Option::is_none` to `Option.isNone`Ryan Lahfa2024-04-241-0/+4
| | | | | | | | | | | | | | | | | | Our backend already have support for `isNone`, we just map it and filter out passing the actual type as it can be inferred via implicit types. Other backends than Lean are not done in this commit. Signed-off-by: Ryan Lahfa <ryan.lahfa@inria.fr>
| * compiler: map `core::mem::swap` to the pure swapRyan Lahfa2024-04-241-0/+2
| | | | | | | | | | | | | | | | | | In the pure functional model, `swap` is mostly about borrow checking and should simplify to the pure swap in our backends. Other backends than Lean are not done in this commit. Signed-off-by: Ryan Lahfa <ryan.lahfa@inria.fr>
| * compiler: map `core::option::Option::take` to identity functionRyan Lahfa2024-04-171-0/+4
| | | | | | | | | | | | | | | | `take` in a pure functional model is the identity function and everything related to borrow checking is handled by the forward/backward mechanism. Signed-off-by: Ryan Lahfa <ryan.lahfa@inria.fr>
* | Add core::option::unwrap builtinZyad Hassan2024-04-241-0/+2
|/
* Add more definitions to the Lean librarySon Ho2024-04-121-0/+73
|
* Start adding integer functions to the Lean librarySon Ho2024-04-121-47/+142
|
* Update the bindings for the extractionSon Ho2024-04-121-14/+11
|
* Add builtins for some checked ops such as checked_addZyad Hassan2024-04-031-0/+31
|
* Update a builtin nameSon Ho2024-03-111-1/+1
|
* Update the builtin name patternsSon Ho2024-03-101-23/+66
|
* Make progress on propagating the changesSon Ho2024-03-081-6/+5
|
* Remove the option to split fwd/back functions and update SymbolicToPureSon Ho2024-03-081-87/+44
|
* Update the library for F*Son Ho2023-12-221-0/+8
|
* Add the alloc::string::String type in the builtinsSon Ho2023-11-241-3/+12
|
* Make a minor modificationSon Ho2023-11-221-2/+3
|
* Use NameMatcher.NameMatcherMap instead of associative listsSon Ho2023-11-221-5/+14
|
* Reorganize the "Extract" filesSon Ho2023-11-211-15/+10
|
* Update more namesSon Ho2023-11-211-6/+7
|
* Fix issues with the builtin namesSon Ho2023-11-211-48/+83
|
* Fix minor issuesSon Ho2023-11-201-3/+5
|
* Fix minor issuesSon Ho2023-11-201-2/+0
|
* Use the name matcher implemented in CharonSon Ho2023-11-201-260/+134
|
* Start updating the name type, cleanup the names and the module abbrevsSon Ho2023-11-151-3/+10
|
* Make the traits work for CoqSon Ho2023-11-091-1/+11
|
* Make minor modifications and update the array test for F*Son Ho2023-10-261-1/+4
|
* Fix some issues and regenerate the HashmapMain example for LeanSon Ho2023-10-261-1/+10
|
* Improve the handling of saved function effects in ExtractBuiltin.mlSon Ho2023-10-261-13/+27
|
* Make progress on fixing the extractionSon Ho2023-10-261-8/+24
|
* Improve ExtractBuiltin.mlSon Ho2023-10-261-37/+49
|
* Fix more issues at extraction and factor out defs in ExtractBuiltinSon Ho2023-10-261-260/+143
|
* Make the hashmap files typecheck again in LeanSon Ho2023-10-251-347/+162
|
* Fix some issues at extraction and add builtinsSon Ho2023-10-251-5/+299
|
* Handle properly the builtin, non fallible functionsSon Ho2023-10-241-1/+33
|
* Start taking into account non-fallible functions like core::mem::replaceSon Ho2023-10-241-0/+8
|
* Fix minor issuesSon Ho2023-10-241-4/+4
|
* Filter some type arguments for the builtin types/functionsSon Ho2023-10-241-8/+7
|
* Add support for builtin trait implementationsSon Ho2023-10-241-0/+34
|
* Fix various issues with the builtinsSon Ho2023-10-241-20/+62
|
* Make progress on handling the builtinsSon Ho2023-10-231-42/+51
|
* Remove some assumed types and add more support for builtin definitionsSon Ho2023-10-231-0/+468
generated by cgit v1.2.3 (git 2.25.1) at 2024-10-18 17:28:24 +0000