diff --git a/src/morphism.rs b/src/morphism.rs
index 4216b33..e713e61 100644
--- a/src/morphism.rs
+++ b/src/morphism.rs
@@ -174,83 +174,104 @@ impl<M: Morphism + Clone> MorphismBase<M> {
/* try to find shortest morphism-path for a given type
*/
pub fn find_morphism_path(&self, ty: MorphismType
- /*, type_dict: &mut impl TypeDict*/
+// , type_dict: &mut impl TypeDict
)
-> Option< Vec<MorphismInstance<M>> >
{
let ty = ty.normalize();
let mut queue = vec![
- MorphismPath { weight: 0, cur_type: ty.src_type.clone(), morphisms: vec![] }
+ MorphismPath::<M> { weight: 0, cur_type: ty.src_type.clone(), morphisms: vec![] }
];
-
+
while ! queue.is_empty() {
queue.sort_by( |p1,p2| p2.weight.cmp(&p1.weight));
if let Some(mut cur_path) = queue.pop() {
if let Ok((halo, σ)) = crate::unification::subtype_unify( &cur_path.cur_type, &ty.dst_type ) {
- // found path
+ /* found path,
+ * now apply substitution and trim to variables in terms of each step
+ */
for n in cur_path.morphisms.iter_mut() {
+ let src_type = n.m.get_type().src_type;
+ let dst_type = n.m.get_type().dst_type;
+
let mut new_σ = HashMap::new();
for (k,v) in σ.iter() {
- new_σ.insert(
- k.clone(),
- v.clone().apply_substitution(&|k| σ.get(k).cloned()).clone()
- );
+ if let TypeID::Var(varid) = k {
+ if src_type.contains_var(*varid)
+ || dst_type.contains_var(*varid) {
+ new_σ.insert(
+ k.clone(),
+ v.clone().apply_substitution(&|k| σ.get(k).cloned()).clone().strip()
+ );
+ }
+ }
}
for (k,v) in n.σ.iter() {
- new_σ.insert(
- k.clone(),
- v.clone().apply_substitution(&|k| σ.get(k).cloned()).clone()
- );
+ if let TypeID::Var(varid) = k {
+ if src_type.contains_var(*varid)
+ || dst_type.contains_var(*varid) {
+ new_σ.insert(
+ k.clone(),
+ v.clone().apply_substitution(&|k| σ.get(k).cloned()).clone().strip()
+ );
+ }
+ }
}
+ n.halo = n.halo.clone().apply_substitution(
+ &|k| σ.get(k).cloned()
+ ).clone().strip();
+
n.σ = new_σ;
}
return Some(cur_path.morphisms);
}
- //eprintln!("cur path (w ={}) : @ {}", cur_path.weight, cur_path.cur_type.clone().sugar(type_dict).pretty(type_dict, 0) );
- for next_morph_inst in self.enum_morphisms(&cur_path.cur_type) {
+ //eprintln!("cur path (w ={}) : @ {:?}", cur_path.weight, cur_path.cur_type);//.clone().sugar(type_dict).pretty(type_dict, 0) );
+ for mut next_morph_inst in self.enum_morphisms(&cur_path.cur_type) {
let dst_type = next_morph_inst.get_type().dst_type;
+// eprintln!("try morph to {}", dst_type.clone().sugar(type_dict).pretty(type_dict, 0));
let mut creates_loop = false;
let mut new_path = cur_path.clone();
for n in new_path.morphisms.iter_mut() {
let mut new_σ = HashMap::new();
- for (k,v) in n.σ.iter() {
- new_σ.insert(
- k.clone(),
- v.clone().apply_substitution(&|k| next_morph_inst.σ.get(k).cloned()).clone()
- );
- }
+
for (k,v) in next_morph_inst.σ.iter() {
new_σ.insert(
k.clone(),
v.clone().apply_substitution(&|k| next_morph_inst.σ.get(k).cloned()).clone()
);
}
+
+ for (k,v) in n.σ.iter() {
+ new_σ.insert(
+ k.clone(),
+ v.clone().apply_substitution(&|k| next_morph_inst.σ.get(k).cloned()).clone()
+ );
+ }
+
+ n.halo = n.halo.clone().apply_substitution(
+ &|k| next_morph_inst.σ.get(k).cloned()
+ ).clone().strip();
+
n.σ = new_σ;
}
for m in new_path.morphisms.iter() {
if m.get_type().src_type == dst_type {
creates_loop = true;
- //eprintln!("creates loop..");
break;
}
}
if ! creates_loop {
- /*eprintln!("next morph ? \n {}\n--> {} ",
- next_morph_inst.get_type().src_type.sugar(type_dict).pretty(type_dict, 0),
- next_morph_inst.get_type().dst_type.sugar(type_dict).pretty(type_dict, 0)
- );
- eprintln!("....take!\n :: halo = {}\n :: σ = {:?}", next_morph_inst.halo.clone().sugar(type_dict).pretty(type_dict, 0), next_morph_inst.σ);
- */
new_path.weight += next_morph_inst.m.weight();
new_path.cur_type = dst_type;
+
new_path.morphisms.push(next_morph_inst);
queue.push(new_path);
}
diff --git a/src/term.rs b/src/term.rs
index 7f9354e..ec58afb 100644
--- a/src/term.rs
+++ b/src/term.rs
@@ -131,9 +131,17 @@ impl TypeTerm {
let mut rungs :Vec<_> = rungs.into_iter()
.filter_map(|mut r| {
r = r.strip();
- if r != TypeTerm::unit() { Some(r) }
+ if r != TypeTerm::unit() {
+ Some(match r {
+ TypeTerm::Ladder(r) => r,
+ a => vec![ a ]
+ })
+ }
else { None }
- }).collect();
+ })
+ .flatten()
+ .collect();
+
if rungs.len() == 1 {
rungs.pop().unwrap()
} else {
diff --git a/src/test/morphism.rs b/src/test/morphism.rs
index 4d33df6..6320f72 100644
--- a/src/test/morphism.rs
+++ b/src/test/morphism.rs
@@ -70,7 +70,216 @@ fn morphism_test_setup() -> ( BimapTypeDict, MorphismBase<DummyMorphism> ) {
}
#[test]
-fn test_morphism_path() {
+fn test_morphism_path1() {
+ let (mut dict, mut base) = morphism_test_setup();
+
+ let path = base.find_morphism_path(MorphismType {
+ src_type: dict.parse("<Digit 10> ~ Char").unwrap(),
+ dst_type: dict.parse("<Digit 10> ~ ℤ_2^64 ~ machine.UInt64").unwrap(),
+ });
+
+ assert_eq!(
+ path,
+ Some(
+ vec![
+ MorphismInstance {
+ σ: vec![
+ (dict.get_typeid(&"Radix".into()).unwrap(), TypeTerm::Num(10)),
+ ].into_iter().collect(),
+ halo: TypeTerm::unit(),
+ m: DummyMorphism(MorphismType {
+ src_type: dict.parse("<Digit Radix> ~ Char").unwrap(),
+ dst_type: dict.parse("<Digit Radix> ~ ℤ_2^64 ~ machine.UInt64").unwrap()
+ }),
+ }
+ ]
+ ));
+}
+
+
+#[test]
+fn test_morphism_path2() {
+ let (mut dict, mut base) = morphism_test_setup();
+
+ let path = base.find_morphism_path(MorphismType {
+ src_type: dict.parse("ℕ ~ <PosInt 10 BigEndian> ~ <Seq <Digit 10> ~ Char>").unwrap(),
+ dst_type: dict.parse("ℕ ~ <PosInt 10 BigEndian> ~ <Seq <Digit 10> ~ ℤ_2^64 ~ machine.UInt64>").unwrap(),
+ });
+
+ assert_eq!(
+ path,
+ Some(
+ vec![
+ MorphismInstance {
+ σ: vec![
+ (dict.get_typeid(&"Radix".into()).unwrap(), TypeTerm::Num(10)),
+ ].into_iter().collect(),
+ halo: dict.parse("ℕ ~ <PosInt 10 BigEndian>").expect(""),
+ m: DummyMorphism(MorphismType {
+ src_type: dict.parse("<Seq <Digit Radix> ~ Char>").unwrap(),
+ dst_type: dict.parse("<Seq <Digit Radix> ~ ℤ_2^64 ~ machine.UInt64>").unwrap()
+ }),
+ }
+ ]
+ ));
+}
+
+
+#[test]
+fn test_morphism_path3() {
+ let (mut dict, mut base) = morphism_test_setup();
+
+ let path = base.find_morphism_path(MorphismType {
+ src_type: dict.parse("ℕ ~ <PosInt 10 LittleEndian> ~ <Seq <Digit 10> ~ Char>").unwrap(),
+ dst_type: dict.parse("ℕ ~ <PosInt 16 LittleEndian> ~ <Seq <Digit 16> ~ ℤ_2^64 ~ machine.UInt64>").unwrap(),
+ });
+
+ fn print_subst(m: &std::collections::HashMap<TypeID, TypeTerm>, dict: &mut impl TypeDict) {
+ eprintln!("{{");
+
+ for (k,v) in m.iter() {
+ eprintln!(" {} --> {}",
+ dict.get_typename(k).unwrap(),
+ dict.unparse(v)
+ );
+ }
+
+ eprintln!("}}");
+ }
+
+ if let Some(path) = path.as_ref() {
+ for n in path.iter() {
+ eprintln!("
+ψ = {}
+morph {}
+ --> {}
+with
+ ",
+ n.halo.clone().sugar(&mut dict).pretty(&mut dict, 0),
+ n.m.get_type().src_type.sugar(&mut dict).pretty(&mut dict, 0),
+ n.m.get_type().dst_type.sugar(&mut dict).pretty(&mut dict, 0),
+ );
+ print_subst(&n.σ, &mut dict)
+ }
+ }
+
+ assert_eq!(
+ path,
+ Some(
+ vec![
+ MorphismInstance {
+ σ: vec![
+ (dict.get_typeid(&"Radix".into()).unwrap(), TypeTerm::Num(10)),
+ ].into_iter().collect(),
+ halo: dict.parse("ℕ ~ <PosInt 10 LittleEndian>").expect(""),
+ m: DummyMorphism(MorphismType {
+ src_type: dict.parse("<Seq <Digit Radix> ~ Char>").unwrap(),
+ dst_type: dict.parse("<Seq <Digit Radix> ~ ℤ_2^64 ~ machine.UInt64>").unwrap()
+ }),
+ },
+
+ MorphismInstance {
+ σ: vec![
+ (dict.get_typeid(&"SrcRadix".into()).unwrap(), TypeTerm::Num(10)),
+ (dict.get_typeid(&"DstRadix".into()).unwrap(), TypeTerm::Num(16)),
+ ].into_iter().collect(),
+ halo: TypeTerm::unit(),
+ m: DummyMorphism(MorphismType {
+ src_type: dict.parse("ℕ ~ <PosInt SrcRadix LittleEndian> ~ <Seq <Digit SrcRadix> ~ ℤ_2^64 ~ machine.UInt64>").unwrap(),
+ dst_type: dict.parse("ℕ ~ <PosInt DstRadix LittleEndian> ~ <Seq <Digit DstRadix> ~ ℤ_2^64 ~ machine.UInt64>").unwrap()
+ }),
+ }
+ ]
+ ));
+}
+
+
+
+#[test]
+fn test_morphism_path4() {
+ let (mut dict, mut base) = morphism_test_setup();
+
+ let path = base.find_morphism_path(MorphismType {
+ src_type: dict.parse("ℕ ~ <PosInt 10 LittleEndian> ~ <Seq <Digit 10> ~ Char>").unwrap(),
+ dst_type: dict.parse("ℕ ~ <PosInt 16 LittleEndian> ~ <Seq <Digit 16> ~ Char>").unwrap()
+ });
+
+ fn print_subst(m: &std::collections::HashMap<TypeID, TypeTerm>, dict: &mut impl TypeDict) {
+ eprintln!("{{");
+
+ for (k,v) in m.iter() {
+ eprintln!(" {} --> {}",
+ dict.get_typename(k).unwrap(),
+ dict.unparse(v)
+ );
+ }
+
+ eprintln!("}}");
+ }
+
+ if let Some(path) = path.as_ref() {
+ for n in path.iter() {
+ eprintln!("
+ψ = {}
+morph {}
+ --> {}
+with
+ ",
+ n.halo.clone().sugar(&mut dict).pretty(&mut dict, 0),
+ n.m.get_type().src_type.sugar(&mut dict).pretty(&mut dict, 0),
+ n.m.get_type().dst_type.sugar(&mut dict).pretty(&mut dict, 0),
+ );
+ print_subst(&n.σ, &mut dict)
+ }
+ }
+
+ assert_eq!(
+ path,
+ Some(
+ vec![
+ MorphismInstance {
+ σ: vec![
+ (dict.get_typeid(&"Radix".into()).unwrap(), TypeTerm::Num(10)),
+ ].into_iter().collect(),
+ halo: dict.parse("ℕ ~ <PosInt 10 LittleEndian>").expect(""),
+ m: DummyMorphism(MorphismType {
+ src_type: dict.parse("<Seq <Digit Radix> ~ Char>").unwrap(),
+ dst_type: dict.parse("<Seq <Digit Radix> ~ ℤ_2^64 ~ machine.UInt64>").unwrap()
+ }),
+ },
+
+ MorphismInstance {
+ σ: vec![
+ (dict.get_typeid(&"SrcRadix".into()).unwrap(), TypeTerm::Num(10)),
+ (dict.get_typeid(&"DstRadix".into()).unwrap(), TypeTerm::Num(16)),
+ ].into_iter().collect(),
+ halo: TypeTerm::unit(),
+ m: DummyMorphism(MorphismType {
+ src_type: dict.parse("ℕ ~ <PosInt SrcRadix LittleEndian> ~ <Seq <Digit SrcRadix> ~ ℤ_2^64 ~ machine.UInt64>").unwrap(),
+ dst_type: dict.parse("ℕ ~ <PosInt DstRadix LittleEndian> ~ <Seq <Digit DstRadix> ~ ℤ_2^64 ~ machine.UInt64>").unwrap()
+ }),
+ },
+
+ MorphismInstance {
+ σ: vec![
+ (dict.get_typeid(&"Radix".into()).unwrap(), TypeTerm::Num(16)),
+ ].into_iter().collect(),
+ halo: dict.parse("ℕ ~ <PosInt 16 LittleEndian>").expect(""),
+ m: DummyMorphism(MorphismType {
+ src_type: dict.parse("<Seq <Digit Radix> ~ ℤ_2^64 ~ machine.UInt64>").unwrap(),
+ dst_type: dict.parse("<Seq <Digit Radix> ~ Char>").unwrap()
+ }),
+ },
+
+ ]
+ ));
+}
+
+
+
+
+#[test]
+fn test_morphism_path_posint() {
let (mut dict, mut base) = morphism_test_setup();
let path = base.find_morphism_path(MorphismType {
@@ -114,8 +323,6 @@ with
MorphismInstance {
σ: vec![
(dict.get_typeid(&"Radix".into()).unwrap(), TypeTerm::Num(10)),
- (dict.get_typeid(&"SrcRadix".into()).unwrap(), TypeTerm::Num(10)),
- (dict.get_typeid(&"DstRadix".into()).unwrap(), TypeTerm::Num(16))
].into_iter().collect(),
halo: dict.parse("ℕ ~ <PosInt 10 BigEndian>").unwrap(),
m: DummyMorphism(MorphismType {
@@ -126,8 +333,6 @@ with
MorphismInstance {
σ: vec![
(dict.get_typeid(&"Radix".into()).unwrap(), TypeTerm::Num(10)),
- (dict.get_typeid(&"SrcRadix".into()).unwrap(), TypeTerm::Num(10)),
- (dict.get_typeid(&"DstRadix".into()).unwrap(), TypeTerm::Num(16))
].into_iter().collect(),
halo: TypeTerm::unit(),
m: DummyMorphism(MorphismType{
@@ -139,7 +344,6 @@ with
σ: vec![
(dict.get_typeid(&"SrcRadix".into()).unwrap(), TypeTerm::Num(10)),
(dict.get_typeid(&"DstRadix".into()).unwrap(), TypeTerm::Num(16)),
- (dict.get_typeid(&"Radix".into()).unwrap(), TypeTerm::Num(16)),
].into_iter().collect(),
halo: TypeTerm::unit(),
m: DummyMorphism(MorphismType{
@@ -150,7 +354,6 @@ with
MorphismInstance {
σ: vec![
(dict.get_typeid(&"Radix".into()).unwrap(), TypeTerm::Num(16)),
- (dict.get_typeid(&"DstRadix".into()).unwrap(), TypeTerm::Num(16))
].into_iter().collect(),
halo: TypeTerm::unit(),
m: DummyMorphism(MorphismType{
@@ -162,7 +365,7 @@ with
σ: vec![
(dict.get_typeid(&"Radix".into()).unwrap(), TypeTerm::Num(16))
].into_iter().collect(),
- halo: dict.parse("ℕ ~ <PosInt Radix BigEndian>").unwrap(),
+ halo: dict.parse("ℕ ~ <PosInt 16 BigEndian>").unwrap(),
m: DummyMorphism(MorphismType{
src_type: dict.parse("<Seq <Digit Radix> ~ ℤ_2^64 ~ machine.UInt64>").unwrap(),
dst_type: dict.parse("<Seq <Digit Radix> ~ Char>").unwrap()
diff --git a/src/unification.rs b/src/unification.rs
index 03c3699..ef8c0fd 100644
--- a/src/unification.rs
+++ b/src/unification.rs
@@ -149,15 +149,58 @@ impl UnificationProblem {
Variables
*/
+ (t, TypeTerm::TypeID(TypeID::Var(varid))) => {
+// eprintln!("t <= variable");
+ if ! t.contains_var( varid ) {
+ // let x = self.σ.get(&TypeID::Var(varid)).cloned();
+ if let Some(lower_bound) = self.lower_bounds.get(&varid).cloned() {
+// eprintln!("var already exists. check max. type");
+ if let Ok(halo) = self.eval_subtype(
+ UnificationPair {
+ lhs: lower_bound.clone(),
+ rhs: t.clone(),
+ halo: TypeTerm::unit(),
+ addr: vec![]
+ }
+ ) {
+// eprintln!("found more general lower bound");
+// eprintln!("set var {}'s lowerbound to {:?}", varid, t.clone());
+ // generalize variable type to supertype
+ self.lower_bounds.insert(varid, t.clone());
+ } else if let Ok(halo) = self.eval_subtype(
+ UnificationPair{
+ lhs: t.clone(),
+ rhs: lower_bound.clone(),
+ halo: TypeTerm::unit(),
+ addr: vec![]
+ }
+ ) {
+// eprintln!("OK, is already larger type");
+ } else {
+// eprintln!("violated subtype restriction");
+ return Err(UnificationError{ addr: unification_pair.addr, t1: TypeTerm::TypeID(TypeID::Var(varid)), t2: t });
+ }
+ } else {
+// eprintln!("set var {}'s lowerbound to {:?}", varid, t.clone());
+ self.lower_bounds.insert(varid, t.clone());
+ }
+ self.reapply_subst();
+ Ok(TypeTerm::unit())
+ } else if t == TypeTerm::TypeID(TypeID::Var(varid)) {
+ Ok(TypeTerm::unit())
+ } else {
+ Err(UnificationError{ addr: unification_pair.addr, t1: TypeTerm::TypeID(TypeID::Var(varid)), t2: t })
+ }
+ }
+
(TypeTerm::TypeID(TypeID::Var(varid)), t) => {
- eprintln!("variable <= t");
+// eprintln!("variable <= t");
if let Some(upper_bound) = self.upper_bounds.get(&varid).cloned() {
if let Ok(_halo) = self.eval_subtype(
UnificationPair {
lhs: t.clone(),
rhs: upper_bound,
-
halo: TypeTerm::unit(),
addr: vec![]
}
@@ -171,49 +214,6 @@ impl UnificationProblem {
Ok(TypeTerm::unit())
}
- (t, TypeTerm::TypeID(TypeID::Var(varid))) => {
- eprintln!("t <= variable");
- if ! t.contains_var( varid ) {
- // let x = self.σ.get(&TypeID::Var(varid)).cloned();
- if let Some(lower_bound) = self.lower_bounds.get(&varid).cloned() {
- eprintln!("var already exists. check max. type");
- if let Ok(halo) = self.eval_subtype(
- UnificationPair {
- lhs: lower_bound.clone(),
- rhs: t.clone(),
- halo: TypeTerm::unit(),
- addr: vec![]
- }
- ) {
- eprintln!("found more general lower bound");
- eprintln!("set var {}'s lowerbound to {:?}", varid, t.clone());
- // generalize variable type to supertype
- self.lower_bounds.insert(varid, t.clone());
- } else if let Ok(halo) = self.eval_subtype(
- UnificationPair{
- lhs: t.clone(),
- rhs: lower_bound.clone(),
- halo: TypeTerm::unit(),
- addr: vec![]
- }
- ) {
- eprintln!("OK, is already larger type");
- } else {
- eprintln!("violated subtype restriction");
- return Err(UnificationError{ addr: unification_pair.addr, t1: TypeTerm::TypeID(TypeID::Var(varid)), t2: t });
- }
- } else {
- eprintln!("set var {}'s lowerbound to {:?}", varid, t.clone());
- self.lower_bounds.insert(varid, t.clone());
- }
- self.reapply_subst();
- Ok(TypeTerm::unit())
- } else if t == TypeTerm::TypeID(TypeID::Var(varid)) {
- Ok(TypeTerm::unit())
- } else {
- Err(UnificationError{ addr: unification_pair.addr, t1: TypeTerm::TypeID(TypeID::Var(varid)), t2: t })
- }
- }
/*
@@ -247,7 +247,7 @@ impl UnificationProblem {
halo: TypeTerm::unit(),
addr: new_addr
}) {
- eprintln!("unified ladders at {}, r_halo = {:?}", i, r_halo);
+// eprintln!("unified ladders at {}, r_halo = {:?}", i, r_halo);
for j in 0..a2.len() {
if i+j < a1.len() {
@@ -320,7 +320,6 @@ impl UnificationProblem {
*/
(TypeTerm::App(a1), TypeTerm::App(a2)) => {
- eprintln!("sub unify {:?}, {:?}", a1, a2);
if a1.len() == a2.len() {
let mut halo_args = Vec::new();
let mut n_halos_required = 0;
@@ -331,11 +330,10 @@ impl UnificationProblem {
x = x.strip();
- eprintln!("before strip: {:?}", y);
+// eprintln!("before strip: {:?}", y);
y = y.strip();
- eprintln!("after strip: {:?}", y);
-
- eprintln!("APP<> eval {:?} \n ?<=? {:?} ", x, y);
+// eprintln!("after strip: {:?}", y);
+// eprintln!("APP<> eval {:?} \n ?<=? {:?} ", x, y);
if let Ok(halo) = self.eval_subtype(
UnificationPair {
@@ -351,9 +349,9 @@ impl UnificationProblem {
y = y.strip();
let mut top = y.get_lnf_vec().first().unwrap().clone();
halo_args.push(top.clone());
- eprintln!("add top {:?}", top);
+// eprintln!("add top {:?}", top);
} else {
- eprintln!("add halo {:?}", halo);
+// eprintln!("add halo {:?}", halo);
if n_halos_required > 0 {
let x = &mut halo_args[n_halos_required-1];
if let TypeTerm::Ladder(argrs) = x {
@@ -380,7 +378,7 @@ impl UnificationProblem {
}
if n_halos_required > 0 {
- eprintln!("halo args : {:?}", halo_args);
+// eprintln!("halo args : {:?}", halo_args);
Ok(TypeTerm::App(halo_args))
} else {
Ok(TypeTerm::unit())
@@ -404,7 +402,7 @@ impl UnificationProblem {
}
// solve subtypes
- eprintln!("------ SOLVE SUBTYPES ---- ");
+// eprintln!("------ SOLVE SUBTYPES ---- ");
for mut subtype_pair in self.subtype_pairs.clone().into_iter() {
subtype_pair.lhs.apply_substitution(&|v| self.σ.get(v).cloned());
subtype_pair.rhs.apply_substitution(&|v| self.σ.get(v).cloned());
@@ -413,18 +411,18 @@ impl UnificationProblem {
// add variables from subtype bounds
for (var_id, t) in self.upper_bounds.iter() {
- eprintln!("VAR {} upper bound {:?}", var_id, t);
+// eprintln!("VAR {} upper bound {:?}", var_id, t);
self.σ.insert(TypeID::Var(*var_id), t.clone().strip());
}
for (var_id, t) in self.lower_bounds.iter() {
- eprintln!("VAR {} lower bound {:?}", var_id, t);
+// eprintln!("VAR {} lower bound {:?}", var_id, t);
self.σ.insert(TypeID::Var(*var_id), t.clone().strip());
}
self.reapply_subst();
- eprintln!("------ MAKE HALOS -----");
+// eprintln!("------ MAKE HALOS -----");
let mut halo_types = Vec::new();
for mut subtype_pair in self.subtype_pairs.clone().into_iter() {
subtype_pair.lhs = subtype_pair.lhs.apply_substitution(&|v| self.σ.get(v).cloned()).clone().strip();