summaryrefslogtreecommitdiff
path: root/lambda-calcul/rust/src/web.rs
diff options
context:
space:
mode:
Diffstat (limited to 'lambda-calcul/rust/src/web.rs')
-rw-r--r--lambda-calcul/rust/src/web.rs22
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 {