Skip to content
Snippets Groups Projects
  1. Dec 04, 2022
    • v-lafeychine's avatar
      Resolve "Infrastructure improvement" ✨️ · bbdd1df8
      v-lafeychine authored and loutr's avatar loutr committed
      Closes #40 🐔️👍️
      Approved-by: default avataraalbert <augustin.albert@bleu-azure.fr>
      Approved-by: default avatarloutr <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
      bbdd1df8
    • aalbert's avatar
      Resolve "Add file handling to proost" ✨️ · dc1fc185
      aalbert authored
      Closes #27, #29 et #36 🐔️👍️
      Approved-by: default avatarloutr <loutr@crans.org>
      Approved-by: default avataraalbert <augustin.albert@bleu-azure.fr>
      Approved-by: default avatarbelazy <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
      dc1fc185
  2. Dec 01, 2022
  3. Nov 30, 2022
    • loutr's avatar
      Uniform Kernel Documentation ✨️ · 0d832e96
      loutr authored
      Closes #42 🐔️👍️
      Approved-by: default avatarbelazy <aarthuur01@gmail.com>
      Approved-by: default avatarv-lafeychine <vincent.lafeychine@proton.me>
      Approved-by: default avataraalbert <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
      0d832e96
  4. Nov 26, 2022
    • loutr's avatar
      Resolve "Refactor memory model of type checker" ✨️ · 066c0829
      loutr authored
      Closes #15 🐔️👍️
      Approved-by: default avataraalbert <augustin.albert@bleu-azure.fr>
      Approved-by: default avatarv-lafeychine <vincent.lafeychine@proton.me>
      Approved-by: default avatarbelazy <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
      066c0829
    • aalbert's avatar
      Resolve "improve README" ✨️ · dc410508
      aalbert authored and v-lafeychine's avatar v-lafeychine committed
      Closes #37 🐔️👍️
      Approved-by: default avataraalbert <augustin.albert@bleu-azure.fr>
      Approved-by: default avatarbelazy <aarthuur01@gmail.com>
      Approved-by: default avatarv-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's avatar
      Resolve "Add functionnalities to proost (toplevel)" ✨️ · 1f0aa51e
      aalbert authored and v-lafeychine's avatar v-lafeychine committed
      Closes #39 🐔️👍️
      Approved-by: default avataraalbert <augustin.albert@bleu-azure.fr>
      Approved-by: default avatarv-lafeychine <vincent.lafeychine@proton.me>
      Approved-by: default avatarbelazy <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
  5. Nov 10, 2022
    • aalbert's avatar
      Resolve "update specs" ✨️ · a28c6526
      aalbert authored
      Closes #35 🐔️👍️
      Approved-by: default avataraalbert <augustin.albert@bleu-azure.fr>
      Approved-by: default avatarloutr <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
      a28c6526
  6. Nov 09, 2022
  7. Nov 04, 2022
    • v-lafeychine's avatar
      Resolve "Kernel errors" ✨️ · a636b12c
      v-lafeychine authored and loutr's avatar loutr committed
      Closes #19 🐔️👍️
      Approved-by: default avataraalbert <augustin.albert@bleu-azure.fr>
      Approved-by: default avatarbelazy <aarthuur01@gmail.com>
      Approved-by: default avatarloutr <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
      a636b12c
  8. Nov 01, 2022
    • aalbert's avatar
      Resolve " tests for parser" ✨️ · 328982eb
      aalbert authored
      Closes #8 🐔️👍️
      Approved-by: default avatarv-lafeychine <vincent.lafeychine@proton.me>
      Approved-by: default avatarbelazy <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
      328982eb
  9. Oct 29, 2022
  10. Oct 28, 2022
  11. 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
  12. Oct 24, 2022
  13. 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
  14. Oct 21, 2022
  15. 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
  16. Oct 18, 2022
  17. 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
  18. Oct 10, 2022
  19. Oct 09, 2022
  20. Oct 07, 2022
  21. 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
  22. Sep 30, 2022
  23. Sep 29, 2022
  24. Sep 22, 2022
  25. Sep 21, 2022
  26. Sep 15, 2022
  27. Sep 13, 2022
Loading