Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

special handling for Completion/NormalCompletion in the typechecker #613

Merged
merged 3 commits into from
Sep 22, 2024
Merged

special handling for Completion/NormalCompletion in the typechecker #613

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
3 commits
Select commit Hold shift + click to select a range
53462ac
special handling for Completion/NormalCompletion
bakkot Sep 17, 2024
bdacf63
conver argument length test to assert
bakkot Sep 18, 2024
a9e4793
add a test
bakkot Sep 18, 2024
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
56 changes: 48 additions & 8 deletions src/type-logic.ts
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -207,11 +207,15 @@ export function meet(a: Type, b: Type): Type {
// union is join. meet distributes over join.
return a.of.map(t => meet(t, b)).reduce(join);
}
if (
(a.kind === 'list' && b.kind === 'list') ||
(a.kind === 'normal completion' && b.kind === 'normal completion')
) {
return { kind: a.kind, of: meet(a.of, b.of) };
if (a.kind === 'list' && b.kind === 'list') {
return { kind: 'list', of: meet(a.of, b.of) };
}
if (a.kind === 'normal completion' && b.kind === 'normal completion') {
const inner = meet(a.of, b.of);
if (inner.kind === 'never') {
return { kind: 'never' };
}
michaelficarra marked this conversation as resolved.
Show resolved Hide resolved
return { kind: 'normal completion', of: inner };
}
return { kind: 'never' };
}
Expand Down Expand Up @@ -318,7 +322,11 @@ export function serialize(type: Type): string {
}
}

export function typeFromExpr(expr: Expr, biblio: Biblio): Type {
export function typeFromExpr(
expr: Expr,
biblio: Biblio,
warn: (offset: number, message: string) => void,
): Type {
seq: if (expr.name === 'seq') {
const items = stripWhitespace(expr.items);
if (items.length === 1) {
Expand Down Expand Up @@ -356,7 +364,7 @@ export function typeFromExpr(expr: Expr, biblio: Biblio): Type {
if (items[0]?.name === 'text' && ['!', '?'].includes(items[0].contents.trim())) {
const remaining = stripWhitespace(items.slice(1));
if (remaining.length === 1 && ['call', 'sdo-call'].includes(remaining[0].name)) {
const callType = typeFromExpr(remaining[0], biblio);
const callType = typeFromExpr(remaining[0], biblio, warn);
if (isCompletion(callType)) {
const normal: Type =
callType.kind === 'normal completion'
Expand Down Expand Up @@ -384,7 +392,7 @@ export function typeFromExpr(expr: Expr, biblio: Biblio): Type {
case 'list': {
return {
kind: 'list',
of: expr.elements.map(t => typeFromExpr(t, biblio)).reduce(join, { kind: 'never' }),
of: expr.elements.map(t => typeFromExpr(t, biblio, warn)).reduce(join, { kind: 'never' }),
};
}
case 'record': {
Expand All @@ -398,6 +406,37 @@ export function typeFromExpr(expr: Expr, biblio: Biblio): Type {
}
const calleeName = callee[0].contents;

// special case: `Completion` is identity on completions
if (expr.name === 'call' && calleeName === 'Completion') {
if (expr.arguments.length === 1) {
const inner = typeFromExpr(expr.arguments[0], biblio, warn);
if (!isCompletion(inner)) {
// probably unknown, we might as well refine to "some completion"
return {
kind: 'union',
of: [
{ kind: 'normal completion', of: { kind: 'unknown' } },
{ kind: 'abrupt completion' },
],
};
}
} else {
warn(expr.location.start.offset, 'expected Completion to be passed exactly one argument');
}
}

// special case: `NormalCompletion` wraps its input
if (expr.name === 'call' && calleeName === 'NormalCompletion') {
if (expr.arguments.length === 1) {
return { kind: 'normal completion', of: typeFromExpr(expr.arguments[0], biblio, warn) };
} else {
warn(
expr.location.start.offset,
'expected NormalCompletion to be passed exactly one argument',
);
}
}

const biblioEntry = biblio.byAoid(calleeName);
if (biblioEntry?.signature?.return == null) {
break;
Expand Down Expand Up @@ -433,6 +472,7 @@ export function typeFromExpr(expr: Expr, biblio: Biblio): Type {
}
return { kind: 'unknown' };
}

export function typeFromExprType(type: BiblioType): Type {
switch (type.kind) {
case 'union': {
Expand Down
2 changes: 1 addition & 1 deletion src/typechecker.ts
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -74,7 +74,7 @@ const getExpressionVisitor =
const params = signature.parameters.concat(signature.optionalParameters);
for (const [arg, param] of zip(args, params, true)) {
if (param.type == null) continue;
const argType = typeFromExpr(arg, spec.biblio);
const argType = typeFromExpr(arg, spec.biblio, warn);
const paramType = typeFromExprType(param.type);

// often we can't infer the argument precisely, so we check only that the intersection is nonempty rather than that the argument type is a subtype of the parameter type
Expand Down
94 changes: 92 additions & 2 deletions test/typecheck.js
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -1511,7 +1511,7 @@ describe('type system', () => {
await assertTypeError(
'an ECMAScript language value',
'NormalCompletion(42)',
'argument type (a normal completion) does not look plausibly assignable to parameter type (ECMAScript language value)',
'argument type (a normal completion containing 42) does not look plausibly assignable to parameter type (ECMAScript language value)',
[completionBiblio],
);

Expand All @@ -1535,7 +1535,14 @@ describe('type system', () => {
await assertTypeError(
'a Boolean',
'NormalCompletion(*false*)',
'argument type (a normal completion) does not look plausibly assignable to parameter type (Boolean)',
'argument type (a normal completion containing false) does not look plausibly assignable to parameter type (Boolean)',
[completionBiblio],
);

await assertTypeError(
'a normal completion containing a Number',
'NormalCompletion(*false*)',
'argument type (a normal completion containing false) does not look plausibly assignable to parameter type (a normal completion containing Number)',
[completionBiblio],
);

Expand All @@ -1544,6 +1551,13 @@ describe('type system', () => {
'NormalCompletion(*false*)',
[completionBiblio],
);

await assertNoTypeError(
'either a normal completion containing an ECMAScript language value or an abrupt completion',
'NormalCompletion(*false*)',
[completionBiblio],
);

await assertNoTypeError('a Boolean', '! Throwy()', [completionBiblio]);
});

Expand Down Expand Up @@ -1709,3 +1723,79 @@ describe('error location', () => {
);
});
});

describe('special cases', () => {
it('NormalCompletion takes one argument', async () => {
await assertLint(
positioned`
<emu-clause id="sec-normalcompletion" type="abstract operation" aoid="NormalCompletion">
<h1>NormalCompletion ( )</h1>
</emu-clause>

<emu-clause id="takesnormalcompletion" type="abstract operation">
<h1>
TakesCompletion (
_x_: a normal completion or an abrupt completion
): ~unused~
</h1>
<dl class="header">
</dl>
<emu-alg>
1. Do something with _x_.
</emu-alg>
</emu-clause>

<emu-clause id="example" type="abstract operation">
<h1>Example ()</h1>
<dl class="header">
</dl>
<emu-alg>
1. Perform TakesCompletion(${M}NormalCompletion()).
</emu-alg>
</emu-clause>
`,
{
ruleId: 'typecheck',
nodeType: 'emu-alg',
message: 'expected NormalCompletion to be passed exactly one argument',
},
);
});

it('NormalCompletion takes one argument', async () => {
await assertLint(
positioned`
<emu-clause id="sec-completion" type="abstract operation" aoid="Completion">
<h1>Completion ( )</h1>
</emu-clause>

<emu-clause id="takesnormalcompletion" type="abstract operation">
<h1>
TakesCompletion (
_x_: a normal completion or an abrupt completion
): ~unused~
</h1>
<dl class="header">
</dl>
<emu-alg>
1. Do something with _x_.
</emu-alg>
</emu-clause>

<emu-clause id="example" type="abstract operation">
<h1>Example ()</h1>
<dl class="header">
</dl>
<emu-alg>
1. Perform TakesCompletion(${M}Completion()).
</emu-alg>
</emu-clause>
`,
{
ruleId: 'typecheck',
nodeType: 'emu-alg',
message: 'expected Completion to be passed exactly one argument',
},
);
});
});
Loading