Fix subtype (#280)

* subtype should only take one env * fix * fix
dfinity · Sep 30, 2021 · dcbfc12 · dcbfc12
1 parent 10291c2
commit dcbfc12
Show file tree

Hide file tree

Showing 5 changed files with 78 additions and 27 deletions.
diff --git a/rust/candid/src/de.rs b/rust/candid/src/de.rs
@@ -192,7 +192,6 @@ impl<'de> Deserializer<'de> {
             &mut self.gamma,
             &self.table,
             &self.wire_type,
-            &self.table,
             &self.expect_type,
         )
         .with_context(|| {

diff --git a/rust/candid/src/parser/typing.rs b/rust/candid/src/parser/typing.rs
@@ -33,6 +33,23 @@ impl TypeEnv {
         }
         Ok(self)
     }
+    pub fn merge_type(&mut self, env: TypeEnv, ty: Type) -> Type {
+        let tau: BTreeMap<String, String> = env
+            .0
+            .keys()
+            .filter(|k| self.0.contains_key(*k))
+            .map(|k| (k.clone(), format!("{}/1", k)))
+            .collect();
+        for (k, t) in env.0.into_iter() {
+            let t = t.subst(&tau);
+            if let Some(new_key) = tau.get(&k) {
+                self.0.insert(new_key.clone(), t);
+            } else {
+                self.0.insert(k, t);
+            }
+        }
+        ty.subst(&tau)
+    }
     pub fn find_type(&self, name: &str) -> Result<&Type> {
         match self.0.get(name) {
             None => Err(Error::msg(format!("Unbound type identifier {}", name))),

diff --git a/rust/candid/src/types/internal.rs b/rust/candid/src/types/internal.rs
@@ -205,6 +205,48 @@ impl Type {
             _ => false,
         }
     }
+    pub fn subst(self, tau: &std::collections::BTreeMap<String, String>) -> Self {
+        use Type::*;
+        match self {
+            Var(id) => match tau.get(&id) {
+                None => Var(id),
+                Some(new_id) => Var(new_id.to_string()),
+            },
+            Opt(t) => Opt(Box::new(t.subst(tau))),
+            Vec(t) => Vec(Box::new(t.subst(tau))),
+            Record(fs) => Record(
+                fs.into_iter()
+                    .map(|Field { id, ty }| Field {
+                        id,
+                        ty: ty.subst(tau),
+                    })
+                    .collect(),
+            ),
+            Variant(fs) => Variant(
+                fs.into_iter()
+                    .map(|Field { id, ty }| Field {
+                        id,
+                        ty: ty.subst(tau),
+                    })
+                    .collect(),
+            ),
+            Func(func) => Func(Function {
+                modes: func.modes,
+                args: func.args.into_iter().map(|t| t.subst(tau)).collect(),
+                rets: func.rets.into_iter().map(|t| t.subst(tau)).collect(),
+            }),
+            Service(serv) => Service(
+                serv.into_iter()
+                    .map(|(meth, ty)| (meth, ty.subst(tau)))
+                    .collect(),
+            ),
+            Class(args, ty) => Class(
+                args.into_iter().map(|t| t.subst(tau)).collect(),
+                Box::new(ty.subst(tau)),
+            ),
+            _ => self,
+        }
+    }
 }
 impl fmt::Display for Type {
     fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {

diff --git a/rust/candid/src/types/subtype.rs b/rust/candid/src/types/subtype.rs
@@ -7,13 +7,7 @@ use std::collections::{HashMap, HashSet};
 pub type Gamma = HashSet<(Type, Type)>;
 
 /// Check if t1 <: t2
-pub fn subtype(
-    gamma: &mut Gamma,
-    env1: &TypeEnv,
-    t1: &Type,
-    env2: &TypeEnv,
-    t2: &Type,
-) -> Result<()> {
+pub fn subtype(gamma: &mut Gamma, env: &TypeEnv, t1: &Type, t2: &Type) -> Result<()> {
     use Type::*;
     if t1 == t2 {
         return Ok(());
@@ -23,10 +17,10 @@ pub fn subtype(
             return Ok(());
         }
         let res = match (t1, t2) {
-            (Var(id), _) => subtype(gamma, env1, env1.rec_find_type(id).unwrap(), env2, t2),
-            (_, Var(id)) => subtype(gamma, env1, t1, env2, env2.rec_find_type(id).unwrap()),
-            (Knot(id), _) => subtype(gamma, env1, &find_type(id).unwrap(), env2, t2),
-            (_, Knot(id)) => subtype(gamma, env1, t1, env2, &find_type(id).unwrap()),
+            (Var(id), _) => subtype(gamma, env, env.rec_find_type(id).unwrap(), t2),
+            (_, Var(id)) => subtype(gamma, env, t1, env.rec_find_type(id).unwrap()),
+            (Knot(id), _) => subtype(gamma, env, &find_type(id).unwrap(), t2),
+            (_, Knot(id)) => subtype(gamma, env, t1, &find_type(id).unwrap()),
             (_, _) => unreachable!(),
         };
         if res.is_err() {
@@ -38,12 +32,12 @@ pub fn subtype(
         (_, Reserved) => Ok(()),
         (Empty, _) => Ok(()),
         (Nat, Int) => Ok(()),
-        (Vec(ty1), Vec(ty2)) => subtype(gamma, env1, ty1, env2, ty2),
+        (Vec(ty1), Vec(ty2)) => subtype(gamma, env, ty1, ty2),
         (Null, Opt(_)) => Ok(()),
-        (Opt(ty1), Opt(ty2)) if subtype(gamma, env1, ty1, env2, ty2).is_ok() => Ok(()),
+        (Opt(ty1), Opt(ty2)) if subtype(gamma, env, ty1, ty2).is_ok() => Ok(()),
         (t1, Opt(ty2))
-            if subtype(gamma, env1, t1, env2, ty2).is_ok()
-                && !matches!(env2.trace_type(ty2)?, Null | Reserved | Opt(_)) =>
+            if subtype(gamma, env, t1, ty2).is_ok()
+                && !matches!(env.trace_type(ty2)?, Null | Reserved | Opt(_)) =>
         {
             Ok(())
         }
@@ -55,8 +49,8 @@ pub fn subtype(
             let fields: HashMap<_, _> = fs1.iter().map(|Field { id, ty }| (id, ty)).collect();
             for Field { id, ty: ty2 } in fs2.iter() {
                 match fields.get(id) {
-                    Some(ty1) => subtype(gamma, env1, ty1, env2, ty2).with_context(|| format!("Record field {}: {} is not a subtype of {}", id, ty1, ty2))?,
-                    None => subtype(gamma, env1, &Opt(Box::new(Empty)), env2, ty2).map_err(|_| anyhow::anyhow!("Record field {}: {} is only in the expected type and is not of opt, reserved or null type", id, ty2))?,
+                    Some(ty1) => subtype(gamma, env, ty1, ty2).with_context(|| format!("Record field {}: {} is not a subtype of {}", id, ty1, ty2))?,
+                    None => subtype(gamma, env, &Opt(Box::new(Empty)), ty2).map_err(|_| anyhow::anyhow!("Record field {}: {} is only in the expected type and is not of opt, reserved or null type", id, ty2))?,
                 }
             }
             Ok(())
@@ -65,7 +59,7 @@ pub fn subtype(
             let fields: HashMap<_, _> = fs2.iter().map(|Field { id, ty }| (id, ty)).collect();
             for Field { id, ty: ty1 } in fs1.iter() {
                 match fields.get(id) {
-                    Some(ty2) => subtype(gamma, env1, ty1, env2, ty2).with_context(|| {
+                    Some(ty2) => subtype(gamma, env, ty1, ty2).with_context(|| {
                         format!("Variant field {}: {} is not a subtype of {}", id, ty1, ty2)
                     })?,
                     None => {
@@ -82,7 +76,7 @@ pub fn subtype(
             let meths: HashMap<_, _> = ms1.iter().map(|(name, ty)| (name, ty)).collect();
             for (name, ty2) in ms2.iter() {
                 match meths.get(name) {
-                    Some(ty1) => subtype(gamma, env1, ty1, env2, ty2).with_context(|| {
+                    Some(ty1) => subtype(gamma, env, ty1, ty2).with_context(|| {
                         format!("Method {}: {} is not a subtype of {}", name, ty1, ty2)
                     })?,
                     None => {
@@ -105,10 +99,8 @@ pub fn subtype(
             let args2 = to_tuple(&f2.args);
             let rets1 = to_tuple(&f1.rets);
             let rets2 = to_tuple(&f2.rets);
-            subtype(gamma, env2, &args2, env1, &args1)
-                .context("Subtype fails at function input type")?;
-            subtype(gamma, env1, &rets1, env2, &rets2)
-                .context("Subtype fails at function return type")?;
+            subtype(gamma, env, &args2, &args1).context("Subtype fails at function input type")?;
+            subtype(gamma, env, &rets1, &rets2).context("Subtype fails at function return type")?;
             Ok(())
         }
         (Class(_, _), Class(_, _)) => unreachable!(),

diff --git a/tools/didc/src/main.rs b/tools/didc/src/main.rs
@@ -158,13 +158,14 @@ fn parse_types(str: &str) -> Result<IDLTypes, Error> {
 fn main() -> Result<()> {
     match Command::from_args() {
         Command::Check { input, previous } => {
-            let (env, opt_t1) = pretty_check_file(&input)?;
+            let (mut env, opt_t1) = pretty_check_file(&input)?;
             if let Some(previous) = previous {
                 let (env2, opt_t2) = pretty_check_file(&previous)?;
                 match (opt_t1, opt_t2) {
                     (Some(t1), Some(t2)) => {
                         let mut gamma = HashSet::new();
-                        candid::types::subtype::subtype(&mut gamma, &env, &t1, &env2, &t2)?;
+                        let t2 = env.merge_type(env2, t2);
+                        candid::types::subtype::subtype(&mut gamma, &env, &t1, &t2)?;
                     }
                     _ => {
                         bail!("did file need to contain the main service type for subtyping check")
@@ -180,7 +181,7 @@ fn main() -> Result<()> {
             };
             let ty1 = env.ast_to_type(&ty1)?;
             let ty2 = env.ast_to_type(&ty2)?;
-            candid::types::subtype::subtype(&mut HashSet::new(), &env, &ty1, &env, &ty2)?;
+            candid::types::subtype::subtype(&mut HashSet::new(), &env, &ty1, &ty2)?;
         }
         Command::Bind { input, target } => {
             let (env, actor) = pretty_check_file(&input)?;