lambdascript 0.2.4

#![allow(unused_variables)]
#![allow(non_snake_case)]
#![allow(non_camel_case_types)]
#![allow(unused_parens)]
#![allow(unused_mut)]
#![allow(unused_imports)]
#![allow(unused_assignments)]
#![allow(dead_code)]

// Lambda7c type
#[derive(Clone,Debug,PartialEq,Eq,Hash)]
pub enum lrtype {
  String_t,
  Unit_t,
  Float_t,
  Int_t,
  LRlist(Box<lrtype>),
  LRtuple(Vec<lrtype>),
  LRfun(Vec<lrtype>), // last type is return type
  LRvar(i32), // type variable, signed for later flexibility
  LRunknown,
  LRuntypable,
}//lrtype
impl Default for lrtype { fn default()->Self {lrtype::LRunknown} }

impl lrtype
{
  fn occurs_check(&self, x:i32) -> bool  // true means does not occur
  {  match self {
       LRvar(y) if x==*y => false,
       LRuntypable => false,
       LRlist(t) => t.occurs_check(x),
       LRtuple(ts) | LRfun(ts) => {
         let mut result = true;
         for t in ts {
           if !t.occurs_check(x) { result=false; break; }
         }
         result
       },
       _ => true,  
     }//match
  }// occurs_check

  // non-destructive substitution [t/x] to type
  fn apply_subst(&self, x:i32, t:&lrtype) -> lrtype
  { match self {
      LRvar(y) if *y==x => t.clone(),
      LRunknown => t.clone(),
      LRlist(ty) => LRlist(Box::new(ty.apply_subst(x,t))),
      LRtuple(ts) => LRtuple(ts.iter().map(|y|y.apply_subst(x,t)).collect()),
      LRfun(ts) => LRfun(ts.iter().map(|y|y.apply_subst(x,t)).collect()),
      _ => self.clone(),
    }//match
  }//apply_subst

  fn grounded(&self) -> bool
  {
    match self {
      LRuntypable | LRunknown | LRvar(_) => false,
      LRlist(t) => t.grounded(),
      LRtuple(tv) | LRfun(tv) => {
        let mut result = true;
        for t in tv { if !t.grounded() {result=false; break;} }
        result
      },
      _ => true,
    }//match
  }//grounded

  fn numerical(&self) -> bool
  {
     match self {
       Int_t | Float_t => true,
       _ => false,
     }
  }//numerical

  fn funtype(&self) -> bool {
    if let LRfun(_) = self {true} else {false}
  }
}// lrtype

// unification algorithm
type Equations = Vec<(lrtype,lrtype)>;

//returns substitution map for unifier on success
pub fn unify_types(equations:&mut Equations) -> Option<HashMap<i32,lrtype>>
{
  let mut unifier = HashMap::new();
  let mut failure = false;
  let mut eqi = 0; //indexes equations
  while eqi < equations.len()  // break when failure detected
  {
    let mut neweqs:BTreeMap<usize,(lrtype,lrtype)> = BTreeMap::new();
    let (ref s,ref t) = equations[eqi];
    if (s==t) { eqi+=1; continue; }
    match (s,t) {
      (LRvar(x),u) | (u,LRvar(x)) if u.occurs_check(*x) => {
        for i in 0..equations.len() {
          if i==eqi {continue;}
          let (ref ta,ref tb) = equations[i];
          let ta2 = ta.apply_subst(*x,u);
          let tb2 = tb.apply_subst(*x,u);
          //equations[i] = (ta2,tb2);  // mutation!
          neweqs.insert(i,(ta2,tb2));
        }//for
      },
      (LRlist(ta),LRlist(tb)) => {
        equations.push((*ta.clone(),*tb.clone())); // why no checker error?
      },      
      (LRtuple(tav),LRtuple(tbv)) | (LRfun(tav),LRfun(tbv)) if tav.len()==tbv.len() => {
        for i in 0..tav.len() {
          neweqs.insert(equations.len()+i,(tav[i].clone(),tbv[i].clone()));
          //equations.push((tav[i].clone(), tbv[i].clone()));
        }
      },
      _ => {failure=true; break; }
    }//match
    let originalen = equations.len();
    for (i,(a,b)) in neweqs {
      if i<originalen { equations[i] = (a,b); }
      else { equations.push((a,b));}
    }
    eqi += 1;
  }//while eqi<equations.len()
  // construct unifier
  eqi = equations.len();
  while eqi>0 
  {
     eqi -= 1;
     match &equations[eqi] {
       (LRvar(x), u) | (u,LRvar(x)) if !unifier.contains_key(x) => {
         unifier.insert(*x,u.clone());
       },
       _ => (),
     }//match
  }// while eqi>0
  if failure {None} else {Some(unifier)}
}//unify_types

pub fn unifytest()
{
  let t1 = LRlist(Box::new(LRvar(4)));
  let t2 = LRlist(Box::new(Int_t));
  let t3 = LRlist(Box::new(LRvar(5)));
  let mut eq1 = vec![(t1.clone(),t2), (t1.clone(),t3)];
  eq1.push((LRvar(1),LRvar(2)));
  eq1.push((LRvar(4),LRvar(2)));  
  if let Some(unifier) = unify_types(&mut eq1) {
    for (x,t) in unifier.iter() {
      println!("var_{} = {:?}", x, t);
    }
  }
  else {println!("unification failed");}
}//unifytest


///////////// type checking lambda7c (with minimal type inference)
// type checking returns a grounded type for all declarations.