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