diff options
Diffstat (limited to 'src')
| -rw-r--r-- | src/ast.rs | 55 | ||||
| -rw-r--r-- | src/classes.rs | 3 | ||||
| -rw-r--r-- | src/effects.rs | 19 | ||||
| -rw-r--r-- | src/main.rs | 51 | ||||
| -rw-r--r-- | src/parser.rs | 6 | ||||
| -rw-r--r-- | src/simple.rs | 50 |
6 files changed, 184 insertions, 0 deletions
diff --git a/src/ast.rs b/src/ast.rs new file mode 100644 index 0000000..9202968 --- /dev/null +++ b/src/ast.rs @@ -0,0 +1,55 @@ +// Bidirectional type checking, simple types for effects (or perhaps subtyping?) and typeclasses + +use core::fmt; +use std::collections::HashMap; + +pub type Identifier = String; +pub type Context = HashMap<Identifier, Term>; + +// note: when comes the time, we'll put effects in here (i think) +#[derive(Clone, PartialEq, Eq)] +pub enum Expression { + Annotation{expr: Box<Expression>, kind: Type}, + Constant{term: Term}, + Variable{id: Identifier}, + Abstraction{param: Identifier, func: Box<Expression>}, + Application{func: Box<Expression>, arg: Box<Expression>}, + Conditional{if_cond: Box<Expression>, if_then: Box<Expression>, if_else: Box<Expression>} +} + +// _every_ type in our language is represented as this and interpreted as a type. +// how to store more data than fits... hmm +pub type Value = i8; + +#[derive(Debug, Copy, Clone, PartialEq, Eq)] +pub enum Type { + Empty, + Unit, + Bool, + Natural, + // Float, + // String, + // Enum(Vec<Type>), + // Record(Vec<Type>), + // Function{from: Box<Type>, to: Box<Type>}, +} + +// this means that functions cannot have types? unless we put them as empty values ig +#[derive(Debug, Copy, Clone, PartialEq, Eq)] +pub struct Term { + pub val: Value, + pub kind: Type, // currently useless / redundant: will be useful for casting +} + +impl fmt::Debug for Expression { + fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result { + match self { + Expression::Annotation { expr, kind } => write!(f, "{:?}:{:?}", expr, kind), + Expression::Constant { term } => write!(f, "{}", term.val), + Expression::Variable { id } => write!(f, "{}", id), + Expression::Abstraction { param, func } => write!(f, "(λ{}.{:?})", param, func), + Expression::Application { func, arg } => write!(f, "{:?} {:?}", func, arg), + Expression::Conditional { if_cond, if_then, if_else } => write!(f, "if {:?} then {:?} else {:?}", if_cond, if_then, if_else), + } + } +} diff --git a/src/classes.rs b/src/classes.rs new file mode 100644 index 0000000..38a4847 --- /dev/null +++ b/src/classes.rs @@ -0,0 +1,3 @@ +// Typeclass pass: monomorphize based on usage, pretty much + + diff --git a/src/effects.rs b/src/effects.rs new file mode 100644 index 0000000..4c4c110 --- /dev/null +++ b/src/effects.rs @@ -0,0 +1,19 @@ +// Simple types for effects + +use crate::ast::*; + +// bad and wrong and useless +pub struct Effection { + expr: Expression, + effect: Effect, +} + +// yeah i'm not dealing with this yet +pub enum Effect { + Empty, + Total, + Exn, + Pure, + IO, +} + diff --git a/src/main.rs b/src/main.rs new file mode 100644 index 0000000..f31e163 --- /dev/null +++ b/src/main.rs @@ -0,0 +1,51 @@ +use std::io::{Write, stdout, stdin}; +use crate::ast::*; + +mod ast; +mod classes; +mod effects; +mod parser; +mod simple; + +fn main() { + println!("type-systems"); + let mut input = String::new(); + loop { + println!("infer, check, or execute? (i/c/e)"); + print!("\x1b[1m==> \x1b[22m"); + stdout().flush().unwrap(); + + input.clear(); + stdin().read_line(&mut input).unwrap(); + match input.trim() { + "i" | "g" | "infer" => { + println!("enter partially annotated expression to fully infer"); + print!("\x1b[1m====> \x1b[22m"); + stdout().flush().unwrap(); + + input.clear(); + stdin().read_line(&mut input).unwrap(); + simple::infer(Context::new(), parser::parse(&input)); + }, + "c" | "t" | "check" | "typecheck" => { + println!("enter fully annotated expression to typecheck"); + print!("\x1b[1m====> \x1b[22m"); + stdout().flush().unwrap(); + + input.clear(); + stdin().read_line(&mut input).unwrap(); + simple::check(Context::new(), parser::parse(&input)); + }, + "e" | "r" | "execute" | "run" => { + println!("enter expression to execute"); + print!("\x1b[1m====> \x1b[22m"); + stdout().flush().unwrap(); + + input.clear(); + stdin().read_line(&mut input).unwrap(); + simple::execute(Context::new(), parser::parse(&input)); + }, + _ => println!("invalid option {}. please try again.", input.trim()) + } + } +} diff --git a/src/parser.rs b/src/parser.rs new file mode 100644 index 0000000..3223619 --- /dev/null +++ b/src/parser.rs @@ -0,0 +1,6 @@ +use crate::ast::*; + +pub fn parse(input: &str) -> Expression { + let input = input.trim(); + todo!(); +} diff --git a/src/simple.rs b/src/simple.rs new file mode 100644 index 0000000..f71da46 --- /dev/null +++ b/src/simple.rs @@ -0,0 +1,50 @@ +// Simple bidirectional type checking + +use crate::ast::*; + +pub fn infer(context: Context, expression: Expression) { + todo!(); +} + +pub fn check(context: Context, expression: Expression) { + todo!(); +} + +/// Evaluates an expression given a context (of variables) to a term. +/// Panics on non-evaluatable code. +pub fn execute(context: Context, expression: Expression) -> Term { + match expression { + Expression::Annotation { expr, .. } => return execute(context, *expr), + Expression::Constant { term } => return term, + Expression::Variable { id } => return context[&id], + Expression::Abstraction { .. } => panic!(), + Expression::Application { func, arg } => { + match *func { + Expression::Abstraction { param, func } => { + let mut context = context; + context.insert(param, execute(context.clone(), *arg)); + return execute(context, *func); + }, + _ => panic!() + } + }, + Expression::Conditional { if_cond, if_then, if_else } => { + match execute(context.clone(), *if_cond).val { + 1 => execute(context, *if_then), + 0 => execute(context, *if_else), + _ => panic!() + } + }, + } +} + +// intentionally small: i want to run into errors +/// assumption: the count is instantiated to zero +fn uniquify(count: &mut u8) -> String { + *count += 1; + if *count == 0 { + panic!("we've overflowed!"); + } else { + return String::from(format!("{:X}", count)); + } +} |