Skip to content

add a compiler frontend #19

New issue

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

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

Already on GitHub? Sign in to your account

Draft
wants to merge 2 commits into
base: main
Choose a base branch
from
Draft
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
8 changes: 4 additions & 4 deletions bin/ski.ts
Original file line number Diff line number Diff line change
Expand Up @@ -32,7 +32,7 @@ import {
prettyPrintSystemFType,
typecheckSystemF,
// Conversion
convertLambda,
bracketLambda,
// Types
prettyPrintTy,
inferType,
Expand Down Expand Up @@ -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) {
Expand All @@ -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');
}
Expand Down
2 changes: 1 addition & 1 deletion lib/conversion/converter.ts
Original file line number Diff line number Diff line change
Expand Up @@ -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);
Expand Down
20 changes: 20 additions & 0 deletions lib/data/avl/avlNode.ts
Original file line number Diff line number Diff line change
Expand Up @@ -293,3 +293,23 @@ export function keyValuePairs<TKey, TValue>(

return result;
}

export function emptyAVL<TKey, TValue>(
tr: AVLTree<TKey, TValue>
): boolean {
return keyValuePairs(tr).length === 0;
}

export function mergeAVL<TKey, TValue>(
a: AVLTree<TKey, TValue>,
b: AVLTree<TKey, TValue>,
compareKeys: (a: TKey, b: TKey) => number
): AVLTree<TKey, TValue> {
let result = a;

for (const [k, v] of keyValuePairs<TKey, TValue>(b)) {
result = insertAVL(result, k, v, compareKeys);
}

return result;
}
4 changes: 2 additions & 2 deletions lib/index.ts
Original file line number Diff line number Diff line change
Expand Up @@ -30,7 +30,7 @@ export {
eraseTypedLambda,
prettyPrintTypedLambda,
type TypedLambda,
typecheck as typecheckTyped
typecheckTypedLambda as typecheckTyped
} from './types/typedLambda.js';

// System F type exports
Expand All @@ -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';
Expand Down
5 changes: 5 additions & 0 deletions lib/meta/frontend.ts
Original file line number Diff line number Diff line change
@@ -0,0 +1,5 @@
import { TripLangProgram } from './trip.js';
import { compile } from './frontend/compilation.js';

export { compile };
export type { TripLangProgram };
21 changes: 21 additions & 0 deletions lib/meta/frontend/builders.ts
Original file line number Diff line number Diff line change
@@ -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<T extends SystemFTerm | TypedLambda | UntypedLambda>(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 [];
}
}
163 changes: 163 additions & 0 deletions lib/meta/frontend/compilation.ts
Original file line number Diff line number Diff line change
@@ -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<string, unknown>;
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<string, BaseType>;
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<string, BaseType>();

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);
}
62 changes: 62 additions & 0 deletions lib/meta/frontend/elaboration.ts
Original file line number Diff line number Diff line change
@@ -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);
}
}
}
Loading