Skip to content
Snippets Groups Projects
  1. Dec 26, 2022
  2. Dec 24, 2022
    • belazy's avatar
      Resolve "Add Universe Polymorphism" ✨️ · 8b20ac80
      belazy authored and loutr's avatar loutr committed
      Closes #28 🐔️👍️
      Approved-by: default avatarbelazy <aarthuur01@gmail.com>
      Approved-by: default avataraalbert <augustin.albert@bleu-azure.fr>
      Approved-by: default avatarv-lafeychine <vincent.lafeychine@proton.me>
      Approved-by: default avatarloutr <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
      8b20ac80
Loading