Repository: tweag/nickel
Pull request #788 (2022-08-02 14:55:33)

Rename sym and (un)wrap to key and (un)seal for more clarity

yannham: Bad search and replace skills, it seems. Thanks.

Patch:
diff --git a/doc/manual/correctness.md b/doc/manual/correctness.md
index f3d03c84..faffd158 100644
--- a/doc/manual/correctness.md
+++ b/doc/manual/correctness.md
@@ -216,7 +216,7 @@ candidate for static typing, which will help:
 - Report errors before execution takes place.
 
 Even if the call site is not statically typed, a type annotation also gives rise
-to a contract (see the [typing section](./typing.md) for more details). Thus,
+to a contract (see the [typing section][./typing.md] for more details). Thus,
 any issue with the arguments passed or the return value will be caught and
 correctly reported.
 
diff --git a/src/eval/mod.rs b/src/eval/mod.rs
index fbbc49b3..b0b37375 100644
--- a/src/eval/mod.rs
+++ b/src/eval/mod.rs
@@ -704,7 +704,7 @@ pub fn subst(rt: RichTerm, global_env: &Environment, env: &Environment) -> RichT
         // loop. Although avoidable, this requires some care and is not currently needed.
         | v @ Term::Fun(..)
         | v @ Term::Lbl(_)
-        | v @ Term::Sym(_)
+        | v @ Term::SealingKey(_)
         | v @ Term::Enum(_)
         | v @ Term::Import(_)
         | v @ Term::ResolvedImport(_) => RichTerm::new(v, pos),
@@ -757,10 +757,10 @@ pub fn subst(rt: RichTerm, global_env: &Environment, env: &Environment) -> RichT
 
             RichTerm::new(Term::OpN(op, ts), pos)
         }
-        Term::Wrapped(i, t) => {
+        Term::Sealed(i, t) => {
             let t = subst(t, global_env, env);
 
-            RichTerm::new(Term::Wrapped(i, t), pos)
+            RichTerm::new(Term::Sealed(i, t), pos)
         }
         Term::Record(map, attrs) => {
             let map = map
diff --git a/src/eval/operation.rs b/src/eval/operation.rs
index a5100d0b..8fd7544b 100644
--- a/src/eval/operation.rs
+++ b/src/eval/operation.rs
@@ -434,10 +434,10 @@ fn process_unary_operation(
                 ))
             }
         },
-        UnaryOp::Wrap() => {
-            if let Term::Sym(s) = &*t {
+        UnaryOp::Seal() => {
+            if let Term::SealingKey(s) = &*t {
                 Ok(Closure::atomic_closure(
-                    mk_fun!("x", Term::Wrapped(*s, mk_term::var("x"))).with_pos(pos_op_inh),
+                    mk_fun!("x", Term::Sealed(*s, mk_term::var("x"))).with_pos(pos_op_inh),
                 ))
             } else {
                 Err(EvalError::TypeError(
@@ -1410,12 +1410,12 @@ fn process_binary_operation(
                 ))
             }
         }
-        BinaryOp::Unwrap() => {
-            if let Term::Sym(s1) = &*t1 {
+        BinaryOp::Unseal() => {
+            if let Term::SealingKey(s1) = &*t1 {
                 // Return a function that either behaves like the identity or
                 // const unwrapped_term
 
-                Ok(if let Term::Wrapped(s2, t) = t2.into_owned() {
+                Ok(if let Term::Sealed(s2, t) = t2.into_owned() {
                     if *s1 == s2 {
                         Closure {
                             body: mk_fun!("-invld", t),
@@ -2398,7 +2398,7 @@ fn eq(env: &mut Environment, c1: Closure, c2: Closure) -> EqResult {
         (Term::Num(n1), Term::Num(n2)) => EqResult::Bool(n1 == n2),
         (Term::Str(s1), Term::Str(s2)) => EqResult::Bool(s1 == s2),
         (Term::Lbl(l1), Term::Lbl(l2)) => EqResult::Bool(l1 == l2),
-        (Term::Sym(s1), Term::Sym(s2)) => EqResult::Bool(s1 == s2),
+        (Term::SealingKey(s1), Term::SealingKey(s2)) => EqResult::Bool(s1 == s2),
         (Term::Enum(id1), Term::Enum(id2)) => EqResult::Bool(id1 == id2),
         (Term::Record(m1, _), Term::Record(m2, _)) => {
             let (left, center, right) = merge::hashmap::split(m1, m2);
diff --git a/src/grammar.lalrpop b/src/grammar.lalrpop
index bee710ff..835236c9 100644
--- a/src/grammar.lalrpop
+++ b/src/grammar.lalrpop
@@ -532,7 +532,7 @@ UOp: UnaryOp = {
     "go_dom" => UnaryOp::GoDom(),
     "go_codom" => UnaryOp::GoCodom(),
     "go_array" => UnaryOp::GoArray(),
-    "wrap" => UnaryOp::Wrap(),
+    "seal" => UnaryOp::Seal(),
     "embed" <Ident> => UnaryOp::Embed(<>),
     "map"  => UnaryOp::ArrayMap(),
     "generate" => UnaryOp::ArrayGen(),
@@ -722,7 +722,7 @@ InfixExpr: UniTerm = {
 
 BOpPre: BinaryOp = {
     "assume" => BinaryOp::Assume(),
-    "unwrap" => BinaryOp::Unwrap(),
+    "unseal" => BinaryOp::Unseal(),
     "go_field" => BinaryOp::GoField(),
     "has_field" => BinaryOp::HasField(),
     "elem_at" => BinaryOp::ArrayElemAt(),
@@ -859,8 +859,8 @@ extern {
         "go_codom" => Token::Normal(NormalToken::GoCodom),
         "go_array" => Token::Normal(NormalToken::GoArray),
         "go_field" => Token::Normal(NormalToken::GoField),
-        "wrap" => Token::Normal(NormalToken::Wrap),
-        "unwrap" => Token::Normal(NormalToken::Unwrap),
+        "seal" => Token::Normal(NormalToken::Seal),
+        "unseal" => Token::Normal(NormalToken::Unseal),
         "embed" => Token::Normal(NormalToken::Embed),
         "record_map" => Token::Normal(NormalToken::RecordMap),
         "record_insert" => Token::Normal(NormalToken::RecordInsert),
diff --git a/src/parser/lexer.rs b/src/parser/lexer.rs
index 5ef17e70..0002b877 100644
--- a/src/parser/lexer.rs
+++ b/src/parser/lexer.rs
@@ -167,10 +167,10 @@ pub enum NormalToken<'input> {
     #[token("%go_array%")]
     GoArray,
 
-    #[token("%wrap%")]
-    Wrap,
-    #[token("%unwrap%")]
-    Unwrap,
+    #[token("%seal%")]
+    Seal,
+    #[token("%unseal%")]
+    Unseal,
     #[token("%embed%")]
     Embed,
     #[token("%record_map%")]
diff --git a/src/pretty.rs b/src/pretty.rs
index fc8f29bf..7063de95 100644
--- a/src/pretty.rs
+++ b/src/pretty.rs
@@ -671,12 +671,12 @@ where
                 )
                 .group(),
 
-            Sym(sym) => allocator
-                .text(format!("# <symbol: {}>", sym))
+            SealingKey(sym) => allocator
+                .text(format!("#<sealing key: {}>", sym))
                 .append(allocator.hardline()),
 
             // TODO
-            Wrapped(_i, _rt) => allocator.text("# <wraped>").append(allocator.hardline()),
+            Sealed(_i, _rt) => allocator.text("#<sealed>").append(allocator.hardline()),
 
             MetaValue(mv) => mv.to_owned().pretty(allocator),
             Import(f) => allocator
@@ -685,7 +685,7 @@ where
                 .append(allocator.as_string(f.to_string_lossy()).double_quotes()),
             ResolvedImport(id) => allocator.text(format!("import <file_id: {:?}>", id)),
             ParseError => allocator
-                .text("# <PARCE ERROR!>")
+                .text("#<PARSE ERROR!>")
                 .append(allocator.hardline()),
         }
     }
diff --git a/src/term.rs b/src/term.rs
index c93860f6..627ec420 100644
--- a/src/term.rs
+++ b/src/term.rs
@@ -119,15 +119,15 @@ pub enum Term {
     #[serde(skip)]
     OpN(NAryOp, Vec<RichTerm>),
 
-    /// A symbol.
+    /// A key locking a sealed term.
     ///
-    /// A unique tag corresponding to a type variable. See `Wrapped` below.
+    /// A unique key corresponding to a type variable. See [`Term::Wrapped`] below.
     #[serde(skip)]
-    Sym(i32),
+    SealingKey(SealingKey),
 
-    /// A wrapped term.
+    /// A sealed term.
     ///
-    /// Wrapped terms are introduced by contracts on polymorphic types. Take the following example:
+    /// Sealed terms are introduced by contracts on polymorphic types. Take the following example:
     ///
     /// ```text
     /// let f = Assume(forall a. forall b. a -> b -> a, fun x y => y) in
@@ -138,13 +138,13 @@ pub enum Term {
     /// - Assign a unique identifier to each type variable: say `a => 1`, `b => 2`
     /// - For each cast on a negative occurrence of a type variable `a` or `b` (corresponding to an
     /// argument position), tag the argument with the associated identifier. In our example, `f
-    /// true "a"` will push `Wrapped(1, true)` then `Wrapped(2, "a")` on the stack.
+    /// true "a"` will push `Sealed(1, true)` then `Sealed(2, "a")` on the stack.
     /// - For each cast on a positive occurrence of a type variable, this contract check that the
-    /// term is of the form `Wrapped(id, term)` where `id` corresponds to the identifier of the
-    /// type variable. In our example, the last cast to `a` finds `Wrapped(2, "a")`, while it
-    /// expected `Wrapped(1, _)`, hence it raises a positive blame.
+    /// term is of the form `Sealed(id, term)` where `id` corresponds to the identifier of the
+    /// type variable. In our example, the last cast to `a` finds `Sealed(2, "a")`, while it
+    /// expected `Sealed(1, _)`, hence it raises a positive blame.
     #[serde(skip)]
-    Wrapped(i32, RichTerm),
+    Sealed(SealingKey, RichTerm),
 
     #[serde(serialize_with = "crate::serialize::serialize_meta_value")]
     #[serde(skip_deserializing)]
@@ -160,6 +160,8 @@ pub enum Term {
     ParseError,
 }
 
+pub type SealingKey = i32;
+
 impl From<MetaValue> for Term {
     fn from(m: MetaValue) -> Self {
         Term::MetaValue(m)
@@ -380,12 +382,12 @@ impl Term {
                     func(t2);
                 });
             }
-            Bool(_) | Num(_) | Str(_) | Lbl(_) | Var(_) | Sym(_) | Enum(_) | Import(_)
+            Bool(_) | Num(_) | Str(_) | Lbl(_) | Var(_) | SealingKey(_) | Enum(_) | Import(_)
             | ResolvedImport(_) => {}
             Fun(_, ref mut t)
             | FunPattern(_, _, ref mut t)
             | Op1(_, ref mut t)
-            | Wrapped(_, ref mut t) => {
+            | Sealed(_, ref mut t) => {
                 func(t);
             }
             MetaValue(ref mut meta) => {
@@ -432,8 +434,8 @@ impl Term {
             Term::Enum(_) => Some("Enum"),
             Term::Record(..) | Term::RecRecord(..) => Some("Record"),
             Term::Array(..) => Some("Array"),
-            Term::Sym(_) => Some("Sym"),
-            Term::Wrapped(_, _) => Some("Wrapped"),
+            Term::SealingKey(_) => Some("SealingKey"),
+            Term::Sealed(_, _) => Some("Sealed"),
             Term::MetaValue(_) => Some("Metavalue"),
             Term::Let(..)
             | Term::LetPattern(..)
@@ -484,8 +486,8 @@ impl Term {
             }
             Term::Record(..) | Term::RecRecord(..) => String::from("{ ... }"),
             Term::Array(..) => String::from("[ ... ]"),
-            Term::Sym(_) => String::from("<sym>"),
-            Term::Wrapped(_, _) => String::from("<wrapped>"),
+            Term::SealingKey(_) => String::from("<sealing key>"),
+            Term::Sealed(_, _) => String::from("<sealed>"),
             Term::MetaValue(ref meta) => {
                 let mut content = String::new();
 
@@ -562,7 +564,7 @@ impl Term {
             | Term::Enum(_)
             | Term::Record(..)
             | Term::Array(..)
-            | Term::Sym(_) => true,
+            | Term::SealingKey(_) => true,
             Term::Let(..)
             | Term::LetPattern(..)
             | Term::FunPattern(..)
@@ -572,7 +574,7 @@ impl Term {
             | Term::Op1(_, _)
             | Term::Op2(_, _, _)
             | Term::OpN(..)
-            | Term::Wrapped(_, _)
+            | Term::Sealed(_, _)
             | Term::MetaValue(_)
             | Term::Import(_)
             | Term::ResolvedImport(_)
@@ -599,7 +601,7 @@ impl Term {
             | Term::Str(_)
             | Term::Lbl(_)
             | Term::Enum(_)
-            | Term::Sym(_) => true,
+            | Term::SealingKey(_) => true,
             Term::Let(..)
             | Term::LetPattern(..)
             | Term::Record(..)
@@ -612,7 +614,7 @@ impl Term {
             | Term::Op1(_, _)
             | Term::Op2(_, _, _)
             | Term::OpN(..)
-            | Term::Wrapped(_, _)
+            | Term::Sealed(_, _)
             | Term::MetaValue(_)
             | Term::Import(_)
             | Term::ResolvedImport(_)
@@ -637,7 +639,7 @@ impl Term {
             | Term::Array(..)
             | Term::Var(..)
             | Term::Op1(..)
-            | Term::Sym(..) => true,
+            | Term::SealingKey(..) => true,
             Term::Let(..)
             | Term::Switch(..)
             | Term::LetPattern(..)
@@ -646,7 +648,7 @@ impl Term {
             | Term::App(..)
             | Term::Op2(..)
             | Term::OpN(..)
-            | Term::Wrapped(..)
+            | Term::Sealed(..)
             | Term::MetaValue(..)
             | Term::Import(..)
             | Term::ResolvedImport(..)
@@ -784,8 +786,8 @@ pub enum UnaryOp {
     /// See `GoDom`.
     GoArray(),
 
-    /// Wrap a term with a type tag (see [`Term::Wrapped`]).
-    Wrap(),
+    /// Seal a term with a sealing key (see [`Term::Sealed`]).
+    Seal(),
 
     /// Force the evaluation of its argument and proceed with the second.
     Seq(),
@@ -933,10 +935,10 @@ pub enum BinaryOp {
     /// operation with its argument. Finally, this operator marks the location of the contract
     /// argument for better error reporting.
     Assume(),
-    /// Unwrap a tagged term.
+    /// Unseal a sealed term.
     ///
-    /// See [`UnaryOp::Wrap`].
-    Unwrap(),
+    /// See [`UnaryOp::Seal`].
+    Unseal(),
     /// Go to a specific field in the type path of a label.
     ///
     /// See `GoDom`.
@@ -1177,10 +1179,10 @@ impl RichTerm {
                     pos,
                 )
             },
-            Term::Wrapped(i, t) => {
+            Term::Sealed(i, t) => {
                 let t = t.traverse(f, state, order)?;
                 RichTerm::new(
-                    Term::Wrapped(i, t),
+                    Term::Sealed(i, t),
                     pos,
                 )
             },
diff --git a/src/transform/free_vars.rs b/src/transform/free_vars.rs
index e2accf72..9ad53263 100644
--- a/src/transform/free_vars.rs
+++ b/src/transform/free_vars.rs
@@ -30,7 +30,7 @@ fn collect_free_vars(rt: &mut RichTerm, free_vars: &mut HashSet<Ident>) {
         | Term::Num(_)
         | Term::Str(_)
         | Term::Lbl(_)
-        | Term::Sym(_)
+        | Term::SealingKey(_)
         | Term::Enum(_)
         | Term::Import(_)
         | Term::ResolvedImport(_) => (),
@@ -99,7 +99,7 @@ fn collect_free_vars(rt: &mut RichTerm, free_vars: &mut HashSet<Ident>) {
                 collect_free_vars(t, free_vars);
             }
         }
-        Term::Wrapped(_, t) => collect_free_vars(t, free_vars),
+        Term::Sealed(_, t) => collect_free_vars(t, free_vars),
         Term::Record(map, _) => {
             for t in map.values_mut() {
                 collect_free_vars(t, free_vars);
diff --git a/src/transform/share_normal_form.rs b/src/transform/share_normal_form.rs
index c3c935ad..ae2c8cfa 100644
--- a/src/transform/share_normal_form.rs
+++ b/src/transform/share_normal_form.rs
@@ -187,7 +187,7 @@ fn should_share(t: &Term) -> bool {
         | Term::Num(_)
         | Term::Str(_)
         | Term::Lbl(_)
-        | Term::Sym(_)
+        | Term::SealingKey(_)
         | Term::Var(_)
         | Term::Enum(_)
         | Term::Fun(_, _) => false,
diff --git a/src/typecheck/eq.rs b/src/typecheck/eq.rs
index 833e5d11..f59ca1f1 100644
--- a/src/typecheck/eq.rs
+++ b/src/typecheck/eq.rs
@@ -123,8 +123,8 @@ fn contract_eq_bounded(
         (Num(n1), Num(n2)) => n1 == n2,
         (Str(s1), Str(s2)) => s1 == s2,
         (Enum(id1), Enum(id2)) => id1 == id2,
-        (Sym(s1), Sym(s2)) => s1 == s2,
-        (Wrapped(key1, inner1), Wrapped(key2, inner2)) => {
+        (SealingKey(s1), SealingKey(s2)) => s1 == s2,
+        (Sealed(key1, inner1), Sealed(key2, inner2)) => {
             key1 == key2 && contract_eq_bounded(state, inner1, env1, inner2, env2)
         }
         // We only compare string chunks when they represent a plain string (they don't contain any
diff --git a/src/typecheck/mod.rs b/src/typecheck/mod.rs
index 07a4eb65..59903039 100644
--- a/src/typecheck/mod.rs
+++ b/src/typecheck/mod.rs
@@ -292,7 +292,7 @@ fn walk<L: Linearizer>(
         | Term::Str(_)
         | Term::Lbl(_)
         | Term::Enum(_)
-        | Term::Sym(_)
+        | Term::SealingKey(_)
         // This function doesn't recursively typecheck imports: this is the responsibility of the
         // caller.
         | Term::Import(_)
@@ -437,7 +437,7 @@ fn walk<L: Linearizer>(
                 _ => Ok(()),
             }
         }
-        Term::Wrapped(_, t) => walk(state, envs, lin, linearizer, t),
+        Term::Sealed(_, t) => walk(state, envs, lin, linearizer, t),
    }
 }
 
@@ -870,9 +870,9 @@ fn type_check_<L: Linearizer>(
                     .map_err(|err| err.into_typecheck_err(state, rt.pos)),
             }
         }
-        Term::Sym(_) => unify(state, ty, mk_typewrapper::sym())
+        Term::SealingKey(_) => unify(state, ty, mk_typewrapper::sym())
             .map_err(|err| err.into_typecheck_err(state, rt.pos)),
-        Term::Wrapped(_, t) => type_check_(state, envs, lin, linearizer, t, ty),
+        Term::Sealed(_, t) => type_check_(state, envs, lin, linearizer, t, ty),
         Term::Import(_) => unify(state, ty, mk_typewrapper::dynamic())
             .map_err(|err| err.into_typecheck_err(state, rt.pos)),
         // We use the apparent type of the import for checking. This function doesn't recursively
@@ -1017,7 +1017,7 @@ pub fn apparent_type(
         }
         Term::Num(_) => ApparentType::Inferred(Types(AbsType::Num())),
         Term::Bool(_) => ApparentType::Inferred(Types(AbsType::Bool())),
-        Term::Sym(_) => ApparentType::Inferred(Types(AbsType::Sym())),
+        Term::SealingKey(_) => ApparentType::Inferred(Types(AbsType::Sym())),
         Term::Str(_) | Term::StrChunks(_) => ApparentType::Inferred(Types(AbsType::Str())),
         Term::Array(..) => {
             ApparentType::Approximated(Types(AbsType::Array(Box::new(Types(AbsType::Dyn())))))
diff --git a/src/typecheck/operation.rs b/src/typecheck/operation.rs
index 17919ff8..d51ebcb4 100644
--- a/src/typecheck/operation.rs
+++ b/src/typecheck/operation.rs
@@ -56,7 +56,7 @@ pub fn get_uop_type(
             (mk_typewrapper::dynamic(), mk_typewrapper::dynamic())
         }
         // Sym -> Dyn -> Dyn
-        UnaryOp::Wrap() => (
+        UnaryOp::Seal() => (
             mk_typewrapper::sym(),
             mk_tyw_arrow!(AbsType::Dyn(), AbsType::Dyn()),
         ),
@@ -228,7 +228,7 @@ pub fn get_bop_type(
             mk_tyw_arrow!(mk_typewrapper::dynamic(), mk_typewrapper::dynamic()),
         ),
         // Sym -> Dyn -> Dyn -> Dyn
-        BinaryOp::Unwrap() => (
+        BinaryOp::Unseal() => (
             mk_typewrapper::sym(),
             mk_typewrapper::dynamic(),
             mk_tyw_arrow!(AbsType::Dyn(), AbsType::Dyn()),
diff --git a/src/types.rs b/src/types.rs
index 85e61a5d..c804124e 100644
--- a/src/types.rs
+++ b/src/types.rs
@@ -241,9 +241,17 @@ impl Types {
             AbsType::Flat(ref t) => t.clone(),
             AbsType::Var(ref id) => get_var(&h, id, true)?,
             AbsType::Forall(ref i, ref t) => {
-                let inst_var = mk_app!(contract::forall_var(), Term::Sym(*sy), Term::Bool(pol));
-
-                let inst_tail = mk_app!(contract::forall_tail(), Term::Sym(*sy), Term::Bool(pol));
+                let inst_var = mk_app!(
+                    contract::forall_var(),
+                    Term::SealingKey(*sy),
+                    Term::Bool(pol)
+                );
+
+                let inst_tail = mk_app!(
+                    contract::forall_tail(),
+                    Term::SealingKey(*sy),
+                    Term::Bool(pol)
+                );
 
                 h.insert(i.clone(), (inst_var, inst_tail));
                 *sy += 1;
diff --git a/stdlib/contract.ncl b/stdlib/contract.ncl
index 14835f18..f1f5409d 100644
--- a/stdlib/contract.ncl
+++ b/stdlib/contract.ncl
@@ -23,9 +23,9 @@
   "$forall_var" = fun sy pol l t =>
       let lPol = %polarity% l in
       if pol == lPol then
-          %unwrap% sy t (%blame% l)
+          %unseal% sy t (%blame% l)
       else
-          %wrap% sy t,
+          %seal% sy t,
 
   "$row_extend" = fun contr case l t =>
       if (case t) then
@@ -57,20 +57,20 @@
           %blame% (%tag% "missing field `%{field}`" l),
 
   "$forall_tail" = fun sy pol acc l t =>
-      let magic_fld = "_%wrapped" in
+      let magic_fld = "_%sealed" in
       if pol == (%polarity% l) then
           if %has_field% magic_fld t then
               let rest = %record_remove% magic_fld t in
               if rest == {} then
                   let fail = %blame% (%tag% "polymorphic tail mismatch" l) in
-                  let inner = %unwrap% sy (t."%{magic_fld}") fail in
+                  let inner = %unseal% sy (t."%{magic_fld}") fail in
                   acc & inner
               else
                   %blame% (%tag% "extra field `%{%head% (%fields% rest)}`" l)
           else
               %blame% (%tag% "missing polymorphic part" l)
       else
-          %record_insert% magic_fld acc (%wrap% sy t),
+          %record_insert% magic_fld acc (%seal% sy t),
 
   "$dyn_tail" = fun acc l t => acc & t,
 


Test patch:
diff --git a/tests/contracts_fail.rs b/tests/contracts_fail.rs
index 511e0e4b..ea200921 100644
--- a/tests/contracts_fail.rs
+++ b/tests/contracts_fail.rs
@@ -110,7 +110,7 @@ fn records_contracts_poly() {
         "let f | forall a. {foo: Num ; a} -> { ; a} = fun x => %record_insert% \"foo\" x 1 in f";
 
     assert_raise_blame!(&format!("{} {{}}", bad_cst));
-    // The polymorphic parts is protected by hiding it. Thus, trying to access the protected field
+    // The polymorphic part is protected by hiding it. Thus, trying to access the protected field
     // gives a field missing error, instead of a blame error.
     assert_matches!(
         eval(&format!("{} {{a=1}}", bad_acc)),