summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--lambda-calcul/rust/src/ast.rs4
-rw-r--r--lambda-calcul/rust/src/lambda.rs73
-rw-r--r--lambda-calcul/rust/src/web.rs17
3 files changed, 73 insertions, 21 deletions
diff --git a/lambda-calcul/rust/src/ast.rs b/lambda-calcul/rust/src/ast.rs
index db3b4a7..18aaaa7 100644
--- a/lambda-calcul/rust/src/ast.rs
+++ b/lambda-calcul/rust/src/ast.rs
@@ -7,7 +7,8 @@ use std::fmt::{self, Display};
#[derive(Debug, PartialEq, Clone, Serialize, Deserialize)]
pub enum Type {
- Int
+ Num,
+ Bool,
}
impl Display for Type {
@@ -19,6 +20,7 @@ impl Display for Type {
#[derive(Debug, PartialEq, Clone, Serialize, Deserialize)]
pub enum TypeError {
UnknownType(Value),
+ UnboundVariable(String),
}
#[derive(Debug, PartialEq, Clone, Serialize, Deserialize)]
diff --git a/lambda-calcul/rust/src/lambda.rs b/lambda-calcul/rust/src/lambda.rs
index ed1515a..c624b19 100644
--- a/lambda-calcul/rust/src/lambda.rs
+++ b/lambda-calcul/rust/src/lambda.rs
@@ -10,12 +10,12 @@ use std::collections::HashMap;
use crate::ast::*;
#[derive(Debug, PartialEq)]
-pub struct Environment<'a> {
- parent: Box<Option<&'a Environment<'a>>>,
- bindings: HashMap<String, Value>,
+pub struct Environment<'a, T> {
+ parent: Box<Option<&'a Environment<'a, T>>>,
+ bindings: HashMap<String, T>,
}
-impl<'a> Environment<'a> {
+impl<'a, T: Clone> Environment<'a, T> {
pub fn new() -> Self {
Environment {
parent: Box::new(None),
@@ -23,7 +23,7 @@ impl<'a> Environment<'a> {
}
}
- fn bind(&mut self, var: &str, value: &Value) {
+ fn bind(&mut self, var: &str, value: &T) {
self.bindings.insert(var.to_string(), value.clone());
}
@@ -34,7 +34,7 @@ impl<'a> Environment<'a> {
}
}
- fn lookup(&self, var: &str) -> Option<&Value> {
+ fn lookup(&self, var: &str) -> Option<&T> {
self.bindings.get(var).or_else(|| match *self.parent {
Some(parent) => parent.lookup(var),
None => None,
@@ -42,7 +42,7 @@ impl<'a> Environment<'a> {
}
}
-impl<'a> Default for Environment<'a> {
+impl<'a, T: Clone> Default for Environment<'a, T> {
fn default() -> Self {
Self::new()
}
@@ -58,7 +58,7 @@ pub fn eval_all(values: &[Value]) -> Vec<Value> {
///
/// call-by-name reduces the leftmost outermost redex first, which is
/// not under a lambda abstraction.
-pub fn eval_whnf(arg: &Value, env: &mut Environment) -> Value {
+pub fn eval_whnf(arg: &Value, env: &mut Environment<Value>) -> Value {
match arg {
Value::Def(var, value) => {
env.bind(var, value);
@@ -98,14 +98,22 @@ 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()
+ values
+ .iter()
+ .map(|v| type_of(v, &mut env).unwrap())
+ .collect()
}
-fn type_of(v: &Value, env: &mut Environment) -> Result<Type, TypeError> {
+fn type_of(v: &Value, env: &mut Environment<Type>) -> Result<Type, TypeError> {
match v {
- Value::Num(_) => Ok(Type::Int),
+ Value::Num(_) => Ok(Type::Num),
+ Value::Bool(_) => Ok(Type::Bool),
+ Value::Sym(s) => match env.lookup(s) {
+ Some(ty) => Ok(ty.clone()),
+ None => Err(TypeError::UnboundVariable(s.clone())),
+ },
_ => Err(TypeError::UnknownType(v.clone())),
- }
+ }
}
pub fn gensym() -> String {
@@ -138,10 +146,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 {
- _ => {
+ 0 => {
let n = any::<u16>().new_tree(runner).unwrap().current();
vec![Value::Num(n.into())]
- }
+ },
+ _ => {
+ let n = any::<bool>().new_tree(runner).unwrap().current();
+ vec![Value::Bool(n.into())]
+ },
+
}
}
@@ -224,7 +237,7 @@ fn gen_terms(u: u32) -> impl Strategy<Value = Value> {
mod lambda_test {
use crate::{ast::Type, parser::parse};
- use super::{Environment, Value, eval_all, eval_whnf, type_of};
+ use super::{eval_all, eval_whnf, type_of, Environment, Value};
fn parse1(string: &str) -> Value {
parse(string).pop().unwrap()
@@ -315,6 +328,34 @@ mod lambda_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);
+ assert_eq!(Type::Num, ty);
+ }
+
+ #[test]
+ fn type_of_a_boolean_is_bool() {
+ let value = parse1("true");
+ let ty = type_of(&value, &mut Environment::new()).unwrap();
+ assert_eq!(Type::Bool, ty);
+ }
+
+ #[test]
+ fn type_of_a_bound_variable_is_looked_up_in_context() {
+ let value = parse1("x");
+ let mut ctx = Environment::new();
+ ctx.bind("x", &Type::Bool);
+
+ let ty = type_of(&value, &mut ctx).unwrap();
+
+ assert_eq!(Type::Bool, ty);
+ }
+
+ #[test]
+ fn type_of_an_unbound_variable_yields_an_error() {
+ let value = parse1("x");
+ let mut ctx = Environment::new();
+
+ let ty = type_of(&value, &mut ctx);
+
+ assert!(ty.is_err());
}
}
diff --git a/lambda-calcul/rust/src/web.rs b/lambda-calcul/rust/src/web.rs
index 27aed21..5ad48bd 100644
--- a/lambda-calcul/rust/src/web.rs
+++ b/lambda-calcul/rust/src/web.rs
@@ -13,7 +13,10 @@ use std::{collections::HashMap, sync::Arc};
use tokio::task::{self, JoinHandle};
use uuid::Uuid;
-use lambda::lambda::{Environment, eval_all, eval_whnf, generate_expr, generate_expression_to_type, generate_exprs, gensym, type_of_all};
+use lambda::lambda::{
+ eval_all, eval_whnf, generate_expr, generate_expression_to_type, generate_exprs, gensym,
+ type_of_all, Environment,
+};
use lambda::parser::{parse, parse_total};
#[derive(Debug, PartialEq, Serialize, Deserialize, Clone)]
@@ -96,6 +99,8 @@ enum TestResult {
}
impl Client {
+ const TYPING_GRADE: u8 = 20;
+
fn new(url: String, name: String, delay: Duration, encoding: AstEncoding) -> Self {
let id = Uuid::new_v4();
let runner = TestRunner::new_with_rng(
@@ -119,7 +124,7 @@ impl Client {
}
fn generate_expr(&mut self) -> (Vec<Value>, Vec<Value>) {
- if self.grade >= 20 {
+ if self.grade >= Self::TYPING_GRADE {
self.generate_expression_to_type()
} else if self.grade >= 10 {
self.generate_exprs()
@@ -131,8 +136,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();
+ let input =
+ generate_expression_to_type((self.grade - Self::TYPING_GRADE).into(), &mut self.runner);
+ let expected = type_of_all(&input)
+ .iter()
+ .map(|t| Value::Type(t.clone()))
+ .collect();
(input, expected)
}
generated by cgit v1.2.3 (git 2.39.1) at 2026-02-05 22:25:48 +0000