finished implementation

src/main.rs

@@ -6,75 +6,107 @@ use std::fmt;
 enum Type {
     Variable(String),
     Function(Box<Type>, Box<Type>),
-    Undefined,
 }
 
 impl fmt::Display for Type {
     fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
         match self {
             Type::Variable(name) => write!(f, "{}", name),
             Type::Function(t1, t2) => write!(f, "({} -> {})", t1, t2),
-            Type::Undefined => write!(f, "undefined")
         }
     }
 }
 
 #[derive(Debug, Clone)]
 enum Term {
-    Variable(String, Type),
+    Variable(String),
     Abstraction(String, Type, Box<Term>),
     Application(Box<Term>, Box<Term>),
 }
 
 impl fmt::Display for Term {
     fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
         match self {
-            Term::Variable(name, _) => write!(f, "{}", name),
-            Term::Abstraction(vname, vtype, t) => write!(f, "λ{}:{}. {})", vname, vtype, t),
+            Term::Variable(name) => write!(f, "{}", name),
+            Term::Abstraction(vname, vtype, t) => write!(f, "λ {}:{}. {}", vname, vtype, t),
             Term::Application(t1, t2) => write!(f, "{} {}", t1, t2),
         }
     }
 }
 
 #[derive(Clone)]
 enum AST {
-    Variable(String),
-    Function(String, Vec<AST>),
-    Assume(Box<AST>, Type),
+    ImpI(Term, Box<AST>),
+    ImpE(Box<AST>, Box<AST>),
+    Assume(Term, Type),
+}
+
+#[derive(Clone)]
+enum Env<K, V> {
+    Entry(K, V, Box<Env<K, V>>),
+    Empty,
+}
+
+impl<K:PartialEq+Clone, V:Clone> Env<K, V> {
+    fn new() -> Env<K, V> {
+        Env::Empty
+    }
+
+    fn insert(&self, key: K, value: V) -> Env<K, V> {
+        Env::Entry(key, value, Box::new(self.clone()))
+    }
+
+    fn find(&self, key: &K) -> Option<V> {
+        match self {
+            Env::Entry(k, v, n) => {
+                if *k == *key {
+                    Some(v.clone())
+                } else {
+                    n.find(key)
+                }
+            },
+            Env::Empty => None
+        }
+    }
+
+    fn marge(&self, env: Env<K, V>) -> Env<K, V> {
+        match self {
+            Env::Entry(k, v, n) => {
+                n.marge(Env::Entry(k.clone(), v.clone(), Box::new(env)))
+            }
+            Env::Empty => env
+        }
+    }
 }
 
+type VarEnv = Env<String, Type>;
+
 macro_rules! s {
     ($str: expr) => { $str.to_string() }
 }
 
 macro_rules! impI {
-    ($($t: expr), *) => { AST::Function(s!("impI"), vec!($($t, )*)) }
+    ($t1: expr, $t2: expr) => { AST::ImpI($t1, Box::new($t2)) }
 }
 
 macro_rules! impE {
-    ($($t: expr), *) => { AST::Function(s!("impE"), vec!($($t, )*)) }
+    ($t1: expr, $t2: expr) => { AST::ImpE(Box::new($t1), Box::new($t2)) }
 }
 
 macro_rules! assume {
-    ($t1: expr, $t2: expr) => { AST::Assume(Box::new($t1), $t2) }
+    ($t1: expr, $t2: expr) => { AST::Assume($t1, $t2) }
 }
 
 macro_rules! fun {
     ($t1: expr, $t2: expr) => { Type::Function(Box::new($t1), Box::new($t2)) }
 }
 
-/*
-macro_rules! check_args {
-    ($args: expr, $($ty: ty), *)
-}
-*/
-
 // reduces function type
-// apply_fun(a -> b, b) => a
+// apply_fun(a -> b, a) => b
 fn apply_fun(t1: Type, t2: Type) -> Result<Type, String> {
     if let Type::Function(a, b) = t1.clone() {
         if *a == t2 {
-            Ok(t1)
+            Ok(*b)
         }
         else {
             Err(format!("argument type of '{:?}' and '{:?}' must be equal", t1, t2))
@@ -85,40 +117,31 @@ fn apply_fun(t1: Type, t2: Type) -> Result<Type, String> {
     }
 }
 
-fn eval(ast: AST) -> Result<(Term, Type), String> {
+fn eval(ast: AST) -> Result<(Term, Type, VarEnv), String> {
     match ast {
-        AST::Variable(name) => Ok((Term::Variable(name, Type::Undefined), Type::Undefined)),
-        AST::Function(name, args) => {
-            match &*name {
-                "impI" => {
-                    let (t1, t1t) = eval(args[0].clone())?;
-                    let (t2, t2t) = eval(args[1].clone())?;
-                    if let Term::Variable(name, _) = t1 {
-                        Ok((Term::Abstraction(name, t1t.clone(), Box::new(t2)), fun!(t1t, t2t)))
-                    }
-                    else {
-                        Err(s!("t1 must be a variable"))
-                    }
-
-                },
-                "impE" => {
-                    let (t1, t1t) = eval(args[0].clone())?;
-                    let (t2, t2t) = eval(args[1].clone())?;
-                    if let Type::Function(_, _) = t1t {
-                        Ok((Term::Application(Box::new(t1), Box::new(t2)), apply_fun(t1t, t2t)?))
-                    }
-                    else {
-                        Err(s!("t1 must be a abstraction"))
-                    }
-
-                },
-                _ => Err(format!("'{}' is not defined", name)),
+        AST::ImpE(t1, t2) => {
+            let (t1, t1t, env1) = eval(*t1)?;
+            let (t2, t2t, env2) = eval(*t2)?;
+            if let Type::Function(_, _) = t1t {
+                Ok((Term::Application(Box::new(t1), Box::new(t2)), apply_fun(t1t, t2t)?, env1.marge(env2)))
             }
-        }
+            else {
+                Err(s!("t1 must be a abstraction"))
+            }
+        },
+        AST::ImpI(t1, t2) => {
+            let (t2, t2t, env2) = eval(*t2)?;
+            if let Term::Variable(name) = t1 {
+                let t1t = env2.find(&name).unwrap();
+                Ok((Term::Abstraction(name, t1t.clone(), Box::new(t2)), fun!(t1t, t2t), env2))
+            }
+            else {
+                Err(s!("t1 must be a variable"))
+            }
+        },
         AST::Assume(t1, t2) => {
-            let (t1, t1t) = eval(*t1)?;
-            if let Term::Variable(name, _) = t1 {
-                Ok((Term::Variable(name, t2.clone()), t2))
+            if let Term::Variable(name) = t1 {
+                Ok((Term::Variable(name.clone()), t2.clone(), VarEnv::new().insert(name, t2)))
             }
             else {
                 Err(s!("t1 must be a Variable"))
@@ -128,13 +151,14 @@ fn eval(ast: AST) -> Result<(Term, Type), String> {
 }
 
 fn main() {
-    let x = AST::Variable(s!("x"));
-    let y = AST::Variable(s!("y"));
+    let x = Term::Variable(s!("x"));
+    let y = Term::Variable(s!("y"));
     let a = Type::Variable(s!("a"));
     let b = Type::Variable(s!("b"));
     let prop = impI!(x.clone(), impI!(y.clone(), impE!(assume!(y, fun!(a.clone(), b)), assume!(x, a))));
 
-    let (expr, ty) = eval(prop).unwrap();
-    println!("{}", expr);
-    println!("{}", ty);
+    let (expr, ty, _) = eval(prop).unwrap();
+    println!("|- {}", ty);
+    println!("because");
+    println!("|- {} : {}", expr, ty);
 }