zjednywacz/src/main.rs

use std::rc::Rc;

// type id = string
#[derive(Eq, PartialEq, Clone, Debug)]
struct Id(Rc<String>);

//type term =
//| Var of id
//| Term of id * term list
#[derive(Eq, PartialEq, Clone, Debug)]
enum Term {
    Var(Id),
    Ter(Id, Vec<Term>),
}

//(* invariant for substitutions: *)
//(* no id on a lhs occurs in any term earlier in the list *)
//type substitution = (id * term) list
#[derive(Eq, PartialEq, Clone, Debug)]
struct Substitution(Vec<(Id, Term)>);

/*
(* check if a variable occurs in a term *)
let rec occurs (x : id) (t : term) : bool =
  match t with
  | Var y -> x = y
  | Term (_, s) -> List.exists (occurs x) s

*/
fn occurs(x: &Id, t: &Term) -> bool {
    match t {
        Term::Var(id) => id == x,
        Term::Ter(_, s) => s.iter().find(|t| occurs(x, t)).is_some()
    }
}

/*
(* substitute term s for all occurrences of variable x in term t *)
let rec subst (s : term) (x : id) (t : term) : term =
  match t with
  | Var y -> if x = y then s else t
  | Term (f, u) -> Term (f, List.map (subst s x) u)
*/

fn subst(s: &Term, x: &Id, t: &Term) -> Term {
    match t {
        Term::Var(y) => if x == y { s.clone() } else { Term::Var(y.clone()) },
        Term::Ter(f, u) => Term::Ter(f.clone(),
                                     u.iter().map(|q| subst(s, x, q)).collect())
    }
}

/*
(* apply a substitution right to left *)
let apply (s : substitution) (t : term) : term =
  List.fold_right (fun (x, u) -> subst u x) s t
*/
fn apply(Substitution(s): &Substitution, t: &Term) -> Term {
    s.iter().fold(t.clone(), |q, (x, u)| subst(u, x, &q))
}

/*
(* unify one pair *)
let rec unify_one (s : term) (t : term) : substitution =
  match (s, t) with
  | (Var x, Var y) -> if x = y then [] else [(x, t)]
  | (Term (f, sc), Term (g, tc)) ->
      if f = g && List.length sc = List.length tc
      then unify (List.combine sc tc)
      else failwith "not unifiable: head symbol conflict"
  | ((Var x, (Term (_, _) as t)) | ((Term (_, _) as t), Var x)) ->
      if occurs x t
      then failwith "not unifiable: circularity"
      else [(x, t)]
*/
fn unify_one(s: &Term, t: &Term) -> Result<Substitution, &'static str> {
    match (s, t) {
        (Term::Var(x), Term::Var(y)) =>
            Ok(Substitution(if x == y { Vec::new() } else { vec![(x.clone(), t.clone())] })),
        (Term::Ter(f, sc), Term::Ter(g, tc)) =>
            if f == g && sc.len() == tc.len()
            { unify(sc.iter().zip(tc.iter()).collect()) } else { Err("Cannot into: head symbol conflict") },
        (Term::Var(x), t @ Term::Ter(_, _)) | (t @ Term::Ter(_, _), Term::Var(x)) =>
            if occurs(x, t) { Err("koło") } else { Ok(Substitution(vec![(x.clone(), t.clone())])) }
    }
}
/*
(* unify a list of pairs *)
and unify (s : (term * term) list) : substitution =
  match s with
  | [] -> []
  | (x, y) :: t ->
      let t2 = unify t in
      let t1 = unify_one (apply t2 x) (apply t2 y) in
      t1 @ t2
*/
fn unify(s: Vec<(&Term, &Term)>) -> Result<Substitution, &'static str> {
    match s.split_first() {
        None => Ok(Substitution(Vec::new())), // Vec::new nie grabi pamięci \:D/
        Some(((x, y), t)) => {
            let t = unify(t.to_vec())?;
            let Substitution(t1) =
                unify_one(&apply(&t, &x), &apply(&t, &y))?;
            let Substitution(v) = t;
            // mógłbym rozszerzać t1 (t1.extend(v);), ale tak bezpieczniej
            Ok(Substitution(t1.into_iter().chain(v.into_iter()).collect()))
        }
    }
}

fn main() {
    {
        let mut x = "x".to_owned();
        let a1 = Rc::new("xd".to_owned());
        x.push('d');
        let a2 = Rc::new(x);
        println!("{}, {}", a1 == a2, &a1 == &a2);
        let a3 = a2.clone();
        println!(" {} {}", Rc::strong_count(&a2), Rc::strong_count(&a3), )
    }
    let a1 = Term::Var(Id(Rc::new("xd".to_owned())));
    let a2 = Term::Var(Id(Rc::new("qw".to_owned())));
    println!("{:?} -- {:?} ---> {:?}", &a1, &a2, unify_one(&a1, &a2));

    let a1 = Term::Ter(Id(Rc::new("xdaad".to_owned())), vec![]);
    let a2 = Term::Ter(Id(Rc::new("xdaad".to_owned())), vec![]);
    println!("{:?} -- {:?} ---> {:?}", &a1, &a2, unify_one(&a1, &a2));

    let a1 = Term::Ter(Id(Rc::new("int".to_owned())), vec![]);
    let a2 = Term::Ter(Id(Rc::new("nat".to_owned())), vec![]);
    println!("{:?} -- {:?} ---> {:?}", &a1, &a2, unify_one(&a1, &a2));

    let a1 = Term::Ter(Id(Rc::new("xdaad".to_owned())), vec![Term::Var(Id(Rc::new("fffxd".to_owned())))]);
    let a2 = Term::Ter(Id(Rc::new("xdaad".to_owned())), vec![Term::Var(Id(Rc::new("zxczxc".to_owned())))]);
    println!("{:?} -- {:?} ---> {:?}", &a1, &a2, unify_one(&a1, &a2));

    let a1 = Term::Ter(Id(Rc::new("xdaad".to_owned())), vec![Term::Var(Id(Rc::new("fffxd".to_owned())))]);
    let a2 = Term::Ter(Id(Rc::new("xdfewfewfewefaad".to_owned())), vec![Term::Var(Id(Rc::new("zxczxc".to_owned())))]);
    println!("{:?} -- {:?} ---> {:?}", &a1, &a2, unify_one(&a1, &a2));

    let a1 = Term::Ter(Id(Rc::new("int".to_owned())), Vec::new());
    let a2 = Term::Var(Id(Rc::new("xdaad".to_owned())));
    println!("{:?} -- {:?} ---> {:?}", &a1, &a2, unify_one(&a1, &a2));
    println!("{:?} -- {:?} ---> {:?}", &a2, &a1, unify_one(&a2, &a1));


    let a1 = Term::Ter(Id(Rc::new("f".to_owned())), vec![Term::Ter(Id(Rc::new("int".to_owned())), Vec::new()), Term::Var(Id(Rc::new("a".to_owned()))), Term::Var(Id(Rc::new("b".to_owned()))), Term::Var(Id(Rc::new("gg".to_owned())))]);
    let a2 = Term::Ter(Id(Rc::new("f".to_owned())), vec![Term::Var(Id(Rc::new("b".to_owned()))), Term::Ter(Id(Rc::new("mat".to_owned())), Vec::new()), Term::Var(Id(Rc::new("c".to_owned()))), Term::Var(Id(Rc::new("gg".to_owned())))]);
    println!("{:?} -- {:?} ---> {:?}", &a1, &a2, unify_one(&a1, &a2));

}