Resolve "proost fonctionality and UI" ✨️

Closes #22 et #7 🐔️👍️
Approved-by: aalbert <augustin.albert@bleu-azure.fr>
Approved-by: belazy <aarthuur01@gmail.com>
Approved-by: loutr <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

kernel/src/type_checker.rs

@@ -424,4 +424,24 @@ mod tests {
         );
         assert!(ty.conversion(&Type(0.into()), &Environment::new(), 0.into()))
     }
+
+    #[test]
+    fn prod_var() {
+        let ty = Prod(box Prop, box Prod(box Var(1.into()), box Var(2.into())));
+        let t = Abs(box Prop, box Abs(box Var(1.into()), box Var(1.into())));
+        assert!(t.check(&ty, &Environment::new()).is_ok())
+    }
+
+    #[test]
+    fn univ_reduc() {
+        let ty = App(
+            box Abs(box Prop, box Type(BigUint::from(0_u64).into())),
+            box Prod(box Prop, box Var(1.into())),
+        );
+        assert!(ty.conversion(
+            &Type(BigUint::from(0_u64).into()),
+            &Environment::new(),
+            0.into()
+        ))
+    }
 }