lsts/
scope.rs

1use std::collections::HashMap;
2use crate::typ::Type;
3use crate::kind::Kind;
4use crate::term::TermId;
5use crate::tlc::TLC;
6
7#[derive(Clone, Copy, Debug)]
8pub struct ScopeId {
9   pub id: usize,
10}
11
12#[derive(Clone)]
13pub struct Scope {
14   pub parent: Option<ScopeId>,
15   pub children: Vec<(String,HashMap<Type,Kind>,Type,Option<TermId>)>,
16}
17
18impl Scope {
19   pub fn lookup_term(tlc: &TLC, scope: ScopeId, v: &str, t: &Type) -> Option<TermId> {
20      let mut candidates = Vec::new();
21      for (cv,_ck,ct,cb) in tlc.scopes[scope.id].children.iter() {
22         // NO  neg:(Integer)->(Integer) => (Whole)->(Integer)
23         // YES neg:(Integer)->(Integer) => (Integer)->(Integer)
24         //arrow candidates are covariant because this is an existential context
25         //domain(variable) => domain(candidate)
26         //range (variable) => range (candidate)
27         if cv == v {
28         if let Some(cb) = cb {
29         match (t,ct) {
30            (Type::Arrow(td,tr),Type::Arrow(ctd,ctr)) => { if
31               !Type::implies(tlc, td, ctd).is_bottom() &&
32               !Type::implies(tlc, tr, ctr).is_bottom() {
33               candidates.push((ct.clone(), *cb));
34            }}, _ => { if !Type::implies(tlc, t, ct).is_bottom() {
35               candidates.push((ct.clone(), *cb));
36            }},
37         }}}
38      }
39      if candidates.len() == 0 {
40         if let Some(psc) = tlc.scopes[scope.id].parent {
41            return Scope::lookup_term(tlc, psc, v, t);
42         } else {
43            return None;
44         }
45      } else if candidates.len() == 1 {
46         return Some(candidates[0].1);
47      } else {
48         //careful specialization can be made sound
49         //symbol .binary : {(Integer)->(SignedBinary)+({Integer+Whole})->({Binary+SignedBinary})}
50         // .binary : (Whole)->(Binary)
51         // .binary : (Integer)->(SignedBinary)', src/scope.rs:57:10
52         //choose (Whole)->(Binary) because
53         // domain(Whole -> Binary) => domain(Integer -> SignedBinary)
54         // range(Whole -> Binary) => range(Integer -> SignedBinary)
55         for (xi,(xt,xb)) in candidates.iter().enumerate() {
56            let mut all_accept = true;
57            for (yi,(yt,_yb)) in candidates.iter().enumerate() {
58               if xi==yi { continue; }
59               match (xt,yt) {
60                  (Type::Arrow(xd,xr),Type::Arrow(yd,yr)) => {
61                  if Type::implies(tlc, xd, yd).is_bottom()
62                  || Type::implies(tlc, xr, yr).is_bottom() {
63                     all_accept = false;
64                  }},
65                  _ => { all_accept = false; }
66               }
67            }
68            if all_accept { return Some(*xb); }
69         }
70         let mut cs = "".to_string();
71         for (ct,_) in candidates.iter() {
72            cs += &format!("\n{} : {:?}", v, ct);
73         };
74         panic!("Scope::lookup_term multiple viable candidate functions found for symbol {} : {:?}{}", v, t, cs)
75      }
76   }
77}
lsts/scope.rs

lsts/
scope.rs
