- Oct 20, 2022
-
-
Closes #9 🐔️👍️ 🦀️
🍰 🦀️🍰 🦀️🍰 * Fix : clippy * Chore : document `TypeCheckingError` * Chore : remove useless mut * Feat : make `Context` private * Feat : simplify `check` * Chore : Remove old comment * Chore : remove eta-expansion for functions to please the big guy * Chore : comment error * Chore : remove `println` * Chore : add doc for `TypeCheckingError` * Fix : put derive before comments * Feat : add more coverage * Fix : golf `whnf()` * Fix : `polymorphism` test * Fix : `pub_crate` for `substitute` * Chore : CamelCase * Feat : add `Type_checking_error` * Chore : move `normal_form` and `whnf` to `term.rs` * Chore : rename tests * Chore : remove debug `println` * Chore : Add documentation * Feat : use `whnf()` instead of `normal_form()` for conversion * Chore : resolve ill-typed `complex_subst` test * Feat : remove `Val`, correctly substitute terms. * Chore : remove `classic_term.rs` * chore(Context): Rename * chore(type_checker): Apply clippy suggestions on tests * fix: Remove Term's Abs/Prop names * chore: format + derive Default for Ctx * chore: Reorganise type_checker + derive Default for Ctx * Feat : add documentation for `type_checker.rs` * Chore: merge `impl Val`s * Chore : remove debug prints in tests * Chore : mark `Err`s with `//TODO #19` * Chore : Move `Val` to the top of the file * Fix : remove `set_var` in tests * Fix : `polymorphism` test * chore: move everything to their respective `impl` * fix: avoid `assert` in `is_def_eq`, move Val-related methods * chore : make `conversion` a method * Fix: make `normal_form` a method * fix: use `self` for `eval` * Fix : Add issue reference * Feat : remove `panic!`s, use `Result` monad instead * Chore : rename `Ctx::empty()` to `Ctx::new()` * Chore : remove duplicate `assert_def_eq` * Chore : add `impl Term` * Chore : remove `use Term::*`, add `use Val::*` instead * Chore : remove `Into` trait for UniverseLevel * remove useless `impl` for `UniverseLevel` * Chore : remove prints * fix : comment `Val` * Fix : make `conv` into an `Into` trait * fix : `Val` constructor names * fix : imports * chore : fix TODO * fix : `lib.rs` imports * fix : inference for lambda-abstractions * chore : remove useless print * chore : fix various comments * fix : `is_universe` * chore : add more comments to `conv` * feat : simplify `quote` * chore : add TODO * fix : commentary for beta_reduction * chore : comment Val * chore : remove old comment * fix : added `Ctx` type to store type of Vars during checking * feat : add polymorphic test which shows the need to add `Ctx` * chore : please Clippy * Fix : stop cloning environments for no reason * fix : test * chore : add comments * feat : add `check` and `infer` * fix: add string data to lambda-pi abstractions from classicTerm * feat: add string data to pi/lambda-abstractions * fix : made clippy happier * chore : adapt existing code to rebase * fix : conversion between Var and VVar * fix : remove complex_subst from the def_eq test suite for now * feat : added Ctx in preparation for type-checking * this pleases the formatter * Fix : conversion algorithm * basic conversion algorithm (doesn't work) -
Closes #16 🐔️👍️ Approved-by:
loutr <loutr@crans.org> Approved-by:
aalbert <augustin.albert@bleu-azure.fr> 🦀️
🍰 🦀️🍰 🦀️🍰 * fix(nix): Add rust-src in rust profile * feat(ci): Add stages for better-CI understanding * feat(ci): Add coverage
-
- Oct 18, 2022
-
-
v-lafeychine authored
-
- Oct 17, 2022
-
-
Closes #10 🐔️👍️ Approved-by:
v-lafeychine <vincent.lafeychine@proton.me> Approved-by:
aalbert <augustin.albert@bleu-azure.fr> Approved-by:
loutr <loutr@crans.org> 🦀️
🍰 🦀️🍰 🦀️🍰 * fix(parser): Fix the semantics of products without parentheses. * chore(parser): renaming * chore(parser & proost): renaming * feat(parser): documentation * fix(parser): resolve threads * feat(parser): Add new syntaxic sugar and meaningfull error messages, add more efficient conversion into terms (VecDeque), remove unused struct ClassicTerm, remove useless & outdated test. feat(kernel): Add new command: DefineCheckType. eg: "def x:P := P" feat(proost): Process multiples commands in one line * feat(parser): Add new syntaxic sugar and meaningfull error messages, add more efficient conversion into terms (VecDeque), remove unused struct ClassicTerm, remove useless & outdated test. feat(kernel): Add new command: DefineCheckType. eg: "def x:P := P" feat(proost): Process multiples commands in one line
-
- Oct 10, 2022
-
-
Closes #6 🐔️👍️ Approved-by:
aalbert <augustin.albert@bleu-azure.fr> Approved-by:
belazy <aarthuur01@gmail.com> Approved-by:
v-lafeychine <vincent.lafeychine@proton.me> 🦀️
🍰 🦀️🍰 🦀️🍰 * docs: add specifications PDF * docs: finish first version of the specifications * docs: finish early description of specifications * docs: add document template for specifiations * feat(git): add LFS settings and TeX-specific .gitignore
-
- Oct 09, 2022
-
-
v-lafeychine authored
Closes #11 🐔️👍️ Approved-by:
belazy <aarthuur01@gmail.com> Approved-by:
aalbert <augustin.albert@bleu-azure.fr> 🦀️
🍰 🦀️🍰 🦀️🍰 * chore: Use reexport of dependencies * feat: Use BigUint for universes * chore(term): Rename NewType of Term::Var and Term::Type * chore(proost): Refactor If-return-else * chore(parser): Add derive_more * chore(kernel): Add derive_more
-
- Oct 07, 2022
-
-
v-lafeychine authored
Closes #13 🐔️👍️ 🦀️
🍰 🦀️🍰 🦀️🍰 * chore!(cargo): Rename crate into -
v-lafeychine authored
-
v-lafeychine authored
Closes #2 🐔️👍️ Approved-by:
belazy <aarthuur01@gmail.com> Approved-by:
loutr <loutr@crans.org> Approved-by:
aalbert <augustin.albert@bleu-azure.fr> 🦀️
🍰 🦀️🍰 🦀️🍰 * feat(term): Complete beta-reduction * [WIP] feat(term): Improve beta-reduction + Add tests * feat(term): Early beta-reduction * feat(term): Add early Term struct + Display trait
-
- Oct 06, 2022
-
-
Closes #5 🦀️🍰️🦀️🍰️🦀️🍰️🦀️🍰️ Approved-by:
loutr <loutr@crans.org> Approved-by:
v-lafeychine <vincent.lafeychine@proton.me> 🦀️🍰️🦀️🍰️🦀️🍰️🦀️🍰️ * fix(proost): iterates over arguments as shared immutable references as to prevent cloning * chore(proost): Add spaces * feat(proost): Add banner support for CLI * feat(proost): Add command line argument support with clap * feat(proost): Add basic CLI and file handling
-
aalbert authored
Closes #3 Approved-by:
belazy <aarthuur01@gmail.com> Approved-by:
aalbert <augustin.albert@bleu-azure.fr> * fix(parser): Fix minor issues (impl PartialEq for tests) * feat(parser): Add more inclusive syntax * feat(parser): Add informative message for free variables * fix(parser): Fix a conversion bug * feat(parser,core): Move classic term from core into parser * feat(parser): Conversion from classic terms to terms * feat(core): Add conversion from classic term to term * chore(parser): Rename pest file * chore(core): Move classic terms in its own file * feat(parser): Add ClassicTerm with variables for easier user input * fix(parser): Reorganize lib.rs and parser.rs * fix(parser): Reorganize lib.rs and parser.rs * fix(parser): Reorganize lib.rs and parser.rs * chore(parser): Rename tests files * chore(parser): Rename tests files * feat(parser): add parser for terms, commands and files * feat(parser): add parser for terms, commands and files * feat(parser): add parser for terms, commands and files * feat(parser): add parser for terms, commands and files * feat(parser): add parser for terms, commands and files * feat(parser): add parser for terms, commands and files * feat(parser): add parser for terms, commands and files * chore(core): add license * chore(parser): remove warnings * chore(core): format files * chore(parser): remove warnings * chore(parser): format code * fix(core): add lib.rs * feat(term): Add early Term struct + Display trait * feat(parser): add parser crate and pest config
-
- Sep 30, 2022
-
-
v-lafeychine authored
-
- Sep 29, 2022
-
-
Closes #4 Approved-by:
aalbert <augustin.albert@bleu-azure.fr> Approved-by:
loutr <loutr@crans.org> * Apply 1 suggestion(s) to 1 file(s) * feat(nix): Build Dockerfile from flake
-
- Sep 22, 2022
-
-
Closes #1 Approved-by:
v-lafeychine <vincent.lafeychine@proton.me> Approved-by:
loutr <loutr@crans.org> * chore(cargo): Add cargo workspace
- Sep 21, 2022
-
-
v-lafeychine authored
- Sep 15, 2022
-
- Sep 13, 2022
-