Skip to content

Commit

Permalink
add attribute for skipping return checks
Browse files Browse the repository at this point in the history
  • Loading branch information
bakkot committed Sep 17, 2024
1 parent 808287b commit 36b9f1c
Show file tree
Hide file tree
Showing 6 changed files with 81 additions and 4 deletions.
1 change: 1 addition & 0 deletions spec/index.html
Original file line number Diff line number Diff line change
Expand Up @@ -212,6 +212,7 @@ <h1>Structured Headers</h1>
<li><b>for:</b> The type of value to which a clause of type "concrete method" or "internal method" applies.</li>
<li><b>redefinition:</b> If "true", the name of the operation will not automatically link (i.e., it will not automatically be given an aoid).</li>
<li><b>skip global checks:</b> If "true", disables consistency checks for this AO which require knowing every callsite.</li>
<li><b>skip return checks:</b> If "true", disables checking that the returned values from this AO correspond to its declared return type.</li>
</ul>
</li>
</ol>
Expand Down
9 changes: 6 additions & 3 deletions src/Biblio.ts
Original file line number Diff line number Diff line change
Expand Up @@ -271,8 +271,10 @@ export default class Biblio {
delete copy.location;
// @ts-ignore
delete copy.referencingIds;
// @ts-ignore
delete copy._node;
for (const key of Object.keys(copy)) {
// @ts-ignore
if (key.startsWith('_')) delete copy[key];
}
return copy;
}),
};
Expand Down Expand Up @@ -344,6 +346,7 @@ export interface AlgorithmBiblioEntry extends BiblioEntryBase {
signature: null | Signature;
effects: string[];
skipGlobalChecks?: boolean;
/** @internal*/ _skipReturnChecks?: boolean;
/** @internal*/ _node?: Element;
}

Expand Down Expand Up @@ -398,7 +401,7 @@ export type PartialBiblioEntry = Unkey<BiblioEntry, NonExportedKeys>;

export type ExportedBiblio = {
location: string;
entries: PartialBiblioEntry[];
entries: Unkey<PartialBiblioEntry, `_${string}`>[];
};

function dumpEnv(env: EnvRec) {
Expand Down
5 changes: 5 additions & 0 deletions src/Clause.ts
Original file line number Diff line number Diff line change
Expand Up @@ -55,6 +55,7 @@ export default class Clause extends Builder {
/** @internal */ readonly effects: string[]; // this is held by identity and mutated by Spec.ts
/** @internal */ signature: Signature | null;
/** @internal */ skipGlobalChecks: boolean;
/** @internal */ skipReturnChecks: boolean;

constructor(spec: Spec, node: HTMLElement, parent: Clause, number: string) {
super(spec, node);
Expand All @@ -67,6 +68,7 @@ export default class Clause extends Builder {
this.examples = [];
this.effects = [];
this.skipGlobalChecks = false;
this.skipReturnChecks = false;

// namespace is either the entire spec or the parent clause's namespace.
let parentNamespace = spec.namespace;
Expand Down Expand Up @@ -206,6 +208,7 @@ export default class Clause extends Builder {
effects,
redefinition,
skipGlobalChecks,
skipReturnChecks,
} = parseStructuredHeaderDl(this.spec, type, dl);

const paras = formatPreamble(
Expand Down Expand Up @@ -237,6 +240,7 @@ export default class Clause extends Builder {
}

this.skipGlobalChecks = skipGlobalChecks;
this.skipReturnChecks = skipReturnChecks;

this.effects.push(...effects);
for (const effect of effects) {
Expand Down Expand Up @@ -373,6 +377,7 @@ export default class Clause extends Builder {
signature,
effects: clause.effects,
_node: clause.node,
_skipReturnChecks: clause.skipReturnChecks,
};
if (clause.skipGlobalChecks) {
op.skipGlobalChecks = true;
Expand Down
32 changes: 32 additions & 0 deletions src/header-parser.ts
Original file line number Diff line number Diff line change
Expand Up @@ -407,12 +407,14 @@ export function parseStructuredHeaderDl(
effects: string[];
redefinition: boolean;
skipGlobalChecks: boolean;
skipReturnChecks: boolean;
} {
let description = null;
let _for = null;
let redefinition: boolean | null = null;
let effects: string[] = [];
let skipGlobalChecks: boolean | null = null;
let skipReturnChecks: boolean | null = null;
for (let i = 0; i < dl.children.length; ++i) {
const dt = dl.children[i];
if (dt.tagName !== 'DT') {
Expand Down Expand Up @@ -482,6 +484,7 @@ export function parseStructuredHeaderDl(
}
break;
}
// TODO figure out how to de-dupe the code for boolean attributes
case 'redefinition': {
if (redefinition != null) {
spec.warn({
Expand Down Expand Up @@ -538,6 +541,34 @@ export function parseStructuredHeaderDl(
}
break;
}
case 'skip return checks': {
if (skipReturnChecks != null) {
spec.warn({
type: 'node',
ruleId: 'header-format',
message: `duplicate "skip return checks" attribute`,
node: dt,
});
}
const contents = (dd.textContent ?? '').trim();
if (contents === 'true') {
skipReturnChecks = true;
} else if (contents === 'false') {
skipReturnChecks = false;
} else {
spec.warn({
type: 'contents',
ruleId: 'header-format',
message: `unknown value for "skip return checks" attribute (expected "true" or "false", got ${JSON.stringify(
contents,
)})`,
node: dd,
nodeRelativeLine: 1,
nodeRelativeColumn: 1,
});
}
break;
}
case '': {
spec.warn({
type: 'node',
Expand All @@ -564,6 +595,7 @@ export function parseStructuredHeaderDl(
effects,
redefinition: redefinition ?? false,
skipGlobalChecks: skipGlobalChecks ?? false,
skipReturnChecks: skipReturnChecks ?? false,
};
}

Expand Down
5 changes: 4 additions & 1 deletion src/typechecker.ts
Original file line number Diff line number Diff line change
Expand Up @@ -275,7 +275,10 @@ export function typecheck(spec: Spec) {
)
? null
: false;
const returnType = signature?.return == null ? null : typeFromExprType(signature.return);
const returnType =
biblioEntry?._skipReturnChecks || signature?.return == null
? null
: typeFromExprType(signature.return);
let numberOfAbstractClosuresWeAreWithin = 0;
const walkLines = (list: OrderedListNode) => {
for (const line of list.contents) {
Expand Down
33 changes: 33 additions & 0 deletions test/typecheck.js
Original file line number Diff line number Diff line change
Expand Up @@ -598,6 +598,39 @@ describe('typechecking completions', () => {
</emu-alg>
</emu-clause>
`);

await assertLintFree(`
<emu-clause id="sec-completion-ao" type="abstract operation">
<h1>
Completion (
_completionRecord_: a Completion Record,
): a Completion Record
</h1>
<dl class="header">
<dt>skip return checks</dt>
<dd>true</dd>
</dl>
<emu-alg>
1. Assert: _completionRecord_ is a Completion Record.
1. Return _completionRecord_.
</emu-alg>
</emu-clause>
<emu-clause id="sec-normalcompletion" type="abstract operation">
<h1>
NormalCompletion (
_value_: any value except a Completion Record,
): a normal completion
</h1>
<dl class="header">
<dt>skip return checks</dt>
<dd>true</dd>
</dl>
<emu-alg>
1. Return Completion Record { [[Type]]: ~normal~, [[Value]]: _value_, [[Target]]: ~empty~ }.
</emu-alg>
</emu-clause>
`);
});
});

Expand Down

0 comments on commit 36b9f1c

Please sign in to comment.