Merge pull request #125 from yeslogic/brendanzab/cond-types

First pass on refinement types
yeslogic · Nov 7, 2018 · 9f12946 · 9f12946
2 parents ef8ec16 + bf4e43f
commit 9f12946
Show file tree

Hide file tree

Showing 16 changed files with 375 additions and 122 deletions.
diff --git a/src/semantics/context.rs b/src/semantics/context.rs
@@ -151,6 +151,7 @@ fn default_extern_definitions() -> HashMap<&'static str, Extern> {
         "string-eq" => prim!(fn(x: String, y: String) -> bool { x == y }),
         "bool-eq" => prim!(fn(x: bool, y: bool) -> bool { x == y }),
         "char-eq" => prim!(fn(x: char, y: char) -> bool { x == y }),
+        "int-eq" => prim!(fn(x: BigInt, y: BigInt) -> bool { x == y }),
         "f32-eq" => prim!(fn(x: f32, y: f32) -> bool { f32::eq(x, y) }),
         "f64-eq" => prim!(fn(x: f64, y: f64) -> bool { f64::eq(x, y) }),
 

diff --git a/src/semantics/mod.rs b/src/semantics/mod.rs
@@ -164,6 +164,12 @@ pub fn is_subtype(context: &Context, ty1: &RcType, ty2: &RcType) -> bool {
             in_min_bound && in_max_bound
         },
 
+        (&Value::Refinement(ref scope), _) => {
+            // NOTE: It's safe to access the pattern without binding the body.
+            // TODO: Should this be reflected in the API of Moniker?
+            is_subtype(context, &(scope.unsafe_pattern.1).0, ty2)
+        },
+
         _ if Type::term_eq(ty1, context.u16le()) => is_subtype(context, context.u16(), ty2),
         _ if Type::term_eq(ty1, context.u32le()) => is_subtype(context, context.u32(), ty2),
         _ if Type::term_eq(ty1, context.u64le()) => is_subtype(context, context.u64(), ty2),
@@ -740,6 +746,26 @@ pub fn infer_term(
             }
         },
 
+        raw::Term::Refinement(_, ref raw_scope) => {
+            let ((Binder(free_var), Embed(raw_ann)), raw_body) = raw_scope.clone().unbind();
+            let (ann, level) = infer_universe(context, &raw_ann)?;
+            let ann_value = nf_term(context, &ann)?;
+
+            // TODO: We should add the predicate to a constraint store
+            let body = {
+                let mut body_context = context.clone();
+                body_context.insert_declaration(free_var.clone(), ann_value);
+                check_term(&body_context, &raw_body, body_context.bool())?
+            };
+
+            let param = (Binder(free_var), Embed(ann));
+
+            Ok((
+                RcTerm::from(Term::Refinement(Scope::new(param, body))),
+                RcValue::from(Value::Universe(level)),
+            ))
+        },
+
         raw::Term::Struct(span, _) => Err(TypeError::AmbiguousStruct { span }),
 
         // I-PROJ

diff --git a/src/semantics/normalize.rs b/src/semantics/normalize.rs
@@ -112,6 +112,15 @@ pub fn nf_term(context: &Context, term: &RcTerm) -> Result<RcValue, InternalErro
             }
         },
 
+        Term::Refinement(ref scope) => {
+            let ((name, Embed(ann)), body) = scope.clone().unbind();
+
+            Ok(RcValue::from(Value::Refinement(Scope::new(
+                (name, Embed(nf_term(context, &ann)?)),
+                nf_term(context, &body)?,
+            ))))
+        },
+
         // E-STRUCT, E-EMPTY-STRUCT
         Term::Struct(ref fields) => {
             let fields = fields

diff --git a/src/semantics/parser.rs b/src/semantics/parser.rs
@@ -13,6 +13,7 @@ pub enum ParseError {
     BadArrayIndex(core::RcValue),
     OffsetPointedToDifferentTypes(core::RcType, core::RcType),
     ParametrizedStructType,
+    FailedPredicate(core::RcValue),
     MissingRoot(Label),
     Io(io::Error),
 }
@@ -243,6 +244,23 @@ where
         _ if core::RcValue::term_eq(ty, context.f64le()) => Ok(Value::F64(bytes.read_f64::<Le>()?)),
         _ if core::RcValue::term_eq(ty, context.f64be()) => Ok(Value::F64(bytes.read_f64::<Be>()?)),
 
+        core::Value::Refinement(ref scope) => {
+            let ((Binder(free_var), Embed(ann)), pred) = scope.clone().unbind();
+            let ann_value = parse_term(context, pending, &ann, bytes)?;
+            let pred_value = {
+                let ann_value = core::RcTerm::from(core::Term::from(&ann_value));
+                nf_term(context, &pred.substs(&[(free_var, ann_value)]))?
+            };
+
+            match *pred_value.inner {
+                core::Value::Literal(core::Literal::Bool(true)) => Ok(ann_value),
+                core::Value::Literal(core::Literal::Bool(false)) => {
+                    Err(ParseError::FailedPredicate(pred.clone()))
+                },
+                _ => unimplemented!("unexpected value: {}", pred_value),
+            }
+        },
+
         // Invalid parse types
         core::Value::Universe(_)
         | core::Value::IntType(_, _)