summaryrefslogtreecommitdiff
path: root/lambda-calcul/rust/src/lambda.rs
diff options
context:
space:
mode:
Diffstat (limited to 'lambda-calcul/rust/src/lambda.rs')
-rw-r--r--lambda-calcul/rust/src/lambda.rs32
1 files changed, 30 insertions, 2 deletions
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);
+ }
}