diff options
Diffstat (limited to 'tests/test_checking.rs')
| -rw-r--r-- | tests/test_checking.rs | 51 |
1 files changed, 27 insertions, 24 deletions
diff --git a/tests/test_checking.rs b/tests/test_checking.rs index a4b5fd3..286283b 100644 --- a/tests/test_checking.rs +++ b/tests/test_checking.rs @@ -7,14 +7,14 @@ use chrysanthemum::util::*; // rust you KNOW these are &'static strs const sanity_check: &'static str = "413: int"; -const negate: &'static str = "(λx. if x then 0 else 1): (bool -> bool)"; +const negate: &'static str = "(λx. if x then false else true): (bool -> bool)"; const basic_abstraction: &'static str = "(λx. x): (int -> int)"; const basic_application: &'static str = "((λx. x): (int -> int)) 413"; const correct_cond_abs: &'static str = "(λx. if x then 1 else 0): (bool -> int)"; -const correct_cond: &'static str = "if 0 then 1: nat else 0: nat"; +const correct_cond: &'static str = "if false then 1: nat else 0: nat"; const not_inferrable: &'static str = "(λx. (λy. (λz. if x then y else z)))"; -const incorrect_branches: &'static str = "if 0: bool then 1: bool else 2: int"; -const incorrect_cond_abs: &'static str = "(λx. if x then 1: bool else 0: bool): (int -> bool)"; +const incorrect_branches: &'static str = "if false: bool then true: bool else 2: int"; +const incorrect_cond_abs: &'static str = "(λx. if x then true: bool else false: bool): (int -> bool)"; #[test] fn test_parsing_succeeds() { @@ -31,31 +31,34 @@ fn test_parsing_succeeds() { #[test] fn test_inference() { - assert_eq!(infer(Context::new(), parse_lambda(sanity_check).unwrap()), Ok(Int)); - assert_eq!(infer(Context::new(), parse_lambda(negate).unwrap()), Ok(Func(Bool, Bool))); - assert_eq!(infer(Context::new(), parse_lambda(basic_abstraction).unwrap()), Ok(Func(Int, Int))); - assert_eq!(infer(Context::new(), parse_lambda(basic_application).unwrap()), Ok(Int)); - assert_eq!(infer(Context::new(), parse_lambda(correct_cond_abs).unwrap()), Ok(Func(Bool, Int))); - assert_eq!(infer(Context::new(), parse_lambda(correct_cond).unwrap()), Ok(Nat)); - assert!(infer(Context::new(), parse_lambda(not_inferrable).unwrap()).is_err()); - assert!(infer(Context::new(), parse_lambda(incorrect_branches).unwrap()).is_err()); - assert!(infer(Context::new(), parse_lambda(incorrect_cond_abs).unwrap()).is_err()); + let context = Context::new(); + assert_eq!(infer(&context, parse_lambda(sanity_check).unwrap()), Ok(Int)); + assert_eq!(infer(&context, parse_lambda(negate).unwrap()), Ok(Func(Bool, Bool))); + assert_eq!(infer(&context, parse_lambda(basic_abstraction).unwrap()), Ok(Func(Int, Int))); + assert_eq!(infer(&context, parse_lambda(basic_application).unwrap()), Ok(Int)); + assert_eq!(infer(&context, parse_lambda(correct_cond_abs).unwrap()), Ok(Func(Bool, Int))); + assert_eq!(infer(&context, parse_lambda(correct_cond).unwrap()), Ok(Nat)); + assert!(infer(&context, parse_lambda(not_inferrable).unwrap()).is_err()); + assert!(infer(&context, parse_lambda(incorrect_branches).unwrap()).is_err()); + assert!(infer(&context, parse_lambda(incorrect_cond_abs).unwrap()).is_err()); } #[test] fn test_checking() { + let context = Context::new(); + // uninteresting - assert!(check(Context::new(), parse_lambda(sanity_check).unwrap(), Int).is_ok()); - assert!(check(Context::new(), parse_lambda(negate).unwrap(), Func(Bool, Bool)).is_ok()); - assert!(check(Context::new(), parse_lambda(basic_abstraction).unwrap(), Func(Int, Int)).is_ok()); - assert!(check(Context::new(), parse_lambda(basic_application).unwrap(), Int).is_ok()); - assert!(check(Context::new(), parse_lambda(correct_cond_abs).unwrap(), Func(Bool, Int)).is_ok()); - assert!(check(Context::new(), parse_lambda(correct_cond).unwrap(), Nat).is_ok()); - assert!(check(Context::new(), parse_lambda(incorrect_branches).unwrap(), Unit).is_err()); - assert!(check(Context::new(), parse_lambda(incorrect_cond_abs).unwrap(), Error).is_err()); + assert!(check(&context, parse_lambda(sanity_check).unwrap(), &Int).is_ok()); + assert!(check(&context, parse_lambda(negate).unwrap(), &Func(Bool, Bool)).is_ok()); + assert!(check(&context, parse_lambda(basic_abstraction).unwrap(), &Func(Int, Int)).is_ok()); + assert!(check(&context, parse_lambda(basic_application).unwrap(), &Int).is_ok()); + assert!(check(&context, parse_lambda(correct_cond_abs).unwrap(), &Func(Bool, Int)).is_ok()); + assert!(check(&context, parse_lambda(correct_cond).unwrap(), &Nat).is_ok()); + assert!(check(&context, parse_lambda(incorrect_branches).unwrap(), &Unit).is_err()); + assert!(check(&context, parse_lambda(incorrect_cond_abs).unwrap(), &Error).is_err()); // more fun - assert!(check(Context::new(), parse_lambda(not_inferrable).unwrap(), Func(Bool, Func(Int, Func(Int, Int)))).is_ok()); - assert!(check(Context::new(), parse_lambda(not_inferrable).unwrap(), Func(Bool, Func(Nat, Func(Nat, Nat)))).is_ok()); - assert!(check(Context::new(), parse_lambda(not_inferrable).unwrap(), Func(Bool, Func(Unit, Func(Unit, Unit)))).is_ok()); + assert!(check(&context, parse_lambda(not_inferrable).unwrap(), &Func(Bool, Func(Int, Func(Int, Int)))).is_ok()); + assert!(check(&context, parse_lambda(not_inferrable).unwrap(), &Func(Bool, Func(Nat, Func(Nat, Nat)))).is_ok()); + assert!(check(&context, parse_lambda(not_inferrable).unwrap(), &Func(Bool, Func(Unit, Func(Unit, Unit)))).is_ok()); } |