make type inference work-ish

This commit is contained in:
NotAFile 2022-02-20 20:12:35 +01:00
parent cce8a3bde4
commit c0f6b5c4be
2 changed files with 76 additions and 16 deletions

View File

@ -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
}
}
}

View File

@ -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, "?: ")?,