use sets in permissions

src/grammar.rs

@@ -1,6 +1,6 @@
 pub use crate::dada_lang::grammar::*;
 use crate::dada_lang::FormalityLang;
-use formality_core::{term, variable, Fallible, Upcast};
+use formality_core::{term, variable, Fallible, Set, Upcast};
 use std::sync::Arc;
 
 mod cast_impls;
@@ -238,14 +238,14 @@ impl Ty {
 
 #[term]
 pub enum Perm {
-    Given(Vec<Place>),
+    #[grammar(given $(?v0))]
+    Given(Set<Place>),
 
-    // FIXME: make these sets
     #[grammar(shared $(?v0))]
-    Shared(Vec<Place>),
+    Shared(Set<Place>),
 
     #[grammar(leased $(v0))]
-    Leased(Vec<Place>),
+    Leased(Set<Place>),
 
     #[variable(Kind::Perm)]
     Var(Variable),

src/type_system/cancellation.rs

@@ -1,4 +1,4 @@
-use formality_core::{judgment_fn, seq, set, Set, Upcast};
+use formality_core::{judgment_fn, seq, set, Set, SetExt, Upcast};
 
 use crate::{
     grammar::{Kind, Perm, Place, Ty},
@@ -221,21 +221,20 @@ judgment_fn! {
         (
             (if let Perm::Given(places) = perm)
             (0..places.len() => i)
-            (let place = &places[i])
-            (let other_places = seq![..&places[0..i], ..&places[i+1..]])
-            (type_place(&env, place) => place_ty)
+            (places.split_nth(i) => (place, other_places))
+            (type_place(&env, &place) => place_ty)
             (let canceled_ty = place_ty.rebase_perms(&*ty))
             (let (env, result_ty) = union_with_given(&env, canceled_ty, &other_places, &*ty))
             ---------------------- ("(given() P) => P")
-            (cancel(env, Ty::ApplyPerm(perm, ty)) => (env, result_ty, set![place]))
+            (cancel(env, Ty::ApplyPerm(perm, ty)) => (env, result_ty, set![place.clone()]))
         )
     }
 }
 
 fn union_with_given(
     env: impl Upcast<Env>,
     canceled_ty: Ty,
-    other_places: &Vec<&Place>,
+    other_places: &Set<Place>,
     base_ty: &Ty,
 ) -> (Env, Ty) {
     let mut env = env.upcast();

src/type_system/tests.rs

@@ -28,7 +28,7 @@ fn bad_class_name_in_fn_parameter() {
     "#]]
     .assert_debug_eq(&check_program(&term(
         "
-        fn no_such_class(c: owned ClassName) -> () {}
+        fn no_such_class(c: given ClassName) -> () {}
     ",
     )));
 }

src/type_system/type_subtype.rs

@@ -1,4 +1,4 @@
-use formality_core::{judgment_fn, Downcast};
+use formality_core::{judgment_fn, Downcast, Set};
 
 use crate::{
     dada_lang::grammar::{ExistentialVar, Variable},
@@ -384,15 +384,15 @@ judgment_fn! {
 /// True if every place listed in `places` is "covered" by one of the places in
 /// `covering_places`. A place P1 *covers* a place P2 if it is a prefix:
 /// for example, `x.y` covers `x.y` and `x.y.z` but not `x.z` or `x1`.
-fn all_places_covered_by_one_of(places: &[Place], covering_places: &[Place]) -> bool {
+fn all_places_covered_by_one_of(places: &Set<Place>, covering_places: &Set<Place>) -> bool {
     places
         .iter()
         .all(|place| place_covered_by_one_of(place, covering_places))
 }
 
 /// See [`all_places_covered_by_one_of`][].
 #[tracing::instrument(level = "Debug", ret)]
-fn place_covered_by_one_of(place: &Place, covering_places: &[Place]) -> bool {
+fn place_covered_by_one_of(place: &Place, covering_places: &Set<Place>) -> bool {
     covering_places
         .iter()
         .any(|covering_place| place_covered_by_place(place, covering_place))