stlt.rs

use std::fmt;

#[derive(Debug)]
enum Type {
    Number,
    Prod(Box<Type>, Box<Type>),
    Fun(Box<Type>, Box<Type>)
}

#[derive(Debug)]
enum SList<T> {
    Nil,
    Snoc(Box<SList<T>>, Box<T>)
}

#[derive(Debug)]
enum Variable {
    Here,
    There(Box<Variable>)
}

#[derive(Debug)]
enum Term {
    Lit(u8),
    Pair(Box<Term>, Box<Term>),
    Fst(Box<Term>),
    Snd(Box<Term>),
    Lam(Box<Term>),
    App(Box<Term>, Box<Term>)
}

#[derive(Debug)]
enum Value {
    LitVal(u8),
    PairVal(Box<Value>, Box<Value>),
    LamVal(Box<SList<Value>>, Box<Term>)
}

fn eval(env: &SList<Value>, tm: &Term) -> Result<Value, &'static str> {
    match &*tm {
        Term::Lit(i) => Ok(Value::LitVal(*i)),
        Term::Pair(x,y) => {
            let u = eval(env, x).unwrap();
            let v = eval(env, y).unwrap();
            Ok(Value::PairVal(Box::new(u), Box::new(v)))
        },
        Term::Fst(p) => {
            let p2 = eval(env, p).unwrap();
            match p2 {
                Value::PairVal(u, _) => Ok(*u),
                _ => Err("Whoops!")
            }
        },
        Term::Snd(p) => {
            let p2 = eval(env, p).unwrap();
            match p2 {
                Value::PairVal(_, v) => Ok(*v),
                _ => Err("Woops!")
            }
        },
        Term::Lam(m) => Ok(Value::LamVal(Box::new(*env), *m)),
        Term::App(f,x) => {
            let u = eval(env, f).unwrap();
            let v = eval(env, x).unwrap();
            match u {
                Value::LamVal(env2, m) => eval(&SList::Snoc(env2, Box::new(v)), &m),
                _ => Err("Whoops!")
            }
        }
    }
}