Commit message (Collapse) | Author | Age | Files | Lines | |
---|---|---|---|---|---|
* | Fix an issue with the type of the values given back by loops | Son Ho | 2024-06-03 | 3 | -157/+237 |
| | |||||
* | Fix a bug when composing the continuations in eval_statement | Son Ho | 2024-06-03 | 4 | -122/+131 |
| | |||||
* | Change the order in which we merge abstractions | Son Ho | 2024-06-03 | 5 | -105/+99 |
| | |||||
* | Cleanup a bit | Son Ho | 2024-06-03 | 3 | -44/+53 |
| | |||||
* | Factor out some code and update some comments | Son Ho | 2024-06-03 | 4 | -166/+173 |
| | |||||
* | Cleanup a bit | Son Ho | 2024-06-03 | 4 | -91/+87 |
| | |||||
* | Make minor modifications | Son Ho | 2024-06-03 | 4 | -19/+25 |
| | |||||
* | Update some comments | Son Ho | 2024-06-03 | 1 | -2/+2 |
| | |||||
* | format | Aymeric Fromherz | 2024-05-31 | 1 | -18/+18 |
| | |||||
* | Add documentation to collapse | Aymeric Fromherz | 2024-05-31 | 1 | -1/+27 |
| | |||||
* | Add missing reverse when collapsing environment | Aymeric Fromherz | 2024-05-31 | 1 | -2/+1 |
| | |||||
* | Fix unused variables warnings | Aymeric Fromherz | 2024-05-31 | 2 | -13/+18 |
| | |||||
* | Avoid adding shared loans twice when merging environments | Aymeric Fromherz | 2024-05-31 | 1 | -5/+28 |
| | |||||
* | Add markers when creating new abstractions because of a join with bottom | Aymeric Fromherz | 2024-05-31 | 3 | -48/+63 |
| | |||||
* | Also fix implementation of Join-SharedBorrow | Aymeric Fromherz | 2024-05-31 | 1 | -3/+3 |
| | |||||
* | destructure_abs can be called during collapse: markers should be allowed | Aymeric Fromherz | 2024-05-30 | 1 | -4/+0 |
| | |||||
* | Correct implementation of Join-MutBorrows: add markers when creating a new ↵ | Aymeric Fromherz | 2024-05-30 | 1 | -3/+4 |
| | | | | abstraction | ||||
* | More lisible sign for proj_right pretty-printing | Aymeric Fromherz | 2024-05-30 | 1 | -1/+1 |
| | |||||
* | Implement two phases of loops join + collapse | Aymeric Fromherz | 2024-05-30 | 4 | -383/+552 |
| | |||||
* | Compute marker information for borrow/loan maps | Aymeric Fromherz | 2024-05-28 | 3 | -50/+73 |
| | |||||
* | Add type and set/map for marker and borrow id | Aymeric Fromherz | 2024-05-28 | 3 | -9/+21 |
| | |||||
* | Simplify collapse_ctx | Aymeric Fromherz | 2024-05-27 | 1 | -6/+5 |
| | |||||
* | Simplify reduce_ctx | Aymeric Fromherz | 2024-05-27 | 1 | -21/+6 |
| | |||||
* | Split collapse into collapse and reduce, rename accordingly | Aymeric Fromherz | 2024-05-27 | 4 | -13/+185 |
| | |||||
* | Add projection markers when joining environments | Aymeric Fromherz | 2024-05-27 | 1 | -0/+59 |
| | |||||
* | Add markers everywhere, do not use them yet | Aymeric Fromherz | 2024-05-27 | 10 | -139/+302 |
| | |||||
* | Start adding markers | Son Ho | 2024-05-24 | 6 | -50/+94 |
| | |||||
* | Expand debug output in loops fixed points | Aymeric Fromherz | 2024-05-24 | 1 | -1/+16 |
| | |||||
* | Rename meta into span | Aymeric Fromherz | 2024-05-24 | 51 | -2939/+2943 |
| | |||||
* | Rename span into raw_span | Aymeric Fromherz | 2024-05-24 | 4 | -20/+20 |
| | |||||
* | Update charon pin | Nadrieril | 2024-05-24 | 2 | -2/+3 |
| | |||||
* | Fix a crash which happens when type definitions are ignored | Son Ho | 2024-05-24 | 1 | -2/+5 |
| | |||||
* | Print the name patterns of the definitions which fail to extract | Son Ho | 2024-05-24 | 2 | -15/+24 |
| | |||||
* | Update the interpreter so that it is not written in CPS style (#120) | Escherichia | 2024-05-23 | 19 | -2294/+2116 |
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | * Start turning the compiler in a style which is less CPS * Update a function in InterpreterExpressions.ml * WIP work on cps * WIP * WIP, currently on InterpreterStatements.ml * WIP * Finished CPS-related modification * Fixed some warning related to documentation comments * Finished loop support, fixed a loop * fixed a typed value * Fixed check_disappeared related error * cleaned check_disappeared related error * Start cleaning up * Do more cleanup * Make some cleanup and fix an issue * Do more cleanup * Do more cleanup * Do more cleanup * Do more cleanup * Do more cleanup * Do more cleanup * Do more cleanup * Do more cleanup * Rename a function * Do more cleanup * Cleanup the loops code and fix some bugs * Cleanup assign_to_place * Make a minor cleanup --------- Co-authored-by: Son Ho <hosonmarc@gmail.com> | ||||
* | Catch new literal variants | Nadrieril | 2024-05-14 | 2 | -0/+6 |
| | |||||
* | Ensure `./charon` points to a valid charon clone | Nadrieril | 2024-05-14 | 2 | -1/+1 |
| | |||||
* | Update charon | Nadrieril | 2024-05-06 | 2 | -3/+12 |
| | |||||
* | Add error when handling mutually recursive traits | Aymeric Fromherz | 2024-05-01 | 1 | -1/+4 |
| | |||||
* | Update compiler/ExtractBuiltin.ml | Son HO | 2024-04-26 | 1 | -1/+1 |
| | | | Co-authored-by: Zyad Hassan <88045115+zhassan-aws@users.noreply.github.com> | ||||
* | Update the backend and ExtractBuiltin.ml | Son Ho | 2024-04-25 | 1 | -1/+4 |
| | |||||
* | Merge branch 'main' into core-option-unwrap | Son Ho | 2024-04-25 | 1 | -0/+25 |
|\ | |||||
| * | Merge branch 'main' into option-take | Son Ho | 2024-04-25 | 10 | -100/+212 |
| |\ | |||||
| * | | 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 | 1 | -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 function | Ryan Lahfa | 2024-04-17 | 1 | -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 builtin | Zyad Hassan | 2024-04-24 | 1 | -0/+2 |
| |/ |/| | |||||
* | | 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 #146 from RaitoBezarius/main | Son HO | 2024-04-19 | 1 | -3/+69 |
|\ \ | | | | | | | fix(backends/lean): add a significant amount of keywords |