Skip to content
Snippets Groups Projects
  1. Oct 28, 2022
  2. Oct 27, 2022
    • aalbert's avatar
      Resolve "Bug rev parser" ✨️ · 1c6e1940
      aalbert authored
      Closes #30 🐔️👍️
      
      🦀️🍰🦀️🍰🦀️🍰
      
      * fix(parser)
      1c6e1940
    • v-lafeychine's avatar
      Resolve "proost fonctionality and UI" ✨️ · 1ffe4f63
      v-lafeychine authored and aalbert's avatar aalbert committed
      Closes #22 et #7 🐔️👍️
      Approved-by: default avataraalbert <augustin.albert@bleu-azure.fr>
      Approved-by: default avatarbelazy <aarthuur01@gmail.com>
      Approved-by: default avatarloutr <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
      1ffe4f63
  3. Oct 24, 2022
  4. Oct 22, 2022
    • belazy's avatar
      Resolve "Type-checker doesn't use the global context" ✨️ · 1a7107b8
      belazy authored and v-lafeychine's avatar v-lafeychine committed
      Closes #17 🐔️👍️
      Approved-by: default avatarbelazy <aarthuur01@gmail.com>
      Approved-by: default avatarloutr <loutr@crans.org>
      Approved-by: default avataraalbert <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`
      1a7107b8
  5. Oct 21, 2022
  6. Oct 20, 2022
    • belazy's avatar
      9-add-a-basic-type-checker ✨️ · d100c562
      belazy authored and v-lafeychine's avatar v-lafeychine committed
      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)
      d100c562
    • v-lafeychine's avatar
      Resolve "Coverage on Pipelines" ✨️ · 4ff816e4
      v-lafeychine authored and aalbert's avatar aalbert committed
      Closes #16 🐔️👍️
      Approved-by: default avatarloutr <loutr@crans.org>
      Approved-by: default avataraalbert <augustin.albert@bleu-azure.fr>
      
      🦀️🍰🦀️🍰🦀️🍰
      
      * fix(nix): Add rust-src in rust profile
      
      * feat(ci): Add stages for better-CI understanding
      
      * feat(ci): Add coverage
      4ff816e4
  7. Oct 18, 2022
  8. Oct 17, 2022
    • aalbert's avatar
      feat(parser): Add new syntaxic sugar and meaningfull error messages, add more... ✨️ · cd56335d
      aalbert authored and loutr's avatar loutr committed
      Closes #10 🐔️👍️
      Approved-by: default avatarv-lafeychine <vincent.lafeychine@proton.me>
      Approved-by: default avataraalbert <augustin.albert@bleu-azure.fr>
      Approved-by: default avatarloutr <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
      cd56335d
  9. Oct 10, 2022
  10. Oct 09, 2022
  11. Oct 07, 2022
  12. Oct 06, 2022
    • aalbert's avatar
      ✨️ Resolve "Add proost program (CLI)" ‼️✨️ · c47a91c0
      aalbert authored and loutr's avatar loutr committed
      Closes #5
      
      🦀️🍰️🦀️🍰️🦀️🍰️🦀️🍰️
      Approved-by: default avatarloutr <loutr@crans.org>
      Approved-by: default avatarv-lafeychine <vincent.lafeychine@proton.me>
      
      🦀️🍰️🦀️🍰️🦀️🍰️🦀️🍰️
      * fix(proost): iterates over arguments as shared immutable references as to prevent cloning
      
      * chore(proost): Add spaces
      
      * feat(proost): Add banner support for CLI
      
      * feat(proost): Add command line argument support with clap
      
      * feat(proost): Add basic CLI and file handling
      c47a91c0
    • aalbert's avatar
      Resolve "Pest parser" · bcb0e9fd
      aalbert authored
      Closes #3
      
      Approved-by: default avatarbelazy <aarthuur01@gmail.com>
      Approved-by: default avataraalbert <augustin.albert@bleu-azure.fr>
      
      * fix(parser): Fix minor issues (impl PartialEq for tests)
      
      * feat(parser): Add more inclusive syntax
      
      * feat(parser): Add informative message for free variables
      
      * fix(parser): Fix a conversion bug
      
      * feat(parser,core): Move classic term from core into parser
      
      * feat(parser): Conversion from classic terms to terms
      
      * feat(core): Add conversion from classic term to term
      
      * chore(parser): Rename pest file
      
      * chore(core): Move classic terms in its own file
      
      * feat(parser): Add ClassicTerm with variables for easier user input
      
      * fix(parser): Reorganize lib.rs and parser.rs
      
      * fix(parser): Reorganize lib.rs and parser.rs
      
      * fix(parser): Reorganize lib.rs and parser.rs
      
      * chore(parser): Rename tests files
      
      * chore(parser): Rename tests files
      
      * feat(parser): add parser for terms, commands and files
      
      * feat(parser): add parser for terms, commands and files
      
      * feat(parser): add parser for terms, commands and files
      
      * feat(parser): add parser for terms, commands and files
      
      * feat(parser): add parser for terms, commands and files
      
      * feat(parser): add parser for terms, commands and files
      
      * feat(parser): add parser for terms, commands and files
      
      * chore(core): add license
      
      * chore(parser): remove warnings
      
      * chore(core): format files
      
      * chore(parser): remove warnings
      
      * chore(parser): format code
      
      * fix(core): add lib.rs
      
      * feat(term): Add early Term struct + Display trait
      
      * feat(parser): add parser crate and pest config
      bcb0e9fd
  13. Sep 30, 2022
  14. Sep 29, 2022
  15. Sep 22, 2022
  16. Sep 21, 2022
  17. Sep 15, 2022
  18. Sep 13, 2022
Loading