Repository: tweag/nickel
Pull request #1181 (2023-03-13 14:12:25)

Feature/IncCache propagation
A small part of the propagation rework for `IncCache`


Patch:
diff --git a/src/eval/cache/incremental.rs b/src/eval/cache/incremental.rs
index 9db27526..5ceccf54 100644
--- a/src/eval/cache/incremental.rs
+++ b/src/eval/cache/incremental.rs
@@ -1,5 +1,6 @@
-/// A [Cache] implementation with incremental computation features.
+use std::collections::{HashMap, HashSet};
 
+//! A [Cache] implementation with incremental computation features.
 use super::{BlackholedError, Cache, CacheIndex, Closure, Environment, IdentKind};
 use crate::{
     identifier::Ident,
@@ -15,6 +16,12 @@ pub enum IncNodeState {
     Evaluated,
 }
 
+#[derive(Debug, Copy, Clone, Eq, PartialEq)]
+pub struct DependencyLink {
+    id: Ident,
+    idx: CacheIndex,
+}
+
 /// A node in the dependent computation graph stored in [IncCache].
 #[derive(Debug, Clone)]
 pub struct IncNode {
@@ -26,8 +33,10 @@ pub struct IncNode {
     bty: BindingType,
     // The state of the node.
     state: IncNodeState,
+    // Forward links to dependencies.
+    fwdlinks: Vec<DependencyLink>,
     // Backlinks to nodes depending on this node.
-    backlinks: Vec<CacheIndex>,
+    backlinks: Vec<DependencyLink>,
 }
 
 impl IncNode {
@@ -38,6 +47,7 @@ impl IncNode {
             kind,
             bty,
             state: IncNodeState::default(),
+            fwdlinks: Vec::new(),
             backlinks: Vec::new(),
         }
     }
@@ -87,6 +97,93 @@ impl IncCache {
             _ => node.clone(),
         }
     }
+
+    fn update_backlinks(&mut self, idx: CacheIndex) {
+        let node = self.store.get(idx).unwrap().clone();
+        for i in node.fwdlinks {
+            let n = self.store.get_mut(i.idx).unwrap();
+            n.backlinks.push(DependencyLink { id: i.id, idx: idx });
+        }
+    }
+
+    fn propagate_dirty(&mut self, idx: CacheIndex) {
+        let mut node = self.store.get_mut(idx).unwrap();
+        node.cached = None;
+        node.state = IncNodeState::Suspended;
+
+        let mut visited = HashSet::new();
+        let mut stack = node.backlinks.clone();
+
+        visited.insert(idx);
+
+        while !stack.is_empty() {
+            let i = stack.pop().unwrap();
+            visited.insert(i.idx);
+            let mut current_node = self.store.get_mut(i.idx).unwrap();
+            current_node.cached = None;
+            current_node.state = IncNodeState::Suspended;
+            stack.extend(
+                current_node
+                    .backlinks
+                    .iter()
+                    .filter(|x| !visited.contains(&x.idx)),
+            )
+        }
+    }
+
+    /* Do we need this when we can revert in place?
+
+    fn propagate_revert(&mut self, id: Ident, idx: CacheIndex) -> HashMap<Ident, CacheIndex> {
+        let mut nodes_reverted = HashMap::new();
+
+        let mut visited = HashSet::new();
+        let mut stack = vec![idx];
+
+        while !stack.is_empty() {
+            let i = stack.pop().unwrap();
+            visited.insert(i);
+
+            let idx_reverted = self.revert(&idx);
+            //FIXME: use the actual node's id
+            let node_id = Ident::from("TODO!");
+            nodes_reverted.insert(node_id, idx_reverted);
+
+            let current_node = self.store.get(i).unwrap();
+
+            stack.extend(
+                current_node
+                    .backlinks
+                    .iter()
+                    .map(|x| x.idx)
+                    .filter(|x| !visited.contains(x)),
+            )
+        }
+
+        nodes_reverted
+    } */
+
+    fn smart_clone(&mut self, v: Vec<CacheIndex>) -> HashMap<CacheIndex, CacheIndex> {
+        let mut new_indices = HashMap::new();
+
+        for i in v.iter() {
+            let current_node = self.store.get(*i).unwrap().clone();
+            new_indices.insert(*i, self.add_node(current_node));
+        }
+
+        for i in new_indices.values() {
+            let current_node = self.store.get_mut(*i).unwrap();
+
+            for dep in current_node.backlinks.iter_mut() {
+                dep.idx = *new_indices.get(i).unwrap();
+            }
+
+            for dep in current_node.fwdlinks.iter_mut() {
+                dep.idx = *new_indices.get(i).unwrap();
+            }
+        }
+
+        new_indices
+    }
 }
 
 impl Cache for IncCache {
@@ -204,9 +301,12 @@ impl Cache for IncCache {
             kind: node.kind,
             bty: node.bty.clone(),
             state: node.state,
+            fwdlinks: node.fwdlinks.clone(),
             backlinks: node.backlinks.clone(),
         };
 
+        // TODO: Should this push the dependencies?
+
         self.add_node(new_node)
     }
 
@@ -224,13 +324,19 @@ impl Cache for IncCache {
             BindingType::Revertible(ref deps) => match deps {
                 FieldDeps::Unknown => new_cached.env.extend(rec_env.iter().cloned()),
                 FieldDeps::Known(deps) if deps.is_empty() => (),
-                FieldDeps::Known(deps) => new_cached
-                    .env
-                    .extend(rec_env.iter().filter(|(id, _)| deps.contains(id)).cloned()),
+                FieldDeps::Known(deps) => {
+                    let deps = rec_env.iter().filter(|(id, _)| deps.contains(id)).cloned();
+                    node.fwdlinks = deps
+                        .clone()
+                        .map(|(id, idx)| DependencyLink { id, idx })
+                        .collect();
+                    new_cached.env.extend(deps);
+                }
             },
         }
 
         node.cached = Some(new_cached);
+        self.update_backlinks(*idx);
     }
 
     fn saturate<'a, I: DoubleEndedIterator<Item = &'a Ident> + Clone>(
diff --git a/src/eval/cache/mod.rs b/src/eval/cache/mod.rs
index 978b21e2..221732b0 100644
--- a/src/eval/cache/mod.rs
+++ b/src/eval/cache/mod.rs
@@ -11,15 +11,15 @@ use crate::{
 };
 
 pub mod lazy;
-//pub mod incremental;
+// pub mod incremental;
 
 /// An index to a specific item stored in the cache
 pub type CacheIndex = lazy::Thunk;
-//pub type CacheIndex = usize;
+// pub type CacheIndex = usize;
 
 /// The current Cache implementation
 pub type CacheImpl = lazy::CBNCache;
-//pub type CacheImpl = incremental::IncCache;
+// pub type CacheImpl = incremental::IncCache;
 
 /// A black-holed node was accessed, which would lead to infinite recursion.
 #[derive(Clone, Copy, Debug, Eq, PartialEq)]
diff --git a/src/typecheck/destructuring.rs b/src/typecheck/destructuring.rs
index 92804989..fab357a0 100644
--- a/src/typecheck/destructuring.rs
+++ b/src/typecheck/destructuring.rs
@@ -2,21 +2,33 @@ use std::collections::HashMap;
 
 use crate::{
     destructuring::{FieldPattern, Match, RecordPattern},
+    error::TypecheckError,
     identifier::Ident,
     mk_uty_row,
+    term::LabeledType,
+    typecheck::{unify, UnifRecordRow},
     types::{RecordRowF, RecordRowsF, TypeF},
 };
 
 use super::{
-    mk_uniftype, Environment, GenericUnifRecordRowsIteratorItem, State, UnifRecordRows, UnifType,
+    mk_uniftype, Context, Environment, GenericUnifRecordRowsIteratorItem, State, UnifRecordRows,
+    UnifType,
 };
 
-pub fn build_pattern_type_walk_mode(state: &mut State, pat: &RecordPattern) -> UnifRecordRows {
-    build_pattern_type(state, pat, TypecheckMode::Walk)
+pub fn build_pattern_type_walk_mode(
+    state: &mut State,
+    ctxt: &Context,
+    pat: &RecordPattern,
+) -> Result<UnifRecordRows, TypecheckError> {
+    build_pattern_type(state, ctxt, pat, TypecheckMode::Walk)
 }
 
-pub fn build_pattern_type_check_mode(state: &mut State, pat: &RecordPattern) -> UnifRecordRows {
-    build_pattern_type(state, pat, TypecheckMode::Check)
+pub fn build_pattern_type_check_mode(
+    state: &mut State,
+    ctxt: &Context,
+    pat: &RecordPattern,
+) -> Result<UnifRecordRows, TypecheckError> {
+    build_pattern_type(state, ctxt, pat, TypecheckMode::Check)
 }
 
 #[derive(Debug, Clone, Copy, PartialEq, Eq)]
@@ -26,23 +38,35 @@ enum TypecheckMode {
 }
 
 /// Build a `UnifType` from a `Destruct` pattern. The type of each "leaf"
-/// identifier will be assigned based on the `leaf_type` argument. The
-/// current possibilities are for each leaf to have type `Dyn` or to be
-/// assigned a fresh unification variable.
+/// identifier will be assigned based on the `mode` argument. The
+/// current possibilities are for each leaf to have type `Dyn`, to use an
+/// explicit type annotation, or to be assigned a fresh unification variable.
 fn build_pattern_type(
     state: &mut State,
+    ctxt: &Context,
     pat: &RecordPattern,
-    leaf_type: TypecheckMode,
-) -> UnifRecordRows {
-    fn new_leaf_type(state: &mut State, leaf_type: TypecheckMode) -> UnifType {
-        match leaf_type {
+    mode: TypecheckMode,
+) -> Result<UnifRecordRows, TypecheckError> {
+    fn new_leaf_type(
+        state: &mut State,
+        ctxt: &Context,
+        mode: TypecheckMode,
+        ty_annot: Option<LabeledType>,
+    ) -> UnifType {
+        match mode {
             TypecheckMode::Walk => mk_uniftype::dynamic(),
-            TypecheckMode::Check => state.table.fresh_type_uvar(),
+            TypecheckMode::Check => {
+                if let Some(l_ty) = ty_annot {
+                    UnifType::from_type(l_ty.types, &ctxt.term_env)
+                } else {
+                    state.table.fresh_type_uvar()
+                }
+            }
         }
     }
 
     let tail = if pat.open {
-        match leaf_type {
+        match mode {
             // We use a dynamic tail here since we're in walk mode,
             // but if/when we remove dynamic record tails this could
             // likely be made an empty tail with no impact.
@@ -53,35 +77,58 @@ fn build_pattern_type(
         UnifRecordRows::Concrete(RecordRowsF::Empty)
     };
 
-    let rows = pat.matches.iter().map(|m| match m {
-        Match::Simple(id, _) => RecordRowF {
+    let mut rows = pat.matches.iter().map(|m| match m {
+        Match::Simple(id, field) => Ok(RecordRowF {
             id: *id,
-            types: Box::new(new_leaf_type(state, leaf_type)),
-        },
-        Match::Assign(id, _, FieldPattern::Ident(_)) => RecordRowF {
+            types: Box::new(new_leaf_type(
+                state,
+                ctxt,
+                mode,
+                field.metadata.annotation.types.clone(),
+            )),
+        }),
+        Match::Assign(id, field, FieldPattern::Ident(_)) => Ok(RecordRowF {
             id: *id,
-            types: Box::new(new_leaf_type(state, leaf_type)),
-        },
+            types: Box::new(new_leaf_type(
+                state,
+                ctxt,
+                mode,
+                field.metadata.annotation.types.clone(),
+            )),
+        }),
         Match::Assign(
             id,
-            _,
+            field,
             FieldPattern::RecordPattern(r_pat)
             | FieldPattern::AliasedRecordPattern { pattern: r_pat, .. },
         ) => {
-            let row_tys = build_pattern_type(state, r_pat, leaf_type);
+            let row_tys = build_pattern_type(state, ctxt, r_pat, mode)?;
             let ty = UnifType::Concrete(TypeF::Record(row_tys));
-            RecordRowF {
+
+            // If there are type annotations within nested record patterns
+            // then we need to unify them with the pattern type we've built
+            // to ensure (1) that they're mutually compatible and (2) that
+            // we assign the annotated types to the right unification variables.
+            if let Some(annot_ty) = &field.metadata.annotation.types {
+                let types = annot_ty.types.clone();
+                let pos = types.pos;
+                let annot_ty = UnifType::from_type(types, &ctxt.term_env);
+                unify(state, ctxt, ty.clone(), annot_ty)
+                    .map_err(|e| e.into_typecheck_err(state, pos))?;
+            }
+
+            Ok(RecordRowF {
                 id: *id,
                 types: Box::new(ty),
-            }
+            })
         }
     });
 
-    rows.fold(tail, |tail, row| {
-        UnifRecordRows::Concrete(RecordRowsF::Extend {
-            row,
+    rows.try_fold(tail, |tail, row: Result<UnifRecordRow, TypecheckError>| {
+        Ok(UnifRecordRows::Concrete(RecordRowsF::Extend {
+            row: row?,
             tail: Box::new(tail),
-        })
+        }))
     })
 }
 
diff --git a/src/typecheck/mod.rs b/src/typecheck/mod.rs
index d96556d6..f04118d1 100644
--- a/src/typecheck/mod.rs
+++ b/src/typecheck/mod.rs
@@ -842,7 +842,7 @@ fn walk<L: Linearizer>(
                 ctxt.type_env.insert(*id, mk_uniftype::dynamic());
             }
 
-            let pattern_ty = destructuring::build_pattern_type_walk_mode(state, pat);
+            let pattern_ty = destructuring::build_pattern_type_walk_mode(state, &ctxt, pat)?;
             destructuring::inject_pattern_variables(state, &mut ctxt.type_env, pat, pattern_ty);
             walk(state, ctxt, lin, linearizer, t)
         }
@@ -885,7 +885,7 @@ fn walk<L: Linearizer>(
                 ctxt.type_env.insert(*x, ty_let);
             }
 
-            let pattern_ty = destructuring::build_pattern_type_walk_mode(state, pat);
+            let pattern_ty = destructuring::build_pattern_type_walk_mode(state, &ctxt, pat)?;
             destructuring::inject_pattern_variables(state, &mut ctxt.type_env, pat, pattern_ty);
 
             walk(state, ctxt, lin, linearizer, rt)
@@ -1147,7 +1147,7 @@ fn type_check_<L: Linearizer>(
             type_check_(state, ctxt, lin, linearizer, t, trg)
         }
         Term::FunPattern(x, pat, t) => {
-            let src_rows_ty = destructuring::build_pattern_type_check_mode(state, pat);
+            let src_rows_ty = destructuring::build_pattern_type_check_mode(state, &ctxt, pat)?;
             let src = UnifType::Concrete(TypeF::Record(src_rows_ty.clone()));
 
             // TODO what to do here, this makes more sense to me, but it means let x = foo in bar
@@ -1217,7 +1217,8 @@ fn type_check_<L: Linearizer>(
         }
         Term::LetPattern(x, pat, re, rt) => {
             // The inferred type of the pattern w/ unification vars
-            let pattern_rows_type = destructuring::build_pattern_type_check_mode(state, pat);
+            let pattern_rows_type =
+                destructuring::build_pattern_type_check_mode(state, &ctxt, pat)?;
             let pattern_type = UnifType::Concrete(TypeF::Record(pattern_rows_type.clone()));
             // The inferred type of the expr being bound
             let ty_let = binding_type(state, re.as_ref(), &ctxt, true);


Test patch:
diff --git a/tests/integration/destructuring.rs b/tests/integration/destructuring.rs
index 76eaaf99..3e07e497 100644
--- a/tests/integration/destructuring.rs
+++ b/tests/integration/destructuring.rs
@@ -60,11 +60,23 @@ fn typecontract_fail() {
 fn type_mismatch_fail() {
     assert_matches!(
         eval_file("destructuring/type_mismatch_fail.ncl"),
-        // Note: ideally this would be a typechecker error, but currently
-        //       annotated types in destructuring patterns are just converted
-        //       into contracts. This should be revisted once the metadata
-        //       rework from RFC005 is implemented
-        Err(Error::EvalError(EvalError::BlameError { .. }))
+        Err(Error::TypecheckError(TypecheckError::RowMismatch(..)))
+    )
+}
+
+#[test]
+fn type_mismatch_field_pattern_fail() {
+    assert_matches!(
+        eval_file("destructuring/type_mismatch_field_pattern_fail.ncl"),
+        Err(Error::TypecheckError(TypecheckError::RowMismatch(..)))
+    )
+}
+
+#[test]
+fn type_mismatch_nested_destructuring_fail() {
+    assert_matches!(
+        eval_file("destructuring/type_mismatch_nested_destructuring_fail.ncl"),
+        Err(Error::TypecheckError(TypecheckError::RowMismatch(..)))
     )
 }
 
diff --git a/tests/integration/destructuring/pass/type_annotations.ncl b/tests/integration/destructuring/pass/type_annotations.ncl
new file mode 100644
index 00000000..e92f0c5b
--- /dev/null
+++ b/tests/integration/destructuring/pass/type_annotations.ncl
@@ -0,0 +1,18 @@
+let test_cases = {
+  "matching type annotation in pattern" = 
+    let { a : Number } = { a = 1 } in
+    a,
+
+  "matching type annotation in renamed pattern binding" = 
+    let { txt : String = other_name } = { txt = "hi" } in
+    other_name,
+
+  "matching type annotation in nested pattern" =
+    let { a = { b = { c : Bool }}} = { a = { b = { c = true }}} in
+    c,
+
+  "matching type annotation above nested pattern" = 
+    let { a : { b : { c : Bool }} = { b = { c }}} = { a = { b = { c = false }}} in
+    c,
+} : _ in
+true
diff --git a/tests/integration/destructuring/type_mismatch_fail.ncl b/tests/integration/destructuring/type_mismatch_fail.ncl
index 3c86e06b..cf20cb26 100644
--- a/tests/integration/destructuring/type_mismatch_fail.ncl
+++ b/tests/integration/destructuring/type_mismatch_fail.ncl
@@ -1,2 +1,2 @@
-let { a : Number } = { a = "hi" } in
-a : _
+(let { a : Number } = { a = "hi" } in
+a) : _
diff --git a/tests/integration/destructuring/type_mismatch_field_pattern_fail.ncl b/tests/integration/destructuring/type_mismatch_field_pattern_fail.ncl
new file mode 100644
index 00000000..78b0d5ad
--- /dev/null
+++ b/tests/integration/destructuring/type_mismatch_field_pattern_fail.ncl
@@ -0,0 +1,1 @@
+(let { a : Number = b } = { a = "x" } in b) : _
diff --git a/tests/integration/destructuring/type_mismatch_nested_destructuring_fail.ncl b/tests/integration/destructuring/type_mismatch_nested_destructuring_fail.ncl
new file mode 100644
index 00000000..db415834
--- /dev/null
+++ b/tests/integration/destructuring/type_mismatch_nested_destructuring_fail.ncl
@@ -0,0 +1,2 @@
+(let { a : { b : Number } = { b }} = { a = { b = "no" }} in
+b) : _
diff --git a/tests/snapshot/inputs/errors/annotated_record_pattern_typecheck_fail.ncl b/tests/snapshot/inputs/errors/annotated_record_pattern_typecheck_fail.ncl
new file mode 100644
index 00000000..595c6ac2
--- /dev/null
+++ b/tests/snapshot/inputs/errors/annotated_record_pattern_typecheck_fail.ncl
@@ -0,0 +1,4 @@
+(
+  let { x : Bool } = { x = 5 } in
+  x
+) : _
\ No newline at end of file
diff --git a/tests/snapshot/inputs/errors/mismatched_row_record_pattern_fail.ncl b/tests/snapshot/inputs/errors/mismatched_row_record_pattern_fail.ncl
new file mode 100644
index 00000000..4c0900a4
--- /dev/null
+++ b/tests/snapshot/inputs/errors/mismatched_row_record_pattern_fail.ncl
@@ -0,0 +1,4 @@
+(
+  let { x : { a : Number } = { a : String } } = { x = { a = true } } 
+  in a
+) : _
diff --git a/tests/snapshot/inputs/errors/nested_annotated_record_pattern_typecheck_fail.ncl b/tests/snapshot/inputs/errors/nested_annotated_record_pattern_typecheck_fail.ncl
new file mode 100644
index 00000000..eca933eb
--- /dev/null
+++ b/tests/snapshot/inputs/errors/nested_annotated_record_pattern_typecheck_fail.ncl
@@ -0,0 +1,4 @@
+(
+  let { x = { a : Number }} = { x = { a = "" }} in
+  x
+) : _
\ No newline at end of file
diff --git a/tests/snapshot/snapshots/snapshot__error_annotated_record_pattern_typecheck_fail.ncl.snap b/tests/snapshot/snapshots/snapshot__error_annotated_record_pattern_typecheck_fail.ncl.snap
new file mode 100644
index 00000000..a2ec6b2f
--- /dev/null
+++ b/tests/snapshot/snapshots/snapshot__error_annotated_record_pattern_typecheck_fail.ncl.snap
@@ -0,0 +1,20 @@
+---
+source: tests/snapshot/main.rs
+expression: snapshot
+---
+error: incompatible rows declaration
+  ┌─ [INPUTS_PATH]/errors/annotated_record_pattern_typecheck_fail.ncl:2:22
+  │
+2 │   let { x : Bool } = { x = 5 } in
+  │                      ^^^^^^^^^ this expression
+  │
+  = The type of the expression was expected to have the row `x: Bool`
+  = The type of the expression was inferred to have the row `x: Number`
+  = Could not match the two declaration of `x`
+
+error: While typing field `x`: incompatible types
+ = The type of the expression was expected to be `Bool`
+ = The type of the expression was inferred to be `Number`
+ = These types are not compatible
+
+
diff --git a/tests/snapshot/snapshots/snapshot__error_mismatched_row_record_pattern_fail.ncl.snap b/tests/snapshot/snapshots/snapshot__error_mismatched_row_record_pattern_fail.ncl.snap
new file mode 100644
index 00000000..20a89d59
--- /dev/null
+++ b/tests/snapshot/snapshots/snapshot__error_mismatched_row_record_pattern_fail.ncl.snap
@@ -0,0 +1,20 @@
+---
+source: tests/snapshot/main.rs
+expression: snapshot
+---
+error: incompatible rows declaration
+  ┌─ [INPUTS_PATH]/errors/mismatched_row_record_pattern_fail.ncl:2:13
+  │
+2 │   let { x : { a : Number } = { a : String } } = { x = { a = true } } 
+  │             ^^^^^^^^^^^^^^ this expression
+  │
+  = The type of the expression was expected to have the row `a: String`
+  = The type of the expression was inferred to have the row `a: Number`
+  = Could not match the two declaration of `a`
+
+error: While typing field `a`: incompatible types
+ = The type of the expression was expected to be `String`
+ = The type of the expression was inferred to be `Number`
+ = These types are not compatible
+
+
diff --git a/tests/snapshot/snapshots/snapshot__error_nested_annotated_record_pattern_typecheck_fail.ncl.snap b/tests/snapshot/snapshots/snapshot__error_nested_annotated_record_pattern_typecheck_fail.ncl.snap
new file mode 100644
index 00000000..ee6484de
--- /dev/null
+++ b/tests/snapshot/snapshots/snapshot__error_nested_annotated_record_pattern_typecheck_fail.ncl.snap
@@ -0,0 +1,20 @@
+---
+source: tests/snapshot/main.rs
+expression: snapshot
+---
+error: incompatible rows declaration
+  ┌─ [INPUTS_PATH]/errors/nested_annotated_record_pattern_typecheck_fail.ncl:2:31
+  │
+2 │   let { x = { a : Number }} = { x = { a = "" }} in
+  │                               ^^^^^^^^^^^^^^^^^ this expression
+  │
+  = The type of the expression was expected to have the row `x.a: Number`
+  = The type of the expression was inferred to have the row `x.a: String`
+  = Could not match the two declaration of `x.a`
+
+error: While typing field `x.a`: incompatible types
+ = The type of the expression was expected to be `Number`
+ = The type of the expression was inferred to be `String`
+ = These types are not compatible
+
+