Skip to content

Commit

Permalink
split completion types in typechecker
Browse files Browse the repository at this point in the history
  • Loading branch information
bakkot committed Sep 17, 2024
1 parent bda4d4c commit 51095be
Show file tree
Hide file tree
Showing 2 changed files with 52 additions and 21 deletions.
67 changes: 49 additions & 18 deletions src/type-logic.ts
Original file line number Diff line number Diff line change
Expand Up @@ -8,7 +8,8 @@ type Type =
| { kind: 'union'; of: NonUnion[] } // constraint: nothing in the union dominates anything else in the union
| { kind: 'list'; of: Type }
| { kind: 'record' } // TODO more precision
| { kind: 'completion'; of: Type }
| { kind: 'normal completion'; of: Type }
| { kind: 'abrupt completion' }
| { kind: 'real' }
| { kind: 'integer' }
| { kind: 'non-negative integer' }
Expand Down Expand Up @@ -50,7 +51,7 @@ const simpleKinds = new Set<Type['kind']>([
const dominateGraph: Partial<Record<Type['kind'], Type['kind'][]>> = {
// @ts-expect-error TS does not know about __proto__
__proto__: null,
record: ['completion'],
record: ['normal completion', 'abrupt completion'],
real: [
'integer',
'non-negative integer',
Expand Down Expand Up @@ -97,7 +98,7 @@ export function dominates(a: Type, b: Type): boolean {
}
if (
(a.kind === 'list' && b.kind === 'list') ||
(a.kind === 'completion' && b.kind === 'completion')
(a.kind === 'normal completion' && b.kind === 'normal completion')
) {
return dominates(a.of, b.of);
}
Expand Down Expand Up @@ -170,7 +171,7 @@ export function join(a: Type, b: Type): Type {
}
if (
(a.kind === 'list' && b.kind === 'list') ||
(a.kind === 'completion' && b.kind === 'completion')
(a.kind === 'normal completion' && b.kind === 'normal completion')
) {
return { kind: a.kind, of: join(a.of, b.of) };
}
Expand All @@ -193,7 +194,7 @@ export function meet(a: Type, b: Type): Type {
}
if (
(a.kind === 'list' && b.kind === 'list') ||
(a.kind === 'completion' && b.kind === 'completion')
(a.kind === 'normal completion' && b.kind === 'normal completion')
) {
return { kind: a.kind, of: meet(a.of, b.of) };
}
Expand Down Expand Up @@ -224,13 +225,16 @@ export function serialize(type: Type): string {
case 'record': {
return 'Record';
}
case 'completion': {
case 'normal completion': {
if (type.of.kind === 'never') {
return 'an abrupt Completion Record';
return 'never';
} else if (type.of.kind === 'unknown') {
return 'a Completion Record';
return 'a normal completion';

This comment has been minimized.

Copy link
@michaelficarra

michaelficarra Sep 18, 2024

Member

We don't use the indefinite article (a/an) in other serialisations. I like it though and would prefer to add it to the others over removing these.

}
return 'a Completion Record normally holding ' + serialize(type.of);
return 'a normal completion containing ' + serialize(type.of);
}
case 'abrupt completion': {
return 'an abrupt completion';
}
case 'real': {
return 'mathematical value';
Expand Down Expand Up @@ -338,8 +342,17 @@ export function typeFromExpr(expr: Expr, biblio: Biblio): Type {
const remaining = stripWhitespace(items.slice(1));
if (remaining.length === 1 && ['call', 'sdo-call'].includes(remaining[0].name)) {
const callType = typeFromExpr(remaining[0], biblio);
if (callType.kind === 'completion') {
return callType.of;
if (isCompletion(callType)) {
const normal: Type =
callType.kind === 'normal completion'
? callType.of
: callType.kind === 'abrupt completion'
? // the expression `? _abrupt_` strictly speaking has type `never`
// however we mostly use `never` to mean user error, so use unknown instead
// this should only ever happen after `Return`
{ kind: 'unknown' }
: callType.of.find(k => k.kind === 'normal completion')?.of ?? { kind: 'unknown' };
return normal;
}
}
}
Expand Down Expand Up @@ -418,15 +431,23 @@ export function typeFromExprType(type: BiblioType): Type {
}
case 'completion': {
if (type.completionType === 'abrupt') {
return { kind: 'completion', of: { kind: 'never' } };
}
return {
kind: 'completion',
of:
return { kind: 'abrupt completion' };
} else {
const normalType: Type =
type.typeOfValueIfNormal == null
? { kind: 'unknown' }
: typeFromExprType(type.typeOfValueIfNormal),
};
: typeFromExprType(type.typeOfValueIfNormal);
if (type.completionType === 'normal') {
return { kind: 'normal completion', of: normalType };
} else if (type.completionType === 'mixed') {
return {
kind: 'union',
of: [{ kind: 'normal completion', of: normalType }, { kind: 'abrupt completion' }],
};
} else {
throw new Error('unreachable: completion kind ' + type.completionType);
}
}
}
case 'opaque': {
const text = type.type;
Expand Down Expand Up @@ -514,6 +535,16 @@ export function typeFromExprType(type: BiblioType): Type {
return { kind: 'unknown' };
}

export function isCompletion(
type: Type,
): type is Type & { kind: 'normal completion' | 'abrupt completion' | 'union' } {
return (
type.kind === 'normal completion' ||
type.kind === 'abrupt completion' ||
(type.kind === 'union' && type.of.some(isCompletion))
);
}

export function stripWhitespace(items: NonSeq[]) {
items = [...items];
while (items[0]?.name === 'text' && /^\s+$/.test(items[0].contents)) {
Expand Down
6 changes: 3 additions & 3 deletions test/typecheck.js
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 Completion Record) does not look plausibly assignable to parameter type (ECMAScript language value)',
'argument type (a normal completion) does not look plausibly assignable to parameter type (ECMAScript language value)',
[completionBiblio],
);

Expand All @@ -1528,14 +1528,14 @@ describe('type system', () => {
await assertTypeError(
'either a normal completion containing a Boolean or an abrupt completion',
'*false*',
'argument (false) does not look plausibly assignable to parameter type (a Completion Record normally holding Boolean)',
'argument (false) does not look plausibly assignable to parameter type (a normal completion containing Boolean or an abrupt completion)',
[completionBiblio],
);

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

Expand Down

0 comments on commit 51095be

Please sign in to comment.