lsts/
typ.rs

1
2use std::collections::HashMap;
3use crate::constant::Constant;
4use crate::kind::Kind;
5use crate::tlc::TLC;
6
7#[derive(Clone,Eq,PartialEq,Ord,PartialOrd,Hash,Copy)]
8pub enum InArrow {
9   No,
10   Lhs,
11   Rhs
12}
13
14///Each Term has at least one Type.
15///
16///Types are composed of Atomic parts like Nameds.
17///An Named type has a name and possibly some parameters.
18///Atomic parts can be combined to form Compound parts like Arrows.
19///Compound parts are formed by some combination of Arrows, Tuples, Products, and Ratios.
20///At the Highest level a Compound type can be pluralized with an And to join it to other Compounds.
21///
22///And types are represented in Conjunctive-Normal-Form which requires the Ands to only occupy the
23///highest level of a type. Some basic typing algorithms may not work correctly if a type is not in
24///Conjunctive-Normal-Form.
25///
26///Subtyping is implemented with And types. An implication, A + A => B, may be rewritten as just A + B.
27#[derive(Clone,Eq,PartialEq,Ord,PartialOrd,Hash)]
28pub enum Type {
29   Any,
30   MaybeZero(Box<Type>),
31   Named(String,Vec<Type>),
32   And(Vec<Type>), //Bottom is the empty conjunctive
33   Arrow(Box<Type>,Box<Type>),
34   Tuple(Vec<Type>),   //Tuple is order-sensitive, Nil is the empty tuple
35   HTuple(Box<Type>,Constant),
36   Product(Vec<Type>), //Product is order-insensitive
37   Ratio(Box<Type>,Box<Type>),
38   Constant(Constant),
39}
40
41impl Type {
42   pub fn datatype(&self) -> String {
43      let dts = vec!["U8","U64","I64","F32","F64","Unit","String"];
44      match self {
45         Type::Tuple(_) => "Tuple".to_string(),
46         Type::HTuple(_,_) => "Tuple".to_string(),
47         Type::Named(base,pars) if pars.len()==0 &&
48                                   dts.contains(&base.as_str()) => {
49            base.clone()
50         },
51         Type::And(ts) => {
52            for t in ts.iter() {
53            if let Type::Tuple(_) = t { return "Tuple".to_string();
54            } else if let Type::HTuple(_,_) = t { return "Tuple".to_string();
55            } else if let Type::Named(base,pars) = t {
56            if pars.len()==0 && dts.contains(&base.as_str()) {
57               return base.clone();
58            }}}
59            unimplemented!("Type::datatype({:?})", self)
60         },
61         _ => unimplemented!("Type::datatype({:?})", self)
62      }
63   }
64   pub fn project_ratio(&self) -> (Vec<Type>,Vec<Type>) {
65       match self {
66         Type::Ratio(p,b) => {
67            let (mut pn,mut pd) = p.project_ratio();
68            let (mut bn,mut bd) = b.project_ratio();
69            pn.append(&mut bd);
70            pd.append(&mut bn);
71            (pn, pd)
72         },
73         Type::Product(ts) => {
74            let mut tn = Vec::new();
75            let mut td = Vec::new();
76            for tc in ts.iter() {
77               let (mut tcn,mut tcd) = tc.project_ratio();
78               tn.append(&mut tcn);
79               td.append(&mut tcd);
80            }
81            (tn, td)
82         },
83         tt => (vec![tt.clone()], Vec::new())
84      }
85   }
86   pub fn is_ctuple(&self) -> bool {
87      if let Type::Tuple(cts) = self {
88         for ct in cts.iter() {
89         if !ct.is_constant() { 
90            return false;
91         }}
92         return true;
93      }
94      false
95   }
96   pub fn is_open(&self) -> bool {
97      match self {
98         Type::Any => true,
99         Type::MaybeZero(_tt) => true,
100         Type::Named(tn,ts) => tn.chars().all(char::is_uppercase) || ts.iter().any(|tt| tt.is_open()),
101         Type::Arrow(p,b) => p.is_open() || b.is_open(),
102         Type::Ratio(p,b) => p.is_open() || b.is_open(),
103         Type::And(ts) => ts.iter().any(|tt| tt.is_open()),
104         Type::Tuple(ts) => ts.iter().any(|tt| tt.is_open()),
105         Type::Product(ts) => ts.iter().any(|tt| tt.is_open()),
106         Type::HTuple(bt,_ct) => bt.is_open(),
107         Type::Constant(_cv) => false,
108      }
109   }
110   pub fn is_constant(&self) -> bool {
111      match self {
112         Type::Constant(_) => true,
113         _ => false,
114      }
115   }
116   pub fn all_named(&self) -> Vec<Type> {
117      match self {
118         Type::Named(_,_) => { vec![self.clone()] },
119         Type::And(ts) => {
120            let mut acc = Vec::new();
121            for ct in ts.iter() {
122               acc.extend(ct.all_named());
123            }
124            acc
125         },
126         _ => { Vec::new() },
127      }
128   }
129   pub fn and(&self, other:&Type) -> Type {
130      match (self,other) {
131         (Type::Any,r) => r.clone(),
132         (l,Type::Any) => l.clone(),
133         (Type::Named(lv,_lps),rt) if lv.chars().all(char::is_uppercase) => rt.clone(),
134         (lt,Type::Named(rv,_rps)) if rv.chars().all(char::is_uppercase) => lt.clone(),
135         (Type::And(ls),Type::And(rs)) => {
136            let mut ts = ls.clone();
137            ts.append(&mut rs.clone());
138            ts.sort(); ts.dedup();
139            Type::And(ts)
140         },
141         (Type::And(ls),r) => {
142            let mut ts = ls.clone();
143            ts.push(r.clone());
144            ts.sort(); ts.dedup();
145            Type::And(ts)
146         }
147         (l,Type::And(rs)) => {
148            let mut ts = rs.clone();
149            ts.push(l.clone());
150            ts.sort(); ts.dedup();
151            Type::And(ts)
152         },
153         (l,r) => {
154            Type::And(vec![l.clone(),r.clone()])
155         }
156      }
157   }
158   pub fn is_var(&self) -> bool {
159      match self {
160         Type::Named(tn,ts) => ts.len()==0 && tn.chars().all(char::is_uppercase),
161         _ => false
162      }
163   }
164   pub fn domain(&self) -> Type {
165      match self {
166         Type::Arrow(p,_b) => *p.clone(),
167         Type::And(ts) => {
168            let mut cts = Vec::new();
169            for ct in ts.iter() {
170               match ct.domain() {
171                  Type::And(mut cta) => {
172                     cts.append(&mut cta);
173                  }, ctr => {
174                     cts.push(ctr);
175                  }
176               }
177            }
178            if cts.len()==1 { cts[0].clone() }
179            else { Type::And(cts) }
180         },
181         _ => Type::And(Vec::new()), //absurd
182      }
183   }
184   pub fn range(&self) -> Type {
185      match self {
186         Type::Arrow(_p,b) => *b.clone(),
187         Type::And(ts) => {
188            let mut cts = Vec::new();
189            for ct in ts.iter() {
190               match ct.range() {
191                  Type::And(mut cta) => {
192                     cts.append(&mut cta);
193                  }, ctr => {
194                     cts.push(ctr);
195                  }
196               }
197            }
198            if cts.len()==1 { cts[0].clone() }
199            else { Type::And(cts) }
200         },
201         _ => Type::And(Vec::new()), //absurd
202      }
203   }
204   pub fn vars(&self) -> Vec<String> {
205      match self {
206         Type::Any => vec![],
207         Type::MaybeZero(tt) => { tt.vars() },
208         Type::Named(tn,ts) => {
209            let mut nv = vec![tn.clone()];
210            for tt in ts.iter() {
211               nv.append(&mut tt.vars());
212            }
213            nv
214         },
215         Type::Arrow(p,b) => { let mut pv=p.vars(); pv.append(&mut b.vars()); pv },
216         Type::Ratio(p,b) => { let mut pv=p.vars(); pv.append(&mut b.vars()); pv },
217         Type::And(ts) => {
218            let mut nv = Vec::new();
219            for tt in ts.iter() {
220               nv.append(&mut tt.vars());
221            }
222            nv
223         },
224         Type::Tuple(ts) => {
225            let mut nv = Vec::new();
226            for tt in ts.iter() {
227               nv.append(&mut tt.vars());
228            }
229            nv
230         },
231         Type::HTuple(bt,_ct) => { bt.vars() },
232         Type::Product(ts) => {
233            let mut nv = Vec::new();
234            for tt in ts.iter() {
235               nv.append(&mut tt.vars());
236            }
237            nv
238         },
239         Type::Constant(_) => vec![]
240      }
241   }
242   pub fn simplify_ratio(&self) -> Type {
243      //assume Typee has already been normalized
244      let (mut num, den) = self.project_ratio();
245      let mut rden = Vec::new();
246      for d in den.into_iter() {
247         if let Some(ni) = num.iter().position(|n|n==&d) {
248            num.remove(ni);
249         } else {
250            rden.push(d);
251         }
252      }
253      let n = if num.len()==0 {
254         Type::Tuple(Vec::new())
255      } else if num.len()==1 {
256         num[0].clone()
257      } else {
258         Type::Product(num)
259      };
260      let tt = if rden.len()==0 {
261         n
262      } else if rden.len()==1 {
263         Type::Ratio(Box::new(n),Box::new(rden[0].clone()))
264      } else {
265         let d = Type::Product(rden);
266         Type::Ratio(Box::new(n),Box::new(d))
267      };
268      tt
269   }
270   pub fn normalize(&self) -> Type {
271      match self {
272         Type::And(ts) => {
273            let mut cnf = Vec::new();
274            for ct in ts.iter() {
275               let ct = ct.normalize();
276               match ct {
277                  Type::And(mut cts) => { cnf.append(&mut cts); },
278                  _ => { cnf.push(ct); }
279               }
280            }
281            cnf.sort(); cnf.dedup();
282            if cnf.len()==1 {
283               cnf[0].clone()
284            } else {
285               Type::And(cnf)
286            }
287         },
288         Type::Product(ts) => {
289            let mut ts = ts.iter().map(|tt|tt.normalize()).collect::<Vec<Type>>();
290            ts.sort();
291            Type::Product(ts).simplify_ratio()
292         },
293         Type::Tuple(ts) => {
294            let ts = ts.iter().map(|tt|tt.normalize()).collect::<Vec<Type>>();
295            Type::Tuple(ts)
296         },
297         Type::Named(tn,ts) => {
298            let ts = ts.iter().map(|tt|tt.normalize()).collect::<Vec<Type>>();
299            Type::Named(tn.clone(),ts)
300         },
301         Type::Arrow(p,b) => {
302            Type::Arrow(Box::new(p.normalize()), Box::new(b.normalize()))
303         },
304         Type::Ratio(_p,_b) => self.simplify_ratio(),
305         tt => tt.clone(),
306      }
307   }
308   pub fn remove(&self, x:&Type) -> Type {
309      if self == x { return Type::And(Vec::new()); }
310      match self {
311         Type::Any => Type::Any,
312         Type::MaybeZero(tt) => Type::MaybeZero(Box::new(tt.remove(x))),
313         Type::Arrow(p,b) => Type::Arrow(Box::new(p.remove(x)),Box::new(b.remove(x))),
314         Type::Ratio(p,b) => Type::Ratio(Box::new(p.remove(x)),Box::new(b.remove(x))),
315         Type::Named(tn,ts) => Type::Named(tn.clone(),ts.iter().map(|t| t.remove(x)).collect::<Vec<Type>>()),
316         Type::And(ts) => Type::And(ts.iter().map(|t| t.remove(x)).collect::<Vec<Type>>()),
317         Type::Tuple(ts) => Type::Tuple(ts.iter().map(|t| t.remove(x)).collect::<Vec<Type>>()),
318         Type::HTuple(bt,ct) => Type::HTuple(Box::new(bt.remove(x)),ct.clone()),
319         Type::Product(ts) => Type::Product(ts.iter().map(|t| t.remove(x)).collect::<Vec<Type>>()),
320         Type::Constant(cv) => Type::Constant(cv.clone())
321      }.normalize()
322   }
323   pub fn substitute(&self, subs:&HashMap<Type,Type>) -> Type {
324      if let Some(st) = subs.get(self) {
325         return st.clone();
326      }
327      match self {
328         Type::Any => Type::Any,
329         Type::MaybeZero(tt) => Type::MaybeZero(Box::new(tt.substitute(subs))),
330         Type::Arrow(p,b) => Type::Arrow(Box::new(p.substitute(subs)),Box::new(b.substitute(subs))),
331         Type::Ratio(p,b) => Type::Ratio(Box::new(p.substitute(subs)),Box::new(b.substitute(subs))),
332         Type::Named(tn,ts) => Type::Named(tn.clone(),ts.iter().map(|t| t.substitute(subs)).collect::<Vec<Type>>()),
333         Type::And(ts) => Type::And(ts.iter().map(|t| t.substitute(subs)).collect::<Vec<Type>>()),
334         Type::Tuple(ts) => Type::Tuple(ts.iter().map(|t| t.substitute(subs)).collect::<Vec<Type>>()),
335         Type::HTuple(bt,ct) => Type::HTuple(Box::new(bt.substitute(subs)),ct.clone()),
336         Type::Product(ts) => Type::Product(ts.iter().map(|t| t.substitute(subs)).collect::<Vec<Type>>()),
337         Type::Constant(cv) => Type::Constant(cv.clone())
338      }
339   }
340   pub fn is_concrete(&self) -> bool {
341      match self {
342         Type::Any => false,
343         Type::MaybeZero(_tt) => false,
344         Type::Arrow(p,b) => p.is_concrete() && b.is_concrete(),
345         Type::Ratio(p,b) => p.is_concrete() && b.is_concrete(),
346         Type::Named(_tn,ts) => ts.iter().all(|tc| tc.is_concrete()),
347         Type::And(ts) => ts.iter().all(|tc| tc.is_concrete()), //bottom Typee is also concrete
348         Type::Tuple(ts) => ts.iter().all(|tc| tc.is_concrete()),
349         Type::HTuple(bt,_ct) => bt.is_concrete(),
350         Type::Product(ts) => ts.iter().all(|tc| tc.is_concrete()),
351         Type::Constant(_) => true,
352      }
353   }
354   pub fn kind(&self, kinds: &HashMap<Type,Kind>) -> Kind {
355      if let Some(k) = kinds.get(&self) {
356         return k.clone();
357      }
358      match self {
359         Type::Constant(_) => Kind::Named("Constant".to_string(),Vec::new()),
360         Type::And(ats) => {
361            let mut aks = Vec::new();
362            for at in ats.iter() {
363              aks.push(at.kind(kinds));
364            }
365            Kind::and(aks)
366         },
367         _ => Kind::Nil,
368      }
369   }
370   pub fn narrow(&self, kinds: &HashMap<Type,Kind>, k: &Kind) -> Type {
371      if !self.kind(kinds).has(k) { return Type::And(Vec::new()); } //nothing here to take
372      let tt = match self {
373         Type::And(ts) => {
374            let mut tcs = Vec::new();
375            for tc in ts.iter() {
376               match tc.narrow(kinds,k) {
377                  Type::And(acs) => {
378                     tcs.append(&mut acs.clone());
379                  }, ac => {
380                     tcs.push(ac.clone());
381                  }
382               }
383            }
384            if tcs.len()==1 { tcs[0].clone() }
385            else { Type::And(tcs) }
386         }
387         tt => tt.clone(),
388      };
389      tt
390   }
391   pub fn is_bottom(&self) -> bool {
392      match self {
393         Type::And(ts) if ts.len()==0 => { true },
394         _ => false
395      }
396   }
397   pub fn compile_subs(subs: &Vec<(Type,Type)>) -> Result<HashMap<Type,Type>,()> {
398      let mut msubs: HashMap<Type,Type> = HashMap::new();
399      for (lt,mut rt) in subs.clone().into_iter() {
400         if let Some(vt) = msubs.get(&lt) {
401            rt = vt.most_general_unifier(&rt);
402            if rt.is_bottom() { return Err(()); }
403         }
404         msubs.insert(lt, rt);
405      }
406      Ok(msubs)
407   }
408   pub fn implies(tlc: &TLC, lt: &Type, rt: &Type) -> Type {
409      let mut subs = Vec::new();
410      Type::subs_implies(tlc, &mut subs, lt, rt)
411   }
412   pub fn arrow_implies(tlc: &TLC, lt: &mut Type, rt: &mut Type, inarrow: InArrow) -> Type {
413      let mut subs = Vec::new();
414      *lt = tlc.extend_implied(lt);
415      *lt = lt.normalize();
416      *rt = tlc.extend_implied(rt);
417      *rt = rt.normalize();
418      lt.__implication_unifier(&rt, &mut subs, inarrow).normalize()
419   }
420   pub fn subs_implies(tlc: &TLC, subs: &mut Vec<(Type,Type)>, lt: &Type, rt: &Type) -> Type {
421      let lt = tlc.extend_implied(lt).normalize();
422      let rt = tlc.extend_implied(rt).normalize();
423      lt.subs_implication_unifier(subs, &rt).normalize()
424   }
425   pub fn nored_implies(tlc: &TLC, subs: &mut Vec<(Type,Type)>, lt: &Type, rt: &Type) -> Type {
426      let lt = tlc.extend_implied(lt).normalize();
427      let rt = tlc.extend_implied(rt).normalize();
428      lt.subs_implication_unifier(subs, &rt).normalize()
429   }
430   pub fn implication_unifier(&self, other: &Type) -> Type {
431      let mut subs = Vec::new();
432      self.subs_implication_unifier(&mut subs, other)
433   }
434   pub fn subs_implication_unifier(&self, subs: &mut Vec<(Type,Type)>, other: &Type) -> Type {
435      let nt = self._implication_unifier(other, subs);
436      if let Ok(msubs) = Type::compile_subs(subs) {
437         nt.substitute(&msubs).normalize()
438      } else {
439         Type::And(vec![])
440      }
441   }
442   fn _implication_unifier(&self, other: &Type, subs: &mut Vec<(Type,Type)>) -> Type {
443      self.__implication_unifier(other, subs, InArrow::No)
444   }
445   fn __implication_unifier(&self, other: &Type, subs: &mut Vec<(Type,Type)>, inarrow: InArrow) -> Type {
446      //if the two types don't unify
447      //then the mgu will be the bottom type
448      let tt = match (self,other) {
449         //wildcard failure
450         (Type::And(lts),_) if lts.len()==0 => { Type::And(vec![]) },
451         (_,Type::And(rts)) if rts.len()==0 => { Type::And(vec![]) },
452
453         //wildcard match
454         (lt,Type::Any) if inarrow != InArrow::Lhs => { lt.clone() },
455         (Type::Any,rt) if inarrow == InArrow::Lhs => { rt.clone() },
456         (Type::Named(lv,_lps),rt) if lv.chars().all(char::is_uppercase) => {
457            subs.push((self.clone(), rt.clone()));
458            self.clone()
459         },
460         (lt,Type::Named(rv,_rps)) if rv.chars().all(char::is_uppercase) => {
461            subs.push((other.clone(), lt.clone()));
462            other.clone()
463         },
464
465         //conjunctive normal form takes precedence
466         (Type::And(_lts),Type::And(rts)) => {
467            let mut mts = Vec::new();
468            for rt in rts.iter() {
469               match self.__implication_unifier(rt,subs,inarrow) {
470                  Type::And(tts) if tts.len()==0 => { return Type::And(vec![]); },
471                  Type::And(mut tts) => { mts.append(&mut tts); },
472                  tt => { mts.push(tt); },
473               }
474            }
475            mts.sort(); mts.dedup();
476            if mts.len()==1 { mts[0].clone() }
477            else { Type::And(mts) }
478         },
479         (Type::And(lts),rt) => {
480            let mut mts = Vec::new();
481            for ltt in lts.iter() {
482               match ltt.__implication_unifier(rt,subs,inarrow) {
483                  Type::And(mut tts) => { mts.append(&mut tts); },
484                  tt => { mts.push(tt); },
485               }
486            }
487            mts.sort(); mts.dedup();
488            if mts.len()==1 { mts[0].clone() }
489            else { Type::And(mts) }
490         },
491         (lt,Type::And(rts)) => {
492            let mut mts = Vec::new();
493            for rt in rts.iter() {
494               match lt.__implication_unifier(rt,subs,inarrow) {
495                  Type::And(tts) if tts.len()==0 => { return Type::And(vec![]); },
496                  Type::And(mut tts) => { mts.append(&mut tts); },
497                  tt => { mts.push(tt); },
498               }
499            }
500            mts.sort(); mts.dedup();
501            if mts.len()==1 { mts[0].clone() }
502            else { Type::And(mts) }
503         }
504
505         //ratio Typees have next precedence
506         (Type::Ratio(pl,bl),Type::Ratio(pr,br)) => {
507            let pt = pl.__implication_unifier(pr,subs,inarrow);
508            if pt.is_bottom() { return pt.clone(); }
509            let bt = bl.__implication_unifier(br,subs,inarrow);
510            if bt.is_bottom() { return bt.clone(); }
511            Type::Ratio(Box::new(pt),Box::new(bt))
512         },
513         (lt,Type::Ratio(pr,br)) => {
514            //assert Nil divisor on rhs
515            match **br {
516               Type::Tuple(ref bs) if bs.len()==0 => {
517                  lt.__implication_unifier(pr,subs,inarrow)
518               }, _ => { Type::And(vec![]) }
519            }
520         },
521         (Type::Ratio(pl,bl),rt) => {
522            //assert Nil divisor on rhs
523            match **bl {
524               Type::Tuple(ref bs) if bs.len()==0 => {
525                  pl.__implication_unifier(rt,subs,inarrow)
526               }, _ => { Type::And(vec![]) }
527            }
528         },
529
530         //everything else is a mixed bag
531         (Type::Named(lv,lps),Type::Named(rv,rps))
532         if lv==rv && lps.len()==rps.len() => {
533            let mut tps = Vec::new();
534            for (lp,rp) in std::iter::zip(lps,rps) {
535               let nt = lp.__implication_unifier(rp,subs,inarrow);
536               if nt.is_bottom() { return nt.clone(); }
537               tps.push(lp.__implication_unifier(rp,subs,inarrow));
538            }
539            Type::Named(lv.clone(),tps)
540         }
541         (Type::Arrow(pl,bl),Type::Arrow(pr,br)) => {
542            let pt = if **bl == Type::Any {
543               pl.__implication_unifier(pr,subs,InArrow::Rhs) //not contravariant
544            } else {
545               pr.__implication_unifier(pl,subs,InArrow::Lhs) //contravariant
546            };
547            if pt.is_bottom() { return pt.clone(); }
548            let bt = if **bl==Type::Any { (**br).clone() }
549            else { bl.__implication_unifier(br,subs,InArrow::Rhs) };
550            if bt.is_bottom() { return bt.clone(); }
551            Type::Arrow(Box::new(pt),Box::new(bt))
552         },
553         (Type::Product(la),Type::Product(ra)) if la.len()==ra.len() => {
554            let mut ts = Vec::new();
555            for (lt,rt) in std::iter::zip(la,ra) {
556               let nt = lt.__implication_unifier(rt,subs,inarrow);
557               if nt.is_bottom() { return nt.clone(); }
558               ts.push(nt.clone());
559            }
560            Type::Product(ts)
561         },
562         (Type::Tuple(la),Type::Tuple(ra)) if la.len()==ra.len() => {
563            let mut ts = Vec::new();
564            for (lt,rt) in std::iter::zip(la,ra) {
565               let nt = lt.__implication_unifier(rt,subs,inarrow);
566               if nt.is_bottom() { return nt.clone(); }
567               ts.push(nt.clone());
568            }
569            Type::Tuple(ts)
570         },
571         (Type::HTuple(lb,lc),Type::HTuple(rb,rc)) if lc==rc => {
572            let bt = lb.__implication_unifier(rb,subs,inarrow);
573            if bt.is_bottom() { return bt.clone(); }
574            Type::HTuple(Box::new(bt), lc.clone())
575         },
576         (Type::HTuple(lb,_lc),Type::HTuple(rb,Constant::Tuple(rc))) => {
577            let bt = lb.__implication_unifier(rb,subs,inarrow);
578            if bt.is_bottom() { return bt.clone(); }
579            Type::HTuple(Box::new(bt), Constant::Tuple(rc.clone()))
580         },
581         (Type::Tuple(lts),Type::HTuple(rb,Constant::Literal(rc))) => {
582            let rlen = str::parse::<usize>(&rc).unwrap();
583            if lts.len()!=rlen { return Type::And(vec![]); }
584            for lt in lts.iter() {
585               let nt = lt.__implication_unifier(rb,subs,inarrow);
586               if nt.is_bottom() { return nt.clone(); }
587            }
588            Type::HTuple(rb.clone(), Constant::Literal(rc.clone()))
589         },
590         (Type::Tuple(lts),Type::HTuple(rb,Constant::Tuple(rc))) => {
591            for lt in lts.iter() {
592               let nt = lt.__implication_unifier(rb,subs,inarrow);
593               if nt.is_bottom() { return nt.clone(); }
594            }
595            Type::HTuple(rb.clone(), Constant::Tuple(rc.clone()))
596         },
597	
598         (Type::Constant(lv),Type::Constant(rv)) if lv==rv => {
599            Type::Constant(lv.clone())
600         },
601         _ => Type::And(vec![]),
602      };
603      tt
604   }
605   pub fn most_general_unifier(&self, other: &Type) -> Type {
606      //if the two types don't unify
607      //then the mgu will be the bottom type
608      match (self,other) {
609         //wildcard failure
610         (Type::And(lts),_) if lts.len()==0 => { Type::And(vec![]) },
611         (_,Type::And(rts)) if rts.len()==0 => { Type::And(vec![]) },
612
613         //wildcard match
614         (Type::Any,Type::Any) => { self.clone() },
615         (lt,Type::Any) => { lt.clone() },
616         (Type::Any,rt) => { rt.clone() },
617         (Type::Named(lv,_lps),Type::Named(rv,_rps)) if lv.chars().all(char::is_uppercase) && lv==rv => {
618            self.clone()
619         },
620
621         (Type::MaybeZero(_lt),_) => { Type::And(vec![]) },
622         (_,Type::MaybeZero(_rt)) => { Type::And(vec![]) },
623
624         //conjunctive normal form takes precedence
625         (Type::And(_lts),Type::And(rts)) => {
626            let mut mts = Vec::new();
627            for rt in rts.iter() {
628               match self.most_general_unifier(rt) {
629                  Type::And(mut tts) => { mts.append(&mut tts); },
630                  tt => { mts.push(tt); },
631               }
632            }
633            mts.sort(); mts.dedup();
634            if mts.len()==1 { mts[0].clone() }
635            else { Type::And(mts) }
636         },
637         (Type::And(lts),rt) => {
638            let mut mts = Vec::new();
639            for ltt in lts.iter() {
640               match ltt.most_general_unifier(rt) {
641                  Type::And(mut tts) => { mts.append(&mut tts); },
642                  tt => { mts.push(tt); },
643               }
644            }
645            mts.sort(); mts.dedup();
646            if mts.len()==1 { mts[0].clone() }
647            else { Type::And(mts) }
648         },
649         (lt,Type::And(rts)) => {
650            let mut mts = Vec::new();
651            for rt in rts.iter() {
652               match lt.most_general_unifier(rt) {
653                  Type::And(mut tts) => { mts.append(&mut tts); },
654                  tt => { mts.push(tt); },
655               }
656            }
657            mts.sort(); mts.dedup();
658            if mts.len()==1 { mts[0].clone() }
659            else { Type::And(mts) }
660         }
661
662         //ratio Typees have next precedence
663         (Type::Ratio(pl,bl),Type::Ratio(pr,br)) => {
664            let pt = pl.most_general_unifier(pr);
665            if pt.is_bottom() { return pt.clone(); }
666            let bt = bl.most_general_unifier(br);
667            if bt.is_bottom() { return bt.clone(); }
668            Type::Ratio(Box::new(pt),Box::new(bt))
669         },
670         (lt,Type::Ratio(pr,br)) => {
671            //assert Nil divisor on rhs
672            match **br {
673               Type::Tuple(ref bs) if bs.len()==0 => {
674                  lt.most_general_unifier(pr)
675               }, _ => { Type::And(vec![]) }
676            }
677         },
678         (Type::Ratio(pl,bl),rt) => {
679            //assert Nil divisor on rhs
680            match **bl {
681               Type::Tuple(ref bs) if bs.len()==0 => {
682                  pl.most_general_unifier(rt)
683               }, _ => { Type::And(vec![]) }
684            }
685         },
686
687         //everything else is a mixed bag
688         (Type::Named(lv,lps),Type::Named(rv,rps))
689         if lv==rv && lps.len()==rps.len() => {
690            let mut tps = Vec::new();
691            for (lp,rp) in std::iter::zip(lps,rps) {
692               let nt = lp.most_general_unifier(rp);
693               if nt.is_bottom() { return nt.clone(); }
694               tps.push(nt);
695            }
696            Type::Named(lv.clone(),tps)
697         }
698         (Type::Arrow(pl,bl),Type::Arrow(pr,br)) => {
699            let pt = if pl == pr { (**pl).clone() } else { Type::And(vec![]) };
700            if pt.is_bottom() { return pt.clone(); }
701            let bt = bl.most_general_unifier(br);
702            if bt.is_bottom() { return bt.clone(); }
703            Type::Arrow(Box::new(pt),Box::new(bt))
704         },
705         (Type::Product(la),Type::Product(ra)) if la.len()==ra.len() => {
706            let mut ts = Vec::new();
707            for (lt,rt) in std::iter::zip(la,ra) {
708               let nt = lt.most_general_unifier(rt);
709               if nt.is_bottom() { return nt.clone(); }
710               ts.push(nt.clone());
711            }
712            Type::Product(ts)
713         },
714         (Type::Tuple(la),Type::Tuple(ra)) if la.len()==ra.len() => {
715            let mut ts = Vec::new();
716            for (lt,rt) in std::iter::zip(la,ra) {
717               let nt = lt.most_general_unifier(rt);
718               if nt.is_bottom() { return nt.clone(); }
719               ts.push(nt.clone());
720            }
721            Type::Tuple(ts)
722         },
723         (Type::Tuple(la),Type::Tuple(ra)) if la.len()==1 && ra.len()==0 => {
724            Type::HTuple(Box::new(la[0].clone()), Constant::Tuple(Vec::new()))
725         },
726         (Type::Tuple(la),Type::Tuple(ra)) if la.len()==0 && ra.len()==1 => {
727            Type::HTuple(Box::new(ra[0].clone()), Constant::Tuple(Vec::new()))
728         },
729         (Type::HTuple(lb,lc),Type::HTuple(rb,rc)) if lc==rc => {
730            let bt = lb.most_general_unifier(rb);
731            if bt.is_bottom() { return bt.clone(); }
732            Type::HTuple(Box::new(bt), lc.clone())
733         },
734
735         (Type::Constant(lv),Type::Constant(rv)) if lv==rv => {
736            Type::Constant(lv.clone())
737         },
738         _ => Type::And(vec![]),
739      }
740   }
741}
742
743impl std::fmt::Debug for Type {
744    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
745        match self {
746           Type::Any => write!(f, "?"),
747           Type::MaybeZero(tt) => write!(f, "{:?}?", tt),
748           Type::Named(t,ts) => {
749              if ts.len()==0 { write!(f, "{}", t) }
750              else { write!(f, "{}<{}>", t, ts.iter().map(|t|format!("{:?}",t)).collect::<Vec<String>>().join(",") ) }
751           }
752           Type::And(ts) => write!(f, "{{{}}}", ts.iter().map(|t|format!("{:?}",t)).collect::<Vec<String>>().join("+") ),
753           Type::Tuple(ts) => write!(f, "({})", ts.iter().map(|t|format!("{:?}",t)).collect::<Vec<String>>().join(",") ),
754           Type::HTuple(bt,ct) => write!(f, "{:?}[{:?}]", bt, ct),
755           Type::Product(ts) => write!(f, "({})", ts.iter().map(|t|format!("{:?}",t)).collect::<Vec<String>>().join("*") ),
756           Type::Arrow(p,b) => write!(f, "({:?})->({:?})", p, b),
757           Type::Ratio(n,d) => write!(f, "({:?})/({:?})", n, d),
758           Type::Constant(cv) => write!(f, "[{:?}]", cv),
759        }
760    }
761}
762