Skip to content

Commit 9034def

Browse files
purefunctorpurefunctor
committed
Extract utility for application checking
1 parent d1a1b8f commit 9034def

5 files changed

Lines changed: 80 additions & 64 deletions

File tree

‎compiler-core/checking2/src/core/toolkit.rs‎

Lines changed: 24 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -13,6 +13,7 @@ use crate::core::{
1313
CheckedClass, CheckedInstance, CheckedSynonym, ForallBinder, KindOrType, Role, Type, TypeId,
1414
constraint, normalise, unification,
1515
};
16+
use crate::error::ErrorKind;
1617
use crate::state::CheckState;
1718
use crate::{ExternalQueries, safe_loop};
1819

@@ -38,6 +39,29 @@ pub struct DecomposedInstance {
3839
pub arguments: Vec<TypeId>,
3940
}
4041

42+
pub fn report_invalid_type_application<Q>(
43+
state: &mut CheckState,
44+
context: &CheckContext<Q>,
45+
function_type: TypeId,
46+
function_kind: TypeId,
47+
argument_type: TypeId,
48+
) -> QueryResult<()>
49+
where
50+
Q: ExternalQueries,
51+
{
52+
let function_type = state.pretty_id(context, function_type)?;
53+
let function_kind = state.pretty_id(context, function_kind)?;
54+
let argument_type = state.pretty_id(context, argument_type)?;
55+
56+
state.insert_error(ErrorKind::InvalidTypeApplication {
57+
function_type,
58+
function_kind,
59+
argument_type,
60+
});
61+
62+
Ok(())
63+
}
64+
4165
pub fn extract_type_application<Q>(
4266
state: &mut CheckState,
4367
context: &CheckContext<Q>,

‎compiler-core/checking2/src/source/operator.rs‎

Lines changed: 16 additions & 19 deletions
Original file line numberDiff line numberDiff line change
@@ -10,10 +10,9 @@ use sugar::bracketing::BracketingResult;
1010
use crate::context::CheckContext;
1111
use crate::core::substitute::SubstituteName;
1212
use crate::core::{Type, TypeId, normalise, toolkit, unification};
13-
use crate::error::ErrorKind;
1413
use crate::source::{binder, synonym, terms, types};
1514
use crate::state::CheckState;
16-
use crate::{ExternalQueries, OperatorBranchTypes};
15+
use crate::{ExternalQueries, OperatorBranchTypes, safe_loop};
1716

1817
#[derive(Copy, Clone, Debug)]
1918
enum OperatorKindMode {
@@ -479,9 +478,8 @@ fn apply_type_argument<Q>(
479478
where
480479
Q: ExternalQueries,
481480
{
482-
loop {
481+
safe_loop! {
483482
function_kind = normalise::normalise(state, context, function_kind)?;
484-
485483
match context.lookup_type(function_kind) {
486484
Type::Function(expected_kind, result_kind) => {
487485
unification::subtype(state, context, argument_kind, expected_kind)?;
@@ -491,10 +489,10 @@ where
491489
}
492490

493491
Type::Unification(unification_id) => {
494-
let result_u = state.fresh_unification(context.queries, context.prim.t);
495-
let function_u = context.intern_function(argument_kind, result_u);
496-
unification::solve(state, context, function_kind, unification_id, function_u)?;
497-
function_kind = result_u;
492+
let result_kind = state.fresh_unification(context.queries, context.prim.t);
493+
let function_type = context.intern_function(argument_kind, result_kind);
494+
unification::solve(state, context, function_kind, unification_id, function_type)?;
495+
function_kind = result_kind;
498496
}
499497

500498
Type::Forall(binder_id, inner_kind) => {
@@ -507,17 +505,16 @@ where
507505
}
508506

509507
_ => {
510-
let invalid = context.intern_application(function_type, argument_type);
511-
let function_type_message = state.pretty_id(context, function_type)?;
512-
let function_kind_message = state.pretty_id(context, function_kind)?;
513-
let argument_type_message = state.pretty_id(context, argument_type)?;
514-
state.insert_error(ErrorKind::InvalidTypeApplication {
515-
function_type: function_type_message,
516-
function_kind: function_kind_message,
517-
argument_type: argument_type_message,
518-
});
519-
let unknown = context.unknown("cannot apply operator type");
520-
return Ok((invalid, unknown));
508+
let invalid_type = context.intern_application(function_type, argument_type);
509+
toolkit::report_invalid_type_application(
510+
state,
511+
context,
512+
function_type,
513+
function_kind,
514+
argument_type,
515+
)?;
516+
let unknown_kind = context.unknown("cannot apply operator type");
517+
return Ok((invalid_type, unknown_kind));
521518
}
522519
}
523520
}

‎compiler-core/checking2/src/source/synonym.rs‎

Lines changed: 18 additions & 21 deletions
Original file line numberDiff line numberDiff line change
@@ -278,46 +278,47 @@ where
278278
Q: ExternalQueries,
279279
{
280280
match context.lookup_type(function_kind) {
281-
Type::Function(function_argument, function_result) => {
281+
Type::Function(expected_kind, result_kind) => {
282282
let argument_type = match argument {
283283
Argument::Syntax(argument_id) => {
284284
let (argument_type, _) =
285-
types::check_kind(state, context, argument_id, function_argument)?;
285+
types::check_kind(state, context, argument_id, expected_kind)?;
286286
argument_type
287287
}
288288
Argument::Core(argument_type, argument_kind) => {
289-
unification::subtype(state, context, argument_kind, function_argument)?;
289+
unification::subtype(state, context, argument_kind, expected_kind)?;
290290
argument_type
291291
}
292292
};
293293

294294
let result_type = context.intern_application(function_type, argument_type);
295-
let result_kind = normalise::normalise(state, context, function_result)?;
295+
let result_kind = normalise::normalise(state, context, result_kind)?;
296296

297297
applications.push(KindOrType::Type(argument_type));
298298
Ok(ControlFlow::Break((result_type, result_kind)))
299299
}
300300

301301
Type::Unification(unification_id) => {
302-
let function_argument = state.fresh_unification(context.queries, context.prim.t);
303-
let function_result = state.fresh_unification(context.queries, context.prim.t);
304-
let function = context.intern_function(function_argument, function_result);
302+
let argument_kind = state.fresh_unification(context.queries, context.prim.t);
303+
let result_kind = state.fresh_unification(context.queries, context.prim.t);
304+
305+
let function = context.intern_function(argument_kind, result_kind);
305306
unification::solve(state, context, function_kind, unification_id, function)?;
306307

307308
let argument_type = match argument {
308309
Argument::Syntax(argument_id) => {
309310
let (argument_type, _) =
310-
types::check_kind(state, context, argument_id, function_argument)?;
311+
types::check_kind(state, context, argument_id, argument_kind)?;
311312
argument_type
312313
}
313314
Argument::Core(argument_type, checked_kind) => {
314-
unification::subtype(state, context, checked_kind, function_argument)?;
315+
unification::subtype(state, context, checked_kind, argument_kind)?;
315316
argument_type
316317
}
317318
};
318319

319320
let result_type = context.intern_application(function_type, argument_type);
320-
let result_kind = normalise::normalise(state, context, function_result)?;
321+
let result_kind = normalise::normalise(state, context, result_kind)?;
321322

322323
applications.push(KindOrType::Type(argument_type));
323324
Ok(ControlFlow::Break((result_type, result_kind)))
@@ -349,17 +350,13 @@ where
349350
let invalid_type = context.intern_application(function_type, argument_type);
350351
let unknown_kind = context.unknown("cannot apply synonym type");
351352

352-
{
353-
let function_type = state.pretty_id(context, function_type)?;
354-
let function_kind = state.pretty_id(context, function_kind)?;
355-
let argument_type = state.pretty_id(context, argument_type)?;
356-
357-
state.insert_error(ErrorKind::InvalidTypeApplication {
358-
function_type,
359-
function_kind,
360-
argument_type,
361-
});
362-
}
353+
toolkit::report_invalid_type_application(
354+
state,
355+
context,
356+
function_type,
357+
function_kind,
358+
argument_type,
359+
)?;
363360

364361
applications.push(KindOrType::Type(argument_type));
365362
Ok(ControlFlow::Break((invalid_type, unknown_kind)))

‎compiler-core/checking2/src/source/terms/application.rs‎

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -143,7 +143,7 @@ where
143143
pub fn check_function_application<Q>(
144144
state: &mut CheckState,
145145
context: &CheckContext<Q>,
146-
function_t: TypeId,
146+
function_type: TypeId,
147147
argument: &lowering::ExpressionArgument,
148148
) -> QueryResult<TypeId>
149149
where
@@ -154,13 +154,13 @@ where
154154
let Some(type_argument) = type_argument else {
155155
return Ok(context.unknown("missing type argument"));
156156
};
157-
check_function_type_application(state, context, function_t, *type_argument)
157+
check_function_type_application(state, context, function_type, *type_argument)
158158
}
159159
lowering::ExpressionArgument::Term(term_argument) => {
160160
let Some(term_argument) = term_argument else {
161161
return Ok(context.unknown("missing term argument"));
162162
};
163-
check_function_term_application(state, context, function_t, *term_argument)
163+
check_function_term_application(state, context, function_type, *term_argument)
164164
}
165165
}
166166
}

‎compiler-core/checking2/src/source/types.rs‎

Lines changed: 19 additions & 21 deletions
Original file line numberDiff line numberDiff line change
@@ -10,7 +10,7 @@ use crate::core::substitute::SubstituteName;
1010
use crate::core::{
1111
ForallBinder, KindOrType, RowField, RowType, Type, TypeId, normalise, toolkit, unification,
1212
};
13-
use crate::error::{ErrorCrumb, ErrorKind};
13+
use crate::error::ErrorCrumb;
1414
use crate::source::{operator, synonym};
1515
use crate::state::CheckState;
1616
use crate::{ExternalQueries, safe_loop};
@@ -394,25 +394,25 @@ where
394394
Type::Function(argument_kind, result_kind) => {
395395
let (argument_type, _) = check_kind(state, context, argument, argument_kind)?;
396396

397-
let t = context.intern_application(function_type, argument_type);
398-
let k = normalise::normalise(state, context, result_kind)?;
397+
let result_type = context.intern_application(function_type, argument_type);
398+
let result_kind = normalise::normalise(state, context, result_kind)?;
399399

400-
Ok((t, k))
400+
Ok((result_type, result_kind))
401401
}
402402

403403
Type::Unification(unification_id) => {
404-
let argument_u = state.fresh_unification(context.queries, context.prim.t);
405-
let result_u = state.fresh_unification(context.queries, context.prim.t);
404+
let argument_kind = state.fresh_unification(context.queries, context.prim.t);
405+
let result_kind = state.fresh_unification(context.queries, context.prim.t);
406406

407-
let function_u = context.intern_function(argument_u, result_u);
408-
unification::solve(state, context, function_kind, unification_id, function_u)?;
407+
let function = context.intern_function(argument_kind, result_kind);
408+
unification::solve(state, context, function_kind, unification_id, function)?;
409409

410-
let (argument_type, _) = check_kind(state, context, argument, argument_u)?;
410+
let (argument_type, _) = check_kind(state, context, argument, argument_kind)?;
411411

412-
let t = context.intern_application(function_type, argument_type);
413-
let k = normalise::normalise(state, context, result_u)?;
412+
let result_type = context.intern_application(function_type, argument_type);
413+
let result_kind = normalise::normalise(state, context, result_kind)?;
414414

415-
Ok((t, k))
415+
Ok((result_type, result_kind))
416416
}
417417

418418
Type::Forall(binder_id, inner_kind) => {
@@ -433,20 +433,18 @@ where
433433
// this ensures that implicit variables are bound.
434434
let (argument_type, _) = infer_kind(state, context, argument)?;
435435

436-
let t = context.intern_application(function_type, argument_type);
437-
let k = context.unknown("cannot apply function type");
436+
let result_type = context.intern_application(function_type, argument_type);
437+
let result_kind = context.unknown("cannot apply function type");
438438

439-
let function_type = state.pretty_id(context, function_type)?;
440-
let function_kind = state.pretty_id(context, function_kind)?;
441-
let argument_type = state.pretty_id(context, argument_type)?;
442-
443-
state.insert_error(ErrorKind::InvalidTypeApplication {
439+
toolkit::report_invalid_type_application(
440+
state,
441+
context,
444442
function_type,
445443
function_kind,
446444
argument_type,
447-
});
445+
)?;
448446

449-
Ok((t, k))
447+
Ok((result_type, result_kind))
450448
}
451449
}
452450
}

0 commit comments

Comments
 (0)