Commit message (Collapse) | Author | Age | Files | Lines | |
---|---|---|---|---|---|
* | Merge branch 'main' into core-option-unwrap | Son Ho | 2024-04-25 | 37 | -238/+1491 |
|\ | |||||
| * | Merge pull request #135 from RaitoBezarius/option-take | Son HO | 2024-04-25 | 36 | -258/+1489 |
| |\ | | | | | | | compiler: add `core::option::Option::{take, is_none}` and `core::mem::swap` support | ||||
| | * | Regenerate the Primitives files | Son Ho | 2024-04-25 | 13 | -0/+975 |
| | | | |||||
| | * | Update the flake.lock | Son Ho | 2024-04-25 | 1 | -15/+15 |
| | | | |||||
| | * | Update the tests for External | Son Ho | 2024-04-25 | 20 | -237/+470 |
| | | | |||||
| | * | Merge branch 'main' into option-take | Son Ho | 2024-04-25 | 29 | -605/+523 |
| | |\ | | |/ | |/| | |||||
| | * | compiler: introduce Lean-only translations | Ryan Lahfa | 2024-04-24 | 1 | -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 Lahfa | 2024-04-24 | 1 | -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 swap | Ryan Lahfa | 2024-04-24 | 3 | -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 function | Ryan Lahfa | 2024-04-17 | 2 | -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> | ||||
* | | | Fix a couple of tests | Zyad Hassan | 2024-04-24 | 4 | -13/+4 |
| | | | |||||
* | | | Update tests | Zyad Hassan | 2024-04-24 | 7 | -44/+0 |
| | | | |||||
* | | | Add core::option::unwrap builtin | Zyad Hassan | 2024-04-24 | 4 | -5/+15 |
|/ / | |||||
* | | Merge pull request #156 from RaitoBezarius/orders | Son HO | 2024-04-23 | 1 | -0/+15 |
|\ \ | | | | | | | feat(backends/lean): scalars form a linear order | ||||
| * | | feat(backends/lean): scalars form a linear order | Ryan Lahfa | 2024-04-23 | 1 | -0/+15 |
| | | | | | | | | | | | | | | | | | | | | | More than c1c33de8, actually, scalars form a linear order with a decidable ≤ operation which is induced by the integer (Z) model. Signed-off-by: Ryan Lahfa <ryan.lahfa@inria.fr> | ||||
* | | | Merge pull request #154 from AeneasVerif/ci-fmt | Son HO | 2024-04-23 | 3 | -2/+23 |
|\ \ \ | | | | | | | | | ci: check code formatting and forbid warnings | ||||
| * | | | Typo | Guillaume Boisseau | 2024-04-23 | 1 | -1/+1 |
| | | | | | | | | | | | | Co-authored-by: Son HO <hosonmarc@gmail.com> | ||||
| * | | | ci: Forbid compilation warnings | Nadrieril | 2024-04-22 | 1 | -0/+1 |
| | | | | |||||
| * | | | ci: check code formatting | Nadrieril | 2024-04-22 | 3 | -2/+22 |
| | | | | |||||
* | | | | Merge pull request #155 from AeneasVerif/dedup-ci | Son HO | 2024-04-23 | 1 | -0/+22 |
|\ \ \ \ | |/ / / |/| | | | ci: avoid running duplicate jobs | ||||
| * | | | ci: avoid running duplicate jobs | Nadrieril | 2024-04-22 | 1 | -0/+22 |
|/ / / | |||||
* | | | Merge pull request #151 from AeneasVerif/son/fix-loops2 | Son HO | 2024-04-22 | 6 | -35/+80 |
|\ \ \ | | | | | | | | | Fix an issue in the loops fixed point | ||||
| * | | | Fix an issue when joining a symbolic value with bottom | Son Ho | 2024-04-22 | 2 | -11/+33 |
| | | | | |||||
| * | | | Reformat some files | Son Ho | 2024-04-22 | 5 | -24/+47 |
|/ / / | |||||
* | | | Merge pull request #132 from AeneasVerif/regen-tests | Son HO | 2024-04-19 | 10 | -15/+10 |
|\ \ \ | | | | | | | | | Ensure we regenerate files properly in CI | ||||
| * | | | Address review comments | Nadrieril | 2024-04-18 | 18 | -2/+20 |
| | | | | |||||
| * | | | Ensure we regenerate files properly in CI | Nadrieril | 2024-04-18 | 27 | -32/+9 |
| | | | | | | | | | | | | | | | | | | | | Files that weren't regenerated were marked as not automatically-generated. | ||||
* | | | | Merge pull request #146 from RaitoBezarius/main | Son HO | 2024-04-19 | 1 | -3/+69 |
|\ \ \ \ | | |/ / | |/| | | fix(backends/lean): add a significant amount of keywords | ||||
| * | | | fix(backends/lean): extract more keywords from `lstlean.tex` | Ryan Lahfa | 2024-04-18 | 1 | -0/+2 |
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Taken from https://github.com/leanprover/lean4/blob/master/doc/latex/lstlean.tex#L33 and https://github.com/leanprover/lean4/blob/master/doc/latex/lstlean.tex#L36-L43. This will not extract the tactics. Signed-off-by: Ryan Lahfa <ryan.lahfa@inria.fr> | ||||
| * | | | fix(backends/lean): extract more keywords from `lstlean.latex` | Ryan Lahfa | 2024-04-18 | 1 | -0/+62 |
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Taken from https://github.com/leanprover/lean4/blob/master/doc/latex/lstlean.tex#L12 and sorted. Tactics are ignored. Signed-off-by: Ryan Lahfa <ryan.lahfa@inria.fr> | ||||
| * | | | chore(backends/lean): sort the keyword list | Ryan Lahfa | 2024-04-17 | 1 | -4/+4 |
| | | | | | | | | | | | | | | | | | | | | | | | | OCD. :D Signed-off-by: Ryan Lahfa <ryan.lahfa@inria.fr> | ||||
| * | | | fix(backends/lean): `from` is a keyword | Ryan Lahfa | 2024-04-17 | 1 | -0/+1 |
| | | | | | | | | | | | | | | | | Signed-off-by: Ryan Lahfa <ryan.lahfa@inria.fr> | ||||
| * | | | fix(backends/lean): `as` is a keyword | Ryan Lahfa | 2024-04-17 | 1 | -0/+1 |
| | |/ | |/| | | | | | | | | | | | | | | | | | | | `as` is a reserved keyword and cannot be used as a variable name. Fixes #139. Signed-off-by: Ryan Lahfa <ryan.lahfa@inria.fr> | ||||
* | | | Merge pull request #116 from AeneasVerif/item_meta | Guillaume Boisseau | 2024-04-18 | 11 | -85/+101 |
|\ \ \ | |_|/ |/| | | |||||
| * | | Update charon pin | Nadrieril | 2024-04-18 | 2 | -5/+20 |
| | | | |||||
| * | | item_meta | Nadrieril | 2024-04-18 | 9 | -80/+81 |
|/ / | |||||
* | | Merge pull request #145 from RaitoBezarius/no-flakes | Guillaume Boisseau | 2024-04-18 | 4 | -1/+50 |
|\ \ | |||||
| * | | feat(nix): support non-Flakes users | Ryan Lahfa | 2024-04-17 | 4 | -1/+50 |
| |/ | | | | | | | | | | | | | | | Not all Nix users can make use of Flakes. This adds the compatibility for non-Flakes users. Signed-off-by: Ryan Lahfa <ryan.lahfa@inria.fr> | ||||
* | | Merge pull request #130 from AeneasVerif/fast-tests-outside-of-ci | Son HO | 2024-04-18 | 2 | -8/+4 |
|\ \ | | | | | | | Run sanity checks in CI only | ||||
| * | | Run sanity checks in CI only | Nadrieril | 2024-04-16 | 2 | -8/+4 |
| | | | |||||
* | | | Merge pull request #147 from AeneasVerif/binops-simplification | Son HO | 2024-04-18 | 4 | -478/+171 |
|\ \ \ | |_|/ |/| | | Bump charon | ||||
| * | | Bump charon | Nadrieril | 2024-04-17 | 4 | -478/+171 |
|/ / | |||||
* | | Merge pull request #126 from RaitoBezarius/scalar-preorders | Son HO | 2024-04-15 | 1 | -0/+10 |
|\ \ | |/ |/| | lean: scalars form a preorder | ||||
| * | lean: scalars form a preorder | Ryan Lahfa | 2024-04-12 | 1 | -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-ci | Son HO | 2024-04-15 | 2 | -2/+5 |
|\ \ | |/ |/| | Fix CI | ||||
| * | Fix CI | Nadrieril | 2024-04-15 | 2 | -2/+5 |
|/ | |||||
* | Merge pull request #124 from AeneasVerif/son/lean1 | Son HO | 2024-04-12 | 11 | -60/+674 |
|\ | | | | | Add more definitions to the Lean library | ||||
| * | Add more definitions to the Lean library | Son Ho | 2024-04-12 | 5 | -0/+200 |
| | | |||||
| * | Reorganize the files in the Lean backend a bit | Son Ho | 2024-04-12 | 5 | -241/+266 |
| | | |||||
| * | Start adding integer functions to the Lean library | Son Ho | 2024-04-12 | 7 | -58/+447 |
|/ |