summaryrefslogtreecommitdiff
Commit message (Collapse)AuthorAgeFilesLines
* 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-243-6/+4
| | | | | | | | | 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-172-0/+6
| | | | | | | | `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>
* Merge pull request #126 from RaitoBezarius/scalar-preordersSon HO2024-04-151-0/+10
|\ | | | | lean: scalars form a preorder
| * lean: scalars form a preorderRyan Lahfa2024-04-121-0/+10
| | | | | | | | | | | | | | | | | | | | Via the canonical injection, we can easily define an induced preorder on scalars and inherit all nice properties. It's useful to reason on specific scalar preorders w.r.t. Ordering, see the binary search tree verification example. Signed-off-by: Ryan Lahfa <ryan.lahfa@inria.fr>
* | Merge pull request #127 from AeneasVerif/fix-ciSon HO2024-04-152-2/+5
|\ \ | |/ |/| Fix CI
| * Fix CINadrieril2024-04-152-2/+5
|/
* Merge pull request #124 from AeneasVerif/son/lean1Son HO2024-04-1211-60/+674
|\ | | | | Add more definitions to the Lean library
| * Add more definitions to the Lean librarySon Ho2024-04-125-0/+200
| |
| * Reorganize the files in the Lean backend a bitSon Ho2024-04-125-241/+266
| |
| * Start adding integer functions to the Lean librarySon Ho2024-04-127-58/+447
|/
* Merge pull request #110 from zhassan-aws/checked-opsSon HO2024-04-122-21/+279
|\ | | | | Add builtins for some checked ops for the Lean backend
| * Update the bindings for the extractionSon Ho2024-04-121-14/+11
| |
| * Merge branch 'main' into checked-opsSon Ho2024-04-120-0/+0
| |\ | |/ |/|
* | Merge pull request #123 from AeneasVerif/son/cleanSon HO2024-04-1180-1997/+1989
|\ \ | | | | | | Cleanup the code in preparation of the nested loops
| | * Fix a proofSon Ho2024-04-121-1/+0
| | |
| | * Update the core.num.checked_* definitionsSon Ho2024-04-121-31/+233
| | |
| | * Merge branch 'son/clean' into checked-opsSon Ho2024-04-11117-2327/+2546
| | |\ | | |/ | |/|
| * | Update a Lean fileSon Ho2024-04-111-1/+1
| | |
| * | Update some Lean proofsSon Ho2024-04-113-24/+24
| | |
| * | Update a commentSon Ho2024-04-111-2/+2
| | |
| * | Fix a Coq fileSon Ho2024-04-111-1/+1
| | |
| * | Fix some F* proofsSon Ho2024-04-111-4/+4
| | |
| * | Merge remote-tracking branch 'origin/main' into son/cleanSon Ho2024-04-1140-130/+310
| |\ \ | |/ / |/| |
* | | Merge pull request #121 from AeneasVerif/son/formatSon HO2024-04-111-9/+6
|\ \ \ | | | | | | | | Reformat the code
| * | | Reformat the codeSon Ho2024-04-111-9/+6
|/ / /
* | | Merge pull request #119 from AeneasVerif/generic-copyGuillaume Boisseau2024-04-114-11/+11
|\ \ \
| * | | Use charon mainNadrieril2024-04-112-5/+4
| | | |
| * | | Update a commentSon HO2024-04-111-1/+1
| | | |
| * | | Trust rustc regarding `Copy` boundsNadrieril2024-04-105-11/+12
|/ / /
* | | Merge pull request #115 from AeneasVerif/nixSon HO2024-04-101-0/+7
|\ \ \ | | | | | | | | Update flake.nix
| * | | Update flake.nixNadrieril2024-04-081-0/+7
|/ / / | | | | | | | | | | | | It was missing some dependencies, and while we're at it we can disable sanity checks in tests.
* | | Merge pull request #113 from AeneasVerif/escherichia/error_catching_translateSon HO2024-04-0715-66/+186
|\ \ \ | | | | | | | | Error catching should tell when code couldn't be generated
| * | | Improve the error messages furtherSon Ho2024-04-073-1/+44
| | | |
| * | | Cleanup a bit and improve the error messagesSon Ho2024-04-0712-82/+91
| | | |
| * | | Resolved comments and added the name of the not translated elementEscherichia2024-04-052-7/+18
| | | |
| * | | resolved commentsEscherichia2024-04-053-99/+113
| | | |
| * | | error catching should now be able to tell when code couldn't be generatedEscherichia2024-04-053-101/+144
| | | |
* | | | Merge pull request #114 from AeneasVerif/son/lean-versionSon HO2024-04-0512-36/+36
|\ \ \ \ | |/ / / |/| | | Bump the version of Lean to 4.7.0
| * | | Update the lean toolchain and fix the proofsSon Ho2024-04-0512-36/+36
| | | |
* | | | Merge pull request #106 from AeneasVerif/escherichia/error_catchingSon HO2024-04-0413-9/+54
|\ \ \ \ | | | | | | | | | | Added Error and EError to expressions and propagated related changes
| * | | | Fix a minor issueSon Ho2024-04-041-1/+1
| | | | |
| * | | | Merge remote-tracking branch 'origin/main' into escherichia/error_catchingSon Ho2024-04-0445-396/+446
| |\ \ \ \
| * | | | | Update the way errors are reportedSon Ho2024-04-042-10/+7
| | | | | |
| * | | | | Update the nix flakeSon Ho2024-04-041-3/+3
| | | | | |
| * | | | | Now prints all errors in the error_listEscherichia2024-04-042-3/+11
| | | | | |
| * | | | | Merge remote-tracking branch 'origin/main' into escherichia/error_catchingEscherichia2024-04-043-5/+2
| |\ \ \ \ \
| * | | | | | resolved requested changesEscherichia2024-04-031-1/+0
| | | | | | |
| * | | | | | resolved requested changesEscherichia2024-04-033-6/+4
| | | | | | |
generated by cgit v1.2.3 (git 2.25.1) at 2024-10-21 01:41:57 +0000