From 36ab465af9ffef468f12dc995ca5a80e56c43431 Mon Sep 17 00:00:00 2001 From: Max DeLiso Date: Sat, 17 May 2025 22:10:37 +0200 Subject: [PATCH 1/2] add a compiler frontend --- bin/ski.ts | 8 +- lib/conversion/converter.ts | 2 +- lib/data/avl/avlNode.ts | 20 ++ lib/index.ts | 4 +- lib/meta/frontend.ts | 5 + lib/meta/frontend/builders.ts | 21 ++ lib/meta/frontend/compilation.ts | 163 +++++++++++ lib/meta/frontend/elaboration.ts | 62 ++++ lib/meta/frontend/externalReferences.ts | 109 +++++++ lib/meta/frontend/predicates.ts | 37 +++ lib/meta/frontend/prettyPrint.ts | 23 ++ lib/meta/frontend/rebuilders.ts | 191 ++++++++++++ lib/meta/frontend/replacers.ts | 31 ++ lib/meta/frontend/substitution.ts | 229 +++++++++++++++ lib/meta/frontend/symbolTable.ts | 59 ++++ lib/meta/frontend/termLevel.ts | 64 ++++ lib/meta/trip.ts | 15 +- lib/parser/systemFType.ts | 8 +- lib/terms/systemF.ts | 14 +- lib/types/systemF.ts | 53 +++- lib/types/typedLambda.ts | 2 +- test/conversion/converter.test.ts | 10 +- test/meta/frontend.test.ts | 274 ++++++++++++++++++ test/meta/frontend/elaboration.test.ts | 221 ++++++++++++++ test/meta/frontend/externalReferences.test.ts | 79 +++++ test/meta/frontend/substitution.test.ts | 144 +++++++++ test/meta/frontend/symbolTable.test.ts | 121 ++++++++ test/meta/inputs/complete.trip | 72 +++++ test/meta/inputs/condSucc.trip | 11 + test/meta/inputs/fact.trip | 13 + test/meta/inputs/fix.trip | 1 + test/meta/inputs/mul.trip | 4 + test/meta/inputs/natBool.trip | 2 + test/meta/inputs/nestedTypeApps.trip | 7 + test/meta/inputs/pair.trip | 7 + test/meta/inputs/pred.trip | 10 + test/meta/inputs/trueFalseZero.trip | 10 + test/parser/tripLang.test.ts | 22 +- test/ski/church.test.ts | 4 +- test/types/typedLambda.test.ts | 10 +- test/util/fileLoader.ts | 7 + 41 files changed, 2090 insertions(+), 59 deletions(-) create mode 100644 lib/meta/frontend.ts create mode 100644 lib/meta/frontend/builders.ts create mode 100644 lib/meta/frontend/compilation.ts create mode 100644 lib/meta/frontend/elaboration.ts create mode 100644 lib/meta/frontend/externalReferences.ts create mode 100644 lib/meta/frontend/predicates.ts create mode 100644 lib/meta/frontend/prettyPrint.ts create mode 100644 lib/meta/frontend/rebuilders.ts create mode 100644 lib/meta/frontend/replacers.ts create mode 100644 lib/meta/frontend/substitution.ts create mode 100644 lib/meta/frontend/symbolTable.ts create mode 100644 lib/meta/frontend/termLevel.ts create mode 100644 test/meta/frontend.test.ts create mode 100644 test/meta/frontend/elaboration.test.ts create mode 100644 test/meta/frontend/externalReferences.test.ts create mode 100644 test/meta/frontend/substitution.test.ts create mode 100644 test/meta/frontend/symbolTable.test.ts create mode 100644 test/meta/inputs/complete.trip create mode 100644 test/meta/inputs/condSucc.trip create mode 100644 test/meta/inputs/fact.trip create mode 100644 test/meta/inputs/fix.trip create mode 100644 test/meta/inputs/mul.trip create mode 100644 test/meta/inputs/natBool.trip create mode 100644 test/meta/inputs/nestedTypeApps.trip create mode 100644 test/meta/inputs/pair.trip create mode 100644 test/meta/inputs/pred.trip create mode 100644 test/meta/inputs/trueFalseZero.trip create mode 100644 test/util/fileLoader.ts diff --git a/bin/ski.ts b/bin/ski.ts index 30dca96..dc2d81d 100755 --- a/bin/ski.ts +++ b/bin/ski.ts @@ -32,7 +32,7 @@ import { prettyPrintSystemFType, typecheckSystemF, // Conversion - convertLambda, + bracketLambda, // Types prettyPrintTy, inferType, @@ -91,13 +91,13 @@ function ensureSKIMode(): boolean { } try { if (currentMode === Mode.Lambda && currentLambda !== null) { - currentSKI = convertLambda(currentLambda); + currentSKI = bracketLambda(currentLambda); } else if (currentMode === Mode.TypedLambda && currentTypedLambda !== null) { const erasedLambda = eraseTypedLambda(currentTypedLambda); if (erasedLambda === null) { throw new Error('failed to erase typed lambda term'); } - currentSKI = convertLambda(erasedLambda); + currentSKI = bracketLambda(erasedLambda); } else if (currentMode === Mode.SystemF && currentSystemF !== null) { const erasedTypedLambda = eraseSystemF(currentSystemF); if (!erasedTypedLambda) { @@ -107,7 +107,7 @@ function ensureSKIMode(): boolean { if (erasedLambda === null) { throw new Error('failed to erase typed lambda term'); } - currentSKI = convertLambda(erasedLambda); + currentSKI = bracketLambda(erasedLambda); } else { throw new Error('current term is null'); } diff --git a/lib/conversion/converter.ts b/lib/conversion/converter.ts index 1eaa14e..b4563a1 100644 --- a/lib/conversion/converter.ts +++ b/lib/conversion/converter.ts @@ -180,7 +180,7 @@ const assertCombinator = (lm: LambdaMixed): SKIExpression => { * Public function. * Converts an untyped lambda expression (UntypedLambda) into an SKI expression. */ -export const convertLambda = (ut: UntypedLambda): SKIExpression => { +export const bracketLambda = (ut: UntypedLambda): SKIExpression => { const lifted = lift(ut); const converted = convertMixed(lifted); return assertCombinator(converted); diff --git a/lib/data/avl/avlNode.ts b/lib/data/avl/avlNode.ts index 4495fc5..d89acc9 100644 --- a/lib/data/avl/avlNode.ts +++ b/lib/data/avl/avlNode.ts @@ -293,3 +293,23 @@ export function keyValuePairs( return result; } + +export function emptyAVL( + tr: AVLTree +): boolean { + return keyValuePairs(tr).length === 0; +} + +export function mergeAVL( + a: AVLTree, + b: AVLTree, + compareKeys: (a: TKey, b: TKey) => number +): AVLTree { + let result = a; + + for (const [k, v] of keyValuePairs(b)) { + result = insertAVL(result, k, v, compareKeys); + } + + return result; +} diff --git a/lib/index.ts b/lib/index.ts index 9833785..ffa9a4c 100644 --- a/lib/index.ts +++ b/lib/index.ts @@ -30,7 +30,7 @@ export { eraseTypedLambda, prettyPrintTypedLambda, type TypedLambda, - typecheck as typecheckTyped + typecheckTypedLambda as typecheckTyped } from './types/typedLambda.js'; // System F type exports @@ -41,7 +41,7 @@ export { } from './types/systemF.js'; // Conversion exports -export { convertLambda } from './conversion/converter.js'; +export { bracketLambda } from './conversion/converter.js'; // Type system exports export { prettyPrintTy } from './types/types.js'; diff --git a/lib/meta/frontend.ts b/lib/meta/frontend.ts new file mode 100644 index 0000000..a5b9315 --- /dev/null +++ b/lib/meta/frontend.ts @@ -0,0 +1,5 @@ +import { TripLangProgram } from './trip.js'; +import { compile } from './frontend/compilation.js'; + +export { compile }; +export type { TripLangProgram }; diff --git a/lib/meta/frontend/builders.ts b/lib/meta/frontend/builders.ts new file mode 100644 index 0000000..d50e04a --- /dev/null +++ b/lib/meta/frontend/builders.ts @@ -0,0 +1,21 @@ +import { SystemFTerm } from '../../terms/systemF.js'; +import { TypedLambda } from '../../types/typedLambda.js'; +import { UntypedLambda } from '../../terms/lambda.js'; +import { isNonTerminalNode } from './predicates.js'; + +export function mkBranch(n: T): T[] { + if (isNonTerminalNode(n)) { + return [n.rgt, n.lft]; + } + + switch (n.kind) { + case 'systemF-abs': + case 'systemF-type-abs': + case 'typed-lambda-abstraction': + return [n.body] as T[]; + case 'systemF-type-app': + return [n.term] as T[]; + default: + return []; + } +} diff --git a/lib/meta/frontend/compilation.ts b/lib/meta/frontend/compilation.ts new file mode 100644 index 0000000..d769fe1 --- /dev/null +++ b/lib/meta/frontend/compilation.ts @@ -0,0 +1,163 @@ +import { TripLangProgram, SymbolTable, TripLangTerm } from '../trip.js'; +import { indexSymbols as indexSymbolsImpl, resolveDefTerm } from './symbolTable.js'; +import { elaborateTerms } from './elaboration.js'; +import { resolveRefs } from './substitution.js'; +import { externalReferences } from './externalReferences.js'; +import { emptyAVL, createEmptyAVL, insertAVL, AVLTree } from '../../data/avl/avlNode.js'; +import { parseTripLang } from '../../parser/tripLang.js'; +import { typecheckSystemF } from '../../index.js'; +import { BaseType } from '../../types/types.js'; +import { typecheckTypedLambda } from '../../types/typedLambda.js'; +import { prettyTerm } from './prettyPrint.js'; +import { compareStrings } from '../../data/map/stringMap.js'; + +export class CompilationError extends Error { + constructor( + message: string, + public readonly stage: 'parse' | 'index' | 'elaborate' | 'resolve' | 'typecheck', + public readonly cause?: unknown + ) { + let causeStr = ''; + if (cause && typeof cause === 'object') { + const causeObj = cause as Record; + if ('term' in causeObj && causeObj.term && typeof causeObj.term === 'object') { + causeStr = `\nTerm: ${prettyTerm(causeObj.term as TripLangTerm)}`; + } + if ('error' in causeObj) { + causeStr += `\nError: ${String(causeObj.error)}`; + } + if ('unresolvedTerms' in causeObj || 'unresolvedTypes' in causeObj) { + causeStr += '\nUnresolved references:'; + if ('unresolvedTerms' in causeObj) { + causeStr += `\nTerms: ${JSON.stringify(causeObj.unresolvedTerms, null, 2)}`; + } + if ('unresolvedTypes' in causeObj) { + causeStr += `\nTypes: ${JSON.stringify(causeObj.unresolvedTypes, null, 2)}`; + } + } + } else if (cause !== undefined) { + causeStr = `\nCause: ${JSON.stringify(cause)}`; + } + super(message + causeStr); + this.name = 'CompilationError'; + } +} + +export type ParsedProgram = TripLangProgram & { readonly __moniker: unique symbol }; +export type IndexedProgram = TripLangProgram & { readonly __moniker: unique symbol }; +export type ElaboratedProgram = TripLangProgram & { readonly __moniker: unique symbol }; +export type ResolvedProgram = TripLangProgram & { readonly __moniker: unique symbol }; +export type TypecheckedProgram = TripLangProgram & { readonly __moniker: unique symbol }; + +export interface ParsedProgramWithSymbols { + program: ParsedProgram; + symbols: SymbolTable; + readonly __moniker: unique symbol; +} + +export interface IndexedProgramWithSymbols { + program: IndexedProgram; + symbols: SymbolTable; + readonly __moniker: unique symbol; +} + +export interface ElaboratedProgramWithSymbols { + program: ElaboratedProgram; + symbols: SymbolTable; + readonly __moniker: unique symbol; +} + +export interface TypecheckedProgramWithTypes { + program: TypecheckedProgram; + types: AVLTree; + readonly __moniker: unique symbol; +} + +export function parse(input: string): ParsedProgram { + const program = parseTripLang(input); + return { ...program, __moniker: Symbol() } as ParsedProgram; +} + +export function indexSymbols( + program: ParsedProgram, + indexFn: (program: ParsedProgram) => SymbolTable +): IndexedProgramWithSymbols { + const symbols = indexFn(program); + return { + program: { ...program, __moniker: Symbol() } as IndexedProgram, + symbols, + __moniker: Symbol() + } as IndexedProgramWithSymbols; +} + +export function elaborate( + programWithSymbols: IndexedProgramWithSymbols, + elaborateFn: (programWithSymbols: IndexedProgramWithSymbols) => TripLangProgram +): ElaboratedProgramWithSymbols { + const elaborated = elaborateFn(programWithSymbols); + const symbols = indexSymbolsImpl(elaborated); + return { + program: { ...elaborated, __moniker: Symbol() } as ElaboratedProgram, + symbols, + __moniker: Symbol() + } as ElaboratedProgramWithSymbols; +} + +export function resolve(programWithSymbols: ElaboratedProgramWithSymbols): ResolvedProgram { + const resolved = resolveRefs(programWithSymbols.program, programWithSymbols.symbols); + + for (const resolvedTerm of resolved.terms) { + const defTerm = resolveDefTerm(resolvedTerm); + const [ut, uty] = externalReferences(defTerm); + if (!emptyAVL(ut) || !emptyAVL(uty)) { + throw new CompilationError( + 'Unresolved external references after resolution', + 'resolve', + { term: resolvedTerm, unresolvedTerms: ut, unresolvedTypes: uty } + ); + } + } + + return { ...resolved, __moniker: Symbol() } as ResolvedProgram; +} + +export function typecheck(program: ResolvedProgram): TypecheckedProgramWithTypes { + let types = createEmptyAVL(); + + for (const term of program.terms) { + try { + switch(term.kind) { + case 'poly': + types = insertAVL(types, term.name, typecheckSystemF(term.term), compareStrings); + break; + case 'typed': + types = insertAVL(types, term.name, typecheckTypedLambda(term.term), compareStrings); + break; + default: + break; + } + } catch (e) { + if (e instanceof TypeError) { + throw new CompilationError( + 'Type error during typechecking', + 'typecheck', + { term, error: e } + ); + } + } + } + + return { + program: { ...program, __moniker: Symbol() } as TypecheckedProgram, + types, + __moniker: Symbol() + } as TypecheckedProgramWithTypes; +} + +export function compile(input: string): TypecheckedProgramWithTypes { + const parsed = parse(input); + const indexed = indexSymbols(parsed, (p) => indexSymbolsImpl(p)); + const elaborated = elaborate(indexed, (p) => elaborateTerms(p.program, p.symbols)); + const resolved = resolve(elaborated); + return typecheck(resolved); +} diff --git a/lib/meta/frontend/elaboration.ts b/lib/meta/frontend/elaboration.ts new file mode 100644 index 0000000..fd4a4c7 --- /dev/null +++ b/lib/meta/frontend/elaboration.ts @@ -0,0 +1,62 @@ +import { searchAVL } from '../../data/avl/avlNode.js'; +import { compareStrings } from '../../data/map/stringMap.js'; +import { SymbolTable, TripLangProgram, TripLangTerm } from '../trip.js'; +import { SystemFTerm, mkSystemFAbs, mkSystemFTAbs, mkSystemFTypeApp } from '../../terms/systemF.js'; +import { BaseType } from '../../types/types.js'; +import { cons } from '../../cons.js'; + +export function elaborateTerms(parsed: TripLangProgram, syms: SymbolTable): TripLangProgram { + return { + kind: 'program', + terms: parsed.terms.map(t => elaborateTerm(t, syms)) + }; +} + +export function elaborateTerm(term: TripLangTerm, syms: SymbolTable): TripLangTerm { + switch (term.kind) { + case 'poly': + return { + ...term, + term: elaborateSystemF(term.term, syms) + }; + case 'typed': + return term; + case 'untyped': + return term; + case 'combinator': + return term; + case 'type': + return term; + } +} + +function getTypeFromVar(term: SystemFTerm, syms: SymbolTable): BaseType | undefined { + if (term.kind === 'systemF-var') { + return searchAVL(syms.types, term.name, compareStrings)?.type; + } + return undefined; +} + +export function elaborateSystemF(systemF: SystemFTerm, syms: SymbolTable): SystemFTerm { + switch (systemF.kind) { + case 'systemF-var': + return systemF; + case 'systemF-abs': + return mkSystemFAbs(systemF.name, systemF.typeAnnotation, elaborateSystemF(systemF.body, syms)); + case 'systemF-type-abs': + return mkSystemFTAbs(systemF.typeVar, elaborateSystemF(systemF.body, syms)); + case 'systemF-type-app': + return mkSystemFTypeApp(elaborateSystemF(systemF.term, syms), systemF.typeArg); + case 'non-terminal': { + const elaboratedLft = elaborateSystemF(systemF.lft, syms); + const elaboratedRgt = elaborateSystemF(systemF.rgt, syms); + const typeArg = getTypeFromVar(elaboratedRgt, syms); + + if (typeArg) { + return mkSystemFTypeApp(elaboratedLft, typeArg); + } + + return cons(elaboratedLft, elaboratedRgt); + } + } +} diff --git a/lib/meta/frontend/externalReferences.ts b/lib/meta/frontend/externalReferences.ts new file mode 100644 index 0000000..7ebeb76 --- /dev/null +++ b/lib/meta/frontend/externalReferences.ts @@ -0,0 +1,109 @@ +import { AVLTree, createEmptyAVL, insertAVL, searchAVL } from '../../data/avl/avlNode.js'; +import { compareStrings } from '../../data/map/stringMap.js'; +import { BaseType } from '../../types/types.js'; +import { TripLangDefType } from '../trip.js'; +import { CompilationError } from './compilation.js'; + +export function externalReferences(td: TripLangDefType): +[ + AVLTree, + AVLTree +] { + let externalTermRefs = createEmptyAVL(); + let externalTypeRefs = createEmptyAVL(); + let absBindMap = createEmptyAVL(); + const defStack: TripLangDefType[] = [td]; + + while (defStack.length) { + const current = defStack.pop(); + + if (current === undefined) { + throw new CompilationError( + 'Underflow in external references stack', + 'resolve', + { stack: defStack } + ); + } + + switch (current.kind) { + case 'systemF-var': { + const external = searchAVL(absBindMap, current.name, compareStrings) === undefined; + + if (external) { + externalTermRefs = insertAVL(externalTermRefs, current.name, current, compareStrings); + } + + break; + } + + case 'lambda-var': { + const external = searchAVL(absBindMap, current.name, compareStrings) === undefined; + + if (external) { + externalTermRefs = insertAVL(externalTermRefs, current.name, current, compareStrings); + } + + break; + } + + case 'type-var': { + const external = searchAVL(absBindMap, current.typeName, compareStrings) === undefined; + + if (external) { + externalTypeRefs = insertAVL(externalTypeRefs, current.typeName, current, compareStrings); + } + + break; + } + + case 'lambda-abs': { + defStack.push(current.body); + absBindMap = insertAVL(absBindMap, current.name, current.body, compareStrings); + break; + } + + case 'systemF-abs': { + defStack.push(current.typeAnnotation); + defStack.push(current.body); + absBindMap = insertAVL(absBindMap, current.name, current.body, compareStrings); + break; + } + + case 'systemF-type-abs': { + defStack.push(current.body); + absBindMap = insertAVL(absBindMap, current.typeVar, current.body, compareStrings); + break; + } + + case 'typed-lambda-abstraction': { + defStack.push(current.ty); + defStack.push(current.body); + absBindMap = insertAVL(absBindMap, current.varName, current.body, compareStrings); + break; + } + + case 'forall': + defStack.push(current.body); + absBindMap = insertAVL(absBindMap, current.typeVar, current.body, compareStrings); + break; + + case 'systemF-type-app': { + defStack.push(current.term); + defStack.push(current.typeArg); + break; + } + + case 'terminal': + // ignore - no bindings possible + break; + + case 'non-terminal': { + defStack.push(current.lft); + defStack.push(current.rgt); + break; + } + } + } + + return [externalTermRefs, externalTypeRefs]; +} diff --git a/lib/meta/frontend/predicates.ts b/lib/meta/frontend/predicates.ts new file mode 100644 index 0000000..60bb67f --- /dev/null +++ b/lib/meta/frontend/predicates.ts @@ -0,0 +1,37 @@ +import { SystemFTerm } from '../../terms/systemF.js'; +import { TypedLambda } from '../../types/typedLambda.js'; +import { UntypedLambda } from '../../terms/lambda.js'; + +export const isNonTerminalNode = (n: T): + n is T & { kind: 'non-terminal'; lft: T; rgt: T } => + n.kind === 'non-terminal'; + +export function needsRebuild(n: SystemFTerm | TypedLambda | UntypedLambda): boolean { + if (isNonTerminalNode(n)) { + return true; + } + + switch (n.kind) { + case 'systemF-abs': + case 'systemF-type-abs': + case 'systemF-type-app': + case 'typed-lambda-abstraction': + return true; + default: + return false; + } +} + +export function needsReplace( + n: SystemFTerm | TypedLambda | UntypedLambda, + termName: string +): boolean { + switch (n.kind) { + case 'systemF-var': + return n.name === termName; + case 'lambda-var': + return n.name === termName; + default: + return false; + } +} diff --git a/lib/meta/frontend/prettyPrint.ts b/lib/meta/frontend/prettyPrint.ts new file mode 100644 index 0000000..6b301b0 --- /dev/null +++ b/lib/meta/frontend/prettyPrint.ts @@ -0,0 +1,23 @@ +import { prettyPrintSKI } from '../../index.js'; +import { prettyPrintUntypedLambda } from '../../terms/lambda.js'; +import { prettyPrintSystemF } from '../../terms/systemF.js'; +import { prettyPrintTypedLambda } from '../../types/typedLambda.js'; +import { prettyPrintTy } from '../../types/types.js'; +import { TripLangTerm } from '../trip.js'; + +const def = ' := '; + +export function prettyTerm(dt: TripLangTerm): string { + switch (dt.kind) { + case 'poly': + return dt.name + def + prettyPrintSystemF(dt.term); + case 'typed': + return dt.name + def + prettyPrintTypedLambda(dt.term); + case 'untyped': + return dt.name + def + prettyPrintUntypedLambda(dt.term); + case 'combinator': + return dt.name + def + prettyPrintSKI(dt.term); + case 'type': + return dt.name + def + prettyPrintTy(dt.type); + } +} diff --git a/lib/meta/frontend/rebuilders.ts b/lib/meta/frontend/rebuilders.ts new file mode 100644 index 0000000..103229d --- /dev/null +++ b/lib/meta/frontend/rebuilders.ts @@ -0,0 +1,191 @@ +import { cons } from '../../cons.js'; +import { referencesVar, substituteSystemFType as substituteType } from '../../types/systemF.js'; +import { BaseType } from '../../types/types.js'; +import { TripLangTerm } from '../trip.js'; +import { SystemFTerm } from '../../terms/systemF.js'; +import { TypedLambda } from '../../types/typedLambda.js'; +import { UntypedLambda } from '../../terms/lambda.js'; +import { isNonTerminalNode } from './predicates.js'; +import { CompilationError } from './compilation.js'; + +export function rebuildNonTerminal( + n: T & { kind: 'non-terminal'; lft: T; rgt: T }, + rebuilt: T[], + consFn: (l: T, r: T) => T +): T { + const rgtNew = rebuilt.pop()!; + const lftNew = rebuilt.pop()!; + return lftNew === n.lft && rgtNew === n.rgt ? n : consFn(lftNew, rgtNew); +} + +export function rebuildSystemFAbs( + n: SystemFTerm & { kind: 'systemF-abs'; }, + rebuilt: SystemFTerm[] +): SystemFTerm & { kind: 'systemF-abs' } { + const popped = rebuilt.pop()!; + return n.body === popped ? n : { ...n, body: popped }; +} + +export function rebuildTypedLambdaAbs( + n: TypedLambda & { kind: 'typed-lambda-abstraction'; }, + rebuilt: TypedLambda[] +): TypedLambda { + const popped = rebuilt.pop()!; + return n.body === popped ? n : { ...n, body: popped }; +} + +export function rebuildTypeAbs( + n: SystemFTerm & { kind: 'systemF-type-abs' }, + rebuilt: SystemFTerm[], +): SystemFTerm & { kind: 'systemF-type-abs' } { + const popped = rebuilt.pop()!; + return n.body === popped ? n : { ...n, body: popped }; +} + +export function rebuildTypeApp( + n: SystemFTerm & { kind: 'systemF-type-app' }, + rebuilt: SystemFTerm[], + nextTypeArg: BaseType +): SystemFTerm & { kind: 'systemF-type-app' } { + const popped = rebuilt.pop()!; + + return (popped === n.term && nextTypeArg === n.typeArg) + ? n + : { ...n, term: popped, typeArg: nextTypeArg }; +} + +export function polyRebuild(n: SystemFTerm, rebuilt: SystemFTerm[], term: TripLangTerm): SystemFTerm { + if (isNonTerminalNode(n)) { + return rebuildNonTerminal(n, rebuilt, cons); + } else if (n.kind === 'systemF-abs') { + return rebuildSystemFAbs(n, rebuilt); + } else if (n.kind === 'systemF-type-abs') { + return rebuildTypeAbs(n, rebuilt); + } else if (n.kind === 'systemF-type-app') { + const nextType = (term.kind === 'type' && referencesVar(n.typeArg, term.name)) + ? substituteType(n.typeArg, term.name, term.type) + : n.typeArg; + return rebuildTypeApp(n, rebuilt, nextType); + } else { + throw new CompilationError( + `Unexpected kind: ${JSON.stringify(n)}`, + 'resolve', + { term: n } + ); + } +} + +export function typedRebuild(n: TypedLambda, rebuilt: TypedLambda[]): TypedLambda { + if (isNonTerminalNode(n)) { + return rebuildNonTerminal(n, rebuilt, cons); + } else if (n.kind === 'typed-lambda-abstraction') { + return rebuildTypedLambdaAbs(n, rebuilt); + } else { + throw new CompilationError( + `Unexpected kind: ${JSON.stringify(n)}`, + 'resolve', + { term: n } + ); + } +} + +export const untypedRebuild = (n: UntypedLambda, rebuilt: UntypedLambda[]): UntypedLambda => + isNonTerminalNode(n) ? rebuildNonTerminal(n, rebuilt, cons) : n; + +export function polyTypeRebuild( + n: SystemFTerm, + rebuilt: SystemFTerm[], + typeRef: string, + targetBase: BaseType +): SystemFTerm { + if (isNonTerminalNode(n)) { + return rebuildNonTerminal(n, rebuilt, cons); + } else if (n.kind === 'systemF-abs') { + const nextType = referencesVar(n.typeAnnotation, typeRef) + ? substituteType(n.typeAnnotation, typeRef, targetBase) + : n.typeAnnotation; + const popped = rebuilt.pop()!; + + return { + ...n, + body: popped, + typeAnnotation: nextType + }; + } else if (n.kind === 'systemF-type-abs') { + return rebuildTypeAbs(n, rebuilt); + } else if (n.kind === 'systemF-type-app') { + const nextType = referencesVar(n.typeArg, typeRef) + ? substituteType(n.typeArg, typeRef, targetBase) + : n.typeArg; + + return rebuildTypeApp(n, rebuilt, nextType); + } else { + throw new CompilationError( + `Unexpected kind: ${JSON.stringify(n)}`, + 'resolve', + { term: n } + ); + } +} + +export function typedTypeRebuild(n: TypedLambda, rebuilt: TypedLambda[]): TypedLambda { + if (isNonTerminalNode(n)) { + return rebuildNonTerminal(n, rebuilt, cons); + } else if (n.kind === 'typed-lambda-abstraction') { + return rebuildTypedLambdaAbs(n, rebuilt); + } else { + throw new CompilationError( + `Unexpected kind: ${JSON.stringify(n)}`, + 'resolve', + { term: n } + ); + } +} + +export function typedTypeRebuildTerm(n: TripLangTerm): TripLangTerm { + switch (n.kind) { + case 'poly': + case 'typed': + case 'untyped': + case 'combinator': + return n; + case 'type': + throw new CompilationError( + `Unexpected kind: ${JSON.stringify(n)}`, + 'resolve', + { term: n } + ); + } +} + +export function untypedTermRebuild(n: TripLangTerm): TripLangTerm { + switch (n.kind) { + case 'poly': + case 'typed': + case 'untyped': + case 'combinator': + return n; + case 'type': + throw new CompilationError( + `Unexpected kind ${JSON.stringify(n)}`, + 'resolve', + { term: n } + ); + } +} + +export function untypedTypeRebuild(n: TripLangTerm): TripLangTerm { + switch (n.kind) { + case 'poly': + case 'typed': + case 'untyped': + case 'combinator': + return n; + case 'type': + throw new CompilationError( + `Unexpected kind: ${JSON.stringify(n)}`, + 'resolve', + { term: n } + ); + } +} diff --git a/lib/meta/frontend/replacers.ts b/lib/meta/frontend/replacers.ts new file mode 100644 index 0000000..90edc51 --- /dev/null +++ b/lib/meta/frontend/replacers.ts @@ -0,0 +1,31 @@ +import { SystemFTerm } from '../../terms/systemF.js'; +import { TypedLambda } from '../../types/typedLambda.js'; +import { UntypedLambda } from '../../terms/lambda.js'; +import { TripLangTerm } from '../trip.js'; +import { substituteSystemFType } from '../../types/systemF.js'; +import { BaseType } from '../../types/types.js'; + +export const replace = (n: T, term: TripLangTerm): T => { + if (n.kind === 'systemF-var' && term.kind === 'poly') { + return term.term as T; + } + if (n.kind === 'lambda-var' && term.kind === 'typed') { + return term.term as T; + } + if (term.kind === 'untyped') { + return term.term as T; + } + return n; +}; + +export function typedTypeReplace(n: TypedLambda, typeRef: string, targetBase: BaseType): TypedLambda { + if (n.kind !== 'typed-lambda-abstraction') { + return n; + } + const newTy = substituteSystemFType(n.ty, typeRef, targetBase); + return { + ...n, + ty: newTy, + }; +} + diff --git a/lib/meta/frontend/substitution.ts b/lib/meta/frontend/substitution.ts new file mode 100644 index 0000000..334a365 --- /dev/null +++ b/lib/meta/frontend/substitution.ts @@ -0,0 +1,229 @@ +import { keyValuePairs, searchAVL } from '../../data/avl/avlNode.js'; +import { compareStrings } from '../../data/map/stringMap.js'; +import { BaseType } from '../../types/types.js'; +import { SymbolTable, TripLangProgram, TripLangTerm, TypeDefinition, TripLangDefType } from '../trip.js'; +import { termLevel, lower } from './termLevel.js'; +import { resolveDefTerm } from './symbolTable.js'; +import { externalReferences } from './externalReferences.js'; +import { mkBranch } from './builders.js'; +import { needsReplace, needsRebuild } from './predicates.js'; +import { replace as replaceTerm, typedTypeReplace } from './replacers.js'; +import { + polyRebuild, + typedRebuild, + untypedRebuild, + polyTypeRebuild, + typedTypeRebuild +} from './rebuilders.js'; +import { CompilationError } from './compilation.js'; + +export function resolveRefs(program: TripLangProgram, syms: SymbolTable): TripLangProgram { + return { + kind: 'program', + terms: program.terms.map(t => resolveTermRefs(t, syms)) + }; +} + +export function resolveTermRefs(term: TripLangTerm, syms: SymbolTable): TripLangTerm { + const programTerm = resolveDefTerm(term); + const [tRefs, tyRefs] = externalReferences(programTerm); + const externalTermRefs = keyValuePairs(tRefs).map(kvp => kvp[0]); + const externalTypeRefs = keyValuePairs(tyRefs).map(kvp => kvp[0]); + + // First resolve all type references + const withResolvedTypes = externalTypeRefs.reduce((acc, typeRef) => { + const resolvedTy = searchAVL(syms.types, typeRef, compareStrings); + + if (resolvedTy === undefined) { + throw new CompilationError( + `Unresolved external type reference: ${typeRef}`, + 'resolve', + { typeRef, syms } + ); + } + + return substituteTripLangType(acc, resolvedTy); + }, term); + + // Then resolve all term references + return externalTermRefs.reduce((acc, termRef) => { + const symbolReferencedTerm = searchAVL(syms.terms, termRef, compareStrings); + const symbolReferencedType = searchAVL(syms.types, termRef, compareStrings); + + if (symbolReferencedTerm === undefined && symbolReferencedType === undefined) { + throw new CompilationError( + `Unresolved external term reference: ${termRef}`, + 'resolve', + { termRef, syms } + ); + } + + if (symbolReferencedTerm !== undefined && symbolReferencedType !== undefined) { + throw new CompilationError( + `Duplicate external term reference resolution: ${termRef}`, + 'resolve', + { termRef, syms } + ); + } + + if (symbolReferencedTerm) { + // note: the symbol referenced term may need resolution too, + // so we recursively resolve it here + const toInsert = resolveTermRefs(symbolReferencedTerm, syms); + return substituteTripLangTerm(acc, toInsert); + } + + if (symbolReferencedType) { + const withType = substituteTripLangType(acc, symbolReferencedType); + // note: system F types can appear in terms + return substituteTripLangTerm(withType, symbolReferencedType); + } + + return acc; + }, withResolvedTypes); +} + +export function substituteTripLangTerm(current: TripLangTerm, term: TripLangTerm): TripLangTerm { + while (termLevel(current) < termLevel(term)) { + term = lower(term); + } + + switch (current.kind) { + case 'poly': { + return { + kind: 'poly', + name: current.name, + term: substitute( + current.term, + mkBranch, + n => needsReplace(n, term.name), + n => replaceTerm(n, term), + needsRebuild, + (n, rebuilt) => polyRebuild(n, rebuilt, term) + ) + }; + } + case 'typed': { + return { + kind: 'typed', + name: current.name, + term: substitute( + current.term, + mkBranch, + n => needsReplace(n, term.name), + n => replaceTerm(n, term), + needsRebuild, + typedRebuild + ), + type: undefined + }; + } + case 'untyped': { + return { + ...current, + term: substitute( + current.term, + mkBranch, + n => needsReplace(n, term.name), + n => replaceTerm(n, term), + needsRebuild, + untypedRebuild + ) + }; + } + case 'combinator': + case 'type': + throw new CompilationError( + 'Unexpected current kind on LHS', + 'resolve', + { current } + ); + } +} + +export function substituteTripLangType(current: TripLangTerm, type: TypeDefinition): TripLangTerm { + if (current.kind === 'type') { + throw new CompilationError( + 'Substitutions never have types on LHS', + 'resolve', + { current } + ); + } + + const typeRef: string = type.name; + const targetBase: BaseType = type.type; + + switch (current.kind) { + case 'poly': + return { + ...current, + term: substitute( + current.term, + mkBranch, + () => false, // note: all rebuilding happens at junction nodes + n => n, + needsRebuild, + (n, rebuilt) => polyTypeRebuild(n, rebuilt, typeRef, targetBase) + ) + }; + case 'typed': + return { + ...current, + term: substitute( + current.term, + mkBranch, + n => needsReplace(n, typeRef), + n => typedTypeReplace(n, typeRef, targetBase), + needsRebuild, + typedTypeRebuild + ) + }; + case 'untyped': + case 'combinator': + return { + ...current + }; + } +} + +export function substitute( + current: T, + mkBranchFn: (_ : T) => T[], + replaceNeeded: (_: T) => boolean, + replaceFn: (_:T) => T, + rebuildNeeded: (_: T) => boolean, + rebuildFn: (_1: T, _2 : T[]) => T +): T { + type Frame = [node: T, visited: boolean]; + const work: Frame[] = [[current, false]]; + const rebuilt: T[] = []; + + while (work.length > 0) { + const r = work.pop(); + if (!r) continue; + + const [n, seen] = r; + + if (!seen) { + work.push([n, true]); + const branches = mkBranchFn(n); + branches.forEach(branch => work.push([branch, false])); + } else if (rebuildNeeded(n)) { + rebuilt.push(rebuildFn(n, rebuilt)); + } else if (replaceNeeded(n)) { + rebuilt.push(replaceFn(n)); + } else { + rebuilt.push(n); + } + } + + const result = rebuilt.pop(); + if (result === undefined) { + throw new CompilationError( + 'Substitution failed: no result found', + 'resolve', + { term: current, substitutions: rebuilt } + ); + } + return result; +} diff --git a/lib/meta/frontend/symbolTable.ts b/lib/meta/frontend/symbolTable.ts new file mode 100644 index 0000000..154daa3 --- /dev/null +++ b/lib/meta/frontend/symbolTable.ts @@ -0,0 +1,59 @@ +import { createEmptyAVL, insertAVL, searchAVL } from '../../data/avl/avlNode.js'; +import { compareStrings } from '../../data/map/stringMap.js'; +import { prettyPrintTy } from '../../types/types.js'; +import { SymbolTable, TripLangDefType, TripLangProgram, TripLangTerm, TypeDefinition } from '../trip.js'; +import { CompilationError } from './compilation.js'; + +export function indexSymbols(program: TripLangProgram): SymbolTable { + let termMap = createEmptyAVL(); + let tyMap = createEmptyAVL(); + + for (const term of program.terms) { + switch (term.kind) { + case 'poly': + case 'typed': + case 'untyped': + case 'combinator': { + if (searchAVL(termMap, term.name, compareStrings) !== undefined) { + throw new CompilationError( + `Duplicate definition: ${term.name}`, + 'index', + { term } + ); + } + + termMap = insertAVL(termMap, term.name, term, compareStrings); + } + break; + case 'type': { + const typeDef = term; + if (searchAVL(tyMap, term.name, compareStrings) !== undefined) { + throw new CompilationError( + `Duplicate type: ${prettyPrintTy(typeDef.type)}`, + 'index', + { typeDef } + ); + } + + tyMap = insertAVL(tyMap, term.name, typeDef, compareStrings); + } + break; + } + } + return { + terms: termMap, + types: tyMap + }; +} + +export function resolveDefTerm(tt: TripLangTerm): TripLangDefType { + switch (tt.kind) { + case 'poly': + case 'typed': + case 'untyped': + case 'combinator': + return tt.term; + case 'type': + return tt.type; + } +} diff --git a/lib/meta/frontend/termLevel.ts b/lib/meta/frontend/termLevel.ts new file mode 100644 index 0000000..d7e3fa4 --- /dev/null +++ b/lib/meta/frontend/termLevel.ts @@ -0,0 +1,64 @@ +import { bracketLambda, eraseSystemF } from '../../index.js'; +import { eraseTypedLambda } from '../../types/typedLambda.js'; +import { TripLangTerm } from '../trip.js'; +import { CompilationError } from './compilation.js'; + +export function termLevel(dt: TripLangTerm): number { + switch (dt.kind) { + case 'poly': + return 4; + case 'typed': + return 3; + case 'untyped': + return 2; + case 'combinator': + return 1; + case 'type': + return -1; + } +} + +export function lower(dt: TripLangTerm): TripLangTerm { + switch (dt.kind) { + case 'poly': { + const erased = eraseSystemF(dt.term); + + return { + kind: 'typed', + name: dt.name, + type: undefined, // note: we'll check it after all the symbols are resolved + term: erased + }; + } + case 'typed': { + const erased = eraseTypedLambda(dt.term); + + return { + kind: 'untyped', + name: dt.name, + term: erased + }; + } + + case 'untyped': { + const erased = bracketLambda(dt.term); + + return { + kind: 'combinator', + name: dt.name, + term: erased + }; + } + + case 'combinator': { + return dt; // fixed point + } + + case 'type': + throw new CompilationError( + 'Cannot lower a type', + 'resolve', + { type: dt } + ); + } +} diff --git a/lib/meta/trip.ts b/lib/meta/trip.ts index 2886c4e..59155d2 100644 --- a/lib/meta/trip.ts +++ b/lib/meta/trip.ts @@ -1,3 +1,4 @@ +import { AVLTree } from '../data/avl/avlNode.js'; import { SKIExpression } from '../ski/expression.js'; import { UntypedLambda } from '../terms/lambda.js'; import { SystemFTerm } from '../terms/systemF.js'; @@ -16,6 +17,13 @@ export type TripLangTerm = | CombinatorDefinition | TypeDefinition; +export type TripLangDefType = + | SystemFTerm + | TypedLambda + | UntypedLambda + | SKIExpression + | BaseType; + export interface PolyDefinition { kind: 'poly'; name: string; @@ -25,7 +33,7 @@ export interface PolyDefinition { export interface TypedDefinition { kind: 'typed'; name: string; - type: BaseType; + type: BaseType | undefined; // note: can be inferred, but only after resolution term: TypedLambda; } @@ -46,3 +54,8 @@ export interface TypeDefinition { name: string; type: BaseType; } + +export interface SymbolTable { + terms: AVLTree; + types: AVLTree; +} diff --git a/lib/parser/systemFType.ts b/lib/parser/systemFType.ts index 16abaf4..66aca70 100644 --- a/lib/parser/systemFType.ts +++ b/lib/parser/systemFType.ts @@ -1,5 +1,5 @@ -import { SystemFType, forall } from '../types/systemF.js'; -import { arrow, mkTypeVariable } from '../types/types.js'; +import { forall } from '../types/systemF.js'; +import { arrow, BaseType, mkTypeVariable } from '../types/types.js'; import { ParseError } from './parseError.js'; import { ParserState, @@ -25,7 +25,7 @@ import { */ export function parseSystemFType( state: ParserState -): [string, SystemFType, ParserState] { +): [string, BaseType, ParserState] { const [ch, s] = peek(state); if (ch === '∀') { // Parse universal type: ∀X. T @@ -57,7 +57,7 @@ export function parseSystemFType( */ function parseSimpleSystemFType( state: ParserState -): [string, SystemFType, ParserState] { +): [string, BaseType, ParserState] { const [ch, s] = peek(state); if (ch === '(') { const stateAfterLP = matchLP(s); diff --git a/lib/terms/systemF.ts b/lib/terms/systemF.ts index 1171030..5173776 100644 --- a/lib/terms/systemF.ts +++ b/lib/terms/systemF.ts @@ -1,5 +1,5 @@ import { ConsCell } from '../cons.js'; -import { SystemFType } from '../types/systemF.js'; +import { BaseType } from '../types/types.js'; /** * A term variable. @@ -20,13 +20,13 @@ export const mkSystemFVar = (name: string): SystemFVar => ({ export interface SystemFAbs { kind: 'systemF-abs'; name: string; - typeAnnotation: SystemFType; + typeAnnotation: BaseType; body: SystemFTerm; } export const mkSystemFAbs = ( name: string, - typeAnnotation: SystemFType, + typeAnnotation: BaseType, body: SystemFTerm ): SystemFAbs => ({ kind: 'systemF-abs', @@ -59,12 +59,12 @@ export const mkSystemFTAbs = ( export interface SystemFTypeApp { kind: 'systemF-type-app'; term: SystemFTerm; - typeArg: SystemFType; + typeArg: BaseType; } export const mkSystemFTypeApp = ( term: SystemFTerm, - typeArg: SystemFType + typeArg: BaseType ): SystemFTypeApp => ({ kind: 'systemF-type-app', term, @@ -106,7 +106,7 @@ export function prettyPrintSystemF(term: SystemFTerm): string { } } -function flattenSystemFApp(term: SystemFTerm): SystemFTerm[] { +export function flattenSystemFApp(term: SystemFTerm): SystemFTerm[] { if (term.kind === 'non-terminal') { const leftParts = flattenSystemFApp(term.lft); return [...leftParts, term.rgt]; @@ -115,7 +115,7 @@ function flattenSystemFApp(term: SystemFTerm): SystemFTerm[] { } } -export function prettyPrintSystemFType(ty: SystemFType): string { +export function prettyPrintSystemFType(ty: BaseType): string { if (ty.kind === 'forall') { return `∀${ty.typeVar}.${prettyPrintSystemFType(ty.body)}`; } else if (ty.kind === 'non-terminal' && 'lft' in ty && 'rgt' in ty) { diff --git a/lib/types/systemF.ts b/lib/types/systemF.ts index 5c6ecb1..9a61ebf 100644 --- a/lib/types/systemF.ts +++ b/lib/types/systemF.ts @@ -5,14 +5,13 @@ import { TypedLambda, mkTypedAbs } from './typedLambda.js'; import { AVLTree, createEmptyAVL, insertAVL, searchAVL } from '../data/avl/avlNode.js'; import { compareStrings } from '../data/map/stringMap.js'; import { Set, createSet, insertSet } from '../data/set/set.js'; +import { normalize } from './normalization.js'; /* * https://en.wikipedia.org/wiki/System_F */ -export type SystemFType = BaseType; - -export const forall = (typeVar: string, body: SystemFType): ForallType => ({ +export const forall = (typeVar: string, body: BaseType): ForallType => ({ kind: 'forall', typeVar, body, @@ -22,10 +21,10 @@ export const forall = (typeVar: string, body: SystemFType): ForallType => ({ * Substitute in the type "original" the sub–type lft with rgt. */ export const substituteSystemFType = ( - original: SystemFType, + original: BaseType, targetVarName: string, - replacement: SystemFType -): SystemFType => { + replacement: BaseType +): BaseType => { switch (original.kind) { case 'type-var': return original.typeName === targetVarName ? replacement : original; @@ -46,13 +45,28 @@ export const substituteSystemFType = ( } }; +export const referencesVar = ( + original: BaseType, + varName: string +): boolean => { + switch (original.kind) { + case 'type-var': + return original.typeName === varName; + case 'non-terminal': + return referencesVar(original.lft, varName) || + referencesVar(original.rgt, varName); + case 'forall': + return referencesVar(original.body, varName); + } +}; + /** * The type checking context for System F. * - termCtx maps term variables (strings) to their types (SystemFType) using a persistent AVL tree. * - typeVars is the set of bound type variables using our persistent AVLSet. */ export interface SystemFContext { - termCtx: AVLTree; + termCtx: AVLTree; typeVars: Set; } @@ -60,7 +74,7 @@ export interface SystemFContext { * Returns an empty System F context. */ export const emptySystemFContext = (): SystemFContext => ({ - termCtx: createEmptyAVL(), + termCtx: createEmptyAVL(), typeVars: createSet(compareStrings) }); @@ -68,7 +82,7 @@ export const emptySystemFContext = (): SystemFContext => ({ * Typechecks a System F term. * Returns just the type (discarding the final context). */ -export const typecheck = (term: SystemFTerm): SystemFType => { +export const typecheck = (term: SystemFTerm): BaseType => { return typecheckSystemF(emptySystemFContext(), term)[0]; }; @@ -90,7 +104,7 @@ export const typecheck = (term: SystemFTerm): SystemFType => { export const typecheckSystemF = ( ctx: SystemFContext, term: SystemFTerm -): [SystemFType, SystemFContext] => { +): [BaseType, SystemFContext] => { switch (term.kind) { case 'systemF-var': { const ty = searchAVL(ctx.termCtx, term.name, compareStrings); @@ -120,9 +134,20 @@ export const typecheckSystemF = ( ); } if (!typesLitEq(funTy.lft, argTy)) { - throw new TypeError( - `function argument type mismatch: expected ${prettyPrintTy(funTy.lft)}, got ${prettyPrintTy(argTy)}` - ); + // Only use normalization for forall types (alpha-equivalence) + if (funTy.lft.kind === 'forall' && argTy.kind === 'forall') { + const normLft = normalize(funTy.lft); + const normArg = normalize(argTy); + if (!typesLitEq(normLft, normArg)) { + throw new TypeError( + `function argument type mismatch: expected ${prettyPrintTy(funTy.lft)}, got ${prettyPrintTy(argTy)}` + ); + } + } else { + throw new TypeError( + `function argument type mismatch: expected ${prettyPrintTy(funTy.lft)}, got ${prettyPrintTy(argTy)}` + ); + } } return [funTy.rgt, ctxAfterRight]; } @@ -152,7 +177,7 @@ export const typecheckSystemF = ( /** * Pretty prints a System F type. */ -export const prettyPrintSystemFType = (ty: SystemFType): string => { +export const prettyPrintSystemFType = (ty: BaseType): string => { if (ty.kind === 'type-var') { return ty.typeName; } diff --git a/lib/types/typedLambda.ts b/lib/types/typedLambda.ts index 3f9b0c7..53b06d2 100644 --- a/lib/types/typedLambda.ts +++ b/lib/types/typedLambda.ts @@ -62,7 +62,7 @@ export const addBinding = return insertAVL(ctx, name, ty, compareStrings); }; -export const typecheck = (typedTerm: TypedLambda): BaseType => { +export const typecheckTypedLambda = (typedTerm: TypedLambda): BaseType => { return typecheckGiven(emptyContext(), typedTerm); }; diff --git a/test/conversion/converter.test.ts b/test/conversion/converter.test.ts index d96aad9..8afe8bf 100644 --- a/test/conversion/converter.test.ts +++ b/test/conversion/converter.test.ts @@ -7,7 +7,7 @@ import { reduce } from '../../lib/evaluator/skiEvaluator.js'; import { UnChurchNumber, ChurchN } from '../../lib/ski/church.js'; import { apply } from '../../lib/ski/expression.js'; import { I } from '../../lib/ski/terminal.js'; -import { convertLambda } from '../../lib/conversion/converter.js'; +import { bracketLambda } from '../../lib/conversion/converter.js'; import { mkUntypedAbs, mkVar, prettyPrintUntypedLambda } from '../../lib/terms/lambda.js'; describe('Lambda conversion', () => { @@ -17,7 +17,7 @@ describe('Lambda conversion', () => { const flip = mkUntypedAbs('x', mkUntypedAbs('y', cons(mkVar('y'), mkVar('x')))); it('should convert λx.x to I', () => { - expect(convertLambda(id)).to.deep.equal(I); + expect(bracketLambda(id)).to.deep.equal(I); }); it('should convert λx.λy.x to something that acts like K', () => { @@ -25,7 +25,7 @@ describe('Lambda conversion', () => { for (let a = 0; a < N; a++) { for (let b = 0; b < N; b++) { const result = UnChurchNumber( - reduce(apply(convertLambda(konst), ChurchN(a), ChurchN(b))) + reduce(apply(bracketLambda(konst), ChurchN(a), ChurchN(b))) ); expect(result).to.equal(a); } @@ -51,7 +51,7 @@ describe('Lambda conversion', () => { for (let b = 0; b < N; b++) { const expected = a ** b; // exponentiation: a^b const result = UnChurchNumber( - reduce(apply(convertLambda(flip), ChurchN(a), ChurchN(b))) + reduce(apply(bracketLambda(flip), ChurchN(a), ChurchN(b))) ); expect(result).to.equal(expected); } @@ -62,7 +62,7 @@ describe('Lambda conversion', () => { for (let n = 0; n < N; n++) { const expected = Math.max(n - 1, 0); // pred(0) is defined as 0. const result = UnChurchNumber( - reduce(apply(convertLambda(predLambda), ChurchN(n))) + reduce(apply(bracketLambda(predLambda), ChurchN(n))) ); expect(result).to.equal(expected); } diff --git a/test/meta/frontend.test.ts b/test/meta/frontend.test.ts new file mode 100644 index 0000000..dd9d474 --- /dev/null +++ b/test/meta/frontend.test.ts @@ -0,0 +1,274 @@ +import { dirname } from 'path'; +import { fileURLToPath } from 'url'; +import { loadInput } from '../util/fileLoader.js'; +import { parseTripLang } from '../../lib/parser/tripLang.js'; +import { prettyPrintSystemF, prettyPrintTy, prettyPrintUntypedLambda, SystemFTerm, typecheckSystemF } from '../../lib/index.js'; +import { assert } from 'chai'; +import { compile } from '../../lib/meta/frontend.js'; +import { indexSymbols } from '../../lib/meta/frontend/symbolTable.js'; +import { resolveRefs } from '../../lib/meta/frontend/substitution.js'; +import { externalReferences } from '../../lib/meta/frontend/externalReferences.js'; +import { keyValuePairs } from '../../lib/data/avl/avlNode.js'; +import { parseSystemF } from '../../lib/parser/systemFTerm.js'; +import { UnChurchNumber } from '../../lib/ski/church.js'; +import { reduce } from '../../lib/evaluator/skiEvaluator.js'; +import { bracketLambda } from '../../lib/conversion/converter.js'; + +const __dirname = dirname(fileURLToPath(import.meta.url)); + +function isSystemFTerm(term: unknown): term is SystemFTerm { + return !!term && typeof term === 'object' && typeof (term as { kind?: unknown }).kind === 'string' && ( + (term as { kind?: unknown }).kind === 'systemF-var' || + (term as { kind?: unknown }).kind === 'systemF-abs' || + (term as { kind?: unknown }).kind === 'systemF-type-abs' || + (term as { kind?: unknown }).kind === 'systemF-type-app' || + (term as { kind?: unknown }).kind === 'non-terminal' + ); +} + +function assertSystemFTermMatches(actual: SystemFTerm, expected: string, message?: string): void { + try { + const [, expectedAST] = parseSystemF(expected); + assert.deepEqual(actual, expectedAST, message ?? 'SystemF ASTs do not match'); + } catch { + // If ASTs do not match, print pretty-printed terms for debugging + const actualPretty = prettyPrintSystemF(actual); + let expectedPretty: string; + try { + const [, expectedAST] = parseSystemF(expected); + expectedPretty = prettyPrintSystemF(expectedAST); + } catch { + expectedPretty = expected; + } + assert.fail( + (message ? message + '\n' : '') + + `SystemF terms do not match symbolically.\nActual: ${actualPretty}\nExpected: ${expectedPretty}` + ); + } +} + +function assertTypeStringMatches(actual: string, expected: string, message?: string): void { + assert.equal(actual, expected, message ?? `Expected type ${expected}, got ${actual}`); +} + +function assertTermMatches(actual: unknown, expected: string, message?: string): void { + if (isSystemFTerm(actual)) { + assertSystemFTermMatches(actual, expected, message); + } else if (typeof actual === 'string') { + // Assume it's a type string or untyped lambda string + assertTypeStringMatches(actual, expected, message); + } else { + assert.fail(`Unexpected type for actual: ${typeof actual}`); + } +} + +describe('compiler', () => { + it('parses natbool', () => { + const input = loadInput('natBool.trip', __dirname); + const program = parseTripLang(input); + assert(program.terms.length == 2); + const fst = program.terms[0]; + const snd = program.terms[1]; + assert(fst.kind == 'type'); + assert(snd.kind == 'type'); + const fstP = prettyPrintTy(fst.type); + const sndP = prettyPrintTy(snd.type); + assertTermMatches(fstP, '∀X.((X→X)→(X→X))'); + assertTermMatches(sndP, '∀B.(B→(B→B))'); + }); + + it('parses true false zero', () => { + const input = loadInput('trueFalseZero.trip', __dirname); + const program = parseTripLang(input); + assert(program.terms.length == 6); + assert(program.terms[0].kind == 'poly'); + assert(program.terms[1].kind == 'poly'); + assert(program.terms[2].kind == 'poly'); + assert(program.terms[3].kind == 'poly'); + const fst = prettyPrintSystemF(program.terms[0].term); + const snd = prettyPrintSystemF(program.terms[1].term); + const trd = prettyPrintSystemF(program.terms[2].term); + const fth = prettyPrintSystemF(program.terms[3].term); + assertTermMatches(fst, 'ΛB.λt:B.λf:B.t'); + assertTermMatches(snd, 'ΛB.λt:B.λf:B.f'); + assertTermMatches(trd, 'ΛX.λs:(X→X).λz:X.z'); + assertTermMatches(fth, 'λn:Nat.(n[Bool] λb:Bool.false true)'); + + const fstTy = typecheckSystemF(program.terms[0].term); + const fstTyStr = prettyPrintTy(fstTy); + + assert(fstTyStr == '∀B.(B→(B→B))'); + + const symTab = indexSymbols(program); + const resolved = resolveRefs(program, symTab); + + assert(program.terms.length == resolved.terms.length); + }); + + it('parses cond succ', () => { + const input = loadInput('condSucc.trip', __dirname); + parseTripLang(input); + }); + + it('parses pair', () => { + const input = loadInput('pair.trip', __dirname); + parseTripLang(input); + }); + + it('parses pred', () => { + const input = loadInput('pred.trip', __dirname); + parseTripLang(input); + }); + + it('parses mul', () => { + const input = loadInput('mul.trip', __dirname); + parseTripLang(input); + }); + + it('loads factorial', () => { + const input = loadInput('fact.trip', __dirname); + const program = parseTripLang(input); + assert(program.terms.length == 5); + const fst = program.terms[0]; + const snd = program.terms[1]; + const trd = program.terms[2]; + const frt = program.terms[3]; + const fif = program.terms[4]; + assert(fst.kind == 'poly'); + assert(snd.kind == 'poly'); + assert(trd.kind == 'untyped'); + assert(frt.kind == 'poly'); + assert(fif.kind == 'untyped'); + const [sndTermRef, sndTypeRef] = externalReferences(snd.term); + const sndExternalTermNames = keyValuePairs(sndTermRef).map(kvp => kvp[0]); + const sndExternalTypeNames = keyValuePairs(sndTypeRef).map(kvp => kvp[0]); + assert.deepStrictEqual(sndExternalTermNames, ['cond', 'isZero', 'mul', 'one', 'pred']); + assert.deepStrictEqual(sndExternalTypeNames, ['Nat']); + }); + + it('loads fix', () => { + const input = loadInput('fix.trip', __dirname); + const program = parseTripLang(input); + assert(program.terms.length == 1); + assert(program.terms[0].kind == 'untyped'); + const untypedDef = program.terms[0]; + const pp = prettyPrintUntypedLambda(untypedDef.term); + assertTermMatches(pp, 'λf.(λx.(f (x x)) λx.(f (x x)))'); + }); + + it('parses and loads the complete program and resolves the refs', () => { + const input = loadInput('complete.trip', __dirname); + const program = parseTripLang(input); + + assert(program.terms.length === 18); + + const syms = indexSymbols(program); + + const resolved = resolveRefs(program, syms); + + assert(resolved.terms.length === 18); + }); + + it('elaborates nested type applications correctly', () => { + const input = loadInput('nestedTypeApps.trip', __dirname); + const program = parseTripLang(input); + + const succTermParsed = program.terms.find(t => t.kind === 'poly' && t.name === 'succ'); + + if(succTermParsed!.kind !== 'poly' || !isSystemFTerm(succTermParsed!.term)) { + throw new Error('Missing succ definition after parse'); + } + + const succParsedPretty = prettyPrintSystemF(succTermParsed!.term); + + assertTermMatches(succParsedPretty, 'λn:Nat.ΛX.λs:(X→X).λz:X.(s (n[X] s z))'); + + const syms = indexSymbols(program); + const resolved = resolveRefs(program, syms); + + const succTermResolved = resolved.terms.find(t => t.kind === 'poly' && t.name === 'succ'); + + if(succTermResolved!.kind !== 'poly' || !isSystemFTerm(succTermResolved!.term)) { + throw new Error('Missing succ resolved definition'); + } + + const succResolvedPretty = prettyPrintSystemF(succTermResolved!.term); + + assertTermMatches(succResolvedPretty, 'λn:∀X.((X→X)→(X→X)).ΛX.λs:(X→X).λz:X.(s (n[X] s z))'); + }); + + it('compiles the complete program', () => { + const input = loadInput('complete.trip', __dirname); + const compiled = compile(input); + + const actualLength = compiled.program.terms.length; + const actualKind = compiled.program.terms[17]?.kind; + + // Assert number of types + const typeCount = keyValuePairs(compiled.types).length; + assert.equal(typeCount, 14, `Expected 14 types, got ${String(typeCount)}`); + + // Assert all types and their IDs + for (const [id, type] of keyValuePairs(compiled.types)) { + const typeStr = prettyPrintTy(type); + switch (id) { + case 'cond': + assertTermMatches(typeStr, '∀X.(∀B.(B→(B→B))→(X→(X→X)))'); + break; + case 'fact': + assertTermMatches(typeStr, '(∀X.((X→X)→(X→X))→∀X.((X→X)→(X→X)))'); + break; + case 'factKernel': + assertTermMatches(typeStr, '((∀X.((X→X)→(X→X))→∀X.((X→X)→(X→X)))→(∀X.((X→X)→(X→X))→∀X.((X→X)→(X→X))))'); + break; + case 'false': + assertTermMatches(typeStr, '∀B.(B→(B→B))'); + break; + case 'three': + assertTermMatches(typeStr, '∀a.((a→a)→(a→a))'); + break; + case 'fst': + assertTermMatches(typeStr, '∀A.∀B.(∀Y.((A→(B→Y))→Y)→A)'); + break; + case 'isZero': + assertTermMatches(typeStr, '(∀X.((X→X)→(X→X))→∀B.(B→(B→B)))'); + break; + case 'mul': + assertTermMatches(typeStr, '(∀X.((X→X)→(X→X))→(∀X.((X→X)→(X→X))→∀a.((a→a)→(a→a))))'); + break; + case 'one': + assertTermMatches(typeStr, '∀a.((a→a)→(a→a))'); + break; + case 'pair': + assertTermMatches(typeStr, '∀A.∀B.(A→(B→∀Y.((A→(B→Y))→Y)))'); + break; + case 'pred': + assertTermMatches(typeStr, '(∀X.((X→X)→(X→X))→∀X.((X→X)→(X→X)))'); + break; + case 'snd': + assertTermMatches(typeStr, '∀A.∀B.(∀Y.((A→(B→Y))→Y)→B)'); + break; + case 'succ': + assertTermMatches(typeStr, '(∀X.((X→X)→(X→X))→∀a.((a→a)→(a→a)))'); + break; + case 'true': + assertTermMatches(typeStr, '∀B.(B→(B→B))'); + break; + case 'zero': + assertTermMatches(typeStr, '∀X.((X→X)→(X→X))'); + break; + default: + assert.fail(`Unexpected type ID: ${id}`); + } + } + + assert(actualLength === 18, `Expected 18 terms, got ${String(actualLength)}`); + assert(actualKind === 'untyped', `Expected kind 'untyped', got '${String(actualKind)}'`); + + const mainTerm = compiled.program.terms[17].term; + const mainSKI = bracketLambda(mainTerm); + const factResult = reduce(mainSKI); + const result = UnChurchNumber(factResult); + assert.equal(result, 24, `Expected 24, got ${String(result)}`); + }); +}); diff --git a/test/meta/frontend/elaboration.test.ts b/test/meta/frontend/elaboration.test.ts new file mode 100644 index 0000000..76c8708 --- /dev/null +++ b/test/meta/frontend/elaboration.test.ts @@ -0,0 +1,221 @@ +import { expect } from 'chai'; +import { elaborateSystemF } from '../../../lib/meta/frontend/elaboration.js'; +import { SymbolTable } from '../../../lib/meta/trip.js'; +import { mkSystemFVar, mkSystemFTypeApp, mkSystemFTAbs, mkSystemFAbs, mkSystemFApp } from '../../../lib/terms/systemF.js'; +import { insertAVL, createEmptyAVL } from '../../../lib/data/avl/avlNode.js'; +import { compareStrings } from '../../../lib/data/map/stringMap.js'; +import { BaseType, arrow } from '../../../lib/types/types.js'; + +describe('elaborateSystemF', () => { + function createSymbolTable(types: { name: string; type: BaseType }[]): SymbolTable { + const table: SymbolTable = { + terms: createEmptyAVL(), + types: createEmptyAVL() + }; + + for (const { name, type } of types) { + table.types = insertAVL(table.types, name, { kind: 'type', name, type }, compareStrings); + } + + return table; + } + + it('should rewrite term applications as type applications when right-hand side is a type', () => { + const syms = createSymbolTable([ + { name: 'T', type: { kind: 'type-var', typeName: 'T' } } + ]); + + // Create expression: x T + const expr = mkSystemFApp( + mkSystemFVar('x'), + mkSystemFVar('T') + ); + + const result = elaborateSystemF(expr, syms); + + expect(result).to.deep.equal( + mkSystemFTypeApp( + mkSystemFVar('x'), + { kind: 'type-var', typeName: 'T' } + ) + ); + }); + + it('should handle nested type applications', () => { + const syms = createSymbolTable([ + { name: 'T', type: { kind: 'type-var', typeName: 'T' } }, + { name: 'U', type: { kind: 'type-var', typeName: 'U' } } + ]); + + // Create expression: (x T) U + const expr = mkSystemFApp( + mkSystemFApp( + mkSystemFVar('x'), + mkSystemFVar('T') + ), + mkSystemFVar('U') + ); + + const result = elaborateSystemF(expr, syms); + + expect(result).to.deep.equal( + mkSystemFTypeApp( + mkSystemFTypeApp( + mkSystemFVar('x'), + { kind: 'type-var', typeName: 'T' } + ), + { kind: 'type-var', typeName: 'U' } + ) + ); + }); + + it('should not rewrite applications when right-hand side is not a type', () => { + const syms = createSymbolTable([ + { name: 'T', type: { kind: 'type-var', typeName: 'T' } } + ]); + + // Create expression: x y + const expr = mkSystemFApp( + mkSystemFVar('x'), + mkSystemFVar('y') + ); + + const result = elaborateSystemF(expr, syms); + + expect(result).to.deep.equal( + mkSystemFApp( + mkSystemFVar('x'), + mkSystemFVar('y') + ) + ); + }); + + it('should handle mixed type and term applications', () => { + const syms = createSymbolTable([ + { name: 'T', type: { kind: 'type-var', typeName: 'T' } } + ]); + + // Create expression: (x T) y + const expr = mkSystemFApp( + mkSystemFApp( + mkSystemFVar('x'), + mkSystemFVar('T') + ), + mkSystemFVar('y') + ); + + const result = elaborateSystemF(expr, syms); + + expect(result).to.deep.equal( + mkSystemFApp( + mkSystemFTypeApp( + mkSystemFVar('x'), + { kind: 'type-var', typeName: 'T' } + ), + mkSystemFVar('y') + ) + ); + }); + + it('should handle type abstractions correctly', () => { + const syms = createSymbolTable([ + { name: 'T', type: { kind: 'type-var', typeName: 'T' } } + ]); + + // Create expression: ΛX. x T + const expr = mkSystemFTAbs( + 'X', + mkSystemFApp( + mkSystemFVar('x'), + mkSystemFVar('T') + ) + ); + + const result = elaborateSystemF(expr, syms); + + expect(result).to.deep.equal( + mkSystemFTAbs( + 'X', + mkSystemFTypeApp( + mkSystemFVar('x'), + { kind: 'type-var', typeName: 'T' } + ) + ) + ); + }); + + it('should handle polymorphic successor function correctly', () => { + const syms = createSymbolTable([ + { name: 'X', type: { kind: 'type-var', typeName: 'X' } } + ]); + + // Create expression: λn:Nat.ΛX.λs:(X→X).λz:X.(s (n[X] s z)) + const expr = mkSystemFAbs( + 'n', + { kind: 'type-var', typeName: 'Nat' }, + mkSystemFTAbs( + 'X', + mkSystemFAbs( + 's', + arrow( + { kind: 'type-var', typeName: 'X' }, + { kind: 'type-var', typeName: 'X' } + ), + mkSystemFAbs( + 'z', + { kind: 'type-var', typeName: 'X' }, + mkSystemFApp( + mkSystemFVar('s'), + mkSystemFApp( + mkSystemFTypeApp( + mkSystemFVar('n'), + { kind: 'type-var', typeName: 'X' } + ), + mkSystemFApp( + mkSystemFVar('s'), + mkSystemFVar('z') + ) + ) + ) + ) + ) + ) + ); + + const result = elaborateSystemF(expr, syms); + + expect(result).to.deep.equal( + mkSystemFAbs( + 'n', + { kind: 'type-var', typeName: 'Nat' }, + mkSystemFTAbs( + 'X', + mkSystemFAbs( + 's', + arrow( + { kind: 'type-var', typeName: 'X' }, + { kind: 'type-var', typeName: 'X' } + ), + mkSystemFAbs( + 'z', + { kind: 'type-var', typeName: 'X' }, + mkSystemFApp( + mkSystemFVar('s'), + mkSystemFApp( + mkSystemFTypeApp( + mkSystemFVar('n'), + { kind: 'type-var', typeName: 'X' } + ), + mkSystemFApp( + mkSystemFVar('s'), + mkSystemFVar('z') + ) + ) + ) + ) + ) + ) + ) + ); + }); +}); diff --git a/test/meta/frontend/externalReferences.test.ts b/test/meta/frontend/externalReferences.test.ts new file mode 100644 index 0000000..d8ec21f --- /dev/null +++ b/test/meta/frontend/externalReferences.test.ts @@ -0,0 +1,79 @@ +import { assert } from 'chai'; +import { externalReferences } from '../../../lib/meta/frontend/externalReferences.js'; +import { keyValuePairs } from '../../../lib/data/avl/avlNode.js'; +import { parseTripLang } from '../../../lib/parser/tripLang.js'; +import { resolveDefTerm } from '../../../lib/meta/frontend/symbolTable.js'; + +describe('externalReferences', () => { + it('identifies external references in a simple lambda abstraction', () => { + const input = 'poly id = λx:A.x'; + const program = parseTripLang(input); + const [termRefs, typeRefs] = externalReferences(resolveDefTerm(program.terms[0])); + + assert.deepStrictEqual(keyValuePairs(termRefs).map(kvp => kvp[0]), []); + assert.deepStrictEqual(keyValuePairs(typeRefs).map(kvp => kvp[0]), ['A']); + }); + + it('identifies external references in a System F term', () => { + const input = 'poly id = ΛX.λx:X.x'; + const program = parseTripLang(input); + const [termRefs, typeRefs] = externalReferences(resolveDefTerm(program.terms[0])); + + assert.deepStrictEqual(keyValuePairs(termRefs).map(kvp => kvp[0]), []); + assert.deepStrictEqual(keyValuePairs(typeRefs).map(kvp => kvp[0]), []); + }); + + it('identifies external references in a term with free variables', () => { + const input = 'poly free = λx:A.y'; + const program = parseTripLang(input); + const [termRefs, typeRefs] = externalReferences(resolveDefTerm(program.terms[0])); + + assert.deepStrictEqual(keyValuePairs(termRefs).map(kvp => kvp[0]), ['y']); + assert.deepStrictEqual(keyValuePairs(typeRefs).map(kvp => kvp[0]), ['A']); + }); + + it('identifies external references in a System F term with free type variables', () => { + const input = 'poly freeType = ΛX.λx:Y.x'; + const program = parseTripLang(input); + const [termRefs, typeRefs] = externalReferences(resolveDefTerm(program.terms[0])); + + assert.deepStrictEqual(keyValuePairs(termRefs).map(kvp => kvp[0]), []); + assert.deepStrictEqual(keyValuePairs(typeRefs).map(kvp => kvp[0]), ['Y']); + }); + + it('identifies external references in a complex term', () => { + const input = 'poly complex = λx:A.λy:B.(x (y z))'; + const program = parseTripLang(input); + const [termRefs, typeRefs] = externalReferences(resolveDefTerm(program.terms[0])); + + assert.deepStrictEqual(keyValuePairs(termRefs).map(kvp => kvp[0]), ['z']); + assert.deepStrictEqual(keyValuePairs(typeRefs).map(kvp => kvp[0]), ['A', 'B']); + }); + + it('identifies external references in a System F term with type application', () => { + const input = 'poly typeApp = ΛX.λx:X.(x[Y])'; + const program = parseTripLang(input); + const [termRefs, typeRefs] = externalReferences(resolveDefTerm(program.terms[0])); + + assert.deepStrictEqual(keyValuePairs(termRefs).map(kvp => kvp[0]), []); + assert.deepStrictEqual(keyValuePairs(typeRefs).map(kvp => kvp[0]), ['Y']); + }); + + it('identifies external references in a non-terminal term', () => { + const input = 'poly app = (x y)'; + const program = parseTripLang(input); + const [termRefs, typeRefs] = externalReferences(resolveDefTerm(program.terms[0])); + + assert.deepStrictEqual(keyValuePairs(termRefs).map(kvp => kvp[0]), ['x', 'y']); + assert.deepStrictEqual(keyValuePairs(typeRefs).map(kvp => kvp[0]), []); + }); + + it('identifies external references in a term with nested abstractions', () => { + const input = 'poly nested = λx:A.λy:B.(λz:C.(x y z))'; + const program = parseTripLang(input); + const [termRefs, typeRefs] = externalReferences(resolveDefTerm(program.terms[0])); + + assert.deepStrictEqual(keyValuePairs(termRefs).map(kvp => kvp[0]), []); + assert.deepStrictEqual(keyValuePairs(typeRefs).map(kvp => kvp[0]), ['A', 'B', 'C']); + }); +}); diff --git a/test/meta/frontend/substitution.test.ts b/test/meta/frontend/substitution.test.ts new file mode 100644 index 0000000..7244f2a --- /dev/null +++ b/test/meta/frontend/substitution.test.ts @@ -0,0 +1,144 @@ +import { assert } from 'chai'; +import { substitute } from '../../../lib/meta/frontend/substitution.js'; +import { CompilationError } from '../../../lib/meta/frontend/compilation.js'; +import { SystemFTerm, mkSystemFVar, mkSystemFAbs, mkSystemFTAbs, mkSystemFTypeApp, mkSystemFApp } from '../../../lib/terms/systemF.js'; + +describe('Substitution', () => { + describe('substitute', () => { + it('should throw on invalid type', () => { + const type = { kind: 'invalid' } as unknown; + + assert.throws( + () => substitute( + type as SystemFTerm, + () => [], + () => false, + n => n, + () => true, + (n, rebuilt) => { + throw new CompilationError( + 'Substitution failed: no result found', 'resolve', + { term: n, substitutions: rebuilt }); + } + ), + CompilationError, + 'Substitution failed: no result found' + ); + }); + + it('should substitute a variable with a term', () => { + const varTerm = mkSystemFVar('x'); + const replacement = mkSystemFVar('y'); + + const result = substitute( + varTerm, + () => [], + n => n.kind === 'systemF-var' && n.name === 'x', + () => replacement, + () => false, + n => n + ); + + assert.deepEqual(result, replacement); + }); + + it('should substitute within a term abstraction', () => { + const absTerm = mkSystemFAbs('x', { kind: 'type-var', typeName: 'T' }, mkSystemFVar('x')); + const replacement = mkSystemFVar('y'); + + const result = substitute( + absTerm, + n => n.kind === 'systemF-abs' ? [n.body] : [], + n => n.kind === 'systemF-var' && n.name === 'x', + () => replacement, + n => n.kind === 'systemF-abs', + (n, rebuilt) => { + if (n.kind === 'systemF-abs') { + return mkSystemFAbs(n.name, n.typeAnnotation, rebuilt.pop()!); + } + return n; + } + ); + + assert.deepEqual(result, mkSystemFAbs('x', { kind: 'type-var', typeName: 'T' }, replacement)); + }); + + it('should substitute within a type abstraction', () => { + const typeAbs = mkSystemFTAbs('X', mkSystemFVar('x')); + const replacement = mkSystemFVar('y'); + + const result = substitute( + typeAbs, + n => n.kind === 'systemF-type-abs' ? [n.body] : [], + n => n.kind === 'systemF-var' && n.name === 'x', + () => replacement, + n => n.kind === 'systemF-type-abs', + (n, rebuilt) => { + if (n.kind === 'systemF-type-abs') { + return mkSystemFTAbs(n.typeVar, rebuilt.pop()!); + } + return n; + } + ); + + assert.deepEqual(result, mkSystemFTAbs('X', replacement)); + }); + + it('should substitute within a type application', () => { + const typeApp = mkSystemFTypeApp(mkSystemFVar('x'), { kind: 'type-var', typeName: 'T' }); + const replacement = mkSystemFVar('y'); + + const result = substitute( + typeApp, + n => n.kind === 'systemF-type-app' ? [n.term] : [], + n => n.kind === 'systemF-var' && n.name === 'x', + () => replacement, + n => n.kind === 'systemF-type-app', + (n, rebuilt) => { + if (n.kind === 'systemF-type-app') { + return mkSystemFTypeApp(rebuilt.pop()!, n.typeArg); + } + return n; + } + ); + + assert.deepEqual(result, mkSystemFTypeApp(replacement, { kind: 'type-var', typeName: 'T' })); + }); + + it('should handle nested term substitution', () => { + const nestedTerm = mkSystemFApp( + mkSystemFAbs('x', { kind: 'type-var', typeName: 'T' }, mkSystemFVar('x')), + mkSystemFVar('y') + ); + const replacement = mkSystemFVar('z'); + + const result = substitute( + nestedTerm, + n => { + if (n.kind === 'non-terminal') return [n.lft, n.rgt]; + if (n.kind === 'systemF-abs') return [n.body]; + return []; + }, + n => n.kind === 'systemF-var' && n.name === 'y', + () => replacement, + n => n.kind === 'non-terminal' || n.kind === 'systemF-abs', + (n, rebuilt) => { + if (n.kind === 'non-terminal') { + return mkSystemFApp(rebuilt.pop()!, rebuilt.pop()!); + } + if (n.kind === 'systemF-abs') { + return mkSystemFAbs(n.name, n.typeAnnotation, rebuilt.pop()!); + } + return n; + } + ); + + const expected = mkSystemFApp( + mkSystemFAbs('x', { kind: 'type-var', typeName: 'T' }, mkSystemFVar('x')), + replacement + ); + + assert.deepEqual(result, expected); + }); + }); +}); diff --git a/test/meta/frontend/symbolTable.test.ts b/test/meta/frontend/symbolTable.test.ts new file mode 100644 index 0000000..6eeda2b --- /dev/null +++ b/test/meta/frontend/symbolTable.test.ts @@ -0,0 +1,121 @@ +import { assert } from 'chai'; +import { indexSymbols, resolveDefTerm } from '../../../lib/meta/frontend/symbolTable.js'; +import { TripLangProgram, PolyDefinition, TypedDefinition, TypeDefinition } from '../../../lib/meta/trip.js'; +import { CompilationError } from '../../../lib/meta/frontend/compilation.js'; +import { searchAVL } from '../../../lib/data/avl/avlNode.js'; +import { compareStrings } from '../../../lib/data/map/stringMap.js'; + +describe('Symbol Table', () => { + describe('indexSymbols', () => { + it('should index a program with unique terms and types', () => { + const program: TripLangProgram = { + kind: 'program', + terms: [ + { + kind: 'poly', + name: 'id', + term: { kind: 'systemF-var', name: 'x' } + }, + { + kind: 'type', + name: 'Nat', + type: { kind: 'type-var', typeName: 'X' } + } + ] + }; + + const symbols = indexSymbols(program); + const term = searchAVL(symbols.terms, 'id', compareStrings); + const type = searchAVL(symbols.types, 'Nat', compareStrings); + + assert.isDefined(term); + assert.isDefined(type); + assert.deepStrictEqual(term, program.terms[0]); + assert.deepStrictEqual(type, program.terms[1]); + }); + + it('should throw on duplicate term definitions', () => { + const program: TripLangProgram = { + kind: 'program', + terms: [ + { + kind: 'poly', + name: 'id', + term: { kind: 'systemF-var', name: 'x' } + }, + { + kind: 'poly', + name: 'id', + term: { kind: 'systemF-var', name: 'y' } + } + ] + }; + + assert.throws( + () => indexSymbols(program), + CompilationError, + 'Duplicate definition: id' + ); + }); + + it('should throw on duplicate type definitions', () => { + const program: TripLangProgram = { + kind: 'program', + terms: [ + { + kind: 'type', + name: 'Nat', + type: { kind: 'type-var', typeName: 'X' } + }, + { + kind: 'type', + name: 'Nat', + type: { kind: 'type-var', typeName: 'Y' } + } + ] + }; + + assert.throws( + () => indexSymbols(program), + CompilationError, + 'Duplicate type' + ); + }); + }); + + describe('resolveDefTerm', () => { + it('should resolve poly term definition', () => { + const term: PolyDefinition = { + kind: 'poly', + name: 'id', + term: { kind: 'systemF-var', name: 'x' } + }; + + const resolved = resolveDefTerm(term); + assert.deepStrictEqual(resolved, { kind: 'systemF-var', name: 'x' }); + }); + + it('should resolve typed term definition', () => { + const term: TypedDefinition = { + kind: 'typed', + name: 'id', + type: { kind: 'type-var', typeName: 'X' }, + term: { kind: 'lambda-var', name: 'x' } + }; + + const resolved = resolveDefTerm(term); + assert.deepStrictEqual(resolved, { kind: 'lambda-var', name: 'x' }); + }); + + it('should resolve type definition', () => { + const term: TypeDefinition = { + kind: 'type', + name: 'Nat', + type: { kind: 'type-var', typeName: 'X' } + }; + + const resolved = resolveDefTerm(term); + assert.deepStrictEqual(resolved, { kind: 'type-var', typeName: 'X' }); + }); + }); +}); diff --git a/test/meta/inputs/complete.trip b/test/meta/inputs/complete.trip new file mode 100644 index 0000000..d26229a --- /dev/null +++ b/test/meta/inputs/complete.trip @@ -0,0 +1,72 @@ +type Nat = ∀X . (X → X) → X → X +type Bool = ∀B. B → B → B + +poly true = ΛB . λt:B . λf:B . t +poly false = ΛB . λt:B . λf:B . f +poly zero = ΛX . λs: X → X . λz : X . z +poly isZero = + λn : Nat . + n [Bool] + (λb : Bool . false) + true + +poly cond = + ΛX . + λb : Bool . + λt : X . + λf : X . + b [X] t f + +poly succ = + λn : Nat . + Λa. λs : a → a . λz : a . + s (n [a] s z) + +poly pair = ΛA . ΛB . λa : A . λb : B . ΛY . λk : A → B → Y . k a b + +poly fst = ΛA . ΛB . λp : ∀Y . (A→B→Y)→Y . + p [A] (λx:A . λy:B . x) + +poly snd = ΛA . ΛB . λp : ∀Y . (A→B→Y)→Y . + p [B] (λx:A . λy:B . y) + +poly pred = λn : Nat . + fst Nat Nat + ( + n [∀Y . (Nat → Nat → Y) → Y] + (λp : ∀Y . (Nat → Nat → Y) → Y . + pair Nat Nat + (snd Nat Nat p) + (succ (snd Nat Nat p)) + ) + (pair Nat Nat zero zero) + ) + +poly mul = + λm : Nat . λn : Nat . + Λa . λs : a → a . λz : a . + m [a] (n [a] s) z + +untyped fix = λf.(λx. f (x x))(λx. f (x x)) + +poly one = succ zero + +poly factKernel = + λself : Nat → Nat . λn : Nat . + cond [Nat] + (isZero n) + one + (mul n (self (pred n))) + +poly fact = λn : Nat . + fst Nat Nat + (n [∀Y . (Nat → Nat → Y) → Y] + (λp : ∀Y . (Nat → Nat → Y) → Y . + pair Nat Nat + (mul (fst Nat Nat p) (snd Nat Nat p)) + (succ (snd Nat Nat p)) + ) + (pair Nat Nat one one) + ) + +untyped main = fact (succ (succ (succ (succ zero)))) \ No newline at end of file diff --git a/test/meta/inputs/condSucc.trip b/test/meta/inputs/condSucc.trip new file mode 100644 index 0000000..afbab32 --- /dev/null +++ b/test/meta/inputs/condSucc.trip @@ -0,0 +1,11 @@ +poly cond = + ΛX . + λb : Bool . + λt : X . + λf : X . + b [X] t f + +poly succ = + λn : Nat . + Λa. λs : a → a . λz : a . + s (n [a] s z) \ No newline at end of file diff --git a/test/meta/inputs/fact.trip b/test/meta/inputs/fact.trip new file mode 100644 index 0000000..49c7b23 --- /dev/null +++ b/test/meta/inputs/fact.trip @@ -0,0 +1,13 @@ +poly one = succ zero + +poly factKernel = + (λself : Nat → Nat . λn : Nat . + cond + [Nat] (isZero n) one + (mul n (self (pred n)))) + +untyped fact = fix factKernel + +poly five = succ succ succ succ succ zero + +untyped main = fact five diff --git a/test/meta/inputs/fix.trip b/test/meta/inputs/fix.trip new file mode 100644 index 0000000..703a5ea --- /dev/null +++ b/test/meta/inputs/fix.trip @@ -0,0 +1 @@ +untyped fix = λf.(λx. f (x x))(λx. f (x x)) diff --git a/test/meta/inputs/mul.trip b/test/meta/inputs/mul.trip new file mode 100644 index 0000000..6a33214 --- /dev/null +++ b/test/meta/inputs/mul.trip @@ -0,0 +1,4 @@ +poly mul = + λm : Nat . λn : Nat . + Λa . λs : a → a . λz : a . + m [a] s (n [a] s z) diff --git a/test/meta/inputs/natBool.trip b/test/meta/inputs/natBool.trip new file mode 100644 index 0000000..d09a122 --- /dev/null +++ b/test/meta/inputs/natBool.trip @@ -0,0 +1,2 @@ +type Nat = ∀X . (X → X) → X → X +type Bool = ∀B. B → B → B diff --git a/test/meta/inputs/nestedTypeApps.trip b/test/meta/inputs/nestedTypeApps.trip new file mode 100644 index 0000000..6b9e484 --- /dev/null +++ b/test/meta/inputs/nestedTypeApps.trip @@ -0,0 +1,7 @@ +type Nat = ∀X.((X→X)→(X→X)) +type Bool = ∀B.(B→(B→B)) +poly true = ΛB.λt:B.λf:B.t +poly false = ΛB.λt:B.λf:B.f +poly zero = ΛX.λs:(X→X).λz:X.z +poly succ = λn:Nat.ΛX.λs:(X→X).λz:X.(s (n[X] s z)) +poly pred = λn:Nat.(n[Bool] λb:Bool.false true) diff --git a/test/meta/inputs/pair.trip b/test/meta/inputs/pair.trip new file mode 100644 index 0000000..5092b95 --- /dev/null +++ b/test/meta/inputs/pair.trip @@ -0,0 +1,7 @@ +poly pair = ΛA . ΛB . λa : A . λb : B . ΛY . λk : A → B → Y . k a b + +poly fst = ΛA . ΛB . λp : ∀Y . (A→B→Y)→Y . + p [A] (λx:A . λy:B . x) + +poly snd = ΛA . ΛB . λp : ∀Y . (A→B→Y)→Y . + p [B] (λx:A . λy:B . x) \ No newline at end of file diff --git a/test/meta/inputs/pred.trip b/test/meta/inputs/pred.trip new file mode 100644 index 0000000..d99130d --- /dev/null +++ b/test/meta/inputs/pred.trip @@ -0,0 +1,10 @@ +poly pred = λn : Nat . + fst Nat Nat + ( + n [∀Y . (Nat → Nat → Y) → Y] + (λp : ∀Y . (Nat → Nat → Y) → Y . + pair Nat Nat + (snd Nat Nat p) + (succ (snd Nat Nat p)) + (pair Nat Nat zero zero)) + ) \ No newline at end of file diff --git a/test/meta/inputs/trueFalseZero.trip b/test/meta/inputs/trueFalseZero.trip new file mode 100644 index 0000000..9de76ad --- /dev/null +++ b/test/meta/inputs/trueFalseZero.trip @@ -0,0 +1,10 @@ +poly true = ΛB . λt:B . λf:B . t +poly false = ΛB . λt:B . λf:B . f +poly zero = ΛX . λs: X → X . λz : X . z +poly isZero = + λn : Nat . + n [Bool] + (λb : Bool . false) + true +type Bool = ∀B. B → B → B +type Nat = ∀X . (X → X) → X → X \ No newline at end of file diff --git a/test/parser/tripLang.test.ts b/test/parser/tripLang.test.ts index 937bf4d..4b7c4fa 100644 --- a/test/parser/tripLang.test.ts +++ b/test/parser/tripLang.test.ts @@ -1,6 +1,5 @@ import { expect } from 'chai'; -import { readFileSync } from 'fs'; -import { dirname, resolve } from 'path'; +import { dirname } from 'path'; import { createParserState } from '../../lib/parser/parserState.js'; import { parseTripLang, parseTripLangDefinition } from '../../lib/parser/tripLang.js'; import { fileURLToPath } from 'url'; @@ -10,16 +9,13 @@ import { mkVar } from '../../lib/terms/lambda.js'; import { TypedLambda } from '../../lib/types/typedLambda.js'; import { SKIExpression } from '../../lib/ski/expression.js'; import { S, K, I } from '../../lib/ski/terminal.js'; +import { loadInput } from '../util/fileLoader.js'; -function loadInput(filename: string): string { - const __dirname = dirname(fileURLToPath(import.meta.url)); - const filePath = resolve(__dirname, 'inputs', filename); - return readFileSync(filePath, 'utf-8').trim(); -} +const __dirname = dirname(fileURLToPath(import.meta.url)); describe('parseTripLang', () => { it('parses polymorphic definitions', () => { - const input = loadInput('polyId.trip'); + const input = loadInput('polyId.trip', __dirname); const [term] = parseTripLangDefinition(createParserState(input)); expect(term).to.deep.equal({ @@ -33,7 +29,7 @@ describe('parseTripLang', () => { }); it('parses typed definitions with explicit types', () => { - const input = loadInput('typedInc.trip'); + const input = loadInput('typedInc.trip', __dirname); const [term] = parseTripLangDefinition(createParserState(input)); expect(term).to.deep.equal({ @@ -56,7 +52,7 @@ describe('parseTripLang', () => { }); it('parses untyped definitions', () => { - const input = loadInput('untypedDouble.trip'); + const input = loadInput('untypedDouble.trip', __dirname); const [term] = parseTripLangDefinition(createParserState(input)); expect(term).to.deep.equal({ @@ -74,7 +70,7 @@ describe('parseTripLang', () => { }); it('parses complex combinator definitions', () => { - const input = loadInput('combinatorY.trip'); + const input = loadInput('combinatorY.trip', __dirname); const [term] = parseTripLangDefinition(createParserState(input)); expect(term).to.deep.equal({ @@ -115,7 +111,7 @@ describe('parseTripLang', () => { }); it('parses type definitions correctly', () => { - const input = loadInput('typeNat.trip'); + const input = loadInput('typeNat.trip', __dirname); const [term] = parseTripLangDefinition(createParserState(input)); const typeVar = (name: string) => ({ kind: 'type-var', typeName: name }); @@ -136,7 +132,7 @@ describe('parseTripLang', () => { }); it('parses multiple definitions', () => { - const input = loadInput('church.trip'); + const input = loadInput('church.trip', __dirname); const program = parseTripLang(input); const typeVar = (name: string) => ({ kind: 'type-var' as const, typeName: name }); const X = typeVar('X'); diff --git a/test/ski/church.test.ts b/test/ski/church.test.ts index 4c3d773..0e171c5 100644 --- a/test/ski/church.test.ts +++ b/test/ski/church.test.ts @@ -5,7 +5,7 @@ import { V, Succ, Fst, Snd, Car, Cdr, F, True, False, Plus, Zero, B } from '../. import { reduce } from '../../lib/evaluator/skiEvaluator.js'; import { UnChurchNumber, ChurchN, ChurchB, UnChurchBoolean } from '../../lib/ski/church.js'; import { S, K, I } from '../../lib/ski/terminal.js'; -import { convertLambda } from '../../lib/conversion/converter.js'; +import { bracketLambda } from '../../lib/conversion/converter.js'; import { predLambda } from '../../lib/consts/lambdas.js'; import { apply } from '../../lib/ski/expression.js'; @@ -152,7 +152,7 @@ describe('Church encodings', () => { const pairZeroZero = apply(V, ChurchN(0), ChurchN(0)); it('computes the predecessor', () => { - const pred = convertLambda(predLambda); + const pred = bracketLambda(predLambda); // Test numbers from 0 to N-1 for (let m = 0; m < N; m++) { diff --git a/test/types/typedLambda.test.ts b/test/types/typedLambda.test.ts index 3e2c3e2..21030c0 100644 --- a/test/types/typedLambda.test.ts +++ b/test/types/typedLambda.test.ts @@ -3,13 +3,13 @@ import { describe, it } from 'mocha'; import { cons } from '../../lib/cons.js'; import { mkVar } from '../../lib/terms/lambda.js'; -import { addBinding, emptyContext, mkTypedAbs, typecheck } from '../../lib/types/typedLambda.js'; +import { addBinding, emptyContext, mkTypedAbs, typecheckTypedLambda } from '../../lib/types/typedLambda.js'; import { mkTypeVariable, arrow, typesLitEq, arrows } from '../../lib/types/types.js'; describe('type checking errors', () => { it('throws an error for free variables', () => { // Create a term with a free variable: just the variable "x" with no binding. - expect(() => typecheck(mkVar('x'))).to.throw(/unknown term named: x/); + expect(() => typecheckTypedLambda(mkVar('x'))).to.throw(/unknown term named: x/); }); it('throws an error on duplicate binding', () => { @@ -24,7 +24,7 @@ describe('type checking', () => { it('typechecks the I combinator', () => { // λx : a . x ≡ I : a -> a const typedI = mkTypedAbs('x', mkTypeVariable('a'), mkVar('x')); - const typeofI = typecheck(typedI); + const typeofI = typecheckTypedLambda(typedI); const expectedTy = arrow(mkTypeVariable('a'), mkTypeVariable('a')); expect(typesLitEq(typeofI, expectedTy)).to.equal(true); }); @@ -37,7 +37,7 @@ describe('type checking', () => { mkVar('x') // x ) ); - const typeofK = typecheck(typedK); + const typeofK = typecheckTypedLambda(typedK); const expectedTy = arrows(mkTypeVariable('a'), mkTypeVariable('b'), mkTypeVariable('a')); expect(typesLitEq(typeofK, expectedTy)).to.equal(true); @@ -71,7 +71,7 @@ describe('type checking', () => { arrows(mkTypeVariable('a'), mkTypeVariable('c')) ); - const typeofS = typecheck(typedS); + const typeofS = typecheckTypedLambda(typedS); expect(typesLitEq(typeofS, expectedTy)).to.equal(true); }); diff --git a/test/util/fileLoader.ts b/test/util/fileLoader.ts new file mode 100644 index 0000000..3307e6f --- /dev/null +++ b/test/util/fileLoader.ts @@ -0,0 +1,7 @@ +import { readFileSync } from 'fs'; +import { resolve } from 'path'; + +export function loadInput(filename: string, dirname: string): string { + const filePath = resolve(dirname, 'inputs', filename); + return readFileSync(filePath, 'utf-8').trim(); +} From cc2011756abec1c0dcd8842a15eab37079d6374d Mon Sep 17 00:00:00 2001 From: Max DeLiso Date: Sun, 18 May 2025 18:03:58 +0200 Subject: [PATCH 2/2] consistent newlines --- test/meta/inputs/complete.trip | 2 +- test/meta/inputs/condSucc.trip | 2 +- test/meta/inputs/pair.trip | 2 +- test/meta/inputs/pred.trip | 2 +- test/meta/inputs/trueFalseZero.trip | 2 +- 5 files changed, 5 insertions(+), 5 deletions(-) diff --git a/test/meta/inputs/complete.trip b/test/meta/inputs/complete.trip index d26229a..05bde95 100644 --- a/test/meta/inputs/complete.trip +++ b/test/meta/inputs/complete.trip @@ -69,4 +69,4 @@ poly fact = λn : Nat . (pair Nat Nat one one) ) -untyped main = fact (succ (succ (succ (succ zero)))) \ No newline at end of file +untyped main = fact (succ (succ (succ (succ zero)))) diff --git a/test/meta/inputs/condSucc.trip b/test/meta/inputs/condSucc.trip index afbab32..4ca8cb0 100644 --- a/test/meta/inputs/condSucc.trip +++ b/test/meta/inputs/condSucc.trip @@ -8,4 +8,4 @@ poly cond = poly succ = λn : Nat . Λa. λs : a → a . λz : a . - s (n [a] s z) \ No newline at end of file + s (n [a] s z) diff --git a/test/meta/inputs/pair.trip b/test/meta/inputs/pair.trip index 5092b95..a0acf60 100644 --- a/test/meta/inputs/pair.trip +++ b/test/meta/inputs/pair.trip @@ -4,4 +4,4 @@ poly fst = ΛA . ΛB . λp : ∀Y . (A→B→Y)→Y . p [A] (λx:A . λy:B . x) poly snd = ΛA . ΛB . λp : ∀Y . (A→B→Y)→Y . - p [B] (λx:A . λy:B . x) \ No newline at end of file + p [B] (λx:A . λy:B . x) diff --git a/test/meta/inputs/pred.trip b/test/meta/inputs/pred.trip index d99130d..4c74c38 100644 --- a/test/meta/inputs/pred.trip +++ b/test/meta/inputs/pred.trip @@ -7,4 +7,4 @@ poly pred = λn : Nat . (snd Nat Nat p) (succ (snd Nat Nat p)) (pair Nat Nat zero zero)) - ) \ No newline at end of file + ) diff --git a/test/meta/inputs/trueFalseZero.trip b/test/meta/inputs/trueFalseZero.trip index 9de76ad..e37009c 100644 --- a/test/meta/inputs/trueFalseZero.trip +++ b/test/meta/inputs/trueFalseZero.trip @@ -7,4 +7,4 @@ poly isZero = (λb : Bool . false) true type Bool = ∀B. B → B → B -type Nat = ∀X . (X → X) → X → X \ No newline at end of file +type Nat = ∀X . (X → X) → X → X