Capability types

ibis/benches/checking_and_planning.rs

@@ -34,16 +34,16 @@ pub fn criterion_benchmark_noop_planning(c: &mut Criterion) {
   "recipes": [
     {
       "nodes": [
-        ["p_a", "a", "write", "Int"],
-        ["p_b", "b", "any", "Number"],
-        ["p_c", "c", "write", "String"],
-        ["p_de", "d", "read", "Serializable"],
-        ["p_de", "e", "read", "ibis.UnionType(Number, String)"],
-        ["p_f", "f", "write", "ibis.ProductType(name: String, age: Int)"],
-        ["p_g", "g", "read", "name: *"],
-        ["p_h", "h", "read", "ibis.ProductType(name: String, age: Int)"],
-        ["p_i", "i", "read", "name: String"],
-        ["p_j", "j", "read", "age: Int"]
+        ["p_a", "a", "write Int"],
+        ["p_b", "b", "any Number"],
+        ["p_c", "c", "write String"],
+        ["p_de", "d", "read Serializable"],
+        ["p_de", "e", "read ibis.UnionType(Number, String)"],
+        ["p_f", "f", "write {name: String, age: Int}"],
+        ["p_g", "g", "read {name: *}"],
+        ["p_h", "h", "read {name: String, age: Int}"],
+        ["p_i", "i", "read {name: String}"],
+        ["p_j", "j", "read {age: Int}"]
       ],
       "claims": [
         ["a", "private"]

ibis/benches/checking_only.rs

@@ -34,16 +34,16 @@ pub fn criterion_benchmark_checking_only(c: &mut Criterion) {
   "recipes": [
     {
       "nodes": [
-        ["p_a", "a", "write", "Int"],
-        ["p_b", "b", "any", "Number"],
-        ["p_c", "c", "write", "String"],
-        ["p_de", "d", "read", "Serializable"],
-        ["p_de", "e", "read", "ibis.UnionType(Number, String)"],
-        ["p_f", "f", "write", "ibis.ProductType(name: String, age: Int)"],
-        ["p_g", "g", "read", "name: *"],
-        ["p_h", "h", "read", "ibis.ProductType(name: String, age: Int)"],
-        ["p_i", "i", "read", "name: String"],
-        ["p_j", "j", "read", "age: Int"]
+        ["p_a", "a", "write Int"],
+        ["p_b", "b", "any Number"],
+        ["p_c", "c", "write String"],
+        ["p_de", "d", "read Serializable"],
+        ["p_de", "e", "read ibis.UnionType(Number, String)"],
+        ["p_f", "f", "write {name: String, age: Int}"],
+        ["p_g", "g", "read {name: *}"],
+        ["p_h", "h", "read {name: String, age: Int}"],
+        ["p_i", "i", "read {name: String}"],
+        ["p_j", "j", "read {age: Int}"]
       ],
       "claims": [
         ["a", "private"]

ibis/demo.json

@@ -25,25 +25,25 @@
         "name": "demo"
       },
       "nodes": [
-        ["p_a", "a", "write", "Int"],
-        ["p_b", "b", "any", "Number"],
-        ["p_c", "c", "write", "String"],
-        ["p_de", "d", "read", "Serializable"],
-        ["p_de", "e", "read", "ibis.UnionType(Number, String)"],
-        ["p_f", "f", "write", "ibis.ProductType(name: String, age: Int)"],
-        ["p_g", "g", "read", "name: *"],
-        ["p_h", "h", "read", "ibis.ProductType(name: String, age: Int)"],
-        ["p_i", "i", "read", "name: String"],
-        ["p_j", "j", "read", "age: Int"]
-      ],
-      "edges": [
-        ["b", "e"]
+        ["p_a", "a", "write Int"],
+        ["p_b", "b", "any Number"],
+        ["p_c", "c", "write String"],
+        ["p_de", "d", "read Serializable"],
+        ["p_de", "e", "read ibis.UnionType(Number, String)"],
+        ["p_f", "f", "write {name: String, age: Int}"],
+        ["p_g", "g", "read {name: *}"],
+        ["p_h", "h", "read {name: String, age: Int}"],
+        ["p_i", "i", "read {name: String}"],
+        ["p_j", "j", "read {age: Int}"]
       ],
       "claims": [
         ["a", "private"]
       ],
       "checks": [
-        ["e", "public"]
+        ["e", "pubic"]
+      ],
+      "edges": [
+        ["b", "e"]
       ],
       "trusted_to_remove_tag": [
         ["b", "private"]

ibis/docs/idealised_grammar.md

@@ -0,0 +1,45 @@
+# Idealised language EBNF
+
+The follow can be used with ebnf tooling like https://matthijsgroen.github.io/ebnf2railroad/try-yourself.html
+
+```ebnf
+grammar = type;
+type = {capability, " " }, structure, {" + ", tag};
+
+tag=label;
+capability = label;
+structure = "*" | parenthesized | product | simple;
+
+simple = type_name, [args];
+args = "(", type, {",", type}, ")";
+
+named = label, ": ", type;
+
+parenthesized = "(", type, ")";
+
+product = "{", (named | type), {",", (named | type)}, "}";
+union = "(", type, {"|", type }, ")";
+
+label = lower_letter , { letter | digit | "_" };
+type_name = upper_letter , { letter | digit | "_" };
+
+(*
+  Basic components
+  ----------------
+  These are low level components, the small building blocks.
+*)
+
+letter = upper_letter | lower_letter ;
+
+upper_letter = "A" | "B" | "C" | "D" | "E" | "F" | "G"
+       | "H" | "I" | "J" | "K" | "L" | "M" | "N"
+       | "O" | "P" | "Q" | "R" | "S" | "T" | "U"
+       | "V" | "W" | "X" | "Y" | "Z";
+lower_letter = "a" | "b"
+       | "c" | "d" | "e" | "f" | "g" | "h" | "i"
+       | "j" | "k" | "l" | "m" | "n" | "o" | "p"
+       | "q" | "r" | "s" | "t" | "u" | "v" | "w"
+       | "x" | "y" | "z" ;
+
+digit = "0" | "1" | "2" | "3" | "4" | "5" | "6" | "7" | "8" | "9" ;
+```

ibis/src/lib.rs

@@ -61,7 +61,17 @@ macro_rules! is_a {
         use crate::type_parser::read_type;
         let name = $type.name();
         let ty = read_type(&name);
-        ty.name == $parent.name()
+        ty.name == $parent.name() && !ty.args.is_empty()
+    }};
+}
+
+#[macro_export]
+macro_rules! name {
+    ($type: expr) => {{
+        use crate::type_parser::read_type;
+        let name = $type.name();
+        let ty = read_type(&name);
+        ent!(&format!("{}", ty.name))
     }};
 }
 
@@ -71,7 +81,22 @@ macro_rules! arg {
         use crate::type_parser::read_type;
         let name = $type.name();
         let ty = read_type(&name);
-        ent!(&format!("{}", ty.args[$ind]))
+        let ind = $ind;
+        if ind >= ty.args.len() {
+            panic!("Cannot access argument {} of {}", ind, name);
+        }
+        ent!(&format!("{}", ty.args[ind]))
+    }};
+}
+
+#[macro_export]
+macro_rules! args {
+    ($type: expr) => {{
+        use crate::type_parser::read_type;
+        read_type(&$type.name())
+            .args
+            .iter()
+            .map(|arg| ent!(&format!("{}", arg)))
     }};
 }
 
@@ -92,7 +117,12 @@ pub fn get_solutions(data: &str, loss: Option<usize>) -> Ibis {
     let mut runtime = Ibis::new();
 
     // TODO: Use ibis::Error and https://serde.rs/error-handling.html instead of expect.
-    let recipes: Ibis = serde_json::from_str(data).expect("JSON Error?");
+    let recipes: Ibis = serde_json::from_str(data)
+        .map_err(|e| {
+            eprintln!("{}", data);
+            e
+        })
+        .expect("JSON Error?");
     runtime.add_recipes(recipes);
 
     runtime.extract_solutions_with_loss(loss)

ibis/src/recipes.rs

@@ -1,5 +1,5 @@
 use crate::util::make;
-use crate::{apply, arg, ent, ibis, is_a, Ent, Sol, SolutionData, ToInput};
+use crate::{apply, arg, args, ent, ibis, is_a, name, Ent, Sol, SolutionData, ToInput};
 use serde::{Deserialize, Serialize};
 
 ibis! {
@@ -10,7 +10,9 @@ ibis! {
     LessPrivateThan(Ent, Ent); // tag, tag
     Capability(Ent, Ent); // cap from, cap to
     Subtype(Ent, Ent); // sub, super
-    Node(Ent, Ent, Ent, Ent); // particle-identifier, identifier, capability, type
+    CompatibleWith(Ent, Ent); // from, to
+    HasCapability(Ent, Ent); // cap, ty
+    Node(Ent, Ent, Ent); // particle-identifier, identifier, capability, type
     Claim(Ent, Ent); // identifier, tag
     Check(Ent, Ent); // identifier, tag
     TrustedToRemoveTag(Ent, Ent); // node, tag
@@ -19,17 +21,51 @@ ibis! {
     HasTag(Sol, Ent, Ent, Ent); // solution, source node, node with tag, tag
     Leak(Sol, Ent, Ent, Ent, Ent); // sol, node, expected_tag, source, tag2
     TypeError(Sol, Ent, Ent, Ent, Ent); // sol, node, ty, source, ty
-    CapabilityError(Sol, Ent, Ent, Ent, Ent); // sol, node, cap, source, cap
 
     UncheckedSolution(parent.add_edge(from, to)) <-
         PlanningIsEnabled(true),
-        Capability(from_capability, to_capability),
-        Node(from_particle, from, from_capability, from_type),
-        Subtype(from_type, to_type),
-        Node(to_particle, to, to_capability, to_type),
+        Node(from_particle, from, from_type),
+        Node(to_particle, to, to_type),
         (from != to),
+        CompatibleWith(from_type, to_type),
+        // ({eprintln!("Connecting {}: {} to {}: {}", from, from_type, to, to_type); true}),
         UncheckedSolution(parent);
 
+    HasCapability(arg!(ty, 0), ty) <-
+        KnownType(ty),
+        (is_a!(ty, ent!("ibis.WithCapability")));
+
+    HasCapability(cap, ty) <-
+        KnownType(ty),
+        (is_a!(ty, ent!("ibis.WithCapability"))),
+        HasCapability(cap, arg!(ty, 1)); // Has all the child capabilities too.
+
+    // Base case: just types.
+    CompatibleWith(x, y) <-
+        KnownType(x),
+        (!is_a!(x, ent!("ibis.WithCapability"))),
+        KnownType(y),
+        (!is_a!(y, ent!("ibis.WithCapability"))),
+        // ({eprintln!("checking subtyping ({}) ({})", x, y); true}),
+        Subtype(x, y);
+
+    CompatibleWith(x, y) <- // Check that y has the capabilities required by x.
+        KnownType(x),
+        (is_a!(x, ent!("ibis.WithCapability"))),
+        KnownType(y),
+        HasCapability(cap, y), // For each of the capabilities y supports
+        // ({eprintln!("checking y has cap ({}) ({})", x, y); true}),
+        Capability(arg!(x, 0), cap), // If this one is supported we can continue.
+        CompatibleWith(arg!(x, 1), y);
+
+    CompatibleWith(x, y) <- // If a type has no capabilities, discard the capabilities of it's possible super type.
+        KnownType(x),
+        (!is_a!(x, ent!("ibis.WithCapability"))),
+        KnownType(y),
+        (is_a!(y, ent!("ibis.WithCapability"))),
+        // ({eprintln!("discarding capability from y ({}) ({})", x, y); true}),
+        CompatibleWith(x, arg!(y, 1));
+
     Subtype(
         x,
         prod
@@ -115,8 +151,8 @@ ibis! {
 
     HasTag(s, source, down, tag) <- // Propagate tags 'across stream' (i.e. inside a particle)
         HasTag(s, source, curr, tag),
-        Node(particle, curr, _, _),
-        Node(particle, down, _, _),
+        Node(particle, curr, _),
+        Node(particle, down, _),
         !TrustedToRemoveTag(down, tag);
 
     Leak(s, n, t1, source, t2) <-
@@ -127,24 +163,18 @@ ibis! {
     TypeError(s, *from, from_ty, *to, to_ty) <-
         UncheckedSolution(s),
         for (from, to) in &s.solution().edges,
-        Node(_from_p, *from, _, from_ty),
-        Node(_to_p, *to, _, to_ty),
-        !Subtype(from_ty, to_ty); // Check failed, from writes an incompatible type into to
-
-    CapabilityError(s, *from, from_capability, *to, to_capability) <-
-        UncheckedSolution(s),
-        for (from, to) in &s.solution().edges,
-        Node(_from_p, *from, from_capability, _),
-        Node(_to_p, *to, to_capability, _),
-        !Capability(from_capability, to_capability); // Check failed, from writes an incompatible type into to
+        Node(_from_p, *from, from_ty),
+        Node(_to_p, *to, to_ty),
+        !CompatibleWith(from_ty, to_ty); // Check failed, from writes an incompatible type into to
 
     Solution(s) <-
         UncheckedSolution(s),
         !TypeError(s, _, _, _, _),
-        !CapabilityError(s, _, _, _, _),
         !Leak(s, _, _, _, _);
 
-    KnownType(x) <- Node(_par, _node, _cap, x); // Infer types that are used in the recipes.
+    KnownType(name!(ty)) <- KnownType(ty); // Types without their arguments are still types
+    KnownType(arg) <- KnownType(ty), for arg in args!(ty); // Types arguments are types
+    KnownType(x) <- Node(_par, _node, x); // Infer types that are used in the recipes.
     KnownType(x) <- Subtype(x, _);
     KnownType(y) <- Subtype(_, y);
     Subtype(x, ent!("ibis.UniversalType")) <- KnownType(x); // Create a universal type.
@@ -188,8 +218,6 @@ pub struct Feedback {
     #[serde(default, skip_serializing_if = "is_default")]
     pub type_errors: Vec<TypeError>,
     #[serde(default, skip_serializing_if = "is_default")]
-    pub capability_errors: Vec<CapabilityError>,
-    #[serde(default, skip_serializing_if = "is_default")]
     pub has_tags: Vec<HasTag>,
 }
 
@@ -381,14 +409,15 @@ impl Ibis {
             mut less_private_than,
             mut capabilities,
             mut subtypes,
+            _compatible_with,
+            _has_capability,
             nodes,
             claims,
             checks,
             trusted_to_remove_tag,
             has_tags,
             leaks,
             type_errors,
-            capability_errors,
         ) = runtime.run();
         let recipes: Vec<Sol> = if self.config.flags.planning {
             solutions.iter().map(|Solution(s)| *s).collect()
@@ -412,11 +441,6 @@ impl Ibis {
                         .filter(|TypeError(type_s, _, _, _, _)| type_s == s)
                         .cloned()
                         .collect(),
-                    capability_errors: capability_errors
-                        .iter()
-                        .filter(|CapabilityError(cap_s, _, _, _, _)| cap_s == s)
-                        .cloned()
-                        .collect(),
                     has_tags: has_tags
                         .iter()
                         .filter(|HasTag(has_tag_s, _, _, _)| has_tag_s == s)

ibis/src/to_dot_impls.rs

@@ -73,7 +73,7 @@ impl ToDot for (&Ibis, &Recipe) {
         let node_id = |node| format!("{}_h_{}", &s_id, node).replace('.', "_");
         let mut sol_graph = DotGraph::default();
         let mut particles = HashMap::new();
-        for Node(particle, node, cap, ty) in &ibis.shared.nodes {
+        for Node(particle, node, ty) in &ibis.shared.nodes {
             let mut extras: Vec<String> = vec![];
             for HasTag(_hts, source, sink, tag) in &recipe.feedback.has_tags {
                 if sink == node && source != node {
@@ -103,7 +103,7 @@ impl ToDot for (&Ibis, &Recipe) {
                 .map(|ex| format!("<tr><td>{}</td></tr>", ex))
                 .collect();
             let particle_g = particles.entry(particle).or_insert_with(DotGraph::default);
-            particle_g.add_node(format!("{node_id} [shape=record label=< <table border=\"0\"><tr><td>{cap} {node} : {ty}</td></tr>{extras}</table>>]", node_id=node_id(node), node=node, cap=cap, ty=ty, extras=extras.join("")));
+            particle_g.add_node(format!("{node_id} [shape=record label=< <table border=\"0\"><tr><td>{node} : {ty}</td></tr>{extras}</table>>]", node_id=node_id(node), node=node, ty=ty, extras=extras.join("")));
         }
         for (particle, particle_g) in particles {
             sol_graph.add_child(