summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--lambda-calcul/rust/src/ast.rs25
-rw-r--r--lambda-calcul/rust/src/lambda.rs32
-rw-r--r--lambda-calcul/rust/src/lib.rs1
-rw-r--r--lambda-calcul/rust/src/types.rs97
-rw-r--r--lambda-calcul/rust/src/web.rs22
5 files changed, 75 insertions, 102 deletions
diff --git a/lambda-calcul/rust/src/ast.rs b/lambda-calcul/rust/src/ast.rs
index 0aaeab4..db3b4a7 100644
--- a/lambda-calcul/rust/src/ast.rs
+++ b/lambda-calcul/rust/src/ast.rs
@@ -6,6 +6,22 @@ use serde::{Deserialize, Serialize};
use std::fmt::{self, Display};
#[derive(Debug, PartialEq, Clone, Serialize, Deserialize)]
+pub enum Type {
+ Int
+}
+
+impl Display for Type {
+ fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
+ write!(f, "Type")
+ }
+}
+
+#[derive(Debug, PartialEq, Clone, Serialize, Deserialize)]
+pub enum TypeError {
+ UnknownType(Value),
+}
+
+#[derive(Debug, PartialEq, Clone, Serialize, Deserialize)]
pub enum Value {
Num(i32),
Bool(bool),
@@ -14,6 +30,13 @@ pub enum Value {
Lam(String, Box<Value>),
Def(String, Box<Value>),
Let(String, Box<Value>, Box<Value>),
+ // typed abstraction
+ TLam(String, Type, Box<Value>),
+ // reified type
+ // this is unsound as we are not in a dependently typed language
+ // but useful to unify external representation (AST). In theory,
+ // we should separate AST from Terms
+ Type(Type)
}
use Value::*;
@@ -50,6 +73,8 @@ impl Display for Value {
Value::Lam(var, body) => write!(f, "(lam {} {})", var, body),
Value::Def(var, value) => write!(f, "(def {} {})", var, value),
Value::Let(var, value, body) => write!(f, "(let ({} {}) {})", var, value, body),
+ Value::TLam(var,typ, body) => write!(f, "(lam ({} {}) {})", var, typ, body),
+ Value::Type(typ) => write!(f, ":{}", typ),
}
}
}
diff --git a/lambda-calcul/rust/src/lambda.rs b/lambda-calcul/rust/src/lambda.rs
index a73ca34..ed1515a 100644
--- a/lambda-calcul/rust/src/lambda.rs
+++ b/lambda-calcul/rust/src/lambda.rs
@@ -96,6 +96,18 @@ fn subst(var: &str, body: &Value, e: &Value) -> Value {
}
}
+pub fn type_of_all(values: &[Value]) -> Vec<Type> {
+ let mut env = Environment::new();
+ values.iter().map(|v| type_of(v, &mut env).unwrap()).collect()
+}
+
+fn type_of(v: &Value, env: &mut Environment) -> Result<Type, TypeError> {
+ match v {
+ Value::Num(_) => Ok(Type::Int),
+ _ => Err(TypeError::UnknownType(v.clone())),
+ }
+}
+
pub fn gensym() -> String {
let mut rng = rand::thread_rng();
@@ -124,6 +136,15 @@ pub fn generate_expr(size: u32, runner: &mut TestRunner) -> Value {
}
}
+pub fn generate_expression_to_type(size: u32, runner: &mut TestRunner) -> Vec<Value> {
+ match size {
+ _ => {
+ let n = any::<u16>().new_tree(runner).unwrap().current();
+ vec![Value::Num(n.into())]
+ }
+ }
+}
+
pub fn generate_exprs(size: u32, runner: &mut TestRunner) -> Vec<Value> {
let sz = (0..size).new_tree(runner).unwrap().current();
(0..sz)
@@ -201,9 +222,9 @@ fn gen_terms(u: u32) -> impl Strategy<Value = Value> {
#[cfg(test)]
mod lambda_test {
- use crate::parser::parse;
+ use crate::{ast::Type, parser::parse};
- use super::{eval_all, eval_whnf, Environment, Value};
+ use super::{Environment, Value, eval_all, eval_whnf, type_of};
fn parse1(string: &str) -> Value {
parse(string).pop().unwrap()
@@ -289,4 +310,11 @@ mod lambda_test {
let values = parse("(let (id (lam x x)) (let (foo 12) (id foo)))");
assert_eq!(vec![Value::Num(12)], eval_all(&values));
}
+
+ #[test]
+ fn type_of_a_number_is_int() {
+ let value = parse1("12");
+ let ty = type_of(&value, &mut Environment::new()).unwrap();
+ assert_eq!(Type::Int, ty);
+ }
}
diff --git a/lambda-calcul/rust/src/lib.rs b/lambda-calcul/rust/src/lib.rs
index 53f4c99..a8cf18e 100644
--- a/lambda-calcul/rust/src/lib.rs
+++ b/lambda-calcul/rust/src/lib.rs
@@ -2,4 +2,3 @@ pub mod ast;
pub mod io;
pub mod lambda;
pub mod parser;
-mod types;
diff --git a/lambda-calcul/rust/src/types.rs b/lambda-calcul/rust/src/types.rs
deleted file mode 100644
index e91d57e..0000000
--- a/lambda-calcul/rust/src/types.rs
+++ /dev/null
@@ -1,97 +0,0 @@
-use crate::ast::Value;
-use proptest::prelude::*;
-use proptest::prop_oneof;
-use std::collections::BTreeMap;
-
-type Name = String;
-
-#[derive(Debug, Clone, PartialEq)]
-enum Type {
- Int,
- Bool,
-}
-
-fn any_type() -> impl Strategy<Value = Type> {
- prop_oneof![Just(Type::Int), Just(Type::Bool),]
-}
-
-struct Context {
- context: BTreeMap<Name, Type>,
-}
-
-impl Context {
- pub fn empty() -> Self {
- Context {
- context: BTreeMap::new(),
- }
- }
-
- pub fn bind(&mut self, sym: Name, ty: Type) -> &mut Self {
- self.context.insert(sym, ty);
- self
- }
-
- pub fn type_of(&self, val: &Value) -> Option<Type> {
- use Value::*;
-
- match val {
- Num(_) => Some(Type::Int),
- Bool(_) => Some(Type::Bool),
- Sym(s) => self.context.get(s).cloned(),
- _ => None,
- }
- }
-}
-
-#[cfg(test)]
-mod tests {
-
- use super::*;
- use crate::ast::Value::*;
- use proptest::prelude::*;
-
- proptest! {
-
- #[test]
- fn any_int_value_has_type_int(n in any::<i32>().prop_map(Num)) {
- let ctx = Context::empty();
-
- let ty = ctx.type_of(&n);
-
- assert_eq!(Some(Type::Int), ty);
- }
-
- #[test]
- fn any_bool_value_has_type_Bool(n in any::<bool>().prop_map(Bool)) {
- let ctx = Context::empty();
-
- let ty = ctx.type_of(&n);
-
- assert_eq!(Some(Type::Bool), ty);
- }
-
- #[test]
- fn any_bound_variable_has_bound_type(s in crate::ast::identifier(), t in any_type()) {
- let mut ctx = Context::empty();
- ctx.bind(s.clone(), t.clone());
-
- let ty = ctx.type_of(&Sym(s));
-
- assert_eq!(Some(t), ty);
- }
-
- #[test]
- fn any_unbound_variable_has_no_type(s in crate::ast::identifier()) {
- let mut ctx = Context::empty();
-
- let ty = ctx.type_of(&Sym(s));
-
- assert_eq!(None, ty);
- }
-
- #[test]
- fn def_symbol_has_type_of_its_body(s in crate::ast::identifier(), t in any_type()) {
- }
-
- }
-}
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 {
generated by cgit v1.2.3 (git 2.39.1) at 2026-02-05 22:20:12 +0000