Closes #75 🐔️👍️

🦀️🍰🦀️🍰🦀️🍰

* chore(clippy): clippy

* fix(kernel): unfold applications where the header is a `Decl`

Closes #68 🐔️👍️
Approved-by: belazy <aarthuur01@gmail.com>
Approved-by: loutr <loutr@crans.org>

🦀️🍰🦀️🍰🦀️🍰

* chore(nix): Bump dependencies

* chore(clippy): Remove useless prefix/suffix (clippy::module_name_repetitions)

* chore(clippy): Prevent failed fallback (clippy::default_fallback_numeric)

* chore(parser): Modify parser hierarchy

* fix(fmt): Reduce chain line to 90 columns

* fix(proost): Fix documentation issues

* fix(evaluator): Move out display function, since self is not used

* chore(clippy): Use Self when possible (clippy::use_self)

* fix(kernel): Use safe conversion char -> u8 instead

* chore(clippy): Use explicit lifetime name (clippy::single_char_lifetime_names)

* chore(clippy): Use explicit unreachable/control-flow operator when needed

* chore(clippy): Use to_owned() when possible (clippy::inefficient_to_string + clippy::str_to_string)

* chore(clippy): Use specific function for map function (clippy::map_unwrap_or + clippy::option_if_let_else)

* chore(clippy): Use correct pattern-matching (clippy::pattern_type_mismatch)

* chore(clippy): Apply must_use (clippy::must_use_candidate clippy::return_self_not_must_use)

* chore(clippy): Modify two-arm matches into if-let (clippy::single_match_else)

* fix(declaration): Made struct only-crate public

* chore(clippy): Use const qualifier when possible (clippy::missing_const_for_fn)

* chore(clippy): Use core instead of std (clippy::alloc_instead_of_core + clippy::std_instead_of_core)

* chore(clippy): Inline format args (clippy::uninlined_format_args)

* chore(clippy): Add LTO hints (clippy::missing_inline_in_public_items)

* chore(clippy): [Non-test only] Remove wildcard import (enum_glob_use + wildcard_imports)

* chore(clippy): Add semicolon when nothing is returned (semicolon_if_nothing_returned)

* feat(clippy): Enable clippy lints

* chore(workspace): Improve cargo workspace for dependencies

Closes #71 🐔️👍️
Approved-by: aalbert <augustin.albert@bleu-azure.fr>

🦀️🍰🦀️🍰🦀️🍰

* feat(proost): add test for is_command behavior with 1 letter

* fix(proost): add missing boundary check

belazy authored 2 years ago and loutr committed 2 years ago

Closes #28 🐔️👍️
Approved-by: belazy <aarthuur01@gmail.com>
Approved-by: aalbert <augustin.albert@bleu-azure.fr>
Approved-by: v-lafeychine <vincent.lafeychine@proton.me>
Approved-by: loutr <loutr@crans.org>

🦀️🍰🦀️🍰🦀️🍰

* fix(proost): added Define command back (need to distinguish between the two in order to bind and reuse correctly later

* chore(kernel, calculus/level): adapt documentation to new type

* chore(level): Add specific enum to handle comparison state

* chore(kernel): c-o-v-e-r-a-g-e

* chore(parser): remove TODO

* chore(parser): more coverage

* fix(kernel): trailing comma when printing `InstantiatedDeclaration`s

* fix(kernel): chiale + aboie, coverage

* chore(kernel): mention #14

* chore(kernel): yet another test

* chore(kernel): always more coverage

* chore(parser): add issue nb to todo

* fix(kernel): avoid reentrant entry bug when infering type of decls with 0 universe arguments

* fix(parser): revert comit, wtf clippy ?

* chore(parser): remove unused branch

* chore(kernel): another test

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

* fix(kernel): remove dangerous function

* chore(kernel): always more coverage

* feat(parser): remove `Define` command

* fix(kernel): interface checking for decls

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

* chore(kernel): add coverage

* 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(kernel): coverage

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

* fix(kernel): over-agressive normalization

* 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)

* 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(parser): avoid spacing befor univ decls/vars

* 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(proost): check existing identifiers for al definitions

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

* feat(parser): add `DeclarationCheckType`

* chore(kernel): remove unused test

* fix(proost): type-check terms before `Eval`uating

* docs: update

* fix: further adjustments to parser

* chore: formatting + some adjustments for kernel tests

* fix(parser, proost): modify command generation for declarations

* chore(parser): add tests todo

* chore(parser): tests on sort parsing

* fix(parser): tests

* feat(parser): parse universe bindings

* feat(parser): parse universe declarations in define_type

* fix(level): comments

* chore: remove biging as a dependency

* chore(kernel): remove todo

* chore(kernel): remove unused file

* chore(kernel): more tests

* chore(kernel): documentation of `level_builder.rs`

* feat(kernel): tests coverage

* fix(kernel): tests

* feat(kernel/term/builder): add binding to (instantiated) declaration builders

* feat(kernel): add builders for declaration

* chore(kernel): refactor builder file hierarchy and simplify these files

* fix(proost): some import errors

* feat(parser): add parsing for univ parameters of definitions

* chore(kernel): add todo

* fix: remove lifetime dependency on LevelEnvironment

* feat : add inference for declarations.

* feat(parser): add new parsing rules for levels

* feat(parser): new syntax for universe polymorphism

* feat(kernel): add type-checking for Decls

* feat: incorporate LevelBuilder in TermBuilder

* fix(kernel): refactor impl organisation: unload most of arena's

* WOOOHOOOO

* fix(kernel, level): fix incorrect assignment in hashcons function

* fix(kernel): more errors

* feat(kernel): fixed some errors

* feat(kernel): finish rudimentary bases for modifying parser and type checker

* feat(kernel): further work on Levels

* WIP feat(kernel): modify declaration.rs structure

* fix(kernel): removing Dweller struct, using a macro instead

* fix(kernel): refactor file structure to add new core types. first attempt for levels.

* feat(kernel): add generic Dweller type

* WIP fix(kernel): refactor file structure to add new core types

* um

* feat:something

* AH

* first commit

Closes #64 🐔️👍️

🦀️🍰🦀️🍰🦀️🍰

* fix : remaining todo

belazy authored 2 years ago and loutr committed 2 years ago

Closes #34 🐔️👍️
Approved-by: aalbert <augustin.albert@bleu-azure.fr>
Approved-by: v-lafeychine <vincent.lafeychine@proton.me>
Approved-by: loutr <loutr@crans.org>

🦀️🍰🦀️🍰🦀️🍰

* feat: coverage

* chore : refactor

* chore : better comments

* chore :  more comments

* feat : more improvements

* feat: uwu

* Feat : don't traverse whnfs when they're syntactically equal

* feat : make whnf() less agressive

Closes #48 🐔️👍️
Approved-by: aalbert <augustin.albert@bleu-azure.fr>
Approved-by: v-lafeychine <vincent.lafeychine@proton.me>

🦀️🍰🦀️🍰🦀️🍰

* chore: change branch name mentions to main

* feat(docs): add user manual

* fix(rustyline): autocompletion format: bold -> grey

* doc(all): add Proost logo

* doc(rustyline_helper): minor URL adjustments

* chore(README): update

* feat(README): add Proost logo

* feat(docs): add Proost logo in specification (LFS test in disguise)

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

Closes #40 🐔️👍️
Approved-by: aalbert <augustin.albert@bleu-azure.fr>
Approved-by: loutr <loutr@crans.org>

🦀️🍰🦀️🍰🦀️🍰

* chore(fmt): Modify format

* chore(coverage): Tune branch + Include no_coverage feature

* bump: Update pest to 2.5.1 and subdependencies

* feat(cargo): Add licence check

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

🦀️🍰🦀️🍰🦀️🍰

* feat(parser): add tests

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

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

* fix(kernel): fix tests

* fix(kernel): fix tests

* clippy

* add tests

* more tests

* feat(proost): tests

* clippy + move tests in kernel

* repl -> evaluator

* ex

* change processor for repl

* add verbose arg

* remove deps

* reference issues

* add issue for search command

* remove commandprocessor trait

* rename repl.rs

* fix error handling when failing to import file

* fix(proost): consider suggestions from review; slight refactor of errors

* chore(parser/commands): better display of the import command

* chore(parser): renaming private functions and correcting some documentation

* feat(proost): add better display for commands and use it instead in the import command display

* fix(proost): adapt proost to new parser behaviour

* fix(parser): make parser produce Builders instead of terms, which prevents evaluating commands too early

* add basic search command

* move pretty printing out of command processor

* functional cyclic dependency test

* better tab

* still buggy, more tests

* better emoji handling

* import file 2/2

* fix tests

* clippy

* import file 1/2: test if files exists

* add convenient command for user

* add import command, not fonctional yet

* clippy

* move command in parser

Closes #47 🐔️👍️

🦀️🍰🦀️🍰🦀️🍰

* fix(type_checker): apply new clippy suggestion

* chore(cargo): update

* chore(nix): dependency update

Closes #42 🐔️👍️
Approved-by: belazy <aarthuur01@gmail.com>
Approved-by: v-lafeychine <vincent.lafeychine@proton.me>
Approved-by: aalbert <augustin.albert@bleu-azure.fr>

🦀️🍰🦀️🍰🦀️🍰

* chore(language): typo hunting

* chore(kernel/type checker): adapt type checker tests to new kernel interface

* chore(kernel/test): adapt `and.rs` test to new kernel interface

* chore(proost): adapt proost to new kernel interface

* chore(parser): adapt parser to new kernel interface

* doc(kernel): complete documentation and interface

* doc(kernel/builder): WIP

* doc(kernel/calculus): complete documentation for calculus.rs

* doc(arena): complete documentation for arena.rs

* doc(kernel/arena): WIP

Closes #15 🐔️👍️
Approved-by: aalbert <augustin.albert@bleu-azure.fr>
Approved-by: v-lafeychine <vincent.lafeychine@proton.me>
Approved-by: belazy <aarthuur01@gmail.com>

🦀️🍰🦀️🍰🦀️🍰

* chore(cargo): update

* fix(from comments): second pass of small review changes

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

* fix(kernel review): take Vincent comments into account

* chore(cargo): update cargo.lock

* fix(kernel tests): adapt to new builder structure

* fix(proost): adapt proost toplevel to the new memory model.
This includes a temporary solution for error management, which will be changed anyway.

* fix(parser): adapt tests to memory model

* fix(kernel): refactor build functions location

* fix(parser): adapt parser to new model WIP

* feat(builders): WIP rewriting builders

* chore(file structure): reorganised the file structure of arena- or term-related functions

* chore(terms): changing some annotations in the file

* fix(tests): all tests now succeed. Errors were due to the rewriting of the tests, not the type checker

* fix(terms): chose to modify Debug impl of Terms instead; which gives better, less verbose results

* fix(terms): add wrapper around OnceCell in order to fix their Debug trait implementation (too enthusiastic by default)

* fix(kernel): fix term generation error with depth, fix wrong imax computation in type inference, fix PartialEq impl for Node

* fix(kernel tests): rewrite the and test

* fix(commands): update commands and the associated other functions

* fix(type checker): add necessary lifetime annotations on result

* fix(kernel tests): refactor tests accordingly

* feat(type checker): adapt type checking and errors to the memory model

* fix(terms and type checker): use deref trait, further temporary changes in type checker, removing previous environment definition; early: won't compile

* fix(terms): adapt all core functions from terms.rs; early: won't compile

* fix(terms): fix lifetime issue; early; won't compile

* feat(terms): finish new term description and generation

* chore(cargo): add `im-rc` dependency for immutable structures

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

Closes #37 🐔️👍️
Approved-by: aalbert <augustin.albert@bleu-azure.fr>
Approved-by: belazy <aarthuur01@gmail.com>
Approved-by: v-lafeychine <vincent.lafeychine@proton.me>

🦀️🍰🦀️🍰🦀️🍰

* add ?main

* nix run

* add backticks

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

* fix links

* add blabla

* mermaid test

* mermaid test

* mermaid test

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

Closes #39 🐔️👍️
Approved-by: aalbert <augustin.albert@bleu-azure.fr>
Approved-by: v-lafeychine <vincent.lafeychine@proton.me>
Approved-by: belazy <aarthuur01@gmail.com>

🦀️🍰🦀️🍰🦀️🍰

* format

* apply suggestion

* clippy

* apply suggestions

* 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)

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

* apply suggested change

* apply suggestion

* apply suggestions

* add cmd option description

* check if terminal and add option for syntax coloring

* add tab

* clippy fix

* apply suggestion

* fix coloring

* apply suggestions

* apply suggestions

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

* add everything listed in issue except full multiline editing

Closes #35 🐔️👍️
Approved-by: aalbert <augustin.albert@bleu-azure.fr>
Approved-by: loutr <loutr@crans.org>

🦀️🍰🦀️🍰🦀️🍰

* docs: fix example

* docs: update README

* docs: mentionning memory model + fix listing

* feat(docs): correct examples

* feat(docs): fix OCaml type and english

* feat(docs): remove lfs

* feat(docs): nixos+coverage

* feat(docs): misc

* feat(docs): add toplevel specs

* feat(docs): update syntax

* fix(tex): resolve listings errors

* feat(docs): update specs

belazy authored 2 years ago and loutr committed 2 years ago

Closes #33 🐔️👍️
Approved-by: belazy <aarthuur01@gmail.com>
Approved-by: v-lafeychine <vincent.lafeychine@proton.me>
Approved-by: aalbert <augustin.albert@bleu-azure.fr>
Approved-by: loutr <loutr@crans.org>

🦀️🍰🦀️🍰🦀️🍰

* fix(kernel): complete beta-reduction

* chore(test): refactor + add lazy-static test dependency

* fix : remove unused branch, again

* chore : fix rebase

* Fix : Dependent application type-checking

* chore : misc.

* fix(kernel) remove unused parameter for `conversion`

* fix(kernel) : shift variables context

* fix(kernel) : substitute dependent products when infering

* chore(kernel) : add coverage

* Fix : check if binder type is indeed a type

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

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

🦀️🍰🦀️🍰🦀️🍰

* chore(Cargo.toml): Add a missing space

* chore(ci): Remove unreachable line in coverage

* chore(cargo): Improve dependencies with workspace feature

* fix(ci): Tune coverage

* chore: Cleaning tests

* chore(kernel) : add coverage

* fix(kernel) : add coverage tests

* feat(errors): Improve errors handling

* chore(rust): Use of Deref/DerefMut for Environment

* chore(type_checker): Cleaning tests + Analyse branches

* chore(error): Add Result type + Improve use

* chore(location): Move location out of error file + Improve struct

Closes #8 🐔️👍️
Approved-by: v-lafeychine <vincent.lafeychine@proton.me>
Approved-by: belazy <aarthuur01@gmail.com>

🦀️🍰🦀️🍰🦀️🍰

* feat(parser): resolve threads

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

* feat(parser): resolve threads

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

* feat(parser): more coverage

* feat(parser): add one more test

* feat(parser): add test for error conversion

* feat(parser): more tests

* feat(parser): more tests

* feat(parser): more tests

* feat(parser): first test

Closes #31 🐔️👍️

🦀️🍰🦀️🍰🦀️🍰

* fix: remove 'z' file

Closes #30 🐔️👍️

🦀️🍰🦀️🍰🦀️🍰

* fix(parser)

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

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

Closes #25 🐔️👍️
Approved-by: loutr <loutr@crans.org>

🦀️🍰🦀️🍰🦀️🍰

* fix(flake): Correctly interlink inputs

* chore: Add coverage folder into gitignore

* feat(ci): Output only branches in CI-view

* feat(nix): Add coverage command with devshell

* feat(ci, nix): Branches coverage

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`

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

Closes #23 🐔️👍️

🦀️🍰🦀️🍰🦀️🍰

* fix(ci): Remove coverage files after tests

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)