feat: introduce typing of expressions

1 files changed, 20 insertions, 2 deletions

diff --git a/lambda-calcul/rust/src/web.rs b/lambda-calcul/rust/src/web.rs
index 5bc8c3f..27aed21 100644
--- a/lambda-calcul/rust/src/web.rs
+++ b/lambda-calcul/rust/src/web.rs
@@ -13,7 +13,7 @@ use std::{collections::HashMap, sync::Arc};
 use tokio::task::{self, JoinHandle};
 use uuid::Uuid;
 
-use lambda::lambda::{eval_all, eval_whnf, generate_expr, generate_exprs, gensym, Environment};
+use lambda::lambda::{Environment, eval_all, eval_whnf, generate_expr, generate_expression_to_type, generate_exprs, gensym, type_of_all};
 use lambda::parser::{parse, parse_total};
 
 #[derive(Debug, PartialEq, Serialize, Deserialize, Clone)]
@@ -119,7 +119,9 @@ impl Client {
     }
 
     fn generate_expr(&mut self) -> (Vec<Value>, Vec<Value>) {
-        if self.grade >= 10 {
+        if self.grade >= 20 {
+            self.generate_expression_to_type()
+        } else if self.grade >= 10 {
             self.generate_exprs()
         } else {
             let input = generate_expr(self.grade.into(), &mut self.runner);
@@ -128,6 +130,12 @@ impl Client {
         }
     }
 
+    fn generate_expression_to_type(&mut self) -> (Vec<Value>, Vec<Value>) {
+        let input = generate_expression_to_type(self.grade.into(), &mut self.runner);
+        let expected = type_of_all(&input).iter().map(|t| Value::Type(t.clone())).collect();
+        (input, expected)
+    }
+
     fn generate_exprs(&mut self) -> (Vec<Value>, Vec<Value>) {
         let input = generate_exprs(self.grade.into(), &mut self.runner);
         let expected = eval_all(&input);
@@ -787,6 +795,16 @@ mod app_tests {
     }
 
     #[test]
+    async fn client_generates_typing_expression_at_level_20() {
+        let mut client = client();
+        client.grade = 20;
+
+        let (input, _) = client.generate_expr();
+
+        assert!(!input.is_empty());
+    }
+
+    #[test]
     async fn client_increases_grade_on_successful_test() {
         let mut client = client();
         let test = Test {