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#[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>), Arrow(Box<Type>,Box<Type>),
34 Tuple(Vec<Type>), HTuple(Box<Type>,Constant),
36 Product(Vec<Type>), 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()), }
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()), }
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 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()), 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()); } 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(<) {
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 let tt = match (self,other) {
449 (Type::And(lts),_) if lts.len()==0 => { Type::And(vec![]) },
451 (_,Type::And(rts)) if rts.len()==0 => { Type::And(vec![]) },
452
453 (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 (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 (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 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 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 (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) } else {
545 pr.__implication_unifier(pl,subs,InArrow::Lhs) };
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 match (self,other) {
609 (Type::And(lts),_) if lts.len()==0 => { Type::And(vec![]) },
611 (_,Type::And(rts)) if rts.len()==0 => { Type::And(vec![]) },
612
613 (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 (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 (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 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 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 (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