repos / machines.rs.git

krivine.rs

 1#[derive(Clone, Debug, PartialEq)]
 2enum V {
 3//    Free(String),
 4    Bound(usize),
 5}
 6
 7#[derive(Clone, Debug)]
 8enum Term {
 9    Appl(Box<(Term, Term)>),
10    Var(V),
11    Abst(Box<Term>),
12}
13
14#[derive(Clone, Debug)]
15enum Value {
16    Closure(Term, Vec<(V, Value)>),
17}
18
19#[derive(Clone, Debug)]
20struct State(Term, Vec<Value>, Vec<(V, Value)>);
21
22impl State {
23    fn eval(&self) -> Self {
24        match self {
25            State(Term::Abst(_), s, _) if s.len() == 0 => self.clone(),
26            s => {
27                let new_s = s.step();
28                new_s.eval()
29            }
30        }
31    }
32
33    fn step(&self) -> Self {
34        match self {
35            State(Term::Abst(m), s, e) => {
36                match s.split_first() {
37                    Some((head, tail)) => {
38                        let mut new_e = vec![(V::Bound(0), head.clone())];
39                        new_e.append(&mut e.clone());
40                        State(*m.clone(), tail.to_vec(), new_e)
41                    },
42                    None => { todo!() }
43                }
44            },
45            State(Term::Appl(tuple), s, e) => {
46                let (m, n) = *tuple.clone();
47                let mut new_s = vec![Value::Closure(n.clone(), e.clone())];
48                new_s.append(&mut s.clone());
49                State(m.clone(), new_s, e.clone())
50            },
51            State(Term::Var(x), s, e) => {
52                let m = e.iter().find(|item| {
53                    let (var, _) = *item;
54                    *var == *x
55                });
56                match m {
57                    Some(item) => {
58                        let (_, Value::Closure(m, new_e)) = item;
59                        State(m.clone(), s.clone(), new_e.clone())
60                    },
61                    None => panic!()
62                        
63                }
64            }
65        }
66    }
67}
68
69pub fn main() {
70    use Term::*;
71    use V::*;
72    println!("Krivine:");
73
74    let t1: Term = Appl(Box::new((Abst(Box::new(Appl(Box::new((Var(Bound(0)), Var(Bound(0))))))), (Abst(Box::new(Var(Bound(0))))))));
75    let result = State(t1, vec![], vec![]).eval();
76    println!("T1 eval: {:?}", result);
77
78    let t2: Term = Appl(Box::new((Appl(Box::new((Abst(Box::new(Var(Bound(0)))), Abst(Box::new(Var(Bound(0))))))), Abst(Box::new(Var(Bound(0)))))));
79    let result2 = State(t2, vec![], vec![]).eval();                                                                     
80    println!("T2 eval: {:?}", result2);
81}