From 36b9f1cb15a27a5c3c0d8a75766284f200097c02 Mon Sep 17 00:00:00 2001 From: Kevin Gibbons Date: Tue, 17 Sep 2024 09:03:01 -0700 Subject: [PATCH] add attribute for skipping return checks --- spec/index.html | 1 + src/Biblio.ts | 9 ++++++--- src/Clause.ts | 5 +++++ src/header-parser.ts | 32 ++++++++++++++++++++++++++++++++ src/typechecker.ts | 5 ++++- test/typecheck.js | 33 +++++++++++++++++++++++++++++++++ 6 files changed, 81 insertions(+), 4 deletions(-) diff --git a/spec/index.html b/spec/index.html index 8c0398d7..25821852 100644 --- a/spec/index.html +++ b/spec/index.html @@ -212,6 +212,7 @@

Structured Headers

  • for: The type of value to which a clause of type "concrete method" or "internal method" applies.
  • redefinition: If "true", the name of the operation will not automatically link (i.e., it will not automatically be given an aoid).
  • skip global checks: If "true", disables consistency checks for this AO which require knowing every callsite.
    • +
  • skip return checks: If "true", disables checking that the returned values from this AO correspond to its declared return type.
    • diff --git a/src/Biblio.ts b/src/Biblio.ts index 0994ba2c..a6e6c192 100644 --- a/src/Biblio.ts +++ b/src/Biblio.ts @@ -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; }), }; @@ -344,6 +346,7 @@ export interface AlgorithmBiblioEntry extends BiblioEntryBase { signature: null | Signature; effects: string[]; skipGlobalChecks?: boolean; + /** @internal*/ _skipReturnChecks?: boolean; /** @internal*/ _node?: Element; } @@ -398,7 +401,7 @@ export type PartialBiblioEntry = Unkey; export type ExportedBiblio = { location: string; - entries: PartialBiblioEntry[]; + entries: Unkey[]; }; function dumpEnv(env: EnvRec) { diff --git a/src/Clause.ts b/src/Clause.ts index 039fd594..a7794f35 100644 --- a/src/Clause.ts +++ b/src/Clause.ts @@ -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); @@ -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; @@ -206,6 +208,7 @@ export default class Clause extends Builder { effects, redefinition, skipGlobalChecks, + skipReturnChecks, } = parseStructuredHeaderDl(this.spec, type, dl); const paras = formatPreamble( @@ -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) { @@ -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; diff --git a/src/header-parser.ts b/src/header-parser.ts index 7195c4c1..66dadbfd 100644 --- a/src/header-parser.ts +++ b/src/header-parser.ts @@ -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') { @@ -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({ @@ -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', @@ -564,6 +595,7 @@ export function parseStructuredHeaderDl( effects, redefinition: redefinition ?? false, skipGlobalChecks: skipGlobalChecks ?? false, + skipReturnChecks: skipReturnChecks ?? false, }; } diff --git a/src/typechecker.ts b/src/typechecker.ts index 31d16400..099282df 100644 --- a/src/typechecker.ts +++ b/src/typechecker.ts @@ -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) { diff --git a/test/typecheck.js b/test/typecheck.js index 702453d2..e60bf631 100644 --- a/test/typecheck.js +++ b/test/typecheck.js @@ -598,6 +598,39 @@ describe('typechecking completions', () => { `); + + await assertLintFree(` + +

    + Completion ( + _completionRecord_: a Completion Record, + ): a Completion Record +

    +
    +
    skip return checks
    +
    true
    +
    + + 1. Assert: _completionRecord_ is a Completion Record. + 1. Return _completionRecord_. + +     + + +

    + NormalCompletion ( + _value_: any value except a Completion Record, + ): a normal completion +

    +
    +
    skip return checks
    +
    true
    +
    + + 1. Return Completion Record { [[Type]]: ~normal~, [[Value]]: _value_, [[Target]]: ~empty~ }. + +     + `); }); });