revise Set

This commit is contained in:
Folkert 2020-06-23 15:36:02 +02:00
parent 6f1639959a
commit b88dfcb537
2 changed files with 92 additions and 51 deletions

View file

@ -845,72 +845,73 @@ pub fn types() -> MutMap<Symbol, (SolvedType, Region)> {
// Set module // Set module
// empty : Set a // empty : Set a
add_type(Symbol::SET_EMPTY, set_type(UVAR1, TVAR1)); add_type(Symbol::SET_EMPTY, {
let_tvars! { star, a };
set_type(star, a)
});
// singleton : a -> Set a // singleton : a -> Set a
add_type( add_type(Symbol::SET_SINGLETON, {
Symbol::SET_SINGLETON, let_tvars! { star, a };
unique_function(vec![flex(TVAR1)], set_type(UVAR1, TVAR1)), unique_function(vec![flex(a)], set_type(star, a))
); });
// op : Attr (u | *) (Set (Attr u a)), Attr (u | *) (Set (Attr u a)) -> Attr * Set (Attr u a) // union : Attr * (Set * a)
// , Attr * (Set * a)
// -> Attr * (Set * a)
let set_combine = { let set_combine = {
let mut store = IDStore::new(); let_tvars! { star1, star2, star3, star4, star5, star6, a };
let u = store.fresh();
let a = store.fresh();
let star1 = store.fresh();
let star2 = store.fresh();
let star3 = store.fresh();
unique_function( unique_function(
vec![ vec![
SolvedType::Apply( SolvedType::Apply(
Symbol::ATTR_ATTR, Symbol::ATTR_ATTR,
vec![ vec![
container(star1, vec![u]), flex(star1),
SolvedType::Apply(Symbol::SET_SET, vec![attr_type(u, a)]), SolvedType::Apply(Symbol::SET_SET, vec![attr_type(star2, a)]),
], ],
), ),
SolvedType::Apply( SolvedType::Apply(
Symbol::ATTR_ATTR, Symbol::ATTR_ATTR,
vec![ vec![
container(star2, vec![u]), flex(star3),
SolvedType::Apply(Symbol::SET_SET, vec![attr_type(u, a)]), SolvedType::Apply(Symbol::SET_SET, vec![attr_type(star4, a)]),
], ],
), ),
], ],
SolvedType::Apply( SolvedType::Apply(
Symbol::ATTR_ATTR, Symbol::ATTR_ATTR,
vec![ vec![
flex(star3), flex(star5),
SolvedType::Apply(Symbol::SET_SET, vec![attr_type(u, a)]), SolvedType::Apply(Symbol::SET_SET, vec![attr_type(star6, a)]),
], ],
), ),
) )
}; };
// union : Set a, Set a -> Set a // union : Attr * (Set * a)
// , Attr * (Set * a)
// -> Attr * (Set * a)
add_type(Symbol::SET_UNION, set_combine.clone()); add_type(Symbol::SET_UNION, set_combine.clone());
// diff : Set a, Set a -> Set a // diff : Attr * (Set * a)
// , Attr * (Set * a)
// -> Attr * (Set * a)
add_type(Symbol::SET_DIFF, set_combine); add_type(Symbol::SET_DIFF, set_combine);
// foldl : Attr (u | *) (Set (Attr u a)), Attr Shared (Attr u a -> b -> b), b -> b // foldl : Attr (* | u) (Set (Attr u a))
// , Attr Shared (Attr u a -> b -> b)
// , b
// -> b
add_type(Symbol::SET_FOLDL, { add_type(Symbol::SET_FOLDL, {
let mut store = IDStore::new(); let_tvars! { star, u, a, b };
let u = store.fresh();
let a = store.fresh();
let b = store.fresh();
let star1 = store.fresh();
unique_function( unique_function(
vec![ vec![
SolvedType::Apply( SolvedType::Apply(
Symbol::ATTR_ATTR, Symbol::ATTR_ATTR,
vec![ vec![
container(star1, vec![u]), container(star, vec![u]),
SolvedType::Apply(Symbol::SET_SET, vec![attr_type(u, a)]), SolvedType::Apply(Symbol::SET_SET, vec![attr_type(u, a)]),
], ],
), ),
@ -924,54 +925,47 @@ pub fn types() -> MutMap<Symbol, (SolvedType, Region)> {
) )
}); });
// insert : Attr (u | *) (Set (Attr u a)), Attr (u | *) a -> Attr * (Set (Attr u a)) // insert : Attr * (Set a)
// , a
// , Attr * (Set a)
add_type(Symbol::SET_INSERT, { add_type(Symbol::SET_INSERT, {
let mut store = IDStore::new(); let_tvars! { star1, star2, a };
let u = store.fresh();
let a = store.fresh();
let star1 = store.fresh();
let star2 = store.fresh();
let star3 = store.fresh();
unique_function( unique_function(
vec![ vec![
SolvedType::Apply( SolvedType::Apply(
Symbol::ATTR_ATTR, Symbol::ATTR_ATTR,
vec![ vec![
container(star1, vec![u]), flex(star1),
SolvedType::Apply(Symbol::SET_SET, vec![attr_type(u, a)]), SolvedType::Apply(Symbol::SET_SET, vec![flex(a)]),
], ],
), ),
SolvedType::Apply(Symbol::ATTR_ATTR, vec![container(star2, vec![u]), flex(a)]), flex(a),
], ],
SolvedType::Apply( SolvedType::Apply(
Symbol::ATTR_ATTR, Symbol::ATTR_ATTR,
vec![ vec![
flex(star3), flex(star2),
SolvedType::Apply(Symbol::SET_SET, vec![attr_type(u, a)]), SolvedType::Apply(Symbol::SET_SET, vec![flex(a)]),
], ],
), ),
) )
}); });
// we can remove a key that is shared from a set of unique keys // we can remove a key that is shared from a set of unique keys
// remove : Attr (u | *) (Set (Attr u a)), Attr * a -> Attr * (Set (Attr u a)) //
// remove : Attr * (Set (Attr u a))
// , Attr * a
// , Attr * (Set (Attr u a))
add_type(Symbol::SET_REMOVE, { add_type(Symbol::SET_REMOVE, {
let mut store = IDStore::new(); let_tvars! { u, a, star1, star2, star3 };
let u = store.fresh();
let a = store.fresh();
let star1 = store.fresh();
let star2 = store.fresh();
let star3 = store.fresh();
unique_function( unique_function(
vec![ vec![
SolvedType::Apply( SolvedType::Apply(
Symbol::ATTR_ATTR, Symbol::ATTR_ATTR,
vec![ vec![
container(star1, vec![u]), flex(star1),
SolvedType::Apply(Symbol::SET_SET, vec![attr_type(u, a)]), SolvedType::Apply(Symbol::SET_SET, vec![attr_type(u, a)]),
], ],
), ),

View file

@ -2151,6 +2151,53 @@ mod test_uniq_solve {
); );
} }
#[test]
fn set_empty() {
infer_eq("Set.empty", "Attr * (Set *)");
}
#[test]
fn set_singelton() {
infer_eq("Set.singleton", "Attr * (a -> Attr * (Set a))");
}
#[test]
fn set_union() {
infer_eq(
"Set.union",
"Attr * (Attr * (Set (Attr * a)), Attr * (Set (Attr * a)) -> Attr * (Set (Attr * a)))",
);
}
#[test]
fn set_diff() {
infer_eq(
"Set.diff",
"Attr * (Attr * (Set (Attr * a)), Attr * (Set (Attr * a)) -> Attr * (Set (Attr * a)))",
);
}
#[test]
fn set_foldl() {
infer_eq(
"Set.foldl",
"Attr * (Attr (* | a) (Set (Attr a b)), Attr Shared (Attr a b, c -> c), c -> c)",
);
}
#[test]
fn set_insert() {
infer_eq("Set.insert", "Attr * (Attr * (Set a), a -> Attr * (Set a))");
}
#[test]
fn set_remove() {
infer_eq(
"Set.remove",
"Attr * (Attr * (Set (Attr a b)), Attr * b -> Attr * (Set (Attr a b)))",
);
}
#[test] #[test]
fn use_correct_ext_var() { fn use_correct_ext_var() {
infer_eq( infer_eq(