Repl

src/exec/mod.rs

@@ -9,7 +9,7 @@ impl Ast {
     pub fn beta_reduce(self) -> Ast {
         match self {
             Ast::Application(lhs, rhs) => match *lhs {
-                Ast::Abstraction(var, _, ast) => ast.subst(var, *rhs),
+                Ast::Abstraction(var, _, ast) => ast.subst(var, *rhs).beta_reduce(),
                 lhs => Ast::Application(Box::new(lhs), rhs),
             },
             t => t,
@@ -79,7 +79,7 @@ impl DeBrujinAst {
     pub fn beta_reduce(self) -> DeBrujinAst {
         match self {
             DeBrujinAst::Application(lhs, rhs) => match *lhs {
-                DeBrujinAst::Abstraction(ast) => ast.subst_bound(1, *rhs),
+                DeBrujinAst::Abstraction(ast) => ast.subst_bound(1, *rhs).beta_reduce(),
                 lhs => DeBrujinAst::Application(Box::new(lhs), rhs),
             },
             a => a,

src/lib.rs

@@ -6,16 +6,19 @@ mod exec;
 mod inference;
 mod parse;
 
+pub use inference::infer_type;
+pub use parse::{ParseError, is_ident, parse, parse_type, sexpr::parse_string};
+
 type Ident = String;
 
 #[derive(Debug, Clone, PartialEq, Eq)]
-enum PrimitiveType {
+pub enum PrimitiveType {
     Nat,
     Bool,
 }
 
 #[derive(Debug, Clone, PartialEq, Eq)]
-enum Type {
+pub enum Type {
     Primitive(PrimitiveType),    // Bool | Nat
     Arrow(Box<Type>, Box<Type>), // 0 -> 1
 }
@@ -33,13 +36,13 @@ impl Type {
 }
 
 #[derive(Debug, Clone, PartialEq, Eq)]
-enum Constant {
+pub enum Constant {
     Nat(usize),
     Bool(bool),
 }
 
 #[derive(Debug, Clone, PartialEq, Eq)]
-enum Ast {
+pub enum Ast {
     Abstraction(Ident, Type, Box<Ast>), // \0:1.2
     Application(Box<Ast>, Box<Ast>),    // 0 1
     Variable(Ident),                    // x
@@ -50,7 +53,7 @@ impl Display for Ast {
     fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
         match self {
             Ast::Abstraction(var, typ, ast) => write!(f, "(\\ ({var} {typ}) ({ast}))"),
-            Ast::Application(lhs, rhs) => write!(f, "(lhs rhs)"),
+            Ast::Application(lhs, rhs) => write!(f, "({lhs} {rhs})"),
             Ast::Variable(v) => write!(f, "{v}"),
             Ast::Constant(constant) => write!(f, "{constant}"),
         }

src/main.rs

@@ -1 +1,80 @@
-fn main() {}
+use std::{
+    collections::HashMap,
+    io::{Write, stdin, stdout},
+    rc::Rc,
+};
+
+use stlc_type_inference::{infer_type, is_ident, parse, parse_string, parse_type};
+
+macro_rules! repl_err {
+    ($err:expr) => {{
+        println!($err);
+        print!("> ");
+        stdout().flush().unwrap();
+        continue;
+    }};
+}
+
+fn main() {
+    let mut gamma = Rc::new(HashMap::new());
+    print!("> ");
+    stdout().flush().unwrap();
+    for line in stdin().lines() {
+        let line = line.unwrap();
+        if let Some(tl) = line.strip_prefix(':') {
+            if let Some((cmd, expr)) = tl.split_once(' ') {
+                match cmd {
+                    "t" => match parse(expr) {
+                        Ok(a) => match infer_type(gamma.clone(), a) {
+                            Ok(t) => println!("{t}"),
+                            Err(e) => repl_err!("Could not infer type {e:?}"),
+                        },
+                        Err(e) => repl_err!("Parse error {e:?}"),
+                    },
+                    "ctx" => {
+                        if let Some((ident, typ)) = expr.split_once(':') {
+                            let ident: String =
+                                ident.chars().filter(|c| !c.is_whitespace()).collect();
+                            if !is_ident(&ident) {
+                                repl_err!("{ident} is not a valid identifer");
+                            }
+                            let typ_ast = match parse_string(typ) {
+                                Ok(t) => t,
+                                Err(e) => repl_err!("Could not parse the type: {e:?}"),
+                            };
+
+                            let typ = match parse_type(&typ_ast) {
+                                Ok(t) => t,
+                                Err(e) => repl_err!("type could not be parsed {e:?}"),
+                            };
+
+                            println!("Added {ident} with type {typ} to the context");
+                            Rc::make_mut(&mut gamma).insert(ident, typ);
+                        }
+                    }
+                    c => println!("Unknown command {c}"),
+                }
+            } else {
+                match tl {
+                    "t" => println!(":t need an expr as an argument"),
+                    "ctx" => println!(":ctx needs an ident and a type as argument"),
+                    c => println!("Unknown command {c}"),
+                }
+            }
+        } else {
+            let ast = match parse(&line) {
+                Ok(a) => a,
+                Err(e) => repl_err!("Parse error {e:?}"),
+            };
+
+            let typ = match infer_type(gamma.clone(), ast.clone()) {
+                Ok(t) => t,
+                Err(e) => repl_err!("Could not infer type {e:?}"),
+            };
+            let ast = ast.beta_reduce();
+            println!("{ast} : {typ}")
+        }
+        print!("> ");
+        stdout().flush().unwrap();
+    }
+}

src/parse/mod.rs

@@ -2,7 +2,7 @@ use sexpr::{Sexpr, parse_string};
 
 use crate::{Ast, Constant, PrimitiveType, Type};
 
-mod sexpr;
+pub mod sexpr;
 #[cfg(test)]
 mod test;
 
@@ -145,11 +145,11 @@ fn parse_symbol(s: String) -> Result<Ast, ParseError> {
     }
 }
 
-fn is_ident(s: &str) -> bool {
+pub fn is_ident(s: &str) -> bool {
     s.starts_with(|c: char| c.is_alphabetic()) && s.chars().all(|c| c.is_alphanumeric())
 }
 
-fn parse_type(ast: &Sexpr) -> Result<Type, ParseError> {
+pub fn parse_type(ast: &Sexpr) -> Result<Type, ParseError> {
     match ast {
         Sexpr::Symbol(s) => parse_prim_type(s),
         Sexpr::List(sexprs) => parse_type_list(sexprs),

src/parse/sexpr.rs

@@ -34,7 +34,7 @@ impl Sexpr {
     }
 }
 
-pub fn tokenize(input: &str) -> Vec<Token> {
+fn tokenize(input: &str) -> Vec<Token> {
     let mut tokens = Vec::new();
     // let mut chars = input.chars().peekable();
     let mut chars = input.chars().peekable();
@@ -77,7 +77,7 @@ fn parse_expr(tokens: &mut Peekable<IntoIter<Token>>) -> Result<Sexpr, ParseErro
     }
 }
 
-pub fn parse(tokens: Vec<Token>) -> Result<Sexpr, ParseError> {
+fn parse(tokens: Vec<Token>) -> Result<Sexpr, ParseError> {
     let mut tokens = tokens.into_iter().peekable();
     let ast = parse_expr(&mut tokens)?;
     if tokens.peek().is_some() {