Add Krivine

diff --git a/src/abstract_machines/krivine.rs b/src/abstract_machines/krivine.rs
new file mode 100644 (file)
index 0000000..db99686
--- /dev/null
+++ b/src/abstract_machines/krivine.rs
@@ -0,0 +1,81 @@
+#[derive(Clone, Debug, PartialEq)]
+enum V {
+    Free(String),
+    Bound(usize),
+}
+
+#[derive(Clone, Debug)]
+enum Term {
+    Appl(Box<(Term, Term)>),
+    Var(V),
+    Abst(Box<Term>),
+}
+
+#[derive(Clone, Debug)]
+enum Value {
+    Closure(Term, Vec<(V, Value)>),
+}
+
+#[derive(Clone, Debug)]
+struct State(Term, Vec<Value>, Vec<(V, Value)>);
+
+impl State {
+    fn eval(&self) -> Self {
+        match self {
+            State(Term::Abst(_), s, _) if s.len() == 0 => self.clone(),
+            s => {
+                let new_s = s.step();
+                new_s.eval()
+            }
+        }
+    }
+
+    fn step(&self) -> Self {
+        match self {
+            State(Term::Abst(m), s, e) => {
+                match s.split_first() {
+                    Some((head, tail)) => {
+                        let mut new_e = vec![(V::Bound(0), head.clone())];
+                        new_e.append(&mut e.clone());
+                        State(*m.clone(), tail.to_vec(), new_e)
+                    },
+                    None => { todo!() }
+                }
+            },
+            State(Term::Appl(tuple), s, e) => {
+                let (m, n) = *tuple.clone();
+                let mut new_s = vec![Value::Closure(n.clone(), e.clone())];
+                new_s.append(&mut s.clone());
+                State(m.clone(), new_s, e.clone())
+            },
+            State(Term::Var(x), s, e) => {
+                let m = e.iter().find(|item| {
+                    let (var, _) = *item;
+                    *var == *x
+                });
+                match m {
+                    Some(item) => {
+                        let (_, Value::Closure(m, new_e)) = item;
+                        State(m.clone(), s.clone(), new_e.clone())
+                    },
+                    None => panic!()
+                        
+                }
+            }
+        }
+    }
+}
+
+pub fn main() {
+    use Term::*;
+    use V::*;
+    println!("Krivine:");
+
+    let t1: Term = Appl(Box::new((Abst(Box::new(Appl(Box::new((Var(Bound(0)), Var(Bound(0))))))), (Abst(Box::new(Var(Bound(0))))))));
+    let result = State(t1, vec![], vec![]).eval();
+    println!("T1 eval: {:?}", result);
+
+    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)))))));
+    let result2 = State(t2, vec![], vec![]).eval();                                                                     
+    println!("T2 eval: {:?}", result2);
+}

diff --git a/src/abstract_machines/mod.rs b/src/abstract_machines/mod.rs
index 59f7641c93f3f04953cd5e3df3944e63a535f654..956384196454a4a4044995a54bfd87a6445e72f4 100644 (file)
--- a/src/abstract_machines/mod.rs
+++ b/src/abstract_machines/mod.rs
@@ -1 +1,2 @@
 pub mod cek;
+pub mod krivine;

diff --git a/src/main.rs b/src/main.rs
index 1b4716d94700b064c4af528ac49c5199133bdec2..d6fa209498fd3b80addf796811eb46fe4a1ba6ff 100644 (file)
--- a/src/main.rs
+++ b/src/main.rs
@@ -1,5 +1,7 @@
 use machines::abstract_machines::cek;
+use machines::abstract_machines::krivine;
 
 fn main() {
     cek::main();
+    krivine::main();
 }