More generic contract generation (tweag#1192)

* Add primops for operating on type environments in labels * Delegate tracking of polarities to a $forall contract * Apply suggestions from code review Co-authored-by: Yann Hamdaoui <[email protected]> * Use field access instead of destructuring for TypeVarData This avoids a pass through the merging code path. The result is a ~10% performance improvement on a large tf-ncl AWS example. Co-authored-by: Yann Hamdaoui <[email protected]> * Rename HasUnifType to ReifyAsUnifType --------- Co-authored-by: Yann Hamdaoui <[email protected]>
mkatychev · Mar 23, 2023 · 7284ce5 · 7284ce5
1 parent 0c9fa8a
commit 7284ce5
Show file tree

Hide file tree

Showing 12 changed files with 275 additions and 30 deletions.
diff --git a/lsp/nls/src/requests/completion.rs b/lsp/nls/src/requests/completion.rs
@@ -820,7 +820,7 @@ mod tests {
 
     #[test]
     fn test_extract_ident_with_path() {
-        use nickel_lang::{mk_uty_record, mk_uty_row, types::RecordRowsF};
+        use nickel_lang::{mk_uty_record, mk_uty_row};
         use std::convert::TryInto;
 
         // Representing the type: {a: {b : {c1 : Num, c2: Num}}}

diff --git a/src/eval/operation.rs b/src/eval/operation.rs
@@ -16,7 +16,7 @@ use super::{
 use crate::{
     error::{EvalError, IllegalPolymorphicTailAction},
     identifier::Ident,
-    label::ty_path,
+    label::{ty_path, Polarity, TypeVarData},
     match_sharedterm, mk_app, mk_fun, mk_opn, mk_record,
     parser::utils::parse_number,
     position::TermPos,
@@ -2798,6 +2798,39 @@ impl<R: ImportResolver, C: Cache> VirtualMachine<R, C> {
                     pos2.into_inherited(),
                 )))
             }
+            BinaryOp::LookupTypeVar() => {
+                let t1 = t1.into_owned();
+                let t2 = t2.into_owned();
+
+                let Term::SealingKey(key) = t1 else {
+                    return Err(EvalError::TypeError(
+                        String::from("Symbol"),
+                        String::from("lookup_type_variable, 1st argument"),
+                        fst_pos,
+                        RichTerm {
+                            term: t1.into(),
+                            pos: pos1,
+                        }
+                    ));
+                };
+
+                let Term::Lbl(label) = t2 else {
+                    return Err(EvalError::TypeError(
+                        String::from("Label"),
+                        String::from("lookup_type_variable, 2nd argument"),
+                        snd_pos,
+                        RichTerm {
+                            term: t2.into(),
+                            pos: pos2,
+                        }
+                    ));
+                };
+
+                Ok(Closure::atomic_closure(RichTerm::new(
+                    label.type_environment.get(&key).unwrap().into(),
+                    pos_op_inh,
+                )))
+            }
         }
     }
 
@@ -3161,6 +3194,92 @@ impl<R: ImportResolver, C: Cache> VirtualMachine<R, C> {
                     )),
                 }
             }
+            NAryOp::InsertTypeVar() => {
+                let mut args = args.into_iter();
+
+                let (
+                    Closure {
+                        body:
+                            RichTerm {
+                                term: key,
+                                pos: key_pos,
+                            },
+                        ..
+                    },
+                    pos1,
+                ) = args.next().unwrap();
+
+                let (
+                    Closure {
+                        body:
+                            RichTerm {
+                                term: polarity,
+                                pos: polarity_pos,
+                            },
+                        ..
+                    },
+                    pos2,
+                ) = args.next().unwrap();
+
+                let (
+                    Closure {
+                        body:
+                            RichTerm {
+                                term: label,
+                                pos: label_pos,
+                            },
+                        ..
+                    },
+                    pos3,
+                ) = args.next().unwrap();
+                debug_assert!(args.next().is_none());
+
+                let Term::SealingKey(key) = *key else {
+                    return Err(EvalError::TypeError(
+                        String::from("Symbol"),
+                        String::from("insert_type_variable, 1st argument"),
+                        key_pos,
+                        RichTerm {
+                            term: key,
+                            pos: pos1,
+                        }
+                    ));
+                };
+
+                let Ok(polarity) = Polarity::try_from(polarity.as_ref()) else {
+                    return Err(EvalError::TypeError(
+                        String::from("Polarity"),
+                        String::from("insert_type_variable, 2nd argument"),
+                        polarity_pos,
+                        RichTerm {
+                            term: polarity,
+                            pos: pos2,
+                        },
+                    ))
+                };
+
+                let Term::Lbl(label) = &*label else {
+                    return Err(EvalError::TypeError(
+                        String::from("Label"),
+                        String::from("insert_type_variable, 3rd argument"),
+                        label_pos,
+                        RichTerm {
+                            term: label,
+                            pos: pos3,
+                        }
+                    ));
+                };
+
+                let mut new_label = label.clone();
+                new_label
+                    .type_environment
+                    .insert(key, TypeVarData { polarity });
+
+                Ok(Closure::atomic_closure(RichTerm::new(
+                    Term::Lbl(new_label),
+                    pos2.into_inherited(),
+                )))
+            }
         }
     }
 }

diff --git a/src/label.rs b/src/label.rs
@@ -2,13 +2,18 @@
 //!
 //! A label is a value holding metadata relative to contract checking. It gives the user useful
 //! information about the context of a contract failure.
-use std::rc::Rc;
+use std::{collections::HashMap, rc::Rc};
 
 use crate::{
     eval::cache::{Cache as EvalCache, CacheIndex},
     identifier::Ident,
+    mk_uty_enum, mk_uty_record,
     position::{RawSpan, TermPos},
-    term::{RichTerm, Term},
+    term::{
+        record::{Field, RecordData},
+        RichTerm, SealingKey, Term,
+    },
+    typecheck::{ReifyAsUnifType, UnifType},
     types::{TypeF, Types},
 };
 
@@ -307,8 +312,42 @@ pub struct Label {
     pub polarity: Polarity,
     /// The path of the type being currently checked in the original type.
     pub path: ty_path::Path,
+    /// An environment mapping type variables to [`TypeVarData`]. Used by
+    /// polymorphic contracts to decide which actions to take when encountering a `forall`.
+    pub type_environment: HashMap<SealingKey, TypeVarData>,
 }
 
+/// Data about type variables that is needed for polymorphic contracts to decide which actions to take.
+#[derive(Debug, Clone, PartialEq, Eq)]
+pub struct TypeVarData {
+    pub polarity: Polarity,
+}
+
+impl From<&TypeVarData> for Term {
+    fn from(value: &TypeVarData) -> Self {
+        Term::Record(RecordData {
+            fields: [(
+                Ident::new("polarity"),
+                Field::from(RichTerm::from(Term::from(value.polarity))),
+            )]
+            .into(),
+            attrs: Default::default(),
+            sealed_tail: None,
+        })
+    }
+}
+
+impl ReifyAsUnifType for TypeVarData {
+    fn unif_type() -> UnifType {
+        mk_uty_record!(("polarity", Polarity::unif_type()))
+    }
+}
+
+impl ReifyAsUnifType for Polarity {
+    fn unif_type() -> UnifType {
+        mk_uty_enum!("Positive", "Negative")
+    }
+}
 /// A polarity. See [`Label`]
 #[derive(Debug, Clone, Copy, PartialEq, Eq)]
 pub enum Polarity {
@@ -334,6 +373,18 @@ impl From<Polarity> for Term {
     }
 }
 
+impl TryFrom<&Term> for Polarity {
+    type Error = ();
+
+    fn try_from(value: &Term) -> Result<Self, Self::Error> {
+        match value {
+            Term::Enum(positive) if positive.label() == "Positive" => Ok(Self::Positive),
+            Term::Enum(negative) if negative.label() == "Negative" => Ok(Self::Negative),
+            _ => Err(()),
+        }
+    }
+}
+
 /// Custom reporting diagnostic that can be set by user-code through the `label` API. Used to
 /// customize contract error messages, and provide more context than "a contract has failed".
 #[derive(Debug, Clone, PartialEq, Default)]
@@ -470,6 +521,7 @@ impl Default for Label {
             arg_idx: Default::default(),
             arg_pos: Default::default(),
             path: Default::default(),
+            type_environment: Default::default(),
         }
     }
 }
diff --git a/src/parser/grammar.lalrpop b/src/parser/grammar.lalrpop
@@ -864,6 +864,7 @@ BOpPre: BinaryOp = {
     "label_with_message" => BinaryOp::LabelWithMessage(),
     "label_with_notes" => BinaryOp::LabelWithNotes(),
     "label_append_note" => BinaryOp::LabelAppendNote(),
+    "lookup_type_variable" => BinaryOp::LookupTypeVar(),
 }
 
 NOpPre<ArgRule>: UniTerm = {
@@ -877,6 +878,8 @@ NOpPre<ArgRule>: UniTerm = {
         UniTerm::from(mk_opn!(NAryOp::RecordSealTail(), t1, t2, t3, t4)),
     "record_unseal_tail" <t1: ArgRule> <t2: ArgRule> <t3: ArgRule> =>
         UniTerm::from(mk_opn!(NAryOp::RecordUnsealTail(), t1, t2, t3)),
+    "insert_type_variable" <key: ArgRule> <pol: ArgRule> <label: ArgRule> =>
+        UniTerm::from(mk_opn!(NAryOp::InsertTypeVar(), key, pol, label)),
 }
 
 TypeBuiltin: Types = {
@@ -1029,6 +1032,8 @@ extern {
         "rec_force_op" => Token::Normal(NormalToken::RecForceOp),
         "rec_default_op" => Token::Normal(NormalToken::RecDefaultOp),
         "trace" => Token::Normal(NormalToken::Trace),
+        "insert_type_variable" => Token::Normal(NormalToken::InsertTypeVar),
+        "lookup_type_variable" => Token::Normal(NormalToken::LookupTypeVar),
 
         "has_field" => Token::Normal(NormalToken::HasField),
         "map" => Token::Normal(NormalToken::Map),

diff --git a/src/parser/lexer.rs b/src/parser/lexer.rs
@@ -204,6 +204,10 @@ pub enum NormalToken<'input> {
     GoArray,
     #[token("%go_dict%")]
     GoDict,
+    #[token("%insert_type_variable%")]
+    InsertTypeVar,
+    #[token("%lookup_type_variable%")]
+    LookupTypeVar,
 
     #[token("%seal%")]
     Seal,

diff --git a/src/stdlib.rs b/src/stdlib.rs
@@ -119,6 +119,7 @@ pub mod contract {
     generate_accessor!(array);
     generate_accessor!(func);
     generate_accessor!(forall_var);
+    generate_accessor!(forall);
     generate_accessor!(fail);
     generate_accessor!(enums);
     generate_accessor!(enum_fail);

diff --git a/src/term/mod.rs b/src/term/mod.rs
@@ -1305,6 +1305,10 @@ pub enum BinaryOp {
     LabelWithNotes(),
     /// Append a note to the current diagnostic of a label.
     LabelAppendNote(),
+
+    /// Look up the [`TypeVarData`] associated with a [`SealingKey`] in the
+    /// type environment of a [label](Term::Lbl)
+    LookupTypeVar(),
 }
 
 impl BinaryOp {
@@ -1363,6 +1367,14 @@ pub enum NAryOp {
     ///     something goes wrong while unsealing,
     ///   - the [record](Term::Record) whose tail we wish to unseal.
     RecordUnsealTail(),
+    /// Insert type variable data into the [`type_environment`] of a [`Label`]
+    ///
+    /// Takes four arguments:
+    ///   - the [sealing key](Term::SealingKey) assigned to the type variable
+    ///   - the [introduction polarity](label::Polarity) of the type variable
+    ///   - the [kind](types::VarKind) of the type variable
+    ///   - a [label](Term::Label) on which to operate
+    InsertTypeVar(),
 }
 
 impl NAryOp {
@@ -1372,7 +1384,8 @@ impl NAryOp {
             | NAryOp::StrReplaceRegex()
             | NAryOp::StrSubstr()
             | NAryOp::MergeContract()
-            | NAryOp::RecordUnsealTail() => 3,
+            | NAryOp::RecordUnsealTail()
+            | NAryOp::InsertTypeVar() => 3,
             NAryOp::RecordSealTail() => 4,
         }
     }
@@ -1387,6 +1400,7 @@ impl fmt::Display for NAryOp {
             NAryOp::MergeContract() => write!(f, "mergeContract"),
             NAryOp::RecordSealTail() => write!(f, "%record_seal_tail%"),
             NAryOp::RecordUnsealTail() => write!(f, "%record_unseal_tail%"),
+            NAryOp::InsertTypeVar() => write!(f, "%insert_type_variable%"),
         }
     }
 }

diff --git a/src/typecheck/mk_uniftype.rs b/src/typecheck/mk_uniftype.rs
@@ -13,7 +13,7 @@ macro_rules! mk_uty_arrow {
         )
     };
     ( $fst:expr, $snd:expr , $( $types:expr ),+ ) => {
-        mk_uty_arrow!($fst, mk_uty_arrow!($snd, $( $types ),+))
+        $crate::mk_uty_arrow!($fst, $crate::mk_uty_arrow!($snd, $( $types ),+))
     };
 }
 
@@ -22,7 +22,7 @@ macro_rules! mk_uty_arrow {
 #[macro_export]
 macro_rules! mk_uty_enum_row {
     () => {
-        $crate::typecheck::UnifEnumRows::Concrete(EnumRowsF::Empty)
+        $crate::typecheck::UnifEnumRows::Concrete($crate::types::EnumRowsF::Empty)
     };
     (; $tail:expr) => {
         $crate::typecheck::UnifEnumRows::from($tail)
@@ -31,7 +31,7 @@ macro_rules! mk_uty_enum_row {
         $crate::typecheck::UnifEnumRows::Concrete(
             $crate::types::EnumRowsF::Extend {
                 row: Ident::from($id),
-                tail: Box::new(mk_uty_enum_row!($( $ids ),* $(; $tail)?))
+                tail: Box::new($crate::mk_uty_enum_row!($( $ids ),* $(; $tail)?))
             }
         )
     };
@@ -43,7 +43,7 @@ macro_rules! mk_uty_enum_row {
 #[macro_export]
 macro_rules! mk_uty_row {
     () => {
-        $crate::typecheck::UnifRecordRows::Concrete(RecordRowsF::Empty)
+        $crate::typecheck::UnifRecordRows::Concrete($crate::types::RecordRowsF::Empty)
     };
     (; $tail:expr) => {
         $crate::typecheck::UnifRecordRows::from($tail)
@@ -55,7 +55,7 @@ macro_rules! mk_uty_row {
                     id: Ident::from($id),
                     types: Box::new($ty.into()),
                 },
-                tail: Box::new(mk_uty_row!($(($ids, $tys)),* $(; $tail)?)),
+                tail: Box::new($crate::mk_uty_row!($(($ids, $tys)),* $(; $tail)?)),
             }
         )
     };
@@ -67,7 +67,7 @@ macro_rules! mk_uty_enum {
     ($( $ids:expr ),* $(; $tail:expr)?) => {
         $crate::typecheck::UnifType::Concrete(
             $crate::types::TypeF::Enum(
-                mk_uty_enum_row!($( $ids ),* $(; $tail)?)
+                $crate::mk_uty_enum_row!($( $ids ),* $(; $tail)?)
             )
         )
     };
@@ -79,7 +79,7 @@ macro_rules! mk_uty_record {
     ($(($ids:expr, $tys:expr)),* $(; $tail:expr)?) => {
         $crate::typecheck::UnifType::Concrete(
             $crate::types::TypeF::Record(
-                mk_uty_row!($(($ids, $tys)),* $(; $tail)?)
+                $crate::mk_uty_row!($(($ids, $tys)),* $(; $tail)?)
             )
         )
     };