diff --git a/src/frontend.rs b/src/frontend.rs index ea77959..bb30c14 100644 --- a/src/frontend.rs +++ b/src/frontend.rs @@ -297,18 +297,46 @@ impl Context { } => { let args_typed: Vec<_> = args.iter().map(|ex| self.infer_expr_types(ex)).collect(); let callee_def = self.callables.get(*called); - if self.types.is_fully_typed(callee_def.ret_type) { - expr.clone().with_type(callee_def.ret_type) - } else { - let param_types: Vec<_> = callee_def.args.iter().map(|param| param.1).collect(); - let mut genargs = callee_def.genargs.clone(); - let inferred_args: Vec<_> = param_types - .iter() - .zip(args_typed) - .map(|(param, arg)| self.types.infer_type(*param, arg.typ)) - .collect(); - expr.clone().with_type(callee_def.ret_type) + + let param_types: Vec<_> = callee_def.args.iter().map(|param| param.1).collect(); + let inferred_args: Vec<_> = param_types + .iter() + .zip(&args_typed) + .map(|(param, arg)| self.types.infer_type(*param, arg.typ)) + .collect(); + + let mut genargs: Vec<_> = callee_def.genargs.iter().map(|a| a.1).collect(); + + let mut new_type = callee_def.ret_type; + + if genargs.len() != 0 { + // need to infer generic arguments + for inf_res in inferred_args { + match inf_res { + types::InferenceResult::First(_) => todo!(), + types::InferenceResult::Second(_) => todo!(), + types::InferenceResult::TypeVar(dbi, tvar, typ) => { + assert_eq!(dbi, 0); + // TODO: type check argument instead of just using it + genargs[tvar as usize] = typ; + } + types::InferenceResult::Incompatible => todo!(), + types::InferenceResult::Ambigous => todo!(), + } + } + + // TODO: HACKY HACKY HACK + new_type = genargs[0]; } + + let mut new_expr = expr.clone(); + new_expr.typ = new_type; + new_expr.kind = typed_ir::ExprKind::Call { + called: called.clone(), + args: args_typed, + genargs, + }; + new_expr } } } diff --git a/src/frontend/types.rs b/src/frontend/types.rs index b791c4a..9690d32 100644 --- a/src/frontend/types.rs +++ b/src/frontend/types.rs @@ -74,6 +74,20 @@ pub enum GenericArg { Type(Type), } +#[derive(Debug)] +pub enum InferenceResult { + /// The first type was inferred + First(Type), + /// The second type was inferred + Second(Type), + /// A typevar was inferred + TypeVar(u32, u32, Type), + /// The types were incompatible + Incompatible, + /// Neither of the types were complete + Ambigous, +} + pub struct PrimitiveTypes { pub elabnum: Type, pub logic: Type, @@ -173,15 +187,28 @@ impl TypingContext { } /// Given the type of a variable in two locations, infer what the true type should be - pub fn infer_type(&mut self, typ_a: Type, typ_b: Type) -> Type { + pub fn infer_type(&mut self, typ_a: Type, typ_b: Type) -> InferenceResult { match (&self.get(typ_a).kind, &self.get(typ_b).kind) { - (a, b) => panic!("cannot infer between: {:?}, {:?}", a, b), + (TypeKind::TypeVar(dbi, tvar), _) => InferenceResult::TypeVar(*dbi, *tvar, typ_b), + (_, TypeKind::TypeVar(dbi, tvar)) => InferenceResult::TypeVar(*dbi, *tvar, typ_a), + (a, b) => { + let a_full = self.is_fully_typed_kind(a); + let b_full = self.is_fully_typed_kind(b); + if a_full && b_full { + InferenceResult::Incompatible + } else if a_full && !b_full { + InferenceResult::Second(typ_a) + } else if !a_full && b_full { + InferenceResult::First(typ_b) + } else { + InferenceResult::Ambigous + } + } } } - /// return whether the type has no unfilled parameters - pub fn is_fully_typed(&self, typ: Type) -> bool { - match &self.get(typ).kind { + fn is_fully_typed_kind(&self, kind: &TypeKind) -> bool { + match kind { TypeKind::ElabType(_) => todo!(), TypeKind::Logic(data) => { if let ElabValue::Concrete(_) = data.value { @@ -201,6 +228,11 @@ impl TypingContext { } } + /// return whether the type has no unfilled parameters + pub fn is_fully_typed(&self, typ: Type) -> bool { + self.is_fully_typed_kind(&self.get(typ).kind) + } + pub fn pretty_value(&self, w: &mut dyn std::fmt::Write, data: &ElabData) -> std::fmt::Result { match &data.value { ElabValue::Infer => write!(w, "?: ")?,