v-lafeychine authored 2 years ago and aalbert committed 2 years ago

Closes #22 et #7 🐔️👍️
Approved-by: aalbert <augustin.albert@bleu-azure.fr>
Approved-by: belazy <aarthuur01@gmail.com>
Approved-by: loutr <loutr@crans.org>

🦀️🍰🦀️🍰🦀️🍰

* Chore : add test

* Fix : shift vars when binding lambda-abstractions

* fix(kernel): some tests were wrong

* HOT fix(kernel): command definition fixed

* HOT fix(parser): fix parenthesis

* HOT fix(parser): order of fun

* feat(parser): resolve threads

* chore(parser): Merge renamed_rules on Error

* chore(command): Merge Define/DefineCheckType + Add tests

* chore(parser): apply suggestions

* feat(parser): add location conversion from pest to proost's kernel

* Apply 1 suggestion(s) to 1 file(s)

* fix(all): resolve thread and change Pos for Loc (range position) +
conversion from position to range position in parser

* fix(all): resolve threads

* feat(kernel): Add tests in commands.rs

* feat(parser, error): add new errors for parser, pos struct, first use of pos and pretty print of parsing errors

* feat(parser, kernel): new kernel error: cannot parse

* feat(proost): new ui v1

* feat(proost): new interface!

* feat(parser, kernel): change grammar and pretty printing

belazy authored 2 years ago and v-lafeychine committed 2 years ago

Closes #17 🐔️👍️
Approved-by: belazy <aarthuur01@gmail.com>
Approved-by: loutr <loutr@crans.org>
Approved-by: aalbert <augustin.albert@bleu-azure.fr>

🦀️🍰🦀️🍰🦀️🍰

* chore: misc

* chore : add test coverage

* chore(kernel): Reduce code complexity

* fix(kernel): Made Context mutable

* fix(kernel): Made type_checker.rs full of reference

* fix(kernel): Made term.rs full of reference

* fix(kernel): Use of reference

* Apply 1 suggestion(s) to 1 file(s)

* Fix : refer to #19

* Apply 1 suggestion(s) to 1 file(s)

* Apply 1 suggestion(s) to 1 file(s)

* Apply 1 suggestion(s) to 1 file(s)

* Fix : remove unused trait

* Fix : apply suggestion

* Fix : use Self in impl

* Apply 1 suggestion(s) to 1 file(s)

* Apply 1 suggestion(s) to 1 file(s)

* Apply 1 suggestion(s) to 1 file(s)

* Apply 1 suggestion(s) to 1 file(s)

* Apply 1 suggestion(s) to 1 file(s)

* Chore: use `Environment::new()` instead of `Default::default()`

* Chore :  add documentation

* Chore : expand tests coverage

* Revert "Feat : parse Constants"

This reverts commit 0618fd79.

* Feat : move `Environment` to respective file

* Feat : add test for Env use during typechecking

* Feat : parse Constants

* Feat : use `Environment` during type-checking/inference

* Feat : add `GlobalContext`

belazy authored 2 years ago and v-lafeychine committed 2 years ago

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)

aalbert authored 2 years ago and loutr committed 2 years ago

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

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

Closes #13 🐔️👍️

🦀️🍰🦀️🍰🦀️🍰

* chore!(cargo): Rename  crate into