From c8062f7843000bcb1295b5b746053aba1570f58a Mon Sep 17 00:00:00 2001 From: Avery Date: Thu, 13 Mar 2025 22:07:44 +0100 Subject: [PATCH] Repl --- src/exec/mod.rs | 4 +-- src/lib.rs | 13 +++++--- src/main.rs | 81 +++++++++++++++++++++++++++++++++++++++++++++- src/parse/mod.rs | 6 ++-- src/parse/sexpr.rs | 4 +-- 5 files changed, 95 insertions(+), 13 deletions(-) diff --git a/src/exec/mod.rs b/src/exec/mod.rs index bb7ea8f..3ef9bc7 100644 --- a/src/exec/mod.rs +++ b/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, diff --git a/src/lib.rs b/src/lib.rs index 3ae9143..07fc847 100644 --- a/src/lib.rs +++ b/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, Box), // 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), // \0:1.2 Application(Box, Box), // 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}"), } diff --git a/src/main.rs b/src/main.rs index f328e4d..fee1d16 100644 --- a/src/main.rs +++ b/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(); + } +} diff --git a/src/parse/mod.rs b/src/parse/mod.rs index dec9d64..65edc05 100644 --- a/src/parse/mod.rs +++ b/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 { } } -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 { +pub fn parse_type(ast: &Sexpr) -> Result { match ast { Sexpr::Symbol(s) => parse_prim_type(s), Sexpr::List(sexprs) => parse_type_list(sexprs), diff --git a/src/parse/sexpr.rs b/src/parse/sexpr.rs index 933cd10..60d0110 100644 --- a/src/parse/sexpr.rs +++ b/src/parse/sexpr.rs @@ -34,7 +34,7 @@ impl Sexpr { } } -pub fn tokenize(input: &str) -> Vec { +fn tokenize(input: &str) -> Vec { 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>) -> Result) -> Result { +fn parse(tokens: Vec) -> Result { let mut tokens = tokens.into_iter().peekable(); let ast = parse_expr(&mut tokens)?; if tokens.peek().is_some() {