summaryrefslogtreecommitdiff
path: root/compiler (unfollow)
Commit message (Expand)AuthorFilesLines
2024-05-31Fix unused variables warningsAymeric Fromherz2-13/+18
2024-05-31Avoid adding shared loans twice when merging environmentsAymeric Fromherz1-5/+28
2024-05-31Add markers when creating new abstractions because of a join with bottomAymeric Fromherz3-48/+63
2024-05-31Also fix implementation of Join-SharedBorrowAymeric Fromherz1-3/+3
2024-05-30destructure_abs can be called during collapse: markers should be allowedAymeric Fromherz1-4/+0
2024-05-30Correct implementation of Join-MutBorrows: add markers when creating a new ab...Aymeric Fromherz1-3/+4
2024-05-30More lisible sign for proj_right pretty-printingAymeric Fromherz1-1/+1
2024-05-30Implement two phases of loops join + collapseAymeric Fromherz4-383/+552
2024-05-28Compute marker information for borrow/loan mapsAymeric Fromherz3-50/+73
2024-05-28Add type and set/map for marker and borrow idAymeric Fromherz3-9/+21
2024-05-27Simplify collapse_ctxAymeric Fromherz1-6/+5
2024-05-27Simplify reduce_ctxAymeric Fromherz1-21/+6
2024-05-27Split collapse into collapse and reduce, rename accordinglyAymeric Fromherz4-13/+185
2024-05-27Add projection markers when joining environmentsAymeric Fromherz1-0/+59
2024-05-27Add markers everywhere, do not use them yetAymeric Fromherz10-139/+302
2024-05-24Start adding markersSon Ho6-50/+94
2024-05-24Expand debug output in loops fixed pointsAymeric Fromherz1-1/+16
2024-05-24Rename meta into spanAymeric Fromherz51-2939/+2943
2024-05-24Rename span into raw_spanAymeric Fromherz4-20/+20
2024-05-24Update charon pinNadrieril2-2/+3
2024-05-24Fix a crash which happens when type definitions are ignoredSon Ho1-2/+5
2024-05-24Print the name patterns of the definitions which fail to extractSon Ho2-15/+24
2024-05-23Update the interpreter so that it is not written in CPS style (#120)Escherichia19-2294/+2116
2024-05-14Catch new literal variantsNadrieril2-0/+6
2024-05-14Ensure `./charon` points to a valid charon cloneNadrieril2-1/+1
2024-05-06Update charonNadrieril2-3/+12
2024-05-01Add error when handling mutually recursive traitsAymeric Fromherz1-1/+4
2024-04-26Update compiler/ExtractBuiltin.mlSon HO1-1/+1
2024-04-25Update the backend and ExtractBuiltin.mlSon Ho1-1/+4
2024-04-24Add core::option::unwrap builtinZyad Hassan1-0/+2
2024-04-24compiler: introduce Lean-only translationsRyan Lahfa1-10/+25
2024-04-24compiler: map `core::option::Option::is_none` to `Option.isNone`Ryan Lahfa1-0/+4
2024-04-24compiler: map `core::mem::swap` to the pure swapRyan Lahfa1-0/+2
2024-04-22Fix an issue when joining a symbolic value with bottomSon Ho2-11/+33
2024-04-22Reformat some filesSon Ho5-24/+47
2024-04-18fix(backends/lean): extract more keywords from `lstlean.tex`Ryan Lahfa1-0/+2
2024-04-18fix(backends/lean): extract more keywords from `lstlean.latex`Ryan Lahfa1-0/+62
2024-04-18item_metaNadrieril9-80/+81
2024-04-17chore(backends/lean): sort the keyword listRyan Lahfa1-4/+4
2024-04-17fix(backends/lean): `from` is a keywordRyan Lahfa1-0/+1
2024-04-17fix(backends/lean): `as` is a keywordRyan Lahfa1-0/+1
2024-04-17compiler: map `core::option::Option::take` to identity functionRyan Lahfa1-0/+4
2024-04-12Add more definitions to the Lean librarySon Ho1-0/+73
2024-04-12Start adding integer functions to the Lean librarySon Ho4-55/+181
2024-04-12Update the bindings for the extractionSon Ho1-14/+11
2024-04-11Update a commentSon Ho1-2/+2
2024-04-11Reformat the codeSon Ho1-9/+6
2024-04-11Update a commentSon HO1-1/+1
2024-04-10Trust rustc regarding `Copy` boundsNadrieril3-7/+7
2024-04-07Improve the error messages furtherSon Ho3-1/+44
generated by cgit v1.2.3 (git 2.25.1) at 2024-12-23 01:16:43 +0000