Skip to content

Commit

Permalink
fix up the packaging, add an infer command
Browse files Browse the repository at this point in the history
  • Loading branch information
maxdeliso committed Feb 10, 2025
1 parent 9e76937 commit 73adb7f
Show file tree
Hide file tree
Showing 45 changed files with 475 additions and 304 deletions.
10 changes: 9 additions & 1 deletion .gitignore
Original file line number Diff line number Diff line change
@@ -1,3 +1,11 @@
node_modules/
build/
.vscode/
.vscode/
.yarn/*
!.yarn/cache
!.yarn/patches
!.yarn/plugins
!.yarn/releases
!.yarn/sdks
!.yarn/versions
*.tgz
1 change: 1 addition & 0 deletions .yarnrc.yml
Original file line number Diff line number Diff line change
@@ -0,0 +1 @@
nodeLinker: node-modules
4 changes: 2 additions & 2 deletions README.md
Original file line number Diff line number Diff line change
Expand Up @@ -8,8 +8,8 @@ In the checkout directory:

```bash
yarn install
yarn run build
yarn run ski
yarn build
yarn ski
```

## Books
Expand Down
80 changes: 59 additions & 21 deletions bin/ski.ts
Original file line number Diff line number Diff line change
Expand Up @@ -5,20 +5,40 @@ import tkexport from 'terminal-kit';
const { create } = rsexport;
const { terminal } = tkexport;

import { stepOnceImmediate, stepOnceSKI } from '../lib/evaluator/skiEvaluator.js';
import { generateExpr, SKIExpression, prettyPrint as prettyPrintSKI } from '../lib/ski/expression.js';
import { parseSKI } from '../lib/parser/ski.js';
import { prettyPrintUntypedLambda, UntypedLambda } from '../lib/terms/lambda.js';
import { parseLambda } from '../lib/parser/untyped.js';
import { prettyPrintSystemF, SystemFTerm } from '../lib/terms/systemF.js';
import { parseSystemF } from '../lib/parser/systemFTerm.js';
import { eraseTypedLambda, prettyPrintTypedLambda, TypedLambda } from '../lib/types/typedLambda.js';
import { parseTypedLambda } from '../lib/parser/typed.js';
import { eraseSystemF, prettyPrintSystemFType } from '../lib/types/systemF.js';
import { convertLambda } from '../lib/conversion/converter.js';
import { typecheck as typecheckTyped } from '../lib/types/typedLambda.js';
import { typecheck as typecheckSystemF } from '../lib/types/systemF.js';
import { prettyPrintTy } from '../lib/types/types.ts';
import {
// SKI evaluator
stepOnceImmediate,
stepOnceSKI,
// SKI expressions
generateExpr,
prettyPrintSKI,
type SKIExpression,
// Parsers
parseSKI,
parseLambda,
parseSystemF,
parseTypedLambda,
// Lambda terms
prettyPrintUntypedLambda,
type UntypedLambda,
// System F
prettyPrintSystemF,
type SystemFTerm,
// Typed Lambda
eraseTypedLambda,
prettyPrintTypedLambda,
type TypedLambda,
typecheckTyped,
// System F types
eraseSystemF,
prettyPrintSystemFType,
typecheckSystemF,
// Conversion
convertLambda,
// Types
prettyPrintTy,
inferType
} from '../lib/index.js';

enum Mode {
SKI = 'SKI',
Expand Down Expand Up @@ -282,6 +302,25 @@ function processCommand(input: string): void {
}
break;
}
}
else if (cmd === 'infer' || cmd === 'i') {
// This command infers the type for the current untyped Lambda expression.
if (currentMode !== Mode.Lambda) {
printYellow('Type inference is only available in Lambda mode.');
} else if (currentLambda === null) {
printRed('No current Lambda term available for type inference.');
} else {
try {
const [typed, inferredType] = inferType(currentLambda);
currentTypedLambda = typed;
// Switch to TypedLambda mode since we now have a typed term.
currentMode = Mode.TypedLambda;
printGreen('Inferred Typed Lambda term: ' + prettyPrintTypedLambda(currentTypedLambda));
printGreen('Inferred type: ' + prettyPrintTy(inferredType));
} catch (e) {
printRed('Type inference error: ' + String(e));
}
}
} else {
printYellow('unknown command: ' + input);
}
Expand All @@ -297,13 +336,12 @@ Available commands:
:mode [ski|lambda|typed|systemf] -- switch mode
:help -- display this help message
:quit -- exit the REPL
Evaluation commands (in SKI mode):
:s or :step -- step once (converts to SKI if necessary)
:m or :stepmany -- step many (max 100 iterations, in SKI mode)
:g or :generate -- generate a new SKI expression (SKI mode only)
:p or :print -- print the current term
Typechecking commands:
:tc or :typecheck -- typecheck the current term (only available in TypedLambda and SystemF modes)
:s or :step -- step once (converts to SKI if necessary)
:m or :stepmany -- step many (max 100 iterations, in SKI mode)
:g or :generate -- generate a new SKI expression (SKI mode only)
:p or :print -- print the current term
:tc or :typecheck -- typecheck the current term (only available in TypedLambda and SystemF modes)
:infer or :i -- infer the type for the current untyped Lambda term and switch to TypedLambda mode
Any other input is interpreted as a new term for the current mode.
Press CTRL+C or type :quit to exit.`);
Expand Down
6 changes: 3 additions & 3 deletions lib/consts/combinators.ts
Original file line number Diff line number Diff line change
@@ -1,6 +1,6 @@
import { parseSKI } from '../parser/ski.ts';
import { apply } from '../ski/expression.ts';
import { K, I, S } from '../ski/terminal.ts';
import { parseSKI } from '../parser/ski.js';
import { apply } from '../ski/expression.js';
import { S, K, I } from '../ski/terminal.js';

/*
* Zero. apply a function to its arguments zero times.
Expand Down
2 changes: 1 addition & 1 deletion lib/consts/lambdas.ts
Original file line number Diff line number Diff line change
@@ -1,3 +1,3 @@
import { parseLambda } from '../parser/untyped.ts';
import { parseLambda } from '../parser/untyped.js';

export const [, predLambda] = parseLambda('λn.λf.λx.n(λg.λh.h(gf))(λu.x)(λu.u)');
12 changes: 6 additions & 6 deletions lib/conversion/converter.ts
Original file line number Diff line number Diff line change
@@ -1,9 +1,9 @@
import { ConsCell, cons } from '../cons.ts';
import { C, B } from '../consts/combinators.ts';
import { LambdaVar, UntypedLambda } from '../terms/lambda.ts';
import { SKIExpression } from '../ski/expression.ts';
import { S, K, I, SKITerminal } from '../ski/terminal.ts';
import { ConversionError } from './conversionError.ts';
import { ConsCell, cons } from '../cons.js';
import { C, B } from '../consts/combinators.js';
import { LambdaVar, UntypedLambda } from '../terms/lambda.js';
import { SKIExpression } from '../ski/expression.js';
import { S, K, I, SKITerminal } from '../ski/terminal.js';
import { ConversionError } from './conversionError.js';

/**
* Internal mixed-domain lambda abstraction.
Expand Down
6 changes: 3 additions & 3 deletions lib/evaluator/skiEvaluator.ts
Original file line number Diff line number Diff line change
@@ -1,6 +1,6 @@
import { cons, ConsCell } from '../cons.ts';
import { prettyPrint, SKIExpression } from '../ski/expression.ts';
import { SKITerminalSymbol } from '../ski/terminal.ts';
import { cons, ConsCell } from '../cons.js';
import { prettyPrint, SKIExpression } from '../ski/expression.js';
import { SKITerminalSymbol } from '../ski/terminal.js';

/**
* the shape of an evaluation result.
Expand Down
49 changes: 49 additions & 0 deletions lib/index.ts
Original file line number Diff line number Diff line change
@@ -0,0 +1,49 @@
// Core evaluator exports
export { stepOnceImmediate, stepOnceSKI } from './evaluator/skiEvaluator.js';

// SKI expression exports
export {
generateExpr,
prettyPrint as prettyPrintSKI,
type SKIExpression
} from './ski/expression.js';

// Parser exports
export { parseSKI } from './parser/ski.js';
export { parseLambda } from './parser/untyped.js';
export { parseSystemF } from './parser/systemFTerm.js';
export { parseTypedLambda } from './parser/typed.js';

// Lambda terms exports
export {
prettyPrintUntypedLambda,
type UntypedLambda
} from './terms/lambda.js';

// System F exports
export {
prettyPrintSystemF,
type SystemFTerm
} from './terms/systemF.js';

// Typed Lambda exports
export {
eraseTypedLambda,
prettyPrintTypedLambda,
type TypedLambda,
typecheck as typecheckTyped
} from './types/typedLambda.js';

// System F type exports
export {
eraseSystemF,
prettyPrintSystemFType,
typecheck as typecheckSystemF
} from './types/systemF.js';

// Conversion exports
export { convertLambda } from './conversion/converter.js';

// Type system exports
export { prettyPrintTy } from './types/types.js';
export { inferType } from './types/inference.js';
6 changes: 3 additions & 3 deletions lib/parser/chain.ts
Original file line number Diff line number Diff line change
@@ -1,6 +1,6 @@
import { cons } from '../cons.ts';
import { ParseError } from './parseError.ts';
import { RecursiveDescentBuffer } from './recursiveDescentBuffer.ts';
import { cons } from '../cons.js';
import { ParseError } from './parseError.js';
import { RecursiveDescentBuffer } from './recursiveDescentBuffer.js';

export function parseLambdaChain<T>(
rdb: RecursiveDescentBuffer,
Expand Down
4 changes: 2 additions & 2 deletions lib/parser/eof.ts
Original file line number Diff line number Diff line change
@@ -1,5 +1,5 @@
import { RecursiveDescentBuffer } from './recursiveDescentBuffer.ts';
import { ParseError } from './parseError.ts';
import { RecursiveDescentBuffer } from './recursiveDescentBuffer.js';
import { ParseError } from './parseError.js';

/**
* Wraps a parser function so that after parsing the input,
Expand Down
2 changes: 1 addition & 1 deletion lib/parser/recursiveDescentBuffer.ts
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
import { ParseError } from './parseError.ts';
import { ParseError } from './parseError.js';

export class RecursiveDescentBuffer {
buf!: string;
Expand Down
12 changes: 6 additions & 6 deletions lib/parser/ski.ts
Original file line number Diff line number Diff line change
@@ -1,9 +1,9 @@
import { SKIExpression } from '../ski/expression.ts';
import { RecursiveDescentBuffer } from './recursiveDescentBuffer.ts';
import { ParseError } from './parseError.ts';
import { parseWithEOF } from './eof.ts';
import { cons } from '../cons.ts';
import { SKITerminalSymbol, term } from '../ski/terminal.ts';
import { SKIExpression } from '../ski/expression.js';
import { RecursiveDescentBuffer } from './recursiveDescentBuffer.js';
import { ParseError } from './parseError.js';
import { parseWithEOF } from './eof.js';
import { cons } from '../cons.js';
import { SKITerminalSymbol, term } from '../ski/terminal.js';

/**
* Parses a chain of SKI atomic terms (term { term }).
Expand Down
12 changes: 6 additions & 6 deletions lib/parser/systemFTerm.ts
Original file line number Diff line number Diff line change
@@ -1,9 +1,9 @@
import { cons } from '../cons.ts';
import { SystemFTerm, mkSystemFAbs, mkSystemFTAbs, mkSystemFVar, mkSystemFTypeApp } from '../terms/systemF.ts';
import { parseWithEOF } from './eof.ts';
import { ParseError } from './parseError.ts';
import { RecursiveDescentBuffer } from './recursiveDescentBuffer.ts';
import { parseSystemFType } from './systemFType.ts';
import { cons } from '../cons.js';
import { SystemFTerm, mkSystemFAbs, mkSystemFTAbs, mkSystemFVar, mkSystemFTypeApp } from '../terms/systemF.js';
import { parseWithEOF } from './eof.js';
import { ParseError } from './parseError.js';
import { RecursiveDescentBuffer } from './recursiveDescentBuffer.js';
import { parseSystemFType } from './systemFType.js';

/**
* Parses an atomic System F term.
Expand Down
8 changes: 4 additions & 4 deletions lib/parser/systemFType.ts
Original file line number Diff line number Diff line change
@@ -1,7 +1,7 @@
import { SystemFType, forall } from '../types/systemF.ts';
import { arrow, mkTypeVariable } from '../types/types.ts';
import { ParseError } from './parseError.ts';
import { RecursiveDescentBuffer } from './recursiveDescentBuffer.ts';
import { SystemFType, forall } from '../types/systemF.js';
import { arrow, mkTypeVariable } from '../types/types.js';
import { ParseError } from './parseError.js';
import { RecursiveDescentBuffer } from './recursiveDescentBuffer.js';

/**
* Parses a System F type.
Expand Down
8 changes: 4 additions & 4 deletions lib/parser/type.ts
Original file line number Diff line number Diff line change
@@ -1,7 +1,7 @@
import { RecursiveDescentBuffer } from './recursiveDescentBuffer.ts';
import { ParseError } from './parseError.ts';
import { BaseType, arrow, mkTypeVariable } from '../types/types.ts';
import { parseWithEOF } from './eof.ts';
import { RecursiveDescentBuffer } from './recursiveDescentBuffer.js';
import { ParseError } from './parseError.js';
import { BaseType, arrow, mkTypeVariable } from '../types/types.js';
import { parseWithEOF } from './eof.js';

/**
* Parses a "simple" type.
Expand Down
12 changes: 6 additions & 6 deletions lib/parser/typed.ts
Original file line number Diff line number Diff line change
@@ -1,9 +1,9 @@
import { mkVar } from '../terms/lambda.ts';
import { TypedLambda, mkTypedAbs } from '../types/typedLambda.ts';
import { RecursiveDescentBuffer } from './recursiveDescentBuffer.ts';
import { parseLambdaChain } from './chain.ts';
import { parseArrowType } from './type.ts';
import { parseWithEOF } from './eof.ts';
import { mkVar } from '../terms/lambda.js';
import { TypedLambda, mkTypedAbs } from '../types/typedLambda.js';
import { RecursiveDescentBuffer } from './recursiveDescentBuffer.js';
import { parseLambdaChain } from './chain.js';
import { parseArrowType } from './type.js';
import { parseWithEOF } from './eof.js';

function parseAtomicTypedLambda(
rdb: RecursiveDescentBuffer
Expand Down
8 changes: 4 additions & 4 deletions lib/parser/untyped.ts
Original file line number Diff line number Diff line change
@@ -1,7 +1,7 @@
import { UntypedLambda, mkUntypedAbs, mkVar } from '../terms/lambda.ts';
import { RecursiveDescentBuffer } from './recursiveDescentBuffer.ts';
import { parseLambdaChain } from './chain.ts';
import { parseWithEOF } from './eof.ts';
import { UntypedLambda, mkUntypedAbs, mkVar } from '../terms/lambda.js';
import { RecursiveDescentBuffer } from './recursiveDescentBuffer.js';
import { parseLambdaChain } from './chain.js';
import { parseWithEOF } from './eof.js';

function parseUntypedLambdaInternal(
rdb: RecursiveDescentBuffer
Expand Down
8 changes: 4 additions & 4 deletions lib/ski/church.ts
Original file line number Diff line number Diff line change
@@ -1,7 +1,7 @@
import { Zero, One, Succ, True, False } from '../consts/combinators.ts';
import { apply, SKIExpression } from './expression.ts';
import { SKITerminalSymbol } from './terminal.ts';
import { reduceSKI } from '../evaluator/skiEvaluator.ts';
import { Zero, One, Succ, True, False } from '../consts/combinators.js';
import { apply, SKIExpression } from './expression.js';
import { SKITerminalSymbol } from './terminal.js';
import { reduceSKI } from '../evaluator/skiEvaluator.js';

/**
* @see https://en.wikipedia.org/wiki/Church_encoding
Expand Down
9 changes: 5 additions & 4 deletions lib/ski/expression.ts
Original file line number Diff line number Diff line change
@@ -1,7 +1,8 @@
import { RandomSeed } from 'random-seed';
import { ConsCell, cons } from '../cons.ts';
import { stepOnceSKI } from '../evaluator/skiEvaluator.ts';
import { SKITerminal, generate } from './terminal.ts';

import { ConsCell, cons } from '../cons.js';
import { stepOnceSKI } from '../evaluator/skiEvaluator.js';
import { SKITerminal, generate } from './terminal.js';

/*
* EBNF grammar:
Expand Down Expand Up @@ -153,4 +154,4 @@ SKIExpression => {
}
};

export { reduceSKI } from '../evaluator/skiEvaluator.ts';
export { reduceSKI } from '../evaluator/skiEvaluator.js';
6 changes: 3 additions & 3 deletions lib/ski/packer.ts
Original file line number Diff line number Diff line change
@@ -1,6 +1,6 @@
import { cons } from '../cons.ts';
import { SKIExpression } from './expression.ts';
import { SKITerminalSymbol, term } from './terminal.ts';
import { cons } from '../cons.js';
import { SKIExpression } from './expression.js';
import { SKITerminalSymbol, term } from './terminal.js';

export type SymbolHeap = (SKITerminalSymbol | undefined)[];

Expand Down
2 changes: 1 addition & 1 deletion lib/terms/lambda.ts
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
import { ConsCell, cons } from '../cons.ts';
import { ConsCell, cons } from '../cons.js';

/**
* This is a single term variable with a name.
Expand Down
4 changes: 2 additions & 2 deletions lib/terms/systemF.ts
Original file line number Diff line number Diff line change
@@ -1,5 +1,5 @@
import { ConsCell } from '../cons.ts';
import { SystemFType } from '../types/systemF.ts';
import { ConsCell } from '../cons.js';
import { SystemFType } from '../types/systemF.js';

/**
* A term variable.
Expand Down
Loading

0 comments on commit 73adb7f

Please sign in to comment.