WIP

.travis.yml

@@ -1,7 +1,7 @@
 language: rust
 cache: cargo
 rust:
-  - 1.26.0
+  - 1.27.0
   - stable
   - beta
   - nightly

moniker/Cargo.toml

@@ -24,10 +24,12 @@ default = ["moniker-derive"]
 [dependencies]
 lazy_static = "1.0"
 moniker-derive = { path = "../moniker-derive", version = "0.1.0", optional = true }
+proptest = { version = "0.8.3", optional = true }
 codespan = { version = "0.1.2", optional = true }
 
 [dev-dependencies]
 im = "10.2"
+proptest = "0.8.3"
 
 [[example]]
 name = "lc"
@@ -47,7 +49,7 @@ required-features = ["moniker-derive"]
 
 [[example]]
 name = "stlc"
-required-features = ["moniker-derive"]
+required-features = ["moniker-derive", "proptest"]
 
 [[example]]
 name = "stlc_data"

moniker/examples/stlc.rs

@@ -7,9 +7,12 @@
 extern crate im;
 #[macro_use]
 extern crate moniker;
+#[macro_use]
+extern crate proptest;
 
 use im::HashMap;
 use moniker::{BoundTerm, Embed, FreeVar, Scope, Var};
+use proptest::prelude::*;
 use std::rc::Rc;
 
 /// Types
@@ -184,6 +187,91 @@ pub fn infer(context: &Context, expr: &RcExpr) -> Result<RcType, String> {
     }
 }
 
+// RcType strategies
+
+fn arb_ty() -> impl Strategy<Value = RcType> {
+    prop_oneof![
+        Just(RcType::from(Type::Int)),
+        Just(RcType::from(Type::Float)),
+        Just(RcType::from(Type::String)),
+    ].prop_recursive(8, 256, 2, |inner| {
+        (inner.clone(), inner.clone())
+            .prop_map(|(param, body)| RcType::from(Type::Arrow(param, body)))
+    })
+}
+
+// Literal strategies
+
+fn arb_literal_int() -> impl Strategy<Value = Literal> {
+    any::<i32>().prop_map(Literal::Int)
+}
+
+fn arb_literal_float() -> impl Strategy<Value = Literal> {
+    any::<f32>().prop_map(Literal::Float)
+}
+
+fn arb_literal_string() -> impl Strategy<Value = Literal> {
+    any::<String>().prop_map(Literal::String)
+}
+
+fn arb_literal() -> impl Strategy<Value = Literal> {
+    prop_oneof![arb_literal_int(), arb_literal_float(), arb_literal_string()]
+}
+
+// RcExpr strategies
+
+fn arb_expr_literal(literal: impl Strategy<Value = Literal>) -> impl Strategy<Value = RcExpr> {
+    literal.prop_map(|lit| RcExpr::from(Expr::Literal(lit)))
+}
+
+fn arb_expr() -> impl Strategy<Value = RcExpr> {
+    prop_oneof![arb_expr_literal(arb_literal())]
+}
+
+// Property tests
+
+proptest! {
+    #[test]
+    fn check_int(expr in arb_expr_literal(arb_literal_int())) {
+        check(&Context::new(), &expr, &RcType::from(Type::Int)).unwrap();
+    }
+
+    #[test]
+    fn check_float(expr in arb_expr_literal(arb_literal_float())) {
+        check(&Context::new(), &expr, &RcType::from(Type::Float)).unwrap();
+    }
+
+    #[test]
+    fn check_string(expr in arb_expr_literal(arb_literal_string())) {
+        check(&Context::new(), &expr, &RcType::from(Type::String)).unwrap();
+    }
+
+    #[test]
+    fn infer_int(expr in arb_expr_literal(arb_literal_int())) {
+        assert_term_eq!(infer(&Context::new(), &expr).unwrap(), RcType::from(Type::Int));
+    }
+
+    #[test]
+    fn infer_float(expr in arb_expr_literal(arb_literal_float())) {
+        assert_term_eq!(infer(&Context::new(), &expr).unwrap(), RcType::from(Type::Float));
+    }
+
+    #[test]
+    fn infer_string(expr in arb_expr_literal(arb_literal_string())) {
+        assert_term_eq!(infer(&Context::new(), &expr).unwrap(), RcType::from(Type::String));
+    }
+
+    #[test]
+    fn apply_literal_is_err(
+        expr1 in arb_expr_literal(arb_literal()),
+        expr2 in arb_expr_literal(arb_literal()),
+    ) {
+        infer(&Context::new(), &RcExpr::from(Expr::App(expr1, expr2))).unwrap_err();
+    }
+}
+
+// Unit tests
+
 #[test]
 fn test_infer() {
     // expr = (\x : Int -> x)

moniker/src/lib.rs

@@ -60,6 +60,9 @@ extern crate lazy_static;
 #[allow(unused_imports)]
 #[macro_use]
 extern crate moniker_derive;
+#[cfg(feature = "proptest")]
+#[macro_use]
+extern crate proptest;
 
 #[cfg(feature = "moniker-derive")]
 #[doc(hidden)]

moniker/src/var.rs

@@ -24,6 +24,14 @@ impl fmt::Display for GenId {
     }
 }
 
+#[cfg(feature = "proptest")]
+proptest! {
+    #[test]
+    fn test_fresh_gen_id(_ in 0..100) {
+        prop_assert_ne!(GenId::fresh(), GenId::fresh());
+    }
+}
+
 /// A free variable
 #[derive(Debug, Clone, PartialEq, Eq, Hash)]
 pub enum FreeVar<Ident> {