v-lafeychine authored 10 months ago and loutr committed 10 months ago

Closes #115 🐔️👍️
Approved-by: loutr <l.ta-ma@proton.me>

🦀️🍰🦀️🍰🦀️🍰

* fix(coverage): Generate format directly with one Nix invocation

* fix(atty): Remove unmaintained atty crate

* feat(ci): Use crane to perform tests

* chore(cargo-deny): Bump to latest syntax

* chore(nix): Use crane and fenix

* chore(rustfmt): Bump to 1.7.0

* chore(cargo): Bump dependencies

* chore(ci): Upgrade coverage tool

* chore(nix): Remove docker + devshell

* chore(ci): Use Nix instead of extern Docker images

* chore: Bump Nix to 23.11

* chore: Bump clippy to 1.80 nightly

* chore: Bump Rust to 1.80 nightly

pigeonmoelleux authored 11 months ago and v-lafeychine committed 11 months ago

Closes #109 🐔️👍️
Approved-by: loutr <l.ta-ma@proton.me>
Approved-by: v-lafeychine <vincent.lafeychine@proton.me>

🦀️🍰🦀️🍰🦀️🍰

* chore(tilleul): fix issues for the merge request

* feat(tilleul): add LICENSE and README for VSCode client

* chore(tilleul): change linter options and the code to comply with it

* chore(tilleul): corrections enlightened by the review

* chore(tilleul): remove unecessary vscode-related files

* feat(tilleul): add language syntax for the vscode client

* feat(tilleul): minimal version of a VSCode LSP client

pigeonmoelleux authored 1 year ago and v-lafeychine committed 1 year ago

Closes #81 🐔️👍️
Approved-by: loutr <l.ta-ma@proton.me>
Approved-by: v-lafeychine <vincent.lafeychine@proton.me>

🦀️🍰🦀️🍰🦀️🍰

* fix(proost): return a `BoundVariable` error when defining a declaration and a definition with the same name

pigeonmoelleux authored 1 year ago and v-lafeychine committed 1 year ago

Closes #110 🐔️👍️
Approved-by: loutr <l.ta-ma@proton.me>
Approved-by: v-lafeychine <vincent.lafeychine@proton.me>

🦀️🍰🦀️🍰🦀️🍰

* fix(tilleul): change tilleul initialization to indicate that no capability is currentlly handled

Closes #107 🐔️👍️

🦀️🍰🦀️🍰🦀️🍰

* chore(std, examples): fix syntax

* chore(parser): change test to fit new syntax

* fix(parser): remove the use of comma as argument separator, for more consistency

* fix(parser): simpler, (hopefully) equivalent grammar

belazy authored 1 year ago and loutr committed 1 year ago

Closes #95 🐔️👍️
Approved-by: aalbert <augustin.albert@bleu-azure.fr>
Approved-by: loutr <l.ta-ma@proton.me>

🦀️🍰🦀️🍰🦀️🍰

* chore(cargo deny): cargo update + temporary cargo deny modification to allow duplicate dependency versions

* fix(kernel, level): remove useless memoization + some minor simplifications

* fix(kernel): use u32 in order to have safe conversions to i64

* fix(kernel): wrap int conversion

* feat(kernel): replace `Succ` constructor with `Add`

Closes #98 🐔️👍️
Approved-by: aalbert <augustin.albert@bleu-azure.fr>
Approved-by: loutr <l.ta-ma@proton.me>

🦀️🍰🦀️🍰🦀️🍰

* chore(parser): add coverage

* chore(parser): make more complex test

* feat(parser): more concise function `parse_args`

* fix(parser): use `try_fold` instead of ` fold`

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

* chore(error): add new rules to parsing errors

* feat(std): use left-args in examples

* chore(parser): comment and test

* feat(parser): parse left-arguments

* feat(parser): add left-args to the syntax

Closes #97 🐔️👍️
Approved-by: loutr <l.ta-ma@proton.me>

🦀️🍰🦀️🍰🦀️🍰

* chore: move the toplevel screenshot to the manual, as a listing

* feat(std): add `add` function over natural numbers, used as an example

* chore(docs): separate header style file for TeX + formatting

* Apply 4 suggestion(s) to 2 file(s)

* chore: update Cargo lock

* chore: update Proost version number

* docs: update manual

* docs: update specifications

* feat: mentionn GitHub mirror in README and update logo link

* docs(parser): incorrect documentation for commands

* docs(kernel: axiom, trace): fix documentation and try to make it more uniform

* docs(elaboration): fix links and typos in documentation

pigeonmoelleux authored 2 years ago and loutr committed 2 years ago

Closes #87 🐔️👍️
Approved-by: belazy <aarthuur01@gmail.com>
Approved-by: loutr <l.ta-ma@proton.me>
Approved-by: aalbert <augustin.albert@bleu-azure.fr>

🦀️🍰🦀️🍰🦀️🍰

* feat(presentation): Add coverage slides

* docs(tex): description of the kernel

* chore(presentation): Improve slides style

* change color

* chore(docs): corrections on the presentation

* feat(docs): ending of presentation for 0.3.0

* feat(docs): beginning of presentation for 0.3.0

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

🦀️🍰🦀️🍰🦀️🍰

* chore(std): clarify separation of definitions across files + manual formatting

* chore: define std folder and reorganise madeleine files structure

* fixup: merge parts of contraposition and classical

Two new files bool.mdln and connectives.mdln containing True, False, And, Or, Not.

Also harmonized naming conventions: Prop and functions returning Prop
(like And) start with a capital letter, lemmas (whose type is itself a
Prop) are lowercased.

* feat: Resolve "Classical logic" (#78)

Add a classical.mdln file with three characterizations of excluded
middle.

loutr authored 2 years ago and loutr committed 2 years ago

Closes #100 🐔️👍️

🦀️🍰🦀️🍰🦀️🍰

* fix(parser): prevent filenames from beings keywords

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

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

🦀️🍰🦀️🍰🦀️🍰



* test: provide tests for parenthesis omission and axiom printing

* feat: less parentheses in printing

* feat: use method `is_certainly_closed` in pretty printing

* chore(pretty): move pretty-printing functions into a separate module

* feat(kernel::memory::term): in pretty printing, associate variables to letters instead of numerical identifier

* fix: no space before ':'

* fix: parenthesis for application

* fix: prettyprint renamed in pretty_print + doc

* fix: cases for Prop display. doc: PrettyTerm and Term::prettyprint

* feat: add PrettyTerm structure for easy display manipulation

* fix(prettyprinting): less parenthesizing

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

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

* fix(prettyprint): comment as clippy wants & self by value as asked by clippy

* fix(prettyprint): variable names corrected

* feat(prettyprint): WIP on new prettyprint. WARNING: Variable names aren't always correct in the argtype.

* Resolve: "Add support for non-nix users" (79) ✨️
Closes #79 🐔️👍️
Approved-by: belazy <aarthuur01@gmail.com>

🦀️🍰🦀️🍰🦀️🍰

* fix: Specified which version is used (1.68.0 nightly 2022-12-27)

* feat: Add "nightly" in the rust toolchain

aplanos authored 2 years ago and loutr committed 2 years ago

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

🦀️🍰🦀️🍰🦀️🍰

* fix(kernel::memory::term): fix incorrect initialisation for is_certainly_closed

* chore: edit documentation & comments

* feat(kernel): Finding certain terms closedness while building them

* fix(kernel): False positive closed term with offset == 0

* feat(kernel): Set 'is_certainly_closed' if effectively closed

* feat(kernel): Add closedness boolean to term header & jump shift if term is closed

pigeonmoelleux authored 2 years ago and loutr committed 2 years ago

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

🦀️🍰🦀️🍰🦀️🍰

* chore(builder): Open issue (#94)

* fix(elaboration): Rebase issues

* chore(parser): Check every branch on unhandled parse_level

* perf(parser): Use try_fold instead of collect

* chore(parser): Remove useless wrapping on parse_level

* feat(parser): add coverage

* feat(parser): remove sum in the parsing of plus

* chore(kernel): add tests for  function

* chore(kernel): Add documentation for the  function

* fix(parser): Handle FromStr failure on usize

* chore(parser): Modify Kind::CannotParse to Kind::UnexpectedToken

* fix(kernel): fixed issues enlightened during the review

* Change the location of `max_depth` which is now a impl of Builder
 * Remove the corresponding tests, which will be added in the future
* The test for the depth is now made before the creation of the `Level` struct

* feat(level): Add max_depth in Builder

Closes #89 🐔️👍️
Approved-by: v-lafeychine <vincent.lafeychine@proton.me>

🦀️🍰🦀️🍰🦀️🍰

* fix(builder): improved branching

* fix(builder): avoid env cloning

* chore(parser): add wildcard tests

* feat(parser): parse wildcards

* feat(builder): don't add wildcards to env

nartan authored 2 years ago and belazy committed 2 years ago

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

🦀️🍰🦀️🍰🦀️🍰

* fix(kernel): fix `type_true_rec`

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

* fixed error in True recursor

* fixed the implementation of the True recursor and added the Tt type

* added true type and true recursor

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

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

🦀️🍰🦀️🍰🦀️🍰



* chore: split example file contraposition.mdln meaningfuly and remove already-defined axioms

* Apply 9 suggestion(s) to 3 file(s)

* Apply 11 suggestion(s) to 4 file(s)

* chore(kernel): add documentation

* chore(kernel): Refactor axiom into own mod

* feat(examples): add more examples

* chore(kernel): Remove let chains in if, because of Deref-missing implementation

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

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

* fix(kernel): comment syntax

* fix(kernel): proof-irrelevance

* fix(kernel): slur in comment

* fix(kernel): fix comment

* chore(kernel): add tests

* fix(kernel): fix relevance for wildcard terms

* feat(kernel): add relevance tag to terms

* fix(examples): fix irrelevance example

* feat(example): add irrelevance example

* fix(kernel): avoid infinite looping

* fix(kernel): fix `is_prop_term`

* feat(kernel): add `is_prop_term` and `is_prop_type`

* feat(kernel): better recursor pattern recognition

* feat(examples): add example using `Eq`

* fix(kernel): whnf reduction on recursors

* fix(kernel): `Eq_rec` type

* feat(kernel): add reduction rule for `Eq_rec`

* fix(kernel): `Eq` type

* feat(kernel): add `Eq` type

* Resolve "LSP: Proof-of-concept" ✨️
Closes #20 🐔️👍️
Approved-by: aalbert <augustin.albert@bleu-azure.fr>
Approved-by: belazy <aarthuur01@gmail.com>
Approved-by: loutr <loutr@crans.org>

🦀️🍰🦀️🍰🦀️🍰

* chore(tilleul): fix typos in documentation

* chore(tilleul): Add axioms

* chore(tilleul): Add global server tests on unexpected queries

* chore(tilleul): Add UTF-8 message test

* chore(tilleul): Add connection tests

* chore(tilleul): Add message write/read test

* chore(tilleul): Add dispatcher tests

* fix(tilleul): Documentation

* feat(editors): Add emacs integration

* feat(tilleul): Add server mock

* chore(coverage): Ignore log functions

* feat(tilleul): Transform Connection into a trait

* feat(tilleul): Add complete LSP lifecycle

* chore(tilleul): Rename backend crate to lsp and payload crate to message, madedocumentation and fix clippy issues

* chore(tilleul): Rename server crate in backend, made a directory for tilleul

* feat(tilleul): Add WaitingForInitialisation + Initialised states

* chore(tilleul): Fix moved dependencies

* feat(lsp): Add early parsing from tilleul

* feat(lsp): Add notification dispatcher + Improve request dispatcher

* refactor(lsp): Add LanguageServerBackend

* chore(lsp): Remove LSP states

* chore(lsp): Improve request handling

* feat(lsp): Early request dispatcher

* feat(lsp): Add early message handling + Rename message into payload

* fix(cargo): Use workspace for tilleul

* fix(cargo): Use workspace for tilleul

* feat(lsp): Add early LSP stages

* feat(lsp): Add exit notification

* feat(lsp): Threads + Early IO server

* feat(lsp): Initial commit

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

🦀️🍰🦀️🍰🦀️🍰

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

* chore: update README and parser dependency

* chore(parser, proost): adapt other crates to use new crate elaboration

* feat(elaboration): implement builders in elaboration crate

* fix: remove elaboration dependency in kernel; consequently add VecBuilderTrait

* chore: rename crate utils -> elaboration

* fix(cargo): Better use of SemVer for dependencies

* feat(kernel): Add Buildable trait

* chore(kernel): Rename 'as_buildertrait' as 'as_closure'

* feat(kernel): Remove useless Builder's realise_in_context

* feat(trace): Allow custom T return type on Traceable trait

* docs: fix typos in kernel documentation

* chore: update description of tilleuil crate

* chore: remove useless variable in gitlab-ci.yml

* chore: updating cargo version of the project

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

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

🦀️🍰🦀️🍰🦀️🍰

* fix(parser): declarations can't be initiated with plus, max and imax

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

🦀️🍰🦀️🍰🦀️🍰

* fix(parser): spaces are not allowed when declaring universe variables

eman authored 2 years ago and aalbert committed 2 years ago

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

🦀️🍰🦀️🍰🦀️🍰

* correct super::**

* fix(proost): clippy in tests

* feat(proost): add tests for pretty_print_loc

* feat(proost): cleanup + correct location display

* update: rewritten using evaluator::process(Command::Import)

* feat(proost): remove typecheck file function and use a different arena for each file

* feat:typecheck files without toplevel

* feat(proost): remove typecheck file function and use a different arena for each file

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

🦀️🍰🦀️🍰🦀️🍰

* fix(proost): remove useless map_err in main routine

* fix(proost): add ResultProcess type alias

* chore(proost): make annoying clippy happy

* fix(proost): add String argument to FileError

* fix(proost): simplify error type

* chore(parser): rename Error field from 'loc' to 'location'

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

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

🦀️🍰🦀️🍰🦀️🍰

* chore(tilleul): fix typos in documentation

* chore(tilleul): Add axioms

* chore(tilleul): Add global server tests on unexpected queries

* chore(tilleul): Add UTF-8 message test

* chore(tilleul): Add connection tests

* chore(tilleul): Add message write/read test

* chore(tilleul): Add dispatcher tests

* fix(tilleul): Documentation

* feat(editors): Add emacs integration

* feat(tilleul): Add server mock

* chore(coverage): Ignore log functions

* feat(tilleul): Transform Connection into a trait

* feat(tilleul): Add complete LSP lifecycle

* chore(tilleul): Rename backend crate to lsp and payload crate to message, madedocumentation and fix clippy issues

* chore(tilleul): Rename server crate in backend, made a directory for tilleul

* feat(tilleul): Add WaitingForInitialisation + Initialised states

* chore(tilleul): Fix moved dependencies

* feat(lsp): Add early parsing from tilleul

* feat(lsp): Add notification dispatcher + Improve request dispatcher

* refactor(lsp): Add LanguageServerBackend

* chore(lsp): Remove LSP states

* chore(lsp): Improve request handling

* feat(lsp): Early request dispatcher

* feat(lsp): Add early message handling + Rename message into payload

* fix(cargo): Use workspace for tilleul

* fix(cargo): Use workspace for tilleul

* feat(lsp): Add early LSP stages

* feat(lsp): Add exit notification

* feat(lsp): Threads + Early IO server

* feat(lsp): Initial commit

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

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

🦀️🍰🦀️🍰🦀️🍰

* fix: change lifetime in functions for axiom-term construction

* docs: refer to payloads in builder documentation when missing item documentation

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

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

* chore(kernel): remove unused pointer

* 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): remove unused file

* chore(kernel): coverage

* chore(kernel):add coverage

* fix(kernel): fix comment

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

* chore(kernel): move axiom.rs back to root

* feat(kernel): have working axioms

* feat(kernel): better Axiom type

* fix(kernel): fix memoization issue with WHNF and reductions

* chore(proost): make annoying clippy happy

* chore(parser): make annoying clippy happy

* chore(kernel): make annoying clippy happy

* fix(kernel): fix type inference memoization issue with declarations

* fix(kernel): seamless builder interface for variable/declarations

* fix(kernel): remove unused function

* feat(kernel): generalize recursors reductors

* fix(parser): parsing of vars

* fix(kernel): recursor reduction

* fix(parser):tests

* Revert "feat(all): remove `Var` builder"

This reverts commit 9380961f.

* feat(kernel): add recursor reduction

* feat(kernel): add axiom declarations

* chore(parser): remove outdated TODO

* chore(kernel): add TODO

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

* feat(kernel): add axiom constructor

* feat(all): remove `Var` builder

* fix(kernel): add axiom constructor

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

Closes #79 🐔️👍️
Approved-by: belazy <aarthuur01@gmail.com>

🦀️🍰🦀️🍰🦀️🍰

* fix: Specified which version is used (1.68.0 nightly 2022-12-27)

* feat: Add "nightly" in the rust toolchain

Closes #77 🐔️👍️

🦀️🍰🦀️🍰🦀️🍰

* chore(clippy): Add clippy lint + Fix pattern_type_mismatch lint

* chore: Updated cargo + nix dependencies

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

🦀️🍰🦀️🍰🦀️🍰

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

* chore(type_checker): Change Kind -> ErrorKind

* fix(trace): Apply trace in the right order (depth-first)

* chore(test): Add tests for traces

* chore(parser): Move convert_error into From trait

* feat(loc): Specify localisation for Command::Import

* feat(loc): Specify localisation for Command

* feat(trace): Add trace for realise

* feat(trace): Add Traceable implementation

* chore(utils): Move Errors + Location + Trace into utils crate

* feat(trace): Recover tests

* feat(trace): Add early trace utility

* chore(clippy): Fix clippy issues

* fix(proost): change error display behaviour during file import

* feat(trace): Add term builder into Proost error

* feat(trace): Add trace for infer and imax functions

* feat(trace): Add early trace + error module

* chore(error): Add new method on Error

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